%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU286+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:52:43 PM UTC 2026
% Result : Theorem 112.80s 16.84s
% Output : Refutation 112.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 19
% Syntax : Number of formulae : 284 ( 16 unt; 17 def)
% Number of atoms : 1302 ( 312 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 1589 ( 571 ~; 796 |; 183 &)
% ( 21 <=>; 16 =>; 0 <=; 2 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 14 prp; 0-4 aty)
% Number of functors : 19 ( 19 usr; 3 con; 0-4 aty)
% Number of variables : 535 ( 0 sgn 413 !; 122 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ! [X2] :
? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,cartesian_product2(X0,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X0)
& ? [X7] :
( X5 = X7
& in(X6,X7)
& ! [X8] :
( in(X8,X7)
=> in(ordered_pair(X6,X8),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_xboole_0__e10_24__wellord2__1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ! [X2] :
? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,cartesian_product2(X0,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X0)
& ? [X7] :
( X5 = X7
& in(X6,X7)
& ! [X8] :
( in(X8,X7)
=> in(ordered_pair(X6,X8),X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f20,axiom,
! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ! [X2] :
( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X0)
& ? [X8] :
( X6 = X8
& in(X7,X8)
& ! [X9] :
( in(X9,X8)
=> in(ordered_pair(X7,X9),X1) ) ) )
& X3 = X5
& ? [X10,X11] :
( ordered_pair(X10,X11) = X5
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(X13,X12)
=> in(ordered_pair(X11,X13),X1) ) ) ) )
=> X4 = X5 )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(X5,cartesian_product2(X0,X2))
& X5 = X4
& ? [X14,X15] :
( ordered_pair(X14,X15) = X4
& in(X14,X0)
& ? [X16] :
( X14 = X16
& in(X15,X16)
& ! [X17] :
( in(X17,X16)
=> in(ordered_pair(X15,X17),X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_tarski__e10_24__wellord2__2) ).
fof(f21,plain,
! [X0,X1] :
( ( ~ empty(X0)
& relation(X1) )
=> ! [X2] :
( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X0)
& ? [X8] :
( X6 = X8
& in(X7,X8)
& ! [X9] :
( in(X9,X8)
=> in(ordered_pair(X7,X9),X1) ) ) )
& X3 = X5
& ? [X10,X11] :
( ordered_pair(X10,X11) = X5
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(X13,X12)
=> in(ordered_pair(X11,X13),X1) ) ) ) )
=> X4 = X5 )
=> ? [X14] :
! [X15] :
( in(X15,X14)
<=> ? [X16] :
( in(X16,cartesian_product2(X0,X2))
& X15 = X16
& ? [X17,X18] :
( ordered_pair(X17,X18) = X15
& in(X17,X0)
& ? [X19] :
( X17 = X19
& in(X18,X19)
& ! [X20] :
( in(X20,X19)
=> in(ordered_pair(X18,X20),X1) ) ) ) ) ) ) ),
inference(rectify,[],[f20]) ).
fof(f25,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(X0,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X0)
& ? [X7] :
( X5 = X7
& in(X6,X7)
& ! [X8] :
( in(ordered_pair(X6,X8),X1)
| ~ in(X8,X7) ) ) ) ) )
& ~ empty(X0)
& relation(X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f26,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(X0,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X0)
& ? [X7] :
( X5 = X7
& in(X6,X7)
& ! [X8] :
( in(ordered_pair(X6,X8),X1)
| ~ in(X8,X7) ) ) ) ) )
& ~ empty(X0)
& relation(X1) ),
inference(flattening,[],[f25]) ).
fof(f35,plain,
! [X0,X1] :
( ! [X2] :
( ? [X14] :
! [X15] :
( in(X15,X14)
<=> ? [X16] :
( in(X16,cartesian_product2(X0,X2))
& X15 = X16
& ? [X17,X18] :
( ordered_pair(X17,X18) = X15
& in(X17,X0)
& ? [X19] :
( X17 = X19
& in(X18,X19)
& ! [X20] :
( in(ordered_pair(X18,X20),X1)
| ~ in(X20,X19) ) ) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X0)
& ? [X8] :
( X6 = X8
& in(X7,X8)
& ! [X9] :
( in(ordered_pair(X7,X9),X1)
| ~ in(X9,X8) ) ) )
& X3 = X5
& ? [X10,X11] :
( ordered_pair(X10,X11) = X5
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) ) ) )
| empty(X0)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f36,plain,
! [X0,X1] :
( ! [X2] :
( ? [X14] :
! [X15] :
( in(X15,X14)
<=> ? [X16] :
( in(X16,cartesian_product2(X0,X2))
& X15 = X16
& ? [X17,X18] :
( ordered_pair(X17,X18) = X15
& in(X17,X0)
& ? [X19] :
( X17 = X19
& in(X18,X19)
& ! [X20] :
( in(ordered_pair(X18,X20),X1)
| ~ in(X20,X19) ) ) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X0)
& ? [X8] :
( X6 = X8
& in(X7,X8)
& ! [X9] :
( in(ordered_pair(X7,X9),X1)
| ~ in(X9,X8) ) ) )
& X3 = X5
& ? [X10,X11] :
( ordered_pair(X10,X11) = X5
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) ) ) )
| empty(X0)
| ~ relation(X1) ),
inference(flattening,[],[f35]) ).
fof(f37,definition,
! [X5,X0,X1] :
( ? [X10,X11] :
( ordered_pair(X10,X11) = X5
& in(X10,X0)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X1)
| ~ in(X13,X12) ) ) )
| ~ sP0(X5,X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X4,X0,X1] :
( ? [X6,X7] :
( ordered_pair(X6,X7) = X4
& in(X6,X0)
& ? [X8] :
( X6 = X8
& in(X7,X8)
& ! [X9] :
( in(ordered_pair(X7,X9),X1)
| ~ in(X9,X8) ) ) )
| ~ sP1(X4,X0,X1) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X2,X0,X15,X1] :
( sP2(X2,X0,X15,X1)
<=> ? [X16] :
( in(X16,cartesian_product2(X0,X2))
& X15 = X16
& ? [X17,X18] :
( ordered_pair(X17,X18) = X15
& in(X17,X0)
& ? [X19] :
( X17 = X19
& in(X18,X19)
& ! [X20] :
( in(ordered_pair(X18,X20),X1)
| ~ in(X20,X19) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X1,X0,X2] :
( ? [X14] :
! [X15] :
( in(X15,X14)
<=> sP2(X2,X0,X15,X1) )
| ~ sP3(X1,X0,X2) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f41,plain,
! [X0,X1] :
( ! [X2] :
( sP3(X1,X0,X2)
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& sP1(X4,X0,X1)
& X3 = X5
& sP0(X5,X0,X1) ) )
| empty(X0)
| ~ relation(X1) ),
inference(definition_folding,[],[f36,f40,f39,f38,f37]) ).
fof(f42,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X0,X2))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(X5,X0)
| ! [X7] :
( X5 != X7
| ~ in(X6,X7)
| ? [X8] :
( ~ in(ordered_pair(X6,X8),X1)
& in(X8,X7) ) ) )
| ~ in(X4,X3) )
& ( ( in(X4,cartesian_product2(X0,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X0)
& ? [X7] :
( X5 = X7
& in(X6,X7)
& ! [X8] :
( in(ordered_pair(X6,X8),X1)
| ~ in(X8,X7) ) ) ) )
| in(X4,X3) ) )
& ~ empty(X0)
& relation(X1) ),
inference(nnf_transformation,[],[f26]) ).
fof(f43,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X0,X2))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(X5,X0)
| ! [X7] :
( X5 != X7
| ~ in(X6,X7)
| ? [X8] :
( ~ in(ordered_pair(X6,X8),X1)
& in(X8,X7) ) ) )
| ~ in(X4,X3) )
& ( ( in(X4,cartesian_product2(X0,X2))
& ? [X5,X6] :
( ordered_pair(X5,X6) = X4
& in(X5,X0)
& ? [X7] :
( X5 = X7
& in(X6,X7)
& ! [X8] :
( in(ordered_pair(X6,X8),X1)
| ~ in(X8,X7) ) ) ) )
| in(X4,X3) ) )
& ~ empty(X0)
& relation(X1) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
? [X0,X1] :
( ? [X2] :
! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X0,X2))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(X5,X0)
| ! [X7] :
( X5 != X7
| ~ in(X6,X7)
| ? [X8] :
( ~ in(ordered_pair(X6,X8),X1)
& in(X8,X7) ) ) )
| ~ in(X4,X3) )
& ( ( in(X4,cartesian_product2(X0,X2))
& ? [X9,X10] :
( ordered_pair(X9,X10) = X4
& in(X9,X0)
& ? [X11] :
( X9 = X11
& in(X10,X11)
& ! [X12] :
( in(ordered_pair(X10,X12),X1)
| ~ in(X12,X11) ) ) ) )
| in(X4,X3) ) )
& ~ empty(X0)
& relation(X1) ),
inference(rectify,[],[f43]) ).
fof(f45,plain,
( ! [X3] :
( ( ~ in(sK7(X3),cartesian_product2(sK4,sK6))
| ! [X5,X6] :
( ordered_pair(X5,X6) != sK7(X3)
| ~ in(X5,sK4)
| ! [X7] :
( X5 != X7
| ~ in(X6,X7)
| ( ~ in(ordered_pair(X6,sK8(X6,X7)),sK5)
& in(sK8(X6,X7),X7) ) ) )
| ~ in(sK7(X3),X3) )
& ( ( in(sK7(X3),cartesian_product2(sK4,sK6))
& sK7(X3) = ordered_pair(sK9(X3),sK10(X3))
& in(sK9(X3),sK4)
& sK9(X3) = sK11(X3)
& in(sK10(X3),sK11(X3))
& ! [X12] :
( in(ordered_pair(sK10(X3),X12),sK5)
| ~ in(X12,sK11(X3)) ) )
| in(sK7(X3),X3) ) )
& ~ empty(sK4)
& relation(sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X4,sK7(X3)),skolemize(X8,sK8(X6,X7)),skolemize(X9,sK9(X3)),skolemize(X10,sK10(X3)),skolemize(X11,sK11(X3))],[f44]) ).
fof(f54,plain,
! [X1,X0,X2] :
( ? [X14] :
! [X15] :
( ( in(X15,X14)
| ~ sP2(X2,X0,X15,X1) )
& ( sP2(X2,X0,X15,X1)
| ~ in(X15,X14) ) )
| ~ sP3(X1,X0,X2) ),
inference(nnf_transformation,[],[f40]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ? [X3] :
! [X4] :
( ( in(X4,X3)
| ~ sP2(X2,X1,X4,X0) )
& ( sP2(X2,X1,X4,X0)
| ~ in(X4,X3) ) )
| ~ sP3(X0,X1,X2) ),
inference(rectify,[],[f54]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ! [X4] :
( ( in(X4,sK20(X0,X1,X2))
| ~ sP2(X2,X1,X4,X0) )
& ( sP2(X2,X1,X4,X0)
| ~ in(X4,sK20(X0,X1,X2)) ) )
| ~ sP3(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X3,sK20(X0,X1,X2))],[f55]) ).
fof(f57,plain,
! [X2,X0,X15,X1] :
( ( sP2(X2,X0,X15,X1)
| ! [X16] :
( ~ in(X16,cartesian_product2(X0,X2))
| X15 != X16
| ! [X17,X18] :
( ordered_pair(X17,X18) != X15
| ~ in(X17,X0)
| ! [X19] :
( X17 != X19
| ~ in(X18,X19)
| ? [X20] :
( ~ in(ordered_pair(X18,X20),X1)
& in(X20,X19) ) ) ) ) )
& ( ? [X16] :
( in(X16,cartesian_product2(X0,X2))
& X15 = X16
& ? [X17,X18] :
( ordered_pair(X17,X18) = X15
& in(X17,X0)
& ? [X19] :
( X17 = X19
& in(X18,X19)
& ! [X20] :
( in(ordered_pair(X18,X20),X1)
| ~ in(X20,X19) ) ) ) )
| ~ sP2(X2,X0,X15,X1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f58,plain,
! [X0,X1,X2,X3] :
( ( sP2(X0,X1,X2,X3)
| ! [X4] :
( ~ in(X4,cartesian_product2(X1,X0))
| X2 != X4
| ! [X5,X6] :
( ordered_pair(X5,X6) != X2
| ~ in(X5,X1)
| ! [X7] :
( X5 != X7
| ~ in(X6,X7)
| ? [X8] :
( ~ in(ordered_pair(X6,X8),X3)
& in(X8,X7) ) ) ) ) )
& ( ? [X9] :
( in(X9,cartesian_product2(X1,X0))
& X2 = X9
& ? [X10,X11] :
( ordered_pair(X10,X11) = X2
& in(X10,X1)
& ? [X12] :
( X10 = X12
& in(X11,X12)
& ! [X13] :
( in(ordered_pair(X11,X13),X3)
| ~ in(X13,X12) ) ) ) )
| ~ sP2(X0,X1,X2,X3) ) ),
inference(rectify,[],[f57]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( ( sP2(X0,X1,X2,X3)
| ! [X4] :
( ~ in(X4,cartesian_product2(X1,X0))
| X2 != X4
| ! [X5,X6] :
( ordered_pair(X5,X6) != X2
| ~ in(X5,X1)
| ! [X7] :
( X5 != X7
| ~ in(X6,X7)
| ( ~ in(ordered_pair(X6,sK21(X3,X6,X7)),X3)
& in(sK21(X3,X6,X7),X7) ) ) ) ) )
& ( ( in(sK22(X0,X1,X2,X3),cartesian_product2(X1,X0))
& sK22(X0,X1,X2,X3) = X2
& ordered_pair(sK23(X1,X2,X3),sK24(X1,X2,X3)) = X2
& in(sK23(X1,X2,X3),X1)
& sK23(X1,X2,X3) = sK25(X1,X2,X3)
& in(sK24(X1,X2,X3),sK25(X1,X2,X3))
& ! [X13] :
( in(ordered_pair(sK24(X1,X2,X3),X13),X3)
| ~ in(X13,sK25(X1,X2,X3)) ) )
| ~ sP2(X0,X1,X2,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23,sK24,sK25]),skolemize(X8,sK21(X3,X6,X7)),skolemize(X9,sK22(X0,X1,X2,X3)),skolemize(X10,sK23(X1,X2,X3)),skolemize(X11,sK24(X1,X2,X3)),skolemize(X12,sK25(X1,X2,X3))],[f58]) ).
fof(f66,plain,
! [X0,X1] :
( ! [X2] :
( sP3(X1,X0,X2)
| ( sK33(X0,X1) != sK34(X0,X1)
& sK32(X0,X1) = sK33(X0,X1)
& sP1(sK33(X0,X1),X0,X1)
& sK32(X0,X1) = sK34(X0,X1)
& sP0(sK34(X0,X1),X0,X1) ) )
| empty(X0)
| ~ relation(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32,sK33,sK34]),skolemize(X3,sK32(X0,X1)),skolemize(X4,sK33(X0,X1)),skolemize(X5,sK34(X0,X1))],[f41]) ).
fof(f67,plain,
relation(sK5),
inference(cnf_transformation,[],[f45]) ).
fof(f68,plain,
~ empty(sK4),
inference(cnf_transformation,[],[f45]) ).
fof(f69,plain,
! [X3,X12] :
( in(ordered_pair(sK10(X3),X12),sK5)
| ~ in(X12,sK11(X3))
| in(sK7(X3),X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f70,plain,
! [X3] :
( in(sK10(X3),sK11(X3))
| in(sK7(X3),X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f71,plain,
! [X3] :
( in(sK7(X3),X3)
| sK9(X3) = sK11(X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f72,plain,
! [X3] :
( in(sK9(X3),sK4)
| in(sK7(X3),X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f73,plain,
! [X3] :
( in(sK7(X3),X3)
| sK7(X3) = ordered_pair(sK9(X3),sK10(X3)) ),
inference(cnf_transformation,[],[f45]) ).
fof(f74,plain,
! [X3] :
( in(sK7(X3),cartesian_product2(sK4,sK6))
| in(sK7(X3),X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f75,plain,
! [X3,X6,X7,X5] :
( ~ in(sK7(X3),cartesian_product2(sK4,sK6))
| ordered_pair(X5,X6) != sK7(X3)
| ~ in(X5,sK4)
| X5 != X7
| ~ in(X6,X7)
| in(sK8(X6,X7),X7)
| ~ in(sK7(X3),X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f76,plain,
! [X3,X6,X7,X5] :
( ~ in(sK7(X3),cartesian_product2(sK4,sK6))
| ordered_pair(X5,X6) != sK7(X3)
| ~ in(X5,sK4)
| X5 != X7
| ~ in(X6,X7)
| ~ in(ordered_pair(X6,sK8(X6,X7)),sK5)
| ~ in(sK7(X3),X3) ),
inference(cnf_transformation,[],[f45]) ).
fof(f110,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,sK20(X0,X1,X2))
| sP2(X2,X1,X4,X0)
| ~ sP3(X0,X1,X2) ),
inference(cnf_transformation,[],[f56]) ).
fof(f111,plain,
! [X2,X0,X1,X4] :
( ~ sP2(X2,X1,X4,X0)
| in(X4,sK20(X0,X1,X2))
| ~ sP3(X0,X1,X2) ),
inference(cnf_transformation,[],[f56]) ).
fof(f112,plain,
! [X2,X3,X0,X1,X13] :
( ~ in(X13,sK25(X1,X2,X3))
| in(ordered_pair(sK24(X1,X2,X3),X13),X3)
| ~ sP2(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f59]) ).
fof(f113,plain,
! [X2,X3,X0,X1] :
( ~ sP2(X0,X1,X2,X3)
| in(sK24(X1,X2,X3),sK25(X1,X2,X3)) ),
inference(cnf_transformation,[],[f59]) ).
fof(f114,plain,
! [X2,X3,X0,X1] :
( ~ sP2(X0,X1,X2,X3)
| sK23(X1,X2,X3) = sK25(X1,X2,X3) ),
inference(cnf_transformation,[],[f59]) ).
fof(f115,plain,
! [X2,X3,X0,X1] :
( ~ sP2(X0,X1,X2,X3)
| in(sK23(X1,X2,X3),X1) ),
inference(cnf_transformation,[],[f59]) ).
fof(f116,plain,
! [X2,X3,X0,X1] :
( ~ sP2(X0,X1,X2,X3)
| ordered_pair(sK23(X1,X2,X3),sK24(X1,X2,X3)) = X2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f117,plain,
! [X2,X3,X0,X1] :
( ~ sP2(X0,X1,X2,X3)
| sK22(X0,X1,X2,X3) = X2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f118,plain,
! [X2,X3,X0,X1] :
( ~ sP2(X0,X1,X2,X3)
| in(sK22(X0,X1,X2,X3),cartesian_product2(X1,X0)) ),
inference(cnf_transformation,[],[f59]) ).
fof(f119,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( sP2(X0,X1,X2,X3)
| ~ in(X4,cartesian_product2(X1,X0))
| X2 != X4
| ordered_pair(X5,X6) != X2
| ~ in(X5,X1)
| X5 != X7
| ~ in(X6,X7)
| in(sK21(X3,X6,X7),X7) ),
inference(cnf_transformation,[],[f59]) ).
fof(f120,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( sP2(X0,X1,X2,X3)
| ~ in(X4,cartesian_product2(X1,X0))
| X2 != X4
| ordered_pair(X5,X6) != X2
| ~ in(X5,X1)
| X5 != X7
| ~ in(X6,X7)
| ~ in(ordered_pair(X6,sK21(X3,X6,X7)),X3) ),
inference(cnf_transformation,[],[f59]) ).
fof(f132,plain,
! [X2,X0,X1] :
( sP3(X1,X0,X2)
| sK32(X0,X1) = sK34(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f134,plain,
! [X2,X0,X1] :
( sP3(X1,X0,X2)
| sK32(X0,X1) = sK33(X0,X1)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f135,plain,
! [X2,X0,X1] :
( sK33(X0,X1) != sK34(X0,X1)
| sP3(X1,X0,X2)
| empty(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f136,plain,
! [X3,X6,X7] :
( sK7(X3) != ordered_pair(X7,X6)
| ~ in(sK7(X3),cartesian_product2(sK4,sK6))
| ~ in(X7,sK4)
| ~ in(X6,X7)
| ~ in(ordered_pair(X6,sK8(X6,X7)),sK5)
| ~ in(sK7(X3),X3) ),
inference(equality_resolution,[],[f76]) ).
fof(f137,plain,
! [X3,X6,X7] :
( sK7(X3) != ordered_pair(X7,X6)
| ~ in(sK7(X3),cartesian_product2(sK4,sK6))
| ~ in(X7,sK4)
| ~ in(X6,X7)
| in(sK8(X6,X7),X7)
| ~ in(sK7(X3),X3) ),
inference(equality_resolution,[],[f75]) ).
fof(f138,plain,
! [X3,X0,X1,X6,X7,X4,X5] :
( sP2(X0,X1,X4,X3)
| ~ in(X4,cartesian_product2(X1,X0))
| ordered_pair(X5,X6) != X4
| ~ in(X5,X1)
| X5 != X7
| ~ in(X6,X7)
| ~ in(ordered_pair(X6,sK21(X3,X6,X7)),X3) ),
inference(equality_resolution,[],[f120]) ).
fof(f139,plain,
! [X3,X0,X1,X6,X7,X5] :
( sP2(X0,X1,ordered_pair(X5,X6),X3)
| ~ in(ordered_pair(X5,X6),cartesian_product2(X1,X0))
| ~ in(X5,X1)
| X5 != X7
| ~ in(X6,X7)
| ~ in(ordered_pair(X6,sK21(X3,X6,X7)),X3) ),
inference(equality_resolution,[],[f138]) ).
fof(f140,plain,
! [X3,X0,X1,X6,X7] :
( ~ in(ordered_pair(X6,sK21(X3,X6,X7)),X3)
| ~ in(ordered_pair(X7,X6),cartesian_product2(X1,X0))
| ~ in(X7,X1)
| ~ in(X6,X7)
| sP2(X0,X1,ordered_pair(X7,X6),X3) ),
inference(equality_resolution,[],[f139]) ).
fof(f141,plain,
! [X3,X0,X1,X6,X7,X4,X5] :
( sP2(X0,X1,X4,X3)
| ~ in(X4,cartesian_product2(X1,X0))
| ordered_pair(X5,X6) != X4
| ~ in(X5,X1)
| X5 != X7
| ~ in(X6,X7)
| in(sK21(X3,X6,X7),X7) ),
inference(equality_resolution,[],[f119]) ).
fof(f142,plain,
! [X3,X0,X1,X6,X7,X5] :
( sP2(X0,X1,ordered_pair(X5,X6),X3)
| ~ in(ordered_pair(X5,X6),cartesian_product2(X1,X0))
| ~ in(X5,X1)
| X5 != X7
| ~ in(X6,X7)
| in(sK21(X3,X6,X7),X7) ),
inference(equality_resolution,[],[f141]) ).
fof(f143,plain,
! [X3,X0,X1,X6,X7] :
( ~ in(ordered_pair(X7,X6),cartesian_product2(X1,X0))
| sP2(X0,X1,ordered_pair(X7,X6),X3)
| ~ in(X7,X1)
| ~ in(X6,X7)
| in(sK21(X3,X6,X7),X7) ),
inference(equality_resolution,[],[f142]) ).
fof(f218,plain,
! [X2,X0,X1] :
( ~ sP3(X2,X1,X0)
| sP2(X0,X1,sK7(sK20(X2,X1,X0)),X2)
| sK9(sK20(X2,X1,X0)) = sK11(sK20(X2,X1,X0)) ),
inference(resolution,[],[f110,f71]) ).
fof(f222,plain,
! [X2,X0,X1] :
( sP2(X2,X0,sK7(sK20(X1,X0,X2)),X1)
| empty(X0)
| ~ relation(X1)
| sK32(X0,X1) = sK34(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2)) ),
inference(resolution,[],[f132,f218]) ).
fof(f248,definition,
( spl35_2
<=> sK32(sK4,sK5) = sK34(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl35_2])],[avatar_definition]) ).
fof(f249,plain,
( sK32(sK4,sK5) != sK34(sK4,sK5)
| spl35_2 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f250,plain,
( sK32(sK4,sK5) = sK34(sK4,sK5)
| ~ spl35_2 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f392,plain,
! [X2,X0,X1] :
( sP2(X2,X0,sK7(sK20(X1,X0,X2)),X1)
| empty(X0)
| ~ relation(X1)
| sK32(X0,X1) = sK33(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2)) ),
inference(resolution,[],[f134,f218]) ).
fof(f455,definition,
( spl35_31
<=> sK34(sK4,sK5) = sK33(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl35_31])],[avatar_definition]) ).
fof(f456,plain,
( sK34(sK4,sK5) != sK33(sK4,sK5)
| spl35_31 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( sK34(sK4,sK5) = sK33(sK4,sK5)
| ~ spl35_31 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f513,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK34(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| in(sK22(X2,X0,sK7(sK20(X1,X0,X2)),X1),cartesian_product2(X0,X2)) ),
inference(resolution,[],[f222,f118]) ).
fof(f515,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK34(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| in(sK24(X0,sK7(sK20(X1,X0,X2)),X1),sK25(X0,sK7(sK20(X1,X0,X2)),X1)) ),
inference(resolution,[],[f222,f113]) ).
fof(f517,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK34(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| in(sK23(X0,sK7(sK20(X1,X0,X2)),X1),X0) ),
inference(resolution,[],[f222,f115]) ).
fof(f520,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK33(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| in(sK22(X2,X0,sK7(sK20(X1,X0,X2)),X1),cartesian_product2(X0,X2)) ),
inference(resolution,[],[f392,f118]) ).
fof(f521,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK33(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| sK23(X0,sK7(sK20(X1,X0,X2)),X1) = sK25(X0,sK7(sK20(X1,X0,X2)),X1) ),
inference(resolution,[],[f392,f114]) ).
fof(f522,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK33(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| in(sK24(X0,sK7(sK20(X1,X0,X2)),X1),sK25(X0,sK7(sK20(X1,X0,X2)),X1)) ),
inference(resolution,[],[f392,f113]) ).
fof(f523,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK33(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| sK7(sK20(X1,X0,X2)) = sK22(X2,X0,sK7(sK20(X1,X0,X2)),X1) ),
inference(resolution,[],[f392,f117]) ).
fof(f524,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK32(X0,X1) = sK33(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2))
| in(sK23(X0,sK7(sK20(X1,X0,X2)),X1),X0) ),
inference(resolution,[],[f392,f115]) ).
fof(f526,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK34(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| in(sK23(X0,sK7(sK20(sK5,X0,X1)),sK5),X0) ),
inference(resolution,[],[f517,f67]) ).
fof(f536,plain,
! [X0] :
( sK32(sK4,sK5) = sK34(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4) ),
inference(resolution,[],[f526,f68]) ).
fof(f650,plain,
! [X2,X0,X1] :
( ~ relation(X1)
| empty(X0)
| sK7(sK20(X1,X0,X2)) = ordered_pair(sK23(X0,sK7(sK20(X1,X0,X2)),X1),sK24(X0,sK7(sK20(X1,X0,X2)),X1))
| sK32(X0,X1) = sK33(X0,X1)
| sK9(sK20(X1,X0,X2)) = sK11(sK20(X1,X0,X2)) ),
inference(resolution,[],[f116,f392]) ).
fof(f662,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK33(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| in(sK23(X0,sK7(sK20(sK5,X0,X1)),sK5),X0) ),
inference(resolution,[],[f524,f67]) ).
fof(f672,plain,
! [X0] :
( sK32(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4) ),
inference(resolution,[],[f662,f68]) ).
fof(f675,plain,
( ! [X0] :
( sK34(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4) )
| ~ spl35_2 ),
inference(forward_demodulation,[],[f672,f250]) ).
fof(f677,definition,
( spl35_46
<=> ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4) ) ),
introduced(definition,[new_symbols(definition,[spl35_46])],[avatar_definition]) ).
fof(f678,plain,
( ! [X0] :
( in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f679,plain,
( spl35_46
| spl35_31
| ~ spl35_2 ),
inference(avatar_split_clause,[],[f675,f248,f455,f677]) ).
fof(f1418,plain,
! [X2,X3,X0,X1] :
( ~ in(sK21(sK5,sK10(X1),X0),sK11(X1))
| ~ in(X0,X2)
| ~ in(sK10(X1),X0)
| sP2(X3,X2,ordered_pair(X0,sK10(X1)),sK5)
| ~ in(ordered_pair(X0,sK10(X1)),cartesian_product2(X2,X3))
| in(sK7(X1),X1) ),
inference(resolution,[],[f140,f69]) ).
fof(f2474,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK34(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| in(sK22(X1,X0,sK7(sK20(sK5,X0,X1)),sK5),cartesian_product2(X0,X1)) ),
inference(resolution,[],[f513,f67]) ).
fof(f2484,plain,
! [X0] :
( sK32(sK4,sK5) = sK34(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5),cartesian_product2(sK4,X0)) ),
inference(resolution,[],[f2474,f68]) ).
fof(f2593,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK33(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| in(sK22(X1,X0,sK7(sK20(sK5,X0,X1)),sK5),cartesian_product2(X0,X1)) ),
inference(resolution,[],[f520,f67]) ).
fof(f2603,plain,
! [X0] :
( sK32(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5),cartesian_product2(sK4,X0)) ),
inference(resolution,[],[f2593,f68]) ).
fof(f2610,plain,
( ! [X0] :
( sK34(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5),cartesian_product2(sK4,X0)) )
| ~ spl35_2 ),
inference(forward_demodulation,[],[f2603,f250]) ).
fof(f2612,definition,
( spl35_90
<=> ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5),cartesian_product2(sK4,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl35_90])],[avatar_definition]) ).
fof(f2613,plain,
( ! [X0] :
( in(sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5),cartesian_product2(sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_90 ),
inference(avatar_component_clause,[],[f2612]) ).
fof(f2614,plain,
( spl35_90
| spl35_31
| ~ spl35_2 ),
inference(avatar_split_clause,[],[f2610,f248,f455,f2612]) ).
fof(f4223,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK33(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| sK7(sK20(sK5,X0,X1)) = sK22(X1,X0,sK7(sK20(sK5,X0,X1)),sK5) ),
inference(resolution,[],[f523,f67]) ).
fof(f4233,plain,
! [X0] :
( sK32(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK7(sK20(sK5,sK4,X0)) = sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5) ),
inference(resolution,[],[f4223,f68]) ).
fof(f4240,plain,
( ! [X0] :
( sK34(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK7(sK20(sK5,sK4,X0)) = sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5) )
| ~ spl35_2 ),
inference(forward_demodulation,[],[f4233,f250]) ).
fof(f4242,definition,
( spl35_121
<=> ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK7(sK20(sK5,sK4,X0)) = sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5) ) ),
introduced(definition,[new_symbols(definition,[spl35_121])],[avatar_definition]) ).
fof(f4243,plain,
( ! [X0] :
( sK7(sK20(sK5,sK4,X0)) = sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_121 ),
inference(avatar_component_clause,[],[f4242]) ).
fof(f4244,plain,
( spl35_121
| spl35_31
| ~ spl35_2 ),
inference(avatar_split_clause,[],[f4240,f248,f455,f4242]) ).
fof(f4246,plain,
( ! [X0] :
( in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_90
| ~ spl35_121 ),
inference(superposition,[],[f2613,f4243]) ).
fof(f4249,plain,
( ! [X0] :
( in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_90
| ~ spl35_121 ),
inference(duplicate_literal_removal,[],[f4246]) ).
fof(f7539,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK34(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| in(sK24(X0,sK7(sK20(sK5,X0,X1)),sK5),sK25(X0,sK7(sK20(sK5,X0,X1)),sK5)) ),
inference(resolution,[],[f515,f67]) ).
fof(f7549,plain,
! [X0] :
( sK32(sK4,sK5) = sK34(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) ),
inference(resolution,[],[f7539,f68]) ).
fof(f7662,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK33(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| sK23(X0,sK7(sK20(sK5,X0,X1)),sK5) = sK25(X0,sK7(sK20(sK5,X0,X1)),sK5) ),
inference(resolution,[],[f521,f67]) ).
fof(f7672,plain,
! [X0] :
( sK32(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5) = sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5) ),
inference(resolution,[],[f7662,f68]) ).
fof(f7680,plain,
( ! [X0] :
( sK34(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5) = sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5) )
| ~ spl35_2 ),
inference(forward_demodulation,[],[f7672,f250]) ).
fof(f7682,definition,
( spl35_149
<=> ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5) = sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5) ) ),
introduced(definition,[new_symbols(definition,[spl35_149])],[avatar_definition]) ).
fof(f7683,plain,
( ! [X0] :
( sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5) = sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_149 ),
inference(avatar_component_clause,[],[f7682]) ).
fof(f7684,plain,
( spl35_149
| spl35_31
| ~ spl35_2 ),
inference(avatar_split_clause,[],[f7680,f248,f455,f7682]) ).
fof(f7687,plain,
( ! [X2,X0,X1] :
( ~ in(X1,sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),X1),sK5)
| ~ sP2(X2,sK4,sK7(sK20(sK5,sK4,X0)),sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_149 ),
inference(superposition,[],[f112,f7683]) ).
fof(f8094,plain,
! [X0,X1] :
( empty(X0)
| sK32(X0,sK5) = sK33(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1))
| in(sK24(X0,sK7(sK20(sK5,X0,X1)),sK5),sK25(X0,sK7(sK20(sK5,X0,X1)),sK5)) ),
inference(resolution,[],[f522,f67]) ).
fof(f8141,plain,
! [X0] :
( sK32(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) ),
inference(resolution,[],[f8094,f68]) ).
fof(f8150,plain,
( ! [X0] :
( sK34(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) )
| ~ spl35_2 ),
inference(forward_demodulation,[],[f8141,f250]) ).
fof(f8152,definition,
( spl35_156
<=> ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) ) ),
introduced(definition,[new_symbols(definition,[spl35_156])],[avatar_definition]) ).
fof(f8153,plain,
( ! [X0] :
( in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_156 ),
inference(avatar_component_clause,[],[f8152]) ).
fof(f8154,plain,
( spl35_156
| spl35_31
| ~ spl35_2 ),
inference(avatar_split_clause,[],[f8150,f248,f455,f8152]) ).
fof(f8157,plain,
( ! [X0] :
( in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_149
| ~ spl35_156 ),
inference(superposition,[],[f8153,f7683]) ).
fof(f8158,plain,
( ! [X0] :
( in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_149
| ~ spl35_156 ),
inference(duplicate_literal_removal,[],[f8157]) ).
fof(f19259,plain,
! [X0,X1] :
( empty(X0)
| sK7(sK20(sK5,X0,X1)) = ordered_pair(sK23(X0,sK7(sK20(sK5,X0,X1)),sK5),sK24(X0,sK7(sK20(sK5,X0,X1)),sK5))
| sK32(X0,sK5) = sK33(X0,sK5)
| sK9(sK20(sK5,X0,X1)) = sK11(sK20(sK5,X0,X1)) ),
inference(resolution,[],[f650,f67]) ).
fof(f19269,plain,
! [X0] :
( sK7(sK20(sK5,sK4,X0)) = ordered_pair(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| sK32(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) ),
inference(resolution,[],[f19259,f68]) ).
fof(f19284,plain,
( ! [X0] :
( sK34(sK4,sK5) = sK33(sK4,sK5)
| sK7(sK20(sK5,sK4,X0)) = ordered_pair(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_2 ),
inference(forward_demodulation,[],[f19269,f250]) ).
fof(f19286,definition,
( spl35_186
<=> ! [X0] :
( sK7(sK20(sK5,sK4,X0)) = ordered_pair(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl35_186])],[avatar_definition]) ).
fof(f19287,plain,
( ! [X0] :
( sK7(sK20(sK5,sK4,X0)) = ordered_pair(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_186 ),
inference(avatar_component_clause,[],[f19286]) ).
fof(f19288,plain,
( spl35_186
| spl35_31
| ~ spl35_2 ),
inference(avatar_split_clause,[],[f19284,f248,f455,f19286]) ).
fof(f19290,plain,
( ! [X0,X1] :
( sK7(sK20(sK5,sK4,X0)) != sK7(X1)
| ~ in(sK7(X1),cartesian_product2(sK4,sK6))
| ~ in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4)
| ~ in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| ~ in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))),sK5)
| ~ in(sK7(X1),X1)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_186 ),
inference(superposition,[],[f136,f19287]) ).
fof(f19291,plain,
( ! [X0,X1] :
( sK7(sK20(sK5,sK4,X0)) != sK7(X1)
| ~ in(sK7(X1),cartesian_product2(sK4,sK6))
| ~ in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4)
| ~ in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5)),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| ~ in(sK7(X1),X1)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_186 ),
inference(superposition,[],[f137,f19287]) ).
fof(f19414,plain,
( ! [X0,X1] :
( sK7(sK20(sK5,sK4,X0)) != sK7(X1)
| ~ in(sK7(X1),cartesian_product2(sK4,sK6))
| ~ in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5)),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| ~ in(sK7(X1),X1)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f19291,f678]) ).
fof(f19415,plain,
( ! [X0,X1] :
( sK7(sK20(sK5,sK4,X0)) != sK7(X1)
| ~ in(sK7(X1),cartesian_product2(sK4,sK6))
| ~ in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| ~ in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))),sK5)
| ~ in(sK7(X1),X1)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f19290,f678]) ).
fof(f19416,plain,
( ! [X0,X1] :
( sK7(sK20(sK5,sK4,X0)) != sK7(X1)
| ~ in(sK7(X1),cartesian_product2(sK4,sK6))
| in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5)),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| ~ in(sK7(X1),X1)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f19414,f8158]) ).
fof(f19417,plain,
( ! [X0,X1] :
( sK7(sK20(sK5,sK4,X0)) != sK7(X1)
| ~ in(sK7(X1),cartesian_product2(sK4,sK6))
| ~ in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))),sK5)
| ~ in(sK7(X1),X1)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f19415,f8158]) ).
fof(f75344,plain,
( ! [X0] :
( ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5)),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| ~ in(sK7(sK20(sK5,sK4,X0)),sK20(sK5,sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(equality_resolution,[],[f19416]) ).
fof(f75345,plain,
( ! [X0] :
( in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5)),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f75344,f71]) ).
fof(f75347,plain,
( ! [X0,X1] :
( ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))),sK5)
| ~ sP2(X1,sK4,sK7(sK20(sK5,sK4,X0)),sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(resolution,[],[f75345,f7687]) ).
fof(f75349,plain,
( ! [X0,X1] :
( ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))),sK5)
| ~ sP2(X1,sK4,sK7(sK20(sK5,sK4,X0)),sK5) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(duplicate_literal_removal,[],[f75347]) ).
fof(f84838,plain,
( ! [X0] :
( ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| ~ in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))),sK5)
| ~ in(sK7(sK20(sK5,sK4,X0)),sK20(sK5,sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(equality_resolution,[],[f19417]) ).
fof(f84839,plain,
( ! [X0] :
( ~ in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5))),sK5)
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f84838,f71]) ).
fof(f87076,plain,
( ! [X0,X1] :
( ~ sP2(X1,sK4,sK7(sK20(sK5,sK4,X0)),sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f75349,f84839]) ).
fof(f87078,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| empty(sK4)
| ~ relation(sK5)
| sK32(sK4,sK5) = sK34(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(resolution,[],[f87076,f222]) ).
fof(f87081,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| empty(sK4)
| ~ relation(sK5)
| sK32(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(resolution,[],[f87076,f392]) ).
fof(f87129,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| empty(sK4)
| ~ relation(sK5)
| sK32(sK4,sK5) = sK33(sK4,sK5) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(duplicate_literal_removal,[],[f87081]) ).
fof(f87130,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| empty(sK4)
| ~ relation(sK5)
| sK32(sK4,sK5) = sK34(sK4,sK5) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(duplicate_literal_removal,[],[f87078]) ).
fof(f87153,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| ~ relation(sK5)
| sK32(sK4,sK5) = sK33(sK4,sK5) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f87129,f68]) ).
fof(f87177,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| sK32(sK4,sK5) = sK33(sK4,sK5) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f87153,f67]) ).
fof(f87179,plain,
( ! [X0] :
( sK34(sK4,sK5) = sK33(sK4,sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6)) )
| ~ spl35_2
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_demodulation,[],[f87177,f250]) ).
fof(f87182,definition,
( spl35_234
<=> ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6)) ) ),
introduced(definition,[new_symbols(definition,[spl35_234])],[avatar_definition]) ).
fof(f87183,plain,
( ! [X0] :
( ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_234 ),
inference(avatar_component_clause,[],[f87182]) ).
fof(f87184,plain,
( spl35_234
| spl35_31
| ~ spl35_2
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(avatar_split_clause,[],[f87179,f19286,f8152,f7682,f677,f248,f455,f87182]) ).
fof(f87189,plain,
( sK9(sK20(sK5,sK4,sK6)) = sK11(sK20(sK5,sK4,sK6))
| sK9(sK20(sK5,sK4,sK6)) = sK11(sK20(sK5,sK4,sK6))
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234 ),
inference(resolution,[],[f87183,f4249]) ).
fof(f87191,plain,
( sK9(sK20(sK5,sK4,sK6)) = sK11(sK20(sK5,sK4,sK6))
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234 ),
inference(duplicate_literal_removal,[],[f87189]) ).
fof(f87192,plain,
( ! [X2,X0,X1] :
( ~ in(sK21(sK5,sK10(sK20(sK5,sK4,sK6)),X0),sK9(sK20(sK5,sK4,sK6)))
| ~ in(X0,X1)
| ~ in(sK10(sK20(sK5,sK4,sK6)),X0)
| sP2(X2,X1,ordered_pair(X0,sK10(sK20(sK5,sK4,sK6))),sK5)
| ~ in(ordered_pair(X0,sK10(sK20(sK5,sK4,sK6))),cartesian_product2(X1,X2))
| in(sK7(sK20(sK5,sK4,sK6)),sK20(sK5,sK4,sK6)) )
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234 ),
inference(superposition,[],[f1418,f87191]) ).
fof(f87196,definition,
( spl35_235
<=> in(sK7(sK20(sK5,sK4,sK6)),sK20(sK5,sK4,sK6)) ),
introduced(definition,[new_symbols(definition,[spl35_235])],[avatar_definition]) ).
fof(f87197,plain,
( ~ in(sK7(sK20(sK5,sK4,sK6)),sK20(sK5,sK4,sK6))
| spl35_235 ),
inference(avatar_component_clause,[],[f87196]) ).
fof(f87198,plain,
( in(sK7(sK20(sK5,sK4,sK6)),sK20(sK5,sK4,sK6))
| ~ spl35_235 ),
inference(avatar_component_clause,[],[f87196]) ).
fof(f87205,definition,
( spl35_237
<=> in(sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6))) ),
introduced(definition,[new_symbols(definition,[spl35_237])],[avatar_definition]) ).
fof(f87207,plain,
( in(sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6)))
| ~ spl35_237 ),
inference(avatar_component_clause,[],[f87205]) ).
fof(f87211,plain,
( sP2(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5)
| ~ sP3(sK5,sK4,sK6)
| ~ spl35_235 ),
inference(resolution,[],[f87198,f110]) ).
fof(f87214,definition,
( spl35_238
<=> sP3(sK5,sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl35_238])],[avatar_definition]) ).
fof(f87215,plain,
( sP3(sK5,sK4,sK6)
| ~ spl35_238 ),
inference(avatar_component_clause,[],[f87214]) ).
fof(f87216,plain,
( ~ sP3(sK5,sK4,sK6)
| spl35_238 ),
inference(avatar_component_clause,[],[f87214]) ).
fof(f87218,definition,
( spl35_239
<=> sP2(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5) ),
introduced(definition,[new_symbols(definition,[spl35_239])],[avatar_definition]) ).
fof(f87219,plain,
( ~ sP2(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5)
| spl35_239 ),
inference(avatar_component_clause,[],[f87218]) ).
fof(f87220,plain,
( sP2(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5)
| ~ spl35_239 ),
inference(avatar_component_clause,[],[f87218]) ).
fof(f87221,plain,
( ~ spl35_238
| spl35_239
| ~ spl35_235 ),
inference(avatar_split_clause,[],[f87211,f87196,f87218,f87214]) ).
fof(f87225,plain,
( sK32(sK4,sK5) = sK33(sK4,sK5)
| spl35_238 ),
inference(unit_resulting_resolution,[],[f134,f67,f68,f87216]) ).
fof(f87226,plain,
( sK34(sK4,sK5) != sK33(sK4,sK5)
| spl35_238 ),
inference(unit_resulting_resolution,[],[f135,f67,f68,f87216]) ).
fof(f87303,plain,
( sK34(sK4,sK5) = sK33(sK4,sK5)
| ~ spl35_2
| spl35_238 ),
inference(superposition,[],[f87225,f250]) ).
fof(f87305,plain,
( ~ spl35_31
| spl35_238 ),
inference(avatar_split_clause,[],[f87226,f87214,f455]) ).
fof(f87306,plain,
( $false
| ~ spl35_2
| spl35_31
| spl35_238 ),
inference(forward_subsumption_resolution,[],[f87303,f456]) ).
fof(f87307,plain,
( ~ spl35_2
| spl35_31
| spl35_238 ),
inference(avatar_contradiction_clause,[],[f87306]) ).
fof(f87313,plain,
( in(sK9(sK20(sK5,sK4,sK6)),sK4)
| spl35_235 ),
inference(unit_resulting_resolution,[],[f72,f87197]) ).
fof(f87315,plain,
( in(sK7(sK20(sK5,sK4,sK6)),cartesian_product2(sK4,sK6))
| spl35_235 ),
inference(unit_resulting_resolution,[],[f74,f87197]) ).
fof(f87319,plain,
( ~ sP2(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5)
| spl35_235
| ~ spl35_238 ),
inference(unit_resulting_resolution,[],[f111,f87215,f87197]) ).
fof(f87333,plain,
( ~ spl35_239
| spl35_235
| ~ spl35_238 ),
inference(avatar_split_clause,[],[f87319,f87214,f87196,f87218]) ).
fof(f94245,plain,
( in(sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,sK6)),sK5))
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f113,f87220]) ).
fof(f94246,plain,
( sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5) = sK25(sK4,sK7(sK20(sK5,sK4,sK6)),sK5)
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f114,f87220]) ).
fof(f94247,plain,
( in(sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK4)
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f115,f87220]) ).
fof(f94248,plain,
( sK7(sK20(sK5,sK4,sK6)) = ordered_pair(sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5))
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f116,f87220]) ).
fof(f94249,plain,
( sK7(sK20(sK5,sK4,sK6)) = sK22(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5)
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f117,f87220]) ).
fof(f94250,plain,
( in(sK22(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5),cartesian_product2(sK4,sK6))
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f118,f87220]) ).
fof(f94285,plain,
( in(sK7(sK20(sK5,sK4,sK6)),cartesian_product2(sK4,sK6))
| ~ spl35_239 ),
inference(superposition,[],[f94250,f94249]) ).
fof(f94315,plain,
( in(sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5))
| ~ spl35_239 ),
inference(superposition,[],[f94245,f94246]) ).
fof(f94377,plain,
( ~ in(ordered_pair(sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK8(sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5))),sK5)
| ~ spl35_235
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f136,f94285,f87198,f94247,f94315,f94248]) ).
fof(f94378,plain,
( in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5)),sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5))
| ~ spl35_235
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f137,f94285,f87198,f94247,f94315,f94248]) ).
fof(f98547,plain,
( ~ in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5)),sK25(sK4,sK7(sK20(sK5,sK4,sK6)),sK5))
| ~ spl35_235
| ~ spl35_239 ),
inference(unit_resulting_resolution,[],[f112,f87220,f94377]) ).
fof(f98548,plain,
( ~ in(sK8(sK24(sK4,sK7(sK20(sK5,sK4,sK6)),sK5),sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5)),sK23(sK4,sK7(sK20(sK5,sK4,sK6)),sK5))
| ~ spl35_235
| ~ spl35_239 ),
inference(forward_demodulation,[],[f98547,f94246]) ).
fof(f98549,plain,
( $false
| ~ spl35_235
| ~ spl35_239 ),
inference(forward_subsumption_resolution,[],[f98548,f94378]) ).
fof(f98550,plain,
( ~ spl35_235
| ~ spl35_239 ),
inference(avatar_contradiction_clause,[],[f98549]) ).
fof(f99815,plain,
( in(sK10(sK20(sK5,sK4,sK6)),sK11(sK20(sK5,sK4,sK6)))
| spl35_235 ),
inference(unit_resulting_resolution,[],[f70,f87197]) ).
fof(f99816,plain,
( sK9(sK20(sK5,sK4,sK6)) = sK11(sK20(sK5,sK4,sK6))
| spl35_235 ),
inference(unit_resulting_resolution,[],[f71,f87197]) ).
fof(f99818,plain,
( sK7(sK20(sK5,sK4,sK6)) = ordered_pair(sK9(sK20(sK5,sK4,sK6)),sK10(sK20(sK5,sK4,sK6)))
| spl35_235 ),
inference(unit_resulting_resolution,[],[f73,f87197]) ).
fof(f99847,plain,
( ! [X2,X0,X1] :
( ~ in(sK7(sK20(sK5,sK4,sK6)),cartesian_product2(X0,X1))
| sP2(X1,X0,sK7(sK20(sK5,sK4,sK6)),X2)
| ~ in(sK9(sK20(sK5,sK4,sK6)),X0)
| ~ in(sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6)))
| in(sK21(X2,sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6))),sK9(sK20(sK5,sK4,sK6))) )
| spl35_235 ),
inference(superposition,[],[f143,f99818]) ).
fof(f100848,plain,
( ! [X2,X0,X1] :
( ~ in(sK7(sK20(sK5,sK4,sK6)),cartesian_product2(X0,X1))
| sP2(X1,X0,sK7(sK20(sK5,sK4,sK6)),X2)
| ~ in(sK9(sK20(sK5,sK4,sK6)),X0)
| in(sK21(X2,sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6))),sK9(sK20(sK5,sK4,sK6))) )
| spl35_235
| ~ spl35_237 ),
inference(forward_subsumption_resolution,[],[f99847,f87207]) ).
fof(f105548,plain,
( in(sK21(sK5,sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6))),sK9(sK20(sK5,sK4,sK6)))
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(unit_resulting_resolution,[],[f100848,f87313,f87219,f87315]) ).
fof(f136035,plain,
( ! [X2,X0,X1] :
( ~ in(sK21(sK5,sK10(sK20(sK5,sK4,sK6)),X0),sK9(sK20(sK5,sK4,sK6)))
| ~ in(X0,X1)
| ~ in(sK10(sK20(sK5,sK4,sK6)),X0)
| sP2(X2,X1,ordered_pair(X0,sK10(sK20(sK5,sK4,sK6))),sK5)
| ~ in(ordered_pair(X0,sK10(sK20(sK5,sK4,sK6))),cartesian_product2(X1,X2)) )
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235 ),
inference(forward_subsumption_resolution,[],[f87192,f87197]) ).
fof(f136036,plain,
( ! [X0,X1] :
( ~ in(sK9(sK20(sK5,sK4,sK6)),X0)
| ~ in(sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6)))
| sP2(X1,X0,ordered_pair(sK9(sK20(sK5,sK4,sK6)),sK10(sK20(sK5,sK4,sK6))),sK5)
| ~ in(ordered_pair(sK9(sK20(sK5,sK4,sK6)),sK10(sK20(sK5,sK4,sK6))),cartesian_product2(X0,X1)) )
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(resolution,[],[f136035,f105548]) ).
fof(f136051,plain,
( ! [X0,X1] :
( ~ in(sK9(sK20(sK5,sK4,sK6)),X0)
| sP2(X1,X0,ordered_pair(sK9(sK20(sK5,sK4,sK6)),sK10(sK20(sK5,sK4,sK6))),sK5)
| ~ in(ordered_pair(sK9(sK20(sK5,sK4,sK6)),sK10(sK20(sK5,sK4,sK6))),cartesian_product2(X0,X1)) )
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(forward_subsumption_resolution,[],[f136036,f87207]) ).
fof(f136059,plain,
( ! [X0,X1] :
( sP2(X1,X0,sK7(sK20(sK5,sK4,sK6)),sK5)
| ~ in(sK9(sK20(sK5,sK4,sK6)),X0)
| ~ in(ordered_pair(sK9(sK20(sK5,sK4,sK6)),sK10(sK20(sK5,sK4,sK6))),cartesian_product2(X0,X1)) )
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(forward_demodulation,[],[f136051,f99818]) ).
fof(f136067,plain,
( ! [X0,X1] :
( ~ in(sK7(sK20(sK5,sK4,sK6)),cartesian_product2(X0,X1))
| sP2(X1,X0,sK7(sK20(sK5,sK4,sK6)),sK5)
| ~ in(sK9(sK20(sK5,sK4,sK6)),X0) )
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(forward_demodulation,[],[f136059,f99818]) ).
fof(f136077,plain,
( sP2(sK6,sK4,sK7(sK20(sK5,sK4,sK6)),sK5)
| ~ in(sK9(sK20(sK5,sK4,sK6)),sK4)
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(resolution,[],[f136067,f87315]) ).
fof(f136089,plain,
( ~ in(sK9(sK20(sK5,sK4,sK6)),sK4)
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(forward_subsumption_resolution,[],[f136077,f87219]) ).
fof(f136100,plain,
( $false
| ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(forward_subsumption_resolution,[],[f136089,f87313]) ).
fof(f136101,plain,
( ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(avatar_contradiction_clause,[],[f136100]) ).
fof(f136146,plain,
( ! [X0] : sP3(sK5,sK4,X0)
| ~ spl35_31 ),
inference(unit_resulting_resolution,[],[f135,f67,f68,f457]) ).
fof(f136169,plain,
( ! [X0] :
( sP2(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| ~ spl35_31 ),
inference(resolution,[],[f136146,f218]) ).
fof(f136176,plain,
( in(sK10(sK20(sK5,sK4,sK6)),sK9(sK20(sK5,sK4,sK6)))
| spl35_235 ),
inference(superposition,[],[f99815,f99816]) ).
fof(f136186,plain,
( spl35_237
| spl35_235 ),
inference(avatar_split_clause,[],[f136176,f87196,f87205]) ).
fof(f136221,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6)) )
| ~ spl35_31
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(resolution,[],[f136169,f87076]) ).
fof(f136226,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) )
| ~ spl35_31 ),
inference(resolution,[],[f136169,f113]) ).
fof(f136227,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5) = sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5) )
| ~ spl35_31 ),
inference(resolution,[],[f136169,f114]) ).
fof(f136228,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4) )
| ~ spl35_31 ),
inference(resolution,[],[f136169,f115]) ).
fof(f136229,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK7(sK20(sK5,sK4,X0)) = ordered_pair(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) )
| ~ spl35_31 ),
inference(resolution,[],[f136169,f116]) ).
fof(f136230,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK7(sK20(sK5,sK4,X0)) = sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5) )
| ~ spl35_31 ),
inference(resolution,[],[f136169,f117]) ).
fof(f136231,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5),cartesian_product2(sK4,X0)) )
| ~ spl35_31 ),
inference(resolution,[],[f136169,f118]) ).
fof(f136237,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6)) )
| ~ spl35_31
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(duplicate_literal_removal,[],[f136221]) ).
fof(f136238,plain,
( spl35_234
| ~ spl35_31
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(avatar_split_clause,[],[f136237,f19286,f8152,f7682,f677,f455,f87182]) ).
fof(f136259,plain,
( spl35_186
| ~ spl35_31 ),
inference(avatar_split_clause,[],[f136229,f455,f19286]) ).
fof(f137334,plain,
( spl35_156
| ~ spl35_31 ),
inference(avatar_split_clause,[],[f136226,f455,f8152]) ).
fof(f137343,plain,
( spl35_149
| ~ spl35_31 ),
inference(avatar_split_clause,[],[f136227,f455,f7682]) ).
fof(f137362,plain,
( spl35_90
| ~ spl35_31 ),
inference(avatar_split_clause,[],[f136231,f455,f2612]) ).
fof(f137372,plain,
( spl35_46
| ~ spl35_31 ),
inference(avatar_split_clause,[],[f136228,f455,f677]) ).
fof(f137395,plain,
( spl35_121
| ~ spl35_31 ),
inference(avatar_split_clause,[],[f136230,f455,f4242]) ).
fof(f137396,plain,
( ! [X0] : sP3(sK5,sK4,X0)
| spl35_2 ),
inference(unit_resulting_resolution,[],[f132,f67,f68,f249]) ).
fof(f137417,plain,
( ! [X0] :
( sP2(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5)
| sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0)) )
| spl35_2 ),
inference(resolution,[],[f137396,f218]) ).
fof(f137439,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5) = sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5) )
| spl35_2 ),
inference(resolution,[],[f137417,f114]) ).
fof(f137441,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK7(sK20(sK5,sK4,X0)) = ordered_pair(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) )
| spl35_2 ),
inference(resolution,[],[f137417,f116]) ).
fof(f137442,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| sK7(sK20(sK5,sK4,X0)) = sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5) )
| spl35_2 ),
inference(resolution,[],[f137417,f117]) ).
fof(f137468,plain,
( spl35_121
| spl35_2 ),
inference(avatar_split_clause,[],[f137442,f248,f4242]) ).
fof(f137469,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| ~ relation(sK5)
| sK32(sK4,sK5) = sK34(sK4,sK5) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f87130,f68]) ).
fof(f137470,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6))
| sK32(sK4,sK5) = sK34(sK4,sK5) )
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f137469,f67]) ).
fof(f137471,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| ~ in(sK7(sK20(sK5,sK4,X0)),cartesian_product2(sK4,sK6)) )
| spl35_2
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(forward_subsumption_resolution,[],[f137470,f249]) ).
fof(f137473,plain,
( spl35_234
| spl35_2
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186 ),
inference(avatar_split_clause,[],[f137471,f19286,f8152,f7682,f677,f248,f87182]) ).
fof(f137482,plain,
( spl35_149
| spl35_2 ),
inference(avatar_split_clause,[],[f137439,f248,f7682]) ).
fof(f137483,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK24(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK25(sK4,sK7(sK20(sK5,sK4,X0)),sK5)) )
| spl35_2 ),
inference(forward_subsumption_resolution,[],[f7549,f249]) ).
fof(f137497,plain,
( spl35_156
| spl35_2 ),
inference(avatar_split_clause,[],[f137483,f248,f8152]) ).
fof(f137508,plain,
( spl35_186
| spl35_2 ),
inference(avatar_split_clause,[],[f137441,f248,f19286]) ).
fof(f137509,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK23(sK4,sK7(sK20(sK5,sK4,X0)),sK5),sK4) )
| spl35_2 ),
inference(forward_subsumption_resolution,[],[f536,f249]) ).
fof(f138580,plain,
( spl35_46
| spl35_2 ),
inference(avatar_split_clause,[],[f137509,f248,f677]) ).
fof(f138582,plain,
( ! [X0] :
( sK9(sK20(sK5,sK4,X0)) = sK11(sK20(sK5,sK4,X0))
| in(sK22(X0,sK4,sK7(sK20(sK5,sK4,X0)),sK5),cartesian_product2(sK4,X0)) )
| spl35_2 ),
inference(forward_subsumption_resolution,[],[f2484,f249]) ).
fof(f138591,plain,
( spl35_90
| spl35_2 ),
inference(avatar_split_clause,[],[f138582,f248,f2612]) ).
fof(f138594,plain,
( $false
| spl35_2
| spl35_238 ),
inference(forward_subsumption_resolution,[],[f87216,f137396]) ).
fof(f138595,plain,
( spl35_2
| spl35_238 ),
inference(avatar_contradiction_clause,[],[f138594]) ).
cnf(s31,plain,
( ~ spl35_2
| spl35_31
| spl35_46 ),
inference(sat_conversion,[],[f679]) ).
cnf(s83,plain,
( ~ spl35_2
| spl35_31
| spl35_90 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s120,plain,
( ~ spl35_2
| spl35_31
| spl35_121 ),
inference(sat_conversion,[],[f4244]) ).
cnf(s151,plain,
( ~ spl35_2
| spl35_31
| spl35_149 ),
inference(sat_conversion,[],[f7684]) ).
cnf(s159,plain,
( ~ spl35_2
| spl35_31
| spl35_156 ),
inference(sat_conversion,[],[f8154]) ).
cnf(s189,plain,
( ~ spl35_2
| spl35_31
| spl35_186 ),
inference(sat_conversion,[],[f19288]) ).
cnf(s237,plain,
( ~ spl35_2
| spl35_31
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186
| spl35_234 ),
inference(sat_conversion,[],[f87184]) ).
cnf(s240,plain,
( ~ spl35_235
| ~ spl35_238
| spl35_239 ),
inference(sat_conversion,[],[f87221]) ).
cnf(s241,plain,
( ~ spl35_31
| spl35_238 ),
inference(sat_conversion,[],[f87305]) ).
cnf(s242,plain,
( ~ spl35_2
| spl35_31
| spl35_238 ),
inference(sat_conversion,[],[f87307]) ).
cnf(s243,plain,
( spl35_235
| ~ spl35_238
| ~ spl35_239 ),
inference(sat_conversion,[],[f87333]) ).
cnf(s272,plain,
( ~ spl35_235
| ~ spl35_239 ),
inference(sat_conversion,[],[f98550]) ).
cnf(s475,plain,
( ~ spl35_90
| ~ spl35_121
| ~ spl35_234
| spl35_235
| ~ spl35_237
| spl35_239 ),
inference(sat_conversion,[],[f136101]) ).
cnf(s476,plain,
( spl35_235
| spl35_237 ),
inference(sat_conversion,[],[f136186]) ).
cnf(s477,plain,
( ~ spl35_31
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186
| spl35_234 ),
inference(sat_conversion,[],[f136238]) ).
cnf(s478,plain,
( ~ spl35_31
| spl35_186 ),
inference(sat_conversion,[],[f136259]) ).
cnf(s479,plain,
( ~ spl35_31
| spl35_156 ),
inference(sat_conversion,[],[f137334]) ).
cnf(s480,plain,
( ~ spl35_31
| spl35_149 ),
inference(sat_conversion,[],[f137343]) ).
cnf(s481,plain,
( ~ spl35_31
| spl35_90 ),
inference(sat_conversion,[],[f137362]) ).
cnf(s482,plain,
( ~ spl35_31
| spl35_46 ),
inference(sat_conversion,[],[f137372]) ).
cnf(s483,plain,
( ~ spl35_31
| spl35_121 ),
inference(sat_conversion,[],[f137395]) ).
cnf(s484,plain,
( spl35_2
| spl35_121 ),
inference(sat_conversion,[],[f137468]) ).
cnf(s485,plain,
( spl35_2
| ~ spl35_46
| ~ spl35_149
| ~ spl35_156
| ~ spl35_186
| spl35_234 ),
inference(sat_conversion,[],[f137473]) ).
cnf(s486,plain,
( spl35_2
| spl35_149 ),
inference(sat_conversion,[],[f137482]) ).
cnf(s487,plain,
( spl35_2
| spl35_156 ),
inference(sat_conversion,[],[f137497]) ).
cnf(s488,plain,
( spl35_2
| spl35_186 ),
inference(sat_conversion,[],[f137508]) ).
cnf(s489,plain,
( spl35_2
| spl35_46 ),
inference(sat_conversion,[],[f138580]) ).
cnf(s490,plain,
( spl35_2
| spl35_90 ),
inference(sat_conversion,[],[f138591]) ).
cnf(s491,plain,
( spl35_2
| spl35_238 ),
inference(sat_conversion,[],[f138595]) ).
cnf(s499,plain,
( spl35_235
| ~ spl35_31 ),
inference(rat,[],[s475,s243,s476,s483,s481,s241,s477,s480,s479,s478,s482]) ).
cnf(s500,plain,
~ spl35_31,
inference(rat,[],[s240,s272,s499,s241]) ).
cnf(s502,plain,
( spl35_235
| ~ spl35_2 ),
inference(rat,[],[s475,s243,s476,s242,s120,s83,s237,s189,s31,s151,s159,s500]) ).
cnf(s503,plain,
~ spl35_2,
inference(rat,[],[s240,s272,s502,s242,s500]) ).
cnf(s504,plain,
spl35_238,
inference(rat,[],[s491,s503]) ).
cnf(s505,plain,
spl35_90,
inference(rat,[],[s490,s503]) ).
cnf(s506,plain,
spl35_46,
inference(rat,[],[s489,s503]) ).
cnf(s507,plain,
spl35_186,
inference(rat,[],[s488,s503]) ).
cnf(s508,plain,
spl35_156,
inference(rat,[],[s487,s503]) ).
cnf(s509,plain,
spl35_149,
inference(rat,[],[s486,s503]) ).
cnf(s510,plain,
spl35_121,
inference(rat,[],[s484,s503]) ).
cnf(s511,plain,
spl35_234,
inference(rat,[],[s485,s503,s507,s508,s509,s506]) ).
cnf(s512,plain,
spl35_235,
inference(rat,[],[s475,s243,s476,s510,s505,s511,s504]) ).
cnf(s513,plain,
~ spl35_239,
inference(rat,[],[s272,s512]) ).
cnf(s514,plain,
$false,
inference(rat,[],[s240,s504,s512,s513]) ).
fof(f138606,plain,
$false,
inference(avatar_sat_refutation,[],[s514]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU286+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 04:30:24 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.46/2.68 % (1875815)Will run a generic schedule for satisfiability detection.
% 15.46/2.68 % (1875824)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2275243150:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.46/2.68 % (1875821)% WARNING: option uhcvi not known.
% 15.46/2.68 % (1875820)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2797714587_2999 on theBenchmark for (2999ds/0Mi)
% 15.46/2.68 % (1875822)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1782127240:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.46/2.68 % (1875823)dis+10_1_sil=32000:sp=arity:random_seed=1021669538:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.46/2.68 % (1875825)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3335522487:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.46/2.68 % (1875826)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=576317151:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.46/2.68 % (1875821)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=122450418:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.46/2.68 % TRYING [1]
% 15.46/2.68 % TRYING [2]
% 15.46/2.68 % TRYING [3]
% 15.46/2.68 % TRYING [4]
% 15.46/2.68 % (1875824)Instruction limit reached!
% 15.46/2.68 % (1875824)------------------------------
% 15.46/2.68 % (1875824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.46/2.68 % (1875824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/2.68 % (1875824)CaDiCaL version: 2.1.3
% 15.46/2.68 % (1875824)Termination reason: Instruction limit
% 15.46/2.68 % (1875824)Termination phase: Saturation
% 15.46/2.68 % (1875824)Time elapsed: 0.037 s
% 15.46/2.68 % (1875824)Peak memory usage: 12 MB
% 15.46/2.68 % (1875824)Instructions burned: 117 (million)
% 15.46/2.68 % (1875834)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=676231839:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.46/2.68 % TRYING [1]
% 15.46/2.68 % TRYING [2]
% 15.46/2.68 % TRYING [3]
% 15.46/2.68 % (1875823)Instruction limit reached!
% 15.46/2.68 % (1875823)------------------------------
% 15.46/2.68 % (1875823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.46/2.68 % (1875823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/2.68 % (1875823)CaDiCaL version: 2.1.3
% 15.46/2.68 % (1875823)Termination reason: Instruction limit
% 15.46/2.68 % (1875823)Termination phase: Saturation
% 15.46/2.68 % (1875823)Time elapsed: 0.063 s
% 15.46/2.68 % (1875823)Peak memory usage: 12 MB
% 15.46/2.68 % (1875823)Instructions burned: 103 (million)
% 15.46/2.68 % TRYING [4]
% 15.46/2.68 % (1875825)Instruction limit reached!
% 15.46/2.68 % (1875825)------------------------------
% 15.46/2.68 % (1875825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.46/2.68 % (1875825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/2.68 % (1875825)CaDiCaL version: 2.1.3
% 15.46/2.68 % (1875825)Termination reason: Instruction limit
% 15.46/2.68 % (1875825)Termination phase: Saturation
% 15.46/2.68 % (1875825)Time elapsed: 0.074 s
% 15.46/2.68 % (1875825)Peak memory usage: 13 MB
% 15.46/2.68 % (1875825)Instructions burned: 133 (million)
% 15.46/2.68 % (1875836)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3135982011:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.46/2.68 % (1875826)Instruction limit reached!
% 15.46/2.68 % (1875826)------------------------------
% 15.46/2.68 % (1875826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.46/2.68 % (1875826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/2.68 % (1875826)CaDiCaL version: 2.1.3
% 15.46/2.68 % (1875826)Termination reason: Instruction limit
% 15.46/2.68 % (1875826)Termination phase: Saturation
% 15.46/2.68 % (1875826)Time elapsed: 0.091 s
% 15.46/2.68 % (1875826)Peak memory usage: 13 MB
% 15.46/2.68 % (1875826)Instructions burned: 160 (million)
% 15.46/2.68 % (1875837)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=683134100:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.46/2.68 % (1875839)ott-21_1_sil=16000:fs=off:random_seed=45817311:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.46/2.68 % (1875836)Instruction limit reached!
% 15.46/2.68 % (1875836)------------------------------
% 15.46/2.68 % (1875836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.46/2.68 % (1875836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.04/4.82 % (1875836)CaDiCaL version: 2.1.3
% 31.04/4.82 % (1875836)Termination reason: Instruction limit
% 31.04/4.82 % (1875836)Termination phase: Saturation
% 31.04/4.82 % (1875836)Time elapsed: 0.079 s
% 31.04/4.82 % (1875836)Peak memory usage: 12 MB
% 31.04/4.82 % (1875836)Instructions burned: 132 (million)
% 31.04/4.82 % (1875842)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3732489930:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 31.04/4.82 % (1875839)Instruction limit reached!
% 31.04/4.82 % (1875839)------------------------------
% 31.04/4.82 % (1875839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.04/4.82 % (1875839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.04/4.82 % (1875839)CaDiCaL version: 2.1.3
% 31.04/4.82 % (1875839)Termination reason: Instruction limit
% 31.04/4.82 % (1875839)Termination phase: Saturation
% 31.04/4.82 % (1875839)Time elapsed: 0.097 s
% 31.04/4.82 % (1875839)Peak memory usage: 12 MB
% 31.04/4.82 % (1875839)Instructions burned: 180 (million)
% 31.04/4.82 % (1875844)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2129544268:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 31.04/4.82 % TRYING [1]
% 31.04/4.82 % TRYING [2]
% 31.04/4.82 % TRYING [3]
% 31.04/4.82 % (1875834)Instruction limit reached!
% 31.04/4.82 % (1875834)------------------------------
% 31.04/4.82 % (1875834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.04/4.82 % (1875834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.04/4.82 % (1875834)CaDiCaL version: 2.1.3
% 31.04/4.82 % (1875834)Termination reason: Instruction limit
% 31.04/4.82 % (1875834)Termination phase: Finite model building SAT solving
% 31.04/4.82 % (1875834)Time elapsed: 0.209 s
% 31.04/4.82 % (1875834)Peak memory usage: 22 MB
% 31.04/4.82 % (1875834)Instructions burned: 714 (million)
% 31.04/4.82 % (1875846)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3628020061:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 31.04/4.82 % TRYING [4]
% 31.04/4.82 % (1875837)Instruction limit reached!
% 31.04/4.82 % (1875837)------------------------------
% 31.04/4.82 % (1875837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.04/4.82 % (1875837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.04/4.82 % (1875837)CaDiCaL version: 2.1.3
% 31.04/4.82 % (1875837)Termination reason: Instruction limit
% 31.04/4.82 % (1875837)Termination phase: Saturation
% 31.04/4.82 % (1875837)Time elapsed: 0.355 s
% 31.04/4.82 % (1875837)Peak memory usage: 15 MB
% 31.04/4.82 % (1875837)Instructions burned: 687 (million)
% 31.04/4.82 % (1875848)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3650766055:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 31.04/4.82 % (1875842)Instruction limit reached!
% 31.04/4.82 % (1875842)------------------------------
% 31.04/4.82 % (1875842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.04/4.82 % (1875842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.04/4.82 % (1875842)CaDiCaL version: 2.1.3
% 31.04/4.82 % (1875842)Termination reason: Instruction limit
% 31.04/4.82 % (1875842)Termination phase: Saturation
% 31.04/4.82 % (1875842)Time elapsed: 0.311 s
% 31.04/4.82 % (1875842)Peak memory usage: 15 MB
% 31.04/4.82 % (1875842)Instructions burned: 478 (million)
% 31.04/4.82 % (1875850)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1309705707:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 31.04/4.82 % (1875846)Instruction limit reached!
% 31.04/4.82 % (1875846)------------------------------
% 31.04/4.82 % (1875846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.04/4.82 % (1875846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.04/4.82 % (1875846)CaDiCaL version: 2.1.3
% 31.04/4.82 % (1875846)Termination reason: Instruction limit
% 31.04/4.82 % (1875846)Termination phase: Saturation
% 31.04/4.82 % (1875846)Time elapsed: 0.289 s
% 31.04/4.82 % (1875846)Peak memory usage: 20 MB
% 31.04/4.82 % (1875846)Instructions burned: 1182 (million)
% 31.04/4.82 % (1875852)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1898899435:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 31.04/4.82 % TRYING [5]
% 31.04/4.82 % (1875844)Instruction limit reached!
% 31.04/4.82 % (1875844)------------------------------
% 31.04/4.82 % (1875844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.07/12.72 % (1875844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.07/12.72 % (1875844)CaDiCaL version: 2.1.3
% 87.07/12.72 % (1875844)Termination reason: Instruction limit
% 87.07/12.72 % (1875844)Termination phase: Finite model building constraint generation
% 87.07/12.72 % (1875844)Time elapsed: 0.437 s
% 87.07/12.72 % (1875844)Peak memory usage: 17 MB
% 87.07/12.72 % (1875844)Instructions burned: 867 (million)
% 87.07/12.72 % (1875854)fmb+10_1_sil=64000:random_seed=716014318:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 87.07/12.72 % TRYING [1]
% 87.07/12.72 % TRYING [2]
% 87.07/12.72 % TRYING [3]
% 87.07/12.72 % TRYING [4]
% 87.07/12.72 % TRYING [5]
% 87.07/12.72 % (1875852)Instruction limit reached!
% 87.07/12.72 % (1875852)------------------------------
% 87.07/12.72 % (1875852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.07/12.72 % (1875852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.07/12.72 % (1875852)CaDiCaL version: 2.1.3
% 87.07/12.72 % (1875852)Termination reason: Instruction limit
% 87.07/12.72 % (1875852)Termination phase: Saturation
% 87.07/12.72 % (1875852)Time elapsed: 0.295 s
% 87.07/12.72 % (1875852)Peak memory usage: 18 MB
% 87.07/12.72 % (1875852)Instructions burned: 881 (million)
% 87.07/12.72 % (1875848)Instruction limit reached!
% 87.07/12.72 % (1875848)------------------------------
% 87.07/12.72 % (1875848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.07/12.72 % (1875848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.07/12.72 % (1875848)CaDiCaL version: 2.1.3
% 87.07/12.72 % (1875848)Termination reason: Instruction limit
% 87.07/12.72 % (1875848)Termination phase: Finite model building constraint generation
% 87.07/12.72 % (1875848)Time elapsed: 0.400 s
% 87.07/12.72 % (1875848)Peak memory usage: 105 MB
% 87.07/12.72 % (1875848)Instructions burned: 890 (million)
% 87.07/12.72 % (1875856)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1848641099:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 87.07/12.72 % TRYING [20]
% 87.07/12.72 % (1875850)Instruction limit reached!
% 87.07/12.72 % (1875850)------------------------------
% 87.07/12.72 % (1875850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.07/12.72 % (1875850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.07/12.72 % (1875850)CaDiCaL version: 2.1.3
% 87.07/12.72 % (1875850)Termination reason: Instruction limit
% 87.07/12.72 % (1875850)Termination phase: Saturation
% 87.07/12.72 % (1875850)Time elapsed: 0.383 s
% 87.07/12.72 % (1875850)Peak memory usage: 21 MB
% 87.07/12.72 % (1875850)Instructions burned: 693 (million)
% 87.07/12.72 % (1875858)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3909859923:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 87.07/12.72 % TRYING [8]
% 87.07/12.72 % (1875859)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3608288429:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 87.07/12.72 % TRYING [5]
% 87.07/12.72 % (1875858)Instruction limit reached!
% 87.07/12.72 % (1875858)------------------------------
% 87.07/12.72 % (1875858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.07/12.72 % (1875858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.07/12.72 % (1875858)CaDiCaL version: 2.1.3
% 87.07/12.72 % (1875858)Termination reason: Instruction limit
% 87.07/12.72 % (1875858)Termination phase: Finite model building constraint generation
% 87.07/12.72 % (1875858)Time elapsed: 0.361 s
% 87.07/12.72 % (1875858)Peak memory usage: 87 MB
% 87.07/12.72 % (1875858)Instructions burned: 922 (million)
% 87.07/12.72 % (1875862)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1900558144:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 87.07/12.72 % (1875862)Instruction limit reached!
% 87.07/12.72 % (1875862)------------------------------
% 87.07/12.72 % (1875862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 87.07/12.72 % (1875862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.07/12.72 % (1875862)CaDiCaL version: 2.1.3
% 87.07/12.72 % (1875862)Termination reason: Instruction limit
% 87.07/12.72 % (1875862)Termination phase: Saturation
% 87.07/12.72 % (1875862)Time elapsed: 0.906 s
% 87.07/12.72 % (1875862)Peak memory usage: 31 MB
% 87.07/12.72 % (1875862)Instructions burned: 1472 (million)
% 87.07/12.72 % (1875864)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=860962699:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 87.07/12.72 % (1875864)Cannot represent all propositional literals internally
% 112.80/16.84 % (1875864)Refutation not found, incomplete strategy
% 112.80/16.84 % (1875864)------------------------------
% 112.80/16.84 % (1875864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875864)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875864)Termination reason: Refutation not found, incomplete strategy
% 112.80/16.84 % (1875864)Time elapsed: 0.005 s
% 112.80/16.84 % (1875864)Peak memory usage: 10 MB
% 112.80/16.84 % (1875864)Instructions burned: 8 (million)
% 112.80/16.84 % (1875864)------------------------------
% 112.80/16.84 % (1875864)------------------------------
% 112.80/16.84 % (1875866)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=840907507:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 112.80/16.84 % TRYING [16]
% 112.80/16.84 % (1875856)Instruction limit reached!
% 112.80/16.84 % (1875856)------------------------------
% 112.80/16.84 % (1875856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875856)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875856)Termination reason: Instruction limit
% 112.80/16.84 % (1875856)Termination phase: Finite model building constraint generation
% 112.80/16.84 % (1875856)Time elapsed: 1.813 s
% 112.80/16.84 % (1875856)Peak memory usage: 552 MB
% 112.80/16.84 % (1875856)Instructions burned: 9521 (million)
% 112.80/16.84 % (1875868)ott-2_1_sil=16000:newcnf=on:random_seed=2260282929:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi)
% 112.80/16.84 % (1875868)Instruction limit reached!
% 112.80/16.84 % (1875868)------------------------------
% 112.80/16.84 % (1875868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875868)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875868)Termination reason: Instruction limit
% 112.80/16.84 % (1875868)Termination phase: Saturation
% 112.80/16.84 % (1875868)Time elapsed: 0.255 s
% 112.80/16.84 % (1875868)Peak memory usage: 20 MB
% 112.80/16.84 % (1875868)Instructions burned: 869 (million)
% 112.80/16.84 % (1875866)Instruction limit reached!
% 112.80/16.84 % (1875866)------------------------------
% 112.80/16.84 % (1875866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875866)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875866)Termination reason: Instruction limit
% 112.80/16.84 % (1875866)Termination phase: Finite model building constraint generation
% 112.80/16.84 % (1875866)Time elapsed: 0.750 s
% 112.80/16.84 % (1875866)Peak memory usage: 138 MB
% 112.80/16.84 % (1875866)Instructions burned: 2176 (million)
% 112.80/16.84 % (1875870)ott+10_1_sil=32000:tgt=ground:random_seed=2067959790:i=5114:av=off_2969 on theBenchmark for (2969ds/5114Mi)
% 112.80/16.84 % (1875872)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2863402943:i=54282_2969 on theBenchmark for (2969ds/54282Mi)
% 112.80/16.84 % TRYING [1]
% 112.80/16.84 % TRYING [2]
% 112.80/16.84 % TRYING [3]
% 112.80/16.84 % TRYING [4]
% 112.80/16.84 % (1875859)Instruction limit reached!
% 112.80/16.84 % (1875859)------------------------------
% 112.80/16.84 % (1875859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875859)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875859)Termination reason: Instruction limit
% 112.80/16.84 % (1875859)Termination phase: Saturation
% 112.80/16.84 % (1875859)Time elapsed: 2.456 s
% 112.80/16.84 % (1875859)Peak memory usage: 25 MB
% 112.80/16.84 % (1875859)Instructions burned: 5133 (million)
% 112.80/16.84 % (1875874)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2373595479:i=3512:aac=none_2965 on theBenchmark for (2965ds/3512Mi)
% 112.80/16.84 % TRYING [5]
% 112.80/16.84 % (1875870)Instruction limit reached!
% 112.80/16.84 % (1875870)------------------------------
% 112.80/16.84 % (1875870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875870)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875870)Termination reason: Instruction limit
% 112.80/16.84 % (1875870)Termination phase: Saturation
% 112.80/16.84 % (1875870)Time elapsed: 1.341 s
% 112.80/16.84 % (1875870)Peak memory usage: 66 MB
% 112.80/16.84 % (1875870)Instructions burned: 5123 (million)
% 112.80/16.84 % (1875876)dis+21_1_sil=32000:sas=cadical:random_seed=645206766:i=3773:amm=off_2956 on theBenchmark for (2956ds/3773Mi)
% 112.80/16.84 % (1875874)Instruction limit reached!
% 112.80/16.84 % (1875874)------------------------------
% 112.80/16.84 % (1875874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875874)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875874)Termination reason: Instruction limit
% 112.80/16.84 % (1875874)Termination phase: Saturation
% 112.80/16.84 % (1875874)Time elapsed: 1.812 s
% 112.80/16.84 % (1875874)Peak memory usage: 23 MB
% 112.80/16.84 % (1875874)Instructions burned: 3514 (million)
% 112.80/16.84 % (1875878)ott+11_1_sil=16000:gs=on:random_seed=3008468110:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2947 on theBenchmark for (2947ds/2251Mi)
% 112.80/16.84 % (1875876)Instruction limit reached!
% 112.80/16.84 % (1875876)------------------------------
% 112.80/16.84 % (1875876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875876)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875876)Termination reason: Instruction limit
% 112.80/16.84 % (1875876)Termination phase: Saturation
% 112.80/16.84 % (1875876)Time elapsed: 0.961 s
% 112.80/16.84 % (1875876)Peak memory usage: 32 MB
% 112.80/16.84 % (1875876)Instructions burned: 3776 (million)
% 112.80/16.84 % (1875880)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2487055958:fmbsr=1.6:i=67534_2946 on theBenchmark for (2946ds/67534Mi)
% 112.80/16.84 % TRYING [7]
% 112.80/16.84 % (1875878)Instruction limit reached!
% 112.80/16.84 % (1875878)------------------------------
% 112.80/16.84 % (1875878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875878)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875878)Termination reason: Instruction limit
% 112.80/16.84 % (1875878)Termination phase: Saturation
% 112.80/16.84 % (1875878)Time elapsed: 1.162 s
% 112.80/16.84 % (1875878)Peak memory usage: 25 MB
% 112.80/16.84 % (1875878)Instructions burned: 2251 (million)
% 112.80/16.84 % (1875882)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1864539520:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2935 on theBenchmark for (2935ds/4591Mi)
% 112.80/16.84 % (1875882)Instruction limit reached!
% 112.80/16.84 % (1875882)------------------------------
% 112.80/16.84 % (1875882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875882)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875882)Termination reason: Instruction limit
% 112.80/16.84 % (1875882)Termination phase: Saturation
% 112.80/16.84 % (1875882)Time elapsed: 2.483 s
% 112.80/16.84 % (1875882)Peak memory usage: 56 MB
% 112.80/16.84 % (1875882)Instructions burned: 4591 (million)
% 112.80/16.84 % (1875884)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=738887536:i=29340_2910 on theBenchmark for (2910ds/29340Mi)
% 112.80/16.84 % (1875854)Instruction limit reached!
% 112.80/16.84 % (1875854)------------------------------
% 112.80/16.84 % (1875854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875854)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875854)Termination reason: Instruction limit
% 112.80/16.84 % (1875854)Termination phase: Finite model building SAT solving
% 112.80/16.84 % (1875854)Time elapsed: 10.186 s
% 112.80/16.84 % (1875854)Peak memory usage: 34 MB
% 112.80/16.84 % (1875854)Instructions burned: 22062 (million)
% 112.80/16.84 % (1875886)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4158129870:i=5211_2890 on theBenchmark for (2890ds/5211Mi)
% 112.80/16.84 % (1875886)Instruction limit reached!
% 112.80/16.84 % (1875886)------------------------------
% 112.80/16.84 % (1875886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875886)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875886)Termination reason: Instruction limit
% 112.80/16.84 % (1875886)Termination phase: Saturation
% 112.80/16.84 % (1875886)Time elapsed: 1.364 s
% 112.80/16.84 % (1875886)Peak memory usage: 46 MB
% 112.80/16.84 % (1875886)Instructions burned: 5215 (million)
% 112.80/16.84 % (1875888)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2338501739:i=5497:nm=2_2877 on theBenchmark for (2877ds/5497Mi)
% 112.80/16.84 % TRYING [17]
% 112.80/16.84 % (1875888)Instruction limit reached!
% 112.80/16.84 % (1875888)------------------------------
% 112.80/16.84 % (1875888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.84 % (1875888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.84 % (1875888)CaDiCaL version: 2.1.3
% 112.80/16.84 % (1875888)Termination reason: Instruction limit
% 112.80/16.84 % (1875888)Termination phase: Finite model building constraint generation
% 112.80/16.84 % (1875888)Time elapsed: 1.040 s
% 112.80/16.84 % (1875888)Peak memory usage: 346 MB
% 112.80/16.84 % (1875888)Instructions burned: 5502 (million)
% 112.80/16.84 % (1875890)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3610091412:fmbsr=2:i=46332_2866 on theBenchmark for (2866ds/46332Mi)
% 112.80/16.84 % TRYING [15]
% 112.80/16.84 % (1875884) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1875815-1875884"...
% 112.80/16.84 % (1875884)...printing done.
% 112.80/16.84 % (1875884)Refutation found. Thanks to Tanya!
% 112.80/16.84 % SZS status Theorem for theBenchmark
% 112.80/16.84 % SZS output start Proof for theBenchmark
% See solution above
% 112.80/16.85 % (1875884)------------------------------
% 112.80/16.85 % (1875884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.80/16.85 % (1875884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.80/16.85 % (1875884)CaDiCaL version: 2.1.3
% 112.80/16.85 % (1875884)Termination reason: Refutation
% 112.80/16.85 % (1875884)Time elapsed: 7.342 s
% 112.80/16.85 % (1875884)Peak memory usage: 47 MB
% 112.80/16.85 % (1875884)Instructions burned: 15827 (million)
% 112.80/16.85 % (1875815)Success in time 16.428 s
% 112.80/16.85 % Vampire exiting
%------------------------------------------------------------------------------