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-c8.opb
MD5SUM	9b291040ec2b77d0bffb739c0db80d53
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1194
Optimality of the best value was proved	NO
Number of terms in the objective function	239
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	10012
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	10012
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.941856
Number of variables	239
Total number of constraints	524
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	4
Minimum length of a constraint	1
Maximum length of a constraint	36
Trace number 5585

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-14 00:37:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4010 boxname=wulflinc1 idbench=250 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9b291040ec2b77d0bffb739c0db80d53  /oldhome/oroussel/tmp/wulflinc1/normalized-c8.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc1/normalized-c8.opb /oldhome/oroussel/tmp/wulflinc1/normalized-c8.opb
IDLAUNCH: 4010
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        851752 kB
Buffers:         40528 kB
Cached:         118184 kB
SwapCached:          0 kB
Active:         106940 kB
Inactive:        54944 kB
HighTotal:      131008 kB
HighFree:        20020 kB
LowTotal:       903652 kB
LowFree:        831732 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15232 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:57:37 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4010 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 519 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 |     514     2268 |     154       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  211/211          
c |         0 |     507     2234 |      --       0       --      -- |     --   | -7/-34
c |         0 |     507     2234 |     202       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.027995 s)
c ==============================================================================
c [1mFound solution: 1728[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29494     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |   71811   168702 |   21543       1       14    14.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/26458          
c   -- var.elim.:  2000/26458          
c   -- var.elim.:  3000/26458          
c   -- var.elim.:  4000/26458          
c   -- var.elim.:  5000/26458          
c   -- var.elim.:  6000/26458          
c   -- var.elim.:  7000/26458          
c   -- var.elim.:  8000/26458          
c   -- var.elim.:  9000/26458          
c   -- var.elim.:  10000/26458          
c   -- var.elim.:  11000/26458          
c   -- var.elim.:  12000/26458          
c   -- var.elim.:  13000/26458          
c   -- var.elim.:  14000/26458          
c   -- var.elim.:  15000/26458          
c   -- var.elim.:  16000/26458          
c   -- var.elim.:  17000/26458          
c   -- var.elim.:  18000/26458          
c   -- var.elim.:  19000/26458          
c   -- var.elim.:  20000/26458          
c   -- var.elim.:  21000/26458          
c   -- var.elim.:  22000/26458          
c   -- var.elim.:  23000/26458          
c   -- var.elim.:  24000/26458          
c   -- var.elim.:  25000/26458          
c   -- var.elim.:  26000/26458          
c   -- var.elim.:  26458/26458          
c   -- var.elim.:  1000/14309          
c   -- var.elim.:  2000/14309          
c   -- var.elim.:  3000/14309          
c   -- var.elim.:  4000/14309          
c   -- var.elim.:  5000/14309          
c   -- var.elim.:  6000/14309          
c   -- var.elim.:  7000/14309          
c   -- var.elim.:  8000/14309          
c   -- var.elim.:  9000/14309          
c   -- var.elim.:  10000/14309          
c   -- var.elim.:  11000/14309          
c   -- var.elim.:  12000/14309          
c   -- var.elim.:  13000/14309          
c   -- var.elim.:  14000/14309          
c   -- var.elim.:  14309/14309          
c   -- subsuming                       
c   -- var.elim.:  1000/2256          
c   -- var.elim.:  2000/2256          
c   -- var.elim.:  2256/2256          
c   -- var.elim.:  782/782          
c   -- subsuming                       
c   -- var.elim.:  269/269          
c |         1 |   64059   206483 |      --       1       --      -- |     --   | -7752/37782
c |         1 |   64059   206483 |   25623       1       14    14.0 |  0.000 % |
c |       101 |   64026   205876 |   28171     100     1567    15.7 |  0.042 % |
c |       251 |   64026   205876 |   30988     250     8648    34.6 |  0.042 % |
c |       476 |   62848   201626 |   33460     468    19185    41.0 |  1.366 % |
c |       813 |   62640   200930 |   36684     802    29686    37.0 |  1.562 % |
c |      1320 |   62301   199802 |   40134    1307    35411    27.1 |  2.024 % |
c |      2079 |   62301   199802 |   44148    2066   193387    93.6 |  2.024 % |
c |      3218 |   62301   199802 |   48562    3205   315576    98.5 |  2.024 % |
c |      4926 |   62252   199637 |   53377    4912   402667    82.0 |  2.094 % |
c |      7488 |   62200   199473 |   58665    7472   820127   109.8 |  2.164 % |
c ==============================================================================
c (current CPU-time: 29.5105 s)
c ==============================================================================
c [1mFound solution: 1688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24438     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8870 |  123766   343334 |   37129    8853   951485   107.5 |  2.164 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24731          
c   -- var.elim.:  2000/24731          
c   -- var.elim.:  3000/24731          
c   -- var.elim.:  4000/24731          
c   -- var.elim.:  5000/24731          
c   -- var.elim.:  6000/24731          
c   -- var.elim.:  7000/24731          
c   -- var.elim.:  8000/24731          
c   -- var.elim.:  9000/24731          
c   -- var.elim.:  10000/24731          
c   -- var.elim.:  11000/24731          
c   -- var.elim.:  12000/24731          
c   -- var.elim.:  13000/24731          
c   -- var.elim.:  14000/24731          
c   -- var.elim.:  15000/24731          
c   -- var.elim.:  16000/24731          
c   -- var.elim.:  17000/24731          
c   -- var.elim.:  18000/24731          
c   -- var.elim.:  19000/24731          
c   -- var.elim.:  20000/24731          
c   -- var.elim.:  21000/24731          
c   -- var.elim.:  22000/24731          
c   -- var.elim.:  23000/24731          
c   -- var.elim.:  24000/24731          
c   -- var.elim.:  24731/24731          
c   -- var.elim.:  1000/13161          
c   -- var.elim.:  2000/13161          
c   -- var.elim.:  3000/13161          
c   -- var.elim.:  4000/13161          
c   -- var.elim.:  5000/13161          
c   -- var.elim.:  6000/13161          
c   -- var.elim.:  7000/13161          
c   -- var.elim.:  8000/13161          
c   -- var.elim.:  9000/13161          
c   -- var.elim.:  10000/13161          
c   -- var.elim.:  11000/13161          
c   -- var.elim.:  12000/13161          
c   -- var.elim.:  13000/13161          
c   -- var.elim.:  13161/13161          
c   -- var.elim.:  84/84          
c   -- var.elim.:  31/31          
c   -- subsuming                       
c   -- var.elim.:  1000/1441          
c   -- var.elim.:  1441/1441          
c   -- var.elim.:  318/318          
c   -- subsuming                       
c   -- var.elim.:  227/227          
c   -- var.elim.:  136/136          
c   -- subsuming                       
c |      8870 |  117098   375361 |      --    8853       --      -- |     --   | -6664/32037
c |      8870 |  117098   375361 |   46839    7652   513277    67.1 |  2.164 % |
c |      8970 |  117098   375361 |   51523    7752   515041    66.4 |  1.218 % |
c |      9120 |  116905   374704 |   56582    7899   515844    65.3 |  1.318 % |
c |      9347 |  116905   374704 |   62240    8126   528837    65.1 |  1.318 % |
c |      9684 |  116869   374580 |   68443    8461   549605    65.0 |  1.338 % |
c |     10191 |  116568   373084 |   75093    8966   595183    66.4 |  1.477 % |
c ==============================================================================
c (current CPU-time: 44.2743 s)
c ==============================================================================
c [1mFound solution: 1674[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 |     10435 |  117271   375092 |   35181    9209   609489    66.2 |  1.477 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2309          
c   -- var.elim.:  2000/2309          
c   -- var.elim.:  2309/2309          
c   -- var.elim.:  990/990          
c   -- subsuming                       
c   -- var.elim.:  83/83          
c |     10435 |  116762   374682 |      --    9209       --      -- |     --   | -506/-403
c |     10435 |  116762   374682 |   46704    8962   569152    63.5 |  1.477 % |
c |     10536 |  116666   374379 |   51333    9062   571506    63.1 |  1.550 % |
c |     10686 |  116666   374379 |   56466    9212   583522    63.3 |  1.550 % |
c |     10911 |  116666   374379 |   62112    9437   602658    63.9 |  1.550 % |
c |     11250 |  116666   374379 |   68324    9776   633917    64.8 |  1.550 % |
c |     11756 |  116666   374379 |   75156   10282   677783    65.9 |  1.550 % |
c |     12515 |  116637   374288 |   82651   11038   772804    70.0 |  1.565 % |
c ==============================================================================
c (current CPU-time: 61.8036 s)
c ==============================================================================
c [1mFound solution: 1651[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:22388     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13067 |  172579   505120 |   51773   11588   821563    70.9 |  1.565 % |
c   -- subsuming                       
c   -- var.elim.:  1000/21419          
c   -- var.elim.:  2000/21419          
c   -- var.elim.:  3000/21419          
c   -- var.elim.:  4000/21419          
c   -- var.elim.:  5000/21419          
c   -- var.elim.:  6000/21419          
c   -- var.elim.:  7000/21419          
c   -- var.elim.:  8000/21419          
c   -- var.elim.:  9000/21419          
c   -- var.elim.:  10000/21419          
c   -- var.elim.:  11000/21419          
c   -- var.elim.:  12000/21419          
c   -- var.elim.:  13000/21419          
c   -- var.elim.:  14000/21419          
c   -- var.elim.:  15000/21419          
c   -- var.elim.:  16000/21419          
c   -- var.elim.:  17000/21419          
c   -- var.elim.:  18000/21419          
c   -- var.elim.:  19000/21419          
c   -- var.elim.:  20000/21419          
c   -- var.elim.:  21000/21419          
c   -- var.elim.:  21419/21419          
c   -- var.elim.:  1000/11681          
c   -- var.elim.:  2000/11681          
c   -- var.elim.:  3000/11681          
c   -- var.elim.:  4000/11681          
c   -- var.elim.:  5000/11681          
c   -- var.elim.:  6000/11681          
c   -- var.elim.:  7000/11681          
c   -- var.elim.:  8000/11681          
c   -- var.elim.:  9000/11681          
c   -- var.elim.:  10000/11681          
c   -- var.elim.:  11000/11681          
c   -- var.elim.:  11681/11681          
c   -- var.elim.:  365/365          
c   -- var.elim.:  488/488          
c   -- subsuming                       
c   -- var.elim.:  1000/1168          
c   -- var.elim.:  1168/1168          
c   -- var.elim.:  259/259          
c   -- subsuming                       
c   -- var.elim.:  156/156          
c   -- var.elim.:  115/115          
c   -- subsuming                       
c   -- var.elim.:  10/10          
c |     13067 |  166466   534454 |      --   11588       --      -- |     --   | -6111/29339
c |     13067 |  166466   534454 |   66586   11164   680208    60.9 |  1.565 % |
c |     13167 |  166466   534454 |   73245   11264   682230    60.6 |  1.144 % |
c |     13317 |  166466   534454 |   80569   11414   694458    60.8 |  1.144 % |
c |     13543 |  166466   534454 |   88626   11640   707714    60.8 |  1.144 % |
c ==============================================================================
c (current CPU-time: 73.2739 s)
c ==============================================================================
c [1mFound solution: 1637[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 |     13588 |  167629   537531 |   50288   11685   709105    60.7 |  1.144 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1537          
c   -- var.elim.:  1537/1537          
c   -- var.elim.:  876/876          
c   -- var.elim.:  88/88          
c   -- subsuming                       
c   -- var.elim.:  114/114          
c   -- var.elim.:  114/114          
c |     13588 |  167071   538225 |      --   11685       --      -- |     --   | -557/697
c |     13588 |  167071   538225 |   66828   11685   709105    60.7 |  1.144 % |
c ==============================================================================
c (current CPU-time: 74.6666 s)
c ==============================================================================
c [1mFound solution: 1625[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13602 |  167228   538875 |   50168   11699   710140    60.7 |  1.144 % |
c   -- subsuming                       
c   -- var.elim.:  542/542          
c   -- var.elim.:  375/375          
c   -- var.elim.:  142/142          
c   -- var.elim.:  146/146          
c |     13602 |  167111   539652 |      --   11699       --      -- |     --   | -117/778
c |     13602 |  167111   539652 |   66844   11699   710140    60.7 |  1.144 % |
c |     13702 |  167111   539652 |   73528   11799   719288    61.0 |  1.147 % |
c |     13852 |  167111   539652 |   80881   11949   725609    60.7 |  1.147 % |
c |     14078 |  167088   539569 |   88957   12174   729001    59.9 |  1.156 % |
c |     14415 |  166949   539091 |   97772   12509   741331    59.3 |  1.205 % |
c |     14921 |  166949   539091 |  107549   13015   840149    64.6 |  1.205 % |
c |     15680 |  166949   539091 |  118304   13774  1022904    74.3 |  1.205 % |
c |     16821 |  166511   537480 |  129793   14897  1111348    74.6 |  1.421 % |
c |     18529 |  166473   537336 |  142739   16602  1245131    75.0 |  1.448 % |
c ==============================================================================
c (current CPU-time: 118.185 s)
c ==============================================================================
c [1mFound solution: 1581[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19004 |  166511   537710 |   49953   17077  1278271    74.9 |  1.448 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1413          
c   -- var.elim.:  1413/1413          
c   -- var.elim.:  515/515          
c   -- var.elim.:  88/88          
c   -- subsuming                       
c   -- var.elim.:  321/321          
c |     19004 |  166439   538423 |      --   17077       --      -- |     --   | -72/714
c |     19004 |  166439   538423 |   66575   16247   979984    60.3 |  1.448 % |
c |     19104 |  166439   538423 |   73233   16347   983504    60.2 |  1.452 % |
c |     19255 |  166439   538423 |   80556   16498  1006964    61.0 |  1.452 % |
c |     19480 |  166439   538423 |   88612   16723  1014759    60.7 |  1.452 % |
c |     19817 |  166439   538423 |   97473   17060  1047303    61.4 |  1.452 % |
c |     20325 |  166416   538292 |  107205   17565  1090755    62.1 |  1.463 % |
c ==============================================================================
c (current CPU-time: 132.422 s)
c ==============================================================================
c [1mFound solution: 1548[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     20884 |  166783   539436 |   50034   18118  1109398    61.2 |  1.463 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1048          
c   -- var.elim.:  1048/1048          
c   -- var.elim.:  634/634          
c   -- var.elim.:  254/254          
c   -- subsuming                       
c   -- var.elim.:  35/35          
c |     20884 |  166531   540344 |      --   18118       --      -- |     --   | -248/917
c |     20884 |  166531   540344 |   66612   18099  1107768    61.2 |  1.463 % |
c |     20984 |  166531   540344 |   73273   18199  1111729    61.1 |  1.497 % |
c |     21135 |  166531   540344 |   80601   18350  1116784    60.9 |  1.497 % |
c |     21362 |  166531   540344 |   88661   18577  1131002    60.9 |  1.497 % |
c |     21700 |  166042   532392 |   97240   18911  1156840    61.2 |  1.678 % |
c |     22207 |  166042   532392 |  106964   19418  1181074    60.8 |  1.678 % |
c |     22968 |  166042   532392 |  117661   20179  1237202    61.3 |  1.678 % |
c |     24113 |  166042   532392 |  129427   21324  1286390    60.3 |  1.678 % |
c |     25821 |  166042   532392 |  142370   23032  1436275    62.4 |  1.678 % |
c |     28384 |  166042   532392 |  156607   25595  1558724    60.9 |  1.678 % |
c ==============================================================================
c (current CPU-time: 194.313 s)
c ==============================================================================
c [1mFound solution: 1544[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 |     29399 |  166099   532791 |   49829   26610  1776601    66.8 |  1.678 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1863          
c   -- var.elim.:  1863/1863          
c   -- var.elim.:  1000/1227          
c   -- var.elim.:  1227/1227          
c   -- var.elim.:  307/307          
c   -- subsuming                       
c   -- var.elim.:  266/266          
c |     29399 |  165891   535278 |      --   26610       --      -- |     --   | -204/2496
c |     29399 |  165891   535278 |   66356   25321  1296981    51.2 |  1.678 % |
c |     29500 |  165891   535278 |   72992   25422  1300636    51.2 |  1.735 % |
c |     29654 |  165891   535278 |   80291   25576  1307665    51.1 |  1.735 % |
c |     29879 |  165891   535278 |   88320   25801  1353107    52.4 |  1.735 % |
c |     30216 |  165891   535278 |   97152   26138  1357322    51.9 |  1.735 % |
c |     30725 |  165665   534502 |  106722   26637  1383046    51.9 |  1.817 % |
c |     31484 |  165570   534187 |  117326   27376  1395089    51.0 |  1.858 % |
c |     32623 |  165489   533686 |  128996   28499  1436953    50.4 |  1.896 % |
c |     34332 |  165459   533587 |  141870   30186  1586353    52.6 |  1.910 % |
c |     36894 |  165459   533587 |  156057   32748  1775362    54.2 |  1.910 % |
c |     40738 |  165459   533587 |  171663   36592  3069905    83.9 |  1.910 % |
c ==============================================================================
c (current CPU-time: 275.616 s)
c ==============================================================================
c [1mFound solution: 1538[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     42458 |  165493   533902 |   49647   38312  3462903    90.4 |  1.910 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1005          
c   -- var.elim.:  1005/1005          
c   -- var.elim.:  549/549          
c   -- var.elim.:  89/89          
c   -- subsuming                       
c   -- var.elim.:  7/7          
c   -- var.elim.:  7/7          
c |     42458 |  165425   534349 |      --   38312       --      -- |     --   | -68/448
c |     42458 |  165425   534349 |   66170   36883  2696024    73.1 |  1.910 % |
c |     42558 |  165425   534349 |   72787   36983  2700158    73.0 |  1.915 % |
c |     42710 |  165425   534349 |   80065   37135  2725566    73.4 |  1.915 % |
c |     42935 |  165425   534349 |   88072   37360  2732738    73.1 |  1.915 % |
c |     43272 |  165414   534302 |   96873   37696  2746219    72.9 |  1.923 % |
c |     43778 |  165414   534302 |  106560   38202  2811270    73.6 |  1.923 % |
c |     44538 |  165414   534302 |  117216   38962  3086395    79.2 |  1.923 % |
c ==============================================================================
c (current CPU-time: 294.407 s)
c ==============================================================================
c [1mFound solution: 1412[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 |     44596 |  165600   535033 |   49679   39020  3091166    79.2 |  1.923 % |
c   -- subsuming                       
c   -- var.elim.:  658/658          
c   -- var.elim.:  406/406          
c   -- var.elim.:  276/276          
c   -- var.elim.:  265/265          
c   -- var.elim.:  263/263          
c |     44#### 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.94 0.90 2/56 18796
Raw data (stat): 18796 (runsolver) R 18795 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 365251087 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.87 0.94 0.90 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 4516 0 0 0 983 15 0 0 25 0 1 0 365251087 20066304 4176 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4899 4176 603 41 0 4858 0
vsize: 19596
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 4871 0 0 0 1982 17 0 0 25 0 1 0 365251087 21540864 4531 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5259 4531 603 41 0 5218 0
vsize: 21036
[startup+30.0027 s]
Raw data (loadavg): 0.91 0.94 0.90 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 6151 0 0 0 2978 21 0 0 25 0 1 0 365251087 25858048 5522 4294967295 134512640 134672761 3221224576 3221222936 1075771665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6313 5522 603 41 0 6272 0
vsize: 25252
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 10055 0 0 0 3964 34 0 0 25 0 1 0 365251087 35991552 7809 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8787 7809 603 41 0 8746 0
vsize: 35148
[startup+50.002 s]
Raw data (loadavg): 0.93 0.94 0.90 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 11777 0 0 0 4959 39 0 0 25 0 1 0 365251087 37236736 8120 4294967295 134512640 134672761 3221224576 3221223616 134613015 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9091 8120 603 41 0 9050 0
vsize: 36364
[startup+60.0018 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 11779 0 0 0 5959 39 0 0 25 0 1 0 365251087 37236736 8122 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9091 8122 603 41 0 9050 0
vsize: 36364
[startup+70.002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 16571 0 0 0 6943 56 0 0 25 0 1 0 365251087 50208768 10079 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 10079 603 41 0 12217 0
vsize: 49032
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 21716 0 0 0 7925 73 0 0 25 0 1 0 365251087 50753536 10210 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12391 10210 603 41 0 12350 0
vsize: 49564
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 21717 0 0 0 8925 73 0 0 25 0 1 0 365251087 50753536 10211 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12391 10211 603 41 0 12350 0
vsize: 49564
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 21850 0 0 0 9925 74 0 0 25 0 1 0 365251087 51417088 10344 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12553 10344 603 41 0 12512 0
vsize: 50212
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 21970 0 0 0 10925 74 0 0 25 0 1 0 365251087 51810304 10464 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12649 10464 603 41 0 12608 0
vsize: 50596
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 24695 0 0 0 11916 83 0 0 25 0 1 0 365251087 54505472 10961 4294967295 134512640 134672761 3221224576 3221223120 134621071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13307 10961 603 41 0 13266 0
vsize: 53228
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 25068 0 0 0 12916 84 0 0 25 0 1 0 365251087 52346880 10588 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12780 10588 603 41 0 12739 0
vsize: 51120
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 27919 0 0 0 13905 94 0 0 25 0 1 0 365251087 52367360 10606 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12785 10606 603 41 0 12744 0
vsize: 51140
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 27920 0 0 0 14905 94 0 0 25 0 1 0 365251087 52367360 10607 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12785 10607 603 41 0 12744 0
vsize: 51140
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 27921 0 0 0 15905 94 0 0 25 0 1 0 365251087 52367360 10608 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12785 10608 603 41 0 12744 0
vsize: 51140
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 27964 0 0 0 16906 94 0 0 25 0 1 0 365251087 52629504 10651 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12849 10651 603 41 0 12808 0
vsize: 51396
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 28053 0 0 0 17906 94 0 0 25 0 1 0 365251087 53026816 10740 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12946 10740 603 41 0 12905 0
vsize: 51784
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 28213 0 0 0 18905 95 0 0 25 0 1 0 365251087 53551104 10900 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13074 10900 603 41 0 13033 0
vsize: 52296
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 31575 0 0 0 19896 104 0 0 25 0 1 0 365251087 54550528 11146 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13318 11146 603 41 0 13277 0
vsize: 53272
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18796
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 31576 0 0 0 20896 105 0 0 25 0 1 0 365251087 54550528 11147 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13318 11147 603 41 0 13277 0
vsize: 53272
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 31578 0 0 0 21895 105 0 0 25 0 1 0 365251087 54550528 11149 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13318 11149 603 41 0 13277 0
vsize: 53272
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 31654 0 0 0 22895 105 0 0 25 0 1 0 365251087 55066624 11225 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13444 11225 603 41 0 13403 0
vsize: 53776
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 31998 0 0 0 23894 106 0 0 25 0 1 0 365251087 56500224 11569 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13794 11569 603 41 0 13753 0
vsize: 55176
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 32368 0 0 0 24893 108 0 0 25 0 1 0 365251087 57954304 11939 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14149 11939 603 41 0 14108 0
vsize: 56596
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 32708 0 0 0 25891 109 0 0 25 0 1 0 365251087 59408384 12279 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14504 12279 603 41 0 14463 0
vsize: 58016
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 33073 0 0 0 26890 111 0 0 25 0 1 0 365251087 60862464 12644 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14859 12644 603 41 0 14818 0
vsize: 59436
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 36505 0 0 0 27879 122 0 0 25 0 1 0 365251087 62038016 12953 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 12953 603 41 0 15105 0
vsize: 60584
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 36505 0 0 0 28879 122 0 0 25 0 1 0 365251087 62038016 12953 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 12953 603 41 0 15105 0
vsize: 60584
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 38944 0 0 0 29872 129 0 0 25 0 1 0 365251087 62050304 12959 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15149 12959 603 41 0 15108 0
vsize: 60596
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 38945 0 0 0 30872 130 0 0 25 0 1 0 365251087 62050304 12960 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15149 12960 603 41 0 15108 0
vsize: 60596
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 38946 0 0 0 31872 130 0 0 25 0 1 0 365251087 62050304 12961 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15149 12961 603 41 0 15108 0
vsize: 60596
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 38947 0 0 0 32872 130 0 0 25 0 1 0 365251087 62050304 12962 4294967295 134512640 134672761 3221224576 3221223776 134610703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15149 12962 603 41 0 15108 0
vsize: 60596
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39005 0 0 0 33872 130 0 0 25 0 1 0 365251087 62312448 13020 4294967295 134512640 134672761 3221224576 3221223760 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15213 13020 603 41 0 15172 0
vsize: 60852
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39074 0 0 0 34871 131 0 0 25 0 1 0 365251087 62574592 13089 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15277 13089 603 41 0 15236 0
vsize: 61108
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39180 0 0 0 35871 131 0 0 25 0 1 0 365251087 63098880 13195 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15405 13195 603 41 0 15364 0
vsize: 61620
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39287 0 0 0 36871 132 0 0 25 0 1 0 365251087 63492096 13302 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15501 13302 603 41 0 15460 0
vsize: 62004
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39400 0 0 0 37870 132 0 0 25 0 1 0 365251087 63889408 13415 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15598 13415 603 41 0 15557 0
vsize: 62392
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39529 0 0 0 38869 133 0 0 25 0 1 0 365251087 64425984 13544 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15729 13544 603 41 0 15688 0
vsize: 62916
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39639 0 0 0 39869 134 0 0 25 0 1 0 365251087 64962560 13654 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15860 13654 603 41 0 15819 0
vsize: 63440
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39828 0 0 0 40868 134 0 0 25 0 1 0 365251087 65748992 13843 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16052 13843 603 41 0 16011 0
vsize: 64208
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 39965 0 0 0 41868 135 0 0 25 0 1 0 365251087 66285568 13980 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16183 13980 603 41 0 16142 0
vsize: 64732
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40115 0 0 0 42868 135 0 0 25 0 1 0 365251087 66805760 14130 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16310 14130 603 41 0 16269 0
vsize: 65240
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40257 0 0 0 43868 135 0 0 25 0 1 0 365251087 67461120 14272 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16470 14272 603 41 0 16429 0
vsize: 65880
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40410 0 0 0 44868 135 0 0 25 0 1 0 365251087 67989504 14425 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16599 14425 603 41 0 16558 0
vsize: 66396
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40531 0 0 0 45868 136 0 0 25 0 1 0 365251087 68517888 14546 4294967295 134512640 134672761 3221224576 3221223744 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16728 14546 603 41 0 16687 0
vsize: 66912
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40648 0 0 0 46868 136 0 0 25 0 1 0 365251087 69042176 14663 4294967295 134512640 134672761 3221224576 3221223760 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16856 14663 603 41 0 16815 0
vsize: 67424
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40749 0 0 0 47868 136 0 0 25 0 1 0 365251087 69439488 14764 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 14764 603 41 0 16912 0
vsize: 67812
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40867 0 0 0 48867 137 0 0 25 0 1 0 365251087 69963776 14882 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17081 14882 603 41 0 17040 0
vsize: 68324
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 40987 0 0 0 49867 137 0 0 25 0 1 0 365251087 70361088 15002 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17178 15002 603 41 0 17137 0
vsize: 68712
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18798
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 41151 0 0 0 50867 137 0 0 25 0 1 0 365251087 71020544 15166 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17339 15166 603 41 0 17298 0
vsize: 69356
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 41303 0 0 0 51867 138 0 0 25 0 1 0 365251087 71680000 15318 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17500 15318 603 41 0 17459 0
vsize: 70000
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 41440 0 0 0 52867 138 0 0 25 0 1 0 365251087 72208384 15455 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17629 15455 603 41 0 17588 0
vsize: 70516
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 41563 0 0 0 53867 138 0 0 25 0 1 0 365251087 72732672 15578 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17757 15578 603 41 0 17716 0
vsize: 71028
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 41748 0 0 0 54867 139 0 0 25 0 1 0 365251087 73519104 15763 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17949 15763 603 41 0 17908 0
vsize: 71796
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 41891 0 0 0 55867 139 0 0 25 0 1 0 365251087 74047488 15906 4294967295 134512640 134672761 3221224576 3221223760 134615848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18078 15906 603 41 0 18037 0
vsize: 72312
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 42127 0 0 0 56866 139 0 0 25 0 1 0 365251087 75091968 16142 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18333 16142 603 41 0 18292 0
vsize: 73332
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 42278 0 0 0 57866 140 0 0 25 0 1 0 365251087 75882496 16293 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18526 16293 603 41 0 18485 0
vsize: 74104
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 42469 0 0 0 58865 141 0 0 25 0 1 0 365251087 76673024 16484 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18719 16484 603 41 0 18678 0
vsize: 74876
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 42637 0 0 0 59866 141 0 0 25 0 1 0 365251087 77332480 16652 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18880 16652 603 41 0 18839 0
vsize: 75520
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 42739 0 0 0 60866 141 0 0 25 0 1 0 365251087 77852672 16754 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19007 16754 603 41 0 18966 0
vsize: 76028
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 42858 0 0 0 61865 142 0 0 25 0 1 0 365251087 78249984 16873 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19104 16873 603 41 0 19063 0
vsize: 76416
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 42995 0 0 0 62865 142 0 0 25 0 1 0 365251087 78913536 17010 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19266 17010 603 41 0 19225 0
vsize: 77064
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 43157 0 0 0 63865 142 0 0 25 0 1 0 365251087 79581184 17172 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19429 17172 603 41 0 19388 0
vsize: 77716
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 43327 0 0 0 64865 143 0 0 25 0 1 0 365251087 80244736 17342 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19591 17342 603 41 0 19550 0
vsize: 78364
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 43515 0 0 0 65864 143 0 0 25 0 1 0 365251087 80908288 17530 4294967295 134512640 134672761 3221224576 3221223752 134615850 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19753 17530 603 41 0 19712 0
vsize: 79012
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 43811 0 0 0 66864 144 0 0 25 0 1 0 365251087 82214912 17826 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20072 17826 603 41 0 20031 0
vsize: 80288
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 44026 0 0 0 67863 145 0 0 25 0 1 0 365251087 83017728 18041 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20268 18041 603 41 0 20227 0
vsize: 81072
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 44156 0 0 0 68863 145 0 0 25 0 1 0 365251087 83550208 18171 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20398 18171 603 41 0 20357 0
vsize: 81592
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 44265 0 0 0 69863 146 0 0 25 0 1 0 365251087 84078592 18280 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20527 18280 603 41 0 20486 0
vsize: 82108
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 44392 0 0 0 70863 146 0 0 25 0 1 0 365251087 84602880 18407 4294967295 134512640 134672761 3221224576 3221223760 134616008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20655 18407 603 41 0 20614 0
vsize: 82620
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 44526 0 0 0 71862 147 0 0 25 0 1 0 365251087 85135360 18541 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20785 18541 603 41 0 20744 0
vsize: 83140
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 44649 0 0 0 72862 147 0 0 25 0 1 0 365251087 85532672 18664 4294967295 134512640 134672761 3221224576 3221223760 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20882 18664 603 41 0 20841 0
vsize: 83528
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 44803 0 0 0 73862 147 0 0 25 0 1 0 365251087 86192128 18818 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21043 18818 603 41 0 21002 0
vsize: 84172
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 45016 0 0 0 74862 148 0 0 25 0 1 0 365251087 87109632 19031 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21267 19031 603 41 0 21226 0
vsize: 85068
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 45273 0 0 0 75862 148 0 0 25 0 1 0 365251087 88166400 19288 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21525 19288 603 41 0 21484 0
vsize: 86100
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 45498 0 0 0 76862 148 0 0 25 0 1 0 365251087 89083904 19513 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21749 19513 603 41 0 21708 0
vsize: 86996
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 45708 0 0 0 77862 148 0 0 25 0 1 0 365251087 89874432 19723 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21942 19723 603 41 0 21901 0
vsize: 87768
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 45998 0 0 0 78861 149 0 0 25 0 1 0 365251087 91058176 20013 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22231 20013 603 41 0 22190 0
vsize: 88924
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 46291 0 0 0 79859 151 0 0 25 0 1 0 365251087 92241920 20306 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22520 20306 603 41 0 22479 0
vsize: 90080
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18800
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 46535 0 0 0 80859 151 0 0 25 0 1 0 365251087 93290496 20550 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22776 20550 603 41 0 22735 0
vsize: 91104
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 46871 0 0 0 81858 153 0 0 25 0 1 0 365251087 94609408 20886 4294967295 134512640 134672761 3221224576 3221223712 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23098 20886 603 41 0 23057 0
vsize: 92392
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 47344 0 0 0 82857 154 0 0 25 0 1 0 365251087 96579584 21359 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23579 21359 603 41 0 23538 0
vsize: 94316
[startup+840.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 47652 0 0 0 83857 154 0 0 25 0 1 0 365251087 97898496 21667 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23901 21667 603 41 0 23860 0
vsize: 95604
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 47988 0 0 0 84856 155 0 0 25 0 1 0 365251087 99209216 22003 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24221 22003 603 41 0 24180 0
vsize: 96884
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 48279 0 0 0 85855 156 0 0 25 0 1 0 365251087 100392960 22294 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24510 22294 603 41 0 24469 0
vsize: 98040
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 48444 0 0 0 86855 157 0 0 25 0 1 0 365251087 101052416 22459 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24671 22459 603 41 0 24630 0
vsize: 98684
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 48694 0 0 0 87854 158 0 0 25 0 1 0 365251087 102100992 22709 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24927 22709 603 41 0 24886 0
vsize: 99708
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 49076 0 0 0 88853 159 0 0 25 0 1 0 365251087 103677952 23091 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25312 23091 603 41 0 25271 0
vsize: 101248
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 49334 0 0 0 89852 160 0 0 25 0 1 0 365251087 104738816 23349 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25571 23349 603 41 0 25530 0
vsize: 102284
[startup+910.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 49459 0 0 0 90852 160 0 0 25 0 1 0 365251087 105267200 23474 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25700 23474 603 41 0 25659 0
vsize: 102800
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 49592 0 0 0 91852 161 0 0 25 0 1 0 365251087 105803776 23607 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25831 23607 603 41 0 25790 0
vsize: 103324
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 49744 0 0 0 92852 161 0 0 25 0 1 0 365251087 106475520 23759 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25995 23759 603 41 0 25954 0
vsize: 103980
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 49884 0 0 0 93851 162 0 0 25 0 1 0 365251087 107008000 23899 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26125 23899 603 41 0 26084 0
vsize: 104500
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 49991 0 0 0 94851 162 0 0 25 0 1 0 365251087 107401216 24006 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26221 24006 603 41 0 26180 0
vsize: 104884
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50102 0 0 0 95851 162 0 0 25 0 1 0 365251087 107933696 24117 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26351 24117 603 41 0 26310 0
vsize: 105404
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50224 0 0 0 96851 162 0 0 25 0 1 0 365251087 108462080 24239 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26480 24239 603 41 0 26439 0
vsize: 105920
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50342 0 0 0 97851 163 0 0 25 0 1 0 365251087 108859392 24357 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26577 24357 603 41 0 26536 0
vsize: 106308
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50465 0 0 0 98851 163 0 0 25 0 1 0 365251087 109391872 24480 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26707 24480 603 41 0 26666 0
vsize: 106828
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50589 0 0 0 99851 163 0 0 25 0 1 0 365251087 109920256 24604 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26836 24604 603 41 0 26795 0
vsize: 107344
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50768 0 0 0 100851 164 0 0 25 0 1 0 365251087 110575616 24783 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26996 24783 603 41 0 26955 0
vsize: 107984
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50860 0 0 0 101851 164 0 0 25 0 1 0 365251087 110972928 24875 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27093 24875 603 41 0 27052 0
vsize: 108372
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 50960 0 0 0 102851 164 0 0 25 0 1 0 365251087 111386624 24975 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27194 24975 603 41 0 27153 0
vsize: 108776
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 51077 0 0 0 103851 164 0 0 25 0 1 0 365251087 111910912 25092 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27322 25092 603 41 0 27281 0
vsize: 109288
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 51189 0 0 0 104850 165 0 0 25 0 1 0 365251087 112308224 25204 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27419 25204 603 41 0 27378 0
vsize: 109676
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 51303 0 0 0 105850 165 0 0 25 0 1 0 365251087 112840704 25318 4294967295 134512640 134672761 3221224576 3221223760 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27549 25318 603 41 0 27508 0
vsize: 110196
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 51433 0 0 0 106850 165 0 0 25 0 1 0 365251087 113360896 25448 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27676 25448 603 41 0 27635 0
vsize: 110704
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 51604 0 0 0 107850 166 0 0 25 0 1 0 365251087 114008064 25619 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27834 25619 603 41 0 27793 0
vsize: 111336
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 51746 0 0 0 108849 166 0 0 25 0 1 0 365251087 114663424 25761 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27994 25761 603 41 0 27953 0
vsize: 111976
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 51899 0 0 0 109849 167 0 0 25 0 1 0 365251087 115200000 25914 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28125 25914 603 41 0 28084 0
vsize: 112500
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18802
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 52042 0 0 0 110848 168 0 0 25 0 1 0 365251087 115859456 26057 4294967295 134512640 134672761 3221224576 3221223760 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28286 26057 603 41 0 28245 0
vsize: 113144
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 52211 0 0 0 111848 168 0 0 25 0 1 0 365251087 116518912 26226 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28447 26226 603 41 0 28406 0
vsize: 113788
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 52390 0 0 0 112847 169 0 0 25 0 1 0 365251087 117178368 26405 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28608 26405 603 41 0 28567 0
vsize: 114432
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 52576 0 0 0 113847 169 0 0 25 0 1 0 365251087 117964800 26591 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28800 26591 603 41 0 28759 0
vsize: 115200
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 52709 0 0 0 114847 170 0 0 25 0 1 0 365251087 118484992 26724 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28927 26724 603 41 0 28886 0
vsize: 115708
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 52876 0 0 0 115847 170 0 0 25 0 1 0 365251087 119287808 26891 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29123 26891 603 41 0 29082 0
vsize: 116492
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 53047 0 0 0 116846 171 0 0 25 0 1 0 365251087 119947264 27062 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29284 27062 603 41 0 29243 0
vsize: 117136
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 53199 0 0 0 117846 171 0 0 25 0 1 0 365251087 120483840 27214 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29415 27214 603 41 0 29374 0
vsize: 117660
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 53375 0 0 0 118846 171 0 0 25 0 1 0 365251087 121282560 27390 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29610 27390 603 41 0 29569 0
vsize: 118440
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18804
Raw data (stat): 18796 (minisat+) R 18795 12452 12451 0 -1 0 53551 0 0 0 119846 172 0 0 25 0 1 0 365251087 121950208 27566 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29773 27566 603 41 0 29732 0
vsize: 119092
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 18804
Raw data (stat): 18796 (minisat+) Z 18795 12452 12451 0 -1 12 53552 0 0 0 119846 177 0 0 25 0 1 0 365251087 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.24
CPU user time (s): 1198.46
CPU system time (s): 1.77973
CPU usage (%): 100.014
Max. virtual memory (Kb): 119092
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####