PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0548.opb
MD5SUM	6f47095f2d417d23ced995954e641689
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	14938
Optimality of the best value was proved	NO
Number of terms in the objective function	416
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	96797
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	96797
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1236.51
Number of variables	548
Total number of constraints	724
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	550
Number of constraints which are nor clauses,nor cardinality constraints	134
Minimum length of a constraint	1
Maximum length of a constraint	143
Trace number 16922

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        870164 kB
Buffers:         13412 kB
Cached:         124020 kB
SwapCached:       1968 kB
Active:          28496 kB
Inactive:       112612 kB
HighTotal:      131008 kB
HighFree:        31052 kB
LowTotal:       903652 kB
LowFree:        839112 kB
SwapTotal:     2097892 kB
SwapFree:      2095196 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            17628 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:24:11 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 12165 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 156 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssss.s..ssss........................................
c ---[ 164]---> Adder-cost: 66   maxlim: 856   bits: 11/10
c ---[ 163]---> Adder-cost: 73   maxlim: 258   bits: 10/9
c ---[ 162]---> Adder-cost: 56   maxlim: 650   bits: 11/10
c ---[ 161]---> Adder-cost: 64   maxlim: 847   bits: 11/10
c ---[ 160]---> Adder-cost: 69   maxlim: 354   bits: 10/9
c ---[ 159]---> Adder-cost: 50   maxlim: 668   bits: 11/10
c ---[ 157]---> Adder-cost: 73   maxlim: 419   bits: 10/9
c ---[ 156]---> Adder-cost: 61   maxlim: 227   bits: 9/8
c ---[ 154]---> Adder-cost: 67   maxlim: 479   bits: 10/9
c ---[ 153]---> Adder-cost: 34   maxlim: 106   bits: 8/7
c ---[ 152]---> Adder-cost: 92   maxlim: 333   bits: 10/9
c ---[ 151]---> Adder-cost: 77   maxlim: 407   bits: 10/9
c ---[ 150]---> Adder-cost: 82   maxlim: 615   bits: 11/10
c ---[ 149]---> Adder-cost: 96   maxlim: 1156   bits: 12/11
c ---[ 148]---> Adder-cost: 34   maxlim: 332   bits: 10/9
c ---[ 147]---> Adder-cost: 86   maxlim: 433   bits: 10/9
c ---[ 146]---> Adder-cost: 77   maxlim: 385   bits: 10/9
c ---[ 145]---> Adder-cost: 88   maxlim: 1134   bits: 12/11
c ---[ 144]---> Adder-cost: 93   maxlim: 249   bits: 9/8
c ---[ 143]---> Adder-cost: 100   maxlim: 295   bits: 10/9
c ---[ 142]---> Adder-cost: 97   maxlim: 249   bits: 9/8
c ---[ 141]---> Adder-cost: 108   maxlim: 494   bits: 10/9
c ---[ 140]---> Adder-cost: 98   maxlim: 506   bits: 10/9
c ---[ 139]---> Adder-cost: 53   maxlim: 259   bits: 10/9
c ---[ 138]---> Adder-cost: 55   maxlim: 439   bits: 10/9
c ---[ 136]---> Adder-cost: 61   maxlim: 393   bits: 10/9
c ---[ 135]---> Adder-cost: 94   maxlim: 1081   bits: 12/11
c ---[ 134]---> Adder-cost: 86   maxlim: 681   bits: 11/10
c ---[ 133]---> Adder-cost: 82   maxlim: 512   bits: 11/10
c ---[ 131]---> Adder-cost: 88   maxlim: 558   bits: 11/10
c ---[ 130]---> Adder-cost: 36   maxlim: 441   bits: 10/9
c ---[ 129]---> Adder-cost: 67   maxlim: 430   bits: 10/9
c ---[ 128]---> Adder-cost: 61   maxlim: 482   bits: 10/9
c ---[ 127]---> Adder-cost: 46   maxlim: 819   bits: 11/10
c ---[ 126]---> Adder-cost: 47   maxlim: 275   bits: 10/9
c ---[ 125]---> Adder-cost: 51   maxlim: 308   bits: 10/9
c ---[ 123]---> Adder-cost: 53   maxlim: 894   bits: 11/10
c ---[ 121]---> Adder-cost: 36   maxlim: 131   bits: 9/8
c ---[ 120]---> Adder-cost: 45   maxlim: 730   bits: 11/10
c ---[ 119]---> Adder-cost: 38   maxlim: 121   bits: 8/7
c ---[ 118]---> Adder-cost: 64   maxlim: 932   bits: 11/10
c ---[ 117]---> Adder-cost: 53   maxlim: 733   bits: 11/10
c ---[ 116]---> Adder-cost: 43   maxlim: 751   bits: 11/10
c ---[ 115]---> Adder-cost: 58   maxlim: 837   bits: 11/10
c ---[ 114]---> Adder-cost: 41   maxlim: 605   bits: 11/10
c ---[ 112]---> Adder-cost: 22   maxlim: 405   bits: 10/9
c ---[ 111]---> Adder-cost: 62   maxlim: 1052   bits: 12/11
c ---[ 110]---> Adder-cost: 53   maxlim: 811   bits: 11/10
c ---[ 109]---> Adder-cost: 47   maxlim: 603   bits: 11/10
c ---[ 107]---> Adder-cost: 18   maxlim: 360   bits: 10/9
c ---[ 106]---> Adder-cost: 47   maxlim: 785   bits: 11/10
c ---[ 105]---> Adder-cost: 49   maxlim: 833   bits: 11/10
c ---[ 104]---> Adder-cost: 49   maxlim: 0   bits: 1/0
c ---[ 103]---> Adder-cost: 59   maxlim: 1277   bits: 12/11
c ---[ 102]---> Adder-cost: 60   maxlim: 1324   bits: 12/11
c ---[ 101]---> Adder-cost: 67   maxlim: 1287   bits: 12/11
c ---[ 100]---> Adder-cost: 62   maxlim: 1125   bits: 12/11
c ---[  99]---> Adder-cost: 61   maxlim: 933   bits: 11/10
c ---[  98]---> Adder-cost: 41   maxlim: 715   bits: 11/10
c ---[  97]---> Adder-cost: 47   maxlim: 374   bits: 10/9
c ---[  96]---> Adder-cost: 72   maxlim: 972   bits: 11/10
c ---[  95]---> Adder-cost: 50   maxlim: 684   bits: 11/10
c ---[  93]---> Adder-cost: 64   maxlim: 390   bits: 10/9
c ---[  92]---> Adder-cost: 55   maxlim: 731   bits: 11/10
c ---[  91]---> Adder-cost: 61   maxlim: 866   bits: 11/10
c ---[  90]---> Adder-cost: 88   maxlim: 1313   bits: 12/11
c ---[  89]---> Adder-cost: 59   maxlim: 888   bits: 11/10
c ---[  88]---> Adder-cost: 28   maxlim: 141   bits: 9/8
c ---[  87]---> Adder-cost: 39   maxlim: 694   bits: 11/10
c ---[  86]---> Adder-cost: 25   maxlim: 447   bits: 10/9
c ---[  83]---> Adder-cost: 39   maxlim: 751   bits: 11/10
c ---[  81]---> Adder-cost: 28   maxlim: 646   bits: 11/10
c ---[  80]---> Adder-cost: 750   maxlim: 2650   bits: 13/12
c ---[  79]---> Adder-cost: 126   maxlim: 381   bits: 10/9
c ---[  78]---> Adder-cost: 171   maxlim: 103   bits: 8/7
c ---[  77]---> Adder-cost: 190   maxlim: 736   bits: 10/10
c ---[  76]---> Adder-cost: 48   maxlim: 173   bits: 8/8
c ---[  75]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  71]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  69]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  55]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  53]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  47]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  33]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  31]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  25]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  19]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[  17]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 98   maxlim: 48   bits: 7/6
c ---[  12]---> Adder-cost: 98   maxlim: 48   bits: 7/6
c ---[  11]---> Adder-cost: 52   maxlim: 25   bits: 6/5
c ---[  10]---> Adder-cost: 10   maxlim: 4   bits: 4/3
c ---[   9]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[   8]---> Adder-cost: 28   maxlim: 114   bits: 8/7
c ---[   7]---> Adder-cost: 24   maxlim: 141   bits: 9/8
c ---[   6]---> Adder-cost: 26   maxlim: 105   bits: 8/7
c ---[   5]---> Adder-cost: 50   maxlim: 158   bits: 9/8
c ---[   4]---> Adder-cost: 21   maxlim: 83   bits: 8/7
c ---[   3]---> Adder-cost: 4   maxlim: 68   bits: 8/7
c ---[   2]---> Adder-cost: 33   maxlim: 122   bits: 8/7
c ---[   1]---> Adder-cost: 4   maxlim: 68   bits: 8/7
c ---[   0]---> Adder-cost: 16   maxlim: 82   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38053   135144 |   12684       0        0     nan |  0.000 % |
c |       100 |   38046   135121 |   13952      98      344     3.5 |  6.965 % |
c |       250 |   38046   135121 |   15347     248     1172     4.7 |  6.965 % |
c |       475 |   38046   135121 |   16882     473     2437     5.2 |  6.965 % |
c |       813 |   38046   135121 |   18570     811     5286     6.5 |  6.965 % |
c |      1319 |   38046   135121 |   20427    1317    11341     8.6 |  6.965 % |
c |      2079 |   38046   135121 |   22470    2077    26694    12.9 |  6.965 % |
c |      3218 |   38000   134951 |   24717    3211    50668    15.8 |  6.979 % |
c |      4926 |   38000   134951 |   27189    4919    95762    19.5 |  6.979 % |
c |      7494 |   38000   134951 |   29908    7487   192830    25.8 |  6.979 % |
c |     11338 |   38000   134951 |   32899   11331   351409    31.0 |  6.979 % |
c |     17105 |   38000   134951 |   36188   17098   551679    32.3 |  6.979 % |
c |     25757 |   38000   134951 |   39807   25750   903072    35.1 |  6.979 % |
c |     38731 |   37995   134935 |   43788   38723  1593201    41.1 |  6.993 % |
c |     58193 |   37995   134935 |   48167   27938   973445    34.8 |  6.993 % |
c |     87387 |   37995   134935 |   52984   22059  1143015    51.8 |  6.993 % |
c |    131176 |   37995   134935 |   58282   26575  1093824    41.2 |  6.993 % |
c |    196860 |   37995   134935 |   64110   50068  2036691    40.7 |  6.993 % |
c |    295386 |   37995   134935 |   70521   51695  3048990    59.0 |  6.993 % |
c |    443176 |   37995   134935 |   77574   40603  1677127    41.3 |  6.993 % |
c |    664859 |   37927   134690 |   85331   73978  4091325    55.3 |  7.022 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.91 2/54 28029
Raw data (stat): 28029 (runsolver) R 28028 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543852205 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.0008 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 1990 0 0 0 993 5 0 0 25 0 1 0 543852205 9945088 1967 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2428 1967 603 41 0 2387 0
vsize: 9712
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 2779 0 0 0 1991 7 0 0 25 0 1 0 543852205 13299712 2756 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3247 2756 603 41 0 3206 0
vsize: 12988
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 3225 0 0 0 2990 8 0 0 25 0 1 0 543852205 15048704 3202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3674 3202 603 41 0 3633 0
vsize: 14696
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 3269 0 0 0 3990 9 0 0 25 0 1 0 543852205 15319040 3246 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3246 603 41 0 3699 0
vsize: 14960
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 3269 0 0 0 4989 9 0 0 25 0 1 0 543852205 15319040 3246 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3740 3246 603 41 0 3699 0
vsize: 14960
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 3376 0 0 0 5989 9 0 0 25 0 1 0 543852205 15716352 3353 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3837 3353 603 41 0 3796 0
vsize: 15348
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 3741 0 0 0 6988 11 0 0 25 0 1 0 543852205 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 3741 0 0 0 7987 12 0 0 25 0 1 0 543852205 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 3741 0 0 0 8987 12 0 0 25 0 1 0 543852205 17182720 3718 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3718 603 41 0 4154 0
vsize: 16780
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 28029
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4103 0 0 0 9986 13 0 0 25 0 1 0 543852205 18665472 4080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4557 4080 603 41 0 4516 0
vsize: 18228
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4191 0 0 0 10986 13 0 0 25 0 1 0 543852205 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4191 0 0 0 11986 13 0 0 25 0 1 0 543852205 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4191 0 0 0 12987 13 0 0 25 0 1 0 543852205 19062784 4168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4168 603 41 0 4613 0
vsize: 18616
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4192 0 0 0 13987 13 0 0 25 0 1 0 543852205 19062784 4169 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4169 603 41 0 4613 0
vsize: 18616
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4197 0 0 0 14987 13 0 0 25 0 1 0 543852205 19062784 4174 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4174 603 41 0 4613 0
vsize: 18616
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4412 0 0 0 15986 14 0 0 25 0 1 0 543852205 20013056 4389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4389 603 41 0 4845 0
vsize: 19544
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4450 0 0 0 16986 14 0 0 25 0 1 0 543852205 20148224 4427 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4450 0 0 0 17987 14 0 0 25 0 1 0 543852205 20148224 4427 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4427 603 41 0 4878 0
vsize: 19676
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4460 0 0 0 18987 14 0 0 25 0 1 0 543852205 20148224 4437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4437 603 41 0 4878 0
vsize: 19676
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4461 0 0 0 19987 14 0 0 25 0 1 0 543852205 20148224 4438 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4438 603 41 0 4878 0
vsize: 19676
[startup+210.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4467 0 0 0 20987 14 0 0 25 0 1 0 543852205 20148224 4444 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4919 4444 603 41 0 4878 0
vsize: 19676
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4468 0 0 0 21986 14 0 0 25 0 1 0 543852205 20148224 4445 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4919 4445 603 41 0 4878 0
vsize: 19676
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4712 0 0 0 22985 16 0 0 25 0 1 0 543852205 21213184 4689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5179 4689 603 41 0 5138 0
vsize: 20716
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4974 0 0 0 23984 17 0 0 25 0 1 0 543852205 22282240 4951 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4951 603 41 0 5399 0
vsize: 21760
[startup+250.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4983 0 0 0 24984 17 0 0 25 0 1 0 543852205 22282240 4960 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4960 603 41 0 5399 0
vsize: 21760
[startup+260.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4986 0 0 0 25985 17 0 0 25 0 1 0 543852205 22282240 4963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4963 603 41 0 5399 0
vsize: 21760
[startup+270.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4986 0 0 0 26985 17 0 0 25 0 1 0 543852205 22282240 4963 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5440 4963 603 41 0 5399 0
vsize: 21760
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 4998 0 0 0 27985 17 0 0 25 0 1 0 543852205 22462464 4975 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5484 4975 603 41 0 5443 0
vsize: 21936
[startup+290.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 5002 0 0 0 28985 17 0 0 25 0 1 0 543852205 22462464 4979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5484 4979 603 41 0 5443 0
vsize: 21936
[startup+300.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 5108 0 0 0 29985 17 0 0 25 0 1 0 543852205 22843392 5085 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5577 5085 603 41 0 5536 0
vsize: 22308
[startup+310.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 5381 0 0 0 30985 18 0 0 25 0 1 0 543852205 24039424 5358 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5869 5358 603 41 0 5828 0
vsize: 23476
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 5660 0 0 0 31984 19 0 0 25 0 1 0 543852205 25100288 5637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6128 5637 603 41 0 6087 0
vsize: 24512
[startup+330.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 5906 0 0 0 32983 19 0 0 25 0 1 0 543852205 26161152 5883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6387 5883 603 41 0 6346 0
vsize: 25548
[startup+340.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6144 0 0 0 33983 20 0 0 25 0 1 0 543852205 27160576 6121 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6631 6121 603 41 0 6590 0
vsize: 26524
[startup+350.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6284 0 0 0 34983 21 0 0 25 0 1 0 543852205 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+360.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6284 0 0 0 35983 21 0 0 25 0 1 0 543852205 27885568 6261 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+370.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6284 0 0 0 36983 21 0 0 25 0 1 0 543852205 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+380.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6284 0 0 0 37983 21 0 0 25 0 1 0 543852205 27885568 6261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6261 603 41 0 6767 0
vsize: 27232
[startup+390.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6291 0 0 0 38983 21 0 0 25 0 1 0 543852205 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+400.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6291 0 0 0 39983 21 0 0 25 0 1 0 543852205 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+410.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6291 0 0 0 40984 21 0 0 25 0 1 0 543852205 27885568 6268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6268 603 41 0 6767 0
vsize: 27232
[startup+420.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6294 0 0 0 41983 21 0 0 25 0 1 0 543852205 27885568 6271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6808 6271 603 41 0 6767 0
vsize: 27232
[startup+430.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6298 0 0 0 42983 21 0 0 25 0 1 0 543852205 28147712 6275 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6275 603 41 0 6831 0
vsize: 27488
[startup+440.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6301 0 0 0 43983 21 0 0 25 0 1 0 543852205 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+450.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6301 0 0 0 44983 21 0 0 25 0 1 0 543852205 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+460.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6301 0 0 0 45983 21 0 0 25 0 1 0 543852205 28147712 6278 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6278 603 41 0 6831 0
vsize: 27488
[startup+470.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6306 0 0 0 46983 21 0 0 25 0 1 0 543852205 28147712 6283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6872 6283 603 41 0 6831 0
vsize: 27488
[startup+480.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6319 0 0 0 47984 21 0 0 25 0 1 0 543852205 28299264 6296 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6296 603 41 0 6868 0
vsize: 27636
[startup+490.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6326 0 0 0 48984 21 0 0 25 0 1 0 543852205 28299264 6303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6303 603 41 0 6868 0
vsize: 27636
[startup+500.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6355 0 0 0 49984 21 0 0 25 0 1 0 543852205 28463104 6332 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6949 6332 603 41 0 6908 0
vsize: 27796
[startup+510.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6375 0 0 0 50984 21 0 0 25 0 1 0 543852205 28463104 6352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6949 6352 603 41 0 6908 0
vsize: 27796
[startup+520.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6385 0 0 0 51984 21 0 0 25 0 1 0 543852205 28626944 6362 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+530.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6385 0 0 0 52984 21 0 0 25 0 1 0 543852205 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+540.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6385 0 0 0 53984 21 0 0 25 0 1 0 543852205 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+550.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6385 0 0 0 54985 21 0 0 25 0 1 0 543852205 28626944 6362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6362 603 41 0 6948 0
vsize: 27956
[startup+560.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6387 0 0 0 55985 21 0 0 25 0 1 0 543852205 28626944 6364 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6364 603 41 0 6948 0
vsize: 27956
[startup+570.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6387 0 0 0 56985 21 0 0 25 0 1 0 543852205 28626944 6364 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6364 603 41 0 6948 0
vsize: 27956
[startup+580.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6388 0 0 0 57985 21 0 0 25 0 1 0 543852205 28626944 6365 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6365 603 41 0 6948 0
vsize: 27956
[startup+590.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6399 0 0 0 58985 21 0 0 25 0 1 0 543852205 28626944 6376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6376 603 41 0 6948 0
vsize: 27956
[startup+600.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6419 0 0 0 59985 22 0 0 25 0 1 0 543852205 28823552 6396 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6396 603 41 0 6996 0
vsize: 28148
[startup+610.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 60986 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+620.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 61986 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+630.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 62986 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+640.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 63986 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+650.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 64986 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+660.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 65985 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+670.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 66985 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+680.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 67985 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+690.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6435 0 0 0 68986 22 0 0 25 0 1 0 543852205 28823552 6412 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6412 603 41 0 6996 0
vsize: 28148
[startup+700.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6438 0 0 0 69986 22 0 0 25 0 1 0 543852205 28823552 6415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6415 603 41 0 6996 0
vsize: 28148
[startup+710.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6442 0 0 0 70986 22 0 0 25 0 1 0 543852205 28823552 6419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6419 603 41 0 6996 0
vsize: 28148
[startup+720.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6449 0 0 0 71986 22 0 0 25 0 1 0 543852205 28823552 6426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6426 603 41 0 6996 0
vsize: 28148
[startup+730.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6450 0 0 0 72986 22 0 0 25 0 1 0 543852205 28823552 6427 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6427 603 41 0 6996 0
vsize: 28148
[startup+740.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6467 0 0 0 73986 22 0 0 25 0 1 0 543852205 28987392 6444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7077 6444 603 41 0 7036 0
vsize: 28308
[startup+750.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6468 0 0 0 74987 22 0 0 25 0 1 0 543852205 28987392 6445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7077 6445 603 41 0 7036 0
vsize: 28308
[startup+760.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6474 0 0 0 75987 22 0 0 25 0 1 0 543852205 28987392 6451 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7077 6451 603 41 0 7036 0
vsize: 28308
[startup+770.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6489 0 0 0 76987 22 0 0 25 0 1 0 543852205 29151232 6466 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7117 6466 603 41 0 7076 0
vsize: 28468
[startup+780.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6496 0 0 0 77987 22 0 0 25 0 1 0 543852205 29151232 6473 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7117 6473 603 41 0 7076 0
vsize: 28468
[startup+790.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6515 0 0 0 78987 22 0 0 25 0 1 0 543852205 29151232 6492 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7117 6492 603 41 0 7076 0
vsize: 28468
[startup+800.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6588 0 0 0 79987 22 0 0 25 0 1 0 543852205 29499392 6565 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7202 6565 603 41 0 7161 0
vsize: 28808
[startup+810.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6662 0 0 0 80987 22 0 0 25 0 1 0 543852205 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+820.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6662 0 0 0 81987 22 0 0 25 0 1 0 543852205 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+830.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6662 0 0 0 82988 22 0 0 25 0 1 0 543852205 29904896 6639 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6639 603 41 0 7260 0
vsize: 29204
[startup+840.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6664 0 0 0 83988 22 0 0 25 0 1 0 543852205 29904896 6641 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6641 603 41 0 7260 0
vsize: 29204
[startup+850.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6674 0 0 0 84988 22 0 0 25 0 1 0 543852205 29904896 6651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6651 603 41 0 7260 0
vsize: 29204
[startup+860.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6681 0 0 0 85988 22 0 0 25 0 1 0 543852205 29904896 6658 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7301 6658 603 41 0 7260 0
vsize: 29204
[startup+870.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6697 0 0 0 86988 23 0 0 25 0 1 0 543852205 30040064 6674 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7334 6674 603 41 0 7293 0
vsize: 29336
[startup+880.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6704 0 0 0 87989 23 0 0 25 0 1 0 543852205 30040064 6681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7334 6681 603 41 0 7293 0
vsize: 29336
[startup+890.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6704 0 0 0 88989 23 0 0 25 0 1 0 543852205 30040064 6681 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7334 6681 603 41 0 7293 0
vsize: 29336
[startup+900.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6720 0 0 0 89989 23 0 0 25 0 1 0 543852205 30203904 6697 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6697 603 41 0 7333 0
vsize: 29496
[startup+910.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6725 0 0 0 90989 23 0 0 25 0 1 0 543852205 30203904 6702 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6702 603 41 0 7333 0
vsize: 29496
[startup+920.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 91989 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+930.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 92989 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+940.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 93990 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+950.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 94990 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+960.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 95990 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+970.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 96990 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+980.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 97990 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+990.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 98991 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6734 0 0 0 99991 23 0 0 25 0 1 0 543852205 30203904 6711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7374 6711 603 41 0 7333 0
vsize: 29496
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 6788 0 0 0 100991 23 0 0 25 0 1 0 543852205 30474240 6765 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7440 6765 603 41 0 7399 0
vsize: 29760
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7063 0 0 0 101990 23 0 0 25 0 1 0 543852205 31678464 7040 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7734 7040 603 41 0 7693 0
vsize: 30936
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7315 0 0 0 102990 24 0 0 25 0 1 0 543852205 32747520 7292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7995 7292 603 41 0 7954 0
vsize: 31980
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7548 0 0 0 103988 25 0 0 25 0 1 0 543852205 33685504 7525 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8224 7525 603 41 0 8183 0
vsize: 32896
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7794 0 0 0 104988 26 0 0 25 0 1 0 543852205 34627584 7771 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8454 7771 603 41 0 8413 0
vsize: 33816
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7939 0 0 0 105988 26 0 0 25 0 1 0 543852205 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7939 0 0 0 106988 26 0 0 25 0 1 0 543852205 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7939 0 0 0 107988 26 0 0 25 0 1 0 543852205 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7939 0 0 0 108988 26 0 0 25 0 1 0 543852205 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7939 0 0 0 109988 26 0 0 25 0 1 0 543852205 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7939 0 0 0 110988 26 0 0 25 0 1 0 543852205 35164160 7916 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8585 7916 603 41 0 8544 0
vsize: 34340
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7950 0 0 0 111989 26 0 0 25 0 1 0 543852205 35315712 7927 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8622 7927 603 41 0 8581 0
vsize: 34488
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 7970 0 0 0 112989 26 0 0 25 0 1 0 543852205 35315712 7947 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8622 7947 603 41 0 8581 0
vsize: 34488
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 8003 0 0 0 113989 26 0 0 25 0 1 0 543852205 35479552 7980 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8662 7980 603 41 0 8621 0
vsize: 34648
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 8007 0 0 0 114989 26 0 0 25 0 1 0 543852205 35479552 7984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8662 7984 603 41 0 8621 0
vsize: 34648
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 8008 0 0 0 115989 26 0 0 25 0 1 0 543852205 35479552 7985 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8662 7985 603 41 0 8621 0
vsize: 34648
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 8022 0 0 0 116989 26 0 0 25 0 1 0 543852205 35676160 7999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 7999 603 41 0 8669 0
vsize: 34840
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 8032 0 0 0 117990 26 0 0 25 0 1 0 543852205 35676160 8009 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 8009 603 41 0 8669 0
vsize: 34840
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 8035 0 0 0 118990 26 0 0 25 0 1 0 543852205 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 28031
Raw data (stat): 28029 (minisat+) R 28028 27222 27221 0 -1 0 8035 0 0 0 119990 26 0 0 25 0 1 0 543852205 35676160 8012 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8710 8012 603 41 0 8669 0
vsize: 34840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 28031
Raw data (stat): 28029 (minisat+) Z 28028 27222 27221 0 -1 12 8037 0 0 0 119990 28 0 0 25 0 1 0 543852205 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.04
CPU time (s): 1200.19
CPU user time (s): 1199.9
CPU system time (s): 0.284956
CPU usage (%): 100.013
Max. virtual memory (Kb): 34840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####