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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare1.opb
MD5SUMba87f5dfbaed559dc55bc00bf07dc880
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3712
Optimality of the best value was proved NO
Number of terms in the objective function 120
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 6291450
Number of bits of the sum of numbers in the objective function 23
Biggest number in a constraint 524288
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 6291450
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.68
Number of variables170
Total number of constraints56
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)50
Number of constraints which are nor clauses,nor cardinality constraints6
Minimum length of a constraint1
Maximum length of a constraint70

Trace number 13821 

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        389608 kB
Buffers:         35664 kB
Cached:         586332 kB
SwapCached:          0 kB
Active:         365868 kB
Inactive:       258904 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        389356 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14696 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:14:55 (client local time) WITH STATUS 10 IN 1200.7 SECONDS
stats: 18511 7 1200.7 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> BDD-cost:23437
c ---[   8]---> BDD-cost:28407
c ---[   6]---> BDD-cost:25972
c ---[   4]---> BDD-cost:24798
c ---[   2]---> BDD-cost:25031
c ---[   0]---> BDD-cost:24117
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  436749  1274733 |  145583       0        0     nan |  0.000 % |
c |       100 |  436749  1274733 |  160141     100     9403    94.0 |  0.012 % |
c ==============================================================================
c Found solution: 862848
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       102 |  440476  1283432 |  146825     102     9461    92.8 |  0.012 % |
c ==============================================================================
c Found solution: 860928
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       105 |  440500  1283513 |  146833     105     9619    91.6 |  0.012 % |
c ==============================================================================
c Found solution: 848640
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       106 |  440508  1283534 |  146836     106     9694    91.5 |  0.012 % |
c ==============================================================================
c Found solution: 839296
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       109 |  440517  1283557 |  146839     109     9892    90.8 |  0.012 % |
c ==============================================================================
c Found solution: 835328
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       112 |  440525  1283579 |  146841     112    10046    89.7 |  0.012 % |
c ==============================================================================
c Found solution: 811776
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       115 |  440531  1283593 |  146843     115    10228    88.9 |  0.012 % |
c ==============================================================================
c Found solution: 793344
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       138 |  440541  1283616 |  146847     138    11635    84.3 |  0.012 % |
c ==============================================================================
c Found solution: 788224
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       193 |  440551  1283638 |  146850     193    14480    75.0 |  0.012 % |
c ==============================================================================
c Found solution: 784256
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       198 |  440561  1283669 |  146853     198    14774    74.6 |  0.012 % |
c ==============================================================================
c Found solution: 760704
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       199 |  440572  1283698 |  146857     199    14819    74.5 |  0.012 % |
c ==============================================================================
c Found solution: 760064
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       222 |  440584  1283728 |  146861     222    15796    71.2 |  0.012 % |
c ==============================================================================
c Found solution: 755840
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       271 |  440596  1283756 |  146865     271    18033    66.5 |  0.012 % |
c ==============================================================================
c Found solution: 740864
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       330 |  440609  1283788 |  146869     330    20875    63.3 |  0.012 % |
c ==============================================================================
c Found solution: 740224
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       388 |  440620  1283814 |  146873     388    23291    60.0 |  0.012 % |
c ==============================================================================
c Found solution: 669184
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       392 |  440630  1283839 |  146876     392    23497    59.9 |  0.012 % |
c |       493 |  440630  1283839 |  161563     493    25965    52.7 |  0.022 % |
c |       645 |  440630  1283839 |  177719     645    38402    59.5 |  0.022 % |
c |       870 |  440630  1283839 |  195491     870    49510    56.9 |  0.022 % |
c |      1208 |  440630  1283839 |  215041    1208    64325    53.2 |  0.022 % |
c ==============================================================================
c Found solution: 619392
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1350 |  440647  1283882 |  146882    1350    70758    52.4 |  0.022 % |
c |      1450 |  440647  1283882 |  161570    1450    75423    52.0 |  0.022 % |
c |      1600 |  440647  1283882 |  177727    1600    82144    51.3 |  0.022 % |
c |      1826 |  440647  1283882 |  195499    1826    92134    50.5 |  0.022 % |
c |      2164 |  440647  1283882 |  215049    2164   108591    50.2 |  0.022 % |
c ==============================================================================
c Found solution: 616960
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2415 |  440661  1283918 |  146887    2415   120616    49.9 |  0.022 % |
c ==============================================================================
c Found solution: 612992
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2449 |  440671  1283942 |  146890    2449   122229    49.9 |  0.022 % |
c ==============================================================================
c Found solution: 600448
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2513 |  440686  1283977 |  146895    2513   125386    49.9 |  0.022 % |
c |      2613 |  440686  1283977 |  161584    2613   129646    49.6 |  0.024 % |
c ==============================================================================
c Found solution: 594048
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2615 |  440697  1284002 |  146899    2615   129753    49.6 |  0.024 % |
c ==============================================================================
c Found solution: 593792
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2659 |  440707  1284025 |  146902    2659   131977    49.6 |  0.024 % |
c |      2760 |  440707  1284025 |  161592    2760   136347    49.4 |  0.026 % |
c |      2911 |  440707  1284025 |  177751    2911   143046    49.1 |  0.026 % |
c ==============================================================================
c Found solution: 576896
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3074 |  440718  1284052 |  146906    3074   150380    48.9 |  0.026 % |
c |      3175 |  440718  1284052 |  161596    3175   153785    48.4 |  0.026 % |
c ==============================================================================
c Found solution: 576128
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3275 |  440725  1284069 |  146908    3275   158596    48.4 |  0.026 % |
c |      3377 |  440725  1284069 |  161598    3377   162887    48.2 |  0.027 % |
c |      3528 |  440725  1284069 |  177758    3528   168251    47.7 |  0.027 % |
c |      3754 |  440725  1284069 |  195534    3754   180561    48.1 |  0.027 % |
c ==============================================================================
c Found solution: 573568
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3791 |  440733  1284088 |  146911    3791   181744    47.9 |  0.027 % |
c ==============================================================================
c Found solution: 573312
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3880 |  440741  1284108 |  146913    3880   185737    47.9 |  0.027 % |
c |      3980 |  440741  1284108 |  161604    3980   190136    47.8 |  0.028 % |
c ==============================================================================
c Found solution: 572288
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4008 |  440749  1284127 |  146916    4008   191213    47.7 |  0.028 % |
c |      4109 |  440749  1284127 |  161607    4109   195601    47.6 |  0.029 % |
c ==============================================================================
c Found solution: 566400
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4172 |  440763  1284159 |  146921    4172   198808    47.7 |  0.029 % |
c ==============================================================================
c Found solution: 566144
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4218 |  440773  1284182 |  146924    4218   200938    47.6 |  0.029 % |
c ==============================================================================
c Found solution: 542848
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4228 |  440782  1284202 |  146927    4228   201373    47.6 |  0.029 % |
c |      4328 |  440782  1284202 |  161619    4328   205475    47.5 |  0.031 % |
c |      4478 |  440782  1284202 |  177781    4478   212196    47.4 |  0.031 % |
c ==============================================================================
c Found solution: 534400
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4640 |  440791  1284222 |  146930    4640   219034    47.2 |  0.031 % |
c |      4741 |  440791  1284222 |  161623    4741   223846    47.2 |  0.031 % |
c |      4891 |  440791  1284222 |  177785    4891   231251    47.3 |  0.031 % |
c |      5116 |  440791  1284222 |  195563    5116   240547    47.0 |  0.031 % |
c |      5453 |  440791  1284222 |  215120    5453   255602    46.9 |  0.031 % |
c |      5959 |  440791  1284222 |  236632    5959   279577    46.9 |  0.031 % |
c |      6720 |  440791  1284222 |  260295    6720   314985    46.9 |  0.031 % |
c |      7859 |  440791  1284222 |  286325    7859   369091    47.0 |  0.031 % |
c ==============================================================================
c Found solution: 531584
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8101 |  440799  1284241 |  146933    8101   380625    47.0 |  0.031 % |
c |      8203 |  440799  1284241 |  161626    8203   385228    47.0 |  0.032 % |
c ==============================================================================
c Found solution: 509312
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8332 |  440811  1284271 |  146937    8332   391378    47.0 |  0.032 % |
c |      8432 |  440811  1284271 |  161630    8432   395334    46.9 |  0.033 % |
c ==============================================================================
c Found solution: 418560
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8441 |  440817  1284284 |  146939    8441   395745    46.9 |  0.033 % |
c |      8541 |  440817  1284284 |  161632    8541   399910    46.8 |  0.033 % |
c ==============================================================================
c Found solution: 411264
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8583 |  440828  1284309 |  146942    8583   401708    46.8 |  0.033 % |
c |      8683 |  440828  1284309 |  161636    8683   405325    46.7 |  0.034 % |
c |      8833 |  440828  1284309 |  177799    8833   412197    46.7 |  0.034 % |
c ==============================================================================
c Found solution: 408064
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8934 |  440835  1284326 |  146945    8934   416333    46.6 |  0.034 % |
c ==============================================================================
c Found solution: 406016
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8987 |  440844  1284347 |  146948    8987   418999    46.6 |  0.034 % |
c ==============================================================================
c Found solution: 404608
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9069 |  440854  1284370 |  146951    9069   422941    46.6 |  0.034 % |
c |      9169 |  440854  1284370 |  161646    9169   427271    46.6 |  0.036 % |
c ==============================================================================
c Found solution: 401664
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9240 |  440864  1284392 |  146954    9240   430660    46.6 |  0.036 % |
c |      9341 |  440864  1284392 |  161649    9341   435483    46.6 |  0.037 % |
c ==============================================================================
c Found solution: 392064
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9444 |  440872  1284413 |  146957    9444   440094    46.6 |  0.037 % |
c ==============================================================================
c Found solution: 386176
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9491 |  440877  1284428 |  146959    9491   442086    46.6 |  0.037 % |
c |      9593 |  440877  1284428 |  161654    9593   446226    46.5 |  0.038 % |
c |      9743 |  440877  1284428 |  177820    9743   452544    46.4 |  0.038 % |
c ==============================================================================
c Found solution: 381952
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9806 |  440889  1284458 |  146963    9806   455422    46.4 |  0.038 % |
c |      9906 |  440889  1284458 |  161659    9906   459239    46.4 |  0.039 % |
c ==============================================================================
c Found solution: 370176
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10008 |  440898  1284480 |  146966   10008   463532    46.3 |  0.039 % |
c |     10108 |  440898  1284480 |  161662   10108   467155    46.2 |  0.039 % |
c ==============================================================================
c Found solution: 369792
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10173 |  440902  1284490 |  146967   10173   469622    46.2 |  0.039 % |
c |     10273 |  440902  1284490 |  161663   10273   473694    46.1 |  0.040 % |
c |     10424 |  440902  1284490 |  177830   10424   479990    46.0 |  0.040 % |
c ==============================================================================
c Found solution: 366464
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10486 |  440910  1284510 |  146970   10486   482731    46.0 |  0.040 % |
c |     10586 |  440910  1284510 |  161667   10586   487704    46.1 |  0.041 % |
c |     10736 |  440910  1284510 |  177833   10736   495363    46.1 |  0.041 % |
c |     10961 |  440910  1284510 |  195617   10961   506231    46.2 |  0.041 % |
c |     11300 |  440910  1284510 |  215178   11300   523137    46.3 |  0.041 % |
c ==============================================================================
c Found solution: 361728
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11531 |  440922  1284538 |  146974   11531   534301    46.3 |  0.041 % |
c |     11633 |  440922  1284538 |  161671   11633   538758    46.3 |  0.041 % |
c |     11783 |  440922  1284538 |  177838   11783   544623    46.2 |  0.041 % |
c ==============================================================================
c Found solution: 348800
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11924 |  440934  1284566 |  146978   11924   550662    46.2 |  0.041 % |
c |     12024 |  440934  1284566 |  161675   12024   554576    46.1 |  0.042 % |
c |     12174 |  440934  1284566 |  177843   12174   561272    46.1 |  0.042 % |
c |     12400 |  440934  1284566 |  195627   12400   571437    46.1 |  0.042 % |
c ==============================================================================
c Found solution: 334976
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12500 |  440942  1284584 |  146980   12500   575891    46.1 |  0.042 % |
c ==============================================================================
c Found solution: 332032
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12596 |  440953  1284609 |  146984   12596   579613    46.0 |  0.042 % |
c |     12696 |  440953  1284609 |  161682   12696   583453    46.0 |  0.043 % |
c |     12847 |  440953  1284609 |  177850   12847   590255    45.9 |  0.043 % |
c |     13072 |  440953  1284609 |  195635   13072   599872    45.9 |  0.043 % |
c ==============================================================================
c Found solution: 329216
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13274 |  440961  1284627 |  146987   13274   608552    45.8 |  0.043 % |
c |     13374 |  440961  1284627 |  161685   13374   612767    45.8 |  0.044 % |
c |     13524 |  440961  1284627 |  177854   13524   619668    45.8 |  0.044 % |
c ==============================================================================
c Found solution: 319104
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13639 |  440969  1284647 |  146989   13639   625710    45.9 |  0.044 % |
c |     13739 |  440969  1284647 |  161687   13739   629890    45.8 |  0.044 % |
c |     13897 |  440969  1284647 |  177856   13897   637746    45.9 |  0.044 % |
c |     14122 |  440969  1284647 |  195642   14122   648374    45.9 |  0.044 % |
c ==============================================================================
c Found solution: 315904
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14372 |  440977  1284667 |  146992   14372   658242    45.8 |  0.044 % |
c |     14475 |  440971  1284654 |  161691   14465   662041    45.8 |  0.046 % |
c |     14625 |  440971  1284654 |  177860   14615   668757    45.8 |  0.046 % |
c ==============================================================================
c Found solution: 304768
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14711 |  440982  1284679 |  146994   14701   672283    45.7 |  0.046 % |
c |     14816 |  440982  1284679 |  161693   14806   677451    45.8 |  0.047 % |
c |     14966 |  440982  1284679 |  177862   14956   683533    45.7 |  0.047 % |
c |     15191 |  440982  1284679 |  195649   15181   692486    45.6 |  0.047 % |
c |     15528 |  440982  1284679 |  215213   15518   709146    45.7 |  0.047 % |
c ==============================================================================
c Found solution: 299776
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15644 |  440991  1284700 |  146997   15634   713370    45.6 |  0.047 % |
c |     15744 |  440991  1284700 |  161696   15734   717890    45.6 |  0.048 % |
c |     15897 |  440991  1284700 |  177866   15887   725496    45.7 |  0.048 % |
c |     16122 |  440991  1284700 |  195653   16112   739108    45.9 |  0.048 % |
c ==============================================================================
c Found solution: 290944
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16208 |  440997  1284715 |  146999   16198   742649    45.8 |  0.048 % |
c |     16308 |  440997  1284715 |  161698   16298   746278    45.8 |  0.048 % |
c |     16458 |  440997  1284715 |  177868   16448   751421    45.7 |  0.048 % |
c |     16683 |  440997  1284715 |  195655   16673   761580    45.7 |  0.048 % |
c ==============================================================================
c Found solution: 290432
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16824 |  441005  1284734 |  147001   16814   767918    45.7 |  0.048 % |
c |     16925 |  441005  1284734 |  161701   16915   773134    45.7 |  0.049 % |
c |     17076 |  441005  1284734 |  177871   17066   779868    45.7 |  0.049 % |
c ==============================================================================
c Found solution: 274816
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17259 |  441014  1284755 |  147004   17249   787911    45.7 |  0.049 % |
c ==============================================================================
c Found solution: 274304
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17335 |  441023  1284775 |  147007   17325   791218    45.7 |  0.049 % |
c |     17435 |  441023  1284775 |  161707   17425   794011    45.6 |  0.050 % |
c |     17585 |  441023  1284775 |  177878   17575   801040    45.6 |  0.050 % |
c |     17810 |  441023  1284775 |  195666   17800   811743    45.6 |  0.050 % |
c |     18147 |  441015  1284757 |  215232   18136   828050    45.7 |  0.052 % |
c ==============================================================================
c Found solution: 273152
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18499 |  441025  1284780 |  147008   18488   843222    45.6 |  0.052 % |
c |     18599 |  441025  1284780 |  161708   18588   846957    45.6 |  0.052 % |
c |     18749 |  441025  1284780 |  177879   18738   853828    45.6 |  0.052 % |
c ==============================================================================
c Found solution: 272256
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18857 |  441032  1284795 |  147010   18846   858450    45.6 |  0.052 % |
c |     18957 |  441032  1284795 |  161711   18946   863843    45.6 |  0.053 % |
c |     19107 |  441032  1284795 |  177882   19096   869575    45.5 |  0.053 % |
c ==============================================================================
c Found solution: 272128
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19272 |  441042  1284817 |  147014   19261   877445    45.6 |  0.053 % |
c |     19372 |  441042  1284817 |  161715   19361   882035    45.6 |  0.054 % |
c ==============================================================================
c Found solution: 262400
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19382 |  441049  1284832 |  147016   19371   882452    45.6 |  0.054 % |
c |     19484 |  441049  1284832 |  161717   19473   887084    45.6 |  0.054 % |
c ==============================================================================
c Found solution: 246400
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19624 |  441058  1284854 |  147019   19613   893335    45.5 |  0.054 % |
c |     19725 |  441058  1284854 |  161720   19714   897482    45.5 |  0.055 % |
c |     19875 |  441058  1284854 |  177892   19864   911553    45.9 |  0.055 % |
c |     20101 |  441058  1284854 |  195682   20090   919918    45.8 |  0.055 % |
c ==============================================================================
c Found solution: 241536
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20304 |  441064  1284869 |  147021   20293   928231    45.7 |  0.055 % |
c |     20404 |  441064  1284869 |  161723   20393   931629    45.7 |  0.056 % |
c ==============================================================================
c Found solution: 240128
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20439 |  441071  1284887 |  147023   20428   932792    45.7 |  0.056 % |
c |     20539 |  441071  1284887 |  161725   20528   937206    45.7 |  0.056 % |
c ==============================================================================
c Found solution: 235264
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20688 |  441081  1284911 |  147027   20677   944124    45.7 |  0.056 % |
c ==============================================================================
c Found solution: 230400
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20751 |  441089  1284930 |  147029   20740   946610    45.6 |  0.056 % |
c ==============================================================================
c Found solution: 211968
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20777 |  441097  1284951 |  147032   20766   947909    45.6 |  0.056 % |
c |     20877 |  441097  1284951 |  161735   20866   951420    45.6 |  0.058 % |
c ==============================================================================
c Found solution: 205568
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20996 |  441100  1284958 |  147033   20985   957006    45.6 |  0.058 % |
c |     21096 |  441100  1284958 |  161736   21085   960796    45.6 |  0.059 % |
c |     21248 |  441100  1284958 |  177909   21237   967199    45.5 |  0.059 % |
c |     21475 |  441100  1284958 |  195700   21464   976785    45.5 |  0.059 % |
c ==============================================================================
c Found solution: 185472
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21659 |  441110  1284982 |  147036   21648   983981    45.5 |  0.059 % |
c |     21759 |  441097  1284955 |  161739   21715   986335    45.4 |  0.062 % |
c |     21909 |  441097  1284955 |  177913   21865   991891    45.4 |  0.062 % |
c |     22134 |  441097  1284955 |  195704   22090  1000890    45.3 |  0.062 % |
c |     22471 |  441097  1284955 |  215275   22427  1015061    45.3 |  0.062 % |
c ==============================================================================
c Found solution: 183296
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22595 |  441106  1284977 |  147035   22551  1020658    45.3 |  0.062 % |
c ==============================================================================
c Found solution: 153216
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22689 |  441117  1285002 |  147039   22645  1024070    45.2 |  0.062 % |
c |     22794 |  441117  1285002 |  161742   22750  1027704    45.2 |  0.063 % |
c |     22945 |  441117  1285002 |  177917   22901  1033448    45.1 |  0.063 % |
c ==============================================================================
c Found solution: 149888
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23023 |  441125  1285020 |  147041   22979  1036578    45.1 |  0.063 % |
c |     23125 |  441125  1285020 |  161745   23081  1041029    45.1 |  0.064 % |
c |     23275 |  441125  1285020 |  177919   23231  1050876    45.2 |  0.064 % |
c ==============================================================================
c Found solution: 145024
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23385 |  441132  1285036 |  147044   23341  1055448    45.2 |  0.064 % |
c |     23485 |  441132  1285036 |  161748   23441  1059200    45.2 |  0.065 % |
c ==============================================================================
c Found solution: 133248
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23491 |  441137  1285047 |  147045   23447  1059434    45.2 |  0.065 % |
c |     23592 |  441137  1285047 |  161749   23548  1062900    45.1 |  0.065 % |
c |     23742 |  441137  1285047 |  177924   23698  1072862    45.3 |  0.065 % |
c |     23968 |  441137  1285047 |  195716   23924  1082499    45.2 |  0.065 % |
c |     24305 |  441133  1285038 |  215288   24259  1098101    45.3 |  0.066 % |
c ==============================================================================
c Found solution: 130688
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24656 |  441100  1284953 |  147033   23871  1089236    45.6 |  0.066 % |
c |     24756 |  441100  1284953 |  161736   23971  1093219    45.6 |  0.076 % |
c ==============================================================================
c Found solution: 129280
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24893 |  441104  1284965 |  147034   24108  1099317    45.6 |  0.076 % |
c |     24993 |  441104  1284965 |  161737   24208  1103007    45.6 |  0.077 % |
c |     25143 |  441095  1284946 |  177911   24020  1095893    45.6 |  0.078 % |
c ==============================================================================
c Found solution: 121728
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25230 |  441100  1284959 |  147033   24107  1099504    45.6 |  0.078 % |
c ==============================================================================
c Found solution: 121344
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25288 |  441106  1284975 |  147035   24165  1101566    45.6 |  0.078 % |
c |     25388 |  441106  1284975 |  161738   24265  1105059    45.5 |  0.080 % |
c ==============================================================================
c Found solution: 120960
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25496 |  441112  1284991 |  147037   24373  1109073    45.5 |  0.080 % |
c |     25597 |  441112  1284991 |  161740   24474  1112801    45.5 |  0.080 % |
c ==============================================================================
c Found solution: 86016
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25667 |  441122  1285014 |  147040   24544  1114984    45.4 |  0.080 % |
c |     25768 |  441122  1285014 |  161744   24645  1118887    45.4 |  0.081 % |
c |     25919 |  441122  1285014 |  177918   24796  1124465    45.3 |  0.081 % |
c ==============================================================================
c Found solution: 85760
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25980 |  441130  1285033 |  147043   24857  1126707    45.3 |  0.081 % |
c ==============================================================================
c Found solution: 83968
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25984 |  441140  1285056 |  147046   24861  1126770    45.3 |  0.081 % |
c ==============================================================================
c Found solution: 81536
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26005 |  441145  1285068 |  147048   24882  1127820    45.3 |  0.081 % |
c ==============================================================================
c Found solution: 77568
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26038 |  441152  1285084 |  147050   24915  1128883    45.3 |  0.081 % |
c |     26138 |  441152  1285084 |  161755   25015  1132458    45.3 |  0.084 % |
c ==============================================================================
c Found solution: 75264
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26253 |  441155  1285091 |  147051   25130  1136516    45.2 |  0.084 % |
c |     26354 |  441155  1285091 |  161756   25231  1140043    45.2 |  0.084 % |
c |     26504 |  441155  1285091 |  177931   25381  1146202    45.2 |  0.084 % |
#### 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.69 0.87 0.89 1/54 18817
Raw data (stat): 18817 (runsolver) D 18816 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 481625506 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99982 s]
Raw data (loadavg): 0.74 0.88 0.89 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14381 0 0 0 917 33 0 0 25 0 1 0 481625506 65925120 13296 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16095 13296 603 41 0 16054 0
vsize: 64380
[startup+19.9993 s]
Raw data (loadavg): 0.78 0.88 0.89 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14517 0 0 0 1917 33 0 0 25 0 1 0 481625506 66510848 13405 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16238 13405 603 41 0 16197 0
vsize: 64952
[startup+29.9995 s]
Raw data (loadavg): 0.81 0.88 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14520 0 0 0 2916 34 0 0 25 0 1 0 481625506 66641920 13408 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16270 13408 603 41 0 16229 0
vsize: 65080
[startup+40 s]
Raw data (loadavg): 0.84 0.89 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14537 0 0 0 3916 34 0 0 25 0 1 0 481625506 66641920 13425 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16270 13425 603 41 0 16229 0
vsize: 65080
[startup+50.001 s]
Raw data (loadavg): 0.87 0.89 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14556 0 0 0 4916 34 0 0 25 0 1 0 481625506 66772992 13444 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16302 13444 603 41 0 16261 0
vsize: 65208
[startup+60.001 s]
Raw data (loadavg): 0.89 0.89 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14572 0 0 0 5916 34 0 0 25 0 1 0 481625506 66772992 13460 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16302 13460 603 41 0 16261 0
vsize: 65208
[startup+70.0002 s]
Raw data (loadavg): 0.90 0.90 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14585 0 0 0 6915 35 0 0 25 0 1 0 481625506 66908160 13473 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16335 13473 603 41 0 16294 0
vsize: 65340
[startup+80.0007 s]
Raw data (loadavg): 0.92 0.90 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14605 0 0 0 7915 35 0 0 25 0 1 0 481625506 66908160 13493 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16335 13493 603 41 0 16294 0
vsize: 65340
[startup+90.0007 s]
Raw data (loadavg): 0.93 0.90 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14624 0 0 0 8915 35 0 0 25 0 1 0 481625506 67039232 13512 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 13512 603 41 0 16326 0
vsize: 65468
[startup+100.001 s]
Raw data (loadavg): 0.94 0.90 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14638 0 0 0 9914 36 0 0 25 0 1 0 481625506 67039232 13526 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 13526 603 41 0 16326 0
vsize: 65468
[startup+110.001 s]
Raw data (loadavg): 0.95 0.91 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14653 0 0 0 10914 36 0 0 25 0 1 0 481625506 67162112 13541 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16397 13541 603 41 0 16356 0
vsize: 65588
[startup+120.001 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14667 0 0 0 11914 36 0 0 25 0 1 0 481625506 67162112 13555 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16397 13555 603 41 0 16356 0
vsize: 65588
[startup+130.001 s]
Raw data (loadavg): 0.96 0.91 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14682 0 0 0 12914 36 0 0 25 0 1 0 481625506 67297280 13570 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16430 13570 603 41 0 16389 0
vsize: 65720
[startup+140.001 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14696 0 0 0 13913 36 0 0 25 0 1 0 481625506 67297280 13584 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16430 13584 603 41 0 16389 0
vsize: 65720
[startup+150.002 s]
Raw data (loadavg): 0.97 0.92 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14714 0 0 0 14912 37 0 0 25 0 1 0 481625506 67424256 13602 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16461 13602 603 41 0 16420 0
vsize: 65844
[startup+160.008 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14732 0 0 0 15912 37 0 0 25 0 1 0 481625506 67424256 13620 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16461 13620 603 41 0 16420 0
vsize: 65844
[startup+170.008 s]
Raw data (loadavg): 1.05 0.94 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14744 0 0 0 16912 38 0 0 25 0 1 0 481625506 67555328 13632 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16493 13632 603 41 0 16452 0
vsize: 65972
[startup+180.008 s]
Raw data (loadavg): 1.04 0.94 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14760 0 0 0 17911 38 0 0 25 0 1 0 481625506 67555328 13648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16493 13648 603 41 0 16452 0
vsize: 65972
[startup+190.012 s]
Raw data (loadavg): 1.04 0.94 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14778 0 0 0 18911 38 0 0 25 0 1 0 481625506 67690496 13666 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16526 13666 603 41 0 16485 0
vsize: 66104
[startup+200.013 s]
Raw data (loadavg): 1.03 0.94 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14793 0 0 0 19911 39 0 0 25 0 1 0 481625506 67690496 13681 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16526 13681 603 41 0 16485 0
vsize: 66104
[startup+210.013 s]
Raw data (loadavg): 1.03 0.94 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14806 0 0 0 20911 39 0 0 25 0 1 0 481625506 67821568 13694 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16558 13694 603 41 0 16517 0
vsize: 66232
[startup+220.017 s]
Raw data (loadavg): 1.02 0.94 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14821 0 0 0 21911 39 0 0 25 0 1 0 481625506 67821568 13709 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16558 13709 603 41 0 16517 0
vsize: 66232
[startup+230.026 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14836 0 0 0 22911 40 0 0 25 0 1 0 481625506 67821568 13724 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16558 13724 603 41 0 16517 0
vsize: 66232
[startup+240.026 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14849 0 0 0 23911 40 0 0 25 0 1 0 481625506 67956736 13737 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16591 13737 603 41 0 16550 0
vsize: 66364
[startup+250.026 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14862 0 0 0 24911 40 0 0 25 0 1 0 481625506 67956736 13750 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16591 13750 603 41 0 16550 0
vsize: 66364
[startup+260.028 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14879 0 0 0 25911 40 0 0 25 0 1 0 481625506 68087808 13767 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16623 13767 603 41 0 16582 0
vsize: 66492
[startup+270.038 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14890 0 0 0 26911 41 0 0 25 0 1 0 481625506 68087808 13778 4294967295 134512640 134672761 3221224528 3221223664 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16623 13778 603 41 0 16582 0
vsize: 66492
[startup+280.143 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14908 0 0 0 27921 41 0 0 25 0 1 0 481625506 68218880 13796 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16655 13796 603 41 0 16614 0
vsize: 66620
[startup+290.143 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14919 0 0 0 28921 41 0 0 25 0 1 0 481625506 68218880 13807 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16655 13807 603 41 0 16614 0
vsize: 66620
[startup+300.144 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14930 0 0 0 29921 41 0 0 25 0 1 0 481625506 68218880 13818 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16655 13818 603 41 0 16614 0
vsize: 66620
[startup+310.143 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 18817
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14947 0 0 0 30919 41 0 0 25 0 1 0 481625506 68354048 13835 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16688 13835 603 41 0 16647 0
vsize: 66752
[startup+320.143 s]
Raw data (loadavg): 1.00 0.95 0.91 3/58 18824
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14971 0 0 0 31919 41 0 0 25 0 1 0 481625506 68534272 13859 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16732 13859 603 41 0 16691 0
vsize: 66928
[startup+330.144 s]
Raw data (loadavg): 1.07 0.97 0.92 2/54 18870
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14978 0 0 0 32920 41 0 0 25 0 1 0 481625506 68534272 13866 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16732 13866 603 41 0 16691 0
vsize: 66928
[startup+340.162 s]
Raw data (loadavg): 1.06 0.97 0.92 2/54 18870
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 14989 0 0 0 33921 42 0 0 25 0 1 0 481625506 68534272 13877 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16732 13877 603 41 0 16691 0
vsize: 66928
[startup+350.162 s]
Raw data (loadavg): 1.05 0.97 0.92 2/54 18870
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15001 0 0 0 34922 42 0 0 25 0 1 0 481625506 68534272 13889 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16732 13889 603 41 0 16691 0
vsize: 66928
[startup+360.163 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 18870
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15015 0 0 0 35922 42 0 0 25 0 1 0 481625506 68669440 13903 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16765 13903 603 41 0 16724 0
vsize: 67060
[startup+370.162 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 18870
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15024 0 0 0 36922 42 0 0 25 0 1 0 481625506 68669440 13912 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16765 13912 603 41 0 16724 0
vsize: 67060
[startup+380.162 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 18870
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15034 0 0 0 37922 42 0 0 25 0 1 0 481625506 68669440 13922 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16765 13922 603 41 0 16724 0
vsize: 67060
[startup+390.17 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15047 0 0 0 38923 42 0 0 25 0 1 0 481625506 68800512 13935 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16797 13935 603 41 0 16756 0
vsize: 67188
[startup+400.18 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15056 0 0 0 39923 42 0 0 25 0 1 0 481625506 68800512 13944 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16797 13944 603 41 0 16756 0
vsize: 67188
[startup+410.179 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15071 0 0 0 40923 42 0 0 25 0 1 0 481625506 68800512 13959 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16797 13959 603 41 0 16756 0
vsize: 67188
[startup+420.179 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15079 0 0 0 41923 42 0 0 25 0 1 0 481625506 68931584 13967 4294967295 134512640 134672761 3221224528 3221223664 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16829 13967 603 41 0 16788 0
vsize: 67316
[startup+430.179 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15092 0 0 0 42924 42 0 0 25 0 1 0 481625506 68931584 13980 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16829 13980 603 41 0 16788 0
vsize: 67316
[startup+440.179 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15106 0 0 0 43924 42 0 0 25 0 1 0 481625506 69062656 13994 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16861 13994 603 41 0 16820 0
vsize: 67444
[startup+450.179 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15119 0 0 0 44924 42 0 0 25 0 1 0 481625506 69062656 14007 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16861 14007 603 41 0 16820 0
vsize: 67444
[startup+460.179 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15130 0 0 0 45924 42 0 0 25 0 1 0 481625506 69062656 14018 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16861 14018 603 41 0 16820 0
vsize: 67444
[startup+470.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15144 0 0 0 46924 42 0 0 25 0 1 0 481625506 69193728 14032 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16893 14032 603 41 0 16852 0
vsize: 67572
[startup+480.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15155 0 0 0 47924 42 0 0 25 0 1 0 481625506 69193728 14043 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16893 14043 603 41 0 16852 0
vsize: 67572
[startup+490.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15168 0 0 0 48924 42 0 0 25 0 1 0 481625506 69193728 14056 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16893 14056 603 41 0 16852 0
vsize: 67572
[startup+500.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15182 0 0 0 49925 42 0 0 25 0 1 0 481625506 69320704 14070 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16924 14070 603 41 0 16883 0
vsize: 67696
[startup+510.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15196 0 0 0 50925 42 0 0 25 0 1 0 481625506 69320704 14084 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16924 14084 603 41 0 16883 0
vsize: 67696
[startup+520.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15207 0 0 0 51925 42 0 0 25 0 1 0 481625506 69439488 14095 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 14095 603 41 0 16912 0
vsize: 67812
[startup+530.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15220 0 0 0 52925 42 0 0 25 0 1 0 481625506 69439488 14108 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 14108 603 41 0 16912 0
vsize: 67812
[startup+540.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15234 0 0 0 53925 43 0 0 25 0 1 0 481625506 69570560 14122 4294967295 134512640 134672761 3221224528 3221223696 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16985 14122 603 41 0 16944 0
vsize: 67940
[startup+550.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15242 0 0 0 54925 43 0 0 25 0 1 0 481625506 69570560 14130 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16985 14130 603 41 0 16944 0
vsize: 67940
[startup+560.179 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15255 0 0 0 55925 43 0 0 25 0 1 0 481625506 69570560 14143 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16985 14143 603 41 0 16944 0
vsize: 67940
[startup+570.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15272 0 0 0 56925 43 0 0 25 0 1 0 481625506 69701632 14160 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17017 14160 603 41 0 16976 0
vsize: 68068
[startup+580.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15283 0 0 0 57925 43 0 0 25 0 1 0 481625506 69701632 14171 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17017 14171 603 41 0 16976 0
vsize: 68068
[startup+590.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15300 0 0 0 58925 43 0 0 25 0 1 0 481625506 69836800 14188 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17050 14188 603 41 0 17009 0
vsize: 68200
[startup+600.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15312 0 0 0 59925 43 0 0 25 0 1 0 481625506 69836800 14200 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17050 14200 603 41 0 17009 0
vsize: 68200
[startup+610.177 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15324 0 0 0 60926 43 0 0 25 0 1 0 481625506 69836800 14212 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17050 14212 603 41 0 17009 0
vsize: 68200
[startup+620.177 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15336 0 0 0 61925 43 0 0 25 0 1 0 481625506 69967872 14224 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17082 14224 603 41 0 17041 0
vsize: 68328
[startup+630.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15343 0 0 0 62926 43 0 0 25 0 1 0 481625506 69967872 14231 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17082 14231 603 41 0 17041 0
vsize: 68328
[startup+640.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15352 0 0 0 63926 43 0 0 25 0 1 0 481625506 69967872 14240 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17082 14240 603 41 0 17041 0
vsize: 68328
[startup+650.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15366 0 0 0 64926 43 0 0 25 0 1 0 481625506 70098944 14254 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17114 14254 603 41 0 17073 0
vsize: 68456
[startup+660.177 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18872
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15375 0 0 0 65926 43 0 0 25 0 1 0 481625506 70098944 14263 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17114 14263 603 41 0 17073 0
vsize: 68456
[startup+670.177 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15392 0 0 0 66926 43 0 0 25 0 1 0 481625506 70242304 14280 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17149 14280 603 41 0 17108 0
vsize: 68596
[startup+680.194 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15403 0 0 0 67928 43 0 0 25 0 1 0 481625506 70242304 14291 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17149 14291 603 41 0 17108 0
vsize: 68596
[startup+690.196 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15423 0 0 0 68929 43 0 0 25 0 1 0 481625506 70438912 14311 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17197 14311 603 41 0 17156 0
vsize: 68788
[startup+700.934 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15431 0 0 0 70003 43 0 0 25 0 1 0 481625506 70438912 14319 4294967295 134512640 134672761 3221224528 3221223696 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17197 14319 603 41 0 17156 0
vsize: 68788
[startup+710.936 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15442 0 0 0 71003 43 0 0 25 0 1 0 481625506 70438912 14330 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17197 14330 603 41 0 17156 0
vsize: 68788
[startup+720.964 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15458 0 0 0 72006 44 0 0 25 0 1 0 481625506 70574080 14346 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17230 14346 603 41 0 17189 0
vsize: 68920
[startup+730.964 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15465 0 0 0 73006 44 0 0 25 0 1 0 481625506 70574080 14353 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17230 14353 603 41 0 17189 0
vsize: 68920
[startup+740.978 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15476 0 0 0 74007 44 0 0 25 0 1 0 481625506 70574080 14364 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17230 14364 603 41 0 17189 0
vsize: 68920
[startup+750.978 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15488 0 0 0 75008 44 0 0 25 0 1 0 481625506 70709248 14376 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17263 14376 603 41 0 17222 0
vsize: 69052
[startup+760.978 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15499 0 0 0 76008 44 0 0 25 0 1 0 481625506 70705152 14387 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17262 14387 603 41 0 17221 0
vsize: 69048
[startup+770.983 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15511 0 0 0 77008 44 0 0 25 0 1 0 481625506 70705152 14399 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17262 14399 603 41 0 17221 0
vsize: 69048
[startup+780.995 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15520 0 0 0 78010 44 0 0 25 0 1 0 481625506 70823936 14408 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17291 14408 603 41 0 17250 0
vsize: 69164
[startup+790.995 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15528 0 0 0 79010 44 0 0 25 0 1 0 481625506 70823936 14416 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17291 14416 603 41 0 17250 0
vsize: 69164
[startup+800.995 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15539 0 0 0 80010 44 0 0 25 0 1 0 481625506 70823936 14427 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17291 14427 603 41 0 17250 0
vsize: 69164
[startup+810.996 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15549 0 0 0 81010 44 0 0 25 0 1 0 481625506 70823936 14437 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17291 14437 603 41 0 17250 0
vsize: 69164
[startup+820.995 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15560 0 0 0 82011 44 0 0 25 0 1 0 481625506 70955008 14448 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17323 14448 603 41 0 17282 0
vsize: 69292
[startup+831 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15567 0 0 0 83011 44 0 0 25 0 1 0 481625506 70955008 14455 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17323 14455 603 41 0 17282 0
vsize: 69292
[startup+841 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15581 0 0 0 84012 44 0 0 25 0 1 0 481625506 71081984 14469 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17354 14469 603 41 0 17313 0
vsize: 69416
[startup+851.002 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15596 0 0 0 85011 44 0 0 25 0 1 0 481625506 71081984 14484 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17354 14484 603 41 0 17313 0
vsize: 69416
[startup+861.002 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15609 0 0 0 86011 44 0 0 25 0 1 0 481625506 71081984 14497 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17354 14497 603 41 0 17313 0
vsize: 69416
[startup+871.001 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15624 0 0 0 87011 44 0 0 25 0 1 0 481625506 71217152 14512 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17387 14512 603 41 0 17346 0
vsize: 69548
[startup+881.02 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15632 0 0 0 88014 44 0 0 25 0 1 0 481625506 71217152 14520 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17387 14520 603 41 0 17346 0
vsize: 69548
[startup+891.021 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15644 0 0 0 89014 44 0 0 25 0 1 0 481625506 71352320 14532 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17420 14532 603 41 0 17379 0
vsize: 69680
[startup+901.027 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15654 0 0 0 90014 44 0 0 25 0 1 0 481625506 71352320 14542 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17420 14542 603 41 0 17379 0
vsize: 69680
[startup+911.027 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15663 0 0 0 91014 44 0 0 25 0 1 0 481625506 71352320 14551 4294967295 134512640 134672761 3221224528 3221223728 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17420 14551 603 41 0 17379 0
vsize: 69680
[startup+921.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15681 0 0 0 92015 44 0 0 25 0 1 0 481625506 71483392 14569 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17452 14569 603 41 0 17411 0
vsize: 69808
[startup+931.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15684 0 0 0 93015 44 0 0 25 0 1 0 481625506 71483392 14572 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17452 14572 603 41 0 17411 0
vsize: 69808
[startup+941.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15692 0 0 0 94015 44 0 0 25 0 1 0 481625506 71483392 14580 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17452 14580 603 41 0 17411 0
vsize: 69808
[startup+951.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15703 0 0 0 95015 44 0 0 25 0 1 0 481625506 71483392 14591 4294967295 134512640 134672761 3221224528 3221223776 134562614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17452 14591 603 41 0 17411 0
vsize: 69808
[startup+961.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15710 0 0 0 96015 44 0 0 25 0 1 0 481625506 71622656 14598 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17486 14598 603 41 0 17445 0
vsize: 69944
[startup+971.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15718 0 0 0 97015 44 0 0 25 0 1 0 481625506 71622656 14606 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17486 14606 603 41 0 17445 0
vsize: 69944
[startup+981.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15730 0 0 0 98016 44 0 0 25 0 1 0 481625506 71622656 14618 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17486 14618 603 41 0 17445 0
vsize: 69944
[startup+991.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15739 0 0 0 99017 44 0 0 25 0 1 0 481625506 71622656 14627 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17486 14627 603 41 0 17445 0
vsize: 69944
[startup+1001.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15745 0 0 0 100017 44 0 0 25 0 1 0 481625506 71753728 14633 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17518 14633 603 41 0 17477 0
vsize: 70072
[startup+1011.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15760 0 0 0 101018 44 0 0 25 0 1 0 481625506 71753728 14648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17518 14648 603 41 0 17477 0
vsize: 70072
[startup+1021.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15768 0 0 0 102018 44 0 0 25 0 1 0 481625506 71753728 14656 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17518 14656 603 41 0 17477 0
vsize: 70072
[startup+1031.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15778 0 0 0 103018 44 0 0 25 0 1 0 481625506 71872512 14666 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17547 14666 603 41 0 17506 0
vsize: 70188
[startup+1041.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15786 0 0 0 104018 44 0 0 25 0 1 0 481625506 71872512 14674 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17547 14674 603 41 0 17506 0
vsize: 70188
[startup+1051.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15799 0 0 0 105018 44 0 0 25 0 1 0 481625506 71872512 14687 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17547 14687 603 41 0 17506 0
vsize: 70188
[startup+1061.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15815 0 0 0 106019 44 0 0 25 0 1 0 481625506 72003584 14703 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17579 14703 603 41 0 17538 0
vsize: 70316
[startup+1071.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15833 0 0 0 107019 44 0 0 25 0 1 0 481625506 72146944 14721 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14721 603 41 0 17573 0
vsize: 70456
[startup+1081.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15842 0 0 0 108019 44 0 0 25 0 1 0 481625506 72146944 14730 4294967295 134512640 134672761 3221224528 3221223712 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14730 603 41 0 17573 0
vsize: 70456
[startup+1091.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15847 0 0 0 109019 45 0 0 25 0 1 0 481625506 72146944 14735 4294967295 134512640 134672761 3221224528 3221223728 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14735 603 41 0 17573 0
vsize: 70456
[startup+1101.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15847 0 0 0 110019 45 0 0 25 0 1 0 481625506 72146944 14735 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14735 603 41 0 17573 0
vsize: 70456
[startup+1111.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15849 0 0 0 111019 45 0 0 25 0 1 0 481625506 72146944 14737 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14737 603 41 0 17573 0
vsize: 70456
[startup+1121.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15849 0 0 0 112019 45 0 0 25 0 1 0 481625506 72146944 14737 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14737 603 41 0 17573 0
vsize: 70456
[startup+1131.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15853 0 0 0 113020 45 0 0 25 0 1 0 481625506 72146944 14741 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14741 603 41 0 17573 0
vsize: 70456
[startup+1141.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15853 0 0 0 114020 45 0 0 25 0 1 0 481625506 72146944 14741 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14741 603 41 0 17573 0
vsize: 70456
[startup+1151.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15862 0 0 0 115020 45 0 0 25 0 1 0 481625506 72146944 14750 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17614 14750 603 41 0 17573 0
vsize: 70456
[startup+1161.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15868 0 0 0 116020 45 0 0 25 0 1 0 481625506 72273920 14756 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17645 14756 603 41 0 17604 0
vsize: 70580
[startup+1171.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15875 0 0 0 117020 45 0 0 25 0 1 0 481625506 72273920 14763 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17645 14763 603 41 0 17604 0
vsize: 70580
[startup+1181.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15881 0 0 0 118020 45 0 0 25 0 1 0 481625506 72273920 14769 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17645 14769 603 41 0 17604 0
vsize: 70580
[startup+1191.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15887 0 0 0 119021 45 0 0 25 0 1 0 481625506 72273920 14775 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17645 14775 603 41 0 17604 0
vsize: 70580
[startup+1201.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 18874
Raw data (stat): 18817 (minisat+) R 18816 25347 25346 0 -1 0 15895 0 0 0 120021 45 0 0 25 0 1 0 481625506 72273920 14783 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17645 14783 603 41 0 17604 0
vsize: 70580
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1201.08 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 18874
Raw data (stat): 18817 (minisat+) Z 18816 25347 25346 0 -1 12 15898 0 0 0 120021 48 0 0 25 0 1 0 481625506 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): 1201.08
CPU time (s): 1200.7
CPU user time (s): 1200.21
CPU system time (s): 0.486925
CPU usage (%): 99.9683
Max. virtual memory (Kb): 70580
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####