PB'05 competition: run trace

Some explanations

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        827884 kB
Buffers:         34684 kB
Cached:         137496 kB
SwapCached:       2376 kB
Active:          57832 kB
Inactive:       119684 kB
HighTotal:      131008 kB
HighFree:          728 kB
LowTotal:       903652 kB
LowFree:        827156 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23680 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:30:32 (client local time) WITH STATUS 10 IN 1210.02 SECONDS
stats: 3916 7 1210.02 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5557 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    5557    18748 |    1667       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  808/808          
c |         0 |    5557    18748 |    2222       0        0     nan |  0.000 % |
c |       102 |    5557    18748 |    2445     102     7604    74.5 |  0.006 % |
c ==============================================================================
c (current CPU-time: 0.301954 s)
c ==============================================================================
c [1mFound solution: 396[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:37286     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       204 |   50814   124567 |   15244     204    15305    75.0 |  0.006 % |
c   -- subsuming                       
c   -- var.elim.:  1000/30329          
c   -- var.elim.:  2000/30329          
c   -- var.elim.:  3000/30329          
c   -- var.elim.:  4000/30329          
c   -- var.elim.:  5000/30329          
c   -- var.elim.:  6000/30329          
c   -- var.elim.:  7000/30329          
c   -- var.elim.:  8000/30329          
c   -- var.elim.:  9000/30329          
c   -- var.elim.:  10000/30329          
c   -- var.elim.:  11000/30329          
c   -- var.elim.:  12000/30329          
c   -- var.elim.:  13000/30329          
c   -- var.elim.:  14000/30329          
c   -- var.elim.:  15000/30329          
c   -- var.elim.:  16000/30329          
c   -- var.elim.:  17000/30329          
c   -- var.elim.:  18000/30329          
c   -- var.elim.:  19000/30329          
c   -- var.elim.:  20000/30329          
c   -- var.elim.:  21000/30329          
c   -- var.elim.:  22000/30329          
c   -- var.elim.:  23000/30329          
c   -- var.elim.:  24000/30329          
c   -- var.elim.:  25000/30329          
c   -- var.elim.:  26000/30329          
c   -- var.elim.:  27000/30329          
c   -- var.elim.:  28000/30329          
c   -- var.elim.:  29000/30329          
c   -- var.elim.:  30000/30329          
c   -- var.elim.:  30329/30329          
c   -- var.elim.:  1000/14931          
c   -- var.elim.:  2000/14931          
c   -- var.elim.:  3000/14931          
c   -- var.elim.:  4000/14931          
c   -- var.elim.:  5000/14931          
c   -- var.elim.:  6000/14931          
c   -- var.elim.:  7000/14931          
c   -- var.elim.:  8000/14931          
c   -- var.elim.:  9000/14931          
c   -- var.elim.:  10000/14931          
c   -- var.elim.:  11000/14931          
c   -- var.elim.:  12000/14931          
c   -- var.elim.:  13000/14931          
c   -- var.elim.:  14000/14931          
c   -- var.elim.:  14931/14931          
c   -- var.elim.:  1000/8909          
c   -- var.elim.:  2000/8909          
c   -- var.elim.:  3000/8909          
c   -- var.elim.:  4000/8909          
c   -- var.elim.:  5000/8909          
c   -- var.elim.:  6000/8909          
c   -- var.elim.:  7000/8909          
c   -- var.elim.:  8000/8909          
c   -- var.elim.:  8909/8909          
c   -- var.elim.:  1000/6428          
c   -- var.elim.:  2000/6428          
c   -- var.elim.:  3000/6428          
c   -- var.elim.:  4000/6428          
c   -- var.elim.:  5000/6428          
c   -- var.elim.:  6000/6428          
c   -- var.elim.:  6428/6428          
c   -- var.elim.:  1000/5015          
c   -- var.elim.:  2000/5015          
c   -- var.elim.:  3000/5015          
c   -- var.elim.:  4000/5015          
c   -- var.elim.:  5000/5015          
c   -- var.elim.:  5015/5015          
c   -- var.elim.:  1000/3315          
c   -- var.elim.:  2000/3315          
c   -- var.elim.:  3000/3315          
c   -- var.elim.:  3315/3315          
c   -- var.elim.:  1000/2538          
c   -- var.elim.:  2000/2538          
c   -- var.elim.:  2538/2538          
c   -- var.elim.:  1000/1545          
c   -- var.elim.:  1545/1545          
c   -- var.elim.:  291/291          
c   -- subsuming                       
c   -- var.elim.:  1000/4338          
c   -- var.elim.:  2000/4338          
c   -- var.elim.:  3000/4338          
c   -- var.elim.:  4000/4338          
c   -- var.elim.:  4338/4338          
c   -- var.elim.:  87/87          
c |       204 |   17723   104874 |      --     204       --      -- |     --   | -33082/-19666
c |       204 |   17723   104874 |    7089     204    15305    75.0 |  0.006 % |
c ==============================================================================
c (current CPU-time: 35.6576 s)
c ==============================================================================
c [1mFound solution: 383[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       220 |   50601   185354 |   15180     220    16516    75.1 |  0.006 % |
c   -- subsuming                       
c   -- var.elim.:  1000/29532          
c   -- var.elim.:  2000/29532          
c   -- var.elim.:  3000/29532          
c   -- var.elim.:  4000/29532          
c   -- var.elim.:  5000/29532          
c   -- var.elim.:  6000/29532          
c   -- var.elim.:  7000/29532          
c   -- var.elim.:  8000/29532          
c   -- var.elim.:  9000/29532          
c   -- var.elim.:  10000/29532          
c   -- var.elim.:  11000/29532          
c   -- var.elim.:  12000/29532          
c   -- var.elim.:  13000/29532          
c   -- var.elim.:  14000/29532          
c   -- var.elim.:  15000/29532          
c   -- var.elim.:  16000/29532          
c   -- var.elim.:  17000/29532          
c   -- var.elim.:  18000/29532          
c   -- var.elim.:  19000/29532          
c   -- var.elim.:  20000/29532          
c   -- var.elim.:  21000/29532          
c   -- var.elim.:  22000/29532          
c   -- var.elim.:  23000/29532          
c   -- var.elim.:  24000/29532          
c   -- var.elim.:  25000/29532          
c   -- var.elim.:  26000/29532          
c   -- var.elim.:  27000/29532          
c   -- var.elim.:  28000/29532          
c   -- var.elim.:  29000/29532          
c   -- var.elim.:  29532/29532          
c   -- var.elim.:  1000/14213          
c   -- var.elim.:  2000/14213          
c   -- var.elim.:  3000/14213          
c   -- var.elim.:  4000/14213          
c   -- var.elim.:  5000/14213          
c   -- var.elim.:  6000/14213          
c   -- var.elim.:  7000/14213          
c   -- var.elim.:  8000/14213          
c   -- var.elim.:  9000/14213          
c   -- var.elim.:  10000/14213          
c   -- var.elim.:  11000/14213          
c   -- var.elim.:  12000/14213          
c   -- var.elim.:  13000/14213          
c   -- var.elim.:  14000/14213          
c   -- var.elim.:  14213/14213          
c   -- var.elim.:  1000/8800          
c   -- var.elim.:  2000/8800          
c   -- var.elim.:  3000/8800          
c   -- var.elim.:  4000/8800          
c   -- var.elim.:  5000/8800          
c   -- var.elim.:  6000/8800          
c   -- var.elim.:  7000/8800          
c   -- var.elim.:  8000/8800          
c   -- var.elim.:  8800/8800          
c   -- var.elim.:  1000/6618          
c   -- var.elim.:  2000/6618          
c   -- var.elim.:  3000/6618          
c   -- var.elim.:  4000/6618          
c   -- var.elim.:  5000/6618          
c   -- var.elim.:  6000/6618          
c   -- var.elim.:  6618/6618          
c   -- var.elim.:  1000/5330          
c   -- var.elim.:  2000/5330          
c   -- var.elim.:  3000/5330          
c   -- var.elim.:  4000/5330          
c   -- var.elim.:  5000/5330          
c   -- var.elim.:  5330/5330          
c   -- var.elim.:  1000/4445          
c   -- var.elim.:  2000/4445          
c   -- var.elim.:  3000/4445          
c   -- var.elim.:  4000/4445          
c   -- var.elim.:  4445/4445          
c   -- var.elim.:  1000/2708          
c   -- var.elim.:  2000/2708          
c   -- var.elim.:  2708/2708          
c   -- var.elim.:  1000/1774          
c   -- var.elim.:  1774/1774          
c   -- var.elim.:  630/630          
c   -- var.elim.:  211/211          
c   -- subsuming                       
c   -- var.elim.:  1000/2677          
c   -- var.elim.:  2000/2677          
c   -- var.elim.:  2677/2677          
c |       220 |   18153   118897 |      --     220       --      -- |     --   | -32448/-66456
c |       220 |   18153   118897 |    7261     220    16516    75.1 |  0.006 % |
c |       320 |   18153   118897 |    7987     320    26124    81.6 |  0.166 % |
c |       471 |   18153   118897 |    8786     471    39864    84.6 |  0.166 % |
c |       699 |   18153   118897 |    9664     699    57527    82.3 |  0.166 % |
c |      1036 |   18153   118897 |   10631    1036    90731    87.6 |  0.166 % |
c |      1546 |   18153   118897 |   11694    1546   138642    89.7 |  0.166 % |
c |      2306 |   18153   118897 |   12863    2306   206227    89.4 |  0.166 % |
c |      3447 |   18153   118897 |   14150    3447   319040    92.6 |  0.166 % |
c |      5156 |   18153   118897 |   15565    5156   484076    93.9 |  0.166 % |
c |      7723 |   18153   118897 |   17121    7723   781297   101.2 |  0.166 % |
c |     11568 |   18153   118897 |   18833   11568  1175707   101.6 |  0.166 % |
c |     17335 |   18153   118897 |   20717   17335  1734845   100.1 |  0.166 % |
c |     25984 |   18153   118897 |   22788   16499  3975771   241.0 |  0.166 % |
c ==============================================================================
c (current CPU-time: 199.318 s)
c ==============================================================================
c [1mFound solution: 375[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35357 |   49236   195126 |   14770   15210  2607437   171.4 |  0.166 % |
c   -- subsuming                       
c   -- var.elim.:  1000/28367          
c   -- var.elim.:  2000/28367          
c   -- var.elim.:  3000/28367          
c   -- var.elim.:  4000/28367          
c   -- var.elim.:  5000/28367          
c   -- var.elim.:  6000/28367          
c   -- var.elim.:  7000/28367          
c   -- var.elim.:  8000/28367          
c   -- var.elim.:  9000/28367          
c   -- var.elim.:  10000/28367          
c   -- var.elim.:  11000/28367          
c   -- var.elim.:  12000/28367          
c   -- var.elim.:  13000/28367          
c   -- var.elim.:  14000/28367          
c   -- var.elim.:  15000/28367          
c   -- var.elim.:  16000/28367          
c   -- var.elim.:  17000/28367          
c   -- var.elim.:  18000/28367          
c   -- var.elim.:  19000/28367          
c   -- var.elim.:  20000/28367          
c   -- var.elim.:  21000/28367          
c   -- var.elim.:  22000/28367          
c   -- var.elim.:  23000/28367          
c   -- var.elim.:  24000/28367          
c   -- var.elim.:  25000/28367          
c   -- var.elim.:  26000/28367          
c   -- var.elim.:  27000/28367          
c   -- var.elim.:  28000/28367          
c   -- var.elim.:  28367/28367          
c   -- var.elim.:  1000/13704          
c   -- var.elim.:  2000/13704          
c   -- var.elim.:  3000/13704          
c   -- var.elim.:  4000/13704          
c   -- var.elim.:  5000/13704          
c   -- var.elim.:  6000/13704          
c   -- var.elim.:  7000/13704          
c   -- var.elim.:  8000/13704          
c   -- var.elim.:  9000/13704          
c   -- var.elim.:  10000/13704          
c   -- var.elim.:  11000/13704          
c   -- var.elim.:  12000/13704          
c   -- var.elim.:  13000/13704          
c   -- var.elim.:  13704/13704          
c   -- var.elim.:  1000/8532          
c   -- var.elim.:  2000/8532          
c   -- var.elim.:  3000/8532          
c   -- var.elim.:  4000/8532          
c   -- var.elim.:  5000/8532          
c   -- var.elim.:  6000/8532          
c   -- var.elim.:  7000/8532          
c   -- var.elim.:  8000/8532          
c   -- var.elim.:  8532/8532          
c   -- var.elim.:  1000/6433          
c   -- var.elim.:  2000/6433          
c   -- var.elim.:  3000/6433          
c   -- var.elim.:  4000/6433          
c   -- var.elim.:  5000/6433          
c   -- var.elim.:  6000/6433          
c   -- var.elim.:  6433/6433          
c   -- var.elim.:  1000/5330          
c   -- var.elim.:  2000/5330          
c   -- var.elim.:  3000/5330          
c   -- var.elim.:  4000/5330          
c   -- var.elim.:  5000/5330          
c   -- var.elim.:  5330/5330          
c   -- var.elim.:  1000/4608          
c   -- var.elim.:  2000/4608          
c   -- var.elim.:  3000/4608          
c   -- var.elim.:  4000/4608          
c   -- var.elim.:  4608/4608          
c   -- var.elim.:  1000/3922          
c   -- var.elim.:  2000/3922          
c   -- var.elim.:  3000/3922          
c   -- var.elim.:  3922/3922          
c   -- var.elim.:  1000/2184          
c   -- var.elim.:  2000/2184          
c   -- var.elim.:  2184/2184          
c   -- var.elim.:  388/388          
c   -- var.elim.:  2/2          
c   -- subsuming                       
c   -- var.elim.:  1000/2735          
c   -- var.elim.:  2000/2735          
c   -- var.elim.:  2735/2735          
c |     35357 |   18398   128795 |      --   15210       --      -- |     --   | -30836/-66326
c |     35357 |   18398   128795 |    7359   14525  1576153   108.5 |  0.166 % |
c ==============================================================================
c (current CPU-time: 249.32 s)
c ==============================================================================
c [1mFound solution: 373[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35437 |   48230   202127 |   14468    6536   589392    90.2 |  0.166 % |
c   -- subsuming                       
c   -- var.elim.:  1000/27410          
c   -- var.elim.:  2000/27410          
c   -- var.elim.:  3000/27410          
c   -- var.elim.:  4000/27410          
c   -- var.elim.:  5000/27410          
c   -- var.elim.:  6000/27410          
c   -- var.elim.:  7000/27410          
c   -- var.elim.:  8000/27410          
c   -- var.elim.:  9000/27410          
c   -- var.elim.:  10000/27410          
c   -- var.elim.:  11000/27410          
c   -- var.elim.:  12000/27410          
c   -- var.elim.:  13000/27410          
c   -- var.elim.:  14000/27410          
c   -- var.elim.:  15000/27410          
c   -- var.elim.:  16000/27410          
c   -- var.elim.:  17000/27410          
c   -- var.elim.:  18000/27410          
c   -- var.elim.:  19000/27410          
c   -- var.elim.:  20000/27410          
c   -- var.elim.:  21000/27410          
c   -- var.elim.:  22000/27410          
c   -- var.elim.:  23000/27410          
c   -- var.elim.:  24000/27410          
c   -- var.elim.:  25000/27410          
c   -- var.elim.:  26000/27410          
c   -- var.elim.:  27000/27410          
c   -- var.elim.:  27410/27410          
c   -- var.elim.:  1000/13205          
c   -- var.elim.:  2000/13205          
c   -- var.elim.:  3000/13205          
c   -- var.elim.:  4000/13205          
c   -- var.elim.:  5000/13205          
c   -- var.elim.:  6000/13205          
c   -- var.elim.:  7000/13205          
c   -- var.elim.:  8000/13205          
c   -- var.elim.:  9000/13205          
c   -- var.elim.:  10000/13205          
c   -- var.elim.:  11000/13205          
c   -- var.elim.:  12000/13205          
c   -- var.elim.:  13000/13205          
c   -- var.elim.:  13205/13205          
c   -- var.elim.:  1000/8265          
c   -- var.elim.:  2000/8265          
c   -- var.elim.:  3000/8265          
c   -- var.elim.:  4000/8265          
c   -- var.elim.:  5000/8265          
c   -- var.elim.:  6000/8265          
c   -- var.elim.:  7000/8265          
c   -- var.elim.:  8000/8265          
c   -- var.elim.:  8265/8265          
c   -- var.elim.:  1000/6182          
c   -- var.elim.:  2000/6182          
c   -- var.elim.:  3000/6182          
c   -- var.elim.:  4000/6182          
c   -- var.elim.:  5000/6182          
c   -- var.elim.:  6000/6182          
c   -- var.elim.:  6182/6182          
c   -- var.elim.:  1000/4964          
c   -- var.elim.:  2000/4964          
c   -- var.elim.:  3000/4964          
c   -- var.elim.:  4000/4964          
c   -- var.elim.:  4964/4964          
c   -- var.elim.:  1000/3847          
c   -- var.elim.:  2000/3847          
c   -- var.elim.:  3000/3847          
c   -- var.elim.:  3847/3847          
c   -- var.elim.:  1000/2608          
c   -- var.elim.:  2000/2608          
c   -- var.elim.:  2608/2608          
c   -- var.elim.:  669/669          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/1322          
c   -- var.elim.:  1322/1322          
c |     35437 |   18518   133823 |      --    6536       --      -- |     --   | -29712/-68303
c |     35437 |   18518   133823 |    7407    6536   589392    90.2 |  0.166 % |
c |     35537 |   18518   133823 |    8147    6636   637296    96.0 |  0.279 % |
c |     35688 |   18518   133823 |    8962    6787   704613   103.8 |  0.279 % |
c |     35914 |   18241   131386 |    9711    7002   849968   121.4 |  2.071 % |
c |     36251 |   18183   130848 |   10648    7335   908391   123.8 |  2.439 % |
c |     36758 |   18183   130848 |   11713    7842   961173   122.6 |  2.439 % |
c |     37518 |   18183   130848 |   12884    8602  1038821   120.8 |  2.439 % |
c |     38657 |   18144   130464 |   14143    9739  1293277   132.8 |  2.644 % |
c |     40365 |   18144   130464 |   15557   11447  1489536   130.1 |  2.644 % |
c |     42930 |   17923   128752 |   16904   14003  3576600   255.4 |  4.040 % |
c |     46774 |   17828   128121 |   18496   12017  5372612   447.1 |  4.642 % |
c |     52540 |   17828   128121 |   20346   17783  6067636   341.2 |  4.642 % |
c ==============================================================================
c (current CPU-time: 391.722 s)
c ==============================================================================
c [1mFound solution: 372[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     55567 |   17781   127448 |    5334   20807  8893489   427.4 |  4.642 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4585          
c   -- var.elim.:  2000/4585          
c   -- var.elim.:  3000/4585          
c   -- var.elim.:  4000/4585          
c   -- var.elim.:  4585/4585          
c   -- var.elim.:  223/223          
c   -- subsuming                       
c   -- var.elim.:  618/618          
c |     55567 |   17700   126745 |      --   20807       --      -- |     --   | -44/-107
c |     55567 |   17700   126745 |    7080   16216  2012811   124.1 |  4.642 % |
c |     55668 |   17700   126745 |    7788    7201   904791   125.6 |  5.328 % |
c |     55819 |   17634   126202 |    8534    7350  1010212   137.4 |  5.756 % |
c |     56046 |   17634   126202 |    9388    7577  1301497   171.8 |  5.756 % |
c |     56383 |   17600   125927 |   10307    7913  1582497   200.0 |  5.962 % |
c |     56892 |   17600   125927 |   11337    8422  2016615   239.4 |  5.962 % |
c |     57651 |   17600   125927 |   12471    9181  2592355   282.4 |  5.962 % |
c |     58792 |   17600   125927 |   13718   10322  2690381   260.6 |  5.962 % |
c |     60501 |   17600   125927 |   15090   12031  2849315   236.8 |  5.962 % |
c |     63063 |   17549   125491 |   16551   14591  3329726   228.2 |  6.272 % |
c |     66909 |   17522   125247 |   18179   12609  2511528   199.2 |  6.434 % |
c |     72676 |   17388   124337 |   19843   18372  5130409   279.3 |  7.231 % |
c |     81325 |   17156   121865 |   21537   18728  7620640   406.9 |  8.648 % |
c |     94299 |   16713   117305 |   23079   22069  5758668   260.9 | 11.555 % |
c |    113762 |   16389   113293 |   24894   18195 14246861   783.0 | 13.710 % |
c |    142957 |   16389   113293 |   27384   23240  2776161   119.5 | 13.710 % |
c |    186746 |   16389   113293 |   30122   21732 13903973   639.8 | 13.710 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 x3 -x4 -x5 x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 -x45 x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 -x59 x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 -x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 -x115 x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 -x129 -x130 x131 -x132 x133 -x134 -x135 -x136 -x137 -x138 x139 -x140 x141 -x142 -x143 -x144 x145 -x146 -x147 -x148 -x149 -x150 x151 -x152 x153 -x154 -x155 x156 -x157 -x158 x159 -x160 -x161 -x162 x163 -x164 x165 -x166 -x167 -x168 -x169 x170 x171 -x172 -x173 -x174 x175 -x176 x17#### 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 0.98 0.91 2/55 26641
Raw data (stat): 26641 (runsolver) R 26640 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480170966 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 26641
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 4626 0 0 0 984 15 0 0 25 0 1 0 480170966 21258240 4540 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5190 4540 603 41 0 5149 0
vsize: 20760
[startup+20.0009 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 4733 0 0 0 1977 22 0 0 25 0 1 0 480170966 21712896 4647 4294967295 134512640 134672761 3221224576 3221223024 134643777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5301 4647 603 41 0 5260 0
vsize: 21204
[startup+30.0015 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 4735 0 0 0 2976 23 0 0 25 0 1 0 480170966 21712896 4649 4294967295 134512640 134672761 3221224576 3221222976 134604052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5301 4649 603 41 0 5260 0
vsize: 21204
[startup+40.0015 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 6637 0 0 0 3964 35 0 0 25 0 1 0 480170966 27271168 5825 4294967295 134512640 134672761 3221224576 3221222960 134541847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6658 5825 603 41 0 6617 0
vsize: 26632
[startup+50.0021 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 6702 0 0 0 4951 37 0 0 25 0 1 0 480170966 27541504 5890 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6724 5890 603 41 0 6683 0
vsize: 26896
[startup+60.0023 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 6707 0 0 0 5941 47 0 0 25 0 1 0 480170966 27541504 5895 4294967295 134512640 134672761 3221224576 3221222784 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6724 5895 603 41 0 6683 0
vsize: 26896
[startup+70.0023 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 6709 0 0 0 6939 49 0 0 25 0 1 0 480170966 27541504 5897 4294967295 134512640 134672761 3221224576 3221223024 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6724 5897 603 41 0 6683 0
vsize: 26896
[startup+80.0024 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 6710 0 0 0 7938 50 0 0 25 0 1 0 480170966 27541504 5898 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6724 5898 603 41 0 6683 0
vsize: 26896
[startup+90.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 7039 0 0 0 8938 50 0 0 25 0 1 0 480170966 28995584 6227 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7079 6227 603 41 0 7038 0
vsize: 28316
[startup+100.003 s]
Raw data (loadavg): 0.99 0.98 0.91 3/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 7466 0 0 0 9936 52 0 0 25 0 1 0 480170966 30728192 6654 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7502 6654 603 41 0 7461 0
vsize: 30008
[startup+110.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 7897 0 0 0 10934 54 0 0 25 0 1 0 480170966 32460800 7085 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7925 7085 603 41 0 7884 0
vsize: 31700
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 8253 0 0 0 11933 55 0 0 25 0 1 0 480170966 34025472 7441 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8307 7441 603 41 0 8266 0
vsize: 33228
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 8648 0 0 0 12932 56 0 0 25 0 1 0 480170966 35606528 7836 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8693 7836 603 41 0 8652 0
vsize: 34772
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 9657 0 0 0 13930 58 0 0 25 0 1 0 480170966 39735296 8845 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9701 8845 603 41 0 9660 0
vsize: 38804
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 10393 0 0 0 14929 59 0 0 25 0 1 0 480170966 42799104 9581 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10449 9581 603 41 0 10408 0
vsize: 41796
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 10743 0 0 0 15928 60 0 0 25 0 1 0 480170966 44244992 9931 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10802 9931 603 41 0 10761 0
vsize: 43208
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 10986 0 0 0 16927 61 0 0 25 0 1 0 480170966 45174784 10174 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11029 10174 603 41 0 10988 0
vsize: 44116
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 11210 0 0 0 17926 62 0 0 25 0 1 0 480170966 46100480 10398 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11255 10398 603 41 0 11214 0
vsize: 45020
[startup+190.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 11434 0 0 0 18926 63 0 0 25 0 1 0 480170966 47026176 10622 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11481 10622 603 41 0 11440 0
vsize: 45924
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 11485 0 0 0 19926 63 0 0 25 0 1 0 480170966 47243264 10673 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11534 10673 603 41 0 11493 0
vsize: 46136
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 13795 0 0 0 20909 80 0 0 25 0 1 0 480170966 53231616 11316 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12996 11316 603 41 0 12955 0
vsize: 51984
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 13795 0 0 0 21905 84 0 0 25 0 1 0 480170966 53231616 11316 4294967295 134512640 134672761 3221224576 3221223024 134643937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12996 11316 603 41 0 12955 0
vsize: 51984
[startup+230.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 13795 0 0 0 22901 88 0 0 25 0 1 0 480170966 53231616 11316 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12996 11316 603 41 0 12955 0
vsize: 51984
[startup+240.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 13795 0 0 0 23901 89 0 0 25 0 1 0 480170966 53231616 11316 4294967295 134512640 134672761 3221224576 3221223024 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12996 11316 603 41 0 12955 0
vsize: 51984
[startup+250.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 13850 0 0 0 24901 89 0 0 25 0 1 0 480170966 53231616 11321 4294967295 134512640 134672761 3221224576 3221223672 134616336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12996 11321 603 41 0 12955 0
vsize: 51984
[startup+260.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16761 0 0 0 25881 108 0 0 25 0 1 0 480170966 53321728 11744 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13018 11744 603 41 0 12977 0
vsize: 52072
[startup+270.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16761 0 0 0 26881 108 0 0 25 0 1 0 480170966 53321728 11744 4294967295 134512640 134672761 3221224576 3221223024 134643719 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13018 11744 603 41 0 12977 0
vsize: 52072
[startup+280.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16761 0 0 0 27862 113 0 0 25 0 1 0 480170966 53321728 11744 4294967295 134512640 134672761 3221224576 3221223024 134643969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13018 11744 603 41 0 12977 0
vsize: 52072
[startup+290.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16761 0 0 0 28861 115 0 0 25 0 1 0 480170966 53321728 11744 4294967295 134512640 134672761 3221224576 3221223024 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13018 11744 603 41 0 12977 0
vsize: 52072
[startup+300.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16761 0 0 0 29861 115 0 0 25 0 1 0 480170966 53321728 11744 4294967295 134512640 134672761 3221224576 3221223024 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13018 11744 603 41 0 12977 0
vsize: 52072
[startup+310.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26643
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16761 0 0 0 30862 115 0 0 25 0 1 0 480170966 53321728 11744 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13018 11744 603 41 0 12977 0
vsize: 52072
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16761 0 0 0 31862 115 0 0 25 0 1 0 480170966 53321728 11744 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13018 11744 603 41 0 12977 0
vsize: 52072
[startup+330.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 16865 0 0 0 32862 115 0 0 25 0 1 0 480170966 53850112 11848 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13147 11848 603 41 0 13106 0
vsize: 52588
[startup+340.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 18619 0 0 0 33858 119 0 0 25 0 1 0 480170966 60960768 13602 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14883 13602 603 41 0 14842 0
vsize: 59532
[startup+350.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 19582 0 0 0 34857 121 0 0 25 0 1 0 480170966 64942080 14564 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15855 14564 603 41 0 15814 0
vsize: 63420
[startup+360.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 19582 0 0 0 35857 121 0 0 25 0 1 0 480170966 64942080 14564 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15855 14564 603 41 0 15814 0
vsize: 63420
[startup+370.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 19582 0 0 0 36857 121 0 0 25 0 1 0 480170966 64942080 14564 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15855 14564 603 41 0 15814 0
vsize: 63420
[startup+380.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 20600 0 0 0 37855 123 0 0 25 0 1 0 480170966 69083136 15582 4294967295 134512640 134672761 3221224576 3221223616 134613120 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16866 15582 603 41 0 16825 0
vsize: 67464
[startup+390.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 21598 0 0 0 38853 125 0 0 25 0 1 0 480170966 73162752 16580 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17862 16580 603 41 0 17821 0
vsize: 71448
[startup+400.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30246 0 0 0 39820 158 0 0 25 0 1 0 480170966 76132352 17305 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18587 17305 603 41 0 18546 0
vsize: 74348
[startup+410.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 40820 158 0 0 25 0 1 0 480170966 76038144 17282 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18564 17282 603 41 0 18523 0
vsize: 74256
[startup+420.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 41820 158 0 0 25 0 1 0 480170966 76038144 17282 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18564 17282 603 41 0 18523 0
vsize: 74256
[startup+430.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 42820 158 0 0 25 0 1 0 480170966 76038144 17282 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18564 17282 603 41 0 18523 0
vsize: 74256
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 43820 158 0 0 25 0 1 0 480170966 76038144 17282 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18564 17282 603 41 0 18523 0
vsize: 74256
[startup+450.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 44820 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+460.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 45820 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+470.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 46820 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223616 134614196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+480.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 47821 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+490.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 48821 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+500.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 49821 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+510.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 50821 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+520.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30395 0 0 0 51821 159 0 0 25 0 1 0 480170966 75984896 17269 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18551 17269 603 41 0 18510 0
vsize: 74204
[startup+530.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 30507 0 0 0 52821 159 0 0 25 0 1 0 480170966 76496896 17381 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18676 17381 603 41 0 18635 0
vsize: 74704
[startup+540.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31390 0 0 0 53820 161 0 0 25 0 1 0 480170966 80117760 18264 4294967295 134512640 134672761 3221224576 3221223720 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19560 18264 603 41 0 19519 0
vsize: 78240
[startup+550.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31414 0 0 0 54820 161 0 0 25 0 1 0 480170966 80183296 18287 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19576 18287 603 41 0 19535 0
vsize: 78304
[startup+560.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31415 0 0 0 55820 161 0 0 25 0 1 0 480170966 80183296 18288 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19576 18288 603 41 0 19535 0
vsize: 78304
[startup+570.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31415 0 0 0 56820 161 0 0 25 0 1 0 480170966 80183296 18288 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19576 18288 603 41 0 19535 0
vsize: 78304
[startup+580.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31415 0 0 0 57820 161 0 0 25 0 1 0 480170966 80183296 18288 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19576 18288 603 41 0 19535 0
vsize: 78304
[startup+590.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31419 0 0 0 58820 161 0 0 25 0 1 0 480170966 80175104 18291 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 18291 603 41 0 19533 0
vsize: 78296
[startup+600.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31419 0 0 0 59821 161 0 0 25 0 1 0 480170966 80175104 18291 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 18291 603 41 0 19533 0
vsize: 78296
[startup+610.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26645
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31419 0 0 0 60821 161 0 0 25 0 1 0 480170966 80175104 18291 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 18291 603 41 0 19533 0
vsize: 78296
[startup+620.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31419 0 0 0 61821 161 0 0 25 0 1 0 480170966 80175104 18291 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 18291 603 41 0 19533 0
vsize: 78296
[startup+630.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31419 0 0 0 62821 161 0 0 25 0 1 0 480170966 80175104 18291 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19574 18291 603 41 0 19533 0
vsize: 78296
[startup+640.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 31825 0 0 0 63821 162 0 0 25 0 1 0 480170966 81854464 18697 4294967295 134512640 134672761 3221224576 3221223584 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19984 18697 603 41 0 19943 0
vsize: 79936
[startup+650.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 33025 0 0 0 64819 164 0 0 25 0 1 0 480170966 86806528 19897 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21193 19897 603 41 0 21152 0
vsize: 84772
[startup+660.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 34069 0 0 0 65816 167 0 0 25 0 1 0 480170966 91078656 20941 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22236 20941 603 41 0 22195 0
vsize: 88944
[startup+670.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 35267 0 0 0 66814 169 0 0 25 0 1 0 480170966 95977472 22139 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23432 22139 603 41 0 23391 0
vsize: 93728
[startup+680.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 35435 0 0 0 67814 169 0 0 25 0 1 0 480170966 96641024 22306 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23594 22306 603 41 0 23553 0
vsize: 94376
[startup+690.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 35435 0 0 0 68814 169 0 0 25 0 1 0 480170966 96641024 22306 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23594 22306 603 41 0 23553 0
vsize: 94376
[startup+700.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 35990 0 0 0 69814 170 0 0 25 0 1 0 480170966 98910208 22861 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24148 22861 603 41 0 24107 0
vsize: 96592
[startup+710.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 36365 0 0 0 70813 171 0 0 25 0 1 0 480170966 100491264 23236 4294967295 134512640 134672761 3221224576 3221223616 134614171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24534 23236 603 41 0 24493 0
vsize: 98136
[startup+720.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 37231 0 0 0 71811 173 0 0 25 0 1 0 480170966 104091648 24102 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25413 24102 603 41 0 25372 0
vsize: 101652
[startup+730.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 38678 0 0 0 72809 175 0 0 25 0 1 0 480170966 109961216 25549 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26846 25549 603 41 0 26805 0
vsize: 107384
[startup+740.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39067 0 0 0 73808 176 0 0 25 0 1 0 480170966 111505408 25938 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27223 25938 603 41 0 27182 0
vsize: 108892
[startup+750.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39291 0 0 0 74808 177 0 0 25 0 1 0 480170966 112443392 26161 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27452 26161 603 41 0 27411 0
vsize: 109808
[startup+760.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39291 0 0 0 75808 177 0 0 25 0 1 0 480170966 112443392 26161 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27452 26161 603 41 0 27411 0
vsize: 109808
[startup+770.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39293 0 0 0 76808 177 0 0 25 0 1 0 480170966 112443392 26163 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27452 26163 603 41 0 27411 0
vsize: 109808
[startup+780.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39293 0 0 0 77808 177 0 0 25 0 1 0 480170966 112443392 26163 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27452 26163 603 41 0 27411 0
vsize: 109808
[startup+790.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39293 0 0 0 78808 177 0 0 25 0 1 0 480170966 112443392 26163 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27452 26163 603 41 0 27411 0
vsize: 109808
[startup+800.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39293 0 0 0 79808 177 0 0 25 0 1 0 480170966 112439296 26162 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26162 603 41 0 27410 0
vsize: 109804
[startup+810.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39293 0 0 0 80809 177 0 0 25 0 1 0 480170966 112439296 26162 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26162 603 41 0 27410 0
vsize: 109804
[startup+820.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39293 0 0 0 81808 177 0 0 25 0 1 0 480170966 112439296 26162 4294967295 134512640 134672761 3221224576 3221223760 134615722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27451 26162 603 41 0 27410 0
vsize: 109804
[startup+830.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39293 0 0 0 82808 177 0 0 25 0 1 0 480170966 112439296 26162 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26162 603 41 0 27410 0
vsize: 109804
[startup+840.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39294 0 0 0 83808 177 0 0 25 0 1 0 480170966 112439296 26163 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26163 603 41 0 27410 0
vsize: 109804
[startup+850.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39295 0 0 0 84808 177 0 0 25 0 1 0 480170966 112439296 26164 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26164 603 41 0 27410 0
vsize: 109804
[startup+860.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39297 0 0 0 85809 177 0 0 25 0 1 0 480170966 112439296 26166 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26166 603 41 0 27410 0
vsize: 109804
[startup+870.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39297 0 0 0 86809 177 0 0 25 0 1 0 480170966 112439296 26166 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26166 603 41 0 27410 0
vsize: 109804
[startup+880.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39297 0 0 0 87809 177 0 0 25 0 1 0 480170966 112439296 26166 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26166 603 41 0 27410 0
vsize: 109804
[startup+890.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39297 0 0 0 88809 177 0 0 25 0 1 0 480170966 112439296 26166 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26166 603 41 0 27410 0
vsize: 109804
[startup+900.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39297 0 0 0 89809 177 0 0 25 0 1 0 480170966 112439296 26166 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26166 603 41 0 27410 0
vsize: 109804
[startup+910.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26647
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39297 0 0 0 90809 177 0 0 25 0 1 0 480170966 112439296 26166 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26166 603 41 0 27410 0
vsize: 109804
[startup+920.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39298 0 0 0 91810 177 0 0 25 0 1 0 480170966 112439296 26167 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27451 26167 603 41 0 27410 0
vsize: 109804
[startup+930.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39300 0 0 0 92810 177 0 0 25 0 1 0 480170966 112435200 26169 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26169 603 41 0 27409 0
vsize: 109800
[startup+940.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39300 0 0 0 93810 178 0 0 25 0 1 0 480170966 112435200 26169 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26169 603 41 0 27409 0
vsize: 109800
[startup+950.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39300 0 0 0 94810 178 0 0 25 0 1 0 480170966 112435200 26169 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26169 603 41 0 27409 0
vsize: 109800
[startup+960.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39300 0 0 0 95810 178 0 0 25 0 1 0 480170966 112435200 26169 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26169 603 41 0 27409 0
vsize: 109800
[startup+970.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39300 0 0 0 96810 178 0 0 25 0 1 0 480170966 112435200 26169 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26169 603 41 0 27409 0
vsize: 109800
[startup+980.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39300 0 0 0 97811 178 0 0 25 0 1 0 480170966 112435200 26169 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26169 603 41 0 27409 0
vsize: 109800
[startup+990.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39300 0 0 0 98811 178 0 0 25 0 1 0 480170966 112435200 26169 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26169 603 41 0 27409 0
vsize: 109800
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 99811 178 0 0 25 0 1 0 480170966 112435200 26170 4294967295 134512640 134672761 3221224576 3221222272 134645466 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27450 26170 603 41 0 27409 0
vsize: 109800
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 100811 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 101811 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223616 134613818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 102811 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 103812 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 104812 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223616 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 105812 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 106812 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 107812 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 39301 0 0 0 108813 178 0 0 25 0 1 0 480170966 112431104 26170 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26170 603 41 0 27408 0
vsize: 109796
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 40108 0 0 0 109812 179 0 0 25 0 1 0 480170966 115802112 26977 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28272 26977 603 41 0 28231 0
vsize: 113088
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 40860 0 0 0 110811 180 0 0 25 0 1 0 480170966 118915072 27729 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29032 27729 603 41 0 28991 0
vsize: 116128
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 41431 0 0 0 111809 181 0 0 25 0 1 0 480170966 121188352 28300 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29587 28300 603 41 0 29546 0
vsize: 118348
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 42819 0 0 0 112808 183 0 0 25 0 1 0 480170966 126840832 29688 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30967 29688 603 41 0 30926 0
vsize: 123868
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43306 0 0 0 113807 184 0 0 25 0 1 0 480170966 128946176 30172 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30172 603 41 0 31440 0
vsize: 125924
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43306 0 0 0 114807 184 0 0 25 0 1 0 480170966 128946176 30172 4294967295 134512640 134672761 3221224576 3221223720 134616183 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30172 603 41 0 31440 0
vsize: 125924
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43307 0 0 0 115807 184 0 0 25 0 1 0 480170966 128946176 30173 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30173 603 41 0 31440 0
vsize: 125924
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43307 0 0 0 116808 184 0 0 25 0 1 0 480170966 128946176 30173 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30173 603 41 0 31440 0
vsize: 125924
[startup+1180.01 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43307 0 0 0 117808 184 0 0 25 0 1 0 480170966 128946176 30173 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30173 603 41 0 31440 0
vsize: 125924
[startup+1190.01 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43307 0 0 0 118808 184 0 0 25 0 1 0 480170966 128946176 30173 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30173 603 41 0 31440 0
vsize: 125924
[startup+1200.01 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43307 0 0 0 119808 184 0 0 25 0 1 0 480170966 128946176 30173 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30173 603 41 0 31440 0
vsize: 125924
[startup+1210.01 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 26649
Raw data (stat): 26641 (minisat+) R 26640 20838 20837 0 -1 0 43307 0 0 0 120808 184 0 0 25 0 1 0 480170966 128946176 30173 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31481 30173 603 41 0 31440 0
vsize: 125924
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.1 s]
Raw data (loadavg): 1.04 1.00 0.92 1/55 26649
Raw data (stat): 26641 (minisat+) Z 26640 20838 20837 0 -1 12 43308 0 0 0 120808 192 0 0 25 0 1 0 480170966 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): 1210.1
CPU time (s): 1210.02
CPU user time (s): 1208.09
CPU system time (s): 1.92971
CPU usage (%): 99.9936
Max. virtual memory (Kb): 125924
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####