%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NUM027-1 : TPTP v9.2.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:29:36 PM UTC 2026
% Result : Unsatisfiable 0.69s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM027-1 : TPTP v9.2.1. Bugfixed v4.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n011.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 12:47:18 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.69/0.70 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.69/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.69/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.69/0.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.69/0.70 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.69/0.70 Execution resolution_1 ended with status: unsatisfiable
% 0.69/0.70 Used heuristic: resolution_1
% 0.69/0.70
% 0.69/0.70 Input Clauses:
% 0.69/0.70
% 0.69/0.70 Predicates: equalish less
% 0.69/0.70 Fol Constants: n0 b a c
% 0.69/0.70 Fol Functions: add successor multiply predecessor_of_1st_minus_2nd
% 0.69/0.70 Problem Properties:
% 0.69/0.70 This is a full first-order problem without equality.
% 0.69/0.70
% 0.69/0.70 After reduction: Problem Properties:
% 0.69/0.70 This is a full first-order problem without equality.
% 0.69/0.70
% 0.69/0.70
% 0.69/0.70 Reduced Input Clauses:
% 0.69/0.70
% 0.69/0.70 Most General Atoms: equalish(x0,x2) less(x1,x0)
% 0.69/0.70
% 0.69/0.70 === Starting SPASS-SCL-FOL A Little Less Naive, considering 44 atoms initially, heuristics mode: resolution_1 ===
% 0.69/0.70
% 0.69/0.70 === Backtracking. Learning clause 22:1:0:[11.2,21.1]:: equalish(n0,c) ->
% 0.69/0.70 === Backtracking. Learning clause 23:2:1:[7.3,19.1]:Top: less(x0,a),less(b,x0) ->
% 0.69/0.70 === Backtracking. Learning clause 24:1:1:[11.2,17.1]:Top: equalish(n0,successor(x0)) ->
% 0.69/0.70 === Backtracking. Learning clause 25:1:1:[11.1,1.1]:Top: -> equalish(x0,add(x0,n0))
% 0.69/0.70 === Backtracking. Learning clause 26:1:1:[11.1,3.1]:Top: -> equalish(n0,multiply(x0,n0))
% 0.69/0.70 === Backtracking. Learning clause 27:2:3:[11.2,8.1]:TopTopTop: equalish(x0,add(successor(x1),x2)) -> less(x2,x0)
% 0.69/0.70 === Backtracking. Learning clause 28:1:1:[8.1,1.1]:Top: -> less(n0,successor(x0))
% 0.69/0.70 === Backtracking. Learning clause 29:1:0:[14.1,20.1]:: equalish(multiply(b,c),multiply(a,c)) ->
% 0.69/0.70 === Backtracking. Learning clause 30:2:1:[7.2,20.1]:Top: less(multiply(a,c),x0) -> less(multiply(b,c),x0)
% 0.69/0.70 === Backtracking. Learning clause 31:2:1:[7.1,20.1]:Top: less(x0,multiply(b,c)) -> less(x0,multiply(a,c))
% 0.69/0.70 === Backtracking. Learning clause 32:1:2:[12.2,2.1,24.1]:TopTop: equalish(n0,add(x0,successor(x1))) ->
% 0.69/0.70 === Conflict found: 27:2:3:[11.2,8.1]:TopTopTop: equalish(x0,add(successor(x1),x2)) -> less(x2,x0) {x0 -> add(successor(n0),n0), x1 -> n0, x2 -> n0}
% 0.69/0.70 === Backtracking. Learning clause 33:1:2:[27.1,10.1]:TopTop: -> less(x0,add(successor(x1),x0))
% 0.69/0.70 === Backtracking. Learning clause 34:2:3:[12.2,4.1]:TopTopTop: equalish(x0,multiply(x1,successor(x2))) -> equalish(x0,add(multiply(x1,x2),x1))
% 0.69/0.70 === Backtracking. Learning clause 35:1:2:[8.1,2.1]:TopTop: -> less(successor(x0),successor(add(successor(x1),x0)))
% 0.69/0.70 === Clause set with instances from active satisfied. Growing active. New size: 73
% 0.69/0.70 === Restarting.
% 0.69/0.70 === Backtracking. Learning clause 36:2:3:[7.1,33.1]:TopTopTop: less(x0,x1) -> less(x0,add(successor(x2),x1))
% 0.69/0.70 === Backtracking. Learning clause 37:1:2:[8.1,25.1]:TopTop: -> less(x0,add(add(successor(x1),x0),n0))
% 0.69/0.70 === Clause set with instances from active satisfied. Growing active. New size: 80
% 0.69/0.70 === Restarting.
% 0.69/0.70 === Backtracking. Learning clause 38:1:0:[13.2,29.1]:: equalish(b,a) ->
% 0.69/0.70 === Backtracking. Learning clause 39:1:2:[14.1,37.1]:TopTop: equalish(x0,add(add(successor(x1),x0),n0)) ->
% 0.69/0.70 === Conflict found: 34:2:3:[12.2,4.1]:TopTopTop: equalish(x0,multiply(x1,successor(x2))) -> equalish(x0,add(multiply(x1,x2),x1)) {x0 -> n0, x1 -> successor(n0), x2 -> n0}
% 0.69/0.70 === Backtracking. Learning clause 40:1:2:[34.2,32.1]:TopTop: equalish(n0,multiply(successor(x0),successor(x1))) ->
% 0.69/0.70 === Clause set with instances from active satisfied. Growing active. New size: 81
% 0.69/0.70 === Restarting.
% 0.69/0.70 === Conflict found: 30:2:1:[7.2,20.1]:Top: less(multiply(a,c),x0) -> less(multiply(b,c),x0) {x0 -> add(add(successor(n0),multiply(a,c)),n0)}
% 0.69/0.70 === Backtracking. Learning clause 41:1:1:[30.1,37.1]:Top: -> less(multiply(b,c),add(add(successor(x0),multiply(a,c)),n0))
% 0.69/0.70 === Clause set with instances from active satisfied. Growing active. New size: 84
% 0.69/0.70 === Restarting.
% 0.69/0.70 === Conflict found: 31:2:1:[7.1,20.1]:Top: less(x0,multiply(b,c)) -> less(x0,multiply(a,c)) {x0 -> n0}
% 0.69/0.70 === Backtracking. Learning clause 42:2:1:[31.2,14.1]:Top: less(x0,multiply(b,c)),equalish(x0,multiply(a,c)) ->
% 0.69/0.70 === Backtracking. Learning clause 43:2:1:[12.3,29.1]:Top: equalish(multiply(b,c),x0),equalish(x0,multiply(a,c)) ->
% 0.69/0.70 === Backtracking. Learning clause 44:1:1:[14.1,41.1]:Top: equalish(multiply(b,c),add(add(successor(x0),multiply(a,c)),n0)) ->
% 0.69/0.70 === Clause set with instances from active satisfied. Growing active. New size: 94
% 0.69/0.70 === Restarting.
% 0.69/0.70 === Backtracking. Learning clause 46:3:1:[21.0,45.1,7.1,18.3,20.1,14.1,13.2,15.1]:Top: equalish(b,x0) -> equalish(x0,a),less(x0,a)
% 0.69/0.70 === Conflict found: 34:2:3:[12.2,4.1]:TopTopTop: equalish(x0,multiply(x1,successor(x2))) -> equalish(x0,add(multiply(x1,x2),x1)) {x0 -> add(successor(n0),n0), x1 -> n0, x2 -> n0}
% 0.69/0.70 === Backtracking. Learning clause 47:3:4:[34.2,12.1]:TopTopTopTop: equalish(x0,multiply(x1,successor(x2))),equalish(add(multiply(x1,x2),x1),x3) -> equalish(x0,x3)
% 0.69/0.70 === Backtracking. Learning clause 48:2:3:[12.1,4.1,11.2]:TopTopTop: equalish(x0,add(multiply(x1,x2),x1)) -> equalish(multiply(x1,successor(x2)),x0)
% 0.69/0.70 === Conflict found: 34:2:3:[12.2,4.1]:TopTopTop: equalish(x0,multiply(x1,successor(x2))) -> equalish(x0,add(multiply(x1,x2),x1)) {x0 -> add(successor(n0),n0), x1 -> n0, x2 -> n0}
% 0.69/0.70 === Backtracking. Learning clause 49:2:4:[34.2,8.1]:TopTopTopTop: equalish(add(successor(x0),x1),multiply(x2,successor(x3))) -> less(x1,add(multiply(x2,x3),x2))
% 0.69/0.70 === Conflict found: 43:2:1:[12.3,29.1]:Top: equalish(multiply(b,c),x0),equalish(x0,multiply(a,c)) -> {x0 -> add(successor(predecessor_of_1st_minus_2nd(multiply(a,c),n0)),n0)}
% 0.69/0.70 === Backtracking. Learning clause 50:2:1:[43.2,9.2]:Top: equalish(multiply(b,c),add(successor(predecessor_of_1st_minus_2nd(multiply(a,c),x0)),x0)),less(x0,multiply(a,c)) ->
% 0.69/0.70 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.69/0.70 === Restarting.
% 0.69/0.70 === Conflict found: 46:3:1:[21.0,45.1,7.1,18.3,20.1,14.1,13.2,15.1]:Top: equalish(b,x0) -> equalish(x0,a),less(x0,a) {x0 -> b}
% 0.69/0.70
% 0.69/0.70 SZS status Unsatisfiable
% 0.69/0.70
% 0.69/0.70 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.69/0.70
% 0.69/0.70 SPASS-SCL-FOL Statistics:
% 0.69/0.70 Number of learned clauses: 28
% 0.69/0.70 Number of propagations: 1244
% 0.69/0.70 Number of decisions: 250
% 0.69/0.70 Number of resolutions: 37
% 0.69/0.70 Number of condensations: 0
% 0.69/0.70 Number of sub resolutions: 1
% 0.69/0.70 Number of input literals (deduplicated): 18
% 0.69/0.70 Number of grows: 6
% 0.69/0.70 Number of considered ground atoms: 121
% 0.69/0.70
% 0.69/0.70 Needed: 0:00:00.15
% 0.69/0.70
%------------------------------------------------------------------------------