%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU277+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:08 PM UTC 2026
% Result : Theorem 18.29s 3.58s
% Output : Refutation 19.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 29
% Syntax : Number of formulae : 267 ( 62 unt; 25 def)
% Number of atoms : 1028 ( 211 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1195 ( 434 ~; 616 |; 119 &)
% ( 16 <=>; 8 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 10 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 4 con; 0-4 aty)
% Number of variables : 448 ( 0 sgn 341 !; 107 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f61,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f199,axiom,
! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
=> X4 = X5 )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(X5,cartesian_product2(X0,X0))
& X5 = X4
& ? [X10,X11] :
( X4 = ordered_pair(X10,X11)
& in(ordered_pair(apply(X2,X10),apply(X2,X11)),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e6_21__wellord2__1) ).
fof(f201,conjecture,
! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,cartesian_product2(X0,X0))
& ? [X5,X6] :
( X4 = ordered_pair(X5,X6)
& in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e6_21__wellord2__1) ).
fof(f202,negated_conjecture,
~ ! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ? [X3] :
! [X4] :
( in(X4,X3)
<=> ( in(X4,cartesian_product2(X0,X0))
& ? [X5,X6] :
( X4 = ordered_pair(X5,X6)
& in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f201]) ).
fof(f330,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f365,plain,
! [X0,X1,X2] :
( ( relation(X1)
& relation(X2)
& function(X2) )
=> ( ! [X3,X4,X5] :
( ( X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
=> X4 = X5 )
=> ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) ) ) ),
inference(rectify,[],[f199]) ).
fof(f528,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f365]) ).
fof(f529,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
| ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f528]) ).
fof(f532,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(X0,X0))
& ? [X5,X6] :
( X4 = ordered_pair(X5,X6)
& in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) ) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(ennf_transformation,[],[f202]) ).
fof(f533,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( in(X4,X3)
<~> ( in(X4,cartesian_product2(X0,X0))
& ? [X5,X6] :
( X4 = ordered_pair(X5,X6)
& in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) ) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(flattening,[],[f532]) ).
fof(f720,definition,
! [X1,X2] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ sP2(X1,X2) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f721,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( in(X11,X10)
<=> ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_folding,[],[f529,f720]) ).
fof(f927,plain,
! [X1,X2] :
( ? [X3,X4,X5] :
( X4 != X5
& X3 = X4
& ? [X6,X7] :
( X4 = ordered_pair(X6,X7)
& in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) )
& X3 = X5
& ? [X8,X9] :
( X5 = ordered_pair(X8,X9)
& in(ordered_pair(apply(X2,X8),apply(X2,X9)),X1) ) )
| ~ sP2(X1,X2) ),
inference(nnf_transformation,[],[f720]) ).
fof(f928,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5,X6] :
( ordered_pair(X5,X6) = X3
& in(ordered_pair(apply(X1,X5),apply(X1,X6)),X0) )
& X2 = X4
& ? [X7,X8] :
( ordered_pair(X7,X8) = X4
& in(ordered_pair(apply(X1,X7),apply(X1,X8)),X0) ) )
| ~ sP2(X0,X1) ),
inference(rectify,[],[f927]) ).
fof(f929,plain,
! [X0,X1] :
( ( sK119(X0,X1) != sK120(X0,X1)
& sK118(X0,X1) = sK119(X0,X1)
& sK119(X0,X1) = ordered_pair(sK121(X0,X1),sK122(X0,X1))
& in(ordered_pair(apply(X1,sK121(X0,X1)),apply(X1,sK122(X0,X1))),X0)
& sK118(X0,X1) = sK120(X0,X1)
& sK120(X0,X1) = ordered_pair(sK123(X0,X1),sK124(X0,X1))
& in(ordered_pair(apply(X1,sK123(X0,X1)),apply(X1,sK124(X0,X1))),X0) )
| ~ sP2(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118,sK119,sK120,sK121,sK122,sK123,sK124]),skolemize(X2,sK118(X0,X1)),skolemize(X3,sK119(X0,X1)),skolemize(X4,sK120(X0,X1)),skolemize(X5,sK121(X0,X1)),skolemize(X6,sK122(X0,X1)),skolemize(X7,sK123(X0,X1)),skolemize(X8,sK124(X0,X1))],[f928]) ).
fof(f930,plain,
! [X0,X1,X2] :
( ? [X10] :
! [X11] :
( ( in(X11,X10)
| ! [X12] :
( ~ in(X12,cartesian_product2(X0,X0))
| X11 != X12
| ! [X13,X14] :
( ordered_pair(X13,X14) != X11
| ~ in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) ) )
& ( ? [X12] :
( in(X12,cartesian_product2(X0,X0))
& X11 = X12
& ? [X13,X14] :
( ordered_pair(X13,X14) = X11
& in(ordered_pair(apply(X2,X13),apply(X2,X14)),X1) ) )
| ~ in(X11,X10) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(nnf_transformation,[],[f721]) ).
fof(f931,plain,
! [X0,X1,X2] :
( ? [X3] :
! [X4] :
( ( in(X4,X3)
| ! [X5] :
( ~ in(X5,cartesian_product2(X0,X0))
| X4 != X5
| ! [X6,X7] :
( ordered_pair(X6,X7) != X4
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) ) ) )
& ( ? [X8] :
( in(X8,cartesian_product2(X0,X0))
& X4 = X8
& ? [X9,X10] :
( ordered_pair(X9,X10) = X4
& in(ordered_pair(apply(X2,X9),apply(X2,X10)),X1) ) )
| ~ in(X4,X3) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(rectify,[],[f930]) ).
fof(f932,plain,
! [X0,X1,X2] :
( ! [X4] :
( ( in(X4,sK125(X0,X1,X2))
| ! [X5] :
( ~ in(X5,cartesian_product2(X0,X0))
| X4 != X5
| ! [X6,X7] :
( ordered_pair(X6,X7) != X4
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1) ) ) )
& ( ( in(sK126(X0,X1,X2,X4),cartesian_product2(X0,X0))
& sK126(X0,X1,X2,X4) = X4
& ordered_pair(sK127(X1,X2,X4),sK128(X1,X2,X4)) = X4
& in(ordered_pair(apply(X2,sK127(X1,X2,X4)),apply(X2,sK128(X1,X2,X4))),X1) )
| ~ in(X4,sK125(X0,X1,X2)) ) )
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK125,sK126,sK127,sK128]),skolemize(X3,sK125(X0,X1,X2)),skolemize(X8,sK126(X0,X1,X2,X4)),skolemize(X9,sK127(X1,X2,X4)),skolemize(X10,sK128(X1,X2,X4))],[f931]) ).
fof(f942,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X0,X0))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) )
| ~ in(X4,X3) )
& ( ( in(X4,cartesian_product2(X0,X0))
& ? [X5,X6] :
( X4 = ordered_pair(X5,X6)
& in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) ) )
| in(X4,X3) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(nnf_transformation,[],[f533]) ).
fof(f943,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X0,X0))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) )
| ~ in(X4,X3) )
& ( ( in(X4,cartesian_product2(X0,X0))
& ? [X5,X6] :
( X4 = ordered_pair(X5,X6)
& in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) ) )
| in(X4,X3) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(flattening,[],[f942]) ).
fof(f944,plain,
? [X0,X1,X2] :
( ! [X3] :
? [X4] :
( ( ~ in(X4,cartesian_product2(X0,X0))
| ! [X5,X6] :
( ordered_pair(X5,X6) != X4
| ~ in(ordered_pair(apply(X2,X5),apply(X2,X6)),X1) )
| ~ in(X4,X3) )
& ( ( in(X4,cartesian_product2(X0,X0))
& ? [X7,X8] :
( ordered_pair(X7,X8) = X4
& in(ordered_pair(apply(X2,X7),apply(X2,X8)),X1) ) )
| in(X4,X3) ) )
& relation(X1)
& relation(X2)
& function(X2) ),
inference(rectify,[],[f943]) ).
fof(f945,plain,
( ! [X3] :
( ( ~ in(sK140(X3),cartesian_product2(sK137,sK137))
| ! [X5,X6] :
( ordered_pair(X5,X6) != sK140(X3)
| ~ in(ordered_pair(apply(sK139,X5),apply(sK139,X6)),sK138) )
| ~ in(sK140(X3),X3) )
& ( ( in(sK140(X3),cartesian_product2(sK137,sK137))
& sK140(X3) = ordered_pair(sK141(X3),sK142(X3))
& in(ordered_pair(apply(sK139,sK141(X3)),apply(sK139,sK142(X3))),sK138) )
| in(sK140(X3),X3) ) )
& relation(sK138)
& relation(sK139)
& function(sK139) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK137,sK138,sK139,sK140,sK141,sK142]),skolemize(X0,sK137),skolemize(X1,sK138),skolemize(X2,sK139),skolemize(X4,sK140(X3)),skolemize(X7,sK141(X3)),skolemize(X8,sK142(X3))],[f944]) ).
fof(f1250,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f61]) ).
fof(f1490,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| sK118(X0,X1) = sK120(X0,X1) ),
inference(cnf_transformation,[],[f929]) ).
fof(f1493,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| sK118(X0,X1) = sK119(X0,X1) ),
inference(cnf_transformation,[],[f929]) ).
fof(f1494,plain,
! [X0,X1] :
( sK119(X0,X1) != sK120(X0,X1)
| ~ sP2(X0,X1) ),
inference(cnf_transformation,[],[f929]) ).
fof(f1495,plain,
! [X2,X0,X1,X4] :
( in(ordered_pair(apply(X2,sK127(X1,X2,X4)),apply(X2,sK128(X1,X2,X4))),X1)
| ~ in(X4,sK125(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1496,plain,
! [X2,X0,X1,X4] :
( ordered_pair(sK127(X1,X2,X4),sK128(X1,X2,X4)) = X4
| ~ in(X4,sK125(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1497,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,sK125(X0,X1,X2))
| sK126(X0,X1,X2,X4) = X4
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1498,plain,
! [X2,X0,X1,X4] :
( in(sK126(X0,X1,X2,X4),cartesian_product2(X0,X0))
| ~ in(X4,sK125(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1499,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK125(X0,X1,X2))
| ~ in(X5,cartesian_product2(X0,X0))
| X4 != X5
| ordered_pair(X6,X7) != X4
| ~ in(ordered_pair(apply(X2,X6),apply(X2,X7)),X1)
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f932]) ).
fof(f1516,plain,
function(sK139),
inference(cnf_transformation,[],[f945]) ).
fof(f1517,plain,
relation(sK139),
inference(cnf_transformation,[],[f945]) ).
fof(f1518,plain,
relation(sK138),
inference(cnf_transformation,[],[f945]) ).
fof(f1519,plain,
! [X3] :
( in(ordered_pair(apply(sK139,sK141(X3)),apply(sK139,sK142(X3))),sK138)
| in(sK140(X3),X3) ),
inference(cnf_transformation,[],[f945]) ).
fof(f1520,plain,
! [X3] :
( sK140(X3) = ordered_pair(sK141(X3),sK142(X3))
| in(sK140(X3),X3) ),
inference(cnf_transformation,[],[f945]) ).
fof(f1521,plain,
! [X3] :
( in(sK140(X3),cartesian_product2(sK137,sK137))
| in(sK140(X3),X3) ),
inference(cnf_transformation,[],[f945]) ).
fof(f1522,plain,
! [X3,X6,X5] :
( ~ in(sK140(X3),cartesian_product2(sK137,sK137))
| ordered_pair(X5,X6) != sK140(X3)
| ~ in(ordered_pair(apply(sK139,X5),apply(sK139,X6)),sK138)
| ~ in(sK140(X3),X3) ),
inference(cnf_transformation,[],[f945]) ).
fof(f1733,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f330]) ).
fof(f1776,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),unordered_pair(X0,X0)),
inference(definition_unfolding,[],[f1250,f1733]) ).
fof(f1922,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( in(X4,sK125(X0,X1,X2))
| ~ in(X5,cartesian_product2(X0,X0))
| X4 != X5
| unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)) != X4
| ~ in(unordered_pair(unordered_pair(apply(X2,X6),apply(X2,X7)),unordered_pair(apply(X2,X6),apply(X2,X6))),X1)
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_unfolding,[],[f1499,f1776,f1776]) ).
fof(f1923,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,sK125(X0,X1,X2))
| unordered_pair(unordered_pair(sK127(X1,X2,X4),sK128(X1,X2,X4)),unordered_pair(sK127(X1,X2,X4),sK127(X1,X2,X4))) = X4
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_unfolding,[],[f1496,f1776]) ).
fof(f1924,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,sK125(X0,X1,X2))
| in(unordered_pair(unordered_pair(apply(X2,sK127(X1,X2,X4)),apply(X2,sK128(X1,X2,X4))),unordered_pair(apply(X2,sK127(X1,X2,X4)),apply(X2,sK127(X1,X2,X4)))),X1)
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(definition_unfolding,[],[f1495,f1776]) ).
fof(f1927,plain,
! [X3,X6,X5] :
( ~ in(sK140(X3),cartesian_product2(sK137,sK137))
| sK140(X3) != unordered_pair(unordered_pair(X5,X6),unordered_pair(X5,X5))
| ~ in(unordered_pair(unordered_pair(apply(sK139,X5),apply(sK139,X6)),unordered_pair(apply(sK139,X5),apply(sK139,X5))),sK138)
| ~ in(sK140(X3),X3) ),
inference(definition_unfolding,[],[f1522,f1776,f1776]) ).
fof(f1928,plain,
! [X3] :
( sK140(X3) = unordered_pair(unordered_pair(sK141(X3),sK142(X3)),unordered_pair(sK141(X3),sK141(X3)))
| in(sK140(X3),X3) ),
inference(definition_unfolding,[],[f1520,f1776]) ).
fof(f1929,plain,
! [X3] :
( in(unordered_pair(unordered_pair(apply(sK139,sK141(X3)),apply(sK139,sK142(X3))),unordered_pair(apply(sK139,sK141(X3)),apply(sK139,sK141(X3)))),sK138)
| in(sK140(X3),X3) ),
inference(definition_unfolding,[],[f1519,f1776]) ).
fof(f2099,plain,
! [X2,X0,X1,X6,X7,X5] :
( in(X5,sK125(X0,X1,X2))
| ~ in(X5,cartesian_product2(X0,X0))
| unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)) != X5
| ~ in(unordered_pair(unordered_pair(apply(X2,X6),apply(X2,X7)),unordered_pair(apply(X2,X6),apply(X2,X6))),X1)
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(equality_resolution,[],[f1922]) ).
fof(f2100,plain,
! [X2,X0,X1,X6,X7] :
( ~ in(unordered_pair(unordered_pair(apply(X2,X6),apply(X2,X7)),unordered_pair(apply(X2,X6),apply(X2,X6))),X1)
| ~ in(unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)),cartesian_product2(X0,X0))
| in(unordered_pair(unordered_pair(X6,X7),unordered_pair(X6,X6)),sK125(X0,X1,X2))
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(equality_resolution,[],[f2099]) ).
fof(f2123,definition,
sF168 = cartesian_product2(sK137,sK137),
introduced(definition,[new_symbols(definition,[sF168])],[function_definition]) ).
fof(f2124,plain,
cartesian_product2(sK137,sK137) = sF168,
inference(reorient_equations,[],[f2123]) ).
fof(f2125,definition,
! [X5] : sF169(X5) = unordered_pair(X5,X5),
introduced(definition,[new_symbols(definition,[sF169])],[function_definition]) ).
fof(f2126,plain,
! [X5] : unordered_pair(X5,X5) = sF169(X5),
inference(reorient_equations,[],[f2125]) ).
fof(f2127,definition,
! [X6,X5] : sF170(X5,X6) = unordered_pair(unordered_pair(X5,X6),sF169(X5)),
introduced(definition,[new_symbols(definition,[sF170])],[function_definition]) ).
fof(f2128,plain,
! [X6,X5] : unordered_pair(unordered_pair(X5,X6),sF169(X5)) = sF170(X5,X6),
inference(reorient_equations,[],[f2127]) ).
fof(f2129,definition,
! [X5] : sF171(X5) = apply(sK139,X5),
introduced(definition,[new_symbols(definition,[sF171])],[function_definition]) ).
fof(f2130,plain,
! [X5] : apply(sK139,X5) = sF171(X5),
inference(reorient_equations,[],[f2129]) ).
fof(f2131,definition,
! [X6,X5] : sF172(X5,X6) = unordered_pair(sF171(X5),sF171(X6)),
introduced(definition,[new_symbols(definition,[sF172])],[function_definition]) ).
fof(f2132,plain,
! [X6,X5] : unordered_pair(sF171(X5),sF171(X6)) = sF172(X5,X6),
inference(reorient_equations,[],[f2131]) ).
fof(f2133,definition,
! [X5] : sF173(X5) = unordered_pair(sF171(X5),sF171(X5)),
introduced(definition,[new_symbols(definition,[sF173])],[function_definition]) ).
fof(f2134,plain,
! [X5] : unordered_pair(sF171(X5),sF171(X5)) = sF173(X5),
inference(reorient_equations,[],[f2133]) ).
fof(f2135,definition,
! [X6,X5] : sF174(X5,X6) = unordered_pair(sF172(X5,X6),sF173(X5)),
introduced(definition,[new_symbols(definition,[sF174])],[function_definition]) ).
fof(f2136,plain,
! [X6,X5] : unordered_pair(sF172(X5,X6),sF173(X5)) = sF174(X5,X6),
inference(reorient_equations,[],[f2135]) ).
fof(f2137,plain,
! [X3,X6,X5] :
( sK140(X3) != sF170(X5,X6)
| ~ in(sK140(X3),sF168)
| ~ in(sF174(X5,X6),sK138)
| ~ in(sK140(X3),X3) ),
inference(definition_folding,[],[f1927,f2136,f2134,f2130,f2130,f2132,f2130,f2130,f2128,f2126,f2124]) ).
fof(f2138,plain,
! [X3] :
( in(sK140(X3),sF168)
| in(sK140(X3),X3) ),
inference(definition_folding,[],[f1521,f2124]) ).
fof(f2139,definition,
! [X3] : sF175(X3) = unordered_pair(sK141(X3),sK142(X3)),
introduced(definition,[new_symbols(definition,[sF175])],[function_definition]) ).
fof(f2140,plain,
! [X3] : unordered_pair(sK141(X3),sK142(X3)) = sF175(X3),
inference(reorient_equations,[],[f2139]) ).
fof(f2141,definition,
! [X3] : sF176(X3) = unordered_pair(sK141(X3),sK141(X3)),
introduced(definition,[new_symbols(definition,[sF176])],[function_definition]) ).
fof(f2142,plain,
! [X3] : unordered_pair(sK141(X3),sK141(X3)) = sF176(X3),
inference(reorient_equations,[],[f2141]) ).
fof(f2143,definition,
! [X3] : sF177(X3) = unordered_pair(sF175(X3),sF176(X3)),
introduced(definition,[new_symbols(definition,[sF177])],[function_definition]) ).
fof(f2144,plain,
! [X3] : unordered_pair(sF175(X3),sF176(X3)) = sF177(X3),
inference(reorient_equations,[],[f2143]) ).
fof(f2145,plain,
! [X3] :
( in(sK140(X3),X3)
| sK140(X3) = sF177(X3) ),
inference(definition_folding,[],[f1928,f2144,f2142,f2140]) ).
fof(f2146,definition,
! [X3] : sF178(X3) = apply(sK139,sK141(X3)),
introduced(definition,[new_symbols(definition,[sF178])],[function_definition]) ).
fof(f2147,plain,
! [X3] : apply(sK139,sK141(X3)) = sF178(X3),
inference(reorient_equations,[],[f2146]) ).
fof(f2148,definition,
! [X3] : sF179(X3) = apply(sK139,sK142(X3)),
introduced(definition,[new_symbols(definition,[sF179])],[function_definition]) ).
fof(f2149,plain,
! [X3] : apply(sK139,sK142(X3)) = sF179(X3),
inference(reorient_equations,[],[f2148]) ).
fof(f2150,definition,
! [X3] : sF180(X3) = unordered_pair(sF178(X3),sF179(X3)),
introduced(definition,[new_symbols(definition,[sF180])],[function_definition]) ).
fof(f2151,plain,
! [X3] : unordered_pair(sF178(X3),sF179(X3)) = sF180(X3),
inference(reorient_equations,[],[f2150]) ).
fof(f2152,definition,
! [X3] : sF181(X3) = unordered_pair(sF178(X3),sF178(X3)),
introduced(definition,[new_symbols(definition,[sF181])],[function_definition]) ).
fof(f2153,plain,
! [X3] : unordered_pair(sF178(X3),sF178(X3)) = sF181(X3),
inference(reorient_equations,[],[f2152]) ).
fof(f2154,definition,
! [X3] : sF182(X3) = unordered_pair(sF180(X3),sF181(X3)),
introduced(definition,[new_symbols(definition,[sF182])],[function_definition]) ).
fof(f2155,plain,
! [X3] : unordered_pair(sF180(X3),sF181(X3)) = sF182(X3),
inference(reorient_equations,[],[f2154]) ).
fof(f2156,plain,
! [X3] :
( in(sF182(X3),sK138)
| in(sK140(X3),X3) ),
inference(definition_folding,[],[f1929,f2155,f2153,f2147,f2147,f2151,f2149,f2147]) ).
fof(f2192,plain,
! [X5] : sF173(X5) = sF169(sF171(X5)),
inference(forward_demodulation,[],[f2134,f2126]) ).
fof(f2193,plain,
! [X3] : sF176(X3) = sF169(sK141(X3)),
inference(forward_demodulation,[],[f2142,f2126]) ).
fof(f2194,plain,
! [X3] : sF178(X3) = sF171(sK141(X3)),
inference(forward_demodulation,[],[f2147,f2130]) ).
fof(f2195,plain,
! [X3] : sF179(X3) = sF171(sK142(X3)),
inference(forward_demodulation,[],[f2149,f2130]) ).
fof(f2196,plain,
! [X3] : sF181(X3) = sF169(sF178(X3)),
inference(forward_demodulation,[],[f2153,f2126]) ).
fof(f2566,plain,
! [X2,X0,X1] :
( in(sK126(sK137,X0,X1,X2),sF168)
| ~ in(X2,sK125(sK137,X0,X1))
| sP2(X0,X1)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(superposition,[],[f1498,f2124]) ).
fof(f2630,plain,
! [X2,X0,X1] :
( sP2(X1,X2)
| sK140(sK125(X0,X1,X2)) = sK126(X0,X1,X2,sK140(sK125(X0,X1,X2)))
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2)
| sK140(sK125(X0,X1,X2)) = sF177(sK125(X0,X1,X2)) ),
inference(resolution,[],[f1497,f2145]) ).
fof(f2631,plain,
! [X2,X0,X1] :
( in(sK140(sK125(X0,X1,X2)),sF168)
| sP2(X1,X2)
| ~ relation(X1)
| ~ relation(X2)
| ~ function(X2)
| sK140(sK125(X0,X1,X2)) = sK126(X0,X1,X2,sK140(sK125(X0,X1,X2))) ),
inference(resolution,[],[f1497,f2138]) ).
fof(f2726,plain,
! [X0] : unordered_pair(sF175(X0),sF169(sK141(X0))) = sF170(sK141(X0),sK142(X0)),
inference(superposition,[],[f2128,f2140]) ).
fof(f2727,plain,
! [X0,X1] : sF170(sF171(X0),sF171(X1)) = unordered_pair(sF172(X0,X1),sF169(sF171(X0))),
inference(superposition,[],[f2128,f2132]) ).
fof(f2732,plain,
! [X0] : unordered_pair(sF180(X0),sF169(sF178(X0))) = sF170(sF178(X0),sF179(X0)),
inference(superposition,[],[f2128,f2151]) ).
fof(f2749,plain,
! [X0] : unordered_pair(sF180(X0),sF181(X0)) = sF170(sF178(X0),sF179(X0)),
inference(forward_demodulation,[],[f2732,f2196]) ).
fof(f2750,plain,
! [X0,X1] : unordered_pair(sF172(X0,X1),sF173(X0)) = sF170(sF171(X0),sF171(X1)),
inference(forward_demodulation,[],[f2727,f2192]) ).
fof(f2751,plain,
! [X0] : unordered_pair(sF175(X0),sF176(X0)) = sF170(sK141(X0),sK142(X0)),
inference(forward_demodulation,[],[f2726,f2193]) ).
fof(f2756,plain,
! [X0] : sF182(X0) = sF170(sF178(X0),sF179(X0)),
inference(forward_demodulation,[],[f2749,f2155]) ).
fof(f2757,plain,
! [X0,X1] : sF174(X0,X1) = sF170(sF171(X0),sF171(X1)),
inference(forward_demodulation,[],[f2750,f2136]) ).
fof(f2758,plain,
! [X0] : sF177(X0) = sF170(sK141(X0),sK142(X0)),
inference(forward_demodulation,[],[f2751,f2144]) ).
fof(f2760,plain,
! [X0,X1] : sF174(sK141(X0),X1) = sF170(sF178(X0),sF171(X1)),
inference(superposition,[],[f2757,f2194]) ).
fof(f2774,plain,
! [X0,X1] :
( sF177(X0) != sK140(X1)
| ~ in(sK140(X1),sF168)
| ~ in(sF174(sK141(X0),sK142(X0)),sK138)
| ~ in(sK140(X1),X1) ),
inference(superposition,[],[f2137,f2758]) ).
fof(f2842,plain,
! [X0,X1] : sF174(sK141(X1),sK142(X0)) = sF170(sF178(X1),sF179(X0)),
inference(superposition,[],[f2760,f2195]) ).
fof(f4858,plain,
! [X2,X0,X1] :
( sK140(sK125(X2,X0,X1)) = unordered_pair(unordered_pair(sK127(X0,X1,sK140(sK125(X2,X0,X1))),sK128(X0,X1,sK140(sK125(X2,X0,X1)))),unordered_pair(sK127(X0,X1,sK140(sK125(X2,X0,X1))),sK127(X0,X1,sK140(sK125(X2,X0,X1)))))
| sP2(X0,X1)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1)
| in(sF182(sK125(X2,X0,X1)),sK138) ),
inference(resolution,[],[f1923,f2156]) ).
fof(f4869,plain,
! [X2,X0,X1] :
( sK140(sK125(X2,X0,X1)) = unordered_pair(unordered_pair(sK127(X0,X1,sK140(sK125(X2,X0,X1))),sK128(X0,X1,sK140(sK125(X2,X0,X1)))),sF169(sK127(X0,X1,sK140(sK125(X2,X0,X1)))))
| sP2(X0,X1)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1)
| in(sF182(sK125(X2,X0,X1)),sK138) ),
inference(forward_demodulation,[],[f4858,f2126]) ).
fof(f4881,plain,
! [X2,X0,X1] :
( in(sF182(sK125(X2,X0,X1)),sK138)
| sP2(X0,X1)
| ~ relation(X0)
| ~ relation(X1)
| ~ function(X1)
| sK140(sK125(X2,X0,X1)) = sF170(sK127(X0,X1,sK140(sK125(X2,X0,X1))),sK128(X0,X1,sK140(sK125(X2,X0,X1)))) ),
inference(forward_demodulation,[],[f4869,f2128]) ).
fof(f5933,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(apply(sK139,X1),sF171(X0)),unordered_pair(apply(sK139,X1),apply(sK139,X1))),X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),cartesian_product2(X3,X3))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2)
| ~ relation(sK139)
| ~ function(sK139) ),
inference(superposition,[],[f2100,f2130]) ).
fof(f5952,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(apply(sK139,X1),sF171(X0)),unordered_pair(apply(sK139,X1),apply(sK139,X1))),X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),cartesian_product2(X3,X3))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2)
| ~ function(sK139) ),
inference(forward_subsumption_resolution,[],[f5933,f1517]) ).
fof(f5968,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(apply(sK139,X1),sF171(X0)),unordered_pair(apply(sK139,X1),apply(sK139,X1))),X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),cartesian_product2(X3,X3))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_subsumption_resolution,[],[f5952,f1516]) ).
fof(f5984,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(apply(sK139,X1),sF171(X0)),sF169(apply(sK139,X1))),X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),cartesian_product2(X3,X3))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f5968,f2126]) ).
fof(f6000,plain,
! [X2,X3,X0,X1] :
( ~ in(sF170(apply(sK139,X1),sF171(X0)),X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),cartesian_product2(X3,X3))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f5984,f2128]) ).
fof(f6016,plain,
! [X2,X3,X0,X1] :
( ~ in(sF170(sF171(X1),sF171(X0)),X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),cartesian_product2(X3,X3))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6000,f2130]) ).
fof(f6026,plain,
! [X2,X3,X0,X1] :
( ~ in(sF174(X1,X0),X2)
| ~ in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),cartesian_product2(X3,X3))
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6016,f2757]) ).
fof(f6032,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X1,X0),sF169(X1)),cartesian_product2(X3,X3))
| ~ in(sF174(X1,X0),X2)
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6026,f2126]) ).
fof(f6037,plain,
! [X2,X3,X0,X1] :
( ~ in(sF170(X1,X0),cartesian_product2(X3,X3))
| ~ in(sF174(X1,X0),X2)
| in(unordered_pair(unordered_pair(X1,X0),unordered_pair(X1,X1)),sK125(X3,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6032,f2128]) ).
fof(f6041,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X1,X0),sF169(X1)),sK125(X3,X2,sK139))
| ~ in(sF170(X1,X0),cartesian_product2(X3,X3))
| ~ in(sF174(X1,X0),X2)
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6037,f2126]) ).
fof(f6044,plain,
! [X2,X3,X0,X1] :
( ~ in(sF170(X1,X0),cartesian_product2(X3,X3))
| in(sF170(X1,X0),sK125(X3,X2,sK139))
| ~ in(sF174(X1,X0),X2)
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6041,f2128]) ).
fof(f6201,plain,
! [X2,X0,X1] :
( ~ in(sF177(X0),cartesian_product2(X1,X1))
| in(sF177(X0),sK125(X1,X2,sK139))
| ~ in(sF174(sK141(X0),sK142(X0)),X2)
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(superposition,[],[f6044,f2758]) ).
fof(f6209,plain,
! [X2,X0,X1] :
( ~ in(sF170(sF178(X0),sF179(X0)),X2)
| ~ in(sF177(X0),cartesian_product2(X1,X1))
| in(sF177(X0),sK125(X1,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6201,f2842]) ).
fof(f6212,plain,
! [X2,X0,X1] :
( ~ in(sF177(X0),cartesian_product2(X1,X1))
| ~ in(sF182(X0),X2)
| in(sF177(X0),sK125(X1,X2,sK139))
| sP2(X2,sK139)
| ~ relation(X2) ),
inference(forward_demodulation,[],[f6209,f2756]) ).
fof(f6641,plain,
! [X0,X1] :
( in(sF177(X0),sK125(sK137,X1,sK139))
| ~ in(sF182(X0),X1)
| ~ in(sF177(X0),sF168)
| sP2(X1,sK139)
| ~ relation(X1) ),
inference(superposition,[],[f6212,f2124]) ).
fof(f6996,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK128(X1,X0,sK140(sK125(X2,X1,X0))))),unordered_pair(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))))),X1)
| sP2(X1,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X0)
| in(sF182(sK125(X2,X1,X0)),sK138) ),
inference(resolution,[],[f1924,f2156]) ).
fof(f6997,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK128(X1,X0,sK140(sK125(X2,X1,X0))))),unordered_pair(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))))),X1)
| sP2(X1,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X0)
| sK140(sK125(X2,X1,X0)) = sF177(sK125(X2,X1,X0)) ),
inference(resolution,[],[f1924,f2145]) ).
fof(f7016,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK128(X1,X0,sK140(sK125(X2,X1,X0))))),sF169(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))))),X1)
| sP2(X1,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X0)
| sK140(sK125(X2,X1,X0)) = sF177(sK125(X2,X1,X0)) ),
inference(forward_demodulation,[],[f6997,f2126]) ).
fof(f7017,plain,
! [X2,X0,X1] :
( in(unordered_pair(unordered_pair(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK128(X1,X0,sK140(sK125(X2,X1,X0))))),sF169(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))))),X1)
| sP2(X1,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X0)
| in(sF182(sK125(X2,X1,X0)),sK138) ),
inference(forward_demodulation,[],[f6996,f2126]) ).
fof(f7037,plain,
! [X2,X0,X1] :
( in(sF170(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK128(X1,X0,sK140(sK125(X2,X1,X0))))),X1)
| sP2(X1,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X0)
| sK140(sK125(X2,X1,X0)) = sF177(sK125(X2,X1,X0)) ),
inference(forward_demodulation,[],[f7016,f2128]) ).
fof(f7038,plain,
! [X2,X0,X1] :
( in(sF170(apply(X0,sK127(X1,X0,sK140(sK125(X2,X1,X0)))),apply(X0,sK128(X1,X0,sK140(sK125(X2,X1,X0))))),X1)
| sP2(X1,X0)
| ~ relation(X1)
| ~ relation(X0)
| ~ function(X0)
| in(sF182(sK125(X2,X1,X0)),sK138) ),
inference(forward_demodulation,[],[f7017,f2128]) ).
fof(f7135,plain,
! [X0,X1] :
( in(sF170(apply(sK139,sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| ~ relation(sK139)
| ~ function(sK139)
| in(sF182(sK125(X1,X0,sK139)),sK138) ),
inference(superposition,[],[f7038,f2130]) ).
fof(f7137,plain,
! [X0,X1] :
( in(sF170(apply(sK139,sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| ~ function(sK139)
| in(sF182(sK125(X1,X0,sK139)),sK138) ),
inference(forward_subsumption_resolution,[],[f7135,f1517]) ).
fof(f7145,plain,
! [X0,X1] :
( in(sF170(apply(sK139,sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| in(sF182(sK125(X1,X0,sK139)),sK138) ),
inference(forward_subsumption_resolution,[],[f7137,f1516]) ).
fof(f7150,plain,
! [X0,X1] :
( in(sF170(sF171(sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| in(sF182(sK125(X1,X0,sK139)),sK138) ),
inference(forward_demodulation,[],[f7145,f2130]) ).
fof(f7152,plain,
! [X0,X1] :
( in(sF174(sK127(X0,sK139,sK140(sK125(X1,X0,sK139))),sK128(X0,sK139,sK140(sK125(X1,X0,sK139)))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| in(sF182(sK125(X1,X0,sK139)),sK138) ),
inference(forward_demodulation,[],[f7150,f2757]) ).
fof(f7252,plain,
! [X0,X1] :
( in(sF170(apply(sK139,sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(X1,X0,sK139)) = sF177(sK125(X1,X0,sK139)) ),
inference(superposition,[],[f7037,f2130]) ).
fof(f7254,plain,
! [X0,X1] :
( in(sF170(apply(sK139,sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| ~ function(sK139)
| sK140(sK125(X1,X0,sK139)) = sF177(sK125(X1,X0,sK139)) ),
inference(forward_subsumption_resolution,[],[f7252,f1517]) ).
fof(f7262,plain,
! [X0,X1] :
( in(sF170(apply(sK139,sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| sK140(sK125(X1,X0,sK139)) = sF177(sK125(X1,X0,sK139)) ),
inference(forward_subsumption_resolution,[],[f7254,f1516]) ).
fof(f7267,plain,
! [X0,X1] :
( in(sF170(sF171(sK127(X0,sK139,sK140(sK125(X1,X0,sK139)))),sF171(sK128(X0,sK139,sK140(sK125(X1,X0,sK139))))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| sK140(sK125(X1,X0,sK139)) = sF177(sK125(X1,X0,sK139)) ),
inference(forward_demodulation,[],[f7262,f2130]) ).
fof(f7269,plain,
! [X0,X1] :
( in(sF174(sK127(X0,sK139,sK140(sK125(X1,X0,sK139))),sK128(X0,sK139,sK140(sK125(X1,X0,sK139)))),X0)
| sP2(X0,sK139)
| ~ relation(X0)
| sK140(sK125(X1,X0,sK139)) = sF177(sK125(X1,X0,sK139)) ),
inference(forward_demodulation,[],[f7267,f2757]) ).
fof(f11219,definition,
( spl183_170
<=> sP2(sK138,sK139) ),
introduced(definition,[new_symbols(definition,[spl183_170])],[avatar_definition]) ).
fof(f11220,plain,
( ~ sP2(sK138,sK139)
| spl183_170 ),
inference(avatar_component_clause,[],[f11219]) ).
fof(f11221,plain,
( sP2(sK138,sK139)
| ~ spl183_170 ),
inference(avatar_component_clause,[],[f11219]) ).
fof(f11299,plain,
( sK118(sK138,sK139) = sK119(sK138,sK139)
| ~ spl183_170 ),
inference(resolution,[],[f11221,f1493]) ).
fof(f11300,plain,
( sK118(sK138,sK139) = sK120(sK138,sK139)
| ~ spl183_170 ),
inference(resolution,[],[f11221,f1490]) ).
fof(f11301,plain,
( sK119(sK138,sK139) = sK120(sK138,sK139)
| ~ spl183_170 ),
inference(forward_demodulation,[],[f11299,f11300]) ).
fof(f11302,plain,
( sK119(sK138,sK139) != sK119(sK138,sK139)
| ~ sP2(sK138,sK139)
| ~ spl183_170 ),
inference(superposition,[],[f1494,f11301]) ).
fof(f11303,plain,
( ~ sP2(sK138,sK139)
| ~ spl183_170 ),
inference(trivial_inequality_removal,[],[f11302]) ).
fof(f11304,plain,
( $false
| ~ spl183_170 ),
inference(forward_subsumption_resolution,[],[f11303,f11221]) ).
fof(f11305,plain,
~ spl183_170,
inference(avatar_contradiction_clause,[],[f11304]) ).
fof(f11638,plain,
( ! [X0] :
( sK140(sK125(X0,sK138,sK139)) = sK126(X0,sK138,sK139,sK140(sK125(X0,sK138,sK139)))
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(X0,sK138,sK139)) = sF177(sK125(X0,sK138,sK139)) )
| spl183_170 ),
inference(resolution,[],[f11220,f2630]) ).
fof(f11639,plain,
( ! [X0] :
( sK140(sK125(X0,sK138,sK139)) = sK126(X0,sK138,sK139,sK140(sK125(X0,sK138,sK139)))
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(X0,sK138,sK139)) = sF177(sK125(X0,sK138,sK139)) )
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11638,f1518]) ).
fof(f11641,plain,
( ! [X0] :
( sK140(sK125(X0,sK138,sK139)) = sK126(X0,sK138,sK139,sK140(sK125(X0,sK138,sK139)))
| ~ function(sK139)
| sK140(sK125(X0,sK138,sK139)) = sF177(sK125(X0,sK138,sK139)) )
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11639,f1517]) ).
fof(f11643,plain,
( ! [X0] :
( sK140(sK125(X0,sK138,sK139)) = sK126(X0,sK138,sK139,sK140(sK125(X0,sK138,sK139)))
| sK140(sK125(X0,sK138,sK139)) = sF177(sK125(X0,sK138,sK139)) )
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11641,f1516]) ).
fof(f11646,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| sP2(sK138,sK139)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170 ),
inference(superposition,[],[f2566,f11643]) ).
fof(f11647,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| sP2(sK138,sK139)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11646,f2138]) ).
fof(f11649,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11647,f11220]) ).
fof(f11651,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11649,f1518]) ).
fof(f11653,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11651,f1517]) ).
fof(f11655,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170 ),
inference(forward_subsumption_resolution,[],[f11653,f1516]) ).
fof(f11658,definition,
( spl183_211
<=> sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139)) ),
introduced(definition,[new_symbols(definition,[spl183_211])],[avatar_definition]) ).
fof(f11659,plain,
( sK140(sK125(sK137,sK138,sK139)) != sF177(sK125(sK137,sK138,sK139))
| spl183_211 ),
inference(avatar_component_clause,[],[f11658]) ).
fof(f11660,plain,
( sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| ~ spl183_211 ),
inference(avatar_component_clause,[],[f11658]) ).
fof(f11662,definition,
( spl183_212
<=> in(sK140(sK125(sK137,sK138,sK139)),sF168) ),
introduced(definition,[new_symbols(definition,[spl183_212])],[avatar_definition]) ).
fof(f11663,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sF168)
| spl183_212 ),
inference(avatar_component_clause,[],[f11662]) ).
fof(f11664,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ spl183_212 ),
inference(avatar_component_clause,[],[f11662]) ).
fof(f11665,plain,
( spl183_211
| spl183_212
| spl183_170 ),
inference(avatar_split_clause,[],[f11655,f11219,f11662,f11658]) ).
fof(f11678,plain,
( ! [X0] :
( sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),sF168)
| ~ in(sF174(sK141(sK125(sK137,sK138,sK139)),sK142(sK125(sK137,sK138,sK139))),sK138)
| ~ in(sK140(X0),X0) )
| ~ spl183_211 ),
inference(superposition,[],[f2774,f11660]) ).
fof(f11682,plain,
( ! [X0] :
( in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,X0,sK139))
| ~ in(sF182(sK125(sK137,sK138,sK139)),X0)
| ~ in(sK140(sK125(sK137,sK138,sK139)),sF168)
| sP2(X0,sK139)
| ~ relation(X0) )
| ~ spl183_211 ),
inference(superposition,[],[f6641,f11660]) ).
fof(f11697,definition,
( spl183_215
<=> ! [X0] :
( in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,X0,sK139))
| ~ relation(X0)
| sP2(X0,sK139)
| ~ in(sF182(sK125(sK137,sK138,sK139)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl183_215])],[avatar_definition]) ).
fof(f11698,plain,
( ! [X0] :
( in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,X0,sK139))
| ~ relation(X0)
| sP2(X0,sK139)
| ~ in(sF182(sK125(sK137,sK138,sK139)),X0) )
| ~ spl183_215 ),
inference(avatar_component_clause,[],[f11697]) ).
fof(f11699,plain,
( ~ spl183_212
| spl183_215
| ~ spl183_211 ),
inference(avatar_split_clause,[],[f11682,f11658,f11697,f11662]) ).
fof(f11700,plain,
( ! [X0] :
( ~ in(sF170(sF178(sK125(sK137,sK138,sK139)),sF179(sK125(sK137,sK138,sK139))),sK138)
| sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),sF168)
| ~ in(sK140(X0),X0) )
| ~ spl183_211 ),
inference(forward_demodulation,[],[f11678,f2842]) ).
fof(f11717,definition,
( spl183_218
<=> sK140(sK125(sK137,sK138,sK139)) = sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139))) ),
introduced(definition,[new_symbols(definition,[spl183_218])],[avatar_definition]) ).
fof(f11718,plain,
( sK140(sK125(sK137,sK138,sK139)) != sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139)))
| spl183_218 ),
inference(avatar_component_clause,[],[f11717]) ).
fof(f11719,plain,
( sK140(sK125(sK137,sK138,sK139)) = sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139)))
| ~ spl183_218 ),
inference(avatar_component_clause,[],[f11717]) ).
fof(f11721,definition,
( spl183_219
<=> in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139)) ),
introduced(definition,[new_symbols(definition,[spl183_219])],[avatar_definition]) ).
fof(f11722,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| spl183_219 ),
inference(avatar_component_clause,[],[f11721]) ).
fof(f11723,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| ~ spl183_219 ),
inference(avatar_component_clause,[],[f11721]) ).
fof(f11725,plain,
( ! [X0] :
( ~ in(sF182(sK125(sK137,sK138,sK139)),sK138)
| sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),sF168)
| ~ in(sK140(X0),X0) )
| ~ spl183_211 ),
inference(forward_demodulation,[],[f11700,f2756]) ).
fof(f11727,definition,
( spl183_220
<=> ! [X0] :
( sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),X0)
| ~ in(sK140(X0),sF168) ) ),
introduced(definition,[new_symbols(definition,[spl183_220])],[avatar_definition]) ).
fof(f11728,plain,
( ! [X0] :
( sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),X0)
| ~ in(sK140(X0),sF168) )
| ~ spl183_220 ),
inference(avatar_component_clause,[],[f11727]) ).
fof(f11730,definition,
( spl183_221
<=> in(sF182(sK125(sK137,sK138,sK139)),sK138) ),
introduced(definition,[new_symbols(definition,[spl183_221])],[avatar_definition]) ).
fof(f11731,plain,
( in(sF182(sK125(sK137,sK138,sK139)),sK138)
| ~ spl183_221 ),
inference(avatar_component_clause,[],[f11730]) ).
fof(f11732,plain,
( ~ in(sF182(sK125(sK137,sK138,sK139)),sK138)
| spl183_221 ),
inference(avatar_component_clause,[],[f11730]) ).
fof(f11733,plain,
( spl183_220
| ~ spl183_221
| ~ spl183_211 ),
inference(avatar_split_clause,[],[f11725,f11658,f11730,f11727]) ).
fof(f11756,definition,
( spl183_222
<=> in(sF174(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),sK138) ),
introduced(definition,[new_symbols(definition,[spl183_222])],[avatar_definition]) ).
fof(f11757,plain,
( in(sF174(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),sK138)
| ~ spl183_222 ),
inference(avatar_component_clause,[],[f11756]) ).
fof(f11758,plain,
( ~ in(sF174(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),sK138)
| spl183_222 ),
inference(avatar_component_clause,[],[f11756]) ).
fof(f11769,plain,
( sP2(sK138,sK139)
| ~ relation(sK138)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_222 ),
inference(resolution,[],[f11758,f7269]) ).
fof(f11770,plain,
( sP2(sK138,sK139)
| ~ relation(sK138)
| in(sF182(sK125(sK137,sK138,sK139)),sK138)
| spl183_222 ),
inference(resolution,[],[f11758,f7152]) ).
fof(f11775,plain,
( ~ relation(sK138)
| in(sF182(sK125(sK137,sK138,sK139)),sK138)
| spl183_170
| spl183_222 ),
inference(forward_subsumption_resolution,[],[f11770,f11220]) ).
fof(f11777,plain,
( in(sF182(sK125(sK137,sK138,sK139)),sK138)
| spl183_170
| spl183_222 ),
inference(forward_subsumption_resolution,[],[f11775,f1518]) ).
fof(f11780,plain,
( $false
| spl183_170
| spl183_221
| spl183_222 ),
inference(forward_subsumption_resolution,[],[f11777,f11732]) ).
fof(f11781,plain,
( spl183_170
| spl183_221
| spl183_222 ),
inference(avatar_contradiction_clause,[],[f11780]) ).
fof(f11792,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| ~ in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ spl183_220 ),
inference(equality_resolution,[],[f11728]) ).
fof(f11793,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| sP2(sK138,sK139)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| ~ spl183_218 ),
inference(superposition,[],[f2566,f11719]) ).
fof(f11796,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| sP2(sK138,sK139)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| spl183_212
| ~ spl183_218 ),
inference(forward_subsumption_resolution,[],[f11793,f11663]) ).
fof(f11798,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| spl183_170
| spl183_212
| ~ spl183_218 ),
inference(forward_subsumption_resolution,[],[f11796,f11220]) ).
fof(f11800,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| ~ relation(sK139)
| ~ function(sK139)
| spl183_170
| spl183_212
| ~ spl183_218 ),
inference(forward_subsumption_resolution,[],[f11798,f1518]) ).
fof(f11802,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| ~ function(sK139)
| spl183_170
| spl183_212
| ~ spl183_218 ),
inference(forward_subsumption_resolution,[],[f11800,f1517]) ).
fof(f11804,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sK125(sK137,sK138,sK139))
| spl183_170
| spl183_212
| ~ spl183_218 ),
inference(forward_subsumption_resolution,[],[f11802,f1516]) ).
fof(f11806,plain,
( ~ spl183_219
| spl183_170
| spl183_212
| ~ spl183_218 ),
inference(avatar_split_clause,[],[f11804,f11717,f11662,f11219,f11721]) ).
fof(f11875,plain,
( in(sF182(sK125(sK137,sK138,sK139)),sK138)
| spl183_219 ),
inference(resolution,[],[f11722,f2156]) ).
fof(f11876,plain,
( sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_219 ),
inference(resolution,[],[f11722,f2145]) ).
fof(f11877,plain,
( in(sK140(sK125(sK137,sK138,sK139)),sF168)
| spl183_219 ),
inference(resolution,[],[f11722,f2138]) ).
fof(f11880,plain,
( $false
| spl183_212
| spl183_219 ),
inference(forward_subsumption_resolution,[],[f11877,f11663]) ).
fof(f11881,plain,
( spl183_212
| spl183_219 ),
inference(avatar_contradiction_clause,[],[f11880]) ).
fof(f11882,plain,
( $false
| spl183_219
| spl183_221 ),
inference(forward_subsumption_resolution,[],[f11875,f11732]) ).
fof(f11883,plain,
( spl183_219
| spl183_221 ),
inference(avatar_contradiction_clause,[],[f11882]) ).
fof(f11885,plain,
( $false
| spl183_211
| spl183_219 ),
inference(forward_subsumption_resolution,[],[f11876,f11659]) ).
fof(f11886,plain,
( spl183_211
| spl183_219 ),
inference(avatar_contradiction_clause,[],[f11885]) ).
fof(f11921,plain,
( sP2(sK138,sK139)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139)))
| spl183_212 ),
inference(resolution,[],[f11663,f2631]) ).
fof(f11924,plain,
( ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139)))
| spl183_170
| spl183_212 ),
inference(forward_subsumption_resolution,[],[f11921,f11220]) ).
fof(f11926,plain,
( ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139)))
| spl183_170
| spl183_212 ),
inference(forward_subsumption_resolution,[],[f11924,f1518]) ).
fof(f11928,plain,
( ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139)))
| spl183_170
| spl183_212 ),
inference(forward_subsumption_resolution,[],[f11926,f1517]) ).
fof(f11930,plain,
( sK140(sK125(sK137,sK138,sK139)) = sK126(sK137,sK138,sK139,sK140(sK125(sK137,sK138,sK139)))
| spl183_170
| spl183_212 ),
inference(forward_subsumption_resolution,[],[f11928,f1516]) ).
fof(f11932,plain,
( $false
| spl183_170
| spl183_212
| spl183_218 ),
inference(forward_subsumption_resolution,[],[f11930,f11718]) ).
fof(f11933,plain,
( spl183_170
| spl183_212
| spl183_218 ),
inference(avatar_contradiction_clause,[],[f11932]) ).
fof(f11934,plain,
( ~ in(sK140(sK125(sK137,sK138,sK139)),sF168)
| ~ spl183_219
| ~ spl183_220 ),
inference(forward_subsumption_resolution,[],[f11792,f11723]) ).
fof(f11937,plain,
( $false
| ~ spl183_212
| ~ spl183_219
| ~ spl183_220 ),
inference(forward_subsumption_resolution,[],[f11934,f11664]) ).
fof(f11938,plain,
( ~ spl183_212
| ~ spl183_219
| ~ spl183_220 ),
inference(avatar_contradiction_clause,[],[f11937]) ).
fof(f11947,plain,
( sP2(sK138,sK139)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF170(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139))))
| spl183_221 ),
inference(resolution,[],[f11732,f4881]) ).
fof(f11952,plain,
( ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF170(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139))))
| spl183_170
| spl183_221 ),
inference(forward_subsumption_resolution,[],[f11947,f11220]) ).
fof(f11954,plain,
( ~ relation(sK139)
| ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF170(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139))))
| spl183_170
| spl183_221 ),
inference(forward_subsumption_resolution,[],[f11952,f1518]) ).
fof(f11956,plain,
( ~ function(sK139)
| sK140(sK125(sK137,sK138,sK139)) = sF170(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139))))
| spl183_170
| spl183_221 ),
inference(forward_subsumption_resolution,[],[f11954,f1517]) ).
fof(f11958,plain,
( sK140(sK125(sK137,sK138,sK139)) = sF170(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139))))
| spl183_170
| spl183_221 ),
inference(forward_subsumption_resolution,[],[f11956,f1516]) ).
fof(f11960,plain,
( ! [X0] :
( sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),sF168)
| ~ in(sF174(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),sK138)
| ~ in(sK140(X0),X0) )
| spl183_170
| spl183_221 ),
inference(superposition,[],[f2137,f11958]) ).
fof(f11973,plain,
( ! [X0] :
( sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),sF168)
| ~ in(sK140(X0),X0) )
| spl183_170
| spl183_221
| ~ spl183_222 ),
inference(forward_subsumption_resolution,[],[f11960,f11757]) ).
fof(f11977,plain,
( spl183_220
| spl183_170
| spl183_221
| ~ spl183_222 ),
inference(avatar_split_clause,[],[f11973,f11756,f11730,f11219,f11727]) ).
fof(f11994,plain,
( sK140(sK125(sK137,sK138,sK139)) = unordered_pair(unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))))
| sP2(sK138,sK139)
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| ~ spl183_219 ),
inference(resolution,[],[f11723,f1923]) ).
fof(f11998,plain,
( sK140(sK125(sK137,sK138,sK139)) = unordered_pair(unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))))
| ~ relation(sK138)
| ~ relation(sK139)
| ~ function(sK139)
| spl183_170
| ~ spl183_219 ),
inference(forward_subsumption_resolution,[],[f11994,f11220]) ).
fof(f12000,plain,
( sK140(sK125(sK137,sK138,sK139)) = unordered_pair(unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))))
| ~ relation(sK139)
| ~ function(sK139)
| spl183_170
| ~ spl183_219 ),
inference(forward_subsumption_resolution,[],[f11998,f1518]) ).
fof(f12002,plain,
( sK140(sK125(sK137,sK138,sK139)) = unordered_pair(unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))))
| ~ function(sK139)
| spl183_170
| ~ spl183_219 ),
inference(forward_subsumption_resolution,[],[f12000,f1517]) ).
fof(f12004,plain,
( sK140(sK125(sK137,sK138,sK139)) = unordered_pair(unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))))
| spl183_170
| ~ spl183_219 ),
inference(forward_subsumption_resolution,[],[f12002,f1516]) ).
fof(f12006,plain,
( sK140(sK125(sK137,sK138,sK139)) = unordered_pair(unordered_pair(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),sF169(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))))
| spl183_170
| ~ spl183_219 ),
inference(forward_demodulation,[],[f12004,f2126]) ).
fof(f12008,plain,
( sK140(sK125(sK137,sK138,sK139)) = sF170(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139))))
| spl183_170
| ~ spl183_219 ),
inference(forward_demodulation,[],[f12006,f2128]) ).
fof(f12052,plain,
( ! [X0] :
( sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),sF168)
| ~ in(sF174(sK127(sK138,sK139,sK140(sK125(sK137,sK138,sK139))),sK128(sK138,sK139,sK140(sK125(sK137,sK138,sK139)))),sK138)
| ~ in(sK140(X0),X0) )
| spl183_170
| ~ spl183_219 ),
inference(superposition,[],[f2137,f12008]) ).
fof(f12065,plain,
( ! [X0] :
( sK140(X0) != sK140(sK125(sK137,sK138,sK139))
| ~ in(sK140(X0),sF168)
| ~ in(sK140(X0),X0) )
| spl183_170
| ~ spl183_219
| ~ spl183_222 ),
inference(forward_subsumption_resolution,[],[f12052,f11757]) ).
fof(f12068,plain,
( spl183_220
| spl183_170
| ~ spl183_219
| ~ spl183_222 ),
inference(avatar_split_clause,[],[f12065,f11756,f11721,f11219,f11727]) ).
fof(f12069,plain,
( ~ relation(sK138)
| sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170
| spl183_222 ),
inference(forward_subsumption_resolution,[],[f11769,f11220]) ).
fof(f12072,plain,
( sK140(sK125(sK137,sK138,sK139)) = sF177(sK125(sK137,sK138,sK139))
| spl183_170
| spl183_222 ),
inference(forward_subsumption_resolution,[],[f12069,f1518]) ).
fof(f12073,plain,
( $false
| spl183_170
| spl183_211
| spl183_222 ),
inference(forward_subsumption_resolution,[],[f12072,f11659]) ).
fof(f12074,plain,
( spl183_170
| spl183_211
| spl183_222 ),
inference(avatar_contradiction_clause,[],[f12073]) ).
fof(f14563,plain,
( ~ relation(sK138)
| sP2(sK138,sK139)
| ~ in(sF182(sK125(sK137,sK138,sK139)),sK138)
| ~ spl183_215
| spl183_219 ),
inference(resolution,[],[f11698,f11722]) ).
fof(f14576,plain,
( sP2(sK138,sK139)
| ~ in(sF182(sK125(sK137,sK138,sK139)),sK138)
| ~ spl183_215
| spl183_219 ),
inference(forward_subsumption_resolution,[],[f14563,f1518]) ).
fof(f14580,plain,
( ~ in(sF182(sK125(sK137,sK138,sK139)),sK138)
| spl183_170
| ~ spl183_215
| spl183_219 ),
inference(forward_subsumption_resolution,[],[f14576,f11220]) ).
fof(f14583,plain,
( $false
| spl183_170
| ~ spl183_215
| spl183_219
| ~ spl183_221 ),
inference(forward_subsumption_resolution,[],[f14580,f11731]) ).
fof(f14584,plain,
( spl183_170
| ~ spl183_215
| spl183_219
| ~ spl183_221 ),
inference(avatar_contradiction_clause,[],[f14583]) ).
cnf(s166,plain,
~ spl183_170,
inference(sat_conversion,[],[f11305]) ).
cnf(s189,plain,
( spl183_170
| spl183_211
| spl183_212 ),
inference(sat_conversion,[],[f11665]) ).
cnf(s191,plain,
( ~ spl183_211
| ~ spl183_212
| spl183_215 ),
inference(sat_conversion,[],[f11699]) ).
cnf(s195,plain,
( ~ spl183_211
| spl183_220
| ~ spl183_221 ),
inference(sat_conversion,[],[f11733]) ).
cnf(s199,plain,
( spl183_170
| spl183_221
| spl183_222 ),
inference(sat_conversion,[],[f11781]) ).
cnf(s200,plain,
( spl183_170
| spl183_212
| ~ spl183_218
| ~ spl183_219 ),
inference(sat_conversion,[],[f11806]) ).
cnf(s208,plain,
( spl183_212
| spl183_219 ),
inference(sat_conversion,[],[f11881]) ).
cnf(s209,plain,
( spl183_219
| spl183_221 ),
inference(sat_conversion,[],[f11883]) ).
cnf(s211,plain,
( spl183_211
| spl183_219 ),
inference(sat_conversion,[],[f11886]) ).
cnf(s212,plain,
( spl183_170
| spl183_212
| spl183_218 ),
inference(sat_conversion,[],[f11933]) ).
cnf(s213,plain,
( ~ spl183_212
| ~ spl183_219
| ~ spl183_220 ),
inference(sat_conversion,[],[f11938]) ).
cnf(s218,plain,
( spl183_170
| spl183_220
| spl183_221
| ~ spl183_222 ),
inference(sat_conversion,[],[f11977]) ).
cnf(s224,plain,
( spl183_170
| ~ spl183_219
| spl183_220
| ~ spl183_222 ),
inference(sat_conversion,[],[f12068]) ).
cnf(s226,plain,
( spl183_170
| spl183_211
| spl183_222 ),
inference(sat_conversion,[],[f12074]) ).
cnf(s293,plain,
( spl183_170
| ~ spl183_215
| spl183_219
| ~ spl183_221 ),
inference(sat_conversion,[],[f14584]) ).
cnf(s312,plain,
spl183_211,
inference(rat,[],[s213,s224,s189,s211,s226,s166]) ).
cnf(s314,plain,
( ~ spl183_221
| ~ spl183_212 ),
inference(rat,[],[s213,s293,s195,s191,s166,s312]) ).
cnf(s315,plain,
~ spl183_212,
inference(rat,[],[s213,s218,s199,s209,s314,s166]) ).
cnf(s316,plain,
spl183_218,
inference(rat,[],[s212,s166,s315]) ).
cnf(s317,plain,
spl183_219,
inference(rat,[],[s208,s315]) ).
cnf(s318,plain,
$false,
inference(rat,[],[s200,s317,s166,s316,s315]) ).
fof(f14590,plain,
$false,
inference(avatar_sat_refutation,[],[s318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU277+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 % Computer : n004.cluster.edu
% 0.10/0.41 % Model : x86_64 x86_64
% 0.10/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.41 % Memory : 8046.5625MB
% 0.10/0.41 % OS : Linux 6.8.0-71-generic
% 0.10/0.41 % CPULimit : 300
% 0.10/0.41 % WCLimit : 300
% 0.10/0.41 % DateTime : Mon Sep 28 04:27:08 UTC 2026
% 0.10/0.41 % CPUTime :
% 0.10/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.45 Running first-order theorem proving
% 0.10/0.45 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.41/2.88 % (4147363)Detected formulas, will run a generic FOF schedule.
% 13.41/2.88 % (4147369)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=2298220591:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.41/2.88 % (4147373)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2747463375:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.41/2.88 % (4147372)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3942690517:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.41/2.88 % (4147370)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=1049079525:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.41/2.88 % (4147368)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=1861665281:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.41/2.88 % (4147371)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3861780350:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.41/2.88 % (4147374)dis-21_1_sil=8000:lcm=predicate:random_seed=749348809: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)
% 13.41/2.88 % (4147371)Instruction limit reached!
% 13.41/2.88 % (4147371)------------------------------
% 13.41/2.88 % (4147371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.41/2.88 % (4147371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.41/2.88 % (4147371)CaDiCaL version: 2.1.3
% 13.41/2.88 % (4147371)Termination reason: Instruction limit
% 13.41/2.88 % (4147371)Termination phase: Saturation
% 13.41/2.88 % (4147371)Time elapsed: 0.066 s
% 13.41/2.88 % (4147371)Peak memory usage: 90 MB
% 13.41/2.88 % (4147371)Instructions burned: 110 (million)
% 13.41/2.88 % (4147374)Instruction limit reached!
% 13.41/2.88 % (4147374)------------------------------
% 13.41/2.88 % (4147374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.41/2.88 % (4147374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.41/2.88 % (4147374)CaDiCaL version: 2.1.3
% 13.41/2.88 % (4147374)Termination reason: Instruction limit
% 13.41/2.88 % (4147374)Termination phase: Saturation
% 13.41/2.88 % (4147374)Time elapsed: 0.067 s
% 13.41/2.88 % (4147374)Peak memory usage: 90 MB
% 13.41/2.88 % (4147374)Instructions burned: 131 (million)
% 13.41/2.88 % (4147372)Instruction limit reached!
% 13.41/2.88 % (4147372)------------------------------
% 13.41/2.88 % (4147372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.41/2.88 % (4147372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.41/2.88 % (4147372)CaDiCaL version: 2.1.3
% 13.41/2.88 % (4147372)Termination reason: Instruction limit
% 13.41/2.88 % (4147372)Termination phase: Saturation
% 13.41/2.88 % (4147372)Time elapsed: 0.076 s
% 13.41/2.88 % (4147372)Peak memory usage: 90 MB
% 13.41/2.88 % (4147372)Instructions burned: 119 (million)
% 13.41/2.88 % (4147373)Instruction limit reached!
% 13.41/2.88 % (4147373)------------------------------
% 13.41/2.88 % (4147373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.41/2.88 % (4147373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.41/2.88 % (4147373)CaDiCaL version: 2.1.3
% 13.41/2.88 % (4147373)Termination reason: Instruction limit
% 13.41/2.88 % (4147373)Termination phase: Saturation
% 13.41/2.88 % (4147373)Time elapsed: 0.092 s
% 13.41/2.88 % (4147373)Peak memory usage: 90 MB
% 13.41/2.88 % (4147373)Instructions burned: 140 (million)
% 13.41/2.88 % (4147382)lrs+10_1_sil=8000:sp=occurrence:random_seed=1289034414:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.41/2.88 % (4147384)lrs+1011_1_sil=32000:sp=occurrence:random_seed=857144519:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.41/2.88 % (4147383)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4011636756:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.41/2.88 % (4147385)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=4176801209:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.41/2.88 % (4147383)Instruction limit reached!
% 18.29/3.58 % (4147383)------------------------------
% 18.29/3.58 % (4147383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147383)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147383)Termination reason: Instruction limit
% 18.29/3.58 % (4147383)Termination phase: Saturation
% 18.29/3.58 % (4147383)Time elapsed: 0.085 s
% 18.29/3.58 % (4147383)Peak memory usage: 91 MB
% 18.29/3.58 % (4147383)Instructions burned: 158 (million)
% 18.29/3.58 % (4147382)Instruction limit reached!
% 18.29/3.58 % (4147382)------------------------------
% 18.29/3.58 % (4147382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147382)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147382)Termination reason: Instruction limit
% 18.29/3.58 % (4147382)Termination phase: Saturation
% 18.29/3.58 % (4147382)Time elapsed: 0.185 s
% 18.29/3.58 % (4147382)Peak memory usage: 94 MB
% 18.29/3.58 % (4147382)Instructions burned: 286 (million)
% 18.29/3.58 % (4147385)Instruction limit reached!
% 18.29/3.58 % (4147385)------------------------------
% 18.29/3.58 % (4147385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147385)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147385)Termination reason: Instruction limit
% 18.29/3.58 % (4147385)Termination phase: Saturation
% 18.29/3.58 % (4147385)Time elapsed: 0.144 s
% 18.29/3.58 % (4147385)Peak memory usage: 94 MB
% 18.29/3.58 % (4147385)Instructions burned: 250 (million)
% 18.29/3.58 % (4147384)Instruction limit reached!
% 18.29/3.58 % (4147384)------------------------------
% 18.29/3.58 % (4147384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147384)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147384)Termination reason: Instruction limit
% 18.29/3.58 % (4147384)Termination phase: Saturation
% 18.29/3.58 % (4147384)Time elapsed: 0.222 s
% 18.29/3.58 % (4147384)Peak memory usage: 93 MB
% 18.29/3.58 % (4147384)Instructions burned: 326 (million)
% 18.29/3.58 % (4147390)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=900768511:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.29/3.58 % (4147391)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=946096663:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 18.29/3.58 % (4147392)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=999812887:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 18.29/3.58 % (4147394)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1198870862:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 18.29/3.58 % (4147392)Instruction limit reached!
% 18.29/3.58 % (4147392)------------------------------
% 18.29/3.58 % (4147392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147392)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147392)Termination reason: Instruction limit
% 18.29/3.58 % (4147392)Termination phase: Saturation
% 18.29/3.58 % (4147392)Time elapsed: 0.070 s
% 18.29/3.58 % (4147392)Peak memory usage: 91 MB
% 18.29/3.58 % (4147392)Instructions burned: 113 (million)
% 18.29/3.58 % (4147390)Instruction limit reached!
% 18.29/3.58 % (4147390)------------------------------
% 18.29/3.58 % (4147390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147390)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147390)Termination reason: Instruction limit
% 18.29/3.58 % (4147390)Termination phase: Saturation
% 18.29/3.58 % (4147390)Time elapsed: 0.188 s
% 18.29/3.58 % (4147390)Peak memory usage: 91 MB
% 18.29/3.58 % (4147390)Instructions burned: 294 (million)
% 18.29/3.58 % (4147394)Instruction limit reached!
% 18.29/3.58 % (4147394)------------------------------
% 18.29/3.58 % (4147394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147394)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147394)Termination reason: Instruction limit
% 18.29/3.58 % (4147394)Termination phase: Saturation
% 18.29/3.58 % (4147394)Time elapsed: 0.066 s
% 18.29/3.58 % (4147394)Peak memory usage: 90 MB
% 18.29/3.58 % (4147394)Instructions burned: 129 (million)
% 18.29/3.58 % (4147398)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2641206382:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 18.29/3.58 % (4147399)lrs+10_1_sil=8000:sp=occurrence:random_seed=3650480343:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 18.29/3.58 % (4147400)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2360602900:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 18.29/3.58 % (4147398)Instruction limit reached!
% 18.29/3.58 % (4147398)------------------------------
% 18.29/3.58 % (4147398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147398)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147398)Termination reason: Instruction limit
% 18.29/3.58 % (4147398)Termination phase: Saturation
% 18.29/3.58 % (4147398)Time elapsed: 0.063 s
% 18.29/3.58 % (4147398)Peak memory usage: 89 MB
% 18.29/3.58 % (4147398)Instructions burned: 114 (million)
% 18.29/3.58 % (4147404)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3846113129:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 18.29/3.58 % (4147400)Instruction limit reached!
% 18.29/3.58 % (4147400)------------------------------
% 18.29/3.58 % (4147400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147400)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147400)Termination reason: Instruction limit
% 18.29/3.58 % (4147400)Termination phase: Saturation
% 18.29/3.58 % (4147400)Time elapsed: 0.265 s
% 18.29/3.58 % (4147400)Peak memory usage: 93 MB
% 18.29/3.58 % (4147400)Instructions burned: 438 (million)
% 18.29/3.58 % (4147406)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2393752019:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 18.29/3.58 % (4147406)Instruction limit reached!
% 18.29/3.58 % (4147406)------------------------------
% 18.29/3.58 % (4147406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147406)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147406)Termination reason: Instruction limit
% 18.29/3.58 % (4147406)Termination phase: Saturation
% 18.29/3.58 % (4147406)Time elapsed: 0.073 s
% 18.29/3.58 % (4147406)Peak memory usage: 92 MB
% 18.29/3.58 % (4147406)Instructions burned: 135 (million)
% 18.29/3.58 % (4147399)Instruction limit reached!
% 18.29/3.58 % (4147399)------------------------------
% 18.29/3.58 % (4147399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147399)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147399)Termination reason: Instruction limit
% 18.29/3.58 % (4147399)Termination phase: Saturation
% 18.29/3.58 % (4147399)Time elapsed: 0.564 s
% 18.29/3.58 % (4147399)Peak memory usage: 102 MB
% 18.29/3.58 % (4147399)Instructions burned: 907 (million)
% 18.29/3.58 % (4147408)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=311555642:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 18.29/3.58 % (4147409)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=24062145:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 18.29/3.58 % (4147408)Instruction limit reached!
% 18.29/3.58 % (4147408)------------------------------
% 18.29/3.58 % (4147408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147408)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147408)Termination reason: Instruction limit
% 18.29/3.58 % (4147408)Termination phase: Saturation
% 18.29/3.58 % (4147408)Time elapsed: 0.354 s
% 18.29/3.58 % (4147408)Peak memory usage: 99 MB
% 18.29/3.58 % (4147408)Instructions burned: 592 (million)
% 18.29/3.58 % (4147412)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=1268929469:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 18.29/3.58 % (4147412)Instruction limit reached!
% 18.29/3.58 % (4147412)------------------------------
% 18.29/3.58 % (4147412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147412)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147412)Termination reason: Instruction limit
% 18.29/3.58 % (4147412)Termination phase: Saturation
% 18.29/3.58 % (4147412)Time elapsed: 0.078 s
% 18.29/3.58 % (4147412)Peak memory usage: 91 MB
% 18.29/3.58 % (4147412)Instructions burned: 126 (million)
% 18.29/3.58 % (4147391)Instruction limit reached!
% 18.29/3.58 % (4147391)------------------------------
% 18.29/3.58 % (4147391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147391)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147391)Termination reason: Instruction limit
% 18.29/3.58 % (4147391)Termination phase: Saturation
% 18.29/3.58 % (4147391)Time elapsed: 1.480 s
% 18.29/3.58 % (4147391)Peak memory usage: 143 MB
% 18.29/3.58 % (4147391)Instructions burned: 2351 (million)
% 18.29/3.58 % (4147414)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4111571281:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 18.29/3.58 % (4147415)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4182497865:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 18.29/3.58 % (4147414)Instruction limit reached!
% 18.29/3.58 % (4147414)------------------------------
% 18.29/3.58 % (4147414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147414)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147414)Termination reason: Instruction limit
% 18.29/3.58 % (4147414)Termination phase: Saturation
% 18.29/3.58 % (4147414)Time elapsed: 0.081 s
% 18.29/3.58 % (4147414)Peak memory usage: 91 MB
% 18.29/3.58 % (4147414)Instructions burned: 135 (million)
% 18.29/3.58 % (4147415)Instruction limit reached!
% 18.29/3.58 % (4147415)------------------------------
% 18.29/3.58 % (4147415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147415)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147415)Termination reason: Instruction limit
% 18.29/3.58 % (4147415)Termination phase: Saturation
% 18.29/3.58 % (4147415)Time elapsed: 0.085 s
% 18.29/3.58 % (4147415)Peak memory usage: 92 MB
% 18.29/3.58 % (4147415)Instructions burned: 142 (million)
% 18.29/3.58 % (4147418)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3498578068:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 18.29/3.58 % (4147368)First to succeed.
% 18.29/3.58 % (4147368)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4147363"
% 18.29/3.58 % (4147419)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=4116920197:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 18.29/3.58 % (4147418)Instruction limit reached!
% 18.29/3.58 % (4147418)------------------------------
% 18.29/3.58 % (4147418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.58 % (4147418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.58 % (4147418)CaDiCaL version: 2.1.3
% 18.29/3.58 % (4147418)Termination reason: Instruction limit
% 18.29/3.58 % (4147418)Termination phase: Saturation
% 18.29/3.58 % (4147418)Time elapsed: 0.258 s
% 18.29/3.58 % (4147418)Peak memory usage: 94 MB
% 18.29/3.58 % (4147418)Instructions burned: 432 (million)
% 18.29/3.58 % (4147368)Refutation found. Thanks to Tanya!
% 18.29/3.58 % SZS status Theorem for theBenchmark
% 18.29/3.58 % SZS output start Proof for theBenchmark
% See solution above
% 19.61/3.78 % (4147368)------------------------------
% 19.61/3.78 % (4147368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.78 % (4147368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.78 % (4147368)CaDiCaL version: 2.1.3
% 19.61/3.78 % (4147368)Termination reason: Refutation
% 19.61/3.78 % (4147368)Time elapsed: 2.280 s
% 19.61/3.78 % (4147368)Peak memory usage: 153 MB
% 19.61/3.78 % (4147368)Instructions burned: 3481 (million)
% 19.61/3.78 % (4147368)------------------------------
% 19.61/3.78 % (4147368)------------------------------
% 19.61/3.78 % (4147363)Success in time 2.699 s
% 19.61/3.78 % Vampire exiting
%------------------------------------------------------------------------------