%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : FLD010-1 : TPTP v9.2.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n027.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:20 PM UTC 2026
% Result : Unsatisfiable 18.77s 4.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : FLD010-1 : TPTP v9.2.1. Bugfixed v2.7.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n027.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 11:49:20 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 18.77/4.23 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.77/4.23 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.77/4.23 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.77/4.23 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.77/4.23 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.77/4.23 Execution lmodel_grow ended with status: unsatisfiable
% 18.77/4.23 Used heuristic: lmodel_grow
% 18.77/4.23
% 18.77/4.23 Input Clauses:
% 18.77/4.23
% 18.77/4.23 Predicates: equalish defined less_or_equal
% 18.77/4.23 Fol Constants: additive_identity multiplicative_identity
% 18.77/4.23 Fol Functions: add additive_inverse multiply multiplicative_inverse
% 18.77/4.23 Problem Properties:
% 18.77/4.23 This is a full first-order problem without equality.
% 18.77/4.23
% 18.77/4.23 After reduction: Problem Properties:
% 18.77/4.23 This is a full first-order problem without equality.
% 18.77/4.23
% 18.77/4.23
% 18.77/4.23 Reduced Input Clauses:
% 18.77/4.23
% 18.77/4.23 Most General Atoms: defined(x2) equalish(x0,x2) less_or_equal(x2,x1)
% 18.77/4.23
% 18.77/4.23 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: lmodel_grow ===
% 18.77/4.23
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 61
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 67
% 18.77/4.23 === Backtracking. Learning clause 29:4:4:[26.3,17.2]:TopTopTopTop: less_or_equal(x0,x1),equalish(x0,x2),less_or_equal(x3,x2) -> less_or_equal(x3,x1)
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 76
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 87
% 18.77/4.23 === Backtracking. Learning clause 30:3:3:[22.2,26.2]:TopTopTop: equalish(x0,x1),less_or_equal(x1,x2) -> less_or_equal(x0,x2)
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 92
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 100
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 110
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 121
% 18.77/4.23 === Backtracking. Learning clause 31:5:3:[18.2,13.3]:TopTopTop: defined(x0),defined(x1),defined(x2) -> less_or_equal(x0,multiply(x1,x2)),less_or_equal(multiply(x1,x2),x0)
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 135
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 149
% 18.77/4.23 === Backtracking. Learning clause 32:7:4:[15.3,29.2,18.1]:TopTopTopTop: defined(x0),less_or_equal(x0,x1),less_or_equal(x2,additive_identity),defined(x3) -> less_or_equal(x2,x1),less_or_equal(multiplicative_inverse(x0),x3),less_or_equal(x3,multiplicative_inverse(x0))
% 18.77/4.23 === Backtracking. Learning clause 33:5:4:[23.1,22.2,16.3,30.3]:TopTopTopTop: equalish(x0,x1),less_or_equal(x0,x2),equalish(x2,x3),less_or_equal(x3,x0) -> equalish(x1,x2)
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 168
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 186
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 202
% 18.77/4.23 === Clause set with instances from active satisfied. Growing active. New size: 218
% 18.77/4.23 === Conflict found: 29:4:4:[26.3,17.2]:TopTopTopTop: less_or_equal(x0,x1),equalish(x0,x2),less_or_equal(x3,x2) -> less_or_equal(x3,x1) {x0 -> multiply(multiplicative_identity,multiplicative_inverse(multiplicative_identity)), x1 -> multiplicative_identity, x2 -> multiplicative_inverse(multiplicative_identity), x3 -> multiplicative_inverse(additive_inverse(additive_identity))}
% 18.77/4.23 === Backtracking. Learning clause 34:6:6:[29.1,30.3,30.3]:TopTopTopTopTopTop: equalish(x0,x1),equalish(x0,x2),less_or_equal(x2,x3),equalish(x4,x5),less_or_equal(x5,x1) -> less_or_equal(x4,x3)
% 18.77/4.23 === Conflict found: 34:6:6:[29.1,30.3,30.3]:TopTopTopTopTopTop: equalish(x0,x1),equalish(x0,x2),less_or_equal(x2,x3),equalish(x4,x5),less_or_equal(x5,x1) -> less_or_equal(x4,x3) {x0 -> multiply(multiplicative_identity,multiplicative_inverse(multiplicative_identity)), x1 -> multiplicative_identity, x2 -> multiplicative_inverse(multiplicative_identity), x3 -> multiplicative_inverse(multiplicative_identity), x4 -> multiply(multiplicative_identity,multiplicative_identity), x5 -> multiply(multiplicative_identity,multiplicative_identity)}
% 18.77/4.23
% 18.77/4.23 SZS status Unsatisfiable
% 18.77/4.23
% 18.77/4.23 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.77/4.23
% 18.77/4.23 SPASS-SCL-FOL Statistics:
% 18.77/4.23 Number of learned clauses: 6
% 18.77/4.23 Number of propagations: 504
% 18.77/4.23 Number of decisions: 88
% 18.77/4.23 Number of resolutions: 27
% 18.77/4.23 Number of condensations: 0
% 18.77/4.23 Number of sub resolutions: 0
% 18.77/4.23 Number of input literals (deduplicated): 27
% 18.77/4.23 Number of grows: 14
% 18.77/4.23 Number of considered ground atoms: 218
% 18.77/4.23
% 18.77/4.23 Needed: 0:00:03.69
% 18.77/4.23
%------------------------------------------------------------------------------