%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG378-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 : n018.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:54 AM UTC 2026
% Result : Unsatisfiable 18.34s 3.12s
% Output : Refutation 19.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 26
% Syntax : Number of formulae : 86 ( 62 unt; 7 def)
% Number of atoms : 118 ( 63 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 66 ( 34 ~; 32 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 12 con; 0-3 aty)
% Number of variables : 99 ( 99 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f42,axiom,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__add__eq__0__iff_1) ).
fof(f43,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(reorient_equations,[],[f42]) ).
fof(f130,axiom,
! [X2,X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Oplus__class_Oplus(X1,X2,X0),X0) = X2
| ~ class_OrderedGroup_Ogroup__add(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_minus__add__cancel_0) ).
fof(f333,axiom,
! [X2,X0,X1] :
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X0) = c_HOL_Ominus__class_Ominus(X2,X1,X0)
| ~ class_OrderedGroup_Oab__group__add(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_minus__diff__eq_0) ).
fof(f540,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__diff__def_0) ).
fof(f541,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),
inference(reorient_equations,[],[f540]) ).
fof(f542,axiom,
! [X0,X1] : c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_abs__minus__add__cancel_0) ).
fof(f543,axiom,
! [X0,X1] : c_RealVector_Odist__class_Odist(X0,X1,tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dist__real__def_0) ).
fof(f563,axiom,
! [X2,X3,X0,X1,X4] :
( c_lessequals(X1,c_HOL_Oplus__class_Oplus(X2,X3,X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add(X0)
| ~ c_lessequals(X4,X3,X0)
| ~ c_lessequals(X1,c_HOL_Oplus__class_Oplus(X2,X4,X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_le__add__right__mono_0) ).
fof(f570,axiom,
! [X2,X0,X1] :
( c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(X1,X2,X0),X0),c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(X1,X0),c_HOL_Oabs__class_Oabs(X2,X0),X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_abs__triangle__ineq4_0) ).
fof(f574,axiom,
! [X2,X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,X2,X0) = c_HOL_Oplus__class_Oplus(X2,X1,X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I24_J_0) ).
fof(f604,axiom,
! [X2,X0,X1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X2,X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__add__cancel_0) ).
fof(f614,axiom,
! [X2,X3,X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Oplus__class_Oplus(X2,X3,X0),X0) = c_HOL_Oplus__class_Oplus(X2,c_HOL_Oplus__class_Oplus(X1,X3,X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I22_J_0) ).
fof(f622,axiom,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X1,X2,X0),X2,X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_add__diff__cancel_0) ).
fof(f623,negated_conjecture,
c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(v_a,v_b,tc_RealDef_Oreal),tc_RealDef_Oreal),v_c,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f624,negated_conjecture,
~ c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(v_b,v_m,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(v_a,v_m,tc_RealDef_Oreal),tc_RealDef_Oreal),v_c,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f631,axiom,
class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__group__add__abs) ).
fof(f637,axiom,
class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__group__add) ).
fof(f647,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1) ).
fof(f659,axiom,
class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Oab__group__add) ).
fof(f667,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add) ).
fof(f676,definition,
sF0 = c_HOL_Ominus__class_Ominus(v_a,v_b,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f677,plain,
c_HOL_Ominus__class_Ominus(v_a,v_b,tc_RealDef_Oreal) = sF0,
inference(reorient_equations,[],[f676]) ).
fof(f678,definition,
sF1 = c_HOL_Oabs__class_Oabs(sF0,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f679,plain,
c_HOL_Oabs__class_Oabs(sF0,tc_RealDef_Oreal) = sF1,
inference(reorient_equations,[],[f678]) ).
fof(f680,plain,
c_lessequals(sF1,v_c,tc_RealDef_Oreal),
inference(definition_folding,[],[f623,f679,f677]) ).
fof(f681,definition,
sF2 = c_HOL_Ominus__class_Ominus(v_b,v_m,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f682,plain,
c_HOL_Ominus__class_Ominus(v_b,v_m,tc_RealDef_Oreal) = sF2,
inference(reorient_equations,[],[f681]) ).
fof(f683,definition,
sF3 = c_HOL_Oabs__class_Oabs(sF2,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f684,plain,
c_HOL_Oabs__class_Oabs(sF2,tc_RealDef_Oreal) = sF3,
inference(reorient_equations,[],[f683]) ).
fof(f685,definition,
sF4 = c_HOL_Ominus__class_Ominus(v_a,v_m,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f686,plain,
c_HOL_Ominus__class_Ominus(v_a,v_m,tc_RealDef_Oreal) = sF4,
inference(reorient_equations,[],[f685]) ).
fof(f687,definition,
sF5 = c_HOL_Oabs__class_Oabs(sF4,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f688,plain,
c_HOL_Oabs__class_Oabs(sF4,tc_RealDef_Oreal) = sF5,
inference(reorient_equations,[],[f687]) ).
fof(f689,definition,
sF6 = c_HOL_Oplus__class_Oplus(sF5,v_c,tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f690,plain,
c_HOL_Oplus__class_Oplus(sF5,v_c,tc_RealDef_Oreal) = sF6,
inference(reorient_equations,[],[f689]) ).
fof(f691,plain,
~ c_lessequals(sF3,sF6,tc_RealDef_Oreal),
inference(definition_folding,[],[f624,f690,f688,f686,f684,f682]) ).
fof(f695,plain,
! [X0,X1] : c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(backward_demodulation,[],[f542,f541]) ).
fof(f700,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(X0,X0,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f43,f541]) ).
fof(f702,plain,
! [X0,X1] : c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(X1,c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_RealVector_Odist__class_Odist(X0,X1,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f695,f543]) ).
fof(f704,plain,
! [X0,X1] : c_RealVector_Odist__class_Odist(X0,X1,tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f702,f541]) ).
fof(f845,plain,
( v_b = c_HOL_Oplus__class_Oplus(sF2,v_m,tc_RealDef_Oreal)
| ~ class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f604,f682]) ).
fof(f854,plain,
v_b = c_HOL_Oplus__class_Oplus(sF2,v_m,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f845,f667]) ).
fof(f859,plain,
! [X0,X1] :
( c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_RealVector_Odist__class_Odist(X1,c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f704,f622]) ).
fof(f864,plain,
! [X0,X1] : c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_RealVector_Odist__class_Odist(X1,c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f859,f667]) ).
fof(f1099,plain,
! [X0] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0
| ~ class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f604,f700]) ).
fof(f1106,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(forward_subsumption_resolution,[],[f1099,f667]) ).
fof(f1217,plain,
! [X0] :
( c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(sF0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(sF1,c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(superposition,[],[f570,f679]) ).
fof(f1232,plain,
! [X0] : c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(sF0,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(sF1,c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1217,f631]) ).
fof(f1252,plain,
! [X0] : c_lessequals(c_RealVector_Odist__class_Odist(sF0,X0,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(sF1,c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f1232,f543]) ).
fof(f1352,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) ),
inference(superposition,[],[f541,f574]) ).
fof(f1377,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f1352,f647]) ).
fof(f2039,plain,
! [X0,X1] :
( c_lessequals(X0,sF6,tc_RealDef_Oreal)
| ~ class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal)
| ~ c_lessequals(X1,v_c,tc_RealDef_Oreal)
| ~ c_lessequals(X0,c_HOL_Oplus__class_Oplus(sF5,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) ),
inference(superposition,[],[f563,f690]) ).
fof(f2043,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_HOL_Oplus__class_Oplus(sF5,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(X1,v_c,tc_RealDef_Oreal)
| c_lessequals(X0,sF6,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f2039,f637]) ).
fof(f2066,plain,
! [X0,X1] :
( ~ c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,sF5,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(X0,v_c,tc_RealDef_Oreal)
| c_lessequals(X1,sF6,tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) ),
inference(superposition,[],[f2043,f574]) ).
fof(f2067,plain,
! [X0,X1] :
( ~ c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,sF5,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_lessequals(X0,v_c,tc_RealDef_Oreal)
| c_lessequals(X1,sF6,tc_RealDef_Oreal) ),
inference(forward_subsumption_resolution,[],[f2066,f647]) ).
fof(f2475,plain,
( v_m = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(sF2,tc_RealDef_Oreal),v_b,tc_RealDef_Oreal)
| ~ class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f130,f854]) ).
fof(f2510,plain,
v_m = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(sF2,tc_RealDef_Oreal),v_b,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f2475,f667]) ).
fof(f2518,plain,
v_m = c_HOL_Ominus__class_Ominus(v_b,sF2,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f2510,f1377]) ).
fof(f2565,plain,
! [X0] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0
| ~ class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f130,f1106]) ).
fof(f2583,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = X0,
inference(forward_subsumption_resolution,[],[f2565,f667]) ).
fof(f2614,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[],[f2583,f1377]) ).
fof(f2640,plain,
! [X0,X1] :
( c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal) = c_RealVector_Odist__class_Odist(X0,c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) ),
inference(superposition,[],[f864,f574]) ).
fof(f2643,plain,
! [X0,X1] : c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal) = c_RealVector_Odist__class_Odist(X0,c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f2640,f647]) ).
fof(f3150,plain,
! [X2,X0,X1] :
( c_HOL_Ominus__class_Ominus(X2,c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X2,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal) ),
inference(superposition,[],[f541,f333]) ).
fof(f3155,plain,
! [X2,X0,X1] : c_HOL_Ominus__class_Ominus(X2,c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X2,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f3150,f659]) ).
fof(f3442,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f3155,f700]) ).
fof(f3514,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[],[f3442,f2614]) ).
fof(f4001,plain,
c_lessequals(c_RealVector_Odist__class_Odist(sF0,sF4,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(sF1,sF5,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1252,f688]) ).
fof(f4024,plain,
( ~ c_lessequals(sF1,v_c,tc_RealDef_Oreal)
| c_lessequals(c_RealVector_Odist__class_Odist(sF0,sF4,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal) ),
inference(resolution,[],[f4001,f2067]) ).
fof(f4035,plain,
c_lessequals(c_RealVector_Odist__class_Odist(sF0,sF4,tc_RealDef_Oreal),sF6,tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f4024,f680]) ).
fof(f17456,plain,
! [X2,X0,X1] :
( c_HOL_Oplus__class_Oplus(X2,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X2,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) ),
inference(superposition,[],[f614,f541]) ).
fof(f17458,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) ),
inference(superposition,[],[f614,f3514]) ).
fof(f17710,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f17458,f647]) ).
fof(f17712,plain,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(X2,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X2,c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_subsumption_resolution,[],[f17456,f647]) ).
fof(f17729,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17710,f3514]) ).
fof(f17731,plain,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(X2,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17712,f541]) ).
fof(f17738,plain,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(X2,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f17731,f3155]) ).
fof(f17747,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,sF0,tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(v_a,c_HOL_Ominus__class_Ominus(v_b,X0,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f17738,f677]) ).
fof(f19937,plain,
c_HOL_Ominus__class_Ominus(v_a,v_m,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(sF2,sF0,tc_RealDef_Oreal),
inference(superposition,[],[f17747,f2518]) ).
fof(f19970,plain,
c_HOL_Ominus__class_Ominus(v_a,v_m,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(sF0,sF2,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f19937,f17729]) ).
fof(f19979,plain,
sF4 = c_HOL_Oplus__class_Oplus(sF0,sF2,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f19970,f686]) ).
fof(f20003,plain,
c_HOL_Oabs__class_Oabs(sF2,tc_RealDef_Oreal) = c_RealVector_Odist__class_Odist(sF0,sF4,tc_RealDef_Oreal),
inference(superposition,[],[f2643,f19979]) ).
fof(f20119,plain,
sF3 = c_RealVector_Odist__class_Odist(sF0,sF4,tc_RealDef_Oreal),
inference(forward_demodulation,[],[f20003,f684]) ).
fof(f20125,plain,
c_lessequals(sF3,sF6,tc_RealDef_Oreal),
inference(backward_demodulation,[],[f4035,f20119]) ).
fof(f20134,plain,
$false,
inference(forward_subsumption_resolution,[],[f20125,f691]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG378-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n018.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 20:16:25 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 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
% 9.40/1.99 % (3722427)Input is clausal, will run a generic CNF schedule.
% 9.40/1.99 % (3722449)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4173558865:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.40/1.99 % (3722445)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2275957208:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.40/1.99 % (3722447)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2496908411:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.40/1.99 % (3722451)dis-21_1_sil=8000:lcm=predicate:random_seed=2732904013: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)
% 9.40/1.99 % (3722444)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=2326157857:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.40/1.99 % (3722448)lrs+10_1_sil=8000:sp=occurrence:random_seed=528209885:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.40/1.99 % (3722450)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3861228148:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.40/1.99 % (3722451)Instruction limit reached!
% 9.40/1.99 % (3722451)------------------------------
% 9.40/1.99 % (3722451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.40/1.99 % (3722451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.40/1.99 % (3722451)CaDiCaL version: 2.1.3
% 9.40/1.99 % (3722451)Termination reason: Instruction limit
% 9.40/1.99 % (3722451)Termination phase: Saturation
% 9.40/1.99 % (3722451)Time elapsed: 0.066 s
% 9.40/1.99 % (3722451)Peak memory usage: 89 MB
% 9.40/1.99 % (3722451)Instructions burned: 118 (million)
% 9.40/1.99 % (3722448)Instruction limit reached!
% 9.40/1.99 % (3722448)------------------------------
% 9.40/1.99 % (3722448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.40/1.99 % (3722448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.40/1.99 % (3722448)CaDiCaL version: 2.1.3
% 9.40/1.99 % (3722448)Termination reason: Instruction limit
% 9.40/1.99 % (3722448)Termination phase: Saturation
% 9.40/1.99 % (3722448)Time elapsed: 0.073 s
% 9.40/1.99 % (3722448)Peak memory usage: 89 MB
% 9.40/1.99 % (3722448)Instructions burned: 108 (million)
% 9.40/1.99 % (3722449)Instruction limit reached!
% 9.40/1.99 % (3722449)------------------------------
% 9.40/1.99 % (3722449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.40/1.99 % (3722449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.40/1.99 % (3722449)CaDiCaL version: 2.1.3
% 9.40/1.99 % (3722449)Termination reason: Instruction limit
% 9.40/1.99 % (3722449)Termination phase: Saturation
% 9.40/1.99 % (3722449)Time elapsed: 0.079 s
% 9.40/1.99 % (3722449)Peak memory usage: 89 MB
% 9.40/1.99 % (3722449)Instructions burned: 114 (million)
% 9.40/1.99 % (3722450)Instruction limit reached!
% 9.40/1.99 % (3722450)------------------------------
% 9.40/1.99 % (3722450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.40/1.99 % (3722450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.40/1.99 % (3722450)CaDiCaL version: 2.1.3
% 9.40/1.99 % (3722450)Termination reason: Instruction limit
% 9.40/1.99 % (3722450)Termination phase: Saturation
% 9.40/1.99 % (3722450)Time elapsed: 0.078 s
% 9.40/1.99 % (3722450)Peak memory usage: 90 MB
% 9.40/1.99 % (3722450)Instructions burned: 180 (million)
% 9.40/1.99 % (3722523)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=2770653073:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.40/1.99 % (3722531)lrs+10_64_to=lpo:sil=8000:random_seed=4152081962:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 9.40/1.99 % (3722530)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1750839036:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.40/1.99 % (3722523)Instruction limit reached!
% 9.40/1.99 % (3722523)------------------------------
% 9.40/1.99 % (3722523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.40/1.99 % (3722523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.11 % (3722523)CaDiCaL version: 2.1.3
% 18.34/3.11 % (3722523)Termination reason: Instruction limit
% 18.34/3.11 % (3722523)Termination phase: Saturation
% 18.34/3.11 % (3722523)Time elapsed: 0.053 s
% 18.34/3.11 % (3722523)Peak memory usage: 90 MB
% 18.34/3.11 % (3722523)Instructions burned: 145 (million)
% 18.34/3.11 % (3722527)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2535300748: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.34/3.11 % (3722531)Instruction limit reached!
% 18.34/3.11 % (3722531)------------------------------
% 18.34/3.11 % (3722531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.11 % (3722531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.11 % (3722531)CaDiCaL version: 2.1.3
% 18.34/3.11 % (3722531)Termination reason: Instruction limit
% 18.34/3.11 % (3722531)Termination phase: Saturation
% 18.34/3.11 % (3722531)Time elapsed: 0.077 s
% 18.34/3.11 % (3722531)Peak memory usage: 89 MB
% 18.34/3.11 % (3722531)Instructions burned: 126 (million)
% 18.34/3.11 % (3722530)Instruction limit reached!
% 18.34/3.11 % (3722530)------------------------------
% 18.34/3.11 % (3722530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.11 % (3722530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.11 % (3722530)CaDiCaL version: 2.1.3
% 18.34/3.11 % (3722530)Termination reason: Instruction limit
% 18.34/3.11 % (3722530)Termination phase: Saturation
% 18.34/3.11 % (3722530)Time elapsed: 0.133 s
% 18.34/3.11 % (3722530)Peak memory usage: 90 MB
% 18.34/3.11 % (3722530)Instructions burned: 220 (million)
% 18.34/3.11 % (3722527)Instruction limit reached!
% 18.34/3.11 % (3722527)------------------------------
% 18.34/3.11 % (3722527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.11 % (3722527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.11 % (3722527)CaDiCaL version: 2.1.3
% 18.34/3.11 % (3722527)Termination reason: Instruction limit
% 18.34/3.11 % (3722527)Termination phase: Saturation
% 18.34/3.11 % (3722527)Time elapsed: 0.129 s
% 18.34/3.11 % (3722527)Peak memory usage: 90 MB
% 18.34/3.11 % (3722527)Instructions burned: 189 (million)
% 18.34/3.11 % (3722562)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2303533184:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 18.34/3.11 % (3722585)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1066206067:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 18.34/3.11 % (3722562)Instruction limit reached!
% 18.34/3.11 % (3722562)------------------------------
% 18.34/3.11 % (3722562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.11 % (3722562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.11 % (3722562)CaDiCaL version: 2.1.3
% 18.34/3.11 % (3722562)Termination reason: Instruction limit
% 18.34/3.11 % (3722562)Termination phase: Saturation
% 18.34/3.11 % (3722562)Time elapsed: 0.082 s
% 18.34/3.11 % (3722562)Peak memory usage: 88 MB
% 18.34/3.11 % (3722562)Instructions burned: 194 (million)
% 18.34/3.11 % (3722600)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=85725300:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 18.34/3.11 % (3722603)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=138699345:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 18.34/3.11 % (3722585)Instruction limit reached!
% 18.34/3.11 % (3722585)------------------------------
% 18.34/3.11 % (3722585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.11 % (3722585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.11 % (3722585)CaDiCaL version: 2.1.3
% 18.34/3.11 % (3722585)Termination reason: Instruction limit
% 18.34/3.11 % (3722585)Termination phase: Saturation
% 18.34/3.11 % (3722585)Time elapsed: 0.149 s
% 18.34/3.11 % (3722585)Peak memory usage: 90 MB
% 18.34/3.11 % (3722585)Instructions burned: 158 (million)
% 18.34/3.11 % (3722612)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3904449843:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 18.34/3.11 % (3722603)Instruction limit reached!
% 18.34/3.11 % (3722603)------------------------------
% 18.34/3.11 % (3722603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722603)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722603)Termination reason: Instruction limit
% 18.34/3.12 % (3722603)Termination phase: Saturation
% 18.34/3.12 % (3722603)Time elapsed: 0.063 s
% 18.34/3.12 % (3722603)Peak memory usage: 89 MB
% 18.34/3.12 % (3722603)Instructions burned: 107 (million)
% 18.34/3.12 % (3722612)Instruction limit reached!
% 18.34/3.12 % (3722612)------------------------------
% 18.34/3.12 % (3722612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722612)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722612)Termination reason: Instruction limit
% 18.34/3.12 % (3722612)Termination phase: Saturation
% 18.34/3.12 % (3722612)Time elapsed: 0.035 s
% 18.34/3.12 % (3722612)Peak memory usage: 89 MB
% 18.34/3.12 % (3722612)Instructions burned: 107 (million)
% 18.34/3.12 % (3722620)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=655170986:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 18.34/3.12 % (3722622)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3027924976:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 18.34/3.12 % (3722623)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1619856240:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 18.34/3.12 % (3722623)Instruction limit reached!
% 18.34/3.12 % (3722623)------------------------------
% 18.34/3.12 % (3722623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722623)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722623)Termination reason: Instruction limit
% 18.34/3.12 % (3722623)Termination phase: Saturation
% 18.34/3.12 % (3722623)Time elapsed: 0.040 s
% 18.34/3.12 % (3722623)Peak memory usage: 89 MB
% 18.34/3.12 % (3722623)Instructions burned: 135 (million)
% 18.34/3.12 % (3722620)Instruction limit reached!
% 18.34/3.12 % (3722620)------------------------------
% 18.34/3.12 % (3722620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722620)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722620)Termination reason: Instruction limit
% 18.34/3.12 % (3722620)Termination phase: Saturation
% 18.34/3.12 % (3722620)Time elapsed: 0.148 s
% 18.34/3.12 % (3722620)Peak memory usage: 90 MB
% 18.34/3.12 % (3722620)Instructions burned: 242 (million)
% 18.34/3.12 % (3722655)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=955170544:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 18.34/3.12 % (3722695)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3928912492:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 18.34/3.12 % (3722655)Instruction limit reached!
% 18.34/3.12 % (3722655)------------------------------
% 18.34/3.12 % (3722655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722655)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722655)Termination reason: Instruction limit
% 18.34/3.12 % (3722655)Termination phase: Saturation
% 18.34/3.12 % (3722655)Time elapsed: 0.173 s
% 18.34/3.12 % (3722655)Peak memory usage: 93 MB
% 18.34/3.12 % (3722655)Instructions burned: 502 (million)
% 18.34/3.12 % (3722695)Instruction limit reached!
% 18.34/3.12 % (3722695)------------------------------
% 18.34/3.12 % (3722695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722695)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722695)Termination reason: Instruction limit
% 18.34/3.12 % (3722695)Termination phase: Saturation
% 18.34/3.12 % (3722695)Time elapsed: 0.128 s
% 18.34/3.12 % (3722695)Peak memory usage: 90 MB
% 18.34/3.12 % (3722695)Instructions burned: 191 (million)
% 18.34/3.12 % (3722736)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1423190822:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 18.34/3.12 % (3722736)Instruction limit reached!
% 18.34/3.12 % (3722736)------------------------------
% 18.34/3.12 % (3722736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722736)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722736)Termination reason: Instruction limit
% 18.34/3.12 % (3722736)Termination phase: Saturation
% 18.34/3.12 % (3722736)Time elapsed: 0.067 s
% 18.34/3.12 % (3722736)Peak memory usage: 90 MB
% 18.34/3.12 % (3722736)Instructions burned: 265 (million)
% 18.34/3.12 % (3722737)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=39900589:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 18.34/3.12 % (3722771)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=1809392046:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 18.34/3.12 % (3722737)Instruction limit reached!
% 18.34/3.12 % (3722737)------------------------------
% 18.34/3.12 % (3722737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722737)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722737)Termination reason: Instruction limit
% 18.34/3.12 % (3722737)Termination phase: Saturation
% 18.34/3.12 % (3722737)Time elapsed: 0.103 s
% 18.34/3.12 % (3722737)Peak memory usage: 90 MB
% 18.34/3.12 % (3722737)Instructions burned: 157 (million)
% 18.34/3.12 % (3722789)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1497213422:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 18.34/3.12 % (3722789)Instruction limit reached!
% 18.34/3.12 % (3722789)------------------------------
% 18.34/3.12 % (3722789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722789)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722789)Termination reason: Instruction limit
% 18.34/3.12 % (3722789)Termination phase: Saturation
% 18.34/3.12 % (3722789)Time elapsed: 0.300 s
% 18.34/3.12 % (3722789)Peak memory usage: 94 MB
% 18.34/3.12 % (3722789)Instructions burned: 538 (million)
% 18.34/3.12 % (3722791)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2674320834:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 18.34/3.12 % (3722447)First to succeed.
% 18.34/3.12 % (3722447)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3722427"
% 18.34/3.12 % (3722791)Instruction limit reached!
% 18.34/3.12 % (3722791)------------------------------
% 18.34/3.12 % (3722791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.12 % (3722791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.12 % (3722791)CaDiCaL version: 2.1.3
% 18.34/3.12 % (3722791)Termination reason: Instruction limit
% 18.34/3.12 % (3722791)Termination phase: Saturation
% 18.34/3.12 % (3722791)Time elapsed: 0.107 s
% 18.34/3.12 % (3722791)Peak memory usage: 88 MB
% 18.34/3.12 % (3722791)Instructions burned: 181 (million)
% 18.34/3.12 % (3722793)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=1499827644:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 18.34/3.12 % (3722444)Also succeeded, but the first one will report.
% 18.34/3.12 % (3722447)Refutation found. Thanks to Tanya!
% 18.34/3.12 % SZS status Unsatisfiable for theBenchmark
% 18.34/3.12 % SZS output start Proof for theBenchmark
% See solution above
% 19.03/3.22 % (3722447)------------------------------
% 19.03/3.22 % (3722447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.03/3.22 % (3722447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.03/3.22 % (3722447)CaDiCaL version: 2.1.3
% 19.03/3.22 % (3722447)Termination reason: Refutation
% 19.03/3.22 % (3722447)Time elapsed: 2.225 s
% 19.03/3.22 % (3722447)Peak memory usage: 147 MB
% 19.03/3.22 % (3722447)Instructions burned: 3268 (million)
% 19.03/3.22 % (3722447)------------------------------
% 19.03/3.22 % (3722447)------------------------------
% 19.03/3.22 % (3722427)Success in time 2.652 s
% 19.03/3.22 % Vampire exiting
%------------------------------------------------------------------------------