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 16747

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        489620 kB
Buffers:           808 kB
Cached:         518712 kB
SwapCached:          0 kB
Active:          18340 kB
Inactive:       504324 kB
HighTotal:      131008 kB
HighFree:        18788 kB
LowTotal:       903652 kB
LowFree:        470832 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            16548 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 08:43:25 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 12659 7 1200.23 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]---> Adder-cost: 132   maxlim: 4632   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       170 |   18089    64333 |    6029     169      862     5.1 | 12.761 % |
c |       270 |   18089    64333 |    6631     269     1662     6.2 | 12.359 % |
c |       420 |   18089    64333 |    7295     419     3064     7.3 | 12.359 % |
c ==============================================================================
c [1mFound solution: 9165824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5378   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       424 |   18103    64412 |    6034     423     3089     7.3 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8893440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5644   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       505 |   18103    64446 |    6034     503     8679    17.3 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8585216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5945   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       521 |   18112    64516 |    6037     519     9447    18.2 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8474624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6053   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       545 |   18120    64577 |    6040     543    11107    20.5 | 12.359 % |
c ==============================================================================
c [1mFound solution: 8449024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6078   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       592 |   18127    64646 |    6042     590    15887    26.9 | 12.359 % |
c |       692 |   18127    64646 |    6646     690    27246    39.5 | 12.999 % |
c ==============================================================================
c [1mFound solution: 8186880[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6334   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       768 |   18143    64748 |    6047     766    36704    47.9 | 12.999 % |
c ==============================================================================
c [1mFound solution: 6665216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7820   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       770 |   18152    64813 |    6050     768    36712    47.8 | 12.999 % |
c ==============================================================================
c [1mFound solution: 6627328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7857   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       773 |   18158    64851 |    6052     771    36893    47.9 | 12.999 % |
c ==============================================================================
c [1mFound solution: 6550528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7932   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       786 |   18171    64943 |    6057     784    37273    47.5 | 12.999 % |
c |       887 |   18171    64943 |    6662     885    47503    53.7 | 13.569 % |
c |      1037 |   18171    64943 |    7328    1035    61402    59.3 | 13.569 % |
c |      1263 |   18171    64943 |    8061    1261    84278    66.8 | 13.569 % |
c |      1603 |   18171    64943 |    8868    1601   136610    85.3 | 13.569 % |
c ==============================================================================
c [1mFound solution: 6333440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8144   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1667 |   18179    64999 |    6059    1665   137841    82.8 | 13.569 % |
c ==============================================================================
c [1mFound solution: 6005760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8464   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1759 |   18129    64485 |    6043    1757   141693    80.6 | 13.569 % |
c |      1859 |   18129    64485 |    6647    1857   145772    78.5 | 13.796 % |
c ==============================================================================
c [1mFound solution: 5316608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9137   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1929 |   18140    64541 |    6046    1927   153114    79.5 | 13.796 % |
c |      2029 |   18140    64541 |    6650    2027   165895    81.8 | 13.937 % |
c |      2179 |   18140    64541 |    7315    2177   182794    84.0 | 13.937 % |
c |      2404 |   18132    64515 |    8047    2401   203350    84.7 | 13.968 % |
c |      2741 |   18132    64515 |    8851    2738   229940    84.0 | 13.968 % |
c ==============================================================================
c [1mFound solution: 4519936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9915   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2958 |   18137    64547 |    6045    2954   245650    83.2 | 13.968 % |
c |      3059 |   18137    64547 |    6649    3055   251248    82.2 | 14.161 % |
c |      3209 |   18137    64547 |    7314    3205   267630    83.5 | 14.161 % |
c |      3435 |   18137    64547 |    8045    3431   294515    85.8 | 14.161 % |
c |      3775 |   18137    64547 |    8850    3771   332410    88.1 | 14.161 % |
c |      4281 |   18137    64547 |    9735    4277   389277    91.0 | 14.161 % |
c |      5040 |   18137    64547 |   10709    5036   475777    94.5 | 14.161 % |
c |      6179 |   18129    64521 |   11779    6174   614893    99.6 | 14.192 % |
c |      7888 |   18121    64495 |   12957    7882   799962   101.5 | 14.223 % |
c |     10450 |   18113    64469 |   14253   10443  1027905    98.4 | 14.255 % |
c |     14294 |   18113    64469 |   15679   14287  1327207    92.9 | 14.255 % |
c ==============================================================================
c [1mFound solution: 4205568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10222   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18031 |   18128    64560 |    6042    9476   707727    74.7 | 14.255 % |
c |     18135 |   18128    64560 |    6646    4842   330421    68.2 | 14.437 % |
c |     18286 |   18128    64560 |    7310    4993   346139    69.3 | 14.437 % |
c |     18512 |   18128    64560 |    8041    5219   363036    69.6 | 14.437 % |
c |     18850 |   18128    64560 |    8846    5557   391760    70.5 | 14.437 % |
c |     19358 |   18128    64560 |    9730    6065   429329    70.8 | 14.437 % |
c |     20117 |   18128    64560 |   10703    6824   501738    73.5 | 14.437 % |
c |     21257 |   18128    64560 |   11774    7964   631096    79.2 | 14.437 % |
c ==============================================================================
c [1mFound solution: 4191232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10236   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22852 |   18128    64584 |    6042    9558   839302    87.8 | 14.437 % |
c ==============================================================================
c [1mFound solution: 3969024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10453   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22951 |   18132    64627 |    6044    4877   436723    89.5 | 14.437 % |
c |     23051 |   18132    64627 |    6648    4977   446395    89.7 | 14.727 % |
c |     23201 |   18132    64627 |    7313    5127   463974    90.5 | 14.727 % |
c |     23426 |   18132    64627 |    8044    5352   488628    91.3 | 14.727 % |
c |     23764 |   18132    64627 |    8849    5690   527568    92.7 | 14.727 % |
c |     24271 |   18107    64544 |    9733    6194   608379    98.2 | 14.819 % |
c |     25030 |   18093    64500 |   10707    6951   683416    98.3 | 14.881 % |
c |     26171 |   18093    64500 |   11778    8092   804242    99.4 | 14.881 % |
c |     27880 |   18093    64500 |   12955    9801   952250    97.2 | 14.881 % |
c |     30442 |   18093    64500 |   14251   12363  1198119    96.9 | 14.881 % |
c |     34287 |   18077    64448 |   15676    8299   742579    89.5 | 14.943 % |
c |     40053 |   18077    64448 |   17244   14065  1280515    91.0 | 14.943 % |
c |     48702 |   18077    64448 |   18968   13371  1140331    85.3 | 14.943 % |
c |     61677 |   18069    64422 |   20865   16116  1649597   102.4 | 14.974 % |
c |     81140 |   18069    64422 |   22952   13399   899255    67.1 | 14.974 % |
c ==============================================================================
c [1mFound solution: 3134464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11268   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82211 |   18074    64456 |    6024   14470  1003543    69.4 | 14.974 % |
c |     82312 |   18074    64456 |    6626    3719   180113    48.4 | 15.043 % |
c |     82463 |   18074    64456 |    7289    3870   182902    47.3 | 15.043 % |
c |     82689 |   18074    64456 |    8017    4096   195175    47.7 | 15.043 % |
c |     83026 |   18074    64456 |    8819    4433   232223    52.4 | 15.043 % |
c |     83533 |   18066    64430 |    9701    4939   261484    52.9 | 15.074 % |
c |     84293 |   18066    64430 |   10671    5699   315475    55.4 | 15.074 % |
c |     85433 |   18066    64430 |   11739    6839   408332    59.7 | 15.074 % |
c |     87141 |   18058    64404 |   12912    8546   505534    59.2 | 15.105 % |
c ==============================================================================
c [1mFound solution: 3055616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11345   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87258 |   18063    64438 |    6021    8663   506965    58.5 | 15.105 % |
c |     87358 |   18063    64438 |    6623    4432   199222    45.0 | 15.174 % |
c |     87508 |   18063    64438 |    7285    4582   202942    44.3 | 15.174 % |
c |     87733 |   18063    64438 |    8013    4807   220980    46.0 | 15.174 % |
c |     88070 |   18063    64438 |    8815    5144   231440    45.0 | 15.174 % |
c |     88576 |   18063    64438 |    9696    5650   251621    44.5 | 15.174 % |
c |     89336 |   18063    64438 |   10666    6410   304672    47.5 | 15.174 % |
c |     90475 |   18063    64438 |   11733    7549   440866    58.4 | 15.174 % |
c ==============================================================================
c [1mFound solution: 2900992[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11496   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90775 |   18073    64494 |    6024    7849   449484    57.3 | 15.174 % |
c ==============================================================================
c [1mFound solution: 2862080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11534   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90869 |   18083    64552 |    6027    4019   218812    54.4 | 15.174 % |
c ==============================================================================
c [1mFound solution: 2467840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11919   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90902 |   18089    64578 |    6029    4052   220365    54.4 | 15.174 % |
c |     91002 |   18089    64578 |    6631    4152   222408    53.6 | 15.450 % |
c |     91153 |   18089    64578 |    7295    4303   224818    52.2 | 15.450 % |
c |     91379 |   18081    64552 |    8024    4528   237701    52.5 | 15.481 % |
c |     91718 |   18081    64552 |    8827    4867   268324    55.1 | 15.481 % |
c |     92224 |   18081    64552 |    9709    5373   338705    63.0 | 15.481 % |
c |     92983 |   18081    64552 |   10680    6132   365305    59.6 | 15.481 % |
c |     94122 |   18081    64552 |   11748    7271   496447    68.3 | 15.481 % |
c |     95830 |   18081    64552 |   12923    8979   588261    65.5 | 15.481 % |
c |     98392 |   18081    64552 |   14216   11541   868525    75.3 | 15.481 % |
c ==============================================================================
c [1mFound solution: 2396160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11989   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100976 |   18089    64599 |    6029   14125   984272    69.7 | 15.481 % |
c |    101077 |   18089    64599 |    6631    3633   110800    30.5 | 15.565 % |
c |    101230 |   18089    64599 |    7295    3786   119102    31.5 | 15.565 % |
c |    101455 |   18083    64579 |    8024    4010   141048    35.2 | 15.596 % |
c |    101792 |   18083    64579 |    8827    4347   148021    34.1 | 15.596 % |
c |    102298 |   18083    64579 |    9709    4853   171678    35.4 | 15.596 % |
c ==============================================================================
c [1mFound solution: 2342912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12041   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102499 |   18089    64611 |    6029    5054   182823    36.2 | 15.596 % |
c |    102599 |   18089    64611 |    6631    5154   191623    37.2 | 15.658 % |
c |    102750 |   18089    64611 |    7295    5305   201586    38.0 | 15.658 % |
c |    102976 |   18089    64611 |    8024    5531   212618    38.4 | 15.658 % |
c |    103313 |   18089    64611 |    8827    5868   230337    39.3 | 15.658 % |
c |    103819 |   18089    64611 |    9709    6374   273398    42.9 | 15.658 % |
c |    104579 |   18089    64611 |   10680    7134   351701    49.3 | 15.658 % |
c |    105719 |   18089    64611 |   11748    8274   470020    56.8 | 15.658 % |
c |    107428 |   18089    64611 |   12923    9983   608905    61.0 | 15.658 % |
c |    109990 |   18089    64611 |   14216   12545   914049    72.9 | 15.658 % |
c ==============================================================================
c [1mFound solution: 2283520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12099   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111605 |   18092    64632 |    6030   14160   986206    69.6 | 15.658 % |
c ==============================================================================
c [1mFound solution: 2247680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12134   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111651 |   18099    64684 |    6033    3586   126357    35.2 | 15.658 % |
c |    111752 |   18099    64684 |    6636    3687   128317    34.8 | 15.793 % |
c |    111902 |   18099    64684 |    7299    3837   129649    33.8 | 15.793 % |
c ==============================================================================
c [1mFound solution: 2119680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 12259   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111915 |   18107    64720 |    6035    3850   129743    33.7 | 15.793 % |
c |    112015 |   18107    64720 |    6638    3950   144109    36.5 | 15.875 % |
c |    112165 |   18107    64720 |    7302    4100   155401    37.9 | 15.875 % |
c |    112390 |   18107    64720 |    8032    4325   162996    37.7 | 15.875 % |
c |    112727 |   18107    64720 |    8835    4662   189457    40.6 | 15.875 % |
c |    113233 |   18107    64720 |    9719    5168   223351    43.2 | 15.875 % |
c |    113993 |   18107    64720 |   10691    5928   274773    46.4 | 15.875 % |
c |    115132 |   18107    64720 |   11760    7067   336663    47.6 | 15.875 % |
c |    116840 |   18107    64720 |   12936    8775   501739    57.2 | 15.875 % |
c |    119403 |   18107    64720 |   14230   11338   727363    64.2 | 15.875 % |
c |    123251 |   18107    64720 |   15653   15186   964162    63.5 | 15.875 % |
c |    129017 |   18107    64720 |   17218   12522   731878    58.4 | 15.875 % |
c |    137666 |   18101    64702 |   18940   11812   658368    55.7 | 15.906 % |
c |    150642 |   18092    64675 |   20834   14699  1106394    75.3 | 15.966 % |
c |    170105 |   18083    64648 |   22917   11849   629813    53.2 | 16.027 % |
c ==============================================================================
c [1mFound solution: 794624[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 6385   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    170767 |   18028    64457 |    6009   12489   640194    51.3 | 16.027 % |
c |    170869 |   18028    64457 |    6609    6347   254917    40.2 | 16.546 % |
c |    171020 |   18021    64434 |    7270    6497   258243    39.7 | 16.576 % |
c |    171245 |   17945    64175 |    7997    6146   200674    32.7 | 16.968 % |
c |    171582 |   17945    64175 |    8797    6483   204951    31.6 | 16.968 % |
c |    172088 |   17837    63514 |    9677    6985   214331    30.7 | 17.298 % |
c |    172850 |   17837    63514 |   10645    7747   254029    32.8 | 17.298 % |
c |    173990 |   17837    63514 |   11709    8887   308313    34.7 | 17.298 % |
c |    175699 |   17837    63514 |   12880   10596   367154    34.7 | 17.298 % |
c |    178261 |   17837    63514 |   14168   13158   489550    37.2 | 17.298 % |
c |    182107 |   17837    63514 |   15585    9196   331647    36.1 | 17.298 % |
c |    187873 |   17837    63514 |   17144   14962   596932    39.9 | 17.298 % |
c |    196523 |   17837    63514 |   18858   14503   674566    46.5 | 17.298 % |
c |    209498 |   17837    63514 |   20744   17603   718960    40.8 | 17.298 % |
c |    228959 |   17837    63514 |   22819   15439   827104    53.6 | 17.298 % |
c |    258152 |   17837    63514 |   25101   20843  1033958    49.6 | 17.298 % |
c |    301941 |   17837    63514 |   27611   25464  1404457    55.2 | 17.298 % |
c |    367627 |   17837    63514 |   30372   19056   831599    43.6 | 17.298 % |
c |    466153 |   17829    63488 |   33409   17635   800117    45.4 | 17.329 % |
c |    613943 |   17820    63461 |   36750   30799  1466980    47.6 | 17.389 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.69 0.88 0.89 2/56 25440
Raw data (stat): 25440 (runsolver) R 25439 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 428534134 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+10.0003 s]
Raw data (loadavg): 0.74 0.88 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 1223 0 0 0 995 3 0 0 25 0 1 0 428534134 6594560 1201 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1610 1201 603 41 0 1569 0
vsize: 6440
[startup+20.0011 s]
Raw data (loadavg): 0.78 0.89 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 1707 0 0 0 1993 5 0 0 25 0 1 0 428534134 8609792 1685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2102 1685 603 41 0 2061 0
vsize: 8408
[startup+30.0009 s]
Raw data (loadavg): 0.81 0.89 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2069 0 0 0 2992 7 0 0 25 0 1 0 428534134 10072064 2047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2459 2047 603 41 0 2418 0
vsize: 9836
[startup+40.0022 s]
Raw data (loadavg): 0.84 0.89 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2365 0 0 0 3991 8 0 0 25 0 1 0 428534134 11268096 2343 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2343 603 41 0 2710 0
vsize: 11004
[startup+50.0025 s]
Raw data (loadavg): 0.86 0.90 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2499 0 0 0 4991 8 0 0 25 0 1 0 428534134 11988992 2477 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2477 603 41 0 2886 0
vsize: 11708
[startup+60.0023 s]
Raw data (loadavg): 0.88 0.90 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2502 0 0 0 5991 8 0 0 25 0 1 0 428534134 11988992 2480 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2480 603 41 0 2886 0
vsize: 11708
[startup+70.0031 s]
Raw data (loadavg): 0.90 0.90 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2502 0 0 0 6991 9 0 0 25 0 1 0 428534134 11988992 2480 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2480 603 41 0 2886 0
vsize: 11708
[startup+80.0039 s]
Raw data (loadavg): 0.92 0.90 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2502 0 0 0 7991 9 0 0 25 0 1 0 428534134 11988992 2480 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2480 603 41 0 2886 0
vsize: 11708
[startup+90.0047 s]
Raw data (loadavg): 0.93 0.91 0.89 2/56 25440
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2565 0 0 0 8991 9 0 0 25 0 1 0 428534134 12124160 2543 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2960 2543 603 41 0 2919 0
vsize: 11840
[startup+100.005 s]
Raw data (loadavg): 0.94 0.91 0.89 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2565 0 0 0 9991 9 0 0 25 0 1 0 428534134 12124160 2543 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2960 2543 603 41 0 2919 0
vsize: 11840
[startup+110.005 s]
Raw data (loadavg): 0.95 0.91 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2641 0 0 0 10990 10 0 0 25 0 1 0 428534134 12521472 2619 4294967295 134512640 134672761 3221224544 3221223728 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3057 2619 603 41 0 3016 0
vsize: 12228
[startup+120.005 s]
Raw data (loadavg): 0.95 0.91 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2739 0 0 0 11990 10 0 0 25 0 1 0 428534134 12918784 2717 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3154 2717 603 41 0 3113 0
vsize: 12616
[startup+130.005 s]
Raw data (loadavg): 0.96 0.92 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2739 0 0 0 12990 10 0 0 25 0 1 0 428534134 12918784 2717 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3154 2717 603 41 0 3113 0
vsize: 12616
[startup+140.005 s]
Raw data (loadavg): 0.97 0.92 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 2856 0 0 0 13990 10 0 0 25 0 1 0 428534134 13320192 2834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3252 2834 603 41 0 3211 0
vsize: 13008
[startup+150.006 s]
Raw data (loadavg): 0.97 0.92 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3052 0 0 0 14990 11 0 0 25 0 1 0 428534134 14114816 3030 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3030 603 41 0 3405 0
vsize: 13784
[startup+160.006 s]
Raw data (loadavg): 0.98 0.92 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3052 0 0 0 15990 11 0 0 25 0 1 0 428534134 14114816 3030 4294967295 134512640 134672761 3221224544 3221223728 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3030 603 41 0 3405 0
vsize: 13784
[startup+170.007 s]
Raw data (loadavg): 0.98 0.92 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3052 0 0 0 16990 11 0 0 25 0 1 0 428534134 14114816 3030 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3030 603 41 0 3405 0
vsize: 13784
[startup+180.007 s]
Raw data (loadavg): 0.98 0.93 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3206 0 0 0 17990 11 0 0 25 0 1 0 428534134 14782464 3184 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+190.007 s]
Raw data (loadavg): 0.98 0.93 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3206 0 0 0 18991 11 0 0 25 0 1 0 428534134 14782464 3184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+200.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3206 0 0 0 19991 11 0 0 25 0 1 0 428534134 14782464 3184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+210.007 s]
Raw data (loadavg): 0.99 0.93 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3206 0 0 0 20991 11 0 0 25 0 1 0 428534134 14782464 3184 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+220.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3206 0 0 0 21991 11 0 0 25 0 1 0 428534134 14782464 3184 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+230.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3206 0 0 0 22991 11 0 0 25 0 1 0 428534134 14782464 3184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+240.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3206 0 0 0 23991 11 0 0 25 0 1 0 428534134 14782464 3184 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3184 603 41 0 3568 0
vsize: 14436
[startup+250.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3207 0 0 0 24992 11 0 0 25 0 1 0 428534134 14782464 3185 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3185 603 41 0 3568 0
vsize: 14436
[startup+260.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 25992 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+270.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 26992 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+280.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 27992 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+290.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 28992 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+300.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 29992 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+310.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 30992 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+320.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 31993 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+330.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 32993 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+340.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 33993 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+350.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 34993 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+360.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 35993 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+370.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 36993 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+380.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 37993 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+390.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 25442
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 38994 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+400.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 39994 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+410.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 40994 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+420.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 41994 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+430.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 42994 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+440.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3208 0 0 0 43995 11 0 0 25 0 1 0 428534134 14782464 3186 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3186 603 41 0 3568 0
vsize: 14436
[startup+450.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3209 0 0 0 44995 11 0 0 25 0 1 0 428534134 14782464 3187 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3187 603 41 0 3568 0
vsize: 14436
[startup+460.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3209 0 0 0 45995 11 0 0 25 0 1 0 428534134 14782464 3187 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3187 603 41 0 3568 0
vsize: 14436
[startup+470.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3209 0 0 0 46995 11 0 0 25 0 1 0 428534134 14782464 3187 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3187 603 41 0 3568 0
vsize: 14436
[startup+480.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3210 0 0 0 47995 12 0 0 25 0 1 0 428534134 14782464 3188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3188 603 41 0 3568 0
vsize: 14436
[startup+490.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3211 0 0 0 48995 12 0 0 25 0 1 0 428534134 14782464 3189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3189 603 41 0 3568 0
vsize: 14436
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3211 0 0 0 49996 12 0 0 25 0 1 0 428534134 14782464 3189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3189 603 41 0 3568 0
vsize: 14436
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3211 0 0 0 50996 12 0 0 25 0 1 0 428534134 14782464 3189 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3189 603 41 0 3568 0
vsize: 14436
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3212 0 0 0 51996 12 0 0 25 0 1 0 428534134 14782464 3190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3190 603 41 0 3568 0
vsize: 14436
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3212 0 0 0 52996 12 0 0 25 0 1 0 428534134 14782464 3190 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3190 603 41 0 3568 0
vsize: 14436
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3212 0 0 0 53996 12 0 0 25 0 1 0 428534134 14782464 3190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3190 603 41 0 3568 0
vsize: 14436
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3241 0 0 0 54997 12 0 0 25 0 1 0 428534134 14917632 3219 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3219 603 41 0 3601 0
vsize: 14568
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3247 0 0 0 55997 12 0 0 25 0 1 0 428534134 14917632 3225 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3225 603 41 0 3601 0
vsize: 14568
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3250 0 0 0 56997 12 0 0 25 0 1 0 428534134 14917632 3228 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3228 603 41 0 3601 0
vsize: 14568
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3267 0 0 0 57997 12 0 0 25 0 1 0 428534134 15060992 3245 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3245 603 41 0 3636 0
vsize: 14708
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3274 0 0 0 58997 12 0 0 25 0 1 0 428534134 15060992 3252 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3252 603 41 0 3636 0
vsize: 14708
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3282 0 0 0 59997 12 0 0 25 0 1 0 428534134 15060992 3260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3260 603 41 0 3636 0
vsize: 14708
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3289 0 0 0 60998 12 0 0 25 0 1 0 428534134 15060992 3267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3267 603 41 0 3636 0
vsize: 14708
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3289 0 0 0 61998 12 0 0 25 0 1 0 428534134 15060992 3267 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3267 603 41 0 3636 0
vsize: 14708
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3302 0 0 0 62998 12 0 0 25 0 1 0 428534134 15257600 3280 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3280 603 41 0 3684 0
vsize: 14900
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3302 0 0 0 64000 12 0 0 25 0 1 0 428534134 15257600 3280 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3280 603 41 0 3684 0
vsize: 14900
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3302 0 0 0 65000 12 0 0 25 0 1 0 428534134 15257600 3280 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3280 603 41 0 3684 0
vsize: 14900
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3302 0 0 0 66000 12 0 0 25 0 1 0 428534134 15257600 3280 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3280 603 41 0 3684 0
vsize: 14900
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3455 0 0 0 67000 12 0 0 25 0 1 0 428534134 15790080 3433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3433 603 41 0 3814 0
vsize: 15420
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3697 0 0 0 67999 13 0 0 25 0 1 0 428534134 16842752 3675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4112 3675 603 41 0 4071 0
vsize: 16448
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25444
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3710 0 0 0 68999 13 0 0 25 0 1 0 428534134 16842752 3688 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4112 3688 603 41 0 4071 0
vsize: 16448
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3714 0 0 0 69999 13 0 0 25 0 1 0 428534134 16842752 3692 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4112 3692 603 41 0 4071 0
vsize: 16448
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 70999 13 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 71999 13 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 73000 13 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 74000 13 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 75000 13 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 76000 13 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 77000 13 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+780.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3827 0 0 0 78001 14 0 0 25 0 1 0 428534134 17387520 3805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4245 3805 603 41 0 4204 0
vsize: 16980
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3834 0 0 0 79001 14 0 0 25 0 1 0 428534134 17387520 3812 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4245 3812 603 41 0 4204 0
vsize: 16980
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3839 0 0 0 80001 14 0 0 25 0 1 0 428534134 17387520 3817 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4245 3817 603 41 0 4204 0
vsize: 16980
[startup+810.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3839 0 0 0 81001 14 0 0 25 0 1 0 428534134 17387520 3817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4245 3817 603 41 0 4204 0
vsize: 16980
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3846 0 0 0 82001 14 0 0 25 0 1 0 428534134 17387520 3824 4294967295 134512640 134672761 3221224544 3221223636 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4245 3824 603 41 0 4204 0
vsize: 16980
[startup+830.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3854 0 0 0 83001 14 0 0 25 0 1 0 428534134 17530880 3832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4280 3832 603 41 0 4239 0
vsize: 17120
[startup+840.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3854 0 0 0 84001 15 0 0 25 0 1 0 428534134 17530880 3832 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4280 3832 603 41 0 4239 0
vsize: 17120
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3854 0 0 0 85001 15 0 0 25 0 1 0 428534134 17530880 3832 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4280 3832 603 41 0 4239 0
vsize: 17120
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3888 0 0 0 86001 15 0 0 25 0 1 0 428534134 17793024 3866 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3888 0 0 0 87001 15 0 0 25 0 1 0 428534134 17793024 3866 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3888 0 0 0 88001 15 0 0 25 0 1 0 428534134 17793024 3866 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3888 0 0 0 89001 15 0 0 25 0 1 0 428534134 17793024 3866 4294967295 134512640 134672761 3221224544 3221223728 134559596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3888 0 0 0 90001 15 0 0 25 0 1 0 428534134 17793024 3866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3866 603 41 0 4303 0
vsize: 17376
[startup+910.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3892 0 0 0 91001 15 0 0 25 0 1 0 428534134 17793024 3870 4294967295 134512640 134672761 3221224544 3221223728 134559358 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3870 603 41 0 4303 0
vsize: 17376
[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3894 0 0 0 92001 15 0 0 25 0 1 0 428534134 17793024 3872 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3872 603 41 0 4303 0
vsize: 17376
[startup+930.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3906 0 0 0 93001 16 0 0 25 0 1 0 428534134 17793024 3884 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3884 603 41 0 4303 0
vsize: 17376
[startup+940.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3913 0 0 0 94001 16 0 0 25 0 1 0 428534134 17793024 3891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3891 603 41 0 4303 0
vsize: 17376
[startup+950.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3914 0 0 0 95001 16 0 0 25 0 1 0 428534134 17793024 3892 4294967295 134512640 134672761 3221224544 3221223728 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4344 3892 603 41 0 4303 0
vsize: 17376
[startup+960.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3920 0 0 0 96002 16 0 0 25 0 1 0 428534134 17956864 3898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4384 3898 603 41 0 4343 0
vsize: 17536
[startup+970.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3921 0 0 0 97001 16 0 0 25 0 1 0 428534134 17956864 3899 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4384 3899 603 41 0 4343 0
vsize: 17536
[startup+980.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3926 0 0 0 98002 16 0 0 25 0 1 0 428534134 17956864 3904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4384 3904 603 41 0 4343 0
vsize: 17536
[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25446
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3928 0 0 0 99002 16 0 0 25 0 1 0 428534134 17956864 3906 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4384 3906 603 41 0 4343 0
vsize: 17536
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3928 0 0 0 100001 16 0 0 25 0 1 0 428534134 17956864 3906 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3906 603 41 0 4343 0
vsize: 17536
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3929 0 0 0 101002 16 0 0 25 0 1 0 428534134 17956864 3907 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3907 603 41 0 4343 0
vsize: 17536
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3929 0 0 0 102002 16 0 0 25 0 1 0 428534134 17956864 3907 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3907 603 41 0 4343 0
vsize: 17536
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3939 0 0 0 103002 16 0 0 25 0 1 0 428534134 17956864 3917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3917 603 41 0 4343 0
vsize: 17536
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3955 0 0 0 104002 16 0 0 25 0 1 0 428534134 18120704 3933 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3955 0 0 0 105002 16 0 0 25 0 1 0 428534134 18120704 3933 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3955 0 0 0 106002 16 0 0 25 0 1 0 428534134 18120704 3933 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3955 0 0 0 107003 16 0 0 25 0 1 0 428534134 18120704 3933 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3955 0 0 0 108003 16 0 0 25 0 1 0 428534134 18120704 3933 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3955 0 0 0 109003 16 0 0 25 0 1 0 428534134 18120704 3933 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 3955 0 0 0 110003 16 0 0 25 0 1 0 428534134 18120704 3933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4424 3933 603 41 0 4383 0
vsize: 17696
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4093 0 0 0 111002 17 0 0 25 0 1 0 428534134 18653184 4071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4554 4071 603 41 0 4513 0
vsize: 18216
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4106 0 0 0 112003 17 0 0 25 0 1 0 428534134 18653184 4084 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4554 4084 603 41 0 4513 0
vsize: 18216
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4114 0 0 0 113003 17 0 0 25 0 1 0 428534134 18653184 4092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4554 4092 603 41 0 4513 0
vsize: 18216
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4123 0 0 0 114002 17 0 0 25 0 1 0 428534134 18788352 4101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4587 4101 603 41 0 4546 0
vsize: 18348
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4141 0 0 0 115002 17 0 0 25 0 1 0 428534134 18788352 4119 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4587 4119 603 41 0 4546 0
vsize: 18348
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4194 0 0 0 116003 17 0 0 25 0 1 0 428534134 19050496 4172 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4172 603 41 0 4610 0
vsize: 18604
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4195 0 0 0 117003 17 0 0 25 0 1 0 428534134 19050496 4173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4173 603 41 0 4610 0
vsize: 18604
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4204 0 0 0 118003 17 0 0 25 0 1 0 428534134 19050496 4182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4651 4182 603 41 0 4610 0
vsize: 18604
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4213 0 0 0 119003 17 0 0 25 0 1 0 428534134 19197952 4191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4191 603 41 0 4646 0
vsize: 18748
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 25448
Raw data (stat): 25440 (minisat+) R 25439 12452 12451 0 -1 0 4213 0 0 0 120003 17 0 0 25 0 1 0 428534134 19197952 4191 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4687 4191 603 41 0 4646 0
vsize: 18748
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 25448
Raw data (stat): 25440 (minisat+) Z 25439 12452 12451 0 -1 12 4216 0 0 0 120003 18 0 0 25 0 1 0 428534134 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.23
CPU user time (s): 1200.04
CPU system time (s): 0.187971
CPU usage (%): 100.014
Max. virtual memory (Kb): 18748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####