%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN705-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 : n026.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.89s 0.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN705-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n026.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:47:24 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.89/0.68 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.89/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.89/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.89/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.89/0.68 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.89/0.68 Execution resolution_1 ended with status: unsatisfiable
% 0.89/0.68 Used heuristic: resolution_1
% 0.89/0.68
% 0.89/0.68 Input Clauses:
% 0.89/0.68
% 0.89/0.68 Predicates: p11 p9 p7 p6 p45 p43 p41 p4 p39 p37 p35 p33 p31 p3 p29 p27 p25 p23 p21 p2 p19 p17 p15 p14 p12 p47
% 0.89/0.68 Fol Constants: c48 c50 c51 c52 c53 c55 c56 c49 c54 c57 c58
% 0.89/0.68 Fol Functions: f18 f16 f13 f5 f26 f24 f22 f20 f10 f46 f44 f42 f38 f36 f34 f8 f32 f28 f30 f40
% 0.89/0.68 Problem Properties:
% 0.89/0.68 This is a full first-order problem without equality.
% 0.89/0.68
% 0.89/0.68 After reduction: Problem Properties:
% 0.89/0.68 This is a full first-order problem without equality.
% 0.89/0.68
% 0.89/0.68
% 0.89/0.68 Reduced Input Clauses:
% 0.89/0.68
% 0.89/0.68 Most General Atoms: p11(x1,x2) p6(x1,x2) p39(x1,x2) p37(x1,x2) p35(x1,x2) p29(x1,x2) p27(x1,x2) p25(x1,x2) p2(x1,x2) p19(x1,x2) p17(x1,x2) p14(x1,x2) p15(x2,x3) p9(x2,x3) p45(x2,x3) p43(x2,x3) p3(x2,x3) p7(x2,x3) p41(x2,x3) p4(x2,x3) p33(x2,x3) p12(x2,x3) p31(x2,x3) p23(x2,x3) p21(x2,x3) p47(x0,x4)
% 0.89/0.68
% 0.89/0.68 === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: resolution_1 ===
% 0.89/0.68
% 0.89/0.68 === Backtracking. Learning clause 81:2:2:[26.2,1.1]:TopTop: p11(x0,x1) -> p11(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 82:2:2:[29.2,4.1]:TopTop: p6(x0,x1) -> p6(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 83:2:2:[31.2,6.1]:TopTop: p43(x0,x1) -> p43(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 84:2:2:[32.2,7.1]:TopTop: p41(x0,x1) -> p41(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 85:2:2:[33.2,8.1]:TopTop: p4(x0,x1) -> p4(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 86:3:2:[53.4,51.1]:TopTop: p47(x0,x1),p7(x1,c55),p4(x0,f5(c48,f13(f16(f18(c50,c51),c52),c53))) ->
% 0.89/0.68 === Backtracking. Learning clause 87:3:6:[53.4,52.1]:TopTopTopTopTopTop: p47(x0,x1),p7(x1,x2),p4(x0,f20(f22(f24(f26(c56,x3),x4),x5),x2)) ->
% 0.89/0.68 === Clause set with instances from active satisfied. Growing active. New size: 115
% 0.89/0.68 === Restarting.
% 0.89/0.68 === Backtracking. Learning clause 88:2:2:[34.2,9.1]:TopTop: p39(x0,x1) -> p39(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 89:2:2:[37.2,12.1]:TopTop: p33(x0,x1) -> p33(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 90:2:2:[38.2,13.1]:TopTop: p31(x0,x1) -> p31(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 91:5:6:[53.3,58.3]:TopTopTopTopTopTop: p47(f5(x0,x1),x2),p7(x2,x3),p2(x0,x4),p3(x1,x5) -> p47(f5(x4,x5),x3)
% 0.89/0.68 === Backtracking. Learning clause 92:2:5:[39.1,80.1]:TopTopTopTopTop: p3(f8(f10(c49,f13(f16(f18(c50,x0),x1),x2)),x3),x4) -> p3(f13(f16(f18(c50,f20(f22(f24(f26(c56,x0),x1),x2),x3)),f30(f32(f34(f36(c57,x0),x1),x2),x3)),f40(f42(f44(f46(c58,x0),x1),x2),x3)),x4)
% 0.89/0.68 === Backtracking. Learning clause 93:2:5:[39.2,80.1]:TopTopTopTopTop: p3(f8(f10(c49,f13(f16(f18(c50,x0),x1),x2)),x3),x4) -> p3(x4,f13(f16(f18(c50,f20(f22(f24(f26(c56,x0),x1),x2),x3)),f30(f32(f34(f36(c57,x0),x1),x2),x3)),f40(f42(f44(f46(c58,x0),x1),x2),x3)))
% 0.89/0.68 === Clause set with instances from active satisfied. Growing active. New size: 120
% 0.89/0.68 === Restarting.
% 0.89/0.68 === Backtracking. Learning clause 94:2:2:[39.2,14.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 95:2:2:[40.2,15.1]:TopTop: p29(x0,x1) -> p29(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 96:1:0:[76.2,51.1]:: p47(c51,c55) ->
% 0.89/0.68 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.89/0.68 === Restarting.
% 0.89/0.68 === Backtracking. Learning clause 97:3:2:[53.4,96.1]:TopTop: p47(x0,x1),p7(x1,c55),p4(x0,c51) ->
% 0.89/0.68 === Backtracking. Learning clause 98:2:2:[35.2,10.1]:TopTop: p37(x0,x1) -> p37(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 99:2:2:[43.2,18.1]:TopTop: p23(x0,x1) -> p23(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 100:2:2:[44.2,19.1]:TopTop: p21(x0,x1) -> p21(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 101:2:2:[48.2,23.1]:TopTop: p15(x0,x1) -> p15(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 102:2:2:[50.2,25.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 0.89/0.68 === Conflict found: 91:5:6:[53.3,58.3]:TopTopTopTopTopTop: p47(f5(x0,x1),x2),p7(x2,x3),p2(x0,x4),p3(x1,x5) -> p47(f5(x4,x5),x3) {x0 -> c48, x1 -> c48, x2 -> c48, x3 -> c48, x4 -> c48, x5 -> f13(f16(f18(c50,c48),c48),c48)}
% 0.89/0.68 === Backtracking. Learning clause 103:5:7:[91.5,74.1]:TopTopTopTopTopTopTop: p47(f5(x0,x1),x2),p7(x2,x3),p2(x0,c48),p3(x1,f13(f16(f18(c50,x4),x5),x6)) -> p47(x4,x3)
% 0.89/0.68 === Backtracking. Learning clause 104:4:5:[33.2,59.3]:TopTopTopTopTop: p4(f20(x0,x1),x2),p19(x0,x3),p7(x1,x4) -> p4(x2,f20(x3,x4))
% 0.89/0.68 === Backtracking. Learning clause 105:3:2:[53.1,77.1]:TopTop: p7(c55,x0),p4(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),x1) -> p47(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 106:2:1:[53.3,8.1,51.1]:Top: p47(f5(c48,f13(f16(f18(c50,c51),c52),c53)),x0),p7(x0,c55) ->
% 0.89/0.68 === Conflict found: 93:2:5:[39.2,80.1]:TopTopTopTopTop: p3(f8(f10(c49,f13(f16(f18(c50,x0),x1),x2)),x3),x4) -> p3(x4,f13(f16(f18(c50,f20(f22(f24(f26(c56,x0),x1),x2),x3)),f30(f32(f34(f36(c57,x0),x1),x2),x3)),f40(f42(f44(f46(c58,x0),x1),x2),x3))) {x0 -> c48, x1 -> c48, x2 -> c48, x3 -> c48, x4 -> c48}
% 0.89/0.68 === Backtracking. Learning clause 107:5:8:[93.2,103.4]:TopTopTopTopTopTopTopTop: p3(f8(f10(c49,f13(f16(f18(c50,x0),x1),x2)),x3),x4),p47(f5(x5,x4),x6),p7(x6,x7),p2(x5,c48) -> p47(f20(f22(f24(f26(c56,x0),x1),x2),x3),x7)
% 0.89/0.68 === Clause set with instances from active satisfied. Growing active. New size: 146
% 0.89/0.68 === Restarting.
% 0.89/0.68 === Conflict found: 85:2:2:[33.2,8.1]:TopTop: p4(x0,x1) -> p4(x1,x0) {x0 -> c48, x1 -> f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54))}
% 0.89/0.68 === Backtracking. Learning clause 108:3:2:[85.2,105.2]:TopTop: p4(x0,f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54))),p7(c55,x1) -> p47(x0,x1)
% 0.89/0.68 === Conflict found: 91:5:6:[53.3,58.3]:TopTopTopTopTopTop: p47(f5(x0,x1),x2),p7(x2,x3),p2(x0,x4),p3(x1,x5) -> p47(f5(x4,x5),x3) {x0 -> c48, x1 -> f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54), x2 -> c55, x3 -> c48, x4 -> c48, x5 -> c48}
% 0.89/0.68 === Backtracking. Learning clause 109:4:3:[91.1,77.1]:TopTopTop: p7(c55,x0),p2(c48,x1),p3(f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54),x2) -> p47(f5(x1,x2),x0)
% 0.89/0.68 === Conflict found: 107:5:8:[93.2,103.4]:TopTopTopTopTopTopTopTop: p3(f8(f10(c49,f13(f16(f18(c50,x0),x1),x2)),x3),x4),p47(f5(x5,x4),x6),p7(x6,x7),p2(x5,c48) -> p47(f20(f22(f24(f26(c56,x0),x1),x2),x3),x7) {x0 -> c48, x1 -> c48, x2 -> c48, x3 -> c48, x4 -> f8(f10(c49,f13(f16(f18(c50,c48),c48),c48)),c48), x5 -> c48, x6 -> c48, x7 -> c48}
% 0.89/0.68 === Backtracking. Learning clause 110:4:7:[107.1,14.1]:TopTopTopTopTopTopTop: p47(f5(x0,f8(f10(c49,f13(f16(f18(c50,x1),x2),x3)),x4)),x5),p7(x5,x6),p2(x0,c48) -> p47(f20(f22(f24(f26(c56,x1),x2),x3),x4),x6)
% 0.89/0.68 === Backtracking. Learning clause 111:2:1:[53.3,8.1,77.1]:Top: p7(c55,x0) -> p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),x0)
% 0.89/0.68 === Clause set with instances from active satisfied. Growing active. New size: 158
% 0.89/0.68 === Restarting.
% 0.89/0.68 === Backtracking. Learning clause 112:2:2:[41.2,16.1]:TopTop: p27(x0,x1) -> p27(x1,x0)
% 0.89/0.68 === Backtracking. Learning clause 113:2:2:[49.2,24.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 0.89/0.68 === Conflict found: 104:4:5:[33.2,59.3]:TopTopTopTopTop: p4(f20(x0,x1),x2),p19(x0,x3),p7(x1,x4) -> p4(x2,f20(x3,x4)) {x0 -> c48, x1 -> c48, x2 -> c48, x3 -> f22(f24(f26(c56,c48),c48),c48), x4 -> c48}
% 0.89/0.68 === Backtracking. Learning clause 114:5:8:[104.4,87.3]:TopTopTopTopTopTopTopTop: p4(f20(x0,x1),x2),p19(x0,f22(f24(f26(c56,x3),x4),x5)),p7(x1,x6),p47(x2,x7),p7(x7,x6) ->
% 0.89/0.68 === Conflict found: 91:5:6:[53.3,58.3]:TopTopTopTopTopTop: p47(f5(x0,x1),x2),p7(x2,x3),p2(x0,x4),p3(x1,x5) -> p47(f5(x4,x5),x3) {x0 -> c48, x1 -> f13(f16(f18(c50,c48),c48),c48), x2 -> c48, x3 -> c48, x4 -> c48, x5 -> c48}
% 0.89/0.68 === Backtracking. Learning clause 115:5:7:[91.1,76.2,94.2]:TopTopTopTopTopTopTop: p7(x0,x1),p2(c48,x2),p47(x3,x0),p3(x4,f13(f16(f18(c50,x3),x5),x6)) -> p47(f5(x2,x4),x1)
% 0.89/0.68 === Conflict found: 110:4:7:[107.1,14.1]:TopTopTopTopTopTopTop: p47(f5(x0,f8(f10(c49,f13(f16(f18(c50,x1),x2),x3)),x4)),x5),p7(x5,x6),p2(x0,c48) -> p47(f20(f22(f24(f26(c56,x1),x2),x3),x4),x6) {x0 -> c48, x1 -> c51, x2 -> c52, x3 -> c53, x4 -> c54, x5 -> c48, x6 -> c48}
% 0.89/0.68 === Backtracking. Learning clause 116:4:2:[110.1,111.2,75.1]:TopTop: p7(x0,x1),p2(c48,c48),p7(c55,x0) -> p47(c51,x1)
% 0.89/0.68 === Conflict found: 116:4:2:[110.1,111.2,75.1]:TopTop: p7(x0,x1),p2(c48,c48),p7(c55,x0) -> p47(c51,x1) {x0 -> c55, x1 -> c55}
% 0.89/0.68
% 0.89/0.68 SZS status Unsatisfiable
% 0.89/0.68
% 0.89/0.68 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.89/0.68
% 0.89/0.68 SPASS-SCL-FOL Statistics:
% 0.89/0.68 Number of learned clauses: 36
% 0.89/0.68 Number of propagations: 1744
% 0.89/0.68 Number of decisions: 889
% 0.89/0.68 Number of resolutions: 43
% 0.89/0.68 Number of condensations: 0
% 0.89/0.68 Number of sub resolutions: 0
% 0.89/0.68 Number of input literals (deduplicated): 79
% 0.89/0.68 Number of grows: 5
% 0.89/0.68 Number of considered ground atoms: 158
% 0.89/0.68
% 0.89/0.68 Needed: 0:00:00.16
% 0.89/0.68
%------------------------------------------------------------------------------