%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n029.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:10:07 PM UTC 2026
% Result : Theorem 0.67s 0.98s
% Output : Proof 0.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 15
% Syntax : Number of formulae : 47 ( 7 unt; 12 def)
% Number of atoms : 649 ( 0 equ)
% Maximal formula atoms : 121 ( 13 avg)
% Number of connectives : 1105 ( 503 ~; 320 |; 268 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-1 aty)
% Number of variables : 155 ( 0 sgn 129 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ( ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p6(X1)
& ~ p106(X1)
& p105(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ~ p106(X1)
& p105(X1) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p5(X1)
& ~ p105(X1)
& p104(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ~ p105(X1)
& p104(X1) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p4(X1)
& ~ p104(X1)
& p103(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ~ p104(X1)
& p103(X1) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p3(X1)
& ~ p103(X1)
& p102(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ~ p103(X1)
& p102(X1) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p2(X1)
& ~ p102(X1)
& p101(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ~ p102(X1)
& p101(X1) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p6(X1)
| ~ p105(X1) )
| p6(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ p105(X1) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p5(X1)
| ~ p104(X1) )
| p5(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ p104(X1) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p4(X1)
| ~ p103(X1) )
| p4(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ p103(X1) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p3(X1)
| ~ p102(X1) )
| p3(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ p102(X1) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1)
| ~ p101(X1) )
| p2(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ p101(X1) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1)
| ~ p100(X1) )
| p1(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1)
| ~ p100(X1) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X1)
& p100(X1) ) ),
file('theBenchmark.p',main) ).
% NEGATING CONJECTURE
fof(main_nc,negated_conjecture,
? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ( ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p6(X1)
& ~ p106(X1)
& p105(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ~ p106(X1)
& p105(X1) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p5(X1)
& ~ p105(X1)
& p104(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ~ p105(X1)
& p104(X1) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p4(X1)
& ~ p104(X1)
& p103(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ~ p104(X1)
& p103(X1) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p3(X1)
& ~ p103(X1)
& p102(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ~ p103(X1)
& p102(X1) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p2(X1)
& ~ p102(X1)
& p101(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ~ p102(X1)
& p101(X1) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p6(X1)
| ~ p105(X1) )
| p6(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ p105(X1) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p5(X1)
| ~ p104(X1) )
| p5(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ p104(X1) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p4(X1)
| ~ p103(X1) )
| p4(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ p103(X1) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p3(X1)
| ~ p102(X1) )
| p3(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ p102(X1) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1)
| ~ p101(X1) )
| p2(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ p101(X1) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1)
| ~ p100(X1) )
| p1(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1)
| ~ p100(X1) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X1)
& p100(X1) ) ),
inference(negating_conjecture,[status(cth)],[main]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimTB,negated_conjecture,
? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ ( ! [X3] :
( ~ r1(X1,X3)
| ( ( ( ~ ! [X4] :
( ~ r1(X3,X4)
| ~ ( ~ p6(X4)
& ~ p106(X4)
& p105(X4) ) )
& ~ ! [X5] :
( ~ r1(X3,X5)
| ~ ( p6(X5)
& ~ p106(X5)
& p105(X5) ) ) )
| ~ ( ~ p105(X3)
& p104(X3) ) )
& ( ( ~ ! [X6] :
( ~ r1(X3,X6)
| ~ ( ~ p5(X6)
& ~ p105(X6)
& p104(X6) ) )
& ~ ! [X7] :
( ~ r1(X3,X7)
| ~ ( p5(X7)
& ~ p105(X7)
& p104(X7) ) ) )
| ~ ( ~ p104(X3)
& p103(X3) ) )
& ( ( ~ ! [X8] :
( ~ r1(X3,X8)
| ~ ( ~ p4(X8)
& ~ p104(X8)
& p103(X8) ) )
& ~ ! [X9] :
( ~ r1(X3,X9)
| ~ ( p4(X9)
& ~ p104(X9)
& p103(X9) ) ) )
| ~ ( ~ p103(X3)
& p102(X3) ) )
& ( ( ~ ! [X10] :
( ~ r1(X3,X10)
| ~ ( ~ p3(X10)
& ~ p103(X10)
& p102(X10) ) )
& ~ ! [X11] :
( ~ r1(X3,X11)
| ~ ( p3(X11)
& ~ p103(X11)
& p102(X11) ) ) )
| ~ ( ~ p102(X3)
& p101(X3) ) )
& ( ( ~ ! [X12] :
( ~ r1(X3,X12)
| ~ ( ~ p2(X12)
& ~ p102(X12)
& p101(X12) ) )
& ~ ! [X13] :
( ~ r1(X3,X13)
| ~ ( p2(X13)
& ~ p102(X13)
& p101(X13) ) ) )
| ~ ( ~ p101(X3)
& p100(X3) ) )
& ( ( ( ! [X14] :
( ~ r1(X3,X14)
| ~ p6(X14)
| ~ p105(X14) )
| p6(X3) )
& ( ! [X15] :
( ~ r1(X3,X15)
| p6(X15)
| ~ p105(X15) )
| ~ p6(X3) ) )
| ~ p105(X3) )
& ( ( ( ! [X16] :
( ~ r1(X3,X16)
| ~ p5(X16)
| ~ p104(X16) )
| p5(X3) )
& ( ! [X17] :
( ~ r1(X3,X17)
| p5(X17)
| ~ p104(X17) )
| ~ p5(X3) ) )
| ~ p104(X3) )
& ( ( ( ! [X18] :
( ~ r1(X3,X18)
| ~ p4(X18)
| ~ p103(X18) )
| p4(X3) )
& ( ! [X19] :
( ~ r1(X3,X19)
| p4(X19)
| ~ p103(X19) )
| ~ p4(X3) ) )
| ~ p103(X3) )
& ( ( ( ! [X20] :
( ~ r1(X3,X20)
| ~ p3(X20)
| ~ p102(X20) )
| p3(X3) )
& ( ! [X21] :
( ~ r1(X3,X21)
| p3(X21)
| ~ p102(X21) )
| ~ p3(X3) ) )
| ~ p102(X3) )
& ( ( ( ! [X22] :
( ~ r1(X3,X22)
| ~ p2(X22)
| ~ p101(X22) )
| p2(X3) )
& ( ! [X23] :
( ~ r1(X3,X23)
| p2(X23)
| ~ p101(X23) )
| ~ p2(X3) ) )
| ~ p101(X3) )
& ( ( ( ! [X24] :
( ~ r1(X3,X24)
| ~ p1(X24)
| ~ p100(X24) )
| p1(X3) )
& ( ! [X25] :
( ~ r1(X3,X25)
| p1(X25)
| ~ p100(X25) )
| ~ p1(X3) ) )
| ~ p100(X3) )
& ( p105(X3)
| ~ p106(X3) )
& ( p104(X3)
| ~ p105(X3) )
& ( p103(X3)
| ~ p104(X3) )
& ( p102(X3)
| ~ p103(X3) )
& ( p101(X3)
| ~ p102(X3) )
& ( p100(X3)
| ~ p101(X3) ) ) )
& ~ p101(X1)
& p100(X1) ) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[main_nc])]) ).
% FOF INTRODUCE RENAMING
fof(ren5_defn,definition,
! [X3] :
( ren5(X3)
=> ( ~ ! [X12] :
( ~ r1(X3,X12)
| ~ ( ~ p2(X12)
& ~ p102(X12)
& p101(X12) ) )
& ~ ! [X13] :
( ~ r1(X3,X13)
| ~ ( p2(X13)
& ~ p102(X13)
& p101(X13) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren5])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren5_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren5(X1)
| ( ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ~ p102(X2)
& p101(X2) )
& ? [X3] :
( r1(X1,X3)
& p2(X3)
& ~ p102(X3)
& p101(X3) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren5_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren5_skol,plain,
! [X1] :
( ~ ren5(X1)
| ( r1(X1,skf9(X1))
& ~ p2(skf9(X1))
& ~ p102(skf9(X1))
& p101(skf9(X1))
& r1(X1,skf10(X1))
& p2(skf10(X1))
& ~ p102(skf10(X1))
& p101(skf10(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf9,skf10]),skolemize(X2,skf9(X1)),skolemize(X3,skf10(X1))],[ren5_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_35,plain,
( ~ ren5(X0)
| r1(X0,skf9(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_skol])]) ).
% FOF INTRODUCE RENAMING
fof(ren1_defn,definition,
! [X3] :
( ren1(X3)
=> ( ~ ! [X4] :
( ~ r1(X3,X4)
| ~ ( ~ p6(X4)
& ~ p106(X4)
& p105(X4) ) )
& ~ ! [X5] :
( ~ r1(X3,X5)
| ~ ( p6(X5)
& ~ p106(X5)
& p105(X5) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren1])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren2_defn,definition,
! [X3] :
( ren2(X3)
=> ( ~ ! [X6] :
( ~ r1(X3,X6)
| ~ ( ~ p5(X6)
& ~ p105(X6)
& p104(X6) ) )
& ~ ! [X7] :
( ~ r1(X3,X7)
| ~ ( p5(X7)
& ~ p105(X7)
& p104(X7) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren2])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren3_defn,definition,
! [X3] :
( ren3(X3)
=> ( ~ ! [X8] :
( ~ r1(X3,X8)
| ~ ( ~ p4(X8)
& ~ p104(X8)
& p103(X8) ) )
& ~ ! [X9] :
( ~ r1(X3,X9)
| ~ ( p4(X9)
& ~ p104(X9)
& p103(X9) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren3])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren4_defn,definition,
! [X3] :
( ren4(X3)
=> ( ~ ! [X10] :
( ~ r1(X3,X10)
| ~ ( ~ p3(X10)
& ~ p103(X10)
& p102(X10) ) )
& ~ ! [X11] :
( ~ r1(X3,X11)
| ~ ( p3(X11)
& ~ p103(X11)
& p102(X11) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren4])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren6_defn,definition,
! [X3] :
( ren6(X3)
=> ( ( ! [X14] :
( ~ r1(X3,X14)
| ~ p6(X14)
| ~ p105(X14) )
| p6(X3) )
& ( ! [X15] :
( ~ r1(X3,X15)
| p6(X15)
| ~ p105(X15) )
| ~ p6(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren6])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren7_defn,definition,
! [X3] :
( ren7(X3)
=> ( ( ! [X16] :
( ~ r1(X3,X16)
| ~ p5(X16)
| ~ p104(X16) )
| p5(X3) )
& ( ! [X17] :
( ~ r1(X3,X17)
| p5(X17)
| ~ p104(X17) )
| ~ p5(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren7])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren8_defn,definition,
! [X3] :
( ren8(X3)
=> ( ( ! [X18] :
( ~ r1(X3,X18)
| ~ p4(X18)
| ~ p103(X18) )
| p4(X3) )
& ( ! [X19] :
( ~ r1(X3,X19)
| p4(X19)
| ~ p103(X19) )
| ~ p4(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren8])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren9_defn,definition,
! [X3] :
( ren9(X3)
=> ( ( ! [X20] :
( ~ r1(X3,X20)
| ~ p3(X20)
| ~ p102(X20) )
| p3(X3) )
& ( ! [X21] :
( ~ r1(X3,X21)
| p3(X21)
| ~ p102(X21) )
| ~ p3(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren9])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren10_defn,definition,
! [X3] :
( ren10(X3)
=> ( ( ! [X22] :
( ~ r1(X3,X22)
| ~ p2(X22)
| ~ p101(X22) )
| p2(X3) )
& ( ! [X23] :
( ~ r1(X3,X23)
| p2(X23)
| ~ p101(X23) )
| ~ p2(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren10])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren11_defn,definition,
! [X3] :
( ren11(X3)
=> ( ( ! [X24] :
( ~ r1(X3,X24)
| ~ p1(X24)
| ~ p100(X24) )
| p1(X3) )
& ( ! [X25] :
( ~ r1(X3,X25)
| p1(X25)
| ~ p100(X25) )
| ~ p1(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren11])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren12_defn,definition,
! [X3] :
( ren12(X3)
=> ( ( ren1(X3)
| ~ ( ~ p105(X3)
& p104(X3) ) )
& ( ren2(X3)
| ~ ( ~ p104(X3)
& p103(X3) ) )
& ( ren3(X3)
| ~ ( ~ p103(X3)
& p102(X3) ) )
& ( ren4(X3)
| ~ ( ~ p102(X3)
& p101(X3) ) )
& ( ren5(X3)
| ~ ( ~ p101(X3)
& p100(X3) ) )
& ( ren6(X3)
| ~ p105(X3) )
& ( ren7(X3)
| ~ p104(X3) )
& ( ren8(X3)
| ~ p103(X3) )
& ( ren9(X3)
| ~ p102(X3) )
& ( ren10(X3)
| ~ p101(X3) )
& ( ren11(X3)
| ~ p100(X3) )
& ( p105(X3)
| ~ p106(X3) )
& ( p104(X3)
| ~ p105(X3) )
& ( p103(X3)
| ~ p104(X3) )
& ( p102(X3)
| ~ p103(X3) )
& ( p101(X3)
| ~ p102(X3) )
& ( p100(X3)
| ~ p101(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren12])],[main_nc_elimTB]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ ( ! [X3] :
( ~ r1(X1,X3)
| ren12(X3) )
& ~ p101(X1)
& p100(X1) ) ),
inference(renaming,[status(esa)],[main_nc_elimTB,ren1_defn,ren2_defn,ren3_defn,ren4_defn,ren5_defn,ren6_defn,ren7_defn,ren8_defn,ren9_defn,ren10_defn,ren11_defn,ren12_defn]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ! [X3] :
( ~ r1(X1,X3)
| ren12(X3) )
& ~ p101(X1)
& p100(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( ! [X2] :
( ~ r1(skc11,X2)
| p3(X2) )
& ! [X3] :
( ~ r1(skc11,X3)
| ren12(X3) )
& ~ p101(skc11)
& p100(skc11) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc11]),skolemize(X1,skc11)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_72,plain,
( ~ r1(skc11,X0)
| p3(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FILE RECORD
fof(transitivity,axiom,
! [X1,X2,X3] :
( ( r1(X1,X2)
& r1(X2,X3) )
=> r1(X1,X3) ),
file('theBenchmark.p',transitivity) ).
% FOF SIMPLE INFERENCE
fof(transitivity_elimTB,axiom,
! [X1,X2,X3] :
( ( r1(X1,X2)
& r1(X2,X3) )
=> r1(X1,X3) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[transitivity])]) ).
% FOF SIMPLE INFERENCE
fof(transitivity_elimImpEquivPushNegMiniScope,axiom,
! [X1,X2,X3] :
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| r1(X1,X3) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[transitivity_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_2,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X0,X2) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[transitivity_elimImpEquivPushNegMiniScope])]) ).
% FOF SIMPLE INFERENCE
fof(ren4_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren4(X1)
| ( ? [X2] :
( r1(X1,X2)
& ~ p3(X2)
& ~ p103(X2)
& p102(X2) )
& ? [X3] :
( r1(X1,X3)
& p3(X3)
& ~ p103(X3)
& p102(X3) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren4_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren4_skol,plain,
! [X1] :
( ~ ren4(X1)
| ( r1(X1,skf7(X1))
& ~ p3(skf7(X1))
& ~ p103(skf7(X1))
& p102(skf7(X1))
& r1(X1,skf8(X1))
& p3(skf8(X1))
& ~ p103(skf8(X1))
& p102(skf8(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf7,skf8]),skolemize(X2,skf7(X1)),skolemize(X3,skf8(X1))],[ren4_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_28,plain,
( ~ ren4(X0)
| ~ p3(skf7(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren4_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_137,plain,
( ~ r1(skc11,X0)
| ~ r1(X0,skf7(X1))
| ~ ren4(X1) ),
inference(resolution,[status(thm)],[c_72,c_2,c_28]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_37,plain,
( ~ ren5(X0)
| ~ p102(skf9(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_skol])]) ).
% FOF SIMPLE INFERENCE
fof(ren12_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren12(X1)
| ( ( ren1(X1)
| p105(X1)
| ~ p104(X1) )
& ( ren2(X1)
| p104(X1)
| ~ p103(X1) )
& ( ren3(X1)
| p103(X1)
| ~ p102(X1) )
& ( ren4(X1)
| p102(X1)
| ~ p101(X1) )
& ( ren5(X1)
| p101(X1)
| ~ p100(X1) )
& ( ren6(X1)
| ~ p105(X1) )
& ( ren7(X1)
| ~ p104(X1) )
& ( ren8(X1)
| ~ p103(X1) )
& ( ren9(X1)
| ~ p102(X1) )
& ( ren10(X1)
| ~ p101(X1) )
& ( ren11(X1)
| ~ p100(X1) )
& ( p105(X1)
| ~ p106(X1) )
& ( p104(X1)
| ~ p105(X1) )
& ( p103(X1)
| ~ p104(X1) )
& ( p102(X1)
| ~ p103(X1) )
& ( p101(X1)
| ~ p102(X1) )
& ( p100(X1)
| ~ p101(X1) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren12_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_58,plain,
( ~ ren12(X0)
| ~ p101(X0)
| ren4(X0)
| p102(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren12_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_38,plain,
( ~ ren5(X0)
| p101(skf9(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_98,plain,
( ~ ren12(skf9(X0))
| ~ ren5(X0)
| ren4(skf9(X0))
| p102(skf9(X0)) ),
inference(resolution,[status(thm)],[c_58,c_38]) ).
% CNF SPASS RESOLUTION.
cnf(c_99,plain,
( ~ ren12(skf9(X0))
| ~ ren5(X0)
| ren4(skf9(X0)) ),
inference(resolution,[status(thm)],[c_37,c_98]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_59,plain,
( ~ ren12(X0)
| ~ p100(X0)
| ren5(X0)
| p101(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren12_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_73,plain,
( ~ r1(skc11,X0)
| ren12(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FILE RECORD
fof(reflexivity,axiom,
! [X1] : r1(X1,X1),
file('theBenchmark.p',reflexivity) ).
% FOF SIMPLE INFERENCE
fof(reflexivity_elimTB,axiom,
! [X1] : r1(X1,X1),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[reflexivity])]) ).
% FOF SIMPLE INFERENCE
fof(reflexivity_elimImpEquivPushNegMiniScope,axiom,
! [X1] : r1(X1,X1),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[reflexivity_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_1,plain,
r1(X0,X0),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[reflexivity_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_74,plain,
~ p101(skc11),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_75,plain,
p100(skc11),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_96,plain,
( ~ ren5(skc11)
| ren12(skf9(skc11)) ),
inference(resolution,[status(thm)],[c_73,c_35]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_27,plain,
( ~ ren4(X0)
| r1(X0,skf7(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren4_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_138,plain,
$false,
inference(byPropositionalAbstraction,[status(thm)],[c_35,c_137,c_99,c_59,c_73,c_1,c_74,c_75,c_96,c_27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n029.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 5 02:08:10 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38
% 0.11/0.38 % Input Clauses:
% 0.11/0.38 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.11/0.38 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2)
% 0.11/0.38 % 3:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.11/0.38 % 4:2:1:INP:Top: ren1(x0),p6(skf1(x0)) ->
% 0.11/0.38 % 5:2:1:INP:Top: ren1(x0),p106(skf1(x0)) ->
% 0.11/0.38 % 6:2:1:INP:Top: ren1(x0) -> p105(skf1(x0))
% 0.11/0.38 % 7:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.11/0.38 % 8:2:1:INP:Top: ren1(x0) -> p6(skf2(x0))
% 0.11/0.38 % 9:2:1:INP:Top: ren1(x0),p106(skf2(x0)) ->
% 0.11/0.38 % 10:2:1:INP:Top: ren1(x0) -> p105(skf2(x0))
% 0.11/0.38 % 11:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0))
% 0.11/0.38 % 12:2:1:INP:Top: ren2(x0),p5(skf3(x0)) ->
% 0.11/0.38 % 13:2:1:INP:Top: ren2(x0),p105(skf3(x0)) ->
% 0.11/0.38 % 14:2:1:INP:Top: ren2(x0) -> p104(skf3(x0))
% 0.11/0.38 % 15:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0))
% 0.11/0.38 % 16:2:1:INP:Top: ren2(x0) -> p5(skf4(x0))
% 0.11/0.38 % 17:2:1:INP:Top: ren2(x0),p105(skf4(x0)) ->
% 0.11/0.38 % 18:2:1:INP:Top: ren2(x0) -> p104(skf4(x0))
% 0.11/0.38 % 19:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0))
% 0.11/0.38 % 20:2:1:INP:Top: ren3(x0),p4(skf5(x0)) ->
% 0.11/0.38 % 21:2:1:INP:Top: ren3(x0),p104(skf5(x0)) ->
% 0.11/0.38 % 22:2:1:INP:Top: ren3(x0) -> p103(skf5(x0))
% 0.11/0.38 % 23:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0))
% 0.11/0.38 % 24:2:1:INP:Top: ren3(x0) -> p4(skf6(x0))
% 0.11/0.38 % 25:2:1:INP:Top: ren3(x0),p104(skf6(x0)) ->
% 0.11/0.38 % 26:2:1:INP:Top: ren3(x0) -> p103(skf6(x0))
% 0.11/0.38 % 27:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0))
% 0.11/0.38 % 28:2:1:INP:Top: ren4(x0),p3(skf7(x0)) ->
% 0.11/0.38 % 29:2:1:INP:Top: ren4(x0),p103(skf7(x0)) ->
% 0.11/0.38 % 30:2:1:INP:Top: ren4(x0) -> p102(skf7(x0))
% 0.11/0.38 % 31:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0))
% 0.11/0.38 % 32:2:1:INP:Top: ren4(x0) -> p3(skf8(x0))
% 0.11/0.38 % 33:2:1:INP:Top: ren4(x0),p103(skf8(x0)) ->
% 0.11/0.38 % 34:2:1:INP:Top: ren4(x0) -> p102(skf8(x0))
% 0.11/0.38 % 35:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0))
% 0.11/0.38 % 36:2:1:INP:Top: ren5(x0),p2(skf9(x0)) ->
% 0.11/0.38 % 37:2:1:INP:Top: ren5(x0),p102(skf9(x0)) ->
% 0.11/0.38 % 38:2:1:INP:Top: ren5(x0) -> p101(skf9(x0))
% 0.11/0.38 % 39:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0))
% 0.11/0.38 % 40:2:1:INP:Top: ren5(x0) -> p2(skf10(x0))
% 0.11/0.38 % 41:2:1:INP:Top: ren5(x0),p102(skf10(x0)) ->
% 0.11/0.38 % 42:2:1:INP:Top: ren5(x0) -> p101(skf10(x0))
% 0.11/0.38 % 43:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0)
% 0.11/0.38 % 44:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1)
% 0.11/0.38 % 45:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0)
% 0.11/0.38 % 46:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1)
% 0.11/0.38 % 47:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0)
% 0.11/0.38 % 48:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1)
% 0.11/0.38 % 49:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0)
% 0.11/0.38 % 50:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1)
% 0.11/0.38 % 51:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.11/0.38 % 52:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.11/0.38 % 53:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.11/0.38 % 54:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.11/0.38 % 55:4:1:INP:Top: ren12(x0),p104(x0) -> ren1(x0),p105(x0)
% 0.11/0.38 % 56:4:1:INP:Top: ren12(x0),p103(x0) -> ren2(x0),p104(x0)
% 0.11/0.38 % 57:4:1:INP:Top: ren12(x0),p102(x0) -> ren3(x0),p103(x0)
% 0.11/0.38 % 58:4:1:INP:Top: ren12(x0),p101(x0) -> ren4(x0),p102(x0)
% 0.11/0.38 % 59:4:1:INP:Top: ren12(x0),p100(x0) -> ren5(x0),p101(x0)
% 0.11/0.38 % 60:3:1:INP:Top: ren12(x0),p105(x0) -> ren6(x0)
% 0.11/0.38 % 61:3:1:INP:Top: ren12(x0),p104(x0) -> ren7(x0)
% 0.11/0.38 % 62:3:1:INP:Top: ren12(x0),p103(x0) -> ren8(x0)
% 0.11/0.38 % 63:3:1:INP:Top: ren12(x0),p102(x0) -> ren9(x0)
% 0.11/0.38 % 64:3:1:INP:Top: ren12(x0),p101(x0) -> ren10(x0)
% 0.11/0.38 % 65:3:1:INP:Top: ren12(x0),p100(x0) -> ren11(x0)
% 0.11/0.38 % 66:3:1:INP:Top: ren12(x0),p106(x0) -> p105(x0)
% 0.11/0.38 % 67:3:1:INP:Top: ren12(x0),p105(x0) -> p104(x0)
% 0.11/0.38 % 68:3:1:INP:Top: ren12(x0),p104(x0) -> p103(x0)
% 0.11/0.38 % 69:3:1:INP:Top: ren12(x0),p103(x0) -> p102(x0)
% 0.11/0.38 % 70:3:1:INP:Top: ren12(x0),p102(x0) -> p101(x0)
% 0.11/0.38 % 71:3:1:INP:Top: ren12(x0),p101(x0) -> p100(x0)
% 0.11/0.38 % 72:2:1:INP:Top: r1(skc11,x0) -> p3(x0)
% 0.11/0.38 % 73:2:1:INP:Top: r1(skc11,x0) -> ren12(x0)
% 0.11/0.38 % 74:1:0:INP:: p101(skc11) ->
% 0.11/0.38 % 75:1:0:INP:: -> p100(skc11)
% 0.11/0.38
% 0.11/0.38 % Predicates: r1 p3 p6 p106 p105 p104 p5 p103 p4 p102 p101 p2 p100 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12
% 0.11/0.38 % Fol Constants: skc11
% 0.11/0.38 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10
% 0.11/0.38 % Problem Properties:
% 0.11/0.38 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.11/0.38
% 0.11/0.38
% 0.11/0.38 % Reduced Input Axiom Clauses:
% 0.67/0.98 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.67/0.98 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2)
% 0.67/0.98 % 3:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.67/0.98 % 4:2:1:INP:Top: ren1(x0),p6(skf1(x0)) ->
% 0.67/0.98 % 5:2:1:INP:Top: ren1(x0),p106(skf1(x0)) ->
% 0.67/0.98 % 6:2:1:INP:Top: ren1(x0) -> p105(skf1(x0))
% 0.67/0.98 % 7:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.67/0.98 % 8:2:1:INP:Top: ren1(x0) -> p6(skf2(x0))
% 0.67/0.98 % 9:2:1:INP:Top: ren1(x0),p106(skf2(x0)) ->
% 0.67/0.98 % 10:2:1:INP:Top: ren1(x0) -> p105(skf2(x0))
% 0.67/0.98 % 11:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0))
% 0.67/0.98 % 12:2:1:INP:Top: ren2(x0),p5(skf3(x0)) ->
% 0.67/0.98 % 13:2:1:INP:Top: ren2(x0),p105(skf3(x0)) ->
% 0.67/0.98 % 14:2:1:INP:Top: ren2(x0) -> p104(skf3(x0))
% 0.67/0.98 % 15:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0))
% 0.67/0.98 % 16:2:1:INP:Top: ren2(x0) -> p5(skf4(x0))
% 0.67/0.98 % 17:2:1:INP:Top: ren2(x0),p105(skf4(x0)) ->
% 0.67/0.98 % 18:2:1:INP:Top: ren2(x0) -> p104(skf4(x0))
% 0.67/0.98 % 19:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0))
% 0.67/0.98 % 20:2:1:INP:Top: ren3(x0),p4(skf5(x0)) ->
% 0.67/0.98 % 21:2:1:INP:Top: ren3(x0),p104(skf5(x0)) ->
% 0.67/0.98 % 22:2:1:INP:Top: ren3(x0) -> p103(skf5(x0))
% 0.67/0.98 % 23:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0))
% 0.67/0.98 % 24:2:1:INP:Top: ren3(x0) -> p4(skf6(x0))
% 0.67/0.98 % 25:2:1:INP:Top: ren3(x0),p104(skf6(x0)) ->
% 0.67/0.98 % 26:2:1:INP:Top: ren3(x0) -> p103(skf6(x0))
% 0.67/0.98 % 27:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0))
% 0.67/0.98 % 28:2:1:INP:Top: ren4(x0),p3(skf7(x0)) ->
% 0.67/0.98 % 29:2:1:INP:Top: ren4(x0),p103(skf7(x0)) ->
% 0.67/0.98 % 30:2:1:INP:Top: ren4(x0) -> p102(skf7(x0))
% 0.67/0.98 % 31:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0))
% 0.67/0.98 % 32:2:1:INP:Top: ren4(x0) -> p3(skf8(x0))
% 0.67/0.98 % 33:2:1:INP:Top: ren4(x0),p103(skf8(x0)) ->
% 0.67/0.98 % 34:2:1:INP:Top: ren4(x0) -> p102(skf8(x0))
% 0.67/0.98 % 35:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0))
% 0.67/0.98 % 36:2:1:INP:Top: ren5(x0),p2(skf9(x0)) ->
% 0.67/0.98 % 37:2:1:INP:Top: ren5(x0),p102(skf9(x0)) ->
% 0.67/0.98 % 38:2:1:INP:Top: ren5(x0) -> p101(skf9(x0))
% 0.67/0.98 % 39:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0))
% 0.67/0.98 % 40:2:1:INP:Top: ren5(x0) -> p2(skf10(x0))
% 0.67/0.98 % 41:2:1:INP:Top: ren5(x0),p102(skf10(x0)) ->
% 0.67/0.98 % 42:2:1:INP:Top: ren5(x0) -> p101(skf10(x0))
% 0.67/0.98 % 43:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0)
% 0.67/0.98 % 44:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1)
% 0.67/0.98 % 45:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0)
% 0.67/0.98 % 46:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1)
% 0.67/0.98 % 47:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0)
% 0.67/0.98 % 48:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1)
% 0.67/0.98 % 49:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0)
% 0.67/0.98 % 50:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1)
% 0.67/0.98 % 51:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.67/0.98 % 52:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.67/0.98 % 53:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.67/0.98 % 54:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.67/0.98 % 55:4:1:INP:Top: ren12(x0),p104(x0) -> ren1(x0),p105(x0)
% 0.67/0.98 % 56:4:1:INP:Top: ren12(x0),p103(x0) -> ren2(x0),p104(x0)
% 0.67/0.98 % 57:4:1:INP:Top: ren12(x0),p102(x0) -> ren3(x0),p103(x0)
% 0.67/0.98 % 58:4:1:INP:Top: ren12(x0),p101(x0) -> ren4(x0),p102(x0)
% 0.67/0.98 % 59:4:1:INP:Top: ren12(x0),p100(x0) -> ren5(x0),p101(x0)
% 0.67/0.98 % 60:3:1:INP:Top: ren12(x0),p105(x0) -> ren6(x0)
% 0.67/0.98 % 61:3:1:INP:Top: ren12(x0),p104(x0) -> ren7(x0)
% 0.67/0.98 % 62:3:1:INP:Top: ren12(x0),p103(x0) -> ren8(x0)
% 0.67/0.98 % 63:3:1:INP:Top: ren12(x0),p102(x0) -> ren9(x0)
% 0.67/0.98 % 64:3:1:INP:Top: ren12(x0),p101(x0) -> ren10(x0)
% 0.67/0.98 % 65:3:1:INP:Top: ren12(x0),p100(x0) -> ren11(x0)
% 0.67/0.98 % 66:3:1:INP:Top: ren12(x0),p106(x0) -> p105(x0)
% 0.67/0.98 % 67:3:1:INP:Top: ren12(x0),p105(x0) -> p104(x0)
% 0.67/0.98 % 68:3:1:INP:Top: ren12(x0),p104(x0) -> p103(x0)
% 0.67/0.98 % 69:3:1:INP:Top: ren12(x0),p103(x0) -> p102(x0)
% 0.67/0.98 % 70:3:1:INP:Top: ren12(x0),p102(x0) -> p101(x0)
% 0.67/0.98 % 71:3:1:INP:Top: ren12(x0),p101(x0) -> p100(x0)
% 0.67/0.98
% 0.67/0.98 % Reduced Input Conjecture Clauses:
% 0.67/0.98 % 72:2:1:INP:Top: r1(skc11,x0) -> p3(x0)
% 0.67/0.98 % 73:2:1:INP:Top: r1(skc11,x0) -> ren12(x0)
% 0.67/0.98 % 74:1:0:INP:: p101(skc11) ->
% 0.67/0.98 % 75:1:0:INP:: -> p100(skc11)
% 0.67/0.98
% 0.67/0.98
% 0.67/0.98 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 196 atoms initially. Used heuristic: lmodel_grow ===
% 0.67/0.98
% 0.67/0.98 %
% 0.67/0.98
% 0.67/0.98 % === SAT Conflict found: 138:0:0:[35.0,137.0,99.0,59.0,73.0,1.0,74.0,75.0,96.0,27.0]:: ->
% 0.67/0.98
% 0.67/0.98 % SZS status Theorem
% 0.67/0.98 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.98
% 0.67/0.98 % SPASS-SCL-FOL Statistics:
% 0.67/0.98 % Number of learned clauses: 52
% 0.67/0.98 % Number of propagations: 5226
% 0.67/0.98 % Number of decisions: 3464
% 0.67/0.98 % Number of resolutions: 73
% 0.67/0.98 % Number of condensations: 0
% 0.67/0.98 % Number of sub resolutions: 10
% 0.67/0.98
% 0.67/0.98 % Solver is done. Empty clause found
% 0.67/0.98
% 0.67/0.98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.67/0.98 % SZS output start Proof for theBenchmark
% See solution above
% 0.67/0.99 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.67/0.99
% 0.67/0.99
% 0.67/0.99 % Needed: 0:00:00.60
% 0.67/0.99
% 0.67/0.99 % ###
% 0.67/0.99 % ### Pagesize: 8192
% 0.67/0.99 % ### Marksize: 0
% 0.67/0.99 % ### Memory demanded: 16392 KBytes
% 0.67/0.99 % ### Memory freed: 16392 KBytes
% 0.67/0.99 % ### Memory remaining: 0 Bytes
% 0.67/0.99 % ### Pages allocated: 1259 Pages
% 0.67/0.99 % ###
%------------------------------------------------------------------------------