%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN887-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:40:22 PM UTC 2026
% Result : Unsatisfiable 61.20s 12.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : SYN887-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.25 % Computer : n024.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Thu May 7 08:50:27 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 SPASS-SCL-FOL version:
% 0.07/0.31 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 61.20/12.64 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.20/12.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.20/12.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.20/12.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.20/12.64 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.20/12.64 Execution lmodel_grow ended with status: unsatisfiable
% 61.20/12.64 Used heuristic: lmodel_grow
% 61.20/12.64
% 61.20/12.64 Input Clauses:
% 61.20/12.65
% 61.20/12.65 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssNder1_5r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssPv32_9r1r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssPv31_10r1r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssPv30_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv36_5r1r1r1r1r1 ssPv38_3r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv24_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv40_1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv18_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv21_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv37_4r1r1r1r1 ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv22_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv39_2r1r1 ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv35_6r1r1r1r1r1r1 ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv34_7r1r1r1r1r1r1r1 ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 61.20/12.65 Fol Constants: skc62 skc63 skc60 skc61 skc58 skc59 skc56 skc57 skc54 skc55 skc52 skc53 skc50 skc51 skc48 skc49 skc46 skc47 skc44 skc45 skc42 skc43 skc40 skc41 skc38 skc39 skc36 skc37 skc34 skc35 skc32 skc33
% 61.20/12.65 Fol Functions:
% 61.20/12.65 Problem Properties:
% 61.20/12.65 This is a Bernays Schoenfinkel problem.
% 61.20/12.65
% 61.20/12.65 After reduction: Problem Properties:
% 61.20/12.65 This is a Bernays Schoenfinkel problem.
% 61.20/12.65
% 61.20/12.65
% 61.20/12.65 Reduced Input Clauses:
% 61.20/12.65 113:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 61.20/12.65 115:1:2:[113.1,3.0,1.0,114.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 61.20/12.65 118:1:3:[115.2,4.0,113.1,116.1,1.0,117.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 61.20/12.65 122:1:4:[118.3,5.0,115.2,119.1,113.1,120.2,1.0,121.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 61.20/12.65 127:1:5:[122.4,6.0,118.3,123.1,115.2,124.2,113.1,125.3,1.0,126.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 61.20/12.65 133:1:6:[127.5,7.0,122.4,128.1,118.3,129.2,115.2,130.3,113.1,131.4,1.0,132.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 61.20/12.65 140:1:7:[133.6,8.0,127.5,134.1,122.4,135.2,118.3,136.3,115.2,137.4,113.1,138.5,1.0,139.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 61.20/12.65 148:1:8:[140.7,9.0,133.6,141.1,127.5,142.2,122.4,143.3,118.3,144.4,115.2,145.5,113.1,146.6,1.0,147.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 61.20/12.65 156:1:8:[140.7,10.0,133.6,149.1,127.5,150.2,122.4,151.3,118.3,152.4,115.2,153.5,113.1,154.6,1.0,155.7]:TopTopTopTopTopTopTopTop: -> ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,skc62)
% 61.20/12.65 164:1:8:[140.7,11.1,133.6,157.2,127.5,158.3,122.4,159.4,118.3,160.5,115.2,161.6,113.1,162.7,1.0,163.8]:TopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,skc63) ->
% 61.20/12.65 173:1:9:[148.8,12.0,140.7,165.1,133.6,166.2,127.5,167.3,122.4,168.4,118.3,169.5,115.2,170.6,113.1,171.7,1.0,172.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 61.20/12.65 182:1:9:[148.8,13.0,140.7,174.1,133.6,175.2,127.5,176.3,122.4,177.4,118.3,178.5,115.2,179.6,113.1,180.7,1.0,181.8]:TopTopTopTopTopTopTopTopTop: -> ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,skc60)
% 61.20/12.65 191:1:9:[148.8,14.1,140.7,183.2,133.6,184.3,127.5,185.4,122.4,186.5,118.3,187.6,115.2,188.7,113.1,189.8,1.0,190.9]:TopTopTopTopTopTopTopTopTop: ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,skc61) ->
% 61.20/12.65 201:1:10:[173.9,15.0,148.8,192.1,140.7,193.2,133.6,194.3,127.5,195.4,122.4,196.5,118.3,197.6,115.2,198.7,113.1,199.8,1.0,200.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 61.20/12.65 211:1:10:[173.9,16.0,148.8,202.1,140.7,203.2,133.6,204.3,127.5,205.4,122.4,206.5,118.3,207.6,115.2,208.7,113.1,209.8,1.0,210.9]:TopTopTopTopTopTopTopTopTopTop: -> ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc58)
% 61.20/12.65 221:1:10:[173.9,17.1,148.8,212.2,140.7,213.3,133.6,214.4,127.5,215.5,122.4,216.6,118.3,217.7,115.2,218.8,113.1,219.9,1.0,220.10]:TopTopTopTopTopTopTopTopTopTop: ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,skc59) ->
% 61.20/12.65 232:1:11:[201.10,18.0,173.9,222.1,148.8,223.2,140.7,224.3,133.6,225.4,127.5,226.5,122.4,227.6,118.3,228.7,115.2,229.8,113.1,230.9,1.0,231.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 61.20/12.65 243:1:11:[201.10,19.0,173.9,233.1,148.8,234.2,140.7,235.3,133.6,236.4,127.5,237.5,122.4,238.6,118.3,239.7,115.2,240.8,113.1,241.9,1.0,242.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,skc56)
% 61.20/12.65 254:1:11:[201.10,20.1,173.9,244.2,148.8,245.3,140.7,246.4,133.6,247.5,127.5,248.6,122.4,249.7,118.3,250.8,115.2,251.9,113.1,252.10,1.0,253.11]:TopTopTopTopTopTopTopTopTopTopTop: ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,skc57) ->
% 61.20/12.65 266:1:12:[232.11,21.0,201.10,255.1,173.9,256.2,148.8,257.3,140.7,258.4,133.6,259.5,127.5,260.6,122.4,261.7,118.3,262.8,115.2,263.9,113.1,264.10,1.0,265.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 61.20/12.65 278:1:12:[232.11,22.0,201.10,267.1,173.9,268.2,148.8,269.3,140.7,270.4,133.6,271.5,127.5,272.6,122.4,273.7,118.3,274.8,115.2,275.9,113.1,276.10,1.0,277.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc54)
% 61.20/12.65 290:1:12:[232.11,23.1,201.10,279.2,173.9,280.3,148.8,281.4,140.7,282.5,133.6,283.6,127.5,284.7,122.4,285.8,118.3,286.9,115.2,287.10,113.1,288.11,1.0,289.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc55) ->
% 61.20/12.65 303:1:13:[266.12,24.0,232.11,291.1,201.10,292.2,173.9,293.3,148.8,294.4,140.7,295.5,133.6,296.6,127.5,297.7,122.4,298.8,118.3,299.9,115.2,300.10,113.1,301.11,1.0,302.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 61.20/12.65 316:1:13:[266.12,25.0,232.11,304.1,201.10,305.2,173.9,306.3,148.8,307.4,140.7,308.5,133.6,309.6,127.5,310.7,122.4,311.8,118.3,312.9,115.2,313.10,113.1,314.11,1.0,315.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc52)
% 61.20/12.65 329:1:13:[266.12,26.1,232.11,317.2,201.10,318.3,173.9,319.4,148.8,320.5,140.7,321.6,133.6,322.7,127.5,323.8,122.4,324.9,118.3,325.10,115.2,326.11,113.1,327.12,1.0,328.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc53) ->
% 61.20/12.65 343:1:14:[303.13,27.0,266.12,330.1,232.11,331.2,201.10,332.3,173.9,333.4,148.8,334.5,140.7,335.6,133.6,336.7,127.5,337.8,122.4,338.9,118.3,339.10,115.2,340.11,113.1,341.12,1.0,342.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 61.20/12.65 357:1:14:[303.13,28.0,266.12,344.1,232.11,345.2,201.10,346.3,173.9,347.4,148.8,348.5,140.7,349.6,133.6,350.7,127.5,351.8,122.4,352.9,118.3,353.10,115.2,354.11,113.1,355.12,1.0,356.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc50)
% 61.20/12.65 371:1:14:[303.13,29.1,266.12,358.2,232.11,359.3,201.10,360.4,173.9,361.5,148.8,362.6,140.7,363.7,133.6,364.8,127.5,365.9,122.4,366.10,118.3,367.11,115.2,368.12,113.1,369.13,1.0,370.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc51) ->
% 61.20/12.65 384:4:13:[266.12,30.0,232.11,372.2,201.10,373.3,173.9,374.4,148.8,375.5,140.7,376.6,133.6,377.7,127.5,378.9,122.4,379.10,118.3,380.11,115.2,381.12,113.1,382.13,1.0,383.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv36_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 399:1:15:[343.14,31.0,303.13,385.1,266.12,386.2,232.11,387.3,201.10,388.4,173.9,389.5,148.8,390.6,140.7,391.7,133.6,392.8,127.5,393.9,122.4,394.10,118.3,395.11,115.2,396.12,113.1,397.13,1.0,398.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 61.20/12.65 414:1:15:[343.14,32.0,303.13,400.1,266.12,401.2,232.11,402.3,201.10,403.4,173.9,404.5,148.8,405.6,140.7,406.7,133.6,407.8,127.5,408.9,122.4,409.10,118.3,410.11,115.2,411.12,113.1,412.13,1.0,413.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc48)
% 61.20/12.65 429:1:15:[343.14,33.1,303.13,415.2,266.12,416.3,232.11,417.4,201.10,418.5,173.9,419.6,148.8,420.7,140.7,421.8,133.6,422.9,127.5,423.10,122.4,424.11,118.3,425.12,115.2,426.13,113.1,427.14,1.0,428.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc49) ->
% 61.20/12.65 445:1:16:[399.15,34.0,343.14,430.1,303.13,431.2,266.12,432.3,232.11,433.4,201.10,434.5,173.9,435.6,148.8,436.7,140.7,437.8,133.6,438.9,127.5,439.10,122.4,440.11,118.3,441.12,115.2,442.13,113.1,443.14,1.0,444.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 61.20/12.65 462:1:17:[445.16,35.0,399.15,446.1,343.14,447.2,303.13,448.3,266.12,449.4,232.11,450.5,201.10,451.6,173.9,452.7,148.8,453.8,140.7,454.9,133.6,455.10,127.5,456.11,122.4,457.12,118.3,458.13,115.2,459.14,113.1,460.15,1.0,461.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 61.20/12.65 480:1:18:[462.17,36.0,445.16,463.1,399.15,464.2,343.14,465.3,303.13,466.4,266.12,467.5,232.11,468.6,201.10,469.7,173.9,470.8,148.8,471.9,140.7,472.10,133.6,473.11,127.5,474.12,122.4,475.13,118.3,476.14,115.2,477.15,113.1,478.16,1.0,479.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 61.20/12.65 497:4:17:[445.16,37.0,399.15,481.2,343.14,482.4,303.13,483.6,266.12,484.7,232.11,485.8,201.10,486.9,173.9,487.10,148.8,488.11,140.7,489.12,133.6,490.13,127.5,491.14,122.4,492.15,118.3,493.16,115.2,494.17,113.1,495.19,1.0,496.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv40_1r1(x0) ->
% 61.20/12.65 516:1:19:[480.18,38.0,462.17,498.1,445.16,499.2,399.15,500.3,343.14,501.4,303.13,502.5,266.12,503.6,232.11,504.7,201.10,505.8,173.9,506.9,148.8,507.10,140.7,508.11,133.6,509.12,127.5,510.13,122.4,511.14,118.3,512.15,115.2,513.16,113.1,514.17,1.0,515.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 61.20/12.65 536:1:20:[516.19,39.0,480.18,517.1,462.17,518.2,445.16,519.3,399.15,520.4,343.14,521.5,303.13,522.6,266.12,523.7,232.11,524.8,201.10,525.9,173.9,526.10,148.8,527.11,140.7,528.12,133.6,529.13,127.5,530.14,122.4,531.15,118.3,532.16,115.2,533.17,113.1,534.18,1.0,535.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 61.20/12.65 554:4:18:[462.17,40.0,445.16,537.2,399.15,538.3,343.14,539.4,303.13,540.5,266.12,541.6,232.11,542.7,201.10,543.8,173.9,544.10,148.8,545.11,140.7,546.12,133.6,547.13,127.5,548.14,122.4,549.15,118.3,550.16,115.2,551.17,113.1,552.18,1.0,553.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv24_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 61.20/12.65 575:1:21:[536.20,41.0,516.19,555.1,480.18,556.2,462.17,557.3,445.16,558.4,399.15,559.5,343.14,560.6,303.13,561.7,266.12,562.8,232.11,563.9,201.10,564.10,173.9,565.11,148.8,566.12,140.7,567.13,133.6,568.14,127.5,569.15,122.4,570.16,118.3,571.17,115.2,572.18,113.1,573.19,1.0,574.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 61.20/12.65 597:1:22:[575.21,42.0,536.20,576.1,516.19,577.2,480.18,578.3,462.17,579.4,445.16,580.5,399.15,581.6,343.14,582.7,303.13,583.8,266.12,584.9,232.11,585.10,201.10,586.11,173.9,587.12,148.8,588.13,140.7,589.14,133.6,590.15,127.5,591.16,122.4,592.17,118.3,593.18,115.2,594.19,113.1,595.20,1.0,596.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
% 61.20/12.65 620:1:23:[597.22,43.0,575.21,598.1,536.20,599.2,516.19,600.3,480.18,601.4,462.17,602.5,445.16,603.6,399.15,604.7,343.14,605.8,303.13,606.9,266.12,607.10,232.11,608.11,201.10,609.12,173.9,610.13,148.8,611.14,140.7,612.15,133.6,613.16,127.5,614.17,122.4,615.18,118.3,616.19,115.2,617.20,113.1,618.21,1.0,619.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22)
% 61.20/12.65 644:1:24:[620.23,44.0,597.22,621.1,575.21,622.2,536.20,623.3,516.19,624.4,480.18,625.5,462.17,626.6,445.16,627.7,399.15,628.8,343.14,629.9,303.13,630.10,266.12,631.11,232.11,632.12,201.10,633.13,173.9,634.14,148.8,635.15,140.7,636.16,133.6,637.17,127.5,638.18,122.4,639.19,118.3,640.20,115.2,641.21,113.1,642.22,1.0,643.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23)
% 61.20/12.65 668:1:24:[620.23,45.0,597.22,645.1,575.21,646.2,536.20,647.3,516.19,648.4,480.18,649.5,462.17,650.6,445.16,651.7,399.15,652.8,343.14,653.9,303.13,654.10,266.12,655.11,232.11,656.12,201.10,657.13,173.9,658.14,148.8,659.15,140.7,660.16,133.6,661.17,127.5,662.18,122.4,663.19,118.3,664.20,115.2,665.21,113.1,666.22,1.0,667.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,skc46)
% 61.20/12.65 692:1:24:[620.23,46.1,597.22,669.2,575.21,670.3,536.20,671.4,516.19,672.5,480.18,673.6,462.17,674.7,445.16,675.8,399.15,676.9,343.14,677.10,303.13,678.11,266.12,679.12,232.11,680.13,201.10,681.14,173.9,682.15,148.8,683.16,140.7,684.17,133.6,685.18,127.5,686.19,122.4,687.20,118.3,688.21,115.2,689.22,113.1,690.23,1.0,691.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,skc47) ->
% 61.20/12.65 717:1:25:[644.24,47.0,620.23,693.1,597.22,694.2,575.21,695.3,536.20,696.4,516.19,697.5,480.18,698.6,462.17,699.7,445.16,700.8,399.15,701.9,343.14,702.10,303.13,703.11,266.12,704.12,232.11,705.13,201.10,706.14,173.9,707.15,148.8,708.16,140.7,709.17,133.6,710.18,127.5,711.19,122.4,712.20,118.3,713.21,115.2,714.22,113.1,715.23,1.0,716.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24)
% 61.20/12.65 742:1:25:[644.24,48.0,620.23,718.1,597.22,719.2,575.21,720.3,536.20,721.4,516.19,722.5,480.18,723.6,462.17,724.7,445.16,725.8,399.15,726.9,343.14,727.10,303.13,728.11,266.12,729.12,232.11,730.13,201.10,731.14,173.9,732.15,148.8,733.16,140.7,734.17,133.6,735.18,127.5,736.19,122.4,737.20,118.3,738.21,115.2,739.22,113.1,740.23,1.0,741.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,skc44)
% 61.20/12.65 767:1:25:[644.24,49.1,620.23,743.2,597.22,744.3,575.21,745.4,536.20,746.5,516.19,747.6,480.18,748.7,462.17,749.8,445.16,750.9,399.15,751.10,343.14,752.11,303.13,753.12,266.12,754.13,232.11,755.14,201.10,756.15,173.9,757.16,148.8,758.17,140.7,759.18,133.6,760.19,127.5,761.20,122.4,762.21,118.3,763.22,115.2,764.23,113.1,765.24,1.0,766.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,skc45) ->
% 61.20/12.65 793:1:26:[717.25,50.0,644.24,768.1,620.23,769.2,597.22,770.3,575.21,771.4,536.20,772.5,516.19,773.6,480.18,774.7,462.17,775.8,445.16,776.9,399.15,777.10,343.14,778.11,303.13,779.12,266.12,780.13,232.11,781.14,201.10,782.15,173.9,783.16,148.8,784.17,140.7,785.18,133.6,786.19,127.5,787.20,122.4,788.21,118.3,789.22,115.2,790.23,113.1,791.24,1.0,792.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25)
% 61.20/12.65 819:1:26:[717.25,51.0,644.24,794.1,620.23,795.2,597.22,796.3,575.21,797.4,536.20,798.5,516.19,799.6,480.18,800.7,462.17,801.8,445.16,802.9,399.15,803.10,343.14,804.11,303.13,805.12,266.12,806.13,232.11,807.14,201.10,808.15,173.9,809.16,148.8,810.17,140.7,811.18,133.6,812.19,127.5,813.20,122.4,814.21,118.3,815.22,115.2,816.23,113.1,817.24,1.0,818.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,skc42)
% 61.20/12.65 845:1:26:[717.25,52.1,644.24,820.2,620.23,821.3,597.22,822.4,575.21,823.5,536.20,824.6,516.19,825.7,480.18,826.8,462.17,827.9,445.16,828.10,399.15,829.11,343.14,830.12,303.13,831.13,266.12,832.14,232.11,833.15,201.10,834.16,173.9,835.17,148.8,836.18,140.7,837.19,133.6,838.20,127.5,839.21,122.4,840.22,118.3,841.23,115.2,842.24,113.1,843.25,1.0,844.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,skc43) ->
% 61.20/12.65 872:1:27:[793.26,53.0,717.25,846.1,644.24,847.2,620.23,848.3,597.22,849.4,575.21,850.5,536.20,851.6,516.19,852.7,480.18,853.8,462.17,854.9,445.16,855.10,399.15,856.11,343.14,857.12,303.13,858.13,266.12,859.14,232.11,860.15,201.10,861.16,173.9,862.17,148.8,863.18,140.7,864.19,133.6,865.20,127.5,866.21,122.4,867.22,118.3,868.23,115.2,869.24,113.1,870.25,1.0,871.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26)
% 61.20/12.65 899:1:27:[793.26,54.0,717.25,873.1,644.24,874.2,620.23,875.3,597.22,876.4,575.21,877.5,536.20,878.6,516.19,879.7,480.18,880.8,462.17,881.9,445.16,882.10,399.15,883.11,343.14,884.12,303.13,885.13,266.12,886.14,232.11,887.15,201.10,888.16,173.9,889.17,148.8,890.18,140.7,891.19,133.6,892.20,127.5,893.21,122.4,894.22,118.3,895.23,115.2,896.24,113.1,897.25,1.0,898.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,skc40)
% 61.20/12.65 926:1:27:[793.26,55.1,717.25,900.2,644.24,901.3,620.23,902.4,597.22,903.5,575.21,904.6,536.20,905.7,516.19,906.8,480.18,907.9,462.17,908.10,445.16,909.11,399.15,910.12,343.14,911.13,303.13,912.14,266.12,913.15,232.11,914.16,201.10,915.17,173.9,916.18,148.8,917.19,140.7,918.20,133.6,919.21,127.5,920.22,122.4,921.23,118.3,922.24,115.2,923.25,113.1,924.26,1.0,925.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,skc41) ->
% 61.20/12.65 951:4:25:[644.24,56.0,620.23,927.2,597.22,928.3,575.21,929.4,536.20,930.6,516.19,931.7,480.18,932.8,462.17,933.9,445.16,934.10,399.15,935.12,343.14,936.13,303.13,937.14,266.12,938.15,232.11,939.16,201.10,940.17,173.9,941.18,148.8,942.19,140.7,943.20,133.6,944.21,127.5,945.22,122.4,946.23,118.3,947.24,115.2,948.25,113.1,949.26,1.0,950.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv21_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24)
% 61.20/12.65 979:1:28:[872.27,57.0,793.26,952.1,717.25,953.2,644.24,954.3,620.23,955.4,597.22,956.5,575.21,957.6,536.20,958.7,516.19,959.8,480.18,960.9,462.17,961.10,445.16,962.11,399.15,963.12,343.14,964.13,303.13,965.14,266.12,966.15,232.11,967.16,201.10,968.17,173.9,969.18,148.8,970.19,140.7,971.20,133.6,972.21,127.5,973.22,122.4,974.23,118.3,975.24,115.2,976.25,113.1,977.26,1.0,978.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
% 61.20/12.65 1007:1:28:[872.27,58.0,793.26,980.1,717.25,981.2,644.24,982.3,620.23,983.4,597.22,984.5,575.21,985.6,536.20,986.7,516.19,987.8,480.18,988.9,462.17,989.10,445.16,990.11,399.15,991.12,343.14,992.13,303.13,993.14,266.12,994.15,232.11,995.16,201.10,996.17,173.9,997.18,148.8,998.19,140.7,999.20,133.6,1000.21,127.5,1001.22,122.4,1002.23,118.3,1003.24,115.2,1004.25,113.1,1005.26,1.0,1006.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,skc38)
% 61.20/12.65 1035:1:28:[872.27,59.1,793.26,1008.2,717.25,1009.3,644.24,1010.4,620.23,1011.5,597.22,1012.6,575.21,1013.7,536.20,1014.8,516.19,1015.9,480.18,1016.10,462.17,1017.11,445.16,1018.12,399.15,1019.13,343.14,1020.14,303.13,1021.15,266.12,1022.16,232.11,1023.17,201.10,1024.18,173.9,1025.19,148.8,1026.20,140.7,1027.21,133.6,1028.22,127.5,1029.23,122.4,1030.24,118.3,1031.25,115.2,1032.26,113.1,1033.27,1.0,1034.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,skc39) ->
% 61.20/12.65 1064:1:29:[979.28,60.0,872.27,1036.1,793.26,1037.2,717.25,1038.3,644.24,1039.4,620.23,1040.5,597.22,1041.6,575.21,1042.7,536.20,1043.8,516.19,1044.9,480.18,1045.10,462.17,1046.11,445.16,1047.12,399.15,1048.13,343.14,1049.14,303.13,1050.15,266.12,1051.16,232.11,1052.17,201.10,1053.18,173.9,1054.19,148.8,1055.20,140.7,1056.21,133.6,1057.22,127.5,1058.23,122.4,1059.24,118.3,1060.25,115.2,1061.26,113.1,1062.27,1.0,1063.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28)
% 61.20/12.65 1093:1:29:[979.28,61.0,872.27,1065.1,793.26,1066.2,717.25,1067.3,644.24,1068.4,620.23,1069.5,597.22,1070.6,575.21,1071.7,536.20,1072.8,516.19,1073.9,480.18,1074.10,462.17,1075.11,445.16,1076.12,399.15,1077.13,343.14,1078.14,303.13,1079.15,266.12,1080.16,232.11,1081.17,201.10,1082.18,173.9,1083.19,148.8,1084.20,140.7,1085.21,133.6,1086.22,127.5,1087.23,122.4,1088.24,118.3,1089.25,115.2,1090.26,113.1,1091.27,1.0,1092.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,skc36)
% 61.20/12.65 1122:1:29:[979.28,62.1,872.27,1094.2,793.26,1095.3,717.25,1096.4,644.24,1097.5,620.23,1098.6,597.22,1099.7,575.21,1100.8,536.20,1101.9,516.19,1102.10,480.18,1103.11,462.17,1104.12,445.16,1105.13,399.15,1106.14,343.14,1107.15,303.13,1108.16,266.12,1109.17,232.11,1110.18,201.10,1111.19,173.9,1112.20,148.8,1113.21,140.7,1114.22,133.6,1115.23,127.5,1116.24,122.4,1117.25,118.3,1118.26,115.2,1119.27,113.1,1120.28,1.0,1121.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,skc37) ->
% 61.20/12.65 1150:4:28:[872.27,63.0,793.26,1123.2,717.25,1124.3,644.24,1125.4,620.23,1126.5,597.22,1127.6,575.21,1128.7,536.20,1129.8,516.19,1130.9,480.18,1131.10,462.17,1132.11,445.16,1133.12,399.15,1134.14,343.14,1135.15,303.13,1136.16,266.12,1137.17,232.11,1138.18,201.10,1139.19,173.9,1140.20,148.8,1141.21,140.7,1142.22,133.6,1143.23,127.5,1144.24,122.4,1145.25,118.3,1146.26,115.2,1147.27,113.1,1148.28,1.0,1149.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv18_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv40_1r1(x0)
% 61.20/12.65 1180:1:30:[1064.29,64.0,979.28,1151.1,872.27,1152.2,793.26,1153.3,717.25,1154.4,644.24,1155.5,620.23,1156.6,597.22,1157.7,575.21,1158.8,536.20,1159.9,516.19,1160.10,480.18,1161.11,462.17,1162.12,445.16,1163.13,399.15,1164.14,343.14,1165.15,303.13,1166.16,266.12,1167.17,232.11,1168.18,201.10,1169.19,173.9,1170.20,148.8,1171.21,140.7,1172.22,133.6,1173.23,127.5,1174.24,122.4,1175.25,118.3,1176.26,115.2,1177.27,113.1,1178.28,1.0,1179.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29)
% 61.20/12.65 1210:1:30:[1064.29,65.0,979.28,1181.1,872.27,1182.2,793.26,1183.3,717.25,1184.4,644.24,1185.5,620.23,1186.6,597.22,1187.7,575.21,1188.8,536.20,1189.9,516.19,1190.10,480.18,1191.11,462.17,1192.12,445.16,1193.13,399.15,1194.14,343.14,1195.15,303.13,1196.16,266.12,1197.17,232.11,1198.18,201.10,1199.19,173.9,1200.20,148.8,1201.21,140.7,1202.22,133.6,1203.23,127.5,1204.24,122.4,1205.25,118.3,1206.26,115.2,1207.27,113.1,1208.28,1.0,1209.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,skc34)
% 61.20/12.65 1240:1:30:[1064.29,66.1,979.28,1211.2,872.27,1212.3,793.26,1213.4,717.25,1214.5,644.24,1215.6,620.23,1216.7,597.22,1217.8,575.21,1218.9,536.20,1219.10,516.19,1220.11,480.18,1221.12,462.17,1222.13,445.16,1223.14,399.15,1224.15,343.14,1225.16,303.13,1226.17,266.12,1227.18,232.11,1228.19,201.10,1229.20,173.9,1230.21,148.8,1231.22,140.7,1232.23,133.6,1233.24,127.5,1234.25,122.4,1235.26,118.3,1236.27,115.2,1237.28,113.1,1238.29,1.0,1239.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,skc35) ->
% 61.20/12.65 1269:4:29:[979.28,67.0,872.27,1241.1,793.26,1242.2,717.25,1243.3,644.24,1244.4,620.23,1245.5,597.22,1246.6,575.21,1247.7,536.20,1248.8,516.19,1249.9,480.18,1250.10,462.17,1251.12,445.16,1252.13,399.15,1253.14,343.14,1254.15,303.13,1255.17,266.12,1256.18,232.11,1257.19,201.10,1258.20,173.9,1259.21,148.8,1260.22,140.7,1261.23,133.6,1262.24,127.5,1263.25,122.4,1264.26,118.3,1265.27,115.2,1266.28,113.1,1267.29,1.0,1268.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv37_4r1r1r1r1(x0,x1,x2,x3)
% 61.20/12.65 1298:4:29:[979.28,68.0,872.27,1270.2,793.26,1271.3,717.25,1272.4,644.24,1273.5,620.23,1274.6,597.22,1275.7,575.21,1276.9,536.20,1277.10,516.19,1278.11,480.18,1279.12,462.17,1280.13,445.16,1281.14,399.15,1282.15,343.14,1283.17,303.13,1284.18,266.12,1285.19,232.11,1286.20,201.10,1287.21,173.9,1288.22,148.8,1289.23,140.7,1290.24,133.6,1291.25,127.5,1292.26,122.4,1293.27,118.3,1294.28,115.2,1295.29,113.1,1296.30,1.0,1297.31]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv40_1r1(x0)
% 61.20/12.65 1327:4:29:[979.28,69.1,872.27,1299.2,793.26,1300.3,717.25,1301.4,644.24,1302.5,620.23,1303.6,597.22,1304.7,575.21,1305.8,536.20,1306.9,516.19,1307.10,480.18,1308.12,462.17,1309.13,445.16,1310.14,399.15,1311.15,343.14,1312.16,303.13,1313.17,266.12,1314.18,232.11,1315.19,201.10,1316.20,173.9,1317.21,148.8,1318.22,140.7,1319.23,133.6,1320.24,127.5,1321.25,122.4,1322.26,118.3,1323.27,115.2,1324.28,113.1,1325.29,1.0,1326.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 1356:4:29:[979.28,70.0,872.27,1328.1,793.26,1329.2,717.25,1330.3,644.24,1331.4,620.23,1332.5,597.22,1333.6,575.21,1334.7,536.20,1335.8,516.19,1336.9,480.18,1337.10,462.17,1338.11,445.16,1339.12,399.15,1340.13,343.14,1341.14,303.13,1342.15,266.12,1343.16,232.11,1344.17,201.10,1345.18,173.9,1346.19,148.8,1347.20,140.7,1348.21,133.6,1349.22,127.5,1350.23,122.4,1351.24,118.3,1352.25,115.2,1353.26,113.1,1354.27,1.0,1355.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv37_4r1r1r1r1(x0,x1,x2,x3)
% 61.20/12.65 1385:4:29:[979.28,71.0,872.27,1357.2,793.26,1358.3,717.25,1359.4,644.24,1360.5,620.23,1361.6,597.22,1362.8,575.21,1363.9,536.20,1364.10,516.19,1365.11,480.18,1366.12,462.17,1367.13,445.16,1368.14,399.15,1369.15,343.14,1370.16,303.13,1371.17,266.12,1372.18,232.11,1373.19,201.10,1374.20,173.9,1375.21,148.8,1376.22,140.7,1377.23,133.6,1378.24,127.5,1379.25,122.4,1380.26,118.3,1381.27,115.2,1382.28,113.1,1383.29,1.0,1384.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv19_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv22_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 61.20/12.65 1416:1:31:[1180.30,72.0,1064.29,1386.1,979.28,1387.2,872.27,1388.3,793.26,1389.4,717.25,1390.5,644.24,1391.6,620.23,1392.7,597.22,1393.8,575.21,1394.9,536.20,1395.10,516.19,1396.11,480.18,1397.12,462.17,1398.13,445.16,1399.14,399.15,1400.15,343.14,1401.16,303.13,1402.17,266.12,1403.18,232.11,1404.19,201.10,1405.20,173.9,1406.21,148.8,1407.22,140.7,1408.23,133.6,1409.24,127.5,1410.25,122.4,1411.26,118.3,1412.27,115.2,1413.28,113.1,1414.29,1.0,1415.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30)
% 61.20/12.65 1447:1:31:[1180.30,73.0,1064.29,1417.1,979.28,1418.2,872.27,1419.3,793.26,1420.4,717.25,1421.5,644.24,1422.6,620.23,1423.7,597.22,1424.8,575.21,1425.9,536.20,1426.10,516.19,1427.11,480.18,1428.12,462.17,1429.13,445.16,1430.14,399.15,1431.15,343.14,1432.16,303.13,1433.17,266.12,1434.18,232.11,1435.19,201.10,1436.20,173.9,1437.21,148.8,1438.22,140.7,1439.23,133.6,1440.24,127.5,1441.25,122.4,1442.26,118.3,1443.27,115.2,1444.28,113.1,1445.29,1.0,1446.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,skc32)
% 61.20/12.65 1478:1:31:[1180.30,74.1,1064.29,1448.2,979.28,1449.3,872.27,1450.4,793.26,1451.5,717.25,1452.6,644.24,1453.7,620.23,1454.8,597.22,1455.9,575.21,1456.10,536.20,1457.11,516.19,1458.12,480.18,1459.13,462.17,1460.14,445.16,1461.15,399.15,1462.16,343.14,1463.17,303.13,1464.18,266.12,1465.19,232.11,1466.20,201.10,1467.21,173.9,1468.22,148.8,1469.23,140.7,1470.24,133.6,1471.25,127.5,1472.26,122.4,1473.27,118.3,1474.28,115.2,1475.29,113.1,1476.30,1.0,1477.31]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,skc33) ->
% 61.20/12.65 1507:4:29:[979.28,75.0,872.27,1479.1,793.26,1480.2,717.25,1481.3,644.24,1482.4,620.23,1483.5,597.22,1484.6,575.21,1485.7,536.20,1486.9,516.19,1487.10,480.18,1488.11,462.17,1489.12,445.16,1490.13,399.15,1491.14,343.14,1492.15,303.13,1493.16,266.12,1494.17,232.11,1495.18,201.10,1496.19,173.9,1497.20,148.8,1498.21,140.7,1499.22,133.6,1500.23,127.5,1501.24,122.4,1502.25,118.3,1503.26,115.2,1504.27,113.1,1505.28,1.0,1506.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv21_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 61.20/12.65 1538:4:31:[1180.30,76.0,1064.29,1508.1,979.28,1509.2,872.27,1510.3,793.26,1511.4,717.25,1512.6,644.24,1513.7,620.23,1514.8,597.22,1515.9,575.21,1516.10,536.20,1517.11,516.19,1518.12,480.18,1519.13,462.17,1520.14,445.16,1521.15,399.15,1522.16,343.14,1523.17,303.13,1524.18,266.12,1525.19,232.11,1526.20,201.10,1527.21,173.9,1528.22,148.8,1529.23,140.7,1530.24,133.6,1531.25,127.5,1532.26,122.4,1533.27,118.3,1534.28,115.2,1535.29,113.1,1536.30,1.0,1537.31]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) -> ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30),ssPv38_3r1r1r1(x0,x1,x2),ssPv39_2r1r1(x0,x1)
% 61.20/12.65 1570:1:32:[1416.31,77.0,1180.30,1539.1,1064.29,1540.2,979.28,1541.3,872.27,1542.4,793.26,1543.5,717.25,1544.6,644.24,1545.7,620.23,1546.8,597.22,1547.9,575.21,1548.10,536.20,1549.11,516.19,1550.12,480.18,1551.13,462.17,1552.14,445.16,1553.15,399.15,1554.16,343.14,1555.17,303.13,1556.18,266.12,1557.19,232.11,1558.20,201.10,1559.21,173.9,1560.22,148.8,1561.23,140.7,1562.24,133.6,1563.25,127.5,1564.26,122.4,1565.27,118.3,1566.28,115.2,1567.29,113.1,1568.30,1.0,1569.31]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31)
% 61.20/12.65 1602:4:32:[1416.31,78.0,1180.30,1571.1,1064.29,1572.2,979.28,1573.3,872.27,1574.4,793.26,1575.5,717.25,1576.6,644.24,1577.7,620.23,1578.8,597.22,1579.9,575.21,1580.10,536.20,1581.11,516.19,1582.12,480.18,1583.13,462.17,1584.14,445.16,1585.15,399.15,1586.16,343.14,1587.17,303.13,1588.18,266.12,1589.19,232.11,1590.21,201.10,1591.22,173.9,1592.23,148.8,1593.24,140.7,1594.25,133.6,1595.26,127.5,1596.27,122.4,1597.28,118.3,1598.29,115.2,1599.30,113.1,1600.31,1.0,1601.32]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv35_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv39_2r1r1(x0,x1)
% 61.20/12.65 1633:4:31:[1180.30,79.0,1064.29,1603.2,979.28,1604.3,872.27,1605.4,793.26,1606.5,717.25,1607.6,644.24,1608.7,620.23,1609.8,597.22,1610.9,575.21,1611.10,536.20,1612.11,516.19,1613.12,480.18,1614.14,462.17,1615.15,445.16,1616.16,399.15,1617.18,343.14,1618.19,303.13,1619.20,266.12,1620.21,232.11,1621.22,201.10,1622.23,173.9,1623.24,148.8,1624.25,140.7,1625.26,133.6,1626.27,127.5,1627.28,122.4,1628.29,118.3,1629.30,115.2,1630.31,113.1,1631.32,1.0,1632.33]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30),ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv22_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 61.20/12.65 1666:1:33:[1570.32,80.0,1416.31,1634.1,1180.30,1635.2,1064.29,1636.3,979.28,1637.4,872.27,1638.5,793.26,1639.6,717.25,1640.7,644.24,1641.8,620.23,1642.9,597.22,1643.10,575.21,1644.11,536.20,1645.12,516.19,1646.13,480.18,1647.14,462.17,1648.15,445.16,1649.16,399.15,1650.17,343.14,1651.18,303.13,1652.19,266.12,1653.20,232.11,1654.21,201.10,1655.22,173.9,1656.23,148.8,1657.24,140.7,1658.25,133.6,1659.26,127.5,1660.27,122.4,1661.28,118.3,1662.29,115.2,1663.30,113.1,1664.31,1.0,1665.32]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32)
% 61.20/12.65 1698:4:32:[1416.31,81.0,1180.30,1667.1,1064.29,1668.2,979.28,1669.3,872.27,1670.4,793.26,1671.5,717.25,1672.6,644.24,1673.7,620.23,1674.8,597.22,1675.9,575.21,1676.11,536.20,1677.12,516.19,1678.13,480.18,1679.14,462.17,1680.15,445.16,1681.16,399.15,1682.17,343.14,1683.18,303.13,1684.19,266.12,1685.20,232.11,1686.21,201.10,1687.22,173.9,1688.23,148.8,1689.24,140.7,1690.25,133.6,1691.26,127.5,1692.27,122.4,1693.28,118.3,1694.29,115.2,1695.30,113.1,1696.31,1.0,1697.32]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) -> ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv17_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 61.20/12.65 1732:1:34:[1666.33,82.0,1570.32,1699.1,1416.31,1700.2,1180.30,1701.3,1064.29,1702.4,979.28,1703.5,872.27,1704.6,793.26,1705.7,717.25,1706.8,644.24,1707.9,620.23,1708.10,597.22,1709.11,575.21,1710.12,536.20,1711.13,516.19,1712.14,480.18,1713.15,462.17,1714.16,445.16,1715.17,399.15,1716.18,343.14,1717.19,303.13,1718.20,266.12,1719.21,232.11,1720.22,201.10,1721.23,173.9,1722.24,148.8,1723.25,140.7,1724.26,133.6,1725.27,127.5,1726.28,122.4,1727.29,118.3,1728.30,115.2,1729.31,113.1,1730.32,1.0,1731.33]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33)
% 61.20/12.65 1764:4:32:[1416.31,83.0,1180.30,1733.2,1064.29,1734.3,979.28,1735.4,872.27,1736.5,793.26,1737.6,717.25,1738.8,644.24,1739.10,620.23,1740.11,597.22,1741.12,575.21,1742.13,536.20,1743.14,516.19,1744.15,480.18,1745.17,462.17,1746.18,445.16,1747.19,399.15,1748.20,343.14,1749.21,303.13,1750.22,266.12,1751.23,232.11,1752.24,201.10,1753.25,173.9,1754.26,148.8,1755.27,140.7,1756.28,133.6,1757.29,127.5,1758.30,122.4,1759.31,118.3,1760.32,115.2,1761.33,113.1,1762.34,1.0,1763.35]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv17_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ->
% 61.20/12.65 1799:1:35:[1732.34,84.0,1666.33,1765.1,1570.32,1766.2,1416.31,1767.3,1180.30,1768.4,1064.29,1769.5,979.28,1770.6,872.27,1771.7,793.26,1772.8,717.25,1773.9,644.24,1774.10,620.23,1775.11,597.22,1776.12,575.21,1777.13,536.20,1778.14,516.19,1779.15,480.18,1780.16,462.17,1781.17,445.16,1782.18,399.15,1783.19,343.14,1784.20,303.13,1785.21,266.12,1786.22,232.11,1787.23,201.10,1788.24,173.9,1789.25,148.8,1790.26,140.7,1791.27,133.6,1792.28,127.5,1793.29,122.4,1794.30,118.3,1795.31,115.2,1796.32,113.1,1797.33,1.0,1798.34]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34)
% 61.20/12.65 1833:4:34:[1666.33,85.0,1570.32,1800.2,1416.31,1801.3,1180.30,1802.4,1064.29,1803.5,979.28,1804.6,872.27,1805.7,793.26,1806.8,717.25,1807.9,644.24,1808.10,620.23,1809.11,597.22,1810.12,575.21,1811.13,536.20,1812.14,516.19,1813.15,480.18,1814.16,462.17,1815.17,445.16,1816.18,399.15,1817.19,343.14,1818.20,303.13,1819.21,266.12,1820.22,232.11,1821.24,201.10,1822.25,173.9,1823.26,148.8,1824.27,140.7,1825.28,133.6,1826.29,127.5,1827.30,122.4,1828.31,118.3,1829.33,115.2,1830.34,113.1,1831.35,1.0,1832.36]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv38_3r1r1r1(x0,x1,x2) -> ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33)
% 61.20/12.65 1866:4:33:[1570.32,86.1,1416.31,1834.3,1180.30,1835.4,1064.29,1836.5,979.28,1837.6,872.27,1838.7,793.26,1839.8,717.25,1840.9,644.24,1841.10,620.23,1842.11,597.22,1843.12,575.21,1844.13,536.20,1845.14,516.19,1846.15,480.18,1847.16,462.17,1848.17,445.16,1849.18,399.15,1850.19,343.14,1851.20,303.13,1852.21,266.12,1853.22,232.11,1854.23,201.10,1855.24,173.9,1856.25,148.8,1857.26,140.7,1858.27,133.6,1859.28,127.5,1860.29,122.4,1861.30,118.3,1862.31,115.2,1863.32,113.1,1864.33,1.0,1865.34]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30) -> ssPv8_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 61.20/12.65 1900:4:34:[1666.33,87.0,1570.32,1867.2,1416.31,1868.3,1180.30,1869.4,1064.29,1870.5,979.28,1871.6,872.27,1872.8,793.26,1873.9,717.25,1874.11,644.24,1875.12,620.23,1876.13,597.22,1877.14,575.21,1878.15,536.20,1879.16,516.19,1880.17,480.18,1881.18,462.17,1882.19,445.16,1883.20,399.15,1884.21,343.14,1885.22,303.13,1886.23,266.12,1887.24,232.11,1888.25,201.10,1889.26,173.9,1890.27,148.8,1891.28,140.7,1892.30,133.6,1893.31,127.5,1894.32,122.4,1895.33,118.3,1896.34,115.2,1897.35,113.1,1898.36,1.0,1899.37]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv34_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ->
% 61.20/12.65 1935:4:35:[1732.34,88.0,1666.33,1901.1,1570.32,1902.2,1416.31,1903.3,1180.30,1904.4,1064.29,1905.5,979.28,1906.6,872.27,1907.7,793.26,1908.8,717.25,1909.9,644.24,1910.10,620.23,1911.11,597.22,1912.12,575.21,1913.13,536.20,1914.14,516.19,1915.15,480.18,1916.16,462.17,1917.17,445.16,1918.18,399.15,1919.19,343.14,1920.20,303.13,1921.21,266.12,1922.23,232.11,1923.24,201.10,1924.25,173.9,1925.26,148.8,1926.27,140.7,1927.28,133.6,1928.29,127.5,1929.30,122.4,1930.31,118.3,1931.32,115.2,1932.33,113.1,1933.34,1.0,1934.35]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv34_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 61.20/12.65 1970:4:35:[1732.34,89.0,1666.33,1936.1,1570.32,1937.2,1416.31,1938.3,1180.30,1939.4,1064.29,1940.5,979.28,1941.6,872.27,1942.7,793.26,1943.8,717.25,1944.9,644.24,1945.10,620.23,1946.11,597.22,1947.12,575.21,1948.13,536.20,1949.14,516.19,1950.15,480.18,1951.16,462.17,1952.17,445.16,1953.18,399.15,1954.19,343.14,1955.20,303.13,1956.21,266.12,1957.22,232.11,1958.23,201.10,1959.24,173.9,1960.25,148.8,1961.26,140.7,1962.27,133.6,1963.28,127.5,1964.29,122.4,1965.30,118.3,1966.32,115.2,1967.33,113.1,1968.34,1.0,1969.35]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv38_3r1r1r1(x0,x1,x2) -> ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34),ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 61.20/12.65 2006:1:36:[1799.35,90.0,1732.34,1971.1,1666.33,1972.2,1570.32,1973.3,1416.31,1974.4,1180.30,1975.5,1064.29,1976.6,979.28,1977.7,872.27,1978.8,793.26,1979.9,717.25,1980.10,644.24,1981.11,620.23,1982.12,597.22,1983.13,575.21,1984.14,536.20,1985.15,516.19,1986.16,480.18,1987.17,462.17,1988.18,445.16,1989.19,399.15,1990.20,343.14,1991.21,303.13,1992.22,266.12,1993.23,232.11,1994.24,201.10,1995.25,173.9,1996.26,148.8,1997.27,140.7,1998.28,133.6,1999.29,127.5,2000.30,122.4,2001.31,118.3,2002.32,115.2,2003.33,113.1,2004.34,1.0,2005.35]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35)
% 61.20/12.65 2041:4:35:[1732.34,91.0,1666.33,2007.2,1570.32,2008.3,1416.31,2009.4,1180.30,2010.5,1064.29,2011.6,979.28,2012.7,872.27,2013.8,793.26,2014.10,717.25,2015.11,644.24,2016.12,620.23,2017.13,597.22,2018.14,575.21,2019.15,536.20,2020.16,516.19,2021.17,480.18,2022.18,462.17,2023.19,445.16,2024.20,399.15,2025.21,343.14,2026.22,303.13,2027.23,266.12,2028.24,232.11,2029.25,201.10,2030.26,173.9,2031.27,148.8,2032.28,140.7,2033.29,133.6,2034.30,127.5,2035.31,122.4,2036.32,118.3,2037.34,115.2,2038.35,113.1,2039.36,1.0,2040.37]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34),ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv38_3r1r1r1(x0,x1,x2) -> ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26)
% 61.20/12.65 2078:1:37:[2006.36,92.0,1799.35,2042.1,1732.34,2043.2,1666.33,2044.3,1570.32,2045.4,1416.31,2046.5,1180.30,2047.6,1064.29,2048.7,979.28,2049.8,872.27,2050.9,793.26,2051.10,717.25,2052.11,644.24,2053.12,620.23,2054.13,597.22,2055.14,575.21,2056.15,536.20,2057.16,516.19,2058.17,480.18,2059.18,462.17,2060.19,445.16,2061.20,399.15,2062.21,343.14,2063.22,303.13,2064.23,266.12,2065.24,232.11,2066.25,201.10,2067.26,173.9,2068.27,148.8,2069.28,140.7,2070.29,133.6,2071.30,127.5,2072.31,122.4,2073.32,118.3,2074.33,115.2,2075.34,113.1,2076.35,1.0,2077.36]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36)
% 61.20/12.65 2114:4:36:[1799.35,93.0,1732.34,2079.1,1666.33,2080.2,1570.32,2081.3,1416.31,2082.4,1180.30,2083.5,1064.29,2084.6,979.28,2085.7,872.27,2086.8,793.26,2087.9,717.25,2088.10,644.24,2089.11,620.23,2090.12,597.22,2091.13,575.21,2092.14,536.20,2093.15,516.19,2094.16,480.18,2095.17,462.17,2096.18,445.16,2097.20,399.15,2098.21,343.14,2099.22,303.13,2100.23,266.12,2101.24,232.11,2102.25,201.10,2103.26,173.9,2104.27,148.8,2105.28,140.7,2106.29,133.6,2107.30,127.5,2108.31,122.4,2109.32,118.3,2110.33,115.2,2111.34,113.1,2112.35,1.0,2113.36]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv5_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35),ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv19_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
% 61.20/12.65 2152:1:38:[2078.37,94.0,2006.36,2115.1,1799.35,2116.2,1732.34,2117.3,1666.33,2118.4,1570.32,2119.5,1416.31,2120.6,1180.30,2121.7,1064.29,2122.8,979.28,2123.9,872.27,2124.10,793.26,2125.11,717.25,2126.12,644.24,2127.13,620.23,2128.14,597.22,2129.15,575.21,2130.16,536.20,2131.17,516.19,2132.18,480.18,2133.19,462.17,2134.20,445.16,2135.21,399.15,2136.22,343.14,2137.23,303.13,2138.24,266.12,2139.25,232.11,2140.26,201.10,2141.27,173.9,2142.28,148.8,2143.29,140.7,2144.30,133.6,2145.31,127.5,2146.32,122.4,2147.33,118.3,2148.34,115.2,2149.35,113.1,2150.36,1.0,2151.37]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37)
% 61.20/12.65 2188:4:36:[1799.35,95.0,1732.34,2153.1,1666.33,2154.3,1570.32,2155.4,1416.31,2156.5,1180.30,2157.6,1064.29,2158.7,979.28,2159.8,872.27,2160.9,793.26,2161.10,717.25,2162.11,644.24,2163.12,620.23,2164.13,597.22,2165.14,575.21,2166.15,536.20,2167.16,516.19,2168.17,480.18,2169.18,462.17,2170.19,445.16,2171.21,399.15,2172.22,343.14,2173.23,303.13,2174.24,266.12,2175.25,232.11,2176.26,201.10,2177.27,173.9,2178.28,148.8,2179.29,140.7,2180.30,133.6,2181.31,127.5,2182.32,122.4,2183.33,118.3,2184.34,115.2,2185.35,113.1,2186.36,1.0,2187.37]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32),ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv5_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35),ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25)
% 61.20/12.65 2225:4:37:[2006.36,96.0,1799.35,2189.2,1732.34,2190.3,1666.33,2191.4,1570.32,2192.5,1416.31,2193.6,1180.30,2194.7,1064.29,2195.8,979.28,2196.9,872.27,2197.10,793.26,2198.11,717.25,2199.13,644.24,2200.14,620.23,2201.15,597.22,2202.16,575.21,2203.17,536.20,2204.18,516.19,2205.19,480.18,2206.20,462.17,2207.21,445.16,2208.22,399.15,2209.23,343.14,2210.24,303.13,2211.25,266.12,2212.26,232.11,2213.27,201.10,2214.28,173.9,2215.29,148.8,2216.30,140.7,2217.31,133.6,2218.32,127.5,2219.33,122.4,2220.34,118.3,2221.35,115.2,2222.36,113.1,2223.37,1.0,2224.38]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) -> ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv40_1r1(x0)
% 61.20/12.65 2262:4:37:[2006.36,97.0,1799.35,2226.2,1732.34,2227.3,1666.33,2228.4,1570.32,2229.5,1416.31,2230.6,1180.30,2231.7,1064.29,2232.8,979.28,2233.9,872.27,2234.10,793.26,2235.11,717.25,2236.12,644.24,2237.13,620.23,2238.14,597.22,2239.15,575.21,2240.16,536.20,2241.17,516.19,2242.18,480.18,2243.19,462.17,2244.20,445.16,2245.21,399.15,2246.22,343.14,2247.23,303.13,2248.24,266.12,2249.25,232.11,2250.27,201.10,2251.28,173.9,2252.29,148.8,2253.30,140.7,2254.31,133.6,2255.32,127.5,2256.33,122.4,2257.34,118.3,2258.36,115.2,2259.37,113.1,2260.38,1.0,2261.39]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv38_3r1r1r1(x0,x1,x2) -> ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26)
% 61.20/12.65 2299:4:37:[2006.36,98.0,1799.35,2263.2,1732.34,2264.3,1666.33,2265.4,1570.32,2266.5,1416.31,2267.6,1180.30,2268.7,1064.29,2269.8,979.28,2270.9,872.27,2271.10,793.26,2272.11,717.25,2273.12,644.24,2274.13,620.23,2275.14,597.22,2276.15,575.21,2277.16,536.20,2278.17,516.19,2279.18,480.18,2280.19,462.17,2281.20,445.16,2282.21,399.15,2283.22,343.14,2284.23,303.13,2285.24,266.12,2286.25,232.11,2287.26,201.10,2288.28,173.9,2289.29,148.8,2290.30,140.7,2291.31,133.6,2292.32,127.5,2293.33,122.4,2294.34,118.3,2295.35,115.2,2296.36,113.1,2297.37,1.0,2298.38]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv19_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 61.20/12.65 2336:4:37:[2006.36,99.0,1799.35,2300.2,1732.34,2301.3,1666.33,2302.4,1570.32,2303.5,1416.31,2304.6,1180.30,2305.7,1064.29,2306.8,979.28,2307.9,872.27,2308.10,793.26,2309.12,717.25,2310.13,644.24,2311.14,620.23,2312.15,597.22,2313.16,575.21,2314.17,536.20,2315.18,516.19,2316.19,480.18,2317.20,462.17,2318.21,445.16,2319.22,399.15,2320.23,343.14,2321.24,303.13,2322.25,266.12,2323.26,232.11,2324.27,201.10,2325.28,173.9,2326.29,148.8,2327.30,140.7,2328.31,133.6,2329.32,127.5,2330.33,122.4,2331.34,118.3,2332.35,115.2,2333.36,113.1,2334.37,1.0,2335.38]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36),ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) -> ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30),ssPv22_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 61.20/12.65 2375:1:39:[2152.38,100.0,2078.37,2337.1,2006.36,2338.2,1799.35,2339.3,1732.34,2340.4,1666.33,2341.5,1570.32,2342.6,1416.31,2343.7,1180.30,2344.8,1064.29,2345.9,979.28,2346.10,872.27,2347.11,793.26,2348.12,717.25,2349.13,644.24,2350.14,620.23,2351.15,597.22,2352.16,575.21,2353.17,536.20,2354.18,516.19,2355.19,480.18,2356.20,462.17,2357.21,445.16,2358.22,399.15,2359.23,343.14,2360.24,303.13,2361.25,266.12,2362.26,232.11,2363.27,201.10,2364.28,173.9,2365.29,148.8,2366.30,140.7,2367.31,133.6,2368.32,127.5,2369.33,122.4,2370.34,118.3,2371.35,115.2,2372.36,113.1,2373.37,1.0,2374.38]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38)
% 61.20/12.65 2412:4:37:[2006.36,101.0,1799.35,2376.2,1732.34,2377.4,1666.33,2378.5,1570.32,2379.7,1416.31,2380.8,1180.30,2381.9,1064.29,2382.10,979.28,2383.11,872.27,2384.12,793.26,2385.13,717.25,2386.14,644.24,2387.15,620.23,2388.16,597.22,2389.17,575.21,2390.18,536.20,2391.19,516.19,2392.20,480.18,2393.21,462.17,2394.22,445.16,2395.23,399.15,2396.24,343.14,2397.26,303.13,2398.27,266.12,2399.28,232.11,2400.29,201.10,2401.30,173.9,2402.31,148.8,2403.32,140.7,2404.33,133.6,2405.34,127.5,2406.35,122.4,2407.36,118.3,2408.37,115.2,2409.38,113.1,2410.39,1.0,2411.40]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36),ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33),ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ->
% 61.20/12.65 2451:4:39:[2152.38,102.0,2078.37,2413.1,2006.36,2414.2,1799.35,2415.3,1732.34,2416.4,1666.33,2417.5,1570.32,2418.6,1416.31,2419.7,1180.30,2420.8,1064.29,2421.9,979.28,2422.10,872.27,2423.11,793.26,2424.12,717.25,2425.13,644.24,2426.14,620.23,2427.15,597.22,2428.16,575.21,2429.17,536.20,2430.18,516.19,2431.19,480.18,2432.20,462.17,2433.21,445.16,2434.22,399.15,2435.23,343.14,2436.25,303.13,2437.26,266.12,2438.27,232.11,2439.28,201.10,2440.29,173.9,2441.30,148.8,2442.31,140.7,2443.32,133.6,2444.33,127.5,2445.34,122.4,2446.36,118.3,2447.37,115.2,2448.38,113.1,2449.39,1.0,2450.40]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv37_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 61.20/12.65 2490:4:39:[2152.38,103.0,2078.37,2452.2,2006.36,2453.3,1799.35,2454.4,1732.34,2455.5,1666.33,2456.6,1570.32,2457.7,1416.31,2458.8,1180.30,2459.9,1064.29,2460.10,979.28,2461.11,872.27,2462.12,793.26,2463.13,717.25,2464.15,644.24,2465.16,620.23,2466.17,597.22,2467.18,575.21,2468.19,536.20,2469.20,516.19,2470.21,480.18,2471.22,462.17,2472.23,445.16,2473.24,399.15,2474.25,343.14,2475.27,303.13,2476.28,266.12,2477.29,232.11,2478.30,201.10,2479.31,173.9,2480.32,148.8,2481.33,140.7,2482.34,133.6,2483.35,127.5,2484.36,122.4,2485.37,118.3,2486.38,115.2,2487.39,113.1,2488.40,1.0,2489.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 2529:4:39:[2152.38,104.0,2078.37,2491.1,2006.36,2492.2,1799.35,2493.3,1732.34,2494.4,1666.33,2495.5,1570.32,2496.6,1416.31,2497.7,1180.30,2498.8,1064.29,2499.9,979.28,2500.10,872.27,2501.11,793.26,2502.12,717.25,2503.13,644.24,2504.14,620.23,2505.15,597.22,2506.16,575.21,2507.17,536.20,2508.18,516.19,2509.19,480.18,2510.20,462.17,2511.21,445.16,2512.22,399.15,2513.23,343.14,2514.24,303.13,2515.26,266.12,2516.27,232.11,2517.28,201.10,2518.30,173.9,2519.31,148.8,2520.32,140.7,2521.33,133.6,2522.34,127.5,2523.35,122.4,2524.36,118.3,2525.37,115.2,2526.38,113.1,2527.39,1.0,2528.40]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33)
% 61.20/12.65 2568:4:39:[2152.38,105.0,2078.37,2530.1,2006.36,2531.2,1799.35,2532.3,1732.34,2533.4,1666.33,2534.5,1570.32,2535.6,1416.31,2536.7,1180.30,2537.8,1064.29,2538.9,979.28,2539.10,872.27,2540.11,793.26,2541.12,717.25,2542.13,644.24,2543.14,620.23,2544.15,597.22,2545.16,575.21,2546.17,536.20,2547.18,516.19,2548.19,480.18,2549.20,462.17,2550.21,445.16,2551.22,399.15,2552.23,343.14,2553.24,303.13,2554.25,266.12,2555.26,232.11,2556.27,201.10,2557.28,173.9,2558.29,148.8,2559.30,140.7,2560.31,133.6,2561.32,127.5,2562.33,122.4,2563.34,118.3,2564.35,115.2,2565.36,113.1,2566.37,1.0,2567.38]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34),ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 61.20/12.65 2608:4:40:[2375.39,106.0,2152.38,2569.1,2078.37,2570.2,2006.36,2571.3,1799.35,2572.4,1732.34,2573.5,1666.33,2574.6,1570.32,2575.7,1416.31,2576.8,1180.30,2577.9,1064.29,2578.10,979.28,2579.11,872.27,2580.12,793.26,2581.13,717.25,2582.14,644.24,2583.15,620.23,2584.16,597.22,2585.17,575.21,2586.18,536.20,2587.19,516.19,2588.20,480.18,2589.21,462.17,2590.22,445.16,2591.23,399.15,2592.24,343.14,2593.25,303.13,2594.26,266.12,2595.27,232.11,2596.28,201.10,2597.29,173.9,2598.31,148.8,2599.32,140.7,2600.33,133.6,2601.34,127.5,2602.35,122.4,2603.36,118.3,2604.37,115.2,2605.38,113.1,2606.40,1.0,2607.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29)
% 61.20/12.65 2648:4:40:[2375.39,107.0,2152.38,2609.2,2078.37,2610.3,2006.36,2611.4,1799.35,2612.5,1732.34,2613.6,1666.33,2614.7,1570.32,2615.8,1416.31,2616.9,1180.30,2617.10,1064.29,2618.11,979.28,2619.12,872.27,2620.13,793.26,2621.14,717.25,2622.15,644.24,2623.16,620.23,2624.17,597.22,2625.18,575.21,2626.19,536.20,2627.20,516.19,2628.21,480.18,2629.22,462.17,2630.23,445.16,2631.24,399.15,2632.25,343.14,2633.26,303.13,2634.27,266.12,2635.28,232.11,2636.29,201.10,2637.30,173.9,2638.31,148.8,2639.32,140.7,2640.33,133.6,2641.34,127.5,2642.35,122.4,2643.36,118.3,2644.37,115.2,2645.38,113.1,2646.39,1.0,2647.40]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39) -> ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 2688:4:40:[2375.39,108.0,2152.38,2649.1,2078.37,2650.2,2006.36,2651.3,1799.35,2652.4,1732.34,2653.5,1666.33,2654.6,1570.32,2655.7,1416.31,2656.8,1180.30,2657.9,1064.29,2658.10,979.28,2659.11,872.27,2660.12,793.26,2661.14,717.25,2662.15,644.24,2663.16,620.23,2664.17,597.22,2665.18,575.21,2666.19,536.20,2667.20,516.19,2668.21,480.18,2669.22,462.17,2670.23,445.16,2671.24,399.15,2672.25,343.14,2673.26,303.13,2674.27,266.12,2675.28,232.11,2676.29,201.10,2677.30,173.9,2678.31,148.8,2679.32,140.7,2680.33,133.6,2681.34,127.5,2682.36,122.4,2683.37,118.3,2684.38,115.2,2685.39,113.1,2686.40,1.0,2687.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv36_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 61.20/12.65 2727:4:39:[2152.38,109.1,2078.37,2689.3,2006.36,2690.4,1799.35,2691.5,1732.34,2692.6,1666.33,2693.7,1570.32,2694.8,1416.31,2695.9,1180.30,2696.10,1064.29,2697.11,979.28,2698.12,872.27,2699.14,793.26,2700.15,717.25,2701.17,644.24,2702.18,620.23,2703.19,597.22,2704.20,575.21,2705.21,536.20,2706.22,516.19,2707.23,480.18,2708.24,462.17,2709.25,445.16,2710.26,399.15,2711.27,343.14,2712.28,303.13,2713.29,266.12,2714.30,232.11,2715.31,201.10,2716.32,173.9,2717.33,148.8,2718.34,140.7,2719.35,133.6,2720.36,127.5,2721.37,122.4,2722.38,118.3,2723.39,115.2,2724.40,113.1,2725.41,1.0,2726.42]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37),ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ->
% 61.20/12.65 2767:4:40:[2375.39,110.0,2152.38,2728.2,2078.37,2729.3,2006.36,2730.4,1799.35,2731.5,1732.34,2732.6,1666.33,2733.7,1570.32,2734.8,1416.31,2735.9,1180.30,2736.10,1064.29,2737.11,979.28,2738.12,872.27,2739.13,793.26,2740.14,717.25,2741.15,644.24,2742.16,620.23,2743.17,597.22,2744.18,575.21,2745.19,536.20,2746.20,516.19,2747.21,480.18,2748.22,462.17,2749.23,445.16,2750.24,399.15,2751.25,343.14,2752.26,303.13,2753.27,266.12,2754.28,232.11,2755.30,201.10,2756.31,173.9,2757.32,148.8,2758.33,140.7,2759.34,133.6,2760.35,127.5,2761.36,122.4,2762.37,118.3,2763.38,115.2,2764.39,113.1,2765.40,1.0,2766.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 61.20/12.65 2807:4:40:[2375.39,111.1,2152.38,2768.3,2078.37,2769.4,2006.36,2770.5,1799.35,2771.6,1732.34,2772.7,1666.33,2773.8,1570.32,2774.9,1416.31,2775.11,1180.30,2776.12,1064.29,2777.13,979.28,2778.14,872.27,2779.15,793.26,2780.16,717.25,2781.18,644.24,2782.19,620.23,2783.20,597.22,2784.21,575.21,2785.22,536.20,2786.23,516.19,2787.24,480.18,2788.25,462.17,2789.26,445.16,2790.27,399.15,2791.28,343.14,2792.29,303.13,2793.30,266.12,2794.31,232.11,2795.32,201.10,2796.33,173.9,2797.34,148.8,2798.35,140.7,2799.36,133.6,2800.37,127.5,2801.38,122.4,2802.39,118.3,2803.40,115.2,2804.41,113.1,2805.42,1.0,2806.43]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ->
% 61.20/12.65 2847:4:40:[2375.39,112.0,2152.38,2808.3,2078.37,2809.4,2006.36,2810.5,1799.35,2811.6,1732.34,2812.7,1666.33,2813.8,1570.32,2814.9,1416.31,2815.10,1180.30,2816.11,1064.29,2817.12,979.28,2818.14,872.27,2819.15,793.26,2820.16,717.25,2821.17,644.24,2822.18,620.23,2823.19,597.22,2824.20,575.21,2825.21,536.20,2826.22,516.19,2827.23,480.18,2828.24,462.17,2829.25,445.16,2830.26,399.15,2831.27,343.14,2832.28,303.13,2833.29,266.12,2834.30,232.11,2835.31,201.10,2836.32,173.9,2837.33,148.8,2838.34,140.7,2839.35,133.6,2840.36,127.5,2841.37,122.4,2842.38,118.3,2843.39,115.2,2844.40,113.1,2845.41,1.0,2846.42]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv3_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37),ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) -> ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30)
% 61.20/12.65
% 61.20/12.65 Most General Atoms: ssNder1_0 ssNder1_1r1(x0) ssNder1_2r1r1(x0,x1) ssNder1_3r1r1r1(x0,x1,x2) ssNder1_4r1r1r1r1(x0,x1,x2,x3) ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv36_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv38_3r1r1r1(x0,x1,x2) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv24_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv40_1r1(x0) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) ssPv18_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) ssPv21_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ssNder1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) ssNder1_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28) ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) ssNder1_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29) ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28) ssPv37_4r1r1r1r1(x0,x1,x2,x3) ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) ssPv19_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssPv22_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssNder1_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30) ssPv10_31r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30) ssPv39_2r1r1(x0,x1) ssNder1_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31) ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31) ssPv35_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32) ssPv17_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ssNder1_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33) ssNder1_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34) ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33) ssPv8_33r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32) ssPv34_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34) ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35) ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ssNder1_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36) ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv5_36r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35) ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29) ssNder1_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37) ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36) ssNder1_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38) ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38) ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39) ssPv3_38r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37)
% 61.20/12.65
% 61.20/12.65 === Starting SPASS-SCL-FOL A Little Less Naive, considering 111 atoms initially, heuristics mode: lmodel_grow ===
% 61.20/12.65
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 130
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 164
% 61.20/12.65 === Conflict found: 2767:4:40:[2375.39,110.0,2152.38,2728.2,2078.37,2729.3,2006.36,2730.4,1799.35,2731.5,1732.34,2732.6,1666.33,2733.7,1570.32,2734.8,1416.31,2735.9,1180.30,2736.10,1064.29,2737.11,979.28,2738.12,872.27,2739.13,793.26,2740.14,717.25,2741.15,644.24,2742.16,620.23,2743.17,597.22,2744.18,575.21,2745.19,536.20,2746.20,516.19,2747.21,480.18,2748.22,462.17,2749.23,445.16,2750.24,399.15,2751.25,343.14,2752.26,303.13,2753.27,266.12,2754.28,232.11,2755.30,201.10,2756.31,173.9,2757.32,148.8,2758.33,140.7,2759.34,133.6,2760.35,127.5,2761.36,122.4,2762.37,118.3,2763.38,115.2,2764.39,113.1,2765.40,1.0,2766.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc62, x10 -> skc62, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc33, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc37, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62, x35 -> skc62, x36 -> skc62, x37 -> skc62, x38 -> skc62, x39 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2848:6:57:[2767.1,2608.3,1122.1,2225.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv4_37r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34) -> ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x47,x48,x49,x50,x51,x52,x53,x54,x55,x56),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 211
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 261
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 313
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 360
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 404
% 61.20/12.65 === Conflict found: 1298:4:29:[979.28,68.0,872.27,1270.2,793.26,1271.3,717.25,1272.4,644.24,1273.5,620.23,1274.6,597.22,1275.7,575.21,1276.9,536.20,1277.10,516.19,1278.11,480.18,1279.12,462.17,1280.13,445.16,1281.14,399.15,1282.15,343.14,1283.17,303.13,1284.18,266.12,1285.19,232.11,1286.20,201.10,1287.21,173.9,1288.22,148.8,1289.23,140.7,1290.24,133.6,1291.25,127.5,1292.26,122.4,1293.27,118.3,1294.28,115.2,1295.29,113.1,1296.30,1.0,1297.31]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv40_1r1(x0) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc62, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc33, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc38}
% 61.20/12.65 === Backtracking. Learning clause 2849:3:21:[1298.1,1007.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv40_1r1(x0)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 438
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 482
% 61.20/12.65 === Conflict found: 2490:4:39:[2152.38,103.0,2078.37,2452.2,2006.36,2453.3,1799.35,2454.4,1732.34,2455.5,1666.33,2456.6,1570.32,2457.7,1416.31,2458.8,1180.30,2459.9,1064.29,2460.10,979.28,2461.11,872.27,2462.12,793.26,2463.13,717.25,2464.15,644.24,2465.16,620.23,2466.17,597.22,2467.18,575.21,2468.19,536.20,2469.20,516.19,2470.21,480.18,2471.22,462.17,2472.23,445.16,2473.24,399.15,2474.25,343.14,2475.27,303.13,2476.28,266.12,2477.29,232.11,2478.30,201.10,2479.31,173.9,2480.32,148.8,2481.33,140.7,2482.34,133.6,2483.35,127.5,2484.36,122.4,2485.37,118.3,2486.38,115.2,2487.39,113.1,2488.40,1.0,2489.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv38_3r1r1r1(x0,x1,x2) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc62, x10 -> skc33, x11 -> skc62, x12 -> skc62, x13 -> skc52, x14 -> skc62, x15 -> skc33, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc46, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc62, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62, x35 -> skc62, x36 -> skc62, x37 -> skc62, x38 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2850:4:16:[2490.2,668.1,2451.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv37_4r1r1r1r1(x0,x1,x2,x3) -> ssPv38_3r1r1r1(x0,x1,x2),ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 61.20/12.65 === Conflict found: 1327:4:29:[979.28,69.1,872.27,1299.2,793.26,1300.3,717.25,1301.4,644.24,1302.5,620.23,1303.6,597.22,1304.7,575.21,1305.8,536.20,1306.9,516.19,1307.10,480.18,1308.12,462.17,1309.13,445.16,1310.14,399.15,1311.15,343.14,1312.16,303.13,1313.17,266.12,1314.18,232.11,1315.19,201.10,1316.20,173.9,1317.21,148.8,1318.22,140.7,1319.23,133.6,1320.24,127.5,1321.25,122.4,1322.26,118.3,1323.27,115.2,1324.28,113.1,1325.29,1.0,1326.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv38_3r1r1r1(x0,x1,x2) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc62, x10 -> skc62, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc62, x27 -> skc40, x28 -> skc39}
% 61.20/12.65 === Backtracking. Learning clause 2851:5:59:[1327.3,1035.1,1833.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv23_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50,x51,x52,x53,x54,x55,x56),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x28,x29,x30,x31,x32,x33,x34,x35) -> ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50,x51,x52,x53,x54,x55,x56,x57,x58)
% 61.20/12.65 === Conflict found: 2849:3:21:[1298.1,1007.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv40_1r1(x0) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc62, x10 -> skc33, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2852:6:40:[2849.2,1698.4,1356.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv40_1r1(x0),ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv17_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x32,x33,x34,x35,x36,x37,x38,x39),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x32,x33,x34,x35,x36,x37),ssPv37_4r1r1r1r1(x0,x1,x2,x3)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 543
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 594
% 61.20/12.65 === Conflict found: 1356:4:29:[979.28,70.0,872.27,1328.1,793.26,1329.2,717.25,1330.3,644.24,1331.4,620.23,1332.5,597.22,1333.6,575.21,1334.7,536.20,1335.8,516.19,1336.9,480.18,1337.10,462.17,1338.11,445.16,1339.12,399.15,1340.13,343.14,1341.14,303.13,1342.15,266.12,1343.16,232.11,1344.17,201.10,1345.18,173.9,1346.19,148.8,1347.20,140.7,1348.21,133.6,1349.22,127.5,1350.23,122.4,1351.24,118.3,1352.25,115.2,1353.26,113.1,1354.27,1.0,1355.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv12_29r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv37_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc62, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc33, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc43, x27 -> skc62, x28 -> skc39}
% 61.20/12.65 === Backtracking. Learning clause 2853:3:14:[1356.1,1035.1,845.1,2849.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv37_4r1r1r1r1(x0,x1,x2,x3),ssPv40_1r1(x0)
% 61.20/12.65 === Conflict found: 2767:4:40:[2375.39,110.0,2152.38,2728.2,2078.37,2729.3,2006.36,2730.4,1799.35,2731.5,1732.34,2732.6,1666.33,2733.7,1570.32,2734.8,1416.31,2735.9,1180.30,2736.10,1064.29,2737.11,979.28,2738.12,872.27,2739.13,793.26,2740.14,717.25,2741.15,644.24,2742.16,620.23,2743.17,597.22,2744.18,575.21,2745.19,536.20,2746.20,516.19,2747.21,480.18,2748.22,462.17,2749.23,445.16,2750.24,399.15,2751.25,343.14,2752.26,303.13,2753.27,266.12,2754.28,232.11,2755.30,201.10,2756.31,173.9,2757.32,148.8,2758.33,140.7,2759.34,133.6,2760.35,127.5,2761.36,122.4,2762.37,118.3,2763.38,115.2,2764.39,113.1,2765.40,1.0,2766.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc62, x10 -> skc62, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc46, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc37, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62, x35 -> skc62, x36 -> skc62, x37 -> skc62, x38 -> skc62, x39 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2854:3:39:[2767.3,1122.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,skc37,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 61.20/12.65 === Conflict found: 2849:3:21:[1298.1,1007.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv40_1r1(x0) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc62, x10 -> skc33, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2855:4:32:[2849.2,1698.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) -> ssPv40_1r1(x0),ssPv9_32r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31),ssPv17_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 639
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 694
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 742
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 789
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 833
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 875
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 916
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 958
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 997
% 61.20/12.65 === Conflict found: 2041:4:35:[1732.34,91.0,1666.33,2007.2,1570.32,2008.3,1416.31,2009.4,1180.30,2010.5,1064.29,2011.6,979.28,2012.7,872.27,2013.8,793.26,2014.10,717.25,2015.11,644.24,2016.12,620.23,2017.13,597.22,2018.14,575.21,2019.15,536.20,2020.16,516.19,2021.17,480.18,2022.18,462.17,2023.19,445.16,2024.20,399.15,2025.21,343.14,2026.22,303.13,2027.23,266.12,2028.24,232.11,2029.25,201.10,2030.26,173.9,2031.27,148.8,2032.28,140.7,2033.29,133.6,2034.30,127.5,2035.31,122.4,2036.32,118.3,2037.34,115.2,2038.35,113.1,2039.36,1.0,2040.37]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34),ssPv15_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv38_3r1r1r1(x0,x1,x2) -> ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc33, x11 -> skc33, x12 -> skc33, x13 -> skc62, x14 -> skc33, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc44, x26 -> skc43, x27 -> skc62, x28 -> skc62, x29 -> skc62, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2856:3:15:[2041.1,1970.2,845.1,742.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv38_3r1r1r1(x0,x1,x2) -> ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 61.20/12.65 === Conflict found: 2856:3:15:[2041.1,1970.2,845.1,742.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv38_3r1r1r1(x0,x1,x2) -> ssPv26_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc33, x11 -> skc62, x12 -> skc32, x13 -> skc62, x14 -> skc51}
% 61.20/12.65 === Backtracking. Learning clause 2857:2:13:[2856.2,371.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv38_3r1r1r1(x0,x1,x2) -> ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1056
% 61.20/12.65 === Conflict found: 384:4:13:[266.12,30.0,232.11,372.2,201.10,373.3,173.9,374.4,148.8,375.5,140.7,376.6,133.6,377.7,127.5,378.9,122.4,379.10,118.3,380.11,115.2,381.12,113.1,382.13,1.0,383.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv36_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv38_3r1r1r1(x0,x1,x2) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc32, x11 -> skc57, x12 -> skc54}
% 61.20/12.65 === Backtracking. Learning clause 2858:3:12:[384.1,278.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv36_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1113
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1157
% 61.20/12.65 === Conflict found: 2767:4:40:[2375.39,110.0,2152.38,2728.2,2078.37,2729.3,2006.36,2730.4,1799.35,2731.5,1732.34,2732.6,1666.33,2733.7,1570.32,2734.8,1416.31,2735.9,1180.30,2736.10,1064.29,2737.11,979.28,2738.12,872.27,2739.13,793.26,2740.14,717.25,2741.15,644.24,2742.16,620.23,2743.17,597.22,2744.18,575.21,2745.19,536.20,2746.20,516.19,2747.21,480.18,2748.22,462.17,2749.23,445.16,2750.24,399.15,2751.25,343.14,2752.26,303.13,2753.27,266.12,2754.28,232.11,2755.30,201.10,2756.31,173.9,2757.32,148.8,2758.33,140.7,2759.34,133.6,2760.35,127.5,2761.36,122.4,2762.37,118.3,2763.38,115.2,2764.39,113.1,2765.40,1.0,2766.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc33, x11 -> skc33, x12 -> skc62, x13 -> skc32, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc62, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62, x35 -> skc62, x36 -> skc62, x37 -> skc62, x38 -> skc62, x39 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2859:5:30:[2767.1,2608.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1213
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1261
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1312
% 61.20/12.65 === Conflict found: 2608:4:40:[2375.39,106.0,2152.38,2569.1,2078.37,2570.2,2006.36,2571.3,1799.35,2572.4,1732.34,2573.5,1666.33,2574.6,1570.32,2575.7,1416.31,2576.8,1180.30,2577.9,1064.29,2578.10,979.28,2579.11,872.27,2580.12,793.26,2581.13,717.25,2582.14,644.24,2583.15,620.23,2584.16,597.22,2585.17,575.21,2586.18,536.20,2587.19,516.19,2588.20,480.18,2589.21,462.17,2590.22,445.16,2591.23,399.15,2592.24,343.14,2593.25,303.13,2594.26,266.12,2595.27,232.11,2596.28,201.10,2597.29,173.9,2598.31,148.8,2599.32,140.7,2600.33,133.6,2601.34,127.5,2602.35,122.4,2603.36,118.3,2604.37,115.2,2605.38,113.1,2606.40,1.0,2607.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc33, x11 -> skc33, x12 -> skc33, x13 -> skc33, x14 -> skc33, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc37, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62, x35 -> skc62, x36 -> skc62, x37 -> skc62, x38 -> skc62, x39 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2860:5:27:[2608.3,2648.1,1122.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1360
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1410
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1455
% 61.20/12.65 === Conflict found: 2859:5:30:[2767.1,2608.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc33, x11 -> skc33, x12 -> skc62, x13 -> skc33, x14 -> skc62, x15 -> skc33, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc37}
% 61.20/12.65 === Backtracking. Learning clause 2861:4:21:[2859.5,1122.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv20_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1498
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1534
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1575
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1608
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1646
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1684
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1717
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1749
% 61.20/12.65 === Conflict found: 2608:4:40:[2375.39,106.0,2152.38,2569.1,2078.37,2570.2,2006.36,2571.3,1799.35,2572.4,1732.34,2573.5,1666.33,2574.6,1570.32,2575.7,1416.31,2576.8,1180.30,2577.9,1064.29,2578.10,979.28,2579.11,872.27,2580.12,793.26,2581.13,717.25,2582.14,644.24,2583.15,620.23,2584.16,597.22,2585.17,575.21,2586.18,536.20,2587.19,516.19,2588.20,480.18,2589.21,462.17,2590.22,445.16,2591.23,399.15,2592.24,343.14,2593.25,303.13,2594.26,266.12,2595.27,232.11,2596.28,201.10,2597.29,173.9,2598.31,148.8,2599.32,140.7,2600.33,133.6,2601.34,127.5,2602.35,122.4,2603.36,118.3,2604.37,115.2,2605.38,113.1,2606.40,1.0,2607.41]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39),ssPv11_30r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc33, x11 -> skc33, x12 -> skc54, x13 -> skc33, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc37, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62, x35 -> skc62, x36 -> skc62, x37 -> skc62, x38 -> skc62, x39 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2862:3:39:[2608.4,1122.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv1_40r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,skc37,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1790
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1827
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1858
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1891
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1931
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 1968
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2003
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2034
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2067
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2098
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2133
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2161
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2191
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2220
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2251
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2280
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2307
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2339
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2370
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2400
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2433
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2463
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2494
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2520
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2551
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2576
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2606
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2635
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2664
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2691
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2718
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2744
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2779
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2809
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2835
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2867
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2892
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2919
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2945
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 2974
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3001
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3025
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3049
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3077
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3100
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3128
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3151
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3177
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3199
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3226
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3247
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3274
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3295
% 61.20/12.65 === Conflict found: 2529:4:39:[2152.38,104.0,2078.37,2491.1,2006.36,2492.2,1799.35,2493.3,1732.34,2494.4,1666.33,2495.5,1570.32,2496.6,1416.31,2497.7,1180.30,2498.8,1064.29,2499.9,979.28,2500.10,872.27,2501.11,793.26,2502.12,717.25,2503.13,644.24,2504.14,620.23,2505.15,597.22,2506.16,575.21,2507.17,536.20,2508.18,516.19,2509.19,480.18,2510.20,462.17,2511.21,445.16,2512.22,399.15,2513.23,343.14,2514.24,303.13,2515.26,266.12,2516.27,232.11,2517.28,201.10,2518.30,173.9,2519.31,148.8,2520.32,140.7,2521.33,133.6,2522.34,127.5,2523.35,122.4,2524.36,118.3,2525.37,115.2,2526.38,113.1,2527.39,1.0,2528.40]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv2_39r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38),ssPv7_34r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29,x30,x31,x32,x33) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc32, x10 -> skc62, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc46, x25 -> skc62, x26 -> skc62, x27 -> skc62, x28 -> skc62, x29 -> skc62, x30 -> skc62, x31 -> skc62, x32 -> skc62, x33 -> skc62, x34 -> skc62, x35 -> skc62, x36 -> skc62, x37 -> skc62, x38 -> skc62}
% 61.20/12.65 === Backtracking. Learning clause 2863:7:27:[2529.3,2490.1,1900.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv34_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 === Conflict found: 2863:7:27:[2529.3,2490.1,1900.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv34_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv38_3r1r1r1(x0,x1,x2) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc33, x11 -> skc32, x12 -> skc54, x13 -> skc52, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc46, x25 -> skc62, x26 -> skc42}
% 61.20/12.65 === Backtracking. Learning clause 2864:8:53:[2863.4,819.1,1935.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv28_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv16_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv29_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x25,x26,x27,x28,x29) -> ssPv38_3r1r1r1(x0,x1,x2),ssPv6_35r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x25,x26,x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40,x41,x42,x43,x44,x45,x46,x47,x48,x49,x50,x51,x52),ssPv31_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x25,x26,x27)
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3339
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3372
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3406
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3433
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3468
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3493
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3518
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3544
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3575
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3603
% 61.20/12.65 === Clause set with instances from active satisfied. Growing active. New size: 3629
% 61.20/12.65 === Conflict found: 2860:5:27:[2608.3,2648.1,1122.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv14_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv38_3r1r1r1(x0,x1,x2) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc33, x10 -> skc41, x11 -> skc62, x12 -> skc62, x13 -> skc62, x14 -> skc62, x15 -> skc62, x16 -> skc62, x17 -> skc62, x18 -> skc62, x19 -> skc62, x20 -> skc62, x21 -> skc62, x22 -> skc62, x23 -> skc62, x24 -> skc62, x25 -> skc62, x26 -> skc43}
% 61.20/12.65 === Backtracking. Learning clause 2865:4:11:[2860.3,845.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv32_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv40_1r1(x0) -> ssPv30_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv38_3r1r1r1(x0,x1,x2)
% 61.20/12.65 === Conflict found: 2850:4:16:[2490.2,668.1,2451.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv37_4r1r1r1r1(x0,x1,x2,x3) -> ssPv38_3r1r1r1(x0,x1,x2),ssPv25_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) {x0 -> skc62, x1 -> skc62, x2 -> skc62, x3 -> skc62, x4 -> skc62, x5 -> skc62, x6 -> skc62, x7 -> skc62, x8 -> skc62, x9 -> skc62, x10 -> skc62, x11 -> skc62, x12 -> skc54, x13 -> skc52, x14 -> skc62, x15 -> skc49}
% 61.20/12.65
% 61.20/12.65 SZS status Unsatisfiable
% 61.20/12.65
% 61.20/12.65 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.20/12.65
% 61.20/12.65 SPASS-SCL-FOL Statistics:
% 61.20/12.65 Number of learned clauses: 18
% 61.20/12.65 Number of propagations: 11054
% 61.20/12.65 Number of decisions: 5164
% 61.20/12.65 Number of resolutions: 39
% 61.20/12.65 Number of condensations: 1
% 61.20/12.65 Number of sub resolutions: 2735
% 61.20/12.65 Number of input literals (deduplicated): 111
% 61.20/12.65 Number of grows: 101
% 61.20/12.65 Number of considered ground atoms: 3629
% 61.20/12.65
% 61.20/12.65 Needed: 0:0:12.22
% 61.20/12.65
%------------------------------------------------------------------------------