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/miplib3/normalized-mps-v2-13-7-air03.opb
MD5SUM	69337cf8d2b6f6cf8cc02fedc291ffcc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	199224
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.13
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 15247

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 03:33:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18158 boxname=wulflinc15 idbench=1397 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69337cf8d2b6f6cf8cc02fedc291ffcc  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-air03.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-air03.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-air03.opb
IDLAUNCH: 18158
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        724572 kB
Buffers:         33992 kB
Cached:         251452 kB
SwapCached:       2060 kB
Active:         119212 kB
Inactive:       171128 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        724320 kB
SwapTotal:     2097136 kB
SwapFree:      2094988 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14032 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:53:54 (client local time) WITH STATUS 0 IN 1200.42 SECONDS
stats: 18158 7 1200.42 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.97 0.94 2/54 27609
Raw data (stat): 27609 (runsolver) R 27608 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483648285 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.001 s]
Raw data (loadavg): 0.93 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17087 0 0 0 958 41 0 0 25 0 1 0 483648285 79626240 16769 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0019 s]
Raw data (loadavg): 0.94 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17116 0 0 0 1958 41 0 0 25 0 1 0 483648285 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.0021 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17188 0 0 0 2958 41 0 0 25 0 1 0 483648285 80052224 16870 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19544 16870 603 41 0 19503 0
vsize: 78176
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17250 0 0 0 3957 42 0 0 25 0 1 0 483648285 80375808 16932 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0039 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17292 0 0 0 4957 42 0 0 25 0 1 0 483648285 80510976 16974 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.0048 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17340 0 0 0 5957 43 0 0 25 0 1 0 483648285 80646144 17022 4294967295 134512640 134672761 3221224544 3221223744 134561972 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.0056 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17383 0 0 0 6956 43 0 0 25 0 1 0 483648285 80916480 17065 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19755 17065 603 41 0 19714 0
vsize: 79020
[startup+80.006 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17417 0 0 0 7956 44 0 0 25 0 1 0 483648285 81051648 17099 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.0062 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17447 0 0 0 8956 44 0 0 25 0 1 0 483648285 81186816 17129 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19821 17129 603 41 0 19780 0
vsize: 79284
[startup+100.006 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17475 0 0 0 9955 45 0 0 25 0 1 0 483648285 81186816 17157 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19821 17157 603 41 0 19780 0
vsize: 79284
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17500 0 0 0 10955 45 0 0 25 0 1 0 483648285 81321984 17182 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19854 17182 603 41 0 19813 0
vsize: 79416
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17528 0 0 0 11955 45 0 0 25 0 1 0 483648285 81457152 17210 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17555 0 0 0 12955 45 0 0 25 0 1 0 483648285 81670144 17237 4294967295 134512640 134672761 3221224544 3221223716 134556596 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17581 0 0 0 13955 45 0 0 25 0 1 0 483648285 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17617 0 0 0 14955 45 0 0 25 0 1 0 483648285 81805312 17299 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17640 0 0 0 15956 45 0 0 25 0 1 0 483648285 81940480 17322 4294967295 134512640 134672761 3221224544 3221223716 134556680 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.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17663 0 0 0 16956 45 0 0 25 0 1 0 483648285 81940480 17345 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20005 17345 603 41 0 19964 0
vsize: 80020
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17678 0 0 0 17956 45 0 0 25 0 1 0 483648285 82075648 17360 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20038 17360 603 41 0 19997 0
vsize: 80152
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17694 0 0 0 18956 46 0 0 25 0 1 0 483648285 82075648 17376 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20038 17376 603 41 0 19997 0
vsize: 80152
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17715 0 0 0 19956 46 0 0 25 0 1 0 483648285 82210816 17397 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20071 17397 603 41 0 20030 0
vsize: 80284
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17737 0 0 0 20956 46 0 0 25 0 1 0 483648285 82210816 17419 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20071 17419 603 41 0 20030 0
vsize: 80284
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17748 0 0 0 21956 46 0 0 25 0 1 0 483648285 82345984 17430 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20104 17430 603 41 0 20063 0
vsize: 80416
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17766 0 0 0 22956 46 0 0 25 0 1 0 483648285 82345984 17448 4294967295 134512640 134672761 3221224544 3221223788 134564647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20104 17448 603 41 0 20063 0
vsize: 80416
[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17783 0 0 0 23957 46 0 0 25 0 1 0 483648285 82481152 17465 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17465 603 41 0 20096 0
vsize: 80548
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17792 0 0 0 24957 46 0 0 25 0 1 0 483648285 82481152 17474 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17802 0 0 0 25957 46 0 0 25 0 1 0 483648285 82481152 17484 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17484 603 41 0 20096 0
vsize: 80548
[startup+270.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17811 0 0 0 26957 46 0 0 25 0 1 0 483648285 82616320 17493 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20170 17493 603 41 0 20129 0
vsize: 80680
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17823 0 0 0 27957 46 0 0 25 0 1 0 483648285 82616320 17505 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20170 17505 603 41 0 20129 0
vsize: 80680
[startup+290.123 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17843 0 0 0 28968 46 0 0 25 0 1 0 483648285 82616320 17525 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20170 17525 603 41 0 20129 0
vsize: 80680
[startup+300.123 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17853 0 0 0 29968 46 0 0 25 0 1 0 483648285 82751488 17535 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17535 603 41 0 20162 0
vsize: 80812
[startup+310.13 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17860 0 0 0 30969 46 0 0 25 0 1 0 483648285 82751488 17542 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17542 603 41 0 20162 0
vsize: 80812
[startup+320.13 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17871 0 0 0 31969 46 0 0 25 0 1 0 483648285 82751488 17553 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.13 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17880 0 0 0 32969 47 0 0 25 0 1 0 483648285 82751488 17562 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17562 603 41 0 20162 0
vsize: 80812
[startup+340.13 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17887 0 0 0 33969 47 0 0 25 0 1 0 483648285 82751488 17569 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.131 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17892 0 0 0 34970 47 0 0 25 0 1 0 483648285 82886656 17574 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.131 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17897 0 0 0 35970 47 0 0 25 0 1 0 483648285 82886656 17579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17579 603 41 0 20195 0
vsize: 80944
[startup+370.131 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17907 0 0 0 36970 47 0 0 25 0 1 0 483648285 82886656 17589 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17589 603 41 0 20195 0
vsize: 80944
[startup+380.131 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17913 0 0 0 37970 47 0 0 25 0 1 0 483648285 82886656 17595 4294967295 134512640 134672761 3221224544 3221223684 134566156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17595 603 41 0 20195 0
vsize: 80944
[startup+390.132 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17921 0 0 0 38970 47 0 0 25 0 1 0 483648285 82886656 17603 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17603 603 41 0 20195 0
vsize: 80944
[startup+400.131 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17929 0 0 0 39970 47 0 0 25 0 1 0 483648285 82886656 17611 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20236 17611 603 41 0 20195 0
vsize: 80944
[startup+410.133 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17932 0 0 0 40970 47 0 0 25 0 1 0 483648285 83021824 17614 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20269 17614 603 41 0 20228 0
vsize: 81076
[startup+420.133 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17934 0 0 0 41970 47 0 0 25 0 1 0 483648285 83021824 17616 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20269 17616 603 41 0 20228 0
vsize: 81076
[startup+430.133 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17973 0 0 0 42971 47 0 0 25 0 1 0 483648285 83283968 17655 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17655 603 41 0 20292 0
vsize: 81332
[startup+440.132 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17973 0 0 0 43971 47 0 0 25 0 1 0 483648285 83283968 17655 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.14 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17977 0 0 0 44972 47 0 0 25 0 1 0 483648285 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+460.141 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17977 0 0 0 45972 47 0 0 25 0 1 0 483648285 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556653 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.141 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17977 0 0 0 46972 47 0 0 25 0 1 0 483648285 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.141 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17977 0 0 0 47972 47 0 0 25 0 1 0 483648285 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556664 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.142 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17977 0 0 0 48972 47 0 0 25 0 1 0 483648285 83283968 17659 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17659 603 41 0 20292 0
vsize: 81332
[startup+500.142 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17980 0 0 0 49973 47 0 0 25 0 1 0 483648285 83283968 17662 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17662 603 41 0 20292 0
vsize: 81332
[startup+510.142 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17984 0 0 0 50973 47 0 0 25 0 1 0 483648285 83283968 17666 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.142 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17984 0 0 0 51973 47 0 0 25 0 1 0 483648285 83283968 17666 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.142 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17984 0 0 0 52973 47 0 0 25 0 1 0 483648285 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.15 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17985 0 0 0 53974 47 0 0 25 0 1 0 483648285 83283968 17667 4294967295 134512640 134672761 3221224544 3221223744 134557885 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.159 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17989 0 0 0 54975 47 0 0 25 0 1 0 483648285 83283968 17671 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17989 0 0 0 55975 47 0 0 25 0 1 0 483648285 83283968 17671 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.16 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17989 0 0 0 56975 47 0 0 25 0 1 0 483648285 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.159 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17994 0 0 0 57975 47 0 0 25 0 1 0 483648285 83283968 17676 4294967295 134512640 134672761 3221224544 3221223740 134556584 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.161 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17995 0 0 0 58976 47 0 0 25 0 1 0 483648285 83283968 17677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17677 603 41 0 20292 0
vsize: 81332
[startup+600.161 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17996 0 0 0 59976 47 0 0 25 0 1 0 483648285 83283968 17678 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.163 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 17998 0 0 0 60976 47 0 0 25 0 1 0 483648285 83283968 17680 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17680 603 41 0 20292 0
vsize: 81332
[startup+620.17 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18002 0 0 0 61977 47 0 0 25 0 1 0 483648285 83283968 17684 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17684 603 41 0 20292 0
vsize: 81332
[startup+630.182 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18006 0 0 0 62978 47 0 0 25 0 1 0 483648285 83283968 17688 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17688 603 41 0 20292 0
vsize: 81332
[startup+640.182 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18006 0 0 0 63978 47 0 0 25 0 1 0 483648285 83283968 17688 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.189 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18007 0 0 0 64979 47 0 0 25 0 1 0 483648285 83283968 17689 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17689 603 41 0 20292 0
vsize: 81332
[startup+660.194 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18008 0 0 0 65980 47 0 0 25 0 1 0 483648285 83283968 17690 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.194 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18013 0 0 0 66980 47 0 0 25 0 1 0 483648285 83283968 17695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17695 603 41 0 20292 0
vsize: 81332
[startup+680.194 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18014 0 0 0 67980 47 0 0 25 0 1 0 483648285 83283968 17696 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17696 603 41 0 20292 0
vsize: 81332
[startup+690.195 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18015 0 0 0 68980 47 0 0 25 0 1 0 483648285 83283968 17697 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17697 603 41 0 20292 0
vsize: 81332
[startup+700.195 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18015 0 0 0 69980 47 0 0 25 0 1 0 483648285 83283968 17697 4294967295 134512640 134672761 3221224544 3221223716 134556669 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.196 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18015 0 0 0 70981 47 0 0 25 0 1 0 483648285 83283968 17697 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.196 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18016 0 0 0 71981 47 0 0 25 0 1 0 483648285 83283968 17698 4294967295 134512640 134672761 3221224544 3221223712 134564764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17698 603 41 0 20292 0
vsize: 81332
[startup+730.195 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18016 0 0 0 72981 47 0 0 25 0 1 0 483648285 83283968 17698 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.195 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18017 0 0 0 73981 47 0 0 25 0 1 0 483648285 83283968 17699 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17699 603 41 0 20292 0
vsize: 81332
[startup+750.195 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18018 0 0 0 74981 47 0 0 25 0 1 0 483648285 83283968 17700 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17700 603 41 0 20292 0
vsize: 81332
[startup+760.196 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18023 0 0 0 75981 47 0 0 25 0 1 0 483648285 83283968 17705 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17705 603 41 0 20292 0
vsize: 81332
[startup+770.196 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18025 0 0 0 76982 47 0 0 25 0 1 0 483648285 83283968 17707 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17707 603 41 0 20292 0
vsize: 81332
[startup+780.196 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18025 0 0 0 77982 47 0 0 25 0 1 0 483648285 83283968 17707 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.196 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18027 0 0 0 78982 47 0 0 25 0 1 0 483648285 83283968 17709 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.196 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18027 0 0 0 79982 47 0 0 25 0 1 0 483648285 83283968 17709 4294967295 134512640 134672761 3221224544 3221223696 134565086 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.197 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18028 0 0 0 80982 47 0 0 25 0 1 0 483648285 83283968 17710 4294967295 134512640 134672761 3221224544 3221223728 134556589 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.197 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18029 0 0 0 81982 47 0 0 25 0 1 0 483648285 83283968 17711 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17711 603 41 0 20292 0
vsize: 81332
[startup+830.197 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18029 0 0 0 82983 47 0 0 25 0 1 0 483648285 83283968 17711 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.197 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18030 0 0 0 83983 47 0 0 25 0 1 0 483648285 83283968 17712 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17712 603 41 0 20292 0
vsize: 81332
[startup+850.197 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18035 0 0 0 84983 47 0 0 25 0 1 0 483648285 83283968 17717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17717 603 41 0 20292 0
vsize: 81332
[startup+860.198 s]
Raw data (loadavg): 1.08 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18039 0 0 0 85983 48 0 0 25 0 1 0 483648285 83283968 17721 4294967295 134512640 134672761 3221224544 3221223716 134556680 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.199 s]
Raw data (loadavg): 1.07 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18039 0 0 0 86983 48 0 0 25 0 1 0 483648285 83283968 17721 4294967295 134512640 134672761 3221224544 3221223680 134560677 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.199 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18039 0 0 0 87983 48 0 0 25 0 1 0 483648285 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+890.199 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18039 0 0 0 88983 48 0 0 25 0 1 0 483648285 83283968 17721 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.199 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18039 0 0 0 89983 48 0 0 25 0 1 0 483648285 83283968 17721 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.2 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18041 0 0 0 90984 48 0 0 25 0 1 0 483648285 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17723 603 41 0 20292 0
vsize: 81332
[startup+920.2 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18041 0 0 0 91984 48 0 0 25 0 1 0 483648285 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.2 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18041 0 0 0 92984 48 0 0 25 0 1 0 483648285 83283968 17723 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.201 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18042 0 0 0 93984 48 0 0 25 0 1 0 483648285 83283968 17724 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17724 603 41 0 20292 0
vsize: 81332
[startup+950.201 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18043 0 0 0 94984 48 0 0 25 0 1 0 483648285 83283968 17725 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17725 603 41 0 20292 0
vsize: 81332
[startup+960.201 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18043 0 0 0 95985 48 0 0 25 0 1 0 483648285 83283968 17725 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.202 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18044 0 0 0 96985 48 0 0 25 0 1 0 483648285 83283968 17726 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.202 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18044 0 0 0 97985 48 0 0 25 0 1 0 483648285 83283968 17726 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.202 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18046 0 0 0 98985 48 0 0 25 0 1 0 483648285 83283968 17728 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17728 603 41 0 20292 0
vsize: 81332
[startup+1000.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18046 0 0 0 99985 48 0 0 25 0 1 0 483648285 83283968 17728 4294967295 134512640 134672761 3221224544 3221223712 134560988 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.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18047 0 0 0 100985 48 0 0 25 0 1 0 483648285 83283968 17729 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17729 603 41 0 20292 0
vsize: 81332
[startup+1020.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18047 0 0 0 101986 48 0 0 25 0 1 0 483648285 83283968 17729 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18052 0 0 0 102986 48 0 0 25 0 1 0 483648285 83427328 17734 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17734 603 41 0 20327 0
vsize: 81472
[startup+1040.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18052 0 0 0 103986 48 0 0 25 0 1 0 483648285 83427328 17734 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18053 0 0 0 104986 48 0 0 25 0 1 0 483648285 83427328 17735 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17735 603 41 0 20327 0
vsize: 81472
[startup+1060.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18053 0 0 0 105986 48 0 0 25 0 1 0 483648285 83427328 17735 4294967295 134512640 134672761 3221224544 3221223668 134566059 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.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18053 0 0 0 106987 48 0 0 25 0 1 0 483648285 83427328 17735 4294967295 134512640 134672761 3221224544 3221223712 134560898 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): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18055 0 0 0 107987 48 0 0 25 0 1 0 483648285 83427328 17737 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1090.21 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18055 0 0 0 108986 48 0 0 25 0 1 0 483648285 83427328 17737 4294967295 134512640 134672761 3221224544 3221223712 134561011 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.2 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18055 0 0 0 109987 48 0 0 25 0 1 0 483648285 83427328 17737 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1110.21 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18055 0 0 0 110987 48 0 0 25 0 1 0 483648285 83427328 17737 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17737 603 41 0 20327 0
vsize: 81472
[startup+1120.21 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18058 0 0 0 111987 48 0 0 25 0 1 0 483648285 83427328 17740 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17740 603 41 0 20327 0
vsize: 81472
[startup+1130.21 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18064 0 0 0 112988 48 0 0 25 0 1 0 483648285 83427328 17746 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17746 603 41 0 20327 0
vsize: 81472
[startup+1140.21 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18065 0 0 0 113988 48 0 0 25 0 1 0 483648285 83427328 17747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17747 603 41 0 20327 0
vsize: 81472
[startup+1150.21 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18066 0 0 0 114988 48 0 0 25 0 1 0 483648285 83427328 17748 4294967295 134512640 134672761 3221224544 3221223796 134562288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17748 603 41 0 20327 0
vsize: 81472
[startup+1160.22 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18069 0 0 0 115989 48 0 0 25 0 1 0 483648285 83427328 17751 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17751 603 41 0 20327 0
vsize: 81472
[startup+1170.22 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18069 0 0 0 116989 48 0 0 25 0 1 0 483648285 83427328 17751 4294967295 134512640 134672761 3221224544 3221223668 134566043 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): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18073 0 0 0 117989 48 0 0 25 0 1 0 483648285 83427328 17755 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17755 603 41 0 20327 0
vsize: 81472
[startup+1190.22 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18074 0 0 0 118990 48 0 0 25 0 1 0 483648285 83427328 17756 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 17756 603 41 0 20327 0
vsize: 81472
[startup+1200.22 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 27609
Raw data (stat): 27609 (minisat+) R 27608 29151 29150 0 -1 0 18074 0 0 0 119990 48 0 0 25 0 1 0 483648285 83427328 17756 4294967295 134512640 134672761 3221224544 3221223752 134561960 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.26 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 27609
Raw data (stat): 27609 (minisat+) Z 27608 29151 29150 0 -1 12 18076 0 0 0 119990 52 0 0 25 0 1 0 483648285 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.26
CPU time (s): 1200.42
CPU user time (s): 1199.9
CPU system time (s): 0.52092
CPU usage (%): 100.013
Max. virtual memory (Kb): 81472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####