PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 32488

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-05-27 10:19:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23873 boxname=wulflinc30 idbench=1517 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f5f6e30a602f3968daa9ca41c7da043  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-neos5.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-neos5.opb
IDLAUNCH: 23873
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        896044 kB
Buffers:          5624 kB
Cached:         113744 kB
SwapCached:        720 kB
Active:          17232 kB
Inactive:       104276 kB
HighTotal:      131008 kB
HighFree:        13748 kB
LowTotal:       903652 kB
LowFree:        882296 kB
SwapTotal:     2097892 kB
SwapFree:      2096304 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5036 kB
Slab:            11536 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 10:39:34 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 23873 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    7
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    7
c ---[  63]---> BDD-cost:    7
c ---[  62]---> BDD-cost:  199
c ---[  61]---> BDD-cost:  309
c ---[  60]---> BDD-cost:  147
c ---[  59]---> BDD-cost:  579
c ---[  58]---> BDD-cost:  378
c ---[  57]---> BDD-cost:  147
c ---[  56]---> BDD-cost:  473
c ---[  55]---> BDD-cost:  378
c ---[  54]---> BDD-cost:  378
c ---[  53]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  473
c ---[  51]---> BDD-cost:  100
c ---[  50]---> BDD-cost:  378
c ---[  49]---> BDD-cost:  471
c ---[  48]---> BDD-cost:  223
c ---[  47]---> BDD-cost:  174
c ---[  46]---> BDD-cost:  177
c ---[  45]---> BDD-cost:  129
c ---[  44]---> BDD-cost:  176
c ---[  43]---> BDD-cost:  177
c ---[  42]---> BDD-cost:  129
c ---[  41]---> BDD-cost:  176
c ---[  40]---> BDD-cost:  171
c ---[  39]---> BDD-cost:  129
c ---[  38]---> BDD-cost:  446
c ---[  37]---> BDD-cost:  176
c ---[  36]---> BDD-cost:  177
c ---[  35]---> BDD-cost:  129
c ---[  34]---> BDD-cost:  176
c ---[  33]---> BDD-cost:  129
c ---[  32]---> BDD-cost:  446
c ---[  31]---> BDD-cost:  177
c ---[  30]---> BDD-cost:  129
c ---[  29]---> BDD-cost:  173
c ---[  28]---> BDD-cost:  354
c ---[  27]---> BDD-cost:  446
c ---[  26]---> BDD-cost:  110
c ---[  25]---> BDD-cost:  110
c ---[  24]---> BDD-cost:  110
c ---[  23]---> BDD-cost:  150
c ---[  22]---> BDD-cost:  110
c ---[  21]---> BDD-cost:  110
c ---[  20]---> BDD-cost:  110
c ---[  19]---> BDD-cost:  150
c ---[  18]---> BDD-cost:  175
c ---[  17]---> BDD-cost:  110
c ---[  16]---> BDD-cost:  110
c ---[  15]---> BDD-cost:  150
c ---[  14]---> BDD-cost:  110
c ---[  13]---> BDD-cost:  150
c ---[  12]---> BDD-cost:  110
c ---[  11]---> BDD-cost:  328
c ---[  10]---> BDD-cost:   90
c ---[   9]---> BDD-cost:   90
c ---[   8]---> BDD-cost:   90
c ---[   7]---> BDD-cost:  175
c ---[   6]---> BDD-cost:   90
c ---[   5]---> BDD-cost:  122
c ---[   4]---> BDD-cost:   90
c ---[   3]---> BDD-cost:   69
c ---[   2]---> BDD-cost:  181
c ---[   1]---> BDD-cost:  193
c ---[   0]---> BDD-cost:  147
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   33911   100622 |   11303       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3713[0m
c ---[   0]---> Sorter-cost: 2729     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38898   112283 |   12966       0        0     nan |  0.000 % |
c |       100 |   38898   112283 |   14262     100      915     9.2 |  0.492 % |
c ==============================================================================
c [1mFound solution: 2710[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       216 |   38991   112524 |   12997     216     1659     7.7 |  0.492 % |
c |       317 |   38991   112524 |   14296     317     2305     7.3 |  0.497 % |
c ==============================================================================
c [1mFound solution: 2578[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       431 |   39004   112564 |   13001     431     3130     7.3 |  0.497 % |
c |       531 |   39004   112564 |   14301     531     4162     7.8 |  0.503 % |
c ==============================================================================
c [1mFound solution: 2558[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       674 |   39012   112582 |   13004     674     5947     8.8 |  0.503 % |
c |       774 |   39012   112582 |   14304     774     7065     9.1 |  0.510 % |
c |       924 |   39012   112582 |   15734     924     8684     9.4 |  0.510 % |
c |      1149 |   39012   112582 |   17308    1149    11311     9.8 |  0.510 % |
c |      1487 |   39012   112582 |   19039    1487    16005    10.8 |  0.510 % |
c |      1993 |   39012   112582 |   20943    1993    22485    11.3 |  0.510 % |
c |      2754 |   39012   112582 |   23037    2754    32826    11.9 |  0.510 % |
c ==============================================================================
c [1mFound solution: 2534[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3128 |   39033   112638 |   13011    3128    38552    12.3 |  0.510 % |
c |      3229 |   39033   112638 |   14312    3229    39501    12.2 |  0.516 % |
c |      3379 |   39033   112638 |   15743    3379    40724    12.1 |  0.516 % |
c |      3605 |   39033   112638 |   17317    3605    46529    12.9 |  0.516 % |
c |      3942 |   39033   112638 |   19049    3942    51933    13.2 |  0.516 % |
c |      4449 |   39033   112638 |   20954    4449    58341    13.1 |  0.516 % |
c ==============================================================================
c [1mFound solution: 2277[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4742 |   39062   112717 |   13020    4742    62046    13.1 |  0.516 % |
c |      4842 |   39062   112717 |   14322    4842    63099    13.0 |  0.522 % |
c |      4993 |   39062   112717 |   15754    4993    64889    13.0 |  0.522 % |
c |      5221 |   39062   112717 |   17329    5221    67757    13.0 |  0.522 % |
c |      5560 |   39062   112717 |   19062    5560    71459    12.9 |  0.522 % |
c |      6067 |   39062   112717 |   20968    6067    80605    13.3 |  0.522 % |
c ==============================================================================
c [1mFound solution: 2226[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6796 |   39070   112741 |   13023    6796    88271    13.0 |  0.522 % |
c |      6898 |   39070   112741 |   14325    6898    90654    13.1 |  0.528 % |
c |      7048 |   39070   112741 |   15757    7048    92973    13.2 |  0.528 % |
c |      7273 |   39070   112741 |   17333    7273    95774    13.2 |  0.528 % |
c |      7611 |   39070   112741 |   19066    7611   101834    13.4 |  0.528 % |
c |      8118 |   39070   112741 |   20973    8118   111260    13.7 |  0.528 % |
c |      8877 |   39070   112741 |   23071    8877   127946    14.4 |  0.528 % |
c |     10016 |   39070   112741 |   25378   10016   153990    15.4 |  0.528 % |
c ==============================================================================
c [1mFound solution: 2214[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10839 |   39075   112753 |   13025   10839   168906    15.6 |  0.528 % |
c |     10940 |   39075   112753 |   14327   10940   172014    15.7 |  0.535 % |
c |     11090 |   39075   112753 |   15760   11090   176255    15.9 |  0.535 % |
c |     11315 |   39075   112753 |   17336   11315   180028    15.9 |  0.535 % |
c |     11653 |   39075   112753 |   19069   11653   185458    15.9 |  0.535 % |
c |     12160 |   39075   112753 |   20976   12160   201326    16.6 |  0.535 % |
c |     12920 |   39075   112753 |   23074   12920   219136    17.0 |  0.535 % |
c |     14059 |   39075   112753 |   25382   14059   250319    17.8 |  0.535 % |
c |     15769 |   39075   112753 |   27920   15769   295387    18.7 |  0.535 % |
c |     18331 |   39075   112753 |   30712   18331   382998    20.9 |  0.535 % |
c ==============================================================================
c [1mFound solution: 2198[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18608 |   39081   112766 |   13027   18608   389598    20.9 |  0.535 % |
c |     18708 |   39081   112766 |   14329    9404   219670    23.4 |  0.541 % |
c |     18859 |   39081   112766 |   15762    9555   222889    23.3 |  0.541 % |
c |     19085 |   39081   112766 |   17338    9781   228854    23.4 |  0.541 % |
c |     19423 |   39081   112766 |   19072   10119   239796    23.7 |  0.541 % |
c |     19929 |   39081   112766 |   20980   10625   256430    24.1 |  0.541 % |
c |     20689 |   39081   112766 |   23078   11385   273717    24.0 |  0.541 % |
c |     21828 |   39081   112766 |   25385   12524   308011    24.6 |  0.541 % |
c |     23536 |   39081   112766 |   27924   14232   329831    23.2 |  0.541 % |
c |     26098 |   39081   112766 |   30716   16794   446902    26.6 |  0.541 % |
c |     29944 |   39081   112766 |   33788   20640   593395    28.7 |  0.541 % |
c ==============================================================================
c [1mFound solution: 2197[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33488 |   39084   112773 |   13028   24153   662202    27.4 |  0.541 % |
c |     33588 |   39084   112773 |   14330   12177   326973    26.9 |  0.561 % |
c |     33738 |   39084   112773 |   15763   12327   328428    26.6 |  0.561 % |
c |     33964 |   39084   112773 |   17340   12553   331968    26.4 |  0.561 % |
c |     34302 |   39084   112773 |   19074   12891   338602    26.3 |  0.561 % |
c ==============================================================================
c [1mFound solution: 2194[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34788 |   39090   112786 |   13030   13377   355016    26.5 |  0.561 % |
c |     34889 |   39090   112786 |   14333    6790   105552    15.5 |  0.567 % |
c |     35039 |   39090   112786 |   15766    6940   109010    15.7 |  0.567 % |
c |     35264 |   39090   112786 |   17342    7165   112498    15.7 |  0.567 % |
c |     35602 |   39090   112786 |   19077    7503   123086    16.4 |  0.567 % |
c |     36109 |   39090   112786 |   20984    8010   133240    16.6 |  0.567 % |
c |     36868 |   39090   112786 |   23083    8769   151960    17.3 |  0.567 % |
c |     38007 |   39090   112786 |   25391    9908   173908    17.6 |  0.567 % |
c ==============================================================================
c [1mFound solution: 2182[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39387 |   39095   112797 |   13031   11288   199430    17.7 |  0.567 % |
c |     39488 |   39095   112797 |   14334   11389   201112    17.7 |  0.574 % |
c |     39638 |   39095   112797 |   15767   11539   203455    17.6 |  0.574 % |
c |     39863 |   39095   112797 |   17344   11764   206157    17.5 |  0.574 % |
c |     40200 |   39095   112797 |   19078   12101   213060    17.6 |  0.574 % |
c |     40707 |   39095   112797 |   20986   12608   221599    17.6 |  0.574 % |
c ==============================================================================
c [1mFound solution: 2181[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41064 |   39100   112808 |   13033   12965   225861    17.4 |  0.574 % |
c |     41164 |   39100   112808 |   14336   13065   228032    17.5 |  0.580 % |
c |     41315 |   39100   112808 |   15769   13216   229867    17.4 |  0.580 % |
c |     41540 |   39100   112808 |   17346   13441   232162    17.3 |  0.580 % |
c |     41879 |   39100   112808 |   19081   13780   239794    17.4 |  0.580 % |
c |     42385 |   39100   112808 |   20989   14286   250802    17.6 |  0.580 % |
c ==============================================================================
c [1mFound solution: 2180[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42464 |   39110   112835 |   13036   14365   251613    17.5 |  0.580 % |
c |     42564 |   39110   112835 |   14339    7283    94911    13.0 |  0.587 % |
c |     42714 |   39110   112835 |   15773    7433    97580    13.1 |  0.587 % |
c ==============================================================================
c [1mFound solution: 2179[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42773 |   39117   112851 |   13039    7492    98398    13.1 |  0.587 % |
c |     42873 |   39117   112851 |   14342    7592   100096    13.2 |  0.593 % |
c |     43023 |   39117   112851 |   15777    7742   103512    13.4 |  0.593 % |
c |     43249 |   39117   112851 |   17354    7968   106173    13.3 |  0.593 % |
c |     43587 |   39117   112851 |   19090    8306   111505    13.4 |  0.593 % |
c |     44093 |   39117   112851 |   20999    8812   127245    14.4 |  0.593 % |
c |     44852 |   39117   112851 |   23099    9571   140492    14.7 |  0.593 % |
c ==============================================================================
c [1mFound solution: 2178[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45190 |   39124   112867 |   13041    9909   145231    14.7 |  0.593 % |
c |     45290 |   39124   112867 |   14345   10009   146867    14.7 |  0.600 % |
c |     45441 |   39124   112867 |   15779   10160   150101    14.8 |  0.600 % |
c |     45666 |   39124   112867 |   17357   10385   153677    14.8 |  0.600 % |
c |     46004 |   39124   112867 |   19093   10723   160889    15.0 |  0.600 % |
c |     46510 |   39124   112867 |   21002   11229   172904    15.4 |  0.600 % |
c |     47270 |   39124   112867 |   23102   11989   194129    16.2 |  0.600 % |
c |     48409 |   39124   112867 |   25413   13128   230083    17.5 |  0.600 % |
c |     50117 |   39124   112867 |   27954   14836   265720    17.9 |  0.600 % |
c ==============================================================================
c [1mFound solution: 2118[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51555 |   39133   112892 |   13044   16274   329483    20.2 |  0.600 % |
c |     51656 |   39133   112892 |   14348    8238   177098    21.5 |  0.606 % |
c |     51806 |   39133   112892 |   15783    8388   180206    21.5 |  0.606 % |
c |     52032 |   39133   112892 |   17361    8614   184942    21.5 |  0.606 % |
c |     52370 |   39133   112892 |   19097    8952   190096    21.2 |  0.606 % |
c |     52876 |   39133   112892 |   21007    9458   198770    21.0 |  0.606 % |
c |     53635 |   39133   112892 |   23108   10217   223410    21.9 |  0.606 % |
c |     54774 |   39133   112892 |   25419   11356   239738    21.1 |  0.606 % |
c |     56483 |   39133   112892 |   27960   13065   277316    21.2 |  0.606 % |
c |     59045 |   39133   112892 |   30757   15627   356100    22.8 |  0.606 % |
c |     62891 |   39133   112892 |   33832   19473   448248    23.0 |  0.606 % |
c ==============================================================================
c [1mFound solution: 2113[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63186 |   39140   112908 |   13046   19768   453358    22.9 |  0.606 % |
c |     63286 |   39140   112908 |   14350    9984   197679    19.8 |  0.613 % |
c |     63436 |   39140   112908 |   15785   10134   201781    19.9 |  0.613 % |
c |     63661 |   39140   112908 |   17364   10359   205325    19.8 |  0.613 % |
c |     63998 |   39140   112908 |   19100   10696   210724    19.7 |  0.613 % |
c |     64507 |   39140   112908 |   21010   11205   228279    20.4 |  0.613 % |
c |     65266 |   39140   112908 |   23111   11964   241822    20.2 |  0.613 % |
c |     66410 |   39140   112908 |   25422   13108   269151    20.5 |  0.613 % |
c |     68119 |   39140   112908 |   27965   14817   326657    22.0 |  0.613 % |
c |     70681 |   39140   112908 |   30761   17379   373421    21.5 |  0.613 % |
c |     74525 |   39140   112908 |   33837   21223   458843    21.6 |  0.613 % |
c |     80292 |   39140   112908 |   37221   26990   707568    26.2 |  0.613 % |
c |     88941 |   39140   112908 |   40943   35639  1070103    30.0 |  0.613 % |
c ==============================================================================
c [1mFound solution: 2108[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91101 |   39149   112929 |   13049   37799  1190486    31.5 |  0.613 % |
c |     91201 |   39149   112929 |   14353    7733   232503    30.1 |  0.619 % |
c |     91351 |   39147   112925 |   15789    7881   233984    29.7 |  0.626 % |
c |     91576 |   39147   112925 |   17368    8106   237486    29.3 |  0.626 % |
c |     91913 |   39147   112925 |   19105    8443   244004    28.9 |  0.626 % |
c |     92421 |   39147   112925 |   21015    8951   252559    28.2 |  0.626 % |
c |     93180 |   39147   112925 |   23117    9710   265335    27.3 |  0.626 % |
c |     94321 |   39147   112925 |   25428   10851   286293    26.4 |  0.626 % |
c |     96031 |   39147   112925 |   27971   12561   324430    25.8 |  0.626 % |
c |     98595 |   39147   112925 |   30768   15125   381915    25.3 |  0.626 % |
c ==============================================================================
c [1mFound solution: 2086[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99390 |   39152   112936 |   13050   15920   392230    24.6 |  0.626 % |
c |     99490 |   39152   112936 |   14355    8060   123820    15.4 |  0.632 % |
c |     99641 |   39152   112936 |   15790    8211   126017    15.3 |  0.632 % |
c |     99866 |   39152   112936 |   17369    8436   128818    15.3 |  0.632 % |
c |    100203 |   39152   112936 |   19106    8773   135875    15.5 |  0.632 % |
c |    100710 |   39152   112936 |   21017    9280   144258    15.5 |  0.632 % |
c |    101469 |   39152   112936 |   23118   10039   157672    15.7 |  0.632 % |
c |    102609 |   39152   112936 |   25430   11179   178631    16.0 |  0.632 % |
c ==============================================================================
c [1mFound solution: 2084[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104126 |   39159   112952 |   13053   12696   214227    16.9 |  0.632 % |
c |    104226 |   39159   112952 |   14358   12796   218101    17.0 |  0.638 % |
c |    104379 |   39159   112952 |   15794   12949   221494    17.1 |  0.638 % |
c |    104604 |   39159   112952 |   17373   13174   225818    17.1 |  0.638 % |
c |    104942 |   39159   112952 |   19110   13512   230644    17.1 |  0.638 % |
c |    105448 |   39159   112952 |   21021   14018   237233    16.9 |  0.638 % |
c |    106207 |   39159   112952 |   23124   14777   251872    17.0 |  0.638 % |
c |    107346 |   39159   112952 |   25436   15916   284816    17.9 |  0.638 % |
c ==============================================================================
c [1mFound solution: 2054[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108040 |   39164   112963 |   13054   16610   296982    17.9 |  0.638 % |
c |    108140 |   39164   112963 |   14359    8405   125008    14.9 |  0.645 % |
c |    108291 |   39164   112963 |   15795    8556   128637    15.0 |  0.645 % |
c |    108516 |   39164   112963 |   17374    8781   134950    15.4 |  0.645 % |
c |    108855 |   39164   112963 |   19112    9120   141445    15.5 |  0.645 % |
c |    109363 |   39164   112963 |   21023    9628   154186    16.0 |  0.645 % |
c |    110122 |   39164   112963 |   23125   10387   168963    16.3 |  0.645 % |
c |    111261 |   39164   112963 |   25438   11526   199481    17.3 |  0.645 % |
c ==============================================================================
c [1mFound solution: 2053[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112223 |   39170   112976 |   13056   12488   218124    17.5 |  0.645 % |
c |    112323 |   39170   112976 |   14361   12588   220064    17.5 |  0.651 % |
c |    112473 |   39170   112976 |   15797   12738   222376    17.5 |  0.651 % |
c ==============================================================================
c [1mFound solution: 2052[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112587 |   39176   112989 |   13058   12852   224961    17.5 |  0.651 % |
c |    112688 |   39176   112989 |   14363   12953   227121    17.5 |  0.658 % |
c |    112838 |   39176   112989 |   15800   13103   231056    17.6 |  0.658 % |
c |    113063 |   39176   112989 |   17380   13328   236720    17.8 |  0.658 % |
c |    113401 |   39176   112989 |   19118   13666   242970    17.8 |  0.658 % |
c |    113908 |   39176   112989 |   21030   14173   248818    17.6 |  0.658 % |
c |    114668 |   39176   112989 |   23133   14933   259678    17.4 |  0.658 % |
c ==============================================================================
c [1mFound solution: 2051[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115732 |   39183   113004 |   13061   15997   300594    18.8 |  0.658 % |
c |    115832 |   39183   113004 |   14367    8099   119026    14.7 |  0.664 % |
c |    115982 |   39183   113004 |   15803    8249   121516    14.7 |  0.664 % |
c |    116208 |   39183   113004 |   17384    8475   125658    14.8 |  0.664 % |
c |    116545 |   39183   113004 |   19122    8812   134437    15.3 |  0.664 % |
c |    117051 |   39183   113004 |   21034    9318   144441    15.5 |  0.664 % |
c |    117810 |   39183   113004 |   23138   10077   158441    15.7 |  0.664 % |
c |    118949 |   39183   113004 |   25452   11216   177286    15.8 |  0.664 % |
c |    120657 |   39183   113004 |   27997   12924   222332    17.2 |  0.664 % |
c ==============================================================================
c [1mFound solution: 2050[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122005 |   39190   113019 |   13063   14272   264416    18.5 |  0.664 % |
c |    122105 |   39190   113019 |   14369    7236   118286    16.3 |  0.671 % |
c |    122255 |   39190   113019 |   15806    7386   120790    16.4 |  0.671 % |
c |    122480 |   39190   113019 |   17386    7611   124288    16.3 |  0.671 % |
c |    122818 |   39190   113019 |   19125    7949   127889    16.1 |  0.671 % |
c |    123325 |   39190   113019 |   21038    8456   136221    16.1 |  0.671 % |
c |    124086 |   39190   113019 |   23141    9217   163643    17.8 |  0.671 % |
c |    125225 |   39190   113019 |   25456   10356   191362    18.5 |  0.671 % |
c |    126933 |   39190   113019 |   28001   12064   237174    19.7 |  0.671 % |
c |    129495 |   39187   113012 |   30801   14509   347040    23.9 |  0.684 % |
c |    133343 |   39187   113012 |   33882   18357   531606    29.0 |  0.684 % |
c |    139109 |   39187   113012 |   37270   24123   755871    31.3 |  0.684 % |
c ==============================================================================
c [1mFound solution: 2049[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    144688 |   39192   113023 |   13064   29702   944308    31.8 |  0.684 % |
c |    144788 |   39192   113023 |   14370    7526   155241    20.6 |  0.690 % |
c |    144940 |   39192   113023 |   15807    7678   157505    20.5 |  0.690 % |
c |    145165 |   39192   113023 |   17388    7903   162421    20.6 |  0.690 % |
c |    145503 |   39192   113023 |   19127    8241   168934    20.5 |  0.690 % |
c |    146013 |   39192   113023 |   21039    8751   179552    20.5 |  0.690 % |
c |    146774 |   39192   113023 |   23143    9512   190278    20.0 |  0.690 % |
c |    147913 |   39190   113019 |   25458   10650   219684    20.6 |  0.697 % |
c |    149622 |   39190   113019 |   28003   12359   257758    20.9 |  0.697 % |
c |    152184 |   39190   113019 |   30804   14921   332505    22.3 |  0.697 % |
c |    156030 |   39190   113019 |   33884   18767   416429    22.2 |  0.697 % |
c |    161797 |   39190   113019 |   37273   24534   516462    21.1 |  0.697 % |
c ==============================================================================
c [1mFound solution: 2048[0m
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    164737 |   39199   113039 |   13066   27474   601402    21.9 |  0.697 % |
c |    164837 |   39199   113039 |   14372    6969   110704    15.9 |  0.703 % |
c |    164989 |   39199   113039 |   15809    7121   112243    15.8 |  0.703 % |
c |    165214 |   39199   113039 |   17390    7346   116712    15.9 |  0.703 % |
c |    165551 |   39199   113039 |   19129    7683   124270    16.2 |  0.703 % |
c |    166058 |   39199   113039 |   21042    8190   131152    16.0 |  0.703 % |
c |    166817 |   39199   113039 |   23147    8949   146515    16.4 |  0.703 % |
c |    167956 |   39199   113039 |   25461   10088   173923    17.2 |  0.703 % |
c |    169665 |   39199   113039 |   28008   11797   221617    18.8 |  0.703 % |
c |    172227 |   39199   113039 |   30808   14359   304218    21.2 |  0.703 % |
c |    176071 |   39199   113039 |   33889   18203   409817    22.5 |  0.703 % |
c |    181838 |   39199   113039 |   37278   23970   535018    22.3 |  0.703 % |
c |    190487 |   39199   113039 |   41006   32619   809512    24.8 |  0.703 % |
c |    203461 |   39199   113039 |   45107   19849   514697    25.9 |  0.703 % |
c ==============================================================================
c [1mFound solution: 2022[0m
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    219104 |   39215   113080 |   13071   35492  1638422    46.2 |  0.703 % |
c |    219206 |   39215   113080 |   14378    7685   342507    44.6 |  0.709 % |
c |    219356 |   39215   113080 |   15815    7835   345471    44.1 |  0.709 % |
c |    219584 |   39215   113080 |   17397    8063   348088    43.2 |  0.709 % |
c |    219922 |   39215   113080 |   19137    8401   357441    42.5 |  0.709 % |
c |    220428 |   39215   113080 |   21050    8907   366831    41.2 |  0.709 % |
c |    221187 |   39215   113080 |   23156    9666   380360    39.4 |  0.709 % |
c |    222326 |   39215   113080 |   25471   10805   400433    37.1 |  0.709 % |
c |    224035 |   39215   113080 |   28018   12514   458854    36.7 |  0.709 % |
c |    226597 |   39215   113080 |   30820   15076   511688    33.9 |  0.709 % |
c |    230442 |   39215   113080 |   33902   18921   595632    31.5 |  0.709 % |
c |    236208 |   39215   113080 |   37293   24687   716653    29.0 |  0.709 % |
c |    244857 |   39215   113080 |   41022   33336   956691    28.7 |  0.709 % |
c |    257832 |   39215   113080 |   45124   19491   624862    32.1 |  0.709 % |
c |    277293 |   39215   113080 |   49637   38952  1587769    40.8 |  0.709 % |
c |    306485 |   39215   113080 |   54600   32539   847118    26.0 |  0.709 % |
c ==============================================================================
c [1mFound solution: 2020[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    345044 |   39220   113096 |   13073   30496  1280501    42.0 |  0.709 % |
c |    345144 |   39220   113096 |   14380    7724   164218    21.3 |  0.716 % |
c |    345295 |   39220   113096 |   15818    7875   166112    21.1 |  0.716 % |
c |    345520 |   39220   113096 |   17400    8100   170123    21.0 |  0.716 % |
c |    345859 |   39220   113096 |   19140    8439   174731    20.7 |  0.716 % |
c |    346366 |   39220   113096 |   21054    8946   182386    20.4 |  0.716 % |
c |    347130 |   39215   113085 |   23159    9698   199767    20.6 |  0.735 % |
c |    348273 |   39215   113085 |   25475   10841   221330    20.4 |  0.735 % |
c |    349981 |   39215   113085 |   28023   12549   255128    20.3 |  0.735 % |
c |    352545 |   39215   113085 |   30825   15113   305897    20.2 |  0.735 % |
c |    356389 |   39215   113085 |   33907   18957   380955    20.1 |  0.735 % |
c |    362155 |   39215   113085 |   37298   24723   543954    22.0 |  0.735 % |
c |    370804 |   39215   113085 |   41028   33372   690051    20.7 |  0.735 % |
c |    383778 |   39215   113085 |   45131   20751   703195    33.9 |  0.735 % |
c |    403239 |   39215   113085 |   49644   40212  1938012    48.2 |  0.735 % |
c ==============================================================================
c [1mFound solution: 2019[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    413668 |   39221   113100 |   13073   18494   529233    28.6 |  0.735 % |
c |    413768 |   39221   113100 |   14380    9347   209360    22.4 |  0.742 % |
c |    413919 |   39221   113100 |   15818    9498   211857    22.3 |  0.742 % |
c |    414144 |   39221   113100 |   17400    9723   215991    22.2 |  0.742 % |
c |    414481 |   39221   113100 |   19140   10060   221556    22.0 |  0.742 % |
c |    414987 |   39221   113100 |   21054   10566   230833    21.8 |  0.742 % |
c |    415747 |   39221   113100 |   23159   11326   248579    21.9 |  0.742 % |
c |    416886 |   39221   113100 |   25475   12465   268279    21.5 |  0.742 % |
c |    418596 |   39221   113100 |   28023   14175   303062    21.4 |  0.742 % |
c |    421160 |   39221   113100 |   30825   16739   374019    22.3 |  0.742 % |
c |    425005 |   39221   113100 |   33907   20584   457277    22.2 |  0.742 % |
c |    430772 |   39221   113100 |   37298   26351   554524    21.0 |  0.742 % |
c |    439421 |   39221   113100 |   41028   35000  1026168    29.3 |  0.742 % |
c |    452396 |   39221   113100 |   45131   22551   990398    43.9 |  0.742 % |
c |    471857 |   39221   113100 |   49644   42012  2141032    51.0 |  0.742 % |
c |    501049 |   39221   113100 |   54609   35709  1166547    32.7 |  0.742 % |
c ==============================================================================
c [1mFound solution: 2018[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    516644 |   39227   113115 |   13075   51304  2106940    41.1 |  0.742 % |
c |    516744 |   39227   113115 |   14382    8377   255250    30.5 |  0.748 % |
c |    516895 |   39227   113115 |   15820    8528   258995    30.4 |  0.748 % |
c |    517124 |   39227   113115 |   17402    8757   265447    30.3 |  0.748 % |
c |    517461 |   39227   113115 |   19143    9094   272822    30.0 |  0.748 % |
c |    517969 |   39227   113115 |   21057    9602   284892    29.7 |  0.748 % |
c |    518729 |   39227   113115 |   23163   10362   299097    28.9 |  0.748 % |
c |    519869 |   39227   113115 |   25479   11502   336446    29.3 |  0.748 % |
c |    521578 |   39227   113115 |   28027   13211   387412    29.3 |  0.748 % |
c |    524141 |   39227   113115 |   30830   15774   452571    28.7 |  0.748 % |
c |    527987 |   39227   113115 |   33913   19620   556397    28.4 |  0.748 % |
c |    533753 |   39227   113115 |   37304   25386   762984    30.1 |  0.748 % |
c |    542402 |   39227   113115 |   41034   34035  1081862    31.8 |  0.748 % |
c ==============================================================================
c [1mFound solution: 2017[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    549661 |   39233   113130 |   13077   41294  1270505    30.8 |  0.748 % |
c |    549761 |   39233   113130 |   14384    8570   124264    14.5 |  0.754 % |
c |    549911 |   39233   113130 |   15823    8720   126840    14.5 |  0.754 % |
c |    550136 |   39233   113130 |   17405    8945   130346    14.6 |  0.754 % |
c |    550473 |   39233   113130 |   19146    9282   136791    14.7 |  0.754 % |
c |    550983 |   39233   113130 |   21060    9792   150415    15.4 |  0.754 % |
c |    551742 |   39233   113130 |   23166   10551   166685    15.8 |  0.754 % |
c |    552881 |   39233   113130 |   25483   11690   182816    15.6 |  0.754 % |
c |    554591 |   39233   113130 |   28031   13400   227750    17.0 |  0.754 % |
c |    557154 |   39233   113130 |   30834   15963   292954    18.4 |  0.754 % |
c |    560998 |   39233   113130 |   33918   19807   385678    19.5 |  0.754 % |
c |    566766 |   39233   113130 |   37310   25575   528204    20.7 |  0.754 % |
c |    575415 |   39233   113130 |   41041   34224   909593    26.6 |  0.754 % |
c |    588389 |   39233   113130 |   45145   18961   528667    27.9 |  0.754 % |
c |    607851 |   39233   113130 |   49659   38423  1022299    26.6 |  0.755 % |
c |    637044 |   39233   113130 |   54625   34500  1479658    42.9 |  0.754 % |
c |    680833 |   39233   113130 |   60088   38207  1141570    29.9 |  0.755 % |
c ==============================================================================
c [1mFound solution: 2016[0m
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    712040 |   39239   113145 |   13079   23500   914500    38.9 |  0.755 % |
c |    712140 |   39239   113145 |   14386   11850   577102    48.7 |  0.761 % |
c |    712290 |   39239   113145 |   15825   12000   579032    48.3 |  0.761 % |
c |    712516 |   39239   113145 |   17408   12226   583747    47.7 |  0.761 % |
c |    712854 |   39239   113145 |   19148   12564   589558    46.9 |  0.761 % |
c |    713360 |   39239   113145 |   21063   13070   605699    46.3 |  0.761 % |
c |    714120 |   39239   113145 |   23170   13830   625085    45.2 |  0.761 % |
c |    715259 |   39239   113145 |   25487   14969   655852    43.8 |  0.761 % |
c |    716967 |   39239   113145 |   28035   16677   708245    42.5 |  0.761 % |
c |    719531 |   39239   113145 |   30839   19241   786345    40.9 |  0.761 % |
c |    723375 |   39239   113145 |   33923   23085   932446    40.4 |  0.761 % |
c |    729141 |   39239   113145 |   37315   28851  1125574    39.0 |  0.761 % |
c ==============================================================================
c [1mFound solution: 2006[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    736188 |   39245   113159 |   13081   35898  1371377    38.2 |  0.761 % |
c |    736288 |   39245   113159 |   14389    8356   107806    12.9 |  0.767 % |
c |    736438 |   39245   113159 |   15828    8506   110493    13.0 |  0.767 % |
c |    736664 |   39245   113159 |   17410    8732   114630    13.1 |  0.767 % |
c |    737003 |   39245   113159 |   19151    9071   119717    13.2 |  0.767 % |
c |    737510 |   39245   113159 |   21067    9578   129395    13.5 |  0.767 % |
c |    738269 |   39245   113159 |   23173   10337   151025    14.6 |  0.767 % |
c |    739408 |   39245   113159 |   25491   11476   183982    16.0 |  0.767 % |
c |    741117 |   39245   113159 |   28040   13185   240450    18.2 |  0.767 % |
c |    743680 |   39245   113159 |   30844   15748   321035    20.4 |  0.767 % |
c ==============================================================================
c [1mFound solution: 2005[0m
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    746764 |   39251   113173 |   13083   18832   416684    22.1 |  0.767 % |
c |    746864 |   39251   113173 |   14391    9516   186005    19.5 |  0.774 % |
c |    747014 |   39251   113173 |   15830    9666   190248    19.7 |  0.774 % |
c |    747239 |   39251   113173 |   17413    9891   196259    19.8 |  0.774 % |
c |    747577 |   39251   113173 |   19154   10229   205501    20.1 |  0.774 % |
c |    748083 |   39251   113173 |   21070   10735   219323    20.4 |  0.774 % |
c |    748842 |   39251   113173 |   23177   11494   240973    21.0 |  0.774 % |
c ==============================================================================
c [1mFound solution: 1998[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    749443 |   39260   113194 |   13086   12095   263797    21.8 |  0.774 % |
c |    749544 |   39260   113194 |   14394   12196   266861    21.9 |  0.780 % |
c |    749695 |   39260   113194 |   15834   12347   271873    22.0 |  0.780 % |
c |    749920 |   39260   113194 |   17417   12572   275432    21.9 |  0.780 % |
c |    750257 |   39260   113194 |   19159   12909   279411    21.6 |  0.780 % |
c |    750763 |   39260   113194 |   21075   13415   285346    21.3 |  0.780 % |
c |    751522 |   39260   113194 |   23182   14174   305973    21.6 |  0.780 % |
c |    752661 |   39260   113194 |   25500   15313   331679    21.7 |  0.780 % |
c |    754369 |   39260   113194 |   28051   17021   360309    21.2 |  0.780 % |
c |    756932 |   39260   113194 |   30856   19584   442144    22.6 |  0.780 % |
c |    760778 |   39260   113194 |   33941   23430   557363    23.8 |  0.780 % |
c |    766544 |   39260   113194 |   37335   29196   737982    25.3 |  0.780 % |
c |    775193 |   39260   113194 |   41069   17046   406925    23.9 |  0.780 % |
c ==============================================================================
c [1mFound solution: 1996[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    781405 |   39269   113215 |   13089   23258   615788    26.5 |  0.780 % |
c |    781505 |   39269   113215 |   14397   11729   254937    21.7 |  0.786 % |
c |    781660 |   39269   113215 |   15837   11884   259362    21.8 |  0.786 % |
c |    781886 |   39269   113215 |   17421   12110   266809    22.0 |  0.786 % |
c |    782223 |   39269   113215 |   19163   12447   275155    22.1 |  0.786 % |
c |    782729 |   39269   113215 |   21079   12953   292925    22.6 |  0.786 % |
c |    783488 |   39269   113215 |   23187   13712   306853    22.4 |  0.786 % |
c |    784627 |   39269   113215 |   25506   14851   340029    22.9 |  0.786 % |
c |    786335 |   39269   113215 |   28057   16559   394345    23.8 |  0.786 % |
c |    788899 |   39269   113215 |   30863   19123   490108    25.6 |  0.786 % |
c |    792745 |   39269   113215 |   33949   22969   600146    26.1 |  0.786 % |
c |    798512 |   39269   113215 |   37344   28736   819817    28.5 |  0.786 % |
c |    807162 |   39269   113215 |   41078   37386  1106840    29.6 |  0.786 % |
c |    820136 |   39259   113193 |   45186   26222   712569    27.2 |  0.825 % |
c ==============================================================================
c [1mFound solution: 1995[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    831545 |   39268   113214 |   13089   37631  1257604    33.4 |  0.825 % |
c |    831646 |   39268   113214 |   14397    8371   284428    34.0 |  0.832 % |
c |    831796 |   39268   113214 |   15837    8521   287306    33.7 |  0.832 % |
c |    832021 |   39268   113214 |   17421    8746   292432    33.4 |  0.832 % |
c |    832358 |   39268   113214 |   19163    9083   299700    33.0 |  0.832 % |
c |    832865 |   39268   113214 |   21079    9590   313068    32.6 |  0.832 % |
c |    833624 |   39268   113214 |   23187   10349   329581    31.8 |  0.832 % |
c |    834763 |   39268   113214 |   25506   11488   356496    31.0 |  0.832 % |
c |    836471 |   39268   113214 |   28057   13196   407735    30.9 |  0.832 % |
c |    839034 |   39268   113214 |   30863   15759   484410    30.7 |  0.832 % |
c |    842878 |   39268   113214 |   33949   19603   590220    30.1 |  0.832 % |
c |    848645 |   39268   113214 |   37344   25370   777976    30.7 |  0.832 % |
c ==============================================================================
c [1mFound solution: 1994[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    853834 |   39277   113235 |   13092   30559   899600    29.4 |  0.832 % |
c |    853935 |   39277   113235 |   14401    7741    90993    11.8 |  0.838 % |
c |    854085 |   39277   113235 |   15841    7891    93905    11.9 |  0.838 % |
c |    854312 |   39277   113235 |   17425    8118   100603    12.4 |  0.838 % |
c |    854650 |   39277   113235 |   19167    8456   111345    13.2 |  0.838 % |
c |    855158 |   39277   113235 |   21084    8964   126635    14.1 |  0.838 % |
c |    855917 |   39277   113235 |   23193    9723   150345    15.5 |  0.838 % |
c |    857056 |   39277   113235 |   25512   10862   187597    17.3 |  0.838 % |
c |    858764 |   39277   113235 |   28063   12570   244480    19.4 |  0.838 % |
c |    861326 |   39277   113235 |   30870   15132   332740    22.0 |  0.838 % |
c |    865171 |   39277   113235 |   33957   18977   471211    24.8 |  0.838 % |
c |    870937 |   39277   113235 |   37353   24743   656602    26.5 |  0.838 % |
c |    879587 |   39277   113235 |   41088   33393   931635    27.9 |  0.838 % |
c |    892561 |   39277   113235 |   45197   19566   467043    23.9 |  0.838 % |
c |    912022 |   39277   113235 |   49716   39027   969843    24.9 |  0.838 % |
c |    941214 |   39277   113235 |   54688   36738   982641    26.7 |  0.838 % |
c |    985003 |   39277   113235 |   60157   42175  1106581    26.2 |  0.838 % |
c ==============================================================================
c [1mFound solution: 1993[0m
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    995602 |   39286   113256 |   13095   52774  1721731    32.6 |  0.838 % |
c |    995704 |   39286   113256 |   14404    8775   378088    43.1 |  0.844 % |
c |    995856 |   39286   113256 |   15844    8927   382919    42.9 |  0.844 % |
c |    996083 |   39286   113256 |   17429    9154   388160    42.4 |  0.844 % |
c |    996420 |   39286   113256 |   19172    9491   397955    41.9 |  0.844 % |
c |    996926 |   39286   113256 |   21089    9997   415034    41.5 |  0.844 % |
c |    997685 |   39286   113256 |   23198   10756   439293    40.8 |  0.844 % |
c |    998824 |   39286   113256 |   25518   11895   482514    40.6 |  0.844 % |
c |   1000532 |   39286   113256 |   28070   13603   541679    39.8 |  0.844 % |
c |   1003094 |   39286   113256 |   30877   16165   621066    38.4 |  0.844 % |
c |   1006938 |   39286   113256 |   33965   20009   754003    37.7 |  0.844 % |
c |   1012704 |   39286   113256 |   37361   25775   954909    37.0 |  0.844 % |
c |   1021353 |   39286   113256 |   41097   34424  1287036    37.4 |  0.844 % |
c |   1034327 |   39286   113256 |   45207   22859   732705    32.1 |  0.844 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 21409 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.85 0.95 0.91 2/54 21405
Raw data (stat): 21405 (runsolver) R 21404 22056 22055 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855381549 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.95 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.95 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0008 s]
Raw data (loadavg): 0.91 0.95 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.95 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0167 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0261 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0266 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.031 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.69 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 21409
Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.69
CPU time (s): 1229.84
CPU user time (s): 1229.6
CPU system time (s): 0.244962
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####