%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN675-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 : n008.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:09 PM UTC 2026
% Result : Unsatisfiable 63.68s 13.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN675-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n008.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:14 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]
% 63.68/13.28 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/13.28 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/13.28 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/13.28 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/13.28 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/13.28 Execution resolution_1 ended with status: unsatisfiable
% 63.68/13.28 Used heuristic: resolution_1
% 63.68/13.28
% 63.68/13.28 Input Clauses:
% 63.68/13.28
% 63.68/13.28 Predicates: p22 p10 p7 p6 p3 p2 p19 p18 p14 p12 p25 p26 p23 p27 p24
% 63.68/13.28 Fol Constants: c28 c37 c34 c36 c33 c32 c31 c29 c30 c35
% 63.68/13.28 Fol Functions: f9 f8 f20 f5 f4 f17 f16 f11 f21 f13 f15
% 63.68/13.28 Problem Properties:
% 63.68/13.28 This is a full first-order problem without equality.
% 63.68/13.28
% 63.68/13.28 After reduction: Problem Properties:
% 63.68/13.28 This is a full first-order problem without equality.
% 63.68/13.28
% 63.68/13.28
% 63.68/13.28 Reduced Input Clauses:
% 63.68/13.28
% 63.68/13.28 Most General Atoms: p22(x1) p6(x1,x2) p19(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) p18(x4,x5) p23(x5,x3,x1)
% 63.68/13.28
% 63.68/13.28 === Starting SPASS-SCL-FOL A Little Less Naive, considering 54 atoms initially, heuristics mode: resolution_1 ===
% 63.68/13.28
% 63.68/13.28 === Backtracking. Learning clause 56:2:1:[26.2,11.1]:Top: p10(c37,x0) -> p10(x0,c34)
% 63.68/13.28 === Backtracking. Learning clause 57:3:2:[37.2,12.1]:TopTop: p2(c33,x0),p2(c36,x1) -> p25(x1,x0)
% 63.68/13.28 === Backtracking. Learning clause 58:2:1:[27.2,16.1]:Top: p7(f8(c29),x0) -> p7(x0,c30)
% 63.68/13.28 === Backtracking. Learning clause 59:2:1:[30.2,15.1]:Top: p2(c32,x0) -> p2(x0,f9(c31))
% 63.68/13.28 === Backtracking. Learning clause 60:2:2:[27.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 63.68/13.28 === Backtracking. Learning clause 61:2:2:[29.2,5.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 63.68/13.28 === Backtracking. Learning clause 62:2:2:[30.2,6.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 63.68/13.28 === Clause set with instances from active satisfied. Growing active. New size: 124
% 63.68/13.28 === Restarting.
% 63.68/13.28 === Backtracking. Learning clause 63:2:2:[33.2,9.1]:TopTop: p14(x0,x1) -> p14(x1,x0)
% 63.68/13.28 === Backtracking. Learning clause 64:2:2:[49.3,19.1]:TopTop: p2(x0,f16(x0,x1)),p2(x1,f9(f17(c31))) ->
% 63.68/13.28 === Backtracking. Learning clause 65:3:2:[37.3,40.1]:TopTop: p2(x0,x1),p25(f11(f4(c32),c34),x0) -> p25(f16(f11(f4(c36),c34),f9(f17(c31))),x1)
% 63.68/13.28 === Backtracking. Learning clause 66:3:2:[35.2,41.1]:TopTop: p2(f11(f4(f21(c33,f9(f17(c31)))),c35),x0),p2(f11(f4(c33),c35),x1) -> p27(x1,x0)
% 63.68/13.28 === Clause set with instances from active satisfied. Growing active. New size: 167
% 63.68/13.28 === Restarting.
% 63.68/13.28 === Conflict found: 56:2:1:[26.2,11.1]:Top: p10(c37,x0) -> p10(x0,c34) {x0 -> c28}
% 63.68/13.28 === Backtracking. Learning clause 67:3:2:[56.1,26.3]:TopTop: p10(x0,c37),p10(x0,x1) -> p10(x1,c34)
% 63.68/13.28 === Backtracking. Learning clause 68:2:2:[31.2,7.1]:TopTop: p19(x0,x1) -> p19(x1,x0)
% 63.68/13.28 === Conflict found: 62:2:2:[30.2,6.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> c28, x1 -> f11(f4(f21(c33,f9(f17(c31)))),c35)}
% 63.68/13.28 === Backtracking. Learning clause 69:3:2:[62.2,66.1]:TopTop: p2(x0,f11(f4(f21(c33,f9(f17(c31)))),c35)),p2(f11(f4(c33),c35),x1) -> p27(x1,x0)
% 63.68/13.28 === Backtracking. Learning clause 70:4:3:[48.3,66.1]:TopTopTop: p10(c35,x0),p3(f4(f21(c33,f9(f17(c31)))),x1),p2(f11(f4(c33),c35),x2) -> p27(x2,f11(x1,x0))
% 63.68/13.28 === Backtracking. Learning clause 71:2:1:[30.1,40.1,62.1]:Top: p2(f11(f4(c32),c34),x0) -> p2(x0,f16(f11(f4(c36),c34),f9(f17(c31))))
% 63.68/13.28 === Backtracking. Learning clause 72:2:1:[30.1,39.1,62.1]:Top: p2(f11(f4(c32),c34),x0) -> p2(x0,f16(f11(f4(c33),c34),f9(f17(c31))))
% 63.68/13.28 === Backtracking. Learning clause 73:2:0:[48.3,43.1]:: p10(c34,c34),p3(f4(f21(c32,f9(f17(c31)))),f4(c32)) ->
% 63.68/13.28 === Clause set with instances from active satisfied. Growing active. New size: 197
% 63.68/13.28 === Restarting.
% 63.68/13.28 === Conflict found: 64:2:2:[49.3,19.1]:TopTop: p2(x0,f16(x0,x1)),p2(x1,f9(f17(c31))) -> {x0 -> c28, x1 -> f9(c28)}
% 63.68/13.28 === Backtracking. Learning clause 74:2:2:[64.2,24.2]:TopTop: p2(x0,f16(x0,f9(x1))),p2(x1,f17(c31)) ->
% 63.68/13.28 === Conflict found: 61:2:2:[29.2,5.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f4(c32), x1 -> f4(f21(c32,f9(f17(c31))))}
% 63.68/13.28 === Backtracking. Learning clause 75:2:0:[61.2,73.2]:: p3(f4(c32),f4(f21(c32,f9(f17(c31))))),p10(c34,c34) ->
% 63.68/13.28 === Conflict found: 70:4:3:[48.3,66.1]:TopTopTop: p10(c35,x0),p3(f4(f21(c33,f9(f17(c31)))),x1),p2(f11(f4(c33),c35),x2) -> p27(x2,f11(x1,x0)) {x0 -> c28, x1 -> c28, x2 -> f11(f4(c33),c35)}
% 63.68/13.28 === Backtracking. Learning clause 76:3:2:[70.3,6.1]:TopTop: p10(c35,x0),p3(f4(f21(c33,f9(f17(c31)))),x1) -> p27(f11(f4(c33),c35),f11(x1,x0))
% 63.68/13.28 === Backtracking. Learning clause 77:5:4:[37.2,65.3,62.2]:TopTopTopTop: p2(x0,x1),p2(x2,x0),p25(f11(f4(c32),c34),x2),p2(x3,f16(f11(f4(c36),c34),f9(f17(c31)))) -> p25(x3,x1)
% 63.68/13.28 === Backtracking. Learning clause 78:5:6:[35.1,48.3]:TopTopTopTopTopTop: p27(x0,f11(x1,x2)),p2(x0,x3),p10(x2,x4),p3(x1,x5) -> p27(x3,f11(x5,x4))
% 63.68/13.28 === Backtracking. Learning clause 79:7:8:[35.2,78.5]:TopTopTopTopTopTopTopTop: p2(f11(x0,x1),x2),p2(x3,x4),p27(x5,f11(x6,x7)),p2(x5,x3),p10(x7,x1),p3(x6,x0) -> p27(x4,x2)
% 63.68/13.28 === Backtracking. Learning clause 80:3:2:[37.1,40.1]:TopTop: p25(x0,f11(f4(c32),c34)),p2(x0,x1) -> p25(x1,f16(f11(f4(c36),c34),f9(f17(c31))))
% 63.68/13.28 === Backtracking. Learning clause 81:3:2:[35.3,40.1]:TopTop: p2(x0,x1),p27(f11(f4(c32),c34),x0) -> p27(f16(f11(f4(c36),c34),f9(f17(c31))),x1)
% 63.68/13.28 === Conflict found: 79:7:8:[35.2,78.5]:TopTopTopTopTopTopTopTop: p2(f11(x0,x1),x2),p2(x3,x4),p27(x5,f11(x6,x7)),p2(x5,x3),p10(x7,x1),p3(x6,x0) -> p27(x4,x2) {x0 -> f4(c32), x1 -> c34, x2 -> f16(f11(f4(c33),c34),f9(f17(c31))), x3 -> c28, x4 -> c28, x5 -> f16(f11(f4(c33),c34),f9(f17(c31))), x6 -> c28, x7 -> c28}
% 63.68/13.28 === Backtracking. Learning clause 82:10:8:[79.1,39.1,78.5,35.2,62.2]:TopTopTopTopTopTopTopTop: p2(x0,x1),p10(x2,c34),p3(x3,f4(c32)),p27(x4,f11(x5,x6)),p2(x4,f16(f11(f4(c33),c34),f9(f17(c31)))),p10(x6,x2),p3(x5,x3),p2(x1,x7),p2(x0,f16(f11(f4(c33),c34),f9(f17(c31)))) -> p27(x7,x0)
% 63.68/13.28 === Conflict found: 79:7:8:[35.2,78.5]:TopTopTopTopTopTopTopTop: p2(f11(x0,x1),x2),p2(x3,x4),p27(x5,f11(x6,x7)),p2(x5,x3),p10(x7,x1),p3(x6,x0) -> p27(x4,x2) {x0 -> f4(c32), x1 -> c34, x2 -> f16(f11(f4(c33),c34),f9(f17(c31))), x3 -> f17(c28), x4 -> c28, x5 -> c28, x6 -> c28, x7 -> c28}
% 63.68/13.28 === Backtracking. Learning clause 83:6:5:[79.1,39.1]:TopTopTopTopTop: p2(x0,x1),p27(x2,f11(x3,x4)),p2(x2,x0),p10(x4,c34),p3(x3,f4(c32)) -> p27(x1,f16(f11(f4(c33),c34),f9(f17(c31))))
% 63.68/13.28 === Backtracking. Learning clause 84:3:2:[37.1,39.1]:TopTop: p25(x0,f11(f4(c32),c34)),p2(x0,x1) -> p25(x1,f16(f11(f4(c33),c34),f9(f17(c31))))
% 63.68/13.28 === Backtracking. Learning clause 85:3:2:[37.2,42.1]:TopTop: p2(f11(f4(f21(c36,f9(f17(c31)))),c37),x0),p2(f11(f4(c36),c37),x1) -> p25(x1,x0)
% 63.68/13.28 === Conflict found: 72:2:1:[30.1,39.1,62.1]:Top: p2(f11(f4(c32),c34),x0) -> p2(x0,f16(f11(f4(c33),c34),f9(f17(c31)))) {x0 -> f11(f4(f21(c33,f9(f17(c31)))),c35)}
% 63.68/13.28 === Backtracking. Learning clause 86:7:7:[72.2,79.2]:TopTopTopTopTopTopTop: p2(f11(f4(c32),c34),x0),p2(f11(x1,x2),x3),p27(x4,f11(x5,x6)),p2(x4,x0),p10(x6,x2),p3(x5,x1) -> p27(f16(f11(f4(c33),c34),f9(f17(c31))),x3)
% 63.68/13.28 === Clause set with instances from active satisfied. Growing active. New size: 237
% 63.68/13.28 === Restarting.
% 63.68/13.28 === Conflict found: 60:2:2:[27.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> f8(c29), x1 -> c30}
% 63.68/13.28 === Backtracking. Learning clause 87:2:1:[60.1,16.1,27.2]:Top: p7(c30,x0) -> p7(x0,f8(c29))
% 63.68/13.28 === Conflict found: 61:2:2:[29.2,5.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> c28, x1 -> f4(f21(c33,f9(f17(c31))))}
% 63.68/13.28 === Backtracking. Learning clause 88:4:3:[61.2,70.2]:TopTopTop: p3(x0,f4(f21(c33,f9(f17(c31))))),p10(c35,x1),p2(f11(f4(c33),c35),x2) -> p27(x2,f11(x0,x1))
% 63.68/13.28 === Backtracking. Learning clause 89:2:0:[23.2,75.1]:: p2(c32,f21(c32,f9(f17(c31)))),p10(c34,c34) ->
% 63.68/13.28 === Conflict found: 88:4:3:[61.2,70.2]:TopTopTop: p3(x0,f4(f21(c33,f9(f17(c31))))),p10(c35,x1),p2(f11(f4(c33),c35),x2) -> p27(x2,f11(x0,x1)) {x0 -> f4(f21(c33,f9(f17(c31)))), x1 -> c28, x2 -> c28}
% 63.68/13.28 === Backtracking. Learning clause 90:3:2:[88.1,5.1]:TopTop: p10(c35,x0),p2(f11(f4(c33),c35),x1) -> p27(x1,f11(f4(f21(c33,f9(f17(c31)))),x0))
% 63.68/13.28 === Conflict found: 71:2:1:[30.1,40.1,62.1]:Top: p2(f11(f4(c32),c34),x0) -> p2(x0,f16(f11(f4(c36),c34),f9(f17(c31)))) {x0 -> f11(f4(c36),c34)}
% 63.68/13.28 === Backtracking. Learning clause 91:1:0:[71.2,19.1]:: p2(f11(f4(c32),c34),f11(f4(c36),c34)) ->
% 63.68/13.28 === Backtracking. Learning clause 92:4:3:[30.2,72.2,30.2]:TopTopTop: p2(x0,x1),p2(f11(f4(c32),c34),x0),p2(x1,x2) -> p2(x2,f16(f11(f4(c33),c34),f9(f17(c31))))
% 63.68/13.28 === Clause set with instances from active satisfied. Growing active. New size: 248
% 63.68/13.28 === Restarting.
% 63.68/13.28 === Conflict found: 60:2:2:[27.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c28, x1 -> f8(c29)}
% 63.68/13.28 === Backtracking. Learning clause 93:2:1:[60.2,58.1]:Top: p7(x0,f8(c29)) -> p7(x0,c30)
% 63.68/13.28 === Backtracking. Learning clause 94:3:1:[30.3,89.1]:Top: p2(x0,c32),p2(x0,f21(c32,f9(f17(c31)))),p10(c34,c34) ->
% 63.68/13.28 === Backtracking. Learning clause 95:2:0:[48.3,91.1]:: p10(c34,c34),p3(f4(c32),f4(c36)) ->
% 63.68/13.28 === Conflict found: 62:2:2:[30.2,6.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f11(f4(c36),c34), x1 -> f11(f4(c32),c34)}
% 63.68/13.28
% 63.68/13.28 SZS status Unsatisfiable
% 63.68/13.28
% 63.68/13.28 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/13.28
% 63.68/13.28 SPASS-SCL-FOL Statistics:
% 63.68/13.28 Number of learned clauses: 40
% 63.68/13.28 Number of propagations: 1955
% 63.68/13.28 Number of decisions: 1537
% 63.68/13.28 Number of resolutions: 52
% 63.68/13.28 Number of condensations: 0
% 63.68/13.28 Number of sub resolutions: 0
% 63.68/13.28 Number of input literals (deduplicated): 58
% 63.68/13.28 Number of grows: 5
% 63.68/13.28 Number of considered ground atoms: 248
% 63.68/13.28
% 63.68/13.28 Needed: 0:0:12.74
% 63.68/13.28
%------------------------------------------------------------------------------