PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-air04.opb
MD5SUM	ee388359e66788d310d5d5b34d6465c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63236
Optimality of the best value was proved	NO
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1185.16
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 16849

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 08:42:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12439 boxname=wulflinc27 idbench=957 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ee388359e66788d310d5d5b34d6465c1  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-air04.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-air04.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-air04.opb
IDLAUNCH: 12439
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        651260 kB
Buffers:          5856 kB
Cached:         351176 kB
SwapCached:        512 kB
Active:          44512 kB
Inactive:       314512 kB
HighTotal:      131008 kB
HighFree:         3696 kB
LowTotal:       903652 kB
LowFree:        647564 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            18728 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:02:59 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 12439 7 1200.31 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   67
c ---[1640]---> BDD-cost:  303
c ---[1638]---> BDD-cost:  119
c ---[1636]---> BDD-cost:  145
c ---[1634]---> BDD-cost:  165
c ---[1632]---> BDD-cost:  239
c ---[1630]---> BDD-cost:  223
c ---[1628]---> BDD-cost:   59
c ---[1626]---> BDD-cost:   35
c ---[1624]---> BDD-cost:   93
c ---[1622]---> BDD-cost:   45
c ---[1620]---> BDD-cost:  213
c ---[1618]---> BDD-cost:   73
c ---[1616]---> BDD-cost:   75
c ---[1614]---> BDD-cost:   63
c ---[1612]---> BDD-cost:   99
c ---[1608]---> BDD-cost:  187
c ---[1606]---> BDD-cost:   55
c ---[1604]---> BDD-cost:  107
c ---[1602]---> BDD-cost:   69
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   75
c ---[1596]---> BDD-cost:    3
c ---[1594]---> BDD-cost:  149
c ---[1592]---> BDD-cost:  137
c ---[1590]---> BDD-cost:  195
c ---[1588]---> BDD-cost:   93
c ---[1586]---> BDD-cost:  157
c ---[1584]---> BDD-cost:  233
c ---[1582]---> BDD-cost:  223
c ---[1580]---> BDD-cost:  225
c ---[1578]---> BDD-cost:  247
c ---[1576]---> BDD-cost:   75
c ---[1574]---> BDD-cost:  179
c ---[1572]---> BDD-cost:  225
c ---[1570]---> BDD-cost:  243
c ---[1568]---> BDD-cost:  199
c ---[1566]---> BDD-cost:   55
c ---[1564]---> BDD-cost:   57
c ---[1562]---> BDD-cost:   99
c ---[1560]---> BDD-cost:    9
c ---[1558]---> BDD-cost:    3
c ---[1556]---> BDD-cost:   23
c ---[1554]---> BDD-cost:   55
c ---[1552]---> BDD-cost:   51
c ---[1550]---> BDD-cost:   25
c ---[1548]---> BDD-cost:   23
c ---[1546]---> BDD-cost:   27
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:   37
c ---[1540]---> BDD-cost:   67
c ---[1538]---> BDD-cost:   67
c ---[1536]---> BDD-cost:  109
c ---[1534]---> BDD-cost:  211
c ---[1532]---> BDD-cost:   15
c ---[1530]---> BDD-cost:    0
c ---[1526]---> BDD-cost:   65
c ---[1524]---> BDD-cost:  117
c ---[1522]---> BDD-cost:   65
c ---[1520]---> BDD-cost:   65
c ---[1518]---> BDD-cost:   49
c ---[1516]---> BDD-cost:  439
c ---[1514]---> BDD-cost:  423
c ---[1512]---> BDD-cost:  287
c ---[1510]---> BDD-cost:   87
c ---[1508]---> BDD-cost:  217
c ---[1506]---> BDD-cost:  195
c ---[1504]---> BDD-cost:   63
c ---[1502]---> BDD-cost:   53
c ---[1500]---> BDD-cost:  359
c ---[1498]---> BDD-cost:  353
c ---[1494]---> BDD-cost:  169
c ---[1492]---> BDD-cost:  139
c ---[1490]---> BDD-cost:  159
c ---[1488]---> BDD-cost:   51
c ---[1486]---> BDD-cost:  223
c ---[1484]---> BDD-cost:  107
c ---[1482]---> BDD-cost:   75
c ---[1480]---> BDD-cost:  109
c ---[1478]---> BDD-cost:   93
c ---[1476]---> BDD-cost:   87
c ---[1474]---> BDD-cost:   87
c ---[1472]---> BDD-cost:    7
c ---[1468]---> BDD-cost:   73
c ---[1466]---> BDD-cost:    1
c ---[1464]---> BDD-cost:   71
c ---[1462]---> BDD-cost:  107
c ---[1460]---> BDD-cost:   77
c ---[1458]---> BDD-cost:    3
c ---[1456]---> BDD-cost:  107
c ---[1454]---> BDD-cost:  131
c ---[1452]---> BDD-cost:  135
c ---[1450]---> BDD-cost:   65
c ---[1448]---> BDD-cost:  165
c ---[1446]---> BDD-cost:  123
c ---[1444]---> BDD-cost:    1
c ---[1442]---> BDD-cost:    1
c ---[1440]---> BDD-cost:   87
c ---[1438]---> BDD-cost:  155
c ---[1436]---> BDD-cost:  167
c ---[1434]---> BDD-cost:  203
c ---[1432]---> BDD-cost:  231
c ---[1430]---> BDD-cost:  147
c ---[1428]---> BDD-cost:  135
c ---[1426]---> BDD-cost:   49
c ---[1424]---> BDD-cost:   31
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   23
c ---[1418]---> BDD-cost:   95
c ---[1416]---> BDD-cost:  325
c ---[1414]---> BDD-cost:  333
c ---[1412]---> BDD-cost:  173
c ---[1410]---> BDD-cost:  269
c ---[1408]---> BDD-cost:   31
c ---[1406]---> BDD-cost:  413
c ---[1404]---> BDD-cost:  313
c ---[1402]---> BDD-cost:  125
c ---[1400]---> BDD-cost:  113
c ---[1398]---> BDD-cost:   11
c ---[1396]---> BDD-cost:  247
c ---[1394]---> BDD-cost:   57
c ---[1392]---> BDD-cost:  237
c ---[1390]---> BDD-cost:  159
c ---[1388]---> BDD-cost:  117
c ---[1386]---> BDD-cost:   43
c ---[1384]---> BDD-cost:  143
c ---[1382]---> BDD-cost:   65
c ---[1380]---> BDD-cost:  123
c ---[1378]---> BDD-cost:   61
c ---[1376]---> BDD-cost:   39
c ---[1374]---> BDD-cost:  103
c ---[1372]---> BDD-cost:   85
c ---[1370]---> BDD-cost:   77
c ---[1368]---> BDD-cost:   57
c ---[1366]---> BDD-cost:  127
c ---[1364]---> BDD-cost:  157
c ---[1362]---> BDD-cost:  267
c ---[1360]---> BDD-cost:  223
c ---[1358]---> BDD-cost:  229
c ---[1356]---> BDD-cost:  257
c ---[1354]---> BDD-cost:   13
c ---[1352]---> BDD-cost:  241
c ---[1350]---> BDD-cost:  195
c ---[1348]---> BDD-cost:   49
c ---[1346]---> BDD-cost:  117
c ---[1344]---> BDD-cost:  197
c ---[1342]---> BDD-cost:  171
c ---[1340]---> BDD-cost:  287
c ---[1338]---> BDD-cost:   75
c ---[1336]---> BDD-cost:  215
c ---[1334]---> BDD-cost:  119
c ---[1332]---> BDD-cost:   57
c ---[1330]---> BDD-cost:  245
c ---[1328]---> BDD-cost:  257
c ---[1326]---> BDD-cost:  279
c ---[1324]---> BDD-cost:  227
c ---[1322]---> BDD-cost:  201
c ---[1320]---> BDD-cost:  143
c ---[1318]---> BDD-cost:  207
c ---[1316]---> BDD-cost:  131
c ---[1314]---> BDD-cost:  245
c ---[1312]---> BDD-cost:  115
c ---[1310]---> BDD-cost:  259
c ---[1308]---> BDD-cost:   91
c ---[1306]---> BDD-cost:   43
c ---[1304]---> BDD-cost:   39
c ---[1302]---> BDD-cost:   91
c ---[1300]---> BDD-cost:  179
c ---[1298]---> BDD-cost:   73
c ---[1296]---> BDD-cost:   29
c ---[1294]---> BDD-cost:  163
c ---[1292]---> BDD-cost:   81
c ---[1290]---> BDD-cost:   63
c ---[1288]---> BDD-cost:  189
c ---[1286]---> BDD-cost:  103
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  115
c ---[1280]---> BDD-cost:   19
c ---[1278]---> BDD-cost:   93
c ---[1276]---> BDD-cost:   99
c ---[1274]---> BDD-cost:   99
c ---[1272]---> BDD-cost:  103
c ---[1270]---> BDD-cost:   67
c ---[1268]---> BDD-cost:   23
c ---[1266]---> BDD-cost:  101
c ---[1264]---> BDD-cost:   85
c ---[1262]---> BDD-cost:   87
c ---[1260]---> BDD-cost:    7
c ---[1258]---> BDD-cost:   45
c ---[1256]---> BDD-cost:   43
c ---[1254]---> BDD-cost:   11
c ---[1252]---> BDD-cost:   59
c ---[1250]---> BDD-cost:  185
c ---[1248]---> BDD-cost:  249
c ---[1246]---> BDD-cost:  315
c ---[1244]---> BDD-cost:  137
c ---[1242]---> BDD-cost:  253
c ---[1240]---> BDD-cost:  161
c ---[1238]---> BDD-cost:  257
c ---[1236]---> BDD-cost:  167
c ---[1234]---> BDD-cost:  167
c ---[1232]---> BDD-cost:  141
c ---[1230]---> BDD-cost:   21
c ---[1228]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   95
c ---[1224]---> BDD-cost:  141
c ---[1222]---> BDD-cost:    0
c ---[1220]---> BDD-cost:  123
c ---[1218]---> BDD-cost:   83
c ---[1216]---> BDD-cost:   55
c ---[1214]---> BDD-cost:  183
c ---[1212]---> BDD-cost:  269
c ---[1210]---> BDD-cost:   63
c ---[1208]---> BDD-cost:   45
c ---[1206]---> BDD-cost:   39
c ---[1204]---> BDD-cost:   97
c ---[1202]---> BDD-cost:   51
c ---[1200]---> BDD-cost:   23
c ---[1198]---> BDD-cost:  101
c ---[1196]---> BDD-cost:   45
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   85
c ---[1190]---> BDD-cost:   35
c ---[1188]---> BDD-cost:   53
c ---[1186]---> BDD-cost:   21
c ---[1184]---> BDD-cost:  115
c ---[1182]---> BDD-cost:   99
c ---[1180]---> BDD-cost:   63
c ---[1178]---> BDD-cost:   77
c ---[1176]---> BDD-cost:   37
c ---[1174]---> BDD-cost:  139
c ---[1172]---> BDD-cost:  109
c ---[1170]---> BDD-cost:  407
c ---[1168]---> BDD-cost:  323
c ---[1166]---> BDD-cost:  109
c ---[1164]---> BDD-cost:   93
c ---[1162]---> BDD-cost:   51
c ---[1160]---> BDD-cost:   79
c ---[1158]---> BDD-cost:   75
c ---[1156]---> BDD-cost:  147
c ---[1154]---> BDD-cost:    0
c ---[1152]---> BDD-cost:  169
c ---[1150]---> BDD-cost:  209
c ---[1148]---> BDD-cost:   69
c ---[1146]---> BDD-cost:   51
c ---[1144]---> BDD-cost:   85
c ---[1140]---> BDD-cost:  103
c ---[1138]---> BDD-cost:  127
c ---[1136]---> BDD-cost:   77
c ---[1134]---> BDD-cost:   77
c ---[1132]---> BDD-cost:  181
c ---[1130]---> BDD-cost:  141
c ---[1128]---> BDD-cost:   89
c ---[1126]---> BDD-cost:   85
c ---[1124]---> BDD-cost:  119
c ---[1122]---> BDD-cost:   69
c ---[1120]---> BDD-cost:   57
c ---[1118]---> BDD-cost:   65
c ---[1116]---> BDD-cost:   47
c ---[1114]---> BDD-cost:   61
c ---[1112]---> BDD-cost:   31
c ---[1110]---> BDD-cost:  283
c ---[1106]---> BDD-cost:  183
c ---[1104]---> BDD-cost:  121
c ---[1102]---> BDD-cost:   89
c ---[1100]---> BDD-cost:  225
c ---[1098]---> BDD-cost:  267
c ---[1094]---> BDD-cost:  159
c ---[1092]---> BDD-cost:  209
c ---[1090]---> BDD-cost:   71
c ---[1088]---> BDD-cost:   99
c ---[1086]---> BDD-cost:  237
c ---[1084]---> BDD-cost:  129
c ---[1082]---> BDD-cost:  365
c ---[1080]---> BDD-cost:  369
c ---[1078]---> BDD-cost:  129
c ---[1076]---> BDD-cost:  101
c ---[1074]---> BDD-cost:  289
c ---[1072]---> BDD-cost:  279
c ---[1070]---> BDD-cost:  345
c ---[1068]---> BDD-cost:   81
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:   69
c ---[1062]---> BDD-cost:   83
c ---[1060]---> BDD-cost:   53
c ---[1058]---> BDD-cost:   67
c ---[1056]---> BDD-cost:   55
c ---[1054]---> BDD-cost:  145
c ---[1052]---> BDD-cost:  149
c ---[1050]---> BDD-cost:  105
c ---[1048]---> BDD-cost:   19
c ---[1046]---> BDD-cost:  105
c ---[1044]---> BDD-cost:  109
c ---[1042]---> BDD-cost:  101
c ---[1040]---> BDD-cost:  147
c ---[1038]---> BDD-cost:  231
c ---[1036]---> BDD-cost:  191
c ---[1034]---> BDD-cost:  157
c ---[1032]---> BDD-cost:  249
c ---[1030]---> BDD-cost:  385
c ---[1028]---> BDD-cost:   67
c ---[1026]---> BDD-cost:   71
c ---[1024]---> BDD-cost:   47
c ---[1022]---> BDD-cost:   75
c ---[1020]---> BDD-cost:  147
c ---[1018]---> BDD-cost:  139
c ---[1016]---> BDD-cost:  273
c ---[1014]---> BDD-cost:  213
c ---[1012]---> BDD-cost:  169
c ---[1010]---> BDD-cost:  239
c ---[1008]---> BDD-cost:  305
c ---[1006]---> BDD-cost:  109
c ---[1004]---> BDD-cost:  105
c ---[1002]---> BDD-cost:  147
c ---[1000]---> BDD-cost:  237
c ---[ 998]---> BDD-cost:  115
c ---[ 996]---> BDD-cost:  115
c ---[ 994]---> BDD-cost:   67
c ---[ 992]---> BDD-cost:  329
c ---[ 990]---> BDD-cost:  295
c ---[ 988]---> BDD-cost:   51
c ---[ 986]---> BDD-cost:   61
c ---[ 984]---> BDD-cost:  317
c ---[ 982]---> BDD-cost:   97
c ---[ 980]---> BDD-cost:   79
c ---[ 978]---> BDD-cost:   29
c ---[ 976]---> BDD-cost:  119
c ---[ 974]---> BDD-cost:   43
c ---[ 972]---> BDD-cost:   85
c ---[ 970]---> BDD-cost:   35
c ---[ 968]---> BDD-cost:   69
c ---[ 964]---> BDD-cost:   45
c ---[ 962]---> BDD-cost:   73
c ---[ 960]---> BDD-cost:   55
c ---[ 956]---> BDD-cost:   33
c ---[ 954]---> BDD-cost:  109
c ---[ 952]---> BDD-cost:   29
c ---[ 950]---> BDD-cost:  245
c ---[ 948]---> BDD-cost:  225
c ---[ 946]---> BDD-cost:  111
c ---[ 944]---> BDD-cost:  117
c ---[ 942]---> BDD-cost:  127
c ---[ 940]---> BDD-cost:  129
c ---[ 938]---> BDD-cost:  259
c ---[ 936]---> BDD-cost:  221
c ---[ 934]---> BDD-cost:  275
c ---[ 932]---> BDD-cost:   83
c ---[ 930]---> BDD-cost:  209
c ---[ 928]---> BDD-cost:  267
c ---[ 926]---> BDD-cost:  171
c ---[ 924]---> BDD-cost:   57
c ---[ 920]---> BDD-cost:  133
c ---[ 918]---> BDD-cost:  185
c ---[ 916]---> BDD-cost:  169
c ---[ 914]---> BDD-cost:  287
c ---[ 912]---> BDD-cost:   81
c ---[ 910]---> BDD-cost:   13
c ---[ 908]---> BDD-cost:  335
c ---[ 906]---> BDD-cost:  365
c ---[ 904]---> BDD-cost:  255
c ---[ 902]---> BDD-cost:  111
c ---[ 900]---> BDD-cost:   57
c ---[ 898]---> BDD-cost:  101
c ---[ 896]---> BDD-cost:  197
c ---[ 894]---> BDD-cost:  383
c ---[ 892]---> BDD-cost:  329
c ---[ 890]---> BDD-cost:  241
c ---[ 888]---> BDD-cost:  157
c ---[ 886]---> BDD-cost:  129
c ---[ 884]---> BDD-cost:   85
c ---[ 882]---> BDD-cost:   71
c ---[ 880]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   77
c ---[ 876]---> BDD-cost:   49
c ---[ 874]---> BDD-cost:  133
c ---[ 872]---> BDD-cost:  133
c ---[ 870]---> BDD-cost:  377
c ---[ 868]---> BDD-cost:  117
c ---[ 866]---> BDD-cost:  155
c ---[ 862]---> BDD-cost:  119
c ---[ 860]---> BDD-cost:  119
c ---[ 858]---> BDD-cost:  151
c ---[ 856]---> BDD-cost:  221
c ---[ 854]---> BDD-cost:  181
c ---[ 850]---> BDD-cost:   87
c ---[ 848]---> BDD-cost:  127
c ---[ 846]---> BDD-cost:  299
c ---[ 844]---> BDD-cost:  109
c ---[ 842]---> BDD-cost:  331
c ---[ 838]---> BDD-cost:   21
c ---[ 836]---> BDD-cost:  205
c ---[ 834]---> BDD-cost:  217
c ---[ 832]---> BDD-cost:  349
c ---[ 830]---> BDD-cost:  291
c ---[ 828]---> BDD-cost:  165
c ---[ 826]---> BDD-cost:  161
c ---[ 824]---> BDD-cost:   61
c ---[ 822]---> BDD-cost:   77
c ---[ 820]---> BDD-cost:   55
c ---[ 818]---> BDD-cost:  113
c ---[ 816]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:  189
c ---[ 812]---> BDD-cost:  157
c ---[ 810]---> BDD-cost:  149
c ---[ 808]---> BDD-cost:  139
c ---[ 806]---> BDD-cost:  165
c ---[ 804]---> BDD-cost:  181
c ---[ 802]---> BDD-cost:  253
c ---[ 800]---> BDD-cost:    0
c ---[ 798]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:  145
c ---[ 794]---> BDD-cost:  141
c ---[ 792]---> BDD-cost:  105
c ---[ 790]---> BDD-cost:   95
c ---[ 788]---> BDD-cost:   75
c ---[ 786]---> BDD-cost:  103
c ---[ 784]---> BDD-cost:  149
c ---[ 782]---> BDD-cost:  137
c ---[ 780]---> BDD-cost:   59
c ---[ 778]---> BDD-cost:  133
c ---[ 776]---> BDD-cost:    5
c ---[ 774]---> BDD-cost:   35
c ---[ 772]---> BDD-cost:    9
c ---[ 770]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   55
c ---[ 762]---> BDD-cost:  197
c ---[ 760]---> BDD-cost:  191
c ---[ 758]---> BDD-cost:  125
c ---[ 756]---> BDD-cost:    0
c ---[ 754]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  173
c ---[ 748]---> BDD-cost:   93
c ---[ 746]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:  321
c ---[ 742]---> BDD-cost:  195
c ---[ 740]---> BDD-cost:  163
c ---[ 734]---> BDD-cost:  151
c ---[ 732]---> BDD-cost:  115
c ---[ 730]---> BDD-cost:  253
c ---[ 728]---> BDD-cost:  381
c ---[ 726]---> BDD-cost:  345
c ---[ 724]---> BDD-cost:  185
c ---[ 720]---> BDD-cost:   83
c ---[ 718]---> BDD-cost:   69
c ---[ 716]---> BDD-cost:   51
c ---[ 714]---> BDD-cost:   47
c ---[ 712]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:  185
c ---[ 708]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  107
c ---[ 704]---> BDD-cost:  363
c ---[ 702]---> BDD-cost:  103
c ---[ 700]---> BDD-cost:  277
c ---[ 698]---> BDD-cost:  341
c ---[ 696]---> BDD-cost:  213
c ---[ 694]---> BDD-cost:  315
c ---[ 692]---> BDD-cost:  275
c ---[ 690]---> BDD-cost:  151
c ---[ 688]---> BDD-cost:  203
c ---[ 686]---> BDD-cost:  111
c ---[ 684]---> BDD-cost:  103
c ---[ 682]---> BDD-cost:   75
c ---[ 680]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   21
c ---[ 676]---> BDD-cost:   11
c ---[ 674]---> BDD-cost:   31
c ---[ 670]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:  149
c ---[ 666]---> BDD-cost:  167
c ---[ 664]---> BDD-cost:    0
c ---[ 662]---> BDD-cost:   97
c ---[ 660]---> BDD-cost:  149
c ---[ 658]---> BDD-cost:  395
c ---[ 656]---> BDD-cost:   25
c ---[ 654]---> BDD-cost:  389
c ---[ 652]---> BDD-cost:  251
c ---[ 650]---> BDD-cost:  375
c ---[ 648]---> BDD-cost:  343
c ---[ 646]---> BDD-cost:  267
c ---[ 644]---> BDD-cost:  135
c ---[ 642]---> BDD-cost:  135
c ---[ 640]---> BDD-cost:  263
c ---[ 638]---> BDD-cost:  259
c ---[ 636]---> BDD-cost:  245
c ---[ 634]---> BDD-cost:   45
c ---[ 632]---> BDD-cost:   41
c ---[ 630]---> BDD-cost:  127
c ---[ 628]---> BDD-cost:  117
c ---[ 626]---> BDD-cost:   53
c ---[ 624]---> BDD-cost:  149
c ---[ 622]---> BDD-cost:    9
c ---[ 620]---> BDD-cost:  103
c ---[ 618]---> BDD-cost:  215
c ---[ 616]---> BDD-cost:   89
c ---[ 614]---> BDD-cost:  177
c ---[ 612]---> BDD-cost:  343
c ---[ 610]---> BDD-cost:  237
c ---[ 608]---> BDD-cost:  177
c ---[ 606]---> BDD-cost:   85
c ---[ 604]---> BDD-cost:  267
c ---[ 602]---> BDD-cost:  225
c ---[ 600]---> BDD-cost:   85
c ---[ 598]---> BDD-cost:  109
c ---[ 596]---> BDD-cost:  105
c ---[ 594]---> BDD-cost:  113
c ---[ 592]---> BDD-cost:   55
c ---[ 590]---> BDD-cost:  117
c ---[ 588]---> BDD-cost:   83
c ---[ 586]---> BDD-cost:   79
c ---[ 584]---> BDD-cost:   81
c ---[ 582]---> BDD-cost:  263
c ---[ 580]---> BDD-cost:  179
c ---[ 578]---> BDD-cost:  143
c ---[ 576]---> BDD-cost:  281
c ---[ 574]---> BDD-cost:  389
c ---[ 572]---> BDD-cost:  333
c ---[ 570]---> BDD-cost:  357
c ---[ 568]---> BDD-cost:  345
c ---[ 566]---> BDD-cost:  263
c ---[ 564]---> BDD-cost:   89
c ---[ 562]---> BDD-cost:  285
c ---[ 558]---> BDD-cost:  419
c ---[ 556]---> BDD-cost:  135
c ---[ 554]---> BDD-cost:  357
c ---[ 552]---> BDD-cost:  473
c ---[ 550]---> BDD-cost:  455
c ---[ 548]---> BDD-cost:  405
c ---[ 546]---> BDD-cost:  241
c ---[ 544]---> BDD-cost:  211
c ---[ 542]---> BDD-cost:  313
c ---[ 540]---> BDD-cost:  371
c ---[ 538]---> BDD-cost:  389
c ---[ 536]---> BDD-cost:  223
c ---[ 534]---> BDD-cost:   71
c ---[ 532]---> BDD-cost:   63
c ---[ 530]---> BDD-cost:  221
c ---[ 528]---> BDD-cost:  147
c ---[ 526]---> BDD-cost:  131
c ---[ 524]---> BDD-cost:  185
c ---[ 522]---> BDD-cost:  141
c ---[ 520]---> BDD-cost:  249
c ---[ 518]---> BDD-cost:  261
c ---[ 516]---> BDD-cost:  311
c ---[ 514]---> BDD-cost:  261
c ---[ 512]---> BDD-cost:  387
c ---[ 510]---> BDD-cost:   51
c ---[ 508]---> BDD-cost:  247
c ---[ 506]---> BDD-cost:  295
c ---[ 504]---> BDD-cost:   31
c ---[ 502]---> BDD-cost:  355
c ---[ 500]---> BDD-cost:  135
c ---[ 498]---> BDD-cost:  443
c ---[ 496]---> BDD-cost:  653
c ---[ 494]---> BDD-cost:  703
c ---[ 492]---> BDD-cost:  517
c ---[ 490]---> BDD-cost:  441
c ---[ 488]---> BDD-cost:  159
c ---[ 486]---> BDD-cost:  411
c ---[ 484]---> BDD-cost:  289
c ---[ 482]---> BDD-cost:  277
c ---[ 480]---> BDD-cost:  239
c ---[ 478]---> BDD-cost:  201
c ---[ 476]---> BDD-cost:  309
c ---[ 474]---> BDD-cost:  287
c ---[ 472]---> BDD-cost:  177
c ---[ 470]---> BDD-cost:  143
c ---[ 468]---> BDD-cost:  131
c ---[ 466]---> BDD-cost:  155
c ---[ 464]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:  189
c ---[ 460]---> BDD-cost:  219
c ---[ 456]---> BDD-cost:  267
c ---[ 454]---> BDD-cost:  135
c ---[ 452]---> BDD-cost:   69
c ---[ 450]---> BDD-cost:   75
c ---[ 448]---> BDD-cost:   51
c ---[ 446]---> BDD-cost:  117
c ---[ 444]---> BDD-cost:  211
c ---[ 442]---> BDD-cost:  117
c ---[ 436]---> BDD-cost:  189
c ---[ 434]---> BDD-cost:   73
c ---[ 432]---> BDD-cost:   55
c ---[ 430]---> BDD-cost:   57
c ---[ 428]---> BDD-cost:   91
c ---[ 426]---> BDD-cost:  325
c ---[ 424]---> BDD-cost:  223
c ---[ 422]---> BDD-cost:   75
c ---[ 420]---> BDD-cost:   57
c ---[ 418]---> BDD-cost:   43
c ---[ 416]---> BDD-cost:  255
c ---[ 414]---> BDD-cost:  285
c ---[ 412]---> BDD-cost:  187
c ---[ 410]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   91
c ---[ 406]---> BDD-cost:  211
c ---[ 404]---> BDD-cost:  159
c ---[ 402]---> BDD-cost:   97
c ---[ 400]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   27
c ---[ 396]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  141
c ---[ 390]---> BDD-cost:  109
c ---[ 388]---> BDD-cost:  321
c ---[ 386]---> BDD-cost:  305
c ---[ 384]---> BDD-cost:  603
c ---[ 382]---> BDD-cost:  441
c ---[ 380]---> BDD-cost:  391
c ---[ 378]---> BDD-cost:   87
c ---[ 376]---> BDD-cost:  387
c ---[ 374]---> BDD-cost:  289
c ---[ 372]---> BDD-cost:  219
c ---[ 370]---> BDD-cost:  309
c ---[ 368]---> BDD-cost:  241
c ---[ 366]---> BDD-cost:  197
c ---[ 364]---> BDD-cost:  279
c ---[ 362]---> BDD-cost:  167
c ---[ 360]---> BDD-cost:  151
c ---[ 358]---> BDD-cost:   49
c ---[ 356]---> BDD-cost:   79
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:  107
c ---[ 350]---> BDD-cost:   55
c ---[ 346]---> BDD-cost:  177
c ---[ 344]---> BDD-cost:  223
c ---[ 342]---> BDD-cost:  119
c ---[ 340]---> BDD-cost:  137
c ---[ 338]---> BDD-cost:  105
c ---[ 336]---> BDD-cost:  183
c ---[ 334]---> BDD-cost:  109
c ---[ 332]---> BDD-cost:  179
c ---[ 330]---> BDD-cost:  285
c ---[ 328]---> BDD-cost:  191
c ---[ 326]---> BDD-cost:  177
c ---[ 324]---> BDD-cost:  145
c ---[ 320]---> BDD-cost:  153
c ---[ 318]---> BDD-cost:  121
c ---[ 316]---> BDD-cost:   95
c ---[ 314]---> BDD-cost:  111
c ---[ 312]---> BDD-cost:   35
c ---[ 310]---> BDD-cost:  115
c ---[ 308]---> BDD-cost:    0
c ---[ 306]---> BDD-cost:  281
c ---[ 304]---> BDD-cost:  265
c ---[ 302]---> BDD-cost:  167
c ---[ 300]---> BDD-cost:  151
c ---[ 298]---> BDD-cost:  167
c ---[ 296]---> BDD-cost:  137
c ---[ 292]---> BDD-cost:  375
c ---[ 290]---> BDD-cost:  287
c ---[ 288]---> BDD-cost:  247
c ---[ 286]---> BDD-cost:  249
c ---[ 284]---> BDD-cost:  131
c ---[ 282]---> BDD-cost:  187
c ---[ 280]---> BDD-cost:  135
c ---[ 278]---> BDD-cost:  129
c ---[ 276]---> BDD-cost:  317
c ---[ 274]---> BDD-cost:  365
c ---[ 272]---> BDD-cost:  235
c ---[ 270]---> BDD-cost:  249
c ---[ 268]---> BDD-cost:  283
c ---[ 266]---> BDD-cost:  105
c ---[ 264]---> BDD-cost:  233
c ---[ 262]---> BDD-cost:  259
c ---[ 260]---> BDD-cost:  287
c ---[ 258]---> BDD-cost:  175
c ---[ 256]---> BDD-cost:  233
c ---[ 254]---> BDD-cost:  167
c ---[ 252]---> BDD-cost:  159
c ---[ 250]---> BDD-cost:   47
c ---[ 246]---> BDD-cost:  135
c ---[ 244]---> BDD-cost:   59
c ---[ 242]---> BDD-cost:  147
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  203
c ---[ 236]---> BDD-cost:  275
c ---[ 234]---> BDD-cost:  263
c ---[ 232]---> BDD-cost:   31
c ---[ 230]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   31
c ---[ 226]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:  225
c ---[ 222]---> BDD-cost:   71
c ---[ 220]---> BDD-cost:   65
c ---[ 218]---> BDD-cost:  385
c ---[ 216]---> BDD-cost:  361
c ---[ 214]---> BDD-cost:   73
c ---[ 212]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:  131
c ---[ 206]---> BDD-cost:  145
c ---[ 204]---> BDD-cost:  121
c ---[ 202]---> BDD-cost:  117
c ---[ 200]---> BDD-cost:   61
c ---[ 198]---> BDD-cost:  111
c ---[ 196]---> BDD-cost:  123
c ---[ 194]---> BDD-cost:  125
c ---[ 192]---> BDD-cost:  243
c ---[ 190]---> BDD-cost:  143
c ---[ 188]---> BDD-cost:  149
c ---[ 186]---> BDD-cost:  103
c ---[ 184]---> BDD-cost:  155
c ---[ 182]---> BDD-cost:  247
c ---[ 180]---> BDD-cost:  143
c ---[ 178]---> BDD-cost:   89
c ---[ 176]---> BDD-cost:   91
c ---[ 174]---> BDD-cost:   81
c ---[ 172]---> BDD-cost:   79
c ---[ 170]---> BDD-cost:  117
c ---[ 168]---> BDD-cost:   89
c ---[ 166]---> BDD-cost:   61
c ---[ 164]---> BDD-cost:  127
c ---[ 162]---> BDD-cost:  135
c ---[ 160]---> BDD-cost:  161
c ---[ 158]---> BDD-cost:  141
c ---[ 156]---> BDD-cost:   91
c ---[ 154]---> BDD-cost:  437
c ---[ 152]---> BDD-cost:  309
c ---[ 150]---> BDD-cost:  173
c ---[ 148]---> BDD-cost:  441
c ---[ 146]---> BDD-cost:  489
c ---[ 144]---> BDD-cost:  299
c ---[ 142]---> BDD-cost:  455
c ---[ 140]---> BDD-cost:  333
c ---[ 138]---> BDD-cost:  421
c ---[ 136]---> BDD-cost:  375
c ---[ 134]---> BDD-cost:  143
c ---[ 132]---> BDD-cost:  433
c ---[ 130]---> BDD-cost:  405
c ---[ 128]---> BDD-cost:  333
c ---[ 126]---> BDD-cost:  673
c ---[ 124]---> BDD-cost:  685
c ---[ 122]---> BDD-cost:  385
c ---[ 120]---> BDD-cost:  267
c ---[ 118]---> BDD-cost:  345
c ---[ 116]---> BDD-cost:  365
c ---[ 114]---> BDD-cost:  391
c ---[ 112]---> BDD-cost:  111
c ---[ 110]---> BDD-cost:  313
c ---[ 108]---> BDD-cost:  275
c ---[ 106]---> BDD-cost:  257
c ---[ 104]---> BDD-cost:  203
c ---[ 102]---> BDD-cost:  311
c ---[ 100]---> BDD-cost:  227
c ---[  98]---> BDD-cost:  295
c ---[  96]---> BDD-cost:  233
c ---[  94]---> BDD-cost:  247
c ---[  92]---> BDD-cost:  237
c ---[  90]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   95
c ---[  86]---> BDD-cost:    0
c ---[  84]---> BDD-cost:  149
c ---[  80]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   85
c ---[  76]---> BDD-cost:  109
c ---[  74]---> BDD-cost:   43
c ---[  72]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   71
c ---[  68]---> BDD-cost:   67
c ---[  66]---> BDD-cost:  169
c ---[  64]---> BDD-cost:  151
c ---[  62]---> BDD-cost:  147
c ---[  60]---> BDD-cost:  177
c ---[  58]---> BDD-cost:  127
c ---[  56]---> BDD-cost:  131
c ---[  54]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  215
c ---[  50]---> BDD-cost:  181
c ---[  48]---> BDD-cost:  235
c ---[  46]---> BDD-cost:  163
c ---[  44]---> BDD-cost:  101
c ---[  42]---> BDD-cost:   57
c ---[  40]---> BDD-cost:   59
c ---[  38]---> BDD-cost:  139
c ---[  36]---> BDD-cost:   39
c ---[  34]---> BDD-cost:  151
c ---[  32]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   45
c ---[  28]---> BDD-cost:   45
c ---[  26]---> BDD-cost:   45
c ---[  24]---> BDD-cost:   65
c ---[  22]---> BDD-cost:   95
c ---[  20]---> BDD-cost:    0
c ---[  16]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   81
c ---[   2]---> BDD-cost:  223
c ---[   0]---> BDD-cost:  271
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  310362   807744 |   93108       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/132244          
c   -- var.elim.:  2000/132244          
c   -- var.elim.:  3000/132244          
c   -- var.elim.:  4000/132244          
c   -- var.elim.:  5000/132244          
c   -- var.elim.:  6000/132244          
c   -- var.elim.:  7000/132244          
c   -- var.elim.:  8000/132244          
c   -- var.elim.:  9000/132244          
c   -- var.elim.:  10000/132244          
c   -- var.elim.:  11000/132244          
c   -- var.elim.:  12000/132244          
c   -- var.elim.:  13000/132244          
c   -- var.elim.:  14000/132244          
c   -- var.elim.:  15000/132244          
c   -- var.elim.:  16000/132244          
c   -- var.elim.:  17000/132244          
c   -- var.elim.:  18000/132244          
c   -- var.elim.:  19000/132244          
c   -- var.elim.:  20000/132244          
c   -- var.elim.:  21000/132244          
c   -- var.elim.:  22000/132244          
c   -- var.elim.:  23000/132244          
c   -- var.elim.:  24000/132244          
c   -- var.elim.:  25000/132244          
c   -- var.elim.:  26000/132244          
c   -- var.elim.:  27000/132244          
c   -- var.elim.:  28000/132244          
c   -- var.elim.:  29000/132244          
c   -- var.elim.:  30000/132244          
c   -- var.elim.:  31000/132244          
c   -- var.elim.:  32000/132244          
c   -- var.elim.:  33000/132244          
c   -- var.elim.:  34000/132244          
c   -- var.elim.:  35000/132244          
c   -- var.elim.:  36000/132244          
c   -- var.elim.:  37000/132244          
c   -- var.elim.:  38000/132244          
c   -- var.elim.:  39000/132244          
c   -- var.elim.:  40000/132244          
c   -- var.elim.:  41000/132244          
c   -- var.elim.:  42000/132244          
c   -- var.elim.:  43000/132244          
c   -- var.elim.:  44000/132244          
c   -- var.elim.:  45000/132244          
c   -- var.elim.:  46000/132244          
c   -- var.elim.:  47000/132244          
c   -- var.elim.:  48000/132244          
c   -- var.elim.:  49000/132244          
c   -- var.elim.:  50000/132244          
c   -- var.elim.:  51000/132244          
c   -- var.elim.:  52000/132244          
c   -- var.elim.:  53000/132244          
c   -- var.elim.:  54000/132244          
c   -- var.elim.:  55000/132244          
c   -- var.elim.:  56000/132244          
c   -- var.elim.:  57000/132244          
c   -- var.elim.:  58000/132244          
c   -- var.elim.:  59000/132244          
c   -- var.elim.:  60000/132244          
c   -- var.elim.:  61000/132244          
c   -- var.elim.:  62000/132244          
c   -- var.elim.:  63000/132244          
c   -- var.elim.:  64000/132244          
c   -- var.elim.:  65000/132244          
c   -- var.elim.:  66000/132244          
c   -- var.elim.:  67000/132244          
c   -- var.elim.:  68000/132244          
c   -- var.elim.:  69000/132244          
c   -- var.elim.:  70000/132244          
c   -- var.elim.:  71000/132244          
c   -- var.elim.:  72000/132244          
c   -- var.elim.:  73000/132244          
c   -- var.elim.:  74000/132244          
c   -- var.elim.:  75000/132244          
c   -- var.elim.:  76000/132244          
c   -- var.elim.:  77000/132244          
c   -- var.elim.:  78000/132244          
c   -- var.elim.:  79000/132244          
c   -- var.elim.:  80000/132244          
c   -- var.elim.:  81000/132244          
c   -- var.elim.:  82000/132244          
c   -- var.elim.:  83000/132244          
c   -- var.elim.:  84000/132244          
c   -- var.elim.:  85000/132244          
c   -- var.elim.:  86000/132244          
c   -- var.elim.:  87000/132244          
c   -- var.elim.:  88000/132244          
c   -- var.elim.:  89000/132244          
c   -- var.elim.:  90000/132244          
c   -- var.elim.:  91000/132244          
c   -- var.elim.:  92000/132244          
c   -- var.elim.:  93000/132244          
c   -- var.elim.:  94000/132244          
c   -- var.elim.:  95000/132244          
c   -- var.elim.:  96000/132244          
c   -- var.elim.:  97000/132244          
c   -- var.elim.:  98000/132244          
c   -- var.elim.:  99000/132244          
c   -- var.elim.:  100000/132244          
c   -- var.elim.:  101000/132244          
c   -- var.elim.:  102000/132244          
c   -- var.elim.:  103000/132244          
c   -- var.elim.:  104000/132244          
c   -- var.elim.:  105000/132244          
c   -- var.elim.:  106000/132244          
c   -- var.elim.:  107000/132244          
c   -- var.elim.:  108000/132244          
c   -- var.elim.:  109000/132244          
c   -- var.elim.:  110000/132244          
c   -- var.elim.:  111000/132244          
c   -- var.elim.:  112000/132244          
c   -- var.elim.:  113000/132244          
c   -- var.elim.:  114000/132244          
c   -- var.elim.:  115000/132244          
c   -- var.elim.:  116000/132244          
c   -- var.elim.:  117000/132244          
c   -- var.elim.:  118000/132244          
c   -- var.elim.:  119000/132244          
c   -- var.elim.:  120000/132244          
c   -- var.elim.:  121000/132244          
c   -- var.elim.:  122000/132244          
c   -- var.elim.:  123000/132244          
c   -- var.elim.:  124000/132244          
c   -- var.elim.:  125000/132244          
c   -- var.elim.:  126000/132244          
c   -- var.elim.:  127000/132244          
c   -- var.elim.:  128000/132244          
c   -- var.elim.:  129000/132244          
c   -- var.elim.:  130000/132244          
c   -- var.elim.:  131000/132244          
c   -- var.elim.:  132000/132244          
c   -- var.elim.:  132244/132244          
c   -- var.elim.:  1000/3150          
c   -- var.elim.:  2000/3150          
c   -- var.elim.:  3000/3150          
c   -- var.elim.:  3150/3150          
c   -- subsuming                       
c   -- var.elim.:  1000/2720          
c   -- var.elim.:  2000/2720          
c   -- var.elim.:  2720/2720          
c   -- var.elim.:  1000/2148          
c   -- var.elim.:  2000/2148          
c   -- var.elim.:  2148/2148          
c   -- subsuming                       
c   -- var.elim.:  1000/1939          
c   -- var.elim.:  1939/1939          
c   -- var.elim.:  15/15          
c |         0 |  307154   797431 |      --       0       --      -- |     --   | -3202/-7951
c |         0 |  307154   797431 |  122861       0        0     nan |  0.000 % |
c |       100 |  307154   797431 |  135147     100     3726    37.3 |  0.597 % |
c |       251 |  307142   797395 |  148656     250    11360    45.4 |  0.598 % |
c |       476 |  307130   797363 |  163516     474    34301    72.4 |  0.599 % |
c |       813 |  307106   797292 |  179853     808    48426    59.9 |  0.599 % |
c |      1319 |  307082   797221 |  197823    1313    82269    62.7 |  0.600 % |
c |      207#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.91 2/54 16213
Raw data (stat): 16213 (runsolver) R 16212 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543725113 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 20813 0 0 0 946 51 0 0 25 0 1 0 543725113 93679616 18590 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22871 18590 603 41 0 22830 0
vsize: 91484
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 21100 0 0 0 1945 52 0 0 25 0 1 0 543725113 94994432 18877 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23192 18877 603 41 0 23151 0
vsize: 92768
[startup+30.0029 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 21426 0 0 0 2944 54 0 0 25 0 1 0 543725113 96448512 19203 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23547 19203 603 41 0 23506 0
vsize: 94188
[startup+40.0038 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 21626 0 0 0 3943 55 0 0 25 0 1 0 543725113 97247232 19403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23742 19403 603 41 0 23701 0
vsize: 94968
[startup+50.0042 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 21891 0 0 0 4942 56 0 0 25 0 1 0 543725113 98234368 19668 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23983 19668 603 41 0 23942 0
vsize: 95932
[startup+60.0054 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 22216 0 0 0 5941 57 0 0 25 0 1 0 543725113 99553280 19993 4294967295 134512640 134672761 3221224544 3221223536 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24305 19993 603 41 0 24264 0
vsize: 97220
[startup+70.0062 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 22770 0 0 0 6940 58 0 0 25 0 1 0 543725113 101928960 20547 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24885 20547 603 41 0 24844 0
vsize: 99540
[startup+80.0066 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 23103 0 0 0 7938 60 0 0 25 0 1 0 543725113 103256064 20880 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25209 20880 603 41 0 25168 0
vsize: 100836
[startup+90.0069 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 23412 0 0 0 8937 61 0 0 25 0 1 0 543725113 104611840 21189 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25540 21189 603 41 0 25499 0
vsize: 102160
[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 23812 0 0 0 9936 62 0 0 25 0 1 0 543725113 106201088 21589 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25928 21589 603 41 0 25887 0
vsize: 103712
[startup+110.007 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 24147 0 0 0 10935 63 0 0 25 0 1 0 543725113 107646976 21924 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26281 21924 603 41 0 26240 0
vsize: 105124
[startup+120.007 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 24588 0 0 0 11934 65 0 0 25 0 1 0 543725113 109371392 22365 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26702 22365 603 41 0 26661 0
vsize: 106808
[startup+130.008 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 24961 0 0 0 12933 66 0 0 25 0 1 0 543725113 110972928 22738 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27093 22738 603 41 0 27052 0
vsize: 108372
[startup+140.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 25350 0 0 0 13931 67 0 0 25 0 1 0 543725113 112553984 23127 4294967295 134512640 134672761 3221224544 3221223704 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27479 23127 603 41 0 27438 0
vsize: 109916
[startup+150.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 26010 0 0 0 14929 70 0 0 25 0 1 0 543725113 115179520 23787 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28120 23787 603 41 0 28079 0
vsize: 112480
[startup+160.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 26294 0 0 0 15928 71 0 0 25 0 1 0 543725113 116375552 24071 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28412 24071 603 41 0 28371 0
vsize: 113648
[startup+170.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 26681 0 0 0 16927 72 0 0 25 0 1 0 543725113 118087680 24458 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28830 24458 603 41 0 28789 0
vsize: 115320
[startup+180.011 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 27124 0 0 0 17926 74 0 0 25 0 1 0 543725113 119934976 24901 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29281 24901 603 41 0 29240 0
vsize: 117124
[startup+190.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 27611 0 0 0 18925 75 0 0 25 0 1 0 543725113 121802752 25388 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29737 25388 603 41 0 29696 0
vsize: 118948
[startup+200.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 28308 0 0 0 19923 77 0 0 25 0 1 0 543725113 124694528 26085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30443 26085 603 41 0 30402 0
vsize: 121772
[startup+210.014 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 28643 0 0 0 20922 78 0 0 25 0 1 0 543725113 126021632 26420 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30767 26420 603 41 0 30726 0
vsize: 123068
[startup+220.015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 29073 0 0 0 21921 79 0 0 25 0 1 0 543725113 127881216 26850 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31221 26850 603 41 0 31180 0
vsize: 124884
[startup+230.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 29379 0 0 0 22920 80 0 0 25 0 1 0 543725113 129073152 27156 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31512 27156 603 41 0 31471 0
vsize: 126048
[startup+240.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 29797 0 0 0 23919 81 0 0 25 0 1 0 543725113 130785280 27574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31930 27574 603 41 0 31889 0
vsize: 127720
[startup+250.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 30346 0 0 0 24918 83 0 0 25 0 1 0 543725113 133025792 28123 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32477 28123 603 41 0 32436 0
vsize: 129908
[startup+260.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 30772 0 0 0 25916 84 0 0 25 0 1 0 543725113 134746112 28549 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32897 28549 603 41 0 32856 0
vsize: 131588
[startup+270.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 31086 0 0 0 26915 85 0 0 25 0 1 0 543725113 136060928 28863 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33218 28863 603 41 0 33177 0
vsize: 132872
[startup+280.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 31563 0 0 0 27914 87 0 0 25 0 1 0 543725113 137920512 29340 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33672 29340 603 41 0 33631 0
vsize: 134688
[startup+290.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 31938 0 0 0 28913 88 0 0 25 0 1 0 543725113 139509760 29715 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34060 29715 603 41 0 34019 0
vsize: 136240
[startup+300.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 32456 0 0 0 29912 89 0 0 25 0 1 0 543725113 141619200 30233 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34575 30233 603 41 0 34534 0
vsize: 138300
[startup+310.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 32980 0 0 0 30910 91 0 0 25 0 1 0 543725113 143736832 30757 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35092 30757 603 41 0 35051 0
vsize: 140368
[startup+320.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 33494 0 0 0 31908 93 0 0 25 0 1 0 543725113 145842176 31271 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35606 31271 603 41 0 35565 0
vsize: 142424
[startup+330.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 33914 0 0 0 32907 94 0 0 25 0 1 0 543725113 147558400 31691 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36025 31691 603 41 0 35984 0
vsize: 144100
[startup+340.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 34510 0 0 0 33904 97 0 0 25 0 1 0 543725113 150061056 32287 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36636 32287 603 41 0 36595 0
vsize: 146544
[startup+350.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 35283 0 0 0 34902 99 0 0 25 0 1 0 543725113 153485312 33060 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37472 33060 603 41 0 37431 0
vsize: 149888
[startup+360.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 35726 0 0 0 35901 101 0 0 25 0 1 0 543725113 155205632 33503 4294967295 134512640 134672761 3221224544 3221223668 134566024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37892 33503 603 41 0 37851 0
vsize: 151568
[startup+370.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 36079 0 0 0 36899 103 0 0 25 0 1 0 543725113 156651520 33856 4294967295 134512640 134672761 3221224544 3221223688 134616339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38245 33856 603 41 0 38204 0
vsize: 152980
[startup+380.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 36549 0 0 0 37898 104 0 0 25 0 1 0 543725113 158633984 34326 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38729 34326 603 41 0 38688 0
vsize: 154916
[startup+390.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 36872 0 0 0 38897 105 0 0 25 0 1 0 543725113 159965184 34649 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39054 34649 603 41 0 39013 0
vsize: 156216
[startup+400.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 37309 0 0 0 39896 106 0 0 25 0 1 0 543725113 161689600 35086 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39475 35086 603 41 0 39434 0
vsize: 157900
[startup+410.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 37649 0 0 0 40895 107 0 0 25 0 1 0 543725113 163160064 35426 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39834 35426 603 41 0 39793 0
vsize: 159336
[startup+420.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 38289 0 0 0 41893 109 0 0 25 0 1 0 543725113 165658624 36066 4294967295 134512640 134672761 3221224544 3221223704 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40444 36066 603 41 0 40403 0
vsize: 161776
[startup+430.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 39089 0 0 0 42891 112 0 0 25 0 1 0 543725113 168964096 36866 4294967295 134512640 134672761 3221224544 3221223584 134612630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41251 36866 603 41 0 41210 0
vsize: 165004
[startup+440.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 39503 0 0 0 43890 113 0 0 25 0 1 0 543725113 170684416 37280 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41671 37280 603 41 0 41630 0
vsize: 166684
[startup+450.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 39821 0 0 0 44889 114 0 0 25 0 1 0 543725113 172007424 37598 4294967295 134512640 134672761 3221224544 3221223728 134615843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41994 37598 603 41 0 41953 0
vsize: 167976
[startup+460.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 40198 0 0 0 45888 115 0 0 25 0 1 0 543725113 173461504 37975 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42349 37975 603 41 0 42308 0
vsize: 169396
[startup+470.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 40589 0 0 0 46887 116 0 0 25 0 1 0 543725113 175050752 38366 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42737 38366 603 41 0 42696 0
vsize: 170948
[startup+480.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 40913 0 0 0 47886 117 0 0 25 0 1 0 543725113 176373760 38690 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43060 38690 603 41 0 43019 0
vsize: 172240
[startup+490.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 41731 0 0 0 48884 120 0 0 25 0 1 0 543725113 179781632 39508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43892 39508 603 41 0 43851 0
vsize: 175568
[startup+500.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 42416 0 0 0 49882 122 0 0 25 0 1 0 543725113 182517760 40193 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44560 40193 603 41 0 44519 0
vsize: 178240
[startup+510.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 42685 0 0 0 50881 123 0 0 25 0 1 0 543725113 183709696 40462 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44851 40462 603 41 0 44810 0
vsize: 179404
[startup+520.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 43073 0 0 0 51880 124 0 0 25 0 1 0 543725113 185298944 40850 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45239 40850 603 41 0 45198 0
vsize: 180956
[startup+530.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 43338 0 0 0 52879 125 0 0 25 0 1 0 543725113 186351616 41115 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45496 41115 603 41 0 45455 0
vsize: 181984
[startup+540.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 43803 0 0 0 53878 127 0 0 25 0 1 0 543725113 188203008 41580 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45948 41580 603 41 0 45907 0
vsize: 183792
[startup+550.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 44266 0 0 0 54877 128 0 0 25 0 1 0 543725113 190181376 42043 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46431 42043 603 41 0 46390 0
vsize: 185724
[startup+560.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 44669 0 0 0 55876 129 0 0 25 0 1 0 543725113 191754240 42446 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46815 42446 603 41 0 46774 0
vsize: 187260
[startup+570.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 44982 0 0 0 56876 129 0 0 25 0 1 0 543725113 193077248 42759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47138 42759 603 41 0 47097 0
vsize: 188552
[startup+580.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 45279 0 0 0 57875 130 0 0 25 0 1 0 543725113 194281472 43056 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47432 43056 603 41 0 47391 0
vsize: 189728
[startup+590.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 45840 0 0 0 58873 132 0 0 25 0 1 0 543725113 196632576 43617 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48006 43617 603 41 0 47965 0
vsize: 192024
[startup+600.036 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 46476 0 0 0 59871 134 0 0 25 0 1 0 543725113 199127040 44253 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48615 44253 603 41 0 48574 0
vsize: 194460
[startup+610.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 47049 0 0 0 60870 136 0 0 25 0 1 0 543725113 201474048 44826 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49188 44826 603 41 0 49147 0
vsize: 196752
[startup+620.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 47593 0 0 0 61869 137 0 0 25 0 1 0 543725113 203722752 45370 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49737 45370 603 41 0 49696 0
vsize: 198948
[startup+630.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 47796 0 0 0 62868 138 0 0 25 0 1 0 543725113 204513280 45573 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49930 45573 603 41 0 49889 0
vsize: 199720
[startup+640.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 48224 0 0 0 63867 139 0 0 25 0 1 0 543725113 206323712 46001 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50372 46001 603 41 0 50331 0
vsize: 201488
[startup+650.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 48575 0 0 0 64866 140 0 0 25 0 1 0 543725113 207769600 46352 4294967295 134512640 134672761 3221224544 3221223584 134612797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50725 46352 603 41 0 50684 0
vsize: 202900
[startup+660.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 48993 0 0 0 65866 141 0 0 25 0 1 0 543725113 209469440 46770 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51140 46770 603 41 0 51099 0
vsize: 204560
[startup+670.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 49703 0 0 0 66864 142 0 0 25 0 1 0 543725113 212369408 47480 4294967295 134512640 134672761 3221224544 3221223416 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51848 47480 603 41 0 51807 0
vsize: 207392
[startup+680.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 50164 0 0 0 67863 144 0 0 25 0 1 0 543725113 214224896 47941 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52301 47941 603 41 0 52260 0
vsize: 209204
[startup+690.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 50354 0 0 0 68862 145 0 0 25 0 1 0 543725113 215015424 48131 4294967295 134512640 134672761 3221224544 3221223688 134616154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52494 48131 603 41 0 52453 0
vsize: 209976
[startup+700.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 50966 0 0 0 69861 146 0 0 25 0 1 0 543725113 217489408 48743 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53098 48743 603 41 0 53057 0
vsize: 212392
[startup+710.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 51348 0 0 0 70860 148 0 0 25 0 1 0 543725113 219070464 49125 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53484 49125 603 41 0 53443 0
vsize: 213936
[startup+720.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 51983 0 0 0 71857 150 0 0 25 0 1 0 543725113 221691904 49760 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54124 49760 603 41 0 54083 0
vsize: 216496
[startup+730.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 52599 0 0 0 72855 152 0 0 25 0 1 0 543725113 224215040 50376 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54740 50376 603 41 0 54699 0
vsize: 218960
[startup+740.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 52971 0 0 0 73853 154 0 0 25 0 1 0 543725113 225677312 50748 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55097 50748 603 41 0 55056 0
vsize: 220388
[startup+750.038 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 53415 0 0 0 74852 156 0 0 25 0 1 0 543725113 227520512 51192 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55547 51192 603 41 0 55506 0
vsize: 222188
[startup+760.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 53620 0 0 0 75852 156 0 0 25 0 1 0 543725113 228433920 51397 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55770 51397 603 41 0 55729 0
vsize: 223080
[startup+770.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 54013 0 0 0 76851 158 0 0 25 0 1 0 543725113 230002688 51790 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56153 51790 603 41 0 56112 0
vsize: 224612
[startup+780.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 54250 0 0 0 77850 158 0 0 25 0 1 0 543725113 230932480 52027 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56380 52028 603 41 0 56339 0
vsize: 225520
[startup+790.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 54621 0 0 0 78849 159 0 0 25 0 1 0 543725113 232517632 52398 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56767 52398 603 41 0 56726 0
vsize: 227068
[startup+800.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 55017 0 0 0 79849 160 0 0 25 0 1 0 543725113 234086400 52794 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57150 52794 603 41 0 57109 0
vsize: 228600
[startup+810.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 55436 0 0 0 80848 161 0 0 25 0 1 0 543725113 235802624 53213 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57569 53213 603 41 0 57528 0
vsize: 230276
[startup+820.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 55790 0 0 0 81847 162 0 0 25 0 1 0 543725113 237264896 53567 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57926 53567 603 41 0 57885 0
vsize: 231704
[startup+830.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 56153 0 0 0 82846 164 0 0 25 0 1 0 543725113 238698496 53930 4294967295 134512640 134672761 3221224544 3221223688 134616256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58276 53930 603 41 0 58235 0
vsize: 233104
[startup+840.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 56427 0 0 0 83845 165 0 0 25 0 1 0 543725113 239886336 54204 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58566 54204 603 41 0 58525 0
vsize: 234264
[startup+850.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 56638 0 0 0 84845 165 0 0 25 0 1 0 543725113 240693248 54415 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58763 54415 603 41 0 58722 0
vsize: 235052
[startup+860.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 56887 0 0 0 85844 166 0 0 25 0 1 0 543725113 241750016 54664 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59021 54664 603 41 0 58980 0
vsize: 236084
[startup+870.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 57304 0 0 0 86842 168 0 0 25 0 1 0 543725113 243470336 55081 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59441 55081 603 41 0 59400 0
vsize: 237764
[startup+880.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 57568 0 0 0 87841 169 0 0 25 0 1 0 543725113 244527104 55345 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59699 55345 603 41 0 59658 0
vsize: 238796
[startup+890.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 57815 0 0 0 88841 170 0 0 25 0 1 0 543725113 245444608 55592 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59923 55592 603 41 0 59882 0
vsize: 239692
[startup+900.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 58048 0 0 0 89840 171 0 0 25 0 1 0 543725113 246505472 55825 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60182 55825 603 41 0 60141 0
vsize: 240728
[startup+910.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 58375 0 0 0 90839 172 0 0 25 0 1 0 543725113 247816192 56152 4294967295 134512640 134672761 3221224544 3221223584 134612741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60502 56152 603 41 0 60461 0
vsize: 242008
[startup+920.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 58590 0 0 0 91839 173 0 0 25 0 1 0 543725113 248610816 56367 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60696 56367 603 41 0 60655 0
vsize: 242784
[startup+930.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 59196 0 0 0 92838 174 0 0 25 0 1 0 543725113 251633664 56973 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61434 56973 603 41 0 61393 0
vsize: 245736
[startup+940.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 59596 0 0 0 93836 175 0 0 25 0 1 0 543725113 253341696 57373 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61851 57373 603 41 0 61810 0
vsize: 247404
[startup+950.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 59935 0 0 0 94836 176 0 0 25 0 1 0 543725113 254672896 57712 4294967295 134512640 134672761 3221224544 3221223688 134616261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62176 57712 603 41 0 62135 0
vsize: 248704
[startup+960.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 60104 0 0 0 95836 176 0 0 25 0 1 0 543725113 255328256 57881 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62336 57881 603 41 0 62295 0
vsize: 249344
[startup+970.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 60295 0 0 0 96835 177 0 0 25 0 1 0 543725113 256118784 58072 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62529 58072 603 41 0 62488 0
vsize: 250116
[startup+980.042 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 60552 0 0 0 97835 178 0 0 25 0 1 0 543725113 257167360 58329 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62785 58329 603 41 0 62744 0
vsize: 251140
[startup+990.042 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 61128 0 0 0 98833 179 0 0 25 0 1 0 543725113 259543040 58905 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63365 58905 603 41 0 63324 0
vsize: 253460
[startup+1000.04 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 61702 0 0 0 99832 181 0 0 25 0 1 0 543725113 261918720 59479 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63945 59479 603 41 0 63904 0
vsize: 255780
[startup+1010.04 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 61962 0 0 0 100831 182 0 0 25 0 1 0 543725113 262979584 59739 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64204 59739 603 41 0 64163 0
vsize: 256816
[startup+1020.04 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 16213
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 62401 0 0 0 101830 183 0 0 25 0 1 0 543725113 264826880 60178 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64655 60178 603 41 0 64614 0
vsize: 258620
[startup+1030.04 s]
Raw data (loadavg): 1.06 1.02 0.93 3/57 16250
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 62813 0 0 0 102829 184 0 0 25 0 1 0 543725113 266420224 60590 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65044 60590 603 41 0 65003 0
vsize: 260176
[startup+1040.04 s]
Raw data (loadavg): 1.13 1.03 0.93 2/54 16266
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 63273 0 0 0 103824 189 0 0 25 0 1 0 543725113 268288000 61050 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65500 61050 603 41 0 65459 0
vsize: 262000
[startup+1050.04 s]
Raw data (loadavg): 1.11 1.03 0.93 2/54 16266
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 63758 0 0 0 104823 190 0 0 25 0 1 0 543725113 270266368 61535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65983 61535 603 41 0 65942 0
vsize: 263932
[startup+1060.05 s]
Raw data (loadavg): 1.09 1.03 0.93 2/54 16266
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 64412 0 0 0 105822 192 0 0 25 0 1 0 543725113 273014784 62189 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66654 62189 603 41 0 66613 0
vsize: 266616
[startup+1070.05 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 16266
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 64957 0 0 0 106821 193 0 0 25 0 1 0 543725113 275234816 62734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67196 62734 603 41 0 67155 0
vsize: 268784
[startup+1080.05 s]
Raw data (loadavg): 1.06 1.03 0.93 2/54 16266
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 65324 0 0 0 107820 195 0 0 25 0 1 0 543725113 276684800 63101 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67550 63101 603 41 0 67509 0
vsize: 270200
[startup+1090.05 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 16266
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 65859 0 0 0 108819 196 0 0 25 0 1 0 543725113 278925312 63636 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68097 63636 603 41 0 68056 0
vsize: 272388
[startup+1100.05 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 16266
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 66949 0 0 0 109816 199 0 0 25 0 1 0 543725113 283332608 64726 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69173 64726 603 41 0 69132 0
vsize: 276692
[startup+1110.05 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 67146 0 0 0 110815 200 0 0 25 0 1 0 543725113 284135424 64923 4294967295 134512640 134672761 3221224544 3221223680 134614664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69369 64923 603 41 0 69328 0
vsize: 277476
[startup+1120.05 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 67357 0 0 0 111815 201 0 0 25 0 1 0 543725113 285061120 65134 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69595 65134 603 41 0 69554 0
vsize: 278380
[startup+1130.05 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 67626 0 0 0 112814 202 0 0 25 0 1 0 543725113 286117888 65403 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69853 65403 603 41 0 69812 0
vsize: 279412
[startup+1140.05 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 67903 0 0 0 113813 203 0 0 25 0 1 0 543725113 287285248 65680 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70138 65680 603 41 0 70097 0
vsize: 280552
[startup+1150.05 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 68191 0 0 0 114812 204 0 0 25 0 1 0 543725113 288468992 65968 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70427 65968 603 41 0 70386 0
vsize: 281708
[startup+1160.05 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 68481 0 0 0 115811 205 0 0 25 0 1 0 543725113 289648640 66258 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70715 66258 603 41 0 70674 0
vsize: 282860
[startup+1170.05 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 68831 0 0 0 116810 206 0 0 25 0 1 0 543725113 291110912 66608 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71072 66608 603 41 0 71031 0
vsize: 284288
[startup+1180.05 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 69670 0 0 0 117808 208 0 0 25 0 1 0 543725113 294416384 67447 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71912 67448 603 41 0 71871 0
vsize: 287516
[startup+1190.05 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 71064 0 0 0 118805 212 0 0 25 0 1 0 543725113 300240896 68841 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73301 68841 603 41 0 73260 0
vsize: 293204
[startup+1200.05 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 16268
Raw data (stat): 16213 (minisat+) R 16212 18865 18864 0 -1 0 71349 0 0 0 119805 212 0 0 25 0 1 0 543725113 301416448 69126 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73588 69126 603 41 0 73547 0
vsize: 294352
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.01 1.01 0.93 1/54 16268
Raw data (stat): 16213 (minisat+) Z 16212 18865 18864 0 -1 12 71349 0 0 0 119805 225 0 0 25 0 1 0 543725113 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: 0
Real time (s): 1200.19
CPU time (s): 1200.31
CPU user time (s): 1198.05
CPU system time (s): 2.25466
CPU usage (%): 100.01
Max. virtual memory (Kb): 294352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####