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/submitted/een/normalized-l152lav.opb
MD5SUM	7ef542195551d721d26b015e392d6d4b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	1989
Biggest coefficient in the objective function	268
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	382524
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	1961
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	382524
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.237962
Number of variables	1989
Total number of constraints	193
Number of constraints which are clauses	95
Number of constraints which are cardinality constraints (but not clauses)	97
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	3
Maximum length of a constraint	1989
Trace number 7144

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-14 21:36:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5224 boxname=wulflinc28 idbench=402 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7ef542195551d721d26b015e392d6d4b  /oldhome/oroussel/tmp/wulflinc28/normalized-l152lav.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc28/normalized-l152lav.opb /oldhome/oroussel/tmp/wulflinc28/normalized-l152lav.opb
IDLAUNCH: 5224
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        855028 kB
Buffers:         36488 kB
Cached:         105968 kB
SwapCached:          4 kB
Active:          68412 kB
Inactive:        77796 kB
HighTotal:      131008 kB
HighFree:        20524 kB
LowTotal:       903652 kB
LowFree:        834504 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27844 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:56:31 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 5224 7 1200.14 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 193 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ==========================================================================================
c   -- Clauses(.)/Splits(s): ......
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    7
c ---[ 187]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   21
c ---[ 183]---> BDD-cost:   35
c ---[ 181]---> BDD-cost:   39
c ---[ 179]---> BDD-cost:   41
c ---[ 177]---> BDD-cost:   45
c ---[ 175]---> BDD-cost:   49
c ---[ 173]---> BDD-cost:   51
c ---[ 171]---> BDD-cost:   59
c ---[ 170]---> BDD-cost:   59
c ---[ 167]---> BDD-cost:   61
c ---[ 165]---> BDD-cost:   61
c ---[ 163]---> BDD-cost:   63
c ---[ 161]---> BDD-cost:   67
c ---[ 159]---> BDD-cost:   71
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:   71
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   81
c ---[ 148]---> BDD-cost:   81
c ---[ 147]---> BDD-cost:   81
c ---[ 145]---> BDD-cost:   83
c ---[ 143]---> BDD-cost:   85
c ---[ 141]---> BDD-cost:   85
c ---[ 139]---> BDD-cost:   85
c ---[ 137]---> BDD-cost:   87
c ---[ 135]---> BDD-cost:   89
c ---[ 133]---> BDD-cost:   91
c ---[ 131]---> BDD-cost:   93
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   93
c ---[ 125]---> BDD-cost:   95
c ---[ 123]---> BDD-cost:   97
c ---[ 120]---> BDD-cost:  101
c ---[ 119]---> BDD-cost:  101
c ---[ 117]---> BDD-cost:  103
c ---[ 115]---> BDD-cost:  105
c ---[ 113]---> BDD-cost:  109
c ---[ 111]---> BDD-cost:  109
c ---[ 109]---> BDD-cost:  113
c ---[ 107]---> BDD-cost:  117
c ---[ 105]---> BDD-cost:  121
c ---[ 103]---> BDD-cost:  121
c ---[ 101]---> BDD-cost:  129
c ---[  99]---> BDD-cost:  133
c ---[  97]---> BDD-cost:  133
c ---[  95]---> BDD-cost:  133
c ---[  93]---> BDD-cost:  143
c ---[  91]---> BDD-cost:  145
c ---[  89]---> BDD-cost:  147
c ---[  87]---> BDD-cost:  147
c ---[  85]---> BDD-cost:  147
c ---[  83]---> BDD-cost:  149
c ---[  81]---> BDD-cost:  151
c ---[  79]---> BDD-cost:  151
c ---[  77]---> BDD-cost:  153
c ---[  75]---> BDD-cost:  155
c ---[  73]---> BDD-cost:  149
c ---[  71]---> BDD-cost:  171
c ---[  69]---> BDD-cost:  173
c ---[  67]---> BDD-cost:  171
c ---[  65]---> BDD-cost:  179
c ---[  63]---> BDD-cost:  181
c ---[  61]---> BDD-cost:  179
c ---[  59]---> BDD-cost:  183
c ---[  57]---> BDD-cost:  181
c ---[  55]---> BDD-cost:  189
c ---[  53]---> BDD-cost:  189
c ---[  52]---> BDD-cost:  189
c ---[  49]---> BDD-cost:  191
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  201
c ---[  43]---> BDD-cost:  203
c ---[  41]---> BDD-cost:  205
c ---[  39]---> BDD-cost:  209
c ---[  37]---> BDD-cost:  213
c ---[  35]---> BDD-cost:  213
c ---[  33]---> BDD-cost:  211
c ---[  31]---> BDD-cost:  221
c ---[  29]---> BDD-cost:  225
c ---[  27]---> BDD-cost:  231
c ---[  25]---> BDD-cost:  239
c ---[  23]---> BDD-cost:  231
c ---[  21]---> BDD-cost:  235
c ---[  19]---> BDD-cost:  235
c ---[  17]---> BDD-cost:  253
c ---[  15]---> BDD-cost:  255
c ---[  13]---> BDD-cost:  271
c ---[  11]---> BDD-cost:  301
c ---[   9]---> BDD-cost:  317
c ---[   7]---> BDD-cost:  323
c ---[   5]---> BDD-cost:  339
c ---[   3]---> BDD-cost:  433
c ---[   2]---> Adder-cost: 5478   maxlim: 25152   bits: 15/15
c ---[   0]---> Adder-cost: 3598   maxlim: 1960   bits: 11/11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   97034   314244 |   29110       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24136          
c   -- var.elim.:  2000/24136          
c   -- var.elim.:  3000/24136          
c   -- var.elim.:  4000/24136          
c   -- var.elim.:  5000/24136          
c   -- var.elim.:  6000/24136          
c   -- var.elim.:  7000/24136          
c   -- var.elim.:  8000/24136          
c   -- var.elim.:  9000/24136          
c   -- var.elim.:  10000/24136          
c   -- var.elim.:  11000/24136          
c   -- var.elim.:  12000/24136          
c   -- var.elim.:  13000/24136          
c   -- var.elim.:  14000/24136          
c   -- var.elim.:  15000/24136          
c   -- var.elim.:  16000/24136          
c   -- var.elim.:  17000/24136          
c   -- var.elim.:  18000/24136          
c   -- var.elim.:  19000/24136          
c   -- var.elim.:  20000/24136          
c   -- var.elim.:  21000/24136          
c   -- var.elim.:  22000/24136          
c   -- var.elim.:  23000/24136          
c   -- var.elim.:  24000/24136          
c   -- var.elim.:  24136/24136          
c   -- var.elim.:  1000/1075          
c   -- var.elim.:  1075/1075          
c   -- subsuming                       
c   -- var.elim.:  810/810          
c   -- var.elim.:  777/777          
c   -- subsuming                       
c   -- var.elim.:  646/646          
c   -- var.elim.:  292/292          
c   -- subsuming                       
c   -- var.elim.:  299/299          
c |         0 |   94000   302118 |      --       0       --      -- |     --   | -3006/-11692
c |         0 |   94000   302118 |   37600       0        0     nan |  0.000 % |
c |       100 |   93103   299033 |   40965      98      431     4.4 |  2.300 % |
c |       250 |   93009   298710 |   45016     247     1212     4.9 |  2.354 % |
c |       475 |   92978   298603 |   49501     471     2974     6.3 |  2.371 % |
c |       812 |   92885   298282 |   54397     807    16684    20.7 |  2.425 % |
c |      1318 |   92885   298282 |   59836    1313    25890    19.7 |  2.424 % |
c |      2077 |   91747   294303 |   65014    2070    40764    19.7 |  3.009 % |
c |      3216 |   91747   294303 |   71515    3209    62166    19.4 |  3.009 % |
c ==============================================================================
c (current CPU-time: 10.7154 s)
c ==============================================================================
c [1mFound solution: 2980[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 14768   maxlim: 379544   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4215 |  195048   663256 |   58514    4208    76780    18.2 |  3.009 % |
c   -- subsuming                       
c   -- var.elim.:  1000/17389          
c   -- var.elim.:  2000/17389          
c   -- var.elim.:  3000/17389          
c   -- var.elim.:  4000/17389          
c   -- var.elim.:  5000/17389          
c   -- var.elim.:  6000/17389          
c   -- var.elim.:  7000/17389          
c   -- var.elim.:  8000/17389          
c   -- var.elim.:  9000/17389          
c   -- var.elim.:  10000/17389          
c   -- var.elim.:  11000/17389          
c   -- var.elim.:  12000/17389          
c   -- var.elim.:  13000/17389          
c   -- var.elim.:  14000/17389          
c   -- var.elim.:  15000/17389          
c   -- var.elim.:  16000/17389          
c   -- var.elim.:  17000/17389          
c   -- var.elim.:  17389/17389          
c   -- var.elim.:  73/73          
c   -- var.elim.:  27/27          
c   -- var.elim.:  5/5          
c |      4215 |  194051   657996 |      --    4208       --      -- |     --   | -966/-5093
c |      4215 |  194051   657996 |   77620    4139    66289    16.0 |  3.009 % |
c |      4316 |  194051   657996 |   85382    4240    69335    16.4 |  2.237 % |
c |      4466 |  194051   657996 |   93920    4390    72304    16.5 |  2.237 % |
c |      4691 |  194051   657996 |  103312    4615    76558    16.6 |  2.237 % |
c |      5028 |  194051   657996 |  113644    4952    85540    17.3 |  2.237 % |
c |      5534 |  194024   657884 |  124991    5455    93534    17.1 |  2.240 % |
c |      6293 |  193997   657772 |  137471    6209   124409    20.0 |  2.242 % |
c ==============================================================================
c (current CPU-time: 21.4137 s)
c ==============================================================================
c [1mFound solution: 2372[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380152   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6425 |  194045   657985 |   58213    6341   130793    20.6 |  2.242 % |
c   -- subsuming                       
c   -- var.elim.:  97/97          
c   -- var.elim.:  13/13          
c |      6425 |  194040   657912 |      --    6341       --      -- |     --   | -5/-66
c |      6425 |  194040   657912 |   77616    6341   130793    20.6 |  2.242 % |
c |      6525 |  194040   657912 |   85377    6441   132614    20.6 |  2.260 % |
c |      6675 |  194040   657912 |   93915    6591   134905    20.5 |  2.260 % |
c |      6905 |  194040   657912 |  103306    6821   154940    22.7 |  2.260 % |
c |      7242 |  194040   657912 |  113637    7158   160179    22.4 |  2.260 % |
c |      7750 |  194040   657912 |  125001    7666   170836    22.3 |  2.260 % |
c |      8511 |  194040   657912 |  137501    8427   198247    23.5 |  2.260 % |
c |      9650 |  194040   657912 |  151251    9566   274435    28.7 |  2.260 % |
c |     11359 |  194014   657805 |  166354   11271   406008    36.0 |  2.262 % |
c |     13921 |  193709   656745 |  182702   13830   722866    52.3 |  2.368 % |
c |     17766 |  193676   656618 |  200938   17673  1172801    66.4 |  2.373 % |
c |     23535 |  193441   655734 |  220763   23421  2174855    92.9 |  2.424 % |
c |     32184 |  193007   654222 |  242295   32059  3810258   118.9 |  2.573 % |
c |     45160 |  192755   653198 |  266177   44998  5836259   129.7 |  2.602 % |
c |     64621 |  192666   652852 |  292659   64444  9486500   147.2 |  2.620 % |
c ==============================================================================
c (current CPU-time: 244.681 s)
c ==============================================================================
c [1mFound solution: 2211[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380313   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     68713 |  192666   652873 |   57799   68533 10917397   159.3 |  2.620 % |
c   -- subsuming                       
c   -- var.elim.:  584/584          
c   -- var.elim.:  81/81          
c   -- var.elim.:  101/101          
c   -- subsuming                       
c   -- var.elim.:  91/91          
c   -- var.elim.:  17/17          
c |     68713 |  192423   651214 |      --   68533       --      -- |     --   | -243/-1654
c |     68713 |  192423   651214 |   76969   58174  5252664    90.3 |  2.620 % |
c |     68813 |  192423   651214 |   84666   58274  5256546    90.2 |  2.706 % |
c |     68964 |  192391   651087 |   93117   58424  5264158    90.1 |  2.711 % |
c |     69189 |  192391   651087 |  102428   58649  5289931    90.2 |  2.711 % |
c |     69527 |  192391   651087 |  112671   58987  5302536    89.9 |  2.711 % |
c |     70035 |  192391   651087 |  123939   59495  5315710    89.3 |  2.711 % |
c |     70795 |  192374   651017 |  136320   60246  5383829    89.4 |  2.713 % |
c |     71938 |  192374   651017 |  149953   61389  5423464    88.3 |  2.713 % |
c |     73646 |  192374   651017 |  164948   63097  5686209    90.1 |  2.713 % |
c |     76209 |  192334   650860 |  181405   65656  6039351    92.0 |  2.719 % |
c |     80053 |  192280   650650 |  199489   69491  6541211    94.1 |  2.729 % |
c |     85820 |  192234   650465 |  219386   75253  7409847    98.5 |  2.734 % |
c |     94471 |  192220   650406 |  241307   83901  8414940   100.3 |  2.737 % |
c |    107445 |  192197   650314 |  265406   96871 10819005   111.7 |  2.739 % |
c ==============================================================================
c (current CPU-time: 479.005 s)
c ==============================================================================
c [1mFound solution: 2198[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380326   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    113158 |  192201   650353 |   57660  102580 11936716   116.4 |  2.739 % |
c   -- subsuming                       
c   -- var.elim.:  194/194          
c   -- var.elim.:  27/27          
c |    113158 |  192191   650209 |      --  102580       --      -- |     --   | -10/-140
c |    113158 |  192191   650209 |   76876  102489 11862417   115.7 |  2.739 % |
c |    113258 |  192191   650209 |   84564   29463  2201415    74.7 |  2.752 % |
c |    113408 |  192191   650209 |   93020   29613  2204325    74.4 |  2.752 % |
c |    113635 |  192191   650209 |  102322   29840  2244063    75.2 |  2.752 % |
c |    113975 |  192143   650010 |  112526   30176  2290809    75.9 |  2.757 % |
c |    114481 |  192129   649956 |  123770   30675  2397017    78.1 |  2.759 % |
c |    115240 |  192129   649956 |  136147   31434  2531598    80.5 |  2.759 % |
c |    116379 |  192115   649902 |  149751   32570  2831219    86.9 |  2.762 % |
c |    118088 |  192115   649902 |  164726   34279  3194269    93.2 |  2.762 % |
c |    120651 |  192052   649650 |  181139   36821  3827310   103.9 |  2.772 % |
c |    124495 |  192023   649534 |  199223   40663  4752476   116.9 |  2.777 % |
c |    130263 |  192006   649464 |  219126   46428  5699769   122.8 |  2.780 % |
c |    138913 |  191974   649337 |  240998   55067  7946507   144.3 |  2.785 % |
c ==============================================================================
c (current CPU-time: 647.459 s)
c ==============================================================================
c [1mFound solution: 2197[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 380327   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    147125 |  191882   648976 |   57564   63249  9982242   157.8 |  2.785 % |
c   -- subsuming                       
c   -- var.elim.:  200/200          
c   -- var.elim.:  47/47          
c |    147125 |  191868   648789 |      --   63249       --      -- |     --   | -14/-186
c |    147125 |  191868   648789 |   76747   55642  5343515    96.0 |  2.785 % |
c |    147225 |  191868   648789 |   84421   55742  5351328    96.0 |  2.801 % |
c |    147375 |  191868   648789 |   92864   55892  5356615    95.8 |  2.801 % |
c |    147603 |  191868   648789 |  102150   56120  5380230    95.9 |  2.801 % |
c |    147940 |  191868   648789 |  112365   56457  5437512    96.3 |  2.801 % |
c |    148448 |  191868   648789 |  123602   56965  5507810    96.7 |  2.801 % |
c |    149208 |  191832   648649 |  135936   57721  5628512    97.5 |  2.806 % |
c |    150350 |  191804   648537 |  149508   58857  5833008    99.1 |  2.809 % |
c |    152061 |  191804   648537 |  164459   60568  6299517   104.0 |  2.809 % |
c |    154626 |  191772   648415 |  180875   63126  7064505   111.9 |  2.817 % |
c |    158470 |  191689   648092 |  198876   66960  7771580   116.1 |  2.832 % |
c ==============================================================================
c (current CPU-time: 725.678 s)
c ==============================================================================
c [1mFound solution: 1420[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381104   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    161000 |  191679   648054 |   57503   69484  8458065   121.7 |  2.832 % |
c   -- subsuming                       
c   -- var.elim.:  739/739          
c   -- var.elim.:  78/78          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  19/19          
c   -- var.elim.:  9/9          
c |    161000 |  189604   639653 |      --   69484       --      -- |     --   | -44/-1287
c |    161000 |  189604   639653 |   75841   59650  4813517    80.7 |  2.832 % |
c |    161100 |  189604   639653 |   83425   59750  4818492    80.6 |  3.589 % |
c |    161250 |  189604   639653 |   91768   59900  4820860    80.5 |  3.589 % |
c |    161476 |  189604   639653 |  100945   60126  4830967    80.3 |  3.589 % |
c |    161813 |  189604   639653 |  111039   60463  4848298    80.2 |  3.589 % |
c |    162321 |  189604   639653 |  122143   60971  4944876    81.1 |  3.589 % |
c |    163080 |  189604   639653 |  134358   61730  5133320    83.2 |  3.589 % |
c |    164220 |  189604   639653 |  147793   62870  5328923    84.8 |  3.589 % |
c |    165928 |  189577   639541 |  162550   64576  5551250    86.0 |  3.591 % |
c ==============================================================================
c (current CPU-time: 758.251 s)
c ==============================================================================
c [1mFound solution: 1415[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381109   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    166233 |  189592   639608 |   56877   64881  5610035    86.5 |  3.591 % |
c   -- subsuming                       
c   -- var.elim.:  38/38          
c   -- var.elim.:  11/11          
c |    166233 |  189590   639596 |      --   64881       --      -- |     --   | -2/-10
c |    166233 |  189590   639596 |   75836   64881  5610035    86.5 |  3.591 % |
c |    166333 |  189590   639596 |   83419   64981  5629162    86.6 |  3.596 % |
c |    166484 |  189564   639496 |   91748   65131  5663698    87.0 |  3.601 % |
c |    166711 |  189564   639496 |  100923   65358  5759822    88.1 |  3.601 % |
c |    167049 |  189564   639496 |  111016   65696  5812438    88.5 |  3.601 % |
c |    167557 |  189564   639496 |  122117   66204  5845806    88.3 |  3.601 % |
c |    168316 |  189564   639496 |  134329   66963  5972214    89.2 |  3.601 % |
c |    169455 |  189564   639496 |  147762   68102  6198861    91.0 |  3.601 % |
c |    171164 |  189564   639496 |  162538   69811  6564241    94.0 |  3.601 % |
c ==============================================================================
c (current CPU-time: 798.584 s)
c ==============================================================================
c [1mFound solution: 1310[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381214   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    172170 |  189593   639628 |   56877   70817  6736714    95.1 |  3.601 % |
c   -- subsuming                       
c   -- var.elim.:  45/45          
c   -- var.elim.:  20/20          
c |    172170 |  189567   639462 |      --   70817       --      -- |     --   | -9/-23
c |    172170 |  189567   639462 |   75826   69428  6200257    89.3 |  3.601 % |
c |    172270 |  189567   639462 |   83409   69528  6204673    89.2 |  3.616 % |
c |    172420 |  189567   639462 |   91750   69678  6247719    89.7 |  3.616 % |
c |    172645 |  189567   639462 |  100925   69903  6299006    90.1 |  3.616 % |
c |    172982 |  189567   639462 |  111018   70240  6371458    90.7 |  3.616 % |
c |    173488 |  189567   639462 |  122119   70746  6413802    90.7 |  3.616 % |
c |    174248 |  189567   639462 |  134331   71506  6558785    91.7 |  3.616 % |
c |    175390 |  189538   639344 |  147742   72641  6839441    94.2 |  3.619 % |
c |    177100 |  189538   639344 |  162516   74351  7342632    98.8 |  3.619 % |
c ==============================================================================
c (current CPU-time: 834.538 s)
c ==============================================================================
c [1mFound solution: 1039[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381485   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    178706 |  189551   639410 |   56865   75957  7651664   100.7 |  3.619 % |
c   -- subsuming                       
c   -- var.elim.:  40/40          
c   -- var.elim.:  20/20          
c |    178706 |  189526   639289 |      --   75957       --      -- |     --   | -17/-57
c |    178706 |  189526   639289 |   75810   74982  7186438    95.8 |  3.619 % |
c |    178806 |  189497   639171 |   83378   75081  7187601    95.7 |  3.634 % |
c |    178956 |  189497   639171 |   91716   75231  7197955    95.7 |  3.634 % |
c |    179181 |  189497   639171 |  100888   75456  7250641    96.1 |  3.634 % |
c |    179518 |  189497   639171 |  110977   75793  7374794    97.3 |  3.634 % |
c |    180025 |  189497   639171 |  122074   76300  7490034    98.2 |  3.634 % |
c |    180784 |  189497   639171 |  134282   77059  7609803    98.8 |  3.634 % |
c |    181923 |  189497   639171 |  147710   78198  7951278   101.7 |  3.634 % |
c ==============================================================================
c (current CPU-time: 863.776 s)
c ==============================================================================
c [1mFound solution: 807[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381717   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    182184 |  189518   639258 |   56855   78459  8070334   102.9 |  3.634 % |
c   -- subsuming                       
c   -- var.elim.:  45/45          
c   -- var.elim.:  11/11          
c |    182184 |  189512   639226 |      --   78459       --      -- |     --   | -6/-28
c |    182184 |  189512   639226 |   75804   78457  8070330   102.9 |  3.634 % |
c |    182286 |  189512   639226 |   83385   33820  2567677    75.9 |  3.644 % |
c |    182436 |  189512   639226 |   91723   33970  2575208    75.8 |  3.644 % |
c |    182662 |  189488   639125 |  100883   34194  2592790    75.8 |  3.646 % |
c |    183004 |  189488   639125 |  110971   34536  2639045    76.4 |  3.646 % |
c |    183510 |  189488   639125 |  122068   35042  2715939    77.5 |  3.646 % |
c |    184272 |  189488   639125 |  134275   35804  2776016    77.5 |  3.646 % |
c |    185411 |  189488   639125 |  147703   36943  3277491    88.7 |  3.646 % |
c |    187120 |  189478   639090 |  162465   38631  3643912    94.3 |  3.649 % |
c ==============================================================================
c (current CPU-time: 913.286 s)
c ==============================================================================
c [1mFound solution: 774[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381750   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    189241 |  189481   639107 |   56844   40748  4268970   104.8 |  3.649 % |
c   -- subsuming                       
c   -- var.elim.:  68/68          
c   -- var.elim.:  25/25          
c |    189241 |  189464   639072 |      --   40748       --      -- |     --   | -17/-30
c |    189241 |  189464   639072 |   75785   40102  4054137   101.1 |  3.649 % |
c |    189343 |  189464   639072 |   83364   40204  4064349   101.1 |  3.666 % |
c |    189494 |  189464   639072 |   91700   40355  4078133   101.1 |  3.666 % |
c |    189720 |  189464   639072 |  100870   40581  4093999   100.9 |  3.666 % |
c |    190057 |  189464   639072 |  110957   40918  4127523   100.9 |  3.666 % |
c |    190564 |  189464   639072 |  122053   41425  4225610   102.0 |  3.666 % |
c |    191324 |  189464   639072 |  134258   42185  4337724   102.8 |  3.666 % |
c |    192464 |  189464   639072 |  147684   43325  4554771   105.1 |  3.666 % |
c |    194174 |  188591   636062 |  161704   44952  4854924   108.0 |  3.977 % |
c ==============================================================================
c (current CPU-time: 943.572 s)
c ==============================================================================
c [1mFound solution: 699[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381825   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    194263 |  188593   636078 |   56577   45041  4865905   108.0 |  3.977 % |
c   -- subsuming                       
c   -- var.elim.:  355/355          
c   -- var.elim.:  21/21          
c |    194263 |  188591   635550 |      --   45041       --      -- |     --   | -2/-526
c |    194263 |  188591   635550 |   75436   44630  4674541   104.7 |  3.977 % |
c |    194363 |  188560   635443 |   82966   44729  4677064   104.6 |  3.993 % |
c |    194517 |  188560   635443 |   91263   44883  4724666   105.3 |  3.993 % |
c ==============================================================================
c (current CPU-time: 948.848 s)
c ==============================================================================
c [1mFound solution: 656[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381868   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    194642 |  188581   635535 |   56574   45008  4736392   105.2 |  3.993 % |
c   -- subsuming                       
c   -- var.elim.:  38/38          
c   -- var.elim.:  18/18          
c |    194642 |  188562   635417 |      --   45008       --      -- |     --   | -19/-114
c |    194642 |  188562   635417 |   75424   44544  4598582   103.2 |  3.993 % |
c |    194742 |  188562   635417 |   82967   44644  4604535   103.1 |  4.003 % |
c |    194893 |  188562   635417 |   91264   44795  4617767   103.1 |  4.003 % |
c |    195118 |  188518   635255 |  100366   45017  4633146   102.9 |  4.013 % |
c |    195456 |  188518   635255 |  110403   45355  4692743   103.5 |  4.013 % |
c |    195962 |  188518   635255 |  121444   45861  4758431   103.8 |  4.013 % |
c ==============================================================================
c (current CPU-time: 966.382 s)
c ==============================================================================
c [1mFound solution: 644[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381880   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    196575 |  188531   635308 |   56559   46474  4905424   105.6 |  4.013 % |
c   -- subsuming                       
c   -- var.elim.:  44/44          
c   -- var.elim.:  22/22          
c   -- var.elim.:  8/8          
c |    196575 |  188513   635229 |      --   46474       --      -- |     --   | -18/-76
c |    196575 |  188513   635229 |   75405   46469  4905407   105.6 |  4.013 % |
c |    196676 |  188513   635229 |   82945   46570  4920671   105.7 |  4.023 % |
c |    196831 |  188513   635229 |   91240   46725  4950382   105.9 |  4.023 % |
c |    197058 |  188513   635229 |  100364   46952  5017533   106.9 |  4.023 % |
c |    197395 |  188227   634247 |  110233   47207  5091951   107.9 |  4.126 % |
c |    197902 |  188133   633924 |  121196   47693  5224614   109.5 |  4.160 % |
c |    198661 |  188133   633924 |  133315   48452  5400878   111.5 |  4.160 % |
c |    199800 |  188039   633601 |  146573   49563  5663666   114.3 |  4.193 % |
c ==============================================================================
c (current CPU-time: 995.758 s)
c ==============================================================================
c [1mFound solution: 643[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381881   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    200518 |  187760   632649 |   56327   50250  5805926   115.5 |  4.193 % |
c   -- subsuming                       
c   -- var.elim.:  263/263          
c   -- var.elim.:  20/20          
c |    200518 |  187745   632135 |      --   50250       --      -- |     --   | -15/-513
c |    200518 |  187745   632135 |   75098   49708  5570446   112.1 |  4.193 % |
c |    200619 |  187745   632135 |   82607   49809  5572037   111.9 |  4.299 % |
c |    200769 |  187713   632026 |   90853   49957  5589132   111.9 |  4.309 % |
c |    200994 |  187713   632026 |   99938   50182  5641936   112.4 |  4.309 % |
c |    201341 |  187713   632026 |  109932   50529  5678154   112.4 |  4.309 % |
c |    201849 |  187713   632026 |  120925   51037  5783583   113.3 |  4.309 % |
c |    202608 |  187713   632026 |  133018   51796  5896994   113.9 |  4.309 % |
c |    203748 |  187713   632026 |  146319   52936  6049490   114.3 |  4.309 % |
c ==============================================================================
c (current CPU-time: 1018.44 s)
c ==============================================================================
c [1mFound solution: 618[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381906   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    204004 |  187728   632099 |   56318   53192  6076833   114.2 |  4.309 % |
c   -- subsuming                       
c   -- var.elim.:  35/35          
c   -- var.elim.:  11/11          
c |    204004 |  187720   632070 |      --   53192       --      -- |     --   | -8/-25
c |    204004 |  187720   632070 |   75088   53192  6076833   114.2 |  4.309 % |
c |    204106 |  187720   632070 |   82596   53294  6083935   114.2 |  4.319 % |
c |    204258 |  187720   632070 |   90856   53446  6133528   114.8 |  4.319 % |
c |    204483 |  187720   632070 |   99942   53671  6168210   114.9 |  4.319 % |
c |    204820 |  187720   632070 |  109936   54008  6205941   114.9 |  4.319 % |
c ==============================================================================
c (current CPU-time: 1034.12 s)
c ==============================================================================
c [1mFound solution: 608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381916   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    205298 |  187736   632145 |   56320   54486  6349209   116.5 |  4.319 % |
c   -- subsuming                       
c   -- var.elim.:  24/24          
c   -- var.elim.:  11/11          
c |    205298 |  187723   632088 |      --   54486       --      -- |     --   | -13/-54
c |    205298 |  187723   632088 |   75089   54486  6349209   116.5 |  4.319 % |
c |    205399 |  187723   632088 |   82598   54587  6354398   116.4 |  4.326 % |
c |    205549 |  187723   632088 |   90857   54737  6376147   116.5 |  4.326 % |
c |    205775 |  187692   631981 |   99927   54960  6383480   116.1 |  4.336 % |
c |    206115 |  187692   631981 |  109919   55300  6450233   116.6 |  4.336 % |
c |    206622 |  187399   630975 |  120723   55743  6531049   117.2 |  4.442 % |
c |    207381 |  187399   630975 |  132795   56502  6665520   118.0 |  4.442 % |
c |    208522 |  187399   630975 |  146075   57643  6800986   118.0 |  4.442 % |
c ==============================================================================
c (current CPU-time: 1060.27 s)
c ==============================================================================
c [1mFound solution: 606[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381918   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    208750 |  187314   630690 |   56194   57863  6888375   119.0 |  4.442 % |
c   -- subsuming                       
c   -- var.elim.:  196/196          
c   -- var.elim.:  24/24          
c |    208750 |  187298   630335 |      --   57863       --      -- |     --   | -16/-353
c |    208750 |  187298   630335 |   74919   57863  6888375   119.0 |  4.442 % |
c |    208850 |  187298   630335 |   82411   57963  6890860   118.9 |  4.480 % |
c |    209001 |  187298   630335 |   90652   58114  6900779   118.7 |  4.480 % |
c ==============================================================================
c (current CPU-time: 1065.61 s)
c ==============================================================================
c [1mFound solution: 602[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381922   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    209109 |  187311   630395 |   56193   58222  6929490   119.0 |  4.480 % |
c   -- subsuming                       
c   -- var.elim.:  22/22          
c   -- var.elim.:  12/12          
c |    209109 |  187302   630337 |      --   58222       --      -- |     --   | -9/-55
c |    209109 |  187302   630337 |   74920   56960  6230565   109.4 |  4.480 % |
c |    209209 |  187302   630337 |   82412   57060  6243231   109.4 |  4.488 % |
c |    209360 |  187302   630337 |   90654   57211  6260850   109.4 |  4.488 % |
c |    209585 |  187302   630337 |   99719   57436  6284062   109.4 |  4.488 % |
c |    209922 |  187302   630337 |  109691   57773  6335516   109.7 |  4.488 % |
c |    210432 |  187302   630337 |  120660   58283  6447793   110.6 |  4.488 % |
c |    211192 |  187302   630337 |  132726   59043  6648330   112.6 |  4.488 % |
c |    212333 |  187208   630014 |  145926   60176  6954352   115.6 |  4.521 % |
c ==============================================================================
c (current CPU-time: 1091.28 s)
c ==============================================================================
c [1mFound solution: 590[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381934   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    213174 |  187220   630074 |   56165   61017  7202017   118.0 |  4.521 % |
c   -- subsuming                       
c   -- var.elim.:  58/58          
c   -- var.elim.:  14/14          
c |    213174 |  187207   629960 |      --   61017       --      -- |     --   | -13/-110
c |    213174 |  187207   629960 |   74882   60654  7135297   117.6 |  4.521 % |
c |    213274 |  187207   629960 |   82371   60754  7152108   117.7 |  4.531 % |
c |    213424 |  187196   629923 |   90602   60903  7177128   117.8 |  4.534 % |
c |    213650 |  187196   629923 |   99663   61129  7230041   118.3 |  4.534 % |
c ==============================================================================
c (current CPU-time: 1099.45 s)
c ==============================================================================
c [1mFound solution: 573[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381951   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    213962 |  187176   629844 |   56152   61423  7260871   118.2 |  4.534 % |
c   -- subsuming                       
c   -- var.elim.:  609/609          
c   -- var.elim.:  76/76          
c   -- var.elim.:  15/15          
c   -- subsuming                       
c |    213962 |  185233   622133 |      --   61423       --      -- |     --   | -76/-1227
c |    213962 |  185233   622133 |   74093   61423  7260871   118.2 |  4.534 % |
c |    214063 |  185233   622133 |   81502   61524  7265603   118.1 |  5.187 % |
c |    214214 |  185233   622133 |   89652   61675  7287627   118.2 |  5.187 % |
c ==============================================================================
c (current CPU-time: 1104.03 s)
c ==============================================================================
c [1mFound solution: 555[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 381969   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    214388 |  185303   622406 |   55590   61849  7314462   118.3 |  5.187 % |
c   -- subsuming                       
c   -- var.elim.:  48/48          
c   -- var.elim.:  25/25          
c |    214388 |  185285   622423 |      --   61849       --      -- |     --   | -18/19
c |    214388 |  185285   622423 |   74114   53415  4854330    90.9 |  5.187 % |
c |    214488 |  185285   622423 |   81525   53515  4858078    90.8 |  5.191 % |
c |    214639 |  185285   622423 |   89677   53666  4864516    90.6 |  5.191 % |
c ==============================================================================
c (current CPU-time: 1108.47 s)
c ==============================================================================
c [1mFound solution: 502[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382022   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    214726 |  185331   622606 |   55599   53753  4873340    90.7 |  5.191 % |
c   -- subsuming                       
c   -- var.elim.:  39/39          
c   -- var.elim.:  17/17          
c |    214726 |  185311   622528 |      --   53753       --      -- |     --   | -11/28
c |    214726 |  185311   622528 |   74124   53753  4873340    90.7 |  5.191 % |
c |    214826 |  185311   622528 |   81536   53853  4878142    90.6 |  5.200 % |
c ==============================================================================
c (current CPU-time: 1113.5 s)
c ==============================================================================
c [1mFound solution: 425[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382099   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    214973 |  185331   622600 |   55599   54000  4931736    91.3 |  5.200 % |
c   -- subsuming                       
c   -- var.elim.:  25/25          
c   -- var.elim.:  20/20          
c   -- var.elim.:  3/3          
c |    214973 |  185294   622426 |      --   54000       --      -- |     --   | -37/-171
c |    214973 |  185294   622426 |   74117   54000  4931736    91.3 |  5.200 % |
c |    215073 |  185294   622426 |   81529   54100  4947678    91.5 |  5.208 % |
c |    215224 |  185294   622426 |   89682   54251  5023432    92.6 |  5.208 % |
c ==============================================================================
c (current CPU-time: 1119.1 s)
c ==============================================================================
c [1mFound solution: 409[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382115   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    215350 |  185308   622481 |   55592   54377  5032725    92.6 |  5.208 % |
c   -- subsuming                       
c   -- var.elim.:  18/18          
c   -- var.elim.:  10/10          
c |    215350 |  185303   622478 |      --   54377       --      -- |     --   | -5/-1
c |    215350 |  185303   622478 |   74121   54377  5032725    92.6 |  5.208 % |
c |    215451 |  185293   622443 |   81528   54477  5036935    92.5 |  5.215 % |
c |    215602 |  185293   622443 |   89681   54628  5051403    92.5 |  5.215 % |
c |    215828 |  185293   622443 |   98649   54854  5102015    93.0 |  5.215 % |
c ==============================================================================
c (current CPU-time: 1128.12 s)
c ==============================================================================
c [1mFound solution: 402[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382122   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    216162 |  184431   619487 |   55329   54941  5117933    93.2 |  5.215 % |
c   -- subsuming                       
c   -- var.elim.:  402/402          
c   -- var.elim.:  31/31          
c |    216162 |  184413   618910 |      --   54941       --      -- |     --   | -18/-574
c |    216162 |  184413   618910 |   73765   54720  5004505    91.5 |  5.215 % |
c |    216267 |  184413   618910 |   81141   54825  5014033    91.5 |  5.531 % |
c ==============================================================================
c (current CPU-time: 1131.6 s)
c ==============================================================================
c [1mFound solution: 382[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382142   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    216365 |  184447   619047 |   55334   54923  5035402    91.7 |  5.531 % |
c   -- subsuming                       
c   -- var.elim.:  32/32          
c   -- var.elim.:  13/13          
c |    216365 |  184429   619016 |      --   54923       --      -- |     --   | -18/-26
c |    216365 |  184429   619016 |   73771   54923  5035402    91.7 |  5.531 % |
c |    216468 |  184398   618909 |   81135   55006  5044562    91.7 |  5.554 % |
c |    216619 |  184388   618874 |   89243   55156  5107140    92.6 |  5.556 % |
c ==============================================================================
c (current CPU-time: 1137.15 s)
c ==============================================================================
c [1mFound solution: 360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382164   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    216694 |  184411   618970 |   55323   55231  5117758    92.7 |  5.556 % |
c   -- subsuming                       
c   -- var.elim.:  42/42          
c   -- var.elim.:  28/28          
c |    216694 |  184377   618715 |      --   55231       --      -- |     --   | -34/-251
c |    216694 |  184377   618715 |   73750   54970  5083994    92.5 |  5.556 % |
c |    216794 |  183811   616773 |   80876   55068  5085264    92.3 |  5.772 % |
c ==============================================================================
c (current CPU-time: 1141.11 s)
c ==============================================================================
c [1mFound solution: 353[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382171   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    216935 |  183786   616691 |   55135   55208  5109562    92.6 |  5.772 % |
c   -- subsuming                       
c   -- var.elim.:  237/237          
c   -- var.elim.:  25/25          
c |    216935 |  183779   616350 |      --   55208       --      -- |     --   | -7/-339
c |    216935 |  183779   616350 |   73511   54051  4720013    87.3 |  5.772 % |
c |    217035 |  183779   616350 |   80862   54151  4734459    87.4 |  5.787 % |
c ==============================================================================
c (current CPU-time: 1144.92 s)
c ==============================================================================
c [1mFound solution: 328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382196   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    217122 |  183802   616441 |   55140   54238  4747162    87.5 |  5.787 % |
c   -- subsuming                       
c   -- var.elim.:  24/24          
c   -- var.elim.:  12/12          
c |    217122 |  183786   616358 |      --   54238       --      -- |     --   | -16/-79
c |    217122 |  183786   616358 |   73514   54238  4747162    87.5 |  5.787 % |
c |    217222 |  183786   616358 |   80865   54338  4764461    87.7 |  5.797 % |
c |    217373 |  183786   616358 |   88952   54489  4777653    87.7 |  5.797 % |
c |    217598 |  183786   616358 |   97847   54714  4836836    88.4 |  5.797 % |
c |    217935 |  183786   616358 |  107632   55051  4921282    89.4 |  5.797 % |
c |    218442 |  183767   616297 |  118383   55555  5041342    90.7 |  5.802 % |
c |    219202 |  183757   616262 |  130214   56314  5269319    93.6 |  5.805 % |
c ==============================================================================
c (current CPU-time: 1159.47 s)
c ==============================================================================
c [1mFound solution: 327[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382197   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    219381 |  183669   615961 |   55100   56433  5288607    93.7 |  5.805 % |
c   -- subsuming                       
c   -- var.elim.:  80/80          
c   -- var.elim.:  27/27          
c |    219381 |  183657   615841 |      --   56433       --      -- |     --   | -12/-119
c |    219381 |  183657   615841 |   73462   56433  5288607    93.7 |  5.805 % |
c ==============================================================================
c (current CPU-time: 1162.73 s)
c ==============================================================================
c [1mFound solution: 326[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382198   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    219471 |  183547   615452 |   55064   55060  4752122    86.3 |  5.805 % |
c   -- subsuming                       
c   -- var.elim.:  66/66          
c   -- var.elim.:  29/29          
c |    219471 |  183535   615385 |      --   55060       --      -- |     --   | -12/-66
c |    219471 |  183535   615385 |   73414   55060  4752122    86.3 |  5.805 % |
c |    219574 |  183535   615385 |   80755   55163  4759175    86.3 |  5.880 % |
c |    219724 |  183535   615385 |   88830   55313  4794424    86.7 |  5.880 % |
c ==============================================================================
c (current CPU-time: 1167.96 s)
c ==============================================================================
c [1mFound solution: 297[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382227   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    219888 |  183454   615103 |   55036   55325  4774641    86.3 |  5.880 % |
c   -- subsuming                       
c   -- var.elim.:  63/63          
c   -- var.elim.:  18/18          
c |    219888 |  183413   614890 |      --   55325       --      -- |     --   | -41/-210
c |    219888 |  183413   614890 |   73365   55325  4774641    86.3 |  5.880 % |
c |    219989 |  183402   614853 |   80696   55425  4777851    86.2 |  5.925 % |
c ==============================================================================
c (current CPU-time: 1171.72 s)
c ==============================================================================
c [1mFound solution: 284[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 382240   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    220080 |  183432   614970 |   55029   55516  4814539    86.7 |  5.925 % |
c   -- subsuming                       
c   -- var.elim.:  35/35          
c   -- var.elim.:  18/18          
c |    220080 |  183414   614905 |      --   55516       --      -- |     --   | -18/-63
c |    220080 |  183414   614905 |   73365   54847  4645830    84.7 |  5.925 % |
c |    220183 |  183414   614905 |   80702   54950  4670644    85.0 |  5.928 % |
c |    220334 |  183077   613741 |   88609   55099  4681158    85.0 |  6.044 % |
c |    220564 |  183077   613741 |   97470   55329  4723244    85.4 |  6.044 % |
c |    220902 |  183077   613741 |  107217   55667  4797748    86.2 |  6.044 % |
c ==============================================================================
c (current CPU-time: 1183.7 s)
c ==============================================================================
c [1mFound solution: 254[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 9558   maxlim: 380443   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    221226 |  249090   849330 |   74726   55005  4704314    85.5 |  6.044 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12248          
c   -- var.elim.:  2000/12248          
c   -- var.elim.:  3000/12248          
c   -- var.elim.:  4000/12248          
c   -- var.elim.:  5000/12248          
c   -- var.elim.:  6000/12248          
c   -- var.elim.:  7000/12248          
c   -- var.elim.:  8000/12248          
c   -- var.elim.:  9000/12248          
c   -- var.elim.:  10000/12248          
c   -- var.elim.:  11000/12248          
c   -- var.elim.:  12000/12248          
c   -- var.elim.:  12248/12248          
c   -- var.elim.:  796/796          
c   -- subsuming                       
c |    221226 |  230461   774684 |      --   55005       --      -- |     --   | -18190/-72896
c |    221226 |  230461   774684 |   92184   55005  4704314    85.5 |  6.044 % |
c ==============================================================================
c (current CPU-time: 1189.17 s)
c ==============================================================================
c [1mFound solution: 240[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 6716   maxlim: 372175   bits: 19/19
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    221316 |  274613   931641 |   82383   51051  3599700    70.5 |  6.044 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9899          
c   -- var.elim.:  2000/9899          
c   -- var.elim.:  3000/9899          
c   -- var.elim.:  4000/9899          
c   -- var.elim.:  5000/9899          
c   -- var.elim.:  6000/9899          
c   -- var.elim.:  7000/9899          
c   -- var.elim.:  8000/9899          
c   -- var.elim.:  9000/9899          
c   -- var.elim.:  9899/9899          
c   -- var.elim.:  1000/1249          
c   -- var.elim.:  1249/1249          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  77/77          
c   -- var.elim.:  37/37          
c |    221316 |  265118   896315 |      --   51051       --      -- |     --   | -5892/-21808
c |    221316 |  265118   896315 |  106047   51051  3599700    70.5 |  6.044 % |
c |    221416 |  265118   896315 |  116651   51151  3604081    70.5 | 11.346 % |
c |    221568 |  265118   896315 |  128317   51303  3613717    70.4 | 11.346 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981#### 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.71 0.89 0.89 2/54 27432
Raw data (stat): 27432 (runsolver) R 27431 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487886039 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.76 0.89 0.89 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 6607 0 0 0 982 17 0 0 25 0 1 0 487886039 27021312 5551 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6597 5551 603 41 0 6556 0
vsize: 26388
[startup+20.0003 s]
Raw data (loadavg): 0.79 0.90 0.89 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 15786 0 0 0 1957 41 0 0 25 0 1 0 487886039 64012288 13114 4294967295 134512640 134672761 3221224560 3221223760 134610683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15628 13114 603 41 0 15587 0
vsize: 62512
[startup+30.0009 s]
Raw data (loadavg): 0.83 0.90 0.89 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 17630 0 0 0 2951 47 0 0 25 0 1 0 487886039 65314816 13470 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15946 13470 603 41 0 15905 0
vsize: 63784
[startup+40.0002 s]
Raw data (loadavg): 0.85 0.90 0.89 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 18043 0 0 0 3950 49 0 0 25 0 1 0 487886039 67039232 13883 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 13883 603 41 0 16326 0
vsize: 65468
[startup+50.0013 s]
Raw data (loadavg): 0.87 0.90 0.89 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 18540 0 0 0 4949 50 0 0 25 0 1 0 487886039 69185536 14380 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16891 14380 603 41 0 16850 0
vsize: 67564
[startup+60.002 s]
Raw data (loadavg): 0.89 0.91 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 18931 0 0 0 5947 52 0 0 25 0 1 0 487886039 70639616 14771 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17246 14771 603 41 0 17205 0
vsize: 68984
[startup+70.0023 s]
Raw data (loadavg): 0.91 0.91 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 19578 0 0 0 6944 55 0 0 25 0 1 0 487886039 73474048 15418 4294967295 134512640 134672761 3221224560 3221223728 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17938 15418 603 41 0 17897 0
vsize: 71752
[startup+80.0034 s]
Raw data (loadavg): 0.92 0.91 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 19944 0 0 0 7943 56 0 0 25 0 1 0 487886039 74924032 15784 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18292 15784 603 41 0 18251 0
vsize: 73168
[startup+90.0031 s]
Raw data (loadavg): 0.93 0.91 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 20443 0 0 0 8941 58 0 0 25 0 1 0 487886039 76906496 16283 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18776 16283 603 41 0 18735 0
vsize: 75104
[startup+100.003 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 21073 0 0 0 9938 61 0 0 25 0 1 0 487886039 79413248 16913 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19388 16913 603 41 0 19347 0
vsize: 77552
[startup+110.004 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 21615 0 0 0 10937 62 0 0 25 0 1 0 487886039 81780736 17455 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19966 17455 603 41 0 19925 0
vsize: 79864
[startup+120.004 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 21845 0 0 0 11936 63 0 0 25 0 1 0 487886039 82706432 17685 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20192 17685 603 41 0 20151 0
vsize: 80768
[startup+130.004 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 22348 0 0 0 12935 65 0 0 25 0 1 0 487886039 84819968 18188 4294967295 134512640 134672761 3221224560 3221223744 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20708 18188 603 41 0 20667 0
vsize: 82832
[startup+140.004 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 23076 0 0 0 13933 66 0 0 25 0 1 0 487886039 87707648 18916 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21413 18916 603 41 0 21372 0
vsize: 85652
[startup+150.005 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 23492 0 0 0 14933 67 0 0 25 0 1 0 487886039 89427968 19332 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21833 19332 603 41 0 21792 0
vsize: 87332
[startup+160.004 s]
Raw data (loadavg): 0.98 0.93 0.91 3/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 23635 0 0 0 15932 68 0 0 25 0 1 0 487886039 90091520 19475 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21995 19475 603 41 0 21954 0
vsize: 87980
[startup+170.004 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 24094 0 0 0 16931 69 0 0 25 0 1 0 487886039 91942912 19934 4294967295 134512640 134672761 3221224560 3221223552 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22447 19934 603 41 0 22406 0
vsize: 89788
[startup+180.005 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 24680 0 0 0 17930 70 0 0 25 0 1 0 487886039 94322688 20520 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23028 20520 603 41 0 22987 0
vsize: 92112
[startup+190.004 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 25322 0 0 0 18929 71 0 0 25 0 1 0 487886039 96960512 21162 4294967295 134512640 134672761 3221224560 3221223744 134615994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23672 21162 603 41 0 23631 0
vsize: 94688
[startup+200.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 26124 0 0 0 19926 74 0 0 25 0 1 0 487886039 100233216 21964 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24471 21964 603 41 0 24430 0
vsize: 97884
[startup+210.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 26570 0 0 0 20926 75 0 0 25 0 1 0 487886039 101953536 22410 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24891 22410 603 41 0 24850 0
vsize: 99564
[startup+220.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 27232 0 0 0 21924 77 0 0 25 0 1 0 487886039 104714240 23072 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25565 23072 603 41 0 25524 0
vsize: 102260
[startup+230.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 27723 0 0 0 22923 78 0 0 25 0 1 0 487886039 106684416 23563 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26046 23563 603 41 0 26005 0
vsize: 104184
[startup+240.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 28539 0 0 0 23921 80 0 0 25 0 1 0 487886039 110260224 24379 4294967295 134512640 134672761 3221224560 3221223704 134616254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26919 24379 603 41 0 26878 0
vsize: 107676
[startup+250.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31018 0 0 0 24915 86 0 0 25 0 1 0 487886039 112562176 24948 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27481 24948 603 41 0 27440 0
vsize: 109924
[startup+260.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31018 0 0 0 25914 87 0 0 25 0 1 0 487886039 112562176 24948 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24948 603 41 0 27440 0
vsize: 109924
[startup+270.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31018 0 0 0 26914 87 0 0 25 0 1 0 487886039 112562176 24948 4294967295 134512640 134672761 3221224560 3221223696 134614710 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24948 603 41 0 27440 0
vsize: 109924
[startup+280.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31018 0 0 0 27914 87 0 0 25 0 1 0 487886039 112562176 24948 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24948 603 41 0 27440 0
vsize: 109924
[startup+290.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31018 0 0 0 28915 87 0 0 25 0 1 0 487886039 112562176 24948 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24948 603 41 0 27440 0
vsize: 109924
[startup+300.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31019 0 0 0 29915 87 0 0 25 0 1 0 487886039 112562176 24949 4294967295 134512640 134672761 3221224560 3221223432 1075352757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24949 603 41 0 27440 0
vsize: 109924
[startup+310.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31021 0 0 0 30915 87 0 0 25 0 1 0 487886039 112562176 24951 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24951 603 41 0 27440 0
vsize: 109924
[startup+320.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31025 0 0 0 31915 87 0 0 25 0 1 0 487886039 112562176 24955 4294967295 134512640 134672761 3221224560 3221223580 134565156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24955 603 41 0 27440 0
vsize: 109924
[startup+330.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31030 0 0 0 32915 87 0 0 25 0 1 0 487886039 112562176 24960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24960 603 41 0 27440 0
vsize: 109924
[startup+340.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31032 0 0 0 33915 87 0 0 25 0 1 0 487886039 112562176 24962 4294967295 134512640 134672761 3221224560 3221223744 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24962 603 41 0 27440 0
vsize: 109924
[startup+350.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31034 0 0 0 34916 87 0 0 25 0 1 0 487886039 112562176 24964 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24964 603 41 0 27440 0
vsize: 109924
[startup+360.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31036 0 0 0 35916 87 0 0 25 0 1 0 487886039 112562176 24966 4294967295 134512640 134672761 3221224560 3221223696 134614488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24966 603 41 0 27440 0
vsize: 109924
[startup+370.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31038 0 0 0 36916 87 0 0 25 0 1 0 487886039 112562176 24968 4294967295 134512640 134672761 3221224560 3221223744 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24968 603 41 0 27440 0
vsize: 109924
[startup+380.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31040 0 0 0 37916 87 0 0 25 0 1 0 487886039 112562176 24970 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24970 603 41 0 27440 0
vsize: 109924
[startup+390.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31042 0 0 0 38916 87 0 0 25 0 1 0 487886039 112562176 24972 4294967295 134512640 134672761 3221224560 3221223728 134615859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24972 603 41 0 27440 0
vsize: 109924
[startup+400.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31043 0 0 0 39917 87 0 0 25 0 1 0 487886039 112562176 24973 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24973 603 41 0 27440 0
vsize: 109924
[startup+410.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31045 0 0 0 40917 87 0 0 25 0 1 0 487886039 112562176 24975 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24975 603 41 0 27440 0
vsize: 109924
[startup+420.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31046 0 0 0 41917 87 0 0 25 0 1 0 487886039 112562176 24976 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24976 603 41 0 27440 0
vsize: 109924
[startup+430.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31048 0 0 0 42917 87 0 0 25 0 1 0 487886039 112562176 24978 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27481 24978 603 41 0 27440 0
vsize: 109924
[startup+440.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31083 0 0 0 43917 87 0 0 25 0 1 0 487886039 112824320 25013 4294967295 134512640 134672761 3221224560 3221223760 134610614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27545 25013 603 41 0 27504 0
vsize: 110180
[startup+450.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31252 0 0 0 44917 87 0 0 25 0 1 0 487886039 113483776 25182 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27706 25182 603 41 0 27665 0
vsize: 110824
[startup+460.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31473 0 0 0 45917 87 0 0 25 0 1 0 487886039 114282496 25403 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27901 25403 603 41 0 27860 0
vsize: 111604
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 31833 0 0 0 46916 88 0 0 25 0 1 0 487886039 115867648 25763 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28288 25763 603 41 0 28247 0
vsize: 113152
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 33576 0 0 0 47913 92 0 0 25 0 1 0 487886039 125210624 27502 4294967295 134512640 134672761 3221224560 3221222656 134566155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30569 27502 603 41 0 30528 0
vsize: 122276
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 48910 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 49910 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 50910 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223584 134612944 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 51910 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 52910 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 53911 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 54911 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 55911 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 56911 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 57911 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 58911 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 59912 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 60912 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 61912 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 62912 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 34394 0 0 0 63912 94 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35600 0 0 0 64910 97 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223600 134521344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35892 0 0 0 65909 98 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35892 0 0 0 66909 98 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35892 0 0 0 67909 98 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35892 0 0 0 68909 98 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35892 0 0 0 69909 98 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35892 0 0 0 70909 98 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 35892 0 0 0 71909 98 0 0 25 0 1 0 487886039 118652928 26419 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28968 26419 603 41 0 28927 0
vsize: 115872
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 37852 0 0 0 72904 103 0 0 25 0 1 0 487886039 118640640 26416 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28965 26416 603 41 0 28924 0
vsize: 115860
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 37852 0 0 0 73904 103 0 0 25 0 1 0 487886039 118640640 26416 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26416 603 41 0 28924 0
vsize: 115860
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 37852 0 0 0 74904 103 0 0 25 0 1 0 487886039 118640640 26416 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26416 603 41 0 28924 0
vsize: 115860
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 39058 0 0 0 75901 106 0 0 25 0 1 0 487886039 118640640 26416 4294967295 134512640 134672761 3221224560 3221221968 134522981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28965 26416 603 41 0 28924 0
vsize: 115860
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 39405 0 0 0 76900 107 0 0 25 0 1 0 487886039 118640640 26417 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26417 603 41 0 28924 0
vsize: 115860
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 39405 0 0 0 77900 107 0 0 25 0 1 0 487886039 118640640 26417 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26417 603 41 0 28924 0
vsize: 115860
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 39405 0 0 0 78901 107 0 0 25 0 1 0 487886039 118640640 26417 4294967295 134512640 134672761 3221224560 3221223336 1075351265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26417 603 41 0 28924 0
vsize: 115860
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 40776 0 0 0 79898 110 0 0 25 0 1 0 487886039 118640640 26417 4294967295 134512640 134672761 3221224560 3221222976 134597012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28965 26417 603 41 0 28924 0
vsize: 115860
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 41110 0 0 0 80896 111 0 0 25 0 1 0 487886039 118640640 26417 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26417 603 41 0 28924 0
vsize: 115860
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 41111 0 0 0 81896 111 0 0 25 0 1 0 487886039 118640640 26418 4294967295 134512640 134672761 3221224560 3221223704 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26418 603 41 0 28924 0
vsize: 115860
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 41111 0 0 0 82897 111 0 0 25 0 1 0 487886039 118640640 26418 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26418 603 41 0 28924 0
vsize: 115860
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 42864 0 0 0 83891 117 0 0 25 0 1 0 487886039 118640640 26418 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26418 603 41 0 28924 0
vsize: 115860
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 42864 0 0 0 84891 117 0 0 25 0 1 0 487886039 118640640 26418 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26418 603 41 0 28924 0
vsize: 115860
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 42864 0 0 0 85891 117 0 0 25 0 1 0 487886039 118640640 26418 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26418 603 41 0 28924 0
vsize: 115860
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 44457 0 0 0 86886 121 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 44457 0 0 0 87887 121 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 44457 0 0 0 88887 121 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 44457 0 0 0 89887 121 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 44457 0 0 0 90887 121 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 46206 0 0 0 91883 125 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+930.015 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 46206 0 0 0 92883 125 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+940.015 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 46206 0 0 0 93884 125 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+950.016 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 47794 0 0 0 94878 130 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+960.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 49382 0 0 0 95874 135 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+970.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 50970 0 0 0 96870 139 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+980.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 50970 0 0 0 97870 139 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+990.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 50970 0 0 0 98870 139 0 0 25 0 1 0 487886039 118640640 26424 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26424 603 41 0 28924 0
vsize: 115860
[startup+1000.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 52558 0 0 0 99867 142 0 0 25 0 1 0 487886039 118640640 26425 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26425 603 41 0 28924 0
vsize: 115860
[startup+1010.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 52559 0 0 0 100867 142 0 0 25 0 1 0 487886039 118640640 26426 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26426 603 41 0 28924 0
vsize: 115860
[startup+1020.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 53644 0 0 0 101865 145 0 0 25 0 1 0 487886039 118640640 26426 4294967295 134512640 134672761 3221224560 3221045168 134594077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28965 26426 603 41 0 28924 0
vsize: 115860
[startup+1030.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 54147 0 0 0 102864 146 0 0 25 0 1 0 487886039 118640640 26426 4294967295 134512640 134672761 3221224560 3221223744 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26426 603 41 0 28924 0
vsize: 115860
[startup+1040.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 55735 0 0 0 103859 150 0 0 25 0 1 0 487886039 118640640 26426 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28965 26426 603 41 0 28924 0
vsize: 115860
[startup+1050.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 55735 0 0 0 104858 150 0 0 25 0 1 0 487886039 118640640 26426 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26426 603 41 0 28924 0
vsize: 115860
[startup+1060.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 55735 0 0 0 105858 150 0 0 25 0 1 0 487886039 118640640 26426 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26426 603 41 0 28924 0
vsize: 115860
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 58913 0 0 0 106850 158 0 0 25 0 1 0 487886039 118640640 26428 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26428 603 41 0 28924 0
vsize: 115860
[startup+1080.02 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 58913 0 0 0 107851 158 0 0 25 0 1 0 487886039 118640640 26428 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26428 603 41 0 28924 0
vsize: 115860
[startup+1090.02 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 58913 0 0 0 108851 159 0 0 25 0 1 0 487886039 118640640 26428 4294967295 134512640 134672761 3221224560 3221223600 134613822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26428 603 41 0 28924 0
vsize: 115860
[startup+1100.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 60501 0 0 0 109846 163 0 0 25 0 1 0 487886039 118640640 26428 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28965 26428 603 41 0 28924 0
vsize: 115860
[startup+1110.02 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 64056 0 0 0 110836 172 0 0 25 0 1 0 487886039 118640640 26429 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26429 603 41 0 28924 0
vsize: 115860
[startup+1120.02 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 67399 0 0 0 111829 179 0 0 25 0 1 0 487886039 118640640 26429 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26429 603 41 0 28924 0
vsize: 115860
[startup+1130.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 70026 0 0 0 112824 185 0 0 25 0 1 0 487886039 125227008 27436 4294967295 134512640 134672761 3221224560 3221222976 134609063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30573 27436 603 41 0 30532 0
vsize: 122292
[startup+1140.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 73380 0 0 0 113815 193 0 0 25 0 1 0 487886039 118640640 26434 4294967295 134512640 134672761 3221224560 3221222112 134522994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28965 26434 603 41 0 28924 0
vsize: 115860
[startup+1150.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 76926 0 0 0 114804 204 0 0 25 0 1 0 487886039 118640640 26434 4294967295 134512640 134672761 3221224560 3221223600 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26434 603 41 0 28924 0
vsize: 115860
[startup+1160.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 76926 0 0 0 115805 204 0 0 25 0 1 0 487886039 118640640 26434 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28965 26434 603 41 0 28924 0
vsize: 115860
[startup+1170.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 80092 0 0 0 116796 212 0 0 25 0 1 0 487886039 118804480 26434 4294967295 134512640 134672761 3221224560 3221222680 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26434 603 41 0 28964 0
vsize: 116020
[startup+1180.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 83234 0 0 0 117788 219 0 0 25 0 1 0 487886039 118743040 26432 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28990 26432 603 41 0 28949 0
vsize: 115960
[startup+1190.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 86014 0 0 0 118781 226 0 0 25 0 1 0 487886039 118743040 26818 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28990 26818 603 41 0 28949 0
vsize: 115960
[startup+1200.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27432
Raw data (stat): 27432 (minisat+) R 27431 10614 10613 0 -1 0 89067 0 0 0 119774 234 0 0 25 0 1 0 487886039 122220544 27136 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29839 27136 603 41 0 29798 0
vsize: 119356
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 27432
Raw data (stat): 27432 (minisat+) Z 27431 10614 10613 0 -1 12 89068 0 0 0 119774 239 0 0 25 0 1 0 487886039 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.14
CPU user time (s): 1197.75
CPU system time (s): 2.39664
CPU usage (%): 100.005
Max. virtual memory (Kb): 122292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####