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 16508

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 07:35:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13174 boxname=wulflinc5 idbench=1014 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  26490113618ae9605b5ebe6370b5910b  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-air04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-air04.opb
IDLAUNCH: 13174
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        870212 kB
Buffers:         21204 kB
Cached:         120576 kB
SwapCached:          0 kB
Active:          32940 kB
Inactive:       111584 kB
HighTotal:      131008 kB
HighFree:        62916 kB
LowTotal:       903652 kB
LowFree:        807296 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14272 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:55:06 (client local time) WITH STATUS 0 IN 1200.5 SECONDS
stats: 13174 7 1200.5 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.91 0.99 0.92 2/54 19145
Raw data (stat): 19145 (runsolver) R 19144 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485099471 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.0008 s]
Raw data (loadavg): 0.92 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 11062 0 0 0 968 30 0 0 25 0 1 0 485099471 54525952 10704 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13312 10704 603 41 0 13271 0
vsize: 53248
[startup+20.0006 s]
Raw data (loadavg): 0.93 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 11306 0 0 0 1967 30 0 0 25 0 1 0 485099471 55472128 10948 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13543 10948 603 41 0 13502 0
vsize: 54172
[startup+30.0014 s]
Raw data (loadavg): 0.94 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 11694 0 0 0 2965 32 0 0 25 0 1 0 485099471 57085952 11336 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13937 11336 603 41 0 13896 0
vsize: 55748
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 12339 0 0 0 3963 34 0 0 25 0 1 0 485099471 59641856 11981 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14561 11981 603 41 0 14520 0
vsize: 58244
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 12745 0 0 0 4961 36 0 0 25 0 1 0 485099471 61390848 12387 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 12387 603 41 0 14947 0
vsize: 59952
[startup+60.0016 s]
Raw data (loadavg): 0.96 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 13030 0 0 0 5961 37 0 0 25 0 1 0 485099471 62472192 12672 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15252 12672 603 41 0 15211 0
vsize: 61008
[startup+70.002 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 13306 0 0 0 6960 38 0 0 25 0 1 0 485099471 63684608 12948 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15548 12948 603 41 0 15507 0
vsize: 62192
[startup+80.0021 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 13554 0 0 0 7959 39 0 0 25 0 1 0 485099471 64626688 13196 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15778 13196 603 41 0 15737 0
vsize: 63112
[startup+90.0018 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 13854 0 0 0 8958 40 0 0 25 0 1 0 485099471 65916928 13496 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16093 13496 603 41 0 16052 0
vsize: 64372
[startup+100.003 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 14213 0 0 0 9957 41 0 0 25 0 1 0 485099471 67399680 13855 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16455 13855 603 41 0 16414 0
vsize: 65820
[startup+110.003 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 14584 0 0 0 10956 43 0 0 25 0 1 0 485099471 68882432 14226 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16817 14226 603 41 0 16776 0
vsize: 67268
[startup+120.003 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 14980 0 0 0 11955 44 0 0 25 0 1 0 485099471 70496256 14622 4294967295 134512640 134672761 3221224624 3221223748 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17211 14622 603 41 0 17170 0
vsize: 68844
[startup+130.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 15225 0 0 0 12954 45 0 0 25 0 1 0 485099471 71577600 14867 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 14867 603 41 0 17434 0
vsize: 69900
[startup+140.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 15513 0 0 0 13953 46 0 0 25 0 1 0 485099471 72650752 15155 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17737 15155 603 41 0 17696 0
vsize: 70948
[startup+150.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 15866 0 0 0 14953 47 0 0 25 0 1 0 485099471 74137600 15508 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18100 15508 603 41 0 18059 0
vsize: 72400
[startup+160.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 16228 0 0 0 15952 48 0 0 25 0 1 0 485099471 75616256 15870 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18461 15870 603 41 0 18420 0
vsize: 73844
[startup+170.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 16509 0 0 0 16952 48 0 0 25 0 1 0 485099471 76697600 16151 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18725 16151 603 41 0 18684 0
vsize: 74900
[startup+180.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 16868 0 0 0 17951 49 0 0 25 0 1 0 485099471 78311424 16510 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19119 16510 603 41 0 19078 0
vsize: 76476
[startup+190.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 17174 0 0 0 18951 50 0 0 25 0 1 0 485099471 79527936 16816 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19416 16816 603 41 0 19375 0
vsize: 77664
[startup+200.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 17495 0 0 0 19950 51 0 0 25 0 1 0 485099471 80863232 17137 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19742 17137 603 41 0 19701 0
vsize: 78968
[startup+210.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 17877 0 0 0 20949 52 0 0 25 0 1 0 485099471 82472960 17519 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20135 17519 603 41 0 20094 0
vsize: 80540
[startup+220.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 18130 0 0 0 21949 52 0 0 25 0 1 0 485099471 83419136 17772 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20366 17772 603 41 0 20325 0
vsize: 81464
[startup+230.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 18341 0 0 0 22948 53 0 0 25 0 1 0 485099471 84357120 17983 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20595 17983 603 41 0 20554 0
vsize: 82380
[startup+240.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 18743 0 0 0 23947 54 0 0 25 0 1 0 485099471 85983232 18385 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20992 18385 603 41 0 20951 0
vsize: 83968
[startup+250.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 19044 0 0 0 24946 55 0 0 25 0 1 0 485099471 87195648 18686 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21288 18686 603 41 0 21247 0
vsize: 85152
[startup+260.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 19480 0 0 0 25945 57 0 0 25 0 1 0 485099471 88952832 19122 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21717 19122 603 41 0 21676 0
vsize: 86868
[startup+270.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 19856 0 0 0 26944 58 0 0 25 0 1 0 485099471 90439680 19498 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22080 19498 603 41 0 22039 0
vsize: 88320
[startup+280.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 20044 0 0 0 27943 59 0 0 25 0 1 0 485099471 91246592 19686 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22277 19686 603 41 0 22236 0
vsize: 89108
[startup+290.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 20306 0 0 0 28942 60 0 0 25 0 1 0 485099471 92327936 19948 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22541 19948 603 41 0 22500 0
vsize: 90164
[startup+300.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 20586 0 0 0 29942 60 0 0 25 0 1 0 485099471 93413376 20228 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22806 20228 603 41 0 22765 0
vsize: 91224
[startup+310.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 20960 0 0 0 30941 61 0 0 25 0 1 0 485099471 95035392 20602 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23202 20602 603 41 0 23161 0
vsize: 92808
[startup+320.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 21259 0 0 0 31941 62 0 0 25 0 1 0 485099471 96251904 20901 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23499 20901 603 41 0 23458 0
vsize: 93996
[startup+330.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 21509 0 0 0 32940 63 0 0 25 0 1 0 485099471 97189888 21151 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23728 21151 603 41 0 23687 0
vsize: 94912
[startup+340.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 21808 0 0 0 33939 64 0 0 25 0 1 0 485099471 98516992 21450 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24052 21450 603 41 0 24011 0
vsize: 96208
[startup+350.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 22052 0 0 0 34938 65 0 0 25 0 1 0 485099471 99454976 21694 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24281 21694 603 41 0 24240 0
vsize: 97124
[startup+360.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 22313 0 0 0 35935 66 0 0 25 0 1 0 485099471 100536320 21955 4294967295 134512640 134672761 3221224624 3221223780 134565028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24545 21955 603 41 0 24504 0
vsize: 98180
[startup+370.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 22903 0 0 0 36934 68 0 0 25 0 1 0 485099471 102977536 22545 4294967295 134512640 134672761 3221224624 3221223792 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25141 22545 603 41 0 25100 0
vsize: 100564
[startup+380.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 23348 0 0 0 37933 69 0 0 25 0 1 0 485099471 104742912 22990 4294967295 134512640 134672761 3221224624 3221223728 134555084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25572 22990 603 41 0 25531 0
vsize: 102288
[startup+390.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 23598 0 0 0 38933 70 0 0 25 0 1 0 485099471 105816064 23240 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25834 23240 603 41 0 25793 0
vsize: 103336
[startup+400.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 23891 0 0 0 39933 70 0 0 25 0 1 0 485099471 106901504 23533 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26099 23533 603 41 0 26058 0
vsize: 104396
[startup+410.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 24214 0 0 0 40932 71 0 0 25 0 1 0 485099471 108503040 23856 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26490 23856 603 41 0 26449 0
vsize: 105960
[startup+420.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 24581 0 0 0 41931 72 0 0 25 0 1 0 485099471 109969408 24223 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26848 24223 603 41 0 26807 0
vsize: 107392
[startup+430.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 25004 0 0 0 42930 73 0 0 25 0 1 0 485099471 111714304 24646 4294967295 134512640 134672761 3221224624 3221223760 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27274 24646 603 41 0 27233 0
vsize: 109096
[startup+440.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 25355 0 0 0 43929 74 0 0 25 0 1 0 485099471 113197056 24997 4294967295 134512640 134672761 3221224624 3221223792 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27636 24997 603 41 0 27595 0
vsize: 110544
[startup+450.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 25602 0 0 0 44929 75 0 0 25 0 1 0 485099471 114139136 25244 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27866 25244 603 41 0 27825 0
vsize: 111464
[startup+460.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 25880 0 0 0 45928 76 0 0 25 0 1 0 485099471 115372032 25522 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28167 25522 603 41 0 28126 0
vsize: 112668
[startup+470.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 26106 0 0 0 46928 76 0 0 25 0 1 0 485099471 116178944 25748 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28364 25748 603 41 0 28323 0
vsize: 113456
[startup+480.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 26422 0 0 0 47927 77 0 0 25 0 1 0 485099471 117522432 26064 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28692 26064 603 41 0 28651 0
vsize: 114768
[startup+490.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 26759 0 0 0 48926 78 0 0 25 0 1 0 485099471 118853632 26401 4294967295 134512640 134672761 3221224624 3221223728 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29017 26401 603 41 0 28976 0
vsize: 116068
[startup+500.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 27023 0 0 0 49925 79 0 0 25 0 1 0 485099471 119930880 26665 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29280 26665 603 41 0 29239 0
vsize: 117120
[startup+510.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 27282 0 0 0 50925 80 0 0 25 0 1 0 485099471 120995840 26924 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29540 26924 603 41 0 29499 0
vsize: 118160
[startup+520.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 27648 0 0 0 51924 81 0 0 25 0 1 0 485099471 122482688 27290 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29903 27290 603 41 0 29862 0
vsize: 119612
[startup+530.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 27920 0 0 0 52924 82 0 0 25 0 1 0 485099471 123703296 27562 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30201 27562 603 41 0 30160 0
vsize: 120804
[startup+540.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 28253 0 0 0 53923 83 0 0 25 0 1 0 485099471 125034496 27895 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 27895 603 41 0 30485 0
vsize: 122104
[startup+550.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 28469 0 0 0 54923 83 0 0 25 0 1 0 485099471 125845504 28111 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30724 28111 603 41 0 30683 0
vsize: 122896
[startup+560.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 28766 0 0 0 55922 84 0 0 25 0 1 0 485099471 127037440 28408 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31015 28408 603 41 0 30974 0
vsize: 124060
[startup+570.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 29065 0 0 0 56922 84 0 0 25 0 1 0 485099471 128253952 28707 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31312 28707 603 41 0 31271 0
vsize: 125248
[startup+580.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 29344 0 0 0 57921 85 0 0 25 0 1 0 485099471 129466368 28986 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31608 28986 603 41 0 31567 0
vsize: 126432
[startup+590.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 29644 0 0 0 58919 87 0 0 25 0 1 0 485099471 130682880 29286 4294967295 134512640 134672761 3221224624 3221223792 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31905 29286 603 41 0 31864 0
vsize: 127620
[startup+600.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 29972 0 0 0 59919 87 0 0 25 0 1 0 485099471 132018176 29614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32231 29614 603 41 0 32190 0
vsize: 128924
[startup+610.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 30294 0 0 0 60919 88 0 0 25 0 1 0 485099471 133361664 29936 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32559 29936 603 41 0 32518 0
vsize: 130236
[startup+620.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 30685 0 0 0 61918 89 0 0 25 0 1 0 485099471 134967296 30327 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32951 30327 603 41 0 32910 0
vsize: 131804
[startup+630.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 31021 0 0 0 62917 90 0 0 25 0 1 0 485099471 136331264 30663 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33284 30663 603 41 0 33243 0
vsize: 133136
[startup+640.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 31343 0 0 0 63916 91 0 0 25 0 1 0 485099471 137674752 30985 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33612 30985 603 41 0 33571 0
vsize: 134448
[startup+650.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 31752 0 0 0 64916 92 0 0 25 0 1 0 485099471 139272192 31394 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34002 31394 603 41 0 33961 0
vsize: 136008
[startup+660.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 31955 0 0 0 65915 92 0 0 25 0 1 0 485099471 140075008 31597 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34198 31597 603 41 0 34157 0
vsize: 136792
[startup+670.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 32236 0 0 0 66915 93 0 0 25 0 1 0 485099471 141283328 31878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34493 31878 603 41 0 34452 0
vsize: 137972
[startup+680.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 32594 0 0 0 67914 94 0 0 25 0 1 0 485099471 142757888 32236 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34853 32236 603 41 0 34812 0
vsize: 139412
[startup+690.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 32859 0 0 0 68914 94 0 0 25 0 1 0 485099471 143835136 32501 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35116 32501 603 41 0 35075 0
vsize: 140464
[startup+700.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 33068 0 0 0 69914 95 0 0 25 0 1 0 485099471 144637952 32710 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35312 32710 603 41 0 35271 0
vsize: 141248
[startup+710.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 33330 0 0 0 70914 95 0 0 25 0 1 0 485099471 145707008 32972 4294967295 134512640 134672761 3221224624 3221223728 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35573 32972 603 41 0 35532 0
vsize: 142292
[startup+720.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 33647 0 0 0 71913 96 0 0 25 0 1 0 485099471 147058688 33289 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35903 33289 603 41 0 35862 0
vsize: 143612
[startup+730.035 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 33943 0 0 0 72914 97 0 0 25 0 1 0 485099471 148250624 33585 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36194 33585 603 41 0 36153 0
vsize: 144776
[startup+740.035 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 34251 0 0 0 73913 98 0 0 25 0 1 0 485099471 149467136 33893 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36491 33893 603 41 0 36450 0
vsize: 145964
[startup+750.038 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 34539 0 0 0 74913 99 0 0 25 0 1 0 485099471 150675456 34181 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36786 34181 603 41 0 36745 0
vsize: 147144
[startup+760.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 34855 0 0 0 75912 100 0 0 25 0 1 0 485099471 152010752 34497 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37112 34497 603 41 0 37071 0
vsize: 148448
[startup+770.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 35193 0 0 0 76911 101 0 0 25 0 1 0 485099471 153350144 34835 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37439 34835 603 41 0 37398 0
vsize: 149756
[startup+780.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 35422 0 0 0 77910 102 0 0 25 0 1 0 485099471 154292224 35064 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37669 35064 603 41 0 37628 0
vsize: 150676
[startup+790.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 35778 0 0 0 78909 103 0 0 25 0 1 0 485099471 155774976 35420 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38031 35420 603 41 0 37990 0
vsize: 152124
[startup+800.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 36131 0 0 0 79908 104 0 0 25 0 1 0 485099471 157241344 35773 4294967295 134512640 134672761 3221224624 3221223728 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38389 35773 603 41 0 38348 0
vsize: 153556
[startup+810.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 36384 0 0 0 80908 105 0 0 25 0 1 0 485099471 158179328 36026 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38618 36026 603 41 0 38577 0
vsize: 154472
[startup+820.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 36662 0 0 0 81907 105 0 0 25 0 1 0 485099471 159391744 36304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38914 36304 603 41 0 38873 0
vsize: 155656
[startup+830.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 36926 0 0 0 82907 106 0 0 25 0 1 0 485099471 160477184 36568 4294967295 134512640 134672761 3221224624 3221223728 134559946 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39179 36568 603 41 0 39138 0
vsize: 156716
[startup+840.04 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 37344 0 0 0 83907 106 0 0 25 0 1 0 485099471 162205696 36986 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39601 36986 603 41 0 39560 0
vsize: 158404
[startup+850.054 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 37773 0 0 0 84907 108 0 0 25 0 1 0 485099471 163946496 37415 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40026 37415 603 41 0 39985 0
vsize: 160104
[startup+860.157 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 38158 0 0 0 85916 109 0 0 25 0 1 0 485099471 165437440 37800 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40390 37800 603 41 0 40349 0
vsize: 161560
[startup+870.157 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 38466 0 0 0 86916 109 0 0 25 0 1 0 485099471 166785024 38108 4294967295 134512640 134672761 3221224624 3221223824 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40719 38108 603 41 0 40678 0
vsize: 162876
[startup+880.164 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 38766 0 0 0 87916 111 0 0 25 0 1 0 485099471 167997440 38408 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41015 38408 603 41 0 40974 0
vsize: 164060
[startup+890.164 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 39084 0 0 0 88915 112 0 0 25 0 1 0 485099471 169213952 38726 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41312 38726 603 41 0 41271 0
vsize: 165248
[startup+900.172 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 39338 0 0 0 89915 112 0 0 25 0 1 0 485099471 170295296 38980 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41576 38980 603 41 0 41535 0
vsize: 166304
[startup+910.181 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 39716 0 0 0 90914 114 0 0 25 0 1 0 485099471 171905024 39358 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41969 39358 603 41 0 41928 0
vsize: 167876
[startup+920.18 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 40118 0 0 0 91914 115 0 0 25 0 1 0 485099471 173514752 39760 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42362 39760 603 41 0 42321 0
vsize: 169448
[startup+930.194 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 40531 0 0 0 92914 116 0 0 25 0 1 0 485099471 175153152 40173 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42762 40173 603 41 0 42721 0
vsize: 171048
[startup+940.194 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 40917 0 0 0 93913 117 0 0 25 0 1 0 485099471 176746496 40559 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43151 40559 603 41 0 43110 0
vsize: 172604
[startup+950.194 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 41360 0 0 0 94912 118 0 0 25 0 1 0 485099471 178511872 41002 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43582 41002 603 41 0 43541 0
vsize: 174328
[startup+960.194 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 41759 0 0 0 95912 119 0 0 25 0 1 0 485099471 180248576 41401 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44006 41401 603 41 0 43965 0
vsize: 176024
[startup+970.194 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 42161 0 0 0 96911 120 0 0 25 0 1 0 485099471 181837824 41803 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44394 41803 603 41 0 44353 0
vsize: 177576
[startup+980.195 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 42458 0 0 0 97910 121 0 0 25 0 1 0 485099471 183050240 42100 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44690 42100 603 41 0 44649 0
vsize: 178760
[startup+990.194 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 42693 0 0 0 98910 122 0 0 25 0 1 0 485099471 183975936 42335 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44916 42335 603 41 0 44875 0
vsize: 179664
[startup+1000.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 43008 0 0 0 99909 122 0 0 25 0 1 0 485099471 185327616 42650 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45246 42650 603 41 0 45205 0
vsize: 180984
[startup+1010.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 43331 0 0 0 100909 122 0 0 25 0 1 0 485099471 186675200 42973 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45575 42973 603 41 0 45534 0
vsize: 182300
[startup+1020.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 43681 0 0 0 101909 123 0 0 25 0 1 0 485099471 188026880 43323 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45905 43323 603 41 0 45864 0
vsize: 183620
[startup+1030.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 44021 0 0 0 102908 124 0 0 25 0 1 0 485099471 189497344 43663 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46264 43665 603 41 0 46223 0
vsize: 185056
[startup+1040.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 44416 0 0 0 103907 125 0 0 25 0 1 0 485099471 191107072 44058 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46657 44058 603 41 0 46616 0
vsize: 186628
[startup+1050.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 44671 0 0 0 104906 126 0 0 25 0 1 0 485099471 192585728 44313 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47018 44313 603 41 0 46977 0
vsize: 188072
[startup+1060.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 44961 0 0 0 105904 127 0 0 25 0 1 0 485099471 193785856 44603 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47311 44603 603 41 0 47270 0
vsize: 189244
[startup+1070.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 45226 0 0 0 106904 128 0 0 25 0 1 0 485099471 194850816 44868 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47571 44868 603 41 0 47530 0
vsize: 190284
[startup+1080.2 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 45512 0 0 0 107904 129 0 0 25 0 1 0 485099471 196067328 45154 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47868 45154 603 41 0 47827 0
vsize: 191472
[startup+1090.24 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 45786 0 0 0 108907 129 0 0 25 0 1 0 485099471 197148672 45428 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48132 45428 603 41 0 48091 0
vsize: 192528
[startup+1100.24 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 46125 0 0 0 109906 130 0 0 25 0 1 0 485099471 198615040 45767 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48490 45767 603 41 0 48449 0
vsize: 193960
[startup+1110.24 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 46476 0 0 0 110906 131 0 0 25 0 1 0 485099471 199958528 46118 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48818 46119 603 41 0 48777 0
vsize: 195272
[startup+1120.24 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 46802 0 0 0 111905 132 0 0 25 0 1 0 485099471 201306112 46444 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49147 46444 603 41 0 49106 0
vsize: 196588
[startup+1130.24 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 47078 0 0 0 112904 134 0 0 25 0 1 0 485099471 202514432 46720 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49442 46720 603 41 0 49401 0
vsize: 197768
[startup+1140.25 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 47301 0 0 0 113903 134 0 0 25 0 1 0 485099471 203313152 46943 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49637 46943 603 41 0 49596 0
vsize: 198548
[startup+1150.25 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 47563 0 0 0 114903 135 0 0 25 0 1 0 485099471 204382208 47205 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49898 47205 603 41 0 49857 0
vsize: 199592
[startup+1160.25 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 47892 0 0 0 115903 136 0 0 25 0 1 0 485099471 205737984 47534 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50229 47534 603 41 0 50188 0
vsize: 200916
[startup+1170.25 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 48253 0 0 0 116902 137 0 0 25 0 1 0 485099471 207204352 47895 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50587 47895 603 41 0 50546 0
vsize: 202348
[startup+1180.25 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 48567 0 0 0 117901 138 0 0 25 0 1 0 485099471 208539648 48209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50913 48209 603 41 0 50872 0
vsize: 203652
[startup+1190.25 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 48845 0 0 0 118900 139 0 0 25 0 1 0 485099471 209616896 48487 4294967295 134512640 134672761 3221224624 3221223728 134559943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51176 48487 603 41 0 51135 0
vsize: 204704
[startup+1200.25 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 19145
Raw data (stat): 19145 (minisat+) R 19144 24215 24214 0 -1 0 49150 0 0 0 119899 140 0 0 25 0 1 0 485099471 210968576 48792 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51506 48792 603 41 0 51465 0
vsize: 206024
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 1.01 1.00 0.93 1/54 19145
Raw data (stat): 19145 (minisat+) Z 19144 24215 24214 0 -1 12 49152 0 0 0 119900 149 0 0 25 0 1 0 485099471 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.35
CPU time (s): 1200.5
CPU user time (s): 1199
CPU system time (s): 1.49477
CPU usage (%): 100.012
Max. virtual memory (Kb): 206024
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####