%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV885-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 01:26:35 PM UTC 2026
% Result : Unsatisfiable 25.58s 4.11s
% Output : Refutation 25.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 41
% Syntax : Number of formulae : 130 ( 96 unt; 11 def)
% Number of atoms : 177 ( 82 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 93 ( 46 ~; 47 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 20 con; 0-4 aty)
% Number of variables : 113 ( 113 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__add__left__commute_0) ).
fof(f30,axiom,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__add__assoc_0) ).
fof(f31,plain,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X2,tc_nat),
inference(reorient_equations,[],[f30]) ).
fof(f45,axiom,
! [X0] : c_Ring__and__Field_Odvd__class_Odvd(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dvd__1__left_0) ).
fof(f76,axiom,
! [X0] : c_Suc(X0) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__eq__plus1_0) ).
fof(f151,axiom,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,X1,tc_nat) = c_HOL_Oplus__class_Oplus(X1,X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__add__commute_0) ).
fof(f441,axiom,
! [X0] : c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_card__empty_0) ).
fof(f442,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0),
inference(reorient_equations,[],[f441]) ).
fof(f471,axiom,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_plus__nat_Oadd__0_0) ).
fof(f578,axiom,
! [X0] :
( X0 = c_Suc(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat))
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__pred_H_0) ).
fof(f579,plain,
! [X0] :
( c_Suc(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) = X0
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
inference(reorient_equations,[],[f578]) ).
fof(f762,axiom,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__Suc__right_0) ).
fof(f763,plain,
! [X0,X1] : c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)) = c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat),
inference(reorient_equations,[],[f762]) ).
fof(f858,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| c_lessequals(X0,X1,tc_nat)
| ~ c_Ring__and__Field_Odvd__class_Odvd(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dvd__imp__le_0) ).
fof(f935,axiom,
! [X0,X1] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__subsetI_0) ).
fof(f953,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(c_Finite__Set_Ocard(X0,X1),c_Finite__Set_Ocard(X2,X1),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X2,tc_fun(X1,tc_bool))
| ~ c_Finite__Set_Ofinite(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_psubset__card__mono_0) ).
fof(f1022,axiom,
! [X2,X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(X0,X2,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__cancel2_0) ).
fof(f1023,plain,
! [X2,X0,X1] : c_HOL_Ominus__class_Ominus(X0,X2,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),tc_nat),
inference(reorient_equations,[],[f1022]) ).
fof(f1029,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__add__inverse_0) ).
fof(f1110,axiom,
! [X2,X0,X1] :
( c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X2,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X2,tc_nat)
| ~ c_lessequals(X2,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__diff__assoc_0) ).
fof(f1111,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X2,X1,tc_nat)
| c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X2,tc_nat),tc_nat) ),
inference(reorient_equations,[],[f1110]) ).
fof(f1112,axiom,
! [X2,X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),X1,tc_nat)
| ~ c_lessequals(X1,X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__diff__assoc2_0) ).
fof(f1113,plain,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X0,tc_nat)
| c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),X1,tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X2,tc_nat) ),
inference(reorient_equations,[],[f1112]) ).
fof(f1124,axiom,
! [X2,X3,X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_Set_Oinsert(X1,X2,X3),tc_fun(X3,tc_bool))
| ~ c_lessequals(X0,X2,tc_fun(X3,tc_bool))
| c_in(X1,X0,X3)
| c_in(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_psubset__insert__iff_3) ).
fof(f1152,axiom,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| c_lessequals(X1,X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__le__linear_0) ).
fof(f1174,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X2,X1,tc_nat)
| c_lessequals(X0,X1,tc_nat)
| ~ c_lessequals(X0,X2,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__trans_0) ).
fof(f1177,axiom,
! [X2,X3,X0,X1] :
( ~ c_lessequals(X3,X1,tc_fun(X2,tc_bool))
| ~ c_in(X0,X3,X2)
| c_in(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_set__mp_0) ).
fof(f1184,axiom,
! [X0] : ~ c_lessequals(c_Suc(X0),X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f1205,axiom,
! [X2,X0,X1] :
( c_Finite__Set_Ofinite(c_Set_Oinsert(X0,X1,X2),X2)
| ~ c_Finite__Set_Ofinite(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_finite__insert_1) ).
fof(f1216,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_lessequals(X0,c_Set_Oimage(X2,X3,X4,X1),tc_fun(X1,tc_bool))
| c_Finite__Set_Ofinite(X0,X1)
| ~ c_Finite__Set_Ofinite(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_finite__surj_0) ).
fof(f1224,axiom,
! [X2,X0,X1] :
( c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| c_in(X0,X1,X2)
| ~ c_Finite__Set_Ofinite(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_card__insert__if_1) ).
fof(f1263,negated_conjecture,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1264,negated_conjecture,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1265,negated_conjecture,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1266,negated_conjecture,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1268,negated_conjecture,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f1269,negated_conjecture,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f1330,plain,
! [X0] : c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat),X0,tc_nat),
inference(definition_unfolding,[],[f45,f76]) ).
fof(f1367,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat) = X0 ),
inference(definition_unfolding,[],[f579,f76]) ).
fof(f1385,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f763,f76,f76]) ).
fof(f1435,plain,
! [X0] : ~ c_lessequals(c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),X0,tc_nat),
inference(definition_unfolding,[],[f1184,f76]) ).
fof(f1442,plain,
! [X2,X0,X1] :
( c_in(X0,X1,X2)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(X1,X2),c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ c_Finite__Set_Ofinite(X1,X2) ),
inference(definition_unfolding,[],[f1224,f76]) ).
fof(f1448,plain,
c_lessequals(c_HOL_Oplus__class_Oplus(v_na,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
inference(definition_unfolding,[],[f1265,f76]) ).
fof(f1449,plain,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_HOL_Oplus__class_Oplus(v_na,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f1266,f76]) ).
fof(f1450,definition,
sF0 = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1451,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = sF0,
inference(reorient_equations,[],[f1450]) ).
fof(f1452,definition,
sF1 = tc_fun(t_a,tc_bool),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1453,plain,
tc_fun(t_a,tc_bool) = sF1,
inference(reorient_equations,[],[f1452]) ).
fof(f1454,plain,
c_lessequals(v_G,sF0,sF1),
inference(definition_folding,[],[f1264,f1453,f1451]) ).
fof(f1455,definition,
sF2 = c_HOL_Oone__class_Oone(tc_nat),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1456,plain,
c_HOL_Oone__class_Oone(tc_nat) = sF2,
inference(reorient_equations,[],[f1455]) ).
fof(f1457,definition,
sF3 = c_HOL_Oplus__class_Oplus(v_na,sF2,tc_nat),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1458,plain,
c_HOL_Oplus__class_Oplus(v_na,sF2,tc_nat) = sF3,
inference(reorient_equations,[],[f1457]) ).
fof(f1459,definition,
sF4 = c_Finite__Set_Ocard(sF0,t_a),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1460,plain,
c_Finite__Set_Ocard(sF0,t_a) = sF4,
inference(reorient_equations,[],[f1459]) ).
fof(f1461,plain,
c_lessequals(sF3,sF4,tc_nat),
inference(definition_folding,[],[f1448,f1460,f1451,f1458,f1456]) ).
fof(f1462,definition,
sF5 = c_Finite__Set_Ocard(v_G,t_a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1463,plain,
c_Finite__Set_Ocard(v_G,t_a) = sF5,
inference(reorient_equations,[],[f1462]) ).
fof(f1464,definition,
sF6 = c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1465,plain,
c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat) = sF6,
inference(reorient_equations,[],[f1464]) ).
fof(f1466,plain,
sF5 = sF6,
inference(definition_folding,[],[f1449,f1465,f1458,f1456,f1460,f1451,f1463]) ).
fof(f1467,definition,
sF7 = hAPP(v_mgt__call,v_pn),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1468,plain,
hAPP(v_mgt__call,v_pn) = sF7,
inference(reorient_equations,[],[f1467]) ).
fof(f1469,plain,
~ c_in(sF7,v_G,t_a),
inference(definition_folding,[],[f1268,f1468]) ).
fof(f1470,definition,
sF8 = c_Set_Oinsert(sF7,v_G,t_a),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1471,plain,
c_Set_Oinsert(sF7,v_G,t_a) = sF8,
inference(reorient_equations,[],[f1470]) ).
fof(f1472,definition,
sF9 = c_Finite__Set_Ocard(sF8,t_a),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1473,plain,
c_Finite__Set_Ocard(sF8,t_a) = sF9,
inference(reorient_equations,[],[f1472]) ).
fof(f1474,definition,
sF10 = c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1475,plain,
c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat) = sF10,
inference(reorient_equations,[],[f1474]) ).
fof(f1476,plain,
sF9 != sF10,
inference(definition_folding,[],[f1269,f1475,f1460,f1451,f1473,f1471,f1468]) ).
fof(f1478,plain,
! [X2,X3,X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_Set_Oinsert(X1,X2,X3),tc_fun(X3,tc_bool))
| ~ c_lessequals(X0,X2,tc_fun(X3,tc_bool))
| c_in(X1,X2,X3) ),
inference(forward_subsumption_resolution,[],[f1124,f1177]) ).
fof(f1505,plain,
! [X0] : c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat),
inference(forward_demodulation,[],[f1330,f471]) ).
fof(f1509,plain,
sF5 = c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat),
inference(forward_demodulation,[],[f1465,f1466]) ).
fof(f1526,plain,
! [X0] : c_Ring__and__Field_Odvd__class_Odvd(sF2,X0,tc_nat),
inference(forward_demodulation,[],[f1505,f1456]) ).
fof(f1660,plain,
! [X0] : ~ c_lessequals(c_HOL_Oplus__class_Oplus(X0,sF2,tc_nat),X0,tc_nat),
inference(superposition,[],[f1435,f1456]) ).
fof(f1832,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(sF1),t_a),
inference(superposition,[],[f442,f1453]) ).
fof(f1900,plain,
! [X0] : c_lessequals(c_Orderings_Obot__class_Obot(sF1),X0,sF1),
inference(superposition,[],[f935,f1453]) ).
fof(f1939,plain,
( ~ c_Finite__Set_Ofinite(v_G,t_a)
| c_Finite__Set_Ofinite(sF8,t_a) ),
inference(superposition,[],[f1205,f1471]) ).
fof(f4046,plain,
! [X0] :
( ~ c_lessequals(X0,sF3,tc_nat)
| c_lessequals(X0,sF4,tc_nat) ),
inference(resolution,[],[f1174,f1461]) ).
fof(f4064,plain,
! [X0] :
( c_lessequals(X0,sF4,tc_nat)
| c_lessequals(sF3,X0,tc_nat) ),
inference(resolution,[],[f4046,f1152]) ).
fof(f4939,plain,
c_lessequals(sF3,c_HOL_Oplus__class_Oplus(sF4,sF2,tc_nat),tc_nat),
inference(resolution,[],[f4064,f1660]) ).
fof(f11949,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,v_na,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,sF2,tc_nat),sF3,tc_nat),
inference(superposition,[],[f1023,f1458]) ).
fof(f15307,plain,
! [X0] :
( ~ c_lessequals(X0,sF0,tc_fun(t_a,tc_bool))
| c_Finite__Set_Ofinite(X0,t_a)
| ~ c_Finite__Set_Ofinite(v_U,tc_Com_Opname) ),
inference(superposition,[],[f1216,f1451]) ).
fof(f15311,plain,
! [X0] :
( ~ c_lessequals(X0,sF0,tc_fun(t_a,tc_bool))
| c_Finite__Set_Ofinite(X0,t_a) ),
inference(forward_subsumption_resolution,[],[f15307,f1263]) ).
fof(f15312,plain,
! [X0] :
( ~ c_lessequals(X0,sF0,sF1)
| c_Finite__Set_Ofinite(X0,t_a) ),
inference(forward_demodulation,[],[f15311,f1453]) ).
fof(f15334,plain,
c_Finite__Set_Ofinite(v_G,t_a),
inference(resolution,[],[f15312,f1454]) ).
fof(f15384,plain,
c_Finite__Set_Ofinite(sF8,t_a),
inference(resolution,[],[f15334,f1939]) ).
fof(f18270,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_Finite__Set_Ocard(X0,t_a),sF9,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,sF8,tc_fun(t_a,tc_bool))
| ~ c_Finite__Set_Ofinite(sF8,t_a) ),
inference(superposition,[],[f953,f1473]) ).
fof(f18272,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_Finite__Set_Ocard(X0,t_a),sF9,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,sF8,tc_fun(t_a,tc_bool)) ),
inference(forward_subsumption_resolution,[],[f18270,f15384]) ).
fof(f18288,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_Finite__Set_Ocard(X0,t_a),sF9,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,sF8,sF1) ),
inference(forward_demodulation,[],[f18272,f1453]) ).
fof(f24618,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(sF4,sF2,tc_nat),X0,tc_nat),sF3,tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(sF4,sF2,tc_nat),sF3,tc_nat),X0,tc_nat),
inference(resolution,[],[f1113,f4939]) ).
fof(f24625,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(sF4,X0,tc_nat),sF3,tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat),X0,tc_nat),
inference(resolution,[],[f1113,f1461]) ).
fof(f24667,plain,
! [X0] : c_HOL_Oplus__class_Oplus(sF5,X0,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(sF4,X0,tc_nat),sF3,tc_nat),
inference(forward_demodulation,[],[f24625,f1509]) ).
fof(f24672,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat),X0,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(sF4,sF2,tc_nat),X0,tc_nat),sF3,tc_nat),
inference(forward_demodulation,[],[f24618,f11949]) ).
fof(f24747,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat),X0,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(sF4,c_HOL_Oplus__class_Oplus(sF2,X0,tc_nat),tc_nat),sF3,tc_nat),
inference(forward_demodulation,[],[f24672,f31]) ).
fof(f24792,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat),X0,tc_nat) = c_HOL_Oplus__class_Oplus(sF5,c_HOL_Oplus__class_Oplus(sF2,X0,tc_nat),tc_nat),
inference(forward_demodulation,[],[f24747,f24667]) ).
fof(f24815,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat),X0,tc_nat) = c_HOL_Oplus__class_Oplus(sF2,c_HOL_Oplus__class_Oplus(sF5,X0,tc_nat),tc_nat),
inference(forward_demodulation,[],[f24792,f29]) ).
fof(f24819,plain,
! [X0] : c_HOL_Oplus__class_Oplus(sF10,X0,tc_nat) = c_HOL_Oplus__class_Oplus(sF2,c_HOL_Oplus__class_Oplus(sF5,X0,tc_nat),tc_nat),
inference(forward_demodulation,[],[f24815,f1475]) ).
fof(f25765,plain,
! [X0] :
( c_HOL_Oord__class_Oless(X0,sF8,tc_fun(t_a,tc_bool))
| ~ c_lessequals(X0,v_G,tc_fun(t_a,tc_bool))
| c_in(sF7,v_G,t_a) ),
inference(superposition,[],[f1478,f1471]) ).
fof(f25768,plain,
! [X0] :
( c_HOL_Oord__class_Oless(X0,sF8,tc_fun(t_a,tc_bool))
| ~ c_lessequals(X0,v_G,tc_fun(t_a,tc_bool)) ),
inference(forward_subsumption_resolution,[],[f25765,f1469]) ).
fof(f25769,plain,
! [X0] :
( c_HOL_Oord__class_Oless(X0,sF8,sF1)
| ~ c_lessequals(X0,v_G,tc_fun(t_a,tc_bool)) ),
inference(forward_demodulation,[],[f25768,f1453]) ).
fof(f25770,plain,
! [X0] :
( ~ c_lessequals(X0,v_G,sF1)
| c_HOL_Oord__class_Oless(X0,sF8,sF1) ),
inference(forward_demodulation,[],[f25769,f1453]) ).
fof(f25786,plain,
c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(sF1),sF8,sF1),
inference(resolution,[],[f25770,f1900]) ).
fof(f29976,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF9,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(sF1),sF8,sF1) ),
inference(superposition,[],[f18288,f1832]) ).
fof(f29983,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF9,tc_nat),
inference(forward_subsumption_resolution,[],[f29976,f25786]) ).
fof(f30242,plain,
sF9 = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(sF9,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(resolution,[],[f29983,f1367]) ).
fof(f30243,plain,
! [X0] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(X0,sF9,tc_nat)
| c_lessequals(X0,sF9,tc_nat) ),
inference(resolution,[],[f29983,f858]) ).
fof(f30255,plain,
sF9 = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_HOL_Ominus__class_Ominus(sF9,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f30242,f151]) ).
fof(f30256,plain,
sF9 = c_HOL_Oplus__class_Oplus(sF2,c_HOL_Ominus__class_Ominus(sF9,sF2,tc_nat),tc_nat),
inference(forward_demodulation,[],[f30255,f1456]) ).
fof(f32056,plain,
c_lessequals(sF2,sF9,tc_nat),
inference(resolution,[],[f30243,f1526]) ).
fof(f32240,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,sF9,tc_nat),sF2,tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(sF9,sF2,tc_nat),tc_nat),
inference(resolution,[],[f32056,f1111]) ).
fof(f33992,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ c_Finite__Set_Ofinite(v_G,t_a) ),
inference(resolution,[],[f1442,f1469]) ).
fof(f34046,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f33992,f15334]) ).
fof(f34073,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),c_Finite__Set_Ocard(v_G,t_a),tc_nat),
inference(forward_demodulation,[],[f34046,f151]) ).
fof(f34078,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),sF5,tc_nat),
inference(forward_demodulation,[],[f34073,f1463]) ).
fof(f34082,plain,
c_HOL_Oplus__class_Oplus(sF5,c_HOL_Oone__class_Oone(tc_nat),tc_nat) = c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a),
inference(forward_demodulation,[],[f34078,f151]) ).
fof(f34086,plain,
c_Finite__Set_Ocard(sF8,t_a) = c_HOL_Oplus__class_Oplus(sF5,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(forward_demodulation,[],[f34082,f1471]) ).
fof(f34087,plain,
c_Finite__Set_Ocard(sF8,t_a) = c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat),
inference(forward_demodulation,[],[f34086,f1456]) ).
fof(f34088,plain,
c_Finite__Set_Ocard(sF8,t_a) = c_HOL_Oplus__class_Oplus(sF2,sF5,tc_nat),
inference(forward_demodulation,[],[f34087,f151]) ).
fof(f34089,plain,
sF9 = c_HOL_Oplus__class_Oplus(sF2,sF5,tc_nat),
inference(forward_demodulation,[],[f34088,f1473]) ).
fof(f34152,plain,
c_HOL_Oplus__class_Oplus(sF9,c_HOL_Oone__class_Oone(tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(sF2,c_HOL_Oplus__class_Oplus(sF5,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f1385,f34089]) ).
fof(f34246,plain,
c_HOL_Oplus__class_Oplus(sF10,c_HOL_Oone__class_Oone(tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(sF9,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(forward_demodulation,[],[f34152,f24819]) ).
fof(f34251,plain,
c_HOL_Oplus__class_Oplus(sF10,sF2,tc_nat) = c_HOL_Oplus__class_Oplus(sF9,sF2,tc_nat),
inference(forward_demodulation,[],[f34246,f1456]) ).
fof(f34253,plain,
c_HOL_Oplus__class_Oplus(sF10,sF2,tc_nat) = c_HOL_Oplus__class_Oplus(sF2,sF9,tc_nat),
inference(forward_demodulation,[],[f34251,f151]) ).
fof(f34254,plain,
c_HOL_Oplus__class_Oplus(sF2,sF10,tc_nat) = c_HOL_Oplus__class_Oplus(sF2,sF9,tc_nat),
inference(forward_demodulation,[],[f34253,f151]) ).
fof(f41255,plain,
sF10 = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(sF2,sF9,tc_nat),sF2,tc_nat),
inference(superposition,[],[f1029,f34254]) ).
fof(f41360,plain,
sF10 = c_HOL_Oplus__class_Oplus(sF2,c_HOL_Ominus__class_Ominus(sF9,sF2,tc_nat),tc_nat),
inference(forward_demodulation,[],[f41255,f32240]) ).
fof(f41366,plain,
sF9 = sF10,
inference(forward_demodulation,[],[f41360,f30256]) ).
fof(f41368,plain,
$false,
inference(forward_subsumption_resolution,[],[f41366,f1476]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV885-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n019.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 12:48:18 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 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
% 10.10/1.98 % (3977173)Will run a generic schedule for satisfiability detection.
% 10.10/1.98 % (3977179)% WARNING: option uhcvi not known.
% 10.10/1.98 % (3977179)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1596013467:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 10.10/1.98 % (3977178)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3585291232_2999 on theBenchmark for (2999ds/0Mi)
% 10.10/1.98 % (3977180)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1556171640:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 10.10/1.98 % (3977181)dis+10_1_sil=32000:sp=arity:random_seed=2640985962:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 10.10/1.98 % (3977182)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1619164588:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 10.10/1.98 % (3977183)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2847860520:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 10.10/1.98 % (3977184)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3671459817:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 10.10/1.98 % (3977181)Instruction limit reached!
% 10.10/1.98 % (3977181)------------------------------
% 10.10/1.98 % (3977181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.10/1.98 % (3977181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/1.98 % (3977181)CaDiCaL version: 2.1.3
% 10.10/1.98 % (3977181)Termination reason: Instruction limit
% 10.10/1.98 % (3977181)Termination phase: Saturation
% 10.10/1.98 % (3977181)Time elapsed: 0.066 s
% 10.10/1.98 % (3977181)Peak memory usage: 13 MB
% 10.10/1.98 % (3977181)Instructions burned: 103 (million)
% 10.10/1.98 % (3977182)Instruction limit reached!
% 10.10/1.98 % (3977182)------------------------------
% 10.10/1.98 % (3977182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.10/1.98 % (3977182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/1.98 % (3977182)CaDiCaL version: 2.1.3
% 10.10/1.98 % (3977182)Termination reason: Instruction limit
% 10.10/1.98 % (3977182)Termination phase: Saturation
% 10.10/1.98 % (3977182)Time elapsed: 0.069 s
% 10.10/1.98 % (3977182)Peak memory usage: 13 MB
% 10.10/1.98 % (3977182)Instructions burned: 116 (million)
% 10.10/1.98 % (3977183)Instruction limit reached!
% 10.10/1.98 % (3977183)------------------------------
% 10.10/1.98 % (3977183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.10/1.98 % (3977183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/1.98 % (3977183)CaDiCaL version: 2.1.3
% 10.10/1.98 % (3977183)Termination reason: Instruction limit
% 10.10/1.98 % (3977183)Termination phase: Saturation
% 10.10/1.98 % (3977183)Time elapsed: 0.080 s
% 10.10/1.98 % (3977183)Peak memory usage: 14 MB
% 10.10/1.98 % (3977183)Instructions burned: 132 (million)
% 10.10/1.98 % (3977192)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=485721572:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 10.10/1.98 % (3977193)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=125639969:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 10.10/1.98 % (3977194)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=325131515:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 10.10/1.98 % (3977184)Instruction limit reached!
% 10.10/1.98 % (3977184)------------------------------
% 10.10/1.98 % (3977184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.10/1.98 % (3977184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/1.98 % (3977184)CaDiCaL version: 2.1.3
% 10.10/1.98 % (3977184)Termination reason: Instruction limit
% 10.10/1.98 % (3977184)Termination phase: Saturation
% 10.10/1.98 % (3977184)Time elapsed: 0.103 s
% 10.10/1.98 % (3977184)Peak memory usage: 14 MB
% 10.10/1.98 % (3977184)Instructions burned: 160 (million)
% 10.10/1.98 % (3977198)ott-21_1_sil=16000:fs=off:random_seed=3728511917:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 10.10/1.98 % TRYING [1]
% 10.10/1.98 % (3977193)Instruction limit reached!
% 10.10/1.98 % (3977193)------------------------------
% 10.10/1.98 % (3977193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.10/1.98 % (3977193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977193)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977193)Termination reason: Instruction limit
% 25.58/4.11 % (3977193)Termination phase: Saturation
% 25.58/4.11 % (3977193)Time elapsed: 0.076 s
% 25.58/4.11 % (3977193)Peak memory usage: 14 MB
% 25.58/4.11 % (3977193)Instructions burned: 133 (million)
% 25.58/4.11 % TRYING [2]
% 25.58/4.11 % (3977200)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2438877302:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 25.58/4.11 % (3977198)Instruction limit reached!
% 25.58/4.11 % (3977198)------------------------------
% 25.58/4.11 % (3977198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977198)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977198)Termination reason: Instruction limit
% 25.58/4.11 % (3977198)Termination phase: Saturation
% 25.58/4.11 % (3977198)Time elapsed: 0.099 s
% 25.58/4.11 % (3977198)Peak memory usage: 14 MB
% 25.58/4.11 % (3977198)Instructions burned: 181 (million)
% 25.58/4.11 % (3977202)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4007046387:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 25.58/4.11 % TRYING [1]
% 25.58/4.11 % TRYING [2]
% 25.58/4.11 % TRYING [3]
% 25.58/4.11 % TRYING [3]
% 25.58/4.11 % (3977192)Instruction limit reached!
% 25.58/4.11 % (3977192)------------------------------
% 25.58/4.11 % (3977192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977192)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977192)Termination reason: Instruction limit
% 25.58/4.11 % (3977192)Termination phase: Finite model building constraint generation
% 25.58/4.11 % (3977192)Time elapsed: 0.314 s
% 25.58/4.11 % (3977192)Peak memory usage: 32 MB
% 25.58/4.11 % (3977192)Instructions burned: 715 (million)
% 25.58/4.11 % TRYING [1]
% 25.58/4.11 % (3977204)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2571175134:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 25.58/4.11 % TRYING [2]
% 25.58/4.11 % (3977200)Instruction limit reached!
% 25.58/4.11 % (3977200)------------------------------
% 25.58/4.11 % (3977200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977200)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977200)Termination reason: Instruction limit
% 25.58/4.11 % (3977200)Termination phase: Saturation
% 25.58/4.11 % (3977200)Time elapsed: 0.313 s
% 25.58/4.11 % (3977200)Peak memory usage: 15 MB
% 25.58/4.11 % (3977200)Instructions burned: 477 (million)
% 25.58/4.11 % (3977194)Instruction limit reached!
% 25.58/4.11 % (3977194)------------------------------
% 25.58/4.11 % (3977194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977194)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977194)Termination reason: Instruction limit
% 25.58/4.11 % (3977194)Termination phase: Saturation
% 25.58/4.11 % (3977194)Time elapsed: 0.408 s
% 25.58/4.11 % (3977194)Peak memory usage: 18 MB
% 25.58/4.11 % (3977194)Instructions burned: 685 (million)
% 25.58/4.11 % (3977206)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1399649414:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 25.58/4.11 % (3977207)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=4029780701: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)
% 25.58/4.11 % (3977202)Instruction limit reached!
% 25.58/4.11 % (3977202)------------------------------
% 25.58/4.11 % (3977202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977202)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977202)Termination reason: Instruction limit
% 25.58/4.11 % (3977202)Termination phase: Finite model building SAT solving
% 25.58/4.11 % (3977202)Time elapsed: 0.402 s
% 25.58/4.11 % (3977202)Peak memory usage: 35 MB
% 25.58/4.11 % (3977202)Instructions burned: 866 (million)
% 25.58/4.11 % (3977210)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=603054669:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 25.58/4.11 % (3977207)Instruction limit reached!
% 25.58/4.11 % (3977207)------------------------------
% 25.58/4.11 % (3977207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977207)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977207)Termination reason: Instruction limit
% 25.58/4.11 % (3977207)Termination phase: Saturation
% 25.58/4.11 % (3977207)Time elapsed: 0.395 s
% 25.58/4.11 % (3977207)Peak memory usage: 17 MB
% 25.58/4.11 % (3977207)Instructions burned: 694 (million)
% 25.58/4.11 % (3977212)fmb+10_1_sil=64000:random_seed=3726127309:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 25.58/4.11 % (3977206)Instruction limit reached!
% 25.58/4.11 % (3977206)------------------------------
% 25.58/4.11 % (3977206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977206)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977206)Termination reason: Instruction limit
% 25.58/4.11 % (3977206)Termination phase: Finite model building constraint generation
% 25.58/4.11 % (3977206)Time elapsed: 0.426 s
% 25.58/4.11 % (3977206)Peak memory usage: 85 MB
% 25.58/4.11 % (3977206)Instructions burned: 891 (million)
% 25.58/4.11 % (3977214)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3469234353:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 25.58/4.11 % TRYING [4]
% 25.58/4.11 % TRYING [1]
% 25.58/4.11 % (3977214)Cannot represent all propositional literals internally
% 25.58/4.11 % (3977214)Refutation not found, incomplete strategy
% 25.58/4.11 % (3977214)------------------------------
% 25.58/4.11 % (3977214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977214)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977214)Termination reason: Refutation not found, incomplete strategy
% 25.58/4.11 % (3977214)Time elapsed: 0.158 s
% 25.58/4.11 % (3977214)Peak memory usage: 17 MB
% 25.58/4.11 % (3977214)Instructions burned: 318 (million)
% 25.58/4.11 % TRYING [2]
% 25.58/4.11 % (3977214)------------------------------
% 25.58/4.11 % (3977214)------------------------------
% 25.58/4.11 % (3977216)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2003441481:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 25.58/4.11 % (3977210)Instruction limit reached!
% 25.58/4.11 % (3977210)------------------------------
% 25.58/4.11 % (3977210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977210)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977210)Termination reason: Instruction limit
% 25.58/4.11 % (3977210)Termination phase: Saturation
% 25.58/4.11 % (3977210)Time elapsed: 0.500 s
% 25.58/4.11 % (3977210)Peak memory usage: 20 MB
% 25.58/4.11 % (3977210)Instructions burned: 881 (million)
% 25.58/4.11 % (3977204)Instruction limit reached!
% 25.58/4.11 % (3977204)------------------------------
% 25.58/4.11 % (3977204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977204)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977204)Termination reason: Instruction limit
% 25.58/4.11 % (3977204)Termination phase: Saturation
% 25.58/4.11 % (3977204)Time elapsed: 0.752 s
% 25.58/4.11 % (3977204)Peak memory usage: 21 MB
% 25.58/4.11 % (3977204)Instructions burned: 1179 (million)
% 25.58/4.11 % (3977218)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2077138619:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 25.58/4.11 % (3977219)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2394573664:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 25.58/4.11 % TRYING [8]
% 25.58/4.11 % (3977216)Instruction limit reached!
% 25.58/4.11 % (3977216)------------------------------
% 25.58/4.11 % (3977216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977216)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977216)Termination reason: Instruction limit
% 25.58/4.11 % (3977216)Termination phase: Finite model building constraint generation
% 25.58/4.11 % (3977216)Time elapsed: 0.363 s
% 25.58/4.11 % (3977216)Peak memory usage: 57 MB
% 25.58/4.11 % (3977216)Instructions burned: 922 (million)
% 25.58/4.11 % (3977222)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3402405012:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 25.58/4.11 % TRYING [3]
% 25.58/4.11 % (3977222)Cannot represent all propositional literals internally
% 25.58/4.11 % (3977222)Refutation not found, incomplete strategy
% 25.58/4.11 % (3977222)------------------------------
% 25.58/4.11 % (3977222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977222)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977222)Termination reason: Refutation not found, incomplete strategy
% 25.58/4.11 % (3977222)Time elapsed: 0.166 s
% 25.58/4.11 % (3977222)Peak memory usage: 18 MB
% 25.58/4.11 % (3977222)Instructions burned: 332 (million)
% 25.58/4.11 % (3977222)------------------------------
% 25.58/4.11 % (3977222)------------------------------
% 25.58/4.11 % (3977224)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=644349177:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi)
% 25.58/4.11 % (3977219)Instruction limit reached!
% 25.58/4.11 % (3977219)------------------------------
% 25.58/4.11 % (3977219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977219)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977219)Termination reason: Instruction limit
% 25.58/4.11 % (3977219)Termination phase: Saturation
% 25.58/4.11 % (3977219)Time elapsed: 0.662 s
% 25.58/4.11 % (3977219)Peak memory usage: 26 MB
% 25.58/4.11 % (3977219)Instructions burned: 1472 (million)
% 25.58/4.11 % (3977226)ott-2_1_sil=16000:newcnf=on:random_seed=445388940:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi)
% 25.58/4.11 % (3977226)Instruction limit reached!
% 25.58/4.11 % (3977226)------------------------------
% 25.58/4.11 % (3977226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977226)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977226)Termination reason: Instruction limit
% 25.58/4.11 % (3977226)Termination phase: Saturation
% 25.58/4.11 % (3977226)Time elapsed: 0.520 s
% 25.58/4.11 % (3977226)Peak memory usage: 17 MB
% 25.58/4.11 % (3977226)Instructions burned: 871 (million)
% 25.58/4.11 % (3977228)ott+10_1_sil=32000:tgt=ground:random_seed=3421344860:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi)
% 25.58/4.11 % (3977224)Cannot represent all propositional literals internally
% 25.58/4.11 % (3977224)Refutation not found, incomplete strategy
% 25.58/4.11 % (3977224)------------------------------
% 25.58/4.11 % (3977224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977224)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977224)Termination reason: Refutation not found, incomplete strategy
% 25.58/4.11 % (3977224)Time elapsed: 0.713 s
% 25.58/4.11 % (3977224)Peak memory usage: 30 MB
% 25.58/4.11 % (3977224)Instructions burned: 1456 (million)
% 25.58/4.11 % (3977224)------------------------------
% 25.58/4.11 % (3977224)------------------------------
% 25.58/4.11 % (3977230)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4175091058:i=54282_2974 on theBenchmark for (2974ds/54282Mi)
% 25.58/4.11 % TRYING [1]
% 25.58/4.11 % TRYING [2]
% 25.58/4.11 % TRYING [3]
% 25.58/4.11 % TRYING [4]
% 25.58/4.11 % (3977228) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3977173-3977228"...
% 25.58/4.11 % (3977228)...printing done.
% 25.58/4.11 % (3977228)Refutation found. Thanks to Tanya!
% 25.58/4.11 % SZS status Unsatisfiable for theBenchmark
% 25.58/4.11 % SZS output start Proof for theBenchmark
% See solution above
% 25.58/4.11 % (3977228)------------------------------
% 25.58/4.11 % (3977228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.58/4.11 % (3977228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.58/4.11 % (3977228)CaDiCaL version: 2.1.3
% 25.58/4.11 % (3977228)Termination reason: Refutation
% 25.58/4.11 % (3977228)Time elapsed: 1.335 s
% 25.58/4.11 % (3977228)Peak memory usage: 26 MB
% 25.58/4.11 % (3977228)Instructions burned: 2097 (million)
% 25.58/4.11 % (3977173)Success in time 3.903 s
% 25.58/4.11 % Vampire exiting
%------------------------------------------------------------------------------