%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN620-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 : n023.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:05 PM UTC 2026
% Result : Unsatisfiable 4.29s 1.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : SYN620-1 : TPTP v9.2.1. Released v2.5.0.
% 0.13/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.37 % Computer : n023.cluster.edu
% 0.19/0.37 % Model : x86_64 x86_64
% 0.19/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.37 % Memory : 8042.1875MB
% 0.19/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.37 % CPULimit : 300
% 0.19/0.37 % WCLimit : 300
% 0.19/0.37 % DateTime : Thu May 7 13:47:39 EDT 2026
% 0.19/0.37 % CPUTime :
% 0.19/0.37 SPASS-SCL-FOL version:
% 0.28/0.47 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 4.29/1.90 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.29/1.90 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.29/1.90 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.29/1.90 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.29/1.90 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.29/1.90 Execution resolution_3 ended with status: unsatisfiable
% 4.29/1.90 Used heuristic: resolution_3
% 4.29/1.90
% 4.29/1.90 Input Clauses:
% 4.29/1.90
% 4.29/1.90 Predicates: p10 p5 p3 p2 p11 p18 p19 p21 p20
% 4.29/1.90 Fol Constants: c24 c22 c23 c25 c26 c27
% 4.29/1.90 Fol Functions: f6 f4 f9 f8 f7 f14 f15 f12 f13 f16 f17
% 4.29/1.90 Problem Properties:
% 4.29/1.90 This is a full first-order problem without equality.
% 4.29/1.90
% 4.29/1.90 After reduction: Problem Properties:
% 4.29/1.90 This is a full first-order problem without equality.
% 4.29/1.90
% 4.29/1.90
% 4.29/1.90 Reduced Input Clauses:
% 4.29/1.90
% 4.29/1.90 Most General Atoms: p18(x1) p2(x1,x2) p3(x2,x3) p21(x1,x3) p19(x1,x3) p11(x2,x3) p20(x3,x1) p5(x2,x3) p10(x2,x3)
% 4.29/1.90
% 4.29/1.90 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_3 ===
% 4.29/1.90
% 4.29/1.90 === Backtracking. Learning clause 35:2:1:[21.2,8.1]:Top: p3(f4(c22),x0) -> p3(x0,c23)
% 4.29/1.90 === Backtracking. Learning clause 36:2:2:[19.2,1.1]:TopTop: p10(x0,x1) -> p10(x1,x0)
% 4.29/1.90 === Backtracking. Learning clause 37:2:2:[20.2,2.1]:TopTop: p5(x0,x1) -> p5(x1,x0)
% 4.29/1.90 === Backtracking. Learning clause 38:2:2:[21.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 4.29/1.90 === Backtracking. Learning clause 39:2:2:[23.2,5.1]:TopTop: p11(x0,x1) -> p11(x1,x0)
% 4.29/1.90 === Backtracking. Learning clause 40:2:2:[19.1,24.1,36.1]:TopTop: p10(f13(f6(c22),x0),x1) -> p10(x1,f13(f6(c24),f16(c26,x0)))
% 4.29/1.90 === Backtracking. Learning clause 41:2:1:[19.3,25.1]:Top: p10(x0,f13(f6(c22),f14(f15(f7(c25))))),p10(x0,f14(f15(f7(c25)))) ->
% 4.29/1.90 === Clause set with instances from active satisfied. Growing active. New size: 98
% 4.29/1.90 === Restarting.
% 4.29/1.90 === Conflict found: 38:2:2:[21.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> c24, x1 -> f4(c22)}
% 4.29/1.90 === Backtracking. Learning clause 42:2:1:[38.2,35.1]:Top: p3(x0,f4(c22)) -> p3(x0,c23)
% 4.29/1.90 === Conflict found: 38:2:2:[21.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f4(c22), x1 -> c23}
% 4.29/1.90 === Backtracking. Learning clause 43:1:0:[38.1,8.1]:: -> p3(c23,f4(c22))
% 4.29/1.90 === Backtracking. Learning clause 44:2:1:[21.1,16.2,8.1]:Top: p2(c22,x0) -> p3(f4(x0),c23)
% 4.29/1.90 === Conflict found: 41:2:1:[19.3,25.1]:Top: p10(x0,f13(f6(c22),f14(f15(f7(c25))))),p10(x0,f14(f15(f7(c25)))) -> {x0 -> f13(c24,c24)}
% 4.29/1.90 === Backtracking. Learning clause 45:3:2:[41.1,29.3]:TopTop: p10(f13(x0,x1),f14(f15(f7(c25)))),p10(x1,f14(f15(f7(c25)))),p5(x0,f6(c22)) ->
% 4.29/1.90 === Backtracking. Learning clause 46:4:4:[28.2,32.1,23.3]:TopTopTopTop: p11(f12(f13(f6(c24),x0)),x1),p11(x2,f12(f13(f6(c22),f14(f15(f7(c25)))))),p11(x2,x3) -> p20(x3,x1)
% 4.29/1.90 === Clause set with instances from active satisfied. Growing active. New size: 109
% 4.29/1.90 === Restarting.
% 4.29/1.90 === Conflict found: 38:2:2:[21.2,3.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f4(c24), x1 -> c23}
% 4.29/1.90 === Backtracking. Learning clause 47:2:1:[38.1,44.2]:Top: p2(c22,x0) -> p3(c23,f4(x0))
% 4.29/1.90 === Conflict found: 46:4:4:[28.2,32.1,23.3]:TopTopTopTop: p11(f12(f13(f6(c24),x0)),x1),p11(x2,f12(f13(f6(c22),f14(f15(f7(c25)))))),p11(x2,x3) -> p20(x3,x1) {x0 -> c24, x1 -> f12(f13(f6(c22),c27)), x2 -> f12(c24), x3 -> f12(f13(f6(c22),f14(f15(f7(c25)))))}
% 4.29/1.90 === Backtracking. Learning clause 48:2:2:[46.4,33.1]:TopTop: p11(f12(f13(f6(c24),x0)),f12(f13(f6(c22),c27))),p11(x1,f12(f13(f6(c22),f14(f15(f7(c25)))))) ->
% 4.29/1.90 === Backtracking. Learning clause 49:3:2:[28.4,33.1]:TopTop: p11(x0,f12(f13(f6(c22),c27))),p20(x1,x0),p11(x1,f12(f13(f6(c22),f14(f15(f7(c25)))))) ->
% 4.29/1.90 === Conflict found: 48:2:2:[46.4,33.1]:TopTop: p11(f12(f13(f6(c24),x0)),f12(f13(f6(c22),c27))),p11(x1,f12(f13(f6(c22),f14(f15(f7(c25)))))) -> {x0 -> c24, x1 -> f12(f13(f6(c22),f14(f15(f7(c25)))))}
% 4.29/1.90 === Backtracking. Learning clause 50:1:1:[48.2,5.1]:Top: p11(f12(f13(f6(c24),x0)),f12(f13(f6(c22),c27))) ->
% 4.29/1.90 === Clause set with instances from active satisfied. Growing active. New size: 114
% 4.29/1.90 === Restarting.
% 4.29/1.90 === Backtracking. Learning clause 51:1:1:[18.2,50.1]:Top: p10(f13(f6(c24),x0),f13(f6(c22),c27)) ->
% 4.29/1.90 === Backtracking. Learning clause 52:2:2:[23.3,50.1]:TopTop: p11(x0,f12(f13(f6(c24),x1))),p11(x0,f12(f13(f6(c22),c27))) ->
% 4.29/1.90 === Clause set with instances from active satisfied. Growing active. New size: 120
% 4.29/1.90 === Restarting.
% 4.29/1.90 === Backtracking. Learning clause 53:7:7:[28.1,18.2,28.2,23.3]:TopTopTopTopTopTopTop: p20(x0,f12(x1)),p11(x0,x2),p10(x1,x3),p11(x2,x4),p11(x5,f12(x3)),p11(x5,x6) -> p20(x4,x6)
% 4.29/1.90 === Conflict found: 53:7:7:[28.1,18.2,28.2,23.3]:TopTopTopTopTopTopTop: p20(x0,f12(x1)),p11(x0,x2),p10(x1,x3),p11(x2,x4),p11(x5,f12(x3)),p11(x5,x6) -> p20(x4,x6) {x0 -> c24, x1 -> c24, x2 -> c24, x3 -> f13(f6(c24),c24), x4 -> c24, x5 -> f12(c24), x6 -> f12(f13(f6(c24),c24))}
% 4.29/1.90 === Backtracking. Learning clause 54:5:5:[53.5,18.2]:TopTopTopTopTop: p20(x0,f12(x1)),p11(x0,x2),p10(x1,x3),p11(x2,x4) -> p20(x4,f12(x3))
% 4.29/1.90 === Conflict found: 52:2:2:[23.3,50.1]:TopTop: p11(x0,f12(f13(f6(c24),x1))),p11(x0,f12(f13(f6(c22),c27))) -> {x0 -> f12(c24), x1 -> c24}
% 4.29/1.90 === Backtracking. Learning clause 55:2:2:[52.2,18.2,18.2]:TopTop: p10(x0,f13(f6(c22),c27)),p10(x0,f13(f6(c24),x1)) ->
% 4.29/1.90 === Backtracking. Learning clause 56:2:1:[29.3,51.1,12.2]:Top: p10(x0,c27),p2(c24,c22) ->
% 4.29/1.90 === Backtracking. Learning clause 57:2:2:[22.2,4.1]:TopTop: p2(x0,x1) -> p2(x1,x0)
% 4.29/1.90 === Backtracking. Learning clause 58:2:1:[29.3,51.1]:Top: p10(x0,c27),p5(f6(c24),f6(c22)) ->
% 4.29/1.90 === Conflict found: 49:3:2:[28.4,33.1]:TopTop: p11(x0,f12(f13(f6(c22),c27))),p20(x1,x0),p11(x1,f12(f13(f6(c22),f14(f15(f7(c25)))))) -> {x0 -> f12(f13(f6(c22),c27)), x1 -> c24}
% 4.29/1.90 === Backtracking. Learning clause 59:2:1:[49.1,5.1]:Top: p20(x0,f12(f13(f6(c22),c27))),p11(x0,f12(f13(f6(c22),f14(f15(f7(c25)))))) ->
% 4.29/1.90 === Backtracking. Learning clause 60:2:1:[28.3,5.1,33.1]:Top: p11(x0,f12(f13(f6(c22),c27))),p20(f12(f13(f6(c22),f14(f15(f7(c25))))),x0) ->
% 4.29/1.90 === Clause set with instances from active satisfied. Growing active. New size: 140
% 4.29/1.90 === Restarting.
% 4.29/1.90 === Conflict found: 53:7:7:[28.1,18.2,28.2,23.3]:TopTopTopTopTopTopTop: p20(x0,f12(x1)),p11(x0,x2),p10(x1,x3),p11(x2,x4),p11(x5,f12(x3)),p11(x5,x6) -> p20(x4,x6) {x0 -> c24, x1 -> f13(c24,c24), x2 -> c24, x3 -> f13(c24,c24), x4 -> c24, x5 -> c24, x6 -> c24}
% 4.29/1.90 === Backtracking. Learning clause 61:6:6:[53.3,1.1]:TopTopTopTopTopTop: p20(x0,f12(x1)),p11(x0,x2),p11(x2,x3),p11(x4,f12(x1)),p11(x4,x5) -> p20(x3,x5)
% 4.29/1.90 === Conflict found: 55:2:2:[52.2,18.2,18.2]:TopTop: p10(x0,f13(f6(c22),c27)),p10(x0,f13(f6(c24),x1)) -> {x0 -> f13(c24,c24), x1 -> c24}
% 4.29/1.90 === Backtracking. Learning clause 62:3:3:[55.1,29.3]:TopTopTop: p10(f13(x0,x1),f13(f6(c24),x2)),p10(x1,c27),p5(x0,f6(c22)) ->
% 4.29/1.90 === Clause set with instances from active satisfied. Growing active. New size: 144
% 4.29/1.90 === Restarting.
% 4.29/1.90 === Conflict found: 54:5:5:[53.5,18.2]:TopTopTopTopTop: p20(x0,f12(x1)),p11(x0,x2),p10(x1,x3),p11(x2,x4) -> p20(x4,f12(x3)) {x0 -> c24, x1 -> f13(f6(c22),c24), x2 -> c24, x3 -> f13(f6(c22),c27), x4 -> c24}
% 4.29/1.90 === Backtracking. Learning clause 63:10:11:[54.3,29.3,61.1]:TopTopTopTopTopTopTopTopTopTopTop: p20(x0,f12(f13(x1,x2))),p11(x0,x3),p11(x3,x4),p10(x2,x5),p5(x1,x6),p11(x4,x7),p11(x7,x8),p11(x9,f12(f13(x6,x5))),p11(x9,x10) -> p20(x8,x10)
% 4.29/1.90 === Backtracking. Learning clause 64:4:5:[19.2,29.3]:TopTopTopTopTop: p10(f13(x0,x1),x2),p10(x1,x3),p5(x0,x4) -> p10(x2,f13(x4,x3))
% 4.29/1.90 === Conflict found: 40:2:2:[19.1,24.1,36.1]:TopTop: p10(f13(f6(c22),x0),x1) -> p10(x1,f13(f6(c24),f16(c26,x0))) {x0 -> c24, x1 -> f13(c24,c24)}
% 4.29/1.90 === Backtracking. Learning clause 65:3:3:[40.2,62.1]:TopTopTop: p10(f13(f6(c22),x0),f13(x1,x2)),p10(x2,c27),p5(x1,f6(c22)) ->
% 4.29/1.90 === Conflict found: 62:3:3:[55.1,29.3]:TopTopTop: p10(f13(x0,x1),f13(f6(c24),x2)),p10(x1,c27),p5(x0,f6(c22)) -> {x0 -> f6(c22), x1 -> c24, x2 -> f16(c26,c24)}
% 4.29/1.90 === Backtracking. Learning clause 66:1:1:[62.1,24.1,2.1]:Top: p10(x0,c27) ->
% 4.29/1.90 === Conflict found: 64:4:5:[19.2,29.3]:TopTopTopTopTop: p10(f13(x0,x1),x2),p10(x1,x3),p5(x0,x4) -> p10(x2,f13(x4,x3)) {x0 -> f6(c24), x1 -> c24, x2 -> c24, x3 -> f14(f15(f7(c25))), x4 -> f6(c22)}
% 4.29/1.90 === Backtracking. Learning clause 67:5:4:[64.4,41.1,19.3]:TopTopTopTop: p10(x0,f14(f15(f7(c25)))),p5(x1,f6(c22)),p10(x2,f14(f15(f7(c25)))),p10(x3,f13(x1,x0)),p10(x3,x2) ->
% 4.29/1.90 === Conflict found: 40:2:2:[19.1,24.1,36.1]:TopTop: p10(f13(f6(c22),x0),x1) -> p10(x1,f13(f6(c24),f16(c26,x0))) {x0 -> c24, x1 -> c24}
% 4.29/1.90 === Backtracking. Learning clause 68:2:2:[40.2,55.2]:TopTop: p10(f13(f6(c22),x0),x1),p10(x1,f13(f6(c22),c27)) ->
% 4.29/1.90 === Conflict found: 64:4:5:[19.2,29.3]:TopTopTopTopTop: p10(f13(x0,x1),x2),p10(x1,x3),p5(x0,x4) -> p10(x2,f13(x4,x3)) {x0 -> f6(c24), x1 -> f17(c24,c24), x2 -> c24, x3 -> f14(f15(f7(c25))), x4 -> f6(c22)}
% 4.29/1.90 === Backtracking. Learning clause 69:4:3:[64.4,41.1]:TopTopTop: p10(f13(x0,x1),x2),p10(x1,f14(f15(f7(c25)))),p5(x0,f6(c22)),p10(x2,f14(f15(f7(c25)))) ->
% 4.29/1.90 === Conflict found: 68:2:2:[40.2,55.2]:TopTop: p10(f13(f6(c22),x0),x1),p10(x1,f13(f6(c22),c27)) -> {x0 -> c24, x1 -> f13(f6(c22),c27)}
% 4.29/1.90 === Backtracking. Learning clause 70:1:1:[68.2,1.1]:Top: p10(f13(f6(c22),x0),f13(f6(c22),c27)) ->
% 4.29/1.90 === Conflict found: 70:1:1:[68.2,1.1]:Top: p10(f13(f6(c22),x0),f13(f6(c22),c27)) -> {x0 -> c27}
% 4.29/1.90
% 4.29/1.90 SZS status Unsatisfiable
% 4.29/1.90
% 4.29/1.90 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.29/1.90
% 4.29/1.90 SPASS-SCL-FOL Statistics:
% 4.29/1.90 Number of learned clauses: 36
% 4.29/1.90 Number of propagations: 1433
% 4.29/1.90 Number of decisions: 1002
% 4.29/1.90 Number of resolutions: 48
% 4.29/1.90 Number of condensations: 1
% 4.29/1.90 Number of sub resolutions: 0
% 4.29/1.90 Number of input literals (deduplicated): 37
% 4.29/1.90 Number of grows: 6
% 4.29/1.90 Number of considered ground atoms: 144
% 4.29/1.90
% 4.29/1.90 Needed: 0:00:01.29
% 4.29/1.90
%------------------------------------------------------------------------------