%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL668+1.001 : 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 : n002.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:05 PM UTC 2026
% Result : Theorem 2.88s 3.19s
% Output : Proof 2.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of formulae : 63 ( 11 unt; 9 def)
% Number of atoms : 674 ( 0 equ)
% Maximal formula atoms : 84 ( 10 avg)
% Number of connectives : 1143 ( 532 ~; 461 |; 141 &)
% ( 0 <=>; 0 =>; 9 <=; 0 <~>)
% Maximal formula depth : 44 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-1 aty)
% Number of variables : 385 ( 0 sgn 273 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ( ~ p12(X1)
& ~ p10(X1)
& ~ p8(X1)
& ~ p6(X1)
& ~ p4(X1)
& ~ p2(X1) ) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p7(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p5(X1)
& ~ p1(X1) )
| ( p1(X1)
& p5(X1) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p4(X1)
& ~ p5(X1) )
| ( p5(X1)
& p4(X1) ) ) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p3(X1)
& ~ p4(X1) )
| ( p4(X1)
& p3(X1) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p2(X1)
& ~ p3(X1) )
| ( p3(X1)
& p2(X1) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p1(X1)
& ~ p2(X1) )
| ( p2(X1)
& p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ( p6(X1)
& p5(X1)
& p4(X1)
& p3(X1)
& p2(X1)
& p1(X1) ) ) ) ) ) ) ) ),
file('theBenchmark.p',main) ).
% NEGATING CONJECTURE
fof(main_nc,negated_conjecture,
? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ( ~ p12(X1)
& ~ p10(X1)
& ~ p8(X1)
& ~ p6(X1)
& ~ p4(X1)
& ~ p2(X1) ) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p7(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p5(X1)
& ~ p1(X1) )
| ( p1(X1)
& p5(X1) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p4(X1)
& ~ p5(X1) )
| ( p5(X1)
& p4(X1) ) ) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p3(X1)
& ~ p4(X1) )
| ( p4(X1)
& p3(X1) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p2(X1)
& ~ p3(X1) )
| ( p3(X1)
& p2(X1) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( ~ p1(X1)
& ~ p2(X1) )
| ( p2(X1)
& p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ( p6(X1)
& p5(X1)
& p4(X1)
& p3(X1)
& p2(X1)
& p1(X1) ) ) ) ) ) ) ) ),
inference(negating_conjecture,[status(cth)],[main]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimTB,negated_conjecture,
? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ( ~ p12(X7)
& ~ p10(X7)
& ~ p8(X7)
& ~ p6(X7)
& ~ p4(X7)
& ~ p2(X7) ) ) ) ) ) ) )
| ! [X8] :
( ~ r1(X1,X8)
| p7(X8) )
| ~ ! [X9] :
( ~ r1(X1,X9)
| ~ ( ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ~ ( ( ~ p5(X16)
& ~ p1(X16) )
| ( p1(X16)
& p5(X16) ) ) ) ) ) ) ) ) )
| ! [X17] :
( ~ r1(X9,X17)
| p6(X17) )
| ~ ! [X18] :
( ~ r1(X9,X18)
| ~ ( ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ~ ( ( ~ p4(X24)
& ~ p5(X24) )
| ( p5(X24)
& p4(X24) ) ) ) ) ) ) ) )
| ! [X25] :
( ~ r1(X18,X25)
| p5(X25) )
| ~ ! [X26] :
( ~ r1(X18,X26)
| ~ ( ~ ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ ( ( ~ p3(X31)
& ~ p4(X31) )
| ( p4(X31)
& p3(X31) ) ) ) ) ) ) )
| ! [X32] :
( ~ r1(X26,X32)
| p4(X32) )
| ~ ! [X33] :
( ~ r1(X26,X33)
| ~ ( ~ ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ( ( ~ p2(X37)
& ~ p3(X37) )
| ( p3(X37)
& p2(X37) ) ) ) ) ) )
| ! [X38] :
( ~ r1(X33,X38)
| p3(X38) )
| ~ ! [X39] :
( ~ r1(X33,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ~ ( ( ~ p1(X42)
& ~ p2(X42) )
| ( p2(X42)
& p1(X42) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X43] :
( ~ r1(X1,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ( p6(X48)
& p5(X48)
& p4(X48)
& p3(X48)
& p2(X48)
& p1(X48) ) ) ) ) ) ) ) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[main_nc])]) ).
% FOF INTRODUCE RENAMING
fof(ren2_defn,definition,
! [X24] :
( ren2(X24)
<= ( ( ~ p4(X24)
& ~ p5(X24) )
| ( p5(X24)
& p4(X24) ) ) ),
introduced(definition,[new_symbols(definition,[ren2])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren2_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ( p4(X1)
| p5(X1) )
& ( ~ p5(X1)
| ~ p4(X1) ) )
| ren2(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren2_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_5,plain,
( ~ p5(X0)
| ~ p4(X0)
| ren2(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren2_elimImpEquivPushNegMiniScope])]) ).
% FOF INTRODUCE RENAMING
fof(ren1_defn,definition,
! [X16] :
( ren1(X16)
<= ( ( ~ p5(X16)
& ~ p1(X16) )
| ( p1(X16)
& p5(X16) ) ) ),
introduced(definition,[new_symbols(definition,[ren1])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren1_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ( p5(X1)
| p1(X1) )
& ( ~ p1(X1)
| ~ p5(X1) ) )
| ren1(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren1_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_2,plain,
( p5(X0)
| p1(X0)
| ren1(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren1_elimImpEquivPushNegMiniScope])]) ).
% FOF INTRODUCE RENAMING
fof(ren3_defn,definition,
! [X31] :
( ren3(X31)
<= ( ( ~ p3(X31)
& ~ p4(X31) )
| ( p4(X31)
& p3(X31) ) ) ),
introduced(definition,[new_symbols(definition,[ren3])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren3_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ( p3(X1)
| p4(X1) )
& ( ~ p4(X1)
| ~ p3(X1) ) )
| ren3(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren3_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_6,plain,
( p3(X0)
| p4(X0)
| ren3(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren3_elimImpEquivPushNegMiniScope])]) ).
% FOF INTRODUCE RENAMING
fof(ren8_defn,definition,
! [X18] :
( ren8(X18)
<= ( ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ~ ren2(X24) ) ) ) ) ) )
| ! [X25] :
( ~ r1(X18,X25)
| p5(X25) )
| ~ ! [X26] :
( ~ r1(X18,X26)
| ~ ren7(X26) ) ) ),
introduced(definition,[new_symbols(definition,[ren8])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren8_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ~ ren2(X7) ) ) ) ) ) )
& ? [X8] :
( r1(X1,X8)
& ~ p5(X8) )
& ! [X9] :
( ~ r1(X1,X9)
| ~ ren7(X9) ) )
| ren8(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren8_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren8_skol,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ~ ren2(X7) ) ) ) ) ) )
& r1(X1,skf3(X1))
& ~ p5(skf3(X1))
& ! [X9] :
( ~ r1(X1,X9)
| ~ ren7(X9) ) )
| ren8(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf3]),skolemize(X8,skf3(X1))],[ren8_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_20,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ ren2(X6)
| ren8(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren8_skol])]) ).
% FOF INTRODUCE RENAMING
fof(ren4_defn,definition,
! [X37] :
( ren4(X37)
<= ( ( ~ p2(X37)
& ~ p3(X37) )
| ( p3(X37)
& p2(X37) ) ) ),
introduced(definition,[new_symbols(definition,[ren4])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren4_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ( p2(X1)
| p3(X1) )
& ( ~ p3(X1)
| ~ p2(X1) ) )
| ren4(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren4_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_9,plain,
( ~ p3(X0)
| ~ p2(X0)
| ren4(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren4_elimImpEquivPushNegMiniScope])]) ).
% FOF INTRODUCE RENAMING
fof(ren7_defn,definition,
! [X26] :
( ren7(X26)
<= ( ~ ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ~ ren3(X31) ) ) ) ) )
| ! [X32] :
( ~ r1(X26,X32)
| p4(X32) )
| ~ ! [X33] :
( ~ r1(X26,X33)
| ~ ren6(X33) ) ) ),
introduced(definition,[new_symbols(definition,[ren7])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren7_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ~ ren3(X6) ) ) ) ) )
& ? [X7] :
( r1(X1,X7)
& ~ p4(X7) )
& ! [X8] :
( ~ r1(X1,X8)
| ~ ren6(X8) ) )
| ren7(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren7_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren7_skol,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ~ ren3(X6) ) ) ) ) )
& r1(X1,skf2(X1))
& ~ p4(skf2(X1))
& ! [X8] :
( ~ r1(X1,X8)
| ~ ren6(X8) ) )
| ren7(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf2]),skolemize(X7,skf2(X1))],[ren7_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_16,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ ren3(X5)
| ren7(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren7_skol])]) ).
% FOF INTRODUCE RENAMING
fof(ren5_defn,definition,
! [X42] :
( ren5(X42)
<= ( ( ~ p1(X42)
& ~ p2(X42) )
| ( p2(X42)
& p1(X42) ) ) ),
introduced(definition,[new_symbols(definition,[ren5])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren5_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ( p1(X1)
| p2(X1) )
& ( ~ p2(X1)
| ~ p1(X1) ) )
| ren5(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren5_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_10,plain,
( p1(X0)
| p2(X0)
| ren5(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_elimImpEquivPushNegMiniScope])]) ).
% FOF INTRODUCE RENAMING
fof(ren6_defn,definition,
! [X33] :
( ren6(X33)
<= ( ~ ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ren4(X37) ) ) ) )
| ! [X38] :
( ~ r1(X33,X38)
| p3(X38) )
| ~ ! [X39] :
( ~ r1(X33,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ~ ren5(X42) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren6])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren6_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ~ ren4(X5) ) ) ) )
& ? [X6] :
( r1(X1,X6)
& ~ p3(X6) )
& ! [X7] :
( ~ r1(X1,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ~ ren5(X10) ) ) ) ) )
| ren6(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren6_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren6_skol,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ~ ren4(X5) ) ) ) )
& r1(X1,skf1(X1))
& ~ p3(skf1(X1))
& ! [X7] :
( ~ r1(X1,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ~ ren5(X10) ) ) ) ) )
| ren6(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf1]),skolemize(X6,skf1(X1))],[ren6_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_12,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ ren4(X4)
| ren6(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren6_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_15,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ ren5(X4)
| ren6(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren6_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_4,plain,
( p4(X0)
| p5(X0)
| ren2(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren2_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_3,plain,
( ~ p1(X0)
| ~ p5(X0)
| ren1(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren1_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_7,plain,
( ~ p4(X0)
| ~ p3(X0)
| ren3(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren3_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_8,plain,
( p2(X0)
| p3(X0)
| ren4(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren4_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_11,plain,
( ~ p2(X0)
| ~ p1(X0)
| ren5(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_elimImpEquivPushNegMiniScope])]) ).
% CNF SPASS RESOLUTION.
cnf(c_52,plain,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X0)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X0)
| ~ p1(X0)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X0)
| ren1(X0)
| ren8(X1)
| ren7(X7)
| ren5(X0)
| ren6(X12) ),
inference(resolution,[status(thm)],[c_4,c_3,c_7,c_20,c_8,c_16,c_11,c_12]) ).
% CNF SPASS RESOLUTION.
cnf(c_53,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X6)
| ~ p1(X6)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X6)
| ren1(X6)
| ren8(X0)
| ren7(X7)
| ren6(X12) ),
inference(resolution,[status(thm)],[c_15,c_52]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_19,plain,
( ~ r1(X0,X1)
| ~ ren6(X1)
| ren7(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren7_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_23,plain,
( ~ r1(X0,X1)
| ~ ren7(X1)
| ren8(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren8_skol])]) ).
% FOF INTRODUCE RENAMING
fof(ren9_defn,definition,
! [X9] :
( ren9(X9)
<= ( ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ~ ren1(X16) ) ) ) ) ) ) )
| ! [X17] :
( ~ r1(X9,X17)
| p6(X17) )
| ~ ! [X18] :
( ~ r1(X9,X18)
| ~ ren8(X18) ) ) ),
introduced(definition,[new_symbols(definition,[ren9])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren9_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ~ ren1(X8) ) ) ) ) ) ) )
& ? [X9] :
( r1(X1,X9)
& ~ p6(X9) )
& ! [X10] :
( ~ r1(X1,X10)
| ~ ren8(X10) ) )
| ren9(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren9_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren9_skol,plain,
! [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ~ ren1(X8) ) ) ) ) ) ) )
& r1(X1,skf4(X1))
& ~ p6(skf4(X1))
& ! [X10] :
( ~ r1(X1,X10)
| ~ ren8(X10) ) )
| ren9(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf4]),skolemize(X9,skf4(X1))],[ren9_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_27,plain,
( ~ r1(X0,X1)
| ~ ren8(X1)
| ren9(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren9_skol])]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ( ~ p12(X7)
& ~ p10(X7)
& ~ p8(X7)
& ~ p6(X7)
& ~ p4(X7)
& ~ p2(X7) ) ) ) ) ) ) )
| ! [X8] :
( ~ r1(X1,X8)
| p7(X8) )
| ~ ! [X9] :
( ~ r1(X1,X9)
| ~ ren9(X9) )
| ! [X43] :
( ~ r1(X1,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ( p6(X48)
& p5(X48)
& p4(X48)
& p3(X48)
& p2(X48)
& p1(X48) ) ) ) ) ) ) ) ),
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]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ? [X2] :
( r1(X1,X2)
& ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ( p12(X7)
| p10(X7)
| p8(X7)
| p6(X7)
| p4(X7)
| p2(X7) ) ) ) ) ) ) )
& ? [X8] :
( r1(X1,X8)
& ~ p7(X8) )
& ! [X9] :
( ~ r1(X1,X9)
| ~ ren9(X9) )
& ? [X10] :
( r1(X1,X10)
& ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ? [X13] :
( r1(X12,X13)
& ? [X14] :
( r1(X13,X14)
& ? [X15] :
( r1(X14,X15)
& ( ~ p6(X15)
| ~ p5(X15)
| ~ p4(X15)
| ~ p3(X15)
| ~ p2(X15)
| ~ p1(X15) ) ) ) ) ) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( r1(skc5,skc6)
& r1(skc6,skc7)
& r1(skc7,skc8)
& r1(skc8,skc9)
& r1(skc9,skc10)
& r1(skc10,skc11)
& ( p12(skc11)
| p10(skc11)
| p8(skc11)
| p6(skc11)
| p4(skc11)
| p2(skc11) )
& r1(skc5,skc12)
& ~ p7(skc12)
& ! [X9] :
( ~ r1(skc5,X9)
| ~ ren9(X9) )
& r1(skc5,skc13)
& r1(skc13,skc14)
& r1(skc14,skc15)
& r1(skc15,skc16)
& r1(skc16,skc17)
& r1(skc17,skc18)
& ( ~ p6(skc18)
| ~ p5(skc18)
| ~ p4(skc18)
| ~ p3(skc18)
| ~ p2(skc18)
| ~ p1(skc18) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc5,skc6,skc7,skc8,skc9,skc10,skc11,skc12,skc13,skc14,skc15,skc16,skc17,skc18]),skolemize(X1,skc5),skolemize(X2,skc6),skolemize(X3,skc7),skolemize(X4,skc8),skolemize(X5,skc9),skolemize(X6,skc10),skolemize(X7,skc11),skolemize(X8,skc12),skolemize(X10,skc13),skolemize(X11,skc14),skolemize(X12,skc15),skolemize(X13,skc16),skolemize(X14,skc17),skolemize(X15,skc18)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_37,plain,
( ~ r1(skc5,X0)
| ~ ren9(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_45,plain,
( ~ r1(X0,X1)
| ~ ren8(X1)
| ~ r1(skc5,X0) ),
inference(resolution,[status(thm)],[c_27,c_37]) ).
% CNF SPASS RESOLUTION.
cnf(c_48,plain,
( ~ r1(X0,X1)
| ~ ren7(X1)
| ~ r1(X2,X0)
| ~ r1(skc5,X2) ),
inference(resolution,[status(thm)],[c_23,c_45]) ).
% CNF SPASS RESOLUTION.
cnf(c_50,plain,
( ~ r1(X0,X1)
| ~ ren6(X1)
| ~ r1(X2,X0)
| ~ r1(X3,X2)
| ~ r1(skc5,X3) ),
inference(resolution,[status(thm)],[c_19,c_48]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_24,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ ren1(X7)
| ren9(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren9_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_32,plain,
r1(skc9,skc10),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_33,plain,
r1(skc10,skc11),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_29,plain,
r1(skc6,skc7),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_30,plain,
r1(skc7,skc8),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_31,plain,
r1(skc8,skc9),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_28,plain,
r1(skc5,skc6),
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])]) ).
% CNF SPASS RESOLUTION.
cnf(c_54,plain,
$false,
inference(resolution,[status(thm)],[c_5,c_2,c_6,c_20,c_9,c_16,c_10,c_12,c_53,c_15,c_50,c_48,c_24,c_32,c_33,c_29,c_30,c_31,c_37,c_45,c_28,c_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL668+1.001 : 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.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 5 07:05:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37
% 0.09/0.37 % Input Clauses:
% 0.09/0.37 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.09/0.37 % 2:3:1:INP:Top: -> p5(x0),p1(x0),ren1(x0)
% 0.09/0.37 % 3:3:1:INP:Top: p1(x0),p5(x0) -> ren1(x0)
% 0.09/0.37 % 4:3:1:INP:Top: -> p4(x0),p5(x0),ren2(x0)
% 0.09/0.37 % 5:3:1:INP:Top: p5(x0),p4(x0) -> ren2(x0)
% 0.09/0.37 % 6:3:1:INP:Top: -> p3(x0),p4(x0),ren3(x0)
% 0.09/0.37 % 7:3:1:INP:Top: p4(x0),p3(x0) -> ren3(x0)
% 0.09/0.37 % 8:3:1:INP:Top: -> p2(x0),p3(x0),ren4(x0)
% 0.09/0.37 % 9:3:1:INP:Top: p3(x0),p2(x0) -> ren4(x0)
% 0.09/0.37 % 10:3:1:INP:Top: -> p1(x0),p2(x0),ren5(x0)
% 0.09/0.37 % 11:3:1:INP:Top: p2(x0),p1(x0) -> ren5(x0)
% 0.09/0.37 % 12:6:5:INP:TopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),ren4(x4) -> ren6(x0)
% 0.09/0.37 % 13:2:1:INP:Top: -> r1(x0,skf1(x0)),ren6(x0)
% 0.09/0.37 % 14:2:1:INP:Top: p3(skf1(x0)) -> ren6(x0)
% 0.09/0.37 % 15:6:5:INP:TopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),ren5(x4) -> ren6(x0)
% 0.09/0.37 % 16:7:6:INP:TopTopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),ren3(x5) -> ren7(x0)
% 0.09/0.37 % 17:2:1:INP:Top: -> r1(x0,skf2(x0)),ren7(x0)
% 0.09/0.37 % 18:2:1:INP:Top: p4(skf2(x0)) -> ren7(x0)
% 0.09/0.37 % 19:3:2:INP:TopTop: r1(x0,x1),ren6(x1) -> ren7(x0)
% 0.09/0.37 % 20:8:7:INP:TopTopTopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),r1(x5,x6),ren2(x6) -> ren8(x0)
% 0.09/0.37 % 21:2:1:INP:Top: -> r1(x0,skf3(x0)),ren8(x0)
% 0.09/0.37 % 22:2:1:INP:Top: p5(skf3(x0)) -> ren8(x0)
% 0.09/0.37 % 23:3:2:INP:TopTop: r1(x0,x1),ren7(x1) -> ren8(x0)
% 0.09/0.37 % 24:9:8:INP:TopTopTopTopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),r1(x5,x6),r1(x6,x7),ren1(x7) -> ren9(x0)
% 0.09/0.37 % 25:2:1:INP:Top: -> r1(x0,skf4(x0)),ren9(x0)
% 0.09/0.37 % 26:2:1:INP:Top: p6(skf4(x0)) -> ren9(x0)
% 0.09/0.37 % 27:3:2:INP:TopTop: r1(x0,x1),ren8(x1) -> ren9(x0)
% 0.09/0.37 % 28:1:0:INP:: -> r1(skc5,skc6)
% 0.09/0.37 % 29:1:0:INP:: -> r1(skc6,skc7)
% 0.09/0.37 % 30:1:0:INP:: -> r1(skc7,skc8)
% 0.09/0.37 % 31:1:0:INP:: -> r1(skc8,skc9)
% 0.09/0.37 % 32:1:0:INP:: -> r1(skc9,skc10)
% 0.09/0.37 % 33:1:0:INP:: -> r1(skc10,skc11)
% 0.09/0.37 % 34:6:0:INP:: -> p12(skc11),p10(skc11),p8(skc11),p6(skc11),p4(skc11),p2(skc11)
% 0.09/0.37 % 35:1:0:INP:: -> r1(skc5,skc12)
% 0.09/0.37 % 36:1:0:INP:: p7(skc12) ->
% 0.09/0.37 % 37:2:1:INP:Top: r1(skc5,x0),ren9(x0) ->
% 0.09/0.37 % 38:1:0:INP:: -> r1(skc5,skc13)
% 0.09/0.37 % 39:1:0:INP:: -> r1(skc13,skc14)
% 0.09/0.37 % 40:1:0:INP:: -> r1(skc14,skc15)
% 0.09/0.37 % 41:1:0:INP:: -> r1(skc15,skc16)
% 0.09/0.37 % 42:1:0:INP:: -> r1(skc16,skc17)
% 0.09/0.37 % 43:1:0:INP:: -> r1(skc17,skc18)
% 0.09/0.37 % 44:6:0:INP:: p6(skc18),p5(skc18),p4(skc18),p3(skc18),p2(skc18),p1(skc18) ->
% 0.09/0.37
% 0.09/0.37 % Predicates: r1 p12 p10 p8 p6 p4 p2 p7 p5 p1 p3 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9
% 0.09/0.37 % Fol Constants: skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18
% 0.09/0.37 % Fol Functions: skf1 skf2 skf3 skf4
% 0.09/0.37 % Problem Properties:
% 0.09/0.37 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.09/0.37
% 0.09/0.37
% 0.09/0.37 % Reduced Input Axiom Clauses:
% 0.09/0.37 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.09/0.37 % 2:3:1:INP:Top: -> p5(x0),p1(x0),ren1(x0)
% 0.09/0.37 % 3:3:1:INP:Top: p1(x0),p5(x0) -> ren1(x0)
% 0.09/0.37 % 4:3:1:INP:Top: -> p4(x0),p5(x0),ren2(x0)
% 0.09/0.37 % 5:3:1:INP:Top: p5(x0),p4(x0) -> ren2(x0)
% 0.09/0.37 % 6:3:1:INP:Top: -> p3(x0),p4(x0),ren3(x0)
% 0.09/0.37 % 7:3:1:INP:Top: p4(x0),p3(x0) -> ren3(x0)
% 0.09/0.37 % 8:3:1:INP:Top: -> p2(x0),p3(x0),ren4(x0)
% 0.09/0.37 % 9:3:1:INP:Top: p3(x0),p2(x0) -> ren4(x0)
% 0.09/0.37 % 10:3:1:INP:Top: -> p1(x0),p2(x0),ren5(x0)
% 0.09/0.37 % 11:3:1:INP:Top: p2(x0),p1(x0) -> ren5(x0)
% 0.09/0.37 % 12:6:5:INP:TopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),ren4(x4) -> ren6(x0)
% 0.09/0.37 % 13:2:1:INP:Top: -> r1(x0,skf1(x0)),ren6(x0)
% 0.09/0.37 % 14:2:1:INP:Top: p3(skf1(x0)) -> ren6(x0)
% 0.09/0.37 % 15:6:5:INP:TopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),ren5(x4) -> ren6(x0)
% 0.09/0.37 % 16:7:6:INP:TopTopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),ren3(x5) -> ren7(x0)
% 0.09/0.37 % 17:2:1:INP:Top: -> r1(x0,skf2(x0)),ren7(x0)
% 0.09/0.37 % 18:2:1:INP:Top: p4(skf2(x0)) -> ren7(x0)
% 0.09/0.37 % 19:3:2:INP:TopTop: r1(x0,x1),ren6(x1) -> ren7(x0)
% 0.09/0.37 % 20:8:7:INP:TopTopTopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),r1(x5,x6),ren2(x6) -> ren8(x0)
% 0.09/0.37 % 21:2:1:INP:Top: -> r1(x0,skf3(x0)),ren8(x0)
% 0.09/0.37 % 22:2:1:INP:Top: p5(skf3(x0)) -> ren8(x0)
% 0.09/0.37 % 23:3:2:INP:TopTop: r1(x0,x1),ren7(x1) -> ren8(x0)
% 0.09/0.37 % 24:9:8:INP:TopTopTopTopTopTopTopTop: r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4),r1(x4,x5),r1(x5,x6),r1(x6,x7),ren1(x7) -> ren9(x0)
% 0.09/0.37 % 25:2:1:INP:Top: -> r1(x0,skf4(x0)),ren9(x0)
% 0.09/0.37 % 26:2:1:INP:Top: p6(skf4(x0)) -> ren9(x0)
% 0.09/0.37 % 27:3:2:INP:TopTop: r1(x0,x1),ren8(x1) -> ren9(x0)
% 2.88/3.19
% 2.88/3.19 % Reduced Input Conjecture Clauses:
% 2.88/3.19 % 28:1:0:INP:: -> r1(skc5,skc6)
% 2.88/3.19 % 29:1:0:INP:: -> r1(skc6,skc7)
% 2.88/3.19 % 30:1:0:INP:: -> r1(skc7,skc8)
% 2.88/3.19 % 31:1:0:INP:: -> r1(skc8,skc9)
% 2.88/3.19 % 32:1:0:INP:: -> r1(skc9,skc10)
% 2.88/3.19 % 33:1:0:INP:: -> r1(skc10,skc11)
% 2.88/3.19 % 34:6:0:INP:: -> p12(skc11),p10(skc11),p8(skc11),p6(skc11),p4(skc11),p2(skc11)
% 2.88/3.19 % 35:1:0:INP:: -> r1(skc5,skc12)
% 2.88/3.19 % 36:1:0:INP:: p7(skc12) ->
% 2.88/3.19 % 37:2:1:INP:Top: r1(skc5,x0),ren9(x0) ->
% 2.88/3.19 % 38:1:0:INP:: -> r1(skc5,skc13)
% 2.88/3.19 % 39:1:0:INP:: -> r1(skc13,skc14)
% 2.88/3.19 % 40:1:0:INP:: -> r1(skc14,skc15)
% 2.88/3.19 % 41:1:0:INP:: -> r1(skc15,skc16)
% 2.88/3.19 % 42:1:0:INP:: -> r1(skc16,skc17)
% 2.88/3.19 % 43:1:0:INP:: -> r1(skc17,skc18)
% 2.88/3.19 % 44:6:0:INP:: p6(skc18),p5(skc18),p4(skc18),p3(skc18),p2(skc18),p1(skc18) ->
% 2.88/3.19
% 2.88/3.19
% 2.88/3.19 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 120 atoms initially. Used heuristic: lmodel_grow ===
% 2.88/3.19
% 2.88/3.19
% 2.88/3.19
% 2.88/3.19 % SZS status Theorem
% 2.88/3.19 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.88/3.19
% 2.88/3.19 % SPASS-SCL-FOL Statistics:
% 2.88/3.19 % Number of learned clauses: 7
% 2.88/3.19 % Number of propagations: 242
% 2.88/3.19 % Number of decisions: 40
% 2.88/3.19 % Number of resolutions: 34
% 2.88/3.19 % Number of condensations: 0
% 2.88/3.19 % Number of sub resolutions: 2
% 2.88/3.19
% 2.88/3.19 % Solver is done. Empty clause found
% 2.88/3.19
% 2.88/3.19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 2.88/3.19 % SZS output start Proof for theBenchmark
% See solution above
% 2.96/3.20 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 2.96/3.20
% 2.96/3.20
% 2.96/3.20 % Needed: 0:00:02.82
% 2.96/3.20
% 2.96/3.20 % ###
% 2.96/3.20 % ### Pagesize: 8192
% 2.96/3.20 % ### Marksize: 0
% 2.96/3.20 % ### Memory demanded: 27038 KBytes
% 2.96/3.20 % ### Memory freed: 27038 KBytes
% 2.96/3.20 % ### Memory remaining: 0 Bytes
% 2.96/3.20 % ### Pages allocated: 3458 Pages
% 2.96/3.20 % ###
%------------------------------------------------------------------------------