↑ Up

SPASS-SCL---0.1.1.CSA-Ass.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : SPASS-SCL---0.1.1
% Problem  : LCL637+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp
% Command  : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n008.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Mon Sep  7 01:09:49 PM UTC 2026

% Result   : CounterSatisfiable 0.15s 0.44s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04  % Problem  : LCL637+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06  % Command  : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41  % Computer : n008.cluster.edu
% 0.15/0.41  % Model    : x86_64 x86_64
% 0.15/0.41  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41  % Memory   : 8046.5625MB
% 0.15/0.41  % OS       : Linux 6.8.0-71-generic
% 0.15/0.41  % CPULimit : 300
% 0.15/0.41  % WCLimit  : 300
% 0.15/0.41  % DateTime : Sat Sep  5 01:18:53 UTC 2026
% 0.15/0.41  % CPUTime  : 
% 0.15/0.41  Running /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.44  
% 0.15/0.44  % Input Clauses:
% 0.15/0.44  % 1:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.15/0.44  % 2:2:1:INP:Top: ren1(x0),p2(skf1(x0)) -> 
% 0.15/0.44  % 3:2:1:INP:Top: ren1(x0),p102(skf1(x0)) -> 
% 0.15/0.44  % 4:2:1:INP:Top: ren1(x0) -> p101(skf1(x0))
% 0.15/0.44  % 5:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.15/0.44  % 6:2:1:INP:Top: ren1(x0) -> p2(skf2(x0))
% 0.15/0.44  % 7:2:1:INP:Top: ren1(x0),p102(skf2(x0)) -> 
% 0.15/0.44  % 8:2:1:INP:Top: ren1(x0) -> p101(skf2(x0))
% 0.15/0.44  % 9:5:2:INP:TopTop: ren2(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.15/0.44  % 10:5:2:INP:TopTop: ren2(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.15/0.44  % 11:5:2:INP:TopTop: ren3(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.15/0.44  % 12:5:2:INP:TopTop: ren3(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.15/0.44  % 13:4:1:INP:Top: ren4(x0),p100(x0) -> ren1(x0),p101(x0)
% 0.15/0.44  % 14:3:1:INP:Top: ren4(x0),p101(x0) -> ren2(x0)
% 0.15/0.44  % 15:3:1:INP:Top: ren4(x0),p100(x0) -> ren3(x0)
% 0.15/0.44  % 16:3:1:INP:Top: ren4(x0),p102(x0) -> p101(x0)
% 0.15/0.44  % 17:3:1:INP:Top: ren4(x0),p101(x0) -> p100(x0)
% 0.15/0.44  % 18:2:1:INP:Top: ren5(x0) -> r1(x0,skf3(x0))
% 0.15/0.44  % 19:2:1:INP:Top: ren5(x0),p2(skf3(x0)) -> 
% 0.15/0.44  % 20:2:1:INP:Top: ren5(x0),p102(skf3(x0)) -> 
% 0.15/0.44  % 21:2:1:INP:Top: ren5(x0) -> p101(skf3(x0))
% 0.15/0.44  % 22:2:1:INP:Top: ren5(x0) -> r1(x0,skf4(x0))
% 0.15/0.44  % 23:2:1:INP:Top: ren5(x0) -> p2(skf4(x0))
% 0.15/0.44  % 24:2:1:INP:Top: ren5(x0),p102(skf4(x0)) -> 
% 0.15/0.44  % 25:2:1:INP:Top: ren5(x0) -> p101(skf4(x0))
% 0.15/0.44  % 26:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.15/0.44  % 27:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.15/0.44  % 28:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.15/0.44  % 29:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.15/0.44  % 30:2:1:INP:Top: r1(skc5,x0) -> ren4(x0)
% 0.15/0.44  % 31:3:0:INP:: p100(skc5) -> ren5(skc5),p101(skc5)
% 0.15/0.44  % 32:2:0:INP:: p101(skc5) -> ren6(skc5)
% 0.15/0.44  % 33:2:0:INP:: p100(skc5) -> ren7(skc5)
% 0.15/0.44  % 34:2:0:INP:: p102(skc5) -> p101(skc5)
% 0.15/0.44  % 35:2:0:INP:: p101(skc5) -> p100(skc5)
% 0.15/0.44  % 36:1:0:INP:: p101(skc5) -> 
% 0.15/0.44  % 37:1:0:INP::  -> p100(skc5)
% 0.15/0.44  
% 0.15/0.44  % Predicates: r1 p2 p102 p101 p100 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 
% 0.15/0.44  % Fol Constants: skc5 
% 0.15/0.44  % Fol Functions: skf1 skf2 skf3 skf4 
% 0.15/0.44  % Problem Properties:
% 0.15/0.44  % This is a full first-order problem without equality. The Problem is non-linear. 
% 0.15/0.44  
% 0.15/0.44  
% 0.15/0.44  % Reduced Input Axiom Clauses:
% 0.15/0.44  % 1:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.15/0.44  % 2:2:1:INP:Top: ren1(x0),p2(skf1(x0)) -> 
% 0.15/0.44  % 3:2:1:INP:Top: ren1(x0),p102(skf1(x0)) -> 
% 0.15/0.44  % 4:2:1:INP:Top: ren1(x0) -> p101(skf1(x0))
% 0.15/0.44  % 5:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.15/0.44  % 6:2:1:INP:Top: ren1(x0) -> p2(skf2(x0))
% 0.15/0.44  % 7:2:1:INP:Top: ren1(x0),p102(skf2(x0)) -> 
% 0.15/0.44  % 8:2:1:INP:Top: ren1(x0) -> p101(skf2(x0))
% 0.15/0.44  % 9:5:2:INP:TopTop: ren2(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.15/0.44  % 10:5:2:INP:TopTop: ren2(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.15/0.44  % 11:5:2:INP:TopTop: ren3(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.15/0.44  % 12:5:2:INP:TopTop: ren3(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.15/0.44  % 13:4:1:INP:Top: ren4(x0),p100(x0) -> ren1(x0),p101(x0)
% 0.15/0.44  % 14:3:1:INP:Top: ren4(x0),p101(x0) -> ren2(x0)
% 0.15/0.44  % 15:3:1:INP:Top: ren4(x0),p100(x0) -> ren3(x0)
% 0.15/0.44  % 16:3:1:INP:Top: ren4(x0),p102(x0) -> p101(x0)
% 0.15/0.44  % 17:3:1:INP:Top: ren4(x0),p101(x0) -> p100(x0)
% 0.15/0.44  % 18:2:1:INP:Top: ren5(x0) -> r1(x0,skf3(x0))
% 0.15/0.44  % 19:2:1:INP:Top: ren5(x0),p2(skf3(x0)) -> 
% 0.15/0.44  % 20:2:1:INP:Top: ren5(x0),p102(skf3(x0)) -> 
% 0.15/0.44  % 21:2:1:INP:Top: ren5(x0) -> p101(skf3(x0))
% 0.15/0.44  % 22:2:1:INP:Top: ren5(x0) -> r1(x0,skf4(x0))
% 0.15/0.44  % 23:2:1:INP:Top: ren5(x0) -> p2(skf4(x0))
% 0.15/0.44  % 24:2:1:INP:Top: ren5(x0),p102(skf4(x0)) -> 
% 0.15/0.44  % 25:2:1:INP:Top: ren5(x0) -> p101(skf4(x0))
% 0.15/0.44  % 26:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.15/0.44  % 27:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.15/0.44  % 28:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.15/0.44  % 29:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.15/0.44  
% 0.15/0.44  % Reduced Input Conjecture Clauses:
% 0.15/0.44  % 30:2:1:INP:Top: r1(skc5,x0) -> ren4(x0)
% 0.15/0.44  % 39:1:0:[37.0,31.0,36.0,38.2]::  -> ren5(skc5)
% 0.15/0.44  % 37:1:0:INP::  -> p100(skc5)
% 0.15/0.44  % 40:1:0:[37.0,33.0]::  -> ren7(skc5)
% 0.15/0.44  % 41:1:0:[36.0,34.1]:: p102(skc5) -> 
% 0.15/0.44  % 36:1:0:INP:: p101(skc5) -> 
% 0.15/0.44  
% 0.15/0.44  
% 0.15/0.44  % === Starting SPASS-SCL-FOL A Little Less Naive, considering 49 atoms initially. Used heuristic: lmodel_grow ===
% 0.15/0.44  
% 0.15/0.44  
% 0.15/0.44  
% 0.15/0.44  % Linear Model Building succeeded.
% 0.15/0.44  % SZS status CounterSatisfiable
% 0.15/0.44  
% 0.15/0.44  
% 0.15/0.44  % SZS status CounterSatisfiable
% 0.15/0.44  % Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.44  
% 0.15/0.44  % SPASS-SCL-FOL Statistics:
% 0.15/0.44  % Number of learned clauses: 23
% 0.15/0.44  % Number of propagations: 287
% 0.15/0.44  % Number of decisions: 256
% 0.15/0.44  % Number of resolutions: 31
% 0.15/0.44  % Number of condensations: 0
% 0.15/0.44  % Number of sub resolutions: 12
% 0.15/0.44  
% 0.15/0.44  % Solver is done. Empty clause found
% 0.15/0.44  
% 0.15/0.44  % Needed:       0:00:00.03
% 0.15/0.44  
% 0.15/0.44  % ###
% 0.15/0.44  % ### Pagesize: 8192
% 0.15/0.44  % ### Marksize: 0
% 0.15/0.44  % ### Memory demanded:  1182 KBytes
% 0.15/0.44  % ### Memory freed:     1182 KBytes
% 0.15/0.44  % ### Memory remaining: 0 Bytes
% 0.15/0.44  % ### Pages allocated:  230 Pages
% 0.15/0.44  % ###
%------------------------------------------------------------------------------