PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:98.opb
MD5SUM	a89f4ed95903fddf213992506514bcf0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16
Optimality of the best value was proved	NO
Number of terms in the objective function	906
Biggest coefficient in the objective function	553
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	2526
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	553
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	2526
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04184
Number of variables	906
Total number of constraints	1944
Number of constraints which are clauses	852
Number of constraints which are cardinality constraints (but not clauses)	1092
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 5114

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-13 21:58:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3335 boxname=wulflinc24 idbench=371 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  a89f4ed95903fddf213992506514bcf0  /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:98.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc24/normalized-10:20:4.5:0.95:98.opb
IDLAUNCH: 3335
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        853116 kB
Buffers:         33824 kB
Cached:         105488 kB
SwapCached:       3828 kB
Active:          48720 kB
Inactive:        97248 kB
HighTotal:      131008 kB
HighFree:        23212 kB
LowTotal:       903652 kB
LowFree:        829904 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            29924 kB
Committed_AS:    63508 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:18:30 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3335 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1038 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 187]---> BDD-cost:    5
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   23
c ---[ 180]---> BDD-cost:   20
c ---[ 179]---> BDD-cost:   29
c ---[ 178]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   38
c ---[ 176]---> BDD-cost:   32
c ---[ 175]---> BDD-cost:   32
c ---[ 174]---> BDD-cost:   23
c ---[ 173]---> BDD-cost:   26
c ---[ 172]---> BDD-cost:   20
c ---[ 171]---> BDD-cost:   20
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   17
c ---[ 163]---> BDD-cost:   18
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   35
c ---[ 160]---> BDD-cost:   35
c ---[ 159]---> BDD-cost:   41
c ---[ 158]---> BDD-cost:   35
c ---[ 157]---> BDD-cost:   38
c ---[ 156]---> BDD-cost:   38
c ---[ 155]---> BDD-cost:   41
c ---[ 154]---> BDD-cost:   35
c ---[ 153]---> BDD-cost:   38
c ---[ 152]---> BDD-cost:   23
c ---[ 151]---> BDD-cost:   20
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   14
c ---[ 144]---> BDD-cost:   17
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   29
c ---[ 141]---> BDD-cost:   41
c ---[ 140]---> BDD-cost:   44
c ---[ 139]---> BDD-cost:   44
c ---[ 138]---> BDD-cost:   38
c ---[ 137]---> BDD-cost:   39
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   44
c ---[ 134]---> BDD-cost:   44
c ---[ 133]---> BDD-cost:   41
c ---[ 132]---> BDD-cost:   29
c ---[ 131]---> BDD-cost:   29
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   26
c ---[ 128]---> BDD-cost:   14
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   14
c ---[ 124]---> BDD-cost:   17
c ---[ 123]---> BDD-cost:   21
c ---[ 122]---> BDD-cost:   29
c ---[ 121]---> BDD-cost:   35
c ---[ 120]---> BDD-cost:   44
c ---[ 119]---> BDD-cost:   47
c ---[ 118]---> BDD-cost:   44
c ---[ 117]---> BDD-cost:   44
c ---[ 116]---> BDD-cost:   44
c ---[ 115]---> BDD-cost:   41
c ---[ 114]---> BDD-cost:   38
c ---[ 113]---> BDD-cost:   35
c ---[ 112]---> BDD-cost:   32
c ---[ 111]---> BDD-cost:   29
c ---[ 110]---> BDD-cost:   26
c ---[ 109]---> BDD-cost:   20
c ---[ 108]---> BDD-cost:    6
c ---[ 107]---> BDD-cost:    5
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   20
c ---[ 104]---> BDD-cost:   23
c ---[ 103]---> BDD-cost:   26
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:   38
c ---[ 100]---> BDD-cost:   35
c ---[  99]---> BDD-cost:   41
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   41
c ---[  96]---> BDD-cost:   38
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:   38
c ---[  93]---> BDD-cost:   29
c ---[  92]---> BDD-cost:   20
c ---[  91]---> BDD-cost:   26
c ---[  90]---> BDD-cost:   20
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:    5
c ---[  87]---> BDD-cost:    5
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   20
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   41
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   35
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   35
c ---[  77]---> BDD-cost:   44
c ---[  76]---> BDD-cost:   35
c ---[  75]---> BDD-cost:   38
c ---[  74]---> BDD-cost:   35
c ---[  73]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   23
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   17
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   23
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   26
c ---[  61]---> BDD-cost:   38
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   32
c ---[  58]---> BDD-cost:   35
c ---[  57]---> BDD-cost:   38
c ---[  56]---> BDD-cost:   32
c ---[  55]---> BDD-cost:   35
c ---[  54]---> BDD-cost:   29
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   29
c ---[  51]---> BDD-cost:   23
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   11
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   20
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:   35
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:   26
c ---[  36]---> BDD-cost:   23
c ---[  35]---> BDD-cost:   23
c ---[  34]---> BDD-cost:   23
c ---[  33]---> BDD-cost:   26
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   20
c ---[  24]---> BDD-cost:   26
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   20
c ---[  20]---> BDD-cost:   20
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   20
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:   14
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   17
c ---[   9]---> BDD-cost:   14
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:   14
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   11181    31975 |    3727       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 959[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2188   maxlim: 461   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26442    86478 |    8814       0        0     nan |  0.000 % |
c |       100 |   26442    86478 |    9695     100      380     3.8 |  2.547 % |
c |       250 |   26433    86447 |   10664     248     1059     4.3 |  2.560 % |
c |       476 |   26433    86447 |   11731     474     2412     5.1 |  2.560 % |
c ==============================================================================
c [1mFound solution: 206[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 1214   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       806 |   26471    86617 |    8823     804     4288     5.3 |  2.560 % |
c ==============================================================================
c [1mFound solution: 143[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1277   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       814 |   26480    86667 |    8826     812     4330     5.3 |  2.560 % |
c |       914 |   26480    86667 |    9708     912     8172     9.0 |  2.738 % |
c |      1064 |   26480    86667 |   10679    1062     8878     8.4 |  2.738 % |
c |      1289 |   26480    86667 |   11747    1287    13915    10.8 |  2.738 % |
c |      1626 |   26480    86667 |   12922    1624    15594     9.6 |  2.738 % |
c |      2132 |   26480    86667 |   14214    2130    18615     8.7 |  2.738 % |
c |      2892 |   26480    86667 |   15635    2890    40463    14.0 |  2.738 % |
c |      4031 |   26480    86667 |   17199    4029    61525    15.3 |  2.738 % |
c |      5740 |   26480    86667 |   18919    5738   145592    25.4 |  2.738 % |
c |      8302 |   26480    86667 |   20811    8300   400387    48.2 |  2.738 % |
c |     12147 |   26480    86667 |   22892   12145   750271    61.8 |  2.738 % |
c ==============================================================================
c [1mFound solution: 130[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1290   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14029 |   26485    86701 |    8828   14027   824966    58.8 |  2.738 % |
c |     14129 |   26485    86701 |    9710    7114   431246    60.6 |  2.789 % |
c |     14279 |   26485    86701 |   10681    7264   431919    59.5 |  2.789 % |
c |     14505 |   26485    86701 |   11750    7490   433807    57.9 |  2.789 % |
c |     14842 |   26485    86701 |   12925    7827   440942    56.3 |  2.789 % |
c |     15349 |   26485    86701 |   14217    8334   463419    55.6 |  2.789 % |
c |     16108 |   26485    86701 |   15639    9093   482022    53.0 |  2.789 % |
c |     17247 |   26485    86701 |   17203   10232   538561    52.6 |  2.789 % |
c |     18955 |   26485    86701 |   18923   11940   602513    50.5 |  2.789 % |
c |     21519 |   26485    86701 |   20815   14504   833364    57.5 |  2.789 % |
c ==============================================================================
c [1mFound solution: 127[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1293   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23171 |   26489    86723 |    8829   16156   882076    54.6 |  2.789 % |
c |     23272 |   26489    86723 |    9711    8179   357304    43.7 |  2.814 % |
c |     23422 |   26489    86723 |   10683    8329   358840    43.1 |  2.814 % |
c |     23647 |   26489    86723 |   11751    8554   363731    42.5 |  2.814 % |
c |     23984 |   26489    86723 |   12926    8891   369197    41.5 |  2.814 % |
c |     24490 |   26489    86723 |   14219    9397   396462    42.2 |  2.814 % |
c |     25250 |   26489    86723 |   15641   10157   425636    41.9 |  2.814 % |
c |     26389 |   26489    86723 |   17205   11296   470056    41.6 |  2.814 % |
c |     28097 |   26489    86723 |   18925   13004   538210    41.4 |  2.814 % |
c |     30662 |   26489    86723 |   20818   15569   771366    49.5 |  2.814 % |
c |     34507 |   26489    86723 |   22900   19414  1108591    57.1 |  2.814 % |
c |     40273 |   26489    86723 |   25190   25180  1530602    60.8 |  2.814 % |
c ==============================================================================
c [1mFound solution: 117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1303   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47450 |   26491    86738 |    8830   18237  1218106    66.8 |  2.814 % |
c |     47550 |   26491    86738 |    9713    4660   289106    62.0 |  2.839 % |
c |     47700 |   26491    86738 |   10684    4810   290323    60.4 |  2.839 % |
c |     47925 |   26491    86738 |   11752    5035   300392    59.7 |  2.839 % |
c |     48262 |   26491    86738 |   12928    5372   302069    56.2 |  2.839 % |
c |     48768 |   26491    86738 |   14220    5878   320891    54.6 |  2.839 % |
c |     49527 |   26491    86738 |   15642    6637   330420    49.8 |  2.839 % |
c |     50666 |   26491    86738 |   17207    7776   374858    48.2 |  2.839 % |
c |     52374 |   26491    86738 |   18927    9484   530806    56.0 |  2.839 % |
c |     54937 |   26491    86738 |   20820   12047   686209    57.0 |  2.839 % |
c |     58782 |   26491    86738 |   22902   15892   975705    61.4 |  2.839 % |
c ==============================================================================
c [1mFound solution: 109[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1311   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     60887 |   26492    86744 |    8830   17997  1087821    60.4 |  2.839 % |
c |     60987 |   26492    86744 |    9713    9099   440274    48.4 |  2.852 % |
c |     61137 |   26492    86744 |   10684    9249   442243    47.8 |  2.852 % |
c |     61363 |   26492    86744 |   11752    9475   447923    47.3 |  2.852 % |
c |     61701 |   26492    86744 |   12928    9813   460334    46.9 |  2.852 % |
c |     62209 |   26492    86744 |   14220   10321   482479    46.7 |  2.852 % |
c |     62968 |   26492    86744 |   15642   11080   518644    46.8 |  2.852 % |
c |     64109 |   26492    86744 |   17207   12221   575864    47.1 |  2.852 % |
c |     65817 |   26492    86744 |   18927   13929   671448    48.2 |  2.852 % |
c |     68380 |   26492    86744 |   20820   16492   791321    48.0 |  2.852 % |
c |     72224 |   26492    86744 |   22902   20336  1038178    51.1 |  2.852 % |
c |     77993 |   26492    86744 |   25193   26105  1602134    61.4 |  2.852 % |
c |     86642 |   26492    86744 |   27712   21702  1613426    74.3 |  2.852 % |
c ==============================================================================
c [1mFound solution: 107[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1313   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90492 |   26493    86754 |    8831   25552  1851614    72.5 |  2.852 % |
c |     90592 |   26493    86754 |    9714    6488   296083    45.6 |  2.865 % |
c |     90742 |   26493    86754 |   10685    6638   298105    44.9 |  2.865 % |
c |     90967 |   26493    86754 |   11754    6863   301577    43.9 |  2.865 % |
c |     91304 |   26493    86754 |   12929    7200   303911    42.2 |  2.865 % |
c |     91810 |   26493    86754 |   14222    7706   318504    41.3 |  2.865 % |
c |     92569 |   26493    86754 |   15644    8465   366545    43.3 |  2.865 % |
c |     93708 |   26493    86754 |   17209    9604   427191    44.5 |  2.865 % |
c |     95418 |   26493    86754 |   18930   11314   506391    44.8 |  2.865 % |
c |     97982 |   26493    86754 |   20823   13878   666721    48.0 |  2.865 % |
c |    101827 |   26493    86754 |   22905   17723  1003862    56.6 |  2.865 % |
c |    107595 |   26493    86754 |   25195   23491  1603772    68.3 |  2.865 % |
c |    116244 |   26493    86754 |   27715   18209  2007969   110.3 |  2.865 % |
c |    129219 |   26493    86754 |   30487   14477  1299051    89.7 |  2.865 % |
c |    148680 |   26493    86754 |   33535   33938  3505926   103.3 |  2.865 % |
c |    177873 |   26493    86754 |   36889   19569  1981304   101.2 |  2.865 % |
c ==============================================================================
c [1mFound solution: 106[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1314   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203130 |   26495    86767 |    8831   17932  2342869   130.7 |  2.865 % |
c |    203230 |   26495    86767 |    9714    9066  1059460   116.9 |  2.877 % |
c |    203380 |   26495    86767 |   10685    9216  1060308   115.1 |  2.877 % |
c |    203605 |   26495    86767 |   11754    9441  1061663   112.5 |  2.877 % |
c |    203942 |   26495    86767 |   12929    9778  1064191   108.8 |  2.877 % |
c |    204450 |   26495    86767 |   14222   10286  1076718   104.7 |  2.877 % |
c |    205211 |   26495    86767 |   15644   11047  1099524    99.5 |  2.877 % |
c |    206350 |   26495    86767 |   17209   12186  1151779    94.5 |  2.877 % |
c |    208058 |   26495    86767 |   18930   13894  1290178    92.9 |  2.877 % |
c |    210620 |   26495    86767 |   20823   16456  1424602    86.6 |  2.877 % |
c |    214466 |   26495    86767 |   22905   20302  1945374    95.8 |  2.877 % |
c |    220234 |   26495    86767 |   25195   13589  1290861    95.0 |  2.877 % |
c |    228886 |   26495    86767 |   27715   22241  2221897    99.9 |  2.877 % |
c |    241860 |   26495    86767 |   30487   16824  1624022    96.5 |  2.877 % |
c |    261324 |   26495    86767 |   33535   18036  1297748    72.0 |  2.877 % |
c |    290519 |   26495    86767 |   36889   27027  2715164   100.5 |  2.877 % |
c |    334311 |   26495    86767 |   40578   18135  1843579   101.7 |  2.877 % |
c |    399995 |   26495    86767 |   44636   25387  6045749   238.1 |  2.877 % |
c ==============================================================================
c [1mFound solution: 98[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1322   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    445674 |   26500    86799 |    8833   37759  6320294   167.4 |  2.877 % |
c |    445774 |   26500    86799 |    9716    6732   774985   115.1 |  2.915 % |
c |    445924 |   26500    86799 |   10687    6882   775935   112.7 |  2.915 % |
c |    446151 |   26500    86799 |   11756    7109   777542   109.4 |  2.915 % |
c |    446488 |   26500    86799 |   12932    7446   782594   105.1 |  2.915 % |
c |    446994 |   26500    86799 |   14225    7952   795902   100.1 |  2.915 % |
c |    447753 |   26500    86799 |   15648    8711   803084    92.2 |  2.915 % |
c |    448892 |   26500    86799 |   17213    9850   821221    83.4 |  2.915 % |
c |    450600 |   26500    86799 |   18934   11558   878453    76.0 |  2.915 % |
c |    453165 |   26500    86799 |   20827   14123  1062292    75.2 |  2.915 % |
c |    457009 |   26500    86799 |   22910   17967  1272621    70.8 |  2.915 % |
c |    462775 |   26500    86799 |   25201   11982   661214    55.2 |  2.915 % |
c |    471427 |   26500    86799 |   27721   20634  1378808    66.8 |  2.915 % |
c |    484402 |   26500    86799 |   30493   14154  2586201   182.7 |  2.915 % |
c |    503864 |   26500    86799 |   33543   33616  5188761   154.4 |  2.915 % |
c |    533056 |   26500    86799 |   36897   18884  2969903   157.3 |  2.915 % |
c |    576845 |   26500    86799 |   40587   35392  5877484   166.1 |  2.915 % |
c |    642534 |   26500    86799 |   44646   42901  8342933   194.5 |  2.915 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v785 v740 v420 v82 -v860 v744 v418 -v859 -v784 v501 -v307 -v85 v788 v419 -v86 -v63 -v861 v504 -v424 v354 -v306 -v62 v863 -v789 -v573 v505 -v64 -v572 -v478 -v441 v353 -v312 -v65 -v27 v864 -v574 -v477 -v310 -v102 v66 v866 -v810 v575 -v479 -v440 -v359 -v262 -v185 -v101 v73 v26 v867 -v814 v576 -v482 -v357 -v311 -v190 v107 -v67 -v30 -v697 v583 v481 -v446 -v399 -v315 -v265 -v216 -v189 -v143 v106 -v68 -v701 v577 v486 -v444 -v358 -v266 -v142 v108 -v69 -v31 -v2 -v578 v485 -v398 v362 v192 -v166 -v144 v112 -v1 -v660 -v579 v483 -v445 v193 v147 v111 -v7 -v659 -v594 -v558 v484 -v449 -v404 -v196 v165 v146 v109 -v6 -v661 -v598 -v557 -v402 -v194 v151 v110 -v8 -v662 v559 -v332 -v195 v171 v150 -v12 v663 -v562 -v403 v169 v148 -v11 v668 v561 v407 -v335 v149 -v9 v664 v563 -v336 v170 -v10 v739 v421 v81 -v855 v743 -v854 -v786 v500 v425 -v302 -v87 v790 -v423 -v862 v506 -v349 -v308 v865 v869 -v835 -v792 -v436 v355 -v313 -v90 -v76 v868 -v839 -v793 -v77 -v809 -v586 -v509 -v442 v360 -v316 -v261 -v212 -v72 v28 -v813 -v587 v480 -v314 -v184 v103 -v32 -v696 v582 -v494 -v447 -v394 v363 -v267 -v215 -v186 v104 -v70 -v700 v490 v361 -v191 v105 v580 v489 -v450 -v400 v188 -v161 v116 -v34 -v448 -v197 -v145 -v35 -v3 -v593 -v542 -v405 -v270 v167 -v159 -v4 -v597 -v155 v5 v671 v408 -v331 v172 -v154 -v16 v672 v560 v406 v667 -v571 -v466 -v337 -v173 v567 v470 -v174 v781 v741 -v496 v422 v83 v745 v426 -v787 v502 -v88 -v856 v791 -v301 -v857 -v795 v747 v507 -v303 v91 -v75 v858 -v794 v748 -v348 -v309 -v89 -v74 -v22 v873 -v834 v761 -v585 -v510 v350 v305 -v257 -v21 -v838 -v765 -v584 -v508 -v435 v356 -v317 -v811 -v491 -v437 v352 -v263 -v211 v29 -v815 -v493 -v443 v364 -v33 -v698 -v439 -v268 -v217 v119 -v71 -v37 -v702 -v451 -v393 -v187 v120 -v36 -v817 v581 -v538 v487 -v395 -v271 -v205 -v156 v115 -v818 -v401 -v269 v201 -v160 -v158 -v704 v670 -v595 -v541 v488 v397 -v327 -v220 v200 -v162 v113 v19 -v705 v669 -v599 v409 v168 v20 -v722 -v568 -v333 v164 -v152 -v15 -v726 -v570 v175 v665 v601 -v465 -v338 -v153 -v131 -v13 v602 -v566 v469 v742 v434 -v79 v780 v746 -v495 v430 v84 v782 v750 -v497 v429 v80 v783 v749 v503 v92 -v876 v799 v499 v877 -v805 -v511 -v304 v872 -v836 v804 v760 v325 -v207 -v840 -v764 -v692 -v492 v351 v321 -v256 -v23 -v884 -v870 -v812 -v691 -v372 v320 v258 -v213 v118 -v24 -v888 -v816 -v438 -v368 -v264 v117 v25 -v842 -v820 -v699 -v459 -v367 v260 -v218 -v202 -v41 -v843 -v819 -v703 -v589 -v455 -v272 -v204 -v157 -v707 -v588 -v537 -v454 -v221 -v18 -v706 -v396 -v219 -v17 -v596 -v543 -v417 v198 -v114 -v600 -v569 -v413 -v326 -v163 -v721 v604 -v412 -v328 -v199 -v183 v127 -v725 v603 -v334 -v179 v666 v546 -v467 v330 -v178 v130 -v14 -v564 v471 v339 v903 v433 -v78 -v875 v802 -v754 v427 v100 -v874 -v830 v803 -v498 v96 -v829 v798 -v519 v428 -v322 v95 -v515 v324 -v837 -v796 v762 -v514 -v369 -v841 v806 v766 -v371 -v206 -v883 -v871 -v845 v807 -v456 -v318 -v291 -v208 v44 -v887 -v844 v808 -v693 -v458 v259 -v214 -v203 v45 -v824 -v768 -v694 v533 -v383 -v365 -v319 v280 -v210 -v40 -v769 -v695 v276 -v222 -v711 v619 v539 -v452 -v414 -v366 v275 -v38 v623 -v590 -v416 v591 -v544 -v453 -v180 v592 v461 -v182 -v723 -v608 v547 v460 -v410 v126 -v727 v545 -v329 -v468 -v411 -v347 -v176 v132 -v565 v472 v343 v801 -v431 v97 v800 v99 -v753 -v654 -v516 -v756 -v518 -v323 v755 -v751 v521 v93 -v831 v525 -v370 -v832 -v797 v763 -v512 v287 -v249 v94 v43 -v833 v767 -v457 v42 -v885 -v849 v827 v771 -v513 -v379 -v290 -v277 -v889 v828 -v770 v279 -v209 -v823 -v714 -v382 -v230 -v715 v532 -v415 -v226 v891 -v821 -v710 -v641 v618 v534 -v273 -v225 -v39 v892 -v717 -v645 v622 v540 -v181 -v716 -v708 -v679 v611 v536 -v274 -v122 -v55 -v683 v612 v548 -v724 -v607 -v344 v128 -v728 v462 -v346 v729 -v605 v463 -v240 -v177 v133 v730 v464 -v342 v904 -v432 v98 -v517 -v653 -v752 v520 -v245 -v879 v757 v524 -v878 -v852 -v826 v758 v286 v248 -v853 -v825 v759 -v278 -v886 -v848 v775 -v713 -v378 -v292 -v227 v890 -v712 -v229 v894 -v846 -v384 v893 -v822 -v640 v620 -v610 -v295 -v223 -v51 -v644 v624 -v609 v535 -v709 v678 v556 -v387 -v224 -v54 -v718 v682 -v552 -v345 v121 -v719 -v626 -v551 -v236 v123 v720 -v627 v12#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 32094
Raw data (stat): 32094 (runsolver) R 32093 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479368619 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.0007 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 2800 0 0 0 991 7 0 0 25 0 1 0 479368619 13037568 2652 4294967295 134512640 134672761 3221224624 3221138992 134592331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3183 2652 603 41 0 3142 0
vsize: 12732
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 2928 0 0 0 1990 7 0 0 25 0 1 0 479368619 13561856 2780 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3311 2780 603 41 0 3270 0
vsize: 13244
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3607 0 0 0 2987 10 0 0 25 0 1 0 479368619 16392192 3459 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4002 3459 603 41 0 3961 0
vsize: 16008
[startup+40.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3844 0 0 0 3986 10 0 0 25 0 1 0 479368619 17334272 3696 4294967295 134512640 134672761 3221224624 3221223728 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4232 3696 603 41 0 4191 0
vsize: 16928
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3844 0 0 0 4987 10 0 0 25 0 1 0 479368619 17334272 3696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4232 3696 603 41 0 4191 0
vsize: 16928
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3844 0 0 0 5987 10 0 0 25 0 1 0 479368619 17334272 3696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4232 3696 603 41 0 4191 0
vsize: 16928
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 3905 0 0 0 6987 10 0 0 25 0 1 0 479368619 17604608 3757 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4298 3757 603 41 0 4257 0
vsize: 17192
[startup+80.0016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 4158 0 0 0 7986 11 0 0 25 0 1 0 479368619 18616320 4010 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4545 4010 603 41 0 4504 0
vsize: 18180
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 32094
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 4161 0 0 0 8986 11 0 0 25 0 1 0 479368619 18616320 4013 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4545 4013 603 41 0 4504 0
vsize: 18180
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 3/57 32133
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 4443 0 0 0 9986 12 0 0 25 0 1 0 479368619 19824640 4295 4294967295 134512640 134672761 3221224624 3221223808 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4840 4295 603 41 0 4799 0
vsize: 19360
[startup+110.004 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 32147
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5412 0 0 0 10983 15 0 0 25 0 1 0 479368619 23732224 5264 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5794 5264 603 41 0 5753 0
vsize: 23176
[startup+120.003 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 32147
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5643 0 0 0 11983 15 0 0 25 0 1 0 479368619 24678400 5495 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6025 5495 603 41 0 5984 0
vsize: 24100
[startup+130.004 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 32147
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5643 0 0 0 12983 15 0 0 25 0 1 0 479368619 24678400 5495 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6025 5495 603 41 0 5984 0
vsize: 24100
[startup+140.004 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 32147
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5807 0 0 0 13983 16 0 0 25 0 1 0 479368619 25477120 5659 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6220 5659 603 41 0 6179 0
vsize: 24880
[startup+150.005 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 32147
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5963 0 0 0 14983 16 0 0 25 0 1 0 479368619 26148864 5815 4294967295 134512640 134672761 3221224624 3221223856 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6384 5815 603 41 0 6343 0
vsize: 25536
[startup+160.004 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 32147
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 5963 0 0 0 15983 16 0 0 25 0 1 0 479368619 26148864 5815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6384 5815 603 41 0 6343 0
vsize: 25536
[startup+170.004 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 32147
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6289 0 0 0 16983 17 0 0 25 0 1 0 479368619 27496448 6141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6141 603 41 0 6672 0
vsize: 26852
[startup+180.004 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6505 0 0 0 17982 18 0 0 25 0 1 0 479368619 28438528 6357 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6943 6357 603 41 0 6902 0
vsize: 27772
[startup+190.004 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6505 0 0 0 18982 18 0 0 25 0 1 0 479368619 28438528 6357 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6943 6357 603 41 0 6902 0
vsize: 27772
[startup+200.005 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6505 0 0 0 19982 18 0 0 25 0 1 0 479368619 28438528 6357 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6943 6357 603 41 0 6902 0
vsize: 27772
[startup+210.005 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 6993 0 0 0 20981 19 0 0 25 0 1 0 479368619 30449664 6845 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7434 6845 603 41 0 7393 0
vsize: 29736
[startup+220.005 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7952 0 0 0 21979 22 0 0 25 0 1 0 479368619 34336768 7804 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8383 7804 603 41 0 8342 0
vsize: 33532
[startup+230.005 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 22979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8416 7839 603 41 0 8375 0
vsize: 33664
[startup+240.005 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 23979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8416 7839 603 41 0 8375 0
vsize: 33664
[startup+250.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 24979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8416 7839 603 41 0 8375 0
vsize: 33664
[startup+260.005 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 25979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8416 7839 603 41 0 8375 0
vsize: 33664
[startup+270.005 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 26979 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8416 7839 603 41 0 8375 0
vsize: 33664
[startup+280.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 27980 22 0 0 25 0 1 0 479368619 34471936 7839 4294967295 134512640 134672761 3221224624 3221223580 1075349771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8416 7839 603 41 0 8375 0
vsize: 33664
[startup+290.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 28980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+300.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 29980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+310.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 30980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+320.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 31980 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+330.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 32981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+340.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 33981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+350.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 34981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+360.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 35981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+370.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 36981 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+380.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 37982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+390.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 38982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+400.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 39982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+410.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 7987 0 0 0 40982 22 0 0 25 0 1 0 479368619 34463744 7839 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8414 7839 603 41 0 8373 0
vsize: 33656
[startup+420.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 8142 0 0 0 41982 23 0 0 25 0 1 0 479368619 35139584 7994 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8579 7994 603 41 0 8538 0
vsize: 34316
[startup+430.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9009 0 0 0 42980 25 0 0 25 0 1 0 479368619 38637568 8861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9433 8861 603 41 0 9392 0
vsize: 37732
[startup+440.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 43979 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9564 8998 603 41 0 9523 0
vsize: 38256
[startup+450.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 44980 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9564 8998 603 41 0 9523 0
vsize: 38256
[startup+460.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 45980 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9564 8998 603 41 0 9523 0
vsize: 38256
[startup+470.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32149
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9146 0 0 0 46980 25 0 0 25 0 1 0 479368619 39174144 8998 4294967295 134512640 134672761 3221224624 3221223728 134560070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9564 8998 603 41 0 9523 0
vsize: 38256
[startup+480.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 9922 0 0 0 47978 27 0 0 25 0 1 0 479368619 42401792 9774 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10352 9774 603 41 0 10311 0
vsize: 41408
[startup+490.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 10612 0 0 0 48977 29 0 0 25 0 1 0 479368619 45252608 10464 4294967295 134512640 134672761 3221224624 3221223728 134554926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11048 10464 603 41 0 11007 0
vsize: 44192
[startup+500.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 11365 0 0 0 49975 31 0 0 25 0 1 0 479368619 48349184 11217 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11804 11217 603 41 0 11763 0
vsize: 47216
[startup+510.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 12060 0 0 0 50973 33 0 0 25 0 1 0 479368619 51175424 11912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12494 11912 603 41 0 12453 0
vsize: 49976
[startup+520.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 12810 0 0 0 51971 36 0 0 25 0 1 0 479368619 54272000 12662 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13250 12662 603 41 0 13209 0
vsize: 53000
[startup+530.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 52968 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13809 13212 603 41 0 13768 0
vsize: 55236
[startup+540.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 53969 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13809 13212 603 41 0 13768 0
vsize: 55236
[startup+550.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 54969 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13809 13212 603 41 0 13768 0
vsize: 55236
[startup+560.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 55969 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13809 13212 603 41 0 13768 0
vsize: 55236
[startup+570.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 56968 38 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13809 13212 603 41 0 13768 0
vsize: 55236
[startup+580.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 57968 39 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13809 13212 603 41 0 13768 0
vsize: 55236
[startup+590.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13360 0 0 0 58968 39 0 0 25 0 1 0 479368619 56561664 13212 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13809 13212 603 41 0 13768 0
vsize: 55236
[startup+600.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13362 0 0 0 59968 39 0 0 25 0 1 0 479368619 56561664 13214 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13809 13214 603 41 0 13768 0
vsize: 55236
[startup+610.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 60968 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 13215 603 41 0 13750 0
vsize: 55164
[startup+620.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 61967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 13215 603 41 0 13750 0
vsize: 55164
[startup+630.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 62967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 13215 603 41 0 13750 0
vsize: 55164
[startup+640.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 63967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 13215 603 41 0 13750 0
vsize: 55164
[startup+650.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13363 0 0 0 64967 40 0 0 25 0 1 0 479368619 56487936 13215 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13791 13215 603 41 0 13750 0
vsize: 55164
[startup+660.017 s]
Raw data (loadavg): 1.00 1.00 0.92 3/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 65967 41 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13146 603 41 0 13666 0
vsize: 54828
[startup+670.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 66966 41 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13146 603 41 0 13666 0
vsize: 54828
[startup+680.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 67966 42 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13146 603 41 0 13666 0
vsize: 54828
[startup+690.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 68966 42 0 0 25 0 1 0 479368619 56143872 13146 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13707 13146 603 41 0 13666 0
vsize: 54828
[startup+700.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 69966 43 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223624 1075350113 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13696 13135 603 41 0 13655 0
vsize: 54784
[startup+710.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 70966 43 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13696 13135 603 41 0 13655 0
vsize: 54784
[startup+720.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 71965 43 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13696 13135 603 41 0 13655 0
vsize: 54784
[startup+730.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 72965 44 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13696 13135 603 41 0 13655 0
vsize: 54784
[startup+740.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 73965 44 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13696 13135 603 41 0 13655 0
vsize: 54784
[startup+750.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 74965 45 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13696 13135 603 41 0 13655 0
vsize: 54784
[startup+760.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 75965 45 0 0 25 0 1 0 479368619 56098816 13135 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13696 13135 603 41 0 13655 0
vsize: 54784
[startup+770.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 76964 45 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+780.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 77963 46 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+790.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 78963 46 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+800.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 79963 47 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+810.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 80963 47 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223804 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+820.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 81962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+830.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 82962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+840.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 83962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223720 1075347361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+850.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 84962 48 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+860.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 85961 49 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+870.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 86961 49 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+880.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 87960 50 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+890.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 88960 50 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223564 1075350563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+900.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 89960 51 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 90959 51 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+920.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 91959 52 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+930.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 92959 52 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+940.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 93959 52 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+950.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 94958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+960.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 95958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223808 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+970.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 96958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223804 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+980.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 97958 53 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+990.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 98958 54 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 99958 54 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 100957 54 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 101957 55 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 102957 55 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 103957 55 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 104957 56 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 105956 56 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 106956 57 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13364 0 0 0 107956 57 0 0 25 0 1 0 479368619 55853056 13075 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13075 603 41 0 13595 0
vsize: 54544
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 108955 57 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 109955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 110955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 111955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 112955 58 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 113955 59 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 114955 59 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 115954 59 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13366 0 0 0 116954 60 0 0 25 0 1 0 479368619 55853056 13077 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13636 13077 603 41 0 13595 0
vsize: 54544
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13367 0 0 0 117954 60 0 0 25 0 1 0 479368619 55853056 13078 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13636 13078 603 41 0 13595 0
vsize: 54544
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13367 0 0 0 118955 60 0 0 25 0 1 0 479368619 55853056 13078 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13636 13078 603 41 0 13595 0
vsize: 54544
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32151
Raw data (stat): 32094 (minisat+) R 32093 28546 28545 0 -1 0 13367 0 0 0 119955 60 0 0 25 0 1 0 479368619 55853056 13078 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13636 13078 603 41 0 13595 0
vsize: 54544
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 32151
Raw data (stat): 32094 (minisat+) Z 32093 28546 28545 0 -1 12 13370 0 0 0 119955 62 0 0 25 0 1 0 479368619 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.07
CPU time (s): 1200.18
CPU user time (s): 1199.56
CPU system time (s): 0.624905
CPU usage (%): 100.009
Max. virtual memory (Kb): 55236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####