%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP027-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 : Thu Sep 24 12:35:30 PM UTC 2026
% Result : Satisfiable 0.17s 0.56s
% Output : Saturation 0.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Xg] : group_member(identity_for(Xg),Xg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [Xg,X] : product(Xg,identity_for(Xg),X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [Xg,X] : product(Xg,X,identity_for(Xg),X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Xg] :
( group_member(inverse(Xg,X),Xg)
| ~ group_member(X,Xg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [Xg,X] : product(Xg,inverse(Xg,X),X,identity_for(Xg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Xg,X] : product(Xg,X,inverse(Xg,X),identity_for(Xg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Xg,Y] :
( product(Xg,X,Y,multiply(Xg,X,Y))
| ~ group_member(Y,Xg)
| ~ group_member(X,Xg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Xg,Y] :
( group_member(multiply(Xg,X,Y),Xg)
| ~ group_member(Y,Xg)
| ~ group_member(X,Xg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Xg,X,Y,Z,W] :
( W = Z
| ~ product(Xg,X,Y,W)
| ~ product(Xg,X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Xg,X,Y,Xy,Z,Yz,Xyz] :
( product(Xg,X,Yz,Xyz)
| ~ product(Xg,Xy,Z,Xyz)
| ~ product(Xg,Y,Z,Yz)
| ~ product(Xg,X,Y,Xy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Xg,X,Y,Xy,Z,Yz,Xyz] :
( product(Xg,Xy,Z,Xyz)
| ~ product(Xg,X,Yz,Xyz)
| ~ product(Xg,Y,Z,Yz)
| ~ product(Xg,X,Y,Xy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
group_member(a,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
group_member(b,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
group_member(c,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
group_member(d,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
group_member(i,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
identity_for(g) = i,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
! [X] :
( X = i
| X = d
| X = c
| X = b
| X = a
| ~ group_member(X,g) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
! [X] : multiply(g,X,multiply(g,X,multiply(g,X,multiply(g,X,X)))) = i,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,hypothesis,
! [X] : not_power_of(g,X) != X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [X] : ~ product(g,X,X,not_power_of(g,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [X] : ~ product(g,X,multiply(g,X,X),not_power_of(g,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [X] : ~ product(g,X,multiply(g,X,multiply(g,X,X)),not_power_of(g,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [X] : ~ product(g,X,multiply(g,X,multiply(g,X,multiply(g,X,X))),not_power_of(g,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,plain,
! [X0] : group_member(identity_for(X0),X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f26,plain,
! [X0,X1] : product(X0,identity_for(X0),X1,X1),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f27,plain,
! [X0,X1] : product(X0,X1,identity_for(X0),X1),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f28,plain,
! [X0,X1] :
( group_member(inverse(X1,X0),X1)
| ~ group_member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f29,plain,
! [X0,X1] : product(X0,inverse(X0,X1),X1,identity_for(X0)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f30,plain,
! [X0,X1] : product(X0,X1,inverse(X0,X1),identity_for(X0)),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f31,plain,
! [X0,X1,X2] :
( product(X1,X0,X2,multiply(X1,X0,X2))
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f32,plain,
! [X0,X1,X2] :
( group_member(multiply(X1,X0,X2),X1)
| ~ group_member(X2,X1)
| ~ group_member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f33,plain,
! [Z,W] :
( W = Z
| ! [Xg,X,Y] :
( ~ product(Xg,X,Y,W)
| ~ product(Xg,X,Y,Z) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f34,plain,
! [X0,X1,X2,X3,X4] :
( X4 = X3
| ~ product(X0,X1,X2,X4)
| ~ product(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [Xg,X,Yz,Xyz] :
( product(Xg,X,Yz,Xyz)
| ! [Xy,Z] :
( ~ product(Xg,Xy,Z,Xyz)
| ! [Y] :
( ~ product(Xg,Y,Z,Yz)
| ~ product(Xg,X,Y,Xy) ) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f36,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( product(X0,X1,X5,X6)
| ~ product(X0,X3,X4,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [Xg,Xy,Z,Xyz] :
( product(Xg,Xy,Z,Xyz)
| ! [X,Yz] :
( ~ product(Xg,X,Yz,Xyz)
| ! [Y] :
( ~ product(Xg,Y,Z,Yz)
| ~ product(Xg,X,Y,Xy) ) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f38,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( product(X0,X3,X4,X6)
| ~ product(X0,X1,X5,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
group_member(a,g),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f40,plain,
group_member(b,g),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f41,plain,
group_member(c,g),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f42,plain,
group_member(d,g),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f43,plain,
group_member(i,g),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f44,plain,
identity_for(g) = i,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f45,plain,
! [X0] :
( X0 = i
| X0 = d
| X0 = c
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f46,plain,
! [X0] : multiply(g,X0,multiply(g,X0,multiply(g,X0,multiply(g,X0,X0)))) = i,
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f47,plain,
! [X0] : not_power_of(g,X0) != X0,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f48,plain,
! [X0] : ~ product(g,X0,X0,not_power_of(g,X0)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f49,plain,
! [X0] : ~ product(g,X0,multiply(g,X0,X0),not_power_of(g,X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f50,plain,
! [X0] : ~ product(g,X0,multiply(g,X0,multiply(g,X0,X0)),not_power_of(g,X0)),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f51,plain,
! [X0] : ~ product(g,X0,multiply(g,X0,multiply(g,X0,multiply(g,X0,X0))),not_power_of(g,X0)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f52,plain,
! [X0,X1] :
( group_member(multiply(X1,identity_for(X1),X0),X1)
| ~ group_member(X0,X1) ),
inference(resolution,[status(thm)],[f25,f32]) ).
fof(f53,plain,
! [X0,X1] :
( product(X1,identity_for(X1),X0,multiply(X1,identity_for(X1),X0))
| ~ group_member(X0,X1) ),
inference(resolution,[status(thm)],[f25,f31]) ).
fof(f54,plain,
! [X0] :
( group_member(multiply(g,a,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f39,f32]) ).
fof(f55,plain,
! [X0] :
( product(g,a,X0,multiply(g,a,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f39,f31]) ).
fof(f56,plain,
! [X0] :
( group_member(multiply(g,b,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f40,f32]) ).
fof(f57,plain,
! [X0] :
( product(g,b,X0,multiply(g,b,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f40,f31]) ).
fof(f58,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ product(X0,identity_for(X0),X1,X2) ),
inference(resolution,[status(thm)],[f26,f34]) ).
fof(f59,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ product(X0,X1,identity_for(X0),X2) ),
inference(resolution,[status(thm)],[f27,f34]) ).
fof(f60,plain,
group_member(inverse(g,b),g),
inference(resolution,[status(thm)],[f28,f40]) ).
fof(f61,plain,
group_member(inverse(g,a),g),
inference(resolution,[status(thm)],[f28,f39]) ).
fof(f67,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,identity_for(X0),X3,X4)
| ~ product(X0,X1,X2,X4)
| ~ product(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f36,f26]) ).
fof(f68,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,X3,X2,X4)
| ~ product(X0,X3,X1,X4)
| ~ product(X0,identity_for(X0),X1,X2) ),
inference(resolution,[status(thm)],[f36,f27]) ).
fof(f69,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,X1,X2,X4)
| ~ product(X0,identity_for(X0),X3,X4)
| ~ product(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f38,f26]) ).
fof(f70,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,X3,X1,X4)
| ~ product(X0,X3,X2,X4)
| ~ product(X0,identity_for(X0),X1,X2) ),
inference(resolution,[status(thm)],[f38,f27]) ).
fof(f71,plain,
group_member(inverse(g,c),g),
inference(resolution,[status(thm)],[f41,f28]) ).
fof(f72,plain,
! [X0] :
( group_member(multiply(g,c,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f41,f32]) ).
fof(f73,plain,
! [X0] :
( product(g,c,X0,multiply(g,c,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f41,f31]) ).
fof(f74,plain,
group_member(inverse(g,d),g),
inference(resolution,[status(thm)],[f42,f28]) ).
fof(f75,plain,
! [X0] :
( group_member(multiply(g,d,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f42,f32]) ).
fof(f76,plain,
! [X0] :
( product(g,d,X0,multiply(g,d,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f42,f31]) ).
fof(f77,plain,
group_member(inverse(g,i),g),
inference(resolution,[status(thm)],[f43,f28]) ).
fof(f78,plain,
! [X0] :
( group_member(multiply(g,i,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f43,f32]) ).
fof(f79,plain,
! [X0] :
( product(g,i,X0,multiply(g,i,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f43,f31]) ).
fof(f80,plain,
! [X0] : identity_for(X0) = inverse(X0,identity_for(X0)),
inference(resolution,[status(thm)],[f29,f59]) ).
fof(f81,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,identity_for(X0),X2,X4)
| ~ product(X0,inverse(X0,X1),X3,X4)
| ~ product(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f29,f38]) ).
fof(f82,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,inverse(X0,X1),X3,X4)
| ~ product(X0,identity_for(X0),X2,X4)
| ~ product(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f29,f36]) ).
fof(f83,plain,
! [X0,X1,X2] :
( X2 = identity_for(X0)
| ~ product(X0,inverse(X0,X1),X1,X2) ),
inference(resolution,[status(thm)],[f29,f34]) ).
fof(f85,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,identity_for(X0),X2,X4)
| ~ product(X0,X1,X3,X4)
| ~ product(X0,inverse(X0,X1),X2,X3) ),
inference(resolution,[status(thm)],[f30,f38]) ).
fof(f86,plain,
! [X0,X1,X2,X3,X4] :
( product(X0,X1,X3,X4)
| ~ product(X0,identity_for(X0),X2,X4)
| ~ product(X0,inverse(X0,X1),X2,X3) ),
inference(resolution,[status(thm)],[f30,f36]) ).
fof(f87,plain,
! [X0,X1,X2] :
( X2 = identity_for(X0)
| ~ product(X0,X1,inverse(X0,X1),X2) ),
inference(resolution,[status(thm)],[f30,f34]) ).
fof(f88,plain,
! [X0] : product(g,X0,inverse(g,X0),i),
inference(paramodulation,[status(thm)],[f44,f30]) ).
fof(f89,plain,
! [X0] : product(g,inverse(g,X0),X0,i),
inference(paramodulation,[status(thm)],[f44,f29]) ).
fof(f90,plain,
! [X0,X1] :
( X1 = X0
| ~ product(g,X0,i,X1) ),
inference(paramodulation,[status(thm)],[f44,f59]) ).
fof(f91,plain,
! [X0,X1] :
( X1 = X0
| ~ product(g,i,X0,X1) ),
inference(paramodulation,[status(thm)],[f44,f58]) ).
fof(f92,plain,
! [X0] : product(g,X0,i,X0),
inference(paramodulation,[status(thm)],[f44,f27]) ).
fof(f93,plain,
! [X0] : product(g,i,X0,X0),
inference(paramodulation,[status(thm)],[f44,f26]) ).
fof(f95,plain,
identity_for(g) = inverse(g,i),
inference(paramodulation,[status(thm)],[f44,f80]) ).
fof(f98,plain,
i = inverse(g,i),
inference(forward_demodulation,[status(thm)],[f44,f95]) ).
fof(f99,plain,
group_member(multiply(g,identity_for(g),i),g),
inference(resolution,[status(thm)],[f52,f43]) ).
fof(f100,plain,
group_member(multiply(g,identity_for(g),d),g),
inference(resolution,[status(thm)],[f52,f42]) ).
fof(f101,plain,
group_member(multiply(g,identity_for(g),c),g),
inference(resolution,[status(thm)],[f52,f41]) ).
fof(f102,plain,
group_member(multiply(g,identity_for(g),b),g),
inference(resolution,[status(thm)],[f52,f40]) ).
fof(f103,plain,
group_member(multiply(g,identity_for(g),a),g),
inference(resolution,[status(thm)],[f52,f39]) ).
fof(f104,plain,
! [X0] : group_member(multiply(X0,identity_for(X0),identity_for(X0)),X0),
inference(resolution,[status(thm)],[f52,f25]) ).
fof(f105,plain,
group_member(multiply(g,i,i),g),
inference(forward_demodulation,[status(thm)],[f44,f99]) ).
fof(f106,plain,
group_member(multiply(g,i,d),g),
inference(forward_demodulation,[status(thm)],[f44,f100]) ).
fof(f107,plain,
group_member(multiply(g,i,c),g),
inference(forward_demodulation,[status(thm)],[f44,f101]) ).
fof(f108,plain,
group_member(multiply(g,i,b),g),
inference(forward_demodulation,[status(thm)],[f44,f102]) ).
fof(f109,plain,
group_member(multiply(g,i,a),g),
inference(forward_demodulation,[status(thm)],[f44,f103]) ).
fof(f111,plain,
product(g,i,i,identity_for(g)),
inference(paramodulation,[status(thm)],[f98,f29]) ).
fof(f113,plain,
product(g,i,i,i),
inference(forward_demodulation,[status(thm)],[f44,f111]) ).
fof(f114,plain,
product(g,identity_for(g),i,multiply(g,identity_for(g),i)),
inference(resolution,[status(thm)],[f53,f43]) ).
fof(f115,plain,
product(g,identity_for(g),d,multiply(g,identity_for(g),d)),
inference(resolution,[status(thm)],[f53,f42]) ).
fof(f116,plain,
product(g,identity_for(g),c,multiply(g,identity_for(g),c)),
inference(resolution,[status(thm)],[f53,f41]) ).
fof(f117,plain,
product(g,identity_for(g),b,multiply(g,identity_for(g),b)),
inference(resolution,[status(thm)],[f53,f40]) ).
fof(f118,plain,
product(g,identity_for(g),a,multiply(g,identity_for(g),a)),
inference(resolution,[status(thm)],[f53,f39]) ).
fof(f119,plain,
! [X0] : product(X0,identity_for(X0),identity_for(X0),multiply(X0,identity_for(X0),identity_for(X0))),
inference(resolution,[status(thm)],[f53,f25]) ).
fof(f120,plain,
product(g,i,i,multiply(g,identity_for(g),i)),
inference(forward_demodulation,[status(thm)],[f44,f114]) ).
fof(f121,plain,
product(g,i,i,multiply(g,i,i)),
inference(forward_demodulation,[status(thm)],[f44,f120]) ).
fof(f122,plain,
product(g,i,d,multiply(g,identity_for(g),d)),
inference(forward_demodulation,[status(thm)],[f44,f115]) ).
fof(f123,plain,
product(g,i,d,multiply(g,i,d)),
inference(forward_demodulation,[status(thm)],[f44,f122]) ).
fof(f124,plain,
product(g,i,c,multiply(g,identity_for(g),c)),
inference(forward_demodulation,[status(thm)],[f44,f116]) ).
fof(f125,plain,
product(g,i,c,multiply(g,i,c)),
inference(forward_demodulation,[status(thm)],[f44,f124]) ).
fof(f126,plain,
product(g,i,b,multiply(g,identity_for(g),b)),
inference(forward_demodulation,[status(thm)],[f44,f117]) ).
fof(f127,plain,
product(g,i,b,multiply(g,i,b)),
inference(forward_demodulation,[status(thm)],[f44,f126]) ).
fof(f128,plain,
product(g,i,a,multiply(g,identity_for(g),a)),
inference(forward_demodulation,[status(thm)],[f44,f118]) ).
fof(f129,plain,
product(g,i,a,multiply(g,i,a)),
inference(forward_demodulation,[status(thm)],[f44,f128]) ).
fof(f130,plain,
group_member(multiply(g,a,i),g),
inference(resolution,[status(thm)],[f54,f43]) ).
fof(f131,plain,
group_member(multiply(g,a,d),g),
inference(resolution,[status(thm)],[f54,f42]) ).
fof(f132,plain,
group_member(multiply(g,a,c),g),
inference(resolution,[status(thm)],[f54,f41]) ).
fof(f133,plain,
group_member(multiply(g,a,b),g),
inference(resolution,[status(thm)],[f54,f40]) ).
fof(f134,plain,
group_member(multiply(g,a,a),g),
inference(resolution,[status(thm)],[f54,f39]) ).
fof(f135,plain,
group_member(multiply(g,a,identity_for(g)),g),
inference(resolution,[status(thm)],[f54,f25]) ).
fof(f136,plain,
group_member(multiply(g,a,i),g),
inference(forward_demodulation,[status(thm)],[f44,f135]) ).
fof(f138,plain,
! [X0,X1,X2,X3] :
( product(g,X2,X0,X3)
| ~ product(g,X2,X1,X3)
| ~ product(g,i,X0,X1) ),
inference(resolution,[status(thm)],[f92,f38]) ).
fof(f139,plain,
! [X0,X1,X2,X3] :
( product(g,X2,X1,X3)
| ~ product(g,X2,X0,X3)
| ~ product(g,i,X0,X1) ),
inference(resolution,[status(thm)],[f92,f36]) ).
fof(f140,plain,
! [X0,X1] :
( X1 = X0
| ~ product(g,X0,i,X1) ),
inference(resolution,[status(thm)],[f92,f34]) ).
fof(f142,plain,
! [X0,X1,X2,X3] :
( product(g,X0,X1,X3)
| ~ product(g,i,X2,X3)
| ~ product(g,X0,X1,X2) ),
inference(resolution,[status(thm)],[f93,f38]) ).
fof(f143,plain,
! [X0,X1,X2,X3] :
( product(g,i,X2,X3)
| ~ product(g,X0,X1,X3)
| ~ product(g,X0,X1,X2) ),
inference(resolution,[status(thm)],[f93,f36]) ).
fof(f144,plain,
! [X0,X1] :
( X1 = X0
| ~ product(g,i,X0,X1) ),
inference(resolution,[status(thm)],[f93,f34]) ).
fof(f146,plain,
( i = i
| i = d
| i = c
| i = b
| i = a ),
inference(resolution,[status(thm)],[f45,f43]) ).
fof(f147,plain,
( d = i
| d = d
| d = c
| d = b
| d = a ),
inference(resolution,[status(thm)],[f45,f42]) ).
fof(f148,plain,
( c = i
| c = d
| c = c
| c = b
| c = a ),
inference(resolution,[status(thm)],[f45,f41]) ).
fof(f149,plain,
( b = i
| b = d
| b = c
| b = b
| b = a ),
inference(resolution,[status(thm)],[f45,f40]) ).
fof(f150,plain,
( a = i
| a = d
| a = c
| a = b
| a = a ),
inference(resolution,[status(thm)],[f45,f39]) ).
fof(f151,plain,
( identity_for(g) = i
| identity_for(g) = d
| identity_for(g) = c
| identity_for(g) = b
| identity_for(g) = a ),
inference(resolution,[status(thm)],[f45,f25]) ).
fof(f152,definition,
( sQ0_spl
<=> i = a ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f153,plain,
( ~ sQ0_spl
| i = a ),
inference(component_clause,[status(thm)],[f152]) ).
fof(f155,definition,
( sQ1_spl
<=> i = b ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f156,plain,
( ~ sQ1_spl
| i = b ),
inference(component_clause,[status(thm)],[f155]) ).
fof(f158,definition,
( sQ2_spl
<=> i = c ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f159,plain,
( ~ sQ2_spl
| i = c ),
inference(component_clause,[status(thm)],[f158]) ).
fof(f161,definition,
( sQ3_spl
<=> i = d ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f162,plain,
( ~ sQ3_spl
| i = d ),
inference(component_clause,[status(thm)],[f161]) ).
fof(f164,definition,
( sQ4_spl
<=> i = i ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f167,plain,
( sQ4_spl
| sQ3_spl
| sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f146,f152,f155,f158,f161,f164]) ).
fof(f168,definition,
( sQ5_spl
<=> d = a ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f169,plain,
( ~ sQ5_spl
| d = a ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,definition,
( sQ6_spl
<=> d = b ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f172,plain,
( ~ sQ6_spl
| d = b ),
inference(component_clause,[status(thm)],[f171]) ).
fof(f174,definition,
( sQ7_spl
<=> d = c ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f175,plain,
( ~ sQ7_spl
| d = c ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,definition,
( sQ8_spl
<=> d = d ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f180,plain,
( sQ3_spl
| sQ8_spl
| sQ7_spl
| sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f147,f168,f171,f174,f177,f161]) ).
fof(f181,definition,
( sQ9_spl
<=> c = a ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( ~ sQ9_spl
| c = a ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f184,definition,
( sQ10_spl
<=> c = b ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( ~ sQ10_spl
| c = b ),
inference(component_clause,[status(thm)],[f184]) ).
fof(f187,definition,
( sQ11_spl
<=> c = c ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f190,plain,
( sQ2_spl
| sQ7_spl
| sQ11_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f148,f181,f184,f187,f174,f158]) ).
fof(f191,definition,
( sQ12_spl
<=> b = a ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( ~ sQ12_spl
| b = a ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,definition,
( sQ13_spl
<=> b = b ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( sQ1_spl
| sQ6_spl
| sQ10_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f149,f191,f194,f184,f171,f155]) ).
fof(f198,definition,
( sQ14_spl
<=> a = a ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f201,plain,
( sQ0_spl
| sQ5_spl
| sQ9_spl
| sQ12_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f150,f198,f191,f181,f168,f152]) ).
fof(f202,definition,
( sQ15_spl
<=> identity_for(g) = a ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f203,plain,
( ~ sQ15_spl
| identity_for(g) = a ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f205,definition,
( sQ16_spl
<=> identity_for(g) = b ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f206,plain,
( ~ sQ16_spl
| identity_for(g) = b ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,definition,
( sQ17_spl
<=> identity_for(g) = c ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f209,plain,
( ~ sQ17_spl
| identity_for(g) = c ),
inference(component_clause,[status(thm)],[f208]) ).
fof(f211,definition,
( sQ18_spl
<=> identity_for(g) = d ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f212,plain,
( ~ sQ18_spl
| identity_for(g) = d ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,definition,
( sQ19_spl
<=> identity_for(g) = i ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( sQ19_spl
| sQ18_spl
| sQ17_spl
| sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f151,f202,f205,f208,f211,f214]) ).
fof(f218,plain,
product(g,a,i,multiply(g,a,i)),
inference(resolution,[status(thm)],[f55,f43]) ).
fof(f219,plain,
product(g,a,d,multiply(g,a,d)),
inference(resolution,[status(thm)],[f55,f42]) ).
fof(f220,plain,
product(g,a,c,multiply(g,a,c)),
inference(resolution,[status(thm)],[f55,f41]) ).
fof(f221,plain,
product(g,a,b,multiply(g,a,b)),
inference(resolution,[status(thm)],[f55,f40]) ).
fof(f222,plain,
product(g,a,a,multiply(g,a,a)),
inference(resolution,[status(thm)],[f55,f39]) ).
fof(f223,plain,
product(g,a,identity_for(g),multiply(g,a,identity_for(g))),
inference(resolution,[status(thm)],[f55,f25]) ).
fof(f224,plain,
product(g,a,i,multiply(g,a,identity_for(g))),
inference(forward_demodulation,[status(thm)],[f44,f223]) ).
fof(f225,plain,
product(g,a,i,multiply(g,a,i)),
inference(forward_demodulation,[status(thm)],[f44,f224]) ).
fof(f231,plain,
group_member(multiply(g,b,i),g),
inference(resolution,[status(thm)],[f56,f43]) ).
fof(f232,plain,
group_member(multiply(g,b,d),g),
inference(resolution,[status(thm)],[f56,f42]) ).
fof(f233,plain,
group_member(multiply(g,b,c),g),
inference(resolution,[status(thm)],[f56,f41]) ).
fof(f234,plain,
group_member(multiply(g,b,b),g),
inference(resolution,[status(thm)],[f56,f40]) ).
fof(f235,plain,
group_member(multiply(g,b,a),g),
inference(resolution,[status(thm)],[f56,f39]) ).
fof(f236,plain,
group_member(multiply(g,b,identity_for(g)),g),
inference(resolution,[status(thm)],[f56,f25]) ).
fof(f237,plain,
group_member(multiply(g,b,i),g),
inference(forward_demodulation,[status(thm)],[f44,f236]) ).
fof(f243,plain,
product(g,b,i,multiply(g,b,i)),
inference(resolution,[status(thm)],[f57,f43]) ).
fof(f244,plain,
product(g,b,d,multiply(g,b,d)),
inference(resolution,[status(thm)],[f57,f42]) ).
fof(f245,plain,
product(g,b,c,multiply(g,b,c)),
inference(resolution,[status(thm)],[f57,f41]) ).
fof(f246,plain,
product(g,b,b,multiply(g,b,b)),
inference(resolution,[status(thm)],[f57,f40]) ).
fof(f247,plain,
product(g,b,a,multiply(g,b,a)),
inference(resolution,[status(thm)],[f57,f39]) ).
fof(f248,plain,
product(g,b,identity_for(g),multiply(g,b,identity_for(g))),
inference(resolution,[status(thm)],[f57,f25]) ).
fof(f249,plain,
product(g,b,i,multiply(g,b,identity_for(g))),
inference(forward_demodulation,[status(thm)],[f44,f248]) ).
fof(f250,plain,
product(g,b,i,multiply(g,b,i)),
inference(forward_demodulation,[status(thm)],[f44,f249]) ).
fof(f252,plain,
! [X0,X1] :
( product(g,identity_for(g),X0,X1)
| ~ product(g,X0,i,X1) ),
inference(resolution,[status(thm)],[f67,f92]) ).
fof(f253,plain,
! [X0,X1,X2] :
( product(X0,identity_for(X0),identity_for(X0),X2)
| ~ product(X0,inverse(X0,X1),X1,X2) ),
inference(resolution,[status(thm)],[f67,f29]) ).
fof(f255,plain,
! [X0,X1,X2] :
( product(X0,identity_for(X0),identity_for(X0),X2)
| ~ product(X0,X1,inverse(X0,X1),X2) ),
inference(resolution,[status(thm)],[f67,f30]) ).
fof(f256,plain,
! [X0,X1,X2] :
( product(X0,identity_for(X0),X1,X2)
| ~ product(X0,X1,identity_for(X0),X2) ),
inference(resolution,[status(thm)],[f67,f27]) ).
fof(f257,plain,
! [X0,X1] :
( product(g,i,X0,X1)
| ~ product(g,X0,i,X1) ),
inference(forward_demodulation,[status(thm)],[f44,f252]) ).
fof(f258,plain,
! [X0,X1] :
( ~ sQ0_spl
| X1 = X0
| ~ product(g,a,X0,X1) ),
inference(backward_demodulation,[status(thm)],[f153,f91]) ).
fof(f259,plain,
! [X0,X1] :
( ~ sQ0_spl
| X1 = X0
| ~ product(g,X0,a,X1) ),
inference(backward_demodulation,[status(thm)],[f153,f90]) ).
fof(f260,plain,
! [X0] :
( ~ sQ0_spl
| multiply(g,X0,multiply(g,X0,multiply(g,X0,multiply(g,X0,X0)))) = a ),
inference(backward_demodulation,[status(thm)],[f153,f46]) ).
fof(f261,plain,
! [X0] :
( ~ sQ0_spl
| X0 = a
| X0 = d
| X0 = c
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(backward_demodulation,[status(thm)],[f153,f45]) ).
fof(f262,plain,
! [X0] :
( ~ sQ0_spl
| product(g,a,X0,X0) ),
inference(backward_demodulation,[status(thm)],[f153,f93]) ).
fof(f263,plain,
! [X0] :
( ~ sQ0_spl
| product(g,X0,a,X0) ),
inference(backward_demodulation,[status(thm)],[f153,f92]) ).
fof(f264,plain,
( ~ sQ0_spl
| i = inverse(g,a) ),
inference(backward_demodulation,[status(thm)],[f153,f98]) ).
fof(f265,plain,
( ~ sQ0_spl
| identity_for(g) = a ),
inference(backward_demodulation,[status(thm)],[f153,f44]) ).
fof(f267,plain,
! [X0] :
( ~ sQ0_spl
| X0 = d
| X0 = c
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(duplicate_literals_removal,[status(thm)],[f261]) ).
fof(f268,plain,
( ~ sQ0_spl
| a = inverse(g,a) ),
inference(forward_demodulation,[status(thm)],[f153,f264]) ).
fof(f271,plain,
! [X0] :
( ~ sQ0_spl
| ~ sQ9_spl
| X0 = d
| X0 = a
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f182,f267]) ).
fof(f272,plain,
! [X0] :
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| X0 = a
| X0 = a
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f169,f271]) ).
fof(f273,plain,
! [X0] :
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(duplicate_literals_removal,[status(thm)],[f272]) ).
fof(f274,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| b = b
| b = a ),
inference(resolution,[status(thm)],[f273,f40]) ).
fof(f275,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| a = b
| a = a ),
inference(resolution,[status(thm)],[f273,f39]) ).
fof(f276,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| identity_for(g) = b
| identity_for(g) = a ),
inference(resolution,[status(thm)],[f273,f25]) ).
fof(f277,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f274,f191,f194,f168,f181,f152]) ).
fof(f278,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| sQ12_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f275,f198,f191,f168,f181,f152]) ).
fof(f279,plain,
( ~ sQ0_spl
| ~ sQ9_spl
| ~ sQ5_spl
| sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f276,f202,f205,f168,f181,f152]) ).
fof(f280,plain,
product(g,i,i,identity_for(g)),
inference(paramodulation,[status(thm)],[f98,f30]) ).
fof(f281,plain,
product(g,i,i,identity_for(g)),
inference(paramodulation,[status(thm)],[f98,f29]) ).
fof(f285,plain,
! [X0] :
( product(g,identity_for(g),i,X0)
| ~ product(g,i,i,X0) ),
inference(resolution,[status(thm)],[f113,f67]) ).
fof(f286,plain,
! [X0,X1,X2] :
( product(g,i,X0,X2)
| ~ product(g,i,X1,X2)
| ~ product(g,i,X0,X1) ),
inference(resolution,[status(thm)],[f113,f38]) ).
fof(f287,plain,
! [X0,X1,X2] :
( product(g,i,X1,X2)
| ~ product(g,i,X0,X2)
| ~ product(g,i,X0,X1) ),
inference(resolution,[status(thm)],[f113,f36]) ).
fof(f288,plain,
! [X0] :
( X0 = i
| ~ product(g,i,i,X0) ),
inference(resolution,[status(thm)],[f113,f34]) ).
fof(f293,plain,
! [X0] :
( product(g,i,i,X0)
| ~ product(g,identity_for(g),i,X0) ),
inference(resolution,[status(thm)],[f69,f113]) ).
fof(f294,plain,
! [X0,X1,X2] :
( product(X0,inverse(X0,X2),X2,X1)
| ~ product(X0,identity_for(X0),identity_for(X0),X1) ),
inference(resolution,[status(thm)],[f69,f29]) ).
fof(f296,plain,
! [X0,X1,X2] :
( product(X0,X2,inverse(X0,X2),X1)
| ~ product(X0,identity_for(X0),identity_for(X0),X1) ),
inference(resolution,[status(thm)],[f69,f30]) ).
fof(f297,plain,
! [X0,X1,X2] :
( product(X0,X1,identity_for(X0),X2)
| ~ product(X0,identity_for(X0),X1,X2) ),
inference(resolution,[status(thm)],[f69,f27]) ).
fof(f305,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ12_spl
| X1 = X0
| ~ product(g,X0,a,X1) ),
inference(backward_demodulation,[status(thm)],[f309,f140]) ).
fof(f306,plain,
( ~ sQ1_spl
| ~ sQ12_spl
| product(g,i,i,a) ),
inference(backward_demodulation,[status(thm)],[f309,f113]) ).
fof(f307,plain,
( ~ sQ1_spl
| ~ sQ12_spl
| i = inverse(g,a) ),
inference(backward_demodulation,[status(thm)],[f309,f98]) ).
fof(f308,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ12_spl
| multiply(g,X0,multiply(g,X0,multiply(g,X0,multiply(g,X0,X0)))) = a ),
inference(backward_demodulation,[status(thm)],[f309,f46]) ).
fof(f309,plain,
( ~ sQ1_spl
| ~ sQ12_spl
| i = a ),
inference(forward_demodulation,[status(thm)],[f192,f156]) ).
fof(f310,plain,
( ~ sQ1_spl
| ~ sQ12_spl
| product(g,a,i,a) ),
inference(forward_demodulation,[status(thm)],[f309,f306]) ).
fof(f311,plain,
( ~ sQ1_spl
| ~ sQ12_spl
| product(g,a,a,a) ),
inference(forward_demodulation,[status(thm)],[f309,f310]) ).
fof(f312,plain,
( ~ sQ1_spl
| ~ sQ12_spl
| a = inverse(g,a) ),
inference(forward_demodulation,[status(thm)],[f309,f307]) ).
fof(f313,plain,
( ~ sQ6_spl
| ~ sQ12_spl
| d = a ),
inference(forward_demodulation,[status(thm)],[f192,f172]) ).
fof(f314,plain,
! [X0] :
( ~ sQ12_spl
| X0 = i
| X0 = d
| X0 = c
| X0 = a
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f192,f45]) ).
fof(f315,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ6_spl
| X0 = i
| X0 = a
| X0 = c
| X0 = a
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f313,f314]) ).
fof(f316,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ6_spl
| ~ sQ1_spl
| X0 = a
| X0 = a
| X0 = c
| X0 = a
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f309,f315]) ).
fof(f317,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ6_spl
| ~ sQ1_spl
| X0 = c
| X0 = a
| ~ group_member(X0,g) ),
inference(duplicate_literals_removal,[status(thm)],[f316]) ).
fof(f318,plain,
( ~ sQ12_spl
| ~ sQ6_spl
| ~ sQ1_spl
| a = c
| a = a ),
inference(resolution,[status(thm)],[f317,f39]) ).
fof(f319,plain,
( ~ sQ12_spl
| ~ sQ6_spl
| ~ sQ1_spl
| identity_for(g) = c
| identity_for(g) = a ),
inference(resolution,[status(thm)],[f317,f25]) ).
fof(f320,plain,
( ~ sQ12_spl
| ~ sQ6_spl
| ~ sQ1_spl
| sQ9_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f318,f198,f181,f155,f171,f191]) ).
fof(f321,plain,
( ~ sQ12_spl
| ~ sQ6_spl
| ~ sQ1_spl
| sQ17_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f319,f202,f208,f155,f171,f191]) ).
fof(f322,plain,
! [X0,X1,X2,X3] :
( product(g,X2,X0,X3)
| ~ product(g,X2,X1,X3)
| ~ product(g,i,X0,X1) ),
inference(paramodulation,[status(thm)],[f44,f70]) ).
fof(f323,plain,
! [X0,X1,X2,X3] :
( product(g,X2,X1,X3)
| ~ product(g,X2,X0,X3)
| ~ product(g,i,X0,X1) ),
inference(paramodulation,[status(thm)],[f44,f68]) ).
fof(f324,plain,
identity_for(g) = inverse(g,i),
inference(paramodulation,[status(thm)],[f44,f80]) ).
fof(f325,plain,
! [X0] : product(g,X0,inverse(g,X0),i),
inference(paramodulation,[status(thm)],[f44,f30]) ).
fof(f326,plain,
! [X0] : product(g,inverse(g,X0),X0,i),
inference(paramodulation,[status(thm)],[f44,f29]) ).
fof(f327,plain,
! [X0,X1] :
( X1 = X0
| ~ product(g,X0,i,X1) ),
inference(paramodulation,[status(thm)],[f44,f59]) ).
fof(f328,plain,
! [X0,X1] :
( X1 = X0
| ~ product(g,i,X0,X1) ),
inference(paramodulation,[status(thm)],[f44,f58]) ).
fof(f329,plain,
! [X0] : product(g,X0,i,X0),
inference(paramodulation,[status(thm)],[f44,f27]) ).
fof(f330,plain,
! [X0] : product(g,i,X0,X0),
inference(paramodulation,[status(thm)],[f44,f26]) ).
fof(f331,plain,
group_member(i,g),
inference(paramodulation,[status(thm)],[f44,f25]) ).
fof(f332,plain,
i = inverse(g,i),
inference(forward_demodulation,[status(thm)],[f44,f324]) ).
fof(f333,plain,
product(g,a,i,multiply(g,a,i)),
inference(resolution,[status(thm)],[f43,f55]) ).
fof(f334,plain,
group_member(multiply(g,a,i),g),
inference(resolution,[status(thm)],[f43,f54]) ).
fof(f335,plain,
product(g,identity_for(g),i,multiply(g,identity_for(g),i)),
inference(resolution,[status(thm)],[f43,f53]) ).
fof(f336,plain,
group_member(multiply(g,identity_for(g),i),g),
inference(resolution,[status(thm)],[f43,f52]) ).
fof(f337,plain,
group_member(inverse(g,i),g),
inference(resolution,[status(thm)],[f43,f28]) ).
fof(f338,plain,
! [X0] :
( group_member(multiply(g,i,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f43,f32]) ).
fof(f339,plain,
! [X0] :
( product(g,i,X0,multiply(g,i,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f43,f31]) ).
fof(f340,plain,
product(g,i,i,multiply(g,identity_for(g),i)),
inference(forward_demodulation,[status(thm)],[f44,f335]) ).
fof(f341,plain,
product(g,i,i,multiply(g,i,i)),
inference(forward_demodulation,[status(thm)],[f44,f340]) ).
fof(f342,plain,
group_member(multiply(g,i,i),g),
inference(forward_demodulation,[status(thm)],[f44,f336]) ).
fof(f343,plain,
group_member(multiply(g,c,i),g),
inference(resolution,[status(thm)],[f72,f43]) ).
fof(f344,plain,
group_member(multiply(g,c,a),g),
inference(resolution,[status(thm)],[f72,f39]) ).
fof(f345,plain,
group_member(multiply(g,c,identity_for(g)),g),
inference(resolution,[status(thm)],[f72,f25]) ).
fof(f346,plain,
group_member(multiply(g,c,i),g),
inference(forward_demodulation,[status(thm)],[f44,f345]) ).
fof(f347,plain,
product(g,i,i,identity_for(g)),
inference(paramodulation,[status(thm)],[f98,f30]) ).
fof(f348,plain,
product(g,i,i,identity_for(g)),
inference(paramodulation,[status(thm)],[f98,f29]) ).
fof(f349,plain,
product(g,i,i,i),
inference(forward_demodulation,[status(thm)],[f44,f347]) ).
fof(f350,plain,
product(g,i,i,i),
inference(forward_demodulation,[status(thm)],[f44,f348]) ).
fof(f351,plain,
product(g,c,i,multiply(g,c,i)),
inference(resolution,[status(thm)],[f73,f43]) ).
fof(f352,plain,
product(g,c,a,multiply(g,c,a)),
inference(resolution,[status(thm)],[f73,f39]) ).
fof(f353,plain,
product(g,c,identity_for(g),multiply(g,c,identity_for(g))),
inference(resolution,[status(thm)],[f73,f25]) ).
fof(f354,plain,
product(g,c,i,multiply(g,c,identity_for(g))),
inference(forward_demodulation,[status(thm)],[f44,f353]) ).
fof(f355,plain,
product(g,c,i,multiply(g,c,i)),
inference(forward_demodulation,[status(thm)],[f44,f354]) ).
fof(f356,plain,
group_member(multiply(g,d,i),g),
inference(resolution,[status(thm)],[f75,f43]) ).
fof(f357,plain,
group_member(multiply(g,d,a),g),
inference(resolution,[status(thm)],[f75,f39]) ).
fof(f358,plain,
group_member(multiply(g,d,identity_for(g)),g),
inference(resolution,[status(thm)],[f75,f25]) ).
fof(f359,plain,
group_member(multiply(g,d,i),g),
inference(forward_demodulation,[status(thm)],[f44,f358]) ).
fof(f360,plain,
! [X0] :
( ~ sQ10_spl
| product(g,c,X0,multiply(g,b,X0))
| ~ group_member(X0,g) ),
inference(backward_demodulation,[status(thm)],[f185,f73]) ).
fof(f361,plain,
! [X0] :
( ~ sQ10_spl
| group_member(multiply(g,b,X0),g)
| ~ group_member(X0,g) ),
inference(backward_demodulation,[status(thm)],[f185,f72]) ).
fof(f362,plain,
! [X0] :
( ~ sQ10_spl
| product(g,b,X0,multiply(g,b,X0))
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f185,f360]) ).
fof(f363,plain,
( ~ sQ2_spl
| ~ sQ10_spl
| i = inverse(g,b) ),
inference(backward_demodulation,[status(thm)],[f366,f98]) ).
fof(f364,plain,
( ~ sQ2_spl
| ~ sQ10_spl
| group_member(b,g) ),
inference(backward_demodulation,[status(thm)],[f366,f43]) ).
fof(f365,plain,
( ~ sQ2_spl
| ~ sQ10_spl
| identity_for(g) = b ),
inference(backward_demodulation,[status(thm)],[f366,f44]) ).
fof(f366,plain,
( ~ sQ2_spl
| ~ sQ10_spl
| i = b ),
inference(forward_demodulation,[status(thm)],[f185,f159]) ).
fof(f367,plain,
( ~ sQ2_spl
| ~ sQ10_spl
| b = inverse(g,b) ),
inference(forward_demodulation,[status(thm)],[f366,f363]) ).
fof(f368,plain,
! [X0] :
( ~ sQ7_spl
| ~ sQ10_spl
| group_member(multiply(g,b,X0),g)
| ~ group_member(X0,g) ),
inference(backward_demodulation,[status(thm)],[f369,f75]) ).
fof(f369,plain,
( ~ sQ7_spl
| ~ sQ10_spl
| d = b ),
inference(forward_demodulation,[status(thm)],[f185,f175]) ).
fof(f370,plain,
( ~ sQ10_spl
| group_member(b,g) ),
inference(forward_demodulation,[status(thm)],[f185,f41]) ).
fof(f371,plain,
( ~ sQ10_spl
| product(g,a,b,multiply(g,a,b)) ),
inference(resolution,[status(thm)],[f370,f55]) ).
fof(f372,plain,
( ~ sQ10_spl
| group_member(multiply(g,a,b),g) ),
inference(resolution,[status(thm)],[f370,f54]) ).
fof(f373,plain,
( ~ sQ10_spl
| product(g,identity_for(g),b,multiply(g,identity_for(g),b)) ),
inference(resolution,[status(thm)],[f370,f53]) ).
fof(f374,plain,
( ~ sQ10_spl
| group_member(multiply(g,identity_for(g),b),g) ),
inference(resolution,[status(thm)],[f370,f52]) ).
fof(f375,plain,
( ~ sQ10_spl
| group_member(inverse(g,b),g) ),
inference(resolution,[status(thm)],[f370,f28]) ).
fof(f376,plain,
! [X0] :
( ~ sQ10_spl
| group_member(multiply(g,b,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f370,f32]) ).
fof(f377,plain,
! [X0] :
( ~ sQ10_spl
| product(g,b,X0,multiply(g,b,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f370,f31]) ).
fof(f379,plain,
! [X0] :
( ~ sQ10_spl
| X0 = i
| X0 = d
| X0 = b
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f185,f45]) ).
fof(f380,plain,
! [X0] :
( ~ sQ10_spl
| ~ sQ7_spl
| X0 = i
| X0 = b
| X0 = b
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f369,f379]) ).
fof(f381,plain,
! [X0] :
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| X0 = b
| X0 = b
| X0 = b
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f366,f380]) ).
fof(f382,plain,
! [X0] :
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(duplicate_literals_removal,[status(thm)],[f381]) ).
fof(f383,plain,
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| b = b
| b = a ),
inference(resolution,[status(thm)],[f382,f370]) ).
fof(f384,plain,
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| a = b
| a = a ),
inference(resolution,[status(thm)],[f382,f39]) ).
fof(f385,plain,
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| identity_for(g) = b
| identity_for(g) = a ),
inference(resolution,[status(thm)],[f382,f25]) ).
fof(f386,plain,
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f383,f191,f194,f158,f174,f184]) ).
fof(f387,plain,
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| sQ12_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f384,f198,f191,f158,f174,f184]) ).
fof(f388,plain,
( ~ sQ10_spl
| ~ sQ7_spl
| ~ sQ2_spl
| sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f385,f202,f205,f158,f174,f184]) ).
fof(f389,plain,
product(g,i,i,identity_for(g)),
inference(paramodulation,[status(thm)],[f332,f30]) ).
fof(f390,plain,
product(g,i,i,identity_for(g)),
inference(paramodulation,[status(thm)],[f332,f29]) ).
fof(f391,plain,
product(g,d,a,multiply(g,d,a)),
inference(resolution,[status(thm)],[f76,f39]) ).
fof(f392,plain,
product(g,d,identity_for(g),multiply(g,d,identity_for(g))),
inference(resolution,[status(thm)],[f76,f25]) ).
fof(f393,plain,
identity_for(g) = inverse(g,i),
inference(resolution,[status(thm)],[f144,f30]) ).
fof(f394,plain,
i = identity_for(g),
inference(resolution,[status(thm)],[f144,f27]) ).
fof(f395,plain,
identity_for(g) = i,
inference(forward_demodulation,[status(thm)],[f332,f393]) ).
fof(f396,plain,
group_member(multiply(g,i,a),g),
inference(resolution,[status(thm)],[f78,f39]) ).
fof(f397,plain,
group_member(multiply(g,i,identity_for(g)),g),
inference(resolution,[status(thm)],[f78,f25]) ).
fof(f398,plain,
product(g,i,a,multiply(g,i,a)),
inference(resolution,[status(thm)],[f79,f39]) ).
fof(f399,plain,
product(g,i,identity_for(g),multiply(g,i,identity_for(g))),
inference(resolution,[status(thm)],[f79,f25]) ).
fof(f401,plain,
! [X0] :
( ~ sQ3_spl
| group_member(multiply(g,d,X0),g)
| ~ group_member(X0,g) ),
inference(backward_demodulation,[status(thm)],[f162,f78]) ).
fof(f402,plain,
! [X0,X1] :
( ~ sQ3_spl
| X1 = X0
| ~ product(g,d,X0,X1) ),
inference(backward_demodulation,[status(thm)],[f162,f144]) ).
fof(f403,plain,
( ~ sQ3_spl
| i = inverse(g,d) ),
inference(backward_demodulation,[status(thm)],[f162,f332]) ).
fof(f405,plain,
( ~ sQ3_spl
| d = inverse(g,d) ),
inference(forward_demodulation,[status(thm)],[f162,f403]) ).
fof(f406,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| product(g,X2,X0,X3)
| ~ product(g,X2,X1,X3)
| ~ product(g,b,X0,X1) ),
inference(paramodulation,[status(thm)],[f206,f70]) ).
fof(f407,plain,
! [X0,X1,X2,X3] :
( ~ sQ16_spl
| product(g,X2,X1,X3)
| ~ product(g,X2,X0,X3)
| ~ product(g,b,X0,X1) ),
inference(paramodulation,[status(thm)],[f206,f68]) ).
fof(f408,plain,
( ~ sQ16_spl
| identity_for(g) = inverse(g,b) ),
inference(paramodulation,[status(thm)],[f206,f80]) ).
fof(f409,plain,
! [X0] :
( ~ sQ16_spl
| product(g,X0,inverse(g,X0),b) ),
inference(paramodulation,[status(thm)],[f206,f30]) ).
fof(f410,plain,
! [X0] :
( ~ sQ16_spl
| product(g,inverse(g,X0),X0,b) ),
inference(paramodulation,[status(thm)],[f206,f29]) ).
fof(f411,plain,
! [X0,X1] :
( ~ sQ16_spl
| X1 = X0
| ~ product(g,X0,b,X1) ),
inference(paramodulation,[status(thm)],[f206,f59]) ).
fof(f412,plain,
! [X0,X1] :
( ~ sQ16_spl
| X1 = X0
| ~ product(g,b,X0,X1) ),
inference(paramodulation,[status(thm)],[f206,f58]) ).
fof(f413,plain,
! [X0] :
( ~ sQ16_spl
| product(g,X0,b,X0) ),
inference(paramodulation,[status(thm)],[f206,f27]) ).
fof(f414,plain,
! [X0] :
( ~ sQ16_spl
| product(g,b,X0,X0) ),
inference(paramodulation,[status(thm)],[f206,f26]) ).
fof(f415,plain,
( ~ sQ16_spl
| group_member(b,g) ),
inference(paramodulation,[status(thm)],[f206,f25]) ).
fof(f416,plain,
( ~ sQ16_spl
| b = inverse(g,b) ),
inference(forward_demodulation,[status(thm)],[f206,f408]) ).
fof(f417,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| a = b ),
inference(backward_demodulation,[status(thm)],[f203,f206]) ).
fof(f420,plain,
( ~ sQ15_spl
| identity_for(g) = inverse(g,a) ),
inference(paramodulation,[status(thm)],[f203,f80]) ).
fof(f428,plain,
( ~ sQ15_spl
| a = inverse(g,a) ),
inference(forward_demodulation,[status(thm)],[f203,f420]) ).
fof(f429,plain,
! [X0] :
( ~ sQ3_spl
| multiply(g,X0,multiply(g,X0,multiply(g,X0,multiply(g,X0,X0)))) = d ),
inference(forward_demodulation,[status(thm)],[f162,f46]) ).
fof(f430,plain,
product(g,d,b,multiply(g,d,b)),
inference(resolution,[status(thm)],[f40,f76]) ).
fof(f431,plain,
product(g,a,b,multiply(g,a,b)),
inference(resolution,[status(thm)],[f40,f55]) ).
fof(f432,plain,
group_member(multiply(g,a,b),g),
inference(resolution,[status(thm)],[f40,f54]) ).
fof(f433,plain,
product(g,identity_for(g),b,multiply(g,identity_for(g),b)),
inference(resolution,[status(thm)],[f40,f53]) ).
fof(f434,plain,
group_member(multiply(g,identity_for(g),b),g),
inference(resolution,[status(thm)],[f40,f52]) ).
fof(f435,plain,
group_member(inverse(g,b),g),
inference(resolution,[status(thm)],[f40,f28]) ).
fof(f436,plain,
! [X0] :
( group_member(multiply(g,b,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f40,f32]) ).
fof(f437,plain,
! [X0] :
( product(g,b,X0,multiply(g,b,X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f40,f31]) ).
fof(f438,plain,
( ~ sQ15_spl
| product(g,a,b,multiply(g,identity_for(g),b)) ),
inference(forward_demodulation,[status(thm)],[f203,f433]) ).
fof(f439,plain,
( ~ sQ15_spl
| product(g,a,b,multiply(g,a,b)) ),
inference(forward_demodulation,[status(thm)],[f203,f438]) ).
fof(f440,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,b),g) ),
inference(forward_demodulation,[status(thm)],[f203,f434]) ).
fof(f441,plain,
! [X0] :
( ~ sQ3_spl
| X0 = d
| X0 = d
| X0 = c
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f162,f45]) ).
fof(f442,plain,
! [X0] :
( ~ sQ3_spl
| X0 = d
| X0 = c
| X0 = b
| X0 = a
| ~ group_member(X0,g) ),
inference(duplicate_literals_removal,[status(thm)],[f441]) ).
fof(f443,plain,
( ~ sQ3_spl
| b = d
| b = c
| b = b
| b = a ),
inference(resolution,[status(thm)],[f442,f40]) ).
fof(f444,plain,
( ~ sQ3_spl
| a = d
| a = c
| a = b
| a = a ),
inference(resolution,[status(thm)],[f442,f39]) ).
fof(f445,plain,
( ~ sQ3_spl
| identity_for(g) = d
| identity_for(g) = c
| identity_for(g) = b
| identity_for(g) = a ),
inference(resolution,[status(thm)],[f442,f25]) ).
fof(f446,plain,
( ~ sQ3_spl
| sQ6_spl
| sQ10_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f443,f191,f194,f184,f171,f161]) ).
fof(f447,plain,
( ~ sQ3_spl
| sQ5_spl
| sQ9_spl
| sQ12_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f444,f198,f191,f181,f168,f161]) ).
fof(f448,plain,
( ~ sQ3_spl
| sQ18_spl
| sQ17_spl
| sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f445,f202,f205,f208,f211,f161]) ).
fof(f449,plain,
( ~ sQ15_spl
| a = i ),
inference(forward_demodulation,[status(thm)],[f203,f395]) ).
fof(f450,plain,
! [X0,X1,X2] :
( product(X0,identity_for(X0),X1,X2)
| ~ product(X0,inverse(X0,inverse(X0,X1)),identity_for(X0),X2) ),
inference(resolution,[status(thm)],[f81,f29]) ).
fof(f455,plain,
( ~ sQ16_spl
| product(g,b,b,identity_for(g)) ),
inference(paramodulation,[status(thm)],[f416,f30]) ).
fof(f456,plain,
( ~ sQ16_spl
| product(g,b,b,identity_for(g)) ),
inference(paramodulation,[status(thm)],[f416,f29]) ).
fof(f465,plain,
! [X0] :
( ~ sQ16_spl
| X0 = identity_for(g)
| ~ product(g,b,b,X0) ),
inference(paramodulation,[status(thm)],[f416,f83]) ).
fof(f471,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| a = c ),
inference(forward_demodulation,[status(thm)],[f203,f209]) ).
fof(f473,plain,
product(g,d,d,multiply(g,d,d)),
inference(resolution,[status(thm)],[f42,f76]) ).
fof(f474,plain,
product(g,a,d,multiply(g,a,d)),
inference(resolution,[status(thm)],[f42,f55]) ).
fof(f475,plain,
group_member(multiply(g,a,d),g),
inference(resolution,[status(thm)],[f42,f54]) ).
fof(f476,plain,
product(g,identity_for(g),d,multiply(g,identity_for(g),d)),
inference(resolution,[status(thm)],[f42,f53]) ).
fof(f477,plain,
group_member(multiply(g,identity_for(g),d),g),
inference(resolution,[status(thm)],[f42,f52]) ).
fof(f478,plain,
group_member(inverse(g,d),g),
inference(resolution,[status(thm)],[f42,f28]) ).
fof(f479,plain,
! [X0] :
( group_member(multiply(g,d,X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f42,f32]) ).
fof(f481,plain,
( ~ sQ15_spl
| product(g,a,d,multiply(g,identity_for(g),d)) ),
inference(forward_demodulation,[status(thm)],[f203,f476]) ).
fof(f482,plain,
( ~ sQ15_spl
| product(g,a,d,multiply(g,a,d)) ),
inference(forward_demodulation,[status(thm)],[f203,f481]) ).
fof(f483,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,d),g) ),
inference(forward_demodulation,[status(thm)],[f203,f477]) ).
fof(f513,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| a = d ),
inference(forward_demodulation,[status(thm)],[f203,f212]) ).
fof(f517,plain,
! [X0] :
( ~ sQ16_spl
| ~ sQ15_spl
| X0 = i
| X0 = d
| X0 = c
| X0 = a
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f417,f45]) ).
fof(f518,plain,
! [X0] :
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| X0 = i
| X0 = d
| X0 = a
| X0 = a
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f471,f517]) ).
fof(f519,plain,
! [X0] :
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ18_spl
| X0 = i
| X0 = a
| X0 = a
| X0 = a
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f513,f518]) ).
fof(f520,plain,
! [X0] :
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ18_spl
| X0 = a
| X0 = a
| X0 = a
| X0 = a
| X0 = a
| ~ group_member(X0,g) ),
inference(forward_demodulation,[status(thm)],[f449,f519]) ).
fof(f521,plain,
! [X0] :
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ18_spl
| X0 = a
| ~ group_member(X0,g) ),
inference(duplicate_literals_removal,[status(thm)],[f520]) ).
fof(f524,plain,
! [X0] :
( ~ sQ15_spl
| multiply(g,X0,multiply(g,X0,multiply(g,X0,multiply(g,X0,X0)))) = a ),
inference(forward_demodulation,[status(thm)],[f449,f46]) ).
fof(f527,plain,
! [X0,X1] :
( ~ sQ15_spl
| X1 = X0
| ~ product(g,a,X0,X1) ),
inference(forward_demodulation,[status(thm)],[f449,f91]) ).
fof(f533,plain,
! [X0,X1] :
( ~ sQ15_spl
| X1 = X0
| ~ product(g,X0,a,X1) ),
inference(forward_demodulation,[status(thm)],[f449,f90]) ).
fof(f540,plain,
! [X0] :
( ~ sQ15_spl
| product(g,a,X0,X0) ),
inference(forward_demodulation,[status(thm)],[f449,f93]) ).
fof(f555,plain,
! [X0] :
( ~ sQ15_spl
| product(g,X0,a,X0) ),
inference(forward_demodulation,[status(thm)],[f449,f92]) ).
fof(f558,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,X1,inverse(g,X1),X0)
| ~ product(g,identity_for(g),a,X0) ),
inference(resolution,[status(thm)],[f555,f86]) ).
fof(f559,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,identity_for(g),a,X1)
| ~ product(g,X0,inverse(g,X0),X1) ),
inference(resolution,[status(thm)],[f555,f85]) ).
fof(f564,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,inverse(g,X1),X1,X0)
| ~ product(g,identity_for(g),a,X0) ),
inference(resolution,[status(thm)],[f555,f82]) ).
fof(f565,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,identity_for(g),a,X1)
| ~ product(g,inverse(g,X0),X0,X1) ),
inference(resolution,[status(thm)],[f555,f81]) ).
fof(f566,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,X0,a,X1)
| ~ product(g,identity_for(g),X0,X1) ),
inference(resolution,[status(thm)],[f555,f69]) ).
fof(f571,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,X1,inverse(g,X1),X0)
| ~ product(g,a,a,X0) ),
inference(forward_demodulation,[status(thm)],[f203,f558]) ).
fof(f572,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,a,a,X1)
| ~ product(g,X0,inverse(g,X0),X1) ),
inference(forward_demodulation,[status(thm)],[f203,f559]) ).
fof(f574,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,inverse(g,X1),X1,X0)
| ~ product(g,a,a,X0) ),
inference(forward_demodulation,[status(thm)],[f203,f564]) ).
fof(f575,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,a,a,X1)
| ~ product(g,inverse(g,X0),X0,X1) ),
inference(forward_demodulation,[status(thm)],[f203,f565]) ).
fof(f576,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,X0,a,X1)
| ~ product(g,a,X0,X1) ),
inference(forward_demodulation,[status(thm)],[f203,f566]) ).
fof(f599,plain,
! [X0] :
( ~ sQ15_spl
| product(g,X0,inverse(g,X0),a) ),
inference(forward_demodulation,[status(thm)],[f449,f88]) ).
fof(f611,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,a,X1,X3)
| ~ product(g,X0,X2,X3)
| ~ product(g,inverse(g,X0),X1,X2) ),
inference(resolution,[status(thm)],[f599,f38]) ).
fof(f612,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,X0,X2,X3)
| ~ product(g,a,X1,X3)
| ~ product(g,inverse(g,X0),X1,X2) ),
inference(resolution,[status(thm)],[f599,f36]) ).
fof(f613,plain,
! [X0,X1] :
( ~ sQ15_spl
| X1 = a
| ~ product(g,X0,inverse(g,X0),X1) ),
inference(resolution,[status(thm)],[f599,f34]) ).
fof(f627,plain,
! [X0] :
( ~ sQ15_spl
| product(g,inverse(g,X0),X0,a) ),
inference(forward_demodulation,[status(thm)],[f449,f89]) ).
fof(f637,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,a,X1,X3)
| ~ product(g,inverse(g,X0),X2,X3)
| ~ product(g,X0,X1,X2) ),
inference(resolution,[status(thm)],[f627,f38]) ).
fof(f638,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,inverse(g,X0),X2,X3)
| ~ product(g,a,X1,X3)
| ~ product(g,X0,X1,X2) ),
inference(resolution,[status(thm)],[f627,f36]) ).
fof(f639,plain,
! [X0,X1] :
( ~ sQ15_spl
| X1 = a
| ~ product(g,inverse(g,X0),X0,X1) ),
inference(resolution,[status(thm)],[f627,f34]) ).
fof(f680,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f449,f105]) ).
fof(f681,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f680]) ).
fof(f682,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ18_spl
| multiply(g,a,a) = a ),
inference(resolution,[status(thm)],[f681,f521]) ).
fof(f683,plain,
( ~ sQ15_spl
| product(g,a,multiply(g,a,a),multiply(g,a,multiply(g,a,a))) ),
inference(resolution,[status(thm)],[f681,f55]) ).
fof(f684,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,multiply(g,a,a)),g) ),
inference(resolution,[status(thm)],[f681,f54]) ).
fof(f685,plain,
( ~ sQ15_spl
| product(g,identity_for(g),multiply(g,a,a),multiply(g,identity_for(g),multiply(g,a,a))) ),
inference(resolution,[status(thm)],[f681,f53]) ).
fof(f686,plain,
( ~ sQ15_spl
| group_member(multiply(g,identity_for(g),multiply(g,a,a)),g) ),
inference(resolution,[status(thm)],[f681,f52]) ).
fof(f687,plain,
( ~ sQ15_spl
| group_member(inverse(g,multiply(g,a,a)),g) ),
inference(resolution,[status(thm)],[f681,f28]) ).
fof(f688,plain,
! [X0] :
( ~ sQ15_spl
| group_member(multiply(g,multiply(g,a,a),X0),g)
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f681,f32]) ).
fof(f689,plain,
! [X0] :
( ~ sQ15_spl
| product(g,multiply(g,a,a),X0,multiply(g,multiply(g,a,a),X0))
| ~ group_member(X0,g) ),
inference(resolution,[status(thm)],[f681,f31]) ).
fof(f690,plain,
( ~ sQ15_spl
| product(g,a,multiply(g,a,a),multiply(g,identity_for(g),multiply(g,a,a))) ),
inference(forward_demodulation,[status(thm)],[f203,f685]) ).
fof(f691,plain,
( ~ sQ15_spl
| product(g,a,multiply(g,a,a),multiply(g,a,multiply(g,a,a))) ),
inference(forward_demodulation,[status(thm)],[f203,f690]) ).
fof(f692,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,multiply(g,a,a)),g) ),
inference(forward_demodulation,[status(thm)],[f203,f686]) ).
fof(f693,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,d),g) ),
inference(forward_demodulation,[status(thm)],[f449,f106]) ).
fof(f695,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,c),g) ),
inference(forward_demodulation,[status(thm)],[f449,f107]) ).
fof(f707,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,b),g) ),
inference(forward_demodulation,[status(thm)],[f449,f108]) ).
fof(f708,plain,
( ~ sQ15_spl
| ~ sQ16_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f417,f707]) ).
fof(f710,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f109]) ).
fof(f713,plain,
product(g,a,multiply(g,identity_for(g),identity_for(g)),multiply(g,a,multiply(g,identity_for(g),identity_for(g)))),
inference(resolution,[status(thm)],[f104,f55]) ).
fof(f714,plain,
group_member(multiply(g,a,multiply(g,identity_for(g),identity_for(g))),g),
inference(resolution,[status(thm)],[f104,f54]) ).
fof(f720,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,identity_for(g)),g) ),
inference(paramodulation,[status(thm)],[f203,f104]) ).
fof(f721,plain,
( ~ sQ15_spl
| group_member(multiply(g,identity_for(g),a),g) ),
inference(paramodulation,[status(thm)],[f203,f104]) ).
fof(f724,plain,
( ~ sQ15_spl
| product(g,a,multiply(g,a,identity_for(g)),multiply(g,a,multiply(g,identity_for(g),identity_for(g)))) ),
inference(forward_demodulation,[status(thm)],[f203,f713]) ).
fof(f725,plain,
( ~ sQ15_spl
| product(g,a,multiply(g,a,a),multiply(g,a,multiply(g,identity_for(g),identity_for(g)))) ),
inference(forward_demodulation,[status(thm)],[f203,f724]) ).
fof(f731,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,multiply(g,a,identity_for(g))),g) ),
inference(forward_demodulation,[status(thm)],[f203,f714]) ).
fof(f732,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,multiply(g,a,a)),g) ),
inference(forward_demodulation,[status(thm)],[f203,f731]) ).
fof(f735,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f203,f720]) ).
fof(f737,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f203,f721]) ).
fof(f739,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f130]) ).
fof(f741,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f513,f131]) ).
fof(f743,plain,
( ~ sQ15_spl
| product(g,a,i,multiply(g,i,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f121]) ).
fof(f744,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,i,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f743]) ).
fof(f745,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f744]) ).
fof(f746,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f745]) ).
fof(f748,plain,
( ~ sQ15_spl
| product(g,a,d,multiply(g,i,d)) ),
inference(forward_demodulation,[status(thm)],[f449,f123]) ).
fof(f749,plain,
( ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,i,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f748]) ).
fof(f750,plain,
( ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,a,d)) ),
inference(forward_demodulation,[status(thm)],[f449,f749]) ).
fof(f751,plain,
( ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f750]) ).
fof(f753,plain,
( ~ sQ15_spl
| product(g,a,c,multiply(g,i,c)) ),
inference(forward_demodulation,[status(thm)],[f449,f125]) ).
fof(f754,plain,
( ~ sQ15_spl
| ~ sQ17_spl
| product(g,a,a,multiply(g,i,c)) ),
inference(forward_demodulation,[status(thm)],[f471,f753]) ).
fof(f755,plain,
( ~ sQ15_spl
| ~ sQ17_spl
| product(g,a,a,multiply(g,a,c)) ),
inference(forward_demodulation,[status(thm)],[f449,f754]) ).
fof(f756,plain,
( ~ sQ15_spl
| ~ sQ17_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f471,f755]) ).
fof(f758,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f471,f132]) ).
fof(f760,plain,
( ~ sQ15_spl
| product(g,a,b,multiply(g,i,b)) ),
inference(forward_demodulation,[status(thm)],[f449,f127]) ).
fof(f761,plain,
( ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,i,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f760]) ).
fof(f762,plain,
( ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,a,b)) ),
inference(forward_demodulation,[status(thm)],[f449,f761]) ).
fof(f763,plain,
( ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f762]) ).
fof(f765,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f417,f133]) ).
fof(f768,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,i,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f129]) ).
fof(f769,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f768]) ).
fof(f773,plain,
! [X0] : multiply(X0,identity_for(X0),identity_for(X0)) = identity_for(X0),
inference(resolution,[status(thm)],[f119,f58]) ).
fof(f782,plain,
( ~ sQ15_spl
| product(g,a,identity_for(g),multiply(g,identity_for(g),identity_for(g))) ),
inference(paramodulation,[status(thm)],[f203,f119]) ).
fof(f783,plain,
( ~ sQ15_spl
| product(g,identity_for(g),a,multiply(g,identity_for(g),identity_for(g))) ),
inference(paramodulation,[status(thm)],[f203,f119]) ).
fof(f784,plain,
( ~ sQ15_spl
| product(g,identity_for(g),identity_for(g),multiply(g,a,identity_for(g))) ),
inference(paramodulation,[status(thm)],[f203,f119]) ).
fof(f785,plain,
( ~ sQ15_spl
| product(g,identity_for(g),identity_for(g),multiply(g,identity_for(g),a)) ),
inference(paramodulation,[status(thm)],[f203,f119]) ).
fof(f788,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,identity_for(g),identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f782]) ).
fof(f789,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f788]) ).
fof(f790,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f203,f789]) ).
fof(f792,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,identity_for(g),identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f783]) ).
fof(f793,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f792]) ).
fof(f794,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f203,f793]) ).
fof(f796,plain,
( ~ sQ15_spl
| product(g,a,identity_for(g),multiply(g,a,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f784]) ).
fof(f797,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f796]) ).
fof(f798,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f203,f797]) ).
fof(f800,plain,
( ~ sQ15_spl
| product(g,a,identity_for(g),multiply(g,identity_for(g),a)) ),
inference(forward_demodulation,[status(thm)],[f203,f785]) ).
fof(f801,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,identity_for(g),a)) ),
inference(forward_demodulation,[status(thm)],[f203,f800]) ).
fof(f802,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f203,f801]) ).
fof(f804,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f136]) ).
fof(f806,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f417,f231]) ).
fof(f807,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f806]) ).
fof(f809,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,d),g) ),
inference(forward_demodulation,[status(thm)],[f417,f232]) ).
fof(f810,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ18_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f513,f809]) ).
fof(f812,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,X2,X0,X3)
| ~ product(g,X2,X1,X3)
| ~ product(g,a,X0,X1) ),
inference(forward_demodulation,[status(thm)],[f449,f138]) ).
fof(f819,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,X2,X1,X3)
| ~ product(g,X2,X0,X3)
| ~ product(g,a,X0,X1) ),
inference(forward_demodulation,[status(thm)],[f449,f139]) ).
fof(f826,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,X0,X1,X3)
| ~ product(g,a,X2,X3)
| ~ product(g,X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f449,f142]) ).
fof(f832,plain,
! [X0] :
( ~ sQ15_spl
| product(g,identity_for(g),identity_for(g),X0)
| ~ product(g,a,multiply(g,identity_for(g),identity_for(g)),X0) ),
inference(resolution,[status(thm)],[f826,f119]) ).
fof(f837,plain,
! [X0] :
( ~ sQ15_spl
| product(g,identity_for(g),identity_for(g),X0)
| ~ product(g,a,multiply(g,a,identity_for(g)),X0) ),
inference(forward_demodulation,[status(thm)],[f203,f832]) ).
fof(f838,plain,
! [X0] :
( ~ sQ15_spl
| product(g,identity_for(g),identity_for(g),X0)
| ~ product(g,a,multiply(g,a,a),X0) ),
inference(forward_demodulation,[status(thm)],[f203,f837]) ).
fof(f843,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,c),g) ),
inference(forward_demodulation,[status(thm)],[f417,f233]) ).
fof(f844,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f471,f843]) ).
fof(f846,plain,
! [X0,X1,X2,X3] :
( ~ sQ15_spl
| product(g,a,X2,X3)
| ~ product(g,X0,X1,X3)
| ~ product(g,X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f449,f143]) ).
fof(f852,plain,
! [X0] :
( ~ sQ15_spl
| product(g,a,multiply(g,identity_for(g),identity_for(g)),X0)
| ~ product(g,identity_for(g),identity_for(g),X0) ),
inference(resolution,[status(thm)],[f846,f119]) ).
fof(f857,plain,
! [X0] :
( ~ sQ15_spl
| product(g,a,multiply(g,identity_for(g),identity_for(g)),X0)
| ~ product(g,a,identity_for(g),X0) ),
inference(forward_demodulation,[status(thm)],[f203,f852]) ).
fof(f858,plain,
! [X0] :
( ~ sQ15_spl
| product(g,a,multiply(g,identity_for(g),identity_for(g)),X0)
| ~ product(g,a,a,X0) ),
inference(forward_demodulation,[status(thm)],[f203,f857]) ).
fof(f859,plain,
! [X0] :
( ~ sQ15_spl
| product(g,a,multiply(g,a,identity_for(g)),X0)
| ~ product(g,a,a,X0) ),
inference(forward_demodulation,[status(thm)],[f203,f858]) ).
fof(f860,plain,
! [X0] :
( ~ sQ15_spl
| product(g,a,multiply(g,a,a),X0)
| ~ product(g,a,a,X0) ),
inference(forward_demodulation,[status(thm)],[f203,f859]) ).
fof(f863,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,b),g) ),
inference(forward_demodulation,[status(thm)],[f417,f234]) ).
fof(f864,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f417,f863]) ).
fof(f866,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f417,f235]) ).
fof(f868,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f218]) ).
fof(f869,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f868]) ).
fof(f871,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f219]) ).
fof(f872,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f871]) ).
fof(f874,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f417,f237]) ).
fof(f875,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f874]) ).
fof(f883,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,c)) ),
inference(forward_demodulation,[status(thm)],[f471,f220]) ).
fof(f884,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f471,f883]) ).
fof(f886,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f221]) ).
fof(f887,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f886]) ).
fof(f893,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f225]) ).
fof(f894,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f893]) ).
fof(f896,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f334]) ).
fof(f898,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f449,f342]) ).
fof(f899,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f898]) ).
fof(f901,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,i,multiply(g,b,i)) ),
inference(forward_demodulation,[status(thm)],[f417,f243]) ).
fof(f902,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,b,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f901]) ).
fof(f903,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f417,f902]) ).
fof(f904,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f903]) ).
fof(f906,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,d,multiply(g,b,d)) ),
inference(forward_demodulation,[status(thm)],[f417,f244]) ).
fof(f907,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,b,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f906]) ).
fof(f908,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,a,d)) ),
inference(forward_demodulation,[status(thm)],[f417,f907]) ).
fof(f909,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f908]) ).
fof(f911,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f471,f343]) ).
fof(f912,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f911]) ).
fof(f914,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f471,f344]) ).
fof(f916,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f471,f346]) ).
fof(f917,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f916]) ).
fof(f919,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,c,multiply(g,b,c)) ),
inference(forward_demodulation,[status(thm)],[f417,f245]) ).
fof(f920,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| product(g,a,a,multiply(g,b,c)) ),
inference(forward_demodulation,[status(thm)],[f471,f919]) ).
fof(f921,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| product(g,a,a,multiply(g,a,c)) ),
inference(forward_demodulation,[status(thm)],[f417,f920]) ).
fof(f922,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| ~ sQ17_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f471,f921]) ).
fof(f924,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,b,multiply(g,b,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f246]) ).
fof(f925,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,b,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f924]) ).
fof(f926,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f925]) ).
fof(f927,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f926]) ).
fof(f929,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,b,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f247]) ).
fof(f930,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f929]) ).
fof(f932,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f513,f356]) ).
fof(f933,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f932]) ).
fof(f935,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,i,multiply(g,b,i)) ),
inference(forward_demodulation,[status(thm)],[f417,f250]) ).
fof(f936,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,b,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f935]) ).
fof(f937,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f417,f936]) ).
fof(f938,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f937]) ).
fof(f940,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f513,f357]) ).
fof(f942,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| group_member(multiply(g,a,i),g) ),
inference(forward_demodulation,[status(thm)],[f513,f359]) ).
fof(f943,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f942]) ).
fof(f945,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,i,X0,X1)
| ~ product(g,X0,a,X1) ),
inference(forward_demodulation,[status(thm)],[f449,f257]) ).
fof(f946,plain,
! [X0,X1] :
( ~ sQ15_spl
| product(g,a,X0,X1)
| ~ product(g,X0,a,X1) ),
inference(forward_demodulation,[status(thm)],[f449,f945]) ).
fof(f975,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f449,f396]) ).
fof(f1011,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f417,f432]) ).
fof(f1020,plain,
( ~ sQ15_spl
| ~ sQ16_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f417,f440]) ).
fof(f1042,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f333]) ).
fof(f1043,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f1042]) ).
fof(f1045,plain,
( ~ sQ15_spl
| product(g,a,i,multiply(g,i,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f341]) ).
fof(f1046,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,i,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f1045]) ).
fof(f1047,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f1046]) ).
fof(f1048,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f1047]) ).
fof(f1050,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f513,f475]) ).
fof(f1052,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,i,multiply(g,c,i)) ),
inference(forward_demodulation,[status(thm)],[f471,f351]) ).
fof(f1053,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,c,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f1052]) ).
fof(f1054,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f471,f1053]) ).
fof(f1055,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f1054]) ).
fof(f1057,plain,
( ~ sQ15_spl
| ~ sQ18_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f513,f483]) ).
fof(f1059,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,c,a)) ),
inference(forward_demodulation,[status(thm)],[f471,f352]) ).
fof(f1060,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f471,f1059]) ).
fof(f1062,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,i,multiply(g,c,i)) ),
inference(forward_demodulation,[status(thm)],[f471,f355]) ).
fof(f1063,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,c,i)) ),
inference(forward_demodulation,[status(thm)],[f449,f1062]) ).
fof(f1064,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,i)) ),
inference(forward_demodulation,[status(thm)],[f471,f1063]) ).
fof(f1065,plain,
( ~ sQ17_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f1064]) ).
fof(f1069,plain,
( ~ sQ15_spl
| multiply(g,a,identity_for(g)) = identity_for(g) ),
inference(paramodulation,[status(thm)],[f203,f773]) ).
fof(f1070,plain,
( ~ sQ15_spl
| multiply(g,identity_for(g),a) = identity_for(g) ),
inference(paramodulation,[status(thm)],[f203,f773]) ).
fof(f1071,plain,
( ~ sQ15_spl
| multiply(g,identity_for(g),multiply(g,identity_for(g),multiply(g,identity_for(g),identity_for(g)))) = a ),
inference(paramodulation,[status(thm)],[f773,f524]) ).
fof(f1072,plain,
~ product(g,identity_for(g),multiply(g,identity_for(g),multiply(g,identity_for(g),identity_for(g))),not_power_of(g,identity_for(g))),
inference(paramodulation,[status(thm)],[f773,f51]) ).
fof(f1073,plain,
~ product(g,identity_for(g),multiply(g,identity_for(g),identity_for(g)),not_power_of(g,identity_for(g))),
inference(paramodulation,[status(thm)],[f773,f50]) ).
fof(f1074,plain,
~ product(g,identity_for(g),identity_for(g),not_power_of(g,identity_for(g))),
inference(paramodulation,[status(thm)],[f773,f49]) ).
fof(f1075,plain,
( ~ sQ15_spl
| multiply(g,a,a) = identity_for(g) ),
inference(forward_demodulation,[status(thm)],[f203,f1069]) ).
fof(f1077,plain,
( ~ sQ15_spl
| multiply(g,a,a) = identity_for(g) ),
inference(forward_demodulation,[status(thm)],[f203,f1070]) ).
fof(f1079,plain,
( ~ sQ15_spl
| multiply(g,a,multiply(g,identity_for(g),multiply(g,identity_for(g),identity_for(g)))) = a ),
inference(forward_demodulation,[status(thm)],[f203,f1071]) ).
fof(f1080,plain,
( ~ sQ15_spl
| multiply(g,a,multiply(g,a,multiply(g,identity_for(g),identity_for(g)))) = a ),
inference(forward_demodulation,[status(thm)],[f203,f1079]) ).
fof(f1081,plain,
( ~ sQ15_spl
| multiply(g,a,multiply(g,a,identity_for(g))) = a ),
inference(forward_demodulation,[status(thm)],[f773,f1080]) ).
fof(f1082,plain,
( ~ sQ15_spl
| multiply(g,a,multiply(g,a,a)) = a ),
inference(forward_demodulation,[status(thm)],[f203,f1081]) ).
fof(f1084,plain,
( ~ sQ15_spl
| ~ product(g,a,multiply(g,identity_for(g),multiply(g,identity_for(g),identity_for(g))),not_power_of(g,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f1072]) ).
fof(f1085,plain,
( ~ sQ15_spl
| ~ product(g,a,multiply(g,a,multiply(g,identity_for(g),identity_for(g))),not_power_of(g,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f1084]) ).
fof(f1086,plain,
( ~ sQ15_spl
| ~ product(g,a,multiply(g,a,identity_for(g)),not_power_of(g,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f773,f1085]) ).
fof(f1087,plain,
( ~ sQ15_spl
| ~ product(g,a,multiply(g,a,a),not_power_of(g,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f1086]) ).
fof(f1097,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,d,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f391]) ).
fof(f1098,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f1097]) ).
fof(f1100,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,identity_for(g),multiply(g,d,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f513,f392]) ).
fof(f1101,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,d,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f1100]) ).
fof(f1102,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f513,f1101]) ).
fof(f1103,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f203,f1102]) ).
fof(f1105,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,identity_for(g)),g) ),
inference(forward_demodulation,[status(thm)],[f449,f397]) ).
fof(f1106,plain,
( ~ sQ15_spl
| group_member(multiply(g,a,a),g) ),
inference(forward_demodulation,[status(thm)],[f203,f1105]) ).
fof(f1108,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,i,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f398]) ).
fof(f1109,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f449,f1108]) ).
fof(f1129,plain,
( ~ sQ15_spl
| product(g,a,identity_for(g),multiply(g,i,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f449,f399]) ).
fof(f1130,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,i,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f203,f1129]) ).
fof(f1131,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,identity_for(g))) ),
inference(forward_demodulation,[status(thm)],[f449,f1130]) ).
fof(f1132,plain,
( ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f203,f1131]) ).
fof(f1137,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,b,multiply(g,d,b)) ),
inference(forward_demodulation,[status(thm)],[f513,f430]) ).
fof(f1138,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,d,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f1137]) ).
fof(f1139,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,a,b)) ),
inference(forward_demodulation,[status(thm)],[f513,f1138]) ).
fof(f1140,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f1139]) ).
fof(f1142,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f431]) ).
fof(f1143,plain,
( ~ sQ16_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f1142]) ).
fof(f1146,plain,
( ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,a,b)) ),
inference(forward_demodulation,[status(thm)],[f417,f439]) ).
fof(f1147,plain,
( ~ sQ15_spl
| ~ sQ16_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f417,f1146]) ).
fof(f1149,plain,
! [X0,X1] : product(X0,identity_for(X0),X1,inverse(X0,inverse(X0,X1))),
inference(resolution,[status(thm)],[f450,f27]) ).
fof(f1166,plain,
! [X0,X1] : inverse(X0,inverse(X0,X1)) = X1,
inference(resolution,[status(thm)],[f1149,f58]) ).
fof(f1226,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,d,multiply(g,d,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f473]) ).
fof(f1227,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,d,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f1226]) ).
fof(f1228,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f1227]) ).
fof(f1229,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f1228]) ).
fof(f1231,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f474]) ).
fof(f1232,plain,
( ~ sQ18_spl
| ~ sQ15_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f1231]) ).
fof(f1235,plain,
( ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,a,d)) ),
inference(forward_demodulation,[status(thm)],[f513,f482]) ).
fof(f1236,plain,
( ~ sQ15_spl
| ~ sQ18_spl
| product(g,a,a,multiply(g,a,a)) ),
inference(forward_demodulation,[status(thm)],[f513,f1235]) ).
fof(model,axiom,
( sQ4_spl
| sQ8_spl
| sQ11_spl
| sQ13_spl
| sQ14_spl
| sQ15_spl
| sQ16_spl
| sQ17_spl
| sQ18_spl
| sQ19_spl ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP027-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n010.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 20 19:55:25 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.17/0.56 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.17/0.56 % SZS output start Saturation for theBenchmark
% See solution above
% 0.74/0.60 % Elapsed time: 0.156324 seconds
% 0.74/0.60 % CPU time: 0.914484 seconds
% 0.74/0.60 % Total memory used: 112.949 MB
% 0.74/0.60 % Net memory used: 111.732 MB
%------------------------------------------------------------------------------