%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV569+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 : 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:30 PM UTC 2026
% Result : Theorem 4.98s 1.19s
% Output : Refutation 4.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 18
% Syntax : Number of formulae : 152 ( 28 unt; 11 def)
% Number of atoms : 373 ( 63 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 383 ( 162 ~; 194 |; 11 &)
% ( 15 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 15 ( 13 usr; 12 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 93 ( 0 sgn 91 !; 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(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(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(f26,conjecture,
~ subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nsubq_2762_2760) ).
fof(f27,negated_conjecture,
~ ~ subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(n(n(e))))))),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f28,plain,
subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(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(f41,plain,
! [X3,X0,X1] :
( ~ mem(X3,X0)
| mem(X3,X1)
| ~ subq(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
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(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(f58,plain,
subq(u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(a(s(n(e)),n(n(e))),a(s(n(s(n(e)))),n(n(n(e)))))),u(a(s(u(n(e),n(s(n(e))))),a(n(e),n(n(e)))),u(s(n(n(e))),a(s(n(s(n(e)))),n(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))))))),s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))))),u(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))))),u(u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))))),u(s(u(u(e,s(e)),s(u(e,s(e))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))))),
inference(definition_unfolding,[],[f58,f54,f59,f59,f59,f54,f59,f59,f59,f54,f59,f59,f59,f54,f59,f59,f59,f59,f59,f54,f59,f59,f59,f54,f59,f59,f59,f59,f59,f54,f59,f59,f59,f59,f59]) ).
fof(f61,plain,
! [X1] : mem(X1,s(X1)),
inference(equality_resolution,[],[f47]) ).
fof(f263,plain,
! [X2,X3,X0,X1] :
( ~ subq(u(X2,X3),X1)
| mem(X0,X1)
| ~ mem(X0,X3) ),
inference(resolution,[],[f41,f49]) ).
fof(f3421,definition,
( spl1_58
<=> ! [X1] : ~ mem(X1,u(e,s(e))) ),
introduced(definition,[new_symbols(definition,[spl1_58])],[avatar_definition]) ).
fof(f3422,plain,
( ! [X1] : ~ mem(X1,u(e,s(e)))
| ~ spl1_58 ),
inference(avatar_component_clause,[],[f3421]) ).
fof(f3428,plain,
( ! [X0] : ~ mem(X0,s(e))
| ~ spl1_58 ),
inference(resolution,[],[f3422,f49]) ).
fof(f3432,plain,
( $false
| ~ spl1_58 ),
inference(resolution,[],[f3428,f61]) ).
fof(f3435,plain,
~ spl1_58,
inference(avatar_contradiction_clause,[],[f3432]) ).
fof(f4833,definition,
( spl1_66
<=> ! [X1] : ~ mem(X1,u(u(e,s(e)),s(u(e,s(e))))) ),
introduced(definition,[new_symbols(definition,[spl1_66])],[avatar_definition]) ).
fof(f4834,plain,
( ! [X1] : ~ mem(X1,u(u(e,s(e)),s(u(e,s(e)))))
| ~ spl1_66 ),
inference(avatar_component_clause,[],[f4833]) ).
fof(f4839,plain,
( ! [X0] : ~ mem(X0,u(e,s(e)))
| ~ spl1_66 ),
inference(resolution,[],[f4834,f50]) ).
fof(f4843,plain,
( spl1_58
| ~ spl1_66 ),
inference(avatar_split_clause,[],[f4839,f4833,f3421]) ).
fof(f5445,definition,
( spl1_68
<=> e = u(s(u(e,s(e))),s(s(u(e,s(e))))) ),
introduced(definition,[new_symbols(definition,[spl1_68])],[avatar_definition]) ).
fof(f5446,plain,
( e != u(s(u(e,s(e))),s(s(u(e,s(e)))))
| spl1_68 ),
inference(avatar_component_clause,[],[f5445]) ).
fof(f5447,plain,
( e = u(s(u(e,s(e))),s(s(u(e,s(e)))))
| ~ spl1_68 ),
inference(avatar_component_clause,[],[f5445]) ).
fof(f5449,definition,
( spl1_69
<=> e = u(u(e,s(e)),s(u(e,s(e)))) ),
introduced(definition,[new_symbols(definition,[spl1_69])],[avatar_definition]) ).
fof(f5450,plain,
( e != u(u(e,s(e)),s(u(e,s(e))))
| spl1_69 ),
inference(avatar_component_clause,[],[f5449]) ).
fof(f5451,plain,
( e = u(u(e,s(e)),s(u(e,s(e))))
| ~ spl1_69 ),
inference(avatar_component_clause,[],[f5449]) ).
fof(f5465,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,s(u(e,s(e)))) )
| ~ spl1_68 ),
inference(superposition,[],[f50,f5447]) ).
fof(f5466,plain,
( ! [X0] : ~ mem(X0,s(u(e,s(e))))
| ~ spl1_68 ),
inference(forward_subsumption_resolution,[],[f5465,f45]) ).
fof(f5468,plain,
( $false
| ~ spl1_68 ),
inference(resolution,[],[f5466,f61]) ).
fof(f5472,plain,
~ spl1_68,
inference(avatar_contradiction_clause,[],[f5468]) ).
fof(f5489,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,u(e,s(e))) )
| ~ spl1_69 ),
inference(superposition,[],[f50,f5451]) ).
fof(f5490,plain,
( ! [X0] : ~ mem(X0,u(e,s(e)))
| ~ spl1_69 ),
inference(forward_subsumption_resolution,[],[f5489,f45]) ).
fof(f5492,plain,
( spl1_58
| ~ spl1_69 ),
inference(avatar_split_clause,[],[f5490,f5449,f3421]) ).
fof(f6656,plain,
! [X0] :
( mem(X0,u(u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))))),u(s(u(u(e,s(e)),s(u(e,s(e))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))))))
| ~ mem(X0,u(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))))) ),
inference(resolution,[],[f263,f60]) ).
fof(f6718,plain,
! [X0] :
( ~ mem(X0,u(u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))))
| mem(X0,u(s(u(u(e,s(e)),s(u(e,s(e))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))))
| mem(X0,u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e))))))))) ),
inference(resolution,[],[f6656,f48]) ).
fof(f6721,plain,
! [X0] :
( mem(X0,u(s(u(u(e,s(e)),s(u(e,s(e))))),u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))))
| mem(X0,u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))))))
| ~ mem(X0,u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e))))))) ),
inference(resolution,[],[f6718,f50]) ).
fof(f6946,definition,
( spl1_115
<=> e = u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))) ),
introduced(definition,[new_symbols(definition,[spl1_115])],[avatar_definition]) ).
fof(f6947,plain,
( e != u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))
| spl1_115 ),
inference(avatar_component_clause,[],[f6946]) ).
fof(f6948,plain,
( e = u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))
| ~ spl1_115 ),
inference(avatar_component_clause,[],[f6946]) ).
fof(f6950,definition,
( spl1_116
<=> e = u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) ),
introduced(definition,[new_symbols(definition,[spl1_116])],[avatar_definition]) ).
fof(f6951,plain,
( e != u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))
| spl1_116 ),
inference(avatar_component_clause,[],[f6950]) ).
fof(f6952,plain,
( e = u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))
| ~ spl1_116 ),
inference(avatar_component_clause,[],[f6950]) ).
fof(f7109,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,u(e,s(e))) )
| ~ spl1_115 ),
inference(superposition,[],[f50,f6948]) ).
fof(f7112,plain,
( ! [X0] : ~ mem(X0,u(e,s(e)))
| ~ spl1_115 ),
inference(forward_subsumption_resolution,[],[f7109,f45]) ).
fof(f7117,plain,
( spl1_58
| ~ spl1_115 ),
inference(avatar_split_clause,[],[f7112,f6946,f3421]) ).
fof(f7179,plain,
( ! [X0] :
( mem(X0,e)
| ~ mem(X0,u(u(e,s(e)),s(u(e,s(e))))) )
| ~ spl1_116 ),
inference(superposition,[],[f50,f6952]) ).
fof(f7182,plain,
( ! [X0] : ~ mem(X0,u(u(e,s(e)),s(u(e,s(e)))))
| ~ spl1_116 ),
inference(forward_subsumption_resolution,[],[f7179,f45]) ).
fof(f7187,plain,
( spl1_66
| ~ spl1_116 ),
inference(avatar_split_clause,[],[f7182,f6950,f4833]) ).
fof(f8029,plain,
! [X0] :
( mem(X0,u(s(u(s(u(e,s(e))),s(s(u(e,s(e)))))),s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))))))
| ~ mem(X0,u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))))
| mem(X0,u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))))))
| mem(X0,s(u(u(e,s(e)),s(u(e,s(e)))))) ),
inference(resolution,[],[f6721,f48]) ).
fof(f8032,plain,
! [X0] :
( mem(X0,u(s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))),s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))))))
| ~ mem(X0,u(s(u(e,s(e))),s(u(u(e,s(e)),s(u(e,s(e)))))))
| mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| mem(X0,s(u(u(u(e,s(e)),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(s(u(e,s(e))))))) ),
inference(resolution,[],[f8029,f48]) ).
fof(f8035,plain,
! [X0] :
( mem(X0,s(u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))))
| mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| ~ mem(X0,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(s(u(e,s(e)))))))
| mem(X0,s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e))))))))
| mem(X0,s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))))) ),
inference(resolution,[],[f8032,f48]) ).
fof(f8047,plain,
! [X0] :
( mem(X0,s(u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))))
| ~ mem(X0,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(s(u(e,s(e)))))))
| mem(X0,s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e))))))))
| mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0 ),
inference(resolution,[],[f8035,f46]) ).
fof(f8103,plain,
! [X0] :
( ~ mem(X0,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(s(u(e,s(e)))))))
| mem(X0,s(u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e))))))))
| mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0
| u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))) = X0 ),
inference(resolution,[],[f8047,f46]) ).
fof(f8107,plain,
! [X0] :
( mem(X0,s(u(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(s(u(e,s(e)))))))
| mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0
| u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))) = X0
| ~ mem(X0,s(u(e,s(e)))) ),
inference(resolution,[],[f8103,f50]) ).
fof(f8868,plain,
! [X0] :
( mem(X0,s(u(s(u(e,s(e))),s(s(u(e,s(e)))))))
| mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0
| u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))) = X0
| ~ mem(X0,s(u(e,s(e))))
| u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0 ),
inference(resolution,[],[f8107,f46]) ).
fof(f8880,plain,
! [X0] :
( mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0
| u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))) = X0
| ~ mem(X0,s(u(e,s(e))))
| u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0
| u(s(u(e,s(e))),s(s(u(e,s(e))))) = X0 ),
inference(resolution,[],[f8868,f46]) ).
fof(f8885,plain,
! [X0] :
( ~ mem(X0,s(u(e,s(e))))
| u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))) = X0
| u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0
| u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))) = X0
| u(s(u(e,s(e))),s(s(u(e,s(e))))) = X0
| u(u(e,s(e)),s(u(e,s(e)))) = X0 ),
inference(resolution,[],[f8880,f46]) ).
fof(f8890,plain,
( u(e,s(e)) = u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))
| u(e,s(e)) = u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))
| u(e,s(e)) = u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e))))))
| u(e,s(e)) = u(s(u(e,s(e))),s(s(u(e,s(e)))))
| u(e,s(e)) = u(u(e,s(e)),s(u(e,s(e)))) ),
inference(resolution,[],[f8885,f61]) ).
fof(f9113,definition,
( spl1_190
<=> u(e,s(e)) = u(u(e,s(e)),s(u(e,s(e)))) ),
introduced(definition,[new_symbols(definition,[spl1_190])],[avatar_definition]) ).
fof(f9115,plain,
( u(e,s(e)) = u(u(e,s(e)),s(u(e,s(e))))
| ~ spl1_190 ),
inference(avatar_component_clause,[],[f9113]) ).
fof(f9117,definition,
( spl1_191
<=> u(e,s(e)) = u(s(u(e,s(e))),s(s(u(e,s(e))))) ),
introduced(definition,[new_symbols(definition,[spl1_191])],[avatar_definition]) ).
fof(f9119,plain,
( u(e,s(e)) = u(s(u(e,s(e))),s(s(u(e,s(e)))))
| ~ spl1_191 ),
inference(avatar_component_clause,[],[f9117]) ).
fof(f9121,definition,
( spl1_192
<=> u(e,s(e)) = u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e)))))) ),
introduced(definition,[new_symbols(definition,[spl1_192])],[avatar_definition]) ).
fof(f9123,plain,
( u(e,s(e)) = u(u(e,s(e)),s(u(u(e,s(e)),s(u(e,s(e))))))
| ~ spl1_192 ),
inference(avatar_component_clause,[],[f9121]) ).
fof(f9125,definition,
( spl1_193
<=> u(e,s(e)) = u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e)))))) ),
introduced(definition,[new_symbols(definition,[spl1_193])],[avatar_definition]) ).
fof(f9127,plain,
( u(e,s(e)) = u(u(u(e,s(e)),s(u(e,s(e)))),s(u(u(e,s(e)),s(u(e,s(e))))))
| ~ spl1_193 ),
inference(avatar_component_clause,[],[f9125]) ).
fof(f9129,definition,
( spl1_194
<=> u(e,s(e)) = u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e)))))) ),
introduced(definition,[new_symbols(definition,[spl1_194])],[avatar_definition]) ).
fof(f9131,plain,
( u(e,s(e)) = u(u(e,s(e)),u(s(u(e,s(e))),s(s(u(e,s(e))))))
| ~ spl1_194 ),
inference(avatar_component_clause,[],[f9129]) ).
fof(f9132,plain,
( spl1_190
| spl1_191
| spl1_192
| spl1_193
| spl1_194 ),
inference(avatar_split_clause,[],[f8890,f9129,f9125,f9121,f9117,f9113]) ).
fof(f9136,plain,
( e != u(e,s(e))
| spl1_69
| ~ spl1_190 ),
inference(superposition,[],[f5450,f9115]) ).
fof(f9268,plain,
( ! [X0] :
( ~ mem(X0,s(u(e,s(e))))
| mem(X0,u(e,s(e))) )
| ~ spl1_190 ),
inference(superposition,[],[f49,f9115]) ).
fof(f9378,plain,
( mem(u(e,s(e)),u(e,s(e)))
| ~ spl1_190 ),
inference(resolution,[],[f9268,f61]) ).
fof(f9537,plain,
( mem(u(e,s(e)),s(e))
| mem(u(e,s(e)),e)
| ~ spl1_190 ),
inference(resolution,[],[f9378,f48]) ).
fof(f9540,plain,
( mem(u(e,s(e)),s(e))
| ~ spl1_190 ),
inference(forward_subsumption_resolution,[],[f9537,f45]) ).
fof(f9542,plain,
( e = u(e,s(e))
| ~ spl1_190 ),
inference(resolution,[],[f9540,f46]) ).
fof(f9545,plain,
( $false
| spl1_69
| ~ spl1_190 ),
inference(forward_subsumption_resolution,[],[f9542,f9136]) ).
fof(f9546,plain,
( spl1_69
| ~ spl1_190 ),
inference(avatar_contradiction_clause,[],[f9545]) ).
fof(f9552,plain,
( e != u(e,s(e))
| spl1_68
| ~ spl1_191 ),
inference(superposition,[],[f5446,f9119]) ).
fof(f9608,plain,
( ! [X0] :
( ~ mem(X0,s(u(e,s(e))))
| mem(X0,u(e,s(e))) )
| ~ spl1_191 ),
inference(superposition,[],[f50,f9119]) ).
fof(f9616,plain,
( mem(u(e,s(e)),u(e,s(e)))
| ~ spl1_191 ),
inference(resolution,[],[f9608,f61]) ).
fof(f9685,plain,
( mem(u(e,s(e)),s(e))
| mem(u(e,s(e)),e)
| ~ spl1_191 ),
inference(resolution,[],[f9616,f48]) ).
fof(f9688,plain,
( mem(u(e,s(e)),s(e))
| ~ spl1_191 ),
inference(forward_subsumption_resolution,[],[f9685,f45]) ).
fof(f9700,plain,
( e = u(e,s(e))
| ~ spl1_191 ),
inference(resolution,[],[f9688,f46]) ).
fof(f9703,plain,
( $false
| spl1_68
| ~ spl1_191 ),
inference(forward_subsumption_resolution,[],[f9700,f9552]) ).
fof(f9704,plain,
( spl1_68
| ~ spl1_191 ),
inference(avatar_contradiction_clause,[],[f9703]) ).
fof(f9759,plain,
( ! [X0] :
( ~ mem(X0,s(u(u(e,s(e)),s(u(e,s(e))))))
| mem(X0,u(e,s(e))) )
| ~ spl1_192 ),
inference(superposition,[],[f49,f9123]) ).
fof(f9779,plain,
( mem(u(u(e,s(e)),s(u(e,s(e)))),u(e,s(e)))
| ~ spl1_192 ),
inference(resolution,[],[f9759,f61]) ).
fof(f9861,plain,
( mem(u(u(e,s(e)),s(u(e,s(e)))),s(e))
| mem(u(u(e,s(e)),s(u(e,s(e)))),e)
| ~ spl1_192 ),
inference(resolution,[],[f9779,f48]) ).
fof(f9864,plain,
( mem(u(u(e,s(e)),s(u(e,s(e)))),s(e))
| ~ spl1_192 ),
inference(forward_subsumption_resolution,[],[f9861,f45]) ).
fof(f9867,plain,
( e = u(u(e,s(e)),s(u(e,s(e))))
| ~ spl1_192 ),
inference(resolution,[],[f9864,f46]) ).
fof(f9870,plain,
( $false
| spl1_69
| ~ spl1_192 ),
inference(forward_subsumption_resolution,[],[f9867,f5450]) ).
fof(f9871,plain,
( spl1_69
| ~ spl1_192 ),
inference(avatar_contradiction_clause,[],[f9870]) ).
fof(f9921,plain,
( e != u(e,s(e))
| spl1_116
| ~ spl1_193 ),
inference(superposition,[],[f6951,f9127]) ).
fof(f9927,plain,
( ! [X0] :
( ~ mem(X0,u(u(e,s(e)),s(u(e,s(e)))))
| mem(X0,u(e,s(e))) )
| ~ spl1_193 ),
inference(superposition,[],[f50,f9127]) ).
fof(f9972,plain,
( ! [X0] :
( ~ mem(X0,s(u(e,s(e))))
| mem(X0,u(e,s(e))) )
| ~ spl1_193 ),
inference(resolution,[],[f9927,f49]) ).
fof(f10013,plain,
( mem(u(e,s(e)),u(e,s(e)))
| ~ spl1_193 ),
inference(resolution,[],[f9972,f61]) ).
fof(f10019,plain,
( mem(u(e,s(e)),s(e))
| mem(u(e,s(e)),e)
| ~ spl1_193 ),
inference(resolution,[],[f10013,f48]) ).
fof(f10022,plain,
( mem(u(e,s(e)),s(e))
| ~ spl1_193 ),
inference(forward_subsumption_resolution,[],[f10019,f45]) ).
fof(f10024,plain,
( e = u(e,s(e))
| ~ spl1_193 ),
inference(resolution,[],[f10022,f46]) ).
fof(f10027,plain,
( $false
| spl1_116
| ~ spl1_193 ),
inference(forward_subsumption_resolution,[],[f10024,f9921]) ).
fof(f10028,plain,
( spl1_116
| ~ spl1_193 ),
inference(avatar_contradiction_clause,[],[f10027]) ).
fof(f10073,plain,
( e != u(e,s(e))
| spl1_115
| ~ spl1_194 ),
inference(superposition,[],[f6947,f9131]) ).
fof(f10077,plain,
( ! [X0] :
( ~ mem(X0,u(s(u(e,s(e))),s(s(u(e,s(e))))))
| mem(X0,u(e,s(e))) )
| ~ spl1_194 ),
inference(superposition,[],[f49,f9131]) ).
fof(f10101,plain,
( ! [X0] :
( ~ mem(X0,s(u(e,s(e))))
| mem(X0,u(e,s(e))) )
| ~ spl1_194 ),
inference(resolution,[],[f10077,f50]) ).
fof(f10145,plain,
( mem(u(e,s(e)),u(e,s(e)))
| ~ spl1_194 ),
inference(resolution,[],[f10101,f61]) ).
fof(f10181,plain,
( mem(u(e,s(e)),s(e))
| mem(u(e,s(e)),e)
| ~ spl1_194 ),
inference(resolution,[],[f10145,f48]) ).
fof(f10184,plain,
( mem(u(e,s(e)),s(e))
| ~ spl1_194 ),
inference(forward_subsumption_resolution,[],[f10181,f45]) ).
fof(f10186,plain,
( e = u(e,s(e))
| ~ spl1_194 ),
inference(resolution,[],[f10184,f46]) ).
fof(f10189,plain,
( $false
| spl1_115
| ~ spl1_194 ),
inference(forward_subsumption_resolution,[],[f10186,f10073]) ).
fof(f10190,plain,
( spl1_115
| ~ spl1_194 ),
inference(avatar_contradiction_clause,[],[f10189]) ).
cnf(s1436,plain,
~ spl1_58,
inference(sat_conversion,[],[f3435]) ).
cnf(s2036,plain,
( spl1_58
| ~ spl1_66 ),
inference(sat_conversion,[],[f4843]) ).
cnf(s2340,plain,
~ spl1_68,
inference(sat_conversion,[],[f5472]) ).
cnf(s2362,plain,
( spl1_58
| ~ spl1_69 ),
inference(sat_conversion,[],[f5492]) ).
cnf(s3458,plain,
( spl1_58
| ~ spl1_115 ),
inference(sat_conversion,[],[f7117]) ).
cnf(s3526,plain,
( spl1_66
| ~ spl1_116 ),
inference(sat_conversion,[],[f7187]) ).
cnf(s4915,plain,
( spl1_190
| spl1_191
| spl1_192
| spl1_193
| spl1_194 ),
inference(sat_conversion,[],[f9132]) ).
cnf(s5231,plain,
( spl1_69
| ~ spl1_190 ),
inference(sat_conversion,[],[f9546]) ).
cnf(s5362,plain,
( spl1_68
| ~ spl1_191 ),
inference(sat_conversion,[],[f9704]) ).
cnf(s5490,plain,
( spl1_69
| ~ spl1_192 ),
inference(sat_conversion,[],[f9871]) ).
cnf(s5621,plain,
( spl1_116
| ~ spl1_193 ),
inference(sat_conversion,[],[f10028]) ).
cnf(s5758,plain,
( spl1_115
| ~ spl1_194 ),
inference(sat_conversion,[],[f10190]) ).
cnf(s5768,plain,
~ spl1_191,
inference(rat,[],[s5362,s2340]) ).
cnf(s5771,plain,
~ spl1_115,
inference(rat,[],[s3458,s1436]) ).
cnf(s5773,plain,
~ spl1_69,
inference(rat,[],[s2362,s1436]) ).
cnf(s5774,plain,
~ spl1_66,
inference(rat,[],[s2036,s1436]) ).
cnf(s5776,plain,
~ spl1_194,
inference(rat,[],[s5758,s5771]) ).
cnf(s5778,plain,
~ spl1_192,
inference(rat,[],[s5490,s5773]) ).
cnf(s5779,plain,
~ spl1_190,
inference(rat,[],[s5231,s5773]) ).
cnf(s5783,plain,
~ spl1_116,
inference(rat,[],[s3526,s5774]) ).
cnf(s5784,plain,
spl1_193,
inference(rat,[],[s4915,s5776,s5778,s5768,s5779]) ).
cnf(s5785,plain,
$false,
inference(rat,[],[s5621,s5784,s5783]) ).
fof(f10191,plain,
$false,
inference(avatar_sat_refutation,[],[s5785]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV569+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n006.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 06:38:10 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 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
% 4.98/1.19 % (3770808)Will run a generic schedule for satisfiability detection.
% 4.98/1.19 % (3770819)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=311176744:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.98/1.19 % (3770815)% WARNING: option uhcvi not known.
% 4.98/1.19 % (3770816)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3822657300:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.98/1.19 % (3770817)dis+10_1_sil=32000:sp=arity:random_seed=4026131674:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.98/1.19 % (3770814)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1603286204_2999 on theBenchmark for (2999ds/0Mi)
% 4.98/1.19 % (3770818)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=111199954:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.98/1.19 % (3770815)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1513882990:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.98/1.19 % TRYING [1]
% 4.98/1.19 % TRYING [2]
% 4.98/1.19 % (3770820)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2690215250:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.98/1.19 % TRYING [3]
% 4.98/1.19 % TRYING [4]
% 4.98/1.19 % TRYING [5]
% 4.98/1.19 % TRYING [6]
% 4.98/1.19 % TRYING [7]
% 4.98/1.19 % (3770819)Instruction limit reached!
% 4.98/1.19 % (3770819)------------------------------
% 4.98/1.19 % (3770819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770819)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770819)Termination reason: Instruction limit
% 4.98/1.19 % (3770819)Termination phase: Saturation
% 4.98/1.19 % (3770819)Time elapsed: 0.052 s
% 4.98/1.19 % (3770819)Peak memory usage: 13 MB
% 4.98/1.19 % (3770819)Instructions burned: 132 (million)
% 4.98/1.19 % (3770840)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1544113709:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.98/1.19 % TRYING [1]
% 4.98/1.19 % TRYING [8]
% 4.98/1.19 % TRYING [2]
% 4.98/1.19 % TRYING [3]
% 4.98/1.19 % TRYING [4]
% 4.98/1.19 % TRYING [5]
% 4.98/1.19 % TRYING [6]
% 4.98/1.19 % (3770817)Instruction limit reached!
% 4.98/1.19 % (3770817)------------------------------
% 4.98/1.19 % (3770817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770817)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770817)Termination reason: Instruction limit
% 4.98/1.19 % (3770817)Termination phase: Saturation
% 4.98/1.19 % (3770817)Time elapsed: 0.069 s
% 4.98/1.19 % (3770817)Peak memory usage: 12 MB
% 4.98/1.19 % (3770817)Instructions burned: 104 (million)
% 4.98/1.19 % (3770818)Instruction limit reached!
% 4.98/1.19 % (3770818)------------------------------
% 4.98/1.19 % (3770818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770818)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770818)Termination reason: Instruction limit
% 4.98/1.19 % (3770818)Termination phase: Saturation
% 4.98/1.19 % (3770818)Time elapsed: 0.071 s
% 4.98/1.19 % (3770818)Peak memory usage: 12 MB
% 4.98/1.19 % (3770818)Instructions burned: 117 (million)
% 4.98/1.19 % TRYING [7]
% 4.98/1.19 % (3770845)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=199755899:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.98/1.19 % (3770846)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=2898446067:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.98/1.19 % (3770820)Instruction limit reached!
% 4.98/1.19 % (3770820)------------------------------
% 4.98/1.19 % (3770820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770820)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770820)Termination reason: Instruction limit
% 4.98/1.19 % (3770820)Termination phase: Saturation
% 4.98/1.19 % (3770820)Time elapsed: 0.094 s
% 4.98/1.19 % (3770820)Peak memory usage: 12 MB
% 4.98/1.19 % (3770820)Instructions burned: 160 (million)
% 4.98/1.19 % (3770849)ott-21_1_sil=16000:fs=off:random_seed=4001687403:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.98/1.19 % TRYING [8]
% 4.98/1.19 % TRYING [9]
% 4.98/1.19 % (3770845)Instruction limit reached!
% 4.98/1.19 % (3770845)------------------------------
% 4.98/1.19 % (3770845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770845)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770845)Termination reason: Instruction limit
% 4.98/1.19 % (3770845)Termination phase: Saturation
% 4.98/1.19 % (3770845)Time elapsed: 0.082 s
% 4.98/1.19 % (3770845)Peak memory usage: 13 MB
% 4.98/1.19 % (3770845)Instructions burned: 131 (million)
% 4.98/1.19 % (3770851)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1546901771:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 4.98/1.19 % (3770849)Instruction limit reached!
% 4.98/1.19 % (3770849)------------------------------
% 4.98/1.19 % (3770849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770849)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770849)Termination reason: Instruction limit
% 4.98/1.19 % (3770849)Termination phase: Saturation
% 4.98/1.19 % (3770849)Time elapsed: 0.092 s
% 4.98/1.19 % (3770849)Peak memory usage: 13 MB
% 4.98/1.19 % (3770849)Instructions burned: 181 (million)
% 4.98/1.19 % (3770853)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=456656535:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.98/1.19 % TRYING [1]
% 4.98/1.19 % TRYING [2]
% 4.98/1.19 % TRYING [3]
% 4.98/1.19 % TRYING [4]
% 4.98/1.19 % (3770840)Instruction limit reached!
% 4.98/1.19 % (3770840)------------------------------
% 4.98/1.19 % (3770840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770840)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770840)Termination reason: Instruction limit
% 4.98/1.19 % (3770840)Termination phase: Finite model building SAT solving
% 4.98/1.19 % (3770840)Time elapsed: 0.198 s
% 4.98/1.19 % (3770840)Peak memory usage: 19 MB
% 4.98/1.19 % (3770840)Instructions burned: 716 (million)
% 4.98/1.19 % TRYING [5]
% 4.98/1.19 % (3770855)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3092927247:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 4.98/1.19 % TRYING [6]
% 4.98/1.19 % TRYING [7]
% 4.98/1.19 % TRYING [8]
% 4.98/1.19 % (3770851)Instruction limit reached!
% 4.98/1.19 % (3770851)------------------------------
% 4.98/1.19 % (3770851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770851)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770851)Termination reason: Instruction limit
% 4.98/1.19 % (3770851)Termination phase: Saturation
% 4.98/1.19 % (3770851)Time elapsed: 0.408 s
% 4.98/1.19 % (3770851)Peak memory usage: 14 MB
% 4.98/1.19 % (3770851)Instructions burned: 478 (million)
% 4.98/1.19 % TRYING [10]
% 4.98/1.19 % (3770846)Instruction limit reached!
% 4.98/1.19 % (3770846)------------------------------
% 4.98/1.19 % (3770846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770846)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770846)Termination reason: Instruction limit
% 4.98/1.19 % (3770846)Termination phase: Saturation
% 4.98/1.19 % (3770846)Time elapsed: 0.524 s
% 4.98/1.19 % (3770846)Peak memory usage: 18 MB
% 4.98/1.19 % (3770846)Instructions burned: 684 (million)
% 4.98/1.19 % (3770892)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1769183668:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 4.98/1.19 % TRYING [14]
% 4.98/1.19 % (3770893)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=185562857:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 4.98/1.19 % (3770815) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3770808-3770815"...
% 4.98/1.19 % (3770816) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3770808-3770816"...
% 4.98/1.19 % (3770853)Instruction limit reached!
% 4.98/1.19 % (3770853)------------------------------
% 4.98/1.19 % (3770853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770853)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770853)Termination reason: Instruction limit
% 4.98/1.19 % (3770853)Termination phase: Finite model building SAT solving
% 4.98/1.19 % (3770853)Time elapsed: 0.475 s
% 4.98/1.19 % (3770853)Peak memory usage: 16 MB
% 4.98/1.19 % (3770853)Instructions burned: 865 (million)
% 4.98/1.19 % (3770816)...printing done.
% 4.98/1.19 % (3770815)...printing done.
% 4.98/1.19 % (3770816)Refutation found. Thanks to Tanya!
% 4.98/1.19 % SZS status Theorem for theBenchmark
% 4.98/1.19 % SZS output start Proof for theBenchmark
% See solution above
% 4.98/1.19 % (3770816)------------------------------
% 4.98/1.19 % (3770816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.98/1.19 % (3770816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.98/1.19 % (3770816)CaDiCaL version: 2.1.3
% 4.98/1.19 % (3770816)Termination reason: Refutation
% 4.98/1.19 % (3770816)Time elapsed: 0.710 s
% 4.98/1.19 % (3770816)Peak memory usage: 17 MB
% 4.98/1.19 % (3770816)Instructions burned: 1026 (million)
% 4.98/1.19 % (3770808)Success in time 0.754 s
% 4.98/1.19 % Vampire exiting
%------------------------------------------------------------------------------