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-markshare2.opb
MD5SUM	b54bb080800e2327586cd478559c04ff
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10368
Optimality of the best value was proved	NO
Number of terms in the objective function	140
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	200
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 18111

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        675328 kB
Buffers:         31400 kB
Cached:         305744 kB
SwapCached:          0 kB
Active:          80452 kB
Inactive:       259556 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        675076 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13512 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:55:40 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18525 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 431615   bits: 20/19
c ---[  10]---> Adder-cost: 380   maxlim: 461183   bits: 20/19
c ---[   8]---> Adder-cost: 350   maxlim: 445183   bits: 20/19
c ---[   6]---> Adder-cost: 340   maxlim: 477951   bits: 20/19
c ---[   4]---> Adder-cost: 390   maxlim: 451839   bits: 20/19
c ---[   2]---> Adder-cost: 358   maxlim: 468735   bits: 20/19
c ---[   0]---> Adder-cost: 374   maxlim: 444543   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17222    61228 |    6314     100      436     4.4 |  9.969 % |
c |       251 |   17222    61228 |    6945     251     1589     6.3 |  9.969 % |
c |       476 |   17222    61228 |    7639     476     4122     8.7 |  9.969 % |
c ==============================================================================
c [1mFound solution: 651648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       699 |   20136    68102 |    6712     699    10913    15.6 |  9.969 % |
c |       799 |   20128    68076 |    7383     798    21519    27.0 |  7.575 % |
c |       949 |   20128    68076 |    8121     948    30181    31.8 |  7.575 % |
c ==============================================================================
c [1mFound solution: 612096[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1058 |   20209    68289 |    6736    1057    40766    38.6 |  7.575 % |
c |      1158 |   20209    68289 |    7409    1157    46287    40.0 |  7.570 % |
c |      1309 |   20209    68289 |    8150    1308    52924    40.5 |  7.570 % |
c |      1534 |   20209    68289 |    8965    1533    81998    53.5 |  7.570 % |
c |      1871 |   20209    68289 |    9862    1870   121887    65.2 |  7.570 % |
c |      2378 |   20185    68211 |   10848    2374   162760    68.6 |  7.648 % |
c ==============================================================================
c [1mFound solution: 574080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2793 |   20200    68242 |    6733    2788   210465    75.5 |  7.648 % |
c ==============================================================================
c [1mFound solution: 239872[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2845 |   20232    68318 |    6744    2840   211547    74.5 |  7.648 % |
c |      2946 |   20224    68292 |    7418    2940   214114    72.8 |  7.716 % |
c |      3097 |   20224    68292 |    8160    3091   215459    69.7 |  7.716 % |
c |      3322 |   20224    68292 |    8976    3316   226783    68.4 |  7.716 % |
c |      3659 |   20200    68214 |    9873    3650   253941    69.6 |  7.794 % |
c |      4166 |   20200    68214 |   10861    4157   276163    66.4 |  7.794 % |
c |      4925 |   20184    68162 |   11947    4914   293765    59.8 |  7.846 % |
c |      6066 |   20184    68162 |   13142    6055   389521    64.3 |  7.846 % |
c |      7774 |   20184    68162 |   14456    7763   530254    68.3 |  7.846 % |
c ==============================================================================
c [1mFound solution: 233472[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8457 |   20206    68216 |    6735    8446   554750    65.7 |  7.846 % |
c |      8557 |   20206    68216 |    7408    4323   242172    56.0 |  7.858 % |
c |      8707 |   20206    68216 |    8149    4473   243252    54.4 |  7.858 % |
c |      8932 |   20206    68216 |    8964    4698   245846    52.3 |  7.858 % |
c |      9270 |   20206    68216 |    9860    5036   254179    50.5 |  7.858 % |
c |      9779 |   20200    68198 |   10846    5544   268398    48.4 |  7.884 % |
c |     10539 |   20200    68198 |   11931    6304   294399    46.7 |  7.884 % |
c |     11680 |   20200    68198 |   13124    7445   351264    47.2 |  7.884 % |
c |     13388 |   20200    68198 |   14437    9153   446317    48.8 |  7.884 % |
c |     15950 |   20200    68198 |   15880   11715   577221    49.3 |  7.884 % |
c |     19794 |   20183    68145 |   17468   15557   857831    55.1 |  7.962 % |
c |     25561 |   20049    67812 |   19215   12157   724474    59.6 |  8.895 % |
c |     34210 |   20017    67733 |   21137   10751   499120    46.4 |  9.077 % |
c |     47184 |   20003    67697 |   23251   12920   530179    41.0 |  9.155 % |
c |     66646 |   20003    67697 |   25576   20218   949013    46.9 |  9.155 % |
c |     95838 |   19995    67671 |   28133   22421  1069802    47.7 |  9.181 % |
c |    139628 |   19995    67671 |   30947   21035  1279848    60.8 |  9.181 % |
c |    205312 |   19934    67518 |   34041   15912   771109    48.5 |  9.621 % |
c |    303841 |   19934    67518 |   37446   33182  1877834    56.6 |  9.621 % |
c |    451632 |   19924    67495 |   41190   22072  1191172    54.0 |  9.673 % |
c ==============================================================================
c [1mFound solution: 131456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    500118 |   19908    67463 |    6636   15146   633146    41.8 |  9.673 % |
c |    500219 |   19908    67463 |    7299    3888   123690    31.8 |  9.876 % |
c |    500369 |   19908    67463 |    8029    4038   126129    31.2 |  9.876 % |
c |    500594 |   19908    67463 |    8832    4263   130256    30.6 |  9.876 % |
c |    500931 |   19908    67463 |    9715    4600   136695    29.7 |  9.876 % |
c |    501437 |   19908    67463 |   10687    5106   149285    29.2 |  9.876 % |
c |    502197 |   19908    67463 |   11756    5866   170398    29.0 |  9.876 % |
c |    503336 |   19908    67463 |   12931    7005   219323    31.3 |  9.876 % |
c |    505044 |   19908    67463 |   14224    8713   304374    34.9 |  9.876 % |
c |    507606 |   19908    67463 |   15647   11275   412063    36.5 |  9.876 % |
c |    511451 |   19908    67463 |   17212   15120   602595    39.9 |  9.876 % |
c |    517218 |   19908    67463 |   18933   11593   389204    33.6 |  9.876 % |
c |    525867 |   19908    67463 |   20826   10250   426781    41.6 |  9.876 % |
c |    538842 |   19895    67433 |   22909   12420   530893    42.7 |  9.979 % |
c |    558303 |   19895    67433 |   25200   19850   991637    50.0 |  9.979 % |
c |    587498 |   19895    67433 |   27720   22344   834383    37.3 |  9.979 % |
c ==============================================================================
c [1mFound solution: 119552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    595514 |   19843    67252 |    6614   12662   510577    40.3 |  9.979 % |
c |    595614 |   19843    67252 |    7275    6431   251107    39.0 | 10.375 % |
c |    595765 |   19843    67252 |    8002    6582   254009    38.6 | 10.375 % |
c |    595990 |   19843    67252 |    8803    6807   259710    38.2 | 10.375 % |
c |    596328 |   19843    67252 |    9683    7145   268031    37.5 | 10.375 % |
c |    596835 |   19843    67252 |   10651    7652   288100    37.7 | 10.375 % |
c |    597594 |   19843    67252 |   11717    8411   306034    36.4 | 10.375 % |
c |    598736 |   19843    67252 |   12888    9553   344822    36.1 | 10.375 % |
c |    600446 |   19682    66882 |   14177   11248   423649    37.7 | 11.617 % |
c |    603008 |   19682    66882 |   15595   13810   528082    38.2 | 11.617 % |
c |    606852 |   19682    66882 |   17155    9379   323702    34.5 | 11.617 % |
c |    612618 |   19682    66882 |   18870   15145   566404    37.4 | 11.617 % |
c |    621269 |   19672    66859 |   20757   13664   620799    45.4 | 11.669 % |
c |    634243 |   19609    66707 |   22833   15806   725391    45.9 | 12.290 % |
c |    653705 |   19609    66707 |   25116   23281  1040677    44.7 | 12.290 % |
c |    682897 |   19609    66707 |   27628   26068  1393797    53.5 | 12.290 % |
c |    726686 |   19609    66707 |   30391   23711  1513201    63.8 | 12.290 % |
#### 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.53 0.83 0.86 2/54 31714
Raw data (stat): 31714 (runsolver) R 31713 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 473697999 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.60 0.83 0.86 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 1338 0 0 0 996 3 0 0 25 0 1 0 473697999 7069696 1316 4294967295 134512640 134672761 3221224544 3221223712 134560788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1726 1316 603 41 0 1685 0
vsize: 6904
[startup+20.0009 s]
Raw data (loadavg): 0.66 0.84 0.86 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 1605 0 0 0 1994 4 0 0 25 0 1 0 473697999 8192000 1583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2000 1583 603 41 0 1959 0
vsize: 8000
[startup+30.0023 s]
Raw data (loadavg): 0.71 0.84 0.86 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2007 0 0 0 2993 5 0 0 25 0 1 0 473697999 9854976 1985 4294967295 134512640 134672761 3221224544 3221223700 134565028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2406 1985 603 41 0 2365 0
vsize: 9624
[startup+40.0031 s]
Raw data (loadavg): 0.76 0.85 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2012 0 0 0 3993 6 0 0 25 0 1 0 473697999 9854976 1990 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2406 1990 603 41 0 2365 0
vsize: 9624
[startup+50.0034 s]
Raw data (loadavg): 0.79 0.85 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2195 0 0 0 4992 6 0 0 25 0 1 0 473697999 10649600 2173 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2600 2173 603 41 0 2559 0
vsize: 10400
[startup+60.0036 s]
Raw data (loadavg): 0.82 0.85 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2196 0 0 0 5992 6 0 0 25 0 1 0 473697999 10649600 2174 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2600 2174 603 41 0 2559 0
vsize: 10400
[startup+70.0041 s]
Raw data (loadavg): 0.85 0.86 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2196 0 0 0 6992 7 0 0 25 0 1 0 473697999 10649600 2174 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2600 2174 603 41 0 2559 0
vsize: 10400
[startup+80.0045 s]
Raw data (loadavg): 0.87 0.86 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2337 0 0 0 7992 7 0 0 25 0 1 0 473697999 11190272 2315 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2732 2315 603 41 0 2691 0
vsize: 10928
[startup+90.0046 s]
Raw data (loadavg): 0.89 0.87 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2444 0 0 0 8992 7 0 0 25 0 1 0 473697999 11595776 2422 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2422 603 41 0 2790 0
vsize: 11324
[startup+100.004 s]
Raw data (loadavg): 0.91 0.87 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2444 0 0 0 9992 8 0 0 25 0 1 0 473697999 11595776 2422 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2422 603 41 0 2790 0
vsize: 11324
[startup+110.005 s]
Raw data (loadavg): 0.92 0.87 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2444 0 0 0 10992 8 0 0 25 0 1 0 473697999 11595776 2422 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2422 603 41 0 2790 0
vsize: 11324
[startup+120.005 s]
Raw data (loadavg): 0.93 0.88 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2519 0 0 0 11992 8 0 0 25 0 1 0 473697999 11866112 2497 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2497 603 41 0 2856 0
vsize: 11588
[startup+130.006 s]
Raw data (loadavg): 0.94 0.88 0.87 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2801 0 0 0 12991 9 0 0 25 0 1 0 473697999 13070336 2779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3191 2779 603 41 0 3150 0
vsize: 12764
[startup+140.005 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2803 0 0 0 13991 9 0 0 25 0 1 0 473697999 13070336 2781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3191 2781 603 41 0 3150 0
vsize: 12764
[startup+150.005 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 2891 0 0 0 14991 9 0 0 25 0 1 0 473697999 13471744 2869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3289 2869 603 41 0 3248 0
vsize: 13156
[startup+160.006 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3091 0 0 0 15991 10 0 0 25 0 1 0 473697999 14266368 3069 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3483 3069 603 41 0 3442 0
vsize: 13932
[startup+170.006 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3108 0 0 0 16991 10 0 0 25 0 1 0 473697999 14417920 3086 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3520 3086 603 41 0 3479 0
vsize: 14080
[startup+180.007 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3115 0 0 0 17991 10 0 0 25 0 1 0 473697999 14417920 3093 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3520 3093 603 41 0 3479 0
vsize: 14080
[startup+190.008 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3370 0 0 0 18990 11 0 0 25 0 1 0 473697999 15519744 3348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3348 603 41 0 3748 0
vsize: 15156
[startup+200.007 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3371 0 0 0 19991 11 0 0 25 0 1 0 473697999 15519744 3349 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3349 603 41 0 3748 0
vsize: 15156
[startup+210.007 s]
Raw data (loadavg): 0.98 0.91 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3379 0 0 0 20990 11 0 0 25 0 1 0 473697999 15519744 3357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3357 603 41 0 3748 0
vsize: 15156
[startup+220.008 s]
Raw data (loadavg): 0.98 0.91 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 21990 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+230.008 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 22991 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+240.008 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 23991 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+250.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3382 0 0 0 24991 11 0 0 25 0 1 0 473697999 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+260.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3388 0 0 0 25991 11 0 0 25 0 1 0 473697999 15519744 3366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3366 603 41 0 3748 0
vsize: 15156
[startup+270.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3396 0 0 0 26991 11 0 0 25 0 1 0 473697999 15519744 3374 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3374 603 41 0 3748 0
vsize: 15156
[startup+280.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3406 0 0 0 27991 11 0 0 25 0 1 0 473697999 15663104 3384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3384 603 41 0 3783 0
vsize: 15296
[startup+290.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3406 0 0 0 28992 11 0 0 25 0 1 0 473697999 15663104 3384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3384 603 41 0 3783 0
vsize: 15296
[startup+300.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 29992 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+310.011 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 30992 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+320.011 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 31992 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223728 134559166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+330.012 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3413 0 0 0 32993 11 0 0 25 0 1 0 473697999 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+340.012 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3638 0 0 0 33992 11 0 0 25 0 1 0 473697999 16728064 3616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4084 3616 603 41 0 4043 0
vsize: 16336
[startup+350.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3651 0 0 0 34992 12 0 0 25 0 1 0 473697999 16728064 3629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4084 3629 603 41 0 4043 0
vsize: 16336
[startup+360.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3666 0 0 0 35992 12 0 0 25 0 1 0 473697999 16875520 3644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4120 3644 603 41 0 4079 0
vsize: 16480
[startup+370.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3667 0 0 0 36992 12 0 0 25 0 1 0 473697999 16875520 3645 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4120 3645 603 41 0 4079 0
vsize: 16480
[startup+380.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3800 0 0 0 37993 12 0 0 25 0 1 0 473697999 17408000 3778 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3778 603 41 0 4209 0
vsize: 17000
[startup+390.014 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 38993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+400.014 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 39993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+410.015 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 40993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+420.014 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 41993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+430.015 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 42993 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+440.015 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3809 0 0 0 43994 12 0 0 25 0 1 0 473697999 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+450.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3810 0 0 0 44994 12 0 0 25 0 1 0 473697999 17408000 3788 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3788 603 41 0 4209 0
vsize: 17000
[startup+460.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3861 0 0 0 45994 12 0 0 25 0 1 0 473697999 17682432 3839 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4317 3839 603 41 0 4276 0
vsize: 17268
[startup+470.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3869 0 0 0 46994 12 0 0 25 0 1 0 473697999 17682432 3847 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4317 3847 603 41 0 4276 0
vsize: 17268
[startup+480.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3877 0 0 0 47994 12 0 0 25 0 1 0 473697999 17682432 3855 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4317 3855 603 41 0 4276 0
vsize: 17268
[startup+490.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 3893 0 0 0 48994 12 0 0 25 0 1 0 473697999 17817600 3871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4350 3871 603 41 0 4309 0
vsize: 17400
[startup+500.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4049 0 0 0 49993 13 0 0 25 0 1 0 473697999 18497536 4027 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4516 4027 603 41 0 4475 0
vsize: 18064
[startup+510.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 50993 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+520.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 51993 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+530.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 52993 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+540.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 53994 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+550.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 54994 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+560.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4086 0 0 0 55994 13 0 0 25 0 1 0 473697999 18632704 4064 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+570.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4087 0 0 0 56994 13 0 0 25 0 1 0 473697999 18632704 4065 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4065 603 41 0 4508 0
vsize: 18196
[startup+580.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4092 0 0 0 57994 13 0 0 25 0 1 0 473697999 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4070 603 41 0 4508 0
vsize: 18196
[startup+590.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4092 0 0 0 58995 13 0 0 25 0 1 0 473697999 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4070 603 41 0 4508 0
vsize: 18196
[startup+600.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4092 0 0 0 59995 13 0 0 25 0 1 0 473697999 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4070 603 41 0 4508 0
vsize: 18196
[startup+610.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4095 0 0 0 60995 13 0 0 25 0 1 0 473697999 18632704 4073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4073 603 41 0 4508 0
vsize: 18196
[startup+620.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4098 0 0 0 61995 13 0 0 25 0 1 0 473697999 18632704 4076 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4076 603 41 0 4508 0
vsize: 18196
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4136 0 0 0 62995 13 0 0 25 0 1 0 473697999 18767872 4114 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4582 4114 603 41 0 4541 0
vsize: 18328
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4162 0 0 0 63995 13 0 0 25 0 1 0 473697999 18903040 4140 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4615 4140 603 41 0 4574 0
vsize: 18460
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4178 0 0 0 64995 13 0 0 25 0 1 0 473697999 19054592 4156 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 4156 603 41 0 4611 0
vsize: 18608
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4179 0 0 0 65996 13 0 0 25 0 1 0 473697999 19054592 4157 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 4157 603 41 0 4611 0
vsize: 18608
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4180 0 0 0 66996 13 0 0 25 0 1 0 473697999 19054592 4158 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 4158 603 41 0 4611 0
vsize: 18608
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4272 0 0 0 67996 14 0 0 25 0 1 0 473697999 19451904 4250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4749 4250 603 41 0 4708 0
vsize: 18996
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4327 0 0 0 68996 14 0 0 25 0 1 0 473697999 19587072 4305 4294967295 134512640 134672761 3221224544 3221223728 134558645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4782 4305 603 41 0 4741 0
vsize: 19128
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4330 0 0 0 69996 14 0 0 25 0 1 0 473697999 19587072 4308 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4782 4308 603 41 0 4741 0
vsize: 19128
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4335 0 0 0 70996 14 0 0 25 0 1 0 473697999 19722240 4313 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4313 603 41 0 4774 0
vsize: 19260
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4345 0 0 0 71996 14 0 0 25 0 1 0 473697999 19722240 4323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4323 603 41 0 4774 0
vsize: 19260
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 72997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 73997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 74997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 75997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223600 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4352 0 0 0 76997 14 0 0 25 0 1 0 473697999 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 77997 14 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 78998 14 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 79997 15 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 80997 15 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4415 0 0 0 81997 15 0 0 25 0 1 0 473697999 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 82997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 83996 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 84997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 85997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 86997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223680 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 87997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 88997 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 89998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 90998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 91998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 92998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 93998 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 94999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 95999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 96999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 97999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 98999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 99999 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 101000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 102000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 103000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 104000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 105000 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 106001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 107001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 108001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 109001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 110001 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 111002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 112002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 113002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 114002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 115002 15 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 116002 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 117002 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 118002 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 119003 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31714
Raw data (stat): 31714 (minisat+) R 31713 26667 26666 0 -1 0 4541 0 0 0 120003 16 0 0 25 0 1 0 473697999 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31714
Raw data (stat): 31714 (minisat+) Z 31713 26667 26666 0 -1 12 4544 0 0 0 120003 17 0 0 25 0 1 0 473697999 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.2
CPU user time (s): 1200.03
CPU system time (s): 0.170974
CPU usage (%): 100.013
Max. virtual memory (Kb): 20044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####