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/miplib/normalized-mps-v2-20-10-air04.opb
MD5SUM	eb0734273e24196dd14c6f237b52fa81
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.12098
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 22340

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        754220 kB
Buffers:         18888 kB
Cached:         240712 kB
SwapCached:        364 kB
Active:          29252 kB
Inactive:       232560 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        753968 kB
SwapTotal:     2097136 kB
SwapFree:      2096008 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            12916 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:19:28 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 11659 7 1200.33 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.81 0.94 0.90 2/54 21772
Raw data (stat): 21772 (runsolver) R 21771 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492081813 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.84 0.94 0.90 2/54 21772
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 20915 0 0 0 947 51 0 0 25 0 1 0 492081813 94146560 18657 4294967295 134512640 134672761 3221224544 3221223696 134565092 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.0014 s]
Raw data (loadavg): 0.86 0.94 0.90 2/54 21772
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 21101 0 0 0 1946 51 0 0 25 0 1 0 492081813 94945280 18843 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23180 18843 603 41 0 23139 0
vsize: 92720
[startup+30.0015 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 21772
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 21446 0 0 0 2945 52 0 0 25 0 1 0 492081813 96411648 19188 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23538 19188 603 41 0 23497 0
vsize: 94152
[startup+40.0023 s]
Raw data (loadavg): 0.98 0.96 0.91 3/57 21813
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 21799 0 0 0 3938 59 0 0 25 0 1 0 492081813 97734656 19541 4294967295 134512640 134672761 3221224544 3221223668 134566095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23861 19541 603 41 0 23820 0
vsize: 95444
[startup+50.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21825
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 22115 0 0 0 4936 60 0 0 25 0 1 0 492081813 99049472 19857 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24182 19857 603 41 0 24141 0
vsize: 96728
[startup+60.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21825
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 22570 0 0 0 5936 61 0 0 25 0 1 0 492081813 100933632 20312 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24642 20312 603 41 0 24601 0
vsize: 98568
[startup+70.0046 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21825
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 22869 0 0 0 6935 62 0 0 25 0 1 0 492081813 102117376 20611 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24931 20611 603 41 0 24890 0
vsize: 99724
[startup+80.0044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21825
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 23360 0 0 0 7934 63 0 0 25 0 1 0 492081813 104239104 21102 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25449 21102 603 41 0 25408 0
vsize: 101796
[startup+90.0047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21825
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 23791 0 0 0 8933 65 0 0 25 0 1 0 492081813 105963520 21533 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25870 21533 603 41 0 25829 0
vsize: 103480
[startup+100.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21825
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 24125 0 0 0 9932 66 0 0 25 0 1 0 492081813 107274240 21867 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26190 21867 603 41 0 26149 0
vsize: 104760
[startup+110.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 24426 0 0 0 10931 67 0 0 25 0 1 0 492081813 108609536 22168 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26516 22168 603 41 0 26475 0
vsize: 106064
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 24785 0 0 0 11930 68 0 0 25 0 1 0 492081813 110071808 22527 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26873 22527 603 41 0 26832 0
vsize: 107492
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 25324 0 0 0 12929 70 0 0 25 0 1 0 492081813 112181248 23066 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27388 23066 603 41 0 27347 0
vsize: 109552
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 25598 0 0 0 13928 71 0 0 25 0 1 0 492081813 113381376 23340 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27681 23340 603 41 0 27640 0
vsize: 110724
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 25956 0 0 0 14927 72 0 0 25 0 1 0 492081813 114835456 23698 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28036 23698 603 41 0 27995 0
vsize: 112144
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 26399 0 0 0 15926 73 0 0 25 0 1 0 492081813 116555776 24141 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28456 24141 603 41 0 28415 0
vsize: 113824
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 26965 0 0 0 16924 75 0 0 25 0 1 0 492081813 119058432 24707 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29067 24707 603 41 0 29026 0
vsize: 116268
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 27417 0 0 0 17923 76 0 0 25 0 1 0 492081813 120905728 25159 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29518 25159 603 41 0 29477 0
vsize: 118072
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 27862 0 0 0 18921 78 0 0 25 0 1 0 492081813 122642432 25604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29942 25604 603 41 0 29901 0
vsize: 119768
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 28351 0 0 0 19920 79 0 0 25 0 1 0 492081813 124755968 26093 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30458 26093 603 41 0 30417 0
vsize: 121832
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 28989 0 0 0 20919 81 0 0 25 0 1 0 492081813 127242240 26731 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31065 26731 603 41 0 31024 0
vsize: 124260
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 29328 0 0 0 21919 81 0 0 25 0 1 0 492081813 128692224 27070 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31419 27070 603 41 0 31378 0
vsize: 125676
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 29652 0 0 0 22918 83 0 0 25 0 1 0 492081813 130015232 27394 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31742 27394 603 41 0 31701 0
vsize: 126968
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 29968 0 0 0 23917 84 0 0 25 0 1 0 492081813 131211264 27710 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32034 27710 603 41 0 31993 0
vsize: 128136
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 30324 0 0 0 24916 84 0 0 25 0 1 0 492081813 132673536 28066 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32391 28066 603 41 0 32350 0
vsize: 129564
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 30799 0 0 0 25915 86 0 0 25 0 1 0 492081813 134656000 28541 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32875 28541 603 41 0 32834 0
vsize: 131500
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 31229 0 0 0 26914 87 0 0 25 0 1 0 492081813 136507392 28971 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33327 28971 603 41 0 33286 0
vsize: 133308
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 31664 0 0 0 27913 88 0 0 25 0 1 0 492081813 138231808 29406 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33748 29406 603 41 0 33707 0
vsize: 134992
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 31900 0 0 0 28912 89 0 0 25 0 1 0 492081813 139300864 29642 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34009 29642 603 41 0 33968 0
vsize: 136036
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 32316 0 0 0 29911 90 0 0 25 0 1 0 492081813 140877824 30058 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34394 30058 603 41 0 34353 0
vsize: 137576
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 32682 0 0 0 30911 91 0 0 25 0 1 0 492081813 142454784 30424 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34779 30424 603 41 0 34738 0
vsize: 139116
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 33159 0 0 0 31910 92 0 0 25 0 1 0 492081813 144429056 30901 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35261 30901 603 41 0 35220 0
vsize: 141044
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 33613 0 0 0 32908 94 0 0 25 0 1 0 492081813 146276352 31355 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35712 31355 603 41 0 35671 0
vsize: 142848
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 34111 0 0 0 33907 96 0 0 25 0 1 0 492081813 148254720 31853 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36195 31853 603 41 0 36154 0
vsize: 144780
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 34411 0 0 0 34906 97 0 0 25 0 1 0 492081813 149454848 32153 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36488 32153 603 41 0 36447 0
vsize: 145952
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 34708 0 0 0 35906 97 0 0 25 0 1 0 492081813 150667264 32450 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36784 32450 603 41 0 36743 0
vsize: 147136
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 34982 0 0 0 36905 98 0 0 25 0 1 0 492081813 151851008 32724 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37073 32724 603 41 0 37032 0
vsize: 148292
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 35344 0 0 0 37904 99 0 0 25 0 1 0 492081813 153325568 33086 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37433 33086 603 41 0 37392 0
vsize: 149732
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 36066 0 0 0 38903 101 0 0 25 0 1 0 492081813 156483584 33808 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38204 33808 603 41 0 38163 0
vsize: 152816
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21827
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 36753 0 0 0 39901 102 0 0 25 0 1 0 492081813 159383552 34495 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38912 34495 603 41 0 38871 0
vsize: 155648
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 37511 0 0 0 40900 104 0 0 25 0 1 0 492081813 162418688 35253 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39653 35253 603 41 0 39612 0
vsize: 158612
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 38146 0 0 0 41899 105 0 0 25 0 1 0 492081813 165064704 35888 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40299 35888 603 41 0 40258 0
vsize: 161196
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 38954 0 0 0 42896 108 0 0 25 0 1 0 492081813 168325120 36696 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41095 36696 603 41 0 41054 0
vsize: 164380
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 39359 0 0 0 43895 109 0 0 25 0 1 0 492081813 170029056 37101 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41511 37101 603 41 0 41470 0
vsize: 166044
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 39606 0 0 0 44895 109 0 0 25 0 1 0 492081813 170954752 37348 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41737 37348 603 41 0 41696 0
vsize: 166948
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 39918 0 0 0 45894 110 0 0 25 0 1 0 492081813 172269568 37660 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42058 37660 603 41 0 42017 0
vsize: 168232
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 40111 0 0 0 46894 111 0 0 25 0 1 0 492081813 173072384 37853 4294967295 134512640 134672761 3221224544 3221223744 134610528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42254 37853 603 41 0 42213 0
vsize: 169016
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 40477 0 0 0 47893 112 0 0 25 0 1 0 492081813 174522368 38219 4294967295 134512640 134672761 3221224544 3221223584 134614207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42608 38219 603 41 0 42567 0
vsize: 170432
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 40748 0 0 0 48893 112 0 0 25 0 1 0 492081813 175595520 38490 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42870 38490 603 41 0 42829 0
vsize: 171480
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 41392 0 0 0 49892 114 0 0 25 0 1 0 492081813 178225152 39134 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43512 39134 603 41 0 43471 0
vsize: 174048
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 41928 0 0 0 50890 115 0 0 25 0 1 0 492081813 180465664 39670 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44059 39670 603 41 0 44018 0
vsize: 176236
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 42408 0 0 0 51889 117 0 0 25 0 1 0 492081813 182435840 40150 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44540 40150 603 41 0 44499 0
vsize: 178160
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 42798 0 0 0 52889 117 0 0 25 0 1 0 492081813 184004608 40540 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44923 40540 603 41 0 44882 0
vsize: 179692
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 43202 0 0 0 53888 118 0 0 25 0 1 0 492081813 185712640 40944 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45340 40944 603 41 0 45299 0
vsize: 181360
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 43690 0 0 0 54886 120 0 0 25 0 1 0 492081813 187682816 41432 4294967295 134512640 134672761 3221224544 3221223688 134616284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45821 41432 603 41 0 45780 0
vsize: 183284
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 43893 0 0 0 55885 121 0 0 25 0 1 0 492081813 188477440 41635 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46015 41635 603 41 0 45974 0
vsize: 184060
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 44410 0 0 0 56884 122 0 0 25 0 1 0 492081813 190582784 42152 4294967295 134512640 134672761 3221224544 3221223668 134565983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46529 42152 603 41 0 46488 0
vsize: 186116
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 44848 0 0 0 57883 124 0 0 25 0 1 0 492081813 192425984 42590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46979 42590 603 41 0 46938 0
vsize: 187916
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 45202 0 0 0 58882 125 0 0 25 0 1 0 492081813 193900544 42944 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47339 42944 603 41 0 47298 0
vsize: 189356
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 45633 0 0 0 59880 127 0 0 25 0 1 0 492081813 195596288 43375 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47753 43375 603 41 0 47712 0
vsize: 191012
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 46096 0 0 0 60880 127 0 0 25 0 1 0 492081813 197562368 43838 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48233 43838 603 41 0 48192 0
vsize: 192932
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 46497 0 0 0 61879 129 0 0 25 0 1 0 492081813 199163904 44239 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48624 44239 603 41 0 48583 0
vsize: 194496
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 46824 0 0 0 62878 130 0 0 25 0 1 0 492081813 200454144 44566 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48939 44566 603 41 0 48898 0
vsize: 195756
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 47168 0 0 0 63878 130 0 0 25 0 1 0 492081813 201904128 44910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49293 44910 603 41 0 49252 0
vsize: 197172
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 47768 0 0 0 64876 132 0 0 25 0 1 0 492081813 204394496 45510 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49901 45510 603 41 0 49860 0
vsize: 199604
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 48046 0 0 0 65875 133 0 0 25 0 1 0 492081813 205443072 45788 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50157 45788 603 41 0 50116 0
vsize: 200628
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 48511 0 0 0 66875 133 0 0 25 0 1 0 492081813 207425536 46253 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50641 46253 603 41 0 50600 0
vsize: 202564
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 48825 0 0 0 67875 134 0 0 25 0 1 0 492081813 208621568 46567 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50933 46567 603 41 0 50892 0
vsize: 203732
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 49143 0 0 0 68874 135 0 0 25 0 1 0 492081813 209932288 46885 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51253 46885 603 41 0 51212 0
vsize: 205012
[startup+700.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 49629 0 0 0 69872 137 0 0 25 0 1 0 492081813 211914752 47371 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51737 47371 603 41 0 51696 0
vsize: 206948
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 49966 0 0 0 70871 138 0 0 25 0 1 0 492081813 213368832 47708 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52092 47708 603 41 0 52051 0
vsize: 208368
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 50384 0 0 0 71870 139 0 0 25 0 1 0 492081813 215089152 48126 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52512 48126 603 41 0 52471 0
vsize: 210048
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 50876 0 0 0 72869 140 0 0 25 0 1 0 492081813 217079808 48618 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52998 48618 603 41 0 52957 0
vsize: 211992
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 51105 0 0 0 73869 141 0 0 25 0 1 0 492081813 218001408 48847 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53223 48847 603 41 0 53182 0
vsize: 212892
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 51283 0 0 0 74868 142 0 0 25 0 1 0 492081813 218660864 49025 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53384 49025 603 41 0 53343 0
vsize: 213536
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 51681 0 0 0 75868 142 0 0 25 0 1 0 492081813 220377088 49423 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53803 49423 603 41 0 53762 0
vsize: 215212
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 51868 0 0 0 76867 143 0 0 25 0 1 0 492081813 221036544 49610 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53964 49610 603 41 0 53923 0
vsize: 215856
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 52235 0 0 0 77867 144 0 0 25 0 1 0 492081813 222625792 49977 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54352 49977 603 41 0 54311 0
vsize: 217408
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 52683 0 0 0 78866 145 0 0 25 0 1 0 492081813 224464896 50425 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54801 50425 603 41 0 54760 0
vsize: 219204
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 53313 0 0 0 79864 147 0 0 25 0 1 0 492081813 226967552 51055 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55412 51055 603 41 0 55371 0
vsize: 221648
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 53904 0 0 0 80863 148 0 0 25 0 1 0 492081813 229347328 51646 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55993 51646 603 41 0 55952 0
vsize: 223972
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 54194 0 0 0 81863 148 0 0 25 0 1 0 492081813 230559744 51936 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56289 51936 603 41 0 56248 0
vsize: 225156
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 54597 0 0 0 82862 149 0 0 25 0 1 0 492081813 232296448 52339 4294967295 134512640 134672761 3221224544 3221223688 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56713 52339 603 41 0 56672 0
vsize: 226852
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 54932 0 0 0 83861 150 0 0 25 0 1 0 492081813 233623552 52674 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57037 52674 603 41 0 56996 0
vsize: 228148
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 55201 0 0 0 84860 151 0 0 25 0 1 0 492081813 234680320 52943 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57295 52943 603 41 0 57254 0
vsize: 229180
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 55524 0 0 0 85860 152 0 0 25 0 1 0 492081813 235995136 53266 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57616 53266 603 41 0 57575 0
vsize: 230464
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 55799 0 0 0 86859 153 0 0 25 0 1 0 492081813 237199360 53541 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57910 53541 603 41 0 57869 0
vsize: 231640
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 56308 0 0 0 87857 155 0 0 25 0 1 0 492081813 239198208 54050 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58398 54050 603 41 0 58357 0
vsize: 233592
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 56758 0 0 0 88857 155 0 0 25 0 1 0 492081813 241045504 54500 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58849 54500 603 41 0 58808 0
vsize: 235396
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 57076 0 0 0 89856 156 0 0 25 0 1 0 492081813 242368512 54818 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59172 54818 603 41 0 59131 0
vsize: 236688
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 57474 0 0 0 90855 157 0 0 25 0 1 0 492081813 244072448 55216 4294967295 134512640 134672761 3221224544 3221223584 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59588 55216 603 41 0 59547 0
vsize: 238352
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 57767 0 0 0 91855 158 0 0 25 0 1 0 492081813 245157888 55509 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59853 55509 603 41 0 59812 0
vsize: 239412
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 58185 0 0 0 92854 159 0 0 25 0 1 0 492081813 246890496 55927 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60276 55927 603 41 0 60235 0
vsize: 241104
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 59264 0 0 0 93852 161 0 0 25 0 1 0 492081813 251346944 57006 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61364 57006 603 41 0 61323 0
vsize: 245456
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 60497 0 0 0 94850 163 0 0 25 0 1 0 492081813 256360448 58239 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62588 58239 603 41 0 62547 0
vsize: 250352
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 60766 0 0 0 95850 164 0 0 25 0 1 0 492081813 257425408 58508 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62848 58508 603 41 0 62807 0
vsize: 251392
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 61061 0 0 0 96849 165 0 0 25 0 1 0 492081813 259149824 58803 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63269 58803 603 41 0 63228 0
vsize: 253076
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 61167 0 0 0 97849 165 0 0 25 0 1 0 492081813 259690496 58909 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63401 58909 603 41 0 63360 0
vsize: 253604
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 61422 0 0 0 98848 166 0 0 25 0 1 0 492081813 260743168 59164 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63658 59164 603 41 0 63617 0
vsize: 254632
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 61717 0 0 0 99848 167 0 0 25 0 1 0 492081813 261926912 59459 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63947 59459 603 41 0 63906 0
vsize: 255788
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 61896 0 0 0 100847 167 0 0 25 0 1 0 492081813 262590464 59638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64109 59638 603 41 0 64068 0
vsize: 256436
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 62145 0 0 0 101846 168 0 0 25 0 1 0 492081813 263639040 59887 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64365 59887 603 41 0 64324 0
vsize: 257460
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 62579 0 0 0 102846 169 0 0 25 0 1 0 492081813 265482240 60321 4294967295 134512640 134672761 3221224544 3221223584 134612963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64815 60321 603 41 0 64774 0
vsize: 259260
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 62800 0 0 0 103845 170 0 0 25 0 1 0 492081813 266276864 60542 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65009 60542 603 41 0 64968 0
vsize: 260036
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 63435 0 0 0 104845 171 0 0 25 0 1 0 492081813 268898304 61177 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65649 61177 603 41 0 65608 0
vsize: 262596
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 63839 0 0 0 105844 172 0 0 25 0 1 0 492081813 270606336 61581 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66066 61581 603 41 0 66025 0
vsize: 264264
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 64143 0 0 0 106843 172 0 0 25 0 1 0 492081813 271806464 61885 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66359 61885 603 41 0 66318 0
vsize: 265436
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 64350 0 0 0 107842 173 0 0 25 0 1 0 492081813 272601088 62092 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66553 62092 603 41 0 66512 0
vsize: 266212
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 64736 0 0 0 108842 174 0 0 25 0 1 0 492081813 274178048 62478 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66938 62478 603 41 0 66897 0
vsize: 267752
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 65020 0 0 0 109842 175 0 0 25 0 1 0 492081813 275374080 62762 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67230 62763 603 41 0 67189 0
vsize: 268920
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 65449 0 0 0 110841 175 0 0 25 0 1 0 492081813 277082112 63191 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67647 63191 603 41 0 67606 0
vsize: 270588
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 65878 0 0 0 111840 176 0 0 25 0 1 0 492081813 278908928 63620 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68093 63620 603 41 0 68052 0
vsize: 272372
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 66345 0 0 0 112839 177 0 0 25 0 1 0 492081813 280739840 64087 4294967295 134512640 134672761 3221224544 3221223720 134615853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68540 64087 603 41 0 68499 0
vsize: 274160
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 66845 0 0 0 113837 179 0 0 25 0 1 0 492081813 282849280 64587 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69055 64587 603 41 0 69014 0
vsize: 276220
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 67193 0 0 0 114837 180 0 0 25 0 1 0 492081813 284327936 64935 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69416 64935 603 41 0 69375 0
vsize: 277664
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 67654 0 0 0 115835 182 0 0 25 0 1 0 492081813 286183424 65396 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69869 65396 603 41 0 69828 0
vsize: 279476
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 68089 0 0 0 116835 183 0 0 25 0 1 0 492081813 287899648 65831 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70288 65831 603 41 0 70247 0
vsize: 281152
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 68501 0 0 0 117833 184 0 0 25 0 1 0 492081813 289615872 66243 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70707 66244 603 41 0 70666 0
vsize: 282828
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 68797 0 0 0 118833 185 0 0 25 0 1 0 492081813 290799616 66539 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70996 66539 603 41 0 70955 0
vsize: 283984
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21829
Raw data (stat): 21772 (minisat+) R 21771 5897 5896 0 -1 0 69144 0 0 0 119832 186 0 0 25 0 1 0 492081813 292265984 66886 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71354 66886 603 41 0 71313 0
vsize: 285416
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 21829
Raw data (stat): 21772 (minisat+) Z 21771 5897 5896 0 -1 12 69144 0 0 0 119833 199 0 0 25 0 1 0 492081813 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.17
CPU time (s): 1200.33
CPU user time (s): 1198.33
CPU system time (s): 1.9947
CPU usage (%): 100.013
Max. virtual memory (Kb): 285416
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####