%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV703-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 : n003.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:18 PM UTC 2026
% Result : Unsatisfiable 35.06s 5.77s
% Output : Refutation 36.22s
% 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.02 % Problem : SWV703-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.05/0.20 % Computer : n003.cluster.edu
% 0.05/0.20 % Model : x86_64 x86_64
% 0.05/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.20 % Memory : 8046.5625MB
% 0.05/0.20 % OS : Linux 6.8.0-71-generic
% 0.05/0.20 % CPULimit : 300
% 0.05/0.20 % WCLimit : 300
% 0.05/0.20 % DateTime : Mon Sep 28 12:19:42 UTC 2026
% 0.05/0.20 % CPUTime :
% 0.05/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.24 Running first-order theorem proving
% 0.05/0.24 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.54/2.39 % (1549657)Input is clausal, will run a generic CNF schedule.
% 11.54/2.39 % (1549664)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=940728133:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.54/2.39 % (1549666)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3294202349:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.54/2.39 % (1549663)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=911401463:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.54/2.39 % (1549668)dis-21_1_sil=8000:lcm=predicate:random_seed=373641879: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.54/2.39 % (1549662)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=1926654856:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.54/2.39 % (1549667)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3708680659:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.54/2.39 % (1549665)lrs+10_1_sil=8000:sp=occurrence:random_seed=1484749671:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.54/2.39 % (1549665)Instruction limit reached!
% 11.54/2.39 % (1549665)------------------------------
% 11.54/2.39 % (1549665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.39 % (1549665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.39 % (1549665)CaDiCaL version: 2.1.3
% 11.54/2.39 % (1549665)Termination reason: Instruction limit
% 11.54/2.39 % (1549665)Termination phase: Saturation
% 11.54/2.39 % (1549665)Time elapsed: 0.068 s
% 11.54/2.39 % (1549665)Peak memory usage: 89 MB
% 11.54/2.39 % (1549665)Instructions burned: 108 (million)
% 11.54/2.39 % (1549668)Instruction limit reached!
% 11.54/2.39 % (1549668)------------------------------
% 11.54/2.39 % (1549668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.39 % (1549668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.39 % (1549668)CaDiCaL version: 2.1.3
% 11.54/2.39 % (1549668)Termination reason: Instruction limit
% 11.54/2.39 % (1549668)Termination phase: Saturation
% 11.54/2.39 % (1549668)Time elapsed: 0.071 s
% 11.54/2.39 % (1549668)Peak memory usage: 90 MB
% 11.54/2.39 % (1549668)Instructions burned: 118 (million)
% 11.54/2.39 % (1549666)Instruction limit reached!
% 11.54/2.39 % (1549666)------------------------------
% 11.54/2.39 % (1549666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.39 % (1549666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.39 % (1549666)CaDiCaL version: 2.1.3
% 11.54/2.39 % (1549666)Termination reason: Instruction limit
% 11.54/2.39 % (1549666)Termination phase: Saturation
% 11.54/2.39 % (1549666)Time elapsed: 0.078 s
% 11.54/2.39 % (1549666)Peak memory usage: 89 MB
% 11.54/2.39 % (1549666)Instructions burned: 115 (million)
% 11.54/2.39 % (1549667)Instruction limit reached!
% 11.54/2.39 % (1549667)------------------------------
% 11.54/2.39 % (1549667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/2.39 % (1549667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/2.39 % (1549667)CaDiCaL version: 2.1.3
% 11.54/2.39 % (1549667)Termination reason: Instruction limit
% 11.54/2.39 % (1549667)Termination phase: Saturation
% 11.54/2.39 % (1549667)Time elapsed: 0.125 s
% 11.54/2.39 % (1549667)Peak memory usage: 90 MB
% 11.54/2.39 % (1549667)Instructions burned: 181 (million)
% 11.54/2.39 % (1549678)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1454620272:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.54/2.39 % (1549677)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=326166059: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.54/2.39 % (1549676)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=562177117:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.54/2.39 % (1549676)Refutation not found, incomplete strategy
% 11.54/2.39 % (1549676)------------------------------
% 11.54/2.39 % (1549676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.07 % (1549676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.07 % (1549676)CaDiCaL version: 2.1.3
% 23.88/4.07 % (1549676)Termination reason: Refutation not found, incomplete strategy
% 23.88/4.07 % (1549676)Time elapsed: 0.010 s
% 23.88/4.07 % (1549676)Peak memory usage: 89 MB
% 23.88/4.07 % (1549676)Instructions burned: 14 (million)
% 23.88/4.07 % (1549678)Refutation not found, incomplete strategy
% 23.88/4.07 % (1549678)------------------------------
% 23.88/4.07 % (1549678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.07 % (1549678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.07 % (1549678)CaDiCaL version: 2.1.3
% 23.88/4.07 % (1549678)Termination reason: Refutation not found, incomplete strategy
% 23.88/4.07 % (1549678)Time elapsed: 0.025 s
% 23.88/4.07 % (1549678)Peak memory usage: 89 MB
% 23.88/4.07 % (1549678)Instructions burned: 40 (million)
% 23.88/4.07 % (1549679)lrs+10_64_to=lpo:sil=8000:random_seed=3679692305:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 23.88/4.07 % (1549677)Instruction limit reached!
% 23.88/4.07 % (1549677)------------------------------
% 23.88/4.07 % (1549677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.07 % (1549677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.07 % (1549677)CaDiCaL version: 2.1.3
% 23.88/4.07 % (1549677)Termination reason: Instruction limit
% 23.88/4.07 % (1549677)Termination phase: Saturation
% 23.88/4.07 % (1549677)Time elapsed: 0.103 s
% 23.88/4.07 % (1549677)Peak memory usage: 91 MB
% 23.88/4.07 % (1549677)Instructions burned: 189 (million)
% 23.88/4.07 % (1549679)Instruction limit reached!
% 23.88/4.07 % (1549679)------------------------------
% 23.88/4.07 % (1549679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.07 % (1549679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.07 % (1549679)CaDiCaL version: 2.1.3
% 23.88/4.07 % (1549679)Termination reason: Instruction limit
% 23.88/4.07 % (1549679)Termination phase: Saturation
% 23.88/4.07 % (1549679)Time elapsed: 0.063 s
% 23.88/4.07 % (1549679)Peak memory usage: 89 MB
% 23.88/4.07 % (1549679)Instructions burned: 127 (million)
% 23.88/4.07 % (1549676)------------------------------
% 23.88/4.07 % (1549676)------------------------------
% 23.88/4.07 % (1549678)------------------------------
% 23.88/4.07 % (1549678)------------------------------
% 23.88/4.07 % (1549684)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1559472648:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 23.88/4.07 % (1549685)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=152925850:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 23.88/4.07 % (1549685)Instruction limit reached!
% 23.88/4.07 % (1549685)------------------------------
% 23.88/4.07 % (1549685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.07 % (1549685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.07 % (1549685)CaDiCaL version: 2.1.3
% 23.88/4.07 % (1549685)Termination reason: Instruction limit
% 23.88/4.07 % (1549685)Termination phase: Saturation
% 23.88/4.07 % (1549685)Time elapsed: 0.101 s
% 23.88/4.07 % (1549685)Peak memory usage: 91 MB
% 23.88/4.07 % (1549685)Instructions burned: 157 (million)
% 23.88/4.07 % (1549684)Instruction limit reached!
% 23.88/4.07 % (1549684)------------------------------
% 23.88/4.07 % (1549684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.88/4.07 % (1549684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.88/4.07 % (1549684)CaDiCaL version: 2.1.3
% 23.88/4.07 % (1549684)Termination reason: Instruction limit
% 23.88/4.07 % (1549684)Termination phase: Saturation
% 23.88/4.07 % (1549684)Time elapsed: 0.130 s
% 23.88/4.07 % (1549684)Peak memory usage: 90 MB
% 23.88/4.07 % (1549684)Instructions burned: 195 (million)
% 23.88/4.07 % (1549686)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1904942971:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 23.88/4.07 % (1549689)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=2895021998:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 23.88/4.07 % (1549689)Instruction limit reached!
% 23.88/4.07 % (1549689)------------------------------
% 23.88/4.07 % (1549689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549689)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549689)Termination reason: Instruction limit
% 35.06/5.77 % (1549689)Termination phase: Saturation
% 35.06/5.77 % (1549689)Time elapsed: 0.059 s
% 35.06/5.77 % (1549689)Peak memory usage: 89 MB
% 35.06/5.77 % (1549689)Instructions burned: 107 (million)
% 35.06/5.77 % (1549690)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1045786366:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 35.06/5.77 % (1549691)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4070450146:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 35.06/5.77 % (1549690)Instruction limit reached!
% 35.06/5.77 % (1549690)------------------------------
% 35.06/5.77 % (1549690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549690)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549690)Termination reason: Instruction limit
% 35.06/5.77 % (1549690)Termination phase: Saturation
% 35.06/5.77 % (1549690)Time elapsed: 0.066 s
% 35.06/5.77 % (1549690)Peak memory usage: 90 MB
% 35.06/5.77 % (1549690)Instructions burned: 108 (million)
% 35.06/5.77 % (1549694)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2350774923:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 35.06/5.77 % (1549691)Instruction limit reached!
% 35.06/5.77 % (1549691)------------------------------
% 35.06/5.77 % (1549691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549691)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549691)Termination reason: Instruction limit
% 35.06/5.77 % (1549691)Termination phase: Saturation
% 35.06/5.77 % (1549691)Time elapsed: 0.146 s
% 35.06/5.77 % (1549691)Peak memory usage: 90 MB
% 35.06/5.77 % (1549691)Instructions burned: 243 (million)
% 35.06/5.77 % (1549697)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1406640784:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 35.06/5.77 % (1549697)Instruction limit reached!
% 35.06/5.77 % (1549697)------------------------------
% 35.06/5.77 % (1549697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549697)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549697)Termination reason: Instruction limit
% 35.06/5.77 % (1549697)Termination phase: Saturation
% 35.06/5.77 % (1549697)Time elapsed: 0.089 s
% 35.06/5.77 % (1549697)Peak memory usage: 90 MB
% 35.06/5.77 % (1549697)Instructions burned: 135 (million)
% 35.06/5.77 % (1549699)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=817644651:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 35.06/5.77 % (1549701)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3679801132:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 35.06/5.77 % (1549701)Instruction limit reached!
% 35.06/5.77 % (1549701)------------------------------
% 35.06/5.77 % (1549701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549701)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549701)Termination reason: Instruction limit
% 35.06/5.77 % (1549701)Termination phase: Saturation
% 35.06/5.77 % (1549701)Time elapsed: 0.110 s
% 35.06/5.77 % (1549701)Peak memory usage: 91 MB
% 35.06/5.77 % (1549701)Instructions burned: 192 (million)
% 35.06/5.77 % (1549699)Instruction limit reached!
% 35.06/5.77 % (1549699)------------------------------
% 35.06/5.77 % (1549699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549699)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549699)Termination reason: Instruction limit
% 35.06/5.77 % (1549699)Termination phase: Saturation
% 35.06/5.77 % (1549699)Time elapsed: 0.302 s
% 35.06/5.77 % (1549699)Peak memory usage: 93 MB
% 35.06/5.77 % (1549699)Instructions burned: 500 (million)
% 35.06/5.77 % (1549704)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2222806979:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 35.06/5.77 % (1549705)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3197598787:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 35.06/5.77 % (1549704)Instruction limit reached!
% 35.06/5.77 % (1549704)------------------------------
% 35.06/5.77 % (1549704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549704)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549704)Termination reason: Instruction limit
% 35.06/5.77 % (1549704)Termination phase: Saturation
% 35.06/5.77 % (1549704)Time elapsed: 0.167 s
% 35.06/5.77 % (1549704)Peak memory usage: 92 MB
% 35.06/5.77 % (1549704)Instructions burned: 264 (million)
% 35.06/5.77 % (1549705)Instruction limit reached!
% 35.06/5.77 % (1549705)------------------------------
% 35.06/5.77 % (1549705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549705)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549705)Termination reason: Instruction limit
% 35.06/5.77 % (1549705)Termination phase: Saturation
% 35.06/5.77 % (1549705)Time elapsed: 0.101 s
% 35.06/5.77 % (1549705)Peak memory usage: 90 MB
% 35.06/5.77 % (1549705)Instructions burned: 156 (million)
% 35.06/5.77 % (1549708)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=1685191562:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 35.06/5.77 % (1549709)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=897186840:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 35.06/5.77 % (1549709)Instruction limit reached!
% 35.06/5.77 % (1549709)------------------------------
% 35.06/5.77 % (1549709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549709)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549709)Termination reason: Instruction limit
% 35.06/5.77 % (1549709)Termination phase: Saturation
% 35.06/5.77 % (1549709)Time elapsed: 0.316 s
% 35.06/5.77 % (1549709)Peak memory usage: 91 MB
% 35.06/5.77 % (1549709)Instructions burned: 539 (million)
% 35.06/5.77 % (1549712)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=24897876:i=180:bd=preordered:av=off_2976 on theBenchmark for (2976ds/180Mi)
% 35.06/5.77 % (1549712)Instruction limit reached!
% 35.06/5.77 % (1549712)------------------------------
% 35.06/5.77 % (1549712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549712)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549712)Termination reason: Instruction limit
% 35.06/5.77 % (1549712)Termination phase: Saturation
% 35.06/5.77 % (1549712)Time elapsed: 0.105 s
% 35.06/5.77 % (1549712)Peak memory usage: 90 MB
% 35.06/5.77 % (1549712)Instructions burned: 181 (million)
% 35.06/5.77 % (1549714)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=3164614112:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2973 on theBenchmark for (2973ds/10307Mi)
% 35.06/5.77 % (1549686)Instruction limit reached!
% 35.06/5.77 % (1549686)------------------------------
% 35.06/5.77 % (1549686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549686)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549686)Termination reason: Instruction limit
% 35.06/5.77 % (1549686)Termination phase: Saturation
% 35.06/5.77 % (1549686)Time elapsed: 2.161 s
% 35.06/5.77 % (1549686)Peak memory usage: 149 MB
% 35.06/5.77 % (1549686)Instructions burned: 3395 (million)
% 35.06/5.77 % (1549716)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=2426538183:i=412:gtgl=4:gtg=exists_all_2969 on theBenchmark for (2969ds/412Mi)
% 35.06/5.77 % (1549716)Instruction limit reached!
% 35.06/5.77 % (1549716)------------------------------
% 35.06/5.77 % (1549716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549716)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549716)Termination reason: Instruction limit
% 35.06/5.77 % (1549716)Termination phase: Saturation
% 35.06/5.77 % (1549716)Time elapsed: 0.211 s
% 35.06/5.77 % (1549716)Peak memory usage: 92 MB
% 35.06/5.77 % (1549716)Instructions burned: 413 (million)
% 35.06/5.77 % (1549718)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=456622325:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi)
% 35.06/5.77 % (1549708)Instruction limit reached!
% 35.06/5.77 % (1549708)------------------------------
% 35.06/5.77 % (1549708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549708)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549708)Termination reason: Instruction limit
% 35.06/5.77 % (1549708)Termination phase: Saturation
% 35.06/5.77 % (1549708)Time elapsed: 2.034 s
% 35.06/5.77 % (1549708)Peak memory usage: 148 MB
% 35.06/5.77 % (1549708)Instructions burned: 3257 (million)
% 35.06/5.77 % (1549720)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=3710043577:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2959 on theBenchmark for (2959ds/303Mi)
% 35.06/5.77 % (1549694)Instruction limit reached!
% 35.06/5.77 % (1549694)------------------------------
% 35.06/5.77 % (1549694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549694)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549694)Termination reason: Instruction limit
% 35.06/5.77 % (1549694)Termination phase: Saturation
% 35.06/5.77 % (1549694)Time elapsed: 3.312 s
% 35.06/5.77 % (1549694)Peak memory usage: 153 MB
% 35.06/5.77 % (1549694)Instructions burned: 5209 (million)
% 35.06/5.77 % (1549720)Instruction limit reached!
% 35.06/5.77 % (1549720)------------------------------
% 35.06/5.77 % (1549720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549720)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549720)Termination reason: Instruction limit
% 35.06/5.77 % (1549720)Termination phase: Saturation
% 35.06/5.77 % (1549720)Time elapsed: 0.183 s
% 35.06/5.77 % (1549720)Peak memory usage: 92 MB
% 35.06/5.77 % (1549720)Instructions burned: 303 (million)
% 35.06/5.77 % (1549723)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1467143224:i=598:bs=on:bd=preordered:av=off:ss=axioms_2955 on theBenchmark for (2955ds/598Mi)
% 35.06/5.77 % (1549722)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2240336472:st=4:i=720:sd=3:fsr=off:ss=axioms_2955 on theBenchmark for (2955ds/720Mi)
% 35.06/5.77 % (1549723)First to succeed.
% 35.06/5.77 % (1549723)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1549657"
% 35.06/5.77 % (1549722)Instruction limit reached!
% 35.06/5.77 % (1549722)------------------------------
% 35.06/5.77 % (1549722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.06/5.77 % (1549722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.06/5.77 % (1549722)CaDiCaL version: 2.1.3
% 35.06/5.77 % (1549722)Termination reason: Instruction limit
% 35.06/5.77 % (1549722)Termination phase: Saturation
% 35.06/5.77 % (1549722)Time elapsed: 0.401 s
% 35.06/5.77 % (1549722)Peak memory usage: 95 MB
% 35.06/5.77 % (1549722)Instructions burned: 721 (million)
% 35.06/5.77 % (1549723)Refutation found. Thanks to Tanya!
% 35.06/5.77 % SZS status Unsatisfiable for theBenchmark
% 35.06/5.77 % SZS output start Proof for theBenchmark
% See solution above
% 36.22/5.88 % (1549723)------------------------------
% 36.22/5.88 % (1549723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.22/5.88 % (1549723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.22/5.88 % (1549723)CaDiCaL version: 2.1.3
% 36.22/5.88 % (1549723)Termination reason: Refutation
% 36.22/5.88 % (1549723)Time elapsed: 0.250 s
% 36.22/5.88 % (1549723)Peak memory usage: 93 MB
% 36.22/5.88 % (1549723)Instructions burned: 407 (million)
% 36.22/5.88 % (1549723)------------------------------
% 36.22/5.88 % (1549723)------------------------------
% 36.22/5.88 % (1549657)Success in time 5.092 s
% 36.22/5.88 % Vampire exiting
%------------------------------------------------------------------------------