PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.5:100.opb
MD5SUM	feaa96df552ef9989407735877840272
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13
Optimality of the best value was proved	NO
Number of terms in the objective function	776
Biggest coefficient in the objective function	474
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	2127
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	474
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	2127
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	776
Total number of constraints	1642
Number of constraints which are clauses	701
Number of constraints which are cardinality constraints (but not clauses)	941
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 6466

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 05:08:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4881 boxname=wulflinc17 idbench=369 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  feaa96df552ef9989407735877840272  /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.5:100.opb
IDLAUNCH: 4881
/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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        815448 kB
Buffers:         36416 kB
Cached:         147936 kB
SwapCached:       2376 kB
Active:          60300 kB
Inactive:       129420 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        815196 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23704 kB
Committed_AS:    63672 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:28:02 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4881 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 866 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   20
c ---[ 169]---> BDD-cost:   20
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   29
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   44
c ---[ 161]---> BDD-cost:   44
c ---[ 160]---> BDD-cost:   50
c ---[ 159]---> BDD-cost:   44
c ---[ 158]---> BDD-cost:   47
c ---[ 157]---> BDD-cost:   44
c ---[ 156]---> BDD-cost:   41
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   20
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   32
c ---[ 143]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   47
c ---[ 141]---> BDD-cost:   47
c ---[ 140]---> BDD-cost:   50
c ---[ 139]---> BDD-cost:   50
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   47
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:   17
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   29
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   35
c ---[ 123]---> BDD-cost:   41
c ---[ 122]---> BDD-cost:   45
c ---[ 121]---> BDD-cost:   47
c ---[ 120]---> BDD-cost:   50
c ---[ 119]---> BDD-cost:   53
c ---[ 118]---> BDD-cost:   53
c ---[ 117]---> BDD-cost:   47
c ---[ 116]---> BDD-cost:   41
c ---[ 115]---> BDD-cost:   35
c ---[ 114]---> BDD-cost:   21
c ---[ 113]---> BDD-cost:   14
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   20
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   20
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   29
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:   41
c ---[ 101]---> BDD-cost:   47
c ---[ 100]---> BDD-cost:   45
c ---[  99]---> BDD-cost:   53
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   47
c ---[  96]---> BDD-cost:   41
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:    5
c ---[  91]---> BDD-cost:   20
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   44
c ---[  78]---> BDD-cost:   38
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   20
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   29
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    7
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    5
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:    7
c ---[  38]---> BDD-cost:   14
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:   11
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    7
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    7
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    8
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    8
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    0
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17906    50153 |    5968       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 641[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:55538     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  159965   382427 |   53321       0        0     nan |  0.000 % |
c |       101 |  159965   382427 |   58653     101      445     4.4 |  0.323 % |
c |       252 |  159614   381634 |   64518     233      957     4.1 |  0.514 % |
c |       477 |  159428   381216 |   70970     457     2331     5.1 |  0.605 % |
c |       814 |  159428   381216 |   78067     794     9838    12.4 |  0.605 % |
c ==============================================================================
c [1mFound solution: 233[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1082 |  163219   390330 |   54406    1052    11528    11.0 |  0.605 % |
c |      1182 |  163219   390330 |   59846    1152    12006    10.4 |  0.765 % |
c |      1332 |  162955   389732 |   65831    1298    15768    12.1 |  0.906 % |
c |      1559 |  162864   389527 |   72414    1523    17241    11.3 |  0.953 % |
c |      1896 |  162796   389371 |   79655    1859    19307    10.4 |  0.989 % |
c |      2402 |  162792   389361 |   87621    2364    25931    11.0 |  0.991 % |
c ==============================================================================
c [1mFound solution: 151[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2749 |  163393   390876 |   54464    2707    27911    10.3 |  0.991 % |
c |      2849 |  163393   390876 |   59910    2807    28726    10.2 |  1.185 % |
c |      2999 |  163393   390876 |   65901    2957    30985    10.5 |  1.185 % |
c |      3224 |  163393   390876 |   72491    3182    32319    10.2 |  1.185 % |
c |      3561 |  163393   390876 |   79740    3519    34851     9.9 |  1.185 % |
c |      4067 |  162894   389740 |   87714    4011    48379    12.1 |  1.459 % |
c |      4826 |  162539   388924 |   96486    4762    54216    11.4 |  1.661 % |
c |      5965 |  162353   388501 |  106134    5900    64942    11.0 |  1.759 % |
c |      7675 |  162046   387797 |  116748    7604    92742    12.2 |  1.931 % |
c |     10237 |  161488   386518 |  128423   10157   122545    12.1 |  2.245 % |
c |     14081 |  160937   385256 |  141265   13984   169727    12.1 |  2.551 % |
c ==============================================================================
c [1mFound solution: 149[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16723 |  160777   384916 |   53592   16614   212666    12.8 |  2.551 % |
c |     16824 |  160777   384916 |   58951   16715   214464    12.8 |  2.682 % |
c |     16976 |  160777   384916 |   64846   16867   215331    12.8 |  2.682 % |
c |     17201 |  160777   384916 |   71330   17092   217023    12.7 |  2.682 % |
c |     17538 |  160777   384916 |   78464   17429   222719    12.8 |  2.682 % |
c |     18046 |  160777   384916 |   86310   17937   227906    12.7 |  2.682 % |
c |     18805 |  160772   384901 |   94941   18694   243456    13.0 |  2.684 % |
c |     19945 |  160340   383905 |  104435   19822   257095    13.0 |  2.939 % |
c |     21653 |  160314   383845 |  114879   21528   274130    12.7 |  2.954 % |
c |     24216 |  160075   383292 |  126367   24077   328349    13.6 |  3.099 % |
c ==============================================================================
c [1mFound solution: 140[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26425 |  160198   383606 |   53399   26281   380794    14.5 |  3.099 % |
c ==============================================================================
c [1mFound solution: 135[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26512 |  160281   383815 |   53427   26368   381406    14.5 |  3.099 % |
c |     26614 |  160281   383815 |   58769   26470   383977    14.5 |  3.107 % |
c |     26764 |  160281   383815 |   64646   26620   387454    14.6 |  3.107 % |
c |     26989 |  160281   383815 |   71111   26845   388832    14.5 |  3.107 % |
c |     27326 |  160281   383815 |   78222   27182   393867    14.5 |  3.107 % |
c |     27833 |  160233   383706 |   86044   27681   404141    14.6 |  3.132 % |
c |     28592 |  160108   383417 |   94649   28435   415447    14.6 |  3.206 % |
c |     29733 |  160086   383366 |  104114   29568   446654    15.1 |  3.219 % |
c |     31442 |  159886   382908 |  114525   31272   484996    15.5 |  3.330 % |
c |     34004 |  159882   382899 |  125978   33831   525781    15.5 |  3.332 % |
c |     37850 |  159778   382659 |  138575   37654   570184    15.1 |  3.385 % |
c ==============================================================================
c [1mFound solution: 133[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42187 |  159507   382051 |   53169   41955   666475    15.9 |  3.385 % |
c |     42287 |  159507   382051 |   58485   42055   667155    15.9 |  3.593 % |
c |     42437 |  159507   382051 |   64334   42205   668183    15.8 |  3.593 % |
c |     42662 |  159507   382051 |   70767   42430   669988    15.8 |  3.593 % |
c |     42999 |  159507   382051 |   77844   42767   672857    15.7 |  3.593 % |
c |     43505 |  159507   382051 |   85629   43273   695252    16.1 |  3.593 % |
c ==============================================================================
c [1mFound solution: 125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44252 |  159646   382404 |   53215   44020   718256    16.3 |  3.593 % |
c |     44352 |  159646   382404 |   58536   44120   718907    16.3 |  3.592 % |
c |     44503 |  159646   382404 |   64390   44271   719969    16.3 |  3.592 % |
c |     44728 |  159646   382404 |   70829   44496   721984    16.2 |  3.592 % |
c |     45066 |  159436   381921 |   77912   44813   728524    16.3 |  3.713 % |
c |     45574 |  159436   381921 |   85703   45321   734095    16.2 |  3.713 % |
c ==============================================================================
c [1mFound solution: 124[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45842 |  159452   381963 |   53150   45589   738315    16.2 |  3.713 % |
c |     45942 |  159452   381963 |   58465   45689   739101    16.2 |  3.714 % |
c |     46094 |  159452   381963 |   64311   45841   740387    16.2 |  3.714 % |
c |     46320 |  159452   381963 |   70742   46067   742585    16.1 |  3.714 % |
c |     46657 |  159452   381963 |   77816   46404   748385    16.1 |  3.714 % |
c |     47163 |  159452   381963 |   85598   46910   756003    16.1 |  3.714 % |
c |     47922 |  159391   381824 |   94158   47658   788429    16.5 |  3.746 % |
c |     49062 |  159315   381648 |  103574   48775   806246    16.5 |  3.790 % |
c |     50773 |  159315   381648 |  113931   50486   839341    16.6 |  3.790 % |
c ==============================================================================
c [1mFound solution: 123[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51955 |  159319   381658 |   53106   51668   868457    16.8 |  3.790 % |
c |     52057 |  159319   381658 |   58416   51770   872661    16.9 |  3.792 % |
c |     52207 |  159319   381658 |   64258   51920   874007    16.8 |  3.792 % |
c |     52433 |  159319   381658 |   70684   52146   876591    16.8 |  3.792 % |
c |     52770 |  159319   381658 |   77752   52483   880381    16.8 |  3.792 % |
c ==============================================================================
c [1mFound solution: 118[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53086 |  159455   382002 |   53151   52799   888447    16.8 |  3.792 % |
c |     53186 |  159455   382002 |   58466   52899   888943    16.8 |  3.791 % |
c |     53338 |  159455   382002 |   64312   53051   902574    17.0 |  3.791 % |
c |     53563 |  159455   382002 |   70743   53276   906086    17.0 |  3.791 % |
c |     53900 |  159455   382002 |   77818   53613   910969    17.0 |  3.791 % |
c |     54408 |  159455   382002 |   85600   54121   916399    16.9 |  3.791 % |
c |     55167 |  159455   382002 |   94160   54880   928774    16.9 |  3.791 % |
c |     56307 |  159445   381979 |  103576   56016   939711    16.8 |  3.796 % |
c ==============================================================================
c [1mFound solution: 117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57274 |  159459   382017 |   53153   56983   970016    17.0 |  3.796 % |
c |     57374 |  159459   382017 |   58468   23950   278312    11.6 |  3.798 % |
c |     57524 |  159459   382017 |   64315   24100   279255    11.6 |  3.798 % |
c |     57749 |  159459   382017 |   70746   24325   282652    11.6 |  3.798 % |
c |     58087 |  159400   381883 |   77821   24660   287564    11.7 |  3.830 % |
c |     58594 |  159400   381883 |   85603   25167   299377    11.9 |  3.830 % |
c |     59353 |  159231   381501 |   94163   25916   314447    12.1 |  3.917 % |
c |     60492 |  159231   381501 |  103580   27055   341477    12.6 |  3.917 % |
c ==============================================================================
c [1mFound solution: 85[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62029 |  159614   382444 |   53204   28592   369532    12.9 |  3.917 % |
c |     62129 |  159614   382444 |   58524   28692   370143    12.9 |  3.911 % |
c |     62280 |  159614   382444 |   64376   28843   374500    13.0 |  3.911 % |
c |     62506 |  159584   382374 |   70814   29063   377132    13.0 |  3.929 % |
c |     62843 |  159509   382205 |   77895   29398   384505    13.1 |  3.967 % |
c |     63349 |  159509   382205 |   85685   29904   391777    13.1 |  3.967 % |
c |     64108 |  159509   382205 |   94254   30663   405357    13.2 |  3.967 % |
c |     65247 |  159318   381764 |  103679   31798   415340    13.1 |  4.080 % |
c |     66955 |  159318   381764 |  114047   33506   586538    17.5 |  4.080 % |
c |     69517 |  159318   381764 |  125452   36068   646398    17.9 |  4.080 % |
c |     73361 |  159318   381764 |  137997   39912   801080    20.1 |  4.080 % |
c |     79127 |  159314   381754 |  151797   45677  1235172    27.0 |  4.082 % |
c |     87776 |  159230   381561 |  166976   54320  1370034    25.2 |  4.127 % |
c ==============================================================================
c [1mFound solution: 84[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91435 |  159246   381603 |   53082   57979  1472482    25.4 |  4.127 % |
c |     91536 |  159246   381603 |   58390   26494   282969    10.7 |  4.128 % |
c |     91686 |  159246   381603 |   64229   26644   284592    10.7 |  4.128 % |
c |     91912 |  159246   381603 |   70652   26870   290103    10.8 |  4.128 % |
c |     92249 |  159246   381603 |   77717   27207   292526    10.8 |  4.128 % |
c |     92755 |  159211   381521 |   85489   27712   299119    10.8 |  4.151 % |
c |     93514 |  159211   381521 |   94038   28471   305948    10.7 |  4.151 % |
c |     94654 |  159203   381503 |  103441   29605   321831    10.9 |  4.155 % |
c |     96362 |  159203   381503 |  113785   31313   348084    11.1 |  4.155 % |
c |     98926 |  159151   381384 |  125164   33866   396479    11.7 |  4.183 % |
c |    102770 |  159151   381384 |  137681   37710   524402    13.9 |  4.183 % |
c |    108538 |  159151   381384 |  151449   43478   701814    16.1 |  4.183 % |
c ==============================================================================
c [1mFound solution: 83[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111984 |  159150   381379 |   53050   46922   785521    16.7 |  4.183 % |
c |    112084 |  159150   381379 |   58355   47022   786357    16.7 |  4.186 % |
c |    112234 |  159150   381379 |   64190   47172   790246    16.8 |  4.186 % |
c |    112459 |  159150   381379 |   70609   47397   792957    16.7 |  4.186 % |
c |    112796 |  158867   380729 |   77670   47636   795367    16.7 |  4.346 % |
c |    113302 |  158867   380729 |   85437   48142   805618    16.7 |  4.346 % |
c |    114061 |  158859   380711 |   93981   48897   815340    16.7 |  4.350 % |
c |    115201 |  158859   380711 |  103379   50037   845803    16.9 |  4.350 % |
c |    116909 |  158859   380711 |  113717   51745   889286    17.2 |  4.350 % |
c |    119472 |  158859   380711 |  125089   54308   951961    17.5 |  4.350 % |
c |    123316 |  158542   379974 |  137598   58120  1073271    18.5 |  4.547 % |
c |    129082 |  158500   379877 |  151357   63879  1306626    20.5 |  4.572 % |
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135089 |  158564   380045 |   52854   69886  1565323    22.4 |  4.572 % |
c |    135189 |  158564   380045 |   58139   31602   564749    17.9 |  4.572 % |
c |    135339 |  158564   380045 |   63953   31752   565939    17.8 |  4.572 % |
c |    135566 |  158564   380045 |   70348   31979   570438    17.8 |  4.572 % |
c |    135904 |  158498   379892 |   77383   32314   573582    17.8 |  4.610 % |
c |    136410 |  158364   379586 |   85121   32811   578975    17.6 |  4.685 % |
c |    137169 |  158364   379586 |   93634   33570   590838    17.6 |  4.685 % |
c |    138308 |  158364   379586 |  102997   34709   643598    18.5 |  4.685 % |
c |    140018 |  158364   379586 |  113297   36419   668506    18.4 |  4.685 % |
c |    142581 |  158310   379462 |  124626   38965   708494    18.2 |  4.715 % |
c |    146426 |  158304   379448 |  137089   42808   855165    20.0 |  4.719 % |
c |    152192 |  158304   379448 |  150798   48574  1227515    25.3 |  4.719 % |
c |    160841 |  158300   379438 |  165878   57222  1797938    31.4 |  4.720 % |
c |    173815 |  158143   379074 |  182466   70192  2771066    39.5 |  4.816 % |
c ==============================================================================
c [1mFound solution: 80[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175928 |  158159   379116 |   52719   72305  2832364    39.2 |  4.816 % |
c |    176028 |  158159   379116 |   57990   32918   962108    29.2 |  4.818 % |
c |    176178 |  158159   379116 |   63789   33068   968041    29.3 |  4.818 % |
c |    176403 |  158159   379116 |   70168   33293   978735    29.4 |  4.818 % |
c |    176741 |  158159   379116 |   77185   33631   987375    29.4 |  4.818 % |
c |    177247 |  158159   379116 |   84904   34137   998366    29.2 |  4.818 % |
c |    178006 |  158159   379116 |   93394   34896  1019631    29.2 |  4.818 % |
c |    179147 |  158159   379116 |  102734   36037  1069301    29.7 |  4.818 % |
c |    180855 |  158154   379101 |  113007   37744  1150523    30.5 |  4.820 % |
c ==============================================================================
c [1mFound solution: 79[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    181553 |  157972   378680 |   52657   38423  1166011    30.3 |  4.820 % |
c |    181653 |  157972   378680 |   57922   38523  1166757    30.3 |  4.934 % |
c |    181803 |  157972   378680 |   63714   38673  1168335    30.2 |  4.934 % |
c |    182030 |  157958   378647 |   70086   38897  1170303    30.1 |  4.943 % |
c |    182367 |  157797   378278 |   77095   39233  1174121    29.9 |  5.034 % |
c |    182874 |  157797   378278 |   84804   39740  1188386    29.9 |  5.034 % |
c |    183633 |  157797   378278 |   93285   40499  1224684    30.2 |  5.034 % |
c |    184774 |  157793   378269 |  102613   41637  1248563    30.0 |  5.035 % |
c |    186483 |  157793   378269 |  112874   43346  1282850    29.6 |  5.035 % |
c |    189045 |  157793   378269 |  124162   45908  1418305    30.9 |  5.035 % |
c ==============================================================================
c [1mFound solution: 78[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    189330 |  157867   378461 |   52622   46193  1428341    30.9 |  5.035 % |
c |    189430 |  157867   378461 |   57884   46293  1429490    30.9 |  5.035 % |
c |    189581 |  157867   378461 |   63672   46444  1431174    30.8 |  5.035 % |
c |    189806 |  157867   378461 |   70039   46669  1433413    30.7 |  5.035 % |
c |    190143 |  157743   378175 |   77043   46869  1440319    30.7 |  5.107 % |
c |    190649 |  157743   378175 |   84748   47375  1451876    30.6 |  5.107 % |
c |    191408 |  157739   378166 |   93223   48133  1481760    30.8 |  5.109 % |
c |    192549 |  157739   378166 |  102545   49274  1506082    30.6 |  5.109 % |
c |    194258 |  157739   378166 |  112799   50983  1541695    30.2 |  5.109 % |
c |    196820 |  157739   378166 |  124079   53545  1611559    30.1 |  5.109 % |
c |    200664 |  157735   378156 |  136487   57388  1716260    29.9 |  5.110 % |
c |    206431 |  157599   377841 |  150136   63153  1869371    29.6 |  5.193 % |
c |    215080 |  157599   377841 |  165150   71802  2135310    29.7 |  5.193 % |
c |    228055 |  157595   377831 |  181665   84776  2803982    33.1 |  5.195 % |
c |    247516 |  157595   377831 |  199831  104237  3677849    35.3 |  5.195 % |
c ==============================================================================
c [1mFound solution: 76[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    249609 |  157607   377863 |   52535  106329  3736065    35.1 |  5.195 % |
c |    249711 |  157607   377863 |   57788   34673   666703    19.2 |  5.198 % |
c |    249861 |  157607   377863 |   63567   34823   669036    19.2 |  5.198 % |
c |    250088 |  157607   377863 |   69924   35050   671758    19.2 |  5.198 % |
c |    250425 |  157607   377863 |   76916   35387   676433    19.1 |  5.198 % |
c |    250931 |  157493   377602 |   84608   35839   681783    19.0 |  5.260 % |
c |    251691 |  157493   377602 |   93068   36599   702708    19.2 |  5.260 % |
c |    252830 |  157493   377602 |  102375   37738   729993    19.3 |  5.260 % |
c |    254539 |  157441   377482 |  112613   39435   756631    19.2 |  5.292 % |
c |    257101 |  157441   377482 |  123874   41997   821200    19.6 |  5.292 % |
c |    260945 |  157287   377125 |  136262   45770   913508    20.0 |  5.384 % |
c |    266711 |  157287   377125 |  149888   51536  1173876    22.8 |  5.384 % |
c |    275360 |  156941   376330 |  164877   60131  1420073    23.6 |  5.581 % |
c ==============================================================================
c [1mFound solution: 74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    275741 |  157005   376498 |   52335   60512  1444814    23.9 |  5.581 % |
c |    275841 |  157005   376498 |   57568   30356   331056    10.9 |  5.581 % |
c |    275992 |  157005   376498 |   63325   30507   332036    10.9 |  5.581 % |
c |    276217 |  157005   376498 |   69657   30732   334562    10.9 |  5.581 % |
c |    276554 |  157005   376498 |   76623   31069   338412    10.9 |  5.581 % |
c |    277060 |  157005   376498 |   84286   31575   345222    10.9 |  5.581 % |
c |    277820 |  157005   376498 |   92714   32335   355180    11.0 |  5.581 % |
c |    278960 |  157001   376489 |  101986   33472   380142    11.4 |  5.583 % |
c |    280669 |  156959   376390 |  112184   35180   468948    13.3 |  5.613 % |
c |    283231 |  156959   376390 |  123403   37742   550119    14.6 |  5.613 % |
c ==============================================================================
c [1mFound solution: 73[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    284372 |  156973   376428 |   52324   38883   590311    15.2 |  5.613 % |
c |    284472 |  156973   376428 |   57556   38983   595958    15.3 |  5.615 % |
c |    284622 |  156973   376428 |   63312   39133   597052    15.3 |  5.615 % |
c |    284847 |  156973   376428 |   69643   39358   599764    15.2 |  5.615 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    285178 |  156986   376463 |   52328   39689   605287    15.3 |  5.615 % |
c |    285278 |  156986   376463 |   57560   39789   606332    15.2 |  5.616 % |
c |    285429 |  156986   376463 |   63316   39940   612887    15.3 |  5.616 % |
c |    285654 |  156986   376463 |   69648   40165   617640    15.4 |  5.616 % |
c |    285991 |  156986   376463 |   76613   40502   622379    15.4 |  5.616 % |
c |    286497 |  156986   376463 |   84274   41008   636155    15.5 |  5.616 % |
c |    287256 |  156974   376435 |   92702   41751   648251    15.5 |  5.624 % |
c |    288395 |  156974   376435 |  101972   42890   667492    15.6 |  5.624 % |
c |    290103 |  156974   376435 |  112169   44598   735708    16.5 |  5.624 % |
c |    292666 |  156974   376435 |  123386   47161   861351    18.3 |  5.624 % |
c ==============================================================================
c [1mFound solution: 71[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    296083 |  156935   376347 |   52311   50572   999046    19.8 |  5.624 % |
c |    296183 |  156935   376347 |   57542   50672   999657    19.7 |  5.650 % |
c |    296333 |  156935   376347 |   63296   50822  1007512    19.8 |  5.650 % |
c |    296558 |  156935   376347 |   69625   51047  1010171    19.8 |  5.650 % |
c |    296896 |  156935   376347 |   76588   51385  1013238    19.7 |  5.650 % |
c |    297403 |  156935   376347 |   84247   51892  1022881    19.7 |  5.650 % |
c |    298162 |  156935   376347 |   92672   52651  1037091    19.7 |  5.650 % |
c |    299301 |  156932   376341 |  101939   53789  1056174    19.6 |  5.652 % |
c |    301009 |  156932   376341 |  112133   55497  1116593    20.1 |  5.652 % |
c |    303572 |  156867   376190 |  123346   58055  1227479    21.1 |  5.693 % |
c |    307416 |  156704   375810 |  135681   61883  1368569    22.1 |  5.785 % |
c |    313182 |  156704   375810 |  149249   67649  1503807    22.2 |  5.785 % |
c |    321831 |  156704   375810 |  164174   76298  2116848    27.7 |  5.785 % |
c |    334806 |  156615   375604 |  180591   89262  2856992    32.0 |  5.832 % |
c |    354269 |  156615   375604 |  198650  108725  4189514    38.5 |  5.832 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v756 v693 -v588 v262 v241 v56 v38 v692 v590 v486 v263 -v246 v55 v37 -v757 v700 v589 v485 -v439 -v266 -v245 v54 v39 -v758 v694 v594 v487 -v444 -v264 v52 v40 -v761 v695 -v612 v593 v488 -v443 -v265 v248 -v53 v47 -v759 -v696 -v611 v591 v489 -v401 v249 v41 -v2 -v760 -v613 v592 v496 -v446 -v421 -v400 -v252 -v198 -v171 v42 -v1 -v734 v616 v490 -v447 -v420 -v406 -v385 -v250 -v176 v43 v3 -v733 v615 v491 -v450 -v422 -v405 v384 v273 -v251 -v197 -v175 -v137 v4 v620 -v492 -v448 v425 -v407 v386 -v366 -v278 -v201 v155 -v136 -v18 v5 -v735 v619 -v559 -v510 -v449 v424 -v411 v387 -v365 -v277 -v178 v154 -v138 -v87 -v17 v12 -v737 -v650 v617 -v515 v429 -v410 v388 -v202 -v179 v156 v141 -v86 v23 v6 -v649 -v618 -v558 -v514 -v466 v428 -v408 -v395 -v367 v280 -v182 v157 v140 -v88 -v66 v22 v7 -v738 -v562 -v426 -v409 v389 v369 v281 -v180 v158 v145 v91 v71 v24 -v8 -v740 -v651 v517 -v469 -v427 v390 -v318 -v284 -v223 -v181 v165 v144 -v121 v90 v70 v28 -v741 v653 -v635 -v563 v518 -v470 -v391 v370 -v317 -v282 v159 -v142 v95 -v27 -v634 -v521 -v372 -v347 -v319 -v283 -v222 v160 -v143 -v120 v94 v73 -v25 v654 -v519 -v373 -v351 v322 v226 -v161 -v92 v74 -v26 v656 -v636 -v520 v321 -v124 -v93 v75 v657 -v639 v323 v227 -v125 v76 -v753 -v703 -v64 -v755 -v704 -v587 -v267 v240 -v60 -v754 v699 -v602 v242 -v59 -v50 -v762 -v598 -v438 -v247 -v51 v710 v697 -v597 -v499 -v440 v244 v46 v714 -v500 -v445 -v253 v495 -v442 v44 -v729 -v614 -v451 -v402 -v170 -v728 -v628 v493 -v403 -v199 -v172 -v15 -v624 -v423 -v404 -v361 v272 -v203 -v177 -v16 -v736 -v623 -v437 -v415 -v398 -v360 v274 -v174 v11 -v739 -v645 -v509 -v433 -v399 -v279 -v183 -v139 -v19 -v743 -v644 -v560 -v511 -v465 -v432 -v394 -v368 v276 v205 -v168 v153 -v20 -v9 -v742 -v564 -v516 v371 -v285 v206 -v169 -v149 -v89 -v65 v21 -v652 v513 -v471 -v392 -v375 v164 -v148 -v116 -v103 -v67 v32 v655 -v630 -v522 -v374 -v99 v72 v659 -v629 -v566 -v346 -v224 v162 -v122 -v98 v69 v658 -v567 -v350 -v320 v228 v77 -v637 -v474 v331 -v126 -v638 -v327 -v701 -v599 v105 -v63 -v49 -v752 -v601 v271 -v48 -v770 -v498 v270 -v57 -v766 -v497 v243 -v765 v709 -v698 -v595 v261 -v58 v713 -v441 v257 -v193 -v625 -v596 -v459 -v302 v256 -v192 v45 -v14 -v627 -v455 -v13 v494 -v454 -v434 -v418 -v397 -v200 -v730 -v554 -v436 -v419 -v396 -v204 -v173 -v731 -v621 -v553 -v461 -v414 v208 -v191 -v167 v150 -v732 -v362 v275 v207 -v187 -v166 v152 -v747 -v622 -v561 -v467 -v430 -v412 -v363 v293 -v186 -v100 -v35 -v10 -v646 -v565 -v512 v364 -v289 v218 -v102 -v36 -v685 -v647 -v569 -v530 -v472 -v431 -v393 -v379 -v288 v217 -v146 v31 v648 -v568 -v526 -v115 -v68 -v663 -v525 -v475 -v348 v328 -v225 -v163 -v147 -v117 -v96 v85 v29 -v631 -v473 -v352 v330 v229 -v123 -v81 -v632 v230 -v119 -v97 -v80 -v633 -v326 v231 -v127 -v767 -v702 -v600 v333 v104 -v61 -v769 v268 v258 v260 -v763 v711 -v456 -v299 v269 v715 -v626 -v458 -v764 -v417 v301 v254 -v435 -v416 -v194 v717 -v452 v255 -v195 -v188 v718 v196 -v190 v151 -v750 -v453 v290 v212 -v34 -v751 -v555 -v460 v292 -v101 -v33 -v746 -v681 -v556 -v527 -v462 -v413 -v382 -v184 -v557 -v529 -v468 -v383 v343 -v744 -v684 -v666 -v573 -v464 -v378 v342 -v286 -v185 v82 -v667 -v476 v329 v219 v84 -v662 -v534 -v523 -v376 -v349 -v287 v220 v30 -v538 -v353 v221 -v118 -v660 -v642 -v604 -v524 v354 v235 -v135 -v78 -v643 v608 v355 -v324 -v131 -v768 v332 v106 -v62 -v706 v259 -v705 -v457 v712 v298 -v108 v716 v720 v303 v719 -v189 -v749 v215 -v748 v291 v216 v677 -v381 -v306 v211 -v528 -v380 -v680 -v665 -v576 v209 -v664 -v577 -v463 v83 -v745 -v686 -v572 -v484 -v480 v344 -v641 -v570 -v533 -v479 -v377 v345 v238 -v132 -v640 -v537 v239 -v134 -v689 -v661 -v603 v234 -v79 v607 -v325 -v130 v502 -v295 v109 -v707 -v107 -v708 v546 -v335 v300 v771 -v724 v304 v214 v213 v673 -v307 -v305 v772 v676 v773 -v575 -v574 v682 -v481 -v210 -v483 v687 v237 v236 -v133 v690 -v571 -v535 -v477 -v358 v688 v539 -v359 -v605 -v478 v232 v609 -v128 v110 v501 v336 v334 -v294 v727 v545 -v296 -v723 -v308 -v721 v672 -v582 -v482 v683 -v532 v679 v531 -v357 v691 -v356 -v536 v540 v606 -v233 v610 -v129 v337 -v114 v726 v503 -v113 v725 v547 -v297 v669 -v506 v316 v312 -v722 v674 -v581 v549 #### 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.92 0.98 0.92 2/55 29585
Raw data (stat): 29585 (runsolver) R 29584 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481957195 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99982 s]
Raw data (loadavg): 0.93 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 4927 0 0 0 986 12 0 0 25 0 1 0 481957195 22265856 4757 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5436 4757 603 41 0 5395 0
vsize: 21744
[startup+20 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5017 0 0 0 1984 13 0 0 25 0 1 0 481957195 22716416 4847 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5546 4847 603 41 0 5505 0
vsize: 22184
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5120 0 0 0 2983 13 0 0 25 0 1 0 481957195 23121920 4950 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5645 4950 603 41 0 5604 0
vsize: 22580
[startup+40.0005 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5250 0 0 0 3982 14 0 0 25 0 1 0 481957195 23691264 5080 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5784 5080 603 41 0 5743 0
vsize: 23136
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5385 0 0 0 4982 14 0 0 25 0 1 0 481957195 24227840 5215 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5215 603 41 0 5874 0
vsize: 23660
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5470 0 0 0 5982 14 0 0 25 0 1 0 481957195 24465408 5300 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5973 5300 603 41 0 5932 0
vsize: 23892
[startup+70.0014 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5619 0 0 0 6981 15 0 0 25 0 1 0 481957195 25264128 5449 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6168 5449 603 41 0 6127 0
vsize: 24672
[startup+80.0023 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5769 0 0 0 7981 15 0 0 25 0 1 0 481957195 25800704 5599 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6299 5599 603 41 0 6258 0
vsize: 25196
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5901 0 0 0 8981 16 0 0 25 0 1 0 481957195 26304512 5731 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6422 5731 603 41 0 6381 0
vsize: 25688
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 5964 0 0 0 9980 16 0 0 25 0 1 0 481957195 26574848 5794 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6488 5794 603 41 0 6447 0
vsize: 25952
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6066 0 0 0 10980 17 0 0 25 0 1 0 481957195 26980352 5896 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6587 5896 603 41 0 6546 0
vsize: 26348
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6157 0 0 0 11980 17 0 0 25 0 1 0 481957195 27394048 5987 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6688 5987 603 41 0 6647 0
vsize: 26752
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6257 0 0 0 12980 17 0 0 25 0 1 0 481957195 27709440 6087 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6765 6087 603 41 0 6724 0
vsize: 27060
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6257 0 0 0 13980 17 0 0 25 0 1 0 481957195 27709440 6087 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6765 6087 603 41 0 6724 0
vsize: 27060
[startup+150.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29585
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6257 0 0 0 14980 17 0 0 25 0 1 0 481957195 27709440 6087 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6765 6087 603 41 0 6724 0
vsize: 27060
[startup+160.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6257 0 0 0 15980 17 0 0 25 0 1 0 481957195 27709440 6087 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6765 6087 603 41 0 6724 0
vsize: 27060
[startup+170.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6257 0 0 0 16980 18 0 0 25 0 1 0 481957195 27709440 6087 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6765 6087 603 41 0 6724 0
vsize: 27060
[startup+180.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6257 0 0 0 17980 18 0 0 25 0 1 0 481957195 27709440 6087 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6765 6087 603 41 0 6724 0
vsize: 27060
[startup+190.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6257 0 0 0 18981 18 0 0 25 0 1 0 481957195 27709440 6087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6765 6087 603 41 0 6724 0
vsize: 27060
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6517 0 0 0 19980 18 0 0 25 0 1 0 481957195 28786688 6347 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7028 6347 603 41 0 6987 0
vsize: 28112
[startup+210.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6566 0 0 0 20980 18 0 0 25 0 1 0 481957195 29052928 6396 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7093 6396 603 41 0 7052 0
vsize: 28372
[startup+220.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6615 0 0 0 21980 19 0 0 25 0 1 0 481957195 29188096 6445 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7126 6445 603 41 0 7085 0
vsize: 28504
[startup+230.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6690 0 0 0 22980 19 0 0 25 0 1 0 481957195 29585408 6520 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7223 6520 603 41 0 7182 0
vsize: 28892
[startup+240.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6825 0 0 0 23980 19 0 0 25 0 1 0 481957195 30121984 6655 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7354 6655 603 41 0 7313 0
vsize: 29416
[startup+250.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 24980 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+260.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 25981 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 26981 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 27981 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+290.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 28981 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+300.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 29981 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+310.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 30982 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+320.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 31982 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+330.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6874 0 0 0 32982 19 0 0 25 0 1 0 481957195 30232576 6704 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6704 603 41 0 7340 0
vsize: 29524
[startup+340.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6876 0 0 0 33982 19 0 0 25 0 1 0 481957195 30232576 6706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6706 603 41 0 7340 0
vsize: 29524
[startup+350.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6879 0 0 0 34982 19 0 0 25 0 1 0 481957195 30232576 6709 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6709 603 41 0 7340 0
vsize: 29524
[startup+360.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 6881 0 0 0 35982 19 0 0 25 0 1 0 481957195 30232576 6711 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6711 603 41 0 7340 0
vsize: 29524
[startup+370.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7127 0 0 0 36982 20 0 0 25 0 1 0 481957195 31477760 6957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6957 603 41 0 7644 0
vsize: 30740
[startup+380.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7127 0 0 0 37982 20 0 0 25 0 1 0 481957195 31477760 6957 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6957 603 41 0 7644 0
vsize: 30740
[startup+390.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7127 0 0 0 38982 20 0 0 25 0 1 0 481957195 31477760 6957 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6957 603 41 0 7644 0
vsize: 30740
[startup+400.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7127 0 0 0 39983 20 0 0 25 0 1 0 481957195 31477760 6957 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6957 603 41 0 7644 0
vsize: 30740
[startup+410.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7128 0 0 0 40983 20 0 0 25 0 1 0 481957195 31477760 6958 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6958 603 41 0 7644 0
vsize: 30740
[startup+420.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7128 0 0 0 41983 20 0 0 25 0 1 0 481957195 31477760 6958 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6958 603 41 0 7644 0
vsize: 30740
[startup+430.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7128 0 0 0 42983 20 0 0 25 0 1 0 481957195 31477760 6958 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6958 603 41 0 7644 0
vsize: 30740
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7128 0 0 0 43983 20 0 0 25 0 1 0 481957195 31477760 6958 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7685 6958 603 41 0 7644 0
vsize: 30740
[startup+450.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29587
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7363 0 0 0 44983 20 0 0 25 0 1 0 481957195 32546816 7193 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7946 7193 603 41 0 7905 0
vsize: 31784
[startup+460.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7512 0 0 0 45983 21 0 0 25 0 1 0 481957195 33075200 7342 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8075 7342 603 41 0 8034 0
vsize: 32300
[startup+470.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 7817 0 0 0 46982 22 0 0 25 0 1 0 481957195 34283520 7647 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8370 7647 603 41 0 8329 0
vsize: 33480
[startup+480.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8029 0 0 0 47982 22 0 0 25 0 1 0 481957195 35217408 7859 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8598 7859 603 41 0 8557 0
vsize: 34392
[startup+490.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8355 0 0 0 48981 23 0 0 25 0 1 0 481957195 36564992 8185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8927 8185 603 41 0 8886 0
vsize: 35708
[startup+500.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8446 0 0 0 49981 23 0 0 25 0 1 0 481957195 36970496 8276 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9026 8276 603 41 0 8985 0
vsize: 36104
[startup+510.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8496 0 0 0 50981 24 0 0 25 0 1 0 481957195 37064704 8326 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8326 603 41 0 9008 0
vsize: 36196
[startup+520.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8496 0 0 0 51981 24 0 0 25 0 1 0 481957195 37064704 8326 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8326 603 41 0 9008 0
vsize: 36196
[startup+530.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8496 0 0 0 52981 24 0 0 25 0 1 0 481957195 37064704 8326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8326 603 41 0 9008 0
vsize: 36196
[startup+540.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8496 0 0 0 53981 24 0 0 25 0 1 0 481957195 37064704 8326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8326 603 41 0 9008 0
vsize: 36196
[startup+550.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8496 0 0 0 54981 24 0 0 25 0 1 0 481957195 37064704 8326 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8326 603 41 0 9008 0
vsize: 36196
[startup+560.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 55982 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+570.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 56982 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+580.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 57982 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+590.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 58982 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+600.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 59982 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+610.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 60982 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+620.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 61983 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+630.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8502 0 0 0 62983 24 0 0 25 0 1 0 481957195 37064704 8332 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8332 603 41 0 9008 0
vsize: 36196
[startup+640.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8506 0 0 0 63983 24 0 0 25 0 1 0 481957195 37064704 8336 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8336 603 41 0 9008 0
vsize: 36196
[startup+650.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8509 0 0 0 64983 24 0 0 25 0 1 0 481957195 37064704 8339 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8339 603 41 0 9008 0
vsize: 36196
[startup+660.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8513 0 0 0 65983 24 0 0 25 0 1 0 481957195 37064704 8343 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9049 8343 603 41 0 9008 0
vsize: 36196
[startup+670.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8695 0 0 0 66983 25 0 0 25 0 1 0 481957195 37863424 8525 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9244 8525 603 41 0 9203 0
vsize: 36976
[startup+680.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8788 0 0 0 67983 25 0 0 25 0 1 0 481957195 38256640 8618 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9340 8618 603 41 0 9299 0
vsize: 37360
[startup+690.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 8886 0 0 0 68982 26 0 0 25 0 1 0 481957195 38658048 8716 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9438 8716 603 41 0 9397 0
vsize: 37752
[startup+700.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9009 0 0 0 69982 26 0 0 25 0 1 0 481957195 39051264 8839 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9534 8839 603 41 0 9493 0
vsize: 38136
[startup+710.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9126 0 0 0 70982 27 0 0 25 0 1 0 481957195 39591936 8956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9666 8956 603 41 0 9625 0
vsize: 38664
[startup+720.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9255 0 0 0 71981 27 0 0 25 0 1 0 481957195 40120320 9085 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9795 9085 603 41 0 9754 0
vsize: 39180
[startup+730.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9382 0 0 0 72981 27 0 0 25 0 1 0 481957195 40652800 9212 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9925 9212 603 41 0 9884 0
vsize: 39700
[startup+740.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9500 0 0 0 73981 28 0 0 25 0 1 0 481957195 41046016 9330 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10021 9330 603 41 0 9980 0
vsize: 40084
[startup+750.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29589
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9606 0 0 0 74981 28 0 0 25 0 1 0 481957195 41443328 9436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10118 9436 603 41 0 10077 0
vsize: 40472
[startup+760.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9706 0 0 0 75981 28 0 0 25 0 1 0 481957195 41848832 9536 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10217 9536 603 41 0 10176 0
vsize: 40868
[startup+770.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 76981 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+780.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 77980 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+790.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 78980 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+800.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 79980 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+810.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 80980 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+820.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 81981 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+830.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 82981 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+840.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 83981 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+850.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 84981 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+860.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 85981 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+870.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 86981 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+880.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 87982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+890.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 88982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+900.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 89982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+910.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 90982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+920.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 91982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+930.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 92982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+940.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 93982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+950.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 94982 29 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+960.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 95982 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+970.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 96982 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+980.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 97983 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+990.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 98983 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 99983 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 100983 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 101983 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223648 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 102984 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 103984 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29591
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 104982 30 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 105982 31 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 106982 31 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223728 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 107983 31 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 108983 31 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9828 0 0 0 109983 31 0 0 25 0 1 0 481957195 42356736 9658 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10341 9658 603 41 0 10300 0
vsize: 41364
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 9979 0 0 0 110983 31 0 0 25 0 1 0 481957195 43032576 9809 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10506 9809 603 41 0 10465 0
vsize: 42024
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 10357 0 0 0 111982 31 0 0 25 0 1 0 481957195 44519424 10187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10869 10187 603 41 0 10828 0
vsize: 43476
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 10532 0 0 0 112982 32 0 0 25 0 1 0 481957195 45326336 10362 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11066 10362 603 41 0 11025 0
vsize: 44264
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 10594 0 0 0 113982 32 0 0 25 0 1 0 481957195 45461504 10424 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11099 10424 603 41 0 11058 0
vsize: 44396
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 10660 0 0 0 114982 33 0 0 25 0 1 0 481957195 45731840 10490 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11165 10490 603 41 0 11124 0
vsize: 44660
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 10744 0 0 0 115981 33 0 0 25 0 1 0 481957195 46129152 10574 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11262 10574 603 41 0 11221 0
vsize: 45048
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 10853 0 0 0 116981 34 0 0 25 0 1 0 481957195 46534656 10683 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11361 10683 603 41 0 11320 0
vsize: 45444
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 11094 0 0 0 117980 35 0 0 25 0 1 0 481957195 47472640 10924 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11590 10924 603 41 0 11549 0
vsize: 46360
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 11263 0 0 0 118979 36 0 0 25 0 1 0 481957195 48136192 11093 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11752 11093 603 41 0 11711 0
vsize: 47008
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 29593
Raw data (stat): 29585 (minisat+) R 29584 20838 20837 0 -1 0 11422 0 0 0 119979 36 0 0 25 0 1 0 481957195 48803840 11252 4294967295 134512640 134672761 3221224544 3221223728 134558853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11915 11252 603 41 0 11874 0
vsize: 47660
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.92 1/55 29593
Raw data (stat): 29585 (minisat+) Z 29584 20838 20837 0 -1 12 11425 0 0 0 119980 38 0 0 25 0 1 0 481957195 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.19
CPU user time (s): 1199.8
CPU system time (s): 0.387941
CPU usage (%): 100.013
Max. virtual memory (Kb): 47660
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####