PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.01684
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 19109

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 17:53:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17027 boxname=wulflinc8 idbench=1310 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-mod008.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-mod008.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-mod008.opb
IDLAUNCH: 17027
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        826820 kB
Buffers:         12300 kB
Cached:         173680 kB
SwapCached:          0 kB
Active:          37352 kB
Inactive:       151560 kB
HighTotal:      131008 kB
HighFree:        20832 kB
LowTotal:       903652 kB
LowFree:        805988 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13272 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:14:00 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 17027 7 1200.21 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.85 0.97 0.93 2/54 1667
Raw data (stat): 1667 (runsolver) R 1666 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 475248186 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 2381 0 0 0 992 6 0 0 25 0 1 0 475248186 11526144 2352 4294967295 134512640 134672761 3221224544 3221223760 134557489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2814 2352 603 41 0 2773 0
vsize: 11256
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 3153 0 0 0 1989 8 0 0 25 0 1 0 475248186 14753792 3124 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3602 3124 603 41 0 3561 0
vsize: 14408
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 3848 0 0 0 2987 11 0 0 25 0 1 0 475248186 17707008 3819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4323 3819 603 41 0 4282 0
vsize: 17292
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 4422 0 0 0 3984 13 0 0 25 0 1 0 475248186 19992576 4393 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 5023 0 0 0 4983 15 0 0 25 0 1 0 475248186 22540288 4994 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5503 4994 603 41 0 5462 0
vsize: 22012
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 5664 0 0 0 5981 17 0 0 25 0 1 0 475248186 25088000 5635 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6125 5635 603 41 0 6084 0
vsize: 24500
[startup+70.0026 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6275 0 0 0 6980 18 0 0 25 0 1 0 475248186 27639808 6246 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6748 6246 603 41 0 6707 0
vsize: 26992
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6338 0 0 0 7980 19 0 0 25 0 1 0 475248186 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.0028 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6338 0 0 0 8980 19 0 0 25 0 1 0 475248186 27930624 6309 4294967295 134512640 134672761 3221224544 3221223712 134561154 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.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6339 0 0 0 9980 19 0 0 25 0 1 0 475248186 27930624 6310 4294967295 134512640 134672761 3221224544 3221223728 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6819 6310 603 41 0 6778 0
vsize: 27276
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6339 0 0 0 10979 19 0 0 25 0 1 0 475248186 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.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6339 0 0 0 11980 19 0 0 25 0 1 0 475248186 27930624 6310 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6339 0 0 0 12980 19 0 0 25 0 1 0 475248186 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.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6339 0 0 0 13980 19 0 0 25 0 1 0 475248186 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+150.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6340 0 0 0 14980 19 0 0 25 0 1 0 475248186 27930624 6311 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6819 6311 603 41 0 6778 0
vsize: 27276
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 6708 0 0 0 15979 20 0 0 25 0 1 0 475248186 29392896 6679 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7176 6679 603 41 0 7135 0
vsize: 28704
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 7004 0 0 0 16979 20 0 0 25 0 1 0 475248186 30588928 6975 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7468 6975 603 41 0 7427 0
vsize: 29872
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 7366 0 0 0 17978 22 0 0 25 0 1 0 475248186 32051200 7337 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7825 7337 603 41 0 7784 0
vsize: 31300
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 7767 0 0 0 18976 23 0 0 25 0 1 0 475248186 33918976 7738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8281 7738 603 41 0 8240 0
vsize: 33124
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8143 0 0 0 19975 25 0 0 25 0 1 0 475248186 35508224 8114 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8669 8114 603 41 0 8628 0
vsize: 34676
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8494 0 0 0 20974 27 0 0 25 0 1 0 475248186 36843520 8465 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8995 8465 603 41 0 8954 0
vsize: 35980
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8896 0 0 0 21973 28 0 0 25 0 1 0 475248186 38457344 8867 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9389 8867 603 41 0 9348 0
vsize: 37556
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8931 0 0 0 22973 28 0 0 25 0 1 0 475248186 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+240.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8931 0 0 0 23973 28 0 0 25 0 1 0 475248186 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8931 0 0 0 24973 28 0 0 25 0 1 0 475248186 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8931 0 0 0 25973 28 0 0 25 0 1 0 475248186 38592512 8902 4294967295 134512640 134672761 3221224544 3221223712 134561375 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8931 0 0 0 26973 28 0 0 25 0 1 0 475248186 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+280.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8932 0 0 0 27973 28 0 0 25 0 1 0 475248186 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+290.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8932 0 0 0 28973 28 0 0 25 0 1 0 475248186 38592512 8903 4294967295 134512640 134672761 3221224544 3221223696 134559753 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8932 0 0 0 29974 28 0 0 25 0 1 0 475248186 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8932 0 0 0 30974 28 0 0 25 0 1 0 475248186 38592512 8903 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8932 0 0 0 31974 28 0 0 25 0 1 0 475248186 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8932 0 0 0 32974 28 0 0 25 0 1 0 475248186 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.009 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 8932 0 0 0 33974 28 0 0 25 0 1 0 475248186 38592512 8903 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8903 603 41 0 9381 0
vsize: 37688
[startup+350.008 s]
Raw data (loadavg): 1.14 1.00 0.94 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9173 0 0 0 34974 29 0 0 25 0 1 0 475248186 39665664 9144 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9684 9144 603 41 0 9643 0
vsize: 38736
[startup+360.009 s]
Raw data (loadavg): 1.11 1.00 0.94 2/54 1667
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 35974 29 0 0 25 0 1 0 475248186 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+370.009 s]
Raw data (loadavg): 1.10 1.00 0.94 3/57 1716
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 36974 29 0 0 25 0 1 0 475248186 40206336 9281 4294967295 134512640 134672761 3221224544 3221223648 134560254 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.008 s]
Raw data (loadavg): 1.08 1.00 0.94 2/54 1720
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 37974 29 0 0 25 0 1 0 475248186 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.009 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 1720
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 38974 30 0 0 25 0 1 0 475248186 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+400.009 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 1720
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 39974 30 0 0 25 0 1 0 475248186 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561201 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.009 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 1720
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 40974 30 0 0 25 0 1 0 475248186 40206336 9281 4294967295 134512640 134672761 3221224544 3221223728 134558662 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.009 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 1720
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 41973 30 0 0 25 0 1 0 475248186 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+430.008 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 1720
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 42973 31 0 0 25 0 1 0 475248186 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+440.008 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 1720
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 43973 31 0 0 25 0 1 0 475248186 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+450.008 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 44973 31 0 0 25 0 1 0 475248186 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+460.009 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 45973 32 0 0 25 0 1 0 475248186 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.008 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 46972 32 0 0 25 0 1 0 475248186 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.009 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9310 0 0 0 47972 33 0 0 25 0 1 0 475248186 40206336 9281 4294967295 134512640 134672761 3221224544 3221223712 134561375 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.009 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9367 0 0 0 48972 33 0 0 25 0 1 0 475248186 40472576 9338 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9881 9338 603 41 0 9840 0
vsize: 39524
[startup+500.01 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9587 0 0 0 49971 34 0 0 25 0 1 0 475248186 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.01 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9587 0 0 0 50970 35 0 0 25 0 1 0 475248186 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9587 0 0 0 51970 35 0 0 25 0 1 0 475248186 41283584 9558 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9558 603 41 0 10038 0
vsize: 40316
[startup+530.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9588 0 0 0 52971 35 0 0 25 0 1 0 475248186 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.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9588 0 0 0 53970 35 0 0 25 0 1 0 475248186 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+550.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9588 0 0 0 54970 35 0 0 25 0 1 0 475248186 41283584 9559 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9588 0 0 0 55970 36 0 0 25 0 1 0 475248186 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+570.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 56970 36 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223728 134558662 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.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 57970 36 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 58970 37 0 0 25 0 1 0 475248186 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+600.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 59970 37 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560956 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.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 60970 37 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560858 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.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 61970 37 0 0 25 0 1 0 475248186 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+630.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 62969 38 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223728 134559330 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.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 63969 38 0 0 25 0 1 0 475248186 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.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 64969 38 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560876 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.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 65969 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223648 134555116 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.014 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1722
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 66969 39 0 0 25 0 1 0 475248186 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.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 67969 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+690.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 68969 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+700.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 69969 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+710.013 s]
Raw data (loadavg): 1.07 1.02 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 70969 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+720.013 s]
Raw data (loadavg): 1.06 1.02 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 71970 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+730.013 s]
Raw data (loadavg): 1.05 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 72970 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+740.014 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 73970 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+750.013 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9590 0 0 0 74970 39 0 0 25 0 1 0 475248186 41283584 9561 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10079 9561 603 41 0 10038 0
vsize: 40316
[startup+760.014 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9591 0 0 0 75970 40 0 0 25 0 1 0 475248186 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+770.015 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9591 0 0 0 76970 40 0 0 25 0 1 0 475248186 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+780.015 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9591 0 0 0 77970 40 0 0 25 0 1 0 475248186 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+790.016 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9591 0 0 0 78970 40 0 0 25 0 1 0 475248186 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+800.015 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9591 0 0 0 79971 40 0 0 25 0 1 0 475248186 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+810.016 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9591 0 0 0 80971 40 0 0 25 0 1 0 475248186 41283584 9562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9562 603 41 0 10038 0
vsize: 40316
[startup+820.016 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 81971 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+830.015 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 82971 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+840.016 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 83971 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+850.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 84971 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+860.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 85972 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+870.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 86972 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+880.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 87972 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+890.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 88972 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+900.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9592 0 0 0 89972 40 0 0 25 0 1 0 475248186 41283584 9563 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9563 603 41 0 10038 0
vsize: 40316
[startup+910.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 90972 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+920.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 91973 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+930.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 92973 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+940.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 93973 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+950.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 94973 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+960.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 95973 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+970.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 96973 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+980.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 97974 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+990.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 98974 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9593 0 0 0 99974 40 0 0 25 0 1 0 475248186 41283584 9564 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10079 9564 603 41 0 10038 0
vsize: 40316
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9812 0 0 0 100974 40 0 0 25 0 1 0 475248186 42205184 9783 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10304 9783 603 41 0 10263 0
vsize: 41216
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 101973 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 102974 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 103974 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 104974 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 105974 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 106974 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 107974 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223720 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 108975 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 109975 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9886 0 0 0 110975 41 0 0 25 0 1 0 475248186 42471424 9857 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9857 603 41 0 10328 0
vsize: 41476
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 9910 0 0 0 111975 41 0 0 25 0 1 0 475248186 42606592 9881 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10402 9881 603 41 0 10361 0
vsize: 41608
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 10117 0 0 0 112975 41 0 0 25 0 1 0 475248186 43536384 10088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10629 10088 603 41 0 10588 0
vsize: 42516
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 10411 0 0 0 113974 42 0 0 25 0 1 0 475248186 44716032 10382 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10917 10382 603 41 0 10876 0
vsize: 43668
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 10655 0 0 0 114974 43 0 0 25 0 1 0 475248186 45629440 10626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11140 10626 603 41 0 11099 0
vsize: 44560
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 11009 0 0 0 115973 44 0 0 25 0 1 0 475248186 47083520 10980 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11495 10980 603 41 0 11454 0
vsize: 45980
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 11380 0 0 0 116972 44 0 0 25 0 1 0 475248186 48664576 11351 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11881 11351 603 41 0 11840 0
vsize: 47524
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 11747 0 0 0 117972 45 0 0 25 0 1 0 475248186 50118656 11718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12236 11718 603 41 0 12195 0
vsize: 48944
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 12036 0 0 0 118970 47 0 0 25 0 1 0 475248186 51314688 12007 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12528 12007 603 41 0 12487 0
vsize: 50112
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 1724
Raw data (stat): 1667 (minisat+) R 1666 26667 26666 0 -1 0 12297 0 0 0 119970 47 0 0 25 0 1 0 475248186 52375552 12268 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12787 12268 603 41 0 12746 0
vsize: 51148
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 1724
Raw data (stat): 1667 (minisat+) Z 1666 26667 26666 0 -1 12 12300 0 0 0 119970 50 0 0 25 0 1 0 475248186 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.71
CPU system time (s): 0.501923
CPU usage (%): 100.013
Max. virtual memory (Kb): 51148
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####