%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP778+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 10:16:11 AM UTC 2026
% Result : Theorem 94.00s 20.71s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 98
% Number of leaves : 14
% Syntax : Number of formulae : 807 ( 792 unt; 0 def)
% Number of atoms : 826 ( 796 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 40 ( 21 ~; 15 |; 2 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 2497 (2497 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : difference(X1,product(X1,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos01) ).
fof(f2,axiom,
! [X0,X1] : product(X1,difference(X1,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos02) ).
fof(f3,axiom,
! [X0,X1] : quotient(product(X1,X0),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos03) ).
fof(f4,axiom,
! [X0,X1] : product(quotient(X1,X0),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos04) ).
fof(f5,axiom,
! [X0,X1,X2,X3] : product(product(X3,X2),product(X1,X0)) = product(product(X3,X1),product(X2,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos05) ).
fof(f6,axiom,
! [X0] : product(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos06) ).
fof(f7,axiom,
! [X0,X1] : product(product(product(X1,X0),X0),product(X0,product(X0,X1))) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos07) ).
fof(f8,axiom,
! [X0,X1,X2] :
( d(X0,X1,X2)
<=> product(X0,X1) = product(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos08) ).
fof(f9,axiom,
! [X0,X1,X2] :
( m(X0,X1,X2)
<=> product(product(X0,X1),product(X1,X2)) = product(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos09) ).
fof(f10,axiom,
d(a1,b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos10) ).
fof(f11,axiom,
d(a,b1,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos11) ).
fof(f12,axiom,
d(a,b,c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos12) ).
fof(f14,axiom,
d(a1,b2,c1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos14) ).
fof(f16,conjecture,
m(b1,b,b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f17,negated_conjecture,
~ m(b1,b,b2),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f18,plain,
~ m(b1,b,b2),
inference(flattening,[],[f17]) ).
fof(f19,plain,
! [X0,X1,X2] :
( ( d(X0,X1,X2)
| product(X0,X1) != product(X1,X2) )
& ( product(X0,X1) = product(X1,X2)
| ~ d(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f20,plain,
! [X0,X1,X2] :
( ( m(X0,X1,X2)
| product(product(X0,X1),product(X1,X2)) != product(X0,X2) )
& ( product(product(X0,X1),product(X1,X2)) = product(X0,X2)
| ~ m(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f21,plain,
! [X0,X1] : difference(X1,product(X1,X0)) = X0,
inference(cnf_transformation,[],[f1]) ).
fof(f22,plain,
! [X0,X1] : product(X1,difference(X1,X0)) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
! [X0,X1] : quotient(product(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f3]) ).
fof(f24,plain,
! [X0,X1] : product(quotient(X1,X0),X0) = X1,
inference(cnf_transformation,[],[f4]) ).
fof(f25,plain,
! [X2,X3,X0,X1] : product(product(X3,X2),product(X1,X0)) = product(product(X3,X1),product(X2,X0)),
inference(cnf_transformation,[],[f5]) ).
fof(f26,plain,
! [X0] : product(X0,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f27,plain,
! [X0,X1] : product(product(product(X1,X0),X0),product(X0,product(X0,X1))) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f28,plain,
! [X2,X0,X1] :
( ~ d(X0,X1,X2)
| product(X0,X1) = product(X1,X2) ),
inference(cnf_transformation,[],[f19]) ).
fof(f31,plain,
! [X2,X0,X1] :
( product(product(X0,X1),product(X1,X2)) != product(X0,X2)
| m(X0,X1,X2) ),
inference(cnf_transformation,[],[f20]) ).
fof(f32,plain,
d(a1,b,c),
inference(cnf_transformation,[],[f10]) ).
fof(f33,plain,
d(a,b1,c),
inference(cnf_transformation,[],[f11]) ).
fof(f34,plain,
d(a,b,c1),
inference(cnf_transformation,[],[f12]) ).
fof(f36,plain,
d(a1,b2,c1),
inference(cnf_transformation,[],[f14]) ).
fof(f38,plain,
~ m(b1,b,b2),
inference(cnf_transformation,[],[f18]) ).
fof(f40,plain,
product(a,b1) = product(b1,c),
inference(resolution,[],[f33,f28]) ).
fof(f41,plain,
product(a1,b) = product(b,c),
inference(resolution,[],[f32,f28]) ).
fof(f42,plain,
product(a1,b2) = product(b2,c1),
inference(resolution,[],[f36,f28]) ).
fof(f43,plain,
product(a,b) = product(b,c1),
inference(resolution,[],[f34,f28]) ).
fof(f47,plain,
! [X0] : difference(X0,X0) = X0,
inference(superposition,[],[f21,f26]) ).
fof(f52,plain,
! [X0,X1] : quotient(X0,difference(X1,X0)) = X1,
inference(superposition,[],[f23,f22]) ).
fof(f53,plain,
! [X0] : quotient(X0,X0) = X0,
inference(superposition,[],[f23,f26]) ).
fof(f61,plain,
! [X0,X1] : difference(quotient(X0,X1),X0) = X1,
inference(superposition,[],[f21,f24]) ).
fof(f65,plain,
c = difference(b,product(a1,b)),
inference(superposition,[],[f21,f41]) ).
fof(f70,plain,
a = quotient(product(b,c1),b),
inference(superposition,[],[f23,f43]) ).
fof(f91,plain,
a = quotient(product(b1,c),b1),
inference(superposition,[],[f23,f40]) ).
fof(f129,plain,
! [X2,X3,X0,X1] : product(product(X1,X2),product(difference(X1,X0),X3)) = product(X0,product(X2,X3)),
inference(superposition,[],[f25,f22]) ).
fof(f130,plain,
! [X2,X0,X1] : product(X0,product(X1,X2)) = product(product(X0,X1),product(X0,X2)),
inference(superposition,[],[f25,f26]) ).
fof(f133,plain,
! [X2,X3,X0,X1] : product(X0,product(X2,X3)) = product(product(quotient(X0,X1),X2),product(X1,X3)),
inference(superposition,[],[f25,f24]) ).
fof(f140,plain,
! [X2,X3,X0,X1] : product(product(X1,X2),product(X3,difference(X2,X0))) = product(product(X1,X3),X0),
inference(superposition,[],[f25,f22]) ).
fof(f141,plain,
! [X2,X0,X1] : product(product(X1,X2),X0) = product(product(X1,X0),product(X2,X0)),
inference(superposition,[],[f25,f26]) ).
fof(f144,plain,
! [X2,X3,X0,X1] : product(product(X1,X3),X0) = product(product(X1,quotient(X0,X2)),product(X3,X2)),
inference(superposition,[],[f25,f24]) ).
fof(f157,plain,
! [X2,X3,X0,X1] : product(X1,X3) = difference(product(X0,X2),product(product(X0,X1),product(X2,X3))),
inference(superposition,[],[f21,f25]) ).
fof(f158,plain,
! [X2,X3,X0,X1] : product(X0,X2) = quotient(product(product(X0,X1),product(X2,X3)),product(X1,X3)),
inference(superposition,[],[f23,f25]) ).
fof(f185,plain,
! [X0,X1] : quotient(X0,X1) = product(product(product(X1,quotient(X0,X1)),quotient(X0,X1)),product(quotient(X0,X1),X0)),
inference(superposition,[],[f27,f24]) ).
fof(f193,plain,
! [X0,X1] : product(X0,product(X0,X1)) = difference(product(product(X1,X0),X0),X0),
inference(superposition,[],[f21,f27]) ).
fof(f194,plain,
! [X0,X1] : product(product(X1,X0),X0) = quotient(X0,product(X0,product(X0,X1))),
inference(superposition,[],[f23,f27]) ).
fof(f228,plain,
! [X0,X1] : product(X1,product(X1,quotient(X0,X1))) = difference(product(X0,X1),X1),
inference(superposition,[],[f193,f24]) ).
fof(f242,plain,
! [X0,X1] : product(product(difference(X1,X0),X1),X1) = quotient(X1,product(X1,X0)),
inference(superposition,[],[f194,f22]) ).
fof(f265,plain,
! [X2,X3,X0,X1] : product(quotient(X0,X1),X2) = quotient(product(X0,product(X2,X3)),product(X1,X3)),
inference(superposition,[],[f158,f24]) ).
fof(f277,plain,
! [X2,X3,X0,X1] : product(X1,quotient(X0,X2)) = quotient(product(product(X1,X3),X0),product(X3,X2)),
inference(superposition,[],[f158,f24]) ).
fof(f334,plain,
! [X2,X3,X0,X1] : product(difference(X1,X0),X2) = difference(product(X1,X3),product(X0,product(X3,X2))),
inference(superposition,[],[f157,f22]) ).
fof(f346,plain,
! [X2,X3,X0,X1] : product(X1,difference(X2,X0)) = difference(product(X3,X2),product(product(X3,X1),X0)),
inference(superposition,[],[f157,f22]) ).
fof(f383,plain,
! [X0,X1] : product(X1,quotient(X0,X1)) = difference(X1,difference(product(X0,X1),X1)),
inference(superposition,[],[f21,f228]) ).
fof(f418,plain,
! [X0,X1] : product(product(X0,X1),X0) = product(X0,product(X1,X0)),
inference(superposition,[],[f141,f26]) ).
fof(f424,plain,
! [X2,X0,X1] : product(X0,product(X2,X1)) = product(product(quotient(X0,X1),X2),X1),
inference(superposition,[],[f141,f24]) ).
fof(f431,plain,
! [X2,X0,X1] : product(product(X1,X2),difference(X2,X0)) = product(product(X1,difference(X2,X0)),X0),
inference(superposition,[],[f141,f22]) ).
fof(f437,plain,
! [X2,X0,X1] : product(product(X1,X2),X0) = product(product(X1,quotient(X0,X2)),X2),
inference(superposition,[],[f141,f24]) ).
fof(f509,plain,
! [X2,X0,X1] : product(X0,product(X1,X2)) = product(X1,product(difference(X1,X0),X2)),
inference(superposition,[],[f130,f22]) ).
fof(f516,plain,
! [X2,X0,X1] : product(quotient(X0,X1),product(X1,X2)) = product(X0,product(quotient(X0,X1),X2)),
inference(superposition,[],[f130,f24]) ).
fof(f523,plain,
! [X2,X0,X1] : product(product(X1,X2),X0) = product(X1,product(X2,difference(X1,X0))),
inference(superposition,[],[f130,f22]) ).
fof(f531,plain,
! [X2,X0,X1] : product(quotient(X0,X1),product(X2,X1)) = product(product(quotient(X0,X1),X2),X0),
inference(superposition,[],[f130,f24]) ).
fof(f694,plain,
! [X2,X0,X1] : product(X0,quotient(X2,X1)) = quotient(product(product(X0,X1),X2),X1),
inference(superposition,[],[f23,f437]) ).
fof(f747,plain,
! [X2,X3,X0,X1] : product(X0,product(X2,X3)) = product(X1,product(difference(quotient(X1,X2),X0),X3)),
inference(superposition,[],[f133,f22]) ).
fof(f751,plain,
! [X2,X3,X0,X1] : product(X1,product(X2,difference(X3,X0))) = product(product(quotient(X1,X3),X2),X0),
inference(superposition,[],[f133,f22]) ).
fof(f834,plain,
! [X2,X0,X1] : product(X1,product(quotient(X1,X2),difference(X2,X0))) = product(quotient(X1,X2),X0),
inference(superposition,[],[f516,f22]) ).
fof(f1016,plain,
! [X2,X3,X0,X1] : product(X0,product(difference(X1,X2),X3)) = product(X2,product(difference(X1,X0),X3)),
inference(superposition,[],[f129,f22]) ).
fof(f1148,plain,
! [X2,X0,X1] : product(X2,difference(X0,X1)) = product(X1,product(difference(X0,X2),difference(X0,X1))),
inference(superposition,[],[f1016,f26]) ).
fof(f1186,plain,
! [X2,X3,X0,X1,X4] : product(product(X2,X4),product(difference(X1,X0),X3)) = product(product(X0,product(difference(X1,X2),X3)),product(X4,product(difference(X1,X0),X3))),
inference(superposition,[],[f141,f1016]) ).
fof(f1221,plain,
! [X2,X3,X0,X1] : product(difference(X1,X0),X3) = difference(X2,product(X0,product(difference(X1,X2),X3))),
inference(superposition,[],[f21,f1016]) ).
fof(f1233,plain,
! [X2,X3,X0,X1,X4] : product(X2,product(X4,product(difference(X1,X0),X3))) = product(product(X2,X4),product(X0,product(difference(X1,X2),X3))),
inference(superposition,[],[f130,f1016]) ).
fof(f1292,plain,
! [X2,X3,X0,X1,X4] : product(product(X2,X4),product(difference(X1,X0),X3)) = product(X0,product(product(difference(X1,X2),X3),product(difference(X1,X4),X3))),
inference(forward_demodulation,[],[f1186,f1233]) ).
fof(f1316,plain,
! [X2,X3,X0,X1,X4] : product(product(X2,X4),product(difference(X1,X0),X3)) = product(X0,product(product(difference(X1,X2),difference(X1,X4)),X3)),
inference(forward_demodulation,[],[f1292,f141]) ).
fof(f1361,plain,
! [X2,X3,X0,X1] : product(product(X1,X2),X0) = product(product(X1,quotient(X0,difference(X2,X3))),X3),
inference(superposition,[],[f140,f24]) ).
fof(f1703,plain,
! [X0,X1] : product(difference(X0,X1),X0) = quotient(quotient(X0,product(X0,X1)),X0),
inference(superposition,[],[f23,f242]) ).
fof(f1717,plain,
! [X2,X0,X1] : product(product(product(difference(X0,X1),X0),X2),X0) = product(quotient(X0,product(X0,X1)),product(X2,X0)),
inference(superposition,[],[f141,f242]) ).
fof(f1816,plain,
! [X2,X3,X0,X1] : product(product(X1,quotient(X0,X2)),X3) = product(product(X1,quotient(X3,X2)),X0),
inference(superposition,[],[f144,f24]) ).
fof(f1974,plain,
! [X2,X3,X0,X1] : product(quotient(X0,X1),quotient(X2,X3)) = quotient(product(X0,X2),product(X1,X3)),
inference(superposition,[],[f277,f24]) ).
fof(f1986,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(product(X1,difference(X3,X2)),X4)) = quotient(product(product(X0,X1),X2),product(X3,X4)),
inference(superposition,[],[f277,f140]) ).
fof(f2001,plain,
! [X2,X3,X0,X1] : product(X1,quotient(X2,difference(X3,X0))) = quotient(product(product(X1,X3),X2),X0),
inference(superposition,[],[f277,f22]) ).
fof(f2020,plain,
! [X2,X3,X0,X1] : product(X1,quotient(X2,X3)) = quotient(product(product(X1,quotient(X0,X3)),X2),X0),
inference(superposition,[],[f277,f24]) ).
fof(f2050,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(product(X1,difference(X3,X2)),X4)) = product(X0,quotient(X2,difference(X1,product(X3,X4)))),
inference(forward_demodulation,[],[f1986,f2001]) ).
fof(f2401,plain,
! [X2,X3,X0,X1] : quotient(product(X0,product(X1,X2)),product(X3,X2)) = product(quotient(X1,X3),difference(X1,X0)),
inference(superposition,[],[f265,f509]) ).
fof(f2403,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X2,X4),difference(X1,X0)) = quotient(product(X0,product(difference(X1,X2),X3)),product(X4,X3)),
inference(superposition,[],[f265,f1016]) ).
fof(f2407,plain,
! [X2,X3,X0,X1] : quotient(product(X0,product(X1,X2)),product(X3,X2)) = product(quotient(product(X0,X1),X3),X0),
inference(superposition,[],[f265,f130]) ).
fof(f2413,plain,
! [X2,X3,X0,X1,X4] : quotient(product(X0,product(X1,X2)),product(X4,X2)) = product(quotient(product(X3,X1),X4),difference(X3,X0)),
inference(superposition,[],[f265,f129]) ).
fof(f2441,plain,
! [X2,X3,X0,X1] : product(quotient(X1,quotient(X0,X2)),X3) = quotient(product(X1,product(X3,X2)),X0),
inference(superposition,[],[f265,f24]) ).
fof(f2500,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X3,X1),X4),difference(X3,X0)) = product(quotient(X0,X4),quotient(product(X1,X2),X2)),
inference(forward_demodulation,[],[f2413,f1974]) ).
fof(f2505,plain,
! [X2,X3,X0,X1] : product(quotient(X0,X3),quotient(product(X1,X2),X2)) = product(quotient(product(X0,X1),X3),X0),
inference(forward_demodulation,[],[f2407,f1974]) ).
fof(f2509,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X2,X4),difference(X1,X0)) = product(quotient(X0,X4),quotient(product(difference(X1,X2),X3),X3)),
inference(forward_demodulation,[],[f2403,f1974]) ).
fof(f2511,plain,
! [X2,X3,X0,X1] : product(quotient(X0,X3),quotient(product(X1,X2),X2)) = product(quotient(X1,X3),difference(X1,X0)),
inference(forward_demodulation,[],[f2401,f1974]) ).
fof(f2558,plain,
! [X3,X0,X1,X4] : product(quotient(X0,X4),X1) = product(quotient(product(X3,X1),X4),difference(X3,X0)),
inference(forward_demodulation,[],[f2500,f23]) ).
fof(f2563,plain,
! [X3,X0,X1] : product(quotient(X0,X3),X1) = product(quotient(product(X0,X1),X3),X0),
inference(forward_demodulation,[],[f2505,f23]) ).
fof(f2567,plain,
! [X2,X0,X1,X4] : product(quotient(X2,X4),difference(X1,X0)) = product(quotient(X0,X4),difference(X1,X2)),
inference(forward_demodulation,[],[f2509,f23]) ).
fof(f2569,plain,
! [X3,X0,X1] : product(quotient(X0,X3),X1) = product(quotient(X1,X3),difference(X1,X0)),
inference(forward_demodulation,[],[f2511,f23]) ).
fof(f2629,plain,
! [X2,X0,X1] : product(X0,difference(X2,X1)) = product(quotient(X1,difference(X0,X2)),X2),
inference(superposition,[],[f2569,f52]) ).
fof(f2646,plain,
! [X2,X3,X0,X1,X4] : product(product(X3,quotient(X2,X1)),product(X4,difference(X2,X0))) = product(product(X3,X4),product(quotient(X0,X1),X2)),
inference(superposition,[],[f25,f2569]) ).
fof(f2919,plain,
! [X2,X3,X0,X1] : product(X1,difference(difference(X2,X0),X3)) = difference(X0,product(product(X2,X1),X3)),
inference(superposition,[],[f346,f22]) ).
fof(f2920,plain,
! [X2,X0,X1] : product(X1,difference(X0,X2)) = difference(X0,product(product(X0,X1),X2)),
inference(superposition,[],[f346,f26]) ).
fof(f2949,plain,
! [X2,X3,X0,X1] : product(difference(X1,X0),difference(X2,X3)) = difference(product(X1,X2),product(X0,X3)),
inference(superposition,[],[f346,f22]) ).
fof(f2950,plain,
! [X2,X0,X1] : product(X0,difference(X1,X2)) = difference(product(X0,X1),product(X0,X2)),
inference(superposition,[],[f346,f26]) ).
fof(f2970,plain,
! [X2,X3,X0,X1] : product(X1,difference(X2,X3)) = difference(product(quotient(X0,X1),X2),product(X0,X3)),
inference(superposition,[],[f346,f24]) ).
fof(f2983,plain,
! [X2,X3,X0,X1,X4] : product(X2,difference(X4,product(X1,X3))) = difference(product(X0,X4),product(product(X0,X1),product(X2,X3))),
inference(superposition,[],[f346,f25]) ).
fof(f2984,plain,
! [X2,X3,X0,X1] : difference(product(X0,X3),product(product(X0,X1),X2)) = product(X2,difference(X3,product(X1,X2))),
inference(superposition,[],[f346,f141]) ).
fof(f2990,plain,
! [X2,X3,X0,X1] : difference(product(X0,X3),product(product(X0,X1),X2)) = product(quotient(X2,X1),difference(X3,X1)),
inference(superposition,[],[f346,f437]) ).
fof(f2992,plain,
! [X2,X3,X0,X1] : product(X1,difference(X2,difference(product(X3,X1),X0))) = difference(product(X3,X2),X0),
inference(superposition,[],[f346,f22]) ).
fof(f3021,plain,
! [X2,X3,X1] : product(X1,difference(X3,X2)) = product(quotient(X2,X1),difference(X3,X1)),
inference(forward_demodulation,[],[f2990,f346]) ).
fof(f3024,plain,
! [X2,X3,X1] : product(X1,difference(X3,X2)) = product(X2,difference(X3,product(X1,X2))),
inference(forward_demodulation,[],[f2984,f346]) ).
fof(f3025,plain,
! [X2,X3,X1,X4] : product(X2,difference(X4,product(X1,X3))) = product(X1,difference(X4,product(X2,X3))),
inference(forward_demodulation,[],[f2983,f346]) ).
fof(f3101,plain,
! [X2,X0,X1] : difference(X1,product(X0,X2)) = product(difference(X1,X0),difference(X1,X2)),
inference(superposition,[],[f2920,f22]) ).
fof(f3104,plain,
! [X2,X3,X0,X1] : product(product(difference(X1,X0),X2),difference(X1,X3)) = difference(X1,product(product(X0,product(X1,X2)),X3)),
inference(superposition,[],[f2920,f509]) ).
fof(f3122,plain,
! [X2,X0,X1] : difference(quotient(X0,X1),product(X0,X2)) = product(X1,difference(quotient(X0,X1),X2)),
inference(superposition,[],[f2920,f24]) ).
fof(f3204,plain,
! [X2,X3,X0,X1] : product(product(difference(X1,X0),X2),difference(X1,X3)) = product(product(X1,X2),difference(difference(X0,X1),X3)),
inference(forward_demodulation,[],[f3104,f2919]) ).
fof(f3245,plain,
! [X0,X1] : product(difference(X0,X1),X0) = difference(X0,product(X1,X0)),
inference(superposition,[],[f3101,f47]) ).
fof(f3247,plain,
! [X2,X0,X1] : difference(product(product(X1,X0),X0),product(X2,X0)) = product(difference(product(product(X1,X0),X0),X2),product(X0,product(X0,X1))),
inference(superposition,[],[f3101,f193]) ).
fof(f3261,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,X1),X3),product(difference(X0,X2),X4)) = product(difference(X0,product(X1,X2)),product(X3,X4)),
inference(superposition,[],[f25,f3101]) ).
fof(f3326,plain,
! [X2,X0,X1] : product(difference(product(product(X1,X0),X0),X2),product(X0,product(X0,X1))) = product(difference(product(X1,X0),X2),difference(X0,X0)),
inference(forward_demodulation,[],[f3247,f2949]) ).
fof(f3349,plain,
! [X2,X0,X1] : product(difference(product(product(X1,X0),X0),X2),product(X0,product(X0,X1))) = product(difference(product(X1,X0),X2),X0),
inference(forward_demodulation,[],[f3326,f47]) ).
fof(f3394,plain,
! [X0,X1] : product(difference(X0,product(difference(X0,X1),X0)),X0) = difference(X0,quotient(X0,product(X0,X1))),
inference(superposition,[],[f3245,f242]) ).
fof(f3396,plain,
! [X0,X1] : difference(X1,X0) = product(difference(X1,quotient(X0,X1)),X1),
inference(superposition,[],[f3245,f24]) ).
fof(f3448,plain,
! [X0,X1] : product(product(difference(X0,difference(X0,X1)),X0),X0) = difference(X0,quotient(X0,product(X0,X1))),
inference(forward_demodulation,[],[f3394,f3245]) ).
fof(f3474,plain,
! [X0,X1] : quotient(X0,product(X0,difference(X0,X1))) = difference(X0,quotient(X0,product(X0,X1))),
inference(forward_demodulation,[],[f3448,f242]) ).
fof(f3494,plain,
! [X0,X1] : quotient(X0,X1) = difference(X0,quotient(X0,product(X0,X1))),
inference(forward_demodulation,[],[f3474,f22]) ).
fof(f3535,plain,
! [X2,X0,X1] : product(X1,difference(difference(X1,X0),X2)) = difference(X0,product(X1,X2)),
inference(superposition,[],[f2950,f22]) ).
fof(f3566,plain,
! [X2,X0,X1] : difference(product(X1,X2),X0) = product(X1,difference(X2,difference(X1,X0))),
inference(superposition,[],[f2950,f22]) ).
fof(f3567,plain,
! [X0,X1] : product(X0,difference(X1,X0)) = difference(product(X0,X1),X0),
inference(superposition,[],[f2950,f26]) ).
fof(f3588,plain,
! [X2,X0,X1] : product(quotient(X0,X1),difference(X2,X1)) = difference(product(quotient(X0,X1),X2),X0),
inference(superposition,[],[f2950,f24]) ).
fof(f3633,plain,
! [X2,X0,X1] : product(X1,difference(X2,X0)) = difference(product(quotient(X0,X1),X2),X0),
inference(forward_demodulation,[],[f3588,f3021]) ).
fof(f3735,plain,
! [X2,X0,X1] : difference(product(X0,X2),X1) = product(difference(X0,X1),difference(X2,X1)),
inference(superposition,[],[f3633,f52]) ).
fof(f3741,plain,
! [X2,X0,X1] : difference(X0,X2) = product(X1,difference(difference(quotient(X2,X1),X0),X2)),
inference(superposition,[],[f3633,f22]) ).
fof(f3972,plain,
! [X2,X0,X1] : difference(product(X1,X2),product(X2,X0)) = product(difference(X1,product(X2,X0)),X0),
inference(superposition,[],[f3735,f21]) ).
fof(f3975,plain,
! [X0,X1] : difference(product(X1,X0),X0) = product(difference(X1,X0),X0),
inference(superposition,[],[f3735,f47]) ).
fof(f3976,plain,
! [X2,X0,X1] : product(difference(X1,X2),X0) = difference(product(X1,quotient(X2,X0)),X2),
inference(superposition,[],[f3735,f61]) ).
fof(f3982,plain,
! [X2,X3,X0,X1] : difference(product(X3,product(quotient(X2,X0),X1)),X2) = product(difference(X3,X2),product(X0,difference(X1,X2))),
inference(superposition,[],[f3735,f3633]) ).
fof(f4074,plain,
! [X2,X0,X1] : product(difference(X1,product(X2,X0)),X0) = product(difference(X1,X2),difference(X2,X0)),
inference(forward_demodulation,[],[f3972,f2949]) ).
fof(f4143,plain,
! [X0,X1] : difference(X0,difference(X1,X0)) = product(difference(X1,difference(X1,X0)),difference(X1,X0)),
inference(superposition,[],[f3975,f22]) ).
fof(f4159,plain,
! [X0,X1] : difference(X0,product(X0,product(X0,X1))) = product(difference(product(product(X1,X0),X0),product(X0,product(X0,X1))),product(X0,product(X0,X1))),
inference(superposition,[],[f3975,f27]) ).
fof(f4166,plain,
! [X0,X1] : difference(X0,X1) = product(difference(quotient(X0,X1),X1),X1),
inference(superposition,[],[f3975,f24]) ).
fof(f4228,plain,
! [X0,X1] : difference(X0,product(X0,product(X0,X1))) = product(difference(product(X1,X0),product(X0,product(X0,X1))),X0),
inference(forward_demodulation,[],[f4159,f3349]) ).
fof(f4244,plain,
! [X0,X1] : difference(X0,difference(X1,X0)) = difference(X1,product(difference(X1,X0),X0)),
inference(forward_demodulation,[],[f4143,f3101]) ).
fof(f4260,plain,
! [X0,X1] : product(product(difference(X1,X0),X1),X0) = difference(X0,product(X0,product(X0,X1))),
inference(forward_demodulation,[],[f4228,f334]) ).
fof(f4283,plain,
! [X0,X1] : product(X0,X1) = product(product(difference(X1,X0),X1),X0),
inference(forward_demodulation,[],[f4260,f21]) ).
fof(f4323,plain,
! [X0,X1] : product(product(X0,X1),product(X1,X0)) = product(product(X1,X0),X1),
inference(superposition,[],[f4283,f21]) ).
fof(f4327,plain,
! [X0,X1] : product(X1,quotient(X1,X0)) = product(product(X0,quotient(X1,X0)),X1),
inference(superposition,[],[f4283,f61]) ).
fof(f4354,plain,
! [X0,X1] : product(product(X0,X1),X1) = product(product(difference(X1,product(X0,X1)),X0),X1),
inference(superposition,[],[f141,f4283]) ).
fof(f4360,plain,
! [X2,X0,X1] : quotient(product(X0,X1),product(X1,X2)) = product(difference(X1,X0),quotient(X0,X2)),
inference(superposition,[],[f277,f4283]) ).
fof(f4361,plain,
! [X0,X1] : product(X0,quotient(X1,X0)) = product(product(difference(quotient(X1,X0),X0),X0),X1),
inference(superposition,[],[f437,f4283]) ).
fof(f4363,plain,
! [X0,X1] : difference(product(difference(X1,X0),X1),product(X0,X1)) = X0,
inference(superposition,[],[f21,f4283]) ).
fof(f4364,plain,
! [X0,X1] : product(difference(X1,X0),X1) = quotient(product(X0,X1),X0),
inference(superposition,[],[f23,f4283]) ).
fof(f4386,plain,
! [X2,X3,X0,X1] : product(X2,product(difference(X1,X0),X1)) = quotient(product(product(X2,X3),product(X0,X1)),product(X3,X0)),
inference(superposition,[],[f158,f4283]) ).
fof(f4429,plain,
! [X2,X3,X0,X1] : product(X2,product(difference(X1,X0),X1)) = product(quotient(product(X2,X3),X3),quotient(product(X0,X1),X0)),
inference(forward_demodulation,[],[f4386,f1974]) ).
fof(f4441,plain,
! [X0,X1] : product(difference(difference(X1,X0),X0),difference(X1,X1)) = X0,
inference(forward_demodulation,[],[f4363,f2949]) ).
fof(f4442,plain,
! [X0,X1] : product(difference(X1,X0),X1) = product(X0,quotient(X1,X0)),
inference(forward_demodulation,[],[f4361,f4166]) ).
fof(f4443,plain,
! [X2,X0,X1] : product(difference(X1,X0),quotient(X0,X2)) = product(quotient(X0,X1),quotient(X1,X2)),
inference(forward_demodulation,[],[f4360,f1974]) ).
fof(f4448,plain,
! [X0,X1] : product(product(X0,X1),X1) = product(product(product(difference(X1,X0),X1),X0),X1),
inference(forward_demodulation,[],[f4354,f3245]) ).
fof(f4467,plain,
! [X0,X1] : product(product(X0,X1),product(X1,X0)) = product(X1,product(X0,X1)),
inference(forward_demodulation,[],[f4323,f418]) ).
fof(f4477,plain,
! [X2,X0,X1] : product(X2,product(difference(X1,X0),X1)) = product(X2,quotient(product(X0,X1),X0)),
inference(forward_demodulation,[],[f4429,f23]) ).
fof(f4487,plain,
! [X0,X1] : product(difference(difference(X1,X0),X0),X1) = X0,
inference(forward_demodulation,[],[f4441,f47]) ).
fof(f4491,plain,
! [X0,X1] : product(product(X0,X1),X1) = product(quotient(X1,product(X1,X0)),product(X0,X1)),
inference(forward_demodulation,[],[f4448,f1717]) ).
fof(f4547,plain,
! [X0,X1] : product(difference(X1,X0),X0) = product(X0,product(difference(X1,X0),X1)),
inference(superposition,[],[f4467,f22]) ).
fof(f4554,plain,
! [X0,X1] : product(quotient(X0,product(X0,X1)),product(X0,product(difference(X0,X1),X0))) = product(X0,quotient(X0,product(X0,X1))),
inference(superposition,[],[f4467,f242]) ).
fof(f4571,plain,
! [X0,X1] : product(X1,X0) = product(X0,product(X1,quotient(X0,X1))),
inference(superposition,[],[f4467,f24]) ).
fof(f4639,plain,
! [X0,X1] : product(X1,X0) = quotient(product(X0,product(X1,X0)),product(X0,X1)),
inference(superposition,[],[f23,f4467]) ).
fof(f4711,plain,
! [X0,X1] : product(X1,X0) = product(quotient(X0,X0),quotient(product(X1,X0),X1)),
inference(forward_demodulation,[],[f4639,f1974]) ).
fof(f4779,plain,
! [X0,X1] : product(X0,quotient(X0,product(X0,X1))) = product(quotient(X0,product(X0,X1)),product(X1,product(X0,X0))),
inference(forward_demodulation,[],[f4554,f509]) ).
fof(f4812,plain,
! [X0,X1] : product(X1,X0) = product(X0,quotient(product(X1,X0),X1)),
inference(forward_demodulation,[],[f4711,f53]) ).
fof(f4861,plain,
! [X0,X1] : product(quotient(X0,product(X0,X1)),product(X1,X0)) = product(X0,quotient(X0,product(X0,X1))),
inference(forward_demodulation,[],[f4779,f26]) ).
fof(f4918,plain,
! [X0,X1] : product(product(X1,X0),X0) = product(X0,quotient(X0,product(X0,X1))),
inference(forward_demodulation,[],[f4861,f4491]) ).
fof(f5061,plain,
! [X0,X1] : product(difference(X0,X1),X0) = difference(X1,product(difference(X0,X1),X1)),
inference(superposition,[],[f21,f4547]) ).
fof(f5062,plain,
! [X0,X1] : quotient(product(difference(X0,X1),X1),product(difference(X0,X1),X0)) = X1,
inference(superposition,[],[f23,f4547]) ).
fof(f5165,plain,
! [X0,X1] : product(quotient(difference(X0,X1),difference(X0,X1)),quotient(X1,X0)) = X1,
inference(forward_demodulation,[],[f5062,f1974]) ).
fof(f5166,plain,
! [X0,X1] : product(difference(X0,X1),X0) = product(difference(X1,difference(X0,X1)),X1),
inference(forward_demodulation,[],[f5061,f3245]) ).
fof(f5207,plain,
! [X0,X1] : product(difference(X0,X1),quotient(X1,X0)) = X1,
inference(forward_demodulation,[],[f5165,f53]) ).
fof(f5300,plain,
! [X2,X0,X1] : product(X0,product(X2,X1)) = product(product(difference(X1,X0),X2),X0),
inference(superposition,[],[f144,f5207]) ).
fof(f5302,plain,
! [X0,X1] : quotient(X0,X1) = difference(difference(X1,X0),X0),
inference(superposition,[],[f21,f5207]) ).
fof(f5303,plain,
! [X0,X1] : difference(X1,X0) = quotient(X0,quotient(X0,X1)),
inference(superposition,[],[f23,f5207]) ).
fof(f5458,plain,
! [X0,X1] : product(X0,quotient(X1,X0)) = difference(X1,product(X0,X1)),
inference(superposition,[],[f21,f4571]) ).
fof(f5488,plain,
! [X2,X3,X0,X1] : product(X2,quotient(X3,product(X0,quotient(X1,X0)))) = quotient(product(product(X2,X1),X3),product(X0,X1)),
inference(superposition,[],[f277,f4571]) ).
fof(f5541,plain,
! [X2,X3,X0,X1] : product(X2,quotient(X3,product(X0,quotient(X1,X0)))) = product(quotient(product(X2,X1),X0),quotient(X3,X1)),
inference(forward_demodulation,[],[f5488,f1974]) ).
fof(f5682,plain,
! [X2,X3,X0,X1] : product(difference(product(difference(X1,X0),X3),X2),product(difference(X1,X0),X3)) = quotient(product(X0,product(difference(X1,X2),X3)),X2),
inference(superposition,[],[f4364,f1016]) ).
fof(f5709,plain,
product(difference(c1,b2),c1) = quotient(product(a1,b2),b2),
inference(superposition,[],[f4364,f42]) ).
fof(f5770,plain,
! [X2,X3,X0,X1] : quotient(product(X0,product(difference(X1,X2),X3)),X0) = product(X2,product(difference(X1,difference(product(difference(X1,X2),X3),X0)),X3)),
inference(superposition,[],[f1016,f4364]) ).
fof(f5792,plain,
a = product(difference(c1,b),c1),
inference(superposition,[],[f70,f4364]) ).
fof(f5795,plain,
a = product(b,quotient(c1,b)),
inference(forward_demodulation,[],[f5792,f4442]) ).
fof(f5811,plain,
! [X2,X3,X0,X1] : product(X2,product(difference(X1,difference(product(difference(X1,X2),X3),X0)),X3)) = product(quotient(X0,quotient(X0,X3)),difference(X1,X2)),
inference(forward_demodulation,[],[f5770,f2441]) ).
fof(f5850,plain,
a1 = product(difference(c1,b2),c1),
inference(forward_demodulation,[],[f5709,f23]) ).
fof(f5873,plain,
! [X2,X3,X0,X1] : product(difference(product(difference(X1,X0),X3),X2),product(difference(X1,X0),X3)) = product(quotient(X0,quotient(X2,X3)),difference(X1,X2)),
inference(forward_demodulation,[],[f5682,f2441]) ).
fof(f5893,plain,
! [X2,X3,X0,X1] : product(difference(X3,X0),difference(X1,X2)) = product(X2,product(difference(X1,difference(product(difference(X1,X2),X3),X0)),X3)),
inference(forward_demodulation,[],[f5811,f5303]) ).
fof(f5912,plain,
a1 = product(b2,quotient(c1,b2)),
inference(forward_demodulation,[],[f5850,f4442]) ).
fof(f5929,plain,
! [X2,X3,X0,X1] : product(X0,product(difference(X1,difference(product(difference(X1,X0),X3),X2)),X3)) = product(quotient(X0,quotient(X2,X3)),difference(X1,X2)),
inference(forward_demodulation,[],[f5873,f1016]) ).
fof(f5966,plain,
! [X2,X3,X0,X1] : product(quotient(X0,quotient(X2,X3)),difference(X1,X2)) = product(difference(X3,X2),difference(X1,X0)),
inference(forward_demodulation,[],[f5929,f5893]) ).
fof(f6010,plain,
! [X0,X1] : difference(X0,product(X1,X0)) = quotient(product(X1,X0),X1),
inference(superposition,[],[f5302,f21]) ).
fof(f6019,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = difference(product(X0,difference(X1,X0)),X0),
inference(superposition,[],[f5302,f3567]) ).
fof(f6051,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(X0,difference(difference(X1,X0),X0)),
inference(forward_demodulation,[],[f6019,f3567]) ).
fof(f6063,plain,
! [X0,X1] : quotient(X0,product(X0,X1)) = product(X0,quotient(X0,X1)),
inference(forward_demodulation,[],[f6051,f5302]) ).
fof(f6371,plain,
! [X0,X1] : difference(difference(X1,X0),X0) = product(X1,quotient(difference(X1,X0),X1)),
inference(superposition,[],[f5458,f22]) ).
fof(f6406,plain,
! [X0,X1] : quotient(X0,X1) = difference(X1,difference(X0,product(X1,X0))),
inference(superposition,[],[f21,f5458]) ).
fof(f6407,plain,
! [X0,X1] : quotient(difference(X0,product(X1,X0)),quotient(X0,X1)) = X1,
inference(superposition,[],[f23,f5458]) ).
fof(f6461,plain,
! [X0,X1] : product(X0,quotient(X1,X0)) = quotient(product(X0,X1),X0),
inference(superposition,[],[f6010,f5458]) ).
fof(f6553,plain,
! [X0,X1] : quotient(product(difference(X0,X1),X0),quotient(X0,X1)) = X1,
inference(forward_demodulation,[],[f6407,f3245]) ).
fof(f6554,plain,
! [X0,X1] : quotient(X0,X1) = difference(X1,product(difference(X0,X1),X0)),
inference(forward_demodulation,[],[f6406,f3245]) ).
fof(f6583,plain,
! [X0,X1] : quotient(X0,X1) = product(X1,quotient(difference(X1,X0),X1)),
inference(forward_demodulation,[],[f6371,f5302]) ).
fof(f6791,plain,
! [X0,X1] : product(X1,quotient(X0,X1)) = difference(product(difference(X1,X0),X1),X1),
inference(superposition,[],[f228,f6583]) ).
fof(f6794,plain,
! [X0,X1] : difference(X1,quotient(X0,X1)) = quotient(difference(X1,X0),X1),
inference(superposition,[],[f21,f6583]) ).
fof(f6878,plain,
! [X0,X1] : product(X1,quotient(X0,X1)) = product(difference(difference(X1,X0),X1),X1),
inference(forward_demodulation,[],[f6791,f3975]) ).
fof(f7062,plain,
! [X2,X3,X0,X1] : product(product(difference(X1,X0),X2),X3) = product(product(X0,quotient(X1,X0)),product(X2,difference(X1,X3))),
inference(superposition,[],[f140,f4442]) ).
fof(f7225,plain,
! [X2,X3,X0,X1] : product(product(difference(X1,X0),X2),X3) = product(product(X0,X2),product(quotient(X3,X0),X1)),
inference(forward_demodulation,[],[f7062,f2646]) ).
fof(f7386,plain,
! [X2,X0,X1] : difference(difference(X1,X0),X2) = difference(X1,difference(X0,product(X1,X2))),
inference(superposition,[],[f21,f3535]) ).
fof(f7566,plain,
! [X2,X0,X1] : product(difference(difference(X1,X0),X0),product(X2,X1)) = product(product(difference(difference(X1,X0),X0),X2),X0),
inference(superposition,[],[f130,f4487]) ).
fof(f7641,plain,
! [X2,X0,X1] : product(X0,product(X2,difference(X1,X0))) = product(difference(difference(X1,X0),X0),product(X2,X1)),
inference(forward_demodulation,[],[f7566,f5300]) ).
fof(f7688,plain,
! [X2,X0,X1] : product(X0,product(X2,difference(X1,X0))) = product(quotient(X0,X1),product(X2,X1)),
inference(forward_demodulation,[],[f7641,f5302]) ).
fof(f7980,plain,
difference(b2,a1) = quotient(c1,b2),
inference(superposition,[],[f21,f5912]) ).
fof(f8271,plain,
! [X0,X1] : difference(X1,X0) = difference(quotient(X1,X0),product(X0,X1)),
inference(superposition,[],[f4244,f61]) ).
fof(f8455,plain,
! [X0,X1] : difference(X1,quotient(X0,X1)) = difference(quotient(X1,quotient(X0,X1)),X0),
inference(superposition,[],[f8271,f24]) ).
fof(f8643,plain,
! [X0,X1] : product(difference(X0,X1),X1) = product(product(difference(X0,X1),X0),quotient(product(difference(X0,X1),X1),X1)),
inference(superposition,[],[f4812,f4547]) ).
fof(f8838,plain,
! [X0,X1] : product(difference(X0,X1),X1) = product(product(difference(X0,X1),X0),difference(X0,X1)),
inference(forward_demodulation,[],[f8643,f23]) ).
fof(f8905,plain,
! [X0,X1] : product(difference(X0,X1),X1) = product(product(X0,X0),difference(difference(X1,X0),X1)),
inference(forward_demodulation,[],[f8838,f3204]) ).
fof(f8945,plain,
! [X0,X1] : product(difference(X0,X1),X1) = product(X0,difference(difference(X1,X0),X1)),
inference(forward_demodulation,[],[f8905,f26]) ).
fof(f9758,plain,
! [X2,X0,X1] : difference(difference(X1,X2),product(product(X0,difference(X1,X2)),X2)) = product(product(X0,X1),quotient(difference(X1,X2),product(X0,X1))),
inference(superposition,[],[f5458,f431]) ).
fof(f9884,plain,
! [X2,X0,X1] : product(product(X0,X1),quotient(difference(X1,X2),product(X0,X1))) = product(difference(X1,X2),difference(difference(X0,difference(X1,X2)),X2)),
inference(forward_demodulation,[],[f9758,f2919]) ).
fof(f10044,plain,
! [X2,X0,X1] : product(product(X0,X1),quotient(difference(X1,X2),product(X0,X1))) = difference(product(X1,difference(X0,difference(X1,X2))),X2),
inference(forward_demodulation,[],[f9884,f3735]) ).
fof(f10157,plain,
! [X2,X0,X1] : product(product(X0,X1),quotient(difference(X1,X2),product(X0,X1))) = difference(difference(product(X1,X0),X2),X2),
inference(forward_demodulation,[],[f10044,f3566]) ).
fof(f10229,plain,
! [X2,X0,X1] : quotient(X2,product(X1,X0)) = product(product(X0,X1),quotient(difference(X1,X2),product(X0,X1))),
inference(forward_demodulation,[],[f10157,f5302]) ).
fof(f10339,plain,
! [X2,X0,X1] : difference(product(X0,difference(X2,difference(X0,X1))),X1) = product(X0,quotient(difference(X0,X1),X2)),
inference(superposition,[],[f3566,f5302]) ).
fof(f10349,plain,
! [X2,X0,X1] : difference(X0,difference(product(X0,X1),X2)) = difference(X1,difference(X0,X2)),
inference(superposition,[],[f21,f3566]) ).
fof(f10439,plain,
! [X2,X0,X1] : product(X0,quotient(difference(X0,X1),X2)) = difference(difference(product(X0,X2),X1),X1),
inference(forward_demodulation,[],[f10339,f3566]) ).
fof(f10470,plain,
! [X2,X0,X1] : quotient(X1,product(X0,X2)) = product(X0,quotient(difference(X0,X1),X2)),
inference(forward_demodulation,[],[f10439,f5302]) ).
fof(f10523,plain,
! [X2,X3,X0,X1] : quotient(product(difference(X1,X0),X2),X3) = difference(X3,product(X0,product(difference(X1,difference(product(difference(X1,X0),X2),X3)),X2))),
inference(superposition,[],[f6554,f1016]) ).
fof(f10542,plain,
! [X2,X0,X1] : product(difference(X1,X2),quotient(X0,X1)) = difference(X1,product(X2,product(difference(X0,X1),X0))),
inference(superposition,[],[f3101,f6554]) ).
fof(f10563,plain,
! [X2,X0,X1] : product(difference(X0,X2),X0) = product(difference(X1,X2),quotient(X0,X1)),
inference(forward_demodulation,[],[f10542,f1221]) ).
fof(f10573,plain,
! [X2,X3,X0,X1] : quotient(product(difference(X1,X0),X2),X3) = difference(X3,product(difference(X2,X3),difference(X1,X0))),
inference(forward_demodulation,[],[f10523,f5893]) ).
fof(f11012,plain,
! [X2,X0,X1] : product(X0,X1) = product(difference(X2,product(X1,X0)),quotient(X1,X2)),
inference(superposition,[],[f10563,f21]) ).
fof(f11036,plain,
! [X2,X0,X1] : product(X0,quotient(X1,X2)) = product(difference(X1,product(X2,X0)),X1),
inference(superposition,[],[f10563,f21]) ).
fof(f11140,plain,
! [X2,X3,X0,X1] : product(product(difference(X2,X1),X3),X0) = product(product(difference(X0,X1),X0),product(X3,X2)),
inference(superposition,[],[f144,f10563]) ).
fof(f11676,plain,
! [X2,X0,X1] : product(X1,quotient(X2,X0)) = quotient(product(product(X0,X1),X2),product(X0,X1)),
inference(superposition,[],[f2020,f4812]) ).
fof(f11680,plain,
! [X2,X3,X0,X1,X4] : product(product(quotient(X0,quotient(X2,X3)),X1),quotient(X4,X3)) = quotient(product(product(X0,product(X1,quotient(X2,X3))),X4),X2),
inference(superposition,[],[f2020,f424]) ).
fof(f11690,plain,
! [X2,X3,X0,X1] : quotient(product(X0,X3),X1) = product(quotient(X0,quotient(X1,X2)),quotient(X3,X2)),
inference(superposition,[],[f2020,f24]) ).
fof(f11795,plain,
! [X2,X3,X0,X1,X4] : product(product(quotient(X0,quotient(X2,X3)),X1),quotient(X4,X3)) = product(X0,quotient(X4,difference(product(X1,quotient(X2,X3)),X2))),
inference(forward_demodulation,[],[f11680,f2001]) ).
fof(f11798,plain,
! [X2,X0,X1] : product(X1,quotient(X2,X0)) = product(quotient(product(X0,X1),X0),quotient(X2,X1)),
inference(forward_demodulation,[],[f11676,f1974]) ).
fof(f11828,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(X4,product(difference(X1,X2),X3))) = product(product(quotient(X0,quotient(X2,X3)),X1),quotient(X4,X3)),
inference(forward_demodulation,[],[f11795,f3976]) ).
fof(f11830,plain,
! [X2,X0,X1] : product(X1,quotient(X2,X0)) = product(product(X0,quotient(X1,X0)),quotient(X2,X1)),
inference(forward_demodulation,[],[f11798,f6461]) ).
fof(f11846,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(X4,product(difference(X1,X2),X3))) = product(X0,product(X1,difference(quotient(X2,X3),quotient(X4,X3)))),
inference(forward_demodulation,[],[f11828,f751]) ).
fof(f11863,plain,
! [X2,X0,X1] : quotient(product(X1,X2),X0) = product(quotient(X1,X0),quotient(X2,X0)),
inference(superposition,[],[f11690,f53]) ).
fof(f11865,plain,
! [X2,X3,X0,X1] : quotient(product(X1,X2),X3) = product(quotient(X1,X0),quotient(X2,difference(X0,X3))),
inference(superposition,[],[f11690,f52]) ).
fof(f11885,plain,
! [X2,X0,X1] : quotient(product(X1,X0),X2) = product(quotient(X1,quotient(X2,X0)),X0),
inference(superposition,[],[f11690,f53]) ).
fof(f11908,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X0,quotient(X2,X3)),quotient(X4,X3)) = quotient(product(quotient(product(X0,X1),X2),X4),X1),
inference(superposition,[],[f2020,f11690]) ).
fof(f11909,plain,
! [X2,X3,X0,X1,X4] : product(product(quotient(X0,quotient(X2,X3)),X4),X1) = product(quotient(product(X0,X1),X2),product(X4,X3)),
inference(superposition,[],[f144,f11690]) ).
fof(f11910,plain,
! [X2,X3,X0,X1] : product(quotient(product(X0,X1),X2),X3) = product(product(quotient(X0,quotient(X2,X3)),X3),X1),
inference(superposition,[],[f437,f11690]) ).
fof(f11927,plain,
! [X2,X3,X0,X1,X4] : product(product(quotient(X0,quotient(X2,X3)),X4),quotient(X1,X3)) = product(quotient(product(X0,X1),X2),product(X4,quotient(X1,X3))),
inference(superposition,[],[f141,f11690]) ).
fof(f11979,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X0,X1),X2),product(X4,quotient(X1,X3))) = product(X0,product(X4,difference(quotient(X2,X3),quotient(X1,X3)))),
inference(forward_demodulation,[],[f11927,f751]) ).
fof(f11988,plain,
! [X2,X3,X0,X1] : product(quotient(product(X0,X1),X2),X3) = product(X0,product(X3,difference(quotient(X2,X3),X1))),
inference(forward_demodulation,[],[f11910,f751]) ).
fof(f11989,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X0,X1),X2),product(X4,X3)) = product(X0,product(X4,difference(quotient(X2,X3),X1))),
inference(forward_demodulation,[],[f11909,f751]) ).
fof(f11990,plain,
! [X2,X0,X1,X4] : quotient(product(quotient(product(X0,X1),X2),X4),X1) = quotient(product(X0,X4),X2),
inference(forward_demodulation,[],[f11908,f11690]) ).
fof(f12022,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X0,X1),X2),product(X4,quotient(X1,X3))) = product(X0,quotient(X1,product(difference(X4,X2),X3))),
inference(forward_demodulation,[],[f11979,f11846]) ).
fof(f12033,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(X1,product(difference(X4,X2),X3))) = product(X0,product(X4,difference(quotient(X2,quotient(X1,X3)),X1))),
inference(forward_demodulation,[],[f12022,f11989]) ).
fof(f12057,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,product(X2,X3)),X4),product(X1,X3)) = product(product(quotient(X0,X1),X2),quotient(X4,product(X1,X3))),
inference(superposition,[],[f11863,f265]) ).
fof(f12066,plain,
! [X2,X0,X1] : product(quotient(X2,quotient(X1,X0)),difference(X0,X1)) = quotient(product(X2,X1),quotient(X1,X0)),
inference(superposition,[],[f11863,f5303]) ).
fof(f12189,plain,
! [X2,X0,X1] : product(difference(X0,X1),difference(X0,X2)) = quotient(product(X2,X1),quotient(X1,X0)),
inference(forward_demodulation,[],[f12066,f5966]) ).
fof(f12197,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,product(X2,X3)),X4),product(X1,X3)) = product(X0,product(X2,difference(X1,quotient(X4,product(X1,X3))))),
inference(forward_demodulation,[],[f12057,f751]) ).
fof(f12239,plain,
! [X2,X0,X1] : difference(X0,product(X1,X2)) = quotient(product(X2,X1),quotient(X1,X0)),
inference(forward_demodulation,[],[f12189,f3101]) ).
fof(f12241,plain,
! [X2,X3,X0,X1,X4] : product(X0,product(X2,difference(X1,quotient(X4,product(X1,X3))))) = product(quotient(product(X0,product(X2,X3)),X1),quotient(X4,X3)),
inference(forward_demodulation,[],[f12197,f1974]) ).
fof(f12266,plain,
! [X2,X3,X0,X1,X4] : product(X0,product(X2,difference(X1,quotient(X4,product(X1,X3))))) = product(product(quotient(X0,quotient(X1,X3)),X2),quotient(X4,X3)),
inference(forward_demodulation,[],[f12241,f2441]) ).
fof(f12275,plain,
! [X2,X3,X0,X1,X4] : product(X0,product(X2,difference(X1,quotient(X4,product(X1,X3))))) = product(X0,product(X2,difference(quotient(X1,X3),quotient(X4,X3)))),
inference(forward_demodulation,[],[f12266,f751]) ).
fof(f12280,plain,
! [X2,X3,X0,X1,X4] : product(X0,product(X2,difference(X1,quotient(X4,product(X1,X3))))) = product(X0,quotient(X4,product(difference(X2,X1),X3))),
inference(forward_demodulation,[],[f12275,f11846]) ).
fof(f12284,plain,
! [X2,X0,X1] : product(product(X1,quotient(X0,X1)),quotient(X2,X1)) = product(difference(X2,difference(product(X0,X1),X1)),X2),
inference(superposition,[],[f11036,f228]) ).
fof(f12288,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X1,X0),X3),quotient(X4,X2)) = product(difference(X4,product(X0,product(difference(X1,X2),X3))),X4),
inference(superposition,[],[f11036,f1016]) ).
fof(f12291,plain,
! [X2,X3,X0,X1] : product(product(quotient(X0,X1),difference(X1,X2)),quotient(X3,X0)) = product(difference(X3,product(quotient(X0,X1),X2)),X3),
inference(superposition,[],[f11036,f834]) ).
fof(f12323,plain,
! [X2,X0,X1] : product(X1,quotient(X2,difference(X1,X0))) = product(difference(X2,product(X0,quotient(X1,X0))),X2),
inference(superposition,[],[f11036,f4442]) ).
fof(f12397,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,quotient(X1,X2)),product(X3,difference(X1,X4))) = product(product(difference(X1,product(X2,X0)),X3),X4),
inference(superposition,[],[f140,f11036]) ).
fof(f12424,plain,
! [X2,X0,X1] : difference(product(X0,quotient(X1,X2)),X1) = product(difference(difference(X1,product(X2,X0)),X1),X1),
inference(superposition,[],[f3975,f11036]) ).
fof(f12433,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(product(difference(X1,X2),X3),X4)) = product(X2,product(difference(X1,difference(product(difference(X1,X2),X3),product(X4,X0))),X3)),
inference(superposition,[],[f1016,f11036]) ).
fof(f12443,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(product(difference(X1,X2),X3),X4)) = product(difference(X3,product(X4,X0)),difference(X1,X2)),
inference(forward_demodulation,[],[f12433,f5893]) ).
fof(f12450,plain,
! [X2,X0,X1] : difference(product(X0,quotient(X1,X2)),X1) = product(X1,quotient(product(X2,X0),X1)),
inference(forward_demodulation,[],[f12424,f6878]) ).
fof(f12473,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,X3),product(quotient(X4,X2),X1)) = product(product(difference(X1,product(X2,X0)),X3),X4),
inference(forward_demodulation,[],[f12397,f2646]) ).
fof(f12525,plain,
! [X2,X0,X1] : product(X1,quotient(X2,difference(X1,X0))) = product(quotient(X1,X0),quotient(X2,X0)),
inference(forward_demodulation,[],[f12323,f11036]) ).
fof(f12548,plain,
! [X2,X3,X0,X1] : product(X2,quotient(X3,quotient(X0,X1))) = product(product(quotient(X0,X1),difference(X1,X2)),quotient(X3,X0)),
inference(forward_demodulation,[],[f12291,f11036]) ).
fof(f12551,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X1,X0),X3),quotient(X4,X2)) = product(product(difference(X1,X2),X3),quotient(X4,X0)),
inference(forward_demodulation,[],[f12288,f11036]) ).
fof(f12554,plain,
! [X2,X0,X1] : product(difference(X2,product(difference(X0,X1),X1)),X2) = product(product(X1,quotient(X0,X1)),quotient(X2,X1)),
inference(forward_demodulation,[],[f12284,f3975]) ).
fof(f12559,plain,
! [X2,X0,X1] : product(difference(X0,X1),X2) = product(X1,quotient(product(X2,X0),X1)),
inference(forward_demodulation,[],[f12450,f3976]) ).
fof(f12595,plain,
! [X2,X0,X1] : product(X1,quotient(X2,difference(X1,X0))) = quotient(product(X1,X2),X0),
inference(forward_demodulation,[],[f12525,f11863]) ).
fof(f12599,plain,
! [X2,X3,X0,X1] : product(X2,quotient(X3,quotient(X0,X1))) = product(X0,product(difference(X1,X2),difference(X1,quotient(X3,X0)))),
inference(forward_demodulation,[],[f12548,f751]) ).
fof(f12601,plain,
! [X2,X0,X1] : product(X1,quotient(X2,difference(X0,X1))) = product(product(X1,quotient(X0,X1)),quotient(X2,X1)),
inference(forward_demodulation,[],[f12554,f11036]) ).
fof(f12621,plain,
! [X2,X3,X0,X1] : product(X2,quotient(X3,quotient(X0,X1))) = product(X0,difference(X1,product(X2,quotient(X3,X0)))),
inference(forward_demodulation,[],[f12599,f3101]) ).
fof(f12665,plain,
! [X2,X3,X0,X1] : product(difference(X1,X2),difference(product(X1,quotient(X0,X1)),X3)) = difference(difference(product(X0,X1),X1),product(X2,X3)),
inference(superposition,[],[f2949,f228]) ).
fof(f12673,plain,
! [X2,X3,X0,X1] : difference(X0,product(X2,X3)) = product(difference(X1,X2),difference(difference(X1,X0),X3)),
inference(superposition,[],[f2949,f22]) ).
fof(f12709,plain,
! [X2,X3,X0,X1] : product(difference(quotient(X0,X1),X2),difference(X1,X3)) = difference(X0,product(X2,X3)),
inference(superposition,[],[f2949,f24]) ).
fof(f12727,plain,
! [X2,X3,X0,X1] : product(difference(X2,X1),difference(X3,product(X1,quotient(X0,X1)))) = difference(product(X2,X3),difference(product(X0,X1),X1)),
inference(superposition,[],[f2949,f228]) ).
fof(f12735,plain,
! [X2,X3,X0,X1] : difference(product(X1,X3),X0) = product(difference(X1,X2),difference(X3,difference(X2,X0))),
inference(superposition,[],[f2949,f22]) ).
fof(f12742,plain,
! [X2,X3,X0,X1] : product(difference(X2,product(difference(X0,X1),X0)),difference(X3,X0)) = difference(product(X2,X3),quotient(X0,product(X0,X1))),
inference(superposition,[],[f2949,f242]) ).
fof(f12771,plain,
! [X2,X3,X0,X1] : difference(product(X1,X3),X0) = product(difference(X1,quotient(X0,X2)),difference(X3,X2)),
inference(superposition,[],[f2949,f24]) ).
fof(f12774,plain,
! [X2,X3,X0,X1,X4] : product(difference(X3,quotient(X0,X2)),difference(X4,quotient(X1,X2))) = difference(product(X3,X4),quotient(product(X0,X1),X2)),
inference(superposition,[],[f2949,f11863]) ).
fof(f12816,plain,
! [X2,X0,X1] : product(difference(X0,difference(product(X0,X1),X2)),difference(X1,X2)) = difference(X2,difference(product(X0,X1),X2)),
inference(superposition,[],[f4244,f2949]) ).
fof(f12883,plain,
! [X2,X0,X1] : difference(X2,difference(product(X0,X1),X2)) = product(difference(X1,difference(X0,X2)),difference(X1,X2)),
inference(forward_demodulation,[],[f12816,f10349]) ).
fof(f12947,plain,
! [X2,X3,X0,X1] : product(difference(X2,product(difference(X0,X1),X0)),difference(X3,X0)) = difference(product(X2,X3),product(X0,quotient(X0,X1))),
inference(forward_demodulation,[],[f12742,f6063]) ).
fof(f12959,plain,
! [X2,X3,X0,X1] : product(difference(X2,X1),difference(X3,product(X1,quotient(X0,X1)))) = difference(product(X2,X3),product(difference(X0,X1),X1)),
inference(forward_demodulation,[],[f12727,f3975]) ).
fof(f13010,plain,
! [X2,X3,X0,X1] : product(difference(X1,X2),difference(product(X1,quotient(X0,X1)),X3)) = difference(product(difference(X0,X1),X1),product(X2,X3)),
inference(forward_demodulation,[],[f12665,f3975]) ).
fof(f13036,plain,
! [X2,X0,X1] : difference(X1,product(difference(X0,X2),X2)) = difference(X2,difference(product(X0,X1),X2)),
inference(forward_demodulation,[],[f12883,f3101]) ).
fof(f13076,plain,
! [X2,X3,X0,X1] : product(difference(X2,product(difference(X0,X1),X0)),difference(X3,X0)) = product(difference(X2,X0),difference(X3,quotient(X0,X1))),
inference(forward_demodulation,[],[f12947,f2949]) ).
fof(f13079,plain,
! [X2,X3,X0,X1] : product(difference(X2,X1),difference(X3,product(X1,quotient(X0,X1)))) = product(difference(X2,difference(X0,X1)),difference(X3,X1)),
inference(forward_demodulation,[],[f12959,f2949]) ).
fof(f13084,plain,
! [X2,X3,X0,X1] : product(difference(X1,X2),difference(product(X1,quotient(X0,X1)),X3)) = product(difference(difference(X0,X1),X2),difference(X1,X3)),
inference(forward_demodulation,[],[f13010,f2949]) ).
fof(f13115,plain,
! [X2,X3,X0,X1] : product(difference(X2,X0),difference(X3,quotient(X0,X1))) = product(X0,quotient(product(difference(X3,X0),X2),difference(X0,X1))),
inference(forward_demodulation,[],[f13076,f12443]) ).
fof(f13116,plain,
! [X2,X3,X0,X1] : product(difference(X2,difference(X0,X1)),difference(X3,X1)) = product(X1,difference(X3,product(difference(X2,X1),quotient(X0,X1)))),
inference(forward_demodulation,[],[f13079,f3025]) ).
fof(f13134,plain,
! [X2,X3,X0,X1] : product(difference(X2,X0),difference(X3,quotient(X0,X1))) = quotient(product(X0,product(difference(X3,X0),X2)),X1),
inference(forward_demodulation,[],[f13115,f12595]) ).
fof(f13135,plain,
! [X2,X3,X0,X1] : product(difference(X2,difference(X0,X1)),difference(X3,X1)) = product(difference(X2,X1),quotient(X0,quotient(X1,X3))),
inference(forward_demodulation,[],[f13116,f12621]) ).
fof(f13146,plain,
! [X2,X3,X0,X1] : product(difference(X2,X0),difference(X3,quotient(X0,X1))) = product(quotient(X0,quotient(X1,X2)),difference(X3,X0)),
inference(forward_demodulation,[],[f13134,f2441]) ).
fof(f13165,plain,
! [X2,X3,X0,X1,X4,X5] : difference(product(X3,X4),product(product(X0,quotient(X5,X2)),X1)) = product(difference(X3,product(X0,quotient(X1,X2))),difference(X4,X5)),
inference(superposition,[],[f12771,f2020]) ).
fof(f13181,plain,
! [X2,X3,X0,X1] : difference(product(X1,X2),X3) = product(difference(X1,quotient(X3,product(X2,X0))),X0),
inference(superposition,[],[f12771,f21]) ).
fof(f13188,plain,
! [X2,X0,X1] : difference(product(X1,X0),X2) = product(difference(X1,quotient(X2,X0)),X0),
inference(superposition,[],[f12771,f47]) ).
fof(f13198,plain,
! [X2,X3,X0,X1] : difference(product(X1,quotient(X2,X0)),X3) = product(difference(X1,quotient(X3,X2)),X0),
inference(superposition,[],[f12771,f61]) ).
fof(f13341,plain,
! [X2,X3,X0,X1,X4,X5] : difference(product(X3,X4),product(product(X0,quotient(X5,X2)),X1)) = product(quotient(X1,X2),quotient(product(difference(X4,X5),X3),X0)),
inference(forward_demodulation,[],[f13165,f12443]) ).
fof(f13370,plain,
! [X2,X3,X0,X1,X4,X5] : product(quotient(X1,X2),quotient(product(difference(X4,X5),X3),X0)) = product(quotient(X5,X2),difference(difference(X0,product(X3,X4)),X1)),
inference(forward_demodulation,[],[f13341,f2919]) ).
fof(f13424,plain,
! [X2,X3,X0,X1] : difference(product(quotient(X1,X0),X2),X3) = product(X0,difference(X2,difference(X1,X3))),
inference(superposition,[],[f12735,f61]) ).
fof(f13430,plain,
! [X2,X3,X0,X1,X4] : difference(product(X3,X4),product(product(X1,X0),X2)) = product(difference(X3,X1),difference(X4,product(X0,difference(X1,X2)))),
inference(superposition,[],[f12735,f2920]) ).
fof(f13480,plain,
! [X2,X3,X0,X1] : difference(product(X0,difference(difference(X0,X1),X2)),X3) = difference(X2,product(difference(X0,X1),difference(X1,X3))),
inference(superposition,[],[f3535,f12735]) ).
fof(f13564,plain,
! [X2,X3,X0,X1] : difference(difference(X1,product(X0,X2)),X3) = difference(X2,product(difference(X0,X1),difference(X1,X3))),
inference(forward_demodulation,[],[f13480,f3535]) ).
fof(f13592,plain,
! [X2,X3,X0,X1,X4] : product(difference(X3,X1),difference(X4,product(X0,difference(X1,X2)))) = product(X0,difference(difference(X1,product(X3,X4)),X2)),
inference(forward_demodulation,[],[f13430,f2919]) ).
fof(f13691,plain,
! [X2,X3,X0,X1] : difference(X1,product(X2,X3)) = product(X0,difference(difference(quotient(X2,X0),X1),X3)),
inference(superposition,[],[f12673,f61]) ).
fof(f14042,plain,
! [X2,X3,X0,X1] : quotient(difference(product(X0,X1),X2),X3) = difference(X0,quotient(X2,product(X1,X3))),
inference(superposition,[],[f23,f13181]) ).
fof(f14285,plain,
! [X2,X0,X1] : product(X0,difference(quotient(X0,X1),X2)) = product(X2,product(X1,difference(quotient(X0,X1),X2))),
inference(superposition,[],[f747,f26]) ).
fof(f14314,plain,
! [X2,X3,X0,X1] : difference(X3,product(X0,product(X1,X2))) = product(difference(quotient(X3,X1),X0),X2),
inference(superposition,[],[f21,f747]) ).
fof(f14440,plain,
! [X2,X0,X1] : product(X0,difference(quotient(X0,X1),X2)) = product(quotient(product(X2,X2),X0),X1),
inference(forward_demodulation,[],[f14285,f11988]) ).
fof(f14492,plain,
! [X2,X0,X1] : product(quotient(X2,X0),X1) = product(X0,difference(quotient(X0,X1),X2)),
inference(forward_demodulation,[],[f14440,f26]) ).
fof(f14587,plain,
! [X2,X0,X1] : difference(quotient(X1,X2),X0) = difference(X1,product(quotient(X0,X1),X2)),
inference(superposition,[],[f21,f14492]) ).
fof(f14623,plain,
! [X2,X3,X0,X1] : difference(X1,product(product(quotient(X0,X1),X2),X3)) = product(difference(quotient(X1,X2),X0),difference(X1,X3)),
inference(superposition,[],[f2920,f14492]) ).
fof(f14675,plain,
! [X2,X3,X0,X1] : product(difference(quotient(X1,X2),X0),difference(X1,X3)) = product(X2,difference(difference(quotient(X0,X1),X1),X3)),
inference(forward_demodulation,[],[f14623,f2919]) ).
fof(f14789,plain,
! [X2,X0,X1] : difference(X1,product(X0,X2)) = difference(quotient(X1,X2),product(X0,X1)),
inference(superposition,[],[f14587,f23]) ).
fof(f14801,plain,
! [X2,X0,X1] : difference(X1,product(quotient(X0,X1),X2)) = difference(quotient(X1,difference(X2,X0)),X2),
inference(superposition,[],[f14587,f2569]) ).
fof(f14909,plain,
! [X2,X0,X1] : difference(quotient(X1,X2),X0) = difference(quotient(X1,difference(X2,X0)),X2),
inference(forward_demodulation,[],[f14801,f14587]) ).
fof(f14970,plain,
! [X2,X3,X0,X1,X4] : difference(product(product(X0,X3),X1),product(X4,product(X3,X2))) = difference(product(X0,quotient(X1,X2)),product(X4,product(product(X0,X3),X1))),
inference(superposition,[],[f14789,f277]) ).
fof(f14998,plain,
! [X2,X3,X0,X1] : difference(X1,product(product(X0,quotient(X2,X1)),X3)) = difference(quotient(X1,X3),product(product(X0,X1),X2)),
inference(superposition,[],[f14789,f437]) ).
fof(f15059,plain,
! [X2,X0,X1] : difference(X0,product(quotient(X1,quotient(X0,X2)),X2)) = difference(quotient(quotient(X0,X2),X0),X1),
inference(superposition,[],[f14587,f14789]) ).
fof(f15075,plain,
! [X2,X3,X0,X1] : difference(product(X1,X0),product(quotient(X0,X2),X3)) = product(quotient(X0,X2),difference(difference(X0,product(X1,X2)),X3)),
inference(superposition,[],[f3535,f14789]) ).
fof(f15120,plain,
! [X2,X3,X0,X1] : product(quotient(X0,X2),difference(difference(X0,product(X1,X2)),X3)) = product(difference(X1,quotient(X0,X2)),difference(X0,X3)),
inference(forward_demodulation,[],[f15075,f2949]) ).
fof(f15129,plain,
! [X2,X0,X1] : difference(X0,quotient(product(X1,X2),X0)) = difference(quotient(quotient(X0,X2),X0),X1),
inference(forward_demodulation,[],[f15059,f11885]) ).
fof(f15166,plain,
! [X2,X3,X0,X1] : difference(X1,product(product(X0,quotient(X2,X1)),X3)) = product(X1,difference(difference(X0,quotient(X1,X3)),X2)),
inference(forward_demodulation,[],[f14998,f2919]) ).
fof(f15187,plain,
! [X2,X3,X0,X1,X4] : difference(product(product(X0,X3),X1),product(X4,product(X3,X2))) = product(difference(quotient(product(X0,quotient(X1,X2)),product(X0,X3)),X4),X1),
inference(forward_demodulation,[],[f14970,f14314]) ).
fof(f15237,plain,
! [X2,X3,X0,X1] : product(X1,difference(difference(X0,quotient(X1,X3)),X2)) = product(quotient(X2,X1),difference(difference(X0,X1),X3)),
inference(forward_demodulation,[],[f15166,f2919]) ).
fof(f15255,plain,
! [X2,X3,X0,X1,X4] : difference(product(product(X0,X3),X1),product(X4,product(X3,X2))) = product(difference(product(quotient(X0,X0),quotient(quotient(X1,X2),X3)),X4),X1),
inference(forward_demodulation,[],[f15187,f1974]) ).
fof(f15301,plain,
! [X2,X3,X0,X1,X4] : difference(product(product(X0,X3),X1),product(X4,product(X3,X2))) = product(product(difference(quotient(X0,X0),quotient(X4,quotient(X1,X2))),X3),X1),
inference(forward_demodulation,[],[f15255,f13198]) ).
fof(f15321,plain,
! [X2,X3,X0,X1,X4] : difference(product(product(X0,X3),X1),product(X4,product(X3,X2))) = product(product(difference(X0,quotient(X4,quotient(X1,X2))),X3),X1),
inference(forward_demodulation,[],[f15301,f53]) ).
fof(f15333,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,quotient(X4,quotient(X1,X2))),X3),X1) = product(difference(quotient(product(product(X0,X3),X1),X3),X4),X2),
inference(forward_demodulation,[],[f15321,f14314]) ).
fof(f15342,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,quotient(X4,quotient(X1,X2))),X3),X1) = product(difference(product(X0,quotient(X1,X3)),X4),X2),
inference(forward_demodulation,[],[f15333,f694]) ).
fof(f15349,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,quotient(X4,quotient(X1,X2))),X3),X1) = product(product(difference(X0,quotient(X4,X1)),X3),X2),
inference(forward_demodulation,[],[f15342,f13198]) ).
fof(f15391,plain,
! [X2,X3,X0,X1] : product(product(difference(X3,X0),difference(X3,X1)),X2) = product(difference(X3,X0),difference(X0,product(X1,X2))),
inference(superposition,[],[f523,f12673]) ).
fof(f15400,plain,
! [X2,X0,X1] : product(X2,product(quotient(X0,X1),X2)) = product(product(X2,quotient(X2,X1)),X0),
inference(superposition,[],[f523,f2569]) ).
fof(f15578,plain,
! [X2,X3,X0,X1] : product(difference(X3,product(X0,X1)),X2) = product(difference(X3,X0),difference(X0,product(X1,X2))),
inference(forward_demodulation,[],[f15391,f3101]) ).
fof(f15774,plain,
! [X0,X1] : difference(difference(X1,X0),X1) = difference(X0,product(difference(X0,X1),X1)),
inference(superposition,[],[f21,f8945]) ).
fof(f15804,plain,
! [X2,X3,X0,X1] : product(X2,quotient(X3,difference(difference(X1,X0),X1))) = quotient(product(product(X2,X0),X3),product(difference(X0,X1),X1)),
inference(superposition,[],[f277,f8945]) ).
fof(f15879,plain,
! [X2,X3,X0,X1] : product(X2,quotient(X3,difference(difference(X1,X0),X1))) = product(quotient(product(X2,X0),difference(X0,X1)),quotient(X3,X1)),
inference(forward_demodulation,[],[f15804,f1974]) ).
fof(f15905,plain,
! [X0,X1] : difference(X1,difference(X0,X1)) = difference(difference(X1,X0),X1),
inference(forward_demodulation,[],[f15774,f4244]) ).
fof(f16385,plain,
! [X2,X0,X1] : quotient(X0,product(X1,X2)) = product(quotient(X0,X1),quotient(X0,X2)),
inference(superposition,[],[f1974,f26]) ).
fof(f16396,plain,
! [X2,X3,X0,X1] : quotient(X0,product(X2,X3)) = product(quotient(X1,X2),quotient(difference(X1,X0),X3)),
inference(superposition,[],[f1974,f22]) ).
fof(f16438,plain,
! [X2,X3,X0,X1,X4] : product(quotient(difference(X1,product(X2,X0)),X3),quotient(X1,X4)) = quotient(product(X0,quotient(X1,X2)),product(X3,X4)),
inference(superposition,[],[f1974,f11036]) ).
fof(f16439,plain,
! [X2,X3,X0,X1] : quotient(X0,product(X2,X3)) = product(quotient(quotient(X0,X1),X2),quotient(X1,X3)),
inference(superposition,[],[f1974,f24]) ).
fof(f16471,plain,
! [X2,X3,X0,X1,X4] : quotient(product(X3,X4),product(quotient(X0,X1),X2)) = product(quotient(X3,X1),quotient(X4,difference(quotient(X1,X2),X0))),
inference(superposition,[],[f1974,f14492]) ).
fof(f16563,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = product(product(X1,X3),product(quotient(X0,X1),quotient(X2,X3))),
inference(superposition,[],[f4442,f1974]) ).
fof(f16573,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,X2),X4),product(X1,X3)) = product(product(quotient(X0,X1),quotient(X2,X3)),quotient(X4,product(X1,X3))),
inference(superposition,[],[f11863,f1974]) ).
fof(f16584,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,X2),X4),product(X1,X3)) = product(X0,product(quotient(X2,X3),difference(X1,quotient(X4,product(X1,X3))))),
inference(forward_demodulation,[],[f16573,f751]) ).
fof(f16594,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = product(product(difference(quotient(X2,X3),X1),X3),X0),
inference(forward_demodulation,[],[f16563,f7225]) ).
fof(f16670,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X3,X1),quotient(X4,difference(quotient(X1,X2),X0))) = product(quotient(X3,quotient(X0,X1)),quotient(X4,X2)),
inference(forward_demodulation,[],[f16471,f1974]) ).
fof(f16696,plain,
! [X2,X3,X0,X1,X4] : product(quotient(difference(X1,product(X2,X0)),X3),quotient(X1,X4)) = product(quotient(X0,X3),quotient(quotient(X1,X2),X4)),
inference(forward_demodulation,[],[f16438,f1974]) ).
fof(f16748,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,X2),X4),product(X1,X3)) = product(X0,quotient(X4,product(difference(quotient(X2,X3),X1),X3))),
inference(forward_demodulation,[],[f16584,f12280]) ).
fof(f16757,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X0,X2),X1)) = product(product(difference(quotient(X2,X3),X1),X3),X0),
inference(forward_demodulation,[],[f16594,f11036]) ).
fof(f16800,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(X4,product(difference(quotient(X2,X3),X1),X3))) = product(quotient(product(X0,X2),X1),quotient(X4,X3)),
inference(forward_demodulation,[],[f16748,f1974]) ).
fof(f16890,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,quotient(X3,X2)),X1),product(X4,X3)) = product(quotient(product(product(X0,quotient(X3,X2)),X1),X4),product(X0,quotient(X1,X2))),
inference(superposition,[],[f16385,f2020]) ).
fof(f16927,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X0,product(X1,X2)),product(X3,X4)) = product(product(quotient(X0,X1),X3),product(quotient(X0,X2),X4)),
inference(superposition,[],[f25,f16385]) ).
fof(f17010,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X0,product(X1,X2)),product(X3,X4)) = product(X0,product(X3,difference(X1,product(quotient(X0,X2),X4)))),
inference(forward_demodulation,[],[f16927,f751]) ).
fof(f17034,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,quotient(X3,X2)),X1),product(X4,X3)) = product(product(X0,quotient(X3,X2)),product(X0,difference(quotient(X4,quotient(X1,X2)),X1))),
inference(forward_demodulation,[],[f16890,f11989]) ).
fof(f17070,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,quotient(X3,X2)),X1),product(X4,X3)) = product(X0,product(quotient(X3,X2),difference(quotient(X4,quotient(X1,X2)),X1))),
inference(forward_demodulation,[],[f17034,f130]) ).
fof(f17099,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,quotient(X3,X2)),X1),product(X4,X3)) = product(X0,quotient(X1,product(difference(quotient(X3,X2),X4),X2))),
inference(forward_demodulation,[],[f17070,f12033]) ).
fof(f17115,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(X0,quotient(X3,X2)),X1),product(X4,X3)) = product(quotient(product(X0,X3),X4),quotient(X1,X2)),
inference(forward_demodulation,[],[f17099,f16800]) ).
fof(f17127,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X0,X3),X4),quotient(X1,X2)) = product(quotient(product(X0,quotient(X3,X2)),X4),quotient(X1,X3)),
inference(forward_demodulation,[],[f17115,f1974]) ).
fof(f17174,plain,
! [X2,X3,X0,X1] : quotient(X1,product(X2,difference(X0,X3))) = product(quotient(quotient(X1,X3),X2),X0),
inference(superposition,[],[f16439,f52]) ).
fof(f17388,plain,
! [X2,X3,X0,X1] : quotient(X1,product(difference(X0,X2),X3)) = product(X0,quotient(difference(X2,X1),X3)),
inference(superposition,[],[f16396,f52]) ).
fof(f18064,plain,
! [X2,X3,X0,X1,X4] : product(difference(X1,difference(X0,X2)),difference(difference(X0,X3),X4)) = difference(X3,product(difference(product(X0,X1),X2),X4)),
inference(superposition,[],[f2919,f3566]) ).
fof(f18188,plain,
! [X2,X3,X0,X1] : product(product(X0,difference(difference(X1,X2),X3)),X2) = product(X3,quotient(X2,product(X1,X0))),
inference(superposition,[],[f11036,f2919]) ).
fof(f18245,plain,
! [X2,X3,X0,X1] : difference(X2,product(product(X1,X0),X3)) = product(X0,difference(difference(X1,quotient(X2,X3)),X2)),
inference(superposition,[],[f14789,f2919]) ).
fof(f18253,plain,
! [X2,X3,X0,X1] : product(X0,difference(difference(X1,X2),X3)) = product(X0,difference(difference(X1,quotient(X2,X3)),X2)),
inference(forward_demodulation,[],[f18245,f2919]) ).
fof(f18536,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X2,product(quotient(X2,X0),X1)),X2)) = product(X3,product(product(X0,difference(X1,X2)),product(quotient(X2,X0),X1))),
inference(superposition,[],[f4477,f3633]) ).
fof(f18739,plain,
! [X2,X0,X1] : product(product(difference(X0,product(difference(X1,X2),X1)),X0),quotient(product(X2,X1),X2)) = product(product(difference(X1,X2),X1),X0),
inference(superposition,[],[f4283,f4477]) ).
fof(f19045,plain,
! [X2,X0,X1] : product(product(difference(X1,X2),X1),X0) = product(product(difference(X0,X2),X0),quotient(product(X2,X1),product(difference(X1,X2),X1))),
inference(forward_demodulation,[],[f18739,f12551]) ).
fof(f19233,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X2,product(quotient(X2,X0),X1)),X2)) = product(X3,product(product(difference(X1,X0),difference(X1,X2)),X2)),
inference(forward_demodulation,[],[f18536,f7225]) ).
fof(f19364,plain,
! [X2,X0,X1] : product(product(difference(X1,X2),X1),X0) = product(product(difference(X0,X2),X0),product(quotient(X2,difference(X1,X2)),quotient(X1,X1))),
inference(forward_demodulation,[],[f19045,f1974]) ).
fof(f19508,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X2,product(quotient(X2,X0),X1)),X2)) = product(product(X0,X2),product(difference(X1,X3),X2)),
inference(forward_demodulation,[],[f19233,f1316]) ).
fof(f19596,plain,
! [X2,X0,X1] : product(product(difference(X1,X2),X1),X0) = product(product(difference(quotient(X1,X1),X2),quotient(X2,difference(X1,X2))),X0),
inference(forward_demodulation,[],[f19364,f11140]) ).
fof(f19689,plain,
! [X2,X3,X0,X1] : product(product(X0,difference(X1,X3)),X2) = product(X3,quotient(product(X2,product(quotient(X2,X0),X1)),X2)),
inference(forward_demodulation,[],[f19508,f141]) ).
fof(f19755,plain,
! [X2,X0,X1] : product(product(difference(X1,X2),X1),X0) = product(product(difference(quotient(X1,X1),X2),X1),X0),
inference(forward_demodulation,[],[f19596,f52]) ).
fof(f19830,plain,
! [X2,X3,X0,X1] : product(product(X0,difference(X1,X3)),X2) = product(X3,product(X2,quotient(product(quotient(X2,X0),X1),X2))),
inference(forward_demodulation,[],[f19689,f6461]) ).
fof(f19885,plain,
! [X2,X0,X1] : product(X1,quotient(product(X0,X1),X2)) = product(product(difference(X1,X2),X1),X0),
inference(forward_demodulation,[],[f19755,f16757]) ).
fof(f19938,plain,
! [X2,X3,X0,X1] : product(product(X0,difference(X1,X3)),X2) = product(X3,product(difference(X1,X2),quotient(X2,X0))),
inference(forward_demodulation,[],[f19830,f12559]) ).
fof(f20231,plain,
! [X0,X1] : product(difference(X1,difference(X1,X0)),X1) = quotient(quotient(X1,X0),X1),
inference(superposition,[],[f1703,f22]) ).
fof(f20251,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = quotient(quotient(product(X0,X2),product(product(X0,X1),product(X2,X3))),product(X0,X2)),
inference(superposition,[],[f1703,f25]) ).
fof(f20403,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = quotient(product(quotient(X0,product(X0,X1)),quotient(X2,product(X2,X3))),product(X0,X2)),
inference(forward_demodulation,[],[f20251,f1974]) ).
fof(f20485,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = product(quotient(quotient(X0,product(X0,X1)),X0),quotient(quotient(X2,product(X2,X3)),X2)),
inference(forward_demodulation,[],[f20403,f1974]) ).
fof(f20549,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = product(quotient(quotient(X0,product(X0,X1)),X0),product(difference(X2,X3),X2)),
inference(forward_demodulation,[],[f20485,f1703]) ).
fof(f20595,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = product(product(difference(X0,X1),X0),product(difference(X2,X3),X2)),
inference(forward_demodulation,[],[f20549,f1703]) ).
fof(f20628,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = product(product(difference(X2,X1),difference(X2,X3)),X0),
inference(forward_demodulation,[],[f20595,f11140]) ).
fof(f20652,plain,
! [X2,X3,X0,X1] : product(difference(product(X0,X2),product(X1,X3)),product(X0,X2)) = product(difference(X2,product(X1,X3)),X0),
inference(forward_demodulation,[],[f20628,f3101]) ).
fof(f20672,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X0,X2),X1)) = product(difference(X2,product(X1,X3)),X0),
inference(forward_demodulation,[],[f20652,f11036]) ).
fof(f20749,plain,
! [X0,X1] : product(difference(X0,X1),product(X0,X0)) = product(X0,quotient(quotient(X0,X1),X0)),
inference(superposition,[],[f509,f20231]) ).
fof(f20870,plain,
! [X0,X1] : product(difference(X0,X1),X0) = product(X0,quotient(quotient(X0,X1),X0)),
inference(forward_demodulation,[],[f20749,f26]) ).
fof(f21108,plain,
! [X2,X3,X0,X1] : product(X2,difference(X3,product(difference(X0,X1),X0))) = difference(product(quotient(X1,X2),X3),product(difference(X0,X1),X1)),
inference(superposition,[],[f2970,f4547]) ).
fof(f21132,plain,
! [X2,X3,X0,X1,X4,X5] : product(X4,difference(X5,product(X1,X3))) = difference(product(quotient(product(X0,X2),X4),X5),product(product(X0,X1),product(X2,X3))),
inference(superposition,[],[f2970,f25]) ).
fof(f21189,plain,
! [X2,X3,X0,X1] : product(X2,quotient(product(quotient(X3,X0),X1),X3)) = product(product(X0,difference(X1,X2)),product(quotient(X3,X0),X1)),
inference(superposition,[],[f11036,f2970]) ).
fof(f21215,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(product(product(X4,X2),product(quotient(X4,X0),X1)),product(X4,X2))) = product(X3,product(product(X0,difference(X1,X2)),product(quotient(X4,X0),X1))),
inference(superposition,[],[f4477,f2970]) ).
fof(f21251,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(product(product(X4,X2),product(quotient(X4,X0),X1)),product(X4,X2))) = product(X3,product(product(difference(X1,X0),difference(X1,X2)),X4)),
inference(forward_demodulation,[],[f21215,f7225]) ).
fof(f21276,plain,
! [X2,X3,X0,X1] : product(X2,quotient(product(quotient(X3,X0),X1),X3)) = product(product(difference(X1,X0),difference(X1,X2)),X3),
inference(forward_demodulation,[],[f21189,f7225]) ).
fof(f21331,plain,
! [X2,X3,X0,X1,X4,X5] : product(X4,difference(X5,product(X1,X3))) = product(difference(quotient(product(quotient(product(X0,X2),X4),X5),X2),product(X0,X1)),X3),
inference(forward_demodulation,[],[f21132,f14314]) ).
fof(f21354,plain,
! [X2,X3,X0,X1] : product(X2,difference(X3,product(difference(X0,X1),X0))) = difference(X1,difference(product(X0,product(quotient(X1,X2),X3)),X1)),
inference(forward_demodulation,[],[f21108,f13036]) ).
fof(f21411,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(product(product(X4,X2),product(quotient(X4,X0),X1)),product(X4,X2))) = product(product(X0,X2),product(difference(X1,X3),X4)),
inference(forward_demodulation,[],[f21251,f1316]) ).
fof(f21431,plain,
! [X2,X3,X0,X1] : product(difference(X1,product(X0,X2)),X3) = product(X2,quotient(product(quotient(X3,X0),X1),X3)),
inference(forward_demodulation,[],[f21276,f3101]) ).
fof(f21463,plain,
! [X2,X3,X0,X1,X4,X5] : product(X4,difference(X5,product(X1,X3))) = product(X1,quotient(product(X3,quotient(product(quotient(product(X0,X2),X4),X5),X2)),X0)),
inference(forward_demodulation,[],[f21331,f20672]) ).
fof(f21481,plain,
! [X2,X3,X0,X1] : product(X2,difference(X3,product(difference(X0,X1),X0))) = difference(X1,product(difference(X0,X1),product(X2,difference(X3,X1)))),
inference(forward_demodulation,[],[f21354,f3982]) ).
fof(f21521,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,X2),product(difference(X1,X3),X4)) = product(X3,product(quotient(product(X4,X2),X4),quotient(product(quotient(X4,X0),X1),X2))),
inference(forward_demodulation,[],[f21411,f1974]) ).
fof(f21537,plain,
! [X2,X3,X0,X1] : product(X2,quotient(product(quotient(X3,X0),X1),X3)) = product(X2,quotient(product(X3,X1),X0)),
inference(forward_demodulation,[],[f21431,f20672]) ).
fof(f21547,plain,
! [X3,X0,X1,X4,X5] : product(X4,difference(X5,product(X1,X3))) = product(X1,quotient(product(X3,quotient(product(X0,X5),X4)),X0)),
inference(forward_demodulation,[],[f21463,f11990]) ).
fof(f21558,plain,
! [X2,X3,X0,X1] : product(X2,difference(X3,product(difference(X0,X1),X0))) = product(difference(quotient(X1,X2),difference(X0,X1)),difference(X3,X1)),
inference(forward_demodulation,[],[f21481,f14314]) ).
fof(f21585,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,X2),product(difference(X1,X3),X4)) = product(X3,product(product(X4,quotient(X2,X4)),quotient(product(quotient(X4,X0),X1),X2))),
inference(forward_demodulation,[],[f21521,f6461]) ).
fof(f21604,plain,
! [X2,X3,X0,X1] : product(X2,difference(X3,product(difference(X0,X1),X0))) = product(difference(quotient(X1,X2),X1),quotient(X0,quotient(X1,X3))),
inference(forward_demodulation,[],[f21558,f13135]) ).
fof(f21619,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,X2),product(difference(X1,X3),X4)) = product(X3,product(X2,quotient(product(quotient(X4,X0),X1),X4))),
inference(forward_demodulation,[],[f21585,f11830]) ).
fof(f21629,plain,
! [X2,X3,X0,X1] : product(X2,difference(X3,product(difference(X0,X1),X0))) = product(X2,quotient(X0,quotient(X1,X3))),
inference(forward_demodulation,[],[f21604,f61]) ).
fof(f21636,plain,
! [X2,X3,X0,X1,X4] : product(product(X0,X2),product(difference(X1,X3),X4)) = product(X3,product(X2,quotient(product(X4,X1),X0))),
inference(forward_demodulation,[],[f21619,f21537]) ).
fof(f21832,plain,
! [X2,X0,X1] : difference(X0,product(product(X1,X0),X2)) = product(difference(X0,X1),difference(X1,X2)),
inference(superposition,[],[f12709,f8271]) ).
fof(f22042,plain,
! [X2,X0,X1] : product(X0,difference(difference(X1,X0),X2)) = product(difference(X0,X1),difference(X1,X2)),
inference(forward_demodulation,[],[f21832,f2919]) ).
fof(f22245,plain,
! [X2,X3,X0,X1] : product(product(X1,quotient(X0,X1)),X2) = quotient(product(product(X0,quotient(X0,X1)),product(X2,X3)),product(X0,X3)),
inference(superposition,[],[f158,f4327]) ).
fof(f22342,plain,
! [X2,X3,X0,X1] : product(product(X1,quotient(X0,X1)),X2) = product(quotient(product(X0,quotient(X0,X1)),X0),quotient(product(X2,X3),X3)),
inference(forward_demodulation,[],[f22245,f1974]) ).
fof(f22450,plain,
! [X2,X0,X1] : product(product(X1,quotient(X0,X1)),X2) = product(quotient(product(X0,quotient(X0,X1)),X0),X2),
inference(forward_demodulation,[],[f22342,f23]) ).
fof(f22525,plain,
! [X2,X0,X1] : product(product(X1,quotient(X0,X1)),X2) = product(product(X0,quotient(quotient(X0,X1),X0)),X2),
inference(forward_demodulation,[],[f22450,f6461]) ).
fof(f22581,plain,
! [X2,X0,X1] : product(product(X1,quotient(X0,X1)),X2) = product(product(difference(X0,X1),X0),X2),
inference(forward_demodulation,[],[f22525,f20870]) ).
fof(f22752,plain,
! [X2,X0,X1] : product(difference(difference(X0,X1),X2),difference(X0,X1)) = product(difference(X0,X2),difference(X0,quotient(X1,X0))),
inference(superposition,[],[f10563,f6794]) ).
fof(f22775,plain,
! [X2,X0,X1] : product(difference(difference(X0,X1),X2),difference(X0,X1)) = difference(X0,product(X2,quotient(X1,X0))),
inference(forward_demodulation,[],[f22752,f3101]) ).
fof(f23463,plain,
! [X2,X3,X0,X1] : product(product(X1,quotient(X2,X1)),X3) = product(product(difference(X0,X1),quotient(X2,X0)),X3),
inference(superposition,[],[f22581,f10563]) ).
fof(f23601,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,X1),X0),product(difference(X2,X3),X4)) = product(X3,product(difference(X2,product(X1,quotient(X0,X1))),X4)),
inference(superposition,[],[f1016,f22581]) ).
fof(f23705,plain,
! [X2,X3,X0,X1] : product(X3,product(difference(X2,product(difference(X1,X0),X1)),X2)) = product(X3,quotient(product(product(X0,quotient(X1,X0)),X2),product(difference(X1,X0),X1))),
inference(superposition,[],[f4477,f22581]) ).
fof(f23709,plain,
! [X2,X0,X1] : difference(X2,product(difference(X1,X0),X1)) = difference(quotient(X2,product(difference(X1,X0),X1)),product(product(X0,quotient(X1,X0)),X2)),
inference(superposition,[],[f8271,f22581]) ).
fof(f23785,plain,
! [X2,X0,X1] : difference(X2,product(difference(X1,X0),X1)) = product(quotient(X1,X0),difference(difference(X0,quotient(X2,product(difference(X1,X0),X1))),X2)),
inference(forward_demodulation,[],[f23709,f2919]) ).
fof(f23789,plain,
! [X2,X3,X0,X1] : product(X3,product(difference(X2,product(difference(X1,X0),X1)),X2)) = product(X3,product(quotient(product(X0,quotient(X1,X0)),difference(X1,X0)),quotient(X2,X1))),
inference(forward_demodulation,[],[f23705,f1974]) ).
fof(f23883,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,X1),X0),product(difference(X2,X3),X4)) = product(X3,product(quotient(X0,X1),quotient(product(X4,X2),X1))),
inference(forward_demodulation,[],[f23601,f20672]) ).
fof(f24078,plain,
! [X2,X0,X1] : difference(X2,product(difference(X1,X0),X1)) = product(quotient(X1,X0),difference(difference(X0,X2),product(difference(X1,X0),X1))),
inference(forward_demodulation,[],[f23785,f18253]) ).
fof(f24082,plain,
! [X2,X3,X0,X1] : product(X3,product(difference(X2,product(difference(X1,X0),X1)),X2)) = product(X3,product(quotient(product(X0,X1),difference(X1,X0)),quotient(X2,X0))),
inference(forward_demodulation,[],[f23789,f17127]) ).
fof(f24157,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,X1),X0),product(difference(X2,X3),X4)) = product(X3,quotient(product(X0,product(X4,X2)),X1)),
inference(forward_demodulation,[],[f23883,f11863]) ).
fof(f24311,plain,
! [X2,X0,X1] : difference(X2,product(difference(X1,X0),X1)) = product(quotient(X1,X0),quotient(X1,quotient(X0,difference(X0,X2)))),
inference(forward_demodulation,[],[f24078,f21629]) ).
fof(f24315,plain,
! [X2,X3,X0,X1] : product(X3,product(difference(X2,product(difference(X1,X0),X1)),X2)) = product(X3,product(X0,quotient(X2,difference(difference(X0,X1),X0)))),
inference(forward_demodulation,[],[f24082,f15879]) ).
fof(f24374,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,X1),X0),product(difference(X2,X3),X4)) = product(X3,product(quotient(X0,quotient(X1,X2)),X4)),
inference(forward_demodulation,[],[f24157,f2441]) ).
fof(f24500,plain,
! [X2,X0,X1] : difference(X2,product(difference(X1,X0),X1)) = quotient(X1,product(X0,quotient(X0,difference(X0,X2)))),
inference(forward_demodulation,[],[f24311,f16385]) ).
fof(f24504,plain,
! [X2,X3,X0,X1] : product(X3,product(difference(X2,product(difference(X1,X0),X1)),X2)) = product(X3,product(X0,quotient(X2,difference(X0,difference(X1,X0))))),
inference(forward_demodulation,[],[f24315,f15905]) ).
fof(f24550,plain,
! [X2,X3,X0,X1,X4] : product(X3,product(quotient(X0,quotient(X1,X2)),X4)) = product(product(difference(X4,X1),difference(X2,X3)),X0),
inference(forward_demodulation,[],[f24374,f11140]) ).
fof(f24648,plain,
! [X2,X0,X1] : difference(X2,product(difference(X1,X0),X1)) = quotient(X1,quotient(product(X0,X0),X2)),
inference(forward_demodulation,[],[f24500,f12595]) ).
fof(f24652,plain,
! [X2,X3,X0,X1] : product(X3,product(difference(X2,product(difference(X1,X0),X1)),X2)) = product(X3,quotient(product(X0,X2),difference(X1,X0))),
inference(forward_demodulation,[],[f24504,f12595]) ).
fof(f24760,plain,
! [X2,X0,X1] : quotient(X1,quotient(X0,X2)) = difference(X2,product(difference(X1,X0),X1)),
inference(forward_demodulation,[],[f24648,f26]) ).
fof(f24764,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X0,X2),difference(X1,X0))) = product(X3,product(X1,quotient(X2,difference(X1,X0)))),
inference(forward_demodulation,[],[f24652,f11036]) ).
fof(f24845,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X1,X2),X0)) = product(X3,quotient(product(X0,X2),difference(X1,X0))),
inference(forward_demodulation,[],[f24764,f12595]) ).
fof(f25243,plain,
! [X2,X0,X1] : product(product(X0,difference(X1,X2)),product(quotient(X2,X0),X1)) = product(difference(X2,product(X0,difference(X1,X2))),X2),
inference(superposition,[],[f5166,f3633]) ).
fof(f25417,plain,
! [X2,X3,X0,X1] : product(quotient(difference(product(X1,X2),difference(X0,product(X1,X2))),X3),X1) = quotient(product(difference(X0,product(X1,X2)),X0),product(X3,X2)),
inference(superposition,[],[f265,f5166]) ).
fof(f25438,plain,
! [X2,X3,X0,X1] : product(quotient(difference(product(X1,X2),difference(X0,product(X1,X2))),X3),X1) = product(quotient(difference(X0,product(X1,X2)),X3),quotient(X0,X2)),
inference(forward_demodulation,[],[f25417,f1974]) ).
fof(f25599,plain,
! [X2,X0,X1] : product(product(X0,difference(X1,X2)),product(quotient(X2,X0),X1)) = product(difference(X1,X2),quotient(X2,X0)),
inference(forward_demodulation,[],[f25243,f11036]) ).
fof(f25632,plain,
! [X2,X3,X0,X1] : product(quotient(difference(product(X1,X2),difference(X0,product(X1,X2))),X3),X1) = product(quotient(X2,X3),quotient(quotient(X0,X1),X2)),
inference(forward_demodulation,[],[f25438,f16696]) ).
fof(f25747,plain,
! [X2,X0,X1] : product(difference(X1,X2),quotient(X2,X0)) = product(product(difference(X1,X0),difference(X1,X2)),X2),
inference(forward_demodulation,[],[f25599,f7225]) ).
fof(f25773,plain,
! [X2,X3,X0,X1] : product(quotient(X2,X3),quotient(quotient(X0,X1),X2)) = product(difference(X1,quotient(difference(X0,product(X1,X2)),product(X2,X3))),X1),
inference(forward_demodulation,[],[f25632,f14042]) ).
fof(f25845,plain,
! [X2,X0,X1] : product(difference(X1,X2),quotient(X2,X0)) = product(X2,product(quotient(X2,quotient(X0,X1)),X1)),
inference(forward_demodulation,[],[f25747,f24550]) ).
fof(f25913,plain,
! [X2,X0,X1] : product(difference(X1,X2),quotient(X2,X0)) = product(X2,quotient(product(X2,X1),X0)),
inference(forward_demodulation,[],[f25845,f11885]) ).
fof(f27312,plain,
! [X0,X1] : quotient(X0,difference(X0,X1)) = difference(difference(X0,difference(X1,X0)),X0),
inference(superposition,[],[f5302,f15905]) ).
fof(f27356,plain,
! [X0,X1] : quotient(X0,difference(X0,X1)) = difference(X0,difference(difference(X1,X0),X0)),
inference(forward_demodulation,[],[f27312,f15905]) ).
fof(f27427,plain,
! [X0,X1] : quotient(X0,difference(X0,X1)) = difference(X0,quotient(X0,X1)),
inference(forward_demodulation,[],[f27356,f5302]) ).
fof(f27716,plain,
! [X2,X0,X1] : product(product(product(X0,X1),X1),product(X1,X2)) = product(X1,product(quotient(X1,product(X1,X0)),X2)),
inference(superposition,[],[f130,f4918]) ).
fof(f27847,plain,
! [X2,X0,X1] : product(product(product(X0,X1),X1),product(X1,X2)) = product(X1,product(product(X1,quotient(X1,X0)),X2)),
inference(forward_demodulation,[],[f27716,f6063]) ).
fof(f28009,plain,
! [X2,X0,X1] : product(product(product(X0,X1),X1),product(X1,X2)) = product(X1,product(X1,product(quotient(X2,X0),X1))),
inference(forward_demodulation,[],[f27847,f15400]) ).
fof(f29952,plain,
! [X2,X3,X0,X1] : product(quotient(product(product(X0,X1),X2),X3),X0) = quotient(product(product(X0,X1),product(X2,product(X0,X1))),product(X3,X1)),
inference(superposition,[],[f265,f418]) ).
fof(f29973,plain,
! [X2,X3,X0,X1] : product(quotient(product(product(X0,X1),X2),X3),X0) = product(quotient(product(X0,X1),X3),quotient(product(X2,product(X0,X1)),X1)),
inference(forward_demodulation,[],[f29952,f1974]) ).
fof(f30158,plain,
! [X2,X3,X0,X1] : product(quotient(product(product(X0,X1),X2),X3),X0) = product(quotient(product(X0,X1),X3),product(quotient(X2,quotient(X1,X1)),X0)),
inference(forward_demodulation,[],[f29973,f2441]) ).
fof(f30283,plain,
! [X2,X3,X0,X1] : product(quotient(product(product(X0,X1),X2),X3),X0) = product(X0,product(quotient(X2,quotient(X1,X1)),difference(quotient(X3,X0),X1))),
inference(forward_demodulation,[],[f30158,f11989]) ).
fof(f30378,plain,
! [X2,X3,X0,X1] : product(quotient(product(product(X0,X1),X2),X3),X0) = product(X0,product(difference(X1,X1),difference(quotient(X3,X0),X2))),
inference(forward_demodulation,[],[f30283,f5966]) ).
fof(f30449,plain,
! [X2,X3,X0,X1] : product(quotient(product(product(X0,X1),X2),X3),X0) = product(X0,product(X1,difference(quotient(X3,X0),X2))),
inference(forward_demodulation,[],[f30378,f47]) ).
fof(f30493,plain,
! [X2,X3,X0,X1] : product(X0,product(X1,difference(quotient(X3,X0),X2))) = product(product(X0,quotient(X2,difference(X1,X3))),X0),
inference(forward_demodulation,[],[f30449,f2001]) ).
fof(f30527,plain,
! [X2,X3,X0,X1] : product(X0,product(X1,difference(quotient(X3,X0),X2))) = product(X0,product(quotient(X2,difference(X1,X3)),X0)),
inference(forward_demodulation,[],[f30493,f418]) ).
fof(f30690,plain,
! [X2,X0,X1] : product(X0,difference(difference(X0,X1),X2)) = product(product(X0,difference(difference(X0,X1),quotient(X2,difference(X0,X1)))),X1),
inference(superposition,[],[f523,f3396]) ).
fof(f30702,plain,
! [X2,X0,X1] : product(X0,difference(difference(X0,X1),X2)) = product(quotient(X2,difference(X0,X1)),quotient(X1,product(X0,X0))),
inference(forward_demodulation,[],[f30690,f18188]) ).
fof(f30785,plain,
! [X2,X0,X1] : product(X0,difference(difference(X0,X1),X2)) = product(quotient(X2,difference(X0,X1)),quotient(X1,X0)),
inference(forward_demodulation,[],[f30702,f26]) ).
fof(f30838,plain,
! [X2,X0,X1] : difference(X1,product(X0,X2)) = product(quotient(X2,difference(X0,X1)),quotient(X1,X0)),
inference(forward_demodulation,[],[f30785,f3535]) ).
fof(f31206,plain,
! [X2,X0,X1] : quotient(product(difference(X1,X0),X1),X2) = difference(product(difference(X1,X0),X1),quotient(product(difference(X1,X0),X1),product(product(X0,quotient(X1,X0)),X2))),
inference(superposition,[],[f3494,f22581]) ).
fof(f31229,plain,
! [X0,X1] : quotient(difference(X1,X0),X1) = difference(difference(X1,X0),quotient(difference(X1,X0),product(X0,quotient(X1,X0)))),
inference(superposition,[],[f3494,f4442]) ).
fof(f31417,plain,
! [X0,X1] : difference(X1,quotient(X0,X1)) = difference(difference(X1,X0),quotient(difference(X1,X0),product(X0,quotient(X1,X0)))),
inference(forward_demodulation,[],[f31229,f6794]) ).
fof(f31437,plain,
! [X2,X0,X1] : quotient(product(difference(X1,X0),X1),X2) = difference(product(difference(X1,X0),X1),product(quotient(difference(X1,X0),product(X0,quotient(X1,X0))),quotient(X1,X2))),
inference(forward_demodulation,[],[f31206,f1974]) ).
fof(f31527,plain,
! [X2,X0,X1] : quotient(product(difference(X1,X0),X1),X2) = product(difference(difference(X1,X0),quotient(difference(X1,X0),product(X0,quotient(X1,X0)))),difference(X1,quotient(X1,X2))),
inference(forward_demodulation,[],[f31437,f2949]) ).
fof(f31596,plain,
! [X2,X0,X1] : quotient(product(difference(X1,X0),X1),X2) = product(difference(X1,quotient(X0,X1)),difference(X1,quotient(X1,X2))),
inference(forward_demodulation,[],[f31527,f31417]) ).
fof(f31648,plain,
! [X2,X0,X1] : quotient(product(difference(X1,X0),X1),X2) = difference(X1,product(quotient(X0,X1),quotient(X1,X2))),
inference(forward_demodulation,[],[f31596,f3101]) ).
fof(f31682,plain,
! [X2,X0,X1] : difference(quotient(X1,quotient(X1,X2)),X0) = quotient(product(difference(X1,X0),X1),X2),
inference(forward_demodulation,[],[f31648,f14587]) ).
fof(f31705,plain,
! [X2,X0,X1] : difference(difference(X2,X1),X0) = quotient(product(difference(X1,X0),X1),X2),
inference(forward_demodulation,[],[f31682,f5303]) ).
fof(f32524,plain,
! [X2,X0,X1] : product(difference(difference(X0,X1),product(X0,X2)),X2) = product(difference(X0,difference(X1,X0)),difference(X0,X2)),
inference(superposition,[],[f4074,f15905]) ).
fof(f32587,plain,
! [X2,X3,X0,X1] : product(difference(X0,product(X1,X2)),product(X3,X2)) = product(product(difference(X0,product(X1,X2)),X3),product(difference(X0,X1),difference(X1,X2))),
inference(superposition,[],[f130,f4074]) ).
fof(f32589,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,product(X1,X2)),X3),X4) = product(product(difference(X0,X1),difference(X1,X2)),product(X3,difference(X2,X4))),
inference(superposition,[],[f140,f4074]) ).
fof(f32637,plain,
! [X2,X3,X0,X1] : difference(X2,product(difference(X0,product(X1,X2)),X3)) = difference(quotient(X2,X3),product(difference(X0,X1),difference(X1,X2))),
inference(superposition,[],[f14789,f4074]) ).
fof(f32838,plain,
! [X2,X3,X0,X1] : difference(X2,product(difference(X0,product(X1,X2)),X3)) = difference(difference(X1,product(X0,quotient(X2,X3))),X2),
inference(forward_demodulation,[],[f32637,f13564]) ).
fof(f32885,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,product(X1,X2)),X3),X4) = product(X2,product(quotient(product(X3,difference(X2,X4)),quotient(X1,X1)),X0)),
inference(forward_demodulation,[],[f32589,f24550]) ).
fof(f32887,plain,
! [X2,X3,X0,X1] : product(difference(X0,product(X1,X2)),product(X3,X2)) = product(difference(X0,product(product(X1,X2),X1)),product(X3,difference(X1,X2))),
inference(forward_demodulation,[],[f32587,f3261]) ).
fof(f32948,plain,
! [X2,X0,X1] : difference(X0,product(difference(X1,X0),X2)) = product(difference(difference(X0,X1),product(X0,X2)),X2),
inference(forward_demodulation,[],[f32524,f3101]) ).
fof(f33163,plain,
! [X2,X3,X0,X1] : difference(difference(X1,product(X0,quotient(X2,X3))),X2) = difference(X2,product(X2,quotient(product(X3,X0),X1))),
inference(forward_demodulation,[],[f32838,f20672]) ).
fof(f33199,plain,
! [X2,X3,X0,X1,X4] : product(product(difference(X0,product(X1,X2)),X3),X4) = product(X2,product(quotient(product(X3,difference(X2,X4)),X1),X0)),
inference(forward_demodulation,[],[f32885,f53]) ).
fof(f33201,plain,
! [X2,X3,X0,X1] : product(difference(X0,product(X1,X2)),product(X3,X2)) = product(X1,quotient(product(product(X3,difference(X1,X2)),X0),product(X1,X2))),
inference(forward_demodulation,[],[f32887,f20672]) ).
fof(f33256,plain,
! [X2,X0,X1] : difference(X0,product(difference(X1,X0),X2)) = product(X2,quotient(product(X2,difference(X0,X1)),X0)),
inference(forward_demodulation,[],[f32948,f20672]) ).
fof(f33433,plain,
! [X2,X3,X0,X1] : quotient(product(X3,X0),X1) = difference(difference(X1,product(X0,quotient(X2,X3))),X2),
inference(forward_demodulation,[],[f33163,f21]) ).
fof(f33459,plain,
! [X2,X3,X0,X1,X4] : product(product(X2,X3),product(quotient(X4,X1),X0)) = product(X2,product(quotient(product(X3,difference(X2,X4)),X1),X0)),
inference(forward_demodulation,[],[f33199,f12473]) ).
fof(f33461,plain,
! [X2,X3,X0,X1] : product(difference(X0,product(X1,X2)),product(X3,X2)) = product(X1,product(quotient(product(X3,difference(X1,X2)),X1),quotient(X0,X2))),
inference(forward_demodulation,[],[f33201,f1974]) ).
fof(f33506,plain,
! [X2,X0,X1] : difference(X0,product(difference(X1,X0),X2)) = product(X2,quotient(X1,difference(X2,product(X0,X0)))),
inference(forward_demodulation,[],[f33256,f2050]) ).
fof(f33662,plain,
! [X2,X3,X0,X1] : product(difference(X0,product(X1,X2)),product(X3,X2)) = product(product(X1,X3),product(quotient(X2,X1),quotient(X0,X2))),
inference(forward_demodulation,[],[f33461,f33459]) ).
fof(f33692,plain,
! [X2,X0,X1] : difference(X0,product(difference(X1,X0),X2)) = quotient(product(X2,X1),product(X0,X0)),
inference(forward_demodulation,[],[f33506,f12595]) ).
fof(f33808,plain,
! [X2,X3,X0,X1] : product(difference(X0,product(X1,X2)),product(X3,X2)) = product(product(difference(quotient(X0,X2),X1),X3),X2),
inference(forward_demodulation,[],[f33662,f7225]) ).
fof(f33829,plain,
! [X2,X0,X1] : difference(X0,product(difference(X1,X0),X2)) = product(quotient(X2,X0),quotient(X1,X0)),
inference(forward_demodulation,[],[f33692,f1974]) ).
fof(f33907,plain,
! [X2,X3,X0,X1] : product(product(difference(quotient(X0,X2),X1),X3),X2) = product(X2,quotient(product(product(X3,X2),X0),X1)),
inference(forward_demodulation,[],[f33808,f20672]) ).
fof(f33925,plain,
! [X2,X0,X1] : difference(X0,product(difference(X1,X0),X2)) = quotient(product(X2,X1),X0),
inference(forward_demodulation,[],[f33829,f11863]) ).
fof(f33969,plain,
! [X2,X3,X0,X1] : product(product(difference(quotient(X0,X2),X1),X3),X2) = product(X2,product(X3,quotient(X0,difference(X2,X1)))),
inference(forward_demodulation,[],[f33907,f2001]) ).
fof(f36322,plain,
product(b,quotient(a,b)) = difference(b,difference(product(b,c1),b)),
inference(superposition,[],[f383,f43]) ).
fof(f36460,plain,
product(b,quotient(a,b)) = difference(c1,difference(b,b)),
inference(forward_demodulation,[],[f36322,f10349]) ).
fof(f36593,plain,
product(b,quotient(a,b)) = difference(c1,b),
inference(forward_demodulation,[],[f36460,f47]) ).
fof(f38148,plain,
! [X2,X3,X0,X1] : product(difference(quotient(X0,X1),X2),X3) = product(product(difference(quotient(X0,X1),quotient(X2,quotient(X0,X1))),quotient(X3,X1)),X0),
inference(superposition,[],[f1816,f3396]) ).
fof(f38559,plain,
! [X2,X3,X0,X1] : product(difference(quotient(X0,X1),X2),X3) = product(product(difference(quotient(X0,X1),quotient(X2,X0)),quotient(X3,X1)),X1),
inference(forward_demodulation,[],[f38148,f15349]) ).
fof(f38778,plain,
! [X2,X3,X0,X1] : product(difference(quotient(X0,X1),X2),X3) = product(X1,product(quotient(X3,X1),quotient(X0,difference(X1,quotient(X2,X0))))),
inference(forward_demodulation,[],[f38559,f33969]) ).
fof(f38910,plain,
! [X2,X3,X0,X1] : product(difference(quotient(X0,X1),X2),X3) = product(X1,quotient(product(X3,X0),quotient(X2,X0))),
inference(forward_demodulation,[],[f38778,f11865]) ).
fof(f39274,plain,
! [X2,X3,X0,X1] : quotient(product(difference(X0,product(X1,X2)),X0),X3) = product(quotient(difference(product(X1,X2),difference(X0,product(X1,X2))),quotient(X3,X2)),X1),
inference(superposition,[],[f2441,f5166]) ).
fof(f39335,plain,
! [X2,X3,X0,X1,X4] : quotient(product(X4,product(X0,product(X3,X2))),X1) = product(quotient(X4,X1),product(quotient(X0,quotient(X1,X2)),X3)),
inference(superposition,[],[f11863,f2441]) ).
fof(f39381,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X4,X1),product(quotient(X0,quotient(X1,X2)),X3)) = product(quotient(X4,quotient(X1,product(X3,X2))),X0),
inference(forward_demodulation,[],[f39335,f2441]) ).
fof(f39433,plain,
! [X2,X3,X0,X1] : quotient(product(difference(X0,product(X1,X2)),X0),X3) = product(difference(X1,quotient(difference(X0,product(X1,X2)),product(X2,quotient(X3,X2)))),X1),
inference(forward_demodulation,[],[f39274,f14042]) ).
fof(f39621,plain,
! [X2,X3,X0,X1] : quotient(product(difference(X0,product(X1,X2)),X0),X3) = product(quotient(X2,quotient(X3,X2)),quotient(quotient(X0,X1),X2)),
inference(forward_demodulation,[],[f39433,f25773]) ).
fof(f39712,plain,
! [X2,X3,X0,X1] : quotient(product(difference(X0,product(X1,X2)),X0),X3) = quotient(product(X2,quotient(X0,X1)),X3),
inference(forward_demodulation,[],[f39621,f11690]) ).
fof(f39767,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(X1,X2)) = quotient(product(X2,quotient(X0,X1)),X3),
inference(forward_demodulation,[],[f39712,f31705]) ).
fof(f40382,plain,
! [X2,X3,X0,X1] : product(quotient(X0,product(X1,X2)),X3) = product(X0,product(quotient(X0,X2),difference(X1,X3))),
inference(superposition,[],[f751,f16385]) ).
fof(f42776,plain,
! [X2,X0,X1] : product(difference(X2,X1),quotient(X1,X0)) = difference(product(X2,X0),product(X0,X1)),
inference(superposition,[],[f334,f4571]) ).
fof(f42788,plain,
! [X2,X0,X1] : difference(product(X2,X0),product(X0,X1)) = product(difference(X2,product(X0,X1)),X1),
inference(superposition,[],[f334,f26]) ).
fof(f43024,plain,
! [X2,X0,X1] : difference(product(X2,X0),product(X0,X1)) = product(X1,quotient(product(X1,X2),X0)),
inference(forward_demodulation,[],[f42788,f20672]) ).
fof(f43036,plain,
! [X2,X0,X1] : product(difference(X2,X0),difference(X0,X1)) = product(difference(X2,X1),quotient(X1,X0)),
inference(forward_demodulation,[],[f42776,f2949]) ).
fof(f43330,plain,
! [X2,X0,X1] : product(difference(X2,X0),difference(X0,X1)) = product(X1,quotient(product(X1,X2),X0)),
inference(forward_demodulation,[],[f43024,f2949]) ).
fof(f44049,plain,
! [X2,X3,X0,X1] : product(difference(X2,X3),difference(X3,product(quotient(X0,X2),X1))) = product(product(quotient(X0,X2),X1),quotient(product(X0,product(X1,X2)),X3)),
inference(superposition,[],[f43330,f424]) ).
fof(f44206,plain,
! [X2,X3,X0,X1] : product(difference(X3,difference(X1,X2)),difference(difference(X1,X2),difference(X2,X0))) = product(difference(X3,product(X0,quotient(product(X0,X1),X2))),difference(X2,X0)),
inference(superposition,[],[f4074,f43330]) ).
fof(f44246,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(product(X2,X0),X1)) = difference(product(X4,X2),product(product(X4,X3),product(difference(X0,X1),difference(X1,X2)))),
inference(superposition,[],[f157,f43330]) ).
fof(f44386,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(product(X2,X0),X1)) = product(difference(quotient(product(X4,X2),difference(X0,X1)),product(X4,X3)),difference(X1,X2)),
inference(forward_demodulation,[],[f44246,f14314]) ).
fof(f44422,plain,
! [X2,X3,X0,X1] : product(difference(X3,difference(X1,X2)),difference(difference(X1,X2),difference(X2,X0))) = product(quotient(product(X0,X1),X2),quotient(product(difference(X2,X0),X3),X0)),
inference(forward_demodulation,[],[f44206,f12443]) ).
fof(f44565,plain,
! [X2,X3,X0,X1] : product(difference(X2,X3),difference(X3,product(quotient(X0,X2),X1))) = product(X0,product(X1,difference(X2,quotient(product(X0,product(X1,X2)),X3)))),
inference(forward_demodulation,[],[f44049,f751]) ).
fof(f44709,plain,
! [X2,X3,X0,X1,X4] : product(X3,quotient(product(X2,X0),X1)) = product(X3,quotient(product(difference(X1,X2),quotient(product(X4,X2),difference(X0,X1))),X4)),
inference(forward_demodulation,[],[f44386,f12443]) ).
fof(f44736,plain,
! [X2,X3,X0,X1] : product(difference(X3,difference(X1,X2)),difference(difference(X1,X2),difference(X2,X0))) = product(quotient(X0,X2),difference(difference(X0,product(X3,X2)),product(X0,X1))),
inference(forward_demodulation,[],[f44422,f13370]) ).
fof(f44855,plain,
! [X2,X3,X0,X1] : product(difference(X2,X3),difference(X3,product(quotient(X0,X2),X1))) = product(X0,product(X1,difference(X2,product(quotient(X0,quotient(X3,X2)),X1)))),
inference(forward_demodulation,[],[f44565,f2441]) ).
fof(f44968,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X2,X0),X1)) = product(difference(X0,X1),difference(X2,product(X3,difference(X1,X2)))),
inference(forward_demodulation,[],[f44709,f21547]) ).
fof(f44986,plain,
! [X2,X3,X0,X1] : product(difference(X3,difference(X1,X2)),difference(difference(X1,X2),difference(X2,X0))) = product(difference(X3,quotient(X0,X2)),difference(X0,product(X0,X1))),
inference(forward_demodulation,[],[f44736,f15120]) ).
fof(f45077,plain,
! [X2,X3,X0,X1] : product(difference(X2,X3),difference(X3,product(quotient(X0,X2),X1))) = product(quotient(X0,product(X2,quotient(X3,X2))),product(X1,X1)),
inference(forward_demodulation,[],[f44855,f17010]) ).
fof(f45165,plain,
! [X2,X3,X0,X1] : product(X3,quotient(product(X2,X0),X1)) = product(X3,difference(difference(X1,product(X0,X2)),X2)),
inference(forward_demodulation,[],[f44968,f13592]) ).
fof(f45177,plain,
! [X2,X3,X0,X1] : product(difference(X3,difference(X1,X2)),difference(difference(X1,X2),difference(X2,X0))) = product(X0,difference(X0,product(difference(X3,quotient(X0,X2)),X1))),
inference(forward_demodulation,[],[f44986,f3025]) ).
fof(f45251,plain,
! [X2,X3,X0,X1] : product(quotient(X0,product(X2,quotient(X3,X2))),X1) = product(difference(X2,X3),difference(X3,product(quotient(X0,X2),X1))),
inference(forward_demodulation,[],[f45077,f26]) ).
fof(f45328,plain,
! [X2,X3,X0,X1] : product(difference(X3,difference(X1,X2)),difference(difference(X1,X2),difference(X2,X0))) = product(difference(X3,quotient(X0,X2)),X1),
inference(forward_demodulation,[],[f45177,f22]) ).
fof(f45379,plain,
! [X2,X3,X0,X1] : product(quotient(X0,product(X2,quotient(X3,X2))),X1) = product(difference(X2,product(X3,quotient(X0,X2))),X1),
inference(forward_demodulation,[],[f45251,f15578]) ).
fof(f45423,plain,
! [X2,X3,X0,X1] : product(difference(X3,quotient(X0,X2)),X1) = difference(X2,product(difference(product(X1,X3),X2),difference(X2,X0))),
inference(forward_demodulation,[],[f45328,f18064]) ).
fof(f45451,plain,
! [X2,X3,X0,X1] : product(quotient(X0,X2),quotient(product(X1,X2),X3)) = product(quotient(X0,product(X2,quotient(X3,X2))),X1),
inference(forward_demodulation,[],[f45379,f20672]) ).
fof(f45476,plain,
! [X2,X3,X0,X1] : product(difference(X3,quotient(X0,X2)),X1) = quotient(product(difference(X2,X0),product(X1,X3)),X2),
inference(forward_demodulation,[],[f45423,f10573]) ).
fof(f45505,plain,
! [X2,X3,X0,X1] : product(difference(X3,quotient(X0,X2)),X1) = product(quotient(difference(X2,X0),quotient(X2,X3)),X1),
inference(forward_demodulation,[],[f45476,f2441]) ).
fof(f46514,plain,
! [X2,X3,X0,X1] : difference(X3,product(product(X0,X1),X2)) = product(difference(X3,product(X0,quotient(X2,difference(X1,X3)))),X3),
inference(superposition,[],[f3245,f1361]) ).
fof(f46577,plain,
! [X2,X3,X0,X1] : difference(X3,product(product(X0,X1),X2)) = product(quotient(X2,difference(X1,X3)),quotient(X3,X0)),
inference(forward_demodulation,[],[f46514,f11036]) ).
fof(f46747,plain,
! [X2,X3,X0,X1] : product(X1,difference(difference(X0,X3),X2)) = product(quotient(X2,difference(X1,X3)),quotient(X3,X0)),
inference(forward_demodulation,[],[f46577,f2919]) ).
fof(f47129,plain,
! [X2,X3,X0,X1,X4] : difference(product(X2,product(X3,X4)),product(product(X0,X3),product(X1,X4))) = product(difference(X2,product(X0,X1)),product(X3,X4)),
inference(superposition,[],[f13188,f158]) ).
fof(f47189,plain,
! [X2,X3,X0,X1] : difference(product(X0,difference(difference(X0,X1),X2)),X3) = difference(X1,product(quotient(X3,difference(difference(X0,X1),X2)),X2)),
inference(superposition,[],[f12673,f13188]) ).
fof(f47193,plain,
! [X2,X3,X0,X1] : difference(product(quotient(X0,X1),difference(X1,X2)),X3) = difference(X0,product(quotient(X3,difference(X1,X2)),X2)),
inference(superposition,[],[f12709,f13188]) ).
fof(f47342,plain,
! [X2,X3,X0,X1] : difference(X0,product(X1,difference(X2,X3))) = difference(product(quotient(X0,X1),difference(X1,X2)),X3),
inference(forward_demodulation,[],[f47193,f2629]) ).
fof(f47346,plain,
! [X2,X3,X0,X1] : difference(product(X0,difference(difference(X0,X1),X2)),X3) = difference(X1,product(difference(X0,X1),difference(X2,X3))),
inference(forward_demodulation,[],[f47189,f2629]) ).
fof(f47386,plain,
! [X2,X3,X0,X1,X4] : difference(product(X2,product(X3,X4)),product(product(X0,X3),product(X1,X4))) = product(X1,quotient(product(product(X3,X4),X2),X0)),
inference(forward_demodulation,[],[f47129,f20672]) ).
fof(f47442,plain,
! [X2,X3,X0,X1] : difference(X0,product(X1,difference(X2,X3))) = product(X1,difference(difference(X1,X2),difference(X0,X3))),
inference(forward_demodulation,[],[f47342,f13424]) ).
fof(f47444,plain,
! [X2,X3,X0,X1] : difference(product(X0,difference(difference(X0,X1),X2)),X3) = quotient(product(difference(X2,X3),X0),X1),
inference(forward_demodulation,[],[f47346,f10573]) ).
fof(f47477,plain,
! [X2,X3,X0,X1,X4] : difference(product(X2,product(X3,X4)),product(product(X0,X3),product(X1,X4))) = product(X1,product(X3,quotient(X2,difference(X4,X0)))),
inference(forward_demodulation,[],[f47386,f2001]) ).
fof(f47515,plain,
! [X2,X3,X0,X1] : difference(X0,product(X1,difference(X2,X3))) = difference(X2,product(X1,difference(X0,X3))),
inference(forward_demodulation,[],[f47442,f3535]) ).
fof(f47516,plain,
! [X2,X3,X0,X1] : difference(difference(X1,product(X0,X2)),X3) = quotient(product(difference(X2,X3),X0),X1),
inference(forward_demodulation,[],[f47444,f3535]) ).
fof(f47538,plain,
! [X2,X3,X0,X1,X4] : product(X1,product(X3,quotient(X2,difference(X4,X0)))) = product(difference(quotient(product(X2,product(X3,X4)),X1),product(X0,X3)),X4),
inference(forward_demodulation,[],[f47477,f14314]) ).
fof(f47571,plain,
! [X2,X3,X0,X1,X4] : product(X1,product(X3,quotient(X2,difference(X4,X0)))) = product(X3,quotient(product(X4,quotient(product(X2,product(X3,X4)),X1)),X0)),
inference(forward_demodulation,[],[f47538,f20672]) ).
fof(f47591,plain,
! [X2,X3,X0,X1,X4] : product(X1,product(X3,quotient(X2,difference(X4,X0)))) = product(X3,difference(difference(X0,product(X2,product(X3,X4))),product(X1,X4))),
inference(forward_demodulation,[],[f47571,f39767]) ).
fof(f47603,plain,
! [X2,X3,X0,X1,X4] : product(X1,product(X3,quotient(X2,difference(X4,X0)))) = product(X3,difference(product(difference(quotient(X0,X3),X2),X4),product(X1,X4))),
inference(forward_demodulation,[],[f47591,f14314]) ).
fof(f47607,plain,
! [X2,X3,X0,X1,X4] : product(X1,product(X3,quotient(X2,difference(X4,X0)))) = product(X3,product(difference(difference(quotient(X0,X3),X2),X1),difference(X4,X4))),
inference(forward_demodulation,[],[f47603,f2949]) ).
fof(f47611,plain,
! [X2,X3,X0,X1,X4] : product(X1,product(X3,quotient(X2,difference(X4,X0)))) = product(X3,product(difference(difference(quotient(X0,X3),X2),X1),X4)),
inference(forward_demodulation,[],[f47607,f47]) ).
fof(f48316,plain,
! [X2,X3,X0,X1] : product(product(quotient(X3,X1),difference(X1,product(X2,X0))),X3) = product(quotient(X3,X1),product(X0,quotient(X1,X2))),
inference(superposition,[],[f531,f11036]) ).
fof(f48989,plain,
! [X2,X3,X0,X1] : product(quotient(X3,X1),product(X0,quotient(X1,X2))) = product(X3,product(difference(X1,product(X2,X0)),difference(X1,X3))),
inference(forward_demodulation,[],[f48316,f751]) ).
fof(f49346,plain,
! [X2,X3,X0,X1] : product(quotient(X3,X1),product(X0,quotient(X1,X2))) = product(product(X2,X0),difference(X1,X3)),
inference(forward_demodulation,[],[f48989,f1148]) ).
fof(f50569,plain,
! [X0,X1] : product(b,quotient(X0,difference(quotient(a,b),X1))) = quotient(product(difference(c1,b),X0),X1),
inference(superposition,[],[f2001,f36593]) ).
fof(f50599,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(X1,difference(quotient(X3,X2),X4))) = quotient(product(product(X0,quotient(X1,X2)),X3),X4),
inference(superposition,[],[f2001,f1816]) ).
fof(f50601,plain,
! [X2,X3,X0,X1,X4] : quotient(product(X0,product(X1,difference(X2,X3))),X4) = product(quotient(X0,X2),quotient(X3,difference(X1,X4))),
inference(superposition,[],[f2001,f751]) ).
fof(f50615,plain,
! [X2,X0,X1] : quotient(product(X0,X1),X2) = product(X0,quotient(product(X0,X1),difference(X1,X2))),
inference(superposition,[],[f2001,f26]) ).
fof(f50721,plain,
! [X2,X3,X0,X1,X4] : product(quotient(product(X0,X2),X3),quotient(X1,X4)) = product(X0,quotient(X1,difference(X2,product(X3,X4)))),
inference(superposition,[],[f1974,f2001]) ).
fof(f50839,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X0,X2),quotient(X3,difference(X1,X4))) = product(quotient(X0,quotient(X4,difference(X2,X3))),X1),
inference(forward_demodulation,[],[f50601,f2441]) ).
fof(f50841,plain,
! [X2,X3,X0,X1,X4] : product(X0,quotient(X1,difference(quotient(X3,X2),X4))) = product(X0,quotient(X3,difference(quotient(X1,X2),X4))),
inference(forward_demodulation,[],[f50599,f2001]) ).
fof(f50871,plain,
! [X0,X1] : product(b,quotient(X0,difference(quotient(a,b),X1))) = difference(difference(X1,product(X0,c1)),b),
inference(forward_demodulation,[],[f50569,f47516]) ).
fof(f54370,plain,
! [X2,X3,X0,X1] : product(quotient(X2,X1),difference(X3,product(X1,X0))) = product(product(difference(X0,X1),X0),difference(X3,X2)),
inference(superposition,[],[f2567,f4364]) ).
fof(f54845,plain,
! [X2,X3,X0,X1] : product(quotient(X2,X1),difference(X3,product(X1,X0))) = product(X0,quotient(product(difference(X3,X2),X0),X1)),
inference(forward_demodulation,[],[f54370,f19885]) ).
fof(f55024,plain,
! [X2,X3,X0,X1] : product(quotient(X2,X1),difference(X3,product(X1,X0))) = product(X0,difference(difference(X1,product(X0,X3)),X2)),
inference(forward_demodulation,[],[f54845,f47516]) ).
fof(f55138,plain,
! [X2,X3,X0,X1] : product(X0,difference(difference(X1,product(X0,X3)),X2)) = product(X1,difference(X3,product(quotient(X2,X1),X0))),
inference(forward_demodulation,[],[f55024,f3025]) ).
fof(f57469,plain,
! [X2,X3,X0,X1,X4] : quotient(product(X3,product(quotient(X0,X1),X2)),X4) = product(quotient(X3,quotient(X4,X0)),quotient(product(X0,X2),X1)),
inference(superposition,[],[f2441,f2563]) ).
fof(f57553,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X3,quotient(X4,X2)),quotient(X0,X1)) = product(quotient(X3,quotient(X4,X0)),quotient(product(X0,X2),X1)),
inference(forward_demodulation,[],[f57469,f2441]) ).
fof(f59205,plain,
! [X2,X3,X0,X1] : difference(X2,difference(X0,product(X1,X3))) = difference(X0,product(difference(X0,X1),difference(X2,X3))),
inference(superposition,[],[f10349,f2949]) ).
fof(f60249,plain,
! [X2,X3,X0,X1] : product(difference(difference(X3,X0),quotient(product(X3,X2),X1)),difference(X3,X0)) = difference(difference(X3,X0),product(quotient(X0,X1),X2)),
inference(superposition,[],[f3245,f2558]) ).
fof(f60260,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = product(quotient(product(X3,X2),X1),quotient(difference(X3,X0),quotient(product(X3,X2),X1))),
inference(superposition,[],[f5458,f2558]) ).
fof(f60276,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = product(X3,quotient(difference(X3,X0),difference(X2,product(X1,quotient(product(X3,X2),X1))))),
inference(forward_demodulation,[],[f60260,f50721]) ).
fof(f60285,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = difference(X3,product(quotient(product(X3,X2),X1),quotient(X0,X3))),
inference(forward_demodulation,[],[f60249,f22775]) ).
fof(f60502,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = quotient(X0,product(X3,difference(X2,product(X1,quotient(product(X3,X2),X1))))),
inference(forward_demodulation,[],[f60276,f10470]) ).
fof(f60510,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = difference(X3,product(X3,quotient(X0,difference(X2,product(X1,X3))))),
inference(forward_demodulation,[],[f60285,f50721]) ).
fof(f60653,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = product(quotient(quotient(X0,product(X1,quotient(product(X3,X2),X1))),X3),X2),
inference(forward_demodulation,[],[f60502,f17174]) ).
fof(f60660,plain,
! [X2,X3,X0,X1] : quotient(X0,difference(X2,product(X1,X3))) = difference(difference(X3,X0),product(quotient(X0,X1),X2)),
inference(forward_demodulation,[],[f60510,f21]) ).
fof(f60758,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = product(quotient(quotient(X0,product(difference(X2,X1),X3)),X3),X2),
inference(forward_demodulation,[],[f60653,f12559]) ).
fof(f60830,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = product(quotient(product(X2,quotient(difference(X1,X0),X3)),X3),X2),
inference(forward_demodulation,[],[f60758,f17388]) ).
fof(f60867,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = product(quotient(X2,X3),quotient(difference(X1,X0),X3)),
inference(forward_demodulation,[],[f60830,f2563]) ).
fof(f60887,plain,
! [X2,X3,X0,X1] : difference(difference(X3,X0),product(quotient(X0,X1),X2)) = quotient(product(X2,difference(X1,X0)),X3),
inference(forward_demodulation,[],[f60867,f11863]) ).
fof(f60901,plain,
! [X2,X3,X0,X1] : quotient(X0,difference(X2,product(X1,X3))) = quotient(product(X2,difference(X1,X0)),X3),
inference(forward_demodulation,[],[f60887,f60660]) ).
fof(f61270,plain,
! [X2,X3,X0,X1,X4] : product(X1,quotient(X3,difference(difference(quotient(X0,X1),X2),X4))) = quotient(product(difference(quotient(X0,X1),product(X0,X2)),X3),X4),
inference(superposition,[],[f2001,f3122]) ).
fof(f61387,plain,
! [X2,X3,X0,X1,X4] : product(X1,quotient(X3,difference(difference(quotient(X0,X1),X2),X4))) = difference(difference(X4,product(X3,quotient(X0,X1))),product(X0,X2)),
inference(forward_demodulation,[],[f61270,f47516]) ).
fof(f64564,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X1,X0),quotient(X3,difference(quotient(X0,X2),X4))) = quotient(product(product(difference(X0,X1),quotient(X1,X2)),X3),X4),
inference(superposition,[],[f2001,f4443]) ).
fof(f64631,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X1,X0),quotient(X3,difference(quotient(X0,X2),X4))) = product(difference(X0,X1),quotient(X3,difference(quotient(X1,X2),X4))),
inference(forward_demodulation,[],[f64564,f2001]) ).
fof(f64961,plain,
! [X2,X3,X0,X1,X4] : product(difference(X0,X1),quotient(X3,difference(quotient(X1,X2),X4))) = product(quotient(X1,quotient(X4,X0)),quotient(X3,X2)),
inference(forward_demodulation,[],[f64631,f16670]) ).
fof(f66115,plain,
! [X2,X3,X0,X1] : difference(product(difference(X0,difference(X0,X1)),X2),X3) = product(X0,difference(X2,difference(quotient(quotient(X0,X1),X0),X3))),
inference(superposition,[],[f2992,f20231]) ).
fof(f66480,plain,
! [X2,X3,X0,X1] : difference(product(difference(X0,difference(X0,X1)),X2),X3) = product(X0,difference(X2,difference(X0,quotient(product(X3,X1),X0)))),
inference(forward_demodulation,[],[f66115,f15129]) ).
fof(f66632,plain,
! [X2,X3,X0,X1] : difference(product(difference(X0,difference(X0,X1)),X2),X3) = difference(product(X0,X2),quotient(product(X3,X1),X0)),
inference(forward_demodulation,[],[f66480,f3566]) ).
fof(f67056,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X3,difference(X0,X2)),X4) = quotient(product(X3,product(X4,difference(X2,X1))),product(difference(X0,X1),quotient(X1,X2))),
inference(superposition,[],[f265,f43036]) ).
fof(f67182,plain,
! [X2,X3,X0,X1,X4] : quotient(product(product(difference(X0,X1),difference(X1,X2)),X3),X4) = product(difference(X0,X2),quotient(X3,difference(quotient(X2,X1),X4))),
inference(superposition,[],[f2001,f43036]) ).
fof(f67249,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X2,quotient(X4,X0)),quotient(X3,X1)) = quotient(product(product(difference(X0,X1),difference(X1,X2)),X3),X4),
inference(forward_demodulation,[],[f67182,f64961]) ).
fof(f67374,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X3,difference(X0,X2)),X4) = product(quotient(X3,difference(X0,X1)),quotient(product(X4,difference(X2,X1)),quotient(X1,X2))),
inference(forward_demodulation,[],[f67056,f1974]) ).
fof(f67603,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X2,quotient(X4,X0)),quotient(X3,X1)) = product(difference(X0,X1),quotient(X3,difference(difference(X1,X2),X4))),
inference(forward_demodulation,[],[f67249,f2001]) ).
fof(f67711,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X3,difference(X0,X2)),X4) = product(quotient(X3,difference(X0,X1)),quotient(X1,difference(X4,product(X2,quotient(X1,X2))))),
inference(forward_demodulation,[],[f67374,f2050]) ).
fof(f67992,plain,
! [X2,X3,X0,X1,X4] : product(quotient(X3,difference(X0,X2)),X4) = product(X0,difference(difference(difference(X4,product(X2,quotient(X1,X2))),X1),X3)),
inference(forward_demodulation,[],[f67711,f46747]) ).
fof(f68225,plain,
! [X2,X3,X0,X4] : product(quotient(X3,difference(X0,X2)),X4) = product(X0,difference(quotient(product(X2,X2),X4),X3)),
inference(forward_demodulation,[],[f67992,f33433]) ).
fof(f68401,plain,
! [X2,X3,X0,X4] : product(quotient(X3,difference(X0,X2)),X4) = product(X0,difference(quotient(X2,X4),X3)),
inference(forward_demodulation,[],[f68225,f26]) ).
fof(f72785,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = quotient(product(product(X0,X1),product(X2,X3)),quotient(product(X2,X3),product(product(X2,X0),product(X3,X1)))),
inference(superposition,[],[f6553,f157]) ).
fof(f73094,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = difference(product(product(X2,X0),product(X3,X1)),product(product(X2,X3),product(X0,X1))),
inference(forward_demodulation,[],[f72785,f12239]) ).
fof(f73237,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(difference(quotient(product(product(X2,X0),product(X3,X1)),X0),product(X2,X3)),X1),
inference(forward_demodulation,[],[f73094,f14314]) ).
fof(f73346,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X3,quotient(product(X1,quotient(product(product(X2,X0),product(X3,X1)),X0)),X2)),
inference(forward_demodulation,[],[f73237,f20672]) ).
fof(f73446,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X3,difference(difference(X2,product(product(X2,X0),product(X3,X1))),product(X0,X1))),
inference(forward_demodulation,[],[f73346,f39767]) ).
fof(f73517,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X3,difference(product(difference(quotient(X2,X3),product(X2,X0)),X1),product(X0,X1))),
inference(forward_demodulation,[],[f73446,f14314]) ).
fof(f73564,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X3,product(difference(difference(quotient(X2,X3),product(X2,X0)),X0),difference(X1,X1))),
inference(forward_demodulation,[],[f73517,f2949]) ).
fof(f73599,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X0,product(X3,quotient(product(X2,X0),difference(difference(X1,X1),X2)))),
inference(forward_demodulation,[],[f73564,f47611]) ).
fof(f73623,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X0,product(X3,quotient(product(difference(X1,X1),X0),X2))),
inference(forward_demodulation,[],[f73599,f24845]) ).
fof(f73642,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X0,product(X3,difference(difference(X2,product(X0,X1)),X1))),
inference(forward_demodulation,[],[f73623,f47516]) ).
fof(f73653,plain,
! [X2,X3,X0,X1] : product(product(X2,X0),product(X3,X1)) = product(X0,product(X3,quotient(product(X1,X0),X2))),
inference(forward_demodulation,[],[f73642,f45165]) ).
fof(f74857,plain,
! [X2,X0,X1] : difference(product(X2,quotient(X0,quotient(X1,X0))),X1) = product(difference(X2,X1),difference(X0,quotient(X1,X0))),
inference(superposition,[],[f3735,f8455]) ).
fof(f74969,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X1,X0)),quotient(X1,X0)) = product(difference(X2,X1),difference(X0,quotient(X1,X0))),
inference(forward_demodulation,[],[f74857,f13198]) ).
fof(f80672,plain,
! [X2,X0,X1] : quotient(quotient(X0,X1),X2) = product(X1,quotient(quotient(X0,X1),difference(quotient(difference(X1,X0),X1),X2))),
inference(superposition,[],[f50615,f6583]) ).
fof(f80775,plain,
! [X0] : quotient(a,X0) = product(b,quotient(a,difference(quotient(c1,b),X0))),
inference(superposition,[],[f50615,f5795]) ).
fof(f81162,plain,
! [X0] : quotient(a,X0) = product(b,quotient(c1,difference(quotient(a,b),X0))),
inference(forward_demodulation,[],[f80775,f50841]) ).
fof(f81265,plain,
! [X2,X0,X1] : quotient(quotient(X0,X1),X2) = product(X1,quotient(difference(X1,X0),difference(quotient(quotient(X0,X1),X1),X2))),
inference(forward_demodulation,[],[f80672,f50841]) ).
fof(f81444,plain,
! [X0] : quotient(a,X0) = difference(difference(X0,product(c1,c1)),b),
inference(forward_demodulation,[],[f81162,f50871]) ).
fof(f81531,plain,
! [X2,X0,X1] : quotient(quotient(X0,X1),X2) = quotient(X0,product(X1,difference(quotient(quotient(X0,X1),X1),X2))),
inference(forward_demodulation,[],[f81265,f10470]) ).
fof(f81679,plain,
! [X0] : quotient(a,X0) = difference(difference(X0,c1),b),
inference(forward_demodulation,[],[f81444,f26]) ).
fof(f81749,plain,
! [X2,X0,X1] : quotient(quotient(X0,X1),X2) = product(quotient(quotient(X0,X2),X1),quotient(quotient(X0,X1),X1)),
inference(forward_demodulation,[],[f81531,f17174]) ).
fof(f81913,plain,
! [X2,X0,X1] : quotient(quotient(X0,X1),X2) = quotient(product(quotient(X0,X2),quotient(X0,X1)),X1),
inference(forward_demodulation,[],[f81749,f11863]) ).
fof(f82040,plain,
! [X2,X0,X1] : quotient(quotient(X0,X1),X2) = difference(difference(X1,X0),product(X1,quotient(X0,X2))),
inference(forward_demodulation,[],[f81913,f39767]) ).
fof(f82351,plain,
! [X0] : difference(X0,b) = quotient(a,quotient(c1,X0)),
inference(superposition,[],[f81679,f61]) ).
fof(f84360,plain,
! [X2,X3,X0,X1] : quotient(product(X0,difference(difference(X1,X0),X2)),X3) = product(difference(X0,X1),quotient(product(X0,difference(difference(X1,X0),X2)),difference(difference(X1,X2),X3))),
inference(superposition,[],[f50615,f22042]) ).
fof(f84361,plain,
! [X2,X3,X0,X1] : quotient(product(X0,difference(difference(X1,X0),X2)),X3) = product(quotient(X2,quotient(X3,X0)),quotient(product(X0,difference(difference(X1,X0),X2)),X1)),
inference(forward_demodulation,[],[f84360,f67603]) ).
fof(f84719,plain,
! [X2,X3,X0,X1] : quotient(product(X0,difference(difference(X1,X0),X2)),X3) = product(quotient(X2,quotient(X3,difference(difference(X1,X0),X2))),quotient(X0,X1)),
inference(forward_demodulation,[],[f84361,f57553]) ).
fof(f85035,plain,
! [X2,X3,X0,X1] : quotient(product(X0,difference(difference(X1,X0),X2)),X3) = product(quotient(X2,difference(X1,X0)),quotient(X2,difference(quotient(X0,X1),X3))),
inference(forward_demodulation,[],[f84719,f50839]) ).
fof(f85267,plain,
! [X2,X3,X0,X1] : quotient(product(X0,difference(difference(X1,X0),X2)),X3) = quotient(X2,product(difference(X1,X0),difference(quotient(X0,X1),X3))),
inference(forward_demodulation,[],[f85035,f16385]) ).
fof(f85418,plain,
! [X2,X3,X0,X1] : quotient(product(X0,difference(difference(X1,X0),X2)),X3) = product(quotient(quotient(X2,X3),difference(X1,X0)),quotient(X0,X1)),
inference(forward_demodulation,[],[f85267,f17174]) ).
fof(f85519,plain,
! [X2,X3,X0,X1] : difference(X0,product(X1,quotient(X2,X3))) = quotient(product(X0,difference(difference(X1,X0),X2)),X3),
inference(forward_demodulation,[],[f85418,f30838]) ).
fof(f85586,plain,
! [X2,X3,X0,X1] : difference(X0,product(X1,quotient(X2,X3))) = quotient(X2,difference(X0,product(difference(X1,X0),X3))),
inference(forward_demodulation,[],[f85519,f60901]) ).
fof(f85629,plain,
! [X2,X3,X0,X1] : difference(X0,product(X1,quotient(X2,X3))) = quotient(X2,quotient(product(X3,X1),X0)),
inference(forward_demodulation,[],[f85586,f33925]) ).
fof(f85713,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(product(quotient(X0,product(X1,quotient(X2,X1))),quotient(difference(X2,X0),quotient(X2,X1))),product(quotient(difference(X2,X0),quotient(X2,X1)),difference(X2,X0))),
inference(superposition,[],[f185,f16396]) ).
fof(f85858,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(difference(product(product(X1,quotient(X0,X1)),quotient(X0,X1)),X2),difference(product(quotient(X0,X1),X0),X3)),
inference(superposition,[],[f2949,f185]) ).
fof(f85880,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X0,X1)),X2) = product(product(quotient(X0,X1),X0),quotient(X2,product(product(X1,quotient(X0,X1)),quotient(X0,X1)))),
inference(superposition,[],[f11036,f185]) ).
fof(f85891,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X0,X1)),X2) = product(X0,product(X0,difference(X1,quotient(X2,product(product(X1,quotient(X0,X1)),quotient(X0,X1)))))),
inference(forward_demodulation,[],[f85880,f751]) ).
fof(f85913,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(difference(product(product(X1,quotient(X0,X1)),quotient(X0,X1)),X2),product(X1,difference(X0,difference(X0,X3)))),
inference(forward_demodulation,[],[f85858,f13424]) ).
fof(f86046,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(X0,product(quotient(difference(X2,X0),quotient(X2,X1)),difference(product(X1,quotient(X2,X1)),product(quotient(difference(X2,X0),quotient(X2,X1)),difference(X2,X0))))),
inference(forward_demodulation,[],[f85713,f751]) ).
fof(f86066,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X0,X1)),X2) = product(X0,product(X0,difference(X1,quotient(X2,product(X1,quotient(X0,difference(X0,X1))))))),
inference(forward_demodulation,[],[f85891,f12601]) ).
fof(f86088,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(product(difference(product(X1,quotient(X0,X1)),quotient(X2,X0)),X1),product(X1,difference(X0,difference(X0,X3)))),
inference(forward_demodulation,[],[f85913,f13198]) ).
fof(f86221,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(X0,product(difference(X1,quotient(X0,X2)),difference(product(X1,quotient(X2,X1)),product(quotient(difference(X2,X0),quotient(X2,X1)),difference(X2,X0))))),
inference(forward_demodulation,[],[f86046,f45505]) ).
fof(f86241,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X0,X1)),X2) = product(X0,quotient(X2,product(difference(X0,X1),quotient(X0,difference(X0,X1))))),
inference(forward_demodulation,[],[f86066,f12280]) ).
fof(f86263,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(product(product(difference(X1,quotient(quotient(X2,X0),X0)),X1),X1),product(X1,difference(X0,difference(X0,X3)))),
inference(forward_demodulation,[],[f86088,f13198]) ).
fof(f86390,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(X0,product(difference(difference(X2,X1),quotient(X0,X2)),difference(X1,product(quotient(difference(X2,X0),quotient(X2,X1)),difference(X2,X0))))),
inference(forward_demodulation,[],[f86221,f13084]) ).
fof(f86409,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X0,X1)),X2) = product(quotient(product(X0,X0),difference(X0,X1)),quotient(X2,X0)),
inference(forward_demodulation,[],[f86241,f5541]) ).
fof(f86431,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(X1,product(X1,product(quotient(difference(X0,difference(X0,X3)),difference(X1,quotient(quotient(X2,X0),X0))),X1))),
inference(forward_demodulation,[],[f86263,f28009]) ).
fof(f86551,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(X0,product(difference(difference(X2,X1),quotient(X0,X2)),difference(X1,product(quotient(X0,quotient(X2,X1)),difference(X2,difference(X2,X0)))))),
inference(forward_demodulation,[],[f86390,f2567]) ).
fof(f86570,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X0,X1)),X2) = product(X0,difference(quotient(X1,quotient(X2,X0)),product(X0,X0))),
inference(forward_demodulation,[],[f86409,f68401]) ).
fof(f86592,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(X1,product(X1,product(X1,difference(quotient(quotient(quotient(X2,X0),X0),X1),difference(X0,difference(X0,X3)))))),
inference(forward_demodulation,[],[f86431,f30527]) ).
fof(f86704,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(quotient(X0,product(X1,quotient(X2,X1))),product(difference(difference(X2,X1),quotient(X0,X2)),difference(X2,difference(X2,X0)))),
inference(forward_demodulation,[],[f86551,f17010]) ).
fof(f86723,plain,
! [X2,X0,X1] : product(difference(X2,quotient(X0,X1)),X2) = product(X0,difference(quotient(X1,quotient(X2,X0)),X0)),
inference(forward_demodulation,[],[f86570,f3024]) ).
fof(f86744,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(X1,product(quotient(product(X1,difference(X0,difference(X0,X3))),quotient(quotient(X2,X0),X0)),X1)),
inference(forward_demodulation,[],[f86592,f11988]) ).
fof(f86849,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(quotient(X0,X1),quotient(product(product(difference(difference(X2,X1),quotient(X0,X2)),difference(X2,difference(X2,X0))),X1),X2)),
inference(forward_demodulation,[],[f86704,f45451]) ).
fof(f86887,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(X1,product(quotient(X1,quotient(quotient(X2,X0),X0)),difference(X0,difference(X0,X3)))),
inference(forward_demodulation,[],[f86744,f2563]) ).
fof(f86987,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(quotient(X0,X1),product(difference(difference(X2,X1),quotient(X0,X2)),quotient(X1,difference(difference(X2,difference(X2,X0)),X2)))),
inference(forward_demodulation,[],[f86849,f2001]) ).
fof(f87024,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(quotient(X1,product(X0,quotient(quotient(X2,X0),X0))),difference(X0,X3)),
inference(forward_demodulation,[],[f86887,f40382]) ).
fof(f87115,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(product(difference(difference(X2,difference(X2,X0)),X2),difference(difference(X2,X1),quotient(X0,X2))),difference(X1,X0)),
inference(forward_demodulation,[],[f86987,f49346]) ).
fof(f87149,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(quotient(X1,X0),quotient(product(difference(X0,X3),X0),quotient(X2,X0))),
inference(forward_demodulation,[],[f87024,f45451]) ).
fof(f87227,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(quotient(X0,X2),product(quotient(difference(X1,X0),quotient(X2,difference(X2,X1))),difference(X2,difference(X2,X0)))),
inference(forward_demodulation,[],[f87115,f24550]) ).
fof(f87260,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(difference(quotient(X0,quotient(X1,X0)),X2),difference(X0,X3)),
inference(forward_demodulation,[],[f87149,f38910]) ).
fof(f87330,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(quotient(X0,quotient(X2,product(difference(X2,difference(X2,X0)),difference(X2,X1)))),difference(X1,X0)),
inference(forward_demodulation,[],[f87227,f39381]) ).
fof(f87360,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(quotient(X1,X0),difference(difference(quotient(X2,X0),X0),X3)),
inference(forward_demodulation,[],[f87260,f14675]) ).
fof(f87426,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(difference(product(difference(X2,difference(X2,X0)),difference(X2,X1)),X0),difference(X1,quotient(X0,X2))),
inference(forward_demodulation,[],[f87330,f13146]) ).
fof(f87453,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = product(X0,difference(difference(quotient(X2,X0),quotient(X0,X3)),X1)),
inference(forward_demodulation,[],[f87360,f15237]) ).
fof(f87505,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(difference(product(X2,difference(X2,X1)),quotient(product(X0,X0),X2)),difference(X1,quotient(X0,X2))),
inference(forward_demodulation,[],[f87426,f66632]) ).
fof(f87529,plain,
! [X2,X3,X0,X1] : difference(quotient(X0,X1),product(X2,X3)) = difference(quotient(X0,X3),product(X2,X1)),
inference(forward_demodulation,[],[f87453,f13691]) ).
fof(f87573,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = difference(product(product(X2,difference(X2,X1)),X1),quotient(product(product(X0,X0),X0),X2)),
inference(forward_demodulation,[],[f87505,f12774]) ).
fof(f87626,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = difference(product(product(X2,difference(X2,X1)),X1),product(X0,quotient(X0,difference(X0,X2)))),
inference(forward_demodulation,[],[f87573,f2001]) ).
fof(f87673,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(difference(product(X2,difference(X2,X1)),X0),difference(X1,quotient(X0,difference(X0,X2)))),
inference(forward_demodulation,[],[f87626,f2949]) ).
fof(f87711,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = product(difference(product(X2,difference(X2,X1)),X0),difference(X1,difference(X0,quotient(X0,X2)))),
inference(forward_demodulation,[],[f87673,f27427]) ).
fof(f87740,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = difference(product(product(X2,difference(X2,X1)),X1),quotient(X0,X2)),
inference(forward_demodulation,[],[f87711,f12735]) ).
fof(f87763,plain,
! [X2,X0,X1] : quotient(difference(X2,X0),quotient(X2,X1)) = difference(product(X1,X1),quotient(X0,X2)),
inference(forward_demodulation,[],[f87740,f22]) ).
fof(f87783,plain,
! [X2,X0,X1] : difference(X1,quotient(X0,X2)) = quotient(difference(X2,X0),quotient(X2,X1)),
inference(forward_demodulation,[],[f87763,f26]) ).
fof(f87943,plain,
! [X2,X0,X1] : difference(X1,quotient(X2,quotient(X2,X0))) = quotient(X0,quotient(quotient(X2,X0),X1)),
inference(superposition,[],[f87783,f61]) ).
fof(f87949,plain,
! [X0] : difference(X0,quotient(product(a1,b),b)) = quotient(c,quotient(b,X0)),
inference(superposition,[],[f87783,f65]) ).
fof(f88164,plain,
! [X0] : difference(X0,a1) = quotient(c,quotient(b,X0)),
inference(forward_demodulation,[],[f87949,f23]) ).
fof(f88170,plain,
! [X2,X0,X1] : difference(X1,difference(X0,X2)) = quotient(X0,quotient(quotient(X2,X0),X1)),
inference(forward_demodulation,[],[f87943,f5303]) ).
fof(f89972,plain,
! [X0] : quotient(b1,quotient(a,X0)) = difference(X0,difference(b1,product(b1,c))),
inference(superposition,[],[f88170,f91]) ).
fof(f90173,plain,
! [X0] : difference(X0,c) = quotient(b1,quotient(a,X0)),
inference(forward_demodulation,[],[f89972,f21]) ).
fof(f90818,plain,
! [X0] : quotient(a,X0) = difference(difference(X0,c),b1),
inference(superposition,[],[f61,f90173]) ).
fof(f91014,plain,
! [X0] : difference(X0,b1) = quotient(a,quotient(c,X0)),
inference(superposition,[],[f90818,f61]) ).
fof(f91978,plain,
! [X0] : difference(quotient(b,X0),b1) = quotient(a,difference(X0,a1)),
inference(superposition,[],[f91014,f88164]) ).
fof(f93079,plain,
! [X2,X0,X1] : product(quotient(X0,quotient(X1,X2)),X2) = product(difference(product(difference(X0,X1),X0),quotient(X0,quotient(X1,X2))),product(difference(X0,X1),X0)),
inference(superposition,[],[f5166,f24760]) ).
fof(f93225,plain,
! [X2,X0,X1] : product(quotient(X0,quotient(X1,X2)),X2) = product(X0,difference(quotient(quotient(X1,X2),quotient(product(difference(X0,X1),X0),X0)),X0)),
inference(forward_demodulation,[],[f93079,f86723]) ).
fof(f93412,plain,
! [X2,X0,X1] : product(quotient(X0,quotient(X1,X2)),X2) = product(X0,difference(difference(X0,product(X0,quotient(quotient(X1,X2),difference(X0,X1)))),X0)),
inference(forward_demodulation,[],[f93225,f85629]) ).
fof(f93549,plain,
! [X2,X0,X1] : product(quotient(X0,quotient(X1,X2)),X2) = product(X0,difference(quotient(quotient(X1,X2),difference(X0,X1)),product(quotient(X0,X0),X0))),
inference(forward_demodulation,[],[f93412,f55138]) ).
fof(f93637,plain,
! [X2,X0,X1] : product(quotient(X0,quotient(X1,X2)),X2) = product(quotient(X0,X0),difference(quotient(quotient(X1,X2),difference(X0,X1)),X0)),
inference(forward_demodulation,[],[f93549,f3024]) ).
fof(f93697,plain,
! [X2,X0,X1] : product(quotient(X0,quotient(X1,X2)),X2) = product(X0,difference(quotient(quotient(X1,X2),difference(X0,X1)),X0)),
inference(forward_demodulation,[],[f93637,f3021]) ).
fof(f93741,plain,
! [X2,X0,X1] : product(quotient(X0,quotient(X1,X2)),X2) = product(X0,difference(quotient(quotient(X1,X2),X0),X1)),
inference(forward_demodulation,[],[f93697,f14909]) ).
fof(f93767,plain,
! [X2,X0,X1] : quotient(product(X0,X2),X1) = product(X0,difference(quotient(quotient(X1,X2),X0),X1)),
inference(forward_demodulation,[],[f93741,f11885]) ).
fof(f94739,plain,
difference(b2,b) = quotient(a,difference(b2,a1)),
inference(superposition,[],[f82351,f7980]) ).
fof(f94879,plain,
difference(b2,b) = difference(quotient(b,b2),b1),
inference(forward_demodulation,[],[f94739,f91978]) ).
fof(f94959,plain,
difference(b1,b) = product(b2,difference(difference(b2,b),b)),
inference(superposition,[],[f3741,f94879]) ).
fof(f94960,plain,
! [X0] : difference(b,product(b1,X0)) = product(difference(b2,b),difference(b2,X0)),
inference(superposition,[],[f12709,f94879]) ).
fof(f94986,plain,
! [X0] : product(quotient(b1,X0),quotient(b,b2)) = product(quotient(quotient(b,b2),X0),difference(b2,b)),
inference(superposition,[],[f2569,f94879]) ).
fof(f94995,plain,
difference(b1,difference(b2,b)) = difference(quotient(b,b2),product(difference(b2,b),b1)),
inference(superposition,[],[f4244,f94879]) ).
fof(f94996,plain,
product(b1,quotient(b,b2)) = product(product(difference(b2,b),quotient(b,b2)),b1),
inference(superposition,[],[f4283,f94879]) ).
fof(f95001,plain,
product(difference(b2,b),b1) = product(b1,product(difference(b2,b),quotient(b,b2))),
inference(superposition,[],[f4547,f94879]) ).
fof(f95008,plain,
quotient(quotient(b,b2),b1) = difference(b1,product(difference(b2,b),quotient(b,b2))),
inference(superposition,[],[f6554,f94879]) ).
fof(f95072,plain,
quotient(quotient(b,b2),b1) = difference(b1,product(b,quotient(product(b,b2),b2))),
inference(forward_demodulation,[],[f95008,f25913]) ).
fof(f95078,plain,
product(difference(b2,b),b1) = product(product(b2,difference(b2,b1)),b),
inference(forward_demodulation,[],[f95001,f19938]) ).
fof(f95083,plain,
product(b1,quotient(b,b2)) = product(product(b,quotient(b,b)),b1),
inference(forward_demodulation,[],[f94996,f23463]) ).
fof(f95084,plain,
difference(b1,difference(b2,b)) = difference(quotient(b,b1),product(difference(b2,b),b2)),
inference(forward_demodulation,[],[f94995,f87529]) ).
fof(f95092,plain,
! [X0] : product(quotient(b1,X0),quotient(b,b2)) = product(quotient(b,X0),difference(b2,quotient(b,b2))),
inference(forward_demodulation,[],[f94986,f2567]) ).
fof(f95109,plain,
! [X0] : difference(b,product(b1,X0)) = difference(b2,product(b,X0)),
inference(forward_demodulation,[],[f94960,f3101]) ).
fof(f95110,plain,
difference(b1,b) = difference(b,product(b2,b)),
inference(forward_demodulation,[],[f94959,f3535]) ).
fof(f95133,plain,
quotient(quotient(b,b2),b1) = difference(b1,product(b,b)),
inference(forward_demodulation,[],[f95072,f23]) ).
fof(f95139,plain,
product(b1,b) = product(difference(b2,b),b1),
inference(forward_demodulation,[],[f95078,f22]) ).
fof(f95144,plain,
product(b1,quotient(b,b2)) = product(product(b,quotient(b1,b)),b),
inference(forward_demodulation,[],[f95083,f1816]) ).
fof(f95145,plain,
difference(b1,difference(b2,b)) = quotient(b2,quotient(b,quotient(b,b1))),
inference(forward_demodulation,[],[f95084,f24760]) ).
fof(f95161,plain,
difference(b1,b) = product(difference(b,b2),b),
inference(forward_demodulation,[],[f95110,f3245]) ).
fof(f95175,plain,
difference(b1,b) = quotient(quotient(b,b2),b1),
inference(forward_demodulation,[],[f95133,f26]) ).
fof(f95182,plain,
product(b1,quotient(b,b2)) = product(b,product(quotient(b1,b),b)),
inference(forward_demodulation,[],[f95144,f418]) ).
fof(f95183,plain,
difference(b1,difference(b2,b)) = quotient(b2,difference(b1,b)),
inference(forward_demodulation,[],[f95145,f5303]) ).
fof(f95193,plain,
difference(b1,b) = product(b2,quotient(b,b2)),
inference(forward_demodulation,[],[f95161,f4442]) ).
fof(f95201,plain,
product(b,b1) = product(b1,quotient(b,b2)),
inference(forward_demodulation,[],[f95182,f24]) ).
fof(f95264,plain,
product(quotient(b,b2),product(quotient(b,b2),b2)) = difference(product(difference(b1,b),quotient(b,b2)),quotient(b,b2)),
inference(superposition,[],[f193,f95193]) ).
fof(f95306,plain,
product(product(quotient(b,b2),b2),b2) = product(b2,quotient(b2,difference(b1,b))),
inference(superposition,[],[f4918,f95193]) ).
fof(f95326,plain,
product(product(quotient(b,b2),b2),b2) = product(b2,difference(b1,difference(b2,b))),
inference(forward_demodulation,[],[f95306,f95183]) ).
fof(f95358,plain,
product(quotient(b,b2),product(quotient(b,b2),b2)) = product(difference(difference(b1,b),quotient(b,b2)),quotient(b,b2)),
inference(forward_demodulation,[],[f95264,f3975]) ).
fof(f95391,plain,
product(product(quotient(b,b2),b2),b2) = difference(product(b2,b1),b),
inference(forward_demodulation,[],[f95326,f3566]) ).
fof(f95410,plain,
product(quotient(b,b2),product(quotient(b,b2),b2)) = product(difference(difference(b1,b),b),difference(b2,quotient(b,b2))),
inference(forward_demodulation,[],[f95358,f74969]) ).
fof(f95429,plain,
difference(product(b2,b1),b) = product(b,product(b2,b2)),
inference(forward_demodulation,[],[f95391,f424]) ).
fof(f95442,plain,
product(quotient(b,b2),product(quotient(b,b2),b2)) = product(quotient(b,b1),difference(b2,quotient(b,b2))),
inference(forward_demodulation,[],[f95410,f5302]) ).
fof(f95453,plain,
product(b,b2) = difference(product(b2,b1),b),
inference(forward_demodulation,[],[f95429,f26]) ).
fof(f95461,plain,
product(quotient(b,b2),product(quotient(b,b2),b2)) = product(quotient(b1,b1),quotient(b,b2)),
inference(forward_demodulation,[],[f95442,f95092]) ).
fof(f95474,plain,
product(b1,quotient(b,b2)) = product(quotient(b,b2),product(quotient(b,b2),b2)),
inference(forward_demodulation,[],[f95461,f53]) ).
fof(f95483,plain,
product(b1,quotient(b,b2)) = product(b,product(quotient(b,b2),difference(b2,b))),
inference(forward_demodulation,[],[f95474,f7688]) ).
fof(f95488,plain,
product(b1,quotient(b,b2)) = product(quotient(b,b2),b),
inference(forward_demodulation,[],[f95483,f834]) ).
fof(f95492,plain,
product(b,b1) = product(quotient(b,b2),b),
inference(forward_demodulation,[],[f95488,f95201]) ).
fof(f95540,plain,
quotient(b,product(b2,b1)) = difference(product(b,b2),b),
inference(superposition,[],[f5302,f95453]) ).
fof(f95610,plain,
product(b,difference(b2,b)) = quotient(b,product(b2,b1)),
inference(forward_demodulation,[],[f95540,f3567]) ).
fof(f95783,plain,
! [X0,X1] : product(X0,b) = difference(product(X1,quotient(b,b2)),product(product(X1,X0),product(b,b1))),
inference(superposition,[],[f157,f95492]) ).
fof(f95820,plain,
! [X0] : product(X0,difference(quotient(quotient(b,b2),X0),b)) = difference(quotient(quotient(b,b2),X0),product(b,b1)),
inference(superposition,[],[f3122,f95492]) ).
fof(f95862,plain,
! [X0] : quotient(product(X0,b2),b) = difference(quotient(quotient(b,b2),X0),product(b,b1)),
inference(forward_demodulation,[],[f95820,f93767]) ).
fof(f95898,plain,
! [X0,X1] : product(X0,b) = product(X0,difference(difference(X1,product(X1,quotient(b,b2))),product(b,b1))),
inference(forward_demodulation,[],[f95783,f2919]) ).
fof(f95965,plain,
! [X0,X1] : product(X0,b) = product(X0,product(b2,quotient(X1,difference(difference(quotient(b,b2),b1),X1)))),
inference(forward_demodulation,[],[f95898,f61387]) ).
fof(f96011,plain,
! [X0] : product(X0,b) = product(X0,product(b2,difference(quotient(b,b2),b1))),
inference(forward_demodulation,[],[f95965,f52]) ).
fof(f96039,plain,
! [X0] : product(X0,b) = product(quotient(product(X0,b1),b),b2),
inference(forward_demodulation,[],[f96011,f11988]) ).
fof(f96178,plain,
difference(quotient(b,b2),b1) = difference(quotient(quotient(b,b2),b1),product(b,b1)),
inference(superposition,[],[f8271,f95201]) ).
fof(f96191,plain,
difference(quotient(b,b2),b1) = quotient(product(b1,b2),b),
inference(forward_demodulation,[],[f96178,f95862]) ).
fof(f96257,plain,
difference(b2,b) = quotient(product(b1,b2),b),
inference(forward_demodulation,[],[f96191,f94879]) ).
fof(f96446,plain,
product(difference(product(b1,b2),b),product(b1,b2)) = product(product(b1,b2),quotient(difference(b2,b),product(b1,b2))),
inference(superposition,[],[f20870,f96257]) ).
fof(f96460,plain,
quotient(b,product(b2,b1)) = product(difference(product(b1,b2),b),product(b1,b2)),
inference(forward_demodulation,[],[f96446,f10229]) ).
fof(f96523,plain,
quotient(b,product(b2,b1)) = quotient(product(b,product(b1,b2)),b),
inference(forward_demodulation,[],[f96460,f4364]) ).
fof(f96569,plain,
quotient(b,product(b2,b1)) = product(b,quotient(product(b1,b2),b)),
inference(forward_demodulation,[],[f96523,f6461]) ).
fof(f96594,plain,
product(difference(b2,b),b1) = quotient(b,product(b2,b1)),
inference(forward_demodulation,[],[f96569,f12559]) ).
fof(f96610,plain,
product(b,difference(b2,b)) = product(difference(b2,b),b1),
inference(forward_demodulation,[],[f96594,f95610]) ).
fof(f96622,plain,
product(b1,b) = product(b,difference(b2,b)),
inference(forward_demodulation,[],[f96610,f95139]) ).
fof(f96677,plain,
difference(quotient(b,b2),b1) = difference(difference(b1,b),product(b1,quotient(b,b2))),
inference(superposition,[],[f8271,f95175]) ).
fof(f96730,plain,
difference(quotient(b,b2),b1) = quotient(quotient(b,b1),b2),
inference(forward_demodulation,[],[f96677,f82040]) ).
fof(f96775,plain,
difference(b2,b) = quotient(quotient(b,b1),b2),
inference(forward_demodulation,[],[f96730,f94879]) ).
fof(f98332,plain,
difference(b2,difference(b2,b)) = difference(quotient(b2,difference(b2,b)),quotient(b,b1)),
inference(superposition,[],[f8455,f96775]) ).
fof(f98346,plain,
! [X0] : difference(quotient(b2,X0),quotient(b,b1)) = difference(b2,product(difference(b2,b),X0)),
inference(superposition,[],[f14587,f96775]) ).
fof(f98384,plain,
difference(b2,difference(b2,b)) = difference(b2,product(difference(b2,b),difference(b2,b))),
inference(forward_demodulation,[],[f98332,f98346]) ).
fof(f98428,plain,
difference(b2,difference(b2,b)) = difference(b2,difference(b2,product(b,b))),
inference(forward_demodulation,[],[f98384,f59205]) ).
fof(f98456,plain,
difference(b2,difference(b2,b)) = difference(b2,difference(b,product(b1,b))),
inference(forward_demodulation,[],[f98428,f95109]) ).
fof(f98471,plain,
difference(b2,difference(b2,b)) = difference(b2,product(difference(b,b1),b)),
inference(forward_demodulation,[],[f98456,f3245]) ).
fof(f98485,plain,
difference(b2,difference(b2,b)) = quotient(b,quotient(b1,b2)),
inference(forward_demodulation,[],[f98471,f24760]) ).
fof(f105789,plain,
! [X0,X1] : product(product(X0,b),product(b,X1)) = product(product(X0,b1),product(b2,X1)),
inference(superposition,[],[f133,f96039]) ).
fof(f115592,plain,
! [X0] : product(X0,b) = product(difference(quotient(b1,b2),product(b,X0)),difference(b2,difference(b2,b))),
inference(superposition,[],[f11012,f98485]) ).
fof(f115634,plain,
! [X0] : product(X0,b) = product(X0,quotient(product(difference(b2,difference(b2,b)),quotient(b1,b2)),b)),
inference(forward_demodulation,[],[f115592,f12443]) ).
fof(f115686,plain,
! [X0] : product(X0,b) = product(X0,difference(difference(b,b1),product(b2,difference(b2,difference(b2,b))))),
inference(forward_demodulation,[],[f115634,f39767]) ).
fof(f115721,plain,
! [X0] : product(X0,b) = product(X0,difference(b2,product(b2,difference(difference(b,b1),difference(b2,b))))),
inference(forward_demodulation,[],[f115686,f47515]) ).
fof(f115748,plain,
! [X0] : product(X0,b) = product(X0,difference(difference(b,b1),difference(b2,b))),
inference(forward_demodulation,[],[f115721,f21]) ).
fof(f140513,plain,
! [X0] : difference(difference(b,X0),difference(b2,b)) = difference(b,difference(X0,product(b1,b))),
inference(superposition,[],[f7386,f96622]) ).
fof(f217153,plain,
! [X0,X1] :
( product(X0,X1) != product(product(X0,b),product(difference(difference(b,b1),difference(b2,b)),X1))
| m(X0,difference(difference(b,b1),difference(b2,b)),X1) ),
inference(superposition,[],[f31,f115748]) ).
fof(f217556,plain,
! [X0,X1] :
( product(X0,X1) != product(product(X0,b),product(difference(b,difference(b1,product(b1,b))),X1))
| m(X0,difference(difference(b,b1),difference(b2,b)),X1) ),
inference(forward_demodulation,[],[f217153,f140513]) ).
fof(f217815,plain,
! [X0,X1] :
( product(X0,X1) != product(product(X0,b),product(difference(b,b),X1))
| m(X0,difference(difference(b,b1),difference(b2,b)),X1) ),
inference(forward_demodulation,[],[f217556,f21]) ).
fof(f218052,plain,
! [X0,X1] :
( product(X0,X1) != product(b,product(b,quotient(product(X1,b),X0)))
| m(X0,difference(difference(b,b1),difference(b2,b)),X1) ),
inference(forward_demodulation,[],[f217815,f21636]) ).
fof(f218216,plain,
! [X0,X1] :
( product(X0,X1) != product(product(X0,b),product(b,X1))
| m(X0,difference(difference(b,b1),difference(b2,b)),X1) ),
inference(forward_demodulation,[],[f218052,f73653]) ).
fof(f218346,plain,
! [X0,X1] :
( product(X0,X1) != product(product(X0,b1),product(b2,X1))
| m(X0,difference(difference(b,b1),difference(b2,b)),X1) ),
inference(forward_demodulation,[],[f218216,f105789]) ).
fof(f218452,plain,
! [X0,X1] :
( m(X0,difference(b,difference(b1,product(b1,b))),X1)
| product(X0,X1) != product(product(X0,b1),product(b2,X1)) ),
inference(forward_demodulation,[],[f218346,f140513]) ).
fof(f218536,plain,
! [X0,X1] :
( m(X0,difference(b,b),X1)
| product(X0,X1) != product(product(X0,b1),product(b2,X1)) ),
inference(forward_demodulation,[],[f218452,f21]) ).
fof(f218608,plain,
! [X0,X1] :
( m(X0,b,X1)
| product(X0,X1) != product(product(X0,b1),product(b2,X1)) ),
inference(forward_demodulation,[],[f218536,f47]) ).
fof(f219062,plain,
product(b1,b2) != product(product(b1,b1),product(b2,b2)),
inference(resolution,[],[f218608,f38]) ).
fof(f219063,plain,
product(b1,b2) != product(product(b1,b1),b2),
inference(forward_demodulation,[],[f219062,f26]) ).
fof(f219064,plain,
product(b1,b2) != product(b1,b2),
inference(forward_demodulation,[],[f219063,f26]) ).
fof(f219065,plain,
$false,
inference(trivial_inequality_removal,[],[f219064]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP778+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 % Computer : n009.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Sun Sep 27 10:44:00 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.46 Running first-order theorem proving
% 0.16/0.46 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.83/4.28 % (1846519)Detected formulas, will run a generic FOF schedule.
% 22.83/4.28 % (1846529)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=608116074:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 22.83/4.28 % (1846524)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=2209034477:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 22.83/4.28 % (1846527)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3921318562:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 22.83/4.28 % (1846528)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2512832193:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 22.83/4.28 % (1846525)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=3834969903:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 22.83/4.28 % (1846526)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=3700373526:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 22.83/4.28 % (1846527)Refutation not found, incomplete strategy
% 22.83/4.28 % (1846527)------------------------------
% 22.83/4.28 % (1846527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.83/4.28 % (1846527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.83/4.28 % (1846527)CaDiCaL version: 2.1.3
% 22.83/4.28 % (1846527)Termination reason: Refutation not found, incomplete strategy
% 22.83/4.28 % (1846527)Time elapsed: 0.001 s
% 22.83/4.28 % (1846527)Peak memory usage: 88 MB
% 22.83/4.28 % (1846529)Instruction limit reached!
% 22.83/4.28 % (1846529)------------------------------
% 22.83/4.28 % (1846529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.83/4.28 % (1846529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.83/4.28 % (1846529)CaDiCaL version: 2.1.3
% 22.83/4.28 % (1846529)Termination reason: Instruction limit
% 22.83/4.28 % (1846529)Termination phase: Saturation
% 22.83/4.28 % (1846529)Time elapsed: 0.069 s
% 22.83/4.28 % (1846529)Peak memory usage: 90 MB
% 22.83/4.28 % (1846529)Instructions burned: 140 (million)
% 22.83/4.28 % (1846530)dis-21_1_sil=8000:lcm=predicate:random_seed=136318521: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)
% 22.83/4.28 % (1846530)Refutation not found, incomplete strategy
% 22.83/4.28 % (1846530)------------------------------
% 22.83/4.28 % (1846530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.83/4.28 % (1846530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.83/4.28 % (1846530)CaDiCaL version: 2.1.3
% 22.83/4.28 % (1846530)Termination reason: Refutation not found, incomplete strategy
% 22.83/4.28 % (1846530)Time elapsed: 0.002 s
% 22.83/4.28 % (1846530)Peak memory usage: 88 MB
% 22.83/4.28 % (1846530)Instructions burned: 1 (million)
% 22.83/4.28 % (1846528)Instruction limit reached!
% 22.83/4.28 % (1846528)------------------------------
% 22.83/4.28 % (1846528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.83/4.28 % (1846528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.83/4.28 % (1846528)CaDiCaL version: 2.1.3
% 22.83/4.28 % (1846528)Termination reason: Instruction limit
% 22.83/4.28 % (1846528)Termination phase: Saturation
% 22.83/4.28 % (1846528)Time elapsed: 0.109 s
% 22.83/4.28 % (1846528)Peak memory usage: 88 MB
% 22.83/4.28 % (1846528)Instructions burned: 120 (million)
% 22.83/4.28 % (1846537)lrs+10_1_sil=8000:sp=occurrence:random_seed=2658980570:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 22.83/4.28 % (1846539)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3113744378:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 22.83/4.28 % (1846539)Refutation not found, incomplete strategy
% 22.83/4.28 % (1846539)------------------------------
% 22.83/4.28 % (1846539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.83/4.28 % (1846539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.83/4.28 % (1846539)CaDiCaL version: 2.1.3
% 22.83/4.28 % (1846539)Termination reason: Refutation not found, incomplete strategy
% 22.83/4.28 % (1846539)Time elapsed: 0.001 s
% 34.35/5.99 % (1846539)Peak memory usage: 88 MB
% 34.35/5.99 % (1846527)------------------------------
% 34.35/5.99 % (1846527)------------------------------
% 34.35/5.99 % (1846537)Instruction limit reached!
% 34.35/5.99 % (1846537)------------------------------
% 34.35/5.99 % (1846537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.35/5.99 % (1846537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.35/5.99 % (1846537)CaDiCaL version: 2.1.3
% 34.35/5.99 % (1846537)Termination reason: Instruction limit
% 34.35/5.99 % (1846537)Termination phase: Saturation
% 34.35/5.99 % (1846537)Time elapsed: 0.200 s
% 34.35/5.99 % (1846537)Peak memory usage: 91 MB
% 34.35/5.99 % (1846537)Instructions burned: 286 (million)
% 34.35/5.99 % (1846530)------------------------------
% 34.35/5.99 % (1846530)------------------------------
% 34.35/5.99 % (1846539)------------------------------
% 34.35/5.99 % (1846539)------------------------------
% 34.35/5.99 % (1846543)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=3504018298:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 34.35/5.99 % (1846542)lrs+1011_1_sil=32000:sp=occurrence:random_seed=811775459:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 34.35/5.99 % (1846542)Refutation not found, incomplete strategy
% 34.35/5.99 % (1846542)------------------------------
% 34.35/5.99 % (1846542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.35/5.99 % (1846542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.35/5.99 % (1846542)CaDiCaL version: 2.1.3
% 34.35/5.99 % (1846542)Termination reason: Refutation not found, incomplete strategy
% 34.35/5.99 % (1846542)Time elapsed: 0.002 s
% 34.35/5.99 % (1846542)Peak memory usage: 88 MB
% 34.35/5.99 % (1846544)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2533905672:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 34.35/5.99 % (1846544)Refutation not found, incomplete strategy
% 34.35/5.99 % (1846544)------------------------------
% 34.35/5.99 % (1846544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.35/5.99 % (1846544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.35/5.99 % (1846544)CaDiCaL version: 2.1.3
% 34.35/5.99 % (1846544)Termination reason: Refutation not found, incomplete strategy
% 34.35/5.99 % (1846544)Time elapsed: 0.002 s
% 34.35/5.99 % (1846544)Peak memory usage: 88 MB
% 34.35/5.99 % (1846545)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3364888946:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 34.35/5.99 % (1846543)Instruction limit reached!
% 34.35/5.99 % (1846543)------------------------------
% 34.35/5.99 % (1846543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.35/5.99 % (1846543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.35/5.99 % (1846543)CaDiCaL version: 2.1.3
% 34.35/5.99 % (1846543)Termination reason: Instruction limit
% 34.35/5.99 % (1846543)Termination phase: Saturation
% 34.35/5.99 % (1846543)Time elapsed: 0.242 s
% 34.35/5.99 % (1846543)Peak memory usage: 92 MB
% 34.35/5.99 % (1846543)Instructions burned: 249 (million)
% 34.35/5.99 % (1846544)------------------------------
% 34.35/5.99 % (1846544)------------------------------
% 34.35/5.99 % (1846542)------------------------------
% 34.35/5.99 % (1846542)------------------------------
% 34.35/5.99 % (1846551)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1822969007:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 34.35/5.99 % (1846551)Refutation not found, incomplete strategy
% 34.35/5.99 % (1846551)------------------------------
% 34.35/5.99 % (1846551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.35/5.99 % (1846551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.35/5.99 % (1846551)CaDiCaL version: 2.1.3
% 34.35/5.99 % (1846551)Termination reason: Refutation not found, incomplete strategy
% 34.35/5.99 % (1846551)Time elapsed: 0.003 s
% 34.35/5.99 % (1846551)Peak memory usage: 88 MB
% 34.35/5.99 % (1846551)Instructions burned: 2 (million)
% 34.35/5.99 % (1846552)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2953337858:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 34.35/5.99 % (1846552)Refutation not found, incomplete strategy
% 34.35/5.99 % (1846552)------------------------------
% 34.35/5.99 % (1846552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.16/10.40 % (1846552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.16/10.40 % (1846552)CaDiCaL version: 2.1.3
% 66.16/10.40 % (1846552)Termination reason: Refutation not found, incomplete strategy
% 66.16/10.40 % (1846552)Time elapsed: 0.002 s
% 66.16/10.40 % (1846552)Peak memory usage: 88 MB
% 66.16/10.40 % (1846553)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=206146286:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 66.16/10.40 % (1846553)Instruction limit reached!
% 66.16/10.40 % (1846553)------------------------------
% 66.16/10.40 % (1846553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.16/10.40 % (1846553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.16/10.40 % (1846553)CaDiCaL version: 2.1.3
% 66.16/10.40 % (1846553)Termination reason: Instruction limit
% 66.16/10.40 % (1846553)Termination phase: Saturation
% 66.16/10.40 % (1846553)Time elapsed: 0.119 s
% 66.16/10.40 % (1846553)Peak memory usage: 89 MB
% 66.16/10.40 % (1846553)Instructions burned: 114 (million)
% 66.16/10.40 % (1846551)------------------------------
% 66.16/10.40 % (1846551)------------------------------
% 66.16/10.40 % (1846552)------------------------------
% 66.16/10.40 % (1846552)------------------------------
% 66.16/10.40 % (1846560)lrs+10_1_sil=8000:sp=occurrence:random_seed=1007871203:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 66.16/10.40 % (1846561)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2087645079:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 66.16/10.40 % (1846561)Refutation not found, incomplete strategy
% 66.16/10.40 % (1846561)------------------------------
% 66.16/10.40 % (1846561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.16/10.40 % (1846561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.16/10.40 % (1846561)CaDiCaL version: 2.1.3
% 66.16/10.40 % (1846561)Termination reason: Refutation not found, incomplete strategy
% 66.16/10.40 % (1846561)Time elapsed: 0.002 s
% 66.16/10.40 % (1846561)Peak memory usage: 88 MB
% 66.16/10.40 % (1846562)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3961335871:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 66.16/10.40 % (1846561)------------------------------
% 66.16/10.40 % (1846561)------------------------------
% 66.16/10.40 % (1846566)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2779461389:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 66.16/10.40 % (1846566)Refutation not found, incomplete strategy
% 66.16/10.40 % (1846566)------------------------------
% 66.16/10.40 % (1846566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.16/10.40 % (1846566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.16/10.40 % (1846566)CaDiCaL version: 2.1.3
% 66.16/10.40 % (1846566)Termination reason: Refutation not found, incomplete strategy
% 66.16/10.40 % (1846566)Time elapsed: 0.003 s
% 66.16/10.40 % (1846566)Peak memory usage: 89 MB
% 66.16/10.40 % (1846566)Instructions burned: 2 (million)
% 66.16/10.40 % (1846560)Instruction limit reached!
% 66.16/10.40 % (1846560)------------------------------
% 66.16/10.40 % (1846560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.16/10.40 % (1846560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.16/10.40 % (1846560)CaDiCaL version: 2.1.3
% 66.16/10.40 % (1846560)Termination reason: Instruction limit
% 66.16/10.40 % (1846560)Termination phase: Saturation
% 66.16/10.40 % (1846560)Time elapsed: 0.966 s
% 66.16/10.40 % (1846560)Peak memory usage: 95 MB
% 66.16/10.40 % (1846560)Instructions burned: 908 (million)
% 66.16/10.40 % (1846566)------------------------------
% 66.16/10.40 % (1846566)------------------------------
% 66.16/10.40 % (1846545)Instruction limit reached!
% 66.16/10.40 % (1846545)------------------------------
% 66.16/10.40 % (1846545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.16/10.40 % (1846545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.16/10.40 % (1846545)CaDiCaL version: 2.1.3
% 66.16/10.40 % (1846545)Termination reason: Instruction limit
% 66.16/10.40 % (1846545)Termination phase: Saturation
% 66.16/10.40 % (1846545)Time elapsed: 2.060 s
% 66.16/10.40 % (1846545)Peak memory usage: 143 MB
% 66.16/10.40 % (1846545)Instructions burned: 2350 (million)
% 66.16/10.40 % (1846568)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1400613307:st=8:i=592:sd=3:ep=RST:ss=axioms_2970 on theBenchmark for (2970ds/592Mi)
% 108.75/16.31 % (1846568)Refutation not found, incomplete strategy
% 108.75/16.31 % (1846568)------------------------------
% 108.75/16.31 % (1846568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.75/16.31 % (1846568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.75/16.31 % (1846568)CaDiCaL version: 2.1.3
% 108.75/16.31 % (1846568)Termination reason: Refutation not found, incomplete strategy
% 108.75/16.31 % (1846568)Time elapsed: 0.002 s
% 108.75/16.31 % (1846568)Peak memory usage: 88 MB
% 108.75/16.31 % (1846569)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2623605646:st=3:i=13193:sd=3:ss=axioms_2969 on theBenchmark for (2969ds/13193Mi)
% 108.75/16.31 % (1846570)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=3377050356:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 108.75/16.31 % (1846570)Instruction limit reached!
% 108.75/16.31 % (1846570)------------------------------
% 108.75/16.31 % (1846570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.75/16.31 % (1846570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.75/16.31 % (1846570)CaDiCaL version: 2.1.3
% 108.75/16.31 % (1846570)Termination reason: Instruction limit
% 108.75/16.31 % (1846570)Termination phase: Saturation
% 108.75/16.31 % (1846570)Time elapsed: 0.138 s
% 108.75/16.31 % (1846570)Peak memory usage: 90 MB
% 108.75/16.31 % (1846570)Instructions burned: 125 (million)
% 108.75/16.31 % (1846568)------------------------------
% 108.75/16.31 % (1846568)------------------------------
% 108.75/16.31 % (1846574)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4280069482:i=134:gtgl=5:slsql=off:gtg=exists_sym_2964 on theBenchmark for (2964ds/134Mi)
% 108.75/16.31 % (1846575)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2438829811:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/141Mi)
% 108.75/16.31 % (1846575)Refutation not found, incomplete strategy
% 108.75/16.31 % (1846575)------------------------------
% 108.75/16.31 % (1846575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.75/16.31 % (1846575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.75/16.31 % (1846575)CaDiCaL version: 2.1.3
% 108.75/16.31 % (1846575)Termination reason: Refutation not found, incomplete strategy
% 108.75/16.31 % (1846575)Time elapsed: 0.001 s
% 108.75/16.31 % (1846575)Peak memory usage: 87 MB
% 108.75/16.31 % (1846574)Instruction limit reached!
% 108.75/16.31 % (1846574)------------------------------
% 108.75/16.31 % (1846574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.75/16.31 % (1846574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.75/16.31 % (1846574)CaDiCaL version: 2.1.3
% 108.75/16.31 % (1846574)Termination reason: Instruction limit
% 108.75/16.31 % (1846574)Termination phase: Saturation
% 108.75/16.31 % (1846574)Time elapsed: 0.144 s
% 108.75/16.31 % (1846574)Peak memory usage: 90 MB
% 108.75/16.31 % (1846574)Instructions burned: 134 (million)
% 108.75/16.31 % (1846578)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2103141012:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2960 on theBenchmark for (2960ds/431Mi)
% 108.75/16.31 % (1846578)Refutation not found, incomplete strategy
% 108.75/16.31 % (1846578)------------------------------
% 108.75/16.31 % (1846578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.75/16.31 % (1846578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.75/16.31 % (1846578)CaDiCaL version: 2.1.3
% 108.75/16.31 % (1846578)Termination reason: Refutation not found, incomplete strategy
% 108.75/16.31 % (1846578)Time elapsed: 0.001 s
% 108.75/16.31 % (1846578)Peak memory usage: 87 MB
% 108.75/16.31 % (1846575)------------------------------
% 108.75/16.31 % (1846575)------------------------------
% 108.75/16.31 % (1846580)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=2372309416:i=6060:aac=none:ins=25_2956 on theBenchmark for (2956ds/6060Mi)
% 108.75/16.31 % (1846578)------------------------------
% 108.75/16.31 % (1846578)------------------------------
% 108.75/16.31 % (1846582)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=2638854200:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2953 on theBenchmark for (2953ds/150Mi)
% 94.00/20.71 % (1846582)Instruction limit reached!
% 94.00/20.71 % (1846582)------------------------------
% 94.00/20.71 % (1846582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846582)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846582)Termination reason: Instruction limit
% 94.00/20.71 % (1846582)Termination phase: Saturation
% 94.00/20.71 % (1846582)Time elapsed: 0.163 s
% 94.00/20.71 % (1846582)Peak memory usage: 91 MB
% 94.00/20.71 % (1846582)Instructions burned: 150 (million)
% 94.00/20.71 % (1846584)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1820817505:i=14155:bd=all_2948 on theBenchmark for (2948ds/14155Mi)
% 94.00/20.71 % (1846562)Instruction limit reached!
% 94.00/20.71 % (1846562)------------------------------
% 94.00/20.71 % (1846562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846562)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846562)Termination reason: Instruction limit
% 94.00/20.71 % (1846562)Termination phase: Saturation
% 94.00/20.71 % (1846562)Time elapsed: 5.273 s
% 94.00/20.71 % (1846562)Peak memory usage: 167 MB
% 94.00/20.71 % (1846562)Instructions burned: 5202 (million)
% 94.00/20.71 % (1846588)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2912570276:i=667:av=off:fsr=off_2924 on theBenchmark for (2924ds/667Mi)
% 94.00/20.71 % (1846588)Refutation not found, incomplete strategy
% 94.00/20.71 % (1846588)------------------------------
% 94.00/20.71 % (1846588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846588)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846588)Termination reason: Refutation not found, incomplete strategy
% 94.00/20.71 % (1846588)Time elapsed: 0.002 s
% 94.00/20.71 % (1846588)Peak memory usage: 88 MB
% 94.00/20.71 % (1846588)------------------------------
% 94.00/20.71 % (1846588)------------------------------
% 94.00/20.71 % (1846590)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=1906782995:s2a=on:i=185:s2at=1.8:fdi=4_2917 on theBenchmark for (2917ds/185Mi)
% 94.00/20.71 % (1846590)Instruction limit reached!
% 94.00/20.71 % (1846590)------------------------------
% 94.00/20.71 % (1846590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846590)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846590)Termination reason: Instruction limit
% 94.00/20.71 % (1846590)Termination phase: Saturation
% 94.00/20.71 % (1846590)Time elapsed: 0.171 s
% 94.00/20.71 % (1846590)Peak memory usage: 91 MB
% 94.00/20.71 % (1846590)Instructions burned: 185 (million)
% 94.00/20.71 % (1846592)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3532678341:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2913 on theBenchmark for (2913ds/193Mi)
% 94.00/20.71 % (1846592)Instruction limit reached!
% 94.00/20.71 % (1846592)------------------------------
% 94.00/20.71 % (1846592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846592)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846592)Termination reason: Instruction limit
% 94.00/20.71 % (1846592)Termination phase: Saturation
% 94.00/20.71 % (1846592)Time elapsed: 0.196 s
% 94.00/20.71 % (1846592)Peak memory usage: 91 MB
% 94.00/20.71 % (1846592)Instructions burned: 193 (million)
% 94.00/20.71 % (1846594)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2999987682:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2908 on theBenchmark for (2908ds/4850Mi)
% 94.00/20.71 % (1846594)Refutation not found, incomplete strategy
% 94.00/20.71 % (1846594)------------------------------
% 94.00/20.71 % (1846594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846594)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846594)Termination reason: Refutation not found, incomplete strategy
% 94.00/20.71 % (1846594)Time elapsed: 0.002 s
% 94.00/20.71 % (1846594)Peak memory usage: 87 MB
% 94.00/20.71 % (1846594)------------------------------
% 94.00/20.71 % (1846594)------------------------------
% 94.00/20.71 % (1846598)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1197379145:i=12111:sd=1:ss=included_2902 on theBenchmark for (2902ds/12111Mi)
% 94.00/20.71 % (1846580)Instruction limit reached!
% 94.00/20.71 % (1846580)------------------------------
% 94.00/20.71 % (1846580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846580)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846580)Termination reason: Instruction limit
% 94.00/20.71 % (1846580)Termination phase: Saturation
% 94.00/20.71 % (1846580)Time elapsed: 6.253 s
% 94.00/20.71 % (1846580)Peak memory usage: 166 MB
% 94.00/20.71 % (1846580)Instructions burned: 6061 (million)
% 94.00/20.71 % (1846602)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1028857491:i=319:kws=precedence:fsr=off_2890 on theBenchmark for (2890ds/319Mi)
% 94.00/20.71 % (1846602)Instruction limit reached!
% 94.00/20.71 % (1846602)------------------------------
% 94.00/20.71 % (1846602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846602)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846602)Termination reason: Instruction limit
% 94.00/20.71 % (1846602)Termination phase: Saturation
% 94.00/20.71 % (1846602)Time elapsed: 0.331 s
% 94.00/20.71 % (1846602)Peak memory usage: 94 MB
% 94.00/20.71 % (1846602)Instructions burned: 319 (million)
% 94.00/20.71 % (1846604)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=265161217:i=2064:ep=RST_2884 on theBenchmark for (2884ds/2064Mi)
% 94.00/20.71 % (1846604)Refutation not found, incomplete strategy
% 94.00/20.71 % (1846604)------------------------------
% 94.00/20.71 % (1846604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846604)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846604)Termination reason: Refutation not found, incomplete strategy
% 94.00/20.71 % (1846604)Time elapsed: 0.002 s
% 94.00/20.71 % (1846604)Peak memory usage: 88 MB
% 94.00/20.71 % (1846604)------------------------------
% 94.00/20.71 % (1846604)------------------------------
% 94.00/20.71 % (1846606)dis-1011_128_sil=32000:random_seed=792834875:i=3706:ep=RST:av=off_2877 on theBenchmark for (2877ds/3706Mi)
% 94.00/20.71 % (1846606)Instruction limit reached!
% 94.00/20.71 % (1846606)------------------------------
% 94.00/20.71 % (1846606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846606)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846606)Termination reason: Instruction limit
% 94.00/20.71 % (1846606)Termination phase: Saturation
% 94.00/20.71 % (1846606)Time elapsed: 2.155 s
% 94.00/20.71 % (1846606)Peak memory usage: 109 MB
% 94.00/20.71 % (1846606)Instructions burned: 3706 (million)
% 94.00/20.71 % (1846761)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1519433958:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2853 on theBenchmark for (2853ds/757Mi)
% 94.00/20.71 % (1846761)Refutation not found, incomplete strategy
% 94.00/20.71 % (1846761)------------------------------
% 94.00/20.71 % (1846761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846761)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846761)Termination reason: Refutation not found, incomplete strategy
% 94.00/20.71 % (1846761)Time elapsed: 0.001 s
% 94.00/20.71 % (1846761)Peak memory usage: 88 MB
% 94.00/20.71 % (1846761)------------------------------
% 94.00/20.71 % (1846761)------------------------------
% 94.00/20.71 % (1846763)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2090722671:i=13913:ss=axioms:sgt=8_2849 on theBenchmark for (2849ds/13913Mi)
% 94.00/20.71 % (1846569)Instruction limit reached!
% 94.00/20.71 % (1846569)------------------------------
% 94.00/20.71 % (1846569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846569)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846569)Termination reason: Instruction limit
% 94.00/20.71 % (1846569)Termination phase: Saturation
% 94.00/20.71 % (1846569)Time elapsed: 11.976 s
% 94.00/20.71 % (1846569)Peak memory usage: 222 MB
% 94.00/20.71 % (1846569)Instructions burned: 13194 (million)
% 94.00/20.71 % (1846765)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=293475713:i=9925:aac=none_2846 on theBenchmark for (2846ds/9925Mi)
% 94.00/20.71 % (1846584)Instruction limit reached!
% 94.00/20.71 % (1846584)------------------------------
% 94.00/20.71 % (1846584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846584)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846584)Termination reason: Instruction limit
% 94.00/20.71 % (1846584)Termination phase: Saturation
% 94.00/20.71 % (1846584)Time elapsed: 11.864 s
% 94.00/20.71 % (1846584)Peak memory usage: 231 MB
% 94.00/20.71 % (1846584)Instructions burned: 14155 (million)
% 94.00/20.71 % (1846767)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2943491045:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2826 on theBenchmark for (2826ds/2479Mi)
% 94.00/20.71 % (1846767)Refutation not found, incomplete strategy
% 94.00/20.71 % (1846767)------------------------------
% 94.00/20.71 % (1846767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846767)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846767)Termination reason: Refutation not found, incomplete strategy
% 94.00/20.71 % (1846767)Time elapsed: 0.001 s
% 94.00/20.71 % (1846767)Peak memory usage: 88 MB
% 94.00/20.71 % (1846767)------------------------------
% 94.00/20.71 % (1846767)------------------------------
% 94.00/20.71 % (1846769)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2567086592:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2822 on theBenchmark for (2822ds/440Mi)
% 94.00/20.71 % (1846769)Instruction limit reached!
% 94.00/20.71 % (1846769)------------------------------
% 94.00/20.71 % (1846769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846769)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846769)Termination reason: Instruction limit
% 94.00/20.71 % (1846769)Termination phase: Saturation
% 94.00/20.71 % (1846769)Time elapsed: 0.252 s
% 94.00/20.71 % (1846769)Peak memory usage: 95 MB
% 94.00/20.71 % (1846769)Instructions burned: 441 (million)
% 94.00/20.71 % (1846771)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2550153895:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2818 on theBenchmark for (2818ds/11145Mi)
% 94.00/20.71 % (1846598)Instruction limit reached!
% 94.00/20.71 % (1846598)------------------------------
% 94.00/20.71 % (1846598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.00/20.71 % (1846598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.00/20.71 % (1846598)CaDiCaL version: 2.1.3
% 94.00/20.71 % (1846598)Termination reason: Instruction limit
% 94.00/20.71 % (1846598)Termination phase: Saturation
% 94.00/20.71 % (1846598)Time elapsed: 8.586 s
% 94.00/20.71 % (1846598)Peak memory usage: 243 MB
% 94.00/20.71 % (1846598)Instructions burned: 12112 (million)
% 94.00/20.71 % (1846773)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=506413578:cts=off:i=3034:av=off:er=known:fsd=on_2813 on theBenchmark for (2813ds/3034Mi)
% 94.00/20.71 % (1846525)First to succeed.
% 94.00/20.71 % (1846525)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1846519"
% 94.00/20.71 % (1846525)Refutation found. Thanks to Tanya!
% 94.00/20.71 % SZS status Theorem for theBenchmark
% 94.00/20.71 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/20.91 % (1846525)------------------------------
% 0.22/20.91 % (1846525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.22/20.91 % (1846525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/20.91 % (1846525)CaDiCaL version: 2.1.3
% 0.22/20.91 % (1846525)Termination reason: Refutation
% 0.22/20.91 % (1846525)Time elapsed: 19.009 s
% 0.22/20.91 % (1846525)Peak memory usage: 334 MB
% 0.22/20.91 % (1846525)Instructions burned: 21300 (million)
% 0.22/20.91 % (1846525)------------------------------
% 0.22/20.91 % (1846525)------------------------------
% 0.22/20.91 % (1846519)Success in time 19.69 s
% 0.22/20.91 % Vampire exiting
%------------------------------------------------------------------------------