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/miplib/normalized-mps-v2-20-10-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	1182.3
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 22325

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-22 02:54:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11685 boxname=wulflinc18 idbench=899 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f85d0079133f298b06c25764b03ff228  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-air06.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-air06.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-air06.opb
IDLAUNCH: 11685
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        633684 kB
Buffers:         20284 kB
Cached:         356912 kB
SwapCached:        748 kB
Active:          26692 kB
Inactive:       352580 kB
HighTotal:      131008 kB
HighFree:        75824 kB
LowTotal:       903652 kB
LowFree:        557860 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15996 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 03:15:01 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 11685 7 1200.33 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.38 0.71 0.82 2/55 17078
Raw data (stat): 17078 (runsolver) R 17077 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550272157 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0013 s]
Raw data (loadavg): 0.48 0.72 0.82 2/55 17078
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 20005 0 0 0 940 58 0 0 25 0 1 0 550272157 78843904 17828 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19249 17828 603 41 0 19208 0
vsize: 76996
[startup+20.0014 s]
Raw data (loadavg): 0.56 0.73 0.82 2/55 17078
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 20178 0 0 0 1939 59 0 0 25 0 1 0 550272157 79630336 17968 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19441 17968 603 41 0 19400 0
vsize: 77764
[startup+30.0013 s]
Raw data (loadavg): 0.62 0.74 0.82 2/55 17078
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 20442 0 0 0 2939 60 0 0 25 0 1 0 550272157 80949248 18232 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 18232 603 41 0 19722 0
vsize: 79052
[startup+40.0015 s]
Raw data (loadavg): 0.68 0.75 0.82 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 20617 0 0 0 3938 60 0 0 25 0 1 0 550272157 81612800 18407 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19925 18407 603 41 0 19884 0
vsize: 79700
[startup+50.0024 s]
Raw data (loadavg): 0.73 0.76 0.82 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 20780 0 0 0 4938 60 0 0 25 0 1 0 550272157 82313216 18570 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20096 18570 603 41 0 20055 0
vsize: 80384
[startup+60.003 s]
Raw data (loadavg): 0.77 0.76 0.82 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 21002 0 0 0 5938 61 0 0 25 0 1 0 550272157 83243008 18792 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20323 18792 603 41 0 20282 0
vsize: 81292
[startup+70.0045 s]
Raw data (loadavg): 0.81 0.77 0.82 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 21256 0 0 0 6937 62 0 0 25 0 1 0 550272157 84287488 19046 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20578 19046 603 41 0 20537 0
vsize: 82312
[startup+80.0049 s]
Raw data (loadavg): 0.84 0.78 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 21500 0 0 0 7937 63 0 0 25 0 1 0 550272157 85225472 19290 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 19290 603 41 0 20766 0
vsize: 83228
[startup+90.0048 s]
Raw data (loadavg): 0.86 0.78 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 21682 0 0 0 8937 63 0 0 25 0 1 0 550272157 86016000 19472 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21000 19472 603 41 0 20959 0
vsize: 84000
[startup+100.005 s]
Raw data (loadavg): 0.88 0.79 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 21906 0 0 0 9936 64 0 0 25 0 1 0 550272157 86949888 19696 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21228 19696 603 41 0 21187 0
vsize: 84912
[startup+110.006 s]
Raw data (loadavg): 0.90 0.80 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 22078 0 0 0 10936 64 0 0 25 0 1 0 550272157 87613440 19868 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21390 19868 603 41 0 21349 0
vsize: 85560
[startup+120.007 s]
Raw data (loadavg): 0.91 0.80 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 22360 0 0 0 11935 66 0 0 25 0 1 0 550272157 88678400 20150 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21650 20150 603 41 0 21609 0
vsize: 86600
[startup+130.007 s]
Raw data (loadavg): 0.93 0.81 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 22765 0 0 0 12934 66 0 0 25 0 1 0 550272157 90382336 20555 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22066 20555 603 41 0 22025 0
vsize: 88264
[startup+140.007 s]
Raw data (loadavg): 0.94 0.81 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 23025 0 0 0 13933 67 0 0 25 0 1 0 550272157 91439104 20815 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22324 20815 603 41 0 22283 0
vsize: 89296
[startup+150.007 s]
Raw data (loadavg): 0.95 0.82 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 23297 0 0 0 14933 68 0 0 25 0 1 0 550272157 92491776 21087 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22581 21087 603 41 0 22540 0
vsize: 90324
[startup+160.008 s]
Raw data (loadavg): 0.95 0.83 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 23589 0 0 0 15932 69 0 0 25 0 1 0 550272157 93679616 21379 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22871 21379 603 41 0 22830 0
vsize: 91484
[startup+170.008 s]
Raw data (loadavg): 0.96 0.83 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 23952 0 0 0 16932 70 0 0 25 0 1 0 550272157 95252480 21742 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23255 21742 603 41 0 23214 0
vsize: 93020
[startup+180.008 s]
Raw data (loadavg): 0.97 0.84 0.83 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 24421 0 0 0 17931 71 0 0 25 0 1 0 550272157 97087488 22211 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23703 22211 603 41 0 23662 0
vsize: 94812
[startup+190.01 s]
Raw data (loadavg): 0.97 0.84 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 24653 0 0 0 18929 72 0 0 25 0 1 0 550272157 98009088 22443 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23928 22443 603 41 0 23887 0
vsize: 95712
[startup+200.01 s]
Raw data (loadavg): 0.98 0.85 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 24881 0 0 0 19929 73 0 0 25 0 1 0 550272157 98938880 22671 4294967295 134512640 134672761 3221224544 3221223688 134616154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24155 22671 603 41 0 24114 0
vsize: 96620
[startup+210.01 s]
Raw data (loadavg): 0.98 0.85 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 25202 0 0 0 20928 74 0 0 25 0 1 0 550272157 100528128 22992 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24543 22992 603 41 0 24502 0
vsize: 98172
[startup+220.011 s]
Raw data (loadavg): 0.98 0.85 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 25724 0 0 0 21927 75 0 0 25 0 1 0 550272157 102617088 23514 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25053 23514 603 41 0 25012 0
vsize: 100212
[startup+230.011 s]
Raw data (loadavg): 0.98 0.86 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 26095 0 0 0 22926 77 0 0 25 0 1 0 550272157 104075264 23885 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25409 23885 603 41 0 25368 0
vsize: 101636
[startup+240.012 s]
Raw data (loadavg): 0.99 0.86 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 26451 0 0 0 23925 77 0 0 25 0 1 0 550272157 105504768 24241 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25758 24241 603 41 0 25717 0
vsize: 103032
[startup+250.012 s]
Raw data (loadavg): 0.99 0.87 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 26718 0 0 0 24924 78 0 0 25 0 1 0 550272157 106704896 24508 4294967295 134512640 134672761 3221224544 3221223728 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26051 24508 603 41 0 26010 0
vsize: 104204
[startup+260.011 s]
Raw data (loadavg): 0.99 0.87 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 27035 0 0 0 25924 79 0 0 25 0 1 0 550272157 107884544 24825 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26339 24825 603 41 0 26298 0
vsize: 105356
[startup+270.011 s]
Raw data (loadavg): 0.99 0.87 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 27342 0 0 0 26923 80 0 0 25 0 1 0 550272157 109203456 25132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26661 25132 603 41 0 26620 0
vsize: 106644
[startup+280.012 s]
Raw data (loadavg): 0.99 0.88 0.84 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 27670 0 0 0 27922 81 0 0 25 0 1 0 550272157 110530560 25460 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26985 25460 603 41 0 26944 0
vsize: 107940
[startup+290.012 s]
Raw data (loadavg): 0.99 0.88 0.85 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 28064 0 0 0 28922 82 0 0 25 0 1 0 550272157 112107520 25854 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27370 25854 603 41 0 27329 0
vsize: 109480
[startup+300.012 s]
Raw data (loadavg): 0.99 0.89 0.85 2/55 17080
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 28320 0 0 0 29921 82 0 0 25 0 1 0 550272157 113147904 26110 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27624 26110 603 41 0 27583 0
vsize: 110496
[startup+310.013 s]
Raw data (loadavg): 1.23 0.94 0.86 3/58 17128
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 28767 0 0 0 30921 83 0 0 25 0 1 0 550272157 114950144 26557 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28064 26557 603 41 0 28023 0
vsize: 112256
[startup+320.014 s]
Raw data (loadavg): 1.20 0.94 0.86 2/55 17133
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 29145 0 0 0 31920 84 0 0 25 0 1 0 550272157 116539392 26935 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28452 26935 603 41 0 28411 0
vsize: 113808
[startup+330.014 s]
Raw data (loadavg): 1.17 0.94 0.87 2/55 17133
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 29522 0 0 0 32919 85 0 0 25 0 1 0 550272157 118136832 27312 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28842 27312 603 41 0 28801 0
vsize: 115368
[startup+340.014 s]
Raw data (loadavg): 1.14 0.94 0.87 2/55 17135
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 29757 0 0 0 33918 86 0 0 25 0 1 0 550272157 119066624 27547 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29069 27547 603 41 0 29028 0
vsize: 116276
[startup+350.014 s]
Raw data (loadavg): 1.12 0.94 0.87 2/55 17135
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 30189 0 0 0 34918 87 0 0 25 0 1 0 550272157 120770560 27979 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29485 27979 603 41 0 29444 0
vsize: 117940
[startup+360.014 s]
Raw data (loadavg): 1.10 0.94 0.87 2/55 17135
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 30636 0 0 0 35917 87 0 0 25 0 1 0 550272157 122626048 28426 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29938 28426 603 41 0 29897 0
vsize: 119752
[startup+370.014 s]
Raw data (loadavg): 1.08 0.95 0.87 2/55 17135
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 31048 0 0 0 36916 88 0 0 25 0 1 0 550272157 124338176 28838 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30356 28838 603 41 0 30315 0
vsize: 121424
[startup+380.013 s]
Raw data (loadavg): 1.07 0.95 0.87 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 31493 0 0 0 37915 90 0 0 25 0 1 0 550272157 126083072 29283 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30782 29283 603 41 0 30741 0
vsize: 123128
[startup+390.014 s]
Raw data (loadavg): 1.06 0.95 0.87 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 31896 0 0 0 38914 91 0 0 25 0 1 0 550272157 127795200 29686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31200 29686 603 41 0 31159 0
vsize: 124800
[startup+400.015 s]
Raw data (loadavg): 1.05 0.95 0.87 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 32407 0 0 0 39913 93 0 0 25 0 1 0 550272157 129900544 30197 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31714 30197 603 41 0 31673 0
vsize: 126856
[startup+410.014 s]
Raw data (loadavg): 1.04 0.95 0.87 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 32650 0 0 0 40912 93 0 0 25 0 1 0 550272157 130830336 30440 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31941 30440 603 41 0 31900 0
vsize: 127764
[startup+420.015 s]
Raw data (loadavg): 1.04 0.95 0.87 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 32944 0 0 0 41912 94 0 0 25 0 1 0 550272157 132034560 30734 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32235 30734 603 41 0 32194 0
vsize: 128940
[startup+430.016 s]
Raw data (loadavg): 1.03 0.95 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 33235 0 0 0 42911 95 0 0 25 0 1 0 550272157 133206016 31025 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32521 31025 603 41 0 32480 0
vsize: 130084
[startup+440.016 s]
Raw data (loadavg): 1.02 0.95 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 33569 0 0 0 43910 96 0 0 25 0 1 0 550272157 134647808 31359 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32873 31359 603 41 0 32832 0
vsize: 131492
[startup+450.016 s]
Raw data (loadavg): 1.02 0.95 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 33894 0 0 0 44910 97 0 0 25 0 1 0 550272157 135962624 31684 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33194 31684 603 41 0 33153 0
vsize: 132776
[startup+460.016 s]
Raw data (loadavg): 1.02 0.95 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 34308 0 0 0 45909 98 0 0 25 0 1 0 550272157 137551872 32098 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33582 32098 603 41 0 33541 0
vsize: 134328
[startup+470.017 s]
Raw data (loadavg): 1.01 0.96 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 34563 0 0 0 46908 98 0 0 25 0 1 0 550272157 138608640 32353 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33840 32353 603 41 0 33799 0
vsize: 135360
[startup+480.017 s]
Raw data (loadavg): 1.01 0.96 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 35091 0 0 0 47907 100 0 0 25 0 1 0 550272157 140853248 32881 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34388 32881 603 41 0 34347 0
vsize: 137552
[startup+490.017 s]
Raw data (loadavg): 1.01 0.96 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 35538 0 0 0 48906 101 0 0 25 0 1 0 550272157 142684160 33328 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34835 33328 603 41 0 34794 0
vsize: 139340
[startup+500.016 s]
Raw data (loadavg): 1.01 0.96 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 35908 0 0 0 49905 102 0 0 25 0 1 0 550272157 144125952 33698 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35187 33698 603 41 0 35146 0
vsize: 140748
[startup+510.016 s]
Raw data (loadavg): 1.01 0.96 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 36462 0 0 0 50904 104 0 0 25 0 1 0 550272157 146644992 34252 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35802 34252 603 41 0 35761 0
vsize: 143208
[startup+520.016 s]
Raw data (loadavg): 1.00 0.96 0.88 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 37117 0 0 0 51903 104 0 0 25 0 1 0 550272157 149368832 34907 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36467 34907 603 41 0 36426 0
vsize: 145868
[startup+530.016 s]
Raw data (loadavg): 1.00 0.96 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 37803 0 0 0 52901 106 0 0 25 0 1 0 550272157 152096768 35593 4294967295 134512640 134672761 3221224544 3221223584 134612992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37133 35593 603 41 0 37092 0
vsize: 148532
[startup+540.017 s]
Raw data (loadavg): 1.00 0.96 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 38338 0 0 0 53900 108 0 0 25 0 1 0 550272157 154312704 36128 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37674 36128 603 41 0 37633 0
vsize: 150696
[startup+550.017 s]
Raw data (loadavg): 1.00 0.96 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 39146 0 0 0 54898 110 0 0 25 0 1 0 550272157 157585408 36936 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38473 36936 603 41 0 38432 0
vsize: 153892
[startup+560.017 s]
Raw data (loadavg): 1.00 0.96 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 39589 0 0 0 55898 111 0 0 25 0 1 0 550272157 159391744 37379 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38914 37379 603 41 0 38873 0
vsize: 155656
[startup+570.018 s]
Raw data (loadavg): 1.00 0.97 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 40025 0 0 0 56895 113 0 0 25 0 1 0 550272157 161255424 37815 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39369 37815 603 41 0 39328 0
vsize: 157476
[startup+580.018 s]
Raw data (loadavg): 1.00 0.97 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 40467 0 0 0 57894 114 0 0 25 0 1 0 550272157 162938880 38257 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39780 38257 603 41 0 39739 0
vsize: 159120
[startup+590.018 s]
Raw data (loadavg): 1.00 0.97 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 40796 0 0 0 58894 115 0 0 25 0 1 0 550272157 164384768 38586 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40133 38586 603 41 0 40092 0
vsize: 160532
[startup+600.018 s]
Raw data (loadavg): 1.00 0.97 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 41164 0 0 0 59893 115 0 0 25 0 1 0 550272157 165838848 38954 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40488 38954 603 41 0 40447 0
vsize: 161952
[startup+610.018 s]
Raw data (loadavg): 1.00 0.97 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 41506 0 0 0 60893 116 0 0 25 0 1 0 550272157 167276544 39296 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40839 39296 603 41 0 40798 0
vsize: 163356
[startup+620.017 s]
Raw data (loadavg): 1.00 0.97 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 42230 0 0 0 61891 118 0 0 25 0 1 0 550272157 170156032 40020 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41542 40020 603 41 0 41501 0
vsize: 166168
[startup+630.017 s]
Raw data (loadavg): 1.00 0.97 0.89 2/55 17137
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 42630 0 0 0 62891 118 0 0 25 0 1 0 550272157 171868160 40420 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41960 40420 603 41 0 41919 0
vsize: 167840
[startup+640.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17139
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 42875 0 0 0 63891 119 0 0 25 0 1 0 550272157 172777472 40665 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42182 40665 603 41 0 42141 0
vsize: 168728
[startup+650.017 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17139
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 43370 0 0 0 64890 120 0 0 25 0 1 0 550272157 174878720 41160 4294967295 134512640 134672761 3221224544 3221223584 134612694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42695 41160 603 41 0 42654 0
vsize: 170780
[startup+660.017 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 43738 0 0 0 65888 122 0 0 25 0 1 0 550272157 176361472 41528 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43057 41528 603 41 0 43016 0
vsize: 172228
[startup+670.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 44274 0 0 0 66887 123 0 0 25 0 1 0 550272157 178581504 42064 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43599 42064 603 41 0 43558 0
vsize: 174396
[startup+680.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 44611 0 0 0 67886 124 0 0 25 0 1 0 550272157 179896320 42401 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43920 42401 603 41 0 43879 0
vsize: 175680
[startup+690.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 45011 0 0 0 68885 125 0 0 25 0 1 0 550272157 181608448 42801 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44338 42801 603 41 0 44297 0
vsize: 177352
[startup+700.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 45222 0 0 0 69885 125 0 0 25 0 1 0 550272157 182398976 43012 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44531 43012 603 41 0 44490 0
vsize: 178124
[startup+710.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 45516 0 0 0 70884 126 0 0 25 0 1 0 550272157 183586816 43306 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44821 43306 603 41 0 44780 0
vsize: 179284
[startup+720.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 45950 0 0 0 71884 127 0 0 25 0 1 0 550272157 185438208 43740 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45273 43740 603 41 0 45232 0
vsize: 181092
[startup+730.018 s]
Raw data (loadavg): 1.00 0.97 0.90 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 46138 0 0 0 72884 127 0 0 25 0 1 0 550272157 186228736 43928 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45466 43928 603 41 0 45425 0
vsize: 181864
[startup+740.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 46506 0 0 0 73883 128 0 0 25 0 1 0 550272157 187699200 44296 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45825 44296 603 41 0 45784 0
vsize: 183300
[startup+750.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 46775 0 0 0 74882 129 0 0 25 0 1 0 550272157 188735488 44565 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46078 44565 603 41 0 46037 0
vsize: 184312
[startup+760.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 47384 0 0 0 75880 131 0 0 25 0 1 0 550272157 191238144 45174 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46689 45174 603 41 0 46648 0
vsize: 186756
[startup+770.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 47639 0 0 0 76880 132 0 0 25 0 1 0 550272157 192282624 45429 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46944 45429 603 41 0 46903 0
vsize: 187776
[startup+780.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 47907 0 0 0 77879 133 0 0 25 0 1 0 550272157 193351680 45697 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47205 45697 603 41 0 47164 0
vsize: 188820
[startup+790.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 48203 0 0 0 78878 134 0 0 25 0 1 0 550272157 194662400 45993 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47525 45993 603 41 0 47484 0
vsize: 190100
[startup+800.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 48662 0 0 0 79877 136 0 0 25 0 1 0 550272157 196521984 46452 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47979 46452 603 41 0 47938 0
vsize: 191916
[startup+810.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 49126 0 0 0 80876 137 0 0 25 0 1 0 550272157 198352896 46916 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48426 46916 603 41 0 48385 0
vsize: 193704
[startup+820.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 49863 0 0 0 81874 138 0 0 25 0 1 0 550272157 201453568 47653 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49183 47653 603 41 0 49142 0
vsize: 196732
[startup+830.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 50316 0 0 0 82873 140 0 0 25 0 1 0 550272157 203264000 48106 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49625 48106 603 41 0 49584 0
vsize: 198500
[startup+840.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 50727 0 0 0 83873 140 0 0 25 0 1 0 550272157 204984320 48517 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50045 48517 603 41 0 50004 0
vsize: 200180
[startup+850.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 51287 0 0 0 84872 141 0 0 25 0 1 0 550272157 207204352 49077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50587 49077 603 41 0 50546 0
vsize: 202348
[startup+860.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 51799 0 0 0 85871 142 0 0 25 0 1 0 550272157 209293312 49589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51097 49589 603 41 0 51056 0
vsize: 204388
[startup+870.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 52565 0 0 0 86870 144 0 0 25 0 1 0 550272157 212385792 50355 4294967295 134512640 134672761 3221224544 3221223680 134614513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51852 50355 603 41 0 51811 0
vsize: 207408
[startup+880.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 52998 0 0 0 87869 145 0 0 25 0 1 0 550272157 214216704 50788 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52299 50788 603 41 0 52258 0
vsize: 209196
[startup+890.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 53473 0 0 0 88868 146 0 0 25 0 1 0 550272157 216219648 51263 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52788 51263 603 41 0 52747 0
vsize: 211152
[startup+900.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 53675 0 0 0 89868 147 0 0 25 0 1 0 550272157 217010176 51465 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52981 51465 603 41 0 52940 0
vsize: 211924
[startup+910.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 53962 0 0 0 90867 147 0 0 25 0 1 0 550272157 218202112 51752 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53272 51752 603 41 0 53231 0
vsize: 213088
[startup+920.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 54322 0 0 0 91866 149 0 0 25 0 1 0 550272157 219643904 52112 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53624 52112 603 41 0 53583 0
vsize: 214496
[startup+930.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17141
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 55142 0 0 0 92865 150 0 0 25 0 1 0 550272157 223023104 52932 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54449 52932 603 41 0 54408 0
vsize: 217796
[startup+940.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 55483 0 0 0 93864 151 0 0 25 0 1 0 550272157 224333824 53273 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54769 53273 603 41 0 54728 0
vsize: 219076
[startup+950.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 56234 0 0 0 94863 153 0 0 25 0 1 0 550272157 227389440 54024 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55515 54024 603 41 0 55474 0
vsize: 222060
[startup+960.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 56568 0 0 0 95862 154 0 0 25 0 1 0 550272157 228810752 54358 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55862 54358 603 41 0 55821 0
vsize: 223448
[startup+970.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 56834 0 0 0 96861 155 0 0 25 0 1 0 550272157 229879808 54624 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56123 54624 603 41 0 56082 0
vsize: 224492
[startup+980.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 57199 0 0 0 97860 156 0 0 25 0 1 0 550272157 231337984 54989 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56479 54989 603 41 0 56438 0
vsize: 225916
[startup+990.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 57377 0 0 0 98859 157 0 0 25 0 1 0 550272157 232144896 55167 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56676 55167 603 41 0 56635 0
vsize: 226704
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 57708 0 0 0 99859 157 0 0 25 0 1 0 550272157 233459712 55498 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56997 55498 603 41 0 56956 0
vsize: 227988
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 58284 0 0 0 100857 159 0 0 25 0 1 0 550272157 235827200 56074 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57575 56074 603 41 0 57534 0
vsize: 230300
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 58690 0 0 0 101856 160 0 0 25 0 1 0 550272157 237514752 56480 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57987 56480 603 41 0 57946 0
vsize: 231948
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 58975 0 0 0 102856 161 0 0 25 0 1 0 550272157 238690304 56765 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58274 56765 603 41 0 58233 0
vsize: 233096
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 59455 0 0 0 103855 162 0 0 25 0 1 0 550272157 240541696 57245 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58726 57245 603 41 0 58685 0
vsize: 234904
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 59853 0 0 0 104854 163 0 0 25 0 1 0 550272157 242282496 57643 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59151 57643 603 41 0 59110 0
vsize: 236604
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 60215 0 0 0 105854 163 0 0 25 0 1 0 550272157 243716096 58005 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59501 58005 603 41 0 59460 0
vsize: 238004
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 60884 0 0 0 106852 166 0 0 25 0 1 0 550272157 246464512 58674 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60172 58674 603 41 0 60131 0
vsize: 240688
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 61317 0 0 0 107851 166 0 0 25 0 1 0 550272157 248168448 59107 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60588 59107 603 41 0 60547 0
vsize: 242352
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 61803 0 0 0 108850 168 0 0 25 0 1 0 550272157 250249216 59593 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61096 59593 603 41 0 61055 0
vsize: 244384
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 62335 0 0 0 109849 169 0 0 25 0 1 0 550272157 252354560 60125 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61610 60125 603 41 0 61569 0
vsize: 246440
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 62759 0 0 0 110847 171 0 0 25 0 1 0 550272157 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+1120.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 63021 0 0 0 111847 172 0 0 25 0 1 0 550272157 255246336 60811 4294967295 134512640 134672761 3221224544 3221223536 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62316 60811 603 41 0 62275 0
vsize: 249264
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 63238 0 0 0 112846 172 0 0 25 0 1 0 550272157 256045056 61028 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62511 61028 603 41 0 62470 0
vsize: 250044
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 63678 0 0 0 113845 173 0 0 25 0 1 0 550272157 257875968 61468 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62958 61468 603 41 0 62917 0
vsize: 251832
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 63883 0 0 0 114845 174 0 0 25 0 1 0 550272157 258670592 61673 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63152 61673 603 41 0 63111 0
vsize: 252608
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 64359 0 0 0 115843 176 0 0 25 0 1 0 550272157 260628480 62149 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63630 62149 603 41 0 63589 0
vsize: 254520
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 64937 0 0 0 116843 176 0 0 25 0 1 0 550272157 263049216 62727 4294967295 134512640 134672761 3221224544 3221223688 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64221 62727 603 41 0 64180 0
vsize: 256884
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 65333 0 0 0 117842 177 0 0 25 0 1 0 550272157 264622080 63123 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64605 63123 603 41 0 64564 0
vsize: 258420
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 66268 0 0 0 118841 179 0 0 25 0 1 0 550272157 268529664 64058 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65559 64058 603 41 0 65518 0
vsize: 262236
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 17143
Raw data (stat): 17078 (minisat+) R 17077 20024 20023 0 -1 0 66999 0 0 0 119839 181 0 0 25 0 1 0 550272157 271396864 64789 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66259 64789 603 41 0 66218 0
vsize: 265036
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 0.97 0.91 1/55 17143
Raw data (stat): 17078 (minisat+) Z 17077 20024 20023 0 -1 12 66999 0 0 0 119839 193 0 0 25 0 1 0 550272157 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.16
CPU time (s): 1200.33
CPU user time (s): 1198.4
CPU system time (s): 1.93271
CPU usage (%): 100.015
Max. virtual memory (Kb): 265036
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####