%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL644+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:09:52 PM UTC 2026
% Result : Theorem 0.15s 0.37s
% Output : Proof 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 26
% Syntax : Number of formulae : 34 ( 3 unt; 25 def)
% Number of atoms : 1093 ( 0 equ)
% Maximal formula atoms : 225 ( 32 avg)
% Number of connectives : 1697 ( 638 ~; 722 |; 312 &)
% ( 0 <=>; 0 =>; 25 <=; 0 <~>)
% Maximal formula depth : 29 ( 13 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 33 ( 32 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 18 con; 0-1 aty)
% Number of variables : 422 ( 0 sgn 390 !; 32 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p6(X2) ) )
| p5(X1) )
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& p5(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) ) )
| p4(X1) )
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& p4(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) )
| p3(X1) )
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& p3(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) ) )
| p2(X1) )
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& p2(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) ) )
| p1(X1) )
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ ( p1(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& p1(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) ) ) ) ),
file('theBenchmark.p',main) ).
% NEGATING CONJECTURE
fof(main_nc,negated_conjecture,
? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p6(X2) ) )
| p5(X1) )
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& p5(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) ) )
| p4(X1) )
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& p4(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) )
| p3(X1) )
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& p3(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) ) )
| p2(X1) )
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& p2(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) ) )
| p1(X1) )
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ ( p1(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& p1(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) ) ) ) ),
inference(negating_conjecture,[status(cth)],[main]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimTB,negated_conjecture,
? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X3] :
( ~ r1(X2,X3)
| p6(X3) ) )
| p5(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p6(X4)
| ~ ( p5(X4)
& ! [X5] :
( ~ r1(X4,X5)
| p5(X5) )
& p5(X4) ) )
| ~ ( ! [X6] :
( ~ r1(X1,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ~ ( p6(X7)
& ! [X8] :
( ~ r1(X7,X8)
| p6(X8) ) )
| p5(X7) )
| p6(X6)
| ~ ( p5(X6)
& ! [X9] :
( ~ r1(X6,X9)
| p5(X9) )
& p5(X6) ) )
& ! [X10] :
( ~ r1(X1,X10)
| ~ ( p6(X10)
& ! [X11] :
( ~ r1(X10,X11)
| p6(X11) ) )
| p5(X10)
| ! [X12] :
( ~ r1(X10,X12)
| p6(X12)
| ~ ( p5(X12)
& ! [X13] :
( ~ r1(X12,X13)
| p5(X13) )
& p5(X12) ) ) )
& ! [X14] :
( ~ r1(X1,X14)
| ~ ( p6(X14)
& ! [X15] :
( ~ r1(X14,X15)
| p6(X15) ) )
| p5(X14)
| p6(X14)
| ~ ( p5(X14)
& ! [X16] :
( ~ r1(X14,X16)
| p5(X16) )
& p5(X14) ) ) ) )
| ~ ( ! [X17] :
( ~ r1(X1,X17)
| ~ ( p5(X17)
& ! [X18] :
( ~ r1(X17,X18)
| p5(X18) ) )
| p4(X17) )
| ! [X19] :
( ~ r1(X1,X19)
| p5(X19)
| ~ ( p4(X19)
& ! [X20] :
( ~ r1(X19,X20)
| p4(X20) )
& p4(X19) ) )
| ~ ( ! [X21] :
( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ~ ( p5(X22)
& ! [X23] :
( ~ r1(X22,X23)
| p5(X23) ) )
| p4(X22) )
| p5(X21)
| ~ ( p4(X21)
& ! [X24] :
( ~ r1(X21,X24)
| p4(X24) )
& p4(X21) ) )
& ! [X25] :
( ~ r1(X1,X25)
| ~ ( p5(X25)
& ! [X26] :
( ~ r1(X25,X26)
| p5(X26) ) )
| p4(X25)
| ! [X27] :
( ~ r1(X25,X27)
| p5(X27)
| ~ ( p4(X27)
& ! [X28] :
( ~ r1(X27,X28)
| p4(X28) )
& p4(X27) ) ) )
& ! [X29] :
( ~ r1(X1,X29)
| ~ ( p5(X29)
& ! [X30] :
( ~ r1(X29,X30)
| p5(X30) ) )
| p4(X29)
| p5(X29)
| ~ ( p4(X29)
& ! [X31] :
( ~ r1(X29,X31)
| p4(X31) )
& p4(X29) ) ) ) )
| ~ ( ! [X32] :
( ~ r1(X1,X32)
| ~ ( p4(X32)
& ! [X33] :
( ~ r1(X32,X33)
| p4(X33) ) )
| p3(X32) )
| ! [X34] :
( ~ r1(X1,X34)
| p4(X34)
| ~ ( p3(X34)
& ! [X35] :
( ~ r1(X34,X35)
| p3(X35) )
& p3(X34) ) )
| ~ ( ! [X36] :
( ~ r1(X1,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ( p4(X37)
& ! [X38] :
( ~ r1(X37,X38)
| p4(X38) ) )
| p3(X37) )
| p4(X36)
| ~ ( p3(X36)
& ! [X39] :
( ~ r1(X36,X39)
| p3(X39) )
& p3(X36) ) )
& ! [X40] :
( ~ r1(X1,X40)
| ~ ( p4(X40)
& ! [X41] :
( ~ r1(X40,X41)
| p4(X41) ) )
| p3(X40)
| ! [X42] :
( ~ r1(X40,X42)
| p4(X42)
| ~ ( p3(X42)
& ! [X43] :
( ~ r1(X42,X43)
| p3(X43) )
& p3(X42) ) ) )
& ! [X44] :
( ~ r1(X1,X44)
| ~ ( p4(X44)
& ! [X45] :
( ~ r1(X44,X45)
| p4(X45) ) )
| p3(X44)
| p4(X44)
| ~ ( p3(X44)
& ! [X46] :
( ~ r1(X44,X46)
| p3(X46) )
& p3(X44) ) ) ) )
| ~ ( ! [X47] :
( ~ r1(X1,X47)
| ~ ( p3(X47)
& ! [X48] :
( ~ r1(X47,X48)
| p3(X48) ) )
| p2(X47) )
| ! [X49] :
( ~ r1(X1,X49)
| p3(X49)
| ~ ( p2(X49)
& ! [X50] :
( ~ r1(X49,X50)
| p2(X50) )
& p2(X49) ) )
| ~ ( ! [X51] :
( ~ r1(X1,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ~ ( p3(X52)
& ! [X53] :
( ~ r1(X52,X53)
| p3(X53) ) )
| p2(X52) )
| p3(X51)
| ~ ( p2(X51)
& ! [X54] :
( ~ r1(X51,X54)
| p2(X54) )
& p2(X51) ) )
& ! [X55] :
( ~ r1(X1,X55)
| ~ ( p3(X55)
& ! [X56] :
( ~ r1(X55,X56)
| p3(X56) ) )
| p2(X55)
| ! [X57] :
( ~ r1(X55,X57)
| p3(X57)
| ~ ( p2(X57)
& ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
& p2(X57) ) ) )
& ! [X59] :
( ~ r1(X1,X59)
| ~ ( p3(X59)
& ! [X60] :
( ~ r1(X59,X60)
| p3(X60) ) )
| p2(X59)
| p3(X59)
| ~ ( p2(X59)
& ! [X61] :
( ~ r1(X59,X61)
| p2(X61) )
& p2(X59) ) ) ) )
| ! [X62] :
( ~ r1(X1,X62)
| p5(X62)
| ~ ( ! [X63] :
( ~ r1(X62,X63)
| p5(X63) )
& p5(X62) ) )
| ! [X64] :
( ~ r1(X1,X64)
| p5(X64)
| ~ ( ! [X65] :
( ~ r1(X64,X65)
| p5(X65) )
& p5(X64) ) )
| ~ ( ! [X66] :
( ~ r1(X1,X66)
| ~ ( p2(X66)
& ! [X67] :
( ~ r1(X66,X67)
| p2(X67) ) )
| p1(X66) )
| ! [X68] :
( ~ r1(X1,X68)
| p2(X68)
| ~ ( p1(X68)
& ! [X69] :
( ~ r1(X68,X69)
| p1(X69) )
& p1(X68) ) )
| ~ ( ! [X70] :
( ~ r1(X1,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ~ ( p2(X71)
& ! [X72] :
( ~ r1(X71,X72)
| p2(X72) ) )
| p1(X71) )
| p2(X70)
| ~ ( p1(X70)
& ! [X73] :
( ~ r1(X70,X73)
| p1(X73) )
& p1(X70) ) )
& ! [X74] :
( ~ r1(X1,X74)
| ~ ( p2(X74)
& ! [X75] :
( ~ r1(X74,X75)
| p2(X75) ) )
| p1(X74)
| ! [X76] :
( ~ r1(X74,X76)
| p2(X76)
| ~ ( p1(X76)
& ! [X77] :
( ~ r1(X76,X77)
| p1(X77) )
& p1(X76) ) ) )
& ! [X78] :
( ~ r1(X1,X78)
| ~ ( p2(X78)
& ! [X79] :
( ~ r1(X78,X79)
| p2(X79) ) )
| p1(X78)
| p2(X78)
| ~ ( p1(X78)
& ! [X80] :
( ~ r1(X78,X80)
| p1(X80) )
& p1(X78) ) ) ) ) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[main_nc])]) ).
% FOF INTRODUCE RENAMING
fof(ren1_defn,definition,
! [X2,X3] :
( ren1(X2,X3)
<= ( ~ r1(X2,X3)
| p6(X3) ) ),
introduced(definition,[new_symbols(definition,[ren1])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren2_defn,definition,
! [X4,X5] :
( ren2(X4,X5)
<= ( ~ r1(X4,X5)
| p5(X5) ) ),
introduced(definition,[new_symbols(definition,[ren2])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren3_defn,definition,
! [X1,X6] :
( ren3(X1,X6)
<= ( ~ r1(X1,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ~ ( p6(X7)
& ! [X8] :
( ~ r1(X7,X8)
| p6(X8) ) )
| p5(X7) )
| p6(X6)
| ~ ( p5(X6)
& ! [X9] :
( ~ r1(X6,X9)
| p5(X9) )
& p5(X6) ) ) ),
introduced(definition,[new_symbols(definition,[ren3])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren4_defn,definition,
! [X1,X10] :
( ren4(X1,X10)
<= ( ~ r1(X1,X10)
| ~ ( p6(X10)
& ! [X11] :
( ~ r1(X10,X11)
| p6(X11) ) )
| p5(X10)
| ! [X12] :
( ~ r1(X10,X12)
| p6(X12)
| ~ ( p5(X12)
& ! [X13] :
( ~ r1(X12,X13)
| p5(X13) )
& p5(X12) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren4])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren5_defn,definition,
! [X1,X14] :
( ren5(X1,X14)
<= ( ~ r1(X1,X14)
| ~ ( p6(X14)
& ! [X15] :
( ~ r1(X14,X15)
| p6(X15) ) )
| p5(X14)
| p6(X14)
| ~ ( p5(X14)
& ! [X16] :
( ~ r1(X14,X16)
| p5(X16) )
& p5(X14) ) ) ),
introduced(definition,[new_symbols(definition,[ren5])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren6_defn,definition,
! [X17,X18] :
( ren6(X17,X18)
<= ( ~ r1(X17,X18)
| p5(X18) ) ),
introduced(definition,[new_symbols(definition,[ren6])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren7_defn,definition,
! [X19,X20] :
( ren7(X19,X20)
<= ( ~ r1(X19,X20)
| p4(X20) ) ),
introduced(definition,[new_symbols(definition,[ren7])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren8_defn,definition,
! [X1,X21] :
( ren8(X1,X21)
<= ( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ~ ( p5(X22)
& ! [X23] :
( ~ r1(X22,X23)
| p5(X23) ) )
| p4(X22) )
| p5(X21)
| ~ ( p4(X21)
& ! [X24] :
( ~ r1(X21,X24)
| p4(X24) )
& p4(X21) ) ) ),
introduced(definition,[new_symbols(definition,[ren8])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren9_defn,definition,
! [X1,X25] :
( ren9(X1,X25)
<= ( ~ r1(X1,X25)
| ~ ( p5(X25)
& ! [X26] :
( ~ r1(X25,X26)
| p5(X26) ) )
| p4(X25)
| ! [X27] :
( ~ r1(X25,X27)
| p5(X27)
| ~ ( p4(X27)
& ! [X28] :
( ~ r1(X27,X28)
| p4(X28) )
& p4(X27) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren9])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren10_defn,definition,
! [X1,X29] :
( ren10(X1,X29)
<= ( ~ r1(X1,X29)
| ~ ( p5(X29)
& ! [X30] :
( ~ r1(X29,X30)
| p5(X30) ) )
| p4(X29)
| p5(X29)
| ~ ( p4(X29)
& ! [X31] :
( ~ r1(X29,X31)
| p4(X31) )
& p4(X29) ) ) ),
introduced(definition,[new_symbols(definition,[ren10])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren11_defn,definition,
! [X32,X33] :
( ren11(X32,X33)
<= ( ~ r1(X32,X33)
| p4(X33) ) ),
introduced(definition,[new_symbols(definition,[ren11])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren12_defn,definition,
! [X34,X35] :
( ren12(X34,X35)
<= ( ~ r1(X34,X35)
| p3(X35) ) ),
introduced(definition,[new_symbols(definition,[ren12])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren13_defn,definition,
! [X1,X36] :
( ren13(X1,X36)
<= ( ~ r1(X1,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ( p4(X37)
& ! [X38] :
( ~ r1(X37,X38)
| p4(X38) ) )
| p3(X37) )
| p4(X36)
| ~ ( p3(X36)
& ! [X39] :
( ~ r1(X36,X39)
| p3(X39) )
& p3(X36) ) ) ),
introduced(definition,[new_symbols(definition,[ren13])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren14_defn,definition,
! [X1,X40] :
( ren14(X1,X40)
<= ( ~ r1(X1,X40)
| ~ ( p4(X40)
& ! [X41] :
( ~ r1(X40,X41)
| p4(X41) ) )
| p3(X40)
| ! [X42] :
( ~ r1(X40,X42)
| p4(X42)
| ~ ( p3(X42)
& ! [X43] :
( ~ r1(X42,X43)
| p3(X43) )
& p3(X42) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren14])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren15_defn,definition,
! [X1,X44] :
( ren15(X1,X44)
<= ( ~ r1(X1,X44)
| ~ ( p4(X44)
& ! [X45] :
( ~ r1(X44,X45)
| p4(X45) ) )
| p3(X44)
| p4(X44)
| ~ ( p3(X44)
& ! [X46] :
( ~ r1(X44,X46)
| p3(X46) )
& p3(X44) ) ) ),
introduced(definition,[new_symbols(definition,[ren15])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren16_defn,definition,
! [X47,X48] :
( ren16(X47,X48)
<= ( ~ r1(X47,X48)
| p3(X48) ) ),
introduced(definition,[new_symbols(definition,[ren16])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren17_defn,definition,
! [X49,X50] :
( ren17(X49,X50)
<= ( ~ r1(X49,X50)
| p2(X50) ) ),
introduced(definition,[new_symbols(definition,[ren17])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren18_defn,definition,
! [X1,X51] :
( ren18(X1,X51)
<= ( ~ r1(X1,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ~ ( p3(X52)
& ! [X53] :
( ~ r1(X52,X53)
| p3(X53) ) )
| p2(X52) )
| p3(X51)
| ~ ( p2(X51)
& ! [X54] :
( ~ r1(X51,X54)
| p2(X54) )
& p2(X51) ) ) ),
introduced(definition,[new_symbols(definition,[ren18])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren19_defn,definition,
! [X1,X55] :
( ren19(X1,X55)
<= ( ~ r1(X1,X55)
| ~ ( p3(X55)
& ! [X56] :
( ~ r1(X55,X56)
| p3(X56) ) )
| p2(X55)
| ! [X57] :
( ~ r1(X55,X57)
| p3(X57)
| ~ ( p2(X57)
& ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
& p2(X57) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren19])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren20_defn,definition,
! [X1,X59] :
( ren20(X1,X59)
<= ( ~ r1(X1,X59)
| ~ ( p3(X59)
& ! [X60] :
( ~ r1(X59,X60)
| p3(X60) ) )
| p2(X59)
| p3(X59)
| ~ ( p2(X59)
& ! [X61] :
( ~ r1(X59,X61)
| p2(X61) )
& p2(X59) ) ) ),
introduced(definition,[new_symbols(definition,[ren20])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren21_defn,definition,
! [X66,X67] :
( ren21(X66,X67)
<= ( ~ r1(X66,X67)
| p2(X67) ) ),
introduced(definition,[new_symbols(definition,[ren21])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren22_defn,definition,
! [X68,X69] :
( ren22(X68,X69)
<= ( ~ r1(X68,X69)
| p1(X69) ) ),
introduced(definition,[new_symbols(definition,[ren22])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren23_defn,definition,
! [X1,X70] :
( ren23(X1,X70)
<= ( ~ r1(X1,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ~ ( p2(X71)
& ! [X72] :
( ~ r1(X71,X72)
| p2(X72) ) )
| p1(X71) )
| p2(X70)
| ~ ( p1(X70)
& ! [X73] :
( ~ r1(X70,X73)
| p1(X73) )
& p1(X70) ) ) ),
introduced(definition,[new_symbols(definition,[ren23])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren24_defn,definition,
! [X1,X74] :
( ren24(X1,X74)
<= ( ~ r1(X1,X74)
| ~ ( p2(X74)
& ! [X75] :
( ~ r1(X74,X75)
| p2(X75) ) )
| p1(X74)
| ! [X76] :
( ~ r1(X74,X76)
| p2(X76)
| ~ ( p1(X76)
& ! [X77] :
( ~ r1(X76,X77)
| p1(X77) )
& p1(X76) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren24])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren25_defn,definition,
! [X1,X78] :
( ren25(X1,X78)
<= ( ~ r1(X1,X78)
| ~ ( p2(X78)
& ! [X79] :
( ~ r1(X78,X79)
| p2(X79) ) )
| p1(X78)
| p2(X78)
| ~ ( p1(X78)
& ! [X80] :
( ~ r1(X78,X80)
| p1(X80) )
& p1(X78) ) ) ),
introduced(definition,[new_symbols(definition,[ren25])],[main_nc_elimTB]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X3] : ren1(X2,X3) )
| p5(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p6(X4)
| ~ ( p5(X4)
& ! [X5] : ren2(X4,X5)
& p5(X4) ) )
| ~ ( ! [X6] : ren3(X1,X6)
& ! [X10] : ren4(X1,X10)
& ! [X14] : ren5(X1,X14) ) )
| ~ ( ! [X17] :
( ~ r1(X1,X17)
| ~ ( p5(X17)
& ! [X18] : ren6(X17,X18) )
| p4(X17) )
| ! [X19] :
( ~ r1(X1,X19)
| p5(X19)
| ~ ( p4(X19)
& ! [X20] : ren7(X19,X20)
& p4(X19) ) )
| ~ ( ! [X21] : ren8(X1,X21)
& ! [X25] : ren9(X1,X25)
& ! [X29] : ren10(X1,X29) ) )
| ~ ( ! [X32] :
( ~ r1(X1,X32)
| ~ ( p4(X32)
& ! [X33] : ren11(X32,X33) )
| p3(X32) )
| ! [X34] :
( ~ r1(X1,X34)
| p4(X34)
| ~ ( p3(X34)
& ! [X35] : ren12(X34,X35)
& p3(X34) ) )
| ~ ( ! [X36] : ren13(X1,X36)
& ! [X40] : ren14(X1,X40)
& ! [X44] : ren15(X1,X44) ) )
| ~ ( ! [X47] :
( ~ r1(X1,X47)
| ~ ( p3(X47)
& ! [X48] : ren16(X47,X48) )
| p2(X47) )
| ! [X49] :
( ~ r1(X1,X49)
| p3(X49)
| ~ ( p2(X49)
& ! [X50] : ren17(X49,X50)
& p2(X49) ) )
| ~ ( ! [X51] : ren18(X1,X51)
& ! [X55] : ren19(X1,X55)
& ! [X59] : ren20(X1,X59) ) )
| ! [X62] :
( ~ r1(X1,X62)
| p5(X62)
| ~ ( ! [X63] :
( ~ r1(X62,X63)
| p5(X63) )
& p5(X62) ) )
| ! [X64] :
( ~ r1(X1,X64)
| p5(X64)
| ~ ( ! [X65] :
( ~ r1(X64,X65)
| p5(X65) )
& p5(X64) ) )
| ~ ( ! [X66] :
( ~ r1(X1,X66)
| ~ ( p2(X66)
& ! [X67] : ren21(X66,X67) )
| p1(X66) )
| ! [X68] :
( ~ r1(X1,X68)
| p2(X68)
| ~ ( p1(X68)
& ! [X69] : ren22(X68,X69)
& p1(X68) ) )
| ~ ( ! [X70] : ren23(X1,X70)
& ! [X74] : ren24(X1,X74)
& ! [X78] : ren25(X1,X78) ) ) ),
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,ren13_defn,ren14_defn,ren15_defn,ren16_defn,ren17_defn,ren18_defn,ren19_defn,ren20_defn,ren21_defn,ren22_defn,ren23_defn,ren24_defn,ren25_defn]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ~ p6(X2)
| ? [X3] : ~ ren1(X2,X3)
| p5(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p6(X4)
| ~ p5(X4)
| ? [X5] : ~ ren2(X4,X5)
| ~ p5(X4) )
| ? [X6] : ~ ren3(X1,X6)
| ? [X7] : ~ ren4(X1,X7)
| ? [X8] : ~ ren5(X1,X8) )
& ( ! [X9] :
( ~ r1(X1,X9)
| ~ p5(X9)
| ? [X10] : ~ ren6(X9,X10)
| p4(X9) )
| ! [X11] :
( ~ r1(X1,X11)
| p5(X11)
| ~ p4(X11)
| ? [X12] : ~ ren7(X11,X12)
| ~ p4(X11) )
| ? [X13] : ~ ren8(X1,X13)
| ? [X14] : ~ ren9(X1,X14)
| ? [X15] : ~ ren10(X1,X15) )
& ( ! [X16] :
( ~ r1(X1,X16)
| ~ p4(X16)
| ? [X17] : ~ ren11(X16,X17)
| p3(X16) )
| ! [X18] :
( ~ r1(X1,X18)
| p4(X18)
| ~ p3(X18)
| ? [X19] : ~ ren12(X18,X19)
| ~ p3(X18) )
| ? [X20] : ~ ren13(X1,X20)
| ? [X21] : ~ ren14(X1,X21)
| ? [X22] : ~ ren15(X1,X22) )
& ( ! [X23] :
( ~ r1(X1,X23)
| ~ p3(X23)
| ? [X24] : ~ ren16(X23,X24)
| p2(X23) )
| ! [X25] :
( ~ r1(X1,X25)
| p3(X25)
| ~ p2(X25)
| ? [X26] : ~ ren17(X25,X26)
| ~ p2(X25) )
| ? [X27] : ~ ren18(X1,X27)
| ? [X28] : ~ ren19(X1,X28)
| ? [X29] : ~ ren20(X1,X29) )
& ? [X30] :
( r1(X1,X30)
& ~ p5(X30)
& ! [X31] :
( ~ r1(X30,X31)
| p5(X31) )
& p5(X30) )
& ? [X32] :
( r1(X1,X32)
& ~ p5(X32)
& ! [X33] :
( ~ r1(X32,X33)
| p5(X33) )
& p5(X32) )
& ( ! [X34] :
( ~ r1(X1,X34)
| ~ p2(X34)
| ? [X35] : ~ ren21(X34,X35)
| p1(X34) )
| ! [X36] :
( ~ r1(X1,X36)
| p2(X36)
| ~ p1(X36)
| ? [X37] : ~ ren22(X36,X37)
| ~ p1(X36) )
| ? [X38] : ~ ren23(X1,X38)
| ? [X39] : ~ ren24(X1,X39)
| ? [X40] : ~ ren25(X1,X40) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( ( ! [X2] :
( ~ r1(skc11,X2)
| ~ p6(X2)
| ~ ren1(X2,skf12(X2))
| p5(X2) )
| ! [X4] :
( ~ r1(skc11,X4)
| p6(X4)
| ~ p5(X4)
| ~ ren2(X4,skf13(X4))
| ~ p5(X4) )
| ~ ren3(skc11,skc14)
| ~ ren4(skc11,skc15)
| ~ ren5(skc11,skc16) )
& ( ! [X9] :
( ~ r1(skc11,X9)
| ~ p5(X9)
| ~ ren6(X9,skf17(X9))
| p4(X9) )
| ! [X11] :
( ~ r1(skc11,X11)
| p5(X11)
| ~ p4(X11)
| ~ ren7(X11,skf18(X11))
| ~ p4(X11) )
| ~ ren8(skc11,skc19)
| ~ ren9(skc11,skc20)
| ~ ren10(skc11,skc21) )
& ( ! [X16] :
( ~ r1(skc11,X16)
| ~ p4(X16)
| ~ ren11(X16,skf22(X16))
| p3(X16) )
| ! [X18] :
( ~ r1(skc11,X18)
| p4(X18)
| ~ p3(X18)
| ~ ren12(X18,skf23(X18))
| ~ p3(X18) )
| ~ ren13(skc11,skc24)
| ~ ren14(skc11,skc25)
| ~ ren15(skc11,skc26) )
& ( ! [X23] :
( ~ r1(skc11,X23)
| ~ p3(X23)
| ~ ren16(X23,skf27(X23))
| p2(X23) )
| ! [X25] :
( ~ r1(skc11,X25)
| p3(X25)
| ~ p2(X25)
| ~ ren17(X25,skf28(X25))
| ~ p2(X25) )
| ~ ren18(skc11,skc29)
| ~ ren19(skc11,skc30)
| ~ ren20(skc11,skc31) )
& r1(skc11,skc32)
& ~ p5(skc32)
& ! [X31] :
( ~ r1(skc32,X31)
| p5(X31) )
& p5(skc32)
& r1(skc11,skc33)
& ~ p5(skc33)
& ! [X33] :
( ~ r1(skc33,X33)
| p5(X33) )
& p5(skc33)
& ( ! [X34] :
( ~ r1(skc11,X34)
| ~ p2(X34)
| ~ ren21(X34,skf34(X34))
| p1(X34) )
| ! [X36] :
( ~ r1(skc11,X36)
| p2(X36)
| ~ p1(X36)
| ~ ren22(X36,skf35(X36))
| ~ p1(X36) )
| ~ ren23(skc11,skc36)
| ~ ren24(skc11,skc37)
| ~ ren25(skc11,skc38) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc11,skf12,skf13,skc14,skc15,skc16,skf17,skf18,skc19,skc20,skc21,skf22,skf23,skc24,skc25,skc26,skf27,skf28,skc29,skc30,skc31,skc32,skc33,skf34,skf35,skc36,skc37,skc38]),skolemize(X1,skc11),skolemize(X3,skf12(X2)),skolemize(X5,skf13(X4)),skolemize(X6,skc14),skolemize(X7,skc15),skolemize(X8,skc16),skolemize(X10,skf17(X9)),skolemize(X12,skf18(X11)),skolemize(X13,skc19),skolemize(X14,skc20),skolemize(X15,skc21),skolemize(X17,skf22(X16)),skolemize(X19,skf23(X18)),skolemize(X20,skc24),skolemize(X21,skc25),skolemize(X22,skc26),skolemize(X24,skf27(X23)),skolemize(X26,skf28(X25)),skolemize(X27,skc29),skolemize(X28,skc30),skolemize(X29,skc31),skolemize(X30,skc32),skolemize(X32,skc33),skolemize(X35,skf34(X34)),skolemize(X37,skf35(X36)),skolemize(X38,skc36),skolemize(X39,skc37),skolemize(X40,skc38)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_162,plain,
p5(skc33),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_160,plain,
~ p5(skc33),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_179,plain,
$false,
inference(resolution,[status(thm)],[c_162,c_160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+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.10/0.36 % Computer : n029.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 07:10:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.37
% 0.15/0.37 % Input Clauses:
% 0.15/0.37 % 1:2:2:INP:TopTop: -> r1(x0,x1),ren1(x0,x1)
% 0.15/0.37 % 2:2:2:INP:TopTop: p6(x0) -> ren1(x1,x0)
% 0.15/0.37 % 3:2:2:INP:TopTop: -> r1(x0,x1),ren2(x0,x1)
% 0.15/0.37 % 4:2:2:INP:TopTop: p5(x0) -> ren2(x1,x0)
% 0.15/0.37 % 5:2:2:INP:TopTop: -> r1(x0,x1),ren3(x0,x1)
% 0.15/0.37 % 6:2:2:INP:TopTop: -> r1(x0,skf1(x0)),ren3(x1,x0)
% 0.15/0.37 % 7:2:2:INP:TopTop: -> p6(skf1(x0)),ren3(x1,x0)
% 0.15/0.37 % 8:3:3:INP:TopTopTop: r1(skf1(x0),x1) -> p6(x1),ren3(x2,x0)
% 0.15/0.37 % 9:2:2:INP:TopTop: p5(skf1(x0)) -> ren3(x1,x0)
% 0.15/0.37 % 10:2:2:INP:TopTop: p6(x0) -> ren3(x1,x0)
% 0.15/0.37 % 11:2:2:INP:TopTop: -> p5(x0),ren3(x1,x0)
% 0.15/0.37 % 12:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren3(x2,x0)
% 0.15/0.37 % 13:2:2:INP:TopTop: -> p5(x0),ren3(x1,x0)
% 0.15/0.37 % 14:2:2:INP:TopTop: -> r1(x0,x1),ren4(x0,x1)
% 0.15/0.37 % 15:2:2:INP:TopTop: -> p6(x0),ren4(x1,x0)
% 0.15/0.37 % 16:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren4(x2,x0)
% 0.15/0.37 % 17:2:2:INP:TopTop: p5(x0) -> ren4(x1,x0)
% 0.15/0.37 % 18:2:2:INP:TopTop: -> r1(x0,skf2(x0)),ren4(x1,x0)
% 0.15/0.37 % 19:2:2:INP:TopTop: p6(skf2(x0)) -> ren4(x1,x0)
% 0.15/0.37 % 20:2:2:INP:TopTop: -> p5(skf2(x0)),ren4(x1,x0)
% 0.15/0.37 % 21:3:3:INP:TopTopTop: r1(skf2(x0),x1) -> p5(x1),ren4(x2,x0)
% 0.15/0.37 % 22:2:2:INP:TopTop: -> p5(skf2(x0)),ren4(x1,x0)
% 0.15/0.37 % 23:2:2:INP:TopTop: -> r1(x0,x1),ren5(x0,x1)
% 0.15/0.37 % 24:2:2:INP:TopTop: -> p6(x0),ren5(x1,x0)
% 0.15/0.37 % 25:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren5(x2,x0)
% 0.15/0.37 % 26:2:2:INP:TopTop: p5(x0) -> ren5(x1,x0)
% 0.15/0.37 % 27:2:2:INP:TopTop: p6(x0) -> ren5(x1,x0)
% 0.15/0.37 % 28:2:2:INP:TopTop: -> p5(x0),ren5(x1,x0)
% 0.15/0.37 % 29:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren5(x2,x0)
% 0.15/0.37 % 30:2:2:INP:TopTop: -> p5(x0),ren5(x1,x0)
% 0.15/0.37 % 31:2:2:INP:TopTop: -> r1(x0,x1),ren6(x0,x1)
% 0.15/0.37 % 32:2:2:INP:TopTop: p5(x0) -> ren6(x1,x0)
% 0.15/0.37 % 33:2:2:INP:TopTop: -> r1(x0,x1),ren7(x0,x1)
% 0.15/0.37 % 34:2:2:INP:TopTop: p4(x0) -> ren7(x1,x0)
% 0.15/0.37 % 35:2:2:INP:TopTop: -> r1(x0,x1),ren8(x0,x1)
% 0.15/0.37 % 36:2:2:INP:TopTop: -> r1(x0,skf3(x0)),ren8(x1,x0)
% 0.15/0.37 % 37:2:2:INP:TopTop: -> p5(skf3(x0)),ren8(x1,x0)
% 0.15/0.37 % 38:3:3:INP:TopTopTop: r1(skf3(x0),x1) -> p5(x1),ren8(x2,x0)
% 0.15/0.37 % 39:2:2:INP:TopTop: p4(skf3(x0)) -> ren8(x1,x0)
% 0.15/0.37 % 40:2:2:INP:TopTop: p5(x0) -> ren8(x1,x0)
% 0.15/0.37 % 41:2:2:INP:TopTop: -> p4(x0),ren8(x1,x0)
% 0.15/0.37 % 42:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren8(x2,x0)
% 0.15/0.37 % 43:2:2:INP:TopTop: -> p4(x0),ren8(x1,x0)
% 0.15/0.37 % 44:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1)
% 0.15/0.37 % 45:2:2:INP:TopTop: -> p5(x0),ren9(x1,x0)
% 0.15/0.37 % 46:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren9(x2,x0)
% 0.15/0.37 % 47:2:2:INP:TopTop: p4(x0) -> ren9(x1,x0)
% 0.15/0.37 % 48:2:2:INP:TopTop: -> r1(x0,skf4(x0)),ren9(x1,x0)
% 0.15/0.37 % 49:2:2:INP:TopTop: p5(skf4(x0)) -> ren9(x1,x0)
% 0.15/0.37 % 50:2:2:INP:TopTop: -> p4(skf4(x0)),ren9(x1,x0)
% 0.15/0.37 % 51:3:3:INP:TopTopTop: r1(skf4(x0),x1) -> p4(x1),ren9(x2,x0)
% 0.15/0.37 % 52:2:2:INP:TopTop: -> p4(skf4(x0)),ren9(x1,x0)
% 0.15/0.37 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren10(x0,x1)
% 0.15/0.37 % 54:2:2:INP:TopTop: -> p5(x0),ren10(x1,x0)
% 0.15/0.37 % 55:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren10(x2,x0)
% 0.15/0.37 % 56:2:2:INP:TopTop: p4(x0) -> ren10(x1,x0)
% 0.15/0.37 % 57:2:2:INP:TopTop: p5(x0) -> ren10(x1,x0)
% 0.15/0.37 % 58:2:2:INP:TopTop: -> p4(x0),ren10(x1,x0)
% 0.15/0.37 % 59:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren10(x2,x0)
% 0.15/0.37 % 60:2:2:INP:TopTop: -> p4(x0),ren10(x1,x0)
% 0.15/0.37 % 61:2:2:INP:TopTop: -> r1(x0,x1),ren11(x0,x1)
% 0.15/0.37 % 62:2:2:INP:TopTop: p4(x0) -> ren11(x1,x0)
% 0.15/0.37 % 63:2:2:INP:TopTop: -> r1(x0,x1),ren12(x0,x1)
% 0.15/0.37 % 64:2:2:INP:TopTop: p3(x0) -> ren12(x1,x0)
% 0.15/0.37 % 65:2:2:INP:TopTop: -> r1(x0,x1),ren13(x0,x1)
% 0.15/0.37 % 66:2:2:INP:TopTop: -> r1(x0,skf5(x0)),ren13(x1,x0)
% 0.15/0.37 % 67:2:2:INP:TopTop: -> p4(skf5(x0)),ren13(x1,x0)
% 0.15/0.37 % 68:3:3:INP:TopTopTop: r1(skf5(x0),x1) -> p4(x1),ren13(x2,x0)
% 0.15/0.37 % 69:2:2:INP:TopTop: p3(skf5(x0)) -> ren13(x1,x0)
% 0.15/0.37 % 70:2:2:INP:TopTop: p4(x0) -> ren13(x1,x0)
% 0.15/0.37 % 71:2:2:INP:TopTop: -> p3(x0),ren13(x1,x0)
% 0.15/0.37 % 72:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren13(x2,x0)
% 0.15/0.37 % 73:2:2:INP:TopTop: -> p3(x0),ren13(x1,x0)
% 0.15/0.37 % 74:2:2:INP:TopTop: -> r1(x0,x1),ren14(x0,x1)
% 0.15/0.37 % 75:2:2:INP:TopTop: -> p4(x0),ren14(x1,x0)
% 0.15/0.37 % 76:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren14(x2,x0)
% 0.15/0.37 % 77:2:2:INP:TopTop: p3(x0) -> ren14(x1,x0)
% 0.15/0.37 % 78:2:2:INP:TopTop: -> r1(x0,skf6(x0)),ren14(x1,x0)
% 0.15/0.37 % 79:2:2:INP:TopTop: p4(skf6(x0)) -> ren14(x1,x0)
% 0.15/0.37 % 80:2:2:INP:TopTop: -> p3(skf6(x0)),ren14(x1,x0)
% 0.15/0.37 % 81:3:3:INP:TopTopTop: r1(skf6(x0),x1) -> p3(x1),ren14(x2,x0)
% 0.15/0.37 % 82:2:2:INP:TopTop: -> p3(skf6(x0)),ren14(x1,x0)
% 0.15/0.37 % 83:2:2:INP:TopTop: -> r1(x0,x1),ren15(x0,x1)
% 0.15/0.37 % 84:2:2:INP:TopTop: -> p4(x0),ren15(x1,x0)
% 0.15/0.37 % 85:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren15(x2,x0)
% 0.15/0.37 % 86:2:2:INP:TopTop: p3(x0) -> ren15(x1,x0)
% 0.15/0.37 % 87:2:2:INP:TopTop: p4(x0) -> ren15(x1,x0)
% 0.15/0.37 % 88:2:2:INP:TopTop: -> p3(x0),ren15(x1,x0)
% 0.15/0.37 % 89:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren15(x2,x0)
% 0.15/0.37 % 90:2:2:INP:TopTop: -> p3(x0),ren15(x1,x0)
% 0.15/0.37 % 91:2:2:INP:TopTop: -> r1(x0,x1),ren16(x0,x1)
% 0.15/0.37 % 92:2:2:INP:TopTop: p3(x0) -> ren16(x1,x0)
% 0.15/0.37 % 93:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1)
% 0.15/0.37 % 94:2:2:INP:TopTop: p2(x0) -> ren17(x1,x0)
% 0.15/0.37 % 95:2:2:INP:TopTop: -> r1(x0,x1),ren18(x0,x1)
% 0.15/0.37 % 96:2:2:INP:TopTop: -> r1(x0,skf7(x0)),ren18(x1,x0)
% 0.15/0.37 % 97:2:2:INP:TopTop: -> p3(skf7(x0)),ren18(x1,x0)
% 0.15/0.37 % 98:3:3:INP:TopTopTop: r1(skf7(x0),x1) -> p3(x1),ren18(x2,x0)
% 0.15/0.37 % 99:2:2:INP:TopTop: p2(skf7(x0)) -> ren18(x1,x0)
% 0.15/0.37 % 100:2:2:INP:TopTop: p3(x0) -> ren18(x1,x0)
% 0.15/0.37 % 101:2:2:INP:TopTop: -> p2(x0),ren18(x1,x0)
% 0.15/0.37 % 102:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren18(x2,x0)
% 0.15/0.37 % 103:2:2:INP:TopTop: -> p2(x0),ren18(x1,x0)
% 0.15/0.37 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren19(x0,x1)
% 0.15/0.37 % 105:2:2:INP:TopTop: -> p3(x0),ren19(x1,x0)
% 0.15/0.37 % 106:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren19(x2,x0)
% 0.15/0.37 % 107:2:2:INP:TopTop: p2(x0) -> ren19(x1,x0)
% 0.15/0.37 % 108:2:2:INP:TopTop: -> r1(x0,skf8(x0)),ren19(x1,x0)
% 0.15/0.37 % 109:2:2:INP:TopTop: p3(skf8(x0)) -> ren19(x1,x0)
% 0.15/0.37 % 110:2:2:INP:TopTop: -> p2(skf8(x0)),ren19(x1,x0)
% 0.15/0.37 % 111:3:3:INP:TopTopTop: r1(skf8(x0),x1) -> p2(x1),ren19(x2,x0)
% 0.15/0.37 % 112:2:2:INP:TopTop: -> p2(skf8(x0)),ren19(x1,x0)
% 0.15/0.37 % 113:2:2:INP:TopTop: -> r1(x0,x1),ren20(x0,x1)
% 0.15/0.37 % 114:2:2:INP:TopTop: -> p3(x0),ren20(x1,x0)
% 0.15/0.37 % 115:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren20(x2,x0)
% 0.15/0.37 % 116:2:2:INP:TopTop: p2(x0) -> ren20(x1,x0)
% 0.15/0.37 % 117:2:2:INP:TopTop: p3(x0) -> ren20(x1,x0)
% 0.15/0.37 % 118:2:2:INP:TopTop: -> p2(x0),ren20(x1,x0)
% 0.15/0.37 % 119:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren20(x2,x0)
% 0.15/0.37 % 120:2:2:INP:TopTop: -> p2(x0),ren20(x1,x0)
% 0.15/0.37 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren21(x0,x1)
% 0.15/0.37 % 122:2:2:INP:TopTop: p2(x0) -> ren21(x1,x0)
% 0.15/0.37 % 123:2:2:INP:TopTop: -> r1(x0,x1),ren22(x0,x1)
% 0.15/0.37 % 124:2:2:INP:TopTop: p1(x0) -> ren22(x1,x0)
% 0.15/0.37 % 125:2:2:INP:TopTop: -> r1(x0,x1),ren23(x0,x1)
% 0.15/0.37 % 126:2:2:INP:TopTop: -> r1(x0,skf9(x0)),ren23(x1,x0)
% 0.15/0.37 % 127:2:2:INP:TopTop: -> p2(skf9(x0)),ren23(x1,x0)
% 0.15/0.37 % 128:3:3:INP:TopTopTop: r1(skf9(x0),x1) -> p2(x1),ren23(x2,x0)
% 0.15/0.37 % 129:2:2:INP:TopTop: p1(skf9(x0)) -> ren23(x1,x0)
% 0.15/0.37 % 130:2:2:INP:TopTop: p2(x0) -> ren23(x1,x0)
% 0.15/0.37 % 131:2:2:INP:TopTop: -> p1(x0),ren23(x1,x0)
% 0.15/0.37 % 132:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren23(x2,x0)
% 0.15/0.37 % 133:2:2:INP:TopTop: -> p1(x0),ren23(x1,x0)
% 0.15/0.37 % 134:2:2:INP:TopTop: -> r1(x0,x1),ren24(x0,x1)
% 0.15/0.37 % 135:2:2:INP:TopTop: -> p2(x0),ren24(x1,x0)
% 0.15/0.37 % 136:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren24(x2,x0)
% 0.15/0.37 % 137:2:2:INP:TopTop: p1(x0) -> ren24(x1,x0)
% 0.15/0.37 % 138:2:2:INP:TopTop: -> r1(x0,skf10(x0)),ren24(x1,x0)
% 0.15/0.37 % 139:2:2:INP:TopTop: p2(skf10(x0)) -> ren24(x1,x0)
% 0.15/0.37 % 140:2:2:INP:TopTop: -> p1(skf10(x0)),ren24(x1,x0)
% 0.15/0.37 % 141:3:3:INP:TopTopTop: r1(skf10(x0),x1) -> p1(x1),ren24(x2,x0)
% 0.15/0.37 % 142:2:2:INP:TopTop: -> p1(skf10(x0)),ren24(x1,x0)
% 0.15/0.37 % 143:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1)
% 0.15/0.37 % 144:2:2:INP:TopTop: -> p2(x0),ren25(x1,x0)
% 0.15/0.37 % 145:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren25(x2,x0)
% 0.15/0.37 % 146:2:2:INP:TopTop: p1(x0) -> ren25(x1,x0)
% 0.15/0.37 % 147:2:2:INP:TopTop: p2(x0) -> ren25(x1,x0)
% 0.15/0.37 % 148:2:2:INP:TopTop: -> p1(x0),ren25(x1,x0)
% 0.15/0.37 % 149:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren25(x2,x0)
% 0.15/0.37 % 150:2:2:INP:TopTop: -> p1(x0),ren25(x1,x0)
% 0.15/0.37 % 151:12:2:INP:TopTop: r1(skc11,x0),p6(x0),ren1(x0,skf12(x0)),r1(skc11,x1),p5(x1),ren2(x1,skf13(x1)),p5(x1),ren3(skc11,skc14),ren4(skc11,skc15),ren5(skc11,skc16) -> p5(x0),p6(x1)
% 0.15/0.37 % 152:12:2:INP:TopTop: r1(skc11,x0),p5(x0),ren6(x0,skf17(x0)),r1(skc11,x1),p4(x1),ren7(x1,skf18(x1)),p4(x1),ren8(skc11,skc19),ren9(skc11,skc20),ren10(skc11,skc21) -> p4(x0),p5(x1)
% 0.15/0.37 % 153:12:2:INP:TopTop: r1(skc11,x0),p4(x0),ren11(x0,skf22(x0)),r1(skc11,x1),p3(x1),ren12(x1,skf23(x1)),p3(x1),ren13(skc11,skc24),ren14(skc11,skc25),ren15(skc11,skc26) -> p3(x0),p4(x1)
% 0.15/0.37 % 154:12:2:INP:TopTop: r1(skc11,x0),p3(x0),ren16(x0,skf27(x0)),r1(skc11,x1),p2(x1),ren17(x1,skf28(x1)),p2(x1),ren18(skc11,skc29),ren19(skc11,skc30),ren20(skc11,skc31) -> p2(x0),p3(x1)
% 0.15/0.37 % 155:1:0:INP:: -> r1(skc11,skc32)
% 0.15/0.37 % 156:1:0:INP:: p5(skc32) ->
% 0.15/0.37 % 157:2:1:INP:Top: r1(skc32,x0) -> p5(x0)
% 0.15/0.37 % 158:1:0:INP:: -> p5(skc32)
% 0.15/0.37 % 159:1:0:INP:: -> r1(skc11,skc33)
% 0.15/0.37 % 160:1:0:INP:: p5(skc33) ->
% 0.15/0.37 % 161:2:1:INP:Top: r1(skc33,x0) -> p5(x0)
% 0.15/0.37 % 162:1:0:INP:: -> p5(skc33)
% 0.15/0.37 % 163:12:2:INP:TopTop: r1(skc11,x0),p2(x0),ren21(x0,skf34(x0)),r1(skc11,x1),p1(x1),ren22(x1,skf35(x1)),p1(x1),ren23(skc11,skc36),ren24(skc11,skc37),ren25(skc11,skc38) -> p1(x0),p2(x1)
% 0.15/0.37
% 0.15/0.37 % Predicates: r1 p6 p5 p4 p3 p2 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25
% 0.15/0.37 % Fol Constants: skc11 skc14 skc15 skc16 skc19 skc20 skc21 skc24 skc25 skc26 skc29 skc30 skc31 skc32 skc33 skc36 skc37 skc38
% 0.15/0.37 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf12 skf13 skf17 skf18 skf22 skf23 skf27 skf28 skf34 skf35
% 0.15/0.37 % Problem Properties:
% 0.15/0.37 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.15/0.37
% 0.15/0.37
% 0.15/0.37 % Reduced Input Axiom Clauses:
% 0.15/0.37 % 1:2:2:INP:TopTop: -> r1(x0,x1),ren1(x0,x1)
% 0.15/0.37 % 2:2:2:INP:TopTop: p6(x0) -> ren1(x1,x0)
% 0.15/0.37 % 3:2:2:INP:TopTop: -> r1(x0,x1),ren2(x0,x1)
% 0.15/0.37 % 4:2:2:INP:TopTop: p5(x0) -> ren2(x1,x0)
% 0.15/0.37 % 5:2:2:INP:TopTop: -> r1(x0,x1),ren3(x0,x1)
% 0.15/0.37 % 6:2:2:INP:TopTop: -> r1(x0,skf1(x0)),ren3(x1,x0)
% 0.15/0.37 % 7:2:2:INP:TopTop: -> p6(skf1(x0)),ren3(x1,x0)
% 0.15/0.37 % 8:3:3:INP:TopTopTop: r1(skf1(x0),x1) -> p6(x1),ren3(x2,x0)
% 0.15/0.37 % 9:2:2:INP:TopTop: p5(skf1(x0)) -> ren3(x1,x0)
% 0.15/0.37 % 10:2:2:INP:TopTop: p6(x0) -> ren3(x1,x0)
% 0.15/0.37 % 12:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren3(x2,x0)
% 0.15/0.37 % 13:2:2:INP:TopTop: -> p5(x0),ren3(x1,x0)
% 0.15/0.37 % 14:2:2:INP:TopTop: -> r1(x0,x1),ren4(x0,x1)
% 0.15/0.37 % 15:2:2:INP:TopTop: -> p6(x0),ren4(x1,x0)
% 0.15/0.37 % 16:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren4(x2,x0)
% 0.15/0.37 % 17:2:2:INP:TopTop: p5(x0) -> ren4(x1,x0)
% 0.15/0.37 % 18:2:2:INP:TopTop: -> r1(x0,skf2(x0)),ren4(x1,x0)
% 0.15/0.37 % 19:2:2:INP:TopTop: p6(skf2(x0)) -> ren4(x1,x0)
% 0.15/0.37 % 21:3:3:INP:TopTopTop: r1(skf2(x0),x1) -> p5(x1),ren4(x2,x0)
% 0.15/0.37 % 22:2:2:INP:TopTop: -> p5(skf2(x0)),ren4(x1,x0)
% 0.15/0.37 % 23:2:2:INP:TopTop: -> r1(x0,x1),ren5(x0,x1)
% 0.15/0.37 % 164:1:2:[27.0,24.0]:TopTop: -> ren5(x0,x1)
% 0.15/0.37 % 165:1:2:[28.0,26.0]:TopTop: -> ren5(x0,x1)
% 0.15/0.37 % 31:2:2:INP:TopTop: -> r1(x0,x1),ren6(x0,x1)
% 0.15/0.37 % 32:2:2:INP:TopTop: p5(x0) -> ren6(x1,x0)
% 0.15/0.37 % 33:2:2:INP:TopTop: -> r1(x0,x1),ren7(x0,x1)
% 0.15/0.37 % 34:2:2:INP:TopTop: p4(x0) -> ren7(x1,x0)
% 0.15/0.37 % 35:2:2:INP:TopTop: -> r1(x0,x1),ren8(x0,x1)
% 0.15/0.37 % 36:2:2:INP:TopTop: -> r1(x0,skf3(x0)),ren8(x1,x0)
% 0.15/0.37 % 37:2:2:INP:TopTop: -> p5(skf3(x0)),ren8(x1,x0)
% 0.15/0.37 % 38:3:3:INP:TopTopTop: r1(skf3(x0),x1) -> p5(x1),ren8(x2,x0)
% 0.15/0.37 % 39:2:2:INP:TopTop: p4(skf3(x0)) -> ren8(x1,x0)
% 0.15/0.37 % 40:2:2:INP:TopTop: p5(x0) -> ren8(x1,x0)
% 0.15/0.37 % 42:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren8(x2,x0)
% 0.15/0.37 % 43:2:2:INP:TopTop: -> p4(x0),ren8(x1,x0)
% 0.15/0.37 % 44:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1)
% 0.15/0.37 % 45:2:2:INP:TopTop: -> p5(x0),ren9(x1,x0)
% 0.15/0.37 % 46:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren9(x2,x0)
% 0.15/0.37 % 47:2:2:INP:TopTop: p4(x0) -> ren9(x1,x0)
% 0.15/0.37 % 48:2:2:INP:TopTop: -> r1(x0,skf4(x0)),ren9(x1,x0)
% 0.15/0.37 % 49:2:2:INP:TopTop: p5(skf4(x0)) -> ren9(x1,x0)
% 0.15/0.37 % 51:3:3:INP:TopTopTop: r1(skf4(x0),x1) -> p4(x1),ren9(x2,x0)
% 0.15/0.37 % 52:2:2:INP:TopTop: -> p4(skf4(x0)),ren9(x1,x0)
% 0.15/0.37 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren10(x0,x1)
% 0.15/0.37 % 166:1:2:[57.0,54.0]:TopTop: -> ren10(x0,x1)
% 0.15/0.37 % 167:1:2:[58.0,56.0]:TopTop: -> ren10(x0,x1)
% 0.15/0.37 % 173:1:2:[150.0,146.0]:TopTop: -> ren25(x0,x1)
% 0.15/0.37 % 61:2:2:INP:TopTop: -> r1(x0,x1),ren11(x0,x1)
% 0.15/0.37 % 62:2:2:INP:TopTop: p4(x0) -> ren11(x1,x0)
% 0.15/0.37 % 63:2:2:INP:TopTop: -> r1(x0,x1),ren12(x0,x1)
% 0.15/0.37 % 64:2:2:INP:TopTop: p3(x0) -> ren12(x1,x0)
% 0.15/0.37 % 65:2:2:INP:TopTop: -> r1(x0,x1),ren13(x0,x1)
% 0.15/0.37 % 66:2:2:INP:TopTop: -> r1(x0,skf5(x0)),ren13(x1,x0)
% 0.15/0.37 % 67:2:2:INP:TopTop: -> p4(skf5(x0)),ren13(x1,x0)
% 0.15/0.37 % 68:3:3:INP:TopTopTop: r1(skf5(x0),x1) -> p4(x1),ren13(x2,x0)
% 0.15/0.37 % 69:2:2:INP:TopTop: p3(skf5(x0)) -> ren13(x1,x0)
% 0.15/0.37 % 70:2:2:INP:TopTop: p4(x0) -> ren13(x1,x0)
% 0.15/0.37 % 172:1:2:[147.0,144.0]:TopTop: -> ren25(x0,x1)
% 0.15/0.37 % 72:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren13(x2,x0)
% 0.15/0.37 % 73:2:2:INP:TopTop: -> p3(x0),ren13(x1,x0)
% 0.15/0.37 % 74:2:2:INP:TopTop: -> r1(x0,x1),ren14(x0,x1)
% 0.15/0.37 % 75:2:2:INP:TopTop: -> p4(x0),ren14(x1,x0)
% 0.15/0.37 % 76:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren14(x2,x0)
% 0.15/0.37 % 77:2:2:INP:TopTop: p3(x0) -> ren14(x1,x0)
% 0.15/0.37 % 78:2:2:INP:TopTop: -> r1(x0,skf6(x0)),ren14(x1,x0)
% 0.15/0.37 % 79:2:2:INP:TopTop: p4(skf6(x0)) -> ren14(x1,x0)
% 0.15/0.37 % 143:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1)
% 0.15/0.37 % 81:3:3:INP:TopTopTop: r1(skf6(x0),x1) -> p3(x1),ren14(x2,x0)
% 0.15/0.37 % 82:2:2:INP:TopTop: -> p3(skf6(x0)),ren14(x1,x0)
% 0.15/0.37 % 83:2:2:INP:TopTop: -> r1(x0,x1),ren15(x0,x1)
% 0.15/0.37 % 168:1:2:[87.0,84.0]:TopTop: -> ren15(x0,x1)
% 0.15/0.37 % 142:2:2:INP:TopTop: -> p1(skf10(x0)),ren24(x1,x0)
% 0.15/0.37 % 169:1:2:[88.0,86.0]:TopTop: -> ren15(x0,x1)
% 0.15/0.37 % 141:3:3:INP:TopTopTop: r1(skf10(x0),x1) -> p1(x1),ren24(x2,x0)
% 0.15/0.37 % 139:2:2:INP:TopTop: p2(skf10(x0)) -> ren24(x1,x0)
% 0.15/0.37 % 138:2:2:INP:TopTop: -> r1(x0,skf10(x0)),ren24(x1,x0)
% 0.15/0.37 % 137:2:2:INP:TopTop: p1(x0) -> ren24(x1,x0)
% 0.15/0.37 % 91:2:2:INP:TopTop: -> r1(x0,x1),ren16(x0,x1)
% 0.15/0.37 % 92:2:2:INP:TopTop: p3(x0) -> ren16(x1,x0)
% 0.15/0.37 % 93:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1)
% 0.15/0.37 % 94:2:2:INP:TopTop: p2(x0) -> ren17(x1,x0)
% 0.15/0.37 % 95:2:2:INP:TopTop: -> r1(x0,x1),ren18(x0,x1)
% 0.15/0.37 % 96:2:2:INP:TopTop: -> r1(x0,skf7(x0)),ren18(x1,x0)
% 0.15/0.37 % 97:2:2:INP:TopTop: -> p3(skf7(x0)),ren18(x1,x0)
% 0.15/0.37 % 98:3:3:INP:TopTopTop: r1(skf7(x0),x1) -> p3(x1),ren18(x2,x0)
% 0.15/0.37 % 99:2:2:INP:TopTop: p2(skf7(x0)) -> ren18(x1,x0)
% 0.15/0.37 % 100:2:2:INP:TopTop: p3(x0) -> ren18(x1,x0)
% 0.15/0.37 % 136:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren24(x2,x0)
% 0.15/0.37 % 102:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren18(x2,x0)
% 0.15/0.37 % 103:2:2:INP:TopTop: -> p2(x0),ren18(x1,x0)
% 0.15/0.37 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren19(x0,x1)
% 0.15/0.37 % 105:2:2:INP:TopTop: -> p3(x0),ren19(x1,x0)
% 0.15/0.37 % 106:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren19(x2,x0)
% 0.15/0.37 % 107:2:2:INP:TopTop: p2(x0) -> ren19(x1,x0)
% 0.15/0.37 % 108:2:2:INP:TopTop: -> r1(x0,skf8(x0)),ren19(x1,x0)
% 0.15/0.37 % 109:2:2:INP:TopTop: p3(skf8(x0)) -> ren19(x1,x0)
% 0.15/0.37 % 135:2:2:INP:TopTop: -> p2(x0),ren24(x1,x0)
% 0.15/0.37 % 111:3:3:INP:TopTopTop: r1(skf8(x0),x1) -> p2(x1),ren19(x2,x0)
% 0.15/0.37 % 112:2:2:INP:TopTop: -> p2(skf8(x0)),ren19(x1,x0)
% 0.15/0.37 % 113:2:2:INP:TopTop: -> r1(x0,x1),ren20(x0,x1)
% 0.15/0.37 % 170:1:2:[117.0,114.0]:TopTop: -> ren20(x0,x1)
% 0.15/0.37 % 134:2:2:INP:TopTop: -> r1(x0,x1),ren24(x0,x1)
% 0.15/0.37 % 171:1:2:[120.0,116.0]:TopTop: -> ren20(x0,x1)
% 0.15/0.37 % 133:2:2:INP:TopTop: -> p1(x0),ren23(x1,x0)
% 0.15/0.37 % 132:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren23(x2,x0)
% 0.15/0.37 % 130:2:2:INP:TopTop: p2(x0) -> ren23(x1,x0)
% 0.15/0.37 % 129:2:2:INP:TopTop: p1(skf9(x0)) -> ren23(x1,x0)
% 0.15/0.37 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren21(x0,x1)
% 0.15/0.37 % 122:2:2:INP:TopTop: p2(x0) -> ren21(x1,x0)
% 0.15/0.37 % 123:2:2:INP:TopTop: -> r1(x0,x1),ren22(x0,x1)
% 0.15/0.37 % 124:2:2:INP:TopTop: p1(x0) -> ren22(x1,x0)
% 0.15/0.37 % 125:2:2:INP:TopTop: -> r1(x0,x1),ren23(x0,x1)
% 0.15/0.37 % 126:2:2:INP:TopTop: -> r1(x0,skf9(x0)),ren23(x1,x0)
% 0.15/0.37 % 127:2:2:INP:TopTop: -> p2(skf9(x0)),ren23(x1,x0)
% 0.15/0.37 % 128:3:3:INP:TopTopTop: r1(skf9(x0),x1) -> p2(x1),ren23(x2,x0)
% 0.15/0.37
% 0.15/0.37 % Reduced Input Conjecture Clauses:
% 0.15/0.37 % 180:10:2:[172.1,163.8]:TopTop: r1(skc11,x0),p2(x0),ren21(x0,skf34(x0)),r1(skc11,x1),ren22(x1,skf35(x1)),p1(x1),ren23(skc11,skc36),ren24(skc11,skc37) -> p1(x0),p2(x1)
% 0.15/0.37 % 162:1:0:INP:: -> p5(skc33)
% 0.15/0.37 % 161:2:1:INP:Top: r1(skc33,x0) -> p5(x0)
% 0.15/0.37 % 179:0:0:[162.0,160.0]:: ->
% 0.15/0.37 % 159:1:0:INP:: -> r1(skc11,skc33)
% 0.15/0.37 % 158:1:0:INP:: -> p5(skc32)
% 0.15/0.37 % 157:2:1:INP:Top: r1(skc32,x0) -> p5(x0)
% 0.15/0.37 % 178:0:0:[158.0,156.0]:: ->
% 0.15/0.37 % 155:1:0:INP:: -> r1(skc11,skc32)
% 0.15/0.37 % 177:10:2:[171.1,154.8]:TopTop: r1(skc11,x0),p3(x0),ren16(x0,skf27(x0)),r1(skc11,x1),ren17(x1,skf28(x1)),p2(x1),ren18(skc11,skc29),ren19(skc11,skc30) -> p2(x0),p3(x1)
% 0.15/0.37 % 176:10:2:[169.1,153.8]:TopTop: r1(skc11,x0),p4(x0),ren11(x0,skf22(x0)),r1(skc11,x1),ren12(x1,skf23(x1)),p3(x1),ren13(skc11,skc24),ren14(skc11,skc25) -> p3(x0),p4(x1)
% 0.15/0.37 % 175:10:2:[166.1,152.8]:TopTop: r1(skc11,x0),p5(x0),ren6(x0,skf17(x0)),r1(skc11,x1),ren7(x1,skf18(x1)),p4(x1),ren8(skc11,skc19),ren9(skc11,skc20) -> p4(x0),p5(x1)
% 0.15/0.37 % 174:10:2:[165.1,151.8]:TopTop: r1(skc11,x0),p6(x0),ren1(x0,skf12(x0)),r1(skc11,x1),ren2(x1,skf13(x1)),p5(x1),ren3(skc11,skc14),ren4(skc11,skc15) -> p5(x0),p6(x1)
% 0.15/0.37
% 0.15/0.37 % SZS status Theorem
% 0.15/0.37
% 0.15/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.15/0.37 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.15/0.38
% 0.15/0.38 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.38
% 0.15/0.38 % SPASS-SCL-FOL Statistics:
% 0.15/0.38 % Number of learned clauses: 0
% 0.15/0.38 % Number of propagations: 0
% 0.15/0.38 % Number of decisions: 0
% 0.15/0.38 % Number of resolutions: 0
% 0.15/0.38 % Number of condensations: 0
% 0.15/0.38 % Number of sub resolutions: 17
% 0.15/0.38
% 0.15/0.38 % Needed: 0:00:00.01
% 0.15/0.38
% 0.15/0.38 % ###
% 0.15/0.38 % ### Pagesize: 8192
% 0.15/0.38 % ### Marksize: 0
% 0.15/0.38 % ### Memory demanded: 545 KBytes
% 0.15/0.38 % ### Memory freed: 545 KBytes
% 0.15/0.38 % ### Memory remaining: 0 Bytes
% 0.15/0.38 % ### Pages allocated: 141 Pages
% 0.15/0.38 % ###
%------------------------------------------------------------------------------