%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL660+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:59:31 AM UTC 2026
% Result : Theorem 1.87s 0.73s
% Output : Refutation 1.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 62
% Syntax : Number of formulae : 620 ( 15 unt; 60 def)
% Number of atoms : 3620 ( 0 equ)
% Maximal formula atoms : 204 ( 5 avg)
% Number of connectives : 5287 (2287 ~;2688 |; 252 &)
% ( 60 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 74 ( 72 usr; 62 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 5 con; 0-1 aty)
% Number of variables : 960 ( 0 sgn 864 !; 96 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p5(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)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p3(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p5(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) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ! [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(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p5(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)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p3(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p5(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) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p5(X1) )
& ( ! [X2] :
( ~ r1(X0,X2)
| p2(X2) )
| ~ ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p2(X5) )
| ~ p2(X4) ) ) ) )
| ! [X6] :
( ~ r1(X0,X6)
| p3(X6) )
| ~ ! [X7] :
( ~ r1(X0,X7)
| p3(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p3(X9) )
| ~ p3(X8) ) )
| ( ~ ! [X10] :
( ~ r1(X0,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p5(X11) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| p2(X12) )
| ~ ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) ) )
| ! [X16] :
( ~ r1(X0,X16)
| p1(X16) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) )
| ~ ( ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ~ ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23) )
| ~ p2(X22) ) ) )
| ~ ! [X24] :
( ~ r1(X0,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ~ ! [X27] :
( ~ r1(X0,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ( ( ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31)
| ~ ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
| ~ ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| p2(X36) )
| ~ p2(X35) ) ) )
& ( p2(X29)
| ~ ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
| ~ ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ~ ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44) )
| ~ p2(X43) ) ) )
| ~ ! [X45] :
( ~ r1(X40,X45)
| p2(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ~ ! [X48] :
( ~ r1(X40,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) ) )
| ~ ( ( ! [X50] :
( ~ r1(X39,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51)
| ~ ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
| ~ ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| p2(X56) )
| ~ p2(X55) ) ) )
& ( p2(X39)
| ~ ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X59] :
( ~ r1(X0,X59)
| $false )
| ~ ! [X60] :
( ~ r1(X0,X60)
| p4(X60)
| p3(X60)
| p2(X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,X61)
| $false )
| ~ ! [X62] :
( ~ r1(X60,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) )
| ~ ( p4(X62)
| p3(X62)
| p2(X62)
| p1(X62)
| ! [X65] :
( ~ r1(X62,X65)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X66] :
( ~ r1(X0,X66)
| $false )
| ~ ! [X67] :
( ~ r1(X0,X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] :
( ~ r1(X67,X68)
| $false )
| ~ ! [X69] :
( ~ r1(X67,X69)
| ! [X70] :
( ~ r1(X69,X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| $false ) )
| ~ ( p3(X69)
| p2(X69)
| p1(X69)
| ! [X72] :
( ~ r1(X69,X72)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X73] :
( ~ r1(X0,X73)
| $false )
| ~ ! [X74] :
( ~ r1(X0,X74)
| p2(X74)
| p1(X74)
| ! [X75] :
( ~ r1(X74,X75)
| $false )
| ~ ! [X76] :
( ~ r1(X74,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p2(X77)
| p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| $false ) )
| ~ ( p2(X76)
| p1(X76)
| ! [X79] :
( ~ r1(X76,X79)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| $false )
| ~ ! [X81] :
( ~ r1(X0,X81)
| p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| $false )
| ~ ! [X83] :
( ~ r1(X81,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| $false ) )
| ~ ( p1(X83)
| ! [X86] :
( ~ r1(X83,X86)
| $false ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| p2(X87)
| ~ ! [X88] :
( ~ r1(X87,X88)
| p2(X88)
| ~ ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p2(X90) )
| ~ p2(X89) ) ) ) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p5(X1) )
& ( ! [X2] :
( ~ r1(X0,X2)
| p2(X2) )
| ~ ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p2(X5) )
| ~ p2(X4) ) ) ) )
| ! [X6] :
( ~ r1(X0,X6)
| p3(X6) )
| ~ ! [X7] :
( ~ r1(X0,X7)
| p3(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| p3(X9) )
| ~ p3(X8) ) )
| ( ~ ! [X10] :
( ~ r1(X0,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ p5(X11) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| p2(X12) )
| ~ ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) ) )
| ! [X16] :
( ~ r1(X0,X16)
| p1(X16) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) )
| ~ ( ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ~ ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23) )
| ~ p2(X22) ) ) )
| ~ ! [X24] :
( ~ r1(X0,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ~ ! [X27] :
( ~ r1(X0,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
| ~ ! [X29] :
( ~ r1(X0,X29)
| ( ( ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31)
| ~ ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
| ~ ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| p2(X36) )
| ~ p2(X35) ) ) )
& ( p2(X29)
| ~ ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
| ~ ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ~ ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44) )
| ~ p2(X43) ) ) )
| ~ ! [X45] :
( ~ r1(X40,X45)
| p2(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ~ ! [X48] :
( ~ r1(X40,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) ) )
| ~ ( ( ! [X50] :
( ~ r1(X39,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51)
| ~ ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
| ~ ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| p2(X56) )
| ~ p2(X55) ) ) )
& ( p2(X39)
| ~ ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X59] :
( ~ r1(X0,X59)
| $false )
| ~ ! [X60] :
( ~ r1(X0,X60)
| p4(X60)
| p3(X60)
| p2(X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,X61)
| $false )
| ~ ! [X62] :
( ~ r1(X60,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) )
| ~ ( p4(X62)
| p3(X62)
| p2(X62)
| p1(X62)
| ! [X65] :
( ~ r1(X62,X65)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X66] :
( ~ r1(X0,X66)
| $false )
| ~ ! [X67] :
( ~ r1(X0,X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] :
( ~ r1(X67,X68)
| $false )
| ~ ! [X69] :
( ~ r1(X67,X69)
| ! [X70] :
( ~ r1(X69,X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| $false ) )
| ~ ( p3(X69)
| p2(X69)
| p1(X69)
| ! [X72] :
( ~ r1(X69,X72)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X73] :
( ~ r1(X0,X73)
| $false )
| ~ ! [X74] :
( ~ r1(X0,X74)
| p2(X74)
| p1(X74)
| ! [X75] :
( ~ r1(X74,X75)
| $false )
| ~ ! [X76] :
( ~ r1(X74,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p2(X77)
| p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| $false ) )
| ~ ( p2(X76)
| p1(X76)
| ! [X79] :
( ~ r1(X76,X79)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| $false )
| ~ ! [X81] :
( ~ r1(X0,X81)
| p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| $false )
| ~ ! [X83] :
( ~ r1(X81,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| $false ) )
| ~ ( p1(X83)
| ! [X86] :
( ~ r1(X83,X86)
| $false ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| p2(X87)
| ~ ! [X88] :
( ~ r1(X87,X88)
| p2(X88)
| ~ ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p2(X90) )
| ~ p2(X89) ) ) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ( ! [X1] :
( ~ r1(X0,X1)
| ~ p5(X1) )
| ( ? [X2] :
( r1(X0,X2)
& ~ p2(X2) )
& ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ~ p2(X5) )
& p2(X4) ) ) ) )
& ? [X6] :
( r1(X0,X6)
& ~ p3(X6) )
& ! [X7] :
( ~ r1(X0,X7)
| p3(X7)
| ? [X8] :
( r1(X7,X8)
& ? [X9] :
( r1(X8,X9)
& ~ p3(X9) )
& p3(X8) ) )
& ( ! [X10] :
( ~ r1(X0,X10)
| ? [X11] :
( r1(X10,X11)
& p5(X11) ) )
| ( ? [X12] :
( r1(X0,X12)
& ~ p2(X12) )
& ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ? [X14] :
( r1(X13,X14)
& ? [X15] :
( r1(X14,X15)
& ~ p2(X15) )
& p2(X14) ) ) ) )
& ? [X16] :
( r1(X0,X16)
& ~ p1(X16) )
& ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ? [X18] :
( r1(X17,X18)
& ? [X19] :
( r1(X18,X19)
& ~ p1(X19) )
& p1(X18) ) )
& ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ? [X22] :
( r1(X21,X22)
& ? [X23] :
( r1(X22,X23)
& ~ p2(X23) )
& p2(X22) ) ) )
| ? [X24] :
( r1(X0,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ? [X27] :
( r1(X0,X27)
& ? [X28] :
( r1(X27,X28)
& ~ p2(X28) )
& p2(X27) ) ) )
| ? [X29] :
( r1(X0,X29)
& ( ( ? [X30] :
( r1(X29,X30)
& ? [X31] :
( r1(X30,X31)
& ~ p2(X31)
& ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
& ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ? [X35] :
( r1(X34,X35)
& ? [X36] :
( r1(X35,X36)
& ~ p2(X36) )
& p2(X35) ) ) )
| ( ~ p2(X29)
& ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ? [X43] :
( r1(X42,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44) )
& p2(X43) ) ) )
| ? [X45] :
( r1(X40,X45)
& ~ p2(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ? [X48] :
( r1(X40,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) ) )
| ( ? [X50] :
( r1(X39,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51)
& ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
& ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ? [X55] :
( r1(X54,X55)
& ? [X56] :
( r1(X55,X56)
& ~ p2(X56) )
& p2(X55) ) ) )
| ( ~ p2(X39)
& ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X59] :
( ~ r1(X0,X59)
| $false )
| ? [X60] :
( r1(X0,X60)
& ~ p4(X60)
& ~ p3(X60)
& ~ p2(X60)
& ~ p1(X60)
& ? [X61] :
( r1(X60,X61)
& $true )
& ! [X62] :
( ~ r1(X60,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) )
| ( ~ p4(X62)
& ~ p3(X62)
& ~ p2(X62)
& ~ p1(X62)
& ? [X65] :
( r1(X62,X65)
& $true ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X66] :
( ~ r1(X0,X66)
| $false )
| ? [X67] :
( r1(X0,X67)
& ~ p3(X67)
& ~ p2(X67)
& ~ p1(X67)
& ? [X68] :
( r1(X67,X68)
& $true )
& ! [X69] :
( ~ r1(X67,X69)
| ! [X70] :
( ~ r1(X69,X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| $false ) )
| ( ~ p3(X69)
& ~ p2(X69)
& ~ p1(X69)
& ? [X72] :
( r1(X69,X72)
& $true ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X73] :
( ~ r1(X0,X73)
| $false )
| ? [X74] :
( r1(X0,X74)
& ~ p2(X74)
& ~ p1(X74)
& ? [X75] :
( r1(X74,X75)
& $true )
& ! [X76] :
( ~ r1(X74,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p2(X77)
| p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| $false ) )
| ( ~ p2(X76)
& ~ p1(X76)
& ? [X79] :
( r1(X76,X79)
& $true ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| $false )
| ? [X81] :
( r1(X0,X81)
& ~ p1(X81)
& ? [X82] :
( r1(X81,X82)
& $true )
& ! [X83] :
( ~ r1(X81,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| $false ) )
| ( ~ p1(X83)
& ? [X86] :
( r1(X83,X86)
& $true ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| p2(X87)
| ? [X88] :
( r1(X87,X88)
& ~ p2(X88)
& ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p2(X90) )
| ~ p2(X89) ) ) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ( ! [X1] :
( ~ r1(X0,X1)
| ~ p5(X1) )
| ( ? [X2] :
( r1(X0,X2)
& ~ p2(X2) )
& ! [X3] :
( ~ r1(X0,X3)
| p2(X3)
| ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ~ p2(X5) )
& p2(X4) ) ) ) )
& ? [X6] :
( r1(X0,X6)
& ~ p3(X6) )
& ! [X7] :
( ~ r1(X0,X7)
| p3(X7)
| ? [X8] :
( r1(X7,X8)
& ? [X9] :
( r1(X8,X9)
& ~ p3(X9) )
& p3(X8) ) )
& ( ! [X10] :
( ~ r1(X0,X10)
| ? [X11] :
( r1(X10,X11)
& p5(X11) ) )
| ( ? [X12] :
( r1(X0,X12)
& ~ p2(X12) )
& ! [X13] :
( ~ r1(X0,X13)
| p2(X13)
| ? [X14] :
( r1(X13,X14)
& ? [X15] :
( r1(X14,X15)
& ~ p2(X15) )
& p2(X14) ) ) ) )
& ? [X16] :
( r1(X0,X16)
& ~ p1(X16) )
& ! [X17] :
( ~ r1(X0,X17)
| p1(X17)
| ? [X18] :
( r1(X17,X18)
& ? [X19] :
( r1(X18,X19)
& ~ p1(X19) )
& p1(X18) ) )
& ( ( ( ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21)
| ? [X22] :
( r1(X21,X22)
& ? [X23] :
( r1(X22,X23)
& ~ p2(X23) )
& p2(X22) ) ) )
| ? [X24] :
( r1(X0,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ( p2(X0)
| ? [X27] :
( r1(X0,X27)
& ? [X28] :
( r1(X27,X28)
& ~ p2(X28) )
& p2(X27) ) ) )
| ? [X29] :
( r1(X0,X29)
& ( ( ? [X30] :
( r1(X29,X30)
& ? [X31] :
( r1(X30,X31)
& ~ p2(X31)
& ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33) )
| ~ p2(X32) ) ) )
& ! [X34] :
( ~ r1(X29,X34)
| p2(X34)
| ? [X35] :
( r1(X34,X35)
& ? [X36] :
( r1(X35,X36)
& ~ p2(X36) )
& p2(X35) ) ) )
| ( ~ p2(X29)
& ! [X37] :
( ~ r1(X29,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ! [X39] :
( ~ r1(X29,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ( ( ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42)
| ? [X43] :
( r1(X42,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44) )
& p2(X43) ) ) )
| ? [X45] :
( r1(X40,X45)
& ~ p2(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p2(X47) )
| ~ p2(X46) ) ) )
& ( p2(X40)
| ? [X48] :
( r1(X40,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) ) )
| ( ? [X50] :
( r1(X39,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51)
& ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53) )
| ~ p2(X52) ) ) )
& ! [X54] :
( ~ r1(X39,X54)
| p2(X54)
| ? [X55] :
( r1(X54,X55)
& ? [X56] :
( r1(X55,X56)
& ~ p2(X56) )
& p2(X55) ) ) )
| ( ~ p2(X39)
& ! [X57] :
( ~ r1(X39,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X59] :
( ~ r1(X0,X59)
| $false )
| ? [X60] :
( r1(X0,X60)
& ~ p4(X60)
& ~ p3(X60)
& ~ p2(X60)
& ~ p1(X60)
& ? [X61] :
( r1(X60,X61)
& $true )
& ! [X62] :
( ~ r1(X60,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) )
| ( ~ p4(X62)
& ~ p3(X62)
& ~ p2(X62)
& ~ p1(X62)
& ? [X65] :
( r1(X62,X65)
& $true ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X66] :
( ~ r1(X0,X66)
| $false )
| ? [X67] :
( r1(X0,X67)
& ~ p3(X67)
& ~ p2(X67)
& ~ p1(X67)
& ? [X68] :
( r1(X67,X68)
& $true )
& ! [X69] :
( ~ r1(X67,X69)
| ! [X70] :
( ~ r1(X69,X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| $false ) )
| ( ~ p3(X69)
& ~ p2(X69)
& ~ p1(X69)
& ? [X72] :
( r1(X69,X72)
& $true ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X73] :
( ~ r1(X0,X73)
| $false )
| ? [X74] :
( r1(X0,X74)
& ~ p2(X74)
& ~ p1(X74)
& ? [X75] :
( r1(X74,X75)
& $true )
& ! [X76] :
( ~ r1(X74,X76)
| ! [X77] :
( ~ r1(X76,X77)
| p2(X77)
| p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| $false ) )
| ( ~ p2(X76)
& ~ p1(X76)
& ? [X79] :
( r1(X76,X79)
& $true ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| $false )
| ? [X81] :
( r1(X0,X81)
& ~ p1(X81)
& ? [X82] :
( r1(X81,X82)
& $true )
& ! [X83] :
( ~ r1(X81,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| $false ) )
| ( ~ p1(X83)
& ? [X86] :
( r1(X83,X86)
& $true ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| p2(X87)
| ? [X88] :
( r1(X87,X88)
& ~ p2(X88)
& ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p2(X90) )
| ~ p2(X89) ) ) ) ),
inference(flattening,[],[f6]) ).
fof(f8,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f22,plain,
! [X29,X32,X33] :
( ~ p2(X32)
| p2(X33)
| ~ r1(X32,X33)
| ~ r1(sK40(X29),X32)
| ~ sP29(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f23,plain,
! [X40,X39] :
( ~ p2(sK49(X40))
| p2(X40)
| ~ r1(X39,X40)
| ~ sP26(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f24,plain,
! [X40,X39] :
( r1(sK44(X40),sK49(X40))
| p2(X40)
| ~ r1(X39,X40)
| ~ sP26(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f25,plain,
! [X39,X54] :
( ~ p2(sK48(X54))
| p2(X54)
| ~ r1(X39,X54)
| ~ sP25(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f26,plain,
! [X39,X54] :
( r1(sK42(X54),sK48(X54))
| p2(X54)
| ~ r1(X39,X54)
| ~ sP25(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f27,plain,
! [X21,X0,X20] :
( ~ p2(sK47(X21))
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| ~ sP20(X20,X0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f28,plain,
! [X21,X0,X20] :
( r1(sK41(X21),sK47(X21))
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| ~ sP20(X20,X0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f29,plain,
! [X29,X34] :
( ~ p2(sK46(X34))
| p2(X34)
| ~ r1(X29,X34)
| ~ sP28(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f30,plain,
! [X29,X34] :
( r1(sK39(X34),sK46(X34))
| p2(X34)
| ~ r1(X29,X34)
| ~ sP28(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f31,plain,
! [X40,X39] :
( p2(sK44(X40))
| p2(X40)
| ~ r1(X39,X40)
| ~ sP26(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f32,plain,
! [X40,X39] :
( r1(X40,sK44(X40))
| p2(X40)
| ~ r1(X39,X40)
| ~ sP26(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f35,plain,
! [X39,X54] :
( p2(sK42(X54))
| p2(X54)
| ~ r1(X39,X54)
| ~ sP25(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f36,plain,
! [X39,X54] :
( r1(X54,sK42(X54))
| p2(X54)
| ~ r1(X39,X54)
| ~ sP25(X39) ),
inference(cnf_transformation,[],[f7]) ).
fof(f37,plain,
! [X21,X0,X20] :
( p2(sK41(X21))
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| ~ sP20(X20,X0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f38,plain,
! [X21,X0,X20] :
( r1(X21,sK41(X21))
| p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| ~ sP20(X20,X0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X29] :
( ~ p2(sK40(X29))
| ~ sP29(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f40,plain,
! [X29] :
( r1(sK35(X29),sK40(X29))
| ~ sP29(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f41,plain,
! [X29,X34] :
( p2(sK39(X34))
| p2(X34)
| ~ r1(X29,X34)
| ~ sP28(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f42,plain,
! [X29,X34] :
( r1(X34,sK39(X34))
| p2(X34)
| ~ r1(X29,X34)
| ~ sP28(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f43,plain,
! [X38,X29,X37] :
( ~ p2(X37)
| p2(X38)
| ~ r1(X37,X38)
| ~ r1(X29,X37)
| ~ sP27(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f48,plain,
! [X58,X39,X57,X20] :
( ~ p2(X57)
| p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f49,plain,
! [X58,X39,X57,X20] :
( ~ p2(X57)
| p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| ~ p2(sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f50,plain,
! [X58,X39,X57,X26,X25,X20] :
( ~ p2(X57)
| p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f65,plain,
! [X39,X26,X25,X20] :
( ~ p2(X39)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f66,plain,
! [X26,X25,X20] :
( r1(sK0,sK7)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f67,plain,
! [X26,X25,X20] :
( sP27(sK7)
| sP29(sK7)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f68,plain,
! [X26,X25,X20] :
( sP27(sK7)
| sP28(sK7)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f69,plain,
! [X26,X25,X20] :
( ~ p2(sK7)
| sP29(sK7)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f70,plain,
! [X26,X25,X20] :
( ~ p2(sK7)
| sP28(sK7)
| ~ p2(X25)
| p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f72,plain,
! [X3,X1] :
( ~ p2(sK37(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p5(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f73,plain,
! [X3,X1] :
( r1(sK24(X3),sK37(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p5(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f74,plain,
! [X10,X13] :
( ~ p2(sK36(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f75,plain,
! [X10,X13] :
( r1(sK22(X13),sK36(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f76,plain,
! [X10,X13] :
( ~ p2(sK36(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f77,plain,
! [X10,X13] :
( r1(sK22(X13),sK36(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f78,plain,
! [X29] :
( r1(X29,sK35(X29))
| ~ sP29(X29) ),
inference(cnf_transformation,[],[f7]) ).
fof(f79,plain,
! [X90,X89,X87] :
( ~ p2(X89)
| p2(X90)
| ~ r1(X89,X90)
| ~ r1(sK8(X87),X89)
| p2(X87)
| ~ r1(sK0,X87) ),
inference(cnf_transformation,[],[f7]) ).
fof(f92,plain,
! [X3,X1] :
( p2(sK24(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p5(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f93,plain,
! [X3,X1] :
( r1(X3,sK24(X3))
| p2(X3)
| ~ r1(sK0,X3)
| ~ p5(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f96,plain,
! [X10,X13] :
( p2(sK22(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f97,plain,
! [X10,X13] :
( r1(X13,sK22(X13))
| p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f98,plain,
! [X10,X13] :
( p2(sK22(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f99,plain,
! [X10,X13] :
( r1(X13,sK22(X13))
| p2(X13)
| ~ r1(sK0,X13)
| p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f104,plain,
! [X39,X20] :
( ~ p2(X39)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f105,plain,
! [X39,X20] :
( ~ p2(X39)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| ~ p2(sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f106,plain,
! [X10] :
( r1(sK0,sK10)
| p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f107,plain,
! [X10] :
( r1(sK0,sK10)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f108,plain,
! [X10] :
( ~ p2(sK10)
| p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f109,plain,
! [X10] :
( ~ p2(sK10)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(cnf_transformation,[],[f7]) ).
fof(f110,plain,
! [X20] :
( r1(sK0,sK7)
| ~ p2(sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f111,plain,
! [X20] :
( r1(sK0,sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f112,plain,
! [X20] :
( sP27(sK7)
| sP29(sK7)
| ~ p2(sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f113,plain,
! [X20] :
( sP27(sK7)
| sP29(sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f114,plain,
! [X20] :
( sP27(sK7)
| sP28(sK7)
| ~ p2(sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f115,plain,
! [X20] :
( sP27(sK7)
| sP28(sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f116,plain,
! [X20] :
( ~ p2(sK7)
| sP29(sK7)
| ~ p2(sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f117,plain,
! [X20] :
( ~ p2(sK7)
| sP29(sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f118,plain,
! [X20] :
( ~ p2(sK7)
| sP28(sK7)
| ~ p2(sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f119,plain,
! [X20] :
( ~ p2(sK7)
| sP28(sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(cnf_transformation,[],[f7]) ).
fof(f134,plain,
! [X1] :
( ~ p2(sK12)
| ~ p5(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f135,plain,
! [X1] :
( r1(sK0,sK12)
| ~ p5(X1)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f154,plain,
! [X87] :
( ~ p2(sK8(X87))
| p2(X87)
| ~ r1(sK0,X87) ),
inference(cnf_transformation,[],[f7]) ).
fof(f155,plain,
! [X87] :
( r1(X87,sK8(X87))
| p2(X87)
| ~ r1(sK0,X87) ),
inference(cnf_transformation,[],[f7]) ).
fof(f161,plain,
! [X87] :
( r1(X87,sK8(X87))
| ~ p2(X87)
| ~ r1(sK0,X87) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f162,plain,
! [X87] :
( p2(sK8(X87))
| ~ p2(X87)
| ~ r1(sK0,X87) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f177,plain,
! [X1] :
( r1(sK0,sK12)
| p5(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f178,plain,
! [X1] :
( p2(sK12)
| p5(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f192,plain,
! [X20] :
( p2(sK7)
| ~ sP28(sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f193,plain,
! [X20] :
( p2(sK7)
| ~ sP28(sK7)
| p2(sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f194,plain,
! [X20] :
( p2(sK7)
| sP29(sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f195,plain,
! [X20] :
( p2(sK7)
| sP29(sK7)
| p2(sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f196,plain,
! [X20] :
( sP27(sK7)
| ~ sP28(sK7)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f197,plain,
! [X20] :
( sP27(sK7)
| ~ sP28(sK7)
| p2(sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f198,plain,
! [X20] :
( sP27(sK7)
| sP29(sK7)
| p2(sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f199,plain,
! [X20] :
( r1(sK0,sK7)
| p2(sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f200,plain,
! [X10] :
( p2(sK10)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f109]) ).
fof(f201,plain,
! [X10] :
( p2(sK10)
| ~ p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f108]) ).
fof(f202,plain,
! [X10] :
( r1(sK0,sK10)
| ~ p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f203,plain,
! [X39,X20] :
( p2(X39)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| p2(sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f204,plain,
! [X39,X20] :
( p2(X39)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f207,plain,
! [X10,X13] :
( r1(X13,sK22(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| ~ p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f208,plain,
! [X10,X13] :
( ~ p2(sK22(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| ~ p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f209,plain,
! [X10,X13] :
( r1(X13,sK22(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f210,plain,
! [X10,X13] :
( ~ p2(sK22(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f213,plain,
! [X3,X1] :
( r1(X3,sK24(X3))
| ~ p2(X3)
| ~ r1(sK0,X3)
| p5(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f93]) ).
fof(f214,plain,
! [X3,X1] :
( ~ p2(sK24(X3))
| ~ p2(X3)
| ~ r1(sK0,X3)
| p5(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f92]) ).
fof(f227,plain,
! [X90,X89,X87] :
( ~ p2(X87)
| ~ p2(X90)
| ~ r1(X89,X90)
| ~ r1(sK8(X87),X89)
| p2(X89)
| ~ r1(sK0,X87) ),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f228,plain,
! [X10,X13] :
( r1(sK22(X13),sK36(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f77]) ).
fof(f229,plain,
! [X10,X13] :
( p2(sK36(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| r1(X10,sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f230,plain,
! [X10,X13] :
( r1(sK22(X13),sK36(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| ~ p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f231,plain,
! [X10,X13] :
( p2(sK36(X13))
| ~ p2(X13)
| ~ r1(sK0,X13)
| ~ p5(sK19(X10))
| ~ r1(sK0,X10) ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f232,plain,
! [X3,X1] :
( r1(sK24(X3),sK37(X3))
| ~ p2(X3)
| ~ r1(sK0,X3)
| p5(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f233,plain,
! [X3,X1] :
( p2(sK37(X3))
| ~ p2(X3)
| ~ r1(sK0,X3)
| p5(X1)
| ~ r1(sK0,X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f234,plain,
! [X26,X25,X20] :
( p2(sK7)
| ~ sP28(sK7)
| p2(X25)
| ~ p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f235,plain,
! [X26,X25,X20] :
( p2(sK7)
| sP29(sK7)
| p2(X25)
| ~ p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f236,plain,
! [X26,X25,X20] :
( sP27(sK7)
| ~ sP28(sK7)
| p2(X25)
| ~ p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f237,plain,
! [X26,X25,X20] :
( sP27(sK7)
| sP29(sK7)
| p2(X25)
| ~ p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f238,plain,
! [X26,X25,X20] :
( r1(sK0,sK7)
| p2(X25)
| ~ p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f239,plain,
! [X39,X26,X25,X20] :
( p2(X39)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| p2(X25)
| ~ p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f252,plain,
! [X58,X39,X57,X26,X25,X20] :
( p2(X57)
| ~ p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| p2(X25)
| ~ p2(X26)
| ~ r1(X25,X26)
| ~ r1(sK18,X25)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f253,plain,
! [X58,X39,X57,X20] :
( p2(X57)
| ~ p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| p2(sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f254,plain,
! [X58,X39,X57,X20] :
( p2(X57)
| ~ p2(X58)
| ~ r1(X57,X58)
| ~ r1(X39,X57)
| sP25(X39)
| sP26(X39)
| ~ r1(sK7,X39)
| r1(sK0,sK18)
| sP20(X20,sK0) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f259,plain,
! [X38,X29,X37] :
( ~ sP27(X29)
| ~ p2(X38)
| ~ r1(X37,X38)
| ~ r1(X29,X37)
| p2(X37) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f260,plain,
! [X29,X34] :
( ~ p2(X34)
| r1(X34,sK39(X34))
| ~ r1(X29,X34)
| sP28(X29) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f261,plain,
! [X29,X34] :
( ~ p2(sK39(X34))
| ~ p2(X34)
| ~ r1(X29,X34)
| sP28(X29) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f262,plain,
! [X29] :
( p2(sK40(X29))
| ~ sP29(X29) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f263,plain,
! [X21,X0,X20] :
( ~ sP20(X20,X0)
| ~ p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| r1(X21,sK41(X21)) ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f264,plain,
! [X21,X0,X20] :
( ~ p2(sK41(X21))
| ~ p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| ~ sP20(X20,X0) ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f265,plain,
! [X39,X54] :
( ~ sP25(X39)
| ~ p2(X54)
| ~ r1(X39,X54)
| r1(X54,sK42(X54)) ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f266,plain,
! [X39,X54] :
( ~ p2(sK42(X54))
| ~ p2(X54)
| ~ r1(X39,X54)
| ~ sP25(X39) ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f268,plain,
! [X40,X39] :
( ~ sP26(X39)
| ~ p2(X40)
| ~ r1(X39,X40)
| r1(X40,sK44(X40)) ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f269,plain,
! [X40,X39] :
( ~ p2(sK44(X40))
| ~ p2(X40)
| ~ r1(X39,X40)
| ~ sP26(X39) ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f270,plain,
! [X29,X34] :
( ~ p2(X34)
| r1(sK39(X34),sK46(X34))
| ~ r1(X29,X34)
| sP28(X29) ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f271,plain,
! [X29,X34] :
( ~ p2(X34)
| p2(sK46(X34))
| ~ r1(X29,X34)
| sP28(X29) ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f272,plain,
! [X21,X0,X20] :
( ~ sP20(X20,X0)
| ~ p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| r1(sK41(X21),sK47(X21)) ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f273,plain,
! [X21,X0,X20] :
( ~ sP20(X20,X0)
| ~ p2(X21)
| ~ r1(X20,X21)
| ~ r1(X0,X20)
| p2(sK47(X21)) ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f274,plain,
! [X39,X54] :
( ~ sP25(X39)
| ~ p2(X54)
| ~ r1(X39,X54)
| r1(sK42(X54),sK48(X54)) ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f275,plain,
! [X39,X54] :
( ~ sP25(X39)
| ~ p2(X54)
| ~ r1(X39,X54)
| p2(sK48(X54)) ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f276,plain,
! [X40,X39] :
( ~ sP26(X39)
| ~ p2(X40)
| ~ r1(X39,X40)
| r1(sK44(X40),sK49(X40)) ),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f277,plain,
! [X40,X39] :
( ~ sP26(X39)
| ~ p2(X40)
| ~ r1(X39,X40)
| p2(sK49(X40)) ),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f278,plain,
! [X29,X32,X33] :
( ~ sP29(X29)
| ~ p2(X33)
| ~ r1(X32,X33)
| ~ r1(sK40(X29),X32)
| p2(X32) ),
inference(consistent_polarity_flipping,[],[f22]) ).
fof(f301,definition,
( spl52_3
<=> ! [X57,X39,X58] :
( p2(X57)
| ~ r1(sK7,X39)
| sP26(X39)
| sP25(X39)
| ~ r1(X39,X57)
| ~ r1(X57,X58)
| ~ p2(X58) ) ),
introduced(definition,[new_symbols(definition,[spl52_3])],[avatar_definition]) ).
fof(f302,plain,
( ! [X58,X39,X57] :
( ~ p2(X58)
| ~ r1(sK7,X39)
| sP26(X39)
| sP25(X39)
| ~ r1(X39,X57)
| ~ r1(X57,X58)
| p2(X57) )
| ~ spl52_3 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f320,definition,
( spl52_7
<=> ! [X20] : sP20(X20,sK0) ),
introduced(definition,[new_symbols(definition,[spl52_7])],[avatar_definition]) ).
fof(f321,plain,
( ! [X20] : sP20(X20,sK0)
| ~ spl52_7 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f323,definition,
( spl52_8
<=> r1(sK0,sK18) ),
introduced(definition,[new_symbols(definition,[spl52_8])],[avatar_definition]) ).
fof(f325,plain,
( r1(sK0,sK18)
| ~ spl52_8 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f326,plain,
( spl52_7
| spl52_8
| spl52_3 ),
inference(avatar_split_clause,[],[f254,f301,f323,f320]) ).
fof(f328,definition,
( spl52_9
<=> p2(sK18) ),
introduced(definition,[new_symbols(definition,[spl52_9])],[avatar_definition]) ).
fof(f330,plain,
( p2(sK18)
| ~ spl52_9 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f331,plain,
( spl52_7
| spl52_9
| spl52_3 ),
inference(avatar_split_clause,[],[f253,f301,f328,f320]) ).
fof(f333,definition,
( spl52_10
<=> ! [X25,X26] :
( p2(X25)
| ~ r1(sK18,X25)
| ~ r1(X25,X26)
| ~ p2(X26) ) ),
introduced(definition,[new_symbols(definition,[spl52_10])],[avatar_definition]) ).
fof(f334,plain,
( ! [X26,X25] :
( ~ r1(sK18,X25)
| p2(X25)
| ~ r1(X25,X26)
| ~ p2(X26) )
| ~ spl52_10 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f335,plain,
( spl52_7
| spl52_10
| spl52_3 ),
inference(avatar_split_clause,[],[f252,f301,f333,f320]) ).
fof(f408,definition,
( spl52_29
<=> ! [X39] :
( p2(X39)
| ~ r1(sK7,X39)
| sP26(X39)
| sP25(X39) ) ),
introduced(definition,[new_symbols(definition,[spl52_29])],[avatar_definition]) ).
fof(f409,plain,
( ! [X39] :
( ~ r1(sK7,X39)
| p2(X39)
| sP26(X39)
| sP25(X39) )
| ~ spl52_29 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f410,plain,
( spl52_7
| spl52_10
| spl52_29 ),
inference(avatar_split_clause,[],[f239,f408,f333,f320]) ).
fof(f412,definition,
( spl52_30
<=> r1(sK0,sK7) ),
introduced(definition,[new_symbols(definition,[spl52_30])],[avatar_definition]) ).
fof(f414,plain,
( r1(sK0,sK7)
| ~ spl52_30 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f415,plain,
( spl52_7
| spl52_10
| spl52_30 ),
inference(avatar_split_clause,[],[f238,f412,f333,f320]) ).
fof(f417,definition,
( spl52_31
<=> sP29(sK7) ),
introduced(definition,[new_symbols(definition,[spl52_31])],[avatar_definition]) ).
fof(f419,plain,
( sP29(sK7)
| ~ spl52_31 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f421,definition,
( spl52_32
<=> sP27(sK7) ),
introduced(definition,[new_symbols(definition,[spl52_32])],[avatar_definition]) ).
fof(f423,plain,
( sP27(sK7)
| ~ spl52_32 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f424,plain,
( spl52_7
| spl52_10
| spl52_31
| spl52_32 ),
inference(avatar_split_clause,[],[f237,f421,f417,f333,f320]) ).
fof(f426,definition,
( spl52_33
<=> sP28(sK7) ),
introduced(definition,[new_symbols(definition,[spl52_33])],[avatar_definition]) ).
fof(f428,plain,
( ~ sP28(sK7)
| spl52_33 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f429,plain,
( spl52_7
| spl52_10
| ~ spl52_33
| spl52_32 ),
inference(avatar_split_clause,[],[f236,f421,f426,f333,f320]) ).
fof(f431,definition,
( spl52_34
<=> p2(sK7) ),
introduced(definition,[new_symbols(definition,[spl52_34])],[avatar_definition]) ).
fof(f432,plain,
( ~ p2(sK7)
| spl52_34 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f433,plain,
( p2(sK7)
| ~ spl52_34 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f434,plain,
( spl52_7
| spl52_10
| spl52_31
| spl52_34 ),
inference(avatar_split_clause,[],[f235,f431,f417,f333,f320]) ).
fof(f435,plain,
( spl52_7
| spl52_10
| ~ spl52_33
| spl52_34 ),
inference(avatar_split_clause,[],[f234,f431,f426,f333,f320]) ).
fof(f437,definition,
( spl52_35
<=> ! [X1] :
( p5(X1)
| ~ r1(sK0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl52_35])],[avatar_definition]) ).
fof(f438,plain,
( ! [X1] :
( ~ r1(sK0,X1)
| p5(X1) )
| ~ spl52_35 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f440,definition,
( spl52_36
<=> ! [X3] :
( p2(sK37(X3))
| ~ r1(sK0,X3)
| ~ p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl52_36])],[avatar_definition]) ).
fof(f441,plain,
( ! [X3] :
( ~ p2(X3)
| ~ r1(sK0,X3)
| p2(sK37(X3)) )
| ~ spl52_36 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f442,plain,
( spl52_35
| spl52_36 ),
inference(avatar_split_clause,[],[f233,f440,f437]) ).
fof(f444,definition,
( spl52_37
<=> ! [X3] :
( r1(sK24(X3),sK37(X3))
| ~ r1(sK0,X3)
| ~ p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl52_37])],[avatar_definition]) ).
fof(f445,plain,
( ! [X3] :
( r1(sK24(X3),sK37(X3))
| ~ r1(sK0,X3)
| ~ p2(X3) )
| ~ spl52_37 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f446,plain,
( spl52_35
| spl52_37 ),
inference(avatar_split_clause,[],[f232,f444,f437]) ).
fof(f448,definition,
( spl52_38
<=> ! [X10] :
( ~ p5(sK19(X10))
| ~ r1(sK0,X10) ) ),
introduced(definition,[new_symbols(definition,[spl52_38])],[avatar_definition]) ).
fof(f449,plain,
( ! [X10] :
( ~ p5(sK19(X10))
| ~ r1(sK0,X10) )
| ~ spl52_38 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f451,definition,
( spl52_39
<=> ! [X13] :
( p2(sK36(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl52_39])],[avatar_definition]) ).
fof(f452,plain,
( ! [X13] :
( p2(sK36(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) )
| ~ spl52_39 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f453,plain,
( spl52_38
| spl52_39 ),
inference(avatar_split_clause,[],[f231,f451,f448]) ).
fof(f455,definition,
( spl52_40
<=> ! [X13] :
( r1(sK22(X13),sK36(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl52_40])],[avatar_definition]) ).
fof(f456,plain,
( ! [X13] :
( r1(sK22(X13),sK36(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) )
| ~ spl52_40 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( spl52_38
| spl52_40 ),
inference(avatar_split_clause,[],[f230,f455,f448]) ).
fof(f459,definition,
( spl52_41
<=> ! [X10] :
( r1(X10,sK19(X10))
| ~ r1(sK0,X10) ) ),
introduced(definition,[new_symbols(definition,[spl52_41])],[avatar_definition]) ).
fof(f460,plain,
( ! [X10] :
( r1(X10,sK19(X10))
| ~ r1(sK0,X10) )
| ~ spl52_41 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( spl52_41
| spl52_39 ),
inference(avatar_split_clause,[],[f229,f451,f459]) ).
fof(f462,plain,
( spl52_41
| spl52_40 ),
inference(avatar_split_clause,[],[f228,f455,f459]) ).
fof(f476,definition,
( spl52_42
<=> ! [X3] :
( ~ p2(sK24(X3))
| ~ r1(sK0,X3)
| ~ p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl52_42])],[avatar_definition]) ).
fof(f477,plain,
( ! [X3] :
( ~ p2(sK24(X3))
| ~ r1(sK0,X3)
| ~ p2(X3) )
| ~ spl52_42 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f478,plain,
( spl52_35
| spl52_42 ),
inference(avatar_split_clause,[],[f214,f476,f437]) ).
fof(f480,definition,
( spl52_43
<=> ! [X3] :
( r1(X3,sK24(X3))
| ~ r1(sK0,X3)
| ~ p2(X3) ) ),
introduced(definition,[new_symbols(definition,[spl52_43])],[avatar_definition]) ).
fof(f481,plain,
( ! [X3] :
( r1(X3,sK24(X3))
| ~ r1(sK0,X3)
| ~ p2(X3) )
| ~ spl52_43 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f482,plain,
( spl52_35
| spl52_43 ),
inference(avatar_split_clause,[],[f213,f480,f437]) ).
fof(f484,definition,
( spl52_44
<=> ! [X13] :
( ~ p2(sK22(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl52_44])],[avatar_definition]) ).
fof(f485,plain,
( ! [X13] :
( ~ p2(sK22(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) )
| ~ spl52_44 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f486,plain,
( spl52_41
| spl52_44 ),
inference(avatar_split_clause,[],[f210,f484,f459]) ).
fof(f488,definition,
( spl52_45
<=> ! [X13] :
( r1(X13,sK22(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) ) ),
introduced(definition,[new_symbols(definition,[spl52_45])],[avatar_definition]) ).
fof(f489,plain,
( ! [X13] :
( r1(X13,sK22(X13))
| ~ r1(sK0,X13)
| ~ p2(X13) )
| ~ spl52_45 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f490,plain,
( spl52_41
| spl52_45 ),
inference(avatar_split_clause,[],[f209,f488,f459]) ).
fof(f491,plain,
( spl52_38
| spl52_44 ),
inference(avatar_split_clause,[],[f208,f484,f448]) ).
fof(f492,plain,
( spl52_38
| spl52_45 ),
inference(avatar_split_clause,[],[f207,f488,f448]) ).
fof(f495,plain,
( spl52_7
| spl52_8
| spl52_29 ),
inference(avatar_split_clause,[],[f204,f408,f323,f320]) ).
fof(f496,plain,
( spl52_7
| spl52_9
| spl52_29 ),
inference(avatar_split_clause,[],[f203,f408,f328,f320]) ).
fof(f498,definition,
( spl52_46
<=> r1(sK0,sK10) ),
introduced(definition,[new_symbols(definition,[spl52_46])],[avatar_definition]) ).
fof(f500,plain,
( r1(sK0,sK10)
| ~ spl52_46 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f501,plain,
( spl52_38
| spl52_46 ),
inference(avatar_split_clause,[],[f202,f498,f448]) ).
fof(f502,plain,
( spl52_41
| spl52_46 ),
inference(avatar_split_clause,[],[f107,f498,f459]) ).
fof(f504,definition,
( spl52_47
<=> p2(sK10) ),
introduced(definition,[new_symbols(definition,[spl52_47])],[avatar_definition]) ).
fof(f506,plain,
( p2(sK10)
| ~ spl52_47 ),
inference(avatar_component_clause,[],[f504]) ).
fof(f507,plain,
( spl52_38
| spl52_47 ),
inference(avatar_split_clause,[],[f201,f504,f448]) ).
fof(f508,plain,
( spl52_41
| spl52_47 ),
inference(avatar_split_clause,[],[f200,f504,f459]) ).
fof(f509,plain,
( spl52_7
| spl52_9
| spl52_30 ),
inference(avatar_split_clause,[],[f199,f412,f328,f320]) ).
fof(f510,plain,
( spl52_7
| spl52_8
| spl52_30 ),
inference(avatar_split_clause,[],[f111,f412,f323,f320]) ).
fof(f511,plain,
( spl52_7
| spl52_9
| spl52_31
| spl52_32 ),
inference(avatar_split_clause,[],[f198,f421,f417,f328,f320]) ).
fof(f512,plain,
( spl52_7
| spl52_8
| spl52_31
| spl52_32 ),
inference(avatar_split_clause,[],[f113,f421,f417,f323,f320]) ).
fof(f513,plain,
( spl52_7
| spl52_9
| ~ spl52_33
| spl52_32 ),
inference(avatar_split_clause,[],[f197,f421,f426,f328,f320]) ).
fof(f514,plain,
( spl52_7
| spl52_8
| ~ spl52_33
| spl52_32 ),
inference(avatar_split_clause,[],[f196,f421,f426,f323,f320]) ).
fof(f515,plain,
( spl52_7
| spl52_9
| spl52_31
| spl52_34 ),
inference(avatar_split_clause,[],[f195,f431,f417,f328,f320]) ).
fof(f516,plain,
( spl52_7
| spl52_8
| spl52_31
| spl52_34 ),
inference(avatar_split_clause,[],[f194,f431,f417,f323,f320]) ).
fof(f517,plain,
( spl52_7
| spl52_9
| ~ spl52_33
| spl52_34 ),
inference(avatar_split_clause,[],[f193,f431,f426,f328,f320]) ).
fof(f518,plain,
( spl52_7
| spl52_8
| ~ spl52_33
| spl52_34 ),
inference(avatar_split_clause,[],[f192,f431,f426,f323,f320]) ).
fof(f550,definition,
( spl52_52
<=> p2(sK12) ),
introduced(definition,[new_symbols(definition,[spl52_52])],[avatar_definition]) ).
fof(f552,plain,
( p2(sK12)
| ~ spl52_52 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f553,plain,
( spl52_35
| spl52_52 ),
inference(avatar_split_clause,[],[f178,f550,f437]) ).
fof(f555,definition,
( spl52_53
<=> r1(sK0,sK12) ),
introduced(definition,[new_symbols(definition,[spl52_53])],[avatar_definition]) ).
fof(f557,plain,
( r1(sK0,sK12)
| ~ spl52_53 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f558,plain,
( spl52_35
| spl52_53 ),
inference(avatar_split_clause,[],[f177,f555,f437]) ).
fof(f651,plain,
( ~ r1(sK0,sK0)
| p5(sK19(sK0))
| ~ spl52_35
| ~ spl52_41 ),
inference(resolution,[],[f460,f438]) ).
fof(f652,plain,
( ~ r1(sK0,sK0)
| ~ spl52_35
| ~ spl52_38
| ~ spl52_41 ),
inference(forward_subsumption_resolution,[],[f651,f449]) ).
fof(f658,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| p2(sK46(sK8(X0)))
| sP28(X1)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f271,f162]) ).
fof(f661,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| r1(sK8(X0),sK39(sK8(X0)))
| sP28(X1)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f260,f162]) ).
fof(f664,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| r1(sK39(sK8(X0)),sK46(sK8(X0)))
| sP28(X1)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f270,f162]) ).
fof(f665,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK0,X1)
| p2(sK47(X0)) )
| ~ spl52_7 ),
inference(resolution,[],[f273,f321]) ).
fof(f668,plain,
( ! [X0,X1] :
( ~ r1(X0,sK8(X1))
| ~ r1(sK0,X0)
| p2(sK47(sK8(X1)))
| ~ p2(X1)
| ~ r1(sK0,X1) )
| ~ spl52_7 ),
inference(resolution,[],[f665,f162]) ).
fof(f669,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK0,X1)
| r1(X0,sK41(X0)) )
| ~ spl52_7 ),
inference(resolution,[],[f263,f321]) ).
fof(f676,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK0,X1)
| r1(sK41(X0),sK47(X0)) )
| ~ spl52_7 ),
inference(resolution,[],[f272,f321]) ).
fof(f679,plain,
( ! [X0,X1] :
( ~ r1(X0,sK8(X1))
| ~ r1(sK0,X0)
| r1(sK41(sK8(X1)),sK47(sK8(X1)))
| ~ p2(X1)
| ~ r1(sK0,X1) )
| ~ spl52_7 ),
inference(resolution,[],[f676,f162]) ).
fof(f680,plain,
( $false
| ~ spl52_35
| ~ spl52_38
| ~ spl52_41 ),
inference(backward_subsumption_resolution,[],[f652,f8]) ).
fof(f682,plain,
( ~ spl52_35
| ~ spl52_38
| ~ spl52_41 ),
inference(avatar_contradiction_clause,[],[f680]) ).
fof(f690,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK8(sK10),X1)
| p2(X1)
| ~ r1(sK0,sK10) )
| ~ spl52_47 ),
inference(resolution,[],[f506,f227]) ).
fof(f734,definition,
( spl52_81
<=> ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(sK8(sK10),X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_81])],[avatar_definition]) ).
fof(f735,plain,
( ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(sK8(sK10),X1)
| ~ r1(X1,X0) )
| ~ spl52_81 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f736,plain,
( ~ spl52_46
| spl52_81
| ~ spl52_47 ),
inference(avatar_split_clause,[],[f690,f504,f734,f498]) ).
fof(f737,plain,
( ! [X0,X1] :
( ~ r1(sK40(sK7),X1)
| ~ r1(X1,X0)
| ~ p2(X0)
| p2(X1) )
| ~ spl52_31 ),
inference(resolution,[],[f419,f278]) ).
fof(f787,definition,
( spl52_89
<=> sP25(sK35(sK7)) ),
introduced(definition,[new_symbols(definition,[spl52_89])],[avatar_definition]) ).
fof(f789,plain,
( sP25(sK35(sK7))
| ~ spl52_89 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f791,definition,
( spl52_90
<=> sP26(sK35(sK7)) ),
introduced(definition,[new_symbols(definition,[spl52_90])],[avatar_definition]) ).
fof(f793,plain,
( sP26(sK35(sK7))
| ~ spl52_90 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f795,definition,
( spl52_91
<=> p2(sK35(sK7)) ),
introduced(definition,[new_symbols(definition,[spl52_91])],[avatar_definition]) ).
fof(f797,plain,
( p2(sK35(sK7))
| ~ spl52_91 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f936,plain,
! [X0] :
( p2(sK46(sK8(X0)))
| sP28(X0)
| ~ p2(X0)
| ~ r1(sK0,X0)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f658,f161]) ).
fof(f938,plain,
! [X0] :
( ~ p2(X0)
| sP28(X0)
| p2(sK46(sK8(X0)))
| ~ r1(sK0,X0) ),
inference(duplicate_literal_removal,[],[f936]) ).
fof(f945,plain,
! [X0] :
( r1(sK8(X0),sK39(sK8(X0)))
| sP28(X0)
| ~ p2(X0)
| ~ r1(sK0,X0)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f661,f161]) ).
fof(f947,plain,
! [X0] :
( r1(sK8(X0),sK39(sK8(X0)))
| sP28(X0)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(duplicate_literal_removal,[],[f945]) ).
fof(f951,plain,
! [X0] :
( r1(sK39(sK8(X0)),sK46(sK8(X0)))
| sP28(X0)
| ~ p2(X0)
| ~ r1(sK0,X0)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(resolution,[],[f664,f161]) ).
fof(f953,plain,
! [X0] :
( r1(sK39(sK8(X0)),sK46(sK8(X0)))
| sP28(X0)
| ~ p2(X0)
| ~ r1(sK0,X0) ),
inference(duplicate_literal_removal,[],[f951]) ).
fof(f1190,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| p2(sK47(sK8(X0)))
| ~ p2(X0)
| ~ r1(sK0,X0)
| ~ p2(X0)
| ~ r1(sK0,X0) )
| ~ spl52_7 ),
inference(resolution,[],[f668,f161]) ).
fof(f1192,plain,
( ! [X0] :
( ~ p2(X0)
| p2(sK47(sK8(X0)))
| ~ r1(sK0,X0) )
| ~ spl52_7 ),
inference(duplicate_literal_removal,[],[f1190]) ).
fof(f1219,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| r1(sK41(sK8(X0)),sK47(sK8(X0)))
| ~ p2(X0)
| ~ r1(sK0,X0)
| ~ p2(X0)
| ~ r1(sK0,X0) )
| ~ spl52_7 ),
inference(resolution,[],[f679,f161]) ).
fof(f1221,plain,
( ! [X0] :
( r1(sK41(sK8(X0)),sK47(sK8(X0)))
| ~ r1(sK0,X0)
| ~ p2(X0) )
| ~ spl52_7 ),
inference(duplicate_literal_removal,[],[f1219]) ).
fof(f1227,plain,
( p2(sK47(sK8(sK10)))
| ~ r1(sK0,sK10)
| ~ spl52_7
| ~ spl52_47 ),
inference(resolution,[],[f1192,f506]) ).
fof(f1233,plain,
( p2(sK47(sK8(sK10)))
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f1227,f500]) ).
fof(f1242,plain,
( ! [X0] :
( ~ r1(X0,sK47(sK8(sK10)))
| ~ r1(sK8(sK10),X0)
| p2(X0) )
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81 ),
inference(resolution,[],[f1233,f735]) ).
fof(f1339,definition,
( spl52_166
<=> p2(sK8(sK10)) ),
introduced(definition,[new_symbols(definition,[spl52_166])],[avatar_definition]) ).
fof(f1340,plain,
( p2(sK8(sK10))
| ~ spl52_166 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1341,plain,
( ~ p2(sK8(sK10))
| spl52_166 ),
inference(avatar_component_clause,[],[f1339]) ).
fof(f1347,plain,
( ~ p2(sK10)
| ~ r1(sK0,sK10)
| spl52_166 ),
inference(resolution,[],[f1341,f162]) ).
fof(f1348,plain,
( ~ r1(sK0,sK10)
| ~ spl52_47
| spl52_166 ),
inference(forward_subsumption_resolution,[],[f1347,f506]) ).
fof(f1349,plain,
( $false
| ~ spl52_46
| ~ spl52_47
| spl52_166 ),
inference(forward_subsumption_resolution,[],[f1348,f500]) ).
fof(f1350,plain,
( ~ spl52_46
| ~ spl52_47
| spl52_166 ),
inference(avatar_contradiction_clause,[],[f1349]) ).
fof(f1357,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK10))
| ~ r1(sK0,X0)
| r1(sK8(sK10),sK41(sK8(sK10))) )
| ~ spl52_7
| ~ spl52_166 ),
inference(resolution,[],[f1340,f669]) ).
fof(f1358,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK10))
| ~ r1(sK0,X0)
| r1(sK41(sK8(sK10)),sK47(sK8(sK10))) )
| ~ spl52_7
| ~ spl52_166 ),
inference(resolution,[],[f1340,f676]) ).
fof(f1394,definition,
( spl52_174
<=> r1(sK41(sK8(sK10)),sK47(sK8(sK10))) ),
introduced(definition,[new_symbols(definition,[spl52_174])],[avatar_definition]) ).
fof(f1396,plain,
( r1(sK41(sK8(sK10)),sK47(sK8(sK10)))
| ~ spl52_174 ),
inference(avatar_component_clause,[],[f1394]) ).
fof(f1398,definition,
( spl52_175
<=> ! [X0] :
( ~ r1(X0,sK8(sK10))
| ~ r1(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_175])],[avatar_definition]) ).
fof(f1399,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK10))
| ~ r1(sK0,X0) )
| ~ spl52_175 ),
inference(avatar_component_clause,[],[f1398]) ).
fof(f1400,plain,
( spl52_174
| spl52_175
| ~ spl52_7
| ~ spl52_166 ),
inference(avatar_split_clause,[],[f1358,f1339,f320,f1398,f1394]) ).
fof(f1402,definition,
( spl52_176
<=> r1(sK8(sK10),sK41(sK8(sK10))) ),
introduced(definition,[new_symbols(definition,[spl52_176])],[avatar_definition]) ).
fof(f1404,plain,
( r1(sK8(sK10),sK41(sK8(sK10)))
| ~ spl52_176 ),
inference(avatar_component_clause,[],[f1402]) ).
fof(f1405,plain,
( spl52_176
| spl52_175
| ~ spl52_7
| ~ spl52_166 ),
inference(avatar_split_clause,[],[f1357,f1339,f320,f1398,f1402]) ).
fof(f1578,plain,
( ~ r1(sK0,sK10)
| ~ p2(sK10)
| ~ r1(sK0,sK10)
| ~ spl52_175 ),
inference(resolution,[],[f1399,f161]) ).
fof(f1580,plain,
( ~ r1(sK0,sK10)
| ~ p2(sK10)
| ~ spl52_175 ),
inference(duplicate_literal_removal,[],[f1578]) ).
fof(f1581,plain,
( ~ p2(sK10)
| ~ spl52_46
| ~ spl52_175 ),
inference(forward_subsumption_resolution,[],[f1580,f500]) ).
fof(f1582,plain,
( $false
| ~ spl52_46
| ~ spl52_47
| ~ spl52_175 ),
inference(forward_subsumption_resolution,[],[f1581,f506]) ).
fof(f1583,plain,
( ~ spl52_46
| ~ spl52_47
| ~ spl52_175 ),
inference(avatar_contradiction_clause,[],[f1582]) ).
fof(f1617,plain,
( ~ r1(sK8(sK10),sK41(sK8(sK10)))
| p2(sK41(sK8(sK10)))
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81
| ~ spl52_174 ),
inference(resolution,[],[f1242,f1396]) ).
fof(f1618,plain,
( p2(sK41(sK8(sK10)))
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81
| ~ spl52_174
| ~ spl52_176 ),
inference(forward_subsumption_resolution,[],[f1617,f1404]) ).
fof(f1622,plain,
( ! [X0,X1] :
( ~ p2(sK8(sK10))
| ~ r1(X0,sK8(sK10))
| ~ r1(X1,X0)
| ~ sP20(X0,X1) )
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81
| ~ spl52_174
| ~ spl52_176 ),
inference(resolution,[],[f1618,f264]) ).
fof(f1672,plain,
( ! [X0,X1] :
( ~ sP20(X0,X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK8(sK10)) )
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81
| ~ spl52_166
| ~ spl52_174
| ~ spl52_176 ),
inference(forward_subsumption_resolution,[],[f1622,f1340]) ).
fof(f1872,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| ~ r1(X0,sK8(sK10)) )
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81
| ~ spl52_166
| ~ spl52_174
| ~ spl52_176 ),
inference(resolution,[],[f1672,f321]) ).
fof(f1873,plain,
( spl52_175
| ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81
| ~ spl52_166
| ~ spl52_174
| ~ spl52_176 ),
inference(avatar_split_clause,[],[f1872,f1402,f1394,f1339,f734,f504,f498,f320,f1398]) ).
fof(f1880,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK8(sK12),X1)
| p2(X1)
| ~ r1(sK0,sK12) )
| ~ spl52_52 ),
inference(resolution,[],[f552,f227]) ).
fof(f1963,definition,
( spl52_267
<=> ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(sK8(sK12),X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_267])],[avatar_definition]) ).
fof(f1964,plain,
( ! [X0,X1] :
( ~ r1(sK8(sK12),X1)
| p2(X1)
| ~ p2(X0)
| ~ r1(X1,X0) )
| ~ spl52_267 ),
inference(avatar_component_clause,[],[f1963]) ).
fof(f1965,plain,
( ~ spl52_53
| spl52_267
| ~ spl52_52 ),
inference(avatar_split_clause,[],[f1880,f550,f1963,f555]) ).
fof(f2156,definition,
( spl52_302
<=> p2(sK8(sK12)) ),
introduced(definition,[new_symbols(definition,[spl52_302])],[avatar_definition]) ).
fof(f2157,plain,
( ~ p2(sK8(sK12))
| spl52_302 ),
inference(avatar_component_clause,[],[f2156]) ).
fof(f2158,plain,
( p2(sK8(sK12))
| ~ spl52_302 ),
inference(avatar_component_clause,[],[f2156]) ).
fof(f2173,definition,
( spl52_305
<=> ! [X0] :
( ~ p2(X0)
| ~ r1(sK41(sK8(sK12)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_305])],[avatar_definition]) ).
fof(f2174,plain,
( ! [X0] :
( ~ r1(sK41(sK8(sK12)),X0)
| ~ p2(X0) )
| ~ spl52_305 ),
inference(avatar_component_clause,[],[f2173]) ).
fof(f2176,definition,
( spl52_306
<=> p2(sK41(sK8(sK12))) ),
introduced(definition,[new_symbols(definition,[spl52_306])],[avatar_definition]) ).
fof(f2178,plain,
( p2(sK41(sK8(sK12)))
| ~ spl52_306 ),
inference(avatar_component_clause,[],[f2176]) ).
fof(f2196,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK12))
| ~ r1(sK0,X0)
| r1(sK8(sK12),sK41(sK8(sK12))) )
| ~ spl52_7
| ~ spl52_302 ),
inference(resolution,[],[f2158,f669]) ).
fof(f2238,definition,
( spl52_316
<=> ! [X0] :
( ~ r1(X0,sK8(sK12))
| ~ r1(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_316])],[avatar_definition]) ).
fof(f2239,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK12))
| ~ r1(sK0,X0) )
| ~ spl52_316 ),
inference(avatar_component_clause,[],[f2238]) ).
fof(f2242,definition,
( spl52_317
<=> r1(sK8(sK12),sK41(sK8(sK12))) ),
introduced(definition,[new_symbols(definition,[spl52_317])],[avatar_definition]) ).
fof(f2244,plain,
( r1(sK8(sK12),sK41(sK8(sK12)))
| ~ spl52_317 ),
inference(avatar_component_clause,[],[f2242]) ).
fof(f2245,plain,
( spl52_317
| spl52_316
| ~ spl52_7
| ~ spl52_302 ),
inference(avatar_split_clause,[],[f2196,f2156,f320,f2238,f2242]) ).
fof(f2769,plain,
( ! [X0] :
( p2(sK41(sK8(sK12)))
| ~ p2(X0)
| ~ r1(sK41(sK8(sK12)),X0) )
| ~ spl52_267
| ~ spl52_317 ),
inference(resolution,[],[f2244,f1964]) ).
fof(f2770,plain,
( spl52_305
| spl52_306
| ~ spl52_267
| ~ spl52_317 ),
inference(avatar_split_clause,[],[f2769,f2242,f1963,f2176,f2173]) ).
fof(f2914,plain,
( ~ p2(sK47(sK8(sK12)))
| ~ r1(sK0,sK12)
| ~ p2(sK12)
| ~ spl52_7
| ~ spl52_305 ),
inference(resolution,[],[f2174,f1221]) ).
fof(f2971,plain,
( ~ r1(sK0,sK12)
| ~ p2(sK12)
| ~ spl52_7
| ~ spl52_305 ),
inference(forward_subsumption_resolution,[],[f2914,f1192]) ).
fof(f2975,plain,
( ~ p2(sK12)
| ~ spl52_7
| ~ spl52_53
| ~ spl52_305 ),
inference(forward_subsumption_resolution,[],[f2971,f557]) ).
fof(f2976,plain,
( $false
| ~ spl52_7
| ~ spl52_52
| ~ spl52_53
| ~ spl52_305 ),
inference(forward_subsumption_resolution,[],[f2975,f552]) ).
fof(f2977,plain,
( ~ spl52_7
| ~ spl52_52
| ~ spl52_53
| ~ spl52_305 ),
inference(avatar_contradiction_clause,[],[f2976]) ).
fof(f2978,plain,
( ! [X0,X1] :
( ~ p2(sK8(sK12))
| ~ r1(X0,sK8(sK12))
| ~ r1(X1,X0)
| ~ sP20(X0,X1) )
| ~ spl52_306 ),
inference(resolution,[],[f2178,f264]) ).
fof(f3071,plain,
( ! [X0,X1] :
( ~ sP20(X0,X1)
| ~ r1(X1,X0)
| ~ r1(X0,sK8(sK12)) )
| ~ spl52_302
| ~ spl52_306 ),
inference(forward_subsumption_resolution,[],[f2978,f2158]) ).
fof(f3124,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| ~ r1(X0,sK8(sK12)) )
| ~ spl52_7
| ~ spl52_302
| ~ spl52_306 ),
inference(resolution,[],[f3071,f321]) ).
fof(f3125,plain,
( spl52_316
| ~ spl52_7
| ~ spl52_302
| ~ spl52_306 ),
inference(avatar_split_clause,[],[f3124,f2176,f2156,f320,f2238]) ).
fof(f3130,plain,
( ~ p2(sK12)
| ~ r1(sK0,sK12)
| spl52_302 ),
inference(resolution,[],[f2157,f162]) ).
fof(f3131,plain,
( ~ r1(sK0,sK12)
| ~ spl52_52
| spl52_302 ),
inference(forward_subsumption_resolution,[],[f3130,f552]) ).
fof(f3132,plain,
( $false
| ~ spl52_52
| ~ spl52_53
| spl52_302 ),
inference(forward_subsumption_resolution,[],[f3131,f557]) ).
fof(f3133,plain,
( ~ spl52_52
| ~ spl52_53
| spl52_302 ),
inference(avatar_contradiction_clause,[],[f3132]) ).
fof(f3171,plain,
( ~ r1(sK0,sK12)
| ~ p2(sK12)
| ~ r1(sK0,sK12)
| ~ spl52_316 ),
inference(resolution,[],[f2239,f161]) ).
fof(f3173,plain,
( ~ r1(sK0,sK12)
| ~ p2(sK12)
| ~ spl52_316 ),
inference(duplicate_literal_removal,[],[f3171]) ).
fof(f3174,plain,
( ~ p2(sK12)
| ~ spl52_53
| ~ spl52_316 ),
inference(forward_subsumption_resolution,[],[f3173,f557]) ).
fof(f3175,plain,
( $false
| ~ spl52_52
| ~ spl52_53
| ~ spl52_316 ),
inference(forward_subsumption_resolution,[],[f3174,f552]) ).
fof(f3176,plain,
( ~ spl52_52
| ~ spl52_53
| ~ spl52_316 ),
inference(avatar_contradiction_clause,[],[f3175]) ).
fof(f3234,plain,
( ! [X0,X1] :
( ~ r1(sK7,X1)
| ~ r1(X1,X0)
| ~ p2(X0)
| p2(X1) )
| ~ spl52_32 ),
inference(resolution,[],[f423,f259]) ).
fof(f3235,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK8(sK7),X1)
| p2(X1)
| ~ r1(sK0,sK7) )
| ~ spl52_34 ),
inference(resolution,[],[f433,f227]) ).
fof(f3268,plain,
( ! [X0,X1] :
( ~ r1(sK8(sK7),X1)
| ~ r1(X1,X0)
| ~ p2(X0)
| p2(X1) )
| ~ spl52_30
| ~ spl52_34 ),
inference(forward_subsumption_resolution,[],[f3235,f414]) ).
fof(f3338,plain,
( p2(sK35(sK7))
| sP26(sK35(sK7))
| sP25(sK35(sK7))
| ~ sP29(sK7)
| ~ spl52_29 ),
inference(resolution,[],[f409,f78]) ).
fof(f3407,plain,
( ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0)
| r1(X0,sK42(X0)) )
| ~ spl52_89 ),
inference(resolution,[],[f789,f265]) ).
fof(f3408,plain,
( ! [X0] :
( r1(sK42(X0),sK48(X0))
| ~ r1(sK35(sK7),X0)
| ~ p2(X0) )
| ~ spl52_89 ),
inference(resolution,[],[f789,f274]) ).
fof(f3409,plain,
( ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0)
| p2(sK48(X0)) )
| ~ spl52_89 ),
inference(resolution,[],[f789,f275]) ).
fof(f3503,plain,
( ! [X0] :
( ~ r1(sK7,X0)
| ~ p2(X0)
| p2(sK7) )
| ~ spl52_32 ),
inference(resolution,[],[f3234,f8]) ).
fof(f3509,plain,
( ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0)
| p2(sK35(sK7))
| ~ sP29(sK7) )
| ~ spl52_32 ),
inference(resolution,[],[f3234,f78]) ).
fof(f3515,plain,
( ! [X0] :
( ~ r1(sK7,X0)
| ~ p2(X0) )
| ~ spl52_32
| spl52_34 ),
inference(forward_subsumption_resolution,[],[f3503,f432]) ).
fof(f3518,definition,
( spl52_506
<=> ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_506])],[avatar_definition]) ).
fof(f3519,plain,
( ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0) )
| ~ spl52_506 ),
inference(avatar_component_clause,[],[f3518]) ).
fof(f3566,definition,
( spl52_514
<=> ! [X0] :
( ~ r1(X0,sK35(sK7))
| sP28(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_514])],[avatar_definition]) ).
fof(f3567,plain,
( ! [X0] :
( ~ r1(X0,sK35(sK7))
| sP28(X0) )
| ~ spl52_514 ),
inference(avatar_component_clause,[],[f3566]) ).
fof(f3569,definition,
( spl52_515
<=> p2(sK46(sK35(sK7))) ),
introduced(definition,[new_symbols(definition,[spl52_515])],[avatar_definition]) ).
fof(f3571,plain,
( p2(sK46(sK35(sK7)))
| ~ spl52_515 ),
inference(avatar_component_clause,[],[f3569]) ).
fof(f3574,definition,
( spl52_516
<=> r1(sK39(sK35(sK7)),sK46(sK35(sK7))) ),
introduced(definition,[new_symbols(definition,[spl52_516])],[avatar_definition]) ).
fof(f3576,plain,
( r1(sK39(sK35(sK7)),sK46(sK35(sK7)))
| ~ spl52_516 ),
inference(avatar_component_clause,[],[f3574]) ).
fof(f3579,definition,
( spl52_517
<=> r1(sK35(sK7),sK39(sK35(sK7))) ),
introduced(definition,[new_symbols(definition,[spl52_517])],[avatar_definition]) ).
fof(f3581,plain,
( r1(sK35(sK7),sK39(sK35(sK7)))
| ~ spl52_517 ),
inference(avatar_component_clause,[],[f3579]) ).
fof(f3650,definition,
( spl52_532
<=> p2(sK40(sK7)) ),
introduced(definition,[new_symbols(definition,[spl52_532])],[avatar_definition]) ).
fof(f3651,plain,
( ~ p2(sK40(sK7))
| spl52_532 ),
inference(avatar_component_clause,[],[f3650]) ).
fof(f3652,plain,
( p2(sK40(sK7))
| ~ spl52_532 ),
inference(avatar_component_clause,[],[f3650]) ).
fof(f3834,plain,
( ~ p2(sK35(sK7))
| ~ sP29(sK7)
| ~ spl52_32
| spl52_34 ),
inference(resolution,[],[f3515,f78]) ).
fof(f3839,plain,
( ~ p2(sK35(sK7))
| ~ spl52_31
| ~ spl52_32
| spl52_34 ),
inference(forward_subsumption_resolution,[],[f3834,f419]) ).
fof(f3840,plain,
( ~ spl52_91
| ~ spl52_31
| ~ spl52_32
| spl52_34 ),
inference(avatar_split_clause,[],[f3839,f431,f421,f417,f795]) ).
fof(f3881,definition,
( spl52_564
<=> ! [X0] :
( ~ r1(sK24(sK7),X0)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_564])],[avatar_definition]) ).
fof(f3882,plain,
( ! [X0] :
( ~ r1(sK24(sK7),X0)
| ~ p2(X0) )
| ~ spl52_564 ),
inference(avatar_component_clause,[],[f3881]) ).
fof(f3885,definition,
( spl52_565
<=> ! [X0] :
( ~ r1(sK22(sK7),X0)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_565])],[avatar_definition]) ).
fof(f3886,plain,
( ! [X0] :
( ~ r1(sK22(sK7),X0)
| ~ p2(X0) )
| ~ spl52_565 ),
inference(avatar_component_clause,[],[f3885]) ).
fof(f3966,plain,
( ~ p2(sK40(sK7))
| ~ sP29(sK7)
| ~ spl52_506 ),
inference(resolution,[],[f3519,f40]) ).
fof(f3985,plain,
( ~ sP29(sK7)
| ~ spl52_506 ),
inference(forward_subsumption_resolution,[],[f3966,f262]) ).
fof(f3986,plain,
( $false
| ~ spl52_31
| ~ spl52_506 ),
inference(forward_subsumption_resolution,[],[f3985,f419]) ).
fof(f3987,plain,
( ~ spl52_31
| ~ spl52_506 ),
inference(avatar_contradiction_clause,[],[f3986]) ).
fof(f3988,plain,
( sP28(sK7)
| ~ sP29(sK7)
| ~ spl52_514 ),
inference(resolution,[],[f3567,f78]) ).
fof(f4140,plain,
( ~ p2(sK40(sK7))
| r1(sK40(sK7),sK42(sK40(sK7)))
| ~ sP29(sK7)
| ~ spl52_89 ),
inference(resolution,[],[f3407,f40]) ).
fof(f4150,plain,
( r1(sK40(sK7),sK42(sK40(sK7)))
| ~ sP29(sK7)
| ~ spl52_89 ),
inference(forward_subsumption_resolution,[],[f4140,f262]) ).
fof(f4156,plain,
( r1(sK40(sK7),sK42(sK40(sK7)))
| ~ spl52_31
| ~ spl52_89 ),
inference(forward_subsumption_resolution,[],[f4150,f419]) ).
fof(f5073,plain,
( ! [X0] :
( ~ r1(sK42(sK40(sK7)),X0)
| ~ p2(X0)
| p2(sK42(sK40(sK7))) )
| ~ spl52_31
| ~ spl52_89 ),
inference(resolution,[],[f4156,f737]) ).
fof(f5075,definition,
( spl52_751
<=> p2(sK42(sK40(sK7))) ),
introduced(definition,[new_symbols(definition,[spl52_751])],[avatar_definition]) ).
fof(f5077,plain,
( p2(sK42(sK40(sK7)))
| ~ spl52_751 ),
inference(avatar_component_clause,[],[f5075]) ).
fof(f5079,definition,
( spl52_752
<=> ! [X0] :
( ~ r1(sK42(sK40(sK7)),X0)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_752])],[avatar_definition]) ).
fof(f5080,plain,
( ! [X0] :
( ~ r1(sK42(sK40(sK7)),X0)
| ~ p2(X0) )
| ~ spl52_752 ),
inference(avatar_component_clause,[],[f5079]) ).
fof(f5129,definition,
( spl52_755
<=> r1(sK35(sK7),sK40(sK7)) ),
introduced(definition,[new_symbols(definition,[spl52_755])],[avatar_definition]) ).
fof(f5130,plain,
( r1(sK35(sK7),sK40(sK7))
| ~ spl52_755 ),
inference(avatar_component_clause,[],[f5129]) ).
fof(f5131,plain,
( ~ r1(sK35(sK7),sK40(sK7))
| spl52_755 ),
inference(avatar_component_clause,[],[f5129]) ).
fof(f5142,plain,
( ~ sP29(sK7)
| spl52_755 ),
inference(resolution,[],[f5131,f40]) ).
fof(f5143,plain,
( $false
| ~ spl52_31
| spl52_755 ),
inference(forward_subsumption_resolution,[],[f5142,f419]) ).
fof(f5144,plain,
( ~ spl52_31
| spl52_755 ),
inference(avatar_contradiction_clause,[],[f5143]) ).
fof(f5427,plain,
( ~ p2(sK48(sK40(sK7)))
| ~ r1(sK35(sK7),sK40(sK7))
| ~ p2(sK40(sK7))
| ~ spl52_89
| ~ spl52_752 ),
inference(resolution,[],[f5080,f3408]) ).
fof(f5478,plain,
( ~ r1(sK35(sK7),sK40(sK7))
| ~ p2(sK40(sK7))
| ~ spl52_89
| ~ spl52_752 ),
inference(forward_subsumption_resolution,[],[f5427,f3409]) ).
fof(f5480,plain,
( ~ p2(sK40(sK7))
| ~ spl52_89
| ~ spl52_752
| ~ spl52_755 ),
inference(forward_subsumption_resolution,[],[f5478,f5130]) ).
fof(f5483,plain,
( ! [X0] :
( ~ p2(sK40(sK7))
| ~ r1(X0,sK40(sK7))
| ~ sP25(X0) )
| ~ spl52_751 ),
inference(resolution,[],[f5077,f266]) ).
fof(f5539,plain,
( ! [X0] :
( ~ r1(X0,sK40(sK7))
| ~ sP25(X0) )
| ~ spl52_532
| ~ spl52_751 ),
inference(forward_subsumption_resolution,[],[f5483,f3652]) ).
fof(f6156,plain,
( ~ sP25(sK35(sK7))
| ~ sP29(sK7)
| ~ spl52_532
| ~ spl52_751 ),
inference(resolution,[],[f5539,f40]) ).
fof(f6160,plain,
( ~ sP29(sK7)
| ~ spl52_89
| ~ spl52_532
| ~ spl52_751 ),
inference(forward_subsumption_resolution,[],[f6156,f789]) ).
fof(f6161,plain,
( $false
| ~ spl52_31
| ~ spl52_89
| ~ spl52_532
| ~ spl52_751 ),
inference(forward_subsumption_resolution,[],[f6160,f419]) ).
fof(f6162,plain,
( ~ spl52_31
| ~ spl52_89
| ~ spl52_532
| ~ spl52_751 ),
inference(avatar_contradiction_clause,[],[f6161]) ).
fof(f6166,plain,
( ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0)
| p2(sK35(sK7)) )
| ~ spl52_31
| ~ spl52_32 ),
inference(forward_subsumption_resolution,[],[f3509,f419]) ).
fof(f6181,plain,
( sP28(sK7)
| ~ spl52_31
| ~ spl52_514 ),
inference(forward_subsumption_resolution,[],[f3988,f419]) ).
fof(f6194,plain,
( p2(sK35(sK7))
| sP26(sK35(sK7))
| sP25(sK35(sK7))
| ~ spl52_29
| ~ spl52_31 ),
inference(forward_subsumption_resolution,[],[f3338,f419]) ).
fof(f6250,plain,
( spl52_91
| spl52_506
| ~ spl52_31
| ~ spl52_32 ),
inference(avatar_split_clause,[],[f6166,f421,f417,f3518,f795]) ).
fof(f6257,plain,
( spl52_33
| ~ spl52_31
| ~ spl52_514 ),
inference(avatar_split_clause,[],[f6181,f3566,f417,f426]) ).
fof(f6261,plain,
( spl52_89
| spl52_90
| spl52_91
| ~ spl52_29
| ~ spl52_31 ),
inference(avatar_split_clause,[],[f6194,f417,f408,f795,f791,f787]) ).
fof(f6413,plain,
( ! [X0] :
( r1(sK35(sK7),sK39(sK35(sK7)))
| ~ r1(X0,sK35(sK7))
| sP28(X0) )
| ~ spl52_91 ),
inference(resolution,[],[f797,f260]) ).
fof(f6414,plain,
( ! [X0] :
( r1(sK39(sK35(sK7)),sK46(sK35(sK7)))
| ~ r1(X0,sK35(sK7))
| sP28(X0) )
| ~ spl52_91 ),
inference(resolution,[],[f797,f270]) ).
fof(f6415,plain,
( ! [X0] :
( p2(sK46(sK35(sK7)))
| ~ r1(X0,sK35(sK7))
| sP28(X0) )
| ~ spl52_91 ),
inference(resolution,[],[f797,f271]) ).
fof(f6422,plain,
( spl52_514
| spl52_515
| ~ spl52_91 ),
inference(avatar_split_clause,[],[f6415,f795,f3569,f3566]) ).
fof(f6423,plain,
( spl52_514
| spl52_516
| ~ spl52_91 ),
inference(avatar_split_clause,[],[f6414,f795,f3574,f3566]) ).
fof(f6424,plain,
( spl52_514
| spl52_517
| ~ spl52_91 ),
inference(avatar_split_clause,[],[f6413,f795,f3579,f3566]) ).
fof(f6496,plain,
( ! [X0] :
( ~ r1(sK22(sK7),X0)
| ~ p2(X0)
| p2(sK22(sK7))
| ~ r1(sK0,sK7)
| ~ p2(sK7) )
| ~ spl52_32
| ~ spl52_45 ),
inference(resolution,[],[f3234,f489]) ).
fof(f6497,plain,
( ! [X0] :
( ~ r1(sK24(sK7),X0)
| ~ p2(X0)
| p2(sK24(sK7))
| ~ r1(sK0,sK7)
| ~ p2(sK7) )
| ~ spl52_32
| ~ spl52_43 ),
inference(resolution,[],[f3234,f481]) ).
fof(f6505,plain,
( ! [X0] :
( ~ r1(sK39(sK8(sK7)),X0)
| ~ p2(X0)
| p2(sK39(sK8(sK7)))
| sP28(sK7)
| ~ p2(sK7)
| ~ r1(sK0,sK7) )
| ~ spl52_30
| ~ spl52_34 ),
inference(resolution,[],[f3268,f947]) ).
fof(f6536,definition,
( spl52_948
<=> p2(sK8(sK7)) ),
introduced(definition,[new_symbols(definition,[spl52_948])],[avatar_definition]) ).
fof(f6537,plain,
( ~ p2(sK8(sK7))
| spl52_948 ),
inference(avatar_component_clause,[],[f6536]) ).
fof(f6554,definition,
( spl52_950
<=> ! [X0] :
( ~ r1(X0,sK8(sK7))
| sP28(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_950])],[avatar_definition]) ).
fof(f6555,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK7))
| sP28(X0) )
| ~ spl52_950 ),
inference(avatar_component_clause,[],[f6554]) ).
fof(f6630,plain,
( ~ p2(sK36(sK7))
| ~ r1(sK0,sK7)
| ~ p2(sK7)
| ~ spl52_40
| ~ spl52_565 ),
inference(resolution,[],[f3886,f456]) ).
fof(f6682,plain,
( ~ r1(sK0,sK7)
| ~ p2(sK7)
| ~ spl52_39
| ~ spl52_40
| ~ spl52_565 ),
inference(forward_subsumption_resolution,[],[f6630,f452]) ).
fof(f6684,plain,
( ~ p2(sK7)
| ~ spl52_30
| ~ spl52_39
| ~ spl52_40
| ~ spl52_565 ),
inference(forward_subsumption_resolution,[],[f6682,f414]) ).
fof(f6685,plain,
( $false
| ~ spl52_30
| ~ spl52_34
| ~ spl52_39
| ~ spl52_40
| ~ spl52_565 ),
inference(forward_subsumption_resolution,[],[f6684,f433]) ).
fof(f6686,plain,
( ~ spl52_30
| ~ spl52_34
| ~ spl52_39
| ~ spl52_40
| ~ spl52_565 ),
inference(avatar_contradiction_clause,[],[f6685]) ).
fof(f6689,plain,
( ! [X0] :
( ~ r1(sK39(sK8(sK7)),X0)
| ~ p2(X0)
| p2(sK39(sK8(sK7)))
| sP28(sK7)
| ~ r1(sK0,sK7) )
| ~ spl52_30
| ~ spl52_34 ),
inference(forward_subsumption_resolution,[],[f6505,f433]) ).
fof(f6691,plain,
( ! [X0] :
( ~ r1(sK39(sK8(sK7)),X0)
| ~ p2(X0)
| p2(sK39(sK8(sK7)))
| sP28(sK7) )
| ~ spl52_30
| ~ spl52_34 ),
inference(forward_subsumption_resolution,[],[f6689,f414]) ).
fof(f6693,definition,
( spl52_973
<=> p2(sK39(sK8(sK7))) ),
introduced(definition,[new_symbols(definition,[spl52_973])],[avatar_definition]) ).
fof(f6695,plain,
( p2(sK39(sK8(sK7)))
| ~ spl52_973 ),
inference(avatar_component_clause,[],[f6693]) ).
fof(f6697,definition,
( spl52_974
<=> ! [X0] :
( ~ r1(sK39(sK8(sK7)),X0)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_974])],[avatar_definition]) ).
fof(f6698,plain,
( ! [X0] :
( ~ r1(sK39(sK8(sK7)),X0)
| ~ p2(X0) )
| ~ spl52_974 ),
inference(avatar_component_clause,[],[f6697]) ).
fof(f6699,plain,
( spl52_33
| spl52_973
| spl52_974
| ~ spl52_30
| ~ spl52_34 ),
inference(avatar_split_clause,[],[f6691,f431,f412,f6697,f6693,f426]) ).
fof(f6809,plain,
( ! [X0,X1] :
( ~ r1(X1,sK46(sK35(sK7)))
| sP26(X0)
| sP25(X0)
| ~ r1(X0,X1)
| ~ r1(sK7,X0)
| p2(X1) )
| ~ spl52_3
| ~ spl52_515 ),
inference(resolution,[],[f3571,f302]) ).
fof(f8206,plain,
( ~ p2(sK46(sK8(sK7)))
| sP28(sK7)
| ~ p2(sK7)
| ~ r1(sK0,sK7)
| ~ spl52_974 ),
inference(resolution,[],[f6698,f953]) ).
fof(f8256,plain,
( sP28(sK7)
| ~ p2(sK7)
| ~ r1(sK0,sK7)
| ~ spl52_974 ),
inference(forward_subsumption_resolution,[],[f8206,f938]) ).
fof(f8260,plain,
( ~ p2(sK7)
| ~ r1(sK0,sK7)
| spl52_33
| ~ spl52_974 ),
inference(forward_subsumption_resolution,[],[f8256,f428]) ).
fof(f8261,plain,
( ~ r1(sK0,sK7)
| spl52_33
| ~ spl52_34
| ~ spl52_974 ),
inference(forward_subsumption_resolution,[],[f8260,f433]) ).
fof(f8262,plain,
( $false
| ~ spl52_30
| spl52_33
| ~ spl52_34
| ~ spl52_974 ),
inference(forward_subsumption_resolution,[],[f8261,f414]) ).
fof(f8263,plain,
( ~ spl52_30
| spl52_33
| ~ spl52_34
| ~ spl52_974 ),
inference(avatar_contradiction_clause,[],[f8262]) ).
fof(f8264,plain,
( ! [X0] :
( ~ p2(sK8(sK7))
| ~ r1(X0,sK8(sK7))
| sP28(X0) )
| ~ spl52_973 ),
inference(resolution,[],[f6695,f261]) ).
fof(f8327,plain,
( sP28(sK7)
| ~ p2(sK7)
| ~ r1(sK0,sK7)
| ~ spl52_950 ),
inference(resolution,[],[f6555,f161]) ).
fof(f8329,plain,
( ~ p2(sK7)
| ~ r1(sK0,sK7)
| spl52_33
| ~ spl52_950 ),
inference(forward_subsumption_resolution,[],[f8327,f428]) ).
fof(f8330,plain,
( ~ r1(sK0,sK7)
| spl52_33
| ~ spl52_34
| ~ spl52_950 ),
inference(forward_subsumption_resolution,[],[f8329,f433]) ).
fof(f8331,plain,
( $false
| ~ spl52_30
| spl52_33
| ~ spl52_34
| ~ spl52_950 ),
inference(forward_subsumption_resolution,[],[f8330,f414]) ).
fof(f8332,plain,
( ~ spl52_30
| spl52_33
| ~ spl52_34
| ~ spl52_950 ),
inference(avatar_contradiction_clause,[],[f8331]) ).
fof(f8337,plain,
( spl52_950
| ~ spl52_948
| ~ spl52_973 ),
inference(avatar_split_clause,[],[f8264,f6693,f6536,f6554]) ).
fof(f8338,plain,
( ~ p2(sK7)
| ~ r1(sK0,sK7)
| spl52_948 ),
inference(resolution,[],[f6537,f162]) ).
fof(f8362,plain,
( ~ p2(sK7)
| ~ spl52_30
| spl52_948 ),
inference(forward_subsumption_resolution,[],[f8338,f414]) ).
fof(f8382,plain,
( ~ spl52_34
| ~ spl52_30
| spl52_948 ),
inference(avatar_split_clause,[],[f8362,f6536,f412,f431]) ).
fof(f8572,definition,
( spl52_1277
<=> p2(sK39(sK35(sK7))) ),
introduced(definition,[new_symbols(definition,[spl52_1277])],[avatar_definition]) ).
fof(f8574,plain,
( p2(sK39(sK35(sK7)))
| ~ spl52_1277 ),
inference(avatar_component_clause,[],[f8572]) ).
fof(f8878,plain,
( ! [X0] :
( sP26(X0)
| sP25(X0)
| ~ r1(X0,sK39(sK35(sK7)))
| ~ r1(sK7,X0)
| p2(sK39(sK35(sK7))) )
| ~ spl52_3
| ~ spl52_515
| ~ spl52_516 ),
inference(resolution,[],[f6809,f3576]) ).
fof(f8880,definition,
( spl52_1323
<=> ! [X0] :
( sP26(X0)
| ~ r1(sK7,X0)
| ~ r1(X0,sK39(sK35(sK7)))
| sP25(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_1323])],[avatar_definition]) ).
fof(f8881,plain,
( ! [X0] :
( ~ r1(X0,sK39(sK35(sK7)))
| ~ r1(sK7,X0)
| sP26(X0)
| sP25(X0) )
| ~ spl52_1323 ),
inference(avatar_component_clause,[],[f8880]) ).
fof(f8882,plain,
( spl52_1277
| spl52_1323
| ~ spl52_3
| ~ spl52_515
| ~ spl52_516 ),
inference(avatar_split_clause,[],[f8878,f3574,f3569,f301,f8880,f8572]) ).
fof(f9026,definition,
( spl52_1348
<=> r1(sK7,sK35(sK7)) ),
introduced(definition,[new_symbols(definition,[spl52_1348])],[avatar_definition]) ).
fof(f9027,plain,
( r1(sK7,sK35(sK7))
| ~ spl52_1348 ),
inference(avatar_component_clause,[],[f9026]) ).
fof(f9028,plain,
( ~ r1(sK7,sK35(sK7))
| spl52_1348 ),
inference(avatar_component_clause,[],[f9026]) ).
fof(f9034,plain,
( ~ sP29(sK7)
| spl52_1348 ),
inference(resolution,[],[f9028,f78]) ).
fof(f9035,plain,
( $false
| ~ spl52_31
| spl52_1348 ),
inference(forward_subsumption_resolution,[],[f9034,f419]) ).
fof(f9036,plain,
( ~ spl52_31
| spl52_1348 ),
inference(avatar_contradiction_clause,[],[f9035]) ).
fof(f10284,plain,
( ~ r1(sK7,sK35(sK7))
| sP26(sK35(sK7))
| sP25(sK35(sK7))
| ~ spl52_517
| ~ spl52_1323 ),
inference(resolution,[],[f8881,f3581]) ).
fof(f10317,plain,
( ! [X0] :
( ~ p2(sK35(sK7))
| ~ r1(X0,sK35(sK7))
| sP28(X0) )
| ~ spl52_1277 ),
inference(resolution,[],[f8574,f261]) ).
fof(f10373,plain,
( ! [X0] :
( ~ r1(X0,sK35(sK7))
| sP28(X0) )
| ~ spl52_91
| ~ spl52_1277 ),
inference(forward_subsumption_resolution,[],[f10317,f797]) ).
fof(f10374,plain,
( spl52_514
| ~ spl52_91
| ~ spl52_1277 ),
inference(avatar_split_clause,[],[f10373,f8572,f795,f3566]) ).
fof(f10385,plain,
( spl52_751
| spl52_752
| ~ spl52_31
| ~ spl52_89 ),
inference(avatar_split_clause,[],[f5073,f787,f417,f5079,f5075]) ).
fof(f10398,plain,
( ~ spl52_532
| ~ spl52_89
| ~ spl52_752
| ~ spl52_755 ),
inference(avatar_split_clause,[],[f5480,f5129,f5079,f787,f3650]) ).
fof(f10404,plain,
( sP26(sK35(sK7))
| sP25(sK35(sK7))
| ~ spl52_517
| ~ spl52_1323
| ~ spl52_1348 ),
inference(forward_subsumption_resolution,[],[f10284,f9027]) ).
fof(f10447,plain,
( spl52_89
| spl52_90
| ~ spl52_517
| ~ spl52_1323
| ~ spl52_1348 ),
inference(avatar_split_clause,[],[f10404,f9026,f8880,f3579,f791,f787]) ).
fof(f10458,plain,
( ~ sP29(sK7)
| spl52_532 ),
inference(resolution,[],[f3651,f262]) ).
fof(f10459,plain,
( $false
| ~ spl52_31
| spl52_532 ),
inference(forward_subsumption_resolution,[],[f10458,f419]) ).
fof(f10460,plain,
( ~ spl52_31
| spl52_532 ),
inference(avatar_contradiction_clause,[],[f10459]) ).
fof(f10463,plain,
( ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0)
| r1(X0,sK44(X0)) )
| ~ spl52_90 ),
inference(resolution,[],[f793,f268]) ).
fof(f10464,plain,
( ! [X0] :
( r1(sK44(X0),sK49(X0))
| ~ r1(sK35(sK7),X0)
| ~ p2(X0) )
| ~ spl52_90 ),
inference(resolution,[],[f793,f276]) ).
fof(f10465,plain,
( ! [X0] :
( ~ r1(sK35(sK7),X0)
| ~ p2(X0)
| p2(sK49(X0)) )
| ~ spl52_90 ),
inference(resolution,[],[f793,f277]) ).
fof(f10509,plain,
( ~ p2(sK40(sK7))
| r1(sK40(sK7),sK44(sK40(sK7)))
| ~ sP29(sK7)
| ~ spl52_90 ),
inference(resolution,[],[f10463,f40]) ).
fof(f10521,plain,
( r1(sK40(sK7),sK44(sK40(sK7)))
| ~ sP29(sK7)
| ~ spl52_90 ),
inference(forward_subsumption_resolution,[],[f10509,f262]) ).
fof(f10528,plain,
( r1(sK40(sK7),sK44(sK40(sK7)))
| ~ spl52_31
| ~ spl52_90 ),
inference(forward_subsumption_resolution,[],[f10521,f419]) ).
fof(f10965,plain,
( ! [X0] :
( ~ r1(sK44(sK40(sK7)),X0)
| ~ p2(X0)
| p2(sK44(sK40(sK7))) )
| ~ spl52_31
| ~ spl52_90 ),
inference(resolution,[],[f10528,f737]) ).
fof(f10967,definition,
( spl52_1617
<=> p2(sK44(sK40(sK7))) ),
introduced(definition,[new_symbols(definition,[spl52_1617])],[avatar_definition]) ).
fof(f10969,plain,
( p2(sK44(sK40(sK7)))
| ~ spl52_1617 ),
inference(avatar_component_clause,[],[f10967]) ).
fof(f10971,definition,
( spl52_1618
<=> ! [X0] :
( ~ r1(sK44(sK40(sK7)),X0)
| ~ p2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_1618])],[avatar_definition]) ).
fof(f10972,plain,
( ! [X0] :
( ~ r1(sK44(sK40(sK7)),X0)
| ~ p2(X0) )
| ~ spl52_1618 ),
inference(avatar_component_clause,[],[f10971]) ).
fof(f10973,plain,
( spl52_1617
| spl52_1618
| ~ spl52_31
| ~ spl52_90 ),
inference(avatar_split_clause,[],[f10965,f791,f417,f10971,f10967]) ).
fof(f11516,plain,
( ~ p2(sK49(sK40(sK7)))
| ~ r1(sK35(sK7),sK40(sK7))
| ~ p2(sK40(sK7))
| ~ spl52_90
| ~ spl52_1618 ),
inference(resolution,[],[f10972,f10464]) ).
fof(f11566,plain,
( ~ r1(sK35(sK7),sK40(sK7))
| ~ p2(sK40(sK7))
| ~ spl52_90
| ~ spl52_1618 ),
inference(forward_subsumption_resolution,[],[f11516,f10465]) ).
fof(f11567,plain,
( ~ p2(sK40(sK7))
| ~ spl52_90
| ~ spl52_755
| ~ spl52_1618 ),
inference(forward_subsumption_resolution,[],[f11566,f5130]) ).
fof(f11568,plain,
( $false
| ~ spl52_90
| ~ spl52_532
| ~ spl52_755
| ~ spl52_1618 ),
inference(forward_subsumption_resolution,[],[f11567,f3652]) ).
fof(f11569,plain,
( ~ spl52_90
| ~ spl52_532
| ~ spl52_755
| ~ spl52_1618 ),
inference(avatar_contradiction_clause,[],[f11568]) ).
fof(f11573,plain,
( ! [X0] :
( ~ p2(sK40(sK7))
| ~ r1(X0,sK40(sK7))
| ~ sP26(X0) )
| ~ spl52_1617 ),
inference(resolution,[],[f10969,f269]) ).
fof(f11634,plain,
( ! [X0] :
( ~ sP26(X0)
| ~ r1(X0,sK40(sK7)) )
| ~ spl52_532
| ~ spl52_1617 ),
inference(forward_subsumption_resolution,[],[f11573,f3652]) ).
fof(f12368,plain,
( ~ r1(sK35(sK7),sK40(sK7))
| ~ spl52_90
| ~ spl52_532
| ~ spl52_1617 ),
inference(resolution,[],[f11634,f793]) ).
fof(f12369,plain,
( $false
| ~ spl52_90
| ~ spl52_532
| ~ spl52_755
| ~ spl52_1617 ),
inference(forward_subsumption_resolution,[],[f12368,f5130]) ).
fof(f12370,plain,
( ~ spl52_90
| ~ spl52_532
| ~ spl52_755
| ~ spl52_1617 ),
inference(avatar_contradiction_clause,[],[f12369]) ).
fof(f12442,plain,
( ! [X0] :
( p2(sK22(sK18))
| ~ r1(sK22(sK18),X0)
| ~ p2(X0)
| ~ r1(sK0,sK18)
| ~ p2(sK18) )
| ~ spl52_10
| ~ spl52_45 ),
inference(resolution,[],[f334,f489]) ).
fof(f12469,plain,
( ! [X0] :
( ~ r1(sK22(sK18),X0)
| ~ p2(X0)
| ~ r1(sK0,sK18)
| ~ p2(sK18) )
| ~ spl52_10
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f12442,f485]) ).
fof(f12472,plain,
( ! [X0] :
( ~ r1(sK22(sK18),X0)
| ~ p2(X0)
| ~ p2(sK18) )
| ~ spl52_8
| ~ spl52_10
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f12469,f325]) ).
fof(f12497,plain,
( ! [X0] :
( ~ r1(sK22(sK18),X0)
| ~ p2(X0) )
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f12472,f330]) ).
fof(f12759,plain,
( ~ p2(sK36(sK18))
| ~ r1(sK0,sK18)
| ~ p2(sK18)
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_40
| ~ spl52_44
| ~ spl52_45 ),
inference(resolution,[],[f12497,f456]) ).
fof(f12808,plain,
( ~ r1(sK0,sK18)
| ~ p2(sK18)
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_39
| ~ spl52_40
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f12759,f452]) ).
fof(f12814,plain,
( ~ p2(sK18)
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_39
| ~ spl52_40
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f12808,f325]) ).
fof(f12815,plain,
( $false
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_39
| ~ spl52_40
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f12814,f330]) ).
fof(f12816,plain,
( ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_39
| ~ spl52_40
| ~ spl52_44
| ~ spl52_45 ),
inference(avatar_contradiction_clause,[],[f12815]) ).
fof(f13296,plain,
( ! [X0] :
( ~ r1(sK0,sK18)
| ~ p2(sK18)
| p2(sK24(sK18))
| ~ r1(sK24(sK18),X0)
| ~ p2(X0) )
| ~ spl52_10
| ~ spl52_43 ),
inference(resolution,[],[f481,f334]) ).
fof(f13354,plain,
( ! [X0] :
( ~ r1(sK0,sK18)
| ~ p2(sK18)
| ~ r1(sK24(sK18),X0)
| ~ p2(X0) )
| ~ spl52_10
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f13296,f477]) ).
fof(f13361,plain,
( ! [X0] :
( ~ p2(sK18)
| ~ r1(sK24(sK18),X0)
| ~ p2(X0) )
| ~ spl52_8
| ~ spl52_10
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f13354,f325]) ).
fof(f13363,plain,
( ! [X0] :
( ~ r1(sK24(sK18),X0)
| ~ p2(X0) )
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f13361,f330]) ).
fof(f13434,plain,
( ~ p2(sK37(sK18))
| ~ r1(sK0,sK18)
| ~ p2(sK18)
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_37
| ~ spl52_42
| ~ spl52_43 ),
inference(resolution,[],[f13363,f445]) ).
fof(f13490,plain,
( ~ r1(sK0,sK18)
| ~ p2(sK18)
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_36
| ~ spl52_37
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f13434,f441]) ).
fof(f13496,plain,
( ~ p2(sK18)
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_36
| ~ spl52_37
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f13490,f325]) ).
fof(f13497,plain,
( $false
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_36
| ~ spl52_37
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f13496,f330]) ).
fof(f13498,plain,
( ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_36
| ~ spl52_37
| ~ spl52_42
| ~ spl52_43 ),
inference(avatar_contradiction_clause,[],[f13497]) ).
fof(f13532,plain,
( ! [X0] :
( ~ r1(sK22(sK7),X0)
| ~ p2(X0)
| ~ r1(sK0,sK7)
| ~ p2(sK7) )
| ~ spl52_32
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f6496,f485]) ).
fof(f13533,plain,
( ! [X0] :
( ~ r1(sK24(sK7),X0)
| ~ p2(X0)
| ~ r1(sK0,sK7)
| ~ p2(sK7) )
| ~ spl52_32
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f6497,f477]) ).
fof(f13592,plain,
( ! [X0] :
( ~ r1(sK22(sK7),X0)
| ~ p2(X0)
| ~ r1(sK0,sK7) )
| ~ spl52_32
| ~ spl52_34
| ~ spl52_44
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f13532,f433]) ).
fof(f13593,plain,
( ! [X0] :
( ~ r1(sK24(sK7),X0)
| ~ p2(X0)
| ~ r1(sK0,sK7) )
| ~ spl52_32
| ~ spl52_34
| ~ spl52_42
| ~ spl52_43 ),
inference(forward_subsumption_resolution,[],[f13533,f433]) ).
fof(f13618,plain,
( ~ spl52_30
| spl52_565
| ~ spl52_32
| ~ spl52_34
| ~ spl52_44
| ~ spl52_45 ),
inference(avatar_split_clause,[],[f13592,f488,f484,f431,f421,f3885,f412]) ).
fof(f13619,plain,
( ~ spl52_30
| spl52_564
| ~ spl52_32
| ~ spl52_34
| ~ spl52_42
| ~ spl52_43 ),
inference(avatar_split_clause,[],[f13593,f480,f476,f431,f421,f3881,f412]) ).
fof(f14135,plain,
( ~ p2(sK37(sK7))
| ~ r1(sK0,sK7)
| ~ p2(sK7)
| ~ spl52_37
| ~ spl52_564 ),
inference(resolution,[],[f3882,f445]) ).
fof(f14145,plain,
( ~ r1(sK0,sK7)
| ~ p2(sK7)
| ~ spl52_36
| ~ spl52_37
| ~ spl52_564 ),
inference(forward_subsumption_resolution,[],[f14135,f441]) ).
fof(f14146,plain,
( ~ p2(sK7)
| ~ spl52_30
| ~ spl52_36
| ~ spl52_37
| ~ spl52_564 ),
inference(forward_subsumption_resolution,[],[f14145,f414]) ).
fof(f14147,plain,
( $false
| ~ spl52_30
| ~ spl52_34
| ~ spl52_36
| ~ spl52_37
| ~ spl52_564 ),
inference(forward_subsumption_resolution,[],[f14146,f433]) ).
fof(f14148,plain,
( ~ spl52_30
| ~ spl52_34
| ~ spl52_36
| ~ spl52_37
| ~ spl52_564 ),
inference(avatar_contradiction_clause,[],[f14147]) ).
cnf(s5,plain,
( spl52_3
| spl52_7
| spl52_8 ),
inference(sat_conversion,[],[f326]) ).
cnf(s6,plain,
( spl52_3
| spl52_7
| spl52_9 ),
inference(sat_conversion,[],[f331]) ).
cnf(s7,plain,
( spl52_3
| spl52_7
| spl52_10 ),
inference(sat_conversion,[],[f335]) ).
cnf(s22,plain,
( spl52_7
| spl52_10
| spl52_29 ),
inference(sat_conversion,[],[f410]) ).
cnf(s23,plain,
( spl52_7
| spl52_10
| spl52_30 ),
inference(sat_conversion,[],[f415]) ).
cnf(s24,plain,
( spl52_7
| spl52_10
| spl52_31
| spl52_32 ),
inference(sat_conversion,[],[f424]) ).
cnf(s25,plain,
( spl52_7
| spl52_10
| spl52_32
| ~ spl52_33 ),
inference(sat_conversion,[],[f429]) ).
cnf(s26,plain,
( spl52_7
| spl52_10
| spl52_31
| spl52_34 ),
inference(sat_conversion,[],[f434]) ).
cnf(s27,plain,
( spl52_7
| spl52_10
| ~ spl52_33
| spl52_34 ),
inference(sat_conversion,[],[f435]) ).
cnf(s28,plain,
( spl52_35
| spl52_36 ),
inference(sat_conversion,[],[f442]) ).
cnf(s29,plain,
( spl52_35
| spl52_37 ),
inference(sat_conversion,[],[f446]) ).
cnf(s30,plain,
( spl52_38
| spl52_39 ),
inference(sat_conversion,[],[f453]) ).
cnf(s31,plain,
( spl52_38
| spl52_40 ),
inference(sat_conversion,[],[f457]) ).
cnf(s32,plain,
( spl52_39
| spl52_41 ),
inference(sat_conversion,[],[f461]) ).
cnf(s33,plain,
( spl52_40
| spl52_41 ),
inference(sat_conversion,[],[f462]) ).
cnf(s46,plain,
( spl52_35
| spl52_42 ),
inference(sat_conversion,[],[f478]) ).
cnf(s47,plain,
( spl52_35
| spl52_43 ),
inference(sat_conversion,[],[f482]) ).
cnf(s48,plain,
( spl52_41
| spl52_44 ),
inference(sat_conversion,[],[f486]) ).
cnf(s49,plain,
( spl52_41
| spl52_45 ),
inference(sat_conversion,[],[f490]) ).
cnf(s50,plain,
( spl52_38
| spl52_44 ),
inference(sat_conversion,[],[f491]) ).
cnf(s51,plain,
( spl52_38
| spl52_45 ),
inference(sat_conversion,[],[f492]) ).
cnf(s54,plain,
( spl52_7
| spl52_8
| spl52_29 ),
inference(sat_conversion,[],[f495]) ).
cnf(s55,plain,
( spl52_7
| spl52_9
| spl52_29 ),
inference(sat_conversion,[],[f496]) ).
cnf(s56,plain,
( spl52_38
| spl52_46 ),
inference(sat_conversion,[],[f501]) ).
cnf(s57,plain,
( spl52_41
| spl52_46 ),
inference(sat_conversion,[],[f502]) ).
cnf(s58,plain,
( spl52_38
| spl52_47 ),
inference(sat_conversion,[],[f507]) ).
cnf(s59,plain,
( spl52_41
| spl52_47 ),
inference(sat_conversion,[],[f508]) ).
cnf(s60,plain,
( spl52_7
| spl52_9
| spl52_30 ),
inference(sat_conversion,[],[f509]) ).
cnf(s61,plain,
( spl52_7
| spl52_8
| spl52_30 ),
inference(sat_conversion,[],[f510]) ).
cnf(s62,plain,
( spl52_7
| spl52_9
| spl52_31
| spl52_32 ),
inference(sat_conversion,[],[f511]) ).
cnf(s63,plain,
( spl52_7
| spl52_8
| spl52_31
| spl52_32 ),
inference(sat_conversion,[],[f512]) ).
cnf(s64,plain,
( spl52_7
| spl52_9
| spl52_32
| ~ spl52_33 ),
inference(sat_conversion,[],[f513]) ).
cnf(s65,plain,
( spl52_7
| spl52_8
| spl52_32
| ~ spl52_33 ),
inference(sat_conversion,[],[f514]) ).
cnf(s66,plain,
( spl52_7
| spl52_9
| spl52_31
| spl52_34 ),
inference(sat_conversion,[],[f515]) ).
cnf(s67,plain,
( spl52_7
| spl52_8
| spl52_31
| spl52_34 ),
inference(sat_conversion,[],[f516]) ).
cnf(s68,plain,
( spl52_7
| spl52_9
| ~ spl52_33
| spl52_34 ),
inference(sat_conversion,[],[f517]) ).
cnf(s69,plain,
( spl52_7
| spl52_8
| ~ spl52_33
| spl52_34 ),
inference(sat_conversion,[],[f518]) ).
cnf(s84,plain,
( spl52_35
| spl52_52 ),
inference(sat_conversion,[],[f553]) ).
cnf(s85,plain,
( spl52_35
| spl52_53 ),
inference(sat_conversion,[],[f558]) ).
cnf(s102,plain,
( ~ spl52_35
| ~ spl52_38
| ~ spl52_41 ),
inference(sat_conversion,[],[f682]) ).
cnf(s110,plain,
( ~ spl52_46
| ~ spl52_47
| spl52_81 ),
inference(sat_conversion,[],[f736]) ).
cnf(s172,plain,
( ~ spl52_46
| ~ spl52_47
| spl52_166 ),
inference(sat_conversion,[],[f1350]) ).
cnf(s177,plain,
( ~ spl52_7
| ~ spl52_166
| spl52_174
| spl52_175 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s178,plain,
( ~ spl52_7
| ~ spl52_166
| spl52_175
| spl52_176 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s203,plain,
( ~ spl52_46
| ~ spl52_47
| ~ spl52_175 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s238,plain,
( ~ spl52_7
| ~ spl52_46
| ~ spl52_47
| ~ spl52_81
| ~ spl52_166
| ~ spl52_174
| spl52_175
| ~ spl52_176 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s252,plain,
( ~ spl52_52
| ~ spl52_53
| spl52_267 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s283,plain,
( ~ spl52_7
| ~ spl52_302
| spl52_316
| spl52_317 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s358,plain,
( ~ spl52_267
| spl52_305
| spl52_306
| ~ spl52_317 ),
inference(sat_conversion,[],[f2770]) ).
cnf(s384,plain,
( ~ spl52_7
| ~ spl52_52
| ~ spl52_53
| ~ spl52_305 ),
inference(sat_conversion,[],[f2977]) ).
cnf(s406,plain,
( ~ spl52_7
| ~ spl52_302
| ~ spl52_306
| spl52_316 ),
inference(sat_conversion,[],[f3125]) ).
cnf(s408,plain,
( ~ spl52_52
| ~ spl52_53
| spl52_302 ),
inference(sat_conversion,[],[f3133]) ).
cnf(s414,plain,
( ~ spl52_52
| ~ spl52_53
| ~ spl52_316 ),
inference(sat_conversion,[],[f3176]) ).
cnf(s504,plain,
( ~ spl52_31
| ~ spl52_32
| spl52_34
| ~ spl52_91 ),
inference(sat_conversion,[],[f3840]) ).
cnf(s533,plain,
( ~ spl52_31
| ~ spl52_506 ),
inference(sat_conversion,[],[f3987]) ).
cnf(s668,plain,
( ~ spl52_31
| spl52_755 ),
inference(sat_conversion,[],[f5144]) ).
cnf(s781,plain,
( ~ spl52_31
| ~ spl52_89
| ~ spl52_532
| ~ spl52_751 ),
inference(sat_conversion,[],[f6162]) ).
cnf(s804,plain,
( ~ spl52_31
| ~ spl52_32
| spl52_91
| spl52_506 ),
inference(sat_conversion,[],[f6250]) ).
cnf(s808,plain,
( ~ spl52_31
| spl52_33
| ~ spl52_514 ),
inference(sat_conversion,[],[f6257]) ).
cnf(s812,plain,
( ~ spl52_29
| ~ spl52_31
| spl52_89
| spl52_90
| spl52_91 ),
inference(sat_conversion,[],[f6261]) ).
cnf(s853,plain,
( ~ spl52_91
| spl52_514
| spl52_515 ),
inference(sat_conversion,[],[f6422]) ).
cnf(s854,plain,
( ~ spl52_91
| spl52_514
| spl52_516 ),
inference(sat_conversion,[],[f6423]) ).
cnf(s855,plain,
( ~ spl52_91
| spl52_514
| spl52_517 ),
inference(sat_conversion,[],[f6424]) ).
cnf(s884,plain,
( ~ spl52_30
| ~ spl52_34
| ~ spl52_39
| ~ spl52_40
| ~ spl52_565 ),
inference(sat_conversion,[],[f6686]) ).
cnf(s888,plain,
( ~ spl52_30
| spl52_33
| ~ spl52_34
| spl52_973
| spl52_974 ),
inference(sat_conversion,[],[f6699]) ).
cnf(s1082,plain,
( ~ spl52_30
| spl52_33
| ~ spl52_34
| ~ spl52_974 ),
inference(sat_conversion,[],[f8263]) ).
cnf(s1092,plain,
( ~ spl52_30
| spl52_33
| ~ spl52_34
| ~ spl52_950 ),
inference(sat_conversion,[],[f8332]) ).
cnf(s1094,plain,
( ~ spl52_948
| spl52_950
| ~ spl52_973 ),
inference(sat_conversion,[],[f8337]) ).
cnf(s1108,plain,
( ~ spl52_30
| ~ spl52_34
| spl52_948 ),
inference(sat_conversion,[],[f8382]) ).
cnf(s1153,plain,
( ~ spl52_3
| ~ spl52_515
| ~ spl52_516
| spl52_1277
| spl52_1323 ),
inference(sat_conversion,[],[f8882]) ).
cnf(s1175,plain,
( ~ spl52_31
| spl52_1348 ),
inference(sat_conversion,[],[f9036]) ).
cnf(s1310,plain,
( ~ spl52_91
| spl52_514
| ~ spl52_1277 ),
inference(sat_conversion,[],[f10374]) ).
cnf(s1312,plain,
( ~ spl52_31
| ~ spl52_89
| spl52_751
| spl52_752 ),
inference(sat_conversion,[],[f10385]) ).
cnf(s1316,plain,
( ~ spl52_89
| ~ spl52_532
| ~ spl52_752
| ~ spl52_755 ),
inference(sat_conversion,[],[f10398]) ).
cnf(s1338,plain,
( spl52_89
| spl52_90
| ~ spl52_517
| ~ spl52_1323
| ~ spl52_1348 ),
inference(sat_conversion,[],[f10447]) ).
cnf(s1340,plain,
( ~ spl52_31
| spl52_532 ),
inference(sat_conversion,[],[f10460]) ).
cnf(s1403,plain,
( ~ spl52_31
| ~ spl52_90
| spl52_1617
| spl52_1618 ),
inference(sat_conversion,[],[f10973]) ).
cnf(s1475,plain,
( ~ spl52_90
| ~ spl52_532
| ~ spl52_755
| ~ spl52_1618 ),
inference(sat_conversion,[],[f11569]) ).
cnf(s1561,plain,
( ~ spl52_90
| ~ spl52_532
| ~ spl52_755
| ~ spl52_1617 ),
inference(sat_conversion,[],[f12370]) ).
cnf(s1615,plain,
( ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_39
| ~ spl52_40
| ~ spl52_44
| ~ spl52_45 ),
inference(sat_conversion,[],[f12816]) ).
cnf(s1716,plain,
( ~ spl52_8
| ~ spl52_9
| ~ spl52_10
| ~ spl52_36
| ~ spl52_37
| ~ spl52_42
| ~ spl52_43 ),
inference(sat_conversion,[],[f13498]) ).
cnf(s1754,plain,
( ~ spl52_30
| ~ spl52_32
| ~ spl52_34
| ~ spl52_44
| ~ spl52_45
| spl52_565 ),
inference(sat_conversion,[],[f13618]) ).
cnf(s1755,plain,
( ~ spl52_30
| ~ spl52_32
| ~ spl52_34
| ~ spl52_42
| ~ spl52_43
| spl52_564 ),
inference(sat_conversion,[],[f13619]) ).
cnf(s1835,plain,
( ~ spl52_30
| ~ spl52_34
| ~ spl52_36
| ~ spl52_37
| ~ spl52_564 ),
inference(sat_conversion,[],[f14148]) ).
cnf(s1836,plain,
( spl52_35
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10 ),
inference(rat,[],[s1716,s28,s29,s46,s47]) ).
cnf(s1837,plain,
( spl52_38
| ~ spl52_8
| ~ spl52_9
| ~ spl52_10 ),
inference(rat,[],[s1615,s30,s31,s50,s51]) ).
cnf(s1838,plain,
( ~ spl52_8
| ~ spl52_10
| ~ spl52_9 ),
inference(rat,[],[s1615,s32,s33,s48,s49,s102,s1837,s1836]) ).
cnf(s1839,plain,
( spl52_7
| spl52_3 ),
inference(rat,[],[s1838,s5,s6,s7]) ).
cnf(s1840,plain,
( spl52_38
| ~ spl52_7 ),
inference(rat,[],[s238,s177,s178,s110,s172,s203,s56,s58]) ).
cnf(s1841,plain,
( spl52_41
| ~ spl52_7 ),
inference(rat,[],[s238,s177,s178,s110,s172,s203,s57,s59]) ).
cnf(s1842,plain,
~ spl52_7,
inference(rat,[],[s358,s283,s406,s252,s384,s408,s414,s84,s85,s102,s1841,s1840]) ).
cnf(s1843,plain,
spl52_3,
inference(rat,[],[s1839,s1842]) ).
cnf(s1844,plain,
( spl52_31
| spl52_10
| spl52_38 ),
inference(rat,[],[s1754,s884,s24,s26,s51,s50,s31,s30,s23,s1842]) ).
cnf(s1845,plain,
( ~ spl52_32
| spl52_10
| spl52_38 ),
inference(rat,[],[s884,s1754,s504,s804,s51,s50,s31,s30,s23,s533,s1844,s1842]) ).
cnf(s1846,plain,
( ~ spl52_34
| spl52_33
| ~ spl52_30 ),
inference(rat,[],[s1094,s888,s1082,s1092,s1108]) ).
cnf(s1847,plain,
( ~ spl52_90
| ~ spl52_31 ),
inference(rat,[],[s1403,s1475,s1561,s1340,s668]) ).
cnf(s1848,plain,
( ~ spl52_89
| ~ spl52_31 ),
inference(rat,[],[s781,s1312,s1316,s1340,s668]) ).
cnf(s1849,plain,
( spl52_10
| spl52_38 ),
inference(rat,[],[s1153,s1338,s853,s854,s855,s1310,s812,s1848,s1847,s808,s25,s1845,s1175,s1844,s22,s1843,s1842]) ).
cnf(s1850,plain,
( spl52_514
| ~ spl52_91
| spl52_89
| spl52_90
| ~ spl52_1348 ),
inference(rat,[],[s1153,s1338,s853,s854,s855,s1310,s1843]) ).
cnf(s1851,plain,
( ~ spl52_33
| spl52_9
| spl52_38 ),
inference(rat,[],[s1754,s884,s64,s68,s51,s50,s31,s30,s60,s1842]) ).
cnf(s1852,plain,
( spl52_9
| spl52_38 ),
inference(rat,[],[s1850,s812,s808,s1848,s1847,s1175,s66,s1846,s1851,s55,s60,s1842]) ).
cnf(s1853,plain,
( ~ spl52_33
| spl52_38 ),
inference(rat,[],[s1754,s884,s65,s69,s51,s50,s31,s30,s61,s1838,s1852,s1849,s1842]) ).
cnf(s1854,plain,
spl52_38,
inference(rat,[],[s1850,s812,s808,s1848,s1847,s1175,s67,s1846,s1853,s54,s61,s1838,s1852,s1849,s1842]) ).
cnf(s1855,plain,
( spl52_35
| ~ spl52_32
| ~ spl52_34
| ~ spl52_30 ),
inference(rat,[],[s1835,s1755,s28,s29,s46,s47]) ).
cnf(s1856,plain,
( ~ spl52_32
| ~ spl52_34
| ~ spl52_30 ),
inference(rat,[],[s884,s1754,s32,s33,s48,s49,s102,s1855,s1854]) ).
cnf(s1857,plain,
( ~ spl52_33
| spl52_10 ),
inference(rat,[],[s1856,s25,s27,s23,s1842]) ).
cnf(s1858,plain,
spl52_10,
inference(rat,[],[s1850,s812,s808,s1848,s1847,s1175,s26,s1846,s1857,s22,s23,s1842]) ).
cnf(s1859,plain,
spl52_29,
inference(rat,[],[s1838,s54,s55,s1858,s1842]) ).
cnf(s1860,plain,
( spl52_32
| ~ spl52_33 ),
inference(rat,[],[s1838,s65,s64,s1842,s1858]) ).
cnf(s1861,plain,
spl52_30,
inference(rat,[],[s1838,s61,s60,s1858,s1842]) ).
cnf(s1862,plain,
( ~ spl52_32
| ~ spl52_31
| ~ spl52_91 ),
inference(rat,[],[s1856,s504,s1861]) ).
cnf(s1863,plain,
~ spl52_31,
inference(rat,[],[s1862,s1860,s808,s1850,s812,s1848,s1847,s1175,s1859]) ).
cnf(s1864,plain,
spl52_32,
inference(rat,[],[s1838,s63,s62,s1858,s1842,s1863]) ).
cnf(s1865,plain,
~ spl52_34,
inference(rat,[],[s1856,s1861,s1864]) ).
cnf(s1866,plain,
spl52_9,
inference(rat,[],[s66,s1863,s1842,s1865]) ).
cnf(s1867,plain,
spl52_8,
inference(rat,[],[s67,s1863,s1842,s1865]) ).
cnf(s1869,plain,
$false,
inference(rat,[],[s1838,s1858,s1867,s1866]) ).
fof(f14149,plain,
$false,
inference(avatar_sat_refutation,[],[s1869]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL660+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 16:26:31 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 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
% 1.87/0.73 % (1835272)Will run a generic schedule for satisfiability detection.
% 1.87/0.73 % (1835282)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1605012935:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.87/0.73 % (1835278)% WARNING: option uhcvi not known.
% 1.87/0.73 % (1835280)dis+10_1_sil=32000:sp=arity:random_seed=1979309772:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.87/0.73 % (1835277)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=374117156_2999 on theBenchmark for (2999ds/0Mi)
% 1.87/0.73 % (1835279)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=820303038:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.87/0.73 % (1835281)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=307948507:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.87/0.73 % (1835283)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2211694055:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.87/0.73 % (1835278)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2010718785:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.87/0.73 % TRYING [1]
% 1.87/0.73 % TRYING [2]
% 1.87/0.73 % TRYING [3]
% 1.87/0.73 % TRYING [4]
% 1.87/0.73 % (1835282)Instruction limit reached!
% 1.87/0.73 % (1835282)------------------------------
% 1.87/0.73 % (1835282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.73 % (1835282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.73 % (1835282)CaDiCaL version: 2.1.3
% 1.87/0.73 % (1835282)Termination reason: Instruction limit
% 1.87/0.73 % (1835282)Termination phase: Saturation
% 1.87/0.73 % (1835282)Time elapsed: 0.047 s
% 1.87/0.73 % (1835282)Peak memory usage: 14 MB
% 1.87/0.73 % (1835282)Instructions burned: 134 (million)
% 1.87/0.73 % (1835291)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2638700322:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.87/0.73 % TRYING [1]
% 1.87/0.73 % TRYING [2]
% 1.87/0.73 % TRYING [3]
% 1.87/0.73 % TRYING [4]
% 1.87/0.73 % (1835280)Instruction limit reached!
% 1.87/0.73 % (1835280)------------------------------
% 1.87/0.73 % (1835280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.73 % (1835280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.73 % (1835280)CaDiCaL version: 2.1.3
% 1.87/0.73 % (1835280)Termination reason: Instruction limit
% 1.87/0.73 % (1835280)Termination phase: Saturation
% 1.87/0.73 % (1835280)Time elapsed: 0.062 s
% 1.87/0.73 % (1835280)Peak memory usage: 13 MB
% 1.87/0.73 % (1835280)Instructions burned: 105 (million)
% 1.87/0.73 % (1835281)Instruction limit reached!
% 1.87/0.73 % (1835281)------------------------------
% 1.87/0.73 % (1835281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.73 % (1835281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.73 % (1835281)CaDiCaL version: 2.1.3
% 1.87/0.73 % (1835281)Termination reason: Instruction limit
% 1.87/0.73 % (1835281)Termination phase: Saturation
% 1.87/0.73 % (1835281)Time elapsed: 0.062 s
% 1.87/0.73 % (1835281)Peak memory usage: 12 MB
% 1.87/0.73 % (1835281)Instructions burned: 116 (million)
% 1.87/0.73 % TRYING [5]
% 1.87/0.73 % (1835293)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=500111742:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.87/0.73 % (1835283)Instruction limit reached!
% 1.87/0.73 % (1835283)------------------------------
% 1.87/0.73 % (1835283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.73 % (1835283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.73 % (1835283)CaDiCaL version: 2.1.3
% 1.87/0.73 % (1835283)Termination reason: Instruction limit
% 1.87/0.73 % (1835283)Termination phase: Saturation
% 1.87/0.73 % (1835283)Time elapsed: 0.082 s
% 1.87/0.73 % (1835283)Peak memory usage: 14 MB
% 1.87/0.73 % (1835283)Instructions burned: 161 (million)
% 1.87/0.73 % (1835294)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=1325730244:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.87/0.73 % TRYING [5]
% 1.87/0.73 % (1835297)ott-21_1_sil=16000:fs=off:random_seed=1222905394:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.87/0.73 % (1835293)Instruction limit reached!
% 1.87/0.73 % (1835293)------------------------------
% 1.87/0.73 % (1835293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.73 % (1835293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.73 % (1835293)CaDiCaL version: 2.1.3
% 1.87/0.73 % (1835293)Termination reason: Instruction limit
% 1.87/0.73 % (1835293)Termination phase: Saturation
% 1.87/0.73 % (1835293)Time elapsed: 0.084 s
% 1.87/0.73 % (1835293)Peak memory usage: 14 MB
% 1.87/0.73 % (1835293)Instructions burned: 132 (million)
% 1.87/0.73 % TRYING [6]
% 1.87/0.73 % (1835299)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=591219002:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.87/0.73 % (1835297)Instruction limit reached!
% 1.87/0.73 % (1835297)------------------------------
% 1.87/0.73 % (1835297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.73 % (1835297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.73 % (1835297)CaDiCaL version: 2.1.3
% 1.87/0.73 % (1835297)Termination reason: Instruction limit
% 1.87/0.73 % (1835297)Termination phase: Saturation
% 1.87/0.73 % (1835297)Time elapsed: 0.096 s
% 1.87/0.73 % (1835297)Peak memory usage: 14 MB
% 1.87/0.73 % (1835297)Instructions burned: 180 (million)
% 1.87/0.73 % (1835301)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4212883683:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.87/0.73 % TRYING [1]
% 1.87/0.73 % TRYING [2]
% 1.87/0.73 % TRYING [3]
% 1.87/0.73 % TRYING [6]
% 1.87/0.73 % TRYING [4]
% 1.87/0.73 % (1835291)Instruction limit reached!
% 1.87/0.73 % (1835291)------------------------------
% 1.87/0.73 % (1835291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.73 % (1835291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.73 % (1835291)CaDiCaL version: 2.1.3
% 1.87/0.73 % (1835291)Termination reason: Instruction limit
% 1.87/0.73 % (1835291)Termination phase: Finite model building SAT solving
% 1.87/0.73 % (1835291)Time elapsed: 0.207 s
% 1.87/0.73 % (1835291)Peak memory usage: 15 MB
% 1.87/0.73 % (1835291)Instructions burned: 716 (million)
% 1.87/0.73 % TRYING [5]
% 1.87/0.73 % (1835278) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1835272-1835278"...
% 1.87/0.73 % (1835303)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2088730348:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.87/0.73 % (1835278)...printing done.
% 1.87/0.73 % (1835278)Refutation found. Thanks to Tanya!
% 1.87/0.73 % SZS status Theorem for theBenchmark
% 1.87/0.73 % SZS output start Proof for theBenchmark
% See solution above
% 1.87/0.74 % (1835278)------------------------------
% 1.87/0.74 % (1835278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.87/0.74 % (1835278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.87/0.74 % (1835278)CaDiCaL version: 2.1.3
% 1.87/0.74 % (1835278)Termination reason: Refutation
% 1.87/0.74 % (1835278)Time elapsed: 0.276 s
% 1.87/0.74 % (1835278)Peak memory usage: 20 MB
% 1.87/0.74 % (1835278)Instructions burned: 466 (million)
% 1.87/0.74 % (1835272)Success in time 0.321 s
% 1.87/0.74 % Vampire exiting
%------------------------------------------------------------------------------