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/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-gr4x6.opb
MD5SUM	c1c7537cd9b3e10215a81ec1ca3be5cb
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2605440
Optimality of the best value was proved	NO
Number of terms in the objective function	504
Biggest coefficient in the objective function	148373504
Number of bits for the biggest coefficient in the objective function	28
Sum of the numbers in the objective function	3393589600
Number of bits of the sum of numbers in the objective function	32
Biggest number in a constraint	148373504
Number of bits of the biggest number in a constraint	28
Biggest sum of numbers in a constraint	3393589600
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	504
Total number of constraints	34
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	34
Minimum length of a constraint	21
Maximum length of a constraint	120
Trace number 14940

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 02:04:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18992 boxname=wulflinc27 idbench=1461 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1c7537cd9b3e10215a81ec1ca3be5cb  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-gr4x6.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-gr4x6.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-gr4x6.opb
IDLAUNCH: 18992
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
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:        858676 kB
Buffers:         12836 kB
Cached:         134120 kB
SwapCached:        604 kB
Active:          26560 kB
Inactive:       122432 kB
HighTotal:      131008 kB
HighFree:        44968 kB
LowTotal:       903652 kB
LowFree:        813708 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5232 kB
Slab:            21284 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:24:39 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18992 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 44 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): (none)
c ---[  42]---> BDD-cost:  495
c ---[  40]---> BDD-cost:  488
c ---[  38]---> BDD-cost:  463
c ---[  36]---> BDD-cost:  435
c ---[  34]---> BDD-cost:  234
c ---[  32]---> BDD-cost:  224
c ---[  30]---> BDD-cost:  224
c ---[  28]---> BDD-cost:  204
c ---[  26]---> BDD-cost:  177
c ---[  24]---> BDD-cost:  177
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   17
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8809    24521 |    2936       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6085600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63811     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         7 |  185634   437451 |   61878       7       28     4.0 |  0.000 % |
c |       109 |  185634   437451 |   68065     109    10829    99.3 |  0.389 % |
c |       259 |  185634   437451 |   74872     259    12339    47.6 |  0.389 % |
c |       484 |  185634   437451 |   82359     484    17455    36.1 |  0.389 % |
c ==============================================================================
c [1mFound solution: 6054672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       543 |  185656   438008 |   61885     543    19291    35.5 |  0.389 % |
c |       645 |  185656   438008 |   68073     645    20191    31.3 |  0.391 % |
c |       796 |  185644   437981 |   74880     795    20911    26.3 |  0.395 % |
c |      1022 |  185620   437927 |   82368    1019    23599    23.2 |  0.405 % |
c |      1359 |  185620   437927 |   90605    1356    26746    19.7 |  0.405 % |
c |      1865 |  185620   437927 |   99666    1862    30127    16.2 |  0.405 % |
c |      2626 |  185620   437927 |  109633    2623    39710    15.1 |  0.405 % |
c |      3767 |  185620   437927 |  120596    3764    54884    14.6 |  0.405 % |
c ==============================================================================
c [1mFound solution: 5902515[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3832 |  186071   439121 |   62023    3829    56124    14.7 |  0.405 % |
c |      3932 |  186071   439121 |   68225    3929    56740    14.4 |  0.405 % |
c ==============================================================================
c [1mFound solution: 5604192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3990 |  186595   440382 |   62198    3987    57332    14.4 |  0.405 % |
c |      4090 |  186595   440382 |   68417    4087    58977    14.4 |  0.404 % |
c |      4240 |  186595   440382 |   75259    4237    60735    14.3 |  0.404 % |
c |      4465 |  186595   440382 |   82785    4462    72438    16.2 |  0.404 % |
c |      4803 |  186316   439754 |   91064    4784    80147    16.8 |  0.521 % |
c |      5313 |  186316   439754 |  100170    5294    85822    16.2 |  0.521 % |
c |      6074 |  186297   439712 |  110187    6054   117578    19.4 |  0.529 % |
c ==============================================================================
c [1mFound solution: 5516752[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6108 |  186757   440811 |   62252    6088   118170    19.4 |  0.529 % |
c |      6210 |  186757   440811 |   68477    6190   121479    19.6 |  0.528 % |
c |      6362 |  186757   440811 |   75324    6342   127324    20.1 |  0.528 % |
c ==============================================================================
c [1mFound solution: 5488590[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6492 |  186992   441414 |   62330    6469   131533    20.3 |  0.528 % |
c |      6592 |  186992   441414 |   68563    6569   132394    20.2 |  0.572 % |
c |      6742 |  186992   441414 |   75419    6719   133154    19.8 |  0.572 % |
c |      6967 |  186992   441414 |   82961    6944   136111    19.6 |  0.572 % |
c |      7304 |  186992   441414 |   91257    7281   141916    19.5 |  0.572 % |
c |      7810 |  186949   441314 |  100383    7784   175720    22.6 |  0.589 % |
c ==============================================================================
c [1mFound solution: 5338603[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7917 |  186973   441372 |   62324    7891   177945    22.6 |  0.589 % |
c |      8020 |  186973   441372 |   68556    7994   199887    25.0 |  0.590 % |
c |      8170 |  186973   441372 |   75412    8144   202174    24.8 |  0.590 % |
c |      8396 |  186801   440984 |   82953    8363   203607    24.3 |  0.663 % |
c |      8733 |  186801   440984 |   91248    8700   205751    23.6 |  0.663 % |
c |      9239 |  186801   440984 |  100373    9206   211248    22.9 |  0.663 % |
c |      9998 |  186801   440984 |  110410    9965   218736    22.0 |  0.663 % |
c |     11137 |  186801   440984 |  121451   11104   228027    20.5 |  0.663 % |
c |     12845 |  186801   440984 |  133597   12812   368304    28.7 |  0.663 % |
c |     15407 |  186801   440984 |  146956   15374   979575    63.7 |  0.663 % |
c ==============================================================================
c [1mFound solution: 5180312[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17753 |  186644   440653 |   62214   17709  1203958    68.0 |  0.663 % |
c |     17854 |  186515   440368 |   68435   17807  1204705    67.7 |  0.806 % |
c |     18005 |  186200   439656 |   75278   17951  1205614    67.2 |  0.943 % |
c |     18230 |  186200   439656 |   82806   18176  1222002    67.2 |  0.943 % |
c |     18568 |  186200   439656 |   91087   18514  1226151    66.2 |  0.943 % |
c |     19074 |  186200   439656 |  100196   19020  1231480    64.7 |  0.943 % |
c |     19833 |  186200   439656 |  110215   19779  1243008    62.8 |  0.943 % |
c ==============================================================================
c [1mFound solution: 4770772[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20202 |  186253   439796 |   62084   20148  1336483    66.3 |  0.943 % |
c |     20303 |  186253   439796 |   68292   20249  1337769    66.1 |  0.944 % |
c ==============================================================================
c [1mFound solution: 4664369[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20452 |  186286   439884 |   62095   20398  1353419    66.4 |  0.944 % |
c ==============================================================================
c [1mFound solution: 3772369[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20500 |  186337   440021 |   62112   20443  1353834    66.2 |  0.944 % |
c ==============================================================================
c [1mFound solution: 3694603[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20503 |  186361   440080 |   62120   20446  1353863    66.2 |  0.944 % |
c ==============================================================================
c [1mFound solution: 3515403[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20508 |  186391   440157 |   62130   20451  1354519    66.2 |  0.944 % |
c |     20608 |  186391   440157 |   68343   20551  1356510    66.0 |  0.963 % |
c |     20758 |  186391   440157 |   75177   20701  1357754    65.6 |  0.963 % |
c |     20983 |  186391   440157 |   82695   20926  1375834    65.7 |  0.963 % |
c |     21322 |  186391   440157 |   90964   21265  1422802    66.9 |  0.963 % |
c |     21830 |  186391   440157 |  100060   21773  1500138    68.9 |  0.963 % |
c |     22591 |  186387   440149 |  110067   22532  1589109    70.5 |  0.966 % |
c ==============================================================================
c [1mFound solution: 3439232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22783 |  186423   440244 |   62141   22724  1598461    70.3 |  0.966 % |
c |     22883 |  186423   440244 |   68355   22824  1601441    70.2 |  0.967 % |
c |     23034 |  186423   440244 |   75190   22975  1604453    69.8 |  0.967 % |
c |     23259 |  186423   440244 |   82709   23200  1620505    69.8 |  0.967 % |
c ==============================================================================
c [1mFound solution: 3298528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23385 |  186440   440289 |   62146   23326  1638607    70.2 |  0.967 % |
c |     23486 |  186339   440062 |   68360   23424  1639187    70.0 |  1.012 % |
c |     23636 |  186339   440062 |   75196   23574  1640902    69.6 |  1.012 % |
c |     23861 |  186339   440062 |   82716   23799  1653029    69.5 |  1.012 % |
c |     24198 |  186284   439937 |   90987   24134  1683585    69.8 |  1.036 % |
c |     24705 |  186284   439937 |  100086   24641  1723776    70.0 |  1.036 % |
c |     25464 |  186284   439937 |  110095   25400  1841069    72.5 |  1.036 % |
c |     26603 |  186284   439937 |  121104   26539  1867145    70.4 |  1.036 % |
c ==============================================================================
c [1mFound solution: 2806400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26960 |  186328   440045 |   62109   26896  1875438    69.7 |  1.036 % |
c |     27060 |  186328   440045 |   68319   26996  1877658    69.6 |  1.040 % |
c |     27210 |  186328   440045 |   75151   27146  1880790    69.3 |  1.040 % |
c |     27436 |  186328   440045 |   82667   27372  1885651    68.9 |  1.040 % |
c |     27774 |  186328   440045 |   90933   27710  1905488    68.8 |  1.040 % |
c |     28282 |  186328   440045 |  100027   28218  1949296    69.1 |  1.040 % |
c |     29044 |  186328   440045 |  110029   28980  1990282    68.7 |  1.040 % |
c |     30184 |  186283   439944 |  121032   30114  2026792    67.3 |  1.062 % |
c |     31893 |  186283   439944 |  133136   31823  2201134    69.2 |  1.062 % |
c |     34456 |  186283   439944 |  146449   34386  2355851    68.5 |  1.062 % |
c |     38301 |  186283   439944 |  161094   38231  2596501    67.9 |  1.062 % |
c |     44069 |  186283   439944 |  177204   43999  2861641    65.0 |  1.062 % |
c |     52719 |  186283   439944 |  194924   52649  3331230    63.3 |  1.062 % |
c |     65694 |  186283   439944 |  214417   65624  4071595    62.0 |  1.062 % |
c |     85157 |  186283   439944 |  235858   85087  5112278    60.1 |  1.062 % |
c |    114349 |  186283   439944 |  259444  114279  7244007    63.4 |  1.062 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 X1_bit1 X1_bit2 X1_bit3 X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 X2_bit0 X2_bit1 X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 X6_bit0 X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 X14_bit1 -X14_bit2 X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 X16_bit0 -X16_bit1 X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 X17_bit0 -X17_bit1 X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bi#### 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.86 0.97 0.91 2/54 10790
Raw data (stat): 10790 (runsolver) R 10789 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541334818 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99963 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 10790
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 5713 0 0 0 985 13 0 0 25 0 1 0 541334818 26275840 5544 4294967295 134512640 134672761 3221224544 3221221408 134522605 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6415 5544 603 41 0 6374 0
vsize: 25660
[startup+20.0009 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 10790
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 5788 0 0 0 1985 13 0 0 25 0 1 0 541334818 26603520 5619 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6495 5619 603 41 0 6454 0
vsize: 25980
[startup+30.0013 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 10790
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 5932 0 0 0 2985 14 0 0 25 0 1 0 541334818 27238400 5763 4294967295 134512640 134672761 3221224544 3221223808 134562492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6650 5763 603 41 0 6609 0
vsize: 26600
[startup+40.0022 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 10790
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 6143 0 0 0 3984 14 0 0 25 0 1 0 541334818 28049408 5974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6848 5974 603 41 0 6807 0
vsize: 27392
[startup+50.003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 10790
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 6525 0 0 0 4983 16 0 0 25 0 1 0 541334818 29646848 6356 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7238 6356 603 41 0 7197 0
vsize: 28952
[startup+60.0029 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 10790
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 6861 0 0 0 5982 17 0 0 25 0 1 0 541334818 31109120 6692 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7595 6692 603 41 0 7554 0
vsize: 30380
[startup+70.0037 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 10790
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7002 0 0 0 6981 18 0 0 25 0 1 0 541334818 31608832 6833 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7717 6833 603 41 0 7676 0
vsize: 30868
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7172 0 0 0 7980 19 0 0 25 0 1 0 541334818 32264192 7003 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7877 7003 603 41 0 7836 0
vsize: 31508
[startup+90.0044 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7273 0 0 0 8980 20 0 0 25 0 1 0 541334818 32657408 7104 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7973 7104 603 41 0 7932 0
vsize: 31892
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7433 0 0 0 9979 21 0 0 25 0 1 0 541334818 33325056 7264 4294967295 134512640 134672761 3221224544 3221223844 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8136 7264 603 41 0 8095 0
vsize: 32544
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7479 0 0 0 10978 21 0 0 25 0 1 0 541334818 33517568 7310 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8183 7310 603 41 0 8142 0
vsize: 32732
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7629 0 0 0 11978 22 0 0 25 0 1 0 541334818 34127872 7460 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8332 7460 603 41 0 8291 0
vsize: 33328
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7711 0 0 0 12977 23 0 0 25 0 1 0 541334818 34529280 7542 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7542 603 41 0 8389 0
vsize: 33720
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7756 0 0 0 13977 24 0 0 25 0 1 0 541334818 34652160 7587 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8460 7587 603 41 0 8419 0
vsize: 33840
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7823 0 0 0 14976 24 0 0 25 0 1 0 541334818 34897920 7654 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8520 7654 603 41 0 8479 0
vsize: 34080
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7899 0 0 0 15976 25 0 0 25 0 1 0 541334818 35295232 7730 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8617 7730 603 41 0 8576 0
vsize: 34468
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 7986 0 0 0 16975 26 0 0 25 0 1 0 541334818 35565568 7817 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8683 7817 603 41 0 8642 0
vsize: 34732
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8088 0 0 0 17975 26 0 0 25 0 1 0 541334818 35971072 7919 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8782 7919 603 41 0 8741 0
vsize: 35128
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8166 0 0 0 18974 27 0 0 25 0 1 0 541334818 36372480 7997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8880 7997 603 41 0 8839 0
vsize: 35520
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8230 0 0 0 19974 27 0 0 25 0 1 0 541334818 36769792 8061 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8977 8061 603 41 0 8936 0
vsize: 35908
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8304 0 0 0 20973 28 0 0 25 0 1 0 541334818 37036032 8135 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9042 8135 603 41 0 9001 0
vsize: 36168
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8381 0 0 0 21973 28 0 0 25 0 1 0 541334818 37298176 8212 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9106 8212 603 41 0 9065 0
vsize: 36424
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8458 0 0 0 22972 29 0 0 25 0 1 0 541334818 37691392 8289 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9202 8289 603 41 0 9161 0
vsize: 36808
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8533 0 0 0 23972 29 0 0 25 0 1 0 541334818 37953536 8364 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9266 8364 603 41 0 9225 0
vsize: 37064
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8608 0 0 0 24972 30 0 0 25 0 1 0 541334818 38211584 8439 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9329 8439 603 41 0 9288 0
vsize: 37316
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8683 0 0 0 25971 30 0 0 25 0 1 0 541334818 38608896 8514 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9426 8514 603 41 0 9385 0
vsize: 37704
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8751 0 0 0 26971 31 0 0 25 0 1 0 541334818 38879232 8582 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9492 8582 603 41 0 9451 0
vsize: 37968
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8814 0 0 0 27971 31 0 0 25 0 1 0 541334818 39141376 8645 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9556 8645 603 41 0 9515 0
vsize: 38224
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8877 0 0 0 28970 32 0 0 25 0 1 0 541334818 39407616 8708 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9621 8708 603 41 0 9580 0
vsize: 38484
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 8934 0 0 0 29970 32 0 0 25 0 1 0 541334818 39542784 8765 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9654 8765 603 41 0 9613 0
vsize: 38616
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9009 0 0 0 30969 33 0 0 25 0 1 0 541334818 39956480 8840 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9755 8840 603 41 0 9714 0
vsize: 39020
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9073 0 0 0 31969 34 0 0 25 0 1 0 541334818 40222720 8904 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9820 8904 603 41 0 9779 0
vsize: 39280
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9137 0 0 0 32968 34 0 0 25 0 1 0 541334818 40501248 8968 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9888 8968 603 41 0 9847 0
vsize: 39552
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9193 0 0 0 33968 35 0 0 25 0 1 0 541334818 40632320 9024 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9920 9024 603 41 0 9879 0
vsize: 39680
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9242 0 0 0 34968 35 0 0 25 0 1 0 541334818 40898560 9073 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9985 9073 603 41 0 9944 0
vsize: 39940
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9300 0 0 0 35967 36 0 0 25 0 1 0 541334818 41029632 9131 4294967295 134512640 134672761 3221224544 3221223728 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10017 9131 603 41 0 9976 0
vsize: 40068
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9354 0 0 0 36966 37 0 0 25 0 1 0 541334818 41283584 9185 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9185 603 41 0 10038 0
vsize: 40316
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9418 0 0 0 37966 37 0 0 25 0 1 0 541334818 41570304 9249 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10149 9249 603 41 0 10108 0
vsize: 40596
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9500 0 0 0 38966 37 0 0 25 0 1 0 541334818 41955328 9331 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10243 9331 603 41 0 10202 0
vsize: 40972
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9578 0 0 0 39966 38 0 0 25 0 1 0 541334818 42221568 9409 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10308 9409 603 41 0 10267 0
vsize: 41232
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9635 0 0 0 40965 39 0 0 25 0 1 0 541334818 42487808 9466 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10373 9466 603 41 0 10332 0
vsize: 41492
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9693 0 0 0 41965 39 0 0 25 0 1 0 541334818 42745856 9524 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10436 9524 603 41 0 10395 0
vsize: 41744
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9749 0 0 0 42964 40 0 0 25 0 1 0 541334818 43008000 9580 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10500 9580 603 41 0 10459 0
vsize: 42000
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9806 0 0 0 43964 40 0 0 25 0 1 0 541334818 43270144 9637 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10564 9637 603 41 0 10523 0
vsize: 42256
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9865 0 0 0 44963 41 0 0 25 0 1 0 541334818 43401216 9696 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10596 9696 603 41 0 10555 0
vsize: 42384
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9928 0 0 0 45963 41 0 0 25 0 1 0 541334818 43663360 9759 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10660 9759 603 41 0 10619 0
vsize: 42640
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 9980 0 0 0 46963 41 0 0 25 0 1 0 541334818 43921408 9811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10723 9811 603 41 0 10682 0
vsize: 42892
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10020 0 0 0 47962 42 0 0 25 0 1 0 541334818 44052480 9851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10755 9851 603 41 0 10714 0
vsize: 43020
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10084 0 0 0 48962 42 0 0 25 0 1 0 541334818 44326912 9915 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10822 9915 603 41 0 10781 0
vsize: 43288
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10150 0 0 0 49962 42 0 0 25 0 1 0 541334818 44593152 9981 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10887 9981 603 41 0 10846 0
vsize: 43548
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10210 0 0 0 50962 42 0 0 25 0 1 0 541334818 44855296 10041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10951 10041 603 41 0 10910 0
vsize: 43804
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10254 0 0 0 51962 42 0 0 25 0 1 0 541334818 45121536 10085 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11016 10085 603 41 0 10975 0
vsize: 44064
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10308 0 0 0 52962 42 0 0 25 0 1 0 541334818 45256704 10139 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11049 10139 603 41 0 11008 0
vsize: 44196
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10355 0 0 0 53963 42 0 0 25 0 1 0 541334818 45453312 10186 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11097 10186 603 41 0 11056 0
vsize: 44388
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10404 0 0 0 54962 43 0 0 25 0 1 0 541334818 45981696 10235 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11226 10235 603 41 0 11185 0
vsize: 44904
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10476 0 0 0 55962 43 0 0 25 0 1 0 541334818 46247936 10307 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11291 10307 603 41 0 11250 0
vsize: 45164
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10539 0 0 0 56961 44 0 0 25 0 1 0 541334818 46567424 10370 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11369 10370 603 41 0 11328 0
vsize: 45476
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10594 0 0 0 57961 44 0 0 25 0 1 0 541334818 46837760 10425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11435 10425 603 41 0 11394 0
vsize: 45740
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10647 0 0 0 58961 44 0 0 25 0 1 0 541334818 46968832 10478 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11467 10478 603 41 0 11426 0
vsize: 45868
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10712 0 0 0 59961 44 0 0 25 0 1 0 541334818 47230976 10543 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11531 10543 603 41 0 11490 0
vsize: 46124
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10774 0 0 0 60961 44 0 0 25 0 1 0 541334818 47603712 10605 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11622 10605 603 41 0 11581 0
vsize: 46488
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10829 0 0 0 61961 45 0 0 25 0 1 0 541334818 47730688 10660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11653 10660 603 41 0 11612 0
vsize: 46612
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10906 0 0 0 62961 45 0 0 25 0 1 0 541334818 48193536 10737 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11766 10737 603 41 0 11725 0
vsize: 47064
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 10963 0 0 0 63961 45 0 0 25 0 1 0 541334818 48324608 10794 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11798 10794 603 41 0 11757 0
vsize: 47192
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11005 0 0 0 64961 45 0 0 25 0 1 0 541334818 48586752 10836 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11862 10836 603 41 0 11821 0
vsize: 47448
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11060 0 0 0 65961 45 0 0 25 0 1 0 541334818 48721920 10891 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11895 10891 603 41 0 11854 0
vsize: 47580
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11119 0 0 0 66961 45 0 0 25 0 1 0 541334818 48984064 10950 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11959 10950 603 41 0 11918 0
vsize: 47836
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11169 0 0 0 67961 46 0 0 25 0 1 0 541334818 49115136 11000 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11991 11000 603 41 0 11950 0
vsize: 47964
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11224 0 0 0 68961 46 0 0 25 0 1 0 541334818 49467392 11055 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12077 11055 603 41 0 12036 0
vsize: 48308
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11282 0 0 0 69961 46 0 0 25 0 1 0 541334818 49725440 11113 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12140 11113 603 41 0 12099 0
vsize: 48560
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11339 0 0 0 70961 46 0 0 25 0 1 0 541334818 50012160 11170 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12210 11170 603 41 0 12169 0
vsize: 48840
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11380 0 0 0 71961 47 0 0 25 0 1 0 541334818 50151424 11211 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12244 11211 603 41 0 12203 0
vsize: 48976
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11423 0 0 0 72961 47 0 0 25 0 1 0 541334818 50278400 11254 4294967295 134512640 134672761 3221224544 3221223648 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12275 11254 603 41 0 12234 0
vsize: 49100
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11508 0 0 0 73961 47 0 0 25 0 1 0 541334818 50589696 11339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12351 11339 603 41 0 12310 0
vsize: 49404
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11566 0 0 0 74961 47 0 0 25 0 1 0 541334818 50851840 11397 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12415 11397 603 41 0 12374 0
vsize: 49660
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11606 0 0 0 75961 47 0 0 25 0 1 0 541334818 50987008 11437 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12448 11437 603 41 0 12407 0
vsize: 49792
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11650 0 0 0 76961 47 0 0 25 0 1 0 541334818 51122176 11481 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12481 11481 603 41 0 12440 0
vsize: 49924
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11690 0 0 0 77961 47 0 0 25 0 1 0 541334818 51384320 11521 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12545 11521 603 41 0 12504 0
vsize: 50180
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11767 0 0 0 78961 48 0 0 25 0 1 0 541334818 51658752 11598 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12612 11598 603 41 0 12571 0
vsize: 50448
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11824 0 0 0 79961 48 0 0 25 0 1 0 541334818 51920896 11655 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11655 603 41 0 12635 0
vsize: 50704
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11879 0 0 0 80961 48 0 0 25 0 1 0 541334818 52187136 11710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12741 11710 603 41 0 12700 0
vsize: 50964
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11937 0 0 0 81961 48 0 0 25 0 1 0 541334818 52314112 11768 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12772 11768 603 41 0 12731 0
vsize: 51088
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 11989 0 0 0 82961 48 0 0 25 0 1 0 541334818 52576256 11820 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12836 11820 603 41 0 12795 0
vsize: 51344
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12047 0 0 0 83961 49 0 0 25 0 1 0 541334818 52903936 11878 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12916 11878 603 41 0 12875 0
vsize: 51664
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12102 0 0 0 84961 49 0 0 25 0 1 0 541334818 53039104 11933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 11933 603 41 0 12908 0
vsize: 51796
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12149 0 0 0 85961 49 0 0 25 0 1 0 541334818 53305344 11980 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13014 11980 603 41 0 12973 0
vsize: 52056
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12208 0 0 0 86961 49 0 0 25 0 1 0 541334818 53563392 12039 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13077 12039 603 41 0 13036 0
vsize: 52308
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12252 0 0 0 87961 49 0 0 25 0 1 0 541334818 53698560 12083 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13110 12083 603 41 0 13069 0
vsize: 52440
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12332 0 0 0 88961 50 0 0 25 0 1 0 541334818 54124544 12163 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13214 12163 603 41 0 13173 0
vsize: 52856
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12390 0 0 0 89961 50 0 0 25 0 1 0 541334818 54259712 12221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13247 12221 603 41 0 13206 0
vsize: 52988
[startup+910.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12476 0 0 0 90961 50 0 0 25 0 1 0 541334818 54652928 12307 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12307 603 41 0 13302 0
vsize: 53372
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12522 0 0 0 91961 50 0 0 25 0 1 0 541334818 55021568 12353 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13433 12353 603 41 0 13392 0
vsize: 53732
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12574 0 0 0 92961 50 0 0 25 0 1 0 541334818 55156736 12405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13466 12405 603 41 0 13425 0
vsize: 53864
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12627 0 0 0 93961 51 0 0 25 0 1 0 541334818 55291904 12458 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13499 12458 603 41 0 13458 0
vsize: 53996
[startup+950.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12691 0 0 0 94961 51 0 0 25 0 1 0 541334818 55554048 12522 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13563 12522 603 41 0 13522 0
vsize: 54252
[startup+960.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12752 0 0 0 95961 51 0 0 25 0 1 0 541334818 55820288 12583 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13628 12583 603 41 0 13587 0
vsize: 54512
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12807 0 0 0 96961 51 0 0 25 0 1 0 541334818 56082432 12638 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13692 12638 603 41 0 13651 0
vsize: 54768
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12862 0 0 0 97961 52 0 0 25 0 1 0 541334818 56209408 12693 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13723 12693 603 41 0 13682 0
vsize: 54892
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12914 0 0 0 98961 52 0 0 25 0 1 0 541334818 56479744 12745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13789 12745 603 41 0 13748 0
vsize: 55156
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 12961 0 0 0 99961 52 0 0 25 0 1 0 541334818 56610816 12792 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13821 12792 603 41 0 13780 0
vsize: 55284
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13093 0 0 0 100961 52 0 0 25 0 1 0 541334818 57368576 12924 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14006 12924 603 41 0 13965 0
vsize: 56024
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13165 0 0 0 101961 53 0 0 25 0 1 0 541334818 57503744 12996 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14039 12996 603 41 0 13998 0
vsize: 56156
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13224 0 0 0 102961 53 0 0 25 0 1 0 541334818 57774080 13055 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14105 13055 603 41 0 14064 0
vsize: 56420
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13291 0 0 0 103961 53 0 0 25 0 1 0 541334818 58032128 13122 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14168 13122 603 41 0 14127 0
vsize: 56672
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13355 0 0 0 104961 53 0 0 25 0 1 0 541334818 58298368 13186 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14233 13186 603 41 0 14192 0
vsize: 56932
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13414 0 0 0 105961 53 0 0 25 0 1 0 541334818 58556416 13245 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14296 13245 603 41 0 14255 0
vsize: 57184
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13505 0 0 0 106961 53 0 0 25 0 1 0 541334818 58949632 13336 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14392 13336 603 41 0 14351 0
vsize: 57568
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13584 0 0 0 107961 53 0 0 25 0 1 0 541334818 59211776 13415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14456 13415 603 41 0 14415 0
vsize: 57824
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13671 0 0 0 108961 53 0 0 25 0 1 0 541334818 59604992 13502 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14552 13502 603 41 0 14511 0
vsize: 58208
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13755 0 0 0 109961 54 0 0 25 0 1 0 541334818 59990016 13586 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14646 13586 603 41 0 14605 0
vsize: 58584
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13832 0 0 0 110962 54 0 0 25 0 1 0 541334818 60264448 13663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14713 13663 603 41 0 14672 0
vsize: 58852
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13910 0 0 0 111962 54 0 0 25 0 1 0 541334818 60530688 13741 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14778 13741 603 41 0 14737 0
vsize: 59112
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 13966 0 0 0 112962 54 0 0 25 0 1 0 541334818 60792832 13797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14842 13797 603 41 0 14801 0
vsize: 59368
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 14024 0 0 0 113962 54 0 0 25 0 1 0 541334818 61042688 13855 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14903 13855 603 41 0 14862 0
vsize: 59612
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 14078 0 0 0 114962 54 0 0 25 0 1 0 541334818 61304832 13909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14967 13909 603 41 0 14926 0
vsize: 59868
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 14138 0 0 0 115962 54 0 0 25 0 1 0 541334818 61452288 13969 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15003 13969 603 41 0 14962 0
vsize: 60012
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 14210 0 0 0 116962 55 0 0 25 0 1 0 541334818 61714432 14041 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15067 14041 603 41 0 15026 0
vsize: 60268
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 14298 0 0 0 117961 55 0 0 25 0 1 0 541334818 62107648 14129 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15163 14129 603 41 0 15122 0
vsize: 60652
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 14347 0 0 0 118961 55 0 0 25 0 1 0 541334818 62361600 14178 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15225 14178 603 41 0 15184 0
vsize: 60900
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10792
Raw data (stat): 10790 (minisat+) R 10789 18865 18864 0 -1 0 14389 0 0 0 119961 55 0 0 25 0 1 0 541334818 62492672 14220 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15257 14220 603 41 0 15216 0
vsize: 61028
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 10792
Raw data (stat): 10790 (minisat+) Z 10789 18865 18864 0 -1 12 14392 0 0 0 119962 58 0 0 25 0 1 0 541334818 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.07
CPU time (s): 1200.2
CPU user time (s): 1199.62
CPU system time (s): 0.583911
CPU usage (%): 100.011
Max. virtual memory (Kb): 61028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####