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-jac3.opb
MD5SUM	43952ea8e0659c6ffd861c99c0b605de
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	15
Optimality of the best value was proved	NO
Number of terms in the objective function	1732
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	1732
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	1732
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.05384
Number of variables	1731
Total number of constraints	1254
Number of constraints which are clauses	1254
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	694
Trace number 5423

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-13 23:52:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3830 boxname=wulflinc9 idbench=70 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  43952ea8e0659c6ffd861c99c0b605de  /oldhome/oroussel/tmp/wulflinc9/normalized-jac3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc9/normalized-jac3.opb /oldhome/oroussel/tmp/wulflinc9/normalized-jac3.opb
IDLAUNCH: 3830
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        907356 kB
Buffers:         34540 kB
Cached:          72880 kB
SwapCached:        564 kB
Active:          52520 kB
Inactive:        58352 kB
HighTotal:      131008 kB
HighFree:        54180 kB
LowTotal:       903652 kB
LowFree:        853176 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10908 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:12:38 (client local time) WITH STATUS 10 IN 1210.07 SECONDS
stats: 3830 7 1210.07 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1254 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 |    1248    23981 |     374       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  932/932          
c |         0 |    1246    23157 |      --       0       --      -- |     --   | -2/-824
c |         0 |    1246    23157 |     498       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.774882 s)
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:97868     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |  110228   277291 |   33068       1       48    48.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/73338          
c   -- var.elim.:  2000/73338          
c   -- var.elim.:  3000/73338          
c   -- var.elim.:  4000/73338          
c   -- var.elim.:  5000/73338          
c   -- var.elim.:  6000/73338          
c   -- var.elim.:  7000/73338          
c   -- var.elim.:  8000/73338          
c   -- var.elim.:  9000/73338          
c   -- var.elim.:  10000/73338          
c   -- var.elim.:  11000/73338          
c   -- var.elim.:  12000/73338          
c   -- var.elim.:  13000/73338          
c   -- var.elim.:  14000/73338          
c   -- var.elim.:  15000/73338          
c   -- var.elim.:  16000/73338          
c   -- var.elim.:  17000/73338          
c   -- var.elim.:  18000/73338          
c   -- var.elim.:  19000/73338          
c   -- var.elim.:  20000/73338          
c   -- var.elim.:  21000/73338          
c   -- var.elim.:  22000/73338          
c   -- var.elim.:  23000/73338          
c   -- var.elim.:  24000/73338          
c   -- var.elim.:  25000/73338          
c   -- var.elim.:  26000/73338          
c   -- var.elim.:  27000/73338          
c   -- var.elim.:  28000/73338          
c   -- var.elim.:  29000/73338          
c   -- var.elim.:  30000/73338          
c   -- var.elim.:  31000/73338          
c   -- var.elim.:  32000/73338          
c   -- var.elim.:  33000/73338          
c   -- var.elim.:  34000/73338          
c   -- var.elim.:  35000/73338          
c   -- var.elim.:  36000/73338          
c   -- var.elim.:  37000/73338          
c   -- var.elim.:  38000/73338          
c   -- var.elim.:  39000/73338          
c   -- var.elim.:  40000/73338          
c   -- var.elim.:  41000/73338          
c   -- var.elim.:  42000/73338          
c   -- var.elim.:  43000/73338          
c   -- var.elim.:  44000/73338          
c   -- var.elim.:  45000/73338          
c   -- var.elim.:  46000/73338          
c   -- var.elim.:  47000/73338          
c   -- var.elim.:  48000/73338          
c   -- var.elim.:  49000/73338          
c   -- var.elim.:  50000/73338          
c   -- var.elim.:  51000/73338          
c   -- var.elim.:  52000/73338          
c   -- var.elim.:  53000/73338          
c   -- var.elim.:  54000/73338          
c   -- var.elim.:  55000/73338          
c   -- var.elim.:  56000/73338          
c   -- var.elim.:  57000/73338          
c   -- var.elim.:  58000/73338          
c   -- var.elim.:  59000/73338          
c   -- var.elim.:  60000/73338          
c   -- var.elim.:  61000/73338          
c   -- var.elim.:  62000/73338          
c   -- var.elim.:  63000/73338          
c   -- var.elim.:  64000/73338          
c   -- var.elim.:  65000/73338          
c   -- var.elim.:  66000/73338          
c   -- var.elim.:  67000/73338          
c   -- var.elim.:  68000/73338          
c   -- var.elim.:  69000/73338          
c   -- var.elim.:  70000/73338          
c   -- var.elim.:  71000/73338          
c   -- var.elim.:  72000/73338          
c   -- var.elim.:  73000/73338          
c   -- var.elim.:  73338/73338          
c   -- var.elim.:  1000/36512          
c   -- var.elim.:  2000/36512          
c   -- var.elim.:  3000/36512          
c   -- var.elim.:  4000/36512          
c   -- var.elim.:  5000/36512          
c   -- var.elim.:  6000/36512          
c   -- var.elim.:  7000/36512          
c   -- var.elim.:  8000/36512          
c   -- var.elim.:  9000/36512          
c   -- var.elim.:  10000/36512          
c   -- var.elim.:  11000/36512          
c   -- var.elim.:  12000/36512          
c   -- var.elim.:  13000/36512          
c   -- var.elim.:  14000/36512          
c   -- var.elim.:  15000/36512          
c   -- var.elim.:  16000/36512          
c   -- var.elim.:  17000/36512          
c   -- var.elim.:  18000/36512          
c   -- var.elim.:  19000/36512          
c   -- var.elim.:  20000/36512          
c   -- var.elim.:  21000/36512          
c   -- var.elim.:  22000/36512          
c   -- var.elim.:  23000/36512          
c   -- var.elim.:  24000/36512          
c   -- var.elim.:  25000/36512          
c   -- var.elim.:  26000/36512          
c   -- var.elim.:  27000/36512          
c   -- var.elim.:  28000/36512          
c   -- var.elim.:  29000/36512          
c   -- var.elim.:  30000/36512          
c   -- var.elim.:  31000/36512          
c   -- var.elim.:  32000/36512          
c   -- var.elim.:  33000/36512          
c   -- var.elim.:  34000/36512          
c   -- var.elim.:  35000/36512          
c   -- var.elim.:  36000/36512          
c   -- var.elim.:  36512/36512          
c   -- subsuming                       
c   -- var.elim.:  1000/31265          
c   -- var.elim.:  2000/31265          
c   -- var.elim.:  3000/31265          
c   -- var.elim.:  4000/31265          
c   -- var.elim.:  5000/31265          
c   -- var.elim.:  6000/31265          
c   -- var.elim.:  7000/31265          
c   -- var.elim.:  8000/31265          
c   -- var.elim.:  9000/31265          
c   -- var.elim.:  10000/31265          
c   -- var.elim.:  11000/31265          
c   -- var.elim.:  12000/31265          
c   -- var.elim.:  13000/31265          
c   -- var.elim.:  14000/31265          
c   -- var.elim.:  15000/31265          
c   -- var.elim.:  16000/31265          
c   -- var.elim.:  17000/31265          
c   -- var.elim.:  18000/31265          
c   -- var.elim.:  19000/31265          
c   -- var.elim.:  20000/31265          
c   -- var.elim.:  21000/31265          
c   -- var.elim.:  22000/31265          
c   -- var.elim.:  23000/31265          
c   -- var.elim.:  24000/31265          
c   -- var.elim.:  25000/31265          
c   -- var.elim.:  26000/31265          
c   -- var.elim.:  27000/31265          
c   -- var.elim.:  28000/31265          
c   -- var.elim.:  29000/31265          
c   -- var.elim.:  30000/31265          
c   -- var.elim.:  31000/31265          
c   -- var.elim.:  31265/31265          
c   -- var.elim.:  56/56          
c |         1 |   74287   608034 |      --       1       --      -- |     --   | -35910/330836
c |         1 |   74287   608034 |   29714       1       48    48.0 |  0.000 % |
c |       103 |   74249   607407 |   32669     102    13301   130.4 |  0.107 % |
c |       254 |   74249   607407 |   35936     253    55628   219.9 |  0.107 % |
c ==============================================================================
c (current CPU-time: 196.711 s)
c ==============================================================================
c [1mFound solution: 20[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 |       285 |   75165   609889 |   22549     284    60392   212.6 |  0.107 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24797          
c   -- var.elim.:  2000/24797          
c   -- var.elim.:  3000/24797          
c   -- var.elim.:  4000/24797          
c   -- var.elim.:  5000/24797          
c   -- var.elim.:  6000/24797          
c   -- var.elim.:  7000/24797          
c   -- var.elim.:  8000/24797          
c   -- var.elim.:  9000/24797          
c   -- var.elim.:  10000/24797          
c   -- var.elim.:  11000/24797          
c   -- var.elim.:  12000/24797          
c   -- var.elim.:  13000/24797          
c   -- var.elim.:  14000/24797          
c   -- var.elim.:  15000/24797          
c   -- var.elim.:  16000/24797          
c   -- var.elim.:  17000/24797          
c   -- var.elim.:  18000/24797          
c   -- var.elim.:  19000/24797          
c   -- var.elim.:  20000/24797          
c   -- var.elim.:  21000/24797          
c   -- var.elim.:  22000/24797          
c   -- var.elim.:  23000/24797          
c   -- var.elim.:  24000/24797          
c   -- var.elim.:  24797/24797          
c   -- var.elim.:  1000/23200          
c   -- var.elim.:  2000/23200          
c   -- var.elim.:  3000/23200          
c   -- var.elim.:  4000/23200          
c   -- var.elim.:  5000/23200          
c   -- var.elim.:  6000/23200          
c   -- var.elim.:  7000/23200          
c   -- var.elim.:  8000/23200          
c   -- var.elim.:  9000/23200          
c   -- var.elim.:  10000/23200          
c   -- var.elim.:  11000/23200          
c   -- var.elim.:  12000/23200          
c   -- var.elim.:  13000/23200          
c   -- var.elim.:  14000/23200          
c   -- var.elim.:  15000/23200          
c   -- var.elim.:  16000/23200          
c   -- var.elim.:  17000/23200          
c   -- var.elim.:  18000/23200          
c   -- var.elim.:  19000/23200          
c   -- var.elim.:  20000/23200          
c   -- var.elim.:  21000/23200          
c   -- var.elim.:  22000/23200          
c   -- var.elim.:  23000/23200          
c   -- var.elim.:  23200/23200          
c   -- var.elim.:  1000/6718          
c   -- var.elim.:  2000/6718          
c   -- var.elim.:  3000/6718          
c   -- var.elim.:  4000/6718          
c   -- var.elim.:  5000/6718          
c   -- var.elim.:  6000/6718          
c   -- var.elim.:  6718/6718          
c   -- var.elim.:  1000/4821          
c   -- var.elim.:  2000/4821          
c   -- var.elim.:  3000/4821          
c   -- var.elim.:  4000/4821          
c   -- var.elim.:  4821/4821          
c   -- var.elim.:  1000/3606          
c   -- var.elim.:  2000/3606          
c   -- var.elim.:  3000/3606          
c   -- var.elim.:  3606/3606          
c   -- var.elim.:  1000/1892          
c   -- var.elim.:  1892/1892          
c   -- subsuming                       
c   -- var.elim.:  1000/6440          
c   -- var.elim.:  2000/6440          
c   -- var.elim.:  3000/6440          
c   -- var.elim.:  4000/6440          
c   -- var.elim.:  5000/6440          
c   -- var.elim.:  6000/6440          
c   -- var.elim.:  6440/6440          
c   -- var.elim.:  356/356          
c |       285 |   58320   381752 |      --     284       --      -- |     --   | -9242/-12455
c |       285 |   58320   381752 |   23328     258    55643   215.7 |  0.107 % |
c |       385 |   58320   381752 |   25660     358    89249   249.3 |  5.809 % |
c |       535 |   58320   381752 |   28226     508   130656   257.2 |  5.809 % |
c |       761 |   58320   381752 |   31049     734   180867   246.4 |  5.809 % |
c |      1098 |   58320   381752 |   34154    1071   284781   265.9 |  5.809 % |
c |      1604 |   58320   381752 |   37569    1577   604462   383.3 |  5.809 % |
c |      2365 |   58320   381752 |   41326    2338  1129844   483.3 |  5.809 % |
c |      3505 |   58320   381752 |   45459    3478  1459010   419.5 |  5.809 % |
c |      5214 |   58289   381541 |   49979    5183  2504361   483.2 |  5.839 % |
c |      7778 |   58289   381541 |   54976    7747  3737676   482.5 |  5.839 % |
c ==============================================================================
c (current CPU-time: 252.075 s)
c ==============================================================================
c [1mFound solution: 17[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 |      8406 |  101644   498998 |   30493    8375  3963341   473.2 |  5.839 % |
c   -- subsuming                       
c   -- var.elim.:  1000/61890          
c   -- var.elim.:  2000/61890          
c   -- var.elim.:  3000/61890          
c   -- var.elim.:  4000/61890          
c   -- var.elim.:  5000/61890          
c   -- var.elim.:  6000/61890          
c   -- var.elim.:  7000/61890          
c   -- var.elim.:  8000/61890          
c   -- var.elim.:  9000/61890          
c   -- var.elim.:  10000/61890          
c   -- var.elim.:  11000/61890          
c   -- var.elim.:  12000/61890          
c   -- var.elim.:  13000/61890          
c   -- var.elim.:  14000/61890          
c   -- var.elim.:  15000/61890          
c   -- var.elim.:  16000/61890          
c   -- var.elim.:  17000/61890          
c   -- var.elim.:  18000/61890          
c   -- var.elim.:  19000/61890          
c   -- var.elim.:  20000/61890          
c   -- var.elim.:  21000/61890          
c   -- var.elim.:  22000/61890          
c   -- var.elim.:  23000/61890          
c   -- var.elim.:  24000/61890          
c   -- var.elim.:  25000/61890          
c   -- var.elim.:  26000/61890          
c   -- var.elim.:  27000/61890          
c   -- var.elim.:  28000/61890          
c   -- var.elim.:  29000/61890          
c   -- var.elim.:  30000/61890          
c   -- var.elim.:  31000/61890          
c   -- var.elim.:  32000/61890          
c   -- var.elim.:  33000/61890          
c   -- var.elim.:  34000/61890          
c   -- var.elim.:  35000/61890          
c   -- var.elim.:  36000/61890          
c   -- var.elim.:  37000/61890          
c   -- var.elim.:  38000/61890          
c   -- var.elim.:  39000/61890          
c   -- var.elim.:  40000/61890          
c   -- var.elim.:  41000/61890          
c   -- var.elim.:  42000/61890          
c   -- var.elim.:  43000/61890          
c   -- var.elim.:  44000/61890          
c   -- var.elim.:  45000/61890          
c   -- var.elim.:  46000/61890          
c   -- var.elim.:  47000/61890          
c   -- var.elim.:  48000/61890          
c   -- var.elim.:  49000/61890          
c   -- var.elim.:  50000/61890          
c   -- var.elim.:  51000/61890          
c   -- var.elim.:  52000/61890          
c   -- var.elim.:  53000/61890          
c   -- var.elim.:  54000/61890          
c   -- var.elim.:  55000/61890          
c   -- var.elim.:  56000/61890          
c   -- var.elim.:  57000/61890          
c   -- var.elim.:  58000/61890          
c   -- var.elim.:  59000/61890          
c   -- var.elim.:  60000/61890          
c   -- var.elim.:  61000/61890          
c   -- var.elim.:  61890/61890          
c   -- var.elim.:  1000/32214          
c   -- var.elim.:  2000/32214          
c   -- var.elim.:  3000/32214          
c   -- var.elim.:  4000/32214          
c   -- var.elim.:  5000/32214          
c   -- var.elim.:  6000/32214          
c   -- var.elim.:  7000/32214          
c   -- var.elim.:  8000/32214          
c   -- var.elim.:  9000/32214          
c   -- var.elim.:  10000/32214          
c   -- var.elim.:  11000/32214          
c   -- var.elim.:  12000/32214          
c   -- var.elim.:  13000/32214          
c   -- var.elim.:  14000/32214          
c   -- var.elim.:  15000/32214          
c   -- var.elim.:  16000/32214          
c   -- var.elim.:  17000/32214          
c   -- var.elim.:  18000/32214          
c   -- var.elim.:  19000/32214          
c   -- var.elim.:  20000/32214          
c   -- var.elim.:  21000/32214          
c   -- var.elim.:  22000/32214          
c   -- var.elim.:  23000/32214          
c   -- var.elim.:  24000/32214          
c   -- var.elim.:  25000/32214          
c   -- var.elim.:  26000/32214          
c   -- var.elim.:  27000/32214          
c   -- var.elim.:  28000/32214          
c   -- var.elim.:  29000/32214          
c   -- var.elim.:  30000/32214          
c   -- var.elim.:  31000/32214          
c   -- var.elim.:  32000/32214          
c   -- var.elim.:  32214/32214          
c   -- var.elim.:  1000/25678          
c   -- var.elim.:  2000/25678          
c   -- var.elim.:  3000/25678          
c   -- var.elim.:  4000/25678          
c   -- var.elim.:  5000/25678          
c   -- var.elim.:  6000/25678          
c   -- var.elim.:  7000/25678          
c   -- var.elim.:  8000/25678          
c   -- var.elim.:  9000/25678          
c   -- var.elim.:  10000/25678          
c   -- var.elim.:  11000/25678          
c   -- var.elim.:  12000/25678          
c   -- var.elim.:  13000/25678          
c   -- var.elim.:  14000/25678          
c   -- var.elim.:  15000/25678          
c   -- var.elim.:  16000/25678          
c   -- var.elim.:  17000/25678          
c   -- var.elim.:  18000/25678          
c   -- var.elim.:  19000/25678          
c   -- var.elim.:  20000/25678          
c   -- var.elim.:  21000/25678          
c   -- var.elim.:  22000/25678          
c   -- var.elim.:  23000/25678          
c   -- var.elim.:  24000/25678          
c   -- var.elim.:  25000/25678          
c   -- var.elim.:  25678/25678          
c   -- var.elim.:  1000/18436          
c   -- var.elim.:  2000/18436          
c   -- var.elim.:  3000/18436          
c   -- var.elim.:  4000/18436          
c   -- var.elim.:  5000/18436          
c   -- var.elim.:  6000/18436          
c   -- var.elim.:  7000/18436          
c   -- var.elim.:  8000/18436          
c   -- var.elim.:  9000/18436          
c   -- var.elim.:  10000/18436          
c   -- var.elim.:  11000/18436          
c   -- var.elim.:  12000/18436          
c   -- var.elim.:  13000/18436          
c   -- var.elim.:  14000/18436          
c   -- var.elim.:  15000/18436          
c   -- var.elim.:  16000/18436          
c   -- var.elim.:  17000/18436          
c   -- var.elim.:  18000/18436          
c   -- var.elim.:  18436/18436          
c   -- var.elim.:  1000/7375          
c   -- var.elim.:  2000/7375          
c   -- var.elim.:  3000/7375          
c   -- var.elim.:  4000/7375          
c   -- var.elim.:  5000/7375          
c   -- var.elim.:  6000/7375          
c   -- var.elim.:  7000/7375          
c   -- var.elim.:  7375/7375          
c   -- var.elim.:  1000/5925          
c   -- var.elim.:  2000/5925          
c   -- var.elim.:  3000/5925          
c   -- var.elim.:  4000/5925          
c   -- var.elim.:  5000/5925          
c   -- var.elim.:  5925/5925          
c   -- var.elim.:  1000/2245          
c   -- var.elim.:  2000/2245          
c   -- var.elim.:  2245/2245          
c   -- var.elim.:  542/542          
c   -- subsuming                       
c   -- var.elim.:  790/790          
c   -- var.elim.:  262/262          
c |      8406 |   58581   384425 |      --    8375       --      -- |     --   | -43062/-114570
c |      8406 |   58581   384425 |   23432    8375  3963341   473.2 |  5.839 % |
c |      8506 |   58581   384425 |   25775    8475  3977029   469.3 |  5.702 % |
c |      8657 |   58581   384425 |   28353    8626  4012141   465.1 |  5.702 % |
c |      8885 |   58581   384425 |   31188    8854  4086072   461.5 |  5.702 % |
c |      9222 |   58581   384425 |   34307    9191  4193451   456.3 |  5.702 % |
c |      9731 |   58581   384425 |   37738    9700  4400036   453.6 |  5.702 % |
c |     10491 |   58581   384425 |   41511   10460  4981461   476.2 |  5.702 % |
c |     11630 |   58581   384425 |   45663   11599  5406860   466.1 |  5.702 % |
c |     13338 |   58581   384425 |   50229   13307  6381229   479.5 |  5.702 % |
c |     15900 |   58581   384425 |   55252   15869  7264353   457.8 |  5.702 % |
c |     19746 |   58581   384425 |   60777   19715  9968294   505.6 |  5.702 % |
c |     25512 |   58581   384425 |   66855   25481 12553835   492.7 |  5.702 % |
c |     34161 |   58581   384425 |   73540   34130 20048818   587.4 |  5.702 % |
c |     47136 |   58581   384425 |   80895   47105 24480038   519.7 |  5.702 % |
c |     66600 |   58581   384425 |   88984   66569 30853978   463.5 |  5.702 % |
c ==============================================================================
c (current CPU-time: 743.056 s)
c ==============================================================================
c [1mFound solution: 16[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 |     67647 |   58588   384442 |   17576   67616 31180343   461.1 |  5.702 % |
c   -- subsuming                       
c   -- var.elim.:  473/473          
c   -- var.elim.:  457/457          
c   -- subsuming                       
c   -- var.elim.:  60/60          
c   -- var.elim.:  112/112          
c |     67647 |   58515   384002 |      --   67616       --      -- |     --   | -18/-32
c |     67647 |   58515   384002 |   23406   51519 22060943   428.2 |  5.702 % |
c |     67749 |   58515   384002 |   25746   11682  2989785   255.9 |  5.747 % |
c |     67899 |   58515   384002 |   28321   11832  3044271   257.3 |  5.747 % |
c |     68125 |   58515   384002 |   31153   12058  3117606   258.6 |  5.747 % |
c |     68464 |   58515   384002 |   34268   12397  3185743   257.0 |  5.747 % |
c |     68971 |   58515   384002 |   37695   12904  3523138   273.0 |  5.747 % |
c |     69731 |   58515   384002 |   41465   13664  3768948   275.8 |  5.747 % |
c |     70871 |   58515   384002 |   45611   14804  4147986   280.2 |  5.747 % |
c |     72585 |   58515   384002 |   50172   16518  5090123   308.2 |  5.747 % |
c |     75151 |   58515   384002 |   55190   19084  6020626   315.5 |  5.747 % |
c |     78997 |   58515   384002 |   60709   22930  7803129   340.3 |  5.747 % |
c |     84763 |   58515   384002 |   66780   28696 10465011   364.7 |  5.747 % |
c |     93412 |   58515   384002 |   73458   37345 16569448   443.7 |  5.747 % |
c |    106386 |   58515   384002 |   80803   50319 23392689   464.9 |  5.747 % |
c |    125848 |   58515   384002 |   88884   69781 37269200   534.1 |  5.747 % |
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 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 #### 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.93 0.97 0.91 2/54 1384
Raw data (stat): 1384 (runsolver) R 1383 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421834914 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10761 0 0 0 957 41 0 0 25 0 1 0 421834914 50241536 10273 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12266 10273 603 41 0 12225 0
vsize: 49064
[startup+20.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10764 0 0 0 1957 41 0 0 25 0 1 0 421834914 50241536 10276 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12266 10276 603 41 0 12225 0
vsize: 49064
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10764 0 0 0 2957 41 0 0 25 0 1 0 421834914 50241536 10276 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12266 10276 603 41 0 12225 0
vsize: 49064
[startup+40.002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10978 0 0 0 3956 43 0 0 25 0 1 0 421834914 51032064 10418 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12459 10418 603 41 0 12418 0
vsize: 49836
[startup+50.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10978 0 0 0 4956 43 0 0 25 0 1 0 421834914 51032064 10418 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12459 10418 603 41 0 12418 0
vsize: 49836
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 5956 43 0 0 25 0 1 0 421834914 51032064 10421 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12459 10421 603 41 0 12418 0
vsize: 49836
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 6956 43 0 0 25 0 1 0 421834914 51032064 10421 4294967295 134512640 134672761 3221224576 3221223024 134643948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12459 10421 603 41 0 12418 0
vsize: 49836
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 7957 43 0 0 25 0 1 0 421834914 51032064 10421 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12459 10421 603 41 0 12418 0
vsize: 49836
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 8957 43 0 0 25 0 1 0 421834914 50245632 10337 4294967295 134512640 134672761 3221224576 3221223084 134642904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 10337 603 41 0 12226 0
vsize: 49068
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 9957 43 0 0 25 0 1 0 421834914 50245632 10337 4294967295 134512640 134672761 3221224576 3221222976 134604652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 10337 603 41 0 12226 0
vsize: 49068
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 10957 43 0 0 25 0 1 0 421834914 50245632 10337 4294967295 134512640 134672761 3221224576 3221222976 134604034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 10337 603 41 0 12226 0
vsize: 49068
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 11957 43 0 0 25 0 1 0 421834914 50245632 10337 4294967295 134512640 134672761 3221224576 3221223040 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 10337 603 41 0 12226 0
vsize: 49068
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 12958 43 0 0 25 0 1 0 421834914 50245632 10337 4294967295 134512640 134672761 3221224576 3221222976 134604658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 10337 603 41 0 12226 0
vsize: 49068
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 13958 43 0 0 25 0 1 0 421834914 50245632 10337 4294967295 134512640 134672761 3221224576 3221223120 134621090 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 10337 603 41 0 12226 0
vsize: 49068
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 10981 0 0 0 14958 43 0 0 25 0 1 0 421834914 50245632 10337 4294967295 134512640 134672761 3221224576 3221223120 134621049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12267 10337 603 41 0 12226 0
vsize: 49068
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 11089 0 0 0 15958 43 0 0 25 0 1 0 421834914 50892800 10445 4294967295 134512640 134672761 3221224576 3221223120 134621086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12425 10445 603 41 0 12384 0
vsize: 49700
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 11159 0 0 0 16958 43 0 0 25 0 1 0 421834914 50544640 10407 4294967295 134512640 134672761 3221224576 3221223024 134643688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12340 10407 603 41 0 12299 0
vsize: 49360
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 11159 0 0 0 17958 43 0 0 25 0 1 0 421834914 50544640 10407 4294967295 134512640 134672761 3221224576 3221223024 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12340 10407 603 41 0 12299 0
vsize: 49360
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 11159 0 0 0 18958 43 0 0 25 0 1 0 421834914 50544640 10407 4294967295 134512640 134672761 3221224576 3221223024 134643524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12340 10407 603 41 0 12299 0
vsize: 49360
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 13833 0 0 0 19946 55 0 0 25 0 1 0 421834914 52396032 10742 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12792 10742 603 41 0 12751 0
vsize: 51168
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 13838 0 0 0 20944 56 0 0 25 0 1 0 421834914 52396032 10747 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12792 10747 603 41 0 12751 0
vsize: 51168
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 14092 0 0 0 21943 57 0 0 25 0 1 0 421834914 52002816 10701 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12696 10701 603 41 0 12655 0
vsize: 50784
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 15114 0 0 0 22941 60 0 0 25 0 1 0 421834914 56217600 11723 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13725 11723 603 41 0 13684 0
vsize: 54900
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 15963 0 0 0 23939 62 0 0 25 0 1 0 421834914 59797504 12572 4294967295 134512640 134672761 3221224576 3221223616 134613120 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14599 12572 603 41 0 14558 0
vsize: 58396
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 17441 0 0 0 24936 65 0 0 25 0 1 0 421834914 65724416 14050 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16046 14050 603 41 0 16005 0
vsize: 64184
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22450 0 0 0 25860 115 0 0 25 0 1 0 421834914 71942144 16332 4294967295 134512640 134672761 3221224576 3221222968 1075280336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17564 16332 603 41 0 17523 0
vsize: 70256
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22463 0 0 0 26858 117 0 0 25 0 1 0 421834914 71942144 16345 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17564 16345 603 41 0 17523 0
vsize: 70256
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22463 0 0 0 27858 117 0 0 25 0 1 0 421834914 71942144 16345 4294967295 134512640 134672761 3221224576 3221222796 1075349878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17564 16345 603 41 0 17523 0
vsize: 70256
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22496 0 0 0 28857 118 0 0 25 0 1 0 421834914 71852032 16317 4294967295 134512640 134672761 3221224576 3221222976 134615266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17542 16317 603 41 0 17501 0
vsize: 70168
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22501 0 0 0 29854 121 0 0 25 0 1 0 421834914 71852032 16322 4294967295 134512640 134672761 3221224576 3221223024 134643959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17542 16322 603 41 0 17501 0
vsize: 70168
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22503 0 0 0 30854 122 0 0 25 0 1 0 421834914 71852032 16324 4294967295 134512640 134672761 3221224576 3221223024 134643963 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17542 16324 603 41 0 17501 0
vsize: 70168
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22503 0 0 0 31854 122 0 0 25 0 1 0 421834914 71852032 16324 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17542 16324 603 41 0 17501 0
vsize: 70168
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 22775 0 0 0 32853 123 0 0 25 0 1 0 421834914 71589888 16264 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17478 16264 603 41 0 17437 0
vsize: 69912
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 23722 0 0 0 33852 125 0 0 25 0 1 0 421834914 75513856 17211 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18436 17211 603 41 0 18395 0
vsize: 73744
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 25073 0 0 0 34848 128 0 0 25 0 1 0 421834914 81018880 18562 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19780 18562 603 41 0 19739 0
vsize: 79120
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 26520 0 0 0 35844 132 0 0 25 0 1 0 421834914 86962176 20009 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21231 20009 603 41 0 21190 0
vsize: 84924
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 28601 0 0 0 36840 137 0 0 25 0 1 0 421834914 95510528 22090 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23318 22090 603 41 0 23277 0
vsize: 93272
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 29705 0 0 0 37837 140 0 0 25 0 1 0 421834914 100110336 23194 4294967295 134512640 134672761 3221224576 3221223712 134614822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24441 23194 603 41 0 24400 0
vsize: 97764
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 30589 0 0 0 38835 143 0 0 25 0 1 0 421834914 103661568 24078 4294967295 134512640 134672761 3221224576 3221223760 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25308 24078 603 41 0 25267 0
vsize: 101232
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 31397 0 0 0 39833 144 0 0 25 0 1 0 421834914 106958848 24886 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26113 24886 603 41 0 26072 0
vsize: 104452
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 32660 0 0 0 40830 147 0 0 25 0 1 0 421834914 112111616 26149 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27371 26151 603 41 0 27330 0
vsize: 109484
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 34165 0 0 0 41828 150 0 0 25 0 1 0 421834914 118304768 27654 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28883 27654 603 41 0 28842 0
vsize: 115532
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 35582 0 0 0 42825 153 0 0 25 0 1 0 421834914 124088320 29071 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30295 29071 603 41 0 30254 0
vsize: 121180
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 36933 0 0 0 43822 157 0 0 25 0 1 0 421834914 129658880 30422 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31655 30422 603 41 0 31614 0
vsize: 126620
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1384
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 38313 0 0 0 44818 160 0 0 25 0 1 0 421834914 135458816 31802 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33071 31802 603 41 0 33030 0
vsize: 132284
[startup+460.019 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 1425
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 38937 0 0 0 45817 162 0 0 25 0 1 0 421834914 137949184 32426 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 32426 603 41 0 33638 0
vsize: 134716
[startup+470.019 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1437
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 39091 0 0 0 46817 162 0 0 25 0 1 0 421834914 138608640 32580 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32580 603 41 0 33799 0
vsize: 135360
[startup+480.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1437
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 39262 0 0 0 47816 163 0 0 25 0 1 0 421834914 139264000 32751 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34000 32751 603 41 0 33959 0
vsize: 136000
[startup+490.021 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1437
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 39607 0 0 0 48816 164 0 0 25 0 1 0 421834914 140726272 33096 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34357 33096 603 41 0 34316 0
vsize: 137428
[startup+500.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1437
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 40148 0 0 0 49814 165 0 0 25 0 1 0 421834914 142835712 33637 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34872 33637 603 41 0 34831 0
vsize: 139488
[startup+510.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1437
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 40382 0 0 0 50813 166 0 0 25 0 1 0 421834914 143908864 33871 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35134 33871 603 41 0 35093 0
vsize: 140536
[startup+520.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1437
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 40685 0 0 0 51812 168 0 0 25 0 1 0 421834914 145084416 34174 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35421 34174 603 41 0 35380 0
vsize: 141684
[startup+530.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1437
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 41077 0 0 0 52811 169 0 0 25 0 1 0 421834914 146677760 34566 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35810 34566 603 41 0 35769 0
vsize: 143240
[startup+540.021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 41332 0 0 0 53811 170 0 0 25 0 1 0 421834914 147738624 34821 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36069 34821 603 41 0 36028 0
vsize: 144276
[startup+550.021 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 41526 0 0 0 54810 171 0 0 25 0 1 0 421834914 148520960 35015 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36260 35015 603 41 0 36219 0
vsize: 145040
[startup+560.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 41779 0 0 0 55810 171 0 0 25 0 1 0 421834914 149573632 35268 4294967295 134512640 134672761 3221224576 3221223760 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36517 35268 603 41 0 36476 0
vsize: 146068
[startup+570.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 42237 0 0 0 56809 172 0 0 25 0 1 0 421834914 151412736 35726 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36966 35726 603 41 0 36925 0
vsize: 147864
[startup+580.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 42798 0 0 0 57807 174 0 0 25 0 1 0 421834914 153763840 36287 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37540 36287 603 41 0 37499 0
vsize: 150160
[startup+590.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 43305 0 0 0 58806 176 0 0 25 0 1 0 421834914 155738112 36794 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38022 36794 603 41 0 37981 0
vsize: 152088
[startup+600.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 43553 0 0 0 59805 177 0 0 25 0 1 0 421834914 156790784 37042 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38279 37042 603 41 0 38238 0
vsize: 153116
[startup+610.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 43920 0 0 0 60804 178 0 0 25 0 1 0 421834914 158371840 37409 4294967295 134512640 134672761 3221224576 3221223712 134614494 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38665 37409 603 41 0 38624 0
vsize: 154660
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 44184 0 0 0 61804 178 0 0 25 0 1 0 421834914 159424512 37673 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38922 37673 603 41 0 38881 0
vsize: 155688
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 44742 0 0 0 62802 180 0 0 25 0 1 0 421834914 161660928 38231 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39468 38231 603 41 0 39427 0
vsize: 157872
[startup+640.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 45189 0 0 0 63801 181 0 0 25 0 1 0 421834914 163516416 38678 4294967295 134512640 134672761 3221224576 3221223732 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39921 38678 603 41 0 39880 0
vsize: 159684
[startup+650.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 45725 0 0 0 64800 182 0 0 25 0 1 0 421834914 165629952 39214 4294967295 134512640 134672761 3221224576 3221223408 1075350401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40437 39214 603 41 0 40396 0
vsize: 161748
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 46162 0 0 0 65798 184 0 0 25 0 1 0 421834914 167477248 39651 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40888 39651 603 41 0 40847 0
vsize: 163552
[startup+670.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 46543 0 0 0 66797 186 0 0 25 0 1 0 421834914 169074688 40032 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41278 40032 603 41 0 41237 0
vsize: 165112
[startup+680.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 46886 0 0 0 67797 186 0 0 25 0 1 0 421834914 170389504 40375 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41599 40375 603 41 0 41558 0
vsize: 166396
[startup+690.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 47412 0 0 0 68796 187 0 0 25 0 1 0 421834914 172646400 40901 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42150 40901 603 41 0 42109 0
vsize: 168600
[startup+700.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 47920 0 0 0 69795 188 0 0 25 0 1 0 421834914 174616576 41409 4294967295 134512640 134672761 3221224576 3221223760 134615985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42631 41409 603 41 0 42590 0
vsize: 170524
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 48447 0 0 0 70795 189 0 0 25 0 1 0 421834914 176857088 41936 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43178 41936 603 41 0 43137 0
vsize: 172712
[startup+720.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 49027 0 0 0 71793 191 0 0 25 0 1 0 421834914 179232768 42516 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43758 42516 603 41 0 43717 0
vsize: 175032
[startup+730.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 49483 0 0 0 72792 192 0 0 25 0 1 0 421834914 181362688 42972 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44278 42972 603 41 0 44237 0
vsize: 177112
[startup+740.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 49815 0 0 0 73792 193 0 0 25 0 1 0 421834914 182689792 43304 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44602 43304 603 41 0 44561 0
vsize: 178408
[startup+750.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54467 0 0 0 74771 213 0 0 25 0 1 0 421834914 184094720 43666 4294967295 134512640 134672761 3221224576 3221223832 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44945 43666 603 41 0 44904 0
vsize: 179780
[startup+760.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54573 0 0 0 75771 213 0 0 25 0 1 0 421834914 184356864 43721 4294967295 134512640 134672761 3221224576 3221223776 134610528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43721 603 41 0 44968 0
vsize: 180036
[startup+770.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1439
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 76772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223616 134612739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+780.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 77772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+790.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 78772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+800.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 79772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+810.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 80772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+820.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 81773 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+830.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 82772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+840.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 83772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+850.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 84772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+860.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 85772 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+870.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 86773 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+880.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 87773 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+890.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 88773 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+900.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 89773 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+910.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 90773 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+920.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 91773 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+930.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 92774 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223776 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+940.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 93774 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+950.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 94774 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223616 134612797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+960.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 95774 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+970.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 96774 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+980.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 97775 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+990.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 98775 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 99775 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 100775 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54574 0 0 0 101775 213 0 0 25 0 1 0 421834914 184356864 43722 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45009 43722 603 41 0 44968 0
vsize: 180036
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 54807 0 0 0 102775 214 0 0 25 0 1 0 421834914 185430016 43955 4294967295 134512640 134672761 3221224576 3221223700 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45271 43955 603 41 0 45230 0
vsize: 181084
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 55556 0 0 0 103773 216 0 0 25 0 1 0 421834914 188477440 44704 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46015 44704 603 41 0 45974 0
vsize: 184060
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 56496 0 0 0 104771 218 0 0 25 0 1 0 421834914 192323584 45644 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46954 45644 603 41 0 46913 0
vsize: 187816
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 57394 0 0 0 105769 221 0 0 25 0 1 0 421834914 196009984 46542 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47854 46542 603 41 0 47813 0
vsize: 191416
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 58389 0 0 0 106767 223 0 0 25 0 1 0 421834914 200052736 47537 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48841 47537 603 41 0 48800 0
vsize: 195364
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 59259 0 0 0 107765 224 0 0 25 0 1 0 421834914 203599872 48407 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49707 48407 603 41 0 49666 0
vsize: 198828
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 60030 0 0 0 108764 226 0 0 25 0 1 0 421834914 206790656 49178 4294967295 134512640 134672761 3221224576 3221223616 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50486 49178 603 41 0 50445 0
vsize: 201944
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 60998 0 0 0 109762 228 0 0 25 0 1 0 421834914 210726912 50146 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51447 50146 603 41 0 51406 0
vsize: 205788
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 61332 0 0 0 110761 229 0 0 25 0 1 0 421834914 212062208 50480 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51773 50480 603 41 0 51732 0
vsize: 207092
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 61559 0 0 0 111761 230 0 0 25 0 1 0 421834914 212992000 50707 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52000 50707 603 41 0 51959 0
vsize: 208000
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 61762 0 0 0 112760 231 0 0 25 0 1 0 421834914 213913600 50910 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52225 50910 603 41 0 52184 0
vsize: 208900
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 62029 0 0 0 113760 231 0 0 25 0 1 0 421834914 214974464 51177 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52484 51177 603 41 0 52443 0
vsize: 209936
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 62293 0 0 0 114759 232 0 0 25 0 1 0 421834914 216031232 51441 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52742 51441 603 41 0 52701 0
vsize: 210968
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 63179 0 0 0 115757 234 0 0 25 0 1 0 421834914 219619328 52327 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53618 52327 603 41 0 53577 0
vsize: 214472
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 63790 0 0 0 116756 235 0 0 25 0 1 0 421834914 222117888 52938 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54228 52938 603 41 0 54187 0
vsize: 216912
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 64364 0 0 0 117755 237 0 0 25 0 1 0 421834914 224497664 53512 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54809 53512 603 41 0 54768 0
vsize: 219236
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 64879 0 0 0 118754 238 0 0 25 0 1 0 421834914 226607104 54027 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55324 54027 603 41 0 55283 0
vsize: 221296
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 65335 0 0 0 119753 239 0 0 25 0 1 0 421834914 228454400 54483 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55775 54483 603 41 0 55734 0
vsize: 223100
[startup+1210.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1441
Raw data (stat): 1384 (minisat+) R 1383 30854 30853 0 -1 0 65837 0 0 0 120752 240 0 0 25 0 1 0 421834914 230543360 54985 4294967295 134512640 134672761 3221224576 3221223728 134614555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56285 54985 603 41 0 56244 0
vsize: 225140
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.18 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1441
Raw data (stat): 1384 (minisat+) Z 1383 30854 30853 0 -1 12 65838 0 0 0 120753 254 0 0 25 0 1 0 421834914 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1210.18
CPU time (s): 1210.07
CPU user time (s): 1207.53
CPU system time (s): 2.54261
CPU usage (%): 99.9912
Max. virtual memory (Kb): 225140
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####