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-ran10x10a.opb
MD5SUM	133d42fd76e8bbd92509939943f41498
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	398336
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	539671039
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	539671039
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	913.784
Number of variables	2100
Total number of constraints	120
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	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 17708

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 11:31:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19193 boxname=wulflinc7 idbench=1477 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  133d42fd76e8bbd92509939943f41498  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran10x10a.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran10x10a.opb
IDLAUNCH: 19193
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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.050
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:        685160 kB
Buffers:         13896 kB
Cached:         313724 kB
SwapCached:          4 kB
Active:         157148 kB
Inactive:       173304 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        684908 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            13424 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:51:45 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 19193 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 136]---> Adder-cost: 178   maxlim: 8694   bits: 14/14
c ---[ 134]---> Adder-cost: 178   maxlim: 8310   bits: 14/14
c ---[ 132]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 2042     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 120]---> Sorter-cost: 2002     Base: 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Adder-cost: 194   maxlim: 16374   bits: 15/14
c ---[ 112]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 108]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Adder-cost: 194   maxlim: 16246   bits: 15/14
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   13
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   10
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   13
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   15
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   12
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   12
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   12
c ---[  18]---> BDD-cost:   12
c ---[  17]---> BDD-cost:   12
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   11
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   12
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   15
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78256   193024 |   26085       0        0     nan |  0.000 % |
c |       100 |   78239   192973 |   28693      99      396     4.0 |  7.452 % |
c |       250 |   77991   192412 |   31562     220      889     4.0 |  7.702 % |
c |       475 |   77683   191705 |   34719     430     1908     4.4 |  8.048 % |
c |       812 |   77639   191604 |   38191     765     3590     4.7 |  8.096 % |
c |      1318 |   77639   191604 |   42010    1271     6232     4.9 |  8.096 % |
c |      2077 |   77341   190885 |   46211    2004    10094     5.0 |  8.415 % |
c |      3216 |   76891   189822 |   50832    3109    15662     5.0 |  8.886 % |
c |      4924 |   76891   189822 |   55915    4817    25706     5.3 |  8.886 % |
c ==============================================================================
c [1mFound solution: 1787021[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3925   maxlim: 638322   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5301 |  104280   287702 |   34760    5194    27799     5.4 |  8.886 % |
c |      5401 |  104255   287621 |   38236    5290    28190     5.3 |  7.820 % |
c |      5551 |  104239   287569 |   42059    5437    28861     5.3 |  7.830 % |
c |      5776 |  104232   287546 |   46265    5661    29929     5.3 |  7.833 % |
c |      6113 |  103995   286987 |   50892    5994    31788     5.3 |  8.077 % |
c |      6619 |  103847   286624 |   55981    6495    34774     5.4 |  8.234 % |
c |      7378 |  103847   286624 |   61579    7254    39864     5.5 |  8.234 % |
c ==============================================================================
c [1mFound solution: 1639947[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 785396   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7986 |  103687   286434 |   34562    7855    45201     5.8 |  8.234 % |
c |      8086 |  103687   286434 |   38018    7955    45711     5.7 |  8.455 % |
c |      8236 |  103687   286434 |   41820    8105    46914     5.8 |  8.455 % |
c |      8462 |  103687   286434 |   46002    8331    48139     5.8 |  8.455 % |
c |      8799 |  103687   286434 |   50602    8668    50201     5.8 |  8.455 % |
c |      9305 |  103687   286434 |   55662    9174    53245     5.8 |  8.455 % |
c |     10065 |  103553   286131 |   61228    9914    65909     6.6 |  8.576 % |
c |     11204 |  103520   286028 |   67351   11049    72961     6.6 |  8.599 % |
c |     12912 |  103520   286028 |   74086   12757   118605     9.3 |  8.599 % |
c |     15474 |  103352   285610 |   81495   15296   143125     9.4 |  8.756 % |
c ==============================================================================
c [1mFound solution: 1439526[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 985817   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16409 |  103347   285690 |   34449   16227   151742     9.4 |  8.756 % |
c |     16510 |  103113   285154 |   37893   16307   152338     9.3 |  9.007 % |
c |     16660 |  103042   284993 |   41683   16451   154734     9.4 |  9.074 % |
c |     16885 |  103042   284993 |   45851   16676   156389     9.4 |  9.074 % |
c |     17223 |  102735   284280 |   50436   16991   158183     9.3 |  9.363 % |
c |     17729 |  102735   284280 |   55480   17497   192784    11.0 |  9.363 % |
c |     18488 |  102693   284175 |   61028   18252   199424    10.9 |  9.404 % |
c |     19628 |  102693   284175 |   67131   19392   239276    12.3 |  9.404 % |
c |     21337 |  102517   283735 |   73844   21069   275781    13.1 |  9.568 % |
c |     23899 |  102456   283571 |   81228   23623   359017    15.2 |  9.623 % |
c ==============================================================================
c [1mFound solution: 1386828[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1038515   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27508 |  102358   283435 |   34119   27207   726320    26.7 |  9.623 % |
c |     27608 |  102358   283435 |   37530   27307   726860    26.6 |  9.748 % |
c |     27758 |  102358   283435 |   41283   27457   731543    26.6 |  9.748 % |
c |     27983 |  102237   283154 |   45412   27657   732755    26.5 |  9.873 % |
c |     28320 |  102237   283154 |   49953   27994   740165    26.4 |  9.873 % |
c |     28826 |  102237   283154 |   54948   28500   772931    27.1 |  9.873 % |
c |     29585 |  102209   283092 |   60443   29253   808194    27.6 |  9.898 % |
c |     30725 |  102209   283092 |   66488   30393   866889    28.5 |  9.898 % |
c |     32434 |  102209   283092 |   73137   32102   927142    28.9 |  9.898 % |
c |     34996 |  102209   283092 |   80450   34664  1252280    36.1 |  9.898 % |
c |     38840 |  102209   283092 |   88495   38508  1419350    36.9 |  9.898 % |
c ==============================================================================
c [1mFound solution: 1383134[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1042209   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39478 |  102081   282870 |   34027   39135  1452696    37.1 |  9.898 % |
c |     39579 |  102081   282870 |   37429   18435   739171    40.1 | 10.043 % |
c |     39729 |  101986   282653 |   41172   18564   739799    39.9 | 10.127 % |
c |     39954 |  101986   282653 |   45289   18789   741338    39.5 | 10.127 % |
c |     40291 |  101920   282500 |   49818   19123   743044    38.9 | 10.200 % |
c |     40800 |  101920   282500 |   54800   19632   774357    39.4 | 10.200 % |
c |     41559 |  101664   281901 |   60280   20378   793484    38.9 | 10.463 % |
c |     42698 |  101551   281639 |   66308   21502   875383    40.7 | 10.569 % |
c |     44406 |  101551   281639 |   72939   23210  1142802    49.2 | 10.569 % |
c ==============================================================================
c [1mFound solution: 1272901[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1152442   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44655 |  101580   281856 |   33860   23459  1147685    48.9 | 10.569 % |
c |     44755 |  101548   281783 |   37246   23556  1148298    48.7 | 10.629 % |
c |     44906 |  101472   281607 |   40970   23706  1149373    48.5 | 10.700 % |
c |     45131 |  101472   281607 |   45067   23931  1151026    48.1 | 10.700 % |
c |     45468 |  101472   281607 |   49574   24268  1154330    47.6 | 10.700 % |
c |     45974 |  101472   281607 |   54531   24774  1165653    47.1 | 10.700 % |
c |     46733 |  101472   281607 |   59985   25533  1194292    46.8 | 10.700 % |
c |     47874 |  101472   281607 |   65983   26674  1320673    49.5 | 10.700 % |
c ==============================================================================
c [1mFound solution: 1071477[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1353866   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48273 |  101484   281730 |   33828   27073  1349463    49.8 | 10.700 % |
c |     48374 |  101484   281730 |   37210   27174  1351300    49.7 | 10.721 % |
c |     48524 |  101434   281615 |   40931   27312  1352183    49.5 | 10.766 % |
c |     48749 |  101434   281615 |   45025   27537  1359198    49.4 | 10.766 % |
c ==============================================================================
c [1mFound solution: 788737[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1636606   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48964 |  101444   281806 |   33814   27750  1367751    49.3 | 10.766 % |
c |     49064 |  101285   281440 |   37195   27843  1368576    49.2 | 10.989 % |
c |     49214 |  101285   281440 |   40914   27993  1370353    49.0 | 10.989 % |
c |     49439 |  101285   281440 |   45006   28218  1384131    49.1 | 10.989 % |
c |     49776 |  101278   281420 |   49507   28456  1385192    48.7 | 10.992 % |
c ==============================================================================
c [1mFound solution: 659299[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1766044   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49924 |  101297   281590 |   33765   28604  1400768    49.0 | 10.992 % |
c |     50024 |  101264   281517 |   37141   28701  1401288    48.8 | 11.052 % |
c |     50174 |  101264   281517 |   40855   28851  1402110    48.6 | 11.052 % |
c |     50399 |  101226   281428 |   44941   29074  1404538    48.3 | 11.094 % |
c |     50738 |  101226   281428 |   49435   29413  1408586    47.9 | 11.094 % |
c |     51245 |  101226   281428 |   54378   29920  1461313    48.8 | 11.094 % |
c |     52005 |  101226   281428 |   59816   30680  1505950    49.1 | 11.094 % |
c |     53144 |  101226   281428 |   65798   31819  1541320    48.4 | 11.094 % |
c |     54852 |  101226   281428 |   72378   33527  1648247    49.2 | 11.094 % |
c |     57414 |  101226   281428 |   79616   36089  1721769    47.7 | 11.094 % |
c |     61258 |  101221   281417 |   87577   39932  1850180    46.3 | 11.100 % |
c |     67024 |  101151   281251 |   96335   45656  2366915    51.8 | 11.164 % |
c |     75674 |  101018   280948 |  105969   54297  2728916    50.3 | 11.283 % |
c |     88651 |  101018   280948 |  116565   67274  6239872    92.8 | 11.283 % |
c |    108112 |  100838   280531 |  128222   86703 11448514   132.0 | 11.459 % |
c |    137307 |  100616   280022 |  141044  115877 14414127   124.4 | 11.673 % |
c |    181096 |  100587   279956 |  155149   25399  4141424   163.1 | 11.702 % |
c |    246781 |  100354   279418 |  170664   91058 12693154   139.4 | 11.951 % |
c |    345308 |  100064   278749 |  187730   26575  1057745    39.8 | 12.236 % |
c ==============================================================================
c [1mFound solution: 467356[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1957987   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    362478 |  100031   278747 |   33343   43741  2964852    67.8 | 12.236 % |
c |    362578 |  100019   278719 |   36677   18288  1527137    83.5 | 12.324 % |
c |    362730 |  100019   278719 |   40345   18440  1527940    82.9 | 12.324 % |
c |    362956 |  100019   278719 |   44379   18666  1529106    81.9 | 12.324 % |
c |    363293 |   99853   278334 |   48817   18994  1530964    80.6 | 12.494 % |
c |    363799 |   99853   278334 |   53699   19500  1548356    79.4 | 12.494 % |
c |    364559 |   99853   278334 |   59069   20260  1586950    78.3 | 12.494 % |
c |    365698 |   99803   278214 |   64976   21397  1596629    74.6 | 12.545 % |
c |    367406 |   99803   278214 |   71473   23105  1786753    77.3 | 12.545 % |
c |    369969 |   99775   278150 |   78621   25667  1849032    72.0 | 12.574 % |
c |    373814 |   99770   278139 |   86483   29511  1960065    66.4 | 12.580 % |
c |    379581 |   99694   277967 |   95131   35273  2402215    68.1 | 12.653 % |
c |    388232 |   99694   277967 |  104644   43924  2804050    63.8 | 12.653 % |
c |    401206 |   99653   277873 |  115109   56889  4266349    75.0 | 12.692 % |
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_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 X24_bit_2 X24_bit_1 X24_bit0 X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 X27_bit_2 -X27_bit_1 X27_bit0 X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 X32_bit_7 X32_bit_6 X32_bit_5 X32_bit_4 X32_bit_3 X32_bit_2 X32_bit_1 X32_bit0 X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 X33_bit_2 -X33_bit_1 -X33_bit0 X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 X37_bit_2 X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 X42_bit_2 X42_bit_1 X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 X52_bit_2 X52_bit_1 X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 X53_bit_5 -X53_bit_4 -X53_bit_3 X53_bit_2 -X53_bit_1 -X53_bit0 X53_bit1 X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 -X56_bit_5 X56_bit_4 X56_bit_3 X56_bit_2 X56_bit_1 -X56_bit0 X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 X62_bit_6 X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 X62_bit_1 X62_bit0 X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 -X63_bit_6 X63_bit_5 X63_bit_4 -X63_bit_3 X63_bit_2 -X63_bit_1 -X63_bit0 X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 X64_bit_6 X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 X64_bit0 X64_bit1 X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 X66_bit_6 X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 X77_bit_2 X77_bit_1 -X77_bit0 X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 X78_bit_6 -X78_bit_5 -X78_bit_4 X78_bit_3 -X78_bit_2 X78_bit_1 X78_bit0 X78_bit1 X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 X79_bit_6 X79_bit_5 X79_bit_4 -X79_bit_3 -X79_bit_2 X79_bit_1 X79_bit0 X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 X83_bit_6 X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 X84_bit_6 -X84_bit_5 X84_bit_4 X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 X88_bit_2 X88_bit_1 X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 X98_bit_6 X98_bit_5 X98_bit_4 -X98_bit_3 -X98_bit_2 X98_bit_1 X98_bit0 -X98_bit1 X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98#### 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.92 0.95 0.90 2/54 5595
Raw data (stat): 5595 (runsolver) R 5594 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486524262 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 4719 0 0 0 987 11 0 0 25 0 1 0 486524262 21299200 4385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5200 4385 603 41 0 5159 0
vsize: 20800
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 4910 0 0 0 1984 12 0 0 25 0 1 0 486524262 21966848 4555 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5363 4555 603 41 0 5322 0
vsize: 21452
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 5254 0 0 0 2983 14 0 0 25 0 1 0 486524262 23314432 4899 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5692 4899 603 41 0 5651 0
vsize: 22768
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 5680 0 0 0 3982 15 0 0 25 0 1 0 486524262 25014272 5304 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6107 5304 603 41 0 6066 0
vsize: 24428
[startup+50.0007 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 6084 0 0 0 4981 16 0 0 25 0 1 0 486524262 26759168 5708 4294967295 134512640 134672761 3221224624 3221223728 134554735 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6533 5708 603 41 0 6492 0
vsize: 26132
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 6470 0 0 0 5980 17 0 0 25 0 1 0 486524262 28274688 6073 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6073 603 41 0 6862 0
vsize: 27612
[startup+70.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 6470 0 0 0 6979 18 0 0 25 0 1 0 486524262 28274688 6073 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6073 603 41 0 6862 0
vsize: 27612
[startup+80.0016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 6472 0 0 0 7979 18 0 0 25 0 1 0 486524262 28274688 6075 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6903 6075 603 41 0 6862 0
vsize: 27612
[startup+90.0016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 6514 0 0 0 8979 18 0 0 25 0 1 0 486524262 28409856 6117 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6936 6117 603 41 0 6895 0
vsize: 27744
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 6734 0 0 0 9978 19 0 0 25 0 1 0 486524262 29351936 6337 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7166 6337 603 41 0 7125 0
vsize: 28664
[startup+110.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 7003 0 0 0 10978 20 0 0 25 0 1 0 486524262 30429184 6606 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7429 6606 603 41 0 7388 0
vsize: 29716
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 7473 0 0 0 11977 21 0 0 25 0 1 0 486524262 32305152 7076 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7887 7076 603 41 0 7846 0
vsize: 31548
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 7956 0 0 0 12975 23 0 0 25 0 1 0 486524262 34320384 7559 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8379 7559 603 41 0 8338 0
vsize: 33516
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 8830 0 0 0 13973 25 0 0 25 0 1 0 486524262 37822464 8433 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9234 8433 603 41 0 9193 0
vsize: 36936
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 9773 0 0 0 14971 27 0 0 25 0 1 0 486524262 41701376 9376 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10181 9376 603 41 0 10140 0
vsize: 40724
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 10571 0 0 0 15969 30 0 0 25 0 1 0 486524262 44908544 10174 4294967295 134512640 134672761 3221224624 3221223748 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10964 10174 603 41 0 10923 0
vsize: 43856
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 11350 0 0 0 16966 33 0 0 25 0 1 0 486524262 48381952 10953 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11812 10953 603 41 0 11771 0
vsize: 47248
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 11829 0 0 0 17965 34 0 0 25 0 1 0 486524262 50397184 11432 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12304 11432 603 41 0 12263 0
vsize: 49216
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 12496 0 0 0 18963 36 0 0 25 0 1 0 486524262 53080064 12099 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12959 12099 603 41 0 12918 0
vsize: 51836
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 13523 0 0 0 19961 38 0 0 25 0 1 0 486524262 57241600 13126 4294967295 134512640 134672761 3221224624 3221223728 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13975 13126 603 41 0 13934 0
vsize: 55900
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 14391 0 0 0 20959 41 0 0 25 0 1 0 486524262 60850176 13994 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14856 13994 603 41 0 14815 0
vsize: 59424
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 15289 0 0 0 21958 42 0 0 25 0 1 0 486524262 64471040 14892 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15740 14892 603 41 0 15699 0
vsize: 62960
[startup+230.013 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 16156 0 0 0 22956 44 0 0 25 0 1 0 486524262 68100096 15759 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16626 15759 603 41 0 16585 0
vsize: 66504
[startup+240.014 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 16880 0 0 0 23954 47 0 0 25 0 1 0 486524262 71049216 16483 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17346 16483 603 41 0 17305 0
vsize: 69384
[startup+250.014 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 17240 0 0 0 24953 47 0 0 25 0 1 0 486524262 72523776 16843 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17706 16843 603 41 0 17665 0
vsize: 70824
[startup+260.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 17643 0 0 0 25952 49 0 0 25 0 1 0 486524262 74141696 17246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18101 17246 603 41 0 18060 0
vsize: 72404
[startup+270.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 17971 0 0 0 26951 50 0 0 25 0 1 0 486524262 75481088 17574 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18428 17574 603 41 0 18387 0
vsize: 73712
[startup+280.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 18475 0 0 0 27950 51 0 0 25 0 1 0 486524262 77500416 18078 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18921 18078 603 41 0 18880 0
vsize: 75684
[startup+290.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 19160 0 0 0 28949 53 0 0 25 0 1 0 486524262 80302080 18763 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19605 18763 603 41 0 19564 0
vsize: 78420
[startup+300.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 19575 0 0 0 29948 54 0 0 25 0 1 0 486524262 82026496 19178 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20026 19178 603 41 0 19985 0
vsize: 80104
[startup+310.014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 19793 0 0 0 30947 54 0 0 25 0 1 0 486524262 82833408 19396 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20223 19396 603 41 0 20182 0
vsize: 80892
[startup+320.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 20025 0 0 0 31947 55 0 0 25 0 1 0 486524262 83787776 19628 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20456 19628 603 41 0 20415 0
vsize: 81824
[startup+330.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 20264 0 0 0 32947 55 0 0 25 0 1 0 486524262 84750336 19867 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20691 19867 603 41 0 20650 0
vsize: 82764
[startup+340.017 s]
Raw data (loadavg): 1.25 1.04 0.93 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 20561 0 0 0 33947 56 0 0 25 0 1 0 486524262 85966848 20164 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20988 20164 603 41 0 20947 0
vsize: 83952
[startup+350.017 s]
Raw data (loadavg): 1.28 1.05 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 20883 0 0 0 34946 56 0 0 25 0 1 0 486524262 87318528 20486 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21318 20486 603 41 0 21277 0
vsize: 85272
[startup+360.018 s]
Raw data (loadavg): 1.24 1.05 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 21116 0 0 0 35946 57 0 0 25 0 1 0 486524262 88256512 20719 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21547 20719 603 41 0 21506 0
vsize: 86188
[startup+370.017 s]
Raw data (loadavg): 1.20 1.05 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 21508 0 0 0 36945 58 0 0 25 0 1 0 486524262 90386432 21111 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22067 21111 603 41 0 22026 0
vsize: 88268
[startup+380.018 s]
Raw data (loadavg): 1.17 1.05 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 22106 0 0 0 37944 59 0 0 25 0 1 0 486524262 92819456 21709 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22661 21709 603 41 0 22620 0
vsize: 90644
[startup+390.018 s]
Raw data (loadavg): 1.14 1.04 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 22597 0 0 0 38943 61 0 0 25 0 1 0 486524262 94822400 22200 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23150 22200 603 41 0 23109 0
vsize: 92600
[startup+400.017 s]
Raw data (loadavg): 1.12 1.04 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 23004 0 0 0 39942 62 0 0 25 0 1 0 486524262 96444416 22607 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23546 22607 603 41 0 23505 0
vsize: 94184
[startup+410.018 s]
Raw data (loadavg): 1.10 1.04 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 23463 0 0 0 40941 63 0 0 25 0 1 0 486524262 98324480 23066 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24005 23066 603 41 0 23964 0
vsize: 96020
[startup+420.019 s]
Raw data (loadavg): 1.09 1.04 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 23880 0 0 0 41940 64 0 0 25 0 1 0 486524262 100077568 23483 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24433 23483 603 41 0 24392 0
vsize: 97732
[startup+430.019 s]
Raw data (loadavg): 1.07 1.04 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 24455 0 0 0 42939 66 0 0 25 0 1 0 486524262 102350848 24058 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24988 24058 603 41 0 24947 0
vsize: 99952
[startup+440.018 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 24909 0 0 0 43938 67 0 0 25 0 1 0 486524262 104206336 24512 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25441 24512 603 41 0 25400 0
vsize: 101764
[startup+450.018 s]
Raw data (loadavg): 1.05 1.03 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 25342 0 0 0 44937 68 0 0 25 0 1 0 486524262 105943040 24945 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25865 24945 603 41 0 25824 0
vsize: 103460
[startup+460.019 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 25793 0 0 0 45936 69 0 0 25 0 1 0 486524262 107786240 25396 4294967295 134512640 134672761 3221224624 3221223728 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26315 25396 603 41 0 26274 0
vsize: 105260
[startup+470.019 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 26227 0 0 0 46935 70 0 0 25 0 1 0 486524262 109649920 25830 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26770 25830 603 41 0 26729 0
vsize: 107080
[startup+480.019 s]
Raw data (loadavg): 1.03 1.03 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 26720 0 0 0 47934 72 0 0 25 0 1 0 486524262 111648768 26323 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27258 26323 603 41 0 27217 0
vsize: 109032
[startup+490.019 s]
Raw data (loadavg): 1.02 1.03 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27151 0 0 0 48932 74 0 0 25 0 1 0 486524262 113389568 26754 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27683 26754 603 41 0 27642 0
vsize: 110732
[startup+500.018 s]
Raw data (loadavg): 1.02 1.03 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 49932 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+510.018 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 50932 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+520.019 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 51931 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+530.019 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 52931 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+540.019 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 53931 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+550.027 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 54932 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+560.027 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 55933 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+570.027 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 56933 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+580.027 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 57933 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+590.029 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 58933 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+600.028 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 59933 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+610.028 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 60934 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+620.028 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 61934 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+630.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 62934 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+640.028 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 63934 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+650.028 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 64934 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+660.035 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 65935 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+670.035 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 66935 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223808 134558938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+680.036 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 67936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+690.037 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 68936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+700.036 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 69936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+710.037 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 70936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+720.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 71936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+730.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 72936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+740.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 73936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+750.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 74936 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+760.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 75937 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+770.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 76937 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+780.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 77937 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+790.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 78937 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+800.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 79937 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+810.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 80937 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+820.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27176 0 0 0 81938 74 0 0 25 0 1 0 486524262 113524736 26779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26779 603 41 0 27675 0
vsize: 110864
[startup+830.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27177 0 0 0 82938 74 0 0 25 0 1 0 486524262 113524736 26780 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26780 603 41 0 27675 0
vsize: 110864
[startup+840.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27177 0 0 0 83938 74 0 0 25 0 1 0 486524262 113524736 26780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26780 603 41 0 27675 0
vsize: 110864
[startup+850.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27177 0 0 0 84938 74 0 0 25 0 1 0 486524262 113524736 26780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26780 603 41 0 27675 0
vsize: 110864
[startup+860.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27177 0 0 0 85938 74 0 0 25 0 1 0 486524262 113524736 26780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26780 603 41 0 27675 0
vsize: 110864
[startup+870.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27177 0 0 0 86939 74 0 0 25 0 1 0 486524262 113524736 26780 4294967295 134512640 134672761 3221224624 3221223760 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26780 603 41 0 27675 0
vsize: 110864
[startup+880.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27177 0 0 0 87939 74 0 0 25 0 1 0 486524262 113524736 26780 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26780 603 41 0 27675 0
vsize: 110864
[startup+890.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27177 0 0 0 88939 74 0 0 25 0 1 0 486524262 113524736 26780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27716 26780 603 41 0 27675 0
vsize: 110864
[startup+900.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27704 0 0 0 89938 75 0 0 25 0 1 0 486524262 115683328 27307 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28243 27307 603 41 0 28202 0
vsize: 112972
[startup+910.041 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 27918 0 0 0 90938 76 0 0 25 0 1 0 486524262 116490240 27521 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28440 27521 603 41 0 28399 0
vsize: 113760
[startup+920.041 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 28155 0 0 0 91938 76 0 0 25 0 1 0 486524262 117432320 27758 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28670 27758 603 41 0 28629 0
vsize: 114680
[startup+930.041 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 28363 0 0 0 92937 77 0 0 25 0 1 0 486524262 118370304 27966 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28899 27966 603 41 0 28858 0
vsize: 115596
[startup+940.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 28630 0 0 0 93937 77 0 0 25 0 1 0 486524262 119451648 28233 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29163 28233 603 41 0 29122 0
vsize: 116652
[startup+950.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 28859 0 0 0 94936 78 0 0 25 0 1 0 486524262 120393728 28462 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29393 28462 603 41 0 29352 0
vsize: 117572
[startup+960.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 29200 0 0 0 95936 79 0 0 25 0 1 0 486524262 121729024 28803 4294967295 134512640 134672761 3221224624 3221223808 134559254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29719 28803 603 41 0 29678 0
vsize: 118876
[startup+970.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 29406 0 0 0 96936 79 0 0 25 0 1 0 486524262 122535936 29009 4294967295 134512640 134672761 3221224624 3221223808 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29916 29009 603 41 0 29875 0
vsize: 119664
[startup+980.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 29622 0 0 0 97935 80 0 0 25 0 1 0 486524262 123473920 29225 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30145 29225 603 41 0 30104 0
vsize: 120580
[startup+990.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30040 0 0 0 98935 81 0 0 25 0 1 0 486524262 125091840 29643 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30540 29643 603 41 0 30499 0
vsize: 122160
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30210 0 0 0 99934 82 0 0 25 0 1 0 486524262 125767680 29813 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30705 29813 603 41 0 30664 0
vsize: 122820
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30424 0 0 0 100934 82 0 0 25 0 1 0 486524262 126722048 30027 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30938 30027 603 41 0 30897 0
vsize: 123752
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30671 0 0 0 101933 83 0 0 25 0 1 0 486524262 127668224 30274 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31169 30274 603 41 0 31128 0
vsize: 124676
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30870 0 0 0 102933 84 0 0 25 0 1 0 486524262 128479232 30473 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30473 603 41 0 31326 0
vsize: 125468
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30870 0 0 0 103933 84 0 0 25 0 1 0 486524262 128479232 30473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31367 30473 603 41 0 31326 0
vsize: 125468
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30870 0 0 0 104932 84 0 0 25 0 1 0 486524262 128479232 30473 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30473 603 41 0 31326 0
vsize: 125468
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30870 0 0 0 105932 84 0 0 25 0 1 0 486524262 128479232 30473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30473 603 41 0 31326 0
vsize: 125468
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30870 0 0 0 106932 84 0 0 25 0 1 0 486524262 128479232 30473 4294967295 134512640 134672761 3221224624 3221221168 134522898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30473 603 41 0 31326 0
vsize: 125468
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30873 0 0 0 107932 84 0 0 25 0 1 0 486524262 128479232 30476 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30476 603 41 0 31326 0
vsize: 125468
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30873 0 0 0 108933 84 0 0 25 0 1 0 486524262 128479232 30476 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30476 603 41 0 31326 0
vsize: 125468
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30873 0 0 0 109933 84 0 0 25 0 1 0 486524262 128479232 30476 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30476 603 41 0 31326 0
vsize: 125468
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30873 0 0 0 110933 84 0 0 25 0 1 0 486524262 128479232 30476 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30476 603 41 0 31326 0
vsize: 125468
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30873 0 0 0 111933 84 0 0 25 0 1 0 486524262 128479232 30476 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30476 603 41 0 31326 0
vsize: 125468
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30873 0 0 0 112933 84 0 0 25 0 1 0 486524262 128479232 30476 4294967295 134512640 134672761 3221224624 3221223760 134560686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30476 603 41 0 31326 0
vsize: 125468
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30875 0 0 0 113934 84 0 0 25 0 1 0 486524262 128479232 30478 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30478 603 41 0 31326 0
vsize: 125468
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30875 0 0 0 114934 84 0 0 25 0 1 0 486524262 128479232 30478 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30478 603 41 0 31326 0
vsize: 125468
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30875 0 0 0 115934 84 0 0 25 0 1 0 486524262 128479232 30478 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30478 603 41 0 31326 0
vsize: 125468
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30875 0 0 0 116934 84 0 0 25 0 1 0 486524262 128479232 30478 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30478 603 41 0 31326 0
vsize: 125468
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30875 0 0 0 117934 84 0 0 25 0 1 0 486524262 128479232 30478 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30478 603 41 0 31326 0
vsize: 125468
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30875 0 0 0 118934 84 0 0 25 0 1 0 486524262 128479232 30478 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30478 603 41 0 31326 0
vsize: 125468
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 5595
Raw data (stat): 5595 (minisat+) R 5594 22932 22931 0 -1 0 30875 0 0 0 119935 84 0 0 25 0 1 0 486524262 128479232 30478 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30478 603 41 0 31326 0
vsize: 125468
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 5595
Raw data (stat): 5595 (minisat+) Z 5594 22932 22931 0 -1 12 30878 0 0 0 119935 90 0 0 25 0 1 0 486524262 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.26
CPU user time (s): 1199.35
CPU system time (s): 0.903862
CPU usage (%): 100.012
Max. virtual memory (Kb): 125468
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####