PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        870416 kB
Buffers:         24868 kB
Cached:         112948 kB
SwapCached:       4304 kB
Active:          40456 kB
Inactive:       103148 kB
HighTotal:      131008 kB
HighFree:        20664 kB
LowTotal:       903652 kB
LowFree:        849752 kB
SwapTotal:     2097892 kB
SwapFree:      2092680 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15056 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 19:27:11 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 16652 7 1200.29 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.87 0.94 0.91 2/54 4521
Raw data (stat): 4521 (runsolver) R 4520 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547470671 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 11066 0 0 0 967 31 0 0 25 0 1 0 547470671 54525952 10708 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13312 10708 603 41 0 13271 0
vsize: 53248
[startup+20.0004 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 11316 0 0 0 1966 33 0 0 25 0 1 0 547470671 55472128 10958 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13543 10958 603 41 0 13502 0
vsize: 54172
[startup+30.0006 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 11729 0 0 0 2964 34 0 0 25 0 1 0 547470671 57221120 11371 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13970 11371 603 41 0 13929 0
vsize: 55880
[startup+40.0014 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 12381 0 0 0 3963 35 0 0 25 0 1 0 547470671 59912192 12023 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14627 12023 603 41 0 14586 0
vsize: 58508
[startup+50.0017 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 12765 0 0 0 4962 37 0 0 25 0 1 0 547470671 61390848 12407 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 12407 603 41 0 14947 0
vsize: 59952
[startup+60.0022 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 13045 0 0 0 5961 38 0 0 25 0 1 0 547470671 62607360 12687 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15285 12687 603 41 0 15244 0
vsize: 61140
[startup+70.0027 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 13342 0 0 0 6960 39 0 0 25 0 1 0 547470671 63815680 12984 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15580 12984 603 41 0 15539 0
vsize: 62320
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 13577 0 0 0 7959 40 0 0 25 0 1 0 547470671 64761856 13219 4294967295 134512640 134672761 3221224544 3221223648 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15811 13219 603 41 0 15770 0
vsize: 63244
[startup+90.0043 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 13948 0 0 0 8958 41 0 0 25 0 1 0 547470671 66322432 13590 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16192 13590 603 41 0 16151 0
vsize: 64768
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 14241 0 0 0 9957 42 0 0 25 0 1 0 547470671 67534848 13883 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16488 13883 603 41 0 16447 0
vsize: 65952
[startup+110.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 14663 0 0 0 10955 44 0 0 25 0 1 0 547470671 69287936 14305 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16916 14305 603 41 0 16875 0
vsize: 67664
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 15002 0 0 0 11954 45 0 0 25 0 1 0 547470671 70631424 14644 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17244 14644 603 41 0 17203 0
vsize: 68976
[startup+130.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 15290 0 0 0 12953 47 0 0 25 0 1 0 547470671 71843840 14932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17540 14932 603 41 0 17499 0
vsize: 70160
[startup+140.016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 15576 0 0 0 13952 48 0 0 25 0 1 0 547470671 72921088 15218 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17803 15218 603 41 0 17762 0
vsize: 71212
[startup+150.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 15991 0 0 0 14951 49 0 0 25 0 1 0 547470671 74678272 15633 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18232 15633 603 41 0 18191 0
vsize: 72928
[startup+160.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 16295 0 0 0 15950 50 0 0 25 0 1 0 547470671 75886592 15937 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18527 15937 603 41 0 18486 0
vsize: 74108
[startup+170.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 16620 0 0 0 16948 52 0 0 25 0 1 0 547470671 77238272 16262 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18857 16262 603 41 0 18816 0
vsize: 75428
[startup+180.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 16901 0 0 0 17947 53 0 0 25 0 1 0 547470671 78446592 16543 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19152 16543 603 41 0 19111 0
vsize: 76608
[startup+190.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 17255 0 0 0 18946 54 0 0 25 0 1 0 547470671 79929344 16897 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19514 16897 603 41 0 19473 0
vsize: 78056
[startup+200.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 17623 0 0 0 19945 55 0 0 25 0 1 0 547470671 81399808 17265 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19873 17265 603 41 0 19832 0
vsize: 79492
[startup+210.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 17980 0 0 0 20944 57 0 0 25 0 1 0 547470671 82878464 17622 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20234 17622 603 41 0 20193 0
vsize: 80936
[startup+220.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 18201 0 0 0 21942 59 0 0 25 0 1 0 547470671 83824640 17843 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20465 17843 603 41 0 20424 0
vsize: 81860
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 18429 0 0 0 22942 59 0 0 25 0 1 0 547470671 84631552 18071 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20662 18071 603 41 0 20621 0
vsize: 82648
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 18846 0 0 0 23940 61 0 0 25 0 1 0 547470671 86384640 18488 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21090 18488 603 41 0 21049 0
vsize: 84360
[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 19201 0 0 0 24940 62 0 0 25 0 1 0 547470671 87879680 18843 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21455 18843 603 41 0 21414 0
vsize: 85820
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 19646 0 0 0 25938 63 0 0 25 0 1 0 547470671 89628672 19288 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21882 19288 603 41 0 21841 0
vsize: 87528
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 19937 0 0 0 26938 64 0 0 25 0 1 0 547470671 90841088 19579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22178 19579 603 41 0 22137 0
vsize: 88712
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 20103 0 0 0 27937 64 0 0 25 0 1 0 547470671 91516928 19745 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22343 19745 603 41 0 22302 0
vsize: 89372
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 20398 0 0 0 28936 66 0 0 25 0 1 0 547470671 92741632 20040 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22642 20040 603 41 0 22601 0
vsize: 90568
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 20709 0 0 0 29935 67 0 0 25 0 1 0 547470671 93954048 20351 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22938 20351 603 41 0 22897 0
vsize: 91752
[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 21091 0 0 0 30934 68 0 0 25 0 1 0 547470671 95576064 20733 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23334 20733 603 41 0 23293 0
vsize: 93336
[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 21359 0 0 0 31933 69 0 0 25 0 1 0 547470671 96657408 21001 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23598 21001 603 41 0 23557 0
vsize: 94392
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 21608 0 0 0 32932 70 0 0 25 0 1 0 547470671 97587200 21250 4294967295 134512640 134672761 3221224544 3221223544 1075349836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23825 21250 603 41 0 23784 0
vsize: 95300
[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 21922 0 0 0 33931 71 0 0 25 0 1 0 547470671 98914304 21564 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24149 21564 603 41 0 24108 0
vsize: 96596
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 22190 0 0 0 34930 72 0 0 25 0 1 0 547470671 99995648 21832 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24413 21832 603 41 0 24372 0
vsize: 97652
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 22563 0 0 0 35929 73 0 0 25 0 1 0 547470671 101486592 22205 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24777 22205 603 41 0 24736 0
vsize: 99108
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 23217 0 0 0 36927 75 0 0 25 0 1 0 547470671 104202240 22859 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25440 22859 603 41 0 25399 0
vsize: 101760
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 23479 0 0 0 37926 77 0 0 25 0 1 0 547470671 105275392 23121 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25702 23121 603 41 0 25661 0
vsize: 102808
[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 23706 0 0 0 38926 77 0 0 25 0 1 0 547470671 106221568 23348 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25933 23348 603 41 0 25892 0
vsize: 103732
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 24049 0 0 0 39925 77 0 0 25 0 1 0 547470671 107569152 23691 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26262 23691 603 41 0 26221 0
vsize: 105048
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 24374 0 0 0 40924 79 0 0 25 0 1 0 547470671 109158400 24016 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26650 24016 603 41 0 26609 0
vsize: 106600
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 24829 0 0 0 41923 80 0 0 25 0 1 0 547470671 111046656 24471 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27111 24471 603 41 0 27070 0
vsize: 108444
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 25165 0 0 0 42923 80 0 0 25 0 1 0 547470671 112381952 24807 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27437 24807 603 41 0 27396 0
vsize: 109748
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 25471 0 0 0 43922 81 0 0 25 0 1 0 547470671 113598464 25113 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27734 25113 603 41 0 27693 0
vsize: 110936
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 25784 0 0 0 44921 83 0 0 25 0 1 0 547470671 114970624 25426 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28069 25426 603 41 0 28028 0
vsize: 112276
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 25994 0 0 0 45921 83 0 0 25 0 1 0 547470671 115773440 25636 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28265 25636 603 41 0 28224 0
vsize: 113060
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 26242 0 0 0 46920 84 0 0 25 0 1 0 547470671 116850688 25884 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28528 25884 603 41 0 28487 0
vsize: 114112
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 26558 0 0 0 47919 85 0 0 25 0 1 0 547470671 118050816 26200 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28821 26200 603 41 0 28780 0
vsize: 115284
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 26869 0 0 0 48919 85 0 0 25 0 1 0 547470671 119394304 26511 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29149 26511 603 41 0 29108 0
vsize: 116596
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 27125 0 0 0 49919 86 0 0 25 0 1 0 547470671 120336384 26767 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29379 26767 603 41 0 29338 0
vsize: 117516
[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 27452 0 0 0 50918 87 0 0 25 0 1 0 547470671 121671680 27094 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29705 27094 603 41 0 29664 0
vsize: 118820
[startup+520.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 27800 0 0 0 51917 88 0 0 25 0 1 0 547470671 123162624 27442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30069 27442 603 41 0 30028 0
vsize: 120276
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 28074 0 0 0 52917 89 0 0 25 0 1 0 547470671 124227584 27716 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30329 27716 603 41 0 30288 0
vsize: 121316
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 28418 0 0 0 53916 90 0 0 25 0 1 0 547470671 125714432 28060 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30692 28060 603 41 0 30651 0
vsize: 122768
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 28647 0 0 0 54915 90 0 0 25 0 1 0 547470671 126636032 28289 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 28289 603 41 0 30876 0
vsize: 123668
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 28932 0 0 0 55915 91 0 0 25 0 1 0 547470671 127713280 28574 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31180 28574 603 41 0 31139 0
vsize: 124720
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 29188 0 0 0 56914 92 0 0 25 0 1 0 547470671 128798720 28830 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31445 28830 603 41 0 31404 0
vsize: 125780
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 29454 0 0 0 57914 92 0 0 25 0 1 0 547470671 129871872 29096 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31707 29096 603 41 0 31666 0
vsize: 126828
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 29817 0 0 0 58912 93 0 0 25 0 1 0 547470671 131342336 29459 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32066 29459 603 41 0 32025 0
vsize: 128264
[startup+600.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 30088 0 0 0 59913 94 0 0 25 0 1 0 547470671 132423680 29730 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32330 29730 603 41 0 32289 0
vsize: 129320
[startup+610.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 30494 0 0 0 60911 96 0 0 25 0 1 0 547470671 134168576 30136 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32756 30136 603 41 0 32715 0
vsize: 131024
[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 30833 0 0 0 61911 96 0 0 25 0 1 0 547470671 135507968 30475 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33083 30475 603 41 0 33042 0
vsize: 132332
[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 31166 0 0 0 62910 97 0 0 25 0 1 0 547470671 136867840 30808 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33415 30808 603 41 0 33374 0
vsize: 133660
[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 31529 0 0 0 63909 98 0 0 25 0 1 0 547470671 138338304 31171 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33774 31171 603 41 0 33733 0
vsize: 135096
[startup+650.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 31854 0 0 0 64909 99 0 0 25 0 1 0 547470671 139677696 31496 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34101 31496 603 41 0 34060 0
vsize: 136404
[startup+660.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 32072 0 0 0 65908 100 0 0 25 0 1 0 547470671 140611584 31714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34329 31714 603 41 0 34288 0
vsize: 137316
[startup+670.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 32382 0 0 0 66908 100 0 0 25 0 1 0 547470671 141819904 32024 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34624 32024 603 41 0 34583 0
vsize: 138496
[startup+680.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 32713 0 0 0 67907 101 0 0 25 0 1 0 547470671 143294464 32355 4294967295 134512640 134672761 3221224544 3221223700 134565028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34984 32355 603 41 0 34943 0
vsize: 139936
[startup+690.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 32977 0 0 0 68907 102 0 0 25 0 1 0 547470671 144367616 32619 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35246 32619 603 41 0 35205 0
vsize: 140984
[startup+700.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 33189 0 0 0 69906 102 0 0 25 0 1 0 547470671 145174528 32831 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35443 32831 603 41 0 35402 0
vsize: 141772
[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 33456 0 0 0 70906 103 0 0 25 0 1 0 547470671 146247680 33098 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35705 33098 603 41 0 35664 0
vsize: 142820
[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 33747 0 0 0 71905 104 0 0 25 0 1 0 547470671 147460096 33389 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36001 33389 603 41 0 35960 0
vsize: 144004
[startup+730.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 34060 0 0 0 72904 105 0 0 25 0 1 0 547470671 148791296 33702 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36326 33702 603 41 0 36285 0
vsize: 145304
[startup+740.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 34371 0 0 0 73904 106 0 0 25 0 1 0 547470671 150007808 34013 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36623 34013 603 41 0 36582 0
vsize: 146492
[startup+750.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 34654 0 0 0 74903 107 0 0 25 0 1 0 547470671 151199744 34296 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36914 34296 603 41 0 36873 0
vsize: 147656
[startup+760.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 35017 0 0 0 75902 107 0 0 25 0 1 0 547470671 152678400 34659 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37275 34659 603 41 0 37234 0
vsize: 149100
[startup+770.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 35288 0 0 0 76901 109 0 0 25 0 1 0 547470671 153751552 34930 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37537 34930 603 41 0 37496 0
vsize: 150148
[startup+780.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 35556 0 0 0 77901 109 0 0 25 0 1 0 547470671 154828800 35198 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37800 35198 603 41 0 37759 0
vsize: 151200
[startup+790.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 35947 0 0 0 78900 111 0 0 25 0 1 0 547470671 156438528 35589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38193 35589 603 41 0 38152 0
vsize: 152772
[startup+800.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 36198 0 0 0 79899 112 0 0 25 0 1 0 547470671 157511680 35840 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38455 35840 603 41 0 38414 0
vsize: 153820
[startup+810.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 36486 0 0 0 80898 113 0 0 25 0 1 0 547470671 158584832 36128 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38717 36128 603 41 0 38676 0
vsize: 154868
[startup+820.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 36759 0 0 0 81897 114 0 0 25 0 1 0 547470671 159793152 36401 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39012 36401 603 41 0 38971 0
vsize: 156048
[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 37046 0 0 0 82896 115 0 0 25 0 1 0 547470671 161001472 36688 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39307 36688 603 41 0 39266 0
vsize: 157228
[startup+840.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 37519 0 0 0 83895 116 0 0 25 0 1 0 547470671 162881536 37161 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39766 37161 603 41 0 39725 0
vsize: 159064
[startup+850.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 37921 0 0 0 84894 117 0 0 25 0 1 0 547470671 164487168 37563 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40158 37563 603 41 0 40117 0
vsize: 160632
[startup+860.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 38304 0 0 0 85894 118 0 0 25 0 1 0 547470671 166105088 37946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40553 37946 603 41 0 40512 0
vsize: 162212
[startup+870.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 38588 0 0 0 86893 119 0 0 25 0 1 0 547470671 167186432 38230 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40817 38230 603 41 0 40776 0
vsize: 163268
[startup+880.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 38846 0 0 0 87893 119 0 0 25 0 1 0 547470671 168267776 38488 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41081 38488 603 41 0 41040 0
vsize: 164324
[startup+890.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 39143 0 0 0 88892 120 0 0 25 0 1 0 547470671 169484288 38785 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41378 38785 603 41 0 41337 0
vsize: 165512
[startup+900.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 39438 0 0 0 89892 121 0 0 25 0 1 0 547470671 170700800 39080 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41675 39080 603 41 0 41634 0
vsize: 166700
[startup+910.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 39835 0 0 0 90890 123 0 0 25 0 1 0 547470671 172306432 39477 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42067 39477 603 41 0 42026 0
vsize: 168268
[startup+920.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 40252 0 0 0 91889 124 0 0 25 0 1 0 547470671 174063616 39894 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42496 39894 603 41 0 42455 0
vsize: 169984
[startup+930.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 40668 0 0 0 92888 125 0 0 25 0 1 0 547470671 175677440 40310 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42890 40310 603 41 0 42849 0
vsize: 171560
[startup+940.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 41039 0 0 0 93888 126 0 0 25 0 1 0 547470671 177295360 40681 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43285 40681 603 41 0 43244 0
vsize: 173140
[startup+950.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 41490 0 0 0 94886 128 0 0 25 0 1 0 547470671 179052544 41132 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43714 41132 603 41 0 43673 0
vsize: 174856
[startup+960.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 41886 0 0 0 95885 129 0 0 25 0 1 0 547470671 180764672 41528 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44132 41528 603 41 0 44091 0
vsize: 176528
[startup+970.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 42284 0 0 0 96885 129 0 0 25 0 1 0 547470671 182378496 41926 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44526 41926 603 41 0 44485 0
vsize: 178104
[startup+980.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 42559 0 0 0 97884 130 0 0 25 0 1 0 547470671 183447552 42201 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44787 42201 603 41 0 44746 0
vsize: 179148
[startup+990.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 42773 0 0 0 98884 131 0 0 25 0 1 0 547470671 184381440 42415 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45015 42415 603 41 0 44974 0
vsize: 180060
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 43096 0 0 0 99883 131 0 0 25 0 1 0 547470671 185593856 42738 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45311 42738 603 41 0 45270 0
vsize: 181244
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 43419 0 0 0 100883 132 0 0 25 0 1 0 547470671 186949632 43061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45642 43061 603 41 0 45601 0
vsize: 182568
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 43779 0 0 0 101882 133 0 0 25 0 1 0 547470671 188444672 43421 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46007 43421 603 41 0 45966 0
vsize: 184028
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 44127 0 0 0 102881 134 0 0 25 0 1 0 547470671 189902848 43769 4294967295 134512640 134672761 3221224544 3221223648 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46363 43769 603 41 0 46322 0
vsize: 185452
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 44483 0 0 0 103880 135 0 0 25 0 1 0 547470671 191377408 44125 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46723 44125 603 41 0 46682 0
vsize: 186892
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 44751 0 0 0 104879 136 0 0 25 0 1 0 547470671 192987136 44393 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47116 44393 603 41 0 47075 0
vsize: 188464
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 45047 0 0 0 105879 137 0 0 25 0 1 0 547470671 194187264 44689 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47409 44689 603 41 0 47368 0
vsize: 189636
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 45306 0 0 0 106879 137 0 0 25 0 1 0 547470671 195256320 44948 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47670 44948 603 41 0 47629 0
vsize: 190680
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 45547 0 0 0 107878 138 0 0 25 0 1 0 547470671 196202496 45189 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47901 45189 603 41 0 47860 0
vsize: 191604
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 45876 0 0 0 108878 138 0 0 25 0 1 0 547470671 197545984 45518 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48229 45518 603 41 0 48188 0
vsize: 192916
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 46237 0 0 0 109876 140 0 0 25 0 1 0 547470671 199020544 45879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48589 45879 603 41 0 48548 0
vsize: 194356
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 46574 0 0 0 110875 142 0 0 25 0 1 0 547470671 200364032 46216 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48917 46216 603 41 0 48876 0
vsize: 195668
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 46906 0 0 0 111874 142 0 0 25 0 1 0 547470671 201703424 46548 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49244 46548 603 41 0 49203 0
vsize: 196976
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 47135 0 0 0 112874 143 0 0 25 0 1 0 547470671 202645504 46777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49474 46777 603 41 0 49433 0
vsize: 197896
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 47351 0 0 0 113873 144 0 0 25 0 1 0 547470671 203583488 46993 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49703 46993 603 41 0 49662 0
vsize: 198812
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 47648 0 0 0 114873 145 0 0 25 0 1 0 547470671 204787712 47290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49997 47290 603 41 0 49956 0
vsize: 199988
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 47980 0 0 0 115872 146 0 0 25 0 1 0 547470671 206135296 47622 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50326 47622 603 41 0 50285 0
vsize: 201304
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 48330 0 0 0 116870 147 0 0 25 0 1 0 547470671 207597568 47972 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50683 47972 603 41 0 50642 0
vsize: 202732
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 48621 0 0 0 117870 148 0 0 25 0 1 0 547470671 208809984 48263 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50979 48263 603 41 0 50938 0
vsize: 203916
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 48906 0 0 0 118869 149 0 0 25 0 1 0 547470671 209891328 48548 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51243 48548 603 41 0 51202 0
vsize: 204972
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4521
Raw data (stat): 4521 (minisat+) R 4520 27222 27221 0 -1 0 49218 0 0 0 119868 150 0 0 25 0 1 0 547470671 211238912 48860 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51572 48860 603 41 0 51531 0
vsize: 206288
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4521
Raw data (stat): 4521 (minisat+) Z 4520 27222 27221 0 -1 12 49220 0 0 0 119868 159 0 0 25 0 1 0 547470671 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.15
CPU time (s): 1200.29
CPU user time (s): 1198.69
CPU system time (s): 1.59976
CPU usage (%): 100.011
Max. virtual memory (Kb): 206288
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####