%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN578-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 : 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:02 PM UTC 2026
% Result : Unsatisfiable 6.64s 1.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : SYN578-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.37 % Computer : n026.cluster.edu
% 0.20/0.37 % Model : x86_64 x86_64
% 0.20/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.37 % Memory : 8042.1875MB
% 0.20/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.20/0.37 % CPULimit : 300
% 0.20/0.37 % WCLimit : 300
% 0.20/0.37 % DateTime : Thu May 7 13:45:54 EDT 2026
% 0.20/0.38 % CPUTime :
% 0.20/0.38 SPASS-SCL-FOL version:
% 0.20/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 6.64/1.89 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.64/1.89 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.64/1.89 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.64/1.89 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.64/1.89 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.64/1.89 Execution resolution_1 ended with status: unsatisfiable
% 6.64/1.89 Used heuristic: resolution_1
% 6.64/1.89
% 6.64/1.89 Input Clauses:
% 6.64/1.89
% 6.64/1.89 Predicates: p10 p7 p3 p2 p9 p11
% 6.64/1.89 Fol Constants: c12 c13 c14 c15 c16
% 6.64/1.89 Fol Functions: f5 f4 f6 f8
% 6.64/1.89 Problem Properties:
% 6.64/1.89 This is a full first-order problem without equality.
% 6.64/1.89
% 6.64/1.89 After reduction: Problem Properties:
% 6.64/1.89 This is a full first-order problem without equality.
% 6.64/1.89
% 6.64/1.89
% 6.64/1.89 Reduced Input Clauses:
% 6.64/1.89
% 6.64/1.89 Most General Atoms: p7(x1,x2) p2(x1,x2) p10(x1,x3) p11(x2,x3) p3(x2,x3) p9(x1,x3)
% 6.64/1.89
% 6.64/1.89 === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially, heuristics mode: resolution_1 ===
% 6.64/1.89
% 6.64/1.89 === Backtracking. Learning clause 24:3:2:[20.2,5.1]:TopTop: p7(c12,x0),p3(c13,x1) -> p9(x0,x1)
% 6.64/1.89 === Backtracking. Learning clause 25:3:2:[19.1,6.1]:TopTop: p2(c14,x0),p10(c15,x1) -> p11(x0,x1)
% 6.64/1.89 === Backtracking. Learning clause 26:2:1:[18.2,7.1]:Top: p2(c16,x0) -> p2(x0,f5(c14))
% 6.64/1.89 === Backtracking. Learning clause 27:2:2:[18.2,4.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 6.64/1.89 === Backtracking. Learning clause 28:3:3:[20.3,8.1]:TopTopTop: p7(x0,x1),p9(x0,f4(f5(x2))) -> p9(x1,f4(x2))
% 6.64/1.89 === Backtracking. Learning clause 29:2:2:[17.2,8.1]:TopTop: p3(f4(f5(x0)),x1) -> p3(x1,f4(x0))
% 6.64/1.89 === Backtracking. Learning clause 30:3:3:[20.3,9.1]:TopTopTop: p7(x0,x1),p9(x0,f6(f5(x2))) -> p9(x1,f6(x2))
% 6.64/1.89 === Backtracking. Learning clause 31:2:2:[17.2,9.1]:TopTop: p3(f6(f5(x0)),x1) -> p3(x1,f6(x0))
% 6.64/1.89 === Backtracking. Learning clause 32:4:1:[10.1,22.4]:Top: p11(c16,c15),p9(c12,x0) -> p9(f8(x0,c16),c13),p9(f8(x0,c16),x0)
% 6.64/1.89 === Backtracking. Learning clause 33:2:2:[16.2,2.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 6.64/1.89 === Backtracking. Learning clause 34:4:1:[22.3,10.1]:Top: p11(x0,c15),p9(c12,f4(c16)) -> p9(f8(f4(c16),x0),f4(x0)),p9(f8(f4(c16),x0),c13)
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 84
% 6.64/1.89 === Restarting.
% 6.64/1.89 === Backtracking. Learning clause 35:2:2:[17.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 6.64/1.89 === Conflict found: 35:2:2:[17.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> c12, x1 -> f6(f5(c12))}
% 6.64/1.89 === Backtracking. Learning clause 36:2:2:[35.2,31.1]:TopTop: p3(x0,f6(f5(x1))) -> p3(x0,f6(x1))
% 6.64/1.89 === Backtracking. Learning clause 37:4:3:[23.3,22.3,20.4]:TopTopTop: p11(x0,c15),p7(x1,c12),p9(x1,x2),p3(x2,f4(x0)) ->
% 6.64/1.89 === Conflict found: 37:4:3:[23.3,22.3,20.4]:TopTopTop: p11(x0,c15),p7(x1,c12),p9(x1,x2),p3(x2,f4(x0)) -> {x0 -> c12, x1 -> c12, x2 -> f4(c12)}
% 6.64/1.89 === Backtracking. Learning clause 38:3:2:[37.4,3.1]:TopTop: p11(x0,c15),p7(x1,c12),p9(x1,f4(x0)) ->
% 6.64/1.89 === Conflict found: 38:3:2:[37.4,3.1]:TopTop: p11(x0,c15),p7(x1,c12),p9(x1,f4(x0)) -> {x0 -> c16, x1 -> c12}
% 6.64/1.89 === Backtracking. Learning clause 39:3:1:[38.3,11.2]:Top: p11(c16,c15),p7(x0,c12),p9(x0,c13) ->
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 98
% 6.64/1.89 === Restarting.
% 6.64/1.89 === Conflict found: 39:3:1:[38.3,11.2]:Top: p11(c16,c15),p7(x0,c12),p9(x0,c13) -> {x0 -> c12}
% 6.64/1.89 === Backtracking. Learning clause 40:3:0:[39.1,25.3,5.1]:: p7(c12,c12),p2(c14,c16),p10(c15,c15) ->
% 6.64/1.89 === Backtracking. Learning clause 41:5:2:[19.4,39.1,25.3,5.1]:TopTop: p2(x0,c16),p10(x1,c15),p7(c12,c12),p2(c14,x0),p10(c15,x1) ->
% 6.64/1.89 === Backtracking. Learning clause 42:3:3:[19.2,4.1]:TopTopTop: p11(x0,x1),p10(x1,x2) -> p11(x0,x2)
% 6.64/1.89 === Backtracking. Learning clause 43:5:5:[20.4,30.2]:TopTopTopTopTop: p7(x0,x1),p9(x0,x2),p3(x2,f6(f5(x3))),p7(x1,x4) -> p9(x4,f6(x3))
% 6.64/1.89 === Conflict found: 35:2:2:[17.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f4(f5(c12)), x1 -> f4(c12)}
% 6.64/1.89 === Backtracking. Learning clause 44:4:3:[35.1,8.1,37.4,42.3]:TopTopTop: p7(x0,c12),p9(x0,f4(x1)),p11(f5(x1),x2),p10(x2,c15) ->
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 106
% 6.64/1.89 === Restarting.
% 6.64/1.89 === Conflict found: 41:5:2:[19.4,39.1,25.3,5.1]:TopTop: p2(x0,c16),p10(x1,c15),p7(c12,c12),p2(c14,x0),p10(c15,x1) -> {x0 -> c12, x1 -> c12}
% 6.64/1.89 === Backtracking. Learning clause 45:5:2:[41.4,27.2]:TopTop: p2(x0,c16),p10(x1,c15),p7(c12,c12),p10(c15,x1),p2(x0,c14) ->
% 6.64/1.89 === Backtracking. Learning clause 46:5:3:[19.4,39.1]:TopTopTop: p11(x0,x1),p2(x0,c16),p10(x1,c15),p7(x2,c12),p9(x2,c13) ->
% 6.64/1.89 === Backtracking. Learning clause 47:7:5:[23.3,43.5]:TopTopTopTopTop: p11(x0,c15),p9(c12,f6(x1)),p9(f8(f6(x1),x0),f4(x0)),p7(x2,x3),p9(x2,x4),p3(x4,f6(f5(x1))),p7(x3,f8(f6(x1),x0)) ->
% 6.64/1.89 === Conflict found: 36:2:2:[35.2,31.1]:TopTop: p3(x0,f6(f5(x1))) -> p3(x0,f6(x1)) {x0 -> f6(f5(f5(c12))), x1 -> c12}
% 6.64/1.89 === Backtracking. Learning clause 48:1:1:[36.1,9.1]:Top: -> p3(f6(f5(f5(x0))),f6(x0))
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 117
% 6.64/1.89 === Restarting.
% 6.64/1.89 === Backtracking. Learning clause 49:4:3:[20.2,11.2,35.2]:TopTopTop: p7(x0,x1),p9(x0,c13),p3(x2,f4(c16)) -> p9(x1,x2)
% 6.64/1.89 === Backtracking. Learning clause 50:6:6:[19.1,19.4,27.2]:TopTopTopTopTopTop: p10(x0,x1),p11(x2,x3),p2(x2,x4),p10(x3,x0),p2(x5,x4) -> p11(x5,x1)
% 6.64/1.89 === Backtracking. Learning clause 51:5:5:[20.4,28.2]:TopTopTopTopTop: p7(x0,x1),p9(x0,x2),p3(x2,f4(f5(x3))),p7(x1,x4) -> p9(x4,f4(x3))
% 6.64/1.89 === Conflict found: 35:2:2:[17.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f6(f5(f5(c12))), x1 -> f6(c12)}
% 6.64/1.89 === Backtracking. Learning clause 52:2:2:[35.1,48.1,17.1]:TopTop: p3(f6(x0),x1) -> p3(f6(f5(f5(x0))),x1)
% 6.64/1.89 === Backtracking. Learning clause 53:4:5:[16.2,21.3]:TopTopTopTopTop: p7(f8(x0,x1),x2),p2(x1,x3),p3(x0,x4) -> p7(x2,f8(x4,x3))
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 131
% 6.64/1.89 === Restarting.
% 6.64/1.89 === Conflict found: 34:4:1:[22.3,10.1]:Top: p11(x0,c15),p9(c12,f4(c16)) -> p9(f8(f4(c16),x0),f4(x0)),p9(f8(f4(c16),x0),c13) {x0 -> c12}
% 6.64/1.89 === Backtracking. Learning clause 54:6:2:[34.3,44.2]:TopTop: p11(x0,c15),p9(c12,f4(c16)),p7(f8(f4(c16),x0),c12),p11(f5(x0),x1),p10(x1,c15) -> p9(f8(f4(c16),x0),c13)
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 195
% 6.64/1.89 === Backtracking. Learning clause 55:3:3:[17.1,35.2,35.2]:TopTopTop: p3(x0,x1),p3(x2,x1) -> p3(x0,x2)
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 259
% 6.64/1.89 === Backtracking. Learning clause 56:5:6:[20.1,21.3]:TopTopTopTopTopTop: p9(f8(x0,x1),x2),p3(x2,x3),p2(x1,x4),p3(x0,x5) -> p9(f8(x5,x4),x3)
% 6.64/1.89 === Clause set with instances from active satisfied. Growing active. New size: 323
% 6.64/1.89
% 6.64/1.89 SZS status Unsatisfiable
% 6.64/1.89
% 6.64/1.89 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.64/1.89
% 6.64/1.89 SPASS-SCL-FOL Statistics:
% 6.64/1.89 Number of learned clauses: 33
% 6.64/1.89 Number of propagations: 1149
% 6.64/1.89 Number of decisions: 744
% 6.64/1.89 Number of resolutions: 51
% 6.64/1.89 Number of condensations: 0
% 6.64/1.89 Number of sub resolutions: 0
% 6.64/1.89 Number of input literals (deduplicated): 25
% 6.64/1.89 Number of grows: 8
% 6.64/1.89 Number of considered ground atoms: 323
% 6.64/1.89
% 6.64/1.89 Needed: 0:00:01.32
% 6.64/1.89
%------------------------------------------------------------------------------