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/submitted/sorensson/garden/normalized-g15x15.opb
MD5SUM	6a083b86cc55025d2acb3bcf68562064
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	54
Optimality of the best value was proved	NO
Number of terms in the objective function	225
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	225
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	225
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01784
Number of variables	225
Total number of constraints	225
Number of constraints which are clauses	225
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	5
Trace number 6508

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 05:30:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4966 boxname=wulflinc3 idbench=382 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6a083b86cc55025d2acb3bcf68562064  /oldhome/oroussel/tmp/wulflinc3/normalized-g15x15.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc3/normalized-g15x15.opb /oldhome/oroussel/tmp/wulflinc3/normalized-g15x15.opb
IDLAUNCH: 4966
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 2
cpu MHz		: 451.190
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:        836012 kB
Buffers:         36400 kB
Cached:         139232 kB
SwapCached:       3276 kB
Active:          83372 kB
Inactive:        98388 kB
HighTotal:      131008 kB
HighFree:         1092 kB
LowTotal:       903652 kB
LowFree:        834920 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11168 kB
Committed_AS:    71704 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:50:23 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4966 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     225     1065 |      75       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 75[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6660     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15434    36689 |    5144       0        0     nan |  0.000 % |
c |       100 |   15403    36620 |    5658      99      475     4.8 |  0.343 % |
c |       250 |   15348    36498 |    6224     246     1899     7.7 |  0.629 % |
c |       475 |   15348    36498 |    6846     471     4425     9.4 |  0.629 % |
c |       815 |   15319    36433 |    7531     809     7552     9.3 |  0.782 % |
c |      1321 |   15251    36279 |    8284    1307    13715    10.5 |  1.163 % |
c |      2081 |   15098    35933 |    9112    2028    19422     9.6 |  2.040 % |
c |      3223 |   15025    35767 |   10024    3161    38315    12.1 |  2.460 % |
c ==============================================================================
c [1mFound solution: 74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3290 |   15076    35895 |    5025    3228    39197    12.1 |  2.460 % |
c |      3391 |   15076    35895 |    5527    3329    40759    12.2 |  2.472 % |
c ==============================================================================
c [1mFound solution: 73[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3402 |   15018    35758 |    5006    3328    40436    12.2 |  2.472 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3454 |   15060    35865 |    5020    3380    41685    12.3 |  2.472 % |
c |      3556 |   15060    35865 |    5522    3482    42351    12.2 |  2.863 % |
c |      3706 |   15060    35865 |    6074    3632    43921    12.1 |  2.863 % |
c |      3931 |   15060    35865 |    6681    3857    47158    12.2 |  2.863 % |
c |      4268 |   15060    35865 |    7349    4194    51285    12.2 |  2.863 % |
c |      4774 |   15060    35865 |    8084    4700    57479    12.2 |  2.863 % |
c |      5533 |   15060    35865 |    8893    5459    74960    13.7 |  2.863 % |
c |      6672 |   15060    35865 |    9782    6598   101584    15.4 |  2.863 % |
c |      8380 |   15004    35738 |   10760    8282   126303    15.3 |  3.185 % |
c |     10942 |   14948    35613 |   11836   10840   162333    15.0 |  3.469 % |
c ==============================================================================
c [1mFound solution: 71[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11519 |   14911    35522 |    4970   11411   171523    15.0 |  3.469 % |
c |     11619 |   14911    35522 |    5467    2953    29047     9.8 |  3.695 % |
c |     11769 |   14911    35522 |    6013    3103    30613     9.9 |  3.696 % |
c |     11995 |   14884    35461 |    6615    3326    32580     9.8 |  3.847 % |
c |     12332 |   14884    35461 |    7276    3663    36390     9.9 |  3.847 % |
c |     12839 |   14884    35461 |    8004    4170    47440    11.4 |  3.847 % |
c |     13598 |   14846    35374 |    8804    4858    57079    11.7 |  4.093 % |
c |     14737 |   14846    35374 |    9685    5997    96321    16.1 |  4.093 % |
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15775 |   14887    35480 |    4962    7031   112673    16.0 |  4.093 % |
c |     15875 |   14887    35480 |    5458    3616    56429    15.6 |  4.175 % |
c |     16025 |   14887    35480 |    6004    3766    58167    15.4 |  4.175 % |
c |     16251 |   14887    35480 |    6604    3992    60113    15.1 |  4.175 % |
c |     16588 |   14869    35438 |    7264    4313    64170    14.9 |  4.289 % |
c |     17096 |   14869    35438 |    7991    4821    70743    14.7 |  4.289 % |
c ==============================================================================
c [1mFound solution: 69[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17290 |   14820    35317 |    4940    4999    72409    14.5 |  4.289 % |
c |     17391 |   14814    35303 |    5434    5099    73334    14.4 |  4.646 % |
c |     17541 |   14814    35303 |    5977    5249    75506    14.4 |  4.646 % |
c |     17766 |   14814    35303 |    6575    5474    79119    14.5 |  4.646 % |
c |     18104 |   14814    35303 |    7232    5812    85259    14.7 |  4.646 % |
c |     18611 |   14789    35246 |    7955    6317    94963    15.0 |  4.797 % |
c |     19371 |   14789    35246 |    8751    7077   109161    15.4 |  4.797 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19559 |   14831    35353 |    4943    7265   112595    15.5 |  4.797 % |
c |     19659 |   14831    35353 |    5437    3733    41490    11.1 |  4.804 % |
c |     19812 |   14831    35353 |    5981    3886    45043    11.6 |  4.804 % |
c |     20037 |   14831    35353 |    6579    4111    47640    11.6 |  4.804 % |
c |     20375 |   14831    35353 |    7237    4449    50985    11.5 |  4.804 % |
c |     20881 |   14831    35353 |    7960    4955    59937    12.1 |  4.804 % |
c |     21641 |   14831    35353 |    8756    5715    72674    12.7 |  4.804 % |
c |     22781 |   14831    35353 |    9632    6855    87146    12.7 |  4.804 % |
c |     24489 |   14828    35347 |   10595    8562   133698    15.6 |  4.823 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26831 |   14879    35475 |    4959   10904   174207    16.0 |  4.823 % |
c |     26932 |   14879    35475 |    5454    2827    21855     7.7 |  4.827 % |
c |     27083 |   14835    35377 |    6000    2977    23023     7.7 |  5.053 % |
c |     27310 |   14835    35377 |    6600    3204    25747     8.0 |  5.053 % |
c |     27648 |   14835    35377 |    7260    3542    32416     9.2 |  5.053 % |
c |     28157 |   14835    35377 |    7986    4051    40461    10.0 |  5.053 % |
c |     28918 |   14804    35306 |    8785    4781    52022    10.9 |  5.240 % |
c |     30057 |   14804    35306 |    9663    5920    74567    12.6 |  5.241 % |
c |     31765 |   14784    35260 |   10630    7623   101490    13.3 |  5.353 % |
c |     34334 |   14784    35260 |   11693   10192   180223    17.7 |  5.353 % |
c ==============================================================================
c [1mFound solution: 65[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36032 |   14700    35058 |    4900   11206   185768    16.6 |  5.353 % |
c |     36132 |   14700    35058 |    5390    2902    24050     8.3 |  5.896 % |
c |     36282 |   14700    35058 |    5929    3052    26629     8.7 |  5.896 % |
c |     36507 |   14700    35058 |    6521    3277    30473     9.3 |  5.896 % |
c |     36844 |   14677    35007 |    7174    3612    34902     9.7 |  6.008 % |
c |     37350 |   14677    35007 |    7891    4118    43707    10.6 |  6.008 % |
c |     38109 |   14668    34987 |    8680    4876    55335    11.3 |  6.065 % |
c |     39248 |   14619    34877 |    9548    6008    71746    11.9 |  6.346 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40072 |   14659    34980 |    4886    6832    90935    13.3 |  6.346 % |
c |     40173 |   14659    34980 |    5374    3517    33054     9.4 |  6.351 % |
c |     40324 |   14659    34980 |    5912    3668    36678    10.0 |  6.351 % |
c |     40549 |   14659    34980 |    6503    3893    40523    10.4 |  6.351 % |
c |     40887 |   14659    34980 |    7153    4231    45456    10.7 |  6.351 % |
c |     41393 |   14659    34980 |    7868    4737    54163    11.4 |  6.351 % |
c |     42152 |   14659    34980 |    8655    5496    67813    12.3 |  6.351 % |
c |     43291 |   14659    34980 |    9521    6635    89122    13.4 |  6.351 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43945 |   14587    34805 |    4862    7282    97262    13.4 |  6.351 % |
c |     44046 |   14587    34805 |    5348    3742    28787     7.7 |  6.760 % |
c |     44198 |   14587    34805 |    5883    3894    30107     7.7 |  6.761 % |
c |     44423 |   14587    34805 |    6471    4119    33032     8.0 |  6.760 % |
c |     44761 |   14587    34805 |    7118    4457    38913     8.7 |  6.761 % |
c |     45270 |   14587    34805 |    7830    4966    49428    10.0 |  6.760 % |
c |     46030 |   14587    34805 |    8613    5726    64141    11.2 |  6.760 % |
c |     47169 |   14587    34805 |    9474    6865    88353    12.9 |  6.760 % |
c |     48878 |   14587    34805 |   10422    8574   119207    13.9 |  6.760 % |
c |     51440 |   14587    34805 |   11464   11136   200347    18.0 |  6.760 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53762 |   14635    34926 |    4878   13458   267039    19.8 |  6.760 % |
c |     53862 |   14635    34926 |    5365    3465    37013    10.7 |  6.760 % |
c |     54015 |   14635    34926 |    5902    3618    38955    10.8 |  6.760 % |
c |     54242 |   14635    34926 |    6492    3845    41344    10.8 |  6.760 % |
c |     54579 |   14635    34926 |    7141    4182    45250    10.8 |  6.760 % |
c |     55086 |   14635    34926 |    7856    4689    53654    11.4 |  6.760 % |
c |     55845 |   14635    34926 |    8641    5448    73046    13.4 |  6.760 % |
c |     56985 |   14635    34926 |    9505    6588    98564    15.0 |  6.760 % |
c |     58693 |   14635    34926 |   10456    8296   161519    19.5 |  6.760 % |
c |     61255 |   14635    34926 |   11502   10858   241845    22.3 |  6.760 % |
c |     65101 |   14635    34926 |   12652   14704   348915    23.7 |  6.760 % |
c ==============================================================================
c [1mFound solution: 61[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66714 |   14382    34338 |    4794    8951   187629    21.0 |  6.760 % |
c |     66814 |   14382    34338 |    5273    4576    68961    15.1 |  8.232 % |
c |     66964 |   14382    34338 |    5800    4726    70450    14.9 |  8.233 % |
c |     67190 |   14382    34338 |    6380    4952    74763    15.1 |  8.232 % |
c |     67528 |   14382    34338 |    7018    5290    79948    15.1 |  8.232 % |
c |     68034 |   14382    34338 |    7720    5796    90398    15.6 |  8.232 % |
c |     68794 |   14382    34338 |    8492    6556   109341    16.7 |  8.233 % |
c |     69934 |   14382    34338 |    9342    7696   138977    18.1 |  8.232 % |
c |     71642 |   14382    34338 |   10276    9404   188221    20.0 |  8.232 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73717 |   14419    34433 |    4806   11479   223909    19.5 |  8.232 % |
c |     73819 |   14419    34433 |    5286    2972    14812     5.0 |  8.251 % |
c |     73970 |   14419    34433 |    5815    3123    16447     5.3 |  8.251 % |
c |     74195 |   14419    34433 |    6396    3348    20759     6.2 |  8.251 % |
c |     74532 |   14419    34433 |    7036    3685    29129     7.9 |  8.251 % |
c |     75041 |   14419    34433 |    7740    4194    36429     8.7 |  8.252 % |
c |     75803 |   14419    34433 |    8514    4956    48958     9.9 |  8.251 % |
c |     76942 |   14419    34433 |    9365    6095    83624    13.7 |  8.251 % |
c |     78651 |   14419    34433 |   10302    7804   128949    16.5 |  8.251 % |
c |     81213 |   14111    33731 |   11332   10168   194890    19.2 | 10.002 % |
c |     85057 |   14111    33731 |   12465   14012   269519    19.2 | 10.002 % |
c |     90823 |   14111    33731 |   13712   12772   258899    20.3 | 10.003 % |
c |     99472 |   14111    33731 |   15083   12449   269113    21.6 | 10.002 % |
c |    112446 |   14111    33731 |   16591    8437   196167    23.3 | 10.002 % |
c ==============================================================================
c [1mFound solution: 59[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122231 |   14060    33600 |    4686   18221   490219    26.9 | 10.002 % |
c |    122331 |   14060    33600 |    5154    4656    92770    19.9 | 10.315 % |
c |    122481 |   14060    33600 |    5670    4806    95931    20.0 | 10.315 % |
c |    122706 |   14060    33600 |    6237    5031    99277    19.7 | 10.315 % |
c |    123043 |   14060    33600 |    6860    5368   103725    19.3 | 10.315 % |
c |    123550 |   14060    33600 |    7546    5875   109674    18.7 | 10.315 % |
c |    124309 |   14056    33591 |    8301    6632   119829    18.1 | 10.333 % |
c |    125449 |   14056    33591 |    9131    7772   148792    19.1 | 10.333 % |
c |    127159 |   14056    33591 |   10044    9482   202551    21.4 | 10.333 % |
c |    129722 |   14056    33591 |   11049   12045   268165    22.3 | 10.333 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131089 |   14097    33694 |    4699    7390   130190    17.6 | 10.333 % |
c |    131189 |   14097    33694 |    5168    3795    34524     9.1 | 10.360 % |
c |    131340 |   14097    33694 |    5685    3946    37284     9.4 | 10.360 % |
c |    131567 |   14097    33694 |    6254    4173    42406    10.2 | 10.360 % |
c |    131904 |   14097    33694 |    6879    4510    50402    11.2 | 10.361 % |
c |    132413 |   14097    33694 |    7567    5019    58285    11.6 | 10.360 % |
c |    133172 |   14097    33694 |    8324    5778    75702    13.1 | 10.360 % |
c |    134314 |   14072    33637 |    9157    6913   106024    15.3 | 10.509 % |
c |    136023 |   14072    33637 |   10072    8622   141489    16.4 | 10.509 % |
c |    138585 |   14072    33637 |   11079   11184   214635    19.2 | 10.509 % |
c |    142430 |   14072    33637 |   12187    7622   103987    13.6 | 10.509 % |
c |    148200 |   14072    33637 |   13406   13392   232614    17.4 | 10.509 % |
c |    156850 |   13928    33312 |   14747   14106   237275    16.8 | 11.307 % |
c |    169825 |   13928    33312 |   16222    9936   296953    29.9 | 11.307 % |
c ==============================================================================
c [1mFound solution: 57[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    176971 |   13530    32384 |    4510   17051   482760    28.3 | 11.307 % |
c |    177071 |   13530    32384 |    4961    4363    47258    10.8 | 13.586 % |
c |    177221 |   13530    32384 |    5457    4513    49867    11.0 | 13.586 % |
c |    177447 |   13530    32384 |    6002    4739    54428    11.5 | 13.586 % |
c |    177784 |   13530    32384 |    6603    5076    65264    12.9 | 13.586 % |
c |    178291 |   13530    32384 |    7263    5583    80671    14.4 | 13.586 % |
c |    179050 |   13530    32384 |    7989    6342   104190    16.4 | 13.586 % |
c |    180189 |   13530    32384 |    8788    7481   125245    16.7 | 13.586 % |
c |    181897 |   13530    32384 |    9667    9189   174943    19.0 | 13.586 % |
c |    184459 |   13530    32384 |   10634   11751   236150    20.1 | 13.586 % |
c |    188304 |   13530    32384 |   11697    9721   165028    17.0 | 13.586 % |
c |    194072 |   13515    32349 |   12867    8139   166080    20.4 | 13.697 % |
c |    202724 |   13515    32349 |   14154    8750   163736    18.7 | 13.697 % |
c |    215700 |   13515    32349 |   15569   13208   305071    23.1 | 13.697 % |
c |    235162 |   13515    32349 |   17126   13725   402565    29.3 | 13.697 % |
c |    264354 |   13515    32349 |   18839   12540   291735    23.3 | 13.697 % |
c |    308146 |   13515    32349 |   20723   22793   636872    27.9 | 13.697 % |
c |    373830 |   13515    32349 |   22795   17394   576847    33.2 | 13.697 % |
c |    472358 |   13515    32349 |   25075   24082   853289    35.4 | 13.697 % |
c ==============================================================================
c [1mFound solution: 56[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    552878 |   13546    32427 |    4515   19354   716303    37.0 | 13.697 % |
c |    552978 |   13546    32427 |    4966    4939    59901    12.1 | 13.722 % |
c |    553128 |   13546    32427 |    5463    5089    62638    12.3 | 13.722 % |
c |    553353 |   13546    32427 |    6009    5314    68015    12.8 | 13.722 % |
c |    553690 |   13546    32427 |    6610    5651    74436    13.2 | 13.722 % |
c |    554197 |   13546    32427 |    7271    6158    81597    13.3 | 13.722 % |
c |    554958 |   13543    32421 |    7998    6917    95084    13.7 | 13.741 % |
c |    556097 |   13543    32421 |    8798    8056   112055    13.9 | 13.741 % |
c |    557806 |   13543    32421 |    9678    9765   141328    14.5 | 13.741 % |
c |    560369 |   13543    32421 |   10646   12328   247893    20.1 | 13.742 % |
c |    564214 |   13543    32421 |   11710   10009   231740    23.2 | 13.741 % |
c |    569981 |   13498    32317 |   12881    8533   139616    16.4 | 14.019 % |
c |    578630 |   13498    32317 |   14170    9018   204663    22.7 | 14.019 % |
c |    591604 |   13498    32317 |   15587   13673   332849    24.3 | 14.019 % |
c |    611065 |   13498    32317 |   17145   13422   272014    20.3 | 14.019 % |
c |    640257 |   13475    32264 |   18860   12574   291417    23.2 | 14.167 % |
c |    684046 |   13475    32264 |   20746   12731   515262    40.5 | 14.167 % |
c |    749730 |   13465    32241 |   22820   19506   370467    19.0 | 14.222 % |
c |    848256 |   13465    32241 |   25103   16421   446335    27.2 | 14.222 % |
c |    996046 |   13442    32190 |   27613   23536   775466    32.9 | 14.333 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1082042 |   13405    32092 |    4468   29547  1279344    43.3 | 14.333 % |
c |   1082143 |   13405    32092 |    4914    3795    25033     6.6 | 14.606 % |
c |   1082293 |   13405    32092 |    5406    3945    26963     6.8 | 14.606 % |
c |   1082518 |   13405    32092 |    5946    4170    30223     7.2 | 14.606 % |
c |   1082855 |   13405    32092 |    6541    4507    36396     8.1 | 14.606 % |
c |   1083361 |   13405    32092 |    7195    5013    44912     9.0 | 14.606 % |
c |   1084121 |   13405    32092 |    7915    5773    57945    10.0 | 14.606 % |
c |   1085260 |   13405    32092 |    8706    6912    82991    12.0 | 14.606 % |
c |   1086968 |   13405    32092 |    9577    8620   118610    13.8 | 14.606 % |
c |   1089532 |   13405    32092 |   10535    5818    54095     9.3 | 14.606 % |
c |   1093377 |   13405    32092 |   11588    9663   138176    14.3 | 14.606 % |
c |   1099145 |   13405    32092 |   12747    9018   104454    11.6 | 14.606 % |
c |   1107794 |   13394    32066 |   14022   10754   145753    13.6 | 14.698 % |
c |   1120768 |   13394    32066 |   15424   15217   458420    30.1 | 14.698 % |
c |   1140230 |   13394    32066 |   16967   15723   298674    19.0 | 14.698 % |
c |   1169422 |   13394    32066 |   18663   14808   389063    26.3 | 14.698 % |
c |   1213211 |   13394    32066 |   20530   15664   331419    21.2 | 14.698 % |
c |   1278897 |   13394    32066 |   22583   22627  1003724    44.4 | 14.698 % |
#### 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.84 0.94 0.91 2/54 20506
Raw data (stat): 20506 (runsolver) R 20505 10720 10719 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 423858822 1052672 97 4294967295 134512640 135381576 3221224464 3221219904 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1022 0 0 0 995 3 0 0 25 0 1 0 423858822 5894144 999 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1439 999 603 41 0 1398 0
vsize: 5756
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1150 0 0 0 1994 3 0 0 25 0 1 0 423858822 6426624 1127 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1569 1127 603 41 0 1528 0
vsize: 6276
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1353 0 0 0 2994 4 0 0 25 0 1 0 423858822 7225344 1330 4294967295 134512640 134672761 3221224576 3221223728 134565140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1330 603 41 0 1723 0
vsize: 7056
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1353 0 0 0 3994 4 0 0 25 0 1 0 423858822 7225344 1330 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1764 1330 603 41 0 1723 0
vsize: 7056
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1501 0 0 0 4993 4 0 0 25 0 1 0 423858822 7888896 1478 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1926 1478 603 41 0 1885 0
vsize: 7704
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1626 0 0 0 5993 5 0 0 25 0 1 0 423858822 8425472 1603 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2057 1603 603 41 0 2016 0
vsize: 8228
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1721 0 0 0 6992 5 0 0 25 0 1 0 423858822 8826880 1698 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2155 1698 603 41 0 2114 0
vsize: 8620
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1721 0 0 0 7992 5 0 0 25 0 1 0 423858822 8826880 1698 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2155 1698 603 41 0 2114 0
vsize: 8620
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1721 0 0 0 8993 5 0 0 25 0 1 0 423858822 8826880 1698 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2155 1698 603 41 0 2114 0
vsize: 8620
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1799 0 0 0 9992 6 0 0 25 0 1 0 423858822 9093120 1776 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2220 1776 603 41 0 2179 0
vsize: 8880
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1799 0 0 0 10993 6 0 0 25 0 1 0 423858822 9093120 1776 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2220 1776 603 41 0 2179 0
vsize: 8880
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1799 0 0 0 11993 6 0 0 25 0 1 0 423858822 9093120 1776 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2220 1776 603 41 0 2179 0
vsize: 8880
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 1946 0 0 0 12993 6 0 0 25 0 1 0 423858822 9768960 1923 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2385 1923 603 41 0 2344 0
vsize: 9540
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2035 0 0 0 13992 6 0 0 25 0 1 0 423858822 10039296 2012 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2451 2012 603 41 0 2410 0
vsize: 9804
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2069 0 0 0 14993 6 0 0 25 0 1 0 423858822 10174464 2046 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2484 2046 603 41 0 2443 0
vsize: 9936
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2134 0 0 0 15993 7 0 0 25 0 1 0 423858822 10461184 2111 4294967295 134512640 134672761 3221224576 3221223712 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2554 2111 603 41 0 2513 0
vsize: 10216
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2264 0 0 0 16992 7 0 0 25 0 1 0 423858822 11001856 2241 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2686 2241 603 41 0 2645 0
vsize: 10744
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2440 0 0 0 17992 7 0 0 25 0 1 0 423858822 11882496 2417 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2901 2417 603 41 0 2860 0
vsize: 11604
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2471 0 0 0 18992 8 0 0 25 0 1 0 423858822 12021760 2448 4294967295 134512640 134672761 3221224576 3221223712 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2935 2448 603 41 0 2894 0
vsize: 11740
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2483 0 0 0 19992 8 0 0 25 0 1 0 423858822 12021760 2460 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2935 2460 603 41 0 2894 0
vsize: 11740
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2490 0 0 0 20992 8 0 0 25 0 1 0 423858822 12021760 2467 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2935 2467 603 41 0 2894 0
vsize: 11740
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2553 0 0 0 21992 8 0 0 25 0 1 0 423858822 12292096 2530 4294967295 134512640 134672761 3221224576 3221223744 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3001 2530 603 41 0 2960 0
vsize: 12004
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2694 0 0 0 22992 8 0 0 25 0 1 0 423858822 12840960 2671 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3135 2671 603 41 0 3094 0
vsize: 12540
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2715 0 0 0 23992 8 0 0 25 0 1 0 423858822 12976128 2692 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3168 2692 603 41 0 3127 0
vsize: 12672
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2716 0 0 0 24992 8 0 0 25 0 1 0 423858822 12976128 2693 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3168 2693 603 41 0 3127 0
vsize: 12672
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2812 0 0 0 25993 9 0 0 25 0 1 0 423858822 13377536 2789 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3266 2789 603 41 0 3225 0
vsize: 13064
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2828 0 0 0 26993 9 0 0 25 0 1 0 423858822 13512704 2805 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3299 2805 603 41 0 3258 0
vsize: 13196
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 2898 0 0 0 27993 9 0 0 25 0 1 0 423858822 13774848 2875 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2875 603 41 0 3322 0
vsize: 13452
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3025 0 0 0 28992 9 0 0 25 0 1 0 423858822 14311424 3002 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3494 3002 603 41 0 3453 0
vsize: 13976
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3065 0 0 0 29992 9 0 0 25 0 1 0 423858822 14442496 3042 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3526 3042 603 41 0 3485 0
vsize: 14104
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3343 0 0 0 30992 10 0 0 25 0 1 0 423858822 15646720 3320 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3320 603 41 0 3779 0
vsize: 15280
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3350 0 0 0 31992 10 0 0 25 0 1 0 423858822 15646720 3327 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3327 603 41 0 3779 0
vsize: 15280
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3351 0 0 0 32993 10 0 0 25 0 1 0 423858822 15646720 3328 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3328 603 41 0 3779 0
vsize: 15280
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3351 0 0 0 33993 10 0 0 25 0 1 0 423858822 15646720 3328 4294967295 134512640 134672761 3221224576 3221223776 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3328 603 41 0 3779 0
vsize: 15280
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3351 0 0 0 34993 10 0 0 25 0 1 0 423858822 15646720 3328 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3328 603 41 0 3779 0
vsize: 15280
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3351 0 0 0 35993 10 0 0 25 0 1 0 423858822 15646720 3328 4294967295 134512640 134672761 3221224576 3221223728 134542670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3328 603 41 0 3779 0
vsize: 15280
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3351 0 0 0 36993 10 0 0 25 0 1 0 423858822 15646720 3328 4294967295 134512640 134672761 3221224576 3221223720 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3328 603 41 0 3779 0
vsize: 15280
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3353 0 0 0 37994 10 0 0 25 0 1 0 423858822 15646720 3330 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3330 603 41 0 3779 0
vsize: 15280
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3353 0 0 0 38994 10 0 0 25 0 1 0 423858822 15646720 3330 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3330 603 41 0 3779 0
vsize: 15280
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3353 0 0 0 39994 10 0 0 25 0 1 0 423858822 15646720 3330 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3330 603 41 0 3779 0
vsize: 15280
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3353 0 0 0 40994 10 0 0 25 0 1 0 423858822 15646720 3330 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3330 603 41 0 3779 0
vsize: 15280
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3354 0 0 0 41994 10 0 0 25 0 1 0 423858822 15646720 3331 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3331 603 41 0 3779 0
vsize: 15280
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3354 0 0 0 42995 10 0 0 25 0 1 0 423858822 15646720 3331 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3331 603 41 0 3779 0
vsize: 15280
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3354 0 0 0 43995 10 0 0 25 0 1 0 423858822 15646720 3331 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3820 3331 603 41 0 3779 0
vsize: 15280
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3400 0 0 0 44995 10 0 0 25 0 1 0 423858822 15790080 3377 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3377 603 41 0 3814 0
vsize: 15420
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3611 0 0 0 45994 11 0 0 25 0 1 0 423858822 16748544 3588 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3588 603 41 0 4048 0
vsize: 16356
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3619 0 0 0 46995 11 0 0 25 0 1 0 423858822 16748544 3596 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3596 603 41 0 4048 0
vsize: 16356
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3619 0 0 0 47995 11 0 0 25 0 1 0 423858822 16748544 3596 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3596 603 41 0 4048 0
vsize: 16356
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3619 0 0 0 48995 11 0 0 25 0 1 0 423858822 16748544 3596 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3596 603 41 0 4048 0
vsize: 16356
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3619 0 0 0 49995 11 0 0 25 0 1 0 423858822 16748544 3596 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3596 603 41 0 4048 0
vsize: 16356
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3619 0 0 0 50995 11 0 0 25 0 1 0 423858822 16748544 3596 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3596 603 41 0 4048 0
vsize: 16356
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3619 0 0 0 51995 11 0 0 25 0 1 0 423858822 16748544 3596 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3596 603 41 0 4048 0
vsize: 16356
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3619 0 0 0 52995 11 0 0 25 0 1 0 423858822 16748544 3596 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3596 603 41 0 4048 0
vsize: 16356
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3620 0 0 0 53996 11 0 0 25 0 1 0 423858822 16748544 3597 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3597 603 41 0 4048 0
vsize: 16356
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3620 0 0 0 54996 11 0 0 25 0 1 0 423858822 16748544 3597 4294967295 134512640 134672761 3221224576 3221223728 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3597 603 41 0 4048 0
vsize: 16356
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3620 0 0 0 55996 11 0 0 25 0 1 0 423858822 16748544 3597 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3597 603 41 0 4048 0
vsize: 16356
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3620 0 0 0 56996 11 0 0 25 0 1 0 423858822 16748544 3597 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3597 603 41 0 4048 0
vsize: 16356
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3620 0 0 0 57996 11 0 0 25 0 1 0 423858822 16748544 3597 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3597 603 41 0 4048 0
vsize: 16356
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3621 0 0 0 58997 11 0 0 25 0 1 0 423858822 16748544 3598 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3598 603 41 0 4048 0
vsize: 16356
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3621 0 0 0 59997 11 0 0 25 0 1 0 423858822 16748544 3598 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3598 603 41 0 4048 0
vsize: 16356
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3621 0 0 0 60997 11 0 0 25 0 1 0 423858822 16748544 3598 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4089 3598 603 41 0 4048 0
vsize: 16356
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3648 0 0 0 61997 11 0 0 25 0 1 0 423858822 16891904 3625 4294967295 134512640 134672761 3221224576 3221223776 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4124 3625 603 41 0 4083 0
vsize: 16496
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3680 0 0 0 62997 11 0 0 25 0 1 0 423858822 17039360 3657 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4160 3657 603 41 0 4119 0
vsize: 16640
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3684 0 0 0 63997 11 0 0 25 0 1 0 423858822 17039360 3661 4294967295 134512640 134672761 3221224576 3221223504 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4160 3661 603 41 0 4119 0
vsize: 16640
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3690 0 0 0 64997 11 0 0 25 0 1 0 423858822 17039360 3667 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4160 3667 603 41 0 4119 0
vsize: 16640
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3720 0 0 0 65997 11 0 0 25 0 1 0 423858822 17203200 3697 4294967295 134512640 134672761 3221224576 3221223712 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4200 3697 603 41 0 4159 0
vsize: 16800
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3740 0 0 0 66998 11 0 0 25 0 1 0 423858822 17350656 3717 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4236 3717 603 41 0 4195 0
vsize: 16944
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3740 0 0 0 67998 11 0 0 25 0 1 0 423858822 17350656 3717 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4236 3717 603 41 0 4195 0
vsize: 16944
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3775 0 0 0 68998 11 0 0 25 0 1 0 423858822 17514496 3752 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4276 3752 603 41 0 4235 0
vsize: 17104
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3787 0 0 0 69998 11 0 0 25 0 1 0 423858822 17514496 3764 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4276 3764 603 41 0 4235 0
vsize: 17104
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3787 0 0 0 70998 11 0 0 25 0 1 0 423858822 17514496 3764 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4276 3764 603 41 0 4235 0
vsize: 17104
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3797 0 0 0 71998 11 0 0 25 0 1 0 423858822 17661952 3774 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4312 3774 603 41 0 4271 0
vsize: 17248
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3806 0 0 0 72999 11 0 0 25 0 1 0 423858822 17661952 3783 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4312 3783 603 41 0 4271 0
vsize: 17248
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3838 0 0 0 73999 11 0 0 25 0 1 0 423858822 17809408 3815 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3815 603 41 0 4307 0
vsize: 17392
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3879 0 0 0 74998 12 0 0 25 0 1 0 423858822 18104320 3856 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4420 3856 603 41 0 4379 0
vsize: 17680
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3887 0 0 0 75999 12 0 0 25 0 1 0 423858822 18104320 3864 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4420 3864 603 41 0 4379 0
vsize: 17680
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3902 0 0 0 76999 12 0 0 25 0 1 0 423858822 18104320 3879 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4420 3879 603 41 0 4379 0
vsize: 17680
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3913 0 0 0 77999 12 0 0 25 0 1 0 423858822 18268160 3890 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4460 3890 603 41 0 4419 0
vsize: 17840
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3923 0 0 0 78999 12 0 0 25 0 1 0 423858822 18268160 3900 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4460 3900 603 41 0 4419 0
vsize: 17840
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3924 0 0 0 79999 12 0 0 25 0 1 0 423858822 18268160 3901 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4460 3901 603 41 0 4419 0
vsize: 17840
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3924 0 0 0 81000 12 0 0 25 0 1 0 423858822 18268160 3901 4294967295 134512640 134672761 3221224576 3221223712 134560613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4460 3901 603 41 0 4419 0
vsize: 17840
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3949 0 0 0 82000 12 0 0 25 0 1 0 423858822 18407424 3926 4294967295 134512640 134672761 3221224576 3221223728 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3926 603 41 0 4453 0
vsize: 17976
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 3976 0 0 0 83000 12 0 0 25 0 1 0 423858822 18546688 3953 4294967295 134512640 134672761 3221224576 3221223776 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 3953 603 41 0 4487 0
vsize: 18112
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4010 0 0 0 84000 12 0 0 25 0 1 0 423858822 18681856 3987 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4561 3987 603 41 0 4520 0
vsize: 18244
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4055 0 0 0 85000 12 0 0 25 0 1 0 423858822 18821120 4032 4294967295 134512640 134672761 3221224576 3221223576 1075350205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4595 4032 603 41 0 4554 0
vsize: 18380
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4162 0 0 0 86000 12 0 0 25 0 1 0 423858822 19226624 4139 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4694 4139 603 41 0 4653 0
vsize: 18776
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4189 0 0 0 87000 12 0 0 25 0 1 0 423858822 19369984 4166 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4729 4166 603 41 0 4688 0
vsize: 18916
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4193 0 0 0 88000 12 0 0 25 0 1 0 423858822 19369984 4170 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4729 4170 603 41 0 4688 0
vsize: 18916
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4239 0 0 0 89000 13 0 0 25 0 1 0 423858822 19640320 4216 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4795 4216 603 41 0 4754 0
vsize: 19180
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4264 0 0 0 90000 13 0 0 25 0 1 0 423858822 19640320 4241 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4795 4241 603 41 0 4754 0
vsize: 19180
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4278 0 0 0 91000 13 0 0 25 0 1 0 423858822 19779584 4255 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4829 4255 603 41 0 4788 0
vsize: 19316
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4427 0 0 0 92000 13 0 0 25 0 1 0 423858822 20361216 4404 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4404 603 41 0 4930 0
vsize: 19884
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4484 0 0 0 92999 14 0 0 25 0 1 0 423858822 20627456 4461 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5036 4461 603 41 0 4995 0
vsize: 20144
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4485 0 0 0 94000 14 0 0 25 0 1 0 423858822 20627456 4462 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5036 4462 603 41 0 4995 0
vsize: 20144
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4544 0 0 0 95000 14 0 0 25 0 1 0 423858822 20889600 4521 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5100 4521 603 41 0 5059 0
vsize: 20400
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4612 0 0 0 95999 14 0 0 25 0 1 0 423858822 21159936 4589 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5166 4589 603 41 0 5125 0
vsize: 20664
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4612 0 0 0 97000 14 0 0 25 0 1 0 423858822 21159936 4589 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5166 4589 603 41 0 5125 0
vsize: 20664
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 98000 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 99000 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223760 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 100000 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223680 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 101000 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 102000 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 103001 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223680 134555130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 104001 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223712 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 105001 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4655 0 0 0 106001 14 0 0 25 0 1 0 423858822 21291008 4632 4294967295 134512640 134672761 3221224576 3221223712 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4632 603 41 0 5157 0
vsize: 20792
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4656 0 0 0 107001 14 0 0 25 0 1 0 423858822 21291008 4633 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4633 603 41 0 5157 0
vsize: 20792
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4656 0 0 0 108002 14 0 0 25 0 1 0 423858822 21291008 4633 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4633 603 41 0 5157 0
vsize: 20792
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4656 0 0 0 109002 14 0 0 25 0 1 0 423858822 21291008 4633 4294967295 134512640 134672761 3221224576 3221223760 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4633 603 41 0 5157 0
vsize: 20792
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4656 0 0 0 110002 14 0 0 25 0 1 0 423858822 21291008 4633 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4633 603 41 0 5157 0
vsize: 20792
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4657 0 0 0 111002 14 0 0 25 0 1 0 423858822 21291008 4634 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4634 603 41 0 5157 0
vsize: 20792
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4657 0 0 0 112002 14 0 0 25 0 1 0 423858822 21291008 4634 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4634 603 41 0 5157 0
vsize: 20792
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4657 0 0 0 113002 14 0 0 25 0 1 0 423858822 21291008 4634 4294967295 134512640 134672761 3221224576 3221223680 134560150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4634 603 41 0 5157 0
vsize: 20792
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4658 0 0 0 114003 14 0 0 25 0 1 0 423858822 21291008 4635 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4635 603 41 0 5157 0
vsize: 20792
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4658 0 0 0 115003 14 0 0 25 0 1 0 423858822 21291008 4635 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4635 603 41 0 5157 0
vsize: 20792
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4724 0 0 0 116003 14 0 0 25 0 1 0 423858822 21557248 4701 4294967295 134512640 134672761 3221224576 3221223680 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5263 4701 603 41 0 5222 0
vsize: 21052
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4743 0 0 0 117003 14 0 0 25 0 1 0 423858822 21692416 4720 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4720 603 41 0 5255 0
vsize: 21184
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4750 0 0 0 118003 14 0 0 25 0 1 0 423858822 21692416 4727 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5296 4727 603 41 0 5255 0
vsize: 21184
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4760 0 0 0 119003 14 0 0 25 0 1 0 423858822 21852160 4737 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5335 4737 603 41 0 5294 0
vsize: 21340
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20506
Raw data (stat): 20506 (minisat+) R 20505 10720 10719 0 -1 0 4760 0 0 0 120004 14 0 0 25 0 1 0 423858822 21852160 4737 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5335 4737 603 41 0 5294 0
vsize: 21340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 20506
Raw data (stat): 20506 (minisat+) Z 20505 10720 10719 0 -1 12 4763 0 0 0 120004 15 0 0 25 0 1 0 423858822 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.04
CPU time (s): 1200.2
CPU user time (s): 1200.04
CPU system time (s): 0.158975
CPU usage (%): 100.013
Max. virtual memory (Kb): 21340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####