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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-nw04.opb
MD5SUM	5a18ff1f45b144b201f1f80233dc9b6b
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	1197.16
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 21811

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-22 01:02:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12869 boxname=wulflinc30 idbench=990 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-nw04.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 12869
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        748384 kB
Buffers:         11672 kB
Cached:         248416 kB
SwapCached:        352 kB
Active:          39368 kB
Inactive:       223408 kB
HighTotal:      131008 kB
HighFree:        18816 kB
LowTotal:       903652 kB
LowFree:        729568 kB
SwapTotal:     2097892 kB
SwapFree:      2097328 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5980 kB
Slab:            17788 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:20:54 (client local time) WITH STATUS 0 IN 1112.27 SECONDS
stats: 12869 7 1112.27 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): 0.87 0.96 0.91 2/54 1087
Raw data (stat): 1087 (runsolver) R 1086 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549602281 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 22973 0 0 0 935 64 0 0 25 0 1 0 549602281 64581632 7176 4294967295 134512640 134672761 3221224544 3220374768 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+19.9994 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 22973 0 0 0 1934 64 0 0 25 0 1 0 549602281 64581632 7176 4294967295 134512640 134672761 3221224544 3220759920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+29.9994 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 23318 0 0 0 2932 65 0 0 25 0 1 0 549602281 65994752 7521 4294967295 134512640 134672761 3221224544 3220667280 134594217 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.0083 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 23706 0 0 0 3932 66 0 0 25 0 1 0 549602281 69140480 7909 4294967295 134512640 134672761 3221224544 3220517248 134594124 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.0088 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 23947 0 0 0 4931 67 0 0 25 0 1 0 549602281 69771264 8150 4294967295 134512640 134672761 3221224544 3220456480 134594106 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.0086 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 24667 0 0 0 5930 69 0 0 25 0 1 0 549602281 71118848 8540 4294967295 134512640 134672761 3221224544 3220355760 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8540 603 41 0 17322 0
vsize: 69452
[startup+70.0088 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 24761 0 0 0 6930 69 0 0 25 0 1 0 549602281 71118848 8634 4294967295 134512640 134672761 3221224544 3220639360 134594101 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.0092 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 24841 0 0 0 7930 69 0 0 25 0 1 0 549602281 71118848 8714 4294967295 134512640 134672761 3221224544 3220276000 134594101 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.009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 25087 0 0 0 8930 70 0 0 25 0 1 0 549602281 74571776 8877 4294967295 134512640 134672761 3221224544 3220957216 134594131 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.009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 25448 0 0 0 9929 70 0 0 25 0 1 0 549602281 75153408 9113 4294967295 134512640 134672761 3221224544 3220616208 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18348 9113 603 41 0 18307 0
vsize: 73392
[startup+110.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 25611 0 0 0 10929 70 0 0 25 0 1 0 549602281 75456512 9234 4294967295 134512640 134672761 3221224544 3220140144 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18422 9234 603 41 0 18381 0
vsize: 73688
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27436 0 0 0 11925 74 0 0 25 0 1 0 549602281 79650816 10317 4294967295 134512640 134672761 3221224544 3220228656 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19446 10317 603 41 0 19405 0
vsize: 77784
[startup+130.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27580 0 0 0 12925 75 0 0 25 0 1 0 549602281 79953920 10419 4294967295 134512640 134672761 3221224544 3220971600 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19520 10419 603 41 0 19479 0
vsize: 78080
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27601 0 0 0 13925 75 0 0 25 0 1 0 549602281 79953920 10440 4294967295 134512640 134672761 3221224544 3220281856 134594092 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27601 0 0 0 14926 75 0 0 25 0 1 0 549602281 79953920 10440 4294967295 134512640 134672761 3221224544 3219288544 134594086 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27987 0 0 0 15925 75 0 0 25 0 1 0 549602281 80965632 10743 4294967295 134512640 134672761 3221224544 3220599888 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19767 10743 603 41 0 19726 0
vsize: 79068
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28230 0 0 0 16924 76 0 0 25 0 1 0 549602281 81002496 10821 4294967295 134512640 134672761 3221224544 3220302576 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19776 10821 603 41 0 19735 0
vsize: 79104
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28384 0 0 0 17924 77 0 0 25 0 1 0 549602281 81305600 10933 4294967295 134512640 134672761 3221224544 3221161200 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19850 10933 603 41 0 19809 0
vsize: 79400
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28389 0 0 0 18924 77 0 0 25 0 1 0 549602281 81305600 10938 4294967295 134512640 134672761 3221224544 3220110880 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1087
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28708 0 0 0 19924 77 0 0 25 0 1 0 549602281 82046976 11174 4294967295 134512640 134672761 3221224544 3220678896 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20031 11174 603 41 0 19990 0
vsize: 80124
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28935 0 0 0 20923 78 0 0 25 0 1 0 549602281 82001920 11236 4294967295 134512640 134672761 3221224544 3220825680 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20020 11236 603 41 0 19979 0
vsize: 80080
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29050 0 0 0 21923 78 0 0 25 0 1 0 549602281 82305024 11309 4294967295 134512640 134672761 3221224544 3220611328 134594086 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29381 0 0 0 22923 79 0 0 25 0 1 0 549602281 83046400 11557 4294967295 134512640 134672761 3221224544 3221163408 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20275 11557 603 41 0 20234 0
vsize: 81100
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29593 0 0 0 23922 79 0 0 25 0 1 0 549602281 83025920 11604 4294967295 134512640 134672761 3221224544 3220692240 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20270 11604 603 41 0 20229 0
vsize: 81080
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29721 0 0 0 24922 80 0 0 25 0 1 0 549602281 83329024 11690 4294967295 134512640 134672761 3221224544 3220629952 134594124 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29721 0 0 0 25922 80 0 0 25 0 1 0 549602281 83329024 11690 4294967295 134512640 134672761 3221224544 3219735712 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30059 0 0 0 26921 81 0 0 25 0 1 0 549602281 90361856 11945 4294967295 134512640 134672761 3221224544 3220818672 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22061 11945 603 41 0 22020 0
vsize: 88244
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30279 0 0 0 27921 81 0 0 25 0 1 0 549602281 90275840 12000 4294967295 134512640 134672761 3221224544 3220386192 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22040 12000 603 41 0 21999 0
vsize: 88160
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30422 0 0 0 28921 82 0 0 25 0 1 0 549602281 90714112 12101 4294967295 134512640 134672761 3221224544 3221123088 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22147 12101 603 41 0 22106 0
vsize: 88588
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30431 0 0 0 29921 82 0 0 25 0 1 0 549602281 90714112 12110 4294967295 134512640 134672761 3221224544 3220144864 134594086 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30523 0 0 0 30921 82 0 0 25 0 1 0 549602281 90849280 12202 4294967295 134512640 134672761 3221224544 3219768816 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22180 12202 603 41 0 22139 0
vsize: 88720
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30906 0 0 0 31921 82 0 0 25 0 1 0 549602281 91197440 12337 4294967295 134512640 134672761 3221224544 3219553872 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22265 12337 603 41 0 22224 0
vsize: 89060
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31111 0 0 0 32920 83 0 0 25 0 1 0 549602281 91672576 12500 4294967295 134512640 134672761 3221224544 3220776048 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22381 12500 603 41 0 22340 0
vsize: 89524
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31148 0 0 0 33920 83 0 0 25 0 1 0 549602281 91807744 12537 4294967295 134512640 134672761 3221224544 3220518400 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31148 0 0 0 34920 83 0 0 25 0 1 0 549602281 91807744 12537 4294967295 134512640 134672761 3221224544 3219660256 134594089 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31481 0 0 0 35920 84 0 0 25 0 1 0 549602281 92549120 12787 4294967295 134512640 134672761 3221224544 3220671408 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22595 12787 603 41 0 22554 0
vsize: 90380
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31702 0 0 0 36920 84 0 0 25 0 1 0 549602281 92479488 12843 4294967295 134512640 134672761 3221224544 3220136688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22578 12843 603 41 0 22537 0
vsize: 90312
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31852 0 0 0 37919 85 0 0 25 0 1 0 549602281 92782592 12951 4294967295 134512640 134672761 3221224544 3220943184 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22652 12951 603 41 0 22611 0
vsize: 90608
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31874 0 0 0 38919 85 0 0 25 0 1 0 549602281 92917760 12973 4294967295 134512640 134672761 3221224544 3220323232 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22685 12973 603 41 0 22644 0
vsize: 90740
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31874 0 0 0 39920 85 0 0 25 0 1 0 549602281 92917760 12973 4294967295 134512640 134672761 3221224544 3219250240 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22685 12973 603 41 0 22644 0
vsize: 90740
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 34848 0 0 0 40914 91 0 0 25 0 1 0 549602281 99061760 14546 4294967295 134512640 134672761 3221224544 3220621584 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24185 14546 603 41 0 24144 0
vsize: 96740
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35105 0 0 0 41913 92 0 0 25 0 1 0 549602281 99180544 14638 4294967295 134512640 134672761 3221224544 3219935280 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24214 14638 603 41 0 24173 0
vsize: 96856
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35258 0 0 0 42913 92 0 0 25 0 1 0 549602281 99483648 14749 4294967295 134512640 134672761 3221224544 3220787760 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24288 14749 603 41 0 24247 0
vsize: 97152
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35294 0 0 0 43913 92 0 0 25 0 1 0 549602281 99618816 14785 4294967295 134512640 134672761 3221224544 3220398976 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24321 14785 603 41 0 24280 0
vsize: 97284
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35294 0 0 0 44913 92 0 0 25 0 1 0 549602281 99618816 14785 4294967295 134512640 134672761 3221224544 3219785056 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24321 14785 603 41 0 24280 0
vsize: 97284
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35356 0 0 0 45913 92 0 0 25 0 1 0 549602281 99753984 14847 4294967295 134512640 134672761 3221224544 3219172944 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24354 14847 603 41 0 24313 0
vsize: 97416
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35680 0 0 0 46913 93 0 0 25 0 1 0 549602281 100495360 15088 4294967295 134512640 134672761 3221224544 3221118768 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24535 15088 603 41 0 24494 0
vsize: 98140
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36042 0 0 0 47913 93 0 0 25 0 1 0 549602281 101081088 15285 4294967295 134512640 134672761 3221224544 3219748560 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24678 15285 603 41 0 24637 0
vsize: 98712
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36179 0 0 0 48913 93 0 0 25 0 1 0 549602281 101384192 15380 4294967295 134512640 134672761 3221224544 3220407216 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24752 15380 603 41 0 24711 0
vsize: 99008
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36217 0 0 0 49913 94 0 0 25 0 1 0 549602281 101519360 15418 4294967295 134512640 134672761 3221224544 3220870512 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24785 15418 603 41 0 24744 0
vsize: 99140
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 50913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3220685728 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 51913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3219577600 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 52913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3219129088 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 53913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3218250976 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36575 0 0 0 54913 95 0 0 25 0 1 0 549602281 102260736 15693 4294967295 134512640 134672761 3221224544 3219805968 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24966 15693 603 41 0 24925 0
vsize: 99864
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36701 0 0 0 55913 95 0 0 25 0 1 0 549602281 102666240 15819 4294967295 134512640 134672761 3221224544 3220909776 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25065 15819 603 41 0 25024 0
vsize: 100260
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36948 0 0 0 56913 95 0 0 25 0 1 0 549602281 102727680 15901 4294967295 134512640 134672761 3221224544 3219275952 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25080 15901 603 41 0 25039 0
vsize: 100320
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37096 0 0 0 57912 95 0 0 25 0 1 0 549602281 103165952 16007 4294967295 134512640 134672761 3221224544 3220080144 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25187 16007 603 41 0 25146 0
vsize: 100748
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37139 0 0 0 58912 95 0 0 25 0 1 0 549602281 103165952 16050 4294967295 134512640 134672761 3221224544 3220592208 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25187 16050 603 41 0 25146 0
vsize: 100748
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37171 0 0 0 59912 95 0 0 25 0 1 0 549602281 103301120 16082 4294967295 134512640 134672761 3221224544 3220987440 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25220 16082 603 41 0 25179 0
vsize: 100880
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 60912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3219963520 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 61912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3219411232 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 62912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3218997664 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 63912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3218196640 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+650.012 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37489 0 0 0 64912 97 0 0 25 0 1 0 549602281 104042496 16317 4294967295 134512640 134672761 3221224544 3219298608 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25401 16317 603 41 0 25360 0
vsize: 101604
[startup+660.011 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37597 0 0 0 65911 97 0 0 25 0 1 0 549602281 104312832 16425 4294967295 134512640 134672761 3221224544 3220609776 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25467 16425 603 41 0 25426 0
vsize: 101868
[startup+670.011 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37748 0 0 0 66911 97 0 0 25 0 1 0 549602281 104103936 16411 4294967295 134512640 134672761 3221224544 3218650128 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25416 16411 603 41 0 25375 0
vsize: 101664
[startup+680.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37958 0 0 0 67911 98 0 0 25 0 1 0 549602281 104579072 16579 4294967295 134512640 134672761 3221224544 3219939504 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25532 16579 603 41 0 25491 0
vsize: 102128
[startup+690.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38008 0 0 0 68911 98 0 0 25 0 1 0 549602281 104714240 16629 4294967295 134512640 134672761 3221224544 3220531632 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25565 16629 603 41 0 25524 0
vsize: 102260
[startup+700.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38043 0 0 0 69911 98 0 0 25 0 1 0 549602281 104849408 16664 4294967295 134512640 134672761 3221224544 3220965168 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16664 603 41 0 25557 0
vsize: 102392
[startup+710.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 70911 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3219962176 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+720.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 71911 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3219479200 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+730.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 72912 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3219001792 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+740.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 73912 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3218078464 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+750.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38421 0 0 0 74911 99 0 0 25 0 1 0 549602281 105725952 16959 4294967295 134512640 134672761 3221224544 3220130928 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25812 16959 603 41 0 25771 0
vsize: 103248
[startup+760.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38497 0 0 0 75911 99 0 0 25 0 1 0 549602281 105861120 17035 4294967295 134512640 134672761 3221224544 3221070288 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25845 17035 603 41 0 25804 0
vsize: 103380
[startup+770.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38704 0 0 0 76911 99 0 0 25 0 1 0 549602281 105762816 17077 4294967295 134512640 134672761 3221224544 3219643248 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25821 17077 603 41 0 25780 0
vsize: 103284
[startup+780.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38844 0 0 0 77911 100 0 0 25 0 1 0 549602281 106201088 17175 4294967295 134512640 134672761 3221224544 3220341264 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25928 17175 603 41 0 25887 0
vsize: 103712
[startup+790.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38884 0 0 0 78911 100 0 0 25 0 1 0 549602281 106201088 17215 4294967295 134512640 134672761 3221224544 3220819536 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25928 17215 603 41 0 25887 0
vsize: 103712
[startup+800.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38915 0 0 0 79911 100 0 0 25 0 1 0 549602281 106336256 17246 4294967295 134512640 134672761 3221224544 3221196816 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17246 603 41 0 25920 0
vsize: 103844
[startup+810.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38916 0 0 0 80911 100 0 0 25 0 1 0 549602281 106336256 17247 4294967295 134512640 134672761 3221224544 3219623872 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+820.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38916 0 0 0 81911 100 0 0 25 0 1 0 549602281 106336256 17247 4294967295 134512640 134672761 3221224544 3219192736 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+830.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38916 0 0 0 82912 100 0 0 25 0 1 0 549602281 106336256 17247 4294967295 134512640 134672761 3221224544 3218356000 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+840.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39224 0 0 0 83911 101 0 0 25 0 1 0 549602281 107077632 17472 4294967295 134512640 134672761 3221224544 3219541488 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26142 17472 603 41 0 26101 0
vsize: 104568
[startup+850.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39326 0 0 0 84911 101 0 0 25 0 1 0 549602281 107347968 17574 4294967295 134512640 134672761 3221224544 3220784016 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26208 17574 603 41 0 26167 0
vsize: 104832
[startup+860.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39521 0 0 0 85911 102 0 0 25 0 1 0 549602281 119758848 17604 4294967295 134512640 134672761 3221224544 3219205680 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29238 17604 603 41 0 29197 0
vsize: 116952
[startup+870.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39679 0 0 0 86910 102 0 0 25 0 1 0 549602281 120061952 17720 4294967295 134512640 134672761 3221224544 3220132464 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29312 17720 603 41 0 29271 0
vsize: 117248
[startup+880.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39724 0 0 0 87911 102 0 0 25 0 1 0 549602281 120197120 17765 4294967295 134512640 134672761 3221224544 3220669680 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29345 17765 603 41 0 29304 0
vsize: 117380
[startup+890.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39757 0 0 0 88911 102 0 0 25 0 1 0 549602281 120332288 17798 4294967295 134512640 134672761 3221224544 3221077488 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17798 603 41 0 29337 0
vsize: 117512
[startup+900.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39768 0 0 0 89911 102 0 0 25 0 1 0 549602281 120332288 17809 4294967295 134512640 134672761 3221224544 3219756064 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+910.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39768 0 0 0 90911 102 0 0 25 0 1 0 549602281 120332288 17809 4294967295 134512640 134672761 3221224544 3219354688 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+920.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39768 0 0 0 91911 102 0 0 25 0 1 0 549602281 120332288 17809 4294967295 134512640 134672761 3221224544 3218794528 134594092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+930.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39986 0 0 0 92911 103 0 0 25 0 1 0 549602281 120803328 17944 4294967295 134512640 134672761 3221224544 3218462832 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29493 17944 603 41 0 29452 0
vsize: 117972
[startup+940.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40156 0 0 0 93911 103 0 0 25 0 1 0 549602281 121208832 18114 4294967295 134512640 134672761 3221224544 3220531536 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29592 18114 603 41 0 29551 0
vsize: 118368
[startup+950.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40422 0 0 0 94911 103 0 0 25 0 1 0 549602281 121425920 18215 4294967295 134512640 134672761 3221224544 3218018160 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29645 18215 603 41 0 29604 0
vsize: 118580
[startup+960.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40633 0 0 0 95910 104 0 0 25 0 1 0 549602281 122036224 18384 4294967295 134512640 134672761 3221224544 3219319920 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29794 18384 603 41 0 29753 0
vsize: 119176
[startup+970.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40683 0 0 0 96911 104 0 0 25 0 1 0 549602281 122171392 18434 4294967295 134512640 134672761 3221224544 3219913488 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29827 18434 603 41 0 29786 0
vsize: 119308
[startup+980.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40718 0 0 0 97910 104 0 0 25 0 1 0 549602281 122171392 18469 4294967295 134512640 134672761 3221224544 3220347504 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29827 18469 603 41 0 29786 0
vsize: 119308
[startup+990.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40748 0 0 0 98911 104 0 0 25 0 1 0 549602281 122306560 18499 4294967295 134512640 134672761 3221224544 3220699728 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29860 18499 603 41 0 29819 0
vsize: 119440
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40772 0 0 0 99911 104 0 0 25 0 1 0 549602281 122306560 18523 4294967295 134512640 134672761 3221224544 3220997328 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29860 18523 603 41 0 29819 0
vsize: 119440
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 100911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3220339168 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 101911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3219153088 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 102911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3218874208 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 103911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3218554048 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 104911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3218134144 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 105912 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3217521088 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41105 0 0 0 106911 105 0 0 25 0 1 0 549602281 123183104 18773 4294967295 134512640 134672761 3221224544 3219012816 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30074 18773 603 41 0 30033 0
vsize: 120296
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41204 0 0 0 107911 105 0 0 25 0 1 0 549602281 123453440 18872 4294967295 134512640 134672761 3221224544 3220217904 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30140 18872 603 41 0 30099 0
vsize: 120560
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41282 0 0 0 108911 105 0 0 25 0 1 0 549602281 123588608 18950 4294967295 134512640 134672761 3221224544 3220888176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30173 18950 603 41 0 30132 0
vsize: 120692
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41623 0 0 0 109910 107 0 0 25 0 1 0 549602281 123748352 19084 4294967295 134512640 134672761 3221224544 3221192128 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30212 19084 603 41 0 30171 0
vsize: 120848
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 56067 0 0 0 110878 139 0 0 25 0 1 0 549602281 146100224 30838 4294967295 134512640 134672761 3221224544 3216366976 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35669 30840 603 41 0 35628 0
vsize: 142676
[startup+1112.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 1089
Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 56067 0 0 0 110878 139 0 0 25 0 1 0 549602281 146100224 30838 4294967295 134512640 134672761 3221224544 3216366976 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35669 30840 603 41 0 35628 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1112.11
CPU time (s): 1112.27
CPU user time (s): 1110.46
CPU system time (s): 1.80472
CPU usage (%): 100.014
Max. virtual memory (Kb): 142676
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####