PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32e2.opb
MD5SUM	4e882bbd92f288daf6e68ac3de757136
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	235
Optimality of the best value was proved	NO
Number of terms in the objective function	534
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	534
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	534
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03084
Number of variables	534
Total number of constraints	3013
Number of constraints which are clauses	3013
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 5498

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 00:11:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3919 boxname=wulflinc2 idbench=159 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4e882bbd92f288daf6e68ac3de757136  /oldhome/oroussel/tmp/wulflinc2/normalized-ii32e2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-ii32e2.opb /oldhome/oroussel/tmp/wulflinc2/normalized-ii32e2.opb
IDLAUNCH: 3919
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        903388 kB
Buffers:         34052 kB
Cached:          76920 kB
SwapCached:          4 kB
Active:          56376 kB
Inactive:        57424 kB
HighTotal:      131008 kB
HighFree:        50400 kB
LowTotal:       903652 kB
LowFree:        852988 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11976 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:31:06 (client local time) WITH STATUS 10 IN 1200.11 SECONDS
stats: 3919 7 1200.11 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3013 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 |    3013    12801 |     903       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  534/534          
c |         0 |    3013    12801 |    1205       0        0     nan |  0.000 % |
c |       102 |    3013    12801 |    1325     102     4917    48.2 |  0.011 % |
c |       252 |    3013    12801 |    1458     252    13097    52.0 |  0.000 % |
c |       477 |    3013    12801 |    1604     477    27042    56.7 |  0.000 % |
c |       815 |    3013    12801 |    1764     815    50914    62.5 |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.396939 s)
c ==============================================================================
c [1mFound solution: 263[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:23900     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       956 |   30821    77882 |    9246     956    57112    59.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18662          
c   -- var.elim.:  2000/18662          
c   -- var.elim.:  3000/18662          
c   -- var.elim.:  4000/18662          
c   -- var.elim.:  5000/18662          
c   -- var.elim.:  6000/18662          
c   -- var.elim.:  7000/18662          
c   -- var.elim.:  8000/18662          
c   -- var.elim.:  9000/18662          
c   -- var.elim.:  10000/18662          
c   -- var.elim.:  11000/18662          
c   -- var.elim.:  12000/18662          
c   -- var.elim.:  13000/18662          
c   -- var.elim.:  14000/18662          
c   -- var.elim.:  15000/18662          
c   -- var.elim.:  16000/18662          
c   -- var.elim.:  17000/18662          
c   -- var.elim.:  18000/18662          
c   -- var.elim.:  18662/18662          
c   -- var.elim.:  1000/9239          
c   -- var.elim.:  2000/9239          
c   -- var.elim.:  3000/9239          
c   -- var.elim.:  4000/9239          
c   -- var.elim.:  5000/9239          
c   -- var.elim.:  6000/9239          
c   -- var.elim.:  7000/9239          
c   -- var.elim.:  8000/9239          
c   -- var.elim.:  9000/9239          
c   -- var.elim.:  9239/9239          
c   -- var.elim.:  1000/5615          
c   -- var.elim.:  2000/5615          
c   -- var.elim.:  3000/5615          
c   -- var.elim.:  4000/5615          
c   -- var.elim.:  5000/5615          
c   -- var.elim.:  5615/5615          
c   -- var.elim.:  1000/3941          
c   -- var.elim.:  2000/3941          
c   -- var.elim.:  3000/3941          
c   -- var.elim.:  3941/3941          
c   -- var.elim.:  1000/3209          
c   -- var.elim.:  2000/3209          
c   -- var.elim.:  3000/3209          
c   -- var.elim.:  3209/3209          
c   -- var.elim.:  1000/2772          
c   -- var.elim.:  2000/2772          
c   -- var.elim.:  2772/2772          
c   -- var.elim.:  1000/2793          
c   -- var.elim.:  2000/2793          
c   -- var.elim.:  2793/2793          
c   -- var.elim.:  1000/2651          
c   -- var.elim.:  2000/2651          
c   -- var.elim.:  2651/2651          
c   -- var.elim.:  252/252          
c   -- subsuming                       
c   -- var.elim.:  1000/2722          
c   -- var.elim.:  2000/2722          
c   -- var.elim.:  2722/2722          
c   -- var.elim.:  5/5          
c |       956 |   10542    69844 |      --     956       --      -- |     --   | -20279/-8037
c |       956 |   10542    69844 |    4216     956    57112    59.7 |  0.000 % |
c ==============================================================================
c (current CPU-time: 29.1916 s)
c ==============================================================================
c [1mFound solution: 258[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 |      1018 |   30510   118810 |    9152    1018    60269    59.2 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18091          
c   -- var.elim.:  2000/18091          
c   -- var.elim.:  3000/18091          
c   -- var.elim.:  4000/18091          
c   -- var.elim.:  5000/18091          
c   -- var.elim.:  6000/18091          
c   -- var.elim.:  7000/18091          
c   -- var.elim.:  8000/18091          
c   -- var.elim.:  9000/18091          
c   -- var.elim.:  10000/18091          
c   -- var.elim.:  11000/18091          
c   -- var.elim.:  12000/18091          
c   -- var.elim.:  13000/18091          
c   -- var.elim.:  14000/18091          
c   -- var.elim.:  15000/18091          
c   -- var.elim.:  16000/18091          
c   -- var.elim.:  17000/18091          
c   -- var.elim.:  18000/18091          
c   -- var.elim.:  18091/18091          
c   -- var.elim.:  1000/8752          
c   -- var.elim.:  2000/8752          
c   -- var.elim.:  3000/8752          
c   -- var.elim.:  4000/8752          
c   -- var.elim.:  5000/8752          
c   -- var.elim.:  6000/8752          
c   -- var.elim.:  7000/8752          
c   -- var.elim.:  8000/8752          
c   -- var.elim.:  8752/8752          
c   -- var.elim.:  1000/5407          
c   -- var.elim.:  2000/5407          
c   -- var.elim.:  3000/5407          
c   -- var.elim.:  4000/5407          
c   -- var.elim.:  5000/5407          
c   -- var.elim.:  5407/5407          
c   -- var.elim.:  1000/4323          
c   -- var.elim.:  2000/4323          
c   -- var.elim.:  3000/4323          
c   -- var.elim.:  4000/4323          
c   -- var.elim.:  4323/4323          
c   -- var.elim.:  1000/3505          
c   -- var.elim.:  2000/3505          
c   -- var.elim.:  3000/3505          
c   -- var.elim.:  3505/3505          
c   -- var.elim.:  1000/3051          
c   -- var.elim.:  2000/3051          
c   -- var.elim.:  3000/3051          
c   -- var.elim.:  3051/3051          
c   -- var.elim.:  1000/2631          
c   -- var.elim.:  2000/2631          
c   -- var.elim.:  2631/2631          
c   -- var.elim.:  1000/2680          
c   -- var.elim.:  2000/2680          
c   -- var.elim.:  2680/2680          
c   -- var.elim.:  631/631          
c   -- subsuming                       
c   -- var.elim.:  1000/1948          
c   -- var.elim.:  1948/1948          
c   -- var.elim.:  17/17          
c |      1018 |   10657    79241 |      --    1018       --      -- |     --   | -19845/-39498
c |      1018 |   10657    79241 |    4262    1018    60269    59.2 |  0.000 % |
c |      1118 |   10657    79241 |    4689    1118    67215    60.1 |  0.147 % |
c |      1268 |   10657    79241 |    5157    1268    77269    60.9 |  0.147 % |
c |      1496 |   10657    79241 |    5673    1496    91520    61.2 |  0.147 % |
c ==============================================================================
c (current CPU-time: 60.5978 s)
c ==============================================================================
c [1mFound solution: 252[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 |      1664 |   30797   128626 |    9239    1664   102388    61.5 |  0.147 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18242          
c   -- var.elim.:  2000/18242          
c   -- var.elim.:  3000/18242          
c   -- var.elim.:  4000/18242          
c   -- var.elim.:  5000/18242          
c   -- var.elim.:  6000/18242          
c   -- var.elim.:  7000/18242          
c   -- var.elim.:  8000/18242          
c   -- var.elim.:  9000/18242          
c   -- var.elim.:  10000/18242          
c   -- var.elim.:  11000/18242          
c   -- var.elim.:  12000/18242          
c   -- var.elim.:  13000/18242          
c   -- var.elim.:  14000/18242          
c   -- var.elim.:  15000/18242          
c   -- var.elim.:  16000/18242          
c   -- var.elim.:  17000/18242          
c   -- var.elim.:  18000/18242          
c   -- var.elim.:  18242/18242          
c   -- var.elim.:  1000/8828          
c   -- var.elim.:  2000/8828          
c   -- var.elim.:  3000/8828          
c   -- var.elim.:  4000/8828          
c   -- var.elim.:  5000/8828          
c   -- var.elim.:  6000/8828          
c   -- var.elim.:  7000/8828          
c   -- var.elim.:  8000/8828          
c   -- var.elim.:  8828/8828          
c   -- var.elim.:  1000/5557          
c   -- var.elim.:  2000/5557          
c   -- var.elim.:  3000/5557          
c   -- var.elim.:  4000/5557          
c   -- var.elim.:  5000/5557          
c   -- var.elim.:  5557/5557          
c   -- var.elim.:  1000/4463          
c   -- var.elim.:  2000/4463          
c   -- var.elim.:  3000/4463          
c   -- var.elim.:  4000/4463          
c   -- var.elim.:  4463/4463          
c   -- var.elim.:  1000/3608          
c   -- var.elim.:  2000/3608          
c   -- var.elim.:  3000/3608          
c   -- var.elim.:  3608/3608          
c   -- var.elim.:  1000/2920          
c   -- var.elim.:  2000/2920          
c   -- var.elim.:  2920/2920          
c   -- var.elim.:  1000/2306          
c   -- var.elim.:  2000/2306          
c   -- var.elim.:  2306/2306          
c   -- var.elim.:  1000/2027          
c   -- var.elim.:  2000/2027          
c   -- var.elim.:  2027/2027          
c   -- var.elim.:  1000/2171          
c   -- var.elim.:  2000/2171          
c   -- var.elim.:  2171/2171          
c   -- var.elim.:  422/422          
c   -- subsuming                       
c   -- var.elim.:  1000/1611          
c   -- var.elim.:  1611/1611          
c |      1664 |   10785    86585 |      --    1664       --      -- |     --   | -19997/-39298
c |      1664 |   10785    86585 |    4314    1663   101325    60.9 |  0.147 % |
c ==============================================================================
c (current CPU-time: 96.9133 s)
c ==============================================================================
c [1mFound solution: 251[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 |      1673 |   30161   134199 |    9048    1672   102230    61.1 |  0.147 % |
c   -- subsuming                       
c   -- var.elim.:  1000/17752          
c   -- var.elim.:  2000/17752          
c   -- var.elim.:  3000/17752          
c   -- var.elim.:  4000/17752          
c   -- var.elim.:  5000/17752          
c   -- var.elim.:  6000/17752          
c   -- var.elim.:  7000/17752          
c   -- var.elim.:  8000/17752          
c   -- var.elim.:  9000/17752          
c   -- var.elim.:  10000/17752          
c   -- var.elim.:  11000/17752          
c   -- var.elim.:  12000/17752          
c   -- var.elim.:  13000/17752          
c   -- var.elim.:  14000/17752          
c   -- var.elim.:  15000/17752          
c   -- var.elim.:  16000/17752          
c   -- var.elim.:  17000/17752          
c   -- var.elim.:  17752/17752          
c   -- var.elim.:  1000/8566          
c   -- var.elim.:  2000/8566          
c   -- var.elim.:  3000/8566          
c   -- var.elim.:  4000/8566          
c   -- var.elim.:  5000/8566          
c   -- var.elim.:  6000/8566          
c   -- var.elim.:  7000/8566          
c   -- var.elim.:  8000/8566          
c   -- var.elim.:  8566/8566          
c   -- var.elim.:  1000/5309          
c   -- var.elim.:  2000/5309          
c   -- var.elim.:  3000/5309          
c   -- var.elim.:  4000/5309          
c   -- var.elim.:  5000/5309          
c   -- var.elim.:  5309/5309          
c   -- var.elim.:  1000/4157          
c   -- var.elim.:  2000/4157          
c   -- var.elim.:  3000/4157          
c   -- var.elim.:  4000/4157          
c   -- var.elim.:  4157/4157          
c   -- var.elim.:  1000/3374          
c   -- var.elim.:  2000/3374          
c   -- var.elim.:  3000/3374          
c   -- var.elim.:  3374/3374          
c   -- var.elim.:  1000/3128          
c   -- var.elim.:  2000/3128          
c   -- var.elim.:  3000/3128          
c   -- var.elim.:  3128/3128          
c   -- var.elim.:  1000/2591          
c   -- var.elim.:  2000/2591          
c   -- var.elim.:  2591/2591          
c   -- var.elim.:  1000/1791          
c   -- var.elim.:  1791/1791          
c   -- var.elim.:  1000/1094          
c   -- var.elim.:  1094/1094          
c   -- var.elim.:  1000/1051          
c   -- var.elim.:  1051/1051          
c   -- subsuming                       
c   -- var.elim.:  1000/1454          
c   -- var.elim.:  1454/1454          
c |      1673 |   10874    95309 |      --    1672       --      -- |     --   | -19287/-38889
c |      1673 |   10874    95309 |    4349    1672   102230    61.1 |  0.147 % |
c ==============================================================================
c (current CPU-time: 146.115 s)
c ==============================================================================
c [1mFound solution: 237[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 |      1681 |   30658   143905 |    9197    1680   104067    61.9 |  0.147 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18048          
c   -- var.elim.:  2000/18048          
c   -- var.elim.:  3000/18048          
c   -- var.elim.:  4000/18048          
c   -- var.elim.:  5000/18048          
c   -- var.elim.:  6000/18048          
c   -- var.elim.:  7000/18048          
c   -- var.elim.:  8000/18048          
c   -- var.elim.:  9000/18048          
c   -- var.elim.:  10000/18048          
c   -- var.elim.:  11000/18048          
c   -- var.elim.:  12000/18048          
c   -- var.elim.:  13000/18048          
c   -- var.elim.:  14000/18048          
c   -- var.elim.:  15000/18048          
c   -- var.elim.:  16000/18048          
c   -- var.elim.:  17000/18048          
c   -- var.elim.:  18000/18048          
c   -- var.elim.:  18048/18048          
c   -- var.elim.:  1000/8740          
c   -- var.elim.:  2000/8740          
c   -- var.elim.:  3000/8740          
c   -- var.elim.:  4000/8740          
c   -- var.elim.:  5000/8740          
c   -- var.elim.:  6000/8740          
c   -- var.elim.:  7000/8740          
c   -- var.elim.:  8000/8740          
c   -- var.elim.:  8740/8740          
c   -- var.elim.:  1000/5426          
c   -- var.elim.:  2000/5426          
c   -- var.elim.:  3000/5426          
c   -- var.elim.:  4000/5426          
c   -- var.elim.:  5000/5426          
c   -- var.elim.:  5426/5426          
c   -- var.elim.:  1000/4282          
c   -- var.elim.:  2000/4282          
c   -- var.elim.:  3000/4282          
c   -- var.elim.:  4000/4282          
c   -- var.elim.:  4282/4282          
c   -- var.elim.:  1000/3228          
c   -- var.elim.:  2000/3228          
c   -- var.elim.:  3000/3228          
c   -- var.elim.:  3228/3228          
c   -- var.elim.:  1000/3195          
c   -- var.elim.:  2000/3195          
c   -- var.elim.:  3000/3195          
c   -- var.elim.:  3195/3195          
c   -- var.elim.:  1000/2965          
c   -- var.elim.:  2000/2965          
c   -- var.elim.:  2965/2965          
c   -- var.elim.:  1000/1967          
c   -- var.elim.:  1967/1967          
c   -- var.elim.:  1000/1333          
c   -- var.elim.:  1333/1333          
c   -- var.elim.:  330/330          
c   -- subsuming                       
c   -- var.elim.:  1000/1701          
c   -- var.elim.:  1701/1701          
c |      1681 |   11120   105742 |      --    1680       --      -- |     --   | -19538/-38162
c |      1681 |   11120   105742 |    4448    1680   104067    61.9 |  0.147 % |
c |      1781 |   11107   105625 |    4887    1779   114381    64.3 |  0.402 % |
c |      1931 |   11107   105625 |    5375    1929   124032    64.3 |  0.402 % |
c |      2156 |   11107   105625 |    5913    2154   137870    64.0 |  0.402 % |
c |      2495 |   11107   105625 |    6504    2493   158359    63.5 |  0.402 % |
c |      3002 |   11081   105469 |    7138    2999   397522   132.6 |  0.661 % |
c |      3761 |   10492   100095 |    7434    3724   667101   179.1 |  6.662 % |
c |      4900 |   10338    98855 |    8058    4855   964661   198.7 |  8.245 % |
c ==============================================================================
c (current CPU-time: 212.483 s)
c ==============================================================================
c [1mFound solution: 236[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 |      5209 |   10351    98895 |    3105    5164   987937   191.3 |  8.245 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2855          
c   -- var.elim.:  2000/2855          
c   -- var.elim.:  2855/2855          
c   -- var.elim.:  348/348          
c   -- subsuming                       
c   -- var.elim.:  1000/1397          
c   -- var.elim.:  1397/1397          
c   -- var.elim.:  5/5          
c |      5209 |   10293    93386 |      --    5164       --      -- |     --   | -29/-95
c |      5209 |   10293    93386 |    4117    4348   348582    80.2 |  8.245 % |
c |      5311 |   10293    93386 |    4528    4450   355720    79.9 |  8.433 % |
c |      5463 |   10293    93386 |    4981    4602   366069    79.5 |  8.433 % |
c |      5688 |   10293    93386 |    5479    4827   384097    79.6 |  8.433 % |
c |      6030 |   10293    93386 |    6027    5169   407571    78.8 |  8.433 % |
c |      6538 |   10293    93386 |    6630    5677   530188    93.4 |  8.433 % |
c |      7297 |   10164    92106 |    7202    6432   784929   122.0 |  9.767 % |
c |      8436 |    9936    89982 |    7744    7559  1137332   150.5 | 12.149 % |
c |     10144 |    9731    87852 |    8343    6445  1331338   206.6 | 14.316 % |
c |     12706 |    9686    87262 |    9135    8991  2611922   290.5 | 14.864 % |
c |     16553 |    9686    87262 |   10049    8759  3042576   347.4 | 14.864 % |
c |     22320 |    9031    80501 |   10306   10800  3184283   294.8 | 21.915 % |
c |     30973 |    8908    78679 |   11182   11771  3450166   293.1 | 23.154 % |
c ==============================================================================
c (current CPU-time: 296.773 s)
c ==============================================================================
c [1mFound solution: 235[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 |     33397 |   27028   122248 |    8108    9848  3876125   393.6 | 23.154 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15947          
c   -- var.elim.:  2000/15947          
c   -- var.elim.:  3000/15947          
c   -- var.elim.:  4000/15947          
c   -- var.elim.:  5000/15947          
c   -- var.elim.:  6000/15947          
c   -- var.elim.:  7000/15947          
c   -- var.elim.:  8000/15947          
c   -- var.elim.:  9000/15947          
c   -- var.elim.:  10000/15947          
c   -- var.elim.:  11000/15947          
c   -- var.elim.:  12000/15947          
c   -- var.elim.:  13000/15947          
c   -- var.elim.:  14000/15947          
c   -- var.elim.:  15000/15947          
c   -- var.elim.:  15947/15947          
c   -- var.elim.:  1000/7308          
c   -- var.elim.:  2000/7308          
c   -- var.elim.:  3000/7308          
c   -- var.elim.:  4000/7308          
c   -- var.elim.:  5000/7308          
c   -- var.elim.:  6000/7308          
c   -- var.elim.:  7000/7308          
c   -- var.elim.:  7308/7308          
c   -- var.elim.:  1000/4316          
c   -- var.elim.:  2000/4316          
c   -- var.elim.:  3000/4316          
c   -- var.elim.:  4000/4316          
c   -- var.elim.:  4316/4316          
c   -- var.elim.:  1000/3182          
c   -- var.elim.:  2000/3182          
c   -- var.elim.:  3000/3182          
c   -- var.elim.:  3182/3182          
c   -- var.elim.:  1000/2486          
c   -- var.elim.:  2000/2486          
c   -- var.elim.:  2486/2486          
c   -- var.elim.:  1000/2147          
c   -- var.elim.:  2000/2147          
c   -- var.elim.:  2147/2147          
c   -- var.elim.:  1000/1582          
c   -- var.elim.:  1582/1582          
c   -- var.elim.:  892/892          
c   -- var.elim.:  512/512          
c   -- subsuming                       
c   -- var.elim.:  1000/1034          
c   -- var.elim.:  1034/1034          
c   -- var.elim.:  40/40          
c |     33397 |    8931    80113 |      --    9848       --      -- |     --   | -17996/-41932
c |     33397 |    8931    80113 |    3572    4418   234478    53.1 | 23.154 % |
c |     33500 |    8931    80113 |    3929    4521   257438    56.9 | 34.723 % |
c |     33651 |    8931    80113 |    4322    4672   280544    60.0 | 34.723 % |
c |     33877 |    8931    80113 |    4754    4898   297257    60.7 | 34.723 % |
c |     34217 |    8931    80113 |    5230    5238   319979    61.1 | 34.723 % |
c |     34723 |    8931    80113 |    5753    5744   504222    87.8 | 34.723 % |
c |     35485 |    8902    79830 |    6308    6505   813310   125.0 | 35.008 % |
c |     36624 |    8743    78230 |    6815    7638  1266267   165.8 | 36.493 % |
c |     38338 |    8670    76445 |    7433    9349  2125981   227.4 | 37.083 % |
c |     40902 |    8634    76115 |    8143    8794  2501803   284.5 | 37.409 % |
c |     44746 |    8562    75359 |    8883    8953  2863982   319.9 | 38.100 % |
c |     50515 |    8359    73168 |    9539   10730  3387449   315.7 | 39.870 % |
c |     59164 |    8222    71630 |   10321   10885  3578067   328.7 | 41.172 % |
c |     72140 |    8194    71350 |   11315   10214  4316386   422.6 | 41.416 % |
c |     91602 |    8168    71030 |   12407   10970  5033484   458.8 | 41.640 % |
c |    120794 |    8168    71030 |   13647   13103  4743913   362.0 | 41.640 % |
c |    164585 |    7764    66588 |   14270   12871  3019915   234.6 | 45.382 % |
c |    230270 |    7665    65369 |   15497   14910  5024383   337.0 | 46.298 % |
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 -x#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 23990
Raw data (stat): 23990 (runsolver) R 23989 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421948442 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99982 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 3148 0 0 0 987 11 0 0 25 0 1 0 421948442 15224832 3036 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3717 3036 603 41 0 3676 0
vsize: 14868
[startup+20.0005 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 3211 0 0 0 1983 15 0 0 25 0 1 0 421948442 15486976 3099 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3781 3099 603 41 0 3740 0
vsize: 15124
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 4182 0 0 0 2978 20 0 0 25 0 1 0 421948442 17350656 3704 4294967295 134512640 134672761 3221224576 3221216228 1074972061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4236 3704 603 41 0 4195 0
vsize: 16944
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 4425 0 0 0 3971 27 0 0 25 0 1 0 421948442 20234240 3911 4294967295 134512640 134672761 3221224576 3221223024 134643545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 3911 603 41 0 4899 0
vsize: 19760
[startup+50.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 4425 0 0 0 4956 32 0 0 25 0 1 0 421948442 20234240 3911 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 3911 603 41 0 4899 0
vsize: 19760
[startup+60.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 4455 0 0 0 5956 32 0 0 25 0 1 0 421948442 20234240 3911 4294967295 134512640 134672761 3221224576 3221223024 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4940 3911 603 41 0 4899 0
vsize: 19760
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 7497 0 0 0 6941 47 0 0 25 0 1 0 421948442 22192128 4645 4294967295 134512640 134672761 3221224576 3221223024 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5418 4645 603 41 0 5377 0
vsize: 21672
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 7499 0 0 0 7936 51 0 0 25 0 1 0 421948442 22192128 4647 4294967295 134512640 134672761 3221224576 3221223024 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5418 4647 603 41 0 5377 0
vsize: 21672
[startup+90.0021 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 7499 0 0 0 8935 52 0 0 25 0 1 0 421948442 22192128 4647 4294967295 134512640 134672761 3221224576 3221223024 134643987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5418 4647 603 41 0 5377 0
vsize: 21672
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 11548 0 0 0 9919 68 0 0 25 0 1 0 421948442 23535616 5242 4294967295 134512640 134672761 3221224576 3221223068 134642766 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5746 5242 603 41 0 5705 0
vsize: 22984
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 11648 0 0 0 10917 71 0 0 25 0 1 0 421948442 23851008 5306 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5823 5306 603 41 0 5782 0
vsize: 23292
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 11648 0 0 0 11911 76 0 0 25 0 1 0 421948442 23851008 5306 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5823 5306 603 41 0 5782 0
vsize: 23292
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 11648 0 0 0 12910 77 0 0 25 0 1 0 421948442 23851008 5306 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5823 5306 603 41 0 5782 0
vsize: 23292
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 11648 0 0 0 13910 77 0 0 25 0 1 0 421948442 23851008 5306 4294967295 134512640 134672761 3221224576 3221223068 134643021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5823 5306 603 41 0 5782 0
vsize: 23292
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 17031 0 0 0 14888 99 0 0 25 0 1 0 421948442 31055872 6029 4294967295 134512640 134672761 3221224576 3221223068 134642890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7582 6029 603 41 0 7541 0
vsize: 30328
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 17154 0 0 0 15883 102 0 0 25 0 1 0 421948442 31469568 6116 4294967295 134512640 134672761 3221224576 3221223024 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7683 6116 603 41 0 7642 0
vsize: 30732
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 17159 0 0 0 16880 107 0 0 25 0 1 0 421948442 31469568 6121 4294967295 134512640 134672761 3221224576 3221223024 134643468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7683 6121 603 41 0 7642 0
vsize: 30732
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 17159 0 0 0 17877 109 0 0 25 0 1 0 421948442 31469568 6121 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7683 6121 603 41 0 7642 0
vsize: 30732
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 17159 0 0 0 18877 110 0 0 25 0 1 0 421948442 31469568 6121 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7683 6121 603 41 0 7642 0
vsize: 30732
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 17159 0 0 0 19877 110 0 0 25 0 1 0 421948442 31469568 6121 4294967295 134512640 134672761 3221224576 3221223120 134621110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7683 6121 603 41 0 7642 0
vsize: 30732
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 17474 0 0 0 20876 111 0 0 25 0 1 0 421948442 32632832 6406 4294967295 134512640 134672761 3221224576 3221223760 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7967 6406 603 41 0 7926 0
vsize: 31868
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 24202 0 0 0 21851 136 0 0 25 0 1 0 421948442 34627584 6911 4294967295 134512640 134672761 3221224576 3221223024 134643545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8454 6911 603 41 0 8413 0
vsize: 33816
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 24302 0 0 0 22851 136 0 0 25 0 1 0 421948442 34623488 6910 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8453 6910 603 41 0 8412 0
vsize: 33812
[startup+240.005 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 24959 0 0 0 23850 137 0 0 25 0 1 0 421948442 37380096 7567 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9126 7567 603 41 0 9085 0
vsize: 36504
[startup+250.006 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 26580 0 0 0 24846 142 0 0 25 0 1 0 421948442 44081152 9188 4294967295 134512640 134672761 3221224576 3221223760 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10762 9188 603 41 0 10721 0
vsize: 43048
[startup+260.005 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 27162 0 0 0 25844 144 0 0 25 0 1 0 421948442 46415872 9770 4294967295 134512640 134672761 3221224576 3221223720 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11332 9770 603 41 0 11291 0
vsize: 45328
[startup+270.006 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 27217 0 0 0 26844 144 0 0 25 0 1 0 421948442 46641152 9825 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11387 9825 603 41 0 11346 0
vsize: 45548
[startup+280.007 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 27217 0 0 0 27844 144 0 0 25 0 1 0 421948442 46641152 9825 4294967295 134512640 134672761 3221224576 3221223488 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11387 9825 603 41 0 11346 0
vsize: 45548
[startup+290.006 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 27217 0 0 0 28844 144 0 0 25 0 1 0 421948442 46632960 9825 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11385 9825 603 41 0 11344 0
vsize: 45540
[startup+300.007 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 33163 0 0 0 29821 166 0 0 25 0 1 0 421948442 76435456 15747 4294967295 134512640 134672761 3221224576 3221222768 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18661 15747 603 41 0 18620 0
vsize: 74644
[startup+310.007 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 33970 0 0 0 30815 172 0 0 25 0 1 0 421948442 49139712 10687 4294967295 134512640 134672761 3221224576 3221223024 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11997 10687 603 41 0 11956 0
vsize: 47988
[startup+320.007 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 33970 0 0 0 31811 176 0 0 25 0 1 0 421948442 49139712 10687 4294967295 134512640 134672761 3221224576 3221222752 134621242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11997 10687 603 41 0 11956 0
vsize: 47988
[startup+330.008 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 33970 0 0 0 32811 177 0 0 25 0 1 0 421948442 49139712 10687 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11997 10687 603 41 0 11956 0
vsize: 47988
[startup+340.008 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34024 0 0 0 33811 177 0 0 25 0 1 0 421948442 49025024 10701 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 10701 603 41 0 11928 0
vsize: 47876
[startup+350.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34024 0 0 0 34811 177 0 0 25 0 1 0 421948442 49025024 10701 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 10701 603 41 0 11928 0
vsize: 47876
[startup+360.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34024 0 0 0 35811 177 0 0 25 0 1 0 421948442 49025024 10701 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 10701 603 41 0 11928 0
vsize: 47876
[startup+370.009 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34025 0 0 0 36811 177 0 0 25 0 1 0 421948442 49025024 10702 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 10702 603 41 0 11928 0
vsize: 47876
[startup+380.01 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34025 0 0 0 37811 177 0 0 25 0 1 0 421948442 49025024 10702 4294967295 134512640 134672761 3221224576 3221223720 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 10702 603 41 0 11928 0
vsize: 47876
[startup+390.009 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34428 0 0 0 38810 178 0 0 25 0 1 0 421948442 50720768 11105 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12383 11105 603 41 0 12342 0
vsize: 49532
[startup+400.009 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34504 0 0 0 39810 178 0 0 25 0 1 0 421948442 51056640 11181 4294967295 134512640 134672761 3221224576 3221223672 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12465 11181 603 41 0 12424 0
vsize: 49860
[startup+410.009 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34504 0 0 0 40810 178 0 0 25 0 1 0 421948442 51056640 11181 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12465 11181 603 41 0 12424 0
vsize: 49860
[startup+420.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 34802 0 0 0 41810 179 0 0 25 0 1 0 421948442 52224000 11479 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12750 11479 603 41 0 12709 0
vsize: 51000
[startup+430.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 35047 0 0 0 42810 180 0 0 25 0 1 0 421948442 53288960 11724 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13010 11724 603 41 0 12969 0
vsize: 52040
[startup+440.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 35534 0 0 0 43809 181 0 0 25 0 1 0 421948442 55214080 12211 4294967295 134512640 134672761 3221224576 3221223616 134612601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13480 12211 603 41 0 13439 0
vsize: 53920
[startup+450.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 35708 0 0 0 44809 181 0 0 25 0 1 0 421948442 55984128 12385 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13668 12385 603 41 0 13627 0
vsize: 54672
[startup+460.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36253 0 0 0 45807 183 0 0 25 0 1 0 421948442 58175488 12930 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 12930 603 41 0 14162 0
vsize: 56812
[startup+470.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36253 0 0 0 46808 183 0 0 25 0 1 0 421948442 58175488 12930 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 12930 603 41 0 14162 0
vsize: 56812
[startup+480.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36253 0 0 0 47808 183 0 0 25 0 1 0 421948442 58175488 12930 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 12930 603 41 0 14162 0
vsize: 56812
[startup+490.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36253 0 0 0 48808 183 0 0 25 0 1 0 421948442 58175488 12930 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 12930 603 41 0 14162 0
vsize: 56812
[startup+500.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36253 0 0 0 49808 183 0 0 25 0 1 0 421948442 58175488 12930 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 12930 603 41 0 14162 0
vsize: 56812
[startup+510.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36253 0 0 0 50808 183 0 0 25 0 1 0 421948442 58175488 12930 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 12930 603 41 0 14162 0
vsize: 56812
[startup+520.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36254 0 0 0 51809 183 0 0 25 0 1 0 421948442 58175488 12931 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 12931 603 41 0 14162 0
vsize: 56812
[startup+530.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36292 0 0 0 52809 183 0 0 25 0 1 0 421948442 58368000 12969 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 12969 603 41 0 14209 0
vsize: 57000
[startup+540.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36642 0 0 0 53808 183 0 0 25 0 1 0 421948442 59781120 13319 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14595 13319 603 41 0 14554 0
vsize: 58380
[startup+550.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36856 0 0 0 54808 184 0 0 25 0 1 0 421948442 60665856 13533 4294967295 134512640 134672761 3221224576 3221223616 134612634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14811 13533 603 41 0 14770 0
vsize: 59244
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 36856 0 0 0 55809 184 0 0 25 0 1 0 421948442 60665856 13533 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14811 13533 603 41 0 14770 0
vsize: 59244
[startup+570.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37218 0 0 0 56808 185 0 0 25 0 1 0 421948442 62115840 13895 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15165 13895 603 41 0 15124 0
vsize: 60660
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37218 0 0 0 57808 185 0 0 25 0 1 0 421948442 62115840 13895 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15165 13895 603 41 0 15124 0
vsize: 60660
[startup+590.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37218 0 0 0 58808 185 0 0 25 0 1 0 421948442 62115840 13895 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15165 13895 603 41 0 15124 0
vsize: 60660
[startup+600.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 59808 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+610.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 60808 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+620.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 61809 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+630.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 62809 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+640.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 63809 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+650.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 64809 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223616 134612587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+660.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 65809 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+670.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37236 0 0 0 66810 185 0 0 25 0 1 0 421948442 62296064 13913 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15209 13913 603 41 0 15168 0
vsize: 60836
[startup+680.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37448 0 0 0 67810 185 0 0 25 0 1 0 421948442 63176704 14125 4294967295 134512640 134672761 3221224576 3221223616 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14125 603 41 0 15383 0
vsize: 61696
[startup+690.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37448 0 0 0 68810 185 0 0 25 0 1 0 421948442 63176704 14125 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14125 603 41 0 15383 0
vsize: 61696
[startup+700.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37448 0 0 0 69810 185 0 0 25 0 1 0 421948442 63176704 14125 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14125 603 41 0 15383 0
vsize: 61696
[startup+710.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37448 0 0 0 70810 185 0 0 25 0 1 0 421948442 63176704 14125 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14125 603 41 0 15383 0
vsize: 61696
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37448 0 0 0 71810 185 0 0 25 0 1 0 421948442 63176704 14125 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14125 603 41 0 15383 0
vsize: 61696
[startup+730.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37448 0 0 0 72811 185 0 0 25 0 1 0 421948442 63176704 14125 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15424 14125 603 41 0 15383 0
vsize: 61696
[startup+740.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37450 0 0 0 73811 185 0 0 25 0 1 0 421948442 63152128 14126 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14126 603 41 0 15377 0
vsize: 61672
[startup+750.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37450 0 0 0 74811 185 0 0 25 0 1 0 421948442 63152128 14126 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14126 603 41 0 15377 0
vsize: 61672
[startup+760.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37450 0 0 0 75811 185 0 0 25 0 1 0 421948442 63152128 14126 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14126 603 41 0 15377 0
vsize: 61672
[startup+770.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 76812 185 0 0 25 0 1 0 421948442 63152128 14127 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14127 603 41 0 15377 0
vsize: 61672
[startup+780.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 77812 185 0 0 25 0 1 0 421948442 63152128 14127 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14127 603 41 0 15377 0
vsize: 61672
[startup+790.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 78812 185 0 0 25 0 1 0 421948442 63152128 14127 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14127 603 41 0 15377 0
vsize: 61672
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 79812 185 0 0 25 0 1 0 421948442 63152128 14127 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14127 603 41 0 15377 0
vsize: 61672
[startup+810.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 80812 185 0 0 25 0 1 0 421948442 63094784 14121 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15404 14121 603 41 0 15363 0
vsize: 61616
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 81812 185 0 0 25 0 1 0 421948442 63094784 14121 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15404 14121 603 41 0 15363 0
vsize: 61616
[startup+830.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 82813 185 0 0 25 0 1 0 421948442 63094784 14121 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15404 14121 603 41 0 15363 0
vsize: 61616
[startup+840.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 83813 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+850.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 84813 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+860.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 85813 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+870.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 86813 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+880.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 87813 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223616 134603565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+890.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 88814 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+900.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 89814 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+910.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37451 0 0 0 90814 185 0 0 25 0 1 0 421948442 63090688 14120 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14120 603 41 0 15362 0
vsize: 61612
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37452 0 0 0 91814 185 0 0 25 0 1 0 421948442 63090688 14121 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14121 603 41 0 15362 0
vsize: 61612
[startup+930.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37452 0 0 0 92814 185 0 0 25 0 1 0 421948442 63090688 14121 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14121 603 41 0 15362 0
vsize: 61612
[startup+940.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37452 0 0 0 93814 185 0 0 25 0 1 0 421948442 63090688 14121 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14121 603 41 0 15362 0
vsize: 61612
[startup+950.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37452 0 0 0 94815 185 0 0 25 0 1 0 421948442 63090688 14121 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14121 603 41 0 15362 0
vsize: 61612
[startup+960.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37452 0 0 0 95815 185 0 0 25 0 1 0 421948442 63090688 14121 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15403 14121 603 41 0 15362 0
vsize: 61612
[startup+970.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37763 0 0 0 96815 185 0 0 25 0 1 0 421948442 64417792 14431 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15727 14431 603 41 0 15686 0
vsize: 62908
[startup+980.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37763 0 0 0 97815 185 0 0 25 0 1 0 421948442 64417792 14431 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15727 14431 603 41 0 15686 0
vsize: 62908
[startup+990.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37763 0 0 0 98815 185 0 0 25 0 1 0 421948442 64417792 14431 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15727 14431 603 41 0 15686 0
vsize: 62908
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37772 0 0 0 99815 185 0 0 25 0 1 0 421948442 64450560 14439 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14439 603 41 0 15694 0
vsize: 62940
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37772 0 0 0 100815 185 0 0 25 0 1 0 421948442 64450560 14439 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14439 603 41 0 15694 0
vsize: 62940
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37772 0 0 0 101816 185 0 0 25 0 1 0 421948442 64450560 14439 4294967295 134512640 134672761 3221224576 3221223616 134612799 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14439 603 41 0 15694 0
vsize: 62940
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37772 0 0 0 102816 185 0 0 25 0 1 0 421948442 64450560 14439 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14439 603 41 0 15694 0
vsize: 62940
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37773 0 0 0 103816 185 0 0 25 0 1 0 421948442 64450560 14440 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14440 603 41 0 15694 0
vsize: 62940
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37773 0 0 0 104816 185 0 0 25 0 1 0 421948442 64450560 14440 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14440 603 41 0 15694 0
vsize: 62940
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 37773 0 0 0 105816 185 0 0 25 0 1 0 421948442 64450560 14440 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14440 603 41 0 15694 0
vsize: 62940
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 38356 0 0 0 106815 187 0 0 25 0 1 0 421948442 66838528 15022 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16318 15022 603 41 0 16277 0
vsize: 65272
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 38356 0 0 0 107815 187 0 0 25 0 1 0 421948442 66838528 15022 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16318 15022 603 41 0 16277 0
vsize: 65272
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 38356 0 0 0 108815 187 0 0 25 0 1 0 421948442 66838528 15022 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16318 15022 603 41 0 16277 0
vsize: 65272
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 38838 0 0 0 109815 188 0 0 25 0 1 0 421948442 68771840 15504 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16790 15504 603 41 0 16749 0
vsize: 67160
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39049 0 0 0 110815 188 0 0 25 0 1 0 421948442 69668864 15714 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17009 15714 603 41 0 16968 0
vsize: 68036
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39049 0 0 0 111815 188 0 0 25 0 1 0 421948442 69668864 15714 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17009 15714 603 41 0 16968 0
vsize: 68036
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39109 0 0 0 112815 188 0 0 25 0 1 0 421948442 69914624 15774 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17069 15774 603 41 0 17028 0
vsize: 68276
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39109 0 0 0 113815 188 0 0 25 0 1 0 421948442 69914624 15774 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17069 15774 603 41 0 17028 0
vsize: 68276
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39109 0 0 0 114816 188 0 0 25 0 1 0 421948442 69914624 15774 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17069 15774 603 41 0 17028 0
vsize: 68276
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39110 0 0 0 115816 188 0 0 25 0 1 0 421948442 69914624 15775 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17069 15775 603 41 0 17028 0
vsize: 68276
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 3/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39110 0 0 0 116816 188 0 0 25 0 1 0 421948442 69914624 15775 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17069 15775 603 41 0 17028 0
vsize: 68276
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39110 0 0 0 117816 188 0 0 25 0 1 0 421948442 69910528 15774 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17068 15774 603 41 0 17027 0
vsize: 68272
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39110 0 0 0 118816 188 0 0 25 0 1 0 421948442 69910528 15774 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17068 15774 603 41 0 17027 0
vsize: 68272
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 3/54 23990
Raw data (stat): 23990 (minisat+) R 23989 20937 20936 0 -1 0 39111 0 0 0 119817 188 0 0 25 0 1 0 421948442 69869568 15775 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17058 15775 603 41 0 17017 0
vsize: 68232
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 23990
Raw data (stat): 23990 (minisat+) Z 23989 20937 20936 0 -1 12 39112 0 0 0 119817 194 0 0 25 0 1 0 421948442 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): 1200.08
CPU time (s): 1200.11
CPU user time (s): 1198.17
CPU system time (s): 1.9407
CPU usage (%): 100.002
Max. virtual memory (Kb): 74644
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####