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 16610

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 08:03:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12870 boxname=wulflinc25 idbench=990 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-nw04.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 12870
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        587156 kB
Buffers:         11836 kB
Cached:         415084 kB
SwapCached:        732 kB
Active:          53156 kB
Inactive:       375696 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        586904 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            13056 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 08:21:13 (client local time) WITH STATUS 0 IN 1087.58 SECONDS
stats: 12870 7 1087.58 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.88 1.00 0.94 2/54 32133
Raw data (stat): 32133 (runsolver) R 32132 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543499264 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.90 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 22973 0 0 0 931 68 0 0 25 0 1 0 543499264 64581632 7176 4294967295 134512640 134672761 3221224544 3220462320 134594259 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.0009 s]
Raw data (loadavg): 0.91 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 22973 0 0 0 1931 68 0 0 25 0 1 0 543499264 64581632 7176 4294967295 134512640 134672761 3221224544 3220879056 134594212 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.0002 s]
Raw data (loadavg): 0.93 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 23318 0 0 0 2930 69 0 0 25 0 1 0 543499264 65994752 7521 4294967295 134512640 134672761 3221224544 3220826256 134594229 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.0011 s]
Raw data (loadavg): 0.94 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 23706 0 0 0 3929 70 0 0 25 0 1 0 543499264 69140480 7909 4294967295 134512640 134672761 3221224544 3220220128 134594131 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.0017 s]
Raw data (loadavg): 0.95 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 23947 0 0 0 4929 71 0 0 25 0 1 0 543499264 69771264 8150 4294967295 134512640 134672761 3221224544 3220396096 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.002 s]
Raw data (loadavg): 0.95 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 24686 0 0 0 5927 72 0 0 25 0 1 0 543499264 71118848 8559 4294967295 134512640 134672761 3221224544 3220984080 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8559 603 41 0 17322 0
vsize: 69452
[startup+70.0023 s]
Raw data (loadavg): 0.96 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 24785 0 0 0 6927 73 0 0 25 0 1 0 543499264 71118848 8658 4294967295 134512640 134672761 3221224544 3220915056 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8658 603 41 0 17322 0
vsize: 69452
[startup+80.0026 s]
Raw data (loadavg): 0.97 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 24841 0 0 0 7926 73 0 0 25 0 1 0 543499264 71118848 8714 4294967295 134512640 134672761 3221224544 3219834784 134594124 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.0028 s]
Raw data (loadavg): 0.97 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 25087 0 0 0 8926 74 0 0 25 0 1 0 543499264 74571776 8877 4294967295 134512640 134672761 3221224544 3220483456 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.006 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 25458 0 0 0 9926 75 0 0 25 0 1 0 543499264 75186176 9123 4294967295 134512640 134672761 3221224544 3220955568 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18356 9123 603 41 0 18315 0
vsize: 73424
[startup+110.012 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 25680 0 0 0 10926 75 0 0 25 0 1 0 543499264 75624448 9303 4294967295 134512640 134672761 3221224544 3220970736 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18463 9303 603 41 0 18422 0
vsize: 73852
[startup+120.012 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 27454 0 0 0 11922 79 0 0 25 0 1 0 543499264 79683584 10335 4294967295 134512640 134672761 3221224544 3220442640 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19454 10335 603 41 0 19413 0
vsize: 77816
[startup+130.012 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 27593 0 0 0 12922 80 0 0 25 0 1 0 543499264 79986688 10432 4294967295 134512640 134672761 3221224544 3221128464 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10432 603 41 0 19487 0
vsize: 78112
[startup+140.012 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 27601 0 0 0 13922 80 0 0 25 0 1 0 543499264 79986688 10440 4294967295 134512640 134672761 3221224544 3220072576 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+150.012 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 32133
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 27601 0 0 0 14922 80 0 0 25 0 1 0 543499264 79986688 10440 4294967295 134512640 134672761 3221224544 3218572192 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+160.013 s]
Raw data (loadavg): 1.20 1.05 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 28052 0 0 0 15921 81 0 0 25 0 1 0 543499264 81133568 10808 4294967295 134512640 134672761 3221224544 3221122800 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19808 10808 603 41 0 19767 0
vsize: 79232
[startup+170.014 s]
Raw data (loadavg): 1.17 1.04 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 28267 0 0 0 16921 81 0 0 25 0 1 0 543499264 81145856 10858 4294967295 134512640 134672761 3221224544 3220756752 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19811 10858 603 41 0 19770 0
vsize: 79244
[startup+180.013 s]
Raw data (loadavg): 1.14 1.04 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 28389 0 0 0 17920 82 0 0 25 0 1 0 543499264 81313792 10938 4294967295 134512640 134672761 3221224544 3220584064 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+190.014 s]
Raw data (loadavg): 1.12 1.04 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 28389 0 0 0 18920 82 0 0 25 0 1 0 543499264 81313792 10938 4294967295 134512640 134672761 3221224544 3218892928 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+200.014 s]
Raw data (loadavg): 1.10 1.04 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 28846 0 0 0 19919 84 0 0 25 0 1 0 543499264 81866752 11147 4294967295 134512640 134672761 3221224544 3220016784 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19987 11147 603 41 0 19946 0
vsize: 79948
[startup+210.015 s]
Raw data (loadavg): 1.09 1.04 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 29050 0 0 0 20919 84 0 0 25 0 1 0 543499264 82341888 11309 4294967295 134512640 134672761 3221224544 3221085472 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20103 11309 603 41 0 20062 0
vsize: 80412
[startup+220.016 s]
Raw data (loadavg): 1.07 1.03 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 29128 0 0 0 21919 84 0 0 25 0 1 0 543499264 82477056 11387 4294967295 134512640 134672761 3221224544 3220092720 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20136 11387 603 41 0 20095 0
vsize: 80544
[startup+230.016 s]
Raw data (loadavg): 1.06 1.03 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 29563 0 0 0 22918 85 0 0 25 0 1 0 543499264 82927616 11574 4294967295 134512640 134672761 3221224544 3220316976 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20246 11574 603 41 0 20205 0
vsize: 80984
[startup+240.016 s]
Raw data (loadavg): 1.05 1.03 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 29713 0 0 0 23918 86 0 0 25 0 1 0 543499264 83230720 11682 4294967295 134512640 134672761 3221224544 3221136816 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20320 11682 603 41 0 20279 0
vsize: 81280
[startup+250.016 s]
Raw data (loadavg): 1.04 1.03 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 29721 0 0 0 24918 86 0 0 25 0 1 0 543499264 83365888 11690 4294967295 134512640 134672761 3221224544 3220073056 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20353 11690 603 41 0 20312 0
vsize: 81412
[startup+260.016 s]
Raw data (loadavg): 1.04 1.03 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 30024 0 0 0 25918 86 0 0 25 0 1 0 543499264 83972096 11910 4294967295 134512640 134672761 3221224544 3220391280 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20501 11910 603 41 0 20460 0
vsize: 82004
[startup+270.016 s]
Raw data (loadavg): 1.03 1.03 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 30250 0 0 0 26917 87 0 0 25 0 1 0 543499264 90292224 11971 4294967295 134512640 134672761 3221224544 3220041840 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22044 11971 603 41 0 22003 0
vsize: 88176
[startup+280.016 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 30411 0 0 0 27917 87 0 0 25 0 1 0 543499264 90595328 12090 4294967295 134512640 134672761 3221224544 3220980048 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22118 12090 603 41 0 22077 0
vsize: 88472
[startup+290.016 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 30431 0 0 0 28917 87 0 0 25 0 1 0 543499264 90730496 12110 4294967295 134512640 134672761 3221224544 3220300864 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+300.015 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 30431 0 0 0 29918 87 0 0 25 0 1 0 543499264 90730496 12110 4294967295 134512640 134672761 3221224544 3218712256 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+310.017 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 30806 0 0 0 30917 89 0 0 25 0 1 0 543499264 91607040 12402 4294967295 134512640 134672761 3221224544 3221200848 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22365 12402 603 41 0 22324 0
vsize: 89460
[startup+320.017 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31017 0 0 0 31917 89 0 0 25 0 1 0 543499264 91508736 12448 4294967295 134512640 134672761 3221224544 3220636752 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22341 12448 603 41 0 22300 0
vsize: 89364
[startup+330.016 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31148 0 0 0 32916 89 0 0 25 0 1 0 543499264 91811840 12537 4294967295 134512640 134672761 3221224544 3220595872 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+340.016 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31148 0 0 0 33917 89 0 0 25 0 1 0 543499264 91811840 12537 4294967295 134512640 134672761 3221224544 3219811456 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+350.017 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31467 0 0 0 34916 90 0 0 25 0 1 0 543499264 92553216 12773 4294967295 134512640 134672761 3221224544 3220503408 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22596 12773 603 41 0 22555 0
vsize: 90384
[startup+360.017 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31688 0 0 0 35916 90 0 0 25 0 1 0 543499264 92495872 12829 4294967295 134512640 134672761 3221224544 3219970416 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22582 12829 603 41 0 22541 0
vsize: 90328
[startup+370.017 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31847 0 0 0 36915 91 0 0 25 0 1 0 543499264 92798976 12946 4294967295 134512640 134672761 3221224544 3220886832 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22656 12946 603 41 0 22615 0
vsize: 90624
[startup+380.017 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31874 0 0 0 37915 91 0 0 25 0 1 0 543499264 92934144 12973 4294967295 134512640 134672761 3221224544 3220346752 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+390.017 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 31874 0 0 0 38916 91 0 0 25 0 1 0 543499264 92934144 12973 4294967295 134512640 134672761 3221224544 3219278752 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+400.017 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 34848 0 0 0 39908 99 0 0 25 0 1 0 543499264 99078144 14546 4294967295 134512640 134672761 3221224544 3220626000 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24189 14546 603 41 0 24148 0
vsize: 96756
[startup+410.017 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 35106 0 0 0 40908 99 0 0 25 0 1 0 543499264 99139584 14639 4294967295 134512640 134672761 3221224544 3219940136 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24204 14639 603 41 0 24163 0
vsize: 96816
[startup+420.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 35259 0 0 0 41908 100 0 0 25 0 1 0 543499264 99577856 14750 4294967295 134512640 134672761 3221224544 3220809840 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14750 603 41 0 24270 0
vsize: 97244
[startup+430.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 35294 0 0 0 42908 100 0 0 25 0 1 0 543499264 99577856 14785 4294967295 134512640 134672761 3221224544 3220353568 134594133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+440.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 35294 0 0 0 43908 100 0 0 25 0 1 0 543499264 99577856 14785 4294967295 134512640 134672761 3221224544 3219674368 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+450.019 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 35585 0 0 0 44908 100 0 0 25 0 1 0 543499264 100319232 14993 4294967295 134512640 134672761 3221224544 3219962736 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24492 14993 603 41 0 24451 0
vsize: 97968
[startup+460.019 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 35953 0 0 0 45907 102 0 0 25 0 1 0 543499264 100655104 15161 4294967295 134512640 134672761 3221224544 3218514000 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24574 15161 603 41 0 24533 0
vsize: 98296
[startup+470.019 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36174 0 0 0 46907 102 0 0 25 0 1 0 543499264 101265408 15340 4294967295 134512640 134672761 3221224544 3219925296 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24723 15340 603 41 0 24682 0
vsize: 98892
[startup+480.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36225 0 0 0 47907 102 0 0 25 0 1 0 543499264 101400576 15391 4294967295 134512640 134672761 3221224544 3220550640 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 15391 603 41 0 24715 0
vsize: 99024
[startup+490.022 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36262 0 0 0 48907 102 0 0 25 0 1 0 543499264 101535744 15428 4294967295 134512640 134672761 3221224544 3220997040 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15428 603 41 0 24748 0
vsize: 99156
[startup+500.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36281 0 0 0 49907 102 0 0 25 0 1 0 543499264 101535744 15447 4294967295 134512640 134672761 3221224544 3219818848 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+510.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36281 0 0 0 50908 102 0 0 25 0 1 0 543499264 101535744 15447 4294967295 134512640 134672761 3221224544 3219437920 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+520.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36281 0 0 0 51908 102 0 0 25 0 1 0 543499264 101535744 15447 4294967295 134512640 134672761 3221224544 3218932192 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+530.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36281 0 0 0 52908 102 0 0 25 0 1 0 543499264 101535744 15447 4294967295 134512640 134672761 3221224544 3217945504 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+540.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36669 0 0 0 53907 103 0 0 25 0 1 0 543499264 102412288 15752 4294967295 134512640 134672761 3221224544 3220363920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25003 15752 603 41 0 24962 0
vsize: 100012
[startup+550.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 36845 0 0 0 54907 104 0 0 25 0 1 0 543499264 102277120 15726 4294967295 134512640 134672761 3221224544 3217679280 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24970 15726 603 41 0 24929 0
vsize: 99880
[startup+560.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37138 0 0 0 55906 104 0 0 25 0 1 0 543499264 103047168 15977 4294967295 134512640 134672761 3221224544 3219714672 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25158 15977 603 41 0 25117 0
vsize: 100632
[startup+570.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37192 0 0 0 56906 104 0 0 25 0 1 0 543499264 103182336 16031 4294967295 134512640 134672761 3221224544 3220367568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25191 16031 603 41 0 25150 0
vsize: 100764
[startup+580.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37230 0 0 0 57907 104 0 0 25 0 1 0 543499264 103317504 16069 4294967295 134512640 134672761 3221224544 3220825680 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16069 603 41 0 25183 0
vsize: 100896
[startup+590.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37259 0 0 0 58907 104 0 0 25 0 1 0 543499264 103317504 16098 4294967295 134512640 134672761 3221224544 3221183952 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16098 603 41 0 25183 0
vsize: 100896
[startup+600.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37262 0 0 0 59907 104 0 0 25 0 1 0 543499264 103317504 16101 4294967295 134512640 134672761 3221224544 3219555808 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+610.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37262 0 0 0 60907 104 0 0 25 0 1 0 543499264 103317504 16101 4294967295 134512640 134672761 3221224544 3219185344 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+620.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37262 0 0 0 61907 105 0 0 25 0 1 0 543499264 103317504 16101 4294967295 134512640 134672761 3221224544 3218690368 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+630.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37262 0 0 0 62907 105 0 0 25 0 1 0 543499264 103317504 16101 4294967295 134512640 134672761 3221224544 3217760320 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+640.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37640 0 0 0 63907 105 0 0 25 0 1 0 543499264 104194048 16396 4294967295 134512640 134672761 3221224544 3220273584 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25438 16396 603 41 0 25397 0
vsize: 101752
[startup+650.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37716 0 0 0 64907 106 0 0 25 0 1 0 543499264 104464384 16472 4294967295 134512640 134672761 3221224544 3221118384 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25504 16472 603 41 0 25463 0
vsize: 102016
[startup+660.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 37962 0 0 0 65906 106 0 0 25 0 1 0 543499264 104411136 16518 4294967295 134512640 134672761 3221224544 3219697104 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25491 16518 603 41 0 25450 0
vsize: 101964
[startup+670.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38104 0 0 0 66906 106 0 0 25 0 1 0 543499264 104714240 16618 4294967295 134512640 134672761 3221224544 3220401264 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16618 603 41 0 25524 0
vsize: 102260
[startup+680.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38143 0 0 0 67906 106 0 0 25 0 1 0 543499264 104849408 16657 4294967295 134512640 134672761 3221224544 3220883376 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16657 603 41 0 25557 0
vsize: 102392
[startup+690.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38171 0 0 0 68907 106 0 0 25 0 1 0 543499264 104849408 16685 4294967295 134512640 134672761 3221224544 3220480672 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+700.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38171 0 0 0 69908 107 0 0 25 0 1 0 543499264 104849408 16685 4294967295 134512640 134672761 3221224544 3219550528 134594131 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.035 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38171 0 0 0 70908 107 0 0 25 0 1 0 543499264 104849408 16685 4294967295 134512640 134672761 3221224544 3219098272 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+720.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38171 0 0 0 71908 107 0 0 25 0 1 0 543499264 104849408 16685 4294967295 134512640 134672761 3221224544 3218207200 134594124 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.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38509 0 0 0 72908 107 0 0 25 0 1 0 543499264 105590784 16940 4294967295 134512640 134672761 3221224544 3219906000 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25779 16940 603 41 0 25738 0
vsize: 103116
[startup+740.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38598 0 0 0 73908 108 0 0 25 0 1 0 543499264 105861120 17029 4294967295 134512640 134672761 3221224544 3220984272 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25845 17029 603 41 0 25804 0
vsize: 103380
[startup+750.037 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38837 0 0 0 74908 108 0 0 25 0 1 0 543499264 105762816 17068 4294967295 134512640 134672761 3221224544 3219528144 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25821 17068 603 41 0 25780 0
vsize: 103284
[startup+760.036 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 38983 0 0 0 75907 108 0 0 25 0 1 0 543499264 106065920 17172 4294967295 134512640 134672761 3221224544 3220303056 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25895 17172 603 41 0 25854 0
vsize: 103580
[startup+770.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39025 0 0 0 76908 108 0 0 25 0 1 0 543499264 106201088 17214 4294967295 134512640 134672761 3221224544 3220813776 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17214 603 41 0 25887 0
vsize: 103712
[startup+780.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39058 0 0 0 77908 108 0 0 25 0 1 0 543499264 106336256 17247 4294967295 134512640 134672761 3221224544 3221199504 134594214 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.047 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39058 0 0 0 78909 109 0 0 25 0 1 0 543499264 106336256 17247 4294967295 134512640 134672761 3221224544 3219613984 134594131 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.054 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39058 0 0 0 79910 109 0 0 25 0 1 0 543499264 106336256 17247 4294967295 134512640 134672761 3221224544 3219182752 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.057 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39058 0 0 0 80910 109 0 0 25 0 1 0 543499264 106336256 17247 4294967295 134512640 134672761 3221224544 3218319808 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+820.058 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39374 0 0 0 81910 109 0 0 25 0 1 0 543499264 107077632 17480 4294967295 134512640 134672761 3221224544 3219626256 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26142 17480 603 41 0 26101 0
vsize: 104568
[startup+830.058 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39474 0 0 0 82910 109 0 0 25 0 1 0 543499264 107347968 17580 4294967295 134512640 134672761 3221224544 3220859760 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26208 17580 603 41 0 26167 0
vsize: 104832
[startup+840.058 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39708 0 0 0 83909 110 0 0 25 0 1 0 543499264 119758848 17614 4294967295 134512640 134672761 3221224544 3219351312 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29238 17614 603 41 0 29197 0
vsize: 116952
[startup+850.068 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39863 0 0 0 84910 110 0 0 25 0 1 0 543499264 120197120 17727 4294967295 134512640 134672761 3221224544 3220216080 134594231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17727 603 41 0 29304 0
vsize: 117380
[startup+860.073 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39907 0 0 0 85911 110 0 0 25 0 1 0 543499264 120197120 17771 4294967295 134512640 134672761 3221224544 3220756368 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17771 603 41 0 29304 0
vsize: 117380
[startup+870.08 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39940 0 0 0 86911 111 0 0 25 0 1 0 543499264 120332288 17804 4294967295 134512640 134672761 3221224544 3221156400 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17804 603 41 0 29337 0
vsize: 117512
[startup+880.08 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39945 0 0 0 87912 111 0 0 25 0 1 0 543499264 120332288 17809 4294967295 134512640 134672761 3221224544 3219665536 134594089 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.087 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39945 0 0 0 88912 111 0 0 25 0 1 0 543499264 120332288 17809 4294967295 134512640 134672761 3221224544 3219244480 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+900.092 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 39945 0 0 0 89913 111 0 0 25 0 1 0 543499264 120332288 17809 4294967295 134512640 134672761 3221224544 3218414656 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+910.096 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 40249 0 0 0 90913 112 0 0 25 0 1 0 543499264 121073664 18030 4294967295 134512640 134672761 3221224544 3219499632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29559 18030 603 41 0 29518 0
vsize: 118236
[startup+920.101 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 40357 0 0 0 91913 112 0 0 25 0 1 0 543499264 121344000 18138 4294967295 134512640 134672761 3221224544 3220823952 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29625 18138 603 41 0 29584 0
vsize: 118500
[startup+930.101 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 40717 0 0 0 92912 113 0 0 25 0 1 0 543499264 121733120 18291 4294967295 134512640 134672761 3221224544 3218668368 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29720 18291 603 41 0 29679 0
vsize: 118880
[startup+940.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 40873 0 0 0 93913 113 0 0 25 0 1 0 543499264 122036224 18405 4294967295 134512640 134672761 3221224544 3219561072 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29794 18405 603 41 0 29753 0
vsize: 119176
[startup+950.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 40918 0 0 0 94913 113 0 0 25 0 1 0 543499264 122171392 18450 4294967295 134512640 134672761 3221224544 3220108944 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18450 603 41 0 29786 0
vsize: 119308
[startup+960.11 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 40951 0 0 0 95913 114 0 0 25 0 1 0 543499264 122306560 18483 4294967295 134512640 134672761 3221224544 3220512816 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18483 603 41 0 29819 0
vsize: 119440
[startup+970.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 40978 0 0 0 96913 114 0 0 25 0 1 0 543499264 122306560 18510 4294967295 134512640 134672761 3221224544 3220840464 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18510 603 41 0 29819 0
vsize: 119440
[startup+980.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41000 0 0 0 97913 114 0 0 25 0 1 0 543499264 122441728 18532 4294967295 134512640 134672761 3221224544 3221122992 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18532 603 41 0 29852 0
vsize: 119572
[startup+990.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41009 0 0 0 98914 114 0 0 25 0 1 0 543499264 122441728 18541 4294967295 134512640 134672761 3221224544 3219507904 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+1000.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41009 0 0 0 99914 114 0 0 25 0 1 0 543499264 122441728 18541 4294967295 134512640 134672761 3221224544 3219013312 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.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41009 0 0 0 100915 114 0 0 25 0 1 0 543499264 122441728 18541 4294967295 134512640 134672761 3221224544 3218718496 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.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41009 0 0 0 101916 114 0 0 25 0 1 0 543499264 122441728 18541 4294967295 134512640 134672761 3221224544 3218368768 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.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41009 0 0 0 102916 114 0 0 25 0 1 0 543499264 122441728 18541 4294967295 134512640 134672761 3221224544 3217744480 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+1040.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41009 0 0 0 103917 114 0 0 25 0 1 0 543499264 122441728 18541 4294967295 134512640 134672761 3221224544 3217214464 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+1050.15 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41393 0 0 0 104918 115 0 0 25 0 1 0 543499264 123318272 18842 4294967295 134512640 134672761 3221224544 3219859920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30107 18842 603 41 0 30066 0
vsize: 120428
[startup+1060.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41475 0 0 0 105918 115 0 0 25 0 1 0 543499264 123588608 18924 4294967295 134512640 134672761 3221224544 3220671696 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30173 18924 603 41 0 30132 0
vsize: 120692
[startup+1070.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 41566 0 0 0 106918 116 0 0 25 0 1 0 543499264 123183104 18850 4294967295 134512640 134672761 3221224544 3220975536 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 18850 603 41 0 30033 0
vsize: 120296
[startup+1080.16 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 42280 0 0 0 107918 117 0 0 25 0 1 0 543499264 124661760 19396 4294967295 134512640 134672761 3221224544 3220916992 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 19396 603 41 0 30394 0
vsize: 121740
[startup+1087.39 s]
Raw data (loadavg): 1.00 1.00 0.95 1/53 32135
Raw data (stat): 32133 (minisat+) R 32132 28099 28098 0 -1 0 42280 0 0 0 107918 117 0 0 25 0 1 0 543499264 124661760 19396 4294967295 134512640 134672761 3221224544 3220916992 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 19396 603 41 0 30394 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1087.39
CPU time (s): 1087.58
CPU user time (s): 1085.52
CPU system time (s): 2.06069
CPU usage (%): 100.018
Max. virtual memory (Kb): 121740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####