PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-air03.opb
MD5SUM	69337cf8d2b6f6cf8cc02fedc291ffcc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	199890
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	1189.44
Number of variables	10757
Total number of constraints	10881
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	10881
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	3861
Trace number 21467

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 23:55:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13166 boxname=wulflinc1 idbench=1013 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69337cf8d2b6f6cf8cc02fedc291ffcc  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-air03.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-air03.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-air03.opb
IDLAUNCH: 13166
/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:        654024 kB
Buffers:          3068 kB
Cached:         352368 kB
SwapCached:          0 kB
Active:         107356 kB
Inactive:       251240 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        653772 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           7172 kB
Slab:            16024 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:15:05 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 13166 7 1200.25 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): (none)
c ---[ 246]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 244]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 242]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 240]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 238]---> Adder-cost: 6   maxlim: 4   bits: 3/3
c ---[ 236]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 234]---> Adder-cost: 16   maxlim: 10   bits: 4/4
c ---[ 232]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 230]---> Adder-cost: 10   maxlim: 11   bits: 4/4
c ---[ 228]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 226]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 224]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[ 222]---> Adder-cost: 44   maxlim: 30   bits: 5/5
c ---[ 220]---> Adder-cost: 18   maxlim: 30   bits: 5/5
c ---[ 218]---> Adder-cost: 50   maxlim: 30   bits: 5/5
c ---[ 216]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 214]---> Adder-cost: 78   maxlim: 41   bits: 6/6
c ---[ 212]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[ 210]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 208]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[ 206]---> Adder-cost: 72   maxlim: 57   bits: 6/6
c ---[ 204]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 202]---> Adder-cost: 78   maxlim: 61   bits: 6/6
c ---[ 200]---> Adder-cost: 140   maxlim: 72   bits: 7/7
c ---[ 198]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[ 196]---> Adder-cost: 48   maxlim: 78   bits: 7/7
c ---[ 194]---> Adder-cost: 172   maxlim: 90   bits: 7/7
c ---[ 192]---> Adder-cost: 158   maxlim: 88   bits: 7/7
c ---[ 190]---> Adder-cost: 196   maxlim: 101   bits: 7/7
c ---[ 188]---> Adder-cost: 226   maxlim: 117   bits: 7/7
c ---[ 186]---> Adder-cost: 62   maxlim: 117   bits: 7/7
c ---[ 184]---> Adder-cost: 232   maxlim: 122   bits: 7/7
c ---[ 182]---> Adder-cost: 262   maxlim: 133   bits: 8/8
c ---[ 180]---> Adder-cost: 258   maxlim: 136   bits: 8/8
c ---[ 178]---> Adder-cost: 224   maxlim: 115   bits: 7/7
c ---[ 176]---> Adder-cost: 62   maxlim: 115   bits: 7/7
c ---[ 174]---> Adder-cost: 290   maxlim: 150   bits: 8/8
c ---[ 172]---> Adder-cost: 304   maxlim: 155   bits: 8/8
c ---[ 170]---> Adder-cost: 298   maxlim: 156   bits: 8/8
c ---[ 168]---> Adder-cost: 230   maxlim: 167   bits: 8/8
c ---[ 166]---> Adder-cost: 220   maxlim: 169   bits: 8/8
c ---[ 164]---> Adder-cost: 338   maxlim: 178   bits: 8/8
c ---[ 162]---> Adder-cost: 346   maxlim: 179   bits: 8/8
c ---[ 160]---> Adder-cost: 344   maxlim: 185   bits: 8/8
c ---[ 158]---> Adder-cost: 438   maxlim: 224   bits: 8/8
c ---[ 156]---> Adder-cost: 456   maxlim: 234   bits: 8/8
c ---[ 154]---> Adder-cost: 462   maxlim: 238   bits: 8/8
c ---[ 152]---> Adder-cost: 474   maxlim: 242   bits: 8/8
c ---[ 150]---> Adder-cost: 114   maxlim: 242   bits: 8/8
c ---[ 148]---> Adder-cost: 538   maxlim: 277   bits: 9/9
c ---[ 146]---> Adder-cost: 120   maxlim: 277   bits: 9/9
c ---[ 144]---> Adder-cost: 654   maxlim: 334   bits: 9/9
c ---[ 142]---> Adder-cost: 666   maxlim: 337   bits: 9/9
c ---[ 140]---> Adder-cost: 642   maxlim: 326   bits: 9/9
c ---[ 138]---> Adder-cost: 674   maxlim: 350   bits: 9/9
c ---[ 136]---> Adder-cost: 544   maxlim: 276   bits: 9/9
c ---[ 134]---> Adder-cost: 804   maxlim: 411   bits: 9/9
c ---[ 132]---> Adder-cost: 820   maxlim: 416   bits: 9/9
c ---[ 130]---> Adder-cost: 842   maxlim: 432   bits: 9/9
c ---[ 128]---> Adder-cost: 828   maxlim: 473   bits: 9/9
c ---[ 126]---> Adder-cost: 756   maxlim: 524   bits: 10/10
c ---[ 124]---> Adder-cost: 1028   maxlim: 553   bits: 10/10
c ---[ 122]---> Adder-cost: 1064   maxlim: 566   bits: 10/10
c ---[ 120]---> Adder-cost: 916   maxlim: 550   bits: 10/10
c ---[ 118]---> Adder-cost: 1020   maxlim: 569   bits: 10/10
c ---[ 116]---> Adder-cost: 1080   maxlim: 600   bits: 10/10
c ---[ 114]---> Adder-cost: 950   maxlim: 569   bits: 10/10
c ---[ 112]---> Adder-cost: 1212   maxlim: 632   bits: 10/10
c ---[ 110]---> Adder-cost: 1104   maxlim: 663   bits: 10/10
c ---[ 108]---> Adder-cost: 1266   maxlim: 676   bits: 10/10
c ---[ 106]---> Adder-cost: 1212   maxlim: 675   bits: 10/10
c ---[ 104]---> Adder-cost: 1276   maxlim: 719   bits: 10/10
c ---[ 102]---> Adder-cost: 1384   maxlim: 745   bits: 10/10
c ---[ 100]---> Adder-cost: 1310   maxlim: 707   bits: 10/10
c ---[  98]---> Adder-cost: 238   maxlim: 707   bits: 10/10
c ---[  96]---> Adder-cost: 1218   maxlim: 794   bits: 10/10
c ---[  94]---> Adder-cost: 1230   maxlim: 679   bits: 10/10
c ---[  92]---> Adder-cost: 1364   maxlim: 854   bits: 10/10
c ---[  90]---> Adder-cost: 1504   maxlim: 768   bits: 10/10
c ---[  88]---> Adder-cost: 1676   maxlim: 917   bits: 10/10
c ---[  86]---> Adder-cost: 258   maxlim: 917   bits: 10/10
c ---[  84]---> Adder-cost: 1668   maxlim: 913   bits: 10/10
c ---[  82]---> Adder-cost: 262   maxlim: 913   bits: 10/10
c ---[  80]---> Adder-cost: 1770   maxlim: 926   bits: 10/10
c ---[  78]---> Adder-cost: 1376   maxlim: 772   bits: 10/10
c ---[  76]---> Adder-cost: 240   maxlim: 772   bits: 10/10
c ---[  74]---> Adder-cost: 1758   maxlim: 979   bits: 10/10
c ---[  72]---> Adder-cost: 968   maxlim: 971   bits: 10/10
c ---[  70]---> Adder-cost: 1536   maxlim: 931   bits: 10/10
c ---[  68]---> Adder-cost: 1712   maxlim: 987   bits: 10/10
c ---[  66]---> Adder-cost: 1794   maxlim: 1019   bits: 10/10
c ---[  64]---> Adder-cost: 1742   maxlim: 1058   bits: 11/11
c ---[  62]---> Adder-cost: 1614   maxlim: 941   bits: 10/10
c ---[  60]---> Adder-cost: 1932   maxlim: 1218   bits: 11/11
c ---[  58]---> Adder-cost: 1278   maxlim: 955   bits: 10/10
c ---[  56]---> Adder-cost: 2032   maxlim: 1198   bits: 11/11
c ---[  54]---> Adder-cost: 2124   maxlim: 1251   bits: 11/11
c ---[  52]---> Adder-cost: 2030   maxlim: 1170   bits: 11/11
c ---[  50]---> Adder-cost: 306   maxlim: 1170   bits: 11/11
c ---[  48]---> Adder-cost: 2424   maxlim: 1342   bits: 11/11
c ---[  46]---> Adder-cost: 2004   maxlim: 1145   bits: 11/11
c ---[  44]---> Adder-cost: 2174   maxlim: 1199   bits: 11/11
c ---[  42]---> Adder-cost: 2214   maxlim: 1229   bits: 11/11
c ---[  40]---> Adder-cost: 2438   maxlim: 1336   bits: 11/11
c ---[  38]---> Adder-cost: 338   maxlim: 1336   bits: 11/11
c ---[  36]---> Adder-cost: 3132   maxlim: 1703   bits: 11/11
c ---[  34]---> Adder-cost: 3032   maxlim: 1715   bits: 11/11
c ---[  32]---> Adder-cost: 2714   maxlim: 1760   bits: 11/11
c ---[  30]---> Adder-cost: 3048   maxlim: 1892   bits: 11/11
c ---[  28]---> Adder-cost: 3062   maxlim: 1915   bits: 11/11
c ---[  26]---> Adder-cost: 3030   maxlim: 1695   bits: 11/11
c ---[  24]---> Adder-cost: 2962   maxlim: 1811   bits: 11/11
c ---[  22]---> Adder-cost: 3048   maxlim: 2055   bits: 12/12
c ---[  20]---> Adder-cost: 3822   maxlim: 1973   bits: 11/11
c ---[  18]---> Adder-cost: 454   maxlim: 1973   bits: 11/11
c ---[  16]---> Adder-cost: 3306   maxlim: 1796   bits: 11/11
c ---[  14]---> Adder-cost: 3062   maxlim: 2049   bits: 12/12
c ---[  12]---> Adder-cost: 3504   maxlim: 2083   bits: 12/12
c ---[  10]---> Adder-cost: 3520   maxlim: 2113   bits: 12/12
c ---[   8]---> Adder-cost: 4242   maxlim: 2483   bits: 12/12
c ---[   6]---> Adder-cost: 4452   maxlim: 2821   bits: 12/12
c ---[   4]---> Adder-cost: 5260   maxlim: 2955   bits: 12/12
c ---[   2]---> Adder-cost: 5882   maxlim: 3756   bits: 12/12
c ---[   0]---> Adder-cost: 6252   maxlim: 3860   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  994582  3549632 |  331527       0        0     nan |  0.000 % |
c |       100 |  993927  3547315 |  364679       7       22     3.1 |  1.533 % |
c |       250 |  993624  3546232 |  401147     115      358     3.1 |  1.566 % |
c |       477 |  992782  3543246 |  441262     218      807     3.7 |  1.656 % |
c |       814 |  990099  3533721 |  485388     158      516     3.3 |  1.945 % |
c |      1320 |  986648  3521520 |  533927     217      717     3.3 |  2.319 % |
c |      2079 |  981344  3502762 |  587320     268      978     3.6 |  2.889 % |
c |      3218 |  973795  3476099 |  646052     488     1716     3.5 |  3.703 % |
c |      4926 |  964350  3442552 |  710657     977     4260     4.4 |  4.718 % |
c |      7488 |  953440  3403916 |  781723    2074    10121     4.9 |  5.868 % |
c |     11333 |  946703  3380059 |  859895    5004    27726     5.5 |  6.585 % |
#### 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.85 0.97 0.92 2/56 6559
Raw data (stat): 6559 (runsolver) R 6558 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 434124819 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+9.99996 s]
Raw data (loadavg): 0.87 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17087 0 0 0 958 40 0 0 25 0 1 0 434124819 79626240 16769 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19440 16769 603 41 0 19399 0
vsize: 77760
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17116 0 0 0 1958 41 0 0 25 0 1 0 434124819 79761408 16798 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19473 16798 603 41 0 19432 0
vsize: 77892
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17188 0 0 0 2958 41 0 0 25 0 1 0 434124819 80052224 16870 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19544 16870 603 41 0 19503 0
vsize: 78176
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17250 0 0 0 3958 41 0 0 25 0 1 0 434124819 80375808 16932 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19623 16932 603 41 0 19582 0
vsize: 78492
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17292 0 0 0 4958 42 0 0 25 0 1 0 434124819 80510976 16974 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19656 16974 603 41 0 19615 0
vsize: 78624
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17340 0 0 0 5958 42 0 0 25 0 1 0 434124819 80646144 17022 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19689 17022 603 41 0 19648 0
vsize: 78756
[startup+70.0037 s]
Raw data (loadavg): 0.95 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17383 0 0 0 6957 42 0 0 25 0 1 0 434124819 80916480 17065 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 17065 603 41 0 19714 0
vsize: 79020
[startup+80.0052 s]
Raw data (loadavg): 0.96 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17417 0 0 0 7957 43 0 0 25 0 1 0 434124819 81051648 17099 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19788 17099 603 41 0 19747 0
vsize: 79152
[startup+90.0052 s]
Raw data (loadavg): 0.96 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17447 0 0 0 8958 43 0 0 25 0 1 0 434124819 81186816 17129 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19821 17129 603 41 0 19780 0
vsize: 79284
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17475 0 0 0 9958 43 0 0 25 0 1 0 434124819 81186816 17157 4294967295 134512640 134672761 3221224544 3221223716 134556664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19821 17157 603 41 0 19780 0
vsize: 79284
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17500 0 0 0 10958 43 0 0 25 0 1 0 434124819 81321984 17182 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19854 17182 603 41 0 19813 0
vsize: 79416
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17528 0 0 0 11958 43 0 0 25 0 1 0 434124819 81457152 17210 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19887 17210 603 41 0 19846 0
vsize: 79548
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17555 0 0 0 12958 43 0 0 25 0 1 0 434124819 81670144 17237 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19939 17237 603 41 0 19898 0
vsize: 79756
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17581 0 0 0 13958 43 0 0 25 0 1 0 434124819 81670144 17263 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19939 17263 603 41 0 19898 0
vsize: 79756
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17617 0 0 0 14958 44 0 0 25 0 1 0 434124819 81805312 17299 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19972 17299 603 41 0 19931 0
vsize: 79888
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17640 0 0 0 15958 44 0 0 25 0 1 0 434124819 81940480 17322 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20005 17322 603 41 0 19964 0
vsize: 80020
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17659 0 0 0 16958 44 0 0 25 0 1 0 434124819 81940480 17341 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20005 17341 603 41 0 19964 0
vsize: 80020
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17675 0 0 0 17958 44 0 0 25 0 1 0 434124819 82075648 17357 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20038 17357 603 41 0 19997 0
vsize: 80152
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17689 0 0 0 18958 44 0 0 25 0 1 0 434124819 82075648 17371 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20038 17371 603 41 0 19997 0
vsize: 80152
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17710 0 0 0 19958 44 0 0 25 0 1 0 434124819 82210816 17392 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20071 17392 603 41 0 20030 0
vsize: 80284
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17734 0 0 0 20957 45 0 0 25 0 1 0 434124819 82210816 17416 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20071 17416 603 41 0 20030 0
vsize: 80284
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17746 0 0 0 21957 45 0 0 25 0 1 0 434124819 82345984 17428 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20104 17428 603 41 0 20063 0
vsize: 80416
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17763 0 0 0 22958 45 0 0 25 0 1 0 434124819 82345984 17445 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20104 17445 603 41 0 20063 0
vsize: 80416
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17781 0 0 0 23958 45 0 0 25 0 1 0 434124819 82481152 17463 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17463 603 41 0 20096 0
vsize: 80548
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17792 0 0 0 24958 45 0 0 25 0 1 0 434124819 82481152 17474 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17474 603 41 0 20096 0
vsize: 80548
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17801 0 0 0 25958 45 0 0 25 0 1 0 434124819 82481152 17483 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17483 603 41 0 20096 0
vsize: 80548
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17810 0 0 0 26958 45 0 0 25 0 1 0 434124819 82481152 17492 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17492 603 41 0 20096 0
vsize: 80548
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17822 0 0 0 27958 46 0 0 25 0 1 0 434124819 82616320 17504 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20170 17504 603 41 0 20129 0
vsize: 80680
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6559
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17832 0 0 0 28958 46 0 0 25 0 1 0 434124819 82616320 17514 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20170 17514 603 41 0 20129 0
vsize: 80680
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/56 6561
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17851 0 0 0 29958 46 0 0 25 0 1 0 434124819 82751488 17533 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17533 603 41 0 20162 0
vsize: 80812
[startup+310.01 s]
Raw data (loadavg): 1.07 0.99 0.92 2/56 6614
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17859 0 0 0 30956 47 0 0 25 0 1 0 434124819 82751488 17541 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 17541 603 41 0 20162 0
vsize: 80812
[startup+320.01 s]
Raw data (loadavg): 1.06 0.99 0.92 2/56 6614
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17871 0 0 0 31956 47 0 0 25 0 1 0 434124819 82751488 17553 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 17553 603 41 0 20162 0
vsize: 80812
[startup+330.01 s]
Raw data (loadavg): 1.05 0.99 0.92 2/56 6614
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17879 0 0 0 32957 47 0 0 25 0 1 0 434124819 82751488 17561 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 17561 603 41 0 20162 0
vsize: 80812
[startup+340.01 s]
Raw data (loadavg): 1.04 0.99 0.92 2/56 6614
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17887 0 0 0 33957 47 0 0 25 0 1 0 434124819 82751488 17569 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 17569 603 41 0 20162 0
vsize: 80812
[startup+350.01 s]
Raw data (loadavg): 1.03 0.99 0.92 2/56 6614
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17892 0 0 0 34957 47 0 0 25 0 1 0 434124819 82886656 17574 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20236 17574 603 41 0 20195 0
vsize: 80944
[startup+360.01 s]
Raw data (loadavg): 1.03 0.99 0.92 2/56 6616
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17895 0 0 0 35956 48 0 0 25 0 1 0 434124819 82886656 17577 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17577 603 41 0 20195 0
vsize: 80944
[startup+370.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/56 6616
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17905 0 0 0 36956 48 0 0 25 0 1 0 434124819 82886656 17587 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17587 603 41 0 20195 0
vsize: 80944
[startup+380.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17912 0 0 0 37956 48 0 0 25 0 1 0 434124819 82886656 17594 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17594 603 41 0 20195 0
vsize: 80944
[startup+390.011 s]
Raw data (loadavg): 1.02 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17919 0 0 0 38956 48 0 0 25 0 1 0 434124819 82886656 17601 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17601 603 41 0 20195 0
vsize: 80944
[startup+400.012 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17927 0 0 0 39956 48 0 0 25 0 1 0 434124819 82886656 17609 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17609 603 41 0 20195 0
vsize: 80944
[startup+410.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17932 0 0 0 40956 49 0 0 25 0 1 0 434124819 83021824 17614 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20269 17614 603 41 0 20228 0
vsize: 81076
[startup+420.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17933 0 0 0 41956 49 0 0 25 0 1 0 434124819 83021824 17615 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20269 17615 603 41 0 20228 0
vsize: 81076
[startup+430.012 s]
Raw data (loadavg): 1.01 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17936 0 0 0 42955 49 0 0 25 0 1 0 434124819 83021824 17618 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20269 17618 603 41 0 20228 0
vsize: 81076
[startup+440.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17973 0 0 0 43955 50 0 0 25 0 1 0 434124819 83283968 17655 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17655 603 41 0 20292 0
vsize: 81332
[startup+450.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17977 0 0 0 44955 50 0 0 25 0 1 0 434124819 83283968 17659 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+460.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17977 0 0 0 45956 50 0 0 25 0 1 0 434124819 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+470.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17977 0 0 0 46956 50 0 0 25 0 1 0 434124819 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+480.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17977 0 0 0 47956 50 0 0 25 0 1 0 434124819 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+490.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17977 0 0 0 48956 50 0 0 25 0 1 0 434124819 83283968 17659 4294967295 134512640 134672761 3221224544 3221223712 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+500.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17977 0 0 0 49956 50 0 0 25 0 1 0 434124819 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+510.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17984 0 0 0 50956 50 0 0 25 0 1 0 434124819 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17666 603 41 0 20292 0
vsize: 81332
[startup+520.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17984 0 0 0 51956 50 0 0 25 0 1 0 434124819 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17666 603 41 0 20292 0
vsize: 81332
[startup+530.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17984 0 0 0 52956 51 0 0 25 0 1 0 434124819 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17666 603 41 0 20292 0
vsize: 81332
[startup+540.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17985 0 0 0 53956 51 0 0 25 0 1 0 434124819 83283968 17667 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17667 603 41 0 20292 0
vsize: 81332
[startup+550.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17989 0 0 0 54956 51 0 0 25 0 1 0 434124819 83283968 17671 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17671 603 41 0 20292 0
vsize: 81332
[startup+560.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17989 0 0 0 55956 51 0 0 25 0 1 0 434124819 83283968 17671 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17671 603 41 0 20292 0
vsize: 81332
[startup+570.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17989 0 0 0 56956 51 0 0 25 0 1 0 434124819 83283968 17671 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17671 603 41 0 20292 0
vsize: 81332
[startup+580.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17994 0 0 0 57956 51 0 0 25 0 1 0 434124819 83283968 17676 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17676 603 41 0 20292 0
vsize: 81332
[startup+590.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6618
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17994 0 0 0 58956 52 0 0 25 0 1 0 434124819 83283968 17676 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17676 603 41 0 20292 0
vsize: 81332
[startup+600.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17996 0 0 0 59956 52 0 0 25 0 1 0 434124819 83283968 17678 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17678 603 41 0 20292 0
vsize: 81332
[startup+610.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 17998 0 0 0 60956 52 0 0 25 0 1 0 434124819 83283968 17680 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17680 603 41 0 20292 0
vsize: 81332
[startup+620.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18001 0 0 0 61956 52 0 0 25 0 1 0 434124819 83283968 17683 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17683 603 41 0 20292 0
vsize: 81332
[startup+630.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18004 0 0 0 62956 52 0 0 25 0 1 0 434124819 83283968 17686 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17686 603 41 0 20292 0
vsize: 81332
[startup+640.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18006 0 0 0 63956 52 0 0 25 0 1 0 434124819 83283968 17688 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17688 603 41 0 20292 0
vsize: 81332
[startup+650.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18006 0 0 0 64956 52 0 0 25 0 1 0 434124819 83283968 17688 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17688 603 41 0 20292 0
vsize: 81332
[startup+660.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18008 0 0 0 65956 52 0 0 25 0 1 0 434124819 83283968 17690 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17690 603 41 0 20292 0
vsize: 81332
[startup+670.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18009 0 0 0 66958 52 0 0 25 0 1 0 434124819 83283968 17691 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17691 603 41 0 20292 0
vsize: 81332
[startup+680.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18013 0 0 0 67958 53 0 0 25 0 1 0 434124819 83283968 17695 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17695 603 41 0 20292 0
vsize: 81332
[startup+690.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18014 0 0 0 68958 53 0 0 25 0 1 0 434124819 83283968 17696 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17696 603 41 0 20292 0
vsize: 81332
[startup+700.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18015 0 0 0 69958 53 0 0 25 0 1 0 434124819 83283968 17697 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17697 603 41 0 20292 0
vsize: 81332
[startup+710.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18015 0 0 0 70958 53 0 0 25 0 1 0 434124819 83283968 17697 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17697 603 41 0 20292 0
vsize: 81332
[startup+720.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18015 0 0 0 71958 53 0 0 25 0 1 0 434124819 83283968 17697 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17697 603 41 0 20292 0
vsize: 81332
[startup+730.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18016 0 0 0 72958 53 0 0 25 0 1 0 434124819 83283968 17698 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17698 603 41 0 20292 0
vsize: 81332
[startup+740.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18016 0 0 0 73958 53 0 0 25 0 1 0 434124819 83283968 17698 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17698 603 41 0 20292 0
vsize: 81332
[startup+750.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18018 0 0 0 74958 54 0 0 25 0 1 0 434124819 83283968 17700 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17700 603 41 0 20292 0
vsize: 81332
[startup+760.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18018 0 0 0 75958 54 0 0 25 0 1 0 434124819 83283968 17700 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17700 603 41 0 20292 0
vsize: 81332
[startup+770.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18023 0 0 0 76959 54 0 0 25 0 1 0 434124819 83283968 17705 4294967295 134512640 134672761 3221224544 3221223708 134564537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17705 603 41 0 20292 0
vsize: 81332
[startup+780.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18025 0 0 0 77958 54 0 0 25 0 1 0 434124819 83283968 17707 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17707 603 41 0 20292 0
vsize: 81332
[startup+790.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18027 0 0 0 78958 54 0 0 25 0 1 0 434124819 83283968 17709 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17709 603 41 0 20292 0
vsize: 81332
[startup+800.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18027 0 0 0 79958 54 0 0 25 0 1 0 434124819 83283968 17709 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17709 603 41 0 20292 0
vsize: 81332
[startup+810.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18028 0 0 0 80958 54 0 0 25 0 1 0 434124819 83283968 17710 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17710 603 41 0 20292 0
vsize: 81332
[startup+820.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18028 0 0 0 81959 54 0 0 25 0 1 0 434124819 83283968 17710 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17710 603 41 0 20292 0
vsize: 81332
[startup+830.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18029 0 0 0 82959 54 0 0 25 0 1 0 434124819 83283968 17711 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17711 603 41 0 20292 0
vsize: 81332
[startup+840.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18029 0 0 0 83959 54 0 0 25 0 1 0 434124819 83283968 17711 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17711 603 41 0 20292 0
vsize: 81332
[startup+850.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18030 0 0 0 84959 54 0 0 25 0 1 0 434124819 83283968 17712 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17712 603 41 0 20292 0
vsize: 81332
[startup+860.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18035 0 0 0 85959 54 0 0 25 0 1 0 434124819 83283968 17717 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17717 603 41 0 20292 0
vsize: 81332
[startup+870.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18039 0 0 0 86959 54 0 0 25 0 1 0 434124819 83283968 17721 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+880.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18039 0 0 0 87959 55 0 0 25 0 1 0 434124819 83283968 17721 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+890.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6620
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18039 0 0 0 88959 55 0 0 25 0 1 0 434124819 83283968 17721 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+900.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18039 0 0 0 89959 55 0 0 25 0 1 0 434124819 83283968 17721 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+910.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18039 0 0 0 90959 56 0 0 25 0 1 0 434124819 83283968 17721 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+920.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18041 0 0 0 91959 56 0 0 25 0 1 0 434124819 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+930.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18041 0 0 0 92959 56 0 0 25 0 1 0 434124819 83283968 17723 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+940.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18041 0 0 0 93959 56 0 0 25 0 1 0 434124819 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+950.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18042 0 0 0 94960 56 0 0 25 0 1 0 434124819 83283968 17724 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17724 603 41 0 20292 0
vsize: 81332
[startup+960.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18043 0 0 0 95960 56 0 0 25 0 1 0 434124819 83283968 17725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17725 603 41 0 20292 0
vsize: 81332
[startup+970.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18044 0 0 0 96960 56 0 0 25 0 1 0 434124819 83283968 17726 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17726 603 41 0 20292 0
vsize: 81332
[startup+980.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18044 0 0 0 97960 56 0 0 25 0 1 0 434124819 83283968 17726 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17726 603 41 0 20292 0
vsize: 81332
[startup+990.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18044 0 0 0 98960 56 0 0 25 0 1 0 434124819 83283968 17726 4294967295 134512640 134672761 3221224544 3221223776 134564644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17726 603 41 0 20292 0
vsize: 81332
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18046 0 0 0 99960 56 0 0 25 0 1 0 434124819 83283968 17728 4294967295 134512640 134672761 3221224544 3221223712 134564499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17728 603 41 0 20292 0
vsize: 81332
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18046 0 0 0 100960 57 0 0 25 0 1 0 434124819 83283968 17728 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17728 603 41 0 20292 0
vsize: 81332
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18047 0 0 0 101960 57 0 0 25 0 1 0 434124819 83283968 17729 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17729 603 41 0 20292 0
vsize: 81332
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18047 0 0 0 102960 57 0 0 25 0 1 0 434124819 83283968 17729 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17729 603 41 0 20292 0
vsize: 81332
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18052 0 0 0 103960 57 0 0 25 0 1 0 434124819 83427328 17734 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17734 603 41 0 20327 0
vsize: 81472
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18052 0 0 0 104960 57 0 0 25 0 1 0 434124819 83427328 17734 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17734 603 41 0 20327 0
vsize: 81472
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18053 0 0 0 105961 57 0 0 25 0 1 0 434124819 83427328 17735 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17735 603 41 0 20327 0
vsize: 81472
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18053 0 0 0 106961 57 0 0 25 0 1 0 434124819 83427328 17735 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17735 603 41 0 20327 0
vsize: 81472
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18053 0 0 0 107961 58 0 0 25 0 1 0 434124819 83427328 17735 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17735 603 41 0 20327 0
vsize: 81472
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18055 0 0 0 108961 58 0 0 25 0 1 0 434124819 83427328 17737 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18055 0 0 0 109961 58 0 0 25 0 1 0 434124819 83427328 17737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18055 0 0 0 110961 58 0 0 25 0 1 0 434124819 83427328 17737 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18055 0 0 0 111961 58 0 0 25 0 1 0 434124819 83427328 17737 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18061 0 0 0 112961 58 0 0 25 0 1 0 434124819 83427328 17743 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17743 603 41 0 20327 0
vsize: 81472
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18064 0 0 0 113961 58 0 0 25 0 1 0 434124819 83427328 17746 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17746 603 41 0 20327 0
vsize: 81472
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18065 0 0 0 114961 58 0 0 25 0 1 0 434124819 83427328 17747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17747 603 41 0 20327 0
vsize: 81472
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18066 0 0 0 115961 58 0 0 25 0 1 0 434124819 83427328 17748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17748 603 41 0 20327 0
vsize: 81472
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18069 0 0 0 116961 58 0 0 25 0 1 0 434124819 83427328 17751 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17751 603 41 0 20327 0
vsize: 81472
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18069 0 0 0 117961 59 0 0 25 0 1 0 434124819 83427328 17751 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17751 603 41 0 20327 0
vsize: 81472
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6622
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18073 0 0 0 118962 59 0 0 25 0 1 0 434124819 83427328 17755 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17755 603 41 0 20327 0
vsize: 81472
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/56 6624
Raw data (stat): 6559 (minisat+) R 6558 12452 12451 0 -1 0 18074 0 0 0 119961 59 0 0 25 0 1 0 434124819 83427328 17756 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17756 603 41 0 20327 0
vsize: 81472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.92 1/56 6624
Raw data (stat): 6559 (minisat+) Z 6558 12452 12451 0 -1 12 18076 0 0 0 119961 62 0 0 25 0 1 0 434124819 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.11
CPU time (s): 1200.25
CPU user time (s): 1199.62
CPU system time (s): 0.626904
CPU usage (%): 100.011
Max. virtual memory (Kb): 81472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####