%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL642+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 : n010.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:08 AM UTC 2026
% Result : Theorem 0.37s 0.48s
% Output : Refutation 0.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 35
% Syntax : Number of formulae : 310 ( 16 unt; 34 def)
% Number of atoms : 1982 ( 0 equ)
% Maximal formula atoms : 107 ( 6 avg)
% Number of connectives : 2879 (1207 ~;1316 |; 328 &)
% ( 28 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 39 ( 38 usr; 29 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 5 con; 0-1 aty)
% Number of variables : 646 ( 0 sgn 508 !; 138 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ 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(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ 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)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p3(X4) )
| ~ p3(X3) ) )
| ! [X5] :
( ~ r1(X0,X5)
| p2(X5) )
| ~ ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| p2(X8) )
| ~ p2(X7) ) )
| ! [X9] :
( ~ r1(X0,X9)
| p1(X9) )
| ~ ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) )
| ~ p1(X11) ) )
| ~ ( ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p2(X16) )
| ~ p2(X15) ) ) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p2(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ~ ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21) )
| ~ p2(X20) ) ) )
| ~ ! [X22] :
( ~ r1(X0,X22)
| ( ( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
| ~ ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| p2(X29) )
| ~ p2(X28) ) ) )
& ( p2(X22)
| ~ ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
| ~ ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ~ ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p2(X37) )
| ~ p2(X36) ) ) )
| ~ ! [X38] :
( ~ r1(X33,X38)
| p2(X38)
| ~ ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ~ ! [X41] :
( ~ r1(X33,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42) )
| ~ p2(X41) ) ) ) )
| ~ ( ( ! [X43] :
( ~ r1(X32,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X32)
| ~ ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| p2(X52)
| ~ ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p3(X4) )
| ~ p3(X3) ) )
| ! [X5] :
( ~ r1(X0,X5)
| p2(X5) )
| ~ ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| p2(X8) )
| ~ p2(X7) ) )
| ! [X9] :
( ~ r1(X0,X9)
| p1(X9) )
| ~ ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) )
| ~ p1(X11) ) )
| ~ ( ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p2(X16) )
| ~ p2(X15) ) ) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p2(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ~ ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21) )
| ~ p2(X20) ) ) )
| ~ ! [X22] :
( ~ r1(X0,X22)
| ( ( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
| ~ ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| p2(X29) )
| ~ p2(X28) ) ) )
& ( p2(X22)
| ~ ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
| ~ ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ~ ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p2(X37) )
| ~ p2(X36) ) ) )
| ~ ! [X38] :
( ~ r1(X33,X38)
| p2(X38)
| ~ ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ~ ! [X41] :
( ~ r1(X33,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42) )
| ~ p2(X41) ) ) ) )
| ~ ( ( ! [X43] :
( ~ r1(X32,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X32)
| ~ ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| p2(X52)
| ~ ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) ) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ? [X22] :
( r1(X0,X22)
& ( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ( ~ p2(X22)
& ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
& ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ? [X36] :
( r1(X35,X36)
& ? [X37] :
( r1(X36,X37)
& ~ p2(X37) )
& p2(X36) ) ) )
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ( ~ p2(X32)
& ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| p2(X52)
| ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ? [X22] :
( r1(X0,X22)
& ( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ( ~ p2(X22)
& ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
& ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ? [X36] :
( r1(X35,X36)
& ? [X37] :
( r1(X36,X37)
& ~ p2(X37) )
& p2(X36) ) ) )
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ( ~ p2(X32)
& ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| p2(X52)
| ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,definition,
! [X33] :
( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ? [X36] :
( r1(X35,X36)
& ? [X37] :
( r1(X36,X37)
& ~ p2(X37) )
& p2(X36) ) ) )
| ~ sP0(X33) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X32] :
( ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ~ sP1(X32) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X32] :
( ! [X33] :
( ~ r1(X32,X33)
| ( ( sP0(X33)
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ~ sP2(X32) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X22] :
( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ~ sP3(X22) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X0] :
( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ~ sP4(X0) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X0] :
( ( ( sP4(X0)
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ~ sP5(X0) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f13,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( sP5(X0)
| ? [X22] :
( r1(X0,X22)
& ( sP3(X22)
| ( ~ p2(X22)
& ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
& ! [X32] :
( ~ r1(X22,X32)
| sP2(X32)
| sP1(X32)
| ( ~ p2(X32)
& ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| p2(X52)
| ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) ) ),
inference(definition_folding,[],[f6,f12,f11,f10,f9,f8,f7]) ).
fof(f14,plain,
! [X0] :
( ( ( sP4(X0)
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ~ sP5(X0) ),
inference(nnf_transformation,[],[f12]) ).
fof(f15,plain,
! [X0] :
( ( ( sP4(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p2(X3) )
| ~ p2(X2) ) ) )
& ( p2(X0)
| ? [X4] :
( r1(X0,X4)
& ? [X5] :
( r1(X4,X5)
& ~ p2(X5) )
& p2(X4) ) ) )
| ~ sP5(X0) ),
inference(rectify,[],[f14]) ).
fof(f16,plain,
! [X0] :
( ( ( sP4(X0)
| ( r1(X0,sK6(X0))
& ~ p2(sK6(X0))
& ! [X2] :
( ~ r1(sK6(X0),X2)
| ! [X3] :
( ~ r1(X2,X3)
| p2(X3) )
| ~ p2(X2) ) ) )
& ( p2(X0)
| ( r1(X0,sK7(X0))
& r1(sK7(X0),sK8(X0))
& ~ p2(sK8(X0))
& p2(sK7(X0)) ) ) )
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X1,sK6(X0)),skolemize(X4,sK7(X0)),skolemize(X5,sK8(X0))],[f15]) ).
fof(f17,plain,
! [X0] :
( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ~ sP4(X0) ),
inference(nnf_transformation,[],[f11]) ).
fof(f18,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p2(X4) )
& p2(X3) ) ) )
| ~ sP4(X0) ),
inference(rectify,[],[f17]) ).
fof(f19,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ( r1(X2,sK9(X2))
& r1(sK9(X2),sK10(X2))
& ~ p2(sK10(X2))
& p2(sK9(X2)) ) ) )
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X3,sK9(X2)),skolemize(X4,sK10(X2))],[f18]) ).
fof(f20,plain,
! [X22] :
( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ~ sP3(X22) ),
inference(nnf_transformation,[],[f10]) ).
fof(f21,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) )
| ~ sP3(X0) ),
inference(rectify,[],[f20]) ).
fof(f22,plain,
! [X0] :
( ( r1(X0,sK11(X0))
& r1(sK11(X0),sK12(X0))
& ~ p2(sK12(X0))
& ! [X3] :
( ~ r1(sK12(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ( r1(X5,sK13(X5))
& r1(sK13(X5),sK14(X5))
& ~ p2(sK14(X5))
& p2(sK13(X5)) ) ) )
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13,sK14]),skolemize(X1,sK11(X0)),skolemize(X2,sK12(X0)),skolemize(X6,sK13(X5)),skolemize(X7,sK14(X5))],[f21]) ).
fof(f23,plain,
! [X32] :
( ! [X33] :
( ~ r1(X32,X33)
| ( ( sP0(X33)
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ~ sP2(X32) ),
inference(nnf_transformation,[],[f9]) ).
fof(f24,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ( sP0(X1)
| ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ( p2(X1)
| ? [X5] :
( r1(X1,X5)
& ? [X6] :
( r1(X5,X6)
& ~ p2(X6) )
& p2(X5) ) ) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f23]) ).
fof(f25,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ( sP0(X1)
| ( r1(X1,sK15(X1))
& ~ p2(sK15(X1))
& ! [X3] :
( ~ r1(sK15(X1),X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ( p2(X1)
| ( r1(X1,sK16(X1))
& r1(sK16(X1),sK17(X1))
& ~ p2(sK17(X1))
& p2(sK16(X1)) ) ) ) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X2,sK15(X1)),skolemize(X5,sK16(X1)),skolemize(X6,sK17(X1))],[f24]) ).
fof(f26,plain,
! [X32] :
( ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ~ sP1(X32) ),
inference(nnf_transformation,[],[f8]) ).
fof(f27,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f26]) ).
fof(f28,plain,
! [X0] :
( ( r1(X0,sK18(X0))
& r1(sK18(X0),sK19(X0))
& ~ p2(sK19(X0))
& ! [X3] :
( ~ r1(sK19(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ( r1(X5,sK20(X5))
& r1(sK20(X5),sK21(X5))
& ~ p2(sK21(X5))
& p2(sK20(X5)) ) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20,sK21]),skolemize(X1,sK18(X0)),skolemize(X2,sK19(X0)),skolemize(X6,sK20(X5)),skolemize(X7,sK21(X5))],[f27]) ).
fof(f32,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( sP5(X0)
| ? [X13] :
( r1(X0,X13)
& ( sP3(X13)
| ( ~ p2(X13)
& ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(X13,X16)
| sP2(X16)
| sP1(X16)
| ( ~ p2(X16)
& ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| p2(X18) )
| ~ p2(X17) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| p2(X19)
| ? [X20] :
( r1(X19,X20)
& ~ p2(X20)
& ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p2(X22) )
| ~ p2(X21) ) ) ) ),
inference(rectify,[],[f13]) ).
fof(f33,plain,
( r1(sK24,sK25)
& ~ p3(sK25)
& ! [X2] :
( ~ r1(sK24,X2)
| p3(X2)
| ( r1(X2,sK26(X2))
& r1(sK26(X2),sK27(X2))
& ~ p3(sK27(X2))
& p3(sK26(X2)) ) )
& r1(sK24,sK28)
& ~ p2(sK28)
& ! [X6] :
( ~ r1(sK24,X6)
| p2(X6)
| ( r1(X6,sK29(X6))
& r1(sK29(X6),sK30(X6))
& ~ p2(sK30(X6))
& p2(sK29(X6)) ) )
& r1(sK24,sK31)
& ~ p1(sK31)
& ! [X10] :
( ~ r1(sK24,X10)
| p1(X10)
| ( r1(X10,sK32(X10))
& r1(sK32(X10),sK33(X10))
& ~ p1(sK33(X10))
& p1(sK32(X10)) ) )
& ( sP5(sK24)
| ( r1(sK24,sK34)
& ( sP3(sK34)
| ( ~ p2(sK34)
& ! [X14] :
( ~ r1(sK34,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(sK34,X16)
| sP2(X16)
| sP1(X16)
| ( ~ p2(X16)
& ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| p2(X18) )
| ~ p2(X17) ) ) ) ) )
& ! [X19] :
( ~ r1(sK24,X19)
| p2(X19)
| ( r1(X19,sK35(X19))
& ~ p2(sK35(X19))
& ! [X21] :
( ~ r1(sK35(X19),X21)
| ! [X22] :
( ~ r1(X21,X22)
| p2(X22) )
| ~ p2(X21) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35]),skolemize(X0,sK24),skolemize(X1,sK25),skolemize(X3,sK26(X2)),skolemize(X4,sK27(X2)),skolemize(X5,sK28),skolemize(X7,sK29(X6)),skolemize(X8,sK30(X6)),skolemize(X9,sK31),skolemize(X11,sK32(X10)),skolemize(X12,sK33(X10)),skolemize(X13,sK34),skolemize(X20,sK35(X19))],[f32]) ).
fof(f38,plain,
! [X2,X3,X0] :
( ~ sP5(X0)
| ~ r1(sK6(X0),X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| sP4(X0) ),
inference(cnf_transformation,[],[f16]) ).
fof(f39,plain,
! [X0] :
( ~ sP5(X0)
| ~ p2(sK6(X0))
| sP4(X0) ),
inference(cnf_transformation,[],[f16]) ).
fof(f40,plain,
! [X0] :
( ~ sP5(X0)
| r1(X0,sK6(X0))
| sP4(X0) ),
inference(cnf_transformation,[],[f16]) ).
fof(f41,plain,
! [X2,X0,X1] :
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| p2(sK9(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f42,plain,
! [X2,X0,X1] :
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(sK10(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(sK9(X2),sK10(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f44,plain,
! [X2,X0,X1] :
( ~ sP4(X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(X2,sK9(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
fof(f45,plain,
! [X0,X5] :
( ~ sP3(X0)
| p2(X5)
| p2(sK13(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f22]) ).
fof(f46,plain,
! [X0,X5] :
( ~ sP3(X0)
| p2(X5)
| ~ p2(sK14(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f22]) ).
fof(f47,plain,
! [X0,X5] :
( ~ sP3(X0)
| p2(X5)
| r1(sK13(X5),sK14(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f22]) ).
fof(f48,plain,
! [X0,X5] :
( ~ sP3(X0)
| p2(X5)
| r1(X5,sK13(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f22]) ).
fof(f49,plain,
! [X3,X0,X4] :
( ~ sP3(X0)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(sK12(X0),X3) ),
inference(cnf_transformation,[],[f22]) ).
fof(f50,plain,
! [X0] :
( ~ sP3(X0)
| ~ p2(sK12(X0)) ),
inference(cnf_transformation,[],[f22]) ).
fof(f51,plain,
! [X0] :
( ~ sP3(X0)
| r1(sK11(X0),sK12(X0)) ),
inference(cnf_transformation,[],[f22]) ).
fof(f52,plain,
! [X0] :
( ~ sP3(X0)
| r1(X0,sK11(X0)) ),
inference(cnf_transformation,[],[f22]) ).
fof(f53,plain,
! [X0,X1] :
( ~ sP2(X0)
| p2(X1)
| p2(sK16(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f54,plain,
! [X0,X1] :
( ~ sP2(X0)
| p2(X1)
| ~ p2(sK17(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f55,plain,
! [X0,X1] :
( ~ sP2(X0)
| p2(X1)
| r1(sK16(X1),sK17(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f56,plain,
! [X0,X1] :
( ~ sP2(X0)
| p2(X1)
| r1(X1,sK16(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f60,plain,
! [X0,X5] :
( ~ sP1(X0)
| p2(X5)
| p2(sK20(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f28]) ).
fof(f61,plain,
! [X0,X5] :
( ~ sP1(X0)
| p2(X5)
| ~ p2(sK21(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f28]) ).
fof(f62,plain,
! [X0,X5] :
( ~ sP1(X0)
| p2(X5)
| r1(sK20(X5),sK21(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f28]) ).
fof(f63,plain,
! [X0,X5] :
( ~ sP1(X0)
| p2(X5)
| r1(X5,sK20(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f28]) ).
fof(f72,plain,
! [X21,X19,X22] :
( ~ p2(X21)
| p2(X19)
| ~ r1(sK35(X19),X21)
| ~ r1(X21,X22)
| p2(X22)
| ~ r1(sK24,X19) ),
inference(cnf_transformation,[],[f33]) ).
fof(f73,plain,
! [X19] :
( ~ p2(sK35(X19))
| p2(X19)
| ~ r1(sK24,X19) ),
inference(cnf_transformation,[],[f33]) ).
fof(f74,plain,
! [X19] :
( ~ r1(sK24,X19)
| p2(X19)
| r1(X19,sK35(X19)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f75,plain,
! [X18,X16,X17] :
( sP5(sK24)
| ~ r1(sK34,X16)
| sP2(X16)
| sP1(X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| p2(X18)
| ~ p2(X17) ),
inference(cnf_transformation,[],[f33]) ).
fof(f76,plain,
! [X16] :
( sP5(sK24)
| ~ r1(sK34,X16)
| sP2(X16)
| sP1(X16)
| ~ p2(X16) ),
inference(cnf_transformation,[],[f33]) ).
fof(f77,plain,
! [X14,X15] :
( sP5(sK24)
| sP3(sK34)
| ~ r1(sK34,X14)
| ~ r1(X14,X15)
| p2(X15)
| ~ p2(X14) ),
inference(cnf_transformation,[],[f33]) ).
fof(f78,plain,
( sP5(sK24)
| sP3(sK34)
| ~ p2(sK34) ),
inference(cnf_transformation,[],[f33]) ).
fof(f79,plain,
( sP5(sK24)
| r1(sK24,sK34) ),
inference(cnf_transformation,[],[f33]) ).
fof(f86,plain,
! [X6] :
( ~ r1(sK24,X6)
| p2(X6)
| p2(sK29(X6)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f87,plain,
! [X6] :
( ~ p2(sK30(X6))
| p2(X6)
| ~ r1(sK24,X6) ),
inference(cnf_transformation,[],[f33]) ).
fof(f88,plain,
! [X6] :
( ~ r1(sK24,X6)
| p2(X6)
| r1(sK29(X6),sK30(X6)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f89,plain,
! [X6] :
( ~ r1(sK24,X6)
| p2(X6)
| r1(X6,sK29(X6)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f90,plain,
~ p2(sK28),
inference(cnf_transformation,[],[f33]) ).
fof(f91,plain,
r1(sK24,sK28),
inference(cnf_transformation,[],[f33]) ).
fof(f99,definition,
( spl36_1
<=> ! [X18,X16,X17] :
( ~ r1(sK34,X16)
| ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(X16,X17)
| sP1(X16)
| sP2(X16) ) ),
introduced(definition,[new_symbols(definition,[spl36_1])],[avatar_definition]) ).
fof(f100,plain,
( ! [X18,X16,X17] :
( ~ p2(X17)
| ~ r1(sK34,X16)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(X16,X17)
| sP1(X16)
| sP2(X16) )
| ~ spl36_1 ),
inference(avatar_component_clause,[],[f99]) ).
fof(f102,definition,
( spl36_2
<=> sP5(sK24) ),
introduced(definition,[new_symbols(definition,[spl36_2])],[avatar_definition]) ).
fof(f104,plain,
( sP5(sK24)
| ~ spl36_2 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f105,plain,
( spl36_1
| spl36_2 ),
inference(avatar_split_clause,[],[f75,f102,f99]) ).
fof(f107,definition,
( spl36_3
<=> ! [X16] :
( ~ r1(sK34,X16)
| ~ p2(X16)
| sP1(X16)
| sP2(X16) ) ),
introduced(definition,[new_symbols(definition,[spl36_3])],[avatar_definition]) ).
fof(f108,plain,
( ! [X16] :
( ~ p2(X16)
| ~ r1(sK34,X16)
| sP1(X16)
| sP2(X16) )
| ~ spl36_3 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f109,plain,
( spl36_3
| spl36_2 ),
inference(avatar_split_clause,[],[f76,f102,f107]) ).
fof(f111,definition,
( spl36_4
<=> ! [X14,X15] :
( ~ r1(sK34,X14)
| ~ p2(X14)
| p2(X15)
| ~ r1(X14,X15) ) ),
introduced(definition,[new_symbols(definition,[spl36_4])],[avatar_definition]) ).
fof(f112,plain,
( ! [X14,X15] :
( ~ p2(X14)
| ~ r1(sK34,X14)
| p2(X15)
| ~ r1(X14,X15) )
| ~ spl36_4 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,definition,
( spl36_5
<=> sP3(sK34) ),
introduced(definition,[new_symbols(definition,[spl36_5])],[avatar_definition]) ).
fof(f116,plain,
( sP3(sK34)
| ~ spl36_5 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f117,plain,
( spl36_4
| spl36_5
| spl36_2 ),
inference(avatar_split_clause,[],[f77,f102,f114,f111]) ).
fof(f119,definition,
( spl36_6
<=> p2(sK34) ),
introduced(definition,[new_symbols(definition,[spl36_6])],[avatar_definition]) ).
fof(f121,plain,
( ~ p2(sK34)
| spl36_6 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f122,plain,
( ~ spl36_6
| spl36_5
| spl36_2 ),
inference(avatar_split_clause,[],[f78,f102,f114,f119]) ).
fof(f124,definition,
( spl36_7
<=> r1(sK24,sK34) ),
introduced(definition,[new_symbols(definition,[spl36_7])],[avatar_definition]) ).
fof(f126,plain,
( r1(sK24,sK34)
| ~ spl36_7 ),
inference(avatar_component_clause,[],[f124]) ).
fof(f127,plain,
( spl36_7
| spl36_2 ),
inference(avatar_split_clause,[],[f79,f102,f124]) ).
fof(f195,plain,
( p2(sK28)
| r1(sK28,sK35(sK28)) ),
inference(resolution,[],[f74,f91]) ).
fof(f202,plain,
r1(sK28,sK35(sK28)),
inference(forward_subsumption_resolution,[],[f195,f90]) ).
fof(f306,plain,
( p2(sK34)
| p2(sK29(sK34))
| ~ spl36_7 ),
inference(resolution,[],[f126,f86]) ).
fof(f333,plain,
( p2(sK29(sK34))
| spl36_6
| ~ spl36_7 ),
inference(forward_subsumption_resolution,[],[f306,f121]) ).
fof(f433,plain,
( p2(sK34)
| r1(sK34,sK29(sK34))
| ~ spl36_7 ),
inference(resolution,[],[f126,f89]) ).
fof(f437,plain,
( r1(sK34,sK29(sK34))
| spl36_6
| ~ spl36_7 ),
inference(forward_subsumption_resolution,[],[f433,f121]) ).
fof(f447,plain,
( ! [X0] :
( ~ r1(sK34,sK29(sK34))
| p2(X0)
| ~ r1(sK29(sK34),X0) )
| ~ spl36_4
| spl36_6
| ~ spl36_7 ),
inference(resolution,[],[f333,f112]) ).
fof(f451,definition,
( spl36_62
<=> ! [X1] :
( ~ r1(sK29(sK34),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl36_62])],[avatar_definition]) ).
fof(f452,plain,
( ! [X1] :
( ~ r1(sK29(sK34),X1)
| p2(X1) )
| ~ spl36_62 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f458,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK29(sK34),X0) )
| ~ spl36_4
| spl36_6
| ~ spl36_7 ),
inference(forward_subsumption_resolution,[],[f447,f437]) ).
fof(f472,plain,
( spl36_62
| ~ spl36_4
| spl36_6
| ~ spl36_7 ),
inference(avatar_split_clause,[],[f458,f124,f119,f111,f451]) ).
fof(f492,plain,
( ~ p2(sK6(sK24))
| sP4(sK24)
| ~ spl36_2 ),
inference(resolution,[],[f39,f104]) ).
fof(f494,definition,
( spl36_70
<=> sP4(sK24) ),
introduced(definition,[new_symbols(definition,[spl36_70])],[avatar_definition]) ).
fof(f495,plain,
( ~ sP4(sK24)
| spl36_70 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f496,plain,
( sP4(sK24)
| ~ spl36_70 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f498,definition,
( spl36_71
<=> p2(sK6(sK24)) ),
introduced(definition,[new_symbols(definition,[spl36_71])],[avatar_definition]) ).
fof(f500,plain,
( ~ p2(sK6(sK24))
| spl36_71 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f501,plain,
( spl36_70
| ~ spl36_71
| ~ spl36_2 ),
inference(avatar_split_clause,[],[f492,f102,f498,f494]) ).
fof(f503,plain,
( r1(sK24,sK6(sK24))
| sP4(sK24)
| ~ spl36_2 ),
inference(resolution,[],[f40,f104]) ).
fof(f505,definition,
( spl36_72
<=> r1(sK24,sK6(sK24)) ),
introduced(definition,[new_symbols(definition,[spl36_72])],[avatar_definition]) ).
fof(f507,plain,
( r1(sK24,sK6(sK24))
| ~ spl36_72 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f508,plain,
( spl36_70
| spl36_72
| ~ spl36_2 ),
inference(avatar_split_clause,[],[f503,f102,f505,f494]) ).
fof(f514,plain,
( p2(sK6(sK24))
| p2(sK29(sK6(sK24)))
| ~ spl36_72 ),
inference(resolution,[],[f507,f86]) ).
fof(f541,plain,
( p2(sK29(sK6(sK24)))
| spl36_71
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f514,f500]) ).
fof(f627,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| p2(X1)
| p2(sK9(X1))
| ~ r1(sK24,X0) )
| ~ spl36_70 ),
inference(resolution,[],[f41,f496]) ).
fof(f697,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| p2(X1)
| r1(X1,sK9(X1))
| ~ r1(sK24,X0) )
| ~ spl36_70 ),
inference(resolution,[],[f44,f496]) ).
fof(f702,plain,
( ! [X0,X1] :
( ~ r1(sK6(sK24),X0)
| ~ r1(X0,X1)
| p2(X1)
| ~ p2(X0)
| sP4(sK24) )
| ~ spl36_2 ),
inference(resolution,[],[f38,f104]) ).
fof(f717,plain,
( p2(sK35(sK28))
| p2(sK9(sK35(sK28)))
| ~ r1(sK24,sK28)
| ~ spl36_70 ),
inference(resolution,[],[f627,f202]) ).
fof(f735,plain,
( p2(sK35(sK28))
| p2(sK9(sK35(sK28)))
| ~ spl36_70 ),
inference(forward_subsumption_resolution,[],[f717,f91]) ).
fof(f751,definition,
( spl36_112
<=> p2(sK9(sK35(sK28))) ),
introduced(definition,[new_symbols(definition,[spl36_112])],[avatar_definition]) ).
fof(f753,plain,
( p2(sK9(sK35(sK28)))
| ~ spl36_112 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f755,definition,
( spl36_113
<=> p2(sK35(sK28)) ),
introduced(definition,[new_symbols(definition,[spl36_113])],[avatar_definition]) ).
fof(f756,plain,
( ~ p2(sK35(sK28))
| spl36_113 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f757,plain,
( p2(sK35(sK28))
| ~ spl36_113 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f758,plain,
( spl36_112
| spl36_113
| ~ spl36_70 ),
inference(avatar_split_clause,[],[f735,f494,f755,f751]) ).
fof(f773,plain,
( p2(sK35(sK28))
| r1(sK35(sK28),sK9(sK35(sK28)))
| ~ r1(sK24,sK28)
| ~ spl36_70 ),
inference(resolution,[],[f697,f202]) ).
fof(f778,plain,
( p2(sK35(sK28))
| r1(sK35(sK28),sK9(sK35(sK28)))
| ~ spl36_70 ),
inference(forward_subsumption_resolution,[],[f773,f91]) ).
fof(f780,definition,
( spl36_116
<=> r1(sK35(sK28),sK9(sK35(sK28))) ),
introduced(definition,[new_symbols(definition,[spl36_116])],[avatar_definition]) ).
fof(f782,plain,
( r1(sK35(sK28),sK9(sK35(sK28)))
| ~ spl36_116 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f783,plain,
( spl36_116
| spl36_113
| ~ spl36_70 ),
inference(avatar_split_clause,[],[f778,f494,f755,f780]) ).
fof(f784,plain,
( p2(sK28)
| ~ r1(sK24,sK28)
| ~ spl36_113 ),
inference(resolution,[],[f757,f73]) ).
fof(f814,plain,
( ~ r1(sK24,sK28)
| ~ spl36_113 ),
inference(forward_subsumption_resolution,[],[f784,f90]) ).
fof(f815,plain,
( $false
| ~ spl36_113 ),
inference(forward_subsumption_resolution,[],[f814,f91]) ).
fof(f816,plain,
~ spl36_113,
inference(avatar_contradiction_clause,[],[f815]) ).
fof(f817,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X0,X1)
| p2(X1)
| ~ r1(sK6(sK24),X0) )
| ~ spl36_2
| spl36_70 ),
inference(forward_subsumption_resolution,[],[f702,f495]) ).
fof(f823,plain,
( p2(sK6(sK24))
| r1(sK29(sK6(sK24)),sK30(sK6(sK24)))
| ~ spl36_72 ),
inference(resolution,[],[f507,f88]) ).
fof(f824,plain,
( p2(sK6(sK24))
| r1(sK6(sK24),sK29(sK6(sK24)))
| ~ spl36_72 ),
inference(resolution,[],[f507,f89]) ).
fof(f834,plain,
( r1(sK6(sK24),sK29(sK6(sK24)))
| spl36_71
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f824,f500]) ).
fof(f835,plain,
( r1(sK29(sK6(sK24)),sK30(sK6(sK24)))
| spl36_71
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f823,f500]) ).
fof(f859,plain,
( ! [X0] :
( ~ r1(sK29(sK6(sK24)),X0)
| p2(X0)
| ~ r1(sK6(sK24),sK29(sK6(sK24))) )
| ~ spl36_2
| spl36_70
| spl36_71
| ~ spl36_72 ),
inference(resolution,[],[f541,f817]) ).
fof(f865,definition,
( spl36_126
<=> ! [X1] :
( ~ r1(sK29(sK6(sK24)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl36_126])],[avatar_definition]) ).
fof(f866,plain,
( ! [X1] :
( ~ r1(sK29(sK6(sK24)),X1)
| p2(X1) )
| ~ spl36_126 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f889,plain,
( ! [X0] :
( ~ r1(sK29(sK6(sK24)),X0)
| p2(X0) )
| ~ spl36_2
| spl36_70
| spl36_71
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f859,f834]) ).
fof(f890,plain,
( spl36_126
| ~ spl36_2
| spl36_70
| spl36_71
| ~ spl36_72 ),
inference(avatar_split_clause,[],[f889,f505,f498,f494,f102,f865]) ).
fof(f895,plain,
( ! [X0,X1] :
( p2(X0)
| ~ r1(sK35(X0),sK9(sK35(sK28)))
| ~ r1(sK9(sK35(sK28)),X1)
| p2(X1)
| ~ r1(sK24,X0) )
| ~ spl36_112 ),
inference(resolution,[],[f753,f72]) ).
fof(f897,definition,
( spl36_132
<=> ! [X1] :
( ~ r1(sK9(sK35(sK28)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl36_132])],[avatar_definition]) ).
fof(f898,plain,
( ! [X1] :
( ~ r1(sK9(sK35(sK28)),X1)
| p2(X1) )
| ~ spl36_132 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f900,definition,
( spl36_133
<=> ! [X0] :
( p2(X0)
| ~ r1(sK24,X0)
| ~ r1(sK35(X0),sK9(sK35(sK28))) ) ),
introduced(definition,[new_symbols(definition,[spl36_133])],[avatar_definition]) ).
fof(f901,plain,
( ! [X0] :
( ~ r1(sK24,X0)
| p2(X0)
| ~ r1(sK35(X0),sK9(sK35(sK28))) )
| ~ spl36_133 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f902,plain,
( spl36_132
| spl36_133
| ~ spl36_112 ),
inference(avatar_split_clause,[],[f895,f751,f900,f897]) ).
fof(f926,plain,
( p2(sK30(sK6(sK24)))
| spl36_71
| ~ spl36_72
| ~ spl36_126 ),
inference(resolution,[],[f866,f835]) ).
fof(f927,plain,
( p2(sK6(sK24))
| ~ r1(sK24,sK6(sK24))
| spl36_71
| ~ spl36_72
| ~ spl36_126 ),
inference(resolution,[],[f926,f87]) ).
fof(f963,plain,
( ~ r1(sK24,sK6(sK24))
| spl36_71
| ~ spl36_72
| ~ spl36_126 ),
inference(forward_subsumption_resolution,[],[f927,f500]) ).
fof(f964,plain,
( $false
| spl36_71
| ~ spl36_72
| ~ spl36_126 ),
inference(forward_subsumption_resolution,[],[f963,f507]) ).
fof(f965,plain,
( spl36_71
| ~ spl36_72
| ~ spl36_126 ),
inference(avatar_contradiction_clause,[],[f964]) ).
fof(f966,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| p2(X1)
| r1(sK9(X1),sK10(X1))
| ~ r1(sK24,X0) )
| ~ spl36_70 ),
inference(resolution,[],[f496,f43]) ).
fof(f968,plain,
( ! [X0,X1] :
( ~ p2(sK10(X1))
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK24,X0) )
| ~ spl36_70 ),
inference(resolution,[],[f496,f42]) ).
fof(f1066,plain,
( p2(sK35(sK28))
| r1(sK9(sK35(sK28)),sK10(sK35(sK28)))
| ~ r1(sK24,sK28)
| ~ spl36_70 ),
inference(resolution,[],[f966,f202]) ).
fof(f1073,plain,
( r1(sK9(sK35(sK28)),sK10(sK35(sK28)))
| ~ r1(sK24,sK28)
| ~ spl36_70
| spl36_113 ),
inference(forward_subsumption_resolution,[],[f1066,f756]) ).
fof(f1075,plain,
( r1(sK9(sK35(sK28)),sK10(sK35(sK28)))
| ~ spl36_70
| spl36_113 ),
inference(forward_subsumption_resolution,[],[f1073,f91]) ).
fof(f1118,definition,
( spl36_165
<=> p2(sK10(sK35(sK28))) ),
introduced(definition,[new_symbols(definition,[spl36_165])],[avatar_definition]) ).
fof(f1120,plain,
( p2(sK10(sK35(sK28)))
| ~ spl36_165 ),
inference(avatar_component_clause,[],[f1118]) ).
fof(f1169,plain,
( p2(sK28)
| ~ r1(sK35(sK28),sK9(sK35(sK28)))
| ~ spl36_133 ),
inference(resolution,[],[f901,f91]) ).
fof(f1171,plain,
( ~ r1(sK35(sK28),sK9(sK35(sK28)))
| ~ spl36_133 ),
inference(forward_subsumption_resolution,[],[f1169,f90]) ).
fof(f1173,plain,
( $false
| ~ spl36_116
| ~ spl36_133 ),
inference(forward_subsumption_resolution,[],[f1171,f782]) ).
fof(f1174,plain,
( ~ spl36_116
| ~ spl36_133 ),
inference(avatar_contradiction_clause,[],[f1173]) ).
fof(f1175,plain,
( p2(sK10(sK35(sK28)))
| ~ spl36_70
| spl36_113
| ~ spl36_132 ),
inference(resolution,[],[f898,f1075]) ).
fof(f1176,plain,
( spl36_165
| ~ spl36_70
| spl36_113
| ~ spl36_132 ),
inference(avatar_split_clause,[],[f1175,f897,f755,f494,f1118]) ).
fof(f1177,plain,
( ! [X0] :
( p2(sK35(sK28))
| ~ r1(X0,sK35(sK28))
| ~ r1(sK24,X0) )
| ~ spl36_70
| ~ spl36_165 ),
inference(resolution,[],[f1120,f968]) ).
fof(f1207,plain,
( ! [X0] :
( ~ r1(X0,sK35(sK28))
| ~ r1(sK24,X0) )
| ~ spl36_70
| spl36_113
| ~ spl36_165 ),
inference(forward_subsumption_resolution,[],[f1177,f756]) ).
fof(f1216,plain,
( ~ r1(sK24,sK28)
| ~ spl36_70
| spl36_113
| ~ spl36_165 ),
inference(resolution,[],[f1207,f202]) ).
fof(f1217,plain,
( $false
| ~ spl36_70
| spl36_113
| ~ spl36_165 ),
inference(forward_subsumption_resolution,[],[f1216,f91]) ).
fof(f1218,plain,
( ~ spl36_70
| spl36_113
| ~ spl36_165 ),
inference(avatar_contradiction_clause,[],[f1217]) ).
fof(f1226,plain,
( p2(sK34)
| r1(sK29(sK34),sK30(sK34))
| ~ spl36_7 ),
inference(resolution,[],[f126,f88]) ).
fof(f1240,plain,
( r1(sK29(sK34),sK30(sK34))
| spl36_6
| ~ spl36_7 ),
inference(forward_subsumption_resolution,[],[f1226,f121]) ).
fof(f1277,plain,
( p2(sK30(sK34))
| spl36_6
| ~ spl36_7
| ~ spl36_62 ),
inference(resolution,[],[f452,f1240]) ).
fof(f1278,plain,
( p2(sK34)
| ~ r1(sK24,sK34)
| spl36_6
| ~ spl36_7
| ~ spl36_62 ),
inference(resolution,[],[f1277,f87]) ).
fof(f1308,plain,
( ~ r1(sK24,sK34)
| spl36_6
| ~ spl36_7
| ~ spl36_62 ),
inference(forward_subsumption_resolution,[],[f1278,f121]) ).
fof(f1309,plain,
( $false
| spl36_6
| ~ spl36_7
| ~ spl36_62 ),
inference(forward_subsumption_resolution,[],[f1308,f126]) ).
fof(f1310,plain,
( spl36_6
| ~ spl36_7
| ~ spl36_62 ),
inference(avatar_contradiction_clause,[],[f1309]) ).
fof(f1311,plain,
( ! [X0] :
( ~ r1(sK34,X0)
| p2(sK13(X0))
| p2(X0) )
| ~ spl36_5 ),
inference(resolution,[],[f116,f45]) ).
fof(f1312,plain,
( ! [X0] :
( ~ p2(sK14(X0))
| p2(X0)
| ~ r1(sK34,X0) )
| ~ spl36_5 ),
inference(resolution,[],[f116,f46]) ).
fof(f1313,plain,
( ! [X0] :
( ~ r1(sK34,X0)
| r1(sK13(X0),sK14(X0))
| p2(X0) )
| ~ spl36_5 ),
inference(resolution,[],[f116,f47]) ).
fof(f1314,plain,
( ! [X0] :
( ~ r1(sK34,X0)
| r1(X0,sK13(X0))
| p2(X0) )
| ~ spl36_5 ),
inference(resolution,[],[f116,f48]) ).
fof(f1315,plain,
( ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK12(sK34),X0) )
| ~ spl36_5 ),
inference(resolution,[],[f116,f49]) ).
fof(f1316,plain,
( ~ p2(sK12(sK34))
| ~ spl36_5 ),
inference(resolution,[],[f116,f50]) ).
fof(f1317,plain,
( r1(sK11(sK34),sK12(sK34))
| ~ spl36_5 ),
inference(resolution,[],[f116,f51]) ).
fof(f1318,plain,
( r1(sK34,sK11(sK34))
| ~ spl36_5 ),
inference(resolution,[],[f116,f52]) ).
fof(f1329,definition,
( spl36_189
<=> sP1(sK11(sK34)) ),
introduced(definition,[new_symbols(definition,[spl36_189])],[avatar_definition]) ).
fof(f1330,plain,
( ~ sP1(sK11(sK34))
| spl36_189 ),
inference(avatar_component_clause,[],[f1329]) ).
fof(f1331,plain,
( sP1(sK11(sK34))
| ~ spl36_189 ),
inference(avatar_component_clause,[],[f1329]) ).
fof(f1333,definition,
( spl36_190
<=> sP2(sK11(sK34)) ),
introduced(definition,[new_symbols(definition,[spl36_190])],[avatar_definition]) ).
fof(f1334,plain,
( ~ sP2(sK11(sK34))
| spl36_190 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1335,plain,
( sP2(sK11(sK34))
| ~ spl36_190 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1359,plain,
( p2(sK13(sK11(sK34)))
| p2(sK11(sK34))
| ~ spl36_5 ),
inference(resolution,[],[f1311,f1318]) ).
fof(f1361,definition,
( spl36_195
<=> p2(sK11(sK34)) ),
introduced(definition,[new_symbols(definition,[spl36_195])],[avatar_definition]) ).
fof(f1362,plain,
( ~ p2(sK11(sK34))
| spl36_195 ),
inference(avatar_component_clause,[],[f1361]) ).
fof(f1363,plain,
( p2(sK11(sK34))
| ~ spl36_195 ),
inference(avatar_component_clause,[],[f1361]) ).
fof(f1365,definition,
( spl36_196
<=> p2(sK13(sK11(sK34))) ),
introduced(definition,[new_symbols(definition,[spl36_196])],[avatar_definition]) ).
fof(f1367,plain,
( p2(sK13(sK11(sK34)))
| ~ spl36_196 ),
inference(avatar_component_clause,[],[f1365]) ).
fof(f1368,plain,
( spl36_195
| spl36_196
| ~ spl36_5 ),
inference(avatar_split_clause,[],[f1359,f114,f1365,f1361]) ).
fof(f1379,plain,
( ~ r1(sK34,sK11(sK34))
| sP1(sK11(sK34))
| sP2(sK11(sK34))
| ~ spl36_3
| ~ spl36_195 ),
inference(resolution,[],[f1363,f108]) ).
fof(f1388,plain,
( sP1(sK11(sK34))
| sP2(sK11(sK34))
| ~ spl36_3
| ~ spl36_5
| ~ spl36_195 ),
inference(forward_subsumption_resolution,[],[f1379,f1318]) ).
fof(f1393,plain,
( spl36_190
| spl36_189
| ~ spl36_3
| ~ spl36_5
| ~ spl36_195 ),
inference(avatar_split_clause,[],[f1388,f1361,f114,f107,f1329,f1333]) ).
fof(f1416,plain,
( r1(sK11(sK34),sK13(sK11(sK34)))
| p2(sK11(sK34))
| ~ spl36_5 ),
inference(resolution,[],[f1314,f1318]) ).
fof(f1420,plain,
( r1(sK13(sK11(sK34)),sK14(sK11(sK34)))
| p2(sK11(sK34))
| ~ spl36_5 ),
inference(resolution,[],[f1313,f1318]) ).
fof(f1422,plain,
( ! [X0] :
( ~ r1(sK11(sK34),X0)
| p2(sK16(X0))
| p2(X0) )
| ~ spl36_190 ),
inference(resolution,[],[f1335,f53]) ).
fof(f1514,plain,
( r1(sK13(sK11(sK34)),sK14(sK11(sK34)))
| ~ spl36_5
| spl36_195 ),
inference(forward_subsumption_resolution,[],[f1420,f1362]) ).
fof(f1516,plain,
( ! [X0,X1] :
( ~ r1(sK34,X0)
| p2(X1)
| ~ r1(sK13(sK11(sK34)),X1)
| ~ r1(X0,sK13(sK11(sK34)))
| sP1(X0)
| sP2(X0) )
| ~ spl36_1
| ~ spl36_196 ),
inference(resolution,[],[f1367,f100]) ).
fof(f1520,definition,
( spl36_217
<=> ! [X1] :
( ~ r1(sK13(sK11(sK34)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl36_217])],[avatar_definition]) ).
fof(f1521,plain,
( ! [X1] :
( ~ r1(sK13(sK11(sK34)),X1)
| p2(X1) )
| ~ spl36_217 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1540,definition,
( spl36_222
<=> ! [X0] :
( ~ r1(sK34,X0)
| sP2(X0)
| sP1(X0)
| ~ r1(X0,sK13(sK11(sK34))) ) ),
introduced(definition,[new_symbols(definition,[spl36_222])],[avatar_definition]) ).
fof(f1541,plain,
( ! [X0] :
( ~ r1(sK34,X0)
| sP2(X0)
| sP1(X0)
| ~ r1(X0,sK13(sK11(sK34))) )
| ~ spl36_222 ),
inference(avatar_component_clause,[],[f1540]) ).
fof(f1542,plain,
( spl36_217
| spl36_222
| ~ spl36_1
| ~ spl36_196 ),
inference(avatar_split_clause,[],[f1516,f1365,f99,f1540,f1520]) ).
fof(f1586,plain,
( p2(sK14(sK11(sK34)))
| ~ spl36_5
| spl36_195
| ~ spl36_217 ),
inference(resolution,[],[f1521,f1514]) ).
fof(f1587,plain,
( p2(sK11(sK34))
| ~ r1(sK34,sK11(sK34))
| ~ spl36_5
| spl36_195
| ~ spl36_217 ),
inference(resolution,[],[f1586,f1312]) ).
fof(f1621,plain,
( ~ r1(sK34,sK11(sK34))
| ~ spl36_5
| spl36_195
| ~ spl36_217 ),
inference(forward_subsumption_resolution,[],[f1587,f1362]) ).
fof(f1622,plain,
( $false
| ~ spl36_5
| spl36_195
| ~ spl36_217 ),
inference(forward_subsumption_resolution,[],[f1621,f1318]) ).
fof(f1623,plain,
( ~ spl36_5
| spl36_195
| ~ spl36_217 ),
inference(avatar_contradiction_clause,[],[f1622]) ).
fof(f1886,plain,
( p2(sK16(sK12(sK34)))
| p2(sK12(sK34))
| ~ spl36_5
| ~ spl36_190 ),
inference(resolution,[],[f1422,f1317]) ).
fof(f1887,plain,
( p2(sK16(sK12(sK34)))
| ~ spl36_5
| ~ spl36_190 ),
inference(forward_subsumption_resolution,[],[f1886,f1316]) ).
fof(f1889,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK16(sK12(sK34)),X0)
| ~ r1(sK12(sK34),sK16(sK12(sK34))) )
| ~ spl36_5
| ~ spl36_190 ),
inference(resolution,[],[f1887,f1315]) ).
fof(f1894,definition,
( spl36_282
<=> ! [X1] :
( ~ r1(sK16(sK12(sK34)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl36_282])],[avatar_definition]) ).
fof(f1895,plain,
( ! [X1] :
( ~ r1(sK16(sK12(sK34)),X1)
| p2(X1) )
| ~ spl36_282 ),
inference(avatar_component_clause,[],[f1894]) ).
fof(f1918,definition,
( spl36_288
<=> r1(sK12(sK34),sK16(sK12(sK34))) ),
introduced(definition,[new_symbols(definition,[spl36_288])],[avatar_definition]) ).
fof(f1921,plain,
( ~ spl36_288
| spl36_282
| ~ spl36_5
| ~ spl36_190 ),
inference(avatar_split_clause,[],[f1889,f1333,f114,f1894,f1918]) ).
fof(f1990,plain,
( ! [X0] :
( ~ r1(sK11(sK34),X0)
| r1(X0,sK16(X0))
| p2(X0) )
| ~ spl36_190 ),
inference(resolution,[],[f1335,f56]) ).
fof(f2001,plain,
( r1(sK12(sK34),sK16(sK12(sK34)))
| p2(sK12(sK34))
| ~ spl36_5
| ~ spl36_190 ),
inference(resolution,[],[f1990,f1317]) ).
fof(f2002,plain,
( r1(sK12(sK34),sK16(sK12(sK34)))
| ~ spl36_5
| ~ spl36_190 ),
inference(forward_subsumption_resolution,[],[f2001,f1316]) ).
fof(f2003,plain,
( spl36_288
| ~ spl36_5
| ~ spl36_190 ),
inference(avatar_split_clause,[],[f2002,f1333,f114,f1918]) ).
fof(f2141,plain,
( ! [X0] :
( ~ r1(sK11(sK34),X0)
| p2(sK20(X0))
| p2(X0) )
| ~ spl36_189 ),
inference(resolution,[],[f1331,f60]) ).
fof(f2142,plain,
( ! [X0] :
( ~ p2(sK21(X0))
| p2(X0)
| ~ r1(sK11(sK34),X0) )
| ~ spl36_189 ),
inference(resolution,[],[f1331,f61]) ).
fof(f2143,plain,
( ! [X0] :
( ~ r1(sK11(sK34),X0)
| r1(sK20(X0),sK21(X0))
| p2(X0) )
| ~ spl36_189 ),
inference(resolution,[],[f1331,f62]) ).
fof(f2144,plain,
( ! [X0] :
( ~ r1(sK11(sK34),X0)
| r1(X0,sK20(X0))
| p2(X0) )
| ~ spl36_189 ),
inference(resolution,[],[f1331,f63]) ).
fof(f2158,plain,
( p2(sK20(sK12(sK34)))
| p2(sK12(sK34))
| ~ spl36_5
| ~ spl36_189 ),
inference(resolution,[],[f2141,f1317]) ).
fof(f2160,plain,
( p2(sK20(sK12(sK34)))
| ~ spl36_5
| ~ spl36_189 ),
inference(forward_subsumption_resolution,[],[f2158,f1316]) ).
fof(f2162,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK20(sK12(sK34)),X0)
| ~ r1(sK12(sK34),sK20(sK12(sK34))) )
| ~ spl36_5
| ~ spl36_189 ),
inference(resolution,[],[f2160,f1315]) ).
fof(f2167,definition,
( spl36_323
<=> ! [X1] :
( ~ r1(sK20(sK12(sK34)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl36_323])],[avatar_definition]) ).
fof(f2168,plain,
( ! [X1] :
( ~ r1(sK20(sK12(sK34)),X1)
| p2(X1) )
| ~ spl36_323 ),
inference(avatar_component_clause,[],[f2167]) ).
fof(f2191,definition,
( spl36_329
<=> r1(sK12(sK34),sK20(sK12(sK34))) ),
introduced(definition,[new_symbols(definition,[spl36_329])],[avatar_definition]) ).
fof(f2194,plain,
( ~ spl36_329
| spl36_323
| ~ spl36_5
| ~ spl36_189 ),
inference(avatar_split_clause,[],[f2162,f1329,f114,f2167,f2191]) ).
fof(f2207,plain,
( r1(sK12(sK34),sK20(sK12(sK34)))
| p2(sK12(sK34))
| ~ spl36_5
| ~ spl36_189 ),
inference(resolution,[],[f2144,f1317]) ).
fof(f2209,plain,
( r1(sK12(sK34),sK20(sK12(sK34)))
| ~ spl36_5
| ~ spl36_189 ),
inference(forward_subsumption_resolution,[],[f2207,f1316]) ).
fof(f2210,plain,
( spl36_329
| ~ spl36_5
| ~ spl36_189 ),
inference(avatar_split_clause,[],[f2209,f1329,f114,f2191]) ).
fof(f2211,plain,
( r1(sK20(sK12(sK34)),sK21(sK12(sK34)))
| p2(sK12(sK34))
| ~ spl36_5
| ~ spl36_189 ),
inference(resolution,[],[f2143,f1317]) ).
fof(f2213,plain,
( r1(sK20(sK12(sK34)),sK21(sK12(sK34)))
| ~ spl36_5
| ~ spl36_189 ),
inference(forward_subsumption_resolution,[],[f2211,f1316]) ).
fof(f2321,plain,
( p2(sK21(sK12(sK34)))
| ~ spl36_5
| ~ spl36_189
| ~ spl36_323 ),
inference(resolution,[],[f2168,f2213]) ).
fof(f2322,plain,
( p2(sK12(sK34))
| ~ r1(sK11(sK34),sK12(sK34))
| ~ spl36_5
| ~ spl36_189
| ~ spl36_323 ),
inference(resolution,[],[f2321,f2142]) ).
fof(f2370,plain,
( ~ r1(sK11(sK34),sK12(sK34))
| ~ spl36_5
| ~ spl36_189
| ~ spl36_323 ),
inference(forward_subsumption_resolution,[],[f2322,f1316]) ).
fof(f2371,plain,
( $false
| ~ spl36_5
| ~ spl36_189
| ~ spl36_323 ),
inference(forward_subsumption_resolution,[],[f2370,f1317]) ).
fof(f2372,plain,
( ~ spl36_5
| ~ spl36_189
| ~ spl36_323 ),
inference(avatar_contradiction_clause,[],[f2371]) ).
fof(f2395,plain,
( ! [X0] :
( ~ p2(sK17(X0))
| p2(X0)
| ~ r1(sK11(sK34),X0) )
| ~ spl36_190 ),
inference(resolution,[],[f1335,f54]) ).
fof(f2396,plain,
( ! [X0] :
( ~ r1(sK11(sK34),X0)
| r1(sK16(X0),sK17(X0))
| p2(X0) )
| ~ spl36_190 ),
inference(resolution,[],[f1335,f55]) ).
fof(f2411,plain,
( r1(sK16(sK12(sK34)),sK17(sK12(sK34)))
| p2(sK12(sK34))
| ~ spl36_5
| ~ spl36_190 ),
inference(resolution,[],[f2396,f1317]) ).
fof(f2412,plain,
( r1(sK16(sK12(sK34)),sK17(sK12(sK34)))
| ~ spl36_5
| ~ spl36_190 ),
inference(forward_subsumption_resolution,[],[f2411,f1316]) ).
fof(f2413,plain,
( p2(sK17(sK12(sK34)))
| ~ spl36_5
| ~ spl36_190
| ~ spl36_282 ),
inference(resolution,[],[f2412,f1895]) ).
fof(f2440,plain,
( p2(sK12(sK34))
| ~ r1(sK11(sK34),sK12(sK34))
| ~ spl36_5
| ~ spl36_190
| ~ spl36_282 ),
inference(resolution,[],[f2413,f2395]) ).
fof(f2485,plain,
( ~ r1(sK11(sK34),sK12(sK34))
| ~ spl36_5
| ~ spl36_190
| ~ spl36_282 ),
inference(forward_subsumption_resolution,[],[f2440,f1316]) ).
fof(f2486,plain,
( $false
| ~ spl36_5
| ~ spl36_190
| ~ spl36_282 ),
inference(forward_subsumption_resolution,[],[f2485,f1317]) ).
fof(f2487,plain,
( ~ spl36_5
| ~ spl36_190
| ~ spl36_282 ),
inference(avatar_contradiction_clause,[],[f2486]) ).
fof(f2488,plain,
( r1(sK11(sK34),sK13(sK11(sK34)))
| ~ spl36_5
| spl36_195 ),
inference(forward_subsumption_resolution,[],[f1416,f1362]) ).
fof(f2536,plain,
( sP2(sK11(sK34))
| sP1(sK11(sK34))
| ~ r1(sK11(sK34),sK13(sK11(sK34)))
| ~ spl36_5
| ~ spl36_222 ),
inference(resolution,[],[f1541,f1318]) ).
fof(f2537,plain,
( sP1(sK11(sK34))
| ~ r1(sK11(sK34),sK13(sK11(sK34)))
| ~ spl36_5
| spl36_190
| ~ spl36_222 ),
inference(forward_subsumption_resolution,[],[f2536,f1334]) ).
fof(f2538,plain,
( ~ r1(sK11(sK34),sK13(sK11(sK34)))
| ~ spl36_5
| spl36_189
| spl36_190
| ~ spl36_222 ),
inference(forward_subsumption_resolution,[],[f2537,f1330]) ).
fof(f2539,plain,
( $false
| ~ spl36_5
| spl36_189
| spl36_190
| spl36_195
| ~ spl36_222 ),
inference(forward_subsumption_resolution,[],[f2538,f2488]) ).
fof(f2540,plain,
( ~ spl36_5
| spl36_189
| spl36_190
| spl36_195
| ~ spl36_222 ),
inference(avatar_contradiction_clause,[],[f2539]) ).
cnf(s1,plain,
( spl36_1
| spl36_2 ),
inference(sat_conversion,[],[f105]) ).
cnf(s2,plain,
( spl36_2
| spl36_3 ),
inference(sat_conversion,[],[f109]) ).
cnf(s3,plain,
( spl36_2
| spl36_4
| spl36_5 ),
inference(sat_conversion,[],[f117]) ).
cnf(s4,plain,
( spl36_2
| spl36_5
| ~ spl36_6 ),
inference(sat_conversion,[],[f122]) ).
cnf(s5,plain,
( spl36_2
| spl36_7 ),
inference(sat_conversion,[],[f127]) ).
cnf(s39,plain,
( ~ spl36_4
| spl36_6
| ~ spl36_7
| spl36_62 ),
inference(sat_conversion,[],[f472]) ).
cnf(s41,plain,
( ~ spl36_2
| spl36_70
| ~ spl36_71 ),
inference(sat_conversion,[],[f501]) ).
cnf(s42,plain,
( ~ spl36_2
| spl36_70
| spl36_72 ),
inference(sat_conversion,[],[f508]) ).
cnf(s70,plain,
( ~ spl36_70
| spl36_112
| spl36_113 ),
inference(sat_conversion,[],[f758]) ).
cnf(s72,plain,
( ~ spl36_70
| spl36_113
| spl36_116 ),
inference(sat_conversion,[],[f783]) ).
cnf(s77,plain,
~ spl36_113,
inference(sat_conversion,[],[f816]) ).
cnf(s85,plain,
( ~ spl36_2
| spl36_70
| spl36_71
| ~ spl36_72
| spl36_126 ),
inference(sat_conversion,[],[f890]) ).
cnf(s86,plain,
( ~ spl36_112
| spl36_132
| spl36_133 ),
inference(sat_conversion,[],[f902]) ).
cnf(s96,plain,
( spl36_71
| ~ spl36_72
| ~ spl36_126 ),
inference(sat_conversion,[],[f965]) ).
cnf(s114,plain,
( ~ spl36_116
| ~ spl36_133 ),
inference(sat_conversion,[],[f1174]) ).
cnf(s115,plain,
( ~ spl36_70
| spl36_113
| ~ spl36_132
| spl36_165 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s121,plain,
( ~ spl36_70
| spl36_113
| ~ spl36_165 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s130,plain,
( spl36_6
| ~ spl36_7
| ~ spl36_62 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s136,plain,
( ~ spl36_5
| spl36_195
| spl36_196 ),
inference(sat_conversion,[],[f1368]) ).
cnf(s140,plain,
( ~ spl36_3
| ~ spl36_5
| spl36_189
| spl36_190
| ~ spl36_195 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s157,plain,
( ~ spl36_1
| ~ spl36_196
| spl36_217
| spl36_222 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s168,plain,
( ~ spl36_5
| spl36_195
| ~ spl36_217 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s204,plain,
( ~ spl36_5
| ~ spl36_190
| spl36_282
| ~ spl36_288 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s212,plain,
( ~ spl36_5
| ~ spl36_190
| spl36_288 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s234,plain,
( ~ spl36_5
| ~ spl36_189
| spl36_323
| ~ spl36_329 ),
inference(sat_conversion,[],[f2194]) ).
cnf(s237,plain,
( ~ spl36_5
| ~ spl36_189
| spl36_329 ),
inference(sat_conversion,[],[f2210]) ).
cnf(s257,plain,
( ~ spl36_5
| ~ spl36_189
| ~ spl36_323 ),
inference(sat_conversion,[],[f2372]) ).
cnf(s269,plain,
( ~ spl36_5
| ~ spl36_190
| ~ spl36_282 ),
inference(sat_conversion,[],[f2487]) ).
cnf(s273,plain,
( ~ spl36_5
| spl36_189
| spl36_190
| spl36_195
| ~ spl36_222 ),
inference(sat_conversion,[],[f2540]) ).
cnf(s274,plain,
( ~ spl36_70
| spl36_116 ),
inference(rat,[],[s72,s77]) ).
cnf(s275,plain,
( ~ spl36_70
| spl36_112 ),
inference(rat,[],[s70,s77]) ).
cnf(s278,plain,
( spl36_70
| ~ spl36_2 ),
inference(rat,[],[s85,s96,s41,s42]) ).
cnf(s279,plain,
( ~ spl36_70
| spl36_165 ),
inference(rat,[],[s86,s114,s275,s274,s115,s77]) ).
cnf(s280,plain,
~ spl36_70,
inference(rat,[],[s279,s121,s77]) ).
cnf(s281,plain,
~ spl36_2,
inference(rat,[],[s278,s280]) ).
cnf(s282,plain,
spl36_7,
inference(rat,[],[s5,s281]) ).
cnf(s283,plain,
spl36_3,
inference(rat,[],[s2,s281]) ).
cnf(s284,plain,
spl36_1,
inference(rat,[],[s1,s281]) ).
cnf(s288,plain,
( spl36_190
| spl36_189
| ~ spl36_5 ),
inference(rat,[],[s157,s273,s136,s168,s140,s283,s284]) ).
cnf(s289,plain,
( ~ spl36_190
| ~ spl36_5 ),
inference(rat,[],[s204,s212,s269]) ).
cnf(s290,plain,
( ~ spl36_189
| ~ spl36_5 ),
inference(rat,[],[s234,s237,s257]) ).
cnf(s291,plain,
( spl36_190
| ~ spl36_5 ),
inference(rat,[],[s290,s288]) ).
cnf(s292,plain,
~ spl36_5,
inference(rat,[],[s291,s289]) ).
cnf(s293,plain,
~ spl36_6,
inference(rat,[],[s4,s281,s292]) ).
cnf(s294,plain,
spl36_4,
inference(rat,[],[s3,s281,s292]) ).
cnf(s296,plain,
~ spl36_62,
inference(rat,[],[s130,s282,s293]) ).
cnf(s297,plain,
$false,
inference(rat,[],[s39,s296,s282,s293,s294]) ).
fof(f2541,plain,
$false,
inference(avatar_sat_refutation,[],[s297]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL642+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 16:10:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.40 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
% 0.37/0.48 % (1135236)Will run a generic schedule for satisfiability detection.
% 0.37/0.48 % (1135242)% WARNING: option uhcvi not known.
% 0.37/0.48 % (1135242)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1948858900:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.37/0.48 % (1135241)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=201824831_2999 on theBenchmark for (2999ds/0Mi)
% 0.37/0.48 % (1135244)dis+10_1_sil=32000:sp=arity:random_seed=3258339407:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.37/0.48 % (1135243)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3372960405:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.37/0.48 % (1135245)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4203167539:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.37/0.48 % (1135246)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2285332277:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.37/0.48 % (1135247)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1704344151:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.37/0.48 % TRYING [1]
% 0.37/0.48 % TRYING [2]
% 0.37/0.48 % TRYING [3]
% 0.37/0.48 % TRYING [4]
% 0.37/0.48 % (1135246) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1135236-1135246"...
% 0.37/0.48 % (1135246)...printing done.
% 0.37/0.48 % (1135246)Refutation found. Thanks to Tanya!
% 0.37/0.48 % SZS status Theorem for theBenchmark
% 0.37/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.37/0.48 % (1135246)------------------------------
% 0.37/0.48 % (1135246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.37/0.48 % (1135246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.37/0.48 % (1135246)CaDiCaL version: 2.1.3
% 0.37/0.48 % (1135246)Termination reason: Refutation
% 0.37/0.48 % (1135246)Time elapsed: 0.036 s
% 0.37/0.48 % (1135246)Peak memory usage: 13 MB
% 0.37/0.48 % (1135246)Instructions burned: 52 (million)
% 0.37/0.48 % (1135236)Success in time 0.077 s
% 0.37/0.48 % Vampire exiting
%------------------------------------------------------------------------------