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-p0201.opb
MD5SUM	ffa3a55eb53181880328dd1b84f91e66
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1523
Optimality of the best value was proved	NO
Number of terms in the objective function	201
Biggest coefficient in the objective function	1920
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	19980
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	1920
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	19980
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	201
Total number of constraints	334
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	227
Number of constraints which are nor clauses,nor cardinality constraints	87
Minimum length of a constraint	1
Maximum length of a constraint	67
Trace number 22073

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        827312 kB
Buffers:         21612 kB
Cached:         150236 kB
SwapCached:      12296 kB
Active:          21276 kB
Inactive:       164620 kB
HighTotal:      131008 kB
HighFree:        77532 kB
LowTotal:       903652 kB
LowFree:        749780 kB
SwapTotal:     2097892 kB
SwapFree:      2085136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5204 kB
Slab:            15784 kB
Committed_AS:    63628 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:23:39 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 12126 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 133 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): sssss
c ---[ 137]---> Adder-cost: 7   maxlim: 5   bits: 4/3
c ---[ 136]---> Adder-cost: 7   maxlim: 5   bits: 4/3
c ---[ 135]---> Adder-cost: 7   maxlim: 5   bits: 4/3
c ---[ 133]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 131]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 129]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 127]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 125]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 123]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 121]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 119]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 117]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 115]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 113]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 111]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 109]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 107]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 105]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 103]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 101]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[  99]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[  97]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[  95]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[  89]---> Adder-cost: 42   maxlim: 9   bits: 5/4
c ---[  88]---> Adder-cost: 62   maxlim: 14   bits: 5/4
c ---[  87]---> Adder-cost: 62   maxlim: 14   bits: 5/4
c ---[  86]---> Adder-cost: 45   maxlim: 14   bits: 5/4
c ---[  85]---> Adder-cost: 53   maxlim: 19   bits: 6/5
c ---[  84]---> Adder-cost: 53   maxlim: 19   bits: 6/5
c ---[  83]---> Adder-cost: 57   maxlim: 19   bits: 6/5
c ---[  82]---> Adder-cost: 57   maxlim: 24   bits: 6/5
c ---[  81]---> Adder-cost: 57   maxlim: 24   bits: 6/5
c ---[  80]---> Adder-cost: 64   maxlim: 24   bits: 6/5
c ---[  79]---> Adder-cost: 65   maxlim: 29   bits: 6/5
c ---[  78]---> Adder-cost: 65   maxlim: 29   bits: 6/5
c ---[  77]---> Adder-cost: 71   maxlim: 29   bits: 6/5
c ---[  76]---> Adder-cost: 82   maxlim: 34   bits: 7/6
c ---[  75]---> Adder-cost: 82   maxlim: 34   bits: 7/6
c ---[  74]---> Adder-cost: 80   maxlim: 34   bits: 7/6
c ---[  73]---> Adder-cost: 78   maxlim: 39   bits: 7/6
c ---[  72]---> Adder-cost: 78   maxlim: 39   bits: 7/6
c ---[  71]---> Adder-cost: 83   maxlim: 39   bits: 7/6
c ---[  70]---> Adder-cost: 95   maxlim: 44   bits: 7/6
c ---[  69]---> Adder-cost: 95   maxlim: 44   bits: 7/6
c ---[  68]---> Adder-cost: 99   maxlim: 44   bits: 7/6
c ---[  67]---> Adder-cost: 91   maxlim: 49   bits: 7/6
c ---[  66]---> Adder-cost: 91   maxlim: 49   bits: 7/6
c ---[  65]---> Adder-cost: 100   maxlim: 49   bits: 7/6
c ---[  64]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  62]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  60]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  58]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  52]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  45]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  40]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  39]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  30]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  29]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  28]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  27]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  26]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  25]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  23]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  17]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  12]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  11]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  10]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   9]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   8]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   7]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   5]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 6   maxlim: 4   bits: 4/3
c ---[   3]---> Adder-cost: 6   maxlim: 4   bits: 4/3
c ---[   2]---> Adder-cost: 6   maxlim: 4   bits: 4/3
c ---[   1]---> Adder-cost: 6   maxlim: 9   bits: 5/4
c ---[   0]---> Adder-cost: 6   maxlim: 9   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13192    46987 |    4397       0        0     nan |  0.000 % |
c |       102 |   13165    46890 |    4836     100      512     5.1 | 13.328 % |
c |       252 |   13165    46890 |    5320     250     1591     6.4 | 13.328 % |
c |       478 |   13096    46639 |    5852     462     2805     6.1 | 13.441 % |
c |       817 |   13046    46459 |    6437     796     4934     6.2 | 13.517 % |
c ==============================================================================
c [1mFound solution: 2428[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1154   maxlim: 12752   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1226 |   20917    74551 |    6972    1183     9347     7.9 | 13.517 % |
c ==============================================================================
c [1mFound solution: 2162[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13018   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1284 |   20935    74652 |    6978    1241    10250     8.3 | 13.517 % |
c |      1385 |   20897    74522 |    7675    1330    11268     8.5 | 10.120 % |
c |      1535 |   20897    74522 |    8443    1480    16368    11.1 | 10.120 % |
c |      1761 |   20877    74453 |    9287    1703    20933    12.3 | 10.225 % |
c |      2098 |   20877    74453 |   10216    2040    49761    24.4 | 10.225 % |
c |      2605 |   20863    74406 |   11238    2544    69218    27.2 | 10.330 % |
c ==============================================================================
c [1mFound solution: 1947[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13233   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3053 |   20861    74423 |    6953    2991    82792    27.7 | 10.330 % |
c |      3153 |   20834    74322 |    7648    3084    83775    27.2 | 10.525 % |
c |      3303 |   20834    74322 |    8413    3234    92849    28.7 | 10.525 % |
c |      3528 |   20834    74322 |    9254    3459   100051    28.9 | 10.525 % |
c |      3865 |   20834    74322 |   10179    3796   106126    28.0 | 10.525 % |
c |      4372 |   20834    74322 |   11197    4303   141217    32.8 | 10.525 % |
c |      5131 |   20834    74322 |   12317    5062   175900    34.7 | 10.525 % |
c |      6270 |   20834    74322 |   13549    6201   226014    36.4 | 10.525 % |
c |      7978 |   20834    74322 |   14904    7909   318227    40.2 | 10.525 % |
c |     10541 |   20815    74257 |   16394   10470   452111    43.2 | 10.577 % |
c |     14385 |   20806    74226 |   18034   14308   674649    47.2 | 10.603 % |
c |     20151 |   20797    74195 |   19837   10130   594184    58.7 | 10.629 % |
c ==============================================================================
c [1mFound solution: 1941[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13239   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20652 |   20798    74205 |    6932   10631   618925    58.2 | 10.629 % |
c |     20755 |   20798    74205 |    7625    5419   298843    55.1 | 10.653 % |
c |     20905 |   20798    74205 |    8387    5569   302559    54.3 | 10.653 % |
c |     21135 |   20733    73974 |    9226    5792   305866    52.8 | 10.757 % |
c |     21472 |   20733    73974 |   10149    6129   323193    52.7 | 10.757 % |
c ==============================================================================
c [1mFound solution: 1881[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13299   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21663 |   20729    73980 |    6909    6314   326921    51.8 | 10.757 % |
c |     21764 |   20729    73980 |    7599    6415   328460    51.2 | 10.874 % |
c |     21914 |   20729    73980 |    8359    6565   331126    50.4 | 10.874 % |
c |     22140 |   20729    73980 |    9195    6791   335685    49.4 | 10.874 % |
c |     22478 |   20729    73980 |   10115    7129   344075    48.3 | 10.874 % |
c |     22984 |   20729    73980 |   11127    7635   371537    48.7 | 10.874 % |
c |     23746 |   20729    73980 |   12239    8397   400269    47.7 | 10.874 % |
c |     24886 |   20729    73980 |   13463    9537   458097    48.0 | 10.874 % |
c |     26596 |   20729    73980 |   14810   11247   536502    47.7 | 10.874 % |
c |     29158 |   20729    73980 |   16291   13809   672019    48.7 | 10.874 % |
c |     33003 |   20729    73980 |   17920    8861   315812    35.6 | 10.874 % |
c |     38770 |   20729    73980 |   19712   14628   696358    47.6 | 10.874 % |
c |     47422 |   20729    73980 |   21683   12478   962229    77.1 | 10.874 % |
c |     60401 |   20720    73949 |   23851   13731  1249003    91.0 | 10.900 % |
c ==============================================================================
c [1mFound solution: 1845[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13335   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79201 |   20710    73927 |    6903   19943  1158596    58.1 | 10.900 % |
c |     79301 |   20701    73896 |    7593    5081   208581    41.1 | 11.071 % |
c |     79455 |   20701    73896 |    8352    5235   211500    40.4 | 11.071 % |
c |     79683 |   20701    73896 |    9187    5463   215382    39.4 | 11.071 % |
c |     80020 |   20608    73570 |   10106    5782   226786    39.2 | 11.383 % |
c |     80526 |   20608    73570 |   11117    6288   256199    40.7 | 11.383 % |
c |     81285 |   20608    73570 |   12229    7047   284205    40.3 | 11.383 % |
c |     82424 |   20608    73570 |   13451    8186   347258    42.4 | 11.383 % |
c |     84133 |   20608    73570 |   14797    9895   437901    44.3 | 11.383 % |
c |     86695 |   20608    73570 |   16276   12457   677783    54.4 | 11.383 % |
c ==============================================================================
c [1mFound solution: 1792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13388   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89854 |   20616    73627 |    6872   15616   849559    54.4 | 11.383 % |
c |     89954 |   20616    73627 |    7559    4004   123632    30.9 | 11.475 % |
c |     90104 |   20616    73627 |    8315    4154   126972    30.6 | 11.475 % |
c |     90330 |   20616    73627 |    9146    4380   143530    32.8 | 11.475 % |
c |     90667 |   20616    73627 |   10061    4717   156029    33.1 | 11.475 % |
c |     91174 |   20616    73627 |   11067    5224   197057    37.7 | 11.475 % |
c |     91933 |   20616    73627 |   12174    5983   231832    38.7 | 11.475 % |
c |     93072 |   20616    73627 |   13391    7122   298894    42.0 | 11.475 % |
c |     94781 |   20601    73576 |   14730    8829   376707    42.7 | 11.527 % |
c |     97344 |   20580    73507 |   16203   11389   507705    44.6 | 11.736 % |
c |    101188 |   20580    73507 |   17824   15233   713304    46.8 | 11.736 % |
c |    106958 |   20573    73484 |   19606   11111   540489    48.6 | 11.762 % |
c |    115607 |   20573    73484 |   21567   19760  1194727    60.5 | 11.762 % |
c ==============================================================================
c [1mFound solution: 1781[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13399   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    123379 |   20577    73506 |    6859   16112  1044981    64.9 | 11.762 % |
c |    123480 |   20577    73506 |    7544    4129   179466    43.5 | 11.801 % |
c |    123630 |   20577    73506 |    8299    4279   183631    42.9 | 11.801 % |
c ==============================================================================
c [1mFound solution: 1776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13404   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    123739 |   20574    73512 |    6858    4385   185485    42.3 | 11.801 % |
c |    123839 |   20574    73512 |    7543    4485   186639    41.6 | 11.870 % |
c |    123989 |   20574    73512 |    8298    4635   189401    40.9 | 11.870 % |
c |    124215 |   20574    73512 |    9127    4861   201143    41.4 | 11.870 % |
c |    124552 |   20574    73512 |   10040    5198   208179    40.0 | 11.870 % |
c |    125059 |   20574    73512 |   11044    5705   224862    39.4 | 11.870 % |
c |    125818 |   20574    73512 |   12149    6464   252405    39.0 | 11.870 % |
c |    126958 |   20574    73512 |   13364    7604   319283    42.0 | 11.870 % |
c |    128666 |   20574    73512 |   14700    9312   379315    40.7 | 11.870 % |
c |    131228 |   20574    73512 |   16170   11874   507598    42.7 | 11.870 % |
c |    135072 |   20574    73512 |   17787   15718   699107    44.5 | 11.870 % |
c |    140838 |   20574    73512 |   19566   12194   511648    42.0 | 11.870 % |
c |    149488 |   20574    73512 |   21523   20844  1145270    54.9 | 11.870 % |
c |    162464 |   20574    73512 |   23675   11598   357808    30.9 | 11.870 % |
c |    181925 |   20574    73512 |   26043   18603   870687    46.8 | 11.870 % |
c |    211118 |   20560    73469 |   28647   20308   950919    46.8 | 12.026 % |
c ==============================================================================
c [1mFound solution: 1755[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13425   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    218305 |   20558    73479 |    6852   27494  1360587    49.5 | 12.026 % |
c |    218405 |   20558    73479 |    7537    6974   282225    40.5 | 12.114 % |
c |    218555 |   20558    73479 |    8290    7124   291456    40.9 | 12.114 % |
c |    218780 |   20558    73479 |    9120    7349   297264    40.4 | 12.114 % |
c |    219118 |   20558    73479 |   10032    7687   312851    40.7 | 12.114 % |
c |    219624 |   20543    73428 |   11035    8192   333718    40.7 | 12.166 % |
c |    220385 |   20543    73428 |   12138    8953   364519    40.7 | 12.166 % |
c |    221524 |   20543    73428 |   13352   10092   445827    44.2 | 12.166 % |
c |    223235 |   20543    73428 |   14687   11803   506621    42.9 | 12.166 % |
c ==============================================================================
c [1mFound solution: 1753[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13427   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    224071 |   20545    73441 |    6848   12639   570718    45.2 | 12.166 % |
c |    224174 |   20545    73441 |    7532    6423   229446    35.7 | 12.186 % |
c |    224325 |   20545    73441 |    8286    6574   231335    35.2 | 12.186 % |
c |    224550 |   20545    73441 |    9114    6799   241235    35.5 | 12.186 % |
c |    224887 |   20545    73441 |   10026    7136   257151    36.0 | 12.186 % |
c |    225393 |   20545    73441 |   11028    7642   277215    36.3 | 12.186 % |
c |    226153 |   20545    73441 |   12131    8402   312015    37.1 | 12.186 % |
c |    227292 |   20534    73402 |   13344    9534   369422    38.7 | 12.237 % |
c |    229000 |   20534    73402 |   14679   11242   449302    40.0 | 12.237 % |
c |    231563 |   20513    73333 |   16147   13801   552988    40.1 | 12.445 % |
c |    235411 |   20513    73333 |   17761    8871   358458    40.4 | 12.445 % |
c |    241177 |   20513    73333 |   19538   14637   660248    45.1 | 12.445 % |
c |    249826 |   20513    73333 |   21491   12851   614043    47.8 | 12.445 % |
c ==============================================================================
c [1mFound solution: 1749[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13431   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    253344 |   20515    73345 |    6838   16369   868856    53.1 | 12.445 % |
c |    253444 |   20515    73345 |    7521    4193   183263    43.7 | 12.464 % |
c |    253596 |   20515    73345 |    8273    4345   185094    42.6 | 12.464 % |
c |    253821 |   20515    73345 |    9101    4570   194627    42.6 | 12.464 % |
c |    254158 |   20515    73345 |   10011    4907   203451    41.5 | 12.464 % |
c |    254665 |   20501    73300 |   11012    5410   234658    43.4 | 12.594 % |
c |    255424 |   20392    72907 |   12113    6163   262281    42.6 | 12.724 % |
c |    256569 |   20392    72907 |   13325    7308   322651    44.2 | 12.724 % |
c |    258277 |   20392    72907 |   14657    9016   417101    46.3 | 12.724 % |
c |    260839 |   20392    72907 |   16123   11578   564920    48.8 | 12.724 % |
c |    264683 |   20392    72907 |   17736   15422   817769    53.0 | 12.724 % |
c |    270449 |   20392    72907 |   19509   11603   556279    47.9 | 12.724 % |
c |    279098 |   20392    72907 |   21460   20252  1002558    49.5 | 12.724 % |
c |    292075 |   20385    72884 |   23606   21612  1253343    58.0 | 12.749 % |
c |    311536 |   20385    72884 |   25967   15413  1163512    75.5 | 12.749 % |
c |    340728 |   20378    72860 |   28564   17676   914637    51.7 | 12.827 % |
c ==============================================================================
c [1mFound solution: 1747[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13433   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    348975 |   20380    72874 |    6793   25923  1421789    54.8 | 12.827 % |
c |    349075 |   20380    72874 |    7472    6581   280029    42.6 | 12.846 % |
c |    349226 |   20380    72874 |    8219    6732   282796    42.0 | 12.846 % |
c |    349451 |   20380    72874 |    9041    6957   297001    42.7 | 12.846 % |
c |    349788 |   20380    72874 |    9945    7294   308706    42.3 | 12.846 % |
c |    350296 |   20380    72874 |   10940    7802   344058    44.1 | 12.846 % |
c |    351056 |   20380    72874 |   12034    8562   385330    45.0 | 12.846 % |
c |    352195 |   20380    72874 |   13237    9701   437147    45.1 | 12.846 % |
c |    353903 |   20380    72874 |   14561   11409   601799    52.7 | 12.846 % |
c |    356467 |   20380    72874 |   16017   13973   802605    57.4 | 12.846 % |
c |    360312 |   20358    72800 |   17619    9252   444555    48.0 | 12.924 % |
c |    366078 |   20357    72796 |   19381   15015   634731    42.3 | 12.950 % |
c |    374728 |   20335    72720 |   21319   13215   555286    42.0 | 13.002 % |
c |    387702 |   20335    72720 |   23451   15014   734359    48.9 | 13.002 % |
c |    407163 |   20335    72720 |   25796   22068  1444824    65.5 | 13.002 % |
c |    436355 |   20328    72697 |   28376   23909  1530806    64.0 | 13.028 % |
c |    480144 |   20321    72675 |   31213   22853  1559072    68.2 | 13.131 % |
c |    545828 |   20307    72630 |   34335   20039  1082279    54.0 | 13.261 % |
c ==============================================================================
c [1mFound solution: 1731[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13449   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    567573 |   20312    72662 |    6770   20925  1488167    71.1 | 13.261 % |
c |    567673 |   20312    72662 |    7447    5332   308185    57.8 | 13.321 % |
c |    567823 |   20312    72662 |    8191    5482   316939    57.8 | 13.321 % |
c |    568048 |   20312    72662 |    9010    5707   327787    57.4 | 13.321 % |
c |    568385 |   20312    72662 |    9911    6044   342106    56.6 | 13.321 % |
c |    568891 |   20312    72662 |   10903    6550   355578    54.3 | 13.321 % |
c |    569652 |   20312    72662 |   11993    7311   376668    51.5 | 13.321 % |
c |    570791 |   20312    72662 |   13192    8450   446785    52.9 | 13.321 % |
c |    572500 |   20312    72662 |   14512   10159   562957    55.4 | 13.321 % |
c |    575062 |   20291    72594 |   15963   12716   672193    52.9 | 13.476 % |
c |    578906 |   20291    72594 |   17559   16560   920761    55.6 | 13.476 % |
c |    584672 |   20291    72594 |   19315   13162   599136    45.5 | 13.476 % |
c |    593322 |   20284    72571 |   21247   11852   532807    45.0 | 13.502 % |
c |    606297 |   20284    72571 |   23371   13541   691950    51.1 | 13.502 % |
c |    625758 |   20284    72571 |   25709   20744  1225003    59.1 | 13.502 % |
c |    654954 |   20263    72503 |   28279   22999  1116401    48.5 | 13.658 % |
c ==============================================================================
c [1mFound solution: 1591[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13589   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    685274 |   20269    72544 |    6756   23990  1270883    53.0 | 13.658 % |
c |    685374 |   20269    72544 |    7431    6098   174802    28.7 | 13.740 % |
c |    685524 |   20269    72544 |    8174    6248   186081    29.8 | 13.740 % |
c |    685749 |   20269    72544 |    8992    6473   192806    29.8 | 13.740 % |
c |    686091 |   20269    72544 |    9891    6815   207068    30.4 | 13.740 % |
c |    686598 |   20269    72544 |   10880    7322   236326    32.3 | 13.740 % |
c |    687357 |   20269    72544 |   11968    8081   280887    34.8 | 13.740 % |
c |    688498 |   20269    72544 |   13165    9222   329454    35.7 | 13.740 % |
c |    690208 |   20262    72521 |   14482   10931   398941    36.5 | 13.766 % |
c |    692770 |   20262    72521 |   15930   13493   520308    38.6 | 13.766 % |
c |    696615 |   20262    72521 |   17523    8889   260805    29.3 | 13.766 % |
c |    702381 |   20262    72521 |   19275   14655   661771    45.2 | 13.766 % |
c |    711030 |   20262    72521 |   21203   13238   639875    48.3 | 13.766 % |
c |    724005 |   20262    72521 |   23323   14574   978289    67.1 | 13.766 % |
c |    743468 |   20262    72521 |   25655   21757  1341594    61.7 | 13.766 % |
c |    772660 |   20262    72521 |   28221   24078  1777531    73.8 | 13.766 % |
c |    816449 |   20262    72521 |   31043   24006  1304022    54.3 | 13.766 % |
c |    882134 |   20262    72521 |   34148   25166  1692918    67.3 | 13.766 % |
#### 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.85 0.95 0.91 2/54 15137
Raw data (stat): 15137 (runsolver) R 15136 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549971190 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.0006 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 1632 0 0 0 993 5 0 0 25 0 1 0 549971190 8364032 1610 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1610 603 41 0 2001 0
vsize: 8168
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 1988 0 0 0 1992 7 0 0 25 0 1 0 549971190 9850880 1966 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2405 1966 603 41 0 2364 0
vsize: 9620
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 1988 0 0 0 2991 7 0 0 25 0 1 0 549971190 9850880 1966 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2405 1966 603 41 0 2364 0
vsize: 9620
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 2301 0 0 0 3989 8 0 0 25 0 1 0 549971190 11055104 2279 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2699 2279 603 41 0 2658 0
vsize: 10796
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 2462 0 0 0 4989 9 0 0 25 0 1 0 549971190 11730944 2440 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2864 2440 603 41 0 2823 0
vsize: 11456
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3100 0 0 0 5988 10 0 0 25 0 1 0 549971190 14413824 3078 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3519 3078 603 41 0 3478 0
vsize: 14076
[startup+70.0028 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3100 0 0 0 6988 10 0 0 25 0 1 0 549971190 14413824 3078 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3519 3078 603 41 0 3478 0
vsize: 14076
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3101 0 0 0 7988 10 0 0 25 0 1 0 549971190 14401536 3079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3079 603 41 0 3475 0
vsize: 14064
[startup+90.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 8988 10 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 9988 10 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 10988 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 11989 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15137
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 12989 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 13988 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 14988 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 15989 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 16989 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 17989 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 18989 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3102 0 0 0 19989 11 0 0 25 0 1 0 549971190 14401536 3080 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3278 0 0 0 20989 12 0 0 25 0 1 0 549971190 15069184 3256 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3679 3256 603 41 0 3638 0
vsize: 14716
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3320 0 0 0 21989 12 0 0 25 0 1 0 549971190 15204352 3298 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3298 603 41 0 3671 0
vsize: 14848
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3332 0 0 0 22990 12 0 0 25 0 1 0 549971190 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3310 603 41 0 3704 0
vsize: 14980
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3332 0 0 0 23990 12 0 0 25 0 1 0 549971190 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3310 603 41 0 3704 0
vsize: 14980
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3333 0 0 0 24990 12 0 0 25 0 1 0 549971190 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3311 603 41 0 3704 0
vsize: 14980
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3333 0 0 0 25990 12 0 0 25 0 1 0 549971190 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3311 603 41 0 3704 0
vsize: 14980
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3333 0 0 0 26990 12 0 0 25 0 1 0 549971190 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3311 603 41 0 3704 0
vsize: 14980
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 27990 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 28990 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 29990 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 30991 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 31991 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 32991 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223552 1075349719 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 33991 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223760 134558170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 34991 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 35992 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 36992 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 37992 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 38992 12 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 39991 13 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 40991 13 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 41991 13 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 42991 13 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 43992 13 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3334 0 0 0 44992 13 0 0 25 0 1 0 549971190 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3363 0 0 0 45992 13 0 0 25 0 1 0 549971190 15474688 3341 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3778 3341 603 41 0 3737 0
vsize: 15112
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3450 0 0 0 46992 13 0 0 25 0 1 0 549971190 15736832 3428 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3842 3428 603 41 0 3801 0
vsize: 15368
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3473 0 0 0 47992 13 0 0 25 0 1 0 549971190 15872000 3451 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3875 3451 603 41 0 3834 0
vsize: 15500
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3549 0 0 0 48992 13 0 0 25 0 1 0 549971190 16138240 3527 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3940 3527 603 41 0 3899 0
vsize: 15760
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3549 0 0 0 49992 13 0 0 25 0 1 0 549971190 16138240 3527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3940 3527 603 41 0 3899 0
vsize: 15760
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3550 0 0 0 50992 13 0 0 25 0 1 0 549971190 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3940 3528 603 41 0 3899 0
vsize: 15760
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3550 0 0 0 51992 13 0 0 25 0 1 0 549971190 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3940 3528 603 41 0 3899 0
vsize: 15760
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3551 0 0 0 52993 13 0 0 25 0 1 0 549971190 16138240 3529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3940 3529 603 41 0 3899 0
vsize: 15760
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3551 0 0 0 53993 13 0 0 25 0 1 0 549971190 16138240 3529 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3940 3529 603 41 0 3899 0
vsize: 15760
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3856 0 0 0 54992 14 0 0 25 0 1 0 549971190 17469440 3834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3834 603 41 0 4224 0
vsize: 17060
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3860 0 0 0 55992 14 0 0 25 0 1 0 549971190 17469440 3838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3838 603 41 0 4224 0
vsize: 17060
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3860 0 0 0 56993 14 0 0 25 0 1 0 549971190 17469440 3838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3838 603 41 0 4224 0
vsize: 17060
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3862 0 0 0 57993 14 0 0 25 0 1 0 549971190 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3862 0 0 0 58992 14 0 0 25 0 1 0 549971190 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3862 0 0 0 59991 14 0 0 25 0 1 0 549971190 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3862 0 0 0 60990 15 0 0 25 0 1 0 549971190 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3862 0 0 0 61990 15 0 0 25 0 1 0 549971190 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3867 0 0 0 62991 15 0 0 25 0 1 0 549971190 17469440 3845 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3845 603 41 0 4224 0
vsize: 17060
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3867 0 0 0 63991 15 0 0 25 0 1 0 549971190 17469440 3845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4265 3845 603 41 0 4224 0
vsize: 17060
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3900 0 0 0 64991 15 0 0 25 0 1 0 549971190 17731584 3878 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4329 3878 603 41 0 4288 0
vsize: 17316
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3900 0 0 0 65991 15 0 0 25 0 1 0 549971190 17731584 3878 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4329 3878 603 41 0 4288 0
vsize: 17316
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3900 0 0 0 66991 15 0 0 25 0 1 0 549971190 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4329 3878 603 41 0 4288 0
vsize: 17316
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3900 0 0 0 67991 15 0 0 25 0 1 0 549971190 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4329 3878 603 41 0 4288 0
vsize: 17316
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3900 0 0 0 68991 15 0 0 25 0 1 0 549971190 17731584 3878 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4329 3878 603 41 0 4288 0
vsize: 17316
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3901 0 0 0 69991 15 0 0 25 0 1 0 549971190 17731584 3879 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4329 3879 603 41 0 4288 0
vsize: 17316
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 70991 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 71991 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 72991 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 73991 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 74991 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223728 134559553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 75991 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 76992 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 77992 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221222524 134566364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 78992 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 79992 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 80992 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 81992 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 82992 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 83993 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 84993 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 85993 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 86993 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 87993 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 88993 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 89994 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 90994 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 91994 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 92994 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 93994 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223560 1075352682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 94994 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 95995 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 3979 0 0 0 96995 15 0 0 25 0 1 0 549971190 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4056 0 0 0 97995 15 0 0 25 0 1 0 549971190 18399232 4034 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4034 603 41 0 4451 0
vsize: 17968
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4060 0 0 0 98995 16 0 0 25 0 1 0 549971190 18399232 4038 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4038 603 41 0 4451 0
vsize: 17968
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 99995 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 100995 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 101995 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 102996 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 103996 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 104996 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 105996 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4068 0 0 0 106996 16 0 0 25 0 1 0 549971190 18399232 4046 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4075 0 0 0 107996 16 0 0 25 0 1 0 549971190 18399232 4053 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4492 4053 603 41 0 4451 0
vsize: 17968
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4082 0 0 0 108997 16 0 0 25 0 1 0 549971190 18546688 4060 4294967295 134512640 134672761 3221224544 3221223728 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4082 0 0 0 109997 16 0 0 25 0 1 0 549971190 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4082 0 0 0 110997 16 0 0 25 0 1 0 549971190 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4082 0 0 0 111997 16 0 0 25 0 1 0 549971190 18546688 4060 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4107 0 0 0 112997 16 0 0 25 0 1 0 549971190 18546688 4085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 4085 603 41 0 4487 0
vsize: 18112
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4129 0 0 0 113998 16 0 0 25 0 1 0 549971190 18677760 4107 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4560 4107 603 41 0 4519 0
vsize: 18240
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4130 0 0 0 114998 16 0 0 25 0 1 0 549971190 18677760 4108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4560 4108 603 41 0 4519 0
vsize: 18240
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4156 0 0 0 115998 16 0 0 25 0 1 0 549971190 18808832 4134 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4592 4134 603 41 0 4551 0
vsize: 18368
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4252 0 0 0 116997 16 0 0 25 0 1 0 549971190 19206144 4230 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4689 4230 603 41 0 4648 0
vsize: 18756
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4259 0 0 0 117997 16 0 0 25 0 1 0 549971190 19206144 4237 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4689 4237 603 41 0 4648 0
vsize: 18756
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4270 0 0 0 118998 16 0 0 25 0 1 0 549971190 19361792 4248 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4727 4248 603 41 0 4686 0
vsize: 18908
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15139
Raw data (stat): 15137 (minisat+) R 15136 26298 26297 0 -1 0 4271 0 0 0 119998 16 0 0 25 0 1 0 549971190 19361792 4249 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4727 4249 603 41 0 4686 0
vsize: 18908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 15139
Raw data (stat): 15137 (minisat+) Z 15136 26298 26297 0 -1 12 4274 0 0 0 119998 17 0 0 25 0 1 0 549971190 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: 10
Real time (s): 1200.03
CPU time (s): 1200.16
CPU user time (s): 1199.98
CPU system time (s): 0.177972
CPU usage (%): 100.011
Max. virtual memory (Kb): 18908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####