%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN036-3 : 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 : n006.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.33s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN036-3 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n006.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Thu May 7 13:39:46 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.18/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.33/0.54 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/0.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/0.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/0.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/0.54 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/0.54 Execution normal ended with status: unsatisfiable
% 0.33/0.54 Used heuristic: normal
% 0.33/0.54
% 0.33/0.54 Input Clauses:
% 0.33/0.54
% 0.33/0.54 Predicates: n2 n9 n6 n10 p n8 n7 n5 q n4 n3 n1
% 0.33/0.54 Fol Constants: s8 s7 s6 s4 s3 s2
% 0.33/0.54 Fol Functions: s5 s1
% 0.33/0.54 Problem Properties:
% 0.33/0.54 This is a full first-order problem without equality.
% 0.33/0.54
% 0.33/0.54 After reduction: Problem Properties:
% 0.33/0.54 This is a full first-order problem without equality.
% 0.33/0.54
% 0.33/0.54
% 0.33/0.54 Reduced Input Clauses:
% 0.33/0.54
% 0.33/0.54 Most General Atoms: n2 n9 n6 n10 n8 n7 n5(x0) q(x1) n4 n3 n1(x0) p(x1)
% 0.33/0.54
% 0.33/0.54 === Starting SPASS-SCL-FOL A Little Less Naive, considering 32 atoms initially, heuristics mode: normal ===
% 0.33/0.54
% 0.33/0.54 === Backtracking. Learning clause 37:3:2:[19.1,17.3,29.2,21.2,18.3]:TopTop: n5(x0),q(x1) -> n9
% 0.33/0.54 === Backtracking. Learning clause 38:3:1:[22.2,37.2,30.1,20.1,37.2,1.2,13.2]:Top: n2,n10,n5(x0) ->
% 0.33/0.54 === Backtracking. Learning clause 39:4:0:[15.2,20.2,20.2,38.3,31.3]:: n2,n10,n3,n9 ->
% 0.33/0.54 === Backtracking. Learning clause 41:1:0:[10.0,40.0,16.1,21.1,21.1,38.3,39.3,6.3,14.1,38.3,23.2,34.3,26.3,11.1,12.1]:: -> p(s7)
% 0.33/0.54 === Backtracking. Learning clause 42:3:3:[27.2,28.3]:TopTopTop: n1(x0),p(x1) -> p(x2)
% 0.33/0.54 === Backtracking. Learning clause 44:4:1:[11.1,43.0,9.2,33.2,42.3,24.2,4.1]:Top: p(x0) -> n9,n6,n10
% 0.33/0.54 === Backtracking. Learning clause 47:3:2:[11.1,45.0,21.1,46.2,25.2,10.2,23.1,10.2,35.3,6.1,44.4,14.1,37.1,31.2,20.1,15.2]:TopTop: p(x0),q(x1) -> n5(x1)
% 0.33/0.54 === Backtracking. Learning clause 49:3:2:[11.1,48.0,25.3,23.1,10.2,10.2,35.3,6.1,44.4,14.1,37.1,31.2,16.2,20.1,47.2]:TopTop: n3,p(x0) -> n5(x1)
% 0.33/0.54 === Backtracking. Learning clause 51:5:1:[49.2,50.2,18.2,22.2,49.3,37.2,7.1]:Top: n3,p(x0),n6 -> n2,n10
% 0.33/0.54 === Conflict found: 42:3:3:[27.2,28.3]:TopTopTop: n1(x0),p(x1) -> p(x2) {x0 -> s2, x1 -> s7, x2 -> s8}
% 0.33/0.54 === Backtracking. Learning clause 52:3:2:[42.1,24.2]:TopTop: p(x0),n2 -> p(x1)
% 0.33/0.54 === Backtracking. Learning clause 53:4:1:[33.1,11.2,9.2,52.3,51.4]:Top: n3,p(x0),n6 -> n10
% 0.33/0.54 === Backtracking. Learning clause 54:3:2:[35.1,11.2,10.1]:TopTop: n10,p(x0) -> p(x1)
% 0.33/0.54 === Backtracking. Learning clause 55:1:0:[25.3,23.1,54.3,38.1,54.3,53.4,13.2,49.3,41.1]:: n3 ->
% 0.33/0.54 === Backtracking. Learning clause 56:2:0:[30.2,20.1,7.1,13.2,16.3,21.1,21.1,55.1]:: -> n2,n10
% 0.33/0.54 === Backtracking. Learning clause 57:2:1:[26.3,23.1,54.2,56.2]:Top: -> p(x0),n2
% 0.33/0.54 === Conflict found: 42:3:3:[27.2,28.3]:TopTopTop: n1(x0),p(x1) -> p(x2) {x0 -> s8, x1 -> s7, x2 -> s1(s8)}
% 0.33/0.54 === Backtracking. Learning clause 58:1:1:[42.2,41.1,26.3,52.1,57.2]:Top: -> p(x0)
% 0.33/0.54 === Backtracking. Learning clause 60:1:0:[57.0,59.0,25.3,23.1,58.1]:: -> n2
% 0.33/0.54 === Backtracking. Learning clause 61:2:0:[33.1,11.2,9.2]:: p(s8) -> n10
% 0.33/0.54
% 0.33/0.54 SZS status Unsatisfiable
% 0.33/0.54
% 0.33/0.54 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/0.54
% 0.33/0.54 SPASS-SCL-FOL Statistics:
% 0.33/0.54 Number of learned clauses: 18
% 0.33/0.54 Number of propagations: 234
% 0.33/0.54 Number of decisions: 23
% 0.33/0.54 Number of resolutions: 98
% 0.33/0.54 Number of condensations: 9
% 0.33/0.54 Number of sub resolutions: 7
% 0.33/0.54 Number of input literals (deduplicated): 20
% 0.33/0.54 Number of grows: 0
% 0.33/0.54 Number of considered ground atoms: 32
% 0.33/0.54
% 0.33/0.54 Needed: 0:00:00.01
% 0.33/0.54
%------------------------------------------------------------------------------