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 15234

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        876496 kB
Buffers:         30332 kB
Cached:         105328 kB
SwapCached:          0 kB
Active:          43420 kB
Inactive:        94740 kB
HighTotal:      131008 kB
HighFree:        51408 kB
LowTotal:       903652 kB
LowFree:        825088 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            14220 kB
Committed_AS:    63548 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:49:28 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 18166 7 1200.27 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.92 0.95 0.90 2/54 23305
Raw data (stat): 23305 (runsolver) R 23304 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483633171 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0011 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 11063 0 0 0 968 30 0 0 25 0 1 0 483633171 54525952 10705 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13312 10705 603 41 0 13271 0
vsize: 53248
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 11307 0 0 0 1967 30 0 0 25 0 1 0 483633171 55472128 10949 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13543 10949 603 41 0 13502 0
vsize: 54172
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 11693 0 0 0 2966 32 0 0 25 0 1 0 483633171 57085952 11335 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13937 11335 603 41 0 13896 0
vsize: 55748
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 12339 0 0 0 3963 34 0 0 25 0 1 0 483633171 59641856 11981 4294967295 134512640 134672761 3221224624 3221223728 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14561 11981 603 41 0 14520 0
vsize: 58244
[startup+50.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 12744 0 0 0 4961 35 0 0 25 0 1 0 483633171 61390848 12386 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 12386 603 41 0 14947 0
vsize: 59952
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 13029 0 0 0 5960 36 0 0 25 0 1 0 483633171 62472192 12671 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15252 12671 603 41 0 15211 0
vsize: 61008
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 13295 0 0 0 6959 37 0 0 25 0 1 0 483633171 63549440 12937 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15515 12937 603 41 0 15474 0
vsize: 62060
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 13544 0 0 0 7959 38 0 0 25 0 1 0 483633171 64626688 13186 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15778 13186 603 41 0 15737 0
vsize: 63112
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 13825 0 0 0 8958 39 0 0 25 0 1 0 483633171 65781760 13467 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16060 13467 603 41 0 16019 0
vsize: 64240
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 14180 0 0 0 9956 40 0 0 25 0 1 0 483633171 67264512 13822 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16422 13822 603 41 0 16381 0
vsize: 65688
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 14551 0 0 0 10956 42 0 0 25 0 1 0 483633171 68747264 14193 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16784 14193 603 41 0 16743 0
vsize: 67136
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 14959 0 0 0 11953 44 0 0 25 0 1 0 483633171 70496256 14601 4294967295 134512640 134672761 3221224624 3221223784 134565025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17211 14601 603 41 0 17170 0
vsize: 68844
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 15201 0 0 0 12953 45 0 0 25 0 1 0 483633171 71442432 14843 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17442 14843 603 41 0 17401 0
vsize: 69768
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 15472 0 0 0 13951 46 0 0 25 0 1 0 483633171 72515584 15114 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17704 15114 603 41 0 17663 0
vsize: 70816
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 15822 0 0 0 14950 47 0 0 25 0 1 0 483633171 74002432 15464 4294967295 134512640 134672761 3221224624 3221223792 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18067 15464 603 41 0 18026 0
vsize: 72268
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 16209 0 0 0 15949 48 0 0 25 0 1 0 483633171 75481088 15851 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18428 15851 603 41 0 18387 0
vsize: 73712
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 16471 0 0 0 16948 49 0 0 25 0 1 0 483633171 76562432 16113 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18692 16113 603 41 0 18651 0
vsize: 74768
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 16848 0 0 0 17947 50 0 0 25 0 1 0 483633171 78311424 16490 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19119 16490 603 41 0 19078 0
vsize: 76476
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 17098 0 0 0 18946 52 0 0 25 0 1 0 483633171 79257600 16740 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19350 16740 603 41 0 19309 0
vsize: 77400
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 17443 0 0 0 19945 53 0 0 25 0 1 0 483633171 80728064 17085 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19709 17085 603 41 0 19668 0
vsize: 78836
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 17856 0 0 0 20944 54 0 0 25 0 1 0 483633171 82341888 17498 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20103 17498 603 41 0 20062 0
vsize: 80412
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 18094 0 0 0 21943 55 0 0 25 0 1 0 483633171 83283968 17736 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 17736 603 41 0 20292 0
vsize: 81332
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 18306 0 0 0 22943 56 0 0 25 0 1 0 483633171 84226048 17948 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20563 17948 603 41 0 20522 0
vsize: 82252
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 18670 0 0 0 23942 57 0 0 25 0 1 0 483633171 85712896 18312 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20926 18312 603 41 0 20885 0
vsize: 83704
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 18964 0 0 0 24941 58 0 0 25 0 1 0 483633171 86790144 18606 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21189 18606 603 41 0 21148 0
vsize: 84756
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 19387 0 0 0 25940 59 0 0 25 0 1 0 483633171 88551424 19029 4294967295 134512640 134672761 3221224624 3221223760 134560714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21619 19029 603 41 0 21578 0
vsize: 86476
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 19784 0 0 0 26940 60 0 0 25 0 1 0 483633171 90169344 19426 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22014 19426 603 41 0 21973 0
vsize: 88056
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 20000 0 0 0 27939 61 0 0 25 0 1 0 483633171 91111424 19642 4294967295 134512640 134672761 3221224624 3221223728 134559958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22244 19642 603 41 0 22203 0
vsize: 88976
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 20225 0 0 0 28938 62 0 0 25 0 1 0 483633171 92057600 19867 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22475 19867 603 41 0 22434 0
vsize: 89900
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 20496 0 0 0 29938 63 0 0 25 0 1 0 483633171 93143040 20138 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22740 20138 603 41 0 22699 0
vsize: 90960
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 20842 0 0 0 30937 63 0 0 25 0 1 0 483633171 94494720 20484 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23070 20484 603 41 0 23029 0
vsize: 92280
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 21191 0 0 0 31936 64 0 0 25 0 1 0 483633171 95981568 20833 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23433 20833 603 41 0 23392 0
vsize: 93732
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 21438 0 0 0 32936 65 0 0 25 0 1 0 483633171 96923648 21080 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23663 21080 603 41 0 23622 0
vsize: 94652
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 21697 0 0 0 33935 66 0 0 25 0 1 0 483633171 97988608 21339 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23923 21339 603 41 0 23882 0
vsize: 95692
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 21982 0 0 0 34933 68 0 0 25 0 1 0 483633171 99184640 21624 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24215 21624 603 41 0 24174 0
vsize: 96860
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 22245 0 0 0 35932 69 0 0 25 0 1 0 483633171 100265984 21887 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24479 21887 603 41 0 24438 0
vsize: 97916
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 22717 0 0 0 36931 70 0 0 25 0 1 0 483633171 102162432 22359 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24942 22359 603 41 0 24901 0
vsize: 99768
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 23261 0 0 0 37930 71 0 0 25 0 1 0 483633171 104341504 22903 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25474 22903 603 41 0 25433 0
vsize: 101896
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 23524 0 0 0 38929 72 0 0 25 0 1 0 483633171 105410560 23166 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25735 23166 603 41 0 25694 0
vsize: 102940
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 23773 0 0 0 39928 73 0 0 25 0 1 0 483633171 106491904 23415 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25999 23415 603 41 0 25958 0
vsize: 103996
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 24134 0 0 0 40927 74 0 0 25 0 1 0 483633171 107970560 23776 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26360 23776 603 41 0 26319 0
vsize: 105440
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 24416 0 0 0 41927 75 0 0 25 0 1 0 483633171 109293568 24058 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26683 24058 603 41 0 26642 0
vsize: 106732
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 24884 0 0 0 42925 76 0 0 25 0 1 0 483633171 111181824 24526 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27144 24526 603 41 0 27103 0
vsize: 108576
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 25219 0 0 0 43925 77 0 0 25 0 1 0 483633171 112652288 24861 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27503 24861 603 41 0 27462 0
vsize: 110012
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 25497 0 0 0 44924 78 0 0 25 0 1 0 483633171 113733632 25139 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27767 25139 603 41 0 27726 0
vsize: 111068
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 25824 0 0 0 45924 79 0 0 25 0 1 0 483633171 115101696 25466 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28101 25466 603 41 0 28060 0
vsize: 112404
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 26017 0 0 0 46923 79 0 0 25 0 1 0 483633171 115908608 25659 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28298 25659 603 41 0 28257 0
vsize: 113192
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 26273 0 0 0 47923 80 0 0 25 0 1 0 483633171 116985856 25915 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28561 25915 603 41 0 28520 0
vsize: 114244
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 26609 0 0 0 48922 81 0 0 25 0 1 0 483633171 118312960 26251 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28885 26251 603 41 0 28844 0
vsize: 115540
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 26900 0 0 0 49922 82 0 0 25 0 1 0 483633171 119525376 26542 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29181 26542 603 41 0 29140 0
vsize: 116724
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 27150 0 0 0 50922 83 0 0 25 0 1 0 483633171 120471552 26792 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29412 26792 603 41 0 29371 0
vsize: 117648
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 27487 0 0 0 51921 83 0 0 25 0 1 0 483633171 121937920 27129 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29770 27129 603 41 0 29729 0
vsize: 119080
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 27827 0 0 0 52920 84 0 0 25 0 1 0 483633171 123297792 27469 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30102 27469 603 41 0 30061 0
vsize: 120408
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 28099 0 0 0 53920 85 0 0 25 0 1 0 483633171 124358656 27741 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30361 27741 603 41 0 30320 0
vsize: 121444
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 28423 0 0 0 54919 86 0 0 25 0 1 0 483633171 125714432 28065 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30692 28065 603 41 0 30651 0
vsize: 122768
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 28660 0 0 0 55918 87 0 0 25 0 1 0 483633171 126636032 28302 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 28302 603 41 0 30876 0
vsize: 123668
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 28946 0 0 0 56917 88 0 0 25 0 1 0 483633171 127848448 28588 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31213 28588 603 41 0 31172 0
vsize: 124852
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 29202 0 0 0 57917 89 0 0 25 0 1 0 483633171 128933888 28844 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31478 28844 603 41 0 31437 0
vsize: 125912
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 29475 0 0 0 58917 90 0 0 25 0 1 0 483633171 130007040 29117 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31740 29117 603 41 0 31699 0
vsize: 126960
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 29834 0 0 0 59915 90 0 0 25 0 1 0 483633171 131477504 29476 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32099 29476 603 41 0 32058 0
vsize: 128396
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 30094 0 0 0 60915 91 0 0 25 0 1 0 483633171 132558848 29736 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32363 29736 603 41 0 32322 0
vsize: 129452
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 30504 0 0 0 61914 92 0 0 25 0 1 0 483633171 134168576 30146 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32756 30146 603 41 0 32715 0
vsize: 131024
[startup+630.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 30834 0 0 0 62913 93 0 0 25 0 1 0 483633171 135507968 30476 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33083 30476 603 41 0 33042 0
vsize: 132332
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 31166 0 0 0 63913 94 0 0 25 0 1 0 483633171 136867840 30808 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33415 30808 603 41 0 33374 0
vsize: 133660
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 31527 0 0 0 64912 95 0 0 25 0 1 0 483633171 138338304 31169 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33774 31169 603 41 0 33733 0
vsize: 135096
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 31851 0 0 0 65911 96 0 0 25 0 1 0 483633171 139677696 31493 4294967295 134512640 134672761 3221224624 3221223728 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34101 31493 603 41 0 34060 0
vsize: 136404
[startup+670.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 32065 0 0 0 66911 96 0 0 25 0 1 0 483633171 140611584 31707 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34329 31707 603 41 0 34288 0
vsize: 137316
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 32373 0 0 0 67910 97 0 0 25 0 1 0 483633171 141819904 32015 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34624 32015 603 41 0 34583 0
vsize: 138496
[startup+690.029 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 32704 0 0 0 68909 98 0 0 25 0 1 0 483633171 143159296 32346 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34951 32346 603 41 0 34910 0
vsize: 139804
[startup+700.028 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 32970 0 0 0 69909 99 0 0 25 0 1 0 483633171 144232448 32612 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35213 32612 603 41 0 35172 0
vsize: 140852
[startup+710.029 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 33178 0 0 0 70908 99 0 0 25 0 1 0 483633171 145174528 32820 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35443 32820 603 41 0 35402 0
vsize: 141772
[startup+720.029 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 33444 0 0 0 71908 100 0 0 25 0 1 0 483633171 146247680 33086 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35705 33086 603 41 0 35664 0
vsize: 142820
[startup+730.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 33735 0 0 0 72907 101 0 0 25 0 1 0 483633171 147460096 33377 4294967295 134512640 134672761 3221224624 3221223728 134560177 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36001 33377 603 41 0 35960 0
vsize: 144004
[startup+740.028 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 34042 0 0 0 73906 102 0 0 25 0 1 0 483633171 148652032 33684 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36292 33684 603 41 0 36251 0
vsize: 145168
[startup+750.027 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 34341 0 0 0 74906 102 0 0 25 0 1 0 483633171 149872640 33983 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36590 33983 603 41 0 36549 0
vsize: 146360
[startup+760.028 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 34642 0 0 0 75905 103 0 0 25 0 1 0 483633171 151064576 34284 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36881 34284 603 41 0 36840 0
vsize: 147524
[startup+770.027 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 34970 0 0 0 76905 104 0 0 25 0 1 0 483633171 152416256 34612 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37211 34612 603 41 0 37170 0
vsize: 148844
[startup+780.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 35260 0 0 0 77904 105 0 0 25 0 1 0 483633171 153616384 34902 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37504 34902 603 41 0 37463 0
vsize: 150016
[startup+790.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 35517 0 0 0 78903 106 0 0 25 0 1 0 483633171 154697728 35159 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37768 35159 603 41 0 37727 0
vsize: 151072
[startup+800.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 35892 0 0 0 79902 107 0 0 25 0 1 0 483633171 156168192 35534 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38127 35534 603 41 0 38086 0
vsize: 152508
[startup+810.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 36186 0 0 0 80901 108 0 0 25 0 1 0 483633171 157376512 35828 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38422 35828 603 41 0 38381 0
vsize: 153688
[startup+820.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 36453 0 0 0 81901 109 0 0 25 0 1 0 483633171 158449664 36095 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38684 36095 603 41 0 38643 0
vsize: 154736
[startup+830.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 36714 0 0 0 82900 110 0 0 25 0 1 0 483633171 159526912 36356 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38947 36356 603 41 0 38906 0
vsize: 155788
[startup+840.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 36986 0 0 0 83899 111 0 0 25 0 1 0 483633171 160739328 36628 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39243 36628 603 41 0 39202 0
vsize: 156972
[startup+850.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 37446 0 0 0 84898 112 0 0 25 0 1 0 483633171 162611200 37088 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39700 37088 603 41 0 39659 0
vsize: 158800
[startup+860.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 37844 0 0 0 85897 113 0 0 25 0 1 0 483633171 164212736 37486 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40091 37486 603 41 0 40050 0
vsize: 160364
[startup+870.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 38226 0 0 0 86897 114 0 0 25 0 1 0 483633171 165699584 37868 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40454 37868 603 41 0 40413 0
vsize: 161816
[startup+880.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 38529 0 0 0 87896 115 0 0 25 0 1 0 483633171 167051264 38171 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40784 38171 603 41 0 40743 0
vsize: 163136
[startup+890.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 38806 0 0 0 88896 116 0 0 25 0 1 0 483633171 168132608 38448 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41048 38448 603 41 0 41007 0
vsize: 164192
[startup+900.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 39124 0 0 0 89895 116 0 0 25 0 1 0 483633171 169484288 38766 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41378 38766 603 41 0 41337 0
vsize: 165512
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 39377 0 0 0 90894 117 0 0 25 0 1 0 483633171 170430464 39019 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41609 39019 603 41 0 41568 0
vsize: 166436
[startup+920.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 39775 0 0 0 91893 119 0 0 25 0 1 0 483633171 172040192 39417 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42002 39417 603 41 0 41961 0
vsize: 168008
[startup+930.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 40171 0 0 0 92892 120 0 0 25 0 1 0 483633171 173649920 39813 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42395 39813 603 41 0 42354 0
vsize: 169580
[startup+940.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 40574 0 0 0 93891 121 0 0 25 0 1 0 483633171 175288320 40216 4294967295 134512640 134672761 3221224624 3221223824 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42795 40216 603 41 0 42754 0
vsize: 171180
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 40964 0 0 0 94890 122 0 0 25 0 1 0 483633171 176881664 40606 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43184 40606 603 41 0 43143 0
vsize: 172736
[startup+960.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 41392 0 0 0 95889 123 0 0 25 0 1 0 483633171 178647040 41034 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43615 41034 603 41 0 43574 0
vsize: 174460
[startup+970.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 41777 0 0 0 96888 125 0 0 25 0 1 0 483633171 180248576 41419 4294967295 134512640 134672761 3221224624 3221223728 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44006 41419 603 41 0 43965 0
vsize: 176024
[startup+980.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 42184 0 0 0 97888 125 0 0 25 0 1 0 483633171 181972992 41826 4294967295 134512640 134672761 3221224624 3221223728 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44427 41826 603 41 0 44386 0
vsize: 177708
[startup+990.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 42474 0 0 0 98887 126 0 0 25 0 1 0 483633171 183177216 42116 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44721 42116 603 41 0 44680 0
vsize: 178884
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 42707 0 0 0 99887 127 0 0 25 0 1 0 483633171 184111104 42349 4294967295 134512640 134672761 3221224624 3221223808 134559553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44949 42349 603 41 0 44908 0
vsize: 179796
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 43018 0 0 0 100886 128 0 0 25 0 1 0 483633171 185327616 42660 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45246 42660 603 41 0 45205 0
vsize: 180984
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 43338 0 0 0 101885 129 0 0 25 0 1 0 483633171 186675200 42980 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45575 42980 603 41 0 45534 0
vsize: 182300
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 43684 0 0 0 102885 129 0 0 25 0 1 0 483633171 188026880 43326 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45905 43326 603 41 0 45864 0
vsize: 183620
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 44020 0 0 0 103884 130 0 0 25 0 1 0 483633171 189362176 43662 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46231 43662 603 41 0 46190 0
vsize: 184924
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 44413 0 0 0 104884 131 0 0 25 0 1 0 483633171 190976000 44055 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46625 44055 603 41 0 46584 0
vsize: 186500
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 44670 0 0 0 105883 131 0 0 25 0 1 0 483633171 192585728 44312 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47018 44312 603 41 0 46977 0
vsize: 188072
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 44961 0 0 0 106882 132 0 0 25 0 1 0 483633171 193785856 44603 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47311 44603 603 41 0 47270 0
vsize: 189244
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 45223 0 0 0 107882 133 0 0 25 0 1 0 483633171 194850816 44865 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47571 44865 603 41 0 47530 0
vsize: 190284
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 45509 0 0 0 108881 133 0 0 25 0 1 0 483633171 196067328 45151 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47868 45151 603 41 0 47827 0
vsize: 191472
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 45767 0 0 0 109880 135 0 0 25 0 1 0 483633171 197148672 45409 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48132 45409 603 41 0 48091 0
vsize: 192528
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 46108 0 0 0 110879 136 0 0 25 0 1 0 483633171 198483968 45750 4294967295 134512640 134672761 3221224624 3221223808 134559516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48458 45750 603 41 0 48417 0
vsize: 193832
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 46448 0 0 0 111878 137 0 0 25 0 1 0 483633171 199823360 46090 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48785 46090 603 41 0 48744 0
vsize: 195140
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 46787 0 0 0 112878 138 0 0 25 0 1 0 483633171 201306112 46429 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49147 46429 603 41 0 49106 0
vsize: 196588
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 47078 0 0 0 113877 138 0 0 25 0 1 0 483633171 202514432 46720 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49442 46720 603 41 0 49401 0
vsize: 197768
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 47279 0 0 0 114877 139 0 0 25 0 1 0 483633171 203313152 46921 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49637 46921 603 41 0 49596 0
vsize: 198548
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 47536 0 0 0 115876 140 0 0 25 0 1 0 483633171 204382208 47178 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49898 47178 603 41 0 49857 0
vsize: 199592
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 47856 0 0 0 116875 141 0 0 25 0 1 0 483633171 205594624 47498 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50194 47498 603 41 0 50153 0
vsize: 200776
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 48204 0 0 0 117875 142 0 0 25 0 1 0 483633171 207069184 47846 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50554 47846 603 41 0 50513 0
vsize: 202216
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 48543 0 0 0 118874 143 0 0 25 0 1 0 483633171 208408576 48185 4294967295 134512640 134672761 3221224624 3221223776 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50881 48185 603 41 0 50840 0
vsize: 203524
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 23305
Raw data (stat): 23305 (minisat+) R 23304 25347 25346 0 -1 0 48797 0 0 0 119873 143 0 0 25 0 1 0 483633171 209481728 48439 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51143 48439 603 41 0 51102 0
vsize: 204572
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 23305
Raw data (stat): 23305 (minisat+) Z 23304 25347 25346 0 -1 12 48799 0 0 0 119873 152 0 0 25 0 1 0 483633171 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.12
CPU time (s): 1200.27
CPU user time (s): 1198.74
CPU system time (s): 1.52877
CPU usage (%): 100.012
Max. virtual memory (Kb): 204572
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####