%------------------------------------------------------------------------------
% File : Vampire-SAT---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/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:06 AM UTC 2026
% Result : Theorem 80.60s 12.01s
% Output : Refutation 80.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 52
% Syntax : Number of formulae : 318 ( 28 unt; 51 def)
% Number of atoms : 1822 ( 0 equ)
% Maximal formula atoms : 121 ( 5 avg)
% Number of connectives : 2718 (1214 ~;1202 |; 275 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 54 ( 53 usr; 28 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-1 aty)
% Number of variables : 800 ( 0 sgn 682 !; 118 ?)
% 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/sandbox2/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,
! [X63] :
( ? [X66] :
( r1(X63,X66)
& ~ p1(X66)
& ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| p1(X68) )
| ~ p1(X67) ) )
| ~ sP0(X63) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X63] :
( ! [X69] :
( ~ r1(X63,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p1(X71) ) )
| ? [X72] :
( r1(X69,X72)
& ~ p1(X72) ) )
| ~ sP1(X63) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X63] :
( p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| ? [X65] :
( r1(X64,X65)
& ~ p1(X65) ) )
| sP0(X63)
| ~ sP2(X63) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X53] :
( ? [X56] :
( r1(X53,X56)
& ~ p1(X56)
& ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57) ) )
| ~ sP3(X53) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X53] :
( ! [X59] :
( ~ r1(X53,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) )
| ~ sP4(X53) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X53] :
( p1(X53)
| ! [X54] :
( ~ r1(X53,X54)
| ? [X55] :
( r1(X54,X55)
& ~ p1(X55) ) )
| sP3(X53)
| ~ sP5(X53) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X50] :
( ? [X51] :
( r1(X50,X51)
& ~ p1(X51) )
| ~ sP6(X50) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X49] :
( ? [X50] :
( r1(X49,X50)
& sP6(X50)
& p1(X50) )
| ~ sP7(X49) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X38] :
( ? [X39] :
( r1(X38,X39)
& ~ p1(X39) )
| ~ sP8(X38) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X37] :
( ? [X38] :
( r1(X37,X38)
& sP8(X38)
& p1(X38) )
| ~ sP9(X37) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X16] :
( ? [X40] :
( r1(X16,X40)
& ~ p1(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) )
| ~ p1(X41) ) )
| ~ sP10(X16) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X16] :
( ? [X29] :
( r1(X16,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) )
| ~ sP11(X16) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X23] :
( ? [X26] :
( r1(X23,X26)
& ~ p1(X26) )
| ~ sP12(X23) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X21] :
( ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ( sP12(X23)
& p1(X23) ) )
| ~ sP13(X21) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X21] :
( ? [X22] :
( r1(X21,X22)
& ~ p1(X22) )
| ~ sP14(X21) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X19] :
( ? [X20] :
( r1(X19,X20)
& ~ p1(X20) )
| ~ sP15(X19) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X18] :
( ? [X19] :
( r1(X18,X19)
& sP15(X19)
& p1(X19) )
| ~ sP16(X18) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X16] :
( ? [X21] :
( r1(X16,X21)
& sP14(X21)
& p1(X21)
& sP13(X21) )
| ~ sP17(X16) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X16] :
( ! [X32] :
( ~ r1(X16,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) )
| ~ sP18(X16) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X16] :
( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| sP11(X16)
| ~ sP19(X16) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X16] :
( ( ( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| sP16(X18) )
| sP17(X16) )
& sP19(X16)
& sP18(X16)
& ( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| sP9(X37) ) )
| sP10(X16) ) )
| ~ sP20(X16) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X4] :
( ? [X7] :
( r1(X4,X7)
& ~ p1(X7)
& ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p1(X9) )
| ~ p1(X8) ) )
| ~ sP21(X4) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X4] :
( ! [X10] :
( ~ r1(X4,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) ) )
| ? [X13] :
( r1(X10,X13)
& ~ p1(X13) ) )
| ~ sP22(X4) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X4] :
( p1(X4)
| ! [X5] :
( ~ r1(X4,X5)
| ? [X6] :
( r1(X5,X6)
& ~ p1(X6) ) )
| sP21(X4)
| ~ sP23(X4) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f31,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( sP23(X4)
& sP22(X4) ) ) ) ) )
& ! [X14] :
( ~ r1(X0,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| sP20(X16) ) ) )
& ? [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)
| sP7(X49) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ( sP5(X53)
& sP4(X53) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ( sP2(X63)
& sP1(X63) ) ) ),
inference(definition_folding,[],[f6,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7]) ).
fof(f41,plain,
! [X16] :
( ( ( ! [X17] :
( ~ r1(X16,X17)
| p1(X17) )
| ~ p1(X16)
| ! [X18] :
( ~ r1(X16,X18)
| sP16(X18) )
| sP17(X16) )
& sP19(X16)
& sP18(X16)
& ( ! [X36] :
( ~ r1(X16,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p1(X37)
| sP9(X37) ) )
| sP10(X16) ) )
| ~ sP20(X16) ),
inference(nnf_transformation,[],[f27]) ).
fof(f42,plain,
! [X0] :
( ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| sP16(X2) )
| sP17(X0) )
& sP19(X0)
& sP18(X0)
& ( ! [X3] :
( ~ r1(X0,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p1(X4)
| sP9(X4) ) )
| sP10(X0) ) )
| ~ sP20(X0) ),
inference(rectify,[],[f41]) ).
fof(f43,plain,
! [X16] :
( p1(X16)
| ! [X27] :
( ~ r1(X16,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| sP11(X16)
| ~ sP19(X16) ),
inference(nnf_transformation,[],[f26]) ).
fof(f44,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ? [X2] :
( r1(X1,X2)
& ~ p1(X2) ) )
| sP11(X0)
| ~ sP19(X0) ),
inference(rectify,[],[f43]) ).
fof(f45,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( r1(X1,sK27(X1))
& ~ p1(sK27(X1)) ) )
| sP11(X0)
| ~ sP19(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(X2,sK27(X1))],[f44]) ).
fof(f46,plain,
! [X16] :
( ! [X32] :
( ~ r1(X16,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) )
| ~ sP18(X16) ),
inference(nnf_transformation,[],[f25]) ).
fof(f47,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p1(X3) ) )
| ? [X4] :
( r1(X1,X4)
& ~ p1(X4) ) )
| ~ sP18(X0) ),
inference(rectify,[],[f46]) ).
fof(f48,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p1(X3) ) )
| ( r1(X1,sK28(X1))
& ~ p1(sK28(X1)) ) )
| ~ sP18(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X4,sK28(X1))],[f47]) ).
fof(f49,plain,
! [X16] :
( ? [X21] :
( r1(X16,X21)
& sP14(X21)
& p1(X21)
& sP13(X21) )
| ~ sP17(X16) ),
inference(nnf_transformation,[],[f24]) ).
fof(f50,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& sP14(X1)
& p1(X1)
& sP13(X1) )
| ~ sP17(X0) ),
inference(rectify,[],[f49]) ).
fof(f51,plain,
! [X0] :
( ( r1(X0,sK29(X0))
& sP14(sK29(X0))
& p1(sK29(X0))
& sP13(sK29(X0)) )
| ~ sP17(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(X1,sK29(X0))],[f50]) ).
fof(f52,plain,
! [X18] :
( ? [X19] :
( r1(X18,X19)
& sP15(X19)
& p1(X19) )
| ~ sP16(X18) ),
inference(nnf_transformation,[],[f23]) ).
fof(f53,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& sP15(X1)
& p1(X1) )
| ~ sP16(X0) ),
inference(rectify,[],[f52]) ).
fof(f54,plain,
! [X0] :
( ( r1(X0,sK30(X0))
& sP15(sK30(X0))
& p1(sK30(X0)) )
| ~ sP16(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(X1,sK30(X0))],[f53]) ).
fof(f55,plain,
! [X19] :
( ? [X20] :
( r1(X19,X20)
& ~ p1(X20) )
| ~ sP15(X19) ),
inference(nnf_transformation,[],[f22]) ).
fof(f56,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1) )
| ~ sP15(X0) ),
inference(rectify,[],[f55]) ).
fof(f57,plain,
! [X0] :
( ( r1(X0,sK31(X0))
& ~ p1(sK31(X0)) )
| ~ sP15(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(X1,sK31(X0))],[f56]) ).
fof(f58,plain,
! [X21] :
( ? [X22] :
( r1(X21,X22)
& ~ p1(X22) )
| ~ sP14(X21) ),
inference(nnf_transformation,[],[f21]) ).
fof(f59,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1) )
| ~ sP14(X0) ),
inference(rectify,[],[f58]) ).
fof(f60,plain,
! [X0] :
( ( r1(X0,sK32(X0))
& ~ p1(sK32(X0)) )
| ~ sP14(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(X1,sK32(X0))],[f59]) ).
fof(f61,plain,
! [X21] :
( ! [X23] :
( ~ r1(X21,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p1(X25) )
| ~ p1(X24) )
| ( sP12(X23)
& p1(X23) ) )
| ~ sP13(X21) ),
inference(nnf_transformation,[],[f20]) ).
fof(f62,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p1(X3) )
| ~ p1(X2) )
| ( sP12(X1)
& p1(X1) ) )
| ~ sP13(X0) ),
inference(rectify,[],[f61]) ).
fof(f66,plain,
! [X16] :
( ? [X29] :
( r1(X16,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) )
| ~ sP11(X16) ),
inference(nnf_transformation,[],[f18]) ).
fof(f67,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p1(X3) )
| ~ p1(X2) ) )
| ~ sP11(X0) ),
inference(rectify,[],[f66]) ).
fof(f68,plain,
! [X0] :
( ( r1(X0,sK34(X0))
& ~ p1(sK34(X0))
& ! [X2] :
( ~ r1(sK34(X0),X2)
| ! [X3] :
( ~ r1(X2,X3)
| p1(X3) )
| ~ p1(X2) ) )
| ~ sP11(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(X1,sK34(X0))],[f67]) ).
fof(f69,plain,
! [X16] :
( ? [X40] :
( r1(X16,X40)
& ~ p1(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p1(X42) )
| ~ p1(X41) ) )
| ~ sP10(X16) ),
inference(nnf_transformation,[],[f17]) ).
fof(f70,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p1(X3) )
| ~ p1(X2) ) )
| ~ sP10(X0) ),
inference(rectify,[],[f69]) ).
fof(f71,plain,
! [X0] :
( ( r1(X0,sK35(X0))
& ~ p1(sK35(X0))
& ! [X2] :
( ~ r1(sK35(X0),X2)
| ! [X3] :
( ~ r1(X2,X3)
| p1(X3) )
| ~ p1(X2) ) )
| ~ sP10(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(X1,sK35(X0))],[f70]) ).
fof(f72,plain,
! [X37] :
( ? [X38] :
( r1(X37,X38)
& sP8(X38)
& p1(X38) )
| ~ sP9(X37) ),
inference(nnf_transformation,[],[f16]) ).
fof(f73,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& sP8(X1)
& p1(X1) )
| ~ sP9(X0) ),
inference(rectify,[],[f72]) ).
fof(f74,plain,
! [X0] :
( ( r1(X0,sK36(X0))
& sP8(sK36(X0))
& p1(sK36(X0)) )
| ~ sP9(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(X1,sK36(X0))],[f73]) ).
fof(f75,plain,
! [X38] :
( ? [X39] :
( r1(X38,X39)
& ~ p1(X39) )
| ~ sP8(X38) ),
inference(nnf_transformation,[],[f15]) ).
fof(f76,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1) )
| ~ sP8(X0) ),
inference(rectify,[],[f75]) ).
fof(f77,plain,
! [X0] :
( ( r1(X0,sK37(X0))
& ~ p1(sK37(X0)) )
| ~ sP8(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(X1,sK37(X0))],[f76]) ).
fof(f78,plain,
! [X49] :
( ? [X50] :
( r1(X49,X50)
& sP6(X50)
& p1(X50) )
| ~ sP7(X49) ),
inference(nnf_transformation,[],[f14]) ).
fof(f79,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& sP6(X1)
& p1(X1) )
| ~ sP7(X0) ),
inference(rectify,[],[f78]) ).
fof(f80,plain,
! [X0] :
( ( r1(X0,sK38(X0))
& sP6(sK38(X0))
& p1(sK38(X0)) )
| ~ sP7(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X1,sK38(X0))],[f79]) ).
fof(f81,plain,
! [X50] :
( ? [X51] :
( r1(X50,X51)
& ~ p1(X51) )
| ~ sP6(X50) ),
inference(nnf_transformation,[],[f13]) ).
fof(f82,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1) )
| ~ sP6(X0) ),
inference(rectify,[],[f81]) ).
fof(f83,plain,
! [X0] :
( ( r1(X0,sK39(X0))
& ~ p1(sK39(X0)) )
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X1,sK39(X0))],[f82]) ).
fof(f102,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( sP23(X4)
& sP22(X4) ) ) ) ) )
& ! [X5] :
( ~ r1(X0,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| sP20(X7) ) ) )
& ? [X8] :
( r1(X0,X8)
& ? [X9] :
( r1(X8,X9)
& ? [X10] :
( r1(X9,X10)
& ? [X11] :
( r1(X10,X11)
& ~ p1(X11) )
& ? [X12] :
( r1(X10,X12)
& ! [X13] :
( ~ r1(X12,X13)
| p1(X13) ) )
& ! [X14] :
( ~ r1(X10,X14)
| p1(X14)
| sP7(X14) ) ) ) )
& ! [X15] :
( ~ r1(X0,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( sP5(X16)
& sP4(X16) ) ) )
& ! [X17] :
( ~ r1(X0,X17)
| ( sP2(X17)
& sP1(X17) ) ) ),
inference(rectify,[],[f31]) ).
fof(f103,plain,
( ! [X1] :
( ~ r1(sK46,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( sP23(X4)
& sP22(X4) ) ) ) ) )
& ! [X5] :
( ~ r1(sK46,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| sP20(X7) ) ) )
& r1(sK46,sK47)
& r1(sK47,sK48)
& r1(sK48,sK49)
& r1(sK49,sK50)
& ~ p1(sK50)
& r1(sK49,sK51)
& ! [X13] :
( ~ r1(sK51,X13)
| p1(X13) )
& ! [X14] :
( ~ r1(sK49,X14)
| p1(X14)
| sP7(X14) )
& ! [X15] :
( ~ r1(sK46,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( sP5(X16)
& sP4(X16) ) ) )
& ! [X17] :
( ~ r1(sK46,X17)
| ( sP2(X17)
& sP1(X17) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46,sK47,sK48,sK49,sK50,sK51]),skolemize(X0,sK46),skolemize(X8,sK47),skolemize(X9,sK48),skolemize(X10,sK49),skolemize(X11,sK50),skolemize(X12,sK51)],[f102]) ).
fof(f111,plain,
! [X3,X0,X4] :
( ~ sP20(X0)
| ~ r1(X3,X4)
| p1(X4)
| sP9(X4)
| sP10(X0)
| ~ r1(X0,X3) ),
inference(cnf_transformation,[],[f42]) ).
fof(f112,plain,
! [X0] :
( sP18(X0)
| ~ sP20(X0) ),
inference(cnf_transformation,[],[f42]) ).
fof(f113,plain,
! [X0] :
( sP19(X0)
| ~ sP20(X0) ),
inference(cnf_transformation,[],[f42]) ).
fof(f114,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X2)
| sP16(X2)
| sP17(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f115,plain,
! [X0,X1] :
( ~ p1(sK27(X1))
| ~ r1(X0,X1)
| p1(X0)
| sP11(X0)
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f116,plain,
! [X0,X1] :
( ~ sP19(X0)
| ~ r1(X0,X1)
| r1(X1,sK27(X1))
| sP11(X0)
| p1(X0) ),
inference(cnf_transformation,[],[f45]) ).
fof(f117,plain,
! [X2,X3,X0,X1] :
( ~ p1(sK28(X1))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ r1(X0,X1)
| ~ sP18(X0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f118,plain,
! [X2,X3,X0,X1] :
( ~ sP18(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK28(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f119,plain,
! [X0] :
( sP13(sK29(X0))
| ~ sP17(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f121,plain,
! [X0] :
( sP14(sK29(X0))
| ~ sP17(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f122,plain,
! [X0] :
( ~ sP17(X0)
| r1(X0,sK29(X0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f124,plain,
! [X0] :
( sP15(sK30(X0))
| ~ sP16(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f125,plain,
! [X0] :
( ~ sP16(X0)
| r1(X0,sK30(X0)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f126,plain,
! [X0] :
( ~ p1(sK31(X0))
| ~ sP15(X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f127,plain,
! [X0] :
( ~ sP15(X0)
| r1(X0,sK31(X0)) ),
inference(cnf_transformation,[],[f57]) ).
fof(f128,plain,
! [X0] :
( ~ p1(sK32(X0))
| ~ sP14(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f129,plain,
! [X0] :
( ~ sP14(X0)
| r1(X0,sK32(X0)) ),
inference(cnf_transformation,[],[f60]) ).
fof(f130,plain,
! [X2,X3,X0,X1] :
( ~ sP13(X0)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| p1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f62]) ).
fof(f134,plain,
! [X2,X3,X0] :
( ~ sP11(X0)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(sK34(X0),X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f135,plain,
! [X0] :
( ~ p1(sK34(X0))
| ~ sP11(X0) ),
inference(cnf_transformation,[],[f68]) ).
fof(f136,plain,
! [X0] :
( ~ sP11(X0)
| r1(X0,sK34(X0)) ),
inference(cnf_transformation,[],[f68]) ).
fof(f137,plain,
! [X2,X3,X0] :
( ~ sP10(X0)
| ~ r1(X2,X3)
| p1(X3)
| ~ p1(X2)
| ~ r1(sK35(X0),X2) ),
inference(cnf_transformation,[],[f71]) ).
fof(f138,plain,
! [X0] :
( ~ p1(sK35(X0))
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f139,plain,
! [X0] :
( ~ sP10(X0)
| r1(X0,sK35(X0)) ),
inference(cnf_transformation,[],[f71]) ).
fof(f140,plain,
! [X0] :
( p1(sK36(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f141,plain,
! [X0] :
( sP8(sK36(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f142,plain,
! [X0] :
( ~ sP9(X0)
| r1(X0,sK36(X0)) ),
inference(cnf_transformation,[],[f74]) ).
fof(f143,plain,
! [X0] :
( ~ p1(sK37(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f144,plain,
! [X0] :
( ~ sP8(X0)
| r1(X0,sK37(X0)) ),
inference(cnf_transformation,[],[f77]) ).
fof(f145,plain,
! [X0] :
( p1(sK38(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f146,plain,
! [X0] :
( sP6(sK38(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f147,plain,
! [X0] :
( ~ sP7(X0)
| r1(X0,sK38(X0)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f148,plain,
! [X0] :
( ~ p1(sK39(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f149,plain,
! [X0] :
( ~ sP6(X0)
| r1(X0,sK39(X0)) ),
inference(cnf_transformation,[],[f83]) ).
fof(f168,plain,
! [X14] :
( ~ r1(sK49,X14)
| p1(X14)
| sP7(X14) ),
inference(cnf_transformation,[],[f103]) ).
fof(f169,plain,
! [X13] :
( ~ r1(sK51,X13)
| p1(X13) ),
inference(cnf_transformation,[],[f103]) ).
fof(f170,plain,
r1(sK49,sK51),
inference(cnf_transformation,[],[f103]) ).
fof(f171,plain,
~ p1(sK50),
inference(cnf_transformation,[],[f103]) ).
fof(f172,plain,
r1(sK49,sK50),
inference(cnf_transformation,[],[f103]) ).
fof(f173,plain,
r1(sK48,sK49),
inference(cnf_transformation,[],[f103]) ).
fof(f174,plain,
r1(sK47,sK48),
inference(cnf_transformation,[],[f103]) ).
fof(f175,plain,
r1(sK46,sK47),
inference(cnf_transformation,[],[f103]) ).
fof(f176,plain,
! [X6,X7,X5] :
( ~ r1(sK46,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| sP20(X7) ),
inference(cnf_transformation,[],[f103]) ).
fof(f196,plain,
! [X0,X1] :
( ~ r1(sK47,X0)
| ~ r1(X0,X1)
| sP20(X1) ),
inference(resolution,[],[f176,f175]) ).
fof(f200,plain,
! [X0] :
( ~ r1(sK48,X0)
| sP20(X0) ),
inference(resolution,[],[f196,f174]) ).
fof(f201,plain,
sP20(sK49),
inference(resolution,[],[f200,f173]) ).
fof(f210,plain,
! [X0] :
( r1(sK30(X0),sK31(sK30(X0)))
| ~ sP16(X0) ),
inference(resolution,[],[f127,f124]) ).
fof(f211,plain,
! [X0] :
( r1(sK29(X0),sK32(sK29(X0)))
| ~ sP17(X0) ),
inference(resolution,[],[f129,f121]) ).
fof(f212,plain,
! [X0] :
( r1(sK36(X0),sK37(sK36(X0)))
| ~ sP9(X0) ),
inference(resolution,[],[f144,f141]) ).
fof(f214,plain,
! [X0] :
( r1(sK38(X0),sK39(sK38(X0)))
| ~ sP7(X0) ),
inference(resolution,[],[f149,f146]) ).
fof(f228,plain,
! [X0,X1] :
( ~ sP20(X0)
| r1(X1,sK27(X1))
| sP11(X0)
| p1(X0)
| ~ r1(X0,X1) ),
inference(resolution,[],[f116,f113]) ).
fof(f255,plain,
! [X0] :
( r1(X0,sK27(X0))
| sP11(sK49)
| p1(sK49)
| ~ r1(sK49,X0) ),
inference(resolution,[],[f228,f201]) ).
fof(f257,definition,
( spl52_11
<=> p1(sK49) ),
introduced(definition,[new_symbols(definition,[spl52_11])],[avatar_definition]) ).
fof(f261,definition,
( spl52_12
<=> sP11(sK49) ),
introduced(definition,[new_symbols(definition,[spl52_12])],[avatar_definition]) ).
fof(f263,plain,
( sP11(sK49)
| ~ spl52_12 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f265,definition,
( spl52_13
<=> ! [X0] :
( r1(X0,sK27(X0))
| ~ r1(sK49,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_13])],[avatar_definition]) ).
fof(f266,plain,
( ! [X0] :
( ~ r1(sK49,X0)
| r1(X0,sK27(X0)) )
| ~ spl52_13 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f267,plain,
( spl52_11
| spl52_12
| spl52_13 ),
inference(avatar_split_clause,[],[f255,f265,f261,f257]) ).
fof(f268,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| p1(X1)
| sP9(X1)
| sP10(sK49)
| ~ r1(sK49,X0) ),
inference(resolution,[],[f111,f201]) ).
fof(f270,definition,
( spl52_14
<=> sP10(sK49) ),
introduced(definition,[new_symbols(definition,[spl52_14])],[avatar_definition]) ).
fof(f272,plain,
( sP10(sK49)
| ~ spl52_14 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f274,definition,
( spl52_15
<=> ! [X0,X1] :
( ~ r1(X0,X1)
| ~ r1(sK49,X0)
| sP9(X1)
| p1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl52_15])],[avatar_definition]) ).
fof(f275,plain,
( ! [X0,X1] :
( ~ r1(sK49,X0)
| ~ r1(X0,X1)
| sP9(X1)
| p1(X1) )
| ~ spl52_15 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f276,plain,
( spl52_14
| spl52_15 ),
inference(avatar_split_clause,[],[f268,f274,f270]) ).
fof(f278,plain,
( r1(sK49,sK35(sK49))
| ~ spl52_14 ),
inference(resolution,[],[f272,f139]) ).
fof(f279,plain,
! [X0,X1] :
( p1(X0)
| ~ p1(sK49)
| ~ r1(sK49,X1)
| sP16(X1)
| sP17(sK49)
| ~ r1(sK49,X0) ),
inference(resolution,[],[f114,f201]) ).
fof(f281,definition,
( spl52_16
<=> sP17(sK49) ),
introduced(definition,[new_symbols(definition,[spl52_16])],[avatar_definition]) ).
fof(f283,plain,
( sP17(sK49)
| ~ spl52_16 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f285,definition,
( spl52_17
<=> ! [X1] :
( ~ r1(sK49,X1)
| sP16(X1) ) ),
introduced(definition,[new_symbols(definition,[spl52_17])],[avatar_definition]) ).
fof(f286,plain,
( ! [X1] :
( ~ r1(sK49,X1)
| sP16(X1) )
| ~ spl52_17 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f288,definition,
( spl52_18
<=> ! [X0] :
( p1(X0)
| ~ r1(sK49,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_18])],[avatar_definition]) ).
fof(f289,plain,
( ! [X0] :
( ~ r1(sK49,X0)
| p1(X0) )
| ~ spl52_18 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f290,plain,
( spl52_16
| spl52_17
| ~ spl52_11
| spl52_18 ),
inference(avatar_split_clause,[],[f279,f288,f257,f285,f281]) ).
fof(f292,plain,
( r1(sK49,sK34(sK49))
| ~ spl52_12 ),
inference(resolution,[],[f263,f136]) ).
fof(f295,plain,
( p1(sK35(sK49))
| sP7(sK35(sK49))
| ~ spl52_14 ),
inference(resolution,[],[f278,f168]) ).
fof(f297,definition,
( spl52_19
<=> sP7(sK35(sK49)) ),
introduced(definition,[new_symbols(definition,[spl52_19])],[avatar_definition]) ).
fof(f299,plain,
( sP7(sK35(sK49))
| ~ spl52_19 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f301,definition,
( spl52_20
<=> p1(sK35(sK49)) ),
introduced(definition,[new_symbols(definition,[spl52_20])],[avatar_definition]) ).
fof(f303,plain,
( p1(sK35(sK49))
| ~ spl52_20 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
( spl52_19
| spl52_20
| ~ spl52_14 ),
inference(avatar_split_clause,[],[f295,f270,f301,f297]) ).
fof(f309,plain,
( p1(sK34(sK49))
| sP7(sK34(sK49))
| ~ spl52_12 ),
inference(resolution,[],[f292,f168]) ).
fof(f311,definition,
( spl52_21
<=> sP7(sK34(sK49)) ),
introduced(definition,[new_symbols(definition,[spl52_21])],[avatar_definition]) ).
fof(f313,plain,
( sP7(sK34(sK49))
| ~ spl52_21 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl52_22
<=> p1(sK34(sK49)) ),
introduced(definition,[new_symbols(definition,[spl52_22])],[avatar_definition]) ).
fof(f317,plain,
( p1(sK34(sK49))
| ~ spl52_22 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
( spl52_21
| spl52_22
| ~ spl52_12 ),
inference(avatar_split_clause,[],[f309,f261,f315,f311]) ).
fof(f319,plain,
! [X2,X3,X0,X1] :
( ~ sP20(X3)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK28(X0))
| ~ r1(X3,X0)
| ~ r1(X0,X1) ),
inference(resolution,[],[f118,f112]) ).
fof(f320,plain,
! [X2,X3,X0,X1] :
( ~ sP17(X3)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(X0)
| ~ r1(sK29(X3),X0)
| ~ r1(X0,X1) ),
inference(resolution,[],[f130,f119]) ).
fof(f321,plain,
( r1(sK51,sK27(sK51))
| ~ spl52_13 ),
inference(resolution,[],[f266,f170]) ).
fof(f324,plain,
( p1(sK27(sK51))
| ~ spl52_13 ),
inference(resolution,[],[f321,f169]) ).
fof(f362,plain,
( r1(sK35(sK49),sK38(sK35(sK49)))
| ~ spl52_19 ),
inference(resolution,[],[f299,f147]) ).
fof(f372,plain,
( r1(sK49,sK29(sK49))
| ~ spl52_16 ),
inference(resolution,[],[f283,f122]) ).
fof(f422,plain,
! [X2,X0,X1] :
( ~ r1(sK49,X2)
| p1(X1)
| r1(X2,sK28(X2))
| ~ r1(X0,X1)
| ~ r1(X2,X0) ),
inference(resolution,[],[f319,f201]) ).
fof(f423,plain,
( ~ sP10(sK49)
| ~ spl52_20 ),
inference(resolution,[],[f303,f138]) ).
fof(f424,plain,
( ~ spl52_14
| ~ spl52_20 ),
inference(avatar_split_clause,[],[f423,f301,f270]) ).
fof(f428,plain,
( ! [X0] :
( ~ r1(sK29(sK49),X0)
| sP9(X0)
| p1(X0) )
| ~ spl52_15
| ~ spl52_16 ),
inference(resolution,[],[f372,f275]) ).
fof(f441,plain,
( ! [X2,X0,X1] :
( ~ r1(sK29(sK49),X2)
| p1(X1)
| ~ p1(X0)
| p1(X2)
| ~ r1(X0,X1)
| ~ r1(X2,X0) )
| ~ spl52_16 ),
inference(resolution,[],[f320,f283]) ).
fof(f523,plain,
( p1(sK50)
| ~ spl52_18 ),
inference(resolution,[],[f289,f172]) ).
fof(f525,plain,
( $false
| ~ spl52_18 ),
inference(global_subsumption,[],[f523,f171]) ).
fof(f526,plain,
~ spl52_18,
inference(avatar_contradiction_clause,[],[f525]) ).
fof(f540,plain,
! [X0,X1] :
( p1(X0)
| r1(sK51,sK28(sK51))
| ~ r1(X1,X0)
| ~ r1(sK51,X1) ),
inference(resolution,[],[f422,f170]) ).
fof(f542,definition,
( spl52_57
<=> r1(sK51,sK28(sK51)) ),
introduced(definition,[new_symbols(definition,[spl52_57])],[avatar_definition]) ).
fof(f544,plain,
( r1(sK51,sK28(sK51))
| ~ spl52_57 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f546,definition,
( spl52_58
<=> ! [X0,X1] :
( p1(X0)
| ~ r1(sK51,X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_58])],[avatar_definition]) ).
fof(f547,plain,
( ! [X0,X1] :
( ~ r1(sK51,X1)
| p1(X0)
| ~ r1(X1,X0) )
| ~ spl52_58 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f548,plain,
( spl52_57
| spl52_58 ),
inference(avatar_split_clause,[],[f540,f546,f542]) ).
fof(f578,plain,
( ! [X0,X1] :
( p1(X0)
| ~ p1(X1)
| p1(sK32(sK29(sK49)))
| ~ r1(X1,X0)
| ~ r1(sK32(sK29(sK49)),X1)
| ~ sP17(sK49) )
| ~ spl52_16 ),
inference(resolution,[],[f441,f211]) ).
fof(f579,plain,
( ! [X0,X1] :
( p1(X0)
| ~ p1(X1)
| p1(sK32(sK29(sK49)))
| ~ r1(X1,X0)
| ~ r1(sK32(sK29(sK49)),X1) )
| ~ spl52_16 ),
inference(global_subsumption,[],[f578,f283]) ).
fof(f581,definition,
( spl52_66
<=> p1(sK32(sK29(sK49))) ),
introduced(definition,[new_symbols(definition,[spl52_66])],[avatar_definition]) ).
fof(f583,plain,
( p1(sK32(sK29(sK49)))
| ~ spl52_66 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f585,definition,
( spl52_67
<=> ! [X0,X1] :
( p1(X0)
| ~ r1(sK32(sK29(sK49)),X1)
| ~ p1(X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_67])],[avatar_definition]) ).
fof(f586,plain,
( ! [X0,X1] :
( ~ r1(sK32(sK29(sK49)),X1)
| p1(X0)
| ~ p1(X1)
| ~ r1(X1,X0) )
| ~ spl52_67 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f587,plain,
( spl52_66
| spl52_67
| ~ spl52_16 ),
inference(avatar_split_clause,[],[f579,f281,f585,f581]) ).
fof(f598,plain,
( p1(sK28(sK51))
| ~ spl52_57 ),
inference(resolution,[],[f544,f169]) ).
fof(f627,plain,
( ! [X2,X0,X1] :
( ~ r1(sK51,X0)
| ~ r1(X0,X1)
| p1(X1)
| ~ r1(X2,sK51)
| ~ sP18(X2) )
| ~ spl52_57 ),
inference(resolution,[],[f598,f117]) ).
fof(f629,definition,
( spl52_75
<=> ! [X2] :
( ~ r1(X2,sK51)
| ~ sP18(X2) ) ),
introduced(definition,[new_symbols(definition,[spl52_75])],[avatar_definition]) ).
fof(f630,plain,
( ! [X2] :
( ~ sP18(X2)
| ~ r1(X2,sK51) )
| ~ spl52_75 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f631,plain,
( spl52_75
| spl52_58
| ~ spl52_57 ),
inference(avatar_split_clause,[],[f627,f542,f546,f629]) ).
fof(f632,plain,
( ~ sP14(sK29(sK49))
| ~ spl52_66 ),
inference(resolution,[],[f583,f128]) ).
fof(f639,plain,
( ~ sP17(sK49)
| ~ spl52_66 ),
inference(resolution,[],[f632,f121]) ).
fof(f640,plain,
( ~ spl52_16
| ~ spl52_66 ),
inference(avatar_split_clause,[],[f639,f581,f281]) ).
fof(f643,plain,
( sP16(sK51)
| ~ spl52_17 ),
inference(resolution,[],[f286,f170]) ).
fof(f645,plain,
( r1(sK51,sK30(sK51))
| ~ spl52_17 ),
inference(resolution,[],[f643,f125]) ).
fof(f718,plain,
( ! [X0] :
( ~ r1(X0,sK51)
| ~ sP20(X0) )
| ~ spl52_75 ),
inference(resolution,[],[f630,f112]) ).
fof(f731,plain,
( ~ sP20(sK49)
| ~ spl52_75 ),
inference(resolution,[],[f718,f170]) ).
fof(f732,plain,
( $false
| ~ spl52_75 ),
inference(global_subsumption,[],[f731,f201]) ).
fof(f733,plain,
~ spl52_75,
inference(avatar_contradiction_clause,[],[f732]) ).
fof(f735,plain,
( ! [X0] :
( ~ r1(sK30(sK51),X0)
| p1(X0) )
| ~ spl52_17
| ~ spl52_58 ),
inference(resolution,[],[f547,f645]) ).
fof(f748,plain,
( p1(sK31(sK30(sK51)))
| ~ sP16(sK51)
| ~ spl52_17
| ~ spl52_58 ),
inference(resolution,[],[f735,f210]) ).
fof(f750,plain,
( p1(sK31(sK30(sK51)))
| ~ spl52_17
| ~ spl52_58 ),
inference(global_subsumption,[],[f748,f643]) ).
fof(f756,plain,
( ! [X0,X1] :
( ~ r1(sK34(sK49),X0)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1) )
| ~ spl52_12 ),
inference(resolution,[],[f263,f134]) ).
fof(f771,plain,
( r1(sK34(sK49),sK38(sK34(sK49)))
| ~ spl52_21 ),
inference(resolution,[],[f313,f147]) ).
fof(f781,plain,
( ~ sP11(sK49)
| ~ spl52_22 ),
inference(resolution,[],[f317,f135]) ).
fof(f782,plain,
( ~ spl52_12
| ~ spl52_22 ),
inference(avatar_split_clause,[],[f781,f315,f261]) ).
fof(f898,plain,
( ! [X0] :
( p1(X0)
| ~ p1(sK38(sK34(sK49)))
| ~ r1(sK38(sK34(sK49)),X0) )
| ~ spl52_12
| ~ spl52_21 ),
inference(resolution,[],[f771,f756]) ).
fof(f900,definition,
( spl52_116
<=> p1(sK38(sK34(sK49))) ),
introduced(definition,[new_symbols(definition,[spl52_116])],[avatar_definition]) ).
fof(f902,plain,
( ~ p1(sK38(sK34(sK49)))
| spl52_116 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f904,definition,
( spl52_117
<=> ! [X0] :
( p1(X0)
| ~ r1(sK38(sK34(sK49)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_117])],[avatar_definition]) ).
fof(f905,plain,
( ! [X0] :
( ~ r1(sK38(sK34(sK49)),X0)
| p1(X0) )
| ~ spl52_117 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f906,plain,
( ~ spl52_116
| spl52_117
| ~ spl52_12
| ~ spl52_21 ),
inference(avatar_split_clause,[],[f898,f311,f261,f904,f900]) ).
fof(f945,plain,
( ~ sP7(sK34(sK49))
| spl52_116 ),
inference(resolution,[],[f902,f145]) ).
fof(f946,plain,
( ~ spl52_21
| spl52_116 ),
inference(avatar_split_clause,[],[f945,f900,f311]) ).
fof(f1016,plain,
( p1(sK39(sK38(sK34(sK49))))
| ~ sP7(sK34(sK49))
| ~ spl52_117 ),
inference(resolution,[],[f905,f214]) ).
fof(f1018,definition,
( spl52_135
<=> p1(sK39(sK38(sK34(sK49)))) ),
introduced(definition,[new_symbols(definition,[spl52_135])],[avatar_definition]) ).
fof(f1020,plain,
( p1(sK39(sK38(sK34(sK49))))
| ~ spl52_135 ),
inference(avatar_component_clause,[],[f1018]) ).
fof(f1021,plain,
( ~ spl52_21
| spl52_135
| ~ spl52_117 ),
inference(avatar_split_clause,[],[f1016,f904,f1018,f311]) ).
fof(f1026,plain,
( ! [X0] :
( ~ sP19(X0)
| p1(X0)
| sP11(X0)
| ~ r1(X0,sK51) )
| ~ spl52_13 ),
inference(resolution,[],[f324,f115]) ).
fof(f1072,plain,
( ! [X0] :
( ~ r1(X0,sK51)
| sP11(X0)
| p1(X0)
| ~ sP20(X0) )
| ~ spl52_13 ),
inference(resolution,[],[f1026,f113]) ).
fof(f1158,plain,
( sP11(sK49)
| p1(sK49)
| ~ sP20(sK49)
| ~ spl52_13 ),
inference(resolution,[],[f1072,f170]) ).
fof(f1159,plain,
( sP11(sK49)
| p1(sK49)
| ~ spl52_13 ),
inference(global_subsumption,[],[f1158,f201]) ).
fof(f1160,plain,
( spl52_11
| spl52_12
| ~ spl52_13 ),
inference(avatar_split_clause,[],[f1159,f265,f261,f257]) ).
fof(f1210,plain,
( sP9(sK32(sK29(sK49)))
| p1(sK32(sK29(sK49)))
| ~ sP17(sK49)
| ~ spl52_15
| ~ spl52_16 ),
inference(resolution,[],[f428,f211]) ).
fof(f1223,plain,
( sP9(sK32(sK29(sK49)))
| p1(sK32(sK29(sK49)))
| ~ spl52_15
| ~ spl52_16 ),
inference(global_subsumption,[],[f1210,f283]) ).
fof(f1225,definition,
( spl52_165
<=> sP9(sK32(sK29(sK49))) ),
introduced(definition,[new_symbols(definition,[spl52_165])],[avatar_definition]) ).
fof(f1227,plain,
( sP9(sK32(sK29(sK49)))
| ~ spl52_165 ),
inference(avatar_component_clause,[],[f1225]) ).
fof(f1228,plain,
( spl52_66
| spl52_165
| ~ spl52_15
| ~ spl52_16 ),
inference(avatar_split_clause,[],[f1223,f281,f274,f1225,f581]) ).
fof(f1240,plain,
( r1(sK32(sK29(sK49)),sK36(sK32(sK29(sK49))))
| ~ spl52_165 ),
inference(resolution,[],[f1227,f142]) ).
fof(f1291,plain,
( ! [X0] :
( p1(X0)
| ~ p1(sK36(sK32(sK29(sK49))))
| ~ r1(sK36(sK32(sK29(sK49))),X0) )
| ~ spl52_67
| ~ spl52_165 ),
inference(resolution,[],[f1240,f586]) ).
fof(f1293,definition,
( spl52_178
<=> p1(sK36(sK32(sK29(sK49)))) ),
introduced(definition,[new_symbols(definition,[spl52_178])],[avatar_definition]) ).
fof(f1295,plain,
( ~ p1(sK36(sK32(sK29(sK49))))
| spl52_178 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1297,definition,
( spl52_179
<=> ! [X0] :
( p1(X0)
| ~ r1(sK36(sK32(sK29(sK49))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_179])],[avatar_definition]) ).
fof(f1298,plain,
( ! [X0] :
( ~ r1(sK36(sK32(sK29(sK49))),X0)
| p1(X0) )
| ~ spl52_179 ),
inference(avatar_component_clause,[],[f1297]) ).
fof(f1299,plain,
( ~ spl52_178
| spl52_179
| ~ spl52_67
| ~ spl52_165 ),
inference(avatar_split_clause,[],[f1291,f1225,f585,f1297,f1293]) ).
fof(f1309,plain,
( ~ sP9(sK32(sK29(sK49)))
| spl52_178 ),
inference(resolution,[],[f1295,f140]) ).
fof(f1310,plain,
( ~ spl52_165
| spl52_178 ),
inference(avatar_split_clause,[],[f1309,f1293,f1225]) ).
fof(f1327,plain,
( p1(sK37(sK36(sK32(sK29(sK49)))))
| ~ sP9(sK32(sK29(sK49)))
| ~ spl52_179 ),
inference(resolution,[],[f1298,f212]) ).
fof(f1329,definition,
( spl52_185
<=> p1(sK37(sK36(sK32(sK29(sK49))))) ),
introduced(definition,[new_symbols(definition,[spl52_185])],[avatar_definition]) ).
fof(f1331,plain,
( p1(sK37(sK36(sK32(sK29(sK49)))))
| ~ spl52_185 ),
inference(avatar_component_clause,[],[f1329]) ).
fof(f1332,plain,
( ~ spl52_165
| spl52_185
| ~ spl52_179 ),
inference(avatar_split_clause,[],[f1327,f1297,f1329,f1225]) ).
fof(f1352,plain,
( ~ sP15(sK30(sK51))
| ~ spl52_17
| ~ spl52_58 ),
inference(resolution,[],[f750,f126]) ).
fof(f1355,plain,
( ~ sP16(sK51)
| ~ spl52_17
| ~ spl52_58 ),
inference(resolution,[],[f1352,f124]) ).
fof(f1356,plain,
( $false
| ~ spl52_17
| ~ spl52_58 ),
inference(global_subsumption,[],[f1355,f643]) ).
fof(f1357,plain,
( ~ spl52_17
| ~ spl52_58 ),
inference(avatar_contradiction_clause,[],[f1356]) ).
fof(f1378,plain,
( ~ sP8(sK36(sK32(sK29(sK49))))
| ~ spl52_185 ),
inference(resolution,[],[f1331,f143]) ).
fof(f1385,plain,
( ~ sP9(sK32(sK29(sK49)))
| ~ spl52_185 ),
inference(resolution,[],[f1378,f141]) ).
fof(f1386,plain,
( ~ spl52_165
| ~ spl52_185 ),
inference(avatar_split_clause,[],[f1385,f1329,f1225]) ).
fof(f1387,plain,
( ! [X0,X1] :
( ~ r1(sK35(sK49),X0)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1) )
| ~ spl52_14 ),
inference(resolution,[],[f272,f137]) ).
fof(f1403,plain,
( ! [X0] :
( p1(X0)
| ~ p1(sK38(sK35(sK49)))
| ~ r1(sK38(sK35(sK49)),X0) )
| ~ spl52_14
| ~ spl52_19 ),
inference(resolution,[],[f1387,f362]) ).
fof(f1405,definition,
( spl52_189
<=> p1(sK38(sK35(sK49))) ),
introduced(definition,[new_symbols(definition,[spl52_189])],[avatar_definition]) ).
fof(f1407,plain,
( ~ p1(sK38(sK35(sK49)))
| spl52_189 ),
inference(avatar_component_clause,[],[f1405]) ).
fof(f1409,definition,
( spl52_190
<=> ! [X0] :
( p1(X0)
| ~ r1(sK38(sK35(sK49)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_190])],[avatar_definition]) ).
fof(f1410,plain,
( ! [X0] :
( ~ r1(sK38(sK35(sK49)),X0)
| p1(X0) )
| ~ spl52_190 ),
inference(avatar_component_clause,[],[f1409]) ).
fof(f1411,plain,
( ~ spl52_189
| spl52_190
| ~ spl52_14
| ~ spl52_19 ),
inference(avatar_split_clause,[],[f1403,f297,f270,f1409,f1405]) ).
fof(f1431,plain,
( ~ sP7(sK35(sK49))
| spl52_189 ),
inference(resolution,[],[f1407,f145]) ).
fof(f1432,plain,
( ~ spl52_19
| spl52_189 ),
inference(avatar_split_clause,[],[f1431,f1405,f297]) ).
fof(f1470,plain,
( p1(sK39(sK38(sK35(sK49))))
| ~ sP7(sK35(sK49))
| ~ spl52_190 ),
inference(resolution,[],[f1410,f214]) ).
fof(f1472,definition,
( spl52_201
<=> p1(sK39(sK38(sK35(sK49)))) ),
introduced(definition,[new_symbols(definition,[spl52_201])],[avatar_definition]) ).
fof(f1474,plain,
( p1(sK39(sK38(sK35(sK49))))
| ~ spl52_201 ),
inference(avatar_component_clause,[],[f1472]) ).
fof(f1475,plain,
( ~ spl52_19
| spl52_201
| ~ spl52_190 ),
inference(avatar_split_clause,[],[f1470,f1409,f1472,f297]) ).
fof(f1476,plain,
( ~ sP6(sK38(sK35(sK49)))
| ~ spl52_201 ),
inference(resolution,[],[f1474,f148]) ).
fof(f1478,plain,
( ~ sP7(sK35(sK49))
| ~ spl52_201 ),
inference(resolution,[],[f1476,f146]) ).
fof(f1479,plain,
( ~ spl52_19
| ~ spl52_201 ),
inference(avatar_split_clause,[],[f1478,f1472,f297]) ).
fof(f1504,plain,
( ~ sP6(sK38(sK34(sK49)))
| ~ spl52_135 ),
inference(resolution,[],[f1020,f148]) ).
fof(f1525,plain,
( ~ sP7(sK34(sK49))
| ~ spl52_135 ),
inference(resolution,[],[f1504,f146]) ).
fof(f1526,plain,
( ~ spl52_21
| ~ spl52_135 ),
inference(avatar_split_clause,[],[f1525,f1018,f311]) ).
cnf(s119,plain,
( spl52_11
| spl52_12
| spl52_13 ),
inference(sat_conversion,[],[f267]) ).
cnf(s122,plain,
( spl52_14
| spl52_15 ),
inference(sat_conversion,[],[f276]) ).
cnf(s127,plain,
( ~ spl52_11
| spl52_16
| spl52_17
| spl52_18 ),
inference(sat_conversion,[],[f290]) ).
cnf(s133,plain,
( ~ spl52_14
| spl52_19
| spl52_20 ),
inference(sat_conversion,[],[f304]) ).
cnf(s141,plain,
( ~ spl52_12
| spl52_21
| spl52_22 ),
inference(sat_conversion,[],[f318]) ).
cnf(s193,plain,
( ~ spl52_14
| ~ spl52_20 ),
inference(sat_conversion,[],[f424]) ).
cnf(s241,plain,
~ spl52_18,
inference(sat_conversion,[],[f526]) ).
cnf(s253,plain,
( spl52_57
| spl52_58 ),
inference(sat_conversion,[],[f548]) ).
cnf(s269,plain,
( ~ spl52_16
| spl52_66
| spl52_67 ),
inference(sat_conversion,[],[f587]) ).
cnf(s289,plain,
( ~ spl52_57
| spl52_58
| spl52_75 ),
inference(sat_conversion,[],[f631]) ).
cnf(s297,plain,
( ~ spl52_16
| ~ spl52_66 ),
inference(sat_conversion,[],[f640]) ).
cnf(s348,plain,
~ spl52_75,
inference(sat_conversion,[],[f733]) ).
cnf(s383,plain,
( ~ spl52_12
| ~ spl52_22 ),
inference(sat_conversion,[],[f782]) ).
cnf(s448,plain,
( ~ spl52_12
| ~ spl52_21
| ~ spl52_116
| spl52_117 ),
inference(sat_conversion,[],[f906]) ).
cnf(s467,plain,
( ~ spl52_21
| spl52_116 ),
inference(sat_conversion,[],[f946]) ).
cnf(s514,plain,
( ~ spl52_21
| ~ spl52_117
| spl52_135 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s596,plain,
( spl52_11
| spl52_12
| ~ spl52_13 ),
inference(sat_conversion,[],[f1160]) ).
cnf(s631,plain,
( ~ spl52_15
| ~ spl52_16
| spl52_66
| spl52_165 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s664,plain,
( ~ spl52_67
| ~ spl52_165
| ~ spl52_178
| spl52_179 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s670,plain,
( ~ spl52_165
| spl52_178 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s681,plain,
( ~ spl52_165
| ~ spl52_179
| spl52_185 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s707,plain,
( ~ spl52_17
| ~ spl52_58 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s727,plain,
( ~ spl52_165
| ~ spl52_185 ),
inference(sat_conversion,[],[f1386]) ).
cnf(s742,plain,
( ~ spl52_14
| ~ spl52_19
| ~ spl52_189
| spl52_190 ),
inference(sat_conversion,[],[f1411]) ).
cnf(s751,plain,
( ~ spl52_19
| spl52_189 ),
inference(sat_conversion,[],[f1432]) ).
cnf(s775,plain,
( ~ spl52_19
| ~ spl52_190
| spl52_201 ),
inference(sat_conversion,[],[f1475]) ).
cnf(s780,plain,
( ~ spl52_19
| ~ spl52_201 ),
inference(sat_conversion,[],[f1479]) ).
cnf(s809,plain,
( ~ spl52_21
| ~ spl52_135 ),
inference(sat_conversion,[],[f1526]) ).
cnf(s811,plain,
( ~ spl52_57
| spl52_58 ),
inference(rat,[],[s289,s348]) ).
cnf(s819,plain,
( ~ spl52_11
| spl52_16
| spl52_17 ),
inference(rat,[],[s127,s241]) ).
cnf(s820,plain,
( spl52_12
| spl52_11 ),
inference(rat,[],[s119,s596]) ).
cnf(s821,plain,
( spl52_22
| ~ spl52_12 ),
inference(rat,[],[s448,s467,s514,s809,s141]) ).
cnf(s822,plain,
~ spl52_12,
inference(rat,[],[s821,s383]) ).
cnf(s823,plain,
spl52_11,
inference(rat,[],[s820,s822]) ).
cnf(s824,plain,
spl52_58,
inference(rat,[],[s253,s811]) ).
cnf(s825,plain,
~ spl52_17,
inference(rat,[],[s707,s824]) ).
cnf(s826,plain,
spl52_16,
inference(rat,[],[s819,s823,s825]) ).
cnf(s827,plain,
~ spl52_66,
inference(rat,[],[s297,s826]) ).
cnf(s828,plain,
spl52_67,
inference(rat,[],[s269,s826,s827]) ).
cnf(s829,plain,
( ~ spl52_165
| spl52_185 ),
inference(rat,[],[s664,s670,s681,s828]) ).
cnf(s830,plain,
~ spl52_165,
inference(rat,[],[s829,s727]) ).
cnf(s831,plain,
~ spl52_15,
inference(rat,[],[s631,s827,s826,s830]) ).
cnf(s832,plain,
spl52_14,
inference(rat,[],[s122,s831]) ).
cnf(s833,plain,
~ spl52_20,
inference(rat,[],[s193,s832]) ).
cnf(s834,plain,
spl52_19,
inference(rat,[],[s133,s832,s833]) ).
cnf(s835,plain,
~ spl52_201,
inference(rat,[],[s780,s834]) ).
cnf(s836,plain,
~ spl52_190,
inference(rat,[],[s775,s835,s834]) ).
cnf(s837,plain,
spl52_189,
inference(rat,[],[s751,s834]) ).
cnf(s838,plain,
$false,
inference(rat,[],[s742,s836,s832,s837,s834]) ).
fof(f1527,plain,
$false,
inference(avatar_sat_refutation,[],[s838]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL640+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.41 % Computer : n001.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 27 16:14:46 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.45 Running first-order model finding
% 0.14/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.48/4.02 % (3759643)Will run a generic schedule for satisfiability detection.
% 24.48/4.02 % (3759652)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4279817751:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 24.48/4.02 % (3759649)% WARNING: option uhcvi not known.
% 24.48/4.02 % (3759651)dis+10_1_sil=32000:sp=arity:random_seed=2514961284:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 24.48/4.02 % (3759648)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2451861218_2999 on theBenchmark for (2999ds/0Mi)
% 24.48/4.02 % (3759650)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=808424724:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 24.48/4.02 % (3759653)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2301816226:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 24.48/4.02 % (3759649)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2430193858:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 24.48/4.02 % (3759654)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3349936029:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 24.48/4.02 % TRYING [1]
% 24.48/4.02 % TRYING [2]
% 24.48/4.02 % TRYING [3]
% 24.48/4.02 % (3759652)Instruction limit reached!
% 24.48/4.02 % (3759652)------------------------------
% 24.48/4.02 % (3759652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.48/4.02 % (3759652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.02 % (3759652)CaDiCaL version: 2.1.3
% 24.48/4.02 % (3759652)Termination reason: Instruction limit
% 24.48/4.02 % (3759652)Termination phase: Saturation
% 24.48/4.02 % (3759652)Time elapsed: 0.050 s
% 24.48/4.02 % (3759652)Peak memory usage: 12 MB
% 24.48/4.02 % (3759652)Instructions burned: 116 (million)
% 24.48/4.02 % (3759662)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=51344931:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 24.48/4.02 % TRYING [1]
% 24.48/4.02 % TRYING [2]
% 24.48/4.02 % TRYING [3]
% 24.48/4.02 % TRYING [4]
% 24.48/4.02 % TRYING [4]
% 24.48/4.02 % (3759651)Instruction limit reached!
% 24.48/4.02 % (3759651)------------------------------
% 24.48/4.02 % (3759651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.48/4.02 % (3759651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.02 % (3759651)CaDiCaL version: 2.1.3
% 24.48/4.02 % (3759651)Termination reason: Instruction limit
% 24.48/4.02 % (3759651)Termination phase: Saturation
% 24.48/4.02 % (3759651)Time elapsed: 0.097 s
% 24.48/4.02 % (3759651)Peak memory usage: 12 MB
% 24.48/4.02 % (3759651)Instructions burned: 103 (million)
% 24.48/4.02 % (3759653)Instruction limit reached!
% 24.48/4.02 % (3759653)------------------------------
% 24.48/4.02 % (3759653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.48/4.02 % (3759653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.02 % (3759653)CaDiCaL version: 2.1.3
% 24.48/4.02 % (3759653)Termination reason: Instruction limit
% 24.48/4.02 % (3759653)Termination phase: Saturation
% 24.48/4.02 % (3759653)Time elapsed: 0.121 s
% 24.48/4.02 % (3759653)Peak memory usage: 14 MB
% 24.48/4.02 % (3759653)Instructions burned: 132 (million)
% 24.48/4.02 % (3759664)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2306978345:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 24.48/4.02 % TRYING [5]
% 24.48/4.02 % (3759665)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2439490432:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 24.48/4.02 % (3759654)Instruction limit reached!
% 24.48/4.02 % (3759654)------------------------------
% 24.48/4.02 % (3759654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.48/4.02 % (3759654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.48/4.02 % (3759654)CaDiCaL version: 2.1.3
% 24.48/4.02 % (3759654)Termination reason: Instruction limit
% 24.48/4.02 % (3759654)Termination phase: Saturation
% 24.48/4.02 % (3759654)Time elapsed: 0.153 s
% 24.48/4.02 % (3759654)Peak memory usage: 14 MB
% 24.48/4.02 % (3759654)Instructions burned: 159 (million)
% 24.48/4.02 % (3759668)ott-21_1_sil=16000:fs=off:random_seed=867011922:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 24.48/4.02 % (3759664)Instruction limit reached!
% 24.48/4.02 % (3759664)------------------------------
% 24.48/4.02 % (3759664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.35/11.23 % (3759664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.35/11.23 % (3759664)CaDiCaL version: 2.1.3
% 76.35/11.23 % (3759664)Termination reason: Instruction limit
% 76.35/11.23 % (3759664)Termination phase: Saturation
% 76.35/11.23 % (3759664)Time elapsed: 0.114 s
% 76.35/11.23 % (3759664)Peak memory usage: 13 MB
% 76.35/11.23 % (3759664)Instructions burned: 132 (million)
% 76.35/11.23 % TRYING [5]
% 76.35/11.23 % (3759670)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4081803112:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 76.35/11.23 % TRYING [6]
% 76.35/11.23 % (3759668)Instruction limit reached!
% 76.35/11.23 % (3759668)------------------------------
% 76.35/11.23 % (3759668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.35/11.23 % (3759668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.35/11.23 % (3759668)CaDiCaL version: 2.1.3
% 76.35/11.23 % (3759668)Termination reason: Instruction limit
% 76.35/11.23 % (3759668)Termination phase: Saturation
% 76.35/11.23 % (3759668)Time elapsed: 0.160 s
% 76.35/11.23 % (3759668)Peak memory usage: 13 MB
% 76.35/11.23 % (3759668)Instructions burned: 180 (million)
% 76.35/11.23 % (3759662)Instruction limit reached!
% 76.35/11.23 % (3759662)------------------------------
% 76.35/11.23 % (3759662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.35/11.23 % (3759662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.35/11.23 % (3759662)CaDiCaL version: 2.1.3
% 76.35/11.23 % (3759662)Termination reason: Instruction limit
% 76.35/11.23 % (3759662)Termination phase: Finite model building SAT solving
% 76.35/11.23 % (3759662)Time elapsed: 0.316 s
% 76.35/11.23 % (3759662)Peak memory usage: 13 MB
% 76.35/11.23 % (3759662)Instructions burned: 716 (million)
% 76.35/11.23 % (3759672)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4089287771:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 76.35/11.23 % TRYING [1]
% 76.35/11.23 % TRYING [2]
% 76.35/11.23 % TRYING [3]
% 76.35/11.23 % (3759673)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=583907783:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 76.35/11.23 % TRYING [4]
% 76.35/11.23 % TRYING [5]
% 76.35/11.23 % (3759670)Instruction limit reached!
% 76.35/11.23 % (3759670)------------------------------
% 76.35/11.23 % (3759670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.35/11.23 % (3759670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.35/11.23 % (3759670)CaDiCaL version: 2.1.3
% 76.35/11.23 % (3759670)Termination reason: Instruction limit
% 76.35/11.23 % (3759670)Termination phase: Saturation
% 76.35/11.23 % (3759670)Time elapsed: 0.463 s
% 76.35/11.23 % (3759670)Peak memory usage: 16 MB
% 76.35/11.23 % (3759670)Instructions burned: 478 (million)
% 76.35/11.23 % TRYING [6]
% 76.35/11.23 % (3759665)Instruction limit reached!
% 76.35/11.23 % (3759665)------------------------------
% 76.35/11.23 % (3759665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.35/11.23 % (3759665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.35/11.23 % (3759665)CaDiCaL version: 2.1.3
% 76.35/11.23 % (3759665)Termination reason: Instruction limit
% 76.35/11.23 % (3759665)Termination phase: Saturation
% 76.35/11.23 % (3759665)Time elapsed: 0.620 s
% 76.35/11.23 % (3759665)Peak memory usage: 16 MB
% 76.35/11.23 % (3759665)Instructions burned: 684 (million)
% 76.35/11.23 % (3759676)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3438548799:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 76.35/11.23 % TRYING [14]
% 76.35/11.23 % (3759677)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4284145865:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 76.35/11.23 % (3759673)Instruction limit reached!
% 76.35/11.23 % (3759673)------------------------------
% 76.35/11.23 % (3759673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.35/11.23 % (3759673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.35/11.23 % (3759673)CaDiCaL version: 2.1.3
% 76.35/11.23 % (3759673)Termination reason: Instruction limit
% 76.35/11.23 % (3759673)Termination phase: Saturation
% 76.35/11.23 % (3759673)Time elapsed: 0.597 s
% 76.35/11.23 % (3759673)Peak memory usage: 23 MB
% 76.35/11.23 % (3759673)Instructions burned: 1182 (million)
% 76.35/11.23 % (3759680)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4141337351:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 76.35/11.23 % (3759672)Instruction limit reached!
% 76.35/11.23 % (3759672)------------------------------
% 80.60/12.00 % (3759672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759672)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759672)Termination reason: Instruction limit
% 80.60/12.00 % (3759672)Termination phase: Finite model building SAT solving
% 80.60/12.00 % (3759672)Time elapsed: 0.716 s
% 80.60/12.00 % (3759672)Peak memory usage: 14 MB
% 80.60/12.00 % (3759672)Instructions burned: 865 (million)
% 80.60/12.00 % TRYING [6]
% 80.60/12.00 % (3759682)fmb+10_1_sil=64000:random_seed=2518412815:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 80.60/12.00 % TRYING [1]
% 80.60/12.00 % TRYING [2]
% 80.60/12.00 % TRYING [3]
% 80.60/12.00 % TRYING [4]
% 80.60/12.00 % TRYING [5]
% 80.60/12.00 % TRYING [6]
% 80.60/12.00 % (3759676)Instruction limit reached!
% 80.60/12.00 % (3759676)------------------------------
% 80.60/12.00 % (3759676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759676)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759676)Termination reason: Instruction limit
% 80.60/12.00 % (3759676)Termination phase: Finite model building SAT solving
% 80.60/12.00 % (3759676)Time elapsed: 0.599 s
% 80.60/12.00 % (3759676)Peak memory usage: 24 MB
% 80.60/12.00 % (3759676)Instructions burned: 889 (million)
% 80.60/12.00 % (3759684)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2238773512:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 80.60/12.00 % (3759677)Instruction limit reached!
% 80.60/12.00 % (3759677)------------------------------
% 80.60/12.00 % (3759677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759677)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759677)Termination reason: Instruction limit
% 80.60/12.00 % (3759677)Termination phase: Saturation
% 80.60/12.00 % (3759677)Time elapsed: 0.611 s
% 80.60/12.00 % (3759677)Peak memory usage: 24 MB
% 80.60/12.00 % (3759677)Instructions burned: 693 (million)
% 80.60/12.00 % TRYING [20]
% 80.60/12.00 % (3759686)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2468638226:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 80.60/12.00 % TRYING [8]
% 80.60/12.00 % TRYING [7]
% 80.60/12.00 % (3759680)Instruction limit reached!
% 80.60/12.00 % (3759680)------------------------------
% 80.60/12.00 % (3759680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759680)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759680)Termination reason: Instruction limit
% 80.60/12.00 % (3759680)Termination phase: Saturation
% 80.60/12.00 % (3759680)Time elapsed: 0.533 s
% 80.60/12.00 % (3759680)Peak memory usage: 14 MB
% 80.60/12.00 % (3759680)Instructions burned: 879 (million)
% 80.60/12.00 % (3759688)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1974869364:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 80.60/12.00 % (3759686)Instruction limit reached!
% 80.60/12.00 % (3759686)------------------------------
% 80.60/12.00 % (3759686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759686)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759686)Termination reason: Instruction limit
% 80.60/12.00 % (3759686)Termination phase: Finite model building SAT solving
% 80.60/12.00 % (3759686)Time elapsed: 0.759 s
% 80.60/12.00 % (3759686)Peak memory usage: 18 MB
% 80.60/12.00 % (3759686)Instructions burned: 921 (million)
% 80.60/12.00 % (3759690)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4177486932:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 80.60/12.00 % TRYING [8]
% 80.60/12.00 % TRYING [7]
% 80.60/12.00 % (3759690)Instruction limit reached!
% 80.60/12.00 % (3759690)------------------------------
% 80.60/12.00 % (3759690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759690)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759690)Termination reason: Instruction limit
% 80.60/12.00 % (3759690)Termination phase: Saturation
% 80.60/12.00 % (3759690)Time elapsed: 1.194 s
% 80.60/12.00 % (3759690)Peak memory usage: 40 MB
% 80.60/12.00 % (3759690)Instructions burned: 1473 (million)
% 80.60/12.00 % (3759692)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2739878782:i=6324_2964 on theBenchmark for (2964ds/6324Mi)
% 80.60/12.00 % TRYING [77]
% 80.60/12.00 % (3759688)Instruction limit reached!
% 80.60/12.00 % (3759688)------------------------------
% 80.60/12.00 % (3759688)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759688)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759688)Termination reason: Instruction limit
% 80.60/12.00 % (3759688)Termination phase: Saturation
% 80.60/12.00 % (3759688)Time elapsed: 3.655 s
% 80.60/12.00 % (3759688)Peak memory usage: 17 MB
% 80.60/12.00 % (3759688)Instructions burned: 5132 (million)
% 80.60/12.00 % (3759696)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1758732703:fmbsr=2.30978:i=2174_2946 on theBenchmark for (2946ds/2174Mi)
% 80.60/12.00 % TRYING [16]
% 80.60/12.00 % (3759696)Instruction limit reached!
% 80.60/12.00 % (3759696)------------------------------
% 80.60/12.00 % (3759696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759696)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759696)Termination reason: Instruction limit
% 80.60/12.00 % (3759696)Termination phase: Finite model building SAT solving
% 80.60/12.00 % (3759696)Time elapsed: 1.780 s
% 80.60/12.00 % (3759696)Peak memory usage: 46 MB
% 80.60/12.00 % (3759696)Instructions burned: 2174 (million)
% 80.60/12.00 % (3759698)ott-2_1_sil=16000:newcnf=on:random_seed=4233008617:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2928 on theBenchmark for (2928ds/869Mi)
% 80.60/12.00 % (3759698)Instruction limit reached!
% 80.60/12.00 % (3759698)------------------------------
% 80.60/12.00 % (3759698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.00 % (3759698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.00 % (3759698)CaDiCaL version: 2.1.3
% 80.60/12.00 % (3759698)Termination reason: Instruction limit
% 80.60/12.00 % (3759698)Termination phase: Saturation
% 80.60/12.00 % (3759698)Time elapsed: 0.705 s
% 80.60/12.00 % (3759698)Peak memory usage: 14 MB
% 80.60/12.00 % (3759698)Instructions burned: 869 (million)
% 80.60/12.00 % (3759700)ott+10_1_sil=32000:tgt=ground:random_seed=1258350806:i=5114:av=off_2921 on theBenchmark for (2921ds/5114Mi)
% 80.60/12.01 % (3759684)Instruction limit reached!
% 80.60/12.01 % (3759684)------------------------------
% 80.60/12.01 % (3759684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.01 % (3759684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.01 % (3759684)CaDiCaL version: 2.1.3
% 80.60/12.01 % (3759684)Termination reason: Instruction limit
% 80.60/12.01 % (3759684)Termination phase: Finite model building SAT solving
% 80.60/12.01 % (3759684)Time elapsed: 6.801 s
% 80.60/12.01 % (3759684)Peak memory usage: 60 MB
% 80.60/12.01 % (3759684)Instructions burned: 9515 (million)
% 80.60/12.01 % (3759702)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2957586067:i=54282_2917 on theBenchmark for (2917ds/54282Mi)
% 80.60/12.01 % TRYING [1]
% 80.60/12.01 % TRYING [2]
% 80.60/12.01 % TRYING [3]
% 80.60/12.01 % TRYING [4]
% 80.60/12.01 % (3759692)Instruction limit reached!
% 80.60/12.01 % (3759692)------------------------------
% 80.60/12.01 % (3759692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.01 % (3759692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.01 % (3759692)CaDiCaL version: 2.1.3
% 80.60/12.01 % (3759692)Termination reason: Instruction limit
% 80.60/12.01 % (3759692)Termination phase: Finite model building constraint generation
% 80.60/12.01 % (3759692)Time elapsed: 4.870 s
% 80.60/12.01 % (3759692)Peak memory usage: 550 MB
% 80.60/12.01 % (3759692)Instructions burned: 6325 (million)
% 80.60/12.01 % TRYING [5]
% 80.60/12.01 % (3759704)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=709123814:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi)
% 80.60/12.01 % TRYING [8]
% 80.60/12.01 % TRYING [6]
% 80.60/12.01 % (3759682)Instruction limit reached!
% 80.60/12.01 % (3759682)------------------------------
% 80.60/12.01 % (3759682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.01 % (3759682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.01 % (3759682)CaDiCaL version: 2.1.3
% 80.60/12.01 % (3759682)Termination reason: Instruction limit
% 80.60/12.01 % (3759682)Termination phase: Finite model building SAT solving
% 80.60/12.01 % (3759682)Time elapsed: 9.550 s
% 80.60/12.01 % (3759682)Peak memory usage: 17 MB
% 80.60/12.01 % (3759682)Instructions burned: 22061 (million)
% 80.60/12.01 % (3759706)dis+21_1_sil=32000:sas=cadical:random_seed=1442479504:i=3773:amm=off_2892 on theBenchmark for (2892ds/3773Mi)
% 80.60/12.01 % TRYING [7]
% 80.60/12.01 % (3759704)Instruction limit reached!
% 80.60/12.01 % (3759704)------------------------------
% 80.60/12.01 % (3759704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.01 % (3759704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.01 % (3759704)CaDiCaL version: 2.1.3
% 80.60/12.01 % (3759704)Termination reason: Instruction limit
% 80.60/12.01 % (3759704)Termination phase: Saturation
% 80.60/12.01 % (3759704)Time elapsed: 2.805 s
% 80.60/12.01 % (3759704)Peak memory usage: 29 MB
% 80.60/12.01 % (3759704)Instructions burned: 3513 (million)
% 80.60/12.01 % (3759708)ott+11_1_sil=16000:gs=on:random_seed=3295834997:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2885 on theBenchmark for (2885ds/2251Mi)
% 80.60/12.01 % (3759708) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3759643-3759708"...
% 80.60/12.01 % (3759708)...printing done.
% 80.60/12.01 % (3759708)Refutation found. Thanks to Tanya!
% 80.60/12.01 % SZS status Theorem for theBenchmark
% 80.60/12.01 % SZS output start Proof for theBenchmark
% See solution above
% 80.60/12.01 % (3759708)------------------------------
% 80.60/12.01 % (3759708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.60/12.01 % (3759708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.60/12.01 % (3759708)CaDiCaL version: 2.1.3
% 80.60/12.01 % (3759708)Termination reason: Refutation
% 80.60/12.01 % (3759708)Time elapsed: 0.063 s
% 80.60/12.01 % (3759708)Peak memory usage: 13 MB
% 80.60/12.01 % (3759708)Instructions burned: 57 (million)
% 80.60/12.01 % (3759643)Success in time 11.543 s
% 80.60/12.01 % Vampire exiting
%------------------------------------------------------------------------------