%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV578+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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:59:31 PM UTC 2026
% Result : Theorem 7.45s 1.55s
% Output : Refutation 7.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 58
% Syntax : Number of formulae : 331 ( 106 unt; 51 def)
% Number of atoms : 648 ( 86 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 557 ( 240 ~; 274 |; 12 &)
% ( 30 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 29 ( 27 usr; 26 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 27 con; 0-2 aty)
% Number of variables : 102 ( 0 sgn 100 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X0)
=> mem(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET010+0.ax',subq_def) ).
fof(f5,axiom,
! [X0,X1] :
( mem(X0,s(X1))
<=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET010+0.ax',s_ax) ).
fof(f6,axiom,
! [X0,X1,X2] :
( mem(X0,u(X1,X2))
<=> ( mem(X0,X1)
| mem(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET010+0.ax',u_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SET010+0.ax',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SET010+0.ax',n_def) ).
fof(f10,axiom,
! [X0,X1] :
( mem(X0,p(X1))
<=> subq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET010+0.ax',p_ax) ).
fof(f26,conjecture,
subq(u(u(s(u(n(e),n(s(n(e))))),a(s(p(s(n(e)))),s(n(n(e))))),a(u(s(n(e)),n(s(s(n(e))))),a(s(n(e)),n(n(e))))),u(u(n(u(n(e),n(s(n(e))))),a(p(p(s(n(e)))),s(n(n(e))))),s(a(s(n(e)),n(n(e)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subq_1462_1463) ).
fof(f27,negated_conjecture,
~ subq(u(u(s(u(n(e),n(s(n(e))))),a(s(p(s(n(e)))),s(n(n(e))))),a(u(s(n(e)),n(s(s(n(e))))),a(s(n(e)),n(n(e))))),u(u(n(u(n(e),n(s(n(e))))),a(p(p(s(n(e)))),s(n(n(e))))),s(a(s(n(e)),n(n(e)))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
~ subq(u(u(s(u(n(e),n(s(n(e))))),a(s(p(s(n(e)))),s(n(n(e))))),a(u(s(n(e)),n(s(s(n(e))))),a(s(n(e)),n(n(e))))),u(u(n(u(n(e),n(s(n(e))))),a(p(p(s(n(e)))),s(n(n(e))))),s(a(s(n(e)),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(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(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] :
( subq(X0,X1)
| mem(sK0(X0,X1),X0) ),
inference(cnf_transformation,[],[f34]) ).
fof(f43,plain,
! [X0,X1] :
( ~ mem(sK0(X0,X1),X1)
| subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
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(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] :
( ~ subq(X0,X1)
| mem(X0,p(X1)) ),
inference(cnf_transformation,[],[f40]) ).
fof(f58,plain,
~ subq(u(u(s(u(n(e),n(s(n(e))))),a(s(p(s(n(e)))),s(n(n(e))))),a(u(s(n(e)),n(s(s(n(e))))),a(s(n(e)),n(n(e))))),u(u(n(u(n(e),n(s(n(e))))),a(p(p(s(n(e)))),s(n(n(e))))),s(a(s(n(e)),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(u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),u(s(p(s(u(e,s(e))))),s(s(u(u(e,s(e)),s(u(e,s(e)))))))),u(u(s(u(e,s(e))),u(s(s(u(e,s(e)))),s(s(s(u(e,s(e))))))),s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e))))))))),u(u(u(u(u(e,s(e)),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)))))))),u(p(p(s(u(e,s(e))))),s(s(u(u(e,s(e)),s(u(e,s(e)))))))),s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e))))))))),
inference(definition_unfolding,[],[f58,f59,f59,f59,f54,f59,f59,f59,f54,f59,f59,f59,f54,f59,f59,f59,f59,f59,f59,f59,f54,f59,f59,f59,f54,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 = s(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f75,plain,
s(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 = s(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f79,plain,
s(sF8) = sF9,
inference(reorient_equations,[],[f78]) ).
fof(f80,definition,
sF10 = u(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f81,plain,
u(sF2,sF3) = sF10,
inference(reorient_equations,[],[f80]) ).
fof(f82,definition,
sF11 = s(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f83,plain,
s(sF10) = sF11,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF12 = s(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f85,plain,
s(sF11) = sF12,
inference(reorient_equations,[],[f84]) ).
fof(f86,definition,
sF13 = u(sF9,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f87,plain,
u(sF9,sF12) = sF13,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF14 = u(sF7,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f89,plain,
u(sF7,sF13) = sF14,
inference(reorient_equations,[],[f88]) ).
fof(f90,definition,
sF15 = s(sF4),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f91,plain,
s(sF4) = sF15,
inference(reorient_equations,[],[f90]) ).
fof(f92,definition,
sF16 = u(sF4,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f93,plain,
u(sF4,sF15) = sF16,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF17 = u(sF3,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f95,plain,
u(sF3,sF16) = sF17,
inference(reorient_equations,[],[f94]) ).
fof(f96,definition,
sF18 = u(sF3,sF11),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f97,plain,
u(sF3,sF11) = sF18,
inference(reorient_equations,[],[f96]) ).
fof(f98,definition,
sF19 = s(sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f99,plain,
s(sF18) = sF19,
inference(reorient_equations,[],[f98]) ).
fof(f100,definition,
sF20 = u(sF17,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f101,plain,
u(sF17,sF19) = sF20,
inference(reorient_equations,[],[f100]) ).
fof(f102,definition,
sF21 = u(sF14,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f103,plain,
u(sF14,sF20) = sF21,
inference(reorient_equations,[],[f102]) ).
fof(f104,definition,
sF22 = u(sF6,sF7),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f105,plain,
u(sF6,sF7) = sF22,
inference(reorient_equations,[],[f104]) ).
fof(f106,definition,
sF23 = p(sF8),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f107,plain,
p(sF8) = sF23,
inference(reorient_equations,[],[f106]) ).
fof(f108,definition,
sF24 = u(sF23,sF12),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f109,plain,
u(sF23,sF12) = sF24,
inference(reorient_equations,[],[f108]) ).
fof(f110,definition,
sF25 = u(sF22,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f111,plain,
u(sF22,sF24) = sF25,
inference(reorient_equations,[],[f110]) ).
fof(f112,definition,
sF26 = u(sF25,sF19),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f113,plain,
u(sF25,sF19) = sF26,
inference(reorient_equations,[],[f112]) ).
fof(f114,plain,
~ subq(sF21,sF26),
inference(definition_folding,[],[f60,f113,f99,f97,f83,f81,f67,f65,f63,f65,f63,f67,f65,f63,f111,f109,f85,f83,f81,f67,f65,f63,f65,f63,f107,f77,f67,f65,f63,f105,f75,f73,f71,f69,f67,f65,f63,f67,f65,f63,f65,f63,f73,f71,f69,f67,f65,f63,f67,f65,f63,f65,f63,f103,f101,f99,f97,f83,f81,f67,f65,f63,f65,f63,f67,f65,f63,f95,f93,f91,f69,f67,f65,f63,f69,f67,f65,f63,f67,f65,f63,f89,f87,f85,f83,f81,f67,f65,f63,f65,f63,f79,f77,f67,f65,f63,f75,f73,f71,f69,f67,f65,f63,f67,f65,f63,f65,f63]) ).
fof(f116,plain,
mem(sF2,sF3),
inference(superposition,[],[f61,f67]) ).
fof(f117,plain,
mem(sF3,sF4),
inference(superposition,[],[f61,f69]) ).
fof(f126,plain,
! [X0] :
( ~ mem(X0,sF3)
| sF2 = X0 ),
inference(superposition,[],[f46,f67]) ).
fof(f127,plain,
! [X0] :
( ~ mem(X0,sF4)
| sF3 = X0 ),
inference(superposition,[],[f46,f69]) ).
fof(f128,plain,
! [X0] :
( ~ mem(X0,sF15)
| sF4 = X0 ),
inference(superposition,[],[f46,f91]) ).
fof(f130,plain,
! [X0] :
( ~ mem(X0,sF9)
| sF8 = X0 ),
inference(superposition,[],[f46,f79]) ).
fof(f138,plain,
mem(sK0(sF21,sF26),sF21),
inference(resolution,[],[f42,f114]) ).
fof(f139,plain,
! [X0,X1] :
( mem(sK0(X0,X1),X0)
| mem(X0,p(X1)) ),
inference(resolution,[],[f42,f57]) ).
fof(f141,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f49,f43]) ).
fof(f143,plain,
! [X0] :
( ~ mem(X0,sF5)
| mem(X0,sF6) ),
inference(superposition,[],[f49,f73]) ).
fof(f145,plain,
! [X0] :
( ~ mem(X0,sF4)
| mem(X0,sF5) ),
inference(superposition,[],[f49,f71]) ).
fof(f149,plain,
! [X0] :
( ~ mem(X0,sF7)
| mem(X0,sF22) ),
inference(superposition,[],[f49,f105]) ).
fof(f154,plain,
! [X0] :
( ~ mem(X0,sF24)
| mem(X0,sF25) ),
inference(superposition,[],[f49,f111]) ).
fof(f155,plain,
! [X0] :
( ~ mem(X0,sF12)
| mem(X0,sF24) ),
inference(superposition,[],[f49,f109]) ).
fof(f158,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f50,f43]) ).
fof(f162,plain,
! [X0] :
( ~ mem(X0,sF3)
| mem(X0,sF5) ),
inference(superposition,[],[f50,f71]) ).
fof(f166,plain,
! [X0] :
( ~ mem(X0,sF6)
| mem(X0,sF22) ),
inference(superposition,[],[f50,f105]) ).
fof(f171,plain,
! [X0] :
( ~ mem(X0,sF22)
| mem(X0,sF25) ),
inference(superposition,[],[f50,f111]) ).
fof(f172,plain,
! [X0] :
( ~ mem(X0,sF23)
| mem(X0,sF24) ),
inference(superposition,[],[f50,f109]) ).
fof(f183,plain,
! [X0] :
( ~ subq(sF4,X0)
| mem(sF3,X0) ),
inference(resolution,[],[f41,f117]) ).
fof(f206,definition,
( spl27_1
<=> sF4 = sK0(sF21,sF26) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
fof(f207,plain,
( sF4 != sK0(sF21,sF26)
| spl27_1 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f208,plain,
( sF4 = sK0(sF21,sF26)
| ~ spl27_1 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f224,definition,
( spl27_5
<=> sF8 = sK0(sF21,sF26) ),
introduced(definition,[new_symbols(definition,[spl27_5])],[avatar_definition]) ).
fof(f225,plain,
( sF8 != sK0(sF21,sF26)
| spl27_5 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f226,plain,
( sF8 = sK0(sF21,sF26)
| ~ spl27_5 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f242,definition,
( spl27_9
<=> sF3 = sK0(sF21,sF26) ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
fof(f243,plain,
( sF3 != sK0(sF21,sF26)
| spl27_9 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f244,plain,
( sF3 = sK0(sF21,sF26)
| ~ spl27_9 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f251,definition,
( spl27_11
<=> sF2 = sK0(sF21,sF26) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
fof(f252,plain,
( sF2 != sK0(sF21,sF26)
| spl27_11 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f253,plain,
( sF2 = sK0(sF21,sF26)
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f275,plain,
! [X0] :
( ~ mem(X0,sF17)
| mem(X0,sF16)
| mem(X0,sF3) ),
inference(superposition,[],[f48,f95]) ).
fof(f277,plain,
! [X0] :
( ~ mem(X0,sF16)
| mem(X0,sF15)
| mem(X0,sF4) ),
inference(superposition,[],[f48,f93]) ).
fof(f279,plain,
! [X0] :
( ~ mem(X0,sF14)
| mem(X0,sF13)
| mem(X0,sF7) ),
inference(superposition,[],[f48,f89]) ).
fof(f280,plain,
! [X0] :
( ~ mem(X0,sF13)
| mem(X0,sF12)
| mem(X0,sF9) ),
inference(superposition,[],[f48,f87]) ).
fof(f281,plain,
! [X0] :
( ~ mem(X0,sF21)
| mem(X0,sF20)
| mem(X0,sF14) ),
inference(superposition,[],[f48,f103]) ).
fof(f282,plain,
! [X0] :
( ~ mem(X0,sF20)
| mem(X0,sF19)
| mem(X0,sF17) ),
inference(superposition,[],[f48,f101]) ).
fof(f393,definition,
( spl27_28
<=> mem(sF3,sF6) ),
introduced(definition,[new_symbols(definition,[spl27_28])],[avatar_definition]) ).
fof(f394,plain,
( ~ mem(sF3,sF6)
| spl27_28 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f395,plain,
( mem(sF3,sF6)
| ~ spl27_28 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f425,definition,
( spl27_32
<=> mem(sK0(sF21,sF26),sF17) ),
introduced(definition,[new_symbols(definition,[spl27_32])],[avatar_definition]) ).
fof(f426,plain,
( ~ mem(sK0(sF21,sF26),sF17)
| spl27_32 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( mem(sK0(sF21,sF26),sF17)
| ~ spl27_32 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f444,definition,
( spl27_34
<=> mem(sK0(sF21,sF26),sF14) ),
introduced(definition,[new_symbols(definition,[spl27_34])],[avatar_definition]) ).
fof(f445,plain,
( ~ mem(sK0(sF21,sF26),sF14)
| spl27_34 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f446,plain,
( mem(sK0(sF21,sF26),sF14)
| ~ spl27_34 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f461,definition,
( spl27_36
<=> mem(sK0(sF21,sF26),sF25) ),
introduced(definition,[new_symbols(definition,[spl27_36])],[avatar_definition]) ).
fof(f462,plain,
( ~ mem(sK0(sF21,sF26),sF25)
| spl27_36 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f463,plain,
( mem(sK0(sF21,sF26),sF25)
| ~ spl27_36 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f476,definition,
( spl27_38
<=> mem(sK0(sF21,sF26),sF6) ),
introduced(definition,[new_symbols(definition,[spl27_38])],[avatar_definition]) ).
fof(f477,plain,
( ~ mem(sK0(sF21,sF26),sF6)
| spl27_38 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f478,plain,
( mem(sK0(sF21,sF26),sF6)
| ~ spl27_38 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f483,plain,
mem(sF2,sF5),
inference(resolution,[],[f162,f116]) ).
fof(f501,definition,
( spl27_40
<=> mem(sK0(sF21,sF26),sF22) ),
introduced(definition,[new_symbols(definition,[spl27_40])],[avatar_definition]) ).
fof(f502,plain,
( ~ mem(sK0(sF21,sF26),sF22)
| spl27_40 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f503,plain,
( mem(sK0(sF21,sF26),sF22)
| ~ spl27_40 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f521,definition,
( spl27_42
<=> mem(sK0(sF21,sF26),sF20) ),
introduced(definition,[new_symbols(definition,[spl27_42])],[avatar_definition]) ).
fof(f522,plain,
( ~ mem(sK0(sF21,sF26),sF20)
| spl27_42 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f523,plain,
( mem(sK0(sF21,sF26),sF20)
| ~ spl27_42 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f562,plain,
! [X0] :
( mem(X0,p(X0))
| subq(X0,X0) ),
inference(resolution,[],[f139,f43]) ).
fof(f581,plain,
! [X0] :
( mem(sK0(sF4,X0),sF5)
| mem(sF4,p(X0)) ),
inference(resolution,[],[f139,f145]) ).
fof(f582,plain,
! [X0] :
( mem(sF4,p(X0))
| sF3 = sK0(sF4,X0) ),
inference(resolution,[],[f139,f127]) ).
fof(f611,plain,
! [X0] : subq(X0,X0),
inference(forward_subsumption_resolution,[],[f562,f56]) ).
fof(f627,definition,
( spl27_48
<=> mem(sK0(sF21,sF26),sF3) ),
introduced(definition,[new_symbols(definition,[spl27_48])],[avatar_definition]) ).
fof(f628,plain,
( ~ mem(sK0(sF21,sF26),sF3)
| spl27_48 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( mem(sK0(sF21,sF26),sF3)
| ~ spl27_48 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f657,plain,
( sF2 = sK0(sF21,sF26)
| ~ spl27_48 ),
inference(resolution,[],[f629,f126]) ).
fof(f659,plain,
( $false
| spl27_11
| ~ spl27_48 ),
inference(forward_subsumption_resolution,[],[f657,f252]) ).
fof(f660,plain,
( spl27_11
| ~ spl27_48 ),
inference(avatar_contradiction_clause,[],[f659]) ).
fof(f683,definition,
( spl27_54
<=> mem(sK0(sF21,sF26),sF7) ),
introduced(definition,[new_symbols(definition,[spl27_54])],[avatar_definition]) ).
fof(f684,plain,
( ~ mem(sK0(sF21,sF26),sF7)
| spl27_54 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f685,plain,
( mem(sK0(sF21,sF26),sF7)
| ~ spl27_54 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f687,definition,
( spl27_55
<=> mem(sK0(sF21,sF26),sF13) ),
introduced(definition,[new_symbols(definition,[spl27_55])],[avatar_definition]) ).
fof(f689,plain,
( mem(sK0(sF21,sF26),sF13)
| ~ spl27_55 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f693,plain,
( mem(sK0(sF21,sF26),sF16)
| mem(sK0(sF21,sF26),sF3)
| ~ spl27_32 ),
inference(resolution,[],[f427,f275]) ).
fof(f697,plain,
( mem(sK0(sF21,sF26),sF16)
| ~ spl27_32
| spl27_48 ),
inference(forward_subsumption_resolution,[],[f693,f628]) ).
fof(f721,plain,
( mem(sK0(sF21,sF26),sF20)
| mem(sK0(sF21,sF26),sF14) ),
inference(resolution,[],[f281,f138]) ).
fof(f1151,plain,
( mem(sF3,sF22)
| ~ spl27_28 ),
inference(resolution,[],[f395,f166]) ).
fof(f1219,plain,
! [X0] :
( ~ mem(sK0(X0,sF6),sF5)
| subq(X0,sF6) ),
inference(superposition,[],[f141,f73]) ).
fof(f1232,plain,
! [X0] :
( ~ mem(sK0(X0,sF26),sF19)
| subq(X0,sF26) ),
inference(superposition,[],[f141,f113]) ).
fof(f1259,plain,
! [X0] :
( ~ mem(sK0(X0,sF26),sF25)
| subq(X0,sF26) ),
inference(superposition,[],[f158,f113]) ).
fof(f1432,plain,
mem(sF2,sF6),
inference(resolution,[],[f483,f143]) ).
fof(f1458,plain,
! [X0] : mem(X0,p(X0)),
inference(resolution,[],[f611,f57]) ).
fof(f1478,plain,
( mem(sF3,sF25)
| ~ spl27_28 ),
inference(resolution,[],[f1151,f171]) ).
fof(f1720,plain,
( subq(sF21,sF26)
| ~ spl27_36 ),
inference(resolution,[],[f463,f1259]) ).
fof(f1724,plain,
( $false
| ~ spl27_36 ),
inference(forward_subsumption_resolution,[],[f1720,f114]) ).
fof(f1725,plain,
~ spl27_36,
inference(avatar_contradiction_clause,[],[f1724]) ).
fof(f1828,plain,
( mem(sK0(sF21,sF26),sF22)
| ~ spl27_38 ),
inference(resolution,[],[f478,f166]) ).
fof(f1872,definition,
( spl27_141
<=> mem(sF3,sF8) ),
introduced(definition,[new_symbols(definition,[spl27_141])],[avatar_definition]) ).
fof(f1873,plain,
( ~ mem(sF3,sF8)
| spl27_141 ),
inference(avatar_component_clause,[],[f1872]) ).
fof(f1874,plain,
( mem(sF3,sF8)
| ~ spl27_141 ),
inference(avatar_component_clause,[],[f1872]) ).
fof(f1908,plain,
( mem(sF4,p(sF6))
| subq(sF4,sF6) ),
inference(resolution,[],[f581,f1219]) ).
fof(f1919,plain,
subq(sF4,sF6),
inference(forward_subsumption_resolution,[],[f1908,f56]) ).
fof(f1921,plain,
( mem(sK0(sF21,sF26),sF25)
| ~ spl27_40 ),
inference(resolution,[],[f503,f171]) ).
fof(f1923,plain,
( $false
| spl27_36
| ~ spl27_40 ),
inference(forward_subsumption_resolution,[],[f1921,f462]) ).
fof(f1924,plain,
( spl27_36
| ~ spl27_40 ),
inference(avatar_contradiction_clause,[],[f1923]) ).
fof(f1925,plain,
( $false
| ~ spl27_38
| spl27_40 ),
inference(forward_subsumption_resolution,[],[f1828,f502]) ).
fof(f1926,plain,
( ~ spl27_38
| spl27_40 ),
inference(avatar_contradiction_clause,[],[f1925]) ).
fof(f1930,plain,
( mem(sF4,sF23)
| sF3 = sK0(sF4,sF8) ),
inference(superposition,[],[f582,f107]) ).
fof(f1932,definition,
( spl27_145
<=> sF3 = sK0(sF4,sF8) ),
introduced(definition,[new_symbols(definition,[spl27_145])],[avatar_definition]) ).
fof(f1934,plain,
( sF3 = sK0(sF4,sF8)
| ~ spl27_145 ),
inference(avatar_component_clause,[],[f1932]) ).
fof(f1936,definition,
( spl27_146
<=> mem(sF4,sF23) ),
introduced(definition,[new_symbols(definition,[spl27_146])],[avatar_definition]) ).
fof(f1938,plain,
( mem(sF4,sF23)
| ~ spl27_146 ),
inference(avatar_component_clause,[],[f1936]) ).
fof(f1939,plain,
( spl27_145
| spl27_146 ),
inference(avatar_split_clause,[],[f1930,f1936,f1932]) ).
fof(f2048,plain,
( mem(sK0(sF21,sF26),sF19)
| mem(sK0(sF21,sF26),sF17)
| ~ spl27_42 ),
inference(resolution,[],[f523,f282]) ).
fof(f2417,plain,
( ~ mem(sF2,sF6)
| ~ spl27_11
| spl27_38 ),
inference(superposition,[],[f477,f253]) ).
fof(f2430,plain,
( $false
| ~ spl27_11
| spl27_38 ),
inference(forward_subsumption_resolution,[],[f2417,f1432]) ).
fof(f2431,plain,
( ~ spl27_11
| spl27_38 ),
inference(avatar_contradiction_clause,[],[f2430]) ).
fof(f2518,plain,
( mem(sK0(sF21,sF26),sF13)
| mem(sK0(sF21,sF26),sF7)
| ~ spl27_34 ),
inference(resolution,[],[f446,f279]) ).
fof(f2573,plain,
( mem(sK0(sF21,sF26),sF22)
| ~ spl27_54 ),
inference(resolution,[],[f685,f149]) ).
fof(f2578,plain,
( $false
| spl27_40
| ~ spl27_54 ),
inference(forward_subsumption_resolution,[],[f2573,f502]) ).
fof(f2579,plain,
( spl27_40
| ~ spl27_54 ),
inference(avatar_contradiction_clause,[],[f2578]) ).
fof(f2580,plain,
( mem(sK0(sF21,sF26),sF13)
| ~ spl27_34
| spl27_54 ),
inference(forward_subsumption_resolution,[],[f2518,f684]) ).
fof(f2581,plain,
( spl27_55
| ~ spl27_34
| spl27_54 ),
inference(avatar_split_clause,[],[f2580,f683,f444,f687]) ).
fof(f2601,definition,
( spl27_190
<=> mem(sK0(sF21,sF26),sF4) ),
introduced(definition,[new_symbols(definition,[spl27_190])],[avatar_definition]) ).
fof(f2602,plain,
( ~ mem(sK0(sF21,sF26),sF4)
| spl27_190 ),
inference(avatar_component_clause,[],[f2601]) ).
fof(f2603,plain,
( mem(sK0(sF21,sF26),sF4)
| ~ spl27_190 ),
inference(avatar_component_clause,[],[f2601]) ).
fof(f2605,definition,
( spl27_191
<=> mem(sK0(sF21,sF26),sF15) ),
introduced(definition,[new_symbols(definition,[spl27_191])],[avatar_definition]) ).
fof(f2607,plain,
( mem(sK0(sF21,sF26),sF15)
| ~ spl27_191 ),
inference(avatar_component_clause,[],[f2605]) ).
fof(f2610,plain,
( mem(sK0(sF21,sF26),sF19)
| spl27_32
| ~ spl27_42 ),
inference(forward_subsumption_resolution,[],[f2048,f426]) ).
fof(f2616,definition,
( spl27_193
<=> mem(sK0(sF21,sF26),sF19) ),
introduced(definition,[new_symbols(definition,[spl27_193])],[avatar_definition]) ).
fof(f2618,plain,
( mem(sK0(sF21,sF26),sF19)
| ~ spl27_193 ),
inference(avatar_component_clause,[],[f2616]) ).
fof(f2620,plain,
( spl27_193
| spl27_32
| ~ spl27_42 ),
inference(avatar_split_clause,[],[f2610,f521,f425,f2616]) ).
fof(f2635,plain,
( mem(sK0(sF21,sF26),sF15)
| mem(sK0(sF21,sF26),sF4)
| ~ spl27_32
| spl27_48 ),
inference(resolution,[],[f697,f277]) ).
fof(f7009,definition,
( spl27_290
<=> mem(sK0(sF21,sF26),sF23) ),
introduced(definition,[new_symbols(definition,[spl27_290])],[avatar_definition]) ).
fof(f7010,plain,
( ~ mem(sK0(sF21,sF26),sF23)
| spl27_290 ),
inference(avatar_component_clause,[],[f7009]) ).
fof(f7011,plain,
( mem(sK0(sF21,sF26),sF23)
| ~ spl27_290 ),
inference(avatar_component_clause,[],[f7009]) ).
fof(f7013,definition,
( spl27_291
<=> mem(sK0(sF21,sF26),sF12) ),
introduced(definition,[new_symbols(definition,[spl27_291])],[avatar_definition]) ).
fof(f7014,plain,
( ~ mem(sK0(sF21,sF26),sF12)
| spl27_291 ),
inference(avatar_component_clause,[],[f7013]) ).
fof(f7015,plain,
( mem(sK0(sF21,sF26),sF12)
| ~ spl27_291 ),
inference(avatar_component_clause,[],[f7013]) ).
fof(f7025,definition,
( spl27_294
<=> subq(sK0(sF21,sF26),sF8) ),
introduced(definition,[new_symbols(definition,[spl27_294])],[avatar_definition]) ).
fof(f7026,plain,
( ~ subq(sK0(sF21,sF26),sF8)
| spl27_294 ),
inference(avatar_component_clause,[],[f7025]) ).
fof(f7027,plain,
( subq(sK0(sF21,sF26),sF8)
| ~ spl27_294 ),
inference(avatar_component_clause,[],[f7025]) ).
fof(f7033,definition,
( spl27_296
<=> mem(sK0(sF21,sF26),sF24) ),
introduced(definition,[new_symbols(definition,[spl27_296])],[avatar_definition]) ).
fof(f7034,plain,
( ~ mem(sK0(sF21,sF26),sF24)
| spl27_296 ),
inference(avatar_component_clause,[],[f7033]) ).
fof(f7035,plain,
( mem(sK0(sF21,sF26),sF24)
| ~ spl27_296 ),
inference(avatar_component_clause,[],[f7033]) ).
fof(f7055,definition,
( spl27_301
<=> mem(sK0(sF21,sF26),sF9) ),
introduced(definition,[new_symbols(definition,[spl27_301])],[avatar_definition]) ).
fof(f7057,plain,
( mem(sK0(sF21,sF26),sF9)
| ~ spl27_301 ),
inference(avatar_component_clause,[],[f7055]) ).
fof(f8109,plain,
mem(sF3,sF6),
inference(resolution,[],[f1919,f183]) ).
fof(f8681,plain,
( mem(sK0(sF21,sF26),sF24)
| ~ spl27_291 ),
inference(resolution,[],[f7015,f155]) ).
fof(f10231,plain,
mem(sF3,sF8),
inference(superposition,[],[f1458,f77]) ).
fof(f10232,plain,
mem(sF8,sF23),
inference(superposition,[],[f1458,f107]) ).
fof(f12288,plain,
( ~ mem(sF3,sF8)
| subq(sF4,sF8)
| ~ spl27_145 ),
inference(superposition,[],[f43,f1934]) ).
fof(f15526,plain,
( mem(sK0(sF21,sF26),sF15)
| ~ spl27_32
| spl27_48
| spl27_190 ),
inference(forward_subsumption_resolution,[],[f2635,f2602]) ).
fof(f15996,plain,
( mem(sK0(sF21,sF26),sF12)
| mem(sK0(sF21,sF26),sF9)
| ~ spl27_55 ),
inference(resolution,[],[f689,f280]) ).
fof(f16002,plain,
( mem(sK0(sF21,sF26),sF9)
| ~ spl27_55
| spl27_291 ),
inference(forward_subsumption_resolution,[],[f15996,f7014]) ).
fof(f16003,plain,
( spl27_301
| ~ spl27_55
| spl27_291 ),
inference(avatar_split_clause,[],[f16002,f7013,f687,f7055]) ).
fof(f16012,plain,
( subq(sF21,sF26)
| ~ spl27_193 ),
inference(resolution,[],[f2618,f1232]) ).
fof(f16026,plain,
( $false
| ~ spl27_193 ),
inference(forward_subsumption_resolution,[],[f16012,f114]) ).
fof(f16027,plain,
~ spl27_193,
inference(avatar_contradiction_clause,[],[f16026]) ).
fof(f16072,plain,
( mem(sK0(sF21,sF26),sF24)
| ~ spl27_290 ),
inference(resolution,[],[f7011,f172]) ).
fof(f16120,plain,
( mem(sK0(sF21,sF26),p(sF8))
| ~ spl27_294 ),
inference(resolution,[],[f7027,f57]) ).
fof(f16121,plain,
( mem(sK0(sF21,sF26),sF23)
| ~ spl27_294 ),
inference(forward_demodulation,[],[f16120,f107]) ).
fof(f16146,plain,
( mem(sK0(sF21,sF26),sF25)
| ~ spl27_296 ),
inference(resolution,[],[f7035,f154]) ).
fof(f16151,plain,
( $false
| spl27_36
| ~ spl27_296 ),
inference(forward_subsumption_resolution,[],[f16146,f462]) ).
fof(f16152,plain,
( spl27_36
| ~ spl27_296 ),
inference(avatar_contradiction_clause,[],[f16151]) ).
fof(f16154,plain,
( $false
| ~ spl27_290
| spl27_296 ),
inference(forward_subsumption_resolution,[],[f16072,f7034]) ).
fof(f16155,plain,
( ~ spl27_290
| spl27_296 ),
inference(avatar_contradiction_clause,[],[f16154]) ).
fof(f16156,plain,
( $false
| spl27_290
| ~ spl27_294 ),
inference(forward_subsumption_resolution,[],[f16121,f7010]) ).
fof(f16157,plain,
( spl27_290
| ~ spl27_294 ),
inference(avatar_contradiction_clause,[],[f16156]) ).
fof(f16240,plain,
( sF8 = sK0(sF21,sF26)
| ~ spl27_301 ),
inference(resolution,[],[f7057,f130]) ).
fof(f16245,plain,
( $false
| spl27_5
| ~ spl27_301 ),
inference(forward_subsumption_resolution,[],[f16240,f225]) ).
fof(f16246,plain,
( spl27_5
| ~ spl27_301 ),
inference(avatar_contradiction_clause,[],[f16245]) ).
fof(f16247,plain,
( $false
| ~ spl27_291
| spl27_296 ),
inference(forward_subsumption_resolution,[],[f8681,f7034]) ).
fof(f16248,plain,
( ~ spl27_291
| spl27_296 ),
inference(avatar_contradiction_clause,[],[f16247]) ).
fof(f16402,plain,
( mem(sK0(sF21,sF26),sF14)
| spl27_42 ),
inference(forward_subsumption_resolution,[],[f721,f522]) ).
fof(f16411,plain,
( $false
| spl27_34
| spl27_42 ),
inference(forward_subsumption_resolution,[],[f16402,f445]) ).
fof(f16412,plain,
( spl27_34
| spl27_42 ),
inference(avatar_contradiction_clause,[],[f16411]) ).
fof(f16531,plain,
( ~ mem(sF8,sF23)
| ~ spl27_5
| spl27_290 ),
inference(superposition,[],[f7010,f226]) ).
fof(f16545,plain,
( $false
| ~ spl27_5
| spl27_290 ),
inference(forward_subsumption_resolution,[],[f16531,f10232]) ).
fof(f16546,plain,
( ~ spl27_5
| spl27_290 ),
inference(avatar_contradiction_clause,[],[f16545]) ).
fof(f27782,plain,
( sF3 = sK0(sF21,sF26)
| ~ spl27_190 ),
inference(resolution,[],[f2603,f127]) ).
fof(f27787,plain,
( $false
| spl27_9
| ~ spl27_190 ),
inference(forward_subsumption_resolution,[],[f27782,f243]) ).
fof(f27788,plain,
( spl27_9
| ~ spl27_190 ),
inference(avatar_contradiction_clause,[],[f27787]) ).
fof(f27791,plain,
( spl27_191
| ~ spl27_32
| spl27_48
| spl27_190 ),
inference(avatar_split_clause,[],[f15526,f2601,f627,f425,f2605]) ).
fof(f27866,plain,
( sF4 = sK0(sF21,sF26)
| ~ spl27_191 ),
inference(resolution,[],[f2607,f128]) ).
fof(f27871,plain,
( $false
| spl27_1
| ~ spl27_191 ),
inference(forward_subsumption_resolution,[],[f27866,f207]) ).
fof(f27872,plain,
( spl27_1
| ~ spl27_191 ),
inference(avatar_contradiction_clause,[],[f27871]) ).
fof(f27956,plain,
( ~ mem(sF4,sF23)
| ~ spl27_1
| spl27_290 ),
inference(superposition,[],[f7010,f208]) ).
fof(f27958,plain,
( ~ subq(sF4,sF8)
| ~ spl27_1
| spl27_294 ),
inference(superposition,[],[f7026,f208]) ).
fof(f27986,plain,
( $false
| ~ spl27_1
| ~ spl27_146
| spl27_290 ),
inference(forward_subsumption_resolution,[],[f27956,f1938]) ).
fof(f27987,plain,
( ~ spl27_1
| ~ spl27_146
| spl27_290 ),
inference(avatar_contradiction_clause,[],[f27986]) ).
fof(f28012,plain,
( subq(sF4,sF8)
| ~ spl27_141
| ~ spl27_145 ),
inference(forward_subsumption_resolution,[],[f12288,f1874]) ).
fof(f28013,plain,
( $false
| ~ spl27_1
| ~ spl27_141
| ~ spl27_145
| spl27_294 ),
inference(forward_subsumption_resolution,[],[f28012,f27958]) ).
fof(f28014,plain,
( ~ spl27_1
| ~ spl27_141
| ~ spl27_145
| spl27_294 ),
inference(avatar_contradiction_clause,[],[f28013]) ).
fof(f28019,plain,
( $false
| spl27_141 ),
inference(forward_subsumption_resolution,[],[f10231,f1873]) ).
fof(f28020,plain,
spl27_141,
inference(avatar_contradiction_clause,[],[f28019]) ).
fof(f28435,plain,
( ~ mem(sF3,sF25)
| subq(sF21,sF26)
| ~ spl27_9 ),
inference(superposition,[],[f1259,f244]) ).
fof(f28441,plain,
( subq(sF21,sF26)
| ~ spl27_9
| ~ spl27_28 ),
inference(forward_subsumption_resolution,[],[f28435,f1478]) ).
fof(f28464,plain,
( $false
| ~ spl27_9
| ~ spl27_28 ),
inference(forward_subsumption_resolution,[],[f28441,f114]) ).
fof(f28465,plain,
( ~ spl27_9
| ~ spl27_28 ),
inference(avatar_contradiction_clause,[],[f28464]) ).
fof(f28470,plain,
( $false
| spl27_28 ),
inference(forward_subsumption_resolution,[],[f8109,f394]) ).
fof(f28471,plain,
spl27_28,
inference(avatar_contradiction_clause,[],[f28470]) ).
cnf(s32,plain,
( spl27_11
| ~ spl27_48 ),
inference(sat_conversion,[],[f660]) ).
cnf(s98,plain,
~ spl27_36,
inference(sat_conversion,[],[f1725]) ).
cnf(s107,plain,
( spl27_36
| ~ spl27_40 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s108,plain,
( ~ spl27_38
| spl27_40 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s109,plain,
( spl27_145
| spl27_146 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s133,plain,
( ~ spl27_11
| spl27_38 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s142,plain,
( spl27_40
| ~ spl27_54 ),
inference(sat_conversion,[],[f2579]) ).
cnf(s143,plain,
( ~ spl27_34
| spl27_54
| spl27_55 ),
inference(sat_conversion,[],[f2581]) ).
cnf(s146,plain,
( spl27_32
| ~ spl27_42
| spl27_193 ),
inference(sat_conversion,[],[f2620]) ).
cnf(s838,plain,
( ~ spl27_55
| spl27_291
| spl27_301 ),
inference(sat_conversion,[],[f16003]) ).
cnf(s841,plain,
~ spl27_193,
inference(sat_conversion,[],[f16027]) ).
cnf(s845,plain,
( spl27_36
| ~ spl27_296 ),
inference(sat_conversion,[],[f16152]) ).
cnf(s846,plain,
( ~ spl27_290
| spl27_296 ),
inference(sat_conversion,[],[f16155]) ).
cnf(s847,plain,
( spl27_290
| ~ spl27_294 ),
inference(sat_conversion,[],[f16157]) ).
cnf(s848,plain,
( spl27_5
| ~ spl27_301 ),
inference(sat_conversion,[],[f16246]) ).
cnf(s849,plain,
( ~ spl27_291
| spl27_296 ),
inference(sat_conversion,[],[f16248]) ).
cnf(s873,plain,
( spl27_34
| spl27_42 ),
inference(sat_conversion,[],[f16412]) ).
cnf(s877,plain,
( ~ spl27_5
| spl27_290 ),
inference(sat_conversion,[],[f16546]) ).
cnf(s1437,plain,
( spl27_9
| ~ spl27_190 ),
inference(sat_conversion,[],[f27788]) ).
cnf(s1439,plain,
( ~ spl27_32
| spl27_48
| spl27_190
| spl27_191 ),
inference(sat_conversion,[],[f27791]) ).
cnf(s1440,plain,
( spl27_1
| ~ spl27_191 ),
inference(sat_conversion,[],[f27872]) ).
cnf(s1444,plain,
( ~ spl27_1
| ~ spl27_146
| spl27_290 ),
inference(sat_conversion,[],[f27987]) ).
cnf(s1451,plain,
( ~ spl27_1
| ~ spl27_141
| ~ spl27_145
| spl27_294 ),
inference(sat_conversion,[],[f28014]) ).
cnf(s1453,plain,
spl27_141,
inference(sat_conversion,[],[f28020]) ).
cnf(s1472,plain,
( ~ spl27_9
| ~ spl27_28 ),
inference(sat_conversion,[],[f28465]) ).
cnf(s1474,plain,
spl27_28,
inference(sat_conversion,[],[f28471]) ).
cnf(s1478,plain,
~ spl27_9,
inference(rat,[],[s1472,s1474]) ).
cnf(s1479,plain,
( ~ spl27_1
| ~ spl27_145
| spl27_294 ),
inference(rat,[],[s1451,s1453]) ).
cnf(s1480,plain,
~ spl27_190,
inference(rat,[],[s1437,s1478]) ).
cnf(s1503,plain,
( spl27_32
| ~ spl27_42 ),
inference(rat,[],[s146,s841]) ).
cnf(s1521,plain,
~ spl27_296,
inference(rat,[],[s845,s98]) ).
cnf(s1526,plain,
~ spl27_40,
inference(rat,[],[s107,s98]) ).
cnf(s1527,plain,
~ spl27_291,
inference(rat,[],[s849,s1521]) ).
cnf(s1528,plain,
~ spl27_290,
inference(rat,[],[s846,s1521]) ).
cnf(s1538,plain,
~ spl27_54,
inference(rat,[],[s142,s1526]) ).
cnf(s1539,plain,
~ spl27_38,
inference(rat,[],[s108,s1526]) ).
cnf(s1540,plain,
~ spl27_5,
inference(rat,[],[s877,s1528]) ).
cnf(s1541,plain,
~ spl27_294,
inference(rat,[],[s847,s1528]) ).
cnf(s1546,plain,
~ spl27_11,
inference(rat,[],[s133,s1539]) ).
cnf(s1548,plain,
~ spl27_301,
inference(rat,[],[s848,s1540]) ).
cnf(s1557,plain,
~ spl27_55,
inference(rat,[],[s838,s1527,s1548]) ).
cnf(s1561,plain,
~ spl27_34,
inference(rat,[],[s143,s1538,s1557]) ).
cnf(s1563,plain,
spl27_42,
inference(rat,[],[s873,s1561]) ).
cnf(s1565,plain,
spl27_32,
inference(rat,[],[s1503,s1563]) ).
cnf(s1578,plain,
~ spl27_48,
inference(rat,[],[s32,s1546]) ).
cnf(s1579,plain,
spl27_191,
inference(rat,[],[s1439,s1565,s1480,s1578]) ).
cnf(s1580,plain,
spl27_1,
inference(rat,[],[s1440,s1579]) ).
cnf(s1581,plain,
~ spl27_145,
inference(rat,[],[s1479,s1541,s1580]) ).
cnf(s1582,plain,
~ spl27_146,
inference(rat,[],[s1444,s1528,s1580]) ).
cnf(s1584,plain,
$false,
inference(rat,[],[s109,s1582,s1581]) ).
fof(f28486,plain,
$false,
inference(avatar_sat_refutation,[],[s1584]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV578+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 28 06:38:55 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 Running first-order model finding
% 0.09/0.38 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.45/1.55 % (3772178)Will run a generic schedule for satisfiability detection.
% 7.45/1.55 % (3772185)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=262547611:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.45/1.55 % (3772184)% WARNING: option uhcvi not known.
% 7.45/1.55 % (3772183)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2157528025_2999 on theBenchmark for (2999ds/0Mi)
% 7.45/1.55 % (3772187)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2346491543:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.45/1.55 % (3772184)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3809044695:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.45/1.55 % (3772189)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2144246210:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.45/1.55 % (3772186)dis+10_1_sil=32000:sp=arity:random_seed=3320099340:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.45/1.55 % (3772188)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=930470896:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.45/1.55 % TRYING [1]
% 7.45/1.55 % TRYING [2]
% 7.45/1.55 % TRYING [3]
% 7.45/1.55 % TRYING [4]
% 7.45/1.55 % TRYING [5]
% 7.45/1.55 % TRYING [6]
% 7.45/1.55 % TRYING [7]
% 7.45/1.55 % TRYING [8]
% 7.45/1.55 % (3772186)Instruction limit reached!
% 7.45/1.55 % (3772186)------------------------------
% 7.45/1.55 % (3772186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772186)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772186)Termination reason: Instruction limit
% 7.45/1.55 % (3772186)Termination phase: Saturation
% 7.45/1.55 % (3772186)Time elapsed: 0.063 s
% 7.45/1.55 % (3772186)Peak memory usage: 12 MB
% 7.45/1.55 % (3772186)Instructions burned: 105 (million)
% 7.45/1.55 % (3772187)Instruction limit reached!
% 7.45/1.55 % (3772187)------------------------------
% 7.45/1.55 % (3772187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772187)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772187)Termination reason: Instruction limit
% 7.45/1.55 % (3772187)Termination phase: Saturation
% 7.45/1.55 % (3772187)Time elapsed: 0.071 s
% 7.45/1.55 % (3772187)Peak memory usage: 12 MB
% 7.45/1.55 % (3772187)Instructions burned: 117 (million)
% 7.45/1.55 % (3772197)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2735571748:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.45/1.55 % (3772188)Instruction limit reached!
% 7.45/1.55 % (3772188)------------------------------
% 7.45/1.55 % (3772188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772188)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772188)Termination reason: Instruction limit
% 7.45/1.55 % (3772188)Termination phase: Saturation
% 7.45/1.55 % (3772188)Time elapsed: 0.083 s
% 7.45/1.55 % (3772188)Peak memory usage: 13 MB
% 7.45/1.55 % (3772188)Instructions burned: 131 (million)
% 7.45/1.55 % TRYING [1]
% 7.45/1.55 % TRYING [2]
% 7.45/1.55 % TRYING [3]
% 7.45/1.55 % TRYING [4]
% 7.45/1.55 % (3772198)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1830977522:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.45/1.55 % TRYING [5]
% 7.45/1.55 % (3772189)Instruction limit reached!
% 7.45/1.55 % (3772189)------------------------------
% 7.45/1.55 % (3772189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772189)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772189)Termination reason: Instruction limit
% 7.45/1.55 % (3772189)Termination phase: Saturation
% 7.45/1.55 % (3772189)Time elapsed: 0.095 s
% 7.45/1.55 % (3772189)Peak memory usage: 12 MB
% 7.45/1.55 % (3772189)Instructions burned: 159 (million)
% 7.45/1.55 % (3772200)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4020152147:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.45/1.55 % TRYING [6]
% 7.45/1.55 % (3772202)ott-21_1_sil=16000:fs=off:random_seed=1848389382:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.45/1.55 % TRYING [7]
% 7.45/1.55 % TRYING [9]
% 7.45/1.55 % (3772198)Instruction limit reached!
% 7.45/1.55 % (3772198)------------------------------
% 7.45/1.55 % (3772198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772198)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772198)Termination reason: Instruction limit
% 7.45/1.55 % (3772198)Termination phase: Saturation
% 7.45/1.55 % (3772198)Time elapsed: 0.083 s
% 7.45/1.55 % (3772198)Peak memory usage: 13 MB
% 7.45/1.55 % (3772198)Instructions burned: 132 (million)
% 7.45/1.55 % (3772205)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2345029127:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 7.45/1.55 % TRYING [8]
% 7.45/1.55 % (3772202)Instruction limit reached!
% 7.45/1.55 % (3772202)------------------------------
% 7.45/1.55 % (3772202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772202)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772202)Termination reason: Instruction limit
% 7.45/1.55 % (3772202)Termination phase: Saturation
% 7.45/1.55 % (3772202)Time elapsed: 0.094 s
% 7.45/1.55 % (3772202)Peak memory usage: 13 MB
% 7.45/1.55 % (3772202)Instructions burned: 182 (million)
% 7.45/1.55 % (3772207)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3207259615:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 7.45/1.55 % TRYING [1]
% 7.45/1.55 % TRYING [2]
% 7.45/1.55 % TRYING [3]
% 7.45/1.55 % TRYING [4]
% 7.45/1.55 % TRYING [5]
% 7.45/1.55 % TRYING [6]
% 7.45/1.55 % TRYING [7]
% 7.45/1.55 % (3772197)Instruction limit reached!
% 7.45/1.55 % (3772197)------------------------------
% 7.45/1.55 % (3772197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772197)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772197)Termination reason: Instruction limit
% 7.45/1.55 % (3772197)Termination phase: Finite model building SAT solving
% 7.45/1.55 % (3772197)Time elapsed: 0.366 s
% 7.45/1.55 % (3772197)Peak memory usage: 19 MB
% 7.45/1.55 % (3772197)Instructions burned: 714 (million)
% 7.45/1.55 % (3772209)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2646445913:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 7.45/1.55 % TRYING [8]
% 7.45/1.55 % TRYING [10]
% 7.45/1.55 % (3772200)Instruction limit reached!
% 7.45/1.55 % (3772200)------------------------------
% 7.45/1.55 % (3772200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772200)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772200)Termination reason: Instruction limit
% 7.45/1.55 % (3772200)Termination phase: Saturation
% 7.45/1.55 % (3772200)Time elapsed: 0.400 s
% 7.45/1.55 % (3772200)Peak memory usage: 18 MB
% 7.45/1.55 % (3772200)Instructions burned: 684 (million)
% 7.45/1.55 % (3772205)Instruction limit reached!
% 7.45/1.55 % (3772205)------------------------------
% 7.45/1.55 % (3772205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772205)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772205)Termination reason: Instruction limit
% 7.45/1.55 % (3772205)Termination phase: Saturation
% 7.45/1.55 % (3772205)Time elapsed: 0.313 s
% 7.45/1.55 % (3772205)Peak memory usage: 14 MB
% 7.45/1.55 % (3772205)Instructions burned: 478 (million)
% 7.45/1.55 % (3772211)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=610484845:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 7.45/1.55 % (3772212)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3064870155:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 7.45/1.55 % TRYING [14]
% 7.45/1.55 % (3772207)Instruction limit reached!
% 7.45/1.55 % (3772207)------------------------------
% 7.45/1.55 % (3772207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772207)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772207)Termination reason: Instruction limit
% 7.45/1.55 % (3772207)Termination phase: Finite model building SAT solving
% 7.45/1.55 % (3772207)Time elapsed: 0.312 s
% 7.45/1.55 % (3772207)Peak memory usage: 17 MB
% 7.45/1.55 % (3772207)Instructions burned: 866 (million)
% 7.45/1.55 % (3772215)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4165565106:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 7.45/1.55 % (3772211)Instruction limit reached!
% 7.45/1.55 % (3772211)------------------------------
% 7.45/1.55 % (3772211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772211)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772211)Termination reason: Instruction limit
% 7.45/1.55 % (3772211)Termination phase: Finite model building SAT solving
% 7.45/1.55 % (3772211)Time elapsed: 0.340 s
% 7.45/1.55 % (3772211)Peak memory usage: 41 MB
% 7.45/1.55 % (3772211)Instructions burned: 890 (million)
% 7.45/1.55 % (3772217)fmb+10_1_sil=64000:random_seed=3145194518:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 7.45/1.55 % TRYING [1]
% 7.45/1.55 % TRYING [2]
% 7.45/1.55 % TRYING [3]
% 7.45/1.55 % TRYING [4]
% 7.45/1.55 % TRYING [5]
% 7.45/1.55 % TRYING [6]
% 7.45/1.55 % (3772212)Instruction limit reached!
% 7.45/1.55 % (3772212)------------------------------
% 7.45/1.55 % (3772212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772212)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772212)Termination reason: Instruction limit
% 7.45/1.55 % (3772212)Termination phase: Saturation
% 7.45/1.55 % (3772212)Time elapsed: 0.410 s
% 7.45/1.55 % (3772212)Peak memory usage: 19 MB
% 7.45/1.55 % (3772212)Instructions burned: 692 (million)
% 7.45/1.55 % (3772219)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4102344013:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 7.45/1.55 % TRYING [20]
% 7.45/1.55 % TRYING [7]
% 7.45/1.55 % TRYING [8]
% 7.45/1.55 % (3772215)Instruction limit reached!
% 7.45/1.55 % (3772215)------------------------------
% 7.45/1.55 % (3772215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.55 % (3772215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.55 % (3772215)CaDiCaL version: 2.1.3
% 7.45/1.55 % (3772215)Termination reason: Instruction limit
% 7.45/1.55 % (3772215)Termination phase: Saturation
% 7.45/1.55 % (3772215)Time elapsed: 0.480 s
% 7.45/1.55 % (3772215)Peak memory usage: 18 MB
% 7.45/1.55 % (3772215)Instructions burned: 880 (million)
% 7.45/1.55 % (3772221)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2153319467:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 7.45/1.55 % TRYING [8]
% 7.45/1.55 % (3772209) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3772178-3772209"...
% 7.45/1.55 % (3772209)...printing done.
% 7.45/1.55 % (3772209)Refutation found. Thanks to Tanya!
% 7.45/1.55 % SZS status Theorem for theBenchmark
% 7.45/1.55 % SZS output start Proof for theBenchmark
% See solution above
% 7.45/1.56 % (3772209)------------------------------
% 7.45/1.56 % (3772209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.56 % (3772209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.56 % (3772209)CaDiCaL version: 2.1.3
% 7.45/1.56 % (3772209)Termination reason: Refutation
% 7.45/1.56 % (3772209)Time elapsed: 0.643 s
% 7.45/1.56 % (3772209)Peak memory usage: 23 MB
% 7.45/1.56 % (3772209)Instructions burned: 1076 (million)
% 7.45/1.56 % (3772178)Success in time 1.159 s
% 7.45/1.56 % Vampire exiting
%------------------------------------------------------------------------------