PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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	199098
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.09
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 15856

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-21 05:53:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16637 boxname=wulflinc17 idbench=1280 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  45da6faf70c895e4acc43dda6a83b925  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-air03.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-air03.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-air03.opb
IDLAUNCH: 16637
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        863512 kB
Buffers:          9824 kB
Cached:         132788 kB
SwapCached:        596 kB
Active:          58252 kB
Inactive:        87916 kB
HighTotal:      131008 kB
HighFree:        25088 kB
LowTotal:       903652 kB
LowFree:        838424 kB
SwapTotal:     2097892 kB
SwapFree:      2097284 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6628 kB
Slab:            19416 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:13:33 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 16637 7 1200.29 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.91 0.95 0.91 2/55 23133
Raw data (stat): 23133 (runsolver) R 23132 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542719292 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 23133
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17087 0 0 0 952 46 0 0 25 0 1 0 542719292 79626240 16769 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 23133
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17116 0 0 0 1952 46 0 0 25 0 1 0 542719292 79761408 16798 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19473 16798 603 41 0 19432 0
vsize: 77892
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 23133
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17188 0 0 0 2951 46 0 0 25 0 1 0 542719292 80052224 16870 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17250 0 0 0 3951 47 0 0 25 0 1 0 542719292 80375808 16932 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19623 16932 603 41 0 19582 0
vsize: 78492
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17292 0 0 0 4951 47 0 0 25 0 1 0 542719292 80510976 16974 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19656 16974 603 41 0 19615 0
vsize: 78624
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17340 0 0 0 5951 47 0 0 25 0 1 0 542719292 80646144 17022 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19689 17022 603 41 0 19648 0
vsize: 78756
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17386 0 0 0 6951 47 0 0 25 0 1 0 542719292 80916480 17068 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19755 17068 603 41 0 19714 0
vsize: 79020
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17417 0 0 0 7951 47 0 0 25 0 1 0 542719292 81051648 17099 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19788 17099 603 41 0 19747 0
vsize: 79152
[startup+90.0021 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17450 0 0 0 8952 47 0 0 25 0 1 0 542719292 81186816 17132 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19821 17132 603 41 0 19780 0
vsize: 79284
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17478 0 0 0 9951 47 0 0 25 0 1 0 542719292 81186816 17160 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19821 17160 603 41 0 19780 0
vsize: 79284
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17505 0 0 0 10952 47 0 0 25 0 1 0 542719292 81321984 17187 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19854 17187 603 41 0 19813 0
vsize: 79416
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17528 0 0 0 11952 47 0 0 25 0 1 0 542719292 81457152 17210 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19887 17210 603 41 0 19846 0
vsize: 79548
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17555 0 0 0 12952 47 0 0 25 0 1 0 542719292 81670144 17237 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19939 17237 603 41 0 19898 0
vsize: 79756
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17584 0 0 0 13952 48 0 0 25 0 1 0 542719292 81670144 17266 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19939 17266 603 41 0 19898 0
vsize: 79756
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17618 0 0 0 14952 48 0 0 25 0 1 0 542719292 81805312 17300 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19972 17300 603 41 0 19931 0
vsize: 79888
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17644 0 0 0 15952 48 0 0 25 0 1 0 542719292 81940480 17326 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20005 17326 603 41 0 19964 0
vsize: 80020
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17664 0 0 0 16952 48 0 0 25 0 1 0 542719292 81940480 17346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20005 17346 603 41 0 19964 0
vsize: 80020
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17678 0 0 0 17952 48 0 0 25 0 1 0 542719292 82075648 17360 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20038 17360 603 41 0 19997 0
vsize: 80152
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17694 0 0 0 18952 48 0 0 25 0 1 0 542719292 82075648 17376 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20038 17376 603 41 0 19997 0
vsize: 80152
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17716 0 0 0 19952 48 0 0 25 0 1 0 542719292 82210816 17398 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20071 17398 603 41 0 20030 0
vsize: 80284
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17738 0 0 0 20952 48 0 0 25 0 1 0 542719292 82345984 17420 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20104 17420 603 41 0 20063 0
vsize: 80416
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17749 0 0 0 21952 48 0 0 25 0 1 0 542719292 82345984 17431 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20104 17431 603 41 0 20063 0
vsize: 80416
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17767 0 0 0 22953 49 0 0 25 0 1 0 542719292 82345984 17449 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20104 17449 603 41 0 20063 0
vsize: 80416
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17783 0 0 0 23953 49 0 0 25 0 1 0 542719292 82481152 17465 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20137 17465 603 41 0 20096 0
vsize: 80548
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17792 0 0 0 24953 49 0 0 25 0 1 0 542719292 82481152 17474 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20137 17474 603 41 0 20096 0
vsize: 80548
[startup+260 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17804 0 0 0 25953 49 0 0 25 0 1 0 542719292 82481152 17486 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20137 17486 603 41 0 20096 0
vsize: 80548
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17811 0 0 0 26953 49 0 0 25 0 1 0 542719292 82616320 17493 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20170 17493 603 41 0 20129 0
vsize: 80680
[startup+280 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17823 0 0 0 27953 49 0 0 25 0 1 0 542719292 82616320 17505 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20170 17505 603 41 0 20129 0
vsize: 80680
[startup+290 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17845 0 0 0 28953 49 0 0 25 0 1 0 542719292 82616320 17527 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20170 17527 603 41 0 20129 0
vsize: 80680
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17853 0 0 0 29953 49 0 0 25 0 1 0 542719292 82751488 17535 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 17535 603 41 0 20162 0
vsize: 80812
[startup+310 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17860 0 0 0 30953 49 0 0 25 0 1 0 542719292 82751488 17542 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 17542 603 41 0 20162 0
vsize: 80812
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17871 0 0 0 31954 49 0 0 25 0 1 0 542719292 82751488 17553 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23135
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17880 0 0 0 32954 49 0 0 25 0 1 0 542719292 82751488 17562 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 17562 603 41 0 20162 0
vsize: 80812
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23137
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17887 0 0 0 33954 49 0 0 25 0 1 0 542719292 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23137
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17892 0 0 0 34954 49 0 0 25 0 1 0 542719292 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.001 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 23137
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17897 0 0 0 35954 49 0 0 25 0 1 0 542719292 82886656 17579 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20236 17579 603 41 0 20195 0
vsize: 80944
[startup+370.002 s]
Raw data (loadavg): 1.22 1.02 0.93 2/55 23137
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17907 0 0 0 36954 49 0 0 25 0 1 0 542719292 82886656 17589 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20236 17589 603 41 0 20195 0
vsize: 80944
[startup+380.002 s]
Raw data (loadavg): 1.18 1.02 0.93 2/55 23137
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17913 0 0 0 37954 50 0 0 25 0 1 0 542719292 82886656 17595 4294967295 134512640 134672761 3221224544 3221223712 134564752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20236 17595 603 41 0 20195 0
vsize: 80944
[startup+390.001 s]
Raw data (loadavg): 1.15 1.02 0.93 2/55 23137
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17921 0 0 0 38954 50 0 0 25 0 1 0 542719292 82886656 17603 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20236 17603 603 41 0 20195 0
vsize: 80944
[startup+400.002 s]
Raw data (loadavg): 1.21 1.03 0.94 2/59 23180
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17929 0 0 0 39951 53 0 0 25 0 1 0 542719292 82886656 17611 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20236 17611 603 41 0 20195 0
vsize: 80944
[startup+410.063 s]
Raw data (loadavg): 1.26 1.05 0.94 2/55 23190
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17932 0 0 0 40957 53 0 0 25 0 1 0 542719292 83021824 17614 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20269 17614 603 41 0 20228 0
vsize: 81076
[startup+420.063 s]
Raw data (loadavg): 1.22 1.05 0.94 2/55 23190
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17934 0 0 0 41957 53 0 0 25 0 1 0 542719292 83021824 17616 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20269 17616 603 41 0 20228 0
vsize: 81076
[startup+430.07 s]
Raw data (loadavg): 1.18 1.04 0.94 2/55 23190
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17973 0 0 0 42958 53 0 0 25 0 1 0 542719292 83283968 17655 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17655 603 41 0 20292 0
vsize: 81332
[startup+440.078 s]
Raw data (loadavg): 1.15 1.04 0.94 2/55 23190
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17973 0 0 0 43959 53 0 0 25 0 1 0 542719292 83283968 17655 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17655 603 41 0 20292 0
vsize: 81332
[startup+450.078 s]
Raw data (loadavg): 1.13 1.04 0.94 2/55 23190
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17977 0 0 0 44959 53 0 0 25 0 1 0 542719292 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+460.078 s]
Raw data (loadavg): 1.11 1.04 0.94 2/55 23190
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17977 0 0 0 45959 53 0 0 25 0 1 0 542719292 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+470.078 s]
Raw data (loadavg): 1.09 1.04 0.94 2/55 23190
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17977 0 0 0 46960 53 0 0 25 0 1 0 542719292 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+480.079 s]
Raw data (loadavg): 1.08 1.03 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17977 0 0 0 47960 53 0 0 25 0 1 0 542719292 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+490.078 s]
Raw data (loadavg): 1.07 1.03 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17977 0 0 0 48960 53 0 0 25 0 1 0 542719292 83283968 17659 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+500.085 s]
Raw data (loadavg): 1.06 1.03 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17980 0 0 0 49961 53 0 0 25 0 1 0 542719292 83283968 17662 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17662 603 41 0 20292 0
vsize: 81332
[startup+510.084 s]
Raw data (loadavg): 1.05 1.03 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17984 0 0 0 50961 53 0 0 25 0 1 0 542719292 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17666 603 41 0 20292 0
vsize: 81332
[startup+520.085 s]
Raw data (loadavg): 1.04 1.03 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17984 0 0 0 51961 53 0 0 25 0 1 0 542719292 83283968 17666 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17666 603 41 0 20292 0
vsize: 81332
[startup+530.086 s]
Raw data (loadavg): 1.03 1.03 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17984 0 0 0 52961 53 0 0 25 0 1 0 542719292 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17666 603 41 0 20292 0
vsize: 81332
[startup+540.085 s]
Raw data (loadavg): 1.03 1.03 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17985 0 0 0 53962 53 0 0 25 0 1 0 542719292 83283968 17667 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17667 603 41 0 20292 0
vsize: 81332
[startup+550.085 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17989 0 0 0 54962 53 0 0 25 0 1 0 542719292 83283968 17671 4294967295 134512640 134672761 3221224544 3221223760 134557616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17671 603 41 0 20292 0
vsize: 81332
[startup+560.085 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17989 0 0 0 55962 53 0 0 25 0 1 0 542719292 83283968 17671 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17671 603 41 0 20292 0
vsize: 81332
[startup+570.085 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17989 0 0 0 56962 53 0 0 25 0 1 0 542719292 83283968 17671 4294967295 134512640 134672761 3221224544 3221223744 134557959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17671 603 41 0 20292 0
vsize: 81332
[startup+580.085 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17994 0 0 0 57962 53 0 0 25 0 1 0 542719292 83283968 17676 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17676 603 41 0 20292 0
vsize: 81332
[startup+590.085 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17995 0 0 0 58962 53 0 0 25 0 1 0 542719292 83283968 17677 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17677 603 41 0 20292 0
vsize: 81332
[startup+600.085 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17996 0 0 0 59962 53 0 0 25 0 1 0 542719292 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.084 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 17998 0 0 0 60962 53 0 0 25 0 1 0 542719292 83283968 17680 4294967295 134512640 134672761 3221224544 3221223724 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17680 603 41 0 20292 0
vsize: 81332
[startup+620.085 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18002 0 0 0 61962 53 0 0 25 0 1 0 542719292 83283968 17684 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17684 603 41 0 20292 0
vsize: 81332
[startup+630.085 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 23192
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18004 0 0 0 62962 53 0 0 25 0 1 0 542719292 83283968 17686 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17686 603 41 0 20292 0
vsize: 81332
[startup+640.085 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18006 0 0 0 63962 53 0 0 25 0 1 0 542719292 83283968 17688 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17688 603 41 0 20292 0
vsize: 81332
[startup+650.085 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18007 0 0 0 64962 53 0 0 25 0 1 0 542719292 83283968 17689 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17689 603 41 0 20292 0
vsize: 81332
[startup+660.084 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18008 0 0 0 65962 53 0 0 25 0 1 0 542719292 83283968 17690 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17690 603 41 0 20292 0
vsize: 81332
[startup+670.085 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18013 0 0 0 66963 53 0 0 25 0 1 0 542719292 83283968 17695 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17695 603 41 0 20292 0
vsize: 81332
[startup+680.086 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18014 0 0 0 67963 53 0 0 25 0 1 0 542719292 83283968 17696 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17696 603 41 0 20292 0
vsize: 81332
[startup+690.085 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18015 0 0 0 68963 53 0 0 25 0 1 0 542719292 83283968 17697 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17697 603 41 0 20292 0
vsize: 81332
[startup+700.085 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18015 0 0 0 69963 53 0 0 25 0 1 0 542719292 83283968 17697 4294967295 134512640 134672761 3221224544 3221223716 134556609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17697 603 41 0 20292 0
vsize: 81332
[startup+710.086 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18015 0 0 0 70963 53 0 0 25 0 1 0 542719292 83283968 17697 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17697 603 41 0 20292 0
vsize: 81332
[startup+720.086 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23194
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18016 0 0 0 71963 54 0 0 25 0 1 0 542719292 83283968 17698 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17698 603 41 0 20292 0
vsize: 81332
[startup+730.086 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18016 0 0 0 72964 54 0 0 25 0 1 0 542719292 83283968 17698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17698 603 41 0 20292 0
vsize: 81332
[startup+740.085 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18017 0 0 0 73964 54 0 0 25 0 1 0 542719292 83283968 17699 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17699 603 41 0 20292 0
vsize: 81332
[startup+750.086 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18018 0 0 0 74964 54 0 0 25 0 1 0 542719292 83283968 17700 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17700 603 41 0 20292 0
vsize: 81332
[startup+760.086 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18023 0 0 0 75964 54 0 0 25 0 1 0 542719292 83283968 17705 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17705 603 41 0 20292 0
vsize: 81332
[startup+770.086 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18025 0 0 0 76964 54 0 0 25 0 1 0 542719292 83283968 17707 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17707 603 41 0 20292 0
vsize: 81332
[startup+780.087 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18025 0 0 0 77965 54 0 0 25 0 1 0 542719292 83283968 17707 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17707 603 41 0 20292 0
vsize: 81332
[startup+790.086 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18027 0 0 0 78965 54 0 0 25 0 1 0 542719292 83283968 17709 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17709 603 41 0 20292 0
vsize: 81332
[startup+800.086 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18027 0 0 0 79965 54 0 0 25 0 1 0 542719292 83283968 17709 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17709 603 41 0 20292 0
vsize: 81332
[startup+810.086 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18028 0 0 0 80965 54 0 0 25 0 1 0 542719292 83283968 17710 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17710 603 41 0 20292 0
vsize: 81332
[startup+820.087 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18029 0 0 0 81965 54 0 0 25 0 1 0 542719292 83283968 17711 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17711 603 41 0 20292 0
vsize: 81332
[startup+830.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18029 0 0 0 82966 54 0 0 25 0 1 0 542719292 83283968 17711 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17711 603 41 0 20292 0
vsize: 81332
[startup+840.087 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18029 0 0 0 83966 54 0 0 25 0 1 0 542719292 83283968 17711 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17711 603 41 0 20292 0
vsize: 81332
[startup+850.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18030 0 0 0 84966 54 0 0 25 0 1 0 542719292 83283968 17712 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17712 603 41 0 20292 0
vsize: 81332
[startup+860.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18039 0 0 0 85966 54 0 0 25 0 1 0 542719292 83283968 17721 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+870.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18039 0 0 0 86965 54 0 0 25 0 1 0 542719292 83283968 17721 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+880.089 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18039 0 0 0 87965 54 0 0 25 0 1 0 542719292 83283968 17721 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+890.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18039 0 0 0 88965 54 0 0 25 0 1 0 542719292 83283968 17721 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+900.089 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18039 0 0 0 89966 54 0 0 25 0 1 0 542719292 83283968 17721 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17721 603 41 0 20292 0
vsize: 81332
[startup+910.088 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18041 0 0 0 90966 54 0 0 25 0 1 0 542719292 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+920.089 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18041 0 0 0 91966 54 0 0 25 0 1 0 542719292 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+930.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23196
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18041 0 0 0 92966 54 0 0 25 0 1 0 542719292 83283968 17723 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+940.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18041 0 0 0 93966 54 0 0 25 0 1 0 542719292 83283968 17723 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+950.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18042 0 0 0 94967 54 0 0 25 0 1 0 542719292 83283968 17724 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17724 603 41 0 20292 0
vsize: 81332
[startup+960.089 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18043 0 0 0 95967 54 0 0 25 0 1 0 542719292 83283968 17725 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17725 603 41 0 20292 0
vsize: 81332
[startup+970.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18044 0 0 0 96967 54 0 0 25 0 1 0 542719292 83283968 17726 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17726 603 41 0 20292 0
vsize: 81332
[startup+980.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18044 0 0 0 97967 54 0 0 25 0 1 0 542719292 83283968 17726 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17726 603 41 0 20292 0
vsize: 81332
[startup+990.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18046 0 0 0 98967 54 0 0 25 0 1 0 542719292 83283968 17728 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17728 603 41 0 20292 0
vsize: 81332
[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18046 0 0 0 99967 54 0 0 25 0 1 0 542719292 83283968 17728 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17728 603 41 0 20292 0
vsize: 81332
[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18046 0 0 0 100967 54 0 0 25 0 1 0 542719292 83283968 17728 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17728 603 41 0 20292 0
vsize: 81332
[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18047 0 0 0 101967 54 0 0 25 0 1 0 542719292 83283968 17729 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 17729 603 41 0 20292 0
vsize: 81332
[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18052 0 0 0 102968 54 0 0 25 0 1 0 542719292 83427328 17734 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17734 603 41 0 20327 0
vsize: 81472
[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18052 0 0 0 103968 54 0 0 25 0 1 0 542719292 83427328 17734 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17734 603 41 0 20327 0
vsize: 81472
[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18052 0 0 0 104968 54 0 0 25 0 1 0 542719292 83427328 17734 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17734 603 41 0 20327 0
vsize: 81472
[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18053 0 0 0 105968 54 0 0 25 0 1 0 542719292 83427328 17735 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17735 603 41 0 20327 0
vsize: 81472
[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18053 0 0 0 106968 54 0 0 25 0 1 0 542719292 83427328 17735 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17735 603 41 0 20327 0
vsize: 81472
[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18055 0 0 0 107969 54 0 0 25 0 1 0 542719292 83427328 17737 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18055 0 0 0 108968 55 0 0 25 0 1 0 542719292 83427328 17737 4294967295 134512640 134672761 3221224544 3221223696 134565086 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.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18055 0 0 0 109968 55 0 0 25 0 1 0 542719292 83427328 17737 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18055 0 0 0 110968 55 0 0 25 0 1 0 542719292 83427328 17737 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18058 0 0 0 111968 55 0 0 25 0 1 0 542719292 83427328 17740 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17740 603 41 0 20327 0
vsize: 81472
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18064 0 0 0 112968 55 0 0 25 0 1 0 542719292 83427328 17746 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17746 603 41 0 20327 0
vsize: 81472
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18064 0 0 0 113968 55 0 0 25 0 1 0 542719292 83427328 17746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17746 603 41 0 20327 0
vsize: 81472
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18066 0 0 0 114969 55 0 0 25 0 1 0 542719292 83427328 17748 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17748 603 41 0 20327 0
vsize: 81472
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18068 0 0 0 115969 55 0 0 25 0 1 0 542719292 83427328 17750 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17750 603 41 0 20327 0
vsize: 81472
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18069 0 0 0 116969 55 0 0 25 0 1 0 542719292 83427328 17751 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17751 603 41 0 20327 0
vsize: 81472
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18072 0 0 0 117969 55 0 0 25 0 1 0 542719292 83427328 17754 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17754 603 41 0 20327 0
vsize: 81472
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18074 0 0 0 118969 55 0 0 25 0 1 0 542719292 83427328 17756 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17756 603 41 0 20327 0
vsize: 81472
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 23198
Raw data (stat): 23133 (minisat+) R 23132 20838 20837 0 -1 0 18074 0 0 0 119969 55 0 0 25 0 1 0 542719292 83427328 17756 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20368 17756 603 41 0 20327 0
vsize: 81472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 23198
Raw data (stat): 23133 (minisat+) Z 23132 20838 20837 0 -1 12 18076 0 0 0 119969 59 0 0 25 0 1 0 542719292 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.12
CPU time (s): 1200.29
CPU user time (s): 1199.7
CPU system time (s): 0.59091
CPU usage (%): 100.014
Max. virtual memory (Kb): 81472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####