PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	c8b965306fec2c21edee64824d12f378
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.08
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 21393

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 23:39:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13518 boxname=wulflinc3 idbench=1040 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c8b965306fec2c21edee64824d12f378  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 13518
/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:        371784 kB
Buffers:         34176 kB
Cached:         606452 kB
SwapCached:          0 kB
Active:         111508 kB
Inactive:       531876 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        371532 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13752 kB
Committed_AS:    71776 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:59:44 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 13518 7 1200.16 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.452931 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.7175 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.9333 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: 62.6865 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: 67.6607 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.1 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: 130.427 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: 133.457 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: 140.226 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: 414.362 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: 444.979 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: 446.928 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: 482.594 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: 498.399 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: 536.435 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: 543.349 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.87 0.93 0.92 2/54 23037
Raw data (stat): 23037 (runsolver) R 23036 10720 10719 0 -1 64 2 0 0 0 0 0 0 0 19 0 1 0 490883221 1052672 97 4294967295 134512640 135381576 3221224432 3221219800 135024953 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.89 0.93 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 1788 0 0 0 993 5 0 0 25 0 1 0 490883221 8327168 1649 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2033 1649 603 41 0 1992 0
vsize: 8132
[startup+20.0008 s]
Raw data (loadavg): 0.91 0.94 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2431 0 0 0 1991 7 0 0 25 0 1 0 490883221 10960896 2292 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2676 2292 603 41 0 2635 0
vsize: 10704
[startup+30.0014 s]
Raw data (loadavg): 0.92 0.94 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2717 0 0 0 2990 8 0 0 25 0 1 0 490883221 11923456 2543 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2911 2543 603 41 0 2870 0
vsize: 11644
[startup+40.0015 s]
Raw data (loadavg): 0.93 0.94 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2742 0 0 0 3989 9 0 0 25 0 1 0 490883221 11747328 2502 4294967295 134512640 134672761 3221224544 3221223536 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2868 2502 603 41 0 2827 0
vsize: 11472
[startup+50.0023 s]
Raw data (loadavg): 0.94 0.94 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2744 0 0 0 4990 9 0 0 25 0 1 0 490883221 11747328 2504 4294967295 134512640 134672761 3221224544 3221223584 134612860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2868 2504 603 41 0 2827 0
vsize: 11472
[startup+60.0018 s]
Raw data (loadavg): 0.95 0.94 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2763 0 0 0 5990 9 0 0 25 0 1 0 490883221 11878400 2523 4294967295 134512640 134672761 3221224544 3221223584 134612636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2900 2523 603 41 0 2859 0
vsize: 11600
[startup+70.002 s]
Raw data (loadavg): 0.96 0.94 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2844 0 0 0 6989 9 0 0 25 0 1 0 490883221 11943936 2552 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2916 2552 603 41 0 2875 0
vsize: 11664
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.94 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2883 0 0 0 7989 9 0 0 25 0 1 0 490883221 11943936 2554 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+90.0023 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2883 0 0 0 8989 9 0 0 25 0 1 0 490883221 11943936 2554 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2883 0 0 0 9989 9 0 0 25 0 1 0 490883221 11943936 2554 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+110.002 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 2883 0 0 0 10989 9 0 0 25 0 1 0 490883221 11943936 2554 4294967295 134512640 134672761 3221224544 3221222784 134645390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2916 2554 603 41 0 2875 0
vsize: 11664
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3022 0 0 0 11989 10 0 0 25 0 1 0 490883221 12603392 2693 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3077 2693 603 41 0 3036 0
vsize: 12308
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3089 0 0 0 12989 10 0 0 25 0 1 0 490883221 12828672 2760 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3132 2760 603 41 0 3091 0
vsize: 12528
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3247 0 0 0 13988 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+150.003 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3318 0 0 0 14988 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+160.003 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3318 0 0 0 15988 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223200 134645479 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+170.003 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3318 0 0 0 16988 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3318 0 0 0 17988 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3318 0 0 0 18989 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3318 0 0 0 19989 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3318 0 0 0 20989 11 0 0 25 0 1 0 490883221 12845056 2774 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3136 2774 603 41 0 3095 0
vsize: 12544
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3355 0 0 0 21989 11 0 0 25 0 1 0 490883221 13037568 2810 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3183 2810 603 41 0 3142 0
vsize: 12732
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3575 0 0 0 22989 12 0 0 25 0 1 0 490883221 13926400 3030 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3400 3030 603 41 0 3359 0
vsize: 13600
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3575 0 0 0 23989 12 0 0 25 0 1 0 490883221 13926400 3030 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3400 3030 603 41 0 3359 0
vsize: 13600
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3589 0 0 0 24989 12 0 0 25 0 1 0 490883221 13983744 3043 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3414 3043 603 41 0 3373 0
vsize: 13656
[startup+260.006 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3589 0 0 0 25989 12 0 0 25 0 1 0 490883221 13983744 3043 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3414 3043 603 41 0 3373 0
vsize: 13656
[startup+270.005 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3591 0 0 0 26989 12 0 0 25 0 1 0 490883221 13979648 3044 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 3044 603 41 0 3372 0
vsize: 13652
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3591 0 0 0 27989 12 0 0 25 0 1 0 490883221 13979648 3044 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 3044 603 41 0 3372 0
vsize: 13652
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3592 0 0 0 28990 12 0 0 25 0 1 0 490883221 13979648 3045 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 3045 603 41 0 3372 0
vsize: 13652
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3592 0 0 0 29990 12 0 0 25 0 1 0 490883221 13979648 3045 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 3045 603 41 0 3372 0
vsize: 13652
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3592 0 0 0 30990 12 0 0 25 0 1 0 490883221 13979648 3045 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 3045 603 41 0 3372 0
vsize: 13652
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3627 0 0 0 31990 12 0 0 25 0 1 0 490883221 14127104 3079 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3743 0 0 0 32990 12 0 0 25 0 1 0 490883221 14651392 3195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3577 3195 603 41 0 3536 0
vsize: 14308
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3814 0 0 0 33990 12 0 0 25 0 1 0 490883221 14880768 3266 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3633 3266 603 41 0 3592 0
vsize: 14532
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3830 0 0 0 34990 12 0 0 25 0 1 0 490883221 15024128 3282 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3668 3282 603 41 0 3627 0
vsize: 14672
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3872 0 0 0 35991 12 0 0 25 0 1 0 490883221 15118336 3324 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3691 3324 603 41 0 3650 0
vsize: 14764
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3872 0 0 0 36991 12 0 0 25 0 1 0 490883221 15118336 3324 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3691 3324 603 41 0 3650 0
vsize: 14764
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3872 0 0 0 37991 12 0 0 25 0 1 0 490883221 15118336 3324 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3691 3324 603 41 0 3650 0
vsize: 14764
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3936 0 0 0 38991 12 0 0 25 0 1 0 490883221 15380480 3388 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3755 3388 603 41 0 3714 0
vsize: 15020
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3936 0 0 0 39991 12 0 0 25 0 1 0 490883221 15380480 3388 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3755 3388 603 41 0 3714 0
vsize: 15020
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 3956 0 0 0 40991 13 0 0 25 0 1 0 490883221 15462400 3408 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3775 3408 603 41 0 3734 0
vsize: 15100
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4077 0 0 0 41990 13 0 0 25 0 1 0 490883221 15720448 3434 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3434 603 41 0 3797 0
vsize: 15352
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4077 0 0 0 42990 14 0 0 25 0 1 0 490883221 15720448 3434 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3434 603 41 0 3797 0
vsize: 15352
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4094 0 0 0 43990 14 0 0 25 0 1 0 490883221 15720448 3451 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3451 603 41 0 3797 0
vsize: 15352
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4121 0 0 0 44990 14 0 0 25 0 1 0 490883221 15720448 3465 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3465 603 41 0 3797 0
vsize: 15352
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4121 0 0 0 45990 14 0 0 25 0 1 0 490883221 15720448 3465 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3465 603 41 0 3797 0
vsize: 15352
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4121 0 0 0 46990 14 0 0 25 0 1 0 490883221 15720448 3465 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3465 603 41 0 3797 0
vsize: 15352
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4121 0 0 0 47990 14 0 0 25 0 1 0 490883221 15720448 3465 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3465 603 41 0 3797 0
vsize: 15352
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4122 0 0 0 48990 14 0 0 25 0 1 0 490883221 15720448 3466 4294967295 134512640 134672761 3221224544 3221222240 134645273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3466 603 41 0 3797 0
vsize: 15352
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4122 0 0 0 49990 14 0 0 25 0 1 0 490883221 15720448 3466 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3466 603 41 0 3797 0
vsize: 15352
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4122 0 0 0 50989 14 0 0 25 0 1 0 490883221 15720448 3466 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3466 603 41 0 3797 0
vsize: 15352
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4122 0 0 0 51989 14 0 0 25 0 1 0 490883221 15720448 3466 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3466 603 41 0 3797 0
vsize: 15352
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4122 0 0 0 52989 14 0 0 25 0 1 0 490883221 15720448 3466 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3466 603 41 0 3797 0
vsize: 15352
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4124 0 0 0 53989 14 0 0 25 0 1 0 490883221 15720448 3468 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3468 603 41 0 3797 0
vsize: 15352
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 54988 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 55989 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 56989 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223584 134612507 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 57989 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 58989 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 59989 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 60989 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 61989 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 62988 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 63988 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 64987 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223584 134612619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4125 0 0 0 65988 15 0 0 25 0 1 0 490883221 15720448 3469 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3469 603 41 0 3797 0
vsize: 15352
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4126 0 0 0 66988 15 0 0 25 0 1 0 490883221 15720448 3470 4294967295 134512640 134672761 3221224544 3221222992 134645479 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3470 603 41 0 3797 0
vsize: 15352
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4126 0 0 0 67988 15 0 0 25 0 1 0 490883221 15720448 3470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3470 603 41 0 3797 0
vsize: 15352
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4126 0 0 0 68988 15 0 0 25 0 1 0 490883221 15720448 3470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3470 603 41 0 3797 0
vsize: 15352
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4126 0 0 0 69988 15 0 0 25 0 1 0 490883221 15720448 3470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3470 603 41 0 3797 0
vsize: 15352
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4126 0 0 0 70988 15 0 0 25 0 1 0 490883221 15720448 3470 4294967295 134512640 134672761 3221224544 3221223584 134603565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3470 603 41 0 3797 0
vsize: 15352
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4126 0 0 0 71989 15 0 0 25 0 1 0 490883221 15720448 3470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3470 603 41 0 3797 0
vsize: 15352
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4142 0 0 0 72989 15 0 0 25 0 1 0 490883221 15814656 3486 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3861 3486 603 41 0 3820 0
vsize: 15444
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4179 0 0 0 73989 15 0 0 25 0 1 0 490883221 15945728 3523 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3893 3523 603 41 0 3852 0
vsize: 15572
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4213 0 0 0 74989 15 0 0 25 0 1 0 490883221 16097280 3556 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3930 3556 603 41 0 3889 0
vsize: 15720
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4223 0 0 0 75989 15 0 0 25 0 1 0 490883221 16228352 3566 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3962 3566 603 41 0 3921 0
vsize: 15848
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4263 0 0 0 76989 15 0 0 25 0 1 0 490883221 16306176 3606 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4263 0 0 0 77990 15 0 0 25 0 1 0 490883221 16306176 3606 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4263 0 0 0 78990 15 0 0 25 0 1 0 490883221 16306176 3606 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3981 3606 603 41 0 3940 0
vsize: 15924
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4286 0 0 0 79990 15 0 0 25 0 1 0 490883221 16465920 3629 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4020 3629 603 41 0 3979 0
vsize: 16080
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4286 0 0 0 80990 15 0 0 25 0 1 0 490883221 16400384 3629 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4004 3629 603 41 0 3963 0
vsize: 16016
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4286 0 0 0 81990 15 0 0 25 0 1 0 490883221 16400384 3629 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4004 3629 603 41 0 3963 0
vsize: 16016
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4422 0 0 0 82990 16 0 0 25 0 1 0 490883221 16953344 3764 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4139 3764 603 41 0 4098 0
vsize: 16556
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4422 0 0 0 83991 16 0 0 25 0 1 0 490883221 16953344 3764 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4139 3764 603 41 0 4098 0
vsize: 16556
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4439 0 0 0 84991 16 0 0 25 0 1 0 490883221 17018880 3780 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3780 603 41 0 4114 0
vsize: 16620
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4439 0 0 0 85991 16 0 0 25 0 1 0 490883221 17018880 3780 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4469 0 0 0 86991 16 0 0 25 0 1 0 490883221 17133568 3810 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4183 3810 603 41 0 4142 0
vsize: 16732
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4470 0 0 0 87991 16 0 0 25 0 1 0 490883221 17133568 3811 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4183 3811 603 41 0 4142 0
vsize: 16732
[startup+890.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4566 0 0 0 88991 16 0 0 25 0 1 0 490883221 17526784 3907 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4279 3907 603 41 0 4238 0
vsize: 17116
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4566 0 0 0 89992 16 0 0 25 0 1 0 490883221 17526784 3907 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4566 0 0 0 90992 16 0 0 25 0 1 0 490883221 17526784 3907 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4736 0 0 0 91991 17 0 0 25 0 1 0 490883221 18317312 4077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4472 4077 603 41 0 4431 0
vsize: 17888
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4855 0 0 0 92991 17 0 0 25 0 1 0 490883221 18710528 4196 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4568 4196 603 41 0 4527 0
vsize: 18272
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4855 0 0 0 93991 17 0 0 25 0 1 0 490883221 18710528 4196 4294967295 134512640 134672761 3221224544 3221223728 134615807 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.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4855 0 0 0 94992 17 0 0 25 0 1 0 490883221 18710528 4196 4294967295 134512640 134672761 3221224544 3221223728 134615663 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.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4867 0 0 0 95992 17 0 0 25 0 1 0 490883221 18759680 4207 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4580 4207 603 41 0 4539 0
vsize: 18320
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4867 0 0 0 96992 17 0 0 25 0 1 0 490883221 18759680 4207 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4580 4207 603 41 0 4539 0
vsize: 18320
[startup+980.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4876 0 0 0 97992 17 0 0 25 0 1 0 490883221 18792448 4215 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4215 603 41 0 4547 0
vsize: 18352
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4876 0 0 0 98992 17 0 0 25 0 1 0 490883221 18792448 4215 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4215 603 41 0 4547 0
vsize: 18352
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4876 0 0 0 99993 17 0 0 25 0 1 0 490883221 18792448 4215 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4215 603 41 0 4547 0
vsize: 18352
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4885 0 0 0 100993 17 0 0 25 0 1 0 490883221 18825216 4223 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4596 4223 603 41 0 4555 0
vsize: 18384
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4885 0 0 0 101993 17 0 0 25 0 1 0 490883221 18825216 4223 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4596 4223 603 41 0 4555 0
vsize: 18384
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4885 0 0 0 102993 17 0 0 25 0 1 0 490883221 18825216 4223 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4596 4223 603 41 0 4555 0
vsize: 18384
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4933 0 0 0 103993 17 0 0 25 0 1 0 490883221 19013632 4270 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4642 4270 603 41 0 4601 0
vsize: 18568
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4933 0 0 0 104994 17 0 0 25 0 1 0 490883221 19013632 4270 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4642 4270 603 41 0 4601 0
vsize: 18568
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4940 0 0 0 105994 17 0 0 25 0 1 0 490883221 19030016 4276 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4276 603 41 0 4605 0
vsize: 18584
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4940 0 0 0 106994 17 0 0 25 0 1 0 490883221 19030016 4276 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4276 603 41 0 4605 0
vsize: 18584
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4940 0 0 0 107994 17 0 0 25 0 1 0 490883221 19030016 4276 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4646 4276 603 41 0 4605 0
vsize: 18584
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.92 3/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4947 0 0 0 108994 17 0 0 25 0 1 0 490883221 19165184 4283 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4679 4283 603 41 0 4638 0
vsize: 18716
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4993 0 0 0 109994 17 0 0 25 0 1 0 490883221 19243008 4329 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4698 4329 603 41 0 4657 0
vsize: 18792
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 4993 0 0 0 110995 17 0 0 25 0 1 0 490883221 19243008 4329 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4698 4329 603 41 0 4657 0
vsize: 18792
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5002 0 0 0 111995 17 0 0 25 0 1 0 490883221 19275776 4337 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4706 4337 603 41 0 4665 0
vsize: 18824
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5002 0 0 0 112995 17 0 0 25 0 1 0 490883221 19275776 4337 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4706 4337 603 41 0 4665 0
vsize: 18824
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5002 0 0 0 113995 17 0 0 25 0 1 0 490883221 19275776 4337 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4706 4337 603 41 0 4665 0
vsize: 18824
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5033 0 0 0 114995 17 0 0 25 0 1 0 490883221 19410944 4368 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4739 4368 603 41 0 4698 0
vsize: 18956
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5140 0 0 0 115995 18 0 0 25 0 1 0 490883221 19841024 4474 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4844 4474 603 41 0 4803 0
vsize: 19376
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5140 0 0 0 116995 18 0 0 25 0 1 0 490883221 19841024 4474 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4844 4474 603 41 0 4803 0
vsize: 19376
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5140 0 0 0 117995 18 0 0 25 0 1 0 490883221 19841024 4474 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4844 4474 603 41 0 4803 0
vsize: 19376
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5187 0 0 0 118995 18 0 0 25 0 1 0 490883221 20029440 4520 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4890 4520 603 41 0 4849 0
vsize: 19560
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 23037
Raw data (stat): 23037 (minisat+) R 23036 10720 10719 0 -1 0 5187 0 0 0 119995 18 0 0 25 0 1 0 490883221 20029440 4520 4294967295 134512640 134672761 3221224544 3221223728 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.06 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 23037
Raw data (stat): 23037 (minisat+) Z 23036 10720 10719 0 -1 12 5188 0 0 0 119996 19 0 0 25 0 1 0 490883221 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.05
CPU time (s): 1200.16
CPU user time (s): 1199.96
CPU system time (s): 0.19497
CPU usage (%): 100.008
Max. virtual memory (Kb): 19560
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####