%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG360-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 09:19:51 AM UTC 2026
% Result : Unsatisfiable 18.59s 3.35s
% Output : Refutation 19.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 41
% Syntax : Number of formulae : 236 ( 119 unt; 19 def)
% Number of atoms : 421 ( 218 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 326 ( 141 ~; 180 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 6 prp; 0-3 aty)
% Number of functors : 29 ( 29 usr; 19 con; 0-3 aty)
% Number of variables : 145 ( 0 sgn 145 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f241,axiom,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X0)
| c_RealVector_Onorm__class_Onorm(X1,X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| X1 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_norm__eq__zero_0) ).
fof(f242,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_RealVector_Onorm__class_Onorm(X1,X0)
| ~ class_RealVector_Oreal__normed__vector(X0)
| c_HOL_Ozero__class_Ozero(X0) = X1 ),
inference(reorient_equations,[],[f241]) ).
fof(f716,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I10_J_0) ).
fof(f717,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(reorient_equations,[],[f716]) ).
fof(f930,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X2,X0) = X1
| X2 = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_eq__divide__eq_0) ).
fof(f931,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X2,X0) = X1
| c_HOL_Ozero__class_Ozero(X0) = X2 ),
inference(reorient_equations,[],[f930]) ).
fof(f1090,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| X1 = c_HOL_Ozero__class_Ozero(X0)
| c_HOL_Oinverse__class_Odivide(X1,X1,X0) = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_right__inverse__eq_1) ).
fof(f1091,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Ozero__class_Ozero(X0) = X1
| c_HOL_Oone__class_Oone(X0) = c_HOL_Oinverse__class_Odivide(X1,X1,X0) ),
inference(reorient_equations,[],[f1090]) ).
fof(f1131,axiom,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Oinverse(X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_complex__divide__def_0) ).
fof(f1188,axiom,
! [X0] : c_HOL_Osgn__class_Osgn(X0,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X0,c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sgn__eq_0) ).
fof(f1204,axiom,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__less__def_1) ).
fof(f1216,axiom,
! [X2,X0,X1] :
( ~ class_RealVector_Oreal__normed__div__algebra(X0)
| c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X1,X2,X0),X0) = c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(X1,X0),c_RealVector_Onorm__class_Onorm(X2,X0),tc_RealDef_Oreal) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_norm__mult_0) ).
fof(f1250,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I17_J_0) ).
fof(f1251,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0) ),
inference(reorient_equations,[],[f1250]) ).
fof(f1258,axiom,
c_RealVector_Onorm__class_Onorm(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_th0_0) ).
fof(f1259,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(reorient_equations,[],[f1258]) ).
fof(f1266,axiom,
! [X2,X3,X0,X1,X4] :
( ~ class_Ring__and__Field_Ofield(X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X2,X0),c_HOL_Oinverse__class_Odivide(X3,X4,X0),X0) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X3,X0),c_HOL_Otimes__class_Otimes(X2,X4,X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mult__frac__frac_0) ).
fof(f1285,axiom,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__mult__1_0) ).
fof(f1293,axiom,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal) = c_HOL_Otimes__class_Otimes(X1,X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__mult__commute_0) ).
fof(f1294,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,X2,X0) = c_HOL_Otimes__class_Otimes(X2,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I7_J_0) ).
fof(f1295,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X2,X1,X0) = c_HOL_Otimes__class_Otimes(X1,X2,X0) ),
inference(reorient_equations,[],[f1294]) ).
fof(f1318,axiom,
c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f1319,axiom,
v_b != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f1320,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_b,c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1423,axiom,
class_RealVector_Oreal__normed__div__algebra(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra) ).
fof(f1427,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Odivision__by__zero) ).
fof(f1428,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f1431,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f1453,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ofield) ).
fof(f1459,definition,
sF0 = c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1460,plain,
c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex) = sF0,
inference(reorient_equations,[],[f1459]) ).
fof(f1461,definition,
sF1 = c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1462,plain,
c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex) = sF1,
inference(reorient_equations,[],[f1461]) ).
fof(f1463,definition,
sF2 = c_HOL_Oinverse__class_Odivide(sF1,v_b,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1464,plain,
c_HOL_Oinverse__class_Odivide(sF1,v_b,tc_Complex_Ocomplex) = sF2,
inference(reorient_equations,[],[f1463]) ).
fof(f1465,definition,
sF3 = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1466,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF3,
inference(reorient_equations,[],[f1465]) ).
fof(f1467,definition,
sF4 = c_HOL_Otimes__class_Otimes(sF2,sF3,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1468,plain,
c_HOL_Otimes__class_Otimes(sF2,sF3,tc_Complex_Ocomplex) = sF4,
inference(reorient_equations,[],[f1467]) ).
fof(f1469,definition,
sF5 = c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1470,plain,
c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex) = sF5,
inference(reorient_equations,[],[f1469]) ).
fof(f1471,definition,
sF6 = c_HOL_Oinverse__class_Odivide(sF5,sF1,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1472,plain,
c_HOL_Oinverse__class_Odivide(sF5,sF1,tc_Complex_Ocomplex) = sF6,
inference(reorient_equations,[],[f1471]) ).
fof(f1473,definition,
sF7 = c_HOL_Otimes__class_Otimes(v_b,sF6,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1474,plain,
c_HOL_Otimes__class_Otimes(v_b,sF6,tc_Complex_Ocomplex) = sF7,
inference(reorient_equations,[],[f1473]) ).
fof(f1475,definition,
sF8 = c_HOL_Otimes__class_Otimes(sF2,sF7,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1476,plain,
c_HOL_Otimes__class_Otimes(sF2,sF7,tc_Complex_Ocomplex) = sF8,
inference(reorient_equations,[],[f1475]) ).
fof(f1477,definition,
sF9 = c_HOL_Oplus__class_Oplus(sF4,sF8,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1478,plain,
c_HOL_Oplus__class_Oplus(sF4,sF8,tc_Complex_Ocomplex) = sF9,
inference(reorient_equations,[],[f1477]) ).
fof(f1479,definition,
sF10 = c_RealVector_Onorm__class_Onorm(sF9,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1480,plain,
c_RealVector_Onorm__class_Onorm(sF9,tc_Complex_Ocomplex) = sF10,
inference(reorient_equations,[],[f1479]) ).
fof(f1481,definition,
sF11 = c_RealVector_Onorm__class_Onorm(sF2,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1482,plain,
c_RealVector_Onorm__class_Onorm(sF2,tc_Complex_Ocomplex) = sF11,
inference(reorient_equations,[],[f1481]) ).
fof(f1483,definition,
sF12 = c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1484,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = sF12,
inference(reorient_equations,[],[f1483]) ).
fof(f1485,definition,
sF13 = c_HOL_Otimes__class_Otimes(sF11,sF12,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1486,plain,
c_HOL_Otimes__class_Otimes(sF11,sF12,tc_RealDef_Oreal) = sF13,
inference(reorient_equations,[],[f1485]) ).
fof(f1487,plain,
~ c_HOL_Oord__class_Oless(sF10,sF13,tc_RealDef_Oreal),
inference(definition_folding,[],[f1320,f1486,f1484,f1482,f1464,f1462,f1460,f1480,f1478,f1476,f1474,f1472,f1462,f1460,f1470,f1464,f1462,f1460,f1468,f1466,f1464,f1462,f1460]) ).
fof(f1492,plain,
c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1318,f1460]) ).
fof(f1493,plain,
c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF12,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1492,f1484]) ).
fof(f1494,plain,
c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),sF5,tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF12,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1493,f1470]) ).
fof(f1495,plain,
c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(sF1,v_b,tc_Complex_Ocomplex),sF5,tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF12,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1494,f1462]) ).
fof(f1496,plain,
c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(sF2,sF5,tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF12,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1495,f1464]) ).
fof(f1507,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF12,X0,tc_RealDef_Oreal) = X0,
inference(superposition,[],[f1285,f1484]) ).
fof(f1511,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(superposition,[],[f1293,f1285]) ).
fof(f1512,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,sF12,tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[],[f1511,f1484]) ).
fof(f1527,plain,
sF11 = sF13,
inference(superposition,[],[f1486,f1512]) ).
fof(f1528,plain,
~ c_HOL_Oord__class_Oless(sF10,sF11,tc_RealDef_Oreal),
inference(superposition,[],[f1487,f1527]) ).
fof(f1624,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f1259,f1460]) ).
fof(f1625,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Oinverse__class_Odivide(sF1,v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1624,f1462]) ).
fof(f1626,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(sF2,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1625,f1464]) ).
fof(f1627,plain,
c_HOL_Oone__class_Oone(tc_RealDef_Oreal) = sF11,
inference(forward_demodulation,[],[f1626,f1482]) ).
fof(f1628,plain,
sF11 = sF12,
inference(forward_demodulation,[],[f1627,f1484]) ).
fof(f1629,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,sF11,tc_RealDef_Oreal) = X0,
inference(superposition,[],[f1512,f1628]) ).
fof(f1630,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF11,X0,tc_RealDef_Oreal) = X0,
inference(superposition,[],[f1507,f1628]) ).
fof(f1631,plain,
c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(sF2,sF5,tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF11,tc_RealDef_Oreal),
inference(superposition,[],[f1496,f1628]) ).
fof(f1943,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex),
inference(resolution,[],[f1428,f1295]) ).
fof(f1952,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex),
inference(superposition,[],[f1131,f1943]) ).
fof(f1953,plain,
sF7 = c_HOL_Otimes__class_Otimes(sF6,v_b,tc_Complex_Ocomplex),
inference(superposition,[],[f1474,f1943]) ).
fof(f2142,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF0
| ~ class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f242,f1460]) ).
fof(f2146,plain,
( c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF0
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(forward_subsumption_resolution,[],[f2142,f1431]) ).
fof(f2148,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != sF0,
inference(forward_subsumption_resolution,[],[f2146,f1319]) ).
fof(f2296,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0
| c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X0,X0,tc_Complex_Ocomplex) ),
inference(resolution,[],[f1453,f1091]) ).
fof(f2725,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(X1,tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(resolution,[],[f1423,f1216]) ).
fof(f2728,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(sF2,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF11,c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(superposition,[],[f2725,f1482]) ).
fof(f2744,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(X1,tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(superposition,[],[f1293,f2725]) ).
fof(f2761,plain,
! [X0,X1] : c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2744,f2725]) ).
fof(f2768,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(sF2,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2728,f1630]) ).
fof(f2847,plain,
! [X0] :
( sF3 = c_HOL_Oinverse__class_Odivide(X0,X0,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(forward_demodulation,[],[f2296,f1466]) ).
fof(f2977,plain,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(X2,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(resolution,[],[f1266,f1453]) ).
fof(f2978,plain,
! [X2,X3,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(X2,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X2,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,X3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f2977,f1427]) ).
fof(f2989,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,v_b,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(X1,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),sF7,tc_Complex_Ocomplex),
inference(superposition,[],[f2978,f1474]) ).
fof(f3076,definition,
( spl14_66
<=> c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF2 ),
introduced(definition,[new_symbols(definition,[spl14_66])],[avatar_definition]) ).
fof(f3077,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF2
| spl14_66 ),
inference(avatar_component_clause,[],[f3076]) ).
fof(f3078,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF2
| ~ spl14_66 ),
inference(avatar_component_clause,[],[f3076]) ).
fof(f3168,plain,
! [X0] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(v_b,X0,tc_Complex_Ocomplex),sF7,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f2989,f2847]) ).
fof(f3202,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(v_b,X0,tc_Complex_Ocomplex),sF7,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(X0,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f3168,f1319]) ).
fof(f3537,definition,
( spl14_77
<=> c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
introduced(definition,[new_symbols(definition,[spl14_77])],[avatar_definition]) ).
fof(f3538,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF1
| spl14_77 ),
inference(avatar_component_clause,[],[f3537]) ).
fof(f3539,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1
| ~ spl14_77 ),
inference(avatar_component_clause,[],[f3537]) ).
fof(f3739,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(resolution,[],[f1251,f1428]) ).
fof(f3742,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(superposition,[],[f3739,f1131]) ).
fof(f3757,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF7,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(v_b,c_HOL_Otimes__class_Otimes(sF6,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3739,f1474]) ).
fof(f3758,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF4,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(sF3,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3739,f1468]) ).
fof(f3759,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF8,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(sF7,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3739,f1476]) ).
fof(f3760,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF7,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Otimes__class_Otimes(v_b,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3739,f1953]) ).
fof(f3775,plain,
! [X2,X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Oinverse(X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f1131,f3739]) ).
fof(f3777,plain,
! [X2,X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f3775,f1131]) ).
fof(f3788,plain,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X2,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f3742,f1952]) ).
fof(f3804,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF7,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(v_b,c_HOL_Otimes__class_Otimes(X0,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3757,f1943]) ).
fof(f3833,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF2,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF1,c_HOL_Oinverse__class_Odivide(X0,v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3788,f1464]) ).
fof(f3921,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF4,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(X0,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3758,f1943]) ).
fof(f3947,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oinverse__class_Odivide(sF7,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF8,c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3759,f1131]) ).
fof(f3962,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oinverse__class_Odivide(sF7,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF8,X0,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f3947,f1131]) ).
fof(f4024,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(sF7,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Oinverse__class_Odivide(v_b,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3777,f1953]) ).
fof(f4300,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF7,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF6,c_HOL_Otimes__class_Otimes(X0,v_b,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3760,f1943]) ).
fof(f4383,plain,
( c_HOL_Oinverse__class_Odivide(sF7,v_b,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF6,sF3,tc_Complex_Ocomplex)
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f4024,f2847]) ).
fof(f4400,plain,
c_HOL_Oinverse__class_Odivide(sF7,v_b,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF6,sF3,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f4383,f1319]) ).
fof(f4410,plain,
c_HOL_Otimes__class_Otimes(sF2,sF7,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF1,c_HOL_Otimes__class_Otimes(sF6,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3833,f4400]) ).
fof(f4446,plain,
sF8 = c_HOL_Otimes__class_Otimes(sF1,c_HOL_Otimes__class_Otimes(sF6,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f4410,f1476]) ).
fof(f4958,plain,
c_HOL_Oinverse__class_Odivide(sF8,v_b,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Otimes__class_Otimes(sF6,sF3,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3962,f4400]) ).
fof(f4983,plain,
c_HOL_Oinverse__class_Odivide(sF8,v_b,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF4,sF6,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f4958,f3921]) ).
fof(f5215,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex)
| c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = X0
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1 ),
inference(resolution,[],[f931,f1453]) ).
fof(f5216,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = X0
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1 ),
inference(forward_subsumption_resolution,[],[f5215,f1427]) ).
fof(f5217,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1 ),
inference(forward_demodulation,[],[f5216,f3788]) ).
fof(f5218,plain,
( ! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0
| sF1 = X1 )
| ~ spl14_77 ),
inference(forward_demodulation,[],[f5217,f3539]) ).
fof(f5219,plain,
( ! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X0,sF3,tc_Complex_Ocomplex) = X0
| sF1 = X1
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1 )
| ~ spl14_77 ),
inference(superposition,[],[f5218,f2847]) ).
fof(f5334,plain,
( ! [X0,X1] :
( sF1 = X1
| c_HOL_Otimes__class_Otimes(X0,sF3,tc_Complex_Ocomplex) = X0
| sF1 = X1 )
| ~ spl14_77 ),
inference(forward_demodulation,[],[f5219,f3539]) ).
fof(f5335,plain,
( ! [X0,X1] :
( sF1 = X1
| c_HOL_Otimes__class_Otimes(X0,sF3,tc_Complex_Ocomplex) = X0 )
| ~ spl14_77 ),
inference(duplicate_literal_removal,[],[f5334]) ).
fof(f5342,definition,
( spl14_82
<=> sF2 = sF4 ),
introduced(definition,[new_symbols(definition,[spl14_82])],[avatar_definition]) ).
fof(f5343,plain,
( sF2 != sF4
| spl14_82 ),
inference(avatar_component_clause,[],[f5342]) ).
fof(f5344,plain,
( sF2 = sF4
| ~ spl14_82 ),
inference(avatar_component_clause,[],[f5342]) ).
fof(f5395,definition,
( spl14_88
<=> ! [X0] : c_HOL_Otimes__class_Otimes(X0,sF3,tc_Complex_Ocomplex) = X0 ),
introduced(definition,[new_symbols(definition,[spl14_88])],[avatar_definition]) ).
fof(f5396,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(X0,sF3,tc_Complex_Ocomplex) = X0
| ~ spl14_88 ),
inference(avatar_component_clause,[],[f5395]) ).
fof(f5398,definition,
( spl14_89
<=> ! [X1] : sF1 = X1 ),
introduced(definition,[new_symbols(definition,[spl14_89])],[avatar_definition]) ).
fof(f5399,plain,
( ! [X1] : sF1 = X1
| ~ spl14_89 ),
inference(avatar_component_clause,[],[f5398]) ).
fof(f5400,plain,
( spl14_88
| spl14_89
| ~ spl14_77 ),
inference(avatar_split_clause,[],[f5335,f3537,f5398,f5395]) ).
fof(f5717,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Odivide(X1,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X0
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1 ),
inference(superposition,[],[f1943,f5217]) ).
fof(f5750,plain,
( sF1 = c_HOL_Otimes__class_Otimes(sF2,v_b,tc_Complex_Ocomplex)
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f3833,f5217]) ).
fof(f5768,plain,
sF1 = c_HOL_Otimes__class_Otimes(sF2,v_b,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f5750,f1319]) ).
fof(f5791,plain,
! [X0,X1] :
( c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X1 ),
inference(forward_demodulation,[],[f5717,f3788]) ).
fof(f6003,plain,
( sF9 = c_HOL_Oplus__class_Oplus(sF2,sF8,tc_Complex_Ocomplex)
| ~ spl14_82 ),
inference(superposition,[],[f1478,f5344]) ).
fof(f6244,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(sF3,X0,tc_Complex_Ocomplex) = X0
| ~ spl14_88 ),
inference(superposition,[],[f1943,f5396]) ).
fof(f6304,plain,
c_RealVector_Onorm__class_Onorm(v_b,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(sF1,tc_Complex_Ocomplex),
inference(superposition,[],[f2768,f5768]) ).
fof(f6305,plain,
c_HOL_Otimes__class_Otimes(sF7,sF2,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF6,sF1,tc_Complex_Ocomplex),
inference(superposition,[],[f4300,f5768]) ).
fof(f6309,plain,
! [X0] : c_HOL_Oinverse__class_Odivide(sF1,X0,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oinverse__class_Odivide(v_b,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f3777,f5768]) ).
fof(f6322,plain,
sF0 = c_RealVector_Onorm__class_Onorm(sF1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f6304,f1460]) ).
fof(f6332,plain,
c_HOL_Osgn__class_Osgn(sF1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF1,c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f1188,f6322]) ).
fof(f6335,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),sF0,tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X0,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f2725,f6322]) ).
fof(f6338,plain,
c_HOL_Osgn__class_Osgn(sF1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF1,sF1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f6332,f1462]) ).
fof(f6343,plain,
! [X0] :
( c_HOL_Otimes__class_Otimes(X0,c_HOL_Osgn__class_Osgn(sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
inference(superposition,[],[f5217,f6338]) ).
fof(f6344,plain,
( sF3 = c_HOL_Osgn__class_Osgn(sF1,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
inference(superposition,[],[f2847,f6338]) ).
fof(f7758,plain,
( sF1 = sF2
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_demodulation,[],[f3539,f3078]) ).
fof(f8290,plain,
( sF1 = c_HOL_Otimes__class_Otimes(v_b,sF2,tc_Complex_Ocomplex)
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f5791,f1464]) ).
fof(f8293,plain,
( sF5 = c_HOL_Otimes__class_Otimes(sF1,sF6,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
inference(superposition,[],[f5791,f1472]) ).
fof(f8340,plain,
( sF7 = c_HOL_Oinverse__class_Odivide(sF8,sF2,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF2 ),
inference(superposition,[],[f3962,f5791]) ).
fof(f8353,plain,
( sF7 = c_HOL_Oinverse__class_Odivide(sF8,sF2,tc_Complex_Ocomplex)
| spl14_66 ),
inference(forward_subsumption_resolution,[],[f8340,f3077]) ).
fof(f8394,plain,
sF1 = c_HOL_Otimes__class_Otimes(v_b,sF2,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f8290,f1319]) ).
fof(f9050,plain,
( c_HOL_Oinverse__class_Odivide(sF1,v_b,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF2,sF3,tc_Complex_Ocomplex)
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f6309,f2847]) ).
fof(f9055,plain,
( v_b = c_HOL_Oinverse__class_Odivide(sF1,sF2,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF2 ),
inference(superposition,[],[f5791,f6309]) ).
fof(f9075,plain,
( v_b = c_HOL_Oinverse__class_Odivide(sF1,sF2,tc_Complex_Ocomplex)
| spl14_66 ),
inference(forward_subsumption_resolution,[],[f9055,f3077]) ).
fof(f9078,plain,
c_HOL_Oinverse__class_Odivide(sF1,v_b,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF2,sF3,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f9050,f1319]) ).
fof(f9087,plain,
c_HOL_Oinverse__class_Odivide(sF1,v_b,tc_Complex_Ocomplex) = sF4,
inference(forward_demodulation,[],[f9078,f1468]) ).
fof(f9617,plain,
( sF8 = c_HOL_Otimes__class_Otimes(v_b,c_HOL_Otimes__class_Otimes(sF4,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| v_b = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(superposition,[],[f5791,f4983]) ).
fof(f9629,plain,
sF8 = c_HOL_Otimes__class_Otimes(v_b,c_HOL_Otimes__class_Otimes(sF4,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f9617,f1319]) ).
fof(f9643,plain,
sF8 = c_HOL_Otimes__class_Otimes(sF7,sF4,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f9629,f3804]) ).
fof(f9656,plain,
( sF8 = c_HOL_Otimes__class_Otimes(sF7,sF2,tc_Complex_Ocomplex)
| ~ spl14_82 ),
inference(forward_demodulation,[],[f9643,f5344]) ).
fof(f9855,plain,
( sF8 = c_HOL_Otimes__class_Otimes(sF1,sF6,tc_Complex_Ocomplex)
| ~ spl14_88 ),
inference(superposition,[],[f4446,f5396]) ).
fof(f10423,plain,
c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(sF2,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF1,sF7,tc_Complex_Ocomplex),
inference(superposition,[],[f3202,f8394]) ).
fof(f16809,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f717,f1428]) ).
fof(f16958,plain,
( sF0 != sF1
| ~ spl14_89 ),
inference(superposition,[],[f2148,f5399]) ).
fof(f18089,plain,
( $false
| ~ spl14_89 ),
inference(forward_subsumption_resolution,[],[f16958,f5399]) ).
fof(f18090,plain,
~ spl14_89,
inference(avatar_contradiction_clause,[],[f18089]) ).
fof(f18392,plain,
( ! [X0] : sF1 = c_HOL_Otimes__class_Otimes(X0,sF1,tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(forward_demodulation,[],[f16809,f3539]) ).
fof(f18637,plain,
( c_HOL_Oinverse__class_Odivide(sF2,sF6,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF1,sF7,tc_Complex_Ocomplex)
| ~ spl14_88 ),
inference(forward_demodulation,[],[f10423,f6244]) ).
fof(f19708,plain,
( sF1 != sF2
| spl14_66
| ~ spl14_77 ),
inference(superposition,[],[f3077,f3539]) ).
fof(f20704,plain,
( sF1 = c_HOL_Otimes__class_Otimes(sF7,sF2,tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(forward_demodulation,[],[f6305,f18392]) ).
fof(f20760,plain,
( sF1 = sF8
| ~ spl14_77
| ~ spl14_82 ),
inference(forward_demodulation,[],[f20704,f9656]) ).
fof(f20831,plain,
( sF7 = c_HOL_Oinverse__class_Odivide(sF1,sF2,tc_Complex_Ocomplex)
| spl14_66
| ~ spl14_77
| ~ spl14_82 ),
inference(superposition,[],[f8353,f20760]) ).
fof(f20832,plain,
( v_b = sF7
| spl14_66
| ~ spl14_77
| ~ spl14_82 ),
inference(forward_demodulation,[],[f20831,f9075]) ).
fof(f20954,plain,
( sF2 = c_HOL_Oinverse__class_Odivide(sF1,sF7,tc_Complex_Ocomplex)
| spl14_66
| ~ spl14_77
| ~ spl14_82 ),
inference(superposition,[],[f1464,f20832]) ).
fof(f21004,plain,
( sF2 = c_HOL_Oinverse__class_Odivide(sF2,sF6,tc_Complex_Ocomplex)
| spl14_66
| ~ spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(forward_demodulation,[],[f20954,f18637]) ).
fof(f21686,plain,
( ! [X0] : sF1 = c_HOL_Otimes__class_Otimes(sF1,X0,tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(superposition,[],[f1943,f18392]) ).
fof(f21692,plain,
( ! [X0,X1] : c_HOL_Oinverse__class_Odivide(sF1,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(sF1,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(superposition,[],[f3777,f18392]) ).
fof(f21714,plain,
( ! [X0,X1] : sF1 = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(sF1,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(superposition,[],[f3788,f18392]) ).
fof(f21716,plain,
( c_HOL_Oinverse__class_Odivide(sF1,sF7,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF3,c_HOL_Oinverse__class_Odivide(sF1,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(superposition,[],[f3202,f18392]) ).
fof(f21735,plain,
( c_HOL_Oinverse__class_Odivide(sF1,sF6,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF1,sF7,tc_Complex_Ocomplex)
| ~ spl14_77
| ~ spl14_88 ),
inference(forward_demodulation,[],[f21716,f6244]) ).
fof(f21740,plain,
( ! [X1] : sF1 = c_HOL_Oinverse__class_Odivide(sF1,X1,tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(forward_demodulation,[],[f21692,f21714]) ).
fof(f21749,plain,
( c_HOL_Oinverse__class_Odivide(sF1,sF6,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF2,sF6,tc_Complex_Ocomplex)
| ~ spl14_77
| ~ spl14_88 ),
inference(forward_demodulation,[],[f21735,f18637]) ).
fof(f21830,plain,
( sF2 = c_HOL_Oinverse__class_Odivide(sF1,sF6,tc_Complex_Ocomplex)
| spl14_66
| ~ spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(forward_demodulation,[],[f21749,f21004]) ).
fof(f21876,plain,
( sF1 = sF2
| spl14_66
| ~ spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(forward_demodulation,[],[f21830,f21740]) ).
fof(f21902,plain,
( $false
| spl14_66
| ~ spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f21876,f19708]) ).
fof(f21903,plain,
( spl14_66
| ~ spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f21902]) ).
fof(f22176,plain,
( sF0 = c_RealVector_Onorm__class_Onorm(sF2,tc_Complex_Ocomplex)
| ~ spl14_66
| ~ spl14_77 ),
inference(superposition,[],[f6322,f7758]) ).
fof(f22180,plain,
( sF0 = sF11
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_demodulation,[],[f22176,f1482]) ).
fof(f22203,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(X0,sF0,tc_RealDef_Oreal) = X0
| ~ spl14_66
| ~ spl14_77 ),
inference(superposition,[],[f1629,f22180]) ).
fof(f23263,plain,
( ! [X0] : c_RealVector_Onorm__class_Onorm(sF1,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(X0,sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(superposition,[],[f2761,f21686]) ).
fof(f23308,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),sF0,tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(sF1,tc_Complex_Ocomplex)
| ~ spl14_77 ),
inference(forward_demodulation,[],[f23263,f6335]) ).
fof(f23317,plain,
( ! [X0] : sF0 = c_HOL_Otimes__class_Otimes(c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex),sF0,tc_RealDef_Oreal)
| ~ spl14_77 ),
inference(forward_demodulation,[],[f23308,f6322]) ).
fof(f23321,plain,
( ! [X0] : c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex) = sF0
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_demodulation,[],[f23317,f22203]) ).
fof(f23382,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ spl14_66
| ~ spl14_77 ),
inference(superposition,[],[f1318,f23321]) ).
fof(f23399,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF12,tc_RealDef_Oreal)
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_demodulation,[],[f23382,f1484]) ).
fof(f23430,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF11,tc_RealDef_Oreal)
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_demodulation,[],[f23399,f1628]) ).
fof(f23458,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(c_RealVector_Oof__real(sF0,tc_Complex_Ocomplex),v_b,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(v_v____,v_na____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),sF0,tc_RealDef_Oreal)
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_demodulation,[],[f23430,f22180]) ).
fof(f23465,plain,
( c_HOL_Oord__class_Oless(sF0,sF0,tc_RealDef_Oreal)
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_demodulation,[],[f23458,f23321]) ).
fof(f23470,plain,
( $false
| ~ spl14_66
| ~ spl14_77 ),
inference(forward_subsumption_resolution,[],[f23465,f1204]) ).
fof(f23471,plain,
( ~ spl14_66
| ~ spl14_77 ),
inference(avatar_contradiction_clause,[],[f23470]) ).
fof(f23478,plain,
( sF3 = c_HOL_Osgn__class_Osgn(sF1,tc_Complex_Ocomplex)
| spl14_77 ),
inference(forward_subsumption_resolution,[],[f6344,f3538]) ).
fof(f23479,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Osgn__class_Osgn(sF1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0
| spl14_77 ),
inference(forward_subsumption_resolution,[],[f6343,f3538]) ).
fof(f23484,plain,
( sF5 = c_HOL_Otimes__class_Otimes(sF1,sF6,tc_Complex_Ocomplex)
| spl14_77 ),
inference(forward_subsumption_resolution,[],[f8293,f3538]) ).
fof(f23613,plain,
( ! [X0] : c_HOL_Otimes__class_Otimes(X0,sF3,tc_Complex_Ocomplex) = X0
| spl14_77 ),
inference(forward_demodulation,[],[f23479,f23478]) ).
fof(f23614,plain,
( sF5 = sF8
| spl14_77
| ~ spl14_88 ),
inference(forward_demodulation,[],[f23484,f9855]) ).
fof(f23914,plain,
( sF9 = c_HOL_Oplus__class_Oplus(sF2,sF5,tc_Complex_Ocomplex)
| spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(superposition,[],[f6003,f23614]) ).
fof(f27403,plain,
( c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(sF9,tc_Complex_Ocomplex),sF11,tc_RealDef_Oreal)
| spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(superposition,[],[f1631,f23914]) ).
fof(f27419,plain,
( c_HOL_Oord__class_Oless(sF10,sF11,tc_RealDef_Oreal)
| spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(forward_demodulation,[],[f27403,f1480]) ).
fof(f27424,plain,
( $false
| spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f27419,f1528]) ).
fof(f27425,plain,
( spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f27424]) ).
fof(f27495,plain,
sF2 = sF4,
inference(forward_demodulation,[],[f9087,f1464]) ).
fof(f27746,plain,
( $false
| spl14_82 ),
inference(forward_subsumption_resolution,[],[f27495,f5343]) ).
fof(f27747,plain,
spl14_82,
inference(avatar_contradiction_clause,[],[f27746]) ).
fof(f28427,plain,
( spl14_88
| spl14_77 ),
inference(avatar_split_clause,[],[f23613,f3537,f5395]) ).
cnf(s78,plain,
( ~ spl14_77
| spl14_88
| spl14_89 ),
inference(sat_conversion,[],[f5400]) ).
cnf(s440,plain,
~ spl14_89,
inference(sat_conversion,[],[f18090]) ).
cnf(s502,plain,
( spl14_66
| ~ spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(sat_conversion,[],[f21903]) ).
cnf(s510,plain,
( ~ spl14_66
| ~ spl14_77 ),
inference(sat_conversion,[],[f23471]) ).
cnf(s598,plain,
( spl14_77
| ~ spl14_82
| ~ spl14_88 ),
inference(sat_conversion,[],[f27425]) ).
cnf(s607,plain,
spl14_82,
inference(sat_conversion,[],[f27747]) ).
cnf(s615,plain,
( spl14_77
| spl14_88 ),
inference(sat_conversion,[],[f28427]) ).
cnf(s620,plain,
( spl14_77
| ~ spl14_88 ),
inference(rat,[],[s598,s607]) ).
cnf(s653,plain,
( spl14_66
| ~ spl14_77
| ~ spl14_88 ),
inference(rat,[],[s502,s607]) ).
cnf(s721,plain,
( ~ spl14_77
| spl14_88 ),
inference(rat,[],[s78,s440]) ).
cnf(s722,plain,
( ~ spl14_77
| spl14_66 ),
inference(rat,[],[s721,s653]) ).
cnf(s723,plain,
spl14_77,
inference(rat,[],[s620,s615]) ).
cnf(s724,plain,
~ spl14_66,
inference(rat,[],[s510,s723]) ).
cnf(s725,plain,
$false,
inference(rat,[],[s722,s724,s723]) ).
fof(f29034,plain,
$false,
inference(avatar_sat_refutation,[],[s725]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG360-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n001.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 20:16:18 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.46/2.16 % (678337)Input is clausal, will run a generic CNF schedule.
% 10.46/2.16 % (678346)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=487705116:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.46/2.16 % (678347)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4047356611:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.46/2.16 % (678348)dis-21_1_sil=8000:lcm=predicate:random_seed=2320198678:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.46/2.16 % (678344)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1900137019:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.46/2.16 % (678345)lrs+10_1_sil=8000:sp=occurrence:random_seed=3204601519:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.46/2.16 % (678342)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=2203867155:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.46/2.16 % (678343)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2188509485:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.46/2.16 % (678346)Instruction limit reached!
% 10.46/2.16 % (678346)------------------------------
% 10.46/2.16 % (678346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.16 % (678346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.16 % (678346)CaDiCaL version: 2.1.3
% 10.46/2.16 % (678346)Termination reason: Instruction limit
% 10.46/2.16 % (678346)Termination phase: Saturation
% 10.46/2.16 % (678346)Time elapsed: 0.042 s
% 10.46/2.16 % (678346)Peak memory usage: 90 MB
% 10.46/2.16 % (678346)Instructions burned: 117 (million)
% 10.46/2.16 % (678348)Instruction limit reached!
% 10.46/2.16 % (678348)------------------------------
% 10.46/2.16 % (678348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.16 % (678348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.16 % (678348)CaDiCaL version: 2.1.3
% 10.46/2.16 % (678348)Termination reason: Instruction limit
% 10.46/2.16 % (678348)Termination phase: Saturation
% 10.46/2.16 % (678348)Time elapsed: 0.063 s
% 10.46/2.16 % (678348)Peak memory usage: 89 MB
% 10.46/2.16 % (678348)Instructions burned: 118 (million)
% 10.46/2.16 % (678345)Instruction limit reached!
% 10.46/2.16 % (678345)------------------------------
% 10.46/2.16 % (678345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.16 % (678345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.16 % (678345)CaDiCaL version: 2.1.3
% 10.46/2.16 % (678345)Termination reason: Instruction limit
% 10.46/2.16 % (678345)Termination phase: Saturation
% 10.46/2.16 % (678345)Time elapsed: 0.072 s
% 10.46/2.16 % (678345)Peak memory usage: 89 MB
% 10.46/2.16 % (678345)Instructions burned: 107 (million)
% 10.46/2.16 % (678347)Instruction limit reached!
% 10.46/2.16 % (678347)------------------------------
% 10.46/2.16 % (678347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.16 % (678347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.16 % (678347)CaDiCaL version: 2.1.3
% 10.46/2.16 % (678347)Termination reason: Instruction limit
% 10.46/2.16 % (678347)Termination phase: Saturation
% 10.46/2.16 % (678347)Time elapsed: 0.117 s
% 10.46/2.16 % (678347)Peak memory usage: 90 MB
% 10.46/2.16 % (678347)Instructions burned: 180 (million)
% 10.46/2.16 % (678356)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=2655549060:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.46/2.16 % (678356)Refutation not found, incomplete strategy
% 10.46/2.16 % (678356)------------------------------
% 10.46/2.16 % (678356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.16 % (678356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.16 % (678356)CaDiCaL version: 2.1.3
% 10.46/2.16 % (678356)Termination reason: Refutation not found, incomplete strategy
% 10.46/2.16 % (678356)Time elapsed: 0.004 s
% 10.46/2.16 % (678356)Peak memory usage: 89 MB
% 10.46/2.16 % (678356)Instructions burned: 10 (million)
% 10.46/2.16 % (678357)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=907674163: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)
% 18.59/3.35 % (678358)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3748894555:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 18.59/3.35 % (678359)lrs+10_64_to=lpo:sil=8000:random_seed=2056288372:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 18.59/3.35 % (678356)------------------------------
% 18.59/3.35 % (678356)------------------------------
% 18.59/3.35 % (678357)Instruction limit reached!
% 18.59/3.35 % (678357)------------------------------
% 18.59/3.35 % (678357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678357)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678357)Termination reason: Instruction limit
% 18.59/3.35 % (678357)Termination phase: Saturation
% 18.59/3.35 % (678357)Time elapsed: 0.104 s
% 18.59/3.35 % (678357)Peak memory usage: 91 MB
% 18.59/3.35 % (678357)Instructions burned: 191 (million)
% 18.59/3.35 % (678358)Instruction limit reached!
% 18.59/3.35 % (678358)------------------------------
% 18.59/3.35 % (678358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678358)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678358)Termination reason: Instruction limit
% 18.59/3.35 % (678358)Termination phase: Saturation
% 18.59/3.35 % (678358)Time elapsed: 0.125 s
% 18.59/3.35 % (678358)Peak memory usage: 91 MB
% 18.59/3.35 % (678358)Instructions burned: 220 (million)
% 18.59/3.35 % (678359)Instruction limit reached!
% 18.59/3.35 % (678359)------------------------------
% 18.59/3.35 % (678359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678359)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678359)Termination reason: Instruction limit
% 18.59/3.35 % (678359)Termination phase: Saturation
% 18.59/3.35 % (678359)Time elapsed: 0.082 s
% 18.59/3.35 % (678359)Peak memory usage: 90 MB
% 18.59/3.35 % (678359)Instructions burned: 126 (million)
% 18.59/3.35 % (678364)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1173789366:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 18.59/3.35 % (678365)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2458394083:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 18.59/3.35 % (678364)Instruction limit reached!
% 18.59/3.35 % (678364)------------------------------
% 18.59/3.35 % (678364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678364)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678364)Termination reason: Instruction limit
% 18.59/3.35 % (678364)Termination phase: Saturation
% 18.59/3.35 % (678364)Time elapsed: 0.071 s
% 18.59/3.35 % (678364)Peak memory usage: 90 MB
% 18.59/3.35 % (678364)Instructions burned: 196 (million)
% 18.59/3.35 % (678367)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=707177067:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 18.59/3.35 % (678366)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1491929092:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.59/3.35 % (678367)Instruction limit reached!
% 18.59/3.35 % (678367)------------------------------
% 18.59/3.35 % (678367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678367)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678367)Termination reason: Instruction limit
% 18.59/3.35 % (678367)Termination phase: Saturation
% 18.59/3.35 % (678367)Time elapsed: 0.059 s
% 18.59/3.35 % (678367)Peak memory usage: 89 MB
% 18.59/3.35 % (678367)Instructions burned: 107 (million)
% 18.59/3.35 % (678365)Instruction limit reached!
% 18.59/3.35 % (678365)------------------------------
% 18.59/3.35 % (678365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678365)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678365)Termination reason: Instruction limit
% 18.59/3.35 % (678365)Termination phase: Saturation
% 18.59/3.35 % (678365)Time elapsed: 0.099 s
% 18.59/3.35 % (678365)Peak memory usage: 91 MB
% 18.59/3.35 % (678365)Instructions burned: 158 (million)
% 18.59/3.35 % (678370)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=764529259:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 18.59/3.35 % (678370)Instruction limit reached!
% 18.59/3.35 % (678370)------------------------------
% 18.59/3.35 % (678370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678370)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678370)Termination reason: Instruction limit
% 18.59/3.35 % (678370)Termination phase: Saturation
% 18.59/3.35 % (678370)Time elapsed: 0.035 s
% 18.59/3.35 % (678370)Peak memory usage: 90 MB
% 18.59/3.35 % (678370)Instructions burned: 110 (million)
% 18.59/3.35 % (678373)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2325659060:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 18.59/3.35 % (678374)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=631133257:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 18.59/3.35 % (678376)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3170432536:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 18.59/3.35 % (678376)Instruction limit reached!
% 18.59/3.35 % (678376)------------------------------
% 18.59/3.35 % (678376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678376)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678376)Termination reason: Instruction limit
% 18.59/3.35 % (678376)Termination phase: Saturation
% 18.59/3.35 % (678376)Time elapsed: 0.036 s
% 18.59/3.35 % (678376)Peak memory usage: 89 MB
% 18.59/3.35 % (678376)Instructions burned: 140 (million)
% 18.59/3.35 % (678373)Instruction limit reached!
% 18.59/3.35 % (678373)------------------------------
% 18.59/3.35 % (678373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678373)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678373)Termination reason: Instruction limit
% 18.59/3.35 % (678373)Termination phase: Saturation
% 18.59/3.35 % (678373)Time elapsed: 0.148 s
% 18.59/3.35 % (678373)Peak memory usage: 90 MB
% 18.59/3.35 % (678373)Instructions burned: 243 (million)
% 18.59/3.35 % (678380)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2717199523:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 18.59/3.35 % (678381)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3384705782:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 18.59/3.35 % (678380)Instruction limit reached!
% 18.59/3.35 % (678380)------------------------------
% 18.59/3.35 % (678380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678380)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678380)Termination reason: Instruction limit
% 18.59/3.35 % (678380)Termination phase: Saturation
% 18.59/3.35 % (678380)Time elapsed: 0.159 s
% 18.59/3.35 % (678380)Peak memory usage: 93 MB
% 18.59/3.35 % (678380)Instructions burned: 500 (million)
% 18.59/3.35 % (678381)Instruction limit reached!
% 18.59/3.35 % (678381)------------------------------
% 18.59/3.35 % (678381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678381)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678381)Termination reason: Instruction limit
% 18.59/3.35 % (678381)Termination phase: Saturation
% 18.59/3.35 % (678381)Time elapsed: 0.131 s
% 18.59/3.35 % (678381)Peak memory usage: 91 MB
% 18.59/3.35 % (678381)Instructions burned: 192 (million)
% 18.59/3.35 % (678384)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1518452958:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 18.59/3.35 % (678384)Instruction limit reached!
% 18.59/3.35 % (678384)------------------------------
% 18.59/3.35 % (678384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678384)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678384)Termination reason: Instruction limit
% 18.59/3.35 % (678384)Termination phase: Saturation
% 18.59/3.35 % (678384)Time elapsed: 0.088 s
% 18.59/3.35 % (678384)Peak memory usage: 92 MB
% 18.59/3.35 % (678384)Instructions burned: 268 (million)
% 18.59/3.35 % (678385)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4097365021:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 18.59/3.35 % (678385)Instruction limit reached!
% 18.59/3.35 % (678385)------------------------------
% 18.59/3.35 % (678385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678385)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678385)Termination reason: Instruction limit
% 18.59/3.35 % (678385)Termination phase: Saturation
% 18.59/3.35 % (678385)Time elapsed: 0.096 s
% 18.59/3.35 % (678385)Peak memory usage: 90 MB
% 18.59/3.35 % (678385)Instructions burned: 158 (million)
% 18.59/3.35 % (678387)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=320312811:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 18.59/3.35 % (678390)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3331414932:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 18.59/3.35 % (678390)Instruction limit reached!
% 18.59/3.35 % (678390)------------------------------
% 18.59/3.35 % (678390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678390)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678390)Termination reason: Instruction limit
% 18.59/3.35 % (678390)Termination phase: Saturation
% 18.59/3.35 % (678390)Time elapsed: 0.316 s
% 18.59/3.35 % (678390)Peak memory usage: 92 MB
% 18.59/3.35 % (678390)Instructions burned: 537 (million)
% 18.59/3.35 % (678392)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1489528199:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 18.59/3.35 % (678392)Instruction limit reached!
% 18.59/3.35 % (678392)------------------------------
% 18.59/3.35 % (678392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.59/3.35 % (678392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.59/3.35 % (678392)CaDiCaL version: 2.1.3
% 18.59/3.35 % (678392)Termination reason: Instruction limit
% 18.59/3.35 % (678392)Termination phase: Saturation
% 18.59/3.35 % (678392)Time elapsed: 0.109 s
% 18.59/3.35 % (678392)Peak memory usage: 90 MB
% 18.59/3.35 % (678392)Instructions burned: 181 (million)
% 18.59/3.35 % (678342)First to succeed.
% 18.59/3.35 % (678342)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-678337"
% 18.59/3.35 % (678394)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=1923709470:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 18.59/3.35 % (678342)Refutation found. Thanks to Tanya!
% 18.59/3.35 % SZS status Unsatisfiable for theBenchmark
% 18.59/3.35 % SZS output start Proof for theBenchmark
% See solution above
% 19.34/3.55 % (678342)------------------------------
% 19.34/3.55 % (678342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.34/3.55 % (678342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.34/3.55 % (678342)CaDiCaL version: 2.1.3
% 19.34/3.55 % (678342)Termination reason: Refutation
% 19.34/3.55 % (678342)Time elapsed: 2.201 s
% 19.34/3.55 % (678342)Peak memory usage: 152 MB
% 19.34/3.55 % (678342)Instructions burned: 3428 (million)
% 19.34/3.55 % (678342)------------------------------
% 19.34/3.55 % (678342)------------------------------
% 19.34/3.55 % (678337)Success in time 2.686 s
% 19.34/3.55 % Vampire exiting
%------------------------------------------------------------------------------