PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.02184
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 15623

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 05:17:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17118 boxname=wulflinc8 idbench=1317 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ffa3a55eb53181880328dd1b84f91e66  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-p0201.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-p0201.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-p0201.opb
IDLAUNCH: 17118
/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:        579928 kB
Buffers:         34524 kB
Cached:         397752 kB
SwapCached:          0 kB
Active:         171316 kB
Inactive:       263808 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        579676 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14048 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:37:19 (client local time) WITH STATUS 10 IN 1209.96 SECONDS
stats: 17118 7 1209.96 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.88 0.99 0.94 2/54 22955
Raw data (stat): 22955 (runsolver) R 22954 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 470706509 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.90 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 1625 0 0 0 993 4 0 0 25 0 1 0 470706509 8228864 1603 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2009 1603 603 41 0 1968 0
vsize: 8036
[startup+20.0009 s]
Raw data (loadavg): 0.91 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 1988 0 0 0 1992 6 0 0 25 0 1 0 470706509 9850880 1966 4294967295 134512640 134672761 3221224544 3221223728 134559345 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.0016 s]
Raw data (loadavg): 0.93 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 1988 0 0 0 2992 6 0 0 25 0 1 0 470706509 9850880 1966 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0029 s]
Raw data (loadavg): 0.94 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 2290 0 0 0 3990 8 0 0 25 0 1 0 470706509 11055104 2268 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2699 2268 603 41 0 2658 0
vsize: 10796
[startup+50.0032 s]
Raw data (loadavg): 0.95 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 2455 0 0 0 4989 8 0 0 25 0 1 0 470706509 11730944 2433 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2433 603 41 0 2823 0
vsize: 11456
[startup+60.0029 s]
Raw data (loadavg): 0.95 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3100 0 0 0 5987 10 0 0 25 0 1 0 470706509 14413824 3078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3519 3078 603 41 0 3478 0
vsize: 14076
[startup+70.0042 s]
Raw data (loadavg): 0.96 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3100 0 0 0 6987 11 0 0 25 0 1 0 470706509 14413824 3078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3519 3078 603 41 0 3478 0
vsize: 14076
[startup+80.0045 s]
Raw data (loadavg): 0.97 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3101 0 0 0 7986 11 0 0 25 0 1 0 470706509 14401536 3079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3079 603 41 0 3475 0
vsize: 14064
[startup+90.0053 s]
Raw data (loadavg): 0.97 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 8986 11 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+100.005 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 9986 12 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223648 134555133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+110.006 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 10985 12 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+120.007 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 11985 13 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+130.007 s]
Raw data (loadavg): 0.98 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 12984 13 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+140.007 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 13984 14 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223600 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+150.008 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 14984 14 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+160.008 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 15983 14 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+170.008 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 16983 15 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+180.008 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 17982 15 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+190.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 18982 15 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+200.01 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3102 0 0 0 19982 15 0 0 25 0 1 0 470706509 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3516 3080 603 41 0 3475 0
vsize: 14064
[startup+210.009 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3315 0 0 0 20981 16 0 0 25 0 1 0 470706509 15204352 3293 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3293 603 41 0 3671 0
vsize: 14848
[startup+220.011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3320 0 0 0 21981 16 0 0 25 0 1 0 470706509 15204352 3298 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3712 3298 603 41 0 3671 0
vsize: 14848
[startup+230.01 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3332 0 0 0 22981 16 0 0 25 0 1 0 470706509 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3310 603 41 0 3704 0
vsize: 14980
[startup+240.011 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3332 0 0 0 23980 17 0 0 25 0 1 0 470706509 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3310 603 41 0 3704 0
vsize: 14980
[startup+250.012 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3333 0 0 0 24980 17 0 0 25 0 1 0 470706509 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3311 603 41 0 3704 0
vsize: 14980
[startup+260.012 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3333 0 0 0 25980 17 0 0 25 0 1 0 470706509 15339520 3311 4294967295 134512640 134672761 3221224544 3221223648 134554877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3311 603 41 0 3704 0
vsize: 14980
[startup+270.012 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3333 0 0 0 26979 18 0 0 25 0 1 0 470706509 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3311 603 41 0 3704 0
vsize: 14980
[startup+280.012 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 27979 18 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+290.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 28978 18 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223680 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+300.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 29978 19 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+310.013 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 30978 19 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+320.015 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 31978 19 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223792 134562680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+330.015 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 32977 19 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+340.015 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 33977 20 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+350.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 34977 20 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+360.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 35976 21 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223744 134557814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+370.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 36976 21 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+380.016 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 37976 21 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+390.017 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 38974 22 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.017 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 39974 23 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.017 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 40973 23 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+420.018 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 41973 23 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+430.018 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 42972 24 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+440.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 43972 24 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+450.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3334 0 0 0 44972 25 0 0 25 0 1 0 470706509 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3745 3312 603 41 0 3704 0
vsize: 14980
[startup+460.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3450 0 0 0 45971 25 0 0 25 0 1 0 470706509 15736832 3428 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3842 3428 603 41 0 3801 0
vsize: 15368
[startup+470.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3450 0 0 0 46971 25 0 0 25 0 1 0 470706509 15736832 3428 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3842 3428 603 41 0 3801 0
vsize: 15368
[startup+480.019 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3549 0 0 0 47970 26 0 0 25 0 1 0 470706509 16138240 3527 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3527 603 41 0 3899 0
vsize: 15760
[startup+490.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3549 0 0 0 48970 26 0 0 25 0 1 0 470706509 16138240 3527 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3527 603 41 0 3899 0
vsize: 15760
[startup+500.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3550 0 0 0 49969 27 0 0 25 0 1 0 470706509 16138240 3528 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3528 603 41 0 3899 0
vsize: 15760
[startup+510.02 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3550 0 0 0 50969 27 0 0 25 0 1 0 470706509 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3528 603 41 0 3899 0
vsize: 15760
[startup+520.021 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3550 0 0 0 51968 28 0 0 25 0 1 0 470706509 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3528 603 41 0 3899 0
vsize: 15760
[startup+530.021 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3551 0 0 0 52968 28 0 0 25 0 1 0 470706509 16138240 3529 4294967295 134512640 134672761 3221224544 3221223744 134557861 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3529 603 41 0 3899 0
vsize: 15760
[startup+540.022 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3551 0 0 0 53968 28 0 0 25 0 1 0 470706509 16138240 3529 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3940 3529 603 41 0 3899 0
vsize: 15760
[startup+550.023 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3856 0 0 0 54966 30 0 0 25 0 1 0 470706509 17469440 3834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3834 603 41 0 4224 0
vsize: 17060
[startup+560.023 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3860 0 0 0 55966 30 0 0 25 0 1 0 470706509 17469440 3838 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3838 603 41 0 4224 0
vsize: 17060
[startup+570.023 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3862 0 0 0 56966 30 0 0 25 0 1 0 470706509 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+580.024 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3862 0 0 0 57965 30 0 0 25 0 1 0 470706509 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+590.025 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3862 0 0 0 58966 30 0 0 25 0 1 0 470706509 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.025 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3862 0 0 0 59965 31 0 0 25 0 1 0 470706509 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.025 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3862 0 0 0 60965 31 0 0 25 0 1 0 470706509 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+620.026 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3862 0 0 0 61965 31 0 0 25 0 1 0 470706509 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3840 603 41 0 4224 0
vsize: 17060
[startup+630.026 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3867 0 0 0 62965 31 0 0 25 0 1 0 470706509 17469440 3845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4265 3845 603 41 0 4224 0
vsize: 17060
[startup+640.026 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3900 0 0 0 63964 32 0 0 25 0 1 0 470706509 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+650.027 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3900 0 0 0 64964 32 0 0 25 0 1 0 470706509 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+660.026 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3900 0 0 0 65963 32 0 0 25 0 1 0 470706509 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4329 3878 603 41 0 4288 0
vsize: 17316
[startup+670.027 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3900 0 0 0 66963 33 0 0 25 0 1 0 470706509 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+680.027 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3900 0 0 0 67963 33 0 0 25 0 1 0 470706509 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.028 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3900 0 0 0 68962 33 0 0 25 0 1 0 470706509 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4329 3878 603 41 0 4288 0
vsize: 17316
[startup+700.029 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 69962 34 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+710.029 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 70962 34 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+720.03 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 71961 34 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+730.03 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 72961 35 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+740.032 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 73961 35 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+750.032 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 74960 36 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+760.032 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 75959 36 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223612 1075346648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+770.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 76959 37 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+780.032 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 77958 37 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+790.033 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 78958 38 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+800.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 79958 38 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+810.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 80957 38 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+820.034 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 81957 38 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+830.035 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 82957 39 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+840.036 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 83956 39 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+850.036 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 84955 40 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+860.037 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 85955 40 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223612 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+870.037 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 86955 40 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+880.037 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 87955 40 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+890.038 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 88954 41 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+900.038 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 89954 41 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+910.039 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 90954 41 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+920.039 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 91954 42 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+930.04 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 92953 42 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+940.041 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 93953 42 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+950.041 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 94952 42 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+960.041 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 3979 0 0 0 95952 43 0 0 25 0 1 0 470706509 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4393 3957 603 41 0 4352 0
vsize: 17572
[startup+970.042 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4004 0 0 0 96952 43 0 0 25 0 1 0 470706509 18128896 3982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4426 3982 603 41 0 4385 0
vsize: 17704
[startup+980.043 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4060 0 0 0 97951 44 0 0 25 0 1 0 470706509 18399232 4038 4294967295 134512640 134672761 3221224544 3221223648 134560134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4038 603 41 0 4451 0
vsize: 17968
[startup+990.043 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4064 0 0 0 98950 45 0 0 25 0 1 0 470706509 18399232 4042 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4042 603 41 0 4451 0
vsize: 17968
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 99950 45 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 100950 45 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 101950 45 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 102949 45 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 103949 46 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 104949 46 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 105948 46 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4068 0 0 0 106948 46 0 0 25 0 1 0 470706509 18399232 4046 4294967295 134512640 134672761 3221224544 3221223264 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4046 603 41 0 4451 0
vsize: 17968
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4076 0 0 0 107948 47 0 0 25 0 1 0 470706509 18399232 4054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4492 4054 603 41 0 4451 0
vsize: 17968
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4082 0 0 0 108948 47 0 0 25 0 1 0 470706509 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4082 0 0 0 109947 47 0 0 25 0 1 0 470706509 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4082 0 0 0 110947 47 0 0 25 0 1 0 470706509 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4082 0 0 0 111947 47 0 0 25 0 1 0 470706509 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4060 603 41 0 4487 0
vsize: 18112
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4126 0 0 0 112947 48 0 0 25 0 1 0 470706509 18677760 4104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4560 4104 603 41 0 4519 0
vsize: 18240
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4130 0 0 0 113946 48 0 0 25 0 1 0 470706509 18677760 4108 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4560 4108 603 41 0 4519 0
vsize: 18240
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4145 0 0 0 114946 49 0 0 25 0 1 0 470706509 18677760 4123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4560 4123 603 41 0 4519 0
vsize: 18240
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4246 0 0 0 115945 49 0 0 25 0 1 0 470706509 19206144 4224 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4689 4224 603 41 0 4648 0
vsize: 18756
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4252 0 0 0 116945 49 0 0 25 0 1 0 470706509 19206144 4230 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4689 4230 603 41 0 4648 0
vsize: 18756
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4270 0 0 0 117945 50 0 0 25 0 1 0 470706509 19361792 4248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4727 4248 603 41 0 4686 0
vsize: 18908
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4271 0 0 0 118944 50 0 0 25 0 1 0 470706509 19361792 4249 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4727 4249 603 41 0 4686 0
vsize: 18908
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4283 0 0 0 119944 50 0 0 25 0 1 0 470706509 19361792 4261 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4727 4261 603 41 0 4686 0
vsize: 18908
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.99 0.94 2/54 22955
Raw data (stat): 22955 (minisat+) R 22954 26667 26666 0 -1 0 4285 0 0 0 120943 51 0 0 25 0 1 0 470706509 19361792 4263 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4727 4263 603 41 0 4686 0
vsize: 18908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.06 s]
Raw data (loadavg): 0.99 0.99 0.94 1/54 22955
Raw data (stat): 22955 (minisat+) Z 22954 26667 26666 0 -1 12 4288 0 0 0 120943 52 0 0 25 0 1 0 470706509 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): 1210.06
CPU time (s): 1209.96
CPU user time (s): 1209.44
CPU system time (s): 0.52092
CPU usage (%): 99.9915
Max. virtual memory (Kb): 18908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####