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.5:100.opb
MD5SUM	feaa96df552ef9989407735877840272
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13
Optimality of the best value was proved	NO
Number of terms in the objective function	776
Biggest coefficient in the objective function	474
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	2127
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	474
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	2127
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.04084
Number of variables	776
Total number of constraints	1642
Number of constraints which are clauses	701
Number of constraints which are cardinality constraints (but not clauses)	941
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 5313

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-13 23:20:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3753 boxname=wulflinc29 idbench=369 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  feaa96df552ef9989407735877840272  /oldhome/oroussel/tmp/wulflinc29/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc29/normalized-10:20:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc29/normalized-10:20:4.5:0.5:100.opb
IDLAUNCH: 3753
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        833704 kB
Buffers:         35856 kB
Cached:         127740 kB
SwapCached:         12 kB
Active:          52956 kB
Inactive:       113476 kB
HighTotal:      131008 kB
HighFree:          868 kB
LowTotal:       903652 kB
LowFree:        832836 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            28940 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:40:37 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3753 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 866 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 172]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 171]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 170]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 164]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 163]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 162]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 159]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 157]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 156]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 155]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 154]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 152]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 151]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 150]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[ 149]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 146]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 145]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 144]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 142]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 141]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 139]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 138]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 137]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 136]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 135]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 134]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 133]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 132]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 131]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 130]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 128]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 127]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 125]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 122]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 121]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 116]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 111]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 110]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 109]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  97]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[  96]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  91]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 17   maxlim: 1   bits: 2/1
c ---[  74]---> Adder-cost: 14   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 11   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  54]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  52]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  48]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  43]---> Adder-cost: 3   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  40]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  39]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  38]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  34]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  33]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  32]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  31]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  30]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 3   maxlim: 1   bits: 2/1
c ---[  28]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  27]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  25]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  20]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  19]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  17]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  15]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  12]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  11]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  10]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   9]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   8]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   7]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   6]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   5]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   3]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   2]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   1]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[   0]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13525    46719 |    4508       0        0     nan |  0.000 % |
c |       100 |   13525    46719 |    4958     100      459     4.6 |  9.091 % |
c |       250 |   13519    46702 |    5454     249     1162     4.7 |  9.121 % |
c ==============================================================================
c [1mFound solution: 148[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1866   maxlim: 1031   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       341 |   26509    93070 |    8836     340     1549     4.6 |  9.121 % |
c |       442 |   26509    93070 |    9719     441     3608     8.2 |  5.874 % |
c |       592 |   26509    93070 |   10691     591     4258     7.2 |  5.874 % |
c |       818 |   26509    93070 |   11760     817     5401     6.6 |  5.874 % |
c |      1156 |   26509    93070 |   12936    1155     8397     7.3 |  5.874 % |
c |      1662 |   26497    93036 |   14230    1659    10943     6.6 |  5.913 % |
c |      2422 |   26491    93019 |   15653    2418    15749     6.5 |  5.932 % |
c |      3562 |   26491    93019 |   17218    3558    30775     8.6 |  5.932 % |
c |      5272 |   26491    93019 |   18940    5268   113345    21.5 |  5.932 % |
c ==============================================================================
c [1mFound solution: 147[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1032   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6672 |   26504    93074 |    8834    6668   143392    21.5 |  5.932 % |
c |      6772 |   26504    93074 |    9717    6768   144297    21.3 |  5.947 % |
c |      6922 |   26504    93074 |   10689    6918   145352    21.0 |  5.947 % |
c |      7148 |   26504    93074 |   11758    7144   149735    21.0 |  5.947 % |
c |      7485 |   26504    93074 |   12933    7481   152028    20.3 |  5.947 % |
c |      7991 |   26504    93074 |   14227    7987   159683    20.0 |  5.947 % |
c |      8751 |   26498    93057 |   15649    8746   177211    20.3 |  5.966 % |
c |      9890 |   26498    93057 |   17214    9885   245839    24.9 |  5.966 % |
c |     11598 |   26498    93057 |   18936   11593   346989    29.9 |  5.966 % |
c |     14160 |   26498    93057 |   20830   14155   593234    41.9 |  5.966 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1088   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15966 |   26505    93091 |    8835   15961   698249    43.7 |  5.966 % |
c |     16066 |   26505    93091 |    9718    8081   453389    56.1 |  6.002 % |
c |     16216 |   26505    93091 |   10690    8231   455478    55.3 |  6.002 % |
c |     16441 |   26505    93091 |   11759    8456   459713    54.4 |  6.002 % |
c |     16778 |   26505    93091 |   12935    8793   465356    52.9 |  6.002 % |
c |     17284 |   26505    93091 |   14228    9299   487735    52.5 |  6.002 % |
c |     18043 |   26505    93091 |   15651   10058   504771    50.2 |  6.002 % |
c |     19184 |   26505    93091 |   17216   11199   549285    49.0 |  6.002 % |
c |     20893 |   26499    93074 |   18938   12906   649575    50.3 |  6.021 % |
c |     23458 |   26499    93074 |   20832   15471   782199    50.6 |  6.021 % |
c |     27303 |   26499    93074 |   22915   19316  1132781    58.6 |  6.021 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1089   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29429 |   26500    93084 |    8833   21442  1313517    61.3 |  6.021 % |
c |     29530 |   26500    93084 |    9716    5462   312662    57.2 |  6.039 % |
c |     29681 |   26500    93084 |   10687    5613   313616    55.9 |  6.039 % |
c |     29907 |   26500    93084 |   11756    5839   315428    54.0 |  6.039 % |
c |     30244 |   26500    93084 |   12932    6176   320931    52.0 |  6.039 % |
c |     30751 |   26500    93084 |   14225    6683   331465    49.6 |  6.039 % |
c |     31515 |   26494    93067 |   15648    7445   356303    47.9 |  6.058 % |
c |     32660 |   26494    93067 |   17213    8590   433987    50.5 |  6.058 % |
c |     34368 |   26494    93067 |   18934   10298   494772    48.0 |  6.058 % |
c |     36930 |   26494    93067 |   20827   12860   675224    52.5 |  6.058 % |
c |     40776 |   26494    93067 |   22910   16706   983169    58.9 |  6.058 % |
c ==============================================================================
c [1mFound solution: 78[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1101   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43286 |   26502    93112 |    8834   19216  1194741    62.2 |  6.058 % |
c |     43388 |   26502    93112 |    9717    4906   265167    54.0 |  6.111 % |
c |     43538 |   26502    93112 |   10689    5056   265977    52.6 |  6.111 % |
c |     43763 |   26502    93112 |   11758    5281   268981    50.9 |  6.111 % |
c |     44102 |   26502    93112 |   12933    5620   271602    48.3 |  6.111 % |
c |     44608 |   26502    93112 |   14227    6126   279825    45.7 |  6.111 % |
c |     45367 |   26502    93112 |   15649    6885   292558    42.5 |  6.111 % |
c |     46507 |   26502    93112 |   17214    8025   340113    42.4 |  6.111 % |
c |     48215 |   26502    93112 |   18936    9733   453201    46.6 |  6.111 % |
c |     50777 |   26502    93112 |   20830   12295   619303    50.4 |  6.111 % |
c |     54621 |   26502    93112 |   22913   16139   912279    56.5 |  6.111 % |
c |     60387 |   26502    93112 |   25204   21905  1354321    61.8 |  6.111 % |
c |     69038 |   26502    93112 |   27724   17394  1273843    73.2 |  6.111 % |
c |     82012 |   26502    93112 |   30497   30368  2465085    81.2 |  6.111 % |
c |    101473 |   26502    93112 |   33547   14896  2091770   140.4 |  6.111 % |
c |    130667 |   26502    93112 |   36901   22190  3156228   142.2 |  6.111 % |
c |    174456 |   26502    93112 |   40591   13605  2011770   147.9 |  6.111 % |
c |    240142 |   26502    93112 |   44651   22792  3757685   164.9 |  6.111 % |
c |    338668 |   26502    93112 |   49116   21531  1841180    85.5 |  6.111 % |
c |    486458 |   26502    93112 |   54027   26926  3450697   128.2 |  6.111 % |
c ==============================================================================
c [1mFound solution: 75[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1104   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    507282 |   26509    93147 |    8836   47750  5044537   105.6 |  6.111 % |
c |    507382 |   26509    93147 |    9719    7252   390857    53.9 |  6.146 % |
c |    507532 |   26509    93147 |   10691    7402   391593    52.9 |  6.146 % |
c |    507759 |   26509    93147 |   11760    7629   393436    51.6 |  6.146 % |
c |    508096 |   26509    93147 |   12936    7966   395766    49.7 |  6.146 % |
c |    508602 |   26509    93147 |   14230    8472   408032    48.2 |  6.146 % |
c |    509361 |   26509    93147 |   15653    9231   434043    47.0 |  6.146 % |
c |    510502 |   26509    93147 |   17218   10372   462820    44.6 |  6.147 % |
c |    512210 |   26509    93147 |   18940   12080   520832    43.1 |  6.146 % |
c |    514772 |   26509    93147 |   20834   14642   670409    45.8 |  6.146 % |
c |    518618 |   26509    93147 |   22918   18488   905970    49.0 |  6.146 % |
c |    524384 |   26509    93147 |   25210   24254  1406057    58.0 |  6.146 % |
c |    533034 |   26509    93147 |   27731   17744  1381937    77.9 |  6.146 % |
c |    546008 |   26509    93147 |   30504   30718  3023274    98.4 |  6.146 % |
c |    565469 |   26509    93147 |   33554   32601  3564901   109.3 |  6.146 % |
c |    594661 |   26509    93147 |   36910   16535  2176716   131.6 |  6.146 % |
c |    638453 |   26509    93147 |   40601   35229  4039853   114.7 |  6.146 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v756 -v693 v588 v262 -v241 v56 -v38 v692 -v590 -v486 v263 -v246 v55 -v37 -v757 v700 v589 -v485 v439 -v266 -v245 -v54 -v39 -v758 v694 v594 v487 -v444 -v264 -v52 v40 -v761 v695 -v612 v593 v488 -v443 -v265 -v248 -v53 -v47 -v759 v696 -v611 v591 v489 -v401 -v249 -v41 -v2 -v760 -v613 v592 v496 -v446 -v421 -v400 v252 -v198 -v171 -v42 -v1 -v734 v616 v490 -v447 -v420 -v406 -v385 v250 -v176 -v43 -v3 -v733 v615 v491 -v450 -v422 -v405 -v384 -v273 -v251 -v197 -v175 -v137 v4 -v620 v492 -v448 -v425 -v407 v386 -v366 -v278 -v201 -v155 -v136 -v18 v5 -v735 -v619 -v559 v510 -v449 -v424 -v411 v387 -v365 -v277 v178 v154 -v138 -v87 -v17 -v12 -v737 -v650 -v617 -v515 -v429 -v410 v388 -v202 -v179 v156 v141 -v86 -v23 -v6 -v649 -v618 v558 -v514 v466 -v428 -v408 -v395 -v367 -v280 -v182 v157 v140 -v88 -v66 -v22 -v7 -v738 -v562 -v426 -v409 v389 -v369 -v281 -v180 v158 -v145 -v91 -v71 -v24 -v8 -v740 -v651 -v517 v469 -v427 -v390 -v318 -v284 -v223 -v181 -v165 -v144 -v121 v90 -v70 v28 -v741 -v653 -v635 -v563 -v518 -v470 -v391 -v370 -v317 -v282 v159 -v142 v95 v27 -v634 -v521 -v372 -v347 -v319 -v283 -v222 v160 -v143 -v120 v94 -v73 v25 -v654 -v519 -v373 -v351 -v322 -v226 v161 v92 -v74 v26 v656 -v636 -v520 -v321 -v124 v93 v75 v657 v639 -v323 -v227 -v125 v76 -v753 v703 v64 -v755 v704 v587 -v267 -v240 v60 -v754 v699 -v602 -v242 v59 -v50 -v762 -v598 v438 -v247 -v51 -v710 v697 -v597 v499 v440 v244 -v46 -v714 v500 -v445 v253 v495 v442 -v44 -v729 -v614 v451 -v402 -v170 -v728 -v628 v493 -v403 -v199 v172 v15 -v624 -v423 -v404 -v361 -v272 -v203 -v177 v16 -v736 -v623 -v437 -v415 v398 -v360 -v274 v174 -v11 -v739 v645 v509 -v433 v399 -v279 v183 -v139 v19 -v743 v644 v560 v511 v465 -v432 -v394 -v368 -v276 -v205 -v168 v153 v20 -v9 -v742 -v564 -v516 -v371 -v285 -v206 -v169 v149 -v89 -v65 v21 v652 v513 v471 -v392 -v375 -v164 v148 -v116 v103 -v67 v32 -v655 -v630 -v522 -v374 v99 -v72 v659 -v629 -v566 -v346 -v224 -v162 -v122 -v98 v69 v658 -v567 -v350 -v320 -v228 v77 -v637 -v474 -v331 -v126 v638 -v327 v701 -v599 -v105 v63 -v49 -v752 -v601 v271 -v48 -v770 -v498 v270 v57 -v766 -v497 v243 -v765 -v709 v698 -v595 v261 v58 -v713 v441 -v257 -v193 -v625 -v596 v459 v302 -v256 -v192 -v45 -v14 -v627 v455 -v13 v494 v454 -v434 -v418 -v397 -v200 -v730 -v554 -v436 -v419 -v396 -v204 v173 -v731 -v621 -v553 -v461 -v414 -v208 v191 -v167 v150 -v732 -v362 -v275 -v207 -v187 -v166 v152 -v747 -v622 v561 v467 -v430 -v412 -v363 -v293 -v186 -v100 -v35 -v10 v646 -v565 v512 -v364 -v289 -v218 v102 -v36 -v685 v647 -v569 -v530 v472 -v431 -v393 -v379 -v288 -v217 v146 v31 v648 -v568 -v526 -v115 -v68 -v663 -v525 v475 -v348 -v328 -v225 -v163 v147 -v117 -v96 -v85 v29 -v631 v473 -v352 -v330 -v229 -v123 v81 v632 -v230 -v119 -v97 v80 v633 -v326 -v231 -v127 -v767 v702 -v600 v333 v104 v61 -v769 -v268 -v258 v260 -v763 v711 v456 v299 -v269 v715 -v626 v458 -v764 -v417 v301 -v254 -v435 -v416 -v194 v717 v452 -v255 -v195 -v188 v718 -v196 -v190 v151 -v750 v453 -v290 -v212 -v34 -v751 -v555 -v460 -v292 -v101 -v33 -v746 v681 -v556 -v527 -v462 -v413 -v382 -v184 v557 -v529 v468 -v383 -v343 -v744 -v684 -v666 -v573 v464 -v378 -v342 -v286 -v185 -v82 v667 v476 -v329 -v219 -v84 -v662 v534 -v523 -v376 -v349 -v287 -v220 v30 v538 -v353 -v221 -v118 -v660 -v642 v604 -v524 -v354 -v235 -v135 v78 -v643 v608 -v355 -v324 -v131 -v768 v332 v106 -v62 v706 -v259 v705 v457 v712 v298 -v108 v716 v720 v303 v719 -v189 -v749 -v215 -v748 -v291 -v216 v677 -v381 v306 -v211 -v528 -v380 v680 -v665 v576 -v209 -v664 v577 -v463 -v83 -v745 v686 -v572 v484 v480 -v344 -v641 -v570 v533 -v479 -v377 v345 -v238 -v132 -v640 v537 -v239 -v134 -v689 -v661 v603 -v234 v79 v607 -v325 -v130 -v502 -v295 v109 v707 -v107 v708 v546 v335 v300 v771 v724 v304 -v214 -v213 v673 v307 v305 -v772 v676 v773 -v575 v574 v682 -v481 -v210 v483 v687 -v237 -v236 -v133 -v690 -v571 v535 -v477 v358 -v688 v539 v359 v605 -v478 -v232 v609 -v128 v110 -v501 v336 v334 -v294 v727 v545 -v296 -v723 v308 -v721 v672 -v582 -v482 v683 -v532 v679 -v531 v357 v691 v356 v536 v540 v606 -v233 v610 -v129 v337 v114 v726 -v503 v113 v725 v547 v297 v669 v506 -v316 v312 -v722 v674 v581 #### 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.84 0.94 0.90 2/54 31718
Raw data (stat): 31718 (runsolver) R 31717 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479862292 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 1707 0 0 0 994 4 0 0 25 0 1 0 479862292 8687616 1685 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2121 1685 603 41 0 2080 0
vsize: 8484
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 2405 0 0 0 1992 5 0 0 25 0 1 0 479862292 11583488 2383 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2828 2383 603 41 0 2787 0
vsize: 11312
[startup+30.002 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 2405 0 0 0 2992 6 0 0 25 0 1 0 479862292 11583488 2383 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2828 2383 603 41 0 2787 0
vsize: 11312
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 2442 0 0 0 3992 6 0 0 25 0 1 0 479862292 11718656 2420 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2861 2420 603 41 0 2820 0
vsize: 11444
[startup+50.0028 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 2839 0 0 0 4991 6 0 0 25 0 1 0 479862292 13336576 2817 4294967295 134512640 134672761 3221224544 3221223712 134564673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3256 2817 603 41 0 3215 0
vsize: 13024
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 3614 0 0 0 5989 8 0 0 25 0 1 0 479862292 16433152 3592 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4012 3592 603 41 0 3971 0
vsize: 16048
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 3775 0 0 0 6989 9 0 0 25 0 1 0 479862292 17108992 3753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4177 3753 603 41 0 4136 0
vsize: 16708
[startup+80.0042 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 4127 0 0 0 7988 10 0 0 25 0 1 0 479862292 18583552 4105 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4537 4105 603 41 0 4496 0
vsize: 18148
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 4958 0 0 0 8986 12 0 0 25 0 1 0 479862292 21938176 4936 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5356 4936 603 41 0 5315 0
vsize: 21424
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 5079 0 0 0 9986 13 0 0 25 0 1 0 479862292 22478848 5057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5488 5057 603 41 0 5447 0
vsize: 21952
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 5164 0 0 0 10986 13 0 0 25 0 1 0 479862292 22880256 5142 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5586 5142 603 41 0 5545 0
vsize: 22344
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 5926 0 0 0 11984 15 0 0 25 0 1 0 479862292 26107904 5904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6374 5904 603 41 0 6333 0
vsize: 25496
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6236 0 0 0 12983 16 0 0 25 0 1 0 479862292 27320320 6214 4294967295 134512640 134672761 3221224544 3221223728 134558768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6214 603 41 0 6629 0
vsize: 26680
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6236 0 0 0 13983 16 0 0 25 0 1 0 479862292 27320320 6214 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6214 603 41 0 6629 0
vsize: 26680
[startup+150.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6237 0 0 0 14983 16 0 0 25 0 1 0 479862292 27320320 6215 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6215 603 41 0 6629 0
vsize: 26680
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6240 0 0 0 15983 16 0 0 25 0 1 0 479862292 27320320 6218 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6218 603 41 0 6629 0
vsize: 26680
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6240 0 0 0 16984 16 0 0 25 0 1 0 479862292 27320320 6218 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6218 603 41 0 6629 0
vsize: 26680
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6240 0 0 0 17984 16 0 0 25 0 1 0 479862292 27320320 6218 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6218 603 41 0 6629 0
vsize: 26680
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6241 0 0 0 18984 16 0 0 25 0 1 0 479862292 27320320 6219 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6219 603 41 0 6629 0
vsize: 26680
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6241 0 0 0 19984 16 0 0 25 0 1 0 479862292 27320320 6219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6219 603 41 0 6629 0
vsize: 26680
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6241 0 0 0 20984 16 0 0 25 0 1 0 479862292 27320320 6219 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6670 6219 603 41 0 6629 0
vsize: 26680
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 6334 0 0 0 21984 16 0 0 25 0 1 0 479862292 27721728 6312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6768 6312 603 41 0 6727 0
vsize: 27072
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7035 0 0 0 22983 18 0 0 25 0 1 0 479862292 30556160 7013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7460 7013 603 41 0 7419 0
vsize: 29840
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7767 0 0 0 23980 21 0 0 25 0 1 0 479862292 33636352 7745 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8212 7745 603 41 0 8171 0
vsize: 32848
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7931 0 0 0 24980 21 0 0 25 0 1 0 479862292 34308096 7909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7909 603 41 0 8335 0
vsize: 33504
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7931 0 0 0 25980 21 0 0 25 0 1 0 479862292 34308096 7909 4294967295 134512640 134672761 3221224544 3221223648 134554919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7909 603 41 0 8335 0
vsize: 33504
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7931 0 0 0 26980 21 0 0 25 0 1 0 479862292 34308096 7909 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7909 603 41 0 8335 0
vsize: 33504
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7931 0 0 0 27981 21 0 0 25 0 1 0 479862292 34308096 7909 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7909 603 41 0 8335 0
vsize: 33504
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7931 0 0 0 28981 21 0 0 25 0 1 0 479862292 34308096 7909 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7909 603 41 0 8335 0
vsize: 33504
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 7931 0 0 0 29981 21 0 0 25 0 1 0 479862292 34308096 7909 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8376 7909 603 41 0 8335 0
vsize: 33504
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 8225 0 0 0 30979 23 0 0 25 0 1 0 479862292 35549184 8203 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8679 8203 603 41 0 8638 0
vsize: 34716
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 8649 0 0 0 31979 24 0 0 25 0 1 0 479862292 37314560 8627 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9110 8627 603 41 0 9069 0
vsize: 36440
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9130 0 0 0 32978 25 0 0 25 0 1 0 479862292 39219200 9108 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9575 9108 603 41 0 9534 0
vsize: 38300
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9630 0 0 0 33976 26 0 0 25 0 1 0 479862292 41410560 9608 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10110 9608 603 41 0 10069 0
vsize: 40440
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9815 0 0 0 34976 27 0 0 25 0 1 0 479862292 42082304 9793 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9793 603 41 0 10233 0
vsize: 41096
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9816 0 0 0 35976 27 0 0 25 0 1 0 479862292 42082304 9794 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10274 9794 603 41 0 10233 0
vsize: 41096
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9816 0 0 0 36975 27 0 0 25 0 1 0 479862292 42082304 9794 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9794 603 41 0 10233 0
vsize: 41096
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9817 0 0 0 37975 27 0 0 25 0 1 0 479862292 42082304 9795 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9795 603 41 0 10233 0
vsize: 41096
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9820 0 0 0 38975 27 0 0 25 0 1 0 479862292 42082304 9798 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9798 603 41 0 10233 0
vsize: 41096
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9822 0 0 0 39976 27 0 0 25 0 1 0 479862292 42082304 9800 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9800 603 41 0 10233 0
vsize: 41096
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9822 0 0 0 40976 27 0 0 25 0 1 0 479862292 42082304 9800 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9800 603 41 0 10233 0
vsize: 41096
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 41976 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 42976 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 43976 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 44977 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 45977 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 46977 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 47977 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 48977 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 49978 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 50978 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 51978 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 52978 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 53978 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 54978 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 55978 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 56979 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9823 0 0 0 57979 27 0 0 25 0 1 0 479862292 42082304 9801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9801 603 41 0 10233 0
vsize: 41096
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 58979 27 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 59979 27 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 60979 28 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 61979 28 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 62979 28 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 63979 28 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 64979 28 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 9825 0 0 0 65979 28 0 0 25 0 1 0 479862292 42082304 9803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10274 9803 603 41 0 10233 0
vsize: 41096
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10281 0 0 0 66978 29 0 0 25 0 1 0 479862292 43962368 10259 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10733 10259 603 41 0 10692 0
vsize: 42932
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 67978 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 68978 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 69978 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 70978 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223500 1075349771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 71978 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 72978 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 73979 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 74979 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223440 134565829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 75979 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 76979 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 77979 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 78979 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 79980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 80980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 81980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 82980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 83980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 84980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 85981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 86980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 87980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 88980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 89980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 90981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 91980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 92980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 93980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 94980 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 95981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 96981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 97981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 98981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 99981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 100981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 101981 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 102982 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 103982 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 104982 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 105982 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 106982 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 107983 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 108983 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223500 1075349917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 109983 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 110983 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 111983 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 112983 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134559829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 113984 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 114984 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 115984 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 116984 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10491 0 0 0 117984 30 0 0 25 0 1 0 479862292 44900352 10469 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10469 603 41 0 10921 0
vsize: 43848
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10492 0 0 0 118985 30 0 0 25 0 1 0 479862292 44900352 10470 4294967295 134512640 134672761 3221224544 3221223648 134559910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10470 603 41 0 10921 0
vsize: 43848
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31718
Raw data (stat): 31718 (minisat+) R 31717 27222 27221 0 -1 0 10492 0 0 0 119985 30 0 0 25 0 1 0 479862292 44900352 10470 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10962 10470 603 41 0 10921 0
vsize: 43848
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31718
Raw data (stat): 31718 (minisat+) Z 31717 27222 27221 0 -1 12 10495 0 0 0 119985 32 0 0 25 0 1 0 479862292 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.04
CPU time (s): 1200.18
CPU user time (s): 1199.85
CPU system time (s): 0.328949
CPU usage (%): 100.012
Max. virtual memory (Kb): 43848
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####