%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN868-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:40:20 PM UTC 2026
% Result : Satisfiable 0.36s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SYN868-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.08 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.27 % Computer : n024.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 08:50:12 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.36/0.44 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/0.44 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/0.44 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/0.44 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/0.44 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/0.44 Execution lmodel_grow ended with status: satisfiable
% 0.36/0.44 Used heuristic: lmodel_grow
% 0.36/0.44
% 0.36/0.44 Input Clauses:
% 0.36/0.44
% 0.36/0.44 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv24_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv22_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv21_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv18_11r1r1r1r1r1r1r1r1r1r1r1 ssPv26_3r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv28_1r1 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_10r1r1r1r1r1r1r1r1r1r1 ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv25_4r1r1r1r1 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 0.36/0.44 Fol Constants: skc34 skc35 skc32 skc33 skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19
% 0.36/0.44 Fol Functions:
% 0.36/0.44 Problem Properties:
% 0.36/0.44 This is a Bernays Schoenfinkel problem.
% 0.36/0.44
% 0.36/0.44 After reduction: Problem Properties:
% 0.36/0.44 This is a Bernays Schoenfinkel problem.
% 0.36/0.44
% 0.36/0.44
% 0.36/0.44 Reduced Input Clauses:
% 0.36/0.44 56:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 0.36/0.44 58:1:2:[56.1,3.0,1.0,57.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 0.36/0.44 61:1:3:[58.2,4.0,56.1,59.1,1.0,60.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 0.36/0.44 65:1:4:[61.3,5.0,58.2,62.1,56.1,63.2,1.0,64.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 0.36/0.44 69:1:4:[61.3,6.0,58.2,66.1,56.1,67.2,1.0,68.3]:TopTopTopTop: -> ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc34)
% 0.36/0.44 73:1:4:[61.3,7.1,58.2,70.2,56.1,71.3,1.0,72.4]:TopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc35) ->
% 0.36/0.44 78:1:5:[65.4,8.0,61.3,74.1,58.2,75.2,56.1,76.3,1.0,77.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.36/0.44 84:1:6:[78.5,9.0,65.4,79.1,61.3,80.2,58.2,81.3,56.1,82.4,1.0,83.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.36/0.44 90:1:6:[78.5,10.0,65.4,85.1,61.3,86.2,58.2,87.3,56.1,88.4,1.0,89.5]:TopTopTopTopTopTop: -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc32)
% 0.36/0.44 96:1:6:[78.5,11.1,65.4,91.2,61.3,92.3,58.2,93.4,56.1,94.5,1.0,95.6]:TopTopTopTopTopTop: ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc33) ->
% 0.36/0.44 103:1:7:[84.6,12.0,78.5,97.1,65.4,98.2,61.3,99.3,58.2,100.4,56.1,101.5,1.0,102.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.36/0.44 110:1:7:[84.6,13.0,78.5,104.1,65.4,105.2,61.3,106.3,58.2,107.4,56.1,108.5,1.0,109.6]:TopTopTopTopTopTopTop: -> ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc30)
% 0.36/0.44 117:1:7:[84.6,14.1,78.5,111.2,65.4,112.3,61.3,113.4,58.2,114.5,56.1,115.6,1.0,116.7]:TopTopTopTopTopTopTop: ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc31) ->
% 0.36/0.44 125:1:8:[103.7,15.0,84.6,118.1,78.5,119.2,65.4,120.3,61.3,121.4,58.2,122.5,56.1,123.6,1.0,124.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.36/0.44 134:1:9:[125.8,16.0,103.7,126.1,84.6,127.2,78.5,128.3,65.4,129.4,61.3,130.5,58.2,131.6,56.1,132.7,1.0,133.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.36/0.44 144:1:10:[134.9,17.0,125.8,135.1,103.7,136.2,84.6,137.3,78.5,138.4,65.4,139.5,61.3,140.6,58.2,141.7,56.1,142.8,1.0,143.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.36/0.44 155:1:11:[144.10,18.0,134.9,145.1,125.8,146.2,103.7,147.3,84.6,148.4,78.5,149.5,65.4,150.6,61.3,151.7,58.2,152.8,56.1,153.9,1.0,154.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.36/0.44 167:1:12:[155.11,19.0,144.10,156.1,134.9,157.2,125.8,158.3,103.7,159.4,84.6,160.5,78.5,161.6,65.4,162.7,61.3,163.8,58.2,164.9,56.1,165.10,1.0,166.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.36/0.44 179:1:12:[155.11,20.0,144.10,168.1,134.9,169.2,125.8,170.3,103.7,171.4,84.6,172.5,78.5,173.6,65.4,174.7,61.3,175.8,58.2,176.9,56.1,177.10,1.0,178.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc28)
% 0.36/0.44 191:1:12:[155.11,21.1,144.10,180.2,134.9,181.3,125.8,182.4,103.7,183.5,84.6,184.6,78.5,185.7,65.4,186.8,61.3,187.9,58.2,188.10,56.1,189.11,1.0,190.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc29) ->
% 0.36/0.44 202:4:11:[144.10,22.0,134.9,192.2,125.8,193.3,103.7,194.5,84.6,195.6,78.5,196.7,65.4,197.8,61.3,198.9,58.2,199.10,56.1,200.11,1.0,201.12]:TopTopTopTopTopTopTopTopTopTopTop: ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv26_3r1r1r1(x0,x1,x2)
% 0.36/0.44 215:1:13:[167.12,23.0,155.11,203.1,144.10,204.2,134.9,205.3,125.8,206.4,103.7,207.5,84.6,208.6,78.5,209.7,65.4,210.8,61.3,211.9,58.2,212.10,56.1,213.11,1.0,214.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.36/0.44 228:1:13:[167.12,24.0,155.11,216.1,144.10,217.2,134.9,218.3,125.8,219.4,103.7,220.5,84.6,221.6,78.5,222.7,65.4,223.8,61.3,224.9,58.2,225.10,56.1,226.11,1.0,227.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc26)
% 0.36/0.44 241:1:13:[167.12,25.1,155.11,229.2,144.10,230.3,134.9,231.4,125.8,232.5,103.7,233.6,84.6,234.7,78.5,235.8,65.4,236.9,61.3,237.10,58.2,238.11,56.1,239.12,1.0,240.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc27) ->
% 0.36/0.44 255:1:14:[215.13,26.0,167.12,242.1,155.11,243.2,144.10,244.3,134.9,245.4,125.8,246.5,103.7,247.6,84.6,248.7,78.5,249.8,65.4,250.9,61.3,251.10,58.2,252.11,56.1,253.12,1.0,254.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.36/0.44 269:1:14:[215.13,27.0,167.12,256.1,155.11,257.2,144.10,258.3,134.9,259.4,125.8,260.5,103.7,261.6,84.6,262.7,78.5,263.8,65.4,264.9,61.3,265.10,58.2,266.11,56.1,267.12,1.0,268.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc24)
% 0.36/0.44 283:1:14:[215.13,28.1,167.12,270.2,155.11,271.3,144.10,272.4,134.9,273.5,125.8,274.6,103.7,275.7,84.6,276.8,78.5,277.9,65.4,278.10,61.3,279.11,58.2,280.12,56.1,281.13,1.0,282.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc25) ->
% 0.36/0.44 298:1:15:[255.14,29.0,215.13,284.1,167.12,285.2,155.11,286.3,144.10,287.4,134.9,288.5,125.8,289.6,103.7,290.7,84.6,291.8,78.5,292.9,65.4,293.10,61.3,294.11,58.2,295.12,56.1,296.13,1.0,297.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.36/0.44 313:1:15:[255.14,30.0,215.13,299.1,167.12,300.2,155.11,301.3,144.10,302.4,134.9,303.5,125.8,304.6,103.7,305.7,84.6,306.8,78.5,307.9,65.4,308.10,61.3,309.11,58.2,310.12,56.1,311.13,1.0,312.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc22)
% 0.36/0.44 328:1:15:[255.14,31.1,215.13,314.2,167.12,315.3,155.11,316.4,144.10,317.5,134.9,318.6,125.8,319.7,103.7,320.8,84.6,321.9,78.5,322.10,65.4,323.11,61.3,324.12,58.2,325.13,56.1,326.14,1.0,327.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc23) ->
% 0.36/0.44 344:1:16:[298.15,32.0,255.14,329.1,215.13,330.2,167.12,331.3,155.11,332.4,144.10,333.5,134.9,334.6,125.8,335.7,103.7,336.8,84.6,337.9,78.5,338.10,65.4,339.11,61.3,340.12,58.2,341.13,56.1,342.14,1.0,343.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.36/0.44 361:1:17:[344.16,33.0,298.15,345.1,255.14,346.2,215.13,347.3,167.12,348.4,155.11,349.5,144.10,350.6,134.9,351.7,125.8,352.8,103.7,353.9,84.6,354.10,78.5,355.11,65.4,356.12,61.3,357.13,58.2,358.14,56.1,359.15,1.0,360.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.36/0.44 379:1:18:[361.17,34.0,344.16,362.1,298.15,363.2,255.14,364.3,215.13,365.4,167.12,366.5,155.11,367.6,144.10,368.7,134.9,369.8,125.8,370.9,103.7,371.10,84.6,372.11,78.5,373.12,65.4,374.13,61.3,375.14,58.2,376.15,56.1,377.16,1.0,378.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.36/0.44 396:4:17:[344.16,35.0,298.15,380.1,255.14,381.2,215.13,382.4,167.12,383.5,155.11,384.6,144.10,385.7,134.9,386.8,125.8,387.10,103.7,388.11,84.6,389.12,78.5,390.13,65.4,391.14,61.3,392.15,58.2,393.16,56.1,394.18,1.0,395.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv28_1r1(x0) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.36/0.44 415:1:19:[379.18,36.0,361.17,397.1,344.16,398.2,298.15,399.3,255.14,400.4,215.13,401.5,167.12,402.6,155.11,403.7,144.10,404.8,134.9,405.9,125.8,406.10,103.7,407.11,84.6,408.12,78.5,409.13,65.4,410.14,61.3,411.15,58.2,412.16,56.1,413.17,1.0,414.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.36/0.44 435:1:20:[415.19,37.0,379.18,416.1,361.17,417.2,344.16,418.3,298.15,419.4,255.14,420.5,215.13,421.6,167.12,422.7,155.11,423.8,144.10,424.9,134.9,425.10,125.8,426.11,103.7,427.12,84.6,428.13,78.5,429.14,65.4,430.15,61.3,431.16,58.2,432.17,56.1,433.18,1.0,434.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.36/0.44 456:1:21:[435.20,38.0,415.19,436.1,379.18,437.2,361.17,438.3,344.16,439.4,298.15,440.5,255.14,441.6,215.13,442.7,167.12,443.8,155.11,444.9,144.10,445.10,134.9,446.11,125.8,447.12,103.7,448.13,84.6,449.14,78.5,450.15,65.4,451.16,61.3,452.17,58.2,453.18,56.1,454.19,1.0,455.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 0.36/0.44 477:1:21:[435.20,39.0,415.19,457.1,379.18,458.2,361.17,459.3,344.16,460.4,298.15,461.5,255.14,462.6,215.13,463.7,167.12,464.8,155.11,465.9,144.10,466.10,134.9,467.11,125.8,468.12,103.7,469.13,84.6,470.14,78.5,471.15,65.4,472.16,61.3,473.17,58.2,474.18,56.1,475.19,1.0,476.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc20)
% 0.36/0.44 498:1:21:[435.20,40.1,415.19,478.2,379.18,479.3,361.17,480.4,344.16,481.5,298.15,482.6,255.14,483.7,215.13,484.8,167.12,485.9,155.11,486.10,144.10,487.11,134.9,488.12,125.8,489.13,103.7,490.14,84.6,491.15,78.5,492.16,65.4,493.17,61.3,494.18,58.2,495.19,56.1,496.20,1.0,497.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc21) ->
% 0.36/0.44 520:1:22:[456.21,41.0,435.20,499.1,415.19,500.2,379.18,501.3,361.17,502.4,344.16,503.5,298.15,504.6,255.14,505.7,215.13,506.8,167.12,507.9,155.11,508.10,144.10,509.11,134.9,510.12,125.8,511.13,103.7,512.14,84.6,513.15,78.5,514.16,65.4,515.17,61.3,516.18,58.2,517.19,56.1,518.20,1.0,519.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
% 0.36/0.44 543:1:23:[520.22,42.0,456.21,521.1,435.20,522.2,415.19,523.3,379.18,524.4,361.17,525.5,344.16,526.6,298.15,527.7,255.14,528.8,215.13,529.9,167.12,530.10,155.11,531.11,144.10,532.12,134.9,533.13,125.8,534.14,103.7,535.15,84.6,536.16,78.5,537.17,65.4,538.18,61.3,539.19,58.2,540.20,56.1,541.21,1.0,542.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22)
% 0.36/0.44 566:1:23:[520.22,43.0,456.21,544.1,435.20,545.2,415.19,546.3,379.18,547.4,361.17,548.5,344.16,549.6,298.15,550.7,255.14,551.8,215.13,552.9,167.12,553.10,155.11,554.11,144.10,555.12,134.9,556.13,125.8,557.14,103.7,558.15,84.6,559.16,78.5,560.17,65.4,561.18,61.3,562.19,58.2,563.20,56.1,564.21,1.0,565.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc18)
% 0.36/0.44 589:1:23:[520.22,44.1,456.21,567.2,435.20,568.3,415.19,569.4,379.18,570.5,361.17,571.6,344.16,572.7,298.15,573.8,255.14,574.9,215.13,575.10,167.12,576.11,155.11,577.12,144.10,578.13,134.9,579.14,125.8,580.15,103.7,581.16,84.6,582.17,78.5,583.18,65.4,584.19,61.3,585.20,58.2,586.21,56.1,587.22,1.0,588.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc19) ->
% 0.36/0.44 611:4:22:[456.21,45.0,435.20,590.3,415.19,591.4,379.18,592.5,361.17,593.6,344.16,594.7,298.15,595.8,255.14,596.9,215.13,597.10,167.12,598.11,155.11,599.12,144.10,600.13,134.9,601.14,125.8,602.15,103.7,603.16,84.6,604.17,78.5,605.18,65.4,606.19,61.3,607.20,58.2,608.21,56.1,609.22,1.0,610.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) -> ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv28_1r1(x0)
% 0.36/0.44 633:4:22:[456.21,46.0,435.20,612.2,415.19,613.3,379.18,614.4,361.17,615.5,344.16,616.6,298.15,617.7,255.14,618.9,215.13,619.10,167.12,620.11,155.11,621.12,144.10,622.14,134.9,623.15,125.8,624.16,103.7,625.17,84.6,626.18,78.5,627.19,65.4,628.20,61.3,629.22,58.2,630.23,56.1,631.24,1.0,632.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv26_3r1r1r1(x0,x1,x2) ->
% 0.36/0.44 657:1:24:[543.23,47.0,520.22,634.1,456.21,635.2,435.20,636.3,415.19,637.4,379.18,638.5,361.17,639.6,344.16,640.7,298.15,641.8,255.14,642.9,215.13,643.10,167.12,644.11,155.11,645.12,144.10,646.13,134.9,647.14,125.8,648.15,103.7,649.16,84.6,650.17,78.5,651.18,65.4,652.19,61.3,653.20,58.2,654.21,56.1,655.22,1.0,656.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23)
% 0.36/0.44 682:1:25:[657.24,48.0,543.23,658.1,520.22,659.2,456.21,660.3,435.20,661.4,415.19,662.5,379.18,663.6,361.17,664.7,344.16,665.8,298.15,666.9,255.14,667.10,215.13,668.11,167.12,669.12,155.11,670.13,144.10,671.14,134.9,672.15,125.8,673.16,103.7,674.17,84.6,675.18,78.5,676.19,65.4,677.20,61.3,678.21,58.2,679.22,56.1,680.23,1.0,681.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24)
% 0.36/0.44 708:1:26:[682.25,49.0,657.24,683.1,543.23,684.2,520.22,685.3,456.21,686.4,435.20,687.5,415.19,688.6,379.18,689.7,361.17,690.8,344.16,691.9,298.15,692.10,255.14,693.11,215.13,694.12,167.12,695.13,155.11,696.14,144.10,697.15,134.9,698.16,125.8,699.17,103.7,700.18,84.6,701.19,78.5,702.20,65.4,703.21,61.3,704.22,58.2,705.23,56.1,706.24,1.0,707.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25)
% 0.36/0.44 733:4:25:[657.24,50.0,543.23,709.2,520.22,710.3,456.21,711.4,435.20,712.5,415.19,713.6,379.18,714.7,361.17,715.8,344.16,716.9,298.15,717.10,255.14,718.12,215.13,719.13,167.12,720.14,155.11,721.15,144.10,722.16,134.9,723.17,125.8,724.18,103.7,725.20,84.6,726.21,78.5,727.22,65.4,728.24,61.3,729.25,58.2,730.26,56.1,731.27,1.0,732.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3) ->
% 0.36/0.44 759:4:26:[682.25,51.0,657.24,734.1,543.23,735.2,520.22,736.3,456.21,737.4,435.20,738.5,415.19,739.6,379.18,740.7,361.17,741.8,344.16,742.9,298.15,743.10,255.14,744.11,215.13,745.12,167.12,746.13,155.11,747.14,144.10,748.15,134.9,749.16,125.8,750.17,103.7,751.18,84.6,752.19,78.5,753.21,65.4,754.22,61.3,755.23,58.2,756.24,56.1,757.25,1.0,758.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.36/0.44 785:4:26:[682.25,52.0,657.24,760.1,543.23,761.2,520.22,762.3,456.21,763.4,435.20,764.5,415.19,765.6,379.18,766.7,361.17,767.8,344.16,768.10,298.15,769.12,255.14,770.13,215.13,771.14,167.12,772.15,155.11,773.16,144.10,774.17,134.9,775.18,125.8,776.19,103.7,777.20,84.6,778.21,78.5,779.22,65.4,780.23,61.3,781.24,58.2,782.25,56.1,783.26,1.0,784.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.36/0.44 811:4:26:[682.25,53.0,657.24,786.1,543.23,787.2,520.22,788.3,456.21,789.4,435.20,790.6,415.19,791.7,379.18,792.8,361.17,793.9,344.16,794.10,298.15,795.12,255.14,796.13,215.13,797.14,167.12,798.15,155.11,799.16,144.10,800.17,134.9,801.18,125.8,802.19,103.7,803.20,84.6,804.21,78.5,805.22,65.4,806.23,61.3,807.24,58.2,808.25,56.1,809.26,1.0,810.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.36/0.44 837:4:26:[682.25,54.0,657.24,812.1,543.23,813.2,520.22,814.4,456.21,815.5,435.20,816.6,415.19,817.7,379.18,818.8,361.17,819.9,344.16,820.10,298.15,821.11,255.14,822.12,215.13,823.13,167.12,824.15,155.11,825.16,144.10,826.17,134.9,827.18,125.8,828.19,103.7,829.20,84.6,830.21,78.5,831.22,65.4,832.23,61.3,833.24,58.2,834.25,56.1,835.26,1.0,836.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.36/0.44 864:4:27:[708.26,55.0,682.25,838.1,657.24,839.2,543.23,840.3,520.22,841.5,456.21,842.6,435.20,843.7,415.19,844.8,379.18,845.9,361.17,846.10,344.16,847.11,298.15,848.12,255.14,849.13,215.13,850.14,167.12,851.15,155.11,852.16,144.10,853.17,134.9,854.18,125.8,855.19,103.7,856.20,84.6,857.21,78.5,858.22,65.4,859.23,61.3,860.24,58.2,861.25,56.1,862.26,1.0,863.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.36/0.44
% 0.36/0.44 Most General Atoms: ssNder1_0 ssNder1_1r1(x0) ssNder1_2r1r1(x0,x1) ssNder1_3r1r1r1(x0,x1,x2) ssNder1_4r1r1r1r1(x0,x1,x2,x3) ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv26_3r1r1r1(x0,x1,x2) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv28_1r1(x0) ssPv12_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) ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ssPv25_4r1r1r1r1(x0,x1,x2,x3) ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23)
% 0.36/0.44
% 0.36/0.44 === Starting SPASS-SCL-FOL A Little Less Naive, considering 66 atoms initially, heuristics mode: lmodel_grow ===
% 0.36/0.44
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 72
% 0.36/0.44 === Conflict found: 633:4:22:[456.21,46.0,435.20,612.2,415.19,613.3,379.18,614.4,361.17,615.5,344.16,616.6,298.15,617.7,255.14,618.9,215.13,619.10,167.12,620.11,155.11,621.12,144.10,622.14,134.9,623.15,125.8,624.16,103.7,625.17,84.6,626.18,78.5,627.19,65.4,628.20,61.3,629.22,58.2,630.23,56.1,631.24,1.0,632.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv26_3r1r1r1(x0,x1,x2) -> {x0 -> skc34, x1 -> skc34, x2 -> skc34, x3 -> skc34, x4 -> skc34, x5 -> skc34, x6 -> skc34, x7 -> skc34, x8 -> skc34, x9 -> skc34, x10 -> skc34, x11 -> skc34, x12 -> skc34, x13 -> skc26, x14 -> skc34, x15 -> skc34, x16 -> skc34, x17 -> skc34, x18 -> skc34, x19 -> skc34, x20 -> skc34, x21 -> skc20}
% 0.36/0.44 === Backtracking. Learning clause 865:3:14:[633.1,477.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv26_3r1r1r1(x0,x1,x2) ->
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 79
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 86
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 93
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 97
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 101
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 105
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 109
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 113
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 117
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 125
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 129
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 133
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 137
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 141
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 145
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 149
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 153
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 157
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 161
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 165
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 169
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 173
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 177
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 181
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 185
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 189
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 193
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 197
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 201
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 205
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 208
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 210
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 211
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 212
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 213
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 214
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 215
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 216
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 217
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 218
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 219
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 220
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 221
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 222
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 223
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 224
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 225
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 226
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 227
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 228
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 229
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 230
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 231
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 232
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 233
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 234
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 235
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 236
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 237
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 238
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 239
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 240
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 241
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 242
% 0.36/0.44 === Clause set with instances from active satisfied. Growing active. New size: 243
% 0.36/0.44
% 0.36/0.44 Linear Model Building succeeded.
% 0.36/0.44 SZS status Satisfiable
% 0.36/0.44
% 0.36/0.44 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/0.44
% 0.36/0.44 SPASS-SCL-FOL Statistics:
% 0.36/0.44 Number of learned clauses: 1
% 0.36/0.44 Number of propagations: 229
% 0.36/0.44 Number of decisions: 31
% 0.36/0.44 Number of resolutions: 1
% 0.36/0.44 Number of condensations: 0
% 0.36/0.44 Number of sub resolutions: 809
% 0.36/0.44 Number of input literals (deduplicated): 66
% 0.36/0.44 Number of grows: 67
% 0.36/0.44 Number of considered ground atoms: 243
% 0.36/0.44
% 0.36/0.44 Needed: 0:00:00.04
% 0.36/0.44
%------------------------------------------------------------------------------