PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-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	1176.04
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 18819

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 16:42:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17431 boxname=wulflinc24 idbench=1341 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ee388359e66788d310d5d5b34d6465c1  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-air04.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 17431
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        784080 kB
Buffers:         28856 kB
Cached:         197196 kB
SwapCached:        524 kB
Active:          81752 kB
Inactive:       146296 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        783828 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16928 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:02:15 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 17431 7 1200.32 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.93 0.97 0.91 2/54 12850
Raw data (stat): 12850 (runsolver) R 12849 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546600541 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+9.99995 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 20812 0 0 0 946 52 0 0 25 0 1 0 546600541 93679616 18589 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22871 18589 603 41 0 22830 0
vsize: 91484
[startup+20 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 21092 0 0 0 1944 53 0 0 25 0 1 0 546600541 94994432 18869 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23192 18869 603 41 0 23151 0
vsize: 92768
[startup+30.0002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 21403 0 0 0 2943 54 0 0 25 0 1 0 546600541 96313344 19180 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23514 19180 603 41 0 23473 0
vsize: 94056
[startup+39.9999 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 21597 0 0 0 3943 54 0 0 25 0 1 0 546600541 97116160 19374 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23710 19374 603 41 0 23669 0
vsize: 94840
[startup+50.0006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 21848 0 0 0 4942 56 0 0 25 0 1 0 546600541 98103296 19625 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23951 19625 603 41 0 23910 0
vsize: 95804
[startup+60.0006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 22146 0 0 0 5942 56 0 0 25 0 1 0 546600541 99287040 19923 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24240 19923 603 41 0 24199 0
vsize: 96960
[startup+70 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 22648 0 0 0 6940 57 0 0 25 0 1 0 546600541 101400576 20425 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 20425 603 41 0 24715 0
vsize: 99024
[startup+80.0011 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 23057 0 0 0 7939 59 0 0 25 0 1 0 546600541 103120896 20834 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25176 20834 603 41 0 25135 0
vsize: 100704
[startup+90.0004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 23334 0 0 0 8938 60 0 0 25 0 1 0 546600541 104345600 21111 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25475 21111 603 41 0 25434 0
vsize: 101900
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 23760 0 0 0 9938 60 0 0 25 0 1 0 546600541 106065920 21537 4294967295 134512640 134672761 3221224544 3221223680 134614551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25895 21537 603 41 0 25854 0
vsize: 103580
[startup+110.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 24009 0 0 0 10937 61 0 0 25 0 1 0 546600541 106991616 21786 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26121 21786 603 41 0 26080 0
vsize: 104484
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 24436 0 0 0 11936 62 0 0 25 0 1 0 546600541 108838912 22213 4294967295 134512640 134672761 3221224544 3221223584 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26572 22213 603 41 0 26531 0
vsize: 106288
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 24783 0 0 0 12936 63 0 0 25 0 1 0 546600541 110174208 22560 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26898 22560 603 41 0 26857 0
vsize: 107592
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 25178 0 0 0 13934 64 0 0 25 0 1 0 546600541 111763456 22955 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27286 22955 603 41 0 27245 0
vsize: 109144
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 25796 0 0 0 14932 67 0 0 25 0 1 0 546600541 114262016 23573 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27896 23573 603 41 0 27855 0
vsize: 111584
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 26162 0 0 0 15931 68 0 0 25 0 1 0 546600541 115843072 23939 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28282 23939 603 41 0 28241 0
vsize: 113128
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 26514 0 0 0 16930 69 0 0 25 0 1 0 546600541 117301248 24291 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28638 24291 603 41 0 28597 0
vsize: 114552
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 26919 0 0 0 17930 70 0 0 25 0 1 0 546600541 119013376 24696 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29056 24696 603 41 0 29015 0
vsize: 116224
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 27365 0 0 0 18928 72 0 0 25 0 1 0 546600541 120868864 25142 4294967295 134512640 134672761 3221224544 3221223692 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29509 25142 603 41 0 29468 0
vsize: 118036
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 27971 0 0 0 19927 73 0 0 25 0 1 0 546600541 123383808 25748 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30123 25748 603 41 0 30082 0
vsize: 120492
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 28410 0 0 0 20925 75 0 0 25 0 1 0 546600541 125095936 26187 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30541 26187 603 41 0 30500 0
vsize: 122164
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 28841 0 0 0 21924 77 0 0 25 0 1 0 546600541 126816256 26618 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30961 26618 603 41 0 30920 0
vsize: 123844
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 29171 0 0 0 22923 78 0 0 25 0 1 0 546600541 128282624 26948 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31319 26948 603 41 0 31278 0
vsize: 125276
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 29506 0 0 0 23922 79 0 0 25 0 1 0 546600541 129601536 27283 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31641 27283 603 41 0 31600 0
vsize: 126564
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 30079 0 0 0 24920 81 0 0 25 0 1 0 546600541 131973120 27856 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32220 27856 603 41 0 32179 0
vsize: 128880
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 30439 0 0 0 25920 81 0 0 25 0 1 0 546600541 133423104 28216 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32574 28216 603 41 0 32533 0
vsize: 130296
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 30932 0 0 0 26918 83 0 0 25 0 1 0 546600541 135405568 28709 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33058 28709 603 41 0 33017 0
vsize: 132232
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 31217 0 0 0 27917 84 0 0 25 0 1 0 546600541 136589312 28994 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33347 28994 603 41 0 33306 0
vsize: 133388
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 31626 0 0 0 28916 85 0 0 25 0 1 0 546600541 138182656 29403 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33736 29403 603 41 0 33695 0
vsize: 134944
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 31981 0 0 0 29915 87 0 0 25 0 1 0 546600541 139644928 29758 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34093 29758 603 41 0 34052 0
vsize: 136372
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 32632 0 0 0 30914 88 0 0 25 0 1 0 546600541 142409728 30409 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34768 30409 603 41 0 34727 0
vsize: 139072
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 33007 0 0 0 31912 90 0 0 25 0 1 0 546600541 143863808 30784 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35123 30784 603 41 0 35082 0
vsize: 140492
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 33575 0 0 0 32911 92 0 0 25 0 1 0 546600541 146231296 31352 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35701 31352 603 41 0 35660 0
vsize: 142804
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 33914 0 0 0 33910 93 0 0 25 0 1 0 546600541 147558400 31691 4294967295 134512640 134672761 3221224544 3221223688 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36025 31691 603 41 0 35984 0
vsize: 144100
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 34569 0 0 0 34908 94 0 0 25 0 1 0 546600541 150192128 32346 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36668 32346 603 41 0 36627 0
vsize: 146672
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 35317 0 0 0 35906 97 0 0 25 0 1 0 546600541 153616384 33094 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37504 33094 603 41 0 37463 0
vsize: 150016
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 35727 0 0 0 36905 98 0 0 25 0 1 0 546600541 155205632 33504 4294967295 134512640 134672761 3221224544 3221223668 134565986 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37892 33504 603 41 0 37851 0
vsize: 151568
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 36079 0 0 0 37904 99 0 0 25 0 1 0 546600541 156651520 33856 4294967295 134512640 134672761 3221224544 3221223688 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38245 33856 603 41 0 38204 0
vsize: 152980
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 36544 0 0 0 38903 101 0 0 25 0 1 0 546600541 158633984 34321 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38729 34321 603 41 0 38688 0
vsize: 154916
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 36838 0 0 0 39902 102 0 0 25 0 1 0 546600541 159834112 34615 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39022 34615 603 41 0 38981 0
vsize: 156088
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 37274 0 0 0 40901 103 0 0 25 0 1 0 546600541 161558528 35051 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39443 35051 603 41 0 39402 0
vsize: 157772
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 37588 0 0 0 41900 104 0 0 25 0 1 0 546600541 162885632 35365 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39767 35365 603 41 0 39726 0
vsize: 159068
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 38163 0 0 0 42898 106 0 0 25 0 1 0 546600541 165269504 35940 4294967295 134512640 134672761 3221224544 3221223348 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40348 35940 603 41 0 40307 0
vsize: 161396
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 38916 0 0 0 43897 108 0 0 25 0 1 0 546600541 168296448 36693 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41088 36693 603 41 0 41047 0
vsize: 164352
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 39440 0 0 0 44895 110 0 0 25 0 1 0 546600541 170418176 37217 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41606 37217 603 41 0 41565 0
vsize: 166424
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 39726 0 0 0 45894 111 0 0 25 0 1 0 546600541 171614208 37503 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41898 37503 603 41 0 41857 0
vsize: 167592
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 40091 0 0 0 46893 112 0 0 25 0 1 0 546600541 173068288 37868 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42253 37868 603 41 0 42212 0
vsize: 169012
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 40475 0 0 0 47892 113 0 0 25 0 1 0 546600541 174653440 38252 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42640 38252 603 41 0 42599 0
vsize: 170560
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 40812 0 0 0 48892 113 0 0 25 0 1 0 546600541 175976448 38589 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42963 38589 603 41 0 42922 0
vsize: 171852
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 41371 0 0 0 49891 115 0 0 25 0 1 0 546600541 178343936 39148 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43541 39148 603 41 0 43500 0
vsize: 174164
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 42333 0 0 0 50889 117 0 0 25 0 1 0 546600541 182247424 40110 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44494 40110 603 41 0 44453 0
vsize: 177976
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 42614 0 0 0 51889 117 0 0 25 0 1 0 546600541 183316480 40391 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44755 40391 603 41 0 44714 0
vsize: 179020
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 42899 0 0 0 52888 118 0 0 25 0 1 0 546600541 184500224 40676 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45044 40676 603 41 0 45003 0
vsize: 180176
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 43212 0 0 0 53887 119 0 0 25 0 1 0 546600541 185819136 40989 4294967295 134512640 134672761 3221224544 3221223688 134616108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45366 40989 603 41 0 45325 0
vsize: 181464
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 43599 0 0 0 54887 120 0 0 25 0 1 0 546600541 187400192 41376 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45752 41376 603 41 0 45711 0
vsize: 183008
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 43945 0 0 0 55886 121 0 0 25 0 1 0 546600541 188866560 41722 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46110 41722 603 41 0 46069 0
vsize: 184440
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 44465 0 0 0 56885 122 0 0 25 0 1 0 546600541 190976000 42242 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46625 42242 603 41 0 46584 0
vsize: 186500
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 44807 0 0 0 57884 123 0 0 25 0 1 0 546600541 192282624 42584 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46944 42584 603 41 0 46903 0
vsize: 187776
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 45079 0 0 0 58883 124 0 0 25 0 1 0 546600541 193478656 42856 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47236 42856 603 41 0 47195 0
vsize: 188944
[startup+600.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 45356 0 0 0 59882 126 0 0 25 0 1 0 546600541 194543616 43133 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47496 43133 603 41 0 47455 0
vsize: 189984
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 46159 0 0 0 60880 128 0 0 25 0 1 0 546600541 197820416 43936 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48296 43936 603 41 0 48255 0
vsize: 193184
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 46562 0 0 0 61879 129 0 0 25 0 1 0 546600541 199528448 44339 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48713 44339 603 41 0 48672 0
vsize: 194852
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 47318 0 0 0 62878 130 0 0 25 0 1 0 546600541 202665984 45095 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49479 45095 603 41 0 49438 0
vsize: 197916
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 47665 0 0 0 63878 131 0 0 25 0 1 0 546600541 203984896 45442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49801 45442 603 41 0 49760 0
vsize: 199204
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 47914 0 0 0 64877 131 0 0 25 0 1 0 546600541 205037568 45691 4294967295 134512640 134672761 3221224544 3221223648 134603769 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50058 45691 603 41 0 50017 0
vsize: 200232
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 48283 0 0 0 65876 132 0 0 25 0 1 0 546600541 206585856 46060 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50436 46060 603 41 0 50395 0
vsize: 201744
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 48656 0 0 0 66875 134 0 0 25 0 1 0 546600541 208039936 46433 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50791 46433 603 41 0 50750 0
vsize: 203164
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 49137 0 0 0 67873 136 0 0 25 0 1 0 546600541 209993728 46914 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51268 46914 603 41 0 51227 0
vsize: 205072
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 49834 0 0 0 68871 138 0 0 25 0 1 0 546600541 212901888 47611 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51978 47611 603 41 0 51937 0
vsize: 207912
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 50164 0 0 0 69871 139 0 0 25 0 1 0 546600541 214224896 47941 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52301 47941 603 41 0 52260 0
vsize: 209204
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 50407 0 0 0 70871 139 0 0 25 0 1 0 546600541 215281664 48184 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52559 48184 603 41 0 52518 0
vsize: 210236
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 50966 0 0 0 71869 141 0 0 25 0 1 0 546600541 217489408 48743 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53098 48743 603 41 0 53057 0
vsize: 212392
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 51466 0 0 0 72868 142 0 0 25 0 1 0 546600541 219594752 49243 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53612 49243 603 41 0 53571 0
vsize: 214448
[startup+740.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 52081 0 0 0 73866 144 0 0 25 0 1 0 546600541 222085120 49858 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54220 49858 603 41 0 54179 0
vsize: 216880
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 52650 0 0 0 74865 146 0 0 25 0 1 0 546600541 224481280 50427 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54805 50427 603 41 0 54764 0
vsize: 219220
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 53019 0 0 0 75864 146 0 0 25 0 1 0 546600541 225943552 50796 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55162 50796 603 41 0 55121 0
vsize: 220648
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 53444 0 0 0 76863 147 0 0 25 0 1 0 546600541 227651584 51221 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55579 51221 603 41 0 55538 0
vsize: 222316
[startup+780.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 53632 0 0 0 77864 147 0 0 25 0 1 0 546600541 228433920 51409 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55770 51409 603 41 0 55729 0
vsize: 223080
[startup+790.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 54035 0 0 0 78863 148 0 0 25 0 1 0 546600541 230133760 51812 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56185 51812 603 41 0 56144 0
vsize: 224740
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 54267 0 0 0 79863 149 0 0 25 0 1 0 546600541 231063552 52044 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56412 52044 603 41 0 56371 0
vsize: 225648
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 54630 0 0 0 80862 150 0 0 25 0 1 0 546600541 232517632 52407 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56767 52407 603 41 0 56726 0
vsize: 227068
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 55019 0 0 0 81861 151 0 0 25 0 1 0 546600541 234086400 52796 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57150 52796 603 41 0 57109 0
vsize: 228600
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 55431 0 0 0 82860 153 0 0 25 0 1 0 546600541 235802624 53208 4294967295 134512640 134672761 3221224544 3221223728 134615945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57569 53208 603 41 0 57528 0
vsize: 230276
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 55772 0 0 0 83859 153 0 0 25 0 1 0 546600541 237129728 53549 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57893 53549 603 41 0 57852 0
vsize: 231572
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 56153 0 0 0 84858 155 0 0 25 0 1 0 546600541 238698496 53930 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58276 53930 603 41 0 58235 0
vsize: 233104
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 56392 0 0 0 85857 155 0 0 25 0 1 0 546600541 239755264 54169 4294967295 134512640 134672761 3221224544 3221223536 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58534 54169 603 41 0 58493 0
vsize: 234136
[startup+870.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 56638 0 0 0 86857 156 0 0 25 0 1 0 546600541 240693248 54415 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58763 54415 603 41 0 58722 0
vsize: 235052
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 56866 0 0 0 87856 157 0 0 25 0 1 0 546600541 241618944 54643 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58989 54643 603 41 0 58948 0
vsize: 235956
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 57261 0 0 0 88855 158 0 0 25 0 1 0 546600541 243208192 55038 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59377 55038 603 41 0 59336 0
vsize: 237508
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 57557 0 0 0 89855 159 0 0 25 0 1 0 546600541 244391936 55334 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59666 55334 603 41 0 59625 0
vsize: 238664
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 57767 0 0 0 90854 160 0 0 25 0 1 0 546600541 245313536 55544 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59891 55544 603 41 0 59850 0
vsize: 239564
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 58007 0 0 0 91854 160 0 0 25 0 1 0 546600541 246239232 55784 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60117 55784 603 41 0 60076 0
vsize: 240468
[startup+930.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 58314 0 0 0 92853 161 0 0 25 0 1 0 546600541 247554048 56091 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60438 56091 603 41 0 60397 0
vsize: 241752
[startup+940.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 58498 0 0 0 93853 161 0 0 25 0 1 0 546600541 248340480 56275 4294967295 134512640 134672761 3221224544 3221223584 134612791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60630 56275 603 41 0 60589 0
vsize: 242520
[startup+950.011 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 59047 0 0 0 94852 163 0 0 25 0 1 0 546600541 250585088 56824 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61178 56824 603 41 0 61137 0
vsize: 244712
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 59491 0 0 0 95851 164 0 0 25 0 1 0 546600541 252817408 57268 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61723 57268 603 41 0 61682 0
vsize: 246892
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 59824 0 0 0 96850 164 0 0 25 0 1 0 546600541 254279680 57601 4294967295 134512640 134672761 3221224544 3221223584 134614207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62080 57601 603 41 0 62039 0
vsize: 248320
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 60019 0 0 0 97850 165 0 0 25 0 1 0 546600541 255066112 57796 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62272 57796 603 41 0 62231 0
vsize: 249088
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 60250 0 0 0 98850 166 0 0 25 0 1 0 546600541 255983616 58027 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62496 58027 603 41 0 62455 0
vsize: 249984
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 60405 0 0 0 99849 167 0 0 25 0 1 0 546600541 256643072 58182 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62657 58182 603 41 0 62616 0
vsize: 250628
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 60953 0 0 0 100847 169 0 0 25 0 1 0 546600541 258887680 58730 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63205 58730 603 41 0 63164 0
vsize: 252820
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 61532 0 0 0 101845 171 0 0 25 0 1 0 546600541 261263360 59309 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63785 59309 603 41 0 63744 0
vsize: 255140
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 61804 0 0 0 102845 171 0 0 25 0 1 0 546600541 262316032 59581 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64042 59581 603 41 0 64001 0
vsize: 256168
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 62260 0 0 0 103844 172 0 0 25 0 1 0 546600541 264179712 60037 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64497 60037 603 41 0 64456 0
vsize: 257988
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 62644 0 0 0 104843 173 0 0 25 0 1 0 546600541 265752576 60421 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64881 60421 603 41 0 64840 0
vsize: 259524
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 63016 0 0 0 105842 174 0 0 25 0 1 0 546600541 267227136 60793 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65241 60793 603 41 0 65200 0
vsize: 260964
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12850
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 63492 0 0 0 106841 176 0 0 25 0 1 0 546600541 269209600 61269 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65725 61269 603 41 0 65684 0
vsize: 262900
[startup+1080.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 12903
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 64155 0 0 0 107835 181 0 0 25 0 1 0 546600541 271953920 61932 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66395 61932 603 41 0 66354 0
vsize: 265580
[startup+1090.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 12903
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 64765 0 0 0 108833 184 0 0 25 0 1 0 546600541 274444288 62542 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67003 62542 603 41 0 66962 0
vsize: 268012
[startup+1100.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 12903
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 65133 0 0 0 109832 185 0 0 25 0 1 0 546600541 275890176 62910 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67356 62910 603 41 0 67315 0
vsize: 269424
[startup+1110.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12903
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 65493 0 0 0 110831 186 0 0 25 0 1 0 546600541 277348352 63270 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67712 63270 603 41 0 67671 0
vsize: 270848
[startup+1120.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12903
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 66460 0 0 0 111828 189 0 0 25 0 1 0 546600541 281378816 64237 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68696 64237 603 41 0 68655 0
vsize: 274784
[startup+1130.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12903
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 67050 0 0 0 112826 191 0 0 25 0 1 0 546600541 283738112 64827 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69272 64827 603 41 0 69231 0
vsize: 277088
[startup+1140.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12905
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 67249 0 0 0 113825 192 0 0 25 0 1 0 546600541 284536832 65026 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69467 65026 603 41 0 69426 0
vsize: 277868
[startup+1150.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12905
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 67381 0 0 0 114824 193 0 0 25 0 1 0 546600541 285192192 65158 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69627 65158 603 41 0 69586 0
vsize: 278508
[startup+1160.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12905
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 67738 0 0 0 115824 194 0 0 25 0 1 0 546600541 286629888 65515 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69978 65515 603 41 0 69937 0
vsize: 279912
[startup+1170.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12905
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 67913 0 0 0 116823 195 0 0 25 0 1 0 546600541 287285248 65690 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70138 65690 603 41 0 70097 0
vsize: 280552
[startup+1180.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12905
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 68326 0 0 0 117822 196 0 0 25 0 1 0 546600541 288989184 66103 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70554 66103 603 41 0 70513 0
vsize: 282216
[startup+1190.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12905
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 68481 0 0 0 118822 196 0 0 25 0 1 0 546600541 289648640 66258 4294967295 134512640 134672761 3221224544 3221223688 134616254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70715 66258 603 41 0 70674 0
vsize: 282860
[startup+1200.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12905
Raw data (stat): 12850 (minisat+) R 12849 28546 28545 0 -1 0 68991 0 0 0 119822 197 0 0 25 0 1 0 546600541 291639296 66768 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71201 66768 603 41 0 71160 0
vsize: 284804
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 12905
Raw data (stat): 12850 (minisat+) Z 12849 28546 28545 0 -1 12 68991 0 0 0 119822 210 0 0 25 0 1 0 546600541 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.15
CPU time (s): 1200.32
CPU user time (s): 1198.22
CPU system time (s): 2.10068
CPU usage (%): 100.014
Max. virtual memory (Kb): 284804
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####