PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-par32-5-c.opb
MD5SUM	b2d6fc6e4e4b51f8b59d0f4ed12a9f74
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	2678
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	2678
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2678
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	2678
Total number of constraints	6689
Number of constraints which are clauses	6689
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	3
Trace number 5560

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-14 00:26:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3971 boxname=wulflinc29 idbench=211 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b2d6fc6e4e4b51f8b59d0f4ed12a9f74  /oldhome/oroussel/tmp/wulflinc29/normalized-par32-5-c.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-par32-5-c.opb /oldhome/oroussel/tmp/wulflinc29/normalized-par32-5-c.opb
IDLAUNCH: 3971
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        831880 kB
Buffers:         36180 kB
Cached:         128980 kB
SwapCached:         12 kB
Active:          53184 kB
Inactive:       114876 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        831628 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29024 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:47:01 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 3971 7 1200.32 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6689 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    6689    18356 |    2006       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2678          
c   -- var.elim.:  2000/2678          
c   -- var.elim.:  2678/2678          
c |         0 |    6567    17990 |      --       0       --      -- |     --   | -122/-366
c |         0 |    6567    17990 |    2626       0        0     nan |  0.000 % |
c |       101 |    6567    17990 |    2889     101     3393    33.6 |  0.003 % |
c |       252 |    6567    17990 |    3178     252     8708    34.6 |  0.000 % |
c |       478 |    6567    17990 |    3496     478    15936    33.3 |  0.000 % |
c |       815 |    6567    17990 |    3845     815    27499    33.7 |  0.000 % |
c |      1321 |    6567    17990 |    4230    1321    47133    35.7 |  0.000 % |
c |      2081 |    6560    17970 |    4648    2080    75078    36.1 |  0.075 % |
c |      3220 |    6560    17970 |    5113    3219   123060    38.2 |  0.075 % |
c |      4#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.94 2/54 32137
Raw data (stat): 32137 (runsolver) R 32136 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480260747 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1070 0 0 0 996 2 0 0 25 0 1 0 480260747 5885952 1048 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1437 1048 603 41 0 1396 0
vsize: 5748
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1195 0 0 0 1995 3 0 0 25 0 1 0 480260747 6402048 1173 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1563 1173 603 41 0 1522 0
vsize: 6252
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1412 0 0 0 2995 3 0 0 25 0 1 0 480260747 7372800 1390 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1800 1390 603 41 0 1759 0
vsize: 7200
[startup+40.001 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1444 0 0 0 3995 3 0 0 25 0 1 0 480260747 7524352 1422 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1837 1422 603 41 0 1796 0
vsize: 7348
[startup+50.002 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1488 0 0 0 4995 3 0 0 25 0 1 0 480260747 7655424 1466 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1869 1466 603 41 0 1828 0
vsize: 7476
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1515 0 0 0 5995 3 0 0 25 0 1 0 480260747 7811072 1493 4294967295 134512640 134672761 3221224560 3221223744 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1907 1493 603 41 0 1866 0
vsize: 7628
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1599 0 0 0 6996 4 0 0 25 0 1 0 480260747 8159232 1577 4294967295 134512640 134672761 3221224560 3221223552 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1992 1577 603 41 0 1951 0
vsize: 7968
[startup+80.0024 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1614 0 0 0 7996 4 0 0 25 0 1 0 480260747 8159232 1592 4294967295 134512640 134672761 3221224560 3221223760 134610614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1992 1592 603 41 0 1951 0
vsize: 7968
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1653 0 0 0 8996 4 0 0 25 0 1 0 480260747 8380416 1631 4294967295 134512640 134672761 3221224560 3221223600 134612650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2046 1631 603 41 0 2005 0
vsize: 8184
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1673 0 0 0 9996 4 0 0 25 0 1 0 480260747 8462336 1651 4294967295 134512640 134672761 3221224560 3221223712 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2066 1651 603 41 0 2025 0
vsize: 8264
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1752 0 0 0 10996 4 0 0 25 0 1 0 480260747 8777728 1730 4294967295 134512640 134672761 3221224560 3221223600 134613025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2143 1730 603 41 0 2102 0
vsize: 8572
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1752 0 0 0 11996 4 0 0 25 0 1 0 480260747 8769536 1730 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2141 1730 603 41 0 2100 0
vsize: 8564
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1760 0 0 0 12996 4 0 0 25 0 1 0 480260747 8769536 1738 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2141 1738 603 41 0 2100 0
vsize: 8564
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1806 0 0 0 13996 4 0 0 25 0 1 0 480260747 8998912 1784 4294967295 134512640 134672761 3221224560 3221223600 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2197 1784 603 41 0 2156 0
vsize: 8788
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1823 0 0 0 14996 4 0 0 25 0 1 0 480260747 9068544 1801 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2214 1801 603 41 0 2173 0
vsize: 8856
[startup+160.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1864 0 0 0 15996 4 0 0 25 0 1 0 480260747 9199616 1842 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2246 1842 603 41 0 2205 0
vsize: 8984
[startup+170.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1902 0 0 0 16996 5 0 0 25 0 1 0 480260747 9465856 1880 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2311 1880 603 41 0 2270 0
vsize: 9244
[startup+180.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1935 0 0 0 17996 5 0 0 25 0 1 0 480260747 9465856 1913 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2311 1913 603 41 0 2270 0
vsize: 9244
[startup+190.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1943 0 0 0 18996 5 0 0 25 0 1 0 480260747 9564160 1921 4294967295 134512640 134672761 3221224560 3221223616 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2335 1921 603 41 0 2294 0
vsize: 9340
[startup+200.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1943 0 0 0 19997 5 0 0 25 0 1 0 480260747 9564160 1921 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2335 1921 603 41 0 2294 0
vsize: 9340
[startup+210.001 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1950 0 0 0 20997 5 0 0 25 0 1 0 480260747 9564160 1928 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2335 1928 603 41 0 2294 0
vsize: 9340
[startup+220.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1950 0 0 0 21997 5 0 0 25 0 1 0 480260747 9564160 1928 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2335 1928 603 41 0 2294 0
vsize: 9340
[startup+230.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1951 0 0 0 22997 5 0 0 25 0 1 0 480260747 9564160 1929 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2335 1929 603 41 0 2294 0
vsize: 9340
[startup+240.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1989 0 0 0 23997 5 0 0 25 0 1 0 480260747 9699328 1967 4294967295 134512640 134672761 3221224560 3221223760 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1967 603 41 0 2327 0
vsize: 9472
[startup+250.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 1989 0 0 0 24997 5 0 0 25 0 1 0 480260747 9699328 1967 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2368 1967 603 41 0 2327 0
vsize: 9472
[startup+260.002 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2005 0 0 0 25998 5 0 0 25 0 1 0 480260747 9789440 1983 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2390 1983 603 41 0 2349 0
vsize: 9560
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2032 0 0 0 26998 5 0 0 25 0 1 0 480260747 9920512 2010 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2422 2010 603 41 0 2381 0
vsize: 9688
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2040 0 0 0 27998 5 0 0 25 0 1 0 480260747 9920512 2018 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2422 2018 603 41 0 2381 0
vsize: 9688
[startup+290.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2049 0 0 0 28998 5 0 0 25 0 1 0 480260747 9990144 2027 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2439 2027 603 41 0 2398 0
vsize: 9756
[startup+300.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2049 0 0 0 29998 5 0 0 25 0 1 0 480260747 9990144 2027 4294967295 134512640 134672761 3221224560 3221223600 134603536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2439 2027 603 41 0 2398 0
vsize: 9756
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2049 0 0 0 30998 5 0 0 25 0 1 0 480260747 9990144 2027 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2439 2027 603 41 0 2398 0
vsize: 9756
[startup+320.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2053 0 0 0 31999 5 0 0 25 0 1 0 480260747 9990144 2031 4294967295 134512640 134672761 3221224560 3221223600 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2439 2031 603 41 0 2398 0
vsize: 9756
[startup+330.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2089 0 0 0 32999 5 0 0 25 0 1 0 480260747 10121216 2067 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2471 2067 603 41 0 2430 0
vsize: 9884
[startup+340.004 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2133 0 0 0 33999 5 0 0 25 0 1 0 480260747 10334208 2111 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2523 2111 603 41 0 2482 0
vsize: 10092
[startup+350.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2136 0 0 0 34999 5 0 0 25 0 1 0 480260747 10334208 2114 4294967295 134512640 134672761 3221224560 3221223744 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2523 2114 603 41 0 2482 0
vsize: 10092
[startup+360.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2136 0 0 0 35999 5 0 0 25 0 1 0 480260747 10334208 2114 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2523 2114 603 41 0 2482 0
vsize: 10092
[startup+370.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2136 0 0 0 36999 5 0 0 25 0 1 0 480260747 10334208 2114 4294967295 134512640 134672761 3221224560 3221223744 134616005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2523 2114 603 41 0 2482 0
vsize: 10092
[startup+380.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2136 0 0 0 38000 5 0 0 25 0 1 0 480260747 10326016 2114 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2114 603 41 0 2480 0
vsize: 10084
[startup+390.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2137 0 0 0 39000 5 0 0 25 0 1 0 480260747 10326016 2115 4294967295 134512640 134672761 3221224560 3221223696 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2115 603 41 0 2480 0
vsize: 10084
[startup+400.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2137 0 0 0 40000 5 0 0 25 0 1 0 480260747 10326016 2115 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2115 603 41 0 2480 0
vsize: 10084
[startup+410.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2137 0 0 0 41000 5 0 0 25 0 1 0 480260747 10326016 2115 4294967295 134512640 134672761 3221224560 3221223760 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2115 603 41 0 2480 0
vsize: 10084
[startup+420.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2138 0 0 0 42000 5 0 0 25 0 1 0 480260747 10326016 2116 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2116 603 41 0 2480 0
vsize: 10084
[startup+430.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2138 0 0 0 43001 5 0 0 25 0 1 0 480260747 10326016 2116 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2116 603 41 0 2480 0
vsize: 10084
[startup+440.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2138 0 0 0 44001 5 0 0 25 0 1 0 480260747 10326016 2116 4294967295 134512640 134672761 3221224560 3221223696 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2116 603 41 0 2480 0
vsize: 10084
[startup+450.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2138 0 0 0 45001 5 0 0 25 0 1 0 480260747 10326016 2116 4294967295 134512640 134672761 3221224560 3221223616 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2116 603 41 0 2480 0
vsize: 10084
[startup+460.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2138 0 0 0 46001 5 0 0 25 0 1 0 480260747 10326016 2116 4294967295 134512640 134672761 3221224560 3221223744 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2116 603 41 0 2480 0
vsize: 10084
[startup+470.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2138 0 0 0 47001 5 0 0 25 0 1 0 480260747 10326016 2116 4294967295 134512640 134672761 3221224560 3221223600 134613015 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2521 2116 603 41 0 2480 0
vsize: 10084
[startup+480.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2213 0 0 0 48001 5 0 0 25 0 1 0 480260747 10588160 2191 4294967295 134512640 134672761 3221224560 3221223712 134565121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2585 2191 603 41 0 2544 0
vsize: 10340
[startup+490.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2237 0 0 0 49001 5 0 0 25 0 1 0 480260747 10719232 2215 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2215 603 41 0 2576 0
vsize: 10468
[startup+500.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2237 0 0 0 50002 5 0 0 25 0 1 0 480260747 10719232 2215 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2215 603 41 0 2576 0
vsize: 10468
[startup+510.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 51001 5 0 0 25 0 1 0 480260747 10719232 2216 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2617 2216 603 41 0 2576 0
vsize: 10468
[startup+520.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 52001 6 0 0 25 0 1 0 480260747 10719232 2216 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2216 603 41 0 2576 0
vsize: 10468
[startup+530.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 53001 6 0 0 25 0 1 0 480260747 10719232 2216 4294967295 134512640 134672761 3221224560 3221223696 134614685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2216 603 41 0 2576 0
vsize: 10468
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 54001 6 0 0 25 0 1 0 480260747 10706944 2216 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2216 603 41 0 2573 0
vsize: 10456
[startup+550.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 55002 6 0 0 25 0 1 0 480260747 10706944 2216 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2216 603 41 0 2573 0
vsize: 10456
[startup+560.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 56002 6 0 0 25 0 1 0 480260747 10706944 2216 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2216 603 41 0 2573 0
vsize: 10456
[startup+570.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 57002 6 0 0 25 0 1 0 480260747 10706944 2216 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2216 603 41 0 2573 0
vsize: 10456
[startup+580.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 58002 6 0 0 25 0 1 0 480260747 10706944 2216 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2216 603 41 0 2573 0
vsize: 10456
[startup+590.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 59002 6 0 0 25 0 1 0 480260747 10706944 2216 4294967295 134512640 134672761 3221224560 3221223744 134615544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2216 603 41 0 2573 0
vsize: 10456
[startup+600.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2238 0 0 0 60003 6 0 0 25 0 1 0 480260747 10706944 2216 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2216 603 41 0 2573 0
vsize: 10456
[startup+610.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2239 0 0 0 61003 6 0 0 25 0 1 0 480260747 10706944 2217 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2217 603 41 0 2573 0
vsize: 10456
[startup+620.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2239 0 0 0 62003 6 0 0 25 0 1 0 480260747 10706944 2217 4294967295 134512640 134672761 3221224560 3221223552 134565140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2217 603 41 0 2573 0
vsize: 10456
[startup+630.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2239 0 0 0 63003 6 0 0 25 0 1 0 480260747 10706944 2217 4294967295 134512640 134672761 3221224560 3221223600 134612510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2614 2217 603 41 0 2573 0
vsize: 10456
[startup+640.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2318 0 0 0 64003 6 0 0 25 0 1 0 480260747 11071488 2296 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2703 2296 603 41 0 2662 0
vsize: 10812
[startup+650.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 65003 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+660.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 66003 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+670.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 67004 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223724 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+680.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 68004 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+690.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 69004 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+700.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 70004 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+710.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 71004 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+720.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 72005 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+730.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 73005 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+740.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 74005 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+750.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 75005 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+760.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 76005 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+770.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 77006 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+780.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 78006 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223616 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+790.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 79006 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+800.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 80006 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+810.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 81006 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+820.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2368 0 0 0 82007 6 0 0 25 0 1 0 480260747 11337728 2346 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2346 603 41 0 2727 0
vsize: 11072
[startup+830.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2376 0 0 0 83007 6 0 0 25 0 1 0 480260747 11337728 2354 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2354 603 41 0 2727 0
vsize: 11072
[startup+840.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2376 0 0 0 84007 6 0 0 25 0 1 0 480260747 11337728 2354 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2354 603 41 0 2727 0
vsize: 11072
[startup+850.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2376 0 0 0 85007 6 0 0 25 0 1 0 480260747 11337728 2354 4294967295 134512640 134672761 3221224560 3221223696 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2354 603 41 0 2727 0
vsize: 11072
[startup+860.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2376 0 0 0 86007 6 0 0 25 0 1 0 480260747 11337728 2354 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2354 603 41 0 2727 0
vsize: 11072
[startup+870.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2376 0 0 0 87007 6 0 0 25 0 1 0 480260747 11337728 2354 4294967295 134512640 134672761 3221224560 3221223600 134612575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2768 2354 603 41 0 2727 0
vsize: 11072
[startup+880.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2378 0 0 0 88008 6 0 0 25 0 1 0 480260747 11370496 2355 4294967295 134512640 134672761 3221224560 3221223760 134610669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2355 603 41 0 2735 0
vsize: 11104
[startup+890.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2378 0 0 0 89008 6 0 0 25 0 1 0 480260747 11370496 2355 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2355 603 41 0 2735 0
vsize: 11104
[startup+900.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2378 0 0 0 90008 6 0 0 25 0 1 0 480260747 11370496 2355 4294967295 134512640 134672761 3221224560 3221223412 1075349627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2355 603 41 0 2735 0
vsize: 11104
[startup+910.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2378 0 0 0 91008 6 0 0 25 0 1 0 480260747 11370496 2355 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2355 603 41 0 2735 0
vsize: 11104
[startup+920.017 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2382 0 0 0 92008 6 0 0 25 0 1 0 480260747 11370496 2359 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2359 603 41 0 2735 0
vsize: 11104
[startup+930.018 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2406 0 0 0 93009 6 0 0 25 0 1 0 480260747 11456512 2383 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2797 2383 603 41 0 2756 0
vsize: 11188
[startup+940.017 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2406 0 0 0 94009 6 0 0 25 0 1 0 480260747 11456512 2383 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2797 2383 603 41 0 2756 0
vsize: 11188
[startup+950.018 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2496 0 0 0 95009 6 0 0 25 0 1 0 480260747 11845632 2473 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2892 2473 603 41 0 2851 0
vsize: 11568
[startup+960.018 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2510 0 0 0 96009 6 0 0 25 0 1 0 480260747 11894784 2486 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2904 2486 603 41 0 2863 0
vsize: 11616
[startup+970.019 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2527 0 0 0 97009 6 0 0 25 0 1 0 480260747 11960320 2502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2920 2502 603 41 0 2879 0
vsize: 11680
[startup+980.019 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2527 0 0 0 98009 6 0 0 25 0 1 0 480260747 11960320 2502 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2920 2502 603 41 0 2879 0
vsize: 11680
[startup+990.018 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2527 0 0 0 99009 6 0 0 25 0 1 0 480260747 11960320 2502 4294967295 134512640 134672761 3221224560 3221223600 134612771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2920 2502 603 41 0 2879 0
vsize: 11680
[startup+1000.02 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2527 0 0 0 100010 6 0 0 25 0 1 0 480260747 11960320 2502 4294967295 134512640 134672761 3221224560 3221223744 134615945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2920 2502 603 41 0 2879 0
vsize: 11680
[startup+1010.02 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2527 0 0 0 101010 6 0 0 25 0 1 0 480260747 11960320 2502 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2920 2502 603 41 0 2879 0
vsize: 11680
[startup+1020.02 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2527 0 0 0 102010 6 0 0 25 0 1 0 480260747 11960320 2502 4294967295 134512640 134672761 3221224560 3221223760 134610683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2920 2502 603 41 0 2879 0
vsize: 11680
[startup+1030.02 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2546 0 0 0 103010 6 0 0 25 0 1 0 480260747 12156928 2521 4294967295 134512640 134672761 3221224560 3221223616 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2968 2521 603 41 0 2927 0
vsize: 11872
[startup+1040.02 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2550 0 0 0 104010 6 0 0 25 0 1 0 480260747 12034048 2523 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2938 2523 603 41 0 2897 0
vsize: 11752
[startup+1050.02 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2550 0 0 0 105011 6 0 0 25 0 1 0 480260747 12034048 2523 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2938 2523 603 41 0 2897 0
vsize: 11752
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2550 0 0 0 106011 6 0 0 25 0 1 0 480260747 12034048 2523 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2938 2523 603 41 0 2897 0
vsize: 11752
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2550 0 0 0 107011 6 0 0 25 0 1 0 480260747 12034048 2523 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2938 2523 603 41 0 2897 0
vsize: 11752
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2550 0 0 0 108011 6 0 0 25 0 1 0 480260747 12034048 2523 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2938 2523 603 41 0 2897 0
vsize: 11752
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2556 0 0 0 109011 6 0 0 25 0 1 0 480260747 12050432 2528 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2528 603 41 0 2901 0
vsize: 11768
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2556 0 0 0 110012 6 0 0 25 0 1 0 480260747 12050432 2528 4294967295 134512640 134672761 3221224560 3221223600 134612972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2942 2528 603 41 0 2901 0
vsize: 11768
[startup+1110.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2561 0 0 0 111023 6 0 0 25 0 1 0 480260747 12062720 2532 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2945 2532 603 41 0 2904 0
vsize: 11780
[startup+1120.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2561 0 0 0 112023 6 0 0 25 0 1 0 480260747 12062720 2532 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2945 2532 603 41 0 2904 0
vsize: 11780
[startup+1130.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2561 0 0 0 113023 6 0 0 25 0 1 0 480260747 12062720 2532 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2945 2532 603 41 0 2904 0
vsize: 11780
[startup+1140.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2567 0 0 0 114023 6 0 0 25 0 1 0 480260747 12083200 2537 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2950 2537 603 41 0 2909 0
vsize: 11800
[startup+1150.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2567 0 0 0 115023 6 0 0 25 0 1 0 480260747 12083200 2537 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2950 2537 603 41 0 2909 0
vsize: 11800
[startup+1160.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2574 0 0 0 116023 6 0 0 25 0 1 0 480260747 12115968 2543 4294967295 134512640 134672761 3221224560 3221223744 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2543 603 41 0 2917 0
vsize: 11832
[startup+1170.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2574 0 0 0 117024 6 0 0 25 0 1 0 480260747 12115968 2543 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2543 603 41 0 2917 0
vsize: 11832
[startup+1180.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2574 0 0 0 118024 6 0 0 25 0 1 0 480260747 12115968 2543 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2543 603 41 0 2917 0
vsize: 11832
[startup+1190.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2574 0 0 0 119024 6 0 0 25 0 1 0 480260747 12115968 2543 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2543 603 41 0 2917 0
vsize: 11832
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 32137
Raw data (stat): 32137 (minisat+) R 32136 27222 27221 0 -1 0 2574 0 0 0 120024 6 0 0 25 0 1 0 480260747 12115968 2543 4294967295 134512640 134672761 3221224560 3221223600 134612966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2958 2543 603 41 0 2917 0
vsize: 11832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 32137
Raw data (stat): 32137 (minisat+) Z 32136 27222 27221 0 -1 12 2574 0 0 0 120024 7 0 0 25 0 1 0 480260747 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.14
CPU time (s): 1200.32
CPU user time (s): 1200.25
CPU system time (s): 0.073988
CPU usage (%): 100.015
Max. virtual memory (Kb): 11872
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####