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-cmb.opb
MD5SUM	a8596c98551f801a6658f1ce91b33278
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1053
Optimality of the best value was proved	NO
Number of terms in the objective function	304
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	12887
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	12887
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.97785
Number of variables	304
Total number of constraints	671
Number of constraints which are clauses	671
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	28
Trace number 5589

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 00:37:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4013 boxname=wulflinc25 idbench=253 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a8596c98551f801a6658f1ce91b33278  /oldhome/oroussel/tmp/wulflinc25/normalized-cmb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-cmb.opb /oldhome/oroussel/tmp/wulflinc25/normalized-cmb.opb
IDLAUNCH: 4013
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        895700 kB
Buffers:         34192 kB
Cached:          70220 kB
SwapCached:         36 kB
Active:          47948 kB
Inactive:        59340 kB
HighTotal:      131008 kB
HighFree:        57120 kB
LowTotal:       903652 kB
LowFree:        838580 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26016 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:57:41 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 4013 7 1200.09 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 667 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 |     666     3356 |     199       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  265/265          
c |         0 |     666     3347 |      --       0       --      -- |     --   | 0/-9
c |         0 |     666     3347 |     266       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.037994 s)
c ==============================================================================
c [1mFound solution: 1524[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:43621     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  105120   247266 |   31535       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/39405          
c   -- var.elim.:  2000/39405          
c   -- var.elim.:  3000/39405          
c   -- var.elim.:  4000/39405          
c   -- var.elim.:  5000/39405          
c   -- var.elim.:  6000/39405          
c   -- var.elim.:  7000/39405          
c   -- var.elim.:  8000/39405          
c   -- var.elim.:  9000/39405          
c   -- var.elim.:  10000/39405          
c   -- var.elim.:  11000/39405          
c   -- var.elim.:  12000/39405          
c   -- var.elim.:  13000/39405          
c   -- var.elim.:  14000/39405          
c   -- var.elim.:  15000/39405          
c   -- var.elim.:  16000/39405          
c   -- var.elim.:  17000/39405          
c   -- var.elim.:  18000/39405          
c   -- var.elim.:  19000/39405          
c   -- var.elim.:  20000/39405          
c   -- var.elim.:  21000/39405          
c   -- var.elim.:  22000/39405          
c   -- var.elim.:  23000/39405          
c   -- var.elim.:  24000/39405          
c   -- var.elim.:  25000/39405          
c   -- var.elim.:  26000/39405          
c   -- var.elim.:  27000/39405          
c   -- var.elim.:  28000/39405          
c   -- var.elim.:  29000/39405          
c   -- var.elim.:  30000/39405          
c   -- var.elim.:  31000/39405          
c   -- var.elim.:  32000/39405          
c   -- var.elim.:  33000/39405          
c   -- var.elim.:  34000/39405          
c   -- var.elim.:  35000/39405          
c   -- var.elim.:  36000/39405          
c   -- var.elim.:  37000/39405          
c   -- var.elim.:  38000/39405          
c   -- var.elim.:  39000/39405          
c   -- var.elim.:  39405/39405          
c   -- var.elim.:  1000/21117          
c   -- var.elim.:  2000/21117          
c   -- var.elim.:  3000/21117          
c   -- var.elim.:  4000/21117          
c   -- var.elim.:  5000/21117          
c   -- var.elim.:  6000/21117          
c   -- var.elim.:  7000/21117          
c   -- var.elim.:  8000/21117          
c   -- var.elim.:  9000/21117          
c   -- var.elim.:  10000/21117          
c   -- var.elim.:  11000/21117          
c   -- var.elim.:  12000/21117          
c   -- var.elim.:  13000/21117          
c   -- var.elim.:  14000/21117          
c   -- var.elim.:  15000/21117          
c   -- var.elim.:  16000/21117          
c   -- var.elim.:  17000/21117          
c   -- var.elim.:  18000/21117          
c   -- var.elim.:  19000/21117          
c   -- var.elim.:  20000/21117          
c   -- var.elim.:  21000/21117          
c   -- var.elim.:  21117/21117          
c   -- subsuming                       
c   -- var.elim.:  1000/4232          
c   -- var.elim.:  2000/4232          
c   -- var.elim.:  3000/4232          
c   -- var.elim.:  4000/4232          
c   -- var.elim.:  4232/4232          
c   -- var.elim.:  836/836          
c   -- var.elim.:  962/962          
c   -- var.elim.:  172/172          
c   -- subsuming                       
c   -- var.elim.:  718/718          
c |         0 |   93226   317289 |      --       0       --      -- |     --   | -11894/70024
c |         0 |   93226   317289 |   37290       0        0     nan |  0.000 % |
c |       100 |   93010   316345 |   40924      98     1388    14.2 |  0.156 % |
c |       250 |   93010   316345 |   45016     248     3151    12.7 |  0.156 % |
c |       476 |   93010   316345 |   49518     474     9347    19.7 |  0.156 % |
c |       813 |   91537   311205 |   53607     699    22352    32.0 |  1.231 % |
c |      1319 |   91011   309430 |   58629    1197   124945   104.4 |  1.709 % |
c |      2080 |   91011   309430 |   64492    1958   167246    85.4 |  1.709 % |
c |      3219 |   90915   308742 |   70867    3092   189500    61.3 |  1.770 % |
c ==============================================================================
c (current CPU-time: 22.4496 s)
c ==============================================================================
c [1mFound solution: 1523[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:34945     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3490 |  177854   512756 |   53356    3362   214801    63.9 |  1.770 % |
c   -- subsuming                       
c   -- var.elim.:  1000/37434          
c   -- var.elim.:  2000/37434          
c   -- var.elim.:  3000/37434          
c   -- var.elim.:  4000/37434          
c   -- var.elim.:  5000/37434          
c   -- var.elim.:  6000/37434          
c   -- var.elim.:  7000/37434          
c   -- var.elim.:  8000/37434          
c   -- var.elim.:  9000/37434          
c   -- var.elim.:  10000/37434          
c   -- var.elim.:  11000/37434          
c   -- var.elim.:  12000/37434          
c   -- var.elim.:  13000/37434          
c   -- var.elim.:  14000/37434          
c   -- var.elim.:  15000/37434          
c   -- var.elim.:  16000/37434          
c   -- var.elim.:  17000/37434          
c   -- var.elim.:  18000/37434          
c   -- var.elim.:  19000/37434          
c   -- var.elim.:  20000/37434          
c   -- var.elim.:  21000/37434          
c   -- var.elim.:  22000/37434          
c   -- var.elim.:  23000/37434          
c   -- var.elim.:  24000/37434          
c   -- var.elim.:  25000/37434          
c   -- var.elim.:  26000/37434          
c   -- var.elim.:  27000/37434          
c   -- var.elim.:  28000/37434          
c   -- var.elim.:  29000/37434          
c   -- var.elim.:  30000/37434          
c   -- var.elim.:  31000/37434          
c   -- var.elim.:  32000/37434          
c   -- var.elim.:  33000/37434          
c   -- var.elim.:  34000/37434          
c   -- var.elim.:  35000/37434          
c   -- var.elim.:  36000/37434          
c   -- var.elim.:  37000/37434          
c   -- var.elim.:  37434/37434          
c   -- var.elim.:  1000/20144          
c   -- var.elim.:  2000/20144          
c   -- var.elim.:  3000/20144          
c   -- var.elim.:  4000/20144          
c   -- var.elim.:  5000/20144          
c   -- var.elim.:  6000/20144          
c   -- var.elim.:  7000/20144          
c   -- var.elim.:  8000/20144          
c   -- var.elim.:  9000/20144          
c   -- var.elim.:  10000/20144          
c   -- var.elim.:  11000/20144          
c   -- var.elim.:  12000/20144          
c   -- var.elim.:  13000/20144          
c   -- var.elim.:  14000/20144          
c   -- var.elim.:  15000/20144          
c   -- var.elim.:  16000/20144          
c   -- var.elim.:  17000/20144          
c   -- var.elim.:  18000/20144          
c   -- var.elim.:  19000/20144          
c   -- var.elim.:  20000/20144          
c   -- var.elim.:  20144/20144          
c   -- var.elim.:  430/430          
c   -- var.elim.:  895/895          
c   -- subsuming                       
c   -- var.elim.:  1000/4798          
c   -- var.elim.:  2000/4798          
c   -- var.elim.:  3000/4798          
c   -- var.elim.:  4000/4798          
c   -- var.elim.:  4798/4798          
c   -- var.elim.:  576/576          
c   -- var.elim.:  44/44          
c   -- subsuming                       
c   -- var.elim.:  340/340          
c   -- var.elim.:  20/20          
c |      3490 |  166422   565245 |      --    3362       --      -- |     --   | -11432/52490
c |      3490 |  166422   565245 |   66568    2853    72298    25.3 |  1.770 % |
c |      3591 |  166422   565245 |   73225    2954    73191    24.8 |  1.024 % |
c |      3741 |  166422   565245 |   80548    3104   101409    32.7 |  1.024 % |
c |      3967 |  166422   565245 |   88603    3330   106141    31.9 |  1.024 % |
c |      4305 |  166422   565245 |   97463    3668   130755    35.6 |  1.024 % |
c |      4811 |  166422   565245 |  107209    4174   199775    47.9 |  1.024 % |
c ==============================================================================
c (current CPU-time: 46.9149 s)
c ==============================================================================
c [1mFound solution: 1465[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35967     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5046 |  255159   772563 |   76547    4405   211861    48.1 |  1.024 % |
c   -- subsuming                       
c   -- var.elim.:  1000/36275          
c   -- var.elim.:  2000/36275          
c   -- var.elim.:  3000/36275          
c   -- var.elim.:  4000/36275          
c   -- var.elim.:  5000/36275          
c   -- var.elim.:  6000/36275          
c   -- var.elim.:  7000/36275          
c   -- var.elim.:  8000/36275          
c   -- var.elim.:  9000/36275          
c   -- var.elim.:  10000/36275          
c   -- var.elim.:  11000/36275          
c   -- var.elim.:  12000/36275          
c   -- var.elim.:  13000/36275          
c   -- var.elim.:  14000/36275          
c   -- var.elim.:  15000/36275          
c   -- var.elim.:  16000/36275          
c   -- var.elim.:  17000/36275          
c   -- var.elim.:  18000/36275          
c   -- var.elim.:  19000/36275          
c   -- var.elim.:  20000/36275          
c   -- var.elim.:  21000/36275          
c   -- var.elim.:  22000/36275          
c   -- var.elim.:  23000/36275          
c   -- var.elim.:  24000/36275          
c   -- var.elim.:  25000/36275          
c   -- var.elim.:  26000/36275          
c   -- var.elim.:  27000/36275          
c   -- var.elim.:  28000/36275          
c   -- var.elim.:  29000/36275          
c   -- var.elim.:  30000/36275          
c   -- var.elim.:  31000/36275          
c   -- var.elim.:  32000/36275          
c   -- var.elim.:  33000/36275          
c   -- var.elim.:  34000/36275          
c   -- var.elim.:  35000/36275          
c   -- var.elim.:  36000/36275          
c   -- var.elim.:  36275/36275          
c   -- var.elim.:  1000/19512          
c   -- var.elim.:  2000/19512          
c   -- var.elim.:  3000/19512          
c   -- var.elim.:  4000/19512          
c   -- var.elim.:  5000/19512          
c   -- var.elim.:  6000/19512          
c   -- var.elim.:  7000/19512          
c   -- var.elim.:  8000/19512          
c   -- var.elim.:  9000/19512          
c   -- var.elim.:  10000/19512          
c   -- var.elim.:  11000/19512          
c   -- var.elim.:  12000/19512          
c   -- var.elim.:  13000/19512          
c   -- var.elim.:  14000/19512          
c   -- var.elim.:  15000/19512          
c   -- var.elim.:  16000/19512          
c   -- var.elim.:  17000/19512          
c   -- var.elim.:  18000/19512          
c   -- var.elim.:  19000/19512          
c   -- var.elim.:  19512/19512          
c   -- var.elim.:  603/603          
c   -- var.elim.:  1000/1115          
c   -- var.elim.:  1115/1115          
c   -- subsuming                       
c   -- var.elim.:  1000/4191          
c   -- var.elim.:  2000/4191          
c   -- var.elim.:  3000/4191          
c   -- var.elim.:  4000/4191          
c   -- var.elim.:  4191/4191          
c   -- var.elim.:  684/684          
c   -- var.elim.:  412/412          
c   -- subsuming                       
c   -- var.elim.:  662/662          
c |      5046 |  244227   827060 |      --    4405       --      -- |     --   | -10932/54498
c |      5046 |  244227   827060 |   97690    4404   211660    48.1 |  1.024 % |
c |      5146 |  244227   827060 |  107459    4504   213583    47.4 |  0.752 % |
c ==============================================================================
c (current CPU-time: 64.4802 s)
c ==============================================================================
c [1mFound solution: 1454[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5180 |  246793   834550 |   74037    4535   214199    47.2 |  0.752 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4793          
c   -- var.elim.:  2000/4793          
c   -- var.elim.:  3000/4793          
c   -- var.elim.:  4000/4793          
c   -- var.elim.:  4793/4793          
c   -- var.elim.:  1000/2576          
c   -- var.elim.:  2000/2576          
c   -- var.elim.:  2576/2576          
c   -- var.elim.:  431/431          
c   -- var.elim.:  483/483          
c   -- subsuming                       
c   -- var.elim.:  1000/2471          
c   -- var.elim.:  2000/2471          
c   -- var.elim.:  2471/2471          
c |      5180 |  244686   831502 |      --    4535       --      -- |     --   | -2107/-3047
c |      5180 |  244686   831502 |   97874    4535   214199    47.2 |  0.752 % |
c ==============================================================================
c (current CPU-time: 71.2222 s)
c ==============================================================================
c [1mFound solution: 1442[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5193 |  245691   834301 |   73707    4548   214672    47.2 |  0.752 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1613          
c   -- var.elim.:  1613/1613          
c   -- var.elim.:  913/913          
c   -- subsuming                       
c   -- var.elim.:  10/10          
c |      5193 |  245138   835619 |      --    4548       --      -- |     --   | -553/1319
c |      5193 |  245138   835619 |   98055    4548   214672    47.2 |  0.752 % |
c ==============================================================================
c (current CPU-time: 73.4688 s)
c ==============================================================================
c [1mFound solution: 1408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5219 |  245395   836361 |   73618    4574   216400    47.3 |  0.752 % |
c   -- subsuming                       
c   -- var.elim.:  483/483          
c   -- var.elim.:  256/256          
c |      5219 |  245173   836116 |      --    4574       --      -- |     --   | -222/-244
c |      5219 |  245173   836116 |   98069    4574   216400    47.3 |  0.752 % |
c ==============================================================================
c (current CPU-time: 75.7375 s)
c ==============================================================================
c [1mFound solution: 1350[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5269 |  245205   836504 |   73561    4624   218032    47.2 |  0.752 % |
c   -- subsuming                       
c   -- var.elim.:  650/650          
c   -- var.elim.:  335/335          
c |      5269 |  245191   837868 |      --    4624       --      -- |     --   | -14/1365
c |      5269 |  245191   837868 |   98076    4624   218032    47.2 |  0.752 % |
c |      5372 |  245191   837868 |  107884    4727   228580    48.4 |  0.758 % |
c |      5522 |  245191   837868 |  118672    4877   230678    47.3 |  0.758 % |
c |      5747 |  245191   837868 |  130539    5102   251075    49.2 |  0.758 % |
c |      6085 |  245191   837868 |  143593    5440   308230    56.7 |  0.758 % |
c |      6591 |  245139   836948 |  157919    5944   323281    54.4 |  0.769 % |
c |      7350 |  245139   836948 |  173711    6703   471228    70.3 |  0.769 % |
c |      8490 |  245139   836948 |  191082    7843   527280    67.2 |  0.769 % |
c |     10200 |  244959   834318 |  210036    9551   637798    66.8 |  0.821 % |
c |     12763 |  244959   834318 |  231040   12114  1905358   157.3 |  0.821 % |
c |     16607 |  244959   834318 |  254144   15958  4007226   251.1 |  0.821 % |
c ==============================================================================
c (current CPU-time: 212.144 s)
c ==============================================================================
c [1mFound solution: 1349[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16794 |  244990   834744 |   73496   16145  4017222   248.8 |  0.821 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1462          
c   -- var.elim.:  1462/1462          
c   -- var.elim.:  560/560          
c   -- subsuming                       
c |     16794 |  244954   835805 |      --   16145       --      -- |     --   | -36/1062
c |     16794 |  244954   835805 |   97981   15144  2621845   173.1 |  0.821 % |
c |     16894 |  244954   835805 |  107779   15244  2642101   173.3 |  0.824 % |
c |     17047 |  244927   835685 |  118544   15393  2643901   171.8 |  0.834 % |
c |     17272 |  244927   835685 |  130399   15618  2658507   170.2 |  0.834 % |
c |     17609 |  244927   835685 |  143439   15955  2672660   167.5 |  0.834 % |
c |     18115 |  244927   835685 |  157782   16461  2764959   168.0 |  0.834 % |
c |     18874 |  244927   835685 |  173561   17220  3008465   174.7 |  0.834 % |
c |     20015 |  244909   835599 |  190903   18360  3045544   165.9 |  0.841 % |
c |     21724 |  244806   835000 |  209905   20066  3408021   169.8 |  0.865 % |
c |     24287 |  244653   833388 |  230751   22624  3688594   163.0 |  0.914 % |
c |     28131 |  244653   833388 |  253826   26468  4938537   186.6 |  0.914 % |
c ==============================================================================
c (current CPU-time: 336.027 s)
c ==============================================================================
c [1mFound solution: 1254[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     30232 |  244774   834087 |   73432   28568  5199577   182.0 |  0.914 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1846          
c   -- var.elim.:  1846/1846          
c   -- var.elim.:  1000/1185          
c   -- var.elim.:  1185/1185          
c   -- var.elim.:  146/146          
c   -- subsuming                       
c   -- var.elim.:  325/325          
c |     30232 |  244650   835324 |      --   28568       --      -- |     --   | -124/1238
c |     30232 |  244650   835324 |   97860   23470  1493503    63.6 |  0.914 % |
c |     30332 |  244650   835324 |  107646   23570  1507306    64.0 |  0.918 % |
c |     30483 |  244650   835324 |  118410   23721  1520890    64.1 |  0.918 % |
c |     30708 |  244650   835324 |  130251   23946  1523960    63.6 |  0.918 % |
c |     31045 |  244505   834310 |  143191   24280  1528398    62.9 |  0.957 % |
c |     31553 |  244490   834261 |  157501   24764  1562472    63.1 |  0.961 % |
c |     32312 |  244233   831156 |  173069   25506  1637862    64.2 |  1.019 % |
c |     33453 |  244233   831156 |  190376   26647  1786755    67.1 |  1.019 % |
c |     35161 |  244233   831156 |  209414   28355  2460657    86.8 |  1.019 % |
c |     37723 |  244161   830899 |  230287   30916  2778538    89.9 |  1.034 % |
c |     41567 |  244161   830899 |  253316   34760  3704188   106.6 |  1.034 % |
c |     47333 |  244161   830899 |  278647   40526  6142969   151.6 |  1.034 % |
c |     55984 |  244161   830899 |  306512   49177  9014709   183.3 |  1.034 % |
c |     68958 |  244134   830803 |  337126   62145 11381803   183.1 |  1.043 % |
c |     88419 |  244134   830803 |  370839   81606 18345315   224.8 |  1.043 % |
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 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 32302
Raw data (stat): 32302 (runsolver) R 32301 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480337210 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+9.99954 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 6397 0 0 0 978 21 0 0 25 0 1 0 480337210 29028352 5935 4294967295 134512640 134672761 3221224576 3221223120 134621250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7087 5935 603 41 0 7046 0
vsize: 28348
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 6874 0 0 0 1975 23 0 0 25 0 1 0 480337210 29773824 6101 4294967295 134512640 134672761 3221224576 3221223760 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7269 6101 603 41 0 7228 0
vsize: 29076
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 12383 0 0 0 2953 45 0 0 25 0 1 0 480337210 50049024 9923 4294967295 134512640 134672761 3221224576 3221223024 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12219 9923 603 41 0 12178 0
vsize: 48876
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 13294 0 0 0 3950 48 0 0 25 0 1 0 480337210 49655808 9902 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12123 9902 603 41 0 12082 0
vsize: 48492
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 20449 0 0 0 4927 70 0 0 25 0 1 0 480337210 62644224 13998 4294967295 134512640 134672761 3221224576 3221221288 134646592 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15294 13998 603 41 0 15253 0
vsize: 61176
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 21165 0 0 0 5900 80 0 0 25 0 1 0 480337210 65531904 14568 4294967295 134512640 134672761 3221224576 3221223120 134621041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15999 14568 603 41 0 15958 0
vsize: 63996
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 26002 0 0 0 6883 97 0 0 25 0 1 0 480337210 65744896 14636 4294967295 134512640 134672761 3221224576 3221223288 134643444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16051 14636 603 41 0 16010 0
vsize: 64204
[startup+80.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 38012 0 0 0 7837 143 0 0 25 0 1 0 480337210 62722048 14140 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15313 14140 603 41 0 15272 0
vsize: 61252
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 38028 0 0 0 8836 143 0 0 25 0 1 0 480337210 62853120 14156 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15345 14156 603 41 0 15304 0
vsize: 61380
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 38169 0 0 0 9836 143 0 0 25 0 1 0 480337210 63381504 14297 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15474 14297 603 41 0 15433 0
vsize: 61896
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 38249 0 0 0 10835 144 0 0 25 0 1 0 480337210 63827968 14377 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15583 14377 603 41 0 15542 0
vsize: 62332
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 38325 0 0 0 11835 144 0 0 25 0 1 0 480337210 64094208 14453 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15648 14453 603 41 0 15607 0
vsize: 62592
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 38497 0 0 0 12834 145 0 0 25 0 1 0 480337210 64749568 14625 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15808 14625 603 41 0 15767 0
vsize: 63232
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 38800 0 0 0 13833 146 0 0 25 0 1 0 480337210 66011136 14928 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16116 14928 603 41 0 16075 0
vsize: 64464
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 39196 0 0 0 14833 147 0 0 25 0 1 0 480337210 67588096 15324 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16501 15324 603 41 0 16460 0
vsize: 66004
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 39662 0 0 0 15831 149 0 0 25 0 1 0 480337210 69492736 15790 4294967295 134512640 134672761 3221224576 3221223760 134615996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16966 15790 603 41 0 16925 0
vsize: 67864
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 40070 0 0 0 16831 150 0 0 25 0 1 0 480337210 71168000 16198 4294967295 134512640 134672761 3221224576 3221223760 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17375 16198 603 41 0 17334 0
vsize: 69500
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 40524 0 0 0 17830 151 0 0 25 0 1 0 480337210 73134080 16652 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17855 16652 603 41 0 17814 0
vsize: 71420
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 40940 0 0 0 18829 152 0 0 25 0 1 0 480337210 74817536 17068 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18266 17068 603 41 0 18225 0
vsize: 73064
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 41315 0 0 0 19828 153 0 0 25 0 1 0 480337210 76259328 17443 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18618 17443 603 41 0 18577 0
vsize: 74472
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 41699 0 0 0 20827 155 0 0 25 0 1 0 480337210 77824000 17827 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19000 17827 603 41 0 18959 0
vsize: 76000
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 21809 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 22809 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 23809 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 24809 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 25810 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 26810 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 27810 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46342 0 0 0 28810 172 0 0 25 0 1 0 480337210 78168064 17921 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19084 17921 603 41 0 19043 0
vsize: 76336
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46481 0 0 0 29810 173 0 0 25 0 1 0 480337210 78823424 18060 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19244 18060 603 41 0 19203 0
vsize: 76976
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 46874 0 0 0 30809 173 0 0 25 0 1 0 480337210 80355328 18453 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19618 18453 603 41 0 19577 0
vsize: 78472
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 47343 0 0 0 31808 174 0 0 25 0 1 0 480337210 82313216 18922 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20096 18922 603 41 0 20055 0
vsize: 80384
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 47491 0 0 0 32808 175 0 0 25 0 1 0 480337210 82976768 19070 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20258 19070 603 41 0 20217 0
vsize: 81032
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 51792 0 0 0 33793 190 0 0 25 0 1 0 480337210 84836352 19354 4294967295 134512640 134672761 3221224576 3221223296 134542427 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20712 19354 603 41 0 20671 0
vsize: 82848
[startup+350.002 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 34791 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+360.002 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 35791 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+370.002 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 36791 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+380.002 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 37791 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+390.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 38791 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+400.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 39792 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+410.003 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 40792 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+420.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 41792 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+430.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 42792 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+440.004 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 43792 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+450.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 44793 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+460.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 45794 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+470.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52212 0 0 0 46794 192 0 0 25 0 1 0 480337210 83492864 19221 4294967295 134512640 134672761 3221224576 3221223744 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20384 19221 603 41 0 20343 0
vsize: 81536
[startup+480.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52245 0 0 0 47794 192 0 0 25 0 1 0 480337210 83755008 19254 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19254 603 41 0 20407 0
vsize: 81792
[startup+490.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52246 0 0 0 48794 192 0 0 25 0 1 0 480337210 83755008 19255 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19255 603 41 0 20407 0
vsize: 81792
[startup+500.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52247 0 0 0 49795 192 0 0 25 0 1 0 480337210 83755008 19256 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19256 603 41 0 20407 0
vsize: 81792
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52247 0 0 0 50795 192 0 0 25 0 1 0 480337210 83755008 19256 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19256 603 41 0 20407 0
vsize: 81792
[startup+520.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52248 0 0 0 51795 192 0 0 25 0 1 0 480337210 83755008 19257 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19257 603 41 0 20407 0
vsize: 81792
[startup+530.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52249 0 0 0 52795 192 0 0 25 0 1 0 480337210 83755008 19258 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19258 603 41 0 20407 0
vsize: 81792
[startup+540.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52250 0 0 0 53796 192 0 0 25 0 1 0 480337210 83755008 19259 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19259 603 41 0 20407 0
vsize: 81792
[startup+550.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52250 0 0 0 54796 192 0 0 25 0 1 0 480337210 83755008 19259 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19259 603 41 0 20407 0
vsize: 81792
[startup+560.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52251 0 0 0 55796 192 0 0 25 0 1 0 480337210 83755008 19260 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19260 603 41 0 20407 0
vsize: 81792
[startup+570.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 52670 0 0 0 56795 194 0 0 25 0 1 0 480337210 85557248 19679 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20888 19679 603 41 0 20847 0
vsize: 83552
[startup+580.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 53020 0 0 0 57793 195 0 0 25 0 1 0 480337210 86953984 20029 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21229 20029 603 41 0 21188 0
vsize: 84916
[startup+590.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 53262 0 0 0 58794 196 0 0 25 0 1 0 480337210 87994368 20271 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21483 20271 603 41 0 21442 0
vsize: 85932
[startup+600.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 53412 0 0 0 59794 197 0 0 25 0 1 0 480337210 88518656 20421 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21611 20421 603 41 0 21570 0
vsize: 86444
[startup+610.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 53601 0 0 0 60793 197 0 0 25 0 1 0 480337210 89313280 20610 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21805 20610 603 41 0 21764 0
vsize: 87220
[startup+620.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 53750 0 0 0 61793 198 0 0 25 0 1 0 480337210 89976832 20759 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21967 20759 603 41 0 21926 0
vsize: 87868
[startup+630.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 53963 0 0 0 62793 198 0 0 25 0 1 0 480337210 90877952 20972 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22187 20972 603 41 0 22146 0
vsize: 88748
[startup+640.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 54081 0 0 0 63792 199 0 0 25 0 1 0 480337210 91275264 21090 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22284 21090 603 41 0 22243 0
vsize: 89136
[startup+650.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 54239 0 0 0 64792 199 0 0 25 0 1 0 480337210 91930624 21248 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22444 21248 603 41 0 22403 0
vsize: 89776
[startup+660.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 54458 0 0 0 65791 200 0 0 25 0 1 0 480337210 92844032 21467 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22667 21467 603 41 0 22626 0
vsize: 90668
[startup+670.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 54762 0 0 0 66791 201 0 0 25 0 1 0 480337210 94019584 21771 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22954 21771 603 41 0 22913 0
vsize: 91816
[startup+680.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 55028 0 0 0 67790 202 0 0 25 0 1 0 480337210 95178752 22037 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23237 22037 603 41 0 23196 0
vsize: 92948
[startup+690.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 55229 0 0 0 68790 203 0 0 25 0 1 0 480337210 95952896 22238 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23426 22238 603 41 0 23385 0
vsize: 93704
[startup+700.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 55397 0 0 0 69789 203 0 0 25 0 1 0 480337210 96735232 22406 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23617 22406 603 41 0 23576 0
vsize: 94468
[startup+710.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 55629 0 0 0 70789 204 0 0 25 0 1 0 480337210 97648640 22638 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23840 22638 603 41 0 23799 0
vsize: 95360
[startup+720.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 55866 0 0 0 71788 204 0 0 25 0 1 0 480337210 98566144 22875 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24064 22875 603 41 0 24023 0
vsize: 96256
[startup+730.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56137 0 0 0 72788 205 0 0 25 0 1 0 480337210 99758080 23146 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24355 23146 603 41 0 24314 0
vsize: 97420
[startup+740.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56267 0 0 0 73787 206 0 0 25 0 1 0 480337210 100286464 23276 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24484 23276 603 41 0 24443 0
vsize: 97936
[startup+750.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56354 0 0 0 74787 206 0 0 25 0 1 0 480337210 100552704 23363 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24549 23363 603 41 0 24508 0
vsize: 98196
[startup+760.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56425 0 0 0 75787 207 0 0 25 0 1 0 480337210 100814848 23434 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24613 23434 603 41 0 24572 0
vsize: 98452
[startup+770.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56493 0 0 0 76787 207 0 0 25 0 1 0 480337210 101208064 23502 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24709 23502 603 41 0 24668 0
vsize: 98836
[startup+780.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56560 0 0 0 77787 207 0 0 25 0 1 0 480337210 101470208 23569 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24773 23569 603 41 0 24732 0
vsize: 99092
[startup+790.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56638 0 0 0 78787 207 0 0 25 0 1 0 480337210 101732352 23647 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24837 23647 603 41 0 24796 0
vsize: 99348
[startup+800.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56773 0 0 0 79786 208 0 0 25 0 1 0 480337210 102260736 23782 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24966 23782 603 41 0 24925 0
vsize: 99864
[startup+810.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56852 0 0 0 80786 208 0 0 25 0 1 0 480337210 102653952 23861 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25062 23861 603 41 0 25021 0
vsize: 100248
[startup+820.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 56974 0 0 0 81786 209 0 0 25 0 1 0 480337210 103178240 23983 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25190 23983 603 41 0 25149 0
vsize: 100760
[startup+830.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 57097 0 0 0 82786 209 0 0 25 0 1 0 480337210 103575552 24106 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25287 24106 603 41 0 25246 0
vsize: 101148
[startup+840.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 57223 0 0 0 83785 210 0 0 25 0 1 0 480337210 104108032 24232 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25417 24232 603 41 0 25376 0
vsize: 101668
[startup+850.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 57343 0 0 0 84785 210 0 0 25 0 1 0 480337210 104632320 24352 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25545 24352 603 41 0 25504 0
vsize: 102180
[startup+860.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 57452 0 0 0 85785 210 0 0 25 0 1 0 480337210 105025536 24461 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25641 24461 603 41 0 25600 0
vsize: 102564
[startup+870.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 57728 0 0 0 86785 211 0 0 25 0 1 0 480337210 106221568 24737 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25933 24737 603 41 0 25892 0
vsize: 103732
[startup+880.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 57845 0 0 0 87784 212 0 0 25 0 1 0 480337210 106631168 24854 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26033 24854 603 41 0 25992 0
vsize: 104132
[startup+890.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 57943 0 0 0 88784 212 0 0 25 0 1 0 480337210 107028480 24952 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26130 24952 603 41 0 26089 0
vsize: 104520
[startup+900.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 58024 0 0 0 89784 213 0 0 25 0 1 0 480337210 107425792 25033 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26227 25033 603 41 0 26186 0
vsize: 104908
[startup+910.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 58124 0 0 0 90784 213 0 0 25 0 1 0 480337210 107823104 25133 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26324 25133 603 41 0 26283 0
vsize: 105296
[startup+920.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 58278 0 0 0 91783 213 0 0 25 0 1 0 480337210 108486656 25287 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26486 25287 603 41 0 26445 0
vsize: 105944
[startup+930.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 58610 0 0 0 92782 214 0 0 25 0 1 0 480337210 109801472 25619 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26807 25619 603 41 0 26766 0
vsize: 107228
[startup+940.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 58747 0 0 0 93782 215 0 0 25 0 1 0 480337210 110354432 25756 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26942 25756 603 41 0 26901 0
vsize: 107768
[startup+950.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 58948 0 0 0 94782 215 0 0 25 0 1 0 480337210 111202304 25957 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27149 25957 603 41 0 27108 0
vsize: 108596
[startup+960.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 59354 0 0 0 95781 216 0 0 25 0 1 0 480337210 112881664 26363 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27559 26363 603 41 0 27518 0
vsize: 110236
[startup+970.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 59744 0 0 0 96781 217 0 0 25 0 1 0 480337210 114417664 26753 4294967295 134512640 134672761 3221224576 3221223584 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27934 26753 603 41 0 27893 0
vsize: 111736
[startup+980.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 59968 0 0 0 97780 218 0 0 25 0 1 0 480337210 115580928 26977 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28218 26977 603 41 0 28177 0
vsize: 112872
[startup+990.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 60631 0 0 0 98779 219 0 0 25 0 1 0 480337210 118358016 27640 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28896 27640 603 41 0 28855 0
vsize: 115584
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 61131 0 0 0 99778 220 0 0 25 0 1 0 480337210 120360960 28140 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29385 28140 603 41 0 29344 0
vsize: 117540
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 61607 0 0 0 100776 222 0 0 25 0 1 0 480337210 122281984 28616 4294967295 134512640 134672761 3221224576 3221223616 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29854 28616 603 41 0 29813 0
vsize: 119416
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 62075 0 0 0 101774 223 0 0 25 0 1 0 480337210 124243968 29084 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30333 29084 603 41 0 30292 0
vsize: 121332
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 62674 0 0 0 102773 225 0 0 25 0 1 0 480337210 126693376 29683 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30931 29683 603 41 0 30890 0
vsize: 123724
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 63263 0 0 0 103770 227 0 0 25 0 1 0 480337210 129110016 30272 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31521 30272 603 41 0 31480 0
vsize: 126084
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 63380 0 0 0 104770 228 0 0 25 0 1 0 480337210 129507328 30389 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31618 30389 603 41 0 31577 0
vsize: 126472
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 63516 0 0 0 105769 228 0 0 25 0 1 0 480337210 130162688 30525 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31778 30525 603 41 0 31737 0
vsize: 127112
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 63631 0 0 0 106769 229 0 0 25 0 1 0 480337210 130560000 30640 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31875 30640 603 41 0 31834 0
vsize: 127500
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 63793 0 0 0 107768 230 0 0 25 0 1 0 480337210 131223552 30802 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32037 30802 603 41 0 31996 0
vsize: 128148
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 64003 0 0 0 108768 230 0 0 25 0 1 0 480337210 132141056 31012 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32261 31012 603 41 0 32220 0
vsize: 129044
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 64222 0 0 0 109767 231 0 0 25 0 1 0 480337210 132923392 31231 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32452 31231 603 41 0 32411 0
vsize: 129808
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 64470 0 0 0 110766 232 0 0 25 0 1 0 480337210 133963776 31479 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32706 31479 603 41 0 32665 0
vsize: 130824
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 64653 0 0 0 111766 232 0 0 25 0 1 0 480337210 134750208 31662 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32898 31662 603 41 0 32857 0
vsize: 131592
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 64904 0 0 0 112766 233 0 0 25 0 1 0 480337210 135802880 31913 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33155 31913 603 41 0 33114 0
vsize: 132620
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 65149 0 0 0 113765 234 0 0 25 0 1 0 480337210 136716288 32158 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33378 32158 603 41 0 33337 0
vsize: 133512
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 65476 0 0 0 114764 235 0 0 25 0 1 0 480337210 138158080 32485 4294967295 134512640 134672761 3221224576 3221223580 134619842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33730 32485 603 41 0 33689 0
vsize: 134920
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 65743 0 0 0 115764 236 0 0 25 0 1 0 480337210 139210752 32752 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33987 32752 603 41 0 33946 0
vsize: 135948
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 65850 0 0 0 116764 236 0 0 25 0 1 0 480337210 139612160 32859 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34085 32859 603 41 0 34044 0
vsize: 136340
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 65946 0 0 0 117764 236 0 0 25 0 1 0 480337210 140001280 32955 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34180 32955 603 41 0 34139 0
vsize: 136720
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 65999 0 0 0 118764 236 0 0 25 0 1 0 480337210 140263424 33008 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34244 33008 603 41 0 34203 0
vsize: 136976
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32302
Raw data (stat): 32302 (minisat+) R 32301 28099 28098 0 -1 0 66110 0 0 0 119764 236 0 0 25 0 1 0 480337210 140640256 33119 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34336 33119 603 41 0 34295 0
vsize: 137344
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 32302
Raw data (stat): 32302 (minisat+) Z 32301 28099 28098 0 -1 12 66111 0 0 0 119764 244 0 0 25 0 1 0 480337210 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.09
CPU user time (s): 1197.64
CPU system time (s): 2.44363
CPU usage (%): 99.9973
Max. virtual memory (Kb): 137344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####