%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV713-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:19:19 PM UTC 2026
% Result : Unsatisfiable 34.19s 5.65s
% Output : Refutation 35.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 28
% Syntax : Number of formulae : 82 ( 66 unt; 5 def)
% Number of atoms : 103 ( 34 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 43 ( 22 ~; 21 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-3 aty)
% Number of variables : 50 ( 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f64,axiom,
! [X0] : c_HOL_Ominus__class_Ominus(c_Suc(X0),c_HOL_Oone__class_Oone(tc_nat),tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__Suc__1_0) ).
fof(f69,axiom,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f220,axiom,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__1_0) ).
fof(f221,axiom,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__1__right_0) ).
fof(f253,axiom,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_nat) = c_HOL_Otimes__class_Otimes(X1,X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__commute_0) ).
fof(f823,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)
| c_HOL_Oord__class_Oless(X1,X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq_0) ).
fof(f873,axiom,
! [X0,X1] :
( c_Power_Opower__class_Opower(X0,X1,tc_nat) = c_HOL_Otimes__class_Otimes(X0,c_Power_Opower__class_Opower(X0,c_HOL_Ominus__class_Ominus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),tc_nat)
| X1 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_power__eq__if_1) ).
fof(f874,plain,
! [X0,X1] :
( c_Power_Opower__class_Opower(X0,X1,tc_nat) = c_HOL_Otimes__class_Otimes(X0,c_Power_Opower__class_Opower(X0,c_HOL_Ominus__class_Ominus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = X1 ),
inference(reorient_equations,[],[f873]) ).
fof(f881,axiom,
c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_One__nat__def_0) ).
fof(f882,plain,
c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(tc_nat),
inference(reorient_equations,[],[f881]) ).
fof(f964,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_Suc(X0),X1,tc_nat)
| c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__lessD_0) ).
fof(f966,axiom,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X2,X0,tc_nat),c_HOL_Otimes__class_Otimes(X2,X1,tc_nat),tc_nat)
| c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mult__less__cancel1_1) ).
fof(f968,axiom,
! [X0] : c_HOL_Oord__class_Oless(X0,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lessI_0) ).
fof(f970,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(c_Suc(X0),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X2,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__trans__Suc_0) ).
fof(f987,axiom,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(X0,X2,tc_nat),c_HOL_Otimes__class_Otimes(X1,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__mult__distrib_0) ).
fof(f988,axiom,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ominus__class_Ominus(X1,X2,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),c_HOL_Otimes__class_Otimes(X0,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__mult__distrib2_0) ).
fof(f1070,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_numeral__2__eq__2_0) ).
fof(f1071,plain,
c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),
inference(reorient_equations,[],[f1070]) ).
fof(f1081,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__diff_0) ).
fof(f1082,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__diff_1) ).
fof(f1131,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__less__n__mult__m_0) ).
fof(f1209,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Power_Opower__class_Opower(X0,X1,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_zero__less__power__nat__eq_2) ).
fof(f1290,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pos2_0) ).
fof(f1297,axiom,
c_HOL_Oord__class_Oless(v_i____,c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),c_Suc(v_ka____),tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_i_0) ).
fof(f1311,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),c_HOL_Ominus__class_Ominus(X0,X2,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(X2,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(X2,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__less__mono2_0) ).
fof(f1349,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(v_i____,c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),v_ka____,tc_nat),tc_nat),c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),v_ka____,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1439,definition,
sF0 = c_Int_OBit1(c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1440,plain,
c_Int_OBit1(c_Int_OPls) = sF0,
inference(reorient_equations,[],[f1439]) ).
fof(f1441,definition,
sF1 = c_Int_OBit0(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1442,plain,
c_Int_OBit0(sF0) = sF1,
inference(reorient_equations,[],[f1441]) ).
fof(f1443,definition,
sF2 = c_Int_Onumber__class_Onumber__of(sF1,tc_nat),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1444,plain,
c_Int_Onumber__class_Onumber__of(sF1,tc_nat) = sF2,
inference(reorient_equations,[],[f1443]) ).
fof(f1445,definition,
sF3 = c_Power_Opower__class_Opower(sF2,v_ka____,tc_nat),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1446,plain,
c_Power_Opower__class_Opower(sF2,v_ka____,tc_nat) = sF3,
inference(reorient_equations,[],[f1445]) ).
fof(f1447,definition,
sF4 = c_HOL_Ominus__class_Ominus(v_i____,sF3,tc_nat),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1448,plain,
c_HOL_Ominus__class_Ominus(v_i____,sF3,tc_nat) = sF4,
inference(reorient_equations,[],[f1447]) ).
fof(f1449,plain,
~ c_HOL_Oord__class_Oless(sF4,sF3,tc_nat),
inference(definition_folding,[],[f1349,f1446,f1444,f1442,f1440,f1448,f1446,f1444,f1442,f1440]) ).
fof(f1461,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = c_Suc(c_HOL_Oone__class_Oone(tc_nat)),
inference(forward_demodulation,[],[f1071,f882]) ).
fof(f1463,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_nat),X1,tc_nat)
| c_HOL_Oord__class_Oless(X0,c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ),
inference(forward_demodulation,[],[f1131,f882]) ).
fof(f1477,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_nat),tc_nat),
inference(backward_demodulation,[],[f1290,f1440]) ).
fof(f1478,plain,
c_HOL_Oord__class_Oless(v_i____,c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_nat),c_Suc(v_ka____),tc_nat),tc_nat),
inference(backward_demodulation,[],[f1297,f1440]) ).
fof(f1486,plain,
c_Suc(c_HOL_Oone__class_Oone(tc_nat)) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_nat),
inference(forward_demodulation,[],[f1461,f1440]) ).
fof(f1488,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_nat),X1,tc_nat)
| c_HOL_Oord__class_Oless(X0,c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f1463,f882]) ).
fof(f1494,plain,
c_HOL_Oord__class_Oless(v_i____,c_Power_Opower__class_Opower(c_Int_Onumber__class_Onumber__of(sF1,tc_nat),c_Suc(v_ka____),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1478,f1442]) ).
fof(f1495,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(sF1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f1477,f1442]) ).
fof(f1500,plain,
c_Int_Onumber__class_Onumber__of(sF1,tc_nat) = c_Suc(c_HOL_Oone__class_Oone(tc_nat)),
inference(forward_demodulation,[],[f1486,f1442]) ).
fof(f1504,plain,
c_HOL_Oord__class_Oless(v_i____,c_Power_Opower__class_Opower(sF2,c_Suc(v_ka____),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1494,f1444]) ).
fof(f1505,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF2,tc_nat),
inference(forward_demodulation,[],[f1495,f1444]) ).
fof(f1509,plain,
sF2 = c_Suc(c_HOL_Oone__class_Oone(tc_nat)),
inference(forward_demodulation,[],[f1500,f1444]) ).
fof(f1520,plain,
c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_nat),sF2,tc_nat),
inference(superposition,[],[f968,f1509]) ).
fof(f1534,plain,
c_HOL_Oone__class_Oone(tc_nat) = c_HOL_Ominus__class_Ominus(sF2,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(superposition,[],[f64,f1509]) ).
fof(f1775,plain,
c_HOL_Oord__class_Oless(sF3,c_Suc(sF4),tc_nat),
inference(unit_resulting_resolution,[],[f823,f1449]) ).
fof(f2380,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF4,tc_nat)
| c_HOL_Oord__class_Oless(sF3,v_i____,tc_nat) ),
inference(superposition,[],[f1081,f1448]) ).
fof(f2810,plain,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF3,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF2,tc_nat) ),
inference(superposition,[],[f1209,f1446]) ).
fof(f2813,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF3,tc_nat),
inference(forward_subsumption_resolution,[],[f2810,f1505]) ).
fof(f2820,plain,
c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(sF4),tc_nat),
inference(unit_resulting_resolution,[],[f970,f1775,f2813]) ).
fof(f2841,plain,
c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_nat),c_Suc(sF4),tc_nat),
inference(forward_demodulation,[],[f2820,f882]) ).
fof(f2964,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(c_Suc(sF4),c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f1082,f2841]) ).
fof(f2976,plain,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),sF4,tc_nat),
inference(forward_demodulation,[],[f2964,f64]) ).
fof(f2978,plain,
c_HOL_Oord__class_Oless(sF3,v_i____,tc_nat),
inference(backward_subsumption_resolution,[],[f2380,f2976]) ).
fof(f3004,plain,
c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),v_i____,tc_nat),
inference(unit_resulting_resolution,[],[f970,f2813,f2978]) ).
fof(f3010,plain,
c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(tc_nat),v_i____,tc_nat),
inference(forward_demodulation,[],[f3004,f882]) ).
fof(f3090,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,sF4,tc_nat),c_HOL_Otimes__class_Otimes(X0,sF3,tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f966,f1449]) ).
fof(f4808,plain,
c_HOL_Oord__class_Oless(v_i____,c_HOL_Otimes__class_Otimes(v_i____,sF2,tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f1488,f3010,f1520]) ).
fof(f4861,plain,
c_HOL_Oord__class_Oless(v_i____,c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),tc_nat),
inference(forward_demodulation,[],[f4808,f253]) ).
fof(f5124,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(X1,X0,tc_nat),X0,tc_nat) = c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat),X0,tc_nat),
inference(superposition,[],[f987,f220]) ).
fof(f5341,plain,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),c_Power_Opower__class_Opower(sF2,c_Suc(v_ka____),tc_nat),tc_nat),c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),v_i____,tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f1311,f1504,f4861]) ).
fof(f5595,plain,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),c_Power_Opower__class_Opower(sF2,c_Suc(v_ka____),tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(sF2,c_HOL_Oone__class_Oone(tc_nat),tc_nat),v_i____,tc_nat),tc_nat),
inference(forward_demodulation,[],[f5341,f5124]) ).
fof(f5700,plain,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),c_Power_Opower__class_Opower(sF2,c_Suc(v_ka____),tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(v_i____,c_HOL_Ominus__class_Ominus(sF2,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f5595,f253]) ).
fof(f5754,plain,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),c_Power_Opower__class_Opower(sF2,c_Suc(v_ka____),tc_nat),tc_nat),c_HOL_Otimes__class_Otimes(v_i____,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f5700,f1534]) ).
fof(f5785,plain,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),c_Power_Opower__class_Opower(sF2,c_Suc(v_ka____),tc_nat),tc_nat),v_i____,tc_nat),
inference(forward_demodulation,[],[f5754,f221]) ).
fof(f7845,plain,
! [X0,X1] :
( c_Power_Opower__class_Opower(X1,c_Suc(X0),tc_nat) = c_HOL_Otimes__class_Otimes(X1,c_Power_Opower__class_Opower(X1,X0,tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Suc(X0) ),
inference(superposition,[],[f874,f64]) ).
fof(f7900,plain,
! [X0,X1] : c_Power_Opower__class_Opower(X1,c_Suc(X0),tc_nat) = c_HOL_Otimes__class_Otimes(X1,c_Power_Opower__class_Opower(X1,X0,tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f7845,f69]) ).
fof(f7954,plain,
c_HOL_Oord__class_Oless(v_i____,c_HOL_Otimes__class_Otimes(sF2,c_Power_Opower__class_Opower(sF2,v_ka____,tc_nat),tc_nat),tc_nat),
inference(backward_demodulation,[],[f1504,f7900]) ).
fof(f7978,plain,
c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(sF2,v_i____,tc_nat),c_HOL_Otimes__class_Otimes(sF2,c_Power_Opower__class_Opower(sF2,v_ka____,tc_nat),tc_nat),tc_nat),v_i____,tc_nat),
inference(backward_demodulation,[],[f5785,f7900]) ).
fof(f8049,plain,
c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(sF2,c_HOL_Ominus__class_Ominus(v_i____,c_Power_Opower__class_Opower(sF2,v_ka____,tc_nat),tc_nat),tc_nat),v_i____,tc_nat),
inference(forward_demodulation,[],[f7978,f988]) ).
fof(f8073,plain,
c_HOL_Oord__class_Oless(v_i____,c_HOL_Otimes__class_Otimes(sF2,sF3,tc_nat),tc_nat),
inference(forward_demodulation,[],[f7954,f1446]) ).
fof(f8115,plain,
c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(sF2,c_HOL_Ominus__class_Ominus(v_i____,sF3,tc_nat),tc_nat),v_i____,tc_nat),
inference(forward_demodulation,[],[f8049,f1446]) ).
fof(f8150,plain,
c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(sF2,sF4,tc_nat),v_i____,tc_nat),
inference(forward_demodulation,[],[f8115,f1448]) ).
fof(f9931,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Otimes__class_Otimes(X0,sF4,tc_nat)),c_HOL_Otimes__class_Otimes(X0,sF3,tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f964,f3090]) ).
fof(f10332,plain,
c_HOL_Oord__class_Oless(c_Suc(c_HOL_Otimes__class_Otimes(sF2,sF4,tc_nat)),c_HOL_Otimes__class_Otimes(sF2,sF3,tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f970,f8073,f8150]) ).
fof(f10365,plain,
$false,
inference(forward_subsumption_resolution,[],[f10332,f9931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV713-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n001.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 12:25:48 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.25/2.31 % (311948)Input is clausal, will run a generic CNF schedule.
% 11.25/2.31 % (311953)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=2537761274:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.25/2.31 % (311958)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3063351544:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.25/2.31 % (311956)lrs+10_1_sil=8000:sp=occurrence:random_seed=572205012:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.25/2.31 % (311954)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3506983666:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.25/2.31 % (311957)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2092343382:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.25/2.31 % (311955)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=896872297:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.25/2.31 % (311959)dis-21_1_sil=8000:lcm=predicate:random_seed=2290718180: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)
% 11.25/2.31 % (311956)Instruction limit reached!
% 11.25/2.31 % (311956)------------------------------
% 11.25/2.31 % (311956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.31 % (311956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.31 % (311956)CaDiCaL version: 2.1.3
% 11.25/2.31 % (311956)Termination reason: Instruction limit
% 11.25/2.31 % (311956)Termination phase: Saturation
% 11.25/2.31 % (311956)Time elapsed: 0.069 s
% 11.25/2.31 % (311956)Peak memory usage: 89 MB
% 11.25/2.31 % (311956)Instructions burned: 108 (million)
% 11.25/2.31 % (311957)Instruction limit reached!
% 11.25/2.31 % (311957)------------------------------
% 11.25/2.31 % (311957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.31 % (311957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.31 % (311957)CaDiCaL version: 2.1.3
% 11.25/2.31 % (311957)Termination reason: Instruction limit
% 11.25/2.31 % (311957)Termination phase: Saturation
% 11.25/2.31 % (311957)Time elapsed: 0.079 s
% 11.25/2.31 % (311957)Peak memory usage: 89 MB
% 11.25/2.31 % (311957)Instructions burned: 114 (million)
% 11.25/2.31 % (311959)Instruction limit reached!
% 11.25/2.31 % (311959)------------------------------
% 11.25/2.31 % (311959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.31 % (311959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.31 % (311959)CaDiCaL version: 2.1.3
% 11.25/2.31 % (311959)Termination reason: Instruction limit
% 11.25/2.31 % (311959)Termination phase: Saturation
% 11.25/2.31 % (311959)Time elapsed: 0.072 s
% 11.25/2.31 % (311959)Peak memory usage: 90 MB
% 11.25/2.31 % (311959)Instructions burned: 119 (million)
% 11.25/2.31 % (311958)Instruction limit reached!
% 11.25/2.31 % (311958)------------------------------
% 11.25/2.31 % (311958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.31 % (311958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.25/2.31 % (311958)CaDiCaL version: 2.1.3
% 11.25/2.31 % (311958)Termination reason: Instruction limit
% 11.25/2.31 % (311958)Termination phase: Saturation
% 11.25/2.31 % (311958)Time elapsed: 0.141 s
% 11.25/2.31 % (311958)Peak memory usage: 90 MB
% 11.25/2.31 % (311958)Instructions burned: 180 (million)
% 11.25/2.31 % (311967)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=407631224:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.25/2.31 % (311969)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1838867564:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.25/2.31 % (311968)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3762977457:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.25/2.31 % (311967)Refutation not found, incomplete strategy
% 11.25/2.31 % (311967)------------------------------
% 11.25/2.31 % (311967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.25/2.31 % (311967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.91/4.02 % (311967)CaDiCaL version: 2.1.3
% 21.91/4.02 % (311967)Termination reason: Refutation not found, incomplete strategy
% 21.91/4.02 % (311967)Time elapsed: 0.010 s
% 21.91/4.02 % (311967)Peak memory usage: 89 MB
% 21.91/4.02 % (311967)Instructions burned: 13 (million)
% 21.91/4.02 % (311969)Refutation not found, incomplete strategy
% 21.91/4.02 % (311969)------------------------------
% 21.91/4.02 % (311969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.91/4.02 % (311969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.91/4.02 % (311969)CaDiCaL version: 2.1.3
% 21.91/4.02 % (311969)Termination reason: Refutation not found, incomplete strategy
% 21.91/4.02 % (311969)Time elapsed: 0.025 s
% 21.91/4.02 % (311969)Peak memory usage: 89 MB
% 21.91/4.02 % (311969)Instructions burned: 40 (million)
% 21.91/4.02 % (311970)lrs+10_64_to=lpo:sil=8000:random_seed=6112464:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 21.91/4.02 % (311968)Instruction limit reached!
% 21.91/4.02 % (311968)------------------------------
% 21.91/4.02 % (311968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.91/4.02 % (311968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.91/4.02 % (311968)CaDiCaL version: 2.1.3
% 21.91/4.02 % (311968)Termination reason: Instruction limit
% 21.91/4.02 % (311968)Termination phase: Saturation
% 21.91/4.02 % (311968)Time elapsed: 0.104 s
% 21.91/4.02 % (311968)Peak memory usage: 90 MB
% 21.91/4.02 % (311968)Instructions burned: 189 (million)
% 21.91/4.02 % (311970)Instruction limit reached!
% 21.91/4.02 % (311970)------------------------------
% 21.91/4.02 % (311970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.91/4.02 % (311970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.91/4.02 % (311970)CaDiCaL version: 2.1.3
% 21.91/4.02 % (311970)Termination reason: Instruction limit
% 21.91/4.02 % (311970)Termination phase: Saturation
% 21.91/4.02 % (311970)Time elapsed: 0.065 s
% 21.91/4.02 % (311970)Peak memory usage: 89 MB
% 21.91/4.02 % (311970)Instructions burned: 128 (million)
% 21.91/4.02 % (311975)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=269580261:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 21.91/4.02 % (311976)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1653576264:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 21.91/4.02 % (311967)------------------------------
% 21.91/4.02 % (311967)------------------------------
% 21.91/4.02 % (311969)------------------------------
% 21.91/4.02 % (311969)------------------------------
% 21.91/4.02 % (311976)Instruction limit reached!
% 21.91/4.02 % (311976)------------------------------
% 21.91/4.02 % (311976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.91/4.02 % (311976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.91/4.02 % (311976)CaDiCaL version: 2.1.3
% 21.91/4.02 % (311976)Termination reason: Instruction limit
% 21.91/4.02 % (311976)Termination phase: Saturation
% 21.91/4.02 % (311976)Time elapsed: 0.102 s
% 21.91/4.02 % (311976)Peak memory usage: 91 MB
% 21.91/4.02 % (311976)Instructions burned: 157 (million)
% 21.91/4.02 % (311975)Instruction limit reached!
% 21.91/4.02 % (311975)------------------------------
% 21.91/4.02 % (311975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.91/4.02 % (311975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.91/4.02 % (311975)CaDiCaL version: 2.1.3
% 21.91/4.02 % (311975)Termination reason: Instruction limit
% 21.91/4.02 % (311975)Termination phase: Saturation
% 21.91/4.02 % (311975)Time elapsed: 0.131 s
% 21.91/4.02 % (311975)Peak memory usage: 90 MB
% 21.91/4.02 % (311975)Instructions burned: 194 (million)
% 21.91/4.02 % (311979)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1642476895:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 21.91/4.02 % (311980)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=2938877203:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 21.91/4.02 % (311980)Instruction limit reached!
% 21.91/4.02 % (311980)------------------------------
% 21.91/4.02 % (311980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.91/4.02 % (311980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311980)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311980)Termination reason: Instruction limit
% 34.19/5.65 % (311980)Termination phase: Saturation
% 34.19/5.65 % (311980)Time elapsed: 0.060 s
% 34.19/5.65 % (311980)Peak memory usage: 89 MB
% 34.19/5.65 % (311980)Instructions burned: 107 (million)
% 34.19/5.65 % (311981)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3973422478:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 34.19/5.65 % (311982)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3321030969:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 34.19/5.65 % (311981)Instruction limit reached!
% 34.19/5.65 % (311981)------------------------------
% 34.19/5.65 % (311981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311981)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311981)Termination reason: Instruction limit
% 34.19/5.65 % (311981)Termination phase: Saturation
% 34.19/5.65 % (311981)Time elapsed: 0.067 s
% 34.19/5.65 % (311981)Peak memory usage: 90 MB
% 34.19/5.65 % (311981)Instructions burned: 109 (million)
% 34.19/5.65 % (311986)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2937068426:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 34.19/5.65 % (311982)Instruction limit reached!
% 34.19/5.65 % (311982)------------------------------
% 34.19/5.65 % (311982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311982)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311982)Termination reason: Instruction limit
% 34.19/5.65 % (311982)Termination phase: Saturation
% 34.19/5.65 % (311982)Time elapsed: 0.147 s
% 34.19/5.65 % (311982)Peak memory usage: 90 MB
% 34.19/5.65 % (311982)Instructions burned: 243 (million)
% 34.19/5.65 % (311988)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=598969782:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 34.19/5.65 % (311988)Instruction limit reached!
% 34.19/5.65 % (311988)------------------------------
% 34.19/5.65 % (311988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311988)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311988)Termination reason: Instruction limit
% 34.19/5.65 % (311988)Termination phase: Saturation
% 34.19/5.65 % (311988)Time elapsed: 0.090 s
% 34.19/5.65 % (311988)Peak memory usage: 90 MB
% 34.19/5.65 % (311988)Instructions burned: 135 (million)
% 34.19/5.65 % (311990)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4118150341:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 34.19/5.65 % (311992)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1586841227:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 34.19/5.65 % (311992)Instruction limit reached!
% 34.19/5.65 % (311992)------------------------------
% 34.19/5.65 % (311992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311992)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311992)Termination reason: Instruction limit
% 34.19/5.65 % (311992)Termination phase: Saturation
% 34.19/5.65 % (311992)Time elapsed: 0.111 s
% 34.19/5.65 % (311992)Peak memory usage: 91 MB
% 34.19/5.65 % (311992)Instructions burned: 192 (million)
% 34.19/5.65 % (311990)Instruction limit reached!
% 34.19/5.65 % (311990)------------------------------
% 34.19/5.65 % (311990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311990)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311990)Termination reason: Instruction limit
% 34.19/5.65 % (311990)Termination phase: Saturation
% 34.19/5.65 % (311990)Time elapsed: 0.303 s
% 34.19/5.65 % (311990)Peak memory usage: 93 MB
% 34.19/5.65 % (311990)Instructions burned: 499 (million)
% 34.19/5.65 % (311995)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=507236945:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 34.19/5.65 % (311996)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4243706482:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 34.19/5.65 % (311995)Instruction limit reached!
% 34.19/5.65 % (311995)------------------------------
% 34.19/5.65 % (311995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311995)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311995)Termination reason: Instruction limit
% 34.19/5.65 % (311995)Termination phase: Saturation
% 34.19/5.65 % (311995)Time elapsed: 0.170 s
% 34.19/5.65 % (311995)Peak memory usage: 92 MB
% 34.19/5.65 % (311995)Instructions burned: 265 (million)
% 34.19/5.65 % (311996)Instruction limit reached!
% 34.19/5.65 % (311996)------------------------------
% 34.19/5.65 % (311996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311996)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311996)Termination reason: Instruction limit
% 34.19/5.65 % (311996)Termination phase: Saturation
% 34.19/5.65 % (311996)Time elapsed: 0.102 s
% 34.19/5.65 % (311996)Peak memory usage: 90 MB
% 34.19/5.65 % (311996)Instructions burned: 157 (million)
% 34.19/5.65 % (311999)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=571566735:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 34.19/5.65 % (312000)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=313879021:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 34.19/5.65 % (312000)Instruction limit reached!
% 34.19/5.65 % (312000)------------------------------
% 34.19/5.65 % (312000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (312000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (312000)CaDiCaL version: 2.1.3
% 34.19/5.65 % (312000)Termination reason: Instruction limit
% 34.19/5.65 % (312000)Termination phase: Saturation
% 34.19/5.65 % (312000)Time elapsed: 0.321 s
% 34.19/5.65 % (312000)Peak memory usage: 91 MB
% 34.19/5.65 % (312000)Instructions burned: 539 (million)
% 34.19/5.65 % (312003)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3418725492:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 34.19/5.65 % (312003)Instruction limit reached!
% 34.19/5.65 % (312003)------------------------------
% 34.19/5.65 % (312003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (312003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (312003)CaDiCaL version: 2.1.3
% 34.19/5.65 % (312003)Termination reason: Instruction limit
% 34.19/5.65 % (312003)Termination phase: Saturation
% 34.19/5.65 % (312003)Time elapsed: 0.105 s
% 34.19/5.65 % (312003)Peak memory usage: 89 MB
% 34.19/5.65 % (312003)Instructions burned: 181 (million)
% 34.19/5.65 % (312005)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=741889240:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 34.19/5.65 % (311979)Instruction limit reached!
% 34.19/5.65 % (311979)------------------------------
% 34.19/5.65 % (311979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311979)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311979)Termination reason: Instruction limit
% 34.19/5.65 % (311979)Termination phase: Saturation
% 34.19/5.65 % (311979)Time elapsed: 2.178 s
% 34.19/5.65 % (311979)Peak memory usage: 149 MB
% 34.19/5.65 % (311979)Instructions burned: 3394 (million)
% 34.19/5.65 % (312007)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=616918067:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi)
% 34.19/5.65 % (312007)Instruction limit reached!
% 34.19/5.65 % (312007)------------------------------
% 34.19/5.65 % (312007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (312007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (312007)CaDiCaL version: 2.1.3
% 34.19/5.65 % (312007)Termination reason: Instruction limit
% 34.19/5.65 % (312007)Termination phase: Saturation
% 34.19/5.65 % (312007)Time elapsed: 0.212 s
% 34.19/5.65 % (312007)Peak memory usage: 91 MB
% 34.19/5.65 % (312007)Instructions burned: 412 (million)
% 34.19/5.65 % (312009)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3367413643:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi)
% 34.19/5.65 % (311999)Instruction limit reached!
% 34.19/5.65 % (311999)------------------------------
% 34.19/5.65 % (311999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311999)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311999)Termination reason: Instruction limit
% 34.19/5.65 % (311999)Termination phase: Saturation
% 34.19/5.65 % (311999)Time elapsed: 2.039 s
% 34.19/5.65 % (311999)Peak memory usage: 148 MB
% 34.19/5.65 % (311999)Instructions burned: 3256 (million)
% 34.19/5.65 % (312011)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2729953750:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2961 on theBenchmark for (2961ds/303Mi)
% 34.19/5.65 % (312011)Instruction limit reached!
% 34.19/5.65 % (312011)------------------------------
% 34.19/5.65 % (312011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (312011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (312011)CaDiCaL version: 2.1.3
% 34.19/5.65 % (312011)Termination reason: Instruction limit
% 34.19/5.65 % (312011)Termination phase: Saturation
% 34.19/5.65 % (312011)Time elapsed: 0.185 s
% 34.19/5.65 % (312011)Peak memory usage: 92 MB
% 34.19/5.65 % (312011)Instructions burned: 303 (million)
% 34.19/5.65 % (312013)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=16996669:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi)
% 34.19/5.65 % (311986)Instruction limit reached!
% 34.19/5.65 % (311986)------------------------------
% 34.19/5.65 % (311986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (311986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (311986)CaDiCaL version: 2.1.3
% 34.19/5.65 % (311986)Termination reason: Instruction limit
% 34.19/5.65 % (311986)Termination phase: Saturation
% 34.19/5.65 % (311986)Time elapsed: 3.307 s
% 34.19/5.65 % (311986)Peak memory usage: 153 MB
% 34.19/5.65 % (311986)Instructions burned: 5209 (million)
% 34.19/5.65 % (312015)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3763644653:i=598:bs=on:bd=preordered:av=off:ss=axioms_2956 on theBenchmark for (2956ds/598Mi)
% 34.19/5.65 % (312015)First to succeed.
% 34.19/5.65 % (312015)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-311948"
% 34.19/5.65 % (312013)Instruction limit reached!
% 34.19/5.65 % (312013)------------------------------
% 34.19/5.65 % (312013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.19/5.65 % (312013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.19/5.65 % (312013)CaDiCaL version: 2.1.3
% 34.19/5.65 % (312013)Termination reason: Instruction limit
% 34.19/5.65 % (312013)Termination phase: Saturation
% 34.19/5.65 % (312013)Time elapsed: 0.403 s
% 34.19/5.65 % (312013)Peak memory usage: 95 MB
% 34.19/5.65 % (312013)Instructions burned: 720 (million)
% 34.19/5.65 % (312017)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1632195678:i=2989:sd=3:ss=axioms:sgt=60_2952 on theBenchmark for (2952ds/2989Mi)
% 34.19/5.65 % (312015)Refutation found. Thanks to Tanya!
% 34.19/5.65 % SZS status Unsatisfiable for theBenchmark
% 34.19/5.65 % SZS output start Proof for theBenchmark
% See solution above
% 35.48/5.85 % (312015)------------------------------
% 35.48/5.85 % (312015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.48/5.85 % (312015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.48/5.85 % (312015)CaDiCaL version: 2.1.3
% 35.48/5.85 % (312015)Termination reason: Refutation
% 35.48/5.85 % (312015)Time elapsed: 0.253 s
% 35.48/5.85 % (312015)Peak memory usage: 93 MB
% 35.48/5.85 % (312015)Instructions burned: 408 (million)
% 35.48/5.85 % (312015)------------------------------
% 35.48/5.85 % (312015)------------------------------
% 35.48/5.85 % (311948)Success in time 4.964 s
% 35.48/5.85 % Vampire exiting
%------------------------------------------------------------------------------