%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : FLD059-3 : 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 : 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:21:28 PM UTC 2026
% Result : Unsatisfiable 0.82s 0.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : FLD059-3 : TPTP v9.2.1. Bugfixed v2.1.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n004.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 11:51:48 EDT 2026
% 0.15/0.35 % CPUTime :
% 0.15/0.35 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.82/0.73 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.73 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.73 Execution lmodel_grow ended with status: unsatisfiable
% 0.82/0.73 Used heuristic: lmodel_grow
% 0.82/0.73
% 0.82/0.73 Input Clauses:
% 0.82/0.73
% 0.82/0.73 Predicates: sum defined product less_or_equal
% 0.82/0.73 Fol Constants: additive_identity multiplicative_identity a
% 0.82/0.73 Fol Functions: additive_inverse multiplicative_inverse add multiply
% 0.82/0.73 Problem Properties:
% 0.82/0.73 This is a full first-order problem without equality.
% 0.82/0.73
% 0.82/0.73 After reduction: Problem Properties:
% 0.82/0.73 This is a full first-order problem without equality.
% 0.82/0.73
% 0.82/0.73
% 0.82/0.73 Reduced Input Clauses:
% 0.82/0.73
% 0.82/0.73 Most General Atoms: product(x2,x3,x6) defined(x1) sum(x1,x2,x4) less_or_equal(x3,x4)
% 0.82/0.73
% 0.82/0.73 === Starting SPASS-SCL-FOL A Little Less Naive, considering 57 atoms initially, heuristics mode: lmodel_grow ===
% 0.82/0.73
% 0.82/0.73 === Clause set with instances from active satisfied. Growing active. New size: 80
% 0.82/0.73 === Backtracking. Learning clause 30:5:2:[24.3,19.3,18.3]:TopTop: less_or_equal(additive_identity,x0),defined(x0),defined(x1) -> less_or_equal(additive_identity,add(x0,x1)),defined(multiplicative_inverse(x1))
% 0.82/0.73 === Clause set with instances from active satisfied. Growing active. New size: 100
% 0.82/0.73 === Backtracking. Learning clause 31:7:9:[24.4,22.2,1.4]:TopTopTopTopTopTopTopTopTop: less_or_equal(x0,x1),sum(x0,x2,x3),less_or_equal(x4,x3),sum(x1,x5,x6),sum(x5,x7,x2),sum(x6,x7,x8) -> less_or_equal(x4,x8)
% 0.82/0.73 === Conflict found: 31:7:9:[24.4,22.2,1.4]:TopTopTopTopTopTopTopTopTop: less_or_equal(x0,x1),sum(x0,x2,x3),less_or_equal(x4,x3),sum(x1,x5,x6),sum(x5,x7,x2),sum(x6,x7,x8) -> less_or_equal(x4,x8) {x0 -> additive_identity, x1 -> a, x2 -> a, x3 -> a, x4 -> additive_identity, x5 -> additive_identity, x6 -> a, x7 -> a, x8 -> add(a,a)}
% 0.82/0.73
% 0.82/0.73 SZS status Unsatisfiable
% 0.82/0.73
% 0.82/0.73 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.82/0.73
% 0.82/0.73 SPASS-SCL-FOL Statistics:
% 0.82/0.73 Number of learned clauses: 2
% 0.82/0.73 Number of propagations: 122
% 0.82/0.73 Number of decisions: 16
% 0.82/0.73 Number of resolutions: 10
% 0.82/0.73 Number of condensations: 0
% 0.82/0.73 Number of sub resolutions: 0
% 0.82/0.73 Number of input literals (deduplicated): 23
% 0.82/0.73 Number of grows: 2
% 0.82/0.73 Number of considered ground atoms: 100
% 0.82/0.73
% 0.82/0.73 Needed: 0:00:00.13
% 0.82/0.73
%------------------------------------------------------------------------------