%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN892-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 : n012.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.38s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SYN892-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.08 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.27 % Computer : n012.cluster.edu
% 0.09/0.27 % Model : x86_64 x86_64
% 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.27 % Memory : 8042.1875MB
% 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.27 % CPULimit : 300
% 0.09/0.27 % WCLimit : 300
% 0.09/0.27 % DateTime : Thu May 7 13:50:16 EDT 2026
% 0.09/0.27 % CPUTime :
% 0.09/0.27 SPASS-SCL-FOL version:
% 0.09/0.32 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.38/0.48 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.48 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.48 Execution resolution_3 ended with status: unsatisfiable
% 0.38/0.48 Used heuristic: resolution_3
% 0.38/0.48
% 0.38/0.48 Input Clauses:
% 0.38/0.48
% 0.38/0.48 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 ssPv20_1r1 ssPv19_2r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv18_3r1r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_4r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 0.38/0.48 Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17
% 0.38/0.48 Fol Functions:
% 0.38/0.48 Problem Properties:
% 0.38/0.48 This is a Bernays Schoenfinkel problem.
% 0.38/0.48
% 0.38/0.48 After reduction: Problem Properties:
% 0.38/0.48 This is a Bernays Schoenfinkel problem.
% 0.38/0.48
% 0.38/0.48
% 0.38/0.48 Reduced Input Clauses:
% 0.38/0.48 87:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 0.38/0.48 89:1:2:[87.1,3.0,1.0,88.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 0.38/0.48 92:1:3:[89.2,4.0,87.1,90.1,1.0,91.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 0.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 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.38/0.48 173:4:7:[125.6,18.0,109.5,167.1,96.4,168.2,92.3,169.3,89.2,170.4,87.1,171.6,1.0,172.7]:TopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 182:1:9:[166.8,19.0,144.7,174.1,125.6,175.2,109.5,176.3,96.4,177.4,92.3,178.5,89.2,179.6,87.1,180.7,1.0,181.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.38/0.48 192:1:10:[182.9,20.0,166.8,183.1,144.7,184.2,125.6,185.3,109.5,186.4,96.4,187.5,92.3,188.6,89.2,189.7,87.1,190.8,1.0,191.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.38/0.48 201:4:9:[166.8,21.0,144.7,193.2,125.6,194.3,109.5,195.4,96.4,196.5,92.3,197.6,89.2,198.7,87.1,199.8,1.0,200.9]:TopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 212:1:11:[192.10,22.0,182.9,202.1,166.8,203.2,144.7,204.3,125.6,205.4,109.5,206.5,96.4,207.6,92.3,208.7,89.2,209.8,87.1,210.9,1.0,211.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.38/0.48 222:4:10:[182.9,23.0,166.8,213.1,144.7,214.2,125.6,215.3,109.5,216.5,96.4,217.6,92.3,218.7,89.2,219.8,87.1,220.10,1.0,221.11]:TopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.38/0.48 234:1:12:[212.11,24.0,192.10,223.1,182.9,224.2,166.8,225.3,144.7,226.4,125.6,227.5,109.5,228.6,96.4,229.7,92.3,230.8,89.2,231.9,87.1,232.10,1.0,233.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.48 246:1:12:[212.11,25.0,192.10,235.1,182.9,236.2,166.8,237.3,144.7,238.4,125.6,239.5,109.5,240.6,96.4,241.7,92.3,242.8,89.2,243.9,87.1,244.10,1.0,245.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 0.38/0.48 258:1:12:[212.11,26.1,192.10,247.2,182.9,248.3,166.8,249.4,144.7,250.5,125.6,251.6,109.5,252.7,96.4,253.8,92.3,254.9,89.2,255.10,87.1,256.11,1.0,257.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) ->
% 0.38/0.48 269:4:11:[192.10,27.0,182.9,259.1,166.8,260.2,144.7,261.3,125.6,262.5,109.5,263.6,96.4,264.7,92.3,265.9,89.2,266.10,87.1,267.11,1.0,268.12]:TopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.38/0.48 282:1:13:[234.12,28.0,212.11,270.1,192.10,271.2,182.9,272.3,166.8,273.4,144.7,274.5,125.6,275.6,109.5,276.7,96.4,277.8,92.3,278.9,89.2,279.10,87.1,280.11,1.0,281.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.48 295:1:13:[234.12,29.0,212.11,283.1,192.10,284.2,182.9,285.3,166.8,286.4,144.7,287.5,125.6,288.6,109.5,289.7,96.4,290.8,92.3,291.9,89.2,292.10,87.1,293.11,1.0,294.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 0.38/0.48 308:1:13:[234.12,30.1,212.11,296.2,192.10,297.3,182.9,298.4,166.8,299.5,144.7,300.6,125.6,301.7,109.5,302.8,96.4,303.9,92.3,304.10,89.2,305.11,87.1,306.12,1.0,307.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) ->
% 0.38/0.48 320:4:12:[212.11,31.0,192.10,309.1,182.9,310.2,166.8,311.3,144.7,312.5,125.6,313.7,109.5,314.8,96.4,315.9,92.3,316.10,89.2,317.11,87.1,318.12,1.0,319.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.48 334:1:14:[282.13,32.0,234.12,321.1,212.11,322.2,192.10,323.3,182.9,324.4,166.8,325.5,144.7,326.6,125.6,327.7,109.5,328.8,96.4,329.9,92.3,330.10,89.2,331.11,87.1,332.12,1.0,333.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.48 346:4:12:[212.11,33.1,192.10,335.3,182.9,336.4,166.8,337.6,144.7,338.7,125.6,339.9,109.5,340.10,96.4,341.11,92.3,342.12,89.2,343.13,87.1,344.14,1.0,345.15]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ->
% 0.38/0.48 360:1:14:[282.13,34.0,234.12,347.1,212.11,348.2,192.10,349.3,182.9,350.4,166.8,351.5,144.7,352.6,125.6,353.7,109.5,354.8,96.4,355.9,92.3,356.10,89.2,357.11,87.1,358.12,1.0,359.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 0.38/0.48 374:1:14:[282.13,35.1,234.12,361.2,212.11,362.3,192.10,363.4,182.9,364.5,166.8,365.6,144.7,366.7,125.6,367.8,109.5,368.9,96.4,369.10,92.3,370.11,89.2,371.12,87.1,372.13,1.0,373.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) ->
% 0.38/0.48 387:4:13:[234.12,36.0,212.11,375.1,192.10,376.2,182.9,377.3,166.8,378.4,144.7,379.5,125.6,380.7,109.5,381.8,96.4,382.9,92.3,383.10,89.2,384.12,87.1,385.13,1.0,386.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> 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)
% 0.38/0.48 400:4:13:[234.12,37.0,212.11,388.1,192.10,389.2,182.9,390.3,166.8,391.4,144.7,392.5,125.6,393.6,109.5,394.8,96.4,395.9,92.3,396.10,89.2,397.11,87.1,398.12,1.0,399.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.48 413:4:13:[234.12,38.0,212.11,401.2,192.10,402.3,182.9,403.4,166.8,404.5,144.7,405.6,125.6,406.8,109.5,407.9,96.4,408.10,92.3,409.11,89.2,410.12,87.1,411.13,1.0,412.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.48 426:4:13:[234.12,39.1,212.11,414.3,192.10,415.4,182.9,416.5,166.8,417.6,144.7,418.8,125.6,419.9,109.5,420.10,96.4,421.11,92.3,422.12,89.2,423.14,87.1,424.15,1.0,425.16]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) ->
% 0.38/0.48 440:4:14:[282.13,40.0,234.12,427.1,212.11,428.2,192.10,429.3,182.9,430.4,166.8,431.5,144.7,432.6,125.6,433.7,109.5,434.8,96.4,435.9,92.3,436.10,89.2,437.11,87.1,438.12,1.0,439.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv20_1r1(x0)
% 0.38/0.48 454:4:14:[282.13,41.0,234.12,441.2,212.11,442.3,192.10,443.4,182.9,444.5,166.8,445.6,144.7,446.7,125.6,447.8,109.5,448.9,96.4,449.11,92.3,450.12,89.2,451.13,87.1,452.14,1.0,453.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 469:1:15:[334.14,42.0,282.13,455.1,234.12,456.2,212.11,457.3,192.10,458.4,182.9,459.5,166.8,460.6,144.7,461.7,125.6,462.8,109.5,463.9,96.4,464.10,92.3,465.11,89.2,466.12,87.1,467.13,1.0,468.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.38/0.48 484:1:15:[334.14,43.0,282.13,470.1,234.12,471.2,212.11,472.3,192.10,473.4,182.9,474.5,166.8,475.6,144.7,476.7,125.6,477.8,109.5,478.9,96.4,479.10,92.3,480.11,89.2,481.12,87.1,482.13,1.0,483.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 0.38/0.48 499:1:15:[334.14,44.1,282.13,485.2,234.12,486.3,212.11,487.4,192.10,488.5,182.9,489.6,166.8,490.7,144.7,491.8,125.6,492.9,109.5,493.10,96.4,494.11,92.3,495.12,89.2,496.13,87.1,497.14,1.0,498.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) ->
% 0.38/0.48 512:4:13:[234.12,45.1,212.11,500.3,192.10,501.4,182.9,502.6,166.8,503.7,144.7,504.8,125.6,505.9,109.5,506.10,96.4,507.11,92.3,508.12,89.2,509.13,87.1,510.14,1.0,511.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.38/0.48 526:4:14:[282.13,46.0,234.12,513.1,212.11,514.2,192.10,515.4,182.9,516.5,166.8,517.6,144.7,518.7,125.6,519.8,109.5,520.9,96.4,521.10,92.3,522.11,89.2,523.12,87.1,524.13,1.0,525.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.48 542:1:16:[469.15,47.0,334.14,527.1,282.13,528.2,234.12,529.3,212.11,530.4,192.10,531.5,182.9,532.6,166.8,533.7,144.7,534.8,125.6,535.9,109.5,536.10,96.4,537.11,92.3,538.12,89.2,539.13,87.1,540.14,1.0,541.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.38/0.48 557:4:15:[334.14,48.1,282.13,543.3,234.12,544.4,212.11,545.5,192.10,546.6,182.9,547.7,166.8,548.8,144.7,549.9,125.6,550.10,109.5,551.11,96.4,552.12,92.3,553.13,89.2,554.14,87.1,555.15,1.0,556.16]: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),ssPv20_1r1(x0)
% 0.38/0.48 572:4:15:[334.14,49.0,282.13,558.1,234.12,559.2,212.11,560.3,192.10,561.4,182.9,562.5,166.8,563.6,144.7,564.8,125.6,565.9,109.5,566.10,96.4,567.11,92.3,568.12,89.2,569.13,87.1,570.14,1.0,571.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.48 587:4:15:[334.14,50.0,282.13,573.1,234.12,574.2,212.11,575.3,192.10,576.4,182.9,577.5,166.8,578.6,144.7,579.7,125.6,580.9,109.5,581.10,96.4,582.11,92.3,583.12,89.2,584.13,87.1,585.14,1.0,586.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> 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),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 602:4:15:[334.14,51.0,282.13,588.1,234.12,589.3,212.11,590.4,192.10,591.5,182.9,592.6,166.8,593.7,144.7,594.8,125.6,595.9,109.5,596.10,96.4,597.11,92.3,598.12,89.2,599.13,87.1,600.15,1.0,601.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv20_1r1(x0) -> 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.38/0.48 617:4:15:[334.14,52.1,282.13,603.3,234.12,604.4,212.11,605.5,192.10,606.6,182.9,607.7,166.8,608.8,144.7,609.9,125.6,610.10,109.5,611.11,96.4,612.13,92.3,613.14,89.2,614.15,87.1,615.16,1.0,616.17]: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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv20_1r1(x0)
% 0.38/0.48 632:4:15:[334.14,53.0,282.13,618.2,234.12,619.3,212.11,620.4,192.10,621.5,182.9,622.6,166.8,623.7,144.7,624.8,125.6,625.9,109.5,626.10,96.4,627.12,92.3,628.14,89.2,629.15,87.1,630.16,1.0,631.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.48 649:1:17:[542.16,54.0,469.15,633.1,334.14,634.2,282.13,635.3,234.12,636.4,212.11,637.5,192.10,638.6,182.9,639.7,166.8,640.8,144.7,641.9,125.6,642.10,109.5,643.11,96.4,644.12,92.3,645.13,89.2,646.14,87.1,647.15,1.0,648.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.38/0.48 664:4:15:[334.14,55.0,282.13,650.2,234.12,651.3,212.11,652.5,192.10,653.6,182.9,654.7,166.8,655.8,144.7,656.9,125.6,657.10,109.5,658.11,96.4,659.12,92.3,660.13,89.2,661.14,87.1,662.15,1.0,663.16]: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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.38/0.48 680:4:16:[469.15,56.0,334.14,665.2,282.13,666.3,234.12,667.4,212.11,668.5,192.10,669.6,182.9,670.8,166.8,671.10,144.7,672.11,125.6,673.12,109.5,674.13,96.4,675.14,92.3,676.15,89.2,677.16,87.1,678.17,1.0,679.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv19_2r1r1(x0,x1)
% 0.38/0.48 696:4:16:[469.15,57.0,334.14,681.2,282.13,682.3,234.12,683.4,212.11,684.5,192.10,685.6,182.9,686.8,166.8,687.9,144.7,688.10,125.6,689.11,109.5,690.12,96.4,691.13,92.3,692.14,89.2,693.16,87.1,694.17,1.0,695.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv19_2r1r1(x0,x1) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.38/0.48 714:1:18:[649.17,58.0,542.16,697.1,469.15,698.2,334.14,699.3,282.13,700.4,234.12,701.5,212.11,702.6,192.10,703.7,182.9,704.8,166.8,705.9,144.7,706.10,125.6,707.11,109.5,708.12,96.4,709.13,92.3,710.14,89.2,711.15,87.1,712.16,1.0,713.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.38/0.48 731:4:17:[542.16,59.0,469.15,715.2,334.14,716.3,282.13,717.5,234.12,718.6,212.11,719.7,192.10,720.8,182.9,721.9,166.8,722.10,144.7,723.11,125.6,724.12,109.5,725.13,96.4,726.14,92.3,727.15,89.2,728.16,87.1,729.17,1.0,730.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0)
% 0.38/0.48 748:4:17:[542.16,60.0,469.15,732.1,334.14,733.3,282.13,734.4,234.12,735.5,212.11,736.6,192.10,737.7,182.9,738.8,166.8,739.9,144.7,740.10,125.6,741.11,109.5,742.12,96.4,743.14,92.3,744.15,89.2,745.16,87.1,746.17,1.0,747.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.48 765:4:17:[542.16,61.0,469.15,749.2,334.14,750.4,282.13,751.5,234.12,752.6,212.11,753.8,192.10,754.9,182.9,755.10,166.8,756.11,144.7,757.12,125.6,758.13,109.5,759.15,96.4,760.16,92.3,761.17,89.2,762.18,87.1,763.19,1.0,764.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ->
% 0.38/0.48 783:4:18:[649.17,62.0,542.16,766.1,469.15,767.2,334.14,768.3,282.13,769.4,234.12,770.5,212.11,771.6,192.10,772.7,182.9,773.8,166.8,774.9,144.7,775.10,125.6,776.11,109.5,777.12,96.4,778.13,92.3,779.15,89.2,780.16,87.1,781.17,1.0,782.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.38/0.48 802:1:19:[714.18,63.0,649.17,784.1,542.16,785.2,469.15,786.3,334.14,787.4,282.13,788.5,234.12,789.6,212.11,790.7,192.10,791.8,182.9,792.9,166.8,793.10,144.7,794.11,125.6,795.12,109.5,796.13,96.4,797.14,92.3,798.15,89.2,799.16,87.1,800.17,1.0,801.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.38/0.48 820:4:18:[649.17,64.0,542.16,803.1,469.15,804.3,334.14,805.4,282.13,806.6,234.12,807.7,212.11,808.8,192.10,809.9,182.9,810.10,166.8,811.11,144.7,812.12,125.6,813.13,109.5,814.14,96.4,815.15,92.3,816.16,89.2,817.17,87.1,818.18,1.0,819.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 838:4:18:[649.17,65.0,542.16,821.2,469.15,822.3,334.14,823.4,282.13,824.6,234.12,825.7,212.11,826.8,192.10,827.9,182.9,828.10,166.8,829.11,144.7,830.12,125.6,831.13,109.5,832.14,96.4,833.15,92.3,834.16,89.2,835.17,87.1,836.18,1.0,837.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv20_1r1(x0)
% 0.38/0.48 856:4:18:[649.17,66.0,542.16,839.1,469.15,840.3,334.14,841.4,282.13,842.6,234.12,843.7,212.11,844.8,192.10,845.9,182.9,846.10,166.8,847.11,144.7,848.12,125.6,849.13,109.5,850.14,96.4,851.15,92.3,852.16,89.2,853.17,87.1,854.19,1.0,855.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.38/0.48 875:4:19:[714.18,67.0,649.17,857.2,542.16,858.3,469.15,859.4,334.14,860.5,282.13,861.6,234.12,862.7,212.11,863.8,192.10,864.9,182.9,865.10,166.8,866.12,144.7,867.13,125.6,868.14,109.5,869.15,96.4,870.16,92.3,871.17,89.2,872.18,87.1,873.19,1.0,874.20]: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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.48 894:4:19:[714.18,68.0,649.17,876.1,542.16,877.3,469.15,878.4,334.14,879.5,282.13,880.6,234.12,881.7,212.11,882.8,192.10,883.9,182.9,884.10,166.8,885.11,144.7,886.12,125.6,887.13,109.5,888.14,96.4,889.15,92.3,890.16,89.2,891.17,87.1,892.18,1.0,893.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),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.48 913:4:19:[714.18,69.0,649.17,895.1,542.16,896.2,469.15,897.4,334.14,898.5,282.13,899.6,234.12,900.7,212.11,901.8,192.10,902.9,182.9,903.11,166.8,904.12,144.7,905.13,125.6,906.14,109.5,907.15,96.4,908.16,92.3,909.17,89.2,910.18,87.1,911.19,1.0,912.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.38/0.48 933:4:20:[802.19,70.0,714.18,914.1,649.17,915.2,542.16,916.3,469.15,917.4,334.14,918.5,282.13,919.6,234.12,920.7,212.11,921.8,192.10,922.9,182.9,923.10,166.8,924.11,144.7,925.12,125.6,926.13,109.5,927.14,96.4,928.15,92.3,929.16,89.2,930.17,87.1,931.18,1.0,932.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 952:4:19:[714.18,71.0,649.17,934.1,542.16,935.2,469.15,936.3,334.14,937.4,282.13,938.6,234.12,939.8,212.11,940.9,192.10,941.10,182.9,942.11,166.8,943.12,144.7,944.13,125.6,945.14,109.5,946.15,96.4,947.16,92.3,948.17,89.2,949.18,87.1,950.19,1.0,951.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> 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)
% 0.38/0.48 971:4:19:[714.18,72.0,649.17,953.2,542.16,954.4,469.15,955.5,334.14,956.7,282.13,957.8,234.12,958.9,212.11,959.10,192.10,960.11,182.9,961.12,166.8,962.13,144.7,963.14,125.6,964.15,109.5,965.16,96.4,966.17,92.3,967.18,89.2,968.19,87.1,969.21,1.0,970.22]: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),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_1r1(x0) ->
% 0.38/0.48 991:4:20:[802.19,73.0,714.18,972.1,649.17,973.2,542.16,974.3,469.15,975.4,334.14,976.5,282.13,977.6,234.12,978.7,212.11,979.8,192.10,980.9,182.9,981.10,166.8,982.11,144.7,983.13,125.6,984.14,109.5,985.16,96.4,986.17,92.3,987.18,89.2,988.19,87.1,989.21,1.0,990.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.38/0.48 1010:4:19:[714.18,74.0,649.17,992.2,542.16,993.3,469.15,994.4,334.14,995.6,282.13,996.7,234.12,997.8,212.11,998.9,192.10,999.10,182.9,1000.11,166.8,1001.12,144.7,1002.13,125.6,1003.14,109.5,1004.15,96.4,1005.16,92.3,1006.17,89.2,1007.18,87.1,1008.19,1.0,1009.20]: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) -> 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)
% 0.38/0.48 1029:4:19:[714.18,75.0,649.17,1011.1,542.16,1012.2,469.15,1013.4,334.14,1014.5,282.13,1015.7,234.12,1016.8,212.11,1017.9,192.10,1018.10,182.9,1019.11,166.8,1020.12,144.7,1021.13,125.6,1022.14,109.5,1023.15,96.4,1024.16,92.3,1025.17,89.2,1026.18,87.1,1027.19,1.0,1028.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.48 1049:4:20:[802.19,76.0,714.18,1030.2,649.17,1031.3,542.16,1032.4,469.15,1033.5,334.14,1034.6,282.13,1035.7,234.12,1036.8,212.11,1037.10,192.10,1038.11,182.9,1039.12,166.8,1040.13,144.7,1041.14,125.6,1042.16,109.5,1043.18,96.4,1044.19,92.3,1045.20,89.2,1046.21,87.1,1047.22,1.0,1048.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ->
% 0.38/0.48 1069:4:20:[802.19,77.0,714.18,1050.1,649.17,1051.2,542.16,1052.3,469.15,1053.4,334.14,1054.5,282.13,1055.6,234.12,1056.7,212.11,1057.8,192.10,1058.9,182.9,1059.10,166.8,1060.11,144.7,1061.12,125.6,1062.13,109.5,1063.14,96.4,1064.15,92.3,1065.16,89.2,1066.18,87.1,1067.19,1.0,1068.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.38/0.48 1089:4:20:[802.19,78.0,714.18,1070.1,649.17,1071.2,542.16,1072.3,469.15,1073.4,334.14,1074.6,282.13,1075.7,234.12,1076.8,212.11,1077.9,192.10,1078.10,182.9,1079.11,166.8,1080.12,144.7,1081.14,125.6,1082.15,109.5,1083.16,96.4,1084.18,92.3,1085.19,89.2,1086.20,87.1,1087.21,1.0,1088.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.38/0.48 1109:4:20:[802.19,79.0,714.18,1090.1,649.17,1091.2,542.16,1092.3,469.15,1093.4,334.14,1094.5,282.13,1095.6,234.12,1096.7,212.11,1097.8,192.10,1098.9,182.9,1099.10,166.8,1100.11,144.7,1101.12,125.6,1102.13,109.5,1103.14,96.4,1104.15,92.3,1105.16,89.2,1106.17,87.1,1107.18,1.0,1108.19]: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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.38/0.48 1129:4:20:[802.19,80.0,714.18,1110.1,649.17,1111.2,542.16,1112.3,469.15,1113.4,334.14,1114.5,282.13,1115.6,234.12,1116.7,212.11,1117.8,192.10,1118.9,182.9,1119.11,166.8,1120.12,144.7,1121.13,125.6,1122.14,109.5,1123.15,96.4,1124.16,92.3,1125.17,89.2,1126.18,87.1,1127.19,1.0,1128.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> 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),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.48 1149:4:20:[802.19,81.0,714.18,1130.2,649.17,1131.3,542.16,1132.4,469.15,1133.5,334.14,1134.6,282.13,1135.7,234.12,1136.8,212.11,1137.9,192.10,1138.10,182.9,1139.11,166.8,1140.12,144.7,1141.13,125.6,1142.14,109.5,1143.15,96.4,1144.16,92.3,1145.17,89.2,1146.19,87.1,1147.20,1.0,1148.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv19_2r1r1(x0,x1) -> ssPv7_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)
% 0.38/0.48 1169:4:20:[802.19,82.0,714.18,1150.3,649.17,1151.4,542.16,1152.5,469.15,1153.6,334.14,1154.7,282.13,1155.8,234.12,1156.9,212.11,1157.10,192.10,1158.11,182.9,1159.12,166.8,1160.13,144.7,1161.14,125.6,1162.15,109.5,1163.17,96.4,1164.18,92.3,1165.19,89.2,1166.20,87.1,1167.21,1.0,1168.22]: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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.48 1189:4:20:[802.19,83.0,714.18,1170.1,649.17,1171.2,542.16,1172.3,469.15,1173.5,334.14,1174.6,282.13,1175.7,234.12,1176.8,212.11,1177.9,192.10,1178.11,182.9,1179.12,166.8,1180.13,144.7,1181.14,125.6,1182.15,109.5,1183.16,96.4,1184.17,92.3,1185.18,89.2,1186.19,87.1,1187.20,1.0,1188.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> 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)
% 0.38/0.48 1209:4:20:[802.19,84.1,714.18,1190.3,649.17,1191.4,542.16,1192.5,469.15,1193.6,334.14,1194.8,282.13,1195.9,234.12,1196.10,212.11,1197.11,192.10,1198.12,182.9,1199.13,166.8,1200.14,144.7,1201.15,125.6,1202.16,109.5,1203.17,96.4,1204.18,92.3,1205.19,89.2,1206.20,87.1,1207.21,1.0,1208.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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.38/0.48 1229:4:20:[802.19,85.0,714.18,1210.1,649.17,1211.2,542.16,1212.4,469.15,1213.5,334.14,1214.7,282.13,1215.8,234.12,1216.9,212.11,1217.10,192.10,1218.12,182.9,1219.13,166.8,1220.14,144.7,1221.15,125.6,1222.16,109.5,1223.17,96.4,1224.18,92.3,1225.19,89.2,1226.20,87.1,1227.21,1.0,1228.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),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) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.38/0.48 1249:4:20:[802.19,86.0,714.18,1230.2,649.17,1231.3,542.16,1232.4,469.15,1233.5,334.14,1234.6,282.13,1235.8,234.12,1236.9,212.11,1237.10,192.10,1238.11,182.9,1239.12,166.8,1240.13,144.7,1241.14,125.6,1242.15,109.5,1243.16,96.4,1244.17,92.3,1245.18,89.2,1246.19,87.1,1247.20,1.0,1248.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),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.48
% 0.38/0.48 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) ssPv20_1r1(x0) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv19_2r1r1(x0,x1) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) 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) ssPv18_3r1r1r1(x0,x1,x2) ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) 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) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) 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) ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) 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) ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) 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.38/0.48
% 0.38/0.48 === Starting SPASS-SCL-FOL A Little Less Naive, considering 28 atoms initially, heuristics mode: resolution_3 ===
% 0.38/0.48
% 0.38/0.48 === Conflict found: 173:4:7:[125.6,18.0,109.5,167.1,96.4,168.2,92.3,169.3,89.2,170.4,87.1,171.6,1.0,172.7]:TopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27}
% 0.38/0.48 === Backtracking. Learning clause 1250:3:6:[173.3,137.1]:TopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 === Conflict found: 400:4:13:[234.12,37.0,212.11,388.1,192.10,389.2,182.9,390.3,166.8,391.4,144.7,392.5,125.6,393.6,109.5,394.8,96.4,395.9,92.3,396.10,89.2,397.11,87.1,398.12,1.0,399.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc23}
% 0.38/0.48 === Backtracking. Learning clause 1251:5:11:[400.3,258.1,346.2]:TopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.48 === Conflict found: 413:4:13:[234.12,38.0,212.11,401.2,192.10,402.3,182.9,403.4,166.8,404.5,144.7,405.6,125.6,406.8,109.5,407.9,96.4,408.10,92.3,409.11,89.2,410.12,87.1,411.13,1.0,412.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),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.38/0.48 === Backtracking. Learning clause 1252:4:8:[413.1,246.1,1251.2]:TopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.48 === Conflict found: 512:4:13:[234.12,45.1,212.11,500.3,192.10,501.4,182.9,502.6,166.8,503.7,144.7,504.8,125.6,505.9,109.5,506.10,96.4,507.11,92.3,508.12,89.2,509.13,87.1,510.14,1.0,511.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> 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 -> skc22}
% 0.38/0.48 === Backtracking. Learning clause 1253:3:12:[512.2,246.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.38/0.48 === Conflict found: 400:4:13:[234.12,37.0,212.11,388.1,192.10,389.2,182.9,390.3,166.8,391.4,144.7,392.5,125.6,393.6,109.5,394.8,96.4,395.9,92.3,396.10,89.2,397.11,87.1,398.12,1.0,399.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc23}
% 0.38/0.48 === Backtracking. Learning clause 1254:4:9:[400.3,258.1,1253.1]:TopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.38/0.48 === Conflict found: 572:4:15:[334.14,49.0,282.13,558.1,234.12,559.2,212.11,560.3,192.10,561.4,182.9,562.5,166.8,563.6,144.7,564.8,125.6,565.9,109.5,566.10,96.4,567.11,92.3,568.12,89.2,569.13,87.1,570.14,1.0,571.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv18_3r1r1r1(x0,x1,x2) {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.38/0.48 === Backtracking. Learning clause 1255:3:10:[572.2,374.1]:TopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.48 === Conflict found: 1049:4:20:[802.19,76.0,714.18,1030.2,649.17,1031.3,542.16,1032.4,469.15,1033.5,334.14,1034.6,282.13,1035.7,234.12,1036.8,212.11,1037.10,192.10,1038.11,182.9,1039.12,166.8,1040.13,144.7,1041.14,125.6,1042.16,109.5,1043.18,96.4,1044.19,92.3,1045.20,89.2,1046.21,87.1,1047.22,1.0,1048.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> {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, x19 -> skc30}
% 0.38/0.48 === Backtracking. Learning clause 1256:5:11:[1049.1,991.4]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) ->
% 0.38/0.48 === Conflict found: 413:4:13:[234.12,38.0,212.11,401.2,192.10,402.3,182.9,403.4,166.8,404.5,144.7,405.6,125.6,406.8,109.5,407.9,96.4,408.10,92.3,409.11,89.2,410.12,87.1,411.13,1.0,412.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),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.38/0.48 === Backtracking. Learning clause 1257:5:7:[413.1,246.1,1256.1]:TopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.48 === Conflict found: 602:4:15:[334.14,51.0,282.13,588.1,234.12,589.3,212.11,590.4,192.10,591.5,182.9,592.6,166.8,593.7,144.7,594.8,125.6,595.9,109.5,596.10,96.4,597.11,92.3,598.12,89.2,599.13,87.1,600.15,1.0,601.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv20_1r1(x0) -> 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 -> skc19}
% 0.38/0.48 === Backtracking. Learning clause 1258:3:12:[602.3,374.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv20_1r1(x0) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.38/0.48 === Conflict found: 400:4:13:[234.12,37.0,212.11,388.1,192.10,389.2,182.9,390.3,166.8,391.4,144.7,392.5,125.6,393.6,109.5,394.8,96.4,395.9,92.3,396.10,89.2,397.11,87.1,398.12,1.0,399.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc23}
% 0.38/0.48 === Backtracking. Learning clause 1259:3:4:[400.3,258.1,1258.1,1257.2,1250.2,100.1]:TopTopTopTop: ssPv20_1r1(x0) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv19_2r1r1(x0,x1)
% 0.38/0.48 === Conflict found: 680:4:16:[469.15,56.0,334.14,665.2,282.13,666.3,234.12,667.4,212.11,668.5,192.10,669.6,182.9,670.8,166.8,671.10,144.7,672.11,125.6,673.12,109.5,674.13,96.4,675.14,92.3,676.15,89.2,677.16,87.1,678.17,1.0,679.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> 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 -> skc30, x15 -> skc16}
% 0.38/0.48 === Backtracking. Learning clause 1260:3:9:[680.1,484.1]:TopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv19_2r1r1(x0,x1)
% 0.38/0.48 === Clause set with instances from active satisfied. Growing active. New size: 31
% 0.38/0.48 === Restarting.
% 0.38/0.48 === Conflict found: 1250:3:6:[173.3,137.1]:TopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29}
% 0.38/0.48 === Backtracking. Learning clause 1261:2:2:[1250.2,119.1]:TopTop: ssPv20_1r1(x0) -> ssPv19_2r1r1(x0,x1)
% 0.38/0.48 === Conflict found: 426:4:13:[234.12,39.1,212.11,414.3,192.10,415.4,182.9,416.5,166.8,417.6,144.7,418.8,125.6,419.9,109.5,420.10,96.4,421.11,92.3,422.12,89.2,423.14,87.1,424.15,1.0,425.16]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),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.38/0.48 === Backtracking. Learning clause 1262:3:12:[426.2,246.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) ->
% 0.38/0.48 === Conflict found: 400:4:13:[234.12,37.0,212.11,388.1,192.10,389.2,182.9,390.3,166.8,391.4,144.7,392.5,125.6,393.6,109.5,394.8,96.4,395.9,92.3,396.10,89.2,397.11,87.1,398.12,1.0,399.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc23}
% 0.38/0.48 === Backtracking. Learning clause 1263:4:7:[400.3,258.1,1262.1]:TopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.48 === Conflict found: 1263:4:7:[400.3,258.1,1262.1]:TopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc26}
% 0.38/0.48 === Backtracking. Learning clause 1264:2:4:[1263.2,131.1,100.1]:TopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.48 === Conflict found: 1209:4:20:[802.19,84.1,714.18,1190.3,649.17,1191.4,542.16,1192.5,469.15,1193.6,334.14,1194.8,282.13,1195.9,234.12,1196.10,212.11,1197.11,192.10,1198.12,182.9,1199.13,166.8,1200.14,144.7,1201.15,125.6,1202.16,109.5,1203.17,96.4,1204.18,92.3,1205.19,89.2,1206.20,87.1,1207.21,1.0,1208.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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, x18 -> skc30, x19 -> skc30}
% 0.38/0.48 === Backtracking. Learning clause 1265:8:15:[1209.2,991.4,1029.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.48 === Conflict found: 1265:8:15:[1209.2,991.4,1029.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),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 -> skc18}
% 0.38/0.49 === Backtracking. Learning clause 1266:7:14:[1265.5,360.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.49 === Conflict found: 1266:7:14:[1265.5,360.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),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 -> skc20}
% 0.38/0.49 === Backtracking. Learning clause 1267:6:13:[1266.1,295.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.49 === Conflict found: 1267:6:13:[1266.1,295.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),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.38/0.49 === Backtracking. Learning clause 1269:4:7:[1250.2,1268.3,1267.4,246.1,1262.1]:TopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.49 === Conflict found: 1269:4:7:[1250.2,1268.3,1267.4,246.1,1262.1]:TopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),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 -> skc26}
% 0.38/0.49 === Backtracking. Learning clause 1270:3:6:[1269.3,131.1]:TopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.49 === Conflict found: 1270:3:6:[1269.3,131.1]:TopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29}
% 0.38/0.49 === Backtracking. Learning clause 1271:1:1:[1270.3,119.1,100.1]:Top: ssPv20_1r1(x0) ->
% 0.38/0.49 === Conflict found: 440:4:14:[282.13,40.0,234.12,427.1,212.11,428.2,192.10,429.3,182.9,430.4,166.8,431.5,144.7,432.6,125.6,433.7,109.5,434.8,96.4,435.9,92.3,436.10,89.2,437.11,87.1,438.12,1.0,439.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3),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 -> skc21}
% 0.38/0.49 === Backtracking. Learning clause 1273:2:6:[1271.0,1272.2,440.1,308.1]:TopTopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.49 === Conflict found: 1273:2:6:[1271.0,1272.2,440.1,308.1]:TopTopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29}
% 0.38/0.49 === Backtracking. Learning clause 1274:1:4:[1273.1,119.1]:TopTopTopTop: -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.49 === Conflict found: 617:4:15:[334.14,52.1,282.13,603.3,234.12,604.4,212.11,605.5,192.10,606.6,182.9,607.7,166.8,608.8,144.7,609.9,125.6,610.10,109.5,611.11,96.4,612.13,92.3,613.14,89.2,614.15,87.1,615.16,1.0,616.17]: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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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 -> skc18}
% 0.38/0.49 === Backtracking. Learning clause 1277:1:14:[1274.0,1275.1,1271.0,1276.2,617.2,360.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ->
% 0.38/0.49 === Conflict found: 1277:1:14:[1274.0,1275.1,1271.0,1276.2,617.2,360.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> {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.38/0.49
% 0.38/0.49 SZS status Unsatisfiable
% 0.38/0.49
% 0.38/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.49
% 0.38/0.49 SPASS-SCL-FOL Statistics:
% 0.38/0.49 Number of learned clauses: 24
% 0.38/0.49 Number of propagations: 203
% 0.38/0.49 Number of decisions: 101
% 0.38/0.49 Number of resolutions: 38
% 0.38/0.49 Number of condensations: 0
% 0.38/0.49 Number of sub resolutions: 1167
% 0.38/0.49 Number of input literals (deduplicated): 56
% 0.38/0.49 Number of grows: 1
% 0.38/0.49 Number of considered ground atoms: 31
% 0.38/0.49
% 0.38/0.49 Needed: 0:00:00.07
% 0.38/0.49
%------------------------------------------------------------------------------