%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ064-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:31:26 PM UTC 2026
% Result : Unsatisfiable 15.44s 3.11s
% Output : Refutation 16.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 37
% Syntax : Number of formulae : 155 ( 63 unt; 15 def)
% Number of atoms : 294 ( 64 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 279 ( 140 ~; 135 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 5 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 17 con; 0-4 aty)
% Number of variables : 176 ( 0 sgn 176 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1630,axiom,
! [X2,X0,X1] : c_Relation_OImage(c_Relation_Odiag(X0,X1),X2,X1,X1) = c_inter(X0,X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Relation_OImage__diag_0) ).
fof(f1957,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_inter(X1,X2,X3),X3)
| c_in(X0,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OInt__iff_0) ).
fof(f1958,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_inter(X1,X2,X3),X3)
| c_in(X0,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OInt__iff_1) ).
fof(f1959,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,X2)
| ~ c_in(X0,X3,X2)
| c_in(X0,c_inter(X3,X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OInt__iff_2) ).
fof(f1960,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X0,c_inter(X1,X2,X3),tc_set(X3))
| c_lessequals(X0,X1,tc_set(X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OInt__subset__iff_0) ).
fof(f1961,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X0,c_inter(X1,X2,X3),tc_set(X3))
| c_lessequals(X0,X2,tc_set(X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OInt__subset__iff_1) ).
fof(f1962,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X0,X1,tc_set(X2))
| ~ c_lessequals(X0,X3,tc_set(X2))
| c_lessequals(X0,c_inter(X3,X1,X2),tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OInt__subset__iff_2) ).
fof(f2007,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_union(X1,X2,X3),X3)
| c_in(X0,X2,X3)
| c_in(X0,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__iff_0) ).
fof(f2008,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,c_union(X1,X3,X2),X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__iff_1) ).
fof(f2009,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,c_union(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__iff_2) ).
fof(f2051,axiom,
! [X0,X1] : ~ c_in(X0,c_emptyset,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_Oempty__iff_0) ).
fof(f2087,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,c_emptyset,tc_set(X1))
| X0 = c_emptyset ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_Osubset__empty_0) ).
fof(f2088,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_emptyset,tc_set(X1))
| c_emptyset = X0 ),
inference(reorient_equations,[],[f2087]) ).
fof(f2254,axiom,
! [X2,X0,X1] :
( c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OsubsetI_0) ).
fof(f2258,axiom,
! [X0,X1] : c_lessequals(X0,X0,tc_set(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_Osubset__refl_0) ).
fof(f3311,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,tc_set(X2))
| ~ c_in(X3,c_Mutil_Otiling(X1,X2),tc_set(X2))
| c_inter(X0,X3,X2) != c_emptyset
| c_in(c_union(X0,X3,X2),c_Mutil_Otiling(X1,X2),tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Mutil_Otiling_OUn_0) ).
fof(f3312,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,X1,tc_set(X2))
| ~ c_in(X3,c_Mutil_Otiling(X1,X2),tc_set(X2))
| c_emptyset != c_inter(X0,X3,X2)
| c_in(c_union(X0,X3,X2),c_Mutil_Otiling(X1,X2),tc_set(X2)) ),
inference(reorient_equations,[],[f3311]) ).
fof(f3314,axiom,
! [X2,X3,X0,X1] : c_union(c_union(X0,X1,X2),X3,X2) = c_union(X0,c_union(X1,X3,X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__assoc_0) ).
fof(f3315,negated_conjecture,
c_in(v_a,v_A,tc_set(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f3317,negated_conjecture,
c_inter(v_a,v_t,t_a) = c_emptyset,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f3318,plain,
c_emptyset = c_inter(v_a,v_t,t_a),
inference(reorient_equations,[],[f3317]) ).
fof(f3319,negated_conjecture,
c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f3320,negated_conjecture,
c_inter(c_union(v_a,v_t,t_a),v_u,t_a) = c_emptyset,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f3321,plain,
c_emptyset = c_inter(c_union(v_a,v_t,t_a),v_u,t_a),
inference(reorient_equations,[],[f3320]) ).
fof(f3322,negated_conjecture,
~ c_in(c_union(c_union(v_a,v_t,t_a),v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f3323,negated_conjecture,
( c_in(c_union(v_t,v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a))
| c_inter(v_t,v_u,t_a) != c_emptyset
| ~ c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f3324,plain,
( c_in(c_union(v_t,v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a))
| c_emptyset != c_inter(v_t,v_u,t_a)
| ~ c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)) ),
inference(reorient_equations,[],[f3323]) ).
fof(f3504,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Relation_OImage(c_Relation_Odiag(X1,X3),X2,X3,X3),X3)
| c_in(X0,X1,X3) ),
inference(definition_unfolding,[],[f1957,f1630]) ).
fof(f3505,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_Relation_OImage(c_Relation_Odiag(X1,X3),X2,X3,X3),X3)
| c_in(X0,X2,X3) ),
inference(definition_unfolding,[],[f1958,f1630]) ).
fof(f3506,plain,
! [X2,X3,X0,X1] :
( c_in(X0,c_Relation_OImage(c_Relation_Odiag(X3,X2),X1,X2,X2),X2)
| ~ c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(definition_unfolding,[],[f1959,f1630]) ).
fof(f3507,plain,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(c_Relation_Odiag(X1,X3),X2,X3,X3),tc_set(X3))
| c_lessequals(X0,X1,tc_set(X3)) ),
inference(definition_unfolding,[],[f1960,f1630]) ).
fof(f3508,plain,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(c_Relation_Odiag(X1,X3),X2,X3,X3),tc_set(X3))
| c_lessequals(X0,X2,tc_set(X3)) ),
inference(definition_unfolding,[],[f1961,f1630]) ).
fof(f3509,plain,
! [X2,X3,X0,X1] :
( c_lessequals(X0,c_Relation_OImage(c_Relation_Odiag(X3,X2),X1,X2,X2),tc_set(X2))
| ~ c_lessequals(X0,X3,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(definition_unfolding,[],[f1962,f1630]) ).
fof(f3547,plain,
! [X2,X3,X0,X1] :
( c_in(c_union(X0,X3,X2),c_Mutil_Otiling(X1,X2),tc_set(X2))
| ~ c_in(X3,c_Mutil_Otiling(X1,X2),tc_set(X2))
| c_emptyset != c_Relation_OImage(c_Relation_Odiag(X0,X2),X3,X2,X2)
| ~ c_in(X0,X1,tc_set(X2)) ),
inference(definition_unfolding,[],[f3312,f1630]) ).
fof(f3548,plain,
c_emptyset = c_Relation_OImage(c_Relation_Odiag(v_a,t_a),v_t,t_a,t_a),
inference(definition_unfolding,[],[f3318,f1630]) ).
fof(f3549,plain,
c_emptyset = c_Relation_OImage(c_Relation_Odiag(c_union(v_a,v_t,t_a),t_a),v_u,t_a,t_a),
inference(definition_unfolding,[],[f3321,f1630]) ).
fof(f3550,plain,
( c_in(c_union(v_t,v_u,t_a),c_Mutil_Otiling(v_A,t_a),tc_set(t_a))
| c_emptyset != c_Relation_OImage(c_Relation_Odiag(v_t,t_a),v_u,t_a,t_a)
| ~ c_in(v_u,c_Mutil_Otiling(v_A,t_a),tc_set(t_a)) ),
inference(definition_unfolding,[],[f3324,f1630]) ).
fof(f3551,definition,
sF0 = tc_set(t_a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f3552,plain,
tc_set(t_a) = sF0,
inference(reorient_equations,[],[f3551]) ).
fof(f3553,plain,
c_in(v_a,v_A,sF0),
inference(definition_folding,[],[f3315,f3552]) ).
fof(f3554,definition,
sF1 = c_Mutil_Otiling(v_A,t_a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f3555,plain,
c_Mutil_Otiling(v_A,t_a) = sF1,
inference(reorient_equations,[],[f3554]) ).
fof(f3557,definition,
sF2 = c_Relation_Odiag(v_a,t_a),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f3558,plain,
c_Relation_Odiag(v_a,t_a) = sF2,
inference(reorient_equations,[],[f3557]) ).
fof(f3559,definition,
sF3 = c_Relation_OImage(sF2,v_t,t_a,t_a),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f3560,plain,
c_Relation_OImage(sF2,v_t,t_a,t_a) = sF3,
inference(reorient_equations,[],[f3559]) ).
fof(f3561,plain,
c_emptyset = sF3,
inference(definition_folding,[],[f3548,f3560,f3558]) ).
fof(f3562,plain,
c_in(v_u,sF1,sF0),
inference(definition_folding,[],[f3319,f3552,f3555]) ).
fof(f3563,definition,
sF4 = c_union(v_a,v_t,t_a),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f3564,plain,
c_union(v_a,v_t,t_a) = sF4,
inference(reorient_equations,[],[f3563]) ).
fof(f3565,definition,
sF5 = c_Relation_Odiag(sF4,t_a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f3566,plain,
c_Relation_Odiag(sF4,t_a) = sF5,
inference(reorient_equations,[],[f3565]) ).
fof(f3567,definition,
sF6 = c_Relation_OImage(sF5,v_u,t_a,t_a),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f3568,plain,
c_Relation_OImage(sF5,v_u,t_a,t_a) = sF6,
inference(reorient_equations,[],[f3567]) ).
fof(f3569,plain,
c_emptyset = sF6,
inference(definition_folding,[],[f3549,f3568,f3566,f3564]) ).
fof(f3570,definition,
sF7 = c_union(sF4,v_u,t_a),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f3571,plain,
c_union(sF4,v_u,t_a) = sF7,
inference(reorient_equations,[],[f3570]) ).
fof(f3572,plain,
~ c_in(sF7,sF1,sF0),
inference(definition_folding,[],[f3322,f3552,f3555,f3571,f3564]) ).
fof(f3573,definition,
sF8 = c_union(v_t,v_u,t_a),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f3574,plain,
c_union(v_t,v_u,t_a) = sF8,
inference(reorient_equations,[],[f3573]) ).
fof(f3575,definition,
sF9 = c_Relation_Odiag(v_t,t_a),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f3576,plain,
c_Relation_Odiag(v_t,t_a) = sF9,
inference(reorient_equations,[],[f3575]) ).
fof(f3577,definition,
sF10 = c_Relation_OImage(sF9,v_u,t_a,t_a),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f3578,plain,
c_Relation_OImage(sF9,v_u,t_a,t_a) = sF10,
inference(reorient_equations,[],[f3577]) ).
fof(f3579,plain,
( c_in(sF8,sF1,sF0)
| c_emptyset != sF10
| ~ c_in(v_u,sF1,sF0) ),
inference(definition_folding,[],[f3550,f3552,f3555,f3578,f3576,f3552,f3555,f3574]) ).
fof(f3582,definition,
( spl11_1
<=> c_in(v_u,sF1,sF0) ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
fof(f3586,definition,
( spl11_2
<=> c_emptyset = sF10 ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f3588,plain,
( c_emptyset != sF10
| spl11_2 ),
inference(avatar_component_clause,[],[f3586]) ).
fof(f3590,definition,
( spl11_3
<=> c_in(sF8,sF1,sF0) ),
introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition]) ).
fof(f3593,plain,
( ~ spl11_1
| ~ spl11_2
| spl11_3 ),
inference(avatar_split_clause,[],[f3579,f3590,f3586,f3582]) ).
fof(f3594,plain,
spl11_1,
inference(avatar_split_clause,[],[f3562,f3582]) ).
fof(f3731,plain,
c_emptyset = c_Relation_OImage(sF2,v_t,t_a,t_a),
inference(forward_demodulation,[],[f3560,f3561]) ).
fof(f3732,plain,
c_emptyset = c_Relation_OImage(sF5,v_u,t_a,t_a),
inference(forward_demodulation,[],[f3568,f3569]) ).
fof(f3787,plain,
! [X0] : c_union(v_a,c_union(v_t,X0,t_a),t_a) = c_union(sF4,X0,t_a),
inference(superposition,[],[f3314,f3564]) ).
fof(f3792,plain,
! [X0,X1] :
( c_in(c_union(X0,X1,t_a),sF1,tc_set(t_a))
| ~ c_in(X1,sF1,tc_set(t_a))
| c_emptyset != c_Relation_OImage(c_Relation_Odiag(X0,t_a),X1,t_a,t_a)
| ~ c_in(X0,v_A,tc_set(t_a)) ),
inference(superposition,[],[f3547,f3555]) ).
fof(f3793,plain,
! [X0,X1] :
( c_in(c_union(X0,X1,t_a),sF1,sF0)
| ~ c_in(X1,sF1,tc_set(t_a))
| c_emptyset != c_Relation_OImage(c_Relation_Odiag(X0,t_a),X1,t_a,t_a)
| ~ c_in(X0,v_A,tc_set(t_a)) ),
inference(forward_demodulation,[],[f3792,f3552]) ).
fof(f3796,plain,
! [X0,X1] :
( ~ c_in(X1,sF1,sF0)
| c_in(c_union(X0,X1,t_a),sF1,sF0)
| c_emptyset != c_Relation_OImage(c_Relation_Odiag(X0,t_a),X1,t_a,t_a)
| ~ c_in(X0,v_A,tc_set(t_a)) ),
inference(forward_demodulation,[],[f3793,f3552]) ).
fof(f3799,plain,
! [X0,X1] :
( c_emptyset != c_Relation_OImage(c_Relation_Odiag(X0,t_a),X1,t_a,t_a)
| ~ c_in(X1,sF1,sF0)
| c_in(c_union(X0,X1,t_a),sF1,sF0)
| ~ c_in(X0,v_A,sF0) ),
inference(forward_demodulation,[],[f3796,f3552]) ).
fof(f3812,plain,
! [X0,X1] :
( ~ c_in(X0,c_Relation_OImage(sF9,X1,t_a,t_a),t_a)
| c_in(X0,X1,t_a) ),
inference(superposition,[],[f3505,f3576]) ).
fof(f3813,plain,
! [X0,X1] :
( ~ c_in(X0,c_Relation_OImage(sF2,X1,t_a,t_a),t_a)
| c_in(X0,X1,t_a) ),
inference(superposition,[],[f3505,f3558]) ).
fof(f3816,plain,
! [X0,X1] :
( ~ c_in(X0,c_Relation_OImage(sF9,X1,t_a,t_a),t_a)
| c_in(X0,v_t,t_a) ),
inference(superposition,[],[f3504,f3576]) ).
fof(f3817,plain,
! [X0,X1] :
( ~ c_in(X0,c_Relation_OImage(sF2,X1,t_a,t_a),t_a)
| c_in(X0,v_a,t_a) ),
inference(superposition,[],[f3504,f3558]) ).
fof(f3823,plain,
! [X0,X1] :
( c_in(X0,c_Relation_OImage(sF2,X1,t_a,t_a),t_a)
| ~ c_in(X0,v_a,t_a)
| ~ c_in(X0,X1,t_a) ),
inference(superposition,[],[f3506,f3558]) ).
fof(f3824,plain,
! [X0,X1] :
( c_in(X0,c_Relation_OImage(sF5,X1,t_a,t_a),t_a)
| ~ c_in(X0,sF4,t_a)
| ~ c_in(X0,X1,t_a) ),
inference(superposition,[],[f3506,f3566]) ).
fof(f3830,plain,
! [X0] :
( c_in(X0,sF4,t_a)
| ~ c_in(X0,v_t,t_a) ),
inference(superposition,[],[f2009,f3564]) ).
fof(f3834,plain,
! [X0] :
( c_in(X0,sF4,t_a)
| ~ c_in(X0,v_a,t_a) ),
inference(superposition,[],[f2008,f3564]) ).
fof(f3840,plain,
! [X0] :
( c_in(X0,v_u,t_a)
| ~ c_in(X0,sF8,t_a)
| c_in(X0,v_t,t_a) ),
inference(superposition,[],[f2007,f3574]) ).
fof(f3849,plain,
! [X0] :
( c_emptyset != c_Relation_OImage(sF2,X0,t_a,t_a)
| ~ c_in(X0,sF1,sF0)
| c_in(c_union(v_a,X0,t_a),sF1,sF0)
| ~ c_in(v_a,v_A,sF0) ),
inference(superposition,[],[f3799,f3558]) ).
fof(f3856,plain,
! [X0] :
( c_in(c_union(v_a,X0,t_a),sF1,sF0)
| ~ c_in(X0,sF1,sF0)
| c_emptyset != c_Relation_OImage(sF2,X0,t_a,t_a) ),
inference(forward_subsumption_resolution,[],[f3849,f3553]) ).
fof(f3904,plain,
! [X0] :
( c_in(X0,c_emptyset,t_a)
| ~ c_in(X0,v_a,t_a)
| ~ c_in(X0,v_t,t_a) ),
inference(superposition,[],[f3823,f3731]) ).
fof(f3906,plain,
! [X0] :
( ~ c_in(X0,v_t,t_a)
| ~ c_in(X0,v_a,t_a) ),
inference(forward_subsumption_resolution,[],[f3904,f2051]) ).
fof(f3916,plain,
! [X0] :
( c_in(X0,v_t,t_a)
| ~ c_in(X0,sF10,t_a) ),
inference(superposition,[],[f3816,f3578]) ).
fof(f3928,plain,
! [X0] :
( c_in(X0,v_u,t_a)
| ~ c_in(X0,sF10,t_a) ),
inference(superposition,[],[f3812,f3578]) ).
fof(f3957,plain,
! [X0] : c_lessequals(X0,X0,sF0),
inference(superposition,[],[f2258,f3552]) ).
fof(f3993,plain,
c_union(sF4,v_u,t_a) = c_union(v_a,sF8,t_a),
inference(superposition,[],[f3787,f3574]) ).
fof(f4008,plain,
sF7 = c_union(v_a,sF8,t_a),
inference(forward_demodulation,[],[f3993,f3571]) ).
fof(f4013,plain,
( c_in(sF7,sF1,sF0)
| ~ c_in(sF8,sF1,sF0)
| c_emptyset != c_Relation_OImage(sF2,sF8,t_a,t_a) ),
inference(superposition,[],[f3856,f4008]) ).
fof(f4022,plain,
( ~ c_in(sF8,sF1,sF0)
| c_emptyset != c_Relation_OImage(sF2,sF8,t_a,t_a) ),
inference(forward_subsumption_resolution,[],[f4013,f3572]) ).
fof(f4028,definition,
( spl11_11
<=> c_emptyset = c_Relation_OImage(sF2,sF8,t_a,t_a) ),
introduced(definition,[new_symbols(definition,[spl11_11])],[avatar_definition]) ).
fof(f4030,plain,
( c_emptyset != c_Relation_OImage(sF2,sF8,t_a,t_a)
| spl11_11 ),
inference(avatar_component_clause,[],[f4028]) ).
fof(f4032,plain,
( ~ spl11_11
| ~ spl11_3 ),
inference(avatar_split_clause,[],[f4022,f3590,f4028]) ).
fof(f4040,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(sF2,X1,t_a,t_a),tc_set(t_a))
| c_lessequals(X0,v_a,tc_set(t_a)) ),
inference(superposition,[],[f3507,f3558]) ).
fof(f4049,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(sF2,X1,t_a,t_a),sF0)
| c_lessequals(X0,v_a,tc_set(t_a)) ),
inference(forward_demodulation,[],[f4040,f3552]) ).
fof(f4052,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(sF2,X1,t_a,t_a),sF0)
| c_lessequals(X0,v_a,sF0) ),
inference(forward_demodulation,[],[f4049,f3552]) ).
fof(f4072,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(sF9,X1,t_a,t_a),tc_set(t_a))
| c_lessequals(X0,X1,tc_set(t_a)) ),
inference(superposition,[],[f3508,f3576]) ).
fof(f4084,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(sF9,X1,t_a,t_a),sF0)
| c_lessequals(X0,X1,tc_set(t_a)) ),
inference(forward_demodulation,[],[f4072,f3552]) ).
fof(f4087,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_Relation_OImage(sF9,X1,t_a,t_a),sF0)
| c_lessequals(X0,X1,sF0) ),
inference(forward_demodulation,[],[f4084,f3552]) ).
fof(f4221,plain,
! [X0] :
( c_in(X0,c_emptyset,t_a)
| ~ c_in(X0,sF4,t_a)
| ~ c_in(X0,v_u,t_a) ),
inference(superposition,[],[f3824,f3732]) ).
fof(f4225,plain,
! [X0] :
( ~ c_in(X0,sF4,t_a)
| ~ c_in(X0,v_u,t_a) ),
inference(forward_subsumption_resolution,[],[f4221,f2051]) ).
fof(f4227,plain,
! [X0] :
( ~ c_in(X0,v_u,t_a)
| ~ c_in(X0,v_a,t_a) ),
inference(resolution,[],[f4225,f3834]) ).
fof(f4228,plain,
! [X0] :
( ~ c_in(X0,v_u,t_a)
| ~ c_in(X0,v_t,t_a) ),
inference(resolution,[],[f4225,f3830]) ).
fof(f4230,plain,
! [X0] :
( ~ c_in(X0,v_a,t_a)
| ~ c_in(X0,sF8,t_a)
| c_in(X0,v_t,t_a) ),
inference(resolution,[],[f4227,f3840]) ).
fof(f4231,plain,
! [X0] :
( ~ c_in(X0,sF8,t_a)
| ~ c_in(X0,v_a,t_a) ),
inference(forward_subsumption_resolution,[],[f4230,f3906]) ).
fof(f4234,plain,
! [X0] :
( ~ c_in(X0,v_t,t_a)
| ~ c_in(X0,sF10,t_a) ),
inference(resolution,[],[f4228,f3928]) ).
fof(f4236,plain,
! [X0] : ~ c_in(X0,sF10,t_a),
inference(forward_subsumption_resolution,[],[f4234,f3916]) ).
fof(f4476,plain,
! [X0,X1] :
( c_lessequals(X0,c_Relation_OImage(sF2,X1,t_a,t_a),tc_set(t_a))
| ~ c_lessequals(X0,v_a,tc_set(t_a))
| ~ c_lessequals(X0,X1,tc_set(t_a)) ),
inference(superposition,[],[f3509,f3558]) ).
fof(f4477,plain,
! [X0,X1] :
( c_lessequals(X0,c_Relation_OImage(sF5,X1,t_a,t_a),tc_set(t_a))
| ~ c_lessequals(X0,sF4,tc_set(t_a))
| ~ c_lessequals(X0,X1,tc_set(t_a)) ),
inference(superposition,[],[f3509,f3566]) ).
fof(f4488,plain,
! [X0,X1] :
( c_lessequals(X0,c_Relation_OImage(sF5,X1,t_a,t_a),sF0)
| ~ c_lessequals(X0,sF4,tc_set(t_a))
| ~ c_lessequals(X0,X1,tc_set(t_a)) ),
inference(forward_demodulation,[],[f4477,f3552]) ).
fof(f4489,plain,
! [X0,X1] :
( c_lessequals(X0,c_Relation_OImage(sF2,X1,t_a,t_a),sF0)
| ~ c_lessequals(X0,v_a,tc_set(t_a))
| ~ c_lessequals(X0,X1,tc_set(t_a)) ),
inference(forward_demodulation,[],[f4476,f3552]) ).
fof(f4491,plain,
! [X0,X1] :
( ~ c_lessequals(X0,sF4,sF0)
| c_lessequals(X0,c_Relation_OImage(sF5,X1,t_a,t_a),sF0)
| ~ c_lessequals(X0,X1,tc_set(t_a)) ),
inference(forward_demodulation,[],[f4488,f3552]) ).
fof(f4492,plain,
! [X0,X1] :
( ~ c_lessequals(X0,v_a,sF0)
| c_lessequals(X0,c_Relation_OImage(sF2,X1,t_a,t_a),sF0)
| ~ c_lessequals(X0,X1,tc_set(t_a)) ),
inference(forward_demodulation,[],[f4489,f3552]) ).
fof(f4494,plain,
! [X0,X1] :
( c_lessequals(X0,c_Relation_OImage(sF5,X1,t_a,t_a),sF0)
| ~ c_lessequals(X0,sF4,sF0)
| ~ c_lessequals(X0,X1,sF0) ),
inference(forward_demodulation,[],[f4491,f3552]) ).
fof(f4495,plain,
! [X0,X1] :
( c_lessequals(X0,c_Relation_OImage(sF2,X1,t_a,t_a),sF0)
| ~ c_lessequals(X0,v_a,sF0)
| ~ c_lessequals(X0,X1,sF0) ),
inference(forward_demodulation,[],[f4492,f3552]) ).
fof(f4511,plain,
! [X0] :
( c_lessequals(X0,c_emptyset,sF0)
| ~ c_lessequals(X0,v_a,sF0)
| ~ c_lessequals(X0,v_t,sF0) ),
inference(superposition,[],[f4495,f3731]) ).
fof(f4521,plain,
! [X0] :
( c_lessequals(X0,c_emptyset,sF0)
| ~ c_lessequals(X0,sF4,sF0)
| ~ c_lessequals(X0,v_u,sF0) ),
inference(superposition,[],[f4494,f3732]) ).
fof(f4956,plain,
! [X0] : c_lessequals(c_Relation_OImage(sF9,X0,t_a,t_a),X0,sF0),
inference(resolution,[],[f3957,f4087]) ).
fof(f4960,plain,
! [X0] : c_lessequals(c_Relation_OImage(sF2,X0,t_a,t_a),v_a,sF0),
inference(resolution,[],[f3957,f4052]) ).
fof(f5045,plain,
c_lessequals(sF10,v_u,sF0),
inference(superposition,[],[f4956,f3578]) ).
fof(f7452,plain,
! [X0] :
( ~ c_lessequals(X0,c_emptyset,sF0)
| c_emptyset = X0 ),
inference(superposition,[],[f2088,f3552]) ).
fof(f7453,plain,
! [X0] :
( ~ c_lessequals(X0,sF4,sF0)
| c_emptyset = X0
| ~ c_lessequals(X0,v_u,sF0) ),
inference(resolution,[],[f7452,f4521]) ).
fof(f7454,plain,
! [X0] :
( ~ c_lessequals(X0,v_t,sF0)
| ~ c_lessequals(X0,v_a,sF0)
| c_emptyset = X0 ),
inference(resolution,[],[f7452,f4511]) ).
fof(f12793,plain,
! [X0,X1] :
( c_lessequals(c_Relation_OImage(sF2,X0,t_a,t_a),X1,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_Relation_OImage(sF2,X0,t_a,t_a),X1,t_a),v_a,t_a) ),
inference(resolution,[],[f2254,f3817]) ).
fof(f12794,plain,
! [X0,X1] :
( c_lessequals(c_Relation_OImage(sF2,X0,t_a,t_a),X1,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_Relation_OImage(sF2,X0,t_a,t_a),X1,t_a),X0,t_a) ),
inference(resolution,[],[f2254,f3813]) ).
fof(f12799,plain,
! [X0] : c_lessequals(sF10,X0,tc_set(t_a)),
inference(resolution,[],[f2254,f4236]) ).
fof(f12805,plain,
! [X0] : c_lessequals(sF10,X0,sF0),
inference(forward_demodulation,[],[f12799,f3552]) ).
fof(f12810,plain,
! [X0,X1] :
( c_in(c_Main_OsubsetI__1(c_Relation_OImage(sF2,X0,t_a,t_a),X1,t_a),X0,t_a)
| c_lessequals(c_Relation_OImage(sF2,X0,t_a,t_a),X1,sF0) ),
inference(forward_demodulation,[],[f12794,f3552]) ).
fof(f12811,plain,
! [X0,X1] :
( c_in(c_Main_OsubsetI__1(c_Relation_OImage(sF2,X0,t_a,t_a),X1,t_a),v_a,t_a)
| c_lessequals(c_Relation_OImage(sF2,X0,t_a,t_a),X1,sF0) ),
inference(forward_demodulation,[],[f12793,f3552]) ).
fof(f12835,plain,
( c_emptyset = sF10
| ~ c_lessequals(sF10,v_u,sF0) ),
inference(resolution,[],[f12805,f7453]) ).
fof(f12840,plain,
( ~ c_lessequals(sF10,v_u,sF0)
| spl11_2 ),
inference(forward_subsumption_resolution,[],[f12835,f3588]) ).
fof(f12843,plain,
( $false
| spl11_2 ),
inference(forward_subsumption_resolution,[],[f12840,f5045]) ).
fof(f12844,plain,
spl11_2,
inference(avatar_contradiction_clause,[],[f12843]) ).
fof(f15062,plain,
! [X0] :
( c_lessequals(c_Relation_OImage(sF2,sF8,t_a,t_a),X0,sF0)
| ~ c_in(c_Main_OsubsetI__1(c_Relation_OImage(sF2,sF8,t_a,t_a),X0,t_a),v_a,t_a) ),
inference(resolution,[],[f12810,f4231]) ).
fof(f15081,plain,
! [X0] : c_lessequals(c_Relation_OImage(sF2,sF8,t_a,t_a),X0,sF0),
inference(forward_subsumption_resolution,[],[f15062,f12811]) ).
fof(f15098,plain,
( ~ c_lessequals(c_Relation_OImage(sF2,sF8,t_a,t_a),v_a,sF0)
| c_emptyset = c_Relation_OImage(sF2,sF8,t_a,t_a) ),
inference(resolution,[],[f15081,f7454]) ).
fof(f15107,plain,
c_emptyset = c_Relation_OImage(sF2,sF8,t_a,t_a),
inference(forward_subsumption_resolution,[],[f15098,f4960]) ).
fof(f15112,plain,
( $false
| spl11_11 ),
inference(forward_subsumption_resolution,[],[f15107,f4030]) ).
fof(f15113,plain,
spl11_11,
inference(avatar_contradiction_clause,[],[f15112]) ).
cnf(s1,plain,
( ~ spl11_1
| ~ spl11_2
| spl11_3 ),
inference(sat_conversion,[],[f3593]) ).
cnf(s2,plain,
spl11_1,
inference(sat_conversion,[],[f3594]) ).
cnf(s11,plain,
( ~ spl11_3
| ~ spl11_11 ),
inference(sat_conversion,[],[f4032]) ).
cnf(s164,plain,
spl11_2,
inference(sat_conversion,[],[f12844]) ).
cnf(s175,plain,
spl11_11,
inference(sat_conversion,[],[f15113]) ).
cnf(s189,plain,
~ spl11_3,
inference(rat,[],[s11,s175]) ).
cnf(s195,plain,
$false,
inference(rat,[],[s1,s189,s164,s2]) ).
fof(f15114,plain,
$false,
inference(avatar_sat_refutation,[],[s195]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ064-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 22:38:16 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.73/2.49 % (1238660)Input is clausal, will run a generic CNF schedule.
% 10.73/2.49 % (1238669)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1825311288:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.73/2.49 % (1238665)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3673486544:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.73/2.49 % (1238667)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=401970603:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.73/2.49 % (1238668)lrs+10_1_sil=8000:sp=occurrence:random_seed=126583000:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.73/2.49 % (1238671)dis-21_1_sil=8000:lcm=predicate:random_seed=3741332879:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.73/2.49 % (1238666)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2463299499:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.73/2.49 % (1238669)Instruction limit reached!
% 10.73/2.49 % (1238669)------------------------------
% 10.73/2.49 % (1238669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.49 % (1238669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.49 % (1238669)CaDiCaL version: 2.1.3
% 10.73/2.49 % (1238669)Termination reason: Instruction limit
% 10.73/2.49 % (1238669)Termination phase: Saturation
% 10.73/2.49 % (1238669)Time elapsed: 0.039 s
% 10.73/2.49 % (1238669)Peak memory usage: 91 MB
% 10.73/2.49 % (1238669)Instructions burned: 115 (million)
% 10.73/2.49 % (1238670)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3531803907:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.73/2.49 % (1238671)Instruction limit reached!
% 10.73/2.49 % (1238671)------------------------------
% 10.73/2.49 % (1238671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.49 % (1238671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.49 % (1238671)CaDiCaL version: 2.1.3
% 10.73/2.49 % (1238671)Termination reason: Instruction limit
% 10.73/2.49 % (1238671)Termination phase: Saturation
% 10.73/2.49 % (1238671)Time elapsed: 0.065 s
% 10.73/2.49 % (1238671)Peak memory usage: 90 MB
% 10.73/2.49 % (1238671)Instructions burned: 118 (million)
% 10.73/2.49 % (1238668)Instruction limit reached!
% 10.73/2.49 % (1238668)------------------------------
% 10.73/2.49 % (1238668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.49 % (1238668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.49 % (1238668)CaDiCaL version: 2.1.3
% 10.73/2.49 % (1238668)Termination reason: Instruction limit
% 10.73/2.49 % (1238668)Termination phase: Saturation
% 10.73/2.49 % (1238668)Time elapsed: 0.076 s
% 10.73/2.49 % (1238668)Peak memory usage: 91 MB
% 10.73/2.49 % (1238668)Instructions burned: 108 (million)
% 10.73/2.49 % (1238678)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=976422585:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.73/2.49 % (1238670)Instruction limit reached!
% 10.73/2.49 % (1238670)------------------------------
% 10.73/2.49 % (1238670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.49 % (1238670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.49 % (1238670)CaDiCaL version: 2.1.3
% 10.73/2.49 % (1238670)Termination reason: Instruction limit
% 10.73/2.49 % (1238670)Termination phase: Saturation
% 10.73/2.49 % (1238670)Time elapsed: 0.113 s
% 10.73/2.49 % (1238670)Peak memory usage: 91 MB
% 10.73/2.49 % (1238670)Instructions burned: 181 (million)
% 10.73/2.49 % (1238678)Instruction limit reached!
% 10.73/2.49 % (1238678)------------------------------
% 10.73/2.49 % (1238678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.73/2.49 % (1238678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.73/2.49 % (1238678)CaDiCaL version: 2.1.3
% 10.73/2.49 % (1238678)Termination reason: Instruction limit
% 10.73/2.49 % (1238678)Termination phase: Saturation
% 10.73/2.49 % (1238678)Time elapsed: 0.049 s
% 10.73/2.49 % (1238678)Peak memory usage: 91 MB
% 10.73/2.49 % (1238678)Instructions burned: 146 (million)
% 10.73/2.49 % (1238680)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3060253567:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 15.44/3.11 % (1238681)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3693147610:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 15.44/3.11 % (1238683)lrs+10_64_to=lpo:sil=8000:random_seed=1645030790:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 15.44/3.11 % (1238684)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4031056197:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 15.44/3.11 % (1238680)Instruction limit reached!
% 15.44/3.11 % (1238680)------------------------------
% 15.44/3.11 % (1238680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238680)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238680)Termination reason: Instruction limit
% 15.44/3.11 % (1238680)Termination phase: Saturation
% 15.44/3.11 % (1238680)Time elapsed: 0.114 s
% 15.44/3.11 % (1238680)Peak memory usage: 92 MB
% 15.44/3.11 % (1238680)Instructions burned: 189 (million)
% 15.44/3.11 % (1238683)Instruction limit reached!
% 15.44/3.11 % (1238683)------------------------------
% 15.44/3.11 % (1238683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238683)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238683)Termination reason: Instruction limit
% 15.44/3.11 % (1238683)Termination phase: Saturation
% 15.44/3.11 % (1238683)Time elapsed: 0.073 s
% 15.44/3.11 % (1238683)Peak memory usage: 92 MB
% 15.44/3.11 % (1238683)Instructions burned: 127 (million)
% 15.44/3.11 % (1238684)Instruction limit reached!
% 15.44/3.11 % (1238684)------------------------------
% 15.44/3.11 % (1238684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238684)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238684)Termination reason: Instruction limit
% 15.44/3.11 % (1238684)Termination phase: Saturation
% 15.44/3.11 % (1238684)Time elapsed: 0.059 s
% 15.44/3.11 % (1238684)Peak memory usage: 92 MB
% 15.44/3.11 % (1238684)Instructions burned: 196 (million)
% 15.44/3.11 % (1238681)Instruction limit reached!
% 15.44/3.11 % (1238681)------------------------------
% 15.44/3.11 % (1238681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238681)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238681)Termination reason: Instruction limit
% 15.44/3.11 % (1238681)Termination phase: Saturation
% 15.44/3.11 % (1238681)Time elapsed: 0.133 s
% 15.44/3.11 % (1238681)Peak memory usage: 93 MB
% 15.44/3.11 % (1238681)Instructions burned: 219 (million)
% 15.44/3.11 % (1238690)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=360444448:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 15.44/3.11 % (1238691)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1524405709:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 15.44/3.11 % (1238689)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3843096838:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 15.44/3.11 % (1238692)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1648375893:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 15.44/3.11 % (1238691)Instruction limit reached!
% 15.44/3.11 % (1238691)------------------------------
% 15.44/3.11 % (1238691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238691)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238691)Termination reason: Instruction limit
% 15.44/3.11 % (1238691)Termination phase: Saturation
% 15.44/3.11 % (1238691)Time elapsed: 0.065 s
% 15.44/3.11 % (1238691)Peak memory usage: 91 MB
% 15.44/3.11 % (1238691)Instructions burned: 106 (million)
% 15.44/3.11 % (1238689)Instruction limit reached!
% 15.44/3.11 % (1238689)------------------------------
% 15.44/3.11 % (1238689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238689)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238689)Termination reason: Instruction limit
% 15.44/3.11 % (1238689)Termination phase: Saturation
% 15.44/3.11 % (1238689)Time elapsed: 0.084 s
% 15.44/3.11 % (1238689)Peak memory usage: 92 MB
% 15.44/3.11 % (1238689)Instructions burned: 157 (million)
% 15.44/3.11 % (1238692)Instruction limit reached!
% 15.44/3.11 % (1238692)------------------------------
% 15.44/3.11 % (1238692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238692)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238692)Termination reason: Instruction limit
% 15.44/3.11 % (1238692)Termination phase: Saturation
% 15.44/3.11 % (1238692)Time elapsed: 0.068 s
% 15.44/3.11 % (1238692)Peak memory usage: 92 MB
% 15.44/3.11 % (1238692)Instructions burned: 107 (million)
% 15.44/3.11 % (1238697)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1150096644:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 15.44/3.11 % (1238698)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2476585954:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 15.44/3.11 % (1238699)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1495419062:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 15.44/3.11 % (1238699)Instruction limit reached!
% 15.44/3.11 % (1238699)------------------------------
% 15.44/3.11 % (1238699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238699)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238699)Termination reason: Instruction limit
% 15.44/3.11 % (1238699)Termination phase: Saturation
% 15.44/3.11 % (1238699)Time elapsed: 0.071 s
% 15.44/3.11 % (1238699)Peak memory usage: 90 MB
% 15.44/3.11 % (1238699)Instructions burned: 136 (million)
% 15.44/3.11 % (1238697)Instruction limit reached!
% 15.44/3.11 % (1238697)------------------------------
% 15.44/3.11 % (1238697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238697)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238697)Termination reason: Instruction limit
% 15.44/3.11 % (1238697)Termination phase: Saturation
% 15.44/3.11 % (1238697)Time elapsed: 0.131 s
% 15.44/3.11 % (1238697)Peak memory usage: 91 MB
% 15.44/3.11 % (1238697)Instructions burned: 242 (million)
% 15.44/3.11 % (1238703)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2810197292:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 15.44/3.11 % (1238704)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2244602834:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 15.44/3.11 % (1238704)Instruction limit reached!
% 15.44/3.11 % (1238704)------------------------------
% 15.44/3.11 % (1238704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238704)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238704)Termination reason: Instruction limit
% 15.44/3.11 % (1238704)Termination phase: Saturation
% 15.44/3.11 % (1238704)Time elapsed: 0.111 s
% 15.44/3.11 % (1238704)Peak memory usage: 92 MB
% 15.44/3.11 % (1238704)Instructions burned: 192 (million)
% 15.44/3.11 % (1238703)Instruction limit reached!
% 15.44/3.11 % (1238703)------------------------------
% 15.44/3.11 % (1238703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238703)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238703)Termination reason: Instruction limit
% 15.44/3.11 % (1238703)Termination phase: Saturation
% 15.44/3.11 % (1238703)Time elapsed: 0.266 s
% 15.44/3.11 % (1238703)Peak memory usage: 99 MB
% 15.44/3.11 % (1238703)Instructions burned: 499 (million)
% 15.44/3.11 % (1238707)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1488596329:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 15.44/3.11 % (1238707)Instruction limit reached!
% 15.44/3.11 % (1238707)------------------------------
% 15.44/3.11 % (1238707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238707)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238707)Termination reason: Instruction limit
% 15.44/3.11 % (1238707)Termination phase: Saturation
% 15.44/3.11 % (1238707)Time elapsed: 0.123 s
% 15.44/3.11 % (1238707)Peak memory usage: 94 MB
% 15.44/3.11 % (1238707)Instructions burned: 265 (million)
% 15.44/3.11 % (1238708)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=959822075:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 15.44/3.11 % (1238708)Instruction limit reached!
% 15.44/3.11 % (1238708)------------------------------
% 15.44/3.11 % (1238708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238708)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238708)Termination reason: Instruction limit
% 15.44/3.11 % (1238708)Termination phase: Saturation
% 15.44/3.11 % (1238708)Time elapsed: 0.085 s
% 15.44/3.11 % (1238708)Peak memory usage: 91 MB
% 15.44/3.11 % (1238708)Instructions burned: 157 (million)
% 15.44/3.11 % (1238710)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=4103241685:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 15.44/3.11 % (1238690)Instruction limit reached!
% 15.44/3.11 % (1238690)------------------------------
% 15.44/3.11 % (1238690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238690)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238690)Termination reason: Instruction limit
% 15.44/3.11 % (1238690)Termination phase: Saturation
% 15.44/3.11 % (1238690)Time elapsed: 1.163 s
% 15.44/3.11 % (1238690)Peak memory usage: 152 MB
% 15.44/3.11 % (1238690)Instructions burned: 3394 (million)
% 15.44/3.11 % (1238712)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2588049350:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 15.44/3.11 % (1238667)First to succeed.
% 15.44/3.11 % (1238667)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1238660"
% 15.44/3.11 % (1238714)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3491273179:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 15.44/3.11 % (1238714)Instruction limit reached!
% 15.44/3.11 % (1238714)------------------------------
% 15.44/3.11 % (1238714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238714)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238714)Termination reason: Instruction limit
% 15.44/3.11 % (1238714)Termination phase: Saturation
% 15.44/3.11 % (1238714)Time elapsed: 0.056 s
% 15.44/3.11 % (1238714)Peak memory usage: 92 MB
% 15.44/3.11 % (1238714)Instructions burned: 182 (million)
% 15.44/3.11 % (1238717)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4051872525:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi)
% 15.44/3.11 % (1238712)Instruction limit reached!
% 15.44/3.11 % (1238712)------------------------------
% 15.44/3.11 % (1238712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.44/3.11 % (1238712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/3.11 % (1238712)CaDiCaL version: 2.1.3
% 15.44/3.11 % (1238712)Termination reason: Instruction limit
% 15.44/3.11 % (1238712)Termination phase: Saturation
% 15.44/3.11 % (1238712)Time elapsed: 0.309 s
% 15.44/3.11 % (1238712)Peak memory usage: 94 MB
% 15.44/3.11 % (1238712)Instructions burned: 538 (million)
% 15.44/3.11 % (1238667)Refutation found. Thanks to Tanya!
% 15.44/3.11 % SZS status Unsatisfiable for theBenchmark
% 15.44/3.11 % SZS output start Proof for theBenchmark
% See solution above
% 16.10/3.21 % (1238667)------------------------------
% 16.10/3.21 % (1238667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.10/3.21 % (1238667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.10/3.21 % (1238667)CaDiCaL version: 2.1.3
% 16.10/3.21 % (1238667)Termination reason: Refutation
% 16.10/3.21 % (1238667)Time elapsed: 1.722 s
% 16.10/3.21 % (1238667)Peak memory usage: 157 MB
% 16.10/3.21 % (1238667)Instructions burned: 2689 (million)
% 16.10/3.21 % (1238667)------------------------------
% 16.10/3.21 % (1238667)------------------------------
% 16.10/3.21 % (1238660)Success in time 2.262 s
% 16.10/3.21 % Vampire exiting
%------------------------------------------------------------------------------