%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU288+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:10 PM UTC 2026
% Result : Theorem 24.89s 4.34s
% Output : Refutation 25.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 75
% Syntax : Number of formulae : 606 ( 68 unt; 68 def)
% Number of atoms : 2878 ( 257 equ)
% Maximal formula atoms : 25 ( 4 avg)
% Number of connectives : 3943 (1671 ~;1927 |; 223 &)
% ( 82 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 74 ( 72 usr; 68 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 3 con; 0-3 aty)
% Number of variables : 793 ( 0 sgn 703 !; 90 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(X6,X5)
=> in(ordered_pair(X3,X6),X1) ) )
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(X8,X7)
=> in(ordered_pair(X4,X8),X1) ) ) )
=> X3 = X4 )
& ! [X2] :
~ ( in(X2,X0)
& ! [X3] :
~ ? [X9] :
( X2 = X9
& in(X3,X9)
& ! [X10] :
( in(X10,X9)
=> in(ordered_pair(X3,X10),X1) ) ) ) )
=> ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = X0
& ! [X3] :
( in(X3,X0)
=> ? [X11] :
( X3 = X11
& in(apply(X2,X3),X11)
& ! [X12] :
( in(X12,X11)
=> in(ordered_pair(apply(X2,X3),X12),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_funct_1__e10_24__wellord2) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(X6,X5)
=> in(ordered_pair(X3,X6),X1) ) )
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(X8,X7)
=> in(ordered_pair(X4,X8),X1) ) ) )
=> X3 = X4 )
& ! [X2] :
~ ( in(X2,X0)
& ! [X3] :
~ ? [X9] :
( X2 = X9
& in(X3,X9)
& ! [X10] :
( in(X10,X9)
=> in(ordered_pair(X3,X10),X1) ) ) ) )
=> ? [X2] :
( relation(X2)
& function(X2)
& relation_dom(X2) = X0
& ! [X3] :
( in(X3,X0)
=> ? [X11] :
( X3 = X11
& in(apply(X2,X3),X11)
& ! [X12] :
( in(X12,X11)
=> in(ordered_pair(apply(X2,X3),X12),X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f21,axiom,
! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ( ! [X2,X3,X4] :
( ( in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(X6,X5)
=> in(ordered_pair(X3,X6),X1) ) )
& in(X2,X0)
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(X8,X7)
=> in(ordered_pair(X4,X8),X1) ) ) )
=> X3 = X4 )
=> ? [X2] :
( relation(X2)
& function(X2)
& ! [X3,X4] :
( in(ordered_pair(X3,X4),X2)
<=> ( in(X3,X0)
& in(X3,X0)
& ? [X9] :
( X3 = X9
& in(X4,X9)
& ! [X10] :
( in(X10,X9)
=> in(ordered_pair(X4,X10),X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_funct_1__e10_24__wellord2__1) ).
fof(f23,axiom,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(f24,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( ( in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) )
& ( ~ in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> X2 = empty_set ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f25,axiom,
! [X0] :
( relation(X0)
=> ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_relat_1) ).
fof(f26,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tarski) ).
fof(f46,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& empty(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f48,plain,
~ ! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ( ( ! [X2,X3,X4] :
( ( in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(X6,X5)
=> in(ordered_pair(X3,X6),X1) ) )
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(X8,X7)
=> in(ordered_pair(X4,X8),X1) ) ) )
=> X3 = X4 )
& ! [X9] :
~ ( in(X9,X0)
& ! [X10] :
~ ? [X11] :
( X9 = X11
& in(X10,X11)
& ! [X12] :
( in(X12,X11)
=> in(ordered_pair(X10,X12),X1) ) ) ) )
=> ? [X13] :
( relation(X13)
& function(X13)
& relation_dom(X13) = X0
& ! [X14] :
( in(X14,X0)
=> ? [X15] :
( X14 = X15
& in(apply(X13,X14),X15)
& ! [X16] :
( in(X16,X15)
=> in(ordered_pair(apply(X13,X14),X16),X1) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f49,plain,
! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ( ! [X2,X3,X4] :
( ( in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(X6,X5)
=> in(ordered_pair(X3,X6),X1) ) )
& in(X2,X0)
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(X8,X7)
=> in(ordered_pair(X4,X8),X1) ) ) )
=> X3 = X4 )
=> ? [X9] :
( relation(X9)
& function(X9)
& ! [X10,X11] :
( in(ordered_pair(X10,X11),X9)
<=> ( in(X10,X0)
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(X13,X12)
=> in(ordered_pair(X11,X13),X1) ) ) ) ) ) ) ),
inference(rectify,[],[f21]) ).
fof(f55,plain,
? [X0,X1] :
( ! [X13] :
( ~ relation(X13)
| ~ function(X13)
| relation_dom(X13) != X0
| ? [X14] :
( ! [X15] :
( X14 != X15
| ~ in(apply(X13,X14),X15)
| ? [X16] :
( ~ in(ordered_pair(apply(X13,X14),X16),X1)
& in(X16,X15) ) )
& in(X14,X0) ) )
& ! [X2,X3,X4] :
( X3 = X4
| ~ in(X2,X0)
| ! [X5] :
( X2 != X5
| ~ in(X3,X5)
| ? [X6] :
( ~ in(ordered_pair(X3,X6),X1)
& in(X6,X5) ) )
| ! [X7] :
( X2 != X7
| ~ in(X4,X7)
| ? [X8] :
( ~ in(ordered_pair(X4,X8),X1)
& in(X8,X7) ) ) )
& ! [X9] :
( ~ in(X9,X0)
| ? [X10,X11] :
( X9 = X11
& in(X10,X11)
& ! [X12] :
( in(ordered_pair(X10,X12),X1)
| ~ in(X12,X11) ) ) )
& ~ empty(X0)
& relation(X1) ),
inference(ennf_transformation,[],[f48]) ).
fof(f56,plain,
? [X0,X1] :
( ! [X13] :
( ~ relation(X13)
| ~ function(X13)
| relation_dom(X13) != X0
| ? [X14] :
( ! [X15] :
( X14 != X15
| ~ in(apply(X13,X14),X15)
| ? [X16] :
( ~ in(ordered_pair(apply(X13,X14),X16),X1)
& in(X16,X15) ) )
& in(X14,X0) ) )
& ! [X2,X3,X4] :
( X3 = X4
| ~ in(X2,X0)
| ! [X5] :
( X2 != X5
| ~ in(X3,X5)
| ? [X6] :
( ~ in(ordered_pair(X3,X6),X1)
& in(X6,X5) ) )
| ! [X7] :
( X2 != X7
| ~ in(X4,X7)
| ? [X8] :
( ~ in(ordered_pair(X4,X8),X1)
& in(X8,X7) ) ) )
& ! [X9] :
( ~ in(X9,X0)
| ? [X10,X11] :
( X9 = X11
& in(X10,X11)
& ! [X12] :
( in(ordered_pair(X10,X12),X1)
| ~ in(X12,X11) ) ) )
& ~ empty(X0)
& relation(X1) ),
inference(flattening,[],[f55]) ).
fof(f65,plain,
! [X0,X1] :
( ? [X9] :
( relation(X9)
& function(X9)
& ! [X10,X11] :
( in(ordered_pair(X10,X11),X9)
<=> ( in(X10,X0)
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(ordered_pair(X3,X6),X1)
| ~ in(X6,X5) ) )
& in(X2,X0)
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(ordered_pair(X4,X8),X1)
| ~ in(X8,X7) ) ) )
| empty(X0)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f66,plain,
! [X0,X1] :
( ? [X9] :
( relation(X9)
& function(X9)
& ! [X10,X11] :
( in(ordered_pair(X10,X11),X9)
<=> ( in(X10,X0)
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(ordered_pair(X3,X6),X1)
| ~ in(X6,X5) ) )
& in(X2,X0)
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(ordered_pair(X4,X8),X1)
| ~ in(X8,X7) ) ) )
| empty(X0)
| ~ relation(X1) ),
inference(flattening,[],[f65]) ).
fof(f68,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f69,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f68]) ).
fof(f70,plain,
! [X0] :
( ! [X1] :
( X1 = relation_dom(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] : in(ordered_pair(X2,X3),X0) ) )
| ~ relation(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f79,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f81,definition,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(ordered_pair(X3,X6),X1)
| ~ in(X6,X5) ) )
& in(X2,X0)
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(ordered_pair(X4,X8),X1)
| ~ in(X8,X7) ) ) )
| ~ sP0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f82,plain,
! [X0,X1] :
( ? [X9] :
( relation(X9)
& function(X9)
& ! [X10,X11] :
( in(ordered_pair(X10,X11),X9)
<=> ( in(X10,X0)
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) ) ) )
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(definition_folding,[],[f66,f81]) ).
fof(f83,plain,
? [X0,X1] :
( ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != X0
| ? [X3] :
( ! [X4] :
( X3 != X4
| ~ in(apply(X2,X3),X4)
| ? [X5] :
( ~ in(ordered_pair(apply(X2,X3),X5),X1)
& in(X5,X4) ) )
& in(X3,X0) ) )
& ! [X6,X7,X8] :
( X7 = X8
| ~ in(X6,X0)
| ! [X9] :
( X6 != X9
| ~ in(X7,X9)
| ? [X10] :
( ~ in(ordered_pair(X7,X10),X1)
& in(X10,X9) ) )
| ! [X11] :
( X6 != X11
| ~ in(X8,X11)
| ? [X12] :
( ~ in(ordered_pair(X8,X12),X1)
& in(X12,X11) ) ) )
& ! [X13] :
( ~ in(X13,X0)
| ? [X14,X15] :
( X13 = X15
& in(X14,X15)
& ! [X16] :
( in(ordered_pair(X14,X16),X1)
| ~ in(X16,X15) ) ) )
& ~ empty(X0)
& relation(X1) ),
inference(rectify,[],[f56]) ).
fof(f84,plain,
( ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| ( ! [X4] :
( sK3(X2) != X4
| ~ in(apply(X2,sK3(X2)),X4)
| ( ~ in(ordered_pair(apply(X2,sK3(X2)),sK4(X2,X4)),sK2)
& in(sK4(X2,X4),X4) ) )
& in(sK3(X2),sK1) ) )
& ! [X6,X7,X8] :
( X7 = X8
| ~ in(X6,sK1)
| ! [X9] :
( X6 != X9
| ~ in(X7,X9)
| ( ~ in(ordered_pair(X7,sK5(X7,X9)),sK2)
& in(sK5(X7,X9),X9) ) )
| ! [X11] :
( X6 != X11
| ~ in(X8,X11)
| ( ~ in(ordered_pair(X8,sK6(X8,X11)),sK2)
& in(sK6(X8,X11),X11) ) ) )
& ! [X13] :
( ~ in(X13,sK1)
| ( sK8(X13) = X13
& in(sK7(X13),sK8(X13))
& ! [X16] :
( in(ordered_pair(sK7(X13),X16),sK2)
| ~ in(X16,sK8(X13)) ) ) )
& ~ empty(sK1)
& relation(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X3,sK3(X2)),skolemize(X5,sK4(X2,X4)),skolemize(X10,sK5(X7,X9)),skolemize(X12,sK6(X8,X11)),skolemize(X14,sK7(X13)),skolemize(X15,sK8(X13))],[f83]) ).
fof(f93,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& in(X2,X0)
& ? [X5] :
( X2 = X5
& in(X3,X5)
& ! [X6] :
( in(ordered_pair(X3,X6),X1)
| ~ in(X6,X5) ) )
& in(X2,X0)
& ? [X7] :
( X2 = X7
& in(X4,X7)
& ! [X8] :
( in(ordered_pair(X4,X8),X1)
| ~ in(X8,X7) ) ) )
| ~ sP0(X0,X1) ),
inference(nnf_transformation,[],[f81]) ).
fof(f94,plain,
! [X0,X1] :
( ( sK18(X0,X1) != sK19(X0,X1)
& in(sK17(X0,X1),X0)
& sK17(X0,X1) = sK20(X0,X1)
& in(sK18(X0,X1),sK20(X0,X1))
& ! [X6] :
( in(ordered_pair(sK18(X0,X1),X6),X1)
| ~ in(X6,sK20(X0,X1)) )
& in(sK17(X0,X1),X0)
& sK17(X0,X1) = sK21(X0,X1)
& in(sK19(X0,X1),sK21(X0,X1))
& ! [X8] :
( in(ordered_pair(sK19(X0,X1),X8),X1)
| ~ in(X8,sK21(X0,X1)) ) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19,sK20,sK21]),skolemize(X2,sK17(X0,X1)),skolemize(X3,sK18(X0,X1)),skolemize(X4,sK19(X0,X1)),skolemize(X5,sK20(X0,X1)),skolemize(X7,sK21(X0,X1))],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( ? [X9] :
( relation(X9)
& function(X9)
& ! [X10,X11] :
( ( in(ordered_pair(X10,X11),X9)
| ~ in(X10,X0)
| ~ in(X10,X0)
| ! [X12] :
( X10 != X12
| ~ in(X11,X12)
| ? [X13] :
( ~ in(ordered_pair(X11,X13),X1)
& in(X13,X12) ) ) )
& ( ( in(X10,X0)
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) )
| ~ in(ordered_pair(X10,X11),X9) ) ) )
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(nnf_transformation,[],[f82]) ).
fof(f96,plain,
! [X0,X1] :
( ? [X9] :
( relation(X9)
& function(X9)
& ! [X10,X11] :
( ( in(ordered_pair(X10,X11),X9)
| ~ in(X10,X0)
| ~ in(X10,X0)
| ! [X12] :
( X10 != X12
| ~ in(X11,X12)
| ? [X13] :
( ~ in(ordered_pair(X11,X13),X1)
& in(X13,X12) ) ) )
& ( ( in(X10,X0)
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) )
| ~ in(ordered_pair(X10,X11),X9) ) ) )
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(flattening,[],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( ? [X2] :
( relation(X2)
& function(X2)
& ! [X3,X4] :
( ( in(ordered_pair(X3,X4),X2)
| ~ in(X3,X0)
| ~ in(X3,X0)
| ! [X5] :
( X3 != X5
| ~ in(X4,X5)
| ? [X6] :
( ~ in(ordered_pair(X4,X6),X1)
& in(X6,X5) ) ) )
& ( ( in(X3,X0)
& in(X3,X0)
& ? [X7] :
( X3 = X7
& in(X4,X7)
& ! [X8] :
( in(ordered_pair(X4,X8),X1)
| ~ in(X8,X7) ) ) )
| ~ in(ordered_pair(X3,X4),X2) ) ) )
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(rectify,[],[f96]) ).
fof(f98,plain,
! [X0,X1] :
( ( relation(sK22(X0,X1))
& function(sK22(X0,X1))
& ! [X3,X4] :
( ( in(ordered_pair(X3,X4),sK22(X0,X1))
| ~ in(X3,X0)
| ~ in(X3,X0)
| ! [X5] :
( X3 != X5
| ~ in(X4,X5)
| ( ~ in(ordered_pair(X4,sK23(X1,X4,X5)),X1)
& in(sK23(X1,X4,X5),X5) ) ) )
& ( ( in(X3,X0)
& in(X3,X0)
& sK24(X1,X3,X4) = X3
& in(X4,sK24(X1,X3,X4))
& ! [X8] :
( in(ordered_pair(X4,X8),X1)
| ~ in(X8,sK24(X1,X3,X4)) ) )
| ~ in(ordered_pair(X3,X4),sK22(X0,X1)) ) ) )
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24]),skolemize(X2,sK22(X0,X1)),skolemize(X6,sK23(X1,X4,X5)),skolemize(X7,sK24(X1,X3,X4))],[f97]) ).
fof(f99,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = apply(X0,X1)
| ~ in(ordered_pair(X1,X2),X0) )
& ( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2 ) )
| ~ in(X1,relation_dom(X0)) )
& ( ( ( X2 = apply(X0,X1)
| empty_set != X2 )
& ( X2 = empty_set
| apply(X0,X1) != X2 ) )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f69]) ).
fof(f100,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| ! [X3] : ~ in(ordered_pair(X2,X3),X0) )
& ( ? [X3] : in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(nnf_transformation,[],[f70]) ).
fof(f101,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ? [X2] :
( ( ! [X3] : ~ in(ordered_pair(X2,X3),X0)
| ~ in(X2,X1) )
& ( ? [X4] : in(ordered_pair(X2,X4),X0)
| in(X2,X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( ? [X7] : in(ordered_pair(X5,X7),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(rectify,[],[f100]) ).
fof(f102,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_dom(X0)
| ( ( ! [X3] : ~ in(ordered_pair(sK25(X0,X1),X3),X0)
| ~ in(sK25(X0,X1),X1) )
& ( in(ordered_pair(sK25(X0,X1),sK26(X0,X1)),X0)
| in(sK25(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] : ~ in(ordered_pair(X5,X6),X0) )
& ( in(ordered_pair(X5,sK27(X0,X5)),X0)
| ~ in(X5,X1) ) )
| relation_dom(X0) != X1 ) )
| ~ relation(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26,sK27]),skolemize(X2,sK25(X0,X1)),skolemize(X4,sK26(X0,X1)),skolemize(X7,sK27(X0,X5))],[f101]) ).
fof(f109,plain,
relation(sK2),
inference(cnf_transformation,[],[f84]) ).
fof(f110,plain,
~ empty(sK1),
inference(cnf_transformation,[],[f84]) ).
fof(f111,plain,
! [X16,X13] :
( ~ in(X13,sK1)
| in(ordered_pair(sK7(X13),X16),sK2)
| ~ in(X16,sK8(X13)) ),
inference(cnf_transformation,[],[f84]) ).
fof(f112,plain,
! [X13] :
( ~ in(X13,sK1)
| in(sK7(X13),sK8(X13)) ),
inference(cnf_transformation,[],[f84]) ).
fof(f113,plain,
! [X13] :
( ~ in(X13,sK1)
| sK8(X13) = X13 ),
inference(cnf_transformation,[],[f84]) ).
fof(f114,plain,
! [X11,X8,X6,X9,X7] :
( X7 = X8
| ~ in(X6,sK1)
| X6 != X9
| ~ in(X7,X9)
| in(sK5(X7,X9),X9)
| X6 != X11
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(cnf_transformation,[],[f84]) ).
fof(f115,plain,
! [X11,X8,X6,X9,X7] :
( X7 = X8
| ~ in(X6,sK1)
| X6 != X9
| ~ in(X7,X9)
| in(sK5(X7,X9),X9)
| X6 != X11
| ~ in(X8,X11)
| ~ in(ordered_pair(X8,sK6(X8,X11)),sK2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f116,plain,
! [X11,X8,X6,X9,X7] :
( X7 = X8
| ~ in(X6,sK1)
| X6 != X9
| ~ in(X7,X9)
| ~ in(ordered_pair(X7,sK5(X7,X9)),sK2)
| X6 != X11
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(cnf_transformation,[],[f84]) ).
fof(f117,plain,
! [X11,X8,X6,X9,X7] :
( X7 = X8
| ~ in(X6,sK1)
| X6 != X9
| ~ in(X7,X9)
| ~ in(ordered_pair(X7,sK5(X7,X9)),sK2)
| X6 != X11
| ~ in(X8,X11)
| ~ in(ordered_pair(X8,sK6(X8,X11)),sK2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f118,plain,
! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| in(sK3(X2),sK1) ),
inference(cnf_transformation,[],[f84]) ).
fof(f119,plain,
! [X2,X4] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| sK3(X2) != X4
| ~ in(apply(X2,sK3(X2)),X4)
| in(sK4(X2,X4),X4) ),
inference(cnf_transformation,[],[f84]) ).
fof(f120,plain,
! [X2,X4] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| sK3(X2) != X4
| ~ in(apply(X2,sK3(X2)),X4)
| ~ in(ordered_pair(apply(X2,sK3(X2)),sK4(X2,X4)),sK2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f154,plain,
! [X0,X1,X8] :
( in(ordered_pair(sK19(X0,X1),X8),X1)
| ~ in(X8,sK21(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f155,plain,
! [X0,X1] :
( in(sK19(X0,X1),sK21(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f156,plain,
! [X0,X1] :
( sK17(X0,X1) = sK21(X0,X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f158,plain,
! [X0,X1,X6] :
( in(ordered_pair(sK18(X0,X1),X6),X1)
| ~ in(X6,sK20(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f159,plain,
! [X0,X1] :
( in(sK18(X0,X1),sK20(X0,X1))
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f160,plain,
! [X0,X1] :
( sK17(X0,X1) = sK20(X0,X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f161,plain,
! [X0,X1] :
( in(sK17(X0,X1),X0)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f162,plain,
! [X0,X1] :
( sK18(X0,X1) != sK19(X0,X1)
| ~ sP0(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f164,plain,
! [X3,X0,X1,X4] :
( in(X4,sK24(X1,X3,X4))
| ~ in(ordered_pair(X3,X4),sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f165,plain,
! [X3,X0,X1,X4] :
( sK24(X1,X3,X4) = X3
| ~ in(ordered_pair(X3,X4),sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f166,plain,
! [X3,X0,X1,X4] :
( in(X3,X0)
| ~ in(ordered_pair(X3,X4),sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f168,plain,
! [X3,X0,X1,X4,X5] :
( in(ordered_pair(X3,X4),sK22(X0,X1))
| ~ in(X3,X0)
| ~ in(X3,X0)
| X3 != X5
| ~ in(X4,X5)
| in(sK23(X1,X4,X5),X5)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f169,plain,
! [X3,X0,X1,X4,X5] :
( in(ordered_pair(X3,X4),sK22(X0,X1))
| ~ in(X3,X0)
| ~ in(X3,X0)
| X3 != X5
| ~ in(X4,X5)
| ~ in(ordered_pair(X4,sK23(X1,X4,X5)),X1)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f170,plain,
! [X0,X1] :
( function(sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f171,plain,
! [X0,X1] :
( relation(sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f173,plain,
! [X0,X1] : unordered_pair(X0,X1) = unordered_pair(X1,X0),
inference(cnf_transformation,[],[f23]) ).
fof(f176,plain,
! [X2,X0,X1] :
( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f177,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| ~ in(ordered_pair(X1,X2),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f178,plain,
! [X0,X1,X5] :
( in(ordered_pair(X5,sK27(X0,X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f179,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(ordered_pair(X5,X6),X0)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f180,plain,
! [X0,X1] :
( relation_dom(X0) = X1
| in(ordered_pair(sK25(X0,X1),sK26(X0,X1)),X0)
| in(sK25(X0,X1),X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f181,plain,
! [X3,X0,X1] :
( relation_dom(X0) = X1
| ~ in(ordered_pair(sK25(X0,X1),X3),X0)
| ~ in(sK25(X0,X1),X1)
| ~ relation(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f182,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f26]) ).
fof(f204,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f206,plain,
! [X2,X4] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| sK3(X2) != X4
| ~ in(apply(X2,sK3(X2)),X4)
| ~ in(unordered_pair(unordered_pair(apply(X2,sK3(X2)),sK4(X2,X4)),singleton(apply(X2,sK3(X2)))),sK2) ),
inference(definition_unfolding,[],[f120,f182]) ).
fof(f207,plain,
! [X11,X8,X6,X9,X7] :
( X7 = X8
| ~ in(X6,sK1)
| X6 != X9
| ~ in(X7,X9)
| ~ in(unordered_pair(unordered_pair(X7,sK5(X7,X9)),singleton(X7)),sK2)
| X6 != X11
| ~ in(X8,X11)
| ~ in(unordered_pair(unordered_pair(X8,sK6(X8,X11)),singleton(X8)),sK2) ),
inference(definition_unfolding,[],[f117,f182,f182]) ).
fof(f208,plain,
! [X11,X8,X6,X9,X7] :
( X7 = X8
| ~ in(X6,sK1)
| X6 != X9
| ~ in(X7,X9)
| ~ in(unordered_pair(unordered_pair(X7,sK5(X7,X9)),singleton(X7)),sK2)
| X6 != X11
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(definition_unfolding,[],[f116,f182]) ).
fof(f209,plain,
! [X11,X8,X6,X9,X7] :
( X7 = X8
| ~ in(X6,sK1)
| X6 != X9
| ~ in(X7,X9)
| in(sK5(X7,X9),X9)
| X6 != X11
| ~ in(X8,X11)
| ~ in(unordered_pair(unordered_pair(X8,sK6(X8,X11)),singleton(X8)),sK2) ),
inference(definition_unfolding,[],[f115,f182]) ).
fof(f210,plain,
! [X16,X13] :
( ~ in(X13,sK1)
| in(unordered_pair(unordered_pair(sK7(X13),X16),singleton(sK7(X13))),sK2)
| ~ in(X16,sK8(X13)) ),
inference(definition_unfolding,[],[f111,f182]) ).
fof(f212,plain,
! [X0,X1,X6] :
( in(unordered_pair(unordered_pair(sK18(X0,X1),X6),singleton(sK18(X0,X1))),X1)
| ~ in(X6,sK20(X0,X1))
| ~ sP0(X0,X1) ),
inference(definition_unfolding,[],[f158,f182]) ).
fof(f213,plain,
! [X0,X1,X8] :
( in(unordered_pair(unordered_pair(sK19(X0,X1),X8),singleton(sK19(X0,X1))),X1)
| ~ in(X8,sK21(X0,X1))
| ~ sP0(X0,X1) ),
inference(definition_unfolding,[],[f154,f182]) ).
fof(f214,plain,
! [X3,X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK22(X0,X1))
| ~ in(X3,X0)
| ~ in(X3,X0)
| X3 != X5
| ~ in(X4,X5)
| ~ in(unordered_pair(unordered_pair(X4,sK23(X1,X4,X5)),singleton(X4)),X1)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(definition_unfolding,[],[f169,f182,f182]) ).
fof(f215,plain,
! [X3,X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK22(X0,X1))
| ~ in(X3,X0)
| ~ in(X3,X0)
| X3 != X5
| ~ in(X4,X5)
| in(sK23(X1,X4,X5),X5)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(definition_unfolding,[],[f168,f182]) ).
fof(f217,plain,
! [X3,X0,X1,X4] :
( in(X3,X0)
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(definition_unfolding,[],[f166,f182]) ).
fof(f218,plain,
! [X3,X0,X1,X4] :
( sK24(X1,X3,X4) = X3
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(definition_unfolding,[],[f165,f182]) ).
fof(f219,plain,
! [X3,X0,X1,X4] :
( in(X4,sK24(X1,X3,X4))
| ~ in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),sK22(X0,X1))
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(definition_unfolding,[],[f164,f182]) ).
fof(f221,plain,
! [X2,X0,X1] :
( apply(X0,X1) = X2
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(definition_unfolding,[],[f177,f182]) ).
fof(f222,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X0)
| apply(X0,X1) != X2
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(definition_unfolding,[],[f176,f182]) ).
fof(f223,plain,
! [X3,X0,X1] :
( relation_dom(X0) = X1
| ~ in(unordered_pair(unordered_pair(sK25(X0,X1),X3),singleton(sK25(X0,X1))),X0)
| ~ in(sK25(X0,X1),X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f181,f182]) ).
fof(f224,plain,
! [X0,X1] :
( relation_dom(X0) = X1
| in(unordered_pair(unordered_pair(sK25(X0,X1),sK26(X0,X1)),singleton(sK25(X0,X1))),X0)
| in(sK25(X0,X1),X1)
| ~ relation(X0) ),
inference(definition_unfolding,[],[f180,f182]) ).
fof(f225,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(unordered_pair(unordered_pair(X5,X6),singleton(X5)),X0)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(definition_unfolding,[],[f179,f182]) ).
fof(f226,plain,
! [X0,X1,X5] :
( in(unordered_pair(unordered_pair(X5,sK27(X0,X5)),singleton(X5)),X0)
| ~ in(X5,X1)
| relation_dom(X0) != X1
| ~ relation(X0) ),
inference(definition_unfolding,[],[f178,f182]) ).
fof(f227,plain,
! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| ~ in(apply(X2,sK3(X2)),sK3(X2))
| ~ in(unordered_pair(unordered_pair(apply(X2,sK3(X2)),sK4(X2,sK3(X2))),singleton(apply(X2,sK3(X2)))),sK2) ),
inference(equality_resolution,[],[f206]) ).
fof(f228,plain,
! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| ~ in(apply(X2,sK3(X2)),sK3(X2))
| in(sK4(X2,sK3(X2)),sK3(X2)) ),
inference(equality_resolution,[],[f119]) ).
fof(f229,plain,
! [X11,X8,X9,X7] :
( X7 = X8
| ~ in(X9,sK1)
| ~ in(X7,X9)
| ~ in(unordered_pair(unordered_pair(X7,sK5(X7,X9)),singleton(X7)),sK2)
| X9 != X11
| ~ in(X8,X11)
| ~ in(unordered_pair(unordered_pair(X8,sK6(X8,X11)),singleton(X8)),sK2) ),
inference(equality_resolution,[],[f207]) ).
fof(f230,plain,
! [X11,X8,X7] :
( X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(unordered_pair(unordered_pair(X7,sK5(X7,X11)),singleton(X7)),sK2)
| ~ in(X8,X11)
| ~ in(unordered_pair(unordered_pair(X8,sK6(X8,X11)),singleton(X8)),sK2) ),
inference(equality_resolution,[],[f229]) ).
fof(f231,plain,
! [X11,X8,X9,X7] :
( X7 = X8
| ~ in(X9,sK1)
| ~ in(X7,X9)
| ~ in(unordered_pair(unordered_pair(X7,sK5(X7,X9)),singleton(X7)),sK2)
| X9 != X11
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(equality_resolution,[],[f208]) ).
fof(f232,plain,
! [X11,X8,X7] :
( X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(unordered_pair(unordered_pair(X7,sK5(X7,X11)),singleton(X7)),sK2)
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(equality_resolution,[],[f231]) ).
fof(f233,plain,
! [X11,X8,X9,X7] :
( X7 = X8
| ~ in(X9,sK1)
| ~ in(X7,X9)
| in(sK5(X7,X9),X9)
| X9 != X11
| ~ in(X8,X11)
| ~ in(unordered_pair(unordered_pair(X8,sK6(X8,X11)),singleton(X8)),sK2) ),
inference(equality_resolution,[],[f209]) ).
fof(f234,plain,
! [X11,X8,X7] :
( X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| in(sK5(X7,X11),X11)
| ~ in(X8,X11)
| ~ in(unordered_pair(unordered_pair(X8,sK6(X8,X11)),singleton(X8)),sK2) ),
inference(equality_resolution,[],[f233]) ).
fof(f235,plain,
! [X11,X8,X9,X7] :
( X7 = X8
| ~ in(X9,sK1)
| ~ in(X7,X9)
| in(sK5(X7,X9),X9)
| X9 != X11
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(equality_resolution,[],[f114]) ).
fof(f236,plain,
! [X11,X8,X7] :
( X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| in(sK5(X7,X11),X11)
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(equality_resolution,[],[f235]) ).
fof(f237,plain,
! [X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),sK22(X0,X1))
| ~ in(X5,X0)
| ~ in(X5,X0)
| ~ in(X4,X5)
| ~ in(unordered_pair(unordered_pair(X4,sK23(X1,X4,X5)),singleton(X4)),X1)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(equality_resolution,[],[f214]) ).
fof(f238,plain,
! [X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),sK22(X0,X1))
| ~ in(X5,X0)
| ~ in(X5,X0)
| ~ in(X4,X5)
| in(sK23(X1,X4,X5),X5)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(equality_resolution,[],[f215]) ).
fof(f239,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X1,apply(X0,X1)),singleton(X1)),X0)
| ~ in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f222]) ).
fof(f242,plain,
! [X0,X6,X5] :
( in(X5,relation_dom(X0))
| ~ in(unordered_pair(unordered_pair(X5,X6),singleton(X5)),X0)
| ~ relation(X0) ),
inference(equality_resolution,[],[f225]) ).
fof(f243,plain,
! [X0,X5] :
( in(unordered_pair(unordered_pair(X5,sK27(X0,X5)),singleton(X5)),X0)
| ~ in(X5,relation_dom(X0))
| ~ relation(X0) ),
inference(equality_resolution,[],[f226]) ).
fof(f246,plain,
! [X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),sK22(X0,X1))
| ~ in(X5,X0)
| ~ in(X4,X5)
| ~ in(unordered_pair(unordered_pair(X4,sK23(X1,X4,X5)),singleton(X4)),X1)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(duplicate_literal_removal,[],[f237]) ).
fof(f247,plain,
! [X0,X1,X4,X5] :
( in(unordered_pair(unordered_pair(X5,X4),singleton(X5)),sK22(X0,X1))
| ~ in(X5,X0)
| ~ in(X4,X5)
| in(sK23(X1,X4,X5),X5)
| sP0(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(duplicate_literal_removal,[],[f238]) ).
fof(f248,plain,
! [X16,X13] :
( in(unordered_pair(singleton(sK7(X13)),unordered_pair(sK7(X13),X16)),sK2)
| ~ in(X13,sK1)
| ~ in(X16,sK8(X13)) ),
inference(forward_demodulation,[],[f210,f173]) ).
fof(f249,plain,
! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X8),unordered_pair(X8,sK6(X8,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| in(sK5(X7,X11),X11)
| ~ in(X8,X11) ),
inference(forward_demodulation,[],[f234,f173]) ).
fof(f250,plain,
! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X7),unordered_pair(X7,sK5(X7,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ),
inference(forward_demodulation,[],[f232,f173]) ).
fof(f251,plain,
! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X7),unordered_pair(X7,sK5(X7,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(X8,X11)
| ~ in(unordered_pair(unordered_pair(X8,sK6(X8,X11)),singleton(X8)),sK2) ),
inference(forward_demodulation,[],[f230,f173]) ).
fof(f252,plain,
! [X2] :
( ~ in(unordered_pair(singleton(apply(X2,sK3(X2))),unordered_pair(apply(X2,sK3(X2)),sK4(X2,sK3(X2)))),sK2)
| ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| ~ in(apply(X2,sK3(X2)),sK3(X2)) ),
inference(forward_demodulation,[],[f227,f173]) ).
fof(f253,plain,
! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X8),unordered_pair(X8,sK6(X8,X11))),sK2)
| ~ in(unordered_pair(singleton(X7),unordered_pair(X7,sK5(X7,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(X8,X11) ),
inference(forward_demodulation,[],[f251,f173]) ).
fof(f255,definition,
( spl34_1
<=> relation(sK2) ),
introduced(definition,[new_symbols(definition,[spl34_1])],[avatar_definition]) ).
fof(f257,plain,
( relation(sK2)
| ~ spl34_1 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f258,plain,
spl34_1,
inference(avatar_split_clause,[],[f109,f255]) ).
fof(f259,plain,
( ! [X0] :
( function(sK22(X0,sK2))
| sP0(X0,sK2)
| empty(X0) )
| ~ spl34_1 ),
inference(resolution,[],[f257,f170]) ).
fof(f260,plain,
( ! [X0] :
( relation(sK22(X0,sK2))
| sP0(X0,sK2)
| empty(X0) )
| ~ spl34_1 ),
inference(resolution,[],[f257,f171]) ).
fof(f263,plain,
( ! [X2,X0,X1] :
( in(X0,X1)
| ~ in(unordered_pair(unordered_pair(X0,X2),singleton(X0)),sK22(X1,sK2))
| sP0(X1,sK2)
| empty(X1) )
| ~ spl34_1 ),
inference(resolution,[],[f257,f217]) ).
fof(f276,plain,
( ! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK22(X2,sK2))
| ~ in(X0,X2)
| ~ in(X1,X0)
| in(sK23(sK2,X1,X0),X0)
| sP0(X2,sK2)
| empty(X2) )
| ~ spl34_1 ),
inference(resolution,[],[f257,f247]) ).
fof(f277,plain,
( ! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK22(X2,sK2))
| ~ in(X0,X2)
| ~ in(X1,X0)
| in(sK23(sK2,X1,X0),X0)
| sP0(X2,sK2) )
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f276,f204]) ).
fof(f288,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK22(X1,sK2))
| in(X0,X1)
| sP0(X1,sK2)
| empty(X1) )
| ~ spl34_1 ),
inference(forward_demodulation,[],[f263,f173]) ).
fof(f290,plain,
( ! [X2,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(X2,sK2))
| ~ in(X0,X2)
| ~ in(X1,X0)
| in(sK23(sK2,X1,X0),X0)
| sP0(X2,sK2) )
| ~ spl34_1 ),
inference(forward_demodulation,[],[f277,f173]) ).
fof(f295,definition,
( spl34_2
<=> empty(sK1) ),
introduced(definition,[new_symbols(definition,[spl34_2])],[avatar_definition]) ).
fof(f297,plain,
( ~ empty(sK1)
| spl34_2 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,plain,
~ spl34_2,
inference(avatar_split_clause,[],[f110,f295]) ).
fof(f305,plain,
( ! [X2,X0,X1] :
( sK24(X0,X1,X2) = X1
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),sK22(sK1,X0))
| sP0(sK1,X0)
| ~ relation(X0) )
| spl34_2 ),
inference(resolution,[],[f297,f218]) ).
fof(f306,plain,
( ! [X2,X0,X1] :
( in(X0,sK24(X1,X2,X0))
| ~ in(unordered_pair(unordered_pair(X2,X0),singleton(X2)),sK22(sK1,X1))
| sP0(sK1,X1)
| ~ relation(X1) )
| spl34_2 ),
inference(resolution,[],[f297,f219]) ).
fof(f308,plain,
( ! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK22(sK1,X2))
| ~ in(X0,sK1)
| ~ in(X1,X0)
| ~ in(unordered_pair(unordered_pair(X1,sK23(X2,X1,X0)),singleton(X1)),X2)
| sP0(sK1,X2)
| ~ relation(X2) )
| spl34_2 ),
inference(resolution,[],[f297,f246]) ).
fof(f311,plain,
( ! [X2,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(sK1,X2))
| ~ in(X0,sK1)
| ~ in(X1,X0)
| ~ in(unordered_pair(unordered_pair(X1,sK23(X2,X1,X0)),singleton(X1)),X2)
| sP0(sK1,X2)
| ~ relation(X2) )
| spl34_2 ),
inference(forward_demodulation,[],[f308,f173]) ).
fof(f313,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X2),unordered_pair(X2,X0)),sK22(sK1,X1))
| in(X0,sK24(X1,X2,X0))
| sP0(sK1,X1)
| ~ relation(X1) )
| spl34_2 ),
inference(forward_demodulation,[],[f306,f173]) ).
fof(f314,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),sK22(sK1,X0))
| sK24(X0,X1,X2) = X1
| sP0(sK1,X0)
| ~ relation(X0) )
| spl34_2 ),
inference(forward_demodulation,[],[f305,f173]) ).
fof(f317,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK23(X2,X1,X0))),X2)
| in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(sK1,X2))
| ~ in(X0,sK1)
| ~ in(X1,X0)
| sP0(sK1,X2)
| ~ relation(X2) )
| spl34_2 ),
inference(forward_demodulation,[],[f311,f173]) ).
fof(f319,definition,
( spl34_3
<=> ! [X13] :
( ~ in(X13,sK1)
| sK8(X13) = X13 ) ),
introduced(definition,[new_symbols(definition,[spl34_3])],[avatar_definition]) ).
fof(f320,plain,
( ! [X13] :
( sK8(X13) = X13
| ~ in(X13,sK1) )
| ~ spl34_3 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
spl34_3,
inference(avatar_split_clause,[],[f113,f319]) ).
fof(f323,definition,
( spl34_4
<=> ! [X13] :
( ~ in(X13,sK1)
| in(sK7(X13),sK8(X13)) ) ),
introduced(definition,[new_symbols(definition,[spl34_4])],[avatar_definition]) ).
fof(f324,plain,
( ! [X13] :
( in(sK7(X13),sK8(X13))
| ~ in(X13,sK1) )
| ~ spl34_4 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f325,plain,
spl34_4,
inference(avatar_split_clause,[],[f112,f323]) ).
fof(f327,definition,
( spl34_5
<=> ! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X8),unordered_pair(X8,sK6(X8,X11))),sK2)
| ~ in(unordered_pair(singleton(X7),unordered_pair(X7,sK5(X7,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(X8,X11) ) ),
introduced(definition,[new_symbols(definition,[spl34_5])],[avatar_definition]) ).
fof(f328,plain,
( ! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X8),unordered_pair(X8,sK6(X8,X11))),sK2)
| ~ in(unordered_pair(singleton(X7),unordered_pair(X7,sK5(X7,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(X8,X11) )
| ~ spl34_5 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f329,plain,
spl34_5,
inference(avatar_split_clause,[],[f253,f327]) ).
fof(f339,definition,
( spl34_6
<=> ! [X13,X16] :
( in(unordered_pair(singleton(sK7(X13)),unordered_pair(sK7(X13),X16)),sK2)
| ~ in(X13,sK1)
| ~ in(X16,sK8(X13)) ) ),
introduced(definition,[new_symbols(definition,[spl34_6])],[avatar_definition]) ).
fof(f340,plain,
( ! [X16,X13] :
( in(unordered_pair(singleton(sK7(X13)),unordered_pair(sK7(X13),X16)),sK2)
| ~ in(X13,sK1)
| ~ in(X16,sK8(X13)) )
| ~ spl34_6 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f341,plain,
spl34_6,
inference(avatar_split_clause,[],[f248,f339]) ).
fof(f364,definition,
( spl34_7
<=> ! [X2] :
( ~ in(unordered_pair(singleton(apply(X2,sK3(X2))),unordered_pair(apply(X2,sK3(X2)),sK4(X2,sK3(X2)))),sK2)
| ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| ~ in(apply(X2,sK3(X2)),sK3(X2)) ) ),
introduced(definition,[new_symbols(definition,[spl34_7])],[avatar_definition]) ).
fof(f365,plain,
( ! [X2] :
( relation_dom(X2) != sK1
| ~ relation(X2)
| ~ function(X2)
| ~ in(unordered_pair(singleton(apply(X2,sK3(X2))),unordered_pair(apply(X2,sK3(X2)),sK4(X2,sK3(X2)))),sK2)
| ~ in(apply(X2,sK3(X2)),sK3(X2)) )
| ~ spl34_7 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f366,plain,
spl34_7,
inference(avatar_split_clause,[],[f252,f364]) ).
fof(f374,definition,
( spl34_8
<=> ! [X11,X7,X8] :
( ~ in(unordered_pair(singleton(X7),unordered_pair(X7,sK5(X7,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ) ),
introduced(definition,[new_symbols(definition,[spl34_8])],[avatar_definition]) ).
fof(f375,plain,
( ! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X7),unordered_pair(X7,sK5(X7,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) )
| ~ spl34_8 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f376,plain,
spl34_8,
inference(avatar_split_clause,[],[f250,f374]) ).
fof(f384,definition,
( spl34_9
<=> ! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X8),unordered_pair(X8,sK6(X8,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| in(sK5(X7,X11),X11)
| ~ in(X8,X11) ) ),
introduced(definition,[new_symbols(definition,[spl34_9])],[avatar_definition]) ).
fof(f385,plain,
( ! [X11,X8,X7] :
( ~ in(unordered_pair(singleton(X8),unordered_pair(X8,sK6(X8,X11))),sK2)
| X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| in(sK5(X7,X11),X11)
| ~ in(X8,X11) )
| ~ spl34_9 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f386,plain,
spl34_9,
inference(avatar_split_clause,[],[f249,f384]) ).
fof(f401,plain,
( ! [X0] :
( in(sK7(X0),X0)
| ~ in(X0,sK1)
| ~ in(X0,sK1) )
| ~ spl34_3
| ~ spl34_4 ),
inference(superposition,[],[f324,f320]) ).
fof(f402,plain,
( ! [X0] :
( in(sK7(X0),X0)
| ~ in(X0,sK1) )
| ~ spl34_3
| ~ spl34_4 ),
inference(duplicate_literal_removal,[],[f401]) ).
fof(f416,definition,
( spl34_10
<=> ! [X0] :
( in(sK7(X0),X0)
| ~ in(X0,sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_10])],[avatar_definition]) ).
fof(f417,plain,
( ! [X0] :
( in(sK7(X0),X0)
| ~ in(X0,sK1) )
| ~ spl34_10 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f418,plain,
( spl34_10
| ~ spl34_3
| ~ spl34_4 ),
inference(avatar_split_clause,[],[f402,f323,f319,f416]) ).
fof(f450,definition,
( spl34_11
<=> ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| ~ in(apply(X2,sK3(X2)),sK3(X2))
| in(sK4(X2,sK3(X2)),sK3(X2)) ) ),
introduced(definition,[new_symbols(definition,[spl34_11])],[avatar_definition]) ).
fof(f451,plain,
( ! [X2] :
( relation_dom(X2) != sK1
| ~ function(X2)
| ~ relation(X2)
| ~ in(apply(X2,sK3(X2)),sK3(X2))
| in(sK4(X2,sK3(X2)),sK3(X2)) )
| ~ spl34_11 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f452,plain,
spl34_11,
inference(avatar_split_clause,[],[f228,f450]) ).
fof(f454,plain,
( ! [X2,X0,X1] :
( sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| ~ in(apply(X1,sK3(X1)),sK3(X1))
| in(sK4(X1,sK3(X1)),sK3(X1))
| ~ in(unordered_pair(unordered_pair(sK25(X1,X0),X2),singleton(sK25(X1,X0))),X1)
| ~ in(sK25(X1,X0),X0)
| ~ relation(X1) )
| ~ spl34_11 ),
inference(superposition,[],[f451,f223]) ).
fof(f455,plain,
( ! [X2,X0,X1] :
( sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| ~ in(apply(X1,sK3(X1)),sK3(X1))
| in(sK4(X1,sK3(X1)),sK3(X1))
| ~ in(unordered_pair(unordered_pair(sK25(X1,X0),X2),singleton(sK25(X1,X0))),X1)
| ~ in(sK25(X1,X0),X0) )
| ~ spl34_11 ),
inference(duplicate_literal_removal,[],[f454]) ).
fof(f457,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(sK25(X1,X0)),unordered_pair(sK25(X1,X0),X2)),X1)
| sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| ~ in(apply(X1,sK3(X1)),sK3(X1))
| in(sK4(X1,sK3(X1)),sK3(X1))
| ~ in(sK25(X1,X0),X0) )
| ~ spl34_11 ),
inference(forward_demodulation,[],[f455,f173]) ).
fof(f460,definition,
( spl34_12
<=> ! [X2] :
( ~ relation(X2)
| ~ function(X2)
| relation_dom(X2) != sK1
| in(sK3(X2),sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_12])],[avatar_definition]) ).
fof(f461,plain,
( ! [X2] :
( relation_dom(X2) != sK1
| ~ function(X2)
| ~ relation(X2)
| in(sK3(X2),sK1) )
| ~ spl34_12 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f462,plain,
spl34_12,
inference(avatar_split_clause,[],[f118,f460]) ).
fof(f463,plain,
( ! [X0,X1] :
( sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| in(sK3(X1),sK1)
| in(unordered_pair(unordered_pair(sK25(X1,X0),sK26(X1,X0)),singleton(sK25(X1,X0))),X1)
| in(sK25(X1,X0),X0)
| ~ relation(X1) )
| ~ spl34_12 ),
inference(superposition,[],[f461,f224]) ).
fof(f466,plain,
( ! [X0,X1] :
( sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| in(sK3(X1),sK1)
| in(unordered_pair(unordered_pair(sK25(X1,X0),sK26(X1,X0)),singleton(sK25(X1,X0))),X1)
| in(sK25(X1,X0),X0) )
| ~ spl34_12 ),
inference(duplicate_literal_removal,[],[f463]) ).
fof(f468,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(sK25(X1,X0)),unordered_pair(sK25(X1,X0),sK26(X1,X0))),X1)
| sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| in(sK3(X1),sK1)
| in(sK25(X1,X0),X0) )
| ~ spl34_12 ),
inference(forward_demodulation,[],[f466,f173]) ).
fof(f498,definition,
( spl34_16
<=> ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X2),unordered_pair(X2,X0)),sK22(sK1,X1))
| in(X0,sK24(X1,X2,X0))
| sP0(sK1,X1)
| ~ relation(X1) ) ),
introduced(definition,[new_symbols(definition,[spl34_16])],[avatar_definition]) ).
fof(f499,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X2),unordered_pair(X2,X0)),sK22(sK1,X1))
| in(X0,sK24(X1,X2,X0))
| sP0(sK1,X1)
| ~ relation(X1) )
| ~ spl34_16 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f500,plain,
( spl34_16
| spl34_2 ),
inference(avatar_split_clause,[],[f313,f295,f498]) ).
fof(f509,definition,
( spl34_17
<=> ! [X11,X8,X7] :
( X7 = X8
| ~ in(X11,sK1)
| ~ in(X7,X11)
| in(sK5(X7,X11),X11)
| ~ in(X8,X11)
| in(sK6(X8,X11),X11) ) ),
introduced(definition,[new_symbols(definition,[spl34_17])],[avatar_definition]) ).
fof(f510,plain,
( ! [X11,X8,X7] :
( in(sK6(X8,X11),X11)
| ~ in(X11,sK1)
| ~ in(X7,X11)
| in(sK5(X7,X11),X11)
| ~ in(X8,X11)
| X7 = X8 )
| ~ spl34_17 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f511,plain,
spl34_17,
inference(avatar_split_clause,[],[f236,f509]) ).
fof(f858,definition,
( spl34_36
<=> ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),sK22(sK1,X0))
| sK24(X0,X1,X2) = X1
| sP0(sK1,X0)
| ~ relation(X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_36])],[avatar_definition]) ).
fof(f859,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),sK22(sK1,X0))
| sK24(X0,X1,X2) = X1
| sP0(sK1,X0)
| ~ relation(X0) )
| ~ spl34_36 ),
inference(avatar_component_clause,[],[f858]) ).
fof(f860,plain,
( spl34_36
| spl34_2 ),
inference(avatar_split_clause,[],[f314,f295,f858]) ).
fof(f869,definition,
( spl34_37
<=> ! [X0,X1] :
( in(unordered_pair(singleton(sK25(X1,X0)),unordered_pair(sK25(X1,X0),sK26(X1,X0))),X1)
| sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| in(sK3(X1),sK1)
| in(sK25(X1,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_37])],[avatar_definition]) ).
fof(f870,plain,
( ! [X0,X1] :
( sK1 != X0
| in(unordered_pair(singleton(sK25(X1,X0)),unordered_pair(sK25(X1,X0),sK26(X1,X0))),X1)
| ~ function(X1)
| ~ relation(X1)
| in(sK3(X1),sK1)
| in(sK25(X1,X0),X0) )
| ~ spl34_37 ),
inference(avatar_component_clause,[],[f869]) ).
fof(f871,plain,
( spl34_37
| ~ spl34_12 ),
inference(avatar_split_clause,[],[f468,f460,f869]) ).
fof(f872,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK25(X0,sK1)),unordered_pair(sK25(X0,sK1),sK26(X0,sK1))),X0)
| ~ function(X0)
| ~ relation(X0)
| in(sK3(X0),sK1)
| in(sK25(X0,sK1),sK1) )
| ~ spl34_37 ),
inference(equality_resolution,[],[f870]) ).
fof(f874,definition,
( spl34_38
<=> ! [X0] :
( in(unordered_pair(singleton(sK25(X0,sK1)),unordered_pair(sK25(X0,sK1),sK26(X0,sK1))),X0)
| ~ function(X0)
| ~ relation(X0)
| in(sK3(X0),sK1)
| in(sK25(X0,sK1),sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_38])],[avatar_definition]) ).
fof(f875,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK25(X0,sK1)),unordered_pair(sK25(X0,sK1),sK26(X0,sK1))),X0)
| ~ function(X0)
| ~ relation(X0)
| in(sK3(X0),sK1)
| in(sK25(X0,sK1),sK1) )
| ~ spl34_38 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f876,plain,
( spl34_38
| ~ spl34_37 ),
inference(avatar_split_clause,[],[f872,f869,f874]) ).
fof(f995,definition,
( spl34_42
<=> ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK22(X1,sK2))
| in(X0,X1)
| sP0(X1,sK2)
| empty(X1) ) ),
introduced(definition,[new_symbols(definition,[spl34_42])],[avatar_definition]) ).
fof(f996,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X2)),sK22(X1,sK2))
| in(X0,X1)
| sP0(X1,sK2)
| empty(X1) )
| ~ spl34_42 ),
inference(avatar_component_clause,[],[f995]) ).
fof(f997,plain,
( spl34_42
| ~ spl34_1 ),
inference(avatar_split_clause,[],[f288,f255,f995]) ).
fof(f998,plain,
( ! [X0] :
( in(sK25(sK22(X0,sK2),sK1),X0)
| sP0(X0,sK2)
| empty(X0)
| ~ function(sK22(X0,sK2))
| ~ relation(sK22(X0,sK2))
| in(sK3(sK22(X0,sK2)),sK1)
| in(sK25(sK22(X0,sK2),sK1),sK1) )
| ~ spl34_38
| ~ spl34_42 ),
inference(resolution,[],[f996,f875]) ).
fof(f1006,plain,
( ! [X0] :
( in(sK25(sK22(X0,sK2),sK1),X0)
| sP0(X0,sK2)
| empty(X0)
| ~ relation(sK22(X0,sK2))
| in(sK3(sK22(X0,sK2)),sK1)
| in(sK25(sK22(X0,sK2),sK1),sK1) )
| ~ spl34_1
| ~ spl34_38
| ~ spl34_42 ),
inference(forward_subsumption_resolution,[],[f998,f259]) ).
fof(f1007,plain,
( ! [X0] :
( in(sK25(sK22(X0,sK2),sK1),X0)
| sP0(X0,sK2)
| empty(X0)
| in(sK3(sK22(X0,sK2)),sK1)
| in(sK25(sK22(X0,sK2),sK1),sK1) )
| ~ spl34_1
| ~ spl34_38
| ~ spl34_42 ),
inference(forward_subsumption_resolution,[],[f1006,f260]) ).
fof(f1009,definition,
( spl34_43
<=> ! [X0] :
( in(sK25(sK22(X0,sK2),sK1),X0)
| sP0(X0,sK2)
| empty(X0)
| in(sK3(sK22(X0,sK2)),sK1)
| in(sK25(sK22(X0,sK2),sK1),sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_43])],[avatar_definition]) ).
fof(f1010,plain,
( ! [X0] :
( in(sK25(sK22(X0,sK2),sK1),sK1)
| sP0(X0,sK2)
| empty(X0)
| in(sK3(sK22(X0,sK2)),sK1)
| in(sK25(sK22(X0,sK2),sK1),X0) )
| ~ spl34_43 ),
inference(avatar_component_clause,[],[f1009]) ).
fof(f1011,plain,
( spl34_43
| ~ spl34_1
| ~ spl34_38
| ~ spl34_42 ),
inference(avatar_split_clause,[],[f1007,f995,f874,f255,f1009]) ).
fof(f1021,plain,
( in(sK25(sK22(sK1,sK2),sK1),sK1)
| sP0(sK1,sK2)
| empty(sK1)
| in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_43 ),
inference(factoring,[],[f1010]) ).
fof(f1022,plain,
( in(sK25(sK22(sK1,sK2),sK1),sK1)
| sP0(sK1,sK2)
| in(sK3(sK22(sK1,sK2)),sK1)
| spl34_2
| ~ spl34_43 ),
inference(forward_subsumption_resolution,[],[f1021,f297]) ).
fof(f1036,definition,
( spl34_44
<=> in(sK3(sK22(sK1,sK2)),sK1) ),
introduced(definition,[new_symbols(definition,[spl34_44])],[avatar_definition]) ).
fof(f1037,plain,
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| spl34_44 ),
inference(avatar_component_clause,[],[f1036]) ).
fof(f1038,plain,
( in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_44 ),
inference(avatar_component_clause,[],[f1036]) ).
fof(f1040,definition,
( spl34_45
<=> sP0(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl34_45])],[avatar_definition]) ).
fof(f1041,plain,
( ~ sP0(sK1,sK2)
| spl34_45 ),
inference(avatar_component_clause,[],[f1040]) ).
fof(f1042,plain,
( sP0(sK1,sK2)
| ~ spl34_45 ),
inference(avatar_component_clause,[],[f1040]) ).
fof(f1044,definition,
( spl34_46
<=> in(sK25(sK22(sK1,sK2),sK1),sK1) ),
introduced(definition,[new_symbols(definition,[spl34_46])],[avatar_definition]) ).
fof(f1045,plain,
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| spl34_46 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1046,plain,
( in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ spl34_46 ),
inference(avatar_component_clause,[],[f1044]) ).
fof(f1047,plain,
( spl34_44
| spl34_45
| spl34_46
| spl34_2
| ~ spl34_43 ),
inference(avatar_split_clause,[],[f1022,f1009,f295,f1044,f1040,f1036]) ).
fof(f1090,definition,
( spl34_48
<=> ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(sK25(X1,X0)),unordered_pair(sK25(X1,X0),X2)),X1)
| sK1 != X0
| ~ function(X1)
| ~ relation(X1)
| ~ in(apply(X1,sK3(X1)),sK3(X1))
| in(sK4(X1,sK3(X1)),sK3(X1))
| ~ in(sK25(X1,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_48])],[avatar_definition]) ).
fof(f1091,plain,
( ! [X2,X0,X1] :
( sK1 != X0
| ~ in(unordered_pair(singleton(sK25(X1,X0)),unordered_pair(sK25(X1,X0),X2)),X1)
| ~ function(X1)
| ~ relation(X1)
| ~ in(apply(X1,sK3(X1)),sK3(X1))
| in(sK4(X1,sK3(X1)),sK3(X1))
| ~ in(sK25(X1,X0),X0) )
| ~ spl34_48 ),
inference(avatar_component_clause,[],[f1090]) ).
fof(f1092,plain,
( spl34_48
| ~ spl34_11 ),
inference(avatar_split_clause,[],[f457,f450,f1090]) ).
fof(f1093,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(sK25(X0,sK1)),unordered_pair(sK25(X0,sK1),X1)),X0)
| ~ function(X0)
| ~ relation(X0)
| ~ in(apply(X0,sK3(X0)),sK3(X0))
| in(sK4(X0,sK3(X0)),sK3(X0))
| ~ in(sK25(X0,sK1),sK1) )
| ~ spl34_48 ),
inference(equality_resolution,[],[f1091]) ).
fof(f1095,definition,
( spl34_49
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(sK25(X0,sK1)),unordered_pair(sK25(X0,sK1),X1)),X0)
| ~ function(X0)
| ~ relation(X0)
| ~ in(apply(X0,sK3(X0)),sK3(X0))
| in(sK4(X0,sK3(X0)),sK3(X0))
| ~ in(sK25(X0,sK1),sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_49])],[avatar_definition]) ).
fof(f1096,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(sK25(X0,sK1)),unordered_pair(sK25(X0,sK1),X1)),X0)
| ~ function(X0)
| ~ relation(X0)
| ~ in(apply(X0,sK3(X0)),sK3(X0))
| in(sK4(X0,sK3(X0)),sK3(X0))
| ~ in(sK25(X0,sK1),sK1) )
| ~ spl34_49 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1097,plain,
( spl34_49
| ~ spl34_48 ),
inference(avatar_split_clause,[],[f1093,f1090,f1095]) ).
fof(f1155,definition,
( spl34_53
<=> ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK23(X2,X1,X0))),X2)
| in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(sK1,X2))
| ~ in(X0,sK1)
| ~ in(X1,X0)
| sP0(sK1,X2)
| ~ relation(X2) ) ),
introduced(definition,[new_symbols(definition,[spl34_53])],[avatar_definition]) ).
fof(f1156,plain,
( ! [X2,X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK23(X2,X1,X0))),X2)
| in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(sK1,X2))
| ~ in(X0,sK1)
| ~ in(X1,X0)
| sP0(sK1,X2)
| ~ relation(X2) )
| ~ spl34_53 ),
inference(avatar_component_clause,[],[f1155]) ).
fof(f1157,plain,
( spl34_53
| spl34_2 ),
inference(avatar_split_clause,[],[f317,f295,f1155]) ).
fof(f1158,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK7(X1))),sK22(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK7(X1),X0)
| sP0(sK1,sK2)
| ~ relation(sK2)
| ~ in(X1,sK1)
| ~ in(sK23(sK2,sK7(X1),X0),sK8(X1)) )
| ~ spl34_6
| ~ spl34_53 ),
inference(resolution,[],[f1156,f340]) ).
fof(f1170,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK7(X1))),sK22(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK7(X1),X0)
| sP0(sK1,sK2)
| ~ in(X1,sK1)
| ~ in(sK23(sK2,sK7(X1),X0),sK8(X1)) )
| ~ spl34_1
| ~ spl34_6
| ~ spl34_53 ),
inference(forward_subsumption_resolution,[],[f1158,f257]) ).
fof(f1349,definition,
( spl34_61
<=> ! [X2,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(X2,sK2))
| ~ in(X0,X2)
| ~ in(X1,X0)
| in(sK23(sK2,X1,X0),X0)
| sP0(X2,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl34_61])],[avatar_definition]) ).
fof(f1350,plain,
( ! [X2,X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(X2,sK2))
| ~ in(X0,X2)
| ~ in(X1,X0)
| in(sK23(sK2,X1,X0),X0)
| sP0(X2,sK2) )
| ~ spl34_61 ),
inference(avatar_component_clause,[],[f1349]) ).
fof(f1351,plain,
( spl34_61
| ~ spl34_1 ),
inference(avatar_split_clause,[],[f290,f255,f1349]) ).
fof(f1713,plain,
( sK21(sK1,sK2) = sK17(sK1,sK2)
| ~ spl34_45 ),
inference(resolution,[],[f1042,f156]) ).
fof(f1728,definition,
( spl34_71
<=> sK21(sK1,sK2) = sK17(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl34_71])],[avatar_definition]) ).
fof(f1730,plain,
( sK21(sK1,sK2) = sK17(sK1,sK2)
| ~ spl34_71 ),
inference(avatar_component_clause,[],[f1728]) ).
fof(f1731,plain,
( spl34_71
| ~ spl34_45 ),
inference(avatar_split_clause,[],[f1713,f1040,f1728]) ).
fof(f1733,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK7(X1))),sK22(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK7(X1),X0)
| ~ in(X1,sK1)
| ~ in(sK23(sK2,sK7(X1),X0),sK8(X1)) )
| ~ spl34_1
| ~ spl34_6
| spl34_45
| ~ spl34_53 ),
inference(backward_subsumption_resolution,[],[f1170,f1041]) ).
fof(f1735,plain,
( ! [X0] :
( sK1 = relation_dom(sK22(sK1,sK2))
| ~ in(unordered_pair(unordered_pair(sK25(sK22(sK1,sK2),sK1),X0),singleton(sK25(sK22(sK1,sK2),sK1))),sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2)) )
| ~ spl34_46 ),
inference(resolution,[],[f1046,f223]) ).
fof(f1748,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK25(sK22(sK1,sK2),sK1)),unordered_pair(sK25(sK22(sK1,sK2),sK1),X0)),sK22(sK1,sK2))
| sK1 = relation_dom(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2)) )
| ~ spl34_46 ),
inference(forward_demodulation,[],[f1735,f173]) ).
fof(f1756,plain,
( relation(sK22(sK1,sK2))
| empty(sK1)
| ~ relation(sK2)
| spl34_45 ),
inference(resolution,[],[f1041,f171]) ).
fof(f1771,plain,
( relation(sK22(sK1,sK2))
| ~ relation(sK2)
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1756,f297]) ).
fof(f1780,plain,
( relation(sK22(sK1,sK2))
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1771,f257]) ).
fof(f1788,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK25(sK22(sK1,sK2),sK1)),unordered_pair(sK25(sK22(sK1,sK2),sK1),X0)),sK22(sK1,sK2))
| sK1 = relation_dom(sK22(sK1,sK2)) )
| ~ spl34_1
| spl34_2
| spl34_45
| ~ spl34_46 ),
inference(backward_subsumption_resolution,[],[f1748,f1780]) ).
fof(f1791,definition,
( spl34_72
<=> sK1 = relation_dom(sK22(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_72])],[avatar_definition]) ).
fof(f1792,plain,
( sK1 != relation_dom(sK22(sK1,sK2))
| spl34_72 ),
inference(avatar_component_clause,[],[f1791]) ).
fof(f1793,plain,
( sK1 = relation_dom(sK22(sK1,sK2))
| ~ spl34_72 ),
inference(avatar_component_clause,[],[f1791]) ).
fof(f1795,definition,
( spl34_73
<=> ! [X0] : ~ in(unordered_pair(singleton(sK25(sK22(sK1,sK2),sK1)),unordered_pair(sK25(sK22(sK1,sK2),sK1),X0)),sK22(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_73])],[avatar_definition]) ).
fof(f1796,plain,
( ! [X0] : ~ in(unordered_pair(singleton(sK25(sK22(sK1,sK2),sK1)),unordered_pair(sK25(sK22(sK1,sK2),sK1),X0)),sK22(sK1,sK2))
| ~ spl34_73 ),
inference(avatar_component_clause,[],[f1795]) ).
fof(f1797,plain,
( spl34_72
| spl34_73
| ~ spl34_1
| spl34_2
| spl34_45
| ~ spl34_46 ),
inference(avatar_split_clause,[],[f1788,f1044,f1040,f295,f255,f1795,f1791]) ).
fof(f1835,plain,
( ! [X0] :
( ~ in(X0,sK17(sK1,sK2))
| in(unordered_pair(unordered_pair(sK19(sK1,sK2),X0),singleton(sK19(sK1,sK2))),sK2)
| ~ sP0(sK1,sK2) )
| ~ spl34_71 ),
inference(superposition,[],[f213,f1730]) ).
fof(f1836,plain,
( in(sK19(sK1,sK2),sK17(sK1,sK2))
| ~ sP0(sK1,sK2)
| ~ spl34_71 ),
inference(superposition,[],[f155,f1730]) ).
fof(f1837,plain,
( in(sK19(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_45
| ~ spl34_71 ),
inference(forward_subsumption_resolution,[],[f1836,f1042]) ).
fof(f1841,definition,
( spl34_75
<=> in(sK19(sK1,sK2),sK17(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_75])],[avatar_definition]) ).
fof(f1843,plain,
( in(sK19(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_75 ),
inference(avatar_component_clause,[],[f1841]) ).
fof(f1844,plain,
( spl34_75
| ~ spl34_45
| ~ spl34_71 ),
inference(avatar_split_clause,[],[f1837,f1728,f1040,f1841]) ).
fof(f1858,plain,
( sK1 != sK1
| ~ relation(sK22(sK1,sK2))
| ~ function(sK22(sK1,sK2))
| ~ in(unordered_pair(singleton(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),unordered_pair(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_7
| ~ spl34_72 ),
inference(superposition,[],[f365,f1793]) ).
fof(f1859,plain,
( sK1 != sK1
| ~ function(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_11
| ~ spl34_72 ),
inference(superposition,[],[f451,f1793]) ).
fof(f1860,plain,
( sK1 != sK1
| ~ function(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_12
| ~ spl34_72 ),
inference(superposition,[],[f461,f1793]) ).
fof(f1861,plain,
( ~ function(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_12
| ~ spl34_72 ),
inference(trivial_inequality_removal,[],[f1860]) ).
fof(f1862,plain,
( ~ function(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_11
| ~ spl34_72 ),
inference(trivial_inequality_removal,[],[f1859]) ).
fof(f1863,plain,
( ~ relation(sK22(sK1,sK2))
| ~ function(sK22(sK1,sK2))
| ~ in(unordered_pair(singleton(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),unordered_pair(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_7
| ~ spl34_72 ),
inference(trivial_inequality_removal,[],[f1858]) ).
fof(f1893,plain,
( function(sK22(sK1,sK2))
| empty(sK1)
| ~ relation(sK2)
| spl34_45 ),
inference(resolution,[],[f1041,f170]) ).
fof(f1894,plain,
( relation(sK22(sK1,sK2))
| empty(sK1)
| ~ relation(sK2)
| spl34_45 ),
inference(resolution,[],[f1041,f171]) ).
fof(f1896,plain,
( ! [X0,X1] :
( in(X0,sK1)
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK22(sK1,sK2))
| empty(sK1)
| ~ relation(sK2) )
| spl34_45 ),
inference(resolution,[],[f1041,f217]) ).
fof(f1907,plain,
( ! [X0,X1] :
( in(X0,sK1)
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK22(sK1,sK2))
| ~ relation(sK2) )
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1896,f297]) ).
fof(f1909,plain,
( relation(sK22(sK1,sK2))
| ~ relation(sK2)
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1894,f297]) ).
fof(f1910,plain,
( function(sK22(sK1,sK2))
| ~ relation(sK2)
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1893,f297]) ).
fof(f1916,plain,
( ! [X0,X1] :
( in(X0,sK1)
| ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sK22(sK1,sK2)) )
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1907,f257]) ).
fof(f1918,plain,
( relation(sK22(sK1,sK2))
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1909,f257]) ).
fof(f1919,plain,
( function(sK22(sK1,sK2))
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(forward_subsumption_resolution,[],[f1910,f257]) ).
fof(f1924,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(sK1,sK2))
| in(X0,sK1) )
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(forward_demodulation,[],[f1916,f173]) ).
fof(f1927,plain,
( ~ function(sK22(sK1,sK2))
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_1
| spl34_2
| ~ spl34_11
| spl34_45
| ~ spl34_72 ),
inference(backward_subsumption_resolution,[],[f1862,f1918]) ).
fof(f1928,plain,
( ~ function(sK22(sK1,sK2))
| ~ in(unordered_pair(singleton(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),unordered_pair(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_1
| spl34_2
| ~ spl34_7
| spl34_45
| ~ spl34_72 ),
inference(backward_subsumption_resolution,[],[f1863,f1918]) ).
fof(f1937,plain,
( ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_1
| spl34_2
| ~ spl34_11
| spl34_45
| ~ spl34_72 ),
inference(forward_subsumption_resolution,[],[f1927,f1919]) ).
fof(f1938,plain,
( ~ in(unordered_pair(singleton(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),unordered_pair(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_1
| spl34_2
| ~ spl34_7
| spl34_45
| ~ spl34_72 ),
inference(forward_subsumption_resolution,[],[f1928,f1919]) ).
fof(f1946,definition,
( spl34_77
<=> in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl34_77])],[avatar_definition]) ).
fof(f1948,plain,
( in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_77 ),
inference(avatar_component_clause,[],[f1946]) ).
fof(f1950,definition,
( spl34_78
<=> in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl34_78])],[avatar_definition]) ).
fof(f1951,plain,
( in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_78 ),
inference(avatar_component_clause,[],[f1950]) ).
fof(f1952,plain,
( ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| spl34_78 ),
inference(avatar_component_clause,[],[f1950]) ).
fof(f1953,plain,
( spl34_77
| ~ spl34_78
| ~ spl34_1
| spl34_2
| ~ spl34_11
| spl34_45
| ~ spl34_72 ),
inference(avatar_split_clause,[],[f1937,f1791,f1040,f450,f295,f255,f1950,f1946]) ).
fof(f1991,definition,
( spl34_80
<=> in(unordered_pair(singleton(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),unordered_pair(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2) ),
introduced(definition,[new_symbols(definition,[spl34_80])],[avatar_definition]) ).
fof(f1993,plain,
( ~ in(unordered_pair(singleton(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),unordered_pair(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| spl34_80 ),
inference(avatar_component_clause,[],[f1991]) ).
fof(f1994,plain,
( ~ spl34_78
| ~ spl34_80
| ~ spl34_1
| spl34_2
| ~ spl34_7
| spl34_45
| ~ spl34_72 ),
inference(avatar_split_clause,[],[f1938,f1791,f1040,f364,f295,f255,f1991,f1950]) ).
fof(f2189,definition,
( spl34_87
<=> function(sK22(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_87])],[avatar_definition]) ).
fof(f2191,plain,
( function(sK22(sK1,sK2))
| ~ spl34_87 ),
inference(avatar_component_clause,[],[f2189]) ).
fof(f2192,plain,
( spl34_87
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(avatar_split_clause,[],[f1919,f1040,f295,f255,f2189]) ).
fof(f2308,definition,
( spl34_90
<=> ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(sK1,sK2))
| in(X0,sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_90])],[avatar_definition]) ).
fof(f2309,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,X1)),sK22(sK1,sK2))
| in(X0,sK1) )
| ~ spl34_90 ),
inference(avatar_component_clause,[],[f2308]) ).
fof(f2310,plain,
( spl34_90
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(avatar_split_clause,[],[f1924,f1040,f295,f255,f2308]) ).
fof(f2341,definition,
( spl34_92
<=> relation(sK22(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_92])],[avatar_definition]) ).
fof(f2343,plain,
( relation(sK22(sK1,sK2))
| ~ spl34_92 ),
inference(avatar_component_clause,[],[f2341]) ).
fof(f2344,plain,
( spl34_92
| ~ spl34_1
| spl34_2
| spl34_45 ),
inference(avatar_split_clause,[],[f1918,f1040,f295,f255,f2341]) ).
fof(f2963,definition,
( spl34_117
<=> ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK27(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| ~ in(X0,sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_117])],[avatar_definition]) ).
fof(f2964,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK27(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| ~ in(X0,sK1) )
| ~ spl34_117 ),
inference(avatar_component_clause,[],[f2963]) ).
fof(f3285,plain,
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ function(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ spl34_49
| ~ spl34_117 ),
inference(resolution,[],[f2964,f1096]) ).
fof(f3298,plain,
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ function(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_49
| ~ spl34_117 ),
inference(duplicate_literal_removal,[],[f3285]) ).
fof(f3764,definition,
( spl34_144
<=> ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK7(X1))),sK22(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK7(X1),X0)
| ~ in(X1,sK1)
| ~ in(sK23(sK2,sK7(X1),X0),sK8(X1)) ) ),
introduced(definition,[new_symbols(definition,[spl34_144])],[avatar_definition]) ).
fof(f3765,plain,
( ! [X0,X1] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK7(X1))),sK22(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK7(X1),X0)
| ~ in(X1,sK1)
| ~ in(sK23(sK2,sK7(X1),X0),sK8(X1)) )
| ~ spl34_144 ),
inference(avatar_component_clause,[],[f3764]) ).
fof(f3766,plain,
( spl34_144
| ~ spl34_1
| ~ spl34_6
| spl34_45
| ~ spl34_53 ),
inference(avatar_split_clause,[],[f1733,f1155,f1040,f339,f255,f3764]) ).
fof(f3980,plain,
( ~ relation(sK22(sK1,sK2))
| in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_12
| ~ spl34_72
| ~ spl34_87 ),
inference(forward_subsumption_resolution,[],[f1861,f2191]) ).
fof(f3992,plain,
( in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_12
| ~ spl34_72
| ~ spl34_87
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f3980,f2343]) ).
fof(f3998,plain,
( $false
| ~ spl34_12
| spl34_44
| ~ spl34_72
| ~ spl34_87
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f3992,f1037]) ).
fof(f3999,plain,
( ~ spl34_12
| spl34_44
| ~ spl34_72
| ~ spl34_87
| ~ spl34_92 ),
inference(avatar_contradiction_clause,[],[f3998]) ).
fof(f4019,plain,
( ~ function(sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_46
| ~ spl34_49
| ~ spl34_117 ),
inference(forward_subsumption_resolution,[],[f3298,f1046]) ).
fof(f4033,plain,
( ~ relation(sK22(sK1,sK2))
| ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_46
| ~ spl34_49
| ~ spl34_87
| ~ spl34_117 ),
inference(forward_subsumption_resolution,[],[f4019,f2191]) ).
fof(f4044,plain,
( ~ in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_46
| ~ spl34_49
| ~ spl34_87
| ~ spl34_92
| ~ spl34_117 ),
inference(forward_subsumption_resolution,[],[f4033,f2343]) ).
fof(f4051,plain,
( in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_46
| ~ spl34_49
| ~ spl34_78
| ~ spl34_87
| ~ spl34_92
| ~ spl34_117 ),
inference(forward_subsumption_resolution,[],[f4044,f1951]) ).
fof(f4105,definition,
( spl34_150
<=> ! [X0] : ~ in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),X0)),sK22(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_150])],[avatar_definition]) ).
fof(f4106,plain,
( ! [X0] : ~ in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),X0)),sK22(sK1,sK2))
| ~ spl34_150 ),
inference(avatar_component_clause,[],[f4105]) ).
fof(f4111,plain,
( ! [X0] :
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ in(X0,sK25(sK22(sK1,sK2),sK1))
| in(sK23(sK2,X0,sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1))
| sP0(sK1,sK2) )
| ~ spl34_61
| ~ spl34_73 ),
inference(resolution,[],[f1796,f1350]) ).
fof(f4112,plain,
( ! [X0] :
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),sK8(X0)) )
| ~ spl34_73
| ~ spl34_144 ),
inference(resolution,[],[f1796,f3765]) ).
fof(f4134,plain,
( ! [X0] :
( ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),sK8(X0)) )
| ~ spl34_46
| ~ spl34_73
| ~ spl34_144 ),
inference(forward_subsumption_resolution,[],[f4112,f1046]) ).
fof(f4135,plain,
( ! [X0] :
( ~ in(X0,sK25(sK22(sK1,sK2),sK1))
| in(sK23(sK2,X0,sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1))
| sP0(sK1,sK2) )
| ~ spl34_46
| ~ spl34_61
| ~ spl34_73 ),
inference(forward_subsumption_resolution,[],[f4111,f1046]) ).
fof(f4141,plain,
( ! [X0] :
( ~ in(X0,sK25(sK22(sK1,sK2),sK1))
| in(sK23(sK2,X0,sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1)) )
| spl34_45
| ~ spl34_46
| ~ spl34_61
| ~ spl34_73 ),
inference(forward_subsumption_resolution,[],[f4135,f1041]) ).
fof(f4153,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),X0),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ in(sK3(sK22(sK1,sK2)),relation_dom(sK22(sK1,sK2)))
| ~ relation(sK22(sK1,sK2))
| ~ function(sK22(sK1,sK2)) )
| spl34_80 ),
inference(superposition,[],[f1993,f221]) ).
fof(f4154,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),X0),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| ~ function(sK22(sK1,sK2)) )
| spl34_80 ),
inference(forward_subsumption_resolution,[],[f4153,f242]) ).
fof(f4160,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),X0),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ function(sK22(sK1,sK2)) )
| spl34_80
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f4154,f2343]) ).
fof(f4165,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),X0),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2)) )
| spl34_80
| ~ spl34_87
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f4160,f2191]) ).
fof(f4168,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),X0)),sK22(sK1,sK2))
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2) )
| spl34_80
| ~ spl34_87
| ~ spl34_92 ),
inference(forward_demodulation,[],[f4165,f173]) ).
fof(f4206,plain,
( spl34_77
| ~ spl34_46
| ~ spl34_49
| ~ spl34_78
| ~ spl34_87
| ~ spl34_92
| ~ spl34_117 ),
inference(avatar_split_clause,[],[f4051,f2963,f2341,f2189,f1950,f1095,f1044,f1946]) ).
fof(f4227,plain,
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_117
| ~ spl34_150 ),
inference(resolution,[],[f4106,f2964]) ).
fof(f4240,plain,
( $false
| ~ spl34_44
| ~ spl34_117
| ~ spl34_150 ),
inference(forward_subsumption_resolution,[],[f4227,f1038]) ).
fof(f4241,plain,
( ~ spl34_44
| ~ spl34_117
| ~ spl34_150 ),
inference(avatar_contradiction_clause,[],[f4240]) ).
fof(f4274,definition,
( spl34_152
<=> in(sK3(sK22(sK1,sK2)),relation_dom(sK22(sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl34_152])],[avatar_definition]) ).
fof(f4275,plain,
( ~ in(sK3(sK22(sK1,sK2)),relation_dom(sK22(sK1,sK2)))
| spl34_152 ),
inference(avatar_component_clause,[],[f4274]) ).
fof(f4276,plain,
( in(sK3(sK22(sK1,sK2)),relation_dom(sK22(sK1,sK2)))
| ~ spl34_152 ),
inference(avatar_component_clause,[],[f4274]) ).
fof(f4312,definition,
( spl34_156
<=> ! [X0] :
( ~ in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),X0)),sK22(sK1,sK2))
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2) ) ),
introduced(definition,[new_symbols(definition,[spl34_156])],[avatar_definition]) ).
fof(f4313,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),X0)),sK22(sK1,sK2))
| ~ in(unordered_pair(singleton(X0),unordered_pair(X0,sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2) )
| ~ spl34_156 ),
inference(avatar_component_clause,[],[f4312]) ).
fof(f4314,plain,
( spl34_156
| spl34_80
| ~ spl34_87
| ~ spl34_92 ),
inference(avatar_split_clause,[],[f4168,f2341,f2189,f1991,f4312]) ).
fof(f4316,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK7(X0)),unordered_pair(sK7(X0),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0)) )
| ~ spl34_144
| ~ spl34_156 ),
inference(resolution,[],[f4313,f3765]) ).
fof(f4331,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK7(X0)),unordered_pair(sK7(X0),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0)) )
| ~ spl34_44
| ~ spl34_144
| ~ spl34_156 ),
inference(forward_subsumption_resolution,[],[f4316,f1038]) ).
fof(f4491,definition,
( spl34_163
<=> ! [X0] :
( ~ in(unordered_pair(singleton(sK7(X0)),unordered_pair(sK7(X0),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl34_163])],[avatar_definition]) ).
fof(f4492,plain,
( ! [X0] :
( ~ in(unordered_pair(singleton(sK7(X0)),unordered_pair(sK7(X0),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0)) )
| ~ spl34_163 ),
inference(avatar_component_clause,[],[f4491]) ).
fof(f4493,plain,
( spl34_163
| ~ spl34_44
| ~ spl34_144
| ~ spl34_156 ),
inference(avatar_split_clause,[],[f4331,f4312,f3764,f1036,f4491]) ).
fof(f4494,plain,
( ! [X0] :
( ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0))
| ~ in(X0,sK1)
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(X0)) )
| ~ spl34_6
| ~ spl34_163 ),
inference(resolution,[],[f4492,f340]) ).
fof(f4501,plain,
( ! [X0] :
( ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(X0)) )
| ~ spl34_6
| ~ spl34_163 ),
inference(duplicate_literal_removal,[],[f4494]) ).
fof(f4508,definition,
( spl34_164
<=> ! [X0] :
( ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl34_164])],[avatar_definition]) ).
fof(f4509,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),sK8(X0))
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(X0)) )
| ~ spl34_164 ),
inference(avatar_component_clause,[],[f4508]) ).
fof(f4510,plain,
( spl34_164
| ~ spl34_6
| ~ spl34_163 ),
inference(avatar_split_clause,[],[f4501,f4491,f339,f4508]) ).
fof(f4514,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),X0)
| ~ in(X0,sK1) )
| ~ spl34_3
| ~ spl34_164 ),
inference(superposition,[],[f4509,f320]) ).
fof(f4515,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),X0) )
| ~ spl34_3
| ~ spl34_164 ),
inference(duplicate_literal_removal,[],[f4514]) ).
fof(f4522,definition,
( spl34_165
<=> ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_165])],[avatar_definition]) ).
fof(f4523,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK3(sK22(sK1,sK2))),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),X0) )
| ~ spl34_165 ),
inference(avatar_component_clause,[],[f4522]) ).
fof(f4524,plain,
( spl34_165
| ~ spl34_3
| ~ spl34_164 ),
inference(avatar_split_clause,[],[f4515,f4508,f319,f4522]) ).
fof(f4528,plain,
( ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ in(sK7(sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| ~ in(sK7(sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| sP0(X0,sK2)
| empty(X0)
| ~ relation(sK2) )
| ~ spl34_165 ),
inference(resolution,[],[f4523,f247]) ).
fof(f4543,plain,
( ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ in(sK7(sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2)
| empty(X0)
| ~ relation(sK2) )
| ~ spl34_165 ),
inference(duplicate_literal_removal,[],[f4528]) ).
fof(f4555,plain,
( ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ in(sK7(sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2)
| ~ relation(sK2) )
| ~ spl34_165 ),
inference(forward_subsumption_resolution,[],[f4543,f204]) ).
fof(f4565,plain,
( ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2)
| ~ relation(sK2) )
| ~ spl34_10
| ~ spl34_165 ),
inference(forward_subsumption_resolution,[],[f4555,f417]) ).
fof(f4574,plain,
( ! [X0] :
( ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2)
| ~ relation(sK2) )
| ~ spl34_10
| ~ spl34_44
| ~ spl34_165 ),
inference(forward_subsumption_resolution,[],[f4565,f1038]) ).
fof(f4581,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2)
| ~ relation(sK2) )
| ~ spl34_10
| ~ spl34_44
| ~ spl34_77
| ~ spl34_165 ),
inference(forward_subsumption_resolution,[],[f4574,f1948]) ).
fof(f4586,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2) )
| ~ spl34_1
| ~ spl34_10
| ~ spl34_44
| ~ spl34_77
| ~ spl34_165 ),
inference(forward_subsumption_resolution,[],[f4581,f257]) ).
fof(f4589,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2))))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2) )
| ~ spl34_1
| ~ spl34_10
| ~ spl34_44
| ~ spl34_77
| ~ spl34_165 ),
inference(forward_demodulation,[],[f4586,f173]) ).
fof(f4678,definition,
( spl34_170
<=> ! [X0] :
( in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2))))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl34_170])],[avatar_definition]) ).
fof(f4679,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),sK7(sK3(sK22(sK1,sK2))))),sK22(X0,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| sP0(X0,sK2) )
| ~ spl34_170 ),
inference(avatar_component_clause,[],[f4678]) ).
fof(f4680,plain,
( spl34_170
| ~ spl34_1
| ~ spl34_10
| ~ spl34_44
| ~ spl34_77
| ~ spl34_165 ),
inference(avatar_split_clause,[],[f4589,f4522,f1946,f1036,f416,f255,f4678]) ).
fof(f4681,plain,
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| sP0(sK1,sK2)
| ~ in(unordered_pair(singleton(sK7(sK3(sK22(sK1,sK2)))),unordered_pair(sK7(sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ spl34_156
| ~ spl34_170 ),
inference(resolution,[],[f4679,f4313]) ).
fof(f4712,plain,
( sP0(sK1,sK2)
| ~ in(unordered_pair(singleton(sK7(sK3(sK22(sK1,sK2)))),unordered_pair(sK7(sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ spl34_44
| ~ spl34_156
| ~ spl34_170 ),
inference(forward_subsumption_resolution,[],[f4681,f1038]) ).
fof(f4719,plain,
( ~ in(unordered_pair(singleton(sK7(sK3(sK22(sK1,sK2)))),unordered_pair(sK7(sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| ~ spl34_44
| spl34_45
| ~ spl34_156
| ~ spl34_170 ),
inference(forward_subsumption_resolution,[],[f4712,f1041]) ).
fof(f4806,definition,
( spl34_174
<=> in(unordered_pair(singleton(sK7(sK3(sK22(sK1,sK2)))),unordered_pair(sK7(sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2) ),
introduced(definition,[new_symbols(definition,[spl34_174])],[avatar_definition]) ).
fof(f4808,plain,
( ~ in(unordered_pair(singleton(sK7(sK3(sK22(sK1,sK2)))),unordered_pair(sK7(sK3(sK22(sK1,sK2))),sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK2)
| spl34_174 ),
inference(avatar_component_clause,[],[f4806]) ).
fof(f4809,plain,
( ~ spl34_174
| ~ spl34_44
| spl34_45
| ~ spl34_156
| ~ spl34_170 ),
inference(avatar_split_clause,[],[f4719,f4678,f4312,f1040,f1036,f4806]) ).
fof(f4830,plain,
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(sK3(sK22(sK1,sK2))))
| ~ spl34_6
| spl34_174 ),
inference(resolution,[],[f4808,f340]) ).
fof(f4838,plain,
( ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(sK3(sK22(sK1,sK2))))
| ~ spl34_6
| ~ spl34_44
| spl34_174 ),
inference(forward_subsumption_resolution,[],[f4830,f1038]) ).
fof(f4890,plain,
( in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| ~ function(sK22(sK1,sK2))
| ~ spl34_152 ),
inference(resolution,[],[f4276,f239]) ).
fof(f4909,plain,
( in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ function(sK22(sK1,sK2))
| ~ spl34_92
| ~ spl34_152 ),
inference(forward_subsumption_resolution,[],[f4890,f2343]) ).
fof(f4918,plain,
( in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ spl34_87
| ~ spl34_92
| ~ spl34_152 ),
inference(forward_subsumption_resolution,[],[f4909,f2191]) ).
fof(f4923,plain,
( in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK22(sK1,sK2))
| ~ spl34_87
| ~ spl34_92
| ~ spl34_152 ),
inference(forward_demodulation,[],[f4918,f173]) ).
fof(f5052,definition,
( spl34_179
<=> in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK22(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_179])],[avatar_definition]) ).
fof(f5054,plain,
( in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))),sK22(sK1,sK2))
| ~ spl34_179 ),
inference(avatar_component_clause,[],[f5052]) ).
fof(f5055,plain,
( spl34_179
| ~ spl34_87
| ~ spl34_92
| ~ spl34_152 ),
inference(avatar_split_clause,[],[f4923,f4274,f2341,f2189,f5052]) ).
fof(f5198,definition,
( spl34_182
<=> in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(sK3(sK22(sK1,sK2)))) ),
introduced(definition,[new_symbols(definition,[spl34_182])],[avatar_definition]) ).
fof(f5200,plain,
( ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK8(sK3(sK22(sK1,sK2))))
| spl34_182 ),
inference(avatar_component_clause,[],[f5198]) ).
fof(f5201,plain,
( ~ spl34_182
| ~ spl34_6
| ~ spl34_44
| spl34_174 ),
inference(avatar_split_clause,[],[f4838,f4806,f1036,f339,f5198]) ).
fof(f5281,plain,
( sK3(sK22(sK1,sK2)) = sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))
| sP0(sK1,sK2)
| ~ relation(sK2)
| ~ spl34_36
| ~ spl34_179 ),
inference(resolution,[],[f5054,f859]) ).
fof(f5283,plain,
( in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))))
| sP0(sK1,sK2)
| ~ relation(sK2)
| ~ spl34_16
| ~ spl34_179 ),
inference(resolution,[],[f5054,f499]) ).
fof(f5307,plain,
( in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))))
| ~ relation(sK2)
| ~ spl34_16
| spl34_45
| ~ spl34_179 ),
inference(forward_subsumption_resolution,[],[f5283,f1041]) ).
fof(f5309,plain,
( sK3(sK22(sK1,sK2)) = sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))
| ~ relation(sK2)
| ~ spl34_36
| spl34_45
| ~ spl34_179 ),
inference(forward_subsumption_resolution,[],[f5281,f1041]) ).
fof(f5317,plain,
( in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))))
| ~ spl34_1
| ~ spl34_16
| spl34_45
| ~ spl34_179 ),
inference(forward_subsumption_resolution,[],[f5307,f257]) ).
fof(f5318,plain,
( sK3(sK22(sK1,sK2)) = sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))
| ~ spl34_1
| ~ spl34_36
| spl34_45
| ~ spl34_179 ),
inference(forward_subsumption_resolution,[],[f5309,f257]) ).
fof(f5324,definition,
( spl34_183
<=> sK3(sK22(sK1,sK2)) = sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))) ),
introduced(definition,[new_symbols(definition,[spl34_183])],[avatar_definition]) ).
fof(f5326,plain,
( sK3(sK22(sK1,sK2)) = sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))
| ~ spl34_183 ),
inference(avatar_component_clause,[],[f5324]) ).
fof(f5357,definition,
( spl34_184
<=> in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))))) ),
introduced(definition,[new_symbols(definition,[spl34_184])],[avatar_definition]) ).
fof(f5359,plain,
( in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK24(sK2,sK3(sK22(sK1,sK2)),apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2)))))
| ~ spl34_184 ),
inference(avatar_component_clause,[],[f5357]) ).
fof(f5597,plain,
( ! [X0] :
( ~ in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),X0),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2)) )
| spl34_152 ),
inference(resolution,[],[f4275,f242]) ).
fof(f5600,plain,
( ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),X0)
| in(unordered_pair(unordered_pair(sK25(sK22(sK1,sK2),X0),sK26(sK22(sK1,sK2),X0)),singleton(sK25(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| in(sK25(sK22(sK1,sK2),X0),X0)
| ~ relation(sK22(sK1,sK2)) )
| spl34_152 ),
inference(superposition,[],[f4275,f224]) ).
fof(f5603,plain,
( ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),X0)
| in(unordered_pair(unordered_pair(sK25(sK22(sK1,sK2),X0),sK26(sK22(sK1,sK2),X0)),singleton(sK25(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| in(sK25(sK22(sK1,sK2),X0),X0) )
| ~ spl34_92
| spl34_152 ),
inference(forward_subsumption_resolution,[],[f5600,f2343]) ).
fof(f5606,plain,
( ! [X0] : ~ in(unordered_pair(unordered_pair(sK3(sK22(sK1,sK2)),X0),singleton(sK3(sK22(sK1,sK2)))),sK22(sK1,sK2))
| ~ spl34_92
| spl34_152 ),
inference(forward_subsumption_resolution,[],[f5597,f2343]) ).
fof(f5608,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK25(sK22(sK1,sK2),X0)),unordered_pair(sK25(sK22(sK1,sK2),X0),sK26(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| in(sK25(sK22(sK1,sK2),X0),X0) )
| ~ spl34_92
| spl34_152 ),
inference(forward_demodulation,[],[f5603,f173]) ).
fof(f5611,plain,
( ! [X0] : ~ in(unordered_pair(singleton(sK3(sK22(sK1,sK2))),unordered_pair(sK3(sK22(sK1,sK2)),X0)),sK22(sK1,sK2))
| ~ spl34_92
| spl34_152 ),
inference(forward_demodulation,[],[f5606,f173]) ).
fof(f5612,plain,
( spl34_150
| ~ spl34_92
| spl34_152 ),
inference(avatar_split_clause,[],[f5611,f4274,f2341,f4105]) ).
fof(f5628,definition,
( spl34_187
<=> ! [X0] :
( in(unordered_pair(singleton(sK25(sK22(sK1,sK2),X0)),unordered_pair(sK25(sK22(sK1,sK2),X0),sK26(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| in(sK25(sK22(sK1,sK2),X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_187])],[avatar_definition]) ).
fof(f5629,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK25(sK22(sK1,sK2),X0)),unordered_pair(sK25(sK22(sK1,sK2),X0),sK26(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| ~ in(sK3(sK22(sK1,sK2)),X0)
| in(sK25(sK22(sK1,sK2),X0),X0) )
| ~ spl34_187 ),
inference(avatar_component_clause,[],[f5628]) ).
fof(f5630,plain,
( spl34_187
| ~ spl34_92
| spl34_152 ),
inference(avatar_split_clause,[],[f5608,f4274,f2341,f5628]) ).
fof(f5638,plain,
( ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),X0)
| in(sK25(sK22(sK1,sK2),X0),X0)
| in(sK25(sK22(sK1,sK2),X0),sK1) )
| ~ spl34_90
| ~ spl34_187 ),
inference(resolution,[],[f5629,f2309]) ).
fof(f5659,definition,
( spl34_188
<=> ! [X0] :
( ~ in(sK3(sK22(sK1,sK2)),X0)
| in(sK25(sK22(sK1,sK2),X0),X0)
| in(sK25(sK22(sK1,sK2),X0),sK1) ) ),
introduced(definition,[new_symbols(definition,[spl34_188])],[avatar_definition]) ).
fof(f5660,plain,
( ! [X0] :
( in(sK25(sK22(sK1,sK2),X0),sK1)
| in(sK25(sK22(sK1,sK2),X0),X0)
| ~ in(sK3(sK22(sK1,sK2)),X0) )
| ~ spl34_188 ),
inference(avatar_component_clause,[],[f5659]) ).
fof(f5661,plain,
( spl34_188
| ~ spl34_90
| ~ spl34_187 ),
inference(avatar_split_clause,[],[f5638,f5628,f2308,f5659]) ).
fof(f5668,plain,
( in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_188 ),
inference(factoring,[],[f5660]) ).
fof(f5818,plain,
( ~ in(sK4(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_3
| spl34_182 ),
inference(superposition,[],[f5200,f320]) ).
fof(f6280,definition,
( spl34_207
<=> ! [X0] :
( ~ in(X0,sK25(sK22(sK1,sK2),sK1))
| in(sK23(sK2,X0,sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1)) ) ),
introduced(definition,[new_symbols(definition,[spl34_207])],[avatar_definition]) ).
fof(f6281,plain,
( ! [X0] :
( in(sK23(sK2,X0,sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1))
| ~ in(X0,sK25(sK22(sK1,sK2),sK1)) )
| ~ spl34_207 ),
inference(avatar_component_clause,[],[f6280]) ).
fof(f6282,plain,
( spl34_207
| spl34_45
| ~ spl34_46
| ~ spl34_61
| ~ spl34_73 ),
inference(avatar_split_clause,[],[f4141,f1795,f1349,f1044,f1040,f6280]) ).
fof(f6335,definition,
( spl34_210
<=> ! [X0] :
( ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1))
| ~ in(X0,sK1)
| ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),sK8(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl34_210])],[avatar_definition]) ).
fof(f6336,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),sK8(X0))
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1)) )
| ~ spl34_210 ),
inference(avatar_component_clause,[],[f6335]) ).
fof(f6337,plain,
( spl34_210
| ~ spl34_46
| ~ spl34_73
| ~ spl34_144 ),
inference(avatar_split_clause,[],[f4134,f3764,f1795,f1044,f6335]) ).
fof(f6338,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1))
| ~ in(X0,sK1) )
| ~ spl34_3
| ~ spl34_210 ),
inference(superposition,[],[f6336,f320]) ).
fof(f6339,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1)) )
| ~ spl34_3
| ~ spl34_210 ),
inference(duplicate_literal_removal,[],[f6338]) ).
fof(f6714,definition,
( spl34_223
<=> ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1)) ) ),
introduced(definition,[new_symbols(definition,[spl34_223])],[avatar_definition]) ).
fof(f6715,plain,
( ! [X0] :
( ~ in(sK23(sK2,sK7(X0),sK25(sK22(sK1,sK2),sK1)),X0)
| ~ in(X0,sK1)
| ~ in(sK7(X0),sK25(sK22(sK1,sK2),sK1)) )
| ~ spl34_223 ),
inference(avatar_component_clause,[],[f6714]) ).
fof(f6716,plain,
( spl34_223
| ~ spl34_3
| ~ spl34_210 ),
inference(avatar_split_clause,[],[f6339,f6335,f319,f6714]) ).
fof(f6723,plain,
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ in(sK7(sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1))
| ~ in(sK7(sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1))
| ~ spl34_207
| ~ spl34_223 ),
inference(resolution,[],[f6715,f6281]) ).
fof(f6735,plain,
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ in(sK7(sK25(sK22(sK1,sK2),sK1)),sK25(sK22(sK1,sK2),sK1))
| ~ spl34_207
| ~ spl34_223 ),
inference(duplicate_literal_removal,[],[f6723]) ).
fof(f6747,plain,
( ~ in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ spl34_10
| ~ spl34_207
| ~ spl34_223 ),
inference(forward_subsumption_resolution,[],[f6735,f417]) ).
fof(f6757,plain,
( $false
| ~ spl34_10
| ~ spl34_46
| ~ spl34_207
| ~ spl34_223 ),
inference(forward_subsumption_resolution,[],[f6747,f1046]) ).
fof(f6758,plain,
( ~ spl34_10
| ~ spl34_46
| ~ spl34_207
| ~ spl34_223 ),
inference(avatar_contradiction_clause,[],[f6757]) ).
fof(f6778,plain,
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| spl34_46
| ~ spl34_188 ),
inference(forward_subsumption_resolution,[],[f5668,f1045]) ).
fof(f6784,plain,
( $false
| ~ spl34_44
| spl34_46
| ~ spl34_188 ),
inference(forward_subsumption_resolution,[],[f6778,f1038]) ).
fof(f6785,plain,
( ~ spl34_44
| spl34_46
| ~ spl34_188 ),
inference(avatar_contradiction_clause,[],[f6784]) ).
fof(f6801,plain,
( ~ in(sK3(sK22(sK1,sK2)),sK1)
| ~ spl34_3
| ~ spl34_77
| spl34_182 ),
inference(forward_subsumption_resolution,[],[f5818,f1948]) ).
fof(f6808,plain,
( $false
| ~ spl34_3
| ~ spl34_44
| ~ spl34_77
| spl34_182 ),
inference(forward_subsumption_resolution,[],[f6801,f1038]) ).
fof(f6809,plain,
( ~ spl34_3
| ~ spl34_44
| ~ spl34_77
| spl34_182 ),
inference(avatar_contradiction_clause,[],[f6808]) ).
fof(f6825,plain,
( sK1 = relation_dom(sK22(sK1,sK2))
| in(unordered_pair(unordered_pair(sK25(sK22(sK1,sK2),sK1),sK26(sK22(sK1,sK2),sK1)),singleton(sK25(sK22(sK1,sK2),sK1))),sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| spl34_46 ),
inference(resolution,[],[f1045,f224]) ).
fof(f6826,plain,
( in(unordered_pair(unordered_pair(sK25(sK22(sK1,sK2),sK1),sK26(sK22(sK1,sK2),sK1)),singleton(sK25(sK22(sK1,sK2),sK1))),sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2))
| spl34_46
| spl34_72 ),
inference(forward_subsumption_resolution,[],[f6825,f1792]) ).
fof(f6827,plain,
( in(unordered_pair(unordered_pair(sK25(sK22(sK1,sK2),sK1),sK26(sK22(sK1,sK2),sK1)),singleton(sK25(sK22(sK1,sK2),sK1))),sK22(sK1,sK2))
| spl34_46
| spl34_72
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f6826,f2343]) ).
fof(f6828,plain,
( in(unordered_pair(singleton(sK25(sK22(sK1,sK2),sK1)),unordered_pair(sK25(sK22(sK1,sK2),sK1),sK26(sK22(sK1,sK2),sK1))),sK22(sK1,sK2))
| spl34_46
| spl34_72
| ~ spl34_92 ),
inference(forward_demodulation,[],[f6827,f173]) ).
fof(f6848,definition,
( spl34_224
<=> in(unordered_pair(singleton(sK25(sK22(sK1,sK2),sK1)),unordered_pair(sK25(sK22(sK1,sK2),sK1),sK26(sK22(sK1,sK2),sK1))),sK22(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_224])],[avatar_definition]) ).
fof(f6850,plain,
( in(unordered_pair(singleton(sK25(sK22(sK1,sK2),sK1)),unordered_pair(sK25(sK22(sK1,sK2),sK1),sK26(sK22(sK1,sK2),sK1))),sK22(sK1,sK2))
| ~ spl34_224 ),
inference(avatar_component_clause,[],[f6848]) ).
fof(f6851,plain,
( spl34_224
| spl34_46
| spl34_72
| ~ spl34_92 ),
inference(avatar_split_clause,[],[f6828,f2341,f1791,f1044,f6848]) ).
fof(f6868,plain,
( spl34_183
| ~ spl34_1
| ~ spl34_36
| spl34_45
| ~ spl34_179 ),
inference(avatar_split_clause,[],[f5318,f5052,f1040,f858,f255,f5324]) ).
fof(f6869,plain,
( spl34_184
| ~ spl34_1
| ~ spl34_16
| spl34_45
| ~ spl34_179 ),
inference(avatar_split_clause,[],[f5317,f5052,f1040,f498,f255,f5357]) ).
fof(f6870,plain,
( in(apply(sK22(sK1,sK2),sK3(sK22(sK1,sK2))),sK3(sK22(sK1,sK2)))
| ~ spl34_183
| ~ spl34_184 ),
inference(forward_demodulation,[],[f5359,f5326]) ).
fof(f6879,plain,
( in(sK25(sK22(sK1,sK2),sK1),sK1)
| ~ spl34_90
| ~ spl34_224 ),
inference(resolution,[],[f6850,f2309]) ).
fof(f6906,plain,
( $false
| spl34_46
| ~ spl34_90
| ~ spl34_224 ),
inference(forward_subsumption_resolution,[],[f6879,f1045]) ).
fof(f6907,plain,
( spl34_46
| ~ spl34_90
| ~ spl34_224 ),
inference(avatar_contradiction_clause,[],[f6906]) ).
fof(f6933,plain,
( ! [X0] :
( ~ in(X0,sK17(sK1,sK2))
| in(unordered_pair(unordered_pair(sK19(sK1,sK2),X0),singleton(sK19(sK1,sK2))),sK2) )
| ~ spl34_45
| ~ spl34_71 ),
inference(forward_subsumption_resolution,[],[f1835,f1042]) ).
fof(f6965,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK19(sK1,sK2)),unordered_pair(sK19(sK1,sK2),X0)),sK2)
| ~ in(X0,sK17(sK1,sK2)) )
| ~ spl34_45
| ~ spl34_71 ),
inference(forward_demodulation,[],[f6933,f173]) ).
fof(f6994,plain,
( $false
| spl34_78
| ~ spl34_183
| ~ spl34_184 ),
inference(forward_subsumption_resolution,[],[f6870,f1952]) ).
fof(f6995,plain,
( spl34_78
| ~ spl34_183
| ~ spl34_184 ),
inference(avatar_contradiction_clause,[],[f6994]) ).
fof(f7023,definition,
( spl34_225
<=> ! [X0] :
( in(unordered_pair(singleton(sK19(sK1,sK2)),unordered_pair(sK19(sK1,sK2),X0)),sK2)
| ~ in(X0,sK17(sK1,sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl34_225])],[avatar_definition]) ).
fof(f7024,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK19(sK1,sK2)),unordered_pair(sK19(sK1,sK2),X0)),sK2)
| ~ in(X0,sK17(sK1,sK2)) )
| ~ spl34_225 ),
inference(avatar_component_clause,[],[f7023]) ).
fof(f7025,plain,
( spl34_225
| ~ spl34_45
| ~ spl34_71 ),
inference(avatar_split_clause,[],[f6965,f1728,f1040,f7023]) ).
fof(f7031,plain,
( ! [X0,X1] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(X1,X0)
| in(sK5(X1,X0),X0)
| ~ in(sK19(sK1,sK2),X0) )
| ~ spl34_9
| ~ spl34_225 ),
inference(resolution,[],[f7024,f385]) ).
fof(f7032,plain,
( ! [X0,X1] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK5(X1,X0))),sK2)
| sK19(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(X1,X0)
| ~ in(sK19(sK1,sK2),X0) )
| ~ spl34_5
| ~ spl34_225 ),
inference(resolution,[],[f7024,f328]) ).
fof(f7060,plain,
( ! [X0] :
( ~ in(X0,sK1)
| in(unordered_pair(unordered_pair(X0,sK27(sK22(sK1,sK2),X0)),singleton(X0)),sK22(sK1,sK2))
| ~ relation(sK22(sK1,sK2)) )
| ~ spl34_72 ),
inference(superposition,[],[f243,f1793]) ).
fof(f7067,plain,
( ! [X0] :
( ~ in(X0,sK1)
| in(unordered_pair(unordered_pair(X0,sK27(sK22(sK1,sK2),X0)),singleton(X0)),sK22(sK1,sK2)) )
| ~ spl34_72
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f7060,f2343]) ).
fof(f7073,plain,
( ! [X0] :
( in(unordered_pair(singleton(X0),unordered_pair(X0,sK27(sK22(sK1,sK2),X0))),sK22(sK1,sK2))
| ~ in(X0,sK1) )
| ~ spl34_72
| ~ spl34_92 ),
inference(forward_demodulation,[],[f7067,f173]) ).
fof(f7082,plain,
( in(sK18(sK1,sK2),sK20(sK1,sK2))
| ~ spl34_45 ),
inference(resolution,[],[f1042,f159]) ).
fof(f7083,plain,
( sK17(sK1,sK2) = sK20(sK1,sK2)
| ~ spl34_45 ),
inference(resolution,[],[f1042,f160]) ).
fof(f7084,plain,
( in(sK17(sK1,sK2),sK1)
| ~ spl34_45 ),
inference(resolution,[],[f1042,f161]) ).
fof(f7085,plain,
( sK19(sK1,sK2) != sK18(sK1,sK2)
| ~ spl34_45 ),
inference(resolution,[],[f1042,f162]) ).
fof(f7086,plain,
( ! [X0] :
( in(unordered_pair(unordered_pair(sK18(sK1,sK2),X0),singleton(sK18(sK1,sK2))),sK2)
| ~ in(X0,sK20(sK1,sK2)) )
| ~ spl34_45 ),
inference(resolution,[],[f1042,f212]) ).
fof(f7089,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK18(sK1,sK2)),unordered_pair(sK18(sK1,sK2),X0)),sK2)
| ~ in(X0,sK20(sK1,sK2)) )
| ~ spl34_45 ),
inference(forward_demodulation,[],[f7086,f173]) ).
fof(f7090,plain,
( in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_45 ),
inference(forward_demodulation,[],[f7082,f7083]) ).
fof(f7093,plain,
( ! [X0] :
( ~ in(X0,sK17(sK1,sK2))
| in(unordered_pair(singleton(sK18(sK1,sK2)),unordered_pair(sK18(sK1,sK2),X0)),sK2) )
| ~ spl34_45 ),
inference(forward_demodulation,[],[f7089,f7083]) ).
fof(f7106,definition,
( spl34_227
<=> in(sK18(sK1,sK2),sK17(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl34_227])],[avatar_definition]) ).
fof(f7108,plain,
( in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_227 ),
inference(avatar_component_clause,[],[f7106]) ).
fof(f7109,plain,
( spl34_227
| ~ spl34_45 ),
inference(avatar_split_clause,[],[f7090,f1040,f7106]) ).
fof(f7115,definition,
( spl34_228
<=> in(sK17(sK1,sK2),sK1) ),
introduced(definition,[new_symbols(definition,[spl34_228])],[avatar_definition]) ).
fof(f7117,plain,
( in(sK17(sK1,sK2),sK1)
| ~ spl34_228 ),
inference(avatar_component_clause,[],[f7115]) ).
fof(f7118,plain,
( spl34_228
| ~ spl34_45 ),
inference(avatar_split_clause,[],[f7084,f1040,f7115]) ).
fof(f7120,definition,
( spl34_229
<=> ! [X0] :
( ~ in(X0,sK17(sK1,sK2))
| in(unordered_pair(singleton(sK18(sK1,sK2)),unordered_pair(sK18(sK1,sK2),X0)),sK2) ) ),
introduced(definition,[new_symbols(definition,[spl34_229])],[avatar_definition]) ).
fof(f7121,plain,
( ! [X0] :
( in(unordered_pair(singleton(sK18(sK1,sK2)),unordered_pair(sK18(sK1,sK2),X0)),sK2)
| ~ in(X0,sK17(sK1,sK2)) )
| ~ spl34_229 ),
inference(avatar_component_clause,[],[f7120]) ).
fof(f7122,plain,
( spl34_229
| ~ spl34_45 ),
inference(avatar_split_clause,[],[f7093,f1040,f7120]) ).
fof(f7126,plain,
( ! [X0,X1] :
( ~ in(sK5(sK18(sK1,sK2),X0),sK17(sK1,sK2))
| sK18(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(sK18(sK1,sK2),X0)
| ~ in(X1,X0)
| in(sK6(X1,X0),X0) )
| ~ spl34_8
| ~ spl34_229 ),
inference(resolution,[],[f7121,f375]) ).
fof(f7146,definition,
( spl34_230
<=> sK19(sK1,sK2) = sK18(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl34_230])],[avatar_definition]) ).
fof(f7148,plain,
( sK19(sK1,sK2) != sK18(sK1,sK2)
| spl34_230 ),
inference(avatar_component_clause,[],[f7146]) ).
fof(f7149,plain,
( ~ spl34_230
| ~ spl34_45 ),
inference(avatar_split_clause,[],[f7085,f1040,f7146]) ).
fof(f7508,definition,
( spl34_247
<=> ! [X0,X1] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK5(X1,X0))),sK2)
| sK19(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(X1,X0)
| ~ in(sK19(sK1,sK2),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_247])],[avatar_definition]) ).
fof(f7509,plain,
( ! [X0,X1] :
( ~ in(unordered_pair(singleton(X1),unordered_pair(X1,sK5(X1,X0))),sK2)
| ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(X1,X0)
| ~ in(sK19(sK1,sK2),X0) )
| ~ spl34_247 ),
inference(avatar_component_clause,[],[f7508]) ).
fof(f7510,plain,
( spl34_247
| ~ spl34_5
| ~ spl34_225 ),
inference(avatar_split_clause,[],[f7032,f7023,f327,f7508]) ).
fof(f7516,definition,
( spl34_249
<=> ! [X0,X1] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(X1,X0)
| in(sK5(X1,X0),X0)
| ~ in(sK19(sK1,sK2),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_249])],[avatar_definition]) ).
fof(f7517,plain,
( ! [X0,X1] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(X1,X0)
| in(sK5(X1,X0),X0)
| ~ in(sK19(sK1,sK2),X0) )
| ~ spl34_249 ),
inference(avatar_component_clause,[],[f7516]) ).
fof(f7518,plain,
( spl34_249
| ~ spl34_9
| ~ spl34_225 ),
inference(avatar_split_clause,[],[f7031,f7023,f384,f7516]) ).
fof(f7519,plain,
( ! [X0,X1] :
( sK19(sK1,sK2) = X0
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(X0,sK17(sK1,sK2))
| in(sK5(X0,sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(X1,sK17(sK1,sK2))
| in(sK5(X1,sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1 )
| ~ spl34_17
| ~ spl34_249 ),
inference(resolution,[],[f7517,f510]) ).
fof(f7520,plain,
( ! [X0,X1] :
( sK19(sK1,sK2) = X0
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(X0,sK17(sK1,sK2))
| in(sK5(X0,sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| ~ in(X1,sK17(sK1,sK2))
| in(sK5(X1,sK17(sK1,sK2)),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1 )
| ~ spl34_17
| ~ spl34_249 ),
inference(duplicate_literal_removal,[],[f7519]) ).
fof(f7521,plain,
( ! [X0,X1] :
( sK19(sK1,sK2) = X0
| ~ in(X0,sK17(sK1,sK2))
| in(sK5(X0,sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| ~ in(X1,sK17(sK1,sK2))
| in(sK5(X1,sK17(sK1,sK2)),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1 )
| ~ spl34_17
| ~ spl34_228
| ~ spl34_249 ),
inference(forward_subsumption_resolution,[],[f7520,f7117]) ).
fof(f7522,plain,
( ! [X0,X1] :
( sK19(sK1,sK2) = X0
| ~ in(X0,sK17(sK1,sK2))
| in(sK5(X0,sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ in(X1,sK17(sK1,sK2))
| in(sK5(X1,sK17(sK1,sK2)),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1 )
| ~ spl34_17
| ~ spl34_75
| ~ spl34_228
| ~ spl34_249 ),
inference(forward_subsumption_resolution,[],[f7521,f1843]) ).
fof(f7534,plain,
( ! [X0] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| sK19(sK1,sK2) = sK18(sK1,sK2)
| ~ in(X0,sK1)
| ~ in(sK18(sK1,sK2),X0)
| ~ in(sK19(sK1,sK2),X0)
| ~ in(sK5(sK18(sK1,sK2),X0),sK17(sK1,sK2)) )
| ~ spl34_229
| ~ spl34_247 ),
inference(resolution,[],[f7509,f7121]) ).
fof(f7539,plain,
( ! [X0] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK18(sK1,sK2),X0)
| ~ in(sK19(sK1,sK2),X0)
| ~ in(sK5(sK18(sK1,sK2),X0),sK17(sK1,sK2)) )
| ~ spl34_229
| spl34_230
| ~ spl34_247 ),
inference(forward_subsumption_resolution,[],[f7534,f7148]) ).
fof(f7835,definition,
( spl34_279
<=> ! [X1] :
( ~ in(X1,sK17(sK1,sK2))
| sK19(sK1,sK2) = X1
| in(sK5(X1,sK17(sK1,sK2)),sK17(sK1,sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl34_279])],[avatar_definition]) ).
fof(f7836,plain,
( ! [X1] :
( in(sK5(X1,sK17(sK1,sK2)),sK17(sK1,sK2))
| sK19(sK1,sK2) = X1
| ~ in(X1,sK17(sK1,sK2)) )
| ~ spl34_279 ),
inference(avatar_component_clause,[],[f7835]) ).
fof(f11198,definition,
( spl34_423
<=> ! [X0,X1] :
( ~ in(sK5(sK18(sK1,sK2),X0),sK17(sK1,sK2))
| sK18(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(sK18(sK1,sK2),X0)
| ~ in(X1,X0)
| in(sK6(X1,X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_423])],[avatar_definition]) ).
fof(f11199,plain,
( ! [X0,X1] :
( ~ in(sK5(sK18(sK1,sK2),X0),sK17(sK1,sK2))
| sK18(sK1,sK2) = X1
| ~ in(X0,sK1)
| ~ in(sK18(sK1,sK2),X0)
| ~ in(X1,X0)
| in(sK6(X1,X0),X0) )
| ~ spl34_423 ),
inference(avatar_component_clause,[],[f11198]) ).
fof(f11200,plain,
( spl34_423
| ~ spl34_8
| ~ spl34_229 ),
inference(avatar_split_clause,[],[f7126,f7120,f374,f11198]) ).
fof(f11207,plain,
( spl34_117
| ~ spl34_72
| ~ spl34_92 ),
inference(avatar_split_clause,[],[f7073,f2341,f1791,f2963]) ).
fof(f11734,definition,
( spl34_448
<=> ! [X0] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK18(sK1,sK2),X0)
| ~ in(sK19(sK1,sK2),X0)
| ~ in(sK5(sK18(sK1,sK2),X0),sK17(sK1,sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl34_448])],[avatar_definition]) ).
fof(f11735,plain,
( ! [X0] :
( ~ in(sK6(sK19(sK1,sK2),X0),sK17(sK1,sK2))
| ~ in(X0,sK1)
| ~ in(sK18(sK1,sK2),X0)
| ~ in(sK19(sK1,sK2),X0)
| ~ in(sK5(sK18(sK1,sK2),X0),sK17(sK1,sK2)) )
| ~ spl34_448 ),
inference(avatar_component_clause,[],[f11734]) ).
fof(f11736,plain,
( spl34_448
| ~ spl34_229
| spl34_230
| ~ spl34_247 ),
inference(avatar_split_clause,[],[f7539,f7508,f7146,f7120,f11734]) ).
fof(f14057,plain,
( spl34_279
| spl34_279
| ~ spl34_17
| ~ spl34_75
| ~ spl34_228
| ~ spl34_249 ),
inference(avatar_split_clause,[],[f7522,f7516,f7115,f1841,f509,f7835,f7835]) ).
fof(f14063,plain,
( ! [X0] :
( sK19(sK1,sK2) = sK18(sK1,sK2)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| sK18(sK1,sK2) = X0
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ in(X0,sK17(sK1,sK2))
| in(sK6(X0,sK17(sK1,sK2)),sK17(sK1,sK2)) )
| ~ spl34_279
| ~ spl34_423 ),
inference(resolution,[],[f7836,f11199]) ).
fof(f14072,plain,
( ! [X0] :
( sK19(sK1,sK2) = sK18(sK1,sK2)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| sK18(sK1,sK2) = X0
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(X0,sK17(sK1,sK2))
| in(sK6(X0,sK17(sK1,sK2)),sK17(sK1,sK2)) )
| ~ spl34_279
| ~ spl34_423 ),
inference(duplicate_literal_removal,[],[f14063]) ).
fof(f14078,plain,
( ! [X0] :
( ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| sK18(sK1,sK2) = X0
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(X0,sK17(sK1,sK2))
| in(sK6(X0,sK17(sK1,sK2)),sK17(sK1,sK2)) )
| spl34_230
| ~ spl34_279
| ~ spl34_423 ),
inference(forward_subsumption_resolution,[],[f14072,f7148]) ).
fof(f14082,plain,
( ! [X0] :
( sK18(sK1,sK2) = X0
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(X0,sK17(sK1,sK2))
| in(sK6(X0,sK17(sK1,sK2)),sK17(sK1,sK2)) )
| ~ spl34_227
| spl34_230
| ~ spl34_279
| ~ spl34_423 ),
inference(forward_subsumption_resolution,[],[f14078,f7108]) ).
fof(f14087,plain,
( ! [X0] :
( sK18(sK1,sK2) = X0
| ~ in(X0,sK17(sK1,sK2))
| in(sK6(X0,sK17(sK1,sK2)),sK17(sK1,sK2)) )
| ~ spl34_227
| ~ spl34_228
| spl34_230
| ~ spl34_279
| ~ spl34_423 ),
inference(forward_subsumption_resolution,[],[f14082,f7117]) ).
fof(f14700,definition,
( spl34_564
<=> ! [X0] :
( sK18(sK1,sK2) = X0
| ~ in(X0,sK17(sK1,sK2))
| in(sK6(X0,sK17(sK1,sK2)),sK17(sK1,sK2)) ) ),
introduced(definition,[new_symbols(definition,[spl34_564])],[avatar_definition]) ).
fof(f14701,plain,
( ! [X0] :
( in(sK6(X0,sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ in(X0,sK17(sK1,sK2))
| sK18(sK1,sK2) = X0 )
| ~ spl34_564 ),
inference(avatar_component_clause,[],[f14700]) ).
fof(f14702,plain,
( spl34_564
| ~ spl34_227
| ~ spl34_228
| spl34_230
| ~ spl34_279
| ~ spl34_423 ),
inference(avatar_split_clause,[],[f14087,f11198,f7835,f7146,f7115,f7106,f14700]) ).
fof(f14705,plain,
( ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| sK19(sK1,sK2) = sK18(sK1,sK2)
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| ~ in(sK5(sK18(sK1,sK2),sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ spl34_448
| ~ spl34_564 ),
inference(resolution,[],[f14701,f11735]) ).
fof(f14726,plain,
( ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| sK19(sK1,sK2) = sK18(sK1,sK2)
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ in(sK5(sK18(sK1,sK2),sK17(sK1,sK2)),sK17(sK1,sK2))
| ~ spl34_448
| ~ spl34_564 ),
inference(duplicate_literal_removal,[],[f14705]) ).
fof(f14733,plain,
( ~ in(sK19(sK1,sK2),sK17(sK1,sK2))
| sK19(sK1,sK2) = sK18(sK1,sK2)
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_279
| ~ spl34_448
| ~ spl34_564 ),
inference(forward_subsumption_resolution,[],[f14726,f7836]) ).
fof(f14736,plain,
( sK19(sK1,sK2) = sK18(sK1,sK2)
| ~ in(sK17(sK1,sK2),sK1)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_75
| ~ spl34_279
| ~ spl34_448
| ~ spl34_564 ),
inference(forward_subsumption_resolution,[],[f14733,f1843]) ).
fof(f14738,plain,
( ~ in(sK17(sK1,sK2),sK1)
| ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_75
| spl34_230
| ~ spl34_279
| ~ spl34_448
| ~ spl34_564 ),
inference(forward_subsumption_resolution,[],[f14736,f7148]) ).
fof(f14739,plain,
( ~ in(sK18(sK1,sK2),sK17(sK1,sK2))
| ~ spl34_75
| ~ spl34_228
| spl34_230
| ~ spl34_279
| ~ spl34_448
| ~ spl34_564 ),
inference(forward_subsumption_resolution,[],[f14738,f7117]) ).
fof(f14740,plain,
( $false
| ~ spl34_75
| ~ spl34_227
| ~ spl34_228
| spl34_230
| ~ spl34_279
| ~ spl34_448
| ~ spl34_564 ),
inference(forward_subsumption_resolution,[],[f14739,f7108]) ).
fof(f14741,plain,
( ~ spl34_75
| ~ spl34_227
| ~ spl34_228
| spl34_230
| ~ spl34_279
| ~ spl34_448
| ~ spl34_564 ),
inference(avatar_contradiction_clause,[],[f14740]) ).
cnf(s1,plain,
spl34_1,
inference(sat_conversion,[],[f258]) ).
cnf(s2,plain,
~ spl34_2,
inference(sat_conversion,[],[f298]) ).
cnf(s3,plain,
spl34_3,
inference(sat_conversion,[],[f321]) ).
cnf(s4,plain,
spl34_4,
inference(sat_conversion,[],[f325]) ).
cnf(s5,plain,
spl34_5,
inference(sat_conversion,[],[f329]) ).
cnf(s6,plain,
spl34_6,
inference(sat_conversion,[],[f341]) ).
cnf(s7,plain,
spl34_7,
inference(sat_conversion,[],[f366]) ).
cnf(s8,plain,
spl34_8,
inference(sat_conversion,[],[f376]) ).
cnf(s9,plain,
spl34_9,
inference(sat_conversion,[],[f386]) ).
cnf(s10,plain,
( ~ spl34_3
| ~ spl34_4
| spl34_10 ),
inference(sat_conversion,[],[f418]) ).
cnf(s11,plain,
spl34_11,
inference(sat_conversion,[],[f452]) ).
cnf(s12,plain,
spl34_12,
inference(sat_conversion,[],[f462]) ).
cnf(s16,plain,
( spl34_2
| spl34_16 ),
inference(sat_conversion,[],[f500]) ).
cnf(s17,plain,
spl34_17,
inference(sat_conversion,[],[f511]) ).
cnf(s35,plain,
( spl34_2
| spl34_36 ),
inference(sat_conversion,[],[f860]) ).
cnf(s36,plain,
( ~ spl34_12
| spl34_37 ),
inference(sat_conversion,[],[f871]) ).
cnf(s37,plain,
( ~ spl34_37
| spl34_38 ),
inference(sat_conversion,[],[f876]) ).
cnf(s41,plain,
( ~ spl34_1
| spl34_42 ),
inference(sat_conversion,[],[f997]) ).
cnf(s42,plain,
( ~ spl34_1
| ~ spl34_38
| ~ spl34_42
| spl34_43 ),
inference(sat_conversion,[],[f1011]) ).
cnf(s43,plain,
( spl34_2
| ~ spl34_43
| spl34_44
| spl34_45
| spl34_46 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s45,plain,
( ~ spl34_11
| spl34_48 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s46,plain,
( ~ spl34_48
| spl34_49 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s50,plain,
( spl34_2
| spl34_53 ),
inference(sat_conversion,[],[f1157]) ).
cnf(s58,plain,
( ~ spl34_1
| spl34_61 ),
inference(sat_conversion,[],[f1351]) ).
cnf(s68,plain,
( ~ spl34_45
| spl34_71 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s69,plain,
( ~ spl34_1
| spl34_2
| spl34_45
| ~ spl34_46
| spl34_72
| spl34_73 ),
inference(sat_conversion,[],[f1797]) ).
cnf(s71,plain,
( ~ spl34_45
| ~ spl34_71
| spl34_75 ),
inference(sat_conversion,[],[f1844]) ).
cnf(s73,plain,
( ~ spl34_1
| spl34_2
| ~ spl34_11
| spl34_45
| ~ spl34_72
| spl34_77
| ~ spl34_78 ),
inference(sat_conversion,[],[f1953]) ).
cnf(s75,plain,
( ~ spl34_1
| spl34_2
| ~ spl34_7
| spl34_45
| ~ spl34_72
| ~ spl34_78
| ~ spl34_80 ),
inference(sat_conversion,[],[f1994]) ).
cnf(s82,plain,
( ~ spl34_1
| spl34_2
| spl34_45
| spl34_87 ),
inference(sat_conversion,[],[f2192]) ).
cnf(s85,plain,
( ~ spl34_1
| spl34_2
| spl34_45
| spl34_90 ),
inference(sat_conversion,[],[f2310]) ).
cnf(s87,plain,
( ~ spl34_1
| spl34_2
| spl34_45
| spl34_92 ),
inference(sat_conversion,[],[f2344]) ).
cnf(s139,plain,
( ~ spl34_1
| ~ spl34_6
| spl34_45
| ~ spl34_53
| spl34_144 ),
inference(sat_conversion,[],[f3766]) ).
cnf(s146,plain,
( ~ spl34_12
| spl34_44
| ~ spl34_72
| ~ spl34_87
| ~ spl34_92 ),
inference(sat_conversion,[],[f3999]) ).
cnf(s152,plain,
( ~ spl34_46
| ~ spl34_49
| spl34_77
| ~ spl34_78
| ~ spl34_87
| ~ spl34_92
| ~ spl34_117 ),
inference(sat_conversion,[],[f4206]) ).
cnf(s153,plain,
( ~ spl34_44
| ~ spl34_117
| ~ spl34_150 ),
inference(sat_conversion,[],[f4241]) ).
cnf(s160,plain,
( spl34_80
| ~ spl34_87
| ~ spl34_92
| spl34_156 ),
inference(sat_conversion,[],[f4314]) ).
cnf(s167,plain,
( ~ spl34_44
| ~ spl34_144
| ~ spl34_156
| spl34_163 ),
inference(sat_conversion,[],[f4493]) ).
cnf(s168,plain,
( ~ spl34_6
| ~ spl34_163
| spl34_164 ),
inference(sat_conversion,[],[f4510]) ).
cnf(s169,plain,
( ~ spl34_3
| ~ spl34_164
| spl34_165 ),
inference(sat_conversion,[],[f4524]) ).
cnf(s175,plain,
( ~ spl34_1
| ~ spl34_10
| ~ spl34_44
| ~ spl34_77
| ~ spl34_165
| spl34_170 ),
inference(sat_conversion,[],[f4680]) ).
cnf(s179,plain,
( ~ spl34_44
| spl34_45
| ~ spl34_156
| ~ spl34_170
| ~ spl34_174 ),
inference(sat_conversion,[],[f4809]) ).
cnf(s187,plain,
( ~ spl34_87
| ~ spl34_92
| ~ spl34_152
| spl34_179 ),
inference(sat_conversion,[],[f5055]) ).
cnf(s192,plain,
( ~ spl34_6
| ~ spl34_44
| spl34_174
| ~ spl34_182 ),
inference(sat_conversion,[],[f5201]) ).
cnf(s211,plain,
( ~ spl34_92
| spl34_150
| spl34_152 ),
inference(sat_conversion,[],[f5612]) ).
cnf(s212,plain,
( ~ spl34_92
| spl34_152
| spl34_187 ),
inference(sat_conversion,[],[f5630]) ).
cnf(s213,plain,
( ~ spl34_90
| ~ spl34_187
| spl34_188 ),
inference(sat_conversion,[],[f5661]) ).
cnf(s234,plain,
( spl34_45
| ~ spl34_46
| ~ spl34_61
| ~ spl34_73
| spl34_207 ),
inference(sat_conversion,[],[f6282]) ).
cnf(s237,plain,
( ~ spl34_46
| ~ spl34_73
| ~ spl34_144
| spl34_210 ),
inference(sat_conversion,[],[f6337]) ).
cnf(s263,plain,
( ~ spl34_3
| ~ spl34_210
| spl34_223 ),
inference(sat_conversion,[],[f6716]) ).
cnf(s264,plain,
( ~ spl34_10
| ~ spl34_46
| ~ spl34_207
| ~ spl34_223 ),
inference(sat_conversion,[],[f6758]) ).
cnf(s265,plain,
( ~ spl34_44
| spl34_46
| ~ spl34_188 ),
inference(sat_conversion,[],[f6785]) ).
cnf(s269,plain,
( ~ spl34_3
| ~ spl34_44
| ~ spl34_77
| spl34_182 ),
inference(sat_conversion,[],[f6809]) ).
cnf(s274,plain,
( spl34_46
| spl34_72
| ~ spl34_92
| spl34_224 ),
inference(sat_conversion,[],[f6851]) ).
cnf(s275,plain,
( ~ spl34_1
| ~ spl34_36
| spl34_45
| ~ spl34_179
| spl34_183 ),
inference(sat_conversion,[],[f6868]) ).
cnf(s276,plain,
( ~ spl34_1
| ~ spl34_16
| spl34_45
| ~ spl34_179
| spl34_184 ),
inference(sat_conversion,[],[f6869]) ).
cnf(s277,plain,
( spl34_46
| ~ spl34_90
| ~ spl34_224 ),
inference(sat_conversion,[],[f6907]) ).
cnf(s283,plain,
( spl34_78
| ~ spl34_183
| ~ spl34_184 ),
inference(sat_conversion,[],[f6995]) ).
cnf(s291,plain,
( ~ spl34_45
| ~ spl34_71
| spl34_225 ),
inference(sat_conversion,[],[f7025]) ).
cnf(s293,plain,
( ~ spl34_45
| spl34_227 ),
inference(sat_conversion,[],[f7109]) ).
cnf(s294,plain,
( ~ spl34_45
| spl34_228 ),
inference(sat_conversion,[],[f7118]) ).
cnf(s295,plain,
( ~ spl34_45
| spl34_229 ),
inference(sat_conversion,[],[f7122]) ).
cnf(s296,plain,
( ~ spl34_45
| ~ spl34_230 ),
inference(sat_conversion,[],[f7149]) ).
cnf(s318,plain,
( ~ spl34_5
| ~ spl34_225
| spl34_247 ),
inference(sat_conversion,[],[f7510]) ).
cnf(s320,plain,
( ~ spl34_9
| ~ spl34_225
| spl34_249 ),
inference(sat_conversion,[],[f7518]) ).
cnf(s483,plain,
( ~ spl34_8
| ~ spl34_229
| spl34_423 ),
inference(sat_conversion,[],[f11200]) ).
cnf(s485,plain,
( ~ spl34_72
| ~ spl34_92
| spl34_117 ),
inference(sat_conversion,[],[f11207]) ).
cnf(s511,plain,
( ~ spl34_229
| spl34_230
| ~ spl34_247
| spl34_448 ),
inference(sat_conversion,[],[f11736]) ).
cnf(s605,plain,
( spl34_279
| ~ spl34_75
| ~ spl34_228
| ~ spl34_249
| ~ spl34_17
| spl34_279 ),
inference(sat_conversion,[],[f14057]) ).
cnf(s606,plain,
( ~ spl34_17
| ~ spl34_75
| ~ spl34_228
| ~ spl34_249
| spl34_279 ),
inference(rat,[],[s605]) ).
cnf(s627,plain,
( ~ spl34_227
| ~ spl34_228
| spl34_230
| ~ spl34_279
| ~ spl34_423
| spl34_564 ),
inference(sat_conversion,[],[f14702]) ).
cnf(s628,plain,
( ~ spl34_75
| ~ spl34_227
| ~ spl34_228
| spl34_230
| ~ spl34_279
| ~ spl34_448
| ~ spl34_564 ),
inference(sat_conversion,[],[f14741]) ).
cnf(s665,plain,
spl34_37,
inference(rat,[],[s36,s12]) ).
cnf(s667,plain,
spl34_38,
inference(rat,[],[s37,s665]) ).
cnf(s672,plain,
spl34_48,
inference(rat,[],[s45,s11]) ).
cnf(s674,plain,
spl34_49,
inference(rat,[],[s46,s672]) ).
cnf(s703,plain,
spl34_10,
inference(rat,[],[s10,s4,s3]) ).
cnf(s717,plain,
spl34_53,
inference(rat,[],[s50,s2]) ).
cnf(s718,plain,
spl34_36,
inference(rat,[],[s35,s2]) ).
cnf(s720,plain,
spl34_16,
inference(rat,[],[s16,s2]) ).
cnf(s753,plain,
spl34_61,
inference(rat,[],[s58,s1]) ).
cnf(s755,plain,
spl34_42,
inference(rat,[],[s41,s1]) ).
cnf(s784,plain,
spl34_43,
inference(rat,[],[s42,s1,s667,s755]) ).
cnf(s836,plain,
( spl34_45
| spl34_44 ),
inference(rat,[],[s264,s263,s234,s237,s69,s146,s43,s82,s87,s139,s703,s3,s753,s2,s1,s12,s784,s6,s717]) ).
cnf(s837,plain,
~ spl34_45,
inference(rat,[],[s628,s627,s511,s606,s318,s320,s71,s291,s483,s68,s293,s294,s295,s296,s17,s5,s9,s8]) ).
cnf(s839,plain,
spl34_144,
inference(rat,[],[s139,s1,s717,s6,s837]) ).
cnf(s840,plain,
spl34_92,
inference(rat,[],[s87,s1,s2,s837]) ).
cnf(s841,plain,
spl34_90,
inference(rat,[],[s85,s1,s2,s837]) ).
cnf(s842,plain,
spl34_87,
inference(rat,[],[s82,s1,s2,s837]) ).
cnf(s843,plain,
spl34_44,
inference(rat,[],[s836,s837]) ).
cnf(s894,plain,
( ~ spl34_73
| ~ spl34_46 ),
inference(rat,[],[s264,s263,s234,s237,s839,s837,s753,s3,s703]) ).
cnf(s895,plain,
( spl34_73
| ~ spl34_46 ),
inference(rat,[],[s175,s169,s179,s168,s192,s167,s269,s160,s152,s75,s283,s275,s276,s187,s211,s153,s485,s69,s720,s718,s2,s7,s674,s842,s840,s839,s6,s837,s3,s843,s1,s703]) ).
cnf(s896,plain,
~ spl34_46,
inference(rat,[],[s895,s894]) ).
cnf(s897,plain,
~ spl34_224,
inference(rat,[],[s277,s841,s896]) ).
cnf(s898,plain,
spl34_72,
inference(rat,[],[s274,s897,s840,s896]) ).
cnf(s899,plain,
~ spl34_188,
inference(rat,[],[s265,s843,s896]) ).
cnf(s907,plain,
~ spl34_187,
inference(rat,[],[s213,s841,s899]) ).
cnf(s922,plain,
spl34_152,
inference(rat,[],[s212,s840,s907]) ).
cnf(s939,plain,
spl34_179,
inference(rat,[],[s187,s842,s840,s922]) ).
cnf(s951,plain,
spl34_184,
inference(rat,[],[s276,s837,s1,s720,s939]) ).
cnf(s952,plain,
spl34_183,
inference(rat,[],[s275,s837,s1,s718,s939]) ).
cnf(s962,plain,
spl34_78,
inference(rat,[],[s283,s951,s952]) ).
cnf(s971,plain,
~ spl34_80,
inference(rat,[],[s75,s898,s837,s1,s2,s7,s962]) ).
cnf(s972,plain,
spl34_77,
inference(rat,[],[s73,s898,s837,s1,s2,s11,s962]) ).
cnf(s977,plain,
spl34_156,
inference(rat,[],[s160,s842,s840,s971]) ).
cnf(s978,plain,
spl34_182,
inference(rat,[],[s269,s843,s3,s972]) ).
cnf(s980,plain,
spl34_163,
inference(rat,[],[s167,s843,s839,s977]) ).
cnf(s982,plain,
spl34_174,
inference(rat,[],[s192,s843,s6,s978]) ).
cnf(s984,plain,
spl34_164,
inference(rat,[],[s168,s6,s980]) ).
cnf(s985,plain,
~ spl34_170,
inference(rat,[],[s179,s977,s843,s837,s982]) ).
cnf(s986,plain,
spl34_165,
inference(rat,[],[s169,s3,s984]) ).
cnf(s987,plain,
$false,
inference(rat,[],[s175,s972,s843,s1,s703,s985,s986]) ).
fof(f14742,plain,
$false,
inference(avatar_sat_refutation,[],[s987]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU288+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 28 04:31:33 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.58/2.35 % (1555109)Detected formulas, will run a generic FOF schedule.
% 10.58/2.35 % (1555117)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=874131431:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.58/2.35 % (1555115)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=50705464:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.58/2.35 % (1555116)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=240603029:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.58/2.35 % (1555119)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3540005600:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.58/2.35 % (1555114)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1687834785:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.58/2.35 % (1555117)Instruction limit reached!
% 10.58/2.35 % (1555117)------------------------------
% 10.58/2.35 % (1555117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.58/2.35 % (1555117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.58/2.35 % (1555117)CaDiCaL version: 2.1.3
% 10.58/2.35 % (1555117)Termination reason: Instruction limit
% 10.58/2.35 % (1555117)Termination phase: Saturation
% 10.58/2.35 % (1555117)Time elapsed: 0.038 s
% 10.58/2.35 % (1555117)Peak memory usage: 89 MB
% 10.58/2.35 % (1555117)Instructions burned: 112 (million)
% 10.58/2.35 % (1555118)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1391051165:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.58/2.35 % (1555120)dis-21_1_sil=8000:lcm=predicate:random_seed=3858884723:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.58/2.35 % (1555119)Instruction limit reached!
% 10.58/2.35 % (1555119)------------------------------
% 10.58/2.35 % (1555119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.58/2.35 % (1555119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.58/2.35 % (1555119)CaDiCaL version: 2.1.3
% 10.58/2.35 % (1555119)Termination reason: Instruction limit
% 10.58/2.35 % (1555119)Termination phase: Saturation
% 10.58/2.35 % (1555119)Time elapsed: 0.058 s
% 10.58/2.35 % (1555119)Peak memory usage: 90 MB
% 10.58/2.35 % (1555119)Instructions burned: 143 (million)
% 10.58/2.35 % (1555120)Instruction limit reached!
% 10.58/2.35 % (1555120)------------------------------
% 10.58/2.35 % (1555120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.58/2.35 % (1555120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.58/2.35 % (1555120)CaDiCaL version: 2.1.3
% 10.58/2.35 % (1555120)Termination reason: Instruction limit
% 10.58/2.35 % (1555120)Termination phase: Saturation
% 10.58/2.35 % (1555120)Time elapsed: 0.076 s
% 10.58/2.35 % (1555120)Peak memory usage: 90 MB
% 10.58/2.35 % (1555120)Instructions burned: 129 (million)
% 10.58/2.35 % (1555118)Instruction limit reached!
% 10.58/2.35 % (1555118)------------------------------
% 10.58/2.35 % (1555118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.58/2.35 % (1555118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.58/2.35 % (1555118)CaDiCaL version: 2.1.3
% 10.58/2.35 % (1555118)Termination reason: Instruction limit
% 10.58/2.35 % (1555118)Termination phase: Saturation
% 10.58/2.35 % (1555118)Time elapsed: 0.077 s
% 10.58/2.35 % (1555118)Peak memory usage: 89 MB
% 10.58/2.35 % (1555118)Instructions burned: 120 (million)
% 10.58/2.35 % (1555128)lrs+10_1_sil=8000:sp=occurrence:random_seed=1085805751:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.58/2.35 % (1555129)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2177342331:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.58/2.35 % (1555129)Refutation not found, incomplete strategy
% 10.58/2.35 % (1555129)------------------------------
% 10.58/2.35 % (1555129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.58/2.35 % (1555129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.58/2.35 % (1555129)CaDiCaL version: 2.1.3
% 10.58/2.35 % (1555129)Termination reason: Refutation not found, incomplete strategy
% 18.33/3.40 % (1555129)Time elapsed: 0.007 s
% 18.33/3.40 % (1555129)Peak memory usage: 89 MB
% 18.33/3.40 % (1555129)Instructions burned: 20 (million)
% 18.33/3.40 % (1555130)lrs+1011_1_sil=32000:sp=occurrence:random_seed=417957359:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 18.33/3.40 % (1555131)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1894689824:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 18.33/3.40 % (1555129)------------------------------
% 18.33/3.40 % (1555129)------------------------------
% 18.33/3.40 % (1555128)Instruction limit reached!
% 18.33/3.40 % (1555128)------------------------------
% 18.33/3.40 % (1555128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.40 % (1555128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.40 % (1555128)CaDiCaL version: 2.1.3
% 18.33/3.40 % (1555128)Termination reason: Instruction limit
% 18.33/3.40 % (1555128)Termination phase: Saturation
% 18.33/3.40 % (1555128)Time elapsed: 0.179 s
% 18.33/3.40 % (1555128)Peak memory usage: 92 MB
% 18.33/3.40 % (1555128)Instructions burned: 285 (million)
% 18.33/3.40 % (1555131)Instruction limit reached!
% 18.33/3.40 % (1555131)------------------------------
% 18.33/3.40 % (1555131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.40 % (1555131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.40 % (1555131)CaDiCaL version: 2.1.3
% 18.33/3.40 % (1555131)Termination reason: Instruction limit
% 18.33/3.40 % (1555131)Termination phase: Saturation
% 18.33/3.40 % (1555131)Time elapsed: 0.124 s
% 18.33/3.40 % (1555131)Peak memory usage: 89 MB
% 18.33/3.40 % (1555131)Instructions burned: 249 (million)
% 18.33/3.40 % (1555136)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3671590125:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.33/3.40 % (1555137)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2180727240:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 18.33/3.40 % (1555130)Instruction limit reached!
% 18.33/3.40 % (1555130)------------------------------
% 18.33/3.40 % (1555130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.40 % (1555130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.40 % (1555130)CaDiCaL version: 2.1.3
% 18.33/3.40 % (1555130)Termination reason: Instruction limit
% 18.33/3.40 % (1555130)Termination phase: Saturation
% 18.33/3.40 % (1555130)Time elapsed: 0.214 s
% 18.33/3.40 % (1555130)Peak memory usage: 91 MB
% 18.33/3.40 % (1555130)Instructions burned: 325 (million)
% 18.33/3.40 % (1555138)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4125083271:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 18.33/3.40 % (1555136)Instruction limit reached!
% 18.33/3.40 % (1555136)------------------------------
% 18.33/3.40 % (1555136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.40 % (1555136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.40 % (1555136)CaDiCaL version: 2.1.3
% 18.33/3.40 % (1555136)Termination reason: Instruction limit
% 18.33/3.40 % (1555136)Termination phase: Saturation
% 18.33/3.40 % (1555136)Time elapsed: 0.096 s
% 18.33/3.40 % (1555136)Peak memory usage: 90 MB
% 18.33/3.40 % (1555136)Instructions burned: 296 (million)
% 18.33/3.40 % (1555141)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3414159668:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 18.33/3.40 % (1555138)Instruction limit reached!
% 18.33/3.40 % (1555138)------------------------------
% 18.33/3.40 % (1555138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.33/3.40 % (1555138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.33/3.40 % (1555138)CaDiCaL version: 2.1.3
% 18.33/3.40 % (1555138)Termination reason: Instruction limit
% 18.33/3.40 % (1555138)Termination phase: Saturation
% 18.33/3.40 % (1555138)Time elapsed: 0.082 s
% 18.33/3.40 % (1555138)Peak memory usage: 90 MB
% 18.33/3.40 % (1555138)Instructions burned: 114 (million)
% 18.33/3.40 % (1555143)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1417392375:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 18.33/3.40 % (1555143)Instruction limit reached!
% 18.33/3.40 % (1555143)------------------------------
% 18.33/3.40 % (1555143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555143)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555143)Termination reason: Instruction limit
% 24.89/4.34 % (1555143)Termination phase: Saturation
% 24.89/4.34 % (1555143)Time elapsed: 0.031 s
% 24.89/4.34 % (1555143)Peak memory usage: 89 MB
% 24.89/4.34 % (1555143)Instructions burned: 117 (million)
% 24.89/4.34 % (1555141)Instruction limit reached!
% 24.89/4.34 % (1555141)------------------------------
% 24.89/4.34 % (1555141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555141)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555141)Termination reason: Instruction limit
% 24.89/4.34 % (1555141)Termination phase: Saturation
% 24.89/4.34 % (1555141)Time elapsed: 0.069 s
% 24.89/4.34 % (1555141)Peak memory usage: 89 MB
% 24.89/4.34 % (1555141)Instructions burned: 128 (million)
% 24.89/4.34 % (1555147)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3135633463:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 24.89/4.34 % (1555145)lrs+10_1_sil=8000:sp=occurrence:random_seed=708944002:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 24.89/4.34 % (1555148)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2511006034:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 24.89/4.34 % (1555147)Instruction limit reached!
% 24.89/4.34 % (1555147)------------------------------
% 24.89/4.34 % (1555147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555147)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555147)Termination reason: Instruction limit
% 24.89/4.34 % (1555147)Termination phase: Saturation
% 24.89/4.34 % (1555147)Time elapsed: 0.138 s
% 24.89/4.34 % (1555147)Peak memory usage: 90 MB
% 24.89/4.34 % (1555147)Instructions burned: 440 (million)
% 24.89/4.34 % (1555152)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2570463575:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 24.89/4.34 % (1555152)Instruction limit reached!
% 24.89/4.34 % (1555152)------------------------------
% 24.89/4.34 % (1555152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555152)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555152)Termination reason: Instruction limit
% 24.89/4.34 % (1555152)Termination phase: Saturation
% 24.89/4.34 % (1555152)Time elapsed: 0.040 s
% 24.89/4.34 % (1555152)Peak memory usage: 90 MB
% 24.89/4.34 % (1555152)Instructions burned: 135 (million)
% 24.89/4.34 % (1555154)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3988879793:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 24.89/4.34 % (1555145)Instruction limit reached!
% 24.89/4.34 % (1555145)------------------------------
% 24.89/4.34 % (1555145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555145)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555145)Termination reason: Instruction limit
% 24.89/4.34 % (1555145)Termination phase: Saturation
% 24.89/4.34 % (1555145)Time elapsed: 0.525 s
% 24.89/4.34 % (1555145)Peak memory usage: 98 MB
% 24.89/4.34 % (1555145)Instructions burned: 908 (million)
% 24.89/4.34 % (1555154)Instruction limit reached!
% 24.89/4.34 % (1555154)------------------------------
% 24.89/4.34 % (1555154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555154)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555154)Termination reason: Instruction limit
% 24.89/4.34 % (1555154)Termination phase: Saturation
% 24.89/4.34 % (1555154)Time elapsed: 0.170 s
% 24.89/4.34 % (1555154)Peak memory usage: 91 MB
% 24.89/4.34 % (1555154)Instructions burned: 593 (million)
% 24.89/4.34 % (1555156)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3916003458:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 24.89/4.34 % (1555157)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=816671328:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi)
% 24.89/4.34 % (1555157)Instruction limit reached!
% 24.89/4.34 % (1555157)------------------------------
% 24.89/4.34 % (1555157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555157)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555157)Termination reason: Instruction limit
% 24.89/4.34 % (1555157)Termination phase: Saturation
% 24.89/4.34 % (1555157)Time elapsed: 0.091 s
% 24.89/4.34 % (1555157)Peak memory usage: 91 MB
% 24.89/4.34 % (1555157)Instructions burned: 126 (million)
% 24.89/4.34 % (1555160)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2088495874:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 24.89/4.34 % (1555160)Instruction limit reached!
% 24.89/4.34 % (1555160)------------------------------
% 24.89/4.34 % (1555160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555160)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555160)Termination reason: Instruction limit
% 24.89/4.34 % (1555160)Termination phase: Saturation
% 24.89/4.34 % (1555160)Time elapsed: 0.079 s
% 24.89/4.34 % (1555160)Peak memory usage: 90 MB
% 24.89/4.34 % (1555160)Instructions burned: 134 (million)
% 24.89/4.34 % (1555162)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2831079816:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 24.89/4.34 % (1555162)Instruction limit reached!
% 24.89/4.34 % (1555162)------------------------------
% 24.89/4.34 % (1555162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555162)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555162)Termination reason: Instruction limit
% 24.89/4.34 % (1555162)Termination phase: Saturation
% 24.89/4.34 % (1555162)Time elapsed: 0.072 s
% 24.89/4.34 % (1555162)Peak memory usage: 89 MB
% 24.89/4.34 % (1555162)Instructions burned: 142 (million)
% 24.89/4.34 % (1555137)Instruction limit reached!
% 24.89/4.34 % (1555137)------------------------------
% 24.89/4.34 % (1555137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555137)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555137)Termination reason: Instruction limit
% 24.89/4.34 % (1555137)Termination phase: Saturation
% 24.89/4.34 % (1555137)Time elapsed: 1.521 s
% 24.89/4.34 % (1555137)Peak memory usage: 141 MB
% 24.89/4.34 % (1555137)Instructions burned: 2351 (million)
% 24.89/4.34 % (1555164)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1587314693:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 24.89/4.34 % (1555164)Refutation not found, incomplete strategy
% 24.89/4.34 % (1555164)------------------------------
% 24.89/4.34 % (1555164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555164)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555164)Termination reason: Refutation not found, incomplete strategy
% 24.89/4.34 % (1555164)Time elapsed: 0.005 s
% 24.89/4.34 % (1555164)Peak memory usage: 89 MB
% 24.89/4.34 % (1555164)Instructions burned: 6 (million)
% 24.89/4.34 % (1555165)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3128428447:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 24.89/4.34 % (1555164)------------------------------
% 24.89/4.34 % (1555164)------------------------------
% 24.89/4.34 % (1555168)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=665035252:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi)
% 24.89/4.34 % (1555168)Refutation not found, incomplete strategy
% 24.89/4.34 % (1555168)------------------------------
% 24.89/4.34 % (1555168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555168)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555168)Termination reason: Refutation not found, incomplete strategy
% 24.89/4.34 % (1555168)Time elapsed: 0.047 s
% 24.89/4.34 % (1555168)Peak memory usage: 90 MB
% 24.89/4.34 % (1555168)Instructions burned: 66 (million)
% 24.89/4.34 % (1555168)------------------------------
% 24.89/4.34 % (1555168)------------------------------
% 24.89/4.34 % (1555148)Instruction limit reached!
% 24.89/4.34 % (1555148)------------------------------
% 24.89/4.34 % (1555148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555148)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555148)Termination reason: Instruction limit
% 24.89/4.34 % (1555148)Termination phase: Saturation
% 24.89/4.34 % (1555148)Time elapsed: 1.936 s
% 24.89/4.34 % (1555148)Peak memory usage: 154 MB
% 24.89/4.34 % (1555148)Instructions burned: 5205 (million)
% 24.89/4.34 % (1555171)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1589041897:i=667:av=off:fsr=off_2971 on theBenchmark for (2971ds/667Mi)
% 24.89/4.34 % (1555170)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=601007934:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 24.89/4.34 % (1555171)Instruction limit reached!
% 24.89/4.34 % (1555171)------------------------------
% 24.89/4.34 % (1555171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555171)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555171)Termination reason: Instruction limit
% 24.89/4.34 % (1555171)Termination phase: Saturation
% 24.89/4.34 % (1555171)Time elapsed: 0.156 s
% 24.89/4.34 % (1555171)Peak memory usage: 90 MB
% 24.89/4.34 % (1555171)Instructions burned: 668 (million)
% 24.89/4.34 % (1555174)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3443953575:s2a=on:i=185:s2at=1.8:fdi=4_2969 on theBenchmark for (2969ds/185Mi)
% 24.89/4.34 % (1555116)First to succeed.
% 24.89/4.34 % (1555116)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1555109"
% 24.89/4.34 % (1555174)Instruction limit reached!
% 24.89/4.34 % (1555174)------------------------------
% 24.89/4.34 % (1555174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555174)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555174)Termination reason: Instruction limit
% 24.89/4.34 % (1555174)Termination phase: Saturation
% 24.89/4.34 % (1555174)Time elapsed: 0.062 s
% 24.89/4.34 % (1555174)Peak memory usage: 91 MB
% 24.89/4.34 % (1555174)Instructions burned: 186 (million)
% 24.89/4.34 % (1555176)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=696920714:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2967 on theBenchmark for (2967ds/193Mi)
% 24.89/4.34 % (1555176)Instruction limit reached!
% 24.89/4.34 % (1555176)------------------------------
% 24.89/4.34 % (1555176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.34 % (1555176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.34 % (1555176)CaDiCaL version: 2.1.3
% 24.89/4.34 % (1555176)Termination reason: Instruction limit
% 24.89/4.34 % (1555176)Termination phase: Saturation
% 24.89/4.34 % (1555176)Time elapsed: 0.065 s
% 24.89/4.34 % (1555176)Peak memory usage: 90 MB
% 24.89/4.34 % (1555176)Instructions burned: 197 (million)
% 24.89/4.34 % (1555116)Refutation found. Thanks to Tanya!
% 24.89/4.34 % SZS status Theorem for theBenchmark
% 24.89/4.34 % SZS output start Proof for theBenchmark
% See solution above
% 25.36/4.53 % (1555116)------------------------------
% 25.36/4.53 % (1555116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.36/4.53 % (1555116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.36/4.53 % (1555116)CaDiCaL version: 2.1.3
% 25.36/4.53 % (1555116)Termination reason: Refutation
% 25.36/4.53 % (1555116)Time elapsed: 3.085 s
% 25.36/4.53 % (1555116)Peak memory usage: 157 MB
% 25.36/4.53 % (1555116)Instructions burned: 4512 (million)
% 25.36/4.53 % (1555116)------------------------------
% 25.36/4.53 % (1555116)------------------------------
% 25.36/4.53 % (1555109)Success in time 3.504 s
% 25.36/4.53 % Vampire exiting
%------------------------------------------------------------------------------