PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-alu4.b.opb
MD5SUM	db06e7fbd4f70a4af68f8f196fdb3636
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50
Optimality of the best value was proved	NO
Number of terms in the objective function	808
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	808
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	808
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03884
Number of variables	807
Total number of constraints	1838
Number of constraints which are clauses	1823
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 4656

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-13 19:30:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3445 boxname=wulflinc3 idbench=61 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  db06e7fbd4f70a4af68f8f196fdb3636  /oldhome/oroussel/tmp/wulflinc3/normalized-alu4.b.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-alu4.b.opb /oldhome/oroussel/tmp/wulflinc3/normalized-alu4.b.opb
IDLAUNCH: 3445
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        917504 kB
Buffers:         34868 kB
Cached:          59368 kB
SwapCached:       3276 kB
Active:          67308 kB
Inactive:        33092 kB
HighTotal:      131008 kB
HighFree:        67592 kB
LowTotal:       903652 kB
LowFree:        849912 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11040 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:50:51 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3445 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1695 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1694    35961 |     564       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1576   maxlim: 740   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12670    75141 |    4223       0        0     nan |  0.000 % |
c |       100 |   12670    75141 |    4645     100      319     3.2 |  0.921 % |
c |       250 |   12654    75087 |    5109     244      858     3.5 |  1.005 % |
c |       475 |   12654    75087 |    5620     469     1754     3.7 |  1.005 % |
c |       812 |   12630    75002 |    6182     798     3231     4.0 |  1.130 % |
c |      1318 |   12630    75002 |    6801    1304     6597     5.1 |  1.130 % |
c |      2079 |   12571    74806 |    7481    2053    13245     6.5 |  1.591 % |
c |      3220 |   12562    74775 |    8229    3190    45421    14.2 |  1.632 % |
c |      4929 |   12553    74744 |    9052    4895   164209    33.5 |  1.674 % |
c |      7491 |   12553    74744 |    9957    7457   343990    46.1 |  1.674 % |
c ==============================================================================
c [1mFound solution: 67[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 741   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7790 |   12554    74753 |    4184    7756   359106    46.3 |  1.674 % |
c |      7890 |   12554    74753 |    4602    3978   180347    45.3 |  1.715 % |
c |      8041 |   12554    74753 |    5062    4129   181741    44.0 |  1.716 % |
c |      8266 |   12554    74753 |    5568    4354   187697    43.1 |  1.715 % |
c |      8606 |   12554    74753 |    6125    4694   201865    43.0 |  1.715 % |
c |      9114 |   12554    74753 |    6738    5202   217122    41.7 |  1.715 % |
c |      9875 |   12554    74753 |    7412    5963   261909    43.9 |  1.715 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 742   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10190 |   12557    74769 |    4185    6278   270085    43.0 |  1.715 % |
c |     10290 |   12557    74769 |    4603    3239    74611    23.0 |  1.757 % |
c |     10440 |   12541    74716 |    5063    3387    76333    22.5 |  1.924 % |
c |     10665 |   12541    74716 |    5570    3612    82233    22.8 |  1.924 % |
c |     11002 |   12541    74716 |    6127    3949    94369    23.9 |  1.924 % |
c |     11509 |   12541    74716 |    6739    4456   121021    27.2 |  1.924 % |
c |     12268 |   12541    74716 |    7413    5215   164470    31.5 |  1.924 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 744   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12419 |   12547    74749 |    4182    5366   168401    31.4 |  1.924 % |
c |     12519 |   12547    74749 |    4600    2783    71221    25.6 |  2.006 % |
c |     12671 |   12547    74749 |    5060    2935    72384    24.7 |  2.006 % |
c |     12896 |   12547    74749 |    5566    3160    75012    23.7 |  2.006 % |
c |     13234 |   12547    74749 |    6122    3498    86534    24.7 |  2.006 % |
c |     13741 |   12547    74749 |    6735    4005   105591    26.4 |  2.006 % |
c |     14500 |   12547    74749 |    7408    4764   175909    36.9 |  2.007 % |
c |     15640 |   12547    74749 |    8149    5904   253751    43.0 |  2.006 % |
c |     17349 |   12547    74749 |    8964    7613   431633    56.7 |  2.006 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 745   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17395 |   12548    74758 |    4182    7659   433697    56.6 |  2.006 % |
c |     17495 |   12548    74758 |    4600    3930   196497    50.0 |  2.047 % |
c |     17646 |   12548    74758 |    5060    4081   201498    49.4 |  2.047 % |
c |     17873 |   12548    74758 |    5566    4308   210304    48.8 |  2.047 % |
c |     18210 |   12548    74758 |    6122    4645   229547    49.4 |  2.047 % |
c |     18716 |   12548    74758 |    6735    5151   262304    50.9 |  2.047 % |
c |     19476 |   12548    74758 |    7408    5911   312116    52.8 |  2.047 % |
c |     20615 |   12548    74758 |    8149    7050   411045    58.3 |  2.047 % |
c |     22323 |   12548    74758 |    8964    8758   602124    68.8 |  2.047 % |
c |     24885 |   12548    74758 |    9860    6384   514758    80.6 |  2.047 % |
c |     28729 |   12548    74758 |   10847   10228   844289    82.5 |  2.047 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 746   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31219 |   12549    74768 |    4183    7159   477104    66.6 |  2.047 % |
c |     31320 |   12549    74768 |    4601    3681   197628    53.7 |  2.088 % |
c |     31470 |   12549    74768 |    5061    3831   201740    52.7 |  2.088 % |
c |     31695 |   12549    74768 |    5567    4056   205367    50.6 |  2.088 % |
c |     32032 |   12549    74768 |    6124    4393   230983    52.6 |  2.088 % |
c |     32539 |   12549    74768 |    6736    4900   245302    50.1 |  2.088 % |
c |     33300 |   12549    74768 |    7410    5661   307283    54.3 |  2.088 % |
c |     34439 |   12549    74768 |    8151    6800   383647    56.4 |  2.088 % |
c |     36147 |   12549    74768 |    8966    8508   464644    54.6 |  2.088 % |
c |     38710 |   12549    74768 |    9863    6222   295701    47.5 |  2.088 % |
c |     42557 |   12549    74768 |   10849   10069   897645    89.1 |  2.088 % |
c |     48325 |   12549    74768 |   11934   10226  1074419   105.1 |  2.088 % |
c |     56974 |   12549    74768 |   13128   12621  1350691   107.0 |  2.088 % |
c |     69951 |   12549    74768 |   14440   11853   779020    65.7 |  2.088 % |
c |     89414 |   12549    74768 |   15884    8620  1182730   137.2 |  2.088 % |
c ==============================================================================
c [1mFound solution: 61[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 747   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     92204 |   12550    74776 |    4183   11410  1638539   143.6 |  2.088 % |
c |     92304 |   12550    74776 |    4601    2953   275608    93.3 |  2.129 % |
c |     92454 |   12550    74776 |    5061    3103   276549    89.1 |  2.129 % |
c |     92679 |   12550    74776 |    5567    3328   278290    83.6 |  2.129 % |
c |     93018 |   12550    74776 |    6124    3667   283455    77.3 |  2.129 % |
c |     93524 |   12550    74776 |    6736    4173   295310    70.8 |  2.129 % |
c |     94283 |   12550    74776 |    7410    4932   365371    74.1 |  2.129 % |
c |     95423 |   12550    74776 |    8151    6072   422363    69.6 |  2.129 % |
c |     97132 |   12550    74776 |    8966    7781   659447    84.8 |  2.129 % |
c |     99694 |   12550    74776 |    9863    5350   426482    79.7 |  2.129 % |
c |    103541 |   12550    74776 |   10849    9197   896810    97.5 |  2.129 % |
c |    109307 |   12550    74776 |   11934    9222  1193532   129.4 |  2.129 % |
c |    117957 |   12550    74776 |   13128   11372  1315827   115.7 |  2.129 % |
c |    130934 |   12544    74756 |   14440   10623  1732813   163.1 |  2.170 % |
c |    150396 |   12544    74756 |   15884   15017  2425025   161.5 |  2.170 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 748   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165248 |   12546    74768 |    4182   12888  1789462   138.8 |  2.170 % |
c |    165348 |   12546    74768 |    4600    3322   303074    91.2 |  2.210 % |
c |    165498 |   12546    74768 |    5060    3472   304029    87.6 |  2.210 % |
c |    165723 |   12546    74768 |    5566    3697   305194    82.6 |  2.210 % |
c |    166060 |   12546    74768 |    6122    4034   311073    77.1 |  2.210 % |
c |    166566 |   12546    74768 |    6735    4540   328239    72.3 |  2.210 % |
c |    167327 |   12546    74768 |    7408    5301   430124    81.1 |  2.210 % |
c |    168466 |   12546    74768 |    8149    6440   486838    75.6 |  2.210 % |
c |    170180 |   12546    74768 |    8964    8154   750281    92.0 |  2.210 % |
c |    172742 |   12546    74768 |    9860    5747   704571   122.6 |  2.210 % |
c |    176587 |   12546    74768 |   10847    9592  1092417   113.9 |  2.210 % |
c |    182356 |   12546    74768 |   11931    9531  1181054   123.9 |  2.210 % |
c |    191006 |   12546    74768 |   13124   11943  1665908   139.5 |  2.210 % |
c |    203981 |   12546    74768 |   14437   11300  1508078   133.5 |  2.210 % |
c ==============================================================================
c [1mFound solution: 56[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 752   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    213529 |   12553    74802 |    4184   13401  1619448   120.8 |  2.210 % |
c |    213629 |   12553    74802 |    4602    3451   289213    83.8 |  2.291 % |
c |    213779 |   12553    74802 |    5062    3601   290100    80.6 |  2.291 % |
c |    214004 |   12553    74802 |    5568    3826   291564    76.2 |  2.291 % |
c |    214341 |   12553    74802 |    6125    4163   295156    70.9 |  2.291 % |
c |    214852 |   12553    74802 |    6738    4674   313664    67.1 |  2.291 % |
c |    215611 |   12553    74802 |    7412    5433   363830    67.0 |  2.291 % |
c |    216750 |   12553    74802 |    8153    6572   451171    68.7 |  2.291 % |
c |    218459 |   12553    74802 |    8968    8281   615986    74.4 |  2.291 % |
c |    221021 |   12553    74802 |    9865    5906   344605    58.3 |  2.291 % |
c |    224865 |   12553    74802 |   10852    9750   956462    98.1 |  2.291 % |
c |    230631 |   12553    74802 |   11937    9561  1363456   142.6 |  2.291 % |
c |    239281 |   12553    74802 |   13131   11902  1515197   127.3 |  2.291 % |
c |    252256 |   12553    74802 |   14444   10744  1877096   174.7 |  2.291 % |
c |    271719 |   12553    74802 |   15888   15272  2368980   155.1 |  2.291 % |
c |    300912 |   12553    74802 |   17477   11342  1852561   163.3 |  2.291 % |
c |    344702 |   12553    74802 |   19225   10138  1681969   165.9 |  2.291 % |
c |    410390 |   12553    74802 |   21147   16453  2447975   148.8 |  2.291 % |
c |    508918 |   12553    74802 |   23262   18342  3606959   196.7 |  2.291 % |
c |    656707 |   12553    74802 |   25588   23785  4087285   171.8 |  2.291 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 753   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    671311 |   12554    74811 |    4184   25096  3951559   157.5 |  2.291 % |
c |    671411 |   12554    74811 |    4602    3237   307947    95.1 |  2.331 % |
c |    671561 |   12554    74811 |    5062    3387   308957    91.2 |  2.331 % |
c |    671786 |   12554    74811 |    5568    3612   310788    86.0 |  2.331 % |
c |    672123 |   12554    74811 |    6125    3949   318830    80.7 |  2.331 % |
c |    672631 |   12554    74811 |    6738    4457   335039    75.2 |  2.331 % |
c |    673390 |   12554    74811 |    7412    5216   373147    71.5 |  2.331 % |
c |    674530 |   12554    74811 |    8153    6356   453977    71.4 |  2.331 % |
c |    676242 |   12554    74811 |    8968    8068   688568    85.3 |  2.331 % |
c |    678804 |   12554    74811 |    9865    5773   487845    84.5 |  2.331 % |
c |    682649 |   12554    74811 |   10852    9618   879773    91.5 |  2.331 % |
c |    688415 |   12554    74811 |   11937    9643  1209268   125.4 |  2.331 % |
c |    697064 |   12554    74811 |   13131   12048  1593641   132.3 |  2.331 % |
c |    710041 |   12554    74811 |   14444   11054  1633739   147.8 |  2.331 % |
c |    729502 |   12554    74811 |   15888   15285  2221357   145.3 |  2.331 % |
c |    758694 |   12554    74811 |   17477   11632  1471084   126.5 |  2.331 % |
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#### 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.14 0.03 0.01 2/54 12867
Raw data (stat): 12867 (runsolver) R 12866 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420261108 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.27 0.06 0.02 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 1195 0 0 0 994 4 0 0 25 0 1 0 420261108 6361088 1173 4294967295 134512640 134672761 3221224576 3221223776 134557777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1553 1173 603 41 0 1512 0
vsize: 6212
[startup+20.0021 s]
Raw data (loadavg): 0.38 0.09 0.03 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 1729 0 0 0 1993 5 0 0 25 0 1 0 420261108 8568832 1707 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2092 1707 603 41 0 2051 0
vsize: 8368
[startup+30.0023 s]
Raw data (loadavg): 0.48 0.12 0.04 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 1986 0 0 0 2991 6 0 0 25 0 1 0 420261108 9641984 1964 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2354 1964 603 41 0 2313 0
vsize: 9416
[startup+40.0025 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 2336 0 0 0 3990 7 0 0 25 0 1 0 420261108 11112448 2314 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2713 2314 603 41 0 2672 0
vsize: 10852
[startup+50.0029 s]
Raw data (loadavg): 0.62 0.18 0.06 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 2420 0 0 0 4990 8 0 0 25 0 1 0 420261108 11378688 2398 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2398 603 41 0 2737 0
vsize: 11112
[startup+60.0035 s]
Raw data (loadavg): 0.79 0.23 0.08 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 3345 0 0 0 5988 10 0 0 25 0 1 0 420261108 15134720 3323 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3695 3323 603 41 0 3654 0
vsize: 14780
[startup+70.004 s]
Raw data (loadavg): 0.82 0.26 0.09 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4107 0 0 0 6986 12 0 0 25 0 1 0 420261108 18350080 4085 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4480 4085 603 41 0 4439 0
vsize: 17920
[startup+80.0041 s]
Raw data (loadavg): 0.85 0.28 0.10 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 7986 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+90.0049 s]
Raw data (loadavg): 0.87 0.31 0.11 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 8986 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+100.004 s]
Raw data (loadavg): 0.89 0.33 0.12 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 9986 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+110.006 s]
Raw data (loadavg): 0.91 0.35 0.12 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 10986 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+120.006 s]
Raw data (loadavg): 0.92 0.37 0.13 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 11986 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+130.006 s]
Raw data (loadavg): 0.93 0.39 0.14 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 12987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+140.007 s]
Raw data (loadavg): 0.94 0.41 0.15 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 13987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+150.007 s]
Raw data (loadavg): 0.95 0.43 0.16 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 14987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+160.007 s]
Raw data (loadavg): 0.96 0.45 0.17 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 15987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223760 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+170.009 s]
Raw data (loadavg): 0.96 0.47 0.18 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 16987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+180.008 s]
Raw data (loadavg): 0.97 0.48 0.19 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 17987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+190.009 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 18987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+200.009 s]
Raw data (loadavg): 0.98 0.52 0.20 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 19987 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+210.01 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 20988 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+220.01 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 21988 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+230.011 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 22988 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+240.011 s]
Raw data (loadavg): 0.99 0.57 0.23 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 23988 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+250.011 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 24988 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+260.012 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 25988 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+270.012 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 26989 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+280.011 s]
Raw data (loadavg): 0.99 0.63 0.26 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 27989 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+290.013 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4302 0 0 0 28989 13 0 0 25 0 1 0 420261108 19152896 4280 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4280 603 41 0 4635 0
vsize: 18704
[startup+300.013 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4604 0 0 0 29989 13 0 0 25 0 1 0 420261108 20353024 4582 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4969 4582 603 41 0 4928 0
vsize: 19876
[startup+310.014 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4834 0 0 0 30988 14 0 0 25 0 1 0 420261108 21291008 4812 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5198 4812 603 41 0 5157 0
vsize: 20792
[startup+320.014 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4851 0 0 0 31988 14 0 0 25 0 1 0 420261108 21426176 4829 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5231 4829 603 41 0 5190 0
vsize: 20924
[startup+330.015 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4851 0 0 0 32989 14 0 0 25 0 1 0 420261108 21426176 4829 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5231 4829 603 41 0 5190 0
vsize: 20924
[startup+340.015 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4851 0 0 0 33989 14 0 0 25 0 1 0 420261108 21426176 4829 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5231 4829 603 41 0 5190 0
vsize: 20924
[startup+350.016 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4851 0 0 0 34989 14 0 0 25 0 1 0 420261108 21426176 4829 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5231 4829 603 41 0 5190 0
vsize: 20924
[startup+360.017 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4851 0 0 0 35989 14 0 0 25 0 1 0 420261108 21426176 4829 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5231 4829 603 41 0 5190 0
vsize: 20924
[startup+370.018 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4851 0 0 0 36990 14 0 0 25 0 1 0 420261108 21426176 4829 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5231 4829 603 41 0 5190 0
vsize: 20924
[startup+380.018 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 4935 0 0 0 37990 14 0 0 25 0 1 0 420261108 21696512 4913 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5297 4913 603 41 0 5256 0
vsize: 21188
[startup+390.019 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 5023 0 0 0 38989 15 0 0 25 0 1 0 420261108 22102016 5001 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 5001 603 41 0 5355 0
vsize: 21584
[startup+400.019 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 5255 0 0 0 39989 15 0 0 25 0 1 0 420261108 23048192 5233 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5627 5233 603 41 0 5586 0
vsize: 22508
[startup+410.021 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 5255 0 0 0 40989 15 0 0 25 0 1 0 420261108 23048192 5233 4294967295 134512640 134672761 3221224576 3221223680 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5627 5233 603 41 0 5586 0
vsize: 22508
[startup+420.021 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 5626 0 0 0 41989 16 0 0 25 0 1 0 420261108 24530944 5604 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5989 5604 603 41 0 5948 0
vsize: 23956
[startup+430.021 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 5632 0 0 0 42989 16 0 0 25 0 1 0 420261108 24530944 5610 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5989 5610 603 41 0 5948 0
vsize: 23956
[startup+440.021 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 5783 0 0 0 43989 16 0 0 25 0 1 0 420261108 25206784 5761 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6154 5761 603 41 0 6113 0
vsize: 24616
[startup+450.021 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6055 0 0 0 44988 17 0 0 25 0 1 0 420261108 26275840 6033 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 6033 603 41 0 6374 0
vsize: 25660
[startup+460.021 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6055 0 0 0 45989 17 0 0 25 0 1 0 420261108 26275840 6033 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6415 6033 603 41 0 6374 0
vsize: 25660
[startup+470.023 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6209 0 0 0 46989 17 0 0 25 0 1 0 420261108 26947584 6187 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6579 6187 603 41 0 6538 0
vsize: 26316
[startup+480.022 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6209 0 0 0 47989 17 0 0 25 0 1 0 420261108 26947584 6187 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6579 6187 603 41 0 6538 0
vsize: 26316
[startup+490.023 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6209 0 0 0 48989 17 0 0 25 0 1 0 420261108 26947584 6187 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6579 6187 603 41 0 6538 0
vsize: 26316
[startup+500.023 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 49989 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+510.024 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 50989 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+520.023 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 51989 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+530.024 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 52990 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223760 134559566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+540.025 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 53990 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+550.025 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 54989 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+560.025 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 55990 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+570.026 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 56990 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+580.025 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 57990 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+590.026 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 58990 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+600.026 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6248 0 0 0 59990 17 0 0 25 0 1 0 420261108 27082752 6226 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6612 6226 603 41 0 6571 0
vsize: 26448
[startup+610.026 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6554 0 0 0 60990 18 0 0 25 0 1 0 420261108 28430336 6532 4294967295 134512640 134672761 3221224576 3221223760 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6941 6532 603 41 0 6900 0
vsize: 27764
[startup+620.026 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6591 0 0 0 61990 18 0 0 25 0 1 0 420261108 28565504 6569 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6569 603 41 0 6933 0
vsize: 27896
[startup+630.025 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 62990 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+640.027 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 63990 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+650.027 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 64990 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+660.026 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 65990 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+670.027 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 66991 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+680.028 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 67991 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+690.028 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 68991 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223760 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+700.028 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6597 0 0 0 69991 18 0 0 25 0 1 0 420261108 28565504 6575 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6575 603 41 0 6933 0
vsize: 27896
[startup+710.028 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 70991 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+720.028 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 71991 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+730.028 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 72992 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+740.029 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 73992 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+750.029 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 74992 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223680 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+760.029 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 75992 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+770.029 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 76992 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223680 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+780.03 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 6626 0 0 0 77993 19 0 0 25 0 1 0 420261108 28700672 6604 4294967295 134512640 134672761 3221224576 3221223712 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7007 6604 603 41 0 6966 0
vsize: 28028
[startup+790.031 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 78991 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223680 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+800.031 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 79991 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+810.031 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 80991 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+820.032 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 81992 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+830.031 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 82992 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223760 134559553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+840.032 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 83992 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+850.033 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 84992 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+860.033 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7016 0 0 0 85992 20 0 0 25 0 1 0 420261108 30306304 6994 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6994 603 41 0 7358 0
vsize: 29596
[startup+870.033 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7024 0 0 0 86992 20 0 0 25 0 1 0 420261108 30478336 7002 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 7002 603 41 0 7400 0
vsize: 29764
[startup+880.033 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7025 0 0 0 87993 20 0 0 25 0 1 0 420261108 30478336 7003 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 7003 603 41 0 7400 0
vsize: 29764
[startup+890.033 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7025 0 0 0 88993 20 0 0 25 0 1 0 420261108 30478336 7003 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 7003 603 41 0 7400 0
vsize: 29764
[startup+900.033 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7025 0 0 0 89993 20 0 0 25 0 1 0 420261108 30478336 7003 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 7003 603 41 0 7400 0
vsize: 29764
[startup+910.033 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7025 0 0 0 90993 20 0 0 25 0 1 0 420261108 30478336 7003 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 7003 603 41 0 7400 0
vsize: 29764
[startup+920.034 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7031 0 0 0 91993 20 0 0 25 0 1 0 420261108 30478336 7009 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 7009 603 41 0 7400 0
vsize: 29764
[startup+930.034 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7171 0 0 0 92993 20 0 0 25 0 1 0 420261108 31019008 7149 4294967295 134512640 134672761 3221224576 3221223744 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7573 7149 603 41 0 7532 0
vsize: 30292
[startup+940.035 s]
Raw data (loadavg): 0.99 0.95 0.61 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7171 0 0 0 93994 20 0 0 25 0 1 0 420261108 31019008 7149 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7573 7149 603 41 0 7532 0
vsize: 30292
[startup+950.035 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7183 0 0 0 94994 20 0 0 25 0 1 0 420261108 31019008 7161 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7573 7161 603 41 0 7532 0
vsize: 30292
[startup+960.035 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7183 0 0 0 95994 20 0 0 25 0 1 0 420261108 31019008 7161 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7573 7161 603 41 0 7532 0
vsize: 30292
[startup+970.036 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7183 0 0 0 96994 20 0 0 25 0 1 0 420261108 31019008 7161 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7573 7161 603 41 0 7532 0
vsize: 30292
[startup+980.036 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7219 0 0 0 97994 20 0 0 25 0 1 0 420261108 31154176 7197 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7606 7197 603 41 0 7565 0
vsize: 30424
[startup+990.037 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7219 0 0 0 98995 20 0 0 25 0 1 0 420261108 31154176 7197 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7606 7197 603 41 0 7565 0
vsize: 30424
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7219 0 0 0 99995 20 0 0 25 0 1 0 420261108 31154176 7197 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7606 7197 603 41 0 7565 0
vsize: 30424
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7219 0 0 0 100995 20 0 0 25 0 1 0 420261108 31154176 7197 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7606 7197 603 41 0 7565 0
vsize: 30424
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 101995 20 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 102995 20 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 103995 20 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 104996 20 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 105996 20 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 106995 20 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223680 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 107995 20 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 108995 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223792 134558157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 109995 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 110995 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 111995 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 112996 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 113996 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223728 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 114996 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 115996 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223576 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 116996 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 117997 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 118997 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 12867
Raw data (stat): 12867 (minisat+) R 12866 10720 10719 0 -1 0 7221 0 0 0 119997 21 0 0 25 0 1 0 420261108 31301632 7199 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7642 7199 603 41 0 7601 0
vsize: 30568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 12867
Raw data (stat): 12867 (minisat+) Z 12866 10720 10719 0 -1 12 7224 0 0 0 119997 22 0 0 25 0 1 0 420261108 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.06
CPU time (s): 1200.2
CPU user time (s): 1199.98
CPU system time (s): 0.225965
CPU usage (%): 100.012
Max. virtual memory (Kb): 30568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####