%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN706-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 : n025.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:10 PM UTC 2026
% Result : Unsatisfiable 0.48s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.15 % Problem : SYN706-1 : TPTP v9.2.1. Released v2.5.0.
% 0.10/0.16 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.39 % Computer : n025.cluster.edu
% 0.22/0.39 % Model : x86_64 x86_64
% 0.22/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.39 % Memory : 8042.1875MB
% 0.22/0.39 % OS : Linux 3.10.0-693.el7.x86_64
% 0.22/0.39 % CPULimit : 300
% 0.22/0.39 % WCLimit : 300
% 0.22/0.39 % DateTime : Thu May 7 13:47:14 EDT 2026
% 0.22/0.39 % CPUTime :
% 0.22/0.39 SPASS-SCL-FOL version:
% 0.30/0.50 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.48/0.84 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.84 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.84 Execution resolution_3 ended with status: unsatisfiable
% 0.48/0.84 Used heuristic: resolution_3
% 0.48/0.84
% 0.48/0.84 Input Clauses:
% 0.48/0.84
% 0.48/0.84 Predicates: p10 p9 p7 p6 p47 p43 p41 p4 p39 p37 p36 p33 p3 p29 p27 p26 p24 p22 p21 p2 p19 p18 p16 p15 p13 p12 p45 p48 p46 p30
% 0.48/0.84 Fol Constants: c52 c50 c58 c49 c51 c59 c60 c54 c55 c56 c57 c53 c62 c61
% 0.48/0.84 Fol Functions: f20 f5 f40 f38 f17 f35 f14 f11 f8 f34 f32 f31 f28 f25 f44 f23 f42
% 0.48/0.84 Problem Properties:
% 0.48/0.84 This is a full first-order problem without equality.
% 0.48/0.84
% 0.48/0.84 After reduction: Problem Properties:
% 0.48/0.84 This is a full first-order problem without equality.
% 0.48/0.84
% 0.48/0.84
% 0.48/0.84 Reduced Input Clauses:
% 0.48/0.84
% 0.48/0.84 Most General Atoms: p10(x1,x2) p6(x1,x2) p47(x1,x2) p43(x1,x2) p36(x1,x2) p29(x1,x2) p26(x1,x2) p24(x1,x2) p2(x1,x2) p18(x1,x2) p15(x1,x2) p12(x1,x2) p19(x0,x3) p45(x3,x2) p37(x2,x3) p48(x3,x1) p22(x2,x3) p46(x3,x1) p13(x2,x3) p7(x2,x3) p9(x2,x3) p3(x2,x3) p4(x2,x3) p39(x2,x3) p33(x2,x3) p30(x2,x3) p27(x2,x3) p21(x2,x3) p41(x2,x3) p16(x2,x3)
% 0.48/0.84
% 0.48/0.84 === Starting SPASS-SCL-FOL A Little Less Naive, considering 52 atoms initially, heuristics mode: resolution_3 ===
% 0.48/0.84
% 0.48/0.84 === Backtracking. Learning clause 82:2:1:[37.3,28.1]:Top: p4(x0,f5(c49,c50)),p4(x0,c51) ->
% 0.48/0.84 === Backtracking. Learning clause 83:3:2:[56.1,27.1]:TopTop: p7(c58,x0),p19(f20(c52,c50),x1) -> p45(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 84:2:2:[30.2,1.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 85:2:2:[32.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 86:2:2:[33.2,4.1]:TopTop: p6(x0,x1) -> p6(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 87:2:2:[36.2,7.1]:TopTop: p41(x0,x1) -> p41(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 88:3:2:[57.4,29.1]:TopTop: p47(x0,c60),p48(x1,x0),p37(x1,f38(f40(c59,c50),c58)) ->
% 0.48/0.84 === Clause set with instances from active satisfied. Growing active. New size: 116
% 0.48/0.84 === Restarting.
% 0.48/0.84 === Backtracking. Learning clause 89:2:2:[37.2,8.1]:TopTop: p4(x0,x1) -> p4(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 90:3:2:[37.1,65.3,28.1]:TopTop: p4(f5(x0,x1),c51),p2(x0,c49),p3(x1,c50) ->
% 0.48/0.84 === Backtracking. Learning clause 91:2:2:[39.2,10.1]:TopTop: p37(x0,x1) -> p37(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 92:2:2:[40.2,11.1]:TopTop: p36(x0,x1) -> p36(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 93:2:2:[43.2,14.1]:TopTop: p29(x0,x1) -> p29(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 94:2:2:[44.2,15.1]:TopTop: p27(x0,x1) -> p27(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 95:2:2:[46.2,17.1]:TopTop: p24(x0,x1) -> p24(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 96:2:2:[47.2,18.1]:TopTop: p22(x0,x1) -> p22(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 97:2:2:[50.2,21.1]:TopTop: p19(x0,x1) -> p19(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 98:2:2:[52.2,23.1]:TopTop: p16(x0,x1) -> p16(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 99:2:2:[54.2,25.1]:TopTop: p13(x0,x1) -> p13(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 100:2:2:[55.2,26.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 0.48/0.84 === Backtracking. Learning clause 101:4:5:[58.2,78.2]:TopTopTopTopTop: p4(f5(c49,x0),x1),p22(f23(c53,f35(x2,x3)),x4),p45(f20(c52,x0),x2) -> p46(x4,x1)
% 0.48/0.84 === Backtracking. Learning clause 102:2:3:[37.1,60.1]:TopTopTop: p4(f25(f28(c56,f31(f34(c57,x0),f32(x1,x0))),x1),x2) -> p4(x1,x2)
% 0.48/0.84 === Clause set with instances from active satisfied. Growing active. New size: 137
% 0.48/0.84 === Restarting.
% 0.48/0.84 === Conflict found: 89:2:2:[37.2,8.1]:TopTop: p4(x0,x1) -> p4(x1,x0) {x0 -> c51, x1 -> f5(c52,c52)}
% 0.48/0.84 === Backtracking. Learning clause 103:3:2:[89.2,90.1]:TopTop: p4(c51,f5(x0,x1)),p2(x0,c49),p3(x1,c50) ->
% 0.48/0.84 === Conflict found: 89:2:2:[37.2,8.1]:TopTop: p4(x0,x1) -> p4(x1,x0) {x0 -> c51, x1 -> f5(c49,c50)}
% 0.48/0.84 === Backtracking. Learning clause 104:1:0:[89.2,28.1]:: p4(c51,f5(c49,c50)) ->
% 0.48/0.84 === Conflict found: 97:2:2:[50.2,21.1]:TopTop: p19(x0,x1) -> p19(x1,x0) {x0 -> c52, x1 -> f20(c52,c50)}
% 0.48/0.84 === Backtracking. Learning clause 105:3:2:[97.2,83.2]:TopTop: p19(x0,f20(c52,c50)),p7(c58,x1) -> p45(x0,x1)
% 0.48/0.84 === Conflict found: 96:2:2:[47.2,18.1]:TopTop: p22(x0,x1) -> p22(x1,x0) {x0 -> c52, x1 -> f23(c53,f35(c52,c52))}
% 0.48/0.84 === Backtracking. Learning clause 106:4:5:[96.2,101.2]:TopTopTopTopTop: p22(x0,f23(c53,f35(x1,x2))),p4(f5(c49,x3),x4),p45(f20(c52,x3),x1) -> p46(x0,x4)
% 0.48/0.84 === Backtracking. Learning clause 107:4:3:[57.3,67.3,29.1]:TopTopTop: p47(x0,c60),p48(f38(x1,x2),x0),p36(x1,f40(c59,c50)),p7(x2,c58) ->
% 0.48/0.84 === Backtracking. Learning clause 108:2:1:[57.3,10.1,29.1]:Top: p47(x0,c60),p48(f38(f40(c59,c50),c58),x0) ->
% 0.48/0.84 === Conflict found: 106:4:5:[96.2,101.2]:TopTopTopTopTop: p22(x0,f23(c53,f35(x1,x2))),p4(f5(c49,x3),x4),p45(f20(c52,x3),x1) -> p46(x0,x4) {x0 -> f23(c53,f35(c52,c52)), x1 -> c52, x2 -> c52, x3 -> c52, x4 -> c52}
% 0.48/0.84 === Backtracking. Learning clause 109:3:4:[106.1,18.1]:TopTopTopTop: p4(f5(c49,x0),x1),p45(f20(c52,x0),x2) -> p46(f23(c53,f35(x2,x3)),x1)
% 0.48/0.84 === Conflict found: 85:2:2:[32.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(f11(c54,f14(f17(c55,c52),f35(c52,c52))),c52), x1 -> c52}
% 0.48/0.84 === Backtracking. Learning clause 110:1:2:[85.1,59.1]:TopTop: -> p7(x0,f8(f11(c54,f14(f17(c55,x1),f35(x0,x1))),x0))
% 0.48/0.84 === Conflict found: 89:2:2:[37.2,8.1]:TopTop: p4(x0,x1) -> p4(x1,x0) {x0 -> f25(f28(c56,f31(f34(c57,c52),f32(c52,c52))),c52), x1 -> c52}
% 0.48/0.84 === Backtracking. Learning clause 111:1:2:[89.1,60.1]:TopTop: -> p4(x0,f25(f28(c56,f31(f34(c57,x1),f32(x0,x1))),x0))
% 0.48/0.84 === Backtracking. Learning clause 112:3:4:[66.3,102.1]:TopTopTopTop: p24(f28(c56,f31(f34(c57,x0),f32(x1,x0))),x2),p4(x1,x3) -> p4(x1,f25(x2,x3))
% 0.48/0.84 === Clause set with instances from active satisfied. Growing active. New size: 154
% 0.48/0.84 === Restarting.
% 0.48/0.84 === Conflict found: 95:2:2:[46.2,17.1]:TopTop: p24(x0,x1) -> p24(x1,x0) {x0 -> c52, x1 -> f28(c56,f31(f34(c57,c52),f32(c52,c52)))}
% 0.48/0.84 === Backtracking. Learning clause 113:3:4:[95.2,112.1]:TopTopTopTop: p24(x0,f28(c56,f31(f34(c57,x1),f32(x2,x1)))),p4(x2,x3) -> p4(x2,f25(x0,x3))
% 0.48/0.84 === Backtracking. Learning clause 114:4:5:[72.3,112.1]:TopTopTopTopTop: p26(c56,x0),p27(f31(f34(c57,x1),f32(x2,x1)),x3),p4(x2,x4) -> p4(x2,f25(f28(x0,x3),x4))
% 0.48/0.84 === Conflict found: 107:4:3:[57.3,67.3,29.1]:TopTopTop: p47(x0,c60),p48(f38(x1,x2),x0),p36(x1,f40(c59,c50)),p7(x2,c58) -> {x0 -> c60, x1 -> f40(c59,c50), x2 -> f8(f11(c54,f14(f17(c55,c61),c52)),c52)}
% 0.48/0.84 === Backtracking. Learning clause 115:5:2:[107.2,81.3]:TopTop: p47(c60,c60),p36(f40(c59,c50),f40(c59,c50)),p7(f8(f11(c54,f14(f17(c55,c61),x0)),x1),c58),p45(f20(c52,c50),x1),p46(f23(c53,x0),f5(c49,c50)) ->
% 0.48/0.84 === Conflict found: 102:2:3:[37.1,60.1]:TopTopTop: p4(f25(f28(c56,f31(f34(c57,x0),f32(x1,x0))),x1),x2) -> p4(x1,x2) {x0 -> c52, x1 -> c52, x2 -> f25(f28(c56,f31(f34(c57,c52),f32(f25(f28(c56,f31(f34(c57,c52),f32(c52,c52))),c52),c52))),f25(f28(c56,f31(f34(c57,c52),f32(c52,c52))),c52))}
% 0.48/0.84 === Backtracking. Learning clause 116:1:3:[102.1,111.1]:TopTopTop: -> p4(x0,f25(f28(c56,f31(f34(c57,x1),f32(f25(f28(c56,f31(f34(c57,x2),f32(x0,x2))),x0),x1))),f25(f28(c56,f31(f34(c57,x2),f32(x0,x2))),x0)))
% 0.48/0.84 === Clause set with instances from active satisfied. Growing active. New size: 171
% 0.48/0.84 === Restarting.
% 0.48/0.84 === Conflict found: 94:2:2:[44.2,15.1]:TopTop: p27(x0,x1) -> p27(x1,x0) {x0 -> c52, x1 -> f31(f34(c57,c52),f32(c52,c52))}
% 0.48/0.84 === Backtracking. Learning clause 117:4:5:[94.2,114.2]:TopTopTopTopTop: p27(x0,f31(f34(c57,x1),f32(x2,x1))),p26(c56,x3),p4(x2,x4) -> p4(x2,f25(f28(x3,x0),x4))
% 0.48/0.84 === Conflict found: 85:2:2:[32.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c58, x1 -> f8(f11(c54,f14(f17(c55,c61),c52)),c52)}
% 0.48/0.84 === Backtracking. Learning clause 118:6:3:[85.2,115.3,32.3]:TopTopTop: p47(c60,c60),p36(f40(c59,c50),f40(c59,c50)),p45(f20(c52,c50),x0),p46(f23(c53,x1),f5(c49,c50)),p7(x2,c58),p7(x2,f8(f11(c54,f14(f17(c55,c61),x1)),x0)) ->
% 0.48/0.84 === Conflict found: 114:4:5:[72.3,112.1]:TopTopTopTopTop: p26(c56,x0),p27(f31(f34(c57,x1),f32(x2,x1)),x3),p4(x2,x4) -> p4(x2,f25(f28(x0,x3),x4)) {x0 -> c52, x1 -> c52, x2 -> c52, x3 -> f31(c52,c52), x4 -> c52}
% 0.48/0.84 === Backtracking. Learning clause 119:5:6:[114.2,71.3]:TopTopTopTopTopTop: p26(c56,x0),p4(x1,x2),p29(f34(c57,x3),x4),p30(f32(x1,x3),x5) -> p4(x1,f25(f28(x0,f31(x4,x5)),x2))
% 0.48/0.84 === Conflict found: 115:5:2:[107.2,81.3]:TopTop: p47(c60,c60),p36(f40(c59,c50),f40(c59,c50)),p7(f8(f11(c54,f14(f17(c55,c61),x0)),x1),c58),p45(f20(c52,c50),x1),p46(f23(c53,x0),f5(c49,c50)) -> {x0 -> f35(c58,c61), x1 -> c58}
% 0.48/0.84
% 0.48/0.84 SZS status Unsatisfiable
% 0.48/0.84
% 0.48/0.84 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.84
% 0.48/0.84 SPASS-SCL-FOL Statistics:
% 0.48/0.84 Number of learned clauses: 38
% 0.48/0.84 Number of propagations: 1895
% 0.48/0.84 Number of decisions: 1004
% 0.48/0.84 Number of resolutions: 47
% 0.48/0.84 Number of condensations: 0
% 0.48/0.84 Number of sub resolutions: 0
% 0.48/0.84 Number of input literals (deduplicated): 86
% 0.48/0.84 Number of grows: 4
% 0.48/0.84 Number of considered ground atoms: 171
% 0.48/0.84
% 0.48/0.84 Needed: 0:00:00.16
% 0.48/0.84
%------------------------------------------------------------------------------