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/miplib2003/normalized-mps-v2-13-7-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	1195.04
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 15347

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 04:03:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17861 boxname=wulflinc6 idbench=1374 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-nw04.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 17861
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        613924 kB
Buffers:         32440 kB
Cached:         365900 kB
SwapCached:          4 kB
Active:         151140 kB
Inactive:       249736 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        613672 kB
SwapTotal:     2097136 kB
SwapFree:      2096768 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5924 kB
Slab:            14132 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:19:44 (client local time) WITH STATUS 0 IN 985.086 SECONDS
stats: 17861 7 985.086 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.86 0.97 0.93 2/54 7344
Raw data (stat): 7344 (runsolver) R 7343 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483827907 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.88 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 22973 0 0 0 937 61 0 0 25 0 1 0 483827907 64581632 7176 4294967295 134512640 134672761 3221224544 3220441156 134592581 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.0053 s]
Raw data (loadavg): 0.90 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 22973 0 0 0 1938 62 0 0 25 0 1 0 483827907 64581632 7176 4294967295 134512640 134672761 3221224544 3220869744 134594229 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.0055 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 23318 0 0 0 2937 63 0 0 25 0 1 0 483827907 65994752 7521 4294967295 134512640 134672761 3221224544 3220833168 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.0066 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 23716 0 0 0 3936 64 0 0 25 0 1 0 483827907 69140480 7919 4294967295 134512640 134672761 3221224544 3220483440 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16880 7919 603 41 0 16839 0
vsize: 67520
[startup+50.0077 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 23947 0 0 0 4935 65 0 0 25 0 1 0 483827907 69771264 8150 4294967295 134512640 134672761 3221224544 3220288096 134594101 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.0079 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 24694 0 0 0 5934 67 0 0 25 0 1 0 483827907 71118848 8567 4294967295 134512640 134672761 3221224544 3221085952 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8567 603 41 0 17322 0
vsize: 69452
[startup+70.008 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 24812 0 0 0 6934 68 0 0 25 0 1 0 483827907 71118848 8685 4294967295 134512640 134672761 3221224544 3220261872 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8685 603 41 0 17322 0
vsize: 69452
[startup+80.0092 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 24959 0 0 0 7933 68 0 0 25 0 1 0 483827907 71458816 8832 4294967295 134512640 134672761 3221224544 3220823280 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17446 8832 603 41 0 17405 0
vsize: 69784
[startup+90.0098 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 25087 0 0 0 8933 69 0 0 25 0 1 0 483827907 74571776 8877 4294967295 134512640 134672761 3221224544 3219894304 134594086 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.01 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 25480 0 0 0 9931 71 0 0 25 0 1 0 483827907 75153408 9145 4294967295 134512640 134672761 3221224544 3220547488 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18348 9145 603 41 0 18307 0
vsize: 73392
[startup+110.014 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 27400 0 0 0 10927 76 0 0 25 0 1 0 483827907 82214912 10940 4294967295 134512640 134672761 3221224544 3219594880 134523741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20072 10940 603 41 0 20031 0
vsize: 80288
[startup+120.015 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 7344
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 27565 0 0 0 11927 76 0 0 25 0 1 0 483827907 79818752 10404 4294967295 134512640 134672761 3221224544 3220791696 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19487 10404 603 41 0 19446 0
vsize: 77948
[startup+130.015 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 27601 0 0 0 12927 76 0 0 25 0 1 0 483827907 79953920 10440 4294967295 134512640 134672761 3221224544 3220356064 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19520 10440 603 41 0 19479 0
vsize: 78080
[startup+140.015 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 27601 0 0 0 13927 76 0 0 25 0 1 0 483827907 79953920 10440 4294967295 134512640 134672761 3221224544 3219102496 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19520 10440 603 41 0 19479 0
vsize: 78080
[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 28017 0 0 0 14927 77 0 0 25 0 1 0 483827907 81100800 10773 4294967295 134512640 134672761 3221224544 3220839504 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19800 10773 603 41 0 19759 0
vsize: 79200
[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 28256 0 0 0 15927 78 0 0 25 0 1 0 483827907 81002496 10847 4294967295 134512640 134672761 3221224544 3220618320 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19776 10847 603 41 0 19735 0
vsize: 79104
[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 28389 0 0 0 16927 78 0 0 25 0 1 0 483827907 81305600 10938 4294967295 134512640 134672761 3221224544 3220608160 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19850 10938 603 41 0 19809 0
vsize: 79400
[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 28455 0 0 0 17927 78 0 0 25 0 1 0 483827907 81575936 11004 4294967295 134512640 134672761 3221224544 3219616048 134523140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19916 11004 603 41 0 19875 0
vsize: 79664
[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 28910 0 0 0 18926 79 0 0 25 0 1 0 483827907 82001920 11211 4294967295 134512640 134672761 3221224544 3220499952 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20020 11211 603 41 0 19979 0
vsize: 80080
[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 29050 0 0 0 19926 79 0 0 25 0 1 0 483827907 82305024 11309 4294967295 134512640 134672761 3221224544 3220725664 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20094 11309 603 41 0 20053 0
vsize: 80376
[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 29384 0 0 0 20926 80 0 0 25 0 1 0 483827907 83046400 11560 4294967295 134512640 134672761 3221224544 3221196816 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20275 11560 603 41 0 20234 0
vsize: 81100
[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 29686 0 0 0 21926 81 0 0 25 0 1 0 483827907 83193856 11655 4294967295 134512640 134672761 3221224544 3220811856 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20311 11655 603 41 0 20270 0
vsize: 81244
[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 29721 0 0 0 22926 81 0 0 25 0 1 0 483827907 83329024 11690 4294967295 134512640 134672761 3221224544 3220398496 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20344 11690 603 41 0 20303 0
vsize: 81376
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 29802 0 0 0 23926 81 0 0 25 0 1 0 483827907 83464192 11771 4294967295 134512640 134672761 3221224544 3219691248 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20377 11771 603 41 0 20336 0
vsize: 81508
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 30246 0 0 0 24925 83 0 0 25 0 1 0 483827907 90275840 11967 4294967295 134512640 134672761 3221224544 3219907536 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22040 11967 603 41 0 21999 0
vsize: 88160
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 30414 0 0 0 25925 83 0 0 25 0 1 0 483827907 90578944 12093 4294967295 134512640 134672761 3221224544 3221014128 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22114 12093 603 41 0 22073 0
vsize: 88456
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 30431 0 0 0 26925 83 0 0 25 0 1 0 483827907 90714112 12110 4294967295 134512640 134672761 3221224544 3220151104 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22147 12110 603 41 0 22106 0
vsize: 88588
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 30719 0 0 0 27925 84 0 0 25 0 1 0 483827907 91320320 12315 4294967295 134512640 134672761 3221224544 3220153680 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22295 12315 603 41 0 22254 0
vsize: 89180
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 30967 0 0 0 28925 85 0 0 25 0 1 0 483827907 91369472 12398 4294967295 134512640 134672761 3221224544 3220035888 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22307 12398 603 41 0 22266 0
vsize: 89228
[startup+300.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 31134 0 0 0 29925 85 0 0 25 0 1 0 483827907 91807744 12523 4294967295 134512640 134672761 3221224544 3221049840 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22414 12523 603 41 0 22373 0
vsize: 89656
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 31148 0 0 0 30925 85 0 0 25 0 1 0 483827907 91807744 12537 4294967295 134512640 134672761 3221224544 3220110688 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22414 12537 603 41 0 22373 0
vsize: 89656
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 31434 0 0 0 31925 86 0 0 25 0 1 0 483827907 92413952 12740 4294967295 134512640 134672761 3221224544 3220089648 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22562 12740 603 41 0 22521 0
vsize: 90248
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 31683 0 0 0 32925 86 0 0 25 0 1 0 483827907 92479488 12824 4294967295 134512640 134672761 3221224544 3219876336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22578 12824 603 41 0 22537 0
vsize: 90312
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 31850 0 0 0 33925 87 0 0 25 0 1 0 483827907 92782592 12949 4294967295 134512640 134672761 3221224544 3220935792 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22652 12949 603 41 0 22611 0
vsize: 90608
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 31874 0 0 0 34925 87 0 0 25 0 1 0 483827907 92917760 12973 4294967295 134512640 134672761 3221224544 3220234816 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+360.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 31874 0 0 0 35925 87 0 0 25 0 1 0 483827907 92917760 12973 4294967295 134512640 134672761 3221224544 3218690272 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+370.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 34891 0 0 0 36919 93 0 0 25 0 1 0 483827907 99196928 14589 4294967295 134512640 134672761 3221224544 3221141712 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24218 14589 603 41 0 24177 0
vsize: 96872
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 35232 0 0 0 37919 94 0 0 25 0 1 0 483827907 99483648 14723 4294967295 134512640 134672761 3221224544 3220479888 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24288 14723 603 41 0 24247 0
vsize: 97152
[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 35289 0 0 0 38919 94 0 0 25 0 1 0 483827907 99618816 14780 4294967295 134512640 134672761 3221224544 3221175984 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24321 14780 603 41 0 24280 0
vsize: 97284
[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 35294 0 0 0 39920 94 0 0 25 0 1 0 483827907 99618816 14785 4294967295 134512640 134672761 3221224544 3219875872 134594092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24321 14785 603 41 0 24280 0
vsize: 97284
[startup+410.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 35564 0 0 0 40929 95 0 0 25 0 1 0 483827907 100225024 14972 4294967295 134512640 134672761 3221224544 3219706320 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24469 14972 603 41 0 24428 0
vsize: 97876
[startup+420.139 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 35920 0 0 0 41930 95 0 0 25 0 1 0 483827907 100773888 15163 4294967295 134512640 134672761 3221224544 3218539152 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24603 15163 603 41 0 24562 0
vsize: 98412
[startup+430.152 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36147 0 0 0 42931 96 0 0 25 0 1 0 483827907 101249024 15348 4294967295 134512640 134672761 3221224544 3220025904 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24719 15348 603 41 0 24678 0
vsize: 98876
[startup+440.152 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36200 0 0 0 43931 96 0 0 25 0 1 0 483827907 101384192 15401 4294967295 134512640 134672761 3221224544 3220671024 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24752 15401 603 41 0 24711 0
vsize: 99008
[startup+450.153 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36238 0 0 0 44932 96 0 0 25 0 1 0 483827907 101519360 15439 4294967295 134512640 134672761 3221224544 3221127024 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15439 603 41 0 24744 0
vsize: 99140
[startup+460.153 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36246 0 0 0 45932 96 0 0 25 0 1 0 483827907 101519360 15447 4294967295 134512640 134672761 3221224544 3219661600 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+470.176 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36246 0 0 0 46935 96 0 0 25 0 1 0 483827907 101519360 15447 4294967295 134512640 134672761 3221224544 3219154912 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+480.208 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36246 0 0 0 47938 96 0 0 25 0 1 0 483827907 101519360 15447 4294967295 134512640 134672761 3221224544 3218041696 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+490.208 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36633 0 0 0 48938 97 0 0 25 0 1 0 483827907 102531072 15751 4294967295 134512640 134672761 3221224544 3220360272 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25032 15751 603 41 0 24991 0
vsize: 100128
[startup+500.443 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 36797 0 0 0 49961 98 0 0 25 0 1 0 483827907 102260736 15750 4294967295 134512640 134672761 3221224544 3217908240 134594226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24966 15750 603 41 0 24925 0
vsize: 99864
[startup+510.443 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37075 0 0 0 50961 98 0 0 25 0 1 0 483827907 103030784 15986 4294967295 134512640 134672761 3221224544 3219818256 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25154 15986 603 41 0 25113 0
vsize: 100616
[startup+520.458 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37131 0 0 0 51963 98 0 0 25 0 1 0 483827907 103165952 16042 4294967295 134512640 134672761 3221224544 3220487184 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25187 16042 603 41 0 25146 0
vsize: 100748
[startup+530.46 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37169 0 0 0 52963 98 0 0 25 0 1 0 483827907 103301120 16080 4294967295 134512640 134672761 3221224544 3220956240 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16080 603 41 0 25179 0
vsize: 100880
[startup+540.489 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37190 0 0 0 53966 98 0 0 25 0 1 0 483827907 103301120 16101 4294967295 134512640 134672761 3221224544 3219950368 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+550.489 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37190 0 0 0 54967 98 0 0 25 0 1 0 483827907 103301120 16101 4294967295 134512640 134672761 3221224544 3219368800 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+560.49 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37190 0 0 0 55967 98 0 0 25 0 1 0 483827907 103301120 16101 4294967295 134512640 134672761 3221224544 3218853088 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+570.49 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37190 0 0 0 56967 98 0 0 25 0 1 0 483827907 103301120 16101 4294967295 134512640 134672761 3221224544 3217745728 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+580.49 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37574 0 0 0 57967 99 0 0 25 0 1 0 483827907 104312832 16402 4294967295 134512640 134672761 3221224544 3220342512 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25467 16402 603 41 0 25426 0
vsize: 101868
[startup+590.493 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37652 0 0 0 58968 99 0 0 25 0 1 0 483827907 104448000 16480 4294967295 134512640 134672761 3221224544 3221184912 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25500 16480 603 41 0 25459 0
vsize: 102000
[startup+600.493 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 37954 0 0 0 59967 100 0 0 25 0 1 0 483827907 104579072 16575 4294967295 134512640 134672761 3221224544 3219882192 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25532 16575 603 41 0 25491 0
vsize: 102128
[startup+610.498 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38011 0 0 0 60968 100 0 0 25 0 1 0 483827907 104714240 16632 4294967295 134512640 134672761 3221224544 3220572912 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16632 603 41 0 25524 0
vsize: 102260
[startup+620.498 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38050 0 0 0 61968 100 0 0 25 0 1 0 483827907 104849408 16671 4294967295 134512640 134672761 3221224544 3221053200 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16671 603 41 0 25557 0
vsize: 102392
[startup+630.499 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38064 0 0 0 62968 100 0 0 25 0 1 0 483827907 104849408 16685 4294967295 134512640 134672761 3221224544 3219732640 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+640.499 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38064 0 0 0 63969 100 0 0 25 0 1 0 483827907 104849408 16685 4294967295 134512640 134672761 3221224544 3219268576 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+650.5 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38064 0 0 0 64969 100 0 0 25 0 1 0 483827907 104849408 16685 4294967295 134512640 134672761 3221224544 3218245696 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+660.5 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38416 0 0 0 65969 101 0 0 25 0 1 0 483827907 105725952 16954 4294967295 134512640 134672761 3221224544 3220082256 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25812 16954 603 41 0 25771 0
vsize: 103248
[startup+670.5 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38500 0 0 0 66969 101 0 0 25 0 1 0 483827907 105861120 17038 4294967295 134512640 134672761 3221224544 3221104752 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25845 17038 603 41 0 25804 0
vsize: 103380
[startup+680.502 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38717 0 0 0 67969 101 0 0 25 0 1 0 483827907 105897984 17090 4294967295 134512640 134672761 3221224544 3219790704 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25854 17090 603 41 0 25813 0
vsize: 103416
[startup+690.501 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38859 0 0 0 68969 102 0 0 25 0 1 0 483827907 106201088 17190 4294967295 134512640 134672761 3221224544 3220517040 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17190 603 41 0 25887 0
vsize: 103712
[startup+700.502 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38900 0 0 0 69969 102 0 0 25 0 1 0 483827907 106336256 17231 4294967295 134512640 134672761 3221224544 3221012016 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17231 603 41 0 25920 0
vsize: 103844
[startup+710.503 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38916 0 0 0 70970 102 0 0 25 0 1 0 483827907 106336256 17247 4294967295 134512640 134672761 3221224544 3219771808 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+720.504 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38916 0 0 0 71970 102 0 0 25 0 1 0 483827907 106336256 17247 4294967295 134512640 134672761 3221224544 3219321568 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+730.508 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 38916 0 0 0 72971 102 0 0 25 0 1 0 483827907 106336256 17247 4294967295 134512640 134672761 3221224544 3218342272 134594092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+740.509 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39256 0 0 0 73970 103 0 0 25 0 1 0 483827907 107077632 17504 4294967295 134512640 134672761 3221224544 3219932016 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26142 17504 603 41 0 26101 0
vsize: 104568
[startup+750.509 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39347 0 0 0 74970 103 0 0 25 0 1 0 483827907 107347968 17595 4294967295 134512640 134672761 3221224544 3221034000 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26208 17595 603 41 0 26167 0
vsize: 104832
[startup+760.51 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39561 0 0 0 75971 103 0 0 25 0 1 0 483827907 119894016 17644 4294967295 134512640 134672761 3221224544 3219710544 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29271 17644 603 41 0 29230 0
vsize: 117084
[startup+770.522 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39708 0 0 0 76971 104 0 0 25 0 1 0 483827907 120197120 17749 4294967295 134512640 134672761 3221224544 3220477872 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17749 603 41 0 29304 0
vsize: 117380
[startup+780.53 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39749 0 0 0 77972 104 0 0 25 0 1 0 483827907 120332288 17790 4294967295 134512640 134672761 3221224544 3220986288 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17790 603 41 0 29337 0
vsize: 117512
[startup+790.53 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39768 0 0 0 78972 104 0 0 25 0 1 0 483827907 120332288 17809 4294967295 134512640 134672761 3221224544 3219802336 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+800.53 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39768 0 0 0 79973 104 0 0 25 0 1 0 483827907 120332288 17809 4294967295 134512640 134672761 3221224544 3219353920 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+810.531 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 39768 0 0 0 80973 104 0 0 25 0 1 0 483827907 120332288 17809 4294967295 134512640 134672761 3221224544 3218390560 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+820.532 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40106 0 0 0 81973 105 0 0 25 0 1 0 483827907 121073664 18064 4294967295 134512640 134672761 3221224544 3219918288 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29559 18064 603 41 0 29518 0
vsize: 118236
[startup+830.532 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40198 0 0 0 82973 105 0 0 25 0 1 0 483827907 121344000 18156 4294967295 134512640 134672761 3221224544 3221033808 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29625 18156 603 41 0 29584 0
vsize: 118500
[startup+840.533 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40531 0 0 0 83973 106 0 0 25 0 1 0 483827907 121733120 18324 4294967295 134512640 134672761 3221224544 3219081936 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29720 18324 603 41 0 29679 0
vsize: 118880
[startup+850.533 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40677 0 0 0 84973 106 0 0 25 0 1 0 483827907 122171392 18428 4294967295 134512640 134672761 3221224544 3219848304 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18428 603 41 0 29786 0
vsize: 119308
[startup+860.533 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40719 0 0 0 85973 106 0 0 25 0 1 0 483827907 122171392 18470 4294967295 134512640 134672761 3221224544 3220356336 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18470 603 41 0 29786 0
vsize: 119308
[startup+870.533 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40750 0 0 0 86973 107 0 0 25 0 1 0 483827907 122306560 18501 4294967295 134512640 134672761 3221224544 3220736880 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18501 603 41 0 29819 0
vsize: 119440
[startup+880.533 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40775 0 0 0 87974 107 0 0 25 0 1 0 483827907 122441728 18526 4294967295 134512640 134672761 3221224544 3221039472 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18526 603 41 0 29852 0
vsize: 119572
[startup+890.534 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40790 0 0 0 88974 107 0 0 25 0 1 0 483827907 122441728 18541 4294967295 134512640 134672761 3221224544 3219969664 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+900.534 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40790 0 0 0 89974 107 0 0 25 0 1 0 483827907 122441728 18541 4294967295 134512640 134672761 3221224544 3219084928 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+910.535 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40790 0 0 0 90975 107 0 0 25 0 1 0 483827907 122441728 18541 4294967295 134512640 134672761 3221224544 3218791840 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+920.535 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40790 0 0 0 91975 107 0 0 25 0 1 0 483827907 122441728 18541 4294967295 134512640 134672761 3221224544 3218443456 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+930.535 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40790 0 0 0 92975 107 0 0 25 0 1 0 483827907 122441728 18541 4294967295 134512640 134672761 3221224544 3217816096 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+940.536 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 40790 0 0 0 93976 107 0 0 25 0 1 0 483827907 122441728 18541 4294967295 134512640 134672761 3221224544 3217235584 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+950.536 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 41177 0 0 0 94975 108 0 0 25 0 1 0 483827907 123318272 18845 4294967295 134512640 134672761 3221224544 3219895440 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30107 18845 603 41 0 30066 0
vsize: 120428
[startup+960.537 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 41265 0 0 0 95976 108 0 0 25 0 1 0 483827907 123588608 18933 4294967295 134512640 134672761 3221224544 3220740528 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30173 18933 603 41 0 30132 0
vsize: 120692
[startup+970.537 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 41451 0 0 0 96976 108 0 0 25 0 1 0 483827907 123387904 18954 4294967295 134512640 134672761 3221224544 3221059056 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30124 18954 603 41 0 30083 0
vsize: 120496
[startup+980.538 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 42947 0 0 0 97972 112 0 0 25 0 1 0 483827907 88866816 17718 4294967295 134512640 134672761 3221224544 3221100364 134542792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21696 17718 603 41 0 21655 0
vsize: 86784
[startup+984.823 s]
Raw data (loadavg): 1.00 0.99 0.93 1/53 7346
Raw data (stat): 7344 (minisat+) R 7343 29653 29652 0 -1 0 42947 0 0 0 97972 112 0 0 25 0 1 0 483827907 88866816 17718 4294967295 134512640 134672761 3221224544 3221100364 134542792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21696 17718 603 41 0 21655 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 984.823
CPU time (s): 985.086
CPU user time (s): 983.284
CPU system time (s): 1.80173
CPU usage (%): 100.027
Max. virtual memory (Kb): 120692
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####