PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	10386fd19d9976c249ce2be861b38a70
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63488
Optimality of the best value was proved	NO
Number of terms in the objective function	180
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	6442450938
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	6442450938
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	1175.12
Number of variables	230
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 16748

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 08:23:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12647 boxname=wulflinc10 idbench=973 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10386fd19d9976c249ce2be861b38a70  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 12647
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        445668 kB
Buffers:         33804 kB
Cached:         532976 kB
SwapCached:          0 kB
Active:         159224 kB
Inactive:       410052 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        445416 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            14088 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 08:43:32 (client local time) WITH STATUS 10 IN 1200.13 SECONDS
stats: 12647 7 1200.13 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> Adder-cost: 304   maxlim: 3240959   bits: 23/22
c ---[   8]---> Adder-cost: 314   maxlim: 3453951   bits: 23/22
c ---[   6]---> Adder-cost: 348   maxlim: 3482623   bits: 23/22
c ---[   4]---> Adder-cost: 318   maxlim: 3294207   bits: 23/22
c ---[   2]---> Adder-cost: 312   maxlim: 3286015   bits: 23/22
c ---[   0]---> Adder-cost: 314   maxlim: 3289087   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   13152    47982 |    3945       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1948          
c   -- var.elim.:  1948/1948          
c   -- var.elim.:  255/255          
c   -- subsuming                       
c   -- var.elim.:  89/89          
c |         0 |   12429    44143 |      --       0       --      -- |     --   | -364/-1112
c |         0 |   12429    44143 |    4971       0        0     nan |  0.000 % |
c |       100 |   12429    44143 |    5468     100      688     6.9 | 15.718 % |
c ==============================================================================
c (current CPU-time: 0.45793 s)
c ==============================================================================
c [1mFound solution: 3053568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  855     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       211 |   14544    49081 |    4363     211     2671    12.7 | 15.718 % |
c   -- subsuming                       
c   -- var.elim.:  810/810          
c   -- var.elim.:  443/443          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  124/124          
c   -- var.elim.:  30/30          
c |       211 |   14219    49850 |      --     211       --      -- |     --   | -325/770
c |       211 |   14219    49850 |    5687     211     2671    12.7 | 15.718 % |
c |       312 |   14219    49850 |    6256     312    17988    57.7 | 13.453 % |
c |       463 |   14219    49850 |    6881     463    31703    68.5 | 13.453 % |
c |       689 |   14219    49850 |    7570     689    70289   102.0 | 13.453 % |
c |      1026 |   14219    49850 |    8327    1026   101311    98.7 | 13.453 % |
c |      1532 |   14219    49850 |    9159    1532   160501   104.8 | 13.453 % |
c |      2292 |   14219    49850 |   10075    2292   235028   102.5 | 13.453 % |
c |      3431 |   14219    49850 |   11083    3431   388676   113.3 | 13.453 % |
c |      5140 |   14219    49850 |   12191    5140   555823   108.1 | 13.453 % |
c |      7702 |   14219    49850 |   13411    7702   935323   121.4 | 13.453 % |
c |     11546 |   14219    49850 |   14752   11546  1409850   122.1 | 13.453 % |
c ==============================================================================
c (current CPU-time: 22.6876 s)
c ==============================================================================
c [1mFound solution: 2376704[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11669 |   14355    50226 |    4306   11669  1423863   122.0 | 13.453 % |
c   -- subsuming                       
c   -- var.elim.:  267/267          
c   -- var.elim.:  132/132          
c |     11669 |   14271    50239 |      --   11669       --      -- |     --   | -84/14
c |     11669 |   14271    50239 |    5708   11669  1423863   122.0 | 13.453 % |
c |     11769 |   14271    50239 |    6279    5287   574571   108.7 | 13.450 % |
c |     11920 |   14271    50239 |    6907    5438   598192   110.0 | 13.450 % |
c |     12145 |   14271    50239 |    7597    5663   619865   109.5 | 13.450 % |
c |     12483 |   14271    50239 |    8357    6001   661431   110.2 | 13.450 % |
c |     12989 |   14271    50239 |    9193    6507   706989   108.7 | 13.450 % |
c |     13748 |   14271    50239 |   10112    7266   782822   107.7 | 13.450 % |
c |     14887 |   14271    50239 |   11124    8405   830794    98.8 | 13.450 % |
c |     16596 |   14271    50239 |   12236   10114  1025259   101.4 | 13.450 % |
c ==============================================================================
c (current CPU-time: 30.9193 s)
c ==============================================================================
c [1mFound solution: 1439744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17069 |   14329    50398 |    4298   10587  1041987    98.4 | 13.450 % |
c   -- subsuming                       
c   -- var.elim.:  124/124          
c   -- var.elim.:  66/66          
c |     17069 |   14305    50596 |      --   10587       --      -- |     --   | -24/199
c |     17069 |   14305    50596 |    5722   10587  1041987    98.4 | 13.450 % |
c |     17169 |   14305    50596 |    6294    4806   323309    67.3 | 13.473 % |
c |     17319 |   14305    50596 |    6923    4956   332289    67.0 | 13.473 % |
c |     17545 |   14305    50596 |    7615    5182   352745    68.1 | 13.473 % |
c |     17883 |   14305    50596 |    8377    5520   392849    71.2 | 13.473 % |
c |     18389 |   14305    50596 |    9215    6026   410638    68.1 | 13.473 % |
c |     19149 |   14305    50596 |   10136    6786   470178    69.3 | 13.473 % |
c |     20289 |   14305    50596 |   11150    7926   530131    66.9 | 13.473 % |
c |     21998 |   14305    50596 |   12265    9635   624905    64.9 | 13.473 % |
c |     24562 |   14259    50082 |   13448   12198   722708    59.2 | 13.511 % |
c |     28406 |   14259    50082 |   14793   11293   522489    46.3 | 13.511 % |
c |     34172 |   14259    50082 |   16273   11914   528669    44.4 | 13.511 % |
c |     42821 |   14211    49880 |   17840   14909   671994    45.1 | 13.744 % |
c ==============================================================================
c (current CPU-time: 63.3104 s)
c ==============================================================================
c [1mFound solution: 1349632[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     50297 |   14234    49943 |    4270   16186   690852    42.7 | 13.744 % |
c   -- subsuming                       
c   -- var.elim.:  123/123          
c   -- var.elim.:  62/62          
c   -- var.elim.:  3/3          
c |     50297 |   14208    49930 |      --   16186       --      -- |     --   | -24/-8
c |     50297 |   14208    49930 |    5683   16184   690790    42.7 | 13.744 % |
c |     50397 |   14208    49930 |    6251    4896   203529    41.6 | 13.965 % |
c |     50547 |   14208    49930 |    6876    5046   207369    41.1 | 13.965 % |
c |     50772 |   14208    49930 |    7564    5271   217531    41.3 | 13.965 % |
c |     51110 |   14208    49930 |    8320    5609   225153    40.1 | 13.965 % |
c |     51617 |   14208    49930 |    9152    6116   238619    39.0 | 13.965 % |
c |     52376 |   14208    49930 |   10068    6875   324522    47.2 | 13.965 % |
c |     53515 |   14208    49930 |   11074    8014   380370    47.5 | 13.965 % |
c |     55223 |   14208    49930 |   12182    9722   462064    47.5 | 13.965 % |
c ==============================================================================
c (current CPU-time: 68.3606 s)
c ==============================================================================
c [1mFound solution: 1114112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     55358 |   14264    50091 |    4279    9857   469189    47.6 | 13.965 % |
c   -- subsuming                       
c   -- var.elim.:  124/124          
c   -- var.elim.:  81/81          
c |     55358 |   14232    50101 |      --    9857       --      -- |     --   | -32/11
c |     55358 |   14232    50101 |    5692    9857   469189    47.6 | 13.965 % |
c |     55459 |   14232    50101 |    6262    4483   214310    47.8 | 13.993 % |
c |     55609 |   14232    50101 |    6888    4633   219009    47.3 | 13.993 % |
c |     55834 |   14232    50101 |    7577    4858   229275    47.2 | 13.993 % |
c |     56171 |   14232    50101 |    8334    5195   237118    45.6 | 13.993 % |
c |     56677 |   14232    50101 |    9168    5701   255178    44.8 | 13.993 % |
c |     57437 |   14232    50101 |   10085    6461   282231    43.7 | 13.993 % |
c |     58577 |   14232    50101 |   11093    7601   327547    43.1 | 13.993 % |
c |     60285 |   14232    50101 |   12203    9309   383224    41.2 | 13.993 % |
c ==============================================================================
c (current CPU-time: 72.8969 s)
c ==============================================================================
c [1mFound solution: 1091584[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     62479 |   14286    50260 |    4285   11503   484638    42.1 | 13.993 % |
c   -- subsuming                       
c   -- var.elim.:  104/104          
c   -- var.elim.:  72/72          
c |     62479 |   14256    50270 |      --   11503       --      -- |     --   | -30/11
c |     62479 |   14256    50270 |    5702   11503   484638    42.1 | 13.993 % |
c |     62579 |   14256    50270 |    6272    5213   177154    34.0 | 14.005 % |
c |     62730 |   14256    50270 |    6899    5364   183255    34.2 | 14.005 % |
c |     62955 |   14256    50270 |    7589    5589   196304    35.1 | 14.005 % |
c |     63293 |   14256    50270 |    8348    5927   208156    35.1 | 14.005 % |
c |     63800 |   14256    50270 |    9183    6434   230618    35.8 | 14.005 % |
c |     64561 |   14256    50270 |   10102    7195   260804    36.2 | 14.005 % |
c |     65700 |   14256    50270 |   11112    8334   309868    37.2 | 14.005 % |
c |     67408 |   14256    50270 |   12223   10042   379759    37.8 | 14.005 % |
c |     69970 |   14256    50270 |   13445   12604   504441    40.0 | 14.005 % |
c |     73815 |   14256    50270 |   14790   11664   562095    48.2 | 14.005 % |
c |     79581 |   14256    50270 |   16269   12228   646047    52.8 | 14.005 % |
c |     88230 |   14256    50270 |   17896   15226   702493    46.1 | 14.005 % |
c |    101205 |   14256    50270 |   19686   14889   944249    63.4 | 14.005 % |
c ==============================================================================
c (current CPU-time: 132.394 s)
c ==============================================================================
c [1mFound solution: 1085440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    112900 |   14304    50412 |    4291   19617  1175865    59.9 | 14.005 % |
c   -- subsuming                       
c   -- var.elim.:  93/93          
c   -- var.elim.:  67/67          
c |    112900 |   14278    50406 |      --   19617       --      -- |     --   | -26/-5
c |    112900 |   14278    50406 |    5711   19617  1175865    59.9 | 14.005 % |
c |    113000 |   14278    50406 |    6282    5564   248740    44.7 | 14.022 % |
c |    113150 |   14278    50406 |    6910    5714   250272    43.8 | 14.022 % |
c |    113376 |   14278    50406 |    7601    5940   260805    43.9 | 14.022 % |
c |    113714 |   14278    50406 |    8361    6278   283190    45.1 | 14.022 % |
c |    114221 |   14278    50406 |    9197    6785   303247    44.7 | 14.022 % |
c |    114980 |   14278    50406 |   10117    7544   336091    44.6 | 14.022 % |
c ==============================================================================
c (current CPU-time: 135.431 s)
c ==============================================================================
c [1mFound solution: 934912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    115741 |   14306    50490 |    4291    8305   377260    45.4 | 14.022 % |
c   -- subsuming                       
c   -- var.elim.:  88/88          
c   -- var.elim.:  82/82          
c   -- var.elim.:  19/19          
c   -- var.elim.:  11/11          
c   -- var.elim.:  20/20          
c |    115741 |   14199    50247 |      --    8305       --      -- |     --   | -70/-96
c |    115741 |   14199    50247 |    5679    7408   281886    38.1 | 14.022 % |
c |    115841 |   14199    50247 |    6247    5039   170645    33.9 | 14.380 % |
c |    115995 |   14199    50247 |    6872    5193   179758    34.6 | 14.380 % |
c |    116220 |   14199    50247 |    7559    5418   190968    35.2 | 14.380 % |
c |    116559 |   14199    50247 |    8315    5757   199420    34.6 | 14.380 % |
c |    117065 |   14199    50247 |    9147    6263   221541    35.4 | 14.380 % |
c |    117824 |   14199    50247 |   10061    7022   247473    35.2 | 14.380 % |
c |    118963 |   14199    50247 |   11067    8161   290223    35.6 | 14.380 % |
c |    120672 |   14182    50154 |   12160    9869   350255    35.5 | 14.457 % |
c |    123236 |   14182    50154 |   13376   12433   484969    39.0 | 14.457 % |
c ==============================================================================
c (current CPU-time: 142.332 s)
c ==============================================================================
c [1mFound solution: 730112[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    123658 |   14219    50270 |    4265   12855   499657    38.9 | 14.457 % |
c   -- subsuming                       
c   -- var.elim.:  125/125          
c   -- var.elim.:  97/97          
c   -- var.elim.:  15/15          
c |    123658 |   14170    50324 |      --   12855       --      -- |     --   | -49/55
c |    123658 |   14170    50324 |    5668   12840   499456    38.9 | 14.457 % |
c |    123759 |   14170    50324 |    6234    5808   209474    36.1 | 14.652 % |
c |    123909 |   14170    50324 |    6858    5958   215622    36.2 | 14.652 % |
c |    124134 |   14170    50324 |    7544    6183   221644    35.8 | 14.652 % |
c |    124474 |   14170    50324 |    8298    6523   233055    35.7 | 14.652 % |
c |    124980 |   14170    50324 |    9128    7029   252621    35.9 | 14.652 % |
c |    125739 |   14170    50324 |   10041    7788   281064    36.1 | 14.652 % |
c |    126879 |   14170    50324 |   11045    8928   323902    36.3 | 14.652 % |
c |    128588 |   14170    50324 |   12149   10637   397003    37.3 | 14.652 % |
c |    131150 |   14170    50324 |   13364    8973   283352    31.6 | 14.652 % |
c |    134995 |   14170    50324 |   14701   12818   457391    35.7 | 14.652 % |
c |    140762 |   14170    50324 |   16171   13470   576250    42.8 | 14.652 % |
c |    149412 |   14170    50324 |   17788   16420   871988    53.1 | 14.652 % |
c |    162387 |   14170    50324 |   19567   17148   901121    52.5 | 14.652 % |
c |    181848 |   14143    50187 |   21483   13229   809485    61.2 | 14.769 % |
c |    211040 |   14134    50152 |   23616   14463   731577    50.6 | 14.808 % |
c |    254831 |   14079    49782 |   25877   13599   732388    53.9 | 15.002 % |
c |    320517 |   14079    49782 |   28464   17581   889976    50.6 | 15.002 % |
c ==============================================================================
c (current CPU-time: 419.67 s)
c ==============================================================================
c [1mFound solution: 719872[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    323037 |   14113    49883 |    4233   20101  1076867    53.6 | 15.002 % |
c   -- subsuming                       
c   -- var.elim.:  145/145          
c   -- var.elim.:  116/116          
c   -- var.elim.:  71/71          
c   -- var.elim.:  16/16          
c   -- var.elim.:  9/9          
c |    323037 |   13931    48823 |      --   20101       --      -- |     --   | -182/-1059
c |    323037 |   13931    48823 |    5572   20076  1073529    53.5 | 15.002 % |
c |    323138 |   13931    48823 |    6129    6050   292049    48.3 | 15.300 % |
c |    323289 |   13931    48823 |    6742    6201   296848    47.9 | 15.300 % |
c |    323515 |   13931    48823 |    7416    6427   304476    47.4 | 15.300 % |
c |    323852 |   13931    48823 |    8158    6764   313830    46.4 | 15.300 % |
c |    324358 |   13931    48823 |    8974    7270   327645    45.1 | 15.300 % |
c |    325118 |   13931    48823 |    9871    8030   356159    44.4 | 15.300 % |
c |    326261 |   13931    48823 |   10859    9173   409371    44.6 | 15.300 % |
c |    327969 |   13931    48823 |   11944   10881   484079    44.5 | 15.300 % |
c |    330532 |   13931    48823 |   13139    9189   340366    37.0 | 15.300 % |
c |    334380 |   13931    48823 |   14453   13037   519853    39.9 | 15.300 % |
c |    340146 |   13931    48823 |   15898   13753   606012    44.1 | 15.300 % |
c |    348795 |   13931    48823 |   17488   11344   503259    44.4 | 15.300 % |
c ==============================================================================
c (current CPU-time: 450.215 s)
c ==============================================================================
c [1mFound solution: 645120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    353355 |   13987    48984 |    4196   15904   692192    43.5 | 15.300 % |
c   -- subsuming                       
c   -- var.elim.:  118/118          
c   -- var.elim.:  72/72          
c |    353355 |   13956    48966 |      --   15904       --      -- |     --   | -31/-17
c |    353355 |   13956    48966 |    5582   15904   692192    43.5 | 15.300 % |
c |    353455 |   13956    48966 |    6140    4813   160374    33.3 | 15.297 % |
c |    353605 |   13956    48966 |    6754    4963   163510    32.9 | 15.297 % |
c |    353830 |   13956    48966 |    7430    5188   168204    32.4 | 15.297 % |
c |    354167 |   13956    48966 |    8173    5525   181010    32.8 | 15.297 % |
c |    354674 |   13956    48966 |    8990    6032   197528    32.7 | 15.297 % |
c |    355433 |   13956    48966 |    9889    6791   219084    32.3 | 15.297 % |
c ==============================================================================
c (current CPU-time: 452.178 s)
c ==============================================================================
c [1mFound solution: 586752[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    355662 |   13981    49052 |    4194    7020   233699    33.3 | 15.297 % |
c   -- subsuming                       
c   -- var.elim.:  66/66          
c   -- var.elim.:  48/48          
c |    355662 |   13967    49030 |      --    7020       --      -- |     --   | -14/-21
c |    355662 |   13967    49030 |    5586    7020   233699    33.3 | 15.297 % |
c |    355763 |   13967    49030 |    6145    4781   137434    28.7 | 15.318 % |
c |    355913 |   13967    49030 |    6760    4931   140243    28.4 | 15.318 % |
c |    356138 |   13967    49030 |    7436    5156   147634    28.6 | 15.318 % |
c |    356477 |   13967    49030 |    8179    5495   163158    29.7 | 15.318 % |
c |    356983 |   13967    49030 |    8997    6001   179260    29.9 | 15.318 % |
c |    357744 |   13967    49030 |    9897    6762   202408    29.9 | 15.318 % |
c |    358883 |   13967    49030 |   10887    7901   239683    30.3 | 15.318 % |
c |    360591 |   13967    49030 |   11975    9609   312804    32.6 | 15.318 % |
c |    363153 |   13967    49030 |   13173   12171   422696    34.7 | 15.318 % |
c |    366997 |   13967    49030 |   14490   11361   391573    34.5 | 15.318 % |
c |    372764 |   13967    49030 |   15939   12116   436879    36.1 | 15.318 % |
c |    381413 |   13967    49030 |   17533   15184   720989    47.5 | 15.318 % |
c ==============================================================================
c (current CPU-time: 488.13 s)
c ==============================================================================
c [1mFound solution: 505856[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    389055 |   13982    49089 |    4194   16738   874844    52.3 | 15.318 % |
c   -- subsuming                       
c   -- var.elim.:  78/78          
c   -- var.elim.:  53/53          
c   -- var.elim.:  44/44          
c   -- var.elim.:  22/22          
c |    389055 |   13827    48417 |      --   16738       --      -- |     --   | -65/-349
c |    389055 |   13827    48417 |    5530   15691   757889    48.3 | 15.318 % |
c |    389155 |   13827    48417 |    6083    4750   179439    37.8 | 15.920 % |
c |    389306 |   13827    48417 |    6692    4901   181811    37.1 | 15.920 % |
c |    389531 |   13827    48417 |    7361    5126   194835    38.0 | 15.920 % |
c |    389869 |   13827    48417 |    8097    5464   203761    37.3 | 15.920 % |
c |    390375 |   13827    48417 |    8907    5970   220801    37.0 | 15.920 % |
c |    391135 |   13827    48417 |    9798    6730   253043    37.6 | 15.920 % |
c |    392274 |   13827    48417 |   10777    7869   297313    37.8 | 15.920 % |
c |    393982 |   13827    48417 |   11855    9577   351251    36.7 | 15.920 % |
c |    396547 |   13816    48368 |   13030   12141   451466    37.2 | 15.959 % |
c |    400391 |   13750    48127 |   14265   11415   400124    35.1 | 16.392 % |
c |    406158 |   13750    48127 |   15692   12097   503090    41.6 | 16.392 % |
c ==============================================================================
c (current CPU-time: 504.044 s)
c ==============================================================================
c [1mFound solution: 416768[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    406504 |   13772    48206 |    4131   12443   522414    42.0 | 16.392 % |
c   -- subsuming                       
c   -- var.elim.:  76/76          
c   -- var.elim.:  63/63          
c   -- var.elim.:  49/49          
c   -- var.elim.:  59/59          
c   -- var.elim.:  11/11          
c |    406504 |   13682    47895 |      --   12443       --      -- |     --   | -90/-310
c |    406504 |   13682    47895 |    5472   10753   372574    34.6 | 16.392 % |
c |    406606 |   13682    47895 |    6020    4882   149374    30.6 | 16.680 % |
c |    406756 |   13682    47895 |    6622    5032   153741    30.6 | 16.680 % |
c |    406981 |   13682    47895 |    7284    5257   157122    29.9 | 16.680 % |
c |    407318 |   13682    47895 |    8012    5594   170896    30.5 | 16.680 % |
c |    407825 |   13682    47895 |    8813    6101   186688    30.6 | 16.680 % |
c |    408585 |   13682    47895 |    9695    6861   214871    31.3 | 16.680 % |
c |    409724 |   13668    47847 |   10654    7998   253597    31.7 | 16.759 % |
c |    411432 |   13668    47847 |   11719    9706   329529    34.0 | 16.759 % |
c |    413995 |   13655    47801 |   12879   12266   427958    34.9 | 16.838 % |
c |    417840 |   13655    47801 |   14167   11623   425850    36.6 | 16.838 % |
c |    423606 |   13655    47801 |   15583   12378   446213    36.0 | 16.838 % |
c |    432255 |   13655    47801 |   17142   15557   608027    39.1 | 16.838 % |
c ==============================================================================
c (current CPU-time: 542.168 s)
c ==============================================================================
c [1mFound solution: 395264[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    444125 |   13741    48016 |    4122   15436   674235    43.7 | 16.838 % |
c   -- subsuming                       
c   -- var.elim.:  169/169          
c   -- var.elim.:  108/108          
c   -- var.elim.:  15/15          
c |    444125 |   13670    47900 |      --   15436       --      -- |     --   | -71/-115
c |    444125 |   13670    47900 |    5468   14790   625455    42.3 | 16.838 % |
c |    444225 |   13670    47900 |    6014    4483   153449    34.2 | 16.930 % |
c |    444375 |   13670    47900 |    6616    4633   158140    34.1 | 16.930 % |
c |    444601 |   13670    47900 |    7277    4859   161964    33.3 | 16.930 % |
c |    444938 |   13670    47900 |    8005    5196   167443    32.2 | 16.930 % |
c |    445444 |   13670    47900 |    8806    5702   187479    32.9 | 16.930 % |
c |    446203 |   13670    47900 |    9686    6461   216905    33.6 | 16.930 % |
c |    447343 |   13670    47900 |   10655    7601   258812    34.0 | 16.930 % |
c |    449052 |   13670    47900 |   11721    9310   319083    34.3 | 16.930 % |
c |    451614 |   13670    47900 |   12893   11872   462516    39.0 | 16.930 % |
c ==============================================================================
c (current CPU-time: 549.248 s)
c ==============================================================================
c [1mFound solution: 392192[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
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    451852 |   13716    48034 |    4114   12110   483502    39.9 | 16.930 % |
c   -- subsuming                       
c   -- var.elim.:  88/88          
c   -- var.elim.:  67/67          
c   -- var.elim.:  31/31          
c |    451852 |   13641    47770 |      --   12110       --      -- |     --   | -75/-263
c |    451852 |   13641    47770 |    5456   12051   478275    39.7 | 16.930 % |
c |    451952 |   13641    47770 |    6002    5456   215790    39.6 | 17.010 % |
c |    452103 |   13641    47770 |    6602    5607   219280    39.1 | 17.010 % |
c |    452328 |   13641    47770 |    7262    5832   225041    38.6 | 17.010 % |
c |    452665 |   13641    47770 |    7988    6169   236550    38.3 | 17.010 % |
c |    453173 |   13641    47770 |    8787    6677   251716    37.7 | 17.010 % |
c |    453934 |   13641    47770 |    9666    7438   280924    37.8 | 17.010 % |
c |    455075 |   13641    47770 |   10632    8579   326590    38.1 | 17.010 % |
c |    456783 |   13641    47770 |   11696   10287   392700    38.2 | 17.010 % |
c |    459345 |   13641    47770 |   12865    8761   290098    33.1 | 17.010 % |
c |    463189 |   13641    47770 |   14152   12605   575879    45.7 | 17.010 % |
c |    468956 |   13641    47770 |   15567   13338   715647    53.7 | 17.010 % |
c |    477605 |   13641    47770 |   17124   11195   530477    47.4 | 17.010 % |
c |    490581 |   13641    47770 |   18836   12239   606057    49.5 | 17.010 % |
c |    5#### 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.55 0.86 0.88 2/54 27998
Raw data (stat): 27998 (runsolver) R 27997 25347 25346 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 485397835 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024803 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99933 s]
Raw data (loadavg): 0.62 0.87 0.88 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 1794 0 0 0 994 4 0 0 25 0 1 0 485397835 8327168 1655 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2033 1655 603 41 0 1992 0
vsize: 8132
[startup+19.9989 s]
Raw data (loadavg): 0.68 0.87 0.88 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2434 0 0 0 1992 6 0 0 25 0 1 0 485397835 10960896 2295 4294967295 134512640 134672761 3221224528 3221223712 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2676 2295 603 41 0 2635 0
vsize: 10704
[startup+29.9996 s]
Raw data (loadavg): 0.72 0.87 0.88 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2717 0 0 0 2991 8 0 0 25 0 1 0 485397835 11923456 2543 4294967295 134512640 134672761 3221224528 3221223568 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2911 2543 603 41 0 2870 0
vsize: 11644
[startup+39.9991 s]
Raw data (loadavg): 0.77 0.88 0.88 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2742 0 0 0 3991 8 0 0 25 0 1 0 485397835 11747328 2502 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2868 2502 603 41 0 2827 0
vsize: 11472
[startup+49.9997 s]
Raw data (loadavg): 0.80 0.88 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2744 0 0 0 4991 8 0 0 25 0 1 0 485397835 11747328 2504 4294967295 134512640 134672761 3221224528 3221223568 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2868 2504 603 41 0 2827 0
vsize: 11472
[startup+59.9993 s]
Raw data (loadavg): 0.83 0.88 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2763 0 0 0 5990 9 0 0 25 0 1 0 485397835 11878400 2523 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2900 2523 603 41 0 2859 0
vsize: 11600
[startup+69.9988 s]
Raw data (loadavg): 0.86 0.89 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2844 0 0 0 6989 10 0 0 25 0 1 0 485397835 11943936 2552 4294967295 134512640 134672761 3221224528 3221223712 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2916 2552 603 41 0 2875 0
vsize: 11664
[startup+79.9994 s]
Raw data (loadavg): 0.88 0.89 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 7989 10 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223568 134612832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+89.999 s]
Raw data (loadavg): 0.90 0.89 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 8989 11 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+99.9995 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 9988 11 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223568 134614239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+110 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2883 0 0 0 10988 11 0 0 25 0 1 0 485397835 11943936 2554 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+120 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 2933 0 0 0 11988 12 0 0 25 0 1 0 485397835 12206080 2604 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2980 2604 603 41 0 2939 0
vsize: 11920
[startup+129.999 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3089 0 0 0 12987 13 0 0 25 0 1 0 485397835 12828672 2760 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3132 2760 603 41 0 3091 0
vsize: 12528
[startup+139.999 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3193 0 0 0 13987 13 0 0 25 0 1 0 485397835 12820480 2768 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3130 2768 603 41 0 3089 0
vsize: 12520
[startup+150 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 14986 14 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2766 603 41 0 3087 0
vsize: 12512
[startup+160 s]
Raw data (loadavg): 0.97 0.91 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 15986 14 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2766 603 41 0 3087 0
vsize: 12512
[startup+169.999 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 16986 15 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2766 603 41 0 3087 0
vsize: 12512
[startup+179.999 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 17985 15 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2766 603 41 0 3087 0
vsize: 12512
[startup+190 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 18985 15 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2766 603 41 0 3087 0
vsize: 12512
[startup+200 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 19985 16 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223712 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2766 603 41 0 3087 0
vsize: 12512
[startup+210 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3248 0 0 0 20985 16 0 0 25 0 1 0 485397835 12812288 2766 4294967295 134512640 134672761 3221224528 3221223664 134614513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2766 603 41 0 3087 0
vsize: 12512
[startup+220 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3293 0 0 0 21985 16 0 0 25 0 1 0 485397835 13041664 2811 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3184 2811 603 41 0 3143 0
vsize: 12736
[startup+230 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3513 0 0 0 22985 17 0 0 25 0 1 0 485397835 13930496 3031 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3401 3031 603 41 0 3360 0
vsize: 13604
[startup+239.999 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3513 0 0 0 23984 17 0 0 25 0 1 0 485397835 13930496 3031 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3401 3031 603 41 0 3360 0
vsize: 13604
[startup+250 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3527 0 0 0 24984 17 0 0 25 0 1 0 485397835 13991936 3044 4294967295 134512640 134672761 3221224528 3221223728 134610705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3416 3044 603 41 0 3375 0
vsize: 13664
[startup+260.001 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3527 0 0 0 25984 18 0 0 25 0 1 0 485397835 13991936 3044 4294967295 134512640 134672761 3221224528 3221223712 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3416 3044 603 41 0 3375 0
vsize: 13664
[startup+270.001 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3527 0 0 0 26984 18 0 0 25 0 1 0 485397835 13991936 3044 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3416 3044 603 41 0 3375 0
vsize: 13664
[startup+280.001 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3529 0 0 0 27984 18 0 0 25 0 1 0 485397835 13983744 3045 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3414 3045 603 41 0 3373 0
vsize: 13656
[startup+290 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3530 0 0 0 28984 18 0 0 25 0 1 0 485397835 13983744 3046 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3414 3046 603 41 0 3373 0
vsize: 13656
[startup+300 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3530 0 0 0 29984 18 0 0 25 0 1 0 485397835 13983744 3046 4294967295 134512640 134672761 3221224528 3221223672 134616132 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3414 3046 603 41 0 3373 0
vsize: 13656
[startup+309.999 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3530 0 0 0 30984 18 0 0 25 0 1 0 485397835 13983744 3046 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3414 3046 603 41 0 3373 0
vsize: 13656
[startup+319.999 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3564 0 0 0 31985 18 0 0 25 0 1 0 485397835 14127104 3079 4294967295 134512640 134672761 3221224528 3221223712 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3449 3079 603 41 0 3408 0
vsize: 13796
[startup+330 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3564 0 0 0 32985 18 0 0 25 0 1 0 485397835 14127104 3079 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3449 3079 603 41 0 3408 0
vsize: 13796
[startup+339.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3751 0 0 0 33985 18 0 0 25 0 1 0 485397835 14880768 3266 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 3266 603 41 0 3592 0
vsize: 14532
[startup+349.998 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3758 0 0 0 34985 18 0 0 25 0 1 0 485397835 15015936 3273 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3666 3273 603 41 0 3625 0
vsize: 14664
[startup+359.998 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 35985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3325 603 41 0 3651 0
vsize: 14768
[startup+369.998 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 36985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3325 603 41 0 3651 0
vsize: 14768
[startup+379.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 37985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3325 603 41 0 3651 0
vsize: 14768
[startup+389.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3810 0 0 0 38985 18 0 0 25 0 1 0 485397835 15122432 3325 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3692 3325 603 41 0 3651 0
vsize: 14768
[startup+399.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3875 0 0 0 39985 19 0 0 25 0 1 0 485397835 15388672 3390 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3757 3390 603 41 0 3716 0
vsize: 15028
[startup+409.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 3875 0 0 0 40985 19 0 0 25 0 1 0 485397835 15388672 3390 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3757 3390 603 41 0 3716 0
vsize: 15028
[startup+419.996 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4013 0 0 0 41985 19 0 0 25 0 1 0 485397835 15544320 3433 4294967295 134512640 134672761 3221224528 3221223784 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3795 3433 603 41 0 3754 0
vsize: 15180
[startup+429.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4019 0 0 0 42984 19 0 0 25 0 1 0 485397835 15740928 3439 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3439 603 41 0 3802 0
vsize: 15372
[startup+439.997 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4037 0 0 0 43985 19 0 0 25 0 1 0 485397835 15740928 3457 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3457 603 41 0 3802 0
vsize: 15372
[startup+449.996 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4037 0 0 0 44985 19 0 0 25 0 1 0 485397835 15740928 3457 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3457 603 41 0 3802 0
vsize: 15372
[startup+459.997 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4063 0 0 0 45984 20 0 0 25 0 1 0 485397835 15740928 3470 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3470 603 41 0 3802 0
vsize: 15372
[startup+469.996 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4063 0 0 0 46984 20 0 0 25 0 1 0 485397835 15740928 3470 4294967295 134512640 134672761 3221224528 3221223664 134614524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3470 603 41 0 3802 0
vsize: 15372
[startup+479.996 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4063 0 0 0 47984 20 0 0 25 0 1 0 485397835 15740928 3470 4294967295 134512640 134672761 3221224528 3221223712 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3470 603 41 0 3802 0
vsize: 15372
[startup+489.995 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 48984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3471 603 41 0 3802 0
vsize: 15372
[startup+499.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 49984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3471 603 41 0 3802 0
vsize: 15372
[startup+509.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 50983 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3471 603 41 0 3802 0
vsize: 15372
[startup+519.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 51984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223728 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3471 603 41 0 3802 0
vsize: 15372
[startup+529.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 52984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3471 603 41 0 3802 0
vsize: 15372
[startup+539.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4064 0 0 0 53984 20 0 0 25 0 1 0 485397835 15740928 3471 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3471 603 41 0 3802 0
vsize: 15372
[startup+549.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 54982 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+559.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 55981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+569.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 56981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 57981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+589.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 58981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+599.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 59981 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+609.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 60982 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+619.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4065 0 0 0 61982 21 0 0 25 0 1 0 485397835 15740928 3472 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3472 603 41 0 3802 0
vsize: 15372
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 62981 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615591 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3474 603 41 0 3802 0
vsize: 15372
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 63981 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3474 603 41 0 3802 0
vsize: 15372
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 64980 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3474 603 41 0 3802 0
vsize: 15372
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 65980 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3843 3474 603 41 0 3802 0
vsize: 15372
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4067 0 0 0 66979 22 0 0 25 0 1 0 485397835 15740928 3474 4294967295 134512640 134672761 3221224528 3221223568 134603510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3474 603 41 0 3802 0
vsize: 15372
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 67979 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3475 603 41 0 3802 0
vsize: 15372
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 68980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3475 603 41 0 3802 0
vsize: 15372
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 69980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3475 603 41 0 3802 0
vsize: 15372
[startup+710.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 70980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3475 603 41 0 3802 0
vsize: 15372
[startup+720.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 71980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3475 603 41 0 3802 0
vsize: 15372
[startup+730.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4068 0 0 0 72980 22 0 0 25 0 1 0 485397835 15740928 3475 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3843 3475 603 41 0 3802 0
vsize: 15372
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4078 0 0 0 73980 22 0 0 25 0 1 0 485397835 15810560 3485 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3860 3485 603 41 0 3819 0
vsize: 15440
[startup+750.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4148 0 0 0 74980 23 0 0 25 0 1 0 485397835 16093184 3554 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3554 603 41 0 3888 0
vsize: 15716
[startup+760.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4148 0 0 0 75981 23 0 0 25 0 1 0 485397835 16093184 3554 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3554 603 41 0 3888 0
vsize: 15716
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 76981 23 0 0 25 0 1 0 485397835 16306176 3606 4294967295 134512640 134672761 3221224528 3221223560 134612937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3981 3606 603 41 0 3940 0
vsize: 15924
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 77981 23 0 0 25 0 1 0 485397835 16306176 3606 4294967295 134512640 134672761 3221224528 3221223712 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3981 3606 603 41 0 3940 0
vsize: 15924
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 78981 23 0 0 25 0 1 0 485397835 16302080 3605 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3980 3605 603 41 0 3939 0
vsize: 15920
[startup+800.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4200 0 0 0 79981 23 0 0 25 0 1 0 485397835 16302080 3605 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3980 3605 603 41 0 3939 0
vsize: 15920
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4223 0 0 0 80981 23 0 0 25 0 1 0 485397835 16396288 3628 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4003 3628 603 41 0 3962 0
vsize: 16012
[startup+820.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4223 0 0 0 81982 23 0 0 25 0 1 0 485397835 16396288 3628 4294967295 134512640 134672761 3221224528 3221223712 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4003 3628 603 41 0 3962 0
vsize: 16012
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4278 0 0 0 82981 23 0 0 25 0 1 0 485397835 16666624 3683 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4069 3683 603 41 0 4028 0
vsize: 16276
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4358 0 0 0 83981 23 0 0 25 0 1 0 485397835 16945152 3762 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4137 3762 603 41 0 4096 0
vsize: 16548
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4358 0 0 0 84982 23 0 0 25 0 1 0 485397835 16945152 3762 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4137 3762 603 41 0 4096 0
vsize: 16548
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4376 0 0 0 85982 23 0 0 25 0 1 0 485397835 17018880 3780 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3780 603 41 0 4114 0
vsize: 16620
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4376 0 0 0 86982 23 0 0 25 0 1 0 485397835 17018880 3780 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3780 603 41 0 4114 0
vsize: 16620
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4405 0 0 0 87982 23 0 0 25 0 1 0 485397835 17125376 3809 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4181 3809 603 41 0 4140 0
vsize: 16724
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4405 0 0 0 88982 23 0 0 25 0 1 0 485397835 17125376 3809 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4181 3809 603 41 0 4140 0
vsize: 16724
[startup+900.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4504 0 0 0 89982 24 0 0 25 0 1 0 485397835 17526784 3907 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4279 3907 603 41 0 4238 0
vsize: 17116
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4504 0 0 0 90982 24 0 0 25 0 1 0 485397835 17526784 3907 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4279 3907 603 41 0 4238 0
vsize: 17116
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4504 0 0 0 91983 24 0 0 25 0 1 0 485397835 17526784 3907 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4279 3907 603 41 0 4238 0
vsize: 17116
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4761 0 0 0 92982 25 0 0 25 0 1 0 485397835 18579456 4164 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4536 4164 603 41 0 4495 0
vsize: 18144
[startup+940.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4793 0 0 0 93982 25 0 0 25 0 1 0 485397835 18710528 4196 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4568 4196 603 41 0 4527 0
vsize: 18272
[startup+950.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4793 0 0 0 94982 25 0 0 25 0 1 0 485397835 18710528 4196 4294967295 134512640 134672761 3221224528 3221223728 134610630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4568 4196 603 41 0 4527 0
vsize: 18272
[startup+960.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4806 0 0 0 95982 25 0 0 25 0 1 0 485397835 18759680 4208 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4580 4208 603 41 0 4539 0
vsize: 18320
[startup+970.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4806 0 0 0 96982 25 0 0 25 0 1 0 485397835 18759680 4208 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4580 4208 603 41 0 4539 0
vsize: 18320
[startup+980.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4806 0 0 0 97983 25 0 0 25 0 1 0 485397835 18759680 4208 4294967295 134512640 134672761 3221224528 3221223712 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4580 4208 603 41 0 4539 0
vsize: 18320
[startup+990.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4815 0 0 0 98983 25 0 0 25 0 1 0 485397835 18792448 4216 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4216 603 41 0 4547 0
vsize: 18352
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4815 0 0 0 99983 25 0 0 25 0 1 0 485397835 18792448 4216 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4216 603 41 0 4547 0
vsize: 18352
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4815 0 0 0 100983 25 0 0 25 0 1 0 485397835 18792448 4216 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4216 603 41 0 4547 0
vsize: 18352
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4824 0 0 0 101983 25 0 0 25 0 1 0 485397835 18825216 4224 4294967295 134512640 134672761 3221224528 3221223712 134615945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4596 4224 603 41 0 4555 0
vsize: 18384
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4824 0 0 0 102984 25 0 0 25 0 1 0 485397835 18825216 4224 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4596 4224 603 41 0 4555 0
vsize: 18384
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4832 0 0 0 103984 25 0 0 25 0 1 0 485397835 18956288 4232 4294967295 134512640 134672761 3221224528 3221223568 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4628 4232 603 41 0 4587 0
vsize: 18512
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4872 0 0 0 104984 25 0 0 25 0 1 0 485397835 19017728 4271 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4643 4271 603 41 0 4602 0
vsize: 18572
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4872 0 0 0 105984 25 0 0 25 0 1 0 485397835 19017728 4271 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4643 4271 603 41 0 4602 0
vsize: 18572
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4880 0 0 0 106984 25 0 0 25 0 1 0 485397835 19034112 4278 4294967295 134512640 134672761 3221224528 3221223712 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4647 4278 603 41 0 4606 0
vsize: 18588
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4880 0 0 0 107984 25 0 0 25 0 1 0 485397835 19034112 4278 4294967295 134512640 134672761 3221224528 3221223568 134614268 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4647 4278 603 41 0 4606 0
vsize: 18588
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4880 0 0 0 108985 25 0 0 25 0 1 0 485397835 19034112 4278 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4647 4278 603 41 0 4606 0
vsize: 18588
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4930 0 0 0 109985 25 0 0 25 0 1 0 485397835 19243008 4328 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4698 4328 603 41 0 4657 0
vsize: 18792
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4930 0 0 0 110985 25 0 0 25 0 1 0 485397835 19243008 4328 4294967295 134512640 134672761 3221224528 3221223568 134612966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4698 4328 603 41 0 4657 0
vsize: 18792
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4930 0 0 0 111985 25 0 0 25 0 1 0 485397835 19243008 4328 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4698 4328 603 41 0 4657 0
vsize: 18792
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4939 0 0 0 112985 25 0 0 25 0 1 0 485397835 19275776 4336 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4706 4336 603 41 0 4665 0
vsize: 18824
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4939 0 0 0 113985 25 0 0 25 0 1 0 485397835 19275776 4336 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4706 4336 603 41 0 4665 0
vsize: 18824
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 4939 0 0 0 114986 25 0 0 25 0 1 0 485397835 19275776 4336 4294967295 134512640 134672761 3221224528 3221223664 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4706 4336 603 41 0 4665 0
vsize: 18824
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5035 0 0 0 115985 25 0 0 25 0 1 0 485397835 19668992 4432 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4802 4432 603 41 0 4761 0
vsize: 19208
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5078 0 0 0 116986 25 0 0 25 0 1 0 485397835 19836928 4474 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4843 4474 603 41 0 4802 0
vsize: 19372
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5078 0 0 0 117986 25 0 0 25 0 1 0 485397835 19836928 4474 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4843 4474 603 41 0 4802 0
vsize: 19372
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5078 0 0 0 118986 25 0 0 25 0 1 0 485397835 19836928 4474 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4843 4474 603 41 0 4802 0
vsize: 19372
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27998
Raw data (stat): 27998 (minisat+) R 27997 25347 25346 0 -1 0 5125 0 0 0 119986 25 0 0 25 0 1 0 485397835 20029440 4520 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4890 4520 603 41 0 4849 0
vsize: 19560
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27998
Raw data (stat): 27998 (minisat+) Z 27997 25347 25346 0 -1 12 5126 0 0 0 119986 26 0 0 25 0 1 0 485397835 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.02
CPU time (s): 1200.13
CPU user time (s): 1199.87
CPU system time (s): 0.268959
CPU usage (%): 100.01
Max. virtual memory (Kb): 19560
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####