PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-air06.opb
MD5SUM	f85d0079133f298b06c25764b03ff228
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50233
Optimality of the best value was proved	NO
Number of terms in the objective function	8627
Biggest coefficient in the objective function	1859
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	4587852
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	1859
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	4587852
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	1175.81
Number of variables	8627
Total number of constraints	9452
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9452
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	461
Trace number 19290

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        538284 kB
Buffers:         27288 kB
Cached:         447828 kB
SwapCached:        544 kB
Active:          52472 kB
Inactive:       424672 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        538004 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13532 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 19:05:20 (client local time) WITH STATUS 0 IN 1200.5 SECONDS
stats: 16677 7 1200.5 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1628 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1626]---> BDD-cost:  103
c ---[1622]---> BDD-cost:   43
c ---[1618]---> BDD-cost:   59
c ---[1616]---> BDD-cost:   33
c ---[1614]---> BDD-cost:  109
c ---[1612]---> BDD-cost:  113
c ---[1610]---> BDD-cost:   79
c ---[1608]---> BDD-cost:    3
c ---[1604]---> BDD-cost:   41
c ---[1602]---> BDD-cost:   51
c ---[1600]---> BDD-cost:  147
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:   23
c ---[1594]---> BDD-cost:  135
c ---[1592]---> BDD-cost:   81
c ---[1590]---> BDD-cost:   41
c ---[1588]---> BDD-cost:   27
c ---[1586]---> BDD-cost:   25
c ---[1584]---> BDD-cost:    8
c ---[1582]---> BDD-cost:   71
c ---[1580]---> BDD-cost:  137
c ---[1578]---> BDD-cost:   25
c ---[1576]---> BDD-cost:   13
c ---[1574]---> BDD-cost:   27
c ---[1572]---> BDD-cost:    9
c ---[1570]---> BDD-cost:  131
c ---[1566]---> BDD-cost:   47
c ---[1564]---> BDD-cost:   41
c ---[1562]---> BDD-cost:   27
c ---[1560]---> BDD-cost:   35
c ---[1558]---> BDD-cost:  133
c ---[1556]---> BDD-cost:  303
c ---[1554]---> BDD-cost:  231
c ---[1552]---> BDD-cost:  175
c ---[1550]---> BDD-cost:  131
c ---[1548]---> BDD-cost:   89
c ---[1546]---> BDD-cost:   53
c ---[1544]---> BDD-cost:   65
c ---[1542]---> BDD-cost:  141
c ---[1540]---> BDD-cost:  129
c ---[1538]---> BDD-cost:   21
c ---[1536]---> BDD-cost:   13
c ---[1534]---> BDD-cost:   83
c ---[1532]---> BDD-cost:   63
c ---[1530]---> BDD-cost:    7
c ---[1528]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   41
c ---[1522]---> BDD-cost:   93
c ---[1520]---> BDD-cost:   55
c ---[1518]---> BDD-cost:   27
c ---[1516]---> BDD-cost:  253
c ---[1514]---> BDD-cost:  189
c ---[1512]---> BDD-cost:  131
c ---[1510]---> BDD-cost:  143
c ---[1508]---> BDD-cost:   55
c ---[1506]---> BDD-cost:  105
c ---[1504]---> BDD-cost:  357
c ---[1502]---> BDD-cost:  355
c ---[1500]---> BDD-cost:  361
c ---[1498]---> BDD-cost:  257
c ---[1496]---> BDD-cost:  263
c ---[1494]---> BDD-cost:  271
c ---[1492]---> BDD-cost:   91
c ---[1488]---> BDD-cost:   15
c ---[1486]---> BDD-cost:    7
c ---[1484]---> BDD-cost:   37
c ---[1478]---> BDD-cost:    1
c ---[1476]---> BDD-cost:   14
c ---[1474]---> BDD-cost:    7
c ---[1472]---> BDD-cost:    1
c ---[1470]---> BDD-cost:    1
c ---[1468]---> BDD-cost:    5
c ---[1466]---> BDD-cost:  103
c ---[1464]---> BDD-cost:  203
c ---[1462]---> BDD-cost:   91
c ---[1460]---> BDD-cost:   49
c ---[1458]---> BDD-cost:    7
c ---[1456]---> BDD-cost:   77
c ---[1452]---> BDD-cost:   55
c ---[1450]---> BDD-cost:   19
c ---[1448]---> BDD-cost:   95
c ---[1446]---> BDD-cost:  101
c ---[1444]---> BDD-cost:  115
c ---[1442]---> BDD-cost:   67
c ---[1440]---> BDD-cost:   33
c ---[1438]---> BDD-cost:   29
c ---[1436]---> BDD-cost:   91
c ---[1434]---> BDD-cost:   25
c ---[1428]---> BDD-cost:   11
c ---[1426]---> BDD-cost:   15
c ---[1424]---> BDD-cost:   29
c ---[1422]---> BDD-cost:  127
c ---[1420]---> BDD-cost:  195
c ---[1418]---> BDD-cost:  143
c ---[1416]---> BDD-cost:  111
c ---[1414]---> BDD-cost:  169
c ---[1412]---> BDD-cost:  169
c ---[1410]---> BDD-cost:  171
c ---[1408]---> BDD-cost:  135
c ---[1406]---> BDD-cost:   43
c ---[1404]---> BDD-cost:  257
c ---[1402]---> BDD-cost:  261
c ---[1400]---> BDD-cost:  167
c ---[1398]---> BDD-cost:  125
c ---[1396]---> BDD-cost:  125
c ---[1394]---> BDD-cost:   39
c ---[1392]---> BDD-cost:   37
c ---[1390]---> BDD-cost:   43
c ---[1386]---> BDD-cost:   29
c ---[1384]---> BDD-cost:   33
c ---[1382]---> BDD-cost:  107
c ---[1380]---> BDD-cost:   57
c ---[1378]---> BDD-cost:  169
c ---[1376]---> BDD-cost:   79
c ---[1374]---> BDD-cost:   81
c ---[1372]---> BDD-cost:  219
c ---[1370]---> BDD-cost:  229
c ---[1368]---> BDD-cost:  111
c ---[1366]---> BDD-cost:    5
c ---[1364]---> BDD-cost:   89
c ---[1362]---> BDD-cost:  389
c ---[1360]---> BDD-cost:  335
c ---[1358]---> BDD-cost:  191
c ---[1356]---> BDD-cost:  121
c ---[1354]---> BDD-cost:  137
c ---[1352]---> BDD-cost:   83
c ---[1350]---> BDD-cost:  199
c ---[1348]---> BDD-cost:   15
c ---[1346]---> BDD-cost:  109
c ---[1344]---> BDD-cost:   55
c ---[1342]---> BDD-cost:  181
c ---[1340]---> BDD-cost:  133
c ---[1338]---> BDD-cost:   81
c ---[1336]---> BDD-cost:   33
c ---[1334]---> BDD-cost:  131
c ---[1332]---> BDD-cost:   75
c ---[1330]---> BDD-cost:   49
c ---[1328]---> BDD-cost:   17
c ---[1326]---> BDD-cost:   97
c ---[1324]---> BDD-cost:  129
c ---[1322]---> BDD-cost:   69
c ---[1320]---> BDD-cost:  273
c ---[1318]---> BDD-cost:  261
c ---[1316]---> BDD-cost:   89
c ---[1314]---> BDD-cost:  119
c ---[1312]---> BDD-cost:   53
c ---[1310]---> BDD-cost:   43
c ---[1308]---> BDD-cost:   61
c ---[1306]---> BDD-cost:   99
c ---[1304]---> BDD-cost:   81
c ---[1302]---> BDD-cost:  165
c ---[1300]---> BDD-cost:  231
c ---[1298]---> BDD-cost:  121
c ---[1296]---> BDD-cost:  135
c ---[1294]---> BDD-cost:  227
c ---[1292]---> BDD-cost:   35
c ---[1290]---> BDD-cost:   55
c ---[1288]---> BDD-cost:  143
c ---[1286]---> BDD-cost:  135
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  177
c ---[1280]---> BDD-cost:  151
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  179
c ---[1274]---> BDD-cost:   61
c ---[1272]---> BDD-cost:  167
c ---[1270]---> BDD-cost:  145
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:  243
c ---[1264]---> BDD-cost:   15
c ---[1262]---> BDD-cost:  137
c ---[1260]---> BDD-cost:   85
c ---[1258]---> BDD-cost:   37
c ---[1254]---> BDD-cost:   43
c ---[1252]---> BDD-cost:   19
c ---[1250]---> BDD-cost:   23
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   91
c ---[1244]---> BDD-cost:   95
c ---[1242]---> BDD-cost:   61
c ---[1240]---> BDD-cost:   79
c ---[1238]---> BDD-cost:   89
c ---[1236]---> BDD-cost:  105
c ---[1234]---> BDD-cost:   97
c ---[1232]---> BDD-cost:  105
c ---[1230]---> BDD-cost:   81
c ---[1228]---> BDD-cost:   19
c ---[1226]---> BDD-cost:   13
c ---[1224]---> BDD-cost:    3
c ---[1222]---> BDD-cost:   21
c ---[1220]---> BDD-cost:   65
c ---[1218]---> BDD-cost:   35
c ---[1216]---> BDD-cost:   69
c ---[1214]---> BDD-cost:   45
c ---[1212]---> BDD-cost:   59
c ---[1210]---> BDD-cost:   89
c ---[1208]---> BDD-cost:   65
c ---[1206]---> BDD-cost:  101
c ---[1204]---> BDD-cost:   87
c ---[1202]---> BDD-cost:   95
c ---[1200]---> BDD-cost:   69
c ---[1198]---> BDD-cost:  119
c ---[1196]---> BDD-cost:   53
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   27
c ---[1190]---> BDD-cost:  273
c ---[1188]---> BDD-cost:  231
c ---[1186]---> BDD-cost:  243
c ---[1184]---> BDD-cost:  121
c ---[1182]---> BDD-cost:  295
c ---[1180]---> BDD-cost:  175
c ---[1178]---> BDD-cost:  115
c ---[1176]---> BDD-cost:  175
c ---[1174]---> BDD-cost:  249
c ---[1172]---> BDD-cost:  233
c ---[1170]---> BDD-cost:  123
c ---[1168]---> BDD-cost:   81
c ---[1166]---> BDD-cost:    5
c ---[1164]---> BDD-cost:   75
c ---[1162]---> BDD-cost:   71
c ---[1160]---> BDD-cost:   39
c ---[1156]---> BDD-cost:   65
c ---[1154]---> BDD-cost:   51
c ---[1152]---> BDD-cost:   21
c ---[1150]---> BDD-cost:   15
c ---[1148]---> BDD-cost:    3
c ---[1146]---> BDD-cost:   21
c ---[1144]---> BDD-cost:   17
c ---[1142]---> BDD-cost:   33
c ---[1140]---> BDD-cost:   11
c ---[1138]---> BDD-cost:   29
c ---[1136]---> BDD-cost:   95
c ---[1134]---> BDD-cost:   79
c ---[1132]---> BDD-cost:   37
c ---[1130]---> BDD-cost:  273
c ---[1128]---> BDD-cost:  221
c ---[1126]---> BDD-cost:  189
c ---[1124]---> BDD-cost:   81
c ---[1122]---> BDD-cost:   35
c ---[1120]---> BDD-cost:  185
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   59
c ---[1114]---> BDD-cost:   59
c ---[1112]---> BDD-cost:  125
c ---[1110]---> BDD-cost:  135
c ---[1108]---> BDD-cost:  117
c ---[1096]---> BDD-cost:   73
c ---[1094]---> BDD-cost:   95
c ---[1092]---> BDD-cost:   53
c ---[1090]---> BDD-cost:  117
c ---[1088]---> BDD-cost:  117
c ---[1086]---> BDD-cost:  199
c ---[1084]---> BDD-cost:  189
c ---[1082]---> BDD-cost:   25
c ---[1080]---> BDD-cost:  173
c ---[1078]---> BDD-cost:   45
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:  219
c ---[1070]---> BDD-cost:  167
c ---[1068]---> BDD-cost:  121
c ---[1066]---> BDD-cost:  203
c ---[1064]---> BDD-cost:   27
c ---[1062]---> BDD-cost:   17
c ---[1060]---> BDD-cost:   87
c ---[1058]---> BDD-cost:  111
c ---[1056]---> BDD-cost:  169
c ---[1054]---> BDD-cost:  251
c ---[1052]---> BDD-cost:  155
c ---[1048]---> BDD-cost:   93
c ---[1044]---> BDD-cost:  141
c ---[1042]---> BDD-cost:  103
c ---[1040]---> BDD-cost:  173
c ---[1038]---> BDD-cost:  221
c ---[1036]---> BDD-cost:  199
c ---[1034]---> BDD-cost:  185
c ---[1032]---> BDD-cost:  259
c ---[1030]---> BDD-cost:  129
c ---[1028]---> BDD-cost:  283
c ---[1026]---> BDD-cost:  187
c ---[1024]---> BDD-cost:  187
c ---[1022]---> BDD-cost:  173
c ---[1018]---> BDD-cost:   55
c ---[1014]---> BDD-cost:   37
c ---[1012]---> BDD-cost:   59
c ---[1010]---> BDD-cost:   57
c ---[1008]---> BDD-cost:   49
c ---[1004]---> BDD-cost:    1
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   91
c ---[ 998]---> BDD-cost:  137
c ---[ 996]---> BDD-cost:   77
c ---[ 994]---> BDD-cost:  125
c ---[ 992]---> BDD-cost:   49
c ---[ 990]---> BDD-cost:  103
c ---[ 988]---> BDD-cost:  119
c ---[ 986]---> BDD-cost:   81
c ---[ 984]---> BDD-cost:  121
c ---[ 982]---> BDD-cost:  127
c ---[ 980]---> BDD-cost:   25
c ---[ 978]---> BDD-cost:  139
c ---[ 976]---> BDD-cost:   73
c ---[ 974]---> BDD-cost:  113
c ---[ 972]---> BDD-cost:   77
c ---[ 970]---> BDD-cost:   69
c ---[ 968]---> BDD-cost:   53
c ---[ 966]---> BDD-cost:   33
c ---[ 962]---> BDD-cost:   65
c ---[ 960]---> BDD-cost:   65
c ---[ 958]---> BDD-cost:  213
c ---[ 956]---> BDD-cost:  247
c ---[ 954]---> BDD-cost:  273
c ---[ 952]---> BDD-cost:  145
c ---[ 950]---> BDD-cost:  535
c ---[ 948]---> BDD-cost:  659
c ---[ 946]---> BDD-cost:  259
c ---[ 944]---> BDD-cost:  213
c ---[ 942]---> BDD-cost:  157
c ---[ 940]---> BDD-cost:   65
c ---[ 938]---> BDD-cost:  561
c ---[ 936]---> BDD-cost:  117
c ---[ 932]---> BDD-cost:  153
c ---[ 930]---> BDD-cost:  113
c ---[ 928]---> BDD-cost:  119
c ---[ 926]---> BDD-cost:   99
c ---[ 922]---> BDD-cost:    6
c ---[ 920]---> BDD-cost:  113
c ---[ 918]---> BDD-cost:   75
c ---[ 914]---> BDD-cost:   17
c ---[ 912]---> BDD-cost:  149
c ---[ 910]---> BDD-cost:   63
c ---[ 908]---> BDD-cost:   41
c ---[ 906]---> BDD-cost:  135
c ---[ 904]---> BDD-cost:   99
c ---[ 902]---> BDD-cost:   99
c ---[ 900]---> BDD-cost:   65
c ---[ 898]---> BDD-cost:  333
c ---[ 896]---> BDD-cost:   93
c ---[ 894]---> BDD-cost:  407
c ---[ 892]---> BDD-cost:  393
c ---[ 890]---> BDD-cost:  349
c ---[ 888]---> BDD-cost:  189
c ---[ 886]---> BDD-cost:  225
c ---[ 884]---> BDD-cost:  115
c ---[ 882]---> BDD-cost:  117
c ---[ 880]---> BDD-cost:   57
c ---[ 878]---> BDD-cost:  109
c ---[ 876]---> BDD-cost:  219
c ---[ 874]---> BDD-cost:  139
c ---[ 872]---> BDD-cost:  239
c ---[ 870]---> BDD-cost:   65
c ---[ 868]---> BDD-cost:   39
c ---[ 866]---> BDD-cost:   59
c ---[ 862]---> BDD-cost:    9
c ---[ 860]---> BDD-cost:  239
c ---[ 858]---> BDD-cost:  165
c ---[ 856]---> BDD-cost:  207
c ---[ 854]---> BDD-cost:  219
c ---[ 852]---> BDD-cost:  391
c ---[ 850]---> BDD-cost:  315
c ---[ 848]---> BDD-cost:  147
c ---[ 846]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:  187
c ---[ 842]---> BDD-cost:  311
c ---[ 840]---> BDD-cost:  187
c ---[ 838]---> BDD-cost:  195
c ---[ 836]---> BDD-cost:  117
c ---[ 834]---> BDD-cost:  111
c ---[ 830]---> BDD-cost:   91
c ---[ 828]---> BDD-cost:  333
c ---[ 826]---> BDD-cost:  207
c ---[ 822]---> BDD-cost:  253
c ---[ 820]---> BDD-cost:   77
c ---[ 818]---> BDD-cost:   77
c ---[ 816]---> BDD-cost:  191
c ---[ 814]---> BDD-cost:  153
c ---[ 812]---> BDD-cost:  255
c ---[ 810]---> BDD-cost:  189
c ---[ 808]---> BDD-cost:   17
c ---[ 806]---> BDD-cost:   39
c ---[ 802]---> BDD-cost:  187
c ---[ 800]---> BDD-cost:  117
c ---[ 798]---> BDD-cost:   49
c ---[ 796]---> BDD-cost:   37
c ---[ 794]---> BDD-cost:   61
c ---[ 792]---> BDD-cost:   33
c ---[ 790]---> BDD-cost:    0
c ---[ 788]---> BDD-cost:   83
c ---[ 786]---> BDD-cost:   73
c ---[ 784]---> BDD-cost:   91
c ---[ 782]---> BDD-cost:   55
c ---[ 780]---> BDD-cost:  105
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  345
c ---[ 774]---> BDD-cost:  295
c ---[ 772]---> BDD-cost:  101
c ---[ 770]---> BDD-cost:   21
c ---[ 768]---> BDD-cost:   71
c ---[ 766]---> BDD-cost:   77
c ---[ 764]---> BDD-cost:   61
c ---[ 762]---> BDD-cost:   53
c ---[ 760]---> BDD-cost:  199
c ---[ 758]---> BDD-cost:  195
c ---[ 756]---> BDD-cost:  155
c ---[ 754]---> BDD-cost:   29
c ---[ 752]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:  133
c ---[ 748]---> BDD-cost:   65
c ---[ 746]---> BDD-cost:   57
c ---[ 744]---> BDD-cost:  157
c ---[ 742]---> BDD-cost:  345
c ---[ 740]---> BDD-cost:  201
c ---[ 738]---> BDD-cost:  205
c ---[ 736]---> BDD-cost:  151
c ---[ 734]---> BDD-cost:  135
c ---[ 732]---> BDD-cost:   73
c ---[ 730]---> BDD-cost:  161
c ---[ 728]---> BDD-cost:  181
c ---[ 726]---> BDD-cost:  177
c ---[ 724]---> BDD-cost:  293
c ---[ 722]---> BDD-cost:  279
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  145
c ---[ 716]---> BDD-cost:  289
c ---[ 714]---> BDD-cost:  163
c ---[ 712]---> BDD-cost:  181
c ---[ 710]---> BDD-cost:  141
c ---[ 708]---> BDD-cost:  115
c ---[ 706]---> BDD-cost:  123
c ---[ 704]---> BDD-cost:  189
c ---[ 702]---> BDD-cost:  139
c ---[ 700]---> BDD-cost:   63
c ---[ 698]---> BDD-cost:  473
c ---[ 696]---> BDD-cost:  429
c ---[ 694]---> BDD-cost:  285
c ---[ 692]---> BDD-cost:    9
c ---[ 690]---> BDD-cost:    5
c ---[ 688]---> BDD-cost:    0
c ---[ 686]---> BDD-cost:    3
c ---[ 684]---> BDD-cost:    4
c ---[ 680]---> BDD-cost:  155
c ---[ 678]---> BDD-cost:  127
c ---[ 676]---> BDD-cost:  109
c ---[ 674]---> BDD-cost:  273
c ---[ 672]---> BDD-cost:   63
c ---[ 670]---> BDD-cost:   45
c ---[ 668]---> BDD-cost:   23
c ---[ 666]---> BDD-cost:   29
c ---[ 664]---> BDD-cost:  245
c ---[ 662]---> BDD-cost:  227
c ---[ 660]---> BDD-cost:   49
c ---[ 658]---> BDD-cost:    9
c ---[ 656]---> BDD-cost:    0
c ---[ 654]---> BDD-cost:  149
c ---[ 652]---> BDD-cost:  183
c ---[ 650]---> BDD-cost:  119
c ---[ 648]---> BDD-cost:  107
c ---[ 646]---> BDD-cost:  235
c ---[ 644]---> BDD-cost:  227
c ---[ 642]---> BDD-cost:  239
c ---[ 640]---> BDD-cost:  269
c ---[ 638]---> BDD-cost:  615
c ---[ 636]---> BDD-cost:  441
c ---[ 634]---> BDD-cost:  231
c ---[ 632]---> BDD-cost:  123
c ---[ 630]---> BDD-cost:  547
c ---[ 628]---> BDD-cost:  543
c ---[ 626]---> BDD-cost:  357
c ---[ 624]---> BDD-cost:  237
c ---[ 620]---> BDD-cost:  327
c ---[ 618]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:  287
c ---[ 614]---> BDD-cost:  205
c ---[ 612]---> BDD-cost:  177
c ---[ 610]---> BDD-cost:  313
c ---[ 608]---> BDD-cost:   57
c ---[ 606]---> BDD-cost:   61
c ---[ 604]---> BDD-cost:   45
c ---[ 602]---> BDD-cost:   35
c ---[ 600]---> BDD-cost:  133
c ---[ 598]---> BDD-cost:  107
c ---[ 596]---> BDD-cost:   91
c ---[ 594]---> BDD-cost:   93
c ---[ 592]---> BDD-cost:   35
c ---[ 590]---> BDD-cost:  187
c ---[ 588]---> BDD-cost:  573
c ---[ 586]---> BDD-cost:  305
c ---[ 584]---> BDD-cost:  607
c ---[ 582]---> BDD-cost:  443
c ---[ 580]---> BDD-cost:  213
c ---[ 578]---> BDD-cost:  213
c ---[ 576]---> BDD-cost:  167
c ---[ 574]---> BDD-cost:    4
c ---[ 572]---> BDD-cost:  283
c ---[ 570]---> BDD-cost:  277
c ---[ 568]---> BDD-cost:  125
c ---[ 566]---> BDD-cost:   85
c ---[ 564]---> BDD-cost:   81
c ---[ 562]---> BDD-cost:  403
c ---[ 560]---> BDD-cost:  391
c ---[ 558]---> BDD-cost:  175
c ---[ 556]---> BDD-cost:  159
c ---[ 554]---> BDD-cost:  155
c ---[ 552]---> BDD-cost:  101
c ---[ 550]---> BDD-cost:  155
c ---[ 548]---> BDD-cost:  165
c ---[ 546]---> BDD-cost:  153
c ---[ 544]---> BDD-cost:  135
c ---[ 542]---> BDD-cost:   81
c ---[ 540]---> BDD-cost:  167
c ---[ 538]---> BDD-cost:   27
c ---[ 536]---> BDD-cost:  147
c ---[ 534]---> BDD-cost:  155
c ---[ 532]---> BDD-cost:  173
c ---[ 530]---> BDD-cost:  267
c ---[ 528]---> BDD-cost:  157
c ---[ 526]---> BDD-cost:   91
c ---[ 524]---> BDD-cost:  259
c ---[ 522]---> BDD-cost:  117
c ---[ 520]---> BDD-cost:  121
c ---[ 518]---> BDD-cost:  323
c ---[ 516]---> BDD-cost:  325
c ---[ 514]---> BDD-cost:  311
c ---[ 512]---> BDD-cost:  313
c ---[ 510]---> BDD-cost:  247
c ---[ 508]---> BDD-cost:  297
c ---[ 506]---> BDD-cost:  211
c ---[ 504]---> BDD-cost:  369
c ---[ 500]---> BDD-cost:  305
c ---[ 498]---> BDD-cost:  341
c ---[ 496]---> BDD-cost:  285
c ---[ 494]---> BDD-cost:   77
c ---[ 492]---> BDD-cost:  317
c ---[ 490]---> BDD-cost:  275
c ---[ 488]---> BDD-cost:  423
c ---[ 486]---> BDD-cost:  403
c ---[ 484]---> BDD-cost:  307
c ---[ 482]---> BDD-cost:  327
c ---[ 480]---> BDD-cost:  307
c ---[ 478]---> BDD-cost:  315
c ---[ 476]---> BDD-cost:  297
c ---[ 474]---> BDD-cost:  273
c ---[ 472]---> BDD-cost:  701
c ---[ 470]---> BDD-cost:  289
c ---[ 468]---> BDD-cost:  245
c ---[ 466]---> BDD-cost:  385
c ---[ 464]---> BDD-cost:  363
c ---[ 462]---> BDD-cost:   27
c ---[ 458]---> BDD-cost:  145
c ---[ 456]---> BDD-cost:  147
c ---[ 454]---> BDD-cost:  149
c ---[ 452]---> BDD-cost:  125
c ---[ 450]---> BDD-cost:  147
c ---[ 448]---> BDD-cost:  111
c ---[ 446]---> BDD-cost:  319
c ---[ 444]---> BDD-cost:  309
c ---[ 438]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:    7
c ---[ 434]---> BDD-cost:  399
c ---[ 432]---> BDD-cost:  401
c ---[ 430]---> BDD-cost:  371
c ---[ 426]---> BDD-cost:   65
c ---[ 422]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:   15
c ---[ 416]---> BDD-cost:  453
c ---[ 414]---> BDD-cost:  457
c ---[ 412]---> BDD-cost:  197
c ---[ 410]---> BDD-cost:  123
c ---[ 408]---> BDD-cost:  165
c ---[ 404]---> BDD-cost:  335
c ---[ 402]---> BDD-cost:  169
c ---[ 400]---> BDD-cost:  209
c ---[ 398]---> BDD-cost:   61
c ---[ 396]---> BDD-cost:   17
c ---[ 394]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:   41
c ---[ 388]---> BDD-cost:  229
c ---[ 386]---> BDD-cost:  231
c ---[ 384]---> BDD-cost:  223
c ---[ 378]---> BDD-cost:  319
c ---[ 376]---> BDD-cost:  223
c ---[ 374]---> BDD-cost:  241
c ---[ 372]---> BDD-cost:  245
c ---[ 370]---> BDD-cost:  229
c ---[ 368]---> BDD-cost:  109
c ---[ 366]---> BDD-cost:   73
c ---[ 364]---> BDD-cost:   85
c ---[ 362]---> BDD-cost:   99
c ---[ 360]---> BDD-cost:  103
c ---[ 358]---> BDD-cost:    5
c ---[ 356]---> BDD-cost:  201
c ---[ 354]---> BDD-cost:  215
c ---[ 352]---> BDD-cost:  197
c ---[ 348]---> BDD-cost:  139
c ---[ 344]---> BDD-cost:   83
c ---[ 340]---> BDD-cost:  125
c ---[ 338]---> BDD-cost:  225
c ---[ 336]---> BDD-cost:  181
c ---[ 334]---> BDD-cost:  151
c ---[ 332]---> BDD-cost:  243
c ---[ 330]---> BDD-cost:  179
c ---[ 328]---> BDD-cost:  207
c ---[ 326]---> BDD-cost:  145
c ---[ 324]---> BDD-cost:   21
c ---[ 322]---> BDD-cost:  235
c ---[ 320]---> BDD-cost:  209
c ---[ 318]---> BDD-cost:   55
c ---[ 316]---> BDD-cost:  223
c ---[ 314]---> BDD-cost:  193
c ---[ 312]---> BDD-cost:  173
c ---[ 310]---> BDD-cost:   63
c ---[ 308]---> BDD-cost:   87
c ---[ 306]---> BDD-cost:   87
c ---[ 304]---> BDD-cost:   33
c ---[ 302]---> BDD-cost:  135
c ---[ 300]---> BDD-cost:   75
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  233
c ---[ 294]---> BDD-cost:  211
c ---[ 292]---> BDD-cost:  119
c ---[ 290]---> BDD-cost:  269
c ---[ 288]---> BDD-cost:   51
c ---[ 286]---> BDD-cost:  205
c ---[ 284]---> BDD-cost:  233
c ---[ 282]---> BDD-cost:  207
c ---[ 280]---> BDD-cost:  243
c ---[ 278]---> BDD-cost:  453
c ---[ 276]---> BDD-cost:  465
c ---[ 274]---> BDD-cost:  259
c ---[ 272]---> BDD-cost:  227
c ---[ 270]---> BDD-cost:  359
c ---[ 268]---> BDD-cost:  209
c ---[ 266]---> BDD-cost:  319
c ---[ 264]---> BDD-cost:  287
c ---[ 262]---> BDD-cost:  225
c ---[ 260]---> BDD-cost:  227
c ---[ 258]---> BDD-cost:  445
c ---[ 256]---> BDD-cost:  339
c ---[ 254]---> BDD-cost:  343
c ---[ 252]---> BDD-cost:  105
c ---[ 250]---> BDD-cost:   73
c ---[ 248]---> BDD-cost:   89
c ---[ 246]---> BDD-cost:  109
c ---[ 242]---> BDD-cost:  597
c ---[ 240]---> BDD-cost:  303
c ---[ 238]---> BDD-cost:  253
c ---[ 236]---> BDD-cost:  133
c ---[ 234]---> BDD-cost:  119
c ---[ 232]---> BDD-cost:   99
c ---[ 230]---> BDD-cost:  119
c ---[ 228]---> BDD-cost:   67
c ---[ 226]---> BDD-cost:  145
c ---[ 224]---> BDD-cost:  135
c ---[ 222]---> BDD-cost:  217
c ---[ 220]---> BDD-cost:  211
c ---[ 218]---> BDD-cost:  141
c ---[ 214]---> BDD-cost:  167
c ---[ 212]---> BDD-cost:  191
c ---[ 210]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  175
c ---[ 206]---> BDD-cost:  147
c ---[ 204]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:  389
c ---[ 200]---> BDD-cost:  349
c ---[ 198]---> BDD-cost:  151
c ---[ 196]---> BDD-cost:  151
c ---[ 194]---> BDD-cost:  307
c ---[ 192]---> BDD-cost:  355
c ---[ 190]---> BDD-cost:  269
c ---[ 188]---> BDD-cost:  267
c ---[ 186]---> BDD-cost:  327
c ---[ 184]---> BDD-cost:  347
c ---[ 182]---> BDD-cost:  187
c ---[ 180]---> BDD-cost:  117
c ---[ 178]---> BDD-cost:   37
c ---[ 176]---> BDD-cost:   17
c ---[ 174]---> BDD-cost:  171
c ---[ 170]---> BDD-cost:  339
c ---[ 168]---> BDD-cost:  429
c ---[ 166]---> BDD-cost:  443
c ---[ 164]---> BDD-cost:  419
c ---[ 162]---> BDD-cost:  465
c ---[ 160]---> BDD-cost:  379
c ---[ 158]---> BDD-cost:  307
c ---[ 156]---> BDD-cost:  907
c ---[ 154]---> BDD-cost:  439
c ---[ 152]---> BDD-cost:  303
c ---[ 150]---> BDD-cost:  239
c ---[ 148]---> BDD-cost:  219
c ---[ 146]---> BDD-cost:  261
c ---[ 144]---> BDD-cost:  247
c ---[ 142]---> BDD-cost:  265
c ---[ 140]---> BDD-cost:  273
c ---[ 138]---> BDD-cost:  673
c ---[ 136]---> BDD-cost:  433
c ---[ 134]---> BDD-cost:  317
c ---[ 132]---> BDD-cost:  187
c ---[ 130]---> BDD-cost:  199
c ---[ 128]---> BDD-cost:  155
c ---[ 126]---> BDD-cost:  105
c ---[ 124]---> BDD-cost:   31
c ---[ 122]---> BDD-cost:  117
c ---[ 120]---> BDD-cost:  107
c ---[ 118]---> BDD-cost:  141
c ---[ 116]---> BDD-cost:  165
c ---[ 114]---> BDD-cost:  221
c ---[ 110]---> BDD-cost:  163
c ---[ 108]---> BDD-cost:  179
c ---[ 106]---> BDD-cost:  139
c ---[ 104]---> BDD-cost:   83
c ---[ 102]---> BDD-cost:   67
c ---[ 100]---> BDD-cost:   87
c ---[  98]---> BDD-cost:   31
c ---[  96]---> BDD-cost:   23
c ---[  94]---> BDD-cost:   31
c ---[  92]---> BDD-cost:   91
c ---[  90]---> BDD-cost:  431
c ---[  88]---> BDD-cost:  203
c ---[  86]---> BDD-cost:  565
c ---[  84]---> BDD-cost:  611
c ---[  82]---> BDD-cost:  347
c ---[  80]---> BDD-cost:  175
c ---[  78]---> BDD-cost:  525
c ---[  76]---> BDD-cost:  505
c ---[  74]---> BDD-cost:   57
c ---[  72]---> BDD-cost:   45
c ---[  70]---> BDD-cost:   57
c ---[  68]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   55
c ---[  64]---> BDD-cost:   57
c ---[  62]---> BDD-cost:   57
c ---[  60]---> BDD-cost:  159
c ---[  58]---> BDD-cost:   71
c ---[  56]---> BDD-cost:  199
c ---[  54]---> BDD-cost:  191
c ---[  52]---> BDD-cost:  225
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:  509
c ---[  46]---> BDD-cost:  321
c ---[  44]---> BDD-cost:  333
c ---[  42]---> BDD-cost:  407
c ---[  40]---> BDD-cost:  191
c ---[  38]---> BDD-cost:  135
c ---[  36]---> BDD-cost:  379
c ---[  34]---> BDD-cost:  365
c ---[  32]---> BDD-cost:   63
c ---[  30]---> BDD-cost:   31
c ---[  28]---> BDD-cost:   33
c ---[  26]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   31
c ---[  18]---> BDD-cost:   47
c ---[  16]---> BDD-cost:  139
c ---[  14]---> BDD-cost:    9
c ---[  12]---> BDD-cost:  135
c ---[  10]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   53
c ---[   6]---> BDD-cost:  129
c ---[   4]---> BDD-cost:    7
c ---[   2]---> BDD-cost:  119
c ---[   0]---> BDD-cost:   85
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  297939   775413 |   89381       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/126968          
c   -- var.elim.:  2000/126968          
c   -- var.elim.:  3000/126968          
c   -- var.elim.:  4000/126968          
c   -- var.elim.:  5000/126968          
c   -- var.elim.:  6000/126968          
c   -- var.elim.:  7000/126968          
c   -- var.elim.:  8000/126968          
c   -- var.elim.:  9000/126968          
c   -- var.elim.:  10000/126968          
c   -- var.elim.:  11000/126968          
c   -- var.elim.:  12000/126968          
c   -- var.elim.:  13000/126968          
c   -- var.elim.:  14000/126968          
c   -- var.elim.:  15000/126968          
c   -- var.elim.:  16000/126968          
c   -- var.elim.:  17000/126968          
c   -- var.elim.:  18000/126968          
c   -- var.elim.:  19000/126968          
c   -- var.elim.:  20000/126968          
c   -- var.elim.:  21000/126968          
c   -- var.elim.:  22000/126968          
c   -- var.elim.:  23000/126968          
c   -- var.elim.:  24000/126968          
c   -- var.elim.:  25000/126968          
c   -- var.elim.:  26000/126968          
c   -- var.elim.:  27000/126968          
c   -- var.elim.:  28000/126968          
c   -- var.elim.:  29000/126968          
c   -- var.elim.:  30000/126968          
c   -- var.elim.:  31000/126968          
c   -- var.elim.:  32000/126968          
c   -- var.elim.:  33000/126968          
c   -- var.elim.:  34000/126968          
c   -- var.elim.:  35000/126968          
c   -- var.elim.:  36000/126968          
c   -- var.elim.:  37000/126968          
c   -- var.elim.:  38000/126968          
c   -- var.elim.:  39000/126968          
c   -- var.elim.:  40000/126968          
c   -- var.elim.:  41000/126968          
c   -- var.elim.:  42000/126968          
c   -- var.elim.:  43000/126968          
c   -- var.elim.:  44000/126968          
c   -- var.elim.:  45000/126968          
c   -- var.elim.:  46000/126968          
c   -- var.elim.:  47000/126968          
c   -- var.elim.:  48000/126968          
c   -- var.elim.:  49000/126968          
c   -- var.elim.:  50000/126968          
c   -- var.elim.:  51000/126968          
c   -- var.elim.:  52000/126968          
c   -- var.elim.:  53000/126968          
c   -- var.elim.:  54000/126968          
c   -- var.elim.:  55000/126968          
c   -- var.elim.:  56000/126968          
c   -- var.elim.:  57000/126968          
c   -- var.elim.:  58000/126968          
c   -- var.elim.:  59000/126968          
c   -- var.elim.:  60000/126968          
c   -- var.elim.:  61000/126968          
c   -- var.elim.:  62000/126968          
c   -- var.elim.:  63000/126968          
c   -- var.elim.:  64000/126968          
c   -- var.elim.:  65000/126968          
c   -- var.elim.:  66000/126968          
c   -- var.elim.:  67000/126968          
c   -- var.elim.:  68000/126968          
c   -- var.elim.:  69000/126968          
c   -- var.elim.:  70000/126968          
c   -- var.elim.:  71000/126968          
c   -- var.elim.:  72000/126968          
c   -- var.elim.:  73000/126968          
c   -- var.elim.:  74000/126968          
c   -- var.elim.:  75000/126968          
c   -- var.elim.:  76000/126968          
c   -- var.elim.:  77000/126968          
c   -- var.elim.:  78000/126968          
c   -- var.elim.:  79000/126968          
c   -- var.elim.:  80000/126968          
c   -- var.elim.:  81000/126968          
c   -- var.elim.:  82000/126968          
c   -- var.elim.:  83000/126968          
c   -- var.elim.:  84000/126968          
c   -- var.el#### 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.59 0.88 0.88 2/54 22362
Raw data (stat): 22362 (runsolver) R 22361 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489120502 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99973 s]
Raw data (loadavg): 0.65 0.88 0.88 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 20005 0 0 0 944 54 0 0 25 0 1 0 489120502 78843904 17828 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19249 17828 603 41 0 19208 0
vsize: 76996
[startup+20.0001 s]
Raw data (loadavg): 0.70 0.88 0.88 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 20181 0 0 0 1944 54 0 0 25 0 1 0 489120502 79761408 17971 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19473 17971 603 41 0 19432 0
vsize: 77892
[startup+30.0002 s]
Raw data (loadavg): 0.75 0.89 0.88 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 20447 0 0 0 2943 55 0 0 25 0 1 0 489120502 80949248 18237 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19763 18237 603 41 0 19722 0
vsize: 79052
[startup+40.0001 s]
Raw data (loadavg): 0.79 0.89 0.88 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 20632 0 0 0 3943 56 0 0 25 0 1 0 489120502 81612800 18422 4294967295 134512640 134672761 3221224544 3221223728 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19925 18422 603 41 0 19884 0
vsize: 79700
[startup+50.0006 s]
Raw data (loadavg): 0.82 0.89 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 20787 0 0 0 4943 56 0 0 25 0 1 0 489120502 82313216 18577 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20096 18577 603 41 0 20055 0
vsize: 80384
[startup+60.0007 s]
Raw data (loadavg): 0.85 0.90 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 21035 0 0 0 5942 58 0 0 25 0 1 0 489120502 83374080 18825 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20355 18825 603 41 0 20314 0
vsize: 81420
[startup+70.0005 s]
Raw data (loadavg): 0.87 0.90 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 21264 0 0 0 6941 58 0 0 25 0 1 0 489120502 84287488 19054 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20578 19054 603 41 0 20537 0
vsize: 82312
[startup+80.001 s]
Raw data (loadavg): 0.89 0.90 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 21542 0 0 0 7941 59 0 0 25 0 1 0 489120502 85356544 19332 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20839 19332 603 41 0 20798 0
vsize: 83356
[startup+90.0011 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 21700 0 0 0 8941 60 0 0 25 0 1 0 489120502 86016000 19490 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21000 19490 603 41 0 20959 0
vsize: 84000
[startup+100.001 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 21924 0 0 0 9940 60 0 0 25 0 1 0 489120502 86949888 19714 4294967295 134512640 134672761 3221224544 3221223728 134615560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21228 19714 603 41 0 21187 0
vsize: 84912
[startup+110.001 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 22139 0 0 0 10941 61 0 0 25 0 1 0 489120502 87879680 19929 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21455 19929 603 41 0 21414 0
vsize: 85820
[startup+120.002 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 22414 0 0 0 11941 61 0 0 25 0 1 0 489120502 88940544 20204 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21714 20204 603 41 0 21673 0
vsize: 86856
[startup+130.001 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 22842 0 0 0 12940 62 0 0 25 0 1 0 489120502 90648576 20632 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22131 20632 603 41 0 22090 0
vsize: 88524
[startup+140.002 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 23088 0 0 0 13940 63 0 0 25 0 1 0 489120502 91701248 20878 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22388 20878 603 41 0 22347 0
vsize: 89552
[startup+150.002 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 23352 0 0 0 14940 63 0 0 25 0 1 0 489120502 92762112 21142 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22647 21142 603 41 0 22606 0
vsize: 90588
[startup+160.002 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 23672 0 0 0 15939 64 0 0 25 0 1 0 489120502 94076928 21462 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22968 21462 603 41 0 22927 0
vsize: 91872
[startup+170.002 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 24207 0 0 0 16938 66 0 0 25 0 1 0 489120502 96296960 21997 4294967295 134512640 134672761 3221224544 3221223680 134614674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 21997 603 41 0 23469 0
vsize: 94040
[startup+180.001 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 24465 0 0 0 17937 66 0 0 25 0 1 0 489120502 97357824 22255 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23769 22255 603 41 0 23728 0
vsize: 95076
[startup+190.001 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 24729 0 0 0 18937 67 0 0 25 0 1 0 489120502 98402304 22519 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24024 22519 603 41 0 23983 0
vsize: 96096
[startup+200.001 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 24953 0 0 0 19936 68 0 0 25 0 1 0 489120502 99336192 22743 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24252 22743 603 41 0 24211 0
vsize: 97008
[startup+210.001 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 25342 0 0 0 20936 69 0 0 25 0 1 0 489120502 101048320 23132 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24670 23132 603 41 0 24629 0
vsize: 98680
[startup+220.001 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 25897 0 0 0 21935 70 0 0 25 0 1 0 489120502 103284736 23687 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25216 23687 603 41 0 25175 0
vsize: 100864
[startup+230.001 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 26173 0 0 0 22934 71 0 0 25 0 1 0 489120502 104468480 23963 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25505 23963 603 41 0 25464 0
vsize: 102020
[startup+240 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 26522 0 0 0 23933 72 0 0 25 0 1 0 489120502 105902080 24312 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25855 24312 603 41 0 25814 0
vsize: 103420
[startup+250 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 26872 0 0 0 24933 73 0 0 25 0 1 0 489120502 107225088 24662 4294967295 134512640 134672761 3221224544 3221223728 134615988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26178 24662 603 41 0 26137 0
vsize: 104712
[startup+260 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 27130 0 0 0 25932 74 0 0 25 0 1 0 489120502 108281856 24920 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26436 24920 603 41 0 26395 0
vsize: 105744
[startup+270 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 27441 0 0 0 26932 74 0 0 25 0 1 0 489120502 109604864 25231 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26759 25231 603 41 0 26718 0
vsize: 107036
[startup+280 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 27799 0 0 0 27932 75 0 0 25 0 1 0 489120502 111054848 25589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27113 25589 603 41 0 27072 0
vsize: 108452
[startup+289.999 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 28131 0 0 0 28931 76 0 0 25 0 1 0 489120502 112373760 25921 4294967295 134512640 134672761 3221224544 3221223688 134616371 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 25921 603 41 0 27394 0
vsize: 109740
[startup+299.999 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 28437 0 0 0 29931 77 0 0 25 0 1 0 489120502 113672192 26227 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27752 26227 603 41 0 27711 0
vsize: 111008
[startup+309.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 28943 0 0 0 30929 79 0 0 25 0 1 0 489120502 115740672 26733 4294967295 134512640 134672761 3221224544 3221223744 134610711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28257 26733 603 41 0 28216 0
vsize: 113028
[startup+319.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 29345 0 0 0 31928 80 0 0 25 0 1 0 489120502 117329920 27135 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28645 27135 603 41 0 28604 0
vsize: 114580
[startup+329.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 29602 0 0 0 32928 81 0 0 25 0 1 0 489120502 118407168 27392 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28908 27392 603 41 0 28867 0
vsize: 115632
[startup+339.998 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 29993 0 0 0 33927 82 0 0 25 0 1 0 489120502 119984128 27783 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29293 27783 603 41 0 29252 0
vsize: 117172
[startup+349.998 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 30437 0 0 0 34926 83 0 0 25 0 1 0 489120502 121823232 28227 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29742 28227 603 41 0 29701 0
vsize: 118968
[startup+359.998 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 30866 0 0 0 35925 84 0 0 25 0 1 0 489120502 123539456 28656 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30161 28656 603 41 0 30120 0
vsize: 120644
[startup+369.998 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 31309 0 0 0 36924 85 0 0 25 0 1 0 489120502 125407232 29099 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30617 29099 603 41 0 30576 0
vsize: 122468
[startup+379.997 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 31766 0 0 0 37923 86 0 0 25 0 1 0 489120502 127275008 29556 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31073 29556 603 41 0 31032 0
vsize: 124292
[startup+389.997 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 32154 0 0 0 38923 87 0 0 25 0 1 0 489120502 128851968 29944 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31458 29944 603 41 0 31417 0
vsize: 125832
[startup+399.997 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 32561 0 0 0 39923 88 0 0 25 0 1 0 489120502 130433024 30351 4294967295 134512640 134672761 3221224544 3221223584 134613027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31844 30351 603 41 0 31803 0
vsize: 127376
[startup+409.997 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 32806 0 0 0 40922 89 0 0 25 0 1 0 489120502 131497984 30596 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32104 30596 603 41 0 32063 0
vsize: 128416
[startup+419.997 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 33151 0 0 0 41921 90 0 0 25 0 1 0 489120502 132939776 30941 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32456 30941 603 41 0 32415 0
vsize: 129824
[startup+429.996 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 33378 0 0 0 42921 91 0 0 25 0 1 0 489120502 133865472 31168 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32682 31168 603 41 0 32641 0
vsize: 130728
[startup+439.996 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 33834 0 0 0 43920 92 0 0 25 0 1 0 489120502 135700480 31624 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33130 31624 603 41 0 33089 0
vsize: 132520
[startup+449.996 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 34087 0 0 0 44920 92 0 0 25 0 1 0 489120502 136753152 31877 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33387 31877 603 41 0 33346 0
vsize: 133548
[startup+459.995 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 34470 0 0 0 45920 93 0 0 25 0 1 0 489120502 138207232 32260 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33742 32260 603 41 0 33701 0
vsize: 134968
[startup+469.996 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 34945 0 0 0 46919 94 0 0 25 0 1 0 489120502 140197888 32735 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34228 32735 603 41 0 34187 0
vsize: 136912
[startup+479.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 35477 0 0 0 47918 95 0 0 25 0 1 0 489120502 142409728 33267 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34768 33267 603 41 0 34727 0
vsize: 139072
[startup+489.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 35784 0 0 0 48918 95 0 0 25 0 1 0 489120502 143597568 33574 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35058 33574 603 41 0 35017 0
vsize: 140232
[startup+499.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 36336 0 0 0 49917 97 0 0 25 0 1 0 489120502 146124800 34126 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35675 34126 603 41 0 35634 0
vsize: 142700
[startup+509.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 36918 0 0 0 50916 98 0 0 25 0 1 0 489120502 148598784 34708 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36279 34708 603 41 0 36238 0
vsize: 145116
[startup+519.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 37590 0 0 0 51915 99 0 0 25 0 1 0 489120502 151314432 35380 4294967295 134512640 134672761 3221224544 3221223536 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36942 35380 603 41 0 36901 0
vsize: 147768
[startup+529.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 38125 0 0 0 52914 101 0 0 25 0 1 0 489120502 153403392 35915 4294967295 134512640 134672761 3221224544 3221223728 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37452 35915 603 41 0 37411 0
vsize: 149808
[startup+539.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 39008 0 0 0 53912 103 0 0 25 0 1 0 489120502 157065216 36798 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38346 36798 603 41 0 38305 0
vsize: 153384
[startup+549.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 39569 0 0 0 54910 105 0 0 25 0 1 0 489120502 159391744 37359 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38914 37359 603 41 0 38873 0
vsize: 155656
[startup+559.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 39929 0 0 0 55910 105 0 0 25 0 1 0 489120502 160854016 37719 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39271 37719 603 41 0 39230 0
vsize: 157084
[startup+569.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 40410 0 0 0 56909 107 0 0 25 0 1 0 489120502 162807808 38200 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39748 38200 603 41 0 39707 0
vsize: 158992
[startup+579.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 40716 0 0 0 57908 108 0 0 25 0 1 0 489120502 163987456 38506 4294967295 134512640 134672761 3221224544 3221223584 134612797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40036 38506 603 41 0 39995 0
vsize: 160144
[startup+589.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 41090 0 0 0 58907 109 0 0 25 0 1 0 489120502 165572608 38880 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40423 38880 603 41 0 40382 0
vsize: 161692
[startup+599.991 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 41400 0 0 0 59906 110 0 0 25 0 1 0 489120502 166752256 39190 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40711 39190 603 41 0 40670 0
vsize: 162844
[startup+609.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 42063 0 0 0 60906 111 0 0 25 0 1 0 489120502 169508864 39853 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41384 39853 603 41 0 41343 0
vsize: 165536
[startup+619.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 42582 0 0 0 61905 112 0 0 25 0 1 0 489120502 171601920 40372 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41895 40372 603 41 0 41854 0
vsize: 167580
[startup+629.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 42810 0 0 0 62905 113 0 0 25 0 1 0 489120502 172515328 40600 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42118 40600 603 41 0 42077 0
vsize: 168472
[startup+639.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 43256 0 0 0 63903 115 0 0 25 0 1 0 489120502 174354432 41046 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42567 41046 603 41 0 42526 0
vsize: 170268
[startup+649.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 43722 0 0 0 64903 116 0 0 25 0 1 0 489120502 176361472 41512 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43057 41512 603 41 0 43016 0
vsize: 172228
[startup+659.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 44221 0 0 0 65901 118 0 0 25 0 1 0 489120502 178319360 42011 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43535 42011 603 41 0 43494 0
vsize: 174140
[startup+669.992 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 44607 0 0 0 66900 119 0 0 25 0 1 0 489120502 179896320 42397 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43920 42397 603 41 0 43879 0
vsize: 175680
[startup+679.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 44998 0 0 0 67899 120 0 0 25 0 1 0 489120502 181477376 42788 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44306 42788 603 41 0 44265 0
vsize: 177224
[startup+689.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 45199 0 0 0 68899 121 0 0 25 0 1 0 489120502 182398976 42989 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44531 42989 603 41 0 44490 0
vsize: 178124
[startup+699.993 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 45473 0 0 0 69899 121 0 0 25 0 1 0 489120502 183455744 43263 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44789 43263 603 41 0 44748 0
vsize: 179156
[startup+709.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 45913 0 0 0 70898 122 0 0 25 0 1 0 489120502 185311232 43703 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45242 43703 603 41 0 45201 0
vsize: 180968
[startup+719.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 46112 0 0 0 71898 123 0 0 25 0 1 0 489120502 186097664 43902 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45434 43902 603 41 0 45393 0
vsize: 181736
[startup+729.994 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 46506 0 0 0 72897 124 0 0 25 0 1 0 489120502 187699200 44296 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45825 44296 603 41 0 45784 0
vsize: 183300
[startup+739.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 46739 0 0 0 73897 124 0 0 25 0 1 0 489120502 188608512 44529 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46047 44529 603 41 0 46006 0
vsize: 184188
[startup+749.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 47352 0 0 0 74896 126 0 0 25 0 1 0 489120502 191107072 45142 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46657 45142 603 41 0 46616 0
vsize: 186628
[startup+759.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 47626 0 0 0 75896 126 0 0 25 0 1 0 489120502 192282624 45416 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46944 45416 603 41 0 46903 0
vsize: 187776
[startup+769.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 47889 0 0 0 76896 127 0 0 25 0 1 0 489120502 193351680 45679 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47205 45679 603 41 0 47164 0
vsize: 188820
[startup+779.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 48202 0 0 0 77895 128 0 0 25 0 1 0 489120502 194662400 45992 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47525 45992 603 41 0 47484 0
vsize: 190100
[startup+789.995 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 48652 0 0 0 78894 129 0 0 25 0 1 0 489120502 196390912 46442 4294967295 134512640 134672761 3221224544 3221223584 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47947 46442 603 41 0 47906 0
vsize: 191788
[startup+799.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 49105 0 0 0 79893 130 0 0 25 0 1 0 489120502 198352896 46895 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48426 46895 603 41 0 48385 0
vsize: 193704
[startup+809.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 49849 0 0 0 80892 132 0 0 25 0 1 0 489120502 201314304 47639 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49149 47639 603 41 0 49108 0
vsize: 196596
[startup+819.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 50313 0 0 0 81891 134 0 0 25 0 1 0 489120502 203264000 48103 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49625 48103 603 41 0 49584 0
vsize: 198500
[startup+829.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 50727 0 0 0 82890 135 0 0 25 0 1 0 489120502 204984320 48517 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50045 48517 603 41 0 50004 0
vsize: 200180
[startup+839.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 51287 0 0 0 83889 137 0 0 25 0 1 0 489120502 207204352 49077 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50587 49077 603 41 0 50546 0
vsize: 202348
[startup+849.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 51816 0 0 0 84888 138 0 0 25 0 1 0 489120502 209416192 49606 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51127 49606 603 41 0 51086 0
vsize: 204508
[startup+859.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 52583 0 0 0 85886 139 0 0 25 0 1 0 489120502 212533248 50373 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51888 50373 603 41 0 51847 0
vsize: 207552
[startup+869.996 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 53002 0 0 0 86886 140 0 0 25 0 1 0 489120502 214216704 50792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52299 50792 603 41 0 52258 0
vsize: 209196
[startup+879.997 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22362
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 53480 0 0 0 87885 141 0 0 25 0 1 0 489120502 216219648 51270 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52788 51270 603 41 0 52747 0
vsize: 211152
[startup+889.999 s]
Raw data (loadavg): 1.00 0.97 0.91 3/56 22409
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 53677 0 0 0 88865 161 0 0 25 0 1 0 489120502 217010176 51467 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52981 51467 603 41 0 52940 0
vsize: 211924
[startup+899.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22415
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 53965 0 0 0 89862 165 0 0 25 0 1 0 489120502 218202112 51755 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53272 51755 603 41 0 53231 0
vsize: 213088
[startup+909.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22415
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 54338 0 0 0 90861 166 0 0 25 0 1 0 489120502 219643904 52128 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53624 52128 603 41 0 53583 0
vsize: 214496
[startup+919.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22415
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 55142 0 0 0 91859 168 0 0 25 0 1 0 489120502 223023104 52932 4294967295 134512640 134672761 3221224544 3221223688 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54449 52932 603 41 0 54408 0
vsize: 217796
[startup+929.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22415
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 55493 0 0 0 92858 169 0 0 25 0 1 0 489120502 224460800 53283 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54800 53283 603 41 0 54759 0
vsize: 219200
[startup+940 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22415
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 56281 0 0 0 93857 171 0 0 25 0 1 0 489120502 227651584 54071 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55579 54071 603 41 0 55538 0
vsize: 222316
[startup+950 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22415
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 56568 0 0 0 94857 172 0 0 25 0 1 0 489120502 228810752 54358 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55862 54358 603 41 0 55821 0
vsize: 223448
[startup+960.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22415
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 56834 0 0 0 95856 173 0 0 25 0 1 0 489120502 229879808 54624 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56123 54624 603 41 0 56082 0
vsize: 224492
[startup+970.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 57220 0 0 0 96855 174 0 0 25 0 1 0 489120502 231469056 55010 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56511 55010 603 41 0 56470 0
vsize: 226044
[startup+980.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 57379 0 0 0 97855 174 0 0 25 0 1 0 489120502 232144896 55169 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56676 55169 603 41 0 56635 0
vsize: 226704
[startup+990.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 57714 0 0 0 98855 175 0 0 25 0 1 0 489120502 233459712 55504 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56997 55504 603 41 0 56956 0
vsize: 227988
[startup+1000 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 58287 0 0 0 99854 177 0 0 25 0 1 0 489120502 235827200 56077 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57575 56077 603 41 0 57534 0
vsize: 230300
[startup+1010 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 58690 0 0 0 100854 177 0 0 25 0 1 0 489120502 237514752 56480 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57987 56480 603 41 0 57946 0
vsize: 231948
[startup+1020 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 58976 0 0 0 101853 178 0 0 25 0 1 0 489120502 238690304 56766 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58274 56766 603 41 0 58233 0
vsize: 233096
[startup+1030 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 59457 0 0 0 102853 178 0 0 25 0 1 0 489120502 240672768 57247 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58758 57247 603 41 0 58717 0
vsize: 235032
[startup+1040 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 59854 0 0 0 103852 179 0 0 25 0 1 0 489120502 242282496 57644 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59151 57644 603 41 0 59110 0
vsize: 236604
[startup+1050 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 60215 0 0 0 104852 180 0 0 25 0 1 0 489120502 243716096 58005 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59501 58005 603 41 0 59460 0
vsize: 238004
[startup+1060 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 60884 0 0 0 105851 182 0 0 25 0 1 0 489120502 246464512 58674 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60172 58674 603 41 0 60131 0
vsize: 240688
[startup+1070 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 61316 0 0 0 106850 183 0 0 25 0 1 0 489120502 248168448 59106 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60588 59106 603 41 0 60547 0
vsize: 242352
[startup+1080 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 61796 0 0 0 107849 184 0 0 25 0 1 0 489120502 250130432 59586 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61067 59586 603 41 0 61026 0
vsize: 244268
[startup+1090 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 62335 0 0 0 108849 185 0 0 25 0 1 0 489120502 252354560 60125 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61610 60125 603 41 0 61569 0
vsize: 246440
[startup+1100 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 62759 0 0 0 109848 185 0 0 25 0 1 0 489120502 254054400 60549 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62025 60549 603 41 0 61984 0
vsize: 248100
[startup+1110 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 63010 0 0 0 110848 186 0 0 25 0 1 0 489120502 255115264 60800 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62284 60800 603 41 0 62243 0
vsize: 249136
[startup+1120 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 63234 0 0 0 111848 186 0 0 25 0 1 0 489120502 256045056 61024 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62511 61024 603 41 0 62470 0
vsize: 250044
[startup+1130 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 63678 0 0 0 112847 187 0 0 25 0 1 0 489120502 257875968 61468 4294967295 134512640 134672761 3221224544 3221223744 134617686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62958 61468 603 41 0 62917 0
vsize: 251832
[startup+1140 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 63871 0 0 0 113847 188 0 0 25 0 1 0 489120502 258670592 61661 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63152 61661 603 41 0 63111 0
vsize: 252608
[startup+1150 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 64321 0 0 0 114846 189 0 0 25 0 1 0 489120502 260493312 62111 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63597 62111 603 41 0 63556 0
vsize: 254388
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 64937 0 0 0 115844 192 0 0 25 0 1 0 489120502 263049216 62727 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64221 62727 603 41 0 64180 0
vsize: 256884
[startup+1170 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 65280 0 0 0 116843 193 0 0 25 0 1 0 489120502 264364032 63070 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64542 63070 603 41 0 64501 0
vsize: 258168
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 66234 0 0 0 117842 194 0 0 25 0 1 0 489120502 268390400 64024 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65525 64024 603 41 0 65484 0
vsize: 262100
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22417
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 66953 0 0 0 118841 196 0 0 25 0 1 0 489120502 271265792 64743 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66227 64743 603 41 0 66186 0
vsize: 264908
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22419
Raw data (stat): 22362 (minisat+) R 22361 29653 29652 0 -1 0 67466 0 0 0 119840 197 0 0 25 0 1 0 489120502 273383424 65256 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66744 65256 603 41 0 66703 0
vsize: 266976
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 22419
Raw data (stat): 22362 (minisat+) Z 22361 29653 29652 0 -1 12 67466 0 0 0 119840 209 0 0 25 0 1 0 489120502 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.5
CPU user time (s): 1198.41
CPU system time (s): 2.09668
CPU usage (%): 100.031
Max. virtual memory (Kb): 266976
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####