%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU416+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:51 PM UTC 2026
% Result : Theorem 11.46s 4.43s
% Output : Refutation 18.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 36
% Syntax : Number of formulae : 217 ( 39 unt; 18 def)
% Number of atoms : 568 ( 141 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 613 ( 262 ~; 282 |; 40 &)
% ( 26 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 19 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% Number of variables : 203 ( 0 sgn 193 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] :
( X1 = k1_tarski(X0)
<=> ! [X2] :
( r2_hidden(X2,X1)
<=> X2 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
fof(f32,axiom,
! [X0,X1,X2] :
( X2 = k4_xboole_0(X0,X1)
<=> ! [X3] :
( r2_hidden(X3,X2)
<=> ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f62,axiom,
! [X0] : k2_xboole_0(X0,k1_xboole_0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_boole) ).
fof(f109,axiom,
! [X0,X1] : k4_xboole_0(k2_xboole_0(X0,X1),X1) = k4_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t40_xboole_1) ).
fof(f110,axiom,
! [X0,X1,X2] : k4_xboole_0(k4_xboole_0(X0,X1),X2) = k4_xboole_0(X0,k2_xboole_0(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_xboole_1) ).
fof(f117,axiom,
! [X0,X1] : k4_xboole_0(X0,k4_xboole_0(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f122,axiom,
! [X0,X1,X2] : k4_xboole_0(X0,k2_xboole_0(X1,X2)) = k3_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t53_xboole_1) ).
fof(f123,axiom,
! [X0,X1,X2] : k4_xboole_0(X0,k3_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_xboole_1) ).
fof(f180,axiom,
! [X0,X1,X2] : k4_xboole_0(k3_xboole_0(X0,X1),k3_xboole_0(X2,X1)) = k3_xboole_0(k4_xboole_0(X0,X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t111_xboole_1) ).
fof(f376,axiom,
! [X0,X1] :
( k3_xboole_0(X0,k1_tarski(X1)) = k1_tarski(X1)
=> r2_hidden(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_zfmisc_1) ).
fof(f377,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> k3_xboole_0(X1,k1_tarski(X0)) = k1_tarski(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t52_zfmisc_1) ).
fof(f390,axiom,
! [X0,X1] :
( k4_xboole_0(X0,k1_tarski(X1)) = X0
<=> ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f392,axiom,
! [X0,X1] :
( k4_xboole_0(k1_tarski(X0),X1) = k1_tarski(X0)
<=> ~ r2_hidden(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t67_zfmisc_1) ).
fof(f393,axiom,
! [X0,X1] :
( k4_xboole_0(k1_tarski(X0),X1) = k1_xboole_0
<=> r2_hidden(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t68_zfmisc_1) ).
fof(f466,axiom,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
=> k4_xboole_0(k2_xboole_0(X1,k1_tarski(X0)),k1_tarski(X0)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t141_zfmisc_1) ).
fof(f14080,axiom,
! [X0] : k3_pua2mss1(X0) = k8_eqrel_1(X0,k6_partfun1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_pua2mss1) ).
fof(f19068,axiom,
! [X0,X1] :
( r2_hidden(X0,k3_pua2mss1(X1))
<=> ? [X2] :
( X0 = k1_tarski(X2)
& r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_relset_2) ).
fof(f19072,conjecture,
! [X0,X1] : k3_pua2mss1(k4_xboole_0(X0,X1)) = k4_xboole_0(k3_pua2mss1(X0),k3_pua2mss1(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_relset_2) ).
fof(f19073,negated_conjecture,
~ ! [X0,X1] : k3_pua2mss1(k4_xboole_0(X0,X1)) = k4_xboole_0(k3_pua2mss1(X0),k3_pua2mss1(X1)),
inference(negated_conjecture,[status(cth)],[f19072]) ).
fof(f19106,plain,
? [X0,X1] : k3_pua2mss1(k4_xboole_0(X0,X1)) != k4_xboole_0(k3_pua2mss1(X0),k3_pua2mss1(X1)),
inference(ennf_transformation,[],[f19073]) ).
fof(f19126,plain,
! [X0,X1] :
( k3_xboole_0(X1,k1_tarski(X0)) = k1_tarski(X0)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f377]) ).
fof(f19127,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| k1_tarski(X1) != k3_xboole_0(X0,k1_tarski(X1)) ),
inference(ennf_transformation,[],[f376]) ).
fof(f19376,plain,
! [X0,X1] :
( k4_xboole_0(k2_xboole_0(X1,k1_tarski(X0)),k1_tarski(X0)) = X1
| r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f466]) ).
fof(f19392,plain,
! [X0,X1] :
( ( r2_hidden(X0,k3_pua2mss1(X1))
| ! [X2] :
( k1_tarski(X2) != X0
| ~ r2_hidden(X2,X1) ) )
& ( ? [X2] :
( X0 = k1_tarski(X2)
& r2_hidden(X2,X1) )
| ~ r2_hidden(X0,k3_pua2mss1(X1)) ) ),
inference(nnf_transformation,[],[f19068]) ).
fof(f19393,plain,
! [X0,X1] :
( ( r2_hidden(X0,k3_pua2mss1(X1))
| ! [X2] :
( k1_tarski(X2) != X0
| ~ r2_hidden(X2,X1) ) )
& ( ? [X3] :
( k1_tarski(X3) = X0
& r2_hidden(X3,X1) )
| ~ r2_hidden(X0,k3_pua2mss1(X1)) ) ),
inference(rectify,[],[f19392]) ).
fof(f19394,plain,
! [X0,X1] :
( ( r2_hidden(X0,k3_pua2mss1(X1))
| ! [X2] :
( k1_tarski(X2) != X0
| ~ r2_hidden(X2,X1) ) )
& ( ( k1_tarski(sK0(X0,X1)) = X0
& r2_hidden(sK0(X0,X1),X1) )
| ~ r2_hidden(X0,k3_pua2mss1(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1))],[f19393]) ).
fof(f19396,plain,
k3_pua2mss1(k4_xboole_0(sK1,sK2)) != k4_xboole_0(k3_pua2mss1(sK1),k3_pua2mss1(sK2)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f19106]) ).
fof(f19445,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ? [X2] :
( ( X0 != X2
| ~ r2_hidden(X2,X1) )
& ( X2 = X0
| r2_hidden(X2,X1) ) ) )
& ( ! [X2] :
( ( r2_hidden(X2,X1)
| X0 != X2 )
& ( X2 = X0
| ~ r2_hidden(X2,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f19446,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ? [X2] :
( ( X0 != X2
| ~ r2_hidden(X2,X1) )
& ( X2 = X0
| r2_hidden(X2,X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ r2_hidden(X3,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(rectify,[],[f19445]) ).
fof(f19447,plain,
! [X0,X1] :
( ( X1 = k1_tarski(X0)
| ( ( sK41(X0,X1) != X0
| ~ r2_hidden(sK41(X0,X1),X1) )
& ( sK41(X0,X1) = X0
| r2_hidden(sK41(X0,X1),X1) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X1)
| X0 != X3 )
& ( X0 = X3
| ~ r2_hidden(X3,X1) ) )
| k1_tarski(X0) != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X2,sK41(X0,X1))],[f19446]) ).
fof(f19475,plain,
! [X0,X1] :
( ( k4_xboole_0(k1_tarski(X0),X1) = k1_xboole_0
| ~ r2_hidden(X0,X1) )
& ( r2_hidden(X0,X1)
| k1_xboole_0 != k4_xboole_0(k1_tarski(X0),X1) ) ),
inference(nnf_transformation,[],[f393]) ).
fof(f19476,plain,
! [X0,X1] :
( ( k4_xboole_0(k1_tarski(X0),X1) = k1_tarski(X0)
| r2_hidden(X0,X1) )
& ( ~ r2_hidden(X0,X1)
| k1_tarski(X0) != k4_xboole_0(k1_tarski(X0),X1) ) ),
inference(nnf_transformation,[],[f392]) ).
fof(f19477,plain,
! [X0,X1] :
( ( k4_xboole_0(X0,k1_tarski(X1)) = X0
| r2_hidden(X1,X0) )
& ( ~ r2_hidden(X1,X0)
| k4_xboole_0(X0,k1_tarski(X1)) != X0 ) ),
inference(nnf_transformation,[],[f390]) ).
fof(f19482,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f19483,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X3] :
( ( r2_hidden(X3,X2)
| ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(X3,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(flattening,[],[f19482]) ).
fof(f19484,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ? [X3] :
( ( ~ r2_hidden(X3,X0)
| r2_hidden(X3,X1)
| ~ r2_hidden(X3,X2) )
& ( ( r2_hidden(X3,X0)
& ~ r2_hidden(X3,X1) )
| r2_hidden(X3,X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(rectify,[],[f19483]) ).
fof(f19485,plain,
! [X0,X1,X2] :
( ( X2 = k4_xboole_0(X0,X1)
| ( ( ~ r2_hidden(sK54(X0,X1,X2),X0)
| r2_hidden(sK54(X0,X1,X2),X1)
| ~ r2_hidden(sK54(X0,X1,X2),X2) )
& ( ( r2_hidden(sK54(X0,X1,X2),X0)
& ~ r2_hidden(sK54(X0,X1,X2),X1) )
| r2_hidden(sK54(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( r2_hidden(X4,X2)
| ~ r2_hidden(X4,X0)
| r2_hidden(X4,X1) )
& ( ( r2_hidden(X4,X0)
& ~ r2_hidden(X4,X1) )
| ~ r2_hidden(X4,X2) ) )
| k4_xboole_0(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X3,sK54(X0,X1,X2))],[f19484]) ).
fof(f19504,plain,
! [X0,X1] :
( r2_hidden(sK0(X0,X1),X1)
| ~ r2_hidden(X0,k3_pua2mss1(X1)) ),
inference(cnf_transformation,[],[f19394]) ).
fof(f19505,plain,
! [X0,X1] :
( k1_tarski(sK0(X0,X1)) = X0
| ~ r2_hidden(X0,k3_pua2mss1(X1)) ),
inference(cnf_transformation,[],[f19394]) ).
fof(f19506,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k3_pua2mss1(X1))
| k1_tarski(X2) != X0
| ~ r2_hidden(X2,X1) ),
inference(cnf_transformation,[],[f19394]) ).
fof(f19511,plain,
k3_pua2mss1(k4_xboole_0(sK1,sK2)) != k4_xboole_0(k3_pua2mss1(sK1),k3_pua2mss1(sK2)),
inference(cnf_transformation,[],[f19396]) ).
fof(f19539,plain,
! [X0,X1] :
( k1_tarski(X0) = k3_xboole_0(X1,k1_tarski(X0))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f19126]) ).
fof(f19540,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| k1_tarski(X1) != k3_xboole_0(X0,k1_tarski(X1)) ),
inference(cnf_transformation,[],[f19127]) ).
fof(f19766,plain,
! [X3,X0,X1] :
( r2_hidden(X3,X1)
| X0 != X3
| k1_tarski(X0) != X1 ),
inference(cnf_transformation,[],[f19447]) ).
fof(f19790,plain,
! [X0] : k3_pua2mss1(X0) = k8_eqrel_1(X0,k6_partfun1(X0)),
inference(cnf_transformation,[],[f14080]) ).
fof(f19868,plain,
! [X0] : k2_xboole_0(X0,k1_xboole_0) = X0,
inference(cnf_transformation,[],[f62]) ).
fof(f19908,plain,
! [X0,X1] :
( k4_xboole_0(k2_xboole_0(X1,k1_tarski(X0)),k1_tarski(X0)) = X1
| r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f19376]) ).
fof(f19916,plain,
! [X0,X1] :
( k1_xboole_0 = k4_xboole_0(k1_tarski(X0),X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f19475]) ).
fof(f19918,plain,
! [X0,X1] :
( k1_tarski(X0) = k4_xboole_0(k1_tarski(X0),X1)
| r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f19476]) ).
fof(f19920,plain,
! [X0,X1] :
( ~ r2_hidden(X1,X0)
| k4_xboole_0(X0,k1_tarski(X1)) != X0 ),
inference(cnf_transformation,[],[f19477]) ).
fof(f19929,plain,
! [X2,X0,X1] : k4_xboole_0(k3_xboole_0(X0,X1),k3_xboole_0(X2,X1)) = k3_xboole_0(k4_xboole_0(X0,X2),X1),
inference(cnf_transformation,[],[f180]) ).
fof(f19932,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k3_xboole_0(X1,X2)) = k2_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2)),
inference(cnf_transformation,[],[f123]) ).
fof(f19933,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k2_xboole_0(X1,X2)) = k3_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2)),
inference(cnf_transformation,[],[f122]) ).
fof(f19938,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k4_xboole_0(X0,k4_xboole_0(X0,X1)),
inference(cnf_transformation,[],[f117]) ).
fof(f19945,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X0,X1),X2) = k4_xboole_0(X0,k2_xboole_0(X1,X2)),
inference(cnf_transformation,[],[f110]) ).
fof(f19946,plain,
! [X0,X1] : k4_xboole_0(X0,X1) = k4_xboole_0(k2_xboole_0(X0,X1),X1),
inference(cnf_transformation,[],[f109]) ).
fof(f19958,plain,
! [X2,X0,X1,X4] :
( ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,X2)
| k4_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f19485]) ).
fof(f19959,plain,
! [X2,X0,X1,X4] :
( r2_hidden(X4,X0)
| ~ r2_hidden(X4,X2)
| k4_xboole_0(X0,X1) != X2 ),
inference(cnf_transformation,[],[f19485]) ).
fof(f19961,plain,
! [X2,X0,X1] :
( k4_xboole_0(X0,X1) = X2
| ~ r2_hidden(sK54(X0,X1,X2),X1)
| r2_hidden(sK54(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f19485]) ).
fof(f19962,plain,
! [X2,X0,X1] :
( k4_xboole_0(X0,X1) = X2
| r2_hidden(sK54(X0,X1,X2),X0)
| r2_hidden(sK54(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f19485]) ).
fof(f19963,plain,
! [X2,X0,X1] :
( k4_xboole_0(X0,X1) = X2
| ~ r2_hidden(sK54(X0,X1,X2),X0)
| r2_hidden(sK54(X0,X1,X2),X1)
| ~ r2_hidden(sK54(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f19485]) ).
fof(f19965,plain,
! [X2,X0,X1] :
( r2_hidden(X0,k8_eqrel_1(X1,k6_partfun1(X1)))
| k1_tarski(X2) != X0
| ~ r2_hidden(X2,X1) ),
inference(definition_unfolding,[],[f19506,f19790]) ).
fof(f19966,plain,
! [X0,X1] :
( k1_tarski(sK0(X0,X1)) = X0
| ~ r2_hidden(X0,k8_eqrel_1(X1,k6_partfun1(X1))) ),
inference(definition_unfolding,[],[f19505,f19790]) ).
fof(f19967,plain,
! [X0,X1] :
( r2_hidden(sK0(X0,X1),X1)
| ~ r2_hidden(X0,k8_eqrel_1(X1,k6_partfun1(X1))) ),
inference(definition_unfolding,[],[f19504,f19790]) ).
fof(f19972,plain,
k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) != k4_xboole_0(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2))),
inference(definition_unfolding,[],[f19511,f19790,f19790,f19790]) ).
fof(f19996,plain,
! [X0,X1] :
( k1_tarski(X0) = k4_xboole_0(X1,k4_xboole_0(X1,k1_tarski(X0)))
| ~ r2_hidden(X0,X1) ),
inference(definition_unfolding,[],[f19539,f19938]) ).
fof(f19997,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| k1_tarski(X1) != k4_xboole_0(X0,k4_xboole_0(X0,k1_tarski(X1))) ),
inference(definition_unfolding,[],[f19540,f19938]) ).
fof(f20034,plain,
! [X2,X0,X1] : k4_xboole_0(k4_xboole_0(X0,k4_xboole_0(X0,X1)),k4_xboole_0(X2,k4_xboole_0(X2,X1))) = k4_xboole_0(k4_xboole_0(X0,X2),k4_xboole_0(k4_xboole_0(X0,X2),X1)),
inference(definition_unfolding,[],[f19929,f19938,f19938,f19938]) ).
fof(f20036,plain,
! [X2,X0,X1] : k2_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2)) = k4_xboole_0(X0,k4_xboole_0(X1,k4_xboole_0(X1,X2))),
inference(definition_unfolding,[],[f19932,f19938]) ).
fof(f20037,plain,
! [X2,X0,X1] : k4_xboole_0(X0,k2_xboole_0(X1,X2)) = k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(k4_xboole_0(X0,X1),k4_xboole_0(X0,X2))),
inference(definition_unfolding,[],[f19933,f19938]) ).
fof(f20043,plain,
! [X2,X1] :
( r2_hidden(k1_tarski(X2),k8_eqrel_1(X1,k6_partfun1(X1)))
| ~ r2_hidden(X2,X1) ),
inference(equality_resolution,[],[f19965]) ).
fof(f20066,plain,
! [X3,X1] :
( r2_hidden(X3,X1)
| k1_tarski(X3) != X1 ),
inference(equality_resolution,[],[f19766]) ).
fof(f20067,plain,
! [X3] : r2_hidden(X3,k1_tarski(X3)),
inference(equality_resolution,[],[f20066]) ).
fof(f20081,plain,
! [X0,X1,X4] :
( r2_hidden(X4,X0)
| ~ r2_hidden(X4,k4_xboole_0(X0,X1)) ),
inference(equality_resolution,[],[f19959]) ).
fof(f20082,plain,
! [X0,X1,X4] :
( ~ r2_hidden(X4,X1)
| ~ r2_hidden(X4,k4_xboole_0(X0,X1)) ),
inference(equality_resolution,[],[f19958]) ).
fof(f20184,definition,
( spl96_1
<=> k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) = k4_xboole_0(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl96_1])],[avatar_definition]) ).
fof(f20186,plain,
( k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) != k4_xboole_0(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| spl96_1 ),
inference(avatar_component_clause,[],[f20184]) ).
fof(f20187,plain,
~ spl96_1,
inference(avatar_split_clause,[],[f19972,f20184]) ).
fof(f20190,plain,
( ! [X0] :
( k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) != X0
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),X0) )
| spl96_1 ),
inference(superposition,[],[f20186,f19963]) ).
fof(f20193,definition,
( spl96_2
<=> ! [X0] :
( k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) != X0
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl96_2])],[avatar_definition]) ).
fof(f20194,plain,
( ! [X0] :
( k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) != X0
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),X0),X0) )
| ~ spl96_2 ),
inference(avatar_component_clause,[],[f20193]) ).
fof(f20195,plain,
( spl96_2
| spl96_1 ),
inference(avatar_split_clause,[],[f20190,f20184,f20193]) ).
fof(f20200,plain,
( ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))
| ~ spl96_2 ),
inference(equality_resolution,[],[f20194]) ).
fof(f20203,definition,
( spl96_3
<=> r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) ),
introduced(definition,[new_symbols(definition,[spl96_3])],[avatar_definition]) ).
fof(f20204,plain,
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))
| ~ spl96_3 ),
inference(avatar_component_clause,[],[f20203]) ).
fof(f20205,plain,
( ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))
| spl96_3 ),
inference(avatar_component_clause,[],[f20203]) ).
fof(f20207,definition,
( spl96_4
<=> r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK2,k6_partfun1(sK2))) ),
introduced(definition,[new_symbols(definition,[spl96_4])],[avatar_definition]) ).
fof(f20208,plain,
( ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| spl96_4 ),
inference(avatar_component_clause,[],[f20207]) ).
fof(f20209,plain,
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| ~ spl96_4 ),
inference(avatar_component_clause,[],[f20207]) ).
fof(f20211,definition,
( spl96_5
<=> r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK1,k6_partfun1(sK1))) ),
introduced(definition,[new_symbols(definition,[spl96_5])],[avatar_definition]) ).
fof(f20212,plain,
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| ~ spl96_5 ),
inference(avatar_component_clause,[],[f20211]) ).
fof(f20213,plain,
( ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| spl96_5 ),
inference(avatar_component_clause,[],[f20211]) ).
fof(f20214,plain,
( ~ spl96_3
| spl96_4
| ~ spl96_5
| ~ spl96_2 ),
inference(avatar_split_clause,[],[f20200,f20193,f20211,f20207,f20203]) ).
fof(f20215,plain,
( k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) = k4_xboole_0(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| spl96_3 ),
inference(resolution,[],[f20205,f19961]) ).
fof(f20216,plain,
( k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))) = k4_xboole_0(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| spl96_3 ),
inference(resolution,[],[f20205,f19962]) ).
fof(f20279,plain,
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| spl96_1
| spl96_3 ),
inference(forward_subsumption_resolution,[],[f20216,f20186]) ).
fof(f20280,plain,
( ~ r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK2,k6_partfun1(sK2)))
| spl96_1
| spl96_3 ),
inference(forward_subsumption_resolution,[],[f20215,f20186]) ).
fof(f20281,plain,
( spl96_5
| spl96_1
| spl96_3 ),
inference(avatar_split_clause,[],[f20279,f20203,f20184,f20211]) ).
fof(f20283,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK1)
| ~ spl96_5 ),
inference(resolution,[],[f20212,f19967]) ).
fof(f20284,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1))
| ~ spl96_5 ),
inference(resolution,[],[f20212,f19966]) ).
fof(f20351,definition,
( spl96_6
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK1) ),
introduced(definition,[new_symbols(definition,[spl96_6])],[avatar_definition]) ).
fof(f20353,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK1)
| ~ spl96_6 ),
inference(avatar_component_clause,[],[f20351]) ).
fof(f20354,plain,
( spl96_6
| ~ spl96_5 ),
inference(avatar_split_clause,[],[f20283,f20211,f20351]) ).
fof(f20431,plain,
( ~ spl96_4
| spl96_1
| spl96_3 ),
inference(avatar_split_clause,[],[f20280,f20203,f20184,f20207]) ).
fof(f20496,definition,
( spl96_7
<=> sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)) ),
introduced(definition,[new_symbols(definition,[spl96_7])],[avatar_definition]) ).
fof(f20498,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1))
| ~ spl96_7 ),
inference(avatar_component_clause,[],[f20496]) ).
fof(f20499,plain,
( spl96_7
| ~ spl96_5 ),
inference(avatar_split_clause,[],[f20284,f20211,f20496]) ).
fof(f20564,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),k4_xboole_0(sK1,sK2))
| ~ spl96_3 ),
inference(resolution,[],[f20204,f19967]) ).
fof(f20633,definition,
( spl96_8
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),k4_xboole_0(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl96_8])],[avatar_definition]) ).
fof(f20635,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),k4_xboole_0(sK1,sK2))
| ~ spl96_8 ),
inference(avatar_component_clause,[],[f20633]) ).
fof(f20636,plain,
( spl96_8
| ~ spl96_3 ),
inference(avatar_split_clause,[],[f20564,f20203,f20633]) ).
fof(f20877,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))
| ~ spl96_7 ),
inference(superposition,[],[f20067,f20498]) ).
fof(f21047,plain,
( ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),sK2)
| ~ spl96_8 ),
inference(resolution,[],[f20635,f20082]) ).
fof(f21048,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),sK1)
| ~ spl96_8 ),
inference(resolution,[],[f20635,f20081]) ).
fof(f21298,plain,
( k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)) = k4_xboole_0(sK1,k4_xboole_0(sK1,k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1))))
| ~ spl96_6 ),
inference(resolution,[],[f20353,f19996]) ).
fof(f21336,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k4_xboole_0(sK1,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))
| ~ spl96_6
| ~ spl96_7 ),
inference(forward_demodulation,[],[f21298,f20498]) ).
fof(f21419,definition,
( spl96_11
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),sK1) ),
introduced(definition,[new_symbols(definition,[spl96_11])],[avatar_definition]) ).
fof(f21421,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),sK1)
| ~ spl96_11 ),
inference(avatar_component_clause,[],[f21419]) ).
fof(f21422,plain,
( spl96_11
| ~ spl96_8 ),
inference(avatar_split_clause,[],[f21048,f20633,f21419]) ).
fof(f21547,definition,
( spl96_13
<=> sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k4_xboole_0(sK1,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))) ),
introduced(definition,[new_symbols(definition,[spl96_13])],[avatar_definition]) ).
fof(f21549,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k4_xboole_0(sK1,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))
| ~ spl96_13 ),
inference(avatar_component_clause,[],[f21547]) ).
fof(f21550,plain,
( spl96_13
| ~ spl96_6
| ~ spl96_7 ),
inference(avatar_split_clause,[],[f21336,f20496,f20351,f21547]) ).
fof(f21615,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)))
| ~ spl96_3 ),
inference(resolution,[],[f20204,f19966]) ).
fof(f21875,definition,
( spl96_14
<=> sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2))) ),
introduced(definition,[new_symbols(definition,[spl96_14])],[avatar_definition]) ).
fof(f21877,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)))
| ~ spl96_14 ),
inference(avatar_component_clause,[],[f21875]) ).
fof(f21878,plain,
( spl96_14
| ~ spl96_3 ),
inference(avatar_split_clause,[],[f21615,f20203,f21875]) ).
fof(f22046,plain,
( r2_hidden(k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2))),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| ~ spl96_11 ),
inference(resolution,[],[f21421,f20043]) ).
fof(f22082,plain,
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(sK1,k6_partfun1(sK1)))
| ~ spl96_11
| ~ spl96_14 ),
inference(forward_demodulation,[],[f22046,f21877]) ).
fof(f22093,plain,
( $false
| spl96_5
| ~ spl96_11
| ~ spl96_14 ),
inference(forward_subsumption_resolution,[],[f22082,f20213]) ).
fof(f22094,plain,
( spl96_5
| ~ spl96_11
| ~ spl96_14 ),
inference(avatar_contradiction_clause,[],[f22093]) ).
fof(f22100,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK2),sK2)
| ~ spl96_4 ),
inference(resolution,[],[f20209,f19967]) ).
fof(f22101,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK2))
| ~ spl96_4 ),
inference(resolution,[],[f20209,f19966]) ).
fof(f22234,definition,
( spl96_15
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl96_15])],[avatar_definition]) ).
fof(f22236,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK2),sK2)
| ~ spl96_15 ),
inference(avatar_component_clause,[],[f22234]) ).
fof(f22237,plain,
( spl96_15
| ~ spl96_4 ),
inference(avatar_split_clause,[],[f22100,f20207,f22234]) ).
fof(f22259,plain,
( sK2 != k4_xboole_0(sK2,k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK2)))
| ~ spl96_15 ),
inference(resolution,[],[f22236,f19920]) ).
fof(f22300,plain,
( sK2 != k4_xboole_0(sK2,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))
| ~ spl96_4
| ~ spl96_15 ),
inference(forward_demodulation,[],[f22259,f22101]) ).
fof(f22419,plain,
( ! [X0] :
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(X0,k6_partfun1(X0)))
| ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),X0) )
| ~ spl96_7 ),
inference(superposition,[],[f20043,f20498]) ).
fof(f22908,definition,
( spl96_19
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))) ),
introduced(definition,[new_symbols(definition,[spl96_19])],[avatar_definition]) ).
fof(f22910,plain,
( r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))
| ~ spl96_19 ),
inference(avatar_component_clause,[],[f22908]) ).
fof(f22911,plain,
( spl96_19
| ~ spl96_7 ),
inference(avatar_split_clause,[],[f20877,f20496,f22908]) ).
fof(f22931,plain,
( k1_xboole_0 = k4_xboole_0(k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))
| ~ spl96_19 ),
inference(resolution,[],[f22910,f19916]) ).
fof(f22976,plain,
( k1_xboole_0 = k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))
| ~ spl96_7
| ~ spl96_19 ),
inference(forward_demodulation,[],[f22931,f20498]) ).
fof(f23282,definition,
( spl96_27
<=> k1_xboole_0 = k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))) ),
introduced(definition,[new_symbols(definition,[spl96_27])],[avatar_definition]) ).
fof(f23284,plain,
( k1_xboole_0 = k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))
| ~ spl96_27 ),
inference(avatar_component_clause,[],[f23282]) ).
fof(f23285,plain,
( spl96_27
| ~ spl96_7
| ~ spl96_19 ),
inference(avatar_split_clause,[],[f22976,f22908,f20496,f23282]) ).
fof(f23367,plain,
( ! [X0] : k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(X0,k4_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))) = k2_xboole_0(k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),X0),k1_xboole_0)
| ~ spl96_27 ),
inference(superposition,[],[f20036,f23284]) ).
fof(f23457,plain,
( ! [X0] : k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),X0) = k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(X0,k4_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))))
| ~ spl96_27 ),
inference(forward_demodulation,[],[f23367,f19868]) ).
fof(f23570,definition,
( spl96_28
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),sK2) ),
introduced(definition,[new_symbols(definition,[spl96_28])],[avatar_definition]) ).
fof(f23572,plain,
( ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)),sK2)
| spl96_28 ),
inference(avatar_component_clause,[],[f23570]) ).
fof(f23573,plain,
( ~ spl96_28
| ~ spl96_8 ),
inference(avatar_split_clause,[],[f21047,f20633,f23570]) ).
fof(f23579,plain,
( sK2 = k4_xboole_0(k2_xboole_0(sK2,k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2)))),k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2))))
| spl96_28 ),
inference(resolution,[],[f23572,f19908]) ).
fof(f23637,plain,
( sK2 = k4_xboole_0(sK2,k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(sK1,sK2))))
| spl96_28 ),
inference(forward_demodulation,[],[f23579,f19946]) ).
fof(f23650,plain,
( sK2 = k4_xboole_0(sK2,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))
| ~ spl96_14
| spl96_28 ),
inference(forward_demodulation,[],[f23637,f21877]) ).
fof(f23655,plain,
( $false
| ~ spl96_4
| ~ spl96_14
| ~ spl96_15
| spl96_28 ),
inference(forward_subsumption_resolution,[],[f23650,f22300]) ).
fof(f23656,plain,
( ~ spl96_4
| ~ spl96_14
| ~ spl96_15
| spl96_28 ),
inference(avatar_contradiction_clause,[],[f23655]) ).
fof(f24482,plain,
( ! [X0] : k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(X0,k4_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))) = k4_xboole_0(k4_xboole_0(sK1,X0),k4_xboole_0(k4_xboole_0(sK1,X0),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))
| ~ spl96_13 ),
inference(superposition,[],[f20034,f21549]) ).
fof(f24568,plain,
( ! [X0] : k4_xboole_0(k4_xboole_0(sK1,X0),k4_xboole_0(k4_xboole_0(sK1,X0),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))) = k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))))
| ~ spl96_13 ),
inference(superposition,[],[f20037,f21549]) ).
fof(f24622,plain,
( ! [X0] : k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))) = k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(k4_xboole_0(sK1,X0),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))))
| ~ spl96_13 ),
inference(forward_demodulation,[],[f24568,f19945]) ).
fof(f24651,plain,
( ! [X0] : k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(X0,k4_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))) = k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(k4_xboole_0(sK1,X0),sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))))
| ~ spl96_13 ),
inference(forward_demodulation,[],[f24482,f19945]) ).
fof(f24682,plain,
( ! [X0] : k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))) = k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(sK1,k2_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))))
| ~ spl96_13 ),
inference(forward_demodulation,[],[f24622,f19945]) ).
fof(f24693,plain,
( ! [X0] : k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(X0,k4_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))) = k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(sK1,k2_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))))
| ~ spl96_13 ),
inference(forward_demodulation,[],[f24651,f19945]) ).
fof(f24703,plain,
( ! [X0] : k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k4_xboole_0(X0,k4_xboole_0(X0,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))) = k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))))
| ~ spl96_13 ),
inference(forward_demodulation,[],[f24693,f24682]) ).
fof(f24710,plain,
( ! [X0] : k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),X0) = k4_xboole_0(sK1,k2_xboole_0(X0,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))))
| ~ spl96_13
| ~ spl96_27 ),
inference(forward_demodulation,[],[f24703,f23457]) ).
fof(f29728,definition,
( spl96_76
<=> ! [X0] :
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(X0,k6_partfun1(X0)))
| ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),X0) ) ),
introduced(definition,[new_symbols(definition,[spl96_76])],[avatar_definition]) ).
fof(f29729,plain,
( ! [X0] :
( r2_hidden(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),k8_eqrel_1(X0,k6_partfun1(X0)))
| ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),X0) )
| ~ spl96_76 ),
inference(avatar_component_clause,[],[f29728]) ).
fof(f29730,plain,
( spl96_76
| ~ spl96_7 ),
inference(avatar_split_clause,[],[f22419,f20496,f29728]) ).
fof(f29731,plain,
( ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),k4_xboole_0(sK1,sK2))
| spl96_3
| ~ spl96_76 ),
inference(resolution,[],[f29729,f20205]) ).
fof(f29732,plain,
( ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK2)
| spl96_4
| ~ spl96_76 ),
inference(resolution,[],[f29729,f20208]) ).
fof(f29806,definition,
( spl96_77
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK2) ),
introduced(definition,[new_symbols(definition,[spl96_77])],[avatar_definition]) ).
fof(f29808,plain,
( ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),sK2)
| spl96_77 ),
inference(avatar_component_clause,[],[f29806]) ).
fof(f29809,plain,
( ~ spl96_77
| spl96_4
| ~ spl96_76 ),
inference(avatar_split_clause,[],[f29732,f29728,f20207,f29806]) ).
fof(f29817,plain,
( k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)) = k4_xboole_0(k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)),sK2)
| spl96_77 ),
inference(resolution,[],[f29808,f19918]) ).
fof(f29873,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) = k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK2)
| ~ spl96_7
| spl96_77 ),
inference(forward_demodulation,[],[f29817,f20498]) ).
fof(f29883,definition,
( spl96_78
<=> r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),k4_xboole_0(sK1,sK2)) ),
introduced(definition,[new_symbols(definition,[spl96_78])],[avatar_definition]) ).
fof(f29885,plain,
( ~ r2_hidden(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1),k4_xboole_0(sK1,sK2))
| spl96_78 ),
inference(avatar_component_clause,[],[f29883]) ).
fof(f29886,plain,
( ~ spl96_78
| spl96_3
| ~ spl96_76 ),
inference(avatar_split_clause,[],[f29731,f29728,f20203,f29883]) ).
fof(f29923,plain,
( k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)) != k4_xboole_0(k4_xboole_0(sK1,sK2),k4_xboole_0(k4_xboole_0(sK1,sK2),k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1))))
| spl96_78 ),
inference(resolution,[],[f29885,f19997]) ).
fof(f29974,plain,
( k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)) != k4_xboole_0(sK1,k2_xboole_0(sK2,k4_xboole_0(k4_xboole_0(sK1,sK2),k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)))))
| spl96_78 ),
inference(forward_demodulation,[],[f29923,f19945]) ).
fof(f30010,plain,
( k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1)) != k4_xboole_0(sK1,k2_xboole_0(sK2,k4_xboole_0(sK1,k2_xboole_0(sK2,k1_tarski(sK0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK1))))))
| spl96_78 ),
inference(forward_demodulation,[],[f29974,f19945]) ).
fof(f30034,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) != k4_xboole_0(sK1,k2_xboole_0(sK2,k4_xboole_0(sK1,k2_xboole_0(sK2,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2))))))))
| ~ spl96_7
| spl96_78 ),
inference(forward_demodulation,[],[f30010,f20498]) ).
fof(f30068,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) != k4_xboole_0(sK1,k2_xboole_0(sK2,k4_xboole_0(sK1,sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))))))
| ~ spl96_7
| ~ spl96_13
| spl96_78 ),
inference(forward_demodulation,[],[f30034,f24682]) ).
fof(f30069,plain,
( sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))) != k4_xboole_0(sK54(k8_eqrel_1(sK1,k6_partfun1(sK1)),k8_eqrel_1(sK2,k6_partfun1(sK2)),k8_eqrel_1(k4_xboole_0(sK1,sK2),k6_partfun1(k4_xboole_0(sK1,sK2)))),sK2)
| ~ spl96_7
| ~ spl96_13
| ~ spl96_27
| spl96_78 ),
inference(forward_demodulation,[],[f30068,f24710]) ).
fof(f30070,plain,
( $false
| ~ spl96_7
| ~ spl96_13
| ~ spl96_27
| spl96_77
| spl96_78 ),
inference(forward_subsumption_resolution,[],[f30069,f29873]) ).
fof(f30071,plain,
( ~ spl96_7
| ~ spl96_13
| ~ spl96_27
| spl96_77
| spl96_78 ),
inference(avatar_contradiction_clause,[],[f30070]) ).
cnf(s1,plain,
~ spl96_1,
inference(sat_conversion,[],[f20187]) ).
cnf(s2,plain,
( spl96_1
| spl96_2 ),
inference(sat_conversion,[],[f20195]) ).
cnf(s3,plain,
( ~ spl96_2
| ~ spl96_3
| spl96_4
| ~ spl96_5 ),
inference(sat_conversion,[],[f20214]) ).
cnf(s4,plain,
( spl96_1
| spl96_3
| spl96_5 ),
inference(sat_conversion,[],[f20281]) ).
cnf(s5,plain,
( ~ spl96_5
| spl96_6 ),
inference(sat_conversion,[],[f20354]) ).
cnf(s6,plain,
( spl96_1
| spl96_3
| ~ spl96_4 ),
inference(sat_conversion,[],[f20431]) ).
cnf(s7,plain,
( ~ spl96_5
| spl96_7 ),
inference(sat_conversion,[],[f20499]) ).
cnf(s8,plain,
( ~ spl96_3
| spl96_8 ),
inference(sat_conversion,[],[f20636]) ).
cnf(s15,plain,
( ~ spl96_8
| spl96_11 ),
inference(sat_conversion,[],[f21422]) ).
cnf(s17,plain,
( ~ spl96_6
| ~ spl96_7
| spl96_13 ),
inference(sat_conversion,[],[f21550]) ).
cnf(s19,plain,
( ~ spl96_3
| spl96_14 ),
inference(sat_conversion,[],[f21878]) ).
cnf(s21,plain,
( spl96_5
| ~ spl96_11
| ~ spl96_14 ),
inference(sat_conversion,[],[f22094]) ).
cnf(s22,plain,
( ~ spl96_4
| spl96_15 ),
inference(sat_conversion,[],[f22237]) ).
cnf(s26,plain,
( ~ spl96_7
| spl96_19 ),
inference(sat_conversion,[],[f22911]) ).
cnf(s34,plain,
( ~ spl96_7
| ~ spl96_19
| spl96_27 ),
inference(sat_conversion,[],[f23285]) ).
cnf(s35,plain,
( ~ spl96_8
| ~ spl96_28 ),
inference(sat_conversion,[],[f23573]) ).
cnf(s41,plain,
( ~ spl96_4
| ~ spl96_14
| ~ spl96_15
| spl96_28 ),
inference(sat_conversion,[],[f23656]) ).
cnf(s201,plain,
( ~ spl96_7
| spl96_76 ),
inference(sat_conversion,[],[f29730]) ).
cnf(s202,plain,
( spl96_4
| ~ spl96_76
| ~ spl96_77 ),
inference(sat_conversion,[],[f29809]) ).
cnf(s203,plain,
( spl96_3
| ~ spl96_76
| ~ spl96_78 ),
inference(sat_conversion,[],[f29886]) ).
cnf(s221,plain,
( ~ spl96_7
| ~ spl96_13
| ~ spl96_27
| spl96_77
| spl96_78 ),
inference(sat_conversion,[],[f30071]) ).
cnf(s224,plain,
spl96_2,
inference(rat,[],[s2,s1]) ).
cnf(s225,plain,
spl96_3,
inference(rat,[],[s221,s34,s202,s203,s17,s26,s201,s5,s7,s4,s6,s1]) ).
cnf(s227,plain,
spl96_14,
inference(rat,[],[s19,s225]) ).
cnf(s228,plain,
spl96_8,
inference(rat,[],[s8,s225]) ).
cnf(s231,plain,
~ spl96_28,
inference(rat,[],[s35,s228]) ).
cnf(s234,plain,
spl96_11,
inference(rat,[],[s15,s228]) ).
cnf(s237,plain,
spl96_5,
inference(rat,[],[s21,s227,s234]) ).
cnf(s242,plain,
spl96_4,
inference(rat,[],[s3,s225,s224,s237]) ).
cnf(s264,plain,
spl96_15,
inference(rat,[],[s22,s242]) ).
cnf(s265,plain,
$false,
inference(rat,[],[s41,s231,s227,s242,s264]) ).
fof(f30072,plain,
$false,
inference(avatar_sat_refutation,[],[s265]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU416+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n015.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 05:19:21 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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
% 16.07/4.13 % (2275837)Detected formulas, will run a generic FOF schedule.
% 16.07/4.13 % (2275842)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=1350346111:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 16.07/4.13 % (2275846)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1787497054:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 16.07/4.13 % (2275847)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2290508038:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 16.07/4.13 % (2275845)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=122256742:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 16.07/4.13 % (2275848)dis-21_1_sil=8000:lcm=predicate:random_seed=128902287:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 16.07/4.13 % (2275844)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=3295497619:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 16.07/4.13 % (2275843)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=415829067:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 16.07/4.13 % (2275847)Instruction limit reached!
% 16.07/4.13 % (2275847)------------------------------
% 16.07/4.13 % (2275847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.07/4.13 % (2275847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/4.13 % (2275847)CaDiCaL version: 2.1.3
% 16.07/4.13 % (2275847)Termination reason: Instruction limit
% 16.07/4.13 % (2275847)Termination phase: Property scanning
% 16.07/4.13 % (2275847)Time elapsed: 0.059 s
% 16.07/4.13 % (2275847)Peak memory usage: 112 MB
% 16.07/4.13 % (2275847)Instructions burned: 140 (million)
% 16.07/4.13 % (2275845)Instruction limit reached!
% 16.07/4.13 % (2275845)------------------------------
% 16.07/4.13 % (2275845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.07/4.13 % (2275845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/4.13 % (2275845)CaDiCaL version: 2.1.3
% 16.07/4.13 % (2275845)Termination reason: Instruction limit
% 16.07/4.13 % (2275845)Termination phase: SInE selection
% 16.07/4.13 % (2275845)Time elapsed: 0.084 s
% 16.07/4.13 % (2275845)Peak memory usage: 112 MB
% 16.07/4.13 % (2275845)Instructions burned: 109 (million)
% 16.07/4.13 % (2275848)Instruction limit reached!
% 16.07/4.13 % (2275848)------------------------------
% 16.07/4.13 % (2275848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.07/4.13 % (2275848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/4.13 % (2275848)CaDiCaL version: 2.1.3
% 16.07/4.13 % (2275848)Termination reason: Instruction limit
% 16.07/4.13 % (2275848)Termination phase: SInE selection
% 16.07/4.13 % (2275848)Time elapsed: 0.086 s
% 16.07/4.13 % (2275848)Peak memory usage: 112 MB
% 16.07/4.13 % (2275848)Instructions burned: 130 (million)
% 16.07/4.13 % (2275846)Instruction limit reached!
% 16.07/4.13 % (2275846)------------------------------
% 16.07/4.13 % (2275846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.07/4.13 % (2275846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/4.13 % (2275846)CaDiCaL version: 2.1.3
% 16.07/4.13 % (2275846)Termination reason: Instruction limit
% 16.07/4.13 % (2275846)Termination phase: Preprocessing 1
% 16.07/4.13 % (2275846)Time elapsed: 0.102 s
% 16.07/4.13 % (2275846)Peak memory usage: 113 MB
% 16.07/4.13 % (2275846)Instructions burned: 119 (million)
% 16.07/4.13 % (2275856)lrs+10_1_sil=8000:sp=occurrence:random_seed=3819225396:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 16.07/4.13 % (2275857)lrs+10_1_sil=32000:urr=on:br=off:random_seed=657700276:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 16.07/4.13 % (2275858)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4007664257:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 16.07/4.13 % (2275859)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=4167663588:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 16.07/4.13 % (2275857)Instruction limit reached!
% 11.46/4.43 % (2275857)------------------------------
% 11.46/4.43 % (2275857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275857)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275857)Termination reason: Instruction limit
% 11.46/4.43 % (2275857)Termination phase: Property scanning
% 11.46/4.43 % (2275857)Time elapsed: 0.068 s
% 11.46/4.43 % (2275857)Peak memory usage: 112 MB
% 11.46/4.43 % (2275857)Instructions burned: 159 (million)
% 11.46/4.43 % (2275859)Instruction limit reached!
% 11.46/4.43 % (2275859)------------------------------
% 11.46/4.43 % (2275859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275859)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275859)Termination reason: Instruction limit
% 11.46/4.43 % (2275859)Termination phase: Property scanning
% 11.46/4.43 % (2275859)Time elapsed: 0.108 s
% 11.46/4.43 % (2275859)Peak memory usage: 112 MB
% 11.46/4.43 % (2275859)Instructions burned: 249 (million)
% 11.46/4.43 % (2275856)Instruction limit reached!
% 11.46/4.43 % (2275856)------------------------------
% 11.46/4.43 % (2275856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275856)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275856)Termination reason: Instruction limit
% 11.46/4.43 % (2275856)Termination phase: Saturation
% 11.46/4.43 % (2275856)Time elapsed: 0.214 s
% 11.46/4.43 % (2275856)Peak memory usage: 119 MB
% 11.46/4.43 % (2275856)Instructions burned: 285 (million)
% 11.46/4.43 % (2275864)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1089618707:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 11.46/4.43 % (2275858)Instruction limit reached!
% 11.46/4.43 % (2275858)------------------------------
% 11.46/4.43 % (2275858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275858)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275858)Termination reason: Instruction limit
% 11.46/4.43 % (2275858)Termination phase: Saturation
% 11.46/4.43 % (2275858)Time elapsed: 0.245 s
% 11.46/4.43 % (2275858)Peak memory usage: 119 MB
% 11.46/4.43 % (2275858)Instructions burned: 326 (million)
% 11.46/4.43 % (2275865)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3401034800:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 11.46/4.43 % (2275866)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3594764252:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 11.46/4.43 % (2275866)Instruction limit reached!
% 11.46/4.43 % (2275866)------------------------------
% 11.46/4.43 % (2275866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275866)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275866)Termination reason: Instruction limit
% 11.46/4.43 % (2275866)Termination phase: SInE selection
% 11.46/4.43 % (2275866)Time elapsed: 0.088 s
% 11.46/4.43 % (2275866)Peak memory usage: 112 MB
% 11.46/4.43 % (2275866)Instructions burned: 113 (million)
% 11.46/4.43 % (2275868)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3338080276:i=127:av=off:fsr=off:sup=off_2982 on theBenchmark for (2982ds/127Mi)
% 11.46/4.43 % (2275864)Instruction limit reached!
% 11.46/4.43 % (2275864)------------------------------
% 11.46/4.43 % (2275864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275864)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275864)Termination reason: Instruction limit
% 11.46/4.43 % (2275864)Termination phase: Property scanning
% 11.46/4.43 % (2275864)Time elapsed: 0.209 s
% 11.46/4.43 % (2275864)Peak memory usage: 118 MB
% 11.46/4.43 % (2275864)Instructions burned: 294 (million)
% 11.46/4.43 % (2275868)Instruction limit reached!
% 11.46/4.43 % (2275868)------------------------------
% 11.46/4.43 % (2275868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275868)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275868)Termination reason: Instruction limit
% 11.46/4.43 % (2275868)Termination phase: Preprocessing 1
% 11.46/4.43 % (2275868)Time elapsed: 0.095 s
% 11.46/4.43 % (2275868)Peak memory usage: 113 MB
% 11.46/4.43 % (2275868)Instructions burned: 128 (million)
% 11.46/4.43 % (2275872)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3230158788:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 11.46/4.43 % (2275873)lrs+10_1_sil=8000:sp=occurrence:random_seed=2939753323:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 11.46/4.43 % (2275872)Instruction limit reached!
% 11.46/4.43 % (2275872)------------------------------
% 11.46/4.43 % (2275872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275872)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275872)Termination reason: Instruction limit
% 11.46/4.43 % (2275872)Termination phase: Property scanning
% 11.46/4.43 % (2275872)Time elapsed: 0.050 s
% 11.46/4.43 % (2275872)Peak memory usage: 112 MB
% 11.46/4.43 % (2275872)Instructions burned: 115 (million)
% 11.46/4.43 % (2275874)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4066422597:i=437:sd=1:aac=none:ss=included_2979 on theBenchmark for (2979ds/437Mi)
% 11.46/4.43 % (2275877)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=596557079:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 11.46/4.43 % (2275874)Refutation not found, incomplete strategy
% 11.46/4.43 % (2275874)------------------------------
% 11.46/4.43 % (2275874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275874)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275874)Termination reason: Refutation not found, incomplete strategy
% 11.46/4.43 % (2275874)Time elapsed: 0.125 s
% 11.46/4.43 % (2275874)Peak memory usage: 117 MB
% 11.46/4.43 % (2275874)Instructions burned: 145 (million)
% 11.46/4.43 % (2275874)------------------------------
% 11.46/4.43 % (2275874)------------------------------
% 11.46/4.43 % (2275873)Instruction limit reached!
% 11.46/4.43 % (2275873)------------------------------
% 11.46/4.43 % (2275873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275873)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275873)Termination reason: Instruction limit
% 11.46/4.43 % (2275873)Termination phase: Property scanning
% 11.46/4.43 % (2275873)Time elapsed: 0.544 s
% 11.46/4.43 % (2275873)Peak memory usage: 132 MB
% 11.46/4.43 % (2275873)Instructions burned: 909 (million)
% 11.46/4.43 % (2275880)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2867099092:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2973 on theBenchmark for (2973ds/134Mi)
% 11.46/4.43 % (2275881)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2115304846:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi)
% 11.46/4.43 % (2275880)Instruction limit reached!
% 11.46/4.43 % (2275880)------------------------------
% 11.46/4.43 % (2275880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275880)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275880)Termination reason: Instruction limit
% 11.46/4.43 % (2275880)Termination phase: Property scanning
% 11.46/4.43 % (2275880)Time elapsed: 0.124 s
% 11.46/4.43 % (2275880)Peak memory usage: 115 MB
% 11.46/4.43 % (2275880)Instructions burned: 134 (million)
% 11.46/4.43 % (2275865)Instruction limit reached!
% 11.46/4.43 % (2275865)------------------------------
% 11.46/4.43 % (2275865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275865)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275865)Termination reason: Instruction limit
% 11.46/4.43 % (2275865)Termination phase: Property scanning
% 11.46/4.43 % (2275865)Time elapsed: 1.261 s
% 11.46/4.43 % (2275865)Peak memory usage: 171 MB
% 11.46/4.43 % (2275865)Instructions burned: 2352 (million)
% 11.46/4.43 % (2275884)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3904717061:st=3:i=13193:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/13193Mi)
% 11.46/4.43 % (2275844)First to succeed.
% 11.46/4.43 % (2275844)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2275837"
% 11.46/4.43 % (2275885)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=4114511156:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 11.46/4.43 % (2275885)Instruction limit reached!
% 11.46/4.43 % (2275885)------------------------------
% 11.46/4.43 % (2275885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275885)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275885)Termination reason: Instruction limit
% 11.46/4.43 % (2275885)Termination phase: Property scanning
% 11.46/4.43 % (2275885)Time elapsed: 0.056 s
% 11.46/4.43 % (2275885)Peak memory usage: 112 MB
% 11.46/4.43 % (2275885)Instructions burned: 125 (million)
% 11.46/4.43 % (2275881)Instruction limit reached!
% 11.46/4.43 % (2275881)------------------------------
% 11.46/4.43 % (2275881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.46/4.43 % (2275881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/4.43 % (2275881)CaDiCaL version: 2.1.3
% 11.46/4.43 % (2275881)Termination reason: Instruction limit
% 11.46/4.43 % (2275881)Termination phase: Preprocessing 3
% 11.46/4.43 % (2275881)Time elapsed: 0.464 s
% 11.46/4.43 % (2275881)Peak memory usage: 134 MB
% 11.46/4.43 % (2275881)Instructions burned: 593 (million)
% 11.46/4.43 % (2275888)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1988519668:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 11.46/4.43 % (2275889)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=588956235:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/141Mi)
% 11.46/4.43 % (2275844)Refutation found. Thanks to Tanya!
% 11.46/4.43 % SZS status Theorem for theBenchmark
% 11.46/4.43 % SZS output start Proof for theBenchmark
% See solution above
% 18.98/4.66 % (2275844)------------------------------
% 18.98/4.66 % (2275844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.98/4.66 % (2275844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.98/4.66 % (2275844)CaDiCaL version: 2.1.3
% 18.98/4.66 % (2275844)Termination reason: Refutation
% 18.98/4.66 % (2275844)Time elapsed: 1.980 s
% 18.98/4.66 % (2275844)Peak memory usage: 176 MB
% 18.98/4.66 % (2275844)Instructions burned: 3049 (million)
% 18.98/4.66 % (2275844)------------------------------
% 18.98/4.66 % (2275844)------------------------------
% 18.98/4.66 % (2275837)Success in time 3.558 s
% 18.98/4.66 % Vampire exiting
%------------------------------------------------------------------------------