PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-air04.opb
MD5SUM	26490113618ae9605b5ebe6370b5910b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.120981
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 15225

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 03:24:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18173 boxname=wulflinc22 idbench=1398 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  26490113618ae9605b5ebe6370b5910b  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air04.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 18173
/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:        801300 kB
Buffers:         23064 kB
Cached:         179620 kB
SwapCached:         24 kB
Active:          28376 kB
Inactive:       177012 kB
HighTotal:      131008 kB
HighFree:        50568 kB
LowTotal:       903652 kB
LowFree:        750732 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22452 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:44:15 (client local time) WITH STATUS 0 IN 1200.38 SECONDS
stats: 18173 7 1200.38 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       100 |  310358   807732 |  113797     100     2792    27.9 |  0.588 % |
c |       250 |  310331   807657 |  125176     249    12761    51.2 |  0.592 % |
c |       475 |  310198   807286 |  137694     459    35376    77.1 |  0.620 % |
c |       812 |  310052   806901 |  151464     787    48598    61.8 |  0.642 % |
c |      1319 |  309884   806468 |  166610    1289    73251    56.8 |  0.667 % |
c |      2078 |  309785   806192 |  183271    2043   141139    69.1 |  0.692 % |
c |      3217 |  309724   806017 |  201598    3171   279873    88.3 |  0.705 % |
c |      4927 |  309614   805741 |  221758    4872   562380   115.4 |  0.716 % |
c |      7490 |  309614   805741 |  243934    7435  1259451   169.4 |  0.716 % |
c |     11334 |  309475   805377 |  268327   11239  1793736   159.6 |  0.732 % |
c |     17101 |  309226   804713 |  295160   16957  2478519   146.2 |  0.776 % |
c |     25752 |  307768   801003 |  324676   25505  3930547   154.1 |  0.987 % |
c |     38728 |  307515   800363 |  357144   38421  6348349   165.2 |  1.003 % |
c |     58191 |  307356   799958 |  392858   57785 10148314   175.6 |  1.017 % |
c |     87385 |  306886   798753 |  432144   86840 17512694   201.7 |  1.062 % |
c |    131176 |  306715   798313 |  475359  130557 31984227   245.0 |  1.079 % |
#### 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.84 0.94 0.93 2/54 26613
Raw data (stat): 26613 (runsolver) R 26612 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541813592 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0004 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 11064 0 0 0 969 29 0 0 25 0 1 0 541813592 54525952 10706 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13312 10706 603 41 0 13271 0
vsize: 53248
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 11310 0 0 0 1968 30 0 0 25 0 1 0 541813592 55472128 10952 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13543 10952 603 41 0 13502 0
vsize: 54172
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 11709 0 0 0 2966 32 0 0 25 0 1 0 541813592 57085952 11351 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13937 11351 603 41 0 13896 0
vsize: 55748
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 12356 0 0 0 3964 34 0 0 25 0 1 0 541813592 59777024 11998 4294967295 134512640 134672761 3221224544 3221223728 134558324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14594 11998 603 41 0 14553 0
vsize: 58376
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 12745 0 0 0 4963 35 0 0 25 0 1 0 541813592 61390848 12387 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 12387 603 41 0 14947 0
vsize: 59952
[startup+60.0035 s]
Raw data (loadavg): 0.94 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 13035 0 0 0 5961 37 0 0 25 0 1 0 541813592 62607360 12677 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15285 12677 603 41 0 15244 0
vsize: 61140
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 13314 0 0 0 6960 38 0 0 25 0 1 0 541813592 63684608 12956 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15548 12956 603 41 0 15507 0
vsize: 62192
[startup+80.005 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 13562 0 0 0 7959 40 0 0 25 0 1 0 541813592 64761856 13204 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15811 13204 603 41 0 15770 0
vsize: 63244
[startup+90.0057 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 13889 0 0 0 8958 40 0 0 25 0 1 0 541813592 66052096 13531 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16126 13531 603 41 0 16085 0
vsize: 64504
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 14223 0 0 0 9957 41 0 0 25 0 1 0 541813592 67399680 13865 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16455 13865 603 41 0 16414 0
vsize: 65820
[startup+110.007 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 14619 0 0 0 10956 42 0 0 25 0 1 0 541813592 69017600 14261 4294967295 134512640 134672761 3221224544 3221223680 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16850 14261 603 41 0 16809 0
vsize: 67400
[startup+120.008 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 14992 0 0 0 11955 44 0 0 25 0 1 0 541813592 70631424 14634 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17244 14634 603 41 0 17203 0
vsize: 68976
[startup+130.008 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 15236 0 0 0 12954 45 0 0 25 0 1 0 541813592 71577600 14878 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14878 603 41 0 17434 0
vsize: 69900
[startup+140.008 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 15549 0 0 0 13953 46 0 0 25 0 1 0 541813592 72785920 15191 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17770 15191 603 41 0 17729 0
vsize: 71080
[startup+150.01 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 15912 0 0 0 14952 47 0 0 25 0 1 0 541813592 74272768 15554 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18133 15554 603 41 0 18092 0
vsize: 72532
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 16264 0 0 0 15951 49 0 0 25 0 1 0 541813592 75751424 15906 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18494 15906 603 41 0 18453 0
vsize: 73976
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 16536 0 0 0 16950 50 0 0 25 0 1 0 541813592 76832768 16178 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18758 16178 603 41 0 18717 0
vsize: 75032
[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 16873 0 0 0 17949 51 0 0 25 0 1 0 541813592 78311424 16515 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19119 16515 603 41 0 19078 0
vsize: 76476
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 17225 0 0 0 18948 52 0 0 25 0 1 0 541813592 79798272 16867 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19482 16867 603 41 0 19441 0
vsize: 77928
[startup+200.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 17542 0 0 0 19947 53 0 0 25 0 1 0 541813592 81133568 17184 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19808 17184 603 41 0 19767 0
vsize: 79232
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 17931 0 0 0 20946 54 0 0 25 0 1 0 541813592 82608128 17573 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20168 17573 603 41 0 20127 0
vsize: 80672
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 18150 0 0 0 21945 55 0 0 25 0 1 0 541813592 83554304 17792 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20399 17792 603 41 0 20358 0
vsize: 81596
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 18371 0 0 0 22945 56 0 0 25 0 1 0 541813592 84492288 18013 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20628 18013 603 41 0 20587 0
vsize: 82512
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 18786 0 0 0 23943 58 0 0 25 0 1 0 541813592 86118400 18428 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21025 18428 603 41 0 20984 0
vsize: 84100
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 19104 0 0 0 24942 60 0 0 25 0 1 0 541813592 87474176 18746 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21356 18746 603 41 0 21315 0
vsize: 85424
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 19542 0 0 0 25940 61 0 0 25 0 1 0 541813592 89223168 19184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21783 19184 603 41 0 21742 0
vsize: 87132
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 19903 0 0 0 26939 62 0 0 25 0 1 0 541813592 90710016 19545 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22146 19545 603 41 0 22105 0
vsize: 88584
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 20062 0 0 0 27938 63 0 0 25 0 1 0 541813592 91381760 19704 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22310 19704 603 41 0 22269 0
vsize: 89240
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 20334 0 0 0 28938 64 0 0 25 0 1 0 541813592 92463104 19976 4294967295 134512640 134672761 3221224544 3221223712 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22574 19976 603 41 0 22533 0
vsize: 90296
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 20623 0 0 0 29937 65 0 0 25 0 1 0 541813592 93683712 20265 4294967295 134512640 134672761 3221224544 3221223784 134541793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22872 20265 603 41 0 22831 0
vsize: 91488
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 20999 0 0 0 30936 66 0 0 25 0 1 0 541813592 95170560 20641 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23235 20641 603 41 0 23194 0
vsize: 92940
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 21286 0 0 0 31935 67 0 0 25 0 1 0 541813592 96387072 20928 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23532 20928 603 41 0 23491 0
vsize: 94128
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 21546 0 0 0 32934 68 0 0 25 0 1 0 541813592 97456128 21188 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23793 21188 603 41 0 23752 0
vsize: 95172
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 21861 0 0 0 33933 69 0 0 25 0 1 0 541813592 98648064 21503 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24084 21503 603 41 0 24043 0
vsize: 96336
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 22129 0 0 0 34932 70 0 0 25 0 1 0 541813592 99725312 21771 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24347 21771 603 41 0 24306 0
vsize: 97388
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 22404 0 0 0 35932 71 0 0 25 0 1 0 541813592 100941824 22046 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24644 22046 603 41 0 24603 0
vsize: 98576
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 23023 0 0 0 36930 73 0 0 25 0 1 0 541813592 103387136 22665 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25241 22665 603 41 0 25200 0
vsize: 100964
[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 23407 0 0 0 37929 74 0 0 25 0 1 0 541813592 105009152 23049 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25637 23049 603 41 0 25596 0
vsize: 102548
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 23641 0 0 0 38928 75 0 0 25 0 1 0 541813592 105951232 23283 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25867 23283 603 41 0 25826 0
vsize: 103468
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 23945 0 0 0 39927 76 0 0 25 0 1 0 541813592 107167744 23587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26164 23587 603 41 0 26123 0
vsize: 104656
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 24272 0 0 0 40926 77 0 0 25 0 1 0 541813592 108769280 23914 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26555 23914 603 41 0 26514 0
vsize: 106220
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 24692 0 0 0 41924 79 0 0 25 0 1 0 541813592 110505984 24334 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26979 24334 603 41 0 26938 0
vsize: 107916
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 25098 0 0 0 42923 81 0 0 25 0 1 0 541813592 112119808 24740 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27373 24740 603 41 0 27332 0
vsize: 109492
[startup+440.025 s]
Raw data (loadavg): 1.15 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 25433 0 0 0 43922 82 0 0 25 0 1 0 541813592 113463296 25075 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27701 25075 603 41 0 27660 0
vsize: 110804
[startup+450.026 s]
Raw data (loadavg): 1.13 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 25686 0 0 0 44921 83 0 0 25 0 1 0 541813592 114556928 25328 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27968 25328 603 41 0 27927 0
vsize: 111872
[startup+460.025 s]
Raw data (loadavg): 1.11 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 25933 0 0 0 45920 84 0 0 25 0 1 0 541813592 115503104 25575 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28199 25575 603 41 0 28158 0
vsize: 112796
[startup+470.025 s]
Raw data (loadavg): 1.09 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 26167 0 0 0 46919 85 0 0 25 0 1 0 541813592 116449280 25809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28430 25809 603 41 0 28389 0
vsize: 113720
[startup+480.026 s]
Raw data (loadavg): 1.08 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 26464 0 0 0 47919 86 0 0 25 0 1 0 541813592 117653504 26106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28724 26106 603 41 0 28683 0
vsize: 114896
[startup+490.025 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 26808 0 0 0 48918 87 0 0 25 0 1 0 541813592 119123968 26450 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29083 26450 603 41 0 29042 0
vsize: 116332
[startup+500.026 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 27054 0 0 0 49917 88 0 0 25 0 1 0 541813592 120066048 26696 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29313 26696 603 41 0 29272 0
vsize: 117252
[startup+510.026 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 27350 0 0 0 50915 90 0 0 25 0 1 0 541813592 121266176 26992 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29606 26992 603 41 0 29565 0
vsize: 118424
[startup+520.026 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 27704 0 0 0 51914 91 0 0 25 0 1 0 541813592 122757120 27346 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29970 27346 603 41 0 29929 0
vsize: 119880
[startup+530.026 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 27958 0 0 0 52914 92 0 0 25 0 1 0 541813592 123838464 27600 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30234 27600 603 41 0 30193 0
vsize: 120936
[startup+540.026 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 28281 0 0 0 53913 92 0 0 25 0 1 0 541813592 125169664 27923 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30559 27923 603 41 0 30518 0
vsize: 122236
[startup+550.027 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 28502 0 0 0 54913 93 0 0 25 0 1 0 541813592 125980672 28144 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30757 28144 603 41 0 30716 0
vsize: 123028
[startup+560.027 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 28791 0 0 0 55912 94 0 0 25 0 1 0 541813592 127172608 28433 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31048 28433 603 41 0 31007 0
vsize: 124192
[startup+570.027 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 29101 0 0 0 56912 95 0 0 25 0 1 0 541813592 128524288 28743 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31378 28743 603 41 0 31337 0
vsize: 125512
[startup+580.027 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 29364 0 0 0 57910 96 0 0 25 0 1 0 541813592 129601536 29006 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31641 29006 603 41 0 31600 0
vsize: 126564
[startup+590.027 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 29662 0 0 0 58910 97 0 0 25 0 1 0 541813592 130813952 29304 4294967295 134512640 134672761 3221224544 3221223712 134560788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31937 29304 603 41 0 31896 0
vsize: 127748
[startup+600.028 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 29995 0 0 0 59908 98 0 0 25 0 1 0 541813592 132153344 29637 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32264 29637 603 41 0 32223 0
vsize: 129056
[startup+610.028 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 30321 0 0 0 60907 99 0 0 25 0 1 0 541813592 133496832 29963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32592 29963 603 41 0 32551 0
vsize: 130368
[startup+620.028 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 30706 0 0 0 61906 100 0 0 25 0 1 0 541813592 134967296 30348 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32951 30348 603 41 0 32910 0
vsize: 131804
[startup+630.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 31043 0 0 0 62905 102 0 0 25 0 1 0 541813592 136331264 30685 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33284 30685 603 41 0 33243 0
vsize: 133136
[startup+640.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 31355 0 0 0 63904 103 0 0 25 0 1 0 541813592 137674752 30997 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33612 30997 603 41 0 33571 0
vsize: 134448
[startup+650.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 31757 0 0 0 64903 104 0 0 25 0 1 0 541813592 139272192 31399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34002 31399 603 41 0 33961 0
vsize: 136008
[startup+660.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 31957 0 0 0 65903 105 0 0 25 0 1 0 541813592 140075008 31599 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34198 31599 603 41 0 34157 0
vsize: 136792
[startup+670.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 32236 0 0 0 66903 105 0 0 25 0 1 0 541813592 141283328 31878 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34493 31878 603 41 0 34452 0
vsize: 137972
[startup+680.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 32594 0 0 0 67902 106 0 0 25 0 1 0 541813592 142757888 32236 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34853 32236 603 41 0 34812 0
vsize: 139412
[startup+690.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 32853 0 0 0 68901 107 0 0 25 0 1 0 541813592 143835136 32495 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35116 32495 603 41 0 35075 0
vsize: 140464
[startup+700.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 33063 0 0 0 69901 107 0 0 25 0 1 0 541813592 144637952 32705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35312 32705 603 41 0 35271 0
vsize: 141248
[startup+710.033 s]
Raw data (loadavg): 1.08 1.02 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 33325 0 0 0 70901 108 0 0 25 0 1 0 541813592 145707008 32967 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35573 32967 603 41 0 35532 0
vsize: 142292
[startup+720.032 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 33633 0 0 0 71900 109 0 0 25 0 1 0 541813592 147058688 33275 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35903 33275 603 41 0 35862 0
vsize: 143612
[startup+730.032 s]
Raw data (loadavg): 1.06 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 33925 0 0 0 72899 109 0 0 25 0 1 0 541813592 148131840 33567 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36165 33567 603 41 0 36124 0
vsize: 144660
[startup+740.032 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 34233 0 0 0 73899 110 0 0 25 0 1 0 541813592 149467136 33875 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36491 33875 603 41 0 36450 0
vsize: 145964
[startup+750.033 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 34526 0 0 0 74898 111 0 0 25 0 1 0 541813592 150675456 34168 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36786 34168 603 41 0 36745 0
vsize: 147144
[startup+760.032 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 34827 0 0 0 75898 112 0 0 25 0 1 0 541813592 151875584 34469 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37079 34469 603 41 0 37038 0
vsize: 148316
[startup+770.032 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 35173 0 0 0 76897 113 0 0 25 0 1 0 541813592 153214976 34815 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37406 34815 603 41 0 37365 0
vsize: 149624
[startup+780.033 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 35396 0 0 0 77896 114 0 0 25 0 1 0 541813592 154157056 35038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37636 35038 603 41 0 37595 0
vsize: 150544
[startup+790.032 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 35735 0 0 0 78896 114 0 0 25 0 1 0 541813592 155639808 35377 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37998 35377 603 41 0 37957 0
vsize: 151992
[startup+800.034 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 36092 0 0 0 79894 116 0 0 25 0 1 0 541813592 156975104 35734 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38324 35734 603 41 0 38283 0
vsize: 153296
[startup+810.04 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 36357 0 0 0 80894 117 0 0 25 0 1 0 541813592 158179328 35999 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38618 35999 603 41 0 38577 0
vsize: 154472
[startup+820.04 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 36635 0 0 0 81893 118 0 0 25 0 1 0 541813592 159256576 36277 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38881 36277 603 41 0 38840 0
vsize: 155524
[startup+830.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 36896 0 0 0 82893 119 0 0 25 0 1 0 541813592 160346112 36538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39147 36538 603 41 0 39106 0
vsize: 156588
[startup+840.048 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 37259 0 0 0 83893 119 0 0 25 0 1 0 541813592 161800192 36901 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39502 36901 603 41 0 39461 0
vsize: 158008
[startup+850.049 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 37720 0 0 0 84892 121 0 0 25 0 1 0 541813592 163676160 37362 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39960 37362 603 41 0 39919 0
vsize: 159840
[startup+860.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 38109 0 0 0 85891 122 0 0 25 0 1 0 541813592 165302272 37751 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40357 37751 603 41 0 40316 0
vsize: 161428
[startup+870.065 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 38428 0 0 0 86892 122 0 0 25 0 1 0 541813592 166649856 38070 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40686 38070 603 41 0 40645 0
vsize: 162744
[startup+880.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 38707 0 0 0 87891 124 0 0 25 0 1 0 541813592 167727104 38349 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40949 38349 603 41 0 40908 0
vsize: 163796
[startup+890.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 39018 0 0 0 88890 125 0 0 25 0 1 0 541813592 168943616 38660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41246 38660 603 41 0 41205 0
vsize: 164984
[startup+900.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 39285 0 0 0 89890 126 0 0 25 0 1 0 541813592 170024960 38927 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41510 38927 603 41 0 41469 0
vsize: 166040
[startup+910.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 39610 0 0 0 90889 126 0 0 25 0 1 0 541813592 171364352 39252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41837 39252 603 41 0 41796 0
vsize: 167348
[startup+920.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 40023 0 0 0 91889 127 0 0 25 0 1 0 541813592 173117440 39665 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42265 39665 603 41 0 42224 0
vsize: 169060
[startup+930.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 40422 0 0 0 92888 128 0 0 25 0 1 0 541813592 174743552 40064 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42662 40064 603 41 0 42621 0
vsize: 170648
[startup+940.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 40828 0 0 0 93888 129 0 0 25 0 1 0 541813592 176349184 40470 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43054 40470 603 41 0 43013 0
vsize: 172216
[startup+950.072 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 41260 0 0 0 94887 130 0 0 25 0 1 0 541813592 178102272 40902 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43482 40902 603 41 0 43441 0
vsize: 173928
[startup+960.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 41653 0 0 0 95886 131 0 0 25 0 1 0 541813592 179724288 41295 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43878 41295 603 41 0 43837 0
vsize: 175512
[startup+970.071 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 42054 0 0 0 96885 132 0 0 25 0 1 0 541813592 181428224 41696 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44294 41696 603 41 0 44253 0
vsize: 177176
[startup+980.072 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 42425 0 0 0 97884 134 0 0 25 0 1 0 541813592 182915072 42067 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44657 42067 603 41 0 44616 0
vsize: 178628
[startup+990.072 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 42624 0 0 0 98883 134 0 0 25 0 1 0 541813592 183713792 42266 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44852 42266 603 41 0 44811 0
vsize: 179408
[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 42912 0 0 0 99882 135 0 0 25 0 1 0 541813592 184922112 42554 4294967295 134512640 134672761 3221224544 3221223668 134566095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45147 42554 603 41 0 45106 0
vsize: 180588
[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 43247 0 0 0 100882 135 0 0 25 0 1 0 541813592 186269696 42889 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45476 42889 603 41 0 45435 0
vsize: 181904
[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 43535 0 0 0 101882 136 0 0 25 0 1 0 541813592 187490304 43177 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45774 43177 603 41 0 45733 0
vsize: 183096
[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 43917 0 0 0 102881 137 0 0 25 0 1 0 541813592 188968960 43559 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46135 43559 603 41 0 46094 0
vsize: 184540
[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 44313 0 0 0 103880 139 0 0 25 0 1 0 541813592 190566400 43955 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46525 43955 603 41 0 46484 0
vsize: 186100
[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 44576 0 0 0 104879 140 0 0 25 0 1 0 541813592 192176128 44218 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46918 44218 603 41 0 46877 0
vsize: 187672
[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 44851 0 0 0 105879 141 0 0 25 0 1 0 541813592 193388544 44493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47214 44493 603 41 0 47173 0
vsize: 188856
[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 45154 0 0 0 106878 141 0 0 25 0 1 0 541813592 194580480 44796 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47505 44796 603 41 0 47464 0
vsize: 190020
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 45406 0 0 0 107878 142 0 0 25 0 1 0 541813592 195661824 45048 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47769 45048 603 41 0 47728 0
vsize: 191076
[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 45640 0 0 0 108878 142 0 0 25 0 1 0 541813592 196608000 45282 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48000 45282 603 41 0 47959 0
vsize: 192000
[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 45998 0 0 0 109877 143 0 0 25 0 1 0 541813592 198078464 45640 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48359 45640 603 41 0 48318 0
vsize: 193436
[startup+1110.08 s]
Raw data (loadavg): 1.08 1.02 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 46356 0 0 0 110876 144 0 0 25 0 1 0 541813592 199553024 45998 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48719 45998 603 41 0 48678 0
vsize: 194876
[startup+1120.09 s]
Raw data (loadavg): 1.07 1.02 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 46667 0 0 0 111876 145 0 0 25 0 1 0 541813592 200769536 46309 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49016 46309 603 41 0 48975 0
vsize: 196064
[startup+1130.09 s]
Raw data (loadavg): 1.06 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 47003 0 0 0 112876 145 0 0 25 0 1 0 541813592 202108928 46645 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49343 46645 603 41 0 49302 0
vsize: 197372
[startup+1140.1 s]
Raw data (loadavg): 1.05 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 47246 0 0 0 113876 146 0 0 25 0 1 0 541813592 203177984 46888 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49604 46888 603 41 0 49563 0
vsize: 198416
[startup+1150.1 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 47458 0 0 0 114876 147 0 0 25 0 1 0 541813592 203984896 47100 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49801 47100 603 41 0 49760 0
vsize: 199204
[startup+1160.11 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 47753 0 0 0 115876 148 0 0 25 0 1 0 541813592 205189120 47395 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50095 47395 603 41 0 50054 0
vsize: 200380
[startup+1170.12 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 48101 0 0 0 116876 149 0 0 25 0 1 0 541813592 206667776 47743 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50456 47743 603 41 0 50415 0
vsize: 201824
[startup+1180.12 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 48442 0 0 0 117875 149 0 0 25 0 1 0 541813592 208003072 48084 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50782 48084 603 41 0 50741 0
vsize: 203128
[startup+1190.13 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 48694 0 0 0 118875 151 0 0 25 0 1 0 541813592 209080320 48336 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51045 48336 603 41 0 51004 0
vsize: 204180
[startup+1200.14 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 26613
Raw data (stat): 26613 (minisat+) R 26612 26298 26297 0 -1 0 49008 0 0 0 119876 151 0 0 25 0 1 0 541813592 210292736 48650 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51341 48650 603 41 0 51300 0
vsize: 205364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 1.02 1.01 0.95 1/54 26613
Raw data (stat): 26613 (minisat+) Z 26612 26298 26297 0 -1 12 49010 0 0 0 119876 160 0 0 25 0 1 0 541813592 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.23
CPU time (s): 1200.38
CPU user time (s): 1198.77
CPU system time (s): 1.60776
CPU usage (%): 100.012
Max. virtual memory (Kb): 205364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####