PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8e1.opb
MD5SUM	979ebd144bbd2b562b23479b90a02c66
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	343
Optimality of the best value was proved	NO
Number of terms in the objective function	1040
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	1040
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1040
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	1040
Total number of constraints	3656
Number of constraints which are clauses	3656
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	10
Trace number 5512

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901388 kB
Buffers:         34876 kB
Cached:          78684 kB
SwapCached:          0 kB
Active:          54112 kB
Inactive:        62332 kB
HighTotal:      131008 kB
HighFree:        48524 kB
LowTotal:       903652 kB
LowFree:        852864 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11096 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:37:28 (client local time) WITH STATUS 10 IN 1200.35 SECONDS
stats: 3935 7 1200.35 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3656 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 |    3656     8440 |    1096       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1030          
c   -- var.elim.:  1030/1030          
c |         0 |    3656     8440 |    1462       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.114982 s)
c ==============================================================================
c [1mFound solution: 476[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:56938     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        23 |   70954   165783 |   21286      23      207     9.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/45021          
c   -- var.elim.:  2000/45021          
c   -- var.elim.:  3000/45021          
c   -- var.elim.:  4000/45021          
c   -- var.elim.:  5000/45021          
c   -- var.elim.:  6000/45021          
c   -- var.elim.:  7000/45021          
c   -- var.elim.:  8000/45021          
c   -- var.elim.:  9000/45021          
c   -- var.elim.:  10000/45021          
c   -- var.elim.:  11000/45021          
c   -- var.elim.:  12000/45021          
c   -- var.elim.:  13000/45021          
c   -- var.elim.:  14000/45021          
c   -- var.elim.:  15000/45021          
c   -- var.elim.:  16000/45021          
c   -- var.elim.:  17000/45021          
c   -- var.elim.:  18000/45021          
c   -- var.elim.:  19000/45021          
c   -- var.elim.:  20000/45021          
c   -- var.elim.:  21000/45021          
c   -- var.elim.:  22000/45021          
c   -- var.elim.:  23000/45021          
c   -- var.elim.:  24000/45021          
c   -- var.elim.:  25000/45021          
c   -- var.elim.:  26000/45021          
c   -- var.elim.:  27000/45021          
c   -- var.elim.:  28000/45021          
c   -- var.elim.:  29000/45021          
c   -- var.elim.:  30000/45021          
c   -- var.elim.:  31000/45021          
c   -- var.elim.:  32000/45021          
c   -- var.elim.:  33000/45021          
c   -- var.elim.:  34000/45021          
c   -- var.elim.:  35000/45021          
c   -- var.elim.:  36000/45021          
c   -- var.elim.:  37000/45021          
c   -- var.elim.:  38000/45021          
c   -- var.elim.:  39000/45021          
c   -- var.elim.:  40000/45021          
c   -- var.elim.:  41000/45021          
c   -- var.elim.:  42000/45021          
c   -- var.elim.:  43000/45021          
c   -- var.elim.:  44000/45021          
c   -- var.elim.:  45000/45021          
c   -- var.elim.:  45021/45021          
c   -- var.elim.:  1000/22327          
c   -- var.elim.:  2000/22327          
c   -- var.elim.:  3000/22327          
c   -- var.elim.:  4000/22327          
c   -- var.elim.:  5000/22327          
c   -- var.elim.:  6000/22327          
c   -- var.elim.:  7000/22327          
c   -- var.elim.:  8000/22327          
c   -- var.elim.:  9000/22327          
c   -- var.elim.:  10000/22327          
c   -- var.elim.:  11000/22327          
c   -- var.elim.:  12000/22327          
c   -- var.elim.:  13000/22327          
c   -- var.elim.:  14000/22327          
c   -- var.elim.:  15000/22327          
c   -- var.elim.:  16000/22327          
c   -- var.elim.:  17000/22327          
c   -- var.elim.:  18000/22327          
c   -- var.elim.:  19000/22327          
c   -- var.elim.:  20000/22327          
c   -- var.elim.:  21000/22327          
c   -- var.elim.:  22000/22327          
c   -- var.elim.:  22327/22327          
c   -- var.elim.:  1000/13735          
c   -- var.elim.:  2000/13735          
c   -- var.elim.:  3000/13735          
c   -- var.elim.:  4000/13735          
c   -- var.elim.:  5000/13735          
c   -- var.elim.:  6000/13735          
c   -- var.elim.:  7000/13735          
c   -- var.elim.:  8000/13735          
c   -- var.elim.:  9000/13735          
c   -- var.elim.:  10000/13735          
c   -- var.elim.:  11000/13735          
c   -- var.elim.:  12000/13735          
c   -- var.elim.:  13000/13735          
c   -- var.elim.:  13735/13735          
c   -- var.elim.:  1000/10110          
c   -- var.elim.:  2000/10110          
c   -- var.elim.:  3000/10110          
c   -- var.elim.:  4000/10110          
c   -- var.elim.:  5000/10110          
c   -- var.elim.:  6000/10110          
c   -- var.elim.:  7000/10110          
c   -- var.elim.:  8000/10110          
c   -- var.elim.:  9000/10110          
c   -- var.elim.:  10000/10110          
c   -- var.elim.:  10110/10110          
c   -- var.elim.:  1000/8244          
c   -- var.elim.:  2000/8244          
c   -- var.elim.:  3000/8244          
c   -- var.elim.:  4000/8244          
c   -- var.elim.:  5000/8244          
c   -- var.elim.:  6000/8244          
c   -- var.elim.:  7000/8244          
c   -- var.elim.:  8000/8244          
c   -- var.elim.:  8244/8244          
c   -- var.elim.:  1000/6967          
c   -- var.elim.:  2000/6967          
c   -- var.elim.:  3000/6967          
c   -- var.elim.:  4000/6967          
c   -- var.elim.:  5000/6967          
c   -- var.elim.:  6000/6967          
c   -- var.elim.:  6967/6967          
c   -- var.elim.:  1000/6944          
c   -- var.elim.:  2000/6944          
c   -- var.elim.:  3000/6944          
c   -- var.elim.:  4000/6944          
c   -- var.elim.:  5000/6944          
c   -- var.elim.:  6000/6944          
c   -- var.elim.:  6944/6944          
c   -- var.elim.:  1000/2505          
c   -- var.elim.:  2000/2505          
c   -- var.elim.:  2505/2505          
c   -- var.elim.:  1000/3743          
c   -- var.elim.:  2000/3743          
c   -- var.elim.:  3000/3743          
c   -- var.elim.:  3743/3743          
c   -- subsuming                       
c   -- var.elim.:  1000/7122          
c   -- var.elim.:  2000/7122          
c   -- var.elim.:  3000/7122          
c   -- var.elim.:  4000/7122          
c   -- var.elim.:  5000/7122          
c   -- var.elim.:  6000/7122          
c   -- var.elim.:  7000/7122          
c   -- var.elim.:  7122/7122          
c   -- var.elim.:  136/136          
c |        23 |   22429   173982 |      --      23       --      -- |     --   | -48484/8325
c |        23 |   22429   173982 |    8971      23      207     9.0 |  0.000 % |
c |       123 |   22065   171108 |    9708     109    11883   109.0 |  1.883 % |
c |       273 |   21826   169001 |   10563     249    28956   116.3 |  2.962 % |
c |       498 |   21687   167729 |   11546     470    49524   105.4 |  3.573 % |
c |       835 |   21573   166806 |   12634     801    96901   121.0 |  4.072 % |
c |      1341 |   21230   163764 |   13676    1295   177871   137.4 |  5.660 % |
c ==============================================================================
c (current CPU-time: 180.208 s)
c ==============================================================================
c [1mFound solution: 433[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 |      1843 |   69835   282383 |   20950    1794   355656   198.2 |  5.660 % |
c   -- subsuming                       
c   -- var.elim.:  1000/43736          
c   -- var.elim.:  2000/43736          
c   -- var.elim.:  3000/43736          
c   -- var.elim.:  4000/43736          
c   -- var.elim.:  5000/43736          
c   -- var.elim.:  6000/43736          
c   -- var.elim.:  7000/43736          
c   -- var.elim.:  8000/43736          
c   -- var.elim.:  9000/43736          
c   -- var.elim.:  10000/43736          
c   -- var.elim.:  11000/43736          
c   -- var.elim.:  12000/43736          
c   -- var.elim.:  13000/43736          
c   -- var.elim.:  14000/43736          
c   -- var.elim.:  15000/43736          
c   -- var.elim.:  16000/43736          
c   -- var.elim.:  17000/43736          
c   -- var.elim.:  18000/43736          
c   -- var.elim.:  19000/43736          
c   -- var.elim.:  20000/43736          
c   -- var.elim.:  21000/43736          
c   -- var.elim.:  22000/43736          
c   -- var.elim.:  23000/43736          
c   -- var.elim.:  24000/43736          
c   -- var.elim.:  25000/43736          
c   -- var.elim.:  26000/43736          
c   -- var.elim.:  27000/43736          
c   -- var.elim.:  28000/43736          
c   -- var.elim.:  29000/43736          
c   -- var.elim.:  30000/43736          
c   -- var.elim.:  31000/43736          
c   -- var.elim.:  32000/43736          
c   -- var.elim.:  33000/43736          
c   -- var.elim.:  34000/43736          
c   -- var.elim.:  35000/43736          
c   -- var.elim.:  36000/43736          
c   -- var.elim.:  37000/43736          
c   -- var.elim.:  38000/43736          
c   -- var.elim.:  39000/43736          
c   -- var.elim.:  40000/43736          
c   -- var.elim.:  41000/43736          
c   -- var.elim.:  42000/43736          
c   -- var.elim.:  43000/43736          
c   -- var.elim.:  43736/43736          
c   -- var.elim.:  1000/21126          
c   -- var.elim.:  2000/21126          
c   -- var.elim.:  3000/21126          
c   -- var.elim.:  4000/21126          
c   -- var.elim.:  5000/21126          
c   -- var.elim.:  6000/21126          
c   -- var.elim.:  7000/21126          
c   -- var.elim.:  8000/21126          
c   -- var.elim.:  9000/21126          
c   -- var.elim.:  10000/21126          
c   -- var.elim.:  11000/21126          
c   -- var.elim.:  12000/21126          
c   -- var.elim.:  13000/21126          
c   -- var.elim.:  14000/21126          
c   -- var.elim.:  15000/21126          
c   -- var.elim.:  16000/21126          
c   -- var.elim.:  17000/21126          
c   -- var.elim.:  18000/21126          
c   -- var.elim.:  19000/21126          
c   -- var.elim.:  20000/21126          
c   -- var.elim.:  21000/21126          
c   -- var.elim.:  21126/21126          
c   -- var.elim.:  1000/12800          
c   -- var.elim.:  2000/12800          
c   -- var.elim.:  3000/12800          
c   -- var.elim.:  4000/12800          
c   -- var.elim.:  5000/12800          
c   -- var.elim.:  6000/12800          
c   -- var.elim.:  7000/12800          
c   -- var.elim.:  8000/12800          
c   -- var.elim.:  9000/12800          
c   -- var.elim.:  10000/12800          
c   -- var.elim.:  11000/12800          
c   -- var.elim.:  12000/12800          
c   -- var.elim.:  12800/12800          
c   -- var.elim.:  1000/10735          
c   -- var.elim.:  2000/10735          
c   -- var.elim.:  3000/10735          
c   -- var.elim.:  4000/10735          
c   -- var.elim.:  5000/10735          
c   -- var.elim.:  6000/10735          
c   -- var.elim.:  7000/10735          
c   -- var.elim.:  8000/10735          
c   -- var.elim.:  9000/10735          
c   -- var.elim.:  10000/10735          
c   -- var.elim.:  10735/10735          
c   -- var.elim.:  1000/8921          
c   -- var.elim.:  2000/8921          
c   -- var.elim.:  3000/8921          
c   -- var.elim.:  4000/8921          
c   -- var.elim.:  5000/8921          
c   -- var.elim.:  6000/8921          
c   -- var.elim.:  7000/8921          
c   -- var.elim.:  8000/8921          
c   -- var.elim.:  8921/8921          
c   -- var.elim.:  1000/6995          
c   -- var.elim.:  2000/6995          
c   -- var.elim.:  3000/6995          
c   -- var.elim.:  4000/6995          
c   -- var.elim.:  5000/6995          
c   -- var.elim.:  6000/6995          
c   -- var.elim.:  6995/6995          
c   -- var.elim.:  1000/6170          
c   -- var.elim.:  2000/6170          
c   -- var.elim.:  3000/6170          
c   -- var.elim.:  4000/6170          
c   -- var.elim.:  5000/6170          
c   -- var.elim.:  6000/6170          
c   -- var.elim.:  6170/6170          
c   -- var.elim.:  1000/5613          
c   -- var.elim.:  2000/5613          
c   -- var.elim.:  3000/5613          
c   -- var.elim.:  4000/5613          
c   -- var.elim.:  5000/5613          
c   -- var.elim.:  5613/5613          
c   -- var.elim.:  1000/3460          
c   -- var.elim.:  2000/3460          
c   -- var.elim.:  3000/3460          
c   -- var.elim.:  3460/3460          
c   -- var.elim.:  310/310          
c   -- var.elim.:  37/37          
c   -- subsuming                       
c   -- var.elim.:  1000/5859          
c   -- var.elim.:  2000/5859          
c   -- var.elim.:  3000/5859          
c   -- var.elim.:  4000/5859          
c   -- var.elim.:  5000/5859          
c   -- var.elim.:  5859/5859          
c   -- var.elim.:  88/88          
c |      1843 |   21881   192660 |      --    1794       --      -- |     --   | -47911/-89636
c |      1843 |   21881   192660 |    8752    1411   106197    75.3 |  5.660 % |
c |      1943 |   21814   191925 |    9598    1508   115368    76.5 |  9.414 % |
c |      2096 |   21427   187713 |   10370    1644   161343    98.1 | 11.060 % |
c |      2321 |   21427   187713 |   11407    1869   286561   153.3 | 11.060 % |
c |      2658 |   21226   185314 |   12430    2195   330152   150.4 | 11.940 % |
c |      3164 |   20902   181553 |   13465    2680   459649   171.5 | 13.328 % |
c |      3923 |   20587   177963 |   14588    3422   563682   164.7 | 14.667 % |
c |      5062 |   20239   173933 |   15776    4532   756052   166.8 | 16.198 % |
c |      6772 |   20014   171037 |   17160    6215  1143956   184.1 | 17.212 % |
c |      9334 |   20014   171037 |   18876    8777  1961523   223.5 | 17.212 % |
c |     13179 |   20014   171037 |   20764   12622  5067892   401.5 | 17.212 % |
c |     18949 |   20014   171037 |   22840   18392  7968117   433.2 | 17.212 % |
c |     27598 |   20014   171037 |   25125   27041 12112441   447.9 | 17.212 % |
c |     40572 |   19942   170327 |   27538   25832 10235601   396.2 | 17.518 % |
c |     60033 |   19891   169809 |   30214   28145 13780112   489.6 | 17.748 % |
c |     89226 |   19891   169809 |   33235   32373 23575061   728.2 | 17.748 % |
c |    133017 |   19861   169528 |   36504   24599 30783245  1251.4 | 17.863 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 x3 -x4 x5 -x6 -x7 -x8 x9 -x10 -x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 -x29 x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 -x43 x44 x45 -x46 x47 -x48 -x49 x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 -x65 x66 x67 -x68 x69 -x70 -x71 -x72 x73 -x74 -x75 x76 x77 -x78 -x79 -x80 x81 -x82 -x83 -x84 x85 -x86 -x87 -x88 x89 -x90 -x91 x92 -x93 -x94 x95 -x96 -x97 x98 x99 -x100 -x101 -x102 x103 -x104 -x105 -x106 x107 -x108 x109 -x110 -x111 x112 -x113 -x114 x115 -x116 x117 -x118 -x119 -x120 x121 -x122 -x123 x124 -x125 -x126 x127 -x128 -x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 -x157 x158 x159 -x160 x161 -x162 -x163 x164 x165 -x166 -x167 x168 x169 -x170 -x171 -x172 -x173 x174 x175 -x176 -x177 -x178 x179 -x180 -x181 x182 x183 -x184 x185 -x186 -x187 x188 x189 -x190 -x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 -x203 x204 x205 -x206 x207 -x208 -x209 x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 -x235 x236 -x237 -x238 x239 -x240 -x241 x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 -x261 x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 -x273 x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 -x317 x318 x319 -x320 -x321 x322 x323 -x324 -x325 x326 -x327 x328 -x329 x330 -x331 x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 x342 -x343 -x344 -x345 x346 -x347 x348 -x349 x350 -x351 x352 -x353 -x354 -x355 x356 x357 -x358 -x359 -x360 -x361 x362 -x363 x364 -x365 x366 -x367 x368 -x369 -x370 -x371 x372 -x373 x374 -x375 x376 -x377 x378 x379 -x380 -x381 x382 -x383 x384 -x385 x386 -x387 x388 -x389 x390 -x391 x392 -x393 x394 -x395 x396 x397 -x398 -x399 x400 -x401 -x402 -x403 x404 -x405 x406 -x407 x408 -x409 x410 -x411 x412 -x413 x414 -x415 x416 -x417 x418 x419 -x420 -x421 x422 -x423 x424 -x425 x426 -x427 x428 -x429 x430 -x431 x432 -x433 x434 -x435 x436 x437 -x438 -x439 x440 -x441 -x442 -x443 x444 -x445 x446 -x447 x448 -x449 -x450 -x451 x452 -x453 x454 -x455 x456 -x457 x458 x459 -x460 -x461 x462 -x463 x464 -x465 x466 -x467 x468 -x469 x470 -x471 x472 -x473 x474 -x475 x476 x477 -x478 -x479 x480 -x481 x482 -x483 -x484 -x485 x486 -x487 x488 -x489 x490 -x491 x492 -x493 -x494 x495 -x496 -x497 x498 -x499 x500 -x501 x502 -x503 x504 -x505 x506 -x507 x508 -x509 x510 -x511 x512 -x513 x514 -x515 x516 -x517 x518 x519 -x520 -x521 x522 -x523 x524 -x525 x526 -x527 x528 -x529 -x530 -x531 x532 -x533 x534 -x535 x536 -x537 x538 x539 -x540 -x541 x542 -x543 x544 -x545 x546 -x547 x548 -x549 -x550 -x551 x552 -x553 x554 -x555 x556 -x557 x558 x559 -x560 -x561 -x562 x563 -x564 -x565 x566 -x567 x568 -x569 -x570 -x571 x572 -x573 -x574 -x575 -x576 -x577 x578 -x579 -x580 x581 -x582 -x583 x584 -x585 -x586 -x587 x588 -x589 -x590 -x591 x592 -x593 x594 -x595 x596 -x597 x598 -x599 -x600 -x601 -x602 -x603 x604 x605 -x606 -x607 x608 -x609 -x610 -x611 x612 -x613 x614 -x615 x616 -x617 x618 -x619 -x620 -x621 x622 -x623 x624 -x625 x626 -x627 x628 -x629 x630 -x631 x632 -x633 x634 -x635 x636 x637 -x638 -x639 x640 -x641 -x642 -x643 x644 -x645 x646 -x647 x648 -x649 x650 -x651 x652 -x653 x654 -x655 x656 -x657 x658 x659 -x660 -x661 x662 x663 -x664 -x665 x666 -x667 x668 -x669 x670 -x671 x672 -x673 -x674 -x675 x676 -x677 -x678 -x679 x680 -x681 -x682 -x683 -x684 -x685 x686 -x687 x688 -x689 x690 -x691 x692 -x693 -x694 -x695 x696 -x697 x698 x699 -x700 -x701 -x702 x703 -x704 -x705 x706 -x707 x708 -x709 -x710 -x711 x712 -x713 -x714 -x715 -x716 -x717 x718 -x719 -x720 -x721 x722 -x723 x724 -x725 x726 -x727 x728 -x729 -x730 -x731 x732 -x733 x734 -x735 x736 -x737 x738 x739 -x740 -x741 x742 -x743 x744 -x745 x746 -x747 x748 -x749 x750 -x751 x752 -x753 x754 -x755 x756 x757 -x758 -x759 x760 -x761 x762 -x763 x764 -x765 x766 -x767 x768 x769 -x770 -x771 x772 -x773 x774 -x775 x776 -x777 x778 -x779 -x780 -x781 x782 x783 -x784 -x785 x786 -x787 x788 -x789 x790 -x791 x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 x802 -x803 -x804 -x805 x806 -x807 x808 -x809 x810 -x811 -x812 x813 -x814 -x815 -x816 -x817 x818 -x819 x820 -x821 -x822 x823 -x824 -x825 x826 -x827 x828 -x829 x830 -x831 x832 -x833 -x834 -x835 -x836 -x837 x838 -x839 -x840 -x841 x842 -x843 x844 -x845 x846 -x847 x848 x849 -x850 -x851 x852 -x853 x854 -x855 x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 x866 -x867 x868 -x869 x870 -x871 x872 x873 -x874 -x875 -x876 -x877 x878 -x879 -x880 -x881 x882 -x883 x884 -x885 x886 -x887 x888 -x889 x890 -x891 x892 -x893 x894 -x895 x896 x897 -x898 -x899 x900 -x901 -x902 -x903 x904 -x905 -x906 -x907 x908 -x909 -x910 -x911 x912 -x913 x914 -x915 x916 -x917 x918 x919 -x920 -x921 x922 -x923 x924 -x925 x926 -x927 x928 -x929 x930 -x931 x932 -x933 x934 -x935 x936 x937 -x938 -x939 x940 -x941 x942 -x943 x944 -x945 x946 -x947 -x948 -x949 -x950 -x951 x952 -x953 x954 -x955 x956 -x957 -x958 x959 -x960 -x961 x962 -x963 x964 -x965 x966 -x967 x968 -x969 x970 -x971 x972 -x973 x974 -x975 x976 x977 -x978 -x979 x980 -x981 x982 -x983 x984 -x985 x986 -x987 x988 -x989 -x990 -x991 x992 -x993 x994 -x995 x996 -x997 -x998 x999 -x1000 -x1001 x1002 -x1003 -x1004 -x1005 x1006 -x1007 x1008 -x1009 x1010 -x1011 x1012 -x1013 -x1014 -x1015 -x1016 x1017 -x1018 -x1019 x1020 -x1021 x1022 x1023 -x1024 -x1025 x1026 -x1027 x1028 -x1029 x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036#### 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.91 0.95 0.90 2/54 10487
Raw data (stat): 10487 (runsolver) R 10486 5897 5896 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 421981055 1052672 97 4294967295 134512640 135381576 3221224464 3221219904 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+9.99991 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 6899 0 0 0 974 24 0 0 25 0 1 0 421981055 31719424 6630 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7744 6630 603 41 0 7703 0
vsize: 30976
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 6904 0 0 0 1974 24 0 0 25 0 1 0 421981055 31719424 6635 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7744 6635 603 41 0 7703 0
vsize: 30976
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 6904 0 0 0 2974 24 0 0 25 0 1 0 421981055 31719424 6635 4294967295 134512640 134672761 3221224576 3221223024 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7744 6635 603 41 0 7703 0
vsize: 30976
[startup+40.0004 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 6904 0 0 0 3975 24 0 0 25 0 1 0 421981055 31719424 6635 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7744 6635 603 41 0 7703 0
vsize: 30976
[startup+50.001 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 6904 0 0 0 4975 24 0 0 25 0 1 0 421981055 31719424 6635 4294967295 134512640 134672761 3221224576 3221223024 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7744 6635 603 41 0 7703 0
vsize: 30976
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7027 0 0 0 5974 25 0 0 25 0 1 0 421981055 32092160 6714 4294967295 134512640 134672761 3221224576 3221223088 134635829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7835 6714 603 41 0 7794 0
vsize: 31340
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7081 0 0 0 6962 37 0 0 25 0 1 0 421981055 32223232 6755 4294967295 134512640 134672761 3221224576 3221223024 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7867 6755 603 41 0 7826 0
vsize: 31468
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7082 0 0 0 7958 41 0 0 25 0 1 0 421981055 32223232 6756 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7867 6756 603 41 0 7826 0
vsize: 31468
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7082 0 0 0 8957 42 0 0 25 0 1 0 421981055 32223232 6756 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7867 6756 603 41 0 7826 0
vsize: 31468
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7082 0 0 0 9957 43 0 0 25 0 1 0 421981055 32223232 6756 4294967295 134512640 134672761 3221224576 3221223024 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7867 6756 603 41 0 7826 0
vsize: 31468
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7083 0 0 0 10957 43 0 0 25 0 1 0 421981055 32223232 6757 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7867 6757 603 41 0 7826 0
vsize: 31468
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7083 0 0 0 11957 43 0 0 25 0 1 0 421981055 32223232 6757 4294967295 134512640 134672761 3221224576 3221223024 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7867 6757 603 41 0 7826 0
vsize: 31468
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7083 0 0 0 12957 44 0 0 25 0 1 0 421981055 32223232 6757 4294967295 134512640 134672761 3221224576 3221223024 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7867 6757 603 41 0 7826 0
vsize: 31468
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7083 0 0 0 13957 44 0 0 25 0 1 0 421981055 31961088 6713 4294967295 134512640 134672761 3221224576 3221223040 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7803 6713 603 41 0 7762 0
vsize: 31212
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7083 0 0 0 14957 44 0 0 25 0 1 0 421981055 31961088 6713 4294967295 134512640 134672761 3221224576 3221222944 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7803 6713 603 41 0 7762 0
vsize: 31212
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7153 0 0 0 15957 44 0 0 25 0 1 0 421981055 32378880 6783 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7905 6783 603 41 0 7864 0
vsize: 31620
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7153 0 0 0 16957 44 0 0 25 0 1 0 421981055 31961088 6713 4294967295 134512640 134672761 3221224576 3221223024 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7803 6713 603 41 0 7762 0
vsize: 31212
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 7162 0 0 0 17957 44 0 0 25 0 1 0 421981055 31961088 6722 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7803 6722 603 41 0 7762 0
vsize: 31212
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 10673 0 0 0 18941 60 0 0 25 0 1 0 421981055 42708992 8745 4294967295 134512640 134672761 3221224576 3221223120 134621035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10427 8745 603 41 0 10386 0
vsize: 41708
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11115 0 0 0 19931 69 0 0 25 0 1 0 421981055 43757568 8992 4294967295 134512640 134672761 3221224576 3221223024 134643468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10683 8992 603 41 0 10642 0
vsize: 42732
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11179 0 0 0 20927 73 0 0 25 0 1 0 421981055 44007424 9056 4294967295 134512640 134672761 3221224576 3221223024 134643624 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10744 9056 603 41 0 10703 0
vsize: 42976
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11179 0 0 0 21927 73 0 0 25 0 1 0 421981055 44007424 9056 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10744 9056 603 41 0 10703 0
vsize: 42976
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 22927 73 0 0 25 0 1 0 421981055 44023808 9035 4294967295 134512640 134672761 3221224576 3221223024 134643545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10748 9035 603 41 0 10707 0
vsize: 42992
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 23922 78 0 0 25 0 1 0 421981055 44023808 9035 4294967295 134512640 134672761 3221224576 3221223024 134643771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10748 9035 603 41 0 10707 0
vsize: 42992
[startup+250.009 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 24917 84 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+260.008 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 25914 87 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134643532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+270.009 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 26913 88 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+280.01 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 27911 90 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+290.01 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 28911 91 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+300.01 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 29909 92 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134643969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+310.011 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 30910 92 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+320.011 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 31910 92 0 0 25 0 1 0 421981055 43905024 9032 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10719 9032 603 41 0 10678 0
vsize: 42876
[startup+330.011 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 32910 92 0 0 25 0 1 0 421981055 43642880 8989 4294967295 134512640 134672761 3221224576 3221223068 134642885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10655 8989 603 41 0 10614 0
vsize: 42620
[startup+340.011 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11201 0 0 0 33910 92 0 0 25 0 1 0 421981055 43642880 8989 4294967295 134512640 134672761 3221224576 3221223068 134643016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10655 8989 603 41 0 10614 0
vsize: 42620
[startup+350.012 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11270 0 0 0 34910 92 0 0 25 0 1 0 421981055 44060672 9058 4294967295 134512640 134672761 3221224576 3221223120 134621065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10757 9058 603 41 0 10716 0
vsize: 43028
[startup+360.012 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11270 0 0 0 35910 92 0 0 25 0 1 0 421981055 43642880 8989 4294967295 134512640 134672761 3221224576 3221223024 134643987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10655 8989 603 41 0 10614 0
vsize: 42620
[startup+370.013 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11270 0 0 0 36910 92 0 0 25 0 1 0 421981055 43642880 8989 4294967295 134512640 134672761 3221224576 3221223720 134616254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10655 8989 603 41 0 10614 0
vsize: 42620
[startup+380.013 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 11449 0 0 0 37910 93 0 0 25 0 1 0 421981055 44421120 9168 4294967295 134512640 134672761 3221224576 3221223040 134566562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10845 9168 603 41 0 10804 0
vsize: 43380
[startup+390.014 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 13272 0 0 0 38906 97 0 0 25 0 1 0 421981055 51924992 10991 4294967295 134512640 134672761 3221224576 3221223584 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12677 10991 603 41 0 12636 0
vsize: 50708
[startup+400.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 15873 0 0 0 39902 101 0 0 25 0 1 0 421981055 62545920 13592 4294967295 134512640 134672761 3221224576 3221223760 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15270 13592 603 41 0 15229 0
vsize: 61080
[startup+410.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 17932 0 0 0 40897 106 0 0 25 0 1 0 421981055 71098368 15651 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17358 15651 603 41 0 17317 0
vsize: 69432
[startup+420.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 19417 0 0 0 41895 109 0 0 25 0 1 0 421981055 77115392 17136 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18827 17136 603 41 0 18786 0
vsize: 75308
[startup+430.016 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 21414 0 0 0 42889 115 0 0 25 0 1 0 421981055 85291008 19133 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20823 19133 603 41 0 20782 0
vsize: 83292
[startup+440.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 22661 0 0 0 43887 117 0 0 25 0 1 0 421981055 90337280 20380 4294967295 134512640 134672761 3221224576 3221223760 134615764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22055 20380 603 41 0 22014 0
vsize: 88220
[startup+450.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 22661 0 0 0 44887 117 0 0 25 0 1 0 421981055 90337280 20380 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22055 20380 603 41 0 22014 0
vsize: 88220
[startup+460.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 22661 0 0 0 45887 117 0 0 25 0 1 0 421981055 90337280 20380 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22055 20380 603 41 0 22014 0
vsize: 88220
[startup+470.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 22661 0 0 0 46887 117 0 0 25 0 1 0 421981055 90337280 20380 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22055 20380 603 41 0 22014 0
vsize: 88220
[startup+480.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 23442 0 0 0 47885 120 0 0 25 0 1 0 421981055 93540352 21161 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22837 21161 603 41 0 22796 0
vsize: 91348
[startup+490.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 23475 0 0 0 48885 120 0 0 25 0 1 0 421981055 93650944 21194 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22864 21194 603 41 0 22823 0
vsize: 91456
[startup+500.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 23475 0 0 0 49885 120 0 0 25 0 1 0 421981055 93650944 21194 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22864 21194 603 41 0 22823 0
vsize: 91456
[startup+510.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 23475 0 0 0 50886 120 0 0 25 0 1 0 421981055 93650944 21194 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22864 21194 603 41 0 22823 0
vsize: 91456
[startup+520.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 24038 0 0 0 51884 121 0 0 25 0 1 0 421981055 95981568 21757 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23433 21757 603 41 0 23392 0
vsize: 93732
[startup+530.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 25307 0 0 0 52882 124 0 0 25 0 1 0 421981055 101216256 23026 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24711 23026 603 41 0 24670 0
vsize: 98844
[startup+540.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 26865 0 0 0 53878 128 0 0 25 0 1 0 421981055 107724800 24584 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26300 24584 603 41 0 26259 0
vsize: 105200
[startup+550.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 28636 0 0 0 54874 132 0 0 25 0 1 0 421981055 114888704 26355 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28049 26355 603 41 0 28008 0
vsize: 112196
[startup+560.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 55872 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+570.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 56872 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+580.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 57872 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+590.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 58872 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+600.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 59872 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+610.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 60873 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+620.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 61873 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223792 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+630.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 62873 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+640.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 30180 0 0 0 63873 135 0 0 25 0 1 0 421981055 121176064 27892 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29584 27892 603 41 0 29543 0
vsize: 118336
[startup+650.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 31026 0 0 0 64871 137 0 0 25 0 1 0 421981055 124743680 28738 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30455 28738 603 41 0 30414 0
vsize: 121820
[startup+660.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 32597 0 0 0 65868 141 0 0 25 0 1 0 421981055 131112960 30309 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32010 30309 603 41 0 31969 0
vsize: 128040
[startup+670.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 34221 0 0 0 66863 146 0 0 25 0 1 0 421981055 137768960 31933 4294967295 134512640 134672761 3221224576 3221223616 134614202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33635 31933 603 41 0 33594 0
vsize: 134540
[startup+680.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 35741 0 0 0 67860 149 0 0 25 0 1 0 421981055 144031744 33453 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35164 33453 603 41 0 35123 0
vsize: 140656
[startup+690.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 68856 153 0 0 25 0 1 0 421981055 149020672 34663 4294967295 134512640 134672761 3221224576 3221223672 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36382 34663 603 41 0 36341 0
vsize: 145528
[startup+700.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 69856 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223616 134612608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+710.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 70856 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+720.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 71857 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+730.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 72857 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+740.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 73857 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+750.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 74857 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+760.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 75857 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+770.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 76858 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+780.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36951 0 0 0 77858 153 0 0 25 0 1 0 421981055 148758528 34626 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34626 603 41 0 36277 0
vsize: 145272
[startup+790.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 36952 0 0 0 78858 153 0 0 25 0 1 0 421981055 148758528 34627 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36318 34627 603 41 0 36277 0
vsize: 145272
[startup+800.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38208 0 0 0 79856 156 0 0 25 0 1 0 421981055 153985024 35883 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37594 35883 603 41 0 37553 0
vsize: 150376
[startup+810.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 80855 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+820.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 81855 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223680 134604309 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+830.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 82856 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+840.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 83856 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+850.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 84856 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+860.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 85856 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+870.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 86856 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223616 134612578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+880.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 87857 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+890.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 38481 0 0 0 88857 156 0 0 25 0 1 0 421981055 154845184 36115 4294967295 134512640 134672761 3221224576 3221223616 134612606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37804 36115 603 41 0 37763 0
vsize: 151216
[startup+900.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 39108 0 0 0 89856 158 0 0 25 0 1 0 421981055 157519872 36742 4294967295 134512640 134672761 3221224576 3221223616 134612827 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38457 36743 603 41 0 38416 0
vsize: 153828
[startup+910.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 40328 0 0 0 90854 160 0 0 25 0 1 0 421981055 162484224 37962 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39669 37962 603 41 0 39628 0
vsize: 158676
[startup+920.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 41737 0 0 0 91851 163 0 0 25 0 1 0 421981055 168247296 39371 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41076 39371 603 41 0 41035 0
vsize: 164304
[startup+930.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 42693 0 0 0 92849 165 0 0 25 0 1 0 421981055 172122112 40327 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42022 40327 603 41 0 41981 0
vsize: 168088
[startup+940.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 44562 0 0 0 93843 171 0 0 25 0 1 0 421981055 179806208 42196 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43898 42196 603 41 0 43857 0
vsize: 175592
[startup+950.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 46013 0 0 0 94840 174 0 0 25 0 1 0 421981055 185790464 43647 4294967295 134512640 134672761 3221224576 3221223616 134612764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45359 43647 603 41 0 45318 0
vsize: 181436
[startup+960.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 47376 0 0 0 95838 176 0 0 25 0 1 0 421981055 191410176 45010 4294967295 134512640 134672761 3221224576 3221223568 134603098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46731 45010 603 41 0 46690 0
vsize: 186924
[startup+970.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 49233 0 0 0 96835 180 0 0 25 0 1 0 421981055 198963200 46867 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48575 46867 603 41 0 48534 0
vsize: 194300
[startup+980.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 50772 0 0 0 97832 183 0 0 25 0 1 0 421981055 205291520 48406 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50120 48406 603 41 0 50079 0
vsize: 200480
[startup+990.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 52388 0 0 0 98829 186 0 0 25 0 1 0 421981055 211890176 50022 4294967295 134512640 134672761 3221224576 3221223760 134615773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51731 50022 603 41 0 51690 0
vsize: 206924
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 53922 0 0 0 99827 189 0 0 25 0 1 0 421981055 218157056 51556 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53261 51556 603 41 0 53220 0
vsize: 213044
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 55222 0 0 0 100825 191 0 0 25 0 1 0 421981055 223498240 52856 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54565 52856 603 41 0 54524 0
vsize: 218260
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 56382 0 0 0 101822 194 0 0 25 0 1 0 421981055 228278272 54016 4294967295 134512640 134672761 3221224576 3221223616 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55732 54016 603 41 0 55691 0
vsize: 222928
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 57544 0 0 0 102820 196 0 0 25 0 1 0 421981055 232931328 55178 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56868 55178 603 41 0 56827 0
vsize: 227472
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 58665 0 0 0 103818 198 0 0 25 0 1 0 421981055 237547520 56299 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57995 56299 603 41 0 57954 0
vsize: 231980
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 59812 0 0 0 104817 200 0 0 25 0 1 0 421981055 242237440 57446 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59140 57446 603 41 0 59099 0
vsize: 236560
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 105817 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 106817 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 107817 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 108817 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 109818 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 110818 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 111818 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1130.04 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 112818 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1140.05 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 113818 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1150.05 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 114819 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1160.05 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 115819 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1170.05 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 116819 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1180.05 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 117819 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1190.05 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 118819 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
[startup+1200.05 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 10487
Raw data (stat): 10487 (minisat+) R 10486 5897 5896 0 -1 0 60086 0 0 0 119820 200 0 0 25 0 1 0 421981055 243150848 57676 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59363 57676 603 41 0 59322 0
vsize: 237452
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.02 1.01 0.93 1/54 10487
Raw data (stat): 10487 (minisat+) Z 10486 5897 5896 0 -1 12 60087 0 0 0 119820 214 0 0 25 0 1 0 421981055 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.19
CPU time (s): 1200.35
CPU user time (s): 1198.2
CPU system time (s): 2.14267
CPU usage (%): 100.013
Max. virtual memory (Kb): 237452
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####