%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV566+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:29 PM UTC 2026
% Result : Theorem 47.12s 7.09s
% Output : Refutation 47.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 23
% Syntax : Number of formulae : 183 ( 42 unt; 13 def)
% Number of atoms : 393 ( 31 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 365 ( 155 ~; 171 |; 17 &)
% ( 19 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 14 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-2 aty)
% Number of variables : 178 ( 0 sgn 176 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subq(X0,X1)
<=> ! [X2] :
( mem(X2,X0)
=> mem(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',subq_def) ).
fof(f2,axiom,
! [X0,X1] :
( subq(X0,X1)
=> ( subq(X1,X0)
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',setext) ).
fof(f4,axiom,
! [X0] : ~ mem(X0,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',e_ax) ).
fof(f5,axiom,
! [X0,X1] :
( mem(X0,s(X1))
<=> X0 = X1 ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET010+0.ax',u_ax) ).
fof(f7,axiom,
! [X0,X1,X2] :
( mem(X0,m(X1,X2))
<=> ( mem(X0,X1)
& ~ mem(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',m_ax) ).
fof(f8,axiom,
! [X0,X1] : a(X0,X1) = u(X0,s(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',a_def) ).
fof(f9,axiom,
! [X0] : n(X0) = a(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',n_def) ).
fof(f10,axiom,
! [X0,X1] :
( mem(X0,p(X1))
<=> subq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax',p_ax) ).
fof(f26,conjecture,
~ subq(u(m(p(u(n(e),n(s(n(e))))),n(p(s(n(e))))),s(a(s(n(e)),n(n(e))))),u(m(p(u(n(e),n(s(n(e))))),u(s(n(e)),n(p(s(n(e)))))),s(a(s(n(e)),n(n(e)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nsubq_1242_1240) ).
fof(f27,negated_conjecture,
~ ~ subq(u(m(p(u(n(e),n(s(n(e))))),n(p(s(n(e))))),s(a(s(n(e)),n(n(e))))),u(m(p(u(n(e),n(s(n(e))))),u(s(n(e)),n(p(s(n(e)))))),s(a(s(n(e)),n(n(e)))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
subq(u(m(p(u(n(e),n(s(n(e))))),n(p(s(n(e))))),s(a(s(n(e)),n(n(e))))),u(m(p(u(n(e),n(s(n(e))))),u(s(n(e)),n(p(s(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(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] :
( ~ subq(X0,X1)
| ~ mem(X3,X0)
| mem(X3,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(X0,X1)
| ~ subq(X1,X0)
| 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))))),n(p(s(n(e))))),s(a(s(n(e)),n(n(e))))),u(m(p(u(n(e),n(s(n(e))))),u(s(n(e)),n(p(s(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(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(p(s(u(e,s(e))))))),s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))))),u(m(p(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),u(s(u(e,s(e))),u(p(s(u(e,s(e)))),s(p(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,f59,f59,f54,f59,f59,f59,f59,f59,f59,f59,f59,f59,f54,f59,f59,f59]) ).
fof(f61,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f47]) ).
fof(f64,plain,
! [X0] : subq(e,X0),
inference(resolution,[],[f42,f45]) ).
fof(f67,plain,
! [X0] :
( subq(X0,X0)
| subq(X0,X0) ),
inference(resolution,[],[f43,f42]) ).
fof(f69,plain,
! [X0] : subq(X0,X0),
inference(duplicate_literal_removal,[],[f67]) ).
fof(f70,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X2)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f49,f43]) ).
fof(f71,plain,
! [X2,X0,X1] :
( ~ mem(sK0(X0,u(X1,X2)),X1)
| subq(X0,u(X1,X2)) ),
inference(resolution,[],[f50,f43]) ).
fof(f72,plain,
! [X2,X0,X1] :
( ~ mem(sK0(m(X0,X1),X2),X1)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f51,f42]) ).
fof(f73,plain,
! [X2,X0,X1] :
( mem(sK0(m(X0,X1),X2),X0)
| subq(m(X0,X1),X2) ),
inference(resolution,[],[f52,f42]) ).
fof(f74,plain,
! [X0] :
( mem(X0,u(m(p(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),u(s(u(e,s(e))),u(p(s(u(e,s(e)))),s(p(s(u(e,s(e)))))))),s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))))))
| ~ mem(X0,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(p(s(u(e,s(e))))))),s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e))))))))) ),
inference(resolution,[],[f41,f60]) ).
fof(f79,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(f81,plain,
! [X0] :
( ~ subq(X0,e)
| e = X0 ),
inference(resolution,[],[f44,f64]) ).
fof(f94,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(f107,plain,
! [X0] :
( ~ mem(X0,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(p(s(u(e,s(e))))))),s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))))))
| mem(X0,s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e))))))))
| mem(X0,m(p(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),u(s(u(e,s(e))),u(p(s(u(e,s(e)))),s(p(s(u(e,s(e))))))))) ),
inference(resolution,[],[f74,f48]) ).
fof(f121,plain,
! [X0,X1] :
( subq(X0,u(X1,X0))
| subq(X0,u(X1,X0)) ),
inference(resolution,[],[f70,f42]) ).
fof(f127,plain,
! [X0,X1] : subq(X0,u(X1,X0)),
inference(duplicate_literal_removal,[],[f121]) ).
fof(f135,plain,
! [X0,X1] :
( subq(X0,u(X0,X1))
| subq(X0,u(X0,X1)) ),
inference(resolution,[],[f71,f42]) ).
fof(f141,plain,
! [X0,X1] : subq(X0,u(X0,X1)),
inference(duplicate_literal_removal,[],[f135]) ).
fof(f151,plain,
! [X2,X3,X0,X1] :
( ~ mem(sK0(m(X0,u(X1,X2)),X3),X1)
| subq(m(X0,u(X1,X2)),X3) ),
inference(resolution,[],[f72,f50]) ).
fof(f157,plain,
! [X0,X1] :
( subq(m(X0,X1),X0)
| subq(m(X0,X1),X0) ),
inference(resolution,[],[f73,f43]) ).
fof(f161,plain,
! [X2,X0,X1] :
( subq(m(s(X0),X1),X2)
| sK0(m(s(X0),X1),X2) = X0 ),
inference(resolution,[],[f73,f46]) ).
fof(f168,plain,
! [X0,X1] : subq(m(X0,X1),X0),
inference(duplicate_literal_removal,[],[f157]) ).
fof(f170,plain,
! [X0,X1] :
( ~ subq(u(X0,X1),X1)
| u(X0,X1) = X1 ),
inference(resolution,[],[f127,f44]) ).
fof(f184,plain,
! [X0,X1] :
( mem(sK0(u(e,X0),X1),X0)
| subq(u(e,X0),X1) ),
inference(resolution,[],[f79,f45]) ).
fof(f199,plain,
! [X0,X1] :
( mem(sK0(X0,m(X0,X1)),X1)
| subq(X0,m(X0,X1))
| subq(X0,m(X0,X1)) ),
inference(resolution,[],[f94,f42]) ).
fof(f200,plain,
! [X2,X0,X1] :
( mem(sK0(m(X0,X1),m(X0,X2)),X2)
| subq(m(X0,X1),m(X0,X2))
| subq(m(X0,X1),m(X0,X2)) ),
inference(resolution,[],[f94,f73]) ).
fof(f210,plain,
! [X2,X0,X1] :
( mem(sK0(m(X0,X1),m(X0,X2)),X2)
| subq(m(X0,X1),m(X0,X2)) ),
inference(duplicate_literal_removal,[],[f200]) ).
fof(f211,plain,
! [X0,X1] :
( mem(sK0(X0,m(X0,X1)),X1)
| subq(X0,m(X0,X1)) ),
inference(duplicate_literal_removal,[],[f199]) ).
fof(f218,plain,
! [X0,X1] :
( ~ subq(X0,m(X0,X1))
| m(X0,X1) = X0 ),
inference(resolution,[],[f168,f44]) ).
fof(f271,plain,
! [X0] :
( mem(X0,m(p(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),u(s(u(e,s(e))),u(p(s(u(e,s(e)))),s(p(s(u(e,s(e)))))))))
| mem(X0,s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e))))))))
| ~ mem(X0,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(p(s(u(e,s(e)))))))) ),
inference(resolution,[],[f107,f50]) ).
fof(f319,plain,
! [X0] :
( subq(u(e,X0),X0)
| subq(u(e,X0),X0) ),
inference(resolution,[],[f184,f43]) ).
fof(f335,plain,
! [X0] : subq(u(e,X0),X0),
inference(duplicate_literal_removal,[],[f319]) ).
fof(f401,plain,
! [X0] : subq(X0,m(X0,e)),
inference(resolution,[],[f211,f45]) ).
fof(f668,plain,
! [X2,X0,X1] :
( subq(m(X0,u(X0,X1)),X2)
| subq(m(X0,u(X0,X1)),X2) ),
inference(resolution,[],[f151,f73]) ).
fof(f679,plain,
! [X2,X0,X1] : subq(m(X0,u(X0,X1)),X2),
inference(duplicate_literal_removal,[],[f668]) ).
fof(f682,plain,
! [X0,X1] : e = m(X0,u(X0,X1)),
inference(resolution,[],[f679,f81]) ).
fof(f4689,plain,
! [X0] :
( ~ mem(X0,u(s(u(e,s(e))),u(p(s(u(e,s(e)))),s(p(s(u(e,s(e))))))))
| ~ mem(X0,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(p(s(u(e,s(e))))))))
| mem(X0,s(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))))) ),
inference(resolution,[],[f271,f51]) ).
fof(f4758,plain,
! [X0] : u(e,X0) = X0,
inference(resolution,[],[f170,f335]) ).
fof(f4910,plain,
! [X0] :
( ~ mem(X0,u(s(s(e)),u(p(s(s(e))),s(p(s(s(e)))))))
| ~ mem(X0,m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e)))))))
| mem(X0,s(u(s(s(e)),s(u(s(e),s(s(e))))))) ),
inference(superposition,[],[f4689,f4758]) ).
fof(f5181,plain,
! [X0] : m(X0,e) = X0,
inference(resolution,[],[f218,f401]) ).
fof(f5569,plain,
! [X0] :
( ~ mem(X0,s(s(e)))
| mem(X0,s(u(s(s(e)),s(u(s(e),s(s(e)))))))
| ~ mem(X0,m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e))))))) ),
inference(resolution,[],[f4910,f50]) ).
fof(f5677,plain,
( mem(s(e),s(u(s(s(e)),s(u(s(e),s(s(e)))))))
| ~ mem(s(e),m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e))))))) ),
inference(resolution,[],[f5569,f61]) ).
fof(f5753,definition,
( spl1_8
<=> mem(s(e),m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e))))))) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f5755,plain,
( ~ mem(s(e),m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e)))))))
| spl1_8 ),
inference(avatar_component_clause,[],[f5753]) ).
fof(f5757,definition,
( spl1_9
<=> mem(s(e),s(u(s(s(e)),s(u(s(e),s(s(e))))))) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
fof(f5759,plain,
( mem(s(e),s(u(s(s(e)),s(u(s(e),s(s(e)))))))
| ~ spl1_9 ),
inference(avatar_component_clause,[],[f5757]) ).
fof(f5832,plain,
( mem(s(e),s(u(s(s(e)),s(u(s(e),s(s(e)))))))
| ~ mem(s(e),m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e))))))) ),
inference(global_subsumption,[],[f5677]) ).
fof(f5873,plain,
( ~ mem(s(e),m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e)))))))
| mem(s(e),s(u(s(s(e)),s(u(s(e),s(s(e))))))) ),
inference(global_subsumption,[],[f5832]) ).
fof(f5879,plain,
( ~ mem(s(e),m(p(u(s(e),u(s(s(e)),s(s(s(e)))))),u(p(s(s(e))),s(p(s(s(e)))))))
| mem(s(e),s(u(s(s(e)),s(u(s(e),s(s(e))))))) ),
inference(global_subsumption,[],[f5873]) ).
fof(f5880,plain,
( spl1_9
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f5879,f5753,f5757]) ).
fof(f5920,plain,
( ~ mem(s(e),p(u(s(e),u(s(s(e)),s(s(s(e)))))))
| mem(s(e),u(p(s(s(e))),s(p(s(s(e))))))
| spl1_8 ),
inference(resolution,[],[f5755,f53]) ).
fof(f5924,definition,
( spl1_10
<=> mem(s(e),u(p(s(s(e))),s(p(s(s(e)))))) ),
introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition]) ).
fof(f5926,plain,
( mem(s(e),u(p(s(s(e))),s(p(s(s(e))))))
| ~ spl1_10 ),
inference(avatar_component_clause,[],[f5924]) ).
fof(f5928,definition,
( spl1_11
<=> mem(s(e),p(u(s(e),u(s(s(e)),s(s(s(e))))))) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
fof(f5930,plain,
( ~ mem(s(e),p(u(s(e),u(s(s(e)),s(s(s(e)))))))
| spl1_11 ),
inference(avatar_component_clause,[],[f5928]) ).
fof(f5931,plain,
( spl1_10
| ~ spl1_11
| spl1_8 ),
inference(avatar_split_clause,[],[f5920,f5753,f5928,f5924]) ).
fof(f5971,plain,
( ~ subq(s(e),u(s(e),u(s(s(e)),s(s(s(e))))))
| spl1_11 ),
inference(resolution,[],[f5930,f57]) ).
fof(f6014,plain,
( $false
| spl1_11 ),
inference(resolution,[],[f5971,f141]) ).
fof(f6016,plain,
spl1_11,
inference(avatar_contradiction_clause,[],[f6014]) ).
fof(f6057,plain,
( s(e) = u(s(s(e)),s(u(s(e),s(s(e)))))
| ~ spl1_9 ),
inference(resolution,[],[f5759,f46]) ).
fof(f6163,plain,
( e = m(s(s(e)),s(e))
| ~ spl1_9 ),
inference(superposition,[],[f682,f6057]) ).
fof(f6231,definition,
( spl1_13
<=> subq(s(e),s(s(e))) ),
introduced(definition,[new_symbols(definition,[spl1_13])],[avatar_definition]) ).
fof(f6232,plain,
( subq(s(e),s(s(e)))
| ~ spl1_13 ),
inference(avatar_component_clause,[],[f6231]) ).
fof(f6275,definition,
( spl1_16
<=> mem(e,s(s(e))) ),
introduced(definition,[new_symbols(definition,[spl1_16])],[avatar_definition]) ).
fof(f6276,plain,
( ~ mem(e,s(s(e)))
| spl1_16 ),
inference(avatar_component_clause,[],[f6275]) ).
fof(f6277,plain,
( mem(e,s(s(e)))
| ~ spl1_16 ),
inference(avatar_component_clause,[],[f6275]) ).
fof(f6345,definition,
( spl1_28
<=> e = s(e) ),
introduced(definition,[new_symbols(definition,[spl1_28])],[avatar_definition]) ).
fof(f6347,plain,
( e = s(e)
| ~ spl1_28 ),
inference(avatar_component_clause,[],[f6345]) ).
fof(f6379,plain,
( mem(s(e),s(p(s(s(e)))))
| mem(s(e),p(s(s(e))))
| ~ spl1_10 ),
inference(resolution,[],[f5926,f48]) ).
fof(f6382,definition,
( spl1_30
<=> mem(s(e),p(s(s(e)))) ),
introduced(definition,[new_symbols(definition,[spl1_30])],[avatar_definition]) ).
fof(f6384,plain,
( mem(s(e),p(s(s(e))))
| ~ spl1_30 ),
inference(avatar_component_clause,[],[f6382]) ).
fof(f6386,definition,
( spl1_31
<=> mem(s(e),s(p(s(s(e))))) ),
introduced(definition,[new_symbols(definition,[spl1_31])],[avatar_definition]) ).
fof(f6388,plain,
( mem(s(e),s(p(s(s(e)))))
| ~ spl1_31 ),
inference(avatar_component_clause,[],[f6386]) ).
fof(f6389,plain,
( spl1_30
| spl1_31
| ~ spl1_10 ),
inference(avatar_split_clause,[],[f6379,f5924,f6386,f6382]) ).
fof(f6413,plain,
( e = s(e)
| ~ spl1_16 ),
inference(resolution,[],[f6277,f46]) ).
fof(f6415,plain,
( spl1_28
| ~ spl1_16 ),
inference(avatar_split_clause,[],[f6413,f6275,f6345]) ).
fof(f6482,plain,
( mem(e,e)
| ~ spl1_28 ),
inference(superposition,[],[f61,f6347]) ).
fof(f6662,plain,
( $false
| ~ spl1_28 ),
inference(resolution,[],[f6482,f45]) ).
fof(f6664,plain,
~ spl1_28,
inference(avatar_contradiction_clause,[],[f6662]) ).
fof(f6925,plain,
( ! [X0] :
( mem(sK0(m(s(s(e)),X0),e),s(e))
| subq(m(s(s(e)),X0),e) )
| ~ spl1_9 ),
inference(superposition,[],[f210,f6163]) ).
fof(f6951,plain,
( ! [X0] :
( mem(s(e),s(e))
| subq(m(s(s(e)),X0),e) )
| ~ spl1_9 ),
inference(forward_subsumption_demodulation,[],[f6925,f161]) ).
fof(f6957,definition,
( spl1_32
<=> subq(s(s(e)),e) ),
introduced(definition,[new_symbols(definition,[spl1_32])],[avatar_definition]) ).
fof(f6958,plain,
( ~ subq(s(s(e)),e)
| spl1_32 ),
inference(avatar_component_clause,[],[f6957]) ).
fof(f6959,plain,
( subq(s(s(e)),e)
| ~ spl1_32 ),
inference(avatar_component_clause,[],[f6957]) ).
fof(f6961,definition,
( spl1_33
<=> mem(s(e),s(e)) ),
introduced(definition,[new_symbols(definition,[spl1_33])],[avatar_definition]) ).
fof(f6963,plain,
( mem(s(e),s(e))
| ~ spl1_33 ),
inference(avatar_component_clause,[],[f6961]) ).
fof(f6966,definition,
( spl1_34
<=> ! [X0] : subq(m(s(s(e)),X0),e) ),
introduced(definition,[new_symbols(definition,[spl1_34])],[avatar_definition]) ).
fof(f6967,plain,
( ! [X0] : subq(m(s(s(e)),X0),e)
| ~ spl1_34 ),
inference(avatar_component_clause,[],[f6966]) ).
fof(f6968,plain,
( spl1_34
| spl1_33
| ~ spl1_9 ),
inference(avatar_split_clause,[],[f6951,f5757,f6961,f6966]) ).
fof(f7004,plain,
( e = s(e)
| ~ spl1_33 ),
inference(resolution,[],[f6963,f46]) ).
fof(f7006,plain,
( spl1_28
| ~ spl1_33 ),
inference(avatar_split_clause,[],[f7004,f6961,f6345]) ).
fof(f7035,plain,
( ! [X0] :
( ~ mem(X0,s(s(e)))
| mem(X0,e) )
| ~ spl1_32 ),
inference(resolution,[],[f6959,f41]) ).
fof(f7037,plain,
( ! [X0] : ~ mem(X0,s(s(e)))
| ~ spl1_32 ),
inference(global_subsumption,[],[f7035,f45]) ).
fof(f7039,definition,
( spl1_37
<=> e = s(s(e)) ),
introduced(definition,[new_symbols(definition,[spl1_37])],[avatar_definition]) ).
fof(f7041,plain,
( e = s(s(e))
| ~ spl1_37 ),
inference(avatar_component_clause,[],[f7039]) ).
fof(f7150,plain,
( $false
| ~ spl1_32 ),
inference(resolution,[],[f7037,f61]) ).
fof(f7189,plain,
~ spl1_32,
inference(avatar_contradiction_clause,[],[f7150]) ).
fof(f7320,plain,
( ~ subq(e,e)
| spl1_32
| ~ spl1_37 ),
inference(forward_demodulation,[],[f6958,f7041]) ).
fof(f7671,plain,
( $false
| spl1_32
| ~ spl1_37 ),
inference(resolution,[],[f7320,f64]) ).
fof(f7675,plain,
( spl1_32
| ~ spl1_37 ),
inference(avatar_contradiction_clause,[],[f7671]) ).
fof(f8052,plain,
( subq(s(s(e)),e)
| ~ spl1_34 ),
inference(superposition,[],[f6967,f5181]) ).
fof(f8056,plain,
( spl1_32
| ~ spl1_34 ),
inference(avatar_split_clause,[],[f8052,f6966,f6957]) ).
fof(f8465,plain,
( s(e) = p(s(s(e)))
| ~ spl1_31 ),
inference(resolution,[],[f6388,f46]) ).
fof(f9137,plain,
( subq(s(e),s(s(e)))
| ~ spl1_30 ),
inference(resolution,[],[f6384,f56]) ).
fof(f9139,plain,
( spl1_13
| ~ spl1_30 ),
inference(avatar_split_clause,[],[f9137,f6382,f6231]) ).
fof(f9170,plain,
( ! [X0] :
( mem(X0,s(s(e)))
| ~ mem(X0,s(e)) )
| ~ spl1_13 ),
inference(resolution,[],[f6232,f41]) ).
fof(f9288,plain,
( ~ mem(e,s(e))
| ~ spl1_13
| spl1_16 ),
inference(resolution,[],[f9170,f6276]) ).
fof(f9355,plain,
( $false
| ~ spl1_13
| spl1_16 ),
inference(resolution,[],[f9288,f61]) ).
fof(f9358,plain,
( ~ spl1_13
| spl1_16 ),
inference(avatar_contradiction_clause,[],[f9355]) ).
fof(f9429,plain,
( ! [X0] :
( ~ subq(X0,s(s(e)))
| mem(X0,s(e)) )
| ~ spl1_31 ),
inference(superposition,[],[f57,f8465]) ).
fof(f9608,plain,
( mem(s(s(e)),s(e))
| ~ spl1_31 ),
inference(resolution,[],[f9429,f69]) ).
fof(f9732,plain,
( e = s(s(e))
| ~ spl1_31 ),
inference(resolution,[],[f9608,f46]) ).
fof(f9735,plain,
( spl1_37
| ~ spl1_31 ),
inference(avatar_split_clause,[],[f9732,f6386,f7039]) ).
cnf(s1599,plain,
( ~ spl1_8
| spl1_9 ),
inference(sat_conversion,[],[f5880]) ).
cnf(s1606,plain,
( spl1_8
| spl1_10
| ~ spl1_11 ),
inference(sat_conversion,[],[f5931]) ).
cnf(s1615,plain,
spl1_11,
inference(sat_conversion,[],[f6016]) ).
cnf(s1737,plain,
( ~ spl1_10
| spl1_30
| spl1_31 ),
inference(sat_conversion,[],[f6389]) ).
cnf(s1790,plain,
( ~ spl1_16
| spl1_28 ),
inference(sat_conversion,[],[f6415]) ).
cnf(s1813,plain,
~ spl1_28,
inference(sat_conversion,[],[f6664]) ).
cnf(s1868,plain,
( ~ spl1_9
| spl1_33
| spl1_34 ),
inference(sat_conversion,[],[f6968]) ).
cnf(s1880,plain,
( spl1_28
| ~ spl1_33 ),
inference(sat_conversion,[],[f7006]) ).
cnf(s1903,plain,
~ spl1_32,
inference(sat_conversion,[],[f7189]) ).
cnf(s1910,plain,
( spl1_32
| ~ spl1_37 ),
inference(sat_conversion,[],[f7675]) ).
cnf(s1965,plain,
( spl1_32
| ~ spl1_34 ),
inference(sat_conversion,[],[f8056]) ).
cnf(s2158,plain,
( spl1_13
| ~ spl1_30 ),
inference(sat_conversion,[],[f9139]) ).
cnf(s2193,plain,
( ~ spl1_13
| spl1_16 ),
inference(sat_conversion,[],[f9358]) ).
cnf(s2277,plain,
( ~ spl1_31
| spl1_37 ),
inference(sat_conversion,[],[f9735]) ).
cnf(s2280,plain,
~ spl1_34,
inference(rat,[],[s1965,s1903]) ).
cnf(s2281,plain,
~ spl1_37,
inference(rat,[],[s1910,s1903]) ).
cnf(s2283,plain,
~ spl1_31,
inference(rat,[],[s2277,s2281]) ).
cnf(s2285,plain,
( ~ spl1_9
| spl1_33 ),
inference(rat,[],[s1868,s2280]) ).
cnf(s2287,plain,
~ spl1_33,
inference(rat,[],[s1880,s1813]) ).
cnf(s2288,plain,
~ spl1_9,
inference(rat,[],[s2285,s2287]) ).
cnf(s2290,plain,
~ spl1_16,
inference(rat,[],[s1790,s1813]) ).
cnf(s2291,plain,
~ spl1_13,
inference(rat,[],[s2193,s2290]) ).
cnf(s2292,plain,
~ spl1_30,
inference(rat,[],[s2158,s2291]) ).
cnf(s2293,plain,
~ spl1_10,
inference(rat,[],[s1737,s2283,s2292]) ).
cnf(s2294,plain,
spl1_8,
inference(rat,[],[s1606,s1615,s2293]) ).
cnf(s2295,plain,
$false,
inference(rat,[],[s1599,s2288,s2294]) ).
fof(f9736,plain,
$false,
inference(avatar_sat_refutation,[],[s2295]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV566+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n018.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 06:37:55 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.88/2.82 % (3178158)Will run a generic schedule for satisfiability detection.
% 16.88/2.82 % (3178168)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=158981051:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.88/2.82 % (3178164)% WARNING: option uhcvi not known.
% 16.88/2.82 % (3178165)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2842741029:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.88/2.82 % (3178166)dis+10_1_sil=32000:sp=arity:random_seed=355190804:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.88/2.82 % (3178163)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=703455661_2999 on theBenchmark for (2999ds/0Mi)
% 16.88/2.82 % (3178164)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3248517394:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.88/2.82 % (3178169)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2487133857:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.88/2.82 % (3178167)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3529182338:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.88/2.82 % TRYING [1]
% 16.88/2.82 % TRYING [2]
% 16.88/2.82 % TRYING [3]
% 16.88/2.82 % TRYING [4]
% 16.88/2.82 % TRYING [5]
% 16.88/2.82 % TRYING [6]
% 16.88/2.82 % TRYING [7]
% 16.88/2.82 % (3178168)Instruction limit reached!
% 16.88/2.82 % (3178168)------------------------------
% 16.88/2.82 % (3178168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.88/2.82 % (3178168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.88/2.82 % (3178168)CaDiCaL version: 2.1.3
% 16.88/2.82 % (3178168)Termination reason: Instruction limit
% 16.88/2.82 % (3178168)Termination phase: Saturation
% 16.88/2.82 % (3178168)Time elapsed: 0.044 s
% 16.88/2.82 % (3178168)Peak memory usage: 13 MB
% 16.88/2.82 % (3178168)Instructions burned: 133 (million)
% 16.88/2.82 % (3178177)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4014513168:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.88/2.82 % TRYING [1]
% 16.88/2.82 % TRYING [2]
% 16.88/2.82 % TRYING [3]
% 16.88/2.82 % TRYING [4]
% 16.88/2.82 % TRYING [5]
% 16.88/2.82 % TRYING [8]
% 16.88/2.82 % TRYING [6]
% 16.88/2.82 % (3178166)Instruction limit reached!
% 16.88/2.82 % (3178166)------------------------------
% 16.88/2.82 % (3178166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.88/2.82 % (3178166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.88/2.82 % (3178166)CaDiCaL version: 2.1.3
% 16.88/2.82 % (3178166)Termination reason: Instruction limit
% 16.88/2.82 % (3178166)Termination phase: Saturation
% 16.88/2.82 % (3178166)Time elapsed: 0.065 s
% 16.88/2.82 % (3178166)Peak memory usage: 12 MB
% 16.88/2.82 % (3178166)Instructions burned: 104 (million)
% 16.88/2.82 % (3178167)Instruction limit reached!
% 16.88/2.82 % (3178167)------------------------------
% 16.88/2.82 % (3178167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.88/2.82 % (3178167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.88/2.82 % (3178167)CaDiCaL version: 2.1.3
% 16.88/2.82 % (3178167)Termination reason: Instruction limit
% 16.88/2.82 % (3178167)Termination phase: Saturation
% 16.88/2.82 % (3178167)Time elapsed: 0.068 s
% 16.88/2.82 % (3178167)Peak memory usage: 12 MB
% 16.88/2.82 % (3178167)Instructions burned: 117 (million)
% 16.88/2.82 % TRYING [7]
% 16.88/2.82 % (3178179)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2953110510:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 16.88/2.82 % (3178180)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=253450505:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 16.88/2.82 % (3178169)Instruction limit reached!
% 16.88/2.82 % (3178169)------------------------------
% 16.88/2.82 % (3178169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.88/2.82 % (3178169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.88/2.82 % (3178169)CaDiCaL version: 2.1.3
% 16.88/2.82 % (3178169)Termination reason: Instruction limit
% 16.88/2.82 % (3178169)Termination phase: Saturation
% 16.88/2.82 % (3178169)Time elapsed: 0.109 s
% 16.88/2.82 % (3178169)Peak memory usage: 13 MB
% 16.88/2.82 % (3178169)Instructions burned: 160 (million)
% 16.88/2.82 % TRYING [8]
% 16.88/2.82 % (3178183)ott-21_1_sil=16000:fs=off:random_seed=590678342:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.88/2.82 % TRYING [9]
% 16.88/2.82 % (3178179)Instruction limit reached!
% 16.88/2.82 % (3178179)------------------------------
% 42.43/6.43 % (3178179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.43 % (3178179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.43 % (3178179)CaDiCaL version: 2.1.3
% 42.43/6.43 % (3178179)Termination reason: Instruction limit
% 42.43/6.43 % (3178179)Termination phase: Saturation
% 42.43/6.43 % (3178179)Time elapsed: 0.083 s
% 42.43/6.43 % (3178179)Peak memory usage: 13 MB
% 42.43/6.43 % (3178179)Instructions burned: 132 (million)
% 42.43/6.43 % (3178185)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3609307059:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.43/6.43 % (3178183)Instruction limit reached!
% 42.43/6.43 % (3178183)------------------------------
% 42.43/6.43 % (3178183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.43 % (3178183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.43 % (3178183)CaDiCaL version: 2.1.3
% 42.43/6.43 % (3178183)Termination reason: Instruction limit
% 42.43/6.43 % (3178183)Termination phase: Saturation
% 42.43/6.43 % (3178183)Time elapsed: 0.094 s
% 42.43/6.43 % (3178183)Peak memory usage: 13 MB
% 42.43/6.43 % (3178183)Instructions burned: 180 (million)
% 42.43/6.43 % (3178187)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1559166418:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.43/6.43 % TRYING [1]
% 42.43/6.43 % TRYING [2]
% 42.43/6.43 % (3178177)Instruction limit reached!
% 42.43/6.43 % (3178177)------------------------------
% 42.43/6.43 % (3178177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.43 % (3178177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.43 % (3178177)CaDiCaL version: 2.1.3
% 42.43/6.43 % (3178177)Termination reason: Instruction limit
% 42.43/6.43 % (3178177)Termination phase: Finite model building SAT solving
% 42.43/6.43 % (3178177)Time elapsed: 0.198 s
% 42.43/6.43 % (3178177)Peak memory usage: 19 MB
% 42.43/6.43 % (3178177)Instructions burned: 715 (million)
% 42.43/6.43 % TRYING [3]
% 42.43/6.43 % TRYING [4]
% 42.43/6.43 % (3178189)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3130257908:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 42.43/6.43 % TRYING [5]
% 42.43/6.43 % TRYING [6]
% 42.43/6.43 % TRYING [7]
% 42.43/6.43 % TRYING [8]
% 42.43/6.43 % (3178185)Instruction limit reached!
% 42.43/6.43 % (3178185)------------------------------
% 42.43/6.43 % (3178185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.43 % (3178185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.43 % (3178185)CaDiCaL version: 2.1.3
% 42.43/6.43 % (3178185)Termination reason: Instruction limit
% 42.43/6.43 % (3178185)Termination phase: Saturation
% 42.43/6.43 % (3178185)Time elapsed: 0.287 s
% 42.43/6.43 % (3178185)Peak memory usage: 13 MB
% 42.43/6.43 % (3178185)Instructions burned: 479 (million)
% 42.43/6.43 % TRYING [10]
% 42.43/6.43 % (3178191)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3353318190:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.43/6.43 % (3178180)Instruction limit reached!
% 42.43/6.43 % (3178180)------------------------------
% 42.43/6.43 % (3178180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.43 % (3178180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.43 % (3178180)CaDiCaL version: 2.1.3
% 42.43/6.43 % (3178180)Termination reason: Instruction limit
% 42.43/6.43 % (3178180)Termination phase: Saturation
% 42.43/6.43 % (3178180)Time elapsed: 0.414 s
% 42.43/6.43 % (3178180)Peak memory usage: 18 MB
% 42.43/6.43 % (3178180)Instructions burned: 684 (million)
% 42.43/6.43 % TRYING [14]
% 42.43/6.43 % (3178193)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=2989327758: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)
% 42.43/6.43 % (3178187)Instruction limit reached!
% 42.43/6.43 % (3178187)------------------------------
% 42.43/6.43 % (3178187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.43/6.43 % (3178187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.43/6.43 % (3178187)CaDiCaL version: 2.1.3
% 42.43/6.43 % (3178187)Termination reason: Instruction limit
% 42.43/6.43 % (3178187)Termination phase: Finite model building SAT solving
% 42.43/6.43 % (3178187)Time elapsed: 0.310 s
% 42.43/6.43 % (3178187)Peak memory usage: 16 MB
% 42.43/6.43 % (3178187)Instructions burned: 866 (million)
% 42.43/6.43 % (3178195)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3023954536:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 47.12/7.09 % (3178189)Instruction limit reached!
% 47.12/7.09 % (3178189)------------------------------
% 47.12/7.09 % (3178189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178189)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178189)Termination reason: Instruction limit
% 47.12/7.09 % (3178189)Termination phase: Saturation
% 47.12/7.09 % (3178189)Time elapsed: 0.385 s
% 47.12/7.09 % (3178189)Peak memory usage: 24 MB
% 47.12/7.09 % (3178189)Instructions burned: 1181 (million)
% 47.12/7.09 % (3178197)fmb+10_1_sil=64000:random_seed=849406915:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 47.12/7.09 % TRYING [1]
% 47.12/7.09 % TRYING [2]
% 47.12/7.09 % TRYING [3]
% 47.12/7.09 % TRYING [4]
% 47.12/7.09 % TRYING [5]
% 47.12/7.09 % TRYING [6]
% 47.12/7.09 % TRYING [7]
% 47.12/7.09 % TRYING [8]
% 47.12/7.09 % TRYING [9]
% 47.12/7.09 % (3178191)Instruction limit reached!
% 47.12/7.09 % (3178191)------------------------------
% 47.12/7.09 % (3178191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178191)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178191)Termination reason: Instruction limit
% 47.12/7.09 % (3178191)Termination phase: Finite model building SAT solving
% 47.12/7.09 % (3178191)Time elapsed: 0.336 s
% 47.12/7.09 % (3178191)Peak memory usage: 39 MB
% 47.12/7.09 % (3178191)Instructions burned: 892 (million)
% 47.12/7.09 % TRYING [10]
% 47.12/7.09 % (3178199)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1908411489:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 47.12/7.09 % TRYING [20]
% 47.12/7.09 % (3178193)Instruction limit reached!
% 47.12/7.09 % (3178193)------------------------------
% 47.12/7.09 % (3178193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178193)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178193)Termination reason: Instruction limit
% 47.12/7.09 % (3178193)Termination phase: Saturation
% 47.12/7.09 % (3178193)Time elapsed: 0.420 s
% 47.12/7.09 % (3178193)Peak memory usage: 19 MB
% 47.12/7.09 % (3178193)Instructions burned: 692 (million)
% 47.12/7.09 % TRYING [11]
% 47.12/7.09 % (3178201)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1819248240:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 47.12/7.09 % TRYING [8]
% 47.12/7.09 % TRYING [9]
% 47.12/7.09 % (3178195)Instruction limit reached!
% 47.12/7.09 % (3178195)------------------------------
% 47.12/7.09 % (3178195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178195)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178195)Termination reason: Instruction limit
% 47.12/7.09 % (3178195)Termination phase: Saturation
% 47.12/7.09 % (3178195)Time elapsed: 0.499 s
% 47.12/7.09 % (3178195)Peak memory usage: 18 MB
% 47.12/7.09 % (3178195)Instructions burned: 880 (million)
% 47.12/7.09 % (3178203)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3196612317:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 47.12/7.09 % TRYING [12]
% 47.12/7.09 % TRYING [13]
% 47.12/7.09 % TRYING [10]
% 47.12/7.09 % (3178201)Instruction limit reached!
% 47.12/7.09 % (3178201)------------------------------
% 47.12/7.09 % (3178201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178201)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178201)Termination reason: Instruction limit
% 47.12/7.09 % (3178201)Termination phase: Finite model building constraint generation
% 47.12/7.09 % (3178201)Time elapsed: 0.450 s
% 47.12/7.09 % (3178201)Peak memory usage: 22 MB
% 47.12/7.09 % (3178201)Instructions burned: 922 (million)
% 47.12/7.09 % (3178205)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2714373893:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 47.12/7.09 % TRYING [14]
% 47.12/7.09 % (3178205)Instruction limit reached!
% 47.12/7.09 % (3178205)------------------------------
% 47.12/7.09 % (3178205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178205)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178205)Termination reason: Instruction limit
% 47.12/7.09 % (3178205)Termination phase: Saturation
% 47.12/7.09 % (3178205)Time elapsed: 0.934 s
% 47.12/7.09 % (3178205)Peak memory usage: 27 MB
% 47.12/7.09 % (3178205)Instructions burned: 1472 (million)
% 47.12/7.09 % (3178207)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1522262005:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 47.12/7.09 % TRYING [77]
% 47.12/7.09 % TRYING [11]
% 47.12/7.09 % TRYING [15]
% 47.12/7.09 % (3178203)Instruction limit reached!
% 47.12/7.09 % (3178203)------------------------------
% 47.12/7.09 % (3178203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178203)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178203)Termination reason: Instruction limit
% 47.12/7.09 % (3178203)Termination phase: Saturation
% 47.12/7.09 % (3178203)Time elapsed: 2.913 s
% 47.12/7.09 % (3178203)Peak memory usage: 31 MB
% 47.12/7.09 % (3178203)Instructions burned: 5131 (million)
% 47.12/7.09 % (3178209)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2813308041:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 47.12/7.09 % TRYING [16]
% 47.12/7.09 % (3178207)Instruction limit reached!
% 47.12/7.09 % (3178207)------------------------------
% 47.12/7.09 % (3178207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178207)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178207)Termination reason: Instruction limit
% 47.12/7.09 % (3178207)Termination phase: Finite model building constraint generation
% 47.12/7.09 % (3178207)Time elapsed: 2.331 s
% 47.12/7.09 % (3178207)Peak memory usage: 494 MB
% 47.12/7.09 % (3178207)Instructions burned: 6326 (million)
% 47.12/7.09 % TRYING [16]
% 47.12/7.09 % (3178211)ott-2_1_sil=16000:newcnf=on:random_seed=34570027:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi)
% 47.12/7.09 % (3178209)Instruction limit reached!
% 47.12/7.09 % (3178209)------------------------------
% 47.12/7.09 % (3178209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178209)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178209)Termination reason: Instruction limit
% 47.12/7.09 % (3178209)Termination phase: Finite model building SAT solving
% 47.12/7.09 % (3178209)Time elapsed: 0.901 s
% 47.12/7.09 % (3178209)Peak memory usage: 132 MB
% 47.12/7.09 % (3178209)Instructions burned: 2176 (million)
% 47.12/7.09 % (3178213)ott+10_1_sil=32000:tgt=ground:random_seed=3525854957:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 47.12/7.09 % (3178211)Instruction limit reached!
% 47.12/7.09 % (3178211)------------------------------
% 47.12/7.09 % (3178211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178211)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178211)Termination reason: Instruction limit
% 47.12/7.09 % (3178211)Termination phase: Saturation
% 47.12/7.09 % (3178211)Time elapsed: 0.516 s
% 47.12/7.09 % (3178211)Peak memory usage: 17 MB
% 47.12/7.09 % (3178211)Instructions burned: 869 (million)
% 47.12/7.09 % (3178215)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1560678948:i=54282_2946 on theBenchmark for (2946ds/54282Mi)
% 47.12/7.09 % TRYING [1]
% 47.12/7.09 % TRYING [2]
% 47.12/7.09 % TRYING [3]
% 47.12/7.09 % TRYING [4]
% 47.12/7.09 % TRYING [5]
% 47.12/7.09 % TRYING [6]
% 47.12/7.09 % TRYING [7]
% 47.12/7.09 % TRYING [8]
% 47.12/7.09 % (3178197)Instruction limit reached!
% 47.12/7.09 % (3178197)------------------------------
% 47.12/7.09 % (3178197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178197)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178197)Termination reason: Instruction limit
% 47.12/7.09 % (3178197)Termination phase: Finite model building SAT solving
% 47.12/7.09 % (3178197)Time elapsed: 4.750 s
% 47.12/7.09 % (3178197)Peak memory usage: 59 MB
% 47.12/7.09 % (3178197)Instructions burned: 22065 (million)
% 47.12/7.09 % (3178217)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1933635033:i=3512:aac=none_2945 on theBenchmark for (2945ds/3512Mi)
% 47.12/7.09 % TRYING [9]
% 47.12/7.09 % TRYING [10]
% 47.12/7.09 % (3178199)Instruction limit reached!
% 47.12/7.09 % (3178199)------------------------------
% 47.12/7.09 % (3178199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178199)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178199)Termination reason: Instruction limit
% 47.12/7.09 % (3178199)Termination phase: Finite model building SAT solving
% 47.12/7.09 % (3178199)Time elapsed: 5.121 s
% 47.12/7.09 % (3178199)Peak memory usage: 186 MB
% 47.12/7.09 % (3178199)Instructions burned: 9518 (million)
% 47.12/7.09 % (3178219)dis+21_1_sil=32000:sas=cadical:random_seed=1791130802:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 47.12/7.09 % (3178217)Instruction limit reached!
% 47.12/7.09 % (3178217)------------------------------
% 47.12/7.09 % (3178217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178217)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178217)Termination reason: Instruction limit
% 47.12/7.09 % (3178217)Termination phase: Saturation
% 47.12/7.09 % (3178217)Time elapsed: 0.995 s
% 47.12/7.09 % (3178217)Peak memory usage: 25 MB
% 47.12/7.09 % (3178217)Instructions burned: 3514 (million)
% 47.12/7.09 % (3178221)ott+11_1_sil=16000:gs=on:random_seed=563425034:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 47.12/7.09 % (3178221) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3178158-3178221"...
% 47.12/7.09 % (3178221)...printing done.
% 47.12/7.09 % (3178221)Refutation found. Thanks to Tanya!
% 47.12/7.09 % SZS status Theorem for theBenchmark
% 47.12/7.09 % SZS output start Proof for theBenchmark
% See solution above
% 47.12/7.09 % (3178221)------------------------------
% 47.12/7.09 % (3178221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.12/7.09 % (3178221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.12/7.09 % (3178221)CaDiCaL version: 2.1.3
% 47.12/7.09 % (3178221)Termination reason: Refutation
% 47.12/7.09 % (3178221)Time elapsed: 0.197 s
% 47.12/7.09 % (3178221)Peak memory usage: 19 MB
% 47.12/7.09 % (3178221)Instructions burned: 655 (million)
% 47.12/7.09 % (3178158)Success in time 6.669 s
% 47.12/7.09 % Vampire exiting
%------------------------------------------------------------------------------