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/miplib/normalized-mps-v2-20-10-air03.opb
MD5SUM	45da6faf70c895e4acc43dda6a83b925
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	205255
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.14
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 22463

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-22 03:07:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11645 boxname=wulflinc29 idbench=896 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  45da6faf70c895e4acc43dda6a83b925  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-air03.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-air03.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-air03.opb
IDLAUNCH: 11645
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        281488 kB
Buffers:         29044 kB
Cached:         700788 kB
SwapCached:        556 kB
Active:          46000 kB
Inactive:       685872 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        281236 kB
SwapTotal:     2097892 kB
SwapFree:      2096428 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            15736 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 03:27:58 (client local time) WITH STATUS 0 IN 1200.39 SECONDS
stats: 11645 7 1200.39 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.92 0.98 0.91 2/54 13960
Raw data (stat): 13960 (runsolver) R 13959 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550355687 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17087 0 0 0 960 38 0 0 25 0 1 0 550355687 79626240 16769 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19440 16769 603 41 0 19399 0
vsize: 77760
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17116 0 0 0 1959 39 0 0 25 0 1 0 550355687 79761408 16798 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.0013 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17188 0 0 0 2958 39 0 0 25 0 1 0 550355687 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.0008 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17250 0 0 0 3958 39 0 0 25 0 1 0 550355687 80375808 16932 4294967295 134512640 134672761 3221224544 3221223760 134561997 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.0015 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17292 0 0 0 4959 39 0 0 25 0 1 0 550355687 80510976 16974 4294967295 134512640 134672761 3221224544 3221223716 134556627 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.0016 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17340 0 0 0 5958 39 0 0 25 0 1 0 550355687 80646144 17022 4294967295 134512640 134672761 3221224544 3221223716 134556660 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.0021 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17383 0 0 0 6959 39 0 0 25 0 1 0 550355687 80916480 17065 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.0022 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17417 0 0 0 7959 39 0 0 25 0 1 0 550355687 81051648 17099 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17448 0 0 0 8959 39 0 0 25 0 1 0 550355687 81186816 17130 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19821 17130 603 41 0 19780 0
vsize: 79284
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17475 0 0 0 9959 40 0 0 25 0 1 0 550355687 81186816 17157 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17500 0 0 0 10959 40 0 0 25 0 1 0 550355687 81321984 17182 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17528 0 0 0 11959 40 0 0 25 0 1 0 550355687 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17555 0 0 0 12959 40 0 0 25 0 1 0 550355687 81670144 17237 4294967295 134512640 134672761 3221224544 3221223744 134561967 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17581 0 0 0 13959 40 0 0 25 0 1 0 550355687 81670144 17263 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17617 0 0 0 14960 40 0 0 25 0 1 0 550355687 81805312 17299 4294967295 134512640 134672761 3221224544 3221223724 134556674 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17640 0 0 0 15960 40 0 0 25 0 1 0 550355687 81940480 17322 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17659 0 0 0 16960 40 0 0 25 0 1 0 550355687 81940480 17341 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17675 0 0 0 17960 40 0 0 25 0 1 0 550355687 82075648 17357 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17689 0 0 0 18960 40 0 0 25 0 1 0 550355687 82075648 17371 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17710 0 0 0 19960 40 0 0 25 0 1 0 550355687 82210816 17392 4294967295 134512640 134672761 3221224544 3221223732 134556588 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.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17734 0 0 0 20960 40 0 0 25 0 1 0 550355687 82210816 17416 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17746 0 0 0 21960 40 0 0 25 0 1 0 550355687 82345984 17428 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17763 0 0 0 22960 40 0 0 25 0 1 0 550355687 82345984 17445 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17781 0 0 0 23960 41 0 0 25 0 1 0 550355687 82481152 17463 4294967295 134512640 134672761 3221224544 3221223728 134556675 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.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17792 0 0 0 24960 41 0 0 25 0 1 0 550355687 82481152 17474 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17801 0 0 0 25960 41 0 0 25 0 1 0 550355687 82481152 17483 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17810 0 0 0 26961 41 0 0 25 0 1 0 550355687 82481152 17492 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17822 0 0 0 27961 41 0 0 25 0 1 0 550355687 82616320 17504 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17832 0 0 0 28961 41 0 0 25 0 1 0 550355687 82616320 17514 4294967295 134512640 134672761 3221224544 3221223760 134561997 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17851 0 0 0 29961 41 0 0 25 0 1 0 550355687 82751488 17533 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17859 0 0 0 30961 41 0 0 25 0 1 0 550355687 82751488 17541 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17541 603 41 0 20162 0
vsize: 80812
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17871 0 0 0 31962 41 0 0 25 0 1 0 550355687 82751488 17553 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17553 603 41 0 20162 0
vsize: 80812
[startup+330.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17879 0 0 0 32962 41 0 0 25 0 1 0 550355687 82751488 17561 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17561 603 41 0 20162 0
vsize: 80812
[startup+340.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17887 0 0 0 33962 41 0 0 25 0 1 0 550355687 82751488 17569 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17569 603 41 0 20162 0
vsize: 80812
[startup+350.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17892 0 0 0 34962 41 0 0 25 0 1 0 550355687 82886656 17574 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17574 603 41 0 20195 0
vsize: 80944
[startup+360.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17894 0 0 0 35963 41 0 0 25 0 1 0 550355687 82886656 17576 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17576 603 41 0 20195 0
vsize: 80944
[startup+370.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17905 0 0 0 36963 41 0 0 25 0 1 0 550355687 82886656 17587 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17912 0 0 0 37962 41 0 0 25 0 1 0 550355687 82886656 17594 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20236 17594 603 41 0 20195 0
vsize: 80944
[startup+390.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17919 0 0 0 38961 41 0 0 25 0 1 0 550355687 82886656 17601 4294967295 134512640 134672761 3221224544 3221223668 134566071 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17927 0 0 0 39962 41 0 0 25 0 1 0 550355687 82886656 17609 4294967295 134512640 134672761 3221224544 3221223760 134561948 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17931 0 0 0 40962 41 0 0 25 0 1 0 550355687 82886656 17613 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17613 603 41 0 20195 0
vsize: 80944
[startup+420.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17933 0 0 0 41962 41 0 0 25 0 1 0 550355687 83021824 17615 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17936 0 0 0 42962 41 0 0 25 0 1 0 550355687 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17973 0 0 0 43962 42 0 0 25 0 1 0 550355687 83283968 17655 4294967295 134512640 134672761 3221224544 3221223728 134556589 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17977 0 0 0 44962 42 0 0 25 0 1 0 550355687 83283968 17659 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17977 0 0 0 45963 42 0 0 25 0 1 0 550355687 83283968 17659 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17977 0 0 0 46963 42 0 0 25 0 1 0 550355687 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556660 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.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17977 0 0 0 47963 42 0 0 25 0 1 0 550355687 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17977 0 0 0 48963 42 0 0 25 0 1 0 550355687 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556641 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17977 0 0 0 49963 42 0 0 25 0 1 0 550355687 83283968 17659 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17984 0 0 0 50963 42 0 0 25 0 1 0 550355687 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556660 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.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17984 0 0 0 51964 42 0 0 25 0 1 0 550355687 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556660 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17984 0 0 0 52964 42 0 0 25 0 1 0 550355687 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+540.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17985 0 0 0 53964 42 0 0 25 0 1 0 550355687 83283968 17667 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17989 0 0 0 54964 42 0 0 25 0 1 0 550355687 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+560.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17989 0 0 0 55975 42 0 0 25 0 1 0 550355687 83283968 17671 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17989 0 0 0 56975 42 0 0 25 0 1 0 550355687 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+580.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17994 0 0 0 57975 42 0 0 25 0 1 0 550355687 83283968 17676 4294967295 134512640 134672761 3221224544 3221223760 134561997 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.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17994 0 0 0 58975 42 0 0 25 0 1 0 550355687 83283968 17676 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.116 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17996 0 0 0 59975 42 0 0 25 0 1 0 550355687 83283968 17678 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17678 603 41 0 20292 0
vsize: 81332
[startup+610.115 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 17998 0 0 0 60974 42 0 0 25 0 1 0 550355687 83283968 17680 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18001 0 0 0 61974 42 0 0 25 0 1 0 550355687 83283968 17683 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18004 0 0 0 62975 42 0 0 25 0 1 0 550355687 83283968 17686 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18006 0 0 0 63975 42 0 0 25 0 1 0 550355687 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+650.117 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18006 0 0 0 64975 42 0 0 25 0 1 0 550355687 83283968 17688 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.118 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18008 0 0 0 65975 42 0 0 25 0 1 0 550355687 83283968 17690 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.118 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18009 0 0 0 66975 42 0 0 25 0 1 0 550355687 83283968 17691 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.118 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18013 0 0 0 67976 42 0 0 25 0 1 0 550355687 83283968 17695 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.119 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18014 0 0 0 68976 42 0 0 25 0 1 0 550355687 83283968 17696 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18015 0 0 0 69976 42 0 0 25 0 1 0 550355687 83283968 17697 4294967295 134512640 134672761 3221224544 3221223716 134556671 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.12 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18015 0 0 0 70976 42 0 0 25 0 1 0 550355687 83283968 17697 4294967295 134512640 134672761 3221224544 3221223716 134556604 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.122 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18015 0 0 0 71977 42 0 0 25 0 1 0 550355687 83283968 17697 4294967295 134512640 134672761 3221224544 3221223668 134566031 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.122 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18016 0 0 0 72977 42 0 0 25 0 1 0 550355687 83283968 17698 4294967295 134512640 134672761 3221224544 3221223668 134566122 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.124 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18016 0 0 0 73977 42 0 0 25 0 1 0 550355687 83283968 17698 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.124 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18018 0 0 0 74977 42 0 0 25 0 1 0 550355687 83283968 17700 4294967295 134512640 134672761 3221224544 3221223712 134561207 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.124 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18018 0 0 0 75978 42 0 0 25 0 1 0 550355687 83283968 17700 4294967295 134512640 134672761 3221224544 3221223696 134565096 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.124 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18023 0 0 0 76978 42 0 0 25 0 1 0 550355687 83283968 17705 4294967295 134512640 134672761 3221224544 3221223712 134561400 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.147 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18025 0 0 0 77980 42 0 0 25 0 1 0 550355687 83283968 17707 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.163 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18027 0 0 0 78982 42 0 0 25 0 1 0 550355687 83283968 17709 4294967295 134512640 134672761 3221224544 3221223668 134566007 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.166 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18027 0 0 0 79982 42 0 0 25 0 1 0 550355687 83283968 17709 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.165 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18028 0 0 0 80982 42 0 0 25 0 1 0 550355687 83283968 17710 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.166 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18028 0 0 0 81983 42 0 0 25 0 1 0 550355687 83283968 17710 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.169 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18029 0 0 0 82983 42 0 0 25 0 1 0 550355687 83283968 17711 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.202 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18029 0 0 0 83987 42 0 0 25 0 1 0 550355687 83283968 17711 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.202 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18030 0 0 0 84987 42 0 0 25 0 1 0 550355687 83283968 17712 4294967295 134512640 134672761 3221224544 3221223760 134561985 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.204 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18035 0 0 0 85987 42 0 0 25 0 1 0 550355687 83283968 17717 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.204 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18039 0 0 0 86986 42 0 0 25 0 1 0 550355687 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.205 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18039 0 0 0 87987 42 0 0 25 0 1 0 550355687 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+890.205 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18039 0 0 0 88987 42 0 0 25 0 1 0 550355687 83283968 17721 4294967295 134512640 134672761 3221224544 3221223732 134556588 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.205 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18039 0 0 0 89987 42 0 0 25 0 1 0 550355687 83283968 17721 4294967295 134512640 134672761 3221224544 3221223668 134566071 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.205 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18039 0 0 0 90987 42 0 0 25 0 1 0 550355687 83283968 17721 4294967295 134512640 134672761 3221224544 3221223668 134566071 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.206 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18041 0 0 0 91987 42 0 0 25 0 1 0 550355687 83283968 17723 4294967295 134512640 134672761 3221224544 3221223696 134565076 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.207 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18041 0 0 0 92988 42 0 0 25 0 1 0 550355687 83283968 17723 4294967295 134512640 134672761 3221224544 3221223712 134564746 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.206 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18041 0 0 0 93988 42 0 0 25 0 1 0 550355687 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556671 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.206 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18042 0 0 0 94988 42 0 0 25 0 1 0 550355687 83283968 17724 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.207 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18043 0 0 0 95988 42 0 0 25 0 1 0 550355687 83283968 17725 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.208 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18044 0 0 0 96988 42 0 0 25 0 1 0 550355687 83283968 17726 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.208 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18044 0 0 0 97989 42 0 0 25 0 1 0 550355687 83283968 17726 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.207 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18044 0 0 0 98989 42 0 0 25 0 1 0 550355687 83283968 17726 4294967295 134512640 134672761 3221224544 3221223700 134564777 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18046 0 0 0 99989 42 0 0 25 0 1 0 550355687 83283968 17728 4294967295 134512640 134672761 3221224544 3221223712 134560867 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18046 0 0 0 100989 42 0 0 25 0 1 0 550355687 83283968 17728 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18047 0 0 0 101989 42 0 0 25 0 1 0 550355687 83283968 17729 4294967295 134512640 134672761 3221224544 3221223708 134564510 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18047 0 0 0 102990 42 0 0 25 0 1 0 550355687 83283968 17729 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18052 0 0 0 103990 42 0 0 25 0 1 0 550355687 83427328 17734 4294967295 134512640 134672761 3221224544 3221223696 134565137 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18052 0 0 0 104990 42 0 0 25 0 1 0 550355687 83427328 17734 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18053 0 0 0 105990 42 0 0 25 0 1 0 550355687 83427328 17735 4294967295 134512640 134672761 3221224544 3221223808 134562196 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18053 0 0 0 106991 42 0 0 25 0 1 0 550355687 83427328 17735 4294967295 134512640 134672761 3221224544 3221223680 134560688 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18053 0 0 0 107991 42 0 0 25 0 1 0 550355687 83427328 17735 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18055 0 0 0 108991 42 0 0 25 0 1 0 550355687 83427328 17737 4294967295 134512640 134672761 3221224544 3221223808 134562156 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18055 0 0 0 109991 43 0 0 25 0 1 0 550355687 83427328 17737 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1110.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18055 0 0 0 110990 43 0 0 25 0 1 0 550355687 83427328 17737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1120.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18055 0 0 0 111989 43 0 0 25 0 1 0 550355687 83427328 17737 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18061 0 0 0 112989 43 0 0 25 0 1 0 550355687 83427328 17743 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18064 0 0 0 113989 43 0 0 25 0 1 0 550355687 83427328 17746 4294967295 134512640 134672761 3221224544 3221223744 134561972 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.21 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18065 0 0 0 114990 43 0 0 25 0 1 0 550355687 83427328 17747 4294967295 134512640 134672761 3221224544 3221223696 134565086 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.22 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18066 0 0 0 115990 43 0 0 25 0 1 0 550355687 83427328 17748 4294967295 134512640 134672761 3221224544 3221223696 134565094 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.22 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18069 0 0 0 116990 43 0 0 25 0 1 0 550355687 83427328 17751 4294967295 134512640 134672761 3221224544 3221223760 134561997 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.22 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18069 0 0 0 117990 43 0 0 25 0 1 0 550355687 83427328 17751 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.22 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18073 0 0 0 118990 43 0 0 25 0 1 0 550355687 83427328 17755 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.22 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13960
Raw data (stat): 13960 (minisat+) R 13959 27222 27221 0 -1 0 18074 0 0 0 119991 43 0 0 25 0 1 0 550355687 83427328 17756 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.25 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 13960
Raw data (stat): 13960 (minisat+) Z 13959 27222 27221 0 -1 12 18076 0 0 0 119991 47 0 0 25 0 1 0 550355687 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.25
CPU time (s): 1200.39
CPU user time (s): 1199.91
CPU system time (s): 0.472928
CPU usage (%): 100.011
Max. virtual memory (Kb): 81472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####