%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW231+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:29:54 PM UTC 2026
% Result : Theorem 68.96s 11.07s
% Output : Refutation 73.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 84
% Syntax : Number of formulae : 399 ( 120 unt; 45 def)
% Number of atoms : 1102 ( 285 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 1349 ( 646 ~; 645 |; 5 &)
% ( 39 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 46 ( 44 usr; 38 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 14 con; 0-3 aty)
% Number of variables : 314 ( 0 sgn 314 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__sqrt__abs2) ).
fof(f4,axiom,
! [X0] : c_NthRoot_Osqrt(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__sqrt__minus) ).
fof(f7,axiom,
! [X0,X1] :
( class_Groups_Oordered__ab__group__add__abs(X1)
=> c_Groups_Oabs__class_Oabs(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_Groups_Oabs__class_Oabs(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_abs__minus__cancel) ).
fof(f24,axiom,
! [X0,X1] :
( class_Groups_Ogroup__add(X1)
=> c_Groups_Ouminus__class_Ouminus(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_minus__minus) ).
fof(f26,axiom,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__mult__commute) ).
fof(f27,axiom,
! [X0,X1] :
( class_Groups_Oordered__ab__group__add__abs(X1)
=> c_Groups_Oabs__class_Oabs(X1,c_Groups_Oabs__class_Oabs(X1,X0)) = c_Groups_Oabs__class_Oabs(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_abs__idempotent) ).
fof(f28,axiom,
! [X0,X1] :
( c_NthRoot_Osqrt(X1) = c_NthRoot_Osqrt(X0)
<=> X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__sqrt__eq__iff) ).
fof(f37,axiom,
! [X0,X1,X2,X3] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X3,X2)),c_Complex_Orcis(X1,X0)) = c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X3),X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rcis__mult) ).
fof(f41,axiom,
! [X0,X1,X2] :
( class_RealVector_Oreal__normed__algebra(X2)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),c_Groups_Ouminus__class_Ouminus(X2,X0)) = c_Groups_Ouminus__class_Ouminus(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_mult_Ominus__right) ).
fof(f57,axiom,
! [X0,X1,X2] :
( class_Rings_Ocomm__semiring__1(X2)
=> c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(f58,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__1(X3)
=> c_Groups_Oplus__class_Oplus(X3,X2,c_Groups_Oplus__class_Oplus(X3,X1,X0)) = c_Groups_Oplus__class_Oplus(X3,X1,c_Groups_Oplus__class_Oplus(X3,X2,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J) ).
fof(f76,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
=> X1 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__le__antisym) ).
fof(f95,axiom,
! [X0,X1] :
( class_Groups_Oordered__ab__group__add__abs(X1)
=> c_Orderings_Oord__class_Oless__eq(X1,X0,c_Groups_Oabs__class_Oabs(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_abs__ge__self) ).
fof(f98,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0))
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__sqrt__le__iff) ).
fof(f109,axiom,
! [X0,X1] :
( class_Rings_Olinordered__idom(X1)
=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Osgn__class_Osgn(X1,X0)),c_Groups_Oabs__class_Oabs(X1,X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_mult__sgn__abs) ).
fof(f146,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__1(X1)
=> c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J) ).
fof(f221,axiom,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
<=> X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__add__minus__iff) ).
fof(f290,axiom,
! [X0,X1,X2] :
( class_Groups_Ogroup__add(X2)
=> c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_diff__add__cancel) ).
fof(f339,axiom,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__diff__def) ).
fof(f349,axiom,
! [X0] : c_Complex_Ocis(X0) = c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_cis__rcis__eq) ).
fof(f360,axiom,
! [X0] : c_Transcendental_Ocos(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Transcendental_Opi)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Transcendental_Ocos(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_cos__periodic__pi) ).
fof(f453,axiom,
! [X0] : c_Transcendental_Osin(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Transcendental_Osin(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_sin__periodic__pi2) ).
fof(f653,axiom,
! [X0] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0) )
& ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_abs__real__def) ).
fof(f946,axiom,
! [X0] : c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_complex__surj) ).
fof(f947,axiom,
! [X0] : c_Complex_OIm(c_Complex_Ocis(X0)) = c_Transcendental_Osin(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Im__cis) ).
fof(f948,axiom,
! [X0] : c_Complex_ORe(c_Complex_Ocis(X0)) = c_Transcendental_Ocos(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Re__cis) ).
fof(f953,axiom,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0) = c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(X0)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_complex__minus__def) ).
fof(f965,axiom,
! [X0,X1] : c_Complex_OIm(c_Complex_Orcis(X1,X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Transcendental_Osin(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Im__rcis) ).
fof(f966,axiom,
! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X1,X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Transcendental_Ocos(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Re__rcis) ).
fof(f1111,axiom,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs) ).
fof(f1112,axiom,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__RealVector_Oreal__normed__algebra) ).
fof(f1137,axiom,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Olinordered__idom) ).
fof(f1138,axiom,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Ocomm__semiring__1) ).
fof(f1149,axiom,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_RealDef__Oreal__Groups_Ogroup__add) ).
fof(f1201,conjecture,
c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a)) = c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1202,negated_conjecture,
c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a)) != c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a),
inference(negated_conjecture,[status(cth)],[f1201]) ).
fof(f1208,plain,
c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a)) != c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a),
inference(flattening,[],[f1202]) ).
fof(f1213,plain,
! [X0,X1] :
( c_Groups_Oabs__class_Oabs(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_Groups_Oabs__class_Oabs(X1,X0)
| ~ class_Groups_Oordered__ab__group__add__abs(X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f1233,plain,
! [X0,X1] :
( c_Groups_Ouminus__class_Ouminus(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = X0
| ~ class_Groups_Ogroup__add(X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f1234,plain,
! [X0,X1] :
( c_Groups_Oabs__class_Oabs(X1,c_Groups_Oabs__class_Oabs(X1,X0)) = c_Groups_Oabs__class_Oabs(X1,X0)
| ~ class_Groups_Oordered__ab__group__add__abs(X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f1246,plain,
! [X0,X1,X2] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),c_Groups_Ouminus__class_Ouminus(X2,X0)) = c_Groups_Ouminus__class_Ouminus(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0))
| ~ class_RealVector_Oreal__normed__algebra(X2) ),
inference(ennf_transformation,[],[f41]) ).
fof(f1262,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1)
| ~ class_Rings_Ocomm__semiring__1(X2) ),
inference(ennf_transformation,[],[f57]) ).
fof(f1263,plain,
! [X0,X1,X2,X3] :
( c_Groups_Oplus__class_Oplus(X3,X2,c_Groups_Oplus__class_Oplus(X3,X1,X0)) = c_Groups_Oplus__class_Oplus(X3,X1,c_Groups_Oplus__class_Oplus(X3,X2,X0))
| ~ class_Rings_Ocomm__semiring__1(X3) ),
inference(ennf_transformation,[],[f58]) ).
fof(f1274,plain,
! [X0,X1] :
( X1 = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(ennf_transformation,[],[f76]) ).
fof(f1275,plain,
! [X0,X1] :
( X1 = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(flattening,[],[f1274]) ).
fof(f1301,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(X1,X0,c_Groups_Oabs__class_Oabs(X1,X0))
| ~ class_Groups_Oordered__ab__group__add__abs(X1) ),
inference(ennf_transformation,[],[f95]) ).
fof(f1314,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Osgn__class_Osgn(X1,X0)),c_Groups_Oabs__class_Oabs(X1,X0)) = X0
| ~ class_Rings_Olinordered__idom(X1) ),
inference(ennf_transformation,[],[f109]) ).
fof(f1350,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0
| ~ class_Rings_Ocomm__semiring__1(X1) ),
inference(ennf_transformation,[],[f146]) ).
fof(f1522,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1
| ~ class_Groups_Ogroup__add(X2) ),
inference(ennf_transformation,[],[f290]) ).
fof(f1867,plain,
! [X0] :
( ( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) )
& ( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ) ),
inference(ennf_transformation,[],[f653]) ).
fof(f2159,plain,
! [X0,X1] :
( ( c_NthRoot_Osqrt(X1) = c_NthRoot_Osqrt(X0)
| X0 != X1 )
& ( X1 = X0
| c_NthRoot_Osqrt(X0) != c_NthRoot_Osqrt(X1) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f2173,plain,
! [X0,X1] :
( ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) )
& ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0)) ) ),
inference(nnf_transformation,[],[f98]) ).
fof(f2219,plain,
! [X0,X1] :
( ( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| X0 != X1 )
& ( X1 = X0
| c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ) ),
inference(nnf_transformation,[],[f221]) ).
fof(f2503,plain,
! [X0] : c_NthRoot_Osqrt(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f2504,plain,
! [X0] : c_NthRoot_Osqrt(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0)),
inference(cnf_transformation,[],[f4]) ).
fof(f2507,plain,
! [X0,X1] :
( ~ class_Groups_Oordered__ab__group__add__abs(X1)
| c_Groups_Oabs__class_Oabs(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = c_Groups_Oabs__class_Oabs(X1,X0) ),
inference(cnf_transformation,[],[f1213]) ).
fof(f2529,plain,
! [X0,X1] :
( ~ class_Groups_Ogroup__add(X1)
| c_Groups_Ouminus__class_Ouminus(X1,c_Groups_Ouminus__class_Ouminus(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f1233]) ).
fof(f2531,plain,
! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1),
inference(cnf_transformation,[],[f26]) ).
fof(f2532,plain,
! [X0,X1] :
( ~ class_Groups_Oordered__ab__group__add__abs(X1)
| c_Groups_Oabs__class_Oabs(X1,X0) = c_Groups_Oabs__class_Oabs(X1,c_Groups_Oabs__class_Oabs(X1,X0)) ),
inference(cnf_transformation,[],[f1234]) ).
fof(f2533,plain,
! [X0,X1] :
( c_NthRoot_Osqrt(X0) != c_NthRoot_Osqrt(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f2159]) ).
fof(f2545,plain,
! [X2,X3,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X3,X2)),c_Complex_Orcis(X1,X0)) = c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X3),X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X0)),
inference(cnf_transformation,[],[f37]) ).
fof(f2549,plain,
! [X2,X0,X1] :
( ~ class_RealVector_Oreal__normed__algebra(X2)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),c_Groups_Ouminus__class_Ouminus(X2,X0)) = c_Groups_Ouminus__class_Ouminus(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X0)) ),
inference(cnf_transformation,[],[f1246]) ).
fof(f2569,plain,
! [X2,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X2)
| c_Groups_Oplus__class_Oplus(X2,X1,X0) = c_Groups_Oplus__class_Oplus(X2,X0,X1) ),
inference(cnf_transformation,[],[f1262]) ).
fof(f2570,plain,
! [X2,X3,X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X3)
| c_Groups_Oplus__class_Oplus(X3,X2,c_Groups_Oplus__class_Oplus(X3,X1,X0)) = c_Groups_Oplus__class_Oplus(X3,X1,c_Groups_Oplus__class_Oplus(X3,X2,X0)) ),
inference(cnf_transformation,[],[f1263]) ).
fof(f2586,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| X0 = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[],[f1275]) ).
fof(f2611,plain,
! [X0,X1] :
( ~ class_Groups_Oordered__ab__group__add__abs(X1)
| c_Orderings_Oord__class_Oless__eq(X1,X0,c_Groups_Oabs__class_Oabs(X1,X0)) ),
inference(cnf_transformation,[],[f1301]) ).
fof(f2614,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[],[f2173]) ).
fof(f2615,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X0)) ),
inference(cnf_transformation,[],[f2173]) ).
fof(f2630,plain,
! [X0,X1] :
( ~ class_Rings_Olinordered__idom(X1)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),c_Groups_Osgn__class_Osgn(X1,X0)),c_Groups_Oabs__class_Oabs(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f1314]) ).
fof(f2679,plain,
! [X0,X1] :
( ~ class_Rings_Ocomm__semiring__1(X1)
| c_Groups_Oplus__class_Oplus(X1,X0,c_Groups_Ozero__class_Ozero(X1)) = X0 ),
inference(cnf_transformation,[],[f1350]) ).
fof(f2795,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| X0 != X1 ),
inference(cnf_transformation,[],[f2219]) ).
fof(f2887,plain,
! [X2,X0,X1] :
( ~ class_Groups_Ogroup__add(X2)
| c_Groups_Oplus__class_Oplus(X2,c_Groups_Ominus__class_Ominus(X2,X1,X0),X0) = X1 ),
inference(cnf_transformation,[],[f1522]) ).
fof(f2943,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0),
inference(cnf_transformation,[],[f339]) ).
fof(f2959,plain,
! [X0] : c_Complex_Ocis(X0) = c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0),
inference(cnf_transformation,[],[f349]) ).
fof(f2972,plain,
! [X0] : c_Transcendental_Ocos(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Transcendental_Opi)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Transcendental_Ocos(X0)),
inference(cnf_transformation,[],[f360]) ).
fof(f3081,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Transcendental_Osin(X0)) = c_Transcendental_Osin(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,X0)),
inference(cnf_transformation,[],[f453]) ).
fof(f3373,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0 ),
inference(cnf_transformation,[],[f1867]) ).
fof(f3374,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) ),
inference(cnf_transformation,[],[f1867]) ).
fof(f3808,plain,
! [X0] : c_Complex_Ocomplex_OComplex(c_Complex_ORe(X0),c_Complex_OIm(X0)) = X0,
inference(cnf_transformation,[],[f946]) ).
fof(f3809,plain,
! [X0] : c_Transcendental_Osin(X0) = c_Complex_OIm(c_Complex_Ocis(X0)),
inference(cnf_transformation,[],[f947]) ).
fof(f3810,plain,
! [X0] : c_Transcendental_Ocos(X0) = c_Complex_ORe(c_Complex_Ocis(X0)),
inference(cnf_transformation,[],[f948]) ).
fof(f3815,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,X0) = c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(X0)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(X0))),
inference(cnf_transformation,[],[f953]) ).
fof(f3827,plain,
! [X0,X1] : c_Complex_OIm(c_Complex_Orcis(X1,X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Transcendental_Osin(X0)),
inference(cnf_transformation,[],[f965]) ).
fof(f3828,plain,
! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X1,X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Transcendental_Ocos(X0)),
inference(cnf_transformation,[],[f966]) ).
fof(f3986,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1111]) ).
fof(f3987,plain,
class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1112]) ).
fof(f4012,plain,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1137]) ).
fof(f4013,plain,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1138]) ).
fof(f4024,plain,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1149]) ).
fof(f4076,plain,
c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a)) != c_Complex_Orcis(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)),v_a),
inference(cnf_transformation,[],[f1208]) ).
fof(f4077,plain,
! [X0] : c_Transcendental_Osin(X0) = c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0)),
inference(definition_unfolding,[],[f3809,f2959]) ).
fof(f4078,plain,
! [X0] : c_Transcendental_Ocos(X0) = c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0)),
inference(definition_unfolding,[],[f3810,f2959]) ).
fof(f4091,plain,
! [X0] : c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Transcendental_Opi))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))),
inference(definition_unfolding,[],[f2972,f4078,f4078]) ).
fof(f4108,plain,
! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))) = c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,X0))),
inference(definition_unfolding,[],[f3081,f4077,f4077]) ).
fof(f4126,plain,
! [X0,X1] : c_Complex_OIm(c_Complex_Orcis(X1,X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))),
inference(definition_unfolding,[],[f3827,f4077]) ).
fof(f4127,plain,
! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X1,X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))),
inference(definition_unfolding,[],[f3828,f4078]) ).
fof(f4172,plain,
! [X1] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)),
inference(equality_resolution,[],[f2795]) ).
fof(f4299,definition,
sF51 = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f4300,plain,
c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal) = sF51,
inference(reorient_equations,[],[f4299]) ).
fof(f4301,definition,
sF52 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f4302,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r) = sF52,
inference(reorient_equations,[],[f4301]) ).
fof(f4303,definition,
sF53 = c_NthRoot_Osqrt(sF52),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f4304,plain,
c_NthRoot_Osqrt(sF52) = sF53,
inference(reorient_equations,[],[f4303]) ).
fof(f4305,definition,
sF54 = hAPP(sF51,sF53),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f4306,plain,
hAPP(sF51,sF53) = sF54,
inference(reorient_equations,[],[f4305]) ).
fof(f4307,definition,
sF55 = hAPP(sF54,sF53),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
fof(f4308,plain,
hAPP(sF54,sF53) = sF55,
inference(reorient_equations,[],[f4307]) ).
fof(f4309,definition,
sF56 = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
fof(f4310,plain,
c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a) = sF56,
inference(reorient_equations,[],[f4309]) ).
fof(f4311,definition,
sF57 = c_Complex_Orcis(sF55,sF56),
introduced(definition,[new_symbols(definition,[sF57])],[function_definition]) ).
fof(f4312,plain,
c_Complex_Orcis(sF55,sF56) = sF57,
inference(reorient_equations,[],[f4311]) ).
fof(f4313,definition,
sF58 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF52),
introduced(definition,[new_symbols(definition,[sF58])],[function_definition]) ).
fof(f4314,plain,
c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF52) = sF58,
inference(reorient_equations,[],[f4313]) ).
fof(f4315,definition,
sF59 = c_Complex_Orcis(sF58,v_a),
introduced(definition,[new_symbols(definition,[sF59])],[function_definition]) ).
fof(f4316,plain,
c_Complex_Orcis(sF58,v_a) = sF59,
inference(reorient_equations,[],[f4315]) ).
fof(f4317,plain,
sF57 != sF59,
inference(definition_folding,[],[f4076,f4316,f4314,f4302,f4312,f4310,f4308,f4304,f4302,f4306,f4304,f4302,f4300]) ).
fof(f4326,definition,
( spl60_1
<=> sF57 = sF59 ),
introduced(definition,[new_symbols(definition,[spl60_1])],[avatar_definition]) ).
fof(f4329,plain,
~ spl60_1,
inference(avatar_split_clause,[],[f4317,f4326]) ).
fof(f4586,definition,
( spl60_53
<=> class_Groups_Ogroup__add(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl60_53])],[avatar_definition]) ).
fof(f4588,plain,
( class_Groups_Ogroup__add(tc_RealDef_Oreal)
| ~ spl60_53 ),
inference(avatar_component_clause,[],[f4586]) ).
fof(f4589,plain,
spl60_53,
inference(avatar_split_clause,[],[f4024,f4586]) ).
fof(f4641,definition,
( spl60_64
<=> class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl60_64])],[avatar_definition]) ).
fof(f4643,plain,
( class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal)
| ~ spl60_64 ),
inference(avatar_component_clause,[],[f4641]) ).
fof(f4644,plain,
spl60_64,
inference(avatar_split_clause,[],[f4013,f4641]) ).
fof(f4646,definition,
( spl60_65
<=> class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl60_65])],[avatar_definition]) ).
fof(f4648,plain,
( class_Rings_Olinordered__idom(tc_RealDef_Oreal)
| ~ spl60_65 ),
inference(avatar_component_clause,[],[f4646]) ).
fof(f4649,plain,
spl60_65,
inference(avatar_split_clause,[],[f4012,f4646]) ).
fof(f4771,definition,
( spl60_90
<=> class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl60_90])],[avatar_definition]) ).
fof(f4773,plain,
( class_RealVector_Oreal__normed__algebra(tc_RealDef_Oreal)
| ~ spl60_90 ),
inference(avatar_component_clause,[],[f4771]) ).
fof(f4774,plain,
spl60_90,
inference(avatar_split_clause,[],[f3987,f4771]) ).
fof(f4776,definition,
( spl60_91
<=> class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[spl60_91])],[avatar_definition]) ).
fof(f4778,plain,
( class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal)
| ~ spl60_91 ),
inference(avatar_component_clause,[],[f4776]) ).
fof(f4779,plain,
spl60_91,
inference(avatar_split_clause,[],[f3986,f4776]) ).
fof(f5583,plain,
! [X1] : c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X1),
inference(forward_demodulation,[],[f4172,f2943]) ).
fof(f5598,definition,
( spl60_249
<=> c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal) = sF51 ),
introduced(definition,[new_symbols(definition,[spl60_249])],[avatar_definition]) ).
fof(f5600,plain,
( c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal) = sF51
| ~ spl60_249 ),
inference(avatar_component_clause,[],[f5598]) ).
fof(f5601,plain,
spl60_249,
inference(avatar_split_clause,[],[f4300,f5598]) ).
fof(f5603,definition,
( spl60_250
<=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r) = sF52 ),
introduced(definition,[new_symbols(definition,[spl60_250])],[avatar_definition]) ).
fof(f5605,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r) = sF52
| ~ spl60_250 ),
inference(avatar_component_clause,[],[f5603]) ).
fof(f5606,plain,
spl60_250,
inference(avatar_split_clause,[],[f4302,f5603]) ).
fof(f5608,definition,
( spl60_251
<=> c_NthRoot_Osqrt(sF52) = sF53 ),
introduced(definition,[new_symbols(definition,[spl60_251])],[avatar_definition]) ).
fof(f5610,plain,
( c_NthRoot_Osqrt(sF52) = sF53
| ~ spl60_251 ),
inference(avatar_component_clause,[],[f5608]) ).
fof(f5611,plain,
spl60_251,
inference(avatar_split_clause,[],[f4304,f5608]) ).
fof(f5613,definition,
( spl60_252
<=> hAPP(sF51,sF53) = sF54 ),
introduced(definition,[new_symbols(definition,[spl60_252])],[avatar_definition]) ).
fof(f5615,plain,
( hAPP(sF51,sF53) = sF54
| ~ spl60_252 ),
inference(avatar_component_clause,[],[f5613]) ).
fof(f5616,plain,
spl60_252,
inference(avatar_split_clause,[],[f4306,f5613]) ).
fof(f5618,definition,
( spl60_253
<=> hAPP(sF54,sF53) = sF55 ),
introduced(definition,[new_symbols(definition,[spl60_253])],[avatar_definition]) ).
fof(f5620,plain,
( hAPP(sF54,sF53) = sF55
| ~ spl60_253 ),
inference(avatar_component_clause,[],[f5618]) ).
fof(f5621,plain,
spl60_253,
inference(avatar_split_clause,[],[f4308,f5618]) ).
fof(f5623,definition,
( spl60_254
<=> c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a) = sF56 ),
introduced(definition,[new_symbols(definition,[spl60_254])],[avatar_definition]) ).
fof(f5625,plain,
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,v_a) = sF56
| ~ spl60_254 ),
inference(avatar_component_clause,[],[f5623]) ).
fof(f5626,plain,
spl60_254,
inference(avatar_split_clause,[],[f4310,f5623]) ).
fof(f5628,definition,
( spl60_255
<=> c_Complex_Orcis(sF55,sF56) = sF57 ),
introduced(definition,[new_symbols(definition,[spl60_255])],[avatar_definition]) ).
fof(f5630,plain,
( c_Complex_Orcis(sF55,sF56) = sF57
| ~ spl60_255 ),
inference(avatar_component_clause,[],[f5628]) ).
fof(f5631,plain,
spl60_255,
inference(avatar_split_clause,[],[f4312,f5628]) ).
fof(f5633,definition,
( spl60_256
<=> c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF52) = sF58 ),
introduced(definition,[new_symbols(definition,[spl60_256])],[avatar_definition]) ).
fof(f5635,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF52) = sF58
| ~ spl60_256 ),
inference(avatar_component_clause,[],[f5633]) ).
fof(f5636,plain,
spl60_256,
inference(avatar_split_clause,[],[f4314,f5633]) ).
fof(f5638,definition,
( spl60_257
<=> c_Complex_Orcis(sF58,v_a) = sF59 ),
introduced(definition,[new_symbols(definition,[spl60_257])],[avatar_definition]) ).
fof(f5641,plain,
spl60_257,
inference(avatar_split_clause,[],[f4316,f5638]) ).
fof(f5703,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF52)) = c_NthRoot_Osqrt(sF58)
| ~ spl60_256 ),
inference(superposition,[],[f2504,f5635]) ).
fof(f5704,plain,
( c_NthRoot_Osqrt(sF58) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF53)
| ~ spl60_251
| ~ spl60_256 ),
inference(forward_demodulation,[],[f5703,f5610]) ).
fof(f5706,definition,
( spl60_264
<=> c_NthRoot_Osqrt(sF58) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF53) ),
introduced(definition,[new_symbols(definition,[spl60_264])],[avatar_definition]) ).
fof(f5708,plain,
( c_NthRoot_Osqrt(sF58) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF53)
| ~ spl60_264 ),
inference(avatar_component_clause,[],[f5706]) ).
fof(f5709,plain,
( spl60_264
| ~ spl60_251
| ~ spl60_256 ),
inference(avatar_split_clause,[],[f5704,f5633,f5608,f5706]) ).
fof(f5722,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_a))) = c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),sF56))
| ~ spl60_254 ),
inference(superposition,[],[f4108,f5625]) ).
fof(f5724,definition,
( spl60_267
<=> c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_a))) = c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),sF56)) ),
introduced(definition,[new_symbols(definition,[spl60_267])],[avatar_definition]) ).
fof(f5726,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_a))) = c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),sF56))
| ~ spl60_267 ),
inference(avatar_component_clause,[],[f5724]) ).
fof(f5727,plain,
( spl60_267
| ~ spl60_254 ),
inference(avatar_split_clause,[],[f5722,f5623,f5724]) ).
fof(f5914,plain,
( ! [X0] :
( c_NthRoot_Osqrt(X0) != sF53
| sF52 = X0 )
| ~ spl60_251 ),
inference(superposition,[],[f2533,f5610]) ).
fof(f6117,plain,
( ! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(hAPP(hAPP(sF51,X0),X0))
| ~ spl60_249 ),
inference(superposition,[],[f2503,f5600]) ).
fof(f6122,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53) = c_NthRoot_Osqrt(hAPP(sF54,sF53))
| ~ spl60_249
| ~ spl60_252 ),
inference(superposition,[],[f6117,f5615]) ).
fof(f6125,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53) = c_NthRoot_Osqrt(sF55)
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253 ),
inference(forward_demodulation,[],[f6122,f5620]) ).
fof(f6127,definition,
( spl60_317
<=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53) = c_NthRoot_Osqrt(sF55) ),
introduced(definition,[new_symbols(definition,[spl60_317])],[avatar_definition]) ).
fof(f6129,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53) = c_NthRoot_Osqrt(sF55)
| ~ spl60_317 ),
inference(avatar_component_clause,[],[f6127]) ).
fof(f6130,plain,
( spl60_317
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253 ),
inference(avatar_split_clause,[],[f6125,f5618,f5613,f5598,f6127]) ).
fof(f6136,plain,
( ! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = X0
| ~ spl60_64 ),
inference(resolution,[],[f4643,f2679]) ).
fof(f6139,plain,
( ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)
| ~ spl60_64 ),
inference(resolution,[],[f4643,f2569]) ).
fof(f6304,plain,
( ! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF53,c_NthRoot_Osqrt(X0))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF52,X0) )
| ~ spl60_251 ),
inference(superposition,[],[f2614,f5610]) ).
fof(f6308,plain,
( ! [X0] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),sF53)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,sF52) )
| ~ spl60_251 ),
inference(superposition,[],[f2614,f5610]) ).
fof(f6379,plain,
( ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1),X1) = X0
| ~ spl60_53 ),
inference(resolution,[],[f4588,f2887]) ).
fof(f6380,plain,
( ! [X0] : c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = X0
| ~ spl60_53 ),
inference(resolution,[],[f4588,f2529]) ).
fof(f6383,plain,
( ! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)) = X0
| ~ spl60_53
| ~ spl60_64 ),
inference(forward_demodulation,[],[f6379,f6139]) ).
fof(f6487,plain,
( sF53 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58))
| ~ spl60_53
| ~ spl60_264 ),
inference(superposition,[],[f6380,f5708]) ).
fof(f6492,definition,
( spl60_335
<=> sF53 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58)) ),
introduced(definition,[new_symbols(definition,[spl60_335])],[avatar_definition]) ).
fof(f6494,plain,
( sF53 = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58))
| ~ spl60_335 ),
inference(avatar_component_clause,[],[f6492]) ).
fof(f6495,plain,
( spl60_335
| ~ spl60_53
| ~ spl60_264 ),
inference(avatar_split_clause,[],[f6487,f5706,f4586,f6492]) ).
fof(f6896,plain,
( ! [X2,X3,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X0,X1)),c_Complex_Orcis(X2,X3)) = c_Complex_Orcis(hAPP(hAPP(sF51,X0),X2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X3))
| ~ spl60_249 ),
inference(superposition,[],[f2545,f5600]) ).
fof(f6898,plain,
( ! [X2,X3,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X2,X1)),c_Complex_Orcis(X3,X0)) = c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X2),X3),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))
| ~ spl60_64 ),
inference(superposition,[],[f2545,f6139]) ).
fof(f6902,plain,
( ! [X2,X3,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X1,X2)),c_Complex_Orcis(X3,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X2))) = c_Complex_Orcis(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),X3),X0)
| ~ spl60_53
| ~ spl60_64 ),
inference(superposition,[],[f2545,f6383]) ).
fof(f6923,plain,
( ! [X2,X3,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X1,X2)),c_Complex_Orcis(X3,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X2))) = c_Complex_Orcis(hAPP(hAPP(sF51,X1),X3),X0)
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249 ),
inference(forward_demodulation,[],[f6902,f5600]) ).
fof(f6927,plain,
( ! [X2,X3,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(X2,X1)),c_Complex_Orcis(X3,X0)) = c_Complex_Orcis(hAPP(hAPP(sF51,X2),X3),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))
| ~ spl60_64
| ~ spl60_249 ),
inference(forward_demodulation,[],[f6898,f5600]) ).
fof(f6933,plain,
( ! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(sF53,X0)),c_Complex_Orcis(X1,X2)) = c_Complex_Orcis(hAPP(sF54,X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X2))
| ~ spl60_249
| ~ spl60_252 ),
inference(superposition,[],[f6896,f5615]) ).
fof(f7038,plain,
( ! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))
| ~ spl60_91 ),
inference(resolution,[],[f4778,f2532]) ).
fof(f7039,plain,
( ! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0))
| ~ spl60_91 ),
inference(resolution,[],[f4778,f2611]) ).
fof(f7041,plain,
( ! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))
| ~ spl60_91 ),
inference(resolution,[],[f4778,f2507]) ).
fof(f7046,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF58) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF52)
| ~ spl60_91
| ~ spl60_256 ),
inference(superposition,[],[f7041,f5635]) ).
fof(f7052,definition,
( spl60_361
<=> c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF58) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF52) ),
introduced(definition,[new_symbols(definition,[spl60_361])],[avatar_definition]) ).
fof(f7054,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF58) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF52)
| ~ spl60_361 ),
inference(avatar_component_clause,[],[f7052]) ).
fof(f7057,plain,
( spl60_361
| ~ spl60_91
| ~ spl60_256 ),
inference(avatar_split_clause,[],[f7046,f5633,f4776,f7052]) ).
fof(f7200,plain,
! [X0] :
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = X0 ),
inference(resolution,[],[f3374,f3373]) ).
fof(f7245,plain,
( ! [X0,X1] : c_Complex_OIm(c_Complex_Orcis(X0,X1)) = hAPP(hAPP(sF51,X0),c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1)))
| ~ spl60_249 ),
inference(superposition,[],[f4126,f5600]) ).
fof(f7284,plain,
( ! [X0] : c_Complex_OIm(c_Complex_Orcis(sF53,X0)) = hAPP(sF54,c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0)))
| ~ spl60_249
| ~ spl60_252 ),
inference(superposition,[],[f7245,f5615]) ).
fof(f7361,plain,
( ! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X0,X1)) = hAPP(hAPP(sF51,X0),c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1)))
| ~ spl60_249 ),
inference(superposition,[],[f4127,f5600]) ).
fof(f7363,plain,
! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Transcendental_Opi))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X1),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0)))),
inference(superposition,[],[f4127,f4091]) ).
fof(f7368,plain,
( ! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Transcendental_Opi))) = hAPP(hAPP(sF51,X1),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))))
| ~ spl60_249 ),
inference(forward_demodulation,[],[f7363,f5600]) ).
fof(f7382,plain,
( ! [X0] : c_Complex_ORe(c_Complex_Orcis(sF53,X0)) = hAPP(sF54,c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0)))
| ~ spl60_249
| ~ spl60_252 ),
inference(superposition,[],[f7361,f5615]) ).
fof(f7810,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,X0)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)) = X0
| ~ spl60_65 ),
inference(resolution,[],[f4648,f2630]) ).
fof(f7812,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,X0)) = X0
| ~ spl60_65 ),
inference(forward_demodulation,[],[f7810,f2531]) ).
fof(f7814,plain,
( ! [X0] : hAPP(hAPP(sF51,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,X0)) = X0
| ~ spl60_65
| ~ spl60_249 ),
inference(forward_demodulation,[],[f7812,f5600]) ).
fof(f7822,plain,
( sF53 = hAPP(hAPP(sF51,c_NthRoot_Osqrt(sF55)),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53))
| ~ spl60_65
| ~ spl60_249
| ~ spl60_317 ),
inference(superposition,[],[f7814,f6129]) ).
fof(f7831,definition,
( spl60_434
<=> sF53 = hAPP(hAPP(sF51,c_NthRoot_Osqrt(sF55)),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53)) ),
introduced(definition,[new_symbols(definition,[spl60_434])],[avatar_definition]) ).
fof(f7833,plain,
( sF53 = hAPP(hAPP(sF51,c_NthRoot_Osqrt(sF55)),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53))
| ~ spl60_434 ),
inference(avatar_component_clause,[],[f7831]) ).
fof(f7834,plain,
( spl60_434
| ~ spl60_65
| ~ spl60_249
| ~ spl60_317 ),
inference(avatar_split_clause,[],[f7822,f6127,f5598,f4646,f7831]) ).
fof(f8425,plain,
( sF52 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF52)
| ~ spl60_91
| ~ spl60_250 ),
inference(superposition,[],[f7038,f5605]) ).
fof(f8437,definition,
( spl60_482
<=> sF52 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF52) ),
introduced(definition,[new_symbols(definition,[spl60_482])],[avatar_definition]) ).
fof(f8439,plain,
( sF52 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF52)
| ~ spl60_482 ),
inference(avatar_component_clause,[],[f8437]) ).
fof(f8440,plain,
( spl60_482
| ~ spl60_91
| ~ spl60_250 ),
inference(avatar_split_clause,[],[f8425,f5603,f4776,f8437]) ).
fof(f8796,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF53) = c_NthRoot_Osqrt(sF55)
| sF53 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53)
| ~ spl60_317 ),
inference(superposition,[],[f6129,f7200]) ).
fof(f8800,plain,
( c_NthRoot_Osqrt(sF58) = c_NthRoot_Osqrt(sF55)
| sF53 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53)
| ~ spl60_264
| ~ spl60_317 ),
inference(forward_demodulation,[],[f8796,f5708]) ).
fof(f8829,plain,
( sF53 = c_NthRoot_Osqrt(sF55)
| c_NthRoot_Osqrt(sF58) = c_NthRoot_Osqrt(sF55)
| ~ spl60_264
| ~ spl60_317 ),
inference(forward_demodulation,[],[f8800,f6129]) ).
fof(f8837,definition,
( spl60_511
<=> sF53 = c_NthRoot_Osqrt(sF55) ),
introduced(definition,[new_symbols(definition,[spl60_511])],[avatar_definition]) ).
fof(f8839,plain,
( sF53 = c_NthRoot_Osqrt(sF55)
| ~ spl60_511 ),
inference(avatar_component_clause,[],[f8837]) ).
fof(f8841,definition,
( spl60_512
<=> c_NthRoot_Osqrt(sF58) = c_NthRoot_Osqrt(sF55) ),
introduced(definition,[new_symbols(definition,[spl60_512])],[avatar_definition]) ).
fof(f8843,plain,
( c_NthRoot_Osqrt(sF58) = c_NthRoot_Osqrt(sF55)
| ~ spl60_512 ),
inference(avatar_component_clause,[],[f8841]) ).
fof(f8857,plain,
( spl60_512
| spl60_511
| ~ spl60_264
| ~ spl60_317 ),
inference(avatar_split_clause,[],[f8829,f6127,f5706,f8837,f8841]) ).
fof(f8880,plain,
( sF53 = hAPP(hAPP(sF51,sF53),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53))
| ~ spl60_434
| ~ spl60_511 ),
inference(superposition,[],[f7833,f8839]) ).
fof(f8891,plain,
( sF53 != sF53
| sF52 = sF55
| ~ spl60_251
| ~ spl60_511 ),
inference(superposition,[],[f5914,f8839]) ).
fof(f8896,plain,
( sF52 = sF55
| ~ spl60_251
| ~ spl60_511 ),
inference(trivial_inequality_removal,[],[f8891]) ).
fof(f8900,definition,
( spl60_517
<=> sF52 = sF55 ),
introduced(definition,[new_symbols(definition,[spl60_517])],[avatar_definition]) ).
fof(f8902,plain,
( sF52 = sF55
| ~ spl60_517 ),
inference(avatar_component_clause,[],[f8900]) ).
fof(f8903,plain,
( spl60_517
| ~ spl60_251
| ~ spl60_511 ),
inference(avatar_split_clause,[],[f8896,f8837,f5608,f8900]) ).
fof(f8912,plain,
( sF53 = hAPP(sF54,c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53))
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511 ),
inference(forward_demodulation,[],[f8880,f5615]) ).
fof(f8931,definition,
( spl60_522
<=> sF53 = hAPP(sF54,c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53)) ),
introduced(definition,[new_symbols(definition,[spl60_522])],[avatar_definition]) ).
fof(f8933,plain,
( sF53 = hAPP(sF54,c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53))
| ~ spl60_522 ),
inference(avatar_component_clause,[],[f8931]) ).
fof(f8940,plain,
( spl60_522
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511 ),
inference(avatar_split_clause,[],[f8912,f8837,f7831,f5613,f8931]) ).
fof(f8970,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF53,c_NthRoot_Osqrt(sF55))
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF52,sF58)
| ~ spl60_251
| ~ spl60_512 ),
inference(superposition,[],[f6304,f8843]) ).
fof(f8971,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF55),sF53)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF58,sF52)
| ~ spl60_251
| ~ spl60_512 ),
inference(superposition,[],[f6308,f8843]) ).
fof(f8993,definition,
( spl60_529
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF58,sF52) ),
introduced(definition,[new_symbols(definition,[spl60_529])],[avatar_definition]) ).
fof(f8995,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF58,sF52)
| ~ spl60_529 ),
inference(avatar_component_clause,[],[f8993]) ).
fof(f8997,definition,
( spl60_530
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF55),sF53) ),
introduced(definition,[new_symbols(definition,[spl60_530])],[avatar_definition]) ).
fof(f9000,plain,
( spl60_529
| ~ spl60_530
| ~ spl60_251
| ~ spl60_512 ),
inference(avatar_split_clause,[],[f8971,f8841,f5608,f8997,f8993]) ).
fof(f9002,definition,
( spl60_531
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF52,sF58) ),
introduced(definition,[new_symbols(definition,[spl60_531])],[avatar_definition]) ).
fof(f9004,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF52,sF58)
| ~ spl60_531 ),
inference(avatar_component_clause,[],[f9002]) ).
fof(f9006,definition,
( spl60_532
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF53,c_NthRoot_Osqrt(sF55)) ),
introduced(definition,[new_symbols(definition,[spl60_532])],[avatar_definition]) ).
fof(f9008,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF53,c_NthRoot_Osqrt(sF55))
| spl60_532 ),
inference(avatar_component_clause,[],[f9006]) ).
fof(f9009,plain,
( spl60_531
| ~ spl60_532
| ~ spl60_251
| ~ spl60_512 ),
inference(avatar_split_clause,[],[f8970,f8841,f5608,f9006,f9002]) ).
fof(f9084,plain,
( sF57 = c_Complex_Orcis(sF52,sF56)
| ~ spl60_255
| ~ spl60_517 ),
inference(superposition,[],[f5630,f8902]) ).
fof(f9101,definition,
( spl60_538
<=> sF57 = c_Complex_Orcis(sF52,sF56) ),
introduced(definition,[new_symbols(definition,[spl60_538])],[avatar_definition]) ).
fof(f9103,plain,
( sF57 = c_Complex_Orcis(sF52,sF56)
| ~ spl60_538 ),
inference(avatar_component_clause,[],[f9101]) ).
fof(f9104,plain,
( spl60_538
| ~ spl60_255
| ~ spl60_517 ),
inference(avatar_split_clause,[],[f9084,f8900,f5628,f9101]) ).
fof(f9111,plain,
( sF53 != c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53)
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53) != c_NthRoot_Osqrt(sF55)
| sF53 = c_NthRoot_Osqrt(sF55) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f9175,definition,
( spl60_542
<=> sF52 = sF58 ),
introduced(definition,[new_symbols(definition,[spl60_542])],[avatar_definition]) ).
fof(f9177,plain,
( sF52 != sF58
| spl60_542 ),
inference(avatar_component_clause,[],[f9175]) ).
fof(f11567,plain,
( ! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0)))
| ~ spl60_91 ),
inference(resolution,[],[f7039,f2615]) ).
fof(f11589,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF53,c_NthRoot_Osqrt(sF55))
| ~ spl60_91
| ~ spl60_317 ),
inference(superposition,[],[f7039,f6129]) ).
fof(f11756,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58),c_NthRoot_Osqrt(c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF52)))
| ~ spl60_91
| ~ spl60_361 ),
inference(superposition,[],[f11567,f7054]) ).
fof(f11757,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58),c_NthRoot_Osqrt(sF52))
| ~ spl60_91
| ~ spl60_361
| ~ spl60_482 ),
inference(forward_demodulation,[],[f11756,f8439]) ).
fof(f11864,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58),sF53)
| ~ spl60_91
| ~ spl60_251
| ~ spl60_361
| ~ spl60_482 ),
inference(forward_demodulation,[],[f11757,f5610]) ).
fof(f12957,plain,
( ! [X2,X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(sF53,X0)),c_Complex_Orcis(X1,X2)) = c_Complex_Orcis(hAPP(sF54,X1),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252 ),
inference(superposition,[],[f6927,f5615]) ).
fof(f12968,plain,
( ! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(c_NthRoot_Osqrt(sF55),X0)),c_Complex_Orcis(c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53),X1)) = c_Complex_Orcis(sF53,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_434 ),
inference(superposition,[],[f6927,f7833]) ).
fof(f13036,plain,
( ! [X0,X1] : c_Complex_Orcis(sF53,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(sF53,X0)),c_Complex_Orcis(c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53),X1))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_434
| ~ spl60_511 ),
inference(forward_demodulation,[],[f12968,f8839]) ).
fof(f13045,plain,
( ! [X0,X1] : c_Complex_Orcis(sF53,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)) = c_Complex_Orcis(hAPP(sF54,c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sF53)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511 ),
inference(forward_demodulation,[],[f13036,f6933]) ).
fof(f13050,plain,
( ! [X0,X1] : c_Complex_Orcis(sF53,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)) = c_Complex_Orcis(sF53,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(forward_demodulation,[],[f13045,f8933]) ).
fof(f13137,plain,
( ! [X2,X3,X0,X1] : c_Complex_Orcis(hAPP(hAPP(sF51,sF53),X2),X3) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(sF53,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1))),c_Complex_Orcis(X2,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X3,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(superposition,[],[f6923,f13050]) ).
fof(f13139,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(hAPP(sF54,sF53),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(sF53,X2)),c_Complex_Orcis(sF53,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(superposition,[],[f6933,f13050]) ).
fof(f13148,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(hAPP(sF54,sF53),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))) = c_Complex_Orcis(hAPP(sF54,sF53),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(forward_demodulation,[],[f13139,f6933]) ).
fof(f13150,plain,
( ! [X2,X3,X0,X1] : c_Complex_Orcis(hAPP(hAPP(sF51,sF53),X2),X3) = c_Complex_Orcis(hAPP(sF54,X2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X3,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(forward_demodulation,[],[f13137,f6933]) ).
fof(f13175,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(sF55,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))) = c_Complex_Orcis(sF55,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(forward_demodulation,[],[f13148,f5620]) ).
fof(f13177,plain,
( ! [X2,X3,X0,X1] : c_Complex_Orcis(hAPP(sF54,X2),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X3,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)))) = c_Complex_Orcis(hAPP(sF54,X2),X3)
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(forward_demodulation,[],[f13150,f5615]) ).
fof(f13191,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))) = c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522 ),
inference(forward_demodulation,[],[f13175,f8902]) ).
fof(f13399,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X0),X1) = hAPP(hAPP(sF51,X1),X0)
| ~ spl60_249 ),
inference(superposition,[],[f2531,f5600]) ).
fof(f13433,plain,
( ! [X0] : hAPP(sF54,X0) = hAPP(hAPP(sF51,X0),sF53)
| ~ spl60_249
| ~ spl60_252 ),
inference(superposition,[],[f13399,f5615]) ).
fof(f14041,plain,
( ! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X2))
| ~ spl60_64 ),
inference(resolution,[],[f2570,f4643]) ).
fof(f14165,plain,
( ! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X2),X1)
| ~ spl60_64 ),
inference(superposition,[],[f6139,f14041]) ).
fof(f14670,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(sF55,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)))) = c_Complex_Orcis(sF55,X2)
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_522 ),
inference(superposition,[],[f13177,f5620]) ).
fof(f14842,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)))) = c_Complex_Orcis(sF52,X2)
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522 ),
inference(forward_demodulation,[],[f14670,f8902]) ).
fof(f14914,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(sF52,X2) = c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)),X1)))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522 ),
inference(forward_demodulation,[],[f14842,f14165]) ).
fof(f14965,plain,
( ! [X2,X0,X1] : c_Complex_Orcis(sF52,X2) = c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X2,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)))))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522 ),
inference(forward_demodulation,[],[f14914,f13191]) ).
fof(f15060,plain,
( ! [X0,X1] : c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)) = c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522 ),
inference(superposition,[],[f14965,f5583]) ).
fof(f15123,plain,
( ! [X0,X1] : c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)) = c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522 ),
inference(forward_demodulation,[],[f15060,f6136]) ).
fof(f33023,plain,
( ! [X0,X1] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X1))
| ~ spl60_90 ),
inference(resolution,[],[f2549,f4773]) ).
fof(f33024,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,hAPP(hAPP(sF51,X0),X1))
| ~ spl60_90
| ~ spl60_249 ),
inference(forward_demodulation,[],[f33023,f5600]) ).
fof(f33026,plain,
( ! [X0] : hAPP(sF54,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,hAPP(sF54,X0))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252 ),
inference(superposition,[],[f33024,f5615]) ).
fof(f33030,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X1),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,hAPP(hAPP(sF51,X0),X1))
| ~ spl60_90
| ~ spl60_249 ),
inference(superposition,[],[f33024,f13399]) ).
fof(f33033,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1))))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Transcendental_Opi))))
| ~ spl60_90
| ~ spl60_249 ),
inference(superposition,[],[f33024,f7368]) ).
fof(f33052,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1)))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(X0,X1)))
| ~ spl60_90
| ~ spl60_249 ),
inference(superposition,[],[f33024,f7245]) ).
fof(f33053,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1)))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(X0,X1)))
| ~ spl60_90
| ~ spl60_249 ),
inference(superposition,[],[f33024,f7361]) ).
fof(f33088,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X0),c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X1))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Transcendental_Opi))))
| ~ spl60_53
| ~ spl60_90
| ~ spl60_249 ),
inference(forward_demodulation,[],[f33033,f6380]) ).
fof(f33103,plain,
( ! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X0,X1)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,c_Transcendental_Opi))))
| ~ spl60_53
| ~ spl60_90
| ~ spl60_249 ),
inference(forward_demodulation,[],[f33088,f7361]) ).
fof(f33214,plain,
( ! [X0,X1] : hAPP(hAPP(sF51,X1),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0)) = hAPP(hAPP(sF51,X0),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1))
| ~ spl60_90
| ~ spl60_249 ),
inference(superposition,[],[f33024,f33030]) ).
fof(f33289,plain,
( hAPP(sF54,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF53)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF55)
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253 ),
inference(superposition,[],[f33026,f5620]) ).
fof(f33310,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF52) = hAPP(sF54,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF53))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_517 ),
inference(forward_demodulation,[],[f33289,f8902]) ).
fof(f33492,plain,
( ! [X0,X1] : c_Complex_ORe(c_Complex_Orcis(X1,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(X1,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Transcendental_Opi,X0))))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_90
| ~ spl60_249 ),
inference(superposition,[],[f33103,f6139]) ).
fof(f33632,plain,
( ! [X0] : hAPP(hAPP(sF51,X0),c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),sF56))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(X0,v_a)))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_267 ),
inference(superposition,[],[f33052,f5726]) ).
fof(f33668,plain,
( ! [X0] : c_Complex_OIm(c_Complex_Orcis(X0,sF56)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(X0,v_a)))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_267 ),
inference(forward_demodulation,[],[f33632,f7245]) ).
fof(f33801,plain,
( ! [X0] : c_Complex_OIm(c_Complex_Orcis(X0,v_a)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(X0,sF56)))
| ~ spl60_53
| ~ spl60_90
| ~ spl60_249
| ~ spl60_267 ),
inference(superposition,[],[f6380,f33668]) ).
fof(f35191,plain,
( ! [X0] : c_Complex_ORe(c_Complex_Orcis(X0,v_a)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(X0,sF56)))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_90
| ~ spl60_249
| ~ spl60_254 ),
inference(superposition,[],[f33492,f5625]) ).
fof(f35659,plain,
( ! [X0] : hAPP(hAPP(sF51,X0),sF53) = hAPP(hAPP(sF51,c_NthRoot_Osqrt(sF58)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_335 ),
inference(superposition,[],[f33214,f6494]) ).
fof(f52723,plain,
( ! [X0] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Orcis(X0,sF56)) = c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(X0,sF56))),c_Complex_OIm(c_Complex_Orcis(X0,v_a)))
| ~ spl60_53
| ~ spl60_90
| ~ spl60_249
| ~ spl60_267 ),
inference(superposition,[],[f3815,f33801]) ).
fof(f52752,plain,
( ! [X0] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Orcis(X0,sF56)) = c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Orcis(X0,v_a)),c_Complex_OIm(c_Complex_Orcis(X0,v_a)))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_90
| ~ spl60_249
| ~ spl60_254
| ~ spl60_267 ),
inference(forward_demodulation,[],[f52723,f35191]) ).
fof(f52814,plain,
( ! [X0] : c_Complex_Orcis(X0,v_a) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Orcis(X0,sF56))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_90
| ~ spl60_249
| ~ spl60_254
| ~ spl60_267 ),
inference(forward_demodulation,[],[f52752,f3808]) ).
fof(f54251,definition,
( spl60_1422
<=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58),sF53) ),
introduced(definition,[new_symbols(definition,[spl60_1422])],[avatar_definition]) ).
fof(f54292,plain,
( spl60_1422
| ~ spl60_91
| ~ spl60_251
| ~ spl60_361
| ~ spl60_482 ),
inference(avatar_split_clause,[],[f11864,f8437,f7052,f5608,f4776,f54251]) ).
fof(f54717,plain,
( c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sF52) = hAPP(sF54,c_NthRoot_Osqrt(sF58))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_264
| ~ spl60_517 ),
inference(forward_demodulation,[],[f33310,f5708]) ).
fof(f54730,plain,
( ! [X0] : hAPP(sF54,X0) = hAPP(hAPP(sF51,c_NthRoot_Osqrt(sF58)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X0))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(forward_demodulation,[],[f35659,f13433]) ).
fof(f55353,plain,
( sF58 = hAPP(sF54,c_NthRoot_Osqrt(sF58))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_256
| ~ spl60_264
| ~ spl60_517 ),
inference(forward_demodulation,[],[f54717,f5635]) ).
fof(f55690,definition,
( spl60_1480
<=> sF58 = hAPP(sF54,c_NthRoot_Osqrt(sF58)) ),
introduced(definition,[new_symbols(definition,[spl60_1480])],[avatar_definition]) ).
fof(f55692,plain,
( sF58 = hAPP(sF54,c_NthRoot_Osqrt(sF58))
| ~ spl60_1480 ),
inference(avatar_component_clause,[],[f55690]) ).
fof(f55693,plain,
( spl60_1480
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_256
| ~ spl60_264
| ~ spl60_517 ),
inference(avatar_split_clause,[],[f55353,f8900,f5706,f5633,f5618,f5613,f5598,f4771,f55690]) ).
fof(f56679,definition,
( spl60_1524
<=> sF57 = c_Complex_Orcis(sF58,v_a) ),
introduced(definition,[new_symbols(definition,[spl60_1524])],[avatar_definition]) ).
fof(f57590,plain,
( sF52 = sF58
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF52,sF58)
| ~ spl60_529 ),
inference(resolution,[],[f8995,f2586]) ).
fof(f57838,plain,
( ! [X0] : hAPP(sF54,c_Complex_OIm(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0)))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(superposition,[],[f33052,f54730]) ).
fof(f57840,plain,
( ! [X0] : hAPP(sF54,c_Complex_ORe(c_Complex_Orcis(c_Groups_Oone__class_Oone(tc_RealDef_Oreal),X0))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0)))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(superposition,[],[f33053,f54730]) ).
fof(f57853,plain,
( ! [X0] : c_Complex_ORe(c_Complex_Orcis(sF53,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0)))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(forward_demodulation,[],[f57840,f7382]) ).
fof(f57855,plain,
( ! [X0] : c_Complex_OIm(c_Complex_Orcis(sF53,X0)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_OIm(c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0)))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(forward_demodulation,[],[f57838,f7284]) ).
fof(f57952,plain,
( ! [X0] : c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0)) = c_Complex_Ocomplex_OComplex(c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c_Complex_ORe(c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0))),c_Complex_OIm(c_Complex_Orcis(sF53,X0)))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(superposition,[],[f3815,f57855]) ).
fof(f57978,plain,
( ! [X0] : c_Complex_Ocomplex_OComplex(c_Complex_ORe(c_Complex_Orcis(sF53,X0)),c_Complex_OIm(c_Complex_Orcis(sF53,X0))) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(forward_demodulation,[],[f57952,f57853]) ).
fof(f57999,plain,
( ! [X0] : c_Complex_Orcis(sF53,X0) = c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex,c_Complex_Orcis(c_NthRoot_Osqrt(sF58),X0))
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_335 ),
inference(forward_demodulation,[],[f57978,f3808]) ).
fof(f58016,plain,
( c_Complex_Orcis(sF53,sF56) = c_Complex_Orcis(c_NthRoot_Osqrt(sF58),v_a)
| ~ spl60_53
| ~ spl60_64
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_254
| ~ spl60_267
| ~ spl60_335 ),
inference(superposition,[],[f52814,f57999]) ).
fof(f58020,definition,
( spl60_1532
<=> c_Complex_Orcis(sF53,sF56) = c_Complex_Orcis(c_NthRoot_Osqrt(sF58),v_a) ),
introduced(definition,[new_symbols(definition,[spl60_1532])],[avatar_definition]) ).
fof(f58022,plain,
( c_Complex_Orcis(sF53,sF56) = c_Complex_Orcis(c_NthRoot_Osqrt(sF58),v_a)
| ~ spl60_1532 ),
inference(avatar_component_clause,[],[f58020]) ).
fof(f58023,plain,
( spl60_1532
| ~ spl60_53
| ~ spl60_64
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_254
| ~ spl60_267
| ~ spl60_335 ),
inference(avatar_split_clause,[],[f58016,f6492,f5724,f5623,f5613,f5598,f4771,f4641,f4586,f58020]) ).
fof(f58057,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(sF53,X0)),c_Complex_Orcis(sF53,sF56)) = c_Complex_Orcis(hAPP(sF54,c_NthRoot_Osqrt(sF58)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_a,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_1532 ),
inference(superposition,[],[f12957,f58022]) ).
fof(f58060,plain,
( ! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Complex_Ocomplex),c_Complex_Orcis(sF53,X0)),c_Complex_Orcis(sF53,sF56)) = c_Complex_Orcis(sF58,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_a,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_1480
| ~ spl60_1532 ),
inference(forward_demodulation,[],[f58057,f55692]) ).
fof(f58076,plain,
( ! [X0] : c_Complex_Orcis(hAPP(sF54,sF53),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,sF56)) = c_Complex_Orcis(sF58,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_a,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_1480
| ~ spl60_1532 ),
inference(forward_demodulation,[],[f58060,f6933]) ).
fof(f58088,plain,
( ! [X0] : c_Complex_Orcis(sF55,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,sF56)) = c_Complex_Orcis(sF58,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_a,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_1480
| ~ spl60_1532 ),
inference(forward_demodulation,[],[f58076,f5620]) ).
fof(f58095,plain,
( ! [X0] : c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,sF56)) = c_Complex_Orcis(sF58,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_a,X0))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_517
| ~ spl60_1480
| ~ spl60_1532 ),
inference(forward_demodulation,[],[f58088,f8902]) ).
fof(f58329,plain,
( c_Complex_Orcis(sF58,v_a) = c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sF56))
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_517
| ~ spl60_1480
| ~ spl60_1532 ),
inference(superposition,[],[f58095,f6136]) ).
fof(f58382,plain,
( c_Complex_Orcis(sF58,v_a) = c_Complex_Orcis(sF52,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,sF56,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522
| ~ spl60_1480
| ~ spl60_1532 ),
inference(forward_demodulation,[],[f58329,f15123]) ).
fof(f58414,plain,
( c_Complex_Orcis(sF58,v_a) = c_Complex_Orcis(sF52,sF56)
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522
| ~ spl60_1480
| ~ spl60_1532 ),
inference(forward_demodulation,[],[f58382,f6136]) ).
fof(f58439,plain,
( sF57 = c_Complex_Orcis(sF58,v_a)
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522
| ~ spl60_538
| ~ spl60_1480
| ~ spl60_1532 ),
inference(forward_demodulation,[],[f58414,f9103]) ).
fof(f58464,plain,
( spl60_1524
| ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522
| ~ spl60_538
| ~ spl60_1480
| ~ spl60_1532 ),
inference(avatar_split_clause,[],[f58439,f58020,f55690,f9101,f8931,f8900,f8837,f7831,f5618,f5613,f5598,f4641,f4586,f56679]) ).
fof(f58478,plain,
( sF57 != c_Complex_Orcis(sF58,v_a)
| c_Complex_Orcis(sF58,v_a) != sF59
| sF57 = sF59 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f58682,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sF52,sF58)
| ~ spl60_529
| spl60_542 ),
inference(forward_subsumption_resolution,[],[f57590,f9177]) ).
fof(f59013,plain,
( $false
| ~ spl60_529
| ~ spl60_531
| spl60_542 ),
inference(forward_subsumption_resolution,[],[f58682,f9004]) ).
fof(f59014,plain,
( ~ spl60_529
| ~ spl60_531
| spl60_542 ),
inference(avatar_contradiction_clause,[],[f59013]) ).
fof(f59139,plain,
( c_NthRoot_Osqrt(sF58) != c_NthRoot_Osqrt(sF55)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF55),sF53)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_NthRoot_Osqrt(sF58),sF53) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f59142,plain,
( sF52 != sF58
| c_NthRoot_Osqrt(sF52) != sF53
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53) != c_NthRoot_Osqrt(sF55)
| c_NthRoot_Osqrt(sF58) != c_NthRoot_Osqrt(sF55)
| sF53 = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,sF53) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f59211,plain,
( $false
| ~ spl60_91
| ~ spl60_317
| spl60_532 ),
inference(forward_subsumption_resolution,[],[f11589,f9008]) ).
fof(f59212,plain,
( ~ spl60_91
| ~ spl60_317
| spl60_532 ),
inference(avatar_contradiction_clause,[],[f59211]) ).
cnf(s1,plain,
~ spl60_1,
inference(sat_conversion,[],[f4329]) ).
cnf(s53,plain,
spl60_53,
inference(sat_conversion,[],[f4589]) ).
cnf(s64,plain,
spl60_64,
inference(sat_conversion,[],[f4644]) ).
cnf(s65,plain,
spl60_65,
inference(sat_conversion,[],[f4649]) ).
cnf(s90,plain,
spl60_90,
inference(sat_conversion,[],[f4774]) ).
cnf(s91,plain,
spl60_91,
inference(sat_conversion,[],[f4779]) ).
cnf(s255,plain,
spl60_249,
inference(sat_conversion,[],[f5601]) ).
cnf(s256,plain,
spl60_250,
inference(sat_conversion,[],[f5606]) ).
cnf(s257,plain,
spl60_251,
inference(sat_conversion,[],[f5611]) ).
cnf(s258,plain,
spl60_252,
inference(sat_conversion,[],[f5616]) ).
cnf(s259,plain,
spl60_253,
inference(sat_conversion,[],[f5621]) ).
cnf(s260,plain,
spl60_254,
inference(sat_conversion,[],[f5626]) ).
cnf(s261,plain,
spl60_255,
inference(sat_conversion,[],[f5631]) ).
cnf(s262,plain,
spl60_256,
inference(sat_conversion,[],[f5636]) ).
cnf(s263,plain,
spl60_257,
inference(sat_conversion,[],[f5641]) ).
cnf(s271,plain,
( ~ spl60_251
| ~ spl60_256
| spl60_264 ),
inference(sat_conversion,[],[f5709]) ).
cnf(s274,plain,
( ~ spl60_254
| spl60_267 ),
inference(sat_conversion,[],[f5727]) ).
cnf(s349,plain,
( ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| spl60_317 ),
inference(sat_conversion,[],[f6130]) ).
cnf(s368,plain,
( ~ spl60_53
| ~ spl60_264
| spl60_335 ),
inference(sat_conversion,[],[f6495]) ).
cnf(s422,plain,
( ~ spl60_91
| ~ spl60_256
| spl60_361 ),
inference(sat_conversion,[],[f7057]) ).
cnf(s566,plain,
( ~ spl60_65
| ~ spl60_249
| ~ spl60_317
| spl60_434 ),
inference(sat_conversion,[],[f7834]) ).
cnf(s646,plain,
( ~ spl60_91
| ~ spl60_250
| spl60_482 ),
inference(sat_conversion,[],[f8440]) ).
cnf(s691,plain,
( ~ spl60_264
| ~ spl60_317
| spl60_511
| spl60_512 ),
inference(sat_conversion,[],[f8857]) ).
cnf(s696,plain,
( ~ spl60_251
| ~ spl60_511
| spl60_517 ),
inference(sat_conversion,[],[f8903]) ).
cnf(s704,plain,
( ~ spl60_252
| ~ spl60_434
| ~ spl60_511
| spl60_522 ),
inference(sat_conversion,[],[f8940]) ).
cnf(s709,plain,
( ~ spl60_251
| ~ spl60_512
| spl60_529
| ~ spl60_530 ),
inference(sat_conversion,[],[f9000]) ).
cnf(s710,plain,
( ~ spl60_251
| ~ spl60_512
| spl60_531
| ~ spl60_532 ),
inference(sat_conversion,[],[f9009]) ).
cnf(s728,plain,
( ~ spl60_255
| ~ spl60_517
| spl60_538 ),
inference(sat_conversion,[],[f9104]) ).
cnf(s729,plain,
( ~ spl60_317
| spl60_511
| ~ spl60_518 ),
inference(sat_conversion,[],[f9111]) ).
cnf(s2292,plain,
( ~ spl60_91
| ~ spl60_251
| ~ spl60_361
| ~ spl60_482
| spl60_1422 ),
inference(sat_conversion,[],[f54292]) ).
cnf(s2408,plain,
( ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_256
| ~ spl60_264
| ~ spl60_517
| spl60_1480 ),
inference(sat_conversion,[],[f55693]) ).
cnf(s2539,plain,
( ~ spl60_53
| ~ spl60_64
| ~ spl60_90
| ~ spl60_249
| ~ spl60_252
| ~ spl60_254
| ~ spl60_267
| ~ spl60_335
| spl60_1532 ),
inference(sat_conversion,[],[f58023]) ).
cnf(s2552,plain,
( ~ spl60_53
| ~ spl60_64
| ~ spl60_249
| ~ spl60_252
| ~ spl60_253
| ~ spl60_434
| ~ spl60_511
| ~ spl60_517
| ~ spl60_522
| ~ spl60_538
| ~ spl60_1480
| spl60_1524
| ~ spl60_1532 ),
inference(sat_conversion,[],[f58464]) ).
cnf(s2556,plain,
( spl60_1
| ~ spl60_257
| ~ spl60_1524 ),
inference(sat_conversion,[],[f58478]) ).
cnf(s2765,plain,
( ~ spl60_529
| ~ spl60_531
| spl60_542 ),
inference(sat_conversion,[],[f59014]) ).
cnf(s2815,plain,
( ~ spl60_512
| spl60_530
| ~ spl60_1422 ),
inference(sat_conversion,[],[f59139]) ).
cnf(s2818,plain,
( ~ spl60_251
| ~ spl60_317
| ~ spl60_512
| spl60_518
| ~ spl60_542 ),
inference(sat_conversion,[],[f59142]) ).
cnf(s2857,plain,
( ~ spl60_91
| ~ spl60_317
| spl60_532 ),
inference(sat_conversion,[],[f59212]) ).
cnf(s2916,plain,
spl60_267,
inference(rat,[],[s274,s260]) ).
cnf(s2919,plain,
spl60_264,
inference(rat,[],[s271,s262,s257]) ).
cnf(s2932,plain,
spl60_317,
inference(rat,[],[s349,s258,s259,s255]) ).
cnf(s2973,plain,
spl60_532,
inference(rat,[],[s2857,s2932,s91]) ).
cnf(s2995,plain,
spl60_482,
inference(rat,[],[s646,s256,s91]) ).
cnf(s3002,plain,
spl60_361,
inference(rat,[],[s422,s262,s91]) ).
cnf(s3004,plain,
spl60_1422,
inference(rat,[],[s2292,s2995,s91,s257,s3002]) ).
cnf(s3013,plain,
spl60_434,
inference(rat,[],[s566,s2932,s255,s65]) ).
cnf(s3071,plain,
spl60_335,
inference(rat,[],[s368,s2919,s53]) ).
cnf(s3102,plain,
spl60_1532,
inference(rat,[],[s2539,s53,s64,s2916,s260,s258,s255,s90,s3071]) ).
cnf(s3124,plain,
~ spl60_1524,
inference(rat,[],[s2556,s263,s1]) ).
cnf(s3199,plain,
~ spl60_511,
inference(rat,[],[s2552,s2408,s728,s704,s696,s255,s258,s259,s3013,s64,s53,s3124,s3102,s262,s2919,s90,s261,s257]) ).
cnf(s3200,plain,
~ spl60_518,
inference(rat,[],[s729,s2932,s3199]) ).
cnf(s3201,plain,
spl60_512,
inference(rat,[],[s691,s2932,s2919,s3199]) ).
cnf(s3204,plain,
spl60_530,
inference(rat,[],[s2815,s3004,s3201]) ).
cnf(s3210,plain,
spl60_531,
inference(rat,[],[s710,s2973,s257,s3201]) ).
cnf(s3211,plain,
spl60_529,
inference(rat,[],[s709,s3204,s257,s3201]) ).
cnf(s3212,plain,
~ spl60_542,
inference(rat,[],[s2818,s3200,s2932,s257,s3201]) ).
cnf(s3221,plain,
$false,
inference(rat,[],[s2765,s3212,s3210,s3211]) ).
fof(f59374,plain,
$false,
inference(avatar_sat_refutation,[],[s3221]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW231+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n014.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 13:20:01 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.90/2.25 % (1774140)Detected formulas, will run a generic FOF schedule.
% 10.90/2.25 % (1774152)dis-21_1_sil=8000:lcm=predicate:random_seed=971654980:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.90/2.25 % (1774152)Instruction limit reached!
% 10.90/2.25 % (1774152)------------------------------
% 10.90/2.25 % (1774152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.25 % (1774152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.25 % (1774152)CaDiCaL version: 2.1.3
% 10.90/2.25 % (1774152)Termination reason: Instruction limit
% 10.90/2.25 % (1774152)Termination phase: Saturation
% 10.90/2.25 % (1774152)Time elapsed: 0.039 s
% 10.90/2.25 % (1774152)Peak memory usage: 91 MB
% 10.90/2.25 % (1774152)Instructions burned: 131 (million)
% 10.90/2.25 % (1774151)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3765089935:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.90/2.25 % (1774150)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3729994482:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.90/2.25 % (1774146)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=2422870425:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.90/2.25 % (1774149)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2126074099:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.90/2.25 % (1774148)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1612758915:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.90/2.25 % (1774147)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4277559852:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.90/2.25 % (1774149)Instruction limit reached!
% 10.90/2.25 % (1774149)------------------------------
% 10.90/2.25 % (1774149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.25 % (1774149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.25 % (1774149)CaDiCaL version: 2.1.3
% 10.90/2.25 % (1774149)Termination reason: Instruction limit
% 10.90/2.25 % (1774149)Termination phase: Saturation
% 10.90/2.25 % (1774149)Time elapsed: 0.064 s
% 10.90/2.25 % (1774149)Peak memory usage: 90 MB
% 10.90/2.25 % (1774149)Instructions burned: 109 (million)
% 10.90/2.25 % (1774150)Instruction limit reached!
% 10.90/2.25 % (1774150)------------------------------
% 10.90/2.25 % (1774150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.25 % (1774150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.25 % (1774150)CaDiCaL version: 2.1.3
% 10.90/2.25 % (1774150)Termination reason: Instruction limit
% 10.90/2.25 % (1774150)Termination phase: Saturation
% 10.90/2.25 % (1774150)Time elapsed: 0.073 s
% 10.90/2.25 % (1774150)Peak memory usage: 90 MB
% 10.90/2.25 % (1774150)Instructions burned: 120 (million)
% 10.90/2.25 % (1774160)lrs+10_1_sil=8000:sp=occurrence:random_seed=1116298551:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.90/2.25 % (1774151)Instruction limit reached!
% 10.90/2.25 % (1774151)------------------------------
% 10.90/2.25 % (1774151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.25 % (1774151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.25 % (1774151)CaDiCaL version: 2.1.3
% 10.90/2.25 % (1774151)Termination reason: Instruction limit
% 10.90/2.25 % (1774151)Termination phase: Saturation
% 10.90/2.25 % (1774151)Time elapsed: 0.104 s
% 10.90/2.25 % (1774151)Peak memory usage: 91 MB
% 10.90/2.25 % (1774151)Instructions burned: 139 (million)
% 10.90/2.25 % (1774161)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3806203092:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 10.90/2.25 % (1774160)Instruction limit reached!
% 10.90/2.25 % (1774160)------------------------------
% 10.90/2.25 % (1774160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.25 % (1774160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.25 % (1774160)CaDiCaL version: 2.1.3
% 10.90/2.25 % (1774160)Termination reason: Instruction limit
% 10.90/2.25 % (1774160)Termination phase: Saturation
% 15.76/2.99 % (1774160)Time elapsed: 0.101 s
% 15.76/2.99 % (1774160)Peak memory usage: 92 MB
% 15.76/2.99 % (1774160)Instructions burned: 288 (million)
% 15.76/2.99 % (1774162)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3174858526:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 15.76/2.99 % (1774164)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4011799767:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 15.76/2.99 % (1774161)Instruction limit reached!
% 15.76/2.99 % (1774161)------------------------------
% 15.76/2.99 % (1774161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/2.99 % (1774161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/2.99 % (1774161)CaDiCaL version: 2.1.3
% 15.76/2.99 % (1774161)Termination reason: Instruction limit
% 15.76/2.99 % (1774161)Termination phase: Saturation
% 15.76/2.99 % (1774161)Time elapsed: 0.087 s
% 15.76/2.99 % (1774161)Peak memory usage: 91 MB
% 15.76/2.99 % (1774161)Instructions burned: 158 (million)
% 15.76/2.99 % (1774166)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1924127381:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 15.76/2.99 % (1774164)Instruction limit reached!
% 15.76/2.99 % (1774164)------------------------------
% 15.76/2.99 % (1774164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/2.99 % (1774164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/2.99 % (1774164)CaDiCaL version: 2.1.3
% 15.76/2.99 % (1774164)Termination reason: Instruction limit
% 15.76/2.99 % (1774164)Termination phase: Saturation
% 15.76/2.99 % (1774164)Time elapsed: 0.145 s
% 15.76/2.99 % (1774164)Peak memory usage: 92 MB
% 15.76/2.99 % (1774164)Instructions burned: 250 (million)
% 15.76/2.99 % (1774166)Instruction limit reached!
% 15.76/2.99 % (1774166)------------------------------
% 15.76/2.99 % (1774166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/2.99 % (1774166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/2.99 % (1774166)CaDiCaL version: 2.1.3
% 15.76/2.99 % (1774166)Termination reason: Instruction limit
% 15.76/2.99 % (1774166)Termination phase: Saturation
% 15.76/2.99 % (1774166)Time elapsed: 0.106 s
% 15.76/2.99 % (1774166)Peak memory usage: 92 MB
% 15.76/2.99 % (1774166)Instructions burned: 294 (million)
% 15.76/2.99 % (1774170)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3189094485:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 15.76/2.99 % (1774162)Instruction limit reached!
% 15.76/2.99 % (1774162)------------------------------
% 15.76/2.99 % (1774162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/2.99 % (1774162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/2.99 % (1774162)CaDiCaL version: 2.1.3
% 15.76/2.99 % (1774162)Termination reason: Instruction limit
% 15.76/2.99 % (1774162)Termination phase: Saturation
% 15.76/2.99 % (1774162)Time elapsed: 0.211 s
% 15.76/2.99 % (1774162)Peak memory usage: 93 MB
% 15.76/2.99 % (1774162)Instructions burned: 326 (million)
% 15.76/2.99 % (1774171)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2824139708:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 15.76/2.99 % (1774171)Instruction limit reached!
% 15.76/2.99 % (1774171)------------------------------
% 15.76/2.99 % (1774171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/2.99 % (1774171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.76/2.99 % (1774171)CaDiCaL version: 2.1.3
% 15.76/2.99 % (1774171)Termination reason: Instruction limit
% 15.76/2.99 % (1774171)Termination phase: Saturation
% 15.76/2.99 % (1774171)Time elapsed: 0.032 s
% 15.76/2.99 % (1774171)Peak memory usage: 90 MB
% 15.76/2.99 % (1774171)Instructions burned: 116 (million)
% 15.76/2.99 % (1774172)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=81180826:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 15.76/2.99 % (1774174)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3021169834:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 15.76/2.99 % (1774172)Refutation not found, incomplete strategy
% 15.76/2.99 % (1774172)------------------------------
% 15.76/2.99 % (1774172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.76/2.99 % (1774172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/6.58 % (1774172)CaDiCaL version: 2.1.3
% 41.43/6.58 % (1774172)Termination reason: Refutation not found, incomplete strategy
% 41.43/6.58 % (1774172)Time elapsed: 0.055 s
% 41.43/6.58 % (1774172)Peak memory usage: 90 MB
% 41.43/6.58 % (1774172)Instructions burned: 109 (million)
% 41.43/6.58 % (1774176)lrs+10_1_sil=8000:sp=occurrence:random_seed=3803981580:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 41.43/6.58 % (1774174)Instruction limit reached!
% 41.43/6.58 % (1774174)------------------------------
% 41.43/6.58 % (1774174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.43/6.58 % (1774174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/6.58 % (1774174)CaDiCaL version: 2.1.3
% 41.43/6.58 % (1774174)Termination reason: Instruction limit
% 41.43/6.58 % (1774174)Termination phase: Saturation
% 41.43/6.58 % (1774174)Time elapsed: 0.056 s
% 41.43/6.58 % (1774174)Peak memory usage: 90 MB
% 41.43/6.58 % (1774174)Instructions burned: 115 (million)
% 41.43/6.58 % (1774180)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3514939259:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 41.43/6.58 % (1774180)Refutation not found, incomplete strategy
% 41.43/6.58 % (1774180)------------------------------
% 41.43/6.58 % (1774180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.43/6.58 % (1774180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/6.58 % (1774180)CaDiCaL version: 2.1.3
% 41.43/6.58 % (1774180)Termination reason: Refutation not found, incomplete strategy
% 41.43/6.58 % (1774180)Time elapsed: 0.059 s
% 41.43/6.58 % (1774180)Peak memory usage: 91 MB
% 41.43/6.58 % (1774180)Instructions burned: 113 (million)
% 41.43/6.58 % (1774172)------------------------------
% 41.43/6.58 % (1774172)------------------------------
% 41.43/6.58 % (1774176)Instruction limit reached!
% 41.43/6.58 % (1774176)------------------------------
% 41.43/6.58 % (1774176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.43/6.58 % (1774176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/6.58 % (1774176)CaDiCaL version: 2.1.3
% 41.43/6.58 % (1774176)Termination reason: Instruction limit
% 41.43/6.58 % (1774176)Termination phase: Saturation
% 41.43/6.58 % (1774176)Time elapsed: 0.303 s
% 41.43/6.58 % (1774176)Peak memory usage: 99 MB
% 41.43/6.58 % (1774176)Instructions burned: 909 (million)
% 41.43/6.58 % (1774182)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2940535573:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 41.43/6.58 % (1774183)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1179124795:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 41.43/6.58 % (1774183)Instruction limit reached!
% 41.43/6.58 % (1774183)------------------------------
% 41.43/6.58 % (1774183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.43/6.58 % (1774183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/6.58 % (1774183)CaDiCaL version: 2.1.3
% 41.43/6.58 % (1774183)Termination reason: Instruction limit
% 41.43/6.58 % (1774183)Termination phase: Saturation
% 41.43/6.58 % (1774183)Time elapsed: 0.038 s
% 41.43/6.58 % (1774183)Peak memory usage: 91 MB
% 41.43/6.58 % (1774183)Instructions burned: 136 (million)
% 41.43/6.58 % (1774180)------------------------------
% 41.43/6.58 % (1774180)------------------------------
% 41.43/6.58 % (1774186)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=559552080:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 41.43/6.58 % (1774187)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1210985845:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 41.43/6.58 % (1774186)Instruction limit reached!
% 41.43/6.58 % (1774186)------------------------------
% 41.43/6.58 % (1774186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.43/6.58 % (1774186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.43/6.58 % (1774186)CaDiCaL version: 2.1.3
% 41.43/6.58 % (1774186)Termination reason: Instruction limit
% 41.43/6.58 % (1774186)Termination phase: Saturation
% 41.43/6.58 % (1774186)Time elapsed: 0.184 s
% 41.43/6.58 % (1774186)Peak memory usage: 98 MB
% 41.43/6.58 % (1774186)Instructions burned: 593 (million)
% 41.43/6.58 % (1774190)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=354347142:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 61.18/9.33 % (1774190)Instruction limit reached!
% 61.18/9.33 % (1774190)------------------------------
% 61.18/9.33 % (1774190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.18/9.33 % (1774190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.18/9.33 % (1774190)CaDiCaL version: 2.1.3
% 61.18/9.33 % (1774190)Termination reason: Instruction limit
% 61.18/9.33 % (1774190)Termination phase: Saturation
% 61.18/9.33 % (1774190)Time elapsed: 0.036 s
% 61.18/9.33 % (1774190)Peak memory usage: 91 MB
% 61.18/9.33 % (1774190)Instructions burned: 127 (million)
% 61.18/9.33 % (1774192)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1846275501:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 61.18/9.33 % (1774192)Instruction limit reached!
% 61.18/9.33 % (1774192)------------------------------
% 61.18/9.33 % (1774192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.18/9.33 % (1774192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.18/9.33 % (1774192)CaDiCaL version: 2.1.3
% 61.18/9.33 % (1774192)Termination reason: Instruction limit
% 61.18/9.33 % (1774192)Termination phase: Saturation
% 61.18/9.33 % (1774192)Time elapsed: 0.036 s
% 61.18/9.33 % (1774192)Peak memory usage: 90 MB
% 61.18/9.33 % (1774192)Instructions burned: 137 (million)
% 61.18/9.33 % (1774194)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3231455504:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi)
% 61.18/9.33 % (1774194)Refutation not found, incomplete strategy
% 61.18/9.33 % (1774194)------------------------------
% 61.18/9.33 % (1774194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.18/9.33 % (1774194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.18/9.33 % (1774194)CaDiCaL version: 2.1.3
% 61.18/9.33 % (1774194)Termination reason: Refutation not found, incomplete strategy
% 61.18/9.33 % (1774194)Time elapsed: 0.004 s
% 61.18/9.33 % (1774194)Peak memory usage: 89 MB
% 61.18/9.33 % (1774194)Instructions burned: 12 (million)
% 61.18/9.33 % (1774194)------------------------------
% 61.18/9.33 % (1774194)------------------------------
% 61.18/9.33 % (1774196)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1048741635:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi)
% 61.18/9.33 % (1774170)Instruction limit reached!
% 61.18/9.33 % (1774170)------------------------------
% 61.18/9.33 % (1774170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.18/9.33 % (1774170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.18/9.33 % (1774170)CaDiCaL version: 2.1.3
% 61.18/9.33 % (1774170)Termination reason: Instruction limit
% 61.18/9.33 % (1774170)Termination phase: Saturation
% 61.18/9.33 % (1774170)Time elapsed: 1.509 s
% 61.18/9.33 % (1774170)Peak memory usage: 147 MB
% 61.18/9.33 % (1774170)Instructions burned: 2351 (million)
% 61.18/9.33 % (1774196)Instruction limit reached!
% 61.18/9.33 % (1774196)------------------------------
% 61.18/9.33 % (1774196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.18/9.33 % (1774196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.18/9.33 % (1774196)CaDiCaL version: 2.1.3
% 61.18/9.33 % (1774196)Termination reason: Instruction limit
% 61.18/9.33 % (1774196)Termination phase: Saturation
% 61.18/9.33 % (1774196)Time elapsed: 0.123 s
% 61.18/9.33 % (1774196)Peak memory usage: 91 MB
% 61.18/9.33 % (1774196)Instructions burned: 434 (million)
% 61.18/9.33 % (1774198)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=162325866:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 61.18/9.33 % (1774199)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=828612535:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi)
% 61.18/9.33 % (1774199)Instruction limit reached!
% 61.18/9.33 % (1774199)------------------------------
% 61.18/9.33 % (1774199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.18/9.33 % (1774199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774199)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774199)Termination reason: Instruction limit
% 68.96/11.07 % (1774199)Termination phase: Saturation
% 68.96/11.07 % (1774199)Time elapsed: 0.043 s
% 68.96/11.07 % (1774199)Peak memory usage: 91 MB
% 68.96/11.07 % (1774199)Instructions burned: 151 (million)
% 68.96/11.07 % (1774202)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3030281712:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi)
% 68.96/11.07 % (1774182)Instruction limit reached!
% 68.96/11.07 % (1774182)------------------------------
% 68.96/11.07 % (1774182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774182)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774182)Termination reason: Instruction limit
% 68.96/11.07 % (1774182)Termination phase: Saturation
% 68.96/11.07 % (1774182)Time elapsed: 3.288 s
% 68.96/11.07 % (1774182)Peak memory usage: 164 MB
% 68.96/11.07 % (1774182)Instructions burned: 5204 (million)
% 68.96/11.07 % (1774204)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2238845415:i=667:av=off:fsr=off_2955 on theBenchmark for (2955ds/667Mi)
% 68.96/11.07 % (1774204)Refutation not found, incomplete strategy
% 68.96/11.07 % (1774204)------------------------------
% 68.96/11.07 % (1774204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774204)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774204)Termination reason: Refutation not found, incomplete strategy
% 68.96/11.07 % (1774204)Time elapsed: 0.054 s
% 68.96/11.07 % (1774204)Peak memory usage: 91 MB
% 68.96/11.07 % (1774204)Instructions burned: 104 (million)
% 68.96/11.07 % (1774204)------------------------------
% 68.96/11.07 % (1774204)------------------------------
% 68.96/11.07 % (1774206)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4275425119:s2a=on:i=185:s2at=1.8:fdi=4_2951 on theBenchmark for (2951ds/185Mi)
% 68.96/11.07 % (1774206)Instruction limit reached!
% 68.96/11.07 % (1774206)------------------------------
% 68.96/11.07 % (1774206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774206)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774206)Termination reason: Instruction limit
% 68.96/11.07 % (1774206)Termination phase: Saturation
% 68.96/11.07 % (1774206)Time elapsed: 0.095 s
% 68.96/11.07 % (1774206)Peak memory usage: 92 MB
% 68.96/11.07 % (1774206)Instructions burned: 186 (million)
% 68.96/11.07 % (1774208)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1639392538:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2948 on theBenchmark for (2948ds/193Mi)
% 68.96/11.07 % (1774208)Instruction limit reached!
% 68.96/11.07 % (1774208)------------------------------
% 68.96/11.07 % (1774208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774208)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774208)Termination reason: Instruction limit
% 68.96/11.07 % (1774208)Termination phase: Saturation
% 68.96/11.07 % (1774208)Time elapsed: 0.120 s
% 68.96/11.07 % (1774208)Peak memory usage: 93 MB
% 68.96/11.07 % (1774208)Instructions burned: 194 (million)
% 68.96/11.07 % (1774210)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2117458303:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2946 on theBenchmark for (2946ds/4850Mi)
% 68.96/11.07 % (1774210)Refutation not found, incomplete strategy
% 68.96/11.07 % (1774210)------------------------------
% 68.96/11.07 % (1774210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774210)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774210)Termination reason: Refutation not found, incomplete strategy
% 68.96/11.07 % (1774210)Time elapsed: 0.044 s
% 68.96/11.07 % (1774210)Peak memory usage: 90 MB
% 68.96/11.07 % (1774210)Instructions burned: 89 (million)
% 68.96/11.07 % (1774210)------------------------------
% 68.96/11.07 % (1774210)------------------------------
% 68.96/11.07 % (1774212)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3218267734:i=12111:sd=1:ss=included_2942 on theBenchmark for (2942ds/12111Mi)
% 68.96/11.07 % (1774198)Instruction limit reached!
% 68.96/11.07 % (1774198)------------------------------
% 68.96/11.07 % (1774198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774198)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774198)Termination reason: Instruction limit
% 68.96/11.07 % (1774198)Termination phase: Saturation
% 68.96/11.07 % (1774198)Time elapsed: 3.795 s
% 68.96/11.07 % (1774198)Peak memory usage: 178 MB
% 68.96/11.07 % (1774198)Instructions burned: 6061 (million)
% 68.96/11.07 % (1774214)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2553811429:i=319:kws=precedence:fsr=off_2939 on theBenchmark for (2939ds/319Mi)
% 68.96/11.07 % (1774214)Instruction limit reached!
% 68.96/11.07 % (1774214)------------------------------
% 68.96/11.07 % (1774214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774214)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774214)Termination reason: Instruction limit
% 68.96/11.07 % (1774214)Termination phase: Saturation
% 68.96/11.07 % (1774214)Time elapsed: 0.175 s
% 68.96/11.07 % (1774214)Peak memory usage: 94 MB
% 68.96/11.07 % (1774214)Instructions burned: 319 (million)
% 68.96/11.07 % (1774216)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3222646176:i=2064:ep=RST_2936 on theBenchmark for (2936ds/2064Mi)
% 68.96/11.07 % (1774202)Instruction limit reached!
% 68.96/11.07 % (1774202)------------------------------
% 68.96/11.07 % (1774202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774202)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774202)Termination reason: Instruction limit
% 68.96/11.07 % (1774202)Termination phase: Saturation
% 68.96/11.07 % (1774202)Time elapsed: 4.855 s
% 68.96/11.07 % (1774202)Peak memory usage: 213 MB
% 68.96/11.07 % (1774202)Instructions burned: 14156 (million)
% 68.96/11.07 % (1774218)dis-1011_128_sil=32000:random_seed=1193607590:i=3706:ep=RST:av=off_2927 on theBenchmark for (2927ds/3706Mi)
% 68.96/11.07 % (1774216)Instruction limit reached!
% 68.96/11.07 % (1774216)------------------------------
% 68.96/11.07 % (1774216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774216)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774216)Termination reason: Instruction limit
% 68.96/11.07 % (1774216)Termination phase: Saturation
% 68.96/11.07 % (1774216)Time elapsed: 1.180 s
% 68.96/11.07 % (1774216)Peak memory usage: 108 MB
% 68.96/11.07 % (1774216)Instructions burned: 2065 (million)
% 68.96/11.07 % (1774220)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=444103240:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2923 on theBenchmark for (2923ds/757Mi)
% 68.96/11.07 % (1774220)Instruction limit reached!
% 68.96/11.07 % (1774220)------------------------------
% 68.96/11.07 % (1774220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774220)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774220)Termination reason: Instruction limit
% 68.96/11.07 % (1774220)Termination phase: Saturation
% 68.96/11.07 % (1774220)Time elapsed: 0.455 s
% 68.96/11.07 % (1774220)Peak memory usage: 97 MB
% 68.96/11.07 % (1774220)Instructions burned: 758 (million)
% 68.96/11.07 % (1774222)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2563905641:i=13913:ss=axioms:sgt=8_2917 on theBenchmark for (2917ds/13913Mi)
% 68.96/11.07 % (1774218)Instruction limit reached!
% 68.96/11.07 % (1774218)------------------------------
% 68.96/11.07 % (1774218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774218)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774218)Termination reason: Instruction limit
% 68.96/11.07 % (1774218)Termination phase: Saturation
% 68.96/11.07 % (1774218)Time elapsed: 1.180 s
% 68.96/11.07 % (1774218)Peak memory usage: 123 MB
% 68.96/11.07 % (1774218)Instructions burned: 3709 (million)
% 68.96/11.07 % (1774224)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1730456129:i=9925:aac=none_2914 on theBenchmark for (2914ds/9925Mi)
% 68.96/11.07 % (1774187)Instruction limit reached!
% 68.96/11.07 % (1774187)------------------------------
% 68.96/11.07 % (1774187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774187)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774187)Termination reason: Instruction limit
% 68.96/11.07 % (1774187)Termination phase: Saturation
% 68.96/11.07 % (1774187)Time elapsed: 7.981 s
% 68.96/11.07 % (1774187)Peak memory usage: 228 MB
% 68.96/11.07 % (1774187)Instructions burned: 13194 (million)
% 68.96/11.07 % (1774226)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3297724269:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2906 on theBenchmark for (2906ds/2479Mi)
% 68.96/11.07 % (1774226)Refutation not found, incomplete strategy
% 68.96/11.07 % (1774226)------------------------------
% 68.96/11.07 % (1774226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774226)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774226)Termination reason: Refutation not found, incomplete strategy
% 68.96/11.07 % (1774226)Time elapsed: 0.035 s
% 68.96/11.07 % (1774226)Peak memory usage: 90 MB
% 68.96/11.07 % (1774226)Instructions burned: 61 (million)
% 68.96/11.07 % (1774226)------------------------------
% 68.96/11.07 % (1774226)------------------------------
% 68.96/11.07 % (1774228)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=464801016:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2902 on theBenchmark for (2902ds/440Mi)
% 68.96/11.07 % (1774212)First to succeed.
% 68.96/11.07 % (1774212)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1774140"
% 68.96/11.07 % (1774228)Instruction limit reached!
% 68.96/11.07 % (1774228)------------------------------
% 68.96/11.07 % (1774228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.96/11.07 % (1774228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.96/11.07 % (1774228)CaDiCaL version: 2.1.3
% 68.96/11.07 % (1774228)Termination reason: Instruction limit
% 68.96/11.07 % (1774228)Termination phase: Saturation
% 68.96/11.07 % (1774228)Time elapsed: 0.226 s
% 68.96/11.07 % (1774228)Peak memory usage: 94 MB
% 68.96/11.07 % (1774228)Instructions burned: 441 (million)
% 68.96/11.07 % (1774230)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1591017886:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2898 on theBenchmark for (2898ds/11145Mi)
% 68.96/11.07 % (1774212)Refutation found. Thanks to Tanya!
% 68.96/11.07 % SZS status Theorem for theBenchmark
% 68.96/11.07 % SZS output start Proof for theBenchmark
% See solution above
% 73.89/11.27 % (1774212)------------------------------
% 73.89/11.27 % (1774212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.89/11.27 % (1774212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.89/11.27 % (1774212)CaDiCaL version: 2.1.3
% 73.89/11.27 % (1774212)Termination reason: Refutation
% 73.89/11.27 % (1774212)Time elapsed: 4.201 s
% 73.89/11.27 % (1774212)Peak memory usage: 188 MB
% 73.89/11.27 % (1774212)Instructions burned: 6459 (million)
% 73.89/11.27 % (1774212)------------------------------
% 73.89/11.27 % (1774212)------------------------------
% 73.89/11.27 % (1774140)Success in time 10.399 s
% 73.89/11.27 % Vampire exiting
%------------------------------------------------------------------------------