%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN670-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.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:08 PM UTC 2026
% Result : Unsatisfiable 19.23s 4.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN670-1 : TPTP v9.2.1. Released v2.5.0.
% 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n028.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 13:47:16 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 19.23/4.37 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.23/4.37 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.23/4.37 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.23/4.37 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.23/4.37 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.23/4.37 Execution resolution_1 ended with status: unsatisfiable
% 19.23/4.37 Used heuristic: resolution_1
% 19.23/4.37
% 19.23/4.37 Input Clauses:
% 19.23/4.37
% 19.23/4.37 Predicates: p22 p10 p7 p6 p3 p20 p2 p19 p14 p12 p25 p26 p23 p27 p24
% 19.23/4.37 Fol Constants: c28 c32 c33 c36 c29 c30 c35 c34 c37 c31
% 19.23/4.37 Fol Functions: f8 f21 f5 f4 f17 f9 f18 f11 f16 f13 f15
% 19.23/4.37 Problem Properties:
% 19.23/4.37 This is a full first-order problem without equality.
% 19.23/4.37
% 19.23/4.37 After reduction: Problem Properties:
% 19.23/4.37 This is a full first-order problem without equality.
% 19.23/4.37
% 19.23/4.37
% 19.23/4.37 Reduced Input Clauses:
% 19.23/4.37
% 19.23/4.37 Most General Atoms: p22(x1) p6(x1,x2) p20(x1,x2) p14(x1,x2) p2(x2,x3) p27(x3,x1) p12(x2,x3) p24(x1,x3) p25(x3,x1) p10(x2,x3) p26(x1,x3) p7(x2,x3) p3(x2,x3) p19(x4,x5) p23(x5,x3,x1)
% 19.23/4.37
% 19.23/4.37 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_1 ===
% 19.23/4.37
% 19.23/4.37 === Backtracking. Learning clause 55:3:2:[36.2,11.1]:TopTop: p2(c33,x0),p2(c32,x1) -> p25(x1,x0)
% 19.23/4.37 === Backtracking. Learning clause 56:2:1:[26.2,14.1]:Top: p7(f8(c29),x0) -> p7(x0,c30)
% 19.23/4.37 === Backtracking. Learning clause 57:2:2:[26.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 19.23/4.37 === Backtracking. Learning clause 58:2:2:[28.2,5.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 19.23/4.37 === Backtracking. Learning clause 59:2:2:[30.2,7.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 19.23/4.37 === Backtracking. Learning clause 60:3:2:[37.2,15.1]:TopTop: p20(f21(c28,c35),x0),p10(c34,x1) -> p26(x0,x1)
% 19.23/4.37 === Backtracking. Learning clause 61:3:2:[37.2,16.1]:TopTop: p20(f21(c28,c37),x0),p10(c34,x1) -> p26(x0,x1)
% 19.23/4.37 === Clause set with instances from active satisfied. Growing active. New size: 121
% 19.23/4.37 === Restarting.
% 19.23/4.37 === Backtracking. Learning clause 62:2:2:[33.2,10.1]:TopTop: p12(x0,x1) -> p12(x1,x0)
% 19.23/4.37 === Backtracking. Learning clause 63:2:2:[48.3,18.1]:TopTop: p2(x0,f18(x0,x1)),p2(x1,f9(f17(c31))) ->
% 19.23/4.37 === Backtracking. Learning clause 64:3:2:[34.3,38.1]:TopTop: p2(x0,x1),p27(f11(f4(c32),c34),x0) -> p27(f18(f11(f4(c33),c34),f9(f17(c31))),x1)
% 19.23/4.37 === Backtracking. Learning clause 65:3:2:[36.3,38.1]:TopTop: p2(x0,x1),p25(f11(f4(c32),c34),x0) -> p25(f18(f11(f4(c33),c34),f9(f17(c31))),x1)
% 19.23/4.37 === Backtracking. Learning clause 66:3:2:[34.3,39.1]:TopTop: p2(x0,x1),p27(f11(f4(c32),c34),x0) -> p27(f18(f11(f4(c36),c34),f9(f17(c31))),x1)
% 19.23/4.37 === Clause set with instances from active satisfied. Growing active. New size: 164
% 19.23/4.37 === Restarting.
% 19.23/4.37 === Backtracking. Learning clause 67:7:8:[37.1,43.3,37.4]:TopTopTopTopTopTopTopTop: p10(x0,x1),p10(x2,x3),p19(x4,x5),p20(x6,f21(x4,x2)),p26(x6,x7),p10(x7,x0) -> p26(f21(x5,x3),x1)
% 19.23/4.37 === Backtracking. Learning clause 68:5:6:[29.1,43.3,29.3]:TopTopTopTopTopTop: p10(x0,x1),p19(x2,x3),p20(x4,f21(x2,x0)),p20(x4,x5) -> p20(f21(x3,x1),x5)
% 19.23/4.37 === Backtracking. Learning clause 69:5:6:[29.2,6.1,68.5]:TopTopTopTopTopTop: p10(x0,x1),p19(x2,x3),p20(x4,f21(x2,x0)),p20(x4,x5) -> p20(x5,f21(x3,x1))
% 19.23/4.37 === Conflict found: 67:7:8:[37.1,43.3,37.4]:TopTopTopTopTopTopTopTop: p10(x0,x1),p10(x2,x3),p19(x4,x5),p20(x6,f21(x4,x2)),p26(x6,x7),p10(x7,x0) -> p26(f21(x5,x3),x1) {x0 -> c28, x1 -> c28, x2 -> c28, x3 -> c28, x4 -> c28, x5 -> c28, x6 -> f21(c28,c35), x7 -> c28}
% 19.23/4.37 === Backtracking. Learning clause 70:8:9:[67.4,43.3]:TopTopTopTopTopTopTopTopTop: p10(x0,x1),p10(x2,x3),p19(x4,x5),p26(f21(x6,x7),x8),p10(x8,x0),p10(x7,x2),p19(x6,x4) -> p26(f21(x5,x3),x1)
% 19.23/4.37 === Conflict found: 69:5:6:[29.2,6.1,68.5]:TopTopTopTopTopTop: p10(x0,x1),p19(x2,x3),p20(x4,f21(x2,x0)),p20(x4,x5) -> p20(x5,f21(x3,x1)) {x0 -> c28, x1 -> c28, x2 -> c28, x3 -> c28, x4 -> f21(c28,c37), x5 -> c28}
% 19.23/4.37 === Backtracking. Learning clause 71:6:7:[69.3,43.3]:TopTopTopTopTopTopTop: p10(x0,x1),p19(x2,x3),p20(f21(x4,x5),x6),p10(x5,x0),p19(x4,x2) -> p20(x6,f21(x3,x1))
% 19.23/4.37 === Backtracking. Learning clause 72:4:2:[30.1,50.3,59.1]:TopTop: p2(f11(f4(x0),c34),x1),p25(x0,c36),p25(c32,x0) -> p2(x1,f11(f4(c32),c34))
% 19.23/4.37 === Backtracking. Learning clause 73:3:2:[36.1,38.1]:TopTop: p25(x0,f11(f4(c32),c34)),p2(x0,x1) -> p25(x1,f18(f11(f4(c33),c34),f9(f17(c31))))
% 19.23/4.37 === Backtracking. Learning clause 74:2:0:[46.3,42.1]:: p10(c34,c34),p3(f4(f16(c32,f9(f17(c31)))),f4(c32)) ->
% 19.23/4.37 === Backtracking. Learning clause 75:3:2:[34.2,41.1]:TopTop: p2(f11(f4(f16(c33,f9(f17(c31)))),c35),x0),p2(f11(f4(c33),c35),x1) -> p27(x1,x0)
% 19.23/4.37 === Clause set with instances from active satisfied. Growing active. New size: 185
% 19.23/4.37 === Restarting.
% 19.23/4.37 === Backtracking. Learning clause 76:3:3:[26.1,21.2,57.2,57.1]:TopTopTop: p6(x0,x1),p7(x2,f8(x0)) -> p7(x2,f8(x1))
% 19.23/4.37 === Conflict found: 57:2:2:[26.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c29), x1 -> c30}
% 19.23/4.37 === Backtracking. Learning clause 77:3:2:[57.1,14.1,26.2,76.2]:TopTop: p7(c30,x0),p6(c29,x1) -> p7(x0,f8(x1))
% 19.23/4.37 === Backtracking. Learning clause 78:3:3:[30.2,23.2]:TopTopTop: p2(f9(x0),x1),p2(x0,x2) -> p2(x1,f9(x2))
% 19.23/4.37 === Backtracking. Learning clause 79:5:6:[29.2,6.1,43.3,37.1]:TopTopTopTopTopTop: p10(x0,x1),p19(x2,x3),p26(f21(x3,x1),x4),p10(x4,x5) -> p26(f21(x2,x0),x5)
% 19.23/4.37 === Backtracking. Learning clause 80:4:4:[52.4,17.1]:TopTopTopTop: p3(f4(x0),x1),p3(f4(f5(x0)),x2),p19(c28,x3) -> p23(x3,x2,x1)
% 19.23/4.37 === Backtracking. Learning clause 81:2:0:[22.2,74.2]:: p2(f16(c32,f9(f17(c31))),c32),p10(c34,c34) ->
% 19.23/4.37 === Conflict found: 58:2:2:[28.2,5.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f4(c32), x1 -> f4(f16(c32,f9(f17(c31))))}
% 19.23/4.37 === Backtracking. Learning clause 82:2:0:[58.2,74.2]:: p3(f4(c32),f4(f16(c32,f9(f17(c31))))),p10(c34,c34) ->
% 19.23/4.37 === Backtracking. Learning clause 83:4:2:[30.1,49.3,59.1,59.2]:TopTop: p25(x0,c33),p25(c32,x0),p2(x1,f11(f4(x0),c34)) -> p2(x1,f11(f4(c32),c34))
% 19.23/4.37 === Backtracking. Learning clause 84:2:1:[30.1,38.1,59.1]:Top: p2(f11(f4(c32),c34),x0) -> p2(x0,f18(f11(f4(c33),c34),f9(f17(c31))))
% 19.23/4.37 === Backtracking. Learning clause 85:2:1:[30.1,39.1,59.1]:Top: p2(f11(f4(c32),c34),x0) -> p2(x0,f18(f11(f4(c36),c34),f9(f17(c31))))
% 19.23/4.37 === Backtracking. Learning clause 86:2:1:[30.3,42.1]:Top: p2(x0,f11(f4(f16(c32,f9(f17(c31)))),c34)),p2(x0,f11(f4(c32),c34)) ->
% 19.23/4.37 === Backtracking. Learning clause 87:2:0:[49.3,42.1]:: p25(f16(c32,f9(f17(c31))),c33),p25(c32,f16(c32,f9(f17(c31)))) ->
% 19.23/4.37 === Backtracking. Learning clause 88:2:0:[50.3,42.1]:: p25(f16(c32,f9(f17(c31))),c36),p25(c32,f16(c32,f9(f17(c31)))) ->
% 19.23/4.37 === Clause set with instances from active satisfied. Growing active. New size: 229
% 19.23/4.37 === Restarting.
% 19.23/4.37 === Backtracking. Learning clause 89:2:2:[25.2,2.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 19.23/4.37 === Conflict found: 80:4:4:[52.4,17.1]:TopTopTopTop: p3(f4(x0),x1),p3(f4(f5(x0)),x2),p19(c28,x3) -> p23(x3,x2,x1) {x0 -> c28, x1 -> c28, x2 -> f4(c28), x3 -> c28}
% 19.23/4.37 === Backtracking. Learning clause 90:7:7:[80.2,22.2,52.4]:TopTopTopTopTopTopTop: p3(f4(x0),x1),p19(c28,x2),p2(f5(x0),x3),p3(x1,x4),p3(f4(x3),x5),p19(x2,x6) -> p23(x6,x5,x4)
% 19.23/4.37 === Conflict found: 80:4:4:[52.4,17.1]:TopTopTopTop: p3(f4(x0),x1),p3(f4(f5(x0)),x2),p19(c28,x3) -> p23(x3,x2,x1) {x0 -> c28, x1 -> c28, x2 -> f4(f5(c28)), x3 -> c28}
% 19.23/4.37 === Backtracking. Learning clause 91:3:3:[80.2,5.1]:TopTopTop: p3(f4(x0),x1),p19(c28,x2) -> p23(x2,f4(f5(x0)),x1)
% 19.23/4.37 === Backtracking. Learning clause 92:2:2:[29.2,6.1]:TopTop: p20(x0,x1) -> p20(x1,x0)
% 19.23/4.37 === Conflict found: 59:2:2:[30.2,7.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c28, x1 -> f11(f4(f16(c33,f9(f17(c31)))),c35)}
% 19.23/4.37 === Backtracking. Learning clause 93:3:2:[59.2,75.1]:TopTop: p2(x0,f11(f4(f16(c33,f9(f17(c31)))),c35)),p2(f11(f4(c33),c35),x1) -> p27(x1,x0)
% 19.23/4.37 === Backtracking. Learning clause 94:1:0:[30.3,18.1,38.1]:: p2(f11(f4(c32),c34),f11(f4(c33),c34)) ->
% 19.23/4.37 === Backtracking. Learning clause 95:1:0:[30.3,18.1,39.1]:: p2(f11(f4(c32),c34),f11(f4(c36),c34)) ->
% 19.23/4.37 === Clause set with instances from active satisfied. Growing active. New size: 243
% 19.23/4.37 === Restarting.
% 19.23/4.37 === Conflict found: 92:2:2:[29.2,6.1]:TopTop: p20(x0,x1) -> p20(x1,x0) {x0 -> c28, x1 -> f21(c28,c35)}
% 19.23/4.37 === Backtracking. Learning clause 96:3:2:[92.2,60.1]:TopTop: p20(x0,f21(c28,c35)),p10(c34,x1) -> p26(x0,x1)
% 19.23/4.37 === Conflict found: 92:2:2:[29.2,6.1]:TopTop: p20(x0,x1) -> p20(x1,x0) {x0 -> c28, x1 -> f21(c28,c37)}
% 19.23/4.37 === Backtracking. Learning clause 97:3:2:[92.2,61.1]:TopTop: p20(x0,f21(c28,c37)),p10(c34,x1) -> p26(x0,x1)
% 19.23/4.37 === Conflict found: 96:3:2:[92.2,60.1]:TopTop: p20(x0,f21(c28,c35)),p10(c34,x1) -> p26(x0,x1) {x0 -> f21(c28,c35), x1 -> c28}
% 19.23/4.37 === Backtracking. Learning clause 98:2:1:[96.1,6.1]:Top: p10(c34,x0) -> p26(f21(c28,c35),x0)
% 19.23/4.37 === Conflict found: 59:2:2:[30.2,7.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c32, x1 -> f16(c32,f9(f17(c31)))}
% 19.23/4.37 === Backtracking. Learning clause 99:2:0:[59.2,81.1]:: p2(c32,f16(c32,f9(f17(c31)))),p10(c34,c34) ->
% 19.23/4.37 === Conflict found: 78:3:3:[30.2,23.2]:TopTopTop: p2(f9(x0),x1),p2(x0,x2) -> p2(x1,f9(x2)) {x0 -> f11(c28,c28), x1 -> c28, x2 -> f11(f4(c32),c34)}
% 19.23/4.37 === Backtracking. Learning clause 100:4:5:[78.2,46.3]:TopTopTopTopTop: p2(f9(f11(x0,x1)),x2),p10(x1,x3),p3(x0,x4) -> p2(x2,f9(f11(x4,x3)))
% 19.23/4.37 === Backtracking. Learning clause 101:5:6:[36.3,46.3]:TopTopTopTopTopTop: p2(x0,x1),p25(f11(x2,x3),x0),p10(x3,x4),p3(x2,x5) -> p25(f11(x5,x4),x1)
% 19.23/4.37 === Backtracking. Learning clause 102:5:6:[36.1,46.3]:TopTopTopTopTopTop: p25(x0,f11(x1,x2)),p2(x0,x3),p10(x2,x4),p3(x1,x5) -> p25(x3,f11(x5,x4))
% 19.23/4.37 === Backtracking. Learning clause 103:6:4:[30.1,46.3,72.1]:TopTopTopTop: p2(f11(x0,x1),x2),p10(x1,c34),p3(x0,f4(x3)),p25(x3,c36),p25(c32,x3) -> p2(x2,f11(f4(c32),c34))
% 19.23/4.37 === Backtracking. Learning clause 104:2:1:[30.3,94.1]:Top: p2(x0,f11(f4(c32),c34)),p2(x0,f11(f4(c33),c34)) ->
% 19.23/4.37 === Backtracking. Learning clause 105:2:0:[46.3,95.1]:: p10(c34,c34),p3(f4(c32),f4(c36)) ->
% 19.23/4.37 === Clause set with instances from active satisfied. Growing active. New size: 270
% 19.23/4.37 === Restarting.
% 19.23/4.37 === Conflict found: 57:2:2:[26.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c28, x1 -> f8(c29)}
% 19.23/4.37 === Backtracking. Learning clause 106:2:1:[57.2,56.1]:Top: p7(x0,f8(c29)) -> p7(x0,c30)
% 19.23/4.37 === Conflict found: 57:2:2:[26.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c29), x1 -> c30}
% 19.23/4.37 === Backtracking. Learning clause 107:1:0:[57.1,14.1]:: -> p7(c30,f8(c29))
% 19.23/4.37 === Backtracking. Learning clause 108:4:4:[30.3,78.1]:TopTopTopTop: p2(x0,f9(x1)),p2(x0,x2),p2(x1,x3) -> p2(x2,f9(x3))
% 19.23/4.37 === Conflict found: 104:2:1:[30.3,94.1]:Top: p2(x0,f11(f4(c32),c34)),p2(x0,f11(f4(c33),c34)) -> {x0 -> f11(c28,c28)}
% 19.23/4.37 === Backtracking. Learning clause 109:9:7:[104.2,46.3,30.3,103.6,30.3]:TopTopTopTopTopTopTop: p10(x0,c34),p3(x1,f4(c33)),p2(x2,f11(x1,x0)),p10(x3,c34),p3(x4,f4(x5)),p25(x5,c36),p25(c32,x5),p2(x6,f11(x4,x3)),p2(x6,x2) ->
% 19.23/4.37 === Backtracking. Learning clause 110:7:8:[36.2,101.5,59.2]:TopTopTopTopTopTopTopTop: p2(x0,x1),p2(x2,x0),p25(f11(x3,x4),x2),p10(x4,x5),p3(x3,x6),p2(x7,f11(x6,x5)) -> p25(x7,x1)
% 19.23/4.37 === Conflict found: 109:9:7:[104.2,46.3,30.3,103.6,30.3]:TopTopTopTopTopTopTop: p10(x0,c34),p3(x1,f4(c33)),p2(x2,f11(x1,x0)),p10(x3,c34),p3(x4,f4(x5)),p25(x5,c36),p25(c32,x5),p2(x6,f11(x4,x3)),p2(x6,x2) -> {x0 -> c28, x1 -> c28, x2 -> f11(c28,c28), x3 -> c28, x4 -> c28, x5 -> c33, x6 -> f11(c28,c28)}
% 19.23/4.37 === Backtracking. Learning clause 111:5:3:[109.3,7.1]:TopTopTop: p3(x1,f4(c33)),p10(x0,c34),p3(x1,f4(x2)),p25(x2,c36),p25(c32,x2) ->
% 19.23/4.37 === Backtracking. Learning clause 112:2:1:[30.3,95.1]:Top: p2(x0,f11(f4(c32),c34)),p2(x0,f11(f4(c36),c34)) ->
% 19.23/4.37 === Conflict found: 59:2:2:[30.2,7.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f11(f4(c33),c34), x1 -> f11(f4(c32),c34)}
% 19.23/4.37
% 19.23/4.37 SZS status Unsatisfiable
% 19.23/4.37
% 19.23/4.37 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.23/4.37
% 19.23/4.37 SPASS-SCL-FOL Statistics:
% 19.23/4.37 Number of learned clauses: 58
% 19.23/4.37 Number of propagations: 3232
% 19.23/4.37 Number of decisions: 2068
% 19.23/4.37 Number of resolutions: 84
% 19.23/4.37 Number of condensations: 0
% 19.23/4.37 Number of sub resolutions: 0
% 19.23/4.37 Number of input literals (deduplicated): 57
% 19.23/4.37 Number of grows: 6
% 19.23/4.37 Number of considered ground atoms: 270
% 19.23/4.37
% 19.23/4.37 Needed: 0:00:03.82
% 19.23/4.37
%------------------------------------------------------------------------------