%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL660+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:59:30 AM UTC 2026
% Result : Theorem 1.06s 0.68s
% Output : Refutation 1.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 53
% Syntax : Number of formulae : 559 ( 17 unt; 51 def)
% Number of atoms : 2934 ( 0 equ)
% Maximal formula atoms : 120 ( 5 avg)
% Number of connectives : 4121 (1746 ~;2168 |; 156 &)
% ( 51 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 63 ( 62 usr; 52 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 5 con; 0-1 aty)
% Number of variables : 691 ( 0 sgn 619 !; 72 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ p4(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ( ( ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ~ ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ p4(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ( ( ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ~ ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) )
& ( ! [X2] :
( ~ r1(X0,X2)
| p2(X2) )
| ~ ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p2(X5) )
| ~ p2(X4) ) ) ) )
| ! [X6] :
( ~ r1(X0,X6)
| p4(X6) )
| ~ ! [X7] :
( ~ r1(X0,X7)
| p4(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p4(X9) )
| ~ p4(X8) ) )
| ( ~ ! [X10] :
( ~ r1(X0,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p3(X11) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| p2(X12) )
| ~ ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) ) )
| ! [X16] :
( ~ r1(X0,X16)
| p1(X16) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) )
| ~ ( ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ~ ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23) )
| ~ p2(X22) ) ) )
| ~ ! [X24] :
( ~ r1(X0,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ~ ! [X27] :
( ~ r1(X0,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ( ( ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31)
| ~ ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
| ~ ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| p2(X36) )
| ~ p2(X35) ) ) )
& ( p2(X29)
| ~ ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
| ~ ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ~ ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44) )
| ~ p2(X43) ) ) )
| ~ ! [X45] :
( ~ r1(X40,X45)
| p2(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ~ ! [X48] :
( ~ r1(X40,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) ) )
| ~ ( ( ! [X50] :
( ~ r1(X39,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51)
| ~ ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
| ~ ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| p2(X56) )
| ~ p2(X55) ) ) )
& ( p2(X39)
| ~ ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) ) )
& ! [X59] :
( ~ r1(X0,X59)
| p2(X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| p2(X60)
| ~ ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p2(X62) )
| ~ p2(X61) ) ) ) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) )
& ( ! [X2] :
( ~ r1(X0,X2)
| p2(X2) )
| ~ ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p2(X5) )
| ~ p2(X4) ) ) ) )
| ! [X6] :
( ~ r1(X0,X6)
| p4(X6) )
| ~ ! [X7] :
( ~ r1(X0,X7)
| p4(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p4(X9) )
| ~ p4(X8) ) )
| ( ~ ! [X10] :
( ~ r1(X0,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p3(X11) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| p2(X12) )
| ~ ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) ) )
| ! [X16] :
( ~ r1(X0,X16)
| p1(X16) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) )
| ~ ( ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ~ ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23) )
| ~ p2(X22) ) ) )
| ~ ! [X24] :
( ~ r1(X0,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ~ ! [X27] :
( ~ r1(X0,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ( ( ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31)
| ~ ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
| ~ ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| p2(X36) )
| ~ p2(X35) ) ) )
& ( p2(X29)
| ~ ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
| ~ ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ~ ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44) )
| ~ p2(X43) ) ) )
| ~ ! [X45] :
( ~ r1(X40,X45)
| p2(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ~ ! [X48] :
( ~ r1(X40,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) ) )
| ~ ( ( ! [X50] :
( ~ r1(X39,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51)
| ~ ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
| ~ ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| p2(X56) )
| ~ p2(X55) ) ) )
& ( p2(X39)
| ~ ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) ) )
& ! [X59] :
( ~ r1(X0,X59)
| p2(X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| p2(X60)
| ~ ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p2(X62) )
| ~ p2(X61) ) ) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ( ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) )
| ( ? [X2] :
( r1(X0,X2)
& ~ p2(X2) )
& ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ~ p2(X5) )
& p2(X4) ) ) ) )
& ? [X6] :
( r1(X0,X6)
& ~ p4(X6) )
& ! [X7] :
( ~ r1(X0,X7)
| p4(X7)
| ? [X8] :
( r1(X7,X8)
& ? [X9] :
( r1(X8,X9)
& ~ p4(X9) )
& p4(X8) ) )
& ( ! [X10] :
( ~ r1(X0,X10)
| ? [X11] :
( r1(X10,X11)
& p3(X11) ) )
| ( ? [X12] :
( r1(X0,X12)
& ~ p2(X12) )
& ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ? [X14] :
( r1(X13,X14)
& ? [X15] :
( r1(X14,X15)
& ~ p2(X15) )
& p2(X14) ) ) ) )
& ? [X16] :
( r1(X0,X16)
& ~ p1(X16) )
& ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ? [X18] :
( r1(X17,X18)
& ? [X19] :
( r1(X18,X19)
& ~ p1(X19) )
& p1(X18) ) )
& ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ? [X22] :
( r1(X21,X22)
& ? [X23] :
( r1(X22,X23)
& ~ p2(X23) )
& p2(X22) ) ) )
| ? [X24] :
( r1(X0,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ? [X27] :
( r1(X0,X27)
& ? [X28] :
( r1(X27,X28)
& ~ p2(X28) )
& p2(X27) ) ) )
| ? [X29] :
( r1(X0,X29)
& ( ( ? [X30] :
( r1(X29,X30)
& ? [X31] :
( r1(X30,X31)
& ~ p2(X31)
& ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
& ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ? [X35] :
( r1(X34,X35)
& ? [X36] :
( r1(X35,X36)
& ~ p2(X36) )
& p2(X35) ) ) )
| ( ~ p2(X29)
& ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ? [X43] :
( r1(X42,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44) )
& p2(X43) ) ) )
| ? [X45] :
( r1(X40,X45)
& ~ p2(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ? [X48] :
( r1(X40,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) ) )
| ( ? [X50] :
( r1(X39,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51)
& ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
& ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ? [X55] :
( r1(X54,X55)
& ? [X56] :
( r1(X55,X56)
& ~ p2(X56) )
& p2(X55) ) ) )
| ( ~ p2(X39)
& ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) )
& ! [X59] :
( ~ r1(X0,X59)
| p2(X59)
| ? [X60] :
( r1(X59,X60)
& ~ p2(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p2(X62) )
| ~ p2(X61) ) ) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ( ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) )
| ( ? [X2] :
( r1(X0,X2)
& ~ p2(X2) )
& ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ~ p2(X5) )
& p2(X4) ) ) ) )
& ? [X6] :
( r1(X0,X6)
& ~ p4(X6) )
& ! [X7] :
( ~ r1(X0,X7)
| p4(X7)
| ? [X8] :
( r1(X7,X8)
& ? [X9] :
( r1(X8,X9)
& ~ p4(X9) )
& p4(X8) ) )
& ( ! [X10] :
( ~ r1(X0,X10)
| ? [X11] :
( r1(X10,X11)
& p3(X11) ) )
| ( ? [X12] :
( r1(X0,X12)
& ~ p2(X12) )
& ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ? [X14] :
( r1(X13,X14)
& ? [X15] :
( r1(X14,X15)
& ~ p2(X15) )
& p2(X14) ) ) ) )
& ? [X16] :
( r1(X0,X16)
& ~ p1(X16) )
& ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ? [X18] :
( r1(X17,X18)
& ? [X19] :
( r1(X18,X19)
& ~ p1(X19) )
& p1(X18) ) )
& ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ? [X22] :
( r1(X21,X22)
& ? [X23] :
( r1(X22,X23)
& ~ p2(X23) )
& p2(X22) ) ) )
| ? [X24] :
( r1(X0,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ? [X27] :
( r1(X0,X27)
& ? [X28] :
( r1(X27,X28)
& ~ p2(X28) )
& p2(X27) ) ) )
| ? [X29] :
( r1(X0,X29)
& ( ( ? [X30] :
( r1(X29,X30)
& ? [X31] :
( r1(X30,X31)
& ~ p2(X31)
& ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
& ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ? [X35] :
( r1(X34,X35)
& ? [X36] :
( r1(X35,X36)
& ~ p2(X36) )
& p2(X35) ) ) )
| ( ~ p2(X29)
& ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ? [X43] :
( r1(X42,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44) )
& p2(X43) ) ) )
| ? [X45] :
( r1(X40,X45)
& ~ p2(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ? [X48] :
( r1(X40,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) ) )
| ( ? [X50] :
( r1(X39,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51)
& ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
& ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ? [X55] :
( r1(X54,X55)
& ? [X56] :
( r1(X55,X56)
& ~ p2(X56) )
& p2(X55) ) ) )
| ( ~ p2(X39)
& ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) )
& ! [X59] :
( ~ r1(X0,X59)
| p2(X59)
| ? [X60] :
( r1(X59,X60)
& ~ p2(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p2(X62) )
| ~ p2(X61) ) ) ) ),
inference(flattening,[],[f6]) ).
fof(f8,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f22,plain,
! [X29,X32,X33] :
( ~ sP21(X29)
| p2(X33)
| ~ r1(X32,X33)
| ~ r1(sK28(X29),X32)
| ~ p2(X32) ),
inference(cnf_transformation,[],[f7]) ).
fof(f23,plain,
! [X40,X39] :
( ~ p2(sK37(X40))
| p2(X40)
| ~ r1(X39,X40)
| ~ sP18(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f24,plain,
! [X40,X39] :
( ~ sP18(X39)
| p2(X40)
| ~ r1(X39,X40)
| r1(sK32(X40),sK37(X40)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f25,plain,
! [X39,X54] :
( ~ p2(sK36(X54))
| p2(X54)
| ~ r1(X39,X54)
| ~ sP17(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f26,plain,
! [X39,X54] :
( ~ sP17(X39)
| p2(X54)
| ~ r1(X39,X54)
| r1(sK30(X54),sK36(X54)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f27,plain,
! [X21,X0,X20] :
( ~ p2(sK35(X21))
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| ~ sP12(X20,X0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f28,plain,
! [X21,X0,X20] :
( ~ sP12(X20,X0)
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| r1(sK29(X21),sK35(X21)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f29,plain,
! [X29,X34] :
( ~ p2(sK34(X34))
| p2(X34)
| ~ r1(X29,X34)
| ~ sP20(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f30,plain,
! [X29,X34] :
( ~ sP20(X29)
| p2(X34)
| ~ r1(X29,X34)
| r1(sK27(X34),sK34(X34)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f31,plain,
! [X40,X39] :
( ~ sP18(X39)
| p2(X40)
| ~ r1(X39,X40)
| p2(sK32(X40)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f32,plain,
! [X40,X39] :
( ~ sP18(X39)
| p2(X40)
| ~ r1(X39,X40)
| r1(X40,sK32(X40)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f35,plain,
! [X39,X54] :
( ~ sP17(X39)
| p2(X54)
| ~ r1(X39,X54)
| p2(sK30(X54)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f36,plain,
! [X39,X54] :
( ~ sP17(X39)
| p2(X54)
| ~ r1(X39,X54)
| r1(X54,sK30(X54)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f37,plain,
! [X21,X0,X20] :
( ~ sP12(X20,X0)
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| p2(sK29(X21)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f38,plain,
! [X21,X0,X20] :
( ~ sP12(X20,X0)
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| r1(X21,sK29(X21)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X29] :
( ~ p2(sK28(X29))
| ~ sP21(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f40,plain,
! [X29] :
( r1(sK23(X29),sK28(X29))
| ~ sP21(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f41,plain,
! [X29,X34] :
( ~ sP20(X29)
| p2(X34)
| ~ r1(X29,X34)
| p2(sK27(X34)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f42,plain,
! [X29,X34] :
( ~ sP20(X29)
| p2(X34)
| ~ r1(X29,X34)
| r1(X34,sK27(X34)) ),
inference(cnf_transformation,[],[f7]) ).
fof(f43,plain,
! [X38,X29,X37] :
( ~ p2(X37)
| p2(X38)
| ~ r1(X37,X38)
| ~ r1(X29,X37)
| ~ sP19(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f48,plain,
! [X58,X39,X57,X20] :
( ~ p2(X57)
| p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP17(X39)
| sP18(X39)
| ~ r1(sK3,X39)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f49,plain,
! [X58,X39,X57,X20] :
( ~ p2(X57)
| p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP17(X39)
| sP18(X39)
| ~ r1(sK3,X39)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f50,plain,
! [X58,X39,X57,X26,X25,X20] :
( ~ p2(X57)
| p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP17(X39)
| sP18(X39)
| ~ r1(sK3,X39)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f51,plain,
! [X39,X26,X25,X20] :
( ~ p2(X39)
| sP17(X39)
| sP18(X39)
| ~ r1(sK3,X39)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f52,plain,
! [X26,X25,X20] :
( r1(sK0,sK3)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f53,plain,
! [X26,X25,X20] :
( sP19(sK3)
| sP21(sK3)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f54,plain,
! [X26,X25,X20] :
( sP19(sK3)
| sP20(sK3)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f55,plain,
! [X26,X25,X20] :
( ~ p2(sK3)
| sP21(sK3)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f56,plain,
! [X26,X25,X20] :
( ~ p2(sK3)
| sP20(sK3)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f58,plain,
! [X3,X1] :
( ~ p2(sK25(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p3(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f59,plain,
! [X3,X1] :
( r1(sK16(X3),sK25(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p3(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f60,plain,
! [X10,X13] :
( ~ p2(sK24(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f61,plain,
! [X10,X13] :
( r1(sK14(X13),sK24(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f62,plain,
! [X10,X13] :
( ~ p2(sK24(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f63,plain,
! [X10,X13] :
( r1(sK14(X13),sK24(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f64,plain,
! [X29] :
( r1(X29,sK23(X29))
| ~ sP21(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f65,plain,
! [X59,X62,X61] :
( ~ p2(X61)
| p2(X62)
| ~ r1(X61,X62)
| ~ r1(sK4(X59),X61)
| p2(X59)
| ~ r1(sK0,X59) ),
inference(cnf_transformation,[],[f7]) ).
fof(f78,plain,
! [X3,X1] :
( p2(sK16(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p3(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f79,plain,
! [X3,X1] :
( r1(X3,sK16(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p3(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f82,plain,
! [X10,X13] :
( p2(sK14(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f83,plain,
! [X10,X13] :
( r1(X13,sK14(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f84,plain,
! [X10,X13] :
( p2(sK14(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f85,plain,
! [X10,X13] :
( r1(X13,sK14(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f90,plain,
! [X39,X20] :
( ~ p2(X39)
| sP17(X39)
| sP18(X39)
| ~ r1(sK3,X39)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f91,plain,
! [X39,X20] :
( ~ p2(X39)
| sP17(X39)
| sP18(X39)
| ~ r1(sK3,X39)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f92,plain,
! [X10] :
( r1(sK0,sK6)
| p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f93,plain,
! [X10] :
( r1(sK0,sK6)
| r1(X10,sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f94,plain,
! [X10] :
( ~ p2(sK6)
| p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f95,plain,
! [X10] :
( ~ p2(sK6)
| r1(X10,sK11(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f96,plain,
! [X20] :
( r1(sK0,sK3)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f97,plain,
! [X20] :
( r1(sK0,sK3)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f98,plain,
! [X20] :
( sP19(sK3)
| sP21(sK3)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f99,plain,
! [X20] :
( sP19(sK3)
| sP21(sK3)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f100,plain,
! [X20] :
( sP19(sK3)
| sP20(sK3)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f101,plain,
! [X20] :
( sP19(sK3)
| sP20(sK3)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f102,plain,
! [X20] :
( ~ p2(sK3)
| sP21(sK3)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f103,plain,
! [X20] :
( ~ p2(sK3)
| sP21(sK3)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f104,plain,
! [X20] :
( ~ p2(sK3)
| sP20(sK3)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f105,plain,
! [X20] :
( ~ p2(sK3)
| sP20(sK3)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f116,plain,
! [X1] :
( ~ p2(sK8)
| ~ p3(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f117,plain,
! [X1] :
( r1(sK0,sK8)
| ~ p3(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f122,plain,
! [X59] :
( ~ p2(sK4(X59))
| p2(X59)
| ~ r1(sK0,X59) ),
inference(cnf_transformation,[],[f7]) ).
fof(f123,plain,
! [X59] :
( r1(X59,sK4(X59))
| p2(X59)
| ~ r1(sK0,X59) ),
inference(cnf_transformation,[],[f7]) ).
fof(f131,plain,
! [X1] :
( r1(sK0,sK8)
| p3(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f132,plain,
! [X1] :
( ~ p2(sK8)
| p3(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f137,plain,
! [X20] :
( ~ sP19(sK3)
| sP20(sK3)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f138,plain,
! [X20] :
( ~ sP19(sK3)
| sP20(sK3)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f139,plain,
! [X20] :
( ~ sP19(sK3)
| sP21(sK3)
| r1(sK0,sK10)
| sP12(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f140,plain,
! [X20] :
( ~ sP19(sK3)
| sP21(sK3)
| ~ p2(sK10)
| sP12(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f141,plain,
! [X10] :
( ~ p2(sK6)
| ~ p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f142,plain,
! [X10] :
( r1(sK0,sK6)
| ~ p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f92]) ).
fof(f143,plain,
! [X10,X13] :
( r1(X13,sK14(X13))
| p2(X13)
| ~ r1(sK0,X13)
| ~ p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f144,plain,
! [X10,X13] :
( p2(sK14(X13))
| p2(X13)
| ~ r1(sK0,X13)
| ~ p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f84]) ).
fof(f147,plain,
! [X3,X1] :
( r1(X3,sK16(X3))
| p2(X3)
| ~ r1(sK0,X3)
| p3(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f148,plain,
! [X3,X1] :
( p2(sK16(X3))
| p2(X3)
| ~ r1(sK0,X3)
| p3(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f153,plain,
! [X10,X13] :
( r1(sK14(X13),sK24(X13))
| p2(X13)
| ~ r1(sK0,X13)
| ~ p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f154,plain,
! [X10,X13] :
( ~ p2(sK24(X13))
| p2(X13)
| ~ r1(sK0,X13)
| ~ p3(sK11(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f155,plain,
! [X3,X1] :
( r1(sK16(X3),sK25(X3))
| p2(X3)
| ~ r1(sK0,X3)
| p3(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f156,plain,
! [X3,X1] :
( ~ p2(sK25(X3))
| p2(X3)
| ~ r1(sK0,X3)
| p3(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f157,plain,
! [X26,X25,X20] :
( ~ sP19(sK3)
| sP20(sK3)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f158,plain,
! [X26,X25,X20] :
( ~ sP19(sK3)
| sP21(sK3)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK10,X25)
| sP12(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f159,plain,
! [X38,X29,X37] :
( ~ p2(X37)
| p2(X38)
| ~ r1(X37,X38)
| ~ r1(X29,X37)
| sP19(X29) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f169,definition,
( spl40_3
<=> ! [X57,X39,X58] :
( ~ p2(X57)
| ~ r1(sK3,X39)
| sP18(X39)
| sP17(X39)
| ~ r1(X39,X57)
| ~ r1(X57,X58)
| p2(X58) ) ),
introduced(definition,[new_symbols(definition,[spl40_3])],[avatar_definition]) ).
fof(f170,plain,
( ! [X58,X39,X57] :
( ~ p2(X57)
| ~ r1(sK3,X39)
| sP18(X39)
| sP17(X39)
| ~ r1(X39,X57)
| ~ r1(X57,X58)
| p2(X58) )
| ~ spl40_3 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f188,definition,
( spl40_7
<=> ! [X20] : sP12(X20,sK0) ),
introduced(definition,[new_symbols(definition,[spl40_7])],[avatar_definition]) ).
fof(f189,plain,
( ! [X20] : sP12(X20,sK0)
| ~ spl40_7 ),
inference(avatar_component_clause,[],[f188]) ).
fof(f191,definition,
( spl40_8
<=> r1(sK0,sK10) ),
introduced(definition,[new_symbols(definition,[spl40_8])],[avatar_definition]) ).
fof(f193,plain,
( r1(sK0,sK10)
| ~ spl40_8 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f194,plain,
( spl40_7
| spl40_8
| spl40_3 ),
inference(avatar_split_clause,[],[f48,f169,f191,f188]) ).
fof(f196,definition,
( spl40_9
<=> p2(sK10) ),
introduced(definition,[new_symbols(definition,[spl40_9])],[avatar_definition]) ).
fof(f198,plain,
( ~ p2(sK10)
| spl40_9 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f199,plain,
( spl40_7
| ~ spl40_9
| spl40_3 ),
inference(avatar_split_clause,[],[f49,f169,f196,f188]) ).
fof(f201,definition,
( spl40_10
<=> ! [X25,X26] :
( ~ p2(X25)
| ~ r1(sK10,X25)
| ~ r1(X25,X26)
| p2(X26) ) ),
introduced(definition,[new_symbols(definition,[spl40_10])],[avatar_definition]) ).
fof(f202,plain,
( ! [X26,X25] :
( ~ r1(sK10,X25)
| ~ p2(X25)
| ~ r1(X25,X26)
| p2(X26) )
| ~ spl40_10 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f203,plain,
( spl40_7
| spl40_10
| spl40_3 ),
inference(avatar_split_clause,[],[f50,f169,f201,f188]) ).
fof(f205,definition,
( spl40_11
<=> ! [X39] :
( ~ p2(X39)
| ~ r1(sK3,X39)
| sP18(X39)
| sP17(X39) ) ),
introduced(definition,[new_symbols(definition,[spl40_11])],[avatar_definition]) ).
fof(f206,plain,
( ! [X39] :
( ~ p2(X39)
| ~ r1(sK3,X39)
| sP18(X39)
| sP17(X39) )
| ~ spl40_11 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f207,plain,
( spl40_7
| spl40_10
| spl40_11 ),
inference(avatar_split_clause,[],[f51,f205,f201,f188]) ).
fof(f209,definition,
( spl40_12
<=> r1(sK0,sK3) ),
introduced(definition,[new_symbols(definition,[spl40_12])],[avatar_definition]) ).
fof(f211,plain,
( r1(sK0,sK3)
| ~ spl40_12 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f212,plain,
( spl40_7
| spl40_10
| spl40_12 ),
inference(avatar_split_clause,[],[f52,f209,f201,f188]) ).
fof(f214,definition,
( spl40_13
<=> sP21(sK3) ),
introduced(definition,[new_symbols(definition,[spl40_13])],[avatar_definition]) ).
fof(f216,plain,
( sP21(sK3)
| ~ spl40_13 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f218,definition,
( spl40_14
<=> sP19(sK3) ),
introduced(definition,[new_symbols(definition,[spl40_14])],[avatar_definition]) ).
fof(f220,plain,
( ~ sP19(sK3)
| spl40_14 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f221,plain,
( spl40_7
| spl40_10
| spl40_13
| ~ spl40_14 ),
inference(avatar_split_clause,[],[f158,f218,f214,f201,f188]) ).
fof(f223,definition,
( spl40_15
<=> sP20(sK3) ),
introduced(definition,[new_symbols(definition,[spl40_15])],[avatar_definition]) ).
fof(f225,plain,
( sP20(sK3)
| ~ spl40_15 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f226,plain,
( spl40_7
| spl40_10
| spl40_15
| ~ spl40_14 ),
inference(avatar_split_clause,[],[f157,f218,f223,f201,f188]) ).
fof(f228,definition,
( spl40_16
<=> p2(sK3) ),
introduced(definition,[new_symbols(definition,[spl40_16])],[avatar_definition]) ).
fof(f229,plain,
( p2(sK3)
| ~ spl40_16 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f230,plain,
( ~ p2(sK3)
| spl40_16 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f231,plain,
( spl40_7
| spl40_10
| spl40_13
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f55,f228,f214,f201,f188]) ).
fof(f232,plain,
( spl40_7
| spl40_10
| spl40_15
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f56,f228,f223,f201,f188]) ).
fof(f234,definition,
( spl40_17
<=> ! [X1] :
( p3(X1)
| ~ r1(sK0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl40_17])],[avatar_definition]) ).
fof(f235,plain,
( ! [X1] :
( ~ r1(sK0,X1)
| p3(X1) )
| ~ spl40_17 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f237,definition,
( spl40_18
<=> ! [X3] :
( ~ p2(sK25(X3))
| ~ r1(sK0,X3)
| p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl40_18])],[avatar_definition]) ).
fof(f238,plain,
( ! [X3] :
( ~ p2(sK25(X3))
| ~ r1(sK0,X3)
| p2(X3) )
| ~ spl40_18 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f239,plain,
( spl40_17
| spl40_18 ),
inference(avatar_split_clause,[],[f156,f237,f234]) ).
fof(f241,definition,
( spl40_19
<=> ! [X3] :
( r1(sK16(X3),sK25(X3))
| ~ r1(sK0,X3)
| p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl40_19])],[avatar_definition]) ).
fof(f242,plain,
( ! [X3] :
( r1(sK16(X3),sK25(X3))
| ~ r1(sK0,X3)
| p2(X3) )
| ~ spl40_19 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f243,plain,
( spl40_17
| spl40_19 ),
inference(avatar_split_clause,[],[f155,f241,f234]) ).
fof(f245,definition,
( spl40_20
<=> ! [X10] :
( ~ p3(sK11(X10))
| ~ r1(sK0,X10) ) ),
introduced(definition,[new_symbols(definition,[spl40_20])],[avatar_definition]) ).
fof(f246,plain,
( ! [X10] :
( ~ p3(sK11(X10))
| ~ r1(sK0,X10) )
| ~ spl40_20 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f248,definition,
( spl40_21
<=> ! [X13] :
( ~ p2(sK24(X13))
| ~ r1(sK0,X13)
| p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl40_21])],[avatar_definition]) ).
fof(f249,plain,
( ! [X13] :
( ~ p2(sK24(X13))
| ~ r1(sK0,X13)
| p2(X13) )
| ~ spl40_21 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f250,plain,
( spl40_20
| spl40_21 ),
inference(avatar_split_clause,[],[f154,f248,f245]) ).
fof(f252,definition,
( spl40_22
<=> ! [X13] :
( r1(sK14(X13),sK24(X13))
| ~ r1(sK0,X13)
| p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl40_22])],[avatar_definition]) ).
fof(f253,plain,
( ! [X13] :
( r1(sK14(X13),sK24(X13))
| ~ r1(sK0,X13)
| p2(X13) )
| ~ spl40_22 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( spl40_20
| spl40_22 ),
inference(avatar_split_clause,[],[f153,f252,f245]) ).
fof(f256,definition,
( spl40_23
<=> ! [X10] :
( r1(X10,sK11(X10))
| ~ r1(sK0,X10) ) ),
introduced(definition,[new_symbols(definition,[spl40_23])],[avatar_definition]) ).
fof(f257,plain,
( ! [X10] :
( r1(X10,sK11(X10))
| ~ r1(sK0,X10) )
| ~ spl40_23 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( spl40_23
| spl40_21 ),
inference(avatar_split_clause,[],[f62,f248,f256]) ).
fof(f259,plain,
( spl40_23
| spl40_22 ),
inference(avatar_split_clause,[],[f63,f252,f256]) ).
fof(f273,definition,
( spl40_24
<=> ! [X3] :
( p2(sK16(X3))
| ~ r1(sK0,X3)
| p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl40_24])],[avatar_definition]) ).
fof(f274,plain,
( ! [X3] :
( p2(sK16(X3))
| ~ r1(sK0,X3)
| p2(X3) )
| ~ spl40_24 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f275,plain,
( spl40_17
| spl40_24 ),
inference(avatar_split_clause,[],[f148,f273,f234]) ).
fof(f277,definition,
( spl40_25
<=> ! [X3] :
( r1(X3,sK16(X3))
| ~ r1(sK0,X3)
| p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl40_25])],[avatar_definition]) ).
fof(f278,plain,
( ! [X3] :
( ~ r1(sK0,X3)
| r1(X3,sK16(X3))
| p2(X3) )
| ~ spl40_25 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f279,plain,
( spl40_17
| spl40_25 ),
inference(avatar_split_clause,[],[f147,f277,f234]) ).
fof(f281,definition,
( spl40_26
<=> ! [X13] :
( p2(sK14(X13))
| ~ r1(sK0,X13)
| p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl40_26])],[avatar_definition]) ).
fof(f282,plain,
( ! [X13] :
( p2(sK14(X13))
| ~ r1(sK0,X13)
| p2(X13) )
| ~ spl40_26 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f283,plain,
( spl40_23
| spl40_26 ),
inference(avatar_split_clause,[],[f82,f281,f256]) ).
fof(f285,definition,
( spl40_27
<=> ! [X13] :
( r1(X13,sK14(X13))
| ~ r1(sK0,X13)
| p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl40_27])],[avatar_definition]) ).
fof(f286,plain,
( ! [X13] :
( r1(X13,sK14(X13))
| ~ r1(sK0,X13)
| p2(X13) )
| ~ spl40_27 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f287,plain,
( spl40_23
| spl40_27 ),
inference(avatar_split_clause,[],[f83,f285,f256]) ).
fof(f288,plain,
( spl40_20
| spl40_26 ),
inference(avatar_split_clause,[],[f144,f281,f245]) ).
fof(f289,plain,
( spl40_20
| spl40_27 ),
inference(avatar_split_clause,[],[f143,f285,f245]) ).
fof(f292,plain,
( spl40_7
| spl40_8
| spl40_11 ),
inference(avatar_split_clause,[],[f90,f205,f191,f188]) ).
fof(f293,plain,
( spl40_7
| ~ spl40_9
| spl40_11 ),
inference(avatar_split_clause,[],[f91,f205,f196,f188]) ).
fof(f295,definition,
( spl40_28
<=> r1(sK0,sK6) ),
introduced(definition,[new_symbols(definition,[spl40_28])],[avatar_definition]) ).
fof(f297,plain,
( r1(sK0,sK6)
| ~ spl40_28 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,plain,
( spl40_20
| spl40_28 ),
inference(avatar_split_clause,[],[f142,f295,f245]) ).
fof(f299,plain,
( spl40_23
| spl40_28 ),
inference(avatar_split_clause,[],[f93,f295,f256]) ).
fof(f301,definition,
( spl40_29
<=> p2(sK6) ),
introduced(definition,[new_symbols(definition,[spl40_29])],[avatar_definition]) ).
fof(f303,plain,
( ~ p2(sK6)
| spl40_29 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
( spl40_20
| ~ spl40_29 ),
inference(avatar_split_clause,[],[f141,f301,f245]) ).
fof(f305,plain,
( spl40_23
| ~ spl40_29 ),
inference(avatar_split_clause,[],[f95,f301,f256]) ).
fof(f306,plain,
( spl40_7
| ~ spl40_9
| spl40_12 ),
inference(avatar_split_clause,[],[f96,f209,f196,f188]) ).
fof(f307,plain,
( spl40_7
| spl40_8
| spl40_12 ),
inference(avatar_split_clause,[],[f97,f209,f191,f188]) ).
fof(f308,plain,
( spl40_7
| ~ spl40_9
| spl40_13
| ~ spl40_14 ),
inference(avatar_split_clause,[],[f140,f218,f214,f196,f188]) ).
fof(f309,plain,
( spl40_7
| spl40_8
| spl40_13
| ~ spl40_14 ),
inference(avatar_split_clause,[],[f139,f218,f214,f191,f188]) ).
fof(f310,plain,
( spl40_7
| ~ spl40_9
| spl40_15
| ~ spl40_14 ),
inference(avatar_split_clause,[],[f138,f218,f223,f196,f188]) ).
fof(f311,plain,
( spl40_7
| spl40_8
| spl40_15
| ~ spl40_14 ),
inference(avatar_split_clause,[],[f137,f218,f223,f191,f188]) ).
fof(f312,plain,
( spl40_7
| ~ spl40_9
| spl40_13
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f102,f228,f214,f196,f188]) ).
fof(f313,plain,
( spl40_7
| spl40_8
| spl40_13
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f103,f228,f214,f191,f188]) ).
fof(f314,plain,
( spl40_7
| ~ spl40_9
| spl40_15
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f104,f228,f223,f196,f188]) ).
fof(f315,plain,
( spl40_7
| spl40_8
| spl40_15
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f105,f228,f223,f191,f188]) ).
fof(f327,definition,
( spl40_30
<=> p2(sK8) ),
introduced(definition,[new_symbols(definition,[spl40_30])],[avatar_definition]) ).
fof(f329,plain,
( ~ p2(sK8)
| spl40_30 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f330,plain,
( spl40_17
| ~ spl40_30 ),
inference(avatar_split_clause,[],[f132,f327,f234]) ).
fof(f332,definition,
( spl40_31
<=> r1(sK0,sK8) ),
introduced(definition,[new_symbols(definition,[spl40_31])],[avatar_definition]) ).
fof(f334,plain,
( r1(sK0,sK8)
| ~ spl40_31 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f335,plain,
( spl40_17
| spl40_31 ),
inference(avatar_split_clause,[],[f131,f332,f234]) ).
fof(f359,plain,
( ~ r1(sK0,sK0)
| p3(sK11(sK0))
| ~ spl40_17
| ~ spl40_23 ),
inference(resolution,[],[f257,f235]) ).
fof(f360,plain,
( ~ r1(sK0,sK0)
| ~ spl40_17
| ~ spl40_20
| ~ spl40_23 ),
inference(forward_subsumption_resolution,[],[f359,f246]) ).
fof(f381,plain,
( ! [X0,X1] :
( ~ r1(sK0,X1)
| ~ r1(X1,X0)
| p2(X0)
| p2(sK29(X0)) )
| ~ spl40_7 ),
inference(resolution,[],[f37,f189]) ).
fof(f382,plain,
( ! [X0,X1] :
( ~ r1(sK0,X1)
| ~ r1(X1,X0)
| p2(X0)
| r1(X0,sK29(X0)) )
| ~ spl40_7 ),
inference(resolution,[],[f38,f189]) ).
fof(f383,plain,
( ! [X0,X1] :
( ~ r1(sK0,X1)
| ~ r1(X1,X0)
| p2(X0)
| r1(sK29(X0),sK35(X0)) )
| ~ spl40_7 ),
inference(resolution,[],[f28,f189]) ).
fof(f410,plain,
( $false
| ~ spl40_17
| ~ spl40_20
| ~ spl40_23 ),
inference(backward_subsumption_resolution,[],[f360,f8]) ).
fof(f413,plain,
( ~ spl40_17
| ~ spl40_20
| ~ spl40_23 ),
inference(avatar_contradiction_clause,[],[f410]) ).
fof(f450,plain,
( ! [X0] :
( p2(sK29(X0))
| p2(X0)
| ~ r1(sK6,X0) )
| ~ spl40_7
| ~ spl40_28 ),
inference(resolution,[],[f297,f381]) ).
fof(f455,plain,
( ! [X2,X0,X1] :
( ~ r1(X2,sK14(X0))
| p2(X0)
| p2(X1)
| ~ r1(sK14(X0),X1)
| ~ r1(sK0,X0)
| sP19(X2) )
| ~ spl40_26 ),
inference(resolution,[],[f282,f159]) ).
fof(f469,plain,
( ! [X0] :
( ~ r1(sK6,X0)
| p2(X0)
| r1(X0,sK29(X0)) )
| ~ spl40_7
| ~ spl40_28 ),
inference(resolution,[],[f382,f297]) ).
fof(f492,plain,
( ! [X0] :
( r1(sK29(X0),sK35(X0))
| p2(X0)
| ~ r1(sK6,X0) )
| ~ spl40_7
| ~ spl40_28 ),
inference(resolution,[],[f383,f297]) ).
fof(f529,plain,
( ! [X0,X1] :
( p2(X0)
| p2(X1)
| ~ r1(sK14(X0),X1)
| ~ r1(sK0,X0)
| sP19(X0)
| ~ r1(sK0,X0)
| p2(X0) )
| ~ spl40_26
| ~ spl40_27 ),
inference(resolution,[],[f455,f286]) ).
fof(f531,plain,
( ! [X0,X1] :
( ~ r1(sK14(X0),X1)
| p2(X1)
| p2(X0)
| ~ r1(sK0,X0)
| sP19(X0) )
| ~ spl40_26
| ~ spl40_27 ),
inference(duplicate_literal_removal,[],[f529]) ).
fof(f533,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(X2),sK29(X0))
| ~ r1(sK6,X0)
| p2(X1)
| ~ r1(sK29(X0),X1)
| p2(X0)
| p2(X2)
| ~ r1(sK0,X2) )
| ~ spl40_7
| ~ spl40_28 ),
inference(resolution,[],[f450,f65]) ).
fof(f781,plain,
( ! [X0] :
( p2(sK24(X0))
| p2(X0)
| ~ r1(sK0,X0)
| sP19(X0)
| ~ r1(sK0,X0)
| p2(X0) )
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(resolution,[],[f531,f253]) ).
fof(f790,plain,
( ! [X0] :
( p2(sK24(X0))
| p2(X0)
| ~ r1(sK0,X0)
| sP19(X0) )
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(duplicate_literal_removal,[],[f781]) ).
fof(f791,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| p2(X0)
| sP19(X0) )
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f790,f249]) ).
fof(f843,definition,
( spl40_103
<=> sP17(sK23(sK3)) ),
introduced(definition,[new_symbols(definition,[spl40_103])],[avatar_definition]) ).
fof(f844,plain,
( ~ sP17(sK23(sK3))
| spl40_103 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f845,plain,
( sP17(sK23(sK3))
| ~ spl40_103 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f847,definition,
( spl40_104
<=> sP18(sK23(sK3)) ),
introduced(definition,[new_symbols(definition,[spl40_104])],[avatar_definition]) ).
fof(f848,plain,
( ~ sP18(sK23(sK3))
| spl40_104 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f849,plain,
( sP18(sK23(sK3))
| ~ spl40_104 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f1031,plain,
( p2(sK3)
| sP19(sK3)
| ~ spl40_12
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(resolution,[],[f791,f211]) ).
fof(f1089,plain,
( p2(sK3)
| ~ spl40_12
| spl40_14
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f1031,f220]) ).
fof(f1103,plain,
( spl40_16
| ~ spl40_12
| spl40_14
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(avatar_split_clause,[],[f1089,f285,f281,f252,f248,f218,f209,f228]) ).
fof(f1212,plain,
( ! [X0,X1] :
( p2(X0)
| ~ r1(sK3,X0)
| ~ r1(X1,sK3)
| sP19(X1) )
| ~ spl40_16 ),
inference(resolution,[],[f229,f159]) ).
fof(f1214,definition,
( spl40_164
<=> ! [X1] :
( ~ r1(X1,sK3)
| sP19(X1) ) ),
introduced(definition,[new_symbols(definition,[spl40_164])],[avatar_definition]) ).
fof(f1215,plain,
( ! [X1] :
( ~ r1(X1,sK3)
| sP19(X1) )
| ~ spl40_164 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1217,definition,
( spl40_165
<=> ! [X0] :
( p2(X0)
| ~ r1(sK3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_165])],[avatar_definition]) ).
fof(f1218,plain,
( ! [X0] :
( ~ r1(sK3,X0)
| p2(X0) )
| ~ spl40_165 ),
inference(avatar_component_clause,[],[f1217]) ).
fof(f1219,plain,
( spl40_164
| spl40_165
| ~ spl40_16 ),
inference(avatar_split_clause,[],[f1212,f228,f1217,f1214]) ).
fof(f1416,plain,
( sP19(sK3)
| ~ spl40_164 ),
inference(resolution,[],[f1215,f8]) ).
fof(f1418,plain,
( $false
| spl40_14
| ~ spl40_164 ),
inference(forward_subsumption_resolution,[],[f1416,f220]) ).
fof(f1419,plain,
( spl40_14
| ~ spl40_164 ),
inference(avatar_contradiction_clause,[],[f1418]) ).
fof(f1430,plain,
( p2(sK23(sK3))
| ~ sP21(sK3)
| ~ spl40_165 ),
inference(resolution,[],[f1218,f64]) ).
fof(f1594,plain,
( p2(sK4(sK6))
| r1(sK4(sK6),sK29(sK4(sK6)))
| p2(sK6)
| ~ r1(sK0,sK6)
| ~ spl40_7
| ~ spl40_28 ),
inference(resolution,[],[f469,f123]) ).
fof(f1630,plain,
( r1(sK4(sK6),sK29(sK4(sK6)))
| p2(sK6)
| ~ r1(sK0,sK6)
| ~ spl40_7
| ~ spl40_28 ),
inference(forward_subsumption_resolution,[],[f1594,f122]) ).
fof(f1667,plain,
( r1(sK4(sK6),sK29(sK4(sK6)))
| ~ r1(sK0,sK6)
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(forward_subsumption_resolution,[],[f1630,f303]) ).
fof(f1668,plain,
( r1(sK4(sK6),sK29(sK4(sK6)))
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(forward_subsumption_resolution,[],[f1667,f297]) ).
fof(f2182,definition,
( spl40_313
<=> p2(sK4(sK6)) ),
introduced(definition,[new_symbols(definition,[spl40_313])],[avatar_definition]) ).
fof(f2183,plain,
( ~ p2(sK4(sK6))
| spl40_313 ),
inference(avatar_component_clause,[],[f2182]) ).
fof(f2184,plain,
( p2(sK4(sK6))
| ~ spl40_313 ),
inference(avatar_component_clause,[],[f2182]) ).
fof(f2186,definition,
( spl40_314
<=> ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK6)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_314])],[avatar_definition]) ).
fof(f2187,plain,
( ! [X0] :
( ~ r1(sK29(sK4(sK6)),X0)
| p2(X0) )
| ~ spl40_314 ),
inference(avatar_component_clause,[],[f2186]) ).
fof(f2189,definition,
( spl40_315
<=> r1(sK6,sK4(sK6)) ),
introduced(definition,[new_symbols(definition,[spl40_315])],[avatar_definition]) ).
fof(f2190,plain,
( r1(sK6,sK4(sK6))
| ~ spl40_315 ),
inference(avatar_component_clause,[],[f2189]) ).
fof(f2191,plain,
( ~ r1(sK6,sK4(sK6))
| spl40_315 ),
inference(avatar_component_clause,[],[f2189]) ).
fof(f2206,plain,
( p2(sK6)
| ~ r1(sK0,sK6)
| spl40_315 ),
inference(resolution,[],[f2191,f123]) ).
fof(f2207,plain,
( ~ r1(sK0,sK6)
| spl40_29
| spl40_315 ),
inference(forward_subsumption_resolution,[],[f2206,f303]) ).
fof(f2208,plain,
( $false
| ~ spl40_28
| spl40_29
| spl40_315 ),
inference(forward_subsumption_resolution,[],[f2207,f297]) ).
fof(f2209,plain,
( ~ spl40_28
| spl40_29
| spl40_315 ),
inference(avatar_contradiction_clause,[],[f2208]) ).
fof(f2210,plain,
( p2(sK6)
| ~ r1(sK0,sK6)
| ~ spl40_313 ),
inference(resolution,[],[f2184,f122]) ).
fof(f2249,plain,
( ! [X0] :
( ~ r1(sK6,sK4(sK6))
| p2(X0)
| ~ r1(sK29(sK4(sK6)),X0)
| p2(sK4(sK6))
| p2(sK6)
| ~ r1(sK0,sK6) )
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(resolution,[],[f533,f1668]) ).
fof(f2255,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK6)),X0)
| p2(sK4(sK6))
| p2(sK6)
| ~ r1(sK0,sK6) )
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(forward_subsumption_resolution,[],[f2249,f123]) ).
fof(f2257,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK6)),X0)
| p2(sK6)
| ~ r1(sK0,sK6) )
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(forward_subsumption_resolution,[],[f2255,f122]) ).
fof(f2259,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK6)),X0)
| ~ r1(sK0,sK6) )
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(forward_subsumption_resolution,[],[f2257,f303]) ).
fof(f2261,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK6)),X0) )
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(forward_subsumption_resolution,[],[f2259,f297]) ).
fof(f2262,plain,
( spl40_314
| ~ spl40_7
| ~ spl40_28
| spl40_29 ),
inference(avatar_split_clause,[],[f2261,f301,f295,f188,f2186]) ).
fof(f2416,plain,
( p2(sK35(sK4(sK6)))
| p2(sK4(sK6))
| ~ r1(sK6,sK4(sK6))
| ~ spl40_7
| ~ spl40_28
| ~ spl40_314 ),
inference(resolution,[],[f2187,f492]) ).
fof(f2487,definition,
( spl40_361
<=> p2(sK35(sK4(sK6))) ),
introduced(definition,[new_symbols(definition,[spl40_361])],[avatar_definition]) ).
fof(f2489,plain,
( p2(sK35(sK4(sK6)))
| ~ spl40_361 ),
inference(avatar_component_clause,[],[f2487]) ).
fof(f2662,plain,
( ! [X0,X1] :
( p2(sK4(sK6))
| ~ r1(X0,sK4(sK6))
| ~ r1(X1,X0)
| ~ sP12(X0,X1) )
| ~ spl40_361 ),
inference(resolution,[],[f2489,f27]) ).
fof(f2676,plain,
( ! [X0,X1] :
( ~ sP12(X0,X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK4(sK6)) )
| spl40_313
| ~ spl40_361 ),
inference(forward_subsumption_resolution,[],[f2662,f2183]) ).
fof(f3277,plain,
( ! [X0] :
( ~ r1(X0,sK4(sK6))
| ~ r1(sK0,X0) )
| ~ spl40_7
| spl40_313
| ~ spl40_361 ),
inference(resolution,[],[f2676,f189]) ).
fof(f3513,plain,
( ~ r1(sK0,sK6)
| p2(sK6)
| ~ r1(sK0,sK6)
| ~ spl40_7
| spl40_313
| ~ spl40_361 ),
inference(resolution,[],[f3277,f123]) ).
fof(f3516,plain,
( ~ r1(sK0,sK6)
| p2(sK6)
| ~ spl40_7
| spl40_313
| ~ spl40_361 ),
inference(duplicate_literal_removal,[],[f3513]) ).
fof(f3519,plain,
( p2(sK6)
| ~ spl40_7
| ~ spl40_28
| spl40_313
| ~ spl40_361 ),
inference(forward_subsumption_resolution,[],[f3516,f297]) ).
fof(f3520,plain,
( $false
| ~ spl40_7
| ~ spl40_28
| spl40_29
| spl40_313
| ~ spl40_361 ),
inference(forward_subsumption_resolution,[],[f3519,f303]) ).
fof(f3521,plain,
( ~ spl40_7
| ~ spl40_28
| spl40_29
| spl40_313
| ~ spl40_361 ),
inference(avatar_contradiction_clause,[],[f3520]) ).
fof(f3522,plain,
( p2(sK6)
| ~ spl40_28
| ~ spl40_313 ),
inference(forward_subsumption_resolution,[],[f2210,f297]) ).
fof(f3528,plain,
( p2(sK35(sK4(sK6)))
| p2(sK4(sK6))
| ~ spl40_7
| ~ spl40_28
| ~ spl40_314
| ~ spl40_315 ),
inference(forward_subsumption_resolution,[],[f2416,f2190]) ).
fof(f3550,plain,
( spl40_29
| ~ spl40_28
| ~ spl40_313 ),
inference(avatar_split_clause,[],[f3522,f2182,f295,f301]) ).
fof(f3551,plain,
( spl40_313
| spl40_361
| ~ spl40_7
| ~ spl40_28
| ~ spl40_314
| ~ spl40_315 ),
inference(avatar_split_clause,[],[f3528,f2189,f2186,f295,f188,f2487,f2182]) ).
fof(f3568,plain,
( ! [X0] :
( r1(sK29(X0),sK35(X0))
| p2(X0)
| ~ r1(sK8,X0) )
| ~ spl40_7
| ~ spl40_31 ),
inference(resolution,[],[f334,f383]) ).
fof(f3569,plain,
( ! [X0] :
( ~ r1(sK8,X0)
| p2(X0)
| r1(X0,sK29(X0)) )
| ~ spl40_7
| ~ spl40_31 ),
inference(resolution,[],[f334,f382]) ).
fof(f3570,plain,
( ! [X0] :
( p2(sK29(X0))
| p2(X0)
| ~ r1(sK8,X0) )
| ~ spl40_7
| ~ spl40_31 ),
inference(resolution,[],[f334,f381]) ).
fof(f3583,plain,
( ! [X2,X0,X1] :
( ~ r1(X2,sK16(X0))
| p2(X0)
| p2(X1)
| ~ r1(sK16(X0),X1)
| ~ r1(sK0,X0)
| sP19(X2) )
| ~ spl40_24 ),
inference(resolution,[],[f274,f159]) ).
fof(f3610,plain,
( ! [X2,X0,X1] :
( ~ r1(sK4(X2),sK29(X0))
| ~ r1(sK8,X0)
| p2(X1)
| ~ r1(sK29(X0),X1)
| p2(X0)
| p2(X2)
| ~ r1(sK0,X2) )
| ~ spl40_7
| ~ spl40_31 ),
inference(resolution,[],[f3570,f65]) ).
fof(f3615,plain,
( p2(sK4(sK8))
| r1(sK4(sK8),sK29(sK4(sK8)))
| p2(sK8)
| ~ r1(sK0,sK8)
| ~ spl40_7
| ~ spl40_31 ),
inference(resolution,[],[f3569,f123]) ).
fof(f3652,plain,
( r1(sK4(sK8),sK29(sK4(sK8)))
| p2(sK8)
| ~ r1(sK0,sK8)
| ~ spl40_7
| ~ spl40_31 ),
inference(forward_subsumption_resolution,[],[f3615,f122]) ).
fof(f3698,plain,
( r1(sK4(sK8),sK29(sK4(sK8)))
| ~ r1(sK0,sK8)
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(forward_subsumption_resolution,[],[f3652,f329]) ).
fof(f3699,plain,
( r1(sK4(sK8),sK29(sK4(sK8)))
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(forward_subsumption_resolution,[],[f3698,f334]) ).
fof(f3838,definition,
( spl40_574
<=> p2(sK4(sK8)) ),
introduced(definition,[new_symbols(definition,[spl40_574])],[avatar_definition]) ).
fof(f3840,plain,
( p2(sK4(sK8))
| ~ spl40_574 ),
inference(avatar_component_clause,[],[f3838]) ).
fof(f3842,definition,
( spl40_575
<=> ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK8)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_575])],[avatar_definition]) ).
fof(f3843,plain,
( ! [X0] :
( ~ r1(sK29(sK4(sK8)),X0)
| p2(X0) )
| ~ spl40_575 ),
inference(avatar_component_clause,[],[f3842]) ).
fof(f3885,plain,
( ! [X0] :
( ~ r1(sK8,sK4(sK8))
| p2(X0)
| ~ r1(sK29(sK4(sK8)),X0)
| p2(sK4(sK8))
| p2(sK8)
| ~ r1(sK0,sK8) )
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(resolution,[],[f3610,f3699]) ).
fof(f3888,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK8)),X0)
| p2(sK4(sK8))
| p2(sK8)
| ~ r1(sK0,sK8) )
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(forward_subsumption_resolution,[],[f3885,f123]) ).
fof(f3889,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK8)),X0)
| p2(sK8)
| ~ r1(sK0,sK8) )
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(forward_subsumption_resolution,[],[f3888,f122]) ).
fof(f3890,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK8)),X0)
| ~ r1(sK0,sK8) )
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(forward_subsumption_resolution,[],[f3889,f329]) ).
fof(f3891,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK4(sK8)),X0) )
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(forward_subsumption_resolution,[],[f3890,f334]) ).
fof(f3892,plain,
( spl40_575
| ~ spl40_7
| spl40_30
| ~ spl40_31 ),
inference(avatar_split_clause,[],[f3891,f332,f327,f188,f3842]) ).
fof(f4131,plain,
( p2(sK35(sK4(sK8)))
| p2(sK4(sK8))
| ~ r1(sK8,sK4(sK8))
| ~ spl40_7
| ~ spl40_31
| ~ spl40_575 ),
inference(resolution,[],[f3843,f3568]) ).
fof(f4197,definition,
( spl40_628
<=> p2(sK35(sK4(sK8))) ),
introduced(definition,[new_symbols(definition,[spl40_628])],[avatar_definition]) ).
fof(f4199,plain,
( p2(sK35(sK4(sK8)))
| ~ spl40_628 ),
inference(avatar_component_clause,[],[f4197]) ).
fof(f4207,definition,
( spl40_630
<=> r1(sK8,sK4(sK8)) ),
introduced(definition,[new_symbols(definition,[spl40_630])],[avatar_definition]) ).
fof(f4209,plain,
( ~ r1(sK8,sK4(sK8))
| spl40_630 ),
inference(avatar_component_clause,[],[f4207]) ).
fof(f4210,plain,
( ~ spl40_630
| spl40_574
| spl40_628
| ~ spl40_7
| ~ spl40_31
| ~ spl40_575 ),
inference(avatar_split_clause,[],[f4131,f3842,f332,f188,f4197,f3838,f4207]) ).
fof(f4248,plain,
( p2(sK8)
| ~ r1(sK0,sK8)
| spl40_630 ),
inference(resolution,[],[f4209,f123]) ).
fof(f4249,plain,
( ~ r1(sK0,sK8)
| spl40_30
| spl40_630 ),
inference(forward_subsumption_resolution,[],[f4248,f329]) ).
fof(f4250,plain,
( $false
| spl40_30
| ~ spl40_31
| spl40_630 ),
inference(forward_subsumption_resolution,[],[f4249,f334]) ).
fof(f4251,plain,
( spl40_30
| ~ spl40_31
| spl40_630 ),
inference(avatar_contradiction_clause,[],[f4250]) ).
fof(f4252,plain,
( ! [X0,X1] :
( p2(sK4(sK8))
| ~ r1(X0,sK4(sK8))
| ~ r1(X1,X0)
| ~ sP12(X0,X1) )
| ~ spl40_628 ),
inference(resolution,[],[f4199,f27]) ).
fof(f4267,definition,
( spl40_638
<=> ! [X0,X1] :
( ~ r1(X0,sK4(sK8))
| ~ sP12(X0,X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_638])],[avatar_definition]) ).
fof(f4268,plain,
( ! [X0,X1] :
( ~ sP12(X0,X1)
| ~ r1(X0,sK4(sK8))
| ~ r1(X1,X0) )
| ~ spl40_638 ),
inference(avatar_component_clause,[],[f4267]) ).
fof(f4269,plain,
( spl40_638
| spl40_574
| ~ spl40_628 ),
inference(avatar_split_clause,[],[f4252,f4197,f3838,f4267]) ).
fof(f4381,plain,
( ! [X0] :
( ~ r1(X0,sK4(sK8))
| ~ r1(sK0,X0) )
| ~ spl40_7
| ~ spl40_638 ),
inference(resolution,[],[f4268,f189]) ).
fof(f4456,plain,
( ~ r1(sK0,sK8)
| p2(sK8)
| ~ r1(sK0,sK8)
| ~ spl40_7
| ~ spl40_638 ),
inference(resolution,[],[f4381,f123]) ).
fof(f4459,plain,
( ~ r1(sK0,sK8)
| p2(sK8)
| ~ spl40_7
| ~ spl40_638 ),
inference(duplicate_literal_removal,[],[f4456]) ).
fof(f4462,plain,
( p2(sK8)
| ~ spl40_7
| ~ spl40_31
| ~ spl40_638 ),
inference(forward_subsumption_resolution,[],[f4459,f334]) ).
fof(f4463,plain,
( $false
| ~ spl40_7
| spl40_30
| ~ spl40_31
| ~ spl40_638 ),
inference(forward_subsumption_resolution,[],[f4462,f329]) ).
fof(f4464,plain,
( ~ spl40_7
| spl40_30
| ~ spl40_31
| ~ spl40_638 ),
inference(avatar_contradiction_clause,[],[f4463]) ).
fof(f4465,plain,
( p2(sK8)
| ~ r1(sK0,sK8)
| ~ spl40_574 ),
inference(resolution,[],[f3840,f122]) ).
fof(f4479,plain,
( ~ r1(sK0,sK8)
| spl40_30
| ~ spl40_574 ),
inference(forward_subsumption_resolution,[],[f4465,f329]) ).
fof(f4480,plain,
( $false
| spl40_30
| ~ spl40_31
| ~ spl40_574 ),
inference(forward_subsumption_resolution,[],[f4479,f334]) ).
fof(f4481,plain,
( spl40_30
| ~ spl40_31
| ~ spl40_574 ),
inference(avatar_contradiction_clause,[],[f4480]) ).
fof(f4518,plain,
( ! [X0] :
( ~ p2(sK14(sK10))
| ~ r1(sK14(sK10),X0)
| p2(X0)
| ~ r1(sK0,sK10)
| p2(sK10) )
| ~ spl40_10
| ~ spl40_27 ),
inference(resolution,[],[f202,f286]) ).
fof(f4545,plain,
( ! [X0] :
( ~ r1(sK14(sK10),X0)
| p2(X0)
| ~ r1(sK0,sK10)
| p2(sK10) )
| ~ spl40_10
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f4518,f282]) ).
fof(f4549,plain,
( ! [X0] :
( ~ r1(sK14(sK10),X0)
| p2(X0)
| p2(sK10) )
| ~ spl40_8
| ~ spl40_10
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f4545,f193]) ).
fof(f4582,plain,
( ! [X0] :
( ~ r1(sK14(sK10),X0)
| p2(X0) )
| ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f4549,f198]) ).
fof(f4583,plain,
( p2(sK24(sK10))
| ~ r1(sK0,sK10)
| p2(sK10)
| ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(resolution,[],[f4582,f253]) ).
fof(f4638,plain,
( ~ r1(sK0,sK10)
| p2(sK10)
| ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f4583,f249]) ).
fof(f4644,plain,
( p2(sK10)
| ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f4638,f193]) ).
fof(f4645,plain,
( $false
| ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(forward_subsumption_resolution,[],[f4644,f198]) ).
fof(f4646,plain,
( ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(avatar_contradiction_clause,[],[f4645]) ).
fof(f4652,plain,
( ! [X39] :
( ~ r1(sK3,X39)
| sP18(X39)
| sP17(X39) )
| ~ spl40_11
| ~ spl40_165 ),
inference(forward_subsumption_resolution,[],[f206,f1218]) ).
fof(f4665,definition,
( spl40_689
<=> p2(sK23(sK3)) ),
introduced(definition,[new_symbols(definition,[spl40_689])],[avatar_definition]) ).
fof(f4666,plain,
( ~ p2(sK23(sK3))
| spl40_689 ),
inference(avatar_component_clause,[],[f4665]) ).
fof(f4667,plain,
( p2(sK23(sK3))
| ~ spl40_689 ),
inference(avatar_component_clause,[],[f4665]) ).
fof(f4669,plain,
( ~ spl40_13
| spl40_689
| ~ spl40_165 ),
inference(avatar_split_clause,[],[f1430,f1217,f4665,f214]) ).
fof(f4692,plain,
( ! [X0,X1] :
( ~ r1(sK28(sK3),X1)
| ~ r1(X1,X0)
| p2(X0)
| ~ p2(X1) )
| ~ spl40_13 ),
inference(resolution,[],[f216,f22]) ).
fof(f4693,plain,
( ! [X0] :
( r1(sK27(X0),sK34(X0))
| ~ r1(sK3,X0)
| p2(X0) )
| ~ spl40_15 ),
inference(resolution,[],[f225,f30]) ).
fof(f4694,plain,
( ! [X0] :
( ~ r1(sK3,X0)
| p2(X0)
| r1(X0,sK27(X0)) )
| ~ spl40_15 ),
inference(resolution,[],[f225,f42]) ).
fof(f4695,plain,
( ! [X0] :
( p2(sK27(X0))
| ~ r1(sK3,X0)
| p2(X0) )
| ~ spl40_15 ),
inference(resolution,[],[f225,f41]) ).
fof(f4707,plain,
( sP18(sK23(sK3))
| sP17(sK23(sK3))
| ~ sP21(sK3)
| ~ spl40_11
| ~ spl40_165 ),
inference(resolution,[],[f4652,f64]) ).
fof(f4710,plain,
( sP18(sK23(sK3))
| sP17(sK23(sK3))
| ~ spl40_11
| ~ spl40_13
| ~ spl40_165 ),
inference(forward_subsumption_resolution,[],[f4707,f216]) ).
fof(f4714,plain,
( spl40_103
| spl40_104
| ~ spl40_11
| ~ spl40_13
| ~ spl40_165 ),
inference(avatar_split_clause,[],[f4710,f1217,f214,f205,f847,f843]) ).
fof(f4719,plain,
( ! [X0,X1] :
( p2(X0)
| ~ r1(sK23(sK3),X0)
| ~ r1(X1,sK23(sK3))
| sP19(X1) )
| ~ spl40_689 ),
inference(resolution,[],[f4667,f159]) ).
fof(f4721,definition,
( spl40_691
<=> ! [X1] :
( ~ r1(X1,sK23(sK3))
| sP19(X1) ) ),
introduced(definition,[new_symbols(definition,[spl40_691])],[avatar_definition]) ).
fof(f4722,plain,
( ! [X1] :
( ~ r1(X1,sK23(sK3))
| sP19(X1) )
| ~ spl40_691 ),
inference(avatar_component_clause,[],[f4721]) ).
fof(f4724,definition,
( spl40_692
<=> ! [X0] :
( p2(X0)
| ~ r1(sK23(sK3),X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_692])],[avatar_definition]) ).
fof(f4725,plain,
( ! [X0] :
( ~ r1(sK23(sK3),X0)
| p2(X0) )
| ~ spl40_692 ),
inference(avatar_component_clause,[],[f4724]) ).
fof(f4726,plain,
( spl40_691
| spl40_692
| ~ spl40_689 ),
inference(avatar_split_clause,[],[f4719,f4665,f4724,f4721]) ).
fof(f4801,definition,
( spl40_709
<=> p2(sK28(sK3)) ),
introduced(definition,[new_symbols(definition,[spl40_709])],[avatar_definition]) ).
fof(f4802,plain,
( p2(sK28(sK3))
| ~ spl40_709 ),
inference(avatar_component_clause,[],[f4801]) ).
fof(f4803,plain,
( ~ p2(sK28(sK3))
| spl40_709 ),
inference(avatar_component_clause,[],[f4801]) ).
fof(f4879,plain,
( ! [X0] :
( r1(sK30(X0),sK36(X0))
| ~ r1(sK23(sK3),X0)
| p2(X0) )
| ~ spl40_103 ),
inference(resolution,[],[f845,f26]) ).
fof(f4880,plain,
( ! [X0] :
( ~ r1(sK23(sK3),X0)
| p2(X0)
| r1(X0,sK30(X0)) )
| ~ spl40_103 ),
inference(resolution,[],[f845,f36]) ).
fof(f4881,plain,
( ! [X0] :
( ~ r1(sK23(sK3),X0)
| p2(X0)
| p2(sK30(X0)) )
| ~ spl40_103 ),
inference(resolution,[],[f845,f35]) ).
fof(f4914,plain,
( sP19(sK3)
| ~ sP21(sK3)
| ~ spl40_691 ),
inference(resolution,[],[f4722,f64]) ).
fof(f4919,plain,
( p2(sK28(sK3))
| ~ sP21(sK3)
| ~ spl40_692 ),
inference(resolution,[],[f4725,f40]) ).
fof(f4938,plain,
( ~ sP21(sK3)
| ~ spl40_692 ),
inference(forward_subsumption_resolution,[],[f4919,f39]) ).
fof(f4939,plain,
( $false
| ~ spl40_13
| ~ spl40_692 ),
inference(forward_subsumption_resolution,[],[f4938,f216]) ).
fof(f4940,plain,
( ~ spl40_13
| ~ spl40_692 ),
inference(avatar_contradiction_clause,[],[f4939]) ).
fof(f4941,plain,
( sP19(sK3)
| ~ spl40_13
| ~ spl40_691 ),
inference(forward_subsumption_resolution,[],[f4914,f216]) ).
fof(f4942,plain,
( spl40_14
| ~ spl40_13
| ~ spl40_691 ),
inference(avatar_split_clause,[],[f4941,f4721,f214,f218]) ).
fof(f4979,plain,
( p2(sK28(sK3))
| p2(sK30(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_103 ),
inference(resolution,[],[f4881,f40]) ).
fof(f4994,plain,
( p2(sK30(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_103 ),
inference(forward_subsumption_resolution,[],[f4979,f39]) ).
fof(f5004,plain,
( p2(sK30(sK28(sK3)))
| ~ spl40_13
| ~ spl40_103 ),
inference(forward_subsumption_resolution,[],[f4994,f216]) ).
fof(f5011,plain,
( ! [X0] :
( r1(sK32(X0),sK37(X0))
| ~ r1(sK23(sK3),X0)
| p2(X0) )
| ~ spl40_104 ),
inference(resolution,[],[f849,f24]) ).
fof(f5012,plain,
( ! [X0] :
( ~ r1(sK23(sK3),X0)
| p2(X0)
| p2(sK32(X0)) )
| ~ spl40_104 ),
inference(resolution,[],[f849,f31]) ).
fof(f5013,plain,
( ! [X0] :
( ~ r1(sK23(sK3),X0)
| p2(X0)
| r1(X0,sK32(X0)) )
| ~ spl40_104 ),
inference(resolution,[],[f849,f32]) ).
fof(f5014,plain,
( p2(sK28(sK3))
| p2(sK32(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_104 ),
inference(resolution,[],[f5012,f40]) ).
fof(f5028,plain,
( p2(sK32(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_104 ),
inference(forward_subsumption_resolution,[],[f5014,f39]) ).
fof(f5029,plain,
( p2(sK32(sK28(sK3)))
| ~ spl40_13
| ~ spl40_104 ),
inference(forward_subsumption_resolution,[],[f5028,f216]) ).
fof(f5047,plain,
( p2(sK28(sK3))
| r1(sK28(sK3),sK32(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_104 ),
inference(resolution,[],[f5013,f40]) ).
fof(f5056,plain,
( r1(sK28(sK3),sK32(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_104 ),
inference(forward_subsumption_resolution,[],[f5047,f39]) ).
fof(f5057,plain,
( r1(sK28(sK3),sK32(sK28(sK3)))
| ~ spl40_13
| ~ spl40_104 ),
inference(forward_subsumption_resolution,[],[f5056,f216]) ).
fof(f5166,definition,
( spl40_746
<=> ! [X0] :
( p2(X0)
| ~ r1(sK32(sK28(sK3)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_746])],[avatar_definition]) ).
fof(f5167,plain,
( ! [X0] :
( ~ r1(sK32(sK28(sK3)),X0)
| p2(X0) )
| ~ spl40_746 ),
inference(avatar_component_clause,[],[f5166]) ).
fof(f5341,plain,
( ! [X0] :
( ~ r1(sK32(sK28(sK3)),X0)
| p2(X0)
| ~ p2(sK32(sK28(sK3))) )
| ~ spl40_13
| ~ spl40_104 ),
inference(resolution,[],[f5057,f4692]) ).
fof(f5342,plain,
( ! [X0] :
( ~ r1(sK32(sK28(sK3)),X0)
| p2(X0) )
| ~ spl40_13
| ~ spl40_104 ),
inference(forward_subsumption_resolution,[],[f5341,f5029]) ).
fof(f5343,plain,
( spl40_746
| ~ spl40_13
| ~ spl40_104 ),
inference(avatar_split_clause,[],[f5342,f847,f214,f5166]) ).
fof(f5412,plain,
( p2(sK37(sK28(sK3)))
| ~ r1(sK23(sK3),sK28(sK3))
| p2(sK28(sK3))
| ~ spl40_104
| ~ spl40_746 ),
inference(resolution,[],[f5167,f5011]) ).
fof(f5466,plain,
( p2(sK37(sK28(sK3)))
| ~ r1(sK23(sK3),sK28(sK3))
| ~ spl40_104
| spl40_709
| ~ spl40_746 ),
inference(forward_subsumption_resolution,[],[f5412,f4803]) ).
fof(f5468,definition,
( spl40_784
<=> r1(sK23(sK3),sK28(sK3)) ),
introduced(definition,[new_symbols(definition,[spl40_784])],[avatar_definition]) ).
fof(f5469,plain,
( r1(sK23(sK3),sK28(sK3))
| ~ spl40_784 ),
inference(avatar_component_clause,[],[f5468]) ).
fof(f5470,plain,
( ~ r1(sK23(sK3),sK28(sK3))
| spl40_784 ),
inference(avatar_component_clause,[],[f5468]) ).
fof(f5472,definition,
( spl40_785
<=> p2(sK37(sK28(sK3))) ),
introduced(definition,[new_symbols(definition,[spl40_785])],[avatar_definition]) ).
fof(f5474,plain,
( p2(sK37(sK28(sK3)))
| ~ spl40_785 ),
inference(avatar_component_clause,[],[f5472]) ).
fof(f5475,plain,
( ~ spl40_784
| spl40_785
| ~ spl40_104
| spl40_709
| ~ spl40_746 ),
inference(avatar_split_clause,[],[f5466,f5166,f4801,f847,f5472,f5468]) ).
fof(f5574,plain,
( ~ sP21(sK3)
| spl40_784 ),
inference(resolution,[],[f5470,f40]) ).
fof(f5575,plain,
( $false
| ~ spl40_13
| spl40_784 ),
inference(forward_subsumption_resolution,[],[f5574,f216]) ).
fof(f5576,plain,
( ~ spl40_13
| spl40_784 ),
inference(avatar_contradiction_clause,[],[f5575]) ).
fof(f5577,plain,
( ! [X0] :
( p2(sK28(sK3))
| ~ r1(X0,sK28(sK3))
| ~ sP18(X0) )
| ~ spl40_785 ),
inference(resolution,[],[f5474,f23]) ).
fof(f5591,plain,
( ! [X0] :
( ~ sP18(X0)
| ~ r1(X0,sK28(sK3)) )
| spl40_709
| ~ spl40_785 ),
inference(forward_subsumption_resolution,[],[f5577,f4803]) ).
fof(f5614,plain,
( ~ r1(sK23(sK3),sK28(sK3))
| ~ spl40_104
| spl40_709
| ~ spl40_785 ),
inference(resolution,[],[f5591,f849]) ).
fof(f5615,plain,
( $false
| ~ spl40_104
| spl40_709
| ~ spl40_784
| ~ spl40_785 ),
inference(forward_subsumption_resolution,[],[f5614,f5469]) ).
fof(f5616,plain,
( ~ spl40_104
| spl40_709
| ~ spl40_784
| ~ spl40_785 ),
inference(avatar_contradiction_clause,[],[f5615]) ).
fof(f5653,plain,
( p2(sK28(sK3))
| r1(sK28(sK3),sK30(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_103 ),
inference(resolution,[],[f4880,f40]) ).
fof(f5664,plain,
( r1(sK28(sK3),sK30(sK28(sK3)))
| ~ sP21(sK3)
| ~ spl40_103 ),
inference(forward_subsumption_resolution,[],[f5653,f39]) ).
fof(f5671,plain,
( r1(sK28(sK3),sK30(sK28(sK3)))
| ~ spl40_13
| ~ spl40_103 ),
inference(forward_subsumption_resolution,[],[f5664,f216]) ).
fof(f5772,definition,
( spl40_815
<=> ! [X0] :
( p2(X0)
| ~ r1(sK30(sK28(sK3)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_815])],[avatar_definition]) ).
fof(f5773,plain,
( ! [X0] :
( ~ r1(sK30(sK28(sK3)),X0)
| p2(X0) )
| ~ spl40_815 ),
inference(avatar_component_clause,[],[f5772]) ).
fof(f5779,plain,
( ! [X0] :
( ~ r1(sK30(sK28(sK3)),X0)
| p2(X0)
| ~ p2(sK30(sK28(sK3))) )
| ~ spl40_13
| ~ spl40_103 ),
inference(resolution,[],[f5671,f4692]) ).
fof(f5780,plain,
( ! [X0] :
( ~ r1(sK30(sK28(sK3)),X0)
| p2(X0) )
| ~ spl40_13
| ~ spl40_103 ),
inference(forward_subsumption_resolution,[],[f5779,f5004]) ).
fof(f5781,plain,
( spl40_815
| ~ spl40_13
| ~ spl40_103 ),
inference(avatar_split_clause,[],[f5780,f843,f214,f5772]) ).
fof(f5845,plain,
( p2(sK36(sK28(sK3)))
| ~ r1(sK23(sK3),sK28(sK3))
| p2(sK28(sK3))
| ~ spl40_103
| ~ spl40_815 ),
inference(resolution,[],[f5773,f4879]) ).
fof(f5899,plain,
( p2(sK36(sK28(sK3)))
| p2(sK28(sK3))
| ~ spl40_103
| ~ spl40_784
| ~ spl40_815 ),
inference(forward_subsumption_resolution,[],[f5845,f5469]) ).
fof(f5900,plain,
( p2(sK36(sK28(sK3)))
| ~ spl40_103
| spl40_709
| ~ spl40_784
| ~ spl40_815 ),
inference(forward_subsumption_resolution,[],[f5899,f4803]) ).
fof(f5901,plain,
( ! [X0] :
( p2(sK28(sK3))
| ~ r1(X0,sK28(sK3))
| ~ sP17(X0) )
| ~ spl40_103
| spl40_709
| ~ spl40_784
| ~ spl40_815 ),
inference(resolution,[],[f5900,f25]) ).
fof(f5915,plain,
( ! [X0] :
( ~ sP17(X0)
| ~ r1(X0,sK28(sK3)) )
| ~ spl40_103
| spl40_709
| ~ spl40_784
| ~ spl40_815 ),
inference(forward_subsumption_resolution,[],[f5901,f4803]) ).
fof(f5916,plain,
( ~ r1(sK23(sK3),sK28(sK3))
| ~ spl40_103
| spl40_709
| ~ spl40_784
| ~ spl40_815 ),
inference(resolution,[],[f5915,f845]) ).
fof(f5917,plain,
( $false
| ~ spl40_103
| spl40_709
| ~ spl40_784
| ~ spl40_815 ),
inference(forward_subsumption_resolution,[],[f5916,f5469]) ).
fof(f5918,plain,
( ~ spl40_103
| spl40_709
| ~ spl40_784
| ~ spl40_815 ),
inference(avatar_contradiction_clause,[],[f5917]) ).
fof(f5962,plain,
( ~ r1(sK3,sK23(sK3))
| sP18(sK23(sK3))
| sP17(sK23(sK3))
| ~ spl40_11
| ~ spl40_689 ),
inference(resolution,[],[f206,f4667]) ).
fof(f6058,plain,
( ~ r1(sK3,sK23(sK3))
| sP17(sK23(sK3))
| ~ spl40_11
| spl40_104
| ~ spl40_689 ),
inference(forward_subsumption_resolution,[],[f5962,f848]) ).
fof(f6158,definition,
( spl40_880
<=> r1(sK3,sK23(sK3)) ),
introduced(definition,[new_symbols(definition,[spl40_880])],[avatar_definition]) ).
fof(f6159,plain,
( r1(sK3,sK23(sK3))
| ~ spl40_880 ),
inference(avatar_component_clause,[],[f6158]) ).
fof(f6160,plain,
( ~ r1(sK3,sK23(sK3))
| spl40_880 ),
inference(avatar_component_clause,[],[f6158]) ).
fof(f6161,plain,
( spl40_103
| ~ spl40_880
| ~ spl40_11
| spl40_104
| ~ spl40_689 ),
inference(avatar_split_clause,[],[f6058,f4665,f847,f205,f6158,f843]) ).
fof(f6546,plain,
( ! [X2,X0,X1] :
( ~ r1(X1,sK27(X0))
| p2(X0)
| ~ r1(sK3,X1)
| sP18(X1)
| sP17(X1)
| ~ r1(sK3,X0)
| ~ r1(sK27(X0),X2)
| p2(X2) )
| ~ spl40_3
| ~ spl40_15 ),
inference(resolution,[],[f4695,f170]) ).
fof(f6557,plain,
( p2(sK23(sK3))
| r1(sK23(sK3),sK27(sK23(sK3)))
| ~ sP21(sK3)
| ~ spl40_15 ),
inference(resolution,[],[f4694,f64]) ).
fof(f6559,plain,
( r1(sK23(sK3),sK27(sK23(sK3)))
| ~ sP21(sK3)
| ~ spl40_15
| spl40_689 ),
inference(forward_subsumption_resolution,[],[f6557,f4666]) ).
fof(f6570,plain,
( r1(sK23(sK3),sK27(sK23(sK3)))
| ~ spl40_13
| ~ spl40_15
| spl40_689 ),
inference(forward_subsumption_resolution,[],[f6559,f216]) ).
fof(f6630,plain,
( ~ sP21(sK3)
| spl40_880 ),
inference(resolution,[],[f6160,f64]) ).
fof(f6631,plain,
( $false
| ~ spl40_13
| spl40_880 ),
inference(forward_subsumption_resolution,[],[f6630,f216]) ).
fof(f6632,plain,
( ~ spl40_13
| spl40_880 ),
inference(avatar_contradiction_clause,[],[f6631]) ).
fof(f6646,plain,
( ! [X0] :
( p2(sK23(sK3))
| ~ r1(sK3,sK23(sK3))
| sP18(sK23(sK3))
| sP17(sK23(sK3))
| ~ r1(sK3,sK23(sK3))
| ~ r1(sK27(sK23(sK3)),X0)
| p2(X0) )
| ~ spl40_3
| ~ spl40_13
| ~ spl40_15
| spl40_689 ),
inference(resolution,[],[f6546,f6570]) ).
fof(f6647,plain,
( ! [X0] :
( p2(sK23(sK3))
| ~ r1(sK3,sK23(sK3))
| sP18(sK23(sK3))
| sP17(sK23(sK3))
| ~ r1(sK27(sK23(sK3)),X0)
| p2(X0) )
| ~ spl40_3
| ~ spl40_13
| ~ spl40_15
| spl40_689 ),
inference(duplicate_literal_removal,[],[f6646]) ).
fof(f6648,plain,
( ! [X0] :
( ~ r1(sK3,sK23(sK3))
| sP18(sK23(sK3))
| sP17(sK23(sK3))
| ~ r1(sK27(sK23(sK3)),X0)
| p2(X0) )
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_689 ),
inference(forward_subsumption_resolution,[],[f6647,f206]) ).
fof(f6649,plain,
( ! [X0] :
( sP18(sK23(sK3))
| sP17(sK23(sK3))
| ~ r1(sK27(sK23(sK3)),X0)
| p2(X0) )
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_689
| ~ spl40_880 ),
inference(forward_subsumption_resolution,[],[f6648,f6159]) ).
fof(f6650,plain,
( ! [X0] :
( sP17(sK23(sK3))
| ~ r1(sK27(sK23(sK3)),X0)
| p2(X0) )
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(forward_subsumption_resolution,[],[f6649,f848]) ).
fof(f6651,plain,
( ! [X0] :
( ~ r1(sK27(sK23(sK3)),X0)
| p2(X0) )
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(forward_subsumption_resolution,[],[f6650,f844]) ).
fof(f6701,plain,
( p2(sK34(sK23(sK3)))
| ~ r1(sK3,sK23(sK3))
| p2(sK23(sK3))
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(resolution,[],[f6651,f4693]) ).
fof(f6756,plain,
( p2(sK34(sK23(sK3)))
| p2(sK23(sK3))
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(forward_subsumption_resolution,[],[f6701,f6159]) ).
fof(f6762,plain,
( p2(sK34(sK23(sK3)))
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(forward_subsumption_resolution,[],[f6756,f4666]) ).
fof(f6788,plain,
( ! [X0] :
( p2(sK23(sK3))
| ~ r1(X0,sK23(sK3))
| ~ sP20(X0) )
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(resolution,[],[f6762,f29]) ).
fof(f6821,plain,
( ! [X0] :
( ~ sP20(X0)
| ~ r1(X0,sK23(sK3)) )
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(forward_subsumption_resolution,[],[f6788,f4666]) ).
fof(f6968,plain,
( ~ r1(sK3,sK23(sK3))
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(resolution,[],[f6821,f225]) ).
fof(f6969,plain,
( $false
| ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(forward_subsumption_resolution,[],[f6968,f6159]) ).
fof(f6970,plain,
( ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(avatar_contradiction_clause,[],[f6969]) ).
fof(f7036,plain,
( r1(sK3,sK16(sK3))
| p2(sK3)
| ~ spl40_12
| ~ spl40_25 ),
inference(resolution,[],[f278,f211]) ).
fof(f7039,plain,
( r1(sK10,sK16(sK10))
| p2(sK10)
| ~ spl40_8
| ~ spl40_25 ),
inference(resolution,[],[f278,f193]) ).
fof(f7048,plain,
( r1(sK10,sK16(sK10))
| ~ spl40_8
| spl40_9
| ~ spl40_25 ),
inference(forward_subsumption_resolution,[],[f7039,f198]) ).
fof(f7093,plain,
( ! [X0] :
( ~ p2(sK16(sK10))
| ~ r1(sK16(sK10),X0)
| p2(X0) )
| ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_25 ),
inference(resolution,[],[f7048,f202]) ).
fof(f7099,definition,
( spl40_1025
<=> ! [X0] :
( ~ r1(sK16(sK10),X0)
| p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl40_1025])],[avatar_definition]) ).
fof(f7100,plain,
( ! [X0] :
( ~ r1(sK16(sK10),X0)
| p2(X0) )
| ~ spl40_1025 ),
inference(avatar_component_clause,[],[f7099]) ).
fof(f7102,definition,
( spl40_1026
<=> p2(sK16(sK10)) ),
introduced(definition,[new_symbols(definition,[spl40_1026])],[avatar_definition]) ).
fof(f7104,plain,
( ~ p2(sK16(sK10))
| spl40_1026 ),
inference(avatar_component_clause,[],[f7102]) ).
fof(f7105,plain,
( spl40_1025
| ~ spl40_1026
| ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_25 ),
inference(avatar_split_clause,[],[f7093,f277,f201,f196,f191,f7102,f7099]) ).
fof(f7108,plain,
( ~ r1(sK0,sK10)
| p2(sK10)
| ~ spl40_24
| spl40_1026 ),
inference(resolution,[],[f7104,f274]) ).
fof(f7109,plain,
( p2(sK10)
| ~ spl40_8
| ~ spl40_24
| spl40_1026 ),
inference(forward_subsumption_resolution,[],[f7108,f193]) ).
fof(f7110,plain,
( $false
| ~ spl40_8
| spl40_9
| ~ spl40_24
| spl40_1026 ),
inference(forward_subsumption_resolution,[],[f7109,f198]) ).
fof(f7111,plain,
( ~ spl40_8
| spl40_9
| ~ spl40_24
| spl40_1026 ),
inference(avatar_contradiction_clause,[],[f7110]) ).
fof(f7151,plain,
( p2(sK25(sK10))
| ~ r1(sK0,sK10)
| p2(sK10)
| ~ spl40_19
| ~ spl40_1025 ),
inference(resolution,[],[f7100,f242]) ).
fof(f7200,plain,
( ~ r1(sK0,sK10)
| p2(sK10)
| ~ spl40_18
| ~ spl40_19
| ~ spl40_1025 ),
inference(forward_subsumption_resolution,[],[f7151,f238]) ).
fof(f7201,plain,
( p2(sK10)
| ~ spl40_8
| ~ spl40_18
| ~ spl40_19
| ~ spl40_1025 ),
inference(forward_subsumption_resolution,[],[f7200,f193]) ).
fof(f7202,plain,
( $false
| ~ spl40_8
| spl40_9
| ~ spl40_18
| ~ spl40_19
| ~ spl40_1025 ),
inference(forward_subsumption_resolution,[],[f7201,f198]) ).
fof(f7203,plain,
( ~ spl40_8
| spl40_9
| ~ spl40_18
| ~ spl40_19
| ~ spl40_1025 ),
inference(avatar_contradiction_clause,[],[f7202]) ).
fof(f7416,plain,
( ~ sP21(sK3)
| ~ spl40_709 ),
inference(resolution,[],[f4802,f39]) ).
fof(f7434,plain,
( $false
| ~ spl40_13
| ~ spl40_709 ),
inference(forward_subsumption_resolution,[],[f7416,f216]) ).
fof(f7435,plain,
( ~ spl40_13
| ~ spl40_709 ),
inference(avatar_contradiction_clause,[],[f7434]) ).
fof(f7470,definition,
( spl40_1058
<=> r1(sK3,sK16(sK3)) ),
introduced(definition,[new_symbols(definition,[spl40_1058])],[avatar_definition]) ).
fof(f7472,plain,
( r1(sK3,sK16(sK3))
| ~ spl40_1058 ),
inference(avatar_component_clause,[],[f7470]) ).
fof(f7474,plain,
( spl40_16
| spl40_1058
| ~ spl40_12
| ~ spl40_25 ),
inference(avatar_split_clause,[],[f7036,f277,f209,f7470,f228]) ).
fof(f7627,plain,
( ! [X0] :
( p2(sK3)
| p2(X0)
| ~ r1(sK16(sK3),X0)
| ~ r1(sK0,sK3)
| sP19(sK3) )
| ~ spl40_24
| ~ spl40_1058 ),
inference(resolution,[],[f7472,f3583]) ).
fof(f7628,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK16(sK3),X0)
| ~ r1(sK0,sK3)
| sP19(sK3) )
| spl40_16
| ~ spl40_24
| ~ spl40_1058 ),
inference(forward_subsumption_resolution,[],[f7627,f230]) ).
fof(f7655,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK16(sK3),X0)
| sP19(sK3) )
| ~ spl40_12
| spl40_16
| ~ spl40_24
| ~ spl40_1058 ),
inference(forward_subsumption_resolution,[],[f7628,f211]) ).
fof(f7657,plain,
( ! [X0] :
( ~ r1(sK16(sK3),X0)
| p2(X0) )
| ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_24
| ~ spl40_1058 ),
inference(forward_subsumption_resolution,[],[f7655,f220]) ).
fof(f7691,plain,
( p2(sK25(sK3))
| ~ r1(sK0,sK3)
| p2(sK3)
| ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_19
| ~ spl40_24
| ~ spl40_1058 ),
inference(resolution,[],[f7657,f242]) ).
fof(f7744,plain,
( ~ r1(sK0,sK3)
| p2(sK3)
| ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_18
| ~ spl40_19
| ~ spl40_24
| ~ spl40_1058 ),
inference(forward_subsumption_resolution,[],[f7691,f238]) ).
fof(f7746,plain,
( p2(sK3)
| ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_18
| ~ spl40_19
| ~ spl40_24
| ~ spl40_1058 ),
inference(forward_subsumption_resolution,[],[f7744,f211]) ).
fof(f7747,plain,
( $false
| ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_18
| ~ spl40_19
| ~ spl40_24
| ~ spl40_1058 ),
inference(forward_subsumption_resolution,[],[f7746,f230]) ).
fof(f7748,plain,
( ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_18
| ~ spl40_19
| ~ spl40_24
| ~ spl40_1058 ),
inference(avatar_contradiction_clause,[],[f7747]) ).
cnf(s5,plain,
( spl40_3
| spl40_7
| spl40_8 ),
inference(sat_conversion,[],[f194]) ).
cnf(s6,plain,
( spl40_3
| spl40_7
| ~ spl40_9 ),
inference(sat_conversion,[],[f199]) ).
cnf(s7,plain,
( spl40_3
| spl40_7
| spl40_10 ),
inference(sat_conversion,[],[f203]) ).
cnf(s8,plain,
( spl40_7
| spl40_10
| spl40_11 ),
inference(sat_conversion,[],[f207]) ).
cnf(s9,plain,
( spl40_7
| spl40_10
| spl40_12 ),
inference(sat_conversion,[],[f212]) ).
cnf(s10,plain,
( spl40_7
| spl40_10
| spl40_13
| ~ spl40_14 ),
inference(sat_conversion,[],[f221]) ).
cnf(s11,plain,
( spl40_7
| spl40_10
| ~ spl40_14
| spl40_15 ),
inference(sat_conversion,[],[f226]) ).
cnf(s12,plain,
( spl40_7
| spl40_10
| spl40_13
| ~ spl40_16 ),
inference(sat_conversion,[],[f231]) ).
cnf(s13,plain,
( spl40_7
| spl40_10
| spl40_15
| ~ spl40_16 ),
inference(sat_conversion,[],[f232]) ).
cnf(s14,plain,
( spl40_17
| spl40_18 ),
inference(sat_conversion,[],[f239]) ).
cnf(s15,plain,
( spl40_17
| spl40_19 ),
inference(sat_conversion,[],[f243]) ).
cnf(s16,plain,
( spl40_20
| spl40_21 ),
inference(sat_conversion,[],[f250]) ).
cnf(s17,plain,
( spl40_20
| spl40_22 ),
inference(sat_conversion,[],[f254]) ).
cnf(s18,plain,
( spl40_21
| spl40_23 ),
inference(sat_conversion,[],[f258]) ).
cnf(s19,plain,
( spl40_22
| spl40_23 ),
inference(sat_conversion,[],[f259]) ).
cnf(s32,plain,
( spl40_17
| spl40_24 ),
inference(sat_conversion,[],[f275]) ).
cnf(s33,plain,
( spl40_17
| spl40_25 ),
inference(sat_conversion,[],[f279]) ).
cnf(s34,plain,
( spl40_23
| spl40_26 ),
inference(sat_conversion,[],[f283]) ).
cnf(s35,plain,
( spl40_23
| spl40_27 ),
inference(sat_conversion,[],[f287]) ).
cnf(s36,plain,
( spl40_20
| spl40_26 ),
inference(sat_conversion,[],[f288]) ).
cnf(s37,plain,
( spl40_20
| spl40_27 ),
inference(sat_conversion,[],[f289]) ).
cnf(s40,plain,
( spl40_7
| spl40_8
| spl40_11 ),
inference(sat_conversion,[],[f292]) ).
cnf(s41,plain,
( spl40_7
| ~ spl40_9
| spl40_11 ),
inference(sat_conversion,[],[f293]) ).
cnf(s42,plain,
( spl40_20
| spl40_28 ),
inference(sat_conversion,[],[f298]) ).
cnf(s43,plain,
( spl40_23
| spl40_28 ),
inference(sat_conversion,[],[f299]) ).
cnf(s44,plain,
( spl40_20
| ~ spl40_29 ),
inference(sat_conversion,[],[f304]) ).
cnf(s45,plain,
( spl40_23
| ~ spl40_29 ),
inference(sat_conversion,[],[f305]) ).
cnf(s46,plain,
( spl40_7
| ~ spl40_9
| spl40_12 ),
inference(sat_conversion,[],[f306]) ).
cnf(s47,plain,
( spl40_7
| spl40_8
| spl40_12 ),
inference(sat_conversion,[],[f307]) ).
cnf(s48,plain,
( spl40_7
| ~ spl40_9
| spl40_13
| ~ spl40_14 ),
inference(sat_conversion,[],[f308]) ).
cnf(s49,plain,
( spl40_7
| spl40_8
| spl40_13
| ~ spl40_14 ),
inference(sat_conversion,[],[f309]) ).
cnf(s50,plain,
( spl40_7
| ~ spl40_9
| ~ spl40_14
| spl40_15 ),
inference(sat_conversion,[],[f310]) ).
cnf(s51,plain,
( spl40_7
| spl40_8
| ~ spl40_14
| spl40_15 ),
inference(sat_conversion,[],[f311]) ).
cnf(s52,plain,
( spl40_7
| ~ spl40_9
| spl40_13
| ~ spl40_16 ),
inference(sat_conversion,[],[f312]) ).
cnf(s53,plain,
( spl40_7
| spl40_8
| spl40_13
| ~ spl40_16 ),
inference(sat_conversion,[],[f313]) ).
cnf(s54,plain,
( spl40_7
| ~ spl40_9
| spl40_15
| ~ spl40_16 ),
inference(sat_conversion,[],[f314]) ).
cnf(s55,plain,
( spl40_7
| spl40_8
| spl40_15
| ~ spl40_16 ),
inference(sat_conversion,[],[f315]) ).
cnf(s66,plain,
( spl40_17
| ~ spl40_30 ),
inference(sat_conversion,[],[f330]) ).
cnf(s67,plain,
( spl40_17
| spl40_31 ),
inference(sat_conversion,[],[f335]) ).
cnf(s72,plain,
( ~ spl40_17
| ~ spl40_20
| ~ spl40_23 ),
inference(sat_conversion,[],[f413]) ).
cnf(s134,plain,
( ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(sat_conversion,[],[f1103]) ).
cnf(s156,plain,
( ~ spl40_16
| spl40_164
| spl40_165 ),
inference(sat_conversion,[],[f1219]) ).
cnf(s179,plain,
( spl40_14
| ~ spl40_164 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s263,plain,
( ~ spl40_28
| spl40_29
| spl40_315 ),
inference(sat_conversion,[],[f2209]) ).
cnf(s270,plain,
( ~ spl40_7
| ~ spl40_28
| spl40_29
| spl40_314 ),
inference(sat_conversion,[],[f2262]) ).
cnf(s416,plain,
( ~ spl40_7
| ~ spl40_28
| spl40_29
| spl40_313
| ~ spl40_361 ),
inference(sat_conversion,[],[f3521]) ).
cnf(s425,plain,
( ~ spl40_28
| spl40_29
| ~ spl40_313 ),
inference(sat_conversion,[],[f3550]) ).
cnf(s426,plain,
( ~ spl40_7
| ~ spl40_28
| spl40_313
| ~ spl40_314
| ~ spl40_315
| spl40_361 ),
inference(sat_conversion,[],[f3551]) ).
cnf(s459,plain,
( ~ spl40_7
| spl40_30
| ~ spl40_31
| spl40_575 ),
inference(sat_conversion,[],[f3892]) ).
cnf(s499,plain,
( ~ spl40_7
| ~ spl40_31
| spl40_574
| ~ spl40_575
| spl40_628
| ~ spl40_630 ),
inference(sat_conversion,[],[f4210]) ).
cnf(s508,plain,
( spl40_30
| ~ spl40_31
| spl40_630 ),
inference(sat_conversion,[],[f4251]) ).
cnf(s511,plain,
( spl40_574
| ~ spl40_628
| spl40_638 ),
inference(sat_conversion,[],[f4269]) ).
cnf(s539,plain,
( ~ spl40_7
| spl40_30
| ~ spl40_31
| ~ spl40_638 ),
inference(sat_conversion,[],[f4464]) ).
cnf(s542,plain,
( spl40_30
| ~ spl40_31
| ~ spl40_574 ),
inference(sat_conversion,[],[f4481]) ).
cnf(s560,plain,
( ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_21
| ~ spl40_22
| ~ spl40_26
| ~ spl40_27 ),
inference(sat_conversion,[],[f4646]) ).
cnf(s569,plain,
( ~ spl40_13
| ~ spl40_165
| spl40_689 ),
inference(sat_conversion,[],[f4669]) ).
cnf(s583,plain,
( ~ spl40_11
| ~ spl40_13
| spl40_103
| spl40_104
| ~ spl40_165 ),
inference(sat_conversion,[],[f4714]) ).
cnf(s586,plain,
( ~ spl40_689
| spl40_691
| spl40_692 ),
inference(sat_conversion,[],[f4726]) ).
cnf(s618,plain,
( ~ spl40_13
| ~ spl40_692 ),
inference(sat_conversion,[],[f4940]) ).
cnf(s619,plain,
( ~ spl40_13
| spl40_14
| ~ spl40_691 ),
inference(sat_conversion,[],[f4942]) ).
cnf(s668,plain,
( ~ spl40_13
| ~ spl40_104
| spl40_746 ),
inference(sat_conversion,[],[f5343]) ).
cnf(s679,plain,
( ~ spl40_104
| spl40_709
| ~ spl40_746
| ~ spl40_784
| spl40_785 ),
inference(sat_conversion,[],[f5475]) ).
cnf(s680,plain,
( ~ spl40_13
| spl40_784 ),
inference(sat_conversion,[],[f5576]) ).
cnf(s683,plain,
( ~ spl40_104
| spl40_709
| ~ spl40_784
| ~ spl40_785 ),
inference(sat_conversion,[],[f5616]) ).
cnf(s701,plain,
( ~ spl40_13
| ~ spl40_103
| spl40_815 ),
inference(sat_conversion,[],[f5781]) ).
cnf(s715,plain,
( ~ spl40_103
| spl40_709
| ~ spl40_784
| ~ spl40_815 ),
inference(sat_conversion,[],[f5918]) ).
cnf(s735,plain,
( ~ spl40_11
| spl40_103
| spl40_104
| ~ spl40_689
| ~ spl40_880 ),
inference(sat_conversion,[],[f6161]) ).
cnf(s794,plain,
( ~ spl40_13
| spl40_880 ),
inference(sat_conversion,[],[f6632]) ).
cnf(s825,plain,
( ~ spl40_3
| ~ spl40_11
| ~ spl40_13
| ~ spl40_15
| spl40_103
| spl40_104
| spl40_689
| ~ spl40_880 ),
inference(sat_conversion,[],[f6970]) ).
cnf(s846,plain,
( ~ spl40_8
| spl40_9
| ~ spl40_10
| ~ spl40_25
| spl40_1025
| ~ spl40_1026 ),
inference(sat_conversion,[],[f7105]) ).
cnf(s848,plain,
( ~ spl40_8
| spl40_9
| ~ spl40_24
| spl40_1026 ),
inference(sat_conversion,[],[f7111]) ).
cnf(s859,plain,
( ~ spl40_8
| spl40_9
| ~ spl40_18
| ~ spl40_19
| ~ spl40_1025 ),
inference(sat_conversion,[],[f7203]) ).
cnf(s904,plain,
( ~ spl40_13
| ~ spl40_709 ),
inference(sat_conversion,[],[f7435]) ).
cnf(s912,plain,
( ~ spl40_12
| spl40_16
| ~ spl40_25
| spl40_1058 ),
inference(sat_conversion,[],[f7474]) ).
cnf(s954,plain,
( ~ spl40_12
| spl40_14
| spl40_16
| ~ spl40_18
| ~ spl40_19
| ~ spl40_24
| ~ spl40_1058 ),
inference(sat_conversion,[],[f7748]) ).
cnf(s955,plain,
( spl40_17
| ~ spl40_8
| spl40_9
| ~ spl40_10 ),
inference(rat,[],[s846,s859,s848,s14,s15,s32,s33]) ).
cnf(s956,plain,
( spl40_20
| ~ spl40_8
| spl40_9
| ~ spl40_10 ),
inference(rat,[],[s560,s16,s17,s36,s37]) ).
cnf(s957,plain,
( ~ spl40_8
| ~ spl40_10
| spl40_9 ),
inference(rat,[],[s560,s18,s19,s34,s35,s72,s956,s955]) ).
cnf(s958,plain,
( spl40_7
| spl40_3 ),
inference(rat,[],[s957,s5,s6,s7]) ).
cnf(s959,plain,
( spl40_20
| ~ spl40_7 ),
inference(rat,[],[s426,s416,s263,s270,s425,s42,s44]) ).
cnf(s960,plain,
( spl40_23
| ~ spl40_7 ),
inference(rat,[],[s426,s416,s263,s270,s425,s43,s45]) ).
cnf(s961,plain,
~ spl40_7,
inference(rat,[],[s499,s511,s459,s508,s539,s542,s66,s67,s72,s960,s959]) ).
cnf(s962,plain,
spl40_3,
inference(rat,[],[s958,s961]) ).
cnf(s963,plain,
( spl40_13
| spl40_10
| spl40_20 ),
inference(rat,[],[s134,s10,s12,s37,s36,s17,s16,s9,s961]) ).
cnf(s964,plain,
( spl40_14
| spl40_10
| spl40_20 ),
inference(rat,[],[s569,s156,s586,s134,s179,s619,s37,s36,s17,s16,s9,s618,s963,s961]) ).
cnf(s965,plain,
( ~ spl40_104
| ~ spl40_13 ),
inference(rat,[],[s668,s679,s683,s904,s680]) ).
cnf(s966,plain,
( ~ spl40_103
| ~ spl40_13 ),
inference(rat,[],[s701,s715,s904,s680]) ).
cnf(s967,plain,
( spl40_103
| ~ spl40_880
| ~ spl40_11
| ~ spl40_13
| spl40_104
| ~ spl40_15 ),
inference(rat,[],[s735,s825,s962]) ).
cnf(s968,plain,
( spl40_10
| spl40_20 ),
inference(rat,[],[s967,s966,s965,s11,s964,s794,s963,s8,s961]) ).
cnf(s969,plain,
( spl40_15
| ~ spl40_9
| spl40_20 ),
inference(rat,[],[s134,s50,s54,s37,s36,s17,s16,s46,s961]) ).
cnf(s970,plain,
( ~ spl40_13
| ~ spl40_15
| ~ spl40_11 ),
inference(rat,[],[s967,s966,s965,s794]) ).
cnf(s971,plain,
( ~ spl40_9
| spl40_20 ),
inference(rat,[],[s134,s52,s48,s970,s969,s41,s46,s37,s36,s17,s16,s961]) ).
cnf(s972,plain,
( spl40_15
| spl40_20 ),
inference(rat,[],[s134,s51,s55,s37,s36,s17,s16,s47,s957,s971,s968,s961]) ).
cnf(s973,plain,
spl40_20,
inference(rat,[],[s134,s49,s53,s970,s972,s40,s47,s957,s971,s968,s16,s17,s36,s37,s961]) ).
cnf(s974,plain,
( spl40_17
| spl40_14
| spl40_16
| ~ spl40_12 ),
inference(rat,[],[s954,s912,s14,s15,s32,s33]) ).
cnf(s975,plain,
( spl40_14
| spl40_16
| ~ spl40_12 ),
inference(rat,[],[s134,s18,s19,s34,s35,s72,s974,s973]) ).
cnf(s976,plain,
( spl40_15
| spl40_10 ),
inference(rat,[],[s975,s11,s13,s9,s961]) ).
cnf(s977,plain,
spl40_10,
inference(rat,[],[s975,s10,s12,s970,s976,s8,s9,s961]) ).
cnf(s978,plain,
( spl40_15
| ~ spl40_14 ),
inference(rat,[],[s957,s50,s51,s961,s977]) ).
cnf(s979,plain,
spl40_11,
inference(rat,[],[s957,s40,s41,s977,s961]) ).
cnf(s980,plain,
( spl40_13
| ~ spl40_14 ),
inference(rat,[],[s957,s49,s48,s961,s977]) ).
cnf(s981,plain,
~ spl40_14,
inference(rat,[],[s980,s970,s978,s979]) ).
cnf(s982,plain,
~ spl40_164,
inference(rat,[],[s179,s981]) ).
cnf(s983,plain,
spl40_12,
inference(rat,[],[s957,s47,s46,s977,s961]) ).
cnf(s984,plain,
spl40_16,
inference(rat,[],[s975,s981,s983]) ).
cnf(s985,plain,
spl40_165,
inference(rat,[],[s156,s982,s984]) ).
cnf(s986,plain,
~ spl40_13,
inference(rat,[],[s583,s966,s965,s979,s985]) ).
cnf(s987,plain,
~ spl40_9,
inference(rat,[],[s52,s984,s961,s986]) ).
cnf(s988,plain,
spl40_8,
inference(rat,[],[s53,s984,s961,s986]) ).
cnf(s990,plain,
$false,
inference(rat,[],[s957,s977,s988,s987]) ).
fof(f7749,plain,
$false,
inference(avatar_sat_refutation,[],[s990]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL660+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 % Computer : n003.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 16:23:56 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.15/0.45 Running first-order model finding
% 0.15/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.06/0.68 % (761347)Will run a generic schedule for satisfiability detection.
% 1.06/0.68 % (761352)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=138118795_2999 on theBenchmark for (2999ds/0Mi)
% 1.06/0.68 % TRYING [1]
% 1.06/0.68 % TRYING [2]
% 1.06/0.68 % (761353)% WARNING: option uhcvi not known.
% 1.06/0.68 % TRYING [3]
% 1.06/0.68 % (761358)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=959316856:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.06/0.68 % (761354)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3505301420:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.06/0.68 % (761355)dis+10_1_sil=32000:sp=arity:random_seed=1685514364:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.06/0.68 % TRYING [4]
% 1.06/0.68 % (761356)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3332407092:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.06/0.68 % (761353)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3361061344:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.06/0.68 % (761357)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2404369516:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.06/0.68 % TRYING [5]
% 1.06/0.68 % (761355)Instruction limit reached!
% 1.06/0.68 % (761355)------------------------------
% 1.06/0.68 % (761355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.68 % (761355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.68 % (761355)CaDiCaL version: 2.1.3
% 1.06/0.68 % (761355)Termination reason: Instruction limit
% 1.06/0.68 % (761355)Termination phase: Saturation
% 1.06/0.68 % (761355)Time elapsed: 0.059 s
% 1.06/0.68 % (761355)Peak memory usage: 13 MB
% 1.06/0.68 % (761355)Instructions burned: 104 (million)
% 1.06/0.68 % (761356)Instruction limit reached!
% 1.06/0.68 % (761356)------------------------------
% 1.06/0.68 % (761356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.68 % (761356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.68 % (761356)CaDiCaL version: 2.1.3
% 1.06/0.68 % (761356)Termination reason: Instruction limit
% 1.06/0.68 % (761356)Termination phase: Saturation
% 1.06/0.68 % (761356)Time elapsed: 0.062 s
% 1.06/0.68 % (761356)Peak memory usage: 12 MB
% 1.06/0.68 % (761356)Instructions burned: 118 (million)
% 1.06/0.68 % (761366)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1678816822:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.06/0.68 % (761357)Instruction limit reached!
% 1.06/0.68 % (761357)------------------------------
% 1.06/0.68 % (761357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.68 % (761357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.68 % (761357)CaDiCaL version: 2.1.3
% 1.06/0.68 % (761357)Termination reason: Instruction limit
% 1.06/0.68 % (761357)Termination phase: Saturation
% 1.06/0.68 % (761357)Time elapsed: 0.081 s
% 1.06/0.68 % (761357)Peak memory usage: 14 MB
% 1.06/0.68 % (761357)Instructions burned: 132 (million)
% 1.06/0.68 % (761367)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2487596138:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.06/0.68 % TRYING [1]
% 1.06/0.68 % TRYING [2]
% 1.06/0.68 % TRYING [3]
% 1.06/0.68 % (761358)Instruction limit reached!
% 1.06/0.68 % (761358)------------------------------
% 1.06/0.68 % (761358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.68 % (761358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.68 % (761358)CaDiCaL version: 2.1.3
% 1.06/0.68 % (761358)Termination reason: Instruction limit
% 1.06/0.68 % (761358)Termination phase: Saturation
% 1.06/0.68 % (761358)Time elapsed: 0.087 s
% 1.06/0.68 % (761358)Peak memory usage: 17 MB
% 1.06/0.68 % (761358)Instructions burned: 160 (million)
% 1.06/0.68 % TRYING [4]
% 1.06/0.68 % (761370)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4283179905:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.06/0.68 % (761371)ott-21_1_sil=16000:fs=off:random_seed=491524435:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.06/0.68 % TRYING [6]
% 1.06/0.68 % TRYING [5]
% 1.06/0.68 % (761367)Instruction limit reached!
% 1.06/0.68 % (761367)------------------------------
% 1.06/0.68 % (761367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.68 % (761367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.68 % (761367)CaDiCaL version: 2.1.3
% 1.06/0.68 % (761367)Termination reason: Instruction limit
% 1.06/0.68 % (761367)Termination phase: Saturation
% 1.06/0.68 % (761367)Time elapsed: 0.079 s
% 1.06/0.68 % (761367)Peak memory usage: 14 MB
% 1.06/0.68 % (761367)Instructions burned: 131 (million)
% 1.06/0.68 % (761353) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-761347-761353"...
% 1.06/0.68 % (761374)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3091772634:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.06/0.68 % (761353)...printing done.
% 1.06/0.68 % (761353)Refutation found. Thanks to Tanya!
% 1.06/0.68 % SZS status Theorem for theBenchmark
% 1.06/0.68 % SZS output start Proof for theBenchmark
% See solution above
% 1.06/0.69 % (761353)------------------------------
% 1.06/0.69 % (761353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.69 % (761353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.69 % (761353)CaDiCaL version: 2.1.3
% 1.06/0.69 % (761353)Termination reason: Refutation
% 1.06/0.69 % (761353)Time elapsed: 0.184 s
% 1.06/0.69 % (761353)Peak memory usage: 17 MB
% 1.06/0.69 % (761353)Instructions burned: 255 (million)
% 1.06/0.69 % (761347)Success in time 0.224 s
% 1.06/0.69 % Vampire exiting
%------------------------------------------------------------------------------