%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN889-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n025.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 0.57s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN889-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n025.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 13:50:29 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.22/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.57/0.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/0.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/0.61 Execution resolution_1 ended with status: unsatisfiable
% 0.57/0.61 Used heuristic: resolution_1
% 0.57/0.61
% 0.57/0.61 Input Clauses:
% 0.57/0.62
% 0.57/0.62 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv16_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv15_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv14_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv13_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssPv18_3r1r1r1 ssPv20_1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssPv19_2r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_4r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 0.57/0.62 Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17
% 0.57/0.62 Fol Functions:
% 0.57/0.62 Problem Properties:
% 0.57/0.62 This is a Bernays Schoenfinkel problem.
% 0.57/0.62
% 0.57/0.62 After reduction: Problem Properties:
% 0.57/0.62 This is a Bernays Schoenfinkel problem.
% 0.57/0.62
% 0.57/0.62
% 0.57/0.62 Reduced Input Clauses:
% 0.57/0.62 87:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 0.57/0.62 89:1:2:[87.1,3.0,1.0,88.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 0.57/0.62 92:1:3:[89.2,4.0,87.1,90.1,1.0,91.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 0.57/0.62 96:1:4:[92.3,5.0,89.2,93.1,87.1,94.2,1.0,95.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 0.57/0.62 100:1:4:[92.3,6.0,89.2,97.1,87.1,98.2,1.0,99.3]:TopTopTopTop: -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc30)
% 0.57/0.62 104:1:4:[92.3,7.1,89.2,101.2,87.1,102.3,1.0,103.4]:TopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc31) ->
% 0.57/0.62 109:1:5:[96.4,8.0,92.3,105.1,89.2,106.2,87.1,107.3,1.0,108.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.57/0.62 114:1:5:[96.4,9.0,92.3,110.1,89.2,111.2,87.1,112.3,1.0,113.4]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28)
% 0.57/0.62 119:1:5:[96.4,10.1,92.3,115.2,89.2,116.3,87.1,117.4,1.0,118.5]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29) ->
% 0.57/0.62 125:1:6:[109.5,11.0,96.4,120.1,92.3,121.2,89.2,122.3,87.1,123.4,1.0,124.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 131:1:6:[109.5,12.0,96.4,126.1,92.3,127.2,89.2,128.3,87.1,129.4,1.0,130.5]:TopTopTopTopTopTop: -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26)
% 0.57/0.62 137:1:6:[109.5,13.1,96.4,132.2,92.3,133.3,89.2,134.4,87.1,135.5,1.0,136.6]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27) ->
% 0.57/0.62 144:1:7:[125.6,14.0,109.5,138.1,96.4,139.2,92.3,140.3,89.2,141.4,87.1,142.5,1.0,143.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.57/0.62 151:1:7:[125.6,15.0,109.5,145.1,96.4,146.2,92.3,147.3,89.2,148.4,87.1,149.5,1.0,150.6]:TopTopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24)
% 0.57/0.62 158:1:7:[125.6,16.1,109.5,152.2,96.4,153.3,92.3,154.4,89.2,155.5,87.1,156.6,1.0,157.7]:TopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25) ->
% 0.57/0.62 166:1:8:[144.7,17.0,125.6,159.1,109.5,160.2,96.4,161.3,92.3,162.4,89.2,163.5,87.1,164.6,1.0,165.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.57/0.62 175:1:9:[166.8,18.0,144.7,167.1,125.6,168.2,109.5,169.3,96.4,170.4,92.3,171.5,89.2,172.6,87.1,173.7,1.0,174.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.57/0.62 183:4:8:[144.7,19.0,125.6,176.1,109.5,177.2,96.4,178.3,92.3,179.5,89.2,180.6,87.1,181.8,1.0,182.9]:TopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.57/0.62 193:1:10:[175.9,20.0,166.8,184.1,144.7,185.2,125.6,186.3,109.5,187.4,96.4,188.5,92.3,189.6,89.2,190.7,87.1,191.8,1.0,192.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.57/0.62 204:1:11:[193.10,21.0,175.9,194.1,166.8,195.2,144.7,196.3,125.6,197.4,109.5,198.5,96.4,199.6,92.3,200.7,89.2,201.8,87.1,202.9,1.0,203.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.57/0.62 214:4:10:[175.9,22.0,166.8,205.1,144.7,206.3,125.6,207.4,109.5,208.5,96.4,209.6,92.3,210.7,89.2,211.8,87.1,212.9,1.0,213.10]:TopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2)
% 0.57/0.62 226:1:12:[204.11,23.0,193.10,215.1,175.9,216.2,166.8,217.3,144.7,218.4,125.6,219.5,109.5,220.6,96.4,221.7,92.3,222.8,89.2,223.9,87.1,224.10,1.0,225.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 238:1:12:[204.11,24.0,193.10,227.1,175.9,228.2,166.8,229.3,144.7,230.4,125.6,231.5,109.5,232.6,96.4,233.7,92.3,234.8,89.2,235.9,87.1,236.10,1.0,237.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 0.57/0.62 250:1:12:[204.11,25.1,193.10,239.2,175.9,240.3,166.8,241.4,144.7,242.5,125.6,243.6,109.5,244.7,96.4,245.8,92.3,246.9,89.2,247.10,87.1,248.11,1.0,249.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) ->
% 0.57/0.62 261:4:11:[193.10,26.0,175.9,251.2,166.8,252.3,144.7,253.4,125.6,254.5,109.5,255.7,96.4,256.8,92.3,257.9,89.2,258.10,87.1,259.12,1.0,260.13]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 272:4:11:[193.10,27.0,175.9,262.1,166.8,263.2,144.7,264.3,125.6,265.4,109.5,266.5,96.4,267.6,92.3,268.7,89.2,269.9,87.1,270.10,1.0,271.11]:TopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.57/0.62 285:1:13:[226.12,28.0,204.11,273.1,193.10,274.2,175.9,275.3,166.8,276.4,144.7,277.5,125.6,278.6,109.5,279.7,96.4,280.8,92.3,281.9,89.2,282.10,87.1,283.11,1.0,284.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.57/0.62 298:1:13:[226.12,29.0,204.11,286.1,193.10,287.2,175.9,288.3,166.8,289.4,144.7,290.5,125.6,291.6,109.5,292.7,96.4,293.8,92.3,294.9,89.2,295.10,87.1,296.11,1.0,297.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 0.57/0.62 311:1:13:[226.12,30.1,204.11,299.2,193.10,300.3,175.9,301.4,166.8,302.5,144.7,303.6,125.6,304.7,109.5,305.8,96.4,306.9,92.3,307.10,89.2,308.11,87.1,309.12,1.0,310.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) ->
% 0.57/0.62 323:4:12:[204.11,31.0,193.10,312.1,175.9,313.2,166.8,314.3,144.7,315.4,125.6,316.6,109.5,317.8,96.4,318.9,92.3,319.10,89.2,320.11,87.1,321.12,1.0,322.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1)
% 0.57/0.62 337:1:14:[285.13,32.0,226.12,324.1,204.11,325.2,193.10,326.3,175.9,327.4,166.8,328.5,144.7,329.6,125.6,330.7,109.5,331.8,96.4,332.9,92.3,333.10,89.2,334.11,87.1,335.12,1.0,336.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.57/0.62 351:1:14:[285.13,33.0,226.12,338.1,204.11,339.2,193.10,340.3,175.9,341.4,166.8,342.5,144.7,343.6,125.6,344.7,109.5,345.8,96.4,346.9,92.3,347.10,89.2,348.11,87.1,349.12,1.0,350.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 0.57/0.62 365:1:14:[285.13,34.1,226.12,352.2,204.11,353.3,193.10,354.4,175.9,355.5,166.8,356.6,144.7,357.7,125.6,358.8,109.5,359.9,96.4,360.10,92.3,361.11,89.2,362.12,87.1,363.13,1.0,364.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) ->
% 0.57/0.62 378:4:13:[226.12,35.0,204.11,366.2,193.10,367.4,175.9,368.5,166.8,369.6,144.7,370.7,125.6,371.8,109.5,372.9,96.4,373.10,92.3,374.11,89.2,375.12,87.1,376.13,1.0,377.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.57/0.62 393:1:15:[337.14,36.0,285.13,379.1,226.12,380.2,204.11,381.3,193.10,382.4,175.9,383.5,166.8,384.6,144.7,385.7,125.6,386.8,109.5,387.9,96.4,388.10,92.3,389.11,89.2,390.12,87.1,391.13,1.0,392.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.57/0.62 408:1:15:[337.14,37.0,285.13,394.1,226.12,395.2,204.11,396.3,193.10,397.4,175.9,398.5,166.8,399.6,144.7,400.7,125.6,401.8,109.5,402.9,96.4,403.10,92.3,404.11,89.2,405.12,87.1,406.13,1.0,407.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 0.57/0.62 423:1:15:[337.14,38.1,285.13,409.2,226.12,410.3,204.11,411.4,193.10,412.5,175.9,413.6,166.8,414.7,144.7,415.8,125.6,416.9,109.5,417.10,96.4,418.11,92.3,419.12,89.2,420.13,87.1,421.14,1.0,422.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) ->
% 0.57/0.62 437:4:14:[285.13,39.0,226.12,424.2,204.11,425.3,193.10,426.4,175.9,427.5,166.8,428.6,144.7,429.7,125.6,430.8,109.5,431.9,96.4,432.10,92.3,433.12,89.2,434.14,87.1,435.15,1.0,436.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.57/0.62 451:4:14:[285.13,40.0,226.12,438.1,204.11,439.3,193.10,440.4,175.9,441.5,166.8,442.6,144.7,443.8,125.6,444.9,109.5,445.10,96.4,446.11,92.3,447.12,89.2,448.13,87.1,449.14,1.0,450.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.57/0.62 465:4:14:[285.13,41.0,226.12,452.2,204.11,453.3,193.10,454.4,175.9,455.5,166.8,456.6,144.7,457.7,125.6,458.8,109.5,459.9,96.4,460.11,92.3,461.12,89.2,462.13,87.1,463.14,1.0,464.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.57/0.62 479:4:14:[285.13,42.0,226.12,466.1,204.11,467.3,193.10,468.4,175.9,469.5,166.8,470.7,144.7,471.8,125.6,472.9,109.5,473.10,96.4,474.11,92.3,475.13,89.2,476.14,87.1,477.15,1.0,478.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.57/0.62 494:4:15:[337.14,43.0,285.13,480.1,226.12,481.2,204.11,482.3,193.10,483.4,175.9,484.5,166.8,485.6,144.7,486.7,125.6,487.9,109.5,488.10,96.4,489.11,92.3,490.13,89.2,491.14,87.1,492.15,1.0,493.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv20_1r1(x0)
% 0.57/0.62 508:4:14:[285.13,44.0,226.12,495.1,204.11,496.3,193.10,497.4,175.9,498.5,166.8,499.6,144.7,500.8,125.6,501.9,109.5,502.10,96.4,503.11,92.3,504.12,89.2,505.13,87.1,506.14,1.0,507.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.57/0.62 522:4:14:[285.13,45.1,226.12,509.4,204.11,510.5,193.10,511.6,175.9,512.7,166.8,513.8,144.7,514.9,125.6,515.10,109.5,516.11,96.4,517.12,92.3,518.13,89.2,519.15,87.1,520.16,1.0,521.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1) ->
% 0.57/0.62 538:1:16:[393.15,46.0,337.14,523.1,285.13,524.2,226.12,525.3,204.11,526.4,193.10,527.5,175.9,528.6,166.8,529.7,144.7,530.8,125.6,531.9,109.5,532.10,96.4,533.11,92.3,534.12,89.2,535.13,87.1,536.14,1.0,537.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.57/0.62 553:4:15:[337.14,47.0,285.13,539.1,226.12,540.2,204.11,541.3,193.10,542.4,175.9,543.5,166.8,544.6,144.7,545.7,125.6,546.8,109.5,547.9,96.4,548.10,92.3,549.11,89.2,550.12,87.1,551.13,1.0,552.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 0.57/0.62 568:4:15:[337.14,48.0,285.13,554.1,226.12,555.2,204.11,556.3,193.10,557.5,175.9,558.6,166.8,559.7,144.7,560.8,125.6,561.9,109.5,562.10,96.4,563.11,92.3,564.12,89.2,565.13,87.1,566.14,1.0,567.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv18_3r1r1r1(x0,x1,x2)
% 0.57/0.62 583:4:15:[337.14,49.0,285.13,569.1,226.12,570.2,204.11,571.4,193.10,572.5,175.9,573.6,166.8,574.8,144.7,575.9,125.6,576.10,109.5,577.11,96.4,578.12,92.3,579.13,89.2,580.15,87.1,581.16,1.0,582.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.57/0.62 598:4:15:[337.14,50.0,285.13,584.2,226.12,585.3,204.11,586.4,193.10,587.5,175.9,588.6,166.8,589.7,144.7,590.8,125.6,591.9,109.5,592.10,96.4,593.11,92.3,594.12,89.2,595.14,87.1,596.15,1.0,597.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 614:4:16:[393.15,51.0,337.14,599.2,285.13,600.3,226.12,601.4,204.11,602.5,193.10,603.6,175.9,604.7,166.8,605.8,144.7,606.9,125.6,607.10,109.5,608.12,96.4,609.14,92.3,610.15,89.2,611.16,87.1,612.17,1.0,613.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv20_1r1(x0)
% 0.57/0.62 629:4:15:[337.14,52.0,285.13,615.2,226.12,616.3,204.11,617.5,193.10,618.6,175.9,619.7,166.8,620.8,144.7,621.9,125.6,622.10,109.5,623.12,96.4,624.13,92.3,625.14,89.2,626.15,87.1,627.16,1.0,628.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 645:4:16:[393.15,53.0,337.14,630.1,285.13,631.2,226.12,632.3,204.11,633.4,193.10,634.5,175.9,635.6,166.8,636.7,144.7,637.8,125.6,638.9,109.5,639.11,96.4,640.13,92.3,641.14,89.2,642.16,87.1,643.17,1.0,644.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv19_2r1r1(x0,x1) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.57/0.62 662:1:17:[538.16,54.0,393.15,646.1,337.14,647.2,285.13,648.3,226.12,649.4,204.11,650.5,193.10,651.6,175.9,652.7,166.8,653.8,144.7,654.9,125.6,655.10,109.5,656.11,96.4,657.12,92.3,658.13,89.2,659.14,87.1,660.15,1.0,661.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.57/0.62 678:4:16:[393.15,55.0,337.14,663.2,285.13,664.3,226.12,665.4,204.11,666.5,193.10,667.6,175.9,668.7,166.8,669.8,144.7,670.9,125.6,671.10,109.5,672.11,96.4,673.12,92.3,674.13,89.2,675.14,87.1,676.15,1.0,677.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1)
% 0.57/0.62 694:4:16:[393.15,56.0,337.14,679.2,285.13,680.3,226.12,681.4,204.11,682.6,193.10,683.7,175.9,684.8,166.8,685.9,144.7,686.10,125.6,687.11,109.5,688.13,96.4,689.14,92.3,690.15,89.2,691.16,87.1,692.17,1.0,693.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.57/0.62 712:1:18:[662.17,57.0,538.16,695.1,393.15,696.2,337.14,697.3,285.13,698.4,226.12,699.5,204.11,700.6,193.10,701.7,175.9,702.8,166.8,703.9,144.7,704.10,125.6,705.11,109.5,706.12,96.4,707.13,92.3,708.14,89.2,709.15,87.1,710.16,1.0,711.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.57/0.62 728:4:16:[393.15,58.0,337.14,713.1,285.13,714.2,226.12,715.3,204.11,716.5,193.10,717.6,175.9,718.7,166.8,719.8,144.7,720.9,125.6,721.10,109.5,722.11,96.4,723.12,92.3,724.13,89.2,725.14,87.1,726.15,1.0,727.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 745:4:17:[538.16,59.0,393.15,729.1,337.14,730.2,285.13,731.3,226.12,732.4,204.11,733.5,193.10,734.6,175.9,735.7,166.8,736.8,144.7,737.9,125.6,738.11,109.5,739.12,96.4,740.13,92.3,741.14,89.2,742.15,87.1,743.16,1.0,744.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 764:1:19:[712.18,60.0,662.17,746.1,538.16,747.2,393.15,748.3,337.14,749.4,285.13,750.5,226.12,751.6,204.11,752.7,193.10,753.8,175.9,754.9,166.8,755.10,144.7,756.11,125.6,757.12,109.5,758.13,96.4,759.14,92.3,760.15,89.2,761.16,87.1,762.17,1.0,763.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.57/0.62 782:4:18:[662.17,61.0,538.16,765.2,393.15,766.3,337.14,767.4,285.13,768.5,226.12,769.6,204.11,770.7,193.10,771.8,175.9,772.9,166.8,773.10,144.7,774.11,125.6,775.12,109.5,776.13,96.4,777.14,92.3,778.16,89.2,779.17,87.1,780.18,1.0,781.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 800:4:18:[662.17,62.0,538.16,783.2,393.15,784.3,337.14,785.4,285.13,786.5,226.12,787.6,204.11,788.8,193.10,789.9,175.9,790.10,166.8,791.11,144.7,792.12,125.6,793.13,109.5,794.14,96.4,795.15,92.3,796.16,89.2,797.17,87.1,798.18,1.0,799.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 818:4:18:[662.17,63.0,538.16,801.1,393.15,802.2,337.14,803.3,285.13,804.4,226.12,805.5,204.11,806.6,193.10,807.7,175.9,808.8,166.8,809.9,144.7,810.11,125.6,811.13,109.5,812.14,96.4,813.15,92.3,814.16,89.2,815.17,87.1,816.18,1.0,817.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.57/0.62 836:4:18:[662.17,64.0,538.16,819.1,393.15,820.2,337.14,821.3,285.13,822.4,226.12,823.5,204.11,824.6,193.10,825.7,175.9,826.8,166.8,827.9,144.7,828.10,125.6,829.11,109.5,830.13,96.4,831.14,92.3,832.15,89.2,833.16,87.1,834.17,1.0,835.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 854:4:18:[662.17,65.0,538.16,837.1,393.15,838.2,337.14,839.3,285.13,840.4,226.12,841.6,204.11,842.7,193.10,843.8,175.9,844.9,166.8,845.10,144.7,846.11,125.6,847.12,109.5,848.13,96.4,849.14,92.3,850.15,89.2,851.16,87.1,852.17,1.0,853.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.57/0.62 872:4:18:[662.17,66.0,538.16,855.2,393.15,856.3,337.14,857.4,285.13,858.5,226.12,859.6,204.11,860.7,193.10,861.8,175.9,862.9,166.8,863.11,144.7,864.12,125.6,865.13,109.5,866.14,96.4,867.15,92.3,868.16,89.2,869.17,87.1,870.18,1.0,871.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.57/0.62 891:4:19:[712.18,67.0,662.17,873.1,538.16,874.2,393.15,875.3,337.14,876.5,285.13,877.6,226.12,878.7,204.11,879.8,193.10,880.9,175.9,881.10,166.8,882.11,144.7,883.12,125.6,884.14,109.5,885.15,96.4,886.16,92.3,887.17,89.2,888.18,87.1,889.19,1.0,890.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.57/0.62 910:4:19:[712.18,68.0,662.17,892.2,538.16,893.3,393.15,894.4,337.14,895.5,285.13,896.6,226.12,897.7,204.11,898.8,193.10,899.9,175.9,900.10,166.8,901.12,144.7,902.13,125.6,903.14,109.5,904.15,96.4,905.16,92.3,906.18,89.2,907.19,87.1,908.20,1.0,909.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.57/0.62 929:4:19:[712.18,69.0,662.17,911.1,538.16,912.3,393.15,913.4,337.14,914.5,285.13,915.6,226.12,916.7,204.11,917.8,193.10,918.9,175.9,919.10,166.8,920.11,144.7,921.12,125.6,922.13,109.5,923.14,96.4,924.15,92.3,925.16,89.2,926.17,87.1,927.18,1.0,928.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.57/0.62 948:4:19:[712.18,70.0,662.17,930.2,538.16,931.3,393.15,932.4,337.14,933.5,285.13,934.6,226.12,935.8,204.11,936.9,193.10,937.10,175.9,938.11,166.8,939.12,144.7,940.13,125.6,941.15,109.5,942.16,96.4,943.17,92.3,944.18,89.2,945.19,87.1,946.20,1.0,947.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.57/0.62 967:4:19:[712.18,71.0,662.17,949.2,538.16,950.4,393.15,951.5,337.14,952.6,285.13,953.7,226.12,954.8,204.11,955.9,193.10,956.10,175.9,957.11,166.8,958.12,144.7,959.13,125.6,960.14,109.5,961.15,96.4,962.17,92.3,963.18,89.2,964.19,87.1,965.20,1.0,966.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.57/0.62 986:4:19:[712.18,72.0,662.17,968.2,538.16,969.3,393.15,970.4,337.14,971.6,285.13,972.7,226.12,973.8,204.11,974.9,193.10,975.10,175.9,976.11,166.8,977.12,144.7,978.13,125.6,979.14,109.5,980.16,96.4,981.17,92.3,982.18,89.2,983.19,87.1,984.20,1.0,985.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.57/0.62 1005:4:19:[712.18,73.0,662.17,987.1,538.16,988.2,393.15,989.3,337.14,990.4,285.13,991.5,226.12,992.6,204.11,993.7,193.10,994.8,175.9,995.9,166.8,996.10,144.7,997.11,125.6,998.12,109.5,999.13,96.4,1000.14,92.3,1001.15,89.2,1002.16,87.1,1003.17,1.0,1004.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.57/0.62 1024:4:19:[712.18,74.0,662.17,1006.2,538.16,1007.3,393.15,1008.4,337.14,1009.6,285.13,1010.7,226.12,1011.8,204.11,1012.9,193.10,1013.10,175.9,1014.11,166.8,1015.12,144.7,1016.13,125.6,1017.14,109.5,1018.15,96.4,1019.16,92.3,1020.17,89.2,1021.18,87.1,1022.19,1.0,1023.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.57/0.62 1043:4:19:[712.18,75.0,662.17,1025.1,538.16,1026.3,393.15,1027.5,337.14,1028.6,285.13,1029.7,226.12,1030.8,204.11,1031.9,193.10,1032.10,175.9,1033.12,166.8,1034.13,144.7,1035.14,125.6,1036.15,109.5,1037.16,96.4,1038.17,92.3,1039.18,89.2,1040.19,87.1,1041.20,1.0,1042.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.57/0.62 1062:4:19:[712.18,76.0,662.17,1044.2,538.16,1045.3,393.15,1046.5,337.14,1047.7,285.13,1048.8,226.12,1049.9,204.11,1050.11,193.10,1051.12,175.9,1052.13,166.8,1053.14,144.7,1054.15,125.6,1055.16,109.5,1056.17,96.4,1057.18,92.3,1058.19,89.2,1059.20,87.1,1060.21,1.0,1061.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ->
% 0.57/0.62 1082:4:20:[764.19,77.0,712.18,1063.2,662.17,1064.3,538.16,1065.4,393.15,1066.5,337.14,1067.6,285.13,1068.7,226.12,1069.8,204.11,1070.9,193.10,1071.10,175.9,1072.11,166.8,1073.12,144.7,1074.13,125.6,1075.14,109.5,1076.15,96.4,1077.16,92.3,1078.17,89.2,1079.18,87.1,1080.20,1.0,1081.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.57/0.62 1102:4:20:[764.19,78.0,712.18,1083.2,662.17,1084.3,538.16,1085.4,393.15,1086.5,337.14,1087.6,285.13,1088.8,226.12,1089.9,204.11,1090.10,193.10,1091.11,175.9,1092.12,166.8,1093.13,144.7,1094.14,125.6,1095.15,109.5,1096.17,96.4,1097.18,92.3,1098.19,89.2,1099.20,87.1,1100.21,1.0,1101.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.57/0.62 1122:4:20:[764.19,79.0,712.18,1103.1,662.17,1104.2,538.16,1105.3,393.15,1106.4,337.14,1107.5,285.13,1108.6,226.12,1109.7,204.11,1110.8,193.10,1111.9,175.9,1112.10,166.8,1113.11,144.7,1114.12,125.6,1115.13,109.5,1116.14,96.4,1117.15,92.3,1118.16,89.2,1119.18,87.1,1120.19,1.0,1121.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.57/0.62 1142:4:20:[764.19,80.0,712.18,1123.2,662.17,1124.3,538.16,1125.4,393.15,1126.5,337.14,1127.6,285.13,1128.7,226.12,1129.8,204.11,1130.9,193.10,1131.10,175.9,1132.11,166.8,1133.13,144.7,1134.14,125.6,1135.15,109.5,1136.16,96.4,1137.17,92.3,1138.19,89.2,1139.20,87.1,1140.21,1.0,1141.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.57/0.62 1162:4:20:[764.19,81.0,712.18,1143.2,662.17,1144.3,538.16,1145.4,393.15,1146.5,337.14,1147.6,285.13,1148.7,226.12,1149.8,204.11,1150.9,193.10,1151.10,175.9,1152.11,166.8,1153.12,144.7,1154.13,125.6,1155.14,109.5,1156.15,96.4,1157.16,92.3,1158.17,89.2,1159.18,87.1,1160.19,1.0,1161.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 1182:4:20:[764.19,82.0,712.18,1163.1,662.17,1164.2,538.16,1165.3,393.15,1166.5,337.14,1167.6,285.13,1168.7,226.12,1169.8,204.11,1170.9,193.10,1171.10,175.9,1172.12,166.8,1173.14,144.7,1174.15,125.6,1175.16,109.5,1176.17,96.4,1177.18,92.3,1178.19,89.2,1179.20,87.1,1180.21,1.0,1181.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.57/0.62 1202:4:20:[764.19,83.0,712.18,1183.1,662.17,1184.2,538.16,1185.3,393.15,1186.4,337.14,1187.6,285.13,1188.7,226.12,1189.8,204.11,1190.9,193.10,1191.10,175.9,1192.11,166.8,1193.12,144.7,1194.13,125.6,1195.15,109.5,1196.16,96.4,1197.17,92.3,1198.18,89.2,1199.19,87.1,1200.20,1.0,1201.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.57/0.62 1222:4:20:[764.19,84.0,712.18,1203.1,662.17,1204.2,538.16,1205.3,393.15,1206.4,337.14,1207.5,285.13,1208.6,226.12,1209.7,204.11,1210.8,193.10,1211.9,175.9,1212.10,166.8,1213.11,144.7,1214.12,125.6,1215.13,109.5,1216.14,96.4,1217.15,92.3,1218.16,89.2,1219.17,87.1,1220.18,1.0,1221.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 1242:4:20:[764.19,85.0,712.18,1223.1,662.17,1224.2,538.16,1225.3,393.15,1226.4,337.14,1227.5,285.13,1228.6,226.12,1229.7,204.11,1230.8,193.10,1231.9,175.9,1232.10,166.8,1233.11,144.7,1234.12,125.6,1235.13,109.5,1236.14,96.4,1237.15,92.3,1238.16,89.2,1239.17,87.1,1240.18,1.0,1241.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.57/0.62 1262:4:20:[764.19,86.0,712.18,1243.2,662.17,1244.3,538.16,1245.4,393.15,1246.5,337.14,1247.6,285.13,1248.8,226.12,1249.9,204.11,1250.10,193.10,1251.11,175.9,1252.12,166.8,1253.13,144.7,1254.14,125.6,1255.15,109.5,1256.16,96.4,1257.17,92.3,1258.18,89.2,1259.19,87.1,1260.20,1.0,1261.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.57/0.62
% 0.57/0.62 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) ssPv18_3r1r1r1(x0,x1,x2) ssPv20_1r1(x0) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) 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) ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv19_2r1r1(x0,x1) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv6_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) ssPv5_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) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.57/0.62
% 0.57/0.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 28 atoms initially, heuristics mode: resolution_1 ===
% 0.57/0.62
% 0.57/0.62 === Conflict found: 183:4:8:[144.7,19.0,125.6,176.1,109.5,177.2,96.4,178.3,92.3,179.5,89.2,180.6,87.1,181.8,1.0,182.9]:TopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc25}
% 0.57/0.62 === Backtracking. Learning clause 1263:3:7:[183.4,158.1]:TopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.57/0.62 === Conflict found: 378:4:13:[226.12,35.0,204.11,366.2,193.10,367.4,175.9,368.5,166.8,369.6,144.7,370.7,125.6,371.8,109.5,372.9,96.4,373.10,92.3,374.11,89.2,375.12,87.1,376.13,1.0,377.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 0.57/0.62 === Backtracking. Learning clause 1264:3:10:[378.1,238.1]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.57/0.62 === Conflict found: 437:4:14:[285.13,39.0,226.12,424.2,204.11,425.3,193.10,426.4,175.9,427.5,166.8,428.6,144.7,429.7,125.6,430.8,109.5,431.9,96.4,432.10,92.3,433.12,89.2,434.14,87.1,435.15,1.0,436.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20}
% 0.57/0.62 === Backtracking. Learning clause 1265:3:13:[437.1,298.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.57/0.62 === Conflict found: 522:4:14:[285.13,45.1,226.12,509.4,204.11,510.5,193.10,511.6,175.9,512.7,166.8,513.8,144.7,514.9,125.6,515.10,109.5,516.11,96.4,517.12,92.3,518.13,89.2,519.15,87.1,520.16,1.0,521.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20}
% 0.57/0.62 === Backtracking. Learning clause 1266:3:12:[522.2,298.1,1265.3]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) ->
% 0.57/0.62 === Conflict found: 598:4:15:[337.14,50.0,285.13,584.2,226.12,585.3,204.11,586.4,193.10,587.5,175.9,588.6,166.8,589.7,144.7,590.8,125.6,591.9,109.5,592.10,96.4,593.11,92.3,594.12,89.2,595.14,87.1,596.15,1.0,597.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.57/0.62 === Backtracking. Learning clause 1267:2:3:[598.3,365.1,1265.3,1266.1]:TopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) ->
% 0.57/0.62 === Clause set with instances from active satisfied. Growing active. New size: 30
% 0.57/0.62 === Restarting.
% 0.57/0.62 === Conflict found: 836:4:18:[662.17,64.0,538.16,819.1,393.15,820.2,337.14,821.3,285.13,822.4,226.12,823.5,204.11,824.6,193.10,825.7,175.9,826.8,166.8,827.9,144.7,828.10,125.6,829.11,109.5,830.13,96.4,831.14,92.3,832.15,89.2,833.16,87.1,834.17,1.0,835.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 0.57/0.62 === Backtracking. Learning clause 1268:6:15:[836.2,782.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 1268:6:15:[836.2,782.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.57/0.62 === Backtracking. Learning clause 1269:5:14:[1268.3,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 1269:5:14:[1268.3,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21}
% 0.57/0.62 === Backtracking. Learning clause 1270:4:12:[1269.4,311.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 1005:4:19:[712.18,73.0,662.17,987.1,538.16,988.2,393.15,989.3,337.14,990.4,285.13,991.5,226.12,992.6,204.11,993.7,193.10,994.8,175.9,995.9,166.8,996.10,144.7,997.11,125.6,998.12,109.5,999.13,96.4,1000.14,92.3,1001.15,89.2,1002.16,87.1,1003.17,1.0,1004.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.57/0.62 === Backtracking. Learning clause 1271:6:15:[1005.2,910.1,782.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 1271:6:15:[1005.2,910.1,782.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.57/0.62 === Backtracking. Learning clause 1272:5:14:[1271.4,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 1272:5:14:[1271.4,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21}
% 0.57/0.62 === Backtracking. Learning clause 1273:4:8:[1272.4,311.1]:TopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 782:4:18:[662.17,61.0,538.16,765.2,393.15,766.3,337.14,767.4,285.13,768.5,226.12,769.6,204.11,770.7,193.10,771.8,175.9,772.9,166.8,773.10,144.7,774.11,125.6,775.12,109.5,776.13,96.4,777.14,92.3,778.16,89.2,779.17,87.1,780.18,1.0,781.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 0.57/0.62 === Backtracking. Learning clause 1274:5:14:[782.1,854.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.57/0.62 === Conflict found: 1274:5:14:[782.1,854.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21}
% 0.57/0.62 === Backtracking. Learning clause 1275:4:7:[1274.4,311.1,1270.3,1273.1]:TopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 1275:4:7:[1274.4,311.1,1270.3,1273.1]:TopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27}
% 0.57/0.62 === Backtracking. Learning clause 1276:3:6:[1275.3,137.1]:TopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.57/0.62 === Conflict found: 494:4:15:[337.14,43.0,285.13,480.1,226.12,481.2,204.11,482.3,193.10,483.4,175.9,484.5,166.8,485.6,144.7,486.7,125.6,487.9,109.5,488.10,96.4,489.11,92.3,490.13,89.2,491.14,87.1,492.15,1.0,493.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.57/0.62 === Backtracking. Learning clause 1277:2:3:[494.3,365.1,1276.3,100.1]:TopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> ssPv20_1r1(x0)
% 0.57/0.62 === Conflict found: 553:4:15:[337.14,47.0,285.13,539.1,226.12,540.2,204.11,541.3,193.10,542.4,175.9,543.5,166.8,544.6,144.7,545.7,125.6,546.8,109.5,547.9,96.4,548.10,92.3,549.11,89.2,550.12,87.1,551.13,1.0,552.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.57/0.62 === Backtracking. Learning clause 1278:3:14:[553.2,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 0.57/0.62 === Conflict found: 1278:3:14:[553.2,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21}
% 0.57/0.62 === Backtracking. Learning clause 1279:2:2:[1278.1,311.1,1277.1]:TopTop: -> ssPv19_2r1r1(x0,x1),ssPv20_1r1(x0)
% 0.57/0.62 === Conflict found: 598:4:15:[337.14,50.0,285.13,584.2,226.12,585.3,204.11,586.4,193.10,587.5,175.9,588.6,166.8,589.7,144.7,590.8,125.6,591.9,109.5,592.10,96.4,593.11,92.3,594.12,89.2,595.14,87.1,596.15,1.0,597.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.57/0.62 === Backtracking. Learning clause 1280:3:13:[598.3,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 === Conflict found: 1280:3:13:[598.3,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 0.57/0.62 === Backtracking. Learning clause 1281:2:12:[1280.1,238.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.57/0.62 === Conflict found: 522:4:14:[285.13,45.1,226.12,509.4,204.11,510.5,193.10,511.6,175.9,512.7,166.8,513.8,144.7,514.9,125.6,515.10,109.5,516.11,96.4,517.12,92.3,518.13,89.2,519.15,87.1,520.16,1.0,521.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20}
% 0.57/0.62 === Backtracking. Learning clause 1283:2:13:[1280.2,1282.1,522.2,298.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) ->
% 0.57/0.62 === Conflict found: 1283:2:13:[1280.2,1282.1,522.2,298.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 0.57/0.62 === Backtracking. Learning clause 1284:1:1:[1283.1,238.1,1279.1]:Top: -> ssPv20_1r1(x0)
% 0.57/0.62 === Conflict found: 1263:3:7:[183.4,158.1]:TopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27}
% 0.57/0.62 === Backtracking. Learning clause 1286:1:3:[1277.1,1285.1,1263.3,137.1]:TopTopTop: ssPv18_3r1r1r1(x0,x1,x2) ->
% 0.57/0.62 === Conflict found: 1278:3:14:[553.2,365.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21}
% 0.57/0.62 === Backtracking. Learning clause 1287:1:2:[1278.1,311.1,1286.1]:TopTop: -> ssPv19_2r1r1(x0,x1)
% 0.57/0.62 === Conflict found: 1283:2:13:[1280.2,1282.1,522.2,298.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 0.57/0.62
% 0.57/0.62 SZS status Unsatisfiable
% 0.57/0.62
% 0.57/0.62 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/0.62
% 0.57/0.62 SPASS-SCL-FOL Statistics:
% 0.57/0.62 Number of learned clauses: 23
% 0.57/0.62 Number of propagations: 204
% 0.57/0.62 Number of decisions: 147
% 0.57/0.62 Number of resolutions: 36
% 0.57/0.62 Number of condensations: 0
% 0.57/0.62 Number of sub resolutions: 1178
% 0.57/0.62 Number of input literals (deduplicated): 56
% 0.57/0.62 Number of grows: 1
% 0.57/0.62 Number of considered ground atoms: 30
% 0.57/0.62
% 0.57/0.62 Needed: 0:00:00.06
% 0.57/0.62
%------------------------------------------------------------------------------