%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : FLD055-1 : TPTP v9.2.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n022.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:21:27 PM UTC 2026
% Result : Unsatisfiable 8.37s 2.26s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.16 % Problem : FLD055-1 : TPTP v9.2.1. Bugfixed v2.1.0.
% 0.09/0.17 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.41 % Computer : n022.cluster.edu
% 0.22/0.41 % Model : x86_64 x86_64
% 0.22/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.41 % Memory : 8042.1875MB
% 0.22/0.41 % OS : Linux 3.10.0-693.el7.x86_64
% 0.22/0.41 % CPULimit : 300
% 0.22/0.41 % WCLimit : 300
% 0.22/0.41 % DateTime : Thu May 7 11:50:07 EDT 2026
% 0.22/0.41 % CPUTime :
% 0.22/0.41 SPASS-SCL-FOL version:
% 0.28/0.52 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 8.37/2.26 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/2.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/2.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/2.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/2.26 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/2.26 Execution lmodel_grow ended with status: unsatisfiable
% 8.37/2.26 Used heuristic: lmodel_grow
% 8.37/2.26
% 8.37/2.26 Input Clauses:
% 8.37/2.26
% 8.37/2.26 Predicates: equalish defined less_or_equal
% 8.37/2.26 Fol Constants: additive_identity multiplicative_identity a b c
% 8.37/2.26 Fol Functions: add additive_inverse multiply multiplicative_inverse
% 8.37/2.26 Problem Properties:
% 8.37/2.26 This is a full first-order problem without equality.
% 8.37/2.26
% 8.37/2.26 After reduction: Problem Properties:
% 8.37/2.26 This is a full first-order problem without equality.
% 8.37/2.26
% 8.37/2.26
% 8.37/2.26 Reduced Input Clauses:
% 8.37/2.26
% 8.37/2.26 Most General Atoms: defined(x2) equalish(x0,x2) less_or_equal(x2,x1)
% 8.37/2.26
% 8.37/2.26 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: lmodel_grow ===
% 8.37/2.26
% 8.37/2.26 === Clause set with instances from active satisfied. Growing active. New size: 67
% 8.37/2.26 === Clause set with instances from active satisfied. Growing active. New size: 75
% 8.37/2.26 === Backtracking. Learning clause 34:3:3:[23.3,22.1]:TopTopTop: equalish(x0,x1),equalish(x1,x2) -> equalish(x2,x0)
% 8.37/2.26 === Clause set with instances from active satisfied. Growing active. New size: 86
% 8.37/2.26 === Conflict found: 34:3:3:[23.3,22.1]:TopTopTop: equalish(x0,x1),equalish(x1,x2) -> equalish(x2,x0) {x0 -> a, x1 -> c, x2 -> c}
% 8.37/2.26 === Backtracking. Learning clause 35:4:3:[34.3,26.2,21.2]:TopTopTop: equalish(x0,x1),less_or_equal(x1,x2),defined(x1) -> less_or_equal(x0,x2)
% 8.37/2.26 === Backtracking. Learning clause 36:1:0:[18.1,30.1,26.1,33.1,22.2]:: equalish(a,c) ->
% 8.37/2.26
% 8.37/2.26 SZS status Unsatisfiable
% 8.37/2.26
% 8.37/2.26 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.37/2.26
% 8.37/2.26 SPASS-SCL-FOL Statistics:
% 8.37/2.26 Number of learned clauses: 3
% 8.37/2.26 Number of propagations: 208
% 8.37/2.26 Number of decisions: 29
% 8.37/2.26 Number of resolutions: 19
% 8.37/2.26 Number of condensations: 0
% 8.37/2.26 Number of sub resolutions: 0
% 8.37/2.26 Number of input literals (deduplicated): 32
% 8.37/2.26 Number of grows: 3
% 8.37/2.26 Number of considered ground atoms: 86
% 8.37/2.26
% 8.37/2.26 Needed: 0:00:01.64
% 8.37/2.26
%------------------------------------------------------------------------------