%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : KRS007-1 : TPTP v9.2.1. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:26:15 PM UTC 2026
% Result : Satisfiable 0.59s 0.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS007-1 : TPTP v9.2.1. Released v2.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 : n020.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 12:19:36 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.59/0.64 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.64 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.64 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.64 Execution lmodel_grow ended with status: satisfiable
% 0.59/0.64 Used heuristic: lmodel_grow
% 0.59/0.64
% 0.59/0.64 Input Clauses:
% 0.59/0.64
% 0.59/0.64 Predicates: e f s2least c equalish s s1most d r r2least
% 0.59/0.64 Fol Constants: exist
% 0.59/0.64 Fol Functions: u1r2 u1r1 u3r2 u3r1 u4r3 u4r2 u4r1 u6r2 u6r1
% 0.59/0.64 Problem Properties:
% 0.59/0.64 This is a full first-order problem without equality.
% 0.59/0.64
% 0.59/0.64 After reduction: Problem Properties:
% 0.59/0.64 This is a full first-order problem without equality.
% 0.59/0.64
% 0.59/0.64
% 0.59/0.64 Reduced Input Clauses:
% 0.59/0.64
% 0.59/0.64 Most General Atoms: s2least(x0) s(x0,x2) equalish(x1,x2) s1most(x0) e(x0) c(x1) r(x0,x2) d(x2) f(x0) r2least(x0)
% 0.59/0.64
% 0.59/0.64 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: lmodel_grow ===
% 0.59/0.64
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 54
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 61
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 66
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 70
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 75
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 80
% 0.59/0.64 === Backtracking. Learning clause 27:2:1:[11.4,5.2,7.2,6.2]:Top: s1most(x0),s2least(x0) ->
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 87
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 93
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 98
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 103
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 108
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 114
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 122
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 129
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 134
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 137
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 141
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 144
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 150
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 157
% 0.59/0.64 === Backtracking. Learning clause 29:2:1:[13.1,28.0,8.4,12.1,14.2]:Top: -> s2least(x0),s1most(x0)
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 166
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 173
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 179
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 184
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 190
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 196
% 0.59/0.64 === Conflict found: 29:2:1:[13.1,28.0,8.4,12.1,14.2]:Top: -> s2least(x0),s1most(x0) {x0 -> u6r2(u1r2(exist))}
% 0.59/0.64 === Backtracking. Learning clause 30:5:3:[29.1,4.1,10.1,20.2]:TopTopTop: r(x0,x1),r(x0,x2),d(x2) -> d(x1),e(x0)
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 200
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 206
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 211
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 215
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 219
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 224
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 229
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 234
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 239
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 244
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 247
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 251
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 257
% 0.59/0.64 === Clause set with instances from active satisfied. Growing active. New size: 260
% 0.59/0.64
% 0.59/0.64 Linear Model Building succeeded.
% 0.59/0.64 SZS status Satisfiable
% 0.59/0.64
% 0.59/0.64 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.64
% 0.59/0.64 SPASS-SCL-FOL Statistics:
% 0.59/0.64 Number of learned clauses: 3
% 0.59/0.64 Number of propagations: 318
% 0.59/0.64 Number of decisions: 295
% 0.59/0.64 Number of resolutions: 8
% 0.59/0.64 Number of condensations: 1
% 0.59/0.64 Number of sub resolutions: 1
% 0.59/0.64 Number of input literals (deduplicated): 26
% 0.59/0.64 Number of grows: 40
% 0.59/0.64 Number of considered ground atoms: 260
% 0.59/0.64
% 0.59/0.64 Needed: 0:00:00.05
% 0.59/0.64
%------------------------------------------------------------------------------