%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL676+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 12:00:01 PM UTC 2026
% Result : Theorem 59.19s 8.85s
% Output : Refutation 59.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 58
% Syntax : Number of formulae : 249 ( 14 unt; 56 def)
% Number of atoms : 1534 ( 0 equ)
% Maximal formula atoms : 123 ( 6 avg)
% Number of connectives : 2292 (1007 ~; 973 |; 293 &)
% ( 18 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 62 ( 61 usr; 19 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-1 aty)
% Number of variables : 634 ( 0 sgn 501 !; 133 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X0,X1)
& r1(X1,X2) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
fof(f3,conjecture,
~ ? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) ) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ p4(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ( ( ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ~ ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f4,negated_conjecture,
~ ~ ? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p3(X1) ) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1) )
| ~ p4(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p3(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ( ( ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ~ ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
~ ~ ? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ~ p3(X3) ) ) )
& ( ! [X4] :
( ~ r1(X0,X4)
| p2(X4) )
| ~ ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| p2(X7) )
| ~ p2(X6) ) ) ) )
| ! [X8] :
( ~ r1(X0,X8)
| p4(X8) )
| ~ ! [X9] :
( ~ r1(X0,X9)
| p4(X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| p4(X11) )
| ~ p4(X10) ) )
| ( ~ ! [X12] :
( ~ r1(X0,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ~ p3(X13) ) )
& ( ! [X14] :
( ~ r1(X0,X14)
| p2(X14) )
| ~ ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p2(X17) )
| ~ p2(X16) ) ) ) )
| ! [X18] :
( ~ r1(X0,X18)
| p1(X18) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ~ ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p1(X21) )
| ~ p1(X20) ) )
| ~ ( ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p2(X25) )
| ~ p2(X24) ) ) )
| ~ ! [X26] :
( ~ r1(X0,X26)
| p2(X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| p2(X30) )
| ~ p2(X29) ) ) )
| ~ ! [X31] :
( ~ r1(X0,X31)
| ( ( ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33)
| ~ ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
| ~ ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ~ ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ( p2(X31)
| ~ ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
| ~ ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X42,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ~ ! [X50] :
( ~ r1(X42,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) )
| ~ ( ( ! [X52] :
( ~ r1(X41,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
| ~ ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) )
& ( p2(X41)
| ~ ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) ) )
& ! [X61] :
( ~ r1(X0,X61)
| p2(X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| p2(X62)
| ~ ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p2(X64) )
| ~ p2(X63) ) ) ) ) ),
inference(rectify,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ~ p3(X3) ) ) )
& ( ! [X4] :
( ~ r1(X0,X4)
| p2(X4) )
| ~ ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| p2(X7) )
| ~ p2(X6) ) ) ) )
| ! [X8] :
( ~ r1(X0,X8)
| p4(X8) )
| ~ ! [X9] :
( ~ r1(X0,X9)
| p4(X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| p4(X11) )
| ~ p4(X10) ) )
| ( ~ ! [X12] :
( ~ r1(X0,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ~ p3(X13) ) )
& ( ! [X14] :
( ~ r1(X0,X14)
| p2(X14) )
| ~ ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p2(X17) )
| ~ p2(X16) ) ) ) )
| ! [X18] :
( ~ r1(X0,X18)
| p1(X18) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ~ ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p1(X21) )
| ~ p1(X20) ) )
| ~ ( ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p2(X25) )
| ~ p2(X24) ) ) )
| ~ ! [X26] :
( ~ r1(X0,X26)
| p2(X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| p2(X30) )
| ~ p2(X29) ) ) )
| ~ ! [X31] :
( ~ r1(X0,X31)
| ( ( ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33)
| ~ ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
| ~ ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ~ ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ( p2(X31)
| ~ ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
| ~ ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X42,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ~ ! [X50] :
( ~ r1(X42,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) )
| ~ ( ( ! [X52] :
( ~ r1(X41,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
| ~ ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) )
& ( p2(X41)
| ~ ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) ) )
& ! [X61] :
( ~ r1(X0,X61)
| p2(X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| p2(X62)
| ~ ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p2(X64) )
| ~ p2(X63) ) ) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f8,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(flattening,[],[f7]) ).
fof(f9,plain,
? [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p3(X3) ) ) )
| ( ? [X4] :
( r1(X0,X4)
& ~ p2(X4) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) ) )
& ? [X8] :
( r1(X0,X8)
& ~ p4(X8) )
& ! [X9] :
( ~ r1(X0,X9)
| p4(X9)
| ? [X10] :
( r1(X9,X10)
& ? [X11] :
( r1(X10,X11)
& ~ p4(X11) )
& p4(X10) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| ? [X13] :
( r1(X12,X13)
& p3(X13) ) )
| ( ? [X14] :
( r1(X0,X14)
& ~ p2(X14) )
& ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ? [X16] :
( r1(X15,X16)
& ? [X17] :
( r1(X16,X17)
& ~ p2(X17) )
& p2(X16) ) ) ) )
& ? [X18] :
( r1(X0,X18)
& ~ p1(X18) )
& ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ? [X20] :
( r1(X19,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p1(X21) )
& p1(X20) ) )
& ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ? [X24] :
( r1(X23,X24)
& ? [X25] :
( r1(X24,X25)
& ~ p2(X25) )
& p2(X24) ) ) )
| ? [X26] :
( r1(X0,X26)
& ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ? [X29] :
( r1(X0,X29)
& ? [X30] :
( r1(X29,X30)
& ~ p2(X30) )
& p2(X29) ) ) )
| ? [X31] :
( r1(X0,X31)
& ( ( ? [X32] :
( r1(X31,X32)
& ? [X33] :
( r1(X32,X33)
& ~ p2(X33)
& ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
& ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ? [X37] :
( r1(X36,X37)
& ? [X38] :
( r1(X37,X38)
& ~ p2(X38) )
& p2(X37) ) ) )
| ( ~ p2(X31)
& ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ~ p2(X46) )
& p2(X45) ) ) )
| ? [X47] :
( r1(X42,X47)
& ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ? [X50] :
( r1(X42,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51) )
& p2(X50) ) ) ) )
| ( ? [X52] :
( r1(X41,X52)
& ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
& ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ? [X57] :
( r1(X56,X57)
& ? [X58] :
( r1(X57,X58)
& ~ p2(X58) )
& p2(X57) ) ) )
| ( ~ p2(X41)
& ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) )
& ! [X61] :
( ~ r1(X0,X61)
| p2(X61)
| ? [X62] :
( r1(X61,X62)
& ~ p2(X62)
& ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p2(X64) )
| ~ p2(X63) ) ) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f10,plain,
? [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p3(X3) ) ) )
| ( ? [X4] :
( r1(X0,X4)
& ~ p2(X4) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) ) )
& ? [X8] :
( r1(X0,X8)
& ~ p4(X8) )
& ! [X9] :
( ~ r1(X0,X9)
| p4(X9)
| ? [X10] :
( r1(X9,X10)
& ? [X11] :
( r1(X10,X11)
& ~ p4(X11) )
& p4(X10) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| ? [X13] :
( r1(X12,X13)
& p3(X13) ) )
| ( ? [X14] :
( r1(X0,X14)
& ~ p2(X14) )
& ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ? [X16] :
( r1(X15,X16)
& ? [X17] :
( r1(X16,X17)
& ~ p2(X17) )
& p2(X16) ) ) ) )
& ? [X18] :
( r1(X0,X18)
& ~ p1(X18) )
& ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ? [X20] :
( r1(X19,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p1(X21) )
& p1(X20) ) )
& ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ? [X24] :
( r1(X23,X24)
& ? [X25] :
( r1(X24,X25)
& ~ p2(X25) )
& p2(X24) ) ) )
| ? [X26] :
( r1(X0,X26)
& ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ? [X29] :
( r1(X0,X29)
& ? [X30] :
( r1(X29,X30)
& ~ p2(X30) )
& p2(X29) ) ) )
| ? [X31] :
( r1(X0,X31)
& ( ( ? [X32] :
( r1(X31,X32)
& ? [X33] :
( r1(X32,X33)
& ~ p2(X33)
& ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
& ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ? [X37] :
( r1(X36,X37)
& ? [X38] :
( r1(X37,X38)
& ~ p2(X38) )
& p2(X37) ) ) )
| ( ~ p2(X31)
& ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ~ p2(X46) )
& p2(X45) ) ) )
| ? [X47] :
( r1(X42,X47)
& ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ? [X50] :
( r1(X42,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51) )
& p2(X50) ) ) ) )
| ( ? [X52] :
( r1(X41,X52)
& ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
& ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ? [X57] :
( r1(X56,X57)
& ? [X58] :
( r1(X57,X58)
& ~ p2(X58) )
& p2(X57) ) ) )
| ( ~ p2(X41)
& ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) )
& ! [X61] :
( ~ r1(X0,X61)
| p2(X61)
| ? [X62] :
( r1(X61,X62)
& ~ p2(X62)
& ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p2(X64) )
| ~ p2(X63) ) ) ) ),
inference(flattening,[],[f9]) ).
fof(f11,definition,
! [X61] :
( ? [X62] :
( r1(X61,X62)
& ~ p2(X62)
& ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p2(X64) )
| ~ p2(X63) ) )
| ~ sP0(X61) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X57] :
( ? [X58] :
( r1(X57,X58)
& ~ p2(X58) )
| ~ sP1(X57) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X56] :
( ? [X57] :
( r1(X56,X57)
& sP1(X57)
& p2(X57) )
| ~ sP2(X56) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X52] :
( ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) )
| ~ sP3(X52) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X41] :
( ? [X52] :
( r1(X41,X52)
& sP3(X52) )
| ~ sP4(X41) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X50] :
( ? [X51] :
( r1(X50,X51)
& ~ p2(X51) )
| ~ sP5(X50) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X42] :
( ? [X50] :
( r1(X42,X50)
& sP5(X50)
& p2(X50) )
| ~ sP6(X42) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X45] :
( ? [X46] :
( r1(X45,X46)
& ~ p2(X46) )
| ~ sP7(X45) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X44] :
( ? [X45] :
( r1(X44,X45)
& sP7(X45)
& p2(X45) )
| ~ sP8(X44) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X42] :
( ? [X47] :
( r1(X42,X47)
& ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) )
| ~ sP9(X42) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X41] :
( ( ~ p2(X41)
& ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) )
| ~ sP10(X41) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X41] :
( ( sP4(X41)
& ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| sP2(X56) ) )
| ~ sP11(X41) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X37] :
( ? [X38] :
( r1(X37,X38)
& ~ p2(X38) )
| ~ sP12(X37) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X36] :
( ? [X37] :
( r1(X36,X37)
& sP12(X37)
& p2(X37) )
| ~ sP13(X36) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X32] :
( ? [X33] :
( r1(X32,X33)
& ~ p2(X33)
& ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) )
| ~ sP14(X32) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X31] :
( ? [X32] :
( r1(X31,X32)
& sP14(X32) )
| ~ sP15(X31) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X31] :
( ( ~ p2(X31)
& ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) )
| ~ sP16(X31) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X31] :
( ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| sP8(X44) ) )
| sP9(X42) )
& ( p2(X42)
| sP6(X42) ) ) )
| sP11(X41)
| sP10(X41) )
| ~ sP17(X31) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X31] :
( ( sP15(X31)
& ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| sP13(X36) ) )
| sP16(X31)
| ~ sP18(X31) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X29] :
( ? [X30] :
( r1(X29,X30)
& ~ p2(X30) )
| ~ sP19(X29) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X0] :
( ? [X29] :
( r1(X0,X29)
& sP19(X29)
& p2(X29) )
| ~ sP20(X0) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X24] :
( ? [X25] :
( r1(X24,X25)
& ~ p2(X25) )
| ~ sP21(X24) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X23] :
( ? [X24] :
( r1(X23,X24)
& sP21(X24)
& p2(X24) )
| ~ sP22(X23) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X0] :
( ? [X26] :
( r1(X0,X26)
& ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) )
| ~ sP23(X0) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X0] :
( ? [X31] :
( r1(X0,X31)
& sP18(X31)
& sP17(X31) )
| ~ sP24(X0) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X20] :
( ? [X21] :
( r1(X20,X21)
& ~ p1(X21) )
| ~ sP25(X20) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f37,definition,
! [X19] :
( ? [X20] :
( r1(X19,X20)
& sP25(X20)
& p1(X20) )
| ~ sP26(X19) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X16] :
( ? [X17] :
( r1(X16,X17)
& ~ p2(X17) )
| ~ sP27(X16) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X15] :
( ? [X16] :
( r1(X15,X16)
& sP27(X16)
& p2(X16) )
| ~ sP28(X15) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X0] :
( ? [X14] :
( r1(X0,X14)
& ~ p2(X14) )
| ~ sP29(X0) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f41,definition,
! [X0] :
( ( sP29(X0)
& ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| sP28(X15) ) )
| ~ sP30(X0) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f42,definition,
! [X10] :
( ? [X11] :
( r1(X10,X11)
& ~ p4(X11) )
| ~ sP31(X10) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f43,definition,
! [X9] :
( ? [X10] :
( r1(X9,X10)
& sP31(X10)
& p4(X10) )
| ~ sP32(X9) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f44,definition,
! [X6] :
( ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
| ~ sP33(X6) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f45,definition,
! [X5] :
( ? [X6] :
( r1(X5,X6)
& sP33(X6)
& p2(X6) )
| ~ sP34(X5) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f46,definition,
! [X0] :
( ? [X4] :
( r1(X0,X4)
& ~ p2(X4) )
| ~ sP35(X0) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f47,definition,
! [X1] :
( ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p3(X3) ) )
| ~ sP36(X1) ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f48,definition,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& sP36(X1) )
| ~ sP37(X0) ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f49,plain,
? [X0] :
( ( sP37(X0)
| ( sP35(X0)
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| sP34(X5) ) ) )
& ? [X8] :
( r1(X0,X8)
& ~ p4(X8) )
& ! [X9] :
( ~ r1(X0,X9)
| p4(X9)
| sP32(X9) )
& ( ! [X12] :
( ~ r1(X0,X12)
| ? [X13] :
( r1(X12,X13)
& p3(X13) ) )
| sP30(X0) )
& ? [X18] :
( r1(X0,X18)
& ~ p1(X18) )
& ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| sP26(X19) )
& ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| sP22(X23) ) )
| sP23(X0) )
& ( p2(X0)
| sP20(X0) ) )
| sP24(X0) )
& ! [X61] :
( ~ r1(X0,X61)
| p2(X61)
| sP0(X61) ) ),
inference(definition_folding,[],[f10,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11]) ).
fof(f50,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& sP36(X1) )
| ~ sP37(X0) ),
inference(nnf_transformation,[],[f48]) ).
fof(f51,plain,
! [X0] :
( ( r1(X0,sK38(X0))
& ~ p1(sK38(X0))
& sP36(sK38(X0)) )
| ~ sP37(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X1,sK38(X0))],[f50]) ).
fof(f52,plain,
! [X1] :
( ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p3(X3) ) )
| ~ sP36(X1) ),
inference(nnf_transformation,[],[f47]) ).
fof(f53,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ! [X2] :
( ~ r1(X1,X2)
| ~ p3(X2) ) )
| ~ sP36(X0) ),
inference(rectify,[],[f52]) ).
fof(f54,plain,
! [X0] :
( ( r1(X0,sK39(X0))
& ! [X2] :
( ~ r1(sK39(X0),X2)
| ~ p3(X2) ) )
| ~ sP36(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(X1,sK39(X0))],[f53]) ).
fof(f55,plain,
! [X0] :
( ? [X4] :
( r1(X0,X4)
& ~ p2(X4) )
| ~ sP35(X0) ),
inference(nnf_transformation,[],[f46]) ).
fof(f56,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1) )
| ~ sP35(X0) ),
inference(rectify,[],[f55]) ).
fof(f57,plain,
! [X0] :
( ( r1(X0,sK40(X0))
& ~ p2(sK40(X0)) )
| ~ sP35(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(X1,sK40(X0))],[f56]) ).
fof(f58,plain,
! [X5] :
( ? [X6] :
( r1(X5,X6)
& sP33(X6)
& p2(X6) )
| ~ sP34(X5) ),
inference(nnf_transformation,[],[f45]) ).
fof(f59,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& sP33(X1)
& p2(X1) )
| ~ sP34(X0) ),
inference(rectify,[],[f58]) ).
fof(f60,plain,
! [X0] :
( ( r1(X0,sK41(X0))
& sP33(sK41(X0))
& p2(sK41(X0)) )
| ~ sP34(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X1,sK41(X0))],[f59]) ).
fof(f61,plain,
! [X6] :
( ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
| ~ sP33(X6) ),
inference(nnf_transformation,[],[f44]) ).
fof(f62,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1) )
| ~ sP33(X0) ),
inference(rectify,[],[f61]) ).
fof(f63,plain,
! [X0] :
( ( r1(X0,sK42(X0))
& ~ p2(sK42(X0)) )
| ~ sP33(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X1,sK42(X0))],[f62]) ).
fof(f70,plain,
! [X0] :
( ( sP29(X0)
& ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| sP28(X15) ) )
| ~ sP30(X0) ),
inference(nnf_transformation,[],[f41]) ).
fof(f71,plain,
! [X0] :
( ( sP29(X0)
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| sP28(X1) ) )
| ~ sP30(X0) ),
inference(rectify,[],[f70]) ).
fof(f72,plain,
! [X0] :
( ? [X14] :
( r1(X0,X14)
& ~ p2(X14) )
| ~ sP29(X0) ),
inference(nnf_transformation,[],[f40]) ).
fof(f73,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1) )
| ~ sP29(X0) ),
inference(rectify,[],[f72]) ).
fof(f74,plain,
! [X0] :
( ( r1(X0,sK45(X0))
& ~ p2(sK45(X0)) )
| ~ sP29(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(X1,sK45(X0))],[f73]) ).
fof(f75,plain,
! [X15] :
( ? [X16] :
( r1(X15,X16)
& sP27(X16)
& p2(X16) )
| ~ sP28(X15) ),
inference(nnf_transformation,[],[f39]) ).
fof(f76,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& sP27(X1)
& p2(X1) )
| ~ sP28(X0) ),
inference(rectify,[],[f75]) ).
fof(f77,plain,
! [X0] :
( ( r1(X0,sK46(X0))
& sP27(sK46(X0))
& p2(sK46(X0)) )
| ~ sP28(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(X1,sK46(X0))],[f76]) ).
fof(f78,plain,
! [X16] :
( ? [X17] :
( r1(X16,X17)
& ~ p2(X17) )
| ~ sP27(X16) ),
inference(nnf_transformation,[],[f38]) ).
fof(f79,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1) )
| ~ sP27(X0) ),
inference(rectify,[],[f78]) ).
fof(f80,plain,
! [X0] :
( ( r1(X0,sK47(X0))
& ~ p2(sK47(X0)) )
| ~ sP27(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(X1,sK47(X0))],[f79]) ).
fof(f154,plain,
! [X61] :
( ? [X62] :
( r1(X61,X62)
& ~ p2(X62)
& ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p2(X64) )
| ~ p2(X63) ) )
| ~ sP0(X61) ),
inference(nnf_transformation,[],[f11]) ).
fof(f155,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p2(X3) )
| ~ p2(X2) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f154]) ).
fof(f156,plain,
! [X0] :
( ( r1(X0,sK69(X0))
& ~ p2(sK69(X0))
& ! [X2] :
( ~ r1(sK69(X0),X2)
| ! [X3] :
( ~ r1(X2,X3)
| p2(X3) )
| ~ p2(X2) ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69]),skolemize(X1,sK69(X0))],[f155]) ).
fof(f157,plain,
? [X0] :
( ( sP37(X0)
| ( sP35(X0)
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| sP34(X1) ) ) )
& ? [X2] :
( r1(X0,X2)
& ~ p4(X2) )
& ! [X3] :
( ~ r1(X0,X3)
| p4(X3)
| sP32(X3) )
& ( ! [X4] :
( ~ r1(X0,X4)
| ? [X5] :
( r1(X4,X5)
& p3(X5) ) )
| sP30(X0) )
& ? [X6] :
( r1(X0,X6)
& ~ p1(X6) )
& ! [X7] :
( ~ r1(X0,X7)
| p1(X7)
| sP26(X7) )
& ( ( ( ! [X8] :
( ~ r1(X0,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p2(X9)
| sP22(X9) ) )
| sP23(X0) )
& ( p2(X0)
| sP20(X0) ) )
| sP24(X0) )
& ! [X10] :
( ~ r1(X0,X10)
| p2(X10)
| sP0(X10) ) ),
inference(rectify,[],[f49]) ).
fof(f158,plain,
( ( sP37(sK70)
| ( sP35(sK70)
& ! [X1] :
( ~ r1(sK70,X1)
| p2(X1)
| sP34(X1) ) ) )
& r1(sK70,sK71)
& ~ p4(sK71)
& ! [X3] :
( ~ r1(sK70,X3)
| p4(X3)
| sP32(X3) )
& ( ! [X4] :
( ~ r1(sK70,X4)
| ( r1(X4,sK72(X4))
& p3(sK72(X4)) ) )
| sP30(sK70) )
& r1(sK70,sK73)
& ~ p1(sK73)
& ! [X7] :
( ~ r1(sK70,X7)
| p1(X7)
| sP26(X7) )
& ( ( ( ! [X8] :
( ~ r1(sK70,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p2(X9)
| sP22(X9) ) )
| sP23(sK70) )
& ( p2(sK70)
| sP20(sK70) ) )
| sP24(sK70) )
& ! [X10] :
( ~ r1(sK70,X10)
| p2(X10)
| sP0(X10) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70,sK71,sK72,sK73]),skolemize(X0,sK70),skolemize(X2,sK71),skolemize(X5,sK72(X4)),skolemize(X6,sK73)],[f157]) ).
fof(f160,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f161,plain,
! [X0] :
( sP36(sK38(X0))
| ~ sP37(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f163,plain,
! [X0] :
( ~ sP37(X0)
| r1(X0,sK38(X0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f164,plain,
! [X2,X0] :
( ~ p3(X2)
| ~ r1(sK39(X0),X2)
| ~ sP36(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f165,plain,
! [X0] :
( ~ sP36(X0)
| r1(X0,sK39(X0)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f166,plain,
! [X0] :
( ~ p2(sK40(X0))
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f167,plain,
! [X0] :
( ~ sP35(X0)
| r1(X0,sK40(X0)) ),
inference(cnf_transformation,[],[f57]) ).
fof(f168,plain,
! [X0] :
( p2(sK41(X0))
| ~ sP34(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f169,plain,
! [X0] :
( sP33(sK41(X0))
| ~ sP34(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f170,plain,
! [X0] :
( ~ sP34(X0)
| r1(X0,sK41(X0)) ),
inference(cnf_transformation,[],[f60]) ).
fof(f171,plain,
! [X0] :
( ~ p2(sK42(X0))
| ~ sP33(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f172,plain,
! [X0] :
( ~ sP33(X0)
| r1(X0,sK42(X0)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f178,plain,
! [X0,X1] :
( ~ sP30(X0)
| p2(X1)
| sP28(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f71]) ).
fof(f179,plain,
! [X0] :
( sP29(X0)
| ~ sP30(X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f180,plain,
! [X0] :
( ~ p2(sK45(X0))
| ~ sP29(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f181,plain,
! [X0] :
( ~ sP29(X0)
| r1(X0,sK45(X0)) ),
inference(cnf_transformation,[],[f74]) ).
fof(f182,plain,
! [X0] :
( p2(sK46(X0))
| ~ sP28(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f183,plain,
! [X0] :
( sP27(sK46(X0))
| ~ sP28(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f184,plain,
! [X0] :
( ~ sP28(X0)
| r1(X0,sK46(X0)) ),
inference(cnf_transformation,[],[f77]) ).
fof(f185,plain,
! [X0] :
( ~ p2(sK47(X0))
| ~ sP27(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f186,plain,
! [X0] :
( ~ sP27(X0)
| r1(X0,sK47(X0)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f251,plain,
! [X2,X3,X0] :
( ~ r1(sK69(X0),X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f156]) ).
fof(f252,plain,
! [X0] :
( ~ p2(sK69(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f156]) ).
fof(f253,plain,
! [X0] :
( ~ sP0(X0)
| r1(X0,sK69(X0)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f254,plain,
! [X10] :
( ~ r1(sK70,X10)
| p2(X10)
| sP0(X10) ),
inference(cnf_transformation,[],[f158]) ).
fof(f260,plain,
! [X4] :
( ~ r1(sK70,X4)
| p3(sK72(X4))
| sP30(sK70) ),
inference(cnf_transformation,[],[f158]) ).
fof(f261,plain,
! [X4] :
( ~ r1(sK70,X4)
| r1(X4,sK72(X4))
| sP30(sK70) ),
inference(cnf_transformation,[],[f158]) ).
fof(f265,plain,
! [X1] :
( sP37(sK70)
| ~ r1(sK70,X1)
| p2(X1)
| sP34(X1) ),
inference(cnf_transformation,[],[f158]) ).
fof(f266,plain,
( sP37(sK70)
| sP35(sK70) ),
inference(cnf_transformation,[],[f158]) ).
fof(f289,definition,
( spl74_6
<=> sP30(sK70) ),
introduced(definition,[new_symbols(definition,[spl74_6])],[avatar_definition]) ).
fof(f291,plain,
( sP30(sK70)
| ~ spl74_6 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl74_7
<=> ! [X4] :
( ~ r1(sK70,X4)
| p3(sK72(X4)) ) ),
introduced(definition,[new_symbols(definition,[spl74_7])],[avatar_definition]) ).
fof(f294,plain,
( ! [X4] :
( ~ r1(sK70,X4)
| p3(sK72(X4)) )
| ~ spl74_7 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f295,plain,
( spl74_6
| spl74_7 ),
inference(avatar_split_clause,[],[f260,f293,f289]) ).
fof(f297,definition,
( spl74_8
<=> ! [X4] :
( ~ r1(sK70,X4)
| r1(X4,sK72(X4)) ) ),
introduced(definition,[new_symbols(definition,[spl74_8])],[avatar_definition]) ).
fof(f298,plain,
( ! [X4] :
( ~ r1(sK70,X4)
| r1(X4,sK72(X4)) )
| ~ spl74_8 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f299,plain,
( spl74_6
| spl74_8 ),
inference(avatar_split_clause,[],[f261,f297,f289]) ).
fof(f301,definition,
( spl74_9
<=> ! [X1] :
( ~ r1(sK70,X1)
| sP34(X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl74_9])],[avatar_definition]) ).
fof(f302,plain,
( ! [X1] :
( ~ r1(sK70,X1)
| sP34(X1)
| p2(X1) )
| ~ spl74_9 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,definition,
( spl74_10
<=> sP37(sK70) ),
introduced(definition,[new_symbols(definition,[spl74_10])],[avatar_definition]) ).
fof(f306,plain,
( sP37(sK70)
| ~ spl74_10 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f307,plain,
( spl74_9
| spl74_10 ),
inference(avatar_split_clause,[],[f265,f304,f301]) ).
fof(f309,definition,
( spl74_11
<=> sP35(sK70) ),
introduced(definition,[new_symbols(definition,[spl74_11])],[avatar_definition]) ).
fof(f311,plain,
( sP35(sK70)
| ~ spl74_11 ),
inference(avatar_component_clause,[],[f309]) ).
fof(f312,plain,
( spl74_11
| spl74_10 ),
inference(avatar_split_clause,[],[f266,f304,f309]) ).
fof(f433,plain,
! [X0] :
( r1(sK38(X0),sK39(sK38(X0)))
| ~ sP37(X0) ),
inference(resolution,[],[f165,f161]) ).
fof(f434,plain,
( r1(sK70,sK40(sK70))
| ~ spl74_11 ),
inference(resolution,[],[f167,f311]) ).
fof(f438,plain,
( p2(sK40(sK70))
| sP0(sK40(sK70))
| ~ spl74_11 ),
inference(resolution,[],[f434,f254]) ).
fof(f441,definition,
( spl74_33
<=> sP0(sK40(sK70)) ),
introduced(definition,[new_symbols(definition,[spl74_33])],[avatar_definition]) ).
fof(f443,plain,
( sP0(sK40(sK70))
| ~ spl74_33 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f445,definition,
( spl74_34
<=> p2(sK40(sK70)) ),
introduced(definition,[new_symbols(definition,[spl74_34])],[avatar_definition]) ).
fof(f447,plain,
( p2(sK40(sK70))
| ~ spl74_34 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f448,plain,
( spl74_33
| spl74_34
| ~ spl74_11 ),
inference(avatar_split_clause,[],[f438,f309,f445,f441]) ).
fof(f472,plain,
( r1(sK70,sK38(sK70))
| ~ spl74_10 ),
inference(resolution,[],[f306,f163]) ).
fof(f473,plain,
! [X0] :
( ~ sP34(X0)
| r1(sK41(X0),sK42(sK41(X0))) ),
inference(resolution,[],[f172,f169]) ).
fof(f489,plain,
! [X0] :
( ~ sP30(X0)
| r1(X0,sK45(X0)) ),
inference(resolution,[],[f181,f179]) ).
fof(f491,plain,
! [X0] :
( ~ sP28(X0)
| r1(sK46(X0),sK47(sK46(X0))) ),
inference(resolution,[],[f186,f183]) ).
fof(f865,plain,
( ! [X0] :
( ~ r1(sK70,X0)
| sP28(X0)
| p2(X0) )
| ~ spl74_6 ),
inference(resolution,[],[f291,f178]) ).
fof(f948,plain,
( r1(sK70,sK45(sK70))
| ~ spl74_6 ),
inference(resolution,[],[f489,f291]) ).
fof(f949,plain,
( p2(sK45(sK70))
| sP0(sK45(sK70))
| ~ spl74_6 ),
inference(resolution,[],[f948,f254]) ).
fof(f958,definition,
( spl74_105
<=> p2(sK45(sK70)) ),
introduced(definition,[new_symbols(definition,[spl74_105])],[avatar_definition]) ).
fof(f960,plain,
( p2(sK45(sK70))
| ~ spl74_105 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f990,definition,
( spl74_112
<=> sP0(sK45(sK70)) ),
introduced(definition,[new_symbols(definition,[spl74_112])],[avatar_definition]) ).
fof(f992,plain,
( sP0(sK45(sK70))
| ~ spl74_112 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f993,plain,
( spl74_112
| spl74_105
| ~ spl74_6 ),
inference(avatar_split_clause,[],[f949,f289,f958,f990]) ).
fof(f994,plain,
! [X0,X1] :
( ~ sP37(X0)
| ~ r1(X1,sK38(X0))
| r1(X1,sK39(sK38(X0))) ),
inference(resolution,[],[f433,f160]) ).
fof(f995,plain,
( ~ sP29(sK70)
| ~ spl74_105 ),
inference(resolution,[],[f960,f180]) ).
fof(f996,plain,
( ~ sP30(sK70)
| ~ spl74_105 ),
inference(resolution,[],[f995,f179]) ).
fof(f997,plain,
( ~ spl74_6
| ~ spl74_105 ),
inference(avatar_split_clause,[],[f996,f958,f289]) ).
fof(f1004,plain,
( r1(sK45(sK70),sK69(sK45(sK70)))
| ~ spl74_112 ),
inference(resolution,[],[f992,f253]) ).
fof(f1049,plain,
( ! [X0] :
( ~ r1(X0,sK45(sK70))
| r1(X0,sK69(sK45(sK70))) )
| ~ spl74_112 ),
inference(resolution,[],[f1004,f160]) ).
fof(f1133,plain,
( ! [X0] :
( ~ r1(X0,sK38(sK70))
| r1(X0,sK39(sK38(sK70))) )
| ~ spl74_10 ),
inference(resolution,[],[f994,f306]) ).
fof(f1169,definition,
( spl74_134
<=> p2(sK69(sK45(sK70))) ),
introduced(definition,[new_symbols(definition,[spl74_134])],[avatar_definition]) ).
fof(f1171,plain,
( p2(sK69(sK45(sK70)))
| ~ spl74_134 ),
inference(avatar_component_clause,[],[f1169]) ).
fof(f1191,plain,
( ~ sP0(sK45(sK70))
| ~ spl74_134 ),
inference(resolution,[],[f1171,f252]) ).
fof(f1192,plain,
( ~ spl74_112
| ~ spl74_134 ),
inference(avatar_split_clause,[],[f1191,f1169,f990]) ).
fof(f1194,plain,
( r1(sK70,sK39(sK38(sK70)))
| ~ spl74_10 ),
inference(resolution,[],[f1133,f472]) ).
fof(f1213,plain,
( p3(sK72(sK39(sK38(sK70))))
| ~ spl74_7
| ~ spl74_10 ),
inference(resolution,[],[f1194,f294]) ).
fof(f1921,plain,
( r1(sK70,sK69(sK45(sK70)))
| ~ spl74_6
| ~ spl74_112 ),
inference(resolution,[],[f1049,f948]) ).
fof(f1998,plain,
( sP28(sK69(sK45(sK70)))
| p2(sK69(sK45(sK70)))
| ~ spl74_6
| ~ spl74_112 ),
inference(resolution,[],[f1921,f865]) ).
fof(f2001,definition,
( spl74_247
<=> sP28(sK69(sK45(sK70))) ),
introduced(definition,[new_symbols(definition,[spl74_247])],[avatar_definition]) ).
fof(f2003,plain,
( sP28(sK69(sK45(sK70)))
| ~ spl74_247 ),
inference(avatar_component_clause,[],[f2001]) ).
fof(f2004,plain,
( spl74_134
| spl74_247
| ~ spl74_6
| ~ spl74_112 ),
inference(avatar_split_clause,[],[f1998,f990,f289,f2001,f1169]) ).
fof(f2031,plain,
( r1(sK46(sK69(sK45(sK70))),sK47(sK46(sK69(sK45(sK70)))))
| ~ spl74_247 ),
inference(resolution,[],[f2003,f491]) ).
fof(f2032,plain,
( r1(sK69(sK45(sK70)),sK46(sK69(sK45(sK70))))
| ~ spl74_247 ),
inference(resolution,[],[f2003,f184]) ).
fof(f2474,plain,
( r1(sK70,sK40(sK70))
| ~ spl74_11 ),
inference(resolution,[],[f311,f167]) ).
fof(f2475,plain,
( r1(sK40(sK70),sK69(sK40(sK70)))
| ~ spl74_33 ),
inference(resolution,[],[f443,f253]) ).
fof(f2533,plain,
( ~ sP35(sK70)
| ~ spl74_34 ),
inference(resolution,[],[f447,f166]) ).
fof(f2534,plain,
( ~ spl74_11
| ~ spl74_34 ),
inference(avatar_split_clause,[],[f2533,f445,f309]) ).
fof(f2552,plain,
( ! [X0] :
( ~ r1(X0,sK40(sK70))
| r1(X0,sK69(sK40(sK70))) )
| ~ spl74_33 ),
inference(resolution,[],[f2475,f160]) ).
fof(f2558,definition,
( spl74_319
<=> p2(sK69(sK40(sK70))) ),
introduced(definition,[new_symbols(definition,[spl74_319])],[avatar_definition]) ).
fof(f2560,plain,
( p2(sK69(sK40(sK70)))
| ~ spl74_319 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2562,plain,
( ~ sP0(sK40(sK70))
| ~ spl74_319 ),
inference(resolution,[],[f2560,f252]) ).
fof(f2563,plain,
( ~ spl74_33
| ~ spl74_319 ),
inference(avatar_split_clause,[],[f2562,f2558,f441]) ).
fof(f2663,plain,
( r1(sK70,sK69(sK40(sK70)))
| ~ spl74_11
| ~ spl74_33 ),
inference(resolution,[],[f2552,f2474]) ).
fof(f2669,plain,
( sP34(sK69(sK40(sK70)))
| p2(sK69(sK40(sK70)))
| ~ spl74_9
| ~ spl74_11
| ~ spl74_33 ),
inference(resolution,[],[f2663,f302]) ).
fof(f2679,definition,
( spl74_335
<=> sP34(sK69(sK40(sK70))) ),
introduced(definition,[new_symbols(definition,[spl74_335])],[avatar_definition]) ).
fof(f2681,plain,
( sP34(sK69(sK40(sK70)))
| ~ spl74_335 ),
inference(avatar_component_clause,[],[f2679]) ).
fof(f2682,plain,
( spl74_319
| spl74_335
| ~ spl74_9
| ~ spl74_11
| ~ spl74_33 ),
inference(avatar_split_clause,[],[f2669,f441,f309,f301,f2679,f2558]) ).
fof(f2713,plain,
( r1(sK69(sK40(sK70)),sK41(sK69(sK40(sK70))))
| ~ spl74_335 ),
inference(resolution,[],[f2681,f170]) ).
fof(f3455,plain,
( ! [X0] :
( ~ r1(X0,sK38(sK70))
| r1(X0,sK39(sK38(sK70))) )
| ~ spl74_10 ),
inference(resolution,[],[f306,f994]) ).
fof(f3456,plain,
( r1(sK70,sK38(sK70))
| ~ spl74_10 ),
inference(resolution,[],[f306,f163]) ).
fof(f3476,plain,
( ! [X0] :
( ~ r1(sK39(X0),sK72(sK39(sK38(sK70))))
| ~ sP36(X0) )
| ~ spl74_7
| ~ spl74_10 ),
inference(resolution,[],[f1213,f164]) ).
fof(f3479,plain,
( r1(sK70,sK39(sK38(sK70)))
| ~ spl74_10 ),
inference(resolution,[],[f3455,f3456]) ).
fof(f3854,plain,
( ! [X0] :
( ~ r1(sK41(sK69(sK40(sK70))),X0)
| p2(X0)
| ~ p2(sK41(sK69(sK40(sK70))))
| ~ sP0(sK40(sK70)) )
| ~ spl74_335 ),
inference(resolution,[],[f2713,f251]) ).
fof(f3857,definition,
( spl74_474
<=> p2(sK41(sK69(sK40(sK70)))) ),
introduced(definition,[new_symbols(definition,[spl74_474])],[avatar_definition]) ).
fof(f3859,plain,
( ~ p2(sK41(sK69(sK40(sK70))))
| spl74_474 ),
inference(avatar_component_clause,[],[f3857]) ).
fof(f3861,definition,
( spl74_475
<=> ! [X0] :
( ~ r1(sK41(sK69(sK40(sK70))),X0)
| p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl74_475])],[avatar_definition]) ).
fof(f3862,plain,
( ! [X0] :
( ~ r1(sK41(sK69(sK40(sK70))),X0)
| p2(X0) )
| ~ spl74_475 ),
inference(avatar_component_clause,[],[f3861]) ).
fof(f3863,plain,
( ~ spl74_33
| ~ spl74_474
| spl74_475
| ~ spl74_335 ),
inference(avatar_split_clause,[],[f3854,f2679,f3861,f3857,f441]) ).
fof(f3874,plain,
( ~ sP34(sK69(sK40(sK70)))
| spl74_474 ),
inference(resolution,[],[f3859,f168]) ).
fof(f3875,plain,
( ~ spl74_335
| spl74_474 ),
inference(avatar_split_clause,[],[f3874,f3857,f2679]) ).
fof(f3900,plain,
( r1(sK39(sK38(sK70)),sK72(sK39(sK38(sK70))))
| ~ spl74_8
| ~ spl74_10 ),
inference(resolution,[],[f298,f3479]) ).
fof(f5018,plain,
( ~ sP36(sK38(sK70))
| ~ spl74_7
| ~ spl74_8
| ~ spl74_10 ),
inference(resolution,[],[f3900,f3476]) ).
fof(f5033,plain,
( ~ sP37(sK70)
| ~ spl74_7
| ~ spl74_8
| ~ spl74_10 ),
inference(resolution,[],[f5018,f161]) ).
fof(f5034,plain,
( $false
| ~ spl74_7
| ~ spl74_8
| ~ spl74_10 ),
inference(global_subsumption,[],[f5033,f306]) ).
fof(f5035,plain,
( ~ spl74_7
| ~ spl74_8
| ~ spl74_10 ),
inference(avatar_contradiction_clause,[],[f5034]) ).
fof(f5175,plain,
( r1(sK41(sK69(sK40(sK70))),sK42(sK41(sK69(sK40(sK70)))))
| ~ spl74_335 ),
inference(resolution,[],[f2681,f473]) ).
fof(f5635,plain,
( ! [X0] :
( ~ r1(sK46(sK69(sK45(sK70))),X0)
| p2(X0)
| ~ p2(sK46(sK69(sK45(sK70))))
| ~ sP0(sK45(sK70)) )
| ~ spl74_247 ),
inference(resolution,[],[f2032,f251]) ).
fof(f7216,plain,
( p2(sK42(sK41(sK69(sK40(sK70)))))
| ~ spl74_335
| ~ spl74_475 ),
inference(resolution,[],[f5175,f3862]) ).
fof(f7219,plain,
( ~ sP33(sK41(sK69(sK40(sK70))))
| ~ spl74_335
| ~ spl74_475 ),
inference(resolution,[],[f7216,f171]) ).
fof(f7221,plain,
( ~ sP34(sK69(sK40(sK70)))
| ~ spl74_335
| ~ spl74_475 ),
inference(resolution,[],[f7219,f169]) ).
fof(f7222,plain,
( $false
| ~ spl74_335
| ~ spl74_475 ),
inference(global_subsumption,[],[f7221,f2681]) ).
fof(f7223,plain,
( ~ spl74_335
| ~ spl74_475 ),
inference(avatar_contradiction_clause,[],[f7222]) ).
fof(f7225,definition,
( spl74_820
<=> p2(sK46(sK69(sK45(sK70)))) ),
introduced(definition,[new_symbols(definition,[spl74_820])],[avatar_definition]) ).
fof(f7227,plain,
( ~ p2(sK46(sK69(sK45(sK70))))
| spl74_820 ),
inference(avatar_component_clause,[],[f7225]) ).
fof(f7229,definition,
( spl74_821
<=> ! [X0] :
( ~ r1(sK46(sK69(sK45(sK70))),X0)
| p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl74_821])],[avatar_definition]) ).
fof(f7230,plain,
( ! [X0] :
( ~ r1(sK46(sK69(sK45(sK70))),X0)
| p2(X0) )
| ~ spl74_821 ),
inference(avatar_component_clause,[],[f7229]) ).
fof(f7231,plain,
( ~ spl74_112
| ~ spl74_820
| spl74_821
| ~ spl74_247 ),
inference(avatar_split_clause,[],[f5635,f2001,f7229,f7225,f990]) ).
fof(f7331,plain,
( ~ sP28(sK69(sK45(sK70)))
| spl74_820 ),
inference(resolution,[],[f7227,f182]) ).
fof(f7332,plain,
( ~ spl74_247
| spl74_820 ),
inference(avatar_split_clause,[],[f7331,f7225,f2001]) ).
fof(f8526,plain,
( p2(sK47(sK46(sK69(sK45(sK70)))))
| ~ spl74_247
| ~ spl74_821 ),
inference(resolution,[],[f2031,f7230]) ).
fof(f8541,plain,
( ~ sP27(sK46(sK69(sK45(sK70))))
| ~ spl74_247
| ~ spl74_821 ),
inference(resolution,[],[f8526,f185]) ).
fof(f8555,plain,
( ~ sP28(sK69(sK45(sK70)))
| ~ spl74_247
| ~ spl74_821 ),
inference(resolution,[],[f8541,f183]) ).
fof(f8556,plain,
( $false
| ~ spl74_247
| ~ spl74_821 ),
inference(global_subsumption,[],[f8555,f2003]) ).
fof(f8557,plain,
( ~ spl74_247
| ~ spl74_821 ),
inference(avatar_contradiction_clause,[],[f8556]) ).
cnf(s10,plain,
( spl74_6
| spl74_7 ),
inference(sat_conversion,[],[f295]) ).
cnf(s12,plain,
( spl74_6
| spl74_8 ),
inference(sat_conversion,[],[f299]) ).
cnf(s17,plain,
( spl74_9
| spl74_10 ),
inference(sat_conversion,[],[f307]) ).
cnf(s19,plain,
( spl74_10
| spl74_11 ),
inference(sat_conversion,[],[f312]) ).
cnf(s167,plain,
( ~ spl74_11
| spl74_33
| spl74_34 ),
inference(sat_conversion,[],[f448]) ).
cnf(s414,plain,
( ~ spl74_6
| spl74_105
| spl74_112 ),
inference(sat_conversion,[],[f993]) ).
cnf(s421,plain,
( ~ spl74_6
| ~ spl74_105 ),
inference(sat_conversion,[],[f997]) ).
cnf(s523,plain,
( ~ spl74_112
| ~ spl74_134 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s892,plain,
( ~ spl74_6
| ~ spl74_112
| spl74_134
| spl74_247 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s1164,plain,
( ~ spl74_11
| ~ spl74_34 ),
inference(sat_conversion,[],[f2534]) ).
cnf(s1187,plain,
( ~ spl74_33
| ~ spl74_319 ),
inference(sat_conversion,[],[f2563]) ).
cnf(s1243,plain,
( ~ spl74_9
| ~ spl74_11
| ~ spl74_33
| spl74_319
| spl74_335 ),
inference(sat_conversion,[],[f2682]) ).
cnf(s1849,plain,
( ~ spl74_33
| ~ spl74_335
| ~ spl74_474
| spl74_475 ),
inference(sat_conversion,[],[f3863]) ).
cnf(s1856,plain,
( ~ spl74_335
| spl74_474 ),
inference(sat_conversion,[],[f3875]) ).
cnf(s2392,plain,
( ~ spl74_7
| ~ spl74_8
| ~ spl74_10 ),
inference(sat_conversion,[],[f5035]) ).
cnf(s3366,plain,
( ~ spl74_335
| ~ spl74_475 ),
inference(sat_conversion,[],[f7223]) ).
cnf(s3375,plain,
( ~ spl74_112
| ~ spl74_247
| ~ spl74_820
| spl74_821 ),
inference(sat_conversion,[],[f7231]) ).
cnf(s3425,plain,
( ~ spl74_247
| spl74_820 ),
inference(sat_conversion,[],[f7332]) ).
cnf(s3891,plain,
( ~ spl74_247
| ~ spl74_821 ),
inference(sat_conversion,[],[f8557]) ).
cnf(s3899,plain,
( spl74_134
| ~ spl74_112
| ~ spl74_6 ),
inference(rat,[],[s3375,s3425,s3891,s892]) ).
cnf(s3900,plain,
( spl74_105
| ~ spl74_6 ),
inference(rat,[],[s3899,s523,s414]) ).
cnf(s3901,plain,
~ spl74_6,
inference(rat,[],[s3900,s421]) ).
cnf(s3902,plain,
spl74_8,
inference(rat,[],[s12,s3901]) ).
cnf(s3903,plain,
spl74_7,
inference(rat,[],[s10,s3901]) ).
cnf(s3904,plain,
~ spl74_10,
inference(rat,[],[s2392,s3902,s3903]) ).
cnf(s3905,plain,
spl74_11,
inference(rat,[],[s19,s3904]) ).
cnf(s3906,plain,
spl74_9,
inference(rat,[],[s17,s3904]) ).
cnf(s3907,plain,
~ spl74_34,
inference(rat,[],[s1164,s3905]) ).
cnf(s3909,plain,
spl74_33,
inference(rat,[],[s167,s3905,s3907]) ).
cnf(s3911,plain,
~ spl74_319,
inference(rat,[],[s1187,s3909]) ).
cnf(s3915,plain,
spl74_335,
inference(rat,[],[s1243,s3909,s3906,s3905,s3911]) ).
cnf(s3916,plain,
~ spl74_475,
inference(rat,[],[s3366,s3915]) ).
cnf(s3917,plain,
spl74_474,
inference(rat,[],[s1856,s3915]) ).
cnf(s3918,plain,
$false,
inference(rat,[],[s1849,s3916,s3909,s3917,s3915]) ).
fof(f8558,plain,
$false,
inference(avatar_sat_refutation,[],[s3918]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL676+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n026.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 16:36:11 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.42 Running first-order model finding
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.08/2.89 % (3051254)Will run a generic schedule for satisfiability detection.
% 16.08/2.89 % (3051261)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3166474941:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.08/2.89 % (3051260)% WARNING: option uhcvi not known.
% 16.08/2.89 % (3051259)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=838675699_2999 on theBenchmark for (2999ds/0Mi)
% 16.08/2.89 % (3051260)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3217747014:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.08/2.89 % (3051262)dis+10_1_sil=32000:sp=arity:random_seed=3955531375:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.08/2.89 % (3051264)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3848235369:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.08/2.89 % (3051263)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2188713953:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.08/2.89 % (3051265)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3655421532:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.08/2.89 % TRYING [1]
% 16.08/2.89 % TRYING [2]
% 16.08/2.89 % TRYING [3]
% 16.08/2.89 % TRYING [4]
% 16.08/2.89 % TRYING [5]
% 16.08/2.89 % (3051262)Instruction limit reached!
% 16.08/2.89 % (3051262)------------------------------
% 16.08/2.89 % (3051262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.08/2.89 % (3051262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.08/2.89 % (3051262)CaDiCaL version: 2.1.3
% 16.08/2.89 % (3051262)Termination reason: Instruction limit
% 16.08/2.89 % (3051262)Termination phase: Saturation
% 16.08/2.89 % (3051262)Time elapsed: 0.060 s
% 16.08/2.89 % (3051262)Peak memory usage: 13 MB
% 16.08/2.89 % (3051262)Instructions burned: 103 (million)
% 16.08/2.89 % (3051263)Instruction limit reached!
% 16.08/2.89 % (3051263)------------------------------
% 16.08/2.89 % (3051263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.08/2.89 % (3051263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.08/2.89 % (3051263)CaDiCaL version: 2.1.3
% 16.08/2.89 % (3051263)Termination reason: Instruction limit
% 16.08/2.89 % (3051263)Termination phase: Saturation
% 16.08/2.89 % (3051263)Time elapsed: 0.063 s
% 16.08/2.89 % (3051263)Peak memory usage: 12 MB
% 16.08/2.89 % (3051263)Instructions burned: 116 (million)
% 16.08/2.89 % TRYING [6]
% 16.08/2.89 % (3051273)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4174649230:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.08/2.89 % (3051264)Instruction limit reached!
% 16.08/2.89 % (3051264)------------------------------
% 16.08/2.89 % (3051264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.08/2.89 % (3051264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.08/2.89 % (3051264)CaDiCaL version: 2.1.3
% 16.08/2.89 % (3051264)Termination reason: Instruction limit
% 16.08/2.89 % (3051264)Termination phase: Saturation
% 16.08/2.89 % (3051264)Time elapsed: 0.080 s
% 16.08/2.89 % (3051264)Peak memory usage: 15 MB
% 16.08/2.89 % (3051264)Instructions burned: 131 (million)
% 16.08/2.89 % (3051274)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1944164150:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 16.08/2.89 % TRYING [1]
% 16.08/2.89 % TRYING [2]
% 16.08/2.89 % TRYING [3]
% 16.08/2.89 % (3051265)Instruction limit reached!
% 16.08/2.89 % (3051265)------------------------------
% 16.08/2.89 % (3051265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.08/2.89 % (3051265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.08/2.89 % (3051265)CaDiCaL version: 2.1.3
% 16.08/2.89 % (3051265)Termination reason: Instruction limit
% 16.08/2.89 % (3051265)Termination phase: Saturation
% 16.08/2.89 % (3051265)Time elapsed: 0.088 s
% 16.08/2.89 % (3051265)Peak memory usage: 16 MB
% 16.08/2.89 % (3051265)Instructions burned: 160 (million)
% 16.08/2.89 % TRYING [4]
% 16.08/2.89 % (3051276)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=2267901979:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.08/2.89 % TRYING [5]
% 16.08/2.89 % (3051278)ott-21_1_sil=16000:fs=off:random_seed=446740999:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.08/2.89 % TRYING [6]
% 16.08/2.89 % (3051274)Instruction limit reached!
% 16.08/2.89 % (3051274)------------------------------
% 16.08/2.89 % (3051274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.20/7.52 % (3051274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.52 % (3051274)CaDiCaL version: 2.1.3
% 50.20/7.52 % (3051274)Termination reason: Instruction limit
% 50.20/7.52 % (3051274)Termination phase: Saturation
% 50.20/7.52 % (3051274)Time elapsed: 0.080 s
% 50.20/7.52 % (3051274)Peak memory usage: 14 MB
% 50.20/7.52 % (3051274)Instructions burned: 131 (million)
% 50.20/7.52 % (3051281)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=599916446:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 50.20/7.52 % (3051278)Instruction limit reached!
% 50.20/7.52 % (3051278)------------------------------
% 50.20/7.52 % (3051278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.20/7.52 % (3051278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.52 % (3051278)CaDiCaL version: 2.1.3
% 50.20/7.52 % (3051278)Termination reason: Instruction limit
% 50.20/7.52 % (3051278)Termination phase: Saturation
% 50.20/7.52 % (3051278)Time elapsed: 0.095 s
% 50.20/7.52 % (3051278)Peak memory usage: 14 MB
% 50.20/7.52 % (3051278)Instructions burned: 181 (million)
% 50.20/7.52 % TRYING [7]
% 50.20/7.52 % (3051283)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3958900128:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 50.20/7.52 % TRYING [1]
% 50.20/7.52 % TRYING [2]
% 50.20/7.52 % TRYING [3]
% 50.20/7.52 % TRYING [4]
% 50.20/7.52 % TRYING [5]
% 50.20/7.52 % TRYING [6]
% 50.20/7.52 % TRYING [7]
% 50.20/7.52 % (3051276)Instruction limit reached!
% 50.20/7.52 % (3051276)------------------------------
% 50.20/7.52 % (3051276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.20/7.52 % (3051276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.52 % (3051276)CaDiCaL version: 2.1.3
% 50.20/7.52 % (3051276)Termination reason: Instruction limit
% 50.20/7.52 % (3051276)Termination phase: Saturation
% 50.20/7.52 % (3051276)Time elapsed: 0.344 s
% 50.20/7.52 % (3051276)Peak memory usage: 21 MB
% 50.20/7.52 % (3051276)Instructions burned: 686 (million)
% 50.20/7.52 % (3051273)Instruction limit reached!
% 50.20/7.52 % (3051273)------------------------------
% 50.20/7.52 % (3051273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.20/7.52 % (3051273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.52 % (3051273)CaDiCaL version: 2.1.3
% 50.20/7.52 % (3051273)Termination reason: Instruction limit
% 50.20/7.52 % (3051273)Termination phase: Finite model building SAT solving
% 50.20/7.52 % (3051273)Time elapsed: 0.386 s
% 50.20/7.52 % (3051273)Peak memory usage: 14 MB
% 50.20/7.52 % (3051273)Instructions burned: 715 (million)
% 50.20/7.52 % (3051285)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2093195369:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 50.20/7.52 % (3051281)Instruction limit reached!
% 50.20/7.52 % (3051281)------------------------------
% 50.20/7.52 % (3051281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.20/7.52 % (3051281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.52 % (3051281)CaDiCaL version: 2.1.3
% 50.20/7.52 % (3051281)Termination reason: Instruction limit
% 50.20/7.52 % (3051281)Termination phase: Saturation
% 50.20/7.52 % (3051281)Time elapsed: 0.288 s
% 50.20/7.52 % (3051281)Peak memory usage: 18 MB
% 50.20/7.52 % (3051281)Instructions burned: 478 (million)
% 50.20/7.52 % (3051286)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=41410673:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 50.20/7.52 % (3051288)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=2711706922:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 50.20/7.52 % TRYING [14]
% 50.20/7.52 % TRYING [8]
% 50.20/7.52 % (3051283)Instruction limit reached!
% 50.20/7.52 % (3051283)------------------------------
% 50.20/7.52 % (3051283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.20/7.52 % (3051283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.20/7.52 % (3051283)CaDiCaL version: 2.1.3
% 50.20/7.52 % (3051283)Termination reason: Instruction limit
% 50.20/7.52 % (3051283)Termination phase: Finite model building SAT solving
% 50.20/7.52 % (3051283)Time elapsed: 0.423 s
% 50.20/7.52 % (3051283)Peak memory usage: 15 MB
% 50.20/7.52 % (3051283)Instructions burned: 866 (million)
% 50.20/7.52 % (3051291)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3340210402:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 59.19/8.85 % (3051286)Instruction limit reached!
% 59.19/8.85 % (3051286)------------------------------
% 59.19/8.85 % (3051286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051286)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051286)Termination reason: Instruction limit
% 59.19/8.85 % (3051286)Termination phase: Finite model building SAT solving
% 59.19/8.85 % (3051286)Time elapsed: 0.297 s
% 59.19/8.85 % (3051286)Peak memory usage: 25 MB
% 59.19/8.85 % (3051286)Instructions burned: 891 (million)
% 59.19/8.85 % TRYING [8]
% 59.19/8.85 % (3051293)fmb+10_1_sil=64000:random_seed=3287073884:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 59.19/8.85 % TRYING [1]
% 59.19/8.85 % TRYING [2]
% 59.19/8.85 % TRYING [3]
% 59.19/8.85 % TRYING [4]
% 59.19/8.85 % TRYING [5]
% 59.19/8.85 % (3051288)Instruction limit reached!
% 59.19/8.85 % (3051288)------------------------------
% 59.19/8.85 % (3051288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051288)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051288)Termination reason: Instruction limit
% 59.19/8.85 % (3051288)Termination phase: Saturation
% 59.19/8.85 % (3051288)Time elapsed: 0.366 s
% 59.19/8.85 % (3051288)Peak memory usage: 14 MB
% 59.19/8.85 % (3051288)Instructions burned: 692 (million)
% 59.19/8.85 % TRYING [6]
% 59.19/8.85 % (3051295)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2088306525:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 59.19/8.85 % TRYING [20]
% 59.19/8.85 % TRYING [7]
% 59.19/8.85 % (3051285)Instruction limit reached!
% 59.19/8.85 % (3051285)------------------------------
% 59.19/8.85 % (3051285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051285)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051285)Termination reason: Instruction limit
% 59.19/8.85 % (3051285)Termination phase: Saturation
% 59.19/8.85 % (3051285)Time elapsed: 0.641 s
% 59.19/8.85 % (3051285)Peak memory usage: 37 MB
% 59.19/8.85 % (3051285)Instructions burned: 1180 (million)
% 59.19/8.85 % (3051291)Instruction limit reached!
% 59.19/8.85 % (3051291)------------------------------
% 59.19/8.85 % (3051291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051291)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051291)Termination reason: Instruction limit
% 59.19/8.85 % (3051291)Termination phase: Saturation
% 59.19/8.85 % (3051291)Time elapsed: 0.460 s
% 59.19/8.85 % (3051291)Peak memory usage: 17 MB
% 59.19/8.85 % (3051291)Instructions burned: 879 (million)
% 59.19/8.85 % (3051297)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1116415976:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 59.19/8.85 % TRYING [8]
% 59.19/8.85 % (3051298)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1283469753:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 59.19/8.85 % TRYING [8]
% 59.19/8.85 % (3051297)Instruction limit reached!
% 59.19/8.85 % (3051297)------------------------------
% 59.19/8.85 % (3051297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051297)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051297)Termination reason: Instruction limit
% 59.19/8.85 % (3051297)Termination phase: Finite model building SAT solving
% 59.19/8.85 % (3051297)Time elapsed: 0.441 s
% 59.19/8.85 % (3051297)Peak memory usage: 18 MB
% 59.19/8.85 % (3051297)Instructions burned: 921 (million)
% 59.19/8.85 % (3051301)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3443263741:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 59.19/8.85 % TRYING [9]
% 59.19/8.85 % (3051301)Instruction limit reached!
% 59.19/8.85 % (3051301)------------------------------
% 59.19/8.85 % (3051301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051301)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051301)Termination reason: Instruction limit
% 59.19/8.85 % (3051301)Termination phase: Saturation
% 59.19/8.85 % (3051301)Time elapsed: 0.823 s
% 59.19/8.85 % (3051301)Peak memory usage: 26 MB
% 59.19/8.85 % (3051301)Instructions burned: 1473 (million)
% 59.19/8.85 % (3051303)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=116314793:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 59.19/8.85 % TRYING [77]
% 59.19/8.85 % TRYING [9]
% 59.19/8.85 % (3051298)Instruction limit reached!
% 59.19/8.85 % (3051298)------------------------------
% 59.19/8.85 % (3051298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051298)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051298)Termination reason: Instruction limit
% 59.19/8.85 % (3051298)Termination phase: Saturation
% 59.19/8.85 % (3051298)Time elapsed: 2.996 s
% 59.19/8.85 % (3051298)Peak memory usage: 31 MB
% 59.19/8.85 % (3051298)Instructions burned: 5131 (million)
% 59.19/8.85 % (3051305)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1796092394:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 59.19/8.85 % TRYING [16]
% 59.19/8.85 % (3051303)Instruction limit reached!
% 59.19/8.85 % (3051303)------------------------------
% 59.19/8.85 % (3051303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051303)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051303)Termination reason: Instruction limit
% 59.19/8.85 % (3051303)Termination phase: Finite model building constraint generation
% 59.19/8.85 % (3051303)Time elapsed: 2.339 s
% 59.19/8.85 % (3051303)Peak memory usage: 484 MB
% 59.19/8.85 % (3051303)Instructions burned: 6324 (million)
% 59.19/8.85 % (3051307)ott-2_1_sil=16000:newcnf=on:random_seed=3665814506:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi)
% 59.19/8.85 % (3051305)Instruction limit reached!
% 59.19/8.85 % (3051305)------------------------------
% 59.19/8.85 % (3051305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051305)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051305)Termination reason: Instruction limit
% 59.19/8.85 % (3051305)Termination phase: Finite model building SAT solving
% 59.19/8.85 % (3051305)Time elapsed: 1.063 s
% 59.19/8.85 % (3051305)Peak memory usage: 46 MB
% 59.19/8.85 % (3051305)Instructions burned: 2175 (million)
% 59.19/8.85 % (3051309)ott+10_1_sil=32000:tgt=ground:random_seed=1953078822:i=5114:av=off_2947 on theBenchmark for (2947ds/5114Mi)
% 59.19/8.85 % (3051295)Instruction limit reached!
% 59.19/8.85 % (3051295)------------------------------
% 59.19/8.85 % (3051295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051295)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051295)Termination reason: Instruction limit
% 59.19/8.85 % (3051295)Termination phase: Finite model building SAT solving
% 59.19/8.85 % (3051295)Time elapsed: 4.437 s
% 59.19/8.85 % (3051295)Peak memory usage: 91 MB
% 59.19/8.85 % (3051295)Instructions burned: 9515 (million)
% 59.19/8.85 % (3051311)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1294461275:i=54282_2946 on theBenchmark for (2946ds/54282Mi)
% 59.19/8.85 % (3051307)Instruction limit reached!
% 59.19/8.85 % (3051307)------------------------------
% 59.19/8.85 % (3051307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051307)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051307)Termination reason: Instruction limit
% 59.19/8.85 % (3051307)Termination phase: Saturation
% 59.19/8.85 % (3051307)Time elapsed: 0.497 s
% 59.19/8.85 % (3051307)Peak memory usage: 17 MB
% 59.19/8.85 % (3051307)Instructions burned: 870 (million)
% 59.19/8.85 % TRYING [1]
% 59.19/8.85 % TRYING [2]
% 59.19/8.85 % TRYING [3]
% 59.19/8.85 % TRYING [4]
% 59.19/8.85 % (3051313)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1414822584:i=3512:aac=none_2946 on theBenchmark for (2946ds/3512Mi)
% 59.19/8.85 % TRYING [5]
% 59.19/8.85 % TRYING [6]
% 59.19/8.85 % TRYING [7]
% 59.19/8.85 % TRYING [8]
% 59.19/8.85 % TRYING [10]
% 59.19/8.85 % (3051313)Instruction limit reached!
% 59.19/8.85 % (3051313)------------------------------
% 59.19/8.85 % (3051313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051313)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051313)Termination reason: Instruction limit
% 59.19/8.85 % (3051313)Termination phase: Saturation
% 59.19/8.85 % (3051313)Time elapsed: 1.689 s
% 59.19/8.85 % (3051313)Peak memory usage: 72 MB
% 59.19/8.85 % (3051313)Instructions burned: 3515 (million)
% 59.19/8.85 % (3051315)dis+21_1_sil=32000:sas=cadical:random_seed=197907450:i=3773:amm=off_2929 on theBenchmark for (2929ds/3773Mi)
% 59.19/8.85 % TRYING [9]
% 59.19/8.85 % (3051309)Instruction limit reached!
% 59.19/8.85 % (3051309)------------------------------
% 59.19/8.85 % (3051309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.85 % (3051309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.85 % (3051309)CaDiCaL version: 2.1.3
% 59.19/8.85 % (3051309)Termination reason: Instruction limit
% 59.19/8.85 % (3051309)Termination phase: Saturation
% 59.19/8.85 % (3051309)Time elapsed: 2.856 s
% 59.19/8.85 % (3051309)Peak memory usage: 83 MB
% 59.19/8.85 % (3051309)Instructions burned: 5114 (million)
% 59.19/8.85 % (3051317)ott+11_1_sil=16000:gs=on:random_seed=320293955:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2918 on theBenchmark for (2918ds/2251Mi)
% 59.19/8.85 % (3051317) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3051254-3051317"...
% 59.19/8.85 % (3051317)...printing done.
% 59.19/8.85 % (3051317)Refutation found. Thanks to Tanya!
% 59.19/8.85 % SZS status Theorem for theBenchmark
% 59.19/8.85 % SZS output start Proof for theBenchmark
% See solution above
% 59.19/8.86 % (3051317)------------------------------
% 59.19/8.86 % (3051317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.19/8.86 % (3051317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.19/8.86 % (3051317)CaDiCaL version: 2.1.3
% 59.19/8.86 % (3051317)Termination reason: Refutation
% 59.19/8.86 % (3051317)Time elapsed: 0.229 s
% 59.19/8.86 % (3051317)Peak memory usage: 18 MB
% 59.19/8.86 % (3051317)Instructions burned: 367 (million)
% 59.19/8.86 % (3051254)Success in time 8.425 s
% 59.19/8.86 % Vampire exiting
%------------------------------------------------------------------------------