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/logic-synthesis/normalized-rot.b.opb
MD5SUM	c5ca4962151c0e84eeae44e16faee495
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	116
Optimality of the best value was proved	NO
Number of terms in the objective function	1452
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	1452
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1452
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04884
Number of variables	1451
Total number of constraints	2984
Number of constraints which are clauses	2932
Number of constraints which are cardinality constraints (but not clauses)	52
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 5425

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-13 23:53:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3832 boxname=wulflinc19 idbench=72 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c5ca4962151c0e84eeae44e16faee495  /oldhome/oroussel/tmp/wulflinc19/normalized-rot.b.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc19/normalized-rot.b.opb /oldhome/oroussel/tmp/wulflinc19/normalized-rot.b.opb
IDLAUNCH: 3832
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        889168 kB
Buffers:         34096 kB
Cached:          77640 kB
SwapCached:         56 kB
Active:          48076 kB
Inactive:        66640 kB
HighTotal:      131008 kB
HighFree:        49308 kB
LowTotal:       903652 kB
LowFree:        839860 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25192 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:13:26 (client local time) WITH STATUS 10 IN 1209.65 SECONDS
stats: 3832 7 1209.65 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2722 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 |    2553    38142 |     765       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  839/839          
c |         0 |    1476    20277 |      --       0       --      -- |     --   | -1077/-17865
c |         0 |    1476    20277 |     590       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.38894 s)
c ==============================================================================
c [1mFound solution: 160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:79826     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         4 |   95427   239408 |   28628       4      142    35.5 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/63138          
c   -- var.elim.:  2000/63138          
c   -- var.elim.:  3000/63138          
c   -- var.elim.:  4000/63138          
c   -- var.elim.:  5000/63138          
c   -- var.elim.:  6000/63138          
c   -- var.elim.:  7000/63138          
c   -- var.elim.:  8000/63138          
c   -- var.elim.:  9000/63138          
c   -- var.elim.:  10000/63138          
c   -- var.elim.:  11000/63138          
c   -- var.elim.:  12000/63138          
c   -- var.elim.:  13000/63138          
c   -- var.elim.:  14000/63138          
c   -- var.elim.:  15000/63138          
c   -- var.elim.:  16000/63138          
c   -- var.elim.:  17000/63138          
c   -- var.elim.:  18000/63138          
c   -- var.elim.:  19000/63138          
c   -- var.elim.:  20000/63138          
c   -- var.elim.:  21000/63138          
c   -- var.elim.:  22000/63138          
c   -- var.elim.:  23000/63138          
c   -- var.elim.:  24000/63138          
c   -- var.elim.:  25000/63138          
c   -- var.elim.:  26000/63138          
c   -- var.elim.:  27000/63138          
c   -- var.elim.:  28000/63138          
c   -- var.elim.:  29000/63138          
c   -- var.elim.:  30000/63138          
c   -- var.elim.:  31000/63138          
c   -- var.elim.:  32000/63138          
c   -- var.elim.:  33000/63138          
c   -- var.elim.:  34000/63138          
c   -- var.elim.:  35000/63138          
c   -- var.elim.:  36000/63138          
c   -- var.elim.:  37000/63138          
c   -- var.elim.:  38000/63138          
c   -- var.elim.:  39000/63138          
c   -- var.elim.:  40000/63138          
c   -- var.elim.:  41000/63138          
c   -- var.elim.:  42000/63138          
c   -- var.elim.:  43000/63138          
c   -- var.elim.:  44000/63138          
c   -- var.elim.:  45000/63138          
c   -- var.elim.:  46000/63138          
c   -- var.elim.:  47000/63138          
c   -- var.elim.:  48000/63138          
c   -- var.elim.:  49000/63138          
c   -- var.elim.:  50000/63138          
c   -- var.elim.:  51000/63138          
c   -- var.elim.:  52000/63138          
c   -- var.elim.:  53000/63138          
c   -- var.elim.:  54000/63138          
c   -- var.elim.:  55000/63138          
c   -- var.elim.:  56000/63138          
c   -- var.elim.:  57000/63138          
c   -- var.elim.:  58000/63138          
c   -- var.elim.:  59000/63138          
c   -- var.elim.:  60000/63138          
c   -- var.elim.:  61000/63138          
c   -- var.elim.:  62000/63138          
c   -- var.elim.:  63000/63138          
c   -- var.elim.:  63138/63138          
c   -- var.elim.:  1000/31406          
c   -- var.elim.:  2000/31406          
c   -- var.elim.:  3000/31406          
c   -- var.elim.:  4000/31406          
c   -- var.elim.:  5000/31406          
c   -- var.elim.:  6000/31406          
c   -- var.elim.:  7000/31406          
c   -- var.elim.:  8000/31406          
c   -- var.elim.:  9000/31406          
c   -- var.elim.:  10000/31406          
c   -- var.elim.:  11000/31406          
c   -- var.elim.:  12000/31406          
c   -- var.elim.:  13000/31406          
c   -- var.elim.:  14000/31406          
c   -- var.elim.:  15000/31406          
c   -- var.elim.:  16000/31406          
c   -- var.elim.:  17000/31406          
c   -- var.elim.:  18000/31406          
c   -- var.elim.:  19000/31406          
c   -- var.elim.:  20000/31406          
c   -- var.elim.:  21000/31406          
c   -- var.elim.:  22000/31406          
c   -- var.elim.:  23000/31406          
c   -- var.elim.:  24000/31406          
c   -- var.elim.:  25000/31406          
c   -- var.elim.:  26000/31406          
c   -- var.elim.:  27000/31406          
c   -- var.elim.:  28000/31406          
c   -- var.elim.:  29000/31406          
c   -- var.elim.:  30000/31406          
c   -- var.elim.:  31000/31406          
c   -- var.elim.:  31406/31406          
c   -- var.elim.:  1000/1699          
c   -- var.elim.:  1699/1699          
c   -- var.elim.:  967/967          
c   -- var.elim.:  1000/3168          
c   -- var.elim.:  2000/3168          
c   -- var.elim.:  3000/3168          
c   -- var.elim.:  3168/3168          
c   -- subsuming                       
c   -- var.elim.:  1000/27288          
c   -- var.elim.:  2000/27288          
c   -- var.elim.:  3000/27288          
c   -- var.elim.:  4000/27288          
c   -- var.elim.:  5000/27288          
c   -- var.elim.:  6000/27288          
c   -- var.elim.:  7000/27288          
c   -- var.elim.:  8000/27288          
c   -- var.elim.:  9000/27288          
c   -- var.elim.:  10000/27288          
c   -- var.elim.:  11000/27288          
c   -- var.elim.:  12000/27288          
c   -- var.elim.:  13000/27288          
c   -- var.elim.:  14000/27288          
c   -- var.elim.:  15000/27288          
c   -- var.elim.:  16000/27288          
c   -- var.elim.:  17000/27288          
c   -- var.elim.:  18000/27288          
c   -- var.elim.:  19000/27288          
c   -- var.elim.:  20000/27288          
c   -- var.elim.:  21000/27288          
c   -- var.elim.:  22000/27288          
c   -- var.elim.:  23000/27288          
c   -- var.elim.:  24000/27288          
c   -- var.elim.:  25000/27288          
c   -- var.elim.:  26000/27288          
c   -- var.elim.:  27000/27288          
c   -- var.elim.:  27288/27288          
c   -- var.elim.:  35/35          
c |         4 |   64054   511509 |      --       4       --      -- |     --   | -31264/272412
c |         4 |   64054   511509 |   25621       4      142    35.5 |  0.000 % |
c |       105 |   63564   506847 |   27968      91     3121    34.3 |  1.120 % |
c |       256 |   63420   505541 |   30695     233     7188    30.8 |  1.314 % |
c |       481 |   63420   505541 |   33764     458    32382    70.7 |  1.314 % |
c |       818 |   63257   503912 |   37045     787    51431    65.4 |  1.530 % |
c |      1327 |   63128   502662 |   40667    1287   104672    81.3 |  1.699 % |
c |      2086 |   63077   502206 |   44697    2041   183947    90.1 |  1.762 % |
c |      3228 |   63077   502206 |   49167    3183   333166   104.7 |  1.762 % |
c |      4936 |   63077   502206 |   54084    4891   641746   131.2 |  1.762 % |
c |      7498 |   63028   501625 |   59446    7442   881549   118.5 |  1.832 % |
c |     11342 |   62994   501363 |   65356   11284  1412497   125.2 |  1.871 % |
c ==============================================================================
c (current CPU-time: 180.221 s)
c ==============================================================================
c [1mFound solution: 140[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 |     12038 |   67380   514126 |   20213   11980  1500451   125.2 |  1.871 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24614          
c   -- var.elim.:  2000/24614          
c   -- var.elim.:  3000/24614          
c   -- var.elim.:  4000/24614          
c   -- var.elim.:  5000/24614          
c   -- var.elim.:  6000/24614          
c   -- var.elim.:  7000/24614          
c   -- var.elim.:  8000/24614          
c   -- var.elim.:  9000/24614          
c   -- var.elim.:  10000/24614          
c   -- var.elim.:  11000/24614          
c   -- var.elim.:  12000/24614          
c   -- var.elim.:  13000/24614          
c   -- var.elim.:  14000/24614          
c   -- var.elim.:  15000/24614          
c   -- var.elim.:  16000/24614          
c   -- var.elim.:  17000/24614          
c   -- var.elim.:  18000/24614          
c   -- var.elim.:  19000/24614          
c   -- var.elim.:  20000/24614          
c   -- var.elim.:  21000/24614          
c   -- var.elim.:  22000/24614          
c   -- var.elim.:  23000/24614          
c   -- var.elim.:  24000/24614          
c   -- var.elim.:  24614/24614          
c   -- var.elim.:  1000/15435          
c   -- var.elim.:  2000/15435          
c   -- var.elim.:  3000/15435          
c   -- var.elim.:  4000/15435          
c   -- var.elim.:  5000/15435          
c   -- var.elim.:  6000/15435          
c   -- var.elim.:  7000/15435          
c   -- var.elim.:  8000/15435          
c   -- var.elim.:  9000/15435          
c   -- var.elim.:  10000/15435          
c   -- var.elim.:  11000/15435          
c   -- var.elim.:  12000/15435          
c   -- var.elim.:  13000/15435          
c   -- var.elim.:  14000/15435          
c   -- var.elim.:  15000/15435          
c   -- var.elim.:  15435/15435          
c   -- var.elim.:  1000/14065          
c   -- var.elim.:  2000/14065          
c   -- var.elim.:  3000/14065          
c   -- var.elim.:  4000/14065          
c   -- var.elim.:  5000/14065          
c   -- var.elim.:  6000/14065          
c   -- var.elim.:  7000/14065          
c   -- var.elim.:  8000/14065          
c   -- var.elim.:  9000/14065          
c   -- var.elim.:  10000/14065          
c   -- var.elim.:  11000/14065          
c   -- var.elim.:  12000/14065          
c   -- var.elim.:  13000/14065          
c   -- var.elim.:  14000/14065          
c   -- var.elim.:  14065/14065          
c   -- var.elim.:  1000/8138          
c   -- var.elim.:  2000/8138          
c   -- var.elim.:  3000/8138          
c   -- var.elim.:  4000/8138          
c   -- var.elim.:  5000/8138          
c   -- var.elim.:  6000/8138          
c   -- var.elim.:  7000/8138          
c   -- var.elim.:  8000/8138          
c   -- var.elim.:  8138/8138          
c   -- var.elim.:  809/809          
c   -- var.elim.:  432/432          
c   -- subsuming                       
c   -- var.elim.:  1000/8070          
c   -- var.elim.:  2000/8070          
c   -- var.elim.:  3000/8070          
c   -- var.elim.:  4000/8070          
c   -- var.elim.:  5000/8070          
c   -- var.elim.:  6000/8070          
c   -- var.elim.:  7000/8070          
c   -- var.elim.:  8000/8070          
c   -- var.elim.:  8070/8070          
c |     12038 |   59804   455198 |      --   11980       --      -- |     --   | -6118/-2497
c |     12038 |   59804   455198 |   23921   10495  1171188   111.6 |  1.871 % |
c |     12138 |   59804   455198 |   26313   10595  1176226   111.0 |  2.817 % |
c |     12288 |   59804   455198 |   28945   10745  1187843   110.5 |  2.817 % |
c |     12514 |   59779   455035 |   31826   10966  1199863   109.4 |  2.850 % |
c |     12852 |   59779   455035 |   35008   11304  1217419   107.7 |  2.850 % |
c |     13364 |   59779   455035 |   38509   11816  1243436   105.2 |  2.850 % |
c |     14123 |   59779   455035 |   42360   12575  1283787   102.1 |  2.850 % |
c |     15263 |   59739   454715 |   46565   13709  1408725   102.8 |  2.904 % |
c |     16971 |   59739   454715 |   51222   15417  1565526   101.5 |  2.904 % |
c |     19534 |   59739   454715 |   56344   17980  1815483   101.0 |  2.904 % |
c |     23378 |   59739   454715 |   61979   21824  2367487   108.5 |  2.904 % |
c |     29146 |   59739   454715 |   68176   27592  3784175   137.1 |  2.904 % |
c |     37797 |   59686   454168 |   74928   36240  5359587   147.9 |  2.941 % |
c |     50771 |   59624   453685 |   82335   49204  7787583   158.3 |  3.014 % |
c |     70232 |   59624   453685 |   90568   68665 11897648   173.3 |  3.014 % |
c ==============================================================================
c (current CPU-time: 419.232 s)
c ==============================================================================
c [1mFound solution: 133[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:31458     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     75208 |  106359   572783 |   31907   73641 12855228   174.6 |  3.014 % |
c   -- subsuming                       
c   -- var.elim.:  1000/52820          
c   -- var.elim.:  2000/52820          
c   -- var.elim.:  3000/52820          
c   -- var.elim.:  4000/52820          
c   -- var.elim.:  5000/52820          
c   -- var.elim.:  6000/52820          
c   -- var.elim.:  7000/52820          
c   -- var.elim.:  8000/52820          
c   -- var.elim.:  9000/52820          
c   -- var.elim.:  10000/52820          
c   -- var.elim.:  11000/52820          
c   -- var.elim.:  12000/52820          
c   -- var.elim.:  13000/52820          
c   -- var.elim.:  14000/52820          
c   -- var.elim.:  15000/52820          
c   -- var.elim.:  16000/52820          
c   -- var.elim.:  17000/52820          
c   -- var.elim.:  18000/52820          
c   -- var.elim.:  19000/52820          
c   -- var.elim.:  20000/52820          
c   -- var.elim.:  21000/52820          
c   -- var.elim.:  22000/52820          
c   -- var.elim.:  23000/52820          
c   -- var.elim.:  24000/52820          
c   -- var.elim.:  25000/52820          
c   -- var.elim.:  26000/52820          
c   -- var.elim.:  27000/52820          
c   -- var.elim.:  28000/52820          
c   -- var.elim.:  29000/52820          
c   -- var.elim.:  30000/52820          
c   -- var.elim.:  31000/52820          
c   -- var.elim.:  32000/52820          
c   -- var.elim.:  33000/52820          
c   -- var.elim.:  34000/52820          
c   -- var.elim.:  35000/52820          
c   -- var.elim.:  36000/52820          
c   -- var.elim.:  37000/52820          
c   -- var.elim.:  38000/52820          
c   -- var.elim.:  39000/52820          
c   -- var.elim.:  40000/52820          
c   -- var.elim.:  41000/52820          
c   -- var.elim.:  42000/52820          
c   -- var.elim.:  43000/52820          
c   -- var.elim.:  44000/52820          
c   -- var.elim.:  45000/52820          
c   -- var.elim.:  46000/52820          
c   -- var.elim.:  47000/52820          
c   -- var.elim.:  48000/52820          
c   -- var.elim.:  49000/52820          
c   -- var.elim.:  50000/52820          
c   -- var.elim.:  51000/52820          
c   -- var.elim.:  52000/52820          
c   -- var.elim.:  52820/52820          
c   -- var.elim.:  1000/26128          
c   -- var.elim.:  2000/26128          
c   -- var.elim.:  3000/26128          
c   -- var.elim.:  4000/26128          
c   -- var.elim.:  5000/26128          
c   -- var.elim.:  6000/26128          
c   -- var.elim.:  7000/26128          
c   -- var.elim.:  8000/26128          
c   -- var.elim.:  9000/26128          
c   -- var.elim.:  10000/26128          
c   -- var.elim.:  11000/26128          
c   -- var.elim.:  12000/26128          
c   -- var.elim.:  13000/26128          
c   -- var.elim.:  14000/26128          
c   -- var.elim.:  15000/26128          
c   -- var.elim.:  16000/26128          
c   -- var.elim.:  17000/26128          
c   -- var.elim.:  18000/26128          
c   -- var.elim.:  19000/26128          
c   -- var.elim.:  20000/26128          
c   -- var.elim.:  21000/26128          
c   -- var.elim.:  22000/26128          
c   -- var.elim.:  23000/26128          
c   -- var.elim.:  24000/26128          
c   -- var.elim.:  25000/26128          
c   -- var.elim.:  26000/26128          
c   -- var.elim.:  26128/26128          
c   -- var.elim.:  1000/15120          
c   -- var.elim.:  2000/15120          
c   -- var.elim.:  3000/15120          
c   -- var.elim.:  4000/15120          
c   -- var.elim.:  5000/15120          
c   -- var.elim.:  6000/15120          
c   -- var.elim.:  7000/15120          
c   -- var.elim.:  8000/15120          
c   -- var.elim.:  9000/15120          
c   -- var.elim.:  10000/15120          
c   -- var.elim.:  11000/15120          
c   -- var.elim.:  12000/15120          
c   -- var.elim.:  13000/15120          
c   -- var.elim.:  14000/15120          
c   -- var.elim.:  15000/15120          
c   -- var.elim.:  15120/15120          
c   -- var.elim.:  1000/12039          
c   -- var.elim.:  2000/12039          
c   -- var.elim.:  3000/12039          
c   -- var.elim.:  4000/12039          
c   -- var.elim.:  5000/12039          
c   -- var.elim.:  6000/12039          
c   -- var.elim.:  7000/12039          
c   -- var.elim.:  8000/12039          
c   -- var.elim.:  9000/12039          
c   -- var.elim.:  10000/12039          
c   -- var.elim.:  11000/12039          
c   -- var.elim.:  12000/12039          
c   -- var.elim.:  12039/12039          
c   -- var.elim.:  1000/5941          
c   -- var.elim.:  2000/5941          
c   -- var.elim.:  3000/5941          
c   -- var.elim.:  4000/5941          
c   -- var.elim.:  5000/5941          
c   -- var.elim.:  5941/5941          
c   -- var.elim.:  1000/2614          
c   -- var.elim.:  2000/2614          
c   -- var.elim.:  2614/2614          
c   -- subsuming                       
c   -- var.elim.:  1000/15039          
c   -- var.elim.:  2000/15039          
c   -- var.elim.:  3000/15039          
c   -- var.elim.:  4000/15039          
c   -- var.elim.:  5000/15039          
c   -- var.elim.:  6000/15039          
c   -- var.elim.:  7000/15039          
c   -- var.elim.:  8000/15039          
c   -- var.elim.:  9000/15039          
c   -- var.elim.:  10000/15039          
c   -- var.elim.:  11000/15039          
c   -- var.elim.:  12000/15039          
c   -- var.elim.:  13000/15039          
c   -- var.elim.:  14000/15039          
c   -- var.elim.:  15000/15039          
c   -- var.elim.:  15039/15039          
c   -- var.elim.:  30/30          
c |     75208 |   77060   587954 |      --   73641       --      -- |     --   | -29299/15172
c |     75208 |   77060   587954 |   30824   69900 11570961   165.5 |  3.014 % |
c |     75308 |   77060   587954 |   33906   13789  2516169   182.5 |  2.827 % |
c |     75460 |   77021   587567 |   37278   13940  2522856   181.0 |  2.848 % |
c |     75686 |   77021   587567 |   41005   14166  2527573   178.4 |  2.848 % |
c |     76027 |   77021   587567 |   45106   14507  2541810   175.2 |  2.848 % |
c |     76534 |   77017   587525 |   49614   15006  2561890   170.7 |  2.853 % |
c |     77293 |   77017   587525 |   54576   15765  2623522   166.4 |  2.853 % |
c |     78432 |   76979   587213 |   60004   16903  2702529   159.9 |  2.895 % |
c |     80141 |   76933   586818 |   65965   18611  2769540   148.8 |  2.953 % |
c |     82705 |   76933   586818 |   72561   21175  3270499   154.5 |  2.953 % |
c |     86550 |   76933   586818 |   79817   25020  3730248   149.1 |  2.953 % |
c |     92319 |   76933   586818 |   87799   30789  4663920   151.5 |  2.953 % |
c |    100970 |   76933   586818 |   96579   39440  6324071   160.3 |  2.953 % |
c |    113945 |   76933   586818 |  106237   52415  8287931   158.1 |  2.953 % |
c |    133406 |   76933   586818 |  116861   71876 10731083   149.3 |  2.953 % |
c |    162599 |   76874   586301 |  128448  101068 18319851   181.3 |  3.024 % |
c |    206388 |   76874   586301 |  141293   20165  3019959   149.8 |  3.024 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 x5 -x6 -x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 x39 -x40 -x41 -x42 x43 -x44 -x45 -x46 x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 x57 x58 -x59 -x60 -x61 x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 x103 -x104 x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 x115 -x116 -x117 -x118 x119 -x120 -x121 -x122 -x123 x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 x192 x193 -x194 -x195 -x196 -x197 -x198 -x199 x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 x226 -x227 -x228 -x229 x230 -x231 -x232 -x233 -x234 -x235 x236 -x237 -x238 -x239 -x240 x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 x343 -x344 -x345 -x346 -x347 x348 -x349 -x350 x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 x487 -x488 x489 x490 x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 x524 -x525 -x526 -x527 -x528 x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 x596 -x597 -x598 -x599 -x600 -x601 x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 x651 -x652 x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 x705 x706 -x707 -x708 x709 -x710 -x711 -x712 -x713 -x714 -x715 x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 x727 x728 x729 -x730 -x731 -x732 -x733 x734 -x735 x736 -x737 x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 x746 -x747 -x748 -x749 -x750 x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 x760 -x761 x762 x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 x772 -x773 -x774 x775 -x776 x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 x805 -x806 x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 x843 -x#### 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/55 27088
Raw data (stat): 27088 (runsolver) R 27087 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480056246 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.0013 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 8890 0 0 0 966 32 0 0 25 0 1 0 480056246 39051264 8652 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9534 8652 603 41 0 9493 0
vsize: 38136
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 8890 0 0 0 1966 32 0 0 25 0 1 0 480056246 39051264 8652 4294967295 134512640 134672761 3221224576 3221223056 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9534 8652 603 41 0 9493 0
vsize: 38136
[startup+30.0017 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9111 0 0 0 2965 33 0 0 25 0 1 0 480056246 39636992 8811 4294967295 134512640 134672761 3221224576 3221223056 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9677 8811 603 41 0 9636 0
vsize: 38708
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9111 0 0 0 3964 33 0 0 25 0 1 0 480056246 39636992 8811 4294967295 134512640 134672761 3221224576 3221223024 134643468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9677 8811 603 41 0 9636 0
vsize: 38708
[startup+50.003 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9111 0 0 0 4964 33 0 0 25 0 1 0 480056246 39636992 8811 4294967295 134512640 134672761 3221224576 3221223068 134638243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9677 8811 603 41 0 9636 0
vsize: 38708
[startup+60.0041 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9114 0 0 0 5964 34 0 0 25 0 1 0 480056246 39636992 8814 4294967295 134512640 134672761 3221224576 3221223024 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9677 8814 603 41 0 9636 0
vsize: 38708
[startup+70.0049 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9114 0 0 0 6963 34 0 0 25 0 1 0 480056246 39374848 8752 4294967295 134512640 134672761 3221224576 3221222944 134565212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9613 8752 603 41 0 9572 0
vsize: 38452
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9114 0 0 0 7963 34 0 0 25 0 1 0 480056246 39374848 8752 4294967295 134512640 134672761 3221224576 3221223136 134607831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9613 8752 603 41 0 9572 0
vsize: 38452
[startup+90.0045 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9114 0 0 0 8963 34 0 0 25 0 1 0 480056246 39374848 8752 4294967295 134512640 134672761 3221224576 3221222528 134566554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9613 8752 603 41 0 9572 0
vsize: 38452
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9114 0 0 0 9963 34 0 0 25 0 1 0 480056246 39374848 8752 4294967295 134512640 134672761 3221224576 3221222976 134605433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9613 8752 603 41 0 9572 0
vsize: 38452
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9114 0 0 0 10963 34 0 0 25 0 1 0 480056246 39374848 8752 4294967295 134512640 134672761 3221224576 3221223072 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9613 8752 603 41 0 9572 0
vsize: 38452
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9208 0 0 0 11963 35 0 0 25 0 1 0 480056246 40124416 8846 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9796 8846 603 41 0 9755 0
vsize: 39184
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9283 0 0 0 12963 35 0 0 25 0 1 0 480056246 39837696 8827 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9726 8827 603 41 0 9685 0
vsize: 38904
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9283 0 0 0 13963 35 0 0 25 0 1 0 480056246 39837696 8827 4294967295 134512640 134672761 3221224576 3221223024 134643539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9726 8827 603 41 0 9685 0
vsize: 38904
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9390 0 0 0 14963 36 0 0 25 0 1 0 480056246 39968768 8885 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9758 8885 603 41 0 9717 0
vsize: 39032
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 9896 0 0 0 15960 38 0 0 25 0 1 0 480056246 41988096 9391 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10251 9391 603 41 0 10210 0
vsize: 41004
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27088
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 10209 0 0 0 16960 39 0 0 25 0 1 0 480056246 43298816 9704 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10571 9704 603 41 0 10530 0
vsize: 42284
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 10800 0 0 0 17958 41 0 0 25 0 1 0 480056246 45707264 10295 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11159 10295 603 41 0 11118 0
vsize: 44636
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 13548 0 0 0 18926 62 0 0 25 0 1 0 480056246 53903360 10913 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13160 10913 603 41 0 13119 0
vsize: 52640
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 13548 0 0 0 19925 62 0 0 25 0 1 0 480056246 53903360 10913 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13160 10913 603 41 0 13119 0
vsize: 52640
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 13549 0 0 0 20924 64 0 0 25 0 1 0 480056246 53903360 10914 4294967295 134512640 134672761 3221224576 3221223024 134644008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13160 10914 603 41 0 13119 0
vsize: 52640
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 13549 0 0 0 21923 64 0 0 25 0 1 0 480056246 53903360 10914 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13160 10914 603 41 0 13119 0
vsize: 52640
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 13737 0 0 0 22922 65 0 0 25 0 1 0 480056246 53903360 10914 4294967295 134512640 134672761 3221224576 3221223024 134643567 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13160 10914 603 41 0 13119 0
vsize: 52640
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 13737 0 0 0 23922 65 0 0 25 0 1 0 480056246 53903360 10914 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13160 10914 603 41 0 13119 0
vsize: 52640
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 13905 0 0 0 24922 65 0 0 25 0 1 0 480056246 54566912 11082 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13322 11082 603 41 0 13281 0
vsize: 53288
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 14644 0 0 0 25919 67 0 0 25 0 1 0 480056246 57602048 11821 4294967295 134512640 134672761 3221224576 3221223760 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14063 11821 603 41 0 14022 0
vsize: 56252
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 16003 0 0 0 26916 71 0 0 25 0 1 0 480056246 63250432 13180 4294967295 134512640 134672761 3221224576 3221223776 134610683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15442 13180 603 41 0 15401 0
vsize: 61768
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 16434 0 0 0 27914 72 0 0 25 0 1 0 480056246 64962560 13611 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15860 13611 603 41 0 15819 0
vsize: 63440
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 16847 0 0 0 28913 73 0 0 25 0 1 0 480056246 66678784 14024 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16279 14024 603 41 0 16238 0
vsize: 65116
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 17184 0 0 0 29912 74 0 0 25 0 1 0 480056246 68116480 14361 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16630 14361 603 41 0 16589 0
vsize: 66520
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 17616 0 0 0 30912 74 0 0 25 0 1 0 480056246 69980160 14793 4294967295 134512640 134672761 3221224576 3221223760 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17085 14793 603 41 0 17044 0
vsize: 68340
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 17979 0 0 0 31912 75 0 0 25 0 1 0 480056246 71430144 15156 4294967295 134512640 134672761 3221224576 3221223760 134615998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17439 15156 603 41 0 17398 0
vsize: 69756
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 18459 0 0 0 32911 76 0 0 25 0 1 0 480056246 73408512 15636 4294967295 134512640 134672761 3221224576 3221223760 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17922 15636 603 41 0 17881 0
vsize: 71688
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 19000 0 0 0 33910 77 0 0 25 0 1 0 480056246 75505664 16177 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18434 16177 603 41 0 18393 0
vsize: 73736
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 19541 0 0 0 34908 79 0 0 25 0 1 0 480056246 77750272 16718 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18982 16718 603 41 0 18941 0
vsize: 75928
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 20148 0 0 0 35907 80 0 0 25 0 1 0 480056246 80252928 17325 4294967295 134512640 134672761 3221224576 3221223388 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19593 17325 603 41 0 19552 0
vsize: 78372
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 21093 0 0 0 36905 83 0 0 25 0 1 0 480056246 84070400 18270 4294967295 134512640 134672761 3221224576 3221223728 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20525 18271 603 41 0 20484 0
vsize: 82100
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 22090 0 0 0 37901 87 0 0 25 0 1 0 480056246 88170496 19267 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21526 19267 603 41 0 21485 0
vsize: 86104
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 22688 0 0 0 38899 89 0 0 25 0 1 0 480056246 90546176 19865 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22106 19865 603 41 0 22065 0
vsize: 88424
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27090
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 23415 0 0 0 39898 91 0 0 25 0 1 0 480056246 93589504 20592 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22849 20592 603 41 0 22808 0
vsize: 91396
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 27093
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 24375 0 0 0 40891 97 0 0 25 0 1 0 480056246 97681408 21552 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23848 21552 603 41 0 23807 0
vsize: 95392
[startup+420.016 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 27143
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 25365 0 0 0 41885 103 0 0 25 0 1 0 480056246 101773312 22542 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24847 22542 603 41 0 24806 0
vsize: 99388
[startup+430.016 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 27143
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 30944 0 0 0 42796 145 0 0 25 0 1 0 480056246 110264320 25549 4294967295 134512640 134672761 3221224576 3221222992 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26920 25549 603 41 0 26879 0
vsize: 107680
[startup+440.017 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 27143
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 30946 0 0 0 43796 145 0 0 25 0 1 0 480056246 110264320 25551 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26920 25551 603 41 0 26879 0
vsize: 107680
[startup+450.017 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 27143
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 30974 0 0 0 44796 145 0 0 25 0 1 0 480056246 110194688 25527 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26903 25527 603 41 0 26862 0
vsize: 107612
[startup+460.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27143
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 30976 0 0 0 45796 146 0 0 25 0 1 0 480056246 110194688 25529 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26903 25529 603 41 0 26862 0
vsize: 107612
[startup+470.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27143
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 30976 0 0 0 46794 147 0 0 25 0 1 0 480056246 110194688 25529 4294967295 134512640 134672761 3221224576 3221223024 134643963 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26903 25529 603 41 0 26862 0
vsize: 107612
[startup+480.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 30976 0 0 0 47793 148 0 0 25 0 1 0 480056246 110059520 25523 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25523 603 41 0 26829 0
vsize: 107480
[startup+490.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 30976 0 0 0 48793 149 0 0 25 0 1 0 480056246 110059520 25523 4294967295 134512640 134672761 3221224576 3221222880 134621885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25523 603 41 0 26829 0
vsize: 107480
[startup+500.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31256 0 0 0 49792 150 0 0 25 0 1 0 480056246 111865856 25751 4294967295 134512640 134672761 3221224576 3221222400 134566724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27311 25751 603 41 0 27270 0
vsize: 109244
[startup+510.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31273 0 0 0 50792 150 0 0 25 0 1 0 480056246 109961216 25492 4294967295 134512640 134672761 3221224576 3221223024 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26846 25492 603 41 0 26805 0
vsize: 107384
[startup+520.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 51792 150 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+530.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 52792 151 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+540.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 53792 151 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+550.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 54791 151 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+560.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 55791 151 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+570.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 56791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+580.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 57791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+590.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 58791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+600.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 59791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+610.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 60791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+620.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 61791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 62791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+640.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 63791 152 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+650.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 64791 153 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 65791 153 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+670.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 66791 153 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+680.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 67791 153 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+690.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 68791 153 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+700.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 69791 153 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27147
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31401 0 0 0 70791 153 0 0 25 0 1 0 480056246 110059520 25535 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25535 603 41 0 26829 0
vsize: 107480
[startup+720.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27149
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31403 0 0 0 71791 153 0 0 25 0 1 0 480056246 110059520 25537 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25537 603 41 0 26829 0
vsize: 107480
[startup+730.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27149
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31404 0 0 0 72792 153 0 0 25 0 1 0 480056246 110059520 25538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25538 603 41 0 26829 0
vsize: 107480
[startup+740.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27149
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31406 0 0 0 73792 153 0 0 25 0 1 0 480056246 110059520 25540 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26870 25540 603 41 0 26829 0
vsize: 107480
[startup+750.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27149
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31438 0 0 0 74792 153 0 0 25 0 1 0 480056246 110194688 25572 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26903 25572 603 41 0 26862 0
vsize: 107612
[startup+760.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27149
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 31885 0 0 0 75791 154 0 0 25 0 1 0 480056246 112033792 26019 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27352 26019 603 41 0 27311 0
vsize: 109408
[startup+770.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27149
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 32256 0 0 0 76790 156 0 0 25 0 1 0 480056246 113618944 26390 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27739 26390 603 41 0 27698 0
vsize: 110956
[startup+780.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 32638 0 0 0 77789 157 0 0 25 0 1 0 480056246 115085312 26772 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28097 26772 603 41 0 28056 0
vsize: 112388
[startup+790.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 33299 0 0 0 78788 158 0 0 25 0 1 0 480056246 117862400 27433 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28775 27433 603 41 0 28734 0
vsize: 115100
[startup+800.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 34074 0 0 0 79785 161 0 0 25 0 1 0 480056246 121020416 28208 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29546 28208 603 41 0 29505 0
vsize: 118184
[startup+810.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 34644 0 0 0 80784 162 0 0 25 0 1 0 480056246 123387904 28778 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30124 28778 603 41 0 30083 0
vsize: 120496
[startup+820.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 35228 0 0 0 81783 164 0 0 25 0 1 0 480056246 125771776 29362 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30706 29362 603 41 0 30665 0
vsize: 122824
[startup+830.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 35809 0 0 0 82782 165 0 0 25 0 1 0 480056246 128151552 29943 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31287 29943 603 41 0 31246 0
vsize: 125148
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 36379 0 0 0 83780 167 0 0 25 0 1 0 480056246 130383872 30513 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31832 30513 603 41 0 31791 0
vsize: 127328
[startup+850.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 36941 0 0 0 84778 169 0 0 25 0 1 0 480056246 132763648 31075 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32413 31075 603 41 0 32372 0
vsize: 129652
[startup+860.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 37368 0 0 0 85778 170 0 0 25 0 1 0 480056246 134492160 31502 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32835 31502 603 41 0 32794 0
vsize: 131340
[startup+870.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 37837 0 0 0 86777 171 0 0 25 0 1 0 480056246 136335360 31971 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33285 31971 603 41 0 33244 0
vsize: 133140
[startup+880.03 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 38404 0 0 0 87775 173 0 0 25 0 1 0 480056246 138698752 32538 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33862 32538 603 41 0 33821 0
vsize: 135448
[startup+890.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 38973 0 0 0 88773 175 0 0 25 0 1 0 480056246 141066240 33107 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34440 33107 603 41 0 34399 0
vsize: 137760
[startup+900.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 39589 0 0 0 89772 177 0 0 25 0 1 0 480056246 143548416 33723 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35046 33723 603 41 0 35005 0
vsize: 140184
[startup+910.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 40218 0 0 0 90770 179 0 0 25 0 1 0 480056246 146079744 34352 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35664 34352 603 41 0 35623 0
vsize: 142656
[startup+920.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 40839 0 0 0 91768 180 0 0 25 0 1 0 480056246 148570112 34973 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36272 34973 603 41 0 36231 0
vsize: 145088
[startup+930.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 41386 0 0 0 92767 182 0 0 25 0 1 0 480056246 150810624 35520 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36819 35520 603 41 0 36778 0
vsize: 147276
[startup+940.031 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 41902 0 0 0 93766 183 0 0 25 0 1 0 480056246 153042944 36036 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37364 36036 603 41 0 37323 0
vsize: 149456
[startup+950.031 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 42285 0 0 0 94765 184 0 0 25 0 1 0 480056246 154501120 36419 4294967295 134512640 134672761 3221224576 3221223760 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37720 36419 603 41 0 37679 0
vsize: 150880
[startup+960.031 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 42480 0 0 0 95765 184 0 0 25 0 1 0 480056246 155291648 36614 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37913 36614 603 41 0 37872 0
vsize: 151652
[startup+970.031 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 42752 0 0 0 96765 185 0 0 25 0 1 0 480056246 156475392 36886 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38202 36886 603 41 0 38161 0
vsize: 152808
[startup+980.031 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 42999 0 0 0 97764 185 0 0 25 0 1 0 480056246 157392896 37133 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38426 37133 603 41 0 38385 0
vsize: 153704
[startup+990.031 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 43241 0 0 0 98763 187 0 0 25 0 1 0 480056246 158453760 37375 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38685 37375 603 41 0 38644 0
vsize: 154740
[startup+1000.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 43433 0 0 0 99763 187 0 0 25 0 1 0 480056246 159244288 37567 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38878 37567 603 41 0 38837 0
vsize: 155512
[startup+1010.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 43637 0 0 0 100762 188 0 0 25 0 1 0 480056246 160034816 37771 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39071 37771 603 41 0 39030 0
vsize: 156284
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 43818 0 0 0 101762 188 0 0 25 0 1 0 480056246 161345536 37952 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39391 37952 603 41 0 39350 0
vsize: 157564
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 44016 0 0 0 102762 188 0 0 25 0 1 0 480056246 162140160 38150 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39585 38150 603 41 0 39544 0
vsize: 158340
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 44218 0 0 0 103762 189 0 0 25 0 1 0 480056246 162938880 38352 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39780 38352 603 41 0 39739 0
vsize: 159120
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 44400 0 0 0 104761 189 0 0 25 0 1 0 480056246 163725312 38534 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39972 38534 603 41 0 39931 0
vsize: 159888
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 44591 0 0 0 105761 190 0 0 25 0 1 0 480056246 164511744 38725 4294967295 134512640 134672761 3221224576 3221223776 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40164 38725 603 41 0 40123 0
vsize: 160656
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27151
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 44814 0 0 0 106761 190 0 0 25 0 1 0 480056246 165310464 38948 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40359 38949 603 41 0 40318 0
vsize: 161436
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 107760 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223712 134614713 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 108761 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223760 134615843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 109761 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223724 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 110761 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 111761 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 112761 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 113761 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 114761 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 115762 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223760 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 116762 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 117762 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223756 134615849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 118762 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 119762 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
[startup+1210.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27153
Raw data (stat): 27088 (minisat+) R 27087 22929 22928 0 -1 0 45145 0 0 0 120762 191 0 0 25 0 1 0 480056246 166100992 39143 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40552 39143 603 41 0 40511 0
vsize: 162208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.92 1/55 27153
Raw data (stat): 27088 (minisat+) Z 27087 22929 22928 0 -1 12 45146 0 0 0 120763 202 0 0 25 0 1 0 480056246 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.14
CPU time (s): 1209.65
CPU user time (s): 1207.63
CPU system time (s): 2.02269
CPU usage (%): 99.9596
Max. virtual memory (Kb): 162208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####