PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.119981
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 15812

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        722716 kB
Buffers:         28468 kB
Cached:         252756 kB
SwapCached:         24 kB
Active:          31308 kB
Inactive:       252604 kB
HighTotal:      131008 kB
HighFree:        14392 kB
LowTotal:       903652 kB
LowFree:        708324 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22340 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:08:58 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 16651 7 1200.32 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   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.92 0.95 0.95 2/54 27450
Raw data (stat): 27450 (runsolver) R 27449 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542682013 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.0009 s]
Raw data (loadavg): 0.93 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 20915 0 0 0 940 58 0 0 25 0 1 0 542682013 94146560 18657 4294967295 134512640 134672761 3221224544 3221223728 134615727 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.0055 s]
Raw data (loadavg): 0.94 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 21088 0 0 0 1940 58 0 0 25 0 1 0 542682013 94945280 18830 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23180 18830 603 41 0 23139 0
vsize: 92720
[startup+30.0054 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 21442 0 0 0 2939 59 0 0 25 0 1 0 542682013 96280576 19184 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23506 19184 603 41 0 23465 0
vsize: 94024
[startup+40.0059 s]
Raw data (loadavg): 0.96 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 21807 0 0 0 3938 61 0 0 25 0 1 0 542682013 97734656 19549 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23861 19549 603 41 0 23820 0
vsize: 95444
[startup+50.0056 s]
Raw data (loadavg): 0.96 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 22118 0 0 0 4937 62 0 0 25 0 1 0 542682013 99049472 19860 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24182 19860 603 41 0 24141 0
vsize: 96728
[startup+60.0056 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 22577 0 0 0 5936 63 0 0 25 0 1 0 542682013 100933632 20319 4294967295 134512640 134672761 3221224544 3221223720 134615850 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24642 20319 603 41 0 24601 0
vsize: 98568
[startup+70.006 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 22889 0 0 0 6935 64 0 0 25 0 1 0 542682013 102248448 20631 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24963 20631 603 41 0 24922 0
vsize: 99852
[startup+80.0057 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 23367 0 0 0 7934 65 0 0 25 0 1 0 542682013 104239104 21109 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25449 21109 603 41 0 25408 0
vsize: 101796
[startup+90.0057 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 23805 0 0 0 8933 66 0 0 25 0 1 0 542682013 105963520 21547 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25870 21547 603 41 0 25829 0
vsize: 103480
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 24179 0 0 0 9933 67 0 0 25 0 1 0 542682013 107536384 21921 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26254 21921 603 41 0 26213 0
vsize: 105016
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 24438 0 0 0 10933 67 0 0 25 0 1 0 542682013 108609536 22180 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26516 22180 603 41 0 26475 0
vsize: 106064
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 24829 0 0 0 11932 68 0 0 25 0 1 0 542682013 110202880 22571 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26905 22571 603 41 0 26864 0
vsize: 107620
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 25392 0 0 0 12929 71 0 0 25 0 1 0 542682013 112443392 23134 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27452 23134 603 41 0 27411 0
vsize: 109808
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 25638 0 0 0 13928 72 0 0 25 0 1 0 542682013 113512448 23380 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27713 23380 603 41 0 27672 0
vsize: 110852
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 26032 0 0 0 14927 74 0 0 25 0 1 0 542682013 115097600 23774 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28100 23774 603 41 0 28059 0
vsize: 112400
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 26503 0 0 0 15925 75 0 0 25 0 1 0 542682013 116953088 24245 4294967295 134512640 134672761 3221224544 3221223728 134615722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28553 24245 603 41 0 28512 0
vsize: 114212
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 27068 0 0 0 16924 77 0 0 25 0 1 0 542682013 119451648 24810 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29163 24810 603 41 0 29122 0
vsize: 116652
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 27493 0 0 0 17922 78 0 0 25 0 1 0 542682013 121167872 25235 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29582 25235 603 41 0 29541 0
vsize: 118328
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 27963 0 0 0 18921 80 0 0 25 0 1 0 542682013 123170816 25705 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30071 25705 603 41 0 30030 0
vsize: 120284
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 28400 0 0 0 19921 81 0 0 25 0 1 0 542682013 124887040 26142 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30490 26142 603 41 0 30449 0
vsize: 121960
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 29068 0 0 0 20919 82 0 0 25 0 1 0 542682013 127639552 26810 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31162 26810 603 41 0 31121 0
vsize: 124648
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 29400 0 0 0 21919 83 0 0 25 0 1 0 542682013 128954368 27142 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31483 27142 603 41 0 31442 0
vsize: 125932
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 29704 0 0 0 22918 84 0 0 25 0 1 0 542682013 130146304 27446 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31774 27446 603 41 0 31733 0
vsize: 127096
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 30054 0 0 0 23916 86 0 0 25 0 1 0 542682013 131612672 27796 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32132 27796 603 41 0 32091 0
vsize: 128528
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 30536 0 0 0 24914 88 0 0 25 0 1 0 542682013 133595136 28278 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32616 28278 603 41 0 32575 0
vsize: 130464
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 30891 0 0 0 25913 89 0 0 25 0 1 0 542682013 135061504 28633 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32974 28633 603 41 0 32933 0
vsize: 131896
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 31351 0 0 0 26912 91 0 0 25 0 1 0 542682013 137043968 29093 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33458 29093 603 41 0 33417 0
vsize: 133832
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 31722 0 0 0 27911 92 0 0 25 0 1 0 542682013 138493952 29464 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33812 29464 603 41 0 33771 0
vsize: 135248
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 32033 0 0 0 28911 92 0 0 25 0 1 0 542682013 139829248 29775 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34138 29775 603 41 0 34097 0
vsize: 136552
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 32452 0 0 0 29910 94 0 0 25 0 1 0 542682013 141537280 30194 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34555 30194 603 41 0 34514 0
vsize: 138220
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 32915 0 0 0 30909 94 0 0 25 0 1 0 542682013 143376384 30657 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35004 30657 603 41 0 34963 0
vsize: 140016
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 33301 0 0 0 31908 95 0 0 25 0 1 0 542682013 144953344 31043 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35389 31043 603 41 0 35348 0
vsize: 141556
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 33802 0 0 0 32907 97 0 0 25 0 1 0 542682013 147066880 31544 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35905 31544 603 41 0 35864 0
vsize: 143620
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 34216 0 0 0 33906 98 0 0 25 0 1 0 542682013 148652032 31958 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36292 31958 603 41 0 36251 0
vsize: 145168
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 34491 0 0 0 34906 98 0 0 25 0 1 0 542682013 149856256 32233 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36586 32233 603 41 0 36545 0
vsize: 146344
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 34827 0 0 0 35905 99 0 0 25 0 1 0 542682013 151195648 32569 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36913 32569 603 41 0 36872 0
vsize: 147652
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 35119 0 0 0 36905 100 0 0 25 0 1 0 542682013 152383488 32861 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37203 32861 603 41 0 37162 0
vsize: 148812
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 35707 0 0 0 37903 102 0 0 25 0 1 0 542682013 155041792 33449 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37852 33449 603 41 0 37811 0
vsize: 151408
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 36375 0 0 0 38902 103 0 0 25 0 1 0 542682013 157806592 34117 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38527 34117 603 41 0 38486 0
vsize: 154108
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 37155 0 0 0 39900 105 0 0 25 0 1 0 542682013 160968704 34897 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39299 34897 603 41 0 39258 0
vsize: 157196
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 37856 0 0 0 40898 107 0 0 25 0 1 0 542682013 163856384 35598 4294967295 134512640 134672761 3221224544 3221223536 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40004 35598 603 41 0 39963 0
vsize: 160016
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 38512 0 0 0 41896 109 0 0 25 0 1 0 542682013 166510592 36254 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40652 36254 603 41 0 40611 0
vsize: 162608
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 39127 0 0 0 42894 111 0 0 25 0 1 0 542682013 168984576 36869 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41256 36869 603 41 0 41215 0
vsize: 165024
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 39510 0 0 0 43893 112 0 0 25 0 1 0 542682013 170561536 37252 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41641 37252 603 41 0 41600 0
vsize: 166564
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 39787 0 0 0 44892 113 0 0 25 0 1 0 542682013 171745280 37529 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41930 37529 603 41 0 41889 0
vsize: 167720
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 40013 0 0 0 45892 114 0 0 25 0 1 0 542682013 172666880 37755 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42155 37755 603 41 0 42114 0
vsize: 168620
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 40295 0 0 0 46892 114 0 0 25 0 1 0 542682013 173744128 38037 4294967295 134512640 134672761 3221224544 3221223688 134616258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42418 38037 603 41 0 42377 0
vsize: 169672
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 40680 0 0 0 47891 116 0 0 25 0 1 0 542682013 175321088 38422 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42803 38422 603 41 0 42762 0
vsize: 171212
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 41083 0 0 0 48890 117 0 0 25 0 1 0 542682013 177041408 38825 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43223 38825 603 41 0 43182 0
vsize: 172892
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 41694 0 0 0 49888 119 0 0 25 0 1 0 542682013 179548160 39436 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43835 39436 603 41 0 43794 0
vsize: 175340
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 42158 0 0 0 50886 120 0 0 25 0 1 0 542682013 181387264 39900 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44284 39900 603 41 0 44243 0
vsize: 177136
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 42629 0 0 0 51885 122 0 0 25 0 1 0 542682013 183353344 40371 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44764 40371 603 41 0 44723 0
vsize: 179056
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 43090 0 0 0 52884 124 0 0 25 0 1 0 542682013 185180160 40832 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45210 40832 603 41 0 45169 0
vsize: 180840
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 43442 0 0 0 53882 125 0 0 25 0 1 0 542682013 186634240 41184 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45565 41184 603 41 0 45524 0
vsize: 182260
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 43769 0 0 0 54881 126 0 0 25 0 1 0 542682013 187944960 41511 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45885 41511 603 41 0 45844 0
vsize: 183540
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 44232 0 0 0 55881 127 0 0 25 0 1 0 542682013 189919232 41974 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46367 41974 603 41 0 46326 0
vsize: 185468
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 44718 0 0 0 56879 128 0 0 25 0 1 0 542682013 191901696 42460 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46851 42460 603 41 0 46810 0
vsize: 187404
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 45067 0 0 0 57878 130 0 0 25 0 1 0 542682013 193347584 42809 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47204 42809 603 41 0 47163 0
vsize: 188816
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 45436 0 0 0 58877 131 0 0 25 0 1 0 542682013 194822144 43178 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47564 43178 603 41 0 47523 0
vsize: 190256
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 45944 0 0 0 59876 132 0 0 25 0 1 0 542682013 196911104 43686 4294967295 134512640 134672761 3221224544 3221223536 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48074 43686 603 41 0 48033 0
vsize: 192296
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 46351 0 0 0 60875 134 0 0 25 0 1 0 542682013 198496256 44093 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48461 44093 603 41 0 48420 0
vsize: 193844
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 46713 0 0 0 61874 135 0 0 25 0 1 0 542682013 200056832 44455 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48842 44455 603 41 0 48801 0
vsize: 195368
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 47049 0 0 0 62873 136 0 0 25 0 1 0 542682013 201375744 44791 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49164 44791 603 41 0 49123 0
vsize: 196656
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 47626 0 0 0 63871 138 0 0 25 0 1 0 542682013 203735040 45368 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49740 45368 603 41 0 49699 0
vsize: 198960
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 47968 0 0 0 64870 139 0 0 25 0 1 0 542682013 205180928 45710 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50093 45710 603 41 0 50052 0
vsize: 200372
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 27450
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 48447 0 0 0 65869 140 0 0 25 0 1 0 542682013 207130624 46189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50569 46189 603 41 0 50528 0
vsize: 202276
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 27453
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 48764 0 0 0 66868 142 0 0 25 0 1 0 542682013 208359424 46506 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50869 46506 603 41 0 50828 0
vsize: 203476
[startup+680.005 s]
Raw data (loadavg): 1.07 0.99 0.95 2/56 27497
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 49056 0 0 0 67865 143 0 0 25 0 1 0 542682013 209539072 46798 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51157 46798 603 41 0 51116 0
vsize: 204628
[startup+690.006 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 27503
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 49518 0 0 0 68864 145 0 0 25 0 1 0 542682013 211517440 47260 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51640 47260 603 41 0 51599 0
vsize: 206560
[startup+700.006 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 27503
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 49900 0 0 0 69863 146 0 0 25 0 1 0 542682013 213102592 47642 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52027 47642 603 41 0 51986 0
vsize: 208108
[startup+710.006 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 27503
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 50312 0 0 0 70862 146 0 0 25 0 1 0 542682013 214687744 48054 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52414 48054 603 41 0 52373 0
vsize: 209656
[startup+720.005 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 27503
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 50806 0 0 0 71860 149 0 0 25 0 1 0 542682013 216813568 48548 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52933 48548 603 41 0 52892 0
vsize: 211732
[startup+730.005 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 27503
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 51069 0 0 0 72860 149 0 0 25 0 1 0 542682013 217870336 48811 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53191 48811 603 41 0 53150 0
vsize: 212764
[startup+740.006 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 27503
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 51218 0 0 0 73860 149 0 0 25 0 1 0 542682013 218398720 48960 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53320 48960 603 41 0 53279 0
vsize: 213280
[startup+750.008 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 27503
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 51617 0 0 0 74859 150 0 0 25 0 1 0 542682013 220114944 49359 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53739 49359 603 41 0 53698 0
vsize: 214956
[startup+760.008 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 51830 0 0 0 75859 151 0 0 25 0 1 0 542682013 220905472 49572 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53932 49572 603 41 0 53891 0
vsize: 215728
[startup+770.009 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 52189 0 0 0 76857 153 0 0 25 0 1 0 542682013 222363648 49931 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54288 49931 603 41 0 54247 0
vsize: 217152
[startup+780.009 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 52569 0 0 0 77856 154 0 0 25 0 1 0 542682013 223936512 50311 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54672 50311 603 41 0 54631 0
vsize: 218688
[startup+790.009 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 53145 0 0 0 78854 156 0 0 25 0 1 0 542682013 226316288 50887 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55253 50887 603 41 0 55212 0
vsize: 221012
[startup+800.009 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 53861 0 0 0 79853 158 0 0 25 0 1 0 542682013 229216256 51603 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55961 51603 603 41 0 55920 0
vsize: 223844
[startup+810.01 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 54160 0 0 0 80851 160 0 0 25 0 1 0 542682013 230428672 51902 4294967295 134512640 134672761 3221224544 3221223696 134614481 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56257 51902 603 41 0 56216 0
vsize: 225028
[startup+820.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 54597 0 0 0 81850 161 0 0 25 0 1 0 542682013 232296448 52339 4294967295 134512640 134672761 3221224544 3221223688 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56713 52339 603 41 0 56672 0
vsize: 226852
[startup+830.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 54905 0 0 0 82850 162 0 0 25 0 1 0 542682013 233488384 52647 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57004 52647 603 41 0 56963 0
vsize: 228016
[startup+840.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 55196 0 0 0 83849 163 0 0 25 0 1 0 542682013 234680320 52938 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57295 52938 603 41 0 57254 0
vsize: 229180
[startup+850.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 55493 0 0 0 84848 164 0 0 25 0 1 0 542682013 235864064 53235 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57584 53235 603 41 0 57543 0
vsize: 230336
[startup+860.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 55790 0 0 0 85847 165 0 0 25 0 1 0 542682013 237199360 53532 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57910 53532 603 41 0 57869 0
vsize: 231640
[startup+870.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 56301 0 0 0 86846 166 0 0 25 0 1 0 542682013 239198208 54043 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58398 54043 603 41 0 58357 0
vsize: 233592
[startup+880.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 56743 0 0 0 87844 168 0 0 25 0 1 0 542682013 241045504 54485 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58849 54485 603 41 0 58808 0
vsize: 235396
[startup+890.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 57074 0 0 0 88843 169 0 0 25 0 1 0 542682013 242368512 54816 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59172 54816 603 41 0 59131 0
vsize: 236688
[startup+900.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 57474 0 0 0 89843 170 0 0 25 0 1 0 542682013 244072448 55216 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59588 55216 603 41 0 59547 0
vsize: 238352
[startup+910.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 57768 0 0 0 90842 170 0 0 25 0 1 0 542682013 245157888 55510 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59853 55510 603 41 0 59812 0
vsize: 239412
[startup+920.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 58200 0 0 0 91841 171 0 0 25 0 1 0 542682013 247025664 55942 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60309 55942 603 41 0 60268 0
vsize: 241236
[startup+930.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 59328 0 0 0 92839 174 0 0 25 0 1 0 542682013 251592704 57070 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61424 57070 603 41 0 61383 0
vsize: 245696
[startup+940.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 60497 0 0 0 93836 177 0 0 25 0 1 0 542682013 256360448 58239 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62588 58239 603 41 0 62547 0
vsize: 250352
[startup+950.011 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 60810 0 0 0 94835 178 0 0 25 0 1 0 542682013 258215936 58552 4294967295 134512640 134672761 3221224544 3221223584 134614246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63041 58552 603 41 0 63000 0
vsize: 252164
[startup+960.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 61075 0 0 0 95835 179 0 0 25 0 1 0 542682013 259284992 58817 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63302 58817 603 41 0 63261 0
vsize: 253208
[startup+970.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 61192 0 0 0 96835 179 0 0 25 0 1 0 542682013 259690496 58934 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63401 58934 603 41 0 63360 0
vsize: 253604
[startup+980.012 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 61422 0 0 0 97835 179 0 0 25 0 1 0 542682013 260743168 59164 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63658 59164 603 41 0 63617 0
vsize: 254632
[startup+990.013 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 61744 0 0 0 98832 181 0 0 25 0 1 0 542682013 262057984 59486 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63979 59486 603 41 0 63938 0
vsize: 255916
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 61908 0 0 0 99832 181 0 0 25 0 1 0 542682013 262721536 59650 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64141 59650 603 41 0 64100 0
vsize: 256564
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 62185 0 0 0 100831 182 0 0 25 0 1 0 542682013 263770112 59927 4294967295 134512640 134672761 3221224544 3221223808 134618040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64397 59927 603 41 0 64356 0
vsize: 257588
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 62635 0 0 0 101831 183 0 0 25 0 1 0 542682013 265609216 60377 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64846 60377 603 41 0 64805 0
vsize: 259384
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27505
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 62862 0 0 0 102830 184 0 0 25 0 1 0 542682013 266539008 60604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65073 60604 603 41 0 65032 0
vsize: 260292
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 63534 0 0 0 103828 186 0 0 25 0 1 0 542682013 269303808 61276 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65748 61276 603 41 0 65707 0
vsize: 262992
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 63912 0 0 0 104828 187 0 0 25 0 1 0 542682013 270868480 61654 4294967295 134512640 134672761 3221224544 3221223680 134614713 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66130 61654 603 41 0 66089 0
vsize: 264520
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 64143 0 0 0 105828 187 0 0 25 0 1 0 542682013 271806464 61885 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66359 61885 603 41 0 66318 0
vsize: 265436
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 64420 0 0 0 106827 188 0 0 25 0 1 0 542682013 272871424 62162 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66619 62162 603 41 0 66578 0
vsize: 266476
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 64808 0 0 0 107826 189 0 0 25 0 1 0 542682013 274579456 62550 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67036 62550 603 41 0 66995 0
vsize: 268144
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 65103 0 0 0 108825 190 0 0 25 0 1 0 542682013 275767296 62845 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67326 62845 603 41 0 67285 0
vsize: 269304
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 65550 0 0 0 109824 191 0 0 25 0 1 0 542682013 277602304 63292 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67774 63292 603 41 0 67733 0
vsize: 271096
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 65984 0 0 0 110824 192 0 0 25 0 1 0 542682013 279298048 63726 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68188 63726 603 41 0 68147 0
vsize: 272752
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 66550 0 0 0 111823 193 0 0 25 0 1 0 542682013 281665536 64292 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68766 64292 603 41 0 68725 0
vsize: 275064
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 66942 0 0 0 112822 194 0 0 25 0 1 0 542682013 283262976 64684 4294967295 134512640 134672761 3221224544 3221223680 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69156 64684 603 41 0 69115 0
vsize: 276624
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 67297 0 0 0 113823 194 0 0 25 0 1 0 542682013 284725248 65039 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69513 65039 603 41 0 69472 0
vsize: 278052
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 67783 0 0 0 114821 196 0 0 25 0 1 0 542682013 286711808 65525 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69998 65525 603 41 0 69957 0
vsize: 279992
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 68215 0 0 0 115821 197 0 0 25 0 1 0 542682013 288432128 65957 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70418 65957 603 41 0 70377 0
vsize: 281672
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 68610 0 0 0 116819 198 0 0 25 0 1 0 542682013 290009088 66352 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70803 66352 603 41 0 70762 0
vsize: 283212
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 68892 0 0 0 117819 199 0 0 25 0 1 0 542682013 291196928 66634 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71093 66634 603 41 0 71052 0
vsize: 284372
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 69345 0 0 0 118818 200 0 0 25 0 1 0 542682013 293060608 67087 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71548 67087 603 41 0 71507 0
vsize: 286192
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 27507
Raw data (stat): 27450 (minisat+) R 27449 26298 26297 0 -1 0 69793 0 0 0 119817 201 0 0 25 0 1 0 542682013 294907904 67535 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71999 67535 603 41 0 71958 0
vsize: 287996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 27507
Raw data (stat): 27450 (minisat+) Z 27449 26298 26297 0 -1 12 69793 0 0 0 119818 213 0 0 25 0 1 0 542682013 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.32
CPU user time (s): 1198.18
CPU system time (s): 2.13768
CPU usage (%): 100.014
Max. virtual memory (Kb): 287996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####