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/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-nw04.opb
MD5SUM	a5c401bba5afccf02c7b40cb1c595b15
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	30407
Optimality of the best value was proved	NO
Number of terms in the objective function	87482
Biggest coefficient in the objective function	5220
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	120189580
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	5220
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1192.4
Number of variables	87482
Total number of constraints	87518
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	87518
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	42032
Trace number 18032

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 13:14:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18680 boxname=wulflinc19 idbench=1437 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-nw04.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 18680
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        752504 kB
Buffers:         18356 kB
Cached:         238944 kB
SwapCached:        556 kB
Active:          51300 kB
Inactive:       208040 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        752252 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            17180 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:32:29 (client local time) WITH STATUS 0 IN 1066.83 SECONDS
stats: 18680 7 1066.83 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### 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): 1.15 1.02 0.93 2/55 1158
Raw data (stat): 1158 (runsolver) R 1157 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545353618 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99996 s]
Raw data (loadavg): 1.13 1.02 0.93 2/55 1158
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 22973 0 0 0 943 55 0 0 25 0 1 0 545353618 64581632 7176 4294967295 134512640 134672761 3221224544 3220489872 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+20.0011 s]
Raw data (loadavg): 1.11 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 22973 0 0 0 1942 56 0 0 25 0 1 0 545353618 64581632 7176 4294967295 134512640 134672761 3221224544 3220821744 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+30.0005 s]
Raw data (loadavg): 1.09 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 23318 0 0 0 2941 57 0 0 25 0 1 0 545353618 65994752 7521 4294967295 134512640 134672761 3221224544 3220664496 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16112 7521 603 41 0 16071 0
vsize: 64448
[startup+40.0003 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 23706 0 0 0 3940 59 0 0 25 0 1 0 545353618 69140480 7909 4294967295 134512640 134672761 3221224544 3220460800 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16880 7909 603 41 0 16839 0
vsize: 67520
[startup+50.0015 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 23947 0 0 0 4940 59 0 0 25 0 1 0 545353618 69771264 8150 4294967295 134512640 134672761 3221224544 3220440928 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17034 8150 603 41 0 16993 0
vsize: 68136
[startup+60.0009 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 24678 0 0 0 5937 62 0 0 25 0 1 0 545353618 71118848 8551 4294967295 134512640 134672761 3221224544 3220697424 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8551 603 41 0 17322 0
vsize: 69452
[startup+70.0008 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 24761 0 0 0 6937 62 0 0 25 0 1 0 545353618 71118848 8634 4294967295 134512640 134672761 3221224544 3220232704 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8634 603 41 0 17322 0
vsize: 69452
[startup+80.0009 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 24841 0 0 0 7937 62 0 0 25 0 1 0 545353618 71118848 8714 4294967295 134512640 134672761 3221224544 3220168428 134594032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8714 603 41 0 17322 0
vsize: 69452
[startup+90.0004 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 25087 0 0 0 8936 64 0 0 25 0 1 0 545353618 74571776 8877 4294967295 134512640 134672761 3221224544 3220644640 134594092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18206 8877 603 41 0 18165 0
vsize: 72824
[startup+100 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 25451 0 0 0 9935 65 0 0 25 0 1 0 545353618 75153408 9116 4294967295 134512640 134672761 3221224544 3220714800 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18348 9116 603 41 0 18307 0
vsize: 73392
[startup+110 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 25630 0 0 0 10934 66 0 0 25 0 1 0 545353618 75591680 9253 4294967295 134512640 134672761 3221224544 3220366512 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18455 9253 603 41 0 18414 0
vsize: 73820
[startup+120.001 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 27444 0 0 0 11930 70 0 0 25 0 1 0 545353618 79650816 10325 4294967295 134512640 134672761 3221224544 3220337808 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19446 10326 603 41 0 19405 0
vsize: 77784
[startup+130.001 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 27583 0 0 0 12929 71 0 0 25 0 1 0 545353618 79953920 10422 4294967295 134512640 134672761 3221224544 3220997424 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19520 10422 603 41 0 19479 0
vsize: 78080
[startup+140.001 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 27601 0 0 0 13929 71 0 0 25 0 1 0 545353618 79953920 10440 4294967295 134512640 134672761 3221224544 3220279168 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19520 10440 603 41 0 19479 0
vsize: 78080
[startup+150.001 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 27601 0 0 0 14929 72 0 0 25 0 1 0 545353618 79953920 10440 4294967295 134512640 134672761 3221224544 3219355744 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19520 10440 603 41 0 19479 0
vsize: 78080
[startup+160.001 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 27999 0 0 0 15928 73 0 0 25 0 1 0 545353618 80965632 10755 4294967295 134512640 134672761 3221224544 3220697904 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19767 10755 603 41 0 19726 0
vsize: 79068
[startup+170.001 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 28243 0 0 0 16927 74 0 0 25 0 1 0 545353618 81002496 10834 4294967295 134512640 134672761 3221224544 3220461648 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19776 10834 603 41 0 19735 0
vsize: 79104
[startup+180.002 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 28388 0 0 0 17926 75 0 0 25 0 1 0 545353618 81305600 10937 4294967295 134512640 134672761 3221224544 3221211792 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19850 10937 603 41 0 19809 0
vsize: 79400
[startup+190.001 s]
Raw data (loadavg): 1.05 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 28389 0 0 0 18926 75 0 0 25 0 1 0 545353618 81305600 10938 4294967295 134512640 134672761 3221224544 3220099648 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19850 10938 603 41 0 19809 0
vsize: 79400
[startup+200.002 s]
Raw data (loadavg): 1.04 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 28724 0 0 0 19925 77 0 0 25 0 1 0 545353618 82182144 11190 4294967295 134512640 134672761 3221224544 3220868016 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20064 11190 603 41 0 20023 0
vsize: 80256
[startup+210.002 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 28949 0 0 0 20924 77 0 0 25 0 1 0 545353618 82137088 11250 4294967295 134512640 134672761 3221224544 3221009520 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20053 11250 603 41 0 20012 0
vsize: 80212
[startup+220.002 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 29050 0 0 0 21924 78 0 0 25 0 1 0 545353618 82305024 11309 4294967295 134512640 134672761 3221224544 3220336384 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20094 11309 603 41 0 20053 0
vsize: 80376
[startup+230.002 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 29536 0 0 0 22922 80 0 0 25 0 1 0 545353618 82890752 11547 4294967295 134512640 134672761 3221224544 3219827856 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20237 11547 603 41 0 20196 0
vsize: 80948
[startup+240.001 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 29695 0 0 0 23921 81 0 0 25 0 1 0 545353618 83193856 11664 4294967295 134512640 134672761 3221224544 3220918992 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20311 11664 603 41 0 20270 0
vsize: 81244
[startup+250.002 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 29721 0 0 0 24921 81 0 0 25 0 1 0 545353618 83329024 11690 4294967295 134512640 134672761 3221224544 3220478368 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20344 11690 603 41 0 20303 0
vsize: 81376
[startup+260.002 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 29721 0 0 0 25921 82 0 0 25 0 1 0 545353618 83329024 11690 4294967295 134512640 134672761 3221224544 3219096448 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20344 11690 603 41 0 20303 0
vsize: 81376
[startup+270.003 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 30137 0 0 0 26920 83 0 0 25 0 1 0 545353618 89968640 11858 4294967295 134512640 134672761 3221224544 3219057648 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21965 11858 603 41 0 21924 0
vsize: 87860
[startup+280.003 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 30390 0 0 0 27919 84 0 0 25 0 1 0 545353618 90578944 12069 4294967295 134512640 134672761 3221224544 3220719504 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22114 12069 603 41 0 22073 0
vsize: 88456
[startup+290.003 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 30431 0 0 0 28919 84 0 0 25 0 1 0 545353618 90714112 12110 4294967295 134512640 134672761 3221224544 3220621696 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22147 12110 603 41 0 22106 0
vsize: 88588
[startup+300.003 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 30431 0 0 0 29918 85 0 0 25 0 1 0 545353618 90714112 12110 4294967295 134512640 134672761 3221224544 3219899968 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22147 12110 603 41 0 22106 0
vsize: 88588
[startup+310.003 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 1160
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 30753 0 0 0 30917 86 0 0 25 0 1 0 545353618 91455488 12349 4294967295 134512640 134672761 3221224544 3220562640 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22328 12349 603 41 0 22287 0
vsize: 89312
[startup+320.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 30986 0 0 0 31916 87 0 0 25 0 1 0 545353618 91369472 12417 4294967295 134512640 134672761 3221224544 3220263792 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22307 12417 603 41 0 22266 0
vsize: 89228
[startup+330.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31132 0 0 0 32915 88 0 0 25 0 1 0 545353618 91672576 12521 4294967295 134512640 134672761 3221224544 3221025168 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22381 12521 603 41 0 22340 0
vsize: 89524
[startup+340.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31148 0 0 0 33915 88 0 0 25 0 1 0 545353618 91807744 12537 4294967295 134512640 134672761 3221224544 3220315072 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22414 12537 603 41 0 22373 0
vsize: 89656
[startup+350.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31148 0 0 0 34915 89 0 0 25 0 1 0 545353618 91807744 12537 4294967295 134512640 134672761 3221224544 3218962720 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22414 12537 603 41 0 22373 0
vsize: 89656
[startup+360.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31526 0 0 0 35914 90 0 0 25 0 1 0 545353618 92684288 12832 4294967295 134512640 134672761 3221224544 3221209968 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22628 12832 603 41 0 22587 0
vsize: 90512
[startup+370.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31821 0 0 0 36913 91 0 0 25 0 1 0 545353618 92782592 12920 4294967295 134512640 134672761 3221224544 3220577712 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22652 12920 603 41 0 22611 0
vsize: 90608
[startup+380.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31869 0 0 0 37913 92 0 0 25 0 1 0 545353618 92917760 12968 4294967295 134512640 134672761 3221224544 3221159856 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22685 12968 603 41 0 22644 0
vsize: 90740
[startup+390.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31874 0 0 0 38913 92 0 0 25 0 1 0 545353618 92917760 12973 4294967295 134512640 134672761 3221224544 3220100800 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22685 12973 603 41 0 22644 0
vsize: 90740
[startup+400.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 31874 0 0 0 39913 92 0 0 25 0 1 0 545353618 92917760 12973 4294967295 134512640 134672761 3221224544 3218632864 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22685 12973 603 41 0 22644 0
vsize: 90740
[startup+410.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 34896 0 0 0 40906 99 0 0 25 0 1 0 545353618 99196928 14594 4294967295 134512640 134672761 3221224544 3221203920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24218 14594 603 41 0 24177 0
vsize: 96872
[startup+420.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 35231 0 0 0 41906 99 0 0 25 0 1 0 545353618 99483648 14722 4294967295 134512640 134672761 3221224544 3220461840 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24288 14722 603 41 0 24247 0
vsize: 97152
[startup+430.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 35280 0 0 0 42906 99 0 0 25 0 1 0 545353618 99618816 14771 4294967295 134512640 134672761 3221224544 3221049360 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24321 14771 603 41 0 24280 0
vsize: 97284
[startup+440.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 35294 0 0 0 43906 99 0 0 25 0 1 0 545353618 99618816 14785 4294967295 134512640 134672761 3221224544 3220170880 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24321 14785 603 41 0 24280 0
vsize: 97284
[startup+450.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 35294 0 0 0 44907 99 0 0 25 0 1 0 545353618 99618816 14785 4294967295 134512640 134672761 3221224544 3219324256 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24321 14785 603 41 0 24280 0
vsize: 97284
[startup+460.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 35636 0 0 0 45906 100 0 0 25 0 1 0 545353618 100360192 15044 4294967295 134512640 134672761 3221224544 3220582128 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24502 15044 603 41 0 24461 0
vsize: 98008
[startup+470.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36010 0 0 0 46905 101 0 0 25 0 1 0 545353618 100945920 15253 4294967295 134512640 134672761 3221224544 3219363312 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24645 15253 603 41 0 24604 0
vsize: 98580
[startup+480.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36160 0 0 0 47904 102 0 0 25 0 1 0 545353618 101384192 15361 4294967295 134512640 134672761 3221224544 3220184880 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24752 15361 603 41 0 24711 0
vsize: 99008
[startup+490.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36201 0 0 0 48905 102 0 0 25 0 1 0 545353618 101384192 15402 4294967295 134512640 134672761 3221224544 3220683792 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24752 15402 603 41 0 24711 0
vsize: 99008
[startup+500.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36234 0 0 0 49905 102 0 0 25 0 1 0 545353618 101519360 15435 4294967295 134512640 134672761 3221224544 3221087472 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15435 603 41 0 24744 0
vsize: 99140
[startup+510.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36246 0 0 0 50905 102 0 0 25 0 1 0 545353618 101519360 15447 4294967295 134512640 134672761 3221224544 3219724960 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+520.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36246 0 0 0 51905 102 0 0 25 0 1 0 545353618 101519360 15447 4294967295 134512640 134672761 3221224544 3219311296 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+530.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36246 0 0 0 52905 102 0 0 25 0 1 0 545353618 101519360 15447 4294967295 134512640 134672761 3221224544 3218448352 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+540.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36578 0 0 0 53905 103 0 0 25 0 1 0 545353618 102260736 15696 4294967295 134512640 134672761 3221224544 3219845520 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24966 15696 603 41 0 24925 0
vsize: 99864
[startup+550.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36713 0 0 0 54905 103 0 0 25 0 1 0 545353618 102666240 15831 4294967295 134512640 134672761 3221224544 3221005680 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25065 15831 603 41 0 25024 0
vsize: 100260
[startup+560.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 36965 0 0 0 55905 103 0 0 25 0 1 0 545353618 102862848 15918 4294967295 134512640 134672761 3221224544 3219485616 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25113 15918 603 41 0 25072 0
vsize: 100452
[startup+570.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37104 0 0 0 56904 104 0 0 25 0 1 0 545353618 103165952 16015 4294967295 134512640 134672761 3221224544 3220166736 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25187 16015 603 41 0 25146 0
vsize: 100748
[startup+580.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37142 0 0 0 57904 104 0 0 25 0 1 0 545353618 103165952 16053 4294967295 134512640 134672761 3221224544 3220641552 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25187 16053 603 41 0 25146 0
vsize: 100748
[startup+590.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37174 0 0 0 58904 104 0 0 25 0 1 0 545353618 103301120 16085 4294967295 134512640 134672761 3221224544 3221030064 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16085 603 41 0 25179 0
vsize: 100880
[startup+600.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37190 0 0 0 59905 104 0 0 25 0 1 0 545353618 103301120 16101 4294967295 134512640 134672761 3221224544 3219686080 134594103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+610.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1162
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37190 0 0 0 60905 104 0 0 25 0 1 0 545353618 103301120 16101 4294967295 134512640 134672761 3221224544 3219329248 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+620.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37190 0 0 0 61905 104 0 0 25 0 1 0 545353618 103301120 16101 4294967295 134512640 134672761 3221224544 3218839360 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+630.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37190 0 0 0 62905 104 0 0 25 0 1 0 545353618 103301120 16101 4294967295 134512640 134672761 3221224544 3217745536 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+640.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37579 0 0 0 63904 105 0 0 25 0 1 0 545353618 104312832 16407 4294967295 134512640 134672761 3221224544 3220400880 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25467 16407 603 41 0 25426 0
vsize: 101868
[startup+650.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37678 0 0 0 64904 105 0 0 25 0 1 0 545353618 103907328 16341 4294967295 134512640 134672761 3221224544 3217999536 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25368 16341 603 41 0 25327 0
vsize: 101472
[startup+660.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 37953 0 0 0 65904 105 0 0 25 0 1 0 545353618 104579072 16574 4294967295 134512640 134672761 3221224544 3219872976 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25532 16574 603 41 0 25491 0
vsize: 102128
[startup+670.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38001 0 0 0 66904 106 0 0 25 0 1 0 545353618 104714240 16622 4294967295 134512640 134672761 3221224544 3220452528 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16622 603 41 0 25524 0
vsize: 102260
[startup+680.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38037 0 0 0 67904 106 0 0 25 0 1 0 545353618 104849408 16658 4294967295 134512640 134672761 3221224544 3220894896 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16658 603 41 0 25557 0
vsize: 102392
[startup+690.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38064 0 0 0 68904 106 0 0 25 0 1 0 545353618 104849408 16685 4294967295 134512640 134672761 3221224544 3220385728 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+700.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38064 0 0 0 69904 106 0 0 25 0 1 0 545353618 104849408 16685 4294967295 134512640 134672761 3221224544 3219529024 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+710.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38064 0 0 0 70904 106 0 0 25 0 1 0 545353618 104849408 16685 4294967295 134512640 134672761 3221224544 3219028960 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+720.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38064 0 0 0 71905 106 0 0 25 0 1 0 545353618 104849408 16685 4294967295 134512640 134672761 3221224544 3217859008 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+730.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38456 0 0 0 72904 106 0 0 25 0 1 0 545353618 105725952 16994 4294967295 134512640 134672761 3221224544 3220560432 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25812 16994 603 41 0 25771 0
vsize: 103248
[startup+740.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38660 0 0 0 73904 107 0 0 25 0 1 0 545353618 105762816 17033 4294967295 134512640 134672761 3221224544 3218936304 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25821 17033 603 41 0 25780 0
vsize: 103284
[startup+750.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38820 0 0 0 74904 108 0 0 25 0 1 0 545353618 106065920 17151 4294967295 134512640 134672761 3221224544 3220038768 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25895 17151 603 41 0 25854 0
vsize: 103580
[startup+760.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38863 0 0 0 75904 108 0 0 25 0 1 0 545353618 106201088 17194 4294967295 134512640 134672761 3221224544 3220570608 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17194 603 41 0 25887 0
vsize: 103712
[startup+770.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38898 0 0 0 76904 108 0 0 25 0 1 0 545353618 106336256 17229 4294967295 134512640 134672761 3221224544 3220992048 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17229 603 41 0 25920 0
vsize: 103844
[startup+780.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38916 0 0 0 77904 108 0 0 25 0 1 0 545353618 106336256 17247 4294967295 134512640 134672761 3221224544 3219811360 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+790.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38916 0 0 0 78904 108 0 0 25 0 1 0 545353618 106336256 17247 4294967295 134512640 134672761 3221224544 3219425152 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+800.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 38916 0 0 0 79904 108 0 0 25 0 1 0 545353618 106336256 17247 4294967295 134512640 134672761 3221224544 3218860288 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+810.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39197 0 0 0 80904 109 0 0 25 0 1 0 545353618 106942464 17445 4294967295 134512640 134672761 3221224544 3219201072 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26109 17445 603 41 0 26068 0
vsize: 104436
[startup+820.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39329 0 0 0 81904 109 0 0 25 0 1 0 545353618 107347968 17577 4294967295 134512640 134672761 3221224544 3220826736 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26208 17577 603 41 0 26167 0
vsize: 104832
[startup+830.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39536 0 0 0 82903 110 0 0 25 0 1 0 545353618 119758848 17619 4294967295 134512640 134672761 3221224544 3219393840 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29238 17619 603 41 0 29197 0
vsize: 116952
[startup+840.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39685 0 0 0 83903 110 0 0 25 0 1 0 545353618 120197120 17726 4294967295 134512640 134672761 3221224544 3220201584 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17726 603 41 0 29304 0
vsize: 117380
[startup+850.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39725 0 0 0 84903 110 0 0 25 0 1 0 545353618 120197120 17766 4294967295 134512640 134672761 3221224544 3220698768 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17766 603 41 0 29304 0
vsize: 117380
[startup+860.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39759 0 0 0 85903 110 0 0 25 0 1 0 545353618 120332288 17800 4294967295 134512640 134672761 3221224544 3221101488 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17800 603 41 0 29337 0
vsize: 117512
[startup+870.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39768 0 0 0 86903 110 0 0 25 0 1 0 545353618 120332288 17809 4294967295 134512640 134672761 3221224544 3219716128 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+880.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39768 0 0 0 87903 111 0 0 25 0 1 0 545353618 120332288 17809 4294967295 134512640 134672761 3221224544 3219293536 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+890.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 39768 0 0 0 88903 111 0 0 25 0 1 0 545353618 120332288 17809 4294967295 134512640 134672761 3221224544 3218358976 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+900.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40111 0 0 0 89903 111 0 0 25 0 1 0 545353618 121208832 18069 4294967295 134512640 134672761 3221224544 3219979248 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29592 18069 603 41 0 29551 0
vsize: 118368
[startup+910.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1164
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40204 0 0 0 90903 111 0 0 25 0 1 0 545353618 121344000 18162 4294967295 134512640 134672761 3221224544 3221104464 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29625 18162 603 41 0 29584 0
vsize: 118500
[startup+920.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40534 0 0 0 91902 112 0 0 25 0 1 0 545353618 121868288 18327 4294967295 134512640 134672761 3221224544 3219120528 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29753 18327 603 41 0 29712 0
vsize: 119012
[startup+930.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40670 0 0 0 92902 112 0 0 25 0 1 0 545353618 122171392 18421 4294967295 134512640 134672761 3221224544 3219748656 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18421 603 41 0 29786 0
vsize: 119308
[startup+940.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40707 0 0 0 93902 113 0 0 25 0 1 0 545353618 122171392 18458 4294967295 134512640 134672761 3221224544 3220208496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18458 603 41 0 29786 0
vsize: 119308
[startup+950.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40738 0 0 0 94902 113 0 0 25 0 1 0 545353618 122306560 18489 4294967295 134512640 134672761 3221224544 3220587696 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18489 603 41 0 29819 0
vsize: 119440
[startup+960.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40764 0 0 0 95902 113 0 0 25 0 1 0 545353618 122306560 18515 4294967295 134512640 134672761 3221224544 3220907952 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18515 603 41 0 29819 0
vsize: 119440
[startup+970.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40787 0 0 0 96902 113 0 0 25 0 1 0 545353618 122441728 18538 4294967295 134512640 134672761 3221224544 3221187600 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18538 603 41 0 29852 0
vsize: 119572
[startup+980.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40790 0 0 0 97902 113 0 0 25 0 1 0 545353618 122441728 18541 4294967295 134512640 134672761 3221224544 3219176512 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+990.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40790 0 0 0 98902 113 0 0 25 0 1 0 545353618 122441728 18541 4294967295 134512640 134672761 3221224544 3218897344 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40790 0 0 0 99903 113 0 0 25 0 1 0 545353618 122441728 18541 4294967295 134512640 134672761 3221224544 3218574400 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40790 0 0 0 100903 113 0 0 25 0 1 0 545353618 122441728 18541 4294967295 134512640 134672761 3221224544 3218124064 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 40790 0 0 0 101903 113 0 0 25 0 1 0 545353618 122441728 18541 4294967295 134512640 134672761 3221224544 3217399840 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 41153 0 0 0 102903 114 0 0 25 0 1 0 545353618 123318272 18821 4294967295 134512640 134672761 3221224544 3219603888 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30107 18821 603 41 0 30066 0
vsize: 120428
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 41245 0 0 0 103903 114 0 0 25 0 1 0 545353618 123453440 18913 4294967295 134512640 134672761 3221224544 3220588752 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30140 18913 603 41 0 30099 0
vsize: 120560
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 41318 0 0 0 104903 114 0 0 25 0 1 0 545353618 123723776 18986 4294967295 134512640 134672761 3221224544 3221176944 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30206 18986 603 41 0 30165 0
vsize: 120824
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 42023 0 0 0 105901 116 0 0 25 0 1 0 545353618 124493824 19358 4294967295 134512640 134672761 3221224544 3220882608 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30394 19358 603 41 0 30353 0
vsize: 121576
[startup+1066.67 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 1166
Raw data (stat): 1158 (minisat+) R 1157 22929 22928 0 -1 0 42023 0 0 0 105901 116 0 0 25 0 1 0 545353618 124493824 19358 4294967295 134512640 134672761 3221224544 3220882608 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30394 19358 603 41 0 30353 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1066.67
CPU time (s): 1066.83
CPU user time (s): 1064.93
CPU system time (s): 1.89871
CPU usage (%): 100.015
Max. virtual memory (Kb): 121576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####