%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL670+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n009.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 : Fri Sep 25 02:08:01 PM UTC 2026
% Result : Theorem 188.73s 34.40s
% Output : CNFRefutation 111.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 5
% Syntax : Number of formulae : 152 ( 22 unt; 3 def)
% Number of atoms : 2290 ( 0 equ)
% Maximal formula atoms : 129 ( 15 avg)
% Number of connectives : 3611 (1749 ~;1494 |; 368 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 21 con; 0-1 aty)
% Number of variables : 1208 ( 0 sgn1036 !; 172 ?; 189 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p2(X0)
| ! [X1] :
( p3(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& p2(X0)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p2(X0)
| ! [X1] :
( p3(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& p2(X0)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ~ ! [X85] :
( ~ ! [X88] :
( ~ p1(X88)
| ~ r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( ~ p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
| ! [X46] :
( ~ ! [X81] :
( ~ ! [X84] :
( ~ p1(X84)
| ~ r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( ~ p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X46,X81) )
| ! [X51] :
( ~ ! [X77] :
( ~ ! [X80] :
( ~ p1(X80)
| ~ r1(X77,X80) )
| ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X51,X77) )
| ! [X56] :
( ~ ! [X73] :
( ~ ! [X76] :
( ~ p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( ~ p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X56,X73) )
| ! [X61] :
( ~ ! [X69] :
( ~ ! [X72] :
( ~ p1(X72)
| ~ r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( ~ p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X61,X69) )
| ! [X66] :
( ~ ! [X67] :
( ~ ! [X68] :
( p2(X68)
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X61,X66) )
| ! [X62] :
( ! [X65] :
( p1(X65)
| ~ r1(X62,X65) )
| ! [X63] :
( ~ ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X56,X61) )
| ! [X57] :
( ! [X60] :
( p1(X60)
| ~ r1(X57,X60) )
| ! [X58] :
( ~ ! [X59] :
( p1(X59)
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X51,X56) )
| ! [X52] :
( ! [X55] :
( p1(X55)
| ~ r1(X52,X55) )
| ! [X53] :
( ~ ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X46,X51) )
| ! [X47] :
( ! [X50] :
( p1(X50)
| ~ r1(X47,X50) )
| ! [X48] :
( ~ ! [X49] :
( p1(X49)
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X0,X46) )
| ! [X42] :
( ! [X45] :
( p1(X45)
| ~ r1(X42,X45) )
| ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X0,X42) )
| ~ ! [X38] :
( ~ ( ! [X41] :
( p1(X41)
| ~ r1(X38,X41) )
& ~ ! [X39] :
( ! [X40] :
( p1(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) ) )
| ~ r1(X0,X38) )
| ~ ! [X2] :
( ~ ( ~ ! [X34] :
( ~ ( ! [X37] :
( p1(X37)
| ~ r1(X34,X37) )
& ~ ! [X35] :
( ! [X36] :
( p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X34,X35) ) )
| ~ r1(X2,X34) )
| ~ ! [X3] :
( ~ ( ~ ! [X30] :
( ~ ( ! [X33] :
( p1(X33)
| ~ r1(X30,X33) )
& ~ ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X3,X30) )
| ~ ! [X4] :
( ~ ( ~ ! [X26] :
( ~ ( ! [X29] :
( p1(X29)
| ~ r1(X26,X29) )
& ~ ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) ) )
| ~ r1(X4,X26) )
| ~ ! [X5] :
( ~ ( ~ ! [X22] :
( ~ ( ! [X25] :
( p1(X25)
| ~ r1(X22,X25) )
& ~ ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X5,X22) )
| ~ ! [X6] :
( ~ ( ( ! [X20] :
( ~ ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X6,X20) )
& ~ ! [X16] :
( ! [X17] :
( ~ ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p3(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) )
| ~ ! [X10] :
( ~ ( ~ ! [X13] :
( ~ ! [X14] :
( ~ ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X10,X13) )
& p2(X10)
& ~ ! [X11] :
( ~ ( ~ p2(X11)
| ! [X12] :
( p3(X12)
| ~ r1(X11,X12) ) )
| ~ r1(X10,X11) ) )
| ~ r1(X6,X10) )
| ~ ! [X7] :
( ~ ! [X8] :
( ~ p2(X8)
| ! [X9] :
( p3(X9)
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ! [X85] :
( ~ ! [X88] :
( ~ p1(X88)
| ~ r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( ~ p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
| ! [X46] :
( ~ ! [X81] :
( ~ ! [X84] :
( ~ p1(X84)
| ~ r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( ~ p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X46,X81) )
| ! [X51] :
( ~ ! [X77] :
( ~ ! [X80] :
( ~ p1(X80)
| ~ r1(X77,X80) )
| ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X51,X77) )
| ! [X56] :
( ~ ! [X73] :
( ~ ! [X76] :
( ~ p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( ~ p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X56,X73) )
| ! [X61] :
( ~ ! [X69] :
( ~ ! [X72] :
( ~ p1(X72)
| ~ r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( ~ p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X61,X69) )
| ! [X66] :
( ~ ! [X67] :
( ~ ! [X68] :
( p2(X68)
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X61,X66) )
| ! [X62] :
( ! [X65] :
( p1(X65)
| ~ r1(X62,X65) )
| ! [X63] :
( ~ ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X56,X61) )
| ! [X57] :
( ! [X60] :
( p1(X60)
| ~ r1(X57,X60) )
| ! [X58] :
( ~ ! [X59] :
( p1(X59)
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X51,X56) )
| ! [X52] :
( ! [X55] :
( p1(X55)
| ~ r1(X52,X55) )
| ! [X53] :
( ~ ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X46,X51) )
| ! [X47] :
( ! [X50] :
( p1(X50)
| ~ r1(X47,X50) )
| ! [X48] :
( ~ ! [X49] :
( p1(X49)
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X0,X46) )
| ! [X42] :
( ! [X45] :
( p1(X45)
| ~ r1(X42,X45) )
| ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X0,X42) )
| ~ ! [X38] :
( ~ ( ! [X41] :
( p1(X41)
| ~ r1(X38,X41) )
& ~ ! [X39] :
( ! [X40] :
( p1(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) ) )
| ~ r1(X0,X38) )
| ~ ! [X2] :
( ~ ( ~ ! [X34] :
( ~ ( ! [X37] :
( p1(X37)
| ~ r1(X34,X37) )
& ~ ! [X35] :
( ! [X36] :
( p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X34,X35) ) )
| ~ r1(X2,X34) )
| ~ ! [X3] :
( ~ ( ~ ! [X30] :
( ~ ( ! [X33] :
( p1(X33)
| ~ r1(X30,X33) )
& ~ ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X3,X30) )
| ~ ! [X4] :
( ~ ( ~ ! [X26] :
( ~ ( ! [X29] :
( p1(X29)
| ~ r1(X26,X29) )
& ~ ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) ) )
| ~ r1(X4,X26) )
| ~ ! [X5] :
( ~ ( ~ ! [X22] :
( ~ ( ! [X25] :
( p1(X25)
| ~ r1(X22,X25) )
& ~ ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X5,X22) )
| ~ ! [X6] :
( ~ ( ( ! [X20] :
( ~ ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X6,X20) )
& ~ ! [X16] :
( ! [X17] :
( ~ ! [X18] :
( ~ p2(X18)
| ! [X19] :
( p3(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) )
| ~ ! [X10] :
( ~ ( ~ ! [X13] :
( ~ ! [X14] :
( ~ ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X10,X13) )
& p2(X10)
& ~ ! [X11] :
( ~ ( ~ p2(X11)
| ! [X12] :
( p3(X12)
| ~ r1(X11,X12) ) )
| ~ r1(X10,X11) ) )
| ~ r1(X6,X10) )
| ~ ! [X7] :
( ~ ! [X8] :
( ~ p2(X8)
| ! [X9] :
( p3(X9)
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ~ ! [X85] :
( ~ ! [X88] :
( ~ p1(X88)
| ~ r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( ~ p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
| ! [X46] :
( ~ ! [X81] :
( ~ ! [X84] :
( ~ p1(X84)
| ~ r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( ~ p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X46,X81) )
| ! [X51] :
( ~ ! [X77] :
( ~ ! [X80] :
( ~ p1(X80)
| ~ r1(X77,X80) )
| ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X51,X77) )
| ! [X56] :
( ~ ! [X73] :
( ~ ! [X76] :
( ~ p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( ~ p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X56,X73) )
| ! [X61] :
( ~ ! [X69] :
( ~ ! [X72] :
( ~ p1(X72)
| ~ r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( ~ p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X61,X69) )
| ! [X66] :
( ~ ! [X67] :
( ~ ! [X68] :
( p2(X68)
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X61,X66) )
| ! [X62] :
( ! [X65] :
( p1(X65)
| ~ r1(X62,X65) )
| ! [X63] :
( ~ ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X56,X61) )
| ! [X57] :
( ! [X60] :
( p1(X60)
| ~ r1(X57,X60) )
| ! [X58] :
( ~ ! [X59] :
( p1(X59)
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X51,X56) )
| ! [X52] :
( ! [X55] :
( p1(X55)
| ~ r1(X52,X55) )
| ! [X53] :
( ~ ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X46,X51) )
| ! [X47] :
( ! [X50] :
( p1(X50)
| ~ r1(X47,X50) )
| ! [X48] :
( ~ ! [X49] :
( p1(X49)
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X0,X46) )
| ! [X42] :
( ! [X45] :
( p1(X45)
| ~ r1(X42,X45) )
| ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X0,X42) )
| ~ ! [X38] :
( ~ ( ! [X41] :
( p1(X41)
| ~ r1(X38,X41) )
& ~ ! [X39] :
( ! [X40] :
( p1(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) ) )
| ~ r1(X0,X38) )
| ~ ! [X2] :
( ~ ( ~ ! [X34] :
( ~ ( ! [X37] :
( p1(X37)
| ~ r1(X34,X37) )
& ~ ! [X35] :
( ! [X36] :
( p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X34,X35) ) )
| ~ r1(X2,X34) )
| ~ ! [X3] :
( ~ ( ~ ! [X30] :
( ~ ( ! [X33] :
( p1(X33)
| ~ r1(X30,X33) )
& ~ ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X3,X30) )
| ~ ! [X4] :
( ~ ( ~ ! [X26] :
( ~ ( ! [X29] :
( p1(X29)
| ~ r1(X26,X29) )
& ~ ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) ) )
| ~ r1(X4,X26) )
| ~ ! [X5] :
( ~ ( ~ ! [X22] :
( ~ ( ! [X25] :
( p1(X25)
| ~ r1(X22,X25) )
& ~ ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X5,X22) )
| ~ ! [X6] :
( ~ ( ( ! [X20] :
( ~ ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X6,X20) )
& ~ ! [X16] :
( ! [X17] :
( ~ ! [X18] :
( ~ p2(X18)
| ! [X19] : ~ r1(X18,X19)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) )
| ~ ! [X10] :
( ~ ( ~ ! [X13] :
( ~ ! [X14] :
( ~ ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X10,X13) )
& p2(X10)
& ~ ! [X11] :
( ~ ( ~ p2(X11)
| ! [X12] : ~ r1(X11,X12) )
| ~ r1(X10,X11) ) )
| ~ r1(X6,X10) )
| ~ ! [X7] :
( ~ ! [X8] :
( ~ p2(X8)
| ! [X9] : ~ r1(X8,X9)
| ~ r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(pure_predicate_removal,[],[f5]) ).
fof(f7,plain,
? [X0] :
~ ( ~ ! [X85] :
( ~ ! [X88] :
( ~ p1(X88)
| ~ r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( ~ p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
| ! [X46] :
( ~ ! [X81] :
( ~ ! [X84] :
( ~ p1(X84)
| ~ r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( ~ p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X46,X81) )
| ! [X51] :
( ~ ! [X77] :
( ~ ! [X80] :
( ~ p1(X80)
| ~ r1(X77,X80) )
| ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X51,X77) )
| ! [X56] :
( ~ ! [X73] :
( ~ ! [X76] :
( ~ p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( ~ p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X56,X73) )
| ! [X61] :
( ~ ! [X69] :
( ~ ! [X72] :
( ~ p1(X72)
| ~ r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( ~ p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X61,X69) )
| ! [X66] :
( ~ ! [X67] :
( ~ ! [X68] :
( p2(X68)
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X61,X66) )
| ! [X62] :
( ! [X65] :
( p1(X65)
| ~ r1(X62,X65) )
| ! [X63] :
( ~ ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X56,X61) )
| ! [X57] :
( ! [X60] :
( p1(X60)
| ~ r1(X57,X60) )
| ! [X58] :
( ~ ! [X59] :
( p1(X59)
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X51,X56) )
| ! [X52] :
( ! [X55] :
( p1(X55)
| ~ r1(X52,X55) )
| ! [X53] :
( ~ ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X46,X51) )
| ! [X47] :
( ! [X50] :
( p1(X50)
| ~ r1(X47,X50) )
| ! [X48] :
( ~ ! [X49] :
( p1(X49)
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X0,X46) )
| ! [X42] :
( ! [X45] :
( p1(X45)
| ~ r1(X42,X45) )
| ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X0,X42) )
| ~ ! [X38] :
( ~ ( ! [X41] :
( p1(X41)
| ~ r1(X38,X41) )
& ~ ! [X39] :
( ! [X40] :
( p1(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) ) )
| ~ r1(X0,X38) )
| ~ ! [X2] :
( ~ ( ~ ! [X34] :
( ~ ( ! [X37] :
( p1(X37)
| ~ r1(X34,X37) )
& ~ ! [X35] :
( ! [X36] :
( p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X34,X35) ) )
| ~ r1(X2,X34) )
| ~ ! [X3] :
( ~ ( ~ ! [X30] :
( ~ ( ! [X33] :
( p1(X33)
| ~ r1(X30,X33) )
& ~ ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X3,X30) )
| ~ ! [X4] :
( ~ ( ~ ! [X26] :
( ~ ( ! [X29] :
( p1(X29)
| ~ r1(X26,X29) )
& ~ ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) ) )
| ~ r1(X4,X26) )
| ~ ! [X5] :
( ~ ( ~ ! [X22] :
( ~ ( ! [X25] :
( p1(X25)
| ~ r1(X22,X25) )
& ~ ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X5,X22) )
| ~ ! [X6] :
( ~ ( ( ! [X20] :
( ~ ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
| ~ r1(X6,X20) )
& ~ ! [X16] :
( ! [X17] :
( ~ ! [X18] :
( ~ p2(X18)
| ! [X19] : ~ r1(X18,X19)
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) )
| ~ ! [X10] :
( ~ ( ~ ! [X13] :
( ~ ! [X14] :
( ~ ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X10,X13) )
& p2(X10)
& ~ ! [X11] :
( ~ ( ~ p2(X11)
| ! [X12] : ~ r1(X11,X12) )
| ~ r1(X10,X11) ) )
| ~ r1(X6,X10) )
| ~ ! [X7] :
( ~ ! [X8] :
( ~ p2(X8)
| ! [X9] : ~ r1(X8,X9)
| ~ r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) ) ),
inference(pure_predicate_removal,[],[f6]) ).
fof(f8,plain,
? [X0] :
( ! [X85] :
( ? [X88] :
( p1(X88)
& r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( ~ p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
& ? [X46] :
( ! [X81] :
( ? [X84] :
( p1(X84)
& r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( ~ p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X46,X81) )
& ? [X51] :
( ! [X77] :
( ? [X80] :
( p1(X80)
& r1(X77,X80) )
| ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X51,X77) )
& ? [X56] :
( ! [X73] :
( ? [X76] :
( p1(X76)
& r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( ~ p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X56,X73) )
& ? [X61] :
( ! [X69] :
( ? [X72] :
( p1(X72)
& r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( ~ p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X61,X69) )
& ? [X66] :
( ! [X67] :
( ? [X68] :
( ~ p2(X68)
& r1(X67,X68) )
| ~ r1(X66,X67) )
& r1(X61,X66) )
& ? [X62] :
( ? [X65] :
( ~ p1(X65)
& r1(X62,X65) )
& ? [X63] :
( ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
& r1(X62,X63) )
& r1(X61,X62) )
& r1(X56,X61) )
& ? [X57] :
( ? [X60] :
( ~ p1(X60)
& r1(X57,X60) )
& ? [X58] :
( ! [X59] :
( p1(X59)
| ~ r1(X58,X59) )
& r1(X57,X58) )
& r1(X56,X57) )
& r1(X51,X56) )
& ? [X52] :
( ? [X55] :
( ~ p1(X55)
& r1(X52,X55) )
& ? [X53] :
( ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
& r1(X52,X53) )
& r1(X51,X52) )
& r1(X46,X51) )
& ? [X47] :
( ? [X50] :
( ~ p1(X50)
& r1(X47,X50) )
& ? [X48] :
( ! [X49] :
( p1(X49)
| ~ r1(X48,X49) )
& r1(X47,X48) )
& r1(X46,X47) )
& r1(X0,X46) )
& ? [X42] :
( ? [X45] :
( ~ p1(X45)
& r1(X42,X45) )
& ? [X43] :
( ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
& r1(X42,X43) )
& r1(X0,X42) )
& ! [X38] :
( ? [X41] :
( ~ p1(X41)
& r1(X38,X41) )
| ! [X39] :
( ! [X40] :
( p1(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X0,X38) )
& ! [X2] :
( ( ! [X34] :
( ? [X37] :
( ~ p1(X37)
& r1(X34,X37) )
| ! [X35] :
( ! [X36] :
( p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X2,X34) )
& ! [X3] :
( ( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X3,X30) )
& ! [X4] :
( ( ! [X26] :
( ? [X29] :
( ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X4,X26) )
& ! [X5] :
( ( ! [X22] :
( ? [X25] :
( ~ p1(X25)
& r1(X22,X25) )
| ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X5,X22) )
& ! [X6] :
( ( ( ? [X20] :
( ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
& r1(X6,X20) )
| ! [X16] :
( ! [X17] :
( ? [X18] :
( p2(X18)
& ? [X19] : r1(X18,X19)
& r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) )
& ! [X10] :
( ! [X13] :
( ? [X14] :
( ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
& r1(X13,X14) )
| ~ r1(X10,X13) )
| ~ p2(X10)
| ! [X11] :
( ( p2(X11)
& ? [X12] : r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X6,X10) )
& ! [X7] :
( ? [X8] :
( p2(X8)
& ? [X9] : r1(X8,X9)
& r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
? [X0] :
( ! [X85] :
( ? [X88] :
( p1(X88)
& r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( ~ p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
& ? [X46] :
( ! [X81] :
( ? [X84] :
( p1(X84)
& r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( ~ p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X46,X81) )
& ? [X51] :
( ! [X77] :
( ? [X80] :
( p1(X80)
& r1(X77,X80) )
| ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X51,X77) )
& ? [X56] :
( ! [X73] :
( ? [X76] :
( p1(X76)
& r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( ~ p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X56,X73) )
& ? [X61] :
( ! [X69] :
( ? [X72] :
( p1(X72)
& r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( ~ p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X61,X69) )
& ? [X66] :
( ! [X67] :
( ? [X68] :
( ~ p2(X68)
& r1(X67,X68) )
| ~ r1(X66,X67) )
& r1(X61,X66) )
& ? [X62] :
( ? [X65] :
( ~ p1(X65)
& r1(X62,X65) )
& ? [X63] :
( ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
& r1(X62,X63) )
& r1(X61,X62) )
& r1(X56,X61) )
& ? [X57] :
( ? [X60] :
( ~ p1(X60)
& r1(X57,X60) )
& ? [X58] :
( ! [X59] :
( p1(X59)
| ~ r1(X58,X59) )
& r1(X57,X58) )
& r1(X56,X57) )
& r1(X51,X56) )
& ? [X52] :
( ? [X55] :
( ~ p1(X55)
& r1(X52,X55) )
& ? [X53] :
( ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
& r1(X52,X53) )
& r1(X51,X52) )
& r1(X46,X51) )
& ? [X47] :
( ? [X50] :
( ~ p1(X50)
& r1(X47,X50) )
& ? [X48] :
( ! [X49] :
( p1(X49)
| ~ r1(X48,X49) )
& r1(X47,X48) )
& r1(X46,X47) )
& r1(X0,X46) )
& ? [X42] :
( ? [X45] :
( ~ p1(X45)
& r1(X42,X45) )
& ? [X43] :
( ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
& r1(X42,X43) )
& r1(X0,X42) )
& ! [X38] :
( ? [X41] :
( ~ p1(X41)
& r1(X38,X41) )
| ! [X39] :
( ! [X40] :
( p1(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X0,X38) )
& ! [X2] :
( ( ! [X34] :
( ? [X37] :
( ~ p1(X37)
& r1(X34,X37) )
| ! [X35] :
( ! [X36] :
( p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X2,X34) )
& ! [X3] :
( ( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X3,X30) )
& ! [X4] :
( ( ! [X26] :
( ? [X29] :
( ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X4,X26) )
& ! [X5] :
( ( ! [X22] :
( ? [X25] :
( ~ p1(X25)
& r1(X22,X25) )
| ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X5,X22) )
& ! [X6] :
( ( ( ? [X20] :
( ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
& r1(X6,X20) )
| ! [X16] :
( ! [X17] :
( ? [X18] :
( p2(X18)
& ? [X19] : r1(X18,X19)
& r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) )
& ! [X10] :
( ! [X13] :
( ? [X14] :
( ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
& r1(X13,X14) )
| ~ r1(X10,X13) )
| ~ p2(X10)
| ! [X11] :
( ( p2(X11)
& ? [X12] : r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X6,X10) )
& ! [X7] :
( ? [X8] :
( p2(X8)
& ? [X9] : r1(X8,X9)
& r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) ) ),
inference(flattening,[],[f8]) ).
fof(f14,plain,
! [X2] :
( ~ sP2(X2)
| ! [X3] :
( ( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X3,X30) )
& ! [X4] :
( ( ! [X26] :
( ? [X29] :
( ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X4,X26) )
& ! [X5] :
( ( ! [X22] :
( ? [X25] :
( ~ p1(X25)
& r1(X22,X25) )
| ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X5,X22) )
& sP1(X5) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f15,plain,
! [X0] :
( ~ sP2(X0)
| ! [X1] :
( ( ! [X12] :
( ? [X15] :
( ~ p1(X15)
& r1(X12,X15) )
| ! [X13] :
( ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X1,X12) )
& ! [X2] :
( ( ! [X8] :
( ? [X11] :
( ~ p1(X11)
& r1(X8,X11) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X2,X8) )
& ! [X3] :
( ( ! [X4] :
( ? [X7] :
( ~ p1(X7)
& r1(X4,X7) )
| ! [X5] :
( ! [X6] :
( p1(X6)
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
& sP1(X3) )
| ~ r1(X2,X3) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f14]) ).
fof(f16,plain,
! [X0] :
( ~ sP2(X0)
| ! [X1] :
( ( ! [X12] :
( ( ~ p1(sK5(X12))
& r1(X12,sK5(X12)) )
| ! [X13] :
( ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X1,X12) )
& ! [X2] :
( ( ! [X8] :
( ( ~ p1(sK4(X8))
& r1(X8,sK4(X8)) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X2,X8) )
& ! [X3] :
( ( ! [X4] :
( ( ~ p1(sK3(X4))
& r1(X4,sK3(X4)) )
| ! [X5] :
( ! [X6] :
( p1(X6)
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
& sP1(X3) )
| ~ r1(X2,X3) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X7,sK3(X4)),skolemize(X11,sK4(X8)),skolemize(X15,sK5(X12))],[f15]) ).
fof(f17,plain,
! [X5] :
( ~ sP1(X5)
| ! [X6] :
( ( sP0(X6)
& ! [X10] :
( ! [X13] :
( ? [X14] :
( ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
& r1(X13,X14) )
| ~ r1(X10,X13) )
| ~ p2(X10)
| ! [X11] :
( ( p2(X11)
& ? [X12] : r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X6,X10) )
& ! [X7] :
( ? [X8] :
( p2(X8)
& ? [X9] : r1(X8,X9)
& r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f18,plain,
! [X0] :
( ~ sP1(X0)
| ! [X1] :
( ( sP0(X1)
& ! [X5] :
( ! [X8] :
( ? [X9] :
( ! [X10] :
( ~ p2(X10)
| ~ r1(X9,X10) )
& r1(X8,X9) )
| ~ r1(X5,X8) )
| ~ p2(X5)
| ! [X6] :
( ( p2(X6)
& ? [X7] : r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X1,X5) )
& ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] : r1(X3,X4)
& r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f17]) ).
fof(f19,plain,
! [X0] :
( ~ sP1(X0)
| ! [X1] :
( ( sP0(X1)
& ! [X5] :
( ! [X8] :
( ( ! [X10] :
( ~ p2(X10)
| ~ r1(sK9(X8),X10) )
& r1(X8,sK9(X8)) )
| ~ r1(X5,X8) )
| ~ p2(X5)
| ! [X6] :
( ( p2(X6)
& r1(X6,sK8(X6)) )
| ~ r1(X5,X6) )
| ~ r1(X1,X5) )
& ! [X2] :
( ( p2(sK6(X2))
& r1(sK6(X2),sK7(X2))
& r1(X2,sK6(X2)) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9]),skolemize(X3,sK6(X2)),skolemize(X4,sK7(X2)),skolemize(X7,sK8(X6)),skolemize(X9,sK9(X8))],[f18]) ).
fof(f23,plain,
? [X0] :
( ! [X53] :
( ? [X56] :
( p1(X56)
& r1(X53,X56) )
| ! [X54] :
( ! [X55] :
( ~ p1(X55)
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X0,X53) )
& ? [X14] :
( ! [X49] :
( ? [X52] :
( p1(X52)
& r1(X49,X52) )
| ! [X50] :
( ! [X51] :
( ~ p1(X51)
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X14,X49) )
& ? [X19] :
( ! [X45] :
( ? [X48] :
( p1(X48)
& r1(X45,X48) )
| ! [X46] :
( ! [X47] :
( ~ p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(X19,X45) )
& ? [X24] :
( ! [X41] :
( ? [X44] :
( p1(X44)
& r1(X41,X44) )
| ! [X42] :
( ! [X43] :
( ~ p1(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X24,X41) )
& ? [X29] :
( ! [X37] :
( ? [X40] :
( p1(X40)
& r1(X37,X40) )
| ! [X38] :
( ! [X39] :
( ~ p1(X39)
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X29,X37) )
& ? [X34] :
( ! [X35] :
( ? [X36] :
( ~ p2(X36)
& r1(X35,X36) )
| ~ r1(X34,X35) )
& r1(X29,X34) )
& ? [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
& ? [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
& r1(X30,X31) )
& r1(X29,X30) )
& r1(X24,X29) )
& ? [X25] :
( ? [X28] :
( ~ p1(X28)
& r1(X25,X28) )
& ? [X26] :
( ! [X27] :
( p1(X27)
| ~ r1(X26,X27) )
& r1(X25,X26) )
& r1(X24,X25) )
& r1(X19,X24) )
& ? [X20] :
( ? [X23] :
( ~ p1(X23)
& r1(X20,X23) )
& ? [X21] :
( ! [X22] :
( p1(X22)
| ~ r1(X21,X22) )
& r1(X20,X21) )
& r1(X19,X20) )
& r1(X14,X19) )
& ? [X15] :
( ? [X18] :
( ~ p1(X18)
& r1(X15,X18) )
& ? [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
& r1(X15,X16) )
& r1(X14,X15) )
& r1(X0,X14) )
& ? [X10] :
( ? [X13] :
( ~ p1(X13)
& r1(X10,X13) )
& ? [X11] :
( ! [X12] :
( p1(X12)
| ~ r1(X11,X12) )
& r1(X10,X11) )
& r1(X0,X10) )
& ! [X6] :
( ? [X9] :
( ~ p1(X9)
& r1(X6,X9) )
| ! [X7] :
( ! [X8] :
( p1(X8)
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X0,X6) )
& ! [X1] :
( ( ! [X2] :
( ? [X5] :
( ~ p1(X5)
& r1(X2,X5) )
| ! [X3] :
( ! [X4] :
( p1(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
& sP2(X1) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f13]) ).
fof(f24,plain,
( ! [X53] :
( ( p1(sK41(X53))
& r1(X53,sK41(X53)) )
| ! [X54] :
( ! [X55] :
( ~ p1(X55)
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(sK13,X53) )
& ! [X49] :
( ( p1(sK40(X49))
& r1(X49,sK40(X49)) )
| ! [X50] :
( ! [X51] :
( ~ p1(X51)
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(sK19,X49) )
& ! [X45] :
( ( p1(sK39(X45))
& r1(X45,sK39(X45)) )
| ! [X46] :
( ! [X47] :
( ~ p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(sK23,X45) )
& ! [X41] :
( ( p1(sK38(X41))
& r1(X41,sK38(X41)) )
| ! [X42] :
( ! [X43] :
( ~ p1(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(sK27,X41) )
& ! [X37] :
( ( p1(sK37(X37))
& r1(X37,sK37(X37)) )
| ! [X38] :
( ! [X39] :
( ~ p1(X39)
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(sK31,X37) )
& ! [X35] :
( ( ~ p2(sK36(X35))
& r1(X35,sK36(X35)) )
| ~ r1(sK35,X35) )
& r1(sK31,sK35)
& ~ p1(sK34)
& r1(sK32,sK34)
& ! [X32] :
( p1(X32)
| ~ r1(sK33,X32) )
& r1(sK32,sK33)
& r1(sK31,sK32)
& r1(sK27,sK31)
& ~ p1(sK30)
& r1(sK28,sK30)
& ! [X27] :
( p1(X27)
| ~ r1(sK29,X27) )
& r1(sK28,sK29)
& r1(sK27,sK28)
& r1(sK23,sK27)
& ~ p1(sK26)
& r1(sK24,sK26)
& ! [X22] :
( p1(X22)
| ~ r1(sK25,X22) )
& r1(sK24,sK25)
& r1(sK23,sK24)
& r1(sK19,sK23)
& ~ p1(sK22)
& r1(sK20,sK22)
& ! [X17] :
( p1(X17)
| ~ r1(sK21,X17) )
& r1(sK20,sK21)
& r1(sK19,sK20)
& r1(sK13,sK19)
& ~ p1(sK18)
& r1(sK16,sK18)
& ! [X12] :
( p1(X12)
| ~ r1(sK17,X12) )
& r1(sK16,sK17)
& r1(sK13,sK16)
& ! [X6] :
( ( ~ p1(sK15(X6))
& r1(X6,sK15(X6)) )
| ! [X7] :
( ! [X8] :
( p1(X8)
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(sK13,X6) )
& ! [X1] :
( ( ! [X2] :
( ( ~ p1(sK14(X2))
& r1(X2,sK14(X2)) )
| ! [X3] :
( ! [X4] :
( p1(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
& sP2(X1) )
| ~ r1(sK13,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41]),skolemize(X0,sK13),skolemize(X5,sK14(X2)),skolemize(X9,sK15(X6)),skolemize(X10,sK16),skolemize(X11,sK17),skolemize(X13,sK18),skolemize(X14,sK19),skolemize(X15,sK20),skolemize(X16,sK21),skolemize(X18,sK22),skolemize(X19,sK23),skolemize(X20,sK24),skolemize(X21,sK25),skolemize(X23,sK26),skolemize(X24,sK27),skolemize(X25,sK28),skolemize(X26,sK29),skolemize(X28,sK30),skolemize(X29,sK31),skolemize(X30,sK32),skolemize(X31,sK33),skolemize(X33,sK34),skolemize(X34,sK35),skolemize(X36,sK36(X35)),skolemize(X40,sK37(X37)),skolemize(X44,sK38(X41)),skolemize(X48,sK39(X45)),skolemize(X52,sK40(X49)),skolemize(X56,sK41(X53))],[f23]) ).
fof(f25,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f32,plain,
! [X2,X3,X0,X1] :
( ~ sP2(X0)
| sP1(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f33,plain,
! [X0,X1] :
( ~ sP1(X0)
| sP0(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f34,plain,
! [X10,X0,X1,X8,X6,X5] :
( ~ sP1(X0)
| ~ p2(X10)
| ~ r1(sK9(X8),X10)
| ~ r1(X5,X8)
| ~ p2(X5)
| p2(X6)
| ~ r1(X5,X6)
| ~ r1(X1,X5)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f35,plain,
! [X0,X1,X8,X6,X5] :
( ~ sP1(X0)
| r1(X8,sK9(X8))
| ~ r1(X5,X8)
| ~ p2(X5)
| p2(X6)
| ~ r1(X5,X6)
| ~ r1(X1,X5)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f38,plain,
! [X2,X0,X1] :
( ~ sP1(X0)
| p2(sK6(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f40,plain,
! [X2,X0,X1] :
( ~ sP1(X0)
| r1(X2,sK6(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f57,plain,
! [X35] :
( ~ p2(sK36(X35))
| ~ r1(sK35,X35) ),
inference(cnf_transformation,[],[f24]) ).
fof(f58,plain,
! [X35] :
( r1(X35,sK36(X35))
| ~ r1(sK35,X35) ),
inference(cnf_transformation,[],[f24]) ).
fof(f59,plain,
r1(sK31,sK35),
inference(cnf_transformation,[],[f24]) ).
fof(f65,plain,
r1(sK27,sK31),
inference(cnf_transformation,[],[f24]) ).
fof(f71,plain,
r1(sK23,sK27),
inference(cnf_transformation,[],[f24]) ).
fof(f77,plain,
r1(sK19,sK23),
inference(cnf_transformation,[],[f24]) ).
fof(f83,plain,
r1(sK13,sK19),
inference(cnf_transformation,[],[f24]) ).
fof(f93,plain,
! [X1] :
( sP2(X1)
| ~ r1(sK13,X1) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f25]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1(X3)
| ~ sP2(X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK6(X2))
| ~ sP1(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK6(X2))
| ~ sP1(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(X3)
| r1(X4,sK9(X4))
| ~ p2(X2)
| ~ sP1(X0)
| ~ r1(X2,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X5)
| ~ p2(X4)
| ~ p2(X1)
| ~ sP1(X2)
| ~ r1(X4,X5)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(sK9(X0),X1) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| ~ sP1(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_71,negated_conjecture,
! [X0: $i] :
( sP2(X0)
| ~ r1(sK13,X0) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_81,negated_conjecture,
r1(sK13,sK19),
inference(cnf_transformation,[],[f83]) ).
tcf(c_87,negated_conjecture,
r1(sK19,sK23),
inference(cnf_transformation,[],[f77]) ).
tcf(c_93,negated_conjecture,
r1(sK23,sK27),
inference(cnf_transformation,[],[f71]) ).
tcf(c_99,negated_conjecture,
r1(sK27,sK31),
inference(cnf_transformation,[],[f65]) ).
tcf(c_105,negated_conjecture,
r1(sK31,sK35),
inference(cnf_transformation,[],[f59]) ).
tcf(c_106,negated_conjecture,
! [X0: $i] :
( r1(X0,sK36(X0))
| ~ r1(sK35,X0) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_107,negated_conjecture,
! [X0: $i] :
( ~ p2(sK36(X0))
| ~ r1(sK35,X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_118,plain,
r1(sK13,sK13),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_982,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1(X3)
| ~ r1(sK13,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_71,c_50]) ).
tcf(c_3137,plain,
( sP0(sK27)
| ~ sP1(sK23) ),
inference(superposition,[status(thm)],[c_93,c_64]) ).
tcf(c_3145,plain,
( sP0(sK35)
| ~ sP1(sK31) ),
inference(superposition,[status(thm)],[c_105,c_64]) ).
tcf(c_3257,plain,
! [X0: $i] :
( p2(sK6(X0))
| ~ sP1(sK23)
| ~ r1(sK27,X0) ),
inference(superposition,[status(thm)],[c_93,c_59]) ).
tcf(c_3265,plain,
! [X0: $i] :
( p2(sK6(X0))
| ~ sP1(sK31)
| ~ r1(sK35,X0) ),
inference(superposition,[status(thm)],[c_105,c_59]) ).
tcf(c_3603,plain,
! [X0: $i] :
( r1(X0,sK6(X0))
| ~ sP1(sK23)
| ~ r1(sK27,X0) ),
inference(superposition,[status(thm)],[c_93,c_57]) ).
tcf(c_3611,plain,
! [X0: $i] :
( r1(X0,sK6(X0))
| ~ sP1(sK31)
| ~ r1(sK35,X0) ),
inference(superposition,[status(thm)],[c_105,c_57]) ).
tcf(c_5285,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(X1)
| r1(X2,sK9(X2))
| ~ sP1(X4)
| ~ p2(sK10(X0))
| ~ r1(X4,X3)
| ~ r1(X3,sK10(X0))
| ~ r1(sK10(X0),X2)
| ~ r1(sK10(X0),X1) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_5326,plain,
( r1(sK10(sK35),sK36(sK10(sK35)))
| ~ r1(sK35,sK10(sK35)) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_16631,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(X1)
| r1(sK10(X0),sK9(sK10(X0)))
| ~ sP1(X3)
| ~ p2(sK10(X0))
| ~ r1(X3,X2)
| ~ r1(X2,sK10(X0))
| ~ r1(sK10(X0),X1)
| ~ r1(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_5285]) ).
tcf(c_16632,plain,
! [X0: $i] : r1(sK10(X0),sK10(X0)),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_49115,plain,
! [X0: $i] : r1(sK9(X0),sK9(X0)),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_49225,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK23)
| ~ r1(sK13,X0)
| ~ r1(X2,sK23)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_49229,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(sK31)
| ~ r1(sK13,X0)
| ~ r1(X2,sK31)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_51647,plain,
! [X0: $i,X1: $i] :
( sP1(sK23)
| ~ r1(sK19,sK23)
| ~ r1(sK13,X0)
| ~ r1(X1,sK19)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_49225]) ).
tcf(c_51648,plain,
( sP1(sK23)
| ~ r1(sK19,sK23)
| ~ r1(sK13,sK19)
| ~ r1(sK13,sK13) ),
inference(instantiation,[status(thm)],[c_51647]) ).
tcf(c_51667,plain,
! [X0: $i,X1: $i] :
( sP1(sK31)
| ~ r1(sK27,sK31)
| ~ r1(sK13,X0)
| ~ r1(X1,sK27)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_49229]) ).
tcf(c_52637,plain,
! [X0: $i] : r1(sK10(X0),sK10(X0)),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_54829,plain,
! [X0: $i] :
( sP1(sK31)
| ~ r1(sK27,sK31)
| ~ r1(sK23,sK27)
| ~ r1(sK13,X0)
| ~ r1(X0,sK23) ),
inference(instantiation,[status(thm)],[c_51667]) ).
tcf(c_54998,plain,
( r1(sK12(sK27),sK6(sK12(sK27)))
| ~ sP1(sK23)
| ~ r1(sK27,sK12(sK27)) ),
inference(instantiation,[status(thm)],[c_3603]) ).
tcf(c_55308,plain,
( sP1(sK31)
| ~ r1(sK27,sK31)
| ~ r1(sK23,sK27)
| ~ r1(sK19,sK23)
| ~ r1(sK13,sK19) ),
inference(instantiation,[status(thm)],[c_54829]) ).
tcf(c_60335,plain,
r1(sK10(sK35),sK10(sK35)),
inference(instantiation,[status(thm)],[c_52637]) ).
tcf(c_68827,plain,
( r1(sK12(sK35),sK6(sK12(sK35)))
| ~ sP1(sK31)
| ~ r1(sK35,sK12(sK35)) ),
inference(instantiation,[status(thm)],[c_3611]) ).
tcf(c_72098,plain,
( p2(sK6(sK12(sK27)))
| ~ sP1(sK23)
| ~ r1(sK27,sK12(sK27)) ),
inference(instantiation,[status(thm)],[c_3257]) ).
tcf(c_119641,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(X1)
| r1(X2,sK9(X2))
| ~ sP1(X4)
| ~ p2(sK10(X0))
| ~ r1(X4,X3)
| ~ r1(X3,sK10(X0))
| ~ r1(sK10(X0),X2)
| ~ r1(sK10(X0),X1) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_122923,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(X1)
| r1(sK10(X0),sK9(sK10(X0)))
| ~ sP1(X3)
| ~ p2(sK10(X0))
| ~ r1(X3,X2)
| ~ r1(X2,sK10(X0))
| ~ r1(sK10(X0),X1)
| ~ r1(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_119641]) ).
tcf(c_144331,plain,
! [X0: $i,X1: $i] :
( p2(sK36(sK10(sK35)))
| r1(sK10(sK35),sK9(sK10(sK35)))
| ~ sP1(X1)
| ~ p2(sK10(sK35))
| ~ r1(X1,X0)
| ~ r1(X0,sK10(sK35))
| ~ r1(sK10(sK35),sK10(sK35))
| ~ r1(sK10(sK35),sK36(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_122923]) ).
tcf(c_149541,plain,
! [X0: $i] :
( p2(sK36(sK10(sK35)))
| r1(sK10(sK35),sK9(sK10(sK35)))
| ~ sP1(X0)
| ~ p2(sK10(sK35))
| ~ r1(X0,sK35)
| ~ r1(sK35,sK10(sK35))
| ~ r1(sK10(sK35),sK10(sK35))
| ~ r1(sK10(sK35),sK36(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_144331]) ).
tcf(c_152305,plain,
( p2(sK6(sK12(sK35)))
| ~ sP1(sK31)
| ~ r1(sK35,sK12(sK35)) ),
inference(instantiation,[status(thm)],[c_3265]) ).
tcf(c_153442,plain,
( p2(sK36(sK10(sK35)))
| r1(sK10(sK35),sK9(sK10(sK35)))
| ~ sP1(sK31)
| ~ p2(sK10(sK35))
| ~ r1(sK31,sK35)
| ~ r1(sK35,sK10(sK35))
| ~ r1(sK10(sK35),sK10(sK35))
| ~ r1(sK10(sK35),sK36(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_149541]) ).
tcf(c_159723,plain,
( ~ p2(sK36(sK10(sK35)))
| ~ r1(sK35,sK10(sK35)) ),
inference(instantiation,[status(thm)],[c_107]) ).
tcf(c_260299,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(X1)
| r1(X2,sK9(X2))
| ~ sP1(X4)
| ~ p2(sK10(X0))
| ~ r1(X4,X3)
| ~ r1(X3,sK10(X0))
| ~ r1(sK10(X0),X2)
| ~ r1(sK10(X0),X1) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_260547,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(X4)
| ~ p2(X3)
| ~ sP1(X1)
| ~ r1(X3,X4)
| ~ r1(X3,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ p2(sK10(sK9(X0)))
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_262193,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(X1)
| r1(sK10(X0),sK9(sK10(X0)))
| ~ sP1(X3)
| ~ p2(sK10(X0))
| ~ r1(X3,X2)
| ~ r1(X2,sK10(X0))
| ~ r1(sK10(X0),X1)
| ~ r1(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_260299]) ).
tcf(c_266737,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(X1)
| r1(sK10(X0),sK9(sK10(X0)))
| ~ sP1(X3)
| ~ p2(sK10(X0))
| ~ r1(X3,X2)
| ~ r1(X2,sK10(X0))
| ~ r1(sK10(X0),X1) ),
inference(global_subsumption_just,[status(thm)],[c_262193,c_16631,c_16632]) ).
tcf(c_266786,plain,
! [X0: $i,X1: $i] :
( p2(sK36(sK10(sK35)))
| r1(sK10(sK35),sK9(sK10(sK35)))
| ~ sP1(X1)
| ~ p2(sK10(sK35))
| ~ r1(X1,X0)
| ~ r1(X0,sK10(sK35))
| ~ r1(sK10(sK35),sK36(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_266737]) ).
tcf(c_317462,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(sK36(X2))
| ~ p2(X1)
| ~ sP1(X3)
| ~ r1(X4,X1)
| ~ r1(X3,X4)
| ~ r1(X1,X0)
| ~ p2(sK10(sK9(X0)))
| ~ r1(X1,sK36(X2))
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_260547]) ).
tcf(c_320417,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK36(sK10(sK35)))
| ~ sP1(X2)
| ~ p2(sK10(sK35))
| ~ r1(X2,X1)
| ~ p2(sK10(sK9(X0)))
| ~ r1(X1,sK10(sK35))
| ~ r1(sK10(sK35),X0)
| ~ r1(sK10(sK35),sK36(sK10(sK35)))
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_317462]) ).
fof(f10,definition,
! [X6] :
( ~ sP0(X6)
| ? [X20] :
( ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
& r1(X6,X20) )
| ! [X16] :
( ! [X17] :
( ? [X18] :
( p2(X18)
& ? [X19] : r1(X18,X19)
& r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X5] :
( ~ sP1(X5)
| ! [X6] :
( ( sP0(X6)
& ! [X10] :
( ! [X13] :
( ? [X14] :
( ! [X15] :
( ~ p2(X15)
| ~ r1(X14,X15) )
& r1(X13,X14) )
| ~ r1(X10,X13) )
| ~ p2(X10)
| ! [X11] :
( ( p2(X11)
& ? [X12] : r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X6,X10) )
& ! [X7] :
( ? [X8] :
( p2(X8)
& ? [X9] : r1(X8,X9)
& r1(X7,X8) )
| ~ r1(X6,X7) ) )
| ~ r1(X5,X6) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X2] :
( ~ sP2(X2)
| ! [X3] :
( ( ! [X30] :
( ? [X33] :
( ~ p1(X33)
& r1(X30,X33) )
| ! [X31] :
( ! [X32] :
( p1(X32)
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X3,X30) )
& ! [X4] :
( ( ! [X26] :
( ? [X29] :
( ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X4,X26) )
& ! [X5] :
( ( ! [X22] :
( ? [X25] :
( ~ p1(X25)
& r1(X22,X25) )
| ! [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X5,X22) )
& sP1(X5) )
| ~ r1(X4,X5) ) )
| ~ r1(X3,X4) ) )
| ~ r1(X2,X3) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,plain,
? [X0] :
( ! [X85] :
( ? [X88] :
( p1(X88)
& r1(X85,X88) )
| ! [X86] :
( ! [X87] :
( ~ p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X0,X85) )
& ? [X46] :
( ! [X81] :
( ? [X84] :
( p1(X84)
& r1(X81,X84) )
| ! [X82] :
( ! [X83] :
( ~ p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| ~ r1(X46,X81) )
& ? [X51] :
( ! [X77] :
( ? [X80] :
( p1(X80)
& r1(X77,X80) )
| ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X51,X77) )
& ? [X56] :
( ! [X73] :
( ? [X76] :
( p1(X76)
& r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( ~ p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X56,X73) )
& ? [X61] :
( ! [X69] :
( ? [X72] :
( p1(X72)
& r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( ~ p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X61,X69) )
& ? [X66] :
( ! [X67] :
( ? [X68] :
( ~ p2(X68)
& r1(X67,X68) )
| ~ r1(X66,X67) )
& r1(X61,X66) )
& ? [X62] :
( ? [X65] :
( ~ p1(X65)
& r1(X62,X65) )
& ? [X63] :
( ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
& r1(X62,X63) )
& r1(X61,X62) )
& r1(X56,X61) )
& ? [X57] :
( ? [X60] :
( ~ p1(X60)
& r1(X57,X60) )
& ? [X58] :
( ! [X59] :
( p1(X59)
| ~ r1(X58,X59) )
& r1(X57,X58) )
& r1(X56,X57) )
& r1(X51,X56) )
& ? [X52] :
( ? [X55] :
( ~ p1(X55)
& r1(X52,X55) )
& ? [X53] :
( ! [X54] :
( p1(X54)
| ~ r1(X53,X54) )
& r1(X52,X53) )
& r1(X51,X52) )
& r1(X46,X51) )
& ? [X47] :
( ? [X50] :
( ~ p1(X50)
& r1(X47,X50) )
& ? [X48] :
( ! [X49] :
( p1(X49)
| ~ r1(X48,X49) )
& r1(X47,X48) )
& r1(X46,X47) )
& r1(X0,X46) )
& ? [X42] :
( ? [X45] :
( ~ p1(X45)
& r1(X42,X45) )
& ? [X43] :
( ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
& r1(X42,X43) )
& r1(X0,X42) )
& ! [X38] :
( ? [X41] :
( ~ p1(X41)
& r1(X38,X41) )
| ! [X39] :
( ! [X40] :
( p1(X40)
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X0,X38) )
& ! [X2] :
( ( ! [X34] :
( ? [X37] :
( ~ p1(X37)
& r1(X34,X37) )
| ! [X35] :
( ! [X36] :
( p1(X36)
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X2,X34) )
& sP2(X2) )
| ~ r1(X0,X2) ) ),
inference(definition_folding,[],[f9,f12,f11,f10]) ).
fof(f20,plain,
! [X6] :
( ~ sP0(X6)
| ? [X20] :
( ! [X21] :
( ~ p2(X21)
| ~ r1(X20,X21) )
& r1(X6,X20) )
| ! [X16] :
( ! [X17] :
( ? [X18] :
( p2(X18)
& ? [X19] : r1(X18,X19)
& r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X6,X16) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f21,plain,
! [X0] :
( ~ sP0(X0)
| ? [X5] :
( ! [X6] :
( ~ p2(X6)
| ~ r1(X5,X6) )
& r1(X0,X5) )
| ! [X1] :
( ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] : r1(X3,X4)
& r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f20]) ).
fof(f22,plain,
! [X0] :
( ~ sP0(X0)
| ( ! [X6] :
( ~ p2(X6)
| ~ r1(sK12(X0),X6) )
& r1(X0,sK12(X0)) )
| ! [X1] :
( ! [X2] :
( ( p2(sK10(X2))
& r1(sK10(X2),sK11(X2))
& r1(X2,sK10(X2)) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X3,sK10(X2)),skolemize(X4,sK11(X2)),skolemize(X5,sK12(X0))],[f21]) ).
fof(f41,plain,
! [X2,X0,X1,X6] :
( ~ sP0(X0)
| ~ p2(X6)
| ~ r1(sK12(X0),X6)
| p2(sK10(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f42,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| r1(X0,sK12(X0))
| p2(sK10(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f45,plain,
! [X2,X0,X1,X6] :
( ~ sP0(X0)
| ~ p2(X6)
| ~ r1(sK12(X0),X6)
| r1(X2,sK10(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| r1(X0,sK12(X0))
| r1(X2,sK10(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK10(X2))
| r1(X0,sK12(X0))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(X3,sK10(X3))
| ~ sP0(X0)
| ~ p2(X1)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| ~ r1(sK12(X0),X1) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK10(X2))
| r1(X0,sK12(X0))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(sK10(X3))
| ~ sP0(X0)
| ~ p2(X1)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| ~ r1(sK12(X0),X1) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_5321,plain,
! [X0: $i,X1: $i] :
( r1(sK35,sK10(sK35))
| r1(X0,sK12(X0))
| ~ sP0(X0)
| ~ r1(X1,sK35)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_12881,plain,
! [X0: $i] :
( r1(sK35,sK10(sK35))
| r1(X0,sK12(X0))
| ~ sP0(X0)
| ~ r1(sK31,sK35)
| ~ r1(X0,sK31) ),
inference(instantiation,[status(thm)],[c_5321]) ).
tcf(c_22084,plain,
( r1(sK35,sK10(sK35))
| r1(sK27,sK12(sK27))
| ~ sP0(sK27)
| ~ r1(sK31,sK35)
| ~ r1(sK27,sK31) ),
inference(instantiation,[status(thm)],[c_12881]) ).
tcf(c_49028,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK10(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ p2(sK6(sK12(X0)))
| ~ r1(sK12(X0),sK6(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_49120,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK12(X2))
| r1(sK9(X1),sK10(sK9(X1)))
| ~ sP0(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK9(X1)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_51147,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK12(X1))
| r1(sK9(X0),sK10(sK9(X0)))
| ~ sP0(X1)
| ~ r1(X1,sK9(X0))
| ~ r1(sK9(X0),sK9(X0)) ),
inference(instantiation,[status(thm)],[c_49120]) ).
tcf(c_51384,plain,
! [X0: $i,X1: $i] :
( r1(sK35,sK10(sK35))
| ~ sP0(X0)
| ~ r1(X1,sK35)
| ~ r1(X0,X1)
| ~ p2(sK6(sK12(X0)))
| ~ r1(sK12(X0),sK6(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_49028]) ).
tcf(c_55501,plain,
! [X0: $i] :
( r1(sK35,sK10(sK35))
| ~ sP0(X0)
| ~ r1(sK31,sK35)
| ~ r1(X0,sK31)
| ~ p2(sK6(sK12(X0)))
| ~ r1(sK12(X0),sK6(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_51384]) ).
tcf(c_59925,plain,
( r1(sK35,sK10(sK35))
| ~ sP0(sK27)
| ~ r1(sK31,sK35)
| ~ r1(sK27,sK31)
| ~ p2(sK6(sK12(sK27)))
| ~ r1(sK12(sK27),sK6(sK12(sK27))) ),
inference(instantiation,[status(thm)],[c_55501]) ).
tcf(c_77429,plain,
! [X0: $i,X1: $i] :
( p2(sK10(sK35))
| r1(X0,sK12(X0))
| ~ sP0(X0)
| ~ r1(X1,sK35)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_95188,plain,
! [X0: $i] :
( p2(sK10(sK35))
| r1(X0,sK12(X0))
| ~ sP0(X0)
| ~ r1(sK31,sK35)
| ~ r1(X0,sK31) ),
inference(instantiation,[status(thm)],[c_77429]) ).
tcf(c_101798,plain,
( p2(sK10(sK35))
| r1(sK27,sK12(sK27))
| ~ sP0(sK27)
| ~ r1(sK31,sK35)
| ~ r1(sK27,sK31) ),
inference(instantiation,[status(thm)],[c_95188]) ).
tcf(c_119634,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK10(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ p2(sK6(sK12(X0)))
| ~ r1(sK12(X0),sK6(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_119781,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK12(X2))
| r1(sK9(X1),sK10(sK9(X1)))
| ~ sP0(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK9(X1)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_122519,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(sK9(X2),sK10(sK9(X2)))
| ~ sP0(X0)
| ~ r1(X0,X1)
| ~ p2(sK6(sK12(X0)))
| ~ r1(X1,sK9(X2))
| ~ r1(sK12(X0),sK6(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_119634]) ).
tcf(c_166373,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK10(sK35))
| ~ sP0(X0)
| ~ p2(X1)
| ~ r1(X2,sK35)
| ~ r1(X0,X2)
| ~ r1(sK12(X0),X1) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_181945,plain,
! [X0: $i,X1: $i] :
( p2(sK10(sK35))
| ~ sP0(X0)
| ~ p2(X1)
| ~ r1(sK31,sK35)
| ~ r1(X0,sK31)
| ~ r1(sK12(X0),X1) ),
inference(instantiation,[status(thm)],[c_166373]) ).
tcf(c_186860,plain,
! [X0: $i] :
( p2(sK10(sK35))
| ~ sP0(sK27)
| ~ p2(X0)
| ~ r1(sK31,sK35)
| ~ r1(sK27,sK31)
| ~ r1(sK12(sK27),X0) ),
inference(instantiation,[status(thm)],[c_181945]) ).
tcf(c_195128,plain,
! [X0: $i] :
( p2(sK10(sK35))
| ~ sP0(sK27)
| ~ r1(sK31,sK35)
| ~ r1(sK27,sK31)
| ~ p2(sK6(X0))
| ~ r1(sK12(sK27),sK6(X0)) ),
inference(instantiation,[status(thm)],[c_186860]) ).
tcf(c_226812,plain,
( p2(sK10(sK35))
| ~ sP0(sK27)
| ~ r1(sK31,sK35)
| ~ r1(sK27,sK31)
| ~ p2(sK6(sK12(sK27)))
| ~ r1(sK12(sK27),sK6(sK12(sK27))) ),
inference(instantiation,[status(thm)],[c_195128]) ).
tcf(c_229611,plain,
! [X0: $i] :
( r1(sK9(sK10(sK35)),sK10(sK9(sK10(sK35))))
| ~ sP0(X0)
| ~ p2(sK6(sK12(X0)))
| ~ r1(X0,sK10(sK35))
| ~ r1(sK10(sK35),sK9(sK10(sK35)))
| ~ r1(sK12(X0),sK6(sK12(X0))) ),
inference(instantiation,[status(thm)],[c_122519]) ).
tcf(c_229616,plain,
! [X0: $i] :
( r1(X0,sK12(X0))
| r1(sK9(sK10(sK35)),sK10(sK9(sK10(sK35))))
| ~ sP0(X0)
| ~ r1(X0,sK10(sK35))
| ~ r1(sK10(sK35),sK9(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_119781]) ).
tcf(c_241465,plain,
( r1(sK35,sK12(sK35))
| r1(sK9(sK10(sK35)),sK10(sK9(sK10(sK35))))
| ~ sP0(sK35)
| ~ r1(sK35,sK10(sK35))
| ~ r1(sK10(sK35),sK9(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_229616]) ).
tcf(c_241585,plain,
( r1(sK9(sK10(sK35)),sK10(sK9(sK10(sK35))))
| ~ sP0(sK35)
| ~ p2(sK6(sK12(sK35)))
| ~ r1(sK35,sK10(sK35))
| ~ r1(sK12(sK35),sK6(sK12(sK35)))
| ~ r1(sK10(sK35),sK9(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_229611]) ).
tcf(c_260108,plain,
! [X0: $i,X1: $i] :
( r1(sK35,sK10(sK35))
| r1(X0,sK12(X0))
| ~ sP0(X0)
| ~ r1(X1,sK35)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_260548,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK12(X2))
| r1(sK9(X1),sK10(sK9(X1)))
| ~ sP0(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK9(X1)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_261858,plain,
r1(sK35,sK10(sK35)),
inference(global_subsumption_just,[status(thm)],[c_260108,c_105,c_99,c_87,c_81,c_118,c_3137,c_22084,c_51648,c_54998,c_59925,c_72098]) ).
tcf(c_261864,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK12(X1))
| r1(sK9(X0),sK10(sK9(X0)))
| ~ sP0(X1)
| ~ r1(X1,sK9(X0))
| ~ r1(sK9(X0),sK9(X0)) ),
inference(instantiation,[status(thm)],[c_260548]) ).
tcf(c_262485,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK10(sK9(X1)))
| r1(X2,sK12(X2))
| ~ sP0(X2)
| ~ r1(X2,X0)
| ~ r1(X0,sK9(X1)) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_262486,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(sK10(sK9(X3)))
| ~ sP0(X0)
| ~ p2(X1)
| ~ r1(X0,X2)
| ~ r1(X2,sK9(X3))
| ~ r1(sK12(X0),X1) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_266547,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK12(X1))
| r1(sK9(X0),sK10(sK9(X0)))
| ~ sP0(X1)
| ~ r1(X1,sK9(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_261864,c_49115,c_51147]) ).
tcf(c_266548,plain,
! [X0: $i,X1: $i] :
( r1(X0,sK12(X0))
| r1(sK9(X1),sK10(sK9(X1)))
| ~ sP0(X0)
| ~ r1(X0,sK9(X1)) ),
inference(renaming,[status(thm)],[c_266547]) ).
tcf(c_270581,plain,
r1(sK10(sK35),sK9(sK10(sK35))),
inference(global_subsumption_just,[status(thm)],[c_266786,c_105,c_99,c_93,c_87,c_81,c_118,c_3137,c_5326,c_22084,c_51648,c_54998,c_55308,c_59925,c_60335,c_72098,c_101798,c_153442,c_159723,c_226812]) ).
tcf(c_270597,plain,
( r1(sK10(sK35),sK12(sK10(sK35)))
| r1(sK9(sK10(sK35)),sK10(sK9(sK10(sK35))))
| ~ sP0(sK10(sK35))
| ~ r1(sK10(sK35),sK9(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_266548]) ).
tcf(c_332537,plain,
! [X0: $i,X1: $i] :
( p2(sK10(sK9(X1)))
| ~ sP0(sK35)
| ~ r1(sK35,X0)
| ~ p2(sK6(sK12(sK35)))
| ~ r1(X0,sK9(X1))
| ~ r1(sK12(sK35),sK6(sK12(sK35))) ),
inference(instantiation,[status(thm)],[c_262486]) ).
tcf(c_341812,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r1(X2,X1)
| ~ p2(sK10(sK9(X0)))
| ~ r1(X1,sK10(sK35))
| ~ r1(sK10(sK35),X0)
| ~ r1(sK9(X0),sK10(sK9(X0)))
| ~ sP1(X2) ),
inference(global_subsumption_just,[status(thm)],[c_320417,c_105,c_99,c_87,c_81,c_118,c_3137,c_5326,c_22084,c_51648,c_54998,c_59925,c_72098,c_101798,c_159723,c_226812,c_320417]) ).
tcf(c_341813,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ sP1(X2)
| ~ r1(X2,X1)
| ~ p2(sK10(sK9(X0)))
| ~ r1(X1,sK10(sK35))
| ~ r1(sK10(sK35),X0)
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(renaming,[status(thm)],[c_341812]) ).
tcf(c_341821,plain,
! [X0: $i,X1: $i] :
( ~ sP1(X1)
| ~ r1(X1,sK35)
| ~ r1(sK35,sK10(sK35))
| ~ p2(sK10(sK9(X0)))
| ~ r1(sK10(sK35),X0)
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_341813]) ).
tcf(c_345478,plain,
! [X0: $i,X1: $i] :
( ~ sP1(X1)
| ~ r1(X1,sK35)
| ~ r1(sK9(X0),sK10(sK9(X0)))
| ~ r1(sK10(sK35),X0)
| ~ p2(sK10(sK9(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_341821,c_105,c_99,c_87,c_81,c_118,c_3137,c_22084,c_51648,c_54998,c_59925,c_72098,c_341821]) ).
tcf(c_345479,plain,
! [X0: $i,X1: $i] :
( ~ sP1(X1)
| ~ r1(X1,sK35)
| ~ p2(sK10(sK9(X0)))
| ~ r1(sK10(sK35),X0)
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(renaming,[status(thm)],[c_345478]) ).
tcf(c_345483,plain,
! [X0: $i] :
( ~ sP1(sK31)
| ~ r1(sK31,sK35)
| ~ p2(sK10(sK9(X0)))
| ~ r1(sK10(sK35),X0)
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(instantiation,[status(thm)],[c_345479]) ).
tcf(c_350960,plain,
! [X0: $i] :
( ~ p2(sK10(sK9(X0)))
| ~ r1(sK10(sK35),X0)
| ~ r1(sK9(X0),sK10(sK9(X0))) ),
inference(global_subsumption_just,[status(thm)],[c_345483,c_105,c_99,c_93,c_87,c_81,c_55308,c_345483]) ).
tcf(c_431044,plain,
! [X0: $i,X1: $i] :
( r1(sK35,sK12(sK35))
| p2(sK10(sK9(X1)))
| ~ sP0(sK35)
| ~ r1(sK35,X0)
| ~ r1(X0,sK9(X1)) ),
inference(instantiation,[status(thm)],[c_262485]) ).
tcf(c_440953,plain,
! [X0: $i,X1: $i] :
( ~ r1(sK35,X0)
| ~ r1(X0,sK9(X1))
| p2(sK10(sK9(X1))) ),
inference(global_subsumption_just,[status(thm)],[c_431044,c_99,c_93,c_87,c_81,c_3145,c_55308,c_68827,c_152305,c_332537,c_431044]) ).
tcf(c_440954,plain,
! [X0: $i,X1: $i] :
( p2(sK10(sK9(X1)))
| ~ r1(sK35,X0)
| ~ r1(X0,sK9(X1)) ),
inference(renaming,[status(thm)],[c_440953]) ).
tcf(c_440997,plain,
! [X0: $i] :
( p2(sK10(sK9(X0)))
| ~ r1(sK35,sK10(sK35))
| ~ r1(sK10(sK35),sK9(X0)) ),
inference(instantiation,[status(thm)],[c_440954]) ).
tcf(c_445159,plain,
r1(sK9(sK10(sK35)),sK10(sK9(sK10(sK35)))),
inference(global_subsumption_just,[status(thm)],[c_270597,c_105,c_99,c_93,c_87,c_81,c_118,c_3145,c_3137,c_5326,c_22084,c_51648,c_54998,c_55308,c_59925,c_60335,c_68827,c_72098,c_101798,c_152305,c_153442,c_159723,c_226812,c_241465,c_241585]) ).
tcf(c_451672,plain,
( ~ p2(sK10(sK9(sK10(sK35))))
| ~ r1(sK10(sK35),sK10(sK35))
| ~ r1(sK9(sK10(sK35)),sK10(sK9(sK10(sK35)))) ),
inference(instantiation,[status(thm)],[c_350960]) ).
tcf(c_457923,plain,
! [X0: $i] :
( p2(sK10(sK9(X0)))
| ~ r1(sK10(sK35),sK9(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_440997,c_261858,c_440997]) ).
tcf(c_457935,plain,
( p2(sK10(sK9(sK10(sK35))))
| ~ r1(sK10(sK35),sK9(sK10(sK35))) ),
inference(instantiation,[status(thm)],[c_457923]) ).
tcf(c_457936,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_457935,c_451672,c_445159,c_270581,c_60335]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL670+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/5.38 % Computer : n009.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Thu Sep 24 00:10:34 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/5.42 Running first-order theorem proving
% 0.15/5.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.43
% 0.15/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.15/5.43
% 0.15/5.43 % Detected problem language: tptp
% 0.15/5.45 % Proving...
% 188.73/34.40 % SZS status Started for theBenchmark.p
% 188.73/34.40 % SZS status Theorem for theBenchmark.p
% 188.73/34.40
% 188.73/34.40 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 188.73/34.40
% 188.73/34.40 % ------ iProver source info
% 188.73/34.40
% 188.73/34.40 % git: date: 2026-07-19 20:42:38 +0200
% 188.73/34.40 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 188.73/34.40 % git: non_committed_changes: false
% 188.73/34.40
% 188.73/34.40 % ------ Parsing...
% 188.73/34.40 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 188.73/34.40
% 188.73/34.40 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 188.73/34.40
% 188.73/34.40 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 188.73/34.40 % ------ Proving...
% 188.73/34.40 % ------ Problem Properties
% 188.73/34.40
% 188.73/34.40 %
% 188.73/34.40 % clauses 68
% 188.73/34.40 % conjectures 46
% 188.73/34.40 % EPR 33
% 188.73/34.40 % Horn 58
% 188.73/34.40 % unary 26
% 188.73/34.40 % binary 7
% 188.73/34.40 % lits 247
% 188.73/34.40 % lits eq 0
% 188.73/34.40 % fd_pure 0
% 188.73/34.40 % fd_pseudo 0
% 188.73/34.40 % fd_cond 0
% 188.73/34.40 % fd_pseudo_cond 0
% 188.73/34.40 % AC symbols 0
% 188.73/34.40
% 188.73/34.40 % ------ Input Options Time Limit: Unbounded
% 188.73/34.40
% 188.73/34.40
% 188.73/34.40 % ------
% 188.73/34.40 % Current options:
% 188.73/34.40 % ------
% 188.73/34.40
% 188.73/34.40
% 188.73/34.40 %
% 188.73/34.40
% 188.73/34.40 % ------ Proving...
% 188.73/34.40 %
% 188.73/34.40
% 188.73/34.40 % SZS status Theorem for theBenchmark.p
% 188.73/34.40
% 188.73/34.40 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 111.92/34.40
% 111.92/34.40
%------------------------------------------------------------------------------