%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV574+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:58:22 PM UTC 2026
% Result : Theorem 37.09s 6.94s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 75
% Syntax : Number of formulae : 600 ( 147 unt; 65 def)
% Number of atoms : 1385 ( 194 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1290 ( 505 ~; 714 |; 17 &)
% ( 51 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 10 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 46 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 21 con; 0-2 aty)
% Number of variables : 294 ( 0 sgn 292 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X0)
=> mem(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subq_def) ).
fof(f2,axiom,
! [X0,X1] :
( subq(X0,X1)
=> ( subq(X1,X0)
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setext) ).
fof(f4,axiom,
! [X0] : ~ mem(X0,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_ax) ).
fof(f5,axiom,
! [X0,X1] :
( mem(X0,s(X1))
<=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s_ax) ).
fof(f6,axiom,
! [X0,X1,X2] :
( mem(X0,u(X1,X2))
<=> ( mem(X0,X1)
| mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_ax) ).
fof(f7,axiom,
! [X0,X1,X2] :
( mem(X0,m(X1,X2))
<=> ( mem(X0,X1)
& ~ mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n_def) ).
fof(f10,axiom,
! [X0,X1] :
( mem(X0,p(X1))
<=> subq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p_ax) ).
fof(f26,conjecture,
subq(u(m(p(u(n(e),n(s(n(e))))),a(p(s(n(e))),n(n(e)))),s(s(n(n(e))))),u(a(a(p(p(s(n(e)))),n(s(n(e)))),u(n(e),n(s(n(e))))),s(s(n(n(e)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subq_498_499) ).
fof(f27,negated_conjecture,
~ subq(u(m(p(u(n(e),n(s(n(e))))),a(p(s(n(e))),n(n(e)))),s(s(n(n(e))))),u(a(a(p(p(s(n(e)))),n(s(n(e)))),u(n(e),n(s(n(e))))),s(s(n(n(e)))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
~ subq(u(m(p(u(n(e),n(s(n(e))))),a(p(s(n(e))),n(n(e)))),s(s(n(n(e))))),u(a(a(p(p(s(n(e)))),n(s(n(e)))),u(n(e),n(s(n(e))))),s(s(n(n(e)))))),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f30,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f31,plain,
! [X0,X1] :
( X0 = X1
| ~ subq(X1,X0)
| ~ subq(X0,X1) ),
inference(flattening,[],[f30]) ).
fof(f32,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ? [X2] :
( ~ mem(X2,X1)
& mem(X2,X0) ) )
& ( ! [X2] :
( mem(X2,X1)
| ~ mem(X2,X0) )
| ~ subq(X0,X1) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f33,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ? [X2] :
( ~ mem(X2,X1)
& mem(X2,X0) ) )
& ( ! [X3] :
( mem(X3,X1)
| ~ mem(X3,X0) )
| ~ subq(X0,X1) ) ),
inference(rectify,[],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( ( subq(X0,X1)
| ( ~ mem(sK0(X0,X1),X1)
& mem(sK0(X0,X1),X0) ) )
& ( ! [X3] :
( mem(X3,X1)
| ~ mem(X3,X0) )
| ~ subq(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f33]) ).
fof(f35,plain,
! [X0,X1] :
( ( mem(X0,s(X1))
| X0 != X1 )
& ( X0 = X1
| ~ mem(X0,s(X1)) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ( mem(X0,u(X1,X2))
| ( ~ mem(X0,X1)
& ~ mem(X0,X2) ) )
& ( mem(X0,X1)
| mem(X0,X2)
| ~ mem(X0,u(X1,X2)) ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f37,plain,
! [X0,X1,X2] :
( ( mem(X0,u(X1,X2))
| ( ~ mem(X0,X1)
& ~ mem(X0,X2) ) )
& ( mem(X0,X1)
| mem(X0,X2)
| ~ mem(X0,u(X1,X2)) ) ),
inference(flattening,[],[f36]) ).
fof(f38,plain,
! [X0,X1,X2] :
( ( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) )
& ( ( mem(X0,X1)
& ~ mem(X0,X2) )
| ~ mem(X0,m(X1,X2)) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X0,X1,X2] :
( ( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) )
& ( ( mem(X0,X1)
& ~ mem(X0,X2) )
| ~ mem(X0,m(X1,X2)) ) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( ( mem(X0,p(X1))
| ~ subq(X0,X1) )
& ( subq(X0,X1)
| ~ mem(X0,p(X1)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f41,plain,
! [X3,X0,X1] :
( ~ mem(X3,X0)
| mem(X3,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f42,plain,
! [X0,X1] :
( mem(sK0(X0,X1),X0)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f43,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
fof(f44,plain,
! [X0,X1] :
( ~ subq(X1,X0)
| X0 = X1
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
fof(f45,plain,
! [X0] : ~ mem(X0,e),
inference(cnf_transformation,[],[f4]) ).
fof(f46,plain,
! [X0,X1] :
( ~ mem(X0,s(X1))
| X0 = X1 ),
inference(cnf_transformation,[],[f35]) ).
fof(f47,plain,
! [X0,X1] :
( mem(X0,s(X1))
| X0 != X1 ),
inference(cnf_transformation,[],[f35]) ).
fof(f48,plain,
! [X2,X0,X1] :
( ~ mem(X0,u(X1,X2))
| mem(X0,X2)
| mem(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f49,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f37]) ).
fof(f50,plain,
! [X2,X0,X1] :
( mem(X0,u(X1,X2))
| ~ mem(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f51,plain,
! [X2,X0,X1] :
( ~ mem(X0,m(X1,X2))
| ~ mem(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f52,plain,
! [X2,X0,X1] :
( ~ mem(X0,m(X1,X2))
| mem(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f53,plain,
! [X2,X0,X1] :
( mem(X0,m(X1,X2))
| ~ mem(X0,X1)
| mem(X0,X2) ),
inference(cnf_transformation,[],[f39]) ).
fof(f54,plain,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
inference(cnf_transformation,[],[f8]) ).
fof(f55,plain,
! [X0] : n(X0) = a(X0,X0),
inference(cnf_transformation,[],[f9]) ).
fof(f56,plain,
! [X0,X1] :
( ~ mem(X0,p(X1))
| subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f57,plain,
! [X0,X1] :
( mem(X0,p(X1))
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
fof(f58,plain,
~ subq(u(m(p(u(n(e),n(s(n(e))))),a(p(s(n(e))),n(n(e)))),s(s(n(n(e))))),u(a(a(p(p(s(n(e)))),n(s(n(e)))),u(n(e),n(s(n(e))))),s(s(n(n(e)))))),
inference(cnf_transformation,[],[f28]) ).
fof(f59,plain,
! [X0] : n(X0) = u(X0,s(X0)),
inference(definition_unfolding,[],[f55,f54]) ).
fof(f60,plain,
~ subq(u(m(p(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),u(p(s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))),s(s(u(u(e,s(e)),s(u(e,s(e))))))),u(u(u(p(p(s(u(e,s(e))))),s(u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))))),s(s(u(u(e,s(e)),s(u(e,s(e)))))))),
inference(definition_unfolding,[],[f58,f59,f59,f59,f54,f59,f59,f59,f59,f59,f54,f54,f59,f59,f59,f59,f59,f59,f59,f59]) ).
fof(f61,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f47]) ).
fof(f62,definition,
sF1 = s(e),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f63,plain,
s(e) = sF1,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF2 = u(e,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f65,plain,
u(e,sF1) = sF2,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF3 = s(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f67,plain,
s(sF2) = sF3,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF4 = s(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f69,plain,
s(sF3) = sF4,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF5 = u(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f71,plain,
u(sF3,sF4) = sF5,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF6 = u(sF2,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f73,plain,
u(sF2,sF5) = sF6,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF7 = p(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f75,plain,
p(sF6) = sF7,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF8 = p(sF3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f77,plain,
p(sF3) = sF8,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF9 = u(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f79,plain,
u(sF2,sF3) = sF9,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF10 = s(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f81,plain,
s(sF9) = sF10,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF11 = u(sF8,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f83,plain,
u(sF8,sF10) = sF11,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF12 = m(sF7,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f85,plain,
m(sF7,sF11) = sF12,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF13 = s(sF10),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f87,plain,
s(sF10) = sF13,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF14 = u(sF12,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f89,plain,
u(sF12,sF13) = sF14,
inference(reorient_equations,[],[f88]) ).
fof(f90,definition,
sF15 = p(sF8),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f91,plain,
p(sF8) = sF15,
inference(reorient_equations,[],[f90]) ).
fof(f92,definition,
sF16 = s(sF5),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f93,plain,
s(sF5) = sF16,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF17 = u(sF15,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f95,plain,
u(sF15,sF16) = sF17,
inference(reorient_equations,[],[f94]) ).
fof(f96,definition,
sF18 = s(sF6),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f97,plain,
s(sF6) = sF18,
inference(reorient_equations,[],[f96]) ).
fof(f98,definition,
sF19 = u(sF17,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f99,plain,
u(sF17,sF18) = sF19,
inference(reorient_equations,[],[f98]) ).
fof(f100,definition,
sF20 = u(sF19,sF13),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f101,plain,
u(sF19,sF13) = sF20,
inference(reorient_equations,[],[f100]) ).
fof(f102,plain,
~ subq(sF14,sF20),
inference(definition_folding,[],[f60,f101,f87,f81,f79,f67,f65,f63,f65,f63,f99,f97,f73,f71,f69,f67,f65,f63,f67,f65,f63,f65,f63,f95,f93,f71,f69,f67,f65,f63,f67,f65,f63,f91,f77,f67,f65,f63,f89,f87,f81,f79,f67,f65,f63,f65,f63,f85,f83,f81,f79,f67,f65,f63,f65,f63,f77,f67,f65,f63,f75,f73,f71,f69,f67,f65,f63,f67,f65,f63,f65,f63]) ).
fof(f103,plain,
! [X0] :
( subq(X0,X0)
| subq(X0,X0) ),
inference(resolution,[],[f42,f43]) ).
fof(f104,plain,
! [X0] : subq(X0,X0),
inference(duplicate_literal_removal,[],[f103]) ).
fof(f105,plain,
mem(e,sF1),
inference(superposition,[],[f61,f63]) ).
fof(f106,plain,
mem(sF2,sF3),
inference(superposition,[],[f61,f67]) ).
fof(f107,plain,
mem(sF3,sF4),
inference(superposition,[],[f61,f69]) ).
fof(f108,plain,
mem(sF5,sF16),
inference(superposition,[],[f61,f93]) ).
fof(f109,plain,
mem(sF6,sF18),
inference(superposition,[],[f61,f97]) ).
fof(f110,plain,
mem(sF9,sF10),
inference(superposition,[],[f61,f81]) ).
fof(f115,plain,
! [X0] :
( ~ mem(X0,sF7)
| subq(X0,sF6) ),
inference(superposition,[],[f56,f75]) ).
fof(f116,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f49,f43]) ).
fof(f117,plain,
! [X0] :
( ~ mem(X0,sF1)
| mem(X0,sF2) ),
inference(superposition,[],[f49,f65]) ).
fof(f118,plain,
! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF5) ),
inference(superposition,[],[f49,f71]) ).
fof(f120,plain,
! [X0] :
( ~ mem(X0,sF13)
| mem(X0,sF20) ),
inference(superposition,[],[f49,f101]) ).
fof(f123,plain,
! [X0] :
( ~ mem(X0,sF10)
| mem(X0,sF11) ),
inference(superposition,[],[f49,f83]) ).
fof(f124,plain,
! [X0] :
( ~ mem(X0,sF16)
| mem(X0,sF17) ),
inference(superposition,[],[f49,f95]) ).
fof(f125,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f50,f43]) ).
fof(f127,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF5) ),
inference(superposition,[],[f50,f71]) ).
fof(f128,plain,
! [X0] :
( ~ mem(X0,sF8)
| mem(X0,sF11) ),
inference(superposition,[],[f50,f83]) ).
fof(f130,plain,
! [X0] :
( ~ mem(X0,sF15)
| mem(X0,sF17) ),
inference(superposition,[],[f50,f95]) ).
fof(f131,plain,
! [X0] :
( ~ mem(X0,sF19)
| mem(X0,sF20) ),
inference(superposition,[],[f50,f101]) ).
fof(f134,plain,
! [X0] :
( ~ mem(X0,sF17)
| mem(X0,sF19) ),
inference(superposition,[],[f50,f99]) ).
fof(f135,plain,
! [X0] :
( ~ mem(X0,sF18)
| mem(X0,sF19) ),
inference(superposition,[],[f49,f99]) ).
fof(f136,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF9) ),
inference(superposition,[],[f50,f79]) ).
fof(f137,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF9) ),
inference(superposition,[],[f49,f79]) ).
fof(f138,plain,
! [X2,X0,X1] :
( mem(sK0(u(X0,X1),X2),X1)
| mem(sK0(u(X0,X1),X2),X0)
| subq(u(X0,X1),X2) ),
inference(resolution,[],[f48,f42]) ).
fof(f141,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF1)
| mem(X0,e) ),
inference(superposition,[],[f48,f65]) ).
fof(f143,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF4)
| mem(X0,sF3) ),
inference(superposition,[],[f48,f71]) ).
fof(f145,plain,
! [X0] :
( ~ mem(X0,sF14)
| mem(X0,sF13)
| mem(X0,sF12) ),
inference(superposition,[],[f48,f89]) ).
fof(f149,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF1) ),
inference(forward_subsumption_resolution,[],[f141,f45]) ).
fof(f150,plain,
! [X2,X0,X1] :
( mem(sK0(m(X0,X1),X2),X0)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f52,f42]) ).
fof(f151,plain,
! [X0] :
( ~ mem(X0,sF12)
| mem(X0,sF7) ),
inference(superposition,[],[f52,f85]) ).
fof(f152,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,m(X1,X2)),X1)
| mem(sK0(X0,m(X1,X2)),X2)
| subq(X0,m(X1,X2)) ),
inference(resolution,[],[f53,f43]) ).
fof(f155,plain,
! [X0] :
( ~ mem(X0,sF6)
| mem(X0,sF5)
| mem(X0,sF2) ),
inference(superposition,[],[f48,f73]) ).
fof(f158,plain,
! [X0,X1] :
( subq(s(X0),X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f46,f42]) ).
fof(f160,plain,
! [X0] :
( ~ mem(X0,sF1)
| e = X0 ),
inference(superposition,[],[f46,f63]) ).
fof(f161,plain,
! [X0] :
( ~ mem(X0,sF3)
| sF2 = X0 ),
inference(superposition,[],[f46,f67]) ).
fof(f162,plain,
! [X0] :
( ~ mem(X0,sF4)
| sF3 = X0 ),
inference(superposition,[],[f46,f69]) ).
fof(f168,plain,
mem(e,sF2),
inference(resolution,[],[f117,f105]) ).
fof(f172,plain,
! [X0] : subq(e,X0),
inference(resolution,[],[f45,f42]) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ mem(sK0(m(X0,X1),X2),X1)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f51,f42]) ).
fof(f176,plain,
! [X0] :
( ~ mem(X0,sF12)
| ~ mem(X0,sF11) ),
inference(superposition,[],[f51,f85]) ).
fof(f180,plain,
mem(sF3,sF5),
inference(resolution,[],[f107,f118]) ).
fof(f181,plain,
! [X0] :
( mem(sK0(sF14,X0),sF12)
| mem(sK0(sF14,X0),sF13)
| subq(sF14,X0) ),
inference(resolution,[],[f145,f42]) ).
fof(f194,plain,
mem(sF2,sF5),
inference(resolution,[],[f106,f127]) ).
fof(f211,plain,
mem(sF2,sF9),
inference(resolution,[],[f137,f106]) ).
fof(f218,plain,
mem(sF5,sF17),
inference(resolution,[],[f108,f124]) ).
fof(f220,plain,
! [X0] :
( mem(sK0(sF14,X0),sF7)
| mem(sK0(sF14,X0),sF13)
| subq(sF14,X0) ),
inference(resolution,[],[f151,f181]) ).
fof(f234,plain,
! [X0] :
( mem(sK0(sF5,X0),sF4)
| mem(sK0(sF5,X0),sF3)
| subq(sF5,X0) ),
inference(resolution,[],[f143,f42]) ).
fof(f236,plain,
! [X0] :
( mem(sK0(sF2,X0),sF1)
| subq(sF2,X0) ),
inference(resolution,[],[f149,f42]) ).
fof(f238,plain,
mem(sF6,sF19),
inference(resolution,[],[f109,f135]) ).
fof(f290,plain,
mem(sF9,sF11),
inference(resolution,[],[f110,f123]) ).
fof(f291,plain,
mem(e,sF9),
inference(resolution,[],[f136,f168]) ).
fof(f348,plain,
mem(sF5,sF19),
inference(resolution,[],[f218,f134]) ).
fof(f357,plain,
! [X0,X1] :
( subq(X0,u(X1,X0))
| subq(X0,u(X1,X0)) ),
inference(resolution,[],[f116,f42]) ).
fof(f376,plain,
! [X0] :
( ~ mem(sK0(X0,sF20),sF13)
| subq(X0,sF20) ),
inference(superposition,[],[f116,f101]) ).
fof(f384,plain,
! [X0,X1] : subq(X0,u(X1,X0)),
inference(duplicate_literal_removal,[],[f357]) ).
fof(f393,plain,
! [X0,X1] :
( subq(X0,u(X0,X1))
| subq(X0,u(X0,X1)) ),
inference(resolution,[],[f125,f42]) ).
fof(f412,plain,
! [X0] :
( ~ mem(sK0(X0,sF20),sF19)
| subq(X0,sF20) ),
inference(superposition,[],[f125,f101]) ).
fof(f420,plain,
! [X0,X1] : subq(X0,u(X0,X1)),
inference(duplicate_literal_removal,[],[f393]) ).
fof(f429,plain,
subq(sF1,sF2),
inference(superposition,[],[f384,f65]) ).
fof(f462,plain,
! [X0] :
( ~ subq(X0,sF3)
| mem(X0,sF8) ),
inference(superposition,[],[f57,f77]) ).
fof(f463,plain,
! [X0] :
( ~ subq(X0,sF8)
| mem(X0,sF15) ),
inference(superposition,[],[f57,f91]) ).
fof(f506,definition,
( spl21_28
<=> mem(e,sF8) ),
introduced(definition,[new_symbols(definition,[spl21_28])],[avatar_definition]) ).
fof(f508,plain,
( mem(e,sF8)
| ~ spl21_28 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f518,plain,
mem(sF3,sF8),
inference(resolution,[],[f462,f104]) ).
fof(f519,plain,
mem(e,sF8),
inference(resolution,[],[f462,f172]) ).
fof(f520,plain,
spl21_28,
inference(avatar_split_clause,[],[f519,f506]) ).
fof(f533,plain,
mem(e,sF15),
inference(resolution,[],[f463,f172]) ).
fof(f542,plain,
mem(e,sF17),
inference(resolution,[],[f533,f130]) ).
fof(f544,plain,
mem(e,sF19),
inference(resolution,[],[f542,f134]) ).
fof(f546,plain,
mem(e,sF20),
inference(resolution,[],[f544,f131]) ).
fof(f557,plain,
( subq(sF2,sF1)
| subq(sF2,sF1) ),
inference(resolution,[],[f236,f43]) ).
fof(f564,plain,
subq(sF2,sF1),
inference(duplicate_literal_removal,[],[f557]) ).
fof(f616,plain,
! [X0,X1] :
( mem(sK0(X0,m(X0,X1)),X1)
| subq(X0,m(X0,X1))
| subq(X0,m(X0,X1)) ),
inference(resolution,[],[f152,f42]) ).
fof(f638,plain,
! [X0,X1] :
( mem(sK0(X0,m(X0,X1)),X1)
| subq(X0,m(X0,X1)) ),
inference(duplicate_literal_removal,[],[f616]) ).
fof(f649,plain,
! [X0,X1] :
( subq(m(X0,X1),X0)
| subq(m(X0,X1),X0) ),
inference(resolution,[],[f150,f43]) ).
fof(f658,plain,
! [X2,X0,X1] :
( subq(m(s(X0),X1),X2)
| sK0(m(s(X0),X1),X2) = X0 ),
inference(resolution,[],[f150,f46]) ).
fof(f710,plain,
! [X0,X1] : subq(m(X0,X1),X0),
inference(duplicate_literal_removal,[],[f649]) ).
fof(f737,plain,
! [X0,X1] :
( ~ subq(s(X0),X1)
| mem(X0,X1) ),
inference(resolution,[],[f41,f61]) ).
fof(f739,plain,
! [X2,X3,X0,X1] :
( ~ subq(u(X2,X3),X1)
| mem(X0,X1)
| ~ mem(X0,X3) ),
inference(resolution,[],[f41,f49]) ).
fof(f740,plain,
! [X2,X3,X0,X1] :
( ~ subq(m(X2,X3),X1)
| mem(X0,X1)
| ~ mem(X0,X2)
| mem(X0,X3) ),
inference(resolution,[],[f41,f53]) ).
fof(f753,plain,
! [X2,X0,X1] :
( mem(sK0(X0,X1),X2)
| ~ subq(X0,X2)
| subq(X0,X1) ),
inference(resolution,[],[f41,f42]) ).
fof(f756,plain,
! [X0,X1] :
( mem(sK0(sF14,X0),sF13)
| mem(sK0(sF14,X0),X1)
| ~ subq(sF7,X1)
| subq(sF14,X0) ),
inference(resolution,[],[f41,f220]) ).
fof(f757,plain,
! [X0,X1] :
( mem(sK0(sF14,X0),sF13)
| mem(sK0(sF14,X0),X1)
| ~ subq(sF12,X1)
| subq(sF14,X0) ),
inference(resolution,[],[f41,f181]) ).
fof(f813,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF2)
| subq(X0,X1)
| ~ subq(X0,sF1) ),
inference(resolution,[],[f753,f117]) ).
fof(f824,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF5)
| subq(X0,X1)
| ~ subq(X0,sF6)
| mem(sK0(X0,X1),sF2) ),
inference(resolution,[],[f753,f155]) ).
fof(f837,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF20)
| subq(X0,X1)
| ~ subq(X0,sF13) ),
inference(resolution,[],[f753,f120]) ).
fof(f841,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF17)
| subq(X0,X1)
| ~ subq(X0,sF15) ),
inference(resolution,[],[f753,f130]) ).
fof(f845,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF19)
| subq(X0,X1)
| ~ subq(X0,sF17) ),
inference(resolution,[],[f753,f134]) ).
fof(f1044,plain,
! [X0,X1] :
( mem(sK0(u(X0,e),X1),X0)
| subq(u(X0,e),X1) ),
inference(resolution,[],[f138,f45]) ).
fof(f1089,plain,
! [X0,X1] :
( mem(sK0(u(X0,X1),X0),X1)
| subq(u(X0,X1),X0)
| subq(u(X0,X1),X0) ),
inference(resolution,[],[f138,f43]) ).
fof(f1092,plain,
! [X2,X0,X1] :
( mem(sK0(u(X0,X1),u(X2,X0)),X1)
| subq(u(X0,X1),u(X2,X0))
| subq(u(X0,X1),u(X2,X0)) ),
inference(resolution,[],[f138,f116]) ).
fof(f1166,plain,
! [X2,X0,X1] :
( mem(sK0(u(X0,X1),u(X2,X0)),X1)
| subq(u(X0,X1),u(X2,X0)) ),
inference(duplicate_literal_removal,[],[f1092]) ).
fof(f1169,plain,
! [X0,X1] :
( mem(sK0(u(X0,X1),X0),X1)
| subq(u(X0,X1),X0) ),
inference(duplicate_literal_removal,[],[f1089]) ).
fof(f1490,plain,
! [X0,X1] :
( mem(X0,X1)
| sK0(s(X0),X1) = X0 ),
inference(resolution,[],[f737,f158]) ).
fof(f1539,plain,
! [X0] :
( mem(X0,sF17)
| sK0(s(X0),sF15) = X0 ),
inference(resolution,[],[f1490,f130]) ).
fof(f1551,plain,
! [X0,X1] :
( subq(X0,X1)
| sK0(X0,X1) = sK0(s(sK0(X0,X1)),X1) ),
inference(resolution,[],[f1490,f43]) ).
fof(f1558,plain,
! [X0] :
( subq(X0,sF20)
| sK0(X0,sF20) = sK0(s(sK0(X0,sF20)),sF13) ),
inference(resolution,[],[f1490,f376]) ).
fof(f1623,plain,
! [X0] : subq(X0,m(X0,e)),
inference(resolution,[],[f638,f45]) ).
fof(f4143,plain,
! [X0] :
( ~ subq(X0,e)
| e = X0 ),
inference(resolution,[],[f44,f172]) ).
fof(f4161,plain,
( sF1 = sF2
| ~ subq(sF1,sF2) ),
inference(resolution,[],[f44,f564]) ).
fof(f4306,plain,
sF1 = sF2,
inference(forward_subsumption_resolution,[],[f4161,f429]) ).
fof(f4335,plain,
! [X0] :
( ~ mem(X0,sF2)
| e = X0 ),
inference(superposition,[],[f160,f4306]) ).
fof(f5389,plain,
! [X0,X1] :
( sK0(m(s(X0),X1),e) = X0
| e = m(s(X0),X1) ),
inference(resolution,[],[f4143,f658]) ).
fof(f5952,plain,
! [X0] : subq(u(X0,e),X0),
inference(resolution,[],[f1169,f45]) ).
fof(f6069,plain,
! [X0] :
( u(X0,e) = X0
| ~ subq(X0,u(X0,e)) ),
inference(resolution,[],[f5952,f44]) ).
fof(f6084,plain,
! [X0] : u(X0,e) = X0,
inference(forward_subsumption_resolution,[],[f6069,f420]) ).
fof(f7261,plain,
! [X0] :
( mem(sK0(sF14,sF20),X0)
| ~ subq(sF7,X0)
| subq(sF14,sF20)
| subq(sF14,sF20) ),
inference(resolution,[],[f756,f376]) ).
fof(f7329,plain,
! [X0] :
( mem(sK0(sF14,sF20),X0)
| ~ subq(sF7,X0)
| subq(sF14,sF20) ),
inference(duplicate_literal_removal,[],[f7261]) ).
fof(f7416,plain,
! [X0] :
( mem(sK0(sF14,sF20),X0)
| ~ subq(sF7,X0) ),
inference(forward_subsumption_resolution,[],[f7329,f102]) ).
fof(f9116,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| subq(m(s(X0),X1),e)
| e = m(s(X0),X1) ),
inference(superposition,[],[f174,f5389]) ).
fof(f9133,plain,
! [X0,X1] :
( ~ mem(X0,X1)
| e = m(s(X0),X1) ),
inference(forward_subsumption_resolution,[],[f9116,f4143]) ).
fof(f9171,plain,
e = m(s(e),sF19),
inference(resolution,[],[f9133,f544]) ).
fof(f9172,plain,
e = m(s(e),sF20),
inference(resolution,[],[f9133,f546]) ).
fof(f12402,plain,
e = m(sF1,sF19),
inference(forward_demodulation,[],[f9171,f63]) ).
fof(f12520,plain,
e = m(sF2,sF19),
inference(forward_demodulation,[],[f12402,f4306]) ).
fof(f13131,plain,
! [X0] :
( mem(X0,e)
| ~ mem(X0,sF2)
| mem(X0,sF19) ),
inference(superposition,[],[f53,f12520]) ).
fof(f13145,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF19) ),
inference(forward_subsumption_resolution,[],[f13131,f45]) ).
fof(f14869,plain,
! [X0] :
( m(X0,e) = X0
| ~ subq(m(X0,e),X0) ),
inference(resolution,[],[f1623,f44]) ).
fof(f14904,plain,
! [X0] : m(X0,e) = X0,
inference(forward_subsumption_resolution,[],[f14869,f710]) ).
fof(f15009,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF4)
| ~ subq(X0,sF6)
| mem(sK0(X0,X1),sF2)
| subq(X0,X1)
| mem(sK0(X0,X1),sF3) ),
inference(resolution,[],[f824,f143]) ).
fof(f16998,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF2)
| ~ subq(X0,sF6)
| subq(X0,X1)
| mem(sK0(X0,X1),sF3)
| sK0(X0,X1) = sF3 ),
inference(resolution,[],[f15009,f162]) ).
fof(f17162,plain,
! [X0,X1] :
( mem(sK0(X0,X1),sF3)
| subq(X0,X1)
| ~ subq(X0,sF6)
| sK0(X0,X1) = sF3
| e = sK0(X0,X1) ),
inference(resolution,[],[f16998,f4335]) ).
fof(f23592,plain,
! [X0,X1] :
( subq(u(X0,X1),u(X1,X0))
| subq(u(X0,X1),u(X1,X0)) ),
inference(resolution,[],[f1166,f125]) ).
fof(f23754,plain,
! [X0,X1] : subq(u(X0,X1),u(X1,X0)),
inference(duplicate_literal_removal,[],[f23592]) ).
fof(f23773,plain,
! [X0,X1] :
( u(X0,X1) = u(X1,X0)
| ~ subq(u(X0,X1),u(X1,X0)) ),
inference(resolution,[],[f23754,f44]) ).
fof(f23817,plain,
! [X0,X1] : u(X0,X1) = u(X1,X0),
inference(forward_subsumption_resolution,[],[f23773,f23754]) ).
fof(f23931,plain,
sF9 = u(sF3,sF2),
inference(superposition,[],[f79,f23817]) ).
fof(f30856,plain,
! [X0] :
( mem(sK0(sF14,sF20),X0)
| ~ subq(sF12,X0)
| subq(sF14,sF20)
| subq(sF14,sF20) ),
inference(resolution,[],[f757,f376]) ).
fof(f30979,plain,
! [X0] :
( mem(sK0(sF14,sF20),X0)
| ~ subq(sF12,X0)
| subq(sF14,sF20) ),
inference(duplicate_literal_removal,[],[f30856]) ).
fof(f31046,plain,
! [X0] :
( mem(sK0(sF14,sF20),X0)
| ~ subq(sF12,X0) ),
inference(forward_subsumption_resolution,[],[f30979,f102]) ).
fof(f33741,plain,
sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF20),
inference(resolution,[],[f1551,f102]) ).
fof(f34293,plain,
! [X0] :
( subq(X0,sF20)
| ~ subq(X0,sF17)
| subq(X0,sF20) ),
inference(resolution,[],[f845,f412]) ).
fof(f34446,plain,
! [X0] :
( ~ subq(X0,sF17)
| subq(X0,sF20) ),
inference(duplicate_literal_removal,[],[f34293]) ).
fof(f37143,plain,
e = m(sF1,sF20),
inference(forward_demodulation,[],[f9172,f63]) ).
fof(f37777,plain,
e = m(sF2,sF20),
inference(forward_demodulation,[],[f37143,f4306]) ).
fof(f39842,definition,
( spl21_958
<=> mem(sK0(sF14,sF20),sF11) ),
introduced(definition,[new_symbols(definition,[spl21_958])],[avatar_definition]) ).
fof(f39843,plain,
( ~ mem(sK0(sF14,sF20),sF11)
| spl21_958 ),
inference(avatar_component_clause,[],[f39842]) ).
fof(f39844,plain,
( mem(sK0(sF14,sF20),sF11)
| ~ spl21_958 ),
inference(avatar_component_clause,[],[f39842]) ).
fof(f39855,definition,
( spl21_961
<=> mem(sK0(sF14,sF20),sF2) ),
introduced(definition,[new_symbols(definition,[spl21_961])],[avatar_definition]) ).
fof(f39856,plain,
( ~ mem(sK0(sF14,sF20),sF2)
| spl21_961 ),
inference(avatar_component_clause,[],[f39855]) ).
fof(f39857,plain,
( mem(sK0(sF14,sF20),sF2)
| ~ spl21_961 ),
inference(avatar_component_clause,[],[f39855]) ).
fof(f39873,definition,
( spl21_965
<=> mem(sK0(sF14,sF20),sF15) ),
introduced(definition,[new_symbols(definition,[spl21_965])],[avatar_definition]) ).
fof(f39874,plain,
( ~ mem(sK0(sF14,sF20),sF15)
| spl21_965 ),
inference(avatar_component_clause,[],[f39873]) ).
fof(f39875,plain,
( mem(sK0(sF14,sF20),sF15)
| ~ spl21_965 ),
inference(avatar_component_clause,[],[f39873]) ).
fof(f39878,definition,
( spl21_966
<=> sF6 = sK0(sF14,sF20) ),
introduced(definition,[new_symbols(definition,[spl21_966])],[avatar_definition]) ).
fof(f39880,plain,
( sF6 = sK0(sF14,sF20)
| ~ spl21_966 ),
inference(avatar_component_clause,[],[f39878]) ).
fof(f39882,definition,
( spl21_967
<=> sF5 = sK0(sF14,sF20) ),
introduced(definition,[new_symbols(definition,[spl21_967])],[avatar_definition]) ).
fof(f39883,plain,
( sF5 != sK0(sF14,sF20)
| spl21_967 ),
inference(avatar_component_clause,[],[f39882]) ).
fof(f39884,plain,
( sF5 = sK0(sF14,sF20)
| ~ spl21_967 ),
inference(avatar_component_clause,[],[f39882]) ).
fof(f39890,definition,
( spl21_969
<=> subq(sK0(sF14,sF20),sF8) ),
introduced(definition,[new_symbols(definition,[spl21_969])],[avatar_definition]) ).
fof(f39891,plain,
( ~ subq(sK0(sF14,sF20),sF8)
| spl21_969 ),
inference(avatar_component_clause,[],[f39890]) ).
fof(f39892,plain,
( subq(sK0(sF14,sF20),sF8)
| ~ spl21_969 ),
inference(avatar_component_clause,[],[f39890]) ).
fof(f39918,definition,
( spl21_975
<=> mem(sK0(sF14,sF20),sF19) ),
introduced(definition,[new_symbols(definition,[spl21_975])],[avatar_definition]) ).
fof(f39919,plain,
( ~ mem(sK0(sF14,sF20),sF19)
| spl21_975 ),
inference(avatar_component_clause,[],[f39918]) ).
fof(f39920,plain,
( mem(sK0(sF14,sF20),sF19)
| ~ spl21_975 ),
inference(avatar_component_clause,[],[f39918]) ).
fof(f39923,definition,
( spl21_976
<=> mem(sK0(sF14,sF20),sF17) ),
introduced(definition,[new_symbols(definition,[spl21_976])],[avatar_definition]) ).
fof(f39925,plain,
( mem(sK0(sF14,sF20),sF17)
| ~ spl21_976 ),
inference(avatar_component_clause,[],[f39923]) ).
fof(f39985,definition,
( spl21_988
<=> mem(sK0(sF14,sF20),sF8) ),
introduced(definition,[new_symbols(definition,[spl21_988])],[avatar_definition]) ).
fof(f39986,plain,
( ~ mem(sK0(sF14,sF20),sF8)
| spl21_988 ),
inference(avatar_component_clause,[],[f39985]) ).
fof(f39987,plain,
( mem(sK0(sF14,sF20),sF8)
| ~ spl21_988 ),
inference(avatar_component_clause,[],[f39985]) ).
fof(f40023,definition,
( spl21_992
<=> mem(sK0(sF14,sF20),sF20) ),
introduced(definition,[new_symbols(definition,[spl21_992])],[avatar_definition]) ).
fof(f40024,plain,
( mem(sK0(sF14,sF20),sF20)
| ~ spl21_992 ),
inference(avatar_component_clause,[],[f40023]) ).
fof(f40025,plain,
( ~ mem(sK0(sF14,sF20),sF20)
| spl21_992 ),
inference(avatar_component_clause,[],[f40023]) ).
fof(f40316,plain,
! [X0] :
( mem(X0,e)
| ~ mem(X0,sF2)
| mem(X0,sF20) ),
inference(superposition,[],[f53,f37777]) ).
fof(f40337,plain,
! [X0] :
( ~ mem(X0,sF2)
| mem(X0,sF20) ),
inference(forward_subsumption_resolution,[],[f40316,f45]) ).
fof(f40338,plain,
! [X0] :
( mem(X0,sF20)
| sK0(s(X0),sF2) = X0 ),
inference(resolution,[],[f40337,f1490]) ).
fof(f41318,plain,
( ~ subq(sF7,sF7)
| subq(sK0(sF14,sF20),sF6) ),
inference(resolution,[],[f7416,f115]) ).
fof(f41368,plain,
subq(sK0(sF14,sF20),sF6),
inference(forward_subsumption_resolution,[],[f41318,f104]) ).
fof(f41392,plain,
( sF6 = sK0(sF14,sF20)
| ~ subq(sF6,sK0(sF14,sF20)) ),
inference(resolution,[],[f41368,f44]) ).
fof(f41394,definition,
( spl21_1002
<=> subq(sF6,sK0(sF14,sF20)) ),
introduced(definition,[new_symbols(definition,[spl21_1002])],[avatar_definition]) ).
fof(f41396,plain,
( ~ subq(sF6,sK0(sF14,sF20))
| spl21_1002 ),
inference(avatar_component_clause,[],[f41394]) ).
fof(f41397,plain,
( ~ spl21_1002
| spl21_966 ),
inference(avatar_split_clause,[],[f41392,f39878,f41394]) ).
fof(f42896,plain,
( sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF2)
| spl21_992 ),
inference(resolution,[],[f40338,f40025]) ).
fof(f42952,definition,
( spl21_1041
<=> subq(s(sK0(sF14,sF20)),sF2) ),
introduced(definition,[new_symbols(definition,[spl21_1041])],[avatar_definition]) ).
fof(f42953,plain,
( ~ subq(s(sK0(sF14,sF20)),sF2)
| spl21_1041 ),
inference(avatar_component_clause,[],[f42952]) ).
fof(f43445,plain,
! [X0] : subq(m(sF17,X0),sF20),
inference(resolution,[],[f34446,f710]) ).
fof(f44115,plain,
( ~ subq(sF12,sF12)
| ~ mem(sK0(sF14,sF20),sF11) ),
inference(resolution,[],[f31046,f176]) ).
fof(f44154,definition,
( spl21_1085
<=> sF9 = sK0(sF14,sF20) ),
introduced(definition,[new_symbols(definition,[spl21_1085])],[avatar_definition]) ).
fof(f44156,plain,
( sF9 = sK0(sF14,sF20)
| ~ spl21_1085 ),
inference(avatar_component_clause,[],[f44154]) ).
fof(f44161,definition,
( spl21_1086
<=> subq(sK0(sF14,sF20),sF3) ),
introduced(definition,[new_symbols(definition,[spl21_1086])],[avatar_definition]) ).
fof(f44162,plain,
( ~ subq(sK0(sF14,sF20),sF3)
| spl21_1086 ),
inference(avatar_component_clause,[],[f44161]) ).
fof(f44163,plain,
( subq(sK0(sF14,sF20),sF3)
| ~ spl21_1086 ),
inference(avatar_component_clause,[],[f44161]) ).
fof(f44878,plain,
( mem(sK0(sF14,sF20),sF11)
| ~ spl21_988 ),
inference(resolution,[],[f39987,f128]) ).
fof(f44881,plain,
( $false
| spl21_958
| ~ spl21_988 ),
inference(forward_subsumption_resolution,[],[f44878,f39843]) ).
fof(f44882,plain,
( spl21_958
| ~ spl21_988 ),
inference(avatar_contradiction_clause,[],[f44881]) ).
fof(f48389,definition,
( spl21_1206
<=> subq(s(sK0(sF14,sF20)),sF15) ),
introduced(definition,[new_symbols(definition,[spl21_1206])],[avatar_definition]) ).
fof(f48390,plain,
( ~ subq(s(sK0(sF14,sF20)),sF15)
| spl21_1206 ),
inference(avatar_component_clause,[],[f48389]) ).
fof(f48394,definition,
( spl21_1207
<=> subq(s(sK0(sF14,sF20)),sF13) ),
introduced(definition,[new_symbols(definition,[spl21_1207])],[avatar_definition]) ).
fof(f48395,plain,
( ~ subq(s(sK0(sF14,sF20)),sF13)
| spl21_1207 ),
inference(avatar_component_clause,[],[f48394]) ).
fof(f48809,definition,
( spl21_1216
<=> mem(sF3,sK0(sF14,sF20)) ),
introduced(definition,[new_symbols(definition,[spl21_1216])],[avatar_definition]) ).
fof(f48810,plain,
( ~ mem(sF3,sK0(sF14,sF20))
| spl21_1216 ),
inference(avatar_component_clause,[],[f48809]) ).
fof(f48811,plain,
( mem(sF3,sK0(sF14,sF20))
| ~ spl21_1216 ),
inference(avatar_component_clause,[],[f48809]) ).
fof(f51043,plain,
! [X0,X1] :
( ~ mem(X0,sF17)
| mem(X0,sF20)
| mem(X0,X1) ),
inference(resolution,[],[f43445,f740]) ).
fof(f52768,plain,
( mem(sK0(sF14,sF20),sF17)
| subq(s(sK0(sF14,sF20)),sF2)
| ~ subq(s(sK0(sF14,sF20)),sF15)
| spl21_992 ),
inference(superposition,[],[f841,f42896]) ).
fof(f53001,plain,
( mem(sK0(sF14,sF20),sF17)
| ~ subq(s(sK0(sF14,sF20)),sF15)
| spl21_992
| spl21_1041 ),
inference(forward_subsumption_resolution,[],[f52768,f42953]) ).
fof(f53066,plain,
( ~ spl21_1206
| spl21_976
| spl21_992
| spl21_1041 ),
inference(avatar_split_clause,[],[f53001,f42952,f40023,f39923,f48389]) ).
fof(f56059,plain,
( mem(sK0(sF14,sF20),sF20)
| subq(s(sK0(sF14,sF20)),sF20)
| ~ subq(s(sK0(sF14,sF20)),sF13) ),
inference(superposition,[],[f837,f33741]) ).
fof(f56217,plain,
( mem(sK0(sF14,sF20),sF20)
| ~ subq(s(sK0(sF14,sF20)),sF13) ),
inference(forward_subsumption_resolution,[],[f56059,f737]) ).
fof(f56229,plain,
( ~ subq(s(sK0(sF14,sF20)),sF13)
| spl21_992 ),
inference(forward_subsumption_resolution,[],[f56217,f40025]) ).
fof(f56238,plain,
( ~ spl21_1207
| spl21_992 ),
inference(avatar_split_clause,[],[f56229,f40023,f48394]) ).
fof(f56629,plain,
sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF13),
inference(resolution,[],[f1558,f102]) ).
fof(f61459,plain,
! [X0] :
( mem(sK0(sF5,X0),sF3)
| subq(sF5,X0)
| sF3 = sK0(sF5,X0) ),
inference(resolution,[],[f234,f162]) ).
fof(f64535,definition,
( spl21_1458
<=> ! [X0] : mem(sK0(sF14,sF20),X0) ),
introduced(definition,[new_symbols(definition,[spl21_1458])],[avatar_definition]) ).
fof(f64536,plain,
( ! [X0] : mem(sK0(sF14,sF20),X0)
| ~ spl21_1458 ),
inference(avatar_component_clause,[],[f64535]) ).
fof(f69667,plain,
! [X0] :
( mem(X0,sF19)
| sK0(s(X0),sF15) = X0 ),
inference(resolution,[],[f1539,f134]) ).
fof(f69695,plain,
! [X0] :
( subq(X0,sF20)
| sK0(X0,sF20) = sK0(s(sK0(X0,sF20)),sF15) ),
inference(resolution,[],[f69667,f412]) ).
fof(f69769,plain,
sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF15),
inference(resolution,[],[f69695,f102]) ).
fof(f79259,plain,
! [X0,X1] :
( ~ subq(X0,sF6)
| subq(X0,X1)
| sK0(X0,X1) = sF3
| e = sK0(X0,X1)
| sK0(X0,X1) = sF2 ),
inference(resolution,[],[f17162,f161]) ).
fof(f79490,plain,
! [X0] :
( subq(sK0(sF14,sF20),X0)
| sF3 = sK0(sK0(sF14,sF20),X0)
| e = sK0(sK0(sF14,sF20),X0)
| sF2 = sK0(sK0(sF14,sF20),X0) ),
inference(resolution,[],[f79259,f41368]) ).
fof(f79544,plain,
( sF3 = sK0(sK0(sF14,sF20),sF3)
| e = sK0(sK0(sF14,sF20),sF3)
| sF2 = sK0(sK0(sF14,sF20),sF3)
| mem(sK0(sF14,sF20),sF8) ),
inference(resolution,[],[f79490,f462]) ).
fof(f79557,plain,
( sF3 = sK0(sK0(sF14,sF20),sF8)
| e = sK0(sK0(sF14,sF20),sF8)
| sF2 = sK0(sK0(sF14,sF20),sF8)
| mem(sK0(sF14,sF20),sF15) ),
inference(resolution,[],[f79490,f463]) ).
fof(f79656,plain,
( sF3 = sK0(sK0(sF14,sF20),sF8)
| e = sK0(sK0(sF14,sF20),sF8)
| sF2 = sK0(sK0(sF14,sF20),sF8)
| spl21_965 ),
inference(forward_subsumption_resolution,[],[f79557,f39874]) ).
fof(f79658,definition,
( spl21_1748
<=> sF2 = sK0(sK0(sF14,sF20),sF5) ),
introduced(definition,[new_symbols(definition,[spl21_1748])],[avatar_definition]) ).
fof(f79659,plain,
( sF2 != sK0(sK0(sF14,sF20),sF5)
| spl21_1748 ),
inference(avatar_component_clause,[],[f79658]) ).
fof(f79660,plain,
( sF2 = sK0(sK0(sF14,sF20),sF5)
| ~ spl21_1748 ),
inference(avatar_component_clause,[],[f79658]) ).
fof(f79662,definition,
( spl21_1749
<=> e = sK0(sK0(sF14,sF20),sF5) ),
introduced(definition,[new_symbols(definition,[spl21_1749])],[avatar_definition]) ).
fof(f79663,plain,
( e != sK0(sK0(sF14,sF20),sF5)
| spl21_1749 ),
inference(avatar_component_clause,[],[f79662]) ).
fof(f79664,plain,
( e = sK0(sK0(sF14,sF20),sF5)
| ~ spl21_1749 ),
inference(avatar_component_clause,[],[f79662]) ).
fof(f79666,definition,
( spl21_1750
<=> sF3 = sK0(sK0(sF14,sF20),sF5) ),
introduced(definition,[new_symbols(definition,[spl21_1750])],[avatar_definition]) ).
fof(f79667,plain,
( sF3 != sK0(sK0(sF14,sF20),sF5)
| spl21_1750 ),
inference(avatar_component_clause,[],[f79666]) ).
fof(f79668,plain,
( sF3 = sK0(sK0(sF14,sF20),sF5)
| ~ spl21_1750 ),
inference(avatar_component_clause,[],[f79666]) ).
fof(f79693,definition,
( spl21_1756
<=> sF2 = sK0(sK0(sF14,sF20),sF3) ),
introduced(definition,[new_symbols(definition,[spl21_1756])],[avatar_definition]) ).
fof(f79695,plain,
( sF2 = sK0(sK0(sF14,sF20),sF3)
| ~ spl21_1756 ),
inference(avatar_component_clause,[],[f79693]) ).
fof(f79697,definition,
( spl21_1757
<=> e = sK0(sK0(sF14,sF20),sF3) ),
introduced(definition,[new_symbols(definition,[spl21_1757])],[avatar_definition]) ).
fof(f79699,plain,
( e = sK0(sK0(sF14,sF20),sF3)
| ~ spl21_1757 ),
inference(avatar_component_clause,[],[f79697]) ).
fof(f79701,definition,
( spl21_1758
<=> sF3 = sK0(sK0(sF14,sF20),sF3) ),
introduced(definition,[new_symbols(definition,[spl21_1758])],[avatar_definition]) ).
fof(f79703,plain,
( sF3 = sK0(sK0(sF14,sF20),sF3)
| ~ spl21_1758 ),
inference(avatar_component_clause,[],[f79701]) ).
fof(f79707,definition,
( spl21_1759
<=> subq(sK0(sF14,sF20),sF9) ),
introduced(definition,[new_symbols(definition,[spl21_1759])],[avatar_definition]) ).
fof(f79708,plain,
( ~ subq(sK0(sF14,sF20),sF9)
| spl21_1759 ),
inference(avatar_component_clause,[],[f79707]) ).
fof(f79712,definition,
( spl21_1760
<=> subq(sK0(sF14,sF20),sF5) ),
introduced(definition,[new_symbols(definition,[spl21_1760])],[avatar_definition]) ).
fof(f79713,plain,
( ~ subq(sK0(sF14,sF20),sF5)
| spl21_1760 ),
inference(avatar_component_clause,[],[f79712]) ).
fof(f79714,plain,
( subq(sK0(sF14,sF20),sF5)
| ~ spl21_1760 ),
inference(avatar_component_clause,[],[f79712]) ).
fof(f79720,plain,
( sF3 = sK0(sK0(sF14,sF20),sF3)
| e = sK0(sK0(sF14,sF20),sF3)
| sF2 = sK0(sK0(sF14,sF20),sF3)
| spl21_988 ),
inference(forward_subsumption_resolution,[],[f79544,f39986]) ).
fof(f79774,definition,
( spl21_1772
<=> sF2 = sK0(sK0(sF14,sF20),sF8) ),
introduced(definition,[new_symbols(definition,[spl21_1772])],[avatar_definition]) ).
fof(f79776,plain,
( sF2 = sK0(sK0(sF14,sF20),sF8)
| ~ spl21_1772 ),
inference(avatar_component_clause,[],[f79774]) ).
fof(f79778,definition,
( spl21_1773
<=> e = sK0(sK0(sF14,sF20),sF8) ),
introduced(definition,[new_symbols(definition,[spl21_1773])],[avatar_definition]) ).
fof(f79780,plain,
( e = sK0(sK0(sF14,sF20),sF8)
| ~ spl21_1773 ),
inference(avatar_component_clause,[],[f79778]) ).
fof(f79782,definition,
( spl21_1774
<=> sF3 = sK0(sK0(sF14,sF20),sF8) ),
introduced(definition,[new_symbols(definition,[spl21_1774])],[avatar_definition]) ).
fof(f79784,plain,
( sF3 = sK0(sK0(sF14,sF20),sF8)
| ~ spl21_1774 ),
inference(avatar_component_clause,[],[f79782]) ).
fof(f79785,plain,
( spl21_1772
| spl21_1773
| spl21_1774
| spl21_965 ),
inference(avatar_split_clause,[],[f79656,f39873,f79782,f79778,f79774]) ).
fof(f79787,plain,
( spl21_1756
| spl21_1757
| spl21_1758
| spl21_988 ),
inference(avatar_split_clause,[],[f79720,f39985,f79701,f79697,f79693]) ).
fof(f79803,plain,
( ~ mem(e,sF8)
| subq(sK0(sF14,sF20),sF8)
| ~ spl21_1773 ),
inference(superposition,[],[f43,f79780]) ).
fof(f79892,definition,
( spl21_1778
<=> ! [X0] :
( mem(e,X0)
| ~ subq(sK0(sF14,sF20),X0) ) ),
introduced(definition,[new_symbols(definition,[spl21_1778])],[avatar_definition]) ).
fof(f79893,plain,
( ! [X0] :
( ~ subq(sK0(sF14,sF20),X0)
| mem(e,X0) )
| ~ spl21_1778 ),
inference(avatar_component_clause,[],[f79892]) ).
fof(f79895,plain,
( subq(sK0(sF14,sF20),sF8)
| ~ spl21_28
| ~ spl21_1773 ),
inference(forward_subsumption_resolution,[],[f79803,f508]) ).
fof(f79897,definition,
( spl21_1779
<=> mem(e,sK0(sF14,sF20)) ),
introduced(definition,[new_symbols(definition,[spl21_1779])],[avatar_definition]) ).
fof(f79899,plain,
( mem(e,sK0(sF14,sF20))
| ~ spl21_1779 ),
inference(avatar_component_clause,[],[f79897]) ).
fof(f79917,plain,
( spl21_969
| ~ spl21_28
| ~ spl21_1773 ),
inference(avatar_split_clause,[],[f79895,f79778,f506,f39890]) ).
fof(f80076,plain,
( mem(sK0(sF14,sF20),sF15)
| ~ spl21_969 ),
inference(resolution,[],[f39892,f463]) ).
fof(f80087,plain,
( $false
| spl21_965
| ~ spl21_969 ),
inference(forward_subsumption_resolution,[],[f80076,f39874]) ).
fof(f80088,plain,
( spl21_965
| ~ spl21_969 ),
inference(avatar_contradiction_clause,[],[f80087]) ).
fof(f80457,plain,
( ~ mem(sF3,sF8)
| subq(sK0(sF14,sF20),sF8)
| ~ spl21_1774 ),
inference(superposition,[],[f43,f79784]) ).
fof(f80569,plain,
( subq(sK0(sF14,sF20),sF8)
| ~ spl21_1774 ),
inference(forward_subsumption_resolution,[],[f80457,f518]) ).
fof(f80611,plain,
( $false
| spl21_969
| ~ spl21_1774 ),
inference(forward_subsumption_resolution,[],[f80569,f39891]) ).
fof(f80612,plain,
( spl21_969
| ~ spl21_1774 ),
inference(avatar_contradiction_clause,[],[f80611]) ).
fof(f80780,plain,
( mem(sF2,sK0(sF14,sF20))
| subq(sK0(sF14,sF20),sF8)
| ~ spl21_1772 ),
inference(superposition,[],[f42,f79776]) ).
fof(f80864,plain,
( mem(sF2,sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772 ),
inference(forward_subsumption_resolution,[],[f80780,f39891]) ).
fof(f80874,plain,
( e = m(s(sF2),sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772 ),
inference(resolution,[],[f80864,f9133]) ).
fof(f80876,plain,
( e = m(sF3,sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772 ),
inference(forward_demodulation,[],[f80874,f67]) ).
fof(f80885,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF3)
| mem(X0,sK0(sF14,sF20)) )
| spl21_969
| ~ spl21_1772 ),
inference(superposition,[],[f53,f80876]) ).
fof(f80915,plain,
( ! [X0] :
( mem(X0,sK0(sF14,sF20))
| ~ mem(X0,sF3) )
| spl21_969
| ~ spl21_1772 ),
inference(forward_subsumption_resolution,[],[f80885,f45]) ).
fof(f80921,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK0(sF14,sF20)),sF3)
| subq(X0,sK0(sF14,sF20)) )
| spl21_969
| ~ spl21_1772 ),
inference(resolution,[],[f80915,f43]) ).
fof(f80935,plain,
( mem(e,sK0(sF14,sF20))
| subq(sK0(sF14,sF20),sF3)
| ~ spl21_1757 ),
inference(superposition,[],[f42,f79699]) ).
fof(f81022,plain,
( mem(e,sK0(sF14,sF20))
| spl21_1086
| ~ spl21_1757 ),
inference(forward_subsumption_resolution,[],[f80935,f44162]) ).
fof(f81033,plain,
( spl21_1779
| spl21_1086
| ~ spl21_1757 ),
inference(avatar_split_clause,[],[f81022,f79697,f44161,f79897]) ).
fof(f81048,plain,
( mem(sK0(sF14,sF20),sF8)
| ~ spl21_1086 ),
inference(resolution,[],[f44163,f462]) ).
fof(f81065,plain,
( $false
| spl21_988
| ~ spl21_1086 ),
inference(forward_subsumption_resolution,[],[f81048,f39986]) ).
fof(f81066,plain,
( spl21_988
| ~ spl21_1086 ),
inference(avatar_contradiction_clause,[],[f81065]) ).
fof(f81475,plain,
( subq(sF5,sK0(sF14,sF20))
| subq(sF5,sK0(sF14,sF20))
| sF3 = sK0(sF5,sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772 ),
inference(resolution,[],[f80921,f61459]) ).
fof(f81500,plain,
( subq(sF5,sK0(sF14,sF20))
| sF3 = sK0(sF5,sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772 ),
inference(duplicate_literal_removal,[],[f81475]) ).
fof(f81506,definition,
( spl21_1790
<=> sF3 = sK0(sF5,sK0(sF14,sF20)) ),
introduced(definition,[new_symbols(definition,[spl21_1790])],[avatar_definition]) ).
fof(f81508,plain,
( sF3 = sK0(sF5,sK0(sF14,sF20))
| ~ spl21_1790 ),
inference(avatar_component_clause,[],[f81506]) ).
fof(f81510,definition,
( spl21_1791
<=> subq(sF5,sK0(sF14,sF20)) ),
introduced(definition,[new_symbols(definition,[spl21_1791])],[avatar_definition]) ).
fof(f81511,plain,
( ~ subq(sF5,sK0(sF14,sF20))
| spl21_1791 ),
inference(avatar_component_clause,[],[f81510]) ).
fof(f81512,plain,
( subq(sF5,sK0(sF14,sF20))
| ~ spl21_1791 ),
inference(avatar_component_clause,[],[f81510]) ).
fof(f81513,plain,
( spl21_1790
| spl21_1791
| spl21_969
| ~ spl21_1772 ),
inference(avatar_split_clause,[],[f81500,f79774,f39890,f81510,f81506]) ).
fof(f81548,definition,
( spl21_1795
<=> sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF15) ),
introduced(definition,[new_symbols(definition,[spl21_1795])],[avatar_definition]) ).
fof(f81550,plain,
( sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF15)
| ~ spl21_1795 ),
inference(avatar_component_clause,[],[f81548]) ).
fof(f81559,plain,
spl21_1795,
inference(avatar_split_clause,[],[f69769,f81548]) ).
fof(f81611,plain,
( ! [X0] :
( mem(sK0(sF14,sF20),sF20)
| mem(sK0(sF14,sF20),X0) )
| ~ spl21_976 ),
inference(resolution,[],[f39925,f51043]) ).
fof(f81619,plain,
( ! [X0] : mem(sK0(sF14,sF20),X0)
| ~ spl21_976
| spl21_992 ),
inference(forward_subsumption_resolution,[],[f81611,f40025]) ).
fof(f81621,plain,
( spl21_1458
| ~ spl21_976
| spl21_992 ),
inference(avatar_split_clause,[],[f81619,f40023,f39923,f64535]) ).
fof(f81698,plain,
( ~ mem(sF3,sK0(sF14,sF20))
| subq(sF5,sK0(sF14,sF20))
| ~ spl21_1790 ),
inference(superposition,[],[f43,f81508]) ).
fof(f81931,plain,
( mem(e,m(sK0(sF14,sF20),e))
| ~ spl21_1778 ),
inference(resolution,[],[f79893,f1623]) ).
fof(f81943,plain,
( mem(e,sK0(sF14,sF20))
| ~ spl21_1778 ),
inference(forward_demodulation,[],[f81931,f14904]) ).
fof(f82306,definition,
( spl21_1801
<=> mem(sF5,p(sK0(sF14,sF20))) ),
introduced(definition,[new_symbols(definition,[spl21_1801])],[avatar_definition]) ).
fof(f82307,plain,
( mem(sF5,p(sK0(sF14,sF20)))
| ~ spl21_1801 ),
inference(avatar_component_clause,[],[f82306]) ).
fof(f82308,plain,
( ~ mem(sF5,p(sK0(sF14,sF20)))
| spl21_1801 ),
inference(avatar_component_clause,[],[f82306]) ).
fof(f82396,plain,
( ~ mem(sK0(sF14,sF20),sF15)
| subq(s(sK0(sF14,sF20)),sF15)
| ~ spl21_1795 ),
inference(superposition,[],[f43,f81550]) ).
fof(f83404,plain,
( subq(s(sK0(sF14,sF20)),sF15)
| ~ spl21_965
| ~ spl21_1795 ),
inference(forward_subsumption_resolution,[],[f82396,f39875]) ).
fof(f83427,plain,
( $false
| ~ spl21_965
| spl21_1206
| ~ spl21_1795 ),
inference(forward_subsumption_resolution,[],[f83404,f48390]) ).
fof(f83428,plain,
( ~ spl21_965
| spl21_1206
| ~ spl21_1795 ),
inference(avatar_contradiction_clause,[],[f83427]) ).
fof(f83456,plain,
( subq(sF14,sF20)
| ~ spl21_992 ),
inference(resolution,[],[f40024,f43]) ).
fof(f83463,plain,
( $false
| ~ spl21_992 ),
inference(forward_subsumption_resolution,[],[f83456,f102]) ).
fof(f83464,plain,
~ spl21_992,
inference(avatar_contradiction_clause,[],[f83463]) ).
fof(f83543,plain,
( subq(sF14,sF20)
| ~ spl21_1458 ),
inference(resolution,[],[f64536,f43]) ).
fof(f83733,plain,
( $false
| ~ spl21_1458 ),
inference(forward_subsumption_resolution,[],[f83543,f102]) ).
fof(f83734,plain,
~ spl21_1458,
inference(avatar_contradiction_clause,[],[f83733]) ).
fof(f83899,definition,
( spl21_1808
<=> sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF13) ),
introduced(definition,[new_symbols(definition,[spl21_1808])],[avatar_definition]) ).
fof(f83901,plain,
( sK0(sF14,sF20) = sK0(s(sK0(sF14,sF20)),sF13)
| ~ spl21_1808 ),
inference(avatar_component_clause,[],[f83899]) ).
fof(f83903,plain,
spl21_1808,
inference(avatar_split_clause,[],[f56629,f83899]) ).
fof(f83975,plain,
( subq(sF14,sF20)
| ~ spl21_975 ),
inference(resolution,[],[f39920,f412]) ).
fof(f83987,plain,
( $false
| ~ spl21_975 ),
inference(forward_subsumption_resolution,[],[f83975,f102]) ).
fof(f83988,plain,
~ spl21_975,
inference(avatar_contradiction_clause,[],[f83987]) ).
fof(f84216,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF3)
| mem(X0,sK0(sF14,sF20)) )
| spl21_969
| ~ spl21_1772 ),
inference(superposition,[],[f53,f80876]) ).
fof(f84246,plain,
( ! [X0] :
( mem(X0,sK0(sF14,sF20))
| ~ mem(X0,sF3) )
| spl21_969
| ~ spl21_1772 ),
inference(forward_subsumption_resolution,[],[f84216,f45]) ).
fof(f84253,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK0(sF14,sF20)),sF3)
| subq(X0,sK0(sF14,sF20)) )
| spl21_969
| ~ spl21_1772 ),
inference(resolution,[],[f84246,f43]) ).
fof(f84282,plain,
( ! [X0] :
( subq(u(sF3,X0),sK0(sF14,sF20))
| mem(sK0(u(sF3,X0),sK0(sF14,sF20)),X0)
| subq(u(sF3,X0),sK0(sF14,sF20)) )
| spl21_969
| ~ spl21_1772 ),
inference(resolution,[],[f84253,f138]) ).
fof(f84305,plain,
( ! [X0] :
( mem(sK0(u(sF3,X0),sK0(sF14,sF20)),X0)
| subq(u(sF3,X0),sK0(sF14,sF20)) )
| spl21_969
| ~ spl21_1772 ),
inference(duplicate_literal_removal,[],[f84282]) ).
fof(f84466,plain,
( spl21_1779
| ~ spl21_1778 ),
inference(avatar_split_clause,[],[f81943,f79892,f79897]) ).
fof(f84474,plain,
( e = m(s(e),sK0(sF14,sF20))
| ~ spl21_1779 ),
inference(resolution,[],[f79899,f9133]) ).
fof(f84476,plain,
( e = m(sF1,sK0(sF14,sF20))
| ~ spl21_1779 ),
inference(forward_demodulation,[],[f84474,f63]) ).
fof(f84477,plain,
( e = m(sF2,sK0(sF14,sF20))
| ~ spl21_1779 ),
inference(forward_demodulation,[],[f84476,f4306]) ).
fof(f84570,plain,
( mem(sK0(sF14,sF20),sF2)
| subq(s(sK0(sF14,sF20)),sF13)
| ~ subq(s(sK0(sF14,sF20)),sF1)
| ~ spl21_1808 ),
inference(superposition,[],[f813,f83901]) ).
fof(f84658,plain,
( subq(s(sK0(sF14,sF20)),sF13)
| ~ subq(s(sK0(sF14,sF20)),sF1)
| spl21_961
| ~ spl21_1808 ),
inference(forward_subsumption_resolution,[],[f84570,f39856]) ).
fof(f84659,plain,
( ~ subq(s(sK0(sF14,sF20)),sF1)
| spl21_961
| spl21_1207
| ~ spl21_1808 ),
inference(forward_subsumption_resolution,[],[f84658,f48395]) ).
fof(f84660,plain,
( ~ subq(s(sK0(sF14,sF20)),sF2)
| spl21_961
| spl21_1207
| ~ spl21_1808 ),
inference(forward_demodulation,[],[f84659,f4306]) ).
fof(f85163,plain,
( ~ mem(sF2,sF3)
| subq(sK0(sF14,sF20),sF3)
| ~ spl21_1756 ),
inference(superposition,[],[f43,f79695]) ).
fof(f85245,plain,
( subq(sK0(sF14,sF20),sF3)
| ~ spl21_1756 ),
inference(forward_subsumption_resolution,[],[f85163,f106]) ).
fof(f85247,plain,
( $false
| spl21_1086
| ~ spl21_1756 ),
inference(forward_subsumption_resolution,[],[f85245,f44162]) ).
fof(f85248,plain,
( spl21_1086
| ~ spl21_1756 ),
inference(avatar_contradiction_clause,[],[f85247]) ).
fof(f85383,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF2)
| mem(X0,sK0(sF14,sF20)) )
| ~ spl21_1779 ),
inference(superposition,[],[f53,f84477]) ).
fof(f85413,plain,
( ! [X0] :
( mem(X0,sK0(sF14,sF20))
| ~ mem(X0,sF2) )
| ~ spl21_1779 ),
inference(forward_subsumption_resolution,[],[f85383,f45]) ).
fof(f85418,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK0(sF14,sF20)),sF2)
| subq(X0,sK0(sF14,sF20)) )
| ~ spl21_1779 ),
inference(resolution,[],[f85413,f43]) ).
fof(f85800,plain,
( ~ mem(sF2,sF5)
| subq(sK0(sF14,sF20),sF5)
| ~ spl21_1748 ),
inference(superposition,[],[f43,f79660]) ).
fof(f85878,plain,
( subq(sK0(sF14,sF20),sF5)
| ~ spl21_1748 ),
inference(forward_subsumption_resolution,[],[f85800,f194]) ).
fof(f85888,plain,
( ! [X0] :
( mem(e,X0)
| ~ subq(sK0(sF14,sF20),X0)
| subq(sK0(sF14,sF20),sF5) )
| ~ spl21_1749 ),
inference(superposition,[],[f753,f79664]) ).
fof(f86224,plain,
( ~ subq(sF5,sK0(sF14,sF20))
| spl21_1801 ),
inference(resolution,[],[f82308,f57]) ).
fof(f89484,plain,
( subq(u(sF3,sF6),sK0(sF14,sF20))
| mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF5)
| mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF2)
| spl21_969
| ~ spl21_1772 ),
inference(resolution,[],[f84305,f155]) ).
fof(f89548,plain,
( mem(sK0(sF9,sK0(sF14,sF20)),sF2)
| subq(sF9,sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772 ),
inference(superposition,[],[f84305,f23931]) ).
fof(f89563,plain,
( subq(sF9,sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772
| ~ spl21_1779 ),
inference(forward_subsumption_resolution,[],[f89548,f85418]) ).
fof(f89906,plain,
( subq(u(sF3,sF6),sK0(sF14,sF20))
| mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF5)
| spl21_969
| ~ spl21_1772
| ~ spl21_1779 ),
inference(forward_subsumption_resolution,[],[f89484,f85418]) ).
fof(f90031,definition,
( spl21_2028
<=> mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF5) ),
introduced(definition,[new_symbols(definition,[spl21_2028])],[avatar_definition]) ).
fof(f90033,plain,
( mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF5)
| ~ spl21_2028 ),
inference(avatar_component_clause,[],[f90031]) ).
fof(f90035,definition,
( spl21_2029
<=> subq(u(sF3,sF6),sK0(sF14,sF20)) ),
introduced(definition,[new_symbols(definition,[spl21_2029])],[avatar_definition]) ).
fof(f90036,plain,
( ~ subq(u(sF3,sF6),sK0(sF14,sF20))
| spl21_2029 ),
inference(avatar_component_clause,[],[f90035]) ).
fof(f90037,plain,
( subq(u(sF3,sF6),sK0(sF14,sF20))
| ~ spl21_2029 ),
inference(avatar_component_clause,[],[f90035]) ).
fof(f90038,plain,
( spl21_2028
| spl21_2029
| spl21_969
| ~ spl21_1772
| ~ spl21_1779 ),
inference(avatar_split_clause,[],[f89906,f79897,f79774,f39890,f90035,f90031]) ).
fof(f90098,plain,
( sF9 = sK0(sF14,sF20)
| ~ subq(sK0(sF14,sF20),sF9)
| spl21_969
| ~ spl21_1772
| ~ spl21_1779 ),
inference(resolution,[],[f89563,f44]) ).
fof(f90099,plain,
( ~ spl21_1759
| spl21_1085
| spl21_969
| ~ spl21_1772
| ~ spl21_1779 ),
inference(avatar_split_clause,[],[f90098,f79897,f79774,f39890,f44154,f79707]) ).
fof(f90100,plain,
( sF3 = sK0(sK0(sF14,sF20),sF9)
| e = sK0(sK0(sF14,sF20),sF9)
| sF2 = sK0(sK0(sF14,sF20),sF9)
| spl21_1759 ),
inference(resolution,[],[f79708,f79490]) ).
fof(f90111,definition,
( spl21_2030
<=> sF2 = sK0(sK0(sF14,sF20),sF9) ),
introduced(definition,[new_symbols(definition,[spl21_2030])],[avatar_definition]) ).
fof(f90113,plain,
( sF2 = sK0(sK0(sF14,sF20),sF9)
| ~ spl21_2030 ),
inference(avatar_component_clause,[],[f90111]) ).
fof(f90115,definition,
( spl21_2031
<=> e = sK0(sK0(sF14,sF20),sF9) ),
introduced(definition,[new_symbols(definition,[spl21_2031])],[avatar_definition]) ).
fof(f90117,plain,
( e = sK0(sK0(sF14,sF20),sF9)
| ~ spl21_2031 ),
inference(avatar_component_clause,[],[f90115]) ).
fof(f90119,definition,
( spl21_2032
<=> sF3 = sK0(sK0(sF14,sF20),sF9) ),
introduced(definition,[new_symbols(definition,[spl21_2032])],[avatar_definition]) ).
fof(f90121,plain,
( sF3 = sK0(sK0(sF14,sF20),sF9)
| ~ spl21_2032 ),
inference(avatar_component_clause,[],[f90119]) ).
fof(f90123,plain,
( spl21_2030
| spl21_2031
| spl21_2032
| spl21_1759 ),
inference(avatar_split_clause,[],[f90100,f79707,f90119,f90115,f90111]) ).
fof(f90125,plain,
( ~ mem(sF2,sF9)
| subq(sK0(sF14,sF20),sF9)
| ~ spl21_2030 ),
inference(superposition,[],[f43,f90113]) ).
fof(f90204,plain,
( subq(sK0(sF14,sF20),sF9)
| ~ spl21_2030 ),
inference(forward_subsumption_resolution,[],[f90125,f211]) ).
fof(f90206,plain,
( $false
| spl21_1759
| ~ spl21_2030 ),
inference(forward_subsumption_resolution,[],[f90204,f79708]) ).
fof(f90207,plain,
( spl21_1759
| ~ spl21_2030 ),
inference(avatar_contradiction_clause,[],[f90206]) ).
fof(f90210,plain,
( ~ mem(e,sF9)
| subq(sK0(sF14,sF20),sF9)
| ~ spl21_2031 ),
inference(superposition,[],[f43,f90117]) ).
fof(f90286,plain,
( subq(sK0(sF14,sF20),sF9)
| ~ spl21_2031 ),
inference(forward_subsumption_resolution,[],[f90210,f291]) ).
fof(f90287,plain,
( $false
| spl21_1759
| ~ spl21_2031 ),
inference(forward_subsumption_resolution,[],[f90286,f79708]) ).
fof(f90288,plain,
( spl21_1759
| ~ spl21_2031 ),
inference(avatar_contradiction_clause,[],[f90287]) ).
fof(f90289,plain,
( mem(sF3,sK0(sF14,sF20))
| subq(sK0(sF14,sF20),sF9)
| ~ spl21_2032 ),
inference(superposition,[],[f42,f90121]) ).
fof(f90391,plain,
( subq(sK0(sF14,sF20),sF9)
| spl21_1216
| ~ spl21_2032 ),
inference(forward_subsumption_resolution,[],[f90289,f48810]) ).
fof(f90421,plain,
( $false
| spl21_1216
| spl21_1759
| ~ spl21_2032 ),
inference(forward_subsumption_resolution,[],[f90391,f79708]) ).
fof(f90422,plain,
( spl21_1216
| spl21_1759
| ~ spl21_2032 ),
inference(avatar_contradiction_clause,[],[f90421]) ).
fof(f90500,plain,
( ~ mem(sF9,sF11)
| spl21_958
| ~ spl21_1085 ),
inference(superposition,[],[f39843,f44156]) ).
fof(f90782,plain,
( $false
| spl21_958
| ~ spl21_1085 ),
inference(forward_subsumption_resolution,[],[f90500,f290]) ).
fof(f90783,plain,
( spl21_958
| ~ spl21_1085 ),
inference(avatar_contradiction_clause,[],[f90782]) ).
fof(f90856,plain,
( ! [X0] :
( mem(e,X0)
| ~ subq(sK0(sF14,sF20),X0) )
| ~ spl21_1749
| spl21_1760 ),
inference(forward_subsumption_resolution,[],[f85888,f79713]) ).
fof(f90892,plain,
( spl21_1778
| ~ spl21_1749
| spl21_1760 ),
inference(avatar_split_clause,[],[f90856,f79712,f79662,f79892]) ).
fof(f91162,plain,
( mem(sF3,sK0(sF14,sF20))
| subq(sK0(sF14,sF20),sF3)
| ~ spl21_1758 ),
inference(superposition,[],[f42,f79703]) ).
fof(f91270,plain,
( subq(sK0(sF14,sF20),sF3)
| spl21_1216
| ~ spl21_1758 ),
inference(forward_subsumption_resolution,[],[f91162,f48810]) ).
fof(f91306,plain,
( $false
| spl21_1086
| spl21_1216
| ~ spl21_1758 ),
inference(forward_subsumption_resolution,[],[f91270,f44162]) ).
fof(f91307,plain,
( spl21_1086
| spl21_1216
| ~ spl21_1758 ),
inference(avatar_contradiction_clause,[],[f91306]) ).
fof(f91423,plain,
~ mem(sK0(sF14,sF20),sF11),
inference(forward_subsumption_resolution,[],[f44115,f104]) ).
fof(f91449,plain,
( $false
| ~ spl21_958 ),
inference(forward_subsumption_resolution,[],[f91423,f39844]) ).
fof(f91450,plain,
~ spl21_958,
inference(avatar_contradiction_clause,[],[f91449]) ).
fof(f91515,plain,
( ~ mem(sF3,sK0(sF14,sF20))
| ~ spl21_1790
| spl21_1791 ),
inference(forward_subsumption_resolution,[],[f81698,f81511]) ).
fof(f91771,plain,
( $false
| ~ spl21_1216
| ~ spl21_1790
| spl21_1791 ),
inference(forward_subsumption_resolution,[],[f91515,f48811]) ).
fof(f91772,plain,
( ~ spl21_1216
| ~ spl21_1790
| spl21_1791 ),
inference(avatar_contradiction_clause,[],[f91771]) ).
fof(f91828,plain,
( $false
| ~ spl21_1791
| spl21_1801 ),
inference(forward_subsumption_resolution,[],[f86224,f81512]) ).
fof(f91829,plain,
( ~ spl21_1791
| spl21_1801 ),
inference(avatar_contradiction_clause,[],[f91828]) ).
fof(f91836,plain,
( e = m(s(sF3),sK0(sF14,sF20))
| ~ spl21_1216 ),
inference(resolution,[],[f48811,f9133]) ).
fof(f91838,plain,
( e = m(sF4,sK0(sF14,sF20))
| ~ spl21_1216 ),
inference(forward_demodulation,[],[f91836,f69]) ).
fof(f91873,plain,
( sF5 = sK0(sF14,sF20)
| ~ subq(sK0(sF14,sF20),sF5)
| ~ spl21_1791 ),
inference(resolution,[],[f81512,f44]) ).
fof(f92030,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF4)
| mem(X0,sK0(sF14,sF20)) )
| ~ spl21_1216 ),
inference(superposition,[],[f53,f91838]) ).
fof(f92060,plain,
( ! [X0] :
( mem(X0,sK0(sF14,sF20))
| ~ mem(X0,sF4) )
| ~ spl21_1216 ),
inference(forward_subsumption_resolution,[],[f92030,f45]) ).
fof(f92065,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK0(sF14,sF20)),sF4)
| subq(X0,sK0(sF14,sF20)) )
| ~ spl21_1216 ),
inference(resolution,[],[f92060,f43]) ).
fof(f93747,plain,
( ~ mem(sF3,sF5)
| subq(sK0(sF14,sF20),sF5)
| ~ spl21_1750 ),
inference(superposition,[],[f43,f79668]) ).
fof(f93820,plain,
( subq(sK0(sF14,sF20),sF5)
| ~ spl21_1750 ),
inference(forward_subsumption_resolution,[],[f93747,f180]) ).
fof(f93822,plain,
( $false
| ~ spl21_1750
| spl21_1760 ),
inference(forward_subsumption_resolution,[],[f93820,f79713]) ).
fof(f93823,plain,
( ~ spl21_1750
| spl21_1760 ),
inference(avatar_contradiction_clause,[],[f93822]) ).
fof(f93911,plain,
( e = m(s(sF5),p(sK0(sF14,sF20)))
| ~ spl21_1801 ),
inference(resolution,[],[f82307,f9133]) ).
fof(f93913,plain,
( e = m(sF16,p(sK0(sF14,sF20)))
| ~ spl21_1801 ),
inference(forward_demodulation,[],[f93911,f93]) ).
fof(f95139,plain,
( mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF4)
| mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF3)
| ~ spl21_2028 ),
inference(resolution,[],[f90033,f143]) ).
fof(f95144,definition,
( spl21_2082
<=> mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF3) ),
introduced(definition,[new_symbols(definition,[spl21_2082])],[avatar_definition]) ).
fof(f95146,plain,
( mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF3)
| ~ spl21_2082 ),
inference(avatar_component_clause,[],[f95144]) ).
fof(f95148,definition,
( spl21_2083
<=> mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF4) ),
introduced(definition,[new_symbols(definition,[spl21_2083])],[avatar_definition]) ).
fof(f95150,plain,
( mem(sK0(u(sF3,sF6),sK0(sF14,sF20)),sF4)
| ~ spl21_2083 ),
inference(avatar_component_clause,[],[f95148]) ).
fof(f95151,plain,
( spl21_2082
| spl21_2083
| ~ spl21_2028 ),
inference(avatar_split_clause,[],[f95139,f90031,f95148,f95144]) ).
fof(f95156,plain,
( subq(u(sF3,sF6),sK0(sF14,sF20))
| ~ spl21_1216
| ~ spl21_2083 ),
inference(resolution,[],[f95150,f92065]) ).
fof(f95184,plain,
( spl21_2029
| ~ spl21_1216
| ~ spl21_2083 ),
inference(avatar_split_clause,[],[f95156,f95148,f48809,f90035]) ).
fof(f95187,plain,
( ! [X0] :
( mem(X0,sK0(sF14,sF20))
| ~ mem(X0,sF6) )
| ~ spl21_2029 ),
inference(resolution,[],[f90037,f739]) ).
fof(f95202,plain,
( ! [X0] :
( ~ mem(sK0(X0,sK0(sF14,sF20)),sF6)
| subq(X0,sK0(sF14,sF20)) )
| ~ spl21_2029 ),
inference(resolution,[],[f95187,f43]) ).
fof(f95453,plain,
( mem(sK0(sF14,sF20),sF19)
| ~ spl21_961 ),
inference(resolution,[],[f39857,f13145]) ).
fof(f95468,plain,
( $false
| ~ spl21_961
| spl21_975 ),
inference(forward_subsumption_resolution,[],[f95453,f39919]) ).
fof(f95469,plain,
( ~ spl21_961
| spl21_975 ),
inference(avatar_contradiction_clause,[],[f95468]) ).
fof(f95500,plain,
( ~ spl21_1041
| spl21_961
| spl21_1207
| ~ spl21_1808 ),
inference(avatar_split_clause,[],[f84660,f83899,f48394,f39855,f42952]) ).
fof(f96077,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,sF16)
| mem(X0,p(sK0(sF14,sF20))) )
| ~ spl21_1801 ),
inference(superposition,[],[f53,f93913]) ).
fof(f96107,plain,
( ! [X0] :
( mem(X0,p(sK0(sF14,sF20)))
| ~ mem(X0,sF16) )
| ~ spl21_1801 ),
inference(forward_subsumption_resolution,[],[f96077,f45]) ).
fof(f96109,plain,
( ! [X0] :
( subq(X0,sK0(sF14,sF20))
| ~ mem(X0,sF16) )
| ~ spl21_1801 ),
inference(resolution,[],[f96107,f56]) ).
fof(f96128,plain,
( ! [X0] :
( ~ subq(sK0(sF14,sF20),X0)
| sK0(sF14,sF20) = X0
| ~ mem(X0,sF16) )
| ~ spl21_1801 ),
inference(resolution,[],[f96109,f44]) ).
fof(f96300,plain,
( ! [X0] :
( sK0(sF14,sF20) = X0
| ~ mem(X0,sF16)
| sF3 = sK0(sK0(sF14,sF20),X0)
| e = sK0(sK0(sF14,sF20),X0)
| sF2 = sK0(sK0(sF14,sF20),X0) )
| ~ spl21_1801 ),
inference(resolution,[],[f96128,f79490]) ).
fof(f96340,definition,
( spl21_2108
<=> ! [X0] :
( sK0(sF14,sF20) = X0
| sF2 = sK0(sK0(sF14,sF20),X0)
| e = sK0(sK0(sF14,sF20),X0)
| sF3 = sK0(sK0(sF14,sF20),X0)
| ~ mem(X0,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl21_2108])],[avatar_definition]) ).
fof(f96341,plain,
( ! [X0] :
( ~ mem(X0,sF16)
| sF2 = sK0(sK0(sF14,sF20),X0)
| e = sK0(sK0(sF14,sF20),X0)
| sF3 = sK0(sK0(sF14,sF20),X0)
| sK0(sF14,sF20) = X0 )
| ~ spl21_2108 ),
inference(avatar_component_clause,[],[f96340]) ).
fof(f96343,plain,
( spl21_2108
| ~ spl21_1801 ),
inference(avatar_split_clause,[],[f96300,f82306,f96340]) ).
fof(f96425,plain,
( sF2 = sK0(sK0(sF14,sF20),sF5)
| e = sK0(sK0(sF14,sF20),sF5)
| sF3 = sK0(sK0(sF14,sF20),sF5)
| sF5 = sK0(sF14,sF20)
| ~ spl21_2108 ),
inference(resolution,[],[f96341,f108]) ).
fof(f96642,plain,
( subq(u(sF6,e),sK0(sF14,sF20))
| subq(u(sF6,e),sK0(sF14,sF20))
| ~ spl21_2029 ),
inference(resolution,[],[f95202,f1044]) ).
fof(f96670,plain,
( subq(u(sF6,e),sK0(sF14,sF20))
| ~ spl21_2029 ),
inference(duplicate_literal_removal,[],[f96642]) ).
fof(f96681,plain,
( subq(sF6,sK0(sF14,sF20))
| ~ spl21_2029 ),
inference(forward_demodulation,[],[f96670,f6084]) ).
fof(f96684,plain,
( $false
| spl21_1002
| ~ spl21_2029 ),
inference(forward_subsumption_resolution,[],[f96681,f41396]) ).
fof(f96685,plain,
( spl21_1002
| ~ spl21_2029 ),
inference(avatar_contradiction_clause,[],[f96684]) ).
fof(f96888,plain,
( ~ mem(sF6,sF19)
| subq(sF14,sF20)
| ~ spl21_966 ),
inference(superposition,[],[f412,f39880]) ).
fof(f96961,plain,
( subq(sF14,sF20)
| ~ spl21_966 ),
inference(forward_subsumption_resolution,[],[f96888,f238]) ).
fof(f97019,plain,
( $false
| ~ spl21_966 ),
inference(forward_subsumption_resolution,[],[f96961,f102]) ).
fof(f97020,plain,
~ spl21_966,
inference(avatar_contradiction_clause,[],[f97019]) ).
fof(f97154,plain,
( subq(u(sF3,sF6),sK0(sF14,sF20))
| spl21_969
| ~ spl21_1772
| ~ spl21_2082 ),
inference(resolution,[],[f95146,f84253]) ).
fof(f97182,plain,
( $false
| spl21_969
| ~ spl21_1772
| spl21_2029
| ~ spl21_2082 ),
inference(forward_subsumption_resolution,[],[f97154,f90036]) ).
fof(f97183,plain,
( spl21_969
| ~ spl21_1772
| spl21_2029
| ~ spl21_2082 ),
inference(avatar_contradiction_clause,[],[f97182]) ).
fof(f97185,plain,
( spl21_1760
| ~ spl21_1748 ),
inference(avatar_split_clause,[],[f85878,f79658,f79712]) ).
fof(f97220,plain,
( sF5 = sK0(sF14,sF20)
| ~ spl21_1760
| ~ spl21_1791 ),
inference(forward_subsumption_resolution,[],[f91873,f79714]) ).
fof(f97243,plain,
( spl21_967
| ~ spl21_1760
| ~ spl21_1791 ),
inference(avatar_split_clause,[],[f97220,f81510,f79712,f39882]) ).
fof(f97435,plain,
( ~ mem(sF5,sF19)
| subq(sF14,sF20)
| ~ spl21_967 ),
inference(superposition,[],[f412,f39884]) ).
fof(f97514,plain,
( subq(sF14,sF20)
| ~ spl21_967 ),
inference(forward_subsumption_resolution,[],[f97435,f348]) ).
fof(f97569,plain,
( $false
| ~ spl21_967 ),
inference(forward_subsumption_resolution,[],[f97514,f102]) ).
fof(f97570,plain,
~ spl21_967,
inference(avatar_contradiction_clause,[],[f97569]) ).
fof(f97589,plain,
( e = sK0(sK0(sF14,sF20),sF5)
| sF3 = sK0(sK0(sF14,sF20),sF5)
| sF5 = sK0(sF14,sF20)
| spl21_1748
| ~ spl21_2108 ),
inference(forward_subsumption_resolution,[],[f96425,f79659]) ).
fof(f97597,plain,
( sF3 = sK0(sK0(sF14,sF20),sF5)
| sF5 = sK0(sF14,sF20)
| spl21_1748
| spl21_1749
| ~ spl21_2108 ),
inference(forward_subsumption_resolution,[],[f97589,f79663]) ).
fof(f97606,plain,
( sF5 = sK0(sF14,sF20)
| spl21_1748
| spl21_1749
| spl21_1750
| ~ spl21_2108 ),
inference(forward_subsumption_resolution,[],[f97597,f79667]) ).
fof(f97613,plain,
( $false
| spl21_967
| spl21_1748
| spl21_1749
| spl21_1750
| ~ spl21_2108 ),
inference(forward_subsumption_resolution,[],[f97606,f39883]) ).
fof(f97614,plain,
( spl21_967
| spl21_1748
| spl21_1749
| spl21_1750
| ~ spl21_2108 ),
inference(avatar_contradiction_clause,[],[f97613]) ).
cnf(s13,plain,
spl21_28,
inference(sat_conversion,[],[f520]) ).
cnf(s2536,plain,
( spl21_966
| ~ spl21_1002 ),
inference(sat_conversion,[],[f41397]) ).
cnf(s2671,plain,
( spl21_958
| ~ spl21_988 ),
inference(sat_conversion,[],[f44882]) ).
cnf(s3062,plain,
( spl21_976
| spl21_992
| spl21_1041
| ~ spl21_1206 ),
inference(sat_conversion,[],[f53066]) ).
cnf(s3170,plain,
( spl21_992
| ~ spl21_1207 ),
inference(sat_conversion,[],[f56238]) ).
cnf(s3923,plain,
( spl21_965
| spl21_1772
| spl21_1773
| spl21_1774 ),
inference(sat_conversion,[],[f79785]) ).
cnf(s3925,plain,
( spl21_988
| spl21_1756
| spl21_1757
| spl21_1758 ),
inference(sat_conversion,[],[f79787]) ).
cnf(s3936,plain,
( ~ spl21_28
| spl21_969
| ~ spl21_1773 ),
inference(sat_conversion,[],[f79917]) ).
cnf(s3975,plain,
( spl21_965
| ~ spl21_969 ),
inference(sat_conversion,[],[f80088]) ).
cnf(s4039,plain,
( spl21_969
| ~ spl21_1774 ),
inference(sat_conversion,[],[f80612]) ).
cnf(s4081,plain,
( spl21_1086
| ~ spl21_1757
| spl21_1779 ),
inference(sat_conversion,[],[f81033]) ).
cnf(s4095,plain,
( spl21_988
| ~ spl21_1086 ),
inference(sat_conversion,[],[f81066]) ).
cnf(s4135,plain,
( spl21_969
| ~ spl21_1772
| spl21_1790
| spl21_1791 ),
inference(sat_conversion,[],[f81513]) ).
cnf(s4145,plain,
spl21_1795,
inference(sat_conversion,[],[f81559]) ).
cnf(s4173,plain,
( ~ spl21_976
| spl21_992
| spl21_1458 ),
inference(sat_conversion,[],[f81621]) ).
cnf(s4247,plain,
( ~ spl21_965
| spl21_1206
| ~ spl21_1795 ),
inference(sat_conversion,[],[f83428]) ).
cnf(s4259,plain,
~ spl21_992,
inference(sat_conversion,[],[f83464]) ).
cnf(s4291,plain,
~ spl21_1458,
inference(sat_conversion,[],[f83734]) ).
cnf(s4332,plain,
spl21_1808,
inference(sat_conversion,[],[f83903]) ).
cnf(s4351,plain,
~ spl21_975,
inference(sat_conversion,[],[f83988]) ).
cnf(s4361,plain,
( ~ spl21_1778
| spl21_1779 ),
inference(sat_conversion,[],[f84466]) ).
cnf(s4389,plain,
( spl21_1086
| ~ spl21_1756 ),
inference(sat_conversion,[],[f85248]) ).
cnf(s4577,plain,
( spl21_969
| ~ spl21_1772
| ~ spl21_1779
| spl21_2028
| spl21_2029 ),
inference(sat_conversion,[],[f90038]) ).
cnf(s4578,plain,
( spl21_969
| spl21_1085
| ~ spl21_1759
| ~ spl21_1772
| ~ spl21_1779 ),
inference(sat_conversion,[],[f90099]) ).
cnf(s4580,plain,
( spl21_1759
| spl21_2030
| spl21_2031
| spl21_2032 ),
inference(sat_conversion,[],[f90123]) ).
cnf(s4581,plain,
( spl21_1759
| ~ spl21_2030 ),
inference(sat_conversion,[],[f90207]) ).
cnf(s4582,plain,
( spl21_1759
| ~ spl21_2031 ),
inference(sat_conversion,[],[f90288]) ).
cnf(s4584,plain,
( spl21_1216
| spl21_1759
| ~ spl21_2032 ),
inference(sat_conversion,[],[f90422]) ).
cnf(s4611,plain,
( spl21_958
| ~ spl21_1085 ),
inference(sat_conversion,[],[f90783]) ).
cnf(s4627,plain,
( ~ spl21_1749
| spl21_1760
| spl21_1778 ),
inference(sat_conversion,[],[f90892]) ).
cnf(s4642,plain,
( spl21_1086
| spl21_1216
| ~ spl21_1758 ),
inference(sat_conversion,[],[f91307]) ).
cnf(s4669,plain,
~ spl21_958,
inference(sat_conversion,[],[f91450]) ).
cnf(s4738,plain,
( ~ spl21_1216
| ~ spl21_1790
| spl21_1791 ),
inference(sat_conversion,[],[f91772]) ).
cnf(s4754,plain,
( ~ spl21_1791
| spl21_1801 ),
inference(sat_conversion,[],[f91829]) ).
cnf(s4786,plain,
( ~ spl21_1750
| spl21_1760 ),
inference(sat_conversion,[],[f93823]) ).
cnf(s4819,plain,
( ~ spl21_2028
| spl21_2082
| spl21_2083 ),
inference(sat_conversion,[],[f95151]) ).
cnf(s4823,plain,
( ~ spl21_1216
| spl21_2029
| ~ spl21_2083 ),
inference(sat_conversion,[],[f95184]) ).
cnf(s4874,plain,
( ~ spl21_961
| spl21_975 ),
inference(sat_conversion,[],[f95469]) ).
cnf(s4897,plain,
( spl21_961
| ~ spl21_1041
| spl21_1207
| ~ spl21_1808 ),
inference(sat_conversion,[],[f95500]) ).
cnf(s4938,plain,
( ~ spl21_1801
| spl21_2108 ),
inference(sat_conversion,[],[f96343]) ).
cnf(s4942,plain,
( spl21_1002
| ~ spl21_2029 ),
inference(sat_conversion,[],[f96685]) ).
cnf(s4951,plain,
~ spl21_966,
inference(sat_conversion,[],[f97020]) ).
cnf(s4962,plain,
( spl21_969
| ~ spl21_1772
| spl21_2029
| ~ spl21_2082 ),
inference(sat_conversion,[],[f97183]) ).
cnf(s4963,plain,
( ~ spl21_1748
| spl21_1760 ),
inference(sat_conversion,[],[f97185]) ).
cnf(s4973,plain,
( spl21_967
| ~ spl21_1760
| ~ spl21_1791 ),
inference(sat_conversion,[],[f97243]) ).
cnf(s4985,plain,
~ spl21_967,
inference(sat_conversion,[],[f97570]) ).
cnf(s4988,plain,
( spl21_967
| spl21_1748
| spl21_1749
| spl21_1750
| ~ spl21_2108 ),
inference(sat_conversion,[],[f97614]) ).
cnf(s4994,plain,
( ~ spl21_1760
| ~ spl21_1791 ),
inference(rat,[],[s4973,s4985]) ).
cnf(s4997,plain,
~ spl21_1085,
inference(rat,[],[s4611,s4669]) ).
cnf(s4998,plain,
( spl21_969
| ~ spl21_1759
| ~ spl21_1772
| ~ spl21_1779 ),
inference(rat,[],[s4578,s4997]) ).
cnf(s5000,plain,
~ spl21_961,
inference(rat,[],[s4874,s4351]) ).
cnf(s5026,plain,
~ spl21_976,
inference(rat,[],[s4173,s4291,s4259]) ).
cnf(s5039,plain,
~ spl21_1207,
inference(rat,[],[s3170,s4259]) ).
cnf(s5040,plain,
~ spl21_1041,
inference(rat,[],[s4897,s4332,s5000,s5039]) ).
cnf(s5042,plain,
~ spl21_1206,
inference(rat,[],[s3062,s5040,s4259,s5026]) ).
cnf(s5043,plain,
~ spl21_965,
inference(rat,[],[s4247,s4145,s5042]) ).
cnf(s5044,plain,
~ spl21_969,
inference(rat,[],[s3975,s5043]) ).
cnf(s5046,plain,
~ spl21_1774,
inference(rat,[],[s4039,s5044]) ).
cnf(s5053,plain,
~ spl21_988,
inference(rat,[],[s2671,s4669]) ).
cnf(s5054,plain,
~ spl21_1086,
inference(rat,[],[s4095,s5053]) ).
cnf(s5055,plain,
~ spl21_1756,
inference(rat,[],[s4389,s5054]) ).
cnf(s5070,plain,
~ spl21_1002,
inference(rat,[],[s2536,s4951]) ).
cnf(s5072,plain,
~ spl21_2029,
inference(rat,[],[s4942,s5070]) ).
cnf(s5467,plain,
~ spl21_1773,
inference(rat,[],[s3936,s5044,s13]) ).
cnf(s5469,plain,
spl21_1772,
inference(rat,[],[s3923,s5046,s5043,s5467]) ).
cnf(s5475,plain,
~ spl21_2082,
inference(rat,[],[s4962,s5072,s5044,s5469]) ).
cnf(s5576,plain,
( spl21_1791
| ~ spl21_1216 ),
inference(rat,[],[s4738,s4135,s5044,s5469]) ).
cnf(s5577,plain,
~ spl21_1216,
inference(rat,[],[s4963,s4988,s4938,s4627,s4786,s4754,s4994,s5576,s4361,s4577,s4819,s4823,s4985,s5044,s5469,s5072,s5475]) ).
cnf(s5579,plain,
~ spl21_1758,
inference(rat,[],[s4642,s5054,s5577]) ).
cnf(s5581,plain,
spl21_1757,
inference(rat,[],[s3925,s5055,s5053,s5579]) ).
cnf(s5583,plain,
spl21_1779,
inference(rat,[],[s4081,s5054,s5581]) ).
cnf(s5598,plain,
~ spl21_1759,
inference(rat,[],[s4998,s5469,s5044,s5583]) ).
cnf(s5619,plain,
~ spl21_2032,
inference(rat,[],[s4584,s5577,s5598]) ).
cnf(s5620,plain,
~ spl21_2031,
inference(rat,[],[s4582,s5598]) ).
cnf(s5621,plain,
~ spl21_2030,
inference(rat,[],[s4581,s5598]) ).
cnf(s5625,plain,
$false,
inference(rat,[],[s4580,s5598,s5620,s5619,s5621]) ).
fof(f97631,plain,
$false,
inference(avatar_sat_refutation,[],[s5625]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV574+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 06:38:32 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 Running first-order theorem proving
% 0.15/0.41 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
% 11.81/2.60 % (4192297)Detected formulas, will run a generic FOF schedule.
% 11.81/2.60 % (4192306)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3118479273:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.81/2.60 % (4192306)Instruction limit reached!
% 11.81/2.60 % (4192306)------------------------------
% 11.81/2.60 % (4192306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.81/2.60 % (4192306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.81/2.60 % (4192306)CaDiCaL version: 2.1.3
% 11.81/2.60 % (4192306)Termination reason: Instruction limit
% 11.81/2.60 % (4192306)Termination phase: Saturation
% 11.81/2.60 % (4192306)Time elapsed: 0.040 s
% 11.81/2.60 % (4192306)Peak memory usage: 89 MB
% 11.81/2.60 % (4192306)Instructions burned: 120 (million)
% 11.81/2.60 % (4192307)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3010397891:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.81/2.60 % (4192302)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=3536879749:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.81/2.60 % (4192305)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=688582343:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.81/2.60 % (4192303)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=2760889192:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.81/2.60 % (4192304)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=706305841:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.81/2.60 % (4192308)dis-21_1_sil=8000:lcm=predicate:random_seed=887428: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)
% 11.81/2.60 % (4192305)Refutation not found, incomplete strategy
% 11.81/2.60 % (4192305)------------------------------
% 11.81/2.60 % (4192305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.81/2.60 % (4192305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.81/2.60 % (4192305)CaDiCaL version: 2.1.3
% 11.81/2.60 % (4192305)Termination reason: Refutation not found, incomplete strategy
% 11.81/2.60 % (4192305)Time elapsed: 0.001 s
% 11.81/2.60 % (4192305)Peak memory usage: 88 MB
% 11.81/2.60 % (4192305)Instructions burned: 1 (million)
% 11.81/2.60 % (4192308)Instruction limit reached!
% 11.81/2.60 % (4192308)------------------------------
% 11.81/2.60 % (4192308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.81/2.60 % (4192308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.81/2.60 % (4192308)CaDiCaL version: 2.1.3
% 11.81/2.60 % (4192308)Termination reason: Instruction limit
% 11.81/2.60 % (4192308)Termination phase: Saturation
% 11.81/2.60 % (4192308)Time elapsed: 0.065 s
% 11.81/2.60 % (4192308)Peak memory usage: 88 MB
% 11.81/2.60 % (4192308)Instructions burned: 129 (million)
% 11.81/2.60 % (4192307)Instruction limit reached!
% 11.81/2.60 % (4192307)------------------------------
% 11.81/2.60 % (4192307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.81/2.60 % (4192307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.81/2.60 % (4192307)CaDiCaL version: 2.1.3
% 11.81/2.60 % (4192307)Termination reason: Instruction limit
% 11.81/2.60 % (4192307)Termination phase: Saturation
% 11.81/2.60 % (4192307)Time elapsed: 0.091 s
% 11.81/2.60 % (4192307)Peak memory usage: 89 MB
% 11.81/2.60 % (4192307)Instructions burned: 139 (million)
% 11.81/2.60 % (4192310)lrs+10_1_sil=8000:sp=occurrence:random_seed=3215762895:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.81/2.60 % (4192310)Instruction limit reached!
% 11.81/2.60 % (4192310)------------------------------
% 11.81/2.60 % (4192310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.81/2.60 % (4192310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.81/2.60 % (4192310)CaDiCaL version: 2.1.3
% 11.81/2.60 % (4192310)Termination reason: Instruction limit
% 11.81/2.60 % (4192310)Termination phase: Saturation
% 11.81/2.60 % (4192310)Time elapsed: 0.100 s
% 11.81/2.60 % (4192310)Peak memory usage: 91 MB
% 11.81/2.60 % (4192310)Instructions burned: 286 (million)
% 11.81/2.60 % (4192317)lrs+10_1_sil=32000:urr=on:br=off:random_seed=958338423:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.35/3.67 % (4192305)------------------------------
% 19.35/3.67 % (4192305)------------------------------
% 19.35/3.67 % (4192318)lrs+1011_1_sil=32000:sp=occurrence:random_seed=984482110:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.35/3.67 % (4192317)Instruction limit reached!
% 19.35/3.67 % (4192317)------------------------------
% 19.35/3.67 % (4192317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.67 % (4192317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.67 % (4192317)CaDiCaL version: 2.1.3
% 19.35/3.67 % (4192317)Termination reason: Instruction limit
% 19.35/3.67 % (4192317)Termination phase: Saturation
% 19.35/3.67 % (4192317)Time elapsed: 0.080 s
% 19.35/3.67 % (4192317)Peak memory usage: 90 MB
% 19.35/3.67 % (4192317)Instructions burned: 157 (million)
% 19.35/3.67 % (4192320)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=3393905965:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 19.35/3.67 % (4192320)Instruction limit reached!
% 19.35/3.67 % (4192320)------------------------------
% 19.35/3.67 % (4192320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.67 % (4192320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.67 % (4192320)CaDiCaL version: 2.1.3
% 19.35/3.67 % (4192320)Termination reason: Instruction limit
% 19.35/3.67 % (4192320)Termination phase: Saturation
% 19.35/3.67 % (4192320)Time elapsed: 0.074 s
% 19.35/3.67 % (4192320)Peak memory usage: 91 MB
% 19.35/3.67 % (4192320)Instructions burned: 250 (million)
% 19.35/3.67 % (4192323)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=293948103:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.35/3.67 % (4192323)Refutation not found, incomplete strategy
% 19.35/3.67 % (4192323)------------------------------
% 19.35/3.67 % (4192323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.67 % (4192323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.67 % (4192323)CaDiCaL version: 2.1.3
% 19.35/3.67 % (4192323)Termination reason: Refutation not found, incomplete strategy
% 19.35/3.67 % (4192323)Time elapsed: 0.002 s
% 19.35/3.67 % (4192323)Peak memory usage: 88 MB
% 19.35/3.67 % (4192323)Instructions burned: 1 (million)
% 19.35/3.67 % (4192324)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1095689005:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 19.35/3.67 % (4192318)Instruction limit reached!
% 19.35/3.67 % (4192318)------------------------------
% 19.35/3.67 % (4192318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.67 % (4192318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.67 % (4192318)CaDiCaL version: 2.1.3
% 19.35/3.67 % (4192318)Termination reason: Instruction limit
% 19.35/3.67 % (4192318)Termination phase: Saturation
% 19.35/3.67 % (4192318)Time elapsed: 0.211 s
% 19.35/3.67 % (4192318)Peak memory usage: 91 MB
% 19.35/3.67 % (4192318)Instructions burned: 326 (million)
% 19.35/3.67 % (4192326)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=764027824:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.35/3.67 % (4192326)Instruction limit reached!
% 19.35/3.67 % (4192326)------------------------------
% 19.35/3.67 % (4192326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.67 % (4192326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/3.67 % (4192326)CaDiCaL version: 2.1.3
% 19.35/3.67 % (4192326)Termination reason: Instruction limit
% 19.35/3.67 % (4192326)Termination phase: Saturation
% 19.35/3.67 % (4192326)Time elapsed: 0.035 s
% 19.35/3.67 % (4192326)Peak memory usage: 89 MB
% 19.35/3.67 % (4192326)Instructions burned: 114 (million)
% 19.35/3.67 % (4192329)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2172933918:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 19.35/3.67 % (4192323)------------------------------
% 19.35/3.67 % (4192323)------------------------------
% 19.35/3.67 % (4192329)Instruction limit reached!
% 19.35/3.67 % (4192329)------------------------------
% 19.35/3.67 % (4192329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/3.67 % (4192329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192329)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192329)Termination reason: Instruction limit
% 37.09/6.93 % (4192329)Termination phase: Saturation
% 37.09/6.93 % (4192329)Time elapsed: 0.058 s
% 37.09/6.93 % (4192329)Peak memory usage: 88 MB
% 37.09/6.93 % (4192329)Instructions burned: 129 (million)
% 37.09/6.93 % (4192331)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=745426406:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 37.09/6.93 % (4192331)Instruction limit reached!
% 37.09/6.93 % (4192331)------------------------------
% 37.09/6.93 % (4192331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192331)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192331)Termination reason: Instruction limit
% 37.09/6.93 % (4192331)Termination phase: Saturation
% 37.09/6.93 % (4192331)Time elapsed: 0.029 s
% 37.09/6.93 % (4192331)Peak memory usage: 88 MB
% 37.09/6.93 % (4192331)Instructions burned: 117 (million)
% 37.09/6.93 % (4192333)lrs+10_1_sil=8000:sp=occurrence:random_seed=587357916:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 37.09/6.93 % (4192336)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4271909112:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 37.09/6.93 % (4192335)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2493865358:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 37.09/6.93 % (4192335)Refutation not found, incomplete strategy
% 37.09/6.93 % (4192335)------------------------------
% 37.09/6.93 % (4192335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192335)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192335)Termination reason: Refutation not found, incomplete strategy
% 37.09/6.93 % (4192335)Time elapsed: 0.001 s
% 37.09/6.93 % (4192335)Peak memory usage: 88 MB
% 37.09/6.93 % (4192335)Instructions burned: 1 (million)
% 37.09/6.93 % (4192335)------------------------------
% 37.09/6.93 % (4192335)------------------------------
% 37.09/6.93 % (4192340)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2419835381:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 37.09/6.93 % (4192340)Instruction limit reached!
% 37.09/6.93 % (4192340)------------------------------
% 37.09/6.93 % (4192340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192340)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192340)Termination reason: Instruction limit
% 37.09/6.93 % (4192340)Termination phase: Saturation
% 37.09/6.93 % (4192340)Time elapsed: 0.069 s
% 37.09/6.93 % (4192340)Peak memory usage: 90 MB
% 37.09/6.93 % (4192340)Instructions burned: 135 (million)
% 37.09/6.93 % (4192333)Instruction limit reached!
% 37.09/6.93 % (4192333)------------------------------
% 37.09/6.93 % (4192333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192333)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192333)Termination reason: Instruction limit
% 37.09/6.93 % (4192333)Termination phase: Saturation
% 37.09/6.93 % (4192333)Time elapsed: 0.570 s
% 37.09/6.93 % (4192333)Peak memory usage: 97 MB
% 37.09/6.93 % (4192333)Instructions burned: 908 (million)
% 37.09/6.93 % (4192342)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1908570142:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 37.09/6.93 % (4192342)Refutation not found, incomplete strategy
% 37.09/6.93 % (4192342)------------------------------
% 37.09/6.93 % (4192342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192342)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192342)Termination reason: Refutation not found, incomplete strategy
% 37.09/6.93 % (4192342)Time elapsed: 0.002 s
% 37.09/6.93 % (4192342)Peak memory usage: 88 MB
% 37.09/6.93 % (4192342)Instructions burned: 1 (million)
% 37.09/6.93 % (4192343)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3604110415:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 37.09/6.93 % (4192342)------------------------------
% 37.09/6.93 % (4192342)------------------------------
% 37.09/6.93 % (4192346)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=2764525701:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 37.09/6.93 % (4192346)Instruction limit reached!
% 37.09/6.93 % (4192346)------------------------------
% 37.09/6.93 % (4192346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192346)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192346)Termination reason: Instruction limit
% 37.09/6.93 % (4192346)Termination phase: Saturation
% 37.09/6.93 % (4192346)Time elapsed: 0.076 s
% 37.09/6.93 % (4192346)Peak memory usage: 90 MB
% 37.09/6.93 % (4192346)Instructions burned: 125 (million)
% 37.09/6.93 % (4192324)Instruction limit reached!
% 37.09/6.93 % (4192324)------------------------------
% 37.09/6.93 % (4192324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192324)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192324)Termination reason: Instruction limit
% 37.09/6.93 % (4192324)Termination phase: Saturation
% 37.09/6.93 % (4192324)Time elapsed: 1.583 s
% 37.09/6.93 % (4192324)Peak memory usage: 141 MB
% 37.09/6.93 % (4192324)Instructions burned: 2351 (million)
% 37.09/6.93 % (4192348)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1065951695:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 37.09/6.93 % (4192348)Instruction limit reached!
% 37.09/6.93 % (4192348)------------------------------
% 37.09/6.93 % (4192348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.93 % (4192348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.93 % (4192348)CaDiCaL version: 2.1.3
% 37.09/6.93 % (4192348)Termination reason: Instruction limit
% 37.09/6.93 % (4192348)Termination phase: Saturation
% 37.09/6.93 % (4192348)Time elapsed: 0.057 s
% 37.09/6.93 % (4192348)Peak memory usage: 89 MB
% 37.09/6.93 % (4192348)Instructions burned: 136 (million)
% 37.09/6.94 % (4192349)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=884177928:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 37.09/6.94 % (4192349)Refutation not found, incomplete strategy
% 37.09/6.94 % (4192349)------------------------------
% 37.09/6.94 % (4192349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.94 % (4192349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.94 % (4192349)CaDiCaL version: 2.1.3
% 37.09/6.94 % (4192349)Termination reason: Refutation not found, incomplete strategy
% 37.09/6.94 % (4192349)Time elapsed: 0.001 s
% 37.09/6.94 % (4192349)Peak memory usage: 88 MB
% 37.09/6.94 % (4192351)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1799343424:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 37.09/6.94 % (4192349)------------------------------
% 37.09/6.94 % (4192349)------------------------------
% 37.09/6.94 % (4192351)Instruction limit reached!
% 37.09/6.94 % (4192351)------------------------------
% 37.09/6.94 % (4192351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.94 % (4192351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.94 % (4192351)CaDiCaL version: 2.1.3
% 37.09/6.94 % (4192351)Termination reason: Instruction limit
% 37.09/6.94 % (4192351)Termination phase: Saturation
% 37.09/6.94 % (4192351)Time elapsed: 0.230 s
% 37.09/6.94 % (4192351)Peak memory usage: 91 MB
% 37.09/6.94 % (4192351)Instructions burned: 432 (million)
% 37.09/6.94 % (4192336)Instruction limit reached!
% 37.09/6.94 % (4192336)------------------------------
% 37.09/6.94 % (4192336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.94 % (4192336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.94 % (4192336)CaDiCaL version: 2.1.3
% 37.09/6.94 % (4192336)Termination reason: Instruction limit
% 37.09/6.94 % (4192336)Termination phase: Saturation
% 37.09/6.94 % (4192336)Time elapsed: 1.753 s
% 37.09/6.94 % (4192336)Peak memory usage: 163 MB
% 37.09/6.94 % (4192336)Instructions burned: 5203 (million)
% 37.09/6.94 % (4192354)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=739286752:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 37.09/6.94 % (4192356)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1889190981:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 37.09/6.94 % (4192355)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1993712680:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 37.09/6.94 % (4192355)Instruction limit reached!
% 37.09/6.94 % (4192355)------------------------------
% 37.09/6.94 % (4192355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.94 % (4192355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.94 % (4192355)CaDiCaL version: 2.1.3
% 37.09/6.94 % (4192355)Termination reason: Instruction limit
% 37.09/6.94 % (4192355)Termination phase: Saturation
% 37.09/6.94 % (4192355)Time elapsed: 0.086 s
% 37.09/6.94 % (4192355)Peak memory usage: 91 MB
% 37.09/6.94 % (4192355)Instructions burned: 152 (million)
% 37.09/6.94 % (4192360)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3704063606:i=667:av=off:fsr=off_2970 on theBenchmark for (2970ds/667Mi)
% 37.09/6.94 % (4192360)Refutation not found, incomplete strategy
% 37.09/6.94 % (4192360)------------------------------
% 37.09/6.94 % (4192360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.94 % (4192360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.94 % (4192360)CaDiCaL version: 2.1.3
% 37.09/6.94 % (4192360)Termination reason: Refutation not found, incomplete strategy
% 37.09/6.94 % (4192360)Time elapsed: 0.002 s
% 37.09/6.94 % (4192360)Peak memory usage: 88 MB
% 37.09/6.94 % (4192360)Instructions burned: 1 (million)
% 37.09/6.94 % (4192360)------------------------------
% 37.09/6.94 % (4192360)------------------------------
% 37.09/6.94 % (4192362)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2598562692:s2a=on:i=185:s2at=1.8:fdi=4_2965 on theBenchmark for (2965ds/185Mi)
% 37.09/6.94 % (4192362)Instruction limit reached!
% 37.09/6.94 % (4192362)------------------------------
% 37.09/6.94 % (4192362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.94 % (4192362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.94 % (4192362)CaDiCaL version: 2.1.3
% 37.09/6.94 % (4192362)Termination reason: Instruction limit
% 37.09/6.94 % (4192362)Termination phase: Saturation
% 37.09/6.94 % (4192362)Time elapsed: 0.106 s
% 37.09/6.94 % (4192362)Peak memory usage: 91 MB
% 37.09/6.94 % (4192362)Instructions burned: 186 (million)
% 37.09/6.94 % (4192364)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3405968824:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2962 on theBenchmark for (2962ds/193Mi)
% 37.09/6.94 % (4192364)Instruction limit reached!
% 37.09/6.94 % (4192364)------------------------------
% 37.09/6.94 % (4192364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.09/6.94 % (4192364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.09/6.94 % (4192364)CaDiCaL version: 2.1.3
% 37.09/6.94 % (4192364)Termination reason: Instruction limit
% 37.09/6.94 % (4192364)Termination phase: Saturation
% 37.09/6.94 % (4192364)Time elapsed: 0.129 s
% 37.09/6.94 % (4192364)Peak memory usage: 92 MB
% 37.09/6.94 % (4192364)Instructions burned: 194 (million)
% 37.09/6.94 % (4192366)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2116010751:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2960 on theBenchmark for (2960ds/4850Mi)
% 37.09/6.94 % (4192302)First to succeed.
% 37.09/6.94 % (4192302)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4192297"
% 37.09/6.94 % (4192302)Refutation found. Thanks to Tanya!
% 37.09/6.94 % SZS status Theorem for theBenchmark
% 37.09/6.94 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/7.13 % (4192302)------------------------------
% 0.18/7.13 % (4192302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/7.13 % (4192302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/7.13 % (4192302)CaDiCaL version: 2.1.3
% 0.18/7.13 % (4192302)Termination reason: Refutation
% 0.18/7.13 % (4192302)Time elapsed: 5.612 s
% 0.18/7.13 % (4192302)Peak memory usage: 190 MB
% 0.18/7.13 % (4192302)Instructions burned: 8663 (million)
% 0.18/7.13 % (4192302)------------------------------
% 0.18/7.13 % (4192302)------------------------------
% 0.18/7.13 % (4192297)Success in time 6.076 s
% 0.18/7.13 % Vampire exiting
%------------------------------------------------------------------------------