%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW174+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:39:34 PM UTC 2026
% Result : Theorem 54.68s 9.46s
% Output : Refutation 54.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 18
% Syntax : Number of formulae : 99 ( 58 unt; 0 def)
% Number of atoms : 140 ( 93 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 88 ( 47 ~; 35 |; 0 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 135 ( 135 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [X0] : c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__abs) ).
fof(f13,axiom,
! [X0] : c_NthRoot_Osqrt(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_real__sqrt__abs2) ).
fof(f59,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/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J) ).
fof(f60,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/sandbox/benchmark/theBenchmark.p',fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
fof(f72,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls) ).
fof(f73,axiom,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__Pls__right) ).
fof(f74,axiom,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit0__def) ).
fof(f97,axiom,
! [X0,X1] :
( class_Int_Onumber__ring(X1)
=> c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oplus__class_Oplus(X1,X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_mult__2__right) ).
fof(f116,axiom,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__commute) ).
fof(f117,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__left__commute) ).
fof(f119,axiom,
! [X0,X1,X2] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zadd__assoc) ).
fof(f917,axiom,
! [X0] :
( class_Int_Onumber__ring(X0)
=> c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit1(c_Int_OPls)) = c_Groups_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_numeral__1__eq__1) ).
fof(f954,axiom,
! [X0,X1] :
( class_Int_Onumber__ring(X1)
=> c_Groups_Oplus__class_Oplus(X1,c_Int_Onumber__class_Onumber__of(X1,X0),c_Groups_Oone__class_Oone(X1)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OBit1(c_Int_OPls))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__special_I3_J) ).
fof(f955,axiom,
! [X0,X1] :
( class_Int_Onumber__ring(X1)
=> c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_add__special_I2_J) ).
fof(f971,axiom,
! [X0] : c_Int_OBit1(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Bit1__def) ).
fof(f1132,axiom,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Rings_Ocomm__semiring__1) ).
fof(f1150,axiom,
class_Int_Onumber__ring(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_RealDef__Oreal__Int_Onumber__ring) ).
fof(f1200,conjecture,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1201,negated_conjecture,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) != c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(negated_conjecture,[status(cth)],[f1200]) ).
fof(f1202,plain,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) != c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(flattening,[],[f1201]) ).
fof(f1236,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,[],[f59]) ).
fof(f1237,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,[],[f60]) ).
fof(f1267,plain,
! [X0,X1] :
( c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oplus__class_Oplus(X1,X0,X0)
| ~ class_Int_Onumber__ring(X1) ),
inference(ennf_transformation,[],[f97]) ).
fof(f2138,plain,
! [X0] :
( c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit1(c_Int_OPls)) = c_Groups_Oone__class_Oone(X0)
| ~ class_Int_Onumber__ring(X0) ),
inference(ennf_transformation,[],[f917]) ).
fof(f2181,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Int_Onumber__class_Onumber__of(X1,X0),c_Groups_Oone__class_Oone(X1)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OBit1(c_Int_OPls)))
| ~ class_Int_Onumber__ring(X1) ),
inference(ennf_transformation,[],[f954]) ).
fof(f2182,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),X0))
| ~ class_Int_Onumber__ring(X1) ),
inference(ennf_transformation,[],[f955]) ).
fof(f2218,plain,
! [X0] : c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[],[f12]) ).
fof(f2219,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f2269,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,[],[f1236]) ).
fof(f2270,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,[],[f1237]) ).
fof(f2286,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0) = X0,
inference(cnf_transformation,[],[f72]) ).
fof(f2287,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OPls) = X0,
inference(cnf_transformation,[],[f73]) ).
fof(f2288,plain,
! [X0] : c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
inference(cnf_transformation,[],[f74]) ).
fof(f2311,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oplus__class_Oplus(X1,X0,X0) ),
inference(cnf_transformation,[],[f1267]) ).
fof(f2330,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X1),
inference(cnf_transformation,[],[f116]) ).
fof(f2331,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X0)),
inference(cnf_transformation,[],[f117]) ).
fof(f2333,plain,
! [X2,X0,X1] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X1,X0)) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X2,X1),X0),
inference(cnf_transformation,[],[f119]) ).
fof(f3606,plain,
! [X0] :
( ~ class_Int_Onumber__ring(X0)
| c_Groups_Oone__class_Oone(X0) = c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit1(c_Int_OPls)) ),
inference(cnf_transformation,[],[f2138]) ).
fof(f3651,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Int_Onumber__class_Onumber__of(X1,X0),c_Groups_Oone__class_Oone(X1)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Int_OBit1(c_Int_OPls))) ),
inference(cnf_transformation,[],[f2181]) ).
fof(f3652,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OBit1(c_Int_OPls),X0)) ),
inference(cnf_transformation,[],[f2182]) ).
fof(f3668,plain,
! [X0] : c_Int_OBit1(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0),
inference(cnf_transformation,[],[f971]) ).
fof(f3837,plain,
class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1132]) ).
fof(f3855,plain,
class_Int_Onumber__ring(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f1150]) ).
fof(f3905,plain,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) != c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),
inference(cnf_transformation,[],[f1202]) ).
fof(f3918,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(definition_unfolding,[],[f2218,f2288,f3668]) ).
fof(f3945,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)))) ),
inference(definition_unfolding,[],[f2311,f2288,f3668]) ).
fof(f4187,plain,
! [X0] :
( ~ class_Int_Onumber__ring(X0)
| c_Groups_Oone__class_Oone(X0) = c_Int_Onumber__class_Onumber__of(X0,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)) ),
inference(definition_unfolding,[],[f3606,f3668]) ).
fof(f4219,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Int_Onumber__class_Onumber__of(X1,X0),c_Groups_Oone__class_Oone(X1)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))) ),
inference(definition_unfolding,[],[f3651,f3668]) ).
fof(f4220,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),X0)) ),
inference(definition_unfolding,[],[f3652,f3668]) ).
fof(f4238,plain,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls)),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))) != c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(definition_unfolding,[],[f3905,f2288,f2288,f3668,f2288,f3668,f2288,f3668]) ).
fof(f4461,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(consistent_polarity_flipping,[],[f2269]) ).
fof(f4462,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(consistent_polarity_flipping,[],[f2270]) ).
fof(f5666,plain,
~ class_Rings_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(consistent_polarity_flipping,[],[f3837]) ).
fof(f5774,plain,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))))) != c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))))),
inference(forward_demodulation,[],[f4238,f2287]) ).
fof(f5775,plain,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))) != c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))),c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),
inference(forward_demodulation,[],[f5774,f2287]) ).
fof(f6492,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),
inference(resolution,[],[f4462,f5666]) ).
fof(f10850,plain,
! [X0] :
( c_Groups_Oone__class_Oone(X0) = c_Int_Onumber__class_Onumber__of(X0,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))
| ~ class_Int_Onumber__ring(X0) ),
inference(forward_demodulation,[],[f4187,f2287]) ).
fof(f10851,plain,
! [X0] :
( ~ class_Int_Onumber__ring(X0)
| c_Groups_Oone__class_Oone(X0) = c_Int_Onumber__class_Onumber__of(X0,c_Groups_Oone__class_Oone(tc_Int_Oint)) ),
inference(forward_demodulation,[],[f10850,f2287]) ).
fof(f10853,plain,
c_Groups_Oone__class_Oone(tc_RealDef_Oreal) = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_Int_Oint)),
inference(resolution,[],[f10851,f3855]) ).
fof(f15398,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)),
inference(resolution,[],[f4461,f5666]) ).
fof(f35354,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Int_Onumber__class_Onumber__of(X1,X0),c_Groups_Oone__class_Oone(X1)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls)))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f4219,f2287]) ).
fof(f35355,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Int_Onumber__class_Onumber__of(X1,X0),c_Groups_Oone__class_Oone(X1)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oone__class_Oone(tc_Int_Oint))) ),
inference(forward_demodulation,[],[f35354,f2287]) ).
fof(f35357,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,X0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oone__class_Oone(tc_Int_Oint))),
inference(resolution,[],[f35355,f3855]) ).
fof(f35360,plain,
! [X0] : c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,c_Groups_Oone__class_Oone(tc_Int_Oint))) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,X0)),
inference(forward_demodulation,[],[f35357,f6492]) ).
fof(f35365,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0)))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f4220,f2333]) ).
fof(f35366,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),X0)))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f35365,f2331]) ).
fof(f35367,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),X0))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f35366,f2286]) ).
fof(f35368,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,X0)))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f35367,f2333]) ).
fof(f35369,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0)))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f35368,f2331]) ).
fof(f35370,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,c_Groups_Oone__class_Oone(X1),c_Int_Onumber__class_Onumber__of(X1,X0)) = c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0)) ),
inference(forward_demodulation,[],[f35369,f2286]) ).
fof(f35372,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,X0)) = c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0)),
inference(resolution,[],[f35370,f3855]) ).
fof(f43127,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))))),
inference(forward_demodulation,[],[f3918,f2331]) ).
fof(f43128,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))))),
inference(forward_demodulation,[],[f43127,f2333]) ).
fof(f43129,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))))),
inference(forward_demodulation,[],[f43128,f2331]) ).
fof(f43130,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))))),
inference(forward_demodulation,[],[f43129,f2286]) ).
fof(f43131,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))),
inference(forward_demodulation,[],[f43130,f2287]) ).
fof(f43132,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))))),
inference(forward_demodulation,[],[f43131,f2287]) ).
fof(f43133,plain,
! [X0] : c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0) = c_NthRoot_Osqrt(c_Power_Opower__class_Opower(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))),
inference(forward_demodulation,[],[f43132,f2287]) ).
fof(f43136,plain,
c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint))))) != c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))),
inference(superposition,[],[f5775,f43133]) ).
fof(f43171,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))) != c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),c_Groups_Oone__class_Oone(tc_Int_Oint))))),
inference(forward_demodulation,[],[f43136,f2331]) ).
fof(f43173,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))) != c_NthRoot_Osqrt(c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
inference(forward_demodulation,[],[f43171,f2330]) ).
fof(f46424,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f3945,f2331]) ).
fof(f46425,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f46424,f2333]) ).
fof(f46426,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Int_OPls,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls)))))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f46425,f2331]) ).
fof(f46427,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls),c_Int_OPls))))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f46426,f2286]) ).
fof(f46428,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls),c_Int_OPls))))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f46427,f2287]) ).
fof(f46429,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Int_OPls))))
| ~ class_Int_Onumber__ring(X1) ),
inference(forward_demodulation,[],[f46428,f2287]) ).
fof(f46430,plain,
! [X0,X1] :
( ~ class_Int_Onumber__ring(X1)
| c_Groups_Oplus__class_Oplus(X1,X0,X0) = c_Groups_Otimes__class_Otimes(X1,X0,c_Int_Onumber__class_Onumber__of(X1,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))) ),
inference(forward_demodulation,[],[f46429,f2287]) ).
fof(f46432,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))),
inference(resolution,[],[f46430,f3855]) ).
fof(f183053,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))) != c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
inference(superposition,[],[f43173,f35372]) ).
fof(f183089,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))) != c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
inference(forward_demodulation,[],[f183053,f35372]) ).
fof(f183125,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_Int_Oint)))) != c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_Int_Oint)))))),
inference(forward_demodulation,[],[f183089,f35360]) ).
fof(f183133,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) != c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
inference(forward_demodulation,[],[f183125,f10853]) ).
fof(f264323,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Int_Onumber__class_Onumber__of(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_Int_Oint)))),
inference(forward_demodulation,[],[f46432,f35360]) ).
fof(f264324,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X0) = c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))),
inference(forward_demodulation,[],[f264323,f10853]) ).
fof(f264492,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
inference(superposition,[],[f2219,f264324]) ).
fof(f264869,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
inference(forward_demodulation,[],[f264492,f15398]) ).
fof(f265137,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))) = c_NthRoot_Osqrt(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))),
inference(forward_demodulation,[],[f264869,f6492]) ).
fof(f265249,plain,
$false,
inference(forward_subsumption_resolution,[],[f265137,f183133]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW174+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n011.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 13:12:45 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.80/2.54 % (3377157)Will run a generic schedule for satisfiability detection.
% 15.80/2.54 % (3377162)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2892578776_2999 on theBenchmark for (2999ds/0Mi)
% 15.80/2.54 % (3377163)% WARNING: option uhcvi not known.
% 15.80/2.54 % (3377164)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=857207180:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.80/2.54 % (3377163)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1752420778:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.80/2.54 % (3377167)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3440078974:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.80/2.54 % (3377165)dis+10_1_sil=32000:sp=arity:random_seed=2803874618:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.80/2.54 % (3377166)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2043203501:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.80/2.54 % (3377168)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=111219785:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.80/2.54 % (3377165)Instruction limit reached!
% 15.80/2.54 % (3377165)------------------------------
% 15.80/2.54 % (3377165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.54 % (3377165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.54 % (3377165)CaDiCaL version: 2.1.3
% 15.80/2.54 % (3377165)Termination reason: Instruction limit
% 15.80/2.54 % (3377165)Termination phase: Saturation
% 15.80/2.54 % (3377165)Time elapsed: 0.050 s
% 15.80/2.54 % (3377165)Peak memory usage: 14 MB
% 15.80/2.54 % (3377165)Instructions burned: 103 (million)
% 15.80/2.54 % (3377166)Instruction limit reached!
% 15.80/2.54 % (3377166)------------------------------
% 15.80/2.54 % (3377166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.54 % (3377166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.54 % (3377166)CaDiCaL version: 2.1.3
% 15.80/2.54 % (3377166)Termination reason: Instruction limit
% 15.80/2.54 % (3377166)Termination phase: Property scanning
% 15.80/2.54 % (3377166)Time elapsed: 0.055 s
% 15.80/2.54 % (3377166)Peak memory usage: 13 MB
% 15.80/2.54 % (3377166)Instructions burned: 118 (million)
% 15.80/2.54 % (3377167)Instruction limit reached!
% 15.80/2.54 % (3377167)------------------------------
% 15.80/2.54 % (3377167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.54 % (3377167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.54 % (3377167)CaDiCaL version: 2.1.3
% 15.80/2.54 % (3377167)Termination reason: Instruction limit
% 15.80/2.54 % (3377167)Termination phase: Saturation
% 15.80/2.54 % (3377167)Time elapsed: 0.067 s
% 15.80/2.54 % (3377167)Peak memory usage: 14 MB
% 15.80/2.54 % (3377167)Instructions burned: 132 (million)
% 15.80/2.54 % (3377176)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2829198621:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.80/2.54 % (3377177)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2474148778:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.80/2.54 % (3377178)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1528821180:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.80/2.54 % (3377168)Instruction limit reached!
% 15.80/2.54 % (3377168)------------------------------
% 15.80/2.54 % (3377168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.54 % (3377168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/2.54 % (3377168)CaDiCaL version: 2.1.3
% 15.80/2.54 % (3377168)Termination reason: Instruction limit
% 15.80/2.54 % (3377168)Termination phase: Saturation
% 15.80/2.54 % (3377168)Time elapsed: 0.088 s
% 15.80/2.54 % (3377168)Peak memory usage: 15 MB
% 15.80/2.54 % (3377168)Instructions burned: 159 (million)
% 15.80/2.54 % (3377182)ott-21_1_sil=16000:fs=off:random_seed=2737811159:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.80/2.54 % (3377177)Instruction limit reached!
% 15.80/2.54 % (3377177)------------------------------
% 15.80/2.54 % (3377177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.80/2.54 % (3377177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.84/6.62 % (3377177)CaDiCaL version: 2.1.3
% 44.84/6.62 % (3377177)Termination reason: Instruction limit
% 44.84/6.62 % (3377177)Termination phase: Property scanning
% 44.84/6.62 % (3377177)Time elapsed: 0.061 s
% 44.84/6.62 % (3377177)Peak memory usage: 13 MB
% 44.84/6.62 % (3377177)Instructions burned: 133 (million)
% 44.84/6.62 % (3377184)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2331214492:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 44.84/6.62 % (3377182)Instruction limit reached!
% 44.84/6.62 % (3377182)------------------------------
% 44.84/6.62 % (3377182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.84/6.62 % (3377182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.84/6.62 % (3377182)CaDiCaL version: 2.1.3
% 44.84/6.62 % (3377182)Termination reason: Instruction limit
% 44.84/6.62 % (3377182)Termination phase: Saturation
% 44.84/6.62 % (3377182)Time elapsed: 0.088 s
% 44.84/6.62 % (3377182)Peak memory usage: 14 MB
% 44.84/6.62 % (3377182)Instructions burned: 180 (million)
% 44.84/6.62 % (3377186)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2671176432:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.84/6.62 % TRYING [1]
% 44.84/6.62 % TRYING [2]
% 44.84/6.62 % (3377176)Instruction limit reached!
% 44.84/6.62 % (3377176)------------------------------
% 44.84/6.62 % (3377176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.84/6.62 % (3377176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.84/6.62 % (3377176)CaDiCaL version: 2.1.3
% 44.84/6.62 % (3377176)Termination reason: Instruction limit
% 44.84/6.62 % (3377176)Termination phase: Finite model building preprocessing
% 44.84/6.62 % (3377176)Time elapsed: 0.346 s
% 44.84/6.62 % (3377176)Peak memory usage: 20 MB
% 44.84/6.62 % (3377176)Instructions burned: 715 (million)
% 44.84/6.62 % TRYING [3]
% 44.84/6.62 % (3377188)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3302791588:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 44.84/6.62 % (3377184)Instruction limit reached!
% 44.84/6.62 % (3377184)------------------------------
% 44.84/6.62 % (3377184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.84/6.62 % (3377184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.84/6.62 % (3377184)CaDiCaL version: 2.1.3
% 44.84/6.62 % (3377184)Termination reason: Instruction limit
% 44.84/6.62 % (3377184)Termination phase: Saturation
% 44.84/6.62 % (3377184)Time elapsed: 0.298 s
% 44.84/6.62 % (3377184)Peak memory usage: 16 MB
% 44.84/6.62 % (3377184)Instructions burned: 479 (million)
% 44.84/6.62 % (3377178)Instruction limit reached!
% 44.84/6.62 % (3377178)------------------------------
% 44.84/6.62 % (3377178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.84/6.62 % (3377178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.84/6.62 % (3377178)CaDiCaL version: 2.1.3
% 44.84/6.62 % (3377178)Termination reason: Instruction limit
% 44.84/6.62 % (3377178)Termination phase: Saturation
% 44.84/6.62 % (3377178)Time elapsed: 0.376 s
% 44.84/6.62 % (3377178)Peak memory usage: 18 MB
% 44.84/6.62 % (3377178)Instructions burned: 685 (million)
% 44.84/6.62 % (3377190)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1609100723:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 44.84/6.62 % (3377191)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1316353213:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 44.84/6.62 % (3377186)Instruction limit reached!
% 44.84/6.62 % (3377186)------------------------------
% 44.84/6.62 % (3377186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.84/6.62 % (3377186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.84/6.62 % (3377186)CaDiCaL version: 2.1.3
% 44.84/6.62 % (3377186)Termination reason: Instruction limit
% 44.84/6.62 % (3377186)Termination phase: Finite model building preprocessing
% 44.84/6.62 % (3377186)Time elapsed: 0.428 s
% 44.84/6.62 % (3377186)Peak memory usage: 20 MB
% 44.84/6.62 % (3377186)Instructions burned: 866 (million)
% 44.84/6.62 % (3377194)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1267891096:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 44.84/6.62 % (3377190)Instruction limit reached!
% 44.84/6.62 % (3377190)------------------------------
% 44.84/6.62 % (3377190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.84/6.62 % (3377190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377190)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377190)Termination reason: Instruction limit
% 54.68/9.46 % (3377190)Termination phase: Finite model building preprocessing
% 54.68/9.46 % (3377190)Time elapsed: 0.442 s
% 54.68/9.46 % (3377190)Peak memory usage: 22 MB
% 54.68/9.46 % (3377190)Instructions burned: 890 (million)
% 54.68/9.46 % (3377191)Instruction limit reached!
% 54.68/9.46 % (3377191)------------------------------
% 54.68/9.46 % (3377191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377191)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377191)Termination reason: Instruction limit
% 54.68/9.46 % (3377191)Termination phase: Saturation
% 54.68/9.46 % (3377191)Time elapsed: 0.447 s
% 54.68/9.46 % (3377191)Peak memory usage: 21 MB
% 54.68/9.46 % (3377191)Instructions burned: 693 (million)
% 54.68/9.46 % (3377196)fmb+10_1_sil=64000:random_seed=2626393317:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 54.68/9.46 % (3377197)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1303361282:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 54.68/9.46 % TRYING [4]
% 54.68/9.46 % (3377194)Instruction limit reached!
% 54.68/9.46 % (3377194)------------------------------
% 54.68/9.46 % (3377194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377194)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377194)Termination reason: Instruction limit
% 54.68/9.46 % (3377194)Termination phase: Saturation
% 54.68/9.46 % (3377194)Time elapsed: 0.456 s
% 54.68/9.46 % (3377194)Peak memory usage: 21 MB
% 54.68/9.46 % (3377194)Instructions burned: 879 (million)
% 54.68/9.46 % (3377200)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2270659134:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 54.68/9.46 % (3377188)Instruction limit reached!
% 54.68/9.46 % (3377188)------------------------------
% 54.68/9.46 % (3377188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377188)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377188)Termination reason: Instruction limit
% 54.68/9.46 % (3377188)Termination phase: Saturation
% 54.68/9.46 % (3377188)Time elapsed: 0.724 s
% 54.68/9.46 % (3377188)Peak memory usage: 21 MB
% 54.68/9.46 % (3377188)Instructions burned: 1180 (million)
% 54.68/9.46 % (3377202)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3346530243:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 54.68/9.46 % TRYING [1]
% 54.68/9.46 % (3377197)Cannot represent all propositional literals internally
% 54.68/9.46 % (3377197)Refutation not found, incomplete strategy
% 54.68/9.46 % (3377197)------------------------------
% 54.68/9.46 % (3377197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377197)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377197)Termination reason: Refutation not found, incomplete strategy
% 54.68/9.46 % (3377197)Time elapsed: 0.568 s
% 54.68/9.46 % (3377197)Peak memory usage: 27 MB
% 54.68/9.46 % (3377197)Instructions burned: 1175 (million)
% 54.68/9.46 % (3377197)------------------------------
% 54.68/9.46 % (3377197)------------------------------
% 54.68/9.46 % (3377204)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3997093629:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 54.68/9.46 % TRYING [2]
% 54.68/9.46 % (3377200)Instruction limit reached!
% 54.68/9.46 % (3377200)------------------------------
% 54.68/9.46 % (3377200)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377200)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377200)Termination reason: Instruction limit
% 54.68/9.46 % (3377200)Termination phase: Finite model building preprocessing
% 54.68/9.46 % (3377200)Time elapsed: 0.456 s
% 54.68/9.46 % (3377200)Peak memory usage: 22 MB
% 54.68/9.46 % (3377200)Instructions burned: 920 (million)
% 54.68/9.46 % (3377206)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3178823637:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 54.68/9.46 % (3377206)Cannot represent all propositional literals internally
% 54.68/9.46 % (3377206)Refutation not found, incomplete strategy
% 54.68/9.46 % (3377206)------------------------------
% 54.68/9.46 % (3377206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377206)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377206)Termination reason: Refutation not found, incomplete strategy
% 54.68/9.46 % (3377206)Time elapsed: 0.595 s
% 54.68/9.46 % (3377206)Peak memory usage: 27 MB
% 54.68/9.46 % (3377206)Instructions burned: 1230 (million)
% 54.68/9.46 % (3377206)------------------------------
% 54.68/9.46 % (3377206)------------------------------
% 54.68/9.46 % (3377208)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=98810100:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 54.68/9.46 % (3377204)Instruction limit reached!
% 54.68/9.46 % (3377204)------------------------------
% 54.68/9.46 % (3377204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377204)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377204)Termination reason: Instruction limit
% 54.68/9.46 % (3377204)Termination phase: Saturation
% 54.68/9.46 % (3377204)Time elapsed: 0.769 s
% 54.68/9.46 % (3377204)Peak memory usage: 27 MB
% 54.68/9.46 % (3377204)Instructions burned: 1472 (million)
% 54.68/9.46 % (3377210)ott-2_1_sil=16000:newcnf=on:random_seed=3659173395:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2976 on theBenchmark for (2976ds/869Mi)
% 54.68/9.46 % TRYING [3]
% 54.68/9.46 % (3377210)Instruction limit reached!
% 54.68/9.46 % (3377210)------------------------------
% 54.68/9.46 % (3377210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377210)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377210)Termination reason: Instruction limit
% 54.68/9.46 % (3377210)Termination phase: Saturation
% 54.68/9.46 % (3377210)Time elapsed: 0.519 s
% 54.68/9.46 % (3377210)Peak memory usage: 19 MB
% 54.68/9.46 % (3377210)Instructions burned: 870 (million)
% 54.68/9.46 % (3377212)ott+10_1_sil=32000:tgt=ground:random_seed=2517157602:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 54.68/9.46 % (3377208)Instruction limit reached!
% 54.68/9.46 % (3377208)------------------------------
% 54.68/9.46 % (3377208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377208)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377208)Termination reason: Instruction limit
% 54.68/9.46 % (3377208)Termination phase: Finite model building preprocessing
% 54.68/9.46 % (3377208)Time elapsed: 1.058 s
% 54.68/9.46 % (3377208)Peak memory usage: 32 MB
% 54.68/9.46 % (3377208)Instructions burned: 2176 (million)
% 54.68/9.46 % (3377214)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=807864864:i=54282_2966 on theBenchmark for (2966ds/54282Mi)
% 54.68/9.46 % TRYING [1]
% 54.68/9.46 % TRYING [5]
% 54.68/9.46 % TRYING [2]
% 54.68/9.46 % TRYING [3]
% 54.68/9.46 % (3377202)Instruction limit reached!
% 54.68/9.46 % (3377202)------------------------------
% 54.68/9.46 % (3377202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377202)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377202)Termination reason: Instruction limit
% 54.68/9.46 % (3377202)Termination phase: Saturation
% 54.68/9.46 % (3377202)Time elapsed: 3.0000 s
% 54.68/9.46 % (3377202)Peak memory usage: 36 MB
% 54.68/9.46 % (3377202)Instructions burned: 5132 (million)
% 54.68/9.46 % (3377216)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3019860167:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 54.68/9.46 % TRYING [4]
% 54.68/9.46 % (3377212)Instruction limit reached!
% 54.68/9.46 % (3377212)------------------------------
% 54.68/9.46 % (3377212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377212)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377212)Termination reason: Instruction limit
% 54.68/9.46 % (3377212)Termination phase: Saturation
% 54.68/9.46 % (3377212)Time elapsed: 3.345 s
% 54.68/9.46 % (3377212)Peak memory usage: 33 MB
% 54.68/9.46 % (3377212)Instructions burned: 5115 (million)
% 54.68/9.46 % (3377218)dis+21_1_sil=32000:sas=cadical:random_seed=3595135408:i=3773:amm=off_2936 on theBenchmark for (2936ds/3773Mi)
% 54.68/9.46 % (3377216)Instruction limit reached!
% 54.68/9.46 % (3377216)------------------------------
% 54.68/9.46 % (3377216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377216)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377216)Termination reason: Instruction limit
% 54.68/9.46 % (3377216)Termination phase: Saturation
% 54.68/9.46 % (3377216)Time elapsed: 2.091 s
% 54.68/9.46 % (3377216)Peak memory usage: 30 MB
% 54.68/9.46 % (3377216)Instructions burned: 3513 (million)
% 54.68/9.46 % (3377220)ott+11_1_sil=16000:gs=on:random_seed=618174679:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 54.68/9.46 % TRYING [4]
% 54.68/9.46 % (3377220)Instruction limit reached!
% 54.68/9.46 % (3377220)------------------------------
% 54.68/9.46 % (3377220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377220)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377220)Termination reason: Instruction limit
% 54.68/9.46 % (3377220)Termination phase: Saturation
% 54.68/9.46 % (3377220)Time elapsed: 1.360 s
% 54.68/9.46 % (3377220)Peak memory usage: 41 MB
% 54.68/9.46 % (3377220)Instructions burned: 2251 (million)
% 54.68/9.46 % (3377222)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3263491461:fmbsr=1.6:i=67534_2922 on theBenchmark for (2922ds/67534Mi)
% 54.68/9.46 % (3377218)Instruction limit reached!
% 54.68/9.46 % (3377218)------------------------------
% 54.68/9.46 % (3377218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.46 % (3377218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.46 % (3377218)CaDiCaL version: 2.1.3
% 54.68/9.46 % (3377218)Termination reason: Instruction limit
% 54.68/9.46 % (3377218)Termination phase: Saturation
% 54.68/9.46 % (3377218)Time elapsed: 2.249 s
% 54.68/9.46 % (3377218)Peak memory usage: 33 MB
% 54.68/9.46 % (3377218)Instructions burned: 3773 (million)
% 54.68/9.46 % (3377224)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3368249368:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2914 on theBenchmark for (2914ds/4591Mi)
% 54.68/9.46 % (3377163) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3377157-3377163"...
% 54.68/9.46 % (3377163)...printing done.
% 54.68/9.46 % (3377163)Refutation found. Thanks to Tanya!
% 54.68/9.46 % SZS status Theorem for theBenchmark
% 54.68/9.46 % SZS output start Proof for theBenchmark
% See solution above
% 54.68/9.47 % (3377163)------------------------------
% 54.68/9.47 % (3377163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.68/9.47 % (3377163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.68/9.47 % (3377163)CaDiCaL version: 2.1.3
% 54.68/9.47 % (3377163)Termination reason: Refutation
% 54.68/9.47 % (3377163)Time elapsed: 8.880 s
% 54.68/9.47 % (3377163)Peak memory usage: 69 MB
% 54.68/9.47 % (3377163)Instructions burned: 14350 (million)
% 54.68/9.47 % (3377157)Success in time 9.223 s
% 54.68/9.47 % Vampire exiting
%------------------------------------------------------------------------------