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/miplib2003/normalized-mps-v2-13-7-air04.opb
MD5SUM	ee388359e66788d310d5d5b34d6465c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63236
Optimality of the best value was proved	NO
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	SAT
Best CPU time to get the best result obtained on this benchmark	1176.04
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 15486

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        714976 kB
Buffers:         32944 kB
Cached:         264760 kB
SwapCached:        408 kB
Active:          30676 kB
Inactive:       269152 kB
HighTotal:      131008 kB
HighFree:        30100 kB
LowTotal:       903652 kB
LowFree:        684876 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14160 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:58:43 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 17432 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   67
c ---[1640]---> BDD-cost:  303
c ---[1638]---> BDD-cost:  119
c ---[1636]---> BDD-cost:  145
c ---[1634]---> BDD-cost:  165
c ---[1632]---> BDD-cost:  239
c ---[1630]---> BDD-cost:  223
c ---[1628]---> BDD-cost:   59
c ---[1626]---> BDD-cost:   35
c ---[1624]---> BDD-cost:   93
c ---[1622]---> BDD-cost:   45
c ---[1620]---> BDD-cost:  213
c ---[1618]---> BDD-cost:   73
c ---[1616]---> BDD-cost:   75
c ---[1614]---> BDD-cost:   63
c ---[1612]---> BDD-cost:   99
c ---[1608]---> BDD-cost:  187
c ---[1606]---> BDD-cost:   55
c ---[1604]---> BDD-cost:  107
c ---[1602]---> BDD-cost:   69
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   75
c ---[1596]---> BDD-cost:    3
c ---[1594]---> BDD-cost:  149
c ---[1592]---> BDD-cost:  137
c ---[1590]---> BDD-cost:  195
c ---[1588]---> BDD-cost:   93
c ---[1586]---> BDD-cost:  157
c ---[1584]---> BDD-cost:  233
c ---[1582]---> BDD-cost:  223
c ---[1580]---> BDD-cost:  225
c ---[1578]---> BDD-cost:  247
c ---[1576]---> BDD-cost:   75
c ---[1574]---> BDD-cost:  179
c ---[1572]---> BDD-cost:  225
c ---[1570]---> BDD-cost:  243
c ---[1568]---> BDD-cost:  199
c ---[1566]---> BDD-cost:   55
c ---[1564]---> BDD-cost:   57
c ---[1562]---> BDD-cost:   99
c ---[1560]---> BDD-cost:    9
c ---[1558]---> BDD-cost:    3
c ---[1556]---> BDD-cost:   23
c ---[1554]---> BDD-cost:   55
c ---[1552]---> BDD-cost:   51
c ---[1550]---> BDD-cost:   25
c ---[1548]---> BDD-cost:   23
c ---[1546]---> BDD-cost:   27
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:   37
c ---[1540]---> BDD-cost:   67
c ---[1538]---> BDD-cost:   67
c ---[1536]---> BDD-cost:  109
c ---[1534]---> BDD-cost:  211
c ---[1532]---> BDD-cost:   15
c ---[1530]---> BDD-cost:    0
c ---[1526]---> BDD-cost:   65
c ---[1524]---> BDD-cost:  117
c ---[1522]---> BDD-cost:   65
c ---[1520]---> BDD-cost:   65
c ---[1518]---> BDD-cost:   49
c ---[1516]---> BDD-cost:  439
c ---[1514]---> BDD-cost:  423
c ---[1512]---> BDD-cost:  287
c ---[1510]---> BDD-cost:   87
c ---[1508]---> BDD-cost:  217
c ---[1506]---> BDD-cost:  195
c ---[1504]---> BDD-cost:   63
c ---[1502]---> BDD-cost:   53
c ---[1500]---> BDD-cost:  359
c ---[1498]---> BDD-cost:  353
c ---[1494]---> BDD-cost:  169
c ---[1492]---> BDD-cost:  139
c ---[1490]---> BDD-cost:  159
c ---[1488]---> BDD-cost:   51
c ---[1486]---> BDD-cost:  223
c ---[1484]---> BDD-cost:  107
c ---[1482]---> BDD-cost:   75
c ---[1480]---> BDD-cost:  109
c ---[1478]---> BDD-cost:   93
c ---[1476]---> BDD-cost:   87
c ---[1474]---> BDD-cost:   87
c ---[1472]---> BDD-cost:    7
c ---[1468]---> BDD-cost:   73
c ---[1466]---> BDD-cost:    1
c ---[1464]---> BDD-cost:   71
c ---[1462]---> BDD-cost:  107
c ---[1460]---> BDD-cost:   77
c ---[1458]---> BDD-cost:    3
c ---[1456]---> BDD-cost:  107
c ---[1454]---> BDD-cost:  131
c ---[1452]---> BDD-cost:  135
c ---[1450]---> BDD-cost:   65
c ---[1448]---> BDD-cost:  165
c ---[1446]---> BDD-cost:  123
c ---[1444]---> BDD-cost:    1
c ---[1442]---> BDD-cost:    1
c ---[1440]---> BDD-cost:   87
c ---[1438]---> BDD-cost:  155
c ---[1436]---> BDD-cost:  167
c ---[1434]---> BDD-cost:  203
c ---[1432]---> BDD-cost:  231
c ---[1430]---> BDD-cost:  147
c ---[1428]---> BDD-cost:  135
c ---[1426]---> BDD-cost:   49
c ---[1424]---> BDD-cost:   31
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   23
c ---[1418]---> BDD-cost:   95
c ---[1416]---> BDD-cost:  325
c ---[1414]---> BDD-cost:  333
c ---[1412]---> BDD-cost:  173
c ---[1410]---> BDD-cost:  269
c ---[1408]---> BDD-cost:   31
c ---[1406]---> BDD-cost:  413
c ---[1404]---> BDD-cost:  313
c ---[1402]---> BDD-cost:  125
c ---[1400]---> BDD-cost:  113
c ---[1398]---> BDD-cost:   11
c ---[1396]---> BDD-cost:  247
c ---[1394]---> BDD-cost:   57
c ---[1392]---> BDD-cost:  237
c ---[1390]---> BDD-cost:  159
c ---[1388]---> BDD-cost:  117
c ---[1386]---> BDD-cost:   43
c ---[1384]---> BDD-cost:  143
c ---[1382]---> BDD-cost:   65
c ---[1380]---> BDD-cost:  123
c ---[1378]---> BDD-cost:   61
c ---[1376]---> BDD-cost:   39
c ---[1374]---> BDD-cost:  103
c ---[1372]---> BDD-cost:   85
c ---[1370]---> BDD-cost:   77
c ---[1368]---> BDD-cost:   57
c ---[1366]---> BDD-cost:  127
c ---[1364]---> BDD-cost:  157
c ---[1362]---> BDD-cost:  267
c ---[1360]---> BDD-cost:  223
c ---[1358]---> BDD-cost:  229
c ---[1356]---> BDD-cost:  257
c ---[1354]---> BDD-cost:   13
c ---[1352]---> BDD-cost:  241
c ---[1350]---> BDD-cost:  195
c ---[1348]---> BDD-cost:   49
c ---[1346]---> BDD-cost:  117
c ---[1344]---> BDD-cost:  197
c ---[1342]---> BDD-cost:  171
c ---[1340]---> BDD-cost:  287
c ---[1338]---> BDD-cost:   75
c ---[1336]---> BDD-cost:  215
c ---[1334]---> BDD-cost:  119
c ---[1332]---> BDD-cost:   57
c ---[1330]---> BDD-cost:  245
c ---[1328]---> BDD-cost:  257
c ---[1326]---> BDD-cost:  279
c ---[1324]---> BDD-cost:  227
c ---[1322]---> BDD-cost:  201
c ---[1320]---> BDD-cost:  143
c ---[1318]---> BDD-cost:  207
c ---[1316]---> BDD-cost:  131
c ---[1314]---> BDD-cost:  245
c ---[1312]---> BDD-cost:  115
c ---[1310]---> BDD-cost:  259
c ---[1308]---> BDD-cost:   91
c ---[1306]---> BDD-cost:   43
c ---[1304]---> BDD-cost:   39
c ---[1302]---> BDD-cost:   91
c ---[1300]---> BDD-cost:  179
c ---[1298]---> BDD-cost:   73
c ---[1296]---> BDD-cost:   29
c ---[1294]---> BDD-cost:  163
c ---[1292]---> BDD-cost:   81
c ---[1290]---> BDD-cost:   63
c ---[1288]---> BDD-cost:  189
c ---[1286]---> BDD-cost:  103
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  115
c ---[1280]---> BDD-cost:   19
c ---[1278]---> BDD-cost:   93
c ---[1276]---> BDD-cost:   99
c ---[1274]---> BDD-cost:   99
c ---[1272]---> BDD-cost:  103
c ---[1270]---> BDD-cost:   67
c ---[1268]---> BDD-cost:   23
c ---[1266]---> BDD-cost:  101
c ---[1264]---> BDD-cost:   85
c ---[1262]---> BDD-cost:   87
c ---[1260]---> BDD-cost:    7
c ---[1258]---> BDD-cost:   45
c ---[1256]---> BDD-cost:   43
c ---[1254]---> BDD-cost:   11
c ---[1252]---> BDD-cost:   59
c ---[1250]---> BDD-cost:  185
c ---[1248]---> BDD-cost:  249
c ---[1246]---> BDD-cost:  315
c ---[1244]---> BDD-cost:  137
c ---[1242]---> BDD-cost:  253
c ---[1240]---> BDD-cost:  161
c ---[1238]---> BDD-cost:  257
c ---[1236]---> BDD-cost:  167
c ---[1234]---> BDD-cost:  167
c ---[1232]---> BDD-cost:  141
c ---[1230]---> BDD-cost:   21
c ---[1228]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   95
c ---[1224]---> BDD-cost:  141
c ---[1222]---> BDD-cost:    0
c ---[1220]---> BDD-cost:  123
c ---[1218]---> BDD-cost:   83
c ---[1216]---> BDD-cost:   55
c ---[1214]---> BDD-cost:  183
c ---[1212]---> BDD-cost:  269
c ---[1210]---> BDD-cost:   63
c ---[1208]---> BDD-cost:   45
c ---[1206]---> BDD-cost:   39
c ---[1204]---> BDD-cost:   97
c ---[1202]---> BDD-cost:   51
c ---[1200]---> BDD-cost:   23
c ---[1198]---> BDD-cost:  101
c ---[1196]---> BDD-cost:   45
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   85
c ---[1190]---> BDD-cost:   35
c ---[1188]---> BDD-cost:   53
c ---[1186]---> BDD-cost:   21
c ---[1184]---> BDD-cost:  115
c ---[1182]---> BDD-cost:   99
c ---[1180]---> BDD-cost:   63
c ---[1178]---> BDD-cost:   77
c ---[1176]---> BDD-cost:   37
c ---[1174]---> BDD-cost:  139
c ---[1172]---> BDD-cost:  109
c ---[1170]---> BDD-cost:  407
c ---[1168]---> BDD-cost:  323
c ---[1166]---> BDD-cost:  109
c ---[1164]---> BDD-cost:   93
c ---[1162]---> BDD-cost:   51
c ---[1160]---> BDD-cost:   79
c ---[1158]---> BDD-cost:   75
c ---[1156]---> BDD-cost:  147
c ---[1154]---> BDD-cost:    0
c ---[1152]---> BDD-cost:  169
c ---[1150]---> BDD-cost:  209
c ---[1148]---> BDD-cost:   69
c ---[1146]---> BDD-cost:   51
c ---[1144]---> BDD-cost:   85
c ---[1140]---> BDD-cost:  103
c ---[1138]---> BDD-cost:  127
c ---[1136]---> BDD-cost:   77
c ---[1134]---> BDD-cost:   77
c ---[1132]---> BDD-cost:  181
c ---[1130]---> BDD-cost:  141
c ---[1128]---> BDD-cost:   89
c ---[1126]---> BDD-cost:   85
c ---[1124]---> BDD-cost:  119
c ---[1122]---> BDD-cost:   69
c ---[1120]---> BDD-cost:   57
c ---[1118]---> BDD-cost:   65
c ---[1116]---> BDD-cost:   47
c ---[1114]---> BDD-cost:   61
c ---[1112]---> BDD-cost:   31
c ---[1110]---> BDD-cost:  283
c ---[1106]---> BDD-cost:  183
c ---[1104]---> BDD-cost:  121
c ---[1102]---> BDD-cost:   89
c ---[1100]---> BDD-cost:  225
c ---[1098]---> BDD-cost:  267
c ---[1094]---> BDD-cost:  159
c ---[1092]---> BDD-cost:  209
c ---[1090]---> BDD-cost:   71
c ---[1088]---> BDD-cost:   99
c ---[1086]---> BDD-cost:  237
c ---[1084]---> BDD-cost:  129
c ---[1082]---> BDD-cost:  365
c ---[1080]---> BDD-cost:  369
c ---[1078]---> BDD-cost:  129
c ---[1076]---> BDD-cost:  101
c ---[1074]---> BDD-cost:  289
c ---[1072]---> BDD-cost:  279
c ---[1070]---> BDD-cost:  345
c ---[1068]---> BDD-cost:   81
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:   69
c ---[1062]---> BDD-cost:   83
c ---[1060]---> BDD-cost:   53
c ---[1058]---> BDD-cost:   67
c ---[1056]---> BDD-cost:   55
c ---[1054]---> BDD-cost:  145
c ---[1052]---> BDD-cost:  149
c ---[1050]---> BDD-cost:  105
c ---[1048]---> BDD-cost:   19
c ---[1046]---> BDD-cost:  105
c ---[1044]---> BDD-cost:  109
c ---[1042]---> BDD-cost:  101
c ---[1040]---> BDD-cost:  147
c ---[1038]---> BDD-cost:  231
c ---[1036]---> BDD-cost:  191
c ---[1034]---> BDD-cost:  157
c ---[1032]---> BDD-cost:  249
c ---[1030]---> BDD-cost:  385
c ---[1028]---> BDD-cost:   67
c ---[1026]---> BDD-cost:   71
c ---[1024]---> BDD-cost:   47
c ---[1022]---> BDD-cost:   75
c ---[1020]---> BDD-cost:  147
c ---[1018]---> BDD-cost:  139
c ---[1016]---> BDD-cost:  273
c ---[1014]---> BDD-cost:  213
c ---[1012]---> BDD-cost:  169
c ---[1010]---> BDD-cost:  239
c ---[1008]---> BDD-cost:  305
c ---[1006]---> BDD-cost:  109
c ---[1004]---> BDD-cost:  105
c ---[1002]---> BDD-cost:  147
c ---[1000]---> BDD-cost:  237
c ---[ 998]---> BDD-cost:  115
c ---[ 996]---> BDD-cost:  115
c ---[ 994]---> BDD-cost:   67
c ---[ 992]---> BDD-cost:  329
c ---[ 990]---> BDD-cost:  295
c ---[ 988]---> BDD-cost:   51
c ---[ 986]---> BDD-cost:   61
c ---[ 984]---> BDD-cost:  317
c ---[ 982]---> BDD-cost:   97
c ---[ 980]---> BDD-cost:   79
c ---[ 978]---> BDD-cost:   29
c ---[ 976]---> BDD-cost:  119
c ---[ 974]---> BDD-cost:   43
c ---[ 972]---> BDD-cost:   85
c ---[ 970]---> BDD-cost:   35
c ---[ 968]---> BDD-cost:   69
c ---[ 964]---> BDD-cost:   45
c ---[ 962]---> BDD-cost:   73
c ---[ 960]---> BDD-cost:   55
c ---[ 956]---> BDD-cost:   33
c ---[ 954]---> BDD-cost:  109
c ---[ 952]---> BDD-cost:   29
c ---[ 950]---> BDD-cost:  245
c ---[ 948]---> BDD-cost:  225
c ---[ 946]---> BDD-cost:  111
c ---[ 944]---> BDD-cost:  117
c ---[ 942]---> BDD-cost:  127
c ---[ 940]---> BDD-cost:  129
c ---[ 938]---> BDD-cost:  259
c ---[ 936]---> BDD-cost:  221
c ---[ 934]---> BDD-cost:  275
c ---[ 932]---> BDD-cost:   83
c ---[ 930]---> BDD-cost:  209
c ---[ 928]---> BDD-cost:  267
c ---[ 926]---> BDD-cost:  171
c ---[ 924]---> BDD-cost:   57
c ---[ 920]---> BDD-cost:  133
c ---[ 918]---> BDD-cost:  185
c ---[ 916]---> BDD-cost:  169
c ---[ 914]---> BDD-cost:  287
c ---[ 912]---> BDD-cost:   81
c ---[ 910]---> BDD-cost:   13
c ---[ 908]---> BDD-cost:  335
c ---[ 906]---> BDD-cost:  365
c ---[ 904]---> BDD-cost:  255
c ---[ 902]---> BDD-cost:  111
c ---[ 900]---> BDD-cost:   57
c ---[ 898]---> BDD-cost:  101
c ---[ 896]---> BDD-cost:  197
c ---[ 894]---> BDD-cost:  383
c ---[ 892]---> BDD-cost:  329
c ---[ 890]---> BDD-cost:  241
c ---[ 888]---> BDD-cost:  157
c ---[ 886]---> BDD-cost:  129
c ---[ 884]---> BDD-cost:   85
c ---[ 882]---> BDD-cost:   71
c ---[ 880]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   77
c ---[ 876]---> BDD-cost:   49
c ---[ 874]---> BDD-cost:  133
c ---[ 872]---> BDD-cost:  133
c ---[ 870]---> BDD-cost:  377
c ---[ 868]---> BDD-cost:  117
c ---[ 866]---> BDD-cost:  155
c ---[ 862]---> BDD-cost:  119
c ---[ 860]---> BDD-cost:  119
c ---[ 858]---> BDD-cost:  151
c ---[ 856]---> BDD-cost:  221
c ---[ 854]---> BDD-cost:  181
c ---[ 850]---> BDD-cost:   87
c ---[ 848]---> BDD-cost:  127
c ---[ 846]---> BDD-cost:  299
c ---[ 844]---> BDD-cost:  109
c ---[ 842]---> BDD-cost:  331
c ---[ 838]---> BDD-cost:   21
c ---[ 836]---> BDD-cost:  205
c ---[ 834]---> BDD-cost:  217
c ---[ 832]---> BDD-cost:  349
c ---[ 830]---> BDD-cost:  291
c ---[ 828]---> BDD-cost:  165
c ---[ 826]---> BDD-cost:  161
c ---[ 824]---> BDD-cost:   61
c ---[ 822]---> BDD-cost:   77
c ---[ 820]---> BDD-cost:   55
c ---[ 818]---> BDD-cost:  113
c ---[ 816]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:  189
c ---[ 812]---> BDD-cost:  157
c ---[ 810]---> BDD-cost:  149
c ---[ 808]---> BDD-cost:  139
c ---[ 806]---> BDD-cost:  165
c ---[ 804]---> BDD-cost:  181
c ---[ 802]---> BDD-cost:  253
c ---[ 800]---> BDD-cost:    0
c ---[ 798]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:  145
c ---[ 794]---> BDD-cost:  141
c ---[ 792]---> BDD-cost:  105
c ---[ 790]---> BDD-cost:   95
c ---[ 788]---> BDD-cost:   75
c ---[ 786]---> BDD-cost:  103
c ---[ 784]---> BDD-cost:  149
c ---[ 782]---> BDD-cost:  137
c ---[ 780]---> BDD-cost:   59
c ---[ 778]---> BDD-cost:  133
c ---[ 776]---> BDD-cost:    5
c ---[ 774]---> BDD-cost:   35
c ---[ 772]---> BDD-cost:    9
c ---[ 770]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   55
c ---[ 762]---> BDD-cost:  197
c ---[ 760]---> BDD-cost:  191
c ---[ 758]---> BDD-cost:  125
c ---[ 756]---> BDD-cost:    0
c ---[ 754]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  173
c ---[ 748]---> BDD-cost:   93
c ---[ 746]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:  321
c ---[ 742]---> BDD-cost:  195
c ---[ 740]---> BDD-cost:  163
c ---[ 734]---> BDD-cost:  151
c ---[ 732]---> BDD-cost:  115
c ---[ 730]---> BDD-cost:  253
c ---[ 728]---> BDD-cost:  381
c ---[ 726]---> BDD-cost:  345
c ---[ 724]---> BDD-cost:  185
c ---[ 720]---> BDD-cost:   83
c ---[ 718]---> BDD-cost:   69
c ---[ 716]---> BDD-cost:   51
c ---[ 714]---> BDD-cost:   47
c ---[ 712]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:  185
c ---[ 708]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  107
c ---[ 704]---> BDD-cost:  363
c ---[ 702]---> BDD-cost:  103
c ---[ 700]---> BDD-cost:  277
c ---[ 698]---> BDD-cost:  341
c ---[ 696]---> BDD-cost:  213
c ---[ 694]---> BDD-cost:  315
c ---[ 692]---> BDD-cost:  275
c ---[ 690]---> BDD-cost:  151
c ---[ 688]---> BDD-cost:  203
c ---[ 686]---> BDD-cost:  111
c ---[ 684]---> BDD-cost:  103
c ---[ 682]---> BDD-cost:   75
c ---[ 680]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   21
c ---[ 676]---> BDD-cost:   11
c ---[ 674]---> BDD-cost:   31
c ---[ 670]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:  149
c ---[ 666]---> BDD-cost:  167
c ---[ 664]---> BDD-cost:    0
c ---[ 662]---> BDD-cost:   97
c ---[ 660]---> BDD-cost:  149
c ---[ 658]---> BDD-cost:  395
c ---[ 656]---> BDD-cost:   25
c ---[ 654]---> BDD-cost:  389
c ---[ 652]---> BDD-cost:  251
c ---[ 650]---> BDD-cost:  375
c ---[ 648]---> BDD-cost:  343
c ---[ 646]---> BDD-cost:  267
c ---[ 644]---> BDD-cost:  135
c ---[ 642]---> BDD-cost:  135
c ---[ 640]---> BDD-cost:  263
c ---[ 638]---> BDD-cost:  259
c ---[ 636]---> BDD-cost:  245
c ---[ 634]---> BDD-cost:   45
c ---[ 632]---> BDD-cost:   41
c ---[ 630]---> BDD-cost:  127
c ---[ 628]---> BDD-cost:  117
c ---[ 626]---> BDD-cost:   53
c ---[ 624]---> BDD-cost:  149
c ---[ 622]---> BDD-cost:    9
c ---[ 620]---> BDD-cost:  103
c ---[ 618]---> BDD-cost:  215
c ---[ 616]---> BDD-cost:   89
c ---[ 614]---> BDD-cost:  177
c ---[ 612]---> BDD-cost:  343
c ---[ 610]---> BDD-cost:  237
c ---[ 608]---> BDD-cost:  177
c ---[ 606]---> BDD-cost:   85
c ---[ 604]---> BDD-cost:  267
c ---[ 602]---> BDD-cost:  225
c ---[ 600]---> BDD-cost:   85
c ---[ 598]---> BDD-cost:  109
c ---[ 596]---> BDD-cost:  105
c ---[ 594]---> BDD-cost:  113
c ---[ 592]---> BDD-cost:   55
c ---[ 590]---> BDD-cost:  117
c ---[ 588]---> BDD-cost:   83
c ---[ 586]---> BDD-cost:   79
c ---[ 584]---> BDD-cost:   81
c ---[ 582]---> BDD-cost:  263
c ---[ 580]---> BDD-cost:  179
c ---[ 578]---> BDD-cost:  143
c ---[ 576]---> BDD-cost:  281
c ---[ 574]---> BDD-cost:  389
c ---[ 572]---> BDD-cost:  333
c ---[ 570]---> BDD-cost:  357
c ---[ 568]---> BDD-cost:  345
c ---[ 566]---> BDD-cost:  263
c ---[ 564]---> BDD-cost:   89
c ---[ 562]---> BDD-cost:  285
c ---[ 558]---> BDD-cost:  419
c ---[ 556]---> BDD-cost:  135
c ---[ 554]---> BDD-cost:  357
c ---[ 552]---> BDD-cost:  473
c ---[ 550]---> BDD-cost:  455
c ---[ 548]---> BDD-cost:  405
c ---[ 546]---> BDD-cost:  241
c ---[ 544]---> BDD-cost:  211
c ---[ 542]---> BDD-cost:  313
c ---[ 540]---> BDD-cost:  371
c ---[ 538]---> BDD-cost:  389
c ---[ 536]---> BDD-cost:  223
c ---[ 534]---> BDD-cost:   71
c ---[ 532]---> BDD-cost:   63
c ---[ 530]---> BDD-cost:  221
c ---[ 528]---> BDD-cost:  147
c ---[ 526]---> BDD-cost:  131
c ---[ 524]---> BDD-cost:  185
c ---[ 522]---> BDD-cost:  141
c ---[ 520]---> BDD-cost:  249
c ---[ 518]---> BDD-cost:  261
c ---[ 516]---> BDD-cost:  311
c ---[ 514]---> BDD-cost:  261
c ---[ 512]---> BDD-cost:  387
c ---[ 510]---> BDD-cost:   51
c ---[ 508]---> BDD-cost:  247
c ---[ 506]---> BDD-cost:  295
c ---[ 504]---> BDD-cost:   31
c ---[ 502]---> BDD-cost:  355
c ---[ 500]---> BDD-cost:  135
c ---[ 498]---> BDD-cost:  443
c ---[ 496]---> BDD-cost:  653
c ---[ 494]---> BDD-cost:  703
c ---[ 492]---> BDD-cost:  517
c ---[ 490]---> BDD-cost:  441
c ---[ 488]---> BDD-cost:  159
c ---[ 486]---> BDD-cost:  411
c ---[ 484]---> BDD-cost:  289
c ---[ 482]---> BDD-cost:  277
c ---[ 480]---> BDD-cost:  239
c ---[ 478]---> BDD-cost:  201
c ---[ 476]---> BDD-cost:  309
c ---[ 474]---> BDD-cost:  287
c ---[ 472]---> BDD-cost:  177
c ---[ 470]---> BDD-cost:  143
c ---[ 468]---> BDD-cost:  131
c ---[ 466]---> BDD-cost:  155
c ---[ 464]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:  189
c ---[ 460]---> BDD-cost:  219
c ---[ 456]---> BDD-cost:  267
c ---[ 454]---> BDD-cost:  135
c ---[ 452]---> BDD-cost:   69
c ---[ 450]---> BDD-cost:   75
c ---[ 448]---> BDD-cost:   51
c ---[ 446]---> BDD-cost:  117
c ---[ 444]---> BDD-cost:  211
c ---[ 442]---> BDD-cost:  117
c ---[ 436]---> BDD-cost:  189
c ---[ 434]---> BDD-cost:   73
c ---[ 432]---> BDD-cost:   55
c ---[ 430]---> BDD-cost:   57
c ---[ 428]---> BDD-cost:   91
c ---[ 426]---> BDD-cost:  325
c ---[ 424]---> BDD-cost:  223
c ---[ 422]---> BDD-cost:   75
c ---[ 420]---> BDD-cost:   57
c ---[ 418]---> BDD-cost:   43
c ---[ 416]---> BDD-cost:  255
c ---[ 414]---> BDD-cost:  285
c ---[ 412]---> BDD-cost:  187
c ---[ 410]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   91
c ---[ 406]---> BDD-cost:  211
c ---[ 404]---> BDD-cost:  159
c ---[ 402]---> BDD-cost:   97
c ---[ 400]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   27
c ---[ 396]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  141
c ---[ 390]---> BDD-cost:  109
c ---[ 388]---> BDD-cost:  321
c ---[ 386]---> BDD-cost:  305
c ---[ 384]---> BDD-cost:  603
c ---[ 382]---> BDD-cost:  441
c ---[ 380]---> BDD-cost:  391
c ---[ 378]---> BDD-cost:   87
c ---[ 376]---> BDD-cost:  387
c ---[ 374]---> BDD-cost:  289
c ---[ 372]---> BDD-cost:  219
c ---[ 370]---> BDD-cost:  309
c ---[ 368]---> BDD-cost:  241
c ---[ 366]---> BDD-cost:  197
c ---[ 364]---> BDD-cost:  279
c ---[ 362]---> BDD-cost:  167
c ---[ 360]---> BDD-cost:  151
c ---[ 358]---> BDD-cost:   49
c ---[ 356]---> BDD-cost:   79
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:  107
c ---[ 350]---> BDD-cost:   55
c ---[ 346]---> BDD-cost:  177
c ---[ 344]---> BDD-cost:  223
c ---[ 342]---> BDD-cost:  119
c ---[ 340]---> BDD-cost:  137
c ---[ 338]---> BDD-cost:  105
c ---[ 336]---> BDD-cost:  183
c ---[ 334]---> BDD-cost:  109
c ---[ 332]---> BDD-cost:  179
c ---[ 330]---> BDD-cost:  285
c ---[ 328]---> BDD-cost:  191
c ---[ 326]---> BDD-cost:  177
c ---[ 324]---> BDD-cost:  145
c ---[ 320]---> BDD-cost:  153
c ---[ 318]---> BDD-cost:  121
c ---[ 316]---> BDD-cost:   95
c ---[ 314]---> BDD-cost:  111
c ---[ 312]---> BDD-cost:   35
c ---[ 310]---> BDD-cost:  115
c ---[ 308]---> BDD-cost:    0
c ---[ 306]---> BDD-cost:  281
c ---[ 304]---> BDD-cost:  265
c ---[ 302]---> BDD-cost:  167
c ---[ 300]---> BDD-cost:  151
c ---[ 298]---> BDD-cost:  167
c ---[ 296]---> BDD-cost:  137
c ---[ 292]---> BDD-cost:  375
c ---[ 290]---> BDD-cost:  287
c ---[ 288]---> BDD-cost:  247
c ---[ 286]---> BDD-cost:  249
c ---[ 284]---> BDD-cost:  131
c ---[ 282]---> BDD-cost:  187
c ---[ 280]---> BDD-cost:  135
c ---[ 278]---> BDD-cost:  129
c ---[ 276]---> BDD-cost:  317
c ---[ 274]---> BDD-cost:  365
c ---[ 272]---> BDD-cost:  235
c ---[ 270]---> BDD-cost:  249
c ---[ 268]---> BDD-cost:  283
c ---[ 266]---> BDD-cost:  105
c ---[ 264]---> BDD-cost:  233
c ---[ 262]---> BDD-cost:  259
c ---[ 260]---> BDD-cost:  287
c ---[ 258]---> BDD-cost:  175
c ---[ 256]---> BDD-cost:  233
c ---[ 254]---> BDD-cost:  167
c ---[ 252]---> BDD-cost:  159
c ---[ 250]---> BDD-cost:   47
c ---[ 246]---> BDD-cost:  135
c ---[ 244]---> BDD-cost:   59
c ---[ 242]---> BDD-cost:  147
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  203
c ---[ 236]---> BDD-cost:  275
c ---[ 234]---> BDD-cost:  263
c ---[ 232]---> BDD-cost:   31
c ---[ 230]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   31
c ---[ 226]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:  225
c ---[ 222]---> BDD-cost:   71
c ---[ 220]---> BDD-cost:   65
c ---[ 218]---> BDD-cost:  385
c ---[ 216]---> BDD-cost:  361
c ---[ 214]---> BDD-cost:   73
c ---[ 212]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:  131
c ---[ 206]---> BDD-cost:  145
c ---[ 204]---> BDD-cost:  121
c ---[ 202]---> BDD-cost:  117
c ---[ 200]---> BDD-cost:   61
c ---[ 198]---> BDD-cost:  111
c ---[ 196]---> BDD-cost:  123
c ---[ 194]---> BDD-cost:  125
c ---[ 192]---> BDD-cost:  243
c ---[ 190]---> BDD-cost:  143
c ---[ 188]---> BDD-cost:  149
c ---[ 186]---> BDD-cost:  103
c ---[ 184]---> BDD-cost:  155
c ---[ 182]---> BDD-cost:  247
c ---[ 180]---> BDD-cost:  143
c ---[ 178]---> BDD-cost:   89
c ---[ 176]---> BDD-cost:   91
c ---[ 174]---> BDD-cost:   81
c ---[ 172]---> BDD-cost:   79
c ---[ 170]---> BDD-cost:  117
c ---[ 168]---> BDD-cost:   89
c ---[ 166]---> BDD-cost:   61
c ---[ 164]---> BDD-cost:  127
c ---[ 162]---> BDD-cost:  135
c ---[ 160]---> BDD-cost:  161
c ---[ 158]---> BDD-cost:  141
c ---[ 156]---> BDD-cost:   91
c ---[ 154]---> BDD-cost:  437
c ---[ 152]---> BDD-cost:  309
c ---[ 150]---> BDD-cost:  173
c ---[ 148]---> BDD-cost:  441
c ---[ 146]---> BDD-cost:  489
c ---[ 144]---> BDD-cost:  299
c ---[ 142]---> BDD-cost:  455
c ---[ 140]---> BDD-cost:  333
c ---[ 138]---> BDD-cost:  421
c ---[ 136]---> BDD-cost:  375
c ---[ 134]---> BDD-cost:  143
c ---[ 132]---> BDD-cost:  433
c ---[ 130]---> BDD-cost:  405
c ---[ 128]---> BDD-cost:  333
c ---[ 126]---> BDD-cost:  673
c ---[ 124]---> BDD-cost:  685
c ---[ 122]---> BDD-cost:  385
c ---[ 120]---> BDD-cost:  267
c ---[ 118]---> BDD-cost:  345
c ---[ 116]---> BDD-cost:  365
c ---[ 114]---> BDD-cost:  391
c ---[ 112]---> BDD-cost:  111
c ---[ 110]---> BDD-cost:  313
c ---[ 108]---> BDD-cost:  275
c ---[ 106]---> BDD-cost:  257
c ---[ 104]---> BDD-cost:  203
c ---[ 102]---> BDD-cost:  311
c ---[ 100]---> BDD-cost:  227
c ---[  98]---> BDD-cost:  295
c ---[  96]---> BDD-cost:  233
c ---[  94]---> BDD-cost:  247
c ---[  92]---> BDD-cost:  237
c ---[  90]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   95
c ---[  86]---> BDD-cost:    0
c ---[  84]---> BDD-cost:  149
c ---[  80]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   85
c ---[  76]---> BDD-cost:  109
c ---[  74]---> BDD-cost:   43
c ---[  72]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   71
c ---[  68]---> BDD-cost:   67
c ---[  66]---> BDD-cost:  169
c ---[  64]---> BDD-cost:  151
c ---[  62]---> BDD-cost:  147
c ---[  60]---> BDD-cost:  177
c ---[  58]---> BDD-cost:  127
c ---[  56]---> BDD-cost:  131
c ---[  54]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  215
c ---[  50]---> BDD-cost:  181
c ---[  48]---> BDD-cost:  235
c ---[  46]---> BDD-cost:  163
c ---[  44]---> BDD-cost:  101
c ---[  42]---> BDD-cost:   57
c ---[  40]---> BDD-cost:   59
c ---[  38]---> BDD-cost:  139
c ---[  36]---> BDD-cost:   39
c ---[  34]---> BDD-cost:  151
c ---[  32]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   45
c ---[  28]---> BDD-cost:   45
c ---[  26]---> BDD-cost:   45
c ---[  24]---> BDD-cost:   65
c ---[  22]---> BDD-cost:   95
c ---[  20]---> BDD-cost:    0
c ---[  16]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   81
c ---[   2]---> BDD-cost:  223
c ---[   0]---> BDD-cost:  271
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 |       101 |  310358   807732 |  113797     101     4421    43.8 |  0.588 % |
c |       251 |  310340   807685 |  125176     248     8941    36.1 |  0.590 % |
c |       477 |  310255   807455 |  137694     461    13728    29.8 |  0.603 % |
c |       814 |  310255   807455 |  151464     798    37090    46.5 |  0.603 % |
c |      1320 |  309505   805553 |  166610    1266    60778    48.0 |  0.693 % |
c |      2079 |  309327   805067 |  183271    2007    94497    47.1 |  0.730 % |
c |      3219 |  308710   803466 |  201598    3121   175840    56.3 |  0.848 % |
c |      4927 |  308374   802597 |  221758    4783   334504    69.9 |  0.896 % |
c |      7489 |  307940   801458 |  243934    7200   539854    75.0 |  0.948 % |
c |     11334 |  307798   801098 |  268327   11017  1054203    95.7 |  0.963 % |
c |     17100 |  307510   800357 |  295160   16719  1913448   114.4 |  0.992 % |
c |     25749 |  307286   799785 |  324676   25320  3051328   120.5 |  1.011 % |
c |     38723 |  307204   799580 |  357144   38277  5578865   145.7 |  1.014 % |
c |     58184 |  306684   798243 |  392858   57603  9277788   161.1 |  1.076 % |
c |     87376 |  306512   797802 |  432144   86712 17039623   196.5 |  1.089 % |
c |    131165 |  306227   797059 |  475359  130316 29832985   228.9 |  1.132 % |
#### 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.85 0.93 0.95 2/54 28611
Raw data (stat): 28611 (runsolver) R 28610 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484037258 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.0007 s]
Raw data (loadavg): 0.88 0.93 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 11039 0 0 0 966 31 0 0 25 0 1 0 484037258 54317056 10670 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13261 10670 603 41 0 13220 0
vsize: 53044
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.93 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 11178 0 0 0 1964 32 0 0 25 0 1 0 484037258 54857728 10809 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13393 10809 603 41 0 13352 0
vsize: 53572
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.94 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 11354 0 0 0 2963 33 0 0 25 0 1 0 484037258 55672832 10985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13592 10985 603 41 0 13551 0
vsize: 54368
[startup+40.0021 s]
Raw data (loadavg): 0.92 0.94 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 11527 0 0 0 3963 33 0 0 25 0 1 0 484037258 56344576 11158 4294967295 134512640 134672761 3221224544 3221223712 134561394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13756 11158 603 41 0 13715 0
vsize: 55024
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 11706 0 0 0 4962 34 0 0 25 0 1 0 484037258 57061376 11337 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13931 11337 603 41 0 13890 0
vsize: 55724
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.94 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 12022 0 0 0 5962 34 0 0 25 0 1 0 484037258 58404864 11653 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14259 11653 603 41 0 14218 0
vsize: 57036
[startup+70.0034 s]
Raw data (loadavg): 0.95 0.94 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 12293 0 0 0 6962 35 0 0 25 0 1 0 484037258 59486208 11924 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14523 11924 603 41 0 14482 0
vsize: 58092
[startup+80.004 s]
Raw data (loadavg): 0.96 0.94 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 12670 0 0 0 7961 36 0 0 25 0 1 0 484037258 60968960 12301 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14885 12301 603 41 0 14844 0
vsize: 59540
[startup+90.0044 s]
Raw data (loadavg): 0.97 0.94 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 12995 0 0 0 8960 37 0 0 25 0 1 0 484037258 62427136 12626 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15241 12626 603 41 0 15200 0
vsize: 60964
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 13313 0 0 0 9958 39 0 0 25 0 1 0 484037258 63643648 12944 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15538 12944 603 41 0 15497 0
vsize: 62152
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 13555 0 0 0 10956 41 0 0 25 0 1 0 484037258 64585728 13186 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15768 13186 603 41 0 15727 0
vsize: 63072
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 13844 0 0 0 11956 41 0 0 25 0 1 0 484037258 65794048 13475 4294967295 134512640 134672761 3221224544 3221223716 134556664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16063 13475 603 41 0 16022 0
vsize: 64252
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 14109 0 0 0 12955 42 0 0 25 0 1 0 484037258 66875392 13740 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16327 13740 603 41 0 16286 0
vsize: 65308
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 14470 0 0 0 13954 43 0 0 25 0 1 0 484037258 68354048 14101 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16688 14101 603 41 0 16647 0
vsize: 66752
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 14714 0 0 0 14954 44 0 0 25 0 1 0 484037258 69292032 14345 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16917 14345 603 41 0 16876 0
vsize: 67668
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 15094 0 0 0 15953 45 0 0 25 0 1 0 484037258 70905856 14725 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17311 14725 603 41 0 17270 0
vsize: 69244
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 15415 0 0 0 16952 45 0 0 25 0 1 0 484037258 72122368 15046 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17608 15046 603 41 0 17567 0
vsize: 70432
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 15740 0 0 0 17952 46 0 0 25 0 1 0 484037258 73469952 15371 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17937 15371 603 41 0 17896 0
vsize: 71748
[startup+190.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 16131 0 0 0 18950 48 0 0 25 0 1 0 484037258 75218944 15762 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18364 15762 603 41 0 18323 0
vsize: 73456
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 16511 0 0 0 19949 49 0 0 25 0 1 0 484037258 76828672 16142 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18757 16142 603 41 0 18716 0
vsize: 75028
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 16825 0 0 0 20949 50 0 0 25 0 1 0 484037258 78036992 16456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19052 16456 603 41 0 19011 0
vsize: 76208
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 17120 0 0 0 21948 51 0 0 25 0 1 0 484037258 79249408 16751 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19348 16751 603 41 0 19307 0
vsize: 77392
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 17336 0 0 0 22948 51 0 0 25 0 1 0 484037258 80056320 16967 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19545 16967 603 41 0 19504 0
vsize: 78180
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 17614 0 0 0 23947 52 0 0 25 0 1 0 484037258 81264640 17245 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19840 17245 603 41 0 19799 0
vsize: 79360
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 17900 0 0 0 24947 53 0 0 25 0 1 0 484037258 82481152 17531 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17531 603 41 0 20096 0
vsize: 80548
[startup+260.009 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 18312 0 0 0 25946 53 0 0 25 0 1 0 484037258 84099072 17943 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20532 17943 603 41 0 20491 0
vsize: 82128
[startup+270.009 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 18593 0 0 0 26946 54 0 0 25 0 1 0 484037258 85180416 18224 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20796 18224 603 41 0 20755 0
vsize: 83184
[startup+280.01 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 18876 0 0 0 27945 55 0 0 25 0 1 0 484037258 86388736 18507 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21091 18507 603 41 0 21050 0
vsize: 84364
[startup+290.01 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 19110 0 0 0 28945 56 0 0 25 0 1 0 484037258 87326720 18741 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21320 18741 603 41 0 21279 0
vsize: 85280
[startup+300.01 s]
Raw data (loadavg): 0.99 0.96 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 19483 0 0 0 29944 57 0 0 25 0 1 0 484037258 88813568 19114 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21683 19114 603 41 0 21642 0
vsize: 86732
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 19831 0 0 0 30943 58 0 0 25 0 1 0 484037258 90288128 19462 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22043 19462 603 41 0 22002 0
vsize: 88172
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 20144 0 0 0 31942 59 0 0 25 0 1 0 484037258 91631616 19775 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22371 19775 603 41 0 22330 0
vsize: 89484
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 20565 0 0 0 32941 60 0 0 25 0 1 0 484037258 93237248 20196 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22763 20196 603 41 0 22722 0
vsize: 91052
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 20926 0 0 0 33940 61 0 0 25 0 1 0 484037258 94715904 20557 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23124 20557 603 41 0 23083 0
vsize: 92496
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 21192 0 0 0 34939 62 0 0 25 0 1 0 484037258 95793152 20823 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23387 20823 603 41 0 23346 0
vsize: 93548
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 21420 0 0 0 35939 62 0 0 25 0 1 0 484037258 96735232 21051 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23617 21051 603 41 0 23576 0
vsize: 94468
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 21864 0 0 0 36938 63 0 0 25 0 1 0 484037258 98619392 21495 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24077 21495 603 41 0 24036 0
vsize: 96308
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 22216 0 0 0 37937 65 0 0 25 0 1 0 484037258 99971072 21847 4294967295 134512640 134672761 3221224544 3221223728 134559566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24407 21847 603 41 0 24366 0
vsize: 97628
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 22559 0 0 0 38936 65 0 0 25 0 1 0 484037258 101437440 22190 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24765 22190 603 41 0 24724 0
vsize: 99060
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 22877 0 0 0 39936 66 0 0 25 0 1 0 484037258 103047168 22508 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25158 22508 603 41 0 25117 0
vsize: 100632
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 23201 0 0 0 40935 67 0 0 25 0 1 0 484037258 104259584 22832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25454 22832 603 41 0 25413 0
vsize: 101816
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 23607 0 0 0 41934 68 0 0 25 0 1 0 484037258 106016768 23238 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25883 23238 603 41 0 25842 0
vsize: 103532
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 24061 0 0 0 42933 70 0 0 25 0 1 0 484037258 107896832 23692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26342 23692 603 41 0 26301 0
vsize: 105368
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 24327 0 0 0 43933 70 0 0 25 0 1 0 484037258 108965888 23958 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26603 23958 603 41 0 26562 0
vsize: 106412
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 24524 0 0 0 44932 71 0 0 25 0 1 0 484037258 109772800 24155 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26800 24155 603 41 0 26759 0
vsize: 107200
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 24908 0 0 0 45931 72 0 0 25 0 1 0 484037258 111251456 24539 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27161 24539 603 41 0 27120 0
vsize: 108644
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 25268 0 0 0 46931 72 0 0 25 0 1 0 484037258 112738304 24899 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27524 24899 603 41 0 27483 0
vsize: 110096
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 25669 0 0 0 47930 73 0 0 25 0 1 0 484037258 114352128 25300 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27918 25300 603 41 0 27877 0
vsize: 111672
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 26057 0 0 0 48930 74 0 0 25 0 1 0 484037258 115957760 25688 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28310 25688 603 41 0 28269 0
vsize: 113240
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 26369 0 0 0 49929 75 0 0 25 0 1 0 484037258 117297152 26000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28637 26000 603 41 0 28596 0
vsize: 114548
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 26671 0 0 0 50928 76 0 0 25 0 1 0 484037258 118497280 26302 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28930 26302 603 41 0 28889 0
vsize: 115720
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 27086 0 0 0 51928 77 0 0 25 0 1 0 484037258 120246272 26717 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29357 26717 603 41 0 29316 0
vsize: 117428
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 27491 0 0 0 52927 78 0 0 25 0 1 0 484037258 121860096 27122 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29751 27122 603 41 0 29710 0
vsize: 119004
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 27820 0 0 0 53926 79 0 0 25 0 1 0 484037258 123195392 27451 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30077 27451 603 41 0 30036 0
vsize: 120308
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 28245 0 0 0 54925 80 0 0 25 0 1 0 484037258 124973056 27876 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30511 27876 603 41 0 30470 0
vsize: 122044
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 28670 0 0 0 55925 80 0 0 25 0 1 0 484037258 126603264 28301 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30909 28301 603 41 0 30868 0
vsize: 123636
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 29105 0 0 0 56923 82 0 0 25 0 1 0 484037258 128479232 28736 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 28736 603 41 0 31326 0
vsize: 125468
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 29537 0 0 0 57922 83 0 0 25 0 1 0 484037258 130220032 29168 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31792 29168 603 41 0 31751 0
vsize: 127168
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 29888 0 0 0 58921 84 0 0 25 0 1 0 484037258 131702784 29519 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32154 29519 603 41 0 32113 0
vsize: 128616
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 30238 0 0 0 59920 86 0 0 25 0 1 0 484037258 133062656 29869 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32486 29869 603 41 0 32445 0
vsize: 129944
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 30689 0 0 0 60919 86 0 0 25 0 1 0 484037258 134828032 30320 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32917 30320 603 41 0 32876 0
vsize: 131668
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 31050 0 0 0 61918 88 0 0 25 0 1 0 484037258 136437760 30681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 30681 603 41 0 33269 0
vsize: 133240
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 31427 0 0 0 62917 89 0 0 25 0 1 0 484037258 137912320 31058 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33670 31058 603 41 0 33629 0
vsize: 134680
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 31837 0 0 0 63917 89 0 0 25 0 1 0 484037258 139640832 31468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34092 31468 603 41 0 34051 0
vsize: 136368
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 32042 0 0 0 64917 90 0 0 25 0 1 0 484037258 140451840 31673 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34290 31673 603 41 0 34249 0
vsize: 137160
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 32351 0 0 0 65916 91 0 0 25 0 1 0 484037258 141799424 31982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34619 31982 603 41 0 34578 0
vsize: 138476
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 32706 0 0 0 66915 92 0 0 25 0 1 0 484037258 143134720 32337 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34945 32337 603 41 0 34904 0
vsize: 139780
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 33107 0 0 0 67915 92 0 0 25 0 1 0 484037258 144871424 32738 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35369 32738 603 41 0 35328 0
vsize: 141476
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 33469 0 0 0 68914 94 0 0 25 0 1 0 484037258 146354176 33100 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35731 33100 603 41 0 35690 0
vsize: 142924
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 33817 0 0 0 69913 95 0 0 25 0 1 0 484037258 147689472 33448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36057 33448 603 41 0 36016 0
vsize: 144228
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 34196 0 0 0 70912 96 0 0 25 0 1 0 484037258 149315584 33827 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36454 33827 603 41 0 36413 0
vsize: 145816
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 34495 0 0 0 71911 97 0 0 25 0 1 0 484037258 150532096 34126 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36751 34126 603 41 0 36710 0
vsize: 147004
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 34856 0 0 0 72910 98 0 0 25 0 1 0 484037258 152018944 34487 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37114 34487 603 41 0 37073 0
vsize: 148456
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 35152 0 0 0 73909 99 0 0 25 0 1 0 484037258 153231360 34783 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37410 34783 603 41 0 37369 0
vsize: 149640
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 35554 0 0 0 74909 100 0 0 25 0 1 0 484037258 154869760 35185 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37810 35185 603 41 0 37769 0
vsize: 151240
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 35897 0 0 0 75908 101 0 0 25 0 1 0 484037258 156241920 35528 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38145 35528 603 41 0 38104 0
vsize: 152580
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 36236 0 0 0 76907 101 0 0 25 0 1 0 484037258 157609984 35867 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38479 35867 603 41 0 38438 0
vsize: 153916
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 36460 0 0 0 77907 102 0 0 25 0 1 0 484037258 158552064 36091 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38709 36091 603 41 0 38668 0
vsize: 154836
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.95 3/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 36800 0 0 0 78906 104 0 0 25 0 1 0 484037258 159887360 36431 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39035 36431 603 41 0 38994 0
vsize: 156140
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 37066 0 0 0 79905 104 0 0 25 0 1 0 484037258 160956416 36697 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39296 36697 603 41 0 39255 0
vsize: 157184
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 37415 0 0 0 80905 105 0 0 25 0 1 0 484037258 162439168 37046 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39658 37046 603 41 0 39617 0
vsize: 158632
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 37640 0 0 0 81904 105 0 0 25 0 1 0 484037258 163381248 37271 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39888 37271 603 41 0 39847 0
vsize: 159552
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 37832 0 0 0 82904 106 0 0 25 0 1 0 484037258 164192256 37463 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40086 37463 603 41 0 40045 0
vsize: 160344
[startup+840.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 38099 0 0 0 83904 106 0 0 25 0 1 0 484037258 165277696 37730 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40351 37730 603 41 0 40310 0
vsize: 161404
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 38394 0 0 0 84903 107 0 0 25 0 1 0 484037258 166498304 38025 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40649 38025 603 41 0 40608 0
vsize: 162596
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 38708 0 0 0 85902 108 0 0 25 0 1 0 484037258 167710720 38339 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40945 38339 603 41 0 40904 0
vsize: 163780
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 39035 0 0 0 86902 109 0 0 25 0 1 0 484037258 169054208 38666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41273 38666 603 41 0 41232 0
vsize: 165092
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 39299 0 0 0 87901 110 0 0 25 0 1 0 484037258 170123264 38930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41534 38930 603 41 0 41493 0
vsize: 166136
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 39586 0 0 0 88900 111 0 0 25 0 1 0 484037258 171331584 39217 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41829 39217 603 41 0 41788 0
vsize: 167316
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 39902 0 0 0 89899 112 0 0 25 0 1 0 484037258 172544000 39533 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42125 39533 603 41 0 42084 0
vsize: 168500
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 40180 0 0 0 90898 113 0 0 25 0 1 0 484037258 173748224 39811 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42419 39811 603 41 0 42378 0
vsize: 169676
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 40499 0 0 0 91898 114 0 0 25 0 1 0 484037258 174956544 40130 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42714 40130 603 41 0 42673 0
vsize: 170856
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 40760 0 0 0 92897 115 0 0 25 0 1 0 484037258 176029696 40391 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42976 40391 603 41 0 42935 0
vsize: 171904
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 40991 0 0 0 93897 115 0 0 25 0 1 0 484037258 177094656 40622 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43236 40622 603 41 0 43195 0
vsize: 172944
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 41268 0 0 0 94896 116 0 0 25 0 1 0 484037258 178167808 40899 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43498 40899 603 41 0 43457 0
vsize: 173992
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 41529 0 0 0 95896 117 0 0 25 0 1 0 484037258 179249152 41160 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43762 41160 603 41 0 43721 0
vsize: 175048
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 41856 0 0 0 96895 118 0 0 25 0 1 0 484037258 180600832 41487 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44092 41487 603 41 0 44051 0
vsize: 176368
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 42162 0 0 0 97895 118 0 0 25 0 1 0 484037258 181800960 41793 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44385 41793 603 41 0 44344 0
vsize: 177540
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 42473 0 0 0 98893 119 0 0 25 0 1 0 484037258 183144448 42104 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44713 42104 603 41 0 44672 0
vsize: 178852
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 42744 0 0 0 99893 120 0 0 25 0 1 0 484037258 184750080 42375 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45105 42375 603 41 0 45064 0
vsize: 180420
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 42942 0 0 0 100892 121 0 0 25 0 1 0 484037258 185561088 42573 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45303 42573 603 41 0 45262 0
vsize: 181212
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 43128 0 0 0 101891 122 0 0 25 0 1 0 484037258 186236928 42759 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45468 42759 603 41 0 45427 0
vsize: 181872
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 43446 0 0 0 102891 123 0 0 25 0 1 0 484037258 187584512 43077 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45797 43077 603 41 0 45756 0
vsize: 183188
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 43820 0 0 0 103891 123 0 0 25 0 1 0 484037258 189079552 43451 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46162 43451 603 41 0 46121 0
vsize: 184648
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 44107 0 0 0 104890 124 0 0 25 0 1 0 484037258 190283776 43738 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46456 43738 603 41 0 46415 0
vsize: 185824
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 44401 0 0 0 105890 124 0 0 25 0 1 0 484037258 191504384 44032 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46754 44032 603 41 0 46713 0
vsize: 187016
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 44698 0 0 0 106889 125 0 0 25 0 1 0 484037258 192704512 44329 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47047 44329 603 41 0 47006 0
vsize: 188188
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 45194 0 0 0 107888 126 0 0 25 0 1 0 484037258 194723840 44825 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47540 44825 603 41 0 47499 0
vsize: 190160
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 45544 0 0 0 108888 127 0 0 25 0 1 0 484037258 196194304 45175 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47899 45175 603 41 0 47858 0
vsize: 191596
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 45770 0 0 0 109888 127 0 0 25 0 1 0 484037258 196997120 45401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48095 45401 603 41 0 48054 0
vsize: 192380
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 46038 0 0 0 110887 128 0 0 25 0 1 0 484037258 198205440 45669 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48390 45669 603 41 0 48349 0
vsize: 193560
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 46317 0 0 0 111886 129 0 0 25 0 1 0 484037258 199274496 45948 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48651 45948 603 41 0 48610 0
vsize: 194604
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 46740 0 0 0 112886 129 0 0 25 0 1 0 484037258 200978432 46371 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49067 46371 603 41 0 49026 0
vsize: 196268
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 46928 0 0 0 113886 130 0 0 25 0 1 0 484037258 201781248 46559 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49263 46559 603 41 0 49222 0
vsize: 197052
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 47131 0 0 0 114885 131 0 0 25 0 1 0 484037258 202592256 46762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49461 46762 603 41 0 49420 0
vsize: 197844
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 47420 0 0 0 115885 131 0 0 25 0 1 0 484037258 203788288 47051 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49753 47051 603 41 0 49712 0
vsize: 199012
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 47643 0 0 0 116885 131 0 0 25 0 1 0 484037258 204759040 47274 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49990 47274 603 41 0 49949 0
vsize: 199960
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 47966 0 0 0 117884 132 0 0 25 0 1 0 484037258 206110720 47597 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50320 47597 603 41 0 50279 0
vsize: 201280
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 48075 0 0 0 118884 132 0 0 25 0 1 0 484037258 206512128 47706 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50418 47706 603 41 0 50377 0
vsize: 201672
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 28611
Raw data (stat): 28611 (minisat+) R 28610 29151 29150 0 -1 0 48314 0 0 0 119884 133 0 0 25 0 1 0 484037258 207454208 47945 4294967295 134512640 134672761 3221224544 3221223712 134553613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50648 47945 603 41 0 50607 0
vsize: 202592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.95 1/54 28611
Raw data (stat): 28611 (minisat+) Z 28610 29151 29150 0 -1 12 48316 0 0 0 119884 142 0 0 25 0 1 0 484037258 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.13
CPU time (s): 1200.27
CPU user time (s): 1198.84
CPU system time (s): 1.42478
CPU usage (%): 100.012
Max. virtual memory (Kb): 202592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####