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/submitted/een/normalized-air03.opb
MD5SUM	017636577e3ff026b2ea720fb537705b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	10757
Biggest coefficient in the objective function	6873
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	13748961
Number of bits of the sum of numbers in the objective function	24
Biggest number in a constraint	6873
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	13748961
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	2.22466
Number of variables	10757
Total number of constraints	248
Number of constraints which are clauses	126
Number of constraints which are cardinality constraints (but not clauses)	122
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	3861
Trace number 6986

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-14 20:50:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5041 boxname=wulflinc1 idbench=388 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  017636577e3ff026b2ea720fb537705b  /oldhome/oroussel/tmp/wulflinc1/normalized-air03.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc1/normalized-air03.opb /oldhome/oroussel/tmp/wulflinc1/normalized-air03.opb
IDLAUNCH: 5041
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        823944 kB
Buffers:         41552 kB
Cached:         144632 kB
SwapCached:          0 kB
Active:         113664 kB
Inactive:        75640 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        823692 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7204 kB
Slab:            15688 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:10:18 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 5041 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 248 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ============================================================================================================================
c   -- Clauses(.)/Splits(s): ..
c ---[ 242]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 240]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 238]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 236]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 234]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 232]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 230]---> Adder-cost: 10   maxlim: 10   bits: 4/4
c ---[ 228]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 226]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 224]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 222]---> Adder-cost: 44   maxlim: 29   bits: 5/5
c ---[ 220]---> Adder-cost: 18   maxlim: 29   bits: 5/5
c ---[ 218]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 216]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[ 214]---> Adder-cost: 78   maxlim: 40   bits: 6/6
c ---[ 212]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[ 210]---> Adder-cost: 92   maxlim: 46   bits: 6/6
c ---[ 208]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 206]---> Adder-cost: 72   maxlim: 56   bits: 6/6
c ---[ 204]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 202]---> Adder-cost: 78   maxlim: 60   bits: 6/6
c ---[ 200]---> Adder-cost: 140   maxlim: 71   bits: 7/7
c ---[ 198]---> Adder-cost: 148   maxlim: 77   bits: 7/7
c ---[ 196]---> Adder-cost: 48   maxlim: 77   bits: 7/7
c ---[ 194]---> Adder-cost: 158   maxlim: 87   bits: 7/7
c ---[ 192]---> Adder-cost: 172   maxlim: 89   bits: 7/7
c ---[ 190]---> Adder-cost: 196   maxlim: 100   bits: 7/7
c ---[ 188]---> Adder-cost: 224   maxlim: 114   bits: 7/7
c ---[ 186]---> Adder-cost: 62   maxlim: 114   bits: 7/7
c ---[ 184]---> Adder-cost: 226   maxlim: 116   bits: 7/7
c ---[ 182]---> Adder-cost: 62   maxlim: 116   bits: 7/7
c ---[ 180]---> Adder-cost: 232   maxlim: 121   bits: 7/7
c ---[ 178]---> Adder-cost: 262   maxlim: 132   bits: 8/8
c ---[ 176]---> Adder-cost: 258   maxlim: 135   bits: 8/8
c ---[ 174]---> Adder-cost: 290   maxlim: 149   bits: 8/8
c ---[ 172]---> Adder-cost: 304   maxlim: 154   bits: 8/8
c ---[ 170]---> Adder-cost: 298   maxlim: 155   bits: 8/8
c ---[ 168]---> Adder-cost: 230   maxlim: 166   bits: 8/8
c ---[ 166]---> Adder-cost: 220   maxlim: 168   bits: 8/8
c ---[ 164]---> Adder-cost: 338   maxlim: 177   bits: 8/8
c ---[ 162]---> Adder-cost: 346   maxlim: 178   bits: 8/8
c ---[ 160]---> Adder-cost: 344   maxlim: 184   bits: 8/8
c ---[ 158]---> Adder-cost: 438   maxlim: 223   bits: 8/8
c ---[ 156]---> Adder-cost: 456   maxlim: 233   bits: 8/8
c ---[ 154]---> Adder-cost: 462   maxlim: 237   bits: 8/8
c ---[ 152]---> Adder-cost: 474   maxlim: 241   bits: 8/8
c ---[ 150]---> Adder-cost: 114   maxlim: 241   bits: 8/8
c ---[ 148]---> Adder-cost: 546   maxlim: 275   bits: 9/9
c ---[ 146]---> Adder-cost: 538   maxlim: 276   bits: 9/9
c ---[ 144]---> Adder-cost: 120   maxlim: 276   bits: 9/9
c ---[ 142]---> Adder-cost: 642   maxlim: 325   bits: 9/9
c ---[ 140]---> Adder-cost: 652   maxlim: 333   bits: 9/9
c ---[ 138]---> Adder-cost: 666   maxlim: 336   bits: 9/9
c ---[ 136]---> Adder-cost: 674   maxlim: 349   bits: 9/9
c ---[ 134]---> Adder-cost: 804   maxlim: 410   bits: 9/9
c ---[ 132]---> Adder-cost: 820   maxlim: 415   bits: 9/9
c ---[ 130]---> Adder-cost: 842   maxlim: 431   bits: 9/9
c ---[ 128]---> Adder-cost: 828   maxlim: 472   bits: 9/9
c ---[ 126]---> Adder-cost: 756   maxlim: 523   bits: 10/10
c ---[ 124]---> Adder-cost: 952   maxlim: 549   bits: 10/10
c ---[ 122]---> Adder-cost: 992   maxlim: 552   bits: 10/10
c ---[ 120]---> Adder-cost: 1064   maxlim: 565   bits: 10/10
c ---[ 118]---> Adder-cost: 994   maxlim: 568   bits: 10/10
c ---[ 116]---> Adder-cost: 1020   maxlim: 568   bits: 10/10
c ---[ 114]---> Adder-cost: 1036   maxlim: 599   bits: 10/10
c ---[ 112]---> Adder-cost: 1212   maxlim: 631   bits: 10/10
c ---[ 110]---> Adder-cost: 1104   maxlim: 662   bits: 10/10
c ---[ 108]---> Adder-cost: 1212   maxlim: 674   bits: 10/10
c ---[ 106]---> Adder-cost: 1266   maxlim: 675   bits: 10/10
c ---[ 104]---> Adder-cost: 1230   maxlim: 678   bits: 10/10
c ---[ 102]---> Adder-cost: 1310   maxlim: 706   bits: 10/10
c ---[ 100]---> Adder-cost: 238   maxlim: 706   bits: 10/10
c ---[  98]---> Adder-cost: 1276   maxlim: 718   bits: 10/10
c ---[  96]---> Adder-cost: 1384   maxlim: 744   bits: 10/10
c ---[  94]---> Adder-cost: 1504   maxlim: 767   bits: 10/10
c ---[  92]---> Adder-cost: 1384   maxlim: 771   bits: 10/10
c ---[  90]---> Adder-cost: 240   maxlim: 771   bits: 10/10
c ---[  88]---> Adder-cost: 1218   maxlim: 793   bits: 10/10
c ---[  86]---> Adder-cost: 1356   maxlim: 853   bits: 10/10
c ---[  84]---> Adder-cost: 1674   maxlim: 912   bits: 10/10
c ---[  82]---> Adder-cost: 262   maxlim: 912   bits: 10/10
c ---[  80]---> Adder-cost: 1670   maxlim: 916   bits: 10/10
c ---[  78]---> Adder-cost: 258   maxlim: 916   bits: 10/10
c ---[  76]---> Adder-cost: 1770   maxlim: 925   bits: 10/10
c ---[  74]---> Adder-cost: 1536   maxlim: 930   bits: 10/10
c ---[  72]---> Adder-cost: 1666   maxlim: 940   bits: 10/10
c ---[  70]---> Adder-cost: 1278   maxlim: 954   bits: 10/10
c ---[  68]---> Adder-cost: 968   maxlim: 970   bits: 10/10
c ---[  66]---> Adder-cost: 1730   maxlim: 978   bits: 10/10
c ---[  64]---> Adder-cost: 1692   maxlim: 986   bits: 10/10
c ---[  62]---> Adder-cost: 1790   maxlim: 1018   bits: 10/10
c ---[  60]---> Adder-cost: 1742   maxlim: 1057   bits: 11/11
c ---[  58]---> Adder-cost: 2034   maxlim: 1144   bits: 11/11
c ---[  56]---> Adder-cost: 2026   maxlim: 1169   bits: 11/11
c ---[  54]---> Adder-cost: 306   maxlim: 1169   bits: 11/11
c ---[  52]---> Adder-cost: 2014   maxlim: 1197   bits: 11/11
c ---[  50]---> Adder-cost: 2180   maxlim: 1198   bits: 11/11
c ---[  48]---> Adder-cost: 1926   maxlim: 1217   bits: 11/11
c ---[  46]---> Adder-cost: 2222   maxlim: 1228   bits: 11/11
c ---[  44]---> Adder-cost: 2112   maxlim: 1250   bits: 11/11
c ---[  42]---> Adder-cost: 2440   maxlim: 1335   bits: 11/11
c ---[  40]---> Adder-cost: 338   maxlim: 1335   bits: 11/11
c ---[  38]---> Adder-cost: 2418   maxlim: 1341   bits: 11/11
c ---[  36]---> Adder-cost: 3050   maxlim: 1694   bits: 11/11
c ---[  34]---> Adder-cost: 3128   maxlim: 1702   bits: 11/11
c ---[  32]---> Adder-cost: 3030   maxlim: 1714   bits: 11/11
c ---[  30]---> Adder-cost: 2712   maxlim: 1759   bits: 11/11
c ---[  28]---> Adder-cost: 3316   maxlim: 1795   bits: 11/11
c ---[  26]---> Adder-cost: 2958   maxlim: 1810   bits: 11/11
c ---[  24]---> Adder-cost: 3036   maxlim: 1891   bits: 11/11
c ---[  22]---> Adder-cost: 3056   maxlim: 1914   bits: 11/11
c ---[  20]---> Adder-cost: 3822   maxlim: 1972   bits: 11/11
c ---[  18]---> Adder-cost: 454   maxlim: 1972   bits: 11/11
c ---[  16]---> Adder-cost: 3080   maxlim: 2048   bits: 12/12
c ---[  14]---> Adder-cost: 3030   maxlim: 2054   bits: 12/12
c ---[  12]---> Adder-cost: 3504   maxlim: 2082   bits: 12/12
c ---[  10]---> Adder-cost: 3520   maxlim: 2112   bits: 12/12
c ---[   8]---> Adder-cost: 4242   maxlim: 2482   bits: 12/12
c ---[   6]---> Adder-cost: 4452   maxlim: 2820   bits: 12/12
c ---[   4]---> Adder-cost: 5260   maxlim: 2954   bits: 12/12
c ---[   2]---> Adder-cost: 5882   maxlim: 3755   bits: 12/12
c ---[   0]---> Adder-cost: 6252   maxlim: 3859   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  995018  3552570 |  331672       0        0     nan |  0.000 % |
c |       100 |  995003  3552517 |  364839      98      303     3.1 |  0.730 % |
c |       250 |  993687  3547825 |  401323      69      214     3.1 |  0.878 % |
c |       475 |  992040  3541944 |  441455      65      207     3.2 |  1.060 % |
c |       813 |  989819  3534095 |  485600     114      386     3.4 |  1.312 % |
c |      1319 |  986197  3521253 |  534161     167      553     3.3 |  1.725 % |
c |      2078 |  981160  3503342 |  587577     246      792     3.2 |  2.283 % |
c |      3217 |  973016  3474375 |  646334     349     1199     3.4 |  3.172 % |
c |      4926 |  963065  3439004 |  710968     774     2872     3.7 |  4.266 % |
c |      7488 |  953112  3403712 |  782065    2013     9586     4.8 |  5.355 % |
#### 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.91 0.95 0.69 2/56 26488
Raw data (stat): 26488 (runsolver) R 26487 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 372528093 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+9.99978 s]
Raw data (loadavg): 0.93 0.95 0.69 2/56 26488
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17107 0 0 0 958 41 0 0 25 0 1 0 372528093 79618048 16723 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19438 16723 603 41 0 19397 0
vsize: 77752
[startup+20.005 s]
Raw data (loadavg): 0.94 0.95 0.69 2/56 26488
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17129 0 0 0 1959 41 0 0 25 0 1 0 372528093 79618048 16745 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19438 16745 603 41 0 19397 0
vsize: 77752
[startup+30.0053 s]
Raw data (loadavg): 0.95 0.96 0.70 2/56 26488
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17186 0 0 0 2959 41 0 0 25 0 1 0 372528093 79912960 16802 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19510 16802 603 41 0 19469 0
vsize: 78040
[startup+40.0051 s]
Raw data (loadavg): 0.95 0.96 0.70 2/56 26488
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17215 0 0 0 3958 41 0 0 25 0 1 0 372528093 80048128 16831 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19543 16831 603 41 0 19502 0
vsize: 78172
[startup+50.0063 s]
Raw data (loadavg): 0.96 0.96 0.70 2/56 26488
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17247 0 0 0 4958 41 0 0 25 0 1 0 372528093 80183296 16863 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19576 16863 603 41 0 19535 0
vsize: 78304
[startup+60.0067 s]
Raw data (loadavg): 0.97 0.96 0.71 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17288 0 0 0 5958 42 0 0 25 0 1 0 372528093 80326656 16904 4294967295 134512640 134672761 3221224576 3221223764 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19611 16904 603 41 0 19570 0
vsize: 78444
[startup+70.0065 s]
Raw data (loadavg): 0.97 0.96 0.71 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17339 0 0 0 6958 42 0 0 25 0 1 0 372528093 80461824 16955 4294967295 134512640 134672761 3221224576 3221223748 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19644 16955 603 41 0 19603 0
vsize: 78576
[startup+80.0076 s]
Raw data (loadavg): 0.98 0.96 0.71 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17373 0 0 0 7958 42 0 0 25 0 1 0 372528093 80732160 16989 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19710 16989 603 41 0 19669 0
vsize: 78840
[startup+90.007 s]
Raw data (loadavg): 0.98 0.96 0.71 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17394 0 0 0 8958 42 0 0 25 0 1 0 372528093 80732160 17010 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19710 17010 603 41 0 19669 0
vsize: 78840
[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.72 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17420 0 0 0 9958 43 0 0 25 0 1 0 372528093 80867328 17036 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19743 17036 603 41 0 19702 0
vsize: 78972
[startup+110.009 s]
Raw data (loadavg): 0.98 0.96 0.72 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17465 0 0 0 10958 43 0 0 25 0 1 0 372528093 81002496 17081 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19776 17081 603 41 0 19735 0
vsize: 79104
[startup+120.009 s]
Raw data (loadavg): 0.99 0.96 0.72 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17484 0 0 0 11958 43 0 0 25 0 1 0 372528093 81137664 17100 4294967295 134512640 134672761 3221224576 3221223748 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19809 17100 603 41 0 19768 0
vsize: 79236
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.73 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17519 0 0 0 12958 43 0 0 25 0 1 0 372528093 81272832 17135 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19842 17135 603 41 0 19801 0
vsize: 79368
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.73 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17545 0 0 0 13958 43 0 0 25 0 1 0 372528093 81408000 17161 4294967295 134512640 134672761 3221224576 3221223748 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19875 17161 603 41 0 19834 0
vsize: 79500
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17570 0 0 0 14958 43 0 0 25 0 1 0 372528093 81408000 17186 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19875 17186 603 41 0 19834 0
vsize: 79500
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17610 0 0 0 15958 44 0 0 25 0 1 0 372528093 81739776 17226 4294967295 134512640 134672761 3221224576 3221223792 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19956 17226 603 41 0 19915 0
vsize: 79824
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.73 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17610 0 0 0 16958 44 0 0 25 0 1 0 372528093 81739776 17226 4294967295 134512640 134672761 3221224576 3221223768 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19956 17226 603 41 0 19915 0
vsize: 79824
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.74 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17616 0 0 0 17957 44 0 0 25 0 1 0 372528093 81739776 17232 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19956 17232 603 41 0 19915 0
vsize: 79824
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.74 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17635 0 0 0 18957 44 0 0 25 0 1 0 372528093 81739776 17251 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19956 17251 603 41 0 19915 0
vsize: 79824
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17667 0 0 0 19957 45 0 0 25 0 1 0 372528093 81874944 17283 4294967295 134512640 134672761 3221224576 3221223748 134556664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19989 17283 603 41 0 19948 0
vsize: 79956
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17694 0 0 0 20957 45 0 0 25 0 1 0 372528093 82010112 17310 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20022 17310 603 41 0 19981 0
vsize: 80088
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17718 0 0 0 21957 45 0 0 25 0 1 0 372528093 82145280 17334 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20055 17334 603 41 0 20014 0
vsize: 80220
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.75 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17726 0 0 0 22956 45 0 0 25 0 1 0 372528093 82145280 17342 4294967295 134512640 134672761 3221224576 3221223748 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20055 17342 603 41 0 20014 0
vsize: 80220
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.75 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17753 0 0 0 23956 45 0 0 25 0 1 0 372528093 82145280 17369 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20055 17369 603 41 0 20014 0
vsize: 80220
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17760 0 0 0 24956 46 0 0 25 0 1 0 372528093 82280448 17376 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20088 17376 603 41 0 20047 0
vsize: 80352
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17770 0 0 0 25957 46 0 0 25 0 1 0 372528093 82280448 17386 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20088 17386 603 41 0 20047 0
vsize: 80352
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17790 0 0 0 26957 46 0 0 25 0 1 0 372528093 82280448 17406 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20088 17406 603 41 0 20047 0
vsize: 80352
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17793 0 0 0 27956 46 0 0 25 0 1 0 372528093 82415616 17409 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20121 17409 603 41 0 20080 0
vsize: 80484
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17800 0 0 0 28956 46 0 0 25 0 1 0 372528093 82415616 17416 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20121 17416 603 41 0 20080 0
vsize: 80484
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17813 0 0 0 29956 47 0 0 25 0 1 0 372528093 82415616 17429 4294967295 134512640 134672761 3221224576 3221223820 134564424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20121 17429 603 41 0 20080 0
vsize: 80484
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.76 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17827 0 0 0 30956 47 0 0 25 0 1 0 372528093 82550784 17443 4294967295 134512640 134672761 3221224576 3221223792 134557646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20154 17443 603 41 0 20113 0
vsize: 80616
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17828 0 0 0 31956 47 0 0 25 0 1 0 372528093 82550784 17444 4294967295 134512640 134672761 3221224576 3221223748 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20154 17444 603 41 0 20113 0
vsize: 80616
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.77 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17838 0 0 0 32956 47 0 0 25 0 1 0 372528093 82550784 17454 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20154 17454 603 41 0 20113 0
vsize: 80616
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.77 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17850 0 0 0 33956 47 0 0 25 0 1 0 372528093 82550784 17466 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20154 17466 603 41 0 20113 0
vsize: 80616
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/56 26490
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17858 0 0 0 34956 47 0 0 25 0 1 0 372528093 82550784 17474 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20154 17474 603 41 0 20113 0
vsize: 80616
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17866 0 0 0 35956 48 0 0 25 0 1 0 372528093 82685952 17482 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20187 17482 603 41 0 20146 0
vsize: 80748
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17877 0 0 0 36956 48 0 0 25 0 1 0 372528093 82685952 17493 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20187 17493 603 41 0 20146 0
vsize: 80748
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.78 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17885 0 0 0 37956 48 0 0 25 0 1 0 372528093 82685952 17501 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20187 17501 603 41 0 20146 0
vsize: 80748
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.78 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17889 0 0 0 38956 48 0 0 25 0 1 0 372528093 82685952 17505 4294967295 134512640 134672761 3221224576 3221223792 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20187 17505 603 41 0 20146 0
vsize: 80748
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.78 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17900 0 0 0 39956 48 0 0 25 0 1 0 372528093 82685952 17516 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20187 17516 603 41 0 20146 0
vsize: 80748
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.78 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17904 0 0 0 40956 48 0 0 25 0 1 0 372528093 82821120 17520 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17520 603 41 0 20179 0
vsize: 80880
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.78 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17908 0 0 0 41956 48 0 0 25 0 1 0 372528093 82821120 17524 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17524 603 41 0 20179 0
vsize: 80880
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.79 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17911 0 0 0 42956 48 0 0 25 0 1 0 372528093 82821120 17527 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17527 603 41 0 20179 0
vsize: 80880
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.79 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17922 0 0 0 43956 49 0 0 25 0 1 0 372528093 82821120 17538 4294967295 134512640 134672761 3221224576 3221223744 134564648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17538 603 41 0 20179 0
vsize: 80880
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.79 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17927 0 0 0 44956 49 0 0 25 0 1 0 372528093 82821120 17543 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17543 603 41 0 20179 0
vsize: 80880
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17936 0 0 0 45956 49 0 0 25 0 1 0 372528093 82821120 17552 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17552 603 41 0 20179 0
vsize: 80880
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.79 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17940 0 0 0 46956 49 0 0 25 0 1 0 372528093 82821120 17556 4294967295 134512640 134672761 3221224576 3221223728 134565134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17556 603 41 0 20179 0
vsize: 80880
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.79 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17943 0 0 0 47956 49 0 0 25 0 1 0 372528093 82821120 17559 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17559 603 41 0 20179 0
vsize: 80880
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.80 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17949 0 0 0 48956 50 0 0 25 0 1 0 372528093 82821120 17565 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17565 603 41 0 20179 0
vsize: 80880
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17949 0 0 0 49956 50 0 0 25 0 1 0 372528093 82821120 17565 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 17565 603 41 0 20179 0
vsize: 80880
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17955 0 0 0 50956 50 0 0 25 0 1 0 372528093 82956288 17571 4294967295 134512640 134672761 3221224576 3221223748 134556609 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20253 17571 603 41 0 20212 0
vsize: 81012
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.80 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17993 0 0 0 51956 50 0 0 25 0 1 0 372528093 83218432 17609 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17609 603 41 0 20276 0
vsize: 81268
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.80 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17993 0 0 0 52956 50 0 0 25 0 1 0 372528093 83218432 17609 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17609 603 41 0 20276 0
vsize: 81268
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.81 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17993 0 0 0 53956 50 0 0 25 0 1 0 372528093 83218432 17609 4294967295 134512640 134672761 3221224576 3221223760 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17609 603 41 0 20276 0
vsize: 81268
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17993 0 0 0 54956 50 0 0 25 0 1 0 372528093 83218432 17609 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17609 603 41 0 20276 0
vsize: 81268
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.81 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17993 0 0 0 55956 51 0 0 25 0 1 0 372528093 83218432 17609 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17609 603 41 0 20276 0
vsize: 81268
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.81 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17993 0 0 0 56956 51 0 0 25 0 1 0 372528093 83218432 17609 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17609 603 41 0 20276 0
vsize: 81268
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.81 2/56 26492
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17994 0 0 0 57956 51 0 0 25 0 1 0 372528093 83218432 17610 4294967295 134512640 134672761 3221224576 3221223776 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17610 603 41 0 20276 0
vsize: 81268
[startup+590.021 s]
Raw data (loadavg): 1.07 0.99 0.82 2/56 26545
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17995 0 0 0 58955 51 0 0 25 0 1 0 372528093 83218432 17611 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20317 17611 603 41 0 20276 0
vsize: 81268
[startup+600.022 s]
Raw data (loadavg): 1.06 0.99 0.82 2/56 26545
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17995 0 0 0 59955 51 0 0 25 0 1 0 372528093 83218432 17611 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20317 17611 603 41 0 20276 0
vsize: 81268
[startup+610.022 s]
Raw data (loadavg): 1.05 0.99 0.82 2/56 26545
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17996 0 0 0 60955 51 0 0 25 0 1 0 372528093 83218432 17612 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20317 17612 603 41 0 20276 0
vsize: 81268
[startup+620.022 s]
Raw data (loadavg): 1.04 0.99 0.82 2/56 26545
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 17996 0 0 0 61956 51 0 0 25 0 1 0 372528093 83218432 17612 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20317 17612 603 41 0 20276 0
vsize: 81268
[startup+630.021 s]
Raw data (loadavg): 1.04 0.99 0.83 2/56 26545
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18000 0 0 0 62956 51 0 0 25 0 1 0 372528093 83218432 17616 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20317 17616 603 41 0 20276 0
vsize: 81268
[startup+640.021 s]
Raw data (loadavg): 1.03 0.99 0.83 2/56 26545
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18000 0 0 0 63956 51 0 0 25 0 1 0 372528093 83218432 17616 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20317 17616 603 41 0 20276 0
vsize: 81268
[startup+650.022 s]
Raw data (loadavg): 1.03 0.99 0.83 2/56 26547
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18002 0 0 0 64955 52 0 0 25 0 1 0 372528093 83218432 17618 4294967295 134512640 134672761 3221224576 3221223744 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17618 603 41 0 20276 0
vsize: 81268
[startup+660.022 s]
Raw data (loadavg): 1.02 0.99 0.83 2/56 26549
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18002 0 0 0 65955 53 0 0 25 0 1 0 372528093 83218432 17618 4294967295 134512640 134672761 3221224576 3221223768 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17618 603 41 0 20276 0
vsize: 81268
[startup+670.022 s]
Raw data (loadavg): 1.02 0.99 0.83 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18003 0 0 0 66955 53 0 0 25 0 1 0 372528093 83218432 17619 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17619 603 41 0 20276 0
vsize: 81268
[startup+680.021 s]
Raw data (loadavg): 1.01 0.99 0.83 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18007 0 0 0 67955 53 0 0 25 0 1 0 372528093 83218432 17623 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17623 603 41 0 20276 0
vsize: 81268
[startup+690.021 s]
Raw data (loadavg): 1.01 0.99 0.83 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18007 0 0 0 68955 53 0 0 25 0 1 0 372528093 83218432 17623 4294967295 134512640 134672761 3221224576 3221223760 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17623 603 41 0 20276 0
vsize: 81268
[startup+700.022 s]
Raw data (loadavg): 1.01 0.99 0.83 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18018 0 0 0 69955 53 0 0 25 0 1 0 372528093 83218432 17634 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17634 603 41 0 20276 0
vsize: 81268
[startup+710.023 s]
Raw data (loadavg): 1.01 0.99 0.83 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18018 0 0 0 70955 53 0 0 25 0 1 0 372528093 83218432 17634 4294967295 134512640 134672761 3221224576 3221223748 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17634 603 41 0 20276 0
vsize: 81268
[startup+720.023 s]
Raw data (loadavg): 1.01 0.99 0.83 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18019 0 0 0 71955 53 0 0 25 0 1 0 372528093 83218432 17635 4294967295 134512640 134672761 3221224576 3221223744 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17635 603 41 0 20276 0
vsize: 81268
[startup+730.022 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18019 0 0 0 72955 54 0 0 25 0 1 0 372528093 83218432 17635 4294967295 134512640 134672761 3221224576 3221223772 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17635 603 41 0 20276 0
vsize: 81268
[startup+740.022 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18022 0 0 0 73955 54 0 0 25 0 1 0 372528093 83218432 17638 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17638 603 41 0 20276 0
vsize: 81268
[startup+750.023 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18023 0 0 0 74955 54 0 0 25 0 1 0 372528093 83218432 17639 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17639 603 41 0 20276 0
vsize: 81268
[startup+760.023 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18024 0 0 0 75955 54 0 0 25 0 1 0 372528093 83218432 17640 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17640 603 41 0 20276 0
vsize: 81268
[startup+770.023 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18026 0 0 0 76955 54 0 0 25 0 1 0 372528093 83218432 17642 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17642 603 41 0 20276 0
vsize: 81268
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18028 0 0 0 77955 54 0 0 25 0 1 0 372528093 83218432 17644 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17644 603 41 0 20276 0
vsize: 81268
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18030 0 0 0 78955 54 0 0 25 0 1 0 372528093 83218432 17646 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17646 603 41 0 20276 0
vsize: 81268
[startup+800.024 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18032 0 0 0 79955 55 0 0 25 0 1 0 372528093 83218432 17648 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17648 603 41 0 20276 0
vsize: 81268
[startup+810.025 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18038 0 0 0 80955 55 0 0 25 0 1 0 372528093 83218432 17654 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17654 603 41 0 20276 0
vsize: 81268
[startup+820.024 s]
Raw data (loadavg): 1.00 0.99 0.84 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18038 0 0 0 81955 55 0 0 25 0 1 0 372528093 83218432 17654 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17654 603 41 0 20276 0
vsize: 81268
[startup+830.025 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18040 0 0 0 82955 55 0 0 25 0 1 0 372528093 83218432 17656 4294967295 134512640 134672761 3221224576 3221223744 134560788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17656 603 41 0 20276 0
vsize: 81268
[startup+840.025 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18040 0 0 0 83955 55 0 0 25 0 1 0 372528093 83218432 17656 4294967295 134512640 134672761 3221224576 3221223728 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17656 603 41 0 20276 0
vsize: 81268
[startup+850.026 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18040 0 0 0 84956 55 0 0 25 0 1 0 372528093 83218432 17656 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17656 603 41 0 20276 0
vsize: 81268
[startup+860.026 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18040 0 0 0 85956 55 0 0 25 0 1 0 372528093 83218432 17656 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17656 603 41 0 20276 0
vsize: 81268
[startup+870.025 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18040 0 0 0 86956 55 0 0 25 0 1 0 372528093 83218432 17656 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17656 603 41 0 20276 0
vsize: 81268
[startup+880.026 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18040 0 0 0 87956 55 0 0 25 0 1 0 372528093 83218432 17656 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17656 603 41 0 20276 0
vsize: 81268
[startup+890.026 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18040 0 0 0 88956 55 0 0 25 0 1 0 372528093 83218432 17656 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17656 603 41 0 20276 0
vsize: 81268
[startup+900.027 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18042 0 0 0 89956 56 0 0 25 0 1 0 372528093 83218432 17658 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17658 603 41 0 20276 0
vsize: 81268
[startup+910.027 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18047 0 0 0 90956 56 0 0 25 0 1 0 372528093 83218432 17663 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17663 603 41 0 20276 0
vsize: 81268
[startup+920.027 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18047 0 0 0 91956 56 0 0 25 0 1 0 372528093 83218432 17663 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17663 603 41 0 20276 0
vsize: 81268
[startup+930.027 s]
Raw data (loadavg): 1.00 0.99 0.85 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18047 0 0 0 92956 56 0 0 25 0 1 0 372528093 83218432 17663 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17663 603 41 0 20276 0
vsize: 81268
[startup+940.027 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18050 0 0 0 93956 56 0 0 25 0 1 0 372528093 83218432 17666 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17666 603 41 0 20276 0
vsize: 81268
[startup+950.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26551
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18050 0 0 0 94957 56 0 0 25 0 1 0 372528093 83218432 17666 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17666 603 41 0 20276 0
vsize: 81268
[startup+960.039 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18053 0 0 0 95957 57 0 0 25 0 1 0 372528093 83218432 17669 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17669 603 41 0 20276 0
vsize: 81268
[startup+970.039 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18053 0 0 0 96957 57 0 0 25 0 1 0 372528093 83218432 17669 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17669 603 41 0 20276 0
vsize: 81268
[startup+980.041 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18053 0 0 0 97957 57 0 0 25 0 1 0 372528093 83218432 17669 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17669 603 41 0 20276 0
vsize: 81268
[startup+990.041 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18053 0 0 0 98957 57 0 0 25 0 1 0 372528093 83218432 17669 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17669 603 41 0 20276 0
vsize: 81268
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18053 0 0 0 99957 57 0 0 25 0 1 0 372528093 83218432 17669 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17669 603 41 0 20276 0
vsize: 81268
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18056 0 0 0 100957 58 0 0 25 0 1 0 372528093 83218432 17672 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17672 603 41 0 20276 0
vsize: 81268
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18056 0 0 0 101957 58 0 0 25 0 1 0 372528093 83218432 17672 4294967295 134512640 134672761 3221224576 3221223748 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17672 603 41 0 20276 0
vsize: 81268
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.86 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18056 0 0 0 102957 58 0 0 25 0 1 0 372528093 83218432 17672 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17672 603 41 0 20276 0
vsize: 81268
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18056 0 0 0 103957 58 0 0 25 0 1 0 372528093 83218432 17672 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17672 603 41 0 20276 0
vsize: 81268
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18057 0 0 0 104957 59 0 0 25 0 1 0 372528093 83218432 17673 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17673 603 41 0 20276 0
vsize: 81268
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18057 0 0 0 105957 59 0 0 25 0 1 0 372528093 83218432 17673 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17673 603 41 0 20276 0
vsize: 81268
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18057 0 0 0 106957 59 0 0 25 0 1 0 372528093 83218432 17673 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17673 603 41 0 20276 0
vsize: 81268
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18058 0 0 0 107957 59 0 0 25 0 1 0 372528093 83218432 17674 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17674 603 41 0 20276 0
vsize: 81268
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 108957 59 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223748 134556615 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 109957 59 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 110957 59 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 111957 59 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.87 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 112957 59 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223740 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.88 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 113957 59 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.88 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 114957 60 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.88 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 115957 60 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223776 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.88 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 116957 60 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.88 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 117957 60 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223760 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.88 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 118957 60 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.88 2/56 26553
Raw data (stat): 26488 (minisat+) R 26487 12452 12451 0 -1 0 18059 0 0 0 119957 60 0 0 25 0 1 0 372528093 83218432 17675 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20317 17675 603 41 0 20276 0
vsize: 81268
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.88 1/56 26553
Raw data (stat): 26488 (minisat+) Z 26487 12452 12451 0 -1 12 18061 0 0 0 119957 64 0 0 25 0 1 0 372528093 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.08
CPU time (s): 1200.22
CPU user time (s): 1199.58
CPU system time (s): 0.643902
CPU usage (%): 100.012
Max. virtual memory (Kb): 81268
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####