%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SYN867-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 : n020.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.40s 0.63s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : SYN867-1 : TPTP v9.2.1. Released v2.5.0. % 0.09/0.15 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.37 % Computer : n020.cluster.edu % 0.20/0.37 % Model : x86_64 x86_64 % 0.20/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.20/0.37 % Memory : 8042.1875MB % 0.20/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.20/0.37 % CPULimit : 300 % 0.20/0.37 % WCLimit : 300 % 0.20/0.37 % DateTime : Thu May 7 13:50:36 EDT 2026 % 0.20/0.38 % CPUTime : % 0.20/0.38 SPASS-SCL-FOL version: % 0.27/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.40/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.62 Execution lmodel_grow ended with status: satisfiable % 0.40/0.62 Used heuristic: lmodel_grow % 0.40/0.62 % 0.40/0.62 Input Clauses: % 0.40/0.62 % 0.40/0.62 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv24_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv23_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv22_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv21_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv26_3r1r1r1 ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_10r1r1r1r1r1r1r1r1r1r1 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 % 0.40/0.62 Fol Constants: skc38 skc39 skc36 skc37 skc34 skc35 skc32 skc33 skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 % 0.40/0.62 Fol Functions: % 0.40/0.62 Problem Properties: % 0.40/0.62 This is a Bernays Schoenfinkel problem. % 0.40/0.62 % 0.40/0.62 After reduction: Problem Properties: % 0.40/0.62 This is a Bernays Schoenfinkel problem. % 0.40/0.62 % 0.40/0.62 % 0.40/0.62 Reduced Input Clauses: % 0.40/0.62 59:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0) % 0.40/0.62 61:1:2:[59.1,3.0,1.0,60.1]:TopTop: -> ssNder1_2r1r1(x0,x1) % 0.40/0.62 64:1:3:[61.2,4.0,59.1,62.1,1.0,63.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2) % 0.40/0.62 68:1:4:[64.3,5.0,61.2,65.1,59.1,66.2,1.0,67.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3) % 0.40/0.62 72:1:4:[64.3,6.0,61.2,69.1,59.1,70.2,1.0,71.3]:TopTopTopTop: -> ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc38) % 0.40/0.62 76:1:4:[64.3,7.1,61.2,73.2,59.1,74.3,1.0,75.4]:TopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc39) -> % 0.40/0.62 81:1:5:[68.4,8.0,64.3,77.1,61.2,78.2,59.1,79.3,1.0,80.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) % 0.40/0.62 86:1:5:[68.4,9.0,64.3,82.1,61.2,83.2,59.1,84.3,1.0,85.4]:TopTopTopTopTop: -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc36) % 0.40/0.62 91:1:5:[68.4,10.1,64.3,87.2,61.2,88.3,59.1,89.4,1.0,90.5]:TopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc37) -> % 0.40/0.63 97:1:6:[81.5,11.0,68.4,92.1,64.3,93.2,61.2,94.3,59.1,95.4,1.0,96.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) % 0.40/0.63 103:1:6:[81.5,12.0,68.4,98.1,64.3,99.2,61.2,100.3,59.1,101.4,1.0,102.5]:TopTopTopTopTopTop: -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc34) % 0.40/0.63 109:1:6:[81.5,13.1,68.4,104.2,64.3,105.3,61.2,106.4,59.1,107.5,1.0,108.6]:TopTopTopTopTopTop: ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc35) -> % 0.40/0.63 116:1:7:[97.6,14.0,81.5,110.1,68.4,111.2,64.3,112.3,61.2,113.4,59.1,114.5,1.0,115.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) % 0.40/0.63 123:1:7:[97.6,15.0,81.5,117.1,68.4,118.2,64.3,119.3,61.2,120.4,59.1,121.5,1.0,122.6]:TopTopTopTopTopTopTop: -> ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc32) % 0.40/0.63 130:1:7:[97.6,16.1,81.5,124.2,68.4,125.3,64.3,126.4,61.2,127.5,59.1,128.6,1.0,129.7]:TopTopTopTopTopTopTop: ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc33) -> % 0.40/0.63 138:1:8:[116.7,17.0,97.6,131.1,81.5,132.2,68.4,133.3,64.3,134.4,61.2,135.5,59.1,136.6,1.0,137.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) % 0.40/0.63 147:1:9:[138.8,18.0,116.7,139.1,97.6,140.2,81.5,141.3,68.4,142.4,64.3,143.5,61.2,144.6,59.1,145.7,1.0,146.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) % 0.40/0.63 157:1:10:[147.9,19.0,138.8,148.1,116.7,149.2,97.6,150.3,81.5,151.4,68.4,152.5,64.3,153.6,61.2,154.7,59.1,155.8,1.0,156.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) % 0.40/0.63 168:1:11:[157.10,20.0,147.9,158.1,138.8,159.2,116.7,160.3,97.6,161.4,81.5,162.5,68.4,163.6,64.3,164.7,61.2,165.8,59.1,166.9,1.0,167.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) % 0.40/0.63 180:1:12:[168.11,21.0,157.10,169.1,147.9,170.2,138.8,171.3,116.7,172.4,97.6,173.5,81.5,174.6,68.4,175.7,64.3,176.8,61.2,177.9,59.1,178.10,1.0,179.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) % 0.40/0.63 192:1:12:[168.11,22.0,157.10,181.1,147.9,182.2,138.8,183.3,116.7,184.4,97.6,185.5,81.5,186.6,68.4,187.7,64.3,188.8,61.2,189.9,59.1,190.10,1.0,191.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc30) % 0.40/0.63 204:1:12:[168.11,23.1,157.10,193.2,147.9,194.3,138.8,195.4,116.7,196.5,97.6,197.6,81.5,198.7,68.4,199.8,64.3,200.9,61.2,201.10,59.1,202.11,1.0,203.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc31) -> % 0.40/0.63 217:1:13:[180.12,24.0,168.11,205.1,157.10,206.2,147.9,207.3,138.8,208.4,116.7,209.5,97.6,210.6,81.5,211.7,68.4,212.8,64.3,213.9,61.2,214.10,59.1,215.11,1.0,216.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) % 0.40/0.63 230:1:13:[180.12,25.0,168.11,218.1,157.10,219.2,147.9,220.3,138.8,221.4,116.7,222.5,97.6,223.6,81.5,224.7,68.4,225.8,64.3,226.9,61.2,227.10,59.1,228.11,1.0,229.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc28) % 0.40/0.63 243:1:13:[180.12,26.1,168.11,231.2,157.10,232.3,147.9,233.4,138.8,234.5,116.7,235.6,97.6,236.7,81.5,237.8,68.4,238.9,64.3,239.10,61.2,240.11,59.1,241.12,1.0,242.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc29) -> % 0.40/0.63 257:1:14:[217.13,27.0,180.12,244.1,168.11,245.2,157.10,246.3,147.9,247.4,138.8,248.5,116.7,249.6,97.6,250.7,81.5,251.8,68.4,252.9,64.3,253.10,61.2,254.11,59.1,255.12,1.0,256.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) % 0.40/0.63 271:1:14:[217.13,28.0,180.12,258.1,168.11,259.2,157.10,260.3,147.9,261.4,138.8,262.5,116.7,263.6,97.6,264.7,81.5,265.8,68.4,266.9,64.3,267.10,61.2,268.11,59.1,269.12,1.0,270.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc26) % 0.40/0.63 285:1:14:[217.13,29.1,180.12,272.2,168.11,273.3,157.10,274.4,147.9,275.5,138.8,276.6,116.7,277.7,97.6,278.8,81.5,279.9,68.4,280.10,64.3,281.11,61.2,282.12,59.1,283.13,1.0,284.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc27) -> % 0.40/0.63 300:1:15:[257.14,30.0,217.13,286.1,180.12,287.2,168.11,288.3,157.10,289.4,147.9,290.5,138.8,291.6,116.7,292.7,97.6,293.8,81.5,294.9,68.4,295.10,64.3,296.11,61.2,297.12,59.1,298.13,1.0,299.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) % 0.40/0.63 315:1:15:[257.14,31.0,217.13,301.1,180.12,302.2,168.11,303.3,157.10,304.4,147.9,305.5,138.8,306.6,116.7,307.7,97.6,308.8,81.5,309.9,68.4,310.10,64.3,311.11,61.2,312.12,59.1,313.13,1.0,314.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc24) % 0.40/0.63 330:1:15:[257.14,32.1,217.13,316.2,180.12,317.3,168.11,318.4,157.10,319.5,147.9,320.6,138.8,321.7,116.7,322.8,97.6,323.9,81.5,324.10,68.4,325.11,64.3,326.12,61.2,327.13,59.1,328.14,1.0,329.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc25) -> % 0.40/0.63 346:1:16:[300.15,33.0,257.14,331.1,217.13,332.2,180.12,333.3,168.11,334.4,157.10,335.5,147.9,336.6,138.8,337.7,116.7,338.8,97.6,339.9,81.5,340.10,68.4,341.11,64.3,342.12,61.2,343.13,59.1,344.14,1.0,345.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) % 0.40/0.63 363:1:17:[346.16,34.0,300.15,347.1,257.14,348.2,217.13,349.3,180.12,350.4,168.11,351.5,157.10,352.6,147.9,353.7,138.8,354.8,116.7,355.9,97.6,356.10,81.5,357.11,68.4,358.12,64.3,359.13,61.2,360.14,59.1,361.15,1.0,362.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) % 0.40/0.63 381:1:18:[363.17,35.0,346.16,364.1,300.15,365.2,257.14,366.3,217.13,367.4,180.12,368.5,168.11,369.6,157.10,370.7,147.9,371.8,138.8,372.9,116.7,373.10,97.6,374.11,81.5,375.12,68.4,376.13,64.3,377.14,61.2,378.15,59.1,379.16,1.0,380.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) % 0.40/0.63 400:1:19:[381.18,36.0,363.17,382.1,346.16,383.2,300.15,384.3,257.14,385.4,217.13,386.5,180.12,387.6,168.11,388.7,157.10,389.8,147.9,390.9,138.8,391.10,116.7,392.11,97.6,393.12,81.5,394.13,68.4,395.14,64.3,396.15,61.2,397.16,59.1,398.17,1.0,399.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) % 0.40/0.63 418:4:18:[363.17,37.0,346.16,401.1,300.15,402.3,257.14,403.4,217.13,404.6,180.12,405.7,168.11,406.8,157.10,407.9,147.9,408.10,138.8,409.11,116.7,410.12,97.6,411.13,81.5,412.14,68.4,413.15,64.3,414.16,61.2,415.17,59.1,416.18,1.0,417.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv26_3r1r1r1(x0,x1,x2) % 0.40/0.63 438:1:20:[400.19,38.0,381.18,419.1,363.17,420.2,346.16,421.3,300.15,422.4,257.14,423.5,217.13,424.6,180.12,425.7,168.11,426.8,157.10,427.9,147.9,428.10,138.8,429.11,116.7,430.12,97.6,431.13,81.5,432.14,68.4,433.15,64.3,434.16,61.2,435.17,59.1,436.18,1.0,437.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.40/0.63 458:1:20:[400.19,39.0,381.18,439.1,363.17,440.2,346.16,441.3,300.15,442.4,257.14,443.5,217.13,444.6,180.12,445.7,168.11,446.8,157.10,447.9,147.9,448.10,138.8,449.11,116.7,450.12,97.6,451.13,81.5,452.14,68.4,453.15,64.3,454.16,61.2,455.17,59.1,456.18,1.0,457.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,skc22) % 0.40/0.63 478:1:20:[400.19,40.1,381.18,459.2,363.17,460.3,346.16,461.4,300.15,462.5,257.14,463.6,217.13,464.7,180.12,465.8,168.11,466.9,157.10,467.10,147.9,468.11,138.8,469.12,116.7,470.13,97.6,471.14,81.5,472.15,68.4,473.16,64.3,474.17,61.2,475.18,59.1,476.19,1.0,477.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,skc23) -> % 0.40/0.63 497:4:19:[381.18,41.0,363.17,479.2,346.16,480.3,300.15,481.4,257.14,482.6,217.13,483.7,180.12,484.8,168.11,485.9,157.10,486.10,147.9,487.11,138.8,488.12,116.7,489.13,97.6,490.14,81.5,491.15,68.4,492.16,64.3,493.17,61.2,494.18,59.1,495.19,1.0,496.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),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),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) % 0.40/0.63 516:4:19:[381.18,42.0,363.17,498.2,346.16,499.4,300.15,500.5,257.14,501.6,217.13,502.7,180.12,503.8,168.11,504.9,157.10,505.10,147.9,506.11,138.8,507.12,116.7,508.13,97.6,509.14,81.5,510.15,68.4,511.16,64.3,512.17,61.2,513.18,59.1,514.19,1.0,515.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) % 0.40/0.63 537:1:21:[438.20,43.0,400.19,517.1,381.18,518.2,363.17,519.3,346.16,520.4,300.15,521.5,257.14,522.6,217.13,523.7,180.12,524.8,168.11,525.9,157.10,526.10,147.9,527.11,138.8,528.12,116.7,529.13,97.6,530.14,81.5,531.15,68.4,532.16,64.3,533.17,61.2,534.18,59.1,535.19,1.0,536.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.40/0.63 559:1:22:[537.21,44.0,438.20,538.1,400.19,539.2,381.18,540.3,363.17,541.4,346.16,542.5,300.15,543.6,257.14,544.7,217.13,545.8,180.12,546.9,168.11,547.10,157.10,548.11,147.9,549.12,138.8,550.13,116.7,551.14,97.6,552.15,81.5,553.16,68.4,554.17,64.3,555.18,61.2,556.19,59.1,557.20,1.0,558.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.40/0.63 582:1:23:[559.22,45.0,537.21,560.1,438.20,561.2,400.19,562.3,381.18,563.4,363.17,564.5,346.16,565.6,300.15,566.7,257.14,567.8,217.13,568.9,180.12,569.10,168.11,570.11,157.10,571.12,147.9,572.13,138.8,573.14,116.7,574.15,97.6,575.16,81.5,576.17,68.4,577.18,64.3,578.19,61.2,579.20,59.1,580.21,1.0,581.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.40/0.63 605:1:23:[559.22,46.0,537.21,583.1,438.20,584.2,400.19,585.3,381.18,586.4,363.17,587.5,346.16,588.6,300.15,589.7,257.14,590.8,217.13,591.9,180.12,592.10,168.11,593.11,157.10,594.12,147.9,595.13,138.8,596.14,116.7,597.15,97.6,598.16,81.5,599.17,68.4,600.18,64.3,601.19,61.2,602.20,59.1,603.21,1.0,604.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,skc20) % 0.40/0.63 628:1:23:[559.22,47.1,537.21,606.2,438.20,607.3,400.19,608.4,381.18,609.5,363.17,610.6,346.16,611.7,300.15,612.8,257.14,613.9,217.13,614.10,180.12,615.11,168.11,616.12,157.10,617.13,147.9,618.14,138.8,619.15,116.7,620.16,97.6,621.17,81.5,622.18,68.4,623.19,64.3,624.20,61.2,625.21,59.1,626.22,1.0,627.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,skc21) -> % 0.40/0.63 652:1:24:[582.23,48.0,559.22,629.1,537.21,630.2,438.20,631.3,400.19,632.4,381.18,633.5,363.17,634.6,346.16,635.7,300.15,636.8,257.14,637.9,217.13,638.10,180.12,639.11,168.11,640.12,157.10,641.13,147.9,642.14,138.8,643.15,116.7,644.16,97.6,645.17,81.5,646.18,68.4,647.19,64.3,648.20,61.2,649.21,59.1,650.22,1.0,651.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.40/0.63 677:1:25:[652.24,49.0,582.23,653.1,559.22,654.2,537.21,655.3,438.20,656.4,400.19,657.5,381.18,658.6,363.17,659.7,346.16,660.8,300.15,661.9,257.14,662.10,217.13,663.11,180.12,664.12,168.11,665.13,157.10,666.14,147.9,667.15,138.8,668.16,116.7,669.17,97.6,670.18,81.5,671.19,68.4,672.20,64.3,673.21,61.2,674.22,59.1,675.23,1.0,676.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.40/0.63 703:1:26:[677.25,50.0,652.24,678.1,582.23,679.2,559.22,680.3,537.21,681.4,438.20,682.5,400.19,683.6,381.18,684.7,363.17,685.8,346.16,686.9,300.15,687.10,257.14,688.11,217.13,689.12,180.12,690.13,168.11,691.14,157.10,692.15,147.9,693.16,138.8,694.17,116.7,695.18,97.6,696.19,81.5,697.20,68.4,698.21,64.3,699.22,61.2,700.23,59.1,701.24,1.0,702.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.40/0.63 728:4:25:[652.24,51.0,582.23,704.2,559.22,705.3,537.21,706.4,438.20,707.5,400.19,708.6,381.18,709.7,363.17,710.8,346.16,711.9,300.15,712.10,257.14,713.11,217.13,714.12,180.12,715.13,168.11,716.14,157.10,717.15,147.9,718.16,138.8,719.18,116.7,720.19,97.6,721.20,81.5,722.22,68.4,723.23,64.3,724.24,61.2,725.25,59.1,726.26,1.0,727.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) % 0.40/0.63 753:4:25:[652.24,52.0,582.23,729.2,559.22,730.3,537.21,731.4,438.20,732.5,400.19,733.6,381.18,734.7,363.17,735.8,346.16,736.9,300.15,737.10,257.14,738.11,217.13,739.12,180.12,740.13,168.11,741.14,157.10,742.15,147.9,743.16,138.8,744.17,116.7,745.18,97.6,746.20,81.5,747.21,68.4,748.22,64.3,749.23,61.2,750.24,59.1,751.25,1.0,752.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) % 0.40/0.63 780:1:27:[703.26,53.0,677.25,754.1,652.24,755.2,582.23,756.3,559.22,757.4,537.21,758.5,438.20,759.6,400.19,760.7,381.18,761.8,363.17,762.9,346.16,763.10,300.15,764.11,257.14,765.12,217.13,766.13,180.12,767.14,168.11,768.15,157.10,769.16,147.9,770.17,138.8,771.18,116.7,772.19,97.6,773.20,81.5,774.21,68.4,775.22,64.3,776.23,61.2,777.24,59.1,778.25,1.0,779.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) % 0.40/0.63 805:4:25:[652.24,54.1,582.23,781.2,559.22,782.3,537.21,783.4,438.20,784.5,400.19,785.6,381.18,786.7,363.17,787.8,346.16,788.9,300.15,789.10,257.14,790.12,217.13,791.13,180.12,792.14,168.11,793.15,157.10,794.16,147.9,795.17,138.8,796.18,116.7,797.19,97.6,798.20,81.5,799.21,68.4,800.22,64.3,801.23,61.2,802.24,59.1,803.25,1.0,804.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> 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),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) % 0.40/0.63 831:4:26:[677.25,55.0,652.24,806.2,582.23,807.3,559.22,808.4,537.21,809.5,438.20,810.6,400.19,811.7,381.18,812.8,363.17,813.9,346.16,814.10,300.15,815.11,257.14,816.12,217.13,817.13,180.12,818.14,168.11,819.15,157.10,820.16,147.9,821.17,138.8,822.18,116.7,823.19,97.6,824.20,81.5,825.21,68.4,826.22,64.3,827.23,61.2,828.24,59.1,829.25,1.0,830.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> 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),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) % 0.40/0.63 857:4:26:[677.25,56.0,652.24,832.1,582.23,833.2,559.22,834.3,537.21,835.4,438.20,836.5,400.19,837.6,381.18,838.7,363.17,839.8,346.16,840.9,300.15,841.10,257.14,842.12,217.13,843.13,180.12,844.14,168.11,845.15,157.10,846.16,147.9,847.17,138.8,848.18,116.7,849.19,97.6,850.20,81.5,851.21,68.4,852.22,64.3,853.23,61.2,854.24,59.1,855.25,1.0,856.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> 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),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),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) % 0.40/0.63 885:4:28:[780.27,57.0,703.26,858.2,677.25,859.3,652.24,860.4,582.23,861.5,559.22,862.6,537.21,863.8,438.20,864.9,400.19,865.10,381.18,866.11,363.17,867.12,346.16,868.13,300.15,869.14,257.14,870.15,217.13,871.16,180.12,872.17,168.11,873.18,157.10,874.19,147.9,875.20,138.8,876.21,116.7,877.22,97.6,878.24,81.5,879.25,68.4,880.26,64.3,881.27,61.2,882.28,59.1,883.29,1.0,884.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) % 0.40/0.63 913:4:28:[780.27,58.0,703.26,886.1,677.25,887.2,652.24,888.4,582.23,889.5,559.22,890.6,537.21,891.7,438.20,892.8,400.19,893.9,381.18,894.10,363.17,895.11,346.16,896.12,300.15,897.13,257.14,898.14,217.13,899.15,180.12,900.16,168.11,901.17,157.10,902.18,147.9,903.19,138.8,904.20,116.7,905.21,97.6,906.23,81.5,907.24,68.4,908.25,64.3,909.26,61.2,910.27,59.1,911.28,1.0,912.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) % 0.40/0.63 % 0.40/0.63 Most General Atoms: ssNder1_0 ssNder1_1r1(x0) ssNder1_2r1r1(x0,x1) ssNder1_3r1r1r1(x0,x1,x2) ssNder1_4r1r1r1r1(x0,x1,x2,x3) ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) 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) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv26_3r1r1r1(x0,x1,x2) ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) 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) ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) 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) ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) 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) 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) ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) % 0.40/0.63 % 0.40/0.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 66 atoms initially, heuristics mode: lmodel_grow === % 0.40/0.63 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 69 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 70 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 72 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 73 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 74 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 75 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 76 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 77 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 78 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 79 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 80 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 81 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 82 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 83 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 84 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 85 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 86 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 87 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 88 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 89 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 90 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 91 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 92 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 93 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 94 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 95 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 96 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 97 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 98 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 99 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 100 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 101 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 102 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 103 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 104 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 105 % 0.40/0.63 === Clause set with instances from active satisfied. Growing active. New size: 106 % 0.40/0.63 % 0.40/0.63 Linear Model Building succeeded. % 0.40/0.63 SZS status Satisfiable % 0.40/0.63 % 0.40/0.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.63 % 0.40/0.63 SPASS-SCL-FOL Statistics: % 0.40/0.63 Number of learned clauses: 0 % 0.40/0.63 Number of propagations: 87 % 0.40/0.63 Number of decisions: 19 % 0.40/0.63 Number of resolutions: 0 % 0.40/0.63 Number of condensations: 0 % 0.40/0.63 Number of sub resolutions: 855 % 0.40/0.63 Number of input literals (deduplicated): 66 % 0.40/0.63 Number of grows: 37 % 0.40/0.63 Number of considered ground atoms: 106 % 0.40/0.63 % 0.40/0.63 Needed: 0:00:00.03 % 0.40/0.63 %------------------------------------------------------------------------------