PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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	1185.16
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 21869

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-22 01:20:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12440 boxname=wulflinc31 idbench=957 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ee388359e66788d310d5d5b34d6465c1  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-air04.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-air04.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-air04.opb
IDLAUNCH: 12440
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        705336 kB
Buffers:         24520 kB
Cached:         280152 kB
SwapCached:        580 kB
Active:          68768 kB
Inactive:       237864 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        705084 kB
SwapTotal:     2097892 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            17084 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:40:04 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 12440 7 1200.25 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.92 0.95 0.90 2/54 7958
Raw data (stat): 7958 (runsolver) R 7957 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549697056 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.93 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 11039 0 0 0 971 28 0 0 25 0 1 0 549697056 54317056 10670 4294967295 134512640 134672761 3221224544 3221223500 1075350517 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.0019 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 11172 0 0 0 1970 29 0 0 25 0 1 0 549697056 54857728 10803 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13393 10803 603 41 0 13352 0
vsize: 53572
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 11352 0 0 0 2969 29 0 0 25 0 1 0 549697056 55672832 10983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13592 10983 603 41 0 13551 0
vsize: 54368
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 11516 0 0 0 3967 31 0 0 25 0 1 0 549697056 56213504 11147 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13724 11147 603 41 0 13683 0
vsize: 54896
[startup+50.0031 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 11702 0 0 0 4966 31 0 0 25 0 1 0 549697056 57061376 11333 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13931 11333 603 41 0 13890 0
vsize: 55724
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 12003 0 0 0 5966 32 0 0 25 0 1 0 549697056 58269696 11634 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14226 11634 603 41 0 14185 0
vsize: 56904
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 12277 0 0 0 6966 32 0 0 25 0 1 0 549697056 59351040 11908 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14490 11908 603 41 0 14449 0
vsize: 57960
[startup+80.0039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 12647 0 0 0 7965 33 0 0 25 0 1 0 549697056 60837888 12278 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14853 12278 603 41 0 14812 0
vsize: 59412
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 12922 0 0 0 8964 34 0 0 25 0 1 0 549697056 62046208 12553 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15148 12553 603 41 0 15107 0
vsize: 60592
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 13288 0 0 0 9963 35 0 0 25 0 1 0 549697056 63508480 12919 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15505 12919 603 41 0 15464 0
vsize: 62020
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 13529 0 0 0 10961 36 0 0 25 0 1 0 549697056 64585728 13160 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15768 13160 603 41 0 15727 0
vsize: 63072
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 13801 0 0 0 11961 37 0 0 25 0 1 0 549697056 65662976 13432 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16031 13432 603 41 0 15990 0
vsize: 64124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 14070 0 0 0 12960 38 0 0 25 0 1 0 549697056 66740224 13701 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16294 13701 603 41 0 16253 0
vsize: 65176
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 14392 0 0 0 13959 39 0 0 25 0 1 0 549697056 67952640 14023 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16590 14023 603 41 0 16549 0
vsize: 66360
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 14661 0 0 0 14958 40 0 0 25 0 1 0 549697056 69021696 14292 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16851 14292 603 41 0 16810 0
vsize: 67404
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 15025 0 0 0 15957 41 0 0 25 0 1 0 549697056 70496256 14656 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17211 14656 603 41 0 17170 0
vsize: 68844
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 15338 0 0 0 16957 42 0 0 25 0 1 0 549697056 71860224 14969 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17544 14969 603 41 0 17503 0
vsize: 70176
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 15651 0 0 0 17956 43 0 0 25 0 1 0 549697056 73068544 15282 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17839 15282 603 41 0 17798 0
vsize: 71356
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 16046 0 0 0 18955 44 0 0 25 0 1 0 549697056 74813440 15677 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18265 15677 603 41 0 18224 0
vsize: 73060
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 16390 0 0 0 19954 45 0 0 25 0 1 0 549697056 76296192 16021 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18627 16022 603 41 0 18586 0
vsize: 74508
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 16734 0 0 0 20953 46 0 0 25 0 1 0 549697056 77635584 16365 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18954 16365 603 41 0 18913 0
vsize: 75816
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 17019 0 0 0 21953 46 0 0 25 0 1 0 549697056 78843904 16650 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19249 16650 603 41 0 19208 0
vsize: 76996
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 17263 0 0 0 22953 47 0 0 25 0 1 0 549697056 79785984 16894 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19479 16894 603 41 0 19438 0
vsize: 77916
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 17507 0 0 0 23952 48 0 0 25 0 1 0 549697056 80859136 17138 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19741 17138 603 41 0 19700 0
vsize: 78964
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 17776 0 0 0 24951 49 0 0 25 0 1 0 549697056 81940480 17407 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20005 17407 603 41 0 19964 0
vsize: 80020
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 18113 0 0 0 25950 50 0 0 25 0 1 0 549697056 83288064 17744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20334 17744 603 41 0 20293 0
vsize: 81336
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 18501 0 0 0 26950 51 0 0 25 0 1 0 549697056 84910080 18132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20730 18132 603 41 0 20689 0
vsize: 82920
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 18763 0 0 0 27949 52 0 0 25 0 1 0 549697056 85987328 18394 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20993 18394 603 41 0 20952 0
vsize: 83972
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 19029 0 0 0 28948 53 0 0 25 0 1 0 549697056 87060480 18660 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21255 18660 603 41 0 21214 0
vsize: 85020
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 19296 0 0 0 29946 55 0 0 25 0 1 0 549697056 88137728 18927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21518 18927 603 41 0 21477 0
vsize: 86072
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 19665 0 0 0 30944 57 0 0 25 0 1 0 549697056 89616384 19296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21879 19296 603 41 0 21838 0
vsize: 87516
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 19966 0 0 0 31943 58 0 0 25 0 1 0 549697056 90828800 19597 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22175 19597 603 41 0 22134 0
vsize: 88700
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 20360 0 0 0 32943 59 0 0 25 0 1 0 549697056 92434432 19991 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22567 19991 603 41 0 22526 0
vsize: 90268
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 20765 0 0 0 33941 60 0 0 25 0 1 0 549697056 94044160 20396 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22960 20396 603 41 0 22919 0
vsize: 91840
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 21023 0 0 0 34940 62 0 0 25 0 1 0 549697056 95121408 20654 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23223 20654 603 41 0 23182 0
vsize: 92892
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 21276 0 0 0 35939 62 0 0 25 0 1 0 549697056 96198656 20907 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23486 20907 603 41 0 23445 0
vsize: 93944
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 21626 0 0 0 36939 63 0 0 25 0 1 0 549697056 97681408 21257 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23848 21257 603 41 0 23807 0
vsize: 95392
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 21997 0 0 0 37937 65 0 0 25 0 1 0 549697056 99160064 21628 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24209 21628 603 41 0 24168 0
vsize: 96836
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 22359 0 0 0 38936 66 0 0 25 0 1 0 549697056 100638720 21990 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24570 21990 603 41 0 24529 0
vsize: 98280
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 22692 0 0 0 39935 67 0 0 25 0 1 0 549697056 102236160 22323 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24960 22323 603 41 0 24919 0
vsize: 99840
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 22968 0 0 0 40935 68 0 0 25 0 1 0 549697056 103317504 22599 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 22599 603 41 0 25183 0
vsize: 100896
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 23350 0 0 0 41934 69 0 0 25 0 1 0 549697056 104935424 22981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25619 22981 603 41 0 25578 0
vsize: 102476
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 23716 0 0 0 42932 71 0 0 25 0 1 0 549697056 106422272 23347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25982 23347 603 41 0 25941 0
vsize: 103928
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 24140 0 0 0 43931 72 0 0 25 0 1 0 549697056 108158976 23771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26406 23771 603 41 0 26365 0
vsize: 105624
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 24342 0 0 0 44930 73 0 0 25 0 1 0 549697056 108965888 23973 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26603 23973 603 41 0 26562 0
vsize: 106412
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 24581 0 0 0 45930 73 0 0 25 0 1 0 549697056 109907968 24212 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26833 24212 603 41 0 26792 0
vsize: 107332
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 24993 0 0 0 46929 74 0 0 25 0 1 0 549697056 111656960 24624 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27260 24624 603 41 0 27219 0
vsize: 109040
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 25331 0 0 0 47929 75 0 0 25 0 1 0 549697056 113008640 24962 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27590 24962 603 41 0 27549 0
vsize: 110360
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 25738 0 0 0 48927 77 0 0 25 0 1 0 549697056 114749440 25369 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28015 25369 603 41 0 27974 0
vsize: 112060
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 26127 0 0 0 49927 78 0 0 25 0 1 0 549697056 116224000 25758 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28375 25758 603 41 0 28334 0
vsize: 113500
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 26413 0 0 0 50926 78 0 0 25 0 1 0 549697056 117432320 26044 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28670 26044 603 41 0 28629 0
vsize: 114680
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 26719 0 0 0 51925 79 0 0 25 0 1 0 549697056 118632448 26350 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28963 26350 603 41 0 28922 0
vsize: 115852
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 27147 0 0 0 52924 80 0 0 25 0 1 0 549697056 120381440 26778 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29390 26778 603 41 0 29349 0
vsize: 117560
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 27518 0 0 0 53923 82 0 0 25 0 1 0 549697056 121991168 27149 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29783 27149 603 41 0 29742 0
vsize: 119132
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 27843 0 0 0 54923 82 0 0 25 0 1 0 549697056 123334656 27474 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30111 27474 603 41 0 30070 0
vsize: 120444
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 28268 0 0 0 55921 84 0 0 25 0 1 0 549697056 124973056 27899 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30511 27899 603 41 0 30470 0
vsize: 122044
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 28698 0 0 0 56920 85 0 0 25 0 1 0 549697056 126742528 28329 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30943 28329 603 41 0 30902 0
vsize: 123772
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 29123 0 0 0 57918 87 0 0 25 0 1 0 549697056 128479232 28754 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 28754 603 41 0 31326 0
vsize: 125468
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 29543 0 0 0 58918 87 0 0 25 0 1 0 549697056 130220032 29174 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31792 29174 603 41 0 31751 0
vsize: 127168
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 29885 0 0 0 59917 88 0 0 25 0 1 0 549697056 131563520 29516 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32120 29516 603 41 0 32079 0
vsize: 128480
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 30238 0 0 0 60916 89 0 0 25 0 1 0 549697056 133062656 29869 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32486 29869 603 41 0 32445 0
vsize: 129944
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 30675 0 0 0 61916 90 0 0 25 0 1 0 549697056 134828032 30306 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32917 30306 603 41 0 32876 0
vsize: 131668
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 31015 0 0 0 62916 90 0 0 25 0 1 0 549697056 136306688 30646 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33278 30646 603 41 0 33237 0
vsize: 133112
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 31394 0 0 0 63915 91 0 0 25 0 1 0 549697056 137777152 31025 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33637 31025 603 41 0 33596 0
vsize: 134548
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 31804 0 0 0 64914 92 0 0 25 0 1 0 549697056 139513856 31435 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34061 31435 603 41 0 34020 0
vsize: 136244
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 32023 0 0 0 65914 92 0 0 25 0 1 0 549697056 140451840 31654 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34290 31654 603 41 0 34249 0
vsize: 137160
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 32309 0 0 0 66914 93 0 0 25 0 1 0 549697056 141529088 31940 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34553 31940 603 41 0 34512 0
vsize: 138212
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 32652 0 0 0 67913 94 0 0 25 0 1 0 549697056 142999552 32283 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34912 32283 603 41 0 34871 0
vsize: 139648
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 33040 0 0 0 68912 95 0 0 25 0 1 0 549697056 144605184 32671 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35304 32671 603 41 0 35263 0
vsize: 141216
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 33400 0 0 0 69912 96 0 0 25 0 1 0 549697056 146083840 33031 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35665 33031 603 41 0 35624 0
vsize: 142660
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 33743 0 0 0 70911 96 0 0 25 0 1 0 549697056 147419136 33374 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35991 33374 603 41 0 35950 0
vsize: 143964
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 34115 0 0 0 71910 97 0 0 25 0 1 0 549697056 148910080 33746 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36355 33746 603 41 0 36314 0
vsize: 145420
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 34409 0 0 0 72909 98 0 0 25 0 1 0 549697056 150126592 34040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36652 34040 603 41 0 36611 0
vsize: 146608
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 34768 0 0 0 73909 99 0 0 25 0 1 0 549697056 151613440 34399 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37015 34399 603 41 0 36974 0
vsize: 148060
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 35075 0 0 0 74908 100 0 0 25 0 1 0 549697056 152821760 34706 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37310 34706 603 41 0 37269 0
vsize: 149240
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 35420 0 0 0 75908 100 0 0 25 0 1 0 549697056 154324992 35051 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37677 35051 603 41 0 37636 0
vsize: 150708
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 35826 0 0 0 76907 102 0 0 25 0 1 0 549697056 155971584 35457 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38079 35457 603 41 0 38038 0
vsize: 152316
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 36113 0 0 0 77906 102 0 0 25 0 1 0 549697056 157061120 35744 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38345 35744 603 41 0 38304 0
vsize: 153380
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 36347 0 0 0 78906 103 0 0 25 0 1 0 549697056 158015488 35978 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38578 35978 603 41 0 38537 0
vsize: 154312
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 36683 0 0 0 79904 104 0 0 25 0 1 0 549697056 159494144 36314 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38939 36314 603 41 0 38898 0
vsize: 155756
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 36962 0 0 0 80903 106 0 0 25 0 1 0 549697056 160555008 36593 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39198 36593 603 41 0 39157 0
vsize: 156792
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 37302 0 0 0 81903 106 0 0 25 0 1 0 549697056 161898496 36933 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39526 36933 603 41 0 39485 0
vsize: 158104
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 37523 0 0 0 82902 107 0 0 25 0 1 0 549697056 162840576 37154 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39756 37154 603 41 0 39715 0
vsize: 159024
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 37774 0 0 0 83902 108 0 0 25 0 1 0 549697056 163921920 37405 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40020 37405 603 41 0 39979 0
vsize: 160080
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 37988 0 0 0 84901 109 0 0 25 0 1 0 549697056 164728832 37619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40217 37619 603 41 0 40176 0
vsize: 160868
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 38246 0 0 0 85901 109 0 0 25 0 1 0 549697056 165818368 37877 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40483 37877 603 41 0 40442 0
vsize: 161932
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 38531 0 0 0 86900 110 0 0 25 0 1 0 549697056 167038976 38162 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40781 38162 603 41 0 40740 0
vsize: 163124
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 38868 0 0 0 87899 112 0 0 25 0 1 0 549697056 168382464 38499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41109 38499 603 41 0 41068 0
vsize: 164436
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 39167 0 0 0 88898 113 0 0 25 0 1 0 549697056 169586688 38798 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41403 38798 603 41 0 41362 0
vsize: 165612
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 39407 0 0 0 89898 113 0 0 25 0 1 0 549697056 170524672 39038 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41632 39038 603 41 0 41591 0
vsize: 166528
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 39733 0 0 0 90897 114 0 0 25 0 1 0 549697056 171876352 39364 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41962 39364 603 41 0 41921 0
vsize: 167848
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 39986 0 0 0 91896 115 0 0 25 0 1 0 549697056 172945408 39617 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42223 39617 603 41 0 42182 0
vsize: 168892
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 40283 0 0 0 92896 116 0 0 25 0 1 0 549697056 174149632 39914 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42517 39914 603 41 0 42476 0
vsize: 170068
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 40590 0 0 0 93895 116 0 0 25 0 1 0 549697056 175362048 40221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42813 40221 603 41 0 42772 0
vsize: 171252
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 40854 0 0 0 94895 117 0 0 25 0 1 0 549697056 176422912 40485 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43072 40485 603 41 0 43031 0
vsize: 172288
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 41052 0 0 0 95895 117 0 0 25 0 1 0 549697056 177229824 40683 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43269 40683 603 41 0 43228 0
vsize: 173076
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 41335 0 0 0 96894 118 0 0 25 0 1 0 549697056 178442240 40966 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43565 40966 603 41 0 43524 0
vsize: 174260
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 41612 0 0 0 97894 119 0 0 25 0 1 0 549697056 179523584 41243 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43829 41243 603 41 0 43788 0
vsize: 175316
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 41906 0 0 0 98893 119 0 0 25 0 1 0 549697056 180736000 41537 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44125 41537 603 41 0 44084 0
vsize: 176500
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 42244 0 0 0 99893 120 0 0 25 0 1 0 549697056 182202368 41875 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44483 41875 603 41 0 44442 0
vsize: 177932
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 42530 0 0 0 100892 121 0 0 25 0 1 0 549697056 183803904 42161 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44874 42161 603 41 0 44833 0
vsize: 179496
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 42791 0 0 0 101891 122 0 0 25 0 1 0 549697056 184885248 42422 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45138 42422 603 41 0 45097 0
vsize: 180552
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 42953 0 0 0 102890 123 0 0 25 0 1 0 549697056 185561088 42584 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45303 42584 603 41 0 45262 0
vsize: 181212
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 43151 0 0 0 103890 124 0 0 25 0 1 0 549697056 186372096 42782 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45501 42782 603 41 0 45460 0
vsize: 182004
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 43468 0 0 0 104888 125 0 0 25 0 1 0 549697056 187719680 43099 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45830 43099 603 41 0 45789 0
vsize: 183320
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 43832 0 0 0 105887 126 0 0 25 0 1 0 549697056 189218816 43463 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46196 43463 603 41 0 46155 0
vsize: 184784
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 44104 0 0 0 106886 127 0 0 25 0 1 0 549697056 190283776 43735 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46456 43735 603 41 0 46415 0
vsize: 185824
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 44387 0 0 0 107886 128 0 0 25 0 1 0 549697056 191369216 44018 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46721 44018 603 41 0 46680 0
vsize: 186884
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 44674 0 0 0 108885 129 0 0 25 0 1 0 549697056 192573440 44305 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47015 44305 603 41 0 46974 0
vsize: 188060
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 45118 0 0 0 109883 130 0 0 25 0 1 0 549697056 194457600 44749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47475 44749 603 41 0 47434 0
vsize: 189900
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 45495 0 0 0 110882 132 0 0 25 0 1 0 549697056 195923968 45126 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47833 45126 603 41 0 47792 0
vsize: 191332
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 45723 0 0 0 111881 133 0 0 25 0 1 0 549697056 196861952 45354 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48062 45354 603 41 0 48021 0
vsize: 192248
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 45971 0 0 0 112880 134 0 0 25 0 1 0 549697056 197939200 45602 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48325 45602 603 41 0 48284 0
vsize: 193300
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 46246 0 0 0 113879 135 0 0 25 0 1 0 549697056 199016448 45877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48588 45877 603 41 0 48547 0
vsize: 194352
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 46654 0 0 0 114878 136 0 0 25 0 1 0 549697056 200712192 46285 4294967295 134512640 134672761 3221224544 3221223648 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49002 46285 603 41 0 48961 0
vsize: 196008
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 46872 0 0 0 115878 137 0 0 25 0 1 0 549697056 201515008 46503 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49198 46503 603 41 0 49157 0
vsize: 196792
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 47061 0 0 0 116877 137 0 0 25 0 1 0 549697056 202326016 46692 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49396 46692 603 41 0 49355 0
vsize: 197584
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 47317 0 0 0 117877 138 0 0 25 0 1 0 549697056 203399168 46948 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49658 46948 603 41 0 49617 0
vsize: 198632
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 47515 0 0 0 118876 139 0 0 25 0 1 0 549697056 204218368 47146 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49858 47146 603 41 0 49817 0
vsize: 199432
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7958
Raw data (stat): 7958 (minisat+) R 7957 23176 23175 0 -1 0 47816 0 0 0 119875 140 0 0 25 0 1 0 549697056 205430784 47447 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50154 47447 603 41 0 50113 0
vsize: 200616
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7958
Raw data (stat): 7958 (minisat+) Z 7957 23176 23175 0 -1 12 47818 0 0 0 119875 150 0 0 25 0 1 0 549697056 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.25
CPU user time (s): 1198.75
CPU system time (s): 1.50077
CPU usage (%): 100.01
Max. virtual memory (Kb): 200616
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####