PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.116981
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 16501

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        747240 kB
Buffers:         29432 kB
Cached:         235996 kB
SwapCached:        316 kB
Active:          59112 kB
Inactive:       208632 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        746988 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            14028 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:53:15 (client local time) WITH STATUS 0 IN 1200.56 SECONDS
stats: 13180 7 1200.56 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.91 0.95 0.90 2/54 22951
Raw data (stat): 22951 (runsolver) R 22950 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485084486 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.93 0.95 0.90 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 20915 0 0 0 943 55 0 0 25 0 1 0 485084486 94146560 18657 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22985 18657 603 41 0 22944 0
vsize: 91940
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 21083 0 0 0 1943 55 0 0 25 0 1 0 485084486 94814208 18825 4294967295 134512640 134672761 3221224544 3221223728 134615576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23148 18825 603 41 0 23107 0
vsize: 92592
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 21426 0 0 0 2942 56 0 0 25 0 1 0 485084486 96280576 19168 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23506 19168 603 41 0 23465 0
vsize: 94024
[startup+40.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 21796 0 0 0 3941 58 0 0 25 0 1 0 485084486 97734656 19538 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23861 19538 603 41 0 23820 0
vsize: 95444
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 22113 0 0 0 4940 59 0 0 25 0 1 0 485084486 99049472 19855 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24182 19855 603 41 0 24141 0
vsize: 96728
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 22568 0 0 0 5939 60 0 0 25 0 1 0 485084486 100933632 20310 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24642 20310 603 41 0 24601 0
vsize: 98568
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 22858 0 0 0 6938 61 0 0 25 0 1 0 485084486 102117376 20600 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24931 20600 603 41 0 24890 0
vsize: 99724
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 23360 0 0 0 7937 62 0 0 25 0 1 0 485084486 104239104 21102 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25449 21102 603 41 0 25408 0
vsize: 101796
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 23786 0 0 0 8936 63 0 0 25 0 1 0 485084486 105963520 21528 4294967295 134512640 134672761 3221224544 3221223712 134564695 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25870 21528 603 41 0 25829 0
vsize: 103480
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 24112 0 0 0 9935 64 0 0 25 0 1 0 485084486 107274240 21854 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26190 21854 603 41 0 26149 0
vsize: 104760
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 24419 0 0 0 10934 66 0 0 25 0 1 0 485084486 108478464 22161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26484 22161 603 41 0 26443 0
vsize: 105936
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 24778 0 0 0 11933 67 0 0 25 0 1 0 485084486 109940736 22520 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26841 22520 603 41 0 26800 0
vsize: 107364
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 25317 0 0 0 12932 69 0 0 25 0 1 0 485084486 112181248 23059 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27388 23059 603 41 0 27347 0
vsize: 109552
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 25594 0 0 0 13931 69 0 0 25 0 1 0 485084486 113381376 23336 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27681 23336 603 41 0 27640 0
vsize: 110724
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 25933 0 0 0 14930 70 0 0 25 0 1 0 485084486 114704384 23675 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28004 23675 603 41 0 27963 0
vsize: 112016
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 26378 0 0 0 15930 71 0 0 25 0 1 0 485084486 116555776 24120 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28456 24120 603 41 0 28415 0
vsize: 113824
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 26947 0 0 0 16928 73 0 0 25 0 1 0 485084486 118923264 24689 4294967295 134512640 134672761 3221224544 3221223356 1075350069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 24690 603 41 0 28993 0
vsize: 116136
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 27411 0 0 0 17927 74 0 0 25 0 1 0 485084486 120905728 25153 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29518 25153 603 41 0 29477 0
vsize: 118072
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 27846 0 0 0 18926 75 0 0 25 0 1 0 485084486 122642432 25588 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29942 25588 603 41 0 29901 0
vsize: 119768
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 28341 0 0 0 19924 77 0 0 25 0 1 0 485084486 124624896 26083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30426 26083 603 41 0 30385 0
vsize: 121704
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 28965 0 0 0 20923 79 0 0 25 0 1 0 485084486 127242240 26707 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31065 26707 603 41 0 31024 0
vsize: 124260
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 29319 0 0 0 21922 80 0 0 25 0 1 0 485084486 128557056 27061 4294967295 134512640 134672761 3221224544 3221223536 134565134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31386 27062 603 41 0 31345 0
vsize: 125544
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 29652 0 0 0 22921 80 0 0 25 0 1 0 485084486 130015232 27394 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31742 27394 603 41 0 31701 0
vsize: 126968
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 29958 0 0 0 23921 81 0 0 25 0 1 0 485084486 131211264 27700 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32034 27700 603 41 0 31993 0
vsize: 128136
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 30302 0 0 0 24919 83 0 0 25 0 1 0 485084486 132673536 28044 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32391 28044 603 41 0 32350 0
vsize: 129564
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 30762 0 0 0 25918 84 0 0 25 0 1 0 485084486 134524928 28504 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32843 28504 603 41 0 32802 0
vsize: 131372
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 31220 0 0 0 26917 85 0 0 25 0 1 0 485084486 136507392 28962 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33327 28962 603 41 0 33286 0
vsize: 133308
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 31656 0 0 0 27916 87 0 0 25 0 1 0 485084486 138231808 29398 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33748 29398 603 41 0 33707 0
vsize: 134992
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 31892 0 0 0 28916 87 0 0 25 0 1 0 485084486 139169792 29634 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33977 29634 603 41 0 33936 0
vsize: 135908
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 32316 0 0 0 29915 88 0 0 25 0 1 0 485084486 140877824 30058 4294967295 134512640 134672761 3221224544 3221223688 134616126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34394 30058 603 41 0 34353 0
vsize: 137576
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 32674 0 0 0 30914 90 0 0 25 0 1 0 485084486 142454784 30416 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34779 30416 603 41 0 34738 0
vsize: 139116
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 33140 0 0 0 31912 91 0 0 25 0 1 0 485084486 144297984 30882 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35229 30882 603 41 0 35188 0
vsize: 140916
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 33579 0 0 0 32912 92 0 0 25 0 1 0 485084486 146149376 31321 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35681 31321 603 41 0 35640 0
vsize: 142724
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 34098 0 0 0 33910 94 0 0 25 0 1 0 485084486 148254720 31840 4294967295 134512640 134672761 3221224544 3221223728 134615576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36195 31840 603 41 0 36154 0
vsize: 144780
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 34411 0 0 0 34910 94 0 0 25 0 1 0 485084486 149454848 32153 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36488 32153 603 41 0 36447 0
vsize: 145952
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 34684 0 0 0 35909 95 0 0 25 0 1 0 485084486 150667264 32426 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36784 32426 603 41 0 36743 0
vsize: 147136
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 34961 0 0 0 36909 96 0 0 25 0 1 0 485084486 151719936 32703 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37041 32703 603 41 0 37000 0
vsize: 148164
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 35313 0 0 0 37907 97 0 0 25 0 1 0 485084486 153186304 33055 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37399 33055 603 41 0 37358 0
vsize: 149596
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 36030 0 0 0 38906 98 0 0 25 0 1 0 485084486 156352512 33772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38172 33772 603 41 0 38131 0
vsize: 152688
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 36738 0 0 0 39905 100 0 0 25 0 1 0 485084486 159252480 34480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38880 34480 603 41 0 38839 0
vsize: 155520
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 37480 0 0 0 40904 102 0 0 25 0 1 0 485084486 162287616 35222 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39621 35222 603 41 0 39580 0
vsize: 158484
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 38125 0 0 0 41903 103 0 0 25 0 1 0 485084486 164929536 35867 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40266 35867 603 41 0 40225 0
vsize: 161064
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 38935 0 0 0 42902 104 0 0 25 0 1 0 485084486 168194048 36677 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41063 36677 603 41 0 41022 0
vsize: 164252
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 39351 0 0 0 43901 105 0 0 25 0 1 0 485084486 169897984 37093 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41479 37093 603 41 0 41438 0
vsize: 165916
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 39582 0 0 0 44901 106 0 0 25 0 1 0 485084486 170954752 37324 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41737 37324 603 41 0 41696 0
vsize: 166948
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 39892 0 0 0 45900 107 0 0 25 0 1 0 485084486 172138496 37634 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42026 37634 603 41 0 41985 0
vsize: 168104
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 40094 0 0 0 46900 107 0 0 25 0 1 0 485084486 172941312 37836 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42222 37836 603 41 0 42181 0
vsize: 168888
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 40468 0 0 0 47900 108 0 0 25 0 1 0 485084486 174522368 38210 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42608 38210 603 41 0 42567 0
vsize: 170432
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 40735 0 0 0 48899 109 0 0 25 0 1 0 485084486 175595520 38477 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42870 38477 603 41 0 42829 0
vsize: 171480
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 41372 0 0 0 49898 110 0 0 25 0 1 0 485084486 178225152 39114 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43512 39114 603 41 0 43471 0
vsize: 174048
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 41919 0 0 0 50897 111 0 0 25 0 1 0 485084486 180465664 39661 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44059 39661 603 41 0 44018 0
vsize: 176236
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 42400 0 0 0 51896 113 0 0 25 0 1 0 485084486 182435840 40142 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44540 40142 603 41 0 44499 0
vsize: 178160
[startup+530.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 42795 0 0 0 52895 114 0 0 25 0 1 0 485084486 184004608 40537 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44923 40537 603 41 0 44882 0
vsize: 179692
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 43194 0 0 0 53893 116 0 0 25 0 1 0 485084486 185577472 40936 4294967295 134512640 134672761 3221224544 3221223536 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45307 40936 603 41 0 45266 0
vsize: 181228
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 43672 0 0 0 54892 117 0 0 25 0 1 0 485084486 187551744 41414 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45789 41414 603 41 0 45748 0
vsize: 183156
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 43882 0 0 0 55891 118 0 0 25 0 1 0 485084486 188477440 41624 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46015 41624 603 41 0 45974 0
vsize: 184060
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 44384 0 0 0 56890 120 0 0 25 0 1 0 485084486 190447616 42126 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46496 42126 603 41 0 46455 0
vsize: 185984
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 44831 0 0 0 57889 121 0 0 25 0 1 0 485084486 192294912 42573 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46947 42573 603 41 0 46906 0
vsize: 187788
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 45195 0 0 0 58888 122 0 0 25 0 1 0 485084486 193765376 42937 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47306 42937 603 41 0 47265 0
vsize: 189224
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 45603 0 0 0 59887 124 0 0 25 0 1 0 485084486 195465216 43345 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47721 43345 603 41 0 47680 0
vsize: 190884
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 46073 0 0 0 60885 125 0 0 25 0 1 0 485084486 197427200 43815 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48200 43815 603 41 0 48159 0
vsize: 192800
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 46458 0 0 0 61884 127 0 0 25 0 1 0 485084486 199032832 44200 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48592 44200 603 41 0 48551 0
vsize: 194368
[startup+630.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 46810 0 0 0 62883 128 0 0 25 0 1 0 485084486 200454144 44552 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48939 44552 603 41 0 48898 0
vsize: 195756
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 47146 0 0 0 63883 128 0 0 25 0 1 0 485084486 201768960 44888 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49260 44888 603 41 0 49219 0
vsize: 197040
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 47753 0 0 0 64881 130 0 0 25 0 1 0 485084486 204259328 45495 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49868 45495 603 41 0 49827 0
vsize: 199472
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 48039 0 0 0 65880 132 0 0 25 0 1 0 485084486 205443072 45781 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50157 45781 603 41 0 50116 0
vsize: 200628
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 48505 0 0 0 66878 133 0 0 25 0 1 0 485084486 207290368 46247 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50608 46247 603 41 0 50567 0
vsize: 202432
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 48825 0 0 0 67878 134 0 0 25 0 1 0 485084486 208621568 46567 4294967295 134512640 134672761 3221224544 3221223688 134616339 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50933 46567 603 41 0 50892 0
vsize: 203732
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 49124 0 0 0 68877 135 0 0 25 0 1 0 485084486 209932288 46866 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51253 46866 603 41 0 51212 0
vsize: 205012
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 49607 0 0 0 69876 136 0 0 25 0 1 0 485084486 211914752 47349 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51737 47349 603 41 0 51696 0
vsize: 206948
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 49955 0 0 0 70876 136 0 0 25 0 1 0 485084486 213237760 47697 4294967295 134512640 134672761 3221224544 3221223728 134615614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52060 47697 603 41 0 52019 0
vsize: 208240
[startup+720.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 50368 0 0 0 71875 137 0 0 25 0 1 0 485084486 214953984 48110 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52479 48110 603 41 0 52438 0
vsize: 209916
[startup+730.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 50864 0 0 0 72875 138 0 0 25 0 1 0 485084486 216944640 48606 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52965 48606 603 41 0 52924 0
vsize: 211860
[startup+740.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 51092 0 0 0 73874 139 0 0 25 0 1 0 485084486 217870336 48834 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53191 48834 603 41 0 53150 0
vsize: 212764
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 51260 0 0 0 74874 140 0 0 25 0 1 0 485084486 218660864 49002 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53384 49002 603 41 0 53343 0
vsize: 213536
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 51661 0 0 0 75873 141 0 0 25 0 1 0 485084486 220241920 49403 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53770 49403 603 41 0 53729 0
vsize: 215080
[startup+770.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 51851 0 0 0 76872 141 0 0 25 0 1 0 485084486 221036544 49593 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53964 49593 603 41 0 53923 0
vsize: 215856
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 52226 0 0 0 77872 142 0 0 25 0 1 0 485084486 222494720 49968 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54320 49968 603 41 0 54279 0
vsize: 217280
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 52642 0 0 0 78871 143 0 0 25 0 1 0 485084486 224198656 50384 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54736 50384 603 41 0 54695 0
vsize: 218944
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 53259 0 0 0 79869 145 0 0 25 0 1 0 485084486 226836480 51001 4294967295 134512640 134672761 3221224544 3221223364 1075755419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55380 51001 603 41 0 55339 0
vsize: 221520
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 53887 0 0 0 80868 146 0 0 25 0 1 0 485084486 229347328 51629 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55993 51629 603 41 0 55952 0
vsize: 223972
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 54183 0 0 0 81868 147 0 0 25 0 1 0 485084486 230559744 51925 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56289 51925 603 41 0 56248 0
vsize: 225156
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 54597 0 0 0 82866 148 0 0 25 0 1 0 485084486 232296448 52339 4294967295 134512640 134672761 3221224544 3221223688 134616254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56713 52339 603 41 0 56672 0
vsize: 226852
[startup+840.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 54922 0 0 0 83867 149 0 0 25 0 1 0 485084486 233623552 52664 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57037 52665 603 41 0 56996 0
vsize: 228148
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 55198 0 0 0 84866 150 0 0 25 0 1 0 485084486 234680320 52940 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57295 52940 603 41 0 57254 0
vsize: 229180
[startup+860.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 55501 0 0 0 85865 151 0 0 25 0 1 0 485084486 235995136 53243 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57616 53243 603 41 0 57575 0
vsize: 230464
[startup+870.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 55792 0 0 0 86865 152 0 0 25 0 1 0 485084486 237199360 53534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57910 53534 603 41 0 57869 0
vsize: 231640
[startup+880.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 56297 0 0 0 87864 153 0 0 25 0 1 0 485084486 239198208 54039 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58398 54039 603 41 0 58357 0
vsize: 233592
[startup+890.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 56728 0 0 0 88863 154 0 0 25 0 1 0 485084486 240914432 54470 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58817 54470 603 41 0 58776 0
vsize: 235268
[startup+900.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 57071 0 0 0 89862 155 0 0 25 0 1 0 485084486 242368512 54813 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59172 54813 603 41 0 59131 0
vsize: 236688
[startup+910.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 57457 0 0 0 90861 156 0 0 25 0 1 0 485084486 243937280 55199 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59555 55199 603 41 0 59514 0
vsize: 238220
[startup+920.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 57754 0 0 0 91861 157 0 0 25 0 1 0 485084486 245157888 55496 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59853 55496 603 41 0 59812 0
vsize: 239412
[startup+930.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 58163 0 0 0 92860 159 0 0 25 0 1 0 485084486 246890496 55905 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60276 55905 603 41 0 60235 0
vsize: 241104
[startup+940.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 59222 0 0 0 93858 160 0 0 25 0 1 0 485084486 251215872 56964 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61332 56964 603 41 0 61291 0
vsize: 245328
[startup+950.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 60497 0 0 0 94866 164 0 0 25 0 1 0 485084486 256360448 58239 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62588 58239 603 41 0 62547 0
vsize: 250352
[startup+960.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 60762 0 0 0 95866 165 0 0 25 0 1 0 485084486 257425408 58504 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62848 58504 603 41 0 62807 0
vsize: 251392
[startup+970.181 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 61056 0 0 0 96867 165 0 0 25 0 1 0 485084486 259149824 58798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63269 58798 603 41 0 63228 0
vsize: 253076
[startup+980.185 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 61165 0 0 0 97867 165 0 0 25 0 1 0 485084486 259690496 58907 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63401 58907 603 41 0 63360 0
vsize: 253604
[startup+990.192 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 61422 0 0 0 98867 166 0 0 25 0 1 0 485084486 260743168 59164 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63658 59164 603 41 0 63617 0
vsize: 254632
[startup+1000.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 61712 0 0 0 99867 167 0 0 25 0 1 0 485084486 261926912 59454 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63947 59454 603 41 0 63906 0
vsize: 255788
[startup+1010.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 61896 0 0 0 100866 167 0 0 25 0 1 0 485084486 262590464 59638 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64109 59638 603 41 0 64068 0
vsize: 256436
[startup+1020.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 62137 0 0 0 101866 168 0 0 25 0 1 0 485084486 263639040 59879 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64365 59879 603 41 0 64324 0
vsize: 257460
[startup+1030.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 62566 0 0 0 102865 170 0 0 25 0 1 0 485084486 265351168 60308 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64783 60308 603 41 0 64742 0
vsize: 259132
[startup+1040.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 62798 0 0 0 103864 170 0 0 25 0 1 0 485084486 266276864 60540 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65009 60540 603 41 0 64968 0
vsize: 260036
[startup+1050.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 63423 0 0 0 104863 172 0 0 25 0 1 0 485084486 268898304 61165 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65649 61165 603 41 0 65608 0
vsize: 262596
[startup+1060.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 63837 0 0 0 105863 173 0 0 25 0 1 0 485084486 270606336 61579 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66066 61579 603 41 0 66025 0
vsize: 264264
[startup+1070.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 64143 0 0 0 106863 174 0 0 25 0 1 0 485084486 271806464 61885 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66359 61885 603 41 0 66318 0
vsize: 265436
[startup+1080.22 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 64346 0 0 0 107863 174 0 0 25 0 1 0 485084486 272601088 62088 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66553 62088 603 41 0 66512 0
vsize: 266212
[startup+1090.22 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 64733 0 0 0 108863 174 0 0 25 0 1 0 485084486 274178048 62475 4294967295 134512640 134672761 3221224544 3221223728 134615773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66938 62475 603 41 0 66897 0
vsize: 267752
[startup+1100.22 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 65019 0 0 0 109862 176 0 0 25 0 1 0 485084486 275374080 62761 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67230 62761 603 41 0 67189 0
vsize: 268920
[startup+1110.22 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 65435 0 0 0 110861 177 0 0 25 0 1 0 485084486 277082112 63177 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67647 63177 603 41 0 67606 0
vsize: 270588
[startup+1120.22 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 65878 0 0 0 111860 178 0 0 25 0 1 0 485084486 278908928 63620 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68093 63620 603 41 0 68052 0
vsize: 272372
[startup+1130.23 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 66334 0 0 0 112860 179 0 0 25 0 1 0 485084486 280739840 64076 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68540 64076 603 41 0 68499 0
vsize: 274160
[startup+1140.23 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 66840 0 0 0 113858 180 0 0 25 0 1 0 485084486 282849280 64582 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69055 64582 603 41 0 69014 0
vsize: 276220
[startup+1150.23 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 67188 0 0 0 114858 181 0 0 25 0 1 0 485084486 284192768 64930 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69383 64930 603 41 0 69342 0
vsize: 277532
[startup+1160.23 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 67648 0 0 0 115857 182 0 0 25 0 1 0 485084486 286183424 65390 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69869 65390 603 41 0 69828 0
vsize: 279476
[startup+1170.24 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 68089 0 0 0 116858 183 0 0 25 0 1 0 485084486 287899648 65831 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70288 65831 603 41 0 70247 0
vsize: 281152
[startup+1180.24 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 68500 0 0 0 117857 184 0 0 25 0 1 0 485084486 289615872 66242 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70707 66242 603 41 0 70666 0
vsize: 282828
[startup+1190.25 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 68789 0 0 0 118857 185 0 0 25 0 1 0 485084486 290799616 66531 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70996 66531 603 41 0 70955 0
vsize: 283984
[startup+1200.25 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 22951
Raw data (stat): 22951 (minisat+) R 22950 25285 25284 0 -1 0 69142 0 0 0 119857 185 0 0 25 0 1 0 485084486 292265984 66884 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71354 66884 603 41 0 71313 0
vsize: 285416
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.46 s]
Raw data (loadavg): 1.01 0.99 0.91 1/54 22951
Raw data (stat): 22951 (minisat+) Z 22950 25285 25284 0 -1 12 69142 0 0 0 119857 198 0 0 21 0 1 0 485084486 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.46
CPU time (s): 1200.56
CPU user time (s): 1198.57
CPU system time (s): 1.9837
CPU usage (%): 100.008
Max. virtual memory (Kb): 285416
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####