%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN036-1 : 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 : 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:39:08 PM UTC 2026
% Result : Unsatisfiable 1.23s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN036-1 : TPTP v9.2.1. Released v1.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n013.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:39:42 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]
% 1.23/0.77 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.23/0.77 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.23/0.77 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.23/0.77 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.23/0.77 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.23/0.77 Execution normal ended with status: unsatisfiable
% 1.23/0.77 Used heuristic: normal
% 1.23/0.77
% 1.23/0.77 Input Clauses:
% 1.23/0.77
% 1.23/0.77 Predicates: big_p big_q
% 1.23/0.77 Fol Constants: c6 c7 c8 c9 c10 c1 c2 c3 c4 c5 c11 c16 c17 c18 c19 c20 c12 c13 c14 c15
% 1.23/0.77 Fol Functions: f1 f2 f4 f3
% 1.23/0.77 Problem Properties:
% 1.23/0.77 This is a full first-order problem without equality.
% 1.23/0.77
% 1.23/0.77 After reduction: Problem Properties:
% 1.23/0.77 This is a full first-order problem without equality.
% 1.23/0.77
% 1.23/0.77
% 1.23/0.77 Reduced Input Clauses:
% 1.23/0.77 129:5:3:[6.4,8.0]:TopTopTop: big_p(x0),big_q(c10) -> big_p(x1),big_p(f1(x1)),big_q(x2)
% 1.23/0.77 130:5:3:[22.4,24.2]:TopTopTop: big_p(x0),big_p(f1(x0)),big_q(c10) -> big_p(x1),big_q(x2)
% 1.23/0.77 161:5:2:[151.1,117.2]:TopTop: big_p(x0),big_p(f3(x0)) -> big_q(f4(x1)),big_q(x1),big_p(c19)
% 1.23/0.77 160:5:3:[115.2,113.5]:TopTopTop: big_p(x0),big_p(f3(x0)),big_q(x1) -> big_q(c14),big_p(x2)
% 1.23/0.77 131:5:1:[130.4,30.2]:Top: big_p(x0),big_p(f1(x0)),big_q(c10) -> big_q(c1),big_q(c8)
% 1.23/0.77 133:4:1:[130.4,32.2,131.5,132.3]:Top: big_p(x0),big_p(f1(x0)),big_q(c10) -> big_q(c1)
% 1.23/0.77 134:4:1:[39.1,37.3]:Top: big_p(c3),big_q(x0) -> big_q(c4),big_p(c9)
% 1.23/0.77 135:4:1:[40.1,38.4]:Top: big_p(c3),big_q(c10) -> big_q(c4),big_p(x0)
% 1.23/0.77 136:5:3:[57.2,41.0]:TopTopTop: big_q(x0),big_p(c5) -> big_p(x1),big_q(f2(x2)),big_q(x2)
% 1.23/0.77 137:5:3:[59.3,43.0]:TopTopTop: big_p(c5),big_q(f2(x0)),big_q(x0) -> big_p(x1),big_q(x2)
% 1.23/0.77 139:4:1:[60.4,44.0,137.5,138.4]:Top: big_p(c5),big_q(f2(x0)),big_q(x0) -> big_p(c6)
% 1.23/0.77 140:4:1:[61.2,45.0]:Top: big_p(c5),big_q(x0) -> big_q(c8),big_p(c9)
% 1.23/0.77 141:4:1:[62.2,46.0]:Top: big_p(c5),big_q(c10) -> big_p(x0),big_q(c8)
% 1.23/0.77 142:4:1:[63.2,47.0]:Top: big_p(c5),big_q(c8) -> big_p(c9),big_q(x0)
% 1.23/0.77 144:4:2:[64.3,48.0,141.4,143.2]:TopTop: big_p(c5),big_q(c10) -> big_p(x0),big_q(x1)
% 1.23/0.77 159:4:1:[152.0,103.2,152.0,158.3]:Top: big_q(f4(x0)),big_q(x0) -> big_q(c14),big_p(c19)
% 1.23/0.77 145:5:2:[134.0,53.2]:TopTop: big_p(x0),big_q(x1) -> big_q(c4),big_q(c8),big_p(c9)
% 1.23/0.77 146:4:1:[56.0,54.4]:Top: big_p(x0),big_q(c10) -> big_p(c3),big_q(c4)
% 1.23/0.77 147:4:1:[134.0,55.2]:Top: big_p(x0),big_q(c8) -> big_q(c4),big_p(c9)
% 1.23/0.77 148:5:1:[137.5,60.3]:Top: big_p(c5),big_q(f2(x0)),big_q(x0) -> big_p(c3),big_p(c6)
% 1.23/0.77 149:4:1:[144.5,64.1]:Top: big_p(c5),big_q(c10) -> big_p(c3),big_q(x0)
% 1.23/0.77 157:5:1:[154.1,100.5]:Top: big_q(c16),big_q(c18) -> big_p(x0),big_p(f3(x0)),big_q(c14)
% 1.23/0.77 156:4:1:[100.0,98.4,154.1,155.5]:Top: big_q(c18) -> big_p(x0),big_p(f3(x0)),big_q(c14)
% 1.23/0.77 154:5:3:[99.0,97.5]:TopTopTop: big_q(x0),big_p(x1) -> big_p(x2),big_p(f3(x2)),big_q(c14)
% 1.23/0.77 153:5:1:[151.1,93.2]:Top: big_p(c13) -> big_p(c11),big_q(f4(x0)),big_q(x0),big_p(c19)
% 1.23/0.77 150:5:1:[93.1,77.0]:Top: big_p(c13) -> big_q(c12),big_q(f4(x0)),big_q(x0),big_p(c19)
% 1.23/0.77 152:5:3:[71.0,87.3]:TopTopTop: big_p(x0),big_q(f4(x1)),big_q(x1) -> big_p(c19),big_q(x2)
% 1.23/0.77 151:5:3:[69.0,85.2]:TopTopTop: big_p(x0),big_q(x1) -> big_q(f4(x2)),big_q(x2),big_p(c19)
% 1.23/0.77
% 1.23/0.77 Most General Atoms: big_p(x0) big_q(x2)
% 1.23/0.77
% 1.23/0.77 === Starting SPASS-SCL-FOL A Little Less Naive, considering 31 atoms initially, heuristics mode: normal ===
% 1.23/0.77
% 1.23/0.77 === Backtracking. Learning clause 162:3:2:[49.2,33.1,65.2,65.2,67.2]:TopTop: big_p(c11) -> big_p(x0),big_q(x1)
% 1.23/0.77 === Backtracking. Learning clause 163:4:3:[83.1,81.4]:TopTopTop: big_q(x0),big_p(x1) -> big_q(x2),big_p(c11)
% 1.23/0.77 === Backtracking. Learning clause 164:3:1:[5.3,163.2,163.2]:Top: big_q(x0) -> big_q(c8),big_p(c11)
% 1.23/0.77 === Backtracking. Learning clause 165:2:1:[101.3,164.1,164.1,49.1,49.1,164.1,33.1,164.1,164.1,164.1,162.1]:Top: -> big_q(c8),big_p(x0)
% 1.23/0.77 === Backtracking. Learning clause 166:3:1:[72.4,162.3,139.1,162.3,162.3,162.3]:Top: big_q(f2(x0)),big_p(c11) -> big_p(c6)
% 1.23/0.77 === Backtracking. Learning clause 167:3:2:[88.4,163.3,163.3,163.3,166.2]:TopTop: big_p(x0),big_q(f2(x1)) -> big_p(c6)
% 1.23/0.77 === Conflict found: 163:4:3:[83.1,81.4]:TopTopTop: big_q(x0),big_p(x1) -> big_q(x2),big_p(c11) {x0 -> c8, x1 -> c3, x2 -> f2(c7)}
% 1.23/0.77 === Backtracking. Learning clause 168:3:2:[163.4,162.1,167.2]:TopTop: big_q(x0),big_p(x1) -> big_p(c6)
% 1.23/0.77 === Backtracking. Learning clause 170:2:1:[165.0,169.0,7.3,168.2,168.2]:Top: -> big_q(x0),big_p(c6)
% 1.23/0.77 === Backtracking. Learning clause 171:1:0:[4.2,170.1,168.2,170.1,170.1]:: -> big_p(c6)
% 1.23/0.77 === Backtracking. Learning clause 174:3:2:[162.1,172.0,162.1,173.1,123.4,121.5,162.2,162.2,162.2]:TopTop: big_q(x0),big_p(c11) -> big_q(x1)
% 1.23/0.77 === Conflict found: 163:4:3:[83.1,81.4]:TopTopTop: big_q(x0),big_p(x1) -> big_q(x2),big_p(c11) {x0 -> c20, x1 -> c6, x2 -> c6}
% 1.23/0.77 === Backtracking. Learning clause 176:2:2:[174.1,175.2,163.2,171.1]:TopTop: big_q(x0) -> big_q(x1)
% 1.23/0.77 === Backtracking. Learning clause 178:2:1:[174.0,177.1,25.3,162.2,176.1,162.2,162.2]:Top: big_p(c11) -> big_q(x0)
% 1.23/0.77 === Backtracking. Learning clause 181:3:2:[176.0,179.2,176.0,180.3,33.1,49.2,176.1,25.3]:TopTop: big_p(x0),big_p(f1(x0)) -> big_q(x1)
% 1.23/0.77 === Backtracking. Learning clause 182:1:1:[33.1,49.2,176.1,176.1,181.2,171.1,176.1]:Top: -> big_q(x0)
% 1.23/0.77 === Backtracking. Learning clause 184:1:0:[178.1,183.1,128.2,72.5,72.5,72.5,182.1]:: big_p(c11) ->
% 1.23/0.77 === Backtracking. Learning clause 186:2:1:[184.0,185.2,88.1,182.1]:Top: big_p(x0),big_q(c20) ->
% 1.23/0.77 === Conflict found: 186:2:1:[184.0,185.2,88.1,182.1]:Top: big_p(x0),big_q(c20) -> {x0 -> f1(c6)}
% 1.23/0.77 === Backtracking. Learning clause 187:1:1:[186.2,182.1]:Top: big_p(x0) ->
% 1.23/0.77
% 1.23/0.77 SZS status Unsatisfiable
% 1.23/0.77
% 1.23/0.77 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.23/0.77
% 1.23/0.77 SPASS-SCL-FOL Statistics:
% 1.23/0.77 Number of learned clauses: 17
% 1.23/0.77 Number of propagations: 182
% 1.23/0.77 Number of decisions: 31
% 1.23/0.77 Number of resolutions: 63
% 1.23/0.77 Number of condensations: 139
% 1.23/0.77 Number of sub resolutions: 42
% 1.23/0.77 Number of input literals (deduplicated): 25
% 1.23/0.77 Number of grows: 0
% 1.23/0.77 Number of considered ground atoms: 31
% 1.23/0.77
% 1.23/0.77 Needed: 0:00:00.21
% 1.23/0.77
%------------------------------------------------------------------------------