PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-C432.opb
MD5SUM	6292e63147fb202dc159fbf5a9ff5c77
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4822
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	33355
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	33355
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	771
Total number of constraints	1951
Number of constraints which are clauses	1949
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 5590

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 00:37:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4008 boxname=wulflinc31 idbench=248 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6292e63147fb202dc159fbf5a9ff5c77  /oldhome/oroussel/tmp/wulflinc31/normalized-C432.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc31/normalized-C432.opb /oldhome/oroussel/tmp/wulflinc31/normalized-C432.opb
IDLAUNCH: 4008
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        906480 kB
Buffers:         35604 kB
Cached:          54104 kB
SwapCached:        392 kB
Active:          51092 kB
Inactive:        41704 kB
HighTotal:      131008 kB
HighFree:        73276 kB
LowTotal:       903652 kB
LowFree:        833204 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29804 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:57:42 (client local time) WITH STATUS 10 IN 1210.11 SECONDS
stats: 4008 7 1210.11 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1905 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 |    1891     9233 |     567       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  704/704          
c |         0 |    1808     8928 |      --       0       --      -- |     --   | -83/-305
c |         0 |    1808     8928 |     723       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.097985 s)
c ==============================================================================
c [1mFound solution: 7184[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:125007     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  296770   697520 |   89030       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/114054          
c   -- var.elim.:  2000/114054          
c   -- var.elim.:  3000/114054          
c   -- var.elim.:  4000/114054          
c   -- var.elim.:  5000/114054          
c   -- var.elim.:  6000/114054          
c   -- var.elim.:  7000/114054          
c   -- var.elim.:  8000/114054          
c   -- var.elim.:  9000/114054          
c   -- var.elim.:  10000/114054          
c   -- var.elim.:  11000/114054          
c   -- var.elim.:  12000/114054          
c   -- var.elim.:  13000/114054          
c   -- var.elim.:  14000/114054          
c   -- var.elim.:  15000/114054          
c   -- var.elim.:  16000/114054          
c   -- var.elim.:  17000/114054          
c   -- var.elim.:  18000/114054          
c   -- var.elim.:  19000/114054          
c   -- var.elim.:  20000/114054          
c   -- var.elim.:  21000/114054          
c   -- var.elim.:  22000/114054          
c   -- var.elim.:  23000/114054          
c   -- var.elim.:  24000/114054          
c   -- var.elim.:  25000/114054          
c   -- var.elim.:  26000/114054          
c   -- var.elim.:  27000/114054          
c   -- var.elim.:  28000/114054          
c   -- var.elim.:  29000/114054          
c   -- var.elim.:  30000/114054          
c   -- var.elim.:  31000/114054          
c   -- var.elim.:  32000/114054          
c   -- var.elim.:  33000/114054          
c   -- var.elim.:  34000/114054          
c   -- var.elim.:  35000/114054          
c   -- var.elim.:  36000/114054          
c   -- var.elim.:  37000/114054          
c   -- var.elim.:  38000/114054          
c   -- var.elim.:  39000/114054          
c   -- var.elim.:  40000/114054          
c   -- var.elim.:  41000/114054          
c   -- var.elim.:  42000/114054          
c   -- var.elim.:  43000/114054          
c   -- var.elim.:  44000/114054          
c   -- var.elim.:  45000/114054          
c   -- var.elim.:  46000/114054          
c   -- var.elim.:  47000/114054          
c   -- var.elim.:  48000/114054          
c   -- var.elim.:  49000/114054          
c   -- var.elim.:  50000/114054          
c   -- var.elim.:  51000/114054          
c   -- var.elim.:  52000/114054          
c   -- var.elim.:  53000/114054          
c   -- var.elim.:  54000/114054          
c   -- var.elim.:  55000/114054          
c   -- var.elim.:  56000/114054          
c   -- var.elim.:  57000/114054          
c   -- var.elim.:  58000/114054          
c   -- var.elim.:  59000/114054          
c   -- var.elim.:  60000/114054          
c   -- var.elim.:  61000/114054          
c   -- var.elim.:  62000/114054          
c   -- var.elim.:  63000/114054          
c   -- var.elim.:  64000/114054          
c   -- var.elim.:  65000/114054          
c   -- var.elim.:  66000/114054          
c   -- var.elim.:  67000/114054          
c   -- var.elim.:  68000/114054          
c   -- var.elim.:  69000/114054          
c   -- var.elim.:  70000/114054          
c   -- var.elim.:  71000/114054          
c   -- var.elim.:  72000/114054          
c   -- var.elim.:  73000/114054          
c   -- var.elim.:  74000/114054          
c   -- var.elim.:  75000/114054          
c   -- var.elim.:  76000/114054          
c   -- var.elim.:  77000/114054          
c   -- var.elim.:  78000/114054          
c   -- var.elim.:  79000/114054          
c   -- var.elim.:  80000/114054          
c   -- var.elim.:  81000/114054          
c   -- var.elim.:  82000/114054          
c   -- var.elim.:  83000/114054          
c   -- var.elim.:  84000/114054          
c   -- var.elim.:  85000/114054          
c   -- var.elim.:  86000/114054          
c   -- var.elim.:  87000/114054          
c   -- var.elim.:  88000/114054          
c   -- var.elim.:  89000/114054          
c   -- var.elim.:  90000/114054          
c   -- var.elim.:  91000/114054          
c   -- var.elim.:  92000/114054          
c   -- var.elim.:  93000/114054          
c   -- var.elim.:  94000/114054          
c   -- var.elim.:  95000/114054          
c   -- var.elim.:  96000/114054          
c   -- var.elim.:  97000/114054          
c   -- var.elim.:  98000/114054          
c   -- var.elim.:  99000/114054          
c   -- var.elim.:  100000/114054          
c   -- var.elim.:  101000/114054          
c   -- var.elim.:  102000/114054          
c   -- var.elim.:  103000/114054          
c   -- var.elim.:  104000/114054          
c   -- var.elim.:  105000/114054          
c   -- var.elim.:  106000/114054          
c   -- var.elim.:  107000/114054          
c   -- var.elim.:  108000/114054          
c   -- var.elim.:  109000/114054          
c   -- var.elim.:  110000/114054          
c   -- var.elim.:  111000/114054          
c   -- var.elim.:  112000/114054          
c   -- var.elim.:  113000/114054          
c   -- var.elim.:  114000/114054          
c   -- var.elim.:  114054/114054          
c   -- var.elim.:  1000/60779          
c   -- var.elim.:  2000/60779          
c   -- var.elim.:  3000/60779          
c   -- var.elim.:  4000/60779          
c   -- var.elim.:  5000/60779          
c   -- var.elim.:  6000/60779          
c   -- var.elim.:  7000/60779          
c   -- var.elim.:  8000/60779          
c   -- var.elim.:  9000/60779          
c   -- var.elim.:  10000/60779          
c   -- var.elim.:  11000/60779          
c   -- var.elim.:  12000/60779          
c   -- var.elim.:  13000/60779          
c   -- var.elim.:  14000/60779          
c   -- var.elim.:  15000/60779          
c   -- var.elim.:  16000/60779          
c   -- var.elim.:  17000/60779          
c   -- var.elim.:  18000/60779          
c   -- var.elim.:  19000/60779          
c   -- var.elim.:  20000/60779          
c   -- var.elim.:  21000/60779          
c   -- var.elim.:  22000/60779          
c   -- var.elim.:  23000/60779          
c   -- var.elim.:  24000/60779          
c   -- var.elim.:  25000/60779          
c   -- var.elim.:  26000/60779          
c   -- var.elim.:  27000/60779          
c   -- var.elim.:  28000/60779          
c   -- var.elim.:  29000/60779          
c   -- var.elim.:  30000/60779          
c   -- var.elim.:  31000/60779          
c   -- var.elim.:  32000/60779          
c   -- var.elim.:  33000/60779          
c   -- var.elim.:  34000/60779          
c   -- var.elim.:  35000/60779          
c   -- var.elim.:  36000/60779          
c   -- var.elim.:  37000/60779          
c   -- var.elim.:  38000/60779          
c   -- var.elim.:  39000/60779          
c   -- var.elim.:  40000/60779          
c   -- var.elim.:  41000/60779          
c   -- var.elim.:  42000/60779          
c   -- var.elim.:  43000/60779          
c   -- var.elim.:  44000/60779          
c   -- var.elim.:  45000/60779          
c   -- var.elim.:  46000/60779          
c   -- var.elim.:  47000/60779          
c   -- var.elim.:  48000/60779          
c   -- var.elim.:  49000/60779          
c   -- var.elim.:  50000/60779          
c   -- var.elim.:  51000/60779          
c   -- var.elim.:  52000/60779          
c   -- var.elim.:  53000/60779          
c   -- var.elim.:  54000/60779          
c   -- var.elim.:  55000/60779          
c   -- var.elim.:  56000/60779          
c   -- var.elim.:  57000/60779          
c   -- var.elim.:  58000/60779          
c   -- var.elim.:  59000/60779          
c   -- var.elim.:  60000/60779          
c   -- var.elim.:  60779/60779          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/15340          
c   -- var.elim.:  2000/15340          
c   -- var.elim.:  3000/15340          
c   -- var.elim.:  4000/15340          
c   -- var.elim.:  5000/15340          
c   -- var.elim.:  6000/15340          
c   -- var.elim.:  7000/15340          
c   -- var.elim.:  8000/15340          
c   -- var.elim.:  9000/15340          
c   -- var.elim.:  10000/15340          
c   -- var.elim.:  11000/15340          
c   -- var.elim.:  12000/15340          
c   -- var.elim.:  13000/15340          
c   -- var.elim.:  14000/15340          
c   -- var.elim.:  15000/15340          
c   -- var.elim.:  15340/15340          
c   -- var.elim.:  1000/2726          
c   -- var.elim.:  2000/2726          
c   -- var.elim.:  2726/2726          
c   -- var.elim.:  632/632          
c   -- var.elim.:  1000/1139          
c   -- var.elim.:  1139/1139          
c   -- subsuming                       
c   -- var.elim.:  1000/1618          
c   -- var.elim.:  1618/1618          
c   -- var.elim.:  6/6          
c |         0 |  262116   933394 |      --       0       --      -- |     --   | -34654/235875
c |         0 |  262116   933394 |  104846       0        0     nan |  0.000 % |
c |       100 |  261202   929211 |  114928      97      438     4.5 |  0.259 % |
c |       250 |  261202   929211 |  126421     247     1923     7.8 |  0.259 % |
c |       475 |  261202   929211 |  139063     472     6021    12.8 |  0.259 % |
c |       813 |  260676   927480 |  152662     808     8231    10.2 |  0.391 % |
c |      1319 |  260676   927480 |  167928    1314    13524    10.3 |  0.391 % |
c |      2078 |  260676   927480 |  184721    2073    24891    12.0 |  0.391 % |
c |      3217 |  260419   926501 |  202993    3209    42773    13.3 |  0.458 % |
c |      4925 |  260419   926501 |  223292    4917   283057    57.6 |  0.458 % |
c |      7487 |  260141   925429 |  245359    7472   328667    44.0 |  0.544 % |
c |     11331 |  259969   924696 |  269717   11314   499456    44.1 |  0.600 % |
c |     17097 |  259567   922609 |  296229   17070  1762575   103.3 |  0.735 % |
c |     25746 |  259543   922385 |  325822   25718  2527451    98.3 |  0.755 % |
c |     38720 |  259506   921624 |  358354   38689  7463322   192.9 |  0.773 % |
c |     58181 |  259506   921624 |  394189   58150  8653986   148.8 |  0.773 % |
c |     87373 |  259354   920007 |  433354   87340 17186182   196.8 |  0.793 % |
c |    131162 |  259305   919772 |  476599  131125 30044658   229.1 |  0.816 % |
c ==============================================================================
c (current CPU-time: 999.037 s)
c ==============================================================================
c [1mFound solution: 7115[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:113802     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    190118 |  526040  1542892 |  157811  190081 45016200   236.8 |  0.816 % |
c   -- subsuming                       
c   -- var.elim.:  1000/113128          
c   -- var.elim.:  2000/113128          
c   -- var.elim.:  3000/113128          
c   -- var.elim.:  4000/113128          
c   -- var.elim.:  5000/113128          
c   -- var.elim.:  6000/113128          
c   -- var.elim.:  7000/113128          
c   -- var.elim.:  8000/113128          
c   -- var.elim.:  9000/113128          
c   -- var.elim.:  10000/113128          
c   -- var.elim.:  11000/113128          
c   -- var.elim.:  12000/113128          
c   -- var.elim.:  13000/113128          
c   -- var.elim.:  14000/113128          
c   -- var.elim.:  15000/113128          
c   -- var.elim.:  16000/113128          
c   -- var.elim.:  17000/113128          
c   -- var.elim.:  18000/113128          
c   -- var.elim.:  19000/113128          
c   -- var.elim.:  20000/113128          
c   -- var.elim.:  21000/113128          
c   -- var.elim.:  22000/113128          
c   -- var.elim.:  23000/113128          
c   -- var.elim.:  24000/113128          
c   -- var.elim.:  25000/113128          
c   -- var.elim.:  26000/113128          
c   -- var.elim.:  27000/113128          
c   -- var.elim.:  28000/113128          
c   -- var.elim.:  29000/113128          
c   -- var.elim.:  30000/113128          
c   -- var.elim.:  31000/113128          
c   -- var.elim.:  32000/113128          
c   -- var.elim.:  33000/113128          
c   -- var.elim.:  34000/113128          
c   -- var.elim.:  35000/113128          
c   -- var.elim.:  36000/113128          
c   -- var.elim.:  37000/113128          
c   -- var.elim.:  38000/113128          
c   -- var.elim.:  39000/113128          
c   -- var.elim.:  40000/113128          
c   -- var.elim.:  41000/113128          
c   -- var.elim.:  42000/113128          
c   -- var.elim.:  43000/113128          
c   -- var.elim.:  44000/113128          
c   -- var.elim.:  45000/113128          
c   -- var.elim.:  46000/113128          
c   -- var.elim.:  47000/113128          
c   -- var.elim.:  48000/113128          
c   -- var.elim.:  49000/113128          
c   -- var.elim.:  50000/113128          
c   -- var.elim.:  51000/113128          
c   -- var.elim.:  52000/113128          
c   -- var.elim.:  53000/113128          
c   -- var.elim.:  54000/113128          
c   -- var.elim.:  55000/113128          
c   -- var.elim.:  56000/113128          
c   -- var.elim.:  57000/113128          
c   -- var.elim.:  58000/113128          
c   -- var.elim.:  59000/113128          
c   -- var.elim.:  60000/113128          
c   -- var.elim.:  61000/113128          
c   -- var.elim.:  62000/113128          
c   -- var.elim.:  63000/113128          
c   -- var.elim.:  64000/113128          
c   -- var.elim.:  65000/113128          
c   -- var.elim.:  66000/113128          
c   -- var.elim.:  67000/113128          
c   -- var.elim.:  68000/113128          
c   -- var.elim.:  69000/113128          
c   -- var.elim.:  70000/113128          
c   -- var.elim.:  71000/113128          
c   -- var.elim.:  72000/113128          
c   -- var.elim.:  73000/113128          
c   -- var.elim.:  74000/113128          
c   -- var.elim.:  75000/113128          
c   -- var.elim.:  76000/113128          
c   -- var.elim.:  77000/113128          
c   -- var.elim.:  78000/113128          
c   -- var.elim.:  79000/113128          
c   -- var.elim.:  80000/113128          
c   -- var.elim.:  81000/113128          
c   -- var.elim.:  82000/113128          
c   -- var.elim.:  83000/113128          
c   -- var.elim.:  84000/113128          
c   -- var.elim.:  85000/113128          
c   -- var.elim.:  86000/113128          
c   -- var.elim.:  87000/113128          
c   -- var.elim.:  88000/113128          
c   -- var.elim.:  89000/113128          
c   -- var.elim.:  90000/113128          
c   -- var.elim.:  91000/113128          
c   -- var.elim.:  92000/113128          
c   -- var.elim.:  93000/113128          
c   -- var.elim.:  94000/113128          
c   -- var.elim.:  95000/113128          
c   -- var.elim.:  96000/113128          
c   -- var.elim.:  97000/113128          
c   -- var.elim.:  98000/113128          
c   -- var.elim.:  99000/113128          
c   -- var.elim.:  100000/113128          
c   -- var.elim.:  101000/113128          
c   -- var.elim.:  102000/113128          
c   -- var.elim.:  103000/113128          
c   -- var.elim.:  104000/113128          
c   -- var.elim.:  105000/113128          
c   -- var.elim.:  106000/113128          
c   -- var.elim.:  107000/113128          
c   -- var.elim.:  108000/113128          
c   -- var.elim.:  109000/113128          
c   -- var.elim.:  110000/113128          
c   -- var.elim.:  111000/113128          
c   -- var.elim.:  112000/113128          
c   -- var.elim.:  113000/113128          
c   -- var.elim.:  113128/113128          
c   -- var.elim.:  1000/59060          
c   -- var.elim.:  2000/59060          
c   -- var.elim.:  3000/59060          
c   -- var.elim.:  4000/59060          
c   -- var.elim.:  5000/59060          
c   -- var.elim.:  6000/59060          
c   -- var.elim.:  7000/59060          
c   -- var.elim.:  8000/59060          
c   -- var.elim.:  9000/59060          
c   -- var.elim.:  10000/59060          
c   -- var.elim.:  11000/59060          
c   -- var.elim.:  12000/59060          
c   -- var.elim.:  13000/59060          
c   -- var.elim.:  14000/59060          
c   -- var.elim.:  15000/59060          
c   -- var.elim.:  16000/59060          
c   -- var.elim.:  17000/59060          
c   -- var.elim.:  18000/59060          
c   -- var.elim.:  19000/59060          
c   -- var.elim.:  20000/59060          
c   -- var.elim.:  21000/59060          
c   -- var.elim.:  22000/59060          
c   -- var.elim.:  23000/59060          
c   -- var.elim.:  24000/59060          
c   -- var.elim.:  25000/59060          
c   -- var.elim.:  26000/59060          
c   -- var.elim.:  27000/59060          
c   -- var.elim.:  28000/59060          
c   -- var.elim.:  29000/59060          
c   -- var.elim.:  30000/59060          
c   -- var.elim.:  31000/59060          
c   -- var.elim.:  32000/59060          
c   -- var.elim.:  33000/59060          
c   -- var.elim.:  34000/59060          
c   -- var.elim.:  35000/59060          
c   -- var.elim.:  36000/59060          
c   -- var.elim.:  37000/59060          
c   -- var.elim.:  38000/59060          
c   -- var.elim.:  39000/59060          
c   -- var.elim.:  40000/59060          
c   -- var.elim.:  41000/59060          
c   -- var.elim.:  42000/59060          
c   -- var.elim.:  43000/59060          
c   -- var.elim.:  44000/59060          
c   -- var.elim.:  45000/59060          
c   -- var.elim.:  46000/59060          
c   -- var.elim.:  47000/59060          
c   -- var.elim.:  48000/59060          
c   -- var.elim.:  49000/59060          
c   -- var.elim.:  50000/59060          
c   -- var.elim.:  51000/59060          
c   -- var.elim.:  52000/59060          
c   -- var.elim.:  53000/59060          
c   -- var.elim.:  54000/59060          
c   -- var.elim.:  55000/59060          
c   -- var.elim.:  56000/59060          
c   -- var.elim.:  57000/59060          
c   -- var.elim.:  58000/59060          
c   -- var.elim.:  59000/59060          
c   -- var.elim.:  59060/59060          
c   -- var.elim.:  828/828          
c   -- var.elim.:  795/795          
c   -- subsuming                       
c   -- var.elim.:  1000/16245          
c   -- var.elim.:  2000/16245          
c   -- var.elim.:  3000/16245          
c   -- var.elim.:  4000/16245          
c   -- var.elim.:  5000/16245          
c   -- var.elim.:  6000/16245          
c   -- var.elim.:  7000/16245          
c   -- var.elim.:  8000/16245          
c   -- var.elim.:  9000/16245          
c   -- var.elim.:  10000/16245          
c   -- var.elim.:  11000/16245          
c   -- var.elim.:  12000/16245          
c   -- var.elim.:  13000/16245          
c   -- var.elim.:  14000/16245          
c   -- var.elim.:  15000/16245          
c   -- var.elim.:  16000/16245          
c   -- var.elim.:  16245/16245          
c   -- var.elim.:  1000/1470          
c   -- var.elim.:  1470/1470          
c   -- subsuming                       
c   -- var.elim.:  537/537          
c   -- var.elim.:  769/769          
c |    190118 |  493231  1767722 |      --  190081       --      -- |     --   | -32777/224908
c |    190118 |  493231  1767722 |  197292  155283 12784591    82.3 |  0.816 % |
c |    190219 |  493231  1767722 |  217021  155384 12786644    82.3 |  0.446 % |
c |    190369 |  493231  1767722 |  238723  155534 12787793    82.2 |  0.446 % |
c |    190594 |  493042  1767082 |  262495  155758 12790751    82.1 |  0.467 % |
c |    190931 |  493042  1767082 |  288745  156095 12794915    82.0 |  0.467 % |
c |    191437 |  493042  1767082 |  317619  156601 12808051    81.8 |  0.467 % |
c |    192197 |  493042  1767082 |  349381  157361 12825714    81.5 |  0.467 % |
c |    193336 |  492763  1765847 |  384102  158498 12847118    81.1 |  0.507 % |
c |    195045 |  492763  1765847 |  422512  160207 12875831    80.4 |  0.507 % |
c |    197607 |  492763  1765847 |  464763  162769 12912996    79.3 |  0.507 % |
c |    201453 |  492763  1765847 |  511240  166615 13101379    78.6 |  0.507 % |
c |    207221 |  492761  1765826 |  562361  172380 14046083    81.5 |  0.508 % |
c |    215870 |  492761  1765826 |  618598  181029 14431419    79.7 |  0.508 % |
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 -#### 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.84 0.94 0.90 2/54 28559
Raw data (stat): 28559 (runsolver) R 28558 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480313806 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17269 0 0 0 948 49 0 0 25 0 1 0 480313806 73367552 16319 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17912 16319 603 41 0 17871 0
vsize: 71648
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17455 0 0 0 1932 65 0 0 25 0 1 0 480313806 73830400 16393 4294967295 134512640 134672761 3221224576 3221222880 1074972061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18025 16393 603 41 0 17984 0
vsize: 72100
[startup+30.0023 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17455 0 0 0 2932 65 0 0 25 0 1 0 480313806 73043968 16221 4294967295 134512640 134672761 3221224576 3221222976 134604097 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17833 16221 603 41 0 17792 0
vsize: 71332
[startup+40.0029 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17455 0 0 0 3932 65 0 0 25 0 1 0 480313806 73043968 16221 4294967295 134512640 134672761 3221224576 3221223120 134621194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17833 16221 603 41 0 17792 0
vsize: 71332
[startup+50.0041 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17774 0 0 0 4931 66 0 0 25 0 1 0 480313806 73043968 16251 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17833 16251 603 41 0 17792 0
vsize: 71332
[startup+60.0043 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18457 0 0 0 5929 68 0 0 25 0 1 0 480313806 73306112 16295 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17897 16295 603 41 0 17856 0
vsize: 71588
[startup+70.0048 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18677 0 0 0 6928 69 0 0 25 0 1 0 480313806 74240000 16515 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18125 16515 603 41 0 18084 0
vsize: 72500
[startup+80.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18807 0 0 0 7927 70 0 0 25 0 1 0 480313806 74813440 16645 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18265 16645 603 41 0 18224 0
vsize: 73060
[startup+90.0059 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18927 0 0 0 8927 70 0 0 25 0 1 0 480313806 75198464 16765 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18359 16765 603 41 0 18318 0
vsize: 73436
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 19278 0 0 0 9926 72 0 0 25 0 1 0 480313806 76640256 17116 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18711 17116 603 41 0 18670 0
vsize: 74844
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20110 0 0 0 10924 74 0 0 25 0 1 0 480313806 80203776 17948 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19581 17948 603 41 0 19540 0
vsize: 78324
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20279 0 0 0 11923 74 0 0 25 0 1 0 480313806 80863232 18117 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19742 18117 603 41 0 19701 0
vsize: 78968
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20504 0 0 0 12923 75 0 0 25 0 1 0 480313806 81780736 18342 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19966 18342 603 41 0 19925 0
vsize: 79864
[startup+140.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20700 0 0 0 13923 75 0 0 25 0 1 0 480313806 82567168 18538 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20158 18538 603 41 0 20117 0
vsize: 80632
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20761 0 0 0 14923 75 0 0 25 0 1 0 480313806 82833408 18599 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20223 18599 603 41 0 20182 0
vsize: 80892
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20858 0 0 0 15923 76 0 0 25 0 1 0 480313806 83234816 18696 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20321 18696 603 41 0 20280 0
vsize: 81284
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20998 0 0 0 16922 76 0 0 25 0 1 0 480313806 83755008 18836 4294967295 134512640 134672761 3221224576 3221223752 134615853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20448 18836 603 41 0 20407 0
vsize: 81792
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 21217 0 0 0 17922 77 0 0 25 0 1 0 480313806 84680704 19055 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20674 19055 603 41 0 20633 0
vsize: 82696
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 21673 0 0 0 18921 78 0 0 25 0 1 0 480313806 86663168 19511 4294967295 134512640 134672761 3221224576 3221223616 134614223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21156 19511 603 41 0 21115 0
vsize: 84632
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 23003 0 0 0 19918 81 0 0 25 0 1 0 480313806 92098560 20841 4294967295 134512640 134672761 3221224576 3221223680 134603709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22485 20841 603 41 0 22444 0
vsize: 89940
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 24166 0 0 0 20917 83 0 0 25 0 1 0 480313806 96800768 22004 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23633 22004 603 41 0 23592 0
vsize: 94532
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 25476 0 0 0 21915 85 0 0 25 0 1 0 480313806 102187008 23314 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24948 23314 603 41 0 24907 0
vsize: 99792
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 25922 0 0 0 22914 86 0 0 25 0 1 0 480313806 103940096 23760 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25376 23760 603 41 0 25335 0
vsize: 101504
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26017 0 0 0 23914 86 0 0 25 0 1 0 480313806 104337408 23855 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25473 23855 603 41 0 25432 0
vsize: 101892
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26290 0 0 0 24913 87 0 0 25 0 1 0 480313806 105508864 24128 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25759 24128 603 41 0 25718 0
vsize: 103036
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26644 0 0 0 25913 87 0 0 25 0 1 0 480313806 106946560 24482 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26110 24482 603 41 0 26069 0
vsize: 104440
[startup+270.013 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26841 0 0 0 26913 88 0 0 25 0 1 0 480313806 107737088 24679 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26303 24679 603 41 0 26262 0
vsize: 105212
[startup+280.013 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 27130 0 0 0 27911 89 0 0 25 0 1 0 480313806 108802048 24968 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26563 24968 603 41 0 26522 0
vsize: 106252
[startup+290.015 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 27322 0 0 0 28911 90 0 0 25 0 1 0 480313806 109596672 25160 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26757 25160 603 41 0 26716 0
vsize: 107028
[startup+300.015 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 27974 0 0 0 29910 92 0 0 25 0 1 0 480313806 112238592 25812 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27402 25812 603 41 0 27361 0
vsize: 109608
[startup+310.015 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 28562 0 0 0 30909 93 0 0 25 0 1 0 480313806 114749440 26400 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28015 26400 603 41 0 27974 0
vsize: 112060
[startup+320.015 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 29064 0 0 0 31907 94 0 0 25 0 1 0 480313806 116695040 26902 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28490 26902 603 41 0 28449 0
vsize: 113960
[startup+330.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 29709 0 0 0 32905 97 0 0 25 0 1 0 480313806 119619584 27547 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29204 27547 603 41 0 29163 0
vsize: 116816
[startup+340.016 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 30642 0 0 0 33903 99 0 0 25 0 1 0 480313806 123420672 28480 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30132 28481 603 41 0 30091 0
vsize: 120528
[startup+350.016 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 31445 0 0 0 34901 102 0 0 25 0 1 0 480313806 126701568 29283 4294967295 134512640 134672761 3221224576 3221223568 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30933 29283 603 41 0 30892 0
vsize: 123732
[startup+360.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 32858 0 0 0 35899 104 0 0 25 0 1 0 480313806 132571136 30696 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32366 30696 603 41 0 32325 0
vsize: 129464
[startup+370.017 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 34066 0 0 0 36896 106 0 0 25 0 1 0 480313806 137396224 31904 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33544 31904 603 41 0 33503 0
vsize: 134176
[startup+380.017 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 34660 0 0 0 37894 108 0 0 25 0 1 0 480313806 139882496 32498 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34151 32498 603 41 0 34110 0
vsize: 136604
[startup+390.018 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 35426 0 0 0 38893 110 0 0 25 0 1 0 480313806 143052800 33264 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34925 33264 603 41 0 34884 0
vsize: 139700
[startup+400.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 35663 0 0 0 39893 111 0 0 25 0 1 0 480313806 143970304 33501 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35149 33501 603 41 0 35108 0
vsize: 140596
[startup+410.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 35786 0 0 0 40892 111 0 0 25 0 1 0 480313806 144498688 33624 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35278 33624 603 41 0 35237 0
vsize: 141112
[startup+420.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36104 0 0 0 41892 112 0 0 25 0 1 0 480313806 145805312 33942 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35597 33942 603 41 0 35556 0
vsize: 142388
[startup+430.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36235 0 0 0 42892 112 0 0 25 0 1 0 480313806 146337792 34073 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35727 34073 603 41 0 35686 0
vsize: 142908
[startup+440.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36391 0 0 0 43891 113 0 0 25 0 1 0 480313806 146866176 34229 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35856 34229 603 41 0 35815 0
vsize: 143424
[startup+450.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36605 0 0 0 44891 113 0 0 25 0 1 0 480313806 147787776 34443 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36081 34443 603 41 0 36040 0
vsize: 144324
[startup+460.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36827 0 0 0 45891 113 0 0 25 0 1 0 480313806 148713472 34665 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36307 34665 603 41 0 36266 0
vsize: 145228
[startup+470.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37082 0 0 0 46891 114 0 0 25 0 1 0 480313806 149762048 34920 4294967295 134512640 134672761 3221224576 3221223712 134614656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36563 34920 603 41 0 36522 0
vsize: 146252
[startup+480.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37172 0 0 0 47891 114 0 0 25 0 1 0 480313806 150016000 35010 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36625 35010 603 41 0 36584 0
vsize: 146500
[startup+490.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37330 0 0 0 48891 115 0 0 25 0 1 0 480313806 150663168 35168 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36783 35168 603 41 0 36742 0
vsize: 147132
[startup+500.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37540 0 0 0 49890 116 0 0 25 0 1 0 480313806 151576576 35378 4294967295 134512640 134672761 3221224576 3221223712 134614814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37006 35378 603 41 0 36965 0
vsize: 148024
[startup+510.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37765 0 0 0 50889 117 0 0 25 0 1 0 480313806 152481792 35603 4294967295 134512640 134672761 3221224576 3221223616 134612739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37227 35603 603 41 0 37186 0
vsize: 148908
[startup+520.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 38107 0 0 0 51889 118 0 0 25 0 1 0 480313806 153927680 35945 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37580 35945 603 41 0 37539 0
vsize: 150320
[startup+530.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 38351 0 0 0 52888 118 0 0 25 0 1 0 480313806 154943488 36189 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37828 36189 603 41 0 37787 0
vsize: 151312
[startup+540.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 39055 0 0 0 53887 120 0 0 25 0 1 0 480313806 157700096 36893 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38501 36893 603 41 0 38460 0
vsize: 154004
[startup+550.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 39974 0 0 0 54883 123 0 0 25 0 1 0 480313806 161452032 37812 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39417 37812 603 41 0 39376 0
vsize: 157668
[startup+560.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 41048 0 0 0 55881 126 0 0 25 0 1 0 480313806 165941248 38886 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40513 38886 603 41 0 40472 0
vsize: 162052
[startup+570.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 42196 0 0 0 56878 129 0 0 25 0 1 0 480313806 170541056 40034 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41636 40034 603 41 0 41595 0
vsize: 166544
[startup+580.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 43145 0 0 0 57877 131 0 0 25 0 1 0 480313806 174489600 40983 4294967295 134512640 134672761 3221224576 3221223616 134614243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42600 40983 603 41 0 42559 0
vsize: 170400
[startup+590.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 43504 0 0 0 58876 132 0 0 25 0 1 0 480313806 175939584 41342 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42954 41342 603 41 0 42913 0
vsize: 171816
[startup+600.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 44243 0 0 0 59874 134 0 0 25 0 1 0 480313806 178954240 42081 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43690 42081 603 41 0 43649 0
vsize: 174760
[startup+610.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 45245 0 0 0 60872 136 0 0 25 0 1 0 480313806 183115776 43083 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44706 43083 603 41 0 44665 0
vsize: 178824
[startup+620.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 45879 0 0 0 61871 137 0 0 25 0 1 0 480313806 185630720 43717 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45320 43717 603 41 0 45279 0
vsize: 181280
[startup+630.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 46278 0 0 0 62870 138 0 0 25 0 1 0 480313806 187326464 44116 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45734 44116 603 41 0 45693 0
vsize: 182936
[startup+640.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 46628 0 0 0 63870 139 0 0 25 0 1 0 480313806 188751872 44466 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46082 44466 603 41 0 46041 0
vsize: 184328
[startup+650.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 47422 0 0 0 64868 141 0 0 25 0 1 0 480313806 191950848 45260 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46863 45260 603 41 0 46822 0
vsize: 187452
[startup+660.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 47974 0 0 0 65867 142 0 0 25 0 1 0 480313806 194191360 45812 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47410 45812 603 41 0 47369 0
vsize: 189640
[startup+670.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 48337 0 0 0 66866 144 0 0 25 0 1 0 480313806 195788800 46175 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47800 46175 603 41 0 47759 0
vsize: 191200
[startup+680.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 48648 0 0 0 67865 145 0 0 25 0 1 0 480313806 196988928 46486 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48093 46486 603 41 0 48052 0
vsize: 192372
[startup+690.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49059 0 0 0 68864 146 0 0 25 0 1 0 480313806 199229440 46897 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48640 46897 603 41 0 48599 0
vsize: 194560
[startup+700.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49302 0 0 0 69864 146 0 0 25 0 1 0 480313806 200146944 47140 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48864 47140 603 41 0 48823 0
vsize: 195456
[startup+710.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49451 0 0 0 70864 146 0 0 25 0 1 0 480313806 200806400 47289 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49025 47289 603 41 0 48984 0
vsize: 196100
[startup+720.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49634 0 0 0 71863 147 0 0 25 0 1 0 480313806 201596928 47472 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49218 47472 603 41 0 49177 0
vsize: 196872
[startup+730.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49918 0 0 0 72863 148 0 0 25 0 1 0 480313806 202645504 47756 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49474 47756 603 41 0 49433 0
vsize: 197896
[startup+740.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 50329 0 0 0 73861 149 0 0 25 0 1 0 480313806 204333056 48167 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49886 48167 603 41 0 49845 0
vsize: 199544
[startup+750.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 50454 0 0 0 74861 150 0 0 25 0 1 0 480313806 204853248 48292 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50013 48292 603 41 0 49972 0
vsize: 200052
[startup+760.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 50774 0 0 0 75860 151 0 0 25 0 1 0 480313806 206176256 48612 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50336 48612 603 41 0 50295 0
vsize: 201344
[startup+770.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51065 0 0 0 76860 152 0 0 25 0 1 0 480313806 207351808 48903 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50623 48903 603 41 0 50582 0
vsize: 202492
[startup+780.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51455 0 0 0 77858 153 0 0 25 0 1 0 480313806 208924672 49293 4294967295 134512640 134672761 3221224576 3221223776 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51007 49293 603 41 0 50966 0
vsize: 204028
[startup+790.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51701 0 0 0 78858 154 0 0 25 0 1 0 480313806 209985536 49539 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51266 49539 603 41 0 51225 0
vsize: 205064
[startup+800.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51987 0 0 0 79858 154 0 0 25 0 1 0 480313806 211169280 49825 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51555 49825 603 41 0 51514 0
vsize: 206220
[startup+810.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 52355 0 0 0 80857 155 0 0 25 0 1 0 480313806 212672512 50193 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51922 50193 603 41 0 51881 0
vsize: 207688
[startup+820.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 52590 0 0 0 81857 156 0 0 25 0 1 0 480313806 213528576 50428 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52131 50428 603 41 0 52090 0
vsize: 208524
[startup+830.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 52783 0 0 0 82856 156 0 0 25 0 1 0 480313806 214310912 50621 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52322 50621 603 41 0 52281 0
vsize: 209288
[startup+840.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53160 0 0 0 83856 157 0 0 25 0 1 0 480313806 215859200 50998 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52700 50998 603 41 0 52659 0
vsize: 210800
[startup+850.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53397 0 0 0 84855 158 0 0 25 0 1 0 480313806 216899584 51235 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52954 51235 603 41 0 52913 0
vsize: 211816
[startup+860.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53508 0 0 0 85855 158 0 0 25 0 1 0 480313806 217305088 51346 4294967295 134512640 134672761 3221224576 3221223776 134610528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53053 51346 603 41 0 53012 0
vsize: 212212
[startup+870.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53950 0 0 0 86854 159 0 0 25 0 1 0 480313806 219017216 51788 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53471 51788 603 41 0 53430 0
vsize: 213884
[startup+880.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 54157 0 0 0 87854 160 0 0 25 0 1 0 480313806 219938816 51995 4294967295 134512640 134672761 3221224576 3221223568 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53696 51995 603 41 0 53655 0
vsize: 214784
[startup+890.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 54606 0 0 0 88853 161 0 0 25 0 1 0 480313806 221798400 52444 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54150 52444 603 41 0 54109 0
vsize: 216600
[startup+900.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 54997 0 0 0 89852 162 0 0 25 0 1 0 480313806 223375360 52835 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54535 52835 603 41 0 54494 0
vsize: 218140
[startup+910.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 55340 0 0 0 90851 163 0 0 25 0 1 0 480313806 224776192 53178 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54877 53178 603 41 0 54836 0
vsize: 219508
[startup+920.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 55708 0 0 0 91850 165 0 0 25 0 1 0 480313806 226197504 53546 4294967295 134512640 134672761 3221224576 3221223760 134615541 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55224 53546 603 41 0 55183 0
vsize: 220896
[startup+930.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 56574 0 0 0 92848 167 0 0 25 0 1 0 480313806 229834752 54412 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56112 54412 603 41 0 56071 0
vsize: 224448
[startup+940.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 57525 0 0 0 93846 169 0 0 25 0 1 0 480313806 233680896 55363 4294967295 134512640 134672761 3221224576 3221223760 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57051 55363 603 41 0 57010 0
vsize: 228204
[startup+950.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 59113 0 0 0 94843 172 0 0 25 0 1 0 480313806 240189440 56951 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58640 56951 603 41 0 58599 0
vsize: 234560
[startup+960.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 60403 0 0 0 95840 175 0 0 25 0 1 0 480313806 245456896 58241 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59926 58241 603 41 0 59885 0
vsize: 239704
[startup+970.054 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 61382 0 0 0 96839 177 0 0 25 0 1 0 480313806 249466880 59220 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60905 59220 603 41 0 60864 0
vsize: 243620
[startup+980.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 62293 0 0 0 97837 178 0 0 25 0 1 0 480313806 253145088 60131 4294967295 134512640 134672761 3221224576 3221223712 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61803 60131 603 41 0 61762 0
vsize: 247212
[startup+990.056 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 63422 0 0 0 98835 181 0 0 25 0 1 0 480313806 257855488 61260 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62953 61260 603 41 0 62912 0
vsize: 251812
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 64337 0 0 0 99833 183 0 0 25 0 1 0 480313806 261591040 62175 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63865 62175 603 41 0 63824 0
vsize: 255460
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 81495 0 0 0 100788 228 0 0 25 0 1 0 480313806 321347584 75282 4294967295 134512640 134672761 3221224576 3221223120 134621238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78454 75282 603 41 0 78413 0
vsize: 313816
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 82587 0 0 0 101781 235 0 0 25 0 1 0 480313806 323121152 75700 4294967295 134512640 134672761 3221224576 3221222784 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78887 75700 603 41 0 78846 0
vsize: 315548
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 82699 0 0 0 102736 253 0 0 25 0 1 0 480313806 323149824 75701 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78894 75701 603 41 0 78853 0
vsize: 315576
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 82699 0 0 0 103737 253 0 0 25 0 1 0 480313806 322887680 75643 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78830 75643 603 41 0 78789 0
vsize: 315320
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 84198 0 0 0 104734 256 0 0 25 0 1 0 480313806 330534912 76935 4294967295 134512640 134672761 3221224576 3221223100 1075346542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80697 76935 603 41 0 80656 0
vsize: 322788
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 84215 0 0 0 105733 257 0 0 25 0 1 0 480313806 322502656 75548 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78736 75548 603 41 0 78695 0
vsize: 314944
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 106730 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 107730 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 108730 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 109731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 110731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223720 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 111731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 112731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 113732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 114732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 115732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 116732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 117732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 118733 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 119733 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
[startup+1210.07 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28559
Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 120733 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78702 75538 603 41 0 78661 0
vsize: 314808
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.24 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 28559
Raw data (stat): 28559 (minisat+) Z 28558 23176 23175 0 -1 12 85355 0 0 0 120733 277 0 0 25 0 1 0 480313806 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.24
CPU time (s): 1210.11
CPU user time (s): 1207.34
CPU system time (s): 2.77458
CPU usage (%): 99.9894
Max. virtual memory (Kb): 322788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####