PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/sorensson/garden/normalized-g15x15.opb
MD5SUM	6a083b86cc55025d2acb3bcf68562064
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	54
Optimality of the best value was proved	NO
Number of terms in the objective function	225
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	225
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	225
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01784
Number of variables	225
Total number of constraints	225
Number of constraints which are clauses	225
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	5
Trace number 6505

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        718288 kB
Buffers:         38372 kB
Cached:         237504 kB
SwapCached:          0 kB
Active:          84804 kB
Inactive:       193892 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        718036 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32128 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:48:06 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4963 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     225     1065 |      75       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 75[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 442   maxlim: 150   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3278    11957 |    1092       0        0     nan |  0.000 % |
c |       101 |    3278    11957 |    1201     101      458     4.5 |  0.745 % |
c |       251 |    3278    11957 |    1321     251     1299     5.2 |  0.745 % |
c |       476 |    3278    11957 |    1453     476     2464     5.2 |  0.745 % |
c ==============================================================================
c [1mFound solution: 73[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 152   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       743 |    3282    11976 |    1094     743     4406     5.9 |  0.745 % |
c |       843 |    3282    11976 |    1203     843     6163     7.3 |  1.040 % |
c |       993 |    3282    11976 |    1323     993     7720     7.8 |  1.040 % |
c |      1219 |    3282    11976 |    1456    1219    15349    12.6 |  1.040 % |
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 153   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1539 |    3283    11983 |    1094    1539    20227    13.1 |  1.040 % |
c |      1640 |    3283    11983 |    1203     871     9531    10.9 |  1.187 % |
c |      1790 |    3283    11983 |    1323    1021    11527    11.3 |  1.187 % |
c |      2015 |    3283    11983 |    1456    1246    15680    12.6 |  1.187 % |
c ==============================================================================
c [1mFound solution: 71[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 154   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2201 |    3284    11991 |    1094    1432    20256    14.1 |  1.187 % |
c |      2302 |    3284    11991 |    1203     817     7554     9.2 |  1.334 % |
c |      2452 |    3284    11991 |    1323     967     9323     9.6 |  1.334 % |
c |      2677 |    3284    11991 |    1456    1192    13512    11.3 |  1.334 % |
c |      3014 |    3284    11991 |    1601    1529    21311    13.9 |  1.334 % |
c |      3521 |    3284    11991 |    1761    1142    19078    16.7 |  1.334 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 157   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3899 |    3286    12004 |    1095    1520    25676    16.9 |  1.334 % |
c |      4000 |    3286    12004 |    1204     861     6781     7.9 |  1.625 % |
c |      4151 |    3286    12004 |    1324    1012     9373     9.3 |  1.625 % |
c |      4376 |    3286    12004 |    1457    1237    12152     9.8 |  1.625 % |
c ==============================================================================
c [1mFound solution: 67[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 158   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4439 |    3288    12014 |    1096    1300    13060    10.0 |  1.625 % |
c |      4541 |    3288    12014 |    1205     752     5292     7.0 |  1.768 % |
c |      4691 |    3288    12014 |    1326     902     7673     8.5 |  1.768 % |
c |      4919 |    3288    12014 |    1458    1130    13385    11.8 |  1.768 % |
c |      5257 |    3288    12014 |    1604    1468    22211    15.1 |  1.768 % |
c |      5764 |    3288    12014 |    1765    1975    37211    18.8 |  1.768 % |
c |      6523 |    3288    12014 |    1941    1747    39098    22.4 |  1.768 % |
c |      7662 |    3288    12014 |    2135    1787    49138    27.5 |  1.768 % |
c |      9370 |    3288    12014 |    2349    1151    12271    10.7 |  1.768 % |
c |     11932 |    3288    12014 |    2584    2420    76585    31.6 |  1.768 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 159   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12215 |    3289    12017 |    1096    2703    84056    31.1 |  1.768 % |
c |     12316 |    3289    12017 |    1205     777     6910     8.9 |  1.912 % |
c |     12466 |    3289    12017 |    1326     927     9350    10.1 |  1.912 % |
c |     12692 |    3289    12017 |    1458    1153    14593    12.7 |  1.912 % |
c |     13030 |    3289    12017 |    1604    1491    23729    15.9 |  1.912 % |
c |     13536 |    3289    12017 |    1765    1123    14204    12.6 |  1.912 % |
c |     14297 |    3289    12017 |    1941    1884    34332    18.2 |  1.912 % |
c |     15437 |    3289    12017 |    2135    1943    32857    16.9 |  1.912 % |
c |     17146 |    3289    12017 |    2349    1263    19983    15.8 |  1.912 % |
c ==============================================================================
c [1mFound solution: 65[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 160   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17818 |    3295    12043 |    1098    1935    37448    19.4 |  1.912 % |
c |     17920 |    3295    12043 |    1207    1070    13165    12.3 |  2.053 % |
c |     18071 |    3295    12043 |    1328    1221    15962    13.1 |  2.053 % |
c |     18297 |    3295    12043 |    1461    1447    18965    13.1 |  2.053 % |
c |     18634 |    3295    12043 |    1607     943     8569     9.1 |  2.053 % |
c |     19141 |    3295    12043 |    1768    1450    22873    15.8 |  2.053 % |
c |     19900 |    3295    12043 |    1945    1224    18681    15.3 |  2.053 % |
c |     21040 |    3295    12043 |    2139    1244    17463    14.0 |  2.053 % |
c |     22752 |    3295    12043 |    2353    1670    37040    22.2 |  2.053 % |
c |     25315 |    3295    12043 |    2589    1562    41492    26.6 |  2.053 % |
c |     29162 |    3295    12043 |    2847    2497   105384    42.2 |  2.053 % |
c |     34930 |    3295    12043 |    3132    2038    59926    29.4 |  2.053 % |
c |     43582 |    3295    12043 |    3445    2317    63101    27.2 |  2.053 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 161   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44005 |    3296    12050 |    1098    2740    74289    27.1 |  2.053 % |
c |     44105 |    3296    12050 |    1207     785     6652     8.5 |  2.196 % |
c |     44255 |    3296    12050 |    1328     935     8260     8.8 |  2.196 % |
c |     44481 |    3296    12050 |    1461    1161    13250    11.4 |  2.196 % |
c |     44820 |    3296    12050 |    1607    1500    20819    13.9 |  2.196 % |
c |     45328 |    3296    12050 |    1768    1034    10892    10.5 |  2.196 % |
c |     46087 |    3296    12050 |    1945    1793    37455    20.9 |  2.196 % |
c |     47226 |    3296    12050 |    2139    1902    47042    24.7 |  2.196 % |
c |     48935 |    3296    12050 |    2353    1280    31600    24.7 |  2.196 % |
c |     51498 |    3296    12050 |    2589    2575    92257    35.8 |  2.196 % |
c |     55342 |    3296    12050 |    2847    2207    74808    33.9 |  2.196 % |
c |     61109 |    3296    12050 |    3132    1901    91111    47.9 |  2.196 % |
c |     69758 |    3296    12050 |    3445    2284    88397    38.7 |  2.196 % |
c ==============================================================================
c [1mFound solution: 63[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 162   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75718 |    3298    12060 |    1099    2850   103366    36.3 |  2.196 % |
c |     75818 |    3298    12060 |    1208     813     9136    11.2 |  2.336 % |
c |     75968 |    3298    12060 |    1329     963    10240    10.6 |  2.336 % |
c |     76193 |    3298    12060 |    1462    1188    15721    13.2 |  2.336 % |
c |     76531 |    3298    12060 |    1609    1526    23094    15.1 |  2.336 % |
c |     77037 |    3298    12060 |    1769    1050    12522    11.9 |  2.336 % |
c |     77797 |    3298    12060 |    1946    1810    28362    15.7 |  2.336 % |
c |     78936 |    3298    12060 |    2141    1880    38212    20.3 |  2.336 % |
c |     80645 |    3298    12060 |    2355    1286    27843    21.7 |  2.336 % |
c |     83207 |    3298    12060 |    2591    1335    27362    20.5 |  2.336 % |
c |     87051 |    3298    12060 |    2850    2305    77122    33.5 |  2.336 % |
c |     92817 |    3298    12060 |    3135    1869    63417    33.9 |  2.336 % |
c |    101466 |    3298    12060 |    3449    2046    84823    41.5 |  2.336 % |
c |    114441 |    3298    12060 |    3794    2394   114416    47.8 |  2.336 % |
c |    133902 |    3298    12060 |    4173    3793   177730    46.9 |  2.336 % |
c ==============================================================================
c [1mFound solution: 61[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 164   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150798 |    3300    12074 |    1100    3121   124224    39.8 |  2.336 % |
c |    150898 |    3300    12074 |    1210     881    11119    12.6 |  2.620 % |
c |    151048 |    3300    12074 |    1331    1031    12271    11.9 |  2.620 % |
c |    151273 |    3300    12074 |    1464    1256    14539    11.6 |  2.620 % |
c |    151611 |    3300    12074 |    1610     809     7783     9.6 |  2.620 % |
c |    152118 |    3300    12074 |    1771    1316    18592    14.1 |  2.620 % |
c |    152877 |    3300    12074 |    1948    2075    37628    18.1 |  2.620 % |
c |    154018 |    3300    12074 |    2143    2179    37616    17.3 |  2.620 % |
c |    155727 |    3300    12074 |    2357    1619    42502    26.3 |  2.620 % |
c |    158291 |    3300    12074 |    2593    1651    53931    32.7 |  2.620 % |
c |    162135 |    3300    12074 |    2853    2656   142568    53.7 |  2.620 % |
c |    167901 |    3300    12074 |    3138    2292    83350    36.4 |  2.620 % |
c |    176550 |    3300    12074 |    3452    2572   110642    43.0 |  2.620 % |
c |    189525 |    3300    12074 |    3797    2827   130135    46.0 |  2.620 % |
c |    208987 |    3300    12074 |    4177    2378    72898    30.7 |  2.620 % |
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 165   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    220775 |    3302    12083 |    1100    3119   121646    39.0 |  2.620 % |
c |    220875 |    3302    12083 |    1210     880    11929    13.6 |  2.758 % |
c |    221026 |    3302    12083 |    1331    1031    13271    12.9 |  2.758 % |
c |    221251 |    3302    12083 |    1464    1256    16354    13.0 |  2.758 % |
c |    221590 |    3302    12083 |    1610    1595    25149    15.8 |  2.758 % |
c |    222096 |    3302    12083 |    1771    1140    16456    14.4 |  2.758 % |
c |    222855 |    3302    12083 |    1948    1899    34422    18.1 |  2.758 % |
c |    223994 |    3302    12083 |    2143    1947    56954    29.3 |  2.758 % |
c |    225703 |    3302    12083 |    2357    2401    77416    32.2 |  2.758 % |
c |    228265 |    3302    12083 |    2593    2448    92375    37.7 |  2.758 % |
c |    232110 |    3302    12083 |    2853    2071    91412    44.1 |  2.758 % |
c |    237876 |    3302    12083 |    3138    1839    59106    32.1 |  2.758 % |
c |    246526 |    3302    12083 |    3452    2075    73400    35.4 |  2.758 % |
c |    259502 |    3302    12083 |    3797    2410   127706    53.0 |  2.758 % |
c |    278964 |    3302    12083 |    4177    3823   168561    44.1 |  2.758 % |
c |    308158 |    3302    12083 |    4594    2554    94268    36.9 |  2.758 % |
c |    351947 |    3302    12083 |    5054    3775   159194    42.2 |  2.758 % |
c |    417633 |    3302    12083 |    5559    4100   163387    39.9 |  2.758 % |
c |    516159 |    3302    12083 |    6115    5401   245430    45.4 |  2.758 % |
c |    663949 |    3302    12083 |    6727    5118   318529    62.2 |  2.758 % |
c ==============================================================================
c [1mFound solution: 59[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 166   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    854959 |    3304    12092 |    1101    5819   353937    60.8 |  2.758 % |
c |    855060 |    3304    12092 |    1211     829    16197    19.5 |  2.895 % |
c |    855210 |    3304    12092 |    1332     979    17583    18.0 |  2.895 % |
c |    855435 |    3304    12092 |    1465    1204    19296    16.0 |  2.895 % |
c |    855774 |    3304    12092 |    1611    1543    29517    19.1 |  2.895 % |
c |    856280 |    3304    12092 |    1773    1121    16700    14.9 |  2.895 % |
c |    857039 |    3304    12092 |    1950    1880    37600    20.0 |  2.895 % |
c |    858178 |    3304    12092 |    2145    1971    42857    21.7 |  2.895 % |
c |    859888 |    3304    12092 |    2360    1353    27721    20.5 |  2.895 % |
c |    862452 |    3304    12092 |    2596    2604    92356    35.5 |  2.895 % |
c |    866299 |    3304    12092 |    2855    2320    92561    39.9 |  2.895 % |
c |    872065 |    3304    12092 |    3141    2038    76250    37.4 |  2.895 % |
c |    880716 |    3304    12092 |    3455    2390    93254    39.0 |  2.895 % |
c |    893690 |    3304    12092 |    3800    2392    85819    35.9 |  2.895 % |
c |    913152 |    3304    12092 |    4181    3886   216417    55.7 |  2.895 % |
c |    942344 |    3304    12092 |    4599    2424   100639    41.5 |  2.895 % |
c |    986134 |    3304    12092 |    5059    3540   153072    43.2 |  2.895 % |
c |   1051820 |    3304    12092 |    5564    3863   200727    52.0 |  2.895 % |
c |   1150347 |    3304    12092 |    6121    5090   285170    56.0 |  2.895 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 167   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1212079 |    3305    12097 |    1101    3964   204493    51.6 |  2.895 % |
c |   1212179 |    3305    12097 |    1211    1091    23538    21.6 |  3.035 % |
c |   1212329 |    3305    12097 |    1332    1241    25369    20.4 |  3.035 % |
c |   1212554 |    3305    12097 |    1465    1466    28261    19.3 |  3.035 % |
c |   1212891 |    3305    12097 |    1611    1053    16764    15.9 |  3.035 % |
c |   1213397 |    3305    12097 |    1773    1559    31000    19.9 |  3.035 % |
c |   1214156 |    3305    12097 |    1950    1314    24612    18.7 |  3.035 % |
c |   1215297 |    3305    12097 |    2145    1338    25431    19.0 |  3.035 % |
c |   1217005 |    3305    12097 |    2360    1867    50002    26.8 |  3.035 % |
c |   1219569 |    3305    12097 |    2596    1872    55952    29.9 |  3.035 % |
c |   1223413 |    3305    12097 |    2855    2840   108765    38.3 |  3.035 % |
c |   1229179 |    3305    12097 |    3141    2384    87589    36.7 |  3.035 % |
c |   1237828 |    3298    12074 |    3455    2574    90195    35.0 |  3.179 % |
c |   1250804 |    3298    12074 |    3800    2724   101470    37.3 |  3.179 % |
c |   1270268 |    3298    12074 |    4181    2155    80421    37.3 |  3.179 % |
c |   1299460 |    3298    12074 |    4599    3097   140488    45.4 |  3.179 % |
c |   1343250 |    3298    12074 |    5059    4285   232126    54.2 |  3.179 % |
c |   1408934 |    3298    12074 |    5564    4310   242993    56.4 |  3.179 % |
c |   1507462 |    3298    12074 |    6121    5306   241671    45.5 |  3.179 % |
c |   1655252 |    3298    12074 |    6733    5781   299030    51.7 |  3.179 % |
c |   1876938 |    3298    12074 |    7406    6846   368196    53.8 |  3.179 % |
c |   2209463 |    3298    12074 |    8147    6409   288523    45.0 |  3.179 % |
c ==============================================================================
c [1mFound solution: 57[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 168   bits: 8/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   2416543 |    3300    12083 |    1100    5713   249903    43.7 |  3.179 % |
c |   2416644 |    3300    12083 |    1210     816    10045    12.3 |  3.314 % |
c |   2416794 |    3300    12083 |    1331     966    13041    13.5 |  3.314 % |
c |   2417020 |    3300    12083 |    1464    1192    16195    13.6 |  3.314 % |
c |   2417359 |    3300    12083 |    1610    1531    23673    15.5 |  3.314 % |
c |   2417866 |    3300    12083 |    1771    1126    13364    11.9 |  3.314 % |
c |   2418625 |    3300    12083 |    1948    1885    34881    18.5 |  3.314 % |
c |   2419765 |    3300    12083 |    2143    1935    44139    22.8 |  3.314 % |
c |   2421474 |    3300    12083 |    2357    1317    34283    26.0 |  3.314 % |
c |   2424037 |    3300    12083 |    2593    2576    86595    33.6 |  3.314 % |
c |   2427881 |    3300    12083 |    2853    2242    66657    29.7 |  3.314 % |
c |   2433648 |    3300    12083 |    3138    1864    56376    30.2 |  3.314 % |
c |   2442297 |    3300    12083 |    3452    2104    92771    44.1 |  3.314 % |
c |   2455272 |    3300    12083 |    3797    2229    89191    40.0 |  3.314 % |
c |   2474733 |    3300    12083 |    4177    3683   171599    46.6 |  3.314 % |
c |   2503925 |    3300    12083 |    4594    2372    89038    37.5 |  3.314 % |
c |   2547714 |    3300    12083 |    5054    3421   125863    36.8 |  3.314 % |
c |   2613398 |    3300    12083 |    5559    3692   170213    46.1 |  3.314 % |
c |   2711927 |    3300    12083 |    6115    4755   258605    54.4 |  3.314 % |
c |   2859716 |    3300    12083 |    6727    5157   288422    55.9 |  3.314 % |
#### 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.91 0.97 0.92 2/54 19594
Raw data (stat): 19594 (runsolver) R 19593 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482067646 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 645 0 0 0 997 1 0 0 25 0 1 0 482067646 4136960 623 4294967295 134512640 134672761 3221224576 3221223760 134559588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1010 623 603 41 0 969 0
vsize: 4040
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 701 0 0 0 1997 1 0 0 25 0 1 0 482067646 4399104 679 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1074 679 603 41 0 1033 0
vsize: 4296
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 823 0 0 0 2996 2 0 0 25 0 1 0 482067646 4927488 801 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1203 801 603 41 0 1162 0
vsize: 4812
[startup+40.0015 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 878 0 0 0 3996 2 0 0 25 0 1 0 482067646 5197824 856 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1269 856 603 41 0 1228 0
vsize: 5076
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 878 0 0 0 4996 2 0 0 25 0 1 0 482067646 5197824 856 4294967295 134512640 134672761 3221224576 3221223592 1075352757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1269 856 603 41 0 1228 0
vsize: 5076
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 911 0 0 0 5996 3 0 0 25 0 1 0 482067646 5320704 889 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1299 889 603 41 0 1258 0
vsize: 5196
[startup+70.003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 994 0 0 0 6996 3 0 0 25 0 1 0 482067646 5591040 972 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1365 972 603 41 0 1324 0
vsize: 5460
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1035 0 0 0 7996 3 0 0 25 0 1 0 482067646 5730304 1013 4294967295 134512640 134672761 3221224576 3221223648 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 1013 603 41 0 1358 0
vsize: 5596
[startup+90.0032 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1053 0 0 0 8996 3 0 0 25 0 1 0 482067646 5861376 1031 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1431 1031 603 41 0 1390 0
vsize: 5724
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1054 0 0 0 9996 3 0 0 25 0 1 0 482067646 5861376 1032 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1431 1032 603 41 0 1390 0
vsize: 5724
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1111 0 0 0 10996 3 0 0 25 0 1 0 482067646 6127616 1089 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1496 1089 603 41 0 1455 0
vsize: 5984
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1141 0 0 0 11996 4 0 0 25 0 1 0 482067646 6262784 1119 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1119 603 41 0 1488 0
vsize: 6116
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1237 0 0 0 12996 4 0 0 25 0 1 0 482067646 6664192 1215 4294967295 134512640 134672761 3221224576 3221223760 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1627 1215 603 41 0 1586 0
vsize: 6508
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1277 0 0 0 13996 4 0 0 25 0 1 0 482067646 6799360 1255 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1255 603 41 0 1619 0
vsize: 6640
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1278 0 0 0 14996 4 0 0 25 0 1 0 482067646 6799360 1256 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1256 603 41 0 1619 0
vsize: 6640
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1285 0 0 0 15996 4 0 0 25 0 1 0 482067646 6799360 1263 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1263 603 41 0 1619 0
vsize: 6640
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1346 0 0 0 16996 4 0 0 25 0 1 0 482067646 7065600 1324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1725 1324 603 41 0 1684 0
vsize: 6900
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1392 0 0 0 17996 4 0 0 25 0 1 0 482067646 7200768 1370 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1758 1370 603 41 0 1717 0
vsize: 7032
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1410 0 0 0 18996 4 0 0 25 0 1 0 482067646 7331840 1388 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1790 1388 603 41 0 1749 0
vsize: 7160
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1468 0 0 0 19996 4 0 0 25 0 1 0 482067646 7598080 1446 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1855 1446 603 41 0 1814 0
vsize: 7420
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1468 0 0 0 20996 5 0 0 25 0 1 0 482067646 7598080 1446 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1855 1446 603 41 0 1814 0
vsize: 7420
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1472 0 0 0 21997 5 0 0 25 0 1 0 482067646 7598080 1450 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1855 1450 603 41 0 1814 0
vsize: 7420
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1489 0 0 0 22997 5 0 0 25 0 1 0 482067646 7598080 1467 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1855 1467 603 41 0 1814 0
vsize: 7420
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1489 0 0 0 23997 5 0 0 25 0 1 0 482067646 7598080 1467 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1855 1467 603 41 0 1814 0
vsize: 7420
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1551 0 0 0 24997 5 0 0 25 0 1 0 482067646 7868416 1529 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1921 1529 603 41 0 1880 0
vsize: 7684
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1556 0 0 0 25997 5 0 0 25 0 1 0 482067646 7868416 1534 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1921 1534 603 41 0 1880 0
vsize: 7684
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 26997 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 27997 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 28997 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 29997 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 30997 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223496 1075351157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 31998 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 32998 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223680 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 33998 5 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 34997 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 35998 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 36998 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223740 134564515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 37998 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 38998 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 39998 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 40998 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223568 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1579 0 0 0 41998 6 0 0 25 0 1 0 482067646 8003584 1557 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1557 603 41 0 1913 0
vsize: 7816
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1586 0 0 0 42998 6 0 0 25 0 1 0 482067646 8003584 1564 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1954 1564 603 41 0 1913 0
vsize: 7816
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1608 0 0 0 43998 6 0 0 25 0 1 0 482067646 8138752 1586 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1586 603 41 0 1946 0
vsize: 7948
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1608 0 0 0 44998 7 0 0 25 0 1 0 482067646 8138752 1586 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1586 603 41 0 1946 0
vsize: 7948
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1608 0 0 0 45998 7 0 0 25 0 1 0 482067646 8138752 1586 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1586 603 41 0 1946 0
vsize: 7948
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1608 0 0 0 46999 7 0 0 25 0 1 0 482067646 8138752 1586 4294967295 134512640 134672761 3221224576 3221223840 134562156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1586 603 41 0 1946 0
vsize: 7948
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1608 0 0 0 47999 7 0 0 25 0 1 0 482067646 8138752 1586 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1586 603 41 0 1946 0
vsize: 7948
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1608 0 0 0 48999 7 0 0 25 0 1 0 482067646 8138752 1586 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1586 603 41 0 1946 0
vsize: 7948
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1611 0 0 0 49999 7 0 0 25 0 1 0 482067646 8138752 1589 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1589 603 41 0 1946 0
vsize: 7948
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1611 0 0 0 50999 7 0 0 25 0 1 0 482067646 8138752 1589 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1589 603 41 0 1946 0
vsize: 7948
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1621 0 0 0 51999 7 0 0 25 0 1 0 482067646 8138752 1599 4294967295 134512640 134672761 3221224576 3221223728 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1599 603 41 0 1946 0
vsize: 7948
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1622 0 0 0 52999 7 0 0 25 0 1 0 482067646 8138752 1600 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1600 603 41 0 1946 0
vsize: 7948
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1622 0 0 0 53999 8 0 0 25 0 1 0 482067646 8138752 1600 4294967295 134512640 134672761 3221224576 3221223760 134559592 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1600 603 41 0 1946 0
vsize: 7948
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1622 0 0 0 54999 8 0 0 25 0 1 0 482067646 8138752 1600 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1600 603 41 0 1946 0
vsize: 7948
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1673 0 0 0 55999 8 0 0 25 0 1 0 482067646 8409088 1651 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1651 603 41 0 2012 0
vsize: 8212
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1685 0 0 0 56999 8 0 0 25 0 1 0 482067646 8409088 1663 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2053 1663 603 41 0 2012 0
vsize: 8212
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1703 0 0 0 57999 8 0 0 25 0 1 0 482067646 8544256 1681 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2086 1681 603 41 0 2045 0
vsize: 8344
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1703 0 0 0 59000 8 0 0 25 0 1 0 482067646 8544256 1681 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2086 1681 603 41 0 2045 0
vsize: 8344
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1703 0 0 0 60000 8 0 0 25 0 1 0 482067646 8544256 1681 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2086 1681 603 41 0 2045 0
vsize: 8344
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1703 0 0 0 61000 8 0 0 25 0 1 0 482067646 8544256 1681 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2086 1681 603 41 0 2045 0
vsize: 8344
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1732 0 0 0 62000 8 0 0 25 0 1 0 482067646 8675328 1710 4294967295 134512640 134672761 3221224576 3221223744 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2118 1710 603 41 0 2077 0
vsize: 8472
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1761 0 0 0 63000 8 0 0 25 0 1 0 482067646 8810496 1739 4294967295 134512640 134672761 3221224576 3221223760 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1739 603 41 0 2110 0
vsize: 8604
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 64000 8 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 65000 8 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 66000 9 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 67001 9 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 68001 9 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 69001 9 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 70001 9 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1778 0 0 0 71001 9 0 0 25 0 1 0 482067646 8810496 1756 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1756 603 41 0 2110 0
vsize: 8604
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1822 0 0 0 72001 9 0 0 25 0 1 0 482067646 9080832 1800 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2217 1800 603 41 0 2176 0
vsize: 8868
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 73001 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 74001 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223680 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 75001 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 76001 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223760 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 77001 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 78002 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 79002 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1860 0 0 0 80002 9 0 0 25 0 1 0 482067646 9228288 1838 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1838 603 41 0 2212 0
vsize: 9012
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1863 0 0 0 81002 10 0 0 25 0 1 0 482067646 9228288 1841 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1841 603 41 0 2212 0
vsize: 9012
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1869 0 0 0 82002 10 0 0 25 0 1 0 482067646 9228288 1847 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1847 603 41 0 2212 0
vsize: 9012
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1872 0 0 0 83002 10 0 0 25 0 1 0 482067646 9228288 1850 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1850 603 41 0 2212 0
vsize: 9012
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1872 0 0 0 84002 10 0 0 25 0 1 0 482067646 9228288 1850 4294967295 134512640 134672761 3221224576 3221223760 134559559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2253 1850 603 41 0 2212 0
vsize: 9012
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1891 0 0 0 85002 10 0 0 25 0 1 0 482067646 9367552 1869 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1869 603 41 0 2246 0
vsize: 9148
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1904 0 0 0 86002 10 0 0 25 0 1 0 482067646 9367552 1882 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2287 1882 603 41 0 2246 0
vsize: 9148
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1915 0 0 0 87002 10 0 0 25 0 1 0 482067646 9515008 1893 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2323 1893 603 41 0 2282 0
vsize: 9292
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1924 0 0 0 88002 10 0 0 25 0 1 0 482067646 9515008 1902 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2323 1902 603 41 0 2282 0
vsize: 9292
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1932 0 0 0 89002 10 0 0 25 0 1 0 482067646 9633792 1910 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2352 1910 603 41 0 2311 0
vsize: 9408
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1933 0 0 0 90002 11 0 0 25 0 1 0 482067646 9633792 1911 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2352 1911 603 41 0 2311 0
vsize: 9408
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1934 0 0 0 91002 11 0 0 25 0 1 0 482067646 9633792 1912 4294967295 134512640 134672761 3221224576 3221223744 134561554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2352 1912 603 41 0 2311 0
vsize: 9408
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1950 0 0 0 92003 11 0 0 25 0 1 0 482067646 9633792 1928 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2352 1928 603 41 0 2311 0
vsize: 9408
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1953 0 0 0 93003 11 0 0 25 0 1 0 482067646 9633792 1931 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2352 1931 603 41 0 2311 0
vsize: 9408
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1963 0 0 0 94003 11 0 0 25 0 1 0 482067646 9768960 1941 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2385 1941 603 41 0 2344 0
vsize: 9540
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1963 0 0 0 95003 11 0 0 25 0 1 0 482067646 9768960 1941 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2385 1941 603 41 0 2344 0
vsize: 9540
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1991 0 0 0 96003 11 0 0 25 0 1 0 482067646 9768960 1969 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2385 1969 603 41 0 2344 0
vsize: 9540
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 97003 11 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223680 134560177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 98003 11 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 99003 11 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 100003 11 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 101004 11 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223668 1075346528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 102004 11 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 103004 12 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 104004 12 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 1995 0 0 0 105004 12 0 0 25 0 1 0 482067646 9916416 1973 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1973 603 41 0 2380 0
vsize: 9684
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2003 0 0 0 106004 12 0 0 25 0 1 0 482067646 9916416 1981 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1981 603 41 0 2380 0
vsize: 9684
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2013 0 0 0 107004 12 0 0 25 0 1 0 482067646 9916416 1991 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1991 603 41 0 2380 0
vsize: 9684
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2013 0 0 0 108004 12 0 0 25 0 1 0 482067646 9916416 1991 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1991 603 41 0 2380 0
vsize: 9684
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2016 0 0 0 109004 12 0 0 25 0 1 0 482067646 9916416 1994 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1994 603 41 0 2380 0
vsize: 9684
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2016 0 0 0 110004 12 0 0 25 0 1 0 482067646 9916416 1994 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2421 1994 603 41 0 2380 0
vsize: 9684
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2022 0 0 0 111005 12 0 0 25 0 1 0 482067646 10051584 2000 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2454 2000 603 41 0 2413 0
vsize: 9816
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2022 0 0 0 112005 12 0 0 25 0 1 0 482067646 10051584 2000 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2454 2000 603 41 0 2413 0
vsize: 9816
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2031 0 0 0 113005 12 0 0 25 0 1 0 482067646 10051584 2009 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2454 2009 603 41 0 2413 0
vsize: 9816
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2074 0 0 0 114005 13 0 0 25 0 1 0 482067646 10186752 2052 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2487 2052 603 41 0 2446 0
vsize: 9948
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2088 0 0 0 115005 13 0 0 25 0 1 0 482067646 10321920 2066 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2520 2066 603 41 0 2479 0
vsize: 10080
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2090 0 0 0 116005 13 0 0 25 0 1 0 482067646 10305536 2068 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2516 2068 603 41 0 2475 0
vsize: 10064
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2092 0 0 0 117005 13 0 0 25 0 1 0 482067646 10305536 2070 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2516 2070 603 41 0 2475 0
vsize: 10064
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2092 0 0 0 118006 13 0 0 25 0 1 0 482067646 10305536 2070 4294967295 134512640 134672761 3221224576 3221223760 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2516 2070 603 41 0 2475 0
vsize: 10064
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2092 0 0 0 119006 13 0 0 25 0 1 0 482067646 10305536 2070 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2516 2070 603 41 0 2475 0
vsize: 10064
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 19594
Raw data (stat): 19594 (minisat+) R 19593 11931 11930 0 -1 0 2092 0 0 0 120006 13 0 0 25 0 1 0 482067646 10305536 2070 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2516 2070 603 41 0 2475 0
vsize: 10064
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 19594
Raw data (stat): 19594 (minisat+) Z 19593 11931 11930 0 -1 12 2095 0 0 0 120006 13 0 0 25 0 1 0 482067646 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.2
CPU user time (s): 1200.07
CPU system time (s): 0.137979
CPU usage (%): 100.014
Max. virtual memory (Kb): 10080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####