PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod008.opb
MD5SUM	fbdb3cf321a85412feefcaac30780520
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	22000
Number of bits of the biggest number in a constraint	15
Biggest sum of numbers in a constraint	1027256
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01584
Number of variables	319
Total number of constraints	325
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	319
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	231
Trace number 22153

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-22 02:21:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12035 boxname=wulflinc26 idbench=926 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-mod008.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 12035
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        257740 kB
Buffers:         33808 kB
Cached:         716028 kB
SwapCached:         68 kB
Active:         199992 kB
Inactive:       552688 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        257460 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6880 kB
Slab:            18500 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:41:04 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 12035 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> Adder-cost: 2481   maxlim: 21999   bits: 16/15
c ---[   5]---> Adder-cost: 2052   maxlim: 4999   bits: 14/13
c ---[   4]---> Adder-cost: 2306   maxlim: 11999   bits: 15/14
c ---[   2]---> Adder-cost: 1315   maxlim: 1199   bits: 12/11
c ---[   1]---> Adder-cost: 1522   maxlim: 2099   bits: 13/12
c ---[   0]---> Adder-cost: 1797   maxlim: 3999   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   76857   275259 |   25619       0        0     nan |  0.000 % |
c |       100 |   76857   275259 |   28180     100      349     3.5 |  0.295 % |
c |       250 |   76857   275259 |   30998     250      989     4.0 |  0.295 % |
c |       475 |   76857   275259 |   34098     475     2362     5.0 |  0.295 % |
c |       812 |   76857   275259 |   37508     812     5564     6.9 |  0.295 % |
c |      1318 |   76857   275259 |   41259    1318     9284     7.0 |  0.295 % |
c |      2078 |   76857   275259 |   45385    2078    19038     9.2 |  0.295 % |
c ==============================================================================
c [1mFound solution: 1931[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1828   maxlim: 21623   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2678 |   89543   320552 |   29847    2678    24935     9.3 |  0.295 % |
c |      2778 |   89543   320552 |   32831    2778    26152     9.4 |  0.337 % |
c |      2929 |   89543   320552 |   36114    2929    27633     9.4 |  0.337 % |
c |      3154 |   89543   320552 |   39726    3154    29393     9.3 |  0.337 % |
c |      3491 |   89543   320552 |   43698    3491    32994     9.5 |  0.337 % |
c |      3997 |   89543   320552 |   48068    3997    37843     9.5 |  0.337 % |
c |      4756 |   89543   320552 |   52875    4756    49159    10.3 |  0.337 % |
c |      5897 |   89543   320552 |   58163    5897   168561    28.6 |  0.337 % |
c |      7605 |   89510   320441 |   63979    7600   178160    23.4 |  0.382 % |
c |     10168 |   89510   320441 |   70377   10163   226253    22.3 |  0.382 % |
c |     14012 |   89510   320441 |   77415   14007   371624    26.5 |  0.382 % |
c |     19778 |   89510   320441 |   85156   19773   607932    30.7 |  0.382 % |
c |     28428 |   89510   320441 |   93672   28423  1292382    45.5 |  0.382 % |
c |     41403 |   89510   320441 |  103039   41398  2357260    56.9 |  0.382 % |
c ==============================================================================
c [1mFound solution: 1848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21706   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54059 |   89531   320545 |   29843   54054  3961992    73.3 |  0.382 % |
c |     54162 |   89531   320545 |   32827   15292  1592576   104.1 |  0.420 % |
c |     54312 |   89531   320545 |   36110   15442  1593483   103.2 |  0.420 % |
c |     54537 |   89531   320545 |   39721   15667  1596982   101.9 |  0.420 % |
c |     54875 |   89531   320545 |   43693   16005  1602668   100.1 |  0.420 % |
c |     55381 |   89531   320545 |   48062   16511  1613704    97.7 |  0.420 % |
c |     56143 |   89531   320545 |   52868   17273  1650155    95.5 |  0.420 % |
c |     57282 |   89531   320545 |   58155   18412  1696606    92.1 |  0.420 % |
c |     58991 |   89531   320545 |   63971   20121  1829381    90.9 |  0.420 % |
c |     61553 |   89531   320545 |   70368   22683  1980310    87.3 |  0.420 % |
c |     65398 |   89531   320545 |   77405   26528  2168363    81.7 |  0.420 % |
c ==============================================================================
c [1mFound solution: 1769[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21785   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70558 |   89538   320589 |   29846   31688  2707051    85.4 |  0.420 % |
c |     70660 |   89538   320589 |   32830   15536   898016    57.8 |  0.449 % |
c |     70810 |   89538   320589 |   36113   15686   900279    57.4 |  0.449 % |
c |     71035 |   89529   320558 |   39725   15901   904385    56.9 |  0.457 % |
c |     71372 |   89529   320558 |   43697   16238   915276    56.4 |  0.457 % |
c |     71880 |   89529   320558 |   48067   16746   927203    55.4 |  0.457 % |
c |     72639 |   89529   320558 |   52874   17505   959636    54.8 |  0.457 % |
c |     73779 |   89529   320558 |   58161   18645  1023755    54.9 |  0.457 % |
c |     75487 |   89529   320558 |   63977   20353  1113996    54.7 |  0.457 % |
c |     78049 |   89529   320558 |   70375   22915  1190720    52.0 |  0.457 % |
c |     81894 |   89529   320558 |   77412   26760  1574240    58.8 |  0.457 % |
c |     87661 |   89529   320558 |   85154   32527  1806448    55.5 |  0.457 % |
c |     96312 |   89529   320558 |   93669   41178  2513161    61.0 |  0.457 % |
c |    109286 |   89529   320558 |  103036   54152  3635289    67.1 |  0.457 % |
c |    128747 |   89529   320558 |  113340   73613  5739322    78.0 |  0.457 % |
c ==============================================================================
c [1mFound solution: 1739[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21815   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133466 |   89533   320587 |   29844   78332  6147778    78.5 |  0.457 % |
c |    133567 |   89533   320587 |   32828   18672  1409334    75.5 |  0.479 % |
c |    133717 |   89533   320587 |   36111   18822  1410854    75.0 |  0.479 % |
c |    133942 |   89524   320556 |   39722   19041  1414922    74.3 |  0.487 % |
c |    134279 |   89524   320556 |   43694   19378  1422933    73.4 |  0.487 % |
c |    134788 |   89498   320466 |   48064   19875  1449674    72.9 |  0.517 % |
c |    135547 |   89498   320466 |   52870   20634  1490582    72.2 |  0.517 % |
c |    136686 |   89498   320466 |   58157   21773  1505141    69.1 |  0.517 % |
c |    138396 |   89498   320466 |   63973   23483  1570444    66.9 |  0.517 % |
c |    140960 |   89498   320466 |   70370   26047  1682244    64.6 |  0.517 % |
c |    144804 |   89498   320466 |   77407   29891  1991777    66.6 |  0.517 % |
c |    150570 |   89498   320466 |   85148   35657  2263637    63.5 |  0.517 % |
c |    159219 |   89498   320466 |   93663   44306  2944918    66.5 |  0.517 % |
c |    172196 |   89498   320466 |  103029   57283  4042943    70.6 |  0.517 % |
c |    191659 |   89498   320466 |  113332   76746  5737800    74.8 |  0.517 % |
c ==============================================================================
c [1mFound solution: 946[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22608   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    196345 |   89445   320200 |   29815   63587  4160391    65.4 |  0.517 % |
c |    196445 |   89445   320200 |   32796   14131   678279    48.0 |  0.621 % |
c |    196596 |   89445   320200 |   36076   14282   680874    47.7 |  0.621 % |
c |    196821 |   89445   320200 |   39683   14507   688020    47.4 |  0.621 % |
c |    197158 |   89445   320200 |   43652   14844   710964    47.9 |  0.621 % |
c |    197664 |   89445   320200 |   48017   15350   728038    47.4 |  0.621 % |
c |    198423 |   89445   320200 |   52819   16109   791575    49.1 |  0.621 % |
c |    199563 |   89445   320200 |   58101   17249   880814    51.1 |  0.621 % |
c |    201271 |   89445   320200 |   63911   18957  1016739    53.6 |  0.621 % |
c |    203833 |   89445   320200 |   70302   21519  1242229    57.7 |  0.621 % |
c |    207677 |   89445   320200 |   77332   25363  1594865    62.9 |  0.621 % |
c |    213445 |   89445   320200 |   85065   31131  2149941    69.1 |  0.621 % |
c |    222096 |   89445   320200 |   93572   39782  3063330    77.0 |  0.621 % |
c |    235070 |   89445   320200 |  102929   52756  4470065    84.7 |  0.621 % |
c ==============================================================================
c [1mFound solution: 911[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22643   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    251560 |   89450   320229 |   29816   69246  6339367    91.5 |  0.621 % |
c |    251660 |   89450   320229 |   32797   18390  1432400    77.9 |  0.643 % |
c |    251810 |   89450   320229 |   36077   18540  1436537    77.5 |  0.644 % |
c |    252040 |   89450   320229 |   39685   18770  1451042    77.3 |  0.643 % |
c |    252378 |   89450   320229 |   43653   19108  1466905    76.8 |  0.643 % |
c |    252885 |   89450   320229 |   48018   19615  1504665    76.7 |  0.643 % |
c |    253644 |   89450   320229 |   52820   20374  1560056    76.6 |  0.643 % |
c |    254783 |   89450   320229 |   58102   21513  1654788    76.9 |  0.643 % |
c |    256493 |   89450   320229 |   63913   23223  1785510    76.9 |  0.643 % |
c |    259055 |   89450   320229 |   70304   25785  1958197    75.9 |  0.643 % |
c |    262900 |   89450   320229 |   77335   29630  2239296    75.6 |  0.643 % |
c |    268666 |   89450   320229 |   85068   35396  2714258    76.7 |  0.643 % |
c |    277315 |   89450   320229 |   93575   44045  3376127    76.7 |  0.643 % |
c ==============================================================================
c [1mFound solution: 770[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22784   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    279769 |   89453   320247 |   29817   46499  3620727    77.9 |  0.643 % |
c |    279869 |   89427   320157 |   32798   16830  1006352    59.8 |  0.688 % |
c |    280019 |   89427   320157 |   36078   16980  1012513    59.6 |  0.688 % |
c |    280248 |   89427   320157 |   39686   17209  1028073    59.7 |  0.688 % |
c |    280588 |   89427   320157 |   43655   17549  1053941    60.1 |  0.688 % |
c |    281097 |   89341   319859 |   48020   18011  1088494    60.4 |  0.793 % |
c |    281856 |   89341   319859 |   52822   18770  1143730    60.9 |  0.793 % |
c |    282995 |   89341   319859 |   58104   19909  1244248    62.5 |  0.793 % |
c ==============================================================================
c [1mFound solution: 749[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22805   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    284349 |   89348   319898 |   29782   21263  1345616    63.3 |  0.793 % |
c |    284450 |   89348   319898 |   32760   21364  1352753    63.3 |  0.815 % |
c |    284604 |   89348   319898 |   36036   21518  1361183    63.3 |  0.815 % |
c |    284829 |   89348   319898 |   39639   21743  1377474    63.4 |  0.815 % |
c |    285166 |   89348   319898 |   43603   22080  1390687    63.0 |  0.815 % |
c |    285672 |   89348   319898 |   47964   22586  1414527    62.6 |  0.815 % |
c ==============================================================================
c [1mFound solution: 741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22813   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    286300 |   89352   319930 |   29784   23214  1454021    62.6 |  0.815 % |
c |    286400 |   89352   319930 |   32762   23314  1458066    62.5 |  0.837 % |
c |    286551 |   89352   319930 |   36038   23465  1467784    62.6 |  0.837 % |
c |    286776 |   89352   319930 |   39642   23690  1481349    62.5 |  0.837 % |
c |    287116 |   89352   319930 |   43606   24030  1500314    62.4 |  0.837 % |
c |    287622 |   89352   319930 |   47967   24536  1529161    62.3 |  0.837 % |
c |    288382 |   89352   319930 |   52764   25296  1584096    62.6 |  0.837 % |
c |    289521 |   89352   319930 |   58040   26435  1669747    63.2 |  0.837 % |
c |    291229 |   89352   319930 |   63844   28143  1799237    63.9 |  0.837 % |
c |    293792 |   89352   319930 |   70229   30706  1972225    64.2 |  0.837 % |
c |    297636 |   89352   319930 |   77252   34550  2247972    65.1 |  0.837 % |
c |    303402 |   89352   319930 |   84977   40316  2660851    66.0 |  0.837 % |
c |    312052 |   89352   319930 |   93474   48966  3274473    66.9 |  0.837 % |
c |    325028 |   89352   319930 |  102822   61942  4241149    68.5 |  0.837 % |
c ==============================================================================
c [1mFound solution: 689[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22865   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    328455 |   89356   319957 |   29785   65369  4571282    69.9 |  0.837 % |
c |    328557 |   89356   319957 |   32763   18757  1074267    57.3 |  0.859 % |
c |    328708 |   89356   319957 |   36039   18908  1086451    57.5 |  0.859 % |
c |    328935 |   89356   319957 |   39643   19135  1100616    57.5 |  0.859 % |
c |    329272 |   89356   319957 |   43608   19472  1127436    57.9 |  0.859 % |
c |    329782 |   89356   319957 |   47969   19982  1166638    58.4 |  0.859 % |
c |    330542 |   89356   319957 |   52765   20742  1214476    58.6 |  0.859 % |
c |    331681 |   89356   319957 |   58042   21881  1299360    59.4 |  0.859 % |
c |    333390 |   89356   319957 |   63846   23590  1448384    61.4 |  0.859 % |
c |    335955 |   89356   319957 |   70231   26155  1643941    62.9 |  0.859 % |
c ==============================================================================
c [1mFound solution: 681[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22873   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    338761 |   89360   319980 |   29786   28961  1945896    67.2 |  0.859 % |
c |    338862 |   89360   319980 |   32764   29062  1947465    67.0 |  0.874 % |
c |    339012 |   89360   319980 |   36041   29212  1953623    66.9 |  0.874 % |
c |    339237 |   89360   319980 |   39645   29437  1975036    67.1 |  0.874 % |
c |    339574 |   89360   319980 |   43609   29774  1988516    66.8 |  0.874 % |
c |    340080 |   89360   319980 |   47970   30280  2027818    67.0 |  0.874 % |
c |    340839 |   89360   319980 |   52767   31039  2085626    67.2 |  0.874 % |
c ==============================================================================
c [1mFound solution: 657[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22897   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    341314 |   89366   320012 |   29788   31514  2129230    67.6 |  0.874 % |
c |    341414 |   89366   320012 |   32766   15857   930079    58.7 |  0.896 % |
c |    341564 |   89366   320012 |   36043   16007   946090    59.1 |  0.896 % |
c |    341789 |   89366   320012 |   39647   16232   967115    59.6 |  0.896 % |
c |    342127 |   89366   320012 |   43612   16570   997471    60.2 |  0.896 % |
c |    342633 |   89366   320012 |   47973   17076  1035864    60.7 |  0.896 % |
c |    343394 |   89366   320012 |   52771   17837  1106067    62.0 |  0.896 % |
c ==============================================================================
c [1mFound solution: 636[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22918   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    343979 |   89371   320052 |   29790   18422  1157747    62.8 |  0.896 % |
c |    344081 |   89371   320052 |   32769   18524  1160795    62.7 |  0.926 % |
c |    344231 |   89371   320052 |   36045   18674  1169790    62.6 |  0.926 % |
c |    344459 |   89371   320052 |   39650   18902  1185454    62.7 |  0.926 % |
c |    344797 |   89371   320052 |   43615   19240  1215432    63.2 |  0.926 % |
c |    345303 |   89371   320052 |   47977   19746  1248021    63.2 |  0.926 % |
c |    346062 |   89371   320052 |   52774   20505  1318239    64.3 |  0.926 % |
c ==============================================================================
c [1mFound solution: 635[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22919   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    347023 |   89373   320063 |   29791   21466  1395363    65.0 |  0.926 % |
c |    347123 |   89373   320063 |   32770   21566  1399600    64.9 |  0.933 % |
c |    347275 |   89373   320063 |   36047   21718  1410545    64.9 |  0.933 % |
c |    347501 |   89373   320063 |   39651   21944  1431487    65.2 |  0.933 % |
c |    347839 |   89373   320063 |   43617   22282  1446347    64.9 |  0.933 % |
c |    348347 |   89373   320063 |   47978   22790  1487027    65.2 |  0.933 % |
c |    349106 |   89373   320063 |   52776   23549  1551551    65.9 |  0.933 % |
c ==============================================================================
c [1mFound solution: 563[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22991   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    349336 |   89376   320079 |   29792   23779  1570821    66.1 |  0.933 % |
c |    349436 |   89376   320079 |   32771   23879  1572338    65.8 |  0.948 % |
c |    349587 |   89376   320079 |   36048   24030  1584564    65.9 |  0.948 % |
c |    349812 |   89376   320079 |   39653   24255  1595306    65.8 |  0.948 % |
c ==============================================================================
c [1mFound solution: 546[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23008   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    349973 |   89330   319927 |   29776   24379  1607855    66.0 |  0.948 % |
c |    350076 |   89330   319927 |   32753   24482  1613253    65.9 |  1.022 % |
c |    350227 |   89330   319927 |   36028   24633  1624363    65.9 |  1.022 % |
c |    350454 |   89330   319927 |   39631   24860  1638779    65.9 |  1.022 % |
c |    350791 |   89330   319927 |   43595   25197  1660811    65.9 |  1.022 % |
c |    351297 |   89330   319927 |   47954   25703  1706767    66.4 |  1.022 % |
c |    352058 |   89330   319927 |   52750   26464  1768930    66.8 |  1.022 % |
c ==============================================================================
c [1mFound solution: 520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23034   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    352787 |   89338   319969 |   29779   27193  1832145    67.4 |  1.022 % |
c |    352887 |   89338   319969 |   32756   27293  1835973    67.3 |  1.051 % |
c |    353037 |   89338   319969 |   36032   27443  1851592    67.5 |  1.051 % |
c |    353263 |   89338   319969 |   39635   27669  1862417    67.3 |  1.051 % |
c |    353600 |   89338   319969 |   43599   28006  1873654    66.9 |  1.051 % |
c |    354106 |   89338   319969 |   47959   28512  1912744    67.1 |  1.051 % |
c |    354865 |   89338   319969 |   52755   29271  1963916    67.1 |  1.051 % |
c |    356004 |   89338   319969 |   58030   30410  2080531    68.4 |  1.051 % |
c |    357712 |   89338   319969 |   63833   32118  2225201    69.3 |  1.051 % |
c |    360276 |   89338   319969 |   70217   34682  2431286    70.1 |  1.051 % |
c |    364123 |   89338   319969 |   77239   38529  2599173    67.5 |  1.051 % |
c ==============================================================================
c [1mFound solution: 480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23074   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    364642 |   89281   319630 |   29760   33995  2124305    62.5 |  1.051 % |
c |    364744 |   89281   319630 |   32736   17100   816807    47.8 |  1.148 % |
c ==============================================================================
c [1mFound solution: 420[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23134   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    364775 |   89293   319683 |   29764   17131   820083    47.9 |  1.148 % |
c |    364875 |   89293   319683 |   32740   17231   823221    47.8 |  1.191 % |
c |    365025 |   89293   319683 |   36014   17381   839441    48.3 |  1.191 % |
c |    365251 |   89293   319683 |   39615   17607   854651    48.5 |  1.191 % |
c |    365588 |   89293   319683 |   43577   17944   879981    49.0 |  1.191 % |
c |    366097 |   89293   319683 |   47935   18453   907479    49.2 |  1.191 % |
c |    366856 |   89293   319683 |   52728   19212   939227    48.9 |  1.191 % |
c |    367995 |   89293   319683 |   58001   20351   990808    48.7 |  1.191 % |
c |    369705 |   89293   319683 |   63801   22061  1077728    48.9 |  1.191 % |
c ==============================================================================
c [1mFound solution: 416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23138   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    371892 |   89299   319710 |   29766   24248  1354947    55.9 |  1.191 % |
c |    371992 |   89299   319710 |   32742   24348  1356814    55.7 |  1.213 % |
c |    372146 |   89299   319710 |   36016   24502  1373796    56.1 |  1.213 % |
c |    372373 |   89299   319710 |   39618   24729  1377921    55.7 |  1.213 % |
c |    372710 |   89299   319710 |   43580   25066  1380528    55.1 |  1.213 % |
c |    373221 |   89299   319710 |   47938   25577  1432054    56.0 |  1.213 % |
c |    373980 |   89299   319710 |   52732   26336  1501098    57.0 |  1.213 % |
c |    375119 |   89299   319710 |   58005   27475  1638401    59.6 |  1.213 % |
c ==============================================================================
c [1mFound solution: 413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23141   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    375458 |   89303   319730 |   29767   27814  1668063    60.0 |  1.213 % |
c |    375561 |   89303   319730 |   32743   27917  1672575    59.9 |  1.228 % |
c |    375713 |   89303   319730 |   36018   28069  1677890    59.8 |  1.228 % |
c |    375938 |   89303   319730 |   39619   28294  1700111    60.1 |  1.228 % |
c |    376275 |   89303   319730 |   43581   28631  1721049    60.1 |  1.228 % |
c |    376783 |   89303   319730 |   47940   29139  1748205    60.0 |  1.228 % |
c |    377542 |   89303   319730 |   52734   29898  1852194    62.0 |  1.228 % |
c |    378681 |   89303   319730 |   58007   31037  1926161    62.1 |  1.228 % |
c ==============================================================================
c [1mFound solution: 391[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23163   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    379305 |   89309   319753 |   29769   31661  1997107    63.1 |  1.228 % |
c |    379405 |   89309   319753 |   32745   15931   987289    62.0 |  1.249 % |
c |    379555 |   89309   319753 |   36020   16081  1004207    62.4 |  1.249 % |
c |    379780 |   89309   319753 |   39622   16306  1021903    62.7 |  1.249 % |
c |    380118 |   89309   319753 |   43584   16644  1068892    64.2 |  1.249 % |
c |    380624 |   89309   319753 |   47943   17150  1124282    65.6 |  1.249 % |
c |    381384 |   89309   319753 |   52737   17910  1177065    65.7 |  1.249 % |
c |    382527 |   89309   319753 |   58011   19053  1260747    66.2 |  1.249 % |
c ==============================================================================
c [1mFound solution: 383[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23171   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    382559 |   89312   319765 |   29770   19085  1263820    66.2 |  1.249 % |
c |    382660 |   89312   319765 |   32747   19186  1279973    66.7 |  1.264 % |
c |    382811 |   89312   319765 |   36021   19337  1281662    66.3 |  1.264 % |
c |    383036 |   89312   319765 |   39623   19562  1283347    65.6 |  1.264 % |
c |    383373 |   89312   319765 |   43586   19899  1286470    64.6 |  1.264 % |
c |    383879 |   89303   319734 |   47944   20374  1292598    63.4 |  1.271 % |
c |    384638 |   89303   319734 |   52739   21133  1426918    67.5 |  1.271 % |
c |    385777 |   89303   319734 |   58013   22272  1442431    64.8 |  1.271 % |
c |    387487 |   89303   319734 |   63814   23982  1652277    68.9 |  1.271 % |
c |    390053 |   89303   319734 |   70196   26548  1847144    69.6 |  1.271 % |
c |    393901 |   89303   319734 |   77215   30396  2175956    71.6 |  1.271 % |
c ==============================================================================
c [1mFound solution: 379[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23175   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    396154 |   89305   319742 |   29768   32649  2348259    71.9 |  1.271 % |
c |    396255 |   89305   319742 |   32744   16426   957663    58.3 |  1.279 % |
c |    396406 |   89305   319742 |   36019   16577   968527    58.4 |  1.279 % |
c |    396631 |   89305   319742 |   39621   16802   981575    58.4 |  1.279 % |
c |    396968 |   89305   319742 |   43583   17139  1003150    58.5 |  1.279 % |
c |    397475 |   89305   319742 |   47941   17646  1038658    58.9 |  1.279 % |
c ==============================================================================
c [1mFound solution: 377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23177   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    398085 |   89307   319752 |   29769   18256  1129253    61.9 |  1.279 % |
c |    398186 |   89307   319752 |   32745   18357  1130922    61.6 |  1.286 % |
c |    398339 |   89307   319752 |   36020   18510  1154631    62.4 |  1.286 % |
c |    398566 |   89307   319752 |   39622   18737  1170433    62.5 |  1.286 % |
c |    398905 |   89307   319752 |   43584   19076  1225864    64.3 |  1.286 % |
c |    399412 |   89307   319752 |   47943   19583  1307495    66.8 |  1.286 % |
c |    400171 |   89307   319752 |   52737   20342  1394079    68.5 |  1.286 % |
c ==============================================================================
c [1mFound solution: 375[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23179   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    400829 |   89308   319760 |   29769   21000  1479193    70.4 |  1.286 % |
c |    400929 |   89308   319760 |   32745   21100  1491899    70.7 |  1.293 % |
c |    401080 |   89308   319760 |   36020   21251  1511648    71.1 |  1.293 % |
c |    401305 |   89308   319760 |   39622   21476  1514293    70.5 |  1.293 % |
c |    401643 |   89222   319462 |   43584   21776  1525877    70.1 |  1.397 % |
c |    402150 |   89222   319462 |   47943   22283  1553678    69.7 |  1.397 % |
c |    402913 |   89222   319462 |   52737   23046  1660939    72.1 |  1.397 % |
c |    404052 |   89222   319462 |   58011   24185  1951488    80.7 |  1.397 % |
c |    405760 |   89222   319462 |   63812   25893  2007780    77.5 |  1.397 % |
c |    408322 |   89222   319462 |   70193   28455  2637423    92.7 |  1.397 % |
c |    412166 |   89222   319462 |   77213   32299  2783887    86.2 |  1.397 % |
c |    417938 |   89222   319462 |   84934   38071  3926319   103.1 |  1.397 % |
c ==============================================================================
c [1mFound solution: 371[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23183   bits: 15/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    426578 |   89224   319470 |   29741   46711  6220556   133.2 |  1.397 % |
c |    426678 |   89224   319470 |   32715   16779  3072475   183.1 |  1.404 % |
c |    426828 |   89224   319470 |   35986   16929  3075611   181.7 |  1.404 % |
c |    427055 |   89224   319470 |   39585   17156  3079240   179.5 |  1.404 % |
c |    427392 |   89224   319470 |   43543   17493  3088913   176.6 |  1.404 % |
c |    427898 |   89224   319470 |   47898   17999  3093916   171.9 |  1.404 % |
c |    428657 |   89224   319470 |   52687   18758  3106406   165.6 |  1.404 % |
c |    429797 |   89189   319349 |   57956   19885  3128940   157.4 |  1.442 % |
c |    431505 |   89189   319349 |   63752   21593  3412504   158.0 |  1.442 % |
c |    434069 |   89175   319301 |   70127   24154  3816541   158.0 |  1.464 % |
c |    437914 |   89098   319034 |   77140   27975  4441778   158.8 |  1.561 % |
c |    443684 |   89040   318834 |   84854   33726  5149734   152.7 |  1.627 % |
c |    452334 |   88999   318693 |   93339   42368  6815244   160.9 |  1.672 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 -C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 -C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 -C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 -C86_0x2e__bit0 -C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 -C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 -C112_0x2e__bit0 -C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 C118_0x2e__bit0 -C119_0x2e__bit0 -C120_0x2e__bit0 -C121_0x2e__bit0 -C122_0x2e__bit0 -C123_0x2e__bit0 C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 -C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 -C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172_0x2e__bit0 -C173_0x2e__bit0 -C174_0x2e__bit0 -C175_0x2e__bit0 -C176_0x2e__bit0 -C177_0x2e__bit0 -C178_0x2e__bit0 -C179_0x2e__bit0 -C180_0x2e__bit0 -C181_0x2e__bit0 -C182_0x2e__bit0 -C183_0x2e__bit0 -C184_0x2e__bit0 -C185_0x2e__bit0 -C186_0x2e__bit0 -C187_0x2e__bit0 -C188_0x2e__bit0 -C189_0x2e__bit0 -C190_0x2e__bit0 -C191_0x2e__bit0 -C192_0x2e__bit0 -C193_0x2e__bit0 -C194_0x2e__bit0 -C195_0x2e__bit0 -C196_0x2e__bit0 -C197_0x2e__bit0 -C198_0x2e__bit0 -C199_0x2e__bit0 -C200_0x2e__bit0 -C201_0x2e__bit0 -C202_0x2e__bit0 -C203_0x2e__bit0 -C204_0x2e__bit0 -C205_0x2e__bit0 -C206_0x2e__bit0 -C207_0x2e__bit0 -C208_0x2e__bit0 -C209_0x2e__bit0 -C210_0x2e__bit0 -C211_0x2e__bit0 -C212_0x2e__bit0 -C213_0x2e__bit0 -C214_0x2e__bit0 -C215_0x2e__bit0 -C216_0x2e__bit0 -C217_0x2e__bit0 -C218_0x2e__bit0 -C219_0x2e__bit0 -C220_0x2e__bit0 -C221_0x2e__bit0 -C222_0x2e__bit0 -C223_0x2e__bit0 -C224_0x2e__bit0 -C225_0x2e__bit0 -C226_0x2e__bit0 -C227_0x2e__bit0 -C228_0x2e__bit0 -C229_0x2e__bit0 -C230_0x2e__bit0 -C231_0x2e__bit0 -C232_0x2e__bit0 -C233_0x2e__bit0 -C234_0x2e__bit0 -C235_0x2e__bit0 -C236_0x2e__bit0 -C237_0x2e__bit0 -C238_0x2e__bit0 -C239_0x2e__bit0 -C240_0x2e__bit0 -C241_0x2e__bit0 -C242_0x2e__bit0 -C243_0x2e__bit0 -C244_0x2e__bit0 -C245_0x2e__bit0 -C246_0x2e__bit0 -C2#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 15172
Raw data (stat): 15172 (runsolver) R 15171 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550082303 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0009 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 2391 0 0 0 992 6 0 0 25 0 1 0 550082303 11661312 2362 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2847 2362 603 41 0 2806 0
vsize: 11388
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 3170 0 0 0 1989 8 0 0 25 0 1 0 550082303 14888960 3141 4294967295 134512640 134672761 3221224544 3221223544 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3635 3141 603 41 0 3594 0
vsize: 14540
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 3876 0 0 0 2987 10 0 0 25 0 1 0 550082303 17842176 3847 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4356 3847 603 41 0 4315 0
vsize: 17424
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 4452 0 0 0 3985 13 0 0 25 0 1 0 550082303 20127744 4423 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4914 4423 603 41 0 4873 0
vsize: 19656
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 5066 0 0 0 4984 14 0 0 25 0 1 0 550082303 22675456 5037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5536 5037 603 41 0 5495 0
vsize: 22144
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 5717 0 0 0 5982 16 0 0 25 0 1 0 550082303 25354240 5688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6190 5688 603 41 0 6149 0
vsize: 24760
[startup+70.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6313 0 0 0 6980 18 0 0 25 0 1 0 550082303 27774976 6284 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6781 6284 603 41 0 6740 0
vsize: 27124
[startup+80.0024 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6338 0 0 0 7980 18 0 0 25 0 1 0 550082303 27930624 6309 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6309 603 41 0 6778 0
vsize: 27276
[startup+90.0021 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6338 0 0 0 8980 18 0 0 25 0 1 0 550082303 27930624 6309 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6309 603 41 0 6778 0
vsize: 27276
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6339 0 0 0 9980 18 0 0 25 0 1 0 550082303 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6339 0 0 0 10980 19 0 0 25 0 1 0 550082303 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6339 0 0 0 11980 19 0 0 25 0 1 0 550082303 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6339 0 0 0 12981 19 0 0 25 0 1 0 550082303 27930624 6310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6339 0 0 0 13981 19 0 0 25 0 1 0 550082303 27930624 6310 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6358 0 0 0 14981 19 0 0 25 0 1 0 550082303 27930624 6329 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6329 603 41 0 6778 0
vsize: 27276
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 6774 0 0 0 15980 20 0 0 25 0 1 0 550082303 29663232 6745 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7242 6745 603 41 0 7201 0
vsize: 28968
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 7098 0 0 0 16980 20 0 0 25 0 1 0 550082303 30986240 7069 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7565 7069 603 41 0 7524 0
vsize: 30260
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 7475 0 0 0 17980 21 0 0 25 0 1 0 550082303 32718848 7446 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7988 7446 603 41 0 7947 0
vsize: 31952
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 7877 0 0 0 18979 22 0 0 25 0 1 0 550082303 34316288 7848 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8378 7848 603 41 0 8337 0
vsize: 33512
[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8243 0 0 0 19979 23 0 0 25 0 1 0 550082303 35909632 8214 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8767 8214 603 41 0 8726 0
vsize: 35068
[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8625 0 0 0 20978 24 0 0 25 0 1 0 550082303 37384192 8596 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9127 8597 603 41 0 9086 0
vsize: 36508
[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8931 0 0 0 21978 24 0 0 25 0 1 0 550082303 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8931 0 0 0 22978 25 0 0 25 0 1 0 550082303 38592512 8902 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8931 0 0 0 23978 25 0 0 25 0 1 0 550082303 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8931 0 0 0 24978 25 0 0 25 0 1 0 550082303 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8931 0 0 0 25978 25 0 0 25 0 1 0 550082303 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8902 603 41 0 9381 0
vsize: 37688
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8932 0 0 0 26978 25 0 0 25 0 1 0 550082303 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8932 0 0 0 27978 25 0 0 25 0 1 0 550082303 38592512 8903 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8932 0 0 0 28978 25 0 0 25 0 1 0 550082303 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8932 0 0 0 29979 25 0 0 25 0 1 0 550082303 38592512 8903 4294967295 134512640 134672761 3221224544 3221223728 134558947 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8932 0 0 0 30979 25 0 0 25 0 1 0 550082303 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8932 0 0 0 31979 25 0 0 25 0 1 0 550082303 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 8932 0 0 0 32979 25 0 0 25 0 1 0 550082303 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+340.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9013 0 0 0 33979 25 0 0 25 0 1 0 550082303 38998016 8984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9521 8984 603 41 0 9480 0
vsize: 38084
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9285 0 0 0 34978 26 0 0 25 0 1 0 550082303 40071168 9256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9783 9256 603 41 0 9742 0
vsize: 39132
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 35978 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 36979 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 37979 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 38978 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 39978 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 40978 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 41979 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 42979 26 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 43979 27 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 44979 27 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 45979 27 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 46979 27 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9310 0 0 0 47980 27 0 0 25 0 1 0 550082303 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 9281 603 41 0 9775 0
vsize: 39264
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9529 0 0 0 48979 27 0 0 25 0 1 0 550082303 41148416 9500 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10046 9500 603 41 0 10005 0
vsize: 40184
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9587 0 0 0 49980 27 0 0 25 0 1 0 550082303 41283584 9558 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9558 603 41 0 10038 0
vsize: 40316
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9587 0 0 0 50980 27 0 0 25 0 1 0 550082303 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9558 603 41 0 10038 0
vsize: 40316
[startup+520.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9588 0 0 0 51980 27 0 0 25 0 1 0 550082303 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9588 0 0 0 52980 27 0 0 25 0 1 0 550082303 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9588 0 0 0 53980 27 0 0 25 0 1 0 550082303 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9588 0 0 0 54980 27 0 0 25 0 1 0 550082303 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9588 0 0 0 55981 27 0 0 25 0 1 0 550082303 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9559 603 41 0 10038 0
vsize: 40316
[startup+570.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 56981 27 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 57981 27 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+590.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 58981 27 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+600.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 59981 27 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+610.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 60981 27 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 61981 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 62982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+640.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 63982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 64982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 65982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 66982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 67982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 68982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+700.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 69982 28 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 70982 29 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 71982 29 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+730.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 72982 29 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9590 0 0 0 73982 29 0 0 25 0 1 0 550082303 41283584 9561 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+750.027 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9591 0 0 0 74982 29 0 0 25 0 1 0 550082303 41283584 9562 4294967295 134512640 134672761 3221224544 3221223692 1074733101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+760.027 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9591 0 0 0 75982 29 0 0 25 0 1 0 550082303 41283584 9562 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+770.026 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9591 0 0 0 76982 29 0 0 25 0 1 0 550082303 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+780.026 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9591 0 0 0 77982 29 0 0 25 0 1 0 550082303 41283584 9562 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+790.026 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9591 0 0 0 78982 29 0 0 25 0 1 0 550082303 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+800.025 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9591 0 0 0 79982 29 0 0 25 0 1 0 550082303 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+810.026 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 80982 29 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+820.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 81983 29 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+830.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 82983 30 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+840.024 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 83983 30 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+850.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 84983 30 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+860.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 85983 30 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+870.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 86983 30 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+880.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9592 0 0 0 87983 30 0 0 25 0 1 0 550082303 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+890.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 88983 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+900.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 89984 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+910.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 90984 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+920.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 91984 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+930.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 92984 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+940.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 93984 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+950.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 94984 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+960.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 95985 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223728 134559033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+970.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 96985 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+980.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9593 0 0 0 97985 30 0 0 25 0 1 0 550082303 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+990.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9603 0 0 0 98985 30 0 0 25 0 1 0 550082303 41418752 9574 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10112 9574 603 41 0 10071 0
vsize: 40448
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 99984 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 100985 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 101985 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 102985 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223728 134559291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 103985 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 104985 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 105985 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 106986 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 107986 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9886 0 0 0 108986 31 0 0 25 0 1 0 550082303 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 9887 0 0 0 109986 31 0 0 25 0 1 0 550082303 42606592 9858 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10402 9858 603 41 0 10361 0
vsize: 41608
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 10099 0 0 0 110986 31 0 0 25 0 1 0 550082303 43405312 10070 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10597 10070 603 41 0 10556 0
vsize: 42388
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 10395 0 0 0 111985 32 0 0 25 0 1 0 550082303 44589056 10366 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10886 10366 603 41 0 10845 0
vsize: 43544
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 10643 0 0 0 112985 33 0 0 25 0 1 0 550082303 45629440 10614 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11140 10614 603 41 0 11099 0
vsize: 44560
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 10986 0 0 0 113984 34 0 0 25 0 1 0 550082303 47083520 10957 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11495 10957 603 41 0 11454 0
vsize: 45980
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 11370 0 0 0 114983 35 0 0 25 0 1 0 550082303 48664576 11341 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11881 11341 603 41 0 11840 0
vsize: 47524
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 11741 0 0 0 115982 36 0 0 25 0 1 0 550082303 50118656 11712 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12236 11712 603 41 0 12195 0
vsize: 48944
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 12036 0 0 0 116982 36 0 0 25 0 1 0 550082303 51314688 12007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12528 12007 603 41 0 12487 0
vsize: 50112
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 12302 0 0 0 117981 37 0 0 25 0 1 0 550082303 52375552 12273 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12787 12273 603 41 0 12746 0
vsize: 51148
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 12566 0 0 0 118981 38 0 0 25 0 1 0 550082303 53551104 12537 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13074 12537 603 41 0 13033 0
vsize: 52296
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15172
Raw data (stat): 15172 (minisat+) R 15171 22612 22611 0 -1 0 12926 0 0 0 119980 39 0 0 25 0 1 0 550082303 54984704 12897 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13424 12897 603 41 0 13383 0
vsize: 53696
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 15172
Raw data (stat): 15172 (minisat+) Z 15171 22612 22611 0 -1 12 12929 0 0 0 119980 41 0 0 25 0 1 0 550082303 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.05
CPU time (s): 1200.22
CPU user time (s): 1199.81
CPU system time (s): 0.417936
CPU usage (%): 100.014
Max. virtual memory (Kb): 53696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####