%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN714-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 : n003.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:11 PM UTC 2026
% Result : Unsatisfiable 0.38s 0.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN714-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.15/0.34 % Computer : n003.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:12 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.38/0.81 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.81 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.81 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.81 Execution resolution_3 ended with status: unsatisfiable
% 0.38/0.81 Used heuristic: resolution_3
% 0.38/0.81
% 0.38/0.81 Input Clauses:
% 0.38/0.81
% 0.38/0.81 Predicates: p48 p47 p10 p7 p5 p42 p40 p36 p33 p32 p30 p3 p28 p26 p24 p23 p2 p19 p18 p16 p15 p51 p53 p49 p52 p50 p57 p45 p46 p54 p55 p56
% 0.38/0.81 Fol Constants: c62 c60 c66 c67 c68 c65 c64 c58 c61 c63 c59
% 0.38/0.81 Fol Functions: f17 f11 f4 f12 f21 f20 f22 f14 f13 f27 f25 f41 f31 f38 f39 f37 f9 f8 f6 f29 f35 f34 f43 f44
% 0.38/0.81 Problem Properties:
% 0.38/0.81 This is a full first-order problem without equality.
% 0.38/0.81
% 0.38/0.81 After reduction: Problem Properties:
% 0.38/0.81 This is a full first-order problem without equality.
% 0.38/0.81
% 0.38/0.81
% 0.38/0.81 Reduced Input Clauses:
% 0.38/0.81
% 0.38/0.81 Most General Atoms: p47(x1) p48(x1) p42(x1,x2) p40(x1,x2) p36(x1,x2) p32(x1,x2) p30(x1,x2) p26(x1,x2) p23(x1,x2) p19(x1,x2) p18(x1,x2) p5(x2,x3) p57(x3,x1) p45(x1,x3) p46(x2,x3) p3(x2,x3) p49(x3,x1) p52(x1,x3) p16(x2,x3) p53(x1,x3) p28(x2,x3) p10(x2,x3) p55(x1,x3) p33(x2,x3) p7(x2,x3) p56(x0,x1) p51(x0,x1) p54(x0,x1) p24(x4,x5) p50(x1,x5,x3) p2(x4,x5) p15(x4,x5)
% 0.38/0.81
% 0.38/0.81 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_3 ===
% 0.38/0.81
% 0.38/0.81 === Backtracking. Learning clause 106:2:2:[45.2,3.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 107:2:2:[49.2,7.1]:TopTop: p40(x0,x1) -> p40(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 108:2:2:[54.2,12.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 109:2:2:[57.2,15.1]:TopTop: p24(x0,x1) -> p24(x1,x0)
% 0.38/0.81 === Clause set with instances from active satisfied. Growing active. New size: 114
% 0.38/0.81 === Restarting.
% 0.38/0.81 === Backtracking. Learning clause 110:3:2:[69.2,22.1]:TopTop: p24(c67,x0),p15(c66,x1) -> p51(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 111:2:1:[62.3,24.1]:Top: p16(x0,f17(c66)),p16(x0,c65) ->
% 0.38/0.81 === Backtracking. Learning clause 112:3:2:[71.2,23.1]:TopTop: p26(c68,x0),p16(f17(c66),x1) -> p53(x0,x1)
% 0.38/0.81 === Backtracking. Learning clause 113:3:2:[73.3,25.1]:TopTop: p5(x0,x1),p55(x0,f11(c62)) -> p55(x1,f11(c60))
% 0.38/0.81 === Backtracking. Learning clause 114:3:2:[67.3,27.1]:TopTop: p46(x0,f12(c62)),p7(x0,x1) -> p46(x1,f12(c60))
% 0.38/0.81 === Backtracking. Learning clause 115:3:2:[68.3,27.1]:TopTop: p3(x0,x1),p49(f12(c62),x0) -> p49(f12(c60),x1)
% 0.38/0.81 === Backtracking. Learning clause 116:3:2:[68.1,27.1]:TopTop: p49(x0,f12(c62)),p3(x0,x1) -> p49(x1,f12(c60))
% 0.38/0.81 === Backtracking. Learning clause 117:2:2:[60.2,18.1]:TopTop: p19(x0,x1) -> p19(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 118:2:2:[62.2,20.1]:TopTop: p16(x0,x1) -> p16(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 119:2:2:[63.2,21.1]:TopTop: p15(x0,x1) -> p15(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 120:3:2:[70.2,28.1]:TopTop: p19(f20(f21(c62,c64)),x0),p15(c66,x1) -> p52(x0,x1)
% 0.38/0.81 === Backtracking. Learning clause 121:2:2:[46.2,4.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 122:4:4:[67.4,75.1]:TopTopTopTop: p46(x0,x1),p7(x0,f8(f9(c58,x2),x3)),p3(x1,f4(f6(c59,c60))) -> p45(x2,c61)
% 0.38/0.81 === Clause set with instances from active satisfied. Growing active. New size: 178
% 0.38/0.81 === Restarting.
% 0.38/0.81 === Backtracking. Learning clause 123:2:2:[47.2,5.1]:TopTop: p5(x0,x1) -> p5(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 124:2:2:[51.2,9.1]:TopTop: p33(x0,x1) -> p33(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 125:2:2:[52.2,10.1]:TopTop: p32(x0,x1) -> p32(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 126:2:2:[55.2,13.1]:TopTop: p28(x0,x1) -> p28(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 127:2:2:[58.2,16.1]:TopTop: p23(x0,x1) -> p23(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 128:2:2:[59.2,17.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 129:2:2:[61.2,19.1]:TopTop: p18(x0,x1) -> p18(x1,x0)
% 0.38/0.81 === Backtracking. Learning clause 130:4:3:[89.5,33.1]:TopTopTop: p15(x0,c66),p2(x1,c60),p24(x2,f25(f27(c59,c68),c67)),p50(x0,x2,x1) ->
% 0.38/0.81 === Clause set with instances from active satisfied. Growing active. New size: 242
% 0.38/0.81 === Restarting.
% 0.38/0.81 === Conflict found: 118:2:2:[62.2,20.1]:TopTop: p16(x0,x1) -> p16(x1,x0) {x0 -> c65, x1 -> f17(c66)}
% 0.38/0.81 === Backtracking. Learning clause 131:1:0:[118.2,24.1]:: p16(c65,f17(c66)) ->
% 0.38/0.81 === Conflict found: 128:2:2:[59.2,17.1]:TopTop: p2(x0,x1) -> p2(x1,x0) {x0 -> f22(c58,c60,c61), x1 -> c62}
% 0.38/0.81 === Backtracking. Learning clause 132:1:0:[128.1,29.1]:: -> p2(c62,f22(c58,c60,c61))
% 0.38/0.81 === Conflict found: 117:2:2:[60.2,18.1]:TopTop: p19(x0,x1) -> p19(x1,x0) {x0 -> c62, x1 -> f20(f21(c62,c64))}
% 0.38/0.81 === Backtracking. Learning clause 133:3:2:[117.2,120.1]:TopTop: p19(x0,f20(f21(c62,c64))),p15(c66,x1) -> p52(x0,x1)
% 0.38/0.81 === Conflict found: 114:3:2:[67.3,27.1]:TopTop: p46(x0,f12(c62)),p7(x0,x1) -> p46(x1,f12(c60)) {x0 -> f8(c62,c62), x1 -> f8(c62,c62)}
% 0.38/0.81 === Backtracking. Learning clause 134:2:1:[114.2,4.1]:Top: p46(x0,f12(c62)) -> p46(x0,f12(c60))
% 0.38/0.81 === Conflict found: 113:3:2:[73.3,25.1]:TopTop: p5(x0,x1),p55(x0,f11(c62)) -> p55(x1,f11(c60)) {x0 -> f9(c62,c62), x1 -> f9(c62,c62)}
% 0.38/0.81 === Backtracking. Learning clause 135:2:1:[113.1,5.1]:Top: p55(x0,f11(c62)) -> p55(x0,f11(c60))
% 0.38/0.81 === Conflict found: 116:3:2:[68.1,27.1]:TopTop: p49(x0,f12(c62)),p3(x0,x1) -> p49(x1,f12(c60)) {x0 -> f13(c62,c62), x1 -> f13(c62,c62)}
% 0.38/0.81 === Backtracking. Learning clause 136:2:1:[116.2,12.1]:Top: p49(x0,f12(c62)) -> p49(x0,f12(c60))
% 0.38/0.81 === Conflict found: 115:3:2:[68.3,27.1]:TopTop: p3(x0,x1),p49(f12(c62),x0) -> p49(f12(c60),x1) {x0 -> f13(c62,c62), x1 -> f13(c62,c62)}
% 0.38/0.81 === Backtracking. Learning clause 137:2:1:[115.1,12.1]:Top: p49(f12(c62),x0) -> p49(f12(c60),x0)
% 0.38/0.81
% 0.38/0.81 SZS status Unsatisfiable
% 0.38/0.81
% 0.38/0.81 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.81
% 0.38/0.81 SPASS-SCL-FOL Statistics:
% 0.38/0.81 Number of learned clauses: 32
% 0.38/0.81 Number of propagations: 1509
% 0.38/0.81 Number of decisions: 1762
% 0.38/0.81 Number of resolutions: 39
% 0.38/0.81 Number of condensations: 0
% 0.38/0.81 Number of sub resolutions: 0
% 0.38/0.81 Number of input literals (deduplicated): 112
% 0.38/0.81 Number of grows: 3
% 0.38/0.81 Number of considered ground atoms: 242
% 0.38/0.81
% 0.38/0.81 Needed: 0:00:00.25
% 0.38/0.81
%------------------------------------------------------------------------------