%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN094-1.005 : TPTP v9.2.1. Bugfixed v1.2.1.
% 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:16 PM UTC 2026
% Result : Unsatisfiable 0.31s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN094-1.005 : TPTP v9.2.1. Bugfixed v1.2.1.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n004.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 13:40:03 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.31/0.55 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.55 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.55 Execution normal ended with status: unsatisfiable
% 0.31/0.55 Used heuristic: normal
% 0.31/0.55
% 0.31/0.55 Input Clauses:
% 0.31/0.55
% 0.31/0.55 Predicates: u_1 p_0 q_0 u_2 p_1 p_2 u_3 q_1 q_2 u_4 p_3 u_5 q_3 u_6 p_4 u_7 q_4 u_8 p_5 u_9 q_5 u_10 p_6 u_11 q_6 u_12 p_7 u_13 q_7 u_14 p_8 u_15 q_8 u_16 p_9 u_17 q_9 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25 u_26 u_27 u_28 u_29 u_30 u_31 u_32 u_33 u_34 u_35 p_10 u_36 u_37 q_10 u_38 u_39 u_40 u_41
% 0.31/0.55 Fol Constants: a
% 0.31/0.55 Fol Functions:
% 0.31/0.55 Problem Properties:
% 0.31/0.55 This is a propositional problem.
% 0.31/0.55
% 0.31/0.55 After reduction: Problem Properties:
% 0.31/0.55 This is a propositional problem.
% 0.31/0.55
% 0.31/0.55
% 0.31/0.55 Reduced Input Clauses:
% 0.31/0.55 83:2:0:[2.0,1.2]:: p_0,q_0 ->
% 0.31/0.55 84:3:0:[4.0,3.2]:: p_1,p_2 -> p_0
% 0.31/0.55 85:3:0:[6.0,5.2]:: q_1,q_2 -> p_0
% 0.31/0.55 86:3:0:[8.0,7.2]:: p_2,p_3 -> p_1
% 0.31/0.55 87:3:0:[10.0,9.2]:: q_2,q_3 -> p_1
% 0.31/0.55 88:3:0:[12.0,11.2]:: p_3,p_4 -> p_2
% 0.31/0.55 89:3:0:[14.0,13.2]:: q_3,q_4 -> p_2
% 0.31/0.55 90:3:0:[16.0,15.2]:: p_4,p_5 -> p_3
% 0.31/0.55 91:3:0:[18.0,17.2]:: q_4,q_5 -> p_3
% 0.31/0.55 92:3:0:[20.0,19.2]:: p_5,p_6 -> p_4
% 0.31/0.55 93:3:0:[22.0,21.2]:: q_5,q_6 -> p_4
% 0.31/0.55 94:3:0:[24.0,23.2]:: p_6,p_7 -> p_5
% 0.31/0.55 95:3:0:[26.0,25.2]:: q_6,q_7 -> p_5
% 0.31/0.55 96:3:0:[28.0,27.2]:: p_7,p_8 -> p_6
% 0.31/0.55 97:3:0:[30.0,29.2]:: q_7,q_8 -> p_6
% 0.31/0.55 98:3:0:[32.0,31.2]:: p_8,p_9 -> p_7
% 0.31/0.55 99:3:0:[34.0,33.2]:: q_8,q_9 -> p_7
% 0.31/0.55 100:3:0:[36.0,35.2]:: p_1,q_2 -> q_0
% 0.31/0.55 101:3:0:[38.0,37.2]:: q_1,p_2 -> q_0
% 0.31/0.55 102:3:0:[40.0,39.2]:: p_2,q_3 -> q_1
% 0.31/0.55 103:3:0:[42.0,41.2]:: q_2,p_3 -> q_1
% 0.31/0.55 104:3:0:[44.0,43.2]:: p_3,q_4 -> q_2
% 0.31/0.55 105:3:0:[46.0,45.2]:: q_3,p_4 -> q_2
% 0.31/0.55 106:3:0:[48.0,47.2]:: p_4,q_5 -> q_3
% 0.31/0.55 107:3:0:[50.0,49.2]:: q_4,p_5 -> q_3
% 0.31/0.55 108:3:0:[52.0,51.2]:: p_5,q_6 -> q_4
% 0.31/0.55 109:3:0:[54.0,53.2]:: q_5,p_6 -> q_4
% 0.31/0.55 110:3:0:[56.0,55.2]:: p_6,q_7 -> q_5
% 0.31/0.55 111:3:0:[58.0,57.2]:: q_6,p_7 -> q_5
% 0.31/0.55 112:3:0:[60.0,59.2]:: p_7,q_8 -> q_6
% 0.31/0.55 113:3:0:[62.0,61.2]:: q_7,p_8 -> q_6
% 0.31/0.55 114:3:0:[64.0,63.2]:: p_8,q_9 -> q_7
% 0.31/0.55 115:3:0:[66.0,65.2]:: q_8,p_9 -> q_7
% 0.31/0.55 116:2:0:[68.0,67.1]:: p_4 -> p_9
% 0.31/0.55 117:2:0:[70.0,69.1]:: p_5 -> p_10
% 0.31/0.55 118:2:0:[72.0,71.1]:: q_4 -> q_9
% 0.31/0.55 119:2:0:[74.0,73.1]:: q_5 -> q_10
% 0.31/0.55 120:1:0:[76.0,75.0]:: -> p_8
% 0.31/0.55 121:1:0:[78.0,77.0]:: -> p_9
% 0.31/0.55 122:1:0:[80.0,79.0]:: -> q_8
% 0.31/0.55 123:1:0:[82.0,81.0]:: -> q_9
% 0.31/0.55
% 0.31/0.55 Most General Atoms: p_0 q_0 u_1 p_1 p_2 u_2 q_1 q_2 u_3 p_3 u_4 q_3 u_5 p_4 u_6 q_4 u_7 p_5 u_8 q_5 u_9 p_6 u_10 q_6 u_11 p_7 u_12 q_7 u_13 p_8 u_14 q_8 u_15 p_9 u_16 q_9 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25 u_26 u_27 u_28 u_29 u_30 u_31 u_32 u_33 u_34 p_10 u_35 u_36 q_10 u_37 u_38 u_39 u_40 u_41
% 0.31/0.55
% 0.31/0.55 === Starting SPASS-SCL-FOL A Little Less Naive, considering 63 atoms initially, heuristics mode: normal ===
% 0.31/0.55
% 0.31/0.55 === Conflict found: 83:2:0:[2.0,1.2]:: p_0,q_0 -> {}
% 0.31/0.55
% 0.31/0.55 SZS status Unsatisfiable
% 0.31/0.55
% 0.31/0.55 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.55
% 0.31/0.55 SPASS-SCL-FOL Statistics:
% 0.31/0.55 Number of learned clauses: 0
% 0.31/0.55 Number of propagations: 23
% 0.31/0.55 Number of decisions: 0
% 0.31/0.55 Number of resolutions: 16
% 0.31/0.55 Number of condensations: 0
% 0.31/0.55 Number of sub resolutions: 41
% 0.31/0.55 Number of input literals (deduplicated): 63
% 0.31/0.55 Number of grows: 0
% 0.31/0.55 Number of considered ground atoms: 63
% 0.31/0.55
% 0.31/0.55 Needed: 0:00:00.00
% 0.31/0.55
%------------------------------------------------------------------------------