PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	10386fd19d9976c249ce2be861b38a70
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63488
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.12
Number of variables	230
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 21843

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-22 01:18:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12648 boxname=wulflinc20 idbench=973 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10386fd19d9976c249ce2be861b38a70  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 12648
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        529156 kB
Buffers:         30156 kB
Cached:         452468 kB
SwapCached:        516 kB
Active:         171288 kB
Inactive:       313336 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        528904 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15280 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:38:11 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 12648 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> BDD-cost:23440
c ---[   8]---> BDD-cost:28410
c ---[   6]---> BDD-cost:25975
c ---[   4]---> BDD-cost:24801
c ---[   2]---> BDD-cost:25034
c ---[   0]---> BDD-cost:24120
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  436767  1274769 |  145589       0        0     nan |  0.000 % |
c |       101 |  436767  1274769 |  160147     101     7599    75.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 6404096[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       101 |  441175  1285058 |  147058     101     7599    75.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5898240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       102 |  441198  1285135 |  147066     102     7622    74.7 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5855232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       125 |  441212  1285169 |  147070     125     9078    72.6 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5680128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       139 |  441234  1285220 |  147078     139     9626    69.3 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5663744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       186 |  441243  1285242 |  147081     186    11744    63.1 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5647360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       268 |  441251  1285261 |  147083     268    15602    58.2 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5596160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       307 |  441266  1285297 |  147088     307    17285    56.3 |  0.040 % |
c ==============================================================================
c [1mFound solution: 5487616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       382 |  441275  1285321 |  147091     382    20883    54.7 |  0.040 % |
c |       482 |  441275  1285321 |  161800     482    24693    51.2 |  0.044 % |
c |       632 |  441275  1285321 |  177980     632    30326    48.0 |  0.044 % |
c ==============================================================================
c [1mFound solution: 5464064[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       730 |  441287  1285350 |  147095     730    35225    48.3 |  0.044 % |
c |       830 |  441287  1285350 |  161804     830    39533    47.6 |  0.045 % |
c ==============================================================================
c [1mFound solution: 5440512[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       904 |  441297  1285373 |  147099     904    43500    48.1 |  0.045 % |
c ==============================================================================
c [1mFound solution: 5271552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       978 |  441308  1285399 |  147102     978    46652    47.7 |  0.045 % |
c |      1078 |  441308  1285399 |  161812    1078    50655    47.0 |  0.046 % |
c |      1229 |  441308  1285399 |  177993    1229    57259    46.6 |  0.046 % |
c |      1457 |  441308  1285399 |  195792    1457    68298    46.9 |  0.046 % |
c |      1796 |  441308  1285399 |  215372    1796    83053    46.2 |  0.046 % |
c |      2303 |  441308  1285399 |  236909    2303   106417    46.2 |  0.046 % |
c ==============================================================================
c [1mFound solution: 5121024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2367 |  441325  1285442 |  147108    2367   109675    46.3 |  0.046 % |
c |      2468 |  441325  1285442 |  161818    2468   113846    46.1 |  0.047 % |
c ==============================================================================
c [1mFound solution: 5060608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2522 |  441335  1285468 |  147111    2522   116155    46.1 |  0.047 % |
c |      2623 |  441335  1285468 |  161822    2623   119822    45.7 |  0.048 % |
c |      2776 |  441335  1285468 |  178004    2776   131258    47.3 |  0.048 % |
c ==============================================================================
c [1mFound solution: 5022720[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2826 |  441345  1285492 |  147115    2826   133538    47.3 |  0.048 % |
c |      2926 |  441345  1285492 |  161826    2926   137038    46.8 |  0.048 % |
c ==============================================================================
c [1mFound solution: 4892672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2993 |  441361  1285530 |  147120    2993   140517    46.9 |  0.048 % |
c |      3093 |  441361  1285530 |  161832    3093   144868    46.8 |  0.049 % |
c |      3243 |  441361  1285530 |  178015    3243   151155    46.6 |  0.049 % |
c |      3468 |  441361  1285530 |  195816    3468   162183    46.8 |  0.049 % |
c |      3805 |  441361  1285530 |  215398    3805   177916    46.8 |  0.049 % |
c |      4313 |  441361  1285530 |  236938    4313   203493    47.2 |  0.049 % |
c |      5073 |  441361  1285530 |  260632    5073   238215    47.0 |  0.049 % |
c |      6212 |  441361  1285530 |  286695    6212   290626    46.8 |  0.049 % |
c |      7925 |  441361  1285530 |  315364    7925   373140    47.1 |  0.049 % |
c |     10487 |  441361  1285530 |  346901   10487   502342    47.9 |  0.049 % |
c ==============================================================================
c [1mFound solution: 3130368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11357 |  441373  1285563 |  147124   11357   548645    48.3 |  0.049 % |
c ==============================================================================
c [1mFound solution: 3030016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11368 |  441383  1285588 |  147127   11368   548955    48.3 |  0.049 % |
c |     11468 |  441383  1285588 |  161839   11468   553078    48.2 |  0.050 % |
c ==============================================================================
c [1mFound solution: 2987008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11526 |  441396  1285620 |  147132   11526   555621    48.2 |  0.050 % |
c |     11627 |  441396  1285620 |  161845   11627   559847    48.2 |  0.051 % |
c ==============================================================================
c [1mFound solution: 2855936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11752 |  441403  1285637 |  147134   11752   565521    48.1 |  0.051 % |
c |     11855 |  441403  1285637 |  161847   11855   569209    48.0 |  0.052 % |
c |     12005 |  441403  1285637 |  178032   12005   578630    48.2 |  0.052 % |
c |     12230 |  441403  1285637 |  195835   12230   588352    48.1 |  0.052 % |
c ==============================================================================
c [1mFound solution: 2851840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12386 |  441412  1285660 |  147137   12386   595871    48.1 |  0.052 % |
c ==============================================================================
c [1mFound solution: 2816000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12476 |  441422  1285685 |  147140   12476   599897    48.1 |  0.052 % |
c |     12576 |  441415  1285670 |  161854   12571   604076    48.1 |  0.054 % |
c ==============================================================================
c [1mFound solution: 2775040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12595 |  441424  1285691 |  147141   12590   604749    48.0 |  0.054 % |
c |     12695 |  441424  1285691 |  161855   12690   608940    48.0 |  0.055 % |
c |     12846 |  441424  1285691 |  178040   12841   616100    48.0 |  0.055 % |
c ==============================================================================
c [1mFound solution: 2662400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12972 |  441436  1285719 |  147145   12967   622239    48.0 |  0.055 % |
c |     13072 |  441436  1285719 |  161859   13067   626166    47.9 |  0.056 % |
c |     13222 |  441436  1285719 |  178045   13217   633053    47.9 |  0.056 % |
c |     13448 |  441436  1285719 |  195849   13443   643739    47.9 |  0.056 % |
c |     13785 |  441436  1285719 |  215434   13780   659014    47.8 |  0.056 % |
c |     14291 |  441436  1285719 |  236978   14286   680978    47.7 |  0.056 % |
c |     15050 |  441436  1285719 |  260676   15045   715068    47.5 |  0.056 % |
c ==============================================================================
c [1mFound solution: 2650112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15554 |  441445  1285739 |  147148   15549   738967    47.5 |  0.056 % |
c |     15654 |  441440  1285729 |  161862   15644   742466    47.5 |  0.057 % |
c |     15805 |  441440  1285729 |  178049   15795   748653    47.4 |  0.057 % |
c |     16031 |  441440  1285729 |  195853   16021   759741    47.4 |  0.057 % |
c |     16369 |  441440  1285729 |  215439   16359   777405    47.5 |  0.057 % |
c ==============================================================================
c [1mFound solution: 2510848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16562 |  441452  1285758 |  147150   16552   785530    47.5 |  0.057 % |
c ==============================================================================
c [1mFound solution: 2456576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16639 |  441463  1285784 |  147154   16629   788726    47.4 |  0.057 % |
c |     16739 |  441463  1285784 |  161869   16729   792734    47.4 |  0.059 % |
c |     16889 |  441463  1285784 |  178056   16879   799286    47.4 |  0.059 % |
c |     17114 |  441463  1285784 |  195861   17104   809644    47.3 |  0.059 % |
c |     17451 |  441463  1285784 |  215448   17441   825471    47.3 |  0.059 % |
c |     17957 |  441463  1285784 |  236992   17947   850339    47.4 |  0.059 % |
c ==============================================================================
c [1mFound solution: 2454528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18184 |  441474  1285811 |  147158   18174   861848    47.4 |  0.059 % |
c ==============================================================================
c [1mFound solution: 2437120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18214 |  441486  1285839 |  147162   18204   863992    47.5 |  0.059 % |
c |     18315 |  441486  1285839 |  161878   18305   867683    47.4 |  0.060 % |
c ==============================================================================
c [1mFound solution: 2432000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18354 |  441499  1285869 |  147166   18344   869636    47.4 |  0.060 % |
c |     18455 |  441499  1285869 |  161882   18445   873073    47.3 |  0.061 % |
c |     18607 |  441499  1285869 |  178070   18597   884539    47.6 |  0.061 % |
c |     18832 |  441499  1285869 |  195877   18822   898770    47.8 |  0.061 % |
c ==============================================================================
c [1mFound solution: 2405376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18988 |  441511  1285897 |  147170   18978   904556    47.7 |  0.061 % |
c ==============================================================================
c [1mFound solution: 2371584[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19036 |  441519  1285915 |  147173   19026   906591    47.7 |  0.061 % |
c |     19136 |  441519  1285915 |  161890   19126   910640    47.6 |  0.062 % |
c |     19286 |  441519  1285915 |  178079   19276   917023    47.6 |  0.062 % |
c |     19511 |  441519  1285915 |  195887   19501   926601    47.5 |  0.062 % |
c ==============================================================================
c [1mFound solution: 2337792[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19570 |  441525  1285930 |  147175   19560   929041    47.5 |  0.062 % |
c ==============================================================================
c [1mFound solution: 2190336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19602 |  441534  1285950 |  147178   19592   930390    47.5 |  0.062 % |
c |     19704 |  441534  1285950 |  161895   19694   934818    47.5 |  0.063 % |
c |     19857 |  441534  1285950 |  178085   19847   941270    47.4 |  0.063 % |
c |     20085 |  441516  1285910 |  195893   20046   949831    47.4 |  0.067 % |
c ==============================================================================
c [1mFound solution: 2168832[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20272 |  441526  1285932 |  147175   20233   956629    47.3 |  0.067 % |
c |     20374 |  441526  1285932 |  161892   20335   960960    47.3 |  0.067 % |
c ==============================================================================
c [1mFound solution: 2154496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20514 |  441534  1285950 |  147178   20475   967662    47.3 |  0.067 % |
c |     20614 |  441534  1285950 |  161895   20575   972104    47.2 |  0.068 % |
c |     20769 |  441534  1285950 |  178085   20730   978293    47.2 |  0.068 % |
c ==============================================================================
c [1mFound solution: 2117632[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20947 |  441540  1285963 |  147180   20908   986503    47.2 |  0.068 % |
c |     21047 |  441540  1285963 |  161898   21008   990370    47.1 |  0.069 % |
c |     21197 |  441540  1285963 |  178087   21158   997355    47.1 |  0.069 % |
c |     21422 |  441540  1285963 |  195896   21383  1007184    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 2114560[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21696 |  441549  1285983 |  147183   21657  1019168    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 1947648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21730 |  441557  1286002 |  147185   21691  1020931    47.1 |  0.069 % |
c ==============================================================================
c [1mFound solution: 1937408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21744 |  441566  1286025 |  147188   21705  1021695    47.1 |  0.069 % |
c |     21844 |  441566  1286025 |  161906   21805  1026027    47.1 |  0.070 % |
c ==============================================================================
c [1mFound solution: 1893376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21949 |  441574  1286045 |  147191   21910  1029023    47.0 |  0.070 % |
c |     22049 |  441574  1286045 |  161910   22010  1033110    46.9 |  0.071 % |
c |     22199 |  441574  1286045 |  178101   22160  1038508    46.9 |  0.071 % |
c ==============================================================================
c [1mFound solution: 1881088[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22225 |  441578  1286055 |  147192   22186  1039839    46.9 |  0.071 % |
c ==============================================================================
c [1mFound solution: 1748992[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22319 |  441590  1286083 |  147196   22280  1043648    46.8 |  0.071 % |
c |     22419 |  441590  1286083 |  161915   22380  1047923    46.8 |  0.072 % |
c ==============================================================================
c [1mFound solution: 1742848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22427 |  441602  1286111 |  147200   22388  1048258    46.8 |  0.072 % |
c ==============================================================================
c [1mFound solution: 1703936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22453 |  441605  1286118 |  147201   22414  1049690    46.8 |  0.072 % |
c |     22555 |  441605  1286118 |  161921   22516  1054292    46.8 |  0.074 % |
c |     22705 |  441605  1286118 |  178113   22666  1061590    46.8 |  0.074 % |
c |     22931 |  441605  1286118 |  195924   22892  1071090    46.8 |  0.074 % |
c |     23268 |  441605  1286118 |  215516   23229  1088121    46.8 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1601536[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23453 |  441608  1286125 |  147202   23414  1096341    46.8 |  0.074 % |
c |     23555 |  441608  1286125 |  161922   23516  1098789    46.7 |  0.074 % |
c |     23705 |  441608  1286125 |  178114   23666  1105702    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1558528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23717 |  441615  1286145 |  147205   23678  1106109    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1415168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23734 |  441623  1286164 |  147207   23695  1106742    46.7 |  0.074 % |
c ==============================================================================
c [1mFound solution: 1394688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23797 |  441634  1286190 |  147211   23758  1109356    46.7 |  0.074 % |
c |     23897 |  441627  1286175 |  161932   23853  1112691    46.6 |  0.078 % |
c |     24047 |  441627  1286175 |  178125   24003  1119318    46.6 |  0.078 % |
c |     24272 |  441627  1286175 |  195937   24228  1131072    46.7 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1338368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24446 |  441634  1286191 |  147211   24402  1138915    46.7 |  0.078 % |
c |     24547 |  441634  1286191 |  161932   24503  1145546    46.8 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1326080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24682 |  441641  1286207 |  147213   24638  1150434    46.7 |  0.078 % |
c ==============================================================================
c [1mFound solution: 1316864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24715 |  441649  1286225 |  147216   24671  1151706    46.7 |  0.078 % |
c |     24815 |  441649  1286225 |  161937   24771  1155628    46.7 |  0.080 % |
c ==============================================================================
c [1mFound solution: 1281024[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24842 |  441658  1286247 |  147219   24798  1156594    46.6 |  0.080 % |
c ==============================================================================
c [1mFound solution: 1177600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24907 |  441665  1286263 |  147221   24863  1159311    46.6 |  0.080 % |
c |     25008 |  441665  1286263 |  161943   24964  1164044    46.6 |  0.081 % |
c |     25158 |  441665  1286263 |  178137   25114  1172031    46.7 |  0.081 % |
c |     25384 |  441665  1286263 |  195951   25340  1181976    46.6 |  0.081 % |
c ==============================================================================
c [1mFound solution: 1070080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25476 |  441676  1286287 |  147225   25432  1185106    46.6 |  0.081 % |
c ==============================================================================
c [1mFound solution: 1029120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25551 |  441653  1286224 |  147217   24181  1129685    46.7 |  0.081 % |
c |     25651 |  441632  1286176 |  161938   22327  1030708    46.2 |  0.094 % |
c ==============================================================================
c [1mFound solution: 959488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25753 |  441638  1286191 |  147212   22429  1033691    46.1 |  0.094 % |
c ==============================================================================
c [1mFound solution: 914432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25851 |  441645  1286209 |  147215   22527  1037806    46.1 |  0.094 % |
c |     25951 |  441645  1286209 |  161936   22627  1041265    46.0 |  0.095 % |
c |     26102 |  441645  1286209 |  178130   22778  1047328    46.0 |  0.095 % |
c ==============================================================================
c [1mFound solution: 880640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26239 |  441654  1286230 |  147218   22915  1053422    46.0 |  0.095 % |
c |     26339 |  441573  1286043 |  161939   20824   956529    45.9 |  0.113 % |
#### 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.95 1.00 0.99 2/54 16900
Raw data (stat): 16900 (runsolver) R 16899 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549699228 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 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+10 s]
Raw data (loadavg): 0.95 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14443 0 0 0 962 34 0 0 25 0 1 0 549699228 66211840 13356 4294967295 134512640 134672761 3221224528 3221223652 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16165 13356 603 41 0 16124 0
vsize: 64660
[startup+20.0007 s]
Raw data (loadavg): 0.96 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14520 0 0 0 1962 34 0 0 25 0 1 0 549699228 66768896 13433 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16301 13433 603 41 0 16260 0
vsize: 65204
[startup+30.0035 s]
Raw data (loadavg): 0.97 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14520 0 0 0 2962 34 0 0 25 0 1 0 549699228 66768896 13433 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16301 13433 603 41 0 16260 0
vsize: 65204
[startup+40.0031 s]
Raw data (loadavg): 0.97 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14530 0 0 0 3961 34 0 0 25 0 1 0 549699228 66768896 13443 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16301 13443 603 41 0 16260 0
vsize: 65204
[startup+50.0043 s]
Raw data (loadavg): 0.97 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14548 0 0 0 4961 34 0 0 25 0 1 0 549699228 66768896 13461 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16301 13461 603 41 0 16260 0
vsize: 65204
[startup+60.0045 s]
Raw data (loadavg): 0.98 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14567 0 0 0 5961 35 0 0 25 0 1 0 549699228 66904064 13480 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16334 13480 603 41 0 16293 0
vsize: 65336
[startup+70.0052 s]
Raw data (loadavg): 0.98 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14584 0 0 0 6961 35 0 0 25 0 1 0 549699228 66904064 13497 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16334 13497 603 41 0 16293 0
vsize: 65336
[startup+80.0062 s]
Raw data (loadavg): 0.98 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14596 0 0 0 7961 35 0 0 25 0 1 0 549699228 67039232 13509 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 13509 603 41 0 16326 0
vsize: 65468
[startup+90.0057 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14621 0 0 0 8961 35 0 0 25 0 1 0 549699228 67039232 13534 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 13534 603 41 0 16326 0
vsize: 65468
[startup+100.005 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14643 0 0 0 9961 35 0 0 25 0 1 0 549699228 67174400 13556 4294967295 134512640 134672761 3221224528 3221223860 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16400 13556 603 41 0 16359 0
vsize: 65600
[startup+110.006 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14658 0 0 0 10961 35 0 0 25 0 1 0 549699228 67309568 13571 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16433 13571 603 41 0 16392 0
vsize: 65732
[startup+120.006 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14677 0 0 0 11961 35 0 0 25 0 1 0 549699228 67309568 13590 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16433 13590 603 41 0 16392 0
vsize: 65732
[startup+130.006 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14695 0 0 0 12961 36 0 0 25 0 1 0 549699228 67444736 13608 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16466 13608 603 41 0 16425 0
vsize: 65864
[startup+140.006 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14714 0 0 0 13961 36 0 0 25 0 1 0 549699228 67444736 13627 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16466 13627 603 41 0 16425 0
vsize: 65864
[startup+150.006 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14729 0 0 0 14961 36 0 0 25 0 1 0 549699228 67579904 13642 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16499 13642 603 41 0 16458 0
vsize: 65996
[startup+160.006 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14743 0 0 0 15961 36 0 0 25 0 1 0 549699228 67579904 13656 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16499 13656 603 41 0 16458 0
vsize: 65996
[startup+170.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14757 0 0 0 16962 36 0 0 25 0 1 0 549699228 67715072 13670 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16532 13670 603 41 0 16491 0
vsize: 66128
[startup+180.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14773 0 0 0 17962 36 0 0 25 0 1 0 549699228 67715072 13686 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16532 13686 603 41 0 16491 0
vsize: 66128
[startup+190.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14787 0 0 0 18962 36 0 0 25 0 1 0 549699228 67846144 13700 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16564 13700 603 41 0 16523 0
vsize: 66256
[startup+200.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14800 0 0 0 19962 36 0 0 25 0 1 0 549699228 67846144 13713 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16564 13713 603 41 0 16523 0
vsize: 66256
[startup+210.006 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14811 0 0 0 20962 36 0 0 25 0 1 0 549699228 67846144 13724 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16564 13724 603 41 0 16523 0
vsize: 66256
[startup+220.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14828 0 0 0 21962 36 0 0 25 0 1 0 549699228 67989504 13741 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16599 13741 603 41 0 16558 0
vsize: 66396
[startup+230.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14846 0 0 0 22962 36 0 0 25 0 1 0 549699228 67989504 13759 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16599 13759 603 41 0 16558 0
vsize: 66396
[startup+240.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14863 0 0 0 23962 36 0 0 25 0 1 0 549699228 68149248 13776 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16638 13776 603 41 0 16597 0
vsize: 66552
[startup+250.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14878 0 0 0 24963 36 0 0 25 0 1 0 549699228 68149248 13791 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16638 13791 603 41 0 16597 0
vsize: 66552
[startup+260.007 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14892 0 0 0 25963 37 0 0 25 0 1 0 549699228 68149248 13805 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16638 13805 603 41 0 16597 0
vsize: 66552
[startup+270.008 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14903 0 0 0 26963 37 0 0 25 0 1 0 549699228 68280320 13816 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16670 13816 603 41 0 16629 0
vsize: 66680
[startup+280.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14919 0 0 0 27963 37 0 0 25 0 1 0 549699228 68280320 13832 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16670 13832 603 41 0 16629 0
vsize: 66680
[startup+290.008 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14933 0 0 0 28963 37 0 0 25 0 1 0 549699228 68415488 13846 4294967295 134512640 134672761 3221224528 3221223712 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16703 13846 603 41 0 16662 0
vsize: 66812
[startup+300.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14954 0 0 0 29963 37 0 0 25 0 1 0 549699228 68567040 13867 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 13867 603 41 0 16699 0
vsize: 66960
[startup+310.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14965 0 0 0 30963 37 0 0 25 0 1 0 549699228 68567040 13878 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 13878 603 41 0 16699 0
vsize: 66960
[startup+320.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14983 0 0 0 31964 37 0 0 25 0 1 0 549699228 68702208 13896 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16773 13896 603 41 0 16732 0
vsize: 67092
[startup+330.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 14997 0 0 0 32964 37 0 0 25 0 1 0 549699228 68702208 13910 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16773 13910 603 41 0 16732 0
vsize: 67092
[startup+340.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15012 0 0 0 33964 37 0 0 25 0 1 0 549699228 68702208 13925 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16773 13925 603 41 0 16732 0
vsize: 67092
[startup+350.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15026 0 0 0 34964 37 0 0 25 0 1 0 549699228 68833280 13939 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16805 13939 603 41 0 16764 0
vsize: 67220
[startup+360.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15038 0 0 0 35964 37 0 0 25 0 1 0 549699228 68833280 13951 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16805 13951 603 41 0 16764 0
vsize: 67220
[startup+370.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15054 0 0 0 36964 37 0 0 25 0 1 0 549699228 68964352 13967 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16837 13967 603 41 0 16796 0
vsize: 67348
[startup+380.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15066 0 0 0 37964 38 0 0 25 0 1 0 549699228 68964352 13979 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16837 13979 603 41 0 16796 0
vsize: 67348
[startup+390.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15077 0 0 0 38964 38 0 0 25 0 1 0 549699228 68964352 13990 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16837 13990 603 41 0 16796 0
vsize: 67348
[startup+400.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15093 0 0 0 39964 38 0 0 25 0 1 0 549699228 69095424 14006 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16869 14006 603 41 0 16828 0
vsize: 67476
[startup+410.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15116 0 0 0 40964 38 0 0 25 0 1 0 549699228 69259264 14029 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16909 14029 603 41 0 16868 0
vsize: 67636
[startup+420.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15129 0 0 0 41965 38 0 0 25 0 1 0 549699228 69259264 14042 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16909 14042 603 41 0 16868 0
vsize: 67636
[startup+430.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15148 0 0 0 42965 38 0 0 25 0 1 0 549699228 69259264 14061 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16909 14061 603 41 0 16868 0
vsize: 67636
[startup+440.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15160 0 0 0 43964 38 0 0 25 0 1 0 549699228 69390336 14073 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16941 14073 603 41 0 16900 0
vsize: 67764
[startup+450.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15169 0 0 0 44964 38 0 0 25 0 1 0 549699228 69390336 14082 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16941 14082 603 41 0 16900 0
vsize: 67764
[startup+460.008 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15181 0 0 0 45964 38 0 0 25 0 1 0 549699228 69521408 14094 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16973 14094 603 41 0 16932 0
vsize: 67892
[startup+470.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15203 0 0 0 46964 38 0 0 25 0 1 0 549699228 69521408 14116 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16973 14116 603 41 0 16932 0
vsize: 67892
[startup+480.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15216 0 0 0 47964 38 0 0 25 0 1 0 549699228 69652480 14129 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 14129 603 41 0 16964 0
vsize: 68020
[startup+490.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15221 0 0 0 48964 38 0 0 25 0 1 0 549699228 69652480 14134 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 14134 603 41 0 16964 0
vsize: 68020
[startup+500.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15231 0 0 0 49965 38 0 0 25 0 1 0 549699228 69652480 14144 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 14144 603 41 0 16964 0
vsize: 68020
[startup+510.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15241 0 0 0 50964 39 0 0 25 0 1 0 549699228 69779456 14154 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17036 14154 603 41 0 16995 0
vsize: 68144
[startup+520.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15256 0 0 0 51965 39 0 0 25 0 1 0 549699228 69779456 14169 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17036 14169 603 41 0 16995 0
vsize: 68144
[startup+530.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15266 0 0 0 52964 39 0 0 25 0 1 0 549699228 69779456 14179 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17036 14179 603 41 0 16995 0
vsize: 68144
[startup+540.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15275 0 0 0 53964 39 0 0 25 0 1 0 549699228 69906432 14188 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17067 14188 603 41 0 17026 0
vsize: 68268
[startup+550.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15286 0 0 0 54965 39 0 0 25 0 1 0 549699228 69906432 14199 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17067 14199 603 41 0 17026 0
vsize: 68268
[startup+560.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15297 0 0 0 55965 39 0 0 25 0 1 0 549699228 69906432 14210 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17067 14210 603 41 0 17026 0
vsize: 68268
[startup+570.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15309 0 0 0 56965 39 0 0 25 0 1 0 549699228 70037504 14222 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17099 14222 603 41 0 17058 0
vsize: 68396
[startup+580.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15320 0 0 0 57965 39 0 0 25 0 1 0 549699228 70037504 14233 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17099 14233 603 41 0 17058 0
vsize: 68396
[startup+590.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15334 0 0 0 58965 39 0 0 25 0 1 0 549699228 70189056 14247 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17136 14247 603 41 0 17095 0
vsize: 68544
[startup+600.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15343 0 0 0 59965 39 0 0 25 0 1 0 549699228 70189056 14256 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17136 14256 603 41 0 17095 0
vsize: 68544
[startup+610.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15353 0 0 0 60965 39 0 0 25 0 1 0 549699228 70189056 14266 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17136 14266 603 41 0 17095 0
vsize: 68544
[startup+620.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15367 0 0 0 61966 40 0 0 25 0 1 0 549699228 70320128 14280 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17168 14280 603 41 0 17127 0
vsize: 68672
[startup+630.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15382 0 0 0 62966 40 0 0 25 0 1 0 549699228 70320128 14295 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17168 14295 603 41 0 17127 0
vsize: 68672
[startup+640.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15397 0 0 0 63966 40 0 0 25 0 1 0 549699228 70459392 14310 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17202 14310 603 41 0 17161 0
vsize: 68808
[startup+650.009 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15410 0 0 0 64966 40 0 0 25 0 1 0 549699228 70459392 14323 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17202 14323 603 41 0 17161 0
vsize: 68808
[startup+660.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15422 0 0 0 65966 40 0 0 25 0 1 0 549699228 70459392 14335 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17202 14335 603 41 0 17161 0
vsize: 68808
[startup+670.011 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15434 0 0 0 66966 40 0 0 25 0 1 0 549699228 70590464 14347 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17234 14347 603 41 0 17193 0
vsize: 68936
[startup+680.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15453 0 0 0 67966 40 0 0 25 0 1 0 549699228 70746112 14366 4294967295 134512640 134672761 3221224528 3221223864 134561962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14366 603 41 0 17231 0
vsize: 69088
[startup+690.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15454 0 0 0 68966 40 0 0 25 0 1 0 549699228 70746112 14367 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14367 603 41 0 17231 0
vsize: 69088
[startup+700.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15463 0 0 0 69966 40 0 0 25 0 1 0 549699228 70746112 14376 4294967295 134512640 134672761 3221224528 3221223696 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14376 603 41 0 17231 0
vsize: 69088
[startup+710.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15473 0 0 0 70966 40 0 0 25 0 1 0 549699228 70746112 14386 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14386 603 41 0 17231 0
vsize: 69088
[startup+720.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15482 0 0 0 71967 40 0 0 25 0 1 0 549699228 70746112 14395 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 14395 603 41 0 17231 0
vsize: 69088
[startup+730.011 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15495 0 0 0 72967 41 0 0 25 0 1 0 549699228 70868992 14408 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 14408 603 41 0 17261 0
vsize: 69208
[startup+740.011 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15504 0 0 0 73967 41 0 0 25 0 1 0 549699228 70868992 14417 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 14417 603 41 0 17261 0
vsize: 69208
[startup+750.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15516 0 0 0 74967 41 0 0 25 0 1 0 549699228 70868992 14429 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17302 14429 603 41 0 17261 0
vsize: 69208
[startup+760.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15530 0 0 0 75967 41 0 0 25 0 1 0 549699228 71000064 14443 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17334 14443 603 41 0 17293 0
vsize: 69336
[startup+770.011 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15542 0 0 0 76967 41 0 0 25 0 1 0 549699228 71000064 14455 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17334 14455 603 41 0 17293 0
vsize: 69336
[startup+780.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15556 0 0 0 77967 41 0 0 25 0 1 0 549699228 71155712 14469 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17372 14469 603 41 0 17331 0
vsize: 69488
[startup+790.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15573 0 0 0 78967 41 0 0 25 0 1 0 549699228 71155712 14486 4294967295 134512640 134672761 3221224528 3221223696 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17372 14486 603 41 0 17331 0
vsize: 69488
[startup+800.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15587 0 0 0 79967 41 0 0 25 0 1 0 549699228 71278592 14500 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17402 14500 603 41 0 17361 0
vsize: 69608
[startup+810.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15595 0 0 0 80967 41 0 0 25 0 1 0 549699228 71278592 14508 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17402 14508 603 41 0 17361 0
vsize: 69608
[startup+820.013 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15610 0 0 0 81967 41 0 0 25 0 1 0 549699228 71278592 14523 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17402 14523 603 41 0 17361 0
vsize: 69608
[startup+830.014 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15620 0 0 0 82968 42 0 0 25 0 1 0 549699228 71409664 14533 4294967295 134512640 134672761 3221224528 3221223728 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17434 14533 603 41 0 17393 0
vsize: 69736
[startup+840.013 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15627 0 0 0 83968 42 0 0 25 0 1 0 549699228 71409664 14540 4294967295 134512640 134672761 3221224528 3221223676 1074732966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17434 14540 603 41 0 17393 0
vsize: 69736
[startup+850.013 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15647 0 0 0 84968 42 0 0 25 0 1 0 549699228 71557120 14560 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17470 14560 603 41 0 17429 0
vsize: 69880
[startup+860.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15654 0 0 0 85968 42 0 0 25 0 1 0 549699228 71557120 14567 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17470 14567 603 41 0 17429 0
vsize: 69880
[startup+870.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15666 0 0 0 86968 42 0 0 25 0 1 0 549699228 71557120 14579 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17470 14579 603 41 0 17429 0
vsize: 69880
[startup+880.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15683 0 0 0 87968 42 0 0 25 0 1 0 549699228 71671808 14596 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17498 14596 603 41 0 17457 0
vsize: 69992
[startup+890.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15700 0 0 0 88968 42 0 0 25 0 1 0 549699228 71823360 14613 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14613 603 41 0 17494 0
vsize: 70140
[startup+900.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15706 0 0 0 89968 42 0 0 25 0 1 0 549699228 71823360 14619 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14619 603 41 0 17494 0
vsize: 70140
[startup+910.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15713 0 0 0 90968 42 0 0 25 0 1 0 549699228 71823360 14626 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14626 603 41 0 17494 0
vsize: 70140
[startup+920.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15724 0 0 0 91968 42 0 0 25 0 1 0 549699228 71823360 14637 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17535 14637 603 41 0 17494 0
vsize: 70140
[startup+930.011 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15737 0 0 0 92968 42 0 0 25 0 1 0 549699228 71946240 14650 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17565 14650 603 41 0 17524 0
vsize: 70260
[startup+940.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15747 0 0 0 93969 42 0 0 25 0 1 0 549699228 71946240 14660 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17565 14660 603 41 0 17524 0
vsize: 70260
[startup+950.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15756 0 0 0 94969 43 0 0 25 0 1 0 549699228 71946240 14669 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17565 14669 603 41 0 17524 0
vsize: 70260
[startup+960.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15764 0 0 0 95969 43 0 0 25 0 1 0 549699228 72077312 14677 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17597 14677 603 41 0 17556 0
vsize: 70388
[startup+970.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15775 0 0 0 96969 43 0 0 25 0 1 0 549699228 72077312 14688 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17597 14688 603 41 0 17556 0
vsize: 70388
[startup+980.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15785 0 0 0 97969 43 0 0 25 0 1 0 549699228 72077312 14698 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17597 14698 603 41 0 17556 0
vsize: 70388
[startup+990.012 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15801 0 0 0 98969 43 0 0 25 0 1 0 549699228 72208384 14714 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14714 603 41 0 17588 0
vsize: 70516
[startup+1000.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15811 0 0 0 99969 43 0 0 25 0 1 0 549699228 72208384 14724 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14724 603 41 0 17588 0
vsize: 70516
[startup+1010.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15820 0 0 0 100969 43 0 0 25 0 1 0 549699228 72208384 14733 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17629 14733 603 41 0 17588 0
vsize: 70516
[startup+1020.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15832 0 0 0 101969 43 0 0 25 0 1 0 549699228 72368128 14745 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14745 603 41 0 17627 0
vsize: 70672
[startup+1030.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15841 0 0 0 102969 43 0 0 25 0 1 0 549699228 72368128 14754 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14754 603 41 0 17627 0
vsize: 70672
[startup+1040.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15854 0 0 0 103969 43 0 0 25 0 1 0 549699228 72368128 14767 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14767 603 41 0 17627 0
vsize: 70672
[startup+1050.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15859 0 0 0 104970 43 0 0 25 0 1 0 549699228 72368128 14772 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17668 14772 603 41 0 17627 0
vsize: 70672
[startup+1060.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15868 0 0 0 105970 43 0 0 25 0 1 0 549699228 72491008 14781 4294967295 134512640 134672761 3221224528 3221223696 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 14781 603 41 0 17657 0
vsize: 70792
[startup+1070.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15875 0 0 0 106970 43 0 0 25 0 1 0 549699228 72491008 14788 4294967295 134512640 134672761 3221224528 3221223696 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 14788 603 41 0 17657 0
vsize: 70792
[startup+1080.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15887 0 0 0 107970 43 0 0 25 0 1 0 549699228 72491008 14800 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 14800 603 41 0 17657 0
vsize: 70792
[startup+1090.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15896 0 0 0 108970 44 0 0 25 0 1 0 549699228 72491008 14809 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17698 14809 603 41 0 17657 0
vsize: 70792
[startup+1100.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15907 0 0 0 109970 44 0 0 25 0 1 0 549699228 72626176 14820 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14820 603 41 0 17690 0
vsize: 70924
[startup+1110.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15914 0 0 0 110970 44 0 0 25 0 1 0 549699228 72626176 14827 4294967295 134512640 134672761 3221224528 3221223664 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14827 603 41 0 17690 0
vsize: 70924
[startup+1120.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15918 0 0 0 111970 44 0 0 25 0 1 0 549699228 72626176 14831 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14831 603 41 0 17690 0
vsize: 70924
[startup+1130.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15929 0 0 0 112971 44 0 0 25 0 1 0 549699228 72626176 14842 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 14842 603 41 0 17690 0
vsize: 70924
[startup+1140.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15936 0 0 0 113971 44 0 0 25 0 1 0 549699228 72757248 14849 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14849 603 41 0 17722 0
vsize: 71052
[startup+1150.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15948 0 0 0 114971 44 0 0 25 0 1 0 549699228 72757248 14861 4294967295 134512640 134672761 3221224528 3221223696 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14861 603 41 0 17722 0
vsize: 71052
[startup+1160.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15948 0 0 0 115971 44 0 0 25 0 1 0 549699228 72757248 14861 4294967295 134512640 134672761 3221224528 3221223652 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14861 603 41 0 17722 0
vsize: 71052
[startup+1170.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15948 0 0 0 116971 44 0 0 25 0 1 0 549699228 72757248 14861 4294967295 134512640 134672761 3221224528 3221223676 1074732978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14861 603 41 0 17722 0
vsize: 71052
[startup+1180.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15948 0 0 0 117971 44 0 0 25 0 1 0 549699228 72757248 14861 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14861 603 41 0 17722 0
vsize: 71052
[startup+1190.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15948 0 0 0 118971 44 0 0 25 0 1 0 549699228 72757248 14861 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14861 603 41 0 17722 0
vsize: 71052
[startup+1200.01 s]
Raw data (loadavg): 0.99 1.00 0.99 2/54 16900
Raw data (stat): 16900 (minisat+) R 16899 27565 27564 0 -1 0 15950 0 0 0 119971 44 0 0 25 0 1 0 549699228 72757248 14863 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17763 14863 603 41 0 17722 0
vsize: 71052
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.99 1/54 16900
Raw data (stat): 16900 (minisat+) Z 16899 27565 27564 0 -1 12 15953 0 0 0 119972 47 0 0 25 0 1 0 549699228 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.05
CPU time (s): 1200.2
CPU user time (s): 1199.72
CPU system time (s): 0.475927
CPU usage (%): 100.013
Max. virtual memory (Kb): 71052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####