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/miplib3/normalized-mps-v2-20-10-markshare2.opb
MD5SUM	111dddb6adf389a5275ab413feff6076
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.36
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 21283

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 23:17:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13532 boxname=wulflinc5 idbench=1041 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  111dddb6adf389a5275ab413feff6076  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare2.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare2.opb
IDLAUNCH: 13532
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        570568 kB
Buffers:         29424 kB
Cached:         413424 kB
SwapCached:        444 kB
Active:          89352 kB
Inactive:       355604 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        570316 kB
SwapTotal:     2097136 kB
SwapFree:      2095948 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            13408 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:37:16 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 13532 7 1200.26 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 % |
c |     17215 |  780307  2284226 |  346195   17215   989567    57.5 |  0.039 % |
c ==============================================================================
c [1mFound solution: 4767744[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 |     17378 |  780316  2284247 |  260105   17378   996586    57.3 |  0.039 % |
c |     17478 |  780316  2284247 |  286115   17478  1001832    57.3 |  0.039 % |
c |     17629 |  780316  2284247 |  314727   17629  1007314    57.1 |  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): 0.44 0.80 0.92 2/54 4588
Raw data (stat): 4588 (runsolver) D 4587 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490753260 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.53 0.81 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24226 0 0 0 943 54 0 0 25 0 1 0 490753260 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.001 s]
Raw data (loadavg): 0.60 0.81 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24794 0 0 0 1942 55 0 0 25 0 1 0 490753260 118697984 23259 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28979 23259 603 41 0 28938 0
vsize: 115916
[startup+30.0022 s]
Raw data (loadavg): 0.66 0.82 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24916 0 0 0 2942 56 0 0 25 0 1 0 490753260 119156736 23381 4294967295 134512640 134672761 3221224528 3221223828 134556598 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.002 s]
Raw data (loadavg): 0.71 0.82 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24930 0 0 0 3942 56 0 0 25 0 1 0 490753260 119287808 23395 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29123 23395 603 41 0 29082 0
vsize: 116492
[startup+50.0023 s]
Raw data (loadavg): 0.76 0.83 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24944 0 0 0 4941 56 0 0 25 0 1 0 490753260 119287808 23409 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29123 23409 603 41 0 29082 0
vsize: 116492
[startup+60.0025 s]
Raw data (loadavg): 0.79 0.83 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24959 0 0 0 5941 56 0 0 25 0 1 0 490753260 119287808 23424 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29123 23424 603 41 0 29082 0
vsize: 116492
[startup+70.0042 s]
Raw data (loadavg): 0.83 0.84 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24973 0 0 0 6941 57 0 0 25 0 1 0 490753260 119418880 23438 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29155 23438 603 41 0 29114 0
vsize: 116620
[startup+80.0044 s]
Raw data (loadavg): 0.85 0.84 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24982 0 0 0 7941 57 0 0 25 0 1 0 490753260 119418880 23447 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29155 23447 603 41 0 29114 0
vsize: 116620
[startup+90.0044 s]
Raw data (loadavg): 0.87 0.85 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24992 0 0 0 8941 57 0 0 25 0 1 0 490753260 119418880 23457 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29155 23457 603 41 0 29114 0
vsize: 116620
[startup+100.005 s]
Raw data (loadavg): 0.89 0.85 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 24998 0 0 0 9941 57 0 0 25 0 1 0 490753260 119418880 23463 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29155 23463 603 41 0 29114 0
vsize: 116620
[startup+110.006 s]
Raw data (loadavg): 0.91 0.86 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25007 0 0 0 10941 57 0 0 25 0 1 0 490753260 119549952 23472 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29187 23472 603 41 0 29146 0
vsize: 116748
[startup+120.007 s]
Raw data (loadavg): 0.92 0.86 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25015 0 0 0 11942 57 0 0 25 0 1 0 490753260 119549952 23480 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29187 23480 603 41 0 29146 0
vsize: 116748
[startup+130.007 s]
Raw data (loadavg): 0.93 0.86 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25028 0 0 0 12942 57 0 0 25 0 1 0 490753260 119549952 23493 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29187 23493 603 41 0 29146 0
vsize: 116748
[startup+140.007 s]
Raw data (loadavg): 0.94 0.87 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25034 0 0 0 13942 57 0 0 25 0 1 0 490753260 119668736 23499 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29216 23499 603 41 0 29175 0
vsize: 116864
[startup+150.008 s]
Raw data (loadavg): 0.95 0.87 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25041 0 0 0 14942 57 0 0 25 0 1 0 490753260 119668736 23506 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29216 23506 603 41 0 29175 0
vsize: 116864
[startup+160.009 s]
Raw data (loadavg): 0.96 0.88 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25053 0 0 0 15942 58 0 0 25 0 1 0 490753260 119668736 23518 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29216 23518 603 41 0 29175 0
vsize: 116864
[startup+170.009 s]
Raw data (loadavg): 0.96 0.88 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25066 0 0 0 16942 58 0 0 25 0 1 0 490753260 119799808 23531 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29248 23531 603 41 0 29207 0
vsize: 116992
[startup+180.009 s]
Raw data (loadavg): 0.97 0.88 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25080 0 0 0 17942 58 0 0 25 0 1 0 490753260 119799808 23545 4294967295 134512640 134672761 3221224528 3221223696 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29248 23545 603 41 0 29207 0
vsize: 116992
[startup+190.01 s]
Raw data (loadavg): 0.97 0.89 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25087 0 0 0 18943 58 0 0 25 0 1 0 490753260 119799808 23552 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29248 23552 603 41 0 29207 0
vsize: 116992
[startup+200.01 s]
Raw data (loadavg): 0.98 0.89 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25097 0 0 0 19943 58 0 0 25 0 1 0 490753260 119934976 23562 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29281 23562 603 41 0 29240 0
vsize: 117124
[startup+210.011 s]
Raw data (loadavg): 0.98 0.89 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25106 0 0 0 20943 58 0 0 25 0 1 0 490753260 119934976 23571 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29281 23571 603 41 0 29240 0
vsize: 117124
[startup+220.012 s]
Raw data (loadavg): 0.98 0.90 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25113 0 0 0 21943 58 0 0 25 0 1 0 490753260 119934976 23578 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29281 23578 603 41 0 29240 0
vsize: 117124
[startup+230.013 s]
Raw data (loadavg): 0.98 0.90 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25124 0 0 0 22943 58 0 0 25 0 1 0 490753260 119934976 23589 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29281 23589 603 41 0 29240 0
vsize: 117124
[startup+240.013 s]
Raw data (loadavg): 0.99 0.90 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25136 0 0 0 23943 58 0 0 25 0 1 0 490753260 120057856 23601 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29311 23601 603 41 0 29270 0
vsize: 117244
[startup+250.013 s]
Raw data (loadavg): 0.99 0.90 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25149 0 0 0 24944 58 0 0 25 0 1 0 490753260 120057856 23614 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29311 23614 603 41 0 29270 0
vsize: 117244
[startup+260.014 s]
Raw data (loadavg): 0.99 0.91 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25160 0 0 0 25944 58 0 0 25 0 1 0 490753260 120176640 23625 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29340 23625 603 41 0 29299 0
vsize: 117360
[startup+270.015 s]
Raw data (loadavg): 0.99 0.91 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25172 0 0 0 26944 58 0 0 25 0 1 0 490753260 120176640 23637 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29340 23637 603 41 0 29299 0
vsize: 117360
[startup+280.016 s]
Raw data (loadavg): 0.99 0.91 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25184 0 0 0 27944 58 0 0 25 0 1 0 490753260 120176640 23649 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29340 23649 603 41 0 29299 0
vsize: 117360
[startup+290.016 s]
Raw data (loadavg): 0.99 0.91 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25197 0 0 0 28944 58 0 0 25 0 1 0 490753260 120307712 23662 4294967295 134512640 134672761 3221224528 3221223664 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29372 23662 603 41 0 29331 0
vsize: 117488
[startup+300.016 s]
Raw data (loadavg): 0.99 0.92 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25205 0 0 0 29944 58 0 0 25 0 1 0 490753260 120307712 23670 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29372 23670 603 41 0 29331 0
vsize: 117488
[startup+310.016 s]
Raw data (loadavg): 0.99 0.92 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25228 0 0 0 30944 58 0 0 25 0 1 0 490753260 120885248 23693 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29513 23693 603 41 0 29472 0
vsize: 118052
[startup+320.016 s]
Raw data (loadavg): 0.99 0.92 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25237 0 0 0 31945 58 0 0 25 0 1 0 490753260 120885248 23702 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29513 23702 603 41 0 29472 0
vsize: 118052
[startup+330.018 s]
Raw data (loadavg): 0.99 0.92 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25249 0 0 0 32945 59 0 0 25 0 1 0 490753260 120885248 23714 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29513 23714 603 41 0 29472 0
vsize: 118052
[startup+340.017 s]
Raw data (loadavg): 0.99 0.92 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25274 0 0 0 33945 59 0 0 25 0 1 0 490753260 121008128 23739 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29543 23739 603 41 0 29502 0
vsize: 118172
[startup+350.018 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25282 0 0 0 34945 59 0 0 25 0 1 0 490753260 121008128 23747 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29543 23747 603 41 0 29502 0
vsize: 118172
[startup+360.018 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25294 0 0 0 35945 59 0 0 25 0 1 0 490753260 121008128 23759 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29543 23759 603 41 0 29502 0
vsize: 118172
[startup+370.018 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25306 0 0 0 36945 59 0 0 25 0 1 0 490753260 121131008 23771 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29573 23771 603 41 0 29532 0
vsize: 118292
[startup+380.019 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25316 0 0 0 37945 59 0 0 25 0 1 0 490753260 121131008 23781 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29573 23781 603 41 0 29532 0
vsize: 118292
[startup+390.019 s]
Raw data (loadavg): 0.99 0.93 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25327 0 0 0 38946 59 0 0 25 0 1 0 490753260 121131008 23792 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29573 23792 603 41 0 29532 0
vsize: 118292
[startup+400.021 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25336 0 0 0 39946 59 0 0 25 0 1 0 490753260 121262080 23801 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29605 23801 603 41 0 29564 0
vsize: 118420
[startup+410.02 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25349 0 0 0 40946 59 0 0 25 0 1 0 490753260 121262080 23814 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29605 23814 603 41 0 29564 0
vsize: 118420
[startup+420.021 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25357 0 0 0 41946 59 0 0 25 0 1 0 490753260 121262080 23822 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29605 23822 603 41 0 29564 0
vsize: 118420
[startup+430.022 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25365 0 0 0 42946 59 0 0 25 0 1 0 490753260 121397248 23830 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29638 23830 603 41 0 29597 0
vsize: 118552
[startup+440.021 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25375 0 0 0 43947 59 0 0 25 0 1 0 490753260 121397248 23840 4294967295 134512640 134672761 3221224528 3221223696 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29638 23840 603 41 0 29597 0
vsize: 118552
[startup+450.022 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25386 0 0 0 44947 59 0 0 25 0 1 0 490753260 121397248 23851 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29638 23851 603 41 0 29597 0
vsize: 118552
[startup+460.022 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25396 0 0 0 45947 59 0 0 25 0 1 0 490753260 121532416 23861 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29671 23861 603 41 0 29630 0
vsize: 118684
[startup+470.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25407 0 0 0 46947 59 0 0 25 0 1 0 490753260 121532416 23872 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29671 23872 603 41 0 29630 0
vsize: 118684
[startup+480.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25420 0 0 0 47947 59 0 0 25 0 1 0 490753260 121532416 23885 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29671 23885 603 41 0 29630 0
vsize: 118684
[startup+490.022 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25423 0 0 0 48947 59 0 0 25 0 1 0 490753260 121532416 23888 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29671 23888 603 41 0 29630 0
vsize: 118684
[startup+500.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25434 0 0 0 49947 59 0 0 25 0 1 0 490753260 121663488 23899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29703 23899 603 41 0 29662 0
vsize: 118812
[startup+510.023 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25444 0 0 0 50947 59 0 0 25 0 1 0 490753260 121663488 23909 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29703 23909 603 41 0 29662 0
vsize: 118812
[startup+520.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25453 0 0 0 51948 59 0 0 25 0 1 0 490753260 121663488 23918 4294967295 134512640 134672761 3221224528 3221223664 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29703 23918 603 41 0 29662 0
vsize: 118812
[startup+530.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25460 0 0 0 52948 59 0 0 25 0 1 0 490753260 121663488 23925 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29703 23925 603 41 0 29662 0
vsize: 118812
[startup+540.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25468 0 0 0 53948 60 0 0 25 0 1 0 490753260 121794560 23933 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29735 23933 603 41 0 29694 0
vsize: 118940
[startup+550.025 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25478 0 0 0 54948 60 0 0 25 0 1 0 490753260 121794560 23943 4294967295 134512640 134672761 3221224528 3221223632 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29735 23943 603 41 0 29694 0
vsize: 118940
[startup+560.024 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25489 0 0 0 55948 60 0 0 25 0 1 0 490753260 121937920 23954 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29770 23954 603 41 0 29729 0
vsize: 119080
[startup+570.026 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25501 0 0 0 56948 60 0 0 25 0 1 0 490753260 121937920 23966 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29770 23966 603 41 0 29729 0
vsize: 119080
[startup+580.026 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25515 0 0 0 57948 60 0 0 25 0 1 0 490753260 121937920 23980 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29770 23980 603 41 0 29729 0
vsize: 119080
[startup+590.025 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25524 0 0 0 58949 60 0 0 25 0 1 0 490753260 122068992 23989 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29802 23989 603 41 0 29761 0
vsize: 119208
[startup+600.026 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25534 0 0 0 59949 60 0 0 25 0 1 0 490753260 122068992 23999 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29802 23999 603 41 0 29761 0
vsize: 119208
[startup+610.026 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25541 0 0 0 60949 60 0 0 25 0 1 0 490753260 122068992 24006 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29802 24006 603 41 0 29761 0
vsize: 119208
[startup+620.027 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25550 0 0 0 61949 60 0 0 25 0 1 0 490753260 122068992 24015 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29802 24015 603 41 0 29761 0
vsize: 119208
[startup+630.027 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25558 0 0 0 62949 60 0 0 25 0 1 0 490753260 122200064 24023 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29834 24023 603 41 0 29793 0
vsize: 119336
[startup+640.028 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25569 0 0 0 63949 60 0 0 25 0 1 0 490753260 122200064 24034 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29834 24034 603 41 0 29793 0
vsize: 119336
[startup+650.028 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25577 0 0 0 64950 60 0 0 25 0 1 0 490753260 122200064 24042 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29834 24042 603 41 0 29793 0
vsize: 119336
[startup+660.028 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25587 0 0 0 65950 60 0 0 25 0 1 0 490753260 122331136 24052 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29866 24052 603 41 0 29825 0
vsize: 119464
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25601 0 0 0 66950 60 0 0 25 0 1 0 490753260 122331136 24066 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29866 24066 603 41 0 29825 0
vsize: 119464
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25611 0 0 0 67950 60 0 0 25 0 1 0 490753260 122331136 24076 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29866 24076 603 41 0 29825 0
vsize: 119464
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25623 0 0 0 68950 60 0 0 25 0 1 0 490753260 122462208 24088 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29898 24088 603 41 0 29857 0
vsize: 119592
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25634 0 0 0 69950 60 0 0 25 0 1 0 490753260 122462208 24099 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29898 24099 603 41 0 29857 0
vsize: 119592
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25641 0 0 0 70950 60 0 0 25 0 1 0 490753260 122462208 24106 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29898 24106 603 41 0 29857 0
vsize: 119592
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25649 0 0 0 71950 60 0 0 25 0 1 0 490753260 122462208 24114 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29898 24114 603 41 0 29857 0
vsize: 119592
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25658 0 0 0 72951 60 0 0 25 0 1 0 490753260 122589184 24123 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29929 24123 603 41 0 29888 0
vsize: 119716
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25671 0 0 0 73951 60 0 0 25 0 1 0 490753260 122589184 24136 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29929 24136 603 41 0 29888 0
vsize: 119716
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25683 0 0 0 74951 60 0 0 25 0 1 0 490753260 122589184 24148 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29929 24148 603 41 0 29888 0
vsize: 119716
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25694 0 0 0 75951 60 0 0 25 0 1 0 490753260 122720256 24159 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29961 24159 603 41 0 29920 0
vsize: 119844
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25703 0 0 0 76951 61 0 0 25 0 1 0 490753260 122720256 24168 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29961 24168 603 41 0 29920 0
vsize: 119844
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25713 0 0 0 77952 61 0 0 25 0 1 0 490753260 122720256 24178 4294967295 134512640 134672761 3221224528 3221223632 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29961 24178 603 41 0 29920 0
vsize: 119844
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25722 0 0 0 78952 61 0 0 25 0 1 0 490753260 122847232 24187 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29992 24187 603 41 0 29951 0
vsize: 119968
[startup+800.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25730 0 0 0 79951 61 0 0 25 0 1 0 490753260 122847232 24195 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29992 24195 603 41 0 29951 0
vsize: 119968
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25741 0 0 0 80951 61 0 0 25 0 1 0 490753260 122847232 24206 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29992 24206 603 41 0 29951 0
vsize: 119968
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25751 0 0 0 81951 61 0 0 25 0 1 0 490753260 122978304 24216 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30024 24216 603 41 0 29983 0
vsize: 120096
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25762 0 0 0 82952 61 0 0 25 0 1 0 490753260 122978304 24227 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30024 24227 603 41 0 29983 0
vsize: 120096
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25772 0 0 0 83951 62 0 0 25 0 1 0 490753260 122978304 24237 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30024 24237 603 41 0 29983 0
vsize: 120096
[startup+850.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25783 0 0 0 84952 62 0 0 25 0 1 0 490753260 123113472 24248 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30057 24248 603 41 0 30016 0
vsize: 120228
[startup+860.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25794 0 0 0 85952 62 0 0 25 0 1 0 490753260 123113472 24259 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30057 24259 603 41 0 30016 0
vsize: 120228
[startup+870.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25805 0 0 0 86952 62 0 0 25 0 1 0 490753260 123113472 24270 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30057 24270 603 41 0 30016 0
vsize: 120228
[startup+880.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25817 0 0 0 87952 62 0 0 25 0 1 0 490753260 123244544 24282 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30089 24282 603 41 0 30048 0
vsize: 120356
[startup+890.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25827 0 0 0 88953 62 0 0 25 0 1 0 490753260 123244544 24292 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30089 24292 603 41 0 30048 0
vsize: 120356
[startup+900.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25835 0 0 0 89953 62 0 0 25 0 1 0 490753260 123244544 24300 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30089 24300 603 41 0 30048 0
vsize: 120356
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25843 0 0 0 90953 62 0 0 25 0 1 0 490753260 123244544 24308 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30089 24308 603 41 0 30048 0
vsize: 120356
[startup+920.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25853 0 0 0 91953 62 0 0 25 0 1 0 490753260 123375616 24318 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30121 24318 603 41 0 30080 0
vsize: 120484
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25864 0 0 0 92953 62 0 0 25 0 1 0 490753260 123375616 24329 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30121 24329 603 41 0 30080 0
vsize: 120484
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25879 0 0 0 93953 62 0 0 25 0 1 0 490753260 123510784 24344 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30154 24344 603 41 0 30113 0
vsize: 120616
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25886 0 0 0 94953 62 0 0 25 0 1 0 490753260 123510784 24351 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30154 24351 603 41 0 30113 0
vsize: 120616
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25897 0 0 0 95953 62 0 0 25 0 1 0 490753260 123510784 24362 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30154 24362 603 41 0 30113 0
vsize: 120616
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25907 0 0 0 96953 62 0 0 25 0 1 0 490753260 123510784 24372 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30154 24372 603 41 0 30113 0
vsize: 120616
[startup+980.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25915 0 0 0 97954 62 0 0 25 0 1 0 490753260 123645952 24380 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30187 24380 603 41 0 30146 0
vsize: 120748
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25924 0 0 0 98954 62 0 0 25 0 1 0 490753260 123645952 24389 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30187 24389 603 41 0 30146 0
vsize: 120748
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25934 0 0 0 99954 62 0 0 25 0 1 0 490753260 123645952 24399 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30187 24399 603 41 0 30146 0
vsize: 120748
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25944 0 0 0 100954 62 0 0 25 0 1 0 490753260 123781120 24409 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30220 24409 603 41 0 30179 0
vsize: 120880
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25959 0 0 0 101954 62 0 0 25 0 1 0 490753260 123781120 24424 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30220 24424 603 41 0 30179 0
vsize: 120880
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25966 0 0 0 102954 62 0 0 25 0 1 0 490753260 123781120 24431 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30220 24431 603 41 0 30179 0
vsize: 120880
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25978 0 0 0 103954 62 0 0 25 0 1 0 490753260 123920384 24443 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30254 24443 603 41 0 30213 0
vsize: 121016
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 25991 0 0 0 104954 62 0 0 25 0 1 0 490753260 123920384 24456 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30254 24456 603 41 0 30213 0
vsize: 121016
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26000 0 0 0 105955 62 0 0 25 0 1 0 490753260 123920384 24465 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30254 24465 603 41 0 30213 0
vsize: 121016
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26010 0 0 0 106955 62 0 0 25 0 1 0 490753260 124047360 24475 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30285 24475 603 41 0 30244 0
vsize: 121140
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26023 0 0 0 107955 62 0 0 25 0 1 0 490753260 124047360 24488 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30285 24488 603 41 0 30244 0
vsize: 121140
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26033 0 0 0 108955 62 0 0 25 0 1 0 490753260 124047360 24498 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30285 24498 603 41 0 30244 0
vsize: 121140
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26053 0 0 0 109955 63 0 0 25 0 1 0 490753260 124317696 24518 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30351 24518 603 41 0 30310 0
vsize: 121404
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26054 0 0 0 110955 63 0 0 25 0 1 0 490753260 124317696 24519 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30351 24519 603 41 0 30310 0
vsize: 121404
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26060 0 0 0 111955 63 0 0 25 0 1 0 490753260 124317696 24525 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30351 24525 603 41 0 30310 0
vsize: 121404
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26069 0 0 0 112955 63 0 0 25 0 1 0 490753260 124317696 24534 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30351 24534 603 41 0 30310 0
vsize: 121404
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26075 0 0 0 113956 63 0 0 25 0 1 0 490753260 124317696 24540 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30351 24540 603 41 0 30310 0
vsize: 121404
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26085 0 0 0 114956 63 0 0 25 0 1 0 490753260 124317696 24550 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30351 24550 603 41 0 30310 0
vsize: 121404
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26087 0 0 0 115956 63 0 0 25 0 1 0 490753260 124317696 24552 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30351 24552 603 41 0 30310 0
vsize: 121404
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26098 0 0 0 116956 63 0 0 25 0 1 0 490753260 124452864 24563 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30384 24563 603 41 0 30343 0
vsize: 121536
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26110 0 0 0 117956 63 0 0 25 0 1 0 490753260 124452864 24575 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30384 24575 603 41 0 30343 0
vsize: 121536
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26119 0 0 0 118956 63 0 0 25 0 1 0 490753260 124452864 24584 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30384 24584 603 41 0 30343 0
vsize: 121536
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 4588
Raw data (stat): 4588 (minisat+) R 4587 24215 24214 0 -1 0 26125 0 0 0 119956 63 0 0 25 0 1 0 490753260 124583936 24590 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30416 24590 603 41 0 30375 0
vsize: 121664
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 4588
Raw data (stat): 4588 (minisat+) Z 4587 24215 24214 0 -1 12 26128 0 0 0 119957 68 0 0 25 0 1 0 490753260 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.09
CPU time (s): 1200.26
CPU user time (s): 1199.57
CPU system time (s): 0.684895
CPU usage (%): 100.013
Max. virtual memory (Kb): 121664
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####