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:10:4.5:0.95:100.opb
MD5SUM	b2c6bc03457d15976fdaf81252d9cdae
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	435
Biggest coefficient in the objective function	282
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	1168
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	282
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	1168
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	435
Total number of constraints	935
Number of constraints which are clauses	403
Number of constraints which are cardinality constraints (but not clauses)	532
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 6462

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890328 kB
Buffers:         36424 kB
Cached:          87812 kB
SwapCached:          0 kB
Active:          57440 kB
Inactive:        69664 kB
HighTotal:      131008 kB
HighFree:        39424 kB
LowTotal:       903652 kB
LowFree:        850904 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11540 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:25:33 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4877 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 500 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:    5
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    3
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   14
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    3
c ---[  81]---> BDD-cost:    7
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   20
c ---[  75]---> BDD-cost:   26
c ---[  74]---> BDD-cost:    7
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   29
c ---[  65]---> BDD-cost:   38
c ---[  64]---> BDD-cost:   32
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   15
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   32
c ---[  56]---> BDD-cost:   35
c ---[  55]---> BDD-cost:   38
c ---[  54]---> BDD-cost:   38
c ---[  53]---> BDD-cost:   27
c ---[  52]---> BDD-cost:   20
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   32
c ---[  45]---> BDD-cost:   41
c ---[  44]---> BDD-cost:   38
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   14
c ---[  38]---> BDD-cost:   20
c ---[  37]---> BDD-cost:   29
c ---[  36]---> BDD-cost:   32
c ---[  35]---> BDD-cost:   35
c ---[  34]---> BDD-cost:   38
c ---[  33]---> BDD-cost:   29
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   20
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:   23
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   32
c ---[  24]---> BDD-cost:   38
c ---[  23]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   23
c ---[  17]---> BDD-cost:   23
c ---[  16]---> BDD-cost:   23
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   26
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:    8
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   20
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   20
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   14
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9454    26412 |    3151       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 345[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24586     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   70477   169164 |   23492       0        0     nan |  0.000 % |
c |       101 |   69647   167273 |   25841      81      814    10.0 |  1.495 % |
c |       251 |   69647   167273 |   28425     231     3624    15.7 |  1.495 % |
c |       478 |   69453   166825 |   31267     453     6074    13.4 |  1.766 % |
c ==============================================================================
c [1mFound solution: 88[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       694 |   72603   174473 |   24201     669     7346    11.0 |  1.766 % |
c |       794 |   72603   174473 |   26621     769     9927    12.9 |  1.748 % |
c |       944 |   72438   174097 |   29283     917    10810    11.8 |  1.953 % |
c ==============================================================================
c [1mFound solution: 67[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       997 |   72599   174519 |   24199     956    11029    11.5 |  1.953 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1028 |   72612   174554 |   24204     987    13604    13.8 |  1.953 % |
c |      1128 |   72524   174357 |   26624    1077    16193    15.0 |  2.184 % |
c |      1279 |   72494   174289 |   29286    1225    21815    17.8 |  2.218 % |
c |      1504 |   72494   174289 |   32215    1450    26959    18.6 |  2.218 % |
c |      1841 |   72494   174289 |   35437    1787    32067    17.9 |  2.218 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 |   72155   173512 |   24051    2088    34281    16.4 |  2.218 % |
c |      2253 |   72085   173355 |   26456    2184    35243    16.1 |  2.762 % |
c |      2403 |   72085   173355 |   29101    2334    37073    15.9 |  2.762 % |
c |      2628 |   71682   172432 |   32011    2538    39821    15.7 |  3.259 % |
c |      2966 |   71485   171987 |   35213    2872    46521    16.2 |  3.489 % |
c |      3473 |   71429   171857 |   38734    3377    51047    15.1 |  3.565 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3563 |   71497   172032 |   23832    3467    51922    15.0 |  3.565 % |
c |      3663 |   71352   171695 |   26215    3562    54524    15.3 |  3.766 % |
c |      3813 |   71265   171494 |   28836    3710    57963    15.6 |  3.885 % |
c |      4038 |   71265   171494 |   31720    3935    62505    15.9 |  3.885 % |
c |      4375 |   71265   171494 |   34892    4272    71911    16.8 |  3.885 % |
c |      4883 |   71257   171476 |   38381    4779    83161    17.4 |  3.893 % |
c |      5644 |   71249   171458 |   42219    5536   101341    18.3 |  3.902 % |
c |      6783 |   71042   170984 |   46441    6651   111232    16.7 |  4.161 % |
c |      8491 |   70801   170430 |   51086    8351   152740    18.3 |  4.467 % |
c |     11053 |   70580   169917 |   56194   10828   203195    18.8 |  4.768 % |
c |     14897 |   70570   169894 |   61814   14670   283281    19.3 |  4.781 % |
c |     20663 |   70511   169760 |   67995   20422   732371    35.9 |  4.853 % |
c |     29315 |   70389   169480 |   74795   29051   997291    34.3 |  5.001 % |
c ==============================================================================
c [1mFound solution: 61[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30877 |   70404   169519 |   23468   30613  1049328    34.3 |  5.001 % |
c |     30978 |   70404   169519 |   25814   15097   512593    34.0 |  5.005 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31047 |   70408   169529 |   23469   15166   513914    33.9 |  5.005 % |
c |     31147 |   70408   169529 |   25815   15266   514506    33.7 |  5.009 % |
c |     31297 |   70408   169529 |   28397   15416   515257    33.4 |  5.009 % |
c |     31522 |   70408   169529 |   31237   15641   518536    33.2 |  5.009 % |
c |     31860 |   70408   169529 |   34360   15979   522652    32.7 |  5.009 % |
c |     32367 |   70408   169529 |   37797   16486   527808    32.0 |  5.009 % |
c |     33126 |   70037   168669 |   41576   17212   565365    32.8 |  5.510 % |
c |     34267 |   70037   168669 |   45734   18353   596763    32.5 |  5.510 % |
c |     35975 |   69989   168559 |   50307   20055   702328    35.0 |  5.569 % |
c |     38537 |   69821   168170 |   55338   22613   840042    37.1 |  5.794 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38909 |   69877   168315 |   23292   22985   848033    36.9 |  5.794 % |
c |     39009 |   69877   168315 |   25621   23085   849287    36.8 |  5.794 % |
c |     39159 |   69831   168211 |   28183   23231   850919    36.6 |  5.849 % |
c |     39384 |   69831   168211 |   31001   23456   852915    36.4 |  5.849 % |
c |     39723 |   69831   168211 |   34101   23795   858224    36.1 |  5.849 % |
c |     40229 |   69831   168211 |   37511   24301   874020    36.0 |  5.849 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40876 |   69852   168273 |   23284   24944   881879    35.4 |  5.849 % |
c |     40976 |   69848   168264 |   25612   12571   350453    27.9 |  5.917 % |
c |     41127 |   69848   168264 |   28173   12722   352685    27.7 |  5.917 % |
c ==============================================================================
c [1mFound solution: 39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41286 |   70040   168737 |   23346   12881   354004    27.5 |  5.917 % |
c |     41386 |   70040   168737 |   25680   12981   359738    27.7 |  5.907 % |
c |     41536 |   70040   168737 |   28248   13131   360976    27.5 |  5.907 % |
c |     41761 |   70040   168737 |   31073   13356   362592    27.1 |  5.907 % |
c |     42098 |   70040   168737 |   34180   13693   368009    26.9 |  5.907 % |
c |     42605 |   70040   168737 |   37598   14200   380665    26.8 |  5.907 % |
c |     43364 |   70005   168655 |   41358   14958   397687    26.6 |  5.962 % |
c |     44504 |   70005   168655 |   45494   16098   451657    28.1 |  5.962 % |
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46139 |   70016   168685 |   23338   17728   495292    27.9 |  5.962 % |
c |     46239 |   70016   168685 |   25671   17828   496271    27.8 |  5.969 % |
c |     46391 |   70016   168685 |   28238   17980   502303    27.9 |  5.969 % |
c ==============================================================================
c [1mFound solution: 36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46555 |   70020   168695 |   23340   18144   508596    28.0 |  5.969 % |
c |     46655 |   70020   168695 |   25674   18244   509370    27.9 |  5.973 % |
c |     46807 |   70020   168695 |   28241   18396   511285    27.8 |  5.973 % |
c ==============================================================================
c [1mFound solution: 34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46964 |   70075   168837 |   23358   18553   513891    27.7 |  5.973 % |
c |     47067 |   70075   168837 |   25693   18656   515006    27.6 |  5.973 % |
c |     47218 |   70075   168837 |   28263   18807   517545    27.5 |  5.973 % |
c |     47444 |   70075   168837 |   31089   19033   532958    28.0 |  5.973 % |
c |     47781 |   70075   168837 |   34198   19370   546931    28.2 |  5.973 % |
c |     48287 |   69870   168368 |   37618   19729   550155    27.9 |  6.235 % |
c |     49046 |   69870   168368 |   41380   20488   564109    27.5 |  6.235 % |
c |     50190 |   69832   168281 |   45518   21616   694507    32.1 |  6.282 % |
c |     51898 |   69832   168281 |   50069   23324   732163    31.4 |  6.281 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53772 |   69850   168327 |   23283   25198   803596    31.9 |  6.281 % |
c |     53872 |   69850   168327 |   25611   12699   308412    24.3 |  6.284 % |
c |     54022 |   69850   168327 |   28172   12849   309907    24.1 |  6.284 % |
c |     54251 |   69850   168327 |   30989   13078   313399    24.0 |  6.284 % |
c |     54589 |   69850   168327 |   34088   13416   320732    23.9 |  6.284 % |
c |     55095 |   69850   168327 |   37497   13922   326727    23.5 |  6.284 % |
c |     55855 |   69850   168327 |   41247   14682   343352    23.4 |  6.284 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56236 |   69911   168483 |   23303   15063   354623    23.5 |  6.284 % |
c |     56336 |   69911   168483 |   25633   15163   356819    23.5 |  6.284 % |
c |     56486 |   69911   168483 |   28196   15313   358233    23.4 |  6.284 % |
c |     56711 |   69911   168483 |   31016   15538   360867    23.2 |  6.284 % |
c |     57048 |   69911   168483 |   34117   15875   374519    23.6 |  6.284 % |
c |     57554 |   69869   168387 |   37529   16367   384062    23.5 |  6.334 % |
c |     58313 |   69869   168387 |   41282   17126   425372    24.8 |  6.334 % |
c ==============================================================================
c [1mFound solution: 29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58639 |   69884   168426 |   23294   17452   434129    24.9 |  6.334 % |
c |     58739 |   69884   168426 |   25623   17552   436449    24.9 |  6.338 % |
c |     58889 |   69884   168426 |   28185   17702   437976    24.7 |  6.338 % |
c |     59115 |   69884   168426 |   31004   17928   439698    24.5 |  6.338 % |
c |     59452 |   69884   168426 |   34104   18265   453209    24.8 |  6.338 % |
c |     59958 |   69884   168426 |   37515   18771   468272    24.9 |  6.338 % |
c |     60717 |   69881   168420 |   41266   19529   492674    25.2 |  6.342 % |
c ==============================================================================
c [1mFound solution: 28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61795 |   69881   168421 |   23293   20606   592077    28.7 |  6.342 % |
c |     61896 |   69881   168421 |   25622   20707   593898    28.7 |  6.350 % |
c |     62049 |   69881   168421 |   28184   20860   599916    28.8 |  6.350 % |
c |     62276 |   69881   168421 |   31002   21087   603337    28.6 |  6.350 % |
c |     62613 |   69881   168421 |   34103   21424   616929    28.8 |  6.350 % |
c |     63121 |   69881   168421 |   37513   21932   643869    29.4 |  6.350 % |
c |     63882 |   69881   168421 |   41264   22693   662043    29.2 |  6.350 % |
c |     65022 |   69881   168421 |   45391   23833   685895    28.8 |  6.350 % |
c |     66730 |   69881   168421 |   49930   25541   750857    29.4 |  6.350 % |
c |     69292 |   69881   168421 |   54923   28103   845062    30.1 |  6.350 % |
c ==============================================================================
c [1mFound solution: 27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71486 |   69933   168556 |   23311   30297  1156008    38.2 |  6.350 % |
c |     71586 |   69933   168556 |   25642   15249   519583    34.1 |  6.350 % |
c |     71736 |   69933   168556 |   28206   15399   521646    33.9 |  6.350 % |
c |     71961 |   69933   168556 |   31026   15624   525035    33.6 |  6.350 % |
c |     72298 |   69933   168556 |   34129   15961   531879    33.3 |  6.350 % |
c |     72804 |   69933   168556 |   37542   16467   570799    34.7 |  6.350 % |
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73372 |   69946   168591 |   23315   17035   595217    34.9 |  6.350 % |
c |     73474 |   69946   168591 |   25646   17137   597171    34.8 |  6.353 % |
c |     73624 |   69946   168591 |   28211   17287   600584    34.7 |  6.353 % |
c |     73849 |   69806   168269 |   31032   17505   603948    34.5 |  6.530 % |
c |     74186 |   69800   168255 |   34135   17836   608353    34.1 |  6.539 % |
c |     74692 |   69800   168255 |   37549   18342   616329    33.6 |  6.539 % |
c |     75451 |   69800   168255 |   41303   19101   638129    33.4 |  6.539 % |
c |     76590 |   69800   168255 |   45434   20240   662268    32.7 |  6.539 % |
c |     78298 |   69800   168255 |   49977   21948   687318    31.3 |  6.539 % |
c |     80863 |   69765   168176 |   54975   24505   723780    29.5 |  6.577 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82226 |   69777   168208 |   23259   25868   811344    31.4 |  6.577 % |
c |     82327 |   69777   168208 |   25584   13035   179676    13.8 |  6.580 % |
c |     82477 |   69777   168208 |   28143   13185   182916    13.9 |  6.580 % |
c |     82702 |   69777   168208 |   30957   13410   188618    14.1 |  6.580 % |
c |     83041 |   69777   168208 |   34053   13749   191754    13.9 |  6.580 % |
c |     83547 |   69732   168103 |   37458   14250   205531    14.4 |  6.643 % |
c |     84307 |   69732   168103 |   41204   15010   219925    14.7 |  6.643 % |
c |     85446 |   69732   168103 |   45325   16149   237651    14.7 |  6.643 % |
c |     87154 |   69732   168103 |   49857   17857   269234    15.1 |  6.643 % |
c |     89716 |   69732   168103 |   54843   20419   343751    16.8 |  6.643 % |
c |     93560 |   69732   168103 |   60327   24263   460500    19.0 |  6.643 % |
c ==============================================================================
c [1mFound solution: 24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94040 |   69736   168113 |   23245   24743   471767    19.1 |  6.643 % |
c |     94141 |   69736   168113 |   25569   24844   474555    19.1 |  6.647 % |
c |     94291 |   69736   168113 |   28126   24994   476428    19.1 |  6.647 % |
c |     94516 |   69736   168113 |   30939   25219   480558    19.1 |  6.647 % |
c |     94853 |   69736   168113 |   34033   25556   488558    19.1 |  6.647 % |
c |     95359 |   69736   168113 |   37436   26062   492998    18.9 |  6.647 % |
c |     96118 |   69736   168113 |   41179   26821   515302    19.2 |  6.647 % |
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96860 |   69797   168269 |   23265   27563   557478    20.2 |  6.647 % |
c |     96960 |   69797   168269 |   25591   13882   206048    14.8 |  6.646 % |
c |     97110 |   69776   168221 |   28150   14031   207021    14.8 |  6.671 % |
c |     97337 |   69776   168221 |   30965   14258   211992    14.9 |  6.672 % |
c |     97675 |   69776   168221 |   34062   14596   216978    14.9 |  6.671 % |
c |     98181 |   69772   168212 |   37468   15098   223008    14.8 |  6.676 % |
c |     98941 |   69595   167799 |   41215   15699   243543    15.5 |  6.924 % |
c |    100080 |   69595   167799 |   45336   16838   317317    18.8 |  6.924 % |
c |    101788 |   69595   167799 |   49870   18546   362327    19.5 |  6.924 % |
c |    104350 |   69595   167799 |   54857   21108   489556    23.2 |  6.924 % |
c |    108195 |   69595   167799 |   60343   24953   637727    25.6 |  6.924 % |
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111565 |   69608   167834 |   23202   28323   809392    28.6 |  6.924 % |
c |    111665 |   69608   167834 |   25522   14262   291547    20.4 |  6.927 % |
c |    111815 |   69608   167834 |   28074   14412   292987    20.3 |  6.928 % |
c |    112042 |   69608   167834 |   30881   14639   298180    20.4 |  6.927 % |
c |    112379 |   69608   167834 |   33970   14976   308404    20.6 |  6.928 % |
c |    112885 |   69608   167834 |   37367   15482   315040    20.3 |  6.927 % |
c |    113644 |   69608   167834 |   41103   16241   324615    20.0 |  6.927 % |
c |    114783 |   69608   167834 |   45214   17380   370844    21.3 |  6.927 % |
c |    116491 |   69608   167834 |   49735   19088   572293    30.0 |  6.927 % |
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117111 |   69620   167866 |   23206   19708   605442    30.7 |  6.927 % |
c |    117212 |   69620   167866 |   25526   19809   606404    30.6 |  6.931 % |
c |    117363 |   69620   167866 |   28079   19960   611311    30.6 |  6.931 % |
c |    117588 |   69620   167866 |   30887   20185   617441    30.6 |  6.931 % |
c |    117928 |   69620   167866 |   33975   20525   627960    30.6 |  6.931 % |
c |    118434 |   69620   167866 |   37373   21031   646770    30.8 |  6.931 % |
c |    119194 |   69620   167866 |   41110   21791   734554    33.7 |  6.931 % |
c |    120333 |   69620   167866 |   45221   22930   767450    33.5 |  6.931 % |
c |    122041 |   69590   167797 |   49744   24635   799050    32.4 |  6.969 % |
c |    124604 |   69590   167797 |   54718   27198   903924    33.2 |  6.969 % |
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128357 |   69594   167807 |   23198   30951  1059993    34.2 |  6.969 % |
c |    128460 |   69594   167807 |   25517   15579   284890    18.3 |  6.972 % |
c |    128611 |   69594   167807 |   28069   15730   287299    18.3 |  6.973 % |
c |    128836 |   69594   167807 |   30876   15955   289774    18.2 |  6.972 % |
c |    129173 |   69594   167807 |   33964   16292   296546    18.2 |  6.972 % |
c |    129679 |   69594   167807 |   37360   16798   311950    18.6 |  6.972 % |
c |    130439 |   69580   167775 |   41096   17555   327834    18.7 |  6.989 % |
c |    131579 |   69580   167775 |   45206   18695   372385    19.9 |  6.989 % |
c |    133287 |   69525   167649 |   49726   20393   429145    21.0 |  7.061 % |
c |    135849 |   69525   167649 |   54699   22955   521441    22.7 |  7.061 % |
c |    139693 |   69525   167649 |   60169   26799  1288347    48.1 |  7.061 % |
c |    145459 |   69525   167649 |   66186   32565  1953701    60.0 |  7.061 % |
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    148282 |   69577   167784 |   23192   35388  2476047    70.0 |  7.061 % |
c |    148383 |   69577   167784 |   25511   17795  1217332    68.4 |  7.061 % |
c |    148533 |   69577   167784 |   28062   17945  1219230    67.9 |  7.061 % |
c |    148758 |   69577   167784 |   30868   18170  1225654    67.5 |  7.061 % |
c |    149096 |   69577   167784 |   33955   18508  1230693    66.5 |  7.061 % |
c |    149602 |   69577   167784 |   37350   19014  1261615    66.4 |  7.061 % |
c |    150362 |   69566   167760 |   41086   19773  1277359    64.6 |  7.065 % |
c |    151501 |   69566   167760 |   45194   20912  1299738    62.2 |  7.065 % |
c |    153210 |   69566   167760 |   49714   22621  1371192    60.6 |  7.065 % |
c |    155772 |   69566   167760 |   54685   25183  1491835    59.2 |  7.065 % |
c |    159616 |   69566   167760 |   60154   29027  1762418    60.7 |  7.065 % |
c |    165382 |   69566   167760 |   66169   34793  2304316    66.2 |  7.065 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173031 |   69579   167795 |   23193   42442  3978534    93.7 |  7.065 % |
c |    173132 |   69579   167795 |   25512   21322  2056239    96.4 |  7.068 % |
c |    173282 |   69579   167795 |   28063   21472  2058841    95.9 |  7.068 % |
c |    173507 |   69579   167795 |   30869   21697  2063130    95.1 |  7.068 % |
c |    173844 |   69579   167795 |   33956   22034  2082877    94.5 |  7.068 % |
c |    174351 |   69579   167795 |   37352   22541  2094406    92.9 |  7.068 % |
c |    175110 |   69575   167786 |   41087   23299  2113134    90.7 |  7.072 % |
c |    176249 |   69575   167786 |   45196   24438  2214327    90.6 |  7.072 % |
c |    177957 |   69575   167786 |   49716   26146  2291099    87.6 |  7.072 % |
c |    180520 |   69575   167786 |   54687   28709  2433849    84.8 |  7.072 % |
c |    184366 |   69533   167690 |   60156   32551  2760076    84.8 |  7.123 % |
c |    190132 |   69533   167690 |   66172   38317  3766127    98.3 |  7.123 % |
c ==============================================================================
c [1mFound solution: 17[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    195953 |   69545   167722 |   23181   44138  4374050    99.1 |  7.123 % |
c |    196053 |   69545   167722 |   25499   22169  1610514    72.6 |  7.126 % |
c |    196205 |   69545   167722 |   28049   22321  1611622    72.2 |  7.126 % |
c |    196430 |   69545   167722 |   30853   22546  1615397    71.6 |  7.126 % |
c |    196767 |   69545   167722 |   33939   22883  1635812    71.5 |  7.126 % |
c |    197273 |   69545   167722 |   37333   23389  1650956    70.6 |  7.126 % |
c |    198032 |   69545   167722 |   41066   24148  1660514    68.8 |  7.126 % |
c |    199171 |   69545   167722 |   45173   25287  1704029    67.4 |  7.126 % |
c |    200879 |   69535   167700 |   49690   26994  1818302    67.4 |  7.130 % |
c |    203441 |   69535   167700 |   54659   29556  2046681    69.2 |  7.130 % |
c ==============================================================================
c [1mFound solution: 16[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206389 |   69538   167707 |   23179   32504  2163215    66.6 |  7.130 % |
c |    206489 |   69538   167707 |   25496   16352   371715    22.7 |  7.134 % |
c |    206639 |   69538   167707 |   28046   16502   375391    22.7 |  7.134 % |
c |    206864 |   69538   167707 |   30851   16727   381799    22.8 |  7.134 % |
c |    207201 |   69538   167707 |   33936   17064   389799    22.8 |  7.134 % |
c |    207708 |   69538   167707 |   37330   17571   406955    23.2 |  7.134 % |
c |    208467 |   69538   167707 |   41063   18330   440404    24.0 |  7.134 % |
c |    209606 |   69538   167707 |   45169   19469   512824    26.3 |  7.134 % |
c |    211314 |   69538   167707 |   49686   21177   569467    26.9 |  7.134 % |
c |    213876 |   69538   167707 |   54654   23739   698718    29.4 |  7.134 % |
c |    217720 |   69533   167692 |   60120   27576  1418934    51.5 |  7.138 % |
c |    223486 |   69463   167533 |   66132   33330  1786979    53.6 |  7.226 % |
c |    232137 |   69326   167215 |   72745   41952  2547860    60.7 |  7.411 % |
c |    245112 |   69326   167215 |   80020   54927  3725222    67.8 |  7.411 % |
c |    264573 |   69326   167215 |   88022   74388  8465319   113.8 |  7.411 % |
c ==============================================================================
c [1mFound solution: 15[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    270270 |   69379   167353 |   23126   80059  8708626   108.8 |  7.411 % |
c |    270370 |   69379   167353 |   25438   13544   115290     8.5 |  7.418 % |
c |    270520 |   69379   167353 |   27982   13694   118166     8.6 |  7.419 % |
c |    270745 |   69379   167353 |   30780   13919   128158     9.2 |  7.418 % |
c |    271082 |   69379   167353 |   33858   14256   140122     9.8 |  7.418 % |
c |    271588 |   69379   167353 |   37244   14762   182410    12.4 |  7.418 % |
c |    272348 |   69379   167353 |   40969   15522   221873    14.3 |  7.418 % |
c |    273487 |   69379   167353 |   45066   16661   255817    15.4 |  7.418 % |
c |    275197 |   69373   167339 |   49572   18368   372802    20.3 |  7.427 % |
c |    277760 |   69373   167339 |   54529   20931   512600    24.5 |  7.427 % |
c |    281604 |   69373   167339 |   59982   24775   714162    28.8 |  7.427 % |
c |    287371 |   69373   167339 |   65981   30542  1307706    42.8 |  7.427 % |
c ==============================================================================
c [1mFound solution: 14[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    288521 |   69386   167374 |   23128   31692  1326491    41.9 |  7.427 % |
c |    288621 |   69386   167374 |   25440   15946   293406    18.4 |  7.430 % |
c |    288772 |   69386   167374 |   27984   16097   298647    18.6 |  7.430 % |
c |    288998 |   69386   167374 |   30783   16323   302340    18.5 |  7.430 % |
c |    289336 |   69386   167374 |   33861   16661   311869    18.7 |  7.430 % |
c |    289842 |   69386   167374 |   37247   17167   330572    19.3 |  7.430 % |
c |    290602 |   69386   167374 |   40972   17927   342385    19.1 |  7.430 % |
c |    291741 |   69386   167374 |   45069   19066   414109    21.7 |  7.430 % |
c |    293449 |   69386   167374 |   49576   20774   474598    22.8 |  7.430 % |
c |    296012 |   69386   167374 |   54534   23337   795365    34.1 |  7.430 % |
c |    299857 |   69386   167374 |   59988   27182   872658    32.1 |  7.430 % |
c |    305623 |   69386   167374 |   65986   32948  1970024    59.8 |  7.430 % |
c ==============================================================================
c [1mFound solution: 13[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    308064 |   69398   167406 |   23132   35389  2043573    57.7 |  7.430 % |
c |    308164 |   69398   167406 |   25445   17795   954930    53.7 |  7.433 % |
c |    308315 |   69398   167406 |   27989   17946   957556    53.4 |  7.433 % |
c |    308540 |   69398   167406 |   30788   18171   962328    53.0 |  7.433 % |
c |    308877 |   69398   167406 |   33867   18508   968521    52.3 |  7.433 % |
c |    309385 |   69398   167406 |   37254   19016   986465    51.9 |  7.433 % |
c |    310145 |   69398   167406 |   40979   19776  1007088    50.9 |  7.433 % |
c |    311287 |   69398   167406 |   45077   20918  1045541    50.0 |  7.433 % |
c |    312996 |   69398   167406 |   49585   22627  1100126    48.6 |  7.433 % |
c |    315561 |   69398   167406 |   54544   25192  1191388    47.3 |  7.433 % |
c |    319405 |   69398   167406 |   59998   29036  1310321    45.1 |  7.433 % |
c |    325172 |   69388   167384 |   65998   34802  1472126    42.3 |  7.438 % |
c |    333823 |   69388   167384 |   72598   43453  2940128    67.7 |  7.438 % |
c |    346800 |   69249   167061 |   79857   56391  5314460    94.2 |  7.627 % |
c |    366262 |   69249   167061 |   87843   75853  8835451   116.5 |  7.627 % |
#### 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.99 1.00 0.94 2/54 13669
Raw data (stat): 13669 (runsolver) R 13668 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423709796 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+9.99976 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13669
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 2462 0 0 0 990 7 0 0 25 0 1 0 423709796 12214272 2384 4294967295 134512640 134672761 3221224544 3221223712 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2982 2384 603 41 0 2941 0
vsize: 11928
[startup+20.0004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13669
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 2649 0 0 0 1988 8 0 0 25 0 1 0 423709796 12922880 2571 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2571 603 41 0 3114 0
vsize: 12620
[startup+30.0006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13669
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 2852 0 0 0 2986 9 0 0 25 0 1 0 423709796 13828096 2774 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3376 2774 603 41 0 3335 0
vsize: 13504
[startup+40.0012 s]
Raw data (loadavg): 0.99 1.00 0.94 3/54 13669
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3235 0 0 0 3985 11 0 0 25 0 1 0 423709796 15302656 3157 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3736 3157 603 41 0 3695 0
vsize: 14944
[startup+50.002 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3428 0 0 0 4985 11 0 0 25 0 1 0 423709796 16105472 3350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3932 3350 603 41 0 3891 0
vsize: 15728
[startup+60.0036 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 5985 12 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223712 134561639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+70.0037 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 6984 12 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+80.0045 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 7984 12 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+90.0058 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 8984 12 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+100.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 9985 12 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+110.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 10985 12 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+120.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 11985 13 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+130.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 12985 13 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+140.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3657 0 0 0 13985 13 0 0 25 0 1 0 423709796 17043456 3579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4161 3579 603 41 0 4120 0
vsize: 16644
[startup+150.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3691 0 0 0 14985 13 0 0 25 0 1 0 423709796 17174528 3613 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4193 3613 603 41 0 4152 0
vsize: 16772
[startup+160.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3872 0 0 0 15985 14 0 0 25 0 1 0 423709796 17940480 3794 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4380 3794 603 41 0 4339 0
vsize: 17520
[startup+170.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3872 0 0 0 16985 14 0 0 25 0 1 0 423709796 17940480 3794 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4380 3794 603 41 0 4339 0
vsize: 17520
[startup+180.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 17985 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+190.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 18985 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+200.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 19985 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+210.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 20985 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+220.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 21986 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+230.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 22986 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223712 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+240.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 23986 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+250.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 24986 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+260.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 25986 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+270.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3873 0 0 0 26986 14 0 0 25 0 1 0 423709796 17936384 3795 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4379 3795 603 41 0 4338 0
vsize: 17516
[startup+280.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3900 0 0 0 27986 14 0 0 25 0 1 0 423709796 18067456 3822 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4411 3822 603 41 0 4370 0
vsize: 17644
[startup+290.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3916 0 0 0 28986 14 0 0 25 0 1 0 423709796 18067456 3838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4411 3838 603 41 0 4370 0
vsize: 17644
[startup+300.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 3916 0 0 0 29987 14 0 0 25 0 1 0 423709796 18067456 3838 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4411 3838 603 41 0 4370 0
vsize: 17644
[startup+310.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 4150 0 0 0 30986 15 0 0 25 0 1 0 423709796 18997248 4072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4638 4072 603 41 0 4597 0
vsize: 18552
[startup+320.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 4418 0 0 0 31986 16 0 0 25 0 1 0 423709796 20197376 4340 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4931 4340 603 41 0 4890 0
vsize: 19724
[startup+330.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 4894 0 0 0 32985 17 0 0 25 0 1 0 423709796 22196224 4816 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5419 4816 603 41 0 5378 0
vsize: 21676
[startup+340.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 5386 0 0 0 33984 18 0 0 25 0 1 0 423709796 24203264 5308 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5909 5308 603 41 0 5868 0
vsize: 23636
[startup+350.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 5386 0 0 0 34984 18 0 0 25 0 1 0 423709796 24203264 5308 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5909 5308 603 41 0 5868 0
vsize: 23636
[startup+360.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 5386 0 0 0 35985 18 0 0 25 0 1 0 423709796 24203264 5308 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5909 5308 603 41 0 5868 0
vsize: 23636
[startup+370.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 5386 0 0 0 36985 18 0 0 25 0 1 0 423709796 24203264 5308 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5909 5308 603 41 0 5868 0
vsize: 23636
[startup+380.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 5386 0 0 0 37985 18 0 0 25 0 1 0 423709796 24203264 5308 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5909 5308 603 41 0 5868 0
vsize: 23636
[startup+390.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 5504 0 0 0 38985 18 0 0 25 0 1 0 423709796 24735744 5426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6039 5426 603 41 0 5998 0
vsize: 24156
[startup+400.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6020 0 0 0 39984 19 0 0 25 0 1 0 423709796 26877952 5942 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6562 5942 603 41 0 6521 0
vsize: 26248
[startup+410.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6539 0 0 0 40982 21 0 0 25 0 1 0 423709796 28884992 6461 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7052 6461 603 41 0 7011 0
vsize: 28208
[startup+420.018 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6979 0 0 0 41981 23 0 0 25 0 1 0 423709796 30748672 6901 4294967295 134512640 134672761 3221224544 3221223456 134565829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7507 6901 603 41 0 7466 0
vsize: 30028
[startup+430.018 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6979 0 0 0 42981 23 0 0 25 0 1 0 423709796 30748672 6901 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7507 6901 603 41 0 7466 0
vsize: 30028
[startup+440.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6979 0 0 0 43981 23 0 0 25 0 1 0 423709796 30748672 6901 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7507 6901 603 41 0 7466 0
vsize: 30028
[startup+450.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6979 0 0 0 44982 23 0 0 25 0 1 0 423709796 30748672 6901 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7507 6901 603 41 0 7466 0
vsize: 30028
[startup+460.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6979 0 0 0 45982 23 0 0 25 0 1 0 423709796 30748672 6901 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7507 6901 603 41 0 7466 0
vsize: 30028
[startup+470.021 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6979 0 0 0 46982 23 0 0 25 0 1 0 423709796 30748672 6901 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7507 6901 603 41 0 7466 0
vsize: 30028
[startup+480.021 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 6979 0 0 0 47982 23 0 0 25 0 1 0 423709796 30748672 6901 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7507 6901 603 41 0 7466 0
vsize: 30028
[startup+490.022 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7334 0 0 0 48981 24 0 0 25 0 1 0 423709796 32223232 7256 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7867 7256 603 41 0 7826 0
vsize: 31468
[startup+500.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 49981 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+510.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 50981 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+520.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 51981 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+530.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 52981 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+540.024 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 53982 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+550.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 54982 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+560.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 55982 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+570.026 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 56982 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+580.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 57982 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+590.026 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 58983 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+600.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7459 0 0 0 59983 24 0 0 25 0 1 0 423709796 32628736 7381 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7381 603 41 0 7925 0
vsize: 31864
[startup+610.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7461 0 0 0 60983 24 0 0 25 0 1 0 423709796 32628736 7383 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7383 603 41 0 7925 0
vsize: 31864
[startup+620.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7464 0 0 0 61983 24 0 0 25 0 1 0 423709796 32628736 7386 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7386 603 41 0 7925 0
vsize: 31864
[startup+630.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7466 0 0 0 62983 24 0 0 25 0 1 0 423709796 32628736 7388 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7388 603 41 0 7925 0
vsize: 31864
[startup+640.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7468 0 0 0 63983 24 0 0 25 0 1 0 423709796 32628736 7390 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7390 603 41 0 7925 0
vsize: 31864
[startup+650.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7471 0 0 0 64984 24 0 0 25 0 1 0 423709796 32628736 7393 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7393 603 41 0 7925 0
vsize: 31864
[startup+660.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7473 0 0 0 65984 24 0 0 25 0 1 0 423709796 32628736 7395 4294967295 134512640 134672761 3221224544 3221223648 134559922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7966 7395 603 41 0 7925 0
vsize: 31864
[startup+670.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 7779 0 0 0 66984 25 0 0 25 0 1 0 423709796 33972224 7701 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8294 7701 603 41 0 8253 0
vsize: 33176
[startup+680.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 8342 0 0 0 67982 26 0 0 25 0 1 0 423709796 36261888 8264 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8853 8264 603 41 0 8812 0
vsize: 35412
[startup+690.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 8866 0 0 0 68981 28 0 0 25 0 1 0 423709796 38674432 8788 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9442 8788 603 41 0 9401 0
vsize: 37768
[startup+700.03 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 9401 0 0 0 69980 29 0 0 25 0 1 0 423709796 40804352 9323 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9962 9323 603 41 0 9921 0
vsize: 39848
[startup+710.031 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 9912 0 0 0 70978 32 0 0 25 0 1 0 423709796 42934272 9834 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10482 9834 603 41 0 10441 0
vsize: 41928
[startup+720.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 10413 0 0 0 71977 32 0 0 25 0 1 0 423709796 44937216 10335 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10971 10335 603 41 0 10930 0
vsize: 43884
[startup+730.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 10896 0 0 0 72975 34 0 0 25 0 1 0 423709796 46956544 10818 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11464 10818 603 41 0 11423 0
vsize: 45856
[startup+740.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 11387 0 0 0 73974 36 0 0 25 0 1 0 423709796 48951296 11309 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11951 11309 603 41 0 11910 0
vsize: 47804
[startup+750.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 11810 0 0 0 74973 37 0 0 25 0 1 0 423709796 50683904 11732 4294967295 134512640 134672761 3221224544 3221223648 134555076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12374 11732 603 41 0 12333 0
vsize: 49496
[startup+760.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 11997 0 0 0 75972 38 0 0 25 0 1 0 423709796 51359744 11919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12539 11919 603 41 0 12498 0
vsize: 50156
[startup+770.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 76972 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+780.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 77972 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+790.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 78972 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+800.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 79973 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+810.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 80973 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+820.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 81973 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+830.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 82973 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+840.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 83973 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+850.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 84973 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+860.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 85973 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+870.035 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 86974 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+880.035 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 87974 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+890.035 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 88974 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+900.036 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 89974 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+910.035 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 90974 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+920.037 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 91974 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+930.036 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 92975 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+940.036 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 93975 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+950.037 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 94975 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+960.037 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 95975 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+970.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 96975 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+980.037 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 97975 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+990.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 98975 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1000.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 99976 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1010.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 100976 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1020.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 101976 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1030.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 102976 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1040.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 103976 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1050.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 104977 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1060.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 105977 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1070.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 106977 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1080.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12118 0 0 0 107977 38 0 0 25 0 1 0 423709796 51896320 12040 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12040 603 41 0 12629 0
vsize: 50680
[startup+1090.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12392 0 0 0 108977 39 0 0 25 0 1 0 423709796 52961280 12314 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12930 12314 603 41 0 12889 0
vsize: 51720
[startup+1100.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12667 0 0 0 109976 40 0 0 25 0 1 0 423709796 54161408 12589 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13223 12589 603 41 0 13182 0
vsize: 52892
[startup+1110.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 12969 0 0 0 110975 41 0 0 25 0 1 0 423709796 55373824 12891 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13519 12891 603 41 0 13478 0
vsize: 54076
[startup+1120.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 13258 0 0 0 111975 42 0 0 25 0 1 0 423709796 56590336 13180 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13816 13180 603 41 0 13775 0
vsize: 55264
[startup+1130.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 13605 0 0 0 112974 43 0 0 25 0 1 0 423709796 57933824 13527 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14144 13527 603 41 0 14103 0
vsize: 56576
[startup+1140.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 13952 0 0 0 113973 44 0 0 25 0 1 0 423709796 59396096 13874 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14501 13874 603 41 0 14460 0
vsize: 58004
[startup+1150.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 14344 0 0 0 114972 45 0 0 25 0 1 0 423709796 61014016 14266 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14896 14266 603 41 0 14855 0
vsize: 59584
[startup+1160.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 14772 0 0 0 115971 46 0 0 25 0 1 0 423709796 62738432 14694 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15317 14694 603 41 0 15276 0
vsize: 61268
[startup+1170.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 15164 0 0 0 116971 47 0 0 25 0 1 0 423709796 64331776 15086 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15706 15086 603 41 0 15665 0
vsize: 62824
[startup+1180.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 15567 0 0 0 117970 48 0 0 25 0 1 0 423709796 65933312 15489 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16097 15489 603 41 0 16056 0
vsize: 64388
[startup+1190.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 15998 0 0 0 118968 50 0 0 25 0 1 0 423709796 67801088 15920 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16553 15920 603 41 0 16512 0
vsize: 66212
[startup+1200.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 13671
Raw data (stat): 13669 (minisat+) R 13668 5897 5896 0 -1 0 16419 0 0 0 119968 50 0 0 25 0 1 0 423709796 69398528 16341 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16943 16341 603 41 0 16902 0
vsize: 67772
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 1.00 0.94 1/54 13671
Raw data (stat): 13669 (minisat+) Z 13668 5897 5896 0 -1 12 16422 0 0 0 119968 53 0 0 25 0 1 0 423709796 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.08
CPU time (s): 1200.22
CPU user time (s): 1199.69
CPU system time (s): 0.537918
CPU usage (%): 100.012
Max. virtual memory (Kb): 67772
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####