%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL640+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:53:42 AM UTC 2026
% Result : Theorem 4.64s 2.04s
% Output : Refutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 30
% Syntax : Number of formulae : 311 ( 30 unt; 29 def)
% Number of atoms : 2202 ( 0 equ)
% Maximal formula atoms : 121 ( 7 avg)
% Number of connectives : 3364 (1473 ~;1569 |; 297 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 26 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 6 con; 0-1 aty)
% Number of variables : 927 ( 0 sgn 802 !; 125 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [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)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) )
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) )
& ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [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)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [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)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) )
| ~ ( ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) )
& ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
& ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [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)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( ( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| p1(X6) ) )
| ~ ! [X7] :
( ~ r1(X4,X7)
| p1(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) ) )
& ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ~ ! [X13] :
( ~ r1(X10,X13)
| p1(X13) ) ) ) ) ) ) )
| ~ ! [X14] :
( ~ r1(X0,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( ( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) )
| ~ p1(X19) ) )
| ~ ! [X21] :
( ~ r1(X16,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) )
| ~ p1(X21)
| ~ ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ~ ( ! [X26] :
( ~ r1(X23,X26)
| p1(X26) )
| ~ p1(X23) ) ) ) )
& ( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p1(X28) ) )
| ~ ! [X29] :
( ~ r1(X16,X29)
| p1(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X16,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ~ ! [X35] :
( ~ r1(X32,X35)
| p1(X35) ) )
& ( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| p1(X39) )
| ~ p1(X38) ) ) )
| ~ ! [X40] :
( ~ r1(X16,X40)
| p1(X40)
| ~ ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) )
| ~ p1(X41) ) ) ) ) ) ) )
| ~ ( ~ ! [X43] :
( ~ r1(X0,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p1(X46) )
| ! [X47] :
( ~ r1(X45,X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| p1(X48) ) )
| ~ ! [X49] :
( ~ r1(X45,X49)
| p1(X49)
| ~ ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p1(X51) )
| ~ p1(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ( ( p1(X53)
| ! [X54] :
( ~ r1(X53,X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| p1(X55) ) )
| ~ ! [X56] :
( ~ r1(X53,X56)
| p1(X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57) ) ) )
& ! [X59] :
( ~ r1(X53,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ~ ! [X62] :
( ~ r1(X59,X62)
| p1(X62) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ( ( p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| ~ ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ~ ! [X66] :
( ~ r1(X63,X66)
| p1(X66)
| ~ ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| p1(X68) )
| ~ p1(X67) ) ) )
& ! [X69] :
( ~ r1(X63,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p1(X71) ) )
| ~ ! [X72] :
( ~ r1(X69,X72)
| p1(X72) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( ( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| p1(X6) ) )
| ~ ! [X7] :
( ~ r1(X4,X7)
| p1(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) ) )
& ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ~ ! [X13] :
( ~ r1(X10,X13)
| p1(X13) ) ) ) ) ) ) )
| ~ ! [X14] :
( ~ r1(X0,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( ( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) )
| ~ p1(X19) ) )
| ~ ! [X21] :
( ~ r1(X16,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) )
| ~ p1(X21)
| ~ ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ~ ( ! [X26] :
( ~ r1(X23,X26)
| p1(X26) )
| ~ p1(X23) ) ) ) )
& ( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p1(X28) ) )
| ~ ! [X29] :
( ~ r1(X16,X29)
| p1(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X16,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ~ ! [X35] :
( ~ r1(X32,X35)
| p1(X35) ) )
& ( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| p1(X39) )
| ~ p1(X38) ) ) )
| ~ ! [X40] :
( ~ r1(X16,X40)
| p1(X40)
| ~ ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) )
| ~ p1(X41) ) ) ) ) ) ) )
| ~ ( ~ ! [X43] :
( ~ r1(X0,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p1(X46) )
| ! [X47] :
( ~ r1(X45,X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| p1(X48) ) )
| ~ ! [X49] :
( ~ r1(X45,X49)
| p1(X49)
| ~ ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p1(X51) )
| ~ p1(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ( ( p1(X53)
| ! [X54] :
( ~ r1(X53,X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| p1(X55) ) )
| ~ ! [X56] :
( ~ r1(X53,X56)
| p1(X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57) ) ) )
& ! [X59] :
( ~ r1(X53,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ~ ! [X62] :
( ~ r1(X59,X62)
| p1(X62) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ( ( p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| ~ ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ~ ! [X66] :
( ~ r1(X63,X66)
| p1(X66)
| ~ ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| p1(X68) )
| ~ p1(X67) ) ) )
& ! [X69] :
( ~ r1(X63,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p1(X71) ) )
| ~ ! [X72] :
( ~ r1(X69,X72)
| p1(X72) ) ) ) ) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( ( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ? [X6] :
( r1(X5,X6)
& ~ p1(X6) ) )
| ? [X7] :
( r1(X4,X7)
& ~ p1(X7)
& ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) ) )
& ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ? [X13] :
( r1(X10,X13)
& ~ p1(X13) ) ) ) ) ) ) )
& ! [X14] :
( ~ r1(X0,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( ( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| ? [X19] :
( r1(X18,X19)
& ? [X20] :
( r1(X19,X20)
& ~ p1(X20) )
& p1(X19) ) )
| ? [X21] :
( r1(X16,X21)
& ? [X22] :
( r1(X21,X22)
& ~ p1(X22) )
& p1(X21)
& ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ( ? [X26] :
( r1(X23,X26)
& ~ p1(X26) )
& p1(X23) ) ) ) )
& ( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X16,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X16,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) )
& ( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| ? [X38] :
( r1(X37,X38)
& ? [X39] :
( r1(X38,X39)
& ~ p1(X39) )
& p1(X38) ) ) )
| ? [X40] :
( r1(X16,X40)
& ~ p1(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) )
| ~ p1(X41) ) ) ) ) ) ) )
& ? [X43] :
( r1(X0,X43)
& ? [X44] :
( r1(X43,X44)
& ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ~ p1(X46) )
& ? [X47] :
( r1(X45,X47)
& ! [X48] :
( ~ r1(X47,X48)
| p1(X48) ) )
& ! [X49] :
( ~ r1(X45,X49)
| p1(X49)
| ? [X50] :
( r1(X49,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p1(X51) )
& p1(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ( ( p1(X53)
| ! [X54] :
( ~ r1(X53,X54)
| ? [X55] :
( r1(X54,X55)
& ~ p1(X55) ) )
| ? [X56] :
( r1(X53,X56)
& ~ p1(X56)
& ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57) ) ) )
& ! [X59] :
( ~ r1(X53,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ( ( p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| ? [X65] :
( r1(X64,X65)
& ~ p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66)
& ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| p1(X68) )
| ~ p1(X67) ) ) )
& ! [X69] :
( ~ r1(X63,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p1(X71) ) )
| ? [X72] :
( r1(X69,X72)
& ~ p1(X72) ) ) ) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( ( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ? [X6] :
( r1(X5,X6)
& ~ p1(X6) ) )
| ? [X7] :
( r1(X4,X7)
& ~ p1(X7)
& ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) ) )
& ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ? [X13] :
( r1(X10,X13)
& ~ p1(X13) ) ) ) ) ) ) )
& ! [X14] :
( ~ r1(X0,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( ( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| ? [X19] :
( r1(X18,X19)
& ? [X20] :
( r1(X19,X20)
& ~ p1(X20) )
& p1(X19) ) )
| ? [X21] :
( r1(X16,X21)
& ? [X22] :
( r1(X21,X22)
& ~ p1(X22) )
& p1(X21)
& ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ( ? [X26] :
( r1(X23,X26)
& ~ p1(X26) )
& p1(X23) ) ) ) )
& ( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X16,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X16,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) )
& ( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| ? [X38] :
( r1(X37,X38)
& ? [X39] :
( r1(X38,X39)
& ~ p1(X39) )
& p1(X38) ) ) )
| ? [X40] :
( r1(X16,X40)
& ~ p1(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) )
| ~ p1(X41) ) ) ) ) ) ) )
& ? [X43] :
( r1(X0,X43)
& ? [X44] :
( r1(X43,X44)
& ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ~ p1(X46) )
& ? [X47] :
( r1(X45,X47)
& ! [X48] :
( ~ r1(X47,X48)
| p1(X48) ) )
& ! [X49] :
( ~ r1(X45,X49)
| p1(X49)
| ? [X50] :
( r1(X49,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p1(X51) )
& p1(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ( ( p1(X53)
| ! [X54] :
( ~ r1(X53,X54)
| ? [X55] :
( r1(X54,X55)
& ~ p1(X55) ) )
| ? [X56] :
( r1(X53,X56)
& ~ p1(X56)
& ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57) ) ) )
& ! [X59] :
( ~ r1(X53,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ( ( p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| ? [X65] :
( r1(X64,X65)
& ~ p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66)
& ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| p1(X68) )
| ~ p1(X67) ) ) )
& ! [X69] :
( ~ r1(X63,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p1(X71) ) )
| ? [X72] :
( r1(X69,X72)
& ~ p1(X72) ) ) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,definition,
! [X16] :
( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| ? [X38] :
( r1(X37,X38)
& ? [X39] :
( r1(X38,X39)
& ~ p1(X39) )
& p1(X38) ) ) )
| ~ sP0(X16) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X16] :
( ? [X21] :
( r1(X16,X21)
& ? [X22] :
( r1(X21,X22)
& ~ p1(X22) )
& p1(X21)
& ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ( ? [X26] :
( r1(X23,X26)
& ~ p1(X26) )
& p1(X23) ) ) )
| ~ sP1(X16) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X16] :
( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X16,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) )
| ~ sP2(X16) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X16] :
( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| ? [X19] :
( r1(X18,X19)
& ? [X20] :
( r1(X19,X20)
& ~ p1(X20) )
& p1(X19) ) )
| sP1(X16)
| ~ sP3(X16) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( ( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ? [X6] :
( r1(X5,X6)
& ~ p1(X6) ) )
| ? [X7] :
( r1(X4,X7)
& ~ p1(X7)
& ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) ) )
& ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ? [X13] :
( r1(X10,X13)
& ~ p1(X13) ) ) ) ) ) ) )
& ! [X14] :
( ~ r1(X0,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( sP3(X16)
& sP2(X16)
& ! [X32] :
( ~ r1(X16,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) )
& ( sP0(X16)
| ? [X40] :
( r1(X16,X40)
& ~ p1(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) )
| ~ p1(X41) ) ) ) ) ) ) )
& ? [X43] :
( r1(X0,X43)
& ? [X44] :
( r1(X43,X44)
& ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ~ p1(X46) )
& ? [X47] :
( r1(X45,X47)
& ! [X48] :
( ~ r1(X47,X48)
| p1(X48) ) )
& ! [X49] :
( ~ r1(X45,X49)
| p1(X49)
| ? [X50] :
( r1(X49,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p1(X51) )
& p1(X50) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ( ( p1(X53)
| ! [X54] :
( ~ r1(X53,X54)
| ? [X55] :
( r1(X54,X55)
& ~ p1(X55) ) )
| ? [X56] :
( r1(X53,X56)
& ~ p1(X56)
& ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57) ) ) )
& ! [X59] :
( ~ r1(X53,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ( ( p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| ? [X65] :
( r1(X64,X65)
& ~ p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66)
& ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| p1(X68) )
| ~ p1(X67) ) ) )
& ! [X69] :
( ~ r1(X63,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p1(X71) ) )
| ? [X72] :
( r1(X69,X72)
& ~ p1(X72) ) ) ) ) ),
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f12,plain,
! [X16] :
( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| ? [X19] :
( r1(X18,X19)
& ? [X20] :
( r1(X19,X20)
& ~ p1(X20) )
& p1(X19) ) )
| sP1(X16)
| ~ sP3(X16) ),
inference(nnf_transformation,[],[f10]) ).
fof(f13,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(rectify,[],[f12]) ).
fof(f14,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ( r1(X2,sK4(X2))
& r1(sK4(X2),sK5(X2))
& ~ p1(sK5(X2))
& p1(sK4(X2)) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X2)),skolemize(X4,sK5(X2))],[f13]) ).
fof(f15,plain,
! [X16] :
( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X16,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) )
| ~ sP2(X16) ),
inference(nnf_transformation,[],[f9]) ).
fof(f16,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ? [X2] :
( r1(X1,X2)
& ~ p1(X2) ) )
| ? [X3] :
( r1(X0,X3)
& ~ p1(X3)
& ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f15]) ).
fof(f17,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( r1(X1,sK6(X1))
& ~ p1(sK6(X1)) ) )
| ( r1(X0,sK7(X0))
& ~ p1(sK7(X0))
& ! [X4] :
( ~ r1(sK7(X0),X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X2,sK6(X1)),skolemize(X3,sK7(X0))],[f16]) ).
fof(f18,plain,
! [X16] :
( ? [X21] :
( r1(X16,X21)
& ? [X22] :
( r1(X21,X22)
& ~ p1(X22) )
& p1(X21)
& ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ( ? [X26] :
( r1(X23,X26)
& ~ p1(X26) )
& p1(X23) ) ) )
| ~ sP1(X16) ),
inference(nnf_transformation,[],[f8]) ).
fof(f19,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p1(X2) )
& p1(X1)
& ! [X3] :
( ~ r1(X1,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( ? [X6] :
( r1(X3,X6)
& ~ p1(X6) )
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f18]) ).
fof(f20,plain,
! [X0] :
( ( r1(X0,sK8(X0))
& r1(sK8(X0),sK9(X0))
& ~ p1(sK9(X0))
& p1(sK8(X0))
& ! [X3] :
( ~ r1(sK8(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( r1(X3,sK10(X3))
& ~ p1(sK10(X3))
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0)),skolemize(X6,sK10(X3))],[f19]) ).
fof(f21,plain,
! [X16] :
( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| ? [X38] :
( r1(X37,X38)
& ? [X39] :
( r1(X38,X39)
& ~ p1(X39) )
& p1(X38) ) ) )
| ~ sP0(X16) ),
inference(nnf_transformation,[],[f7]) ).
fof(f22,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ( r1(X2,sK11(X2))
& r1(sK11(X2),sK12(X2))
& ~ p1(sK12(X2))
& p1(sK11(X2)) ) ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f22]) ).
fof(f24,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( ( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ? [X6] :
( r1(X5,X6)
& ~ p1(X6) ) )
| ? [X7] :
( r1(X4,X7)
& ~ p1(X7)
& ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) ) )
& ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ? [X13] :
( r1(X10,X13)
& ~ p1(X13) ) ) ) ) ) ) )
& ! [X14] :
( ~ r1(X0,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( sP3(X16)
& sP2(X16)
& ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) ) )
| ? [X20] :
( r1(X17,X20)
& ~ p1(X20) ) )
& ( sP0(X16)
| ? [X21] :
( r1(X16,X21)
& ~ p1(X21)
& ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p1(X23) )
| ~ p1(X22) ) ) ) ) ) ) )
& ? [X24] :
( r1(X0,X24)
& ? [X25] :
( r1(X24,X25)
& ? [X26] :
( r1(X25,X26)
& ? [X27] :
( r1(X26,X27)
& ~ p1(X27) )
& ? [X28] :
( r1(X26,X28)
& ! [X29] :
( ~ r1(X28,X29)
| p1(X29) ) )
& ! [X30] :
( ~ r1(X26,X30)
| p1(X30)
| ? [X31] :
( r1(X30,X31)
& ? [X32] :
( r1(X31,X32)
& ~ p1(X32) )
& p1(X31) ) ) ) ) )
& ! [X33] :
( ~ r1(X0,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ( ( p1(X34)
| ! [X35] :
( ~ r1(X34,X35)
| ? [X36] :
( r1(X35,X36)
& ~ p1(X36) ) )
| ? [X37] :
( r1(X34,X37)
& ~ p1(X37)
& ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| p1(X39) )
| ~ p1(X38) ) ) )
& ! [X40] :
( ~ r1(X34,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) ) )
| ? [X43] :
( r1(X40,X43)
& ~ p1(X43) ) ) ) ) )
& ! [X44] :
( ~ r1(X0,X44)
| ( ( p1(X44)
| ! [X45] :
( ~ r1(X44,X45)
| ? [X46] :
( r1(X45,X46)
& ~ p1(X46) ) )
| ? [X47] :
( r1(X44,X47)
& ~ p1(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p1(X49) )
| ~ p1(X48) ) ) )
& ! [X50] :
( ~ r1(X44,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| p1(X52) ) )
| ? [X53] :
( r1(X50,X53)
& ~ p1(X53) ) ) ) ) ),
inference(rectify,[],[f11]) ).
fof(f25,plain,
( ! [X1] :
( ~ r1(sK13,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( ( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ( r1(X5,sK14(X5))
& ~ p1(sK14(X5)) ) )
| ( r1(X4,sK15(X4))
& ~ p1(sK15(X4))
& ! [X8] :
( ~ r1(sK15(X4),X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) ) )
& ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ( r1(X10,sK16(X10))
& ~ p1(sK16(X10)) ) ) ) ) ) ) )
& ! [X14] :
( ~ r1(sK13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( sP3(X16)
& sP2(X16)
& ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) ) )
| ( r1(X17,sK17(X17))
& ~ p1(sK17(X17)) ) )
& ( sP0(X16)
| ( r1(X16,sK18(X16))
& ~ p1(sK18(X16))
& ! [X22] :
( ~ r1(sK18(X16),X22)
| ! [X23] :
( ~ r1(X22,X23)
| p1(X23) )
| ~ p1(X22) ) ) ) ) ) ) )
& r1(sK13,sK19)
& r1(sK19,sK20)
& r1(sK20,sK21)
& r1(sK21,sK22)
& ~ p1(sK22)
& r1(sK21,sK23)
& ! [X29] :
( ~ r1(sK23,X29)
| p1(X29) )
& ! [X30] :
( ~ r1(sK21,X30)
| p1(X30)
| ( r1(X30,sK24(X30))
& r1(sK24(X30),sK25(X30))
& ~ p1(sK25(X30))
& p1(sK24(X30)) ) )
& ! [X33] :
( ~ r1(sK13,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ( ( p1(X34)
| ! [X35] :
( ~ r1(X34,X35)
| ( r1(X35,sK26(X35))
& ~ p1(sK26(X35)) ) )
| ( r1(X34,sK27(X34))
& ~ p1(sK27(X34))
& ! [X38] :
( ~ r1(sK27(X34),X38)
| ! [X39] :
( ~ r1(X38,X39)
| p1(X39) )
| ~ p1(X38) ) ) )
& ! [X40] :
( ~ r1(X34,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) ) )
| ( r1(X40,sK28(X40))
& ~ p1(sK28(X40)) ) ) ) ) )
& ! [X44] :
( ~ r1(sK13,X44)
| ( ( p1(X44)
| ! [X45] :
( ~ r1(X44,X45)
| ( r1(X45,sK29(X45))
& ~ p1(sK29(X45)) ) )
| ( r1(X44,sK30(X44))
& ~ p1(sK30(X44))
& ! [X48] :
( ~ r1(sK30(X44),X48)
| ! [X49] :
( ~ r1(X48,X49)
| p1(X49) )
| ~ p1(X48) ) ) )
& ! [X50] :
( ~ r1(X44,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| p1(X52) ) )
| ( r1(X50,sK31(X50))
& ~ p1(sK31(X50)) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31]),skolemize(X0,sK13),skolemize(X6,sK14(X5)),skolemize(X7,sK15(X4)),skolemize(X13,sK16(X10)),skolemize(X20,sK17(X17)),skolemize(X21,sK18(X16)),skolemize(X24,sK19),skolemize(X25,sK20),skolemize(X26,sK21),skolemize(X27,sK22),skolemize(X28,sK23),skolemize(X31,sK24(X30)),skolemize(X32,sK25(X30)),skolemize(X36,sK26(X35)),skolemize(X37,sK27(X34)),skolemize(X43,sK28(X40)),skolemize(X46,sK29(X45)),skolemize(X47,sK30(X44)),skolemize(X53,sK31(X50))],[f24]) ).
fof(f27,plain,
! [X2,X0,X1] :
( ~ p1(sK5(X2))
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1)
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f28,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(sK4(X2),sK5(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(X2,sK4(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f30,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f31,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
! [X0,X1] :
( ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0)
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f33,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f34,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f35,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| p1(X0)
| r1(X1,sK6(X1))
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f36,plain,
! [X3,X0,X4,X5] :
( ~ r1(sK8(X0),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| p1(X3)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f40,plain,
! [X0] :
( ~ p1(sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f41,plain,
! [X0] :
( r1(sK8(X0),sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f42,plain,
! [X0] :
( r1(X0,sK8(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| p1(sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f44,plain,
! [X2,X0,X1] :
( ~ p1(sK12(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(sK11(X2),sK12(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(X2,sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f63,plain,
! [X30] :
( ~ r1(sK21,X30)
| p1(X30)
| p1(sK24(X30)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f64,plain,
! [X30] :
( ~ p1(sK25(X30))
| p1(X30)
| ~ r1(sK21,X30) ),
inference(cnf_transformation,[],[f25]) ).
fof(f65,plain,
! [X30] :
( r1(sK24(X30),sK25(X30))
| p1(X30)
| ~ r1(sK21,X30) ),
inference(cnf_transformation,[],[f25]) ).
fof(f66,plain,
! [X30] :
( r1(X30,sK24(X30))
| p1(X30)
| ~ r1(sK21,X30) ),
inference(cnf_transformation,[],[f25]) ).
fof(f67,plain,
! [X29] :
( ~ r1(sK23,X29)
| p1(X29) ),
inference(cnf_transformation,[],[f25]) ).
fof(f68,plain,
r1(sK21,sK23),
inference(cnf_transformation,[],[f25]) ).
fof(f69,plain,
~ p1(sK22),
inference(cnf_transformation,[],[f25]) ).
fof(f70,plain,
r1(sK21,sK22),
inference(cnf_transformation,[],[f25]) ).
fof(f71,plain,
r1(sK20,sK21),
inference(cnf_transformation,[],[f25]) ).
fof(f72,plain,
r1(sK19,sK20),
inference(cnf_transformation,[],[f25]) ).
fof(f73,plain,
r1(sK13,sK19),
inference(cnf_transformation,[],[f25]) ).
fof(f74,plain,
! [X16,X14,X15,X22,X23] :
( ~ r1(sK18(X16),X22)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| sP0(X16)
| ~ r1(sK13,X14)
| ~ r1(X22,X23)
| p1(X23)
| ~ p1(X22) ),
inference(cnf_transformation,[],[f25]) ).
fof(f75,plain,
! [X16,X14,X15] :
( ~ p1(sK18(X16))
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| sP0(X16)
| ~ r1(sK13,X14) ),
inference(cnf_transformation,[],[f25]) ).
fof(f76,plain,
! [X16,X14,X15] :
( ~ r1(sK13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| sP0(X16)
| r1(X16,sK18(X16)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f77,plain,
! [X18,X19,X16,X14,X17,X15] :
( ~ p1(sK17(X17))
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| p1(X19)
| ~ r1(sK13,X14) ),
inference(cnf_transformation,[],[f25]) ).
fof(f78,plain,
! [X18,X19,X16,X14,X17,X15] :
( ~ r1(sK13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| ~ r1(X18,X19)
| p1(X19)
| r1(X17,sK17(X17)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f79,plain,
! [X16,X14,X15] :
( ~ r1(sK13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| sP2(X16) ),
inference(cnf_transformation,[],[f25]) ).
fof(f80,plain,
! [X16,X14,X15] :
( ~ r1(sK13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| sP3(X16) ),
inference(cnf_transformation,[],[f25]) ).
fof(f93,plain,
( p1(sK21)
| r1(sK23,sK6(sK23))
| r1(sK21,sK7(sK21))
| ~ sP2(sK21) ),
inference(resolution,[],[f35,f68]) ).
fof(f95,definition,
( spl32_1
<=> sP2(sK21) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
fof(f96,plain,
( sP2(sK21)
| ~ spl32_1 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f97,plain,
( ~ sP2(sK21)
| spl32_1 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f99,definition,
( spl32_2
<=> r1(sK21,sK7(sK21)) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
fof(f101,plain,
( r1(sK21,sK7(sK21))
| ~ spl32_2 ),
inference(avatar_component_clause,[],[f99]) ).
fof(f103,definition,
( spl32_3
<=> r1(sK23,sK6(sK23)) ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
fof(f104,plain,
( ~ r1(sK23,sK6(sK23))
| spl32_3 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f105,plain,
( r1(sK23,sK6(sK23))
| ~ spl32_3 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f107,definition,
( spl32_4
<=> p1(sK21) ),
introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition]) ).
fof(f108,plain,
( ~ p1(sK21)
| spl32_4 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f109,plain,
( p1(sK21)
| ~ spl32_4 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f110,plain,
( ~ spl32_1
| spl32_2
| spl32_3
| spl32_4 ),
inference(avatar_split_clause,[],[f93,f107,f103,f99,f95]) ).
fof(f214,plain,
! [X0,X1] :
( ~ r1(sK19,X0)
| ~ r1(X0,X1)
| sP2(X1) ),
inference(resolution,[],[f79,f73]) ).
fof(f215,plain,
! [X0,X1] :
( ~ r1(sK19,X0)
| ~ r1(X0,X1)
| sP3(X1) ),
inference(resolution,[],[f80,f73]) ).
fof(f230,plain,
! [X0] :
( p1(X0)
| ~ p1(sK21)
| ~ r1(sK21,X0)
| r1(sK23,sK4(sK23))
| sP1(sK21)
| ~ sP3(sK21) ),
inference(resolution,[],[f29,f68]) ).
fof(f231,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK21,X0)
| r1(sK23,sK4(sK23))
| sP1(sK21)
| ~ sP3(sK21) )
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f230,f109]) ).
fof(f252,definition,
( spl32_32
<=> sP3(sK21) ),
introduced(definition,[new_symbols(definition,[spl32_32])],[avatar_definition]) ).
fof(f253,plain,
( sP3(sK21)
| ~ spl32_32 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( ~ sP3(sK21)
| spl32_32 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f256,definition,
( spl32_33
<=> sP1(sK21) ),
introduced(definition,[new_symbols(definition,[spl32_33])],[avatar_definition]) ).
fof(f257,plain,
( ~ sP1(sK21)
| spl32_33 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( sP1(sK21)
| ~ spl32_33 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f260,definition,
( spl32_34
<=> r1(sK23,sK4(sK23)) ),
introduced(definition,[new_symbols(definition,[spl32_34])],[avatar_definition]) ).
fof(f262,plain,
( r1(sK23,sK4(sK23))
| ~ spl32_34 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f264,definition,
( spl32_35
<=> ! [X0] :
( p1(X0)
| ~ r1(sK21,X0) ) ),
introduced(definition,[new_symbols(definition,[spl32_35])],[avatar_definition]) ).
fof(f265,plain,
( ! [X0] :
( ~ r1(sK21,X0)
| p1(X0) )
| ~ spl32_35 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( ~ spl32_32
| spl32_33
| spl32_34
| spl32_35
| ~ spl32_4 ),
inference(avatar_split_clause,[],[f231,f107,f264,f260,f256,f252]) ).
fof(f304,plain,
! [X0,X1] :
( ~ r1(sK19,X0)
| ~ r1(X0,X1)
| sP0(X1)
| r1(X1,sK18(X1)) ),
inference(resolution,[],[f76,f73]) ).
fof(f310,plain,
! [X2,X0,X1] :
( p1(sK7(X0))
| ~ r1(sK21,sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK24(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK24(sK7(X0)))
| ~ sP2(X0) ),
inference(resolution,[],[f66,f33]) ).
fof(f321,plain,
! [X2,X0,X1] :
( p1(sK7(X0))
| ~ r1(sK21,sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK24(sK7(X0)),X2)
| p1(X2)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f310,f63]) ).
fof(f338,plain,
! [X2,X0,X1] :
( ~ r1(sK24(sK7(X0)),X2)
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK21,sK7(X0))
| p1(X2)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f321,f34]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ sP1(X0)
| ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(sK9(X0))
| ~ sP1(X0) ),
inference(resolution,[],[f41,f36]) ).
fof(f342,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f43]) ).
fof(f343,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f45]) ).
fof(f344,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f46]) ).
fof(f346,plain,
! [X2,X0,X1] :
( ~ sP1(X0)
| ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(sK9(X0)) ),
inference(duplicate_literal_removal,[],[f340]) ).
fof(f348,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f344,f40]) ).
fof(f349,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f343,f40]) ).
fof(f350,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f342,f40]) ).
fof(f352,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ sP1(X0)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1) ),
inference(forward_subsumption_resolution,[],[f346,f40]) ).
fof(f385,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(sK24(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK24(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK21,sK7(X0)) ),
inference(resolution,[],[f30,f66]) ).
fof(f388,plain,
! [X2,X0,X1] :
( ~ r1(sK24(sK7(X0)),X2)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK24(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK21,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f385,f31]) ).
fof(f404,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f349,f42]) ).
fof(f405,plain,
! [X0] :
( r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f404]) ).
fof(f411,plain,
! [X0] :
( ~ r1(sK20,X0)
| sP2(X0) ),
inference(resolution,[],[f214,f72]) ).
fof(f418,plain,
sP2(sK21),
inference(resolution,[],[f411,f71]) ).
fof(f426,plain,
( $false
| spl32_1 ),
inference(forward_subsumption_resolution,[],[f418,f97]) ).
fof(f427,plain,
spl32_1,
inference(avatar_contradiction_clause,[],[f426]) ).
fof(f435,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK19,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK17(X2)) ),
inference(resolution,[],[f78,f73]) ).
fof(f438,plain,
! [X0] :
( ~ r1(sK20,X0)
| sP3(X0) ),
inference(resolution,[],[f215,f72]) ).
fof(f441,plain,
sP3(sK21),
inference(resolution,[],[f438,f71]) ).
fof(f444,plain,
( $false
| spl32_32 ),
inference(forward_subsumption_resolution,[],[f441,f254]) ).
fof(f445,plain,
spl32_32,
inference(avatar_contradiction_clause,[],[f444]) ).
fof(f447,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK21,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(sK25(sK7(X0)))
| ~ p1(sK24(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK21,sK7(X0)) ),
inference(resolution,[],[f65,f388]) ).
fof(f453,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK21,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(sK25(sK7(X0)))
| ~ p1(sK24(sK7(X0)))
| ~ sP2(X0) ),
inference(duplicate_literal_removal,[],[f447]) ).
fof(f459,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK21,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| ~ p1(sK24(sK7(X0)))
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f453,f64]) ).
fof(f461,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK21,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f459,f63]) ).
fof(f463,plain,
! [X0,X1] :
( ~ r1(sK21,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f461,f31]) ).
fof(f464,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK21,sK7(X0))
| p1(sK25(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK21,sK7(X0)) ),
inference(resolution,[],[f338,f65]) ).
fof(f467,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK21,sK7(X0))
| p1(sK25(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0)) ),
inference(duplicate_literal_removal,[],[f464]) ).
fof(f468,plain,
! [X0,X1] :
( ~ r1(sK21,sK7(X0))
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(sK25(sK7(X0)))
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f467,f34]) ).
fof(f469,plain,
! [X0] :
( ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f350,f42]) ).
fof(f470,plain,
! [X0] :
( p1(sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f469]) ).
fof(f479,plain,
! [X0] :
( p1(X0)
| ~ p1(sK21)
| ~ r1(sK21,X0)
| r1(sK4(sK23),sK5(sK23))
| sP1(sK21)
| ~ sP3(sK21) ),
inference(resolution,[],[f28,f68]) ).
fof(f484,plain,
! [X2,X3,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP0(X2)
| ~ r1(sK13,X0)
| ~ r1(sK24(sK18(X2)),X3)
| p1(X3)
| ~ p1(sK24(sK18(X2)))
| p1(sK18(X2))
| ~ r1(sK21,sK18(X2)) ),
inference(resolution,[],[f74,f66]) ).
fof(f487,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK24(sK18(X2)),X3)
| ~ r1(X1,X2)
| sP0(X2)
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(X3)
| ~ p1(sK24(sK18(X2)))
| ~ r1(sK21,sK18(X2)) ),
inference(forward_subsumption_resolution,[],[f484,f75]) ).
fof(f488,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| sP0(X1)
| ~ r1(sK13,X2)
| ~ r1(X2,X0)
| p1(sK25(sK18(X1)))
| ~ p1(sK24(sK18(X1)))
| ~ r1(sK21,sK18(X1))
| p1(sK18(X1))
| ~ r1(sK21,sK18(X1)) ),
inference(resolution,[],[f487,f65]) ).
fof(f491,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| sP0(X1)
| ~ r1(sK13,X2)
| ~ r1(X2,X0)
| p1(sK25(sK18(X1)))
| ~ p1(sK24(sK18(X1)))
| ~ r1(sK21,sK18(X1))
| p1(sK18(X1)) ),
inference(duplicate_literal_removal,[],[f488]) ).
fof(f492,plain,
! [X2,X0,X1] :
( ~ p1(sK24(sK18(X1)))
| sP0(X1)
| ~ r1(sK13,X2)
| ~ r1(X2,X0)
| p1(sK25(sK18(X1)))
| ~ r1(X0,X1)
| ~ r1(sK21,sK18(X1)) ),
inference(forward_subsumption_resolution,[],[f491,f75]) ).
fof(f493,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f348,f42]) ).
fof(f494,plain,
! [X0] :
( r1(sK9(X0),sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f493]) ).
fof(f495,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ sP1(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0))) ),
inference(resolution,[],[f494,f352]) ).
fof(f502,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0))) ),
inference(duplicate_literal_removal,[],[f495]) ).
fof(f504,plain,
! [X0,X1] :
( ~ r1(sK11(sK9(X0)),X1)
| ~ sP0(X0)
| ~ sP1(X0)
| p1(X1) ),
inference(forward_subsumption_resolution,[],[f502,f470]) ).
fof(f505,plain,
! [X0] :
( ~ sP0(X0)
| ~ sP1(X0)
| p1(sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(resolution,[],[f504,f405]) ).
fof(f508,plain,
! [X0] :
( p1(sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f505]) ).
fof(f509,plain,
! [X2,X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(X1,sK9(X0))
| p1(sK9(X0))
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(resolution,[],[f508,f44]) ).
fof(f510,plain,
! [X2,X0,X1] :
( ~ r1(X1,sK9(X0))
| ~ sP0(X0)
| ~ sP1(X0)
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(forward_subsumption_resolution,[],[f509,f40]) ).
fof(f511,plain,
! [X0,X1] :
( ~ sP0(X0)
| ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| ~ sP0(X1)
| ~ sP1(X0) ),
inference(resolution,[],[f510,f41]) ).
fof(f512,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| ~ sP0(X0)
| ~ sP0(X1) ),
inference(duplicate_literal_removal,[],[f511]) ).
fof(f513,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f512,f42]) ).
fof(f514,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f513]) ).
fof(f515,plain,
( ~ sP0(sK21)
| ~ spl32_33 ),
inference(resolution,[],[f514,f258]) ).
fof(f663,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK20,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK17(X1)) ),
inference(resolution,[],[f435,f72]) ).
fof(f666,plain,
! [X2,X0,X1] :
( ~ r1(sK21,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK17(X0)) ),
inference(resolution,[],[f663,f71]) ).
fof(f670,plain,
! [X0,X1] :
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK23,sK17(sK23)) ),
inference(resolution,[],[f666,f68]) ).
fof(f675,definition,
( spl32_75
<=> r1(sK23,sK17(sK23)) ),
introduced(definition,[new_symbols(definition,[spl32_75])],[avatar_definition]) ).
fof(f677,plain,
( r1(sK23,sK17(sK23))
| ~ spl32_75 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f679,definition,
( spl32_76
<=> ! [X0,X1] :
( ~ r1(sK23,X0)
| p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl32_76])],[avatar_definition]) ).
fof(f680,plain,
( ! [X0,X1] :
( ~ r1(sK23,X0)
| p1(X1)
| ~ r1(X0,X1) )
| ~ spl32_76 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f681,plain,
( spl32_75
| spl32_76 ),
inference(avatar_split_clause,[],[f670,f679,f675]) ).
fof(f698,plain,
( p1(sK22)
| ~ spl32_35 ),
inference(resolution,[],[f265,f70]) ).
fof(f702,plain,
( $false
| ~ spl32_35 ),
inference(forward_subsumption_resolution,[],[f698,f69]) ).
fof(f703,plain,
~ spl32_35,
inference(avatar_contradiction_clause,[],[f702]) ).
fof(f786,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK21,X0)
| r1(sK4(sK23),sK5(sK23))
| sP1(sK21)
| ~ sP3(sK21) )
| ~ spl32_4 ),
inference(forward_subsumption_resolution,[],[f479,f109]) ).
fof(f790,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK21,X0)
| r1(sK4(sK23),sK5(sK23))
| ~ sP3(sK21) )
| ~ spl32_4
| spl32_33 ),
inference(forward_subsumption_resolution,[],[f786,f257]) ).
fof(f794,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK21,X0)
| r1(sK4(sK23),sK5(sK23)) )
| ~ spl32_4
| ~ spl32_32
| spl32_33 ),
inference(forward_subsumption_resolution,[],[f790,f253]) ).
fof(f799,definition,
( spl32_97
<=> r1(sK4(sK23),sK5(sK23)) ),
introduced(definition,[new_symbols(definition,[spl32_97])],[avatar_definition]) ).
fof(f801,plain,
( r1(sK4(sK23),sK5(sK23))
| ~ spl32_97 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f802,plain,
( spl32_97
| spl32_35
| ~ spl32_4
| ~ spl32_32
| spl32_33 ),
inference(avatar_split_clause,[],[f794,f256,f252,f107,f264,f799]) ).
fof(f820,plain,
( p1(sK6(sK23))
| ~ spl32_3 ),
inference(resolution,[],[f105,f67]) ).
fof(f833,definition,
( spl32_102
<=> p1(sK6(sK23)) ),
introduced(definition,[new_symbols(definition,[spl32_102])],[avatar_definition]) ).
fof(f835,plain,
( p1(sK6(sK23))
| ~ spl32_102 ),
inference(avatar_component_clause,[],[f833]) ).
fof(f850,plain,
( spl32_102
| ~ spl32_3 ),
inference(avatar_split_clause,[],[f820,f103,f833]) ).
fof(f954,plain,
( p1(sK17(sK23))
| ~ spl32_75 ),
inference(resolution,[],[f677,f67]) ).
fof(f967,definition,
( spl32_123
<=> p1(sK17(sK23)) ),
introduced(definition,[new_symbols(definition,[spl32_123])],[avatar_definition]) ).
fof(f969,plain,
( p1(sK17(sK23))
| ~ spl32_123 ),
inference(avatar_component_clause,[],[f967]) ).
fof(f981,plain,
( spl32_123
| ~ spl32_75 ),
inference(avatar_split_clause,[],[f954,f675,f967]) ).
fof(f1055,plain,
! [X0] :
( r1(X0,sK18(X0))
| sP0(X0)
| ~ r1(sK20,X0) ),
inference(resolution,[],[f304,f72]) ).
fof(f1094,plain,
( sP0(sK21)
| ~ r1(sK20,sK21)
| p1(sK18(sK21))
| p1(sK24(sK18(sK21))) ),
inference(resolution,[],[f1055,f63]) ).
fof(f1285,definition,
( spl32_174
<=> p1(sK24(sK18(sK21))) ),
introduced(definition,[new_symbols(definition,[spl32_174])],[avatar_definition]) ).
fof(f1287,plain,
( p1(sK24(sK18(sK21)))
| ~ spl32_174 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1289,definition,
( spl32_175
<=> p1(sK18(sK21)) ),
introduced(definition,[new_symbols(definition,[spl32_175])],[avatar_definition]) ).
fof(f1290,plain,
( ~ p1(sK18(sK21))
| spl32_175 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1291,plain,
( p1(sK18(sK21))
| ~ spl32_175 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1309,plain,
( sP0(sK21)
| p1(sK18(sK21))
| p1(sK24(sK18(sK21))) ),
inference(forward_subsumption_resolution,[],[f1094,f71]) ).
fof(f1313,definition,
( spl32_178
<=> sP0(sK21) ),
introduced(definition,[new_symbols(definition,[spl32_178])],[avatar_definition]) ).
fof(f1314,plain,
( ~ sP0(sK21)
| spl32_178 ),
inference(avatar_component_clause,[],[f1313]) ).
fof(f1316,plain,
( spl32_174
| spl32_175
| spl32_178 ),
inference(avatar_split_clause,[],[f1309,f1313,f1289,f1285]) ).
fof(f1431,definition,
( spl32_185
<=> p1(sK7(sK21)) ),
introduced(definition,[new_symbols(definition,[spl32_185])],[avatar_definition]) ).
fof(f1432,plain,
( ~ p1(sK7(sK21))
| spl32_185 ),
inference(avatar_component_clause,[],[f1431]) ).
fof(f1433,plain,
( p1(sK7(sK21))
| ~ spl32_185 ),
inference(avatar_component_clause,[],[f1431]) ).
fof(f1525,plain,
( ! [X0] :
( ~ r1(sK4(sK23),X0)
| p1(X0) )
| ~ spl32_34
| ~ spl32_76 ),
inference(resolution,[],[f262,f680]) ).
fof(f1547,definition,
( spl32_190
<=> p1(sK5(sK23)) ),
introduced(definition,[new_symbols(definition,[spl32_190])],[avatar_definition]) ).
fof(f1549,plain,
( p1(sK5(sK23))
| ~ spl32_190 ),
inference(avatar_component_clause,[],[f1547]) ).
fof(f1700,definition,
( spl32_220
<=> ! [X0,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X1,sK21) ) ),
introduced(definition,[new_symbols(definition,[spl32_220])],[avatar_definition]) ).
fof(f1701,plain,
( ! [X0,X1] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK21) )
| ~ spl32_220 ),
inference(avatar_component_clause,[],[f1700]) ).
fof(f1707,definition,
( spl32_221
<=> r1(sK21,sK18(sK21)) ),
introduced(definition,[new_symbols(definition,[spl32_221])],[avatar_definition]) ).
fof(f1708,plain,
( r1(sK21,sK18(sK21))
| ~ spl32_221 ),
inference(avatar_component_clause,[],[f1707]) ).
fof(f1709,plain,
( ~ r1(sK21,sK18(sK21))
| spl32_221 ),
inference(avatar_component_clause,[],[f1707]) ).
fof(f1730,plain,
( sP0(sK21)
| ~ r1(sK20,sK21)
| spl32_221 ),
inference(resolution,[],[f1709,f1055]) ).
fof(f1731,plain,
( ~ r1(sK20,sK21)
| spl32_178
| spl32_221 ),
inference(forward_subsumption_resolution,[],[f1730,f1314]) ).
fof(f1732,plain,
( $false
| spl32_178
| spl32_221 ),
inference(forward_subsumption_resolution,[],[f1731,f71]) ).
fof(f1733,plain,
( spl32_178
| spl32_221 ),
inference(avatar_contradiction_clause,[],[f1732]) ).
fof(f1763,plain,
( ! [X0,X1] :
( sP0(sK21)
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(sK25(sK18(sK21)))
| ~ r1(X1,sK21)
| ~ r1(sK21,sK18(sK21)) )
| ~ spl32_174 ),
inference(resolution,[],[f1287,f492]) ).
fof(f1967,plain,
( p1(sK5(sK23))
| ~ spl32_34
| ~ spl32_76
| ~ spl32_97 ),
inference(resolution,[],[f1525,f801]) ).
fof(f2015,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK23)
| ~ r1(sK23,X3)
| ~ r1(X3,X4)
| p1(X4)
| ~ r1(sK13,X0) )
| ~ spl32_123 ),
inference(resolution,[],[f969,f77]) ).
fof(f2017,definition,
( spl32_266
<=> ! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X2,sK23)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl32_266])],[avatar_definition]) ).
fof(f2018,plain,
( ! [X2,X0,X1] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK23)
| ~ r1(X1,X2) )
| ~ spl32_266 ),
inference(avatar_component_clause,[],[f2017]) ).
fof(f2019,plain,
( spl32_76
| spl32_266
| ~ spl32_123 ),
inference(avatar_split_clause,[],[f2015,f967,f2017,f679]) ).
fof(f2020,plain,
( ! [X0,X1] :
( ~ r1(sK19,X0)
| ~ r1(X1,sK23)
| ~ r1(X0,X1) )
| ~ spl32_266 ),
inference(resolution,[],[f2018,f73]) ).
fof(f2024,plain,
( ! [X0] :
( ~ r1(sK20,X0)
| ~ r1(X0,sK23) )
| ~ spl32_266 ),
inference(resolution,[],[f2020,f72]) ).
fof(f2028,plain,
( ~ r1(sK21,sK23)
| ~ spl32_266 ),
inference(resolution,[],[f2024,f71]) ).
fof(f2032,plain,
( $false
| ~ spl32_266 ),
inference(forward_subsumption_resolution,[],[f2028,f68]) ).
fof(f2033,plain,
~ spl32_266,
inference(avatar_contradiction_clause,[],[f2032]) ).
fof(f2035,plain,
( spl32_190
| ~ spl32_34
| ~ spl32_76
| ~ spl32_97 ),
inference(avatar_split_clause,[],[f1967,f799,f679,f260,f1547]) ).
fof(f2044,plain,
( ! [X0,X1] :
( ~ r1(X1,sK23)
| ~ p1(X1)
| p1(X0)
| ~ r1(X1,X0)
| sP1(X1)
| ~ sP3(X1) )
| ~ spl32_190 ),
inference(resolution,[],[f1549,f27]) ).
fof(f2052,plain,
( ! [X0] :
( ~ p1(sK21)
| p1(X0)
| ~ r1(sK21,X0)
| sP1(sK21)
| ~ sP3(sK21) )
| ~ spl32_190 ),
inference(resolution,[],[f2044,f68]) ).
fof(f2053,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK21,X0)
| sP1(sK21)
| ~ sP3(sK21) )
| ~ spl32_4
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f2052,f109]) ).
fof(f2054,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK21,X0)
| ~ sP3(sK21) )
| ~ spl32_4
| spl32_33
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f2053,f257]) ).
fof(f2055,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK21,X0) )
| ~ spl32_4
| ~ spl32_32
| spl32_33
| ~ spl32_190 ),
inference(forward_subsumption_resolution,[],[f2054,f253]) ).
fof(f2056,plain,
( spl32_35
| ~ spl32_4
| ~ spl32_32
| spl32_33
| ~ spl32_190 ),
inference(avatar_split_clause,[],[f2055,f1547,f256,f252,f107,f264]) ).
fof(f2057,plain,
( ~ spl32_178
| ~ spl32_33 ),
inference(avatar_split_clause,[],[f515,f256,f1313]) ).
fof(f2059,plain,
( ! [X0,X1] :
( sP0(sK21)
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(sK25(sK18(sK21)))
| ~ r1(X1,sK21) )
| ~ spl32_174 ),
inference(forward_subsumption_resolution,[],[f1763,f76]) ).
fof(f2061,plain,
( ! [X0,X1] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(sK25(sK18(sK21)))
| ~ r1(X1,sK21) )
| ~ spl32_174
| spl32_178 ),
inference(forward_subsumption_resolution,[],[f2059,f1314]) ).
fof(f2063,definition,
( spl32_267
<=> p1(sK25(sK18(sK21))) ),
introduced(definition,[new_symbols(definition,[spl32_267])],[avatar_definition]) ).
fof(f2065,plain,
( p1(sK25(sK18(sK21)))
| ~ spl32_267 ),
inference(avatar_component_clause,[],[f2063]) ).
fof(f2066,plain,
( spl32_267
| spl32_220
| ~ spl32_174
| spl32_178 ),
inference(avatar_split_clause,[],[f2061,f1313,f1285,f1700,f2063]) ).
fof(f2077,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,sK21)
| sP0(sK21)
| ~ r1(sK13,X0) )
| ~ spl32_175 ),
inference(resolution,[],[f1291,f75]) ).
fof(f2078,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,sK21)
| ~ r1(sK13,X0) )
| ~ spl32_175
| spl32_178 ),
inference(forward_subsumption_resolution,[],[f2077,f1314]) ).
fof(f2079,plain,
( spl32_220
| ~ spl32_175
| spl32_178 ),
inference(avatar_split_clause,[],[f2078,f1313,f1289,f1700]) ).
fof(f2091,plain,
( p1(sK18(sK21))
| ~ r1(sK21,sK18(sK21))
| ~ spl32_267 ),
inference(resolution,[],[f2065,f64]) ).
fof(f2092,plain,
( ~ r1(sK21,sK18(sK21))
| spl32_175
| ~ spl32_267 ),
inference(forward_subsumption_resolution,[],[f2091,f1290]) ).
fof(f2093,plain,
( $false
| spl32_175
| ~ spl32_221
| ~ spl32_267 ),
inference(forward_subsumption_resolution,[],[f2092,f1708]) ).
fof(f2094,plain,
( spl32_175
| ~ spl32_221
| ~ spl32_267 ),
inference(avatar_contradiction_clause,[],[f2093]) ).
fof(f2095,plain,
( ! [X0] :
( ~ r1(sK19,X0)
| ~ r1(X0,sK21) )
| ~ spl32_220 ),
inference(resolution,[],[f1701,f73]) ).
fof(f2099,plain,
( ~ r1(sK20,sK21)
| ~ spl32_220 ),
inference(resolution,[],[f2095,f72]) ).
fof(f2103,plain,
( $false
| ~ spl32_220 ),
inference(forward_subsumption_resolution,[],[f2099,f71]) ).
fof(f2104,plain,
~ spl32_220,
inference(avatar_contradiction_clause,[],[f2103]) ).
fof(f2122,plain,
( ! [X0] :
( ~ r1(sK21,X0)
| ~ p1(sK6(X0))
| p1(sK21)
| ~ sP2(sK21) )
| ~ spl32_185 ),
inference(resolution,[],[f1433,f31]) ).
fof(f2123,plain,
( ! [X0] :
( ~ r1(sK21,X0)
| r1(X0,sK6(X0))
| p1(sK21)
| ~ sP2(sK21) )
| ~ spl32_185 ),
inference(resolution,[],[f1433,f34]) ).
fof(f2124,plain,
( ! [X0] :
( ~ r1(sK21,X0)
| r1(X0,sK6(X0))
| ~ sP2(sK21) )
| spl32_4
| ~ spl32_185 ),
inference(forward_subsumption_resolution,[],[f2123,f108]) ).
fof(f2125,plain,
( ! [X0] :
( ~ r1(sK21,X0)
| ~ p1(sK6(X0))
| ~ sP2(sK21) )
| spl32_4
| ~ spl32_185 ),
inference(forward_subsumption_resolution,[],[f2122,f108]) ).
fof(f2126,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK21,X0) )
| ~ spl32_1
| spl32_4
| ~ spl32_185 ),
inference(forward_subsumption_resolution,[],[f2124,f96]) ).
fof(f2127,plain,
( ! [X0] :
( ~ r1(sK21,X0)
| ~ p1(sK6(X0)) )
| ~ spl32_1
| spl32_4
| ~ spl32_185 ),
inference(forward_subsumption_resolution,[],[f2125,f96]) ).
fof(f2170,plain,
( ~ r1(sK21,sK23)
| p1(sK6(sK23))
| ~ spl32_1
| spl32_4
| ~ spl32_185 ),
inference(resolution,[],[f2126,f67]) ).
fof(f2190,plain,
( ~ r1(sK21,sK23)
| ~ spl32_1
| spl32_4
| ~ spl32_185 ),
inference(forward_subsumption_resolution,[],[f2170,f2127]) ).
fof(f2257,plain,
( $false
| ~ spl32_1
| spl32_4
| ~ spl32_185 ),
inference(forward_subsumption_resolution,[],[f2190,f68]) ).
fof(f2258,plain,
( ~ spl32_1
| spl32_4
| ~ spl32_185 ),
inference(avatar_contradiction_clause,[],[f2257]) ).
fof(f2260,plain,
( ! [X0] :
( r1(X0,sK7(X0))
| p1(X0)
| ~ r1(X0,sK23)
| ~ sP2(X0) )
| ~ spl32_102 ),
inference(resolution,[],[f835,f32]) ).
fof(f2314,definition,
( spl32_294
<=> ! [X0] :
( ~ r1(sK21,X0)
| r1(X0,sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_294])],[avatar_definition]) ).
fof(f2315,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK21,X0) )
| ~ spl32_294 ),
inference(avatar_component_clause,[],[f2314]) ).
fof(f2318,definition,
( spl32_295
<=> ! [X0] :
( ~ r1(sK21,X0)
| ~ p1(sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_295])],[avatar_definition]) ).
fof(f2319,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK21,X0) )
| ~ spl32_295 ),
inference(avatar_component_clause,[],[f2318]) ).
fof(f2357,plain,
( ! [X0] :
( p1(sK21)
| ~ r1(sK21,sK23)
| ~ sP2(sK21)
| ~ p1(sK6(X0))
| p1(sK21)
| ~ r1(sK21,X0)
| ~ sP2(sK21) )
| ~ spl32_102 ),
inference(resolution,[],[f2260,f463]) ).
fof(f2371,plain,
( ! [X0] :
( p1(sK21)
| ~ r1(sK21,sK23)
| ~ sP2(sK21)
| ~ p1(sK6(X0))
| ~ r1(sK21,X0) )
| ~ spl32_102 ),
inference(duplicate_literal_removal,[],[f2357]) ).
fof(f2374,plain,
( ! [X0] :
( ~ r1(sK21,sK23)
| ~ sP2(sK21)
| ~ p1(sK6(X0))
| ~ r1(sK21,X0) )
| spl32_4
| ~ spl32_102 ),
inference(forward_subsumption_resolution,[],[f2371,f108]) ).
fof(f2381,plain,
( ! [X0] :
( ~ sP2(sK21)
| ~ p1(sK6(X0))
| ~ r1(sK21,X0) )
| spl32_4
| ~ spl32_102 ),
inference(forward_subsumption_resolution,[],[f2374,f68]) ).
fof(f2383,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK21,X0) )
| ~ spl32_1
| spl32_4
| ~ spl32_102 ),
inference(forward_subsumption_resolution,[],[f2381,f96]) ).
fof(f2384,plain,
( spl32_295
| ~ spl32_1
| spl32_4
| ~ spl32_102 ),
inference(avatar_split_clause,[],[f2383,f833,f107,f95,f2318]) ).
fof(f2385,plain,
( ~ r1(sK21,sK23)
| ~ spl32_102
| ~ spl32_295 ),
inference(resolution,[],[f2319,f835]) ).
fof(f2386,plain,
( $false
| ~ spl32_102
| ~ spl32_295 ),
inference(forward_subsumption_resolution,[],[f2385,f68]) ).
fof(f2387,plain,
( ~ spl32_102
| ~ spl32_295 ),
inference(avatar_contradiction_clause,[],[f2386]) ).
fof(f2513,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| p1(sK21)
| ~ r1(sK21,X0)
| p1(sK25(sK7(sK21)))
| ~ sP2(sK21) )
| ~ spl32_2 ),
inference(resolution,[],[f468,f101]) ).
fof(f2514,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK21,X0)
| p1(sK25(sK7(sK21)))
| ~ sP2(sK21) )
| ~ spl32_2
| spl32_4 ),
inference(forward_subsumption_resolution,[],[f2513,f108]) ).
fof(f2515,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK21,X0)
| p1(sK25(sK7(sK21))) )
| ~ spl32_1
| ~ spl32_2
| spl32_4 ),
inference(forward_subsumption_resolution,[],[f2514,f96]) ).
fof(f2517,definition,
( spl32_318
<=> p1(sK25(sK7(sK21))) ),
introduced(definition,[new_symbols(definition,[spl32_318])],[avatar_definition]) ).
fof(f2519,plain,
( p1(sK25(sK7(sK21)))
| ~ spl32_318 ),
inference(avatar_component_clause,[],[f2517]) ).
fof(f2520,plain,
( spl32_318
| spl32_294
| ~ spl32_1
| ~ spl32_2
| spl32_4 ),
inference(avatar_split_clause,[],[f2515,f107,f99,f95,f2314,f2517]) ).
fof(f2563,plain,
( ~ r1(sK21,sK23)
| spl32_3
| ~ spl32_294 ),
inference(resolution,[],[f2315,f104]) ).
fof(f2581,plain,
( $false
| spl32_3
| ~ spl32_294 ),
inference(forward_subsumption_resolution,[],[f2563,f68]) ).
fof(f2582,plain,
( spl32_3
| ~ spl32_294 ),
inference(avatar_contradiction_clause,[],[f2581]) ).
fof(f2604,plain,
( p1(sK7(sK21))
| ~ r1(sK21,sK7(sK21))
| ~ spl32_318 ),
inference(resolution,[],[f2519,f64]) ).
fof(f2605,plain,
( ~ r1(sK21,sK7(sK21))
| spl32_185
| ~ spl32_318 ),
inference(forward_subsumption_resolution,[],[f2604,f1432]) ).
fof(f2606,plain,
( $false
| ~ spl32_2
| spl32_185
| ~ spl32_318 ),
inference(forward_subsumption_resolution,[],[f2605,f101]) ).
fof(f2607,plain,
( ~ spl32_2
| spl32_185
| ~ spl32_318 ),
inference(avatar_contradiction_clause,[],[f2606]) ).
cnf(s1,plain,
( ~ spl32_1
| spl32_2
| spl32_3
| spl32_4 ),
inference(sat_conversion,[],[f110]) ).
cnf(s12,plain,
( ~ spl32_4
| ~ spl32_32
| spl32_33
| spl32_34
| spl32_35 ),
inference(sat_conversion,[],[f266]) ).
cnf(s25,plain,
spl32_1,
inference(sat_conversion,[],[f427]) ).
cnf(s26,plain,
spl32_32,
inference(sat_conversion,[],[f445]) ).
cnf(s37,plain,
( spl32_75
| spl32_76 ),
inference(sat_conversion,[],[f681]) ).
cnf(s40,plain,
~ spl32_35,
inference(sat_conversion,[],[f703]) ).
cnf(s50,plain,
( ~ spl32_4
| ~ spl32_32
| spl32_33
| spl32_35
| spl32_97 ),
inference(sat_conversion,[],[f802]) ).
cnf(s57,plain,
( ~ spl32_3
| spl32_102 ),
inference(sat_conversion,[],[f850]) ).
cnf(s74,plain,
( ~ spl32_75
| spl32_123 ),
inference(sat_conversion,[],[f981]) ).
cnf(s111,plain,
( spl32_174
| spl32_175
| spl32_178 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s142,plain,
( spl32_178
| spl32_221 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s169,plain,
( spl32_76
| ~ spl32_123
| spl32_266 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s170,plain,
~ spl32_266,
inference(sat_conversion,[],[f2033]) ).
cnf(s172,plain,
( ~ spl32_34
| ~ spl32_76
| ~ spl32_97
| spl32_190 ),
inference(sat_conversion,[],[f2035]) ).
cnf(s175,plain,
( ~ spl32_4
| ~ spl32_32
| spl32_33
| spl32_35
| ~ spl32_190 ),
inference(sat_conversion,[],[f2056]) ).
cnf(s176,plain,
( ~ spl32_33
| ~ spl32_178 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s179,plain,
( ~ spl32_174
| spl32_178
| spl32_220
| spl32_267 ),
inference(sat_conversion,[],[f2066]) ).
cnf(s180,plain,
( ~ spl32_175
| spl32_178
| spl32_220 ),
inference(sat_conversion,[],[f2079]) ).
cnf(s181,plain,
( spl32_175
| ~ spl32_221
| ~ spl32_267 ),
inference(sat_conversion,[],[f2094]) ).
cnf(s182,plain,
~ spl32_220,
inference(sat_conversion,[],[f2104]) ).
cnf(s198,plain,
( ~ spl32_1
| spl32_4
| ~ spl32_185 ),
inference(sat_conversion,[],[f2258]) ).
cnf(s205,plain,
( ~ spl32_1
| spl32_4
| ~ spl32_102
| spl32_295 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s206,plain,
( ~ spl32_102
| ~ spl32_295 ),
inference(sat_conversion,[],[f2387]) ).
cnf(s218,plain,
( ~ spl32_1
| ~ spl32_2
| spl32_4
| spl32_294
| spl32_318 ),
inference(sat_conversion,[],[f2520]) ).
cnf(s220,plain,
( spl32_3
| ~ spl32_294 ),
inference(sat_conversion,[],[f2582]) ).
cnf(s233,plain,
( ~ spl32_2
| spl32_185
| ~ spl32_318 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s234,plain,
( ~ spl32_175
| spl32_178 ),
inference(rat,[],[s180,s182]) ).
cnf(s235,plain,
( ~ spl32_174
| spl32_178
| spl32_267 ),
inference(rat,[],[s179,s182]) ).
cnf(s236,plain,
( spl32_76
| ~ spl32_123 ),
inference(rat,[],[s169,s170]) ).
cnf(s251,plain,
( ~ spl32_4
| spl32_33
| spl32_34 ),
inference(rat,[],[s12,s40,s26]) ).
cnf(s253,plain,
( spl32_2
| spl32_3
| spl32_4 ),
inference(rat,[],[s1,s25]) ).
cnf(s254,plain,
spl32_76,
inference(rat,[],[s74,s37,s236]) ).
cnf(s255,plain,
( spl32_33
| ~ spl32_4 ),
inference(rat,[],[s172,s175,s251,s50,s40,s26,s254]) ).
cnf(s256,plain,
spl32_178,
inference(rat,[],[s235,s181,s111,s142,s234]) ).
cnf(s257,plain,
~ spl32_33,
inference(rat,[],[s176,s256]) ).
cnf(s259,plain,
~ spl32_4,
inference(rat,[],[s255,s257]) ).
cnf(s263,plain,
~ spl32_185,
inference(rat,[],[s198,s25,s259]) ).
cnf(s264,plain,
~ spl32_102,
inference(rat,[],[s205,s206,s25,s259]) ).
cnf(s265,plain,
~ spl32_3,
inference(rat,[],[s57,s264]) ).
cnf(s266,plain,
~ spl32_294,
inference(rat,[],[s220,s265]) ).
cnf(s267,plain,
spl32_2,
inference(rat,[],[s253,s259,s265]) ).
cnf(s268,plain,
spl32_318,
inference(rat,[],[s218,s266,s259,s25,s267]) ).
cnf(s269,plain,
$false,
inference(rat,[],[s233,s263,s268,s267]) ).
fof(f2608,plain,
$false,
inference(avatar_sat_refutation,[],[s269]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL640+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 16:12:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.64/2.04 % (1828455)Detected formulas, will run a generic FOF schedule.
% 4.64/2.04 % (1828464)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=129604542:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.64/2.04 % (1828465)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2669171754:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.64/2.04 % (1828462)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2981238034:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.64/2.04 % (1828466)dis-21_1_sil=8000:lcm=predicate:random_seed=2440447340:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.64/2.04 % (1828463)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4077172412:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.64/2.04 % (1828460)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=411624180:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.64/2.04 % (1828461)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1269796202:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.64/2.04 % (1828464)Instruction limit reached!
% 4.64/2.04 % (1828464)------------------------------
% 4.64/2.04 % (1828464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828464)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828464)Termination reason: Instruction limit
% 4.64/2.04 % (1828464)Termination phase: Saturation
% 4.64/2.04 % (1828464)Time elapsed: 0.034 s
% 4.64/2.04 % (1828464)Peak memory usage: 88 MB
% 4.64/2.04 % (1828464)Instructions burned: 123 (million)
% 4.64/2.04 % (1828465)Instruction limit reached!
% 4.64/2.04 % (1828465)------------------------------
% 4.64/2.04 % (1828465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828465)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828465)Termination reason: Instruction limit
% 4.64/2.04 % (1828465)Termination phase: Saturation
% 4.64/2.04 % (1828465)Time elapsed: 0.049 s
% 4.64/2.04 % (1828465)Peak memory usage: 89 MB
% 4.64/2.04 % (1828465)Instructions burned: 140 (million)
% 4.64/2.04 % (1828463)Instruction limit reached!
% 4.64/2.04 % (1828463)------------------------------
% 4.64/2.04 % (1828463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828463)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828463)Termination reason: Instruction limit
% 4.64/2.04 % (1828463)Termination phase: Saturation
% 4.64/2.04 % (1828463)Time elapsed: 0.059 s
% 4.64/2.04 % (1828463)Peak memory usage: 90 MB
% 4.64/2.04 % (1828463)Instructions burned: 109 (million)
% 4.64/2.04 % (1828466)Instruction limit reached!
% 4.64/2.04 % (1828466)------------------------------
% 4.64/2.04 % (1828466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828466)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828466)Termination reason: Instruction limit
% 4.64/2.04 % (1828466)Termination phase: Saturation
% 4.64/2.04 % (1828466)Time elapsed: 0.069 s
% 4.64/2.04 % (1828466)Peak memory usage: 89 MB
% 4.64/2.04 % (1828466)Instructions burned: 132 (million)
% 4.64/2.04 % (1828474)lrs+10_1_sil=8000:sp=occurrence:random_seed=505091246:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.64/2.04 % (1828475)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3361230685:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 4.64/2.04 % (1828475)Refutation not found, incomplete strategy
% 4.64/2.04 % (1828475)------------------------------
% 4.64/2.04 % (1828475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828475)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828475)Termination reason: Refutation not found, incomplete strategy
% 4.64/2.04 % (1828475)Time elapsed: 0.007 s
% 4.64/2.04 % (1828475)Peak memory usage: 88 MB
% 4.64/2.04 % (1828475)Instructions burned: 23 (million)
% 4.64/2.04 % (1828476)lrs+1011_1_sil=32000:sp=occurrence:random_seed=373705364:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.64/2.04 % (1828477)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2138457766:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 4.64/2.04 % (1828477)Refutation not found, incomplete strategy
% 4.64/2.04 % (1828477)------------------------------
% 4.64/2.04 % (1828477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828477)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828477)Termination reason: Refutation not found, incomplete strategy
% 4.64/2.04 % (1828477)Time elapsed: 0.019 s
% 4.64/2.04 % (1828477)Peak memory usage: 88 MB
% 4.64/2.04 % (1828477)Instructions burned: 33 (million)
% 4.64/2.04 % (1828475)------------------------------
% 4.64/2.04 % (1828475)------------------------------
% 4.64/2.04 % (1828474)Instruction limit reached!
% 4.64/2.04 % (1828474)------------------------------
% 4.64/2.04 % (1828474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828474)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828474)Termination reason: Instruction limit
% 4.64/2.04 % (1828474)Termination phase: Saturation
% 4.64/2.04 % (1828474)Time elapsed: 0.173 s
% 4.64/2.04 % (1828474)Peak memory usage: 92 MB
% 4.64/2.04 % (1828474)Instructions burned: 286 (million)
% 4.64/2.04 % (1828476)Instruction limit reached!
% 4.64/2.04 % (1828476)------------------------------
% 4.64/2.04 % (1828476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828476)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828476)Termination reason: Instruction limit
% 4.64/2.04 % (1828476)Termination phase: Saturation
% 4.64/2.04 % (1828476)Time elapsed: 0.165 s
% 4.64/2.04 % (1828476)Peak memory usage: 90 MB
% 4.64/2.04 % (1828476)Instructions burned: 327 (million)
% 4.64/2.04 % (1828482)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3099383425:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.64/2.04 % (1828483)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3471858453:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 4.64/2.04 % (1828477)------------------------------
% 4.64/2.04 % (1828477)------------------------------
% 4.64/2.04 % (1828482)Instruction limit reached!
% 4.64/2.04 % (1828482)------------------------------
% 4.64/2.04 % (1828482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828482)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828482)Termination reason: Instruction limit
% 4.64/2.04 % (1828482)Termination phase: Saturation
% 4.64/2.04 % (1828482)Time elapsed: 0.081 s
% 4.64/2.04 % (1828482)Peak memory usage: 89 MB
% 4.64/2.04 % (1828482)Instructions burned: 294 (million)
% 4.64/2.04 % (1828484)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=402238051:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 4.64/2.04 % (1828488)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=873229747:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 4.64/2.04 % (1828484)Instruction limit reached!
% 4.64/2.04 % (1828484)------------------------------
% 4.64/2.04 % (1828484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828484)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828484)Termination reason: Instruction limit
% 4.64/2.04 % (1828484)Termination phase: Saturation
% 4.64/2.04 % (1828484)Time elapsed: 0.067 s
% 4.64/2.04 % (1828484)Peak memory usage: 90 MB
% 4.64/2.04 % (1828484)Instructions burned: 114 (million)
% 4.64/2.04 % (1828488)Instruction limit reached!
% 4.64/2.04 % (1828488)------------------------------
% 4.64/2.04 % (1828488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828488)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828488)Termination reason: Instruction limit
% 4.64/2.04 % (1828488)Termination phase: Saturation
% 4.64/2.04 % (1828488)Time elapsed: 0.030 s
% 4.64/2.04 % (1828488)Peak memory usage: 88 MB
% 4.64/2.04 % (1828488)Instructions burned: 117 (million)
% 4.64/2.04 % (1828487)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3264646755:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 4.64/2.04 % (1828487)Instruction limit reached!
% 4.64/2.04 % (1828487)------------------------------
% 4.64/2.04 % (1828487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828487)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828487)Termination reason: Instruction limit
% 4.64/2.04 % (1828487)Termination phase: Saturation
% 4.64/2.04 % (1828487)Time elapsed: 0.075 s
% 4.64/2.04 % (1828487)Peak memory usage: 89 MB
% 4.64/2.04 % (1828487)Instructions burned: 128 (million)
% 4.64/2.04 % (1828492)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2028352993:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 4.64/2.04 % (1828491)lrs+10_1_sil=8000:sp=occurrence:random_seed=61311298:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 4.64/2.04 % (1828460)First to succeed.
% 4.64/2.04 % (1828460)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1828455"
% 4.64/2.04 % (1828492)Instruction limit reached!
% 4.64/2.04 % (1828492)------------------------------
% 4.64/2.04 % (1828492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828492)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828492)Termination reason: Instruction limit
% 4.64/2.04 % (1828492)Termination phase: Saturation
% 4.64/2.04 % (1828492)Time elapsed: 0.124 s
% 4.64/2.04 % (1828492)Peak memory usage: 91 MB
% 4.64/2.04 % (1828492)Instructions burned: 439 (million)
% 4.64/2.04 % (1828495)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3289449901:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 4.64/2.04 % (1828461)Also succeeded, but the first one will report.
% 4.64/2.04 % (1828498)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=639874791:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 4.64/2.04 % (1828498)Refutation not found, incomplete strategy
% 4.64/2.04 % (1828498)------------------------------
% 4.64/2.04 % (1828498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/2.04 % (1828498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/2.04 % (1828498)CaDiCaL version: 2.1.3
% 4.64/2.04 % (1828498)Termination reason: Refutation not found, incomplete strategy
% 4.64/2.04 % (1828498)Time elapsed: 0.017 s
% 4.64/2.04 % (1828498)Peak memory usage: 89 MB
% 4.64/2.04 % (1828498)Instructions burned: 63 (million)
% 4.64/2.04 % (1828460)Refutation found. Thanks to Tanya!
% 4.64/2.04 % SZS status Theorem for theBenchmark
% 4.64/2.04 % SZS output start Proof for theBenchmark
% See solution above
% 0.14/2.13 % (1828460)------------------------------
% 0.14/2.13 % (1828460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.14/2.13 % (1828460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.14/2.13 % (1828460)CaDiCaL version: 2.1.3
% 0.14/2.13 % (1828460)Termination reason: Refutation
% 0.14/2.13 % (1828460)Time elapsed: 0.772 s
% 0.14/2.13 % (1828460)Peak memory usage: 130 MB
% 0.14/2.13 % (1828460)Instructions burned: 1126 (million)
% 0.14/2.13 % (1828460)------------------------------
% 0.14/2.13 % (1828460)------------------------------
% 0.14/2.13 % (1828455)Success in time 1.187 s
% 0.14/2.13 % Vampire exiting
%------------------------------------------------------------------------------