%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN869-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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:40:21 PM UTC 2026
% Result : Unsatisfiable 0.53s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14 % Problem : SYN869-1 : TPTP v9.2.1. Released v2.5.0.
% 0.11/0.15 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.36 % Computer : n007.cluster.edu
% 0.18/0.36 % Model : x86_64 x86_64
% 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.36 % Memory : 8042.1875MB
% 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.36 % CPULimit : 300
% 0.18/0.36 % WCLimit : 300
% 0.18/0.36 % DateTime : Thu May 7 13:49:24 EDT 2026
% 0.18/0.36 % CPUTime :
% 0.18/0.36 SPASS-SCL-FOL version:
% 0.18/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.53/0.69 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/0.69 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/0.69 Execution lmodel_grow ended with status: unsatisfiable
% 0.53/0.69 Used heuristic: lmodel_grow
% 0.53/0.69
% 0.53/0.69 Input Clauses:
% 0.53/0.69
% 0.53/0.69 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv16_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv15_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv14_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv13_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_2r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv20_1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv18_3r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_4r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 0.53/0.69 Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17
% 0.53/0.69 Fol Functions:
% 0.53/0.69 Problem Properties:
% 0.53/0.69 This is a Bernays Schoenfinkel problem.
% 0.53/0.69
% 0.53/0.69 After reduction: Problem Properties:
% 0.53/0.69 This is a Bernays Schoenfinkel problem.
% 0.53/0.69
% 0.53/0.69
% 0.53/0.69 Reduced Input Clauses:
% 0.53/0.69 57:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 0.53/0.69 59:1:2:[57.1,3.0,1.0,58.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 0.53/0.69 62:1:3:[59.2,4.0,57.1,60.1,1.0,61.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 0.53/0.69 66:1:4:[62.3,5.0,59.2,63.1,57.1,64.2,1.0,65.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 0.53/0.69 70:1:4:[62.3,6.0,59.2,67.1,57.1,68.2,1.0,69.3]:TopTopTopTop: -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc30)
% 0.53/0.69 74:1:4:[62.3,7.1,59.2,71.2,57.1,72.3,1.0,73.4]:TopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc31) ->
% 0.53/0.69 79:1:5:[66.4,8.0,62.3,75.1,59.2,76.2,57.1,77.3,1.0,78.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.53/0.69 84:1:5:[66.4,9.0,62.3,80.1,59.2,81.2,57.1,82.3,1.0,83.4]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28)
% 0.53/0.69 89:1:5:[66.4,10.1,62.3,85.2,59.2,86.3,57.1,87.4,1.0,88.5]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29) ->
% 0.53/0.69 95:1:6:[79.5,11.0,66.4,90.1,62.3,91.2,59.2,92.3,57.1,93.4,1.0,94.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.53/0.69 101:1:6:[79.5,12.0,66.4,96.1,62.3,97.2,59.2,98.3,57.1,99.4,1.0,100.5]:TopTopTopTopTopTop: -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26)
% 0.53/0.69 107:1:6:[79.5,13.1,66.4,102.2,62.3,103.3,59.2,104.4,57.1,105.5,1.0,106.6]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27) ->
% 0.53/0.69 114:1:7:[95.6,14.0,79.5,108.1,66.4,109.2,62.3,110.3,59.2,111.4,57.1,112.5,1.0,113.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.53/0.69 121:1:7:[95.6,15.0,79.5,115.1,66.4,116.2,62.3,117.3,59.2,118.4,57.1,119.5,1.0,120.6]:TopTopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24)
% 0.53/0.69 128:1:7:[95.6,16.1,79.5,122.2,66.4,123.3,62.3,124.4,59.2,125.5,57.1,126.6,1.0,127.7]:TopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25) ->
% 0.53/0.69 136:1:8:[114.7,17.0,95.6,129.1,79.5,130.2,66.4,131.3,62.3,132.4,59.2,133.5,57.1,134.6,1.0,135.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.53/0.69 145:1:9:[136.8,18.0,114.7,137.1,95.6,138.2,79.5,139.3,66.4,140.4,62.3,141.5,59.2,142.6,57.1,143.7,1.0,144.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.53/0.69 155:1:10:[145.9,19.0,136.8,146.1,114.7,147.2,95.6,148.3,79.5,149.4,66.4,150.5,62.3,151.6,59.2,152.7,57.1,153.8,1.0,154.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.53/0.69 166:1:11:[155.10,20.0,145.9,156.1,136.8,157.2,114.7,158.3,95.6,159.4,79.5,160.5,66.4,161.6,62.3,162.7,59.2,163.8,57.1,164.9,1.0,165.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.53/0.69 178:1:12:[166.11,21.0,155.10,167.1,145.9,168.2,136.8,169.3,114.7,170.4,95.6,171.5,79.5,172.6,66.4,173.7,62.3,174.8,59.2,175.9,57.1,176.10,1.0,177.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.53/0.69 190:1:12:[166.11,22.0,155.10,179.1,145.9,180.2,136.8,181.3,114.7,182.4,95.6,183.5,79.5,184.6,66.4,185.7,62.3,186.8,59.2,187.9,57.1,188.10,1.0,189.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 0.53/0.69 202:1:12:[166.11,23.1,155.10,191.2,145.9,192.3,136.8,193.4,114.7,194.5,95.6,195.6,79.5,196.7,66.4,197.8,62.3,198.9,59.2,199.10,57.1,200.11,1.0,201.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) ->
% 0.53/0.69 213:4:11:[155.10,24.0,145.9,203.1,136.8,204.3,114.7,205.4,95.6,206.5,79.5,207.6,66.4,208.7,62.3,209.8,59.2,210.10,57.1,211.11,1.0,212.12]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.53/0.69 226:1:13:[178.12,25.0,166.11,214.1,155.10,215.2,145.9,216.3,136.8,217.4,114.7,218.5,95.6,219.6,79.5,220.7,66.4,221.8,62.3,222.9,59.2,223.10,57.1,224.11,1.0,225.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.53/0.69 239:1:13:[178.12,26.0,166.11,227.1,155.10,228.2,145.9,229.3,136.8,230.4,114.7,231.5,95.6,232.6,79.5,233.7,66.4,234.8,62.3,235.9,59.2,236.10,57.1,237.11,1.0,238.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 0.53/0.69 252:1:13:[178.12,27.1,166.11,240.2,155.10,241.3,145.9,242.4,136.8,243.5,114.7,244.6,95.6,245.7,79.5,246.8,66.4,247.9,62.3,248.10,59.2,249.11,57.1,250.12,1.0,251.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) ->
% 0.53/0.69 264:4:12:[166.11,28.0,155.10,253.1,145.9,254.2,136.8,255.3,114.7,256.5,95.6,257.6,79.5,258.7,66.4,259.8,62.3,260.9,59.2,261.10,57.1,262.11,1.0,263.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0)
% 0.53/0.69 278:1:14:[226.13,29.0,178.12,265.1,166.11,266.2,155.10,267.3,145.9,268.4,136.8,269.5,114.7,270.6,95.6,271.7,79.5,272.8,66.4,273.9,62.3,274.10,59.2,275.11,57.1,276.12,1.0,277.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.53/0.69 292:1:14:[226.13,30.0,178.12,279.1,166.11,280.2,155.10,281.3,145.9,282.4,136.8,283.5,114.7,284.6,95.6,285.7,79.5,286.8,66.4,287.9,62.3,288.10,59.2,289.11,57.1,290.12,1.0,291.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 0.53/0.69 306:1:14:[226.13,31.1,178.12,293.2,166.11,294.3,155.10,295.4,145.9,296.5,136.8,297.6,114.7,298.7,95.6,299.8,79.5,300.9,66.4,301.10,62.3,302.11,59.2,303.12,57.1,304.13,1.0,305.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) ->
% 0.53/0.69 320:4:14:[226.13,32.0,178.12,307.1,166.11,308.2,155.10,309.3,145.9,310.4,136.8,311.5,114.7,312.6,95.6,313.7,79.5,314.8,66.4,315.9,62.3,316.10,59.2,317.11,57.1,318.13,1.0,319.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2)
% 0.53/0.69 335:1:15:[278.14,33.0,226.13,321.1,178.12,322.2,166.11,323.3,155.10,324.4,145.9,325.5,136.8,326.6,114.7,327.7,95.6,328.8,79.5,329.9,66.4,330.10,62.3,331.11,59.2,332.12,57.1,333.13,1.0,334.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.53/0.69 350:1:15:[278.14,34.0,226.13,336.1,178.12,337.2,166.11,338.3,155.10,339.4,145.9,340.5,136.8,341.6,114.7,342.7,95.6,343.8,79.5,344.9,66.4,345.10,62.3,346.11,59.2,347.12,57.1,348.13,1.0,349.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 0.53/0.69 364:4:14:[226.13,35.0,178.12,351.1,166.11,352.2,155.10,353.3,145.9,354.4,136.8,355.6,114.7,356.7,95.6,357.8,79.5,358.9,66.4,359.10,62.3,360.11,59.2,361.12,57.1,362.13,1.0,363.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv18_3r1r1r1(x0,x1,x2)
% 0.53/0.69 379:1:15:[278.14,36.1,226.13,365.2,178.12,366.3,166.11,367.4,155.10,368.5,145.9,369.6,136.8,370.7,114.7,371.8,95.6,372.9,79.5,373.10,66.4,374.11,62.3,375.12,59.2,376.13,57.1,377.14,1.0,378.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) ->
% 0.53/0.69 393:4:14:[226.13,37.0,178.12,380.2,166.11,381.4,155.10,382.5,145.9,383.6,136.8,384.7,114.7,385.9,95.6,386.10,79.5,387.11,66.4,388.12,62.3,389.13,59.2,390.15,57.1,391.16,1.0,392.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) ->
% 0.53/0.69 407:4:14:[226.13,38.0,178.12,394.3,166.11,395.4,155.10,396.5,145.9,397.6,136.8,398.8,114.7,399.9,95.6,400.10,79.5,401.11,66.4,402.12,62.3,403.13,59.2,404.14,57.1,405.16,1.0,406.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) ->
% 0.53/0.69 422:4:15:[278.14,39.0,226.13,408.1,178.12,409.2,166.11,410.3,155.10,411.4,145.9,412.5,136.8,413.6,114.7,414.7,95.6,415.8,79.5,416.9,66.4,417.10,62.3,418.11,59.2,419.12,57.1,420.13,1.0,421.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv20_1r1(x0)
% 0.53/0.69 438:1:16:[335.15,40.0,278.14,423.1,226.13,424.2,178.12,425.3,166.11,426.4,155.10,427.5,145.9,428.6,136.8,429.7,114.7,430.8,95.6,431.9,79.5,432.10,66.4,433.11,62.3,434.12,59.2,435.13,57.1,436.14,1.0,437.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.53/0.69 453:4:15:[278.14,41.0,226.13,439.2,178.12,440.3,166.11,441.4,155.10,442.5,145.9,443.6,136.8,444.7,114.7,445.8,95.6,446.9,79.5,447.10,66.4,448.11,62.3,449.13,59.2,450.14,57.1,451.15,1.0,452.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.53/0.69 468:4:15:[278.14,42.0,226.13,454.1,178.12,455.2,166.11,456.3,155.10,457.4,145.9,458.5,136.8,459.6,114.7,460.8,95.6,461.9,79.5,462.10,66.4,463.11,62.3,464.12,59.2,465.13,57.1,466.14,1.0,467.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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.53/0.69 483:4:15:[278.14,43.0,226.13,469.1,178.12,470.2,166.11,471.3,155.10,472.4,145.9,473.5,136.8,474.6,114.7,475.7,95.6,476.8,79.5,477.9,66.4,478.10,62.3,479.11,59.2,480.12,57.1,481.13,1.0,482.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> 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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1)
% 0.53/0.69 500:1:17:[438.16,44.0,335.15,484.1,278.14,485.2,226.13,486.3,178.12,487.4,166.11,488.5,155.10,489.6,145.9,490.7,136.8,491.8,114.7,492.9,95.6,493.10,79.5,494.11,66.4,495.12,62.3,496.13,59.2,497.14,57.1,498.15,1.0,499.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.53/0.69 516:4:16:[335.15,45.0,278.14,501.1,226.13,502.2,178.12,503.3,166.11,504.5,155.10,505.6,145.9,506.7,136.8,507.8,114.7,508.9,95.6,509.10,79.5,510.11,66.4,511.12,62.3,512.14,59.2,513.15,57.1,514.16,1.0,515.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv18_3r1r1r1(x0,x1,x2) -> 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)
% 0.53/0.69 534:1:18:[500.17,46.0,438.16,517.1,335.15,518.2,278.14,519.3,226.13,520.4,178.12,521.5,166.11,522.6,155.10,523.7,145.9,524.8,136.8,525.9,114.7,526.10,95.6,527.11,79.5,528.12,66.4,529.13,62.3,530.14,59.2,531.15,57.1,532.16,1.0,533.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.53/0.69 551:4:17:[438.16,47.0,335.15,535.2,278.14,536.3,226.13,537.4,178.12,538.5,166.11,539.6,155.10,540.7,145.9,541.8,136.8,542.9,114.7,543.10,95.6,544.11,79.5,545.12,66.4,546.14,62.3,547.15,59.2,548.16,57.1,549.17,1.0,550.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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)
% 0.53/0.69 568:4:17:[438.16,48.0,335.15,552.2,278.14,553.4,226.13,554.5,178.12,555.6,166.11,556.7,155.10,557.8,145.9,558.9,136.8,559.11,114.7,560.12,95.6,561.13,79.5,562.14,66.4,563.15,62.3,564.16,59.2,565.17,57.1,566.18,1.0,567.19]: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),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.53/0.69 585:4:17:[438.16,49.0,335.15,569.2,278.14,570.4,226.13,571.5,178.12,572.6,166.11,573.7,155.10,574.8,145.9,575.9,136.8,576.10,114.7,577.11,95.6,578.12,79.5,579.13,66.4,580.14,62.3,581.15,59.2,582.16,57.1,583.17,1.0,584.18]: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) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.53/0.69 604:1:19:[534.18,50.0,500.17,586.1,438.16,587.2,335.15,588.3,278.14,589.4,226.13,590.5,178.12,591.6,166.11,592.7,155.10,593.8,145.9,594.9,136.8,595.10,114.7,596.11,95.6,597.12,79.5,598.13,66.4,599.14,62.3,600.15,59.2,601.16,57.1,602.17,1.0,603.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.53/0.69 622:4:18:[500.17,51.0,438.16,605.2,335.15,606.4,278.14,607.5,226.13,608.6,178.12,609.7,166.11,610.8,155.10,611.9,145.9,612.11,136.8,613.12,114.7,614.13,95.6,615.14,79.5,616.15,66.4,617.16,62.3,618.17,59.2,619.18,57.1,620.19,1.0,621.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.53/0.69 641:4:19:[534.18,52.0,500.17,623.1,438.16,624.2,335.15,625.3,278.14,626.4,226.13,627.5,178.12,628.6,166.11,629.7,155.10,630.8,145.9,631.9,136.8,632.10,114.7,633.11,95.6,634.12,79.5,635.14,66.4,636.15,62.3,637.16,59.2,638.17,57.1,639.19,1.0,640.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.53/0.69 660:4:19:[534.18,53.0,500.17,642.2,438.16,643.3,335.15,644.4,278.14,645.5,226.13,646.6,178.12,647.7,166.11,648.8,155.10,649.9,145.9,650.10,136.8,651.11,114.7,652.12,95.6,653.14,79.5,654.15,66.4,655.16,62.3,656.17,59.2,657.18,57.1,658.19,1.0,659.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv20_1r1(x0)
% 0.53/0.69 680:4:20:[604.19,54.0,534.18,661.2,500.17,662.3,438.16,663.4,335.15,664.5,278.14,665.6,226.13,666.7,178.12,667.8,166.11,668.9,155.10,669.10,145.9,670.11,136.8,671.12,114.7,672.14,95.6,673.15,79.5,674.16,66.4,675.17,62.3,676.18,59.2,677.19,57.1,678.20,1.0,679.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv19_2r1r1(x0,x1)
% 0.53/0.69 700:4:20:[604.19,55.0,534.18,681.2,500.17,682.3,438.16,683.4,335.15,684.5,278.14,685.7,226.13,686.8,178.12,687.9,166.11,688.10,155.10,689.11,145.9,690.12,136.8,691.13,114.7,692.14,95.6,693.15,79.5,694.17,66.4,695.18,62.3,696.19,59.2,697.20,57.1,698.21,1.0,699.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.53/0.69 720:4:20:[604.19,56.0,534.18,701.1,500.17,702.2,438.16,703.3,335.15,704.4,278.14,705.6,226.13,706.7,178.12,707.8,166.11,708.9,155.10,709.10,145.9,710.11,136.8,711.12,114.7,712.13,95.6,713.14,79.5,714.15,66.4,715.16,62.3,716.17,59.2,717.18,57.1,718.19,1.0,719.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.53/0.69
% 0.53/0.69 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) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv19_2r1r1(x0,x1) ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv20_1r1(x0) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv18_3r1r1r1(x0,x1,x2) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) 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) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.53/0.69
% 0.53/0.69 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: lmodel_grow ===
% 0.53/0.69
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 66
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 78
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 92
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 107
% 0.53/0.69 === Conflict found: 516:4:16:[335.15,45.0,278.14,501.1,226.13,502.2,178.12,503.3,166.11,504.5,155.10,505.6,145.9,506.7,136.8,507.8,114.7,508.9,95.6,509.10,79.5,510.11,66.4,511.12,62.3,512.14,59.2,513.15,57.1,514.16,1.0,515.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv18_3r1r1r1(x0,x1,x2) -> 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) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc17, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc17, x14 -> skc30, x15 -> skc17}
% 0.53/0.69 === Backtracking. Learning clause 721:3:14:[516.3,379.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 117
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 132
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 144
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 157
% 0.53/0.69 === Conflict found: 721:3:14:[516.3,379.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv18_3r1r1r1(x0,x1,x2) -> 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 -> skc17, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21}
% 0.53/0.69 === Backtracking. Learning clause 722:2:11:[721.3,252.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv18_3r1r1r1(x0,x1,x2) ->
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 168
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 181
% 0.53/0.69 === Conflict found: 407:4:14:[226.13,38.0,178.12,394.3,166.11,395.4,155.10,396.5,145.9,397.6,136.8,398.8,114.7,399.9,95.6,400.10,79.5,401.11,66.4,402.12,62.3,403.13,59.2,404.14,57.1,405.16,1.0,406.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc17, x5 -> skc30, x6 -> skc17, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20}
% 0.53/0.69 === Backtracking. Learning clause 723:3:12:[407.1,239.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) ->
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 196
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 209
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 220
% 0.53/0.69 === Conflict found: 483:4:15:[278.14,43.0,226.13,469.1,178.12,470.2,166.11,471.3,155.10,472.4,145.9,473.5,136.8,474.6,114.7,475.7,95.6,476.8,79.5,477.9,66.4,478.10,62.3,479.11,59.2,480.12,57.1,481.13,1.0,482.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> 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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc17, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc19}
% 0.53/0.69 === Backtracking. Learning clause 724:2:12:[483.1,306.1,202.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1)
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 229
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 238
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 247
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 256
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 265
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 274
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 282
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 291
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 299
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 306
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 313
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 320
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 327
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 334
% 0.53/0.69 === Conflict found: 422:4:15:[278.14,39.0,226.13,408.1,178.12,409.2,166.11,410.3,155.10,411.4,145.9,412.5,136.8,413.6,114.7,414.7,95.6,415.8,79.5,416.9,66.4,417.10,62.3,418.11,59.2,419.12,57.1,420.13,1.0,421.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.53/0.69 === Backtracking. Learning clause 725:2:5:[422.1,306.1,723.3,724.1,213.2,121.1,121.1,722.1]:TopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 346
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 359
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 371
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 381
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 393
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 402
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 411
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 418
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 427
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 434
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 443
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 450
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 459
% 0.53/0.69 === Conflict found: 393:4:14:[226.13,37.0,178.12,380.2,166.11,381.4,155.10,382.5,145.9,383.6,136.8,384.7,114.7,385.9,95.6,386.10,79.5,387.11,66.4,388.12,62.3,389.13,59.2,390.15,57.1,391.16,1.0,392.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc20, x5 -> skc30, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20}
% 0.53/0.69 === Backtracking. Learning clause 726:3:11:[393.1,239.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) ->
% 0.53/0.69 === Clause set with instances from active satisfied. Growing active. New size: 468
% 0.53/0.69 === Conflict found: 213:4:11:[155.10,24.0,145.9,203.1,136.8,204.3,114.7,205.4,95.6,206.5,79.5,207.6,66.4,208.7,62.3,209.8,59.2,210.10,57.1,211.11,1.0,212.12]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 0.53/0.69 === Backtracking. Learning clause 727:5:28:[213.1,121.1,726.1,101.1,422.3,407.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv16_5r1r1r1r1r1(x0,x14,x15,x16,x17)
% 0.53/0.69 === Conflict found: 213:4:11:[155.10,24.0,145.9,203.1,136.8,204.3,114.7,205.4,95.6,206.5,79.5,207.6,66.4,208.7,62.3,209.8,59.2,210.10,57.1,211.11,1.0,212.12]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 0.53/0.69
% 0.53/0.69 SZS status Unsatisfiable
% 0.53/0.69
% 0.53/0.69 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.53/0.69
% 0.53/0.69 SPASS-SCL-FOL Statistics:
% 0.53/0.69 Number of learned clauses: 7
% 0.53/0.69 Number of propagations: 1159
% 0.53/0.69 Number of decisions: 348
% 0.53/0.69 Number of resolutions: 27
% 0.53/0.69 Number of condensations: 2
% 0.53/0.69 Number of sub resolutions: 664
% 0.53/0.69 Number of input literals (deduplicated): 56
% 0.53/0.69 Number of grows: 41
% 0.53/0.69 Number of considered ground atoms: 468
% 0.53/0.69
% 0.53/0.69 Needed: 0:00:00.11
% 0.53/0.69
%------------------------------------------------------------------------------