PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod013.opb
MD5SUM	b964292d4197638ce79b3f213e8fe89b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5130240
Optimality of the best value was proved	NO
Number of terms in the objective function	1008
Biggest coefficient in the objective function	366477312
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	12643636975
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	366477312
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	12643636975
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	1008
Total number of constraints	110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	48
Number of constraints which are nor clauses,nor cardinality constraints	62
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 19057

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 17:45:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17056 boxname=wulflinc15 idbench=1312 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b964292d4197638ce79b3f213e8fe89b  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-mod013.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-mod013.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-mod013.opb
IDLAUNCH: 17056
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        583580 kB
Buffers:         32264 kB
Cached:         397328 kB
SwapCached:        440 kB
Active:          70376 kB
Inactive:       361352 kB
HighTotal:      131008 kB
HighFree:          504 kB
LowTotal:       903652 kB
LowFree:        583076 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13724 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:05:10 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 17056 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   19
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  58]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   14
c ---[  46]---> Sorter-cost: 1495     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   13
c ---[  34]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  22]---> Sorter-cost: 1441     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  10]---> Sorter-cost: 1391     Base: 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   4]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  970     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   40242    95592 |   13414       0        0     nan |  0.000 % |
c |       100 |   40242    95592 |   14755     100      425     4.2 |  7.948 % |
c |       250 |   40190    95474 |   16230     248     1098     4.4 |  8.044 % |
c ==============================================================================
c [1mFound solution: 11170220[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4334   maxlim: 19794243   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       301 |   70461   203609 |   23487     299     1310     4.4 |  8.044 % |
c |       401 |   70461   203609 |   25835     399     1672     4.2 |  6.250 % |
c |       551 |   70461   203609 |   28419     549     2303     4.2 |  6.250 % |
c |       776 |   70461   203609 |   31261     774     3315     4.3 |  6.250 % |
c |      1113 |   70452   203578 |   34387    1109     9709     8.8 |  6.255 % |
c ==============================================================================
c [1mFound solution: 10705958[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 20258505   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1289 |   70413   203641 |   23471    1279    10625     8.3 |  6.255 % |
c |      1390 |   70413   203641 |   25818    1380    17217    12.5 |  6.394 % |
c |      1540 |   70413   203641 |   28399    1530    18118    11.8 |  6.394 % |
c |      1765 |   70413   203641 |   31239    1755    19858    11.3 |  6.394 % |
c |      2103 |   70413   203641 |   34363    2093    27111    13.0 |  6.394 % |
c ==============================================================================
c [1mFound solution: 9557265[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21407198   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2184 |   70435   203897 |   23478    2174    28294    13.0 |  6.394 % |
c |      2285 |   70435   203897 |   25825    2275    28792    12.7 |  6.462 % |
c |      2435 |   70435   203897 |   28408    2425    30299    12.5 |  6.462 % |
c |      2660 |   70435   203897 |   31249    2650    74817    28.2 |  6.462 % |
c |      2997 |   70435   203897 |   34374    2987    77551    26.0 |  6.462 % |
c |      3503 |   70435   203897 |   37811    3493   169940    48.7 |  6.462 % |
c |      4264 |   70396   203809 |   41592    4252   239359    56.3 |  6.520 % |
c |      5403 |   70396   203809 |   45751    5391   343988    63.8 |  6.520 % |
c |      7111 |   70396   203809 |   50327    7099   753160   106.1 |  6.520 % |
c |      9673 |   70353   203712 |   55359    9659  1011595   104.7 |  6.584 % |
c ==============================================================================
c [1mFound solution: 8089439[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22875024   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10537 |   70371   203866 |   23457   10523  1092409   103.8 |  6.584 % |
c |     10638 |   70371   203866 |   25802   10624  1098153   103.4 |  6.632 % |
c |     10788 |   70342   203798 |   28382   10772  1106905   102.8 |  6.674 % |
c |     11014 |   70342   203798 |   31221   10998  1125804   102.4 |  6.674 % |
c |     11352 |   70275   203645 |   34343   11331  1179446   104.1 |  6.774 % |
c |     11859 |   70213   203502 |   37777   11835  1227611   103.7 |  6.874 % |
c |     12618 |   70046   203117 |   41555   12583  1262212   100.3 |  7.148 % |
c |     13758 |   70030   203081 |   45711   13722  1298067    94.6 |  7.169 % |
c |     15467 |   70030   203081 |   50282   15431  1444729    93.6 |  7.169 % |
c |     18029 |   69897   202778 |   55310   17976  1770930    98.5 |  7.390 % |
c |     21873 |   69893   202768 |   60841   21819  2644466   121.2 |  7.395 % |
c ==============================================================================
c [1mFound solution: 7533276[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23431187   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25289 |   69904   202860 |   23301   25234  2836153   112.4 |  7.395 % |
c |     25389 |   69904   202860 |   25631   12717  1388257   109.2 |  7.438 % |
c |     25539 |   69904   202860 |   28194   12867  1390092   108.0 |  7.438 % |
c |     25764 |   69904   202860 |   31013   13092  1403485   107.2 |  7.438 % |
c |     26101 |   69904   202860 |   34114   13429  1429001   106.4 |  7.438 % |
c |     26609 |   69900   202850 |   37526   13936  1465827   105.2 |  7.443 % |
c |     27368 |   69736   202471 |   41279   14686  1508853   102.7 |  7.733 % |
c |     28508 |   69736   202471 |   45407   15826  1606581   101.5 |  7.733 % |
c |     30217 |   69736   202471 |   49947   17535  1759205   100.3 |  7.733 % |
c |     32780 |   69692   202369 |   54942   20095  1891938    94.1 |  7.791 % |
c |     36625 |   69692   202369 |   60436   23940  3378534   141.1 |  7.791 % |
c |     42391 |   69623   202214 |   66480   29702  4034180   135.8 |  7.896 % |
c |     51041 |   69623   202214 |   73128   38352  5676912   148.0 |  7.896 % |
c ==============================================================================
c [1mFound solution: 6029863[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24934600   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51799 |   69609   202306 |   23203   39107  5726337   146.4 |  7.896 % |
c |     51899 |   69609   202306 |   25523   14965  1826892   122.1 |  8.016 % |
c |     52050 |   69609   202306 |   28075   15116  1832509   121.2 |  8.016 % |
c |     52275 |   69609   202306 |   30883   15341  1871762   122.0 |  8.016 % |
c |     52614 |   69543   202157 |   33971   15676  1901780   121.3 |  8.116 % |
c |     53121 |   69521   202108 |   37368   16181  1927057   119.1 |  8.152 % |
c |     53881 |   69521   202108 |   41105   16941  2114754   124.8 |  8.152 % |
c |     55021 |   69521   202108 |   45216   18081  2327564   128.7 |  8.152 % |
c |     56731 |   69521   202108 |   49737   19791  2667790   134.8 |  8.152 % |
c |     59293 |   69486   202019 |   54711   22350  3045403   136.3 |  8.200 % |
c |     63138 |   69482   202009 |   60182   26194  3545891   135.4 |  8.205 % |
c ==============================================================================
c [1mFound solution: 5780339[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25184124   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65463 |   69424   201303 |   23141   28315  4081649   144.2 |  8.205 % |
c |     65563 |   69424   201303 |   25455   14258  1745256   122.4 |  8.277 % |
c |     65713 |   69287   200988 |   28000   14399  1746701   121.3 |  8.524 % |
c |     65938 |   69278   200968 |   30800   14623  1748561   119.6 |  8.540 % |
c |     66276 |   69278   200968 |   33880   14961  1766003   118.0 |  8.540 % |
c |     66782 |   69278   200968 |   37268   15467  1807570   116.9 |  8.540 % |
c |     67541 |   69278   200968 |   40995   16226  1836568   113.2 |  8.540 % |
c |     68681 |   69253   200913 |   45095   17363  1892328   109.0 |  8.577 % |
c |     70389 |   69253   200913 |   49604   19071  1997262   104.7 |  8.577 % |
c |     72952 |   69238   200879 |   54565   21633  2191718   101.3 |  8.603 % |
c |     76797 |   69238   200879 |   60021   25478  2651885   104.1 |  8.603 % |
c |     82563 |   69165   200714 |   66023   31241  3029729    97.0 |  8.724 % |
c |     91214 |   69154   200688 |   72626   39890  5604613   140.5 |  8.734 % |
c |    104189 |   69103   200575 |   79889   52863  6609847   125.0 |  8.813 % |
c |    123654 |   69099   200565 |   87877   72327  8264391   114.3 |  8.818 % |
c |    152846 |   69099   200565 |   96665   17635  3087836   175.1 |  8.818 % |
c |    196636 |   69095   200556 |  106332   61424 17102835   278.4 |  8.824 % |
c |    262321 |   69058   200469 |  116965   25994  4280701   164.7 |  8.887 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1_0x2e__bit_7 -C1_0x2e__bit_6 -C1_0x2e__bit_5 -C1_0x2e__bit_4 -C1_0x2e__bit_3 -C1_0x2e__bit_2 C1_0x2e__bit_1 -C1_0x2e__bit0 -C1_0x2e__bit1 C1_0x2e__bit2 C1_0x2e__bit3 -C1_0x2e__bit4 -C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C2_0x2e__bit_7 -C2_0x2e__bit_6 -C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 -C2_0x2e__bit_2 -C2_0x2e__bit_1 -C2_0x2e__bit0 -C2_0x2e__bit1 -C2_0x2e__bit2 -C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C3_0x2e__bit_7 -C3_0x2e__bit_6 -C3_0x2e__bit_5 -C3_0x2e__bit_4 -C3_0x2e__bit_3 -C3_0x2e__bit_2 -C3_0x2e__bit_1 -C3_0x2e__bit0 -C3_0x2e__bit1 -C3_0x2e__bit2 -C3_0x2e__bit3 -C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 -C4_0x2e__bit_7 -C4_0x2e__bit_6 -C4_0x2e__bit_5 -C4_0x2e__bit_4 -C4_0x2e__bit_3 -C4_0x2e__bit_2 -C4_0x2e__bit_1 -C4_0x2e__bit0 -C4_0x2e__bit1 C4_0x2e__bit2 -C4_0x2e__bit3 C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C5_0x2e__bit_7 -C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 -C5_0x2e__bit_3 -C5_0x2e__bit_2 -C5_0x2e__bit_1 -C5_0x2e__bit0 C5_0x2e__bit1 C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 -C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 -C7_0x2e__bit_7 -C7_0x2e__bit_6 -C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 -C7_0x2e__bit_2 C7_0x2e__bit_1 -C7_0x2e__bit0 C7_0x2e__bit1 C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C8_0x2e__bit_7 -C8_0x2e__bit_6 -C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 -C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 C9_0x2e__bit_7 -C9_0x2e__bit_6 -C9_0x2e__bit_5 C9_0x2e__bit_4 -C9_0x2e__bit_3 -C9_0x2e__bit_2 -C9_0x2e__bit_1 C9_0x2e__bit0 C9_0x2e__bit1 C9_0x2e__bit2 C9_0x2e__bit3 -C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 C10_0x2e__bit_7 C10_0x2e__bit_6 C10_0x2e__bit_5 -C10_0x2e__bit_4 C10_0x2e__bit_3 C10_0x2e__bit_2 C10_0x2e__bit_1 C10_0x2e__bit0 C10_0x2e__bit1 C10_0x2e__bit2 C10_0x2e__bit3 -C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 -C11_0x2e__bit_7 -C11_0x2e__bit_6 -C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 -C11_0x2e__bit0 -C11_0x2e__bit1 -C11_0x2e__bit2 -C11_0x2e__bit3 -C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 -C12_0x2e__bit_7 -C12_0x2e__bit_6 -C12_0x2e__bit_5 -C12_0x2e__bit_4 -C12_0x2e__bit_3 -C12_0x2e__bit_2 -C12_0x2e__bit_1 -C12_0x2e__bit0 -C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 -C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 -C13_0x2e__bit_7 -C13_0x2e__bit_6 -C13_0x2e__bit_5 -C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 -C13_0x2e__bit_1 C13_0x2e__bit0 -C13_0x2e__bit1 -C13_0x2e__bit2 C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C14_0x2e__bit_7 -C14_0x2e__bit_6 -C14_0x2e__bit_5 -C14_0x2e__bit_4 -C14_0x2e__bit_3 -C14_0x2e__bit_2 -C14_0x2e__bit_1 -C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 -C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 -C16_0x2e__bit_7 -C16_0x2e__bit_6 -C16_0x2e__bit_5 -C16_0x2e__bit_4 -C16_0x2e__bit_3 -C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 -C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 C17_0x2e__bit_7 C17_0x2e__bit_6 C17_0x2e__bit_5 -C17_0x2e__bit_4 C17_0x2e__bit_3 C17_0x2e__bit_2 -C17_0x2e__bit_1 C17_0x2e__bit0 C17_0x2e__bit1 C17_0x2e__bit2 -C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 C18_0x2e__bit_7 -C18_0x2e__bit_6 -C18_0x2e__bit_5 C18_0x2e__bit_4 -C18_0x2e__bit_3 -C18_0x2e__bit_2 C18_0x2e__bit_1 C18_0x2e__bit0 C18_0x2e__bit1 C18_0x2e__bit2 -C18_0x2e__bit3 -C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 -C19_0x2e__bit_7 -C19_0x2e__bit_6 -C19_0x2e__bit_5 -C19_0x2e__bit_4 -C19_0x2e__bit_3 -C19_0x2e__bit_2 C19_0x2e__bit_1 C19_0x2e__bit0 C19_0x2e__bit1 -C19_0x2e__bit2 C19_0x2e__bit3 -C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 -C21_0x2e__bit_7 -C21_0x2e__bit_6 -C21_0x2e__bit_5 -C21_0x2e__bit_4 -C21_0x2e__bit_3 -C21_0x2e__bit_2 -C21_0x2e__bit_1 -C21_0x2e__bit0 -C21_0x2e__bit1 -C21_0x2e__bit2 -C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 -C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 C24_0x2e__bit_1 C24_0x2e__bit0 C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 -C25_0x2e__bit_7 -C25_0x2e__bit_6 -C25_0x2e__bit_5 -C25_0x2e__bit_4 -C25_0x2e__bit_3 -C25_0x2e__bit_2 -C25_0x2e__bit_1 -C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 -C26_0x2e__bit_7 -C26_0x2e__bit_6 -C26_0x2e__bit_5 -C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 -C26_0x2e__bit1 -C26_0x2e__bit2 -C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 C27_0x2e__bit_1 C27_0x2e__bit0 -C27_0x2e__bit1 C27_0x2e__bit2 C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 -C28_0x2e__bit_7 -C28_0x2e__bit_6 -C28_0x2e__bit_5 -C28_0x2e__bit_4 -C28_0x2e__bit_3 -C28_0x2e__bit_2 -C28_0x2e__bit_1 -C28_0x2e__bit0 -C28_0x2e__bit1 -C28_0x2e__bit2 -C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 -C29_0x2e__bit_7 -C29_0x2e__bit_6 -C29_0x2e__bit_5 -C29_0x2e__bit_4 -C29_0x2e__bit_3 -C29_0x2e__bit_2 -C29_0x2e__bit_1 -C29_0x2e__bit0 -C29_0x2e__bit1 -C29_0x2e__bit2 -C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 -C30_0x2e__bit_7 -C30_0x2e__bit_6 -C30_0x2e__bit_5 -C30_0x2e__bit_4 -C30_0x2e__bit_3 -C30_0x2e__bit_2 C30_0x2e__bit_1 -C30_0x2e__bit0 C30_0x2e__bit1 C30_0x2e__bit2 -C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 -C31_0x2e__bit_7 -C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 -C31_0x2e__bit0 -C31_0x2e__bit1 -C31_0x2e__bit2 -C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 -C32_0x2e__bit_7 -C32_0x2e__bit_6 -C32_0x2e__bit_5 -C32_0x2e__bit_4 -C32_0x2e__bit_3 -C32_0x2e__bit_2 -C32_0x2e__bit_1 -C32_0x2e__bit0 -C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C33_0x2e__bit_7 -C33_0x2e__bit_6 -C33_0x2e__bit_5 -C33_0x2e__bit_4 -C33_0x2e__bit_3 -C33_0x2e__bit_2 -C33_0x2e__bit_1 -C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C34_0x2e__bit_7 -C34_0x2e__bit_6 -C34_0x2e__bit_5 -C34_0x2e__bit_4 -C34_0x2e__bit_3 -C34_0x2e__bit_2 C34_0x2e__bit_1 -C34_0x2e__bit0 C34_0x2e__bit1 C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C35_0x2e__bit_7 -C35_0x2e__bit_6 -C35_0x2e__bit_5 -C35_0x2e__bit_4 -C35_0x2e__bit_3 -C35_0x2e__bit_2 -C35_0x2e__bit_1 -C35_0x2e__bit0 -C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 -C36_0x2e__bit_7 -C36_0x2e__bit_6 -C36_0x2e__bit_5 -C36_0x2e__bit_4 -C36_0x2e__bit_3 -C36_0x2e__bit_2 -C36_0x2e__bit_1 -C36_0x2e__bit0 -C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C37_0x2e__bit_7 -C37_0x2e__bit_6 -C37_0x2e__bit_5 -C37_0x2e__bit_4 -C37_0x2e__bit_3 -C37_0x2e__bit_2 -C37_0x2e__bit_1 -C37_0x2e__bit0 -C37_0x2e__bit1 -C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C38_0x2e__bit_7 -C38_0x2e__bit_6 -C38_0x2e__bit_5 -C38_0x2e__bit_4 -C38_0x2e__bit_3 -C38_0x2e__bit_2 C38_0x2e__bit_1 C38_0x2e__bit0 C38_0x2e__bit1 -C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -#### 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 11572
Raw data (stat): 11572 (runsolver) R 11571 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488756562 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.001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 4828 0 0 0 985 12 0 0 25 0 1 0 488756562 20185088 4030 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4928 4030 603 41 0 4887 0
vsize: 19712
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 5519 0 0 0 1982 15 0 0 25 0 1 0 488756562 23019520 4721 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5620 4721 603 41 0 5579 0
vsize: 22480
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 6047 0 0 0 2981 16 0 0 25 0 1 0 488756562 24793088 5176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6053 5176 603 41 0 6012 0
vsize: 24212
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 6595 0 0 0 3979 18 0 0 25 0 1 0 488756562 27152384 5724 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6629 5724 603 41 0 6588 0
vsize: 26516
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 7333 0 0 0 4978 19 0 0 25 0 1 0 488756562 30220288 6462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7378 6462 603 41 0 7337 0
vsize: 29512
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 7656 0 0 0 5977 20 0 0 25 0 1 0 488756562 31428608 6785 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7673 6785 603 41 0 7632 0
vsize: 30692
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 7811 0 0 0 6975 21 0 0 25 0 1 0 488756562 31784960 6868 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7760 6868 603 41 0 7719 0
vsize: 31040
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 7811 0 0 0 7974 22 0 0 25 0 1 0 488756562 31784960 6868 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7760 6868 603 41 0 7719 0
vsize: 31040
[startup+90.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 7984 0 0 0 8974 22 0 0 25 0 1 0 488756562 32456704 7041 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7924 7041 603 41 0 7883 0
vsize: 31696
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 8675 0 0 0 9972 24 0 0 25 0 1 0 488756562 35266560 7732 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8610 7732 603 41 0 8569 0
vsize: 34440
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 9172 0 0 0 10970 26 0 0 25 0 1 0 488756562 37285888 8229 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8229 603 41 0 9062 0
vsize: 36412
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10075 0 0 0 11968 29 0 0 25 0 1 0 488756562 41172992 9132 4294967295 134512640 134672761 3221224544 3221223648 134559905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10052 9132 603 41 0 10011 0
vsize: 40208
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10784 0 0 0 12965 32 0 0 25 0 1 0 488756562 44109824 9841 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10769 9841 603 41 0 10728 0
vsize: 43076
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10917 0 0 0 13965 32 0 0 25 0 1 0 488756562 44281856 9901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9901 603 41 0 10770 0
vsize: 43244
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10917 0 0 0 14965 32 0 0 25 0 1 0 488756562 44281856 9901 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9901 603 41 0 10770 0
vsize: 43244
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10917 0 0 0 15965 32 0 0 25 0 1 0 488756562 44281856 9901 4294967295 134512640 134672761 3221224544 3221223664 134542715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9901 603 41 0 10770 0
vsize: 43244
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 16965 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 17965 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 18966 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 19966 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 20966 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 21966 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 22966 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223728 134559583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 10919 0 0 0 23966 32 0 0 25 0 1 0 488756562 44281856 9903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10811 9903 603 41 0 10770 0
vsize: 43244
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 11184 0 0 0 24966 33 0 0 25 0 1 0 488756562 45363200 10168 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11075 10168 603 41 0 11034 0
vsize: 44300
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 11590 0 0 0 25964 35 0 0 25 0 1 0 488756562 46956544 10574 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11464 10574 603 41 0 11423 0
vsize: 45856
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 11993 0 0 0 26963 36 0 0 25 0 1 0 488756562 48693248 10977 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11888 10977 603 41 0 11847 0
vsize: 47552
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 12356 0 0 0 27963 36 0 0 25 0 1 0 488756562 50040832 11340 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12217 11340 603 41 0 12176 0
vsize: 48868
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 12814 0 0 0 28962 38 0 0 25 0 1 0 488756562 51929088 11798 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12678 11798 603 41 0 12637 0
vsize: 50712
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 13207 0 0 0 29961 39 0 0 25 0 1 0 488756562 53792768 12191 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13133 12191 603 41 0 13092 0
vsize: 52532
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 13733 0 0 0 30960 40 0 0 25 0 1 0 488756562 55947264 12717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13659 12717 603 41 0 13618 0
vsize: 54636
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 13988 0 0 0 31960 40 0 0 25 0 1 0 488756562 57028608 12972 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13923 12972 603 41 0 13882 0
vsize: 55692
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 14323 0 0 0 32959 41 0 0 25 0 1 0 488756562 58368000 13307 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13307 603 41 0 14209 0
vsize: 57000
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 14651 0 0 0 33958 42 0 0 25 0 1 0 488756562 59699200 13635 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14575 13635 603 41 0 14534 0
vsize: 58300
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 14930 0 0 0 34957 43 0 0 25 0 1 0 488756562 60760064 13914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14834 13914 603 41 0 14793 0
vsize: 59336
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 15352 0 0 0 35957 44 0 0 25 0 1 0 488756562 62504960 14336 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15260 14336 603 41 0 15219 0
vsize: 61040
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 16089 0 0 0 36954 47 0 0 25 0 1 0 488756562 65572864 15073 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16009 15073 603 41 0 15968 0
vsize: 64036
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 16800 0 0 0 37952 49 0 0 25 0 1 0 488756562 68403200 15784 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16700 15784 603 41 0 16659 0
vsize: 66800
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17487 0 0 0 38951 51 0 0 25 0 1 0 488756562 71213056 16471 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17386 16471 603 41 0 17345 0
vsize: 69544
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 39951 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 40950 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 41950 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 42951 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 43951 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 44951 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 45951 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 46951 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 47952 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 48952 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 49952 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 50952 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 51952 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 17855 0 0 0 52952 51 0 0 25 0 1 0 488756562 72687616 16839 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17746 16839 603 41 0 17705 0
vsize: 70984
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 18204 0 0 0 53952 52 0 0 25 0 1 0 488756562 74133504 17188 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18099 17188 603 41 0 18058 0
vsize: 72396
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 18815 0 0 0 54950 54 0 0 25 0 1 0 488756562 76636160 17799 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18710 17799 603 41 0 18669 0
vsize: 74840
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 19359 0 0 0 55949 55 0 0 25 0 1 0 488756562 78864384 18343 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19254 18343 603 41 0 19213 0
vsize: 77016
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 19965 0 0 0 56947 57 0 0 25 0 1 0 488756562 81375232 18949 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19867 18949 603 41 0 19826 0
vsize: 79468
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 20599 0 0 0 57945 59 0 0 25 0 1 0 488756562 84025344 19583 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20514 19583 603 41 0 20473 0
vsize: 82056
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 21169 0 0 0 58944 60 0 0 25 0 1 0 488756562 86274048 20153 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21063 20153 603 41 0 21022 0
vsize: 84252
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 21695 0 0 0 59943 61 0 0 25 0 1 0 488756562 88494080 20679 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21605 20679 603 41 0 21564 0
vsize: 86420
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 22162 0 0 0 60942 63 0 0 25 0 1 0 488756562 90333184 21146 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22054 21146 603 41 0 22013 0
vsize: 88216
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 22624 0 0 0 61941 64 0 0 25 0 1 0 488756562 92323840 21608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22540 21608 603 41 0 22499 0
vsize: 90160
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 23067 0 0 0 62940 65 0 0 25 0 1 0 488756562 94056448 22051 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22963 22051 603 41 0 22922 0
vsize: 91852
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 23470 0 0 0 63939 66 0 0 25 0 1 0 488756562 95666176 22454 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23356 22454 603 41 0 23315 0
vsize: 93424
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 23856 0 0 0 64938 67 0 0 25 0 1 0 488756562 97275904 22840 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23749 22840 603 41 0 23708 0
vsize: 94996
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 24259 0 0 0 65937 69 0 0 25 0 1 0 488756562 99020800 23243 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24175 23243 603 41 0 24134 0
vsize: 96700
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 24653 0 0 0 66937 69 0 0 25 0 1 0 488756562 100511744 23637 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24573 23639 603 41 0 24532 0
vsize: 98156
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 25218 0 0 0 67936 70 0 0 25 0 1 0 488756562 102932480 24202 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25130 24202 603 41 0 25089 0
vsize: 100520
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 25752 0 0 0 68934 72 0 0 25 0 1 0 488756562 105082880 24736 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25655 24736 603 41 0 25614 0
vsize: 102620
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 26430 0 0 0 69933 74 0 0 25 0 1 0 488756562 107884544 25414 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26339 25414 603 41 0 26298 0
vsize: 105356
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 27098 0 0 0 70931 75 0 0 25 0 1 0 488756562 110563328 26082 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26993 26082 603 41 0 26952 0
vsize: 107972
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 27700 0 0 0 71930 76 0 0 25 0 1 0 488756562 113070080 26684 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27605 26684 603 41 0 27564 0
vsize: 110420
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 28312 0 0 0 72929 78 0 0 25 0 1 0 488756562 115609600 27296 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28225 27296 603 41 0 28184 0
vsize: 112900
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 28921 0 0 0 73928 79 0 0 25 0 1 0 488756562 118026240 27905 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28815 27905 603 41 0 28774 0
vsize: 115260
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 29776 0 0 0 74926 82 0 0 25 0 1 0 488756562 121511936 28760 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29666 28760 603 41 0 29625 0
vsize: 118664
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 30578 0 0 0 75924 83 0 0 25 0 1 0 488756562 124858368 29562 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30483 29562 603 41 0 30442 0
vsize: 121932
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 31348 0 0 0 76922 85 0 0 25 0 1 0 488756562 127946752 30332 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31237 30332 603 41 0 31196 0
vsize: 124948
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 32108 0 0 0 77921 87 0 0 25 0 1 0 488756562 131117056 31092 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32011 31092 603 41 0 31970 0
vsize: 128044
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 32727 0 0 0 78920 88 0 0 25 0 1 0 488756562 133533696 31711 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32601 31711 603 41 0 32560 0
vsize: 130404
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33338 0 0 0 79919 90 0 0 25 0 1 0 488756562 136085504 32322 4294967295 134512640 134672761 3221224544 3221223648 134559818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33224 32322 603 41 0 33183 0
vsize: 132896
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33927 0 0 0 80917 91 0 0 25 0 1 0 488756562 138477568 32911 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33808 32911 603 41 0 33767 0
vsize: 135232
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 81918 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 82917 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223728 134558923 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 83917 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 84918 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 85918 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 86918 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 87918 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11572
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 88918 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11619
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 89919 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11625
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 90920 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11625
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 91920 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11625
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 92920 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11625
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 93920 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11625
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 94920 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11625
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 95921 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11625
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 96921 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 97921 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 98921 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 99922 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 100922 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 101922 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 102922 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 103922 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 104922 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 105923 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 106923 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 107923 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 108923 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 109923 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 110924 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 111924 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223708 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 112924 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 113924 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 114924 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 115925 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 116925 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 117925 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 118925 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11627
Raw data (stat): 11572 (minisat+) R 11571 29151 29150 0 -1 0 33959 0 0 0 119925 91 0 0 25 0 1 0 488756562 138608640 32943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32943 603 41 0 33799 0
vsize: 135360
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 11627
Raw data (stat): 11572 (minisat+) Z 11571 29151 29150 0 -1 12 33962 0 0 0 119926 97 0 0 25 0 1 0 488756562 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.24
CPU user time (s): 1199.26
CPU system time (s): 0.976851
CPU usage (%): 100.011
Max. virtual memory (Kb): 135360
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####