%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN036-4 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:39:08 PM UTC 2026
% Result : Unsatisfiable 0.29s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN036-4 : TPTP v9.2.1. Released v1.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n004.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:39:48 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.29/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.29/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.29/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.29/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.29/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.29/0.57 Execution normal ended with status: unsatisfiable
% 0.29/0.57 Used heuristic: normal
% 0.29/0.57
% 0.29/0.57 Input Clauses:
% 0.29/0.57
% 0.29/0.57 Predicates: p q
% 0.29/0.57 Fol Constants: cx cw
% 0.29/0.57 Fol Functions: fy5 fz5 fz fy
% 0.29/0.57 Problem Properties:
% 0.29/0.57 This is a full first-order problem without equality.
% 0.29/0.57
% 0.29/0.57 After reduction: Problem Properties:
% 0.29/0.57 This is a full first-order problem without equality.
% 0.29/0.57
% 0.29/0.57
% 0.29/0.57 Reduced Input Clauses:
% 0.29/0.57 33:4:2:[3.2,5.0]:TopTop: p(x0),p(fy5(x0)),q(cw) -> q(x1)
% 0.29/0.57 35:3:2:[4.2,6.0,13.2,34.1]:TopTop: p(fy5(x0)),q(x1) -> q(cw)
% 0.29/0.57 36:4:2:[2.3,7.1]:TopTop: p(cx),q(x0),q(fz5(x0)) -> p(x1)
% 0.29/0.57 37:4:2:[1.1,10.2]:TopTop: p(cx) -> p(x0),q(x1),q(fz(x1))
% 0.29/0.57 38:4:3:[35.2,14.3]:TopTopTop: p(x0),q(x1) -> p(x2),q(cw)
% 0.29/0.57 39:4:2:[3.1,15.2]:TopTop: p(x0) -> p(cx),q(x1),q(fz(x1))
% 0.29/0.57 40:4:2:[4.3,16.1]:TopTop: p(x0),q(x1),q(fz5(x1)) -> p(cx)
% 0.29/0.57 41:4:2:[1.0,19.1]:TopTop: q(cw) -> p(x0),p(fy(x0)),q(x1)
% 0.29/0.57 43:3:2:[38.0,20.1,38.0,42.2]:TopTop: q(x0) -> p(fy(x1)),q(cw)
% 0.29/0.57 46:3:1:[38.2,21.0,38.2,44.1,43.3,45.2]:Top: q(x0),q(fz(x0)) -> q(cw)
% 0.29/0.57 47:5:2:[39.1,22.0]:TopTop: p(x0),p(fy(x0)) -> q(cw),q(x1),q(fz(x1))
% 0.29/0.57 49:4:2:[40.4,23.0,35.4,48.3]:TopTop: p(x0),p(fy5(x0)),q(x1),q(fz5(x1)) ->
% 0.29/0.57 50:5:2:[4.3,24.2]:TopTop: p(x0),p(fy(x0)),q(x1),q(fz(x1)) -> p(cx)
% 0.29/0.57 51:5:2:[3.1,29.3]:TopTop: p(x0),p(fy5(x0)) -> p(cx),q(x1),q(fz5(x1))
% 0.29/0.57 52:5:2:[43.4,30.0]:TopTop: q(x0),q(fz(x0)) -> p(cx),p(x1),p(fy(x1))
% 0.29/0.57 55:3:1:[38.0,31.2,38.0,53.3,35.2,54.4]:Top: q(x0),q(fz5(x0)) -> q(cw)
% 0.29/0.57
% 0.29/0.57 Most General Atoms: p(x2) q(x3)
% 0.29/0.57
% 0.29/0.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 44 atoms initially, heuristics mode: normal ===
% 0.29/0.57
% 0.29/0.57 === Backtracking. Learning clause 56:3:1:[3.1,41.3]:Top: q(cw) -> p(cx),q(x0)
% 0.29/0.57 === Backtracking. Learning clause 57:2:0:[32.6,43.1,39.1,39.1,56.1]:: -> q(fz(cw)),p(cx)
% 0.29/0.57 === Conflict found: 40:4:2:[4.3,16.1]:TopTop: p(x0),q(x1),q(fz5(x1)) -> p(cx) {x0 -> fy(cx), x1 -> cw}
% 0.29/0.57 === Backtracking. Learning clause 58:3:2:[40.3,3.4,4.4]:TopTop: p(x0),q(x1) -> p(cx)
% 0.29/0.57 === Conflict found: 52:5:2:[43.4,30.0]:TopTop: q(x0),q(fz(x0)) -> p(cx),p(x1),p(fy(x1)) {x0 -> cw, x1 -> cx}
% 0.29/0.57 === Backtracking. Learning clause 59:1:0:[52.1,43.3,58.1,57.1]:: -> p(cx)
% 0.29/0.57 === Backtracking. Learning clause 60:4:2:[11.4,33.2]:TopTop: p(x0),p(fy(x0)),q(cw) -> q(x1)
% 0.29/0.57 === Conflict found: 36:4:2:[2.3,7.1]:TopTop: p(cx),q(x0),q(fz5(x0)) -> p(x1) {x0 -> cw, x1 -> fy5(cx)}
% 0.29/0.57 === Backtracking. Learning clause 61:2:0:[36.4,49.2,60.4,59.1]:: p(fy(cx)),q(cw) ->
% 0.29/0.57 === Conflict found: 36:4:2:[2.3,7.1]:TopTop: p(cx),q(x0),q(fz5(x0)) -> p(x1) {x0 -> cw, x1 -> fy(cx)}
% 0.29/0.57 === Backtracking. Learning clause 62:1:0:[36.3,1.4,59.1,61.1]:: q(cw) ->
% 0.29/0.57 === Conflict found: 35:3:2:[4.2,6.0,13.2,34.1]:TopTop: p(fy5(x0)),q(x1) -> q(cw) {x0 -> cx, x1 -> fz(cw)}
% 0.29/0.57 === Backtracking. Learning clause 64:1:0:[61.1,63.1,35.1,38.3,47.5,59.1]:: p(fy(cx)) ->
% 0.29/0.57 === Conflict found: 37:4:2:[1.1,10.2]:TopTop: p(cx) -> p(x0),q(x1),q(fz(x1)) {x0 -> fy(cx), x1 -> cw}
% 0.29/0.57
% 0.29/0.57 SZS status Unsatisfiable
% 0.29/0.57
% 0.29/0.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.29/0.57
% 0.29/0.57 SPASS-SCL-FOL Statistics:
% 0.29/0.57 Number of learned clauses: 8
% 0.29/0.57 Number of propagations: 29
% 0.29/0.57 Number of decisions: 9
% 0.29/0.57 Number of resolutions: 24
% 0.29/0.57 Number of condensations: 9
% 0.29/0.57 Number of sub resolutions: 24
% 0.29/0.57 Number of input literals (deduplicated): 8
% 0.29/0.57 Number of grows: 0
% 0.29/0.57 Number of considered ground atoms: 44
% 0.29/0.57
% 0.29/0.57 Needed: 0:00:00.01
% 0.29/0.57
%------------------------------------------------------------------------------