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 21783

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-22 00:57:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12661 boxname=wulflinc24 idbench=974 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c00b2eef1eabd5880b83093b756a5dd4  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare2.opb
IDLAUNCH: 12661
/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:        473712 kB
Buffers:         34248 kB
Cached:         502564 kB
SwapCached:        524 kB
Active:         215156 kB
Inactive:       323632 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        473460 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16568 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:17:27 (client local time) WITH STATUS 10 IN 1200.38 SECONDS
stats: 12661 7 1200.38 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]---> BDD-cost:33300
c ---[  10]---> BDD-cost:39181
c ---[   8]---> BDD-cost:34989
c ---[   6]---> BDD-cost:41590
c ---[   4]---> BDD-cost:41670
c ---[   2]---> BDD-cost:41238
c ---[   0]---> BDD-cost:35327
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  774421  2270408 |  258140       0        0     nan |  0.000 % |
c |       100 |  774421  2270408 |  283954     100    10529   105.3 |  0.026 % |
c ==============================================================================
c [1mFound solution: 8321024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2158     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       101 |  779941  2283300 |  259980     101    10563   104.6 |  0.026 % |
c ==============================================================================
c [1mFound solution: 8070144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       103 |  779972  2283416 |  259990     103    10593   102.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7919616[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 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 |       103 |  779984  2283446 |  259994     103    10593   102.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7883776[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 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 |       103 |  779998  2283478 |  259999     103    10593   102.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7766016[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 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 |       195 |  780011  2283508 |  260003     195    17056    87.5 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7600128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       195 |  780017  2283523 |  260005     195    17056    87.5 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7581696[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 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 |       210 |  780028  2283551 |  260009     210    17898    85.2 |  0.026 % |
c ==============================================================================
c [1mFound solution: 7541760[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 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 |       289 |  780041  2283581 |  260013     289    22921    79.3 |  0.026 % |
c |       389 |  780041  2283581 |  286014     389    28159    72.4 |  0.029 % |
c |       542 |  780041  2283581 |  314615     542    36432    67.2 |  0.029 % |
c ==============================================================================
c [1mFound solution: 7353344[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 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 |       611 |  780051  2283603 |  260017     611    40926    67.0 |  0.029 % |
c |       711 |  780051  2283603 |  286018     711    45549    64.1 |  0.029 % |
c |       861 |  780051  2283603 |  314620     861    53044    61.6 |  0.029 % |
c |      1088 |  780051  2283603 |  346082    1088    68036    62.5 |  0.029 % |
c |      1425 |  780051  2283603 |  380690    1425    89057    62.5 |  0.029 % |
c ==============================================================================
c [1mFound solution: 7134208[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 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 |      1552 |  780074  2283662 |  260024    1552    96231    62.0 |  0.029 % |
c ==============================================================================
c [1mFound solution: 7091200[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 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1588 |  780084  2283688 |  260028    1588    98169    61.8 |  0.029 % |
c ==============================================================================
c [1mFound solution: 6865920[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 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 |      1629 |  780095  2283714 |  260031    1629   100375    61.6 |  0.029 % |
c |      1730 |  780095  2283714 |  286034    1730   105382    60.9 |  0.030 % |
c ==============================================================================
c [1mFound solution: 6863872[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 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 |      1870 |  780107  2283742 |  260035    1870   113202    60.5 |  0.030 % |
c |      1970 |  780107  2283742 |  286038    1970   117506    59.6 |  0.031 % |
c |      2120 |  780107  2283742 |  314642    2120   124851    58.9 |  0.031 % |
c ==============================================================================
c [1mFound solution: 6833152[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 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 |      2280 |  780117  2283765 |  260039    2280   133876    58.7 |  0.031 % |
c |      2380 |  780117  2283765 |  286042    2380   138500    58.2 |  0.031 % |
c |      2530 |  780117  2283765 |  314647    2530   147991    58.5 |  0.031 % |
c |      2755 |  780117  2283765 |  346111    2755   162068    58.8 |  0.031 % |
c ==============================================================================
c [1mFound solution: 6819840[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 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 |      3070 |  780129  2283792 |  260043    3070   178746    58.2 |  0.031 % |
c ==============================================================================
c [1mFound solution: 6724608[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 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 |      3123 |  780139  2283816 |  260046    3123   181367    58.1 |  0.031 % |
c |      3223 |  780139  2283816 |  286050    3223   188180    58.4 |  0.032 % |
c |      3374 |  780139  2283816 |  314655    3374   196412    58.2 |  0.032 % |
c ==============================================================================
c [1mFound solution: 6516736[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 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 |      3454 |  780148  2283838 |  260049    3454   201541    58.4 |  0.032 % |
c ==============================================================================
c [1mFound solution: 6364160[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 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 |      3517 |  780157  2283858 |  260052    3517   205162    58.3 |  0.032 % |
c |      3618 |  780157  2283858 |  286057    3618   211177    58.4 |  0.033 % |
c |      3769 |  780157  2283858 |  314662    3769   217893    57.8 |  0.033 % |
c |      3994 |  780157  2283858 |  346129    3994   227695    57.0 |  0.033 % |
c ==============================================================================
c [1mFound solution: 6243328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4031 |  780166  2283883 |  260055    4031   229780    57.0 |  0.033 % |
c |      4131 |  780166  2283883 |  286060    4131   234574    56.8 |  0.033 % |
c |      4285 |  780166  2283883 |  314666    4285   242550    56.6 |  0.033 % |
c ==============================================================================
c [1mFound solution: 5986304[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 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 |      4421 |  780176  2283908 |  260058    4421   249628    56.5 |  0.033 % |
c |      4521 |  780176  2283908 |  286063    4521   255299    56.5 |  0.033 % |
c |      4672 |  780176  2283908 |  314670    4672   264929    56.7 |  0.033 % |
c ==============================================================================
c [1mFound solution: 5938176[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 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4877 |  780183  2283925 |  260061    4877   273374    56.1 |  0.033 % |
c |      4980 |  780183  2283925 |  286067    4980   278523    55.9 |  0.034 % |
c ==============================================================================
c [1mFound solution: 5903360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5049 |  780192  2283946 |  260064    5049   282254    55.9 |  0.034 % |
c |      5149 |  780192  2283946 |  286070    5149   287079    55.8 |  0.034 % |
c |      5299 |  780192  2283946 |  314677    5299   295239    55.7 |  0.034 % |
c ==============================================================================
c [1mFound solution: 5857280[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 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 |      5385 |  780205  2283977 |  260068    5385   300440    55.8 |  0.034 % |
c |      5486 |  780205  2283977 |  286074    5486   305598    55.7 |  0.035 % |
c |      5636 |  780205  2283977 |  314682    5636   313066    55.5 |  0.035 % |
c |      5863 |  780205  2283977 |  346150    5863   324692    55.4 |  0.035 % |
c |      6200 |  780205  2283977 |  380765    6200   347453    56.0 |  0.035 % |
c ==============================================================================
c [1mFound solution: 5834752[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 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 |      6661 |  780219  2284009 |  260073    6661   378987    56.9 |  0.035 % |
c |      6761 |  780219  2284009 |  286080    6761   384193    56.8 |  0.035 % |
c |      6911 |  780219  2284009 |  314688    6911   393158    56.9 |  0.035 % |
c ==============================================================================
c [1mFound solution: 5734400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7077 |  780224  2284023 |  260074    7077   402215    56.8 |  0.035 % |
c |      7177 |  780224  2284023 |  286081    7177   407628    56.8 |  0.035 % |
c |      7328 |  780224  2284023 |  314689    7328   415420    56.7 |  0.035 % |
c |      7554 |  780224  2284023 |  346158    7554   427298    56.6 |  0.035 % |
c ==============================================================================
c [1mFound solution: 5697536[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 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 |      7670 |  780232  2284043 |  260077    7670   433847    56.6 |  0.035 % |
c |      7770 |  780232  2284043 |  286084    7770   439094    56.5 |  0.036 % |
c |      7920 |  780232  2284043 |  314693    7920   447260    56.5 |  0.036 % |
c |      8146 |  780232  2284043 |  346162    8146   459809    56.4 |  0.036 % |
c ==============================================================================
c [1mFound solution: 5468160[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 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8426 |  780238  2284056 |  260079    8426   473802    56.2 |  0.036 % |
c |      8527 |  780238  2284056 |  286086    8527   477769    56.0 |  0.036 % |
c |      8677 |  780238  2284056 |  314695    8677   487858    56.2 |  0.036 % |
c |      8902 |  780238  2284056 |  346165    8902   499073    56.1 |  0.036 % |
c |      9240 |  780238  2284056 |  380781    9240   518923    56.2 |  0.036 % |
c |      9746 |  780238  2284056 |  418859    9746   545702    56.0 |  0.036 % |
c |     10505 |  780238  2284056 |  460745   10505   592588    56.4 |  0.036 % |
c |     11645 |  780238  2284056 |  506820   11645   666340    57.2 |  0.036 % |
c ==============================================================================
c [1mFound solution: 5413888[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 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 |     11919 |  780242  2284065 |  260080   11919   681943    57.2 |  0.036 % |
c |     12019 |  780242  2284065 |  286088   12019   686729    57.1 |  0.036 % |
c |     12169 |  780242  2284065 |  314696   12169   695133    57.1 |  0.036 % |
c |     12394 |  780242  2284065 |  346166   12394   708680    57.2 |  0.036 % |
c |     12731 |  780242  2284065 |  380783   12731   730101    57.3 |  0.036 % |
c |     13238 |  780242  2284065 |  418861   13238   763643    57.7 |  0.036 % |
c ==============================================================================
c [1mFound solution: 5405696[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 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 |     13777 |  780252  2284088 |  260084   13777   795945    57.8 |  0.036 % |
c |     13878 |  780252  2284088 |  286092   13878   802651    57.8 |  0.037 % |
c ==============================================================================
c [1mFound solution: 5364736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14021 |  780259  2284104 |  260086   14021   812373    57.9 |  0.037 % |
c |     14121 |  780259  2284104 |  286094   14121   817922    57.9 |  0.037 % |
c |     14273 |  780259  2284104 |  314704   14273   826360    57.9 |  0.037 % |
c |     14498 |  780259  2284104 |  346174   14498   838932    57.9 |  0.037 % |
c |     14835 |  780259  2284104 |  380791   14835   857354    57.8 |  0.037 % |
c ==============================================================================
c [1mFound solution: 5243904[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 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 |     15330 |  780268  2284123 |  260089   15330   887315    57.9 |  0.037 % |
c ==============================================================================
c [1mFound solution: 5239808[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 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 |     15423 |  780279  2284155 |  260093   15423   893070    57.9 |  0.037 % |
c |     15523 |  780279  2284155 |  286102   15523   899973    58.0 |  0.038 % |
c |     15673 |  780279  2284155 |  314712   15673   908713    58.0 |  0.038 % |
c ==============================================================================
c [1mFound solution: 5169152[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 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 |     15833 |  780287  2284178 |  260095   15833   916731    57.9 |  0.038 % |
c |     15935 |  780287  2284178 |  286104   15935   920864    57.8 |  0.038 % |
c |     16086 |  780287  2284178 |  314714   16086   931652    57.9 |  0.038 % |
c ==============================================================================
c [1mFound solution: 5128192[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 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 |     16122 |  780297  2284203 |  260099   16122   933881    57.9 |  0.038 % |
c |     16222 |  780297  2284203 |  286108   16222   939703    57.9 |  0.039 % |
c |     16372 |  780297  2284203 |  314719   16372   946289    57.8 |  0.039 % |
c |     16597 |  780297  2284203 |  346191   16597   961057    57.9 |  0.039 % |
c ==============================================================================
c [1mFound solution: 4799488[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 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 |     16734 |  780307  2284226 |  260102   16734   967493    57.8 |  0.039 % |
c |     16837 |  780307  2284226 |  286112   16837   971971    57.7 |  0.039 % |
c |     16990 |  780307  2284226 |  314723   16990   978660    57.6 |  0.039 % |
#### 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): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (runsolver) R 21802 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549572195 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 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.0161 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24226 0 0 0 942 57 0 0 25 0 1 0 549572195 115720192 22691 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28252 22691 603 41 0 28211 0
vsize: 113008
[startup+20.0325 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24794 0 0 0 1940 59 0 0 25 0 1 0 549572195 118697984 23259 4294967295 134512640 134672761 3221224528 3221223860 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28979 23259 603 41 0 28938 0
vsize: 115916
[startup+30.1421 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24916 0 0 0 2950 59 0 0 25 0 1 0 549572195 119156736 23381 4294967295 134512640 134672761 3221224528 3221223632 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29091 23381 603 41 0 29050 0
vsize: 116364
[startup+40.1421 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24928 0 0 0 3949 59 0 0 25 0 1 0 549572195 119156736 23393 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29091 23393 603 41 0 29050 0
vsize: 116364
[startup+50.1425 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24941 0 0 0 4950 59 0 0 25 0 1 0 549572195 119287808 23406 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29123 23406 603 41 0 29082 0
vsize: 116492
[startup+60.1495 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24955 0 0 0 5950 59 0 0 25 0 1 0 549572195 119287808 23420 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29123 23420 603 41 0 29082 0
vsize: 116492
[startup+70.1549 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24969 0 0 0 6950 59 0 0 25 0 1 0 549572195 119418880 23434 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29155 23434 603 41 0 29114 0
vsize: 116620
[startup+80.1546 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24979 0 0 0 7949 59 0 0 25 0 1 0 549572195 119418880 23444 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29155 23444 603 41 0 29114 0
vsize: 116620
[startup+90.1545 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24988 0 0 0 8950 60 0 0 25 0 1 0 549572195 119418880 23453 4294967295 134512640 134672761 3221224528 3221223632 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29155 23453 603 41 0 29114 0
vsize: 116620
[startup+100.154 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 24995 0 0 0 9950 60 0 0 25 0 1 0 549572195 119418880 23460 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29155 23460 603 41 0 29114 0
vsize: 116620
[startup+110.16 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25004 0 0 0 10950 60 0 0 25 0 1 0 549572195 119549952 23469 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29187 23469 603 41 0 29146 0
vsize: 116748
[startup+120.16 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25011 0 0 0 11951 60 0 0 25 0 1 0 549572195 119549952 23476 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29187 23476 603 41 0 29146 0
vsize: 116748
[startup+130.16 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25021 0 0 0 12950 60 0 0 25 0 1 0 549572195 119549952 23486 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29187 23486 603 41 0 29146 0
vsize: 116748
[startup+140.16 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25031 0 0 0 13950 60 0 0 25 0 1 0 549572195 119668736 23496 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29216 23496 603 41 0 29175 0
vsize: 116864
[startup+150.168 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 21803
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25034 0 0 0 14951 60 0 0 25 0 1 0 549572195 119668736 23499 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29216 23499 603 41 0 29175 0
vsize: 116864
[startup+160.167 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 21804
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25049 0 0 0 15951 60 0 0 25 0 1 0 549572195 119668736 23514 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29216 23514 603 41 0 29175 0
vsize: 116864
[startup+170.182 s]
Raw data (loadavg): 1.23 1.02 0.93 2/57 21840
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25058 0 0 0 16953 60 0 0 25 0 1 0 549572195 119668736 23523 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29216 23523 603 41 0 29175 0
vsize: 116864
[startup+180.183 s]
Raw data (loadavg): 1.35 1.05 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25069 0 0 0 17953 60 0 0 25 0 1 0 549572195 119799808 23534 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29248 23534 603 41 0 29207 0
vsize: 116992
[startup+190.183 s]
Raw data (loadavg): 1.29 1.05 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25081 0 0 0 18953 60 0 0 25 0 1 0 549572195 119799808 23546 4294967295 134512640 134672761 3221224528 3221223784 134562565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29248 23546 603 41 0 29207 0
vsize: 116992
[startup+200.183 s]
Raw data (loadavg): 1.25 1.05 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25089 0 0 0 19953 60 0 0 25 0 1 0 549572195 119799808 23554 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29248 23554 603 41 0 29207 0
vsize: 116992
[startup+210.189 s]
Raw data (loadavg): 1.21 1.05 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25099 0 0 0 20954 60 0 0 25 0 1 0 549572195 119934976 23564 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29281 23564 603 41 0 29240 0
vsize: 117124
[startup+220.197 s]
Raw data (loadavg): 1.18 1.05 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25108 0 0 0 21954 60 0 0 25 0 1 0 549572195 119934976 23573 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29281 23573 603 41 0 29240 0
vsize: 117124
[startup+230.201 s]
Raw data (loadavg): 1.15 1.04 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25114 0 0 0 22954 60 0 0 25 0 1 0 549572195 119934976 23579 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29281 23579 603 41 0 29240 0
vsize: 117124
[startup+240.202 s]
Raw data (loadavg): 1.13 1.04 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25125 0 0 0 23954 60 0 0 25 0 1 0 549572195 119934976 23590 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29281 23590 603 41 0 29240 0
vsize: 117124
[startup+250.201 s]
Raw data (loadavg): 1.11 1.04 0.94 2/54 21856
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25136 0 0 0 24954 60 0 0 25 0 1 0 549572195 120057856 23601 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29311 23601 603 41 0 29270 0
vsize: 117244
[startup+260.201 s]
Raw data (loadavg): 1.09 1.04 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25149 0 0 0 25955 60 0 0 25 0 1 0 549572195 120057856 23614 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29311 23614 603 41 0 29270 0
vsize: 117244
[startup+270.202 s]
Raw data (loadavg): 1.08 1.04 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25160 0 0 0 26955 60 0 0 25 0 1 0 549572195 120176640 23625 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29340 23625 603 41 0 29299 0
vsize: 117360
[startup+280.202 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25172 0 0 0 27955 61 0 0 25 0 1 0 549572195 120176640 23637 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29340 23637 603 41 0 29299 0
vsize: 117360
[startup+290.206 s]
Raw data (loadavg): 1.05 1.03 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25183 0 0 0 28955 61 0 0 25 0 1 0 549572195 120176640 23648 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29340 23648 603 41 0 29299 0
vsize: 117360
[startup+300.207 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25195 0 0 0 29955 61 0 0 25 0 1 0 549572195 120307712 23660 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29372 23660 603 41 0 29331 0
vsize: 117488
[startup+310.206 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25203 0 0 0 30955 61 0 0 25 0 1 0 549572195 120307712 23668 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29372 23668 603 41 0 29331 0
vsize: 117488
[startup+320.206 s]
Raw data (loadavg): 1.03 1.03 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25213 0 0 0 31956 61 0 0 25 0 1 0 549572195 120307712 23678 4294967295 134512640 134672761 3221224528 3221223652 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29372 23678 603 41 0 29331 0
vsize: 117488
[startup+330.206 s]
Raw data (loadavg): 1.03 1.03 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25235 0 0 0 32956 61 0 0 25 0 1 0 549572195 120885248 23700 4294967295 134512640 134672761 3221224528 3221223712 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29513 23700 603 41 0 29472 0
vsize: 118052
[startup+340.207 s]
Raw data (loadavg): 1.02 1.03 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25246 0 0 0 33956 61 0 0 25 0 1 0 549572195 120885248 23711 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29513 23711 603 41 0 29472 0
vsize: 118052
[startup+350.207 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25265 0 0 0 34956 61 0 0 25 0 1 0 549572195 121008128 23730 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29543 23730 603 41 0 29502 0
vsize: 118172
[startup+360.207 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25281 0 0 0 35955 62 0 0 25 0 1 0 549572195 121008128 23746 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29543 23746 603 41 0 29502 0
vsize: 118172
[startup+370.207 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25288 0 0 0 36955 62 0 0 25 0 1 0 549572195 121008128 23753 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29543 23753 603 41 0 29502 0
vsize: 118172
[startup+380.207 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25302 0 0 0 37956 62 0 0 25 0 1 0 549572195 121131008 23767 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29573 23767 603 41 0 29532 0
vsize: 118292
[startup+390.207 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25312 0 0 0 38956 62 0 0 25 0 1 0 549572195 121131008 23777 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29573 23777 603 41 0 29532 0
vsize: 118292
[startup+400.207 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25321 0 0 0 39956 62 0 0 25 0 1 0 549572195 121131008 23786 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29573 23786 603 41 0 29532 0
vsize: 118292
[startup+410.214 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25330 0 0 0 40956 62 0 0 25 0 1 0 549572195 121262080 23795 4294967295 134512640 134672761 3221224528 3221223696 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29605 23795 603 41 0 29564 0
vsize: 118420
[startup+420.215 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25342 0 0 0 41957 62 0 0 25 0 1 0 549572195 121262080 23807 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29605 23807 603 41 0 29564 0
vsize: 118420
[startup+430.215 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25353 0 0 0 42957 62 0 0 25 0 1 0 549572195 121262080 23818 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29605 23818 603 41 0 29564 0
vsize: 118420
[startup+440.215 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25360 0 0 0 43957 62 0 0 25 0 1 0 549572195 121262080 23825 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29605 23825 603 41 0 29564 0
vsize: 118420
[startup+450.215 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25370 0 0 0 44957 62 0 0 25 0 1 0 549572195 121397248 23835 4294967295 134512640 134672761 3221224528 3221223712 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29638 23835 603 41 0 29597 0
vsize: 118552
[startup+460.214 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25378 0 0 0 45957 62 0 0 25 0 1 0 549572195 121397248 23843 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29638 23843 603 41 0 29597 0
vsize: 118552
[startup+470.214 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25390 0 0 0 46957 62 0 0 25 0 1 0 549572195 121397248 23855 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29638 23855 603 41 0 29597 0
vsize: 118552
[startup+480.214 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25400 0 0 0 47957 62 0 0 25 0 1 0 549572195 121532416 23865 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29671 23865 603 41 0 29630 0
vsize: 118684
[startup+490.215 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25408 0 0 0 48958 62 0 0 25 0 1 0 549572195 121532416 23873 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29671 23873 603 41 0 29630 0
vsize: 118684
[startup+500.215 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25420 0 0 0 49958 62 0 0 25 0 1 0 549572195 121532416 23885 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29671 23885 603 41 0 29630 0
vsize: 118684
[startup+510.215 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21858
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25424 0 0 0 50958 63 0 0 25 0 1 0 549572195 121532416 23889 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29671 23889 603 41 0 29630 0
vsize: 118684
[startup+520.215 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25434 0 0 0 51958 63 0 0 25 0 1 0 549572195 121663488 23899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29703 23899 603 41 0 29662 0
vsize: 118812
[startup+530.215 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25444 0 0 0 52958 63 0 0 25 0 1 0 549572195 121663488 23909 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29703 23909 603 41 0 29662 0
vsize: 118812
[startup+540.216 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25453 0 0 0 53958 63 0 0 25 0 1 0 549572195 121663488 23918 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29703 23918 603 41 0 29662 0
vsize: 118812
[startup+550.216 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25460 0 0 0 54959 63 0 0 25 0 1 0 549572195 121663488 23925 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29703 23925 603 41 0 29662 0
vsize: 118812
[startup+560.216 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25468 0 0 0 55959 63 0 0 25 0 1 0 549572195 121794560 23933 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29735 23933 603 41 0 29694 0
vsize: 118940
[startup+570.217 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25478 0 0 0 56959 63 0 0 25 0 1 0 549572195 121794560 23943 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29735 23943 603 41 0 29694 0
vsize: 118940
[startup+580.216 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25488 0 0 0 57959 63 0 0 25 0 1 0 549572195 121937920 23953 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29770 23953 603 41 0 29729 0
vsize: 119080
[startup+590.216 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25500 0 0 0 58959 63 0 0 25 0 1 0 549572195 121937920 23965 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29770 23965 603 41 0 29729 0
vsize: 119080
[startup+600.217 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25513 0 0 0 59959 63 0 0 25 0 1 0 549572195 121937920 23978 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29770 23978 603 41 0 29729 0
vsize: 119080
[startup+610.216 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25522 0 0 0 60959 63 0 0 25 0 1 0 549572195 122068992 23987 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29802 23987 603 41 0 29761 0
vsize: 119208
[startup+620.217 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25531 0 0 0 61959 63 0 0 25 0 1 0 549572195 122068992 23996 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29802 23996 603 41 0 29761 0
vsize: 119208
[startup+630.217 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25538 0 0 0 62959 63 0 0 25 0 1 0 549572195 122068992 24003 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29802 24003 603 41 0 29761 0
vsize: 119208
[startup+640.218 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25546 0 0 0 63959 64 0 0 25 0 1 0 549572195 122068992 24011 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29802 24011 603 41 0 29761 0
vsize: 119208
[startup+650.218 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25553 0 0 0 64960 64 0 0 25 0 1 0 549572195 122068992 24018 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29802 24018 603 41 0 29761 0
vsize: 119208
[startup+660.218 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25564 0 0 0 65960 64 0 0 25 0 1 0 549572195 122200064 24029 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29834 24029 603 41 0 29793 0
vsize: 119336
[startup+670.218 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25572 0 0 0 66960 64 0 0 25 0 1 0 549572195 122200064 24037 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29834 24037 603 41 0 29793 0
vsize: 119336
[startup+680.218 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25582 0 0 0 67960 64 0 0 25 0 1 0 549572195 122200064 24047 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29834 24047 603 41 0 29793 0
vsize: 119336
[startup+690.218 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25591 0 0 0 68960 64 0 0 25 0 1 0 549572195 122331136 24056 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29866 24056 603 41 0 29825 0
vsize: 119464
[startup+700.219 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25603 0 0 0 69960 64 0 0 25 0 1 0 549572195 122331136 24068 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29866 24068 603 41 0 29825 0
vsize: 119464
[startup+710.219 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25615 0 0 0 70960 64 0 0 25 0 1 0 549572195 122331136 24080 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29866 24080 603 41 0 29825 0
vsize: 119464
[startup+720.22 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25626 0 0 0 71961 64 0 0 25 0 1 0 549572195 122462208 24091 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29898 24091 603 41 0 29857 0
vsize: 119592
[startup+730.22 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25636 0 0 0 72961 64 0 0 25 0 1 0 549572195 122462208 24101 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29898 24101 603 41 0 29857 0
vsize: 119592
[startup+740.22 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25641 0 0 0 73961 64 0 0 25 0 1 0 549572195 122462208 24106 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29898 24106 603 41 0 29857 0
vsize: 119592
[startup+750.22 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25649 0 0 0 74961 64 0 0 25 0 1 0 549572195 122462208 24114 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29898 24114 603 41 0 29857 0
vsize: 119592
[startup+760.219 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25660 0 0 0 75961 64 0 0 25 0 1 0 549572195 122589184 24125 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29929 24125 603 41 0 29888 0
vsize: 119716
[startup+770.22 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25672 0 0 0 76961 64 0 0 25 0 1 0 549572195 122589184 24137 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29929 24137 603 41 0 29888 0
vsize: 119716
[startup+780.22 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25683 0 0 0 77961 64 0 0 25 0 1 0 549572195 122589184 24148 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29929 24148 603 41 0 29888 0
vsize: 119716
[startup+790.22 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25694 0 0 0 78961 64 0 0 25 0 1 0 549572195 122720256 24159 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29961 24159 603 41 0 29920 0
vsize: 119844
[startup+800.221 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25703 0 0 0 79961 65 0 0 25 0 1 0 549572195 122720256 24168 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29961 24168 603 41 0 29920 0
vsize: 119844
[startup+810.221 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25712 0 0 0 80962 65 0 0 25 0 1 0 549572195 122720256 24177 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29961 24177 603 41 0 29920 0
vsize: 119844
[startup+820.221 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25720 0 0 0 81962 65 0 0 25 0 1 0 549572195 122847232 24185 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29992 24185 603 41 0 29951 0
vsize: 119968
[startup+830.221 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25730 0 0 0 82961 65 0 0 25 0 1 0 549572195 122847232 24195 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29992 24195 603 41 0 29951 0
vsize: 119968
[startup+840.222 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25740 0 0 0 83961 66 0 0 25 0 1 0 549572195 122847232 24205 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29992 24205 603 41 0 29951 0
vsize: 119968
[startup+850.223 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25748 0 0 0 84960 66 0 0 25 0 1 0 549572195 122978304 24213 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30024 24213 603 41 0 29983 0
vsize: 120096
[startup+860.222 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25758 0 0 0 85960 66 0 0 25 0 1 0 549572195 122978304 24223 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30024 24223 603 41 0 29983 0
vsize: 120096
[startup+870.223 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25770 0 0 0 86960 66 0 0 25 0 1 0 549572195 122978304 24235 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30024 24235 603 41 0 29983 0
vsize: 120096
[startup+880.223 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25780 0 0 0 87961 66 0 0 25 0 1 0 549572195 123113472 24245 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30057 24245 603 41 0 30016 0
vsize: 120228
[startup+890.223 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25792 0 0 0 88961 66 0 0 25 0 1 0 549572195 123113472 24257 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30057 24257 603 41 0 30016 0
vsize: 120228
[startup+900.224 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25800 0 0 0 89961 66 0 0 25 0 1 0 549572195 123113472 24265 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30057 24265 603 41 0 30016 0
vsize: 120228
[startup+910.224 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25813 0 0 0 90961 66 0 0 25 0 1 0 549572195 123113472 24278 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30057 24278 603 41 0 30016 0
vsize: 120228
[startup+920.224 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25825 0 0 0 91961 66 0 0 25 0 1 0 549572195 123244544 24290 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30089 24290 603 41 0 30048 0
vsize: 120356
[startup+930.224 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25833 0 0 0 92961 66 0 0 25 0 1 0 549572195 123244544 24298 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30089 24298 603 41 0 30048 0
vsize: 120356
[startup+940.225 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25838 0 0 0 93962 66 0 0 25 0 1 0 549572195 123244544 24303 4294967295 134512640 134672761 3221224528 3221223696 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30089 24303 603 41 0 30048 0
vsize: 120356
[startup+950.224 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25846 0 0 0 94961 67 0 0 25 0 1 0 549572195 123375616 24311 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30121 24311 603 41 0 30080 0
vsize: 120484
[startup+960.225 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25859 0 0 0 95961 67 0 0 25 0 1 0 549572195 123375616 24324 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30121 24324 603 41 0 30080 0
vsize: 120484
[startup+970.225 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25867 0 0 0 96961 67 0 0 25 0 1 0 549572195 123375616 24332 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30121 24332 603 41 0 30080 0
vsize: 120484
[startup+980.224 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25879 0 0 0 97961 67 0 0 25 0 1 0 549572195 123510784 24344 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30154 24344 603 41 0 30113 0
vsize: 120616
[startup+990.225 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25889 0 0 0 98961 68 0 0 25 0 1 0 549572195 123510784 24354 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30154 24354 603 41 0 30113 0
vsize: 120616
[startup+1000.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25899 0 0 0 99961 68 0 0 25 0 1 0 549572195 123510784 24364 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30154 24364 603 41 0 30113 0
vsize: 120616
[startup+1010.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25908 0 0 0 100961 68 0 0 25 0 1 0 549572195 123645952 24373 4294967295 134512640 134672761 3221224528 3221223728 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30187 24373 603 41 0 30146 0
vsize: 120748
[startup+1020.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25915 0 0 0 101962 68 0 0 25 0 1 0 549572195 123645952 24380 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30187 24380 603 41 0 30146 0
vsize: 120748
[startup+1030.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25924 0 0 0 102962 68 0 0 25 0 1 0 549572195 123645952 24389 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30187 24389 603 41 0 30146 0
vsize: 120748
[startup+1040.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25934 0 0 0 103962 68 0 0 25 0 1 0 549572195 123645952 24399 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30187 24399 603 41 0 30146 0
vsize: 120748
[startup+1050.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25942 0 0 0 104962 68 0 0 25 0 1 0 549572195 123781120 24407 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30220 24407 603 41 0 30179 0
vsize: 120880
[startup+1060.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25957 0 0 0 105962 68 0 0 25 0 1 0 549572195 123781120 24422 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30220 24422 603 41 0 30179 0
vsize: 120880
[startup+1070.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25966 0 0 0 106962 68 0 0 25 0 1 0 549572195 123781120 24431 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30220 24431 603 41 0 30179 0
vsize: 120880
[startup+1080.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25976 0 0 0 107962 68 0 0 25 0 1 0 549572195 123920384 24441 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30254 24441 603 41 0 30213 0
vsize: 121016
[startup+1090.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 25987 0 0 0 108963 68 0 0 25 0 1 0 549572195 123920384 24452 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30254 24452 603 41 0 30213 0
vsize: 121016
[startup+1100.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26000 0 0 0 109963 68 0 0 25 0 1 0 549572195 123920384 24465 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30254 24465 603 41 0 30213 0
vsize: 121016
[startup+1110.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26009 0 0 0 110963 68 0 0 25 0 1 0 549572195 124047360 24474 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30285 24474 603 41 0 30244 0
vsize: 121140
[startup+1120.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26019 0 0 0 111963 69 0 0 25 0 1 0 549572195 124047360 24484 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30285 24484 603 41 0 30244 0
vsize: 121140
[startup+1130.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26031 0 0 0 112963 69 0 0 25 0 1 0 549572195 124047360 24496 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30285 24496 603 41 0 30244 0
vsize: 121140
[startup+1140.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26053 0 0 0 113963 69 0 0 25 0 1 0 549572195 124317696 24518 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30351 24518 603 41 0 30310 0
vsize: 121404
[startup+1150.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26053 0 0 0 114963 69 0 0 25 0 1 0 549572195 124317696 24518 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30351 24518 603 41 0 30310 0
vsize: 121404
[startup+1160.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26058 0 0 0 115963 69 0 0 25 0 1 0 549572195 124317696 24523 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30351 24523 603 41 0 30310 0
vsize: 121404
[startup+1170.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26067 0 0 0 116963 69 0 0 25 0 1 0 549572195 124317696 24532 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30351 24532 603 41 0 30310 0
vsize: 121404
[startup+1180.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26070 0 0 0 117963 69 0 0 25 0 1 0 549572195 124317696 24535 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30351 24535 603 41 0 30310 0
vsize: 121404
[startup+1190.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26078 0 0 0 118963 69 0 0 25 0 1 0 549572195 124317696 24543 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30351 24543 603 41 0 30310 0
vsize: 121404
[startup+1200.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 21860
Raw data (stat): 21803 (minisat+) R 21802 28546 28545 0 -1 0 26087 0 0 0 119963 69 0 0 25 0 1 0 549572195 124317696 24552 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30351 24552 603 41 0 30310 0
vsize: 121404
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.28 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 21860
Raw data (stat): 21803 (minisat+) Z 21802 28546 28545 0 -1 12 26090 0 0 0 119964 74 0 0 25 0 1 0 549572195 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.28
CPU time (s): 1200.38
CPU user time (s): 1199.64
CPU system time (s): 0.742887
CPU usage (%): 100.008
Max. virtual memory (Kb): 121404
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####