PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        717760 kB
Buffers:         14000 kB
Cached:         282648 kB
SwapCached:        716 kB
Active:          37584 kB
Inactive:       260936 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        717508 kB
SwapTotal:     2097892 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12664 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 00:10:20 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 13181 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
c ==================================[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.95 0.91 0.89 2/54 17302
Raw data (stat): 17302 (runsolver) R 17301 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549183300 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 11066 0 0 0 967 31 0 0 25 0 1 0 549183300 54525952 10708 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13312 10708 603 41 0 13271 0
vsize: 53248
[startup+20.001 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 11317 0 0 0 1966 32 0 0 25 0 1 0 549183300 55472128 10959 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13543 10959 603 41 0 13502 0
vsize: 54172
[startup+30.0017 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 11733 0 0 0 2965 33 0 0 25 0 1 0 549183300 57221120 11375 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13970 11375 603 41 0 13929 0
vsize: 55880
[startup+40.0018 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 12382 0 0 0 3963 34 0 0 25 0 1 0 549183300 59912192 12024 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14627 12024 603 41 0 14586 0
vsize: 58508
[startup+50.0019 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 12763 0 0 0 4961 37 0 0 25 0 1 0 549183300 61390848 12405 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 12405 603 41 0 14947 0
vsize: 59952
[startup+60.0016 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 13045 0 0 0 5960 38 0 0 25 0 1 0 549183300 62607360 12687 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15285 12687 603 41 0 15244 0
vsize: 61140
[startup+70.0025 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 13336 0 0 0 6959 39 0 0 25 0 1 0 549183300 63815680 12978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15580 12978 603 41 0 15539 0
vsize: 62320
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 13571 0 0 0 7958 39 0 0 25 0 1 0 549183300 64761856 13213 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15811 13213 603 41 0 15770 0
vsize: 63244
[startup+90.0034 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 13931 0 0 0 8957 41 0 0 25 0 1 0 549183300 66322432 13573 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16192 13573 603 41 0 16151 0
vsize: 64768
[startup+100.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 14238 0 0 0 9956 42 0 0 25 0 1 0 549183300 67534848 13880 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16488 13880 603 41 0 16447 0
vsize: 65952
[startup+110.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 14649 0 0 0 10954 44 0 0 25 0 1 0 549183300 69152768 14291 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16883 14291 603 41 0 16842 0
vsize: 67532
[startup+120.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 14999 0 0 0 11953 46 0 0 25 0 1 0 549183300 70631424 14641 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17244 14641 603 41 0 17203 0
vsize: 68976
[startup+130.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 15275 0 0 0 12952 47 0 0 25 0 1 0 549183300 71708672 14917 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17507 14917 603 41 0 17466 0
vsize: 70028
[startup+140.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 15570 0 0 0 13951 47 0 0 25 0 1 0 549183300 72921088 15212 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17803 15212 603 41 0 17762 0
vsize: 71212
[startup+150.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 15956 0 0 0 14950 49 0 0 25 0 1 0 549183300 74543104 15598 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18199 15598 603 41 0 18158 0
vsize: 72796
[startup+160.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 16285 0 0 0 15948 51 0 0 25 0 1 0 549183300 75886592 15927 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18527 15927 603 41 0 18486 0
vsize: 74108
[startup+170.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 16577 0 0 0 16947 52 0 0 25 0 1 0 549183300 76967936 16219 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18791 16219 603 41 0 18750 0
vsize: 75164
[startup+180.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 16885 0 0 0 17946 53 0 0 25 0 1 0 549183300 78446592 16527 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19152 16527 603 41 0 19111 0
vsize: 76608
[startup+190.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 17244 0 0 0 18945 55 0 0 25 0 1 0 549183300 79929344 16886 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19514 16886 603 41 0 19473 0
vsize: 78056
[startup+200.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 17584 0 0 0 19942 57 0 0 25 0 1 0 549183300 81268736 17226 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19841 17226 603 41 0 19800 0
vsize: 79364
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 17949 0 0 0 20941 59 0 0 25 0 1 0 549183300 82743296 17591 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 17591 603 41 0 20160 0
vsize: 80804
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 18169 0 0 0 21941 59 0 0 25 0 1 0 549183300 83689472 17811 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20432 17811 603 41 0 20391 0
vsize: 81728
[startup+230.008 s]
Raw data (loadavg): 1.07 0.96 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 18385 0 0 0 22939 60 0 0 25 0 1 0 549183300 84492288 18027 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20628 18027 603 41 0 20587 0
vsize: 82512
[startup+240.008 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 18814 0 0 0 23938 62 0 0 25 0 1 0 549183300 86253568 18456 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21058 18456 603 41 0 21017 0
vsize: 84232
[startup+250.008 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 19154 0 0 0 24936 64 0 0 25 0 1 0 549183300 87609344 18796 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21389 18796 603 41 0 21348 0
vsize: 85556
[startup+260.009 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 19591 0 0 0 25934 66 0 0 25 0 1 0 549183300 89358336 19233 4294967295 134512640 134672761 3221224544 3221223500 1075350277 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21816 19233 603 41 0 21775 0
vsize: 87264
[startup+270.009 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 19911 0 0 0 26933 67 0 0 25 0 1 0 549183300 90710016 19553 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22146 19553 603 41 0 22105 0
vsize: 88584
[startup+280.01 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 20078 0 0 0 27932 68 0 0 25 0 1 0 549183300 91381760 19720 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22310 19720 603 41 0 22269 0
vsize: 89240
[startup+290.011 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 20360 0 0 0 28931 69 0 0 25 0 1 0 549183300 92606464 20002 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22609 20002 603 41 0 22568 0
vsize: 90436
[startup+300.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 20647 0 0 0 29930 71 0 0 25 0 1 0 549183300 93683712 20289 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22872 20289 603 41 0 22831 0
vsize: 91488
[startup+310.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 21024 0 0 0 30928 73 0 0 25 0 1 0 549183300 95305728 20666 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23268 20666 603 41 0 23227 0
vsize: 93072
[startup+320.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 21308 0 0 0 31927 74 0 0 25 0 1 0 549183300 96387072 20950 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23532 20950 603 41 0 23491 0
vsize: 94128
[startup+330.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 21555 0 0 0 32926 75 0 0 25 0 1 0 549183300 97456128 21197 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23793 21197 603 41 0 23752 0
vsize: 95172
[startup+340.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 21884 0 0 0 33925 76 0 0 25 0 1 0 549183300 98783232 21526 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24117 21526 603 41 0 24076 0
vsize: 96468
[startup+350.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 22157 0 0 0 34923 78 0 0 25 0 1 0 549183300 99860480 21799 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24380 21799 603 41 0 24339 0
vsize: 97520
[startup+360.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 22454 0 0 0 35922 80 0 0 25 0 1 0 549183300 101076992 22096 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24677 22096 603 41 0 24636 0
vsize: 98708
[startup+370.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 23084 0 0 0 36921 81 0 0 25 0 1 0 549183300 103661568 22726 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25308 22726 603 41 0 25267 0
vsize: 101232
[startup+380.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 23439 0 0 0 37919 82 0 0 25 0 1 0 549183300 105144320 23081 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25670 23081 603 41 0 25629 0
vsize: 102680
[startup+390.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 23660 0 0 0 38918 84 0 0 25 0 1 0 549183300 106086400 23302 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25900 23302 603 41 0 25859 0
vsize: 103600
[startup+400.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 23971 0 0 0 39917 85 0 0 25 0 1 0 549183300 107298816 23613 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26196 23613 603 41 0 26155 0
vsize: 104784
[startup+410.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 24300 0 0 0 40916 86 0 0 25 0 1 0 549183300 108896256 23942 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26586 23942 603 41 0 26545 0
vsize: 106344
[startup+420.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 24730 0 0 0 41915 87 0 0 25 0 1 0 549183300 110641152 24372 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27012 24372 603 41 0 26971 0
vsize: 108048
[startup+430.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 25099 0 0 0 42914 88 0 0 25 0 1 0 549183300 112119808 24741 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27373 24741 603 41 0 27332 0
vsize: 109492
[startup+440.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 25456 0 0 0 43913 90 0 0 25 0 1 0 549183300 113598464 25098 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27734 25098 603 41 0 27693 0
vsize: 110936
[startup+450.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 25730 0 0 0 44912 91 0 0 25 0 1 0 549183300 114692096 25372 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28001 25372 603 41 0 27960 0
vsize: 112004
[startup+460.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 25959 0 0 0 45911 92 0 0 25 0 1 0 549183300 115638272 25601 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28232 25601 603 41 0 28191 0
vsize: 112928
[startup+470.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 26203 0 0 0 46910 92 0 0 25 0 1 0 549183300 116580352 25845 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28462 25845 603 41 0 28421 0
vsize: 113848
[startup+480.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 26500 0 0 0 47909 94 0 0 25 0 1 0 549183300 117788672 26142 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28757 26142 603 41 0 28716 0
vsize: 115028
[startup+490.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 26853 0 0 0 48908 95 0 0 25 0 1 0 549183300 119259136 26495 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29116 26495 603 41 0 29075 0
vsize: 116464
[startup+500.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 27090 0 0 0 49907 96 0 0 25 0 1 0 549183300 120201216 26732 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29346 26732 603 41 0 29305 0
vsize: 117384
[startup+510.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 27422 0 0 0 50906 97 0 0 25 0 1 0 549183300 121671680 27064 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29705 27064 603 41 0 29664 0
vsize: 118820
[startup+520.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 27753 0 0 0 51906 97 0 0 25 0 1 0 549183300 123027456 27395 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30036 27395 603 41 0 29995 0
vsize: 120144
[startup+530.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 28038 0 0 0 52905 98 0 0 25 0 1 0 549183300 124092416 27680 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30296 27680 603 41 0 30255 0
vsize: 121184
[startup+540.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 28379 0 0 0 53904 99 0 0 25 0 1 0 549183300 125579264 28021 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30659 28021 603 41 0 30618 0
vsize: 122636
[startup+550.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 28608 0 0 0 54904 100 0 0 25 0 1 0 549183300 126500864 28250 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30884 28250 603 41 0 30843 0
vsize: 123536
[startup+560.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 28913 0 0 0 55903 101 0 0 25 0 1 0 549183300 127713280 28555 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31180 28555 603 41 0 31139 0
vsize: 124720
[startup+570.015 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 29178 0 0 0 56902 102 0 0 25 0 1 0 549183300 128798720 28820 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31445 28820 603 41 0 31404 0
vsize: 125780
[startup+580.016 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 17302
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 29449 0 0 0 57902 102 0 0 25 0 1 0 549183300 129871872 29091 4294967295 134512640 134672761 3221224544 3221223712 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31707 29091 603 41 0 31666 0
vsize: 126828
[startup+590.016 s]
Raw data (loadavg): 1.06 0.99 0.92 3/57 17343
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 29801 0 0 0 58898 107 0 0 25 0 1 0 549183300 131342336 29443 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32066 29443 603 41 0 32025 0
vsize: 128264
[startup+600.016 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 17355
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 30081 0 0 0 59897 107 0 0 25 0 1 0 549183300 132423680 29723 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32330 29723 603 41 0 32289 0
vsize: 129320
[startup+610.016 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 17355
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 30483 0 0 0 60896 109 0 0 25 0 1 0 549183300 134168576 30125 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32756 30125 603 41 0 32715 0
vsize: 131024
[startup+620.016 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 17355
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 30833 0 0 0 61895 110 0 0 25 0 1 0 549183300 135507968 30475 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33083 30475 603 41 0 33042 0
vsize: 132332
[startup+630.016 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 17355
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 31173 0 0 0 62894 111 0 0 25 0 1 0 549183300 136867840 30815 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33415 30815 603 41 0 33374 0
vsize: 133660
[startup+640.017 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 17355
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 31544 0 0 0 63893 112 0 0 25 0 1 0 549183300 138469376 31186 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33806 31186 603 41 0 33765 0
vsize: 135224
[startup+650.016 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 17355
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 31869 0 0 0 64892 114 0 0 25 0 1 0 549183300 139812864 31511 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34134 31511 603 41 0 34093 0
vsize: 136536
[startup+660.017 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 32094 0 0 0 65892 114 0 0 25 0 1 0 549183300 140746752 31736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34362 31736 603 41 0 34321 0
vsize: 137448
[startup+670.016 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 32419 0 0 0 66891 115 0 0 25 0 1 0 549183300 142086144 32061 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34689 32061 603 41 0 34648 0
vsize: 138756
[startup+680.016 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 32739 0 0 0 67891 115 0 0 25 0 1 0 549183300 143294464 32381 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34984 32381 603 41 0 34943 0
vsize: 139936
[startup+690.016 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 32998 0 0 0 68890 116 0 0 25 0 1 0 549183300 144367616 32640 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35246 32640 603 41 0 35205 0
vsize: 140984
[startup+700.016 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 33236 0 0 0 69889 117 0 0 25 0 1 0 549183300 145309696 32878 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35476 32878 603 41 0 35435 0
vsize: 141904
[startup+710.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 33492 0 0 0 70888 118 0 0 25 0 1 0 549183300 146382848 33134 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35738 33134 603 41 0 35697 0
vsize: 142952
[startup+720.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 33793 0 0 0 71888 119 0 0 25 0 1 0 549183300 147595264 33435 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36034 33435 603 41 0 35993 0
vsize: 144136
[startup+730.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 34124 0 0 0 72887 120 0 0 25 0 1 0 549183300 149061632 33766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36392 33766 603 41 0 36351 0
vsize: 145568
[startup+740.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 34427 0 0 0 73887 121 0 0 25 0 1 0 549183300 150274048 34069 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36688 34069 603 41 0 36647 0
vsize: 146752
[startup+750.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 34724 0 0 0 74886 122 0 0 25 0 1 0 549183300 151470080 34366 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36980 34366 603 41 0 36939 0
vsize: 147920
[startup+760.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 35084 0 0 0 75885 123 0 0 25 0 1 0 549183300 152948736 34726 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37341 34726 603 41 0 37300 0
vsize: 149364
[startup+770.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 35353 0 0 0 76884 123 0 0 25 0 1 0 549183300 154021888 34995 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37603 34995 603 41 0 37562 0
vsize: 150412
[startup+780.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 35646 0 0 0 77884 124 0 0 25 0 1 0 549183300 155234304 35288 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37899 35288 603 41 0 37858 0
vsize: 151596
[startup+790.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 36062 0 0 0 78883 125 0 0 25 0 1 0 549183300 156975104 35704 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38324 35704 603 41 0 38283 0
vsize: 153296
[startup+800.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 36289 0 0 0 79882 126 0 0 25 0 1 0 549183300 157782016 35931 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38521 35931 603 41 0 38480 0
vsize: 154084
[startup+810.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 36575 0 0 0 80881 127 0 0 25 0 1 0 549183300 158986240 36217 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38815 36217 603 41 0 38774 0
vsize: 155260
[startup+820.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 36870 0 0 0 81881 128 0 0 25 0 1 0 549183300 160210944 36512 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39114 36512 603 41 0 39073 0
vsize: 156456
[startup+830.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 37208 0 0 0 82880 129 0 0 25 0 1 0 549183300 161546240 36850 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39440 36850 603 41 0 39399 0
vsize: 157760
[startup+840.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 37670 0 0 0 83879 130 0 0 25 0 1 0 549183300 163549184 37312 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39929 37312 603 41 0 39888 0
vsize: 159716
[startup+850.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 38065 0 0 0 84878 131 0 0 25 0 1 0 549183300 165167104 37707 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40324 37707 603 41 0 40283 0
vsize: 161296
[startup+860.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 38404 0 0 0 85878 132 0 0 25 0 1 0 549183300 166510592 38046 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40652 38046 603 41 0 40611 0
vsize: 162608
[startup+870.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 38693 0 0 0 86877 133 0 0 25 0 1 0 549183300 167727104 38335 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40949 38335 603 41 0 40908 0
vsize: 163796
[startup+880.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 39007 0 0 0 87876 134 0 0 25 0 1 0 549183300 168943616 38649 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41246 38649 603 41 0 41205 0
vsize: 164984
[startup+890.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 39284 0 0 0 88876 135 0 0 25 0 1 0 549183300 170024960 38926 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41510 38926 603 41 0 41469 0
vsize: 166040
[startup+900.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 39615 0 0 0 89875 136 0 0 25 0 1 0 549183300 171364352 39257 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41837 39257 603 41 0 41796 0
vsize: 167348
[startup+910.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17357
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 40031 0 0 0 90874 137 0 0 25 0 1 0 549183300 173117440 39673 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42265 39673 603 41 0 42224 0
vsize: 169060
[startup+920.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 40447 0 0 0 91877 138 0 0 25 0 1 0 549183300 174878720 40089 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42695 40089 603 41 0 42654 0
vsize: 170780
[startup+930.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 40847 0 0 0 92876 139 0 0 25 0 1 0 549183300 176484352 40489 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43087 40489 603 41 0 43046 0
vsize: 172348
[startup+940.061 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 41299 0 0 0 93875 140 0 0 25 0 1 0 549183300 178376704 40941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43549 40941 603 41 0 43508 0
vsize: 174196
[startup+950.061 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 41693 0 0 0 94874 141 0 0 25 0 1 0 549183300 179990528 41335 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43943 41335 603 41 0 43902 0
vsize: 175772
[startup+960.061 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 42109 0 0 0 95873 143 0 0 25 0 1 0 549183300 181563392 41751 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44327 41751 603 41 0 44286 0
vsize: 177308
[startup+970.06 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 42440 0 0 0 96873 143 0 0 25 0 1 0 549183300 182915072 42082 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44657 42082 603 41 0 44616 0
vsize: 178628
[startup+980.061 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 42659 0 0 0 97872 144 0 0 25 0 1 0 549183300 183840768 42301 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44883 42301 603 41 0 44842 0
vsize: 179532
[startup+990.062 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 42962 0 0 0 98872 145 0 0 25 0 1 0 549183300 185057280 42604 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45180 42604 603 41 0 45139 0
vsize: 180720
[startup+1000.06 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 43301 0 0 0 99871 146 0 0 25 0 1 0 549183300 186540032 42943 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45542 42943 603 41 0 45501 0
vsize: 182168
[startup+1010.06 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 43634 0 0 0 100870 146 0 0 25 0 1 0 549183300 187891712 43276 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45872 43276 603 41 0 45831 0
vsize: 183488
[startup+1020.06 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 43995 0 0 0 101870 147 0 0 25 0 1 0 549183300 189362176 43637 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46231 43637 603 41 0 46190 0
vsize: 184924
[startup+1030.06 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 44399 0 0 0 102869 148 0 0 25 0 1 0 549183300 190976000 44041 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46625 44041 603 41 0 46584 0
vsize: 186500
[startup+1040.06 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 44657 0 0 0 103867 149 0 0 25 0 1 0 549183300 192585728 44299 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47018 44299 603 41 0 46977 0
vsize: 188072
[startup+1050.07 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 44954 0 0 0 104866 151 0 0 25 0 1 0 549183300 193785856 44596 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47311 44596 603 41 0 47270 0
vsize: 189244
[startup+1060.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 45222 0 0 0 105867 151 0 0 25 0 1 0 549183300 194850816 44864 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47571 44864 603 41 0 47530 0
vsize: 190284
[startup+1070.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 45512 0 0 0 106866 153 0 0 25 0 1 0 549183300 196067328 45154 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47868 45154 603 41 0 47827 0
vsize: 191472
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 45786 0 0 0 107865 153 0 0 25 0 1 0 549183300 197148672 45428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48132 45428 603 41 0 48091 0
vsize: 192528
[startup+1090.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 46129 0 0 0 108865 154 0 0 25 0 1 0 549183300 198615040 45771 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48490 45771 603 41 0 48449 0
vsize: 193960
[startup+1100.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 46489 0 0 0 109864 155 0 0 25 0 1 0 549183300 200093696 46131 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48851 46131 603 41 0 48810 0
vsize: 195404
[startup+1110.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 46817 0 0 0 110863 156 0 0 25 0 1 0 549183300 201437184 46459 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49179 46459 603 41 0 49138 0
vsize: 196716
[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 47078 0 0 0 111863 157 0 0 25 0 1 0 549183300 202514432 46720 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49442 46720 603 41 0 49401 0
vsize: 197768
[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 47306 0 0 0 112862 157 0 0 25 0 1 0 549183300 203448320 46948 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49670 46948 603 41 0 49629 0
vsize: 198680
[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 47582 0 0 0 113862 158 0 0 25 0 1 0 549183300 204517376 47224 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49931 47224 603 41 0 49890 0
vsize: 199724
[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 47922 0 0 0 114861 159 0 0 25 0 1 0 549183300 205864960 47564 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50260 47564 603 41 0 50219 0
vsize: 201040
[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 48283 0 0 0 115860 160 0 0 25 0 1 0 549183300 207335424 47925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50619 47925 603 41 0 50578 0
vsize: 202476
[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 48591 0 0 0 116860 161 0 0 25 0 1 0 549183300 208674816 48233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50946 48233 603 41 0 50905 0
vsize: 203784
[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 48893 0 0 0 117859 162 0 0 25 0 1 0 549183300 209891328 48535 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51243 48535 603 41 0 51202 0
vsize: 204972
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 49197 0 0 0 118860 162 0 0 25 0 1 0 549183300 211103744 48839 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51539 48839 603 41 0 51498 0
vsize: 206156
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 17359
Raw data (stat): 17302 (minisat+) R 17301 28099 28098 0 -1 0 49491 0 0 0 119861 163 0 0 25 0 1 0 549183300 212299776 49133 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51831 49133 603 41 0 51790 0
vsize: 207324
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 17359
Raw data (stat): 17302 (minisat+) Z 17301 28099 28098 0 -1 12 49493 0 0 0 119861 172 0 0 25 0 1 0 549183300 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.2
CPU time (s): 1200.33
CPU user time (s): 1198.61
CPU system time (s): 1.72274
CPU usage (%): 100.011
Max. virtual memory (Kb): 207324
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####