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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-5.opb
MD5SUM	38d41fdbe49543e8928c5210e4323f00
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
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	760
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	760
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	1175.08
Number of variables	760
Total number of constraints	41619
Number of constraints which are clauses	41619
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	2
Trace number 5620

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        905224 kB
Buffers:         35760 kB
Cached:          54900 kB
SwapCached:        392 kB
Active:          52204 kB
Inactive:        41596 kB
HighTotal:      131008 kB
HighFree:        72436 kB
LowTotal:       903652 kB
LowFree:        832788 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            30108 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:17:52 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 4088 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41619 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 |   41619    83238 |   12485       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |   41619    83238 |   16647       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 1.75273 s)
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   77738   168085 |   23321       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24720          
c   -- var.elim.:  2000/24720          
c   -- var.elim.:  3000/24720          
c   -- var.elim.:  4000/24720          
c   -- var.elim.:  5000/24720          
c   -- var.elim.:  6000/24720          
c   -- var.elim.:  7000/24720          
c   -- var.elim.:  8000/24720          
c   -- var.elim.:  9000/24720          
c   -- var.elim.:  10000/24720          
c   -- var.elim.:  11000/24720          
c   -- var.elim.:  12000/24720          
c   -- var.elim.:  13000/24720          
c   -- var.elim.:  14000/24720          
c   -- var.elim.:  15000/24720          
c   -- var.elim.:  16000/24720          
c   -- var.elim.:  17000/24720          
c   -- var.elim.:  18000/24720          
c   -- var.elim.:  19000/24720          
c   -- var.elim.:  20000/24720          
c   -- var.elim.:  21000/24720          
c   -- var.elim.:  22000/24720          
c   -- var.elim.:  23000/24720          
c   -- var.elim.:  24000/24720          
c   -- var.elim.:  24720/24720          
c   -- var.elim.:  1000/12563          
c   -- var.elim.:  2000/12563          
c   -- var.elim.:  3000/12563          
c   -- var.elim.:  4000/12563          
c   -- var.elim.:  5000/12563          
c   -- var.elim.:  6000/12563          
c   -- var.elim.:  7000/12563          
c   -- var.elim.:  8000/12563          
c   -- var.elim.:  9000/12563          
c   -- var.elim.:  10000/12563          
c   -- var.elim.:  11000/12563          
c   -- var.elim.:  12000/12563          
c   -- var.elim.:  12563/12563          
c   -- var.elim.:  1000/2609          
c   -- var.elim.:  2000/2609          
c   -- var.elim.:  2609/2609          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  1000/4974          
c   -- var.elim.:  2000/4974          
c   -- var.elim.:  3000/4974          
c   -- var.elim.:  4000/4974          
c   -- var.elim.:  4974/4974          
c   -- var.elim.:  355/355          
c |         0 |   52275   168018 |      --       0       --      -- |     --   | -25463/-66
c |         0 |   52275   168018 |   20910       0        0     nan |  0.000 % |
c |       100 |   52275   168018 |   23001     100    16808   168.1 | 52.680 % |
c |       251 |   52275   168018 |   25301     251    55976   223.0 | 52.679 % |
c |       476 |   52275   168018 |   27831     476    92098   193.5 | 52.679 % |
c |       813 |   52275   168018 |   30614     813   139309   171.4 | 52.679 % |
c ==============================================================================
c (current CPU-time: 54.7187 s)
c ==============================================================================
c [1mFound solution: -31[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 |       873 |   57716   182694 |   17314     873   169091   193.7 | 52.679 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9101          
c   -- var.elim.:  2000/9101          
c   -- var.elim.:  3000/9101          
c   -- var.elim.:  4000/9101          
c   -- var.elim.:  5000/9101          
c   -- var.elim.:  6000/9101          
c   -- var.elim.:  7000/9101          
c   -- var.elim.:  8000/9101          
c   -- var.elim.:  9000/9101          
c   -- var.elim.:  9101/9101          
c   -- var.elim.:  1000/3825          
c   -- var.elim.:  2000/3825          
c   -- var.elim.:  3000/3825          
c   -- var.elim.:  3825/3825          
c   -- var.elim.:  198/198          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/3746          
c   -- var.elim.:  2000/3746          
c   -- var.elim.:  3000/3746          
c   -- var.elim.:  3746/3746          
c   -- var.elim.:  234/234          
c |       873 |   52426   177815 |      --     873       --      -- |     --   | -5282/-4862
c |       873 |   52426   177815 |   20970     873   169091   193.7 | 52.679 % |
c |       973 |   52426   177815 |   23067     973   188191   193.4 | 62.100 % |
c |      1123 |   52398   177514 |   25360    1121   205419   183.2 | 62.189 % |
c |      1349 |   52376   177288 |   27884    1344   230265   171.3 | 62.259 % |
c |      1686 |   52376   177288 |   30673    1681   257256   153.0 | 62.259 % |
c |      2192 |   52231   175764 |   33647    2175   315150   144.9 | 62.684 % |
c |      2952 |   52120   174700 |   36933    2925   411491   140.7 | 63.021 % |
c |      4091 |   51804   171352 |   40380    4034   558215   138.4 | 63.871 % |
c |      5799 |   51182   165729 |   43885    5658   775283   137.0 | 65.751 % |
c |      8361 |   50491   159566 |   47622    8031  1216536   151.5 | 67.883 % |
c |     12205 |   50177   156676 |   52058   11773  1829918   155.4 | 68.861 % |
c |     17972 |   49270   148458 |   56229   17202  2831478   164.6 | 71.705 % |
c ==============================================================================
c (current CPU-time: 120.719 s)
c ==============================================================================
c [1mFound solution: -32[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 |     21785 |   50877   152087 |   15263   20979  3771374   179.8 | 71.705 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6056          
c   -- var.elim.:  2000/6056          
c   -- var.elim.:  3000/6056          
c   -- var.elim.:  4000/6056          
c   -- var.elim.:  5000/6056          
c   -- var.elim.:  6000/6056          
c   -- var.elim.:  6056/6056          
c   -- var.elim.:  1000/1507          
c   -- var.elim.:  1507/1507          
c |     21785 |   49155   146159 |      --   20979       --      -- |     --   | -1702/-2915
c |     21785 |   49155   146159 |   19662   17954  1760109    98.0 | 71.705 % |
c |     21885 |   49129   145913 |   21616   18053  1765456    97.8 | 73.001 % |
c |     22036 |   49129   145913 |   23778   18204  1795741    98.6 | 73.001 % |
c |     22261 |   49065   145401 |   26122   18391  1820865    99.0 | 73.193 % |
c |     22600 |   48985   144691 |   28687   18727  1874825   100.1 | 73.439 % |
c |     23106 |   48939   144253 |   31526   19194  2011150   104.8 | 73.581 % |
c |     23865 |   48939   144253 |   34679   19953  2223394   111.4 | 73.581 % |
c |     25004 |   48911   144022 |   38125   21034  2513740   119.5 | 73.667 % |
c |     26713 |   48847   143387 |   41883   22725  2967585   130.6 | 73.864 % |
c |     29275 |   48635   141485 |   45871   25163  3426977   136.2 | 74.469 % |
c |     33119 |   48567   140892 |   50388   28952  4336992   149.8 | 74.666 % |
c ==============================================================================
c (current CPU-time: 172.041 s)
c ==============================================================================
c [1mFound solution: -33[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 |     38546 |   49965   144532 |   14989   34346  5908518   172.0 | 74.666 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5367          
c   -- var.elim.:  2000/5367          
c   -- var.elim.:  3000/5367          
c   -- var.elim.:  4000/5367          
c   -- var.elim.:  5000/5367          
c   -- var.elim.:  5367/5367          
c   -- var.elim.:  1000/1366          
c   -- var.elim.:  1366/1366          
c |     38546 |   48547   142184 |      --   34346       --      -- |     --   | -1418/-2347
c |     38546 |   48547   142184 |   19418   33538  5767741   172.0 | 74.666 % |
c |     38646 |   48547   142184 |   21360   16765  2814634   167.9 | 75.493 % |
c |     38796 |   48547   142184 |   23496   16915  2844338   168.2 | 75.493 % |
c |     39021 |   48547   142184 |   25846   17140  2934558   171.2 | 75.493 % |
c |     39358 |   48483   141707 |   28393   17471  2998390   171.6 | 75.679 % |
c |     39864 |   48483   141707 |   31232   17977  3119475   173.5 | 75.679 % |
c |     40625 |   48450   141397 |   34332   18727  3308116   176.6 | 75.776 % |
c |     41765 |   48377   140772 |   37709   19861  3521425   177.3 | 75.986 % |
c |     43474 |   48302   140123 |   41415   21561  3888698   180.4 | 76.202 % |
c |     46037 |   48244   139567 |   45502   24103  4627214   192.0 | 76.376 % |
c |     49882 |   48049   137770 |   49850   27889  5789956   207.6 | 76.947 % |
c |     55648 |   47764   135197 |   54510   33567  7171321   213.6 | 77.782 % |
c |     64297 |   47639   134097 |   59804   42153  9661939   229.2 | 78.149 % |
c |     77271 |   47405   131630 |   65461   54962 13228162   240.7 | 78.804 % |
c ==============================================================================
c (current CPU-time: 387.277 s)
c ==============================================================================
c [1mFound solution: -34[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 |     89537 |   47935   131887 |   14380   67133 16828421   250.7 | 78.804 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4118          
c   -- var.elim.:  2000/4118          
c   -- var.elim.:  3000/4118          
c   -- var.elim.:  4000/4118          
c   -- var.elim.:  4118/4118          
c   -- var.elim.:  1000/1194          
c   -- var.elim.:  1194/1194          
c |     89537 |   47154   128482 |      --   67133       --      -- |     --   | -766/-1323
c |     89537 |   47154   128482 |   18861   52511  8430356   160.5 | 78.804 % |
c |     89639 |   47154   128482 |   20747   16753  1938224   115.7 | 79.643 % |
c |     89789 |   47154   128482 |   22822   16903  1964912   116.2 | 79.643 % |
c |     90014 |   47073   127781 |   25061   17121  1976130   115.4 | 79.883 % |
c |     90352 |   47071   127757 |   27566   17448  1988528   114.0 | 79.889 % |
c |     90859 |   47032   127445 |   30298   17954  2084105   116.1 | 79.992 % |
c |     91618 |   47000   127166 |   33305   18702  2219693   118.7 | 80.076 % |
c |     92757 |   47000   127166 |   36635   19841  2590446   130.6 | 80.076 % |
c |     94465 |   47000   127166 |   40299   21549  2981579   138.4 | 80.076 % |
c |     97028 |   46970   126916 |   44301   24105  3654704   151.6 | 80.154 % |
c |    100872 |   46970   126916 |   48731   27949  4618372   165.2 | 80.154 % |
c |    106638 |   46968   126897 |   53602   33711  6084542   180.5 | 80.160 % |
c |    115288 |   46897   126323 |   58873   42323  8404049   198.6 | 80.371 % |
c |    128262 |   46693   124619 |   64478   55245 12075934   218.6 | 80.955 % |
c ==============================================================================
c (current CPU-time: 615.584 s)
c ==============================================================================
c [1mFound solution: -35[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 |    144843 |   49959   132505 |   14987   71793 16821104   234.3 | 80.955 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5698          
c   -- var.elim.:  2000/5698          
c   -- var.elim.:  3000/5698          
c   -- var.elim.:  4000/5698          
c   -- var.elim.:  5000/5698          
c   -- var.elim.:  5698/5698          
c   -- var.elim.:  1000/1985          
c   -- var.elim.:  1985/1985          
c   -- var.elim.:  99/99          
c   -- var.elim.:  101/101          
c |    144843 |   46643   126614 |      --   71793       --      -- |     --   | -3300/-5858
c |    144843 |   46643   126614 |   18657   65405 13117513   200.6 | 80.955 % |
c |    144944 |   46643   126614 |   20522   19645  2748238   139.9 | 83.356 % |
c |    145094 |   46643   126614 |   22575   19795  2774095   140.1 | 83.356 % |
c |    145319 |   46643   126614 |   24832   20020  2841641   141.9 | 83.356 % |
c |    145658 |   46643   126614 |   27316   20359  2881304   141.5 | 83.356 % |
c |    146164 |   46643   126614 |   30047   20865  3020812   144.8 | 83.356 % |
c |    146923 |   46643   126614 |   33052   21624  3193421   147.7 | 83.356 % |
c |    148062 |   46643   126614 |   36357   22763  3557726   156.3 | 83.356 % |
c |    149770 |   46610   126318 |   39965   24470  4051911   165.6 | 83.425 % |
c |    152333 |   46610   126318 |   43961   27033  4770815   176.5 | 83.425 % |
c |    156177 |   46610   126318 |   48357   30877  5782175   187.3 | 83.425 % |
c |    161943 |   46517   125531 |   53087   36602  7211980   197.0 | 83.648 % |
c |    170592 |   46346   124227 |   58181   45189  9794107   216.7 | 84.036 % |
c |    183568 |   46233   123113 |   63843   58095 13542268   233.1 | 84.334 % |
c |    203029 |   46203   122803 |   70182   77533 19940547   257.2 | 84.414 % |
c |    232222 |   45909   120322 |   76709   42786  9654962   225.7 | 85.159 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 C746 -C745 -C744 -C743 -C742 C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 C535 -C534 -C533 -C532 C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 C458 -C457 -C456 C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 C325 -C324 -C323 C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 28649
Raw data (stat): 28649 (runsolver) R 28648 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480435772 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 4988 0 0 0 980 17 0 0 25 0 1 0 480435772 22245376 4698 4294967295 134512640 134672761 3221224560 3221223088 134606420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5431 4698 603 41 0 5390 0
vsize: 21724
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 5009 0 0 0 1980 18 0 0 25 0 1 0 480435772 22503424 4719 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4719 603 41 0 5453 0
vsize: 21976
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 5029 0 0 0 2980 18 0 0 25 0 1 0 480435772 22503424 4739 4294967295 134512640 134672761 3221224560 3221222816 134621179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4739 603 41 0 5453 0
vsize: 21976
[startup+40.001 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 5035 0 0 0 3981 18 0 0 25 0 1 0 480435772 22503424 4745 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5494 4745 603 41 0 5453 0
vsize: 21976
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 5187 0 0 0 4981 18 0 0 25 0 1 0 480435772 23568384 4897 4294967295 134512640 134672761 3221224560 3221223104 134621242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5754 4897 603 41 0 5713 0
vsize: 23016
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 6460 0 0 0 5963 35 0 0 25 0 1 0 480435772 26509312 5218 4294967295 134512640 134672761 3221224560 3221223040 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6472 5218 603 41 0 6431 0
vsize: 25888
[startup+70.0028 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 6612 0 0 0 6963 35 0 0 25 0 1 0 480435772 27754496 5370 4294967295 134512640 134672761 3221224560 3221223104 134621071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6776 5370 603 41 0 6735 0
vsize: 27104
[startup+80.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 6695 0 0 0 7963 35 0 0 25 0 1 0 480435772 26894336 5301 4294967295 134512640 134672761 3221224560 3221223408 134604097 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6566 5301 603 41 0 6525 0
vsize: 26264
[startup+90.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 7368 0 0 0 8962 36 0 0 25 0 1 0 480435772 29642752 5974 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 5974 603 41 0 7196 0
vsize: 28948
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 8033 0 0 0 9961 38 0 0 25 0 1 0 480435772 32362496 6639 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7901 6639 603 41 0 7860 0
vsize: 31604
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 8848 0 0 0 10959 40 0 0 25 0 1 0 480435772 35844096 7454 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8751 7454 603 41 0 8710 0
vsize: 35004
[startup+120.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 9719 0 0 0 11956 43 0 0 25 0 1 0 480435772 39366656 8325 4294967295 134512640 134672761 3221224560 3221223824 134617892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9611 8325 603 41 0 9570 0
vsize: 38444
[startup+130.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28649
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 11336 0 0 0 12944 54 0 0 25 0 1 0 480435772 40263680 8613 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9830 8613 603 41 0 9789 0
vsize: 39320
[startup+140.009 s]
Raw data (loadavg): 1.06 0.98 0.91 2/56 28697
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 11338 0 0 0 13944 54 0 0 25 0 1 0 480435772 40263680 8615 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9830 8615 603 41 0 9789 0
vsize: 39320
[startup+150.01 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 28702
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 11342 0 0 0 14944 55 0 0 25 0 1 0 480435772 40263680 8619 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9830 8619 603 41 0 9789 0
vsize: 39320
[startup+160.01 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 28702
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 12235 0 0 0 15941 57 0 0 25 0 1 0 480435772 43929600 9512 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10725 9512 603 41 0 10684 0
vsize: 42900
[startup+170.01 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 28702
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 13288 0 0 0 16939 60 0 0 25 0 1 0 480435772 48361472 10565 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10565 603 41 0 11766 0
vsize: 47228
[startup+180.01 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 28702
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 15186 0 0 0 17928 71 0 0 25 0 1 0 480435772 50008064 10950 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12209 10950 603 41 0 12168 0
vsize: 48836
[startup+190.011 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 28702
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 15186 0 0 0 18928 71 0 0 25 0 1 0 480435772 50008064 10950 4294967295 134512640 134672761 3221224560 3221223408 134604019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12209 10950 603 41 0 12168 0
vsize: 48836
[startup+200.011 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 28702
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 15186 0 0 0 19928 72 0 0 25 0 1 0 480435772 50008064 10950 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12209 10950 603 41 0 12168 0
vsize: 48836
[startup+210.011 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 15186 0 0 0 20928 72 0 0 25 0 1 0 480435772 50008064 10950 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12209 10950 603 41 0 12168 0
vsize: 48836
[startup+220.011 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 15725 0 0 0 21927 73 0 0 25 0 1 0 480435772 52080640 11489 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12715 11489 603 41 0 12674 0
vsize: 50860
[startup+230.011 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 16403 0 0 0 22925 75 0 0 25 0 1 0 480435772 54833152 12167 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13387 12167 603 41 0 13346 0
vsize: 53548
[startup+240.011 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 17031 0 0 0 23923 77 0 0 25 0 1 0 480435772 57450496 12795 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14026 12795 603 41 0 13985 0
vsize: 56104
[startup+250.012 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 17953 0 0 0 24921 79 0 0 25 0 1 0 480435772 61231104 13717 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14949 13717 603 41 0 14908 0
vsize: 59796
[startup+260.012 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 18647 0 0 0 25919 81 0 0 25 0 1 0 480435772 64073728 14411 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15643 14411 603 41 0 15602 0
vsize: 62572
[startup+270.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 19522 0 0 0 26917 84 0 0 25 0 1 0 480435772 67571712 15286 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16497 15286 603 41 0 16456 0
vsize: 65988
[startup+280.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 20261 0 0 0 27914 86 0 0 25 0 1 0 480435772 70664192 16025 4294967295 134512640 134672761 3221224560 3221223744 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17252 16025 603 41 0 17211 0
vsize: 69008
[startup+290.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 20878 0 0 0 28913 88 0 0 25 0 1 0 480435772 73142272 16642 4294967295 134512640 134672761 3221224560 3221223684 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17857 16642 603 41 0 17816 0
vsize: 71428
[startup+300.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 21593 0 0 0 29911 90 0 0 25 0 1 0 480435772 76042240 17357 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18565 17357 603 41 0 18524 0
vsize: 74260
[startup+310.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 22181 0 0 0 30909 92 0 0 25 0 1 0 480435772 78512128 17945 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19168 17945 603 41 0 19127 0
vsize: 76672
[startup+320.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 22627 0 0 0 31908 93 0 0 25 0 1 0 480435772 80232448 18391 4294967295 134512640 134672761 3221224560 3221223600 134612606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19588 18391 603 41 0 19547 0
vsize: 78352
[startup+330.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 23210 0 0 0 32906 95 0 0 25 0 1 0 480435772 82710528 18974 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20193 18974 603 41 0 20152 0
vsize: 80772
[startup+340.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 23808 0 0 0 33904 97 0 0 25 0 1 0 480435772 85078016 19572 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20771 19572 603 41 0 20730 0
vsize: 83084
[startup+350.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 24491 0 0 0 34902 99 0 0 25 0 1 0 480435772 87941120 20255 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20255 603 41 0 21429 0
vsize: 85880
[startup+360.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 25079 0 0 0 35901 101 0 0 25 0 1 0 480435772 90267648 20843 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22038 20843 603 41 0 21997 0
vsize: 88152
[startup+370.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 25528 0 0 0 36900 102 0 0 25 0 1 0 480435772 92086272 21292 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22482 21292 603 41 0 22441 0
vsize: 89928
[startup+380.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 26084 0 0 0 37898 104 0 0 25 0 1 0 480435772 94707712 21848 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23122 21848 603 41 0 23081 0
vsize: 92488
[startup+390.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28280 0 0 0 38888 114 0 0 25 0 1 0 480435772 96825344 22406 4294967295 134512640 134672761 3221224560 3221222848 134565575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23639 22406 603 41 0 23598 0
vsize: 94556
[startup+400.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28370 0 0 0 39887 116 0 0 25 0 1 0 480435772 97112064 22476 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22476 603 41 0 23668 0
vsize: 94836
[startup+410.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28370 0 0 0 40887 116 0 0 25 0 1 0 480435772 97112064 22476 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22476 603 41 0 23668 0
vsize: 94836
[startup+420.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28370 0 0 0 41887 116 0 0 25 0 1 0 480435772 97112064 22476 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22476 603 41 0 23668 0
vsize: 94836
[startup+430.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28370 0 0 0 42886 116 0 0 25 0 1 0 480435772 97112064 22476 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22476 603 41 0 23668 0
vsize: 94836
[startup+440.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28704
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28370 0 0 0 43886 117 0 0 25 0 1 0 480435772 97112064 22476 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22476 603 41 0 23668 0
vsize: 94836
[startup+450.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28370 0 0 0 44886 117 0 0 25 0 1 0 480435772 97112064 22476 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22476 603 41 0 23668 0
vsize: 94836
[startup+460.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28370 0 0 0 45886 118 0 0 25 0 1 0 480435772 97112064 22476 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22476 603 41 0 23668 0
vsize: 94836
[startup+470.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28371 0 0 0 46886 118 0 0 25 0 1 0 480435772 97112064 22477 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22477 603 41 0 23668 0
vsize: 94836
[startup+480.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28371 0 0 0 47886 118 0 0 25 0 1 0 480435772 97112064 22477 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22477 603 41 0 23668 0
vsize: 94836
[startup+490.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 48886 118 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+500.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 49885 119 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+510.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 50885 119 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+520.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 51885 119 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+530.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 52885 120 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+540.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 53885 120 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+550.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 54885 120 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+560.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 55885 121 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+570.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 56884 121 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+580.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 57884 122 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+590.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28372 0 0 0 58884 122 0 0 25 0 1 0 480435772 97112064 22478 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22478 603 41 0 23668 0
vsize: 94836
[startup+600.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28373 0 0 0 59884 122 0 0 25 0 1 0 480435772 97112064 22479 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22479 603 41 0 23668 0
vsize: 94836
[startup+610.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 28375 0 0 0 60884 122 0 0 25 0 1 0 480435772 97112064 22481 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23709 22481 603 41 0 23668 0
vsize: 94836
[startup+620.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30281 0 0 0 61871 135 0 0 25 0 1 0 480435772 98549760 22938 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24060 22938 603 41 0 24019 0
vsize: 96240
[startup+630.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 62871 135 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+640.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 63871 136 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223600 134603548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+650.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 64871 136 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+660.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 65871 136 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+670.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 66871 136 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+680.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 67871 136 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+690.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 68871 137 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+700.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 69870 137 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+710.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 70870 137 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+720.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 71870 138 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+730.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 72870 138 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+740.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 73870 139 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+750.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 74870 139 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+760.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 75870 139 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+770.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 76869 140 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+780.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 77869 140 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+790.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 78869 140 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+800.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 79869 141 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+810.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 80868 141 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+820.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 81868 141 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223684 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+830.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30321 0 0 0 82869 141 0 0 25 0 1 0 480435772 98574336 22946 4294967295 134512640 134672761 3221224560 3221223704 134616368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24066 22946 603 41 0 24025 0
vsize: 96264
[startup+840.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 30620 0 0 0 83867 142 0 0 25 0 1 0 480435772 99864576 23245 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24381 23245 603 41 0 24340 0
vsize: 97524
[startup+850.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 31146 0 0 0 84866 144 0 0 25 0 1 0 480435772 101978112 23771 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24897 23771 603 41 0 24856 0
vsize: 99588
[startup+860.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 31886 0 0 0 85863 147 0 0 25 0 1 0 480435772 105058304 24511 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25649 24511 603 41 0 25608 0
vsize: 102596
[startup+870.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 32517 0 0 0 86862 149 0 0 25 0 1 0 480435772 107667456 25142 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26286 25142 603 41 0 26245 0
vsize: 105144
[startup+880.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 32952 0 0 0 87861 150 0 0 25 0 1 0 480435772 109477888 25577 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26728 25577 603 41 0 26687 0
vsize: 106912
[startup+890.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 33554 0 0 0 88860 151 0 0 25 0 1 0 480435772 111935488 26179 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27328 26179 603 41 0 27287 0
vsize: 109312
[startup+900.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 34069 0 0 0 89858 152 0 0 25 0 1 0 480435772 114008064 26694 4294967295 134512640 134672761 3221224560 3221223744 134616005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27834 26694 603 41 0 27793 0
vsize: 111336
[startup+910.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 34391 0 0 0 90857 154 0 0 25 0 1 0 480435772 115318784 27016 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28154 27016 603 41 0 28113 0
vsize: 112616
[startup+920.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 34810 0 0 0 91857 155 0 0 25 0 1 0 480435772 116998144 27435 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28564 27435 603 41 0 28523 0
vsize: 114256
[startup+930.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 35106 0 0 0 92856 155 0 0 25 0 1 0 480435772 118296576 27731 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28881 27731 603 41 0 28840 0
vsize: 115524
[startup+940.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 35638 0 0 0 93855 157 0 0 25 0 1 0 480435772 120360960 28263 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29385 28263 603 41 0 29344 0
vsize: 117540
[startup+950.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36036 0 0 0 94853 158 0 0 25 0 1 0 480435772 122060800 28661 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29800 28661 603 41 0 29759 0
vsize: 119200
[startup+960.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 95853 159 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+970.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 96853 159 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223600 134603517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+980.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 97853 160 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+990.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 98853 160 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 99852 160 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223704 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 100852 161 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 101853 161 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 102853 161 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 103853 161 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 104853 161 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 105852 161 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 106852 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 107852 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 108852 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 109852 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 110852 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 111852 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 112853 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 113853 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 114853 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 115853 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 116853 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 117853 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 118853 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 28706
Raw data (stat): 28649 (minisat+) R 28648 23176 23175 0 -1 0 36296 0 0 0 119854 162 0 0 25 0 1 0 480435772 122667008 28836 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29948 28836 603 41 0 29907 0
vsize: 119792
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 28706
Raw data (stat): 28649 (minisat+) Z 28648 23176 23175 0 -1 12 36297 0 0 0 119854 170 0 0 25 0 1 0 480435772 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.25
CPU user time (s): 1198.54
CPU system time (s): 1.70174
CPU usage (%): 100.011
Max. virtual memory (Kb): 119792
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####