PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32d1.opb
MD5SUM	151e246868267296e134c3c76a3cb289
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	285
Optimality of the best value was proved	NO
Number of terms in the objective function	664
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	664
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	664
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02484
Number of variables	664
Total number of constraints	3035
Number of constraints which are clauses	3035
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 5491

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 00:10:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3915 boxname=wulflinc32 idbench=155 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  151e246868267296e134c3c76a3cb289  /oldhome/oroussel/tmp/wulflinc32/normalized-ii32d1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc32/normalized-ii32d1.opb /oldhome/oroussel/tmp/wulflinc32/normalized-ii32d1.opb
IDLAUNCH: 3915
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        709668 kB
Buffers:         34604 kB
Cached:         178996 kB
SwapCached:       1212 kB
Active:         145284 kB
Inactive:       148644 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        709412 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2288 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25272 kB
Committed_AS:   173996 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:30:15 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 3915 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3035 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3035     9828 |     910       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  664/664          
c |         0 |    3035     9828 |    1214       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.133979 s)
c ==============================================================================
c [1mFound solution: 321[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30182     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        46 |   39413    94898 |   11823      46     3340    72.6 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24392          
c   -- var.elim.:  2000/24392          
c   -- var.elim.:  3000/24392          
c   -- var.elim.:  4000/24392          
c   -- var.elim.:  5000/24392          
c   -- var.elim.:  6000/24392          
c   -- var.elim.:  7000/24392          
c   -- var.elim.:  8000/24392          
c   -- var.elim.:  9000/24392          
c   -- var.elim.:  10000/24392          
c   -- var.elim.:  11000/24392          
c   -- var.elim.:  12000/24392          
c   -- var.elim.:  13000/24392          
c   -- var.elim.:  14000/24392          
c   -- var.elim.:  15000/24392          
c   -- var.elim.:  16000/24392          
c   -- var.elim.:  17000/24392          
c   -- var.elim.:  18000/24392          
c   -- var.elim.:  19000/24392          
c   -- var.elim.:  20000/24392          
c   -- var.elim.:  21000/24392          
c   -- var.elim.:  22000/24392          
c   -- var.elim.:  23000/24392          
c   -- var.elim.:  24000/24392          
c   -- var.elim.:  24392/24392          
c   -- var.elim.:  1000/11997          
c   -- var.elim.:  2000/11997          
c   -- var.elim.:  3000/11997          
c   -- var.elim.:  4000/11997          
c   -- var.elim.:  5000/11997          
c   -- var.elim.:  6000/11997          
c   -- var.elim.:  7000/11997          
c   -- var.elim.:  8000/11997          
c   -- var.elim.:  9000/11997          
c   -- var.elim.:  10000/11997          
c   -- var.elim.:  11000/11997          
c   -- var.elim.:  11997/11997          
c   -- var.elim.:  1000/7358          
c   -- var.elim.:  2000/7358          
c   -- var.elim.:  3000/7358          
c   -- var.elim.:  4000/7358          
c   -- var.elim.:  5000/7358          
c   -- var.elim.:  6000/7358          
c   -- var.elim.:  7000/7358          
c   -- var.elim.:  7358/7358          
c   -- var.elim.:  1000/5098          
c   -- var.elim.:  2000/5098          
c   -- var.elim.:  3000/5098          
c   -- var.elim.:  4000/5098          
c   -- var.elim.:  5000/5098          
c   -- var.elim.:  5098/5098          
c   -- var.elim.:  1000/4226          
c   -- var.elim.:  2000/4226          
c   -- var.elim.:  3000/4226          
c   -- var.elim.:  4000/4226          
c   -- var.elim.:  4226/4226          
c   -- var.elim.:  1000/3442          
c   -- var.elim.:  2000/3442          
c   -- var.elim.:  3000/3442          
c   -- var.elim.:  3442/3442          
c   -- var.elim.:  1000/2559          
c   -- var.elim.:  2000/2559          
c   -- var.elim.:  2559/2559          
c   -- var.elim.:  256/256          
c   -- subsuming                       
c   -- var.elim.:  1000/3500          
c   -- var.elim.:  2000/3500          
c   -- var.elim.:  3000/3500          
c   -- var.elim.:  3500/3500          
c   -- var.elim.:  398/398          
c |        46 |   13086    84643 |      --      46       --      -- |     --   | -26327/-10254
c |        46 |   13086    84643 |    5234      46     3340    72.6 |  0.000 % |
c |       148 |   13086    84643 |    5757     148     9141    61.8 |  0.019 % |
c |       300 |   13086    84643 |    6333     300    19619    65.4 |  0.019 % |
c |       527 |   13086    84643 |    6966     527    33469    63.5 |  0.019 % |
c |       867 |   13086    84643 |    7663     867    55198    63.7 |  0.019 % |
c ==============================================================================
c (current CPU-time: 33.4939 s)
c ==============================================================================
c [1mFound solution: 314[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1292 |   38236   146376 |   11470    1292   119868    92.8 |  0.019 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22943          
c   -- var.elim.:  2000/22943          
c   -- var.elim.:  3000/22943          
c   -- var.elim.:  4000/22943          
c   -- var.elim.:  5000/22943          
c   -- var.elim.:  6000/22943          
c   -- var.elim.:  7000/22943          
c   -- var.elim.:  8000/22943          
c   -- var.elim.:  9000/22943          
c   -- var.elim.:  10000/22943          
c   -- var.elim.:  11000/22943          
c   -- var.elim.:  12000/22943          
c   -- var.elim.:  13000/22943          
c   -- var.elim.:  14000/22943          
c   -- var.elim.:  15000/22943          
c   -- var.elim.:  16000/22943          
c   -- var.elim.:  17000/22943          
c   -- var.elim.:  18000/22943          
c   -- var.elim.:  19000/22943          
c   -- var.elim.:  20000/22943          
c   -- var.elim.:  21000/22943          
c   -- var.elim.:  22000/22943          
c   -- var.elim.:  22943/22943          
c   -- var.elim.:  1000/11075          
c   -- var.elim.:  2000/11075          
c   -- var.elim.:  3000/11075          
c   -- var.elim.:  4000/11075          
c   -- var.elim.:  5000/11075          
c   -- var.elim.:  6000/11075          
c   -- var.elim.:  7000/11075          
c   -- var.elim.:  8000/11075          
c   -- var.elim.:  9000/11075          
c   -- var.elim.:  10000/11075          
c   -- var.elim.:  11000/11075          
c   -- var.elim.:  11075/11075          
c   -- var.elim.:  1000/6869          
c   -- var.elim.:  2000/6869          
c   -- var.elim.:  3000/6869          
c   -- var.elim.:  4000/6869          
c   -- var.elim.:  5000/6869          
c   -- var.elim.:  6000/6869          
c   -- var.elim.:  6869/6869          
c   -- var.elim.:  1000/5064          
c   -- var.elim.:  2000/5064          
c   -- var.elim.:  3000/5064          
c   -- var.elim.:  4000/5064          
c   -- var.elim.:  5000/5064          
c   -- var.elim.:  5064/5064          
c   -- var.elim.:  1000/3935          
c   -- var.elim.:  2000/3935          
c   -- var.elim.:  3000/3935          
c   -- var.elim.:  3935/3935          
c   -- var.elim.:  1000/3128          
c   -- var.elim.:  2000/3128          
c   -- var.elim.:  3000/3128          
c   -- var.elim.:  3128/3128          
c   -- var.elim.:  1000/1916          
c   -- var.elim.:  1916/1916          
c   -- var.elim.:  776/776          
c   -- var.elim.:  38/38          
c   -- subsuming                       
c   -- var.elim.:  650/650          
c |      1292 |   13252    86850 |      --    1292       --      -- |     --   | -24976/-59437
c |      1292 |   13252    86850 |    5300    1255    78855    62.8 |  0.019 % |
c |      1393 |   13252    86850 |    5830    1356    95558    70.5 |  0.110 % |
c |      1543 |   13252    86850 |    6413    1506   114207    75.8 |  0.110 % |
c |      1768 |   13252    86850 |    7055    1731   166658    96.3 |  0.110 % |
c |      2105 |   13252    86850 |    7760    2068   323117   156.2 |  0.110 % |
c ==============================================================================
c (current CPU-time: 62.2455 s)
c ==============================================================================
c [1mFound solution: 299[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2472 |   36740   136513 |   11021    2373   422280   178.0 |  0.110 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22365          
c   -- var.elim.:  2000/22365          
c   -- var.elim.:  3000/22365          
c   -- var.elim.:  4000/22365          
c   -- var.elim.:  5000/22365          
c   -- var.elim.:  6000/22365          
c   -- var.elim.:  7000/22365          
c   -- var.elim.:  8000/22365          
c   -- var.elim.:  9000/22365          
c   -- var.elim.:  10000/22365          
c   -- var.elim.:  11000/22365          
c   -- var.elim.:  12000/22365          
c   -- var.elim.:  13000/22365          
c   -- var.elim.:  14000/22365          
c   -- var.elim.:  15000/22365          
c   -- var.elim.:  16000/22365          
c   -- var.elim.:  17000/22365          
c   -- var.elim.:  18000/22365          
c   -- var.elim.:  19000/22365          
c   -- var.elim.:  20000/22365          
c   -- var.elim.:  21000/22365          
c   -- var.elim.:  22000/22365          
c   -- var.elim.:  22365/22365          
c   -- var.elim.:  1000/10615          
c   -- var.elim.:  2000/10615          
c   -- var.elim.:  3000/10615          
c   -- var.elim.:  4000/10615          
c   -- var.elim.:  5000/10615          
c   -- var.elim.:  6000/10615          
c   -- var.elim.:  7000/10615          
c   -- var.elim.:  8000/10615          
c   -- var.elim.:  9000/10615          
c   -- var.elim.:  10000/10615          
c   -- var.elim.:  10615/10615          
c   -- var.elim.:  1000/6605          
c   -- var.elim.:  2000/6605          
c   -- var.elim.:  3000/6605          
c   -- var.elim.:  4000/6605          
c   -- var.elim.:  5000/6605          
c   -- var.elim.:  6000/6605          
c   -- var.elim.:  6605/6605          
c   -- var.elim.:  1000/4878          
c   -- var.elim.:  2000/4878          
c   -- var.elim.:  3000/4878          
c   -- var.elim.:  4000/4878          
c   -- var.elim.:  4878/4878          
c   -- var.elim.:  1000/3761          
c   -- var.elim.:  2000/3761          
c   -- var.elim.:  3000/3761          
c   -- var.elim.:  3761/3761          
c   -- var.elim.:  1000/3420          
c   -- var.elim.:  2000/3420          
c   -- var.elim.:  3000/3420          
c   -- var.elim.:  3420/3420          
c   -- var.elim.:  1000/3010          
c   -- var.elim.:  2000/3010          
c   -- var.elim.:  3000/3010          
c   -- var.elim.:  3010/3010          
c   -- var.elim.:  1000/1638          
c   -- var.elim.:  1638/1638          
c   -- var.elim.:  279/279          
c   -- subsuming                       
c   -- var.elim.:  1000/2265          
c   -- var.elim.:  2000/2265          
c   -- var.elim.:  2265/2265          
c   -- var.elim.:  5/5          
c |      2472 |   12210    79967 |      --    2373       --      -- |     --   | -24466/-56417
c |      2472 |   12210    79967 |    4884    1997   142999    71.6 |  0.110 % |
c |      2573 |   12210    79967 |    5372    2098   153116    73.0 | 17.163 % |
c |      2723 |   12210    79967 |    5909    2248   216592    96.3 | 17.163 % |
c |      2950 |   12172    79631 |    6480    2474   259109   104.7 | 17.448 % |
c |      3290 |   12172    79631 |    7128    2814   505820   179.8 | 17.448 % |
c |      3796 |   12172    79631 |    7841    3320   920377   277.2 | 17.448 % |
c |      4555 |   12108    79021 |    8580    4075  1184126   290.6 | 17.902 % |
c |      5694 |   12052    78635 |    9394    5212  1573105   301.8 | 18.255 % |
c |      7402 |   12020    78407 |   10306    6919  2267202   327.7 | 18.507 % |
c ==============================================================================
c (current CPU-time: 102.53 s)
c ==============================================================================
c [1mFound solution: 297[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8281 |   35277   134911 |   10583    7797  2874520   368.7 | 18.507 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21259          
c   -- var.elim.:  2000/21259          
c   -- var.elim.:  3000/21259          
c   -- var.elim.:  4000/21259          
c   -- var.elim.:  5000/21259          
c   -- var.elim.:  6000/21259          
c   -- var.elim.:  7000/21259          
c   -- var.elim.:  8000/21259          
c   -- var.elim.:  9000/21259          
c   -- var.elim.:  10000/21259          
c   -- var.elim.:  11000/21259          
c   -- var.elim.:  12000/21259          
c   -- var.elim.:  13000/21259          
c   -- var.elim.:  14000/21259          
c   -- var.elim.:  15000/21259          
c   -- var.elim.:  16000/21259          
c   -- var.elim.:  17000/21259          
c   -- var.elim.:  18000/21259          
c   -- var.elim.:  19000/21259          
c   -- var.elim.:  20000/21259          
c   -- var.elim.:  21000/21259          
c   -- var.elim.:  21259/21259          
c   -- var.elim.:  1000/9844          
c   -- var.elim.:  2000/9844          
c   -- var.elim.:  3000/9844          
c   -- var.elim.:  4000/9844          
c   -- var.elim.:  5000/9844          
c   -- var.elim.:  6000/9844          
c   -- var.elim.:  7000/9844          
c   -- var.elim.:  8000/9844          
c   -- var.elim.:  9000/9844          
c   -- var.elim.:  9844/9844          
c   -- var.elim.:  1000/6113          
c   -- var.elim.:  2000/6113          
c   -- var.elim.:  3000/6113          
c   -- var.elim.:  4000/6113          
c   -- var.elim.:  5000/6113          
c   -- var.elim.:  6000/6113          
c   -- var.elim.:  6113/6113          
c   -- var.elim.:  1000/4263          
c   -- var.elim.:  2000/4263          
c   -- var.elim.:  3000/4263          
c   -- var.elim.:  4000/4263          
c   -- var.elim.:  4263/4263          
c   -- var.elim.:  1000/3413          
c   -- var.elim.:  2000/3413          
c   -- var.elim.:  3000/3413          
c   -- var.elim.:  3413/3413          
c   -- var.elim.:  1000/2877          
c   -- var.elim.:  2000/2877          
c   -- var.elim.:  2877/2877          
c   -- var.elim.:  1000/2423          
c   -- var.elim.:  2000/2423          
c   -- var.elim.:  2423/2423          
c   -- var.elim.:  763/763          
c   -- subsuming                       
c   -- var.elim.:  1000/1511          
c   -- var.elim.:  1511/1511          
c |      8281 |   12051    80033 |      --    7797       --      -- |     --   | -23212/-54849
c |      8281 |   12051    80033 |    4820    5145   525619   102.2 | 18.507 % |
c |      8381 |   11920    78952 |    5244    5240   559208   106.7 | 20.354 % |
c |      8533 |   11920    78952 |    5769    5392   650023   120.6 | 20.354 % |
c |      8758 |   11882    78660 |    6325    5615   759876   135.3 | 20.634 % |
c |      9098 |   11882    78660 |    6958    5955  1008386   169.3 | 20.634 % |
c ==============================================================================
c (current CPU-time: 130.19 s)
c ==============================================================================
c [1mFound solution: 296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9540 |   28090   118052 |    8426    6397  1323367   206.9 | 20.634 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15405          
c   -- var.elim.:  2000/15405          
c   -- var.elim.:  3000/15405          
c   -- var.elim.:  4000/15405          
c   -- var.elim.:  5000/15405          
c   -- var.elim.:  6000/15405          
c   -- var.elim.:  7000/15405          
c   -- var.elim.:  8000/15405          
c   -- var.elim.:  9000/15405          
c   -- var.elim.:  10000/15405          
c   -- var.elim.:  11000/15405          
c   -- var.elim.:  12000/15405          
c   -- var.elim.:  13000/15405          
c   -- var.elim.:  14000/15405          
c   -- var.elim.:  15000/15405          
c   -- var.elim.:  15405/15405          
c   -- var.elim.:  1000/6727          
c   -- var.elim.:  2000/6727          
c   -- var.elim.:  3000/6727          
c   -- var.elim.:  4000/6727          
c   -- var.elim.:  5000/6727          
c   -- var.elim.:  6000/6727          
c   -- var.elim.:  6727/6727          
c   -- var.elim.:  1000/4105          
c   -- var.elim.:  2000/4105          
c   -- var.elim.:  3000/4105          
c   -- var.elim.:  4000/4105          
c   -- var.elim.:  4105/4105          
c   -- var.elim.:  1000/2784          
c   -- var.elim.:  2000/2784          
c   -- var.elim.:  2784/2784          
c   -- var.elim.:  1000/2051          
c   -- var.elim.:  2000/2051          
c   -- var.elim.:  2051/2051          
c   -- var.elim.:  1000/1735          
c   -- var.elim.:  1735/1735          
c   -- var.elim.:  896/896          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  397/397          
c |      9540 |   11865    78414 |      --    6397       --      -- |     --   | -16191/-39274
c |      9540 |   11865    78414 |    4746    5540   530773    95.8 | 20.634 % |
c |      9640 |   11865    78414 |    5220    5640   565554   100.3 | 21.077 % |
c |      9790 |   11865    78414 |    5742    5790   663316   114.6 | 21.077 % |
c |     10015 |   11865    78414 |    6316    6015   699670   116.3 | 21.077 % |
c |     10353 |   11865    78414 |    6948    6353   840577   132.3 | 21.077 % |
c |     10859 |   11865    78414 |    7643    6859  1038605   151.4 | 21.077 % |
c |     11618 |   11837    78183 |    8387    7617  1557874   204.5 | 21.287 % |
c |     12758 |   11793    77864 |    9192    8756  2359047   269.4 | 21.579 % |
c |     14466 |   11660    76690 |    9997   10459  3396782   324.8 | 22.568 % |
c |     17029 |   11620    76375 |   10959    8731  3839857   439.8 | 22.876 % |
c |     20873 |   11620    76375 |   12055   12575  6547295   520.7 | 22.876 % |
c ==============================================================================
c (current CPU-time: 199.235 s)
c ==============================================================================
c [1mFound solution: 289[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     22589 |   35062   132985 |   10518   14288  7808080   546.5 | 22.876 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21216          
c   -- var.elim.:  2000/21216          
c   -- var.elim.:  3000/21216          
c   -- var.elim.:  4000/21216          
c   -- var.elim.:  5000/21216          
c   -- var.elim.:  6000/21216          
c   -- var.elim.:  7000/21216          
c   -- var.elim.:  8000/21216          
c   -- var.elim.:  9000/21216          
c   -- var.elim.:  10000/21216          
c   -- var.elim.:  11000/21216          
c   -- var.elim.:  12000/21216          
c   -- var.elim.:  13000/21216          
c   -- var.elim.:  14000/21216          
c   -- var.elim.:  15000/21216          
c   -- var.elim.:  16000/21216          
c   -- var.elim.:  17000/21216          
c   -- var.elim.:  18000/21216          
c   -- var.elim.:  19000/21216          
c   -- var.elim.:  20000/21216          
c   -- var.elim.:  21000/21216          
c   -- var.elim.:  21216/21216          
c   -- var.elim.:  1000/9900          
c   -- var.elim.:  2000/9900          
c   -- var.elim.:  3000/9900          
c   -- var.elim.:  4000/9900          
c   -- var.elim.:  5000/9900          
c   -- var.elim.:  6000/9900          
c   -- var.elim.:  7000/9900          
c   -- var.elim.:  8000/9900          
c   -- var.elim.:  9000/9900          
c   -- var.elim.:  9900/9900          
c   -- var.elim.:  1000/6132          
c   -- var.elim.:  2000/6132          
c   -- var.elim.:  3000/6132          
c   -- var.elim.:  4000/6132          
c   -- var.elim.:  5000/6132          
c   -- var.elim.:  6000/6132          
c   -- var.elim.:  6132/6132          
c   -- var.elim.:  1000/4107          
c   -- var.elim.:  2000/4107          
c   -- var.elim.:  3000/4107          
c   -- var.elim.:  4000/4107          
c   -- var.elim.:  4107/4107          
c   -- var.elim.:  1000/3099          
c   -- var.elim.:  2000/3099          
c   -- var.elim.:  3000/3099          
c   -- var.elim.:  3099/3099          
c   -- var.elim.:  1000/2475          
c   -- var.elim.:  2000/2475          
c   -- var.elim.:  2475/2475          
c   -- var.elim.:  1000/1693          
c   -- var.elim.:  1693/1693          
c   -- var.elim.:  146/146          
c   -- subsuming                       
c   -- var.elim.:  1000/1379          
c   -- var.elim.:  1379/1379          
c   -- var.elim.:  5/5          
c |     22589 |   11701    77005 |      --   14288       --      -- |     --   | -23328/-55913
c |     22589 |   11701    77005 |    4680    6020   579760    96.3 | 22.876 % |
c |     22691 |   11701    77005 |    5148    6122   637956   104.2 | 24.932 % |
c |     22841 |   11701    77005 |    5663    6272   732710   116.8 | 24.932 % |
c |     23066 |   11701    77005 |    6229    6497   813729   125.2 | 24.932 % |
c |     23403 |   11701    77005 |    6852    6834  1067164   156.2 | 24.932 % |
c |     23909 |   11701    77005 |    7537    7340  1375419   187.4 | 24.932 % |
c |     24668 |   11701    77005 |    8291    8099  2017912   249.2 | 24.932 % |
c |     25808 |   11627    76372 |    9063    9236  2924080   316.6 | 25.427 % |
c |     27516 |   11454    74927 |    9821    7358  3907012   531.0 | 26.639 % |
c |     30081 |   11371    74262 |   10724    9921  5999127   604.7 | 27.245 % |
c |     33925 |   11335    73892 |   11760    9241  6568381   710.8 | 27.468 % |
c ==============================================================================
c (current CPU-time: 289.161 s)
c ==============================================================================
c [1mFound solution: 285[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     34847 |   33830   128425 |   10148   10163  7402614   728.4 | 27.468 % |
c   -- subsuming                       
c   -- var.elim.:  1000/20298          
c   -- var.elim.:  2000/20298          
c   -- var.elim.:  3000/20298          
c   -- var.elim.:  4000/20298          
c   -- var.elim.:  5000/20298          
c   -- var.elim.:  6000/20298          
c   -- var.elim.:  7000/20298          
c   -- var.elim.:  8000/20298          
c   -- var.elim.:  9000/20298          
c   -- var.elim.:  10000/20298          
c   -- var.elim.:  11000/20298          
c   -- var.elim.:  12000/20298          
c   -- var.elim.:  13000/20298          
c   -- var.elim.:  14000/20298          
c   -- var.elim.:  15000/20298          
c   -- var.elim.:  16000/20298          
c   -- var.elim.:  17000/20298          
c   -- var.elim.:  18000/20298          
c   -- var.elim.:  19000/20298          
c   -- var.elim.:  20000/20298          
c   -- var.elim.:  20298/20298          
c   -- var.elim.:  1000/9271          
c   -- var.elim.:  2000/9271          
c   -- var.elim.:  3000/9271          
c   -- var.elim.:  4000/9271          
c   -- var.elim.:  5000/9271          
c   -- var.elim.:  6000/9271          
c   -- var.elim.:  7000/9271          
c   -- var.elim.:  8000/9271          
c   -- var.elim.:  9000/9271          
c   -- var.elim.:  9271/9271          
c   -- var.elim.:  1000/5593          
c   -- var.elim.:  2000/5593          
c   -- var.elim.:  3000/5593          
c   -- var.elim.:  4000/5593          
c   -- var.elim.:  5000/5593          
c   -- var.elim.:  5593/5593          
c   -- var.elim.:  1000/3924          
c   -- var.elim.:  2000/3924          
c   -- var.elim.:  3000/3924          
c   -- var.elim.:  3924/3924          
c   -- var.elim.:  1000/2971          
c   -- var.elim.:  2000/2971          
c   -- var.elim.:  2971/2971          
c   -- var.elim.:  1000/2518          
c   -- var.elim.:  2000/2518          
c   -- var.elim.:  2518/2518          
c   -- var.elim.:  1000/2089          
c   -- var.elim.:  2000/2089          
c   -- var.elim.:  2089/2089          
c   -- var.elim.:  262/262          
c   -- var.elim.:  22/22          
c   -- subsuming                       
c   -- var.elim.:  1000/1399          
c   -- var.elim.:  1399/1399          
c   -- var.elim.:  5/5          
c |     34847 |   11417    75080 |      --   10163       --      -- |     --   | -22386/-53290
c |     34847 |   11417    75080 |    4566    3312   276535    83.5 | 27.468 % |
c |     34948 |   11417    75080 |    5023    3413   315421    92.4 | 28.970 % |
c |     35100 |   11417    75080 |    5525    3565   374894   105.2 | 28.970 % |
c |     35329 |   11417    75080 |    6078    3794   525269   138.4 | 28.971 % |
c |     35667 |   11417    75080 |    6686    4132   769628   186.3 | 28.970 % |
c |     36175 |   11379    74794 |    7330    4639  1112412   239.8 | 29.190 % |
c |     36936 |   11379    74794 |    8063    5400  1693868   313.7 | 29.190 % |
c |     38075 |   11301    74075 |    8808    6537  2396949   366.7 | 29.739 % |
c |     39786 |   10397    65769 |    8914    8193  3656273   446.3 | 36.064 % |
c |     42353 |   10302    64879 |    9716   10747  5714446   531.7 | 36.660 % |
c |     46198 |   10272    64651 |   10657   10376  5916279   570.2 | 36.880 % |
c |     51965 |   10227    64170 |   11671   11449  5977624   522.1 | 37.210 % |
c |     60615 |    9970    62021 |   12516   10113  5594875   553.2 | 39.030 % |
c |     73591 |    9875    61229 |   13636   12060  7139469   592.0 | 39.689 % |
c |     93056 |    9776    59895 |   14849   14439  9234306   639.5 | 40.317 % |
c |    122248 |    9469    57170 |   15821   13288  6548869   492.8 | 42.483 % |
c |    166037 |    9240    55067 |   16983   17152  8820399   514.2 | 44.131 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 x3 -x4 -x5 -x6 x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 x15 -x16 -x17 -x18 x19 -x20 -x21 -x22 x23 -x24 -x25 -x26 x27 -x28 -x29 -x30 x31 -x32 x33 -x34 -x35 -x36 x37 -x38 -x39 -x40 -x41 -x42 x43 -x44 -x45 -x46 x47 -x48 x49 -x50 -x51 -x52 x53 -x54 -x55 -x56 x57 -x58 -x59 -x60 x61 -x62 -x63 x64 -x65 -x66 x67 -x68 -x69 -x70 x71 -x72 x73 -x74 -x75 -x76 -x77 -x78 x79 -x80 x81 -x82 -x83 -x84 -x85 -x86 x87 -x88 x89 -x90 -x91 x92 -x93 -x94 x95 -x96 x97 -x98 -x99 -x100 x101 -x102 -x103 x104 -x105 -x106 x107 -x108 x109 -x110 -x111 -x112 x113 -x114 -x115 -x116 x117 -x118 -x119 -x120 x121 -x122 -x123 -x124 x125 -x126 -x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 -x139 x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 -x161 x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 x203 -x204 -x205 x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x24#### 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.91 0.95 0.90 2/53 13525
Raw data (stat): 13525 (runsolver) R 13524 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480158289 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.92 0.95 0.90 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 3812 0 0 0 986 12 0 0 25 0 1 0 480158289 17727488 3697 4294967295 134512640 134672761 3221224576 3221223024 134643532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4328 3697 603 41 0 4287 0
vsize: 17312
[startup+20.0023 s]
Raw data (loadavg): 0.93 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 3904 0 0 0 1980 19 0 0 25 0 1 0 480158289 18145280 3789 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3789 603 41 0 4389 0
vsize: 17720
[startup+30.0032 s]
Raw data (loadavg): 0.94 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 3905 0 0 0 2980 19 0 0 25 0 1 0 480158289 18145280 3790 4294967295 134512640 134672761 3221224576 3221223120 134621051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3790 603 41 0 4389 0
vsize: 17720
[startup+40.0039 s]
Raw data (loadavg): 0.95 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 5727 0 0 0 3971 28 0 0 25 0 1 0 480158289 23371776 4841 4294967295 134512640 134672761 3221224576 3221223024 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5706 4841 603 41 0 5665 0
vsize: 22824
[startup+50.0047 s]
Raw data (loadavg): 0.96 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 5738 0 0 0 4966 32 0 0 25 0 1 0 480158289 23371776 4852 4294967295 134512640 134672761 3221224576 3221223056 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5706 4852 603 41 0 5665 0
vsize: 22824
[startup+60.0054 s]
Raw data (loadavg): 0.96 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 5835 0 0 0 5965 34 0 0 25 0 1 0 480158289 23543808 4898 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5748 4898 603 41 0 5707 0
vsize: 22992
[startup+70.0064 s]
Raw data (loadavg): 0.97 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 9154 0 0 0 6948 50 0 0 25 0 1 0 480158289 31072256 7054 4294967295 134512640 134672761 3221224576 3221222856 1075352977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7586 7054 603 41 0 7545 0
vsize: 30344
[startup+80.0069 s]
Raw data (loadavg): 0.97 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 9154 0 0 0 7941 57 0 0 25 0 1 0 480158289 31072256 7054 4294967295 134512640 134672761 3221224576 3221223024 134643771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7586 7054 603 41 0 7545 0
vsize: 30344
[startup+90.0067 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 9155 0 0 0 8940 59 0 0 25 0 1 0 480158289 31072256 7055 4294967295 134512640 134672761 3221224576 3221223712 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7586 7055 603 41 0 7545 0
vsize: 30344
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 9719 0 0 0 9939 60 0 0 25 0 1 0 480158289 33394688 7619 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8153 7619 603 41 0 8112 0
vsize: 32612
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 16011 0 0 0 10913 85 0 0 25 0 1 0 480158289 44720128 9391 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10918 9391 603 41 0 10877 0
vsize: 43672
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 16011 0 0 0 11907 91 0 0 25 0 1 0 480158289 44720128 9391 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 9391 603 41 0 10877 0
vsize: 43672
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 16011 0 0 0 12907 91 0 0 25 0 1 0 480158289 44720128 9391 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10918 9391 603 41 0 10877 0
vsize: 43672
[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 20744 0 0 0 13881 117 0 0 25 0 1 0 480158289 44826624 9675 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10944 9675 603 41 0 10903 0
vsize: 43776
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 20744 0 0 0 14877 120 0 0 25 0 1 0 480158289 44826624 9675 4294967295 134512640 134672761 3221224576 3221223776 134619616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10944 9675 603 41 0 10903 0
vsize: 43776
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 20744 0 0 0 15877 120 0 0 25 0 1 0 480158289 44826624 9675 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10944 9675 603 41 0 10903 0
vsize: 43776
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 21728 0 0 0 16875 123 0 0 25 0 1 0 480158289 48877568 10659 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11933 10659 603 41 0 11892 0
vsize: 47732
[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 22728 0 0 0 17871 127 0 0 25 0 1 0 480158289 53063680 11659 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12955 11659 603 41 0 12914 0
vsize: 51820
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 24469 0 0 0 18867 131 0 0 25 0 1 0 480158289 60137472 13400 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14682 13400 603 41 0 14641 0
vsize: 58728
[startup+200.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 25713 0 0 0 19864 134 0 0 25 0 1 0 480158289 65286144 14644 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15939 14644 603 41 0 15898 0
vsize: 63756
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 34036 0 0 0 20830 167 0 0 25 0 1 0 480158289 68583424 15781 4294967295 134512640 134672761 3221224576 3221223056 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16744 15781 603 41 0 16703 0
vsize: 66976
[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 34036 0 0 0 21827 170 0 0 25 0 1 0 480158289 68407296 15758 4294967295 134512640 134672761 3221224576 3221223120 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 15758 603 41 0 16660 0
vsize: 66804
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 34076 0 0 0 22827 170 0 0 25 0 1 0 480158289 68407296 15760 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 15760 603 41 0 16660 0
vsize: 66804
[startup+240.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 34076 0 0 0 23827 170 0 0 25 0 1 0 480158289 68407296 15760 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 15760 603 41 0 16660 0
vsize: 66804
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 34076 0 0 0 24827 170 0 0 25 0 1 0 480158289 68407296 15760 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 15760 603 41 0 16660 0
vsize: 66804
[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 34076 0 0 0 25828 170 0 0 25 0 1 0 480158289 68407296 15760 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 15760 603 41 0 16660 0
vsize: 66804
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 34076 0 0 0 26828 170 0 0 25 0 1 0 480158289 68407296 15760 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 15760 603 41 0 16660 0
vsize: 66804
[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 35519 0 0 0 27824 174 0 0 25 0 1 0 480158289 74354688 17203 4294967295 134512640 134672761 3221224576 3221223448 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18153 17205 603 41 0 18112 0
vsize: 72612
[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 35846 0 0 0 28824 175 0 0 25 0 1 0 480158289 75661312 17530 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18472 17530 603 41 0 18431 0
vsize: 73888
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42563 0 0 0 29793 206 0 0 25 0 1 0 480158289 75882496 17911 4294967295 134512640 134672761 3221224576 3221223024 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18526 17911 603 41 0 18485 0
vsize: 74104
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42563 0 0 0 30786 212 0 0 25 0 1 0 480158289 75882496 17911 4294967295 134512640 134672761 3221224576 3221223024 134643969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18526 17911 603 41 0 18485 0
vsize: 74104
[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42601 0 0 0 31786 212 0 0 25 0 1 0 480158289 75710464 17882 4294967295 134512640 134672761 3221224576 3221223616 134612966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17882 603 41 0 18443 0
vsize: 73936
[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 32786 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 33786 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 34787 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 35787 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 36787 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 37787 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223568 134603098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 38788 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 39788 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42602 0 0 0 40788 212 0 0 25 0 1 0 480158289 75710464 17883 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17883 603 41 0 18443 0
vsize: 73936
[startup+420.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42603 0 0 0 41788 212 0 0 25 0 1 0 480158289 75710464 17884 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17884 603 41 0 18443 0
vsize: 73936
[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42603 0 0 0 42788 212 0 0 25 0 1 0 480158289 75710464 17884 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17884 603 41 0 18443 0
vsize: 73936
[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42603 0 0 0 43789 212 0 0 25 0 1 0 480158289 75710464 17884 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17884 603 41 0 18443 0
vsize: 73936
[startup+450.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 42603 0 0 0 44789 212 0 0 25 0 1 0 480158289 75710464 17884 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18484 17884 603 41 0 18443 0
vsize: 73936
[startup+460.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 43076 0 0 0 45788 213 0 0 25 0 1 0 480158289 77656064 18357 4294967295 134512640 134672761 3221224576 3221223568 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18959 18357 603 41 0 18918 0
vsize: 75836
[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 43076 0 0 0 46788 213 0 0 25 0 1 0 480158289 77656064 18357 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18959 18357 603 41 0 18918 0
vsize: 75836
[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 43076 0 0 0 47789 213 0 0 25 0 1 0 480158289 77656064 18357 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18959 18357 603 41 0 18918 0
vsize: 75836
[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 43895 0 0 0 48787 215 0 0 25 0 1 0 480158289 81018880 19176 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19780 19176 603 41 0 19739 0
vsize: 79120
[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44232 0 0 0 49786 216 0 0 25 0 1 0 480158289 82501632 19512 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20142 19512 603 41 0 20101 0
vsize: 80568
[startup+510.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44232 0 0 0 50786 216 0 0 25 0 1 0 480158289 82501632 19512 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20142 19512 603 41 0 20101 0
vsize: 80568
[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44232 0 0 0 51787 216 0 0 25 0 1 0 480158289 82501632 19512 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20142 19512 603 41 0 20101 0
vsize: 80568
[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44415 0 0 0 52787 217 0 0 25 0 1 0 480158289 83283968 19695 4294967295 134512640 134672761 3221224576 3221223672 134616108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20333 19695 603 41 0 20292 0
vsize: 81332
[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44415 0 0 0 53787 217 0 0 25 0 1 0 480158289 83251200 19695 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20325 19695 603 41 0 20284 0
vsize: 81300
[startup+550.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44415 0 0 0 54787 217 0 0 25 0 1 0 480158289 83251200 19695 4294967295 134512640 134672761 3221224576 3221223616 134614271 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20325 19695 603 41 0 20284 0
vsize: 81300
[startup+560.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44415 0 0 0 55787 217 0 0 25 0 1 0 480158289 83251200 19695 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20325 19695 603 41 0 20284 0
vsize: 81300
[startup+570.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44415 0 0 0 56787 217 0 0 25 0 1 0 480158289 83251200 19695 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20325 19695 603 41 0 20284 0
vsize: 81300
[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44730 0 0 0 57786 218 0 0 25 0 1 0 480158289 84541440 20010 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20010 603 41 0 20599 0
vsize: 82560
[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44730 0 0 0 58787 218 0 0 25 0 1 0 480158289 84541440 20010 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20010 603 41 0 20599 0
vsize: 82560
[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44730 0 0 0 59787 218 0 0 25 0 1 0 480158289 84541440 20010 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20010 603 41 0 20599 0
vsize: 82560
[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44730 0 0 0 60787 218 0 0 25 0 1 0 480158289 84541440 20010 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20010 603 41 0 20599 0
vsize: 82560
[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44730 0 0 0 61787 218 0 0 25 0 1 0 480158289 84541440 20010 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20010 603 41 0 20599 0
vsize: 82560
[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44730 0 0 0 62788 218 0 0 25 0 1 0 480158289 84541440 20010 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20010 603 41 0 20599 0
vsize: 82560
[startup+640.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44730 0 0 0 63788 218 0 0 25 0 1 0 480158289 84541440 20010 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20010 603 41 0 20599 0
vsize: 82560
[startup+650.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 44731 0 0 0 64788 218 0 0 25 0 1 0 480158289 84541440 20011 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20640 20011 603 41 0 20599 0
vsize: 82560
[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 45452 0 0 0 65787 220 0 0 25 0 1 0 480158289 87478272 20732 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21357 20732 603 41 0 21316 0
vsize: 85428
[startup+670.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 45452 0 0 0 66787 220 0 0 25 0 1 0 480158289 87478272 20732 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21357 20732 603 41 0 21316 0
vsize: 85428
[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 45452 0 0 0 67788 220 0 0 25 0 1 0 480158289 87478272 20732 4294967295 134512640 134672761 3221224576 3221223616 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21357 20732 603 41 0 21316 0
vsize: 85428
[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 45452 0 0 0 68788 220 0 0 25 0 1 0 480158289 87478272 20732 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21357 20732 603 41 0 21316 0
vsize: 85428
[startup+700.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 45452 0 0 0 69788 220 0 0 25 0 1 0 480158289 87478272 20732 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21357 20732 603 41 0 21316 0
vsize: 85428
[startup+710.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 45985 0 0 0 70786 222 0 0 25 0 1 0 480158289 89694208 21265 4294967295 134512640 134672761 3221224576 3221223592 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21898 21265 603 41 0 21857 0
vsize: 87592
[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46364 0 0 0 71785 223 0 0 25 0 1 0 480158289 91217920 21644 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21644 603 41 0 22229 0
vsize: 89080
[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46364 0 0 0 72786 223 0 0 25 0 1 0 480158289 91217920 21644 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21644 603 41 0 22229 0
vsize: 89080
[startup+740.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46364 0 0 0 73786 223 0 0 25 0 1 0 480158289 91217920 21644 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21644 603 41 0 22229 0
vsize: 89080
[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46364 0 0 0 74786 223 0 0 25 0 1 0 480158289 91217920 21644 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21644 603 41 0 22229 0
vsize: 89080
[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 75786 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223712 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 76787 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 77787 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 78787 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 79787 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223616 134614209 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 80788 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223616 134613116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+820.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 81788 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+830.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 82788 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 83788 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 84789 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223776 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+860.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 85789 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+870.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 86789 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+880.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 87789 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46365 0 0 0 88790 223 0 0 25 0 1 0 480158289 91217920 21645 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21645 603 41 0 22229 0
vsize: 89080
[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 89790 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+910.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 90790 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 91790 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 92791 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 93791 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 94791 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223616 134613769 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 95791 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+970.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 96792 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223616 134614348 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+980.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 97792 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+990.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 98792 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 99792 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46366 0 0 0 100793 223 0 0 25 0 1 0 480158289 91217920 21646 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21646 603 41 0 22229 0
vsize: 89080
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 101793 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 102793 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 103793 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 104794 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 105794 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 106794 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 107794 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 108795 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 109795 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 110795 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 111795 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 112796 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 113796 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 114796 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223568 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 115796 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 116797 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 117797 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 118797 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13525
Raw data (stat): 13525 (minisat+) R 13524 7987 7986 0 -1 0 46367 0 0 0 119797 223 0 0 25 0 1 0 480158289 91217920 21647 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21647 603 41 0 22229 0
vsize: 89080
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 13525
Raw data (stat): 13525 (minisat+) Z 13524 7987 7986 0 -1 12 46368 0 0 0 119798 230 0 0 25 0 1 0 480158289 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.18
CPU time (s): 1200.29
CPU user time (s): 1197.98
CPU system time (s): 2.30965
CPU usage (%): 100.009
Max. virtual memory (Kb): 89080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####