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/synthesis-ptl-cmos-circuits/normalized-my_adder.opb
MD5SUM	fe8f615a95a6852516985b8e3e78bd85
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4561
Optimality of the best value was proved	NO
Number of terms in the objective function	577
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	24510
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	24510
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	577
Total number of constraints	1322
Number of constraints which are clauses	1306
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	16
Minimum length of a constraint	2
Maximum length of a constraint	17
Trace number 5592

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-14 00:39:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4015 boxname=wulflinc3 idbench=255 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fe8f615a95a6852516985b8e3e78bd85  /oldhome/oroussel/tmp/wulflinc3/normalized-my_adder.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc3/normalized-my_adder.opb /oldhome/oroussel/tmp/wulflinc3/normalized-my_adder.opb
IDLAUNCH: 4015
/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:        873712 kB
Buffers:         35812 kB
Cached:         102148 kB
SwapCached:       3276 kB
Active:          68556 kB
Inactive:        75500 kB
HighTotal:      131008 kB
HighFree:        24976 kB
LowTotal:       903652 kB
LowFree:        848736 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11272 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:59:38 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 4015 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1322 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 |    1322     4977 |     396       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  508/508          
c |         0 |    1322     4962 |      --       0       --      -- |     --   | 0/-15
c |         0 |    1322     4962 |     528       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.057991 s)
c ==============================================================================
c [1mFound solution: 6275[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:87830     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |  209641   491461 |   62892       1        7     7.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/79716          
c   -- var.elim.:  2000/79716          
c   -- var.elim.:  3000/79716          
c   -- var.elim.:  4000/79716          
c   -- var.elim.:  5000/79716          
c   -- var.elim.:  6000/79716          
c   -- var.elim.:  7000/79716          
c   -- var.elim.:  8000/79716          
c   -- var.elim.:  9000/79716          
c   -- var.elim.:  10000/79716          
c   -- var.elim.:  11000/79716          
c   -- var.elim.:  12000/79716          
c   -- var.elim.:  13000/79716          
c   -- var.elim.:  14000/79716          
c   -- var.elim.:  15000/79716          
c   -- var.elim.:  16000/79716          
c   -- var.elim.:  17000/79716          
c   -- var.elim.:  18000/79716          
c   -- var.elim.:  19000/79716          
c   -- var.elim.:  20000/79716          
c   -- var.elim.:  21000/79716          
c   -- var.elim.:  22000/79716          
c   -- var.elim.:  23000/79716          
c   -- var.elim.:  24000/79716          
c   -- var.elim.:  25000/79716          
c   -- var.elim.:  26000/79716          
c   -- var.elim.:  27000/79716          
c   -- var.elim.:  28000/79716          
c   -- var.elim.:  29000/79716          
c   -- var.elim.:  30000/79716          
c   -- var.elim.:  31000/79716          
c   -- var.elim.:  32000/79716          
c   -- var.elim.:  33000/79716          
c   -- var.elim.:  34000/79716          
c   -- var.elim.:  35000/79716          
c   -- var.elim.:  36000/79716          
c   -- var.elim.:  37000/79716          
c   -- var.elim.:  38000/79716          
c   -- var.elim.:  39000/79716          
c   -- var.elim.:  40000/79716          
c   -- var.elim.:  41000/79716          
c   -- var.elim.:  42000/79716          
c   -- var.elim.:  43000/79716          
c   -- var.elim.:  44000/79716          
c   -- var.elim.:  45000/79716          
c   -- var.elim.:  46000/79716          
c   -- var.elim.:  47000/79716          
c   -- var.elim.:  48000/79716          
c   -- var.elim.:  49000/79716          
c   -- var.elim.:  50000/79716          
c   -- var.elim.:  51000/79716          
c   -- var.elim.:  52000/79716          
c   -- var.elim.:  53000/79716          
c   -- var.elim.:  54000/79716          
c   -- var.elim.:  55000/79716          
c   -- var.elim.:  56000/79716          
c   -- var.elim.:  57000/79716          
c   -- var.elim.:  58000/79716          
c   -- var.elim.:  59000/79716          
c   -- var.elim.:  60000/79716          
c   -- var.elim.:  61000/79716          
c   -- var.elim.:  62000/79716          
c   -- var.elim.:  63000/79716          
c   -- var.elim.:  64000/79716          
c   -- var.elim.:  65000/79716          
c   -- var.elim.:  66000/79716          
c   -- var.elim.:  67000/79716          
c   -- var.elim.:  68000/79716          
c   -- var.elim.:  69000/79716          
c   -- var.elim.:  70000/79716          
c   -- var.elim.:  71000/79716          
c   -- var.elim.:  72000/79716          
c   -- var.elim.:  73000/79716          
c   -- var.elim.:  74000/79716          
c   -- var.elim.:  75000/79716          
c   -- var.elim.:  76000/79716          
c   -- var.elim.:  77000/79716          
c   -- var.elim.:  78000/79716          
c   -- var.elim.:  79000/79716          
c   -- var.elim.:  79716/79716          
c   -- var.elim.:  1000/42469          
c   -- var.elim.:  2000/42469          
c   -- var.elim.:  3000/42469          
c   -- var.elim.:  4000/42469          
c   -- var.elim.:  5000/42469          
c   -- var.elim.:  6000/42469          
c   -- var.elim.:  7000/42469          
c   -- var.elim.:  8000/42469          
c   -- var.elim.:  9000/42469          
c   -- var.elim.:  10000/42469          
c   -- var.elim.:  11000/42469          
c   -- var.elim.:  12000/42469          
c   -- var.elim.:  13000/42469          
c   -- var.elim.:  14000/42469          
c   -- var.elim.:  15000/42469          
c   -- var.elim.:  16000/42469          
c   -- var.elim.:  17000/42469          
c   -- var.elim.:  18000/42469          
c   -- var.elim.:  19000/42469          
c   -- var.elim.:  20000/42469          
c   -- var.elim.:  21000/42469          
c   -- var.elim.:  22000/42469          
c   -- var.elim.:  23000/42469          
c   -- var.elim.:  24000/42469          
c   -- var.elim.:  25000/42469          
c   -- var.elim.:  26000/42469          
c   -- var.elim.:  27000/42469          
c   -- var.elim.:  28000/42469          
c   -- var.elim.:  29000/42469          
c   -- var.elim.:  30000/42469          
c   -- var.elim.:  31000/42469          
c   -- var.elim.:  32000/42469          
c   -- var.elim.:  33000/42469          
c   -- var.elim.:  34000/42469          
c   -- var.elim.:  35000/42469          
c   -- var.elim.:  36000/42469          
c   -- var.elim.:  37000/42469          
c   -- var.elim.:  38000/42469          
c   -- var.elim.:  39000/42469          
c   -- var.elim.:  40000/42469          
c   -- var.elim.:  41000/42469          
c   -- var.elim.:  42000/42469          
c   -- var.elim.:  42469/42469          
c   -- var.elim.:  66/66          
c   -- subsuming                       
c   -- var.elim.:  1000/9396          
c   -- var.elim.:  2000/9396          
c   -- var.elim.:  3000/9396          
c   -- var.elim.:  4000/9396          
c   -- var.elim.:  5000/9396          
c   -- var.elim.:  6000/9396          
c   -- var.elim.:  7000/9396          
c   -- var.elim.:  8000/9396          
c   -- var.elim.:  9000/9396          
c   -- var.elim.:  9396/9396          
c   -- var.elim.:  881/881          
c   -- subsuming                       
c   -- var.elim.:  38/38          
c |         1 |  185426   668787 |      --       1       --      -- |     --   | -24215/177327
c |         1 |  185426   668787 |   74170       1        7     7.0 |  0.000 % |
c |       101 |  185426   668787 |   81587     101     2433    24.1 |  0.002 % |
c |       251 |  182093   653197 |   88133     223     3088    13.8 |  1.585 % |
c |       476 |  182093   653197 |   96946     448    17910    40.0 |  1.585 % |
c |       813 |  182093   653197 |  106640     785    20405    26.0 |  1.585 % |
c |      1320 |  181779   651768 |  117102    1290    27994    21.7 |  1.770 % |
c |      2079 |  179940   643949 |  127509    2041   136979    67.1 |  2.710 % |
c |      3218 |  179912   643734 |  140239    3155   164971    52.3 |  2.741 % |
c |      4926 |  179912   643734 |  154262    4863   214842    44.2 |  2.741 % |
c |      7490 |  179912   643734 |  169689    7427   388284    52.3 |  2.741 % |
c |     11334 |  179912   643734 |  186658   11271   588712    52.2 |  2.741 % |
c |     17100 |  179876   643388 |  205282   17032  1337539    78.5 |  2.771 % |
c ==============================================================================
c (current CPU-time: 137.321 s)
c ==============================================================================
c [1mFound solution: 6190[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:64909     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24722 |  322015   975326 |   96604   24650  3132423   127.1 |  2.771 % |
c   -- subsuming                       
c   -- var.elim.:  1000/69225          
c   -- var.elim.:  2000/69225          
c   -- var.elim.:  3000/69225          
c   -- var.elim.:  4000/69225          
c   -- var.elim.:  5000/69225          
c   -- var.elim.:  6000/69225          
c   -- var.elim.:  7000/69225          
c   -- var.elim.:  8000/69225          
c   -- var.elim.:  9000/69225          
c   -- var.elim.:  10000/69225          
c   -- var.elim.:  11000/69225          
c   -- var.elim.:  12000/69225          
c   -- var.elim.:  13000/69225          
c   -- var.elim.:  14000/69225          
c   -- var.elim.:  15000/69225          
c   -- var.elim.:  16000/69225          
c   -- var.elim.:  17000/69225          
c   -- var.elim.:  18000/69225          
c   -- var.elim.:  19000/69225          
c   -- var.elim.:  20000/69225          
c   -- var.elim.:  21000/69225          
c   -- var.elim.:  22000/69225          
c   -- var.elim.:  23000/69225          
c   -- var.elim.:  24000/69225          
c   -- var.elim.:  25000/69225          
c   -- var.elim.:  26000/69225          
c   -- var.elim.:  27000/69225          
c   -- var.elim.:  28000/69225          
c   -- var.elim.:  29000/69225          
c   -- var.elim.:  30000/69225          
c   -- var.elim.:  31000/69225          
c   -- var.elim.:  32000/69225          
c   -- var.elim.:  33000/69225          
c   -- var.elim.:  34000/69225          
c   -- var.elim.:  35000/69225          
c   -- var.elim.:  36000/69225          
c   -- var.elim.:  37000/69225          
c   -- var.elim.:  38000/69225          
c   -- var.elim.:  39000/69225          
c   -- var.elim.:  40000/69225          
c   -- var.elim.:  41000/69225          
c   -- var.elim.:  42000/69225          
c   -- var.elim.:  43000/69225          
c   -- var.elim.:  44000/69225          
c   -- var.elim.:  45000/69225          
c   -- var.elim.:  46000/69225          
c   -- var.elim.:  47000/69225          
c   -- var.elim.:  48000/69225          
c   -- var.elim.:  49000/69225          
c   -- var.elim.:  50000/69225          
c   -- var.elim.:  51000/69225          
c   -- var.elim.:  52000/69225          
c   -- var.elim.:  53000/69225          
c   -- var.elim.:  54000/69225          
c   -- var.elim.:  55000/69225          
c   -- var.elim.:  56000/69225          
c   -- var.elim.:  57000/69225          
c   -- var.elim.:  58000/69225          
c   -- var.elim.:  59000/69225          
c   -- var.elim.:  60000/69225          
c   -- var.elim.:  61000/69225          
c   -- var.elim.:  62000/69225          
c   -- var.elim.:  63000/69225          
c   -- var.elim.:  64000/69225          
c   -- var.elim.:  65000/69225          
c   -- var.elim.:  66000/69225          
c   -- var.elim.:  67000/69225          
c   -- var.elim.:  68000/69225          
c   -- var.elim.:  69000/69225          
c   -- var.elim.:  69225/69225          
c   -- var.elim.:  1000/33268          
c   -- var.elim.:  2000/33268          
c   -- var.elim.:  3000/33268          
c   -- var.elim.:  4000/33268          
c   -- var.elim.:  5000/33268          
c   -- var.elim.:  6000/33268          
c   -- var.elim.:  7000/33268          
c   -- var.elim.:  8000/33268          
c   -- var.elim.:  9000/33268          
c   -- var.elim.:  10000/33268          
c   -- var.elim.:  11000/33268          
c   -- var.elim.:  12000/33268          
c   -- var.elim.:  13000/33268          
c   -- var.elim.:  14000/33268          
c   -- var.elim.:  15000/33268          
c   -- var.elim.:  16000/33268          
c   -- var.elim.:  17000/33268          
c   -- var.elim.:  18000/33268          
c   -- var.elim.:  19000/33268          
c   -- var.elim.:  20000/33268          
c   -- var.elim.:  21000/33268          
c   -- var.elim.:  22000/33268          
c   -- var.elim.:  23000/33268          
c   -- var.elim.:  24000/33268          
c   -- var.elim.:  25000/33268          
c   -- var.elim.:  26000/33268          
c   -- var.elim.:  27000/33268          
c   -- var.elim.:  28000/33268          
c   -- var.elim.:  29000/33268          
c   -- var.elim.:  30000/33268          
c   -- var.elim.:  31000/33268          
c   -- var.elim.:  32000/33268          
c   -- var.elim.:  33000/33268          
c   -- var.elim.:  33268/33268          
c   -- subsuming                       
c   -- var.elim.:  1000/9594          
c   -- var.elim.:  2000/9594          
c   -- var.elim.:  3000/9594          
c   -- var.elim.:  4000/9594          
c   -- var.elim.:  5000/9594          
c   -- var.elim.:  6000/9594          
c   -- var.elim.:  7000/9594          
c   -- var.elim.:  8000/9594          
c   -- var.elim.:  9000/9594          
c   -- var.elim.:  9594/9594          
c   -- var.elim.:  1000/2745          
c   -- var.elim.:  2000/2745          
c   -- var.elim.:  2745/2745          
c   -- subsuming                       
c   -- var.elim.:  1000/2524          
c   -- var.elim.:  2000/2524          
c   -- var.elim.:  2524/2524          
c   -- var.elim.:  385/385          
c   -- subsuming                       
c   -- var.elim.:  12/12          
c   -- var.elim.:  7/7          
c   -- var.elim.:  11/11          
c |     24722 |  301842  1129509 |      --   24650       --      -- |     --   | -20167/154196
c |     24722 |  301842  1129509 |  120736   20432   759043    37.1 |  2.771 % |
c |     24822 |  301842  1129509 |  132810   20532   759758    37.0 |  1.709 % |
c |     24972 |  301842  1129509 |  146091   20682   761402    36.8 |  1.709 % |
c |     25197 |  301842  1129509 |  160700   20907   766385    36.7 |  1.709 % |
c |     25536 |  301842  1129509 |  176770   21246   773640    36.4 |  1.709 % |
c |     26043 |  301842  1129509 |  194447   21753   779531    35.8 |  1.709 % |
c |     26802 |  301842  1129509 |  213892   22512   813927    36.2 |  1.709 % |
c |     27941 |  301842  1129509 |  235281   23651   836411    35.4 |  1.709 % |
c |     29649 |  301842  1129509 |  258810   25359  1137812    44.9 |  1.709 % |
c |     32211 |  301842  1129509 |  284691   27921  1297614    46.5 |  1.709 % |
c |     36056 |  301842  1129509 |  313160   31766  1443821    45.5 |  1.709 % |
c |     41822 |  301842  1129509 |  344476   37532  1630592    43.4 |  1.709 % |
c |     50471 |  301842  1129509 |  378923   46181  4433168    96.0 |  1.709 % |
c |     63445 |  301723  1129109 |  416651   59147  6125926   103.6 |  1.732 % |
c ==============================================================================
c (current CPU-time: 586.273 s)
c ==============================================================================
c [1mFound solution: 6189[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     73691 |  302927  1130434 |   90878   69299  7037971   101.6 |  1.732 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3341          
c   -- var.elim.:  2000/3341          
c   -- var.elim.:  3000/3341          
c   -- var.elim.:  3341/3341          
c   -- var.elim.:  1000/2106          
c   -- var.elim.:  2000/2106          
c   -- var.elim.:  2106/2106          
c   -- var.elim.:  641/641          
c   -- subsuming                       
c   -- var.elim.:  647/647          
c   -- var.elim.:  8/8          
c |     73691 |  301969  1132548 |      --   69299       --      -- |     --   | -955/2121
c |     73691 |  301969  1132548 |  120787   64185  4727055    73.6 |  1.732 % |
c |     73792 |  301969  1132548 |  132866   64286  4728010    73.5 |  1.819 % |
c |     73942 |  301969  1132548 |  146152   64436  4728813    73.4 |  1.819 % |
c |     74167 |  301969  1132548 |  160768   64661  4730037    73.2 |  1.819 % |
c |     74507 |  301969  1132548 |  176845   65001  4734405    72.8 |  1.819 % |
c |     75013 |  301969  1132548 |  194529   65507  4741077    72.4 |  1.819 % |
c |     75772 |  301969  1132548 |  213982   66266  4760491    71.8 |  1.819 % |
c |     76913 |  301969  1132548 |  235380   67407  4783109    71.0 |  1.819 % |
c |     78622 |  301958  1132507 |  258909   69115  4813451    69.6 |  1.820 % |
c |     81184 |  301958  1132507 |  284800   71677  5079155    70.9 |  1.820 % |
c |     85028 |  301958  1132507 |  313280   75521  5308100    70.3 |  1.820 % |
c |     90797 |  301958  1132507 |  344608   81290  5444648    67.0 |  1.820 % |
c |     99446 |  301647  1128675 |  378679   89371  6334231    70.9 |  1.892 % |
c |    112420 |  301418  1127894 |  416230  102317 12389554   121.1 |  1.936 % |
c |    131881 |  301418  1127894 |  457853  121778 13375087   109.8 |  1.936 % |
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 -#### 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.85 0.95 0.90 2/54 18233
Raw data (stat): 18233 (runsolver) R 18232 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422114090 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99988 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 12523 0 0 0 965 32 0 0 25 0 1 0 422114090 56545280 11771 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13805 11771 603 41 0 13764 0
vsize: 55220
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 12652 0 0 0 1952 45 0 0 25 0 1 0 422114090 56975360 11822 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13910 11822 603 41 0 13869 0
vsize: 55640
[startup+30.0018 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 12653 0 0 0 2952 45 0 0 25 0 1 0 422114090 56188928 11731 4294967295 134512640 134672761 3221224576 3221222976 134604652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13718 11731 603 41 0 13677 0
vsize: 54872
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 12653 0 0 0 3952 45 0 0 25 0 1 0 422114090 56188928 11731 4294967295 134512640 134672761 3221224576 3221223068 134642880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13718 11731 603 41 0 13677 0
vsize: 54872
[startup+50.0035 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 12857 0 0 0 4952 46 0 0 25 0 1 0 422114090 57204736 11935 4294967295 134512640 134672761 3221224576 3221223120 134621405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13966 11935 603 41 0 13925 0
vsize: 55864
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 13409 0 0 0 5951 47 0 0 25 0 1 0 422114090 56827904 11826 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13874 11826 603 41 0 13833 0
vsize: 55496
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 13487 0 0 0 6951 48 0 0 25 0 1 0 422114090 57073664 11904 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13934 11904 603 41 0 13893 0
vsize: 55736
[startup+80.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 13667 0 0 0 7950 48 0 0 25 0 1 0 422114090 57856000 12084 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14125 12084 603 41 0 14084 0
vsize: 56500
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 13827 0 0 0 8950 49 0 0 25 0 1 0 422114090 58515456 12244 4294967295 134512640 134672761 3221224576 3221223760 134615835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14286 12244 603 41 0 14245 0
vsize: 57144
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 14221 0 0 0 9949 50 0 0 25 0 1 0 422114090 60080128 12638 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 12638 603 41 0 14627 0
vsize: 58672
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 14563 0 0 0 10947 52 0 0 25 0 1 0 422114090 61599744 12980 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 12980 603 41 0 14998 0
vsize: 60156
[startup+120.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 14858 0 0 0 11947 52 0 0 25 0 1 0 422114090 62783488 13275 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15328 13275 603 41 0 15287 0
vsize: 61312
[startup+130.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 15413 0 0 0 12945 54 0 0 25 0 1 0 422114090 64978944 13830 4294967295 134512640 134672761 3221224576 3221223616 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15864 13830 603 41 0 15823 0
vsize: 63456
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 24463 0 0 0 13919 80 0 0 25 0 1 0 422114090 101380096 20446 4294967295 134512640 134672761 3221224576 3221200216 1075349622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24751 20446 603 41 0 24710 0
vsize: 99004
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 26746 0 0 0 14909 89 0 0 25 0 1 0 422114090 105476096 21597 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25751 21597 603 41 0 25710 0
vsize: 103004
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 26796 0 0 0 15902 96 0 0 25 0 1 0 422114090 105611264 21647 4294967295 134512640 134672761 3221224576 3221223072 134636606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25784 21647 603 41 0 25743 0
vsize: 103136
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 26841 0 0 0 16896 102 0 0 25 0 1 0 422114090 105746432 21624 4294967295 134512640 134672761 3221224576 3221223024 134643468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25817 21624 603 41 0 25776 0
vsize: 103268
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 26841 0 0 0 17896 102 0 0 25 0 1 0 422114090 105746432 21624 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25817 21624 603 41 0 25776 0
vsize: 103268
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 27706 0 0 0 18895 103 0 0 25 0 1 0 422114090 110301184 22411 4294967295 134512640 134672761 3221224576 3221222560 134566476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26929 22411 603 41 0 26888 0
vsize: 107716
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 27706 0 0 0 19895 103 0 0 25 0 1 0 422114090 110301184 22411 4294967295 134512640 134672761 3221224576 3221223068 134642912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26929 22411 603 41 0 26888 0
vsize: 107716
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 27718 0 0 0 20895 103 0 0 25 0 1 0 422114090 105099264 21560 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25659 21560 603 41 0 25618 0
vsize: 102636
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 27718 0 0 0 21895 104 0 0 25 0 1 0 422114090 105099264 21560 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25659 21560 603 41 0 25618 0
vsize: 102636
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 28411 0 0 0 22893 105 0 0 25 0 1 0 422114090 105033728 21560 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25643 21560 603 41 0 25602 0
vsize: 102572
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29156 0 0 0 23892 107 0 0 25 0 1 0 422114090 105295872 21614 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25707 21614 603 41 0 25666 0
vsize: 102828
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29166 0 0 0 24892 107 0 0 25 0 1 0 422114090 105295872 21624 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25707 21624 603 41 0 25666 0
vsize: 102828
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29169 0 0 0 25891 108 0 0 25 0 1 0 422114090 105295872 21627 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25707 21627 603 41 0 25666 0
vsize: 102828
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29172 0 0 0 26891 108 0 0 25 0 1 0 422114090 105295872 21630 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25707 21630 603 41 0 25666 0
vsize: 102828
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29208 0 0 0 27891 108 0 0 25 0 1 0 422114090 105558016 21666 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25771 21666 603 41 0 25730 0
vsize: 103084
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29213 0 0 0 28891 108 0 0 25 0 1 0 422114090 105558016 21671 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25771 21671 603 41 0 25730 0
vsize: 103084
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29215 0 0 0 29891 108 0 0 25 0 1 0 422114090 105558016 21673 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25771 21673 603 41 0 25730 0
vsize: 103084
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29216 0 0 0 30892 108 0 0 25 0 1 0 422114090 105558016 21674 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25771 21674 603 41 0 25730 0
vsize: 103084
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29278 0 0 0 31892 108 0 0 25 0 1 0 422114090 105820160 21736 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25835 21736 603 41 0 25794 0
vsize: 103340
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 29801 0 0 0 32891 109 0 0 25 0 1 0 422114090 108027904 22259 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26374 22259 603 41 0 26333 0
vsize: 105496
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 30536 0 0 0 33889 111 0 0 25 0 1 0 422114090 111009792 22994 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27102 22994 603 41 0 27061 0
vsize: 108408
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 30669 0 0 0 34889 112 0 0 25 0 1 0 422114090 111542272 23127 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27232 23127 603 41 0 27191 0
vsize: 108928
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 30868 0 0 0 35888 113 0 0 25 0 1 0 422114090 112324608 23326 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27423 23326 603 41 0 27382 0
vsize: 109692
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 31352 0 0 0 36887 114 0 0 25 0 1 0 422114090 114302976 23810 4294967295 134512640 134672761 3221224576 3221223776 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27906 23810 603 41 0 27865 0
vsize: 111624
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32018 0 0 0 37885 116 0 0 25 0 1 0 422114090 117055488 24476 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28578 24476 603 41 0 28537 0
vsize: 114312
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32135 0 0 0 38884 116 0 0 25 0 1 0 422114090 117452800 24593 4294967295 134512640 134672761 3221224576 3221223616 134613022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28675 24593 603 41 0 28634 0
vsize: 114700
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32227 0 0 0 39884 117 0 0 25 0 1 0 422114090 117850112 24685 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28772 24685 603 41 0 28731 0
vsize: 115088
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32289 0 0 0 40885 117 0 0 25 0 1 0 422114090 118116352 24747 4294967295 134512640 134672761 3221224576 3221223720 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28837 24747 603 41 0 28796 0
vsize: 115348
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32300 0 0 0 41885 117 0 0 25 0 1 0 422114090 118116352 24758 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28837 24758 603 41 0 28796 0
vsize: 115348
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32321 0 0 0 42885 117 0 0 25 0 1 0 422114090 118251520 24779 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28870 24779 603 41 0 28829 0
vsize: 115480
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32343 0 0 0 43885 117 0 0 25 0 1 0 422114090 118251520 24801 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28870 24801 603 41 0 28829 0
vsize: 115480
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32384 0 0 0 44885 117 0 0 25 0 1 0 422114090 118513664 24842 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28934 24842 603 41 0 28893 0
vsize: 115736
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32423 0 0 0 45885 117 0 0 25 0 1 0 422114090 118644736 24881 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28966 24881 603 41 0 28925 0
vsize: 115864
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32475 0 0 0 46885 117 0 0 25 0 1 0 422114090 118906880 24933 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29030 24933 603 41 0 28989 0
vsize: 116120
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32554 0 0 0 47885 117 0 0 25 0 1 0 422114090 119169024 25012 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29094 25012 603 41 0 29053 0
vsize: 116376
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32616 0 0 0 48885 118 0 0 25 0 1 0 422114090 119431168 25074 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29158 25074 603 41 0 29117 0
vsize: 116632
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32666 0 0 0 49885 118 0 0 25 0 1 0 422114090 119566336 25124 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29191 25124 603 41 0 29150 0
vsize: 116764
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32708 0 0 0 50885 118 0 0 25 0 1 0 422114090 119836672 25166 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29257 25166 603 41 0 29216 0
vsize: 117028
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32770 0 0 0 51885 118 0 0 25 0 1 0 422114090 120102912 25228 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29322 25228 603 41 0 29281 0
vsize: 117288
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32808 0 0 0 52885 118 0 0 25 0 1 0 422114090 120496128 25266 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29418 25266 603 41 0 29377 0
vsize: 117672
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32895 0 0 0 53885 118 0 0 25 0 1 0 422114090 120758272 25353 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29482 25353 603 41 0 29441 0
vsize: 117928
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 32951 0 0 0 54885 119 0 0 25 0 1 0 422114090 121020416 25409 4294967295 134512640 134672761 3221224576 3221223776 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29546 25409 603 41 0 29505 0
vsize: 118184
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 33044 0 0 0 55885 119 0 0 25 0 1 0 422114090 121417728 25502 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29643 25502 603 41 0 29602 0
vsize: 118572
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 33126 0 0 0 56885 119 0 0 25 0 1 0 422114090 121794560 25584 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29735 25584 603 41 0 29694 0
vsize: 118940
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 33190 0 0 0 57885 120 0 0 25 0 1 0 422114090 122064896 25648 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29801 25648 603 41 0 29760 0
vsize: 119204
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 38587 0 0 0 58865 140 0 0 25 0 1 0 422114090 123248640 25951 4294967295 134512640 134672761 3221224576 3221223056 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30090 25951 603 41 0 30049 0
vsize: 120360
[startup+600.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39284 0 0 0 59862 142 0 0 25 0 1 0 422114090 123248640 25951 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30090 25951 603 41 0 30049 0
vsize: 120360
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39285 0 0 0 60861 142 0 0 25 0 1 0 422114090 123248640 25952 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25952 603 41 0 30049 0
vsize: 120360
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39287 0 0 0 61862 142 0 0 25 0 1 0 422114090 123248640 25954 4294967295 134512640 134672761 3221224576 3221223616 134614286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25954 603 41 0 30049 0
vsize: 120360
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39287 0 0 0 62862 142 0 0 25 0 1 0 422114090 123248640 25954 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25954 603 41 0 30049 0
vsize: 120360
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39289 0 0 0 63862 142 0 0 25 0 1 0 422114090 123248640 25956 4294967295 134512640 134672761 3221224576 3221223760 134616025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25956 603 41 0 30049 0
vsize: 120360
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39292 0 0 0 64862 142 0 0 25 0 1 0 422114090 123248640 25959 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25959 603 41 0 30049 0
vsize: 120360
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39296 0 0 0 65862 142 0 0 25 0 1 0 422114090 123248640 25963 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25963 603 41 0 30049 0
vsize: 120360
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39298 0 0 0 66862 142 0 0 25 0 1 0 422114090 123248640 25965 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25965 603 41 0 30049 0
vsize: 120360
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39299 0 0 0 67862 142 0 0 25 0 1 0 422114090 123248640 25966 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25966 603 41 0 30049 0
vsize: 120360
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39300 0 0 0 68863 142 0 0 25 0 1 0 422114090 123248640 25967 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25967 603 41 0 30049 0
vsize: 120360
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39303 0 0 0 69863 142 0 0 25 0 1 0 422114090 123248640 25970 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25970 603 41 0 30049 0
vsize: 120360
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39304 0 0 0 70863 142 0 0 25 0 1 0 422114090 123248640 25971 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25971 603 41 0 30049 0
vsize: 120360
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39305 0 0 0 71863 142 0 0 25 0 1 0 422114090 123248640 25972 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 25972 603 41 0 30049 0
vsize: 120360
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39406 0 0 0 72863 142 0 0 25 0 1 0 422114090 123768832 26073 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30217 26073 603 41 0 30176 0
vsize: 120868
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 39704 0 0 0 73862 143 0 0 25 0 1 0 422114090 124940288 26371 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30503 26371 603 41 0 30462 0
vsize: 122012
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 40342 0 0 0 74861 145 0 0 25 0 1 0 422114090 127537152 27009 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31137 27009 603 41 0 31096 0
vsize: 124548
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 41433 0 0 0 75858 148 0 0 25 0 1 0 422114090 131993600 28100 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32225 28100 603 41 0 32184 0
vsize: 128900
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 42209 0 0 0 76858 149 0 0 25 0 1 0 422114090 135184384 28876 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33004 28876 603 41 0 32963 0
vsize: 132016
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 42821 0 0 0 77856 151 0 0 25 0 1 0 422114090 137633792 29488 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33602 29488 603 41 0 33561 0
vsize: 134408
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 43683 0 0 0 78854 153 0 0 25 0 1 0 422114090 141242368 30350 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34483 30350 603 41 0 34442 0
vsize: 137932
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 44242 0 0 0 79853 154 0 0 25 0 1 0 422114090 143429632 30909 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35017 30909 603 41 0 34976 0
vsize: 140068
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 44467 0 0 0 80853 154 0 0 25 0 1 0 422114090 144449536 31134 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35266 31134 603 41 0 35225 0
vsize: 141064
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 44734 0 0 0 81853 154 0 0 25 0 1 0 422114090 145481728 31401 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35518 31401 603 41 0 35477 0
vsize: 142072
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 44865 0 0 0 82852 155 0 0 25 0 1 0 422114090 146010112 31532 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35647 31532 603 41 0 35606 0
vsize: 142588
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 45294 0 0 0 83852 156 0 0 25 0 1 0 422114090 147808256 31961 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36086 31961 603 41 0 36045 0
vsize: 144344
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 45453 0 0 0 84851 156 0 0 25 0 1 0 422114090 148459520 32120 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36245 32120 603 41 0 36204 0
vsize: 144980
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 45606 0 0 0 85851 157 0 0 25 0 1 0 422114090 148987904 32273 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36374 32273 603 41 0 36333 0
vsize: 145496
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 45787 0 0 0 86850 158 0 0 25 0 1 0 422114090 149778432 32454 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36567 32454 603 41 0 36526 0
vsize: 146268
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 45948 0 0 0 87850 158 0 0 25 0 1 0 422114090 150441984 32615 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36729 32615 603 41 0 36688 0
vsize: 146916
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46096 0 0 0 88850 159 0 0 25 0 1 0 422114090 150970368 32763 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36858 32763 603 41 0 36817 0
vsize: 147432
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46176 0 0 0 89850 159 0 0 25 0 1 0 422114090 151236608 32843 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36923 32843 603 41 0 36882 0
vsize: 147692
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46231 0 0 0 90850 159 0 0 25 0 1 0 422114090 151502848 32898 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36988 32898 603 41 0 36947 0
vsize: 147952
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46315 0 0 0 91850 160 0 0 25 0 1 0 422114090 151904256 32982 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37086 32982 603 41 0 37045 0
vsize: 148344
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46409 0 0 0 92849 160 0 0 25 0 1 0 422114090 152301568 33076 4294967295 134512640 134672761 3221224576 3221223616 134612636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37183 33076 603 41 0 37142 0
vsize: 148732
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46468 0 0 0 93850 160 0 0 25 0 1 0 422114090 152432640 33135 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37215 33135 603 41 0 37174 0
vsize: 148860
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46547 0 0 0 94849 161 0 0 25 0 1 0 422114090 152834048 33214 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37313 33214 603 41 0 37272 0
vsize: 149252
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46705 0 0 0 95849 161 0 0 25 0 1 0 422114090 154013696 33372 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37601 33372 603 41 0 37560 0
vsize: 150404
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 46955 0 0 0 96849 162 0 0 25 0 1 0 422114090 154939392 33622 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37827 33622 603 41 0 37786 0
vsize: 151308
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 47309 0 0 0 97848 162 0 0 25 0 1 0 422114090 156389376 33976 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38181 33976 603 41 0 38140 0
vsize: 152724
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 47880 0 0 0 98847 164 0 0 25 0 1 0 422114090 158826496 34547 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38776 34547 603 41 0 38735 0
vsize: 155104
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 48582 0 0 0 99846 165 0 0 25 0 1 0 422114090 161652736 35249 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39466 35249 603 41 0 39425 0
vsize: 157864
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 49152 0 0 0 100844 166 0 0 25 0 1 0 422114090 163942400 35819 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40025 35819 603 41 0 39984 0
vsize: 160100
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 49494 0 0 0 101844 167 0 0 25 0 1 0 422114090 165384192 36161 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40377 36161 603 41 0 40336 0
vsize: 161508
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 49932 0 0 0 102843 169 0 0 25 0 1 0 422114090 167190528 36599 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40818 36599 603 41 0 40777 0
vsize: 163272
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 50587 0 0 0 103841 170 0 0 25 0 1 0 422114090 169873408 37254 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41473 37254 603 41 0 41432 0
vsize: 165892
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 51037 0 0 0 104841 171 0 0 25 0 1 0 422114090 171671552 37704 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41912 37704 603 41 0 41871 0
vsize: 167648
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 52074 0 0 0 105838 173 0 0 25 0 1 0 422114090 175976448 38741 4294967295 134512640 134672761 3221224576 3221223584 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42963 38741 603 41 0 42922 0
vsize: 171852
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 52688 0 0 0 106837 175 0 0 25 0 1 0 422114090 178491392 39355 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43577 39355 603 41 0 43536 0
vsize: 174308
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 53028 0 0 0 107836 176 0 0 25 0 1 0 422114090 179826688 39695 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43903 39695 603 41 0 43862 0
vsize: 175612
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 53348 0 0 0 108836 177 0 0 25 0 1 0 422114090 181137408 40015 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44223 40015 603 41 0 44182 0
vsize: 176892
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 53829 0 0 0 109834 179 0 0 25 0 1 0 422114090 183103488 40496 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44703 40496 603 41 0 44662 0
vsize: 178812
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 54231 0 0 0 110833 180 0 0 25 0 1 0 422114090 184819712 40898 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45122 40898 603 41 0 45081 0
vsize: 180488
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 54704 0 0 0 111831 181 0 0 25 0 1 0 422114090 186634240 41371 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45565 41371 603 41 0 45524 0
vsize: 182260
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 55104 0 0 0 112830 183 0 0 25 0 1 0 422114090 188329984 41771 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45979 41771 603 41 0 45938 0
vsize: 183916
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 55493 0 0 0 113829 184 0 0 25 0 1 0 422114090 189902848 42160 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46363 42160 603 41 0 46322 0
vsize: 185452
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 55793 0 0 0 114829 185 0 0 25 0 1 0 422114090 191086592 42460 4294967295 134512640 134672761 3221224576 3221223616 134612630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46652 42460 603 41 0 46611 0
vsize: 186608
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 56055 0 0 0 115828 185 0 0 25 0 1 0 422114090 192151552 42722 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46912 42722 603 41 0 46871 0
vsize: 187648
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 56390 0 0 0 116828 186 0 0 25 0 1 0 422114090 193597440 43057 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47265 43057 603 41 0 47224 0
vsize: 189060
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 56749 0 0 0 117827 187 0 0 25 0 1 0 422114090 195055616 43416 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47621 43416 603 41 0 47580 0
vsize: 190484
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 57197 0 0 0 118826 188 0 0 25 0 1 0 422114090 196907008 43864 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48073 43864 603 41 0 48032 0
vsize: 192292
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18233
Raw data (stat): 18233 (minisat+) R 18232 10720 10719 0 -1 0 57793 0 0 0 119825 190 0 0 25 0 1 0 422114090 199335936 44460 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48666 44460 603 41 0 48625 0
vsize: 194664
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 18233
Raw data (stat): 18233 (minisat+) Z 18232 10720 10719 0 -1 12 57794 0 0 0 119825 200 0 0 25 0 1 0 422114090 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.14
CPU time (s): 1200.26
CPU user time (s): 1198.25
CPU system time (s): 2.00669
CPU usage (%): 100.01
Max. virtual memory (Kb): 194664
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####