%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 : Tue Sep 29 11:55:30 AM UTC 2026
% Result : Theorem 3.33s 1.32s
% Output : Refutation 3.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 99
% Syntax : Number of formulae : 513 ( 66 unt; 97 def)
% Number of atoms : 2236 ( 0 equ)
% Maximal formula atoms : 84 ( 4 avg)
% Number of connectives : 3349 (1626 ~;1378 |; 250 &)
% ( 95 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 42 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 109 ( 108 usr; 46 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-1 aty)
% Number of variables : 1024 ( 0 sgn 961 !; 63 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ~ p12(X0)
& ~ p10(X0)
& ~ p8(X0)
& ~ p6(X0)
& ~ p4(X0)
& ~ p2(X0) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p5(X0)
& ~ p1(X0) )
| ( p1(X0)
& p5(X0) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p6(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p4(X0)
& ~ p5(X0) )
| ( p5(X0)
& p4(X0) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p5(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p3(X0)
& ~ p4(X0) )
| ( p4(X0)
& p3(X0) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p2(X0)
& ~ p3(X0) )
| ( p3(X0)
& p2(X0) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p1(X0)
& ~ p2(X0) )
| ( p2(X0)
& p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( p6(X0)
& p5(X0)
& p4(X0)
& p3(X0)
& p2(X0)
& p1(X0) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ~ p12(X0)
& ~ p10(X0)
& ~ p8(X0)
& ~ p6(X0)
& ~ p4(X0)
& ~ p2(X0) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p7(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p5(X0)
& ~ p1(X0) )
| ( p1(X0)
& p5(X0) ) ) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p6(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p4(X0)
& ~ p5(X0) )
| ( p5(X0)
& p4(X0) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p5(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p3(X0)
& ~ p4(X0) )
| ( p4(X0)
& p3(X0) ) ) ) ) ) ) )
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p2(X0)
& ~ p3(X0) )
| ( p3(X0)
& p2(X0) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ( ( ~ p1(X0)
& ~ p2(X0) )
| ( p2(X0)
& p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( p6(X0)
& p5(X0)
& p4(X0)
& p3(X0)
& p2(X0)
& p1(X0) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ( ~ p12(X6)
& ~ p10(X6)
& ~ p8(X6)
& ~ p6(X6)
& ~ p4(X6)
& ~ p2(X6) ) ) ) ) ) ) )
| ! [X7] :
( ~ r1(X0,X7)
| p7(X7) )
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ~ ( ( ~ p5(X15)
& ~ p1(X15) )
| ( p1(X15)
& p5(X15) ) ) ) ) ) ) ) ) )
| ! [X16] :
( ~ r1(X8,X16)
| p6(X16) )
| ~ ! [X17] :
( ~ r1(X8,X17)
| ~ ( ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ( ( ~ p4(X23)
& ~ p5(X23) )
| ( p5(X23)
& p4(X23) ) ) ) ) ) ) ) )
| ! [X24] :
( ~ r1(X17,X24)
| p5(X24) )
| ~ ! [X25] :
( ~ r1(X17,X25)
| ~ ( ~ ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ~ ( ( ~ p3(X30)
& ~ p4(X30) )
| ( p4(X30)
& p3(X30) ) ) ) ) ) ) )
| ! [X31] :
( ~ r1(X25,X31)
| p4(X31) )
| ~ ! [X32] :
( ~ r1(X25,X32)
| ~ ( ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ~ ( ( ~ p2(X36)
& ~ p3(X36) )
| ( p3(X36)
& p2(X36) ) ) ) ) ) )
| ! [X37] :
( ~ r1(X32,X37)
| p3(X37) )
| ~ ! [X38] :
( ~ r1(X32,X38)
| ~ ~ ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ~ ( ( ~ p1(X41)
& ~ p2(X41) )
| ( p2(X41)
& p1(X41) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ( p6(X47)
& p5(X47)
& p4(X47)
& p3(X47)
& p2(X47)
& p1(X47) ) ) ) ) ) ) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ( ~ p12(X6)
& ~ p10(X6)
& ~ p8(X6)
& ~ p6(X6)
& ~ p4(X6)
& ~ p2(X6) ) ) ) ) ) ) )
| ! [X7] :
( ~ r1(X0,X7)
| p7(X7) )
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ~ ( ( ~ p5(X15)
& ~ p1(X15) )
| ( p1(X15)
& p5(X15) ) ) ) ) ) ) ) ) )
| ! [X16] :
( ~ r1(X8,X16)
| p6(X16) )
| ~ ! [X17] :
( ~ r1(X8,X17)
| ~ ( ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ( ( ~ p4(X23)
& ~ p5(X23) )
| ( p5(X23)
& p4(X23) ) ) ) ) ) ) ) )
| ! [X24] :
( ~ r1(X17,X24)
| p5(X24) )
| ~ ! [X25] :
( ~ r1(X17,X25)
| ~ ( ~ ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ~ ( ( ~ p3(X30)
& ~ p4(X30) )
| ( p4(X30)
& p3(X30) ) ) ) ) ) ) )
| ! [X31] :
( ~ r1(X25,X31)
| p4(X31) )
| ~ ! [X32] :
( ~ r1(X25,X32)
| ~ ( ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ~ ( ( ~ p2(X36)
& ~ p3(X36) )
| ( p3(X36)
& p2(X36) ) ) ) ) ) )
| ! [X37] :
( ~ r1(X32,X37)
| p3(X37) )
| ~ ! [X38] :
( ~ r1(X32,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ~ ( ( ~ p1(X41)
& ~ p2(X41) )
| ( p2(X41)
& p1(X41) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ( p6(X47)
& p5(X47)
& p4(X47)
& p3(X47)
& p2(X47)
& p1(X47) ) ) ) ) ) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ( ~ p12(X6)
& ~ p10(X6)
& ~ p8(X6)
& ~ p6(X6)
& ~ p4(X6)
& ~ p2(X6) ) ) ) ) ) ) )
| ! [X7] : ~ r1(X0,X7)
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ~ ( ( ~ p5(X15)
& ~ p1(X15) )
| ( p1(X15)
& p5(X15) ) ) ) ) ) ) ) ) )
| ! [X16] :
( ~ r1(X8,X16)
| p6(X16) )
| ~ ! [X17] :
( ~ r1(X8,X17)
| ~ ( ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ( ( ~ p4(X23)
& ~ p5(X23) )
| ( p5(X23)
& p4(X23) ) ) ) ) ) ) ) )
| ! [X24] :
( ~ r1(X17,X24)
| p5(X24) )
| ~ ! [X25] :
( ~ r1(X17,X25)
| ~ ( ~ ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ~ ( ( ~ p3(X30)
& ~ p4(X30) )
| ( p4(X30)
& p3(X30) ) ) ) ) ) ) )
| ! [X31] :
( ~ r1(X25,X31)
| p4(X31) )
| ~ ! [X32] :
( ~ r1(X25,X32)
| ~ ( ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ~ ( ( ~ p2(X36)
& ~ p3(X36) )
| ( p3(X36)
& p2(X36) ) ) ) ) ) )
| ! [X37] :
( ~ r1(X32,X37)
| p3(X37) )
| ~ ! [X38] :
( ~ r1(X32,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ~ ( ( ~ p1(X41)
& ~ p2(X41) )
| ( p2(X41)
& p1(X41) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ( p6(X47)
& p5(X47)
& p4(X47)
& p3(X47)
& p2(X47)
& p1(X47) ) ) ) ) ) ) ) ),
inference(pure_predicate_removal,[],[f5]) ).
fof(f7,plain,
? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] : ~ r1(X5,X6) ) ) ) ) )
| ! [X7] : ~ r1(X0,X7)
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ~ ( ( ~ p5(X15)
& ~ p1(X15) )
| ( p1(X15)
& p5(X15) ) ) ) ) ) ) ) ) )
| ! [X16] :
( ~ r1(X8,X16)
| p6(X16) )
| ~ ! [X17] :
( ~ r1(X8,X17)
| ~ ( ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ( ( ~ p4(X23)
& ~ p5(X23) )
| ( p5(X23)
& p4(X23) ) ) ) ) ) ) ) )
| ! [X24] :
( ~ r1(X17,X24)
| p5(X24) )
| ~ ! [X25] :
( ~ r1(X17,X25)
| ~ ( ~ ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ~ ( ( ~ p3(X30)
& ~ p4(X30) )
| ( p4(X30)
& p3(X30) ) ) ) ) ) ) )
| ! [X31] :
( ~ r1(X25,X31)
| p4(X31) )
| ~ ! [X32] :
( ~ r1(X25,X32)
| ~ ( ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ~ ( ( ~ p2(X36)
& ~ p3(X36) )
| ( p3(X36)
& p2(X36) ) ) ) ) ) )
| ! [X37] :
( ~ r1(X32,X37)
| p3(X37) )
| ~ ! [X38] :
( ~ r1(X32,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ~ ( ( ~ p1(X41)
& ~ p2(X41) )
| ( p2(X41)
& p1(X41) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ( p6(X47)
& p5(X47)
& p4(X47)
& p3(X47)
& p2(X47)
& p1(X47) ) ) ) ) ) ) ) ),
inference(pure_predicate_removal,[],[f6]) ).
fof(f8,plain,
? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] : ~ r1(X5,X6) ) ) ) ) )
| ! [X7] : ~ r1(X0,X7)
| ~ ! [X8] :
( ~ r1(X0,X8)
| ~ ( ~ ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ~ ( ( ~ p5(X15)
& ~ p1(X15) )
| ( p1(X15)
& p5(X15) ) ) ) ) ) ) ) ) )
| ! [X16] : ~ r1(X8,X16)
| ~ ! [X17] :
( ~ r1(X8,X17)
| ~ ( ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ~ ( ( ~ p4(X23)
& ~ p5(X23) )
| ( p5(X23)
& p4(X23) ) ) ) ) ) ) ) )
| ! [X24] :
( ~ r1(X17,X24)
| p5(X24) )
| ~ ! [X25] :
( ~ r1(X17,X25)
| ~ ( ~ ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ~ ( ( ~ p3(X30)
& ~ p4(X30) )
| ( p4(X30)
& p3(X30) ) ) ) ) ) ) )
| ! [X31] :
( ~ r1(X25,X31)
| p4(X31) )
| ~ ! [X32] :
( ~ r1(X25,X32)
| ~ ( ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ~ ( ( ~ p2(X36)
& ~ p3(X36) )
| ( p3(X36)
& p2(X36) ) ) ) ) ) )
| ! [X37] :
( ~ r1(X32,X37)
| p3(X37) )
| ~ ! [X38] :
( ~ r1(X32,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ~ ( ( ~ p1(X41)
& ~ p2(X41) )
| ( p2(X41)
& p1(X41) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] : ~ r1(X46,X47) ) ) ) ) ) ),
inference(pure_predicate_removal,[],[f7]) ).
fof(f9,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ? [X6] : r1(X5,X6) ) ) ) ) )
& ? [X7] : r1(X0,X7)
& ! [X8] :
( ~ r1(X0,X8)
| ( ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ( ( p5(X15)
| p1(X15) )
& ( ~ p1(X15)
| ~ p5(X15) ) ) ) ) ) ) ) ) )
& ? [X16] : r1(X8,X16)
& ! [X17] :
( ~ r1(X8,X17)
| ( ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ( ( p4(X23)
| p5(X23) )
& ( ~ p5(X23)
| ~ p4(X23) ) ) ) ) ) ) ) )
& ? [X24] :
( r1(X17,X24)
& ~ p5(X24) )
& ! [X25] :
( ~ r1(X17,X25)
| ( ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( p3(X30)
| p4(X30) )
& ( ~ p4(X30)
| ~ p3(X30) ) ) ) ) ) ) )
& ? [X31] :
( r1(X25,X31)
& ~ p4(X31) )
& ! [X32] :
( ~ r1(X25,X32)
| ( ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p2(X36)
| p3(X36) )
& ( ~ p3(X36)
| ~ p2(X36) ) ) ) ) ) )
& ? [X37] :
( r1(X32,X37)
& ~ p3(X37) )
& ! [X38] :
( ~ r1(X32,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ( ( p1(X41)
| p2(X41) )
& ( ~ p2(X41)
| ~ p1(X41) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X42] :
( r1(X0,X42)
& ? [X43] :
( r1(X42,X43)
& ? [X44] :
( r1(X43,X44)
& ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ? [X47] : r1(X46,X47) ) ) ) ) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f10,definition,
! [X25] :
( ! [X32] :
( ~ r1(X25,X32)
| ( ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p2(X36)
| p3(X36) )
& ( ~ p3(X36)
| ~ p2(X36) ) ) ) ) ) )
& ? [X37] :
( r1(X32,X37)
& ~ p3(X37) )
& ! [X38] :
( ~ r1(X32,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ( ( p1(X41)
| p2(X41) )
& ( ~ p2(X41)
| ~ p1(X41) ) ) ) ) ) ) ) )
| ~ sP0(X25) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X17] :
( ! [X25] :
( ~ r1(X17,X25)
| ( ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( p3(X30)
| p4(X30) )
& ( ~ p4(X30)
| ~ p3(X30) ) ) ) ) ) ) )
& ? [X31] :
( r1(X25,X31)
& ~ p4(X31) )
& sP0(X25) ) )
| ~ sP1(X17) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ? [X6] : r1(X5,X6) ) ) ) ) )
& ? [X7] : r1(X0,X7)
& ! [X8] :
( ~ r1(X0,X8)
| ( ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ( ( p5(X15)
| p1(X15) )
& ( ~ p1(X15)
| ~ p5(X15) ) ) ) ) ) ) ) ) )
& ? [X16] : r1(X8,X16)
& ! [X17] :
( ~ r1(X8,X17)
| ( ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ( ( p4(X23)
| p5(X23) )
& ( ~ p5(X23)
| ~ p4(X23) ) ) ) ) ) ) ) )
& ? [X24] :
( r1(X17,X24)
& ~ p5(X24) )
& sP1(X17) ) ) ) )
& ? [X42] :
( r1(X0,X42)
& ? [X43] :
( r1(X42,X43)
& ? [X44] :
( r1(X43,X44)
& ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ? [X47] : r1(X46,X47) ) ) ) ) ) ),
inference(definition_folding,[],[f9,f11,f10]) ).
fof(f13,plain,
! [X17] :
( ! [X25] :
( ~ r1(X17,X25)
| ( ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ( ( p3(X30)
| p4(X30) )
& ( ~ p4(X30)
| ~ p3(X30) ) ) ) ) ) ) )
& ? [X31] :
( r1(X25,X31)
& ~ p4(X31) )
& sP0(X25) ) )
| ~ sP1(X17) ),
inference(nnf_transformation,[],[f11]) ).
fof(f14,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ( ( p3(X6)
| p4(X6) )
& ( ~ p4(X6)
| ~ p3(X6) ) ) ) ) ) ) )
& ? [X7] :
( r1(X1,X7)
& ~ p4(X7) )
& sP0(X1) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f13]) ).
fof(f15,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ( ( p3(X6)
| p4(X6) )
& ( ~ p4(X6)
| ~ p3(X6) ) ) ) ) ) ) )
& r1(X1,sK2(X1))
& ~ p4(sK2(X1))
& sP0(X1) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X7,sK2(X1))],[f14]) ).
fof(f16,plain,
! [X25] :
( ! [X32] :
( ~ r1(X25,X32)
| ( ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p2(X36)
| p3(X36) )
& ( ~ p3(X36)
| ~ p2(X36) ) ) ) ) ) )
& ? [X37] :
( r1(X32,X37)
& ~ p3(X37) )
& ! [X38] :
( ~ r1(X32,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ( ( p1(X41)
| p2(X41) )
& ( ~ p2(X41)
| ~ p1(X41) ) ) ) ) ) ) ) )
| ~ sP0(X25) ),
inference(nnf_transformation,[],[f10]) ).
fof(f17,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ( ( p2(X5)
| p3(X5) )
& ( ~ p3(X5)
| ~ p2(X5) ) ) ) ) ) )
& ? [X6] :
( r1(X1,X6)
& ~ p3(X6) )
& ! [X7] :
( ~ r1(X1,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ( ( p1(X10)
| p2(X10) )
& ( ~ p2(X10)
| ~ p1(X10) ) ) ) ) ) ) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f16]) ).
fof(f18,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ( ( p2(X5)
| p3(X5) )
& ( ~ p3(X5)
| ~ p2(X5) ) ) ) ) ) )
& r1(X1,sK3(X1))
& ~ p3(sK3(X1))
& ! [X7] :
( ~ r1(X1,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ( ( p1(X10)
| p2(X10) )
& ( ~ p2(X10)
| ~ p1(X10) ) ) ) ) ) ) ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X6,sK3(X1))],[f17]) ).
fof(f19,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ? [X6] : r1(X5,X6) ) ) ) ) )
& ? [X7] : r1(X0,X7)
& ! [X8] :
( ~ r1(X0,X8)
| ( ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ( ( p5(X15)
| p1(X15) )
& ( ~ p1(X15)
| ~ p5(X15) ) ) ) ) ) ) ) ) )
& ? [X16] : r1(X8,X16)
& ! [X17] :
( ~ r1(X8,X17)
| ( ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ( ( p4(X23)
| p5(X23) )
& ( ~ p5(X23)
| ~ p4(X23) ) ) ) ) ) ) ) )
& ? [X24] :
( r1(X17,X24)
& ~ p5(X24) )
& sP1(X17) ) ) ) )
& ? [X25] :
( r1(X0,X25)
& ? [X26] :
( r1(X25,X26)
& ? [X27] :
( r1(X26,X27)
& ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ? [X30] : r1(X29,X30) ) ) ) ) ) ),
inference(rectify,[],[f12]) ).
fof(f20,plain,
( r1(sK4,sK5)
& r1(sK5,sK6)
& r1(sK6,sK7)
& r1(sK7,sK8)
& r1(sK8,sK9)
& r1(sK9,sK10)
& r1(sK4,sK11)
& ! [X8] :
( ~ r1(sK4,X8)
| ( ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ( ( p5(X15)
| p1(X15) )
& ( ~ p1(X15)
| ~ p5(X15) ) ) ) ) ) ) ) ) )
& r1(X8,sK12(X8))
& ! [X17] :
( ~ r1(X8,X17)
| ( ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ( ( p4(X23)
| p5(X23) )
& ( ~ p5(X23)
| ~ p4(X23) ) ) ) ) ) ) ) )
& r1(X17,sK13(X17))
& ~ p5(sK13(X17))
& sP1(X17) ) ) ) )
& r1(sK4,sK14)
& r1(sK14,sK15)
& r1(sK15,sK16)
& r1(sK16,sK17)
& r1(sK17,sK18)
& r1(sK18,sK19) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X3,sK7),skolemize(X4,sK8),skolemize(X5,sK9),skolemize(X6,sK10),skolemize(X7,sK11),skolemize(X16,sK12(X8)),skolemize(X24,sK13(X17)),skolemize(X25,sK14),skolemize(X26,sK15),skolemize(X27,sK16),skolemize(X28,sK17),skolemize(X29,sK18),skolemize(X30,sK19)],[f19]) ).
fof(f21,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP0(X1)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f15]) ).
fof(f24,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ p4(X6)
| ~ p3(X6)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f15]) ).
fof(f25,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p3(X6)
| p4(X6)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f15]) ).
fof(f26,plain,
! [X10,X0,X1,X8,X9,X7] :
( ~ r1(X0,X1)
| ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ p2(X10)
| ~ p1(X10)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f27,plain,
! [X10,X0,X1,X8,X9,X7] :
( ~ r1(X0,X1)
| ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| p1(X10)
| p2(X10)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f30,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ p3(X5)
| ~ p2(X5)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f31,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p2(X5)
| p3(X5)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f32,plain,
r1(sK18,sK19),
inference(cnf_transformation,[],[f20]) ).
fof(f33,plain,
r1(sK17,sK18),
inference(cnf_transformation,[],[f20]) ).
fof(f34,plain,
r1(sK16,sK17),
inference(cnf_transformation,[],[f20]) ).
fof(f35,plain,
r1(sK15,sK16),
inference(cnf_transformation,[],[f20]) ).
fof(f36,plain,
r1(sK14,sK15),
inference(cnf_transformation,[],[f20]) ).
fof(f37,plain,
r1(sK4,sK14),
inference(cnf_transformation,[],[f20]) ).
fof(f38,plain,
! [X8,X17] :
( ~ r1(sK4,X8)
| ~ r1(X8,X17)
| sP1(X17) ),
inference(cnf_transformation,[],[f20]) ).
fof(f41,plain,
! [X21,X18,X8,X19,X17,X22,X23,X20] :
( ~ r1(sK4,X8)
| ~ r1(X8,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ p5(X23)
| ~ p4(X23) ),
inference(cnf_transformation,[],[f20]) ).
fof(f42,plain,
! [X21,X18,X8,X19,X17,X22,X23,X20] :
( ~ r1(sK4,X8)
| ~ r1(X8,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p4(X23)
| p5(X23) ),
inference(cnf_transformation,[],[f20]) ).
fof(f44,plain,
! [X10,X11,X8,X9,X14,X15,X12,X13] :
( ~ r1(sK4,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ p1(X15)
| ~ p5(X15) ),
inference(cnf_transformation,[],[f20]) ).
fof(f45,plain,
! [X10,X11,X8,X9,X14,X15,X12,X13] :
( ~ r1(sK4,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| p5(X15)
| p1(X15) ),
inference(cnf_transformation,[],[f20]) ).
fof(f53,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f54,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP1(X0)
| sP20(X1) ),
inference(cnf_transformation,[],[f54_D]) ).
fof(f54_D,definition,
! [X1] :
( ! [X0] :
( ~ r1(X0,X1)
| ~ sP1(X0) )
<=> ~ sP20(X1) ),
introduced(definition,[new_symbols(definition,[sP20])],[general_splitting_component_introduction]) ).
fof(f55,plain,
! [X2,X3,X1,X6,X4,X5] :
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p3(X6)
| p4(X6)
| ~ sP20(X1) ),
inference(general_splitting,[],[f25,f54_D]) ).
fof(f56,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| ~ sP20(X1)
| sP21(X2) ),
inference(cnf_transformation,[],[f56_D]) ).
fof(f56_D,definition,
! [X2] :
( ! [X1] :
( ~ r1(X1,X2)
| ~ sP20(X1) )
<=> ~ sP21(X2) ),
introduced(definition,[new_symbols(definition,[sP21])],[general_splitting_component_introduction]) ).
fof(f57,plain,
! [X2,X3,X6,X4,X5] :
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p3(X6)
| p4(X6)
| ~ sP21(X2) ),
inference(general_splitting,[],[f55,f56_D]) ).
fof(f58,plain,
! [X2,X3] :
( ~ r1(X2,X3)
| ~ sP21(X2)
| sP22(X3) ),
inference(cnf_transformation,[],[f58_D]) ).
fof(f58_D,definition,
! [X3] :
( ! [X2] :
( ~ r1(X2,X3)
| ~ sP21(X2) )
<=> ~ sP22(X3) ),
introduced(definition,[new_symbols(definition,[sP22])],[general_splitting_component_introduction]) ).
fof(f59,plain,
! [X3,X6,X4,X5] :
( ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p3(X6)
| p4(X6)
| ~ sP22(X3) ),
inference(general_splitting,[],[f57,f58_D]) ).
fof(f60,plain,
! [X3,X4] :
( ~ r1(X3,X4)
| ~ sP22(X3)
| sP23(X4) ),
inference(cnf_transformation,[],[f60_D]) ).
fof(f60_D,definition,
! [X4] :
( ! [X3] :
( ~ r1(X3,X4)
| ~ sP22(X3) )
<=> ~ sP23(X4) ),
introduced(definition,[new_symbols(definition,[sP23])],[general_splitting_component_introduction]) ).
fof(f61,plain,
! [X6,X4,X5] :
( ~ r1(X4,X5)
| ~ r1(X5,X6)
| p3(X6)
| p4(X6)
| ~ sP23(X4) ),
inference(general_splitting,[],[f59,f60_D]) ).
fof(f62,plain,
! [X6,X5] :
( ~ r1(X5,X6)
| p3(X6)
| p4(X6)
| sP24(X5) ),
inference(cnf_transformation,[],[f62_D]) ).
fof(f62_D,definition,
! [X5] :
( ! [X6] :
( ~ r1(X5,X6)
| p3(X6)
| p4(X6) )
<=> ~ sP24(X5) ),
introduced(definition,[new_symbols(definition,[sP24])],[general_splitting_component_introduction]) ).
fof(f63,plain,
! [X4,X5] :
( ~ r1(X4,X5)
| ~ sP23(X4)
| ~ sP24(X5) ),
inference(general_splitting,[],[f61,f62_D]) ).
fof(f64,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP1(X0)
| sP25(X1) ),
inference(cnf_transformation,[],[f64_D]) ).
fof(f64_D,definition,
! [X1] :
( ! [X0] :
( ~ r1(X0,X1)
| ~ sP1(X0) )
<=> ~ sP25(X1) ),
introduced(definition,[new_symbols(definition,[sP25])],[general_splitting_component_introduction]) ).
fof(f65,plain,
! [X2,X3,X1,X6,X4,X5] :
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ p4(X6)
| ~ p3(X6)
| ~ sP25(X1) ),
inference(general_splitting,[],[f24,f64_D]) ).
fof(f66,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| ~ sP25(X1)
| sP26(X2) ),
inference(cnf_transformation,[],[f66_D]) ).
fof(f66_D,definition,
! [X2] :
( ! [X1] :
( ~ r1(X1,X2)
| ~ sP25(X1) )
<=> ~ sP26(X2) ),
introduced(definition,[new_symbols(definition,[sP26])],[general_splitting_component_introduction]) ).
fof(f67,plain,
! [X2,X3,X6,X4,X5] :
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ p4(X6)
| ~ p3(X6)
| ~ sP26(X2) ),
inference(general_splitting,[],[f65,f66_D]) ).
fof(f68,plain,
! [X2,X3] :
( ~ r1(X2,X3)
| ~ sP26(X2)
| sP27(X3) ),
inference(cnf_transformation,[],[f68_D]) ).
fof(f68_D,definition,
! [X3] :
( ! [X2] :
( ~ r1(X2,X3)
| ~ sP26(X2) )
<=> ~ sP27(X3) ),
introduced(definition,[new_symbols(definition,[sP27])],[general_splitting_component_introduction]) ).
fof(f69,plain,
! [X3,X6,X4,X5] :
( ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ p4(X6)
| ~ p3(X6)
| ~ sP27(X3) ),
inference(general_splitting,[],[f67,f68_D]) ).
fof(f70,plain,
! [X3,X4] :
( ~ r1(X3,X4)
| ~ sP27(X3)
| sP28(X4) ),
inference(cnf_transformation,[],[f70_D]) ).
fof(f70_D,definition,
! [X4] :
( ! [X3] :
( ~ r1(X3,X4)
| ~ sP27(X3) )
<=> ~ sP28(X4) ),
introduced(definition,[new_symbols(definition,[sP28])],[general_splitting_component_introduction]) ).
fof(f71,plain,
! [X6,X4,X5] :
( ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ p4(X6)
| ~ p3(X6)
| ~ sP28(X4) ),
inference(general_splitting,[],[f69,f70_D]) ).
fof(f72,plain,
! [X6,X5] :
( ~ r1(X5,X6)
| ~ p4(X6)
| ~ p3(X6)
| sP29(X5) ),
inference(cnf_transformation,[],[f72_D]) ).
fof(f72_D,definition,
! [X5] :
( ! [X6] :
( ~ r1(X5,X6)
| ~ p4(X6)
| ~ p3(X6) )
<=> ~ sP29(X5) ),
introduced(definition,[new_symbols(definition,[sP29])],[general_splitting_component_introduction]) ).
fof(f73,plain,
! [X4,X5] :
( ~ r1(X4,X5)
| ~ sP28(X4)
| ~ sP29(X5) ),
inference(general_splitting,[],[f71,f72_D]) ).
fof(f74,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP0(X0)
| sP30(X1) ),
inference(cnf_transformation,[],[f74_D]) ).
fof(f74_D,definition,
! [X1] :
( ! [X0] :
( ~ r1(X0,X1)
| ~ sP0(X0) )
<=> ~ sP30(X1) ),
introduced(definition,[new_symbols(definition,[sP30])],[general_splitting_component_introduction]) ).
fof(f75,plain,
! [X2,X3,X1,X4,X5] :
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p2(X5)
| p3(X5)
| ~ sP30(X1) ),
inference(general_splitting,[],[f31,f74_D]) ).
fof(f76,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| ~ sP30(X1)
| sP31(X2) ),
inference(cnf_transformation,[],[f76_D]) ).
fof(f76_D,definition,
! [X2] :
( ! [X1] :
( ~ r1(X1,X2)
| ~ sP30(X1) )
<=> ~ sP31(X2) ),
introduced(definition,[new_symbols(definition,[sP31])],[general_splitting_component_introduction]) ).
fof(f77,plain,
! [X2,X3,X4,X5] :
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p2(X5)
| p3(X5)
| ~ sP31(X2) ),
inference(general_splitting,[],[f75,f76_D]) ).
fof(f78,plain,
! [X2,X3] :
( ~ r1(X2,X3)
| ~ sP31(X2)
| sP32(X3) ),
inference(cnf_transformation,[],[f78_D]) ).
fof(f78_D,definition,
! [X3] :
( ! [X2] :
( ~ r1(X2,X3)
| ~ sP31(X2) )
<=> ~ sP32(X3) ),
introduced(definition,[new_symbols(definition,[sP32])],[general_splitting_component_introduction]) ).
fof(f79,plain,
! [X3,X4,X5] :
( ~ r1(X3,X4)
| ~ r1(X4,X5)
| p2(X5)
| p3(X5)
| ~ sP32(X3) ),
inference(general_splitting,[],[f77,f78_D]) ).
fof(f80,plain,
! [X3,X4] :
( ~ r1(X3,X4)
| ~ sP32(X3)
| sP33(X4) ),
inference(cnf_transformation,[],[f80_D]) ).
fof(f80_D,definition,
! [X4] :
( ! [X3] :
( ~ r1(X3,X4)
| ~ sP32(X3) )
<=> ~ sP33(X4) ),
introduced(definition,[new_symbols(definition,[sP33])],[general_splitting_component_introduction]) ).
fof(f81,plain,
! [X4,X5] :
( ~ r1(X4,X5)
| p2(X5)
| p3(X5)
| ~ sP33(X4) ),
inference(general_splitting,[],[f79,f80_D]) ).
fof(f82,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP0(X0)
| sP34(X1) ),
inference(cnf_transformation,[],[f82_D]) ).
fof(f82_D,definition,
! [X1] :
( ! [X0] :
( ~ r1(X0,X1)
| ~ sP0(X0) )
<=> ~ sP34(X1) ),
introduced(definition,[new_symbols(definition,[sP34])],[general_splitting_component_introduction]) ).
fof(f83,plain,
! [X2,X3,X1,X4,X5] :
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ p3(X5)
| ~ p2(X5)
| ~ sP34(X1) ),
inference(general_splitting,[],[f30,f82_D]) ).
fof(f84,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| ~ sP34(X1)
| sP35(X2) ),
inference(cnf_transformation,[],[f84_D]) ).
fof(f84_D,definition,
! [X2] :
( ! [X1] :
( ~ r1(X1,X2)
| ~ sP34(X1) )
<=> ~ sP35(X2) ),
introduced(definition,[new_symbols(definition,[sP35])],[general_splitting_component_introduction]) ).
fof(f85,plain,
! [X2,X3,X4,X5] :
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ p3(X5)
| ~ p2(X5)
| ~ sP35(X2) ),
inference(general_splitting,[],[f83,f84_D]) ).
fof(f86,plain,
! [X2,X3] :
( ~ r1(X2,X3)
| ~ sP35(X2)
| sP36(X3) ),
inference(cnf_transformation,[],[f86_D]) ).
fof(f86_D,definition,
! [X3] :
( ! [X2] :
( ~ r1(X2,X3)
| ~ sP35(X2) )
<=> ~ sP36(X3) ),
introduced(definition,[new_symbols(definition,[sP36])],[general_splitting_component_introduction]) ).
fof(f87,plain,
! [X3,X4,X5] :
( ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ p3(X5)
| ~ p2(X5)
| ~ sP36(X3) ),
inference(general_splitting,[],[f85,f86_D]) ).
fof(f88,plain,
! [X3,X4] :
( ~ r1(X3,X4)
| ~ sP36(X3)
| sP37(X4) ),
inference(cnf_transformation,[],[f88_D]) ).
fof(f88_D,definition,
! [X4] :
( ! [X3] :
( ~ r1(X3,X4)
| ~ sP36(X3) )
<=> ~ sP37(X4) ),
introduced(definition,[new_symbols(definition,[sP37])],[general_splitting_component_introduction]) ).
fof(f89,plain,
! [X4,X5] :
( ~ r1(X4,X5)
| ~ p3(X5)
| ~ p2(X5)
| ~ sP37(X4) ),
inference(general_splitting,[],[f87,f88_D]) ).
fof(f90,plain,
! [X10,X9] :
( ~ r1(X9,X10)
| p1(X10)
| p2(X10)
| sP38(X9) ),
inference(cnf_transformation,[],[f90_D]) ).
fof(f90_D,definition,
! [X9] :
( ! [X10] :
( ~ r1(X9,X10)
| p1(X10)
| p2(X10) )
<=> ~ sP38(X9) ),
introduced(definition,[new_symbols(definition,[sP38])],[general_splitting_component_introduction]) ).
fof(f91,plain,
! [X0,X1,X8,X9,X7] :
( ~ r1(X0,X1)
| ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ sP0(X0)
| ~ sP38(X9) ),
inference(general_splitting,[],[f27,f90_D]) ).
fof(f92,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP0(X0)
| sP39(X1) ),
inference(cnf_transformation,[],[f92_D]) ).
fof(f92_D,definition,
! [X1] :
( ! [X0] :
( ~ r1(X0,X1)
| ~ sP0(X0) )
<=> ~ sP39(X1) ),
introduced(definition,[new_symbols(definition,[sP39])],[general_splitting_component_introduction]) ).
fof(f93,plain,
! [X1,X8,X9,X7] :
( ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ sP38(X9)
| ~ sP39(X1) ),
inference(general_splitting,[],[f91,f92_D]) ).
fof(f94,plain,
! [X1,X7] :
( ~ r1(X1,X7)
| ~ sP39(X1)
| sP40(X7) ),
inference(cnf_transformation,[],[f94_D]) ).
fof(f94_D,definition,
! [X7] :
( ! [X1] :
( ~ r1(X1,X7)
| ~ sP39(X1) )
<=> ~ sP40(X7) ),
introduced(definition,[new_symbols(definition,[sP40])],[general_splitting_component_introduction]) ).
fof(f95,plain,
! [X8,X9,X7] :
( ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ sP38(X9)
| ~ sP40(X7) ),
inference(general_splitting,[],[f93,f94_D]) ).
fof(f96,plain,
! [X8,X9] :
( ~ r1(X8,X9)
| ~ sP38(X9)
| sP41(X8) ),
inference(cnf_transformation,[],[f96_D]) ).
fof(f96_D,definition,
! [X8] :
( ! [X9] :
( ~ r1(X8,X9)
| ~ sP38(X9) )
<=> ~ sP41(X8) ),
introduced(definition,[new_symbols(definition,[sP41])],[general_splitting_component_introduction]) ).
fof(f97,plain,
! [X8,X7] :
( ~ r1(X7,X8)
| ~ sP40(X7)
| ~ sP41(X8) ),
inference(general_splitting,[],[f95,f96_D]) ).
fof(f98,plain,
! [X10,X9] :
( ~ r1(X9,X10)
| ~ p2(X10)
| ~ p1(X10)
| sP42(X9) ),
inference(cnf_transformation,[],[f98_D]) ).
fof(f98_D,definition,
! [X9] :
( ! [X10] :
( ~ r1(X9,X10)
| ~ p2(X10)
| ~ p1(X10) )
<=> ~ sP42(X9) ),
introduced(definition,[new_symbols(definition,[sP42])],[general_splitting_component_introduction]) ).
fof(f99,plain,
! [X0,X1,X8,X9,X7] :
( ~ r1(X0,X1)
| ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ sP0(X0)
| ~ sP42(X9) ),
inference(general_splitting,[],[f26,f98_D]) ).
fof(f100,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP0(X0)
| sP43(X1) ),
inference(cnf_transformation,[],[f100_D]) ).
fof(f100_D,definition,
! [X1] :
( ! [X0] :
( ~ r1(X0,X1)
| ~ sP0(X0) )
<=> ~ sP43(X1) ),
introduced(definition,[new_symbols(definition,[sP43])],[general_splitting_component_introduction]) ).
fof(f101,plain,
! [X1,X8,X9,X7] :
( ~ r1(X1,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ sP42(X9)
| ~ sP43(X1) ),
inference(general_splitting,[],[f99,f100_D]) ).
fof(f102,plain,
! [X1,X7] :
( ~ r1(X1,X7)
| ~ sP43(X1)
| sP44(X7) ),
inference(cnf_transformation,[],[f102_D]) ).
fof(f102_D,definition,
! [X7] :
( ! [X1] :
( ~ r1(X1,X7)
| ~ sP43(X1) )
<=> ~ sP44(X7) ),
introduced(definition,[new_symbols(definition,[sP44])],[general_splitting_component_introduction]) ).
fof(f103,plain,
! [X8,X9,X7] :
( ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ sP42(X9)
| ~ sP44(X7) ),
inference(general_splitting,[],[f101,f102_D]) ).
fof(f104,plain,
! [X8,X9] :
( ~ r1(X8,X9)
| ~ sP42(X9)
| sP45(X8) ),
inference(cnf_transformation,[],[f104_D]) ).
fof(f104_D,definition,
! [X8] :
( ! [X9] :
( ~ r1(X8,X9)
| ~ sP42(X9) )
<=> ~ sP45(X8) ),
introduced(definition,[new_symbols(definition,[sP45])],[general_splitting_component_introduction]) ).
fof(f105,plain,
! [X8,X7] :
( ~ r1(X7,X8)
| ~ sP44(X7)
| ~ sP45(X8) ),
inference(general_splitting,[],[f103,f104_D]) ).
fof(f106,plain,
! [X8,X9] :
( ~ r1(sK4,X8)
| ~ r1(X8,X9)
| sP46(X9) ),
inference(cnf_transformation,[],[f106_D]) ).
fof(f106_D,definition,
! [X9] :
( ! [X8] :
( ~ r1(sK4,X8)
| ~ r1(X8,X9) )
<=> ~ sP46(X9) ),
introduced(definition,[new_symbols(definition,[sP46])],[general_splitting_component_introduction]) ).
fof(f107,plain,
! [X10,X11,X9,X14,X15,X12,X13] :
( ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| p5(X15)
| p1(X15)
| ~ sP46(X9) ),
inference(general_splitting,[],[f45,f106_D]) ).
fof(f108,plain,
! [X10,X9] :
( ~ r1(X9,X10)
| ~ sP46(X9)
| sP47(X10) ),
inference(cnf_transformation,[],[f108_D]) ).
fof(f108_D,definition,
! [X10] :
( ! [X9] :
( ~ r1(X9,X10)
| ~ sP46(X9) )
<=> ~ sP47(X10) ),
introduced(definition,[new_symbols(definition,[sP47])],[general_splitting_component_introduction]) ).
fof(f109,plain,
! [X10,X11,X14,X15,X12,X13] :
( ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| p5(X15)
| p1(X15)
| ~ sP47(X10) ),
inference(general_splitting,[],[f107,f108_D]) ).
fof(f110,plain,
! [X10,X11] :
( ~ r1(X10,X11)
| ~ sP47(X10)
| sP48(X11) ),
inference(cnf_transformation,[],[f110_D]) ).
fof(f110_D,definition,
! [X11] :
( ! [X10] :
( ~ r1(X10,X11)
| ~ sP47(X10) )
<=> ~ sP48(X11) ),
introduced(definition,[new_symbols(definition,[sP48])],[general_splitting_component_introduction]) ).
fof(f111,plain,
! [X11,X14,X15,X12,X13] :
( ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| p5(X15)
| p1(X15)
| ~ sP48(X11) ),
inference(general_splitting,[],[f109,f110_D]) ).
fof(f112,plain,
! [X11,X12] :
( ~ r1(X11,X12)
| ~ sP48(X11)
| sP49(X12) ),
inference(cnf_transformation,[],[f112_D]) ).
fof(f112_D,definition,
! [X12] :
( ! [X11] :
( ~ r1(X11,X12)
| ~ sP48(X11) )
<=> ~ sP49(X12) ),
introduced(definition,[new_symbols(definition,[sP49])],[general_splitting_component_introduction]) ).
fof(f113,plain,
! [X14,X15,X12,X13] :
( ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| p5(X15)
| p1(X15)
| ~ sP49(X12) ),
inference(general_splitting,[],[f111,f112_D]) ).
fof(f114,plain,
! [X14,X15] :
( ~ r1(X14,X15)
| p5(X15)
| p1(X15)
| sP50(X14) ),
inference(cnf_transformation,[],[f114_D]) ).
fof(f114_D,definition,
! [X14] :
( ! [X15] :
( ~ r1(X14,X15)
| p5(X15)
| p1(X15) )
<=> ~ sP50(X14) ),
introduced(definition,[new_symbols(definition,[sP50])],[general_splitting_component_introduction]) ).
fof(f115,plain,
! [X14,X12,X13] :
( ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ sP49(X12)
| ~ sP50(X14) ),
inference(general_splitting,[],[f113,f114_D]) ).
fof(f116,plain,
! [X14,X13] :
( ~ r1(X13,X14)
| ~ sP50(X14)
| sP51(X13) ),
inference(cnf_transformation,[],[f116_D]) ).
fof(f116_D,definition,
! [X13] :
( ! [X14] :
( ~ r1(X13,X14)
| ~ sP50(X14) )
<=> ~ sP51(X13) ),
introduced(definition,[new_symbols(definition,[sP51])],[general_splitting_component_introduction]) ).
fof(f117,plain,
! [X12,X13] :
( ~ r1(X12,X13)
| ~ sP49(X12)
| ~ sP51(X13) ),
inference(general_splitting,[],[f115,f116_D]) ).
fof(f118,plain,
! [X8,X9] :
( ~ r1(sK4,X8)
| ~ r1(X8,X9)
| sP52(X9) ),
inference(cnf_transformation,[],[f118_D]) ).
fof(f118_D,definition,
! [X9] :
( ! [X8] :
( ~ r1(sK4,X8)
| ~ r1(X8,X9) )
<=> ~ sP52(X9) ),
introduced(definition,[new_symbols(definition,[sP52])],[general_splitting_component_introduction]) ).
fof(f119,plain,
! [X10,X11,X9,X14,X15,X12,X13] :
( ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ p1(X15)
| ~ p5(X15)
| ~ sP52(X9) ),
inference(general_splitting,[],[f44,f118_D]) ).
fof(f120,plain,
! [X10,X9] :
( ~ r1(X9,X10)
| ~ sP52(X9)
| sP53(X10) ),
inference(cnf_transformation,[],[f120_D]) ).
fof(f120_D,definition,
! [X10] :
( ! [X9] :
( ~ r1(X9,X10)
| ~ sP52(X9) )
<=> ~ sP53(X10) ),
introduced(definition,[new_symbols(definition,[sP53])],[general_splitting_component_introduction]) ).
fof(f121,plain,
! [X10,X11,X14,X15,X12,X13] :
( ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ p1(X15)
| ~ p5(X15)
| ~ sP53(X10) ),
inference(general_splitting,[],[f119,f120_D]) ).
fof(f122,plain,
! [X10,X11] :
( ~ r1(X10,X11)
| ~ sP53(X10)
| sP54(X11) ),
inference(cnf_transformation,[],[f122_D]) ).
fof(f122_D,definition,
! [X11] :
( ! [X10] :
( ~ r1(X10,X11)
| ~ sP53(X10) )
<=> ~ sP54(X11) ),
introduced(definition,[new_symbols(definition,[sP54])],[general_splitting_component_introduction]) ).
fof(f123,plain,
! [X11,X14,X15,X12,X13] :
( ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ p1(X15)
| ~ p5(X15)
| ~ sP54(X11) ),
inference(general_splitting,[],[f121,f122_D]) ).
fof(f124,plain,
! [X11,X12] :
( ~ r1(X11,X12)
| ~ sP54(X11)
| sP55(X12) ),
inference(cnf_transformation,[],[f124_D]) ).
fof(f124_D,definition,
! [X12] :
( ! [X11] :
( ~ r1(X11,X12)
| ~ sP54(X11) )
<=> ~ sP55(X12) ),
introduced(definition,[new_symbols(definition,[sP55])],[general_splitting_component_introduction]) ).
fof(f125,plain,
! [X14,X15,X12,X13] :
( ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ p1(X15)
| ~ p5(X15)
| ~ sP55(X12) ),
inference(general_splitting,[],[f123,f124_D]) ).
fof(f126,plain,
! [X14,X15] :
( ~ r1(X14,X15)
| ~ p1(X15)
| ~ p5(X15)
| sP56(X14) ),
inference(cnf_transformation,[],[f126_D]) ).
fof(f126_D,definition,
! [X14] :
( ! [X15] :
( ~ r1(X14,X15)
| ~ p1(X15)
| ~ p5(X15) )
<=> ~ sP56(X14) ),
introduced(definition,[new_symbols(definition,[sP56])],[general_splitting_component_introduction]) ).
fof(f127,plain,
! [X14,X12,X13] :
( ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ sP55(X12)
| ~ sP56(X14) ),
inference(general_splitting,[],[f125,f126_D]) ).
fof(f128,plain,
! [X14,X13] :
( ~ r1(X13,X14)
| ~ sP56(X14)
| sP57(X13) ),
inference(cnf_transformation,[],[f128_D]) ).
fof(f128_D,definition,
! [X13] :
( ! [X14] :
( ~ r1(X13,X14)
| ~ sP56(X14) )
<=> ~ sP57(X13) ),
introduced(definition,[new_symbols(definition,[sP57])],[general_splitting_component_introduction]) ).
fof(f129,plain,
! [X12,X13] :
( ~ r1(X12,X13)
| ~ sP55(X12)
| ~ sP57(X13) ),
inference(general_splitting,[],[f127,f128_D]) ).
fof(f130,plain,
! [X8,X17] :
( ~ r1(sK4,X8)
| ~ r1(X8,X17)
| sP58(X17) ),
inference(cnf_transformation,[],[f130_D]) ).
fof(f130_D,definition,
! [X17] :
( ! [X8] :
( ~ r1(sK4,X8)
| ~ r1(X8,X17) )
<=> ~ sP58(X17) ),
introduced(definition,[new_symbols(definition,[sP58])],[general_splitting_component_introduction]) ).
fof(f131,plain,
! [X21,X18,X19,X17,X22,X23,X20] :
( ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p4(X23)
| p5(X23)
| ~ sP58(X17) ),
inference(general_splitting,[],[f42,f130_D]) ).
fof(f132,plain,
! [X18,X17] :
( ~ r1(X17,X18)
| ~ sP58(X17)
| sP59(X18) ),
inference(cnf_transformation,[],[f132_D]) ).
fof(f132_D,definition,
! [X18] :
( ! [X17] :
( ~ r1(X17,X18)
| ~ sP58(X17) )
<=> ~ sP59(X18) ),
introduced(definition,[new_symbols(definition,[sP59])],[general_splitting_component_introduction]) ).
fof(f133,plain,
! [X21,X18,X19,X22,X23,X20] :
( ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p4(X23)
| p5(X23)
| ~ sP59(X18) ),
inference(general_splitting,[],[f131,f132_D]) ).
fof(f134,plain,
! [X18,X19] :
( ~ r1(X18,X19)
| ~ sP59(X18)
| sP60(X19) ),
inference(cnf_transformation,[],[f134_D]) ).
fof(f134_D,definition,
! [X19] :
( ! [X18] :
( ~ r1(X18,X19)
| ~ sP59(X18) )
<=> ~ sP60(X19) ),
introduced(definition,[new_symbols(definition,[sP60])],[general_splitting_component_introduction]) ).
fof(f135,plain,
! [X21,X19,X22,X23,X20] :
( ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p4(X23)
| p5(X23)
| ~ sP60(X19) ),
inference(general_splitting,[],[f133,f134_D]) ).
fof(f136,plain,
! [X19,X20] :
( ~ r1(X19,X20)
| ~ sP60(X19)
| sP61(X20) ),
inference(cnf_transformation,[],[f136_D]) ).
fof(f136_D,definition,
! [X20] :
( ! [X19] :
( ~ r1(X19,X20)
| ~ sP60(X19) )
<=> ~ sP61(X20) ),
introduced(definition,[new_symbols(definition,[sP61])],[general_splitting_component_introduction]) ).
fof(f137,plain,
! [X21,X22,X23,X20] :
( ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| p4(X23)
| p5(X23)
| ~ sP61(X20) ),
inference(general_splitting,[],[f135,f136_D]) ).
fof(f138,plain,
! [X22,X23] :
( ~ r1(X22,X23)
| p4(X23)
| p5(X23)
| sP62(X22) ),
inference(cnf_transformation,[],[f138_D]) ).
fof(f138_D,definition,
! [X22] :
( ! [X23] :
( ~ r1(X22,X23)
| p4(X23)
| p5(X23) )
<=> ~ sP62(X22) ),
introduced(definition,[new_symbols(definition,[sP62])],[general_splitting_component_introduction]) ).
fof(f139,plain,
! [X21,X22,X20] :
( ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ sP61(X20)
| ~ sP62(X22) ),
inference(general_splitting,[],[f137,f138_D]) ).
fof(f140,plain,
! [X21,X22] :
( ~ r1(X21,X22)
| ~ sP62(X22)
| sP63(X21) ),
inference(cnf_transformation,[],[f140_D]) ).
fof(f140_D,definition,
! [X21] :
( ! [X22] :
( ~ r1(X21,X22)
| ~ sP62(X22) )
<=> ~ sP63(X21) ),
introduced(definition,[new_symbols(definition,[sP63])],[general_splitting_component_introduction]) ).
fof(f141,plain,
! [X21,X20] :
( ~ r1(X20,X21)
| ~ sP61(X20)
| ~ sP63(X21) ),
inference(general_splitting,[],[f139,f140_D]) ).
fof(f142,plain,
! [X8,X17] :
( ~ r1(sK4,X8)
| ~ r1(X8,X17)
| sP64(X17) ),
inference(cnf_transformation,[],[f142_D]) ).
fof(f142_D,definition,
! [X17] :
( ! [X8] :
( ~ r1(sK4,X8)
| ~ r1(X8,X17) )
<=> ~ sP64(X17) ),
introduced(definition,[new_symbols(definition,[sP64])],[general_splitting_component_introduction]) ).
fof(f143,plain,
! [X21,X18,X19,X17,X22,X23,X20] :
( ~ r1(X17,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ p5(X23)
| ~ p4(X23)
| ~ sP64(X17) ),
inference(general_splitting,[],[f41,f142_D]) ).
fof(f144,plain,
! [X18,X17] :
( ~ r1(X17,X18)
| ~ sP64(X17)
| sP65(X18) ),
inference(cnf_transformation,[],[f144_D]) ).
fof(f144_D,definition,
! [X18] :
( ! [X17] :
( ~ r1(X17,X18)
| ~ sP64(X17) )
<=> ~ sP65(X18) ),
introduced(definition,[new_symbols(definition,[sP65])],[general_splitting_component_introduction]) ).
fof(f145,plain,
! [X21,X18,X19,X22,X23,X20] :
( ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ p5(X23)
| ~ p4(X23)
| ~ sP65(X18) ),
inference(general_splitting,[],[f143,f144_D]) ).
fof(f146,plain,
! [X18,X19] :
( ~ r1(X18,X19)
| ~ sP65(X18)
| sP66(X19) ),
inference(cnf_transformation,[],[f146_D]) ).
fof(f146_D,definition,
! [X19] :
( ! [X18] :
( ~ r1(X18,X19)
| ~ sP65(X18) )
<=> ~ sP66(X19) ),
introduced(definition,[new_symbols(definition,[sP66])],[general_splitting_component_introduction]) ).
fof(f147,plain,
! [X21,X19,X22,X23,X20] :
( ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ p5(X23)
| ~ p4(X23)
| ~ sP66(X19) ),
inference(general_splitting,[],[f145,f146_D]) ).
fof(f148,plain,
! [X19,X20] :
( ~ r1(X19,X20)
| ~ sP66(X19)
| sP67(X20) ),
inference(cnf_transformation,[],[f148_D]) ).
fof(f148_D,definition,
! [X20] :
( ! [X19] :
( ~ r1(X19,X20)
| ~ sP66(X19) )
<=> ~ sP67(X20) ),
introduced(definition,[new_symbols(definition,[sP67])],[general_splitting_component_introduction]) ).
fof(f149,plain,
! [X21,X22,X23,X20] :
( ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ p5(X23)
| ~ p4(X23)
| ~ sP67(X20) ),
inference(general_splitting,[],[f147,f148_D]) ).
fof(f150,plain,
! [X22,X23] :
( ~ r1(X22,X23)
| ~ p5(X23)
| ~ p4(X23)
| sP68(X22) ),
inference(cnf_transformation,[],[f150_D]) ).
fof(f150_D,definition,
! [X22] :
( ! [X23] :
( ~ r1(X22,X23)
| ~ p5(X23)
| ~ p4(X23) )
<=> ~ sP68(X22) ),
introduced(definition,[new_symbols(definition,[sP68])],[general_splitting_component_introduction]) ).
fof(f151,plain,
! [X21,X22,X20] :
( ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ sP67(X20)
| ~ sP68(X22) ),
inference(general_splitting,[],[f149,f150_D]) ).
fof(f152,plain,
! [X21,X22] :
( ~ r1(X21,X22)
| ~ sP68(X22)
| sP69(X21) ),
inference(cnf_transformation,[],[f152_D]) ).
fof(f152_D,definition,
! [X21] :
( ! [X22] :
( ~ r1(X21,X22)
| ~ sP68(X22) )
<=> ~ sP69(X21) ),
introduced(definition,[new_symbols(definition,[sP69])],[general_splitting_component_introduction]) ).
fof(f153,plain,
! [X21,X20] :
( ~ r1(X20,X21)
| ~ sP67(X20)
| ~ sP69(X21) ),
inference(general_splitting,[],[f151,f152_D]) ).
fof(f159,plain,
( p3(sK19)
| p4(sK19)
| sP24(sK18) ),
inference(resolution,[],[f32,f62]) ).
fof(f165,plain,
( ~ p4(sK19)
| ~ p3(sK19)
| sP29(sK18) ),
inference(resolution,[],[f32,f72]) ).
fof(f171,plain,
( p2(sK19)
| p3(sK19)
| ~ sP33(sK18) ),
inference(resolution,[],[f32,f81]) ).
fof(f176,plain,
( ~ p3(sK19)
| ~ p2(sK19)
| ~ sP37(sK18) ),
inference(resolution,[],[f32,f89]) ).
fof(f177,plain,
( p1(sK19)
| p2(sK19)
| sP38(sK18) ),
inference(resolution,[],[f32,f90]) ).
fof(f182,plain,
( ~ p2(sK19)
| ~ p1(sK19)
| sP42(sK18) ),
inference(resolution,[],[f32,f98]) ).
fof(f224,definition,
( spl70_9
<=> sP42(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_9])],[avatar_definition]) ).
fof(f228,definition,
( spl70_10
<=> p1(sK19) ),
introduced(definition,[new_symbols(definition,[spl70_10])],[avatar_definition]) ).
fof(f229,plain,
( p1(sK19)
| ~ spl70_10 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f230,plain,
( ~ p1(sK19)
| spl70_10 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f232,definition,
( spl70_11
<=> p2(sK19) ),
introduced(definition,[new_symbols(definition,[spl70_11])],[avatar_definition]) ).
fof(f235,plain,
( spl70_9
| ~ spl70_10
| ~ spl70_11 ),
inference(avatar_split_clause,[],[f182,f232,f228,f224]) ).
fof(f269,definition,
( spl70_19
<=> sP38(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_19])],[avatar_definition]) ).
fof(f272,plain,
( spl70_19
| spl70_11
| spl70_10 ),
inference(avatar_split_clause,[],[f177,f228,f232,f269]) ).
fof(f274,definition,
( spl70_20
<=> sP37(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_20])],[avatar_definition]) ).
fof(f278,definition,
( spl70_21
<=> p3(sK19) ),
introduced(definition,[new_symbols(definition,[spl70_21])],[avatar_definition]) ).
fof(f281,plain,
( ~ spl70_20
| ~ spl70_11
| ~ spl70_21 ),
inference(avatar_split_clause,[],[f176,f278,f232,f274]) ).
fof(f315,definition,
( spl70_29
<=> sP33(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_29])],[avatar_definition]) ).
fof(f318,plain,
( ~ spl70_29
| spl70_21
| spl70_11 ),
inference(avatar_split_clause,[],[f171,f232,f278,f315]) ).
fof(f361,definition,
( spl70_39
<=> sP29(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_39])],[avatar_definition]) ).
fof(f365,definition,
( spl70_40
<=> p4(sK19) ),
introduced(definition,[new_symbols(definition,[spl70_40])],[avatar_definition]) ).
fof(f366,plain,
( p4(sK19)
| ~ spl70_40 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f367,plain,
( ~ p4(sK19)
| spl70_40 ),
inference(avatar_component_clause,[],[f365]) ).
fof(f368,plain,
( spl70_39
| ~ spl70_21
| ~ spl70_40 ),
inference(avatar_split_clause,[],[f165,f365,f278,f361]) ).
fof(f415,definition,
( spl70_51
<=> sP24(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_51])],[avatar_definition]) ).
fof(f418,plain,
( spl70_51
| spl70_40
| spl70_21 ),
inference(avatar_split_clause,[],[f159,f278,f365,f415]) ).
fof(f462,plain,
( ~ sP23(sK17)
| ~ sP24(sK18) ),
inference(resolution,[],[f33,f63]) ).
fof(f468,plain,
( ~ sP28(sK17)
| ~ sP29(sK18) ),
inference(resolution,[],[f33,f73]) ).
fof(f472,plain,
( ~ sP32(sK17)
| sP33(sK18) ),
inference(resolution,[],[f33,f80]) ).
fof(f477,plain,
( ~ sP36(sK17)
| sP37(sK18) ),
inference(resolution,[],[f33,f88]) ).
fof(f482,plain,
( ~ sP38(sK18)
| sP41(sK17) ),
inference(resolution,[],[f33,f96]) ).
fof(f487,plain,
( ~ sP42(sK18)
| sP45(sK17) ),
inference(resolution,[],[f33,f104]) ).
fof(f495,definition,
( spl70_61
<=> sP45(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_61])],[avatar_definition]) ).
fof(f498,plain,
( spl70_61
| ~ spl70_9 ),
inference(avatar_split_clause,[],[f487,f224,f495]) ).
fof(f524,definition,
( spl70_67
<=> sP41(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_67])],[avatar_definition]) ).
fof(f527,plain,
( spl70_67
| ~ spl70_19 ),
inference(avatar_split_clause,[],[f482,f269,f524]) ).
fof(f549,definition,
( spl70_72
<=> sP36(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_72])],[avatar_definition]) ).
fof(f551,plain,
( ~ sP36(sK17)
| spl70_72 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f552,plain,
( spl70_20
| ~ spl70_72 ),
inference(avatar_split_clause,[],[f477,f549,f274]) ).
fof(f562,definition,
( spl70_74
<=> sP32(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_74])],[avatar_definition]) ).
fof(f564,plain,
( ~ sP32(sK17)
| spl70_74 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f565,plain,
( spl70_29
| ~ spl70_74 ),
inference(avatar_split_clause,[],[f472,f562,f315]) ).
fof(f570,definition,
( spl70_75
<=> sP28(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_75])],[avatar_definition]) ).
fof(f572,plain,
( ~ sP28(sK17)
| spl70_75 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f573,plain,
( ~ spl70_39
| ~ spl70_75 ),
inference(avatar_split_clause,[],[f468,f570,f361]) ).
fof(f588,definition,
( spl70_78
<=> sP23(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_78])],[avatar_definition]) ).
fof(f590,plain,
( ~ sP23(sK17)
| spl70_78 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f591,plain,
( ~ spl70_51
| ~ spl70_78 ),
inference(avatar_split_clause,[],[f462,f588,f415]) ).
fof(f606,plain,
( ~ sP22(sK16)
| sP23(sK17) ),
inference(resolution,[],[f34,f60]) ).
fof(f612,plain,
( ~ sP27(sK16)
| sP28(sK17) ),
inference(resolution,[],[f34,f70]) ).
fof(f617,plain,
( ~ sP31(sK16)
| sP32(sK17) ),
inference(resolution,[],[f34,f78]) ).
fof(f622,plain,
( ~ sP35(sK16)
| sP36(sK17) ),
inference(resolution,[],[f34,f86]) ).
fof(f629,plain,
( ~ sP40(sK16)
| ~ sP41(sK17) ),
inference(resolution,[],[f34,f97]) ).
fof(f634,plain,
( ~ sP44(sK16)
| ~ sP45(sK17) ),
inference(resolution,[],[f34,f105]) ).
fof(f636,definition,
( spl70_80
<=> sP44(sK16) ),
introduced(definition,[new_symbols(definition,[spl70_80])],[avatar_definition]) ).
fof(f639,plain,
( ~ spl70_61
| ~ spl70_80 ),
inference(avatar_split_clause,[],[f634,f636,f495]) ).
fof(f665,definition,
( spl70_86
<=> sP40(sK16) ),
introduced(definition,[new_symbols(definition,[spl70_86])],[avatar_definition]) ).
fof(f667,plain,
( ~ sP40(sK16)
| spl70_86 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f668,plain,
( ~ spl70_67
| ~ spl70_86 ),
inference(avatar_split_clause,[],[f629,f665,f524]) ).
fof(f695,plain,
( ~ sP35(sK16)
| spl70_72 ),
inference(forward_subsumption_resolution,[],[f622,f551]) ).
fof(f708,plain,
( ~ sP31(sK16)
| spl70_74 ),
inference(forward_subsumption_resolution,[],[f617,f564]) ).
fof(f725,plain,
( ~ sP27(sK16)
| spl70_75 ),
inference(forward_subsumption_resolution,[],[f612,f572]) ).
fof(f739,plain,
( ~ sP22(sK16)
| spl70_78 ),
inference(forward_subsumption_resolution,[],[f606,f590]) ).
fof(f747,plain,
( ~ sP21(sK15)
| sP22(sK16) ),
inference(resolution,[],[f35,f58]) ).
fof(f753,plain,
( ~ sP26(sK15)
| sP27(sK16) ),
inference(resolution,[],[f35,f68]) ).
fof(f758,plain,
( ~ sP30(sK15)
| sP31(sK16) ),
inference(resolution,[],[f35,f76]) ).
fof(f763,plain,
( ~ sP34(sK15)
| sP35(sK16) ),
inference(resolution,[],[f35,f84]) ).
fof(f769,plain,
( ~ sP39(sK15)
| sP40(sK16) ),
inference(resolution,[],[f35,f94]) ).
fof(f774,plain,
( ~ sP43(sK15)
| sP44(sK16) ),
inference(resolution,[],[f35,f102]) ).
fof(f788,definition,
( spl70_101
<=> sP43(sK15) ),
introduced(definition,[new_symbols(definition,[spl70_101])],[avatar_definition]) ).
fof(f790,plain,
( ~ sP43(sK15)
| spl70_101 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f791,plain,
( spl70_80
| ~ spl70_101 ),
inference(avatar_split_clause,[],[f774,f788,f636]) ).
fof(f816,plain,
( ~ sP39(sK15)
| spl70_86 ),
inference(forward_subsumption_resolution,[],[f769,f667]) ).
fof(f838,plain,
( ~ sP34(sK15)
| spl70_72 ),
inference(forward_subsumption_resolution,[],[f763,f695]) ).
fof(f851,plain,
( ~ sP30(sK15)
| spl70_74 ),
inference(forward_subsumption_resolution,[],[f758,f708]) ).
fof(f868,plain,
( ~ sP26(sK15)
| spl70_75 ),
inference(forward_subsumption_resolution,[],[f753,f725]) ).
fof(f886,plain,
( ~ sP21(sK15)
| spl70_78 ),
inference(forward_subsumption_resolution,[],[f747,f739]) ).
fof(f892,plain,
( ~ sP20(sK14)
| sP21(sK15) ),
inference(resolution,[],[f36,f56]) ).
fof(f898,plain,
( ~ sP25(sK14)
| sP26(sK15) ),
inference(resolution,[],[f36,f66]) ).
fof(f903,plain,
( ~ sP0(sK14)
| sP30(sK15) ),
inference(resolution,[],[f36,f74]) ).
fof(f908,plain,
( ~ sP0(sK14)
| sP34(sK15) ),
inference(resolution,[],[f36,f82]) ).
fof(f914,plain,
( ~ sP0(sK14)
| sP39(sK15) ),
inference(resolution,[],[f36,f92]) ).
fof(f919,plain,
( ~ sP0(sK14)
| sP43(sK15) ),
inference(resolution,[],[f36,f100]) ).
fof(f938,plain,
( ~ sP0(sK14)
| spl70_101 ),
inference(forward_subsumption_resolution,[],[f919,f790]) ).
fof(f963,plain,
( ~ sP0(sK14)
| spl70_86 ),
inference(forward_subsumption_resolution,[],[f914,f816]) ).
fof(f985,plain,
( ~ sP0(sK14)
| spl70_72 ),
inference(forward_subsumption_resolution,[],[f908,f838]) ).
fof(f998,plain,
( ~ sP0(sK14)
| spl70_74 ),
inference(forward_subsumption_resolution,[],[f903,f851]) ).
fof(f1015,plain,
( ~ sP25(sK14)
| spl70_75 ),
inference(forward_subsumption_resolution,[],[f898,f868]) ).
fof(f1029,plain,
( ~ sP20(sK14)
| spl70_78 ),
inference(forward_subsumption_resolution,[],[f892,f886]) ).
fof(f1032,plain,
( sP0(sK14)
| ~ sP1(sK4) ),
inference(resolution,[],[f37,f21]) ).
fof(f1033,plain,
( ~ sP1(sK4)
| sP20(sK14) ),
inference(resolution,[],[f37,f54]) ).
fof(f1039,plain,
( ~ sP1(sK4)
| sP25(sK14) ),
inference(resolution,[],[f37,f64]) ).
fof(f1158,plain,
( ~ sP1(sK4)
| spl70_75 ),
inference(forward_subsumption_resolution,[],[f1039,f1015]) ).
fof(f1176,plain,
( ~ sP1(sK4)
| spl70_78 ),
inference(forward_subsumption_resolution,[],[f1033,f1029]) ).
fof(f1177,plain,
( ~ sP1(sK4)
| spl70_101 ),
inference(forward_subsumption_resolution,[],[f1032,f938]) ).
fof(f2213,plain,
! [X0] :
( ~ sP46(X0)
| sP47(X0) ),
inference(resolution,[],[f108,f53]) ).
fof(f2271,definition,
( spl70_315
<=> sP46(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_315])],[avatar_definition]) ).
fof(f2272,plain,
( sP46(sK14)
| ~ spl70_315 ),
inference(avatar_component_clause,[],[f2271]) ).
fof(f2273,plain,
( ~ sP46(sK14)
| spl70_315 ),
inference(avatar_component_clause,[],[f2271]) ).
fof(f2335,definition,
( spl70_329
<=> sP47(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_329])],[avatar_definition]) ).
fof(f2336,plain,
( ~ sP47(sK14)
| spl70_329 ),
inference(avatar_component_clause,[],[f2335]) ).
fof(f2351,plain,
( ~ sP47(sK14)
| sP48(sK15) ),
inference(resolution,[],[f110,f36]) ).
fof(f2377,definition,
( spl70_334
<=> sP48(sK15) ),
introduced(definition,[new_symbols(definition,[spl70_334])],[avatar_definition]) ).
fof(f2380,plain,
( spl70_334
| ~ spl70_329 ),
inference(avatar_split_clause,[],[f2351,f2335,f2377]) ).
fof(f2438,plain,
( ~ sP48(sK15)
| sP49(sK16) ),
inference(resolution,[],[f112,f35]) ).
fof(f2458,definition,
( spl70_347
<=> sP49(sK16) ),
introduced(definition,[new_symbols(definition,[spl70_347])],[avatar_definition]) ).
fof(f2461,plain,
( spl70_347
| ~ spl70_334 ),
inference(avatar_split_clause,[],[f2438,f2377,f2458]) ).
fof(f2526,plain,
( ~ sP50(sK18)
| sP51(sK17) ),
inference(resolution,[],[f116,f33]) ).
fof(f2538,definition,
( spl70_360
<=> sP51(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_360])],[avatar_definition]) ).
fof(f2542,definition,
( spl70_361
<=> sP50(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_361])],[avatar_definition]) ).
fof(f2544,plain,
( ~ sP50(sK18)
| spl70_361 ),
inference(avatar_component_clause,[],[f2542]) ).
fof(f2545,plain,
( spl70_360
| ~ spl70_361 ),
inference(avatar_split_clause,[],[f2526,f2542,f2538]) ).
fof(f2651,plain,
( ~ sP49(sK16)
| ~ sP51(sK17) ),
inference(resolution,[],[f117,f34]) ).
fof(f2660,plain,
( ~ spl70_360
| ~ spl70_347 ),
inference(avatar_split_clause,[],[f2651,f2458,f2538]) ).
fof(f2683,plain,
! [X0] :
( ~ sP52(X0)
| sP53(X0) ),
inference(resolution,[],[f120,f53]) ).
fof(f2741,definition,
( spl70_395
<=> sP52(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_395])],[avatar_definition]) ).
fof(f2742,plain,
( sP52(sK14)
| ~ spl70_395 ),
inference(avatar_component_clause,[],[f2741]) ).
fof(f2743,plain,
( ~ sP52(sK14)
| spl70_395 ),
inference(avatar_component_clause,[],[f2741]) ).
fof(f2805,definition,
( spl70_409
<=> sP53(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_409])],[avatar_definition]) ).
fof(f2806,plain,
( ~ sP53(sK14)
| spl70_409 ),
inference(avatar_component_clause,[],[f2805]) ).
fof(f2821,plain,
( ~ sP53(sK14)
| sP54(sK15) ),
inference(resolution,[],[f122,f36]) ).
fof(f2847,definition,
( spl70_414
<=> sP54(sK15) ),
introduced(definition,[new_symbols(definition,[spl70_414])],[avatar_definition]) ).
fof(f2850,plain,
( spl70_414
| ~ spl70_409 ),
inference(avatar_split_clause,[],[f2821,f2805,f2847]) ).
fof(f2908,plain,
( ~ sP54(sK15)
| sP55(sK16) ),
inference(resolution,[],[f124,f35]) ).
fof(f2928,definition,
( spl70_427
<=> sP55(sK16) ),
introduced(definition,[new_symbols(definition,[spl70_427])],[avatar_definition]) ).
fof(f2931,plain,
( spl70_427
| ~ spl70_414 ),
inference(avatar_split_clause,[],[f2908,f2847,f2928]) ).
fof(f2996,plain,
( ~ sP56(sK18)
| sP57(sK17) ),
inference(resolution,[],[f128,f33]) ).
fof(f3008,definition,
( spl70_440
<=> sP57(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_440])],[avatar_definition]) ).
fof(f3012,definition,
( spl70_441
<=> sP56(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_441])],[avatar_definition]) ).
fof(f3014,plain,
( ~ sP56(sK18)
| spl70_441 ),
inference(avatar_component_clause,[],[f3012]) ).
fof(f3015,plain,
( spl70_440
| ~ spl70_441 ),
inference(avatar_split_clause,[],[f2996,f3012,f3008]) ).
fof(f3121,plain,
( ~ sP55(sK16)
| ~ sP57(sK17) ),
inference(resolution,[],[f129,f34]) ).
fof(f3130,plain,
( ~ spl70_440
| ~ spl70_427 ),
inference(avatar_split_clause,[],[f3121,f2928,f3008]) ).
fof(f3153,plain,
! [X0] :
( ~ sP58(X0)
| sP59(X0) ),
inference(resolution,[],[f132,f53]) ).
fof(f3211,definition,
( spl70_475
<=> sP58(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_475])],[avatar_definition]) ).
fof(f3212,plain,
( sP58(sK14)
| ~ spl70_475 ),
inference(avatar_component_clause,[],[f3211]) ).
fof(f3213,plain,
( ~ sP58(sK14)
| spl70_475 ),
inference(avatar_component_clause,[],[f3211]) ).
fof(f3275,definition,
( spl70_489
<=> sP59(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_489])],[avatar_definition]) ).
fof(f3276,plain,
( ~ sP59(sK14)
| spl70_489 ),
inference(avatar_component_clause,[],[f3275]) ).
fof(f3291,plain,
( ~ sP59(sK14)
| sP60(sK15) ),
inference(resolution,[],[f134,f36]) ).
fof(f3317,definition,
( spl70_494
<=> sP60(sK15) ),
introduced(definition,[new_symbols(definition,[spl70_494])],[avatar_definition]) ).
fof(f3320,plain,
( spl70_494
| ~ spl70_489 ),
inference(avatar_split_clause,[],[f3291,f3275,f3317]) ).
fof(f3378,plain,
( ~ sP60(sK15)
| sP61(sK16) ),
inference(resolution,[],[f136,f35]) ).
fof(f3398,definition,
( spl70_507
<=> sP61(sK16) ),
introduced(definition,[new_symbols(definition,[spl70_507])],[avatar_definition]) ).
fof(f3401,plain,
( spl70_507
| ~ spl70_494 ),
inference(avatar_split_clause,[],[f3378,f3317,f3398]) ).
fof(f3466,plain,
( ~ sP62(sK18)
| sP63(sK17) ),
inference(resolution,[],[f140,f33]) ).
fof(f3478,definition,
( spl70_520
<=> sP63(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_520])],[avatar_definition]) ).
fof(f3482,definition,
( spl70_521
<=> sP62(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_521])],[avatar_definition]) ).
fof(f3484,plain,
( ~ sP62(sK18)
| spl70_521 ),
inference(avatar_component_clause,[],[f3482]) ).
fof(f3485,plain,
( spl70_520
| ~ spl70_521 ),
inference(avatar_split_clause,[],[f3466,f3482,f3478]) ).
fof(f3591,plain,
( ~ sP61(sK16)
| ~ sP63(sK17) ),
inference(resolution,[],[f141,f34]) ).
fof(f3600,plain,
( ~ spl70_520
| ~ spl70_507 ),
inference(avatar_split_clause,[],[f3591,f3398,f3478]) ).
fof(f3635,plain,
( ~ sP64(sK14)
| sP65(sK15) ),
inference(resolution,[],[f144,f36]) ).
fof(f3677,definition,
( spl70_554
<=> sP65(sK15) ),
introduced(definition,[new_symbols(definition,[spl70_554])],[avatar_definition]) ).
fof(f3681,definition,
( spl70_555
<=> sP64(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_555])],[avatar_definition]) ).
fof(f3683,plain,
( ~ sP64(sK14)
| spl70_555 ),
inference(avatar_component_clause,[],[f3681]) ).
fof(f3684,plain,
( spl70_554
| ~ spl70_555 ),
inference(avatar_split_clause,[],[f3635,f3681,f3677]) ).
fof(f3762,plain,
( ~ sP65(sK15)
| sP66(sK16) ),
inference(resolution,[],[f146,f35]) ).
fof(f3782,definition,
( spl70_573
<=> sP66(sK16) ),
introduced(definition,[new_symbols(definition,[spl70_573])],[avatar_definition]) ).
fof(f3785,plain,
( spl70_573
| ~ spl70_554 ),
inference(avatar_split_clause,[],[f3762,f3677,f3782]) ).
fof(f3849,plain,
( ~ sP66(sK16)
| sP67(sK17) ),
inference(resolution,[],[f148,f34]) ).
fof(f3863,definition,
( spl70_586
<=> sP67(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_586])],[avatar_definition]) ).
fof(f3866,plain,
( spl70_586
| ~ spl70_573 ),
inference(avatar_split_clause,[],[f3849,f3782,f3863]) ).
fof(f3936,plain,
( ~ sP68(sK18)
| sP69(sK17) ),
inference(resolution,[],[f152,f33]) ).
fof(f3948,definition,
( spl70_600
<=> sP69(sK17) ),
introduced(definition,[new_symbols(definition,[spl70_600])],[avatar_definition]) ).
fof(f3950,plain,
( sP69(sK17)
| ~ spl70_600 ),
inference(avatar_component_clause,[],[f3948]) ).
fof(f3952,definition,
( spl70_601
<=> sP68(sK18) ),
introduced(definition,[new_symbols(definition,[spl70_601])],[avatar_definition]) ).
fof(f3955,plain,
( spl70_600
| ~ spl70_601 ),
inference(avatar_split_clause,[],[f3936,f3952,f3948]) ).
fof(f4047,plain,
! [X0] :
( ~ sP69(X0)
| ~ sP67(X0) ),
inference(resolution,[],[f153,f53]) ).
fof(f4096,plain,
! [X0] :
( ~ r1(sK4,X0)
| sP1(X0) ),
inference(resolution,[],[f38,f53]) ).
fof(f4115,plain,
! [X0] :
( ~ r1(sK14,X0)
| sP46(X0) ),
inference(resolution,[],[f106,f37]) ).
fof(f4123,plain,
! [X0] :
( ~ r1(sK14,X0)
| sP52(X0) ),
inference(resolution,[],[f118,f37]) ).
fof(f4131,plain,
! [X0] :
( ~ r1(sK14,X0)
| sP58(X0) ),
inference(resolution,[],[f130,f37]) ).
fof(f4139,plain,
! [X0] :
( ~ r1(sK14,X0)
| sP64(X0) ),
inference(resolution,[],[f142,f37]) ).
fof(f4163,plain,
( p5(sK19)
| p1(sK19)
| sP50(sK18) ),
inference(resolution,[],[f114,f32]) ).
fof(f4194,plain,
( ~ p1(sK19)
| ~ p5(sK19)
| sP56(sK18) ),
inference(resolution,[],[f126,f32]) ).
fof(f4195,plain,
( ~ p5(sK19)
| sP56(sK18)
| ~ spl70_10 ),
inference(forward_subsumption_resolution,[],[f4194,f229]) ).
fof(f4208,plain,
( ~ p5(sK19)
| ~ spl70_10
| spl70_441 ),
inference(forward_subsumption_resolution,[],[f4195,f3014]) ).
fof(f4245,plain,
( p4(sK19)
| p5(sK19)
| sP62(sK18) ),
inference(resolution,[],[f138,f32]) ).
fof(f4246,plain,
( p5(sK19)
| sP62(sK18)
| spl70_40 ),
inference(forward_subsumption_resolution,[],[f4245,f367]) ).
fof(f4260,plain,
( sP62(sK18)
| ~ spl70_10
| spl70_40
| spl70_441 ),
inference(forward_subsumption_resolution,[],[f4246,f4208]) ).
fof(f4277,plain,
( $false
| ~ spl70_10
| spl70_40
| spl70_441
| spl70_521 ),
inference(forward_subsumption_resolution,[],[f4260,f3484]) ).
fof(f4278,plain,
( ~ spl70_10
| spl70_40
| spl70_441
| spl70_521 ),
inference(avatar_contradiction_clause,[],[f4277]) ).
fof(f4316,plain,
( p5(sK19)
| sP50(sK18)
| spl70_10 ),
inference(forward_subsumption_resolution,[],[f4163,f230]) ).
fof(f4327,plain,
( p5(sK19)
| spl70_10
| spl70_361 ),
inference(forward_subsumption_resolution,[],[f4316,f2544]) ).
fof(f4344,plain,
( ~ p5(sK19)
| ~ p4(sK19)
| sP68(sK18) ),
inference(resolution,[],[f150,f32]) ).
fof(f4788,plain,
sP1(sK4),
inference(resolution,[],[f4096,f53]) ).
fof(f4794,plain,
( $false
| spl70_75 ),
inference(forward_subsumption_resolution,[],[f4788,f1158]) ).
fof(f4795,plain,
spl70_75,
inference(avatar_contradiction_clause,[],[f4794]) ).
fof(f4811,definition,
( spl70_703
<=> sP1(sK4) ),
introduced(definition,[new_symbols(definition,[spl70_703])],[avatar_definition]) ).
fof(f4812,plain,
( sP1(sK4)
| ~ spl70_703 ),
inference(avatar_component_clause,[],[f4811]) ).
fof(f4815,plain,
( ~ spl70_703
| spl70_78 ),
inference(avatar_split_clause,[],[f1176,f588,f4811]) ).
fof(f4816,plain,
( ~ spl70_703
| spl70_101 ),
inference(avatar_split_clause,[],[f1177,f788,f4811]) ).
fof(f4835,plain,
spl70_703,
inference(avatar_split_clause,[],[f4788,f4811]) ).
fof(f4870,plain,
( ~ sP1(sK4)
| spl70_86 ),
inference(forward_subsumption_resolution,[],[f1032,f963]) ).
fof(f4890,plain,
( $false
| spl70_86
| ~ spl70_703 ),
inference(forward_subsumption_resolution,[],[f4870,f4812]) ).
fof(f4891,plain,
( spl70_86
| ~ spl70_703 ),
inference(avatar_contradiction_clause,[],[f4890]) ).
fof(f4910,definition,
( spl70_719
<=> sP0(sK14) ),
introduced(definition,[new_symbols(definition,[spl70_719])],[avatar_definition]) ).
fof(f4914,plain,
( ~ spl70_719
| spl70_72 ),
inference(avatar_split_clause,[],[f985,f549,f4910]) ).
fof(f4915,plain,
( ~ spl70_719
| spl70_74 ),
inference(avatar_split_clause,[],[f998,f562,f4910]) ).
fof(f4916,plain,
( sP0(sK14)
| ~ spl70_703 ),
inference(forward_subsumption_resolution,[],[f1032,f4812]) ).
fof(f4918,plain,
( spl70_719
| ~ spl70_703 ),
inference(avatar_split_clause,[],[f4916,f4811,f4910]) ).
fof(f4960,plain,
( ~ p4(sK19)
| sP68(sK18)
| spl70_10
| spl70_361 ),
inference(forward_subsumption_resolution,[],[f4344,f4327]) ).
fof(f4966,plain,
( sP68(sK18)
| spl70_10
| ~ spl70_40
| spl70_361 ),
inference(forward_subsumption_resolution,[],[f4960,f366]) ).
fof(f5014,plain,
sP46(sK14),
inference(resolution,[],[f4115,f53]) ).
fof(f5020,plain,
( $false
| spl70_315 ),
inference(forward_subsumption_resolution,[],[f5014,f2273]) ).
fof(f5021,plain,
spl70_315,
inference(avatar_contradiction_clause,[],[f5020]) ).
fof(f5024,plain,
( spl70_601
| spl70_10
| ~ spl70_40
| spl70_361 ),
inference(avatar_split_clause,[],[f4966,f2542,f365,f228,f3952]) ).
fof(f5030,plain,
( sP47(sK14)
| ~ spl70_315 ),
inference(resolution,[],[f2272,f2213]) ).
fof(f5031,plain,
( $false
| ~ spl70_315
| spl70_329 ),
inference(forward_subsumption_resolution,[],[f5030,f2336]) ).
fof(f5032,plain,
( ~ spl70_315
| spl70_329 ),
inference(avatar_contradiction_clause,[],[f5031]) ).
fof(f5042,plain,
( ~ sP67(sK17)
| ~ spl70_600 ),
inference(resolution,[],[f3950,f4047]) ).
fof(f5043,plain,
( ~ spl70_586
| ~ spl70_600 ),
inference(avatar_split_clause,[],[f5042,f3948,f3863]) ).
fof(f5121,plain,
sP52(sK14),
inference(resolution,[],[f4123,f53]) ).
fof(f5127,plain,
( $false
| spl70_395 ),
inference(forward_subsumption_resolution,[],[f5121,f2743]) ).
fof(f5128,plain,
spl70_395,
inference(avatar_contradiction_clause,[],[f5127]) ).
fof(f5136,plain,
( sP53(sK14)
| ~ spl70_395 ),
inference(resolution,[],[f2742,f2683]) ).
fof(f5137,plain,
( $false
| ~ spl70_395
| spl70_409 ),
inference(forward_subsumption_resolution,[],[f5136,f2806]) ).
fof(f5138,plain,
( ~ spl70_395
| spl70_409 ),
inference(avatar_contradiction_clause,[],[f5137]) ).
fof(f5214,plain,
sP58(sK14),
inference(resolution,[],[f4131,f53]) ).
fof(f5220,plain,
( $false
| spl70_475 ),
inference(forward_subsumption_resolution,[],[f5214,f3213]) ).
fof(f5221,plain,
spl70_475,
inference(avatar_contradiction_clause,[],[f5220]) ).
fof(f5229,plain,
( sP59(sK14)
| ~ spl70_475 ),
inference(resolution,[],[f3212,f3153]) ).
fof(f5230,plain,
( $false
| ~ spl70_475
| spl70_489 ),
inference(forward_subsumption_resolution,[],[f5229,f3276]) ).
fof(f5231,plain,
( ~ spl70_475
| spl70_489 ),
inference(avatar_contradiction_clause,[],[f5230]) ).
fof(f5308,plain,
sP64(sK14),
inference(resolution,[],[f4139,f53]) ).
fof(f5314,plain,
( $false
| spl70_555 ),
inference(forward_subsumption_resolution,[],[f5308,f3683]) ).
fof(f5315,plain,
spl70_555,
inference(avatar_contradiction_clause,[],[f5314]) ).
cnf(s5,plain,
( spl70_9
| ~ spl70_10
| ~ spl70_11 ),
inference(sat_conversion,[],[f235]) ).
cnf(s10,plain,
( spl70_10
| spl70_11
| spl70_19 ),
inference(sat_conversion,[],[f272]) ).
cnf(s11,plain,
( ~ spl70_11
| ~ spl70_20
| ~ spl70_21 ),
inference(sat_conversion,[],[f281]) ).
cnf(s16,plain,
( spl70_11
| spl70_21
| ~ spl70_29 ),
inference(sat_conversion,[],[f318]) ).
cnf(s22,plain,
( ~ spl70_21
| spl70_39
| ~ spl70_40 ),
inference(sat_conversion,[],[f368]) ).
cnf(s28,plain,
( spl70_21
| spl70_40
| spl70_51 ),
inference(sat_conversion,[],[f418]) ).
cnf(s35,plain,
( ~ spl70_9
| spl70_61 ),
inference(sat_conversion,[],[f498]) ).
cnf(s39,plain,
( ~ spl70_19
| spl70_67 ),
inference(sat_conversion,[],[f527]) ).
cnf(s43,plain,
( spl70_20
| ~ spl70_72 ),
inference(sat_conversion,[],[f552]) ).
cnf(s45,plain,
( spl70_29
| ~ spl70_74 ),
inference(sat_conversion,[],[f565]) ).
cnf(s46,plain,
( ~ spl70_39
| ~ spl70_75 ),
inference(sat_conversion,[],[f573]) ).
cnf(s48,plain,
( ~ spl70_51
| ~ spl70_78 ),
inference(sat_conversion,[],[f591]) ).
cnf(s50,plain,
( ~ spl70_61
| ~ spl70_80 ),
inference(sat_conversion,[],[f639]) ).
cnf(s54,plain,
( ~ spl70_67
| ~ spl70_86 ),
inference(sat_conversion,[],[f668]) ).
cnf(s67,plain,
( spl70_80
| ~ spl70_101 ),
inference(sat_conversion,[],[f791]) ).
cnf(s238,plain,
( ~ spl70_329
| spl70_334 ),
inference(sat_conversion,[],[f2380]) ).
cnf(s250,plain,
( ~ spl70_334
| spl70_347 ),
inference(sat_conversion,[],[f2461]) ).
cnf(s261,plain,
( spl70_360
| ~ spl70_361 ),
inference(sat_conversion,[],[f2545]) ).
cnf(s275,plain,
( ~ spl70_347
| ~ spl70_360 ),
inference(sat_conversion,[],[f2660]) ).
cnf(s303,plain,
( ~ spl70_409
| spl70_414 ),
inference(sat_conversion,[],[f2850]) ).
cnf(s315,plain,
( ~ spl70_414
| spl70_427 ),
inference(sat_conversion,[],[f2931]) ).
cnf(s326,plain,
( spl70_440
| ~ spl70_441 ),
inference(sat_conversion,[],[f3015]) ).
cnf(s340,plain,
( ~ spl70_427
| ~ spl70_440 ),
inference(sat_conversion,[],[f3130]) ).
cnf(s368,plain,
( ~ spl70_489
| spl70_494 ),
inference(sat_conversion,[],[f3320]) ).
cnf(s380,plain,
( ~ spl70_494
| spl70_507 ),
inference(sat_conversion,[],[f3401]) ).
cnf(s391,plain,
( spl70_520
| ~ spl70_521 ),
inference(sat_conversion,[],[f3485]) ).
cnf(s405,plain,
( ~ spl70_507
| ~ spl70_520 ),
inference(sat_conversion,[],[f3600]) ).
cnf(s420,plain,
( spl70_554
| ~ spl70_555 ),
inference(sat_conversion,[],[f3684]) ).
cnf(s432,plain,
( ~ spl70_554
| spl70_573 ),
inference(sat_conversion,[],[f3785]) ).
cnf(s444,plain,
( ~ spl70_573
| spl70_586 ),
inference(sat_conversion,[],[f3866]) ).
cnf(s456,plain,
( spl70_600
| ~ spl70_601 ),
inference(sat_conversion,[],[f3955]) ).
cnf(s490,plain,
( ~ spl70_10
| spl70_40
| spl70_441
| spl70_521 ),
inference(sat_conversion,[],[f4278]) ).
cnf(s579,plain,
spl70_75,
inference(sat_conversion,[],[f4795]) ).
cnf(s583,plain,
( spl70_78
| ~ spl70_703 ),
inference(sat_conversion,[],[f4815]) ).
cnf(s584,plain,
( spl70_101
| ~ spl70_703 ),
inference(sat_conversion,[],[f4816]) ).
cnf(s588,plain,
spl70_703,
inference(sat_conversion,[],[f4835]) ).
cnf(s601,plain,
( spl70_86
| ~ spl70_703 ),
inference(sat_conversion,[],[f4891]) ).
cnf(s607,plain,
( spl70_72
| ~ spl70_719 ),
inference(sat_conversion,[],[f4914]) ).
cnf(s608,plain,
( spl70_74
| ~ spl70_719 ),
inference(sat_conversion,[],[f4915]) ).
cnf(s610,plain,
( ~ spl70_703
| spl70_719 ),
inference(sat_conversion,[],[f4918]) ).
cnf(s632,plain,
spl70_315,
inference(sat_conversion,[],[f5021]) ).
cnf(s634,plain,
( spl70_10
| ~ spl70_40
| spl70_361
| spl70_601 ),
inference(sat_conversion,[],[f5024]) ).
cnf(s636,plain,
( ~ spl70_315
| spl70_329 ),
inference(sat_conversion,[],[f5032]) ).
cnf(s639,plain,
( ~ spl70_586
| ~ spl70_600 ),
inference(sat_conversion,[],[f5043]) ).
cnf(s659,plain,
spl70_395,
inference(sat_conversion,[],[f5128]) ).
cnf(s662,plain,
( ~ spl70_395
| spl70_409 ),
inference(sat_conversion,[],[f5138]) ).
cnf(s679,plain,
spl70_475,
inference(sat_conversion,[],[f5221]) ).
cnf(s682,plain,
( ~ spl70_475
| spl70_489 ),
inference(sat_conversion,[],[f5231]) ).
cnf(s699,plain,
spl70_555,
inference(sat_conversion,[],[f5315]) ).
cnf(s709,plain,
spl70_489,
inference(rat,[],[s682,s679]) ).
cnf(s720,plain,
spl70_409,
inference(rat,[],[s662,s659]) ).
cnf(s731,plain,
spl70_329,
inference(rat,[],[s636,s632]) ).
cnf(s735,plain,
spl70_719,
inference(rat,[],[s610,s588]) ).
cnf(s738,plain,
spl70_86,
inference(rat,[],[s601,s588]) ).
cnf(s755,plain,
spl70_74,
inference(rat,[],[s608,s735]) ).
cnf(s756,plain,
spl70_72,
inference(rat,[],[s607,s735]) ).
cnf(s776,plain,
spl70_101,
inference(rat,[],[s584,s588]) ).
cnf(s777,plain,
spl70_78,
inference(rat,[],[s583,s588]) ).
cnf(s838,plain,
spl70_554,
inference(rat,[],[s420,s699]) ).
cnf(s839,plain,
spl70_573,
inference(rat,[],[s432,s838]) ).
cnf(s840,plain,
spl70_586,
inference(rat,[],[s444,s839]) ).
cnf(s841,plain,
~ spl70_600,
inference(rat,[],[s639,s840]) ).
cnf(s843,plain,
~ spl70_601,
inference(rat,[],[s456,s841]) ).
cnf(s868,plain,
spl70_494,
inference(rat,[],[s368,s709]) ).
cnf(s869,plain,
spl70_507,
inference(rat,[],[s380,s868]) ).
cnf(s870,plain,
~ spl70_520,
inference(rat,[],[s405,s869]) ).
cnf(s871,plain,
~ spl70_521,
inference(rat,[],[s391,s870]) ).
cnf(s909,plain,
spl70_414,
inference(rat,[],[s303,s720]) ).
cnf(s910,plain,
spl70_427,
inference(rat,[],[s315,s909]) ).
cnf(s911,plain,
~ spl70_440,
inference(rat,[],[s340,s910]) ).
cnf(s912,plain,
~ spl70_441,
inference(rat,[],[s326,s911]) ).
cnf(s950,plain,
spl70_334,
inference(rat,[],[s238,s731]) ).
cnf(s951,plain,
spl70_347,
inference(rat,[],[s250,s950]) ).
cnf(s952,plain,
~ spl70_360,
inference(rat,[],[s275,s951]) ).
cnf(s953,plain,
~ spl70_361,
inference(rat,[],[s261,s952]) ).
cnf(s1004,plain,
spl70_80,
inference(rat,[],[s67,s776]) ).
cnf(s1005,plain,
~ spl70_67,
inference(rat,[],[s54,s738]) ).
cnf(s1007,plain,
~ spl70_61,
inference(rat,[],[s50,s1004]) ).
cnf(s1008,plain,
~ spl70_51,
inference(rat,[],[s48,s777]) ).
cnf(s1009,plain,
~ spl70_39,
inference(rat,[],[s46,s579]) ).
cnf(s1010,plain,
spl70_29,
inference(rat,[],[s45,s755]) ).
cnf(s1011,plain,
spl70_20,
inference(rat,[],[s43,s756]) ).
cnf(s1013,plain,
~ spl70_19,
inference(rat,[],[s39,s1005]) ).
cnf(s1016,plain,
~ spl70_9,
inference(rat,[],[s35,s1007]) ).
cnf(s1019,plain,
( spl70_21
| spl70_40 ),
inference(rat,[],[s28,s1008]) ).
cnf(s1022,plain,
( ~ spl70_21
| ~ spl70_40 ),
inference(rat,[],[s22,s1009]) ).
cnf(s1026,plain,
( spl70_11
| spl70_21 ),
inference(rat,[],[s16,s1010]) ).
cnf(s1029,plain,
( ~ spl70_11
| ~ spl70_21 ),
inference(rat,[],[s11,s1011]) ).
cnf(s1030,plain,
( spl70_10
| spl70_11 ),
inference(rat,[],[s10,s1013]) ).
cnf(s1033,plain,
( ~ spl70_10
| ~ spl70_11 ),
inference(rat,[],[s5,s1016]) ).
cnf(s1036,plain,
spl70_10,
inference(rat,[],[s1029,s1019,s1030,s634,s953,s843]) ).
cnf(s1037,plain,
spl70_40,
inference(rat,[],[s490,s871,s912,s1036]) ).
cnf(s1038,plain,
~ spl70_11,
inference(rat,[],[s1033,s1036]) ).
cnf(s1039,plain,
~ spl70_21,
inference(rat,[],[s1022,s1037]) ).
cnf(s1040,plain,
$false,
inference(rat,[],[s1026,s1039,s1038]) ).
fof(f5318,plain,
$false,
inference(avatar_sat_refutation,[],[s1040]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n004.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 16:27:36 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.33/1.32 % (3714945)Detected formulas, will run a generic FOF schedule.
% 3.33/1.32 % (3715048)dis-21_1_sil=8000:lcm=predicate:random_seed=3014466416:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.33/1.32 % (3715048)Instruction limit reached!
% 3.33/1.32 % (3715048)------------------------------
% 3.33/1.32 % (3715048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.32 % (3715048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.32 % (3715048)CaDiCaL version: 2.1.3
% 3.33/1.32 % (3715048)Termination reason: Instruction limit
% 3.33/1.32 % (3715048)Termination phase: Saturation
% 3.33/1.32 % (3715048)Time elapsed: 0.023 s
% 3.33/1.32 % (3715048)Peak memory usage: 88 MB
% 3.33/1.32 % (3715048)Instructions burned: 131 (million)
% 3.33/1.32 % (3715046)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3978712944:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.33/1.32 % (3715045)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2499710610:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.33/1.32 % (3715042)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2574564200:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.33/1.32 % (3715044)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3118607804:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.33/1.32 % (3715043)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4223296519:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.33/1.32 % (3715045)First to succeed.
% 3.33/1.32 % (3715046)Instruction limit reached!
% 3.33/1.32 % (3715046)------------------------------
% 3.33/1.32 % (3715046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.32 % (3715046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.32 % (3715046)CaDiCaL version: 2.1.3
% 3.33/1.32 % (3715046)Termination reason: Instruction limit
% 3.33/1.32 % (3715046)Termination phase: Saturation
% 3.33/1.32 % (3715046)Time elapsed: 0.052 s
% 3.33/1.32 % (3715046)Peak memory usage: 88 MB
% 3.33/1.32 % (3715046)Instructions burned: 120 (million)
% 3.33/1.32 % (3715045)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3714945"
% 3.33/1.32 % (3715047)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3812307766:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.33/1.32 % (3715063)lrs+10_1_sil=8000:sp=occurrence:random_seed=98132283:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.33/1.32 % (3715047)Instruction limit reached!
% 3.33/1.32 % (3715047)------------------------------
% 3.33/1.32 % (3715047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.32 % (3715047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.32 % (3715047)CaDiCaL version: 2.1.3
% 3.33/1.32 % (3715047)Termination reason: Instruction limit
% 3.33/1.32 % (3715047)Termination phase: Saturation
% 3.33/1.32 % (3715047)Time elapsed: 0.083 s
% 3.33/1.32 % (3715047)Peak memory usage: 88 MB
% 3.33/1.32 % (3715047)Instructions burned: 140 (million)
% 3.33/1.32 % (3715063)Instruction limit reached!
% 3.33/1.32 % (3715063)------------------------------
% 3.33/1.32 % (3715063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.32 % (3715063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.32 % (3715063)CaDiCaL version: 2.1.3
% 3.33/1.32 % (3715063)Termination reason: Instruction limit
% 3.33/1.32 % (3715063)Termination phase: Saturation
% 3.33/1.32 % (3715063)Time elapsed: 0.069 s
% 3.33/1.32 % (3715063)Peak memory usage: 90 MB
% 3.33/1.32 % (3715063)Instructions burned: 289 (million)
% 3.33/1.32 % (3715069)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1786228205:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.33/1.32 % (3715069)Instruction limit reached!
% 3.33/1.32 % (3715069)------------------------------
% 3.33/1.32 % (3715069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.33/1.32 % (3715069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/1.32 % (3715069)CaDiCaL version: 2.1.3
% 3.33/1.32 % (3715069)Termination reason: Instruction limit
% 3.33/1.32 % (3715069)Termination phase: Saturation
% 3.33/1.32 % (3715069)Time elapsed: 0.069 s
% 3.33/1.32 % (3715069)Peak memory usage: 90 MB
% 3.33/1.32 % (3715069)Instructions burned: 158 (million)
% 3.33/1.32 % (3715073)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3300976780:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 3.33/1.32 % (3715045)Refutation found. Thanks to Tanya!
% 3.33/1.32 % SZS status Theorem for theBenchmark
% 3.33/1.32 % SZS output start Proof for theBenchmark
% See solution above
% 3.88/1.52 % (3715045)------------------------------
% 3.88/1.52 % (3715045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.88/1.52 % (3715045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.88/1.52 % (3715045)CaDiCaL version: 2.1.3
% 3.88/1.52 % (3715045)Termination reason: Refutation
% 3.88/1.52 % (3715045)Time elapsed: 0.052 s
% 3.88/1.52 % (3715045)Peak memory usage: 91 MB
% 3.88/1.52 % (3715045)Instructions burned: 93 (million)
% 3.88/1.52 % (3715045)------------------------------
% 3.88/1.52 % (3715045)------------------------------
% 3.88/1.52 % (3714945)Success in time 0.461 s
% 3.88/1.52 % Vampire exiting
%------------------------------------------------------------------------------