%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN880-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 : n021.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:21 PM UTC 2026
% Result : Unsatisfiable 0.30s 0.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.25 % Problem : SYN880-1 : TPTP v9.2.1. Released v2.5.0.
% 0.11/0.26 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.48 % Computer : n021.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8042.1875MB
% 0.18/0.48 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Thu May 7 13:50:43 EDT 2026
% 0.18/0.48 % CPUTime :
% 0.18/0.48 SPASS-SCL-FOL version:
% 0.26/0.57 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.30/0.79 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.79 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.79 Execution resolution_3 ended with status: unsatisfiable
% 0.30/0.79 Used heuristic: resolution_3
% 0.30/0.79
% 0.30/0.79 Input Clauses:
% 0.30/0.79
% 0.30/0.79 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv24_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv23_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv22_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv21_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv27_2r1r1 ssPv18_11r1r1r1r1r1r1r1r1r1r1r1 ssPv28_1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv20_9r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv26_3r1r1r1 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_10r1r1r1r1r1r1r1r1r1r1 ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv25_4r1r1r1r1 ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 0.30/0.79 Fol Constants: skc46 skc47 skc44 skc45 skc42 skc43 skc40 skc41 skc38 skc39 skc36 skc37 skc34 skc35 skc32 skc33 skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25
% 0.30/0.79 Fol Functions:
% 0.30/0.79 Problem Properties:
% 0.30/0.79 This is a Bernays Schoenfinkel problem.
% 0.30/0.79
% 0.30/0.79 After reduction: Problem Properties:
% 0.30/0.79 This is a Bernays Schoenfinkel problem.
% 0.30/0.79
% 0.30/0.79
% 0.30/0.79 Reduced Input Clauses:
% 0.30/0.79 93:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 0.30/0.79 95:1:2:[93.1,3.0,1.0,94.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 0.30/0.79 98:1:3:[95.2,4.0,93.1,96.1,1.0,97.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 0.30/0.79 102:1:4:[98.3,5.0,95.2,99.1,93.1,100.2,1.0,101.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 106:1:4:[98.3,6.0,95.2,103.1,93.1,104.2,1.0,105.3]:TopTopTopTop: -> ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc46)
% 0.30/0.79 110:1:4:[98.3,7.1,95.2,107.2,93.1,108.3,1.0,109.4]:TopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc47) ->
% 0.30/0.79 115:1:5:[102.4,8.0,98.3,111.1,95.2,112.2,93.1,113.3,1.0,114.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.30/0.79 120:1:5:[102.4,9.0,98.3,116.1,95.2,117.2,93.1,118.3,1.0,119.4]:TopTopTopTopTop: -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc44)
% 0.30/0.79 125:1:5:[102.4,10.1,98.3,121.2,95.2,122.3,93.1,123.4,1.0,124.5]:TopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc45) ->
% 0.30/0.79 131:1:6:[115.5,11.0,102.4,126.1,98.3,127.2,95.2,128.3,93.1,129.4,1.0,130.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 137:1:6:[115.5,12.0,102.4,132.1,98.3,133.2,95.2,134.3,93.1,135.4,1.0,136.5]:TopTopTopTopTopTop: -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc42)
% 0.30/0.79 143:1:6:[115.5,13.1,102.4,138.2,98.3,139.3,95.2,140.4,93.1,141.5,1.0,142.6]:TopTopTopTopTopTop: ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc43) ->
% 0.30/0.79 150:1:7:[131.6,14.0,115.5,144.1,102.4,145.2,98.3,146.3,95.2,147.4,93.1,148.5,1.0,149.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.30/0.79 157:1:7:[131.6,15.0,115.5,151.1,102.4,152.2,98.3,153.3,95.2,154.4,93.1,155.5,1.0,156.6]:TopTopTopTopTopTopTop: -> ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc40)
% 0.30/0.79 164:1:7:[131.6,16.1,115.5,158.2,102.4,159.3,98.3,160.4,95.2,161.5,93.1,162.6,1.0,163.7]:TopTopTopTopTopTopTop: ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc41) ->
% 0.30/0.79 172:1:8:[150.7,17.0,131.6,165.1,115.5,166.2,102.4,167.3,98.3,168.4,95.2,169.5,93.1,170.6,1.0,171.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.30/0.79 181:1:9:[172.8,18.0,150.7,173.1,131.6,174.2,115.5,175.3,102.4,176.4,98.3,177.5,95.2,178.6,93.1,179.7,1.0,180.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.30/0.79 191:1:10:[181.9,19.0,172.8,182.1,150.7,183.2,131.6,184.3,115.5,185.4,102.4,186.5,98.3,187.6,95.2,188.7,93.1,189.8,1.0,190.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.30/0.79 202:1:11:[191.10,20.0,181.9,192.1,172.8,193.2,150.7,194.3,131.6,195.4,115.5,196.5,102.4,197.6,98.3,198.7,95.2,199.8,93.1,200.9,1.0,201.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.30/0.79 214:1:12:[202.11,21.0,191.10,203.1,181.9,204.2,172.8,205.3,150.7,206.4,131.6,207.5,115.5,208.6,102.4,209.7,98.3,210.8,95.2,211.9,93.1,212.10,1.0,213.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.30/0.79 226:1:12:[202.11,22.0,191.10,215.1,181.9,216.2,172.8,217.3,150.7,218.4,131.6,219.5,115.5,220.6,102.4,221.7,98.3,222.8,95.2,223.9,93.1,224.10,1.0,225.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc38)
% 0.30/0.79 238:1:12:[202.11,23.1,191.10,227.2,181.9,228.3,172.8,229.4,150.7,230.5,131.6,231.6,115.5,232.7,102.4,233.8,98.3,234.9,95.2,235.10,93.1,236.11,1.0,237.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc39) ->
% 0.30/0.79 251:1:13:[214.12,24.0,202.11,239.1,191.10,240.2,181.9,241.3,172.8,242.4,150.7,243.5,131.6,244.6,115.5,245.7,102.4,246.8,98.3,247.9,95.2,248.10,93.1,249.11,1.0,250.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.30/0.79 264:1:13:[214.12,25.0,202.11,252.1,191.10,253.2,181.9,254.3,172.8,255.4,150.7,256.5,131.6,257.6,115.5,258.7,102.4,259.8,98.3,260.9,95.2,261.10,93.1,262.11,1.0,263.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc36)
% 0.30/0.79 277:1:13:[214.12,26.1,202.11,265.2,191.10,266.3,181.9,267.4,172.8,268.5,150.7,269.6,131.6,270.7,115.5,271.8,102.4,272.9,98.3,273.10,95.2,274.11,93.1,275.12,1.0,276.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc37) ->
% 0.30/0.79 291:1:14:[251.13,27.0,214.12,278.1,202.11,279.2,191.10,280.3,181.9,281.4,172.8,282.5,150.7,283.6,131.6,284.7,115.5,285.8,102.4,286.9,98.3,287.10,95.2,288.11,93.1,289.12,1.0,290.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.30/0.79 305:1:14:[251.13,28.0,214.12,292.1,202.11,293.2,191.10,294.3,181.9,295.4,172.8,296.5,150.7,297.6,131.6,298.7,115.5,299.8,102.4,300.9,98.3,301.10,95.2,302.11,93.1,303.12,1.0,304.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc34)
% 0.30/0.79 319:1:14:[251.13,29.1,214.12,306.2,202.11,307.3,191.10,308.4,181.9,309.5,172.8,310.6,150.7,311.7,131.6,312.8,115.5,313.9,102.4,314.10,98.3,315.11,95.2,316.12,93.1,317.13,1.0,318.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc35) ->
% 0.30/0.79 332:4:13:[214.12,30.0,202.11,320.1,191.10,321.2,181.9,322.3,172.8,323.4,150.7,324.5,131.6,325.6,115.5,326.7,102.4,327.8,98.3,328.9,95.2,329.11,93.1,330.12,1.0,331.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.30/0.79 346:4:14:[251.13,31.0,214.12,333.2,202.11,334.3,191.10,335.4,181.9,336.5,172.8,337.6,150.7,338.7,131.6,339.8,115.5,340.10,102.4,341.11,98.3,342.12,95.2,343.13,93.1,344.15,1.0,345.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv28_1r1(x0) -> ssPv27_2r1r1(x0,x1)
% 0.30/0.79 361:1:15:[291.14,32.0,251.13,347.1,214.12,348.2,202.11,349.3,191.10,350.4,181.9,351.5,172.8,352.6,150.7,353.7,131.6,354.8,115.5,355.9,102.4,356.10,98.3,357.11,95.2,358.12,93.1,359.13,1.0,360.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.30/0.79 376:1:15:[291.14,33.0,251.13,362.1,214.12,363.2,202.11,364.3,191.10,365.4,181.9,366.5,172.8,367.6,150.7,368.7,131.6,369.8,115.5,370.9,102.4,371.10,98.3,372.11,95.2,373.12,93.1,374.13,1.0,375.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc32)
% 0.30/0.79 391:1:15:[291.14,34.1,251.13,377.2,214.12,378.3,202.11,379.4,191.10,380.5,181.9,381.6,172.8,382.7,150.7,383.8,131.6,384.9,115.5,385.10,102.4,386.11,98.3,387.12,95.2,388.13,93.1,389.14,1.0,390.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc33) ->
% 0.30/0.79 407:1:16:[361.15,35.0,291.14,392.1,251.13,393.2,214.12,394.3,202.11,395.4,191.10,396.5,181.9,397.6,172.8,398.7,150.7,399.8,131.6,400.9,115.5,401.10,102.4,402.11,98.3,403.12,95.2,404.13,93.1,405.14,1.0,406.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.30/0.79 424:1:17:[407.16,36.0,361.15,408.1,291.14,409.2,251.13,410.3,214.12,411.4,202.11,412.5,191.10,413.6,181.9,414.7,172.8,415.8,150.7,416.9,131.6,417.10,115.5,418.11,102.4,419.12,98.3,420.13,95.2,421.14,93.1,422.15,1.0,423.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.30/0.79 440:4:16:[361.15,37.0,291.14,425.2,251.13,426.3,214.12,427.4,202.11,428.6,191.10,429.7,181.9,430.8,172.8,431.9,150.7,432.10,131.6,433.11,115.5,434.12,102.4,435.13,98.3,436.14,95.2,437.15,93.1,438.16,1.0,439.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv28_1r1(x0)
% 0.30/0.79 456:4:16:[361.15,38.0,291.14,441.2,251.13,442.4,214.12,443.5,202.11,444.6,191.10,445.7,181.9,446.8,172.8,447.9,150.7,448.10,131.6,449.11,115.5,450.12,102.4,451.13,98.3,452.14,95.2,453.15,93.1,454.17,1.0,455.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv28_1r1(x0) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.30/0.79 474:1:18:[424.17,39.0,407.16,457.1,361.15,458.2,291.14,459.3,251.13,460.4,214.12,461.5,202.11,462.6,191.10,463.7,181.9,464.8,172.8,465.9,150.7,466.10,131.6,467.11,115.5,468.12,102.4,469.13,98.3,470.14,95.2,471.15,93.1,472.16,1.0,473.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.30/0.79 491:4:17:[407.16,40.0,361.15,475.1,291.14,476.2,251.13,477.3,214.12,478.4,202.11,479.5,191.10,480.6,181.9,481.7,172.8,482.8,150.7,483.10,131.6,484.11,115.5,485.12,102.4,486.13,98.3,487.14,95.2,488.15,93.1,489.16,1.0,490.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.30/0.79 510:1:19:[474.18,41.0,424.17,492.1,407.16,493.2,361.15,494.3,291.14,495.4,251.13,496.5,214.12,497.6,202.11,498.7,191.10,499.8,181.9,500.9,172.8,501.10,150.7,502.11,131.6,503.12,115.5,504.13,102.4,505.14,98.3,506.15,95.2,507.16,93.1,508.17,1.0,509.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.30/0.79 528:4:18:[424.17,42.0,407.16,511.1,361.15,512.3,291.14,513.4,251.13,514.5,214.12,515.6,202.11,516.7,191.10,517.8,181.9,518.9,172.8,519.11,150.7,520.12,131.6,521.13,115.5,522.14,102.4,523.15,98.3,524.17,95.2,525.18,93.1,526.19,1.0,527.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.30/0.79 548:1:20:[510.19,43.0,474.18,529.1,424.17,530.2,407.16,531.3,361.15,532.4,291.14,533.5,251.13,534.6,214.12,535.7,202.11,536.8,191.10,537.9,181.9,538.10,172.8,539.11,150.7,540.12,131.6,541.13,115.5,542.14,102.4,543.15,98.3,544.16,95.2,545.17,93.1,546.18,1.0,547.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.30/0.79 568:1:20:[510.19,44.0,474.18,549.1,424.17,550.2,407.16,551.3,361.15,552.4,291.14,553.5,251.13,554.6,214.12,555.7,202.11,556.8,191.10,557.9,181.9,558.10,172.8,559.11,150.7,560.12,131.6,561.13,115.5,562.14,102.4,563.15,98.3,564.16,95.2,565.17,93.1,566.18,1.0,567.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,skc30)
% 0.30/0.79 588:1:20:[510.19,45.1,474.18,569.2,424.17,570.3,407.16,571.4,361.15,572.5,291.14,573.6,251.13,574.7,214.12,575.8,202.11,576.9,191.10,577.10,181.9,578.11,172.8,579.12,150.7,580.13,131.6,581.14,115.5,582.15,102.4,583.16,98.3,584.17,95.2,585.18,93.1,586.19,1.0,587.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,skc31) ->
% 0.30/0.79 609:1:21:[548.20,46.0,510.19,589.1,474.18,590.2,424.17,591.3,407.16,592.4,361.15,593.5,291.14,594.6,251.13,595.7,214.12,596.8,202.11,597.9,191.10,598.10,181.9,599.11,172.8,600.12,150.7,601.13,131.6,602.14,115.5,603.15,102.4,604.16,98.3,605.17,95.2,606.18,93.1,607.19,1.0,608.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)
% 0.30/0.79 630:1:21:[548.20,47.0,510.19,610.1,474.18,611.2,424.17,612.3,407.16,613.4,361.15,614.5,291.14,615.6,251.13,616.7,214.12,617.8,202.11,618.9,191.10,619.10,181.9,620.11,172.8,621.12,150.7,622.13,131.6,623.14,115.5,624.15,102.4,625.16,98.3,626.17,95.2,627.18,93.1,628.19,1.0,629.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc28)
% 0.30/0.79 651:1:21:[548.20,48.1,510.19,631.2,474.18,632.3,424.17,633.4,407.16,634.5,361.15,635.6,291.14,636.7,251.13,637.8,214.12,638.9,202.11,639.10,191.10,640.11,181.9,641.12,172.8,642.13,150.7,643.14,131.6,644.15,115.5,645.16,102.4,646.17,98.3,647.18,95.2,648.19,93.1,649.20,1.0,650.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc29) ->
% 0.30/0.79 671:4:20:[510.19,49.0,474.18,652.2,424.17,653.3,407.16,654.4,361.15,655.5,291.14,656.6,251.13,657.7,214.12,658.8,202.11,659.9,191.10,660.10,181.9,661.11,172.8,662.12,150.7,663.13,131.6,664.14,115.5,665.15,102.4,666.16,98.3,667.17,95.2,668.19,93.1,669.20,1.0,670.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv27_2r1r1(x0,x1) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 691:4:20:[510.19,50.0,474.18,672.1,424.17,673.2,407.16,674.3,361.15,675.4,291.14,676.5,251.13,677.6,214.12,678.7,202.11,679.8,191.10,680.9,181.9,681.10,172.8,682.11,150.7,683.12,131.6,684.13,115.5,685.14,102.4,686.15,98.3,687.16,95.2,688.17,93.1,689.18,1.0,690.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv28_1r1(x0)
% 0.30/0.79 711:4:20:[510.19,51.0,474.18,692.1,424.17,693.2,407.16,694.3,361.15,695.5,291.14,696.6,251.13,697.7,214.12,698.9,202.11,699.10,191.10,700.11,181.9,701.12,172.8,702.13,150.7,703.14,131.6,704.15,115.5,705.17,102.4,706.18,98.3,707.19,95.2,708.20,93.1,709.21,1.0,710.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.30/0.79 731:4:20:[510.19,52.0,474.18,712.1,424.17,713.2,407.16,714.3,361.15,715.4,291.14,716.6,251.13,717.7,214.12,718.8,202.11,719.9,191.10,720.11,181.9,721.12,172.8,722.13,150.7,723.14,131.6,724.15,115.5,725.16,102.4,726.17,98.3,727.18,95.2,728.19,93.1,729.20,1.0,730.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.30/0.79 751:4:20:[510.19,53.0,474.18,732.1,424.17,733.2,407.16,734.4,361.15,735.6,291.14,736.7,251.13,737.8,214.12,738.9,202.11,739.10,191.10,740.11,181.9,741.13,172.8,742.14,150.7,743.15,131.6,744.16,115.5,745.17,102.4,746.18,98.3,747.19,95.2,748.20,93.1,749.21,1.0,750.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.30/0.79 773:1:22:[609.21,54.0,548.20,752.1,510.19,753.2,474.18,754.3,424.17,755.4,407.16,756.5,361.15,757.6,291.14,758.7,251.13,759.8,214.12,760.9,202.11,761.10,191.10,762.11,181.9,763.12,172.8,764.13,150.7,765.14,131.6,766.15,115.5,767.16,102.4,768.17,98.3,769.18,95.2,770.19,93.1,771.20,1.0,772.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)
% 0.30/0.79 795:1:22:[609.21,55.0,548.20,774.1,510.19,775.2,474.18,776.3,424.17,777.4,407.16,778.5,361.15,779.6,291.14,780.7,251.13,781.8,214.12,782.9,202.11,783.10,191.10,784.11,181.9,785.12,172.8,786.13,150.7,787.14,131.6,788.15,115.5,789.16,102.4,790.17,98.3,791.18,95.2,792.19,93.1,793.20,1.0,794.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc26)
% 0.30/0.79 817:1:22:[609.21,56.1,548.20,796.2,510.19,797.3,474.18,798.4,424.17,799.5,407.16,800.6,361.15,801.7,291.14,802.8,251.13,803.9,214.12,804.10,202.11,805.11,191.10,806.12,181.9,807.13,172.8,808.14,150.7,809.15,131.6,810.16,115.5,811.17,102.4,812.18,98.3,813.19,95.2,814.20,93.1,815.21,1.0,816.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc27) ->
% 0.30/0.79 840:1:23:[773.22,57.0,609.21,818.1,548.20,819.2,510.19,820.3,474.18,821.4,424.17,822.5,407.16,823.6,361.15,824.7,291.14,825.8,251.13,826.9,214.12,827.10,202.11,828.11,191.10,829.12,181.9,830.13,172.8,831.14,150.7,832.15,131.6,833.16,115.5,834.17,102.4,835.18,98.3,836.19,95.2,837.20,93.1,838.21,1.0,839.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)
% 0.30/0.79 863:1:23:[773.22,58.0,609.21,841.1,548.20,842.2,510.19,843.3,474.18,844.4,424.17,845.5,407.16,846.6,361.15,847.7,291.14,848.8,251.13,849.9,214.12,850.10,202.11,851.11,191.10,852.12,181.9,853.13,172.8,854.14,150.7,855.15,131.6,856.16,115.5,857.17,102.4,858.18,98.3,859.19,95.2,860.20,93.1,861.21,1.0,862.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc24)
% 0.30/0.79 886:1:23:[773.22,59.1,609.21,864.2,548.20,865.3,510.19,866.4,474.18,867.5,424.17,868.6,407.16,869.7,361.15,870.8,291.14,871.9,251.13,872.10,214.12,873.11,202.11,874.12,191.10,875.13,181.9,876.14,172.8,877.15,150.7,878.16,131.6,879.17,115.5,880.18,102.4,881.19,98.3,882.20,95.2,883.21,93.1,884.22,1.0,885.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc25) ->
% 0.30/0.79 908:4:22:[609.21,60.0,548.20,887.2,510.19,888.3,474.18,889.4,424.17,890.5,407.16,891.6,361.15,892.7,291.14,893.8,251.13,894.9,214.12,895.10,202.11,896.11,191.10,897.12,181.9,898.13,172.8,899.14,150.7,900.15,131.6,901.16,115.5,902.17,102.4,903.18,98.3,904.19,95.2,905.20,93.1,906.21,1.0,907.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv28_1r1(x0)
% 0.30/0.79 930:4:22:[609.21,61.0,548.20,909.1,510.19,910.2,474.18,911.3,424.17,912.4,407.16,913.5,361.15,914.6,291.14,915.7,251.13,916.8,214.12,917.10,202.11,918.11,191.10,919.12,181.9,920.13,172.8,921.14,150.7,922.15,131.6,923.16,115.5,924.17,102.4,925.18,98.3,926.19,95.2,927.20,93.1,928.21,1.0,929.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv26_3r1r1r1(x0,x1,x2)
% 0.30/0.79 952:4:22:[609.21,62.0,548.20,931.2,510.19,932.3,474.18,933.4,424.17,934.5,407.16,935.6,361.15,936.7,291.14,937.9,251.13,938.10,214.12,939.11,202.11,940.13,191.10,941.14,181.9,942.15,172.8,943.16,150.7,944.17,131.6,945.18,115.5,946.19,102.4,947.20,98.3,948.21,95.2,949.22,93.1,950.23,1.0,951.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 974:4:22:[609.21,63.0,548.20,953.1,510.19,954.3,474.18,955.4,424.17,956.5,407.16,957.6,361.15,958.7,291.14,959.8,251.13,960.9,214.12,961.10,202.11,962.11,191.10,963.12,181.9,964.13,172.8,965.14,150.7,966.15,131.6,967.16,115.5,968.18,102.4,969.19,98.3,970.20,95.2,971.21,93.1,972.22,1.0,973.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.30/0.79 997:4:23:[773.22,64.0,609.21,975.1,548.20,976.2,510.19,977.3,474.18,978.4,424.17,979.5,407.16,980.6,361.15,981.7,291.14,982.8,251.13,983.9,214.12,984.10,202.11,985.11,191.10,986.12,181.9,987.13,172.8,988.14,150.7,989.15,131.6,990.16,115.5,991.17,102.4,992.18,98.3,993.19,95.2,994.21,93.1,995.22,1.0,996.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.30/0.79 1021:1:24:[840.23,65.0,773.22,998.1,609.21,999.2,548.20,1000.3,510.19,1001.4,474.18,1002.5,424.17,1003.6,407.16,1004.7,361.15,1005.8,291.14,1006.9,251.13,1007.10,214.12,1008.11,202.11,1009.12,191.10,1010.13,181.9,1011.14,172.8,1012.15,150.7,1013.16,131.6,1014.17,115.5,1015.18,102.4,1016.19,98.3,1017.20,95.2,1018.21,93.1,1019.22,1.0,1020.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)
% 0.30/0.79 1044:4:23:[773.22,66.0,609.21,1022.2,548.20,1023.3,510.19,1024.4,474.18,1025.5,424.17,1026.6,407.16,1027.7,361.15,1028.9,291.14,1029.10,251.13,1030.11,214.12,1031.12,202.11,1032.13,191.10,1033.14,181.9,1034.15,172.8,1035.16,150.7,1036.17,131.6,1037.18,115.5,1038.19,102.4,1039.20,98.3,1040.21,95.2,1041.22,93.1,1042.24,1.0,1043.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv28_1r1(x0) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.30/0.79 1067:4:23:[773.22,67.0,609.21,1045.1,548.20,1046.2,510.19,1047.3,474.18,1048.4,424.17,1049.5,407.16,1050.6,361.15,1051.7,291.14,1052.9,251.13,1053.10,214.12,1054.11,202.11,1055.12,191.10,1056.13,181.9,1057.14,172.8,1058.15,150.7,1059.16,131.6,1060.17,115.5,1061.18,102.4,1062.19,98.3,1063.20,95.2,1064.21,93.1,1065.22,1.0,1066.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 1090:4:23:[773.22,68.0,609.21,1068.2,548.20,1069.3,510.19,1070.4,474.18,1071.6,424.17,1072.7,407.16,1073.8,361.15,1074.9,291.14,1075.10,251.13,1076.11,214.12,1077.12,202.11,1078.13,191.10,1079.14,181.9,1080.16,172.8,1081.17,150.7,1082.19,131.6,1083.20,115.5,1084.21,102.4,1085.22,98.3,1086.23,95.2,1087.24,93.1,1088.25,1.0,1089.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ->
% 0.30/0.79 1113:4:23:[773.22,69.0,609.21,1091.2,548.20,1092.3,510.19,1093.4,474.18,1094.6,424.17,1095.7,407.16,1096.8,361.15,1097.9,291.14,1098.10,251.13,1099.12,214.12,1100.13,202.11,1101.14,191.10,1102.15,181.9,1103.16,172.8,1104.17,150.7,1105.18,131.6,1106.19,115.5,1107.20,102.4,1108.22,98.3,1109.23,95.2,1110.24,93.1,1111.25,1.0,1112.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3) ->
% 0.30/0.79 1136:4:23:[773.22,70.0,609.21,1114.2,548.20,1115.4,510.19,1116.5,474.18,1117.6,424.17,1118.7,407.16,1119.8,361.15,1120.9,291.14,1121.10,251.13,1122.11,214.12,1123.13,202.11,1124.14,191.10,1125.15,181.9,1126.16,172.8,1127.18,150.7,1128.19,131.6,1129.20,115.5,1130.21,102.4,1131.22,98.3,1132.23,95.2,1133.24,93.1,1134.25,1.0,1135.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ->
% 0.30/0.79 1159:4:23:[773.22,71.0,609.21,1137.1,548.20,1138.2,510.19,1139.4,474.18,1140.5,424.17,1141.6,407.16,1142.7,361.15,1143.8,291.14,1144.9,251.13,1145.10,214.12,1146.11,202.11,1147.12,191.10,1148.13,181.9,1149.14,172.8,1150.15,150.7,1151.16,131.6,1152.17,115.5,1153.18,102.4,1154.20,98.3,1155.21,95.2,1156.22,93.1,1157.23,1.0,1158.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 0.30/0.79 1184:1:25:[1021.24,72.0,840.23,1160.1,773.22,1161.2,609.21,1162.3,548.20,1163.4,510.19,1164.5,474.18,1165.6,424.17,1166.7,407.16,1167.8,361.15,1168.9,291.14,1169.10,251.13,1170.11,214.12,1171.12,202.11,1172.13,191.10,1173.14,181.9,1174.15,172.8,1175.16,150.7,1176.17,131.6,1177.18,115.5,1178.19,102.4,1179.20,98.3,1180.21,95.2,1181.22,93.1,1182.23,1.0,1183.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)
% 0.30/0.79 1208:4:24:[840.23,73.0,773.22,1185.1,609.21,1186.2,548.20,1187.3,510.19,1188.4,474.18,1189.5,424.17,1190.6,407.16,1191.7,361.15,1192.8,291.14,1193.9,251.13,1194.10,214.12,1195.11,202.11,1196.13,191.10,1197.14,181.9,1198.15,172.8,1199.16,150.7,1200.17,131.6,1201.18,115.5,1202.20,102.4,1203.21,98.3,1204.22,95.2,1205.23,93.1,1206.24,1.0,1207.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv5_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_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.30/0.79 1232:4:24:[840.23,74.1,773.22,1209.2,609.21,1210.3,548.20,1211.4,510.19,1212.5,474.18,1213.6,424.17,1214.7,407.16,1215.8,361.15,1216.9,291.14,1217.10,251.13,1218.11,214.12,1219.12,202.11,1220.13,191.10,1221.14,181.9,1222.15,172.8,1223.16,150.7,1224.17,131.6,1225.18,115.5,1226.19,102.4,1227.20,98.3,1228.21,95.2,1229.22,93.1,1230.23,1.0,1231.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) -> ssPv5_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),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.30/0.79 1258:1:26:[1184.25,75.0,1021.24,1233.1,840.23,1234.2,773.22,1235.3,609.21,1236.4,548.20,1237.5,510.19,1238.6,474.18,1239.7,424.17,1240.8,407.16,1241.9,361.15,1242.10,291.14,1243.11,251.13,1244.12,214.12,1245.13,202.11,1246.14,191.10,1247.15,181.9,1248.16,172.8,1249.17,150.7,1250.18,131.6,1251.19,115.5,1252.20,102.4,1253.21,98.3,1254.22,95.2,1255.23,93.1,1256.24,1.0,1257.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)
% 0.30/0.79 1283:4:25:[1021.24,76.0,840.23,1259.2,773.22,1260.3,609.21,1261.4,548.20,1262.5,510.19,1263.7,474.18,1264.8,424.17,1265.9,407.16,1266.10,361.15,1267.12,291.14,1268.13,251.13,1269.14,214.12,1270.15,202.11,1271.16,191.10,1272.17,181.9,1273.18,172.8,1274.19,150.7,1275.20,131.6,1276.21,115.5,1277.22,102.4,1278.23,98.3,1279.24,95.2,1280.25,93.1,1281.26,1.0,1282.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_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_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 1308:4:25:[1021.24,77.0,840.23,1284.3,773.22,1285.4,609.21,1286.5,548.20,1287.6,510.19,1288.7,474.18,1289.8,424.17,1290.9,407.16,1291.10,361.15,1292.11,291.14,1293.12,251.13,1294.13,214.12,1295.14,202.11,1296.15,191.10,1297.16,181.9,1298.17,172.8,1299.18,150.7,1300.19,131.6,1301.20,115.5,1302.21,102.4,1303.22,98.3,1304.23,95.2,1305.24,93.1,1306.25,1.0,1307.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_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),ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 1335:1:27:[1258.26,78.0,1184.25,1309.1,1021.24,1310.2,840.23,1311.3,773.22,1312.4,609.21,1313.5,548.20,1314.6,510.19,1315.7,474.18,1316.8,424.17,1317.9,407.16,1318.10,361.15,1319.11,291.14,1320.12,251.13,1321.13,214.12,1322.14,202.11,1323.15,191.10,1324.16,181.9,1325.17,172.8,1326.18,150.7,1327.19,131.6,1328.20,115.5,1329.21,102.4,1330.22,98.3,1331.23,95.2,1332.24,93.1,1333.25,1.0,1334.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)
% 0.30/0.79 1361:4:26:[1184.25,79.0,1021.24,1336.1,840.23,1337.2,773.22,1338.3,609.21,1339.4,548.20,1340.5,510.19,1341.6,474.18,1342.7,424.17,1343.8,407.16,1344.9,361.15,1345.10,291.14,1346.12,251.13,1347.13,214.12,1348.14,202.11,1349.15,191.10,1350.16,181.9,1351.17,172.8,1352.18,150.7,1353.20,131.6,1354.21,115.5,1355.22,102.4,1356.23,98.3,1357.25,95.2,1358.26,93.1,1359.27,1.0,1360.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv3_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)
% 0.30/0.79 1387:4:26:[1184.25,80.0,1021.24,1362.3,840.23,1363.4,773.22,1364.5,609.21,1365.6,548.20,1366.7,510.19,1367.8,474.18,1368.9,424.17,1369.10,407.16,1370.11,361.15,1371.12,291.14,1372.13,251.13,1373.14,214.12,1374.15,202.11,1375.16,191.10,1376.17,181.9,1377.18,172.8,1378.19,150.7,1379.20,131.6,1380.21,115.5,1381.22,102.4,1382.23,98.3,1383.24,95.2,1384.25,93.1,1385.27,1.0,1386.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_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),ssPv5_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),ssPv28_1r1(x0) -> ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.30/0.79 1413:4:26:[1184.25,81.0,1021.24,1388.1,840.23,1389.2,773.22,1390.4,609.21,1391.5,548.20,1392.6,510.19,1393.7,474.18,1394.8,424.17,1395.9,407.16,1396.10,361.15,1397.11,291.14,1398.12,251.13,1399.13,214.12,1400.14,202.11,1401.15,191.10,1402.16,181.9,1403.17,172.8,1404.18,150.7,1405.20,131.6,1406.21,115.5,1407.22,102.4,1408.23,98.3,1409.24,95.2,1410.26,93.1,1411.27,1.0,1412.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv27_2r1r1(x0,x1) -> ssPv3_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)
% 0.30/0.79 1439:4:26:[1184.25,82.0,1021.24,1414.1,840.23,1415.2,773.22,1416.3,609.21,1417.4,548.20,1418.5,510.19,1419.6,474.18,1420.7,424.17,1421.8,407.16,1422.9,361.15,1423.10,291.14,1424.11,251.13,1425.12,214.12,1426.13,202.11,1427.14,191.10,1428.15,181.9,1429.16,172.8,1430.17,150.7,1431.18,131.6,1432.19,115.5,1433.21,102.4,1434.22,98.3,1435.23,95.2,1436.24,93.1,1437.25,1.0,1438.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_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),ssPv5_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),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.30/0.79 1465:4:26:[1184.25,83.0,1021.24,1440.2,840.23,1441.3,773.22,1442.4,609.21,1443.5,548.20,1444.7,510.19,1445.8,474.18,1446.9,424.17,1447.10,407.16,1448.11,361.15,1449.12,291.14,1450.13,251.13,1451.14,214.12,1452.15,202.11,1453.16,191.10,1454.17,181.9,1455.18,172.8,1456.19,150.7,1457.20,131.6,1458.21,115.5,1459.22,102.4,1460.23,98.3,1461.24,95.2,1462.25,93.1,1463.26,1.0,1464.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_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),ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 1491:4:26:[1184.25,84.0,1021.24,1466.2,840.23,1467.3,773.22,1468.4,609.21,1469.6,548.20,1470.7,510.19,1471.8,474.18,1472.9,424.17,1473.10,407.16,1474.11,361.15,1475.12,291.14,1476.13,251.13,1477.15,214.12,1478.16,202.11,1479.17,191.10,1480.18,181.9,1481.19,172.8,1482.20,150.7,1483.21,131.6,1484.22,115.5,1485.23,102.4,1486.24,98.3,1487.25,95.2,1488.26,93.1,1489.27,1.0,1490.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_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),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.30/0.79 1518:4:27:[1258.26,85.0,1184.25,1492.2,1021.24,1493.3,840.23,1494.4,773.22,1495.5,609.21,1496.6,548.20,1497.7,510.19,1498.8,474.18,1499.9,424.17,1500.10,407.16,1501.11,361.15,1502.12,291.14,1503.13,251.13,1504.14,214.12,1505.15,202.11,1506.16,191.10,1507.17,181.9,1508.18,172.8,1509.19,150.7,1510.21,131.6,1511.22,115.5,1512.23,102.4,1513.25,98.3,1514.26,95.2,1515.27,93.1,1516.28,1.0,1517.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_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),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.30/0.79 1545:4:27:[1258.26,86.0,1184.25,1519.1,1021.24,1520.2,840.23,1521.3,773.22,1522.4,609.21,1523.5,548.20,1524.6,510.19,1525.7,474.18,1526.8,424.17,1527.9,407.16,1528.10,361.15,1529.11,291.14,1530.12,251.13,1531.13,214.12,1532.14,202.11,1533.15,191.10,1534.16,181.9,1535.17,172.8,1536.19,150.7,1537.20,131.6,1538.21,115.5,1539.22,102.4,1540.23,98.3,1541.24,95.2,1542.25,93.1,1543.26,1.0,1544.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv2_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_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.30/0.79 1572:4:27:[1258.26,87.0,1184.25,1546.2,1021.24,1547.3,840.23,1548.4,773.22,1549.5,609.21,1550.6,548.20,1551.7,510.19,1552.8,474.18,1553.9,424.17,1554.10,407.16,1555.11,361.15,1556.12,291.14,1557.13,251.13,1558.14,214.12,1559.15,202.11,1560.16,191.10,1561.17,181.9,1562.18,172.8,1563.19,150.7,1564.20,131.6,1565.21,115.5,1566.22,102.4,1567.23,98.3,1568.24,95.2,1569.25,93.1,1570.26,1.0,1571.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_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) -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.30/0.79 1600:4:28:[1335.27,88.0,1258.26,1573.2,1184.25,1574.3,1021.24,1575.4,840.23,1576.5,773.22,1577.6,609.21,1578.7,548.20,1579.8,510.19,1580.9,474.18,1581.10,424.17,1582.11,407.16,1583.12,361.15,1584.14,291.14,1585.15,251.13,1586.16,214.12,1587.17,202.11,1588.18,191.10,1589.19,181.9,1590.20,172.8,1591.21,150.7,1592.22,131.6,1593.24,115.5,1594.25,102.4,1595.26,98.3,1596.27,95.2,1597.28,93.1,1598.29,1.0,1599.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_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),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.30/0.79 1628:4:28:[1335.27,89.0,1258.26,1601.2,1184.25,1602.3,1021.24,1603.4,840.23,1604.5,773.22,1605.6,609.21,1606.7,548.20,1607.8,510.19,1608.9,474.18,1609.10,424.17,1610.11,407.16,1611.12,361.15,1612.13,291.14,1613.14,251.13,1614.15,214.12,1615.16,202.11,1616.17,191.10,1617.18,181.9,1618.19,172.8,1619.20,150.7,1620.21,131.6,1621.22,115.5,1622.23,102.4,1623.24,98.3,1624.25,95.2,1625.26,93.1,1626.27,1.0,1627.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_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) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 1656:4:28:[1335.27,90.0,1258.26,1629.1,1184.25,1630.2,1021.24,1631.3,840.23,1632.4,773.22,1633.5,609.21,1634.6,548.20,1635.7,510.19,1636.8,474.18,1637.9,424.17,1638.10,407.16,1639.11,361.15,1640.13,291.14,1641.15,251.13,1642.16,214.12,1643.17,202.11,1644.18,191.10,1645.19,181.9,1646.20,172.8,1647.21,150.7,1648.22,131.6,1649.23,115.5,1650.24,102.4,1651.25,98.3,1652.26,95.2,1653.27,93.1,1654.28,1.0,1655.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv1_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),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.30/0.79 1684:4:28:[1335.27,91.0,1258.26,1657.2,1184.25,1658.3,1021.24,1659.4,840.23,1660.5,773.22,1661.6,609.21,1662.7,548.20,1663.8,510.19,1664.9,474.18,1665.10,424.17,1666.11,407.16,1667.12,361.15,1668.13,291.14,1669.14,251.13,1670.15,214.12,1671.16,202.11,1672.17,191.10,1673.18,181.9,1674.19,172.8,1675.20,150.7,1676.21,131.6,1677.22,115.5,1678.23,102.4,1679.24,98.3,1680.25,95.2,1681.26,93.1,1682.27,1.0,1683.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_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) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.30/0.79 1712:4:28:[1335.27,92.0,1258.26,1685.2,1184.25,1686.3,1021.24,1687.5,840.23,1688.6,773.22,1689.7,609.21,1690.8,548.20,1691.9,510.19,1692.10,474.18,1693.11,424.17,1694.12,407.16,1695.13,361.15,1696.15,291.14,1697.16,251.13,1698.17,214.12,1699.18,202.11,1700.19,191.10,1701.20,181.9,1702.21,172.8,1703.22,150.7,1704.23,131.6,1705.24,115.5,1706.25,102.4,1707.26,98.3,1708.27,95.2,1709.28,93.1,1710.29,1.0,1711.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_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),ssPv5_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),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv3_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)
% 0.30/0.79
% 0.30/0.79 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) ssPv27_2r1r1(x0,x1) ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv28_1r1(x0) 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) ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv26_3r1r1r1(x0,x1,x2) ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) 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) ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssPv25_4r1r1r1r1(x0,x1,x2,x3) ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv6_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) ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) 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) ssPv5_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_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) ssPv4_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_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) ssPv3_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) ssPv2_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) ssPv1_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)
% 0.30/0.79
% 0.30/0.79 === Starting SPASS-SCL-FOL A Little Less Naive, considering 35 atoms initially, heuristics mode: resolution_3 ===
% 0.30/0.79
% 0.30/0.79 === Conflict found: 332:4:13:[214.12,30.0,202.11,320.1,191.10,321.2,181.9,322.3,172.8,323.4,150.7,324.5,131.6,325.6,115.5,326.7,102.4,327.8,98.3,328.9,95.2,329.11,93.1,330.12,1.0,331.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.30/0.79 === Backtracking. Learning clause 1713:3:11:[332.2,238.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.30/0.79 === Conflict found: 731:4:20:[510.19,52.0,474.18,712.1,424.17,713.2,407.16,714.3,361.15,715.4,291.14,716.6,251.13,717.7,214.12,718.8,202.11,719.9,191.10,720.11,181.9,721.12,172.8,722.13,150.7,723.14,131.6,724.15,115.5,725.16,102.4,726.17,98.3,727.18,95.2,728.19,93.1,729.20,1.0,730.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46}
% 0.30/0.79 === Backtracking. Learning clause 1714:5:14:[731.3,671.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_2r1r1(x0,x1) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 === Conflict found: 1714:5:14:[731.3,671.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_2r1r1(x0,x1) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.30/0.79 === Backtracking. Learning clause 1715:4:13:[1714.1,264.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_2r1r1(x0,x1) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 === Conflict found: 1715:4:13:[1714.1,264.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_2r1r1(x0,x1) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.30/0.79 === Backtracking. Learning clause 1716:3:10:[1715.3,238.1]:TopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv27_2r1r1(x0,x1) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.79 === Conflict found: 974:4:22:[609.21,63.0,548.20,953.1,510.19,954.3,474.18,955.4,424.17,956.5,407.16,957.6,361.15,958.7,291.14,959.8,251.13,960.9,214.12,961.10,202.11,962.11,191.10,963.12,181.9,964.13,172.8,965.14,150.7,966.15,131.6,967.16,115.5,968.18,102.4,969.19,98.3,970.20,95.2,971.21,93.1,972.22,1.0,973.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46}
% 0.30/0.79 === Backtracking. Learning clause 1717:6:19:[974.3,952.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 === Conflict found: 952:4:22:[609.21,62.0,548.20,931.2,510.19,932.3,474.18,933.4,424.17,934.5,407.16,935.6,361.15,936.7,291.14,937.9,251.13,938.10,214.12,939.11,202.11,940.13,191.10,941.14,181.9,942.15,172.8,943.16,150.7,944.17,131.6,945.18,115.5,946.19,102.4,947.20,98.3,948.21,95.2,949.22,93.1,950.23,1.0,951.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc28}
% 0.30/0.79 === Backtracking. Learning clause 1718:3:14:[952.1,630.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 === Conflict found: 1718:3:14:[952.1,630.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.30/0.79 === Backtracking. Learning clause 1719:3:7:[1718.1,264.1,1713.2]:TopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.30/0.79 === Conflict found: 974:4:22:[609.21,63.0,548.20,953.1,510.19,954.3,474.18,955.4,424.17,956.5,407.16,957.6,361.15,958.7,291.14,959.8,251.13,960.9,214.12,961.10,202.11,962.11,191.10,963.12,181.9,964.13,172.8,965.14,150.7,966.15,131.6,967.16,115.5,968.18,102.4,969.19,98.3,970.20,95.2,971.21,93.1,972.22,1.0,973.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc29}
% 0.30/0.79 === Backtracking. Learning clause 1720:3:19:[974.3,651.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.30/0.79 === Conflict found: 1067:4:23:[773.22,67.0,609.21,1045.1,548.20,1046.2,510.19,1047.3,474.18,1048.4,424.17,1049.5,407.16,1050.6,361.15,1051.7,291.14,1052.9,251.13,1053.10,214.12,1054.11,202.11,1055.12,191.10,1056.13,181.9,1057.14,172.8,1058.15,150.7,1059.16,131.6,1060.17,115.5,1061.18,102.4,1062.19,98.3,1063.20,95.2,1064.21,93.1,1065.22,1.0,1066.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc27}
% 0.30/0.79 === Backtracking. Learning clause 1721:3:18:[1067.2,817.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 === Conflict found: 1090:4:23:[773.22,68.0,609.21,1068.2,548.20,1069.3,510.19,1070.4,474.18,1071.6,424.17,1072.7,407.16,1073.8,361.15,1074.9,291.14,1075.10,251.13,1076.11,214.12,1077.12,202.11,1078.13,191.10,1079.14,181.9,1080.16,172.8,1081.17,150.7,1082.19,131.6,1083.20,115.5,1084.21,102.4,1085.22,98.3,1086.23,95.2,1087.24,93.1,1088.25,1.0,1089.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc26}
% 0.30/0.79 === Backtracking. Learning clause 1722:4:14:[1090.1,795.1,1721.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 === Conflict found: 1722:4:14:[1090.1,795.1,1721.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.30/0.79 === Backtracking. Learning clause 1723:3:9:[1722.3,264.1]:TopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.79 === Conflict found: 1232:4:24:[840.23,74.1,773.22,1209.2,609.21,1210.3,548.20,1211.4,510.19,1212.5,474.18,1213.6,424.17,1214.7,407.16,1215.8,361.15,1216.9,291.14,1217.10,251.13,1218.11,214.12,1219.12,202.11,1220.13,191.10,1221.14,181.9,1222.15,172.8,1223.16,150.7,1224.17,131.6,1225.18,115.5,1226.19,102.4,1227.20,98.3,1228.21,95.2,1229.22,93.1,1230.23,1.0,1231.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) -> ssPv5_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),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc25}
% 0.30/0.80 === Backtracking. Learning clause 1724:3:23:[1232.2,886.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.30/0.80 === Conflict found: 1724:3:23:[1232.2,886.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc26}
% 0.30/0.80 === Backtracking. Learning clause 1725:2:12:[1724.1,795.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.30/0.80 === Conflict found: 930:4:22:[609.21,61.0,548.20,909.1,510.19,910.2,474.18,911.3,424.17,912.4,407.16,913.5,361.15,914.6,291.14,915.7,251.13,916.8,214.12,917.10,202.11,918.11,191.10,919.12,181.9,920.13,172.8,921.14,150.7,922.15,131.6,923.16,115.5,924.17,102.4,925.18,98.3,926.19,95.2,927.20,93.1,928.21,1.0,929.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc29}
% 0.30/0.80 === Backtracking. Learning clause 1726:3:16:[930.2,651.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv26_3r1r1r1(x0,x1,x2)
% 0.30/0.80 === Clause set with instances from active satisfied. Growing active. New size: 37
% 0.30/0.80 === Restarting.
% 0.30/0.80 === Conflict found: 1719:3:7:[1718.1,264.1,1713.2]:TopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc43}
% 0.30/0.80 === Backtracking. Learning clause 1727:2:4:[1719.3,143.1]:TopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.30/0.80 === Conflict found: 997:4:23:[773.22,64.0,609.21,975.1,548.20,976.2,510.19,977.3,474.18,978.4,424.17,979.5,407.16,980.6,361.15,981.7,291.14,982.8,251.13,983.9,214.12,984.10,202.11,985.11,191.10,986.12,181.9,987.13,172.8,988.14,150.7,989.15,131.6,990.16,115.5,991.17,102.4,992.18,98.3,993.19,95.2,994.21,93.1,995.22,1.0,996.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc27}
% 0.30/0.80 === Backtracking. Learning clause 1728:3:7:[997.2,817.1,1716.1]:TopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.80 === Conflict found: 1728:3:7:[997.2,817.1,1716.1]:TopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc43}
% 0.30/0.80 === Backtracking. Learning clause 1729:2:6:[1728.2,143.1]:TopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.80 === Conflict found: 1208:4:24:[840.23,73.0,773.22,1185.1,609.21,1186.2,548.20,1187.3,510.19,1188.4,474.18,1189.5,424.17,1190.6,407.16,1191.7,361.15,1192.8,291.14,1193.9,251.13,1194.10,214.12,1195.11,202.11,1196.13,191.10,1197.14,181.9,1198.15,172.8,1199.16,150.7,1200.17,131.6,1201.18,115.5,1202.20,102.4,1203.21,98.3,1204.22,95.2,1205.23,93.1,1206.24,1.0,1207.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv5_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_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc25}
% 0.30/0.80 === Backtracking. Learning clause 1730:3:17:[1208.3,886.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.30/0.80 === Clause set with instances from active satisfied. Growing active. New size: 38
% 0.30/0.80 === Restarting.
% 0.30/0.80 === Conflict found: 1729:2:6:[1728.2,143.1]:TopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc45}
% 0.30/0.80 === Backtracking. Learning clause 1731:1:2:[1729.2,125.1]:TopTop: ssPv27_2r1r1(x0,x1) ->
% 0.30/0.80 === Conflict found: 346:4:14:[251.13,31.0,214.12,333.2,202.11,334.3,191.10,335.4,181.9,336.5,172.8,337.6,150.7,338.7,131.6,339.8,115.5,340.10,102.4,341.11,98.3,342.12,95.2,343.13,93.1,344.15,1.0,345.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv28_1r1(x0) -> ssPv27_2r1r1(x0,x1) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.30/0.80 === Backtracking. Learning clause 1732:1:1:[346.1,264.1,106.1,1731.1]:Top: ssPv28_1r1(x0) ->
% 0.30/0.80 === Conflict found: 1726:3:16:[930.2,651.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.30/0.80 === Backtracking. Learning clause 1733:2:11:[1726.2,391.1,1725.1]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv26_3r1r1r1(x0,x1,x2),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.30/0.80 === Conflict found: 1718:3:14:[952.1,630.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.30/0.80 === Backtracking. Learning clause 1734:2:4:[1718.1,264.1,1733.2]:TopTopTopTop: -> ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv26_3r1r1r1(x0,x1,x2)
% 0.30/0.80 === Conflict found: 440:4:16:[361.15,37.0,291.14,425.2,251.13,426.3,214.12,427.4,202.11,428.6,191.10,429.7,181.9,430.8,172.8,431.9,150.7,432.10,131.6,433.11,115.5,434.12,102.4,435.13,98.3,436.14,95.2,437.15,93.1,438.16,1.0,439.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc32}
% 0.30/0.80 === Backtracking. Learning clause 1736:2:13:[1732.0,1735.2,440.1,376.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.30/0.80 === Conflict found: 1736:2:13:[1732.0,1735.2,440.1,376.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.30/0.80 === Backtracking. Learning clause 1737:1:3:[1736.2,238.1,1733.2]:TopTopTop: -> ssPv26_3r1r1r1(x0,x1,x2)
% 0.30/0.80 === Conflict found: 908:4:22:[609.21,60.0,548.20,887.2,510.19,888.3,474.18,889.4,424.17,890.5,407.16,891.6,361.15,892.7,291.14,893.8,251.13,894.9,214.12,895.10,202.11,896.11,191.10,897.12,181.9,898.13,172.8,899.14,150.7,900.15,131.6,901.16,115.5,902.17,102.4,903.18,98.3,904.19,95.2,905.20,93.1,906.21,1.0,907.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc29}
% 0.30/0.80 === Backtracking. Learning clause 1739:4:14:[1732.0,1738.3,908.2,651.1,731.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.30/0.80 === Conflict found: 1739:4:14:[1732.0,1738.3,908.2,651.1,731.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.30/0.80 === Backtracking. Learning clause 1740:3:13:[1739.1,264.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.30/0.80 === Conflict found: 1740:3:13:[1739.1,264.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.30/0.80 === Backtracking. Learning clause 1741:2:10:[1740.3,238.1]:TopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.80 === Conflict found: 908:4:22:[609.21,60.0,548.20,887.2,510.19,888.3,474.18,889.4,424.17,890.5,407.16,891.6,361.15,892.7,291.14,893.8,251.13,894.9,214.12,895.10,202.11,896.11,191.10,897.12,181.9,898.13,172.8,899.14,150.7,900.15,131.6,901.16,115.5,902.17,102.4,903.18,98.3,904.19,95.2,905.20,93.1,906.21,1.0,907.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc29}
% 0.30/0.80 === Backtracking. Learning clause 1743:3:16:[1732.0,1742.3,908.2,651.1,691.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.30/0.80 === Conflict found: 1743:3:16:[1732.0,1742.3,908.2,651.1,691.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.30/0.80 === Backtracking. Learning clause 1744:2:15:[1743.2,391.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.30/0.80 === Conflict found: 908:4:22:[609.21,60.0,548.20,887.2,510.19,888.3,474.18,889.4,424.17,890.5,407.16,891.6,361.15,892.7,291.14,893.8,251.13,894.9,214.12,895.10,202.11,896.11,191.10,897.12,181.9,898.13,172.8,899.14,150.7,900.15,131.6,901.16,115.5,902.17,102.4,903.18,98.3,904.19,95.2,905.20,93.1,906.21,1.0,907.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc29}
% 0.30/0.80 === Backtracking. Learning clause 1746:3:11:[1732.0,1745.1,908.2,651.1,711.4,1744.2,1725.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.30/0.80 === Conflict found: 1736:2:13:[1732.0,1735.2,440.1,376.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.30/0.80 === Backtracking. Learning clause 1747:2:6:[1736.2,238.1,1746.3]:TopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.30/0.80 === Conflict found: 1747:2:6:[1736.2,238.1,1746.3]:TopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc45}
% 0.30/0.80
% 0.30/0.80 SZS status Unsatisfiable
% 0.30/0.80
% 0.30/0.80 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.80
% 0.30/0.80 SPASS-SCL-FOL Statistics:
% 0.30/0.80 Number of learned clauses: 31
% 0.30/0.80 Number of propagations: 260
% 0.30/0.80 Number of decisions: 235
% 0.30/0.80 Number of resolutions: 47
% 0.30/0.80 Number of condensations: 0
% 0.30/0.80 Number of sub resolutions: 1624
% 0.30/0.80 Number of input literals (deduplicated): 80
% 0.30/0.80 Number of grows: 2
% 0.30/0.80 Number of considered ground atoms: 38
% 0.30/0.80
% 0.30/0.80 Needed: 0:00:00.08
% 0.30/0.80
%------------------------------------------------------------------------------