PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare1.opb
MD5SUM	6f06e375914e0285ec75de90ad627758
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
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 numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.1
Number of variables	170
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	70
Trace number 32322

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        786020 kB
Buffers:          8328 kB
Cached:         219384 kB
SwapCached:        972 kB
Active:          17204 kB
Inactive:       212604 kB
HighTotal:      131008 kB
HighFree:        17724 kB
LowTotal:       903652 kB
LowFree:        768296 kB
SwapTotal:     2097892 kB
SwapFree:      2096008 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           5128 kB
Slab:            12992 kB
Committed_AS:    63916 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 09:29:36 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 23713 7 1229.86 152
#### 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 [1mFound solution: 862848[0m
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 [1mFound solution: 860928[0m
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 [1mFound solution: 848640[0m
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 [1mFound solution: 839296[0m
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 [1mFound solution: 835328[0m
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 [1mFound solution: 811776[0m
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 [1mFound solution: 793344[0m
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 [1mFound solution: 788224[0m
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 [1mFound solution: 784256[0m
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 [1mFound solution: 760704[0m
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 [1mFound solution: 760064[0m
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 [1mFound solution: 755840[0m
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 [1mFound solution: 740864[0m
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 [1mFound solution: 740224[0m
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 [1mFound solution: 669184[0m
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 [1mFound solution: 619392[0m
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 [1mFound solution: 616960[0m
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 [1mFound solution: 612992[0m
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 [1mFound solution: 600448[0m
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 [1mFound solution: 594048[0m
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 [1mFound solution: 593792[0m
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 [1mFound solution: 576896[0m
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 [1mFound solution: 576128[0m
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 [1mFound solution: 573568[0m
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 [1mFound solution: 573312[0m
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 [1mFound solution: 572288[0m
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 [1mFound solution: 566400[0m
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 [1mFound solution: 566144[0m
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 [1mFound solution: 542848[0m
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 [1mFound solution: 534400[0m
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 [1mFound solution: 531584[0m
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 [1mFound solution: 509312[0m
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 [1mFound solution: 418560[0m
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 [1mFound solution: 411264[0m
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 [1mFound solution: 408064[0m
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 [1mFound solution: 406016[0m
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 [1mFound solution: 404608[0m
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 [1mFound solution: 401664[0m
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 [1mFound solution: 392064[0m
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 [1mFound solution: 386176[0m
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 [1mFound solution: 381952[0m
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 [1mFound solution: 370176[0m
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 [1mFound solution: 369792[0m
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 [1mFound solution: 366464[0m
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 [1mFound solution: 361728[0m
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 [1mFound solution: 348800[0m
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 [1mFound solution: 334976[0m
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 [1mFound solution: 332032[0m
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 [1mFound solution: 329216[0m
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 [1mFound solution: 319104[0m
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 [1mFound solution: 315904[0m
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 [1mFound solution: 304768[0m
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 [1mFound solution: 299776[0m
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 [1mFound solution: 290944[0m
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 [1mFound solution: 290432[0m
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 [1mFound solution: 274816[0m
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 [1mFound solution: 274304[0m
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 [1mFound solution: 273152[0m
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 [1mFound solution: 272256[0m
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 [1mFound solution: 272128[0m
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 [1mFound solution: 262400[0m
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 [1mFound solution: 246400[0m
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 [1mFound solution: 241536[0m
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 [1mFound solution: 240128[0m
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 [1mFound solution: 235264[0m
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 [1mFound solution: 230400[0m
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 [1mFound solution: 211968[0m
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 [1mFound solution: 205568[0m
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 [1mFound solution: 185472[0m
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 [1mFound solution: 183296[0m
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 [1mFound solution: 153216[0m
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 [1mFound solution: 149888[0m
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 [1mFound solution: 145024[0m
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 [1mFound solution: 133248[0m
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 [1mFound solution: 130688[0m
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 [1mFound solution: 129280[0m
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 [1mFound solution: 121728[0m
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 [1mFound solution: 121344[0m
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 [1mFound solution: 120960[0m
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 [1mFound solution: 86016[0m
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 [1mFound solution: 85760[0m
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 [1mFound solution: 83968[0m
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 [1mFound solution: 81536[0m
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 [1mFound solution: 77568[0m
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 [1mFound solution: 75264[0m
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 % |
c |     26729 |  441155  1285091 |  195724   25606  1154457    45.1 |  0.084 % |
c ==============================================================================
c [1mFound solution: 66816[0m
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 |     26850 |  441158  1285098 |  147052   25727  1158926    45.0 |  0.084 % |
c |     26951 |  441158  1285098 |  161757   25828  1162787    45.0 |  0.085 % |
c |     27102 |  441158  1285098 |  177932   25979  1168196    45.0 |  0.085 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 28464 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.91 0.95 0.90 2/55 28460
Raw data (stat): 28460 (runsolver) R 28459 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 732232037 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99993 s]
Raw data (loadavg): 0.92 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0006 s]
Raw data (loadavg): 0.93 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+99.9999 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.69 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28464
Raw data (stat): 28460 (minisat+_script) S 28459 32363 32362 0 -1 0 275 239 0 0 0 1 0 0 20 0 1 0 732232037 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.69
CPU time (s): 1229.86
CPU user time (s): 1229.35
CPU system time (s): 0.517921
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####