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/miplib3/normalized-mps-v2-13-7-air04.opb
MD5SUM	26490113618ae9605b5ebe6370b5910b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.120981
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 18359

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 14:30:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18172 boxname=wulflinc26 idbench=1398 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  26490113618ae9605b5ebe6370b5910b  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-air04.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 18172
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        845592 kB
Buffers:         28368 kB
Cached:         132588 kB
SwapCached:         68 kB
Active:          33996 kB
Inactive:       129820 kB
HighTotal:      131008 kB
HighFree:        65940 kB
LowTotal:       903652 kB
LowFree:        779652 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            19460 kB
Committed_AS:    63724 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:50:41 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 18172 7 1200.35 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:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
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     2530    25.3 |  0.597 % |
c |       250 |  307133   797368 |  148652     249    14202    57.0 |  0.598 % |
c |       476 |  307133   797368 |  163517     475    37478    78.9 |  0.598 % |
c |       813 |  307133   797368 |  179869     812    54056    66.6 |  0.598 % |
c |      1320 |  307082   797220 |  197823    1314    93656    71.3 |  0.606 % |
c |      2079 |  306986   796936 |  217537    2070   144740    69.9 |  0.610 % |
c |      3218 |  306974   796900 |  239282    3207   305716    95.3 |  0.611 % |
c |      4926 |  306937   796791 |  263178    4905   497537   101.4 |  0.614 % |
c |      #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 390
Raw data (stat): 390 (runsolver) R 389 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545819388 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 20915 0 0 0 940 58 0 0 25 0 1 0 545819388 94146560 18657 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22985 18657 603 41 0 22944 0
vsize: 91940
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 21060 0 0 0 1940 59 0 0 25 0 1 0 545819388 94814208 18802 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23148 18802 603 41 0 23107 0
vsize: 92592
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 21418 0 0 0 2939 60 0 0 25 0 1 0 545819388 96280576 19160 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23506 19160 603 41 0 23465 0
vsize: 94024
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 21793 0 0 0 3938 61 0 0 25 0 1 0 545819388 97734656 19535 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23861 19535 603 41 0 23820 0
vsize: 95444
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 22099 0 0 0 4937 62 0 0 25 0 1 0 545819388 99049472 19841 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24182 19841 603 41 0 24141 0
vsize: 96728
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 22519 0 0 0 5936 63 0 0 25 0 1 0 545819388 100667392 20261 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24577 20261 603 41 0 24536 0
vsize: 98308
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 22835 0 0 0 6936 64 0 0 25 0 1 0 545819388 101986304 20577 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24899 20577 603 41 0 24858 0
vsize: 99596
[startup+80.0042 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 23337 0 0 0 7934 65 0 0 25 0 1 0 545819388 104108032 21079 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25417 21079 603 41 0 25376 0
vsize: 101668
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 23753 0 0 0 8934 66 0 0 25 0 1 0 545819388 105828352 21495 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25837 21495 603 41 0 25796 0
vsize: 103348
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 24063 0 0 0 9933 67 0 0 25 0 1 0 545819388 107008000 21805 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26125 21805 603 41 0 26084 0
vsize: 104500
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 24363 0 0 0 10931 69 0 0 25 0 1 0 545819388 108343296 22105 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26451 22105 603 41 0 26410 0
vsize: 105804
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 24702 0 0 0 11931 70 0 0 25 0 1 0 545819388 109674496 22444 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26776 22444 603 41 0 26735 0
vsize: 107104
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 25306 0 0 0 12929 72 0 0 25 0 1 0 545819388 112181248 23048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27388 23048 603 41 0 27347 0
vsize: 109552
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 25568 0 0 0 13928 73 0 0 25 0 1 0 545819388 113246208 23310 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27648 23310 603 41 0 27607 0
vsize: 110592
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 25874 0 0 0 14927 73 0 0 25 0 1 0 545819388 114434048 23616 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27938 23616 603 41 0 27897 0
vsize: 111752
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 26297 0 0 0 15926 75 0 0 25 0 1 0 545819388 116162560 24039 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28360 24039 603 41 0 28319 0
vsize: 113440
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 26856 0 0 0 16924 77 0 0 25 0 1 0 545819388 118530048 24598 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28938 24598 603 41 0 28897 0
vsize: 115752
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 27364 0 0 0 17922 79 0 0 25 0 1 0 545819388 120639488 25106 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29453 25106 603 41 0 29412 0
vsize: 117812
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 27818 0 0 0 18920 81 0 0 25 0 1 0 545819388 122503168 25560 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29908 25560 603 41 0 29867 0
vsize: 119632
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 28276 0 0 0 19918 84 0 0 25 0 1 0 545819388 124362752 26018 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30362 26018 603 41 0 30321 0
vsize: 121448
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 28920 0 0 0 20917 85 0 0 25 0 1 0 545819388 126980096 26662 4294967295 134512640 134672761 3221224544 3221223680 134614560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31001 26662 603 41 0 30960 0
vsize: 124004
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 29276 0 0 0 21916 86 0 0 25 0 1 0 545819388 128425984 27018 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31354 27018 603 41 0 31313 0
vsize: 125416
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 29592 0 0 0 22915 87 0 0 25 0 1 0 545819388 129748992 27334 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31677 27334 603 41 0 31636 0
vsize: 126708
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 29873 0 0 0 23914 88 0 0 25 0 1 0 545819388 130809856 27615 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31936 27615 603 41 0 31895 0
vsize: 127744
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 30235 0 0 0 24913 89 0 0 25 0 1 0 545819388 132403200 27977 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32325 27977 603 41 0 32284 0
vsize: 129300
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 30699 0 0 0 25911 91 0 0 25 0 1 0 545819388 134262784 28441 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32779 28441 603 41 0 32738 0
vsize: 131116
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 31107 0 0 0 26910 93 0 0 25 0 1 0 545819388 135983104 28849 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33199 28849 603 41 0 33158 0
vsize: 132796
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 31604 0 0 0 27909 94 0 0 25 0 1 0 545819388 138096640 29346 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33715 29346 603 41 0 33674 0
vsize: 134860
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 31851 0 0 0 28908 95 0 0 25 0 1 0 545819388 139034624 29593 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33944 29593 603 41 0 33903 0
vsize: 135776
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 32169 0 0 0 29906 96 0 0 25 0 1 0 545819388 140357632 29911 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34267 29911 603 41 0 34226 0
vsize: 137068
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 32624 0 0 0 30905 98 0 0 25 0 1 0 545819388 142192640 30366 4294967295 134512640 134672761 3221224544 3221223744 134610608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34715 30366 603 41 0 34674 0
vsize: 138860
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 33106 0 0 0 31903 100 0 0 25 0 1 0 545819388 144166912 30848 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35197 30848 603 41 0 35156 0
vsize: 140788
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 33478 0 0 0 32902 101 0 0 25 0 1 0 545819388 145743872 31220 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35582 31220 603 41 0 35541 0
vsize: 142328
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 34042 0 0 0 33900 104 0 0 25 0 1 0 545819388 147992576 31784 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36131 31784 603 41 0 36090 0
vsize: 144524
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 34339 0 0 0 34898 105 0 0 25 0 1 0 545819388 149188608 32081 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36423 32081 603 41 0 36382 0
vsize: 145692
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 34584 0 0 0 35898 106 0 0 25 0 1 0 545819388 150261760 32326 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36685 32326 603 41 0 36644 0
vsize: 146740
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 34874 0 0 0 36897 107 0 0 25 0 1 0 545819388 151326720 32616 4294967295 134512640 134672761 3221224544 3221223536 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36945 32616 603 41 0 36904 0
vsize: 147780
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 35203 0 0 0 37896 108 0 0 25 0 1 0 545819388 152784896 32945 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37301 32945 603 41 0 37260 0
vsize: 149204
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 35832 0 0 0 38894 110 0 0 25 0 1 0 545819388 155561984 33574 4294967295 134512640 134672761 3221224544 3221223576 134603663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37979 33574 603 41 0 37938 0
vsize: 151916
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 36505 0 0 0 39892 112 0 0 25 0 1 0 545819388 158330880 34247 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38655 34247 603 41 0 38614 0
vsize: 154620
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 37304 0 0 0 40890 114 0 0 25 0 1 0 545819388 161624064 35046 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39459 35046 603 41 0 39418 0
vsize: 157836
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 37926 0 0 0 41889 116 0 0 25 0 1 0 545819388 164130816 35668 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40071 35668 603 41 0 40030 0
vsize: 160284
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 38611 0 0 0 42887 118 0 0 25 0 1 0 545819388 166903808 36353 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40748 36353 603 41 0 40707 0
vsize: 162992
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 39155 0 0 0 43885 120 0 0 25 0 1 0 545819388 169119744 36897 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41289 36897 603 41 0 41248 0
vsize: 165156
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 39532 0 0 0 44884 121 0 0 25 0 1 0 545819388 170692608 37274 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41673 37274 603 41 0 41632 0
vsize: 166692
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 39787 0 0 0 45883 122 0 0 25 0 1 0 545819388 171745280 37529 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41930 37529 603 41 0 41889 0
vsize: 167720
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 40050 0 0 0 46882 124 0 0 25 0 1 0 545819388 172806144 37792 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42189 37792 603 41 0 42148 0
vsize: 168756
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 40295 0 0 0 47881 124 0 0 25 0 1 0 545819388 173744128 38037 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42418 38037 603 41 0 42377 0
vsize: 169672
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 40680 0 0 0 48881 125 0 0 25 0 1 0 545819388 175321088 38422 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42803 38422 603 41 0 42762 0
vsize: 171212
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 41099 0 0 0 49880 126 0 0 25 0 1 0 545819388 177041408 38841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43223 38841 603 41 0 43182 0
vsize: 172892
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 41696 0 0 0 50878 128 0 0 25 0 1 0 545819388 179548160 39438 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43835 39438 603 41 0 43794 0
vsize: 175340
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 42151 0 0 0 51877 129 0 0 25 0 1 0 545819388 181387264 39893 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44284 39893 603 41 0 44243 0
vsize: 177136
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 42612 0 0 0 52875 131 0 0 25 0 1 0 545819388 183222272 40354 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44732 40354 603 41 0 44691 0
vsize: 178928
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 43058 0 0 0 53874 132 0 0 25 0 1 0 545819388 185049088 40800 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45178 40800 603 41 0 45137 0
vsize: 180712
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 43423 0 0 0 54874 133 0 0 25 0 1 0 545819388 186634240 41165 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45565 41165 603 41 0 45524 0
vsize: 182260
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 43747 0 0 0 55872 135 0 0 25 0 1 0 545819388 187944960 41489 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45885 41489 603 41 0 45844 0
vsize: 183540
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 44203 0 0 0 56871 136 0 0 25 0 1 0 545819388 189788160 41945 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46335 41945 603 41 0 46294 0
vsize: 185340
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 44692 0 0 0 57869 138 0 0 25 0 1 0 545819388 191766528 42434 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46818 42434 603 41 0 46777 0
vsize: 187272
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 45033 0 0 0 58867 140 0 0 25 0 1 0 545819388 193216512 42775 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47172 42775 603 41 0 47131 0
vsize: 188688
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 45377 0 0 0 59867 141 0 0 25 0 1 0 545819388 194560000 43119 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47500 43119 603 41 0 47459 0
vsize: 190000
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 45899 0 0 0 60865 143 0 0 25 0 1 0 545819388 196648960 43641 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48010 43641 603 41 0 47969 0
vsize: 192040
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 46314 0 0 0 61864 144 0 0 25 0 1 0 545819388 198365184 44056 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48429 44056 603 41 0 48388 0
vsize: 193716
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 46698 0 0 0 62864 145 0 0 25 0 1 0 545819388 199921664 44440 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48809 44440 603 41 0 48768 0
vsize: 195236
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 47049 0 0 0 63862 146 0 0 25 0 1 0 545819388 201375744 44791 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49164 44791 603 41 0 49123 0
vsize: 196656
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 47528 0 0 0 64860 148 0 0 25 0 1 0 545819388 203337728 45270 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49643 45270 603 41 0 49602 0
vsize: 198572
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 47854 0 0 0 65859 150 0 0 25 0 1 0 545819388 204656640 45596 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49965 45596 603 41 0 49924 0
vsize: 199860
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 48346 0 0 0 66857 152 0 0 25 0 1 0 545819388 206737408 46088 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50473 46088 603 41 0 50432 0
vsize: 201892
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 48640 0 0 0 67855 153 0 0 25 0 1 0 545819388 207958016 46382 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50771 46382 603 41 0 50730 0
vsize: 203084
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 48931 0 0 0 68855 154 0 0 25 0 1 0 545819388 209145856 46673 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51061 46673 603 41 0 51020 0
vsize: 204244
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 49347 0 0 0 69853 156 0 0 25 0 1 0 545819388 210853888 47089 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51478 47089 603 41 0 51437 0
vsize: 205912
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 49874 0 0 0 70851 158 0 0 25 0 1 0 545819388 212971520 47616 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51995 47616 603 41 0 51954 0
vsize: 207980
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 50157 0 0 0 71849 160 0 0 25 0 1 0 545819388 214167552 47899 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52287 47899 603 41 0 52246 0
vsize: 209148
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 50679 0 0 0 72849 161 0 0 25 0 1 0 545819388 216289280 48421 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52805 48421 603 41 0 52764 0
vsize: 211220
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 51030 0 0 0 73847 162 0 0 25 0 1 0 545819388 217604096 48772 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53126 48772 603 41 0 53085 0
vsize: 212504
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 51208 0 0 0 74847 164 0 0 25 0 1 0 545819388 218398720 48950 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53320 48950 603 41 0 53279 0
vsize: 213280
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 51464 0 0 0 75845 165 0 0 25 0 1 0 545819388 219451392 49206 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53577 49206 603 41 0 53536 0
vsize: 214308
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 51811 0 0 0 76845 166 0 0 25 0 1 0 545819388 220905472 49553 4294967295 134512640 134672761 3221224544 3221223728 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53932 49553 603 41 0 53891 0
vsize: 215728
[startup+780.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 52019 0 0 0 77844 167 0 0 25 0 1 0 545819388 221708288 49761 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54128 49761 603 41 0 54087 0
vsize: 216512
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 52418 0 0 0 78842 169 0 0 25 0 1 0 545819388 223281152 50160 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54512 50160 603 41 0 54471 0
vsize: 218048
[startup+800.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 52863 0 0 0 79841 170 0 0 25 0 1 0 545819388 225132544 50605 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54964 50605 603 41 0 54923 0
vsize: 219856
[startup+810.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 53603 0 0 0 80839 172 0 0 25 0 1 0 545819388 228155392 51345 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55702 51345 603 41 0 55661 0
vsize: 222808
[startup+820.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 54002 0 0 0 81838 174 0 0 25 0 1 0 545819388 229900288 51744 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56128 51744 603 41 0 56087 0
vsize: 224512
[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 54476 0 0 0 82837 176 0 0 25 0 1 0 545819388 231763968 52218 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56583 52218 603 41 0 56542 0
vsize: 226332
[startup+840.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 54679 0 0 0 83838 176 0 0 25 0 1 0 545819388 232558592 52421 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56777 52421 603 41 0 56736 0
vsize: 227108
[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 55044 0 0 0 84837 177 0 0 25 0 1 0 545819388 234151936 52786 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57166 52786 603 41 0 57125 0
vsize: 228664
[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 55255 0 0 0 85837 178 0 0 25 0 1 0 545819388 234946560 52997 4294967295 134512640 134672761 3221224544 3221223688 134616366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57360 52997 603 41 0 57319 0
vsize: 229440
[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 55681 0 0 0 86835 180 0 0 25 0 1 0 545819388 236662784 53423 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57779 53423 603 41 0 57738 0
vsize: 231116
[startup+880.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 55972 0 0 0 87835 180 0 0 25 0 1 0 545819388 237862912 53714 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58072 53714 603 41 0 58031 0
vsize: 232288
[startup+890.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 56441 0 0 0 88833 182 0 0 25 0 1 0 545819388 239861760 54183 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58560 54183 603 41 0 58519 0
vsize: 234240
[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 56823 0 0 0 89832 183 0 0 25 0 1 0 545819388 241311744 54565 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58914 54565 603 41 0 58873 0
vsize: 235656
[startup+910.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 57182 0 0 0 90831 185 0 0 25 0 1 0 545819388 242761728 54924 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59268 54924 603 41 0 59227 0
vsize: 237072
[startup+920.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 57511 0 0 0 91831 185 0 0 25 0 1 0 545819388 244203520 55253 4294967295 134512640 134672761 3221224544 3221223688 134616258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59620 55253 603 41 0 59579 0
vsize: 238480
[startup+930.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 57960 0 0 0 92830 186 0 0 25 0 1 0 545819388 245964800 55702 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60050 55702 603 41 0 60009 0
vsize: 240200
[startup+940.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 58498 0 0 0 93827 189 0 0 25 0 1 0 545819388 248213504 56240 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60599 56240 603 41 0 60558 0
vsize: 242396
[startup+950.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 59654 0 0 0 94825 192 0 0 25 0 1 0 545819388 252882944 57396 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61739 57396 603 41 0 61698 0
vsize: 246956
[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 60497 0 0 0 95822 194 0 0 25 0 1 0 545819388 256360448 58239 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62588 58239 603 41 0 62547 0
vsize: 250352
[startup+970.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 60855 0 0 0 96821 195 0 0 25 0 1 0 545819388 258351104 58597 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63074 58597 603 41 0 63033 0
vsize: 252296
[startup+980.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 61118 0 0 0 97821 196 0 0 25 0 1 0 545819388 259428352 58860 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63337 58860 603 41 0 63296 0
vsize: 253348
[startup+990.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 61279 0 0 0 98819 198 0 0 25 0 1 0 545819388 260083712 59021 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63497 59021 603 41 0 63456 0
vsize: 253988
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 61469 0 0 0 99819 198 0 0 25 0 1 0 545819388 260874240 59211 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63690 59211 603 41 0 63649 0
vsize: 254760
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 61809 0 0 0 100818 200 0 0 25 0 1 0 545819388 262324224 59551 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64044 59551 603 41 0 64003 0
vsize: 256176
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 61969 0 0 0 101817 200 0 0 25 0 1 0 545819388 262979584 59711 4294967295 134512640 134672761 3221224544 3221223704 134614477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64204 59711 603 41 0 64163 0
vsize: 256816
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 62219 0 0 0 102817 201 0 0 25 0 1 0 545819388 263905280 59961 4294967295 134512640 134672761 3221224544 3221223536 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64430 59961 603 41 0 64389 0
vsize: 257720
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 62680 0 0 0 103815 202 0 0 25 0 1 0 545819388 265879552 60422 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64912 60422 603 41 0 64871 0
vsize: 259648
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 62887 0 0 0 104815 203 0 0 25 0 1 0 545819388 266674176 60629 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65106 60629 603 41 0 65065 0
vsize: 260424
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 63581 0 0 0 105813 205 0 0 25 0 1 0 545819388 269565952 61323 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65812 61323 603 41 0 65771 0
vsize: 263248
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 63921 0 0 0 106812 206 0 0 25 0 1 0 545819388 270868480 61663 4294967295 134512640 134672761 3221224544 3221223744 134610688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66130 61663 603 41 0 66089 0
vsize: 264520
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 64143 0 0 0 107812 207 0 0 25 0 1 0 545819388 271806464 61885 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66359 61885 603 41 0 66318 0
vsize: 265436
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 64445 0 0 0 108811 207 0 0 25 0 1 0 545819388 273006592 62187 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66652 62187 603 41 0 66611 0
vsize: 266608
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 64825 0 0 0 109811 208 0 0 25 0 1 0 545819388 274579456 62567 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67036 62567 603 41 0 66995 0
vsize: 268144
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 65132 0 0 0 110810 209 0 0 25 0 1 0 545819388 275898368 62874 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67358 62874 603 41 0 67317 0
vsize: 269432
[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 65562 0 0 0 111809 210 0 0 25 0 1 0 545819388 277602304 63304 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67774 63304 603 41 0 67733 0
vsize: 271096
[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 65998 0 0 0 112808 211 0 0 25 0 1 0 545819388 279429120 63740 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68220 63740 603 41 0 68179 0
vsize: 272880
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 66565 0 0 0 113806 214 0 0 25 0 1 0 545819388 281665536 64307 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68766 64307 603 41 0 68725 0
vsize: 275064
[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 66946 0 0 0 114805 215 0 0 25 0 1 0 545819388 283262976 64688 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69156 64688 603 41 0 69115 0
vsize: 276624
[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 67312 0 0 0 115804 216 0 0 25 0 1 0 545819388 284725248 65054 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69513 65054 603 41 0 69472 0
vsize: 278052
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 67793 0 0 0 116803 217 0 0 25 0 1 0 545819388 286711808 65535 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69998 65535 603 41 0 69957 0
vsize: 279992
[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 68228 0 0 0 117802 218 0 0 25 0 1 0 545819388 288563200 65970 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70450 65970 603 41 0 70409 0
vsize: 281800
[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 68616 0 0 0 118802 220 0 0 25 0 1 0 545819388 290144256 66358 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70836 66358 603 41 0 70795 0
vsize: 283344
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 390
Raw data (stat): 390 (minisat+) R 389 22612 22611 0 -1 0 68905 0 0 0 119802 220 0 0 25 0 1 0 545819388 291328000 66647 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71125 66647 603 41 0 71084 0
vsize: 284500
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 390
Raw data (stat): 390 (minisat+) Z 389 22612 22611 0 -1 12 68905 0 0 0 119802 232 0 0 25 0 1 0 545819388 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.22
CPU time (s): 1200.35
CPU user time (s): 1198.02
CPU system time (s): 2.32865
CPU usage (%): 100.011
Max. virtual memory (Kb): 284500
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####