PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare2.opb
MD5SUM	c00b2eef1eabd5880b83093b756a5dd4
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	429056
Optimality of the best value was proved	NO
Number of terms in the objective function	210
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	7516192761
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	7516192761
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1201.34
Number of variables	270
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	90
Trace number 21842

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-22 01:17:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12654 boxname=wulflinc24 idbench=974 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c00b2eef1eabd5880b83093b756a5dd4  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2.opb
IDLAUNCH: 12654
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        472984 kB
Buffers:         34552 kB
Cached:         502804 kB
SwapCached:        524 kB
Active:         215704 kB
Inactive:       323656 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        472732 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16692 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:37:58 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 12654 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 3452927   bits: 23/22
c ---[  10]---> Adder-cost: 380   maxlim: 3689471   bits: 23/22
c ---[   8]---> Adder-cost: 350   maxlim: 3561471   bits: 23/22
c ---[   6]---> Adder-cost: 340   maxlim: 3823615   bits: 23/22
c ---[   4]---> Adder-cost: 390   maxlim: 3614719   bits: 23/22
c ---[   2]---> Adder-cost: 358   maxlim: 3749887   bits: 23/22
c ---[   0]---> Adder-cost: 374   maxlim: 3556351   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17214    61202 |    6314      99      310     3.1 | 12.761 % |
c ==============================================================================
c [1mFound solution: 9929728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       170 |   19863    67394 |    6621     169      862     5.1 | 12.761 % |
c |       270 |   19847    67342 |    7283     267     1398     5.2 |  9.797 % |
c ==============================================================================
c [1mFound solution: 9154560[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       390 |   19874    67444 |    6624     387     3000     7.8 |  9.797 % |
c ==============================================================================
c [1mFound solution: 9147392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       420 |   19888    67485 |    6629     417     6353    15.2 |  9.797 % |
c |       520 |   19888    67485 |    7291     517    10812    20.9 |  9.776 % |
c ==============================================================================
c [1mFound solution: 7954432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       552 |   19902    67521 |    6634     549    12623    23.0 |  9.776 % |
c ==============================================================================
c [1mFound solution: 7805952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       598 |   19914    67554 |    6638     595    16053    27.0 |  9.776 % |
c |       699 |   19890    67476 |    7301     693    28096    40.5 |  9.863 % |
c |       851 |   19882    67450 |    8031     844    41822    49.6 |  9.888 % |
c ==============================================================================
c [1mFound solution: 7643136[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       986 |   19894    67479 |    6631     979    63040    64.4 |  9.888 % |
c ==============================================================================
c [1mFound solution: 6888448[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1042 |   19906    67503 |    6635    1034    67129    64.9 |  9.888 % |
c |      1144 |   19906    67503 |    7298    1136    81563    71.8 |  9.914 % |
c |      1295 |   19906    67503 |    8028    1287    98275    76.4 |  9.914 % |
c |      1520 |   19898    67477 |    8831    1511   117286    77.6 |  9.939 % |
c |      1858 |   19898    67477 |    9714    1849   140264    75.9 |  9.939 % |
c |      2364 |   19898    67477 |   10685    2355   182832    77.6 |  9.939 % |
c |      3123 |   19898    67477 |   11754    3114   256165    82.3 |  9.939 % |
c ==============================================================================
c [1mFound solution: 5861376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3469 |   19904    67486 |    6634    3459   283309    81.9 |  9.939 % |
c |      3569 |   19904    67486 |    7297    3559   300055    84.3 |  9.967 % |
c |      3720 |   19904    67486 |    8027    3710   307885    83.0 |  9.967 % |
c |      3945 |   19904    67486 |    8829    3935   344859    87.6 |  9.967 % |
c |      4282 |   19904    67486 |    9712    4272   396303    92.8 |  9.967 % |
c |      4789 |   19904    67486 |   10684    4779   432588    90.5 |  9.967 % |
c |      5548 |   19904    67486 |   11752    5538   541320    97.7 |  9.967 % |
c ==============================================================================
c [1mFound solution: 5195776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5997 |   19918    67523 |    6639    5987   601231   100.4 |  9.967 % |
c |      6098 |   19918    67523 |    7302    6088   618703   101.6 |  9.970 % |
c |      6249 |   19918    67523 |    8033    6239   626932   100.5 |  9.970 % |
c |      6475 |   19910    67497 |    8836    6464   656309   101.5 |  9.995 % |
c |      6812 |   19910    67497 |    9720    6801   696089   102.4 |  9.995 % |
c |      7320 |   19910    67497 |   10692    7309   731836   100.1 |  9.995 % |
c |      8082 |   19910    67497 |   11761    8071   795887    98.6 |  9.995 % |
c |      9221 |   19910    67497 |   12937    9210   908038    98.6 |  9.995 % |
c |     10930 |   19910    67497 |   14231   10919  1103571   101.1 |  9.995 % |
c |     13493 |   19910    67497 |   15654   13482  1375845   102.1 |  9.995 % |
c |     17337 |   19910    67497 |   17219    8787   834221    94.9 |  9.995 % |
c |     23104 |   19880    67401 |   18941   14550  1340020    92.1 | 10.095 % |
c |     31753 |   19880    67401 |   20836   12937  1343299   103.8 | 10.095 % |
c ==============================================================================
c [1mFound solution: 5003264[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32527 |   19890    67428 |    6630   13711  1411626   103.0 | 10.095 % |
c |     32627 |   19890    67428 |    7293    6956   715766   102.9 | 10.105 % |
c |     32778 |   19890    67428 |    8022    7107   727028   102.3 | 10.105 % |
c |     33003 |   19890    67428 |    8824    7332   754819   102.9 | 10.105 % |
c |     33341 |   19890    67428 |    9706    7670   787535   102.7 | 10.105 % |
c |     33847 |   19890    67428 |   10677    8176   839414   102.7 | 10.105 % |
c |     34607 |   19890    67428 |   11745    8936   873644    97.8 | 10.105 % |
c |     35747 |   19890    67428 |   12919   10076   941502    93.4 | 10.105 % |
c ==============================================================================
c [1mFound solution: 4755456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35779 |   19904    67460 |    6634   10108   942640    93.3 | 10.105 % |
c |     35879 |   19904    67460 |    7297    5154   282091    54.7 | 10.110 % |
c |     36030 |   19904    67460 |    8027    5305   293923    55.4 | 10.110 % |
c |     36258 |   19904    67460 |    8829    5533   315402    57.0 | 10.110 % |
c |     36595 |   19904    67460 |    9712    5870   343649    58.5 | 10.110 % |
c |     37103 |   19896    67434 |   10684    6377   396528    62.2 | 10.135 % |
c |     37862 |   19896    67434 |   11752    7136   463376    64.9 | 10.135 % |
c |     39001 |   19896    67434 |   12927    8275   565260    68.3 | 10.135 % |
c ==============================================================================
c [1mFound solution: 4734976[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39899 |   19909    67464 |    6636    9173   639714    69.7 | 10.135 % |
c ==============================================================================
c [1mFound solution: 3594240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39906 |   19920    67491 |    6640    4594   288279    62.8 | 10.135 % |
c |     40008 |   19920    67491 |    7304    4696   295775    63.0 | 10.150 % |
c |     40158 |   19920    67491 |    8034    4846   308279    63.6 | 10.150 % |
c |     40384 |   19920    67491 |    8837    5072   332107    65.5 | 10.150 % |
c |     40721 |   19920    67491 |    9721    5409   357102    66.0 | 10.150 % |
c |     41227 |   19920    67491 |   10693    5915   380151    64.3 | 10.150 % |
c |     41988 |   19920    67491 |   11763    6676   455590    68.2 | 10.150 % |
c ==============================================================================
c [1mFound solution: 3588096[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42026 |   19928    67511 |    6642    6714   457571    68.2 | 10.150 % |
c |     42126 |   19928    67511 |    7306    6814   470595    69.1 | 10.162 % |
c |     42276 |   19928    67511 |    8036    6964   479269    68.8 | 10.162 % |
c |     42501 |   19928    67511 |    8840    7189   491049    68.3 | 10.162 % |
c |     42839 |   19928    67511 |    9724    7527   539920    71.7 | 10.162 % |
c |     43346 |   19928    67511 |   10697    8034   570107    71.0 | 10.162 % |
c |     44105 |   19928    67511 |   11766    8793   627248    71.3 | 10.162 % |
c |     45245 |   19928    67511 |   12943    9933   697751    70.2 | 10.162 % |
c ==============================================================================
c [1mFound solution: 2887680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45267 |   19940    67539 |    6646    9955   698020    70.1 | 10.162 % |
c |     45369 |   19940    67539 |    7310    5080   268355    52.8 | 10.172 % |
c |     45519 |   19940    67539 |    8041    5230   273672    52.3 | 10.172 % |
c |     45744 |   19940    67539 |    8845    5455   303851    55.7 | 10.172 % |
c |     46082 |   19940    67539 |    9730    5793   324113    55.9 | 10.172 % |
c |     46589 |   19940    67539 |   10703    6300   343830    54.6 | 10.172 % |
c |     47349 |   19940    67539 |   11773    7060   403882    57.2 | 10.172 % |
c |     48488 |   19932    67513 |   12951    8198   536289    65.4 | 10.196 % |
c |     50196 |   19924    67487 |   14246    9905   614440    62.0 | 10.221 % |
c |     52762 |   19918    67469 |   15670   12470   771014    61.8 | 10.246 % |
c |     56606 |   19918    67469 |   17238   16314  1003494    61.5 | 10.246 % |
c ==============================================================================
c [1mFound solution: 2847744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57500 |   19929    67497 |    6643   17208  1113811    64.7 | 10.246 % |
c |     57601 |   19929    67497 |    7307    4403   226769    51.5 | 10.253 % |
c |     57751 |   19929    67497 |    8038    4553   240342    52.8 | 10.253 % |
c |     57976 |   19929    67497 |    8841    4778   248307    52.0 | 10.253 % |
c |     58313 |   19929    67497 |    9726    5115   266177    52.0 | 10.253 % |
c |     58819 |   19929    67497 |   10698    5621   301876    53.7 | 10.253 % |
c |     59580 |   19929    67497 |   11768    6382   405638    63.6 | 10.253 % |
c |     60719 |   19929    67497 |   12945    7521   468128    62.2 | 10.253 % |
c |     62427 |   19929    67497 |   14239    9229   530637    57.5 | 10.253 % |
c |     64989 |   19929    67497 |   15663   11791   930394    78.9 | 10.253 % |
c ==============================================================================
c [1mFound solution: 2835456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68346 |   19941    67526 |    6647   15148  1223872    80.8 | 10.253 % |
c |     68447 |   19941    67526 |    7311    3888   198569    51.1 | 10.258 % |
c |     68597 |   19941    67526 |    8042    4038   203731    50.5 | 10.258 % |
c |     68824 |   19941    67526 |    8847    4265   220342    51.7 | 10.258 % |
c |     69162 |   19941    67526 |    9731    4603   235771    51.2 | 10.258 % |
c |     69669 |   19941    67526 |   10705    5110   253501    49.6 | 10.258 % |
c |     70428 |   19941    67526 |   11775    5869   306369    52.2 | 10.258 % |
c |     71569 |   19937    67517 |   12953    7009   426770    60.9 | 10.282 % |
c |     73277 |   19937    67517 |   14248    8717   529658    60.8 | 10.282 % |
c |     75839 |   19937    67517 |   15673   11279   655327    58.1 | 10.282 % |
c ==============================================================================
c [1mFound solution: 2778112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77546 |   19948    67544 |    6649   12986   731385    56.3 | 10.282 % |
c |     77646 |   19948    67544 |    7313    6593   247614    37.6 | 10.289 % |
c |     77797 |   19948    67544 |    8045    6744   256608    38.0 | 10.289 % |
c |     78023 |   19948    67544 |    8849    6970   268841    38.6 | 10.289 % |
c |     78362 |   19948    67544 |    9734    7309   280051    38.3 | 10.289 % |
c |     78868 |   19942    67531 |   10708    7813   298870    38.3 | 10.339 % |
c |     79627 |   19942    67531 |   11779    8572   342608    40.0 | 10.339 % |
c |     80766 |   19942    67531 |   12957    9711   439104    45.2 | 10.339 % |
c |     82475 |   19936    67513 |   14252   11419   560031    49.0 | 10.364 % |
c |     85038 |   19936    67513 |   15677   13982   704208    50.4 | 10.364 % |
c |     88882 |   19924    67486 |   17245    9494   573325    60.4 | 10.438 % |
c |     94648 |   19924    67486 |   18970   15260   955968    62.6 | 10.438 % |
c |    103297 |   19916    67460 |   20867   13789   713329    51.7 | 10.463 % |
c |    116272 |   19910    67442 |   22954   15743   751219    47.7 | 10.487 % |
c ==============================================================================
c [1mFound solution: 2522112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127359 |   19922    67471 |    6640   14702   794493    54.0 | 10.487 % |
c |    127459 |   19922    67471 |    7304    3776   127552    33.8 | 10.494 % |
c |    127609 |   19922    67471 |    8034    3926   129716    33.0 | 10.494 % |
c |    127835 |   19922    67471 |    8837    4152   156130    37.6 | 10.494 % |
c |    128172 |   19912    67449 |    9721    4485   164235    36.6 | 10.568 % |
c |    128679 |   19912    67449 |   10693    4992   183225    36.7 | 10.568 % |
c |    129440 |   19912    67449 |   11763    5753   205051    35.6 | 10.568 % |
c |    130579 |   19912    67449 |   12939    6892   257149    37.3 | 10.568 % |
c |    132287 |   19912    67449 |   14233    8600   340347    39.6 | 10.568 % |
c |    134854 |   19912    67449 |   15656   11167   490010    43.9 | 10.568 % |
c |    138701 |   19912    67449 |   17222   15014   707463    47.1 | 10.568 % |
c |    144468 |   19912    67449 |   18944   11874   493715    41.6 | 10.568 % |
c ==============================================================================
c [1mFound solution: 2021376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149824 |   19918    67463 |    6639   17230   725431    42.1 | 10.568 % |
c |    149924 |   19918    67463 |    7302    4408   152704    34.6 | 10.582 % |
c |    150074 |   19918    67463 |    8033    4558   155333    34.1 | 10.582 % |
c |    150302 |   19918    67463 |    8836    4786   165404    34.6 | 10.582 % |
c |    150640 |   19918    67463 |    9720    5124   180854    35.3 | 10.582 % |
c |    151147 |   19904    67426 |   10692    5627   198519    35.3 | 10.681 % |
c |    151906 |   19904    67426 |   11761    6386   231775    36.3 | 10.681 % |
c |    153045 |   19904    67426 |   12937    7525   270866    36.0 | 10.681 % |
c |    154753 |   19904    67426 |   14231    9233   344640    37.3 | 10.681 % |
c |    157316 |   19904    67426 |   15654   11796   468997    39.8 | 10.681 % |
c |    161161 |   19904    67426 |   17219   15641   682108    43.6 | 10.681 % |
c |    166928 |   19904    67426 |   18941   12371   584652    47.3 | 10.681 % |
c |    175577 |   19904    67426 |   20836   10965   555413    50.7 | 10.681 % |
c |    188551 |   19904    67426 |   22919   13084   624549    47.7 | 10.681 % |
c |    208015 |   19895    67399 |   25211   20521  1335297    65.1 | 10.730 % |
c |    237207 |   19895    67399 |   27732   23675  1338137    56.5 | 10.730 % |
c |    280999 |   19868    67339 |   30506   22421  1362077    60.8 | 10.927 % |
c ==============================================================================
c [1mFound solution: 1964032[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    337469 |   19877    67361 |    6625   27521  1615060    58.7 | 10.927 % |
c |    337571 |   19877    67361 |    7287    6983   298754    42.8 | 10.941 % |
c |    337722 |   19877    67361 |    8016    7134   304165    42.6 | 10.941 % |
c |    337948 |   19877    67361 |    8817    7360   309684    42.1 | 10.941 % |
c ==============================================================================
c [1mFound solution: 818176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    338139 |   19831    67198 |    6610    7544   315949    41.9 | 10.941 % |
c |    338239 |   19831    67198 |    7271    3872   117087    30.2 | 11.128 % |
c |    338389 |   19809    67148 |    7998    4020   118738    29.5 | 11.275 % |
c |    338614 |   19809    67148 |    8797    4245   122647    28.9 | 11.275 % |
c |    338952 |   19809    67148 |    9677    4583   134194    29.3 | 11.275 % |
c |    339458 |   19809    67148 |   10645    5089   150331    29.5 | 11.275 % |
c |    340217 |   19809    67148 |   11710    5848   169574    29.0 | 11.275 % |
c |    341356 |   19809    67148 |   12881    6987   201444    28.8 | 11.275 % |
c |    343064 |   19809    67148 |   14169    8695   267895    30.8 | 11.275 % |
c |    345627 |   19781    67084 |   15586   11254   356949    31.7 | 11.497 % |
c |    349471 |   19757    67031 |   17144   15086   500268    33.2 | 11.694 % |
c |    355239 |   19713    66930 |   18859   11909   399091    33.5 | 12.063 % |
c |    363889 |   19713    66930 |   20745   10449   365385    35.0 | 12.063 % |
c |    376863 |   19661    66810 |   22819   12706   515813    40.6 | 12.506 % |
c |    396324 |   19661    66810 |   25101   20102  1154823    57.4 | 12.506 % |
c ==============================================================================
c [1mFound solution: 790528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    397868 |   19664    66818 |    6554   21646  1262196    58.3 | 12.506 % |
c |    397968 |   19647    66780 |    7209    5511   243966    44.3 | 12.645 % |
c |    398119 |   19647    66780 |    7930    5662   245316    43.3 | 12.645 % |
c |    398345 |   19647    66780 |    8723    5888   250643    42.6 | 12.645 % |
c |    398684 |   19647    66780 |    9595    6227   258778    41.6 | 12.645 % |
c |    399190 |   19647    66780 |   10555    6733   276773    41.1 | 12.645 % |
c |    399949 |   19647    66780 |   11610    7492   299025    39.9 | 12.645 % |
c |    401089 |   19647    66780 |   12771    8632   333558    38.6 | 12.645 % |
c |    402797 |   19647    66780 |   14049   10340   410168    39.7 | 12.645 % |
c |    405360 |   19647    66780 |   15453   12903   533783    41.4 | 12.645 % |
c |    409205 |   19647    66780 |   16999    8408   351582    41.8 | 12.645 % |
c |    414971 |   19612    66701 |   18699   14170   623685    44.0 | 12.891 % |
c |    423622 |   19612    66701 |   20569   12588   579955    46.1 | 12.891 % |
c |    436596 |   19612    66701 |   22626   14760   726082    49.2 | 12.891 % |
c |    456060 |   19612    66701 |   24888   22396  1079856    48.2 | 12.891 % |
c |    485253 |   19592    66654 |   27377   25538  1323214    51.8 | 13.087 % |
c |    529042 |   19574    66614 |   30115   24738  1096257    44.3 | 13.235 % |
c ==============================================================================
c [1mFound solution: 580608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    530944 |   19580    66629 |    6526   26640  1206714    45.3 | 13.235 % |
c |    531044 |   19580    66629 |    7178    6606   240336    36.4 | 13.250 % |
c |    531196 |   19580    66629 |    7896    6758   243751    36.1 | 13.250 % |
c |    531421 |   19580    66629 |    8686    6983   247742    35.5 | 13.250 % |
c |    531758 |   19580    66629 |    9554    7320   256616    35.1 | 13.250 % |
c |    532264 |   19580    66629 |   10510    7826   269328    34.4 | 13.250 % |
c |    533026 |   19580    66629 |   11561    8588   288887    33.6 | 13.250 % |
c |    534165 |   19580    66629 |   12717    9727   322283    33.1 | 13.250 % |
c |    535877 |   19580    66629 |   13989   11439   383971    33.6 | 13.250 % |
c |    538439 |   19580    66629 |   15387   14001   485193    34.7 | 13.250 % |
c |    542284 |   19580    66629 |   16926    9703   309759    31.9 | 13.250 % |
c |    548052 |   19580    66629 |   18619   15471   577157    37.3 | 13.250 % |
c |    556702 |   19580    66629 |   20481   14388   611959    42.5 | 13.250 % |
c |    569677 |   19580    66629 |   22529   16607   882005    53.1 | 13.250 % |
c |    589138 |   19580    66629 |   24782   12766   455111    35.7 | 13.250 % |
c |    618332 |   19568    66602 |   27260   15694   694024    44.2 | 13.348 % |
c |    662121 |   19568    66602 |   29986   16216   706500    43.6 | 13.348 % |
c |    727805 |   19514    66480 |   32985   14865   654057    44.0 | 13.766 % |
c ==============================================================================
c [1mFound solution: 550912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    758120 |   19515    66482 |    6505   24867  1269806    51.1 | 13.766 % |
c |    758220 |   19515    66482 |    7155    6317   262163    41.5 | 13.808 % |
c |    758371 |   19515    66482 |    7871    6468   265260    41.0 | 13.808 % |
c |    758596 |   19515    66482 |    8658    6693   272564    40.7 | 13.808 % |
c |    758933 |   19515    66482 |    9523    7030   281856    40.1 | 13.808 % |
c |    759439 |   19501    66449 |   10476    7534   293604    39.0 | 13.931 % |
c |    760198 |   19501    66449 |   11524    8293   317919    38.3 | 13.931 % |
c |    761337 |   19501    66449 |   12676    9432   355218    37.7 | 13.931 % |
c |    763045 |   19501    66449 |   13944   11140   405332    36.4 | 13.931 % |
c |    765608 |   19501    66449 |   15338   13703   537756    39.2 | 13.931 % |
c |    769453 |   19501    66449 |   16872    9424   333768    35.4 | 13.931 % |
c |    775219 |   19501    66449 |   18559   15190   597919    39.4 | 13.931 % |
c |    783868 |   19501    66449 |   20415   14112   581917    41.2 | 13.931 % |
#### 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.74 0.94 0.92 2/54 22132
Raw data (stat): 22132 (runsolver) R 22131 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549695299 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.78 0.94 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 1298 0 0 0 993 3 0 0 25 0 1 0 549695299 6967296 1276 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1701 1276 603 41 0 1660 0
vsize: 6804
[startup+20.0204 s]
Raw data (loadavg): 0.81 0.94 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 1771 0 0 0 1993 5 0 0 25 0 1 0 549695299 8843264 1749 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2159 1749 603 41 0 2118 0
vsize: 8636
[startup+30.04 s]
Raw data (loadavg): 0.84 0.94 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 2206 0 0 0 2993 6 0 0 25 0 1 0 549695299 10567680 2184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2580 2184 603 41 0 2539 0
vsize: 10320
[startup+40.0401 s]
Raw data (loadavg): 0.87 0.94 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 2574 0 0 0 3991 8 0 0 25 0 1 0 549695299 12161024 2552 4294967295 134512640 134672761 3221224624 3221223808 134558671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2969 2552 603 41 0 2928 0
vsize: 11876
[startup+50.0401 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 2721 0 0 0 4991 9 0 0 25 0 1 0 549695299 12791808 2699 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3123 2699 603 41 0 3082 0
vsize: 12492
[startup+60.0405 s]
Raw data (loadavg): 0.90 0.94 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 2721 0 0 0 5991 9 0 0 25 0 1 0 549695299 12791808 2699 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3123 2699 603 41 0 3082 0
vsize: 12492
[startup+70.0402 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 2732 0 0 0 6991 9 0 0 25 0 1 0 549695299 12791808 2710 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3123 2710 603 41 0 3082 0
vsize: 12492
[startup+80.0402 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3105 0 0 0 7990 10 0 0 25 0 1 0 549695299 14385152 3083 4294967295 134512640 134672761 3221224624 3221223808 134559422 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3083 603 41 0 3471 0
vsize: 14048
[startup+90.0409 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 8990 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+100.04 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 9990 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223808 134559327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+110.041 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 10991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+120.042 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 11991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+130.041 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 12991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+140.041 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 13991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+150.042 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 14991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+160.042 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 15991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+170.042 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 16991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+180.042 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 17991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+190.043 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 18992 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+200.042 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 19992 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223808 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+210.042 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 20992 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+220.043 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3128 0 0 0 21991 10 0 0 25 0 1 0 549695299 14385152 3106 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3106 603 41 0 3471 0
vsize: 14048
[startup+230.042 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3129 0 0 0 22991 10 0 0 25 0 1 0 549695299 14385152 3107 4294967295 134512640 134672761 3221224624 3221223800 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3107 603 41 0 3471 0
vsize: 14048
[startup+240.042 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3129 0 0 0 23992 10 0 0 25 0 1 0 549695299 14385152 3107 4294967295 134512640 134672761 3221224624 3221223808 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3107 603 41 0 3471 0
vsize: 14048
[startup+250.042 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 24992 10 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+260.042 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 25992 10 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+270.042 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 26992 10 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+280.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 27992 10 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+290.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 28992 10 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+300.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 29993 10 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+310.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 30993 10 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+320.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 31992 11 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+330.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 32992 11 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+340.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 33993 11 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+350.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3131 0 0 0 34993 11 0 0 25 0 1 0 549695299 14385152 3109 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3109 603 41 0 3471 0
vsize: 14048
[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3133 0 0 0 35993 11 0 0 25 0 1 0 549695299 14385152 3111 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3111 603 41 0 3471 0
vsize: 14048
[startup+370.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3133 0 0 0 36993 11 0 0 25 0 1 0 549695299 14385152 3111 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3111 603 41 0 3471 0
vsize: 14048
[startup+380.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3133 0 0 0 37993 12 0 0 25 0 1 0 549695299 14385152 3111 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3111 603 41 0 3471 0
vsize: 14048
[startup+390.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3133 0 0 0 38993 12 0 0 25 0 1 0 549695299 14385152 3111 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3111 603 41 0 3471 0
vsize: 14048
[startup+400.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3136 0 0 0 39993 12 0 0 25 0 1 0 549695299 14385152 3114 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3114 603 41 0 3471 0
vsize: 14048
[startup+410.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3268 0 0 0 40993 12 0 0 25 0 1 0 549695299 15052800 3246 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3675 3246 603 41 0 3634 0
vsize: 14700
[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3287 0 0 0 41993 12 0 0 25 0 1 0 549695299 15052800 3265 4294967295 134512640 134672761 3221224624 3221223776 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3675 3265 603 41 0 3634 0
vsize: 14700
[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3287 0 0 0 42993 12 0 0 25 0 1 0 549695299 15052800 3265 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3675 3265 603 41 0 3634 0
vsize: 14700
[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3287 0 0 0 43993 12 0 0 25 0 1 0 549695299 15052800 3265 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3675 3265 603 41 0 3634 0
vsize: 14700
[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3287 0 0 0 44993 12 0 0 25 0 1 0 549695299 15052800 3265 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3675 3265 603 41 0 3634 0
vsize: 14700
[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3287 0 0 0 45994 12 0 0 25 0 1 0 549695299 15052800 3265 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3675 3265 603 41 0 3634 0
vsize: 14700
[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3289 0 0 0 46994 12 0 0 25 0 1 0 549695299 15052800 3267 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3675 3267 603 41 0 3634 0
vsize: 14700
[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3483 0 0 0 47993 13 0 0 25 0 1 0 549695299 15863808 3461 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3461 603 41 0 3832 0
vsize: 15492
[startup+490.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3487 0 0 0 48993 13 0 0 25 0 1 0 549695299 15863808 3465 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3465 603 41 0 3832 0
vsize: 15492
[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3497 0 0 0 49993 13 0 0 25 0 1 0 549695299 15863808 3475 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3475 603 41 0 3832 0
vsize: 15492
[startup+510.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3497 0 0 0 50994 13 0 0 25 0 1 0 549695299 15863808 3475 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3475 603 41 0 3832 0
vsize: 15492
[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3497 0 0 0 51994 13 0 0 25 0 1 0 549695299 15863808 3475 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3873 3475 603 41 0 3832 0
vsize: 15492
[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3518 0 0 0 52994 13 0 0 25 0 1 0 549695299 15994880 3496 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3905 3496 603 41 0 3864 0
vsize: 15620
[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3530 0 0 0 53994 13 0 0 25 0 1 0 549695299 16130048 3508 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3508 603 41 0 3897 0
vsize: 15752
[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 54994 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 55994 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 56994 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+580.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 57995 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 58995 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+600.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 59995 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 60995 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+620.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 61995 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+630.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 62995 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+640.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 63996 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+650.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 64996 13 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+660.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 65996 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+670.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 66996 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 67996 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+690.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 68996 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 69996 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+710.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 70997 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+720.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 71997 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+730.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 72997 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+740.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 73997 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+750.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3538 0 0 0 74997 14 0 0 25 0 1 0 549695299 16130048 3516 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3516 603 41 0 3897 0
vsize: 15752
[startup+760.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3562 0 0 0 75997 14 0 0 25 0 1 0 549695299 16130048 3540 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3938 3540 603 41 0 3897 0
vsize: 15752
[startup+770.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3563 0 0 0 76998 14 0 0 25 0 1 0 549695299 16265216 3541 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3971 3541 603 41 0 3930 0
vsize: 15884
[startup+780.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3633 0 0 0 77998 14 0 0 25 0 1 0 549695299 16531456 3611 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4036 3611 603 41 0 3995 0
vsize: 16144
[startup+790.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3633 0 0 0 78998 14 0 0 25 0 1 0 549695299 16531456 3611 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4036 3611 603 41 0 3995 0
vsize: 16144
[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3633 0 0 0 79998 14 0 0 25 0 1 0 549695299 16531456 3611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4036 3611 603 41 0 3995 0
vsize: 16144
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 80998 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 81998 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 82998 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 83999 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 84998 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 85999 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+870.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 86999 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 87999 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+890.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 88999 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+900.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 89999 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+910.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 90999 14 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+920.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 91999 15 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 92999 15 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 93999 15 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+950.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 94999 15 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+960.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3679 0 0 0 96000 15 0 0 25 0 1 0 549695299 16662528 3657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3657 603 41 0 4027 0
vsize: 16272
[startup+970.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3680 0 0 0 97000 15 0 0 25 0 1 0 549695299 16662528 3658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3658 603 41 0 4027 0
vsize: 16272
[startup+980.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3680 0 0 0 98000 15 0 0 25 0 1 0 549695299 16662528 3658 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3658 603 41 0 4027 0
vsize: 16272
[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3680 0 0 0 99000 15 0 0 25 0 1 0 549695299 16662528 3658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3658 603 41 0 4027 0
vsize: 16272
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3680 0 0 0 100000 16 0 0 25 0 1 0 549695299 16662528 3658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3658 603 41 0 4027 0
vsize: 16272
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3680 0 0 0 101000 16 0 0 25 0 1 0 549695299 16662528 3658 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4068 3658 603 41 0 4027 0
vsize: 16272
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3696 0 0 0 102000 16 0 0 25 0 1 0 549695299 16797696 3674 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4101 3674 603 41 0 4060 0
vsize: 16404
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3731 0 0 0 103000 16 0 0 25 0 1 0 549695299 16932864 3709 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4134 3709 603 41 0 4093 0
vsize: 16536
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3731 0 0 0 104001 16 0 0 25 0 1 0 549695299 16932864 3709 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4134 3709 603 41 0 4093 0
vsize: 16536
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3995 0 0 0 105000 17 0 0 25 0 1 0 549695299 17997824 3973 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4394 3973 603 41 0 4353 0
vsize: 17576
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3995 0 0 0 106000 17 0 0 25 0 1 0 549695299 17997824 3973 4294967295 134512640 134672761 3221224624 3221223760 134565121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4394 3973 603 41 0 4353 0
vsize: 17576
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 3998 0 0 0 107000 17 0 0 25 0 1 0 549695299 17997824 3976 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4394 3976 603 41 0 4353 0
vsize: 17576
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4139 0 0 0 108000 17 0 0 25 0 1 0 549695299 18530304 4117 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4524 4117 603 41 0 4483 0
vsize: 18096
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4267 0 0 0 109000 18 0 0 25 0 1 0 549695299 19058688 4245 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4653 4245 603 41 0 4612 0
vsize: 18612
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4267 0 0 0 110000 18 0 0 25 0 1 0 549695299 19058688 4245 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4653 4245 603 41 0 4612 0
vsize: 18612
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4267 0 0 0 111000 18 0 0 25 0 1 0 549695299 19058688 4245 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4653 4245 603 41 0 4612 0
vsize: 18612
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4267 0 0 0 112000 18 0 0 25 0 1 0 549695299 19058688 4245 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4653 4245 603 41 0 4612 0
vsize: 18612
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4267 0 0 0 113000 18 0 0 25 0 1 0 549695299 19058688 4245 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4653 4245 603 41 0 4612 0
vsize: 18612
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4267 0 0 0 114000 18 0 0 25 0 1 0 549695299 19058688 4245 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4653 4245 603 41 0 4612 0
vsize: 18612
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4301 0 0 0 115000 18 0 0 25 0 1 0 549695299 19320832 4279 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4279 603 41 0 4676 0
vsize: 18868
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4301 0 0 0 116001 18 0 0 25 0 1 0 549695299 19320832 4279 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4279 603 41 0 4676 0
vsize: 18868
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4301 0 0 0 117001 18 0 0 25 0 1 0 549695299 19320832 4279 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4279 603 41 0 4676 0
vsize: 18868
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4301 0 0 0 118001 18 0 0 25 0 1 0 549695299 19320832 4279 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4279 603 41 0 4676 0
vsize: 18868
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4301 0 0 0 119001 18 0 0 25 0 1 0 549695299 19320832 4279 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4279 603 41 0 4676 0
vsize: 18868
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22132
Raw data (stat): 22132 (minisat+) R 22131 28546 28545 0 -1 0 4301 0 0 0 120001 18 0 0 25 0 1 0 549695299 19320832 4279 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4279 603 41 0 4676 0
vsize: 18868
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 22132
Raw data (stat): 22132 (minisat+) Z 22131 28546 28545 0 -1 12 4304 0 0 0 120001 19 0 0 25 0 1 0 549695299 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1200.01
CPU system time (s): 0.197969
CPU usage (%): 100.013
Max. virtual memory (Kb): 18868
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####