%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG337-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:30:21 AM UTC 2026
% Result : Unsatisfiable 93.43s 31.02s
% Output : Refutation 93.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 21
% Syntax : Number of formulae : 64 ( 58 unt; 0 def)
% Number of atoms : 70 ( 59 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 25 ( 19 ~; 6 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 66 ( 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f278,axiom,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(X0,X1,tc_Int_Oint),X2,tc_Int_Oint) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_Int_Oint),tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zadd__assoc_0) ).
fof(f279,axiom,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_Int_Oint),tc_Int_Oint) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_Int_Oint),tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zadd__left__commute_0) ).
fof(f1010,axiom,
! [X0] : c_HOL_Oplus__class_Oplus(c_Int_OPls,X0,tc_Int_Oint) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__Pls_0) ).
fof(f1170,axiom,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_Int_OBit1(X0),c_Int_OBit0(X1),tc_Int_Oint) = c_Int_OBit1(c_HOL_Oplus__class_Oplus(X0,X1,tc_Int_Oint)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__Bit1__Bit0_0) ).
fof(f1171,plain,
! [X0,X1] : c_Int_OBit1(c_HOL_Oplus__class_Oplus(X0,X1,tc_Int_Oint)) = c_HOL_Oplus__class_Oplus(c_Int_OBit1(X0),c_Int_OBit0(X1),tc_Int_Oint),
inference(reorient_equations,[],[f1170]) ).
fof(f1195,axiom,
! [X0] : c_Int_OBit0(X0) = c_HOL_Oplus__class_Oplus(X0,X0,tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Bit0__def_0) ).
fof(f1314,axiom,
! [X0] : c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sqrt__abs_0) ).
fof(f1315,plain,
! [X0] : c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal)),
inference(reorient_equations,[],[f1314]) ).
fof(f1346,axiom,
! [X0] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sqrt__abs2_0) ).
fof(f1347,plain,
! [X0] : c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)),
inference(reorient_equations,[],[f1346]) ).
fof(f1443,axiom,
! [X0] :
( ~ class_Int_Onumber__ring(X0)
| c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(X0),c_HOL_Oone__class_Oone(X0),X0) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_one__add__one__is__two_0) ).
fof(f1446,axiom,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sq4_H_I1_J_0) ).
fof(f1462,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| c_HOL_Oplus__class_Oplus(X1,X2,X0) = c_HOL_Oplus__class_Oplus(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_comm__monoid__add_Omult__commute_0) ).
fof(f1496,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__average__minus__first_0) ).
fof(f1499,axiom,
! [X0,X1] : c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(X0,X1,tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(X1),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sqrt__divide_0) ).
fof(f1531,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X2,X0),X3,X0) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X1,X3,X0),c_HOL_Oinverse__class_Odivide(X2,X3,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__divide__distrib_0) ).
fof(f1540,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,X0),X2,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__add__cancel_0) ).
fof(f1578,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ogroup__add(X0)
| c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X1,X2,X0),X2,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__diff__cancel_0) ).
fof(f1581,axiom,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f1582,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(reorient_equations,[],[f1581]) ).
fof(f1585,negated_conjecture,
c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal) != v_x____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1586,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),
inference(reorient_equations,[],[f1585]) ).
fof(f1712,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Ocomm__monoid__add) ).
fof(f1729,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add) ).
fof(f1733,axiom,
class_Ring__and__Field_Ofield(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ofield) ).
fof(f1741,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Int_Onumber__ring) ).
fof(f1829,plain,
! [X0,X1] : c_Int_OBit1(c_HOL_Oplus__class_Oplus(X0,X1,tc_Int_Oint)) = c_HOL_Oplus__class_Oplus(c_Int_OBit1(X0),c_HOL_Oplus__class_Oplus(X1,X1,tc_Int_Oint),tc_Int_Oint),
inference(definition_unfolding,[],[f1171,f1195]) ).
fof(f1878,plain,
! [X0] : c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_nat),tc_RealDef_Oreal)),
inference(definition_unfolding,[],[f1315,f1195]) ).
fof(f1914,plain,
! [X0] :
( ~ class_Int_Onumber__ring(X0)
| c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(X0),c_HOL_Oone__class_Oone(X0),X0) = c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),X0) ),
inference(definition_unfolding,[],[f1443,f1195]) ).
fof(f1916,plain,
c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_nat),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(definition_unfolding,[],[f1446,f1195,f1195,f1195,f1195]) ).
fof(f1929,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X1,X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(definition_unfolding,[],[f1496,f1195,f1195]) ).
fof(f1937,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(definition_unfolding,[],[f1582,f1195,f1195,f1195]) ).
fof(f1939,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),
inference(definition_unfolding,[],[f1586,f1195,f1195,f1195,f1195]) ).
fof(f2964,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),
inference(resolution,[],[f1462,f1712]) ).
fof(f3000,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0,
inference(resolution,[],[f1540,f1729]) ).
fof(f3001,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(forward_demodulation,[],[f3000,f2964]) ).
fof(f3017,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal) = X0,
inference(resolution,[],[f1578,f1729]) ).
fof(f3562,plain,
! [X0,X1] : c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal),X1,tc_RealDef_Oreal)) = c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_NthRoot_Osqrt(X1),tc_RealDef_Oreal),
inference(superposition,[],[f1499,f1347]) ).
fof(f3947,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(superposition,[],[f3017,f3001]) ).
fof(f6297,plain,
! [X2,X0,X1] : c_HOL_Oplus__class_Oplus(X2,c_Int_OBit1(c_HOL_Oplus__class_Oplus(X0,X1,tc_Int_Oint)),tc_Int_Oint) = c_HOL_Oplus__class_Oplus(c_Int_OBit1(X0),c_HOL_Oplus__class_Oplus(X2,c_HOL_Oplus__class_Oplus(X1,X1,tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),
inference(superposition,[],[f279,f1829]) ).
fof(f8074,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_NthRoot_Osqrt(X1),tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X0,c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_nat),tc_RealDef_Oreal),X1,tc_RealDef_Oreal)),
inference(superposition,[],[f1499,f1878]) ).
fof(f9461,plain,
c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[],[f1914,f1741]) ).
fof(f14271,plain,
! [X2,X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(X0,X2,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(resolution,[],[f1531,f1733]) ).
fof(f24591,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(superposition,[],[f3947,f1929]) ).
fof(f24636,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(forward_demodulation,[],[f24591,f14271]) ).
fof(f24672,plain,
! [X0,X1] : c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X1,X0,tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(forward_demodulation,[],[f24636,f9461]) ).
fof(f42807,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_nat),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(superposition,[],[f1916,f278]) ).
fof(f43027,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f42807,f8074]) ).
fof(f43138,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_HOL_Oplus__class_Oplus(c_Int_OPls,c_Int_OBit1(c_Int_OPls),tc_Int_Oint)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f43027,f6297]) ).
fof(f43239,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f43138,f1010]) ).
fof(f43337,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f43239,f2964]) ).
fof(f43424,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f43337,f2964]) ).
fof(f43507,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f43424,f9461]) ).
fof(f45589,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(superposition,[],[f1939,f1937]) ).
fof(f45803,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f45589,f9461]) ).
fof(f45913,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f45803,f2964]) ).
fof(f46022,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f45913,f3562]) ).
fof(f46130,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OPls),tc_Int_Oint),tc_Int_Oint),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f46022,f278]) ).
fof(f46237,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_HOL_Oplus__class_Oplus(c_Int_OPls,c_Int_OBit1(c_Int_OPls),tc_Int_Oint)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f46130,f6297]) ).
fof(f46344,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f46237,f1010]) ).
fof(f46419,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(c_HOL_Oplus__class_Oplus(c_Int_OBit1(c_Int_OPls),c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f46344,f2964]) ).
fof(f46434,plain,
v_x____ != c_HOL_Ominus__class_Ominus(c_HOL_Oinverse__class_Odivide(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f46419,f43507]) ).
fof(f46441,plain,
v_x____ != c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(v_x____,c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_RealDef_Oreal),c_HOL_Ominus__class_Ominus(c_NthRoot_Osqrt(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(v_y____,v_y____,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v_x____,v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal)),v_x____,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(forward_demodulation,[],[f46434,f14271]) ).
fof(f46444,plain,
$false,
inference(forward_subsumption_resolution,[],[f46441,f24672]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG337-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n004.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:06:37 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.22/2.38 % (711142)Will run a generic schedule for satisfiability detection.
% 14.22/2.38 % (711147)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=986852062_2999 on theBenchmark for (2999ds/0Mi)
% 14.22/2.38 % (711148)% WARNING: option uhcvi not known.
% 14.22/2.38 % (711148)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4049715931:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.22/2.38 % (711149)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1130962820:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.22/2.38 % (711150)dis+10_1_sil=32000:sp=arity:random_seed=2946642657:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.22/2.38 % (711151)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3871202059:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.22/2.38 % (711152)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2636575313:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.22/2.38 % (711153)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2243631471:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.22/2.38 % (711150)Instruction limit reached!
% 14.22/2.38 % (711150)------------------------------
% 14.22/2.38 % (711150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.22/2.38 % (711150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.22/2.38 % (711150)CaDiCaL version: 2.1.3
% 14.22/2.38 % (711150)Termination reason: Instruction limit
% 14.22/2.38 % (711150)Termination phase: Saturation
% 14.22/2.38 % (711150)Time elapsed: 0.063 s
% 14.22/2.38 % (711150)Peak memory usage: 14 MB
% 14.22/2.38 % (711150)Instructions burned: 103 (million)
% 14.22/2.38 % (711151)Instruction limit reached!
% 14.22/2.38 % (711151)------------------------------
% 14.22/2.38 % (711151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.22/2.38 % (711151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.22/2.38 % (711151)CaDiCaL version: 2.1.3
% 14.22/2.38 % (711151)Termination reason: Instruction limit
% 14.22/2.38 % (711151)Termination phase: Saturation
% 14.22/2.38 % (711151)Time elapsed: 0.065 s
% 14.22/2.38 % (711151)Peak memory usage: 14 MB
% 14.22/2.38 % (711151)Instructions burned: 117 (million)
% 14.22/2.38 % (711152)Instruction limit reached!
% 14.22/2.38 % (711152)------------------------------
% 14.22/2.38 % (711152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.22/2.38 % (711152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.22/2.38 % (711152)CaDiCaL version: 2.1.3
% 14.22/2.38 % (711152)Termination reason: Instruction limit
% 14.22/2.38 % (711152)Termination phase: Saturation
% 14.22/2.38 % (711152)Time elapsed: 0.076 s
% 14.22/2.38 % (711152)Peak memory usage: 14 MB
% 14.22/2.38 % (711152)Instructions burned: 131 (million)
% 14.22/2.38 % (711161)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3915431196:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.22/2.38 % (711162)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1140541974:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.22/2.38 % (711163)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3783265983:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.22/2.38 % (711153)Instruction limit reached!
% 14.22/2.38 % (711153)------------------------------
% 14.22/2.38 % (711153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.22/2.38 % (711153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.22/2.38 % (711153)CaDiCaL version: 2.1.3
% 14.22/2.38 % (711153)Termination reason: Instruction limit
% 14.22/2.38 % (711153)Termination phase: Saturation
% 14.22/2.38 % (711153)Time elapsed: 0.106 s
% 14.22/2.38 % (711153)Peak memory usage: 15 MB
% 14.22/2.38 % (711153)Instructions burned: 160 (million)
% 14.22/2.38 % (711167)ott-21_1_sil=16000:fs=off:random_seed=152072055:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 14.22/2.38 % (711162)Instruction limit reached!
% 14.22/2.38 % (711162)------------------------------
% 14.22/2.38 % (711162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.22/2.38 % (711162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.22/2.38 % (711162)CaDiCaL version: 2.1.3
% 14.22/2.38 % (711162)Termination reason: Instruction limit
% 43.93/6.56 % (711162)Termination phase: Saturation
% 43.93/6.56 % (711162)Time elapsed: 0.076 s
% 43.93/6.56 % (711162)Peak memory usage: 14 MB
% 43.93/6.56 % (711162)Instructions burned: 132 (million)
% 43.93/6.56 % (711169)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2343096470:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 43.93/6.56 % TRYING [1]
% 43.93/6.56 % (711167)Instruction limit reached!
% 43.93/6.56 % (711167)------------------------------
% 43.93/6.56 % (711167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.93/6.56 % (711167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.93/6.56 % (711167)CaDiCaL version: 2.1.3
% 43.93/6.56 % (711167)Termination reason: Instruction limit
% 43.93/6.56 % (711167)Termination phase: Saturation
% 43.93/6.56 % (711167)Time elapsed: 0.093 s
% 43.93/6.56 % (711167)Peak memory usage: 14 MB
% 43.93/6.56 % (711167)Instructions burned: 180 (million)
% 43.93/6.56 % TRYING [2]
% 43.93/6.56 % (711171)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3297768540:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 43.93/6.56 % TRYING [3]
% 43.93/6.56 % (711161)Instruction limit reached!
% 43.93/6.56 % (711161)------------------------------
% 43.93/6.56 % (711161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.93/6.56 % (711161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.93/6.56 % (711161)CaDiCaL version: 2.1.3
% 43.93/6.56 % (711161)Termination reason: Instruction limit
% 43.93/6.56 % (711161)Termination phase: Finite model building preprocessing
% 43.93/6.56 % (711161)Time elapsed: 0.345 s
% 43.93/6.56 % (711161)Peak memory usage: 20 MB
% 43.93/6.56 % (711161)Instructions burned: 716 (million)
% 43.93/6.56 % (711173)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1755823380:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 43.93/6.56 % (711163)Instruction limit reached!
% 43.93/6.56 % (711163)------------------------------
% 43.93/6.56 % (711163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.93/6.56 % (711163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.93/6.56 % (711163)CaDiCaL version: 2.1.3
% 43.93/6.56 % (711163)Termination reason: Instruction limit
% 43.93/6.56 % (711163)Termination phase: Saturation
% 43.93/6.56 % (711163)Time elapsed: 0.394 s
% 43.93/6.56 % (711163)Peak memory usage: 19 MB
% 43.93/6.56 % (711163)Instructions burned: 685 (million)
% 43.93/6.56 % (711169)Instruction limit reached!
% 43.93/6.56 % (711169)------------------------------
% 43.93/6.56 % (711169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.93/6.56 % (711169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.93/6.56 % (711169)CaDiCaL version: 2.1.3
% 43.93/6.56 % (711169)Termination reason: Instruction limit
% 43.93/6.56 % (711169)Termination phase: Saturation
% 43.93/6.56 % (711169)Time elapsed: 0.311 s
% 43.93/6.56 % (711169)Peak memory usage: 16 MB
% 43.93/6.56 % (711169)Instructions burned: 477 (million)
% 43.93/6.56 % (711176)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3407253986:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 43.93/6.56 % (711175)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4016131254:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 43.93/6.56 % TRYING [1]
% 43.93/6.56 % (711171)Instruction limit reached!
% 43.93/6.56 % (711171)------------------------------
% 43.93/6.56 % (711171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.93/6.56 % (711171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.93/6.56 % (711171)CaDiCaL version: 2.1.3
% 43.93/6.56 % (711171)Termination reason: Instruction limit
% 43.93/6.56 % (711171)Termination phase: Finite model building constraint generation
% 43.93/6.56 % (711171)Time elapsed: 0.414 s
% 43.93/6.56 % (711171)Peak memory usage: 24 MB
% 43.93/6.56 % (711171)Instructions burned: 867 (million)
% 43.93/6.56 % (711179)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1640836426:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 43.93/6.56 % TRYING [4]
% 43.93/6.56 % (711176)Instruction limit reached!
% 43.93/6.56 % (711176)------------------------------
% 43.93/6.56 % (711176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.93/6.56 % (711176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.93/6.56 % (711176)CaDiCaL version: 2.1.3
% 94.74/13.77 % (711176)Termination reason: Instruction limit
% 94.74/13.77 % (711176)Termination phase: Saturation
% 94.74/13.77 % (711176)Time elapsed: 0.419 s
% 94.74/13.77 % (711176)Peak memory usage: 21 MB
% 94.74/13.77 % (711176)Instructions burned: 693 (million)
% 94.74/13.77 % (711175)Instruction limit reached!
% 94.74/13.77 % (711175)------------------------------
% 94.74/13.77 % (711175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.74/13.77 % (711175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.74/13.77 % (711175)CaDiCaL version: 2.1.3
% 94.74/13.77 % (711175)Termination reason: Instruction limit
% 94.74/13.77 % (711175)Termination phase: Finite model building constraint generation
% 94.74/13.77 % (711175)Time elapsed: 0.427 s
% 94.74/13.77 % (711175)Peak memory usage: 30 MB
% 94.74/13.77 % (711175)Instructions burned: 889 (million)
% 94.74/13.77 % (711181)fmb+10_1_sil=64000:random_seed=147848992:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 94.74/13.77 % (711182)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2871066647:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 94.74/13.77 % (711179)Instruction limit reached!
% 94.74/13.77 % (711179)------------------------------
% 94.74/13.77 % (711179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.74/13.77 % (711179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.74/13.77 % (711179)CaDiCaL version: 2.1.3
% 94.74/13.77 % (711179)Termination reason: Instruction limit
% 94.74/13.77 % (711179)Termination phase: Saturation
% 94.74/13.77 % (711179)Time elapsed: 0.468 s
% 94.74/13.77 % (711179)Peak memory usage: 21 MB
% 94.74/13.77 % (711179)Instructions burned: 879 (million)
% 94.74/13.77 % (711185)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=386748746:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 94.74/13.77 % (711173)Instruction limit reached!
% 94.74/13.77 % (711173)------------------------------
% 94.74/13.77 % (711173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.74/13.77 % (711173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.74/13.77 % (711173)CaDiCaL version: 2.1.3
% 94.74/13.77 % (711173)Termination reason: Instruction limit
% 94.74/13.77 % (711173)Termination phase: Saturation
% 94.74/13.77 % (711173)Time elapsed: 0.731 s
% 94.74/13.77 % (711173)Peak memory usage: 23 MB
% 94.74/13.77 % (711173)Instructions burned: 1180 (million)
% 94.74/13.77 % (711187)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1732789635:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 94.74/13.77 % TRYING [1]
% 94.74/13.77 % (711182)Cannot represent all propositional literals internally
% 94.74/13.77 % (711182)Refutation not found, incomplete strategy
% 94.74/13.77 % (711182)------------------------------
% 94.74/13.77 % (711182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.74/13.77 % (711182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.74/13.77 % (711182)CaDiCaL version: 2.1.3
% 94.74/13.77 % (711182)Termination reason: Refutation not found, incomplete strategy
% 94.74/13.77 % (711182)Time elapsed: 0.401 s
% 94.74/13.77 % (711182)Peak memory usage: 23 MB
% 94.74/13.77 % (711182)Instructions burned: 837 (million)
% 94.74/13.77 % (711182)------------------------------
% 94.74/13.77 % (711182)------------------------------
% 94.74/13.77 % (711189)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4116681910:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 94.74/13.77 % TRYING [2]
% 94.74/13.77 % TRYING [8]
% 94.74/13.77 % (711185)Instruction limit reached!
% 94.74/13.77 % (711185)------------------------------
% 94.74/13.77 % (711185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.74/13.77 % (711185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.74/13.77 % (711185)CaDiCaL version: 2.1.3
% 94.74/13.77 % (711185)Termination reason: Instruction limit
% 94.74/13.77 % (711185)Termination phase: Finite model building constraint generation
% 94.74/13.77 % (711185)Time elapsed: 0.433 s
% 94.74/13.77 % (711185)Peak memory usage: 28 MB
% 94.74/13.77 % (711185)Instructions burned: 921 (million)
% 94.74/13.77 % (711191)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1815835272:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 94.74/13.77 % (711191)Cannot represent all propositional literals internally
% 94.74/13.77 % (711191)Refutation not found, incomplete strategy
% 94.74/13.77 % (711191)------------------------------
% 94.74/13.77 % (711191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.74/13.77 % (711191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711191)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711191)Termination reason: Refutation not found, incomplete strategy
% 93.43/31.02 % (711191)Time elapsed: 0.418 s
% 93.43/31.02 % (711191)Peak memory usage: 24 MB
% 93.43/31.02 % (711191)Instructions burned: 861 (million)
% 93.43/31.02 % (711191)------------------------------
% 93.43/31.02 % (711191)------------------------------
% 93.43/31.02 % (711193)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1789144069:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 93.43/31.02 % TRYING [3]
% 93.43/31.02 % (711189)Instruction limit reached!
% 93.43/31.02 % (711189)------------------------------
% 93.43/31.02 % (711189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711189)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711189)Termination reason: Instruction limit
% 93.43/31.02 % (711189)Termination phase: Saturation
% 93.43/31.02 % (711189)Time elapsed: 0.788 s
% 93.43/31.02 % (711189)Peak memory usage: 33 MB
% 93.43/31.02 % (711189)Instructions burned: 1473 (million)
% 93.43/31.02 % (711195)ott-2_1_sil=16000:newcnf=on:random_seed=2665421674:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2977 on theBenchmark for (2977ds/869Mi)
% 93.43/31.02 % (711195)Instruction limit reached!
% 93.43/31.02 % (711195)------------------------------
% 93.43/31.02 % (711195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711195)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711195)Termination reason: Instruction limit
% 93.43/31.02 % (711195)Termination phase: Saturation
% 93.43/31.02 % (711195)Time elapsed: 0.547 s
% 93.43/31.02 % (711195)Peak memory usage: 19 MB
% 93.43/31.02 % (711195)Instructions burned: 869 (million)
% 93.43/31.02 % (711197)ott+10_1_sil=32000:tgt=ground:random_seed=3904614446:i=5114:av=off_2971 on theBenchmark for (2971ds/5114Mi)
% 93.43/31.02 % TRYING [5]
% 93.43/31.02 % (711193)Instruction limit reached!
% 93.43/31.02 % (711193)------------------------------
% 93.43/31.02 % (711193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711193)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711193)Termination reason: Instruction limit
% 93.43/31.02 % (711193)Termination phase: Finite model building preprocessing
% 93.43/31.02 % (711193)Time elapsed: 1.069 s
% 93.43/31.02 % (711193)Peak memory usage: 28 MB
% 93.43/31.02 % (711193)Instructions burned: 2175 (million)
% 93.43/31.02 % (711199)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1467103307:i=54282_2967 on theBenchmark for (2967ds/54282Mi)
% 93.43/31.02 % TRYING [1]
% 93.43/31.02 % TRYING [2]
% 93.43/31.02 % TRYING [3]
% 93.43/31.02 % (711187)Instruction limit reached!
% 93.43/31.02 % (711187)------------------------------
% 93.43/31.02 % (711187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711187)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711187)Termination reason: Instruction limit
% 93.43/31.02 % (711187)Termination phase: Saturation
% 93.43/31.02 % (711187)Time elapsed: 2.940 s
% 93.43/31.02 % (711187)Peak memory usage: 36 MB
% 93.43/31.02 % (711187)Instructions burned: 5131 (million)
% 93.43/31.02 % (711201)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3017173139:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 93.43/31.02 % TRYING [4]
% 93.43/31.02 % TRYING [4]
% 93.43/31.02 % (711197)Instruction limit reached!
% 93.43/31.02 % (711197)------------------------------
% 93.43/31.02 % (711197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711197)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711197)Termination reason: Instruction limit
% 93.43/31.02 % (711197)Termination phase: Saturation
% 93.43/31.02 % (711197)Time elapsed: 3.320 s
% 93.43/31.02 % (711197)Peak memory usage: 36 MB
% 93.43/31.02 % (711197)Instructions burned: 5115 (million)
% 93.43/31.02 % (711203)dis+21_1_sil=32000:sas=cadical:random_seed=1178117678:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 93.43/31.02 % (711201)Instruction limit reached!
% 93.43/31.02 % (711201)------------------------------
% 93.43/31.02 % (711201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711201)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711201)Termination reason: Instruction limit
% 93.43/31.02 % (711201)Termination phase: Saturation
% 93.43/31.02 % (711201)Time elapsed: 2.056 s
% 93.43/31.02 % (711201)Peak memory usage: 34 MB
% 93.43/31.02 % (711201)Instructions burned: 3513 (million)
% 93.43/31.02 % (711205)ott+11_1_sil=16000:gs=on:random_seed=376751724:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 93.43/31.02 % (711205)Instruction limit reached!
% 93.43/31.02 % (711205)------------------------------
% 93.43/31.02 % (711205)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711205)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711205)Termination reason: Instruction limit
% 93.43/31.02 % (711205)Termination phase: Saturation
% 93.43/31.02 % (711205)Time elapsed: 1.202 s
% 93.43/31.02 % (711205)Peak memory usage: 33 MB
% 93.43/31.02 % (711205)Instructions burned: 2251 (million)
% 93.43/31.02 % (711207)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3810022443:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi)
% 93.43/31.02 % (711203)Instruction limit reached!
% 93.43/31.02 % (711203)------------------------------
% 93.43/31.02 % (711203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711203)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711203)Termination reason: Instruction limit
% 93.43/31.02 % (711203)Termination phase: Saturation
% 93.43/31.02 % (711203)Time elapsed: 2.204 s
% 93.43/31.02 % (711203)Peak memory usage: 33 MB
% 93.43/31.02 % (711203)Instructions burned: 3774 (million)
% 93.43/31.02 % (711209)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3472160645:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2915 on theBenchmark for (2915ds/4591Mi)
% 93.43/31.02 % TRYING [5]
% 93.43/31.02 % TRYING [6]
% 93.43/31.02 % (711209)Instruction limit reached!
% 93.43/31.02 % (711209)------------------------------
% 93.43/31.02 % (711209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711209)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711209)Termination reason: Instruction limit
% 93.43/31.02 % (711209)Termination phase: Saturation
% 93.43/31.02 % (711209)Time elapsed: 1.898 s
% 93.43/31.02 % (711209)Peak memory usage: 32 MB
% 93.43/31.02 % (711209)Instructions burned: 4592 (million)
% 93.43/31.02 % (711211)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4251561019:i=29340_2896 on theBenchmark for (2896ds/29340Mi)
% 93.43/31.02 % (711181)Instruction limit reached!
% 93.43/31.02 % (711181)------------------------------
% 93.43/31.02 % (711181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711181)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711181)Termination reason: Instruction limit
% 93.43/31.02 % (711181)Termination phase: Finite model building SAT solving
% 93.43/31.02 % (711181)Time elapsed: 9.377 s
% 93.43/31.02 % (711181)Peak memory usage: 481 MB
% 93.43/31.02 % (711181)Instructions burned: 22062 (million)
% 93.43/31.02 % (711213)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1416126564:i=5211_2895 on theBenchmark for (2895ds/5211Mi)
% 93.43/31.02 % TRYING [7]
% 93.43/31.02 % (711213)Instruction limit reached!
% 93.43/31.02 % (711213)------------------------------
% 93.43/31.02 % (711213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711213)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711213)Termination reason: Instruction limit
% 93.43/31.02 % (711213)Termination phase: Saturation
% 93.43/31.02 % (711213)Time elapsed: 2.580 s
% 93.43/31.02 % (711213)Peak memory usage: 45 MB
% 93.43/31.02 % (711213)Instructions burned: 5212 (million)
% 93.43/31.02 % (711215)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2873826597:i=5497:nm=2_2869 on theBenchmark for (2869ds/5497Mi)
% 93.43/31.02 % (711215)Cannot represent all propositional literals internally
% 93.43/31.02 % (711215)Refutation not found, incomplete strategy
% 93.43/31.02 % (711215)------------------------------
% 93.43/31.02 % (711215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711215)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711215)Termination reason: Refutation not found, incomplete strategy
% 93.43/31.02 % (711215)Time elapsed: 0.416 s
% 93.43/31.02 % (711215)Peak memory usage: 24 MB
% 93.43/31.02 % (711215)Instructions burned: 861 (million)
% 93.43/31.02 % (711215)------------------------------
% 93.43/31.02 % (711215)------------------------------
% 93.43/31.02 % (711217)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=157512827:fmbsr=2:i=46332_2864 on theBenchmark for (2864ds/46332Mi)
% 93.43/31.02 % TRYING [15]
% 93.43/31.02 % TRYING [6]
% 93.43/31.02 % (711199)Instruction limit reached!
% 93.43/31.02 % (711199)------------------------------
% 93.43/31.02 % (711199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711199)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711199)Termination reason: Instruction limit
% 93.43/31.02 % (711199)Termination phase: Finite model building constraint generation
% 93.43/31.02 % (711199)Time elapsed: 20.524 s
% 93.43/31.02 % (711199)Peak memory usage: 1735 MB
% 93.43/31.02 % (711199)Instructions burned: 54283 (million)
% 93.43/31.02 % (711211)Instruction limit reached!
% 93.43/31.02 % (711211)------------------------------
% 93.43/31.02 % (711211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711211)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711211)Termination reason: Instruction limit
% 93.43/31.02 % (711211)Termination phase: Saturation
% 93.43/31.02 % (711211)Time elapsed: 13.483 s
% 93.43/31.02 % (711211)Peak memory usage: 129 MB
% 93.43/31.02 % (711211)Instructions burned: 29341 (million)
% 93.43/31.02 % (711219)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4154247181:i=14071_2761 on theBenchmark for (2761ds/14071Mi)
% 93.43/31.02 % (711221)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2285544194:i=22565:add=on:rawr=on_2760 on theBenchmark for (2760ds/22565Mi)
% 93.43/31.02 % TRYING [12]
% 93.43/31.02 % TRYING [7]
% 93.43/31.02 % (711219)Instruction limit reached!
% 93.43/31.02 % (711219)------------------------------
% 93.43/31.02 % (711219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711219)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711219)Termination reason: Instruction limit
% 93.43/31.02 % (711219)Termination phase: Finite model building constraint generation
% 93.43/31.02 % (711219)Time elapsed: 4.950 s
% 93.43/31.02 % (711219)Peak memory usage: 801 MB
% 93.43/31.02 % (711219)Instructions burned: 14072 (million)
% 93.43/31.02 % (711223)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2409060269:i=8173:av=off_2710 on theBenchmark for (2710ds/8173Mi)
% 93.43/31.02 % (711217)Instruction limit reached!
% 93.43/31.02 % (711217)------------------------------
% 93.43/31.02 % (711217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711217)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711217)Termination reason: Instruction limit
% 93.43/31.02 % (711217)Termination phase: Finite model building constraint generation
% 93.43/31.02 % (711217)Time elapsed: 16.135 s
% 93.43/31.02 % (711217)Peak memory usage: 2673 MB
% 93.43/31.02 % (711217)Instructions burned: 46335 (million)
% 93.43/31.02 % (711225)dis+10_16:1_sil=16000:random_seed=4018105647:i=9155:fsr=off_2699 on theBenchmark for (2699ds/9155Mi)
% 93.43/31.02 % (711207)Instruction limit reached!
% 93.43/31.02 % (711207)------------------------------
% 93.43/31.02 % (711207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.02 % (711207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.02 % (711207)CaDiCaL version: 2.1.3
% 93.43/31.02 % (711207)Termination reason: Instruction limit
% 93.43/31.02 % (711207)Termination phase: Finite model building constraint generation
% 93.43/31.02 % (711207)Time elapsed: 22.551 s
% 93.43/31.02 % (711207)Peak memory usage: 3412 MB
% 93.43/31.02 % (711207)Instructions burned: 67535 (million)
% 93.43/31.02 % (711223) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-711142-711223"...
% 93.43/31.02 % (711223)...printing done.
% 93.43/31.02 % (711223)Refutation found. Thanks to Tanya!
% 93.43/31.02 % SZS status Unsatisfiable for theBenchmark
% 93.43/31.02 % SZS output start Proof for theBenchmark
% See solution above
% 93.43/31.03 % (711223)------------------------------
% 93.43/31.03 % (711223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.43/31.03 % (711223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.43/31.03 % (711223)CaDiCaL version: 2.1.3
% 93.43/31.03 % (711223)Termination reason: Refutation
% 93.43/31.03 % (711223)Time elapsed: 1.557 s
% 93.43/31.03 % (711223)Peak memory usage: 33 MB
% 93.43/31.03 % (711223)Instructions burned: 2574 (million)
% 93.43/31.03 % (711142)Success in time 30.782 s
% 93.43/31.03 % Vampire exiting
%------------------------------------------------------------------------------