%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN657-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 : n013.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:07 PM UTC 2026
% Result : Unsatisfiable 4.57s 1.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SYN657-1 : TPTP v9.2.1. Released v2.5.0.
% 0.11/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.35 % Computer : n013.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Thu May 7 13:46:57 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 SPASS-SCL-FOL version:
% 0.17/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 4.57/1.45 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.57/1.45 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.57/1.45 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.57/1.45 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.57/1.45 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.57/1.45 Execution resolution_3 ended with status: unsatisfiable
% 4.57/1.45 Used heuristic: resolution_3
% 4.57/1.45
% 4.57/1.45 Input Clauses:
% 4.57/1.45
% 4.57/1.45 Predicates: p17 p7 p6 p4 p3 p2 p24 p26 p23 p25
% 4.57/1.45 Fol Constants: c32 c31 c35 c34 c28 c33 c27 c29 c30 c36
% 4.57/1.45 Fol Functions: f10 f12 f11 f9 f8 f18 f21 f19 f15 f5 f16 f13 f20 f14 f22
% 4.57/1.45 Problem Properties:
% 4.57/1.45 This is a full first-order problem without equality.
% 4.57/1.45
% 4.57/1.45 After reduction: Problem Properties:
% 4.57/1.45 This is a full first-order problem without equality.
% 4.57/1.45
% 4.57/1.45
% 4.57/1.45 Reduced Input Clauses:
% 4.57/1.45
% 4.57/1.45 Most General Atoms: p3(x1,x2) p6(x2,x3) p23(x1,x3) p4(x2,x3) p26(x1,x3) p17(x1,x3) p25(x2,x3) p24(x1,x3) p7(x2,x3) p2(x4,x5)
% 4.57/1.45
% 4.57/1.45 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_3 ===
% 4.57/1.45
% 4.57/1.45 === Backtracking. Learning clause 51:3:2:[32.3,8.1]:TopTop: p4(c32,x0),p4(c31,x1) -> p26(x0,x1)
% 4.57/1.45 === Backtracking. Learning clause 52:2:1:[25.3,11.1]:Top: p6(x0,c28),p6(x0,f10(c33)) ->
% 4.57/1.45 === Backtracking. Learning clause 53:2:2:[23.2,1.1]:TopTop: p17(x0,x1) -> p17(x1,x0)
% 4.57/1.45 === Backtracking. Learning clause 54:2:2:[25.2,3.1]:TopTop: p6(x0,x1) -> p6(x1,x0)
% 4.57/1.45 === Backtracking. Learning clause 55:2:2:[26.2,4.1]:TopTop: p4(x0,x1) -> p4(x1,x0)
% 4.57/1.45 === Backtracking. Learning clause 56:3:2:[31.3,12.1]:TopTop: p6(f10(f11(f12(c33))),x0),p6(c28,x1) -> p23(x0,x1)
% 4.57/1.45 === Backtracking. Learning clause 57:2:1:[26.2,30.1]:Top: p4(c35,x0) -> p4(x0,f13(c32,f16(f8(c27,f9(c28,c29)),c31)))
% 4.57/1.45 === Clause set with instances from active satisfied. Growing active. New size: 125
% 4.57/1.45 === Restarting.
% 4.57/1.45 === Backtracking. Learning clause 58:3:2:[34.3,7.1]:TopTop: p4(c32,x0),p4(c31,x1) -> p24(x0,x1)
% 4.57/1.45 === Backtracking. Learning clause 59:2:2:[24.2,2.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 4.57/1.45 === Backtracking. Learning clause 60:2:2:[28.2,6.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 4.57/1.45 === Backtracking. Learning clause 61:3:2:[33.1,14.1,53.2]:TopTop: p4(c32,x0),p17(x1,f18(f8(c27,f9(c28,c29)))) -> p25(x0,x1)
% 4.57/1.45 === Backtracking. Learning clause 62:2:0:[41.3,14.1]:: p24(c32,c35),p24(c32,c32) ->
% 4.57/1.45 === Backtracking. Learning clause 63:3:2:[32.1,42.1]:TopTop: p4(x0,x1),p26(f16(f8(c27,f9(c28,c29)),c34),x0) -> p26(f16(f8(c27,f9(c28,c29)),c31),x1)
% 4.57/1.45 === Backtracking. Learning clause 64:3:2:[32.2,42.1]:TopTop: p4(x0,x1),p26(x0,f16(f8(c27,f9(c28,c29)),c34)) -> p26(x1,f16(f8(c27,f9(c28,c29)),c31))
% 4.57/1.45 === Backtracking. Learning clause 65:3:2:[34.1,42.1]:TopTop: p4(x0,x1),p24(f16(f8(c27,f9(c28,c29)),c34),x0) -> p24(f16(f8(c27,f9(c28,c29)),c31),x1)
% 4.57/1.45 === Backtracking. Learning clause 66:3:2:[34.2,42.1]:TopTop: p4(x0,x1),p24(x0,f16(f8(c27,f9(c28,c29)),c34)) -> p24(x1,f16(f8(c27,f9(c28,c29)),c31))
% 4.57/1.45 === Backtracking. Learning clause 67:2:1:[26.2,42.1]:Top: p4(f16(f8(c27,f9(c28,c29)),c34),x0) -> p4(x0,f16(f8(c27,f9(c28,c29)),c31))
% 4.57/1.45 === Backtracking. Learning clause 68:3:2:[33.2,42.1]:TopTop: p25(f16(f8(c27,f9(c28,c29)),c34),x0),p17(x0,x1) -> p25(f16(f8(c27,f9(c28,c29)),c31),x1)
% 4.57/1.45 === Clause set with instances from active satisfied. Growing active. New size: 189
% 4.57/1.45 === Restarting.
% 4.57/1.45 === Backtracking. Learning clause 69:3:3:[25.1,20.2,54.1]:TopTopTop: p6(f10(x0),x1),p6(x0,x2) -> p6(x1,f10(x2))
% 4.57/1.45 === Conflict found: 54:2:2:[25.2,3.1]:TopTop: p6(x0,x1) -> p6(x1,x0) {x0 -> c32, x1 -> f10(f11(f12(c33)))}
% 4.57/1.45 === Backtracking. Learning clause 70:3:2:[54.2,56.1]:TopTop: p6(x0,f10(f11(f12(c33)))),p6(c28,x1) -> p23(x0,x1)
% 4.57/1.45 === Conflict found: 54:2:2:[25.2,3.1]:TopTop: p6(x0,x1) -> p6(x1,x0) {x0 -> f21(f8(c32,f9(c32,c32))), x1 -> c32}
% 4.57/1.45 === Backtracking. Learning clause 71:1:3:[54.1,15.1]:TopTopTop: -> p6(x0,f21(f8(x1,f9(x0,x2))))
% 4.57/1.45 === Backtracking. Learning clause 72:2:1:[31.1,3.1,12.1]:Top: p6(c28,x0) -> p23(f10(f11(f12(c33))),x0)
% 4.57/1.45 === Backtracking. Learning clause 73:2:4:[25.2,15.1]:TopTopTopTop: p6(f21(f8(x0,f9(x1,x2))),x3) -> p6(x3,x1)
% 4.57/1.45 === Conflict found: 55:2:2:[26.2,4.1]:TopTop: p4(x0,x1) -> p4(x1,x0) {x0 -> f5(f8(c27,f9(c28,c29)),c30,c31), x1 -> c32}
% 4.57/1.45 === Backtracking. Learning clause 74:1:0:[55.1,29.1]:: -> p4(c32,f5(f8(c27,f9(c28,c29)),c30,c31))
% 4.57/1.45 === Backtracking. Learning clause 75:2:0:[49.3,44.1]:: p24(f19(f20(c31,c34)),f19(f20(c31,f22(f8(c27,f9(c28,c29)),c31,c34)))) -> p6(f21(f8(c27,f9(c28,c29))),f10(c33))
% 4.57/1.45 === Backtracking. Learning clause 76:2:0:[48.3,44.1]:: -> p6(f21(f8(c27,f9(c28,c29))),f10(c33)),p25(f22(f8(c27,f9(c28,c29)),c31,c34),f18(f8(c27,f9(c28,c29))))
% 4.57/1.45
% 4.57/1.45 SZS status Unsatisfiable
% 4.57/1.45
% 4.57/1.45 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.57/1.45
% 4.57/1.45 SPASS-SCL-FOL Statistics:
% 4.57/1.45 Number of learned clauses: 26
% 4.57/1.45 Number of propagations: 825
% 4.57/1.45 Number of decisions: 1015
% 4.57/1.45 Number of resolutions: 34
% 4.57/1.45 Number of condensations: 0
% 4.57/1.45 Number of sub resolutions: 0
% 4.57/1.45 Number of input literals (deduplicated): 55
% 4.57/1.45 Number of grows: 2
% 4.57/1.45 Number of considered ground atoms: 189
% 4.57/1.45
% 4.57/1.45 Needed: 0:00:00.87
% 4.57/1.45
%------------------------------------------------------------------------------