%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO582+1 : TPTP v9.2.1. Released v5.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:41:09 PM UTC 2026
% Result : CounterSatisfiable 0.39s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO582+1 : TPTP v9.2.1. Released v5.5.0.
% 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.34 % Computer : n009.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Thu May 7 13:55:11 EDT 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.62 Execution resolution_1 ended with status: satisfiable
% 0.39/0.62 Used heuristic: resolution_1
% 0.39/0.62
% 0.39/0.62 Input Clauses:
% 0.39/0.62
% 0.39/0.62 Predicates: k04_buttercup10517 k04_buttercup10516 b48_buttercup10518 b48_buttercup10515 b48_buttercup10519 b48_buttercup10520 b48_buttercup10521 b48_buttercup10421 b48_buttercup10417 b48_buttercup10422 b48_buttercup10227 b48_buttercup10222 b48_buttercup10228 b48_buttercup10229 k04_buttercup10419 k04_buttercup10225 ren1
% 0.39/0.62 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 skc21 skc22 skc23 skc24 skc25 skc26 skc27 skc28 skc29 skc30 skc31 skc32 skc33
% 0.39/0.62 Fol Functions:
% 0.39/0.62 Problem Properties:
% 0.39/0.62 This is a Bernays Schoenfinkel problem.
% 0.39/0.62
% 0.39/0.62 After reduction: Problem Properties:
% 0.39/0.62 This is a Bernays Schoenfinkel problem.
% 0.39/0.62
% 0.39/0.62
% 0.39/0.62 Reduced Input Clauses:
% 0.39/0.62
% 0.39/0.62 Most General Atoms: k04_buttercup10517(x0) k04_buttercup10516(x0) b48_buttercup10518(x0) b48_buttercup10515(x0) b48_buttercup10520(x0) b48_buttercup10521(x0) b48_buttercup10421(x0) b48_buttercup10417(x0) b48_buttercup10422(x0) b48_buttercup10227(x0) b48_buttercup10222(x0) b48_buttercup10228(x0) b48_buttercup10229(x0) k04_buttercup10419(x0) ren1(x0) b48_buttercup10519(x1) k04_buttercup10225(x2)
% 0.39/0.62
% 0.39/0.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: resolution_1 ===
% 0.39/0.62
% 0.39/0.62 === Backtracking. Learning clause 72:1:0:[1.2,28.1]:: k04_buttercup10517(skc7) ->
% 0.39/0.62 === Backtracking. Learning clause 73:2:1:[2.2,32.1]:Top: b48_buttercup10518(x0) -> k04_buttercup10516(x0)
% 0.39/0.62 === Backtracking. Learning clause 74:1:0:[2.2,34.1]:: b48_buttercup10518(skc9) ->
% 0.39/0.62 === Backtracking. Learning clause 75:1:0:[32.1,59.1]:: -> k04_buttercup10516(skc26)
% 0.39/0.62 === Backtracking. Learning clause 76:1:0:[3.1,61.1]:: -> b48_buttercup10515(skc28)
% 0.39/0.62 === Backtracking. Learning clause 77:1:0:[5.1,52.1]:: -> b48_buttercup10515(skc19)
% 0.39/0.62 === Backtracking. Learning clause 78:1:0:[41.1,54.1]:: -> k04_buttercup10517(skc21)
% 0.39/0.62 === Backtracking. Learning clause 79:1:0:[6.2,45.1]:: b48_buttercup10421(skc13) ->
% 0.39/0.62 === Backtracking. Learning clause 80:1:0:[26.2,45.1]:: k04_buttercup10516(skc13) ->
% 0.39/0.62 === Backtracking. Learning clause 81:1:0:[7.1,53.1]:: -> b48_buttercup10417(skc20)
% 0.39/0.62 === Backtracking. Learning clause 82:1:0:[8.2,23.1]:: b48_buttercup10227(skc5) ->
% 0.39/0.62 === Backtracking. Learning clause 83:1:0:[9.1,60.1]:: -> b48_buttercup10222(skc27)
% 0.39/0.62 === Backtracking. Learning clause 84:1:0:[10.1,56.1]:: -> b48_buttercup10222(skc23)
% 0.39/0.62 === Backtracking. Learning clause 85:1:0:[17.2,24.1]:: b48_buttercup10228(skc6) ->
% 0.39/0.62 === Backtracking. Learning clause 86:1:0:[11.2,24.1]:: b48_buttercup10422(skc6) ->
% 0.39/0.62 === Backtracking. Learning clause 87:2:0:[17.2,38.1]:: b48_buttercup10228(skc11),b48_buttercup10421(skc11) ->
% 0.39/0.62 === Backtracking. Learning clause 88:2:0:[11.2,38.1]:: b48_buttercup10422(skc11),b48_buttercup10421(skc11) ->
% 0.39/0.62 === Backtracking. Learning clause 89:1:0:[17.2,46.1]:: b48_buttercup10228(skc14) ->
% 0.39/0.62 === Backtracking. Learning clause 90:1:0:[11.2,46.1]:: b48_buttercup10422(skc14) ->
% 0.39/0.62 === Backtracking. Learning clause 91:1:0:[35.1,15.1]:: -> b48_buttercup10222(skc2)
% 0.39/0.62 === Backtracking. Learning clause 92:1:0:[35.1,30.1]:: -> b48_buttercup10222(skc8)
% 0.39/0.62 === Backtracking. Learning clause 93:1:0:[29.2,37.1]:: b48_buttercup10229(skc10) ->
% 0.39/0.62 === Backtracking. Learning clause 94:1:0:[14.2,37.1]:: b48_buttercup10227(skc10) ->
% 0.39/0.62 === Backtracking. Learning clause 95:1:0:[35.1,48.1]:: -> b48_buttercup10222(skc15)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 75
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Conflict found: 73:2:1:[2.2,32.1]:Top: b48_buttercup10518(x0) -> k04_buttercup10516(x0) {x0 -> skc29}
% 0.39/0.62 === Backtracking. Learning clause 96:1:0:[73.1,62.1]:: -> k04_buttercup10516(skc29)
% 0.39/0.62 === Backtracking. Learning clause 97:1:0:[32.1,77.1]:: -> k04_buttercup10516(skc19)
% 0.39/0.62 === Backtracking. Learning clause 98:1:0:[32.1,76.1]:: -> k04_buttercup10516(skc28)
% 0.39/0.62 === Backtracking. Learning clause 99:1:0:[3.1,71.1]:: -> b48_buttercup10515(skc33)
% 0.39/0.62 === Backtracking. Learning clause 100:5:1:[65.2,68.1,69.6,30.1,15.1,14.2]:Top: b48_buttercup10519(skc8),b48_buttercup10519(skc32),b48_buttercup10227(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc2)
% 0.39/0.62 === Backtracking. Learning clause 101:5:1:[65.2,68.1,69.6,30.1,15.1]:Top: k04_buttercup10225(x0),b48_buttercup10519(skc8),b48_buttercup10519(skc32) -> b48_buttercup10519(x0),b48_buttercup10519(skc2)
% 0.39/0.62 === Conflict found: 101:5:1:[65.2,68.1,69.6,30.1,15.1]:Top: k04_buttercup10225(x0),b48_buttercup10519(skc8),b48_buttercup10519(skc32) -> b48_buttercup10519(x0),b48_buttercup10519(skc2) {x0 -> skc2}
% 0.39/0.62 === Backtracking. Learning clause 102:3:0:[101.1,15.1]:: b48_buttercup10519(skc8),b48_buttercup10519(skc32) -> b48_buttercup10519(skc2)
% 0.39/0.62 === Backtracking. Learning clause 103:3:1:[68.1,64.2]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc32)
% 0.39/0.62 === Backtracking. Learning clause 104:3:1:[14.2,103.1]:Top: b48_buttercup10227(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc32)
% 0.39/0.62 === Conflict found: 103:3:1:[68.1,64.2]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc32) {x0 -> skc2}
% 0.39/0.62 === Backtracking. Learning clause 105:2:0:[103.1,15.1,102.2]:: b48_buttercup10519(skc8) -> b48_buttercup10519(skc2)
% 0.39/0.62 === Backtracking. Learning clause 106:3:1:[65.2,68.1]:Top: k04_buttercup10225(skc32),k04_buttercup10225(x0) -> b48_buttercup10519(x0)
% 0.39/0.62 === Backtracking. Learning clause 109:3:1:[71.0,107.0,104.2,108.1,69.1,70.1,106.1,30.1,14.2]:Top: b48_buttercup10227(x0) -> b48_buttercup10519(skc8),b48_buttercup10519(x0)
% 0.39/0.62 === Backtracking. Learning clause 112:3:1:[71.0,110.0,103.2,111.1,69.1,70.1,106.1,30.1]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(skc8),b48_buttercup10519(x0)
% 0.39/0.62 === Conflict found: 112:3:1:[71.0,110.0,103.2,111.1,69.1,70.1,106.1,30.1]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(skc8),b48_buttercup10519(x0) {x0 -> skc2}
% 0.39/0.62 === Backtracking. Learning clause 113:1:0:[112.1,15.1,105.1]:: -> b48_buttercup10519(skc2)
% 0.39/0.62 === Backtracking. Learning clause 116:3:1:[113.0,114.0,104.2,115.1,69.6,106.1,67.1,15.1,14.2]:Top: b48_buttercup10227(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc31)
% 0.39/0.62 === Backtracking. Learning clause 119:3:1:[113.0,117.0,103.2,118.1,69.6,106.1,67.1,15.1]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc31)
% 0.39/0.62 === Conflict found: 119:3:1:[113.0,117.0,103.2,118.1,69.6,106.1,67.1,15.1]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc31) {x0 -> skc15}
% 0.39/0.62 === Backtracking. Learning clause 120:2:0:[119.1,48.1]:: -> b48_buttercup10519(skc15),b48_buttercup10519(skc31)
% 0.39/0.62 === Backtracking. Learning clause 123:2:1:[109.1,121.0,116.2,122.1,69.6,66.1,30.1,14.2]:Top: b48_buttercup10227(x0) -> b48_buttercup10519(x0)
% 0.39/0.62 === Backtracking. Learning clause 126:2:1:[112.1,124.0,119.2,125.2,69.6,66.1,30.1]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(x0)
% 0.39/0.62 === Conflict found: 126:2:1:[112.1,124.0,119.2,125.2,69.6,66.1,30.1]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(x0) {x0 -> skc15}
% 0.39/0.62 === Backtracking. Learning clause 127:1:0:[126.1,48.1]:: -> b48_buttercup10519(skc15)
% 0.39/0.62 === Backtracking. Learning clause 128:3:1:[29.2,119.1]:Top: b48_buttercup10229(x0) -> b48_buttercup10519(x0),b48_buttercup10519(skc31)
% 0.39/0.62 === Backtracking. Learning clause 129:1:0:[67.1,119.1]:: -> b48_buttercup10519(skc31)
% 0.39/0.62 === Backtracking. Learning clause 131:1:0:[129.0,130.1,29.2,66.1]:: b48_buttercup10229(skc31) ->
% 0.39/0.62 === Backtracking. Learning clause 133:1:0:[123.1,132.1,14.2,66.1]:: b48_buttercup10227(skc31) ->
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 84
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 134:1:0:[1.2,80.1]:: k04_buttercup10517(skc13) ->
% 0.39/0.62 === Backtracking. Learning clause 135:1:0:[32.1,99.1]:: -> k04_buttercup10516(skc33)
% 0.39/0.62 === Backtracking. Learning clause 136:1:0:[3.1,129.1]:: -> b48_buttercup10515(skc31)
% 0.39/0.62 === Backtracking. Learning clause 137:1:0:[4.1,63.1]:: -> b48_buttercup10515(skc30)
% 0.39/0.62 === Backtracking. Learning clause 138:2:1:[29.2,126.1]:Top: b48_buttercup10229(x0) -> b48_buttercup10519(x0)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 86
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 139:1:0:[32.1,137.1]:: -> k04_buttercup10516(skc30)
% 0.39/0.62 === Backtracking. Learning clause 140:1:0:[3.1,127.1]:: -> b48_buttercup10515(skc15)
% 0.39/0.62 === Conflict found: 138:2:1:[29.2,126.1]:Top: b48_buttercup10229(x0) -> b48_buttercup10519(x0) {x0 -> skc23}
% 0.39/0.62 === Backtracking. Learning clause 141:1:0:[138.1,56.1]:: -> b48_buttercup10519(skc23)
% 0.39/0.62 === Conflict found: 126:2:1:[112.1,124.0,119.2,125.2,69.6,66.1,30.1]:Top: k04_buttercup10225(x0) -> b48_buttercup10519(x0) {x0 -> skc8}
% 0.39/0.62 === Backtracking. Learning clause 142:1:0:[126.1,30.1]:: -> b48_buttercup10519(skc8)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 89
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 143:1:0:[3.1,113.1]:: -> b48_buttercup10515(skc2)
% 0.39/0.62 === Conflict found: 123:2:1:[109.1,121.0,116.2,122.1,69.6,66.1,30.1,14.2]:Top: b48_buttercup10227(x0) -> b48_buttercup10519(x0) {x0 -> skc22}
% 0.39/0.62 === Backtracking. Learning clause 144:1:0:[123.1,55.1]:: -> b48_buttercup10519(skc22)
% 0.39/0.62 === Backtracking. Learning clause 145:1:0:[35.1,70.1]:: -> b48_buttercup10222(skc33)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 91
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 146:1:0:[32.1,140.1]:: -> k04_buttercup10516(skc15)
% 0.39/0.62 === Backtracking. Learning clause 147:1:0:[3.1,144.1]:: -> b48_buttercup10515(skc22)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 92
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 148:1:0:[32.1,147.1]:: -> k04_buttercup10516(skc22)
% 0.39/0.62 === Backtracking. Learning clause 149:1:0:[3.1,142.1]:: -> b48_buttercup10515(skc8)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 93
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 150:1:0:[3.1,141.1]:: -> b48_buttercup10515(skc23)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 94
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 151:1:0:[32.1,143.1]:: -> k04_buttercup10516(skc2)
% 0.39/0.62 === Backtracking. Learning clause 152:1:0:[32.1,150.1]:: -> k04_buttercup10516(skc23)
% 0.39/0.62 === Backtracking. Learning clause 153:1:0:[32.1,136.1]:: -> k04_buttercup10516(skc31)
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 143
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 207
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 271
% 0.39/0.62
% 0.39/0.62 Linear Model Building succeeded.
% 0.39/0.62 SZS status Satisfiable
% 0.39/0.62
% 0.39/0.62 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.62
% 0.39/0.62 SPASS-SCL-FOL Statistics:
% 0.39/0.62 Number of learned clauses: 68
% 0.39/0.62 Number of propagations: 2736
% 0.39/0.62 Number of decisions: 833
% 0.39/0.62 Number of resolutions: 90
% 0.39/0.62 Number of condensations: 0
% 0.39/0.62 Number of sub resolutions: 14
% 0.39/0.62 Number of input literals (deduplicated): 66
% 0.39/0.62 Number of grows: 11
% 0.39/0.62 Number of considered ground atoms: 271
% 0.39/0.62
% 0.39/0.62 Needed: 0:00:00.07
% 0.39/0.62
%------------------------------------------------------------------------------