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/miplib/normalized-mps-v2-13-7-l152lav.opb
MD5SUM	00855a9538cee8df79108d56ee6867b4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5046
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	268
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1176.34
Number of variables	1989
Total number of constraints	2086
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2085
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1989
Trace number 15701

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-21 05:31:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16898 boxname=wulflinc9 idbench=1300 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00855a9538cee8df79108d56ee6867b4  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-l152lav.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-l152lav.opb /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-l152lav.opb
IDLAUNCH: 16898
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        474072 kB
Buffers:         35716 kB
Cached:         502088 kB
SwapCached:          8 kB
Active:         120860 kB
Inactive:       419808 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        473820 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            14224 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:51:31 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 16898 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 192]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[ 190]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:  255
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   83
c ---[ 182]---> BDD-cost:   93
c ---[ 180]---> BDD-cost:  149
c ---[ 178]---> BDD-cost:  235
c ---[ 176]---> BDD-cost:  339
c ---[ 174]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:   21
c ---[ 170]---> BDD-cost:  301
c ---[ 168]---> BDD-cost:  181
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   71
c ---[ 162]---> BDD-cost:   67
c ---[ 160]---> BDD-cost:   57
c ---[ 158]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:   39
c ---[ 154]---> BDD-cost:   85
c ---[ 152]---> BDD-cost:  147
c ---[ 150]---> BDD-cost:  189
c ---[ 148]---> BDD-cost:  211
c ---[ 146]---> BDD-cost:   95
c ---[ 144]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   35
c ---[ 140]---> BDD-cost:   59
c ---[ 138]---> BDD-cost:  171
c ---[ 136]---> BDD-cost:   59
c ---[ 134]---> BDD-cost:   51
c ---[ 132]---> BDD-cost:  151
c ---[ 130]---> BDD-cost:  147
c ---[ 128]---> BDD-cost:  317
c ---[ 126]---> BDD-cost:  201
c ---[ 124]---> BDD-cost:  105
c ---[ 122]---> BDD-cost:  101
c ---[ 120]---> BDD-cost:  121
c ---[ 118]---> BDD-cost:  133
c ---[ 116]---> BDD-cost:  149
c ---[ 114]---> BDD-cost:  189
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:  201
c ---[ 108]---> BDD-cost:   49
c ---[ 106]---> BDD-cost:   81
c ---[ 104]---> BDD-cost:  121
c ---[ 102]---> BDD-cost:  433
c ---[ 100]---> BDD-cost:  191
c ---[  98]---> BDD-cost:   81
c ---[  96]---> BDD-cost:   71
c ---[  94]---> BDD-cost:  103
c ---[  92]---> BDD-cost:   93
c ---[  90]---> BDD-cost:   85
c ---[  88]---> BDD-cost:  189
c ---[  86]---> BDD-cost:  231
c ---[  84]---> BDD-cost:  101
c ---[  82]---> BDD-cost:  109
c ---[  80]---> BDD-cost:  171
c ---[  78]---> BDD-cost:  183
c ---[  76]---> BDD-cost:  173
c ---[  74]---> BDD-cost:  239
c ---[  72]---> BDD-cost:   91
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  239
c ---[  66]---> BDD-cost:  105
c ---[  64]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  221
c ---[  60]---> BDD-cost:  213
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  179
c ---[  54]---> BDD-cost:  213
c ---[  52]---> BDD-cost:  143
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:   81
c ---[  46]---> BDD-cost:  205
c ---[  44]---> BDD-cost:   61
c ---[  42]---> BDD-cost:  225
c ---[  40]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  253
c ---[  36]---> BDD-cost:   71
c ---[  34]---> BDD-cost:  203
c ---[  32]---> BDD-cost:   45
c ---[  30]---> BDD-cost:  133
c ---[  28]---> BDD-cost:  323
c ---[  26]---> BDD-cost:  155
c ---[  24]---> BDD-cost:   89
c ---[  22]---> BDD-cost:   93
c ---[  20]---> BDD-cost:   83
c ---[  18]---> BDD-cost:   67
c ---[  16]---> BDD-cost:  133
c ---[  14]---> BDD-cost:  247
c ---[  12]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   8]---> BDD-cost:  151
c ---[   6]---> BDD-cost:  181
c ---[   4]---> BDD-cost:  151
c ---[   2]---> BDD-cost:  181
c ---[   0]---> Adder-cost: 3598   maxlim: 1961   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   97126   314221 |   29137       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24129          
c   -- var.elim.:  2000/24129          
c   -- var.elim.:  3000/24129          
c   -- var.elim.:  4000/24129          
c   -- var.elim.:  5000/24129          
c   -- var.elim.:  6000/24129          
c   -- var.elim.:  7000/24129          
c   -- var.eli#### 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.84 0.94 0.90 2/54 2459
Raw data (stat): 2459 (runsolver) R 2458 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484357650 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.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 6475 0 0 0 983 15 0 0 25 0 1 0 484357650 27369472 5574 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6682 5574 603 41 0 6641 0
vsize: 26728
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 6863 0 0 0 1982 16 0 0 25 0 1 0 484357650 28954624 5962 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7069 5962 603 41 0 7028 0
vsize: 28276
[startup+30.0017 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 7313 0 0 0 2981 18 0 0 25 0 1 0 484357650 30822400 6412 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7525 6412 603 41 0 7484 0
vsize: 30100
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 7881 0 0 0 3980 19 0 0 25 0 1 0 484357650 33189888 6980 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 6981 603 41 0 8062 0
vsize: 32412
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 8493 0 0 0 4977 21 0 0 25 0 1 0 484357650 35565568 7592 4294967295 134512640 134672761 3221224544 3221223680 134614656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8683 7592 603 41 0 8642 0
vsize: 34732
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 9227 0 0 0 5976 23 0 0 25 0 1 0 484357650 38572032 8326 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9417 8326 603 41 0 9376 0
vsize: 37668
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 10084 0 0 0 6974 25 0 0 25 0 1 0 484357650 42123264 9183 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10284 9183 603 41 0 10243 0
vsize: 41136
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 11819 0 0 0 7970 29 0 0 25 0 1 0 484357650 49348608 10918 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12048 10918 603 41 0 12007 0
vsize: 48192
[startup+90.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 12467 0 0 0 8969 31 0 0 25 0 1 0 484357650 51990528 11566 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11566 603 41 0 12652 0
vsize: 50772
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 13356 0 0 0 9967 33 0 0 25 0 1 0 484357650 55541760 12455 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13560 12455 603 41 0 13519 0
vsize: 54240
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 14276 0 0 0 10965 35 0 0 25 0 1 0 484357650 59408384 13375 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14504 13375 603 41 0 14463 0
vsize: 58016
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 14748 0 0 0 11964 36 0 0 25 0 1 0 484357650 61263872 13847 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14957 13847 603 41 0 14916 0
vsize: 59828
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 16168 0 0 0 12961 40 0 0 25 0 1 0 484357650 67055616 15267 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16371 15267 603 41 0 16330 0
vsize: 65484
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 17329 0 0 0 13958 42 0 0 25 0 1 0 484357650 71790592 16428 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17527 16428 603 41 0 17486 0
vsize: 70108
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 18303 0 0 0 14955 45 0 0 25 0 1 0 484357650 75730944 17402 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18489 17402 603 41 0 18448 0
vsize: 73956
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 19522 0 0 0 15952 49 0 0 25 0 1 0 484357650 80748544 18621 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19714 18621 603 41 0 19673 0
vsize: 78856
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 20520 0 0 0 16950 51 0 0 25 0 1 0 484357650 84807680 19619 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 19619 603 41 0 20664 0
vsize: 82820
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 21686 0 0 0 17947 54 0 0 25 0 1 0 484357650 89812992 20785 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21927 20785 603 41 0 21886 0
vsize: 87708
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 22913 0 0 0 18943 58 0 0 25 0 1 0 484357650 94822400 22012 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23150 22012 603 41 0 23109 0
vsize: 92600
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 23915 0 0 0 19940 61 0 0 25 0 1 0 484357650 99037184 23014 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24179 23014 603 41 0 24138 0
vsize: 96716
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 25020 0 0 0 20938 64 0 0 25 0 1 0 484357650 103518208 24119 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25273 24119 603 41 0 25232 0
vsize: 101092
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 26908 0 0 0 21932 69 0 0 25 0 1 0 484357650 111263744 26007 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27164 26007 603 41 0 27123 0
vsize: 108656
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 27742 0 0 0 22930 72 0 0 25 0 1 0 484357650 114634752 26841 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27987 26841 603 41 0 27946 0
vsize: 111948
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 28754 0 0 0 23928 74 0 0 25 0 1 0 484357650 118697984 27853 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28979 27853 603 41 0 28938 0
vsize: 115916
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 29869 0 0 0 24926 77 0 0 25 0 1 0 484357650 123293696 28968 4294967295 134512640 134672761 3221224544 3221223744 134610683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30101 28968 603 41 0 30060 0
vsize: 120404
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 31034 0 0 0 25923 80 0 0 25 0 1 0 484357650 128086016 30133 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31271 30133 603 41 0 31230 0
vsize: 125084
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 31938 0 0 0 26920 83 0 0 25 0 1 0 484357650 131776512 31037 4294967295 134512640 134672761 3221224544 3221223680 134614741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32172 31037 603 41 0 32131 0
vsize: 128688
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 32776 0 0 0 27918 85 0 0 25 0 1 0 484357650 135208960 31875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33010 31875 603 41 0 32969 0
vsize: 132040
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 33842 0 0 0 28916 87 0 0 25 0 1 0 484357650 139538432 32941 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34067 32941 603 41 0 34026 0
vsize: 136268
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 34626 0 0 0 29914 89 0 0 25 0 1 0 484357650 142708736 33725 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34841 33725 603 41 0 34800 0
vsize: 139364
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 35637 0 0 0 30913 91 0 0 25 0 1 0 484357650 146931712 34736 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35872 34736 603 41 0 35831 0
vsize: 143488
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 36721 0 0 0 31910 93 0 0 25 0 1 0 484357650 151277568 35820 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36933 35820 603 41 0 36892 0
vsize: 147732
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 37571 0 0 0 32908 96 0 0 25 0 1 0 484357650 154816512 36670 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37797 36670 603 41 0 37756 0
vsize: 151188
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 38667 0 0 0 33906 98 0 0 25 0 1 0 484357650 159313920 37766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38895 37766 603 41 0 38854 0
vsize: 155580
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 39547 0 0 0 34904 100 0 0 25 0 1 0 484357650 162852864 38646 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39759 38646 603 41 0 39718 0
vsize: 159036
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 40723 0 0 0 35902 102 0 0 25 0 1 0 484357650 167686144 39822 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40939 39822 603 41 0 40898 0
vsize: 163756
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 41438 0 0 0 36901 104 0 0 25 0 1 0 484357650 170553344 40537 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41639 40537 603 41 0 41598 0
vsize: 166556
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 42225 0 0 0 37900 105 0 0 25 0 1 0 484357650 173813760 41324 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42435 41324 603 41 0 42394 0
vsize: 169740
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 42924 0 0 0 38898 107 0 0 25 0 1 0 484357650 176709632 42023 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43142 42023 603 41 0 43101 0
vsize: 172568
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 43238 0 0 0 39897 108 0 0 25 0 1 0 484357650 177901568 42337 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43433 42337 603 41 0 43392 0
vsize: 173732
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 43665 0 0 0 40896 109 0 0 25 0 1 0 484357650 179752960 42764 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43885 42764 603 41 0 43844 0
vsize: 175540
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 43990 0 0 0 41896 110 0 0 25 0 1 0 484357650 181075968 43089 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44208 43089 603 41 0 44167 0
vsize: 176832
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 44390 0 0 0 42895 111 0 0 25 0 1 0 484357650 182640640 43489 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44590 43489 603 41 0 44549 0
vsize: 178360
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 45085 0 0 0 43894 113 0 0 25 0 1 0 484357650 185548800 44184 4294967295 134512640 134672761 3221224544 3221223584 134614286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45300 44184 603 41 0 45259 0
vsize: 181200
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 45958 0 0 0 44892 114 0 0 25 0 1 0 484357650 189116416 45057 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46171 45057 603 41 0 46130 0
vsize: 184684
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 46717 0 0 0 45891 116 0 0 25 0 1 0 484357650 192126976 45816 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46906 45816 603 41 0 46865 0
vsize: 187624
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 47328 0 0 0 46889 118 0 0 25 0 1 0 484357650 195166208 46427 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47648 46427 603 41 0 47607 0
vsize: 190592
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 48107 0 0 0 47887 120 0 0 25 0 1 0 484357650 198426624 47206 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48444 47206 603 41 0 48403 0
vsize: 193776
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 48528 0 0 0 48886 121 0 0 25 0 1 0 484357650 200142848 47627 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48863 47627 603 41 0 48822 0
vsize: 195452
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 49253 0 0 0 49884 123 0 0 25 0 1 0 484357650 203030528 48352 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49568 48352 603 41 0 49527 0
vsize: 198272
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 50056 0 0 0 50882 126 0 0 25 0 1 0 484357650 206344192 49155 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50377 49155 603 41 0 50336 0
vsize: 201508
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 51053 0 0 0 51880 128 0 0 25 0 1 0 484357650 210415616 50152 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51371 50152 603 41 0 51330 0
vsize: 205484
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 51810 0 0 0 52878 130 0 0 25 0 1 0 484357650 213458944 50909 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52114 50909 603 41 0 52073 0
vsize: 208456
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 52485 0 0 0 53876 132 0 0 25 0 1 0 484357650 216223744 51584 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52789 51584 603 41 0 52748 0
vsize: 211156
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 53110 0 0 0 54875 134 0 0 25 0 1 0 484357650 218832896 52209 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53426 52209 603 41 0 53385 0
vsize: 213704
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 53815 0 0 0 55873 136 0 0 25 0 1 0 484357650 221614080 52914 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54105 52914 603 41 0 54064 0
vsize: 216420
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 54851 0 0 0 56870 138 0 0 25 0 1 0 484357650 225882112 53950 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55147 53950 603 41 0 55106 0
vsize: 220588
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 56045 0 0 0 57868 141 0 0 25 0 1 0 484357650 230821888 55144 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56353 55144 603 41 0 56312 0
vsize: 225412
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 56868 0 0 0 58866 143 0 0 25 0 1 0 484357650 234115072 55967 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57157 55967 603 41 0 57116 0
vsize: 228628
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 57563 0 0 0 59865 145 0 0 25 0 1 0 484357650 236978176 56662 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57856 56662 603 41 0 57815 0
vsize: 231424
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 58150 0 0 0 60863 147 0 0 25 0 1 0 484357650 239353856 57249 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58436 57249 603 41 0 58395 0
vsize: 233744
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 58976 0 0 0 61861 149 0 0 25 0 1 0 484357650 242782208 58075 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59273 58075 603 41 0 59232 0
vsize: 237092
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 59864 0 0 0 62859 151 0 0 25 0 1 0 484357650 246448128 58963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60168 58963 603 41 0 60127 0
vsize: 240672
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 60651 0 0 0 63858 152 0 0 25 0 1 0 484357650 249614336 59750 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60941 59750 603 41 0 60900 0
vsize: 243764
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 61435 0 0 0 64857 154 0 0 25 0 1 0 484357650 252772352 60534 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61712 60534 603 41 0 61671 0
vsize: 246848
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 62179 0 0 0 65855 156 0 0 25 0 1 0 484357650 255918080 61278 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62480 61278 603 41 0 62439 0
vsize: 249920
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 63006 0 0 0 66853 158 0 0 25 0 1 0 484357650 259207168 62105 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63283 62105 603 41 0 63242 0
vsize: 253132
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 63821 0 0 0 67852 159 0 0 25 0 1 0 484357650 262627328 62920 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64118 62920 603 41 0 64077 0
vsize: 256472
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 64738 0 0 0 68850 161 0 0 25 0 1 0 484357650 266305536 63837 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65016 63837 603 41 0 64975 0
vsize: 260064
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 65818 0 0 0 69848 163 0 0 25 0 1 0 484357650 270749696 64917 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66101 64917 603 41 0 66060 0
vsize: 264404
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 66479 0 0 0 70847 165 0 0 25 0 1 0 484357650 273526784 65578 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66779 65578 603 41 0 66738 0
vsize: 267116
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 67359 0 0 0 71844 167 0 0 25 0 1 0 484357650 277045248 66458 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67638 66458 603 41 0 67597 0
vsize: 270552
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 68322 0 0 0 72843 169 0 0 25 0 1 0 484357650 281042944 67421 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68614 67421 603 41 0 68573 0
vsize: 274456
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 69529 0 0 0 73840 172 0 0 25 0 1 0 484357650 285982720 68628 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69820 68628 603 41 0 69779 0
vsize: 279280
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 70688 0 0 0 74839 174 0 0 25 0 1 0 484357650 290705408 69787 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70973 69787 603 41 0 70932 0
vsize: 283892
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 71762 0 0 0 75836 176 0 0 25 0 1 0 484357650 295137280 70861 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72055 70861 603 41 0 72014 0
vsize: 288220
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 72908 0 0 0 76835 178 0 0 25 0 1 0 484357650 299773952 72007 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73187 72007 603 41 0 73146 0
vsize: 292748
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 73970 0 0 0 77832 181 0 0 25 0 1 0 484357650 304168960 73069 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74260 73069 603 41 0 74219 0
vsize: 297040
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 75228 0 0 0 78830 183 0 0 25 0 1 0 484357650 309354496 74327 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75526 74327 603 41 0 75485 0
vsize: 302104
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76389 0 0 0 79827 186 0 0 25 0 1 0 484357650 314036224 75488 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76669 75488 603 41 0 76628 0
vsize: 306676
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 80826 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 81826 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 82827 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 83827 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 84827 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 85827 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 86827 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 87827 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 88828 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 89828 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 90828 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 91828 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 92828 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 93829 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 94829 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 95829 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 96829 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134614330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 97829 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 98830 187 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 99829 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 100830 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 101830 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 102830 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 103830 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 104831 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 105831 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 106831 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 107831 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 108831 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 109832 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 110832 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 111832 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 112832 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 113832 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 114832 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 115833 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 116833 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 117833 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 118833 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2459
Raw data (stat): 2459 (minisat+) R 2458 30854 30853 0 -1 0 76845 0 0 0 119833 188 0 0 25 0 1 0 484357650 315408384 75734 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77004 75734 603 41 0 76963 0
vsize: 308016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2459
Raw data (stat): 2459 (minisat+) Z 2458 30854 30853 0 -1 12 76845 0 0 0 119833 202 0 0 25 0 1 0 484357650 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.17
CPU time (s): 1200.36
CPU user time (s): 1198.34
CPU system time (s): 2.02169
CPU usage (%): 100.016
Max. virtual memory (Kb): 308016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####