%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV712-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 : n017.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:16 PM UTC 2026
% Result : Unsatisfiable 33.37s 5.13s
% Output : Refutation 33.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 43
% Syntax : Number of formulae : 114 ( 107 unt; 33 def)
% Number of atoms : 121 ( 110 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 16 ( 9 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 55 ( 55 usr; 40 con; 0-5 aty)
% Number of variables : 55 ( 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f83,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Ouminus__class_Ouminus(X2,X0),X0) = c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Lim_Ominus__diff__minus_0) ).
fof(f336,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| c_HOL_Ominus__class_Ominus(X1,c_HOL_Ouminus__class_Ouminus(X2,X0),X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__minus__eq__add_0) ).
fof(f337,plain,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X2) = c_HOL_Ominus__class_Ominus(X1,c_HOL_Ouminus__class_Ouminus(X2,X0),X0) ),
inference(reorient_equations,[],[f336]) ).
fof(f345,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X0) = c_HOL_Ominus__class_Ominus(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_minus__diff__eq_0) ).
fof(f527,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),c_HOL_Ouminus__class_Ouminus(X1,X0)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X2)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_minus__add__cancel_0) ).
fof(f534,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),c_HOL_Ominus__class_Ominus(X1,X2,X0)),X2) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__add__cancel_0) ).
fof(f722,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____),tc_nat)
| c_FFT__Mirabelle_OIDFT(hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____),X0,X1) = hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc_Ohyps_0) ).
fof(f782,axiom,
c_HOL_Oord__class_Oless(v_i____,hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_True_0) ).
fof(f912,negated_conjecture,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex),c_FFT__Mirabelle_OIDFT(hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____),c_COMBB(v_a____,hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),tc_nat,tc_Complex_Ocomplex,tc_nat),v_i____)),hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____))),tc_Complex_Ocomplex)),v_i____)),c_FFT__Mirabelle_OIDFT(hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____),c_COMBB(v_a____,c_COMBB(c_Suc,hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),tc_nat,tc_nat,tc_nat),tc_nat,tc_Complex_Ocomplex,tc_nat),v_i____))) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex),hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,c_COMBB(v_a____,hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),tc_nat,tc_Complex_Ocomplex,tc_nat)),v_i____)),hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex),hAPP(hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____))),tc_Complex_Ocomplex)),v_i____)),hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,c_COMBB(v_a____,c_COMBB(c_Suc,hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),tc_nat,tc_nat,tc_nat),tc_nat,tc_Complex_Ocomplex,tc_nat)),v_i____))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1004,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add) ).
fof(f1009,axiom,
class_OrderedGroup_Ogroup__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Ogroup__add) ).
fof(f1024,definition,
sF0 = c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1025,plain,
c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex) = sF0,
inference(reorient_equations,[],[f1024]) ).
fof(f1026,definition,
sF1 = c_Power_Opower__class_Opower(tc_nat),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1027,plain,
c_Power_Opower__class_Opower(tc_nat) = sF1,
inference(reorient_equations,[],[f1026]) ).
fof(f1028,definition,
sF2 = c_Int_OBit1(c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1029,plain,
c_Int_OBit1(c_Int_OPls) = sF2,
inference(reorient_equations,[],[f1028]) ).
fof(f1030,definition,
sF3 = c_Int_OBit0(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1031,plain,
c_Int_OBit0(sF2) = sF3,
inference(reorient_equations,[],[f1030]) ).
fof(f1032,definition,
sF4 = c_Int_Onumber__class_Onumber__of(sF3,tc_nat),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1033,plain,
c_Int_Onumber__class_Onumber__of(sF3,tc_nat) = sF4,
inference(reorient_equations,[],[f1032]) ).
fof(f1034,definition,
sF5 = hAPP(sF1,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1035,plain,
hAPP(sF1,sF4) = sF5,
inference(reorient_equations,[],[f1034]) ).
fof(f1036,definition,
sF6 = hAPP(sF5,v_ka____),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1037,plain,
hAPP(sF5,v_ka____) = sF6,
inference(reorient_equations,[],[f1036]) ).
fof(f1038,definition,
sF7 = c_HOL_Otimes__class_Otimes(tc_nat),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1039,plain,
c_HOL_Otimes__class_Otimes(tc_nat) = sF7,
inference(reorient_equations,[],[f1038]) ).
fof(f1040,definition,
sF8 = hAPP(sF7,sF4),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1041,plain,
hAPP(sF7,sF4) = sF8,
inference(reorient_equations,[],[f1040]) ).
fof(f1042,definition,
sF9 = c_COMBB(v_a____,sF8,tc_nat,tc_Complex_Ocomplex,tc_nat),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1043,plain,
c_COMBB(v_a____,sF8,tc_nat,tc_Complex_Ocomplex,tc_nat) = sF9,
inference(reorient_equations,[],[f1042]) ).
fof(f1044,definition,
sF10 = c_FFT__Mirabelle_OIDFT(sF6,sF9,v_i____),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1045,plain,
c_FFT__Mirabelle_OIDFT(sF6,sF9,v_i____) = sF10,
inference(reorient_equations,[],[f1044]) ).
fof(f1046,definition,
sF11 = hAPP(sF0,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1047,plain,
hAPP(sF0,sF10) = sF11,
inference(reorient_equations,[],[f1046]) ).
fof(f1048,definition,
sF12 = c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1049,plain,
c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex) = sF12,
inference(reorient_equations,[],[f1048]) ).
fof(f1050,definition,
sF13 = c_Power_Opower__class_Opower(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1051,plain,
c_Power_Opower__class_Opower(tc_Complex_Ocomplex) = sF13,
inference(reorient_equations,[],[f1050]) ).
fof(f1052,definition,
sF14 = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1053,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF14,
inference(reorient_equations,[],[f1052]) ).
fof(f1054,definition,
sF15 = hAPP(sF8,sF6),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f1055,plain,
hAPP(sF8,sF6) = sF15,
inference(reorient_equations,[],[f1054]) ).
fof(f1056,definition,
sF16 = c_FFT__Mirabelle_Oroot(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f1057,plain,
c_FFT__Mirabelle_Oroot(sF15) = sF16,
inference(reorient_equations,[],[f1056]) ).
fof(f1058,definition,
sF17 = c_HOL_Oinverse__class_Odivide(sF14,sF16,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f1059,plain,
c_HOL_Oinverse__class_Odivide(sF14,sF16,tc_Complex_Ocomplex) = sF17,
inference(reorient_equations,[],[f1058]) ).
fof(f1060,definition,
sF18 = hAPP(sF13,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f1061,plain,
hAPP(sF13,sF17) = sF18,
inference(reorient_equations,[],[f1060]) ).
fof(f1062,definition,
sF19 = hAPP(sF18,v_i____),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f1063,plain,
hAPP(sF18,v_i____) = sF19,
inference(reorient_equations,[],[f1062]) ).
fof(f1064,definition,
sF20 = hAPP(sF12,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f1065,plain,
hAPP(sF12,sF19) = sF20,
inference(reorient_equations,[],[f1064]) ).
fof(f1066,definition,
sF21 = c_COMBB(c_Suc,sF8,tc_nat,tc_nat,tc_nat),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f1067,plain,
c_COMBB(c_Suc,sF8,tc_nat,tc_nat,tc_nat) = sF21,
inference(reorient_equations,[],[f1066]) ).
fof(f1068,definition,
sF22 = c_COMBB(v_a____,sF21,tc_nat,tc_Complex_Ocomplex,tc_nat),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f1069,plain,
c_COMBB(v_a____,sF21,tc_nat,tc_Complex_Ocomplex,tc_nat) = sF22,
inference(reorient_equations,[],[f1068]) ).
fof(f1070,definition,
sF23 = c_FFT__Mirabelle_OIDFT(sF6,sF22,v_i____),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f1071,plain,
c_FFT__Mirabelle_OIDFT(sF6,sF22,v_i____) = sF23,
inference(reorient_equations,[],[f1070]) ).
fof(f1072,definition,
sF24 = hAPP(sF20,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f1073,plain,
hAPP(sF20,sF23) = sF24,
inference(reorient_equations,[],[f1072]) ).
fof(f1074,definition,
sF25 = hAPP(sF11,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f1075,plain,
hAPP(sF11,sF24) = sF25,
inference(reorient_equations,[],[f1074]) ).
fof(f1076,definition,
sF26 = c_FFT__Mirabelle_OIFFT(v_ka____,sF9),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f1077,plain,
c_FFT__Mirabelle_OIFFT(v_ka____,sF9) = sF26,
inference(reorient_equations,[],[f1076]) ).
fof(f1078,definition,
sF27 = hAPP(sF26,v_i____),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f1079,plain,
hAPP(sF26,v_i____) = sF27,
inference(reorient_equations,[],[f1078]) ).
fof(f1080,definition,
sF28 = hAPP(sF0,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f1081,plain,
hAPP(sF0,sF27) = sF28,
inference(reorient_equations,[],[f1080]) ).
fof(f1082,definition,
sF29 = c_FFT__Mirabelle_OIFFT(v_ka____,sF22),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f1083,plain,
c_FFT__Mirabelle_OIFFT(v_ka____,sF22) = sF29,
inference(reorient_equations,[],[f1082]) ).
fof(f1084,definition,
sF30 = hAPP(sF29,v_i____),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f1085,plain,
hAPP(sF29,v_i____) = sF30,
inference(reorient_equations,[],[f1084]) ).
fof(f1086,definition,
sF31 = hAPP(sF20,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f1087,plain,
hAPP(sF20,sF30) = sF31,
inference(reorient_equations,[],[f1086]) ).
fof(f1088,definition,
sF32 = hAPP(sF28,sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f1089,plain,
hAPP(sF28,sF31) = sF32,
inference(reorient_equations,[],[f1088]) ).
fof(f1090,plain,
sF25 != sF32,
inference(definition_folding,[],[f912,f1089,f1087,f1085,f1083,f1069,f1067,f1041,f1033,f1031,f1029,f1039,f1065,f1063,f1061,f1059,f1057,f1055,f1037,f1035,f1033,f1031,f1029,f1027,f1041,f1033,f1031,f1029,f1039,f1053,f1051,f1049,f1081,f1079,f1077,f1043,f1041,f1033,f1031,f1029,f1039,f1025,f1075,f1073,f1071,f1069,f1067,f1041,f1033,f1031,f1029,f1039,f1037,f1035,f1033,f1031,f1029,f1027,f1065,f1063,f1061,f1059,f1057,f1055,f1037,f1035,f1033,f1031,f1029,f1027,f1041,f1033,f1031,f1029,f1039,f1053,f1051,f1049,f1047,f1045,f1043,f1041,f1033,f1031,f1029,f1039,f1037,f1035,f1033,f1031,f1029,f1027,f1025]) ).
fof(f1838,plain,
! [X0,X1] : c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ominus__class_Ominus(X1,X0,tc_Complex_Ocomplex),
inference(resolution,[],[f345,f1004]) ).
fof(f1840,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex)),X1) = X0,
inference(resolution,[],[f534,f1009]) ).
fof(f1841,plain,
! [X0,X1] : hAPP(hAPP(sF0,c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex)),X1) = X0,
inference(forward_demodulation,[],[f1840,f1025]) ).
fof(f2961,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex),X0),X1) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f337,f1009]) ).
fof(f2962,plain,
! [X0,X1] : hAPP(hAPP(sF0,X0),X1) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2961,f1025]) ).
fof(f3722,plain,
! [X0,X1] : c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f83,f1004]) ).
fof(f3723,plain,
! [X0,X1] : c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = hAPP(hAPP(sF0,c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex)),X1),
inference(forward_demodulation,[],[f3722,f2962]) ).
fof(f3725,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X1,X0,tc_Complex_Ocomplex) = hAPP(hAPP(sF0,c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex)),X1),
inference(forward_demodulation,[],[f3723,f1838]) ).
fof(f3904,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex),c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_Complex_Ocomplex),X0),X1)) = X1,
inference(resolution,[],[f527,f1009]) ).
fof(f3905,plain,
! [X0,X1] : hAPP(hAPP(sF0,c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex)),hAPP(hAPP(sF0,X0),X1)) = X1,
inference(forward_demodulation,[],[f3904,f1025]) ).
fof(f3907,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(hAPP(hAPP(sF0,X0),X1),X0,tc_Complex_Ocomplex) = X1,
inference(forward_demodulation,[],[f3905,f3725]) ).
fof(f3987,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(sF11,X0),sF10,tc_Complex_Ocomplex) = X0,
inference(superposition,[],[f3907,f1047]) ).
fof(f3988,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(sF28,X0),sF27,tc_Complex_Ocomplex) = X0,
inference(superposition,[],[f3907,f1081]) ).
fof(f4022,plain,
! [X0] : hAPP(sF11,X0) = hAPP(hAPP(sF0,X0),sF10),
inference(superposition,[],[f1841,f3987]) ).
fof(f4152,plain,
! [X0] : hAPP(sF28,X0) = hAPP(hAPP(sF0,X0),sF27),
inference(superposition,[],[f1841,f3988]) ).
fof(f12867,plain,
! [X0] : c_FFT__Mirabelle_OIDFT(hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),v_ka____),X0,v_i____) = hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),v_i____),
inference(resolution,[],[f722,f782]) ).
fof(f12910,plain,
! [X0] : hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),v_i____) = c_FFT__Mirabelle_OIDFT(hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat)),v_ka____),X0,v_i____),
inference(forward_demodulation,[],[f12867,f1029]) ).
fof(f12932,plain,
! [X0] : hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),v_i____) = c_FFT__Mirabelle_OIDFT(hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),c_Int_Onumber__class_Onumber__of(sF3,tc_nat)),v_ka____),X0,v_i____),
inference(forward_demodulation,[],[f12910,f1031]) ).
fof(f12954,plain,
! [X0] : hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),v_i____) = c_FFT__Mirabelle_OIDFT(hAPP(hAPP(c_Power_Opower__class_Opower(tc_nat),sF4),v_ka____),X0,v_i____),
inference(forward_demodulation,[],[f12932,f1033]) ).
fof(f12976,plain,
! [X0] : hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),v_i____) = c_FFT__Mirabelle_OIDFT(hAPP(hAPP(sF1,sF4),v_ka____),X0,v_i____),
inference(forward_demodulation,[],[f12954,f1027]) ).
fof(f12998,plain,
! [X0] : hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),v_i____) = c_FFT__Mirabelle_OIDFT(hAPP(sF5,v_ka____),X0,v_i____),
inference(forward_demodulation,[],[f12976,f1035]) ).
fof(f13020,plain,
! [X0] : hAPP(c_FFT__Mirabelle_OIFFT(v_ka____,X0),v_i____) = c_FFT__Mirabelle_OIDFT(sF6,X0,v_i____),
inference(forward_demodulation,[],[f12998,f1037]) ).
fof(f13152,plain,
c_FFT__Mirabelle_OIDFT(sF6,sF9,v_i____) = hAPP(sF26,v_i____),
inference(superposition,[],[f13020,f1077]) ).
fof(f13153,plain,
c_FFT__Mirabelle_OIDFT(sF6,sF22,v_i____) = hAPP(sF29,v_i____),
inference(superposition,[],[f13020,f1083]) ).
fof(f13154,plain,
c_FFT__Mirabelle_OIDFT(sF6,sF22,v_i____) = sF30,
inference(forward_demodulation,[],[f13153,f1085]) ).
fof(f13155,plain,
c_FFT__Mirabelle_OIDFT(sF6,sF9,v_i____) = sF27,
inference(forward_demodulation,[],[f13152,f1079]) ).
fof(f13156,plain,
sF23 = sF30,
inference(forward_demodulation,[],[f13154,f1071]) ).
fof(f13157,plain,
sF10 = sF27,
inference(forward_demodulation,[],[f13155,f1045]) ).
fof(f13221,plain,
hAPP(sF20,sF23) = sF31,
inference(superposition,[],[f1087,f13156]) ).
fof(f13222,plain,
sF24 = sF31,
inference(forward_demodulation,[],[f13221,f1073]) ).
fof(f13294,plain,
! [X0] : hAPP(sF28,X0) = hAPP(hAPP(sF0,X0),sF10),
inference(superposition,[],[f4152,f13157]) ).
fof(f13303,plain,
! [X0] : hAPP(sF11,X0) = hAPP(sF28,X0),
inference(forward_demodulation,[],[f13294,f4022]) ).
fof(f13333,plain,
sF32 = hAPP(sF28,sF24),
inference(superposition,[],[f1089,f13222]) ).
fof(f13334,plain,
hAPP(sF11,sF24) = sF32,
inference(forward_demodulation,[],[f13333,f13303]) ).
fof(f13339,plain,
sF25 = sF32,
inference(forward_demodulation,[],[f13334,f1075]) ).
fof(f13340,plain,
$false,
inference(forward_subsumption_resolution,[],[f13339,f1090]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV712-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.25 % Computer : n017.cluster.edu
% 0.09/0.25 % Model : x86_64 x86_64
% 0.09/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.25 % Memory : 8046.5625MB
% 0.09/0.25 % OS : Linux 6.8.0-71-generic
% 0.09/0.25 % CPULimit : 300
% 0.09/0.25 % WCLimit : 300
% 0.09/0.25 % DateTime : Mon Sep 28 12:15:21 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.29 Running first-order model finding
% 0.25/0.29 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
% 19.20/3.06 % (3504827)Will run a generic schedule for satisfiability detection.
% 19.20/3.06 % (3504837)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2887662836:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 19.20/3.06 % (3504832)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2361588390_2999 on theBenchmark for (2999ds/0Mi)
% 19.20/3.06 % (3504833)% WARNING: option uhcvi not known.
% 19.20/3.06 % (3504833)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1110820971:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 19.20/3.06 % (3504836)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1766490328:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 19.20/3.06 % (3504835)dis+10_1_sil=32000:sp=arity:random_seed=3542296718:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 19.20/3.06 % (3504834)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1079847661:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 19.20/3.06 % (3504838)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2594309113:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 19.20/3.06 % (3504837)Instruction limit reached!
% 19.20/3.06 % (3504837)------------------------------
% 19.20/3.06 % (3504837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.20/3.06 % (3504837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.06 % (3504837)CaDiCaL version: 2.1.3
% 19.20/3.06 % (3504837)Termination reason: Instruction limit
% 19.20/3.06 % (3504837)Termination phase: Saturation
% 19.20/3.06 % (3504837)Time elapsed: 0.073 s
% 19.20/3.06 % (3504837)Peak memory usage: 13 MB
% 19.20/3.06 % (3504837)Instructions burned: 132 (million)
% 19.20/3.06 % (3504847)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1573563905:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 19.20/3.06 % (3504835)Instruction limit reached!
% 19.20/3.06 % (3504835)------------------------------
% 19.20/3.06 % (3504835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.20/3.06 % (3504835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.06 % (3504835)CaDiCaL version: 2.1.3
% 19.20/3.06 % (3504835)Termination reason: Instruction limit
% 19.20/3.06 % (3504835)Termination phase: Saturation
% 19.20/3.06 % (3504835)Time elapsed: 0.107 s
% 19.20/3.06 % (3504835)Peak memory usage: 13 MB
% 19.20/3.06 % (3504835)Instructions burned: 103 (million)
% 19.20/3.06 % (3504836)Instruction limit reached!
% 19.20/3.06 % (3504836)------------------------------
% 19.20/3.06 % (3504836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.20/3.06 % (3504836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.06 % (3504836)CaDiCaL version: 2.1.3
% 19.20/3.06 % (3504836)Termination reason: Instruction limit
% 19.20/3.06 % (3504836)Termination phase: Saturation
% 19.20/3.06 % (3504836)Time elapsed: 0.117 s
% 19.20/3.06 % (3504836)Peak memory usage: 13 MB
% 19.20/3.06 % (3504836)Instructions burned: 116 (million)
% 19.20/3.06 % (3504849)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2644919043:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 19.20/3.06 % (3504850)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=1157420883:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 19.20/3.06 % TRYING [1]
% 19.20/3.06 % TRYING [2]
% 19.20/3.06 % (3504838)Instruction limit reached!
% 19.20/3.06 % (3504838)------------------------------
% 19.20/3.06 % (3504838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.20/3.06 % (3504838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.06 % (3504838)CaDiCaL version: 2.1.3
% 19.20/3.06 % (3504838)Termination reason: Instruction limit
% 19.20/3.06 % (3504838)Termination phase: Saturation
% 19.20/3.06 % (3504838)Time elapsed: 0.220 s
% 19.20/3.06 % (3504838)Peak memory usage: 14 MB
% 19.20/3.06 % (3504838)Instructions burned: 159 (million)
% 19.20/3.06 % (3504849)Instruction limit reached!
% 19.20/3.06 % (3504849)------------------------------
% 19.20/3.06 % (3504849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.20/3.06 % (3504849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.06 % (3504849)CaDiCaL version: 2.1.3
% 19.20/3.06 % (3504849)Termination reason: Instruction limit
% 19.20/3.06 % (3504849)Termination phase: Saturation
% 33.37/5.13 % (3504849)Time elapsed: 0.088 s
% 33.37/5.13 % (3504849)Peak memory usage: 13 MB
% 33.37/5.13 % (3504849)Instructions burned: 131 (million)
% 33.37/5.13 % (3504854)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1947319085:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 33.37/5.13 % (3504853)ott-21_1_sil=16000:fs=off:random_seed=1417222893:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 33.37/5.13 % TRYING [3]
% 33.37/5.13 % TRYING [1]
% 33.37/5.13 % TRYING [2]
% 33.37/5.13 % (3504853)Instruction limit reached!
% 33.37/5.13 % (3504853)------------------------------
% 33.37/5.13 % (3504853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504853)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504853)Termination reason: Instruction limit
% 33.37/5.13 % (3504853)Termination phase: Saturation
% 33.37/5.13 % (3504853)Time elapsed: 0.184 s
% 33.37/5.13 % (3504853)Peak memory usage: 13 MB
% 33.37/5.13 % (3504853)Instructions burned: 181 (million)
% 33.37/5.13 % (3504857)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2620377654:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 33.37/5.13 % TRYING [3]
% 33.37/5.13 % (3504847)Instruction limit reached!
% 33.37/5.13 % (3504847)------------------------------
% 33.37/5.13 % (3504847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504847)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504847)Termination reason: Instruction limit
% 33.37/5.13 % (3504847)Termination phase: Finite model building constraint generation
% 33.37/5.13 % (3504847)Time elapsed: 0.586 s
% 33.37/5.13 % (3504847)Peak memory usage: 33 MB
% 33.37/5.13 % (3504847)Instructions burned: 715 (million)
% 33.37/5.13 % (3504861)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2139380021:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 33.37/5.13 % (3504854)Instruction limit reached!
% 33.37/5.13 % (3504854)------------------------------
% 33.37/5.13 % (3504854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504854)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504854)Termination reason: Instruction limit
% 33.37/5.13 % (3504854)Termination phase: Saturation
% 33.37/5.13 % (3504854)Time elapsed: 0.512 s
% 33.37/5.13 % (3504854)Peak memory usage: 14 MB
% 33.37/5.13 % (3504854)Instructions burned: 477 (million)
% 33.37/5.13 % (3504864)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3972076934:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 33.37/5.13 % (3504850)Instruction limit reached!
% 33.37/5.13 % (3504850)------------------------------
% 33.37/5.13 % (3504850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504850)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504850)Termination reason: Instruction limit
% 33.37/5.13 % (3504850)Termination phase: Saturation
% 33.37/5.13 % (3504850)Time elapsed: 0.658 s
% 33.37/5.13 % (3504850)Peak memory usage: 15 MB
% 33.37/5.13 % (3504850)Instructions burned: 685 (million)
% 33.37/5.13 % TRYING [1]
% 33.37/5.13 % (3504866)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=1075972868:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 33.37/5.13 % TRYING [2]
% 33.37/5.13 % TRYING [4]
% 33.37/5.13 % (3504857)Instruction limit reached!
% 33.37/5.13 % (3504857)------------------------------
% 33.37/5.13 % (3504857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504857)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504857)Termination reason: Instruction limit
% 33.37/5.13 % (3504857)Termination phase: Finite model building SAT solving
% 33.37/5.13 % (3504857)Time elapsed: 0.658 s
% 33.37/5.13 % (3504857)Peak memory usage: 35 MB
% 33.37/5.13 % (3504857)Instructions burned: 865 (million)
% 33.37/5.13 % (3504870)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3197728531:i=879:kws=inv_precedence:fsr=off_2987 on theBenchmark for (2987ds/879Mi)
% 33.37/5.13 % (3504866)Instruction limit reached!
% 33.37/5.13 % (3504866)------------------------------
% 33.37/5.13 % (3504866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504866)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504866)Termination reason: Instruction limit
% 33.37/5.13 % (3504866)Termination phase: Saturation
% 33.37/5.13 % (3504866)Time elapsed: 0.740 s
% 33.37/5.13 % (3504866)Peak memory usage: 16 MB
% 33.37/5.13 % (3504866)Instructions burned: 692 (million)
% 33.37/5.13 % (3504873)fmb+10_1_sil=64000:random_seed=3738089512:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi)
% 33.37/5.13 % (3504870)Instruction limit reached!
% 33.37/5.13 % (3504870)------------------------------
% 33.37/5.13 % (3504870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504870)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504870)Termination reason: Instruction limit
% 33.37/5.13 % (3504870)Termination phase: Saturation
% 33.37/5.13 % (3504870)Time elapsed: 0.476 s
% 33.37/5.13 % (3504870)Peak memory usage: 19 MB
% 33.37/5.13 % (3504870)Instructions burned: 879 (million)
% 33.37/5.13 % (3504864)Instruction limit reached!
% 33.37/5.13 % (3504864)------------------------------
% 33.37/5.13 % (3504864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504864)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504864)Termination reason: Instruction limit
% 33.37/5.13 % (3504864)Termination phase: Finite model building constraint generation
% 33.37/5.13 % (3504864)Time elapsed: 0.860 s
% 33.37/5.13 % (3504864)Peak memory usage: 86 MB
% 33.37/5.13 % (3504864)Instructions burned: 889 (million)
% 33.37/5.13 % (3504875)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=398026019:i=9515:nm=5_2982 on theBenchmark for (2982ds/9515Mi)
% 33.37/5.13 % (3504877)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1040355361:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 33.37/5.13 % TRYING [1]
% 33.37/5.13 % TRYING [2]
% 33.37/5.13 % (3504861)Instruction limit reached!
% 33.37/5.13 % (3504861)------------------------------
% 33.37/5.13 % (3504861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504861)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504861)Termination reason: Instruction limit
% 33.37/5.13 % (3504861)Termination phase: Saturation
% 33.37/5.13 % (3504861)Time elapsed: 1.165 s
% 33.37/5.13 % (3504861)Peak memory usage: 19 MB
% 33.37/5.13 % (3504861)Instructions burned: 1179 (million)
% 33.37/5.13 % (3504879)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2095571997:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 33.37/5.13 % TRYING [8]
% 33.37/5.13 % (3504875)Cannot represent all propositional literals internally
% 33.37/5.13 % (3504875)Refutation not found, incomplete strategy
% 33.37/5.13 % (3504875)------------------------------
% 33.37/5.13 % (3504875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504875)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504875)Termination reason: Refutation not found, incomplete strategy
% 33.37/5.13 % (3504875)Time elapsed: 0.307 s
% 33.37/5.13 % (3504875)Peak memory usage: 17 MB
% 33.37/5.13 % (3504875)Instructions burned: 350 (million)
% 33.37/5.13 % (3504875)------------------------------
% 33.37/5.13 % (3504875)------------------------------
% 33.37/5.13 % (3504881)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=292905968:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi)
% 33.37/5.13 % TRYING [3]
% 33.37/5.13 % (3504877)Instruction limit reached!
% 33.37/5.13 % (3504877)------------------------------
% 33.37/5.13 % (3504877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504877)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504877)Termination reason: Instruction limit
% 33.37/5.13 % (3504877)Termination phase: Finite model building constraint generation
% 33.37/5.13 % (3504877)Time elapsed: 0.610 s
% 33.37/5.13 % (3504877)Peak memory usage: 49 MB
% 33.37/5.13 % (3504877)Instructions burned: 921 (million)
% 33.37/5.13 % (3504883)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=72898153:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 33.37/5.13 % (3504883)Cannot represent all propositional literals internally
% 33.37/5.13 % (3504883)Refutation not found, incomplete strategy
% 33.37/5.13 % (3504883)------------------------------
% 33.37/5.13 % (3504883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504883)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504883)Termination reason: Refutation not found, incomplete strategy
% 33.37/5.13 % (3504883)Time elapsed: 0.323 s
% 33.37/5.13 % (3504883)Peak memory usage: 17 MB
% 33.37/5.13 % (3504883)Instructions burned: 358 (million)
% 33.37/5.13 % (3504883)------------------------------
% 33.37/5.13 % (3504883)------------------------------
% 33.37/5.13 % (3504888)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1188216054:fmbsr=2.30978:i=2174_2972 on theBenchmark for (2972ds/2174Mi)
% 33.37/5.13 % (3504881)Instruction limit reached!
% 33.37/5.13 % (3504881)------------------------------
% 33.37/5.13 % (3504881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504881)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504881)Termination reason: Instruction limit
% 33.37/5.13 % (3504881)Termination phase: Saturation
% 33.37/5.13 % (3504881)Time elapsed: 1.414 s
% 33.37/5.13 % (3504881)Peak memory usage: 26 MB
% 33.37/5.13 % (3504881)Instructions burned: 1473 (million)
% 33.37/5.13 % (3504892)ott-2_1_sil=16000:newcnf=on:random_seed=993385280:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2964 on theBenchmark for (2964ds/869Mi)
% 33.37/5.13 % (3504888)Cannot represent all propositional literals internally
% 33.37/5.13 % (3504888)Refutation not found, incomplete strategy
% 33.37/5.13 % (3504888)------------------------------
% 33.37/5.13 % (3504888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504888)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504888)Termination reason: Refutation not found, incomplete strategy
% 33.37/5.13 % (3504888)Time elapsed: 1.303 s
% 33.37/5.13 % (3504888)Peak memory usage: 29 MB
% 33.37/5.13 % (3504888)Instructions burned: 1532 (million)
% 33.37/5.13 % (3504888)------------------------------
% 33.37/5.13 % (3504888)------------------------------
% 33.37/5.13 % (3504896)ott+10_1_sil=32000:tgt=ground:random_seed=3559748456:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi)
% 33.37/5.13 % (3504892)Instruction limit reached!
% 33.37/5.13 % (3504892)------------------------------
% 33.37/5.13 % (3504892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.13 % (3504892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.13 % (3504892)CaDiCaL version: 2.1.3
% 33.37/5.13 % (3504892)Termination reason: Instruction limit
% 33.37/5.13 % (3504892)Termination phase: Saturation
% 33.37/5.13 % (3504892)Time elapsed: 0.844 s
% 33.37/5.13 % (3504892)Peak memory usage: 16 MB
% 33.37/5.13 % (3504892)Instructions burned: 869 (million)
% 33.37/5.13 % (3504898)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3451383124:i=54282_2956 on theBenchmark for (2956ds/54282Mi)
% 33.37/5.13 % (3504896) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3504827-3504896"...
% 33.37/5.13 % (3504896)...printing done.
% 33.37/5.13 % (3504896)Refutation found. Thanks to Tanya!
% 33.37/5.13 % SZS status Unsatisfiable for theBenchmark
% 33.37/5.13 % SZS output start Proof for theBenchmark
% See solution above
% 33.37/5.14 % (3504896)------------------------------
% 33.37/5.14 % (3504896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.37/5.14 % (3504896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.37/5.14 % (3504896)CaDiCaL version: 2.1.3
% 33.37/5.14 % (3504896)Termination reason: Refutation
% 33.37/5.14 % (3504896)Time elapsed: 0.611 s
% 33.37/5.14 % (3504896)Peak memory usage: 16 MB
% 33.37/5.14 % (3504896)Instructions burned: 614 (million)
% 33.37/5.14 % (3504827)Success in time 4.836 s
% 33.37/5.14 % Vampire exiting
%------------------------------------------------------------------------------