%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP026-1 : TPTP v9.3.1. Bugfixed v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:28 PM UTC 2026
% Result : Unsatisfiable 27.53s 9.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP026-1 : TPTP v9.3.1. Bugfixed v2.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.38 % Computer : n001.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Sun Sep 20 19:59:49 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.15/5.40 % Drodi V4.1.1
% 27.53/9.00 % Refutation found
% 27.53/9.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 27.53/9.00 % SZS output start CNFRefutation for theBenchmark
% 27.53/9.00 fof(f1,axiom,(
% 27.53/9.00 (![Xg]: (group_member(identity_for(Xg),Xg) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f2,axiom,(
% 27.53/9.00 (![Xg,X]: (product(Xg,identity_for(Xg),X,X) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f3,axiom,(
% 27.53/9.00 (![Xg,X]: (product(Xg,X,identity_for(Xg),X) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f7,axiom,(
% 27.53/9.00 (![X,Xg,Y]: (( ~ group_member(X,Xg)| ~ group_member(Y,Xg)| product(Xg,X,Y,multiply(Xg,X,Y)) ) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f8,axiom,(
% 27.53/9.00 (![X,Xg,Y]: (( ~ group_member(X,Xg)| ~ group_member(Y,Xg)| group_member(multiply(Xg,X,Y),Xg) ) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f9,axiom,(
% 27.53/9.00 (![Xg,X,Y,Z,W]: (( ~ product(Xg,X,Y,Z)| ~ product(Xg,X,Y,W)| W = Z ) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f10,axiom,(
% 27.53/9.00 (![Xg,X,Y,Xy,Z,Yz,Xyz]: (( ~ product(Xg,X,Y,Xy)| ~ product(Xg,Y,Z,Yz)| ~ product(Xg,Xy,Z,Xyz)| product(Xg,X,Yz,Xyz) ) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f11,axiom,(
% 27.53/9.00 (![Xg,X,Y,Xy,Z,Yz,Xyz]: (( ~ product(Xg,X,Y,Xy)| ~ product(Xg,Y,Z,Yz)| ~ product(Xg,X,Yz,Xyz)| product(Xg,Xy,Z,Xyz) ) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f12,hypothesis,(
% 27.53/9.00 group_member(a,g1) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f13,hypothesis,(
% 27.53/9.00 group_member(b,g1) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f14,hypothesis,(
% 27.53/9.00 group_member(c,g1) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f15,hypothesis,(
% 27.53/9.00 group_member(f,g2) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f16,hypothesis,(
% 27.53/9.00 group_member(g,g2) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f17,hypothesis,(
% 27.53/9.00 group_member(h,g2) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f18,hypothesis,(
% 27.53/9.00 (![X]: (( ~ group_member(X,g1)| X = a| X = b| X = c ) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f19,hypothesis,(
% 27.53/9.00 (![X]: (( ~ group_member(X,g2)| X = f| X = g| X = h ) ))),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f20,hypothesis,(
% 27.53/9.00 product(g1,a,a,a) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f21,hypothesis,(
% 27.53/9.00 product(g1,a,b,b) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f22,hypothesis,(
% 27.53/9.00 product(g1,b,a,b) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f23,hypothesis,(
% 27.53/9.00 product(g1,a,c,c) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f24,hypothesis,(
% 27.53/9.00 product(g1,c,a,c) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f25,hypothesis,(
% 27.53/9.00 product(g1,b,b,c) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f26,hypothesis,(
% 27.53/9.00 product(g1,b,c,a) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f27,hypothesis,(
% 27.53/9.00 product(g1,c,b,a) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f28,hypothesis,(
% 27.53/9.00 product(g1,c,c,b) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f29,hypothesis,(
% 27.53/9.00 product(g2,f,f,f) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f30,hypothesis,(
% 27.53/9.00 product(g2,f,g,g) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f32,hypothesis,(
% 27.53/9.00 product(g2,f,h,h) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f33,hypothesis,(
% 27.53/9.00 product(g2,h,f,h) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f34,hypothesis,(
% 27.53/9.00 product(g2,g,g,h) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f35,hypothesis,(
% 27.53/9.00 product(g2,g,h,f) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f36,hypothesis,(
% 27.53/9.00 product(g2,h,g,f) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f37,hypothesis,(
% 27.53/9.00 product(g2,h,h,g) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f38,hypothesis,(
% 27.53/9.00 an_isomorphism(a) = f ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f39,hypothesis,(
% 27.53/9.00 an_isomorphism(b) = g ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f40,hypothesis,(
% 27.53/9.00 an_isomorphism(c) = h ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f41,hypothesis,(
% 27.53/9.00 group_member(d1,g1) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f42,hypothesis,(
% 27.53/9.00 group_member(d2,g1) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f43,hypothesis,(
% 27.53/9.00 group_member(d3,g1) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f44,hypothesis,(
% 27.53/9.00 product(g1,d1,d2,d3) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f45,negated_conjecture,(
% 27.53/9.00 ~ product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)) ),
% 27.53/9.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.53/9.00 fof(f46,plain,(
% 27.53/9.00 ![X0]: (group_member(identity_for(X0),X0))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f1])).
% 27.53/9.00 fof(f47,plain,(
% 27.53/9.00 ![X0,X1]: (product(X0,identity_for(X0),X1,X1))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f2])).
% 27.53/9.00 fof(f48,plain,(
% 27.53/9.00 ![X0,X1]: (product(X0,X1,identity_for(X0),X1))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f3])).
% 27.53/9.00 fof(f52,plain,(
% 27.53/9.00 ![X0,X1,X2]: (~group_member(X0,X1)|~group_member(X2,X1)|product(X1,X0,X2,multiply(X1,X0,X2)))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f7])).
% 27.53/9.00 fof(f53,plain,(
% 27.53/9.00 ![X0,X1,X2]: (~group_member(X0,X1)|~group_member(X2,X1)|group_member(multiply(X1,X0,X2),X1))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f8])).
% 27.53/9.00 fof(f54,plain,(
% 27.53/9.00 ![Z,W]: ((![Xg,X,Y]: (~product(Xg,X,Y,Z)|~product(Xg,X,Y,W)))|W=Z)),
% 27.53/9.00 inference(miniscoping,[status(thm)],[f9])).
% 27.53/9.00 fof(f55,plain,(
% 27.53/9.00 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2,X3)|~product(X0,X1,X2,X4)|X4=X3)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f54])).
% 27.53/9.00 fof(f56,plain,(
% 27.53/9.00 ![Xg,X,Yz,Xyz]: ((![Xy,Z]: ((![Y]: (~product(Xg,X,Y,Xy)|~product(Xg,Y,Z,Yz)))|~product(Xg,Xy,Z,Xyz)))|product(Xg,X,Yz,Xyz))),
% 27.53/9.00 inference(miniscoping,[status(thm)],[f10])).
% 27.53/9.00 fof(f57,plain,(
% 27.53/9.00 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2,X3)|~product(X0,X2,X4,X5)|~product(X0,X3,X4,X6)|product(X0,X1,X5,X6))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f56])).
% 27.53/9.00 fof(f58,plain,(
% 27.53/9.00 ![Xg,Xy,Z,Xyz]: ((![X,Yz]: ((![Y]: (~product(Xg,X,Y,Xy)|~product(Xg,Y,Z,Yz)))|~product(Xg,X,Yz,Xyz)))|product(Xg,Xy,Z,Xyz))),
% 27.53/9.00 inference(miniscoping,[status(thm)],[f11])).
% 27.53/9.00 fof(f59,plain,(
% 27.53/9.00 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2,X3)|~product(X0,X2,X4,X5)|~product(X0,X1,X5,X6)|product(X0,X3,X4,X6))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f58])).
% 27.53/9.00 fof(f60,plain,(
% 27.53/9.00 group_member(a,g1)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f12])).
% 27.53/9.00 fof(f61,plain,(
% 27.53/9.00 group_member(b,g1)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f13])).
% 27.53/9.00 fof(f62,plain,(
% 27.53/9.00 group_member(c,g1)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f14])).
% 27.53/9.00 fof(f63,plain,(
% 27.53/9.00 group_member(f,g2)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f15])).
% 27.53/9.00 fof(f64,plain,(
% 27.53/9.00 group_member(g,g2)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f16])).
% 27.53/9.00 fof(f65,plain,(
% 27.53/9.00 group_member(h,g2)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f17])).
% 27.53/9.00 fof(f66,plain,(
% 27.53/9.00 ![X0]: (~group_member(X0,g1)|X0=a|X0=b|X0=c)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f18])).
% 27.53/9.00 fof(f67,plain,(
% 27.53/9.00 ![X0]: (~group_member(X0,g2)|X0=f|X0=g|X0=h)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f19])).
% 27.53/9.00 fof(f68,plain,(
% 27.53/9.00 product(g1,a,a,a)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f20])).
% 27.53/9.00 fof(f69,plain,(
% 27.53/9.00 product(g1,a,b,b)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f21])).
% 27.53/9.00 fof(f70,plain,(
% 27.53/9.00 product(g1,b,a,b)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f22])).
% 27.53/9.00 fof(f71,plain,(
% 27.53/9.00 product(g1,a,c,c)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f23])).
% 27.53/9.00 fof(f72,plain,(
% 27.53/9.00 product(g1,c,a,c)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f24])).
% 27.53/9.00 fof(f73,plain,(
% 27.53/9.00 product(g1,b,b,c)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f25])).
% 27.53/9.00 fof(f74,plain,(
% 27.53/9.00 product(g1,b,c,a)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f26])).
% 27.53/9.00 fof(f75,plain,(
% 27.53/9.00 product(g1,c,b,a)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f27])).
% 27.53/9.00 fof(f76,plain,(
% 27.53/9.00 product(g1,c,c,b)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f28])).
% 27.53/9.00 fof(f77,plain,(
% 27.53/9.00 product(g2,f,f,f)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f29])).
% 27.53/9.00 fof(f78,plain,(
% 27.53/9.00 product(g2,f,g,g)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f30])).
% 27.53/9.00 fof(f80,plain,(
% 27.53/9.00 product(g2,f,h,h)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f32])).
% 27.53/9.00 fof(f81,plain,(
% 27.53/9.00 product(g2,h,f,h)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f33])).
% 27.53/9.00 fof(f82,plain,(
% 27.53/9.00 product(g2,g,g,h)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f34])).
% 27.53/9.00 fof(f83,plain,(
% 27.53/9.00 product(g2,g,h,f)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f35])).
% 27.53/9.00 fof(f84,plain,(
% 27.53/9.00 product(g2,h,g,f)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f36])).
% 27.53/9.00 fof(f85,plain,(
% 27.53/9.00 product(g2,h,h,g)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f37])).
% 27.53/9.00 fof(f86,plain,(
% 27.53/9.00 an_isomorphism(a)=f),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f38])).
% 27.53/9.00 fof(f87,plain,(
% 27.53/9.00 an_isomorphism(b)=g),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f39])).
% 27.53/9.00 fof(f88,plain,(
% 27.53/9.00 an_isomorphism(c)=h),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f40])).
% 27.53/9.00 fof(f89,plain,(
% 27.53/9.00 group_member(d1,g1)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f41])).
% 27.53/9.00 fof(f90,plain,(
% 27.53/9.00 group_member(d2,g1)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f42])).
% 27.53/9.00 fof(f91,plain,(
% 27.53/9.00 group_member(d3,g1)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f43])).
% 27.53/9.00 fof(f92,plain,(
% 27.53/9.00 product(g1,d1,d2,d3)),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f44])).
% 27.53/9.00 fof(f93,plain,(
% 27.53/9.00 ~product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3))),
% 27.53/9.00 inference(cnf_transformation,[status(thm)],[f45])).
% 27.53/9.00 fof(f94,plain,(
% 27.53/9.00 ![X0]: (~product(g1,d1,d2,X0)|d3=X0)),
% 27.53/9.00 inference(resolution,[status(thm)],[f55,f92])).
% 27.53/9.00 fof(f97,plain,(
% 27.53/9.00 ![X0,X1,X2]: (~product(g1,X0,d1,X1)|~product(g1,X1,d2,X2)|product(g1,X0,d3,X2))),
% 27.53/9.00 inference(resolution,[status(thm)],[f57,f92])).
% 27.53/9.00 fof(f100,plain,(
% 27.53/9.00 ![X0,X1,X2]: (~product(g1,X0,d1,X1)|~product(g1,X0,d3,X2)|product(g1,X1,d2,X2))),
% 27.53/9.00 inference(resolution,[status(thm)],[f59,f92])).
% 27.53/9.00 fof(f117,plain,(
% 27.53/9.00 ![X0,X1,X2]: (~product(X0,identity_for(X0),X1,X2)|X1=X2)),
% 27.53/9.00 inference(resolution,[status(thm)],[f47,f55])).
% 27.53/9.00 fof(f129,plain,(
% 27.53/9.00 ![X0,X1,X2]: (~product(X0,X1,identity_for(X0),X2)|X1=X2)),
% 27.53/9.00 inference(resolution,[status(thm)],[f48,f55])).
% 27.53/9.00 fof(f140,plain,(
% 27.53/9.00 ![X0]: (~product(g1,a,a,X0)|a=X0)),
% 27.53/9.00 inference(resolution,[status(thm)],[f68,f55])).
% 27.53/9.00 fof(f151,plain,(
% 27.53/9.00 ![X0]: (~product(g1,a,b,X0)|b=X0)),
% 27.53/9.00 inference(resolution,[status(thm)],[f69,f55])).
% 27.53/9.00 fof(f158,plain,(
% 27.53/9.00 ![X0]: (~product(g1,b,a,X0)|b=X0)),
% 27.53/9.00 inference(resolution,[status(thm)],[f70,f55])).
% 27.53/9.00 fof(f169,plain,(
% 27.53/9.00 ![X0]: (~product(g1,a,c,X0)|c=X0)),
% 27.53/9.00 inference(resolution,[status(thm)],[f71,f55])).
% 27.53/9.00 fof(f176,plain,(
% 27.53/9.00 ![X0]: (~product(g1,c,a,X0)|c=X0)),
% 27.53/9.00 inference(resolution,[status(thm)],[f72,f55])).
% 27.53/9.00 fof(f197,plain,(
% 27.53/9.00 ~group_member(d1,g1)|~group_member(d2,g1)|d3=multiply(g1,d1,d2)),
% 27.53/9.00 inference(resolution,[status(thm)],[f52,f94])).
% 27.53/9.00 fof(f198,plain,(
% 27.53/9.00 ![X0,X1]: (~group_member(X0,g1)|~group_member(d3,g1)|~product(g1,X0,d1,X1)|product(g1,X1,d2,multiply(g1,X0,d3)))),
% 27.53/9.00 inference(resolution,[status(thm)],[f52,f100])).
% 27.53/9.00 fof(f199,plain,(
% 27.53/9.00 ![X0,X1]: (~group_member(X0,g1)|~group_member(d1,g1)|~product(g1,multiply(g1,X0,d1),d2,X1)|product(g1,X0,d3,X1))),
% 27.53/9.00 inference(resolution,[status(thm)],[f52,f97])).
% 27.53/9.00 fof(f207,definition,(
% 27.53/9.00 sQ0_spl <=> (group_member(d1,g1))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f209,plain,(
% 27.53/9.00 ~group_member(d1,g1)|sQ0_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f207])).
% 27.53/9.00 fof(f210,definition,(
% 27.53/9.00 sQ1_spl <=> (group_member(d2,g1))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f212,plain,(
% 27.53/9.00 ~group_member(d2,g1)|sQ1_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f210])).
% 27.53/9.00 fof(f213,definition,(
% 27.53/9.00 sQ2_spl <=> (d3=multiply(g1,d1,d2))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f214,plain,(
% 27.53/9.00 d3=multiply(g1,d1,d2)|~sQ2_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f213])).
% 27.53/9.00 fof(f216,plain,(
% 27.53/9.00 ~sQ0_spl|~sQ1_spl|sQ2_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f197,f207,f210,f213])).
% 27.53/9.00 fof(f217,definition,(
% 27.53/9.00 ![X0,X1]: (sQ3_spl <=> (~group_member(X0,g1)|~product(g1,X0,d1,X1)|product(g1,X1,d2,multiply(g1,X0,d3))))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f220,definition,(
% 27.53/9.00 sQ4_spl <=> (group_member(d3,g1))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f223,plain,(
% 27.53/9.00 sQ3_spl|~sQ4_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f198,f217,f220])).
% 27.53/9.00 fof(f224,definition,(
% 27.53/9.00 ![X0,X1]: (sQ5_spl <=> (~group_member(X0,g1)|~product(g1,multiply(g1,X0,d1),d2,X1)|product(g1,X0,d3,X1)))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f227,plain,(
% 27.53/9.00 sQ5_spl|~sQ0_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f199,f224,f207])).
% 27.53/9.00 fof(f228,plain,(
% 27.53/9.00 $false|sQ0_spl),
% 27.53/9.00 inference(forward_subsumption_resolution,[status(thm)],[f209,f89])).
% 27.53/9.00 fof(f229,plain,(
% 27.53/9.00 sQ0_spl),
% 27.53/9.00 inference(contradiction_clause,[status(thm)],[f228])).
% 27.53/9.00 fof(f230,plain,(
% 27.53/9.00 $false|sQ1_spl),
% 27.53/9.00 inference(forward_subsumption_resolution,[status(thm)],[f212,f90])).
% 27.53/9.00 fof(f231,plain,(
% 27.53/9.00 sQ1_spl),
% 27.53/9.00 inference(contradiction_clause,[status(thm)],[f230])).
% 27.53/9.00 fof(f235,plain,(
% 27.53/9.00 ![X0,X1]: (X0=multiply(X1,identity_for(X1),X0)|~group_member(identity_for(X1),X1)|~group_member(X0,X1))),
% 27.53/9.00 inference(resolution,[status(thm)],[f117,f52])).
% 27.53/9.00 fof(f236,plain,(
% 27.53/9.00 ![X0,X1]: (X0=multiply(X1,identity_for(X1),X0)|~group_member(X0,X1))),
% 27.53/9.00 inference(forward_subsumption_resolution,[status(thm)],[f235,f46])).
% 27.53/9.00 fof(f243,plain,(
% 27.53/9.00 ![X0,X1]: (X0=multiply(X1,X0,identity_for(X1))|~group_member(X0,X1)|~group_member(identity_for(X1),X1))),
% 27.53/9.00 inference(resolution,[status(thm)],[f129,f52])).
% 27.53/9.00 fof(f244,plain,(
% 27.53/9.00 ![X0,X1]: (X0=multiply(X1,X0,identity_for(X1))|~group_member(X0,X1))),
% 27.53/9.00 inference(forward_subsumption_resolution,[status(thm)],[f243,f46])).
% 27.53/9.00 fof(f245,plain,(
% 27.53/9.00 ~group_member(d1,g1)|~group_member(d2,g1)|product(g1,d1,d2,d3)|~sQ2_spl),
% 27.53/9.00 inference(paramodulation,[status(thm)],[f214,f52])).
% 27.53/9.00 fof(f246,definition,(
% 27.53/9.00 sQ6_spl <=> (product(g1,d1,d2,d3))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f249,plain,(
% 27.53/9.00 ~sQ0_spl|~sQ1_spl|sQ6_spl|~sQ2_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f245,f207,f210,f246,f213])).
% 27.53/9.00 fof(f251,plain,(
% 27.53/9.00 a=multiply(g1,a,a)|~group_member(a,g1)|~group_member(a,g1)),
% 27.53/9.00 inference(resolution,[status(thm)],[f140,f52])).
% 27.53/9.00 fof(f252,definition,(
% 27.53/9.00 sQ7_spl <=> (a=multiply(g1,a,a))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f253,plain,(
% 27.53/9.00 a=multiply(g1,a,a)|~sQ7_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f252])).
% 27.53/9.00 fof(f255,definition,(
% 27.53/9.00 sQ8_spl <=> (group_member(a,g1))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f257,plain,(
% 27.53/9.00 ~group_member(a,g1)|sQ8_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f255])).
% 27.53/9.00 fof(f258,plain,(
% 27.53/9.00 sQ7_spl|~sQ8_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f251,f252,f255])).
% 27.53/9.00 fof(f261,plain,(
% 27.53/9.00 ~group_member(a,g1)|~group_member(a,g1)|product(g1,a,a,a)|~sQ7_spl),
% 27.53/9.00 inference(paramodulation,[status(thm)],[f253,f52])).
% 27.53/9.00 fof(f262,definition,(
% 27.53/9.00 sQ9_spl <=> (product(g1,a,a,a))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f265,plain,(
% 27.53/9.00 ~sQ8_spl|sQ9_spl|~sQ7_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f261,f255,f262,f252])).
% 27.53/9.00 fof(f266,plain,(
% 27.53/9.00 $false|sQ8_spl),
% 27.53/9.00 inference(forward_subsumption_resolution,[status(thm)],[f257,f60])).
% 27.53/9.00 fof(f267,plain,(
% 27.53/9.00 sQ8_spl),
% 27.53/9.00 inference(contradiction_clause,[status(thm)],[f266])).
% 27.53/9.00 fof(f271,plain,(
% 27.53/9.00 b=multiply(g1,a,b)|~group_member(a,g1)|~group_member(b,g1)),
% 27.53/9.00 inference(resolution,[status(thm)],[f151,f52])).
% 27.53/9.00 fof(f272,definition,(
% 27.53/9.00 sQ10_spl <=> (b=multiply(g1,a,b))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f273,plain,(
% 27.53/9.00 b=multiply(g1,a,b)|~sQ10_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f272])).
% 27.53/9.00 fof(f275,definition,(
% 27.53/9.00 sQ11_spl <=> (group_member(b,g1))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f277,plain,(
% 27.53/9.00 ~group_member(b,g1)|sQ11_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f275])).
% 27.53/9.00 fof(f278,plain,(
% 27.53/9.00 sQ10_spl|~sQ8_spl|~sQ11_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f271,f272,f255,f275])).
% 27.53/9.00 fof(f279,plain,(
% 27.53/9.00 ~group_member(a,g1)|~group_member(b,g1)|product(g1,a,b,b)|~sQ10_spl),
% 27.53/9.00 inference(paramodulation,[status(thm)],[f273,f52])).
% 27.53/9.00 fof(f280,definition,(
% 27.53/9.00 sQ12_spl <=> (product(g1,a,b,b))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f283,plain,(
% 27.53/9.00 ~sQ8_spl|~sQ11_spl|sQ12_spl|~sQ10_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f279,f255,f275,f280,f272])).
% 27.53/9.00 fof(f284,plain,(
% 27.53/9.00 $false|sQ11_spl),
% 27.53/9.00 inference(forward_subsumption_resolution,[status(thm)],[f277,f61])).
% 27.53/9.00 fof(f285,plain,(
% 27.53/9.00 sQ11_spl),
% 27.53/9.00 inference(contradiction_clause,[status(thm)],[f284])).
% 27.53/9.00 fof(f289,plain,(
% 27.53/9.00 b=multiply(g1,b,a)|~group_member(b,g1)|~group_member(a,g1)),
% 27.53/9.00 inference(resolution,[status(thm)],[f158,f52])).
% 27.53/9.00 fof(f290,definition,(
% 27.53/9.00 sQ13_spl <=> (b=multiply(g1,b,a))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f291,plain,(
% 27.53/9.00 b=multiply(g1,b,a)|~sQ13_spl),
% 27.53/9.00 inference(component_clause,[status(thm)],[f290])).
% 27.53/9.00 fof(f293,plain,(
% 27.53/9.00 sQ13_spl|~sQ11_spl|~sQ8_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f289,f290,f275,f255])).
% 27.53/9.00 fof(f294,plain,(
% 27.53/9.00 ~group_member(b,g1)|~group_member(a,g1)|product(g1,b,a,b)|~sQ13_spl),
% 27.53/9.00 inference(paramodulation,[status(thm)],[f291,f52])).
% 27.53/9.00 fof(f295,definition,(
% 27.53/9.00 sQ14_spl <=> (product(g1,b,a,b))),
% 27.53/9.00 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 27.53/9.00 fof(f298,plain,(
% 27.53/9.00 ~sQ11_spl|~sQ8_spl|sQ14_spl|~sQ13_spl),
% 27.53/9.00 inference(split_clause,[status(thm)],[f294,f275,f255,f295,f290])).
% 27.53/9.00 fof(f300,plain,(
% 27.53/9.01 c=multiply(g1,a,c)|~group_member(a,g1)|~group_member(c,g1)),
% 27.53/9.01 inference(resolution,[status(thm)],[f169,f52])).
% 27.53/9.01 fof(f301,definition,(
% 27.53/9.01 sQ15_spl <=> (c=multiply(g1,a,c))),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f302,plain,(
% 27.53/9.01 c=multiply(g1,a,c)|~sQ15_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f301])).
% 27.53/9.01 fof(f304,definition,(
% 27.53/9.01 sQ16_spl <=> (group_member(c,g1))),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f306,plain,(
% 27.53/9.01 ~group_member(c,g1)|sQ16_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f304])).
% 27.53/9.01 fof(f307,plain,(
% 27.53/9.01 sQ15_spl|~sQ8_spl|~sQ16_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f300,f301,f255,f304])).
% 27.53/9.01 fof(f308,plain,(
% 27.53/9.01 ~group_member(a,g1)|~group_member(c,g1)|product(g1,a,c,c)|~sQ15_spl),
% 27.53/9.01 inference(paramodulation,[status(thm)],[f302,f52])).
% 27.53/9.01 fof(f309,definition,(
% 27.53/9.01 sQ17_spl <=> (product(g1,a,c,c))),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f312,plain,(
% 27.53/9.01 ~sQ8_spl|~sQ16_spl|sQ17_spl|~sQ15_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f308,f255,f304,f309,f301])).
% 27.53/9.01 fof(f313,plain,(
% 27.53/9.01 $false|sQ16_spl),
% 27.53/9.01 inference(forward_subsumption_resolution,[status(thm)],[f306,f62])).
% 27.53/9.01 fof(f314,plain,(
% 27.53/9.01 sQ16_spl),
% 27.53/9.01 inference(contradiction_clause,[status(thm)],[f313])).
% 27.53/9.01 fof(f347,plain,(
% 27.53/9.01 ![X0]: (~product(g1,c,b,X0)|a=X0)),
% 27.53/9.01 inference(resolution,[status(thm)],[f75,f55])).
% 27.53/9.01 fof(f354,plain,(
% 27.53/9.01 ![X0]: (~product(g1,c,c,X0)|b=X0)),
% 27.53/9.01 inference(resolution,[status(thm)],[f76,f55])).
% 27.53/9.01 fof(f408,plain,(
% 27.53/9.01 ![X0]: (~product(g2,g,g,X0)|h=X0)),
% 27.53/9.01 inference(resolution,[status(thm)],[f82,f55])).
% 27.53/9.01 fof(f415,plain,(
% 27.53/9.01 ![X0]: (~product(g2,g,h,X0)|f=X0)),
% 27.53/9.01 inference(resolution,[status(thm)],[f83,f55])).
% 27.53/9.01 fof(f422,plain,(
% 27.53/9.01 ![X0]: (~product(g2,h,g,X0)|f=X0)),
% 27.53/9.01 inference(resolution,[status(thm)],[f84,f55])).
% 27.53/9.01 fof(f429,plain,(
% 27.53/9.01 ![X0]: (~product(g2,h,h,X0)|g=X0)),
% 27.53/9.01 inference(resolution,[status(thm)],[f85,f55])).
% 27.53/9.01 fof(f431,plain,(
% 27.53/9.01 c=multiply(g1,c,a)|~group_member(c,g1)|~group_member(a,g1)),
% 27.53/9.01 inference(resolution,[status(thm)],[f176,f52])).
% 27.53/9.01 fof(f432,definition,(
% 27.53/9.01 sQ18_spl <=> (c=multiply(g1,c,a))),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f433,plain,(
% 27.53/9.01 c=multiply(g1,c,a)|~sQ18_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f432])).
% 27.53/9.01 fof(f435,plain,(
% 27.53/9.01 sQ18_spl|~sQ16_spl|~sQ8_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f431,f432,f304,f255])).
% 27.53/9.01 fof(f436,plain,(
% 27.53/9.01 ~group_member(c,g1)|~group_member(a,g1)|product(g1,c,a,c)|~sQ18_spl),
% 27.53/9.01 inference(paramodulation,[status(thm)],[f433,f52])).
% 27.53/9.01 fof(f437,definition,(
% 27.53/9.01 sQ19_spl <=> (product(g1,c,a,c))),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f440,plain,(
% 27.53/9.01 ~sQ16_spl|~sQ8_spl|sQ19_spl|~sQ18_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f436,f304,f255,f437,f432])).
% 27.53/9.01 fof(f446,plain,(
% 27.53/9.01 ~group_member(d1,g1)|~group_member(d2,g1)|group_member(d3,g1)|~sQ2_spl),
% 27.53/9.01 inference(paramodulation,[status(thm)],[f214,f53])).
% 27.53/9.01 fof(f452,plain,(
% 27.53/9.01 ~sQ0_spl|~sQ1_spl|sQ4_spl|~sQ2_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f446,f207,f210,f220,f213])).
% 27.53/9.01 fof(f457,plain,(
% 27.53/9.01 identity_for(g1)=a|identity_for(g1)=b|identity_for(g1)=c),
% 27.53/9.01 inference(resolution,[status(thm)],[f66,f46])).
% 27.53/9.01 fof(f459,plain,(
% 27.53/9.01 d3=a|d3=b|d3=c),
% 27.53/9.01 inference(resolution,[status(thm)],[f66,f91])).
% 27.53/9.01 fof(f460,plain,(
% 27.53/9.01 d2=a|d2=b|d2=c),
% 27.53/9.01 inference(resolution,[status(thm)],[f66,f90])).
% 27.53/9.01 fof(f461,plain,(
% 27.53/9.01 d1=a|d1=b|d1=c),
% 27.53/9.01 inference(resolution,[status(thm)],[f66,f89])).
% 27.53/9.01 fof(f462,definition,(
% 27.53/9.01 sQ20_spl <=> (c=a)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f463,plain,(
% 27.53/9.01 c=a|~sQ20_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f462])).
% 27.53/9.01 fof(f464,plain,(
% 27.53/9.01 ~c=a|sQ20_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f462])).
% 27.53/9.01 fof(f465,definition,(
% 27.53/9.01 sQ21_spl <=> (c=b)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f466,plain,(
% 27.53/9.01 c=b|~sQ21_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f465])).
% 27.53/9.01 fof(f483,definition,(
% 27.53/9.01 sQ26_spl <=> (identity_for(g1)=a)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f484,plain,(
% 27.53/9.01 identity_for(g1)=a|~sQ26_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f483])).
% 27.53/9.01 fof(f486,definition,(
% 27.53/9.01 sQ27_spl <=> (identity_for(g1)=b)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f487,plain,(
% 27.53/9.01 identity_for(g1)=b|~sQ27_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f486])).
% 27.53/9.01 fof(f489,definition,(
% 27.53/9.01 sQ28_spl <=> (identity_for(g1)=c)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f490,plain,(
% 27.53/9.01 identity_for(g1)=c|~sQ28_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f489])).
% 27.53/9.01 fof(f492,plain,(
% 27.53/9.01 sQ26_spl|sQ27_spl|sQ28_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f457,f483,f486,f489])).
% 27.53/9.01 fof(f493,definition,(
% 27.53/9.01 sQ29_spl <=> (d3=a)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f494,plain,(
% 27.53/9.01 d3=a|~sQ29_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f493])).
% 27.53/9.01 fof(f495,plain,(
% 27.53/9.01 ~d3=a|sQ29_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f493])).
% 27.53/9.01 fof(f496,definition,(
% 27.53/9.01 sQ30_spl <=> (d3=b)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f497,plain,(
% 27.53/9.01 d3=b|~sQ30_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f496])).
% 27.53/9.01 fof(f498,plain,(
% 27.53/9.01 ~d3=b|sQ30_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f496])).
% 27.53/9.01 fof(f499,definition,(
% 27.53/9.01 sQ31_spl <=> (d3=c)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f500,plain,(
% 27.53/9.01 d3=c|~sQ31_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f499])).
% 27.53/9.01 fof(f501,plain,(
% 27.53/9.01 ~d3=c|sQ31_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f499])).
% 27.53/9.01 fof(f502,plain,(
% 27.53/9.01 sQ29_spl|sQ30_spl|sQ31_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f459,f493,f496,f499])).
% 27.53/9.01 fof(f503,definition,(
% 27.53/9.01 sQ32_spl <=> (d2=a)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f504,plain,(
% 27.53/9.01 d2=a|~sQ32_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f503])).
% 27.53/9.01 fof(f505,plain,(
% 27.53/9.01 ~d2=a|sQ32_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f503])).
% 27.53/9.01 fof(f506,definition,(
% 27.53/9.01 sQ33_spl <=> (d2=b)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f507,plain,(
% 27.53/9.01 d2=b|~sQ33_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f506])).
% 27.53/9.01 fof(f509,definition,(
% 27.53/9.01 sQ34_spl <=> (d2=c)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f510,plain,(
% 27.53/9.01 d2=c|~sQ34_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f509])).
% 27.53/9.01 fof(f511,plain,(
% 27.53/9.01 ~d2=c|sQ34_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f509])).
% 27.53/9.01 fof(f512,plain,(
% 27.53/9.01 sQ32_spl|sQ33_spl|sQ34_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f460,f503,f506,f509])).
% 27.53/9.01 fof(f513,definition,(
% 27.53/9.01 sQ35_spl <=> (d1=a)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f514,plain,(
% 27.53/9.01 d1=a|~sQ35_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f513])).
% 27.53/9.01 fof(f515,plain,(
% 27.53/9.01 ~d1=a|sQ35_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f513])).
% 27.53/9.01 fof(f516,definition,(
% 27.53/9.01 sQ36_spl <=> (d1=b)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f517,plain,(
% 27.53/9.01 d1=b|~sQ36_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f516])).
% 27.53/9.01 fof(f519,definition,(
% 27.53/9.01 sQ37_spl <=> (d1=c)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f520,plain,(
% 27.53/9.01 d1=c|~sQ37_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f519])).
% 27.53/9.01 fof(f521,plain,(
% 27.53/9.01 ~d1=c|sQ37_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f519])).
% 27.53/9.01 fof(f522,plain,(
% 27.53/9.01 sQ35_spl|sQ36_spl|sQ37_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f461,f513,f516,f519])).
% 27.53/9.01 fof(f525,plain,(
% 27.53/9.01 g=f|g=g|g=h),
% 27.53/9.01 inference(resolution,[status(thm)],[f67,f64])).
% 27.53/9.01 fof(f526,plain,(
% 27.53/9.01 f=f|f=g|f=h),
% 27.53/9.01 inference(resolution,[status(thm)],[f67,f63])).
% 27.53/9.01 fof(f527,plain,(
% 27.53/9.01 identity_for(g2)=f|identity_for(g2)=g|identity_for(g2)=h),
% 27.53/9.01 inference(resolution,[status(thm)],[f67,f46])).
% 27.53/9.01 fof(f529,definition,(
% 27.53/9.01 sQ38_spl <=> (h=f)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f532,definition,(
% 27.53/9.01 sQ39_spl <=> (h=g)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f539,definition,(
% 27.53/9.01 sQ41_spl <=> (g=f)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f540,plain,(
% 27.53/9.01 g=f|~sQ41_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f539])).
% 27.53/9.01 fof(f542,definition,(
% 27.53/9.01 sQ42_spl <=> (g=g)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f545,plain,(
% 27.53/9.01 sQ41_spl|sQ42_spl|sQ39_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f525,f539,f542,f532])).
% 27.53/9.01 fof(f546,definition,(
% 27.53/9.01 sQ43_spl <=> (f=f)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f549,plain,(
% 27.53/9.01 sQ43_spl|sQ41_spl|sQ38_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f526,f546,f539,f529])).
% 27.53/9.01 fof(f550,definition,(
% 27.53/9.01 sQ44_spl <=> (identity_for(g2)=f)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f551,plain,(
% 27.53/9.01 identity_for(g2)=f|~sQ44_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f550])).
% 27.53/9.01 fof(f552,plain,(
% 27.53/9.01 ~identity_for(g2)=f|sQ44_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f550])).
% 27.53/9.01 fof(f553,definition,(
% 27.53/9.01 sQ45_spl <=> (identity_for(g2)=g)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f554,plain,(
% 27.53/9.01 identity_for(g2)=g|~sQ45_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f553])).
% 27.53/9.01 fof(f555,plain,(
% 27.53/9.01 ~identity_for(g2)=g|sQ45_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f553])).
% 27.53/9.01 fof(f556,definition,(
% 27.53/9.01 sQ46_spl <=> (identity_for(g2)=h)),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f557,plain,(
% 27.53/9.01 identity_for(g2)=h|~sQ46_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f556])).
% 27.53/9.01 fof(f559,plain,(
% 27.53/9.01 sQ44_spl|sQ45_spl|sQ46_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f527,f550,f553,f556])).
% 27.53/9.01 fof(f560,plain,(
% 27.53/9.01 ![X0]: (~group_member(X0,g1)|X0=a|X0=b|X0=d1|~sQ37_spl)),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f520,f66])).
% 27.53/9.01 fof(f587,plain,(
% 27.53/9.01 an_isomorphism(d1)=g|~sQ36_spl),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f517,f87])).
% 27.53/9.01 fof(f598,plain,(
% 27.53/9.01 an_isomorphism(d1)=f|~sQ35_spl),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f514,f86])).
% 27.53/9.01 fof(f613,plain,(
% 27.53/9.01 ~product(g2,an_isomorphism(d1),an_isomorphism(d1),an_isomorphism(d3))|~sQ37_spl|~sQ34_spl),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f614,f93])).
% 27.53/9.01 fof(f614,plain,(
% 27.53/9.01 d2=d1|~sQ37_spl|~sQ34_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f520,f510])).
% 27.53/9.01 fof(f623,plain,(
% 27.53/9.01 d1=b|~sQ37_spl|~sQ34_spl|~sQ33_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f614,f507])).
% 27.53/9.01 fof(f625,plain,(
% 27.53/9.01 ~product(g2,an_isomorphism(d1),an_isomorphism(d1),an_isomorphism(d1))|~sQ31_spl|~sQ37_spl|~sQ34_spl),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f628,f613])).
% 27.53/9.01 fof(f628,plain,(
% 27.53/9.01 d3=d1|~sQ37_spl|~sQ31_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f520,f500])).
% 27.53/9.01 fof(f632,plain,(
% 27.53/9.01 f=g|~sQ35_spl|~sQ36_spl),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f598,f587])).
% 27.53/9.01 fof(f650,plain,(
% 27.53/9.01 d1=b|~sQ37_spl|~sQ21_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f520,f466])).
% 27.53/9.01 fof(f670,plain,(
% 27.53/9.01 identity_for(g1)=d1|~sQ37_spl|~sQ28_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f520,f490])).
% 27.53/9.01 fof(f730,definition,(
% 27.53/9.01 sQ47_spl <=> (group_member(f,g2))),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f732,plain,(
% 27.53/9.01 ~group_member(f,g2)|sQ47_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f730])).
% 27.53/9.01 fof(f757,plain,(
% 27.53/9.01 d1=b|~sQ37_spl|~sQ28_spl|~sQ27_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f670,f487])).
% 27.53/9.01 fof(f760,plain,(
% 27.53/9.01 an_isomorphism(d1)=f|~sQ41_spl|~sQ36_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f540,f587])).
% 27.53/9.01 fof(f778,definition,(
% 27.53/9.01 sQ48_spl <=> (product(g1,d1,d1,d1))),
% 27.53/9.01 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 27.53/9.01 fof(f779,plain,(
% 27.53/9.01 product(g1,d1,d1,d1)|~sQ48_spl),
% 27.53/9.01 inference(component_clause,[status(thm)],[f778])).
% 27.53/9.01 fof(f783,plain,(
% 27.53/9.01 c=d1|~sQ36_spl|~sQ21_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f517,f466])).
% 27.53/9.01 fof(f787,plain,(
% 27.53/9.01 ![X0]: (~group_member(X0,g1)|X0=a|X0=d1|X0=c|~sQ36_spl)),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f517,f66])).
% 27.53/9.01 fof(f790,plain,(
% 27.53/9.01 product(g1,d1,c,a)|~sQ36_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f517,f74])).
% 27.53/9.01 fof(f791,plain,(
% 27.53/9.01 product(g1,d1,b,c)|~sQ36_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f517,f73])).
% 27.53/9.01 fof(f792,plain,(
% 27.53/9.01 product(g1,d1,d1,c)|~sQ36_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f517,f791])).
% 27.53/9.01 fof(f819,plain,(
% 27.53/9.01 ~d1=d1|~sQ36_spl|~sQ21_spl|sQ37_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f783,f521])).
% 27.53/9.01 fof(f820,plain,(
% 27.53/9.01 $false|~sQ36_spl|~sQ21_spl|sQ37_spl),
% 27.53/9.01 inference(trivial_equality_resolution,[status(thm)],[f819])).
% 27.53/9.01 fof(f821,plain,(
% 27.53/9.01 ~sQ36_spl|~sQ21_spl|sQ37_spl),
% 27.53/9.01 inference(contradiction_clause,[status(thm)],[f820])).
% 27.53/9.01 fof(f829,plain,(
% 27.53/9.01 sQ36_spl|~sQ37_spl|~sQ28_spl|~sQ27_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f757,f516,f519,f489,f486])).
% 27.53/9.01 fof(f830,plain,(
% 27.53/9.01 sQ36_spl|~sQ37_spl|~sQ21_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f650,f516,f519,f465])).
% 27.53/9.01 fof(f831,plain,(
% 27.53/9.01 sQ36_spl|~sQ37_spl|~sQ34_spl|~sQ33_spl),
% 27.53/9.01 inference(split_clause,[status(thm)],[f623,f516,f519,f509,f506])).
% 27.53/9.01 fof(f834,plain,(
% 27.53/9.01 d3=d2|~sQ32_spl|~sQ29_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f504,f494])).
% 27.53/9.01 fof(f860,plain,(
% 27.53/9.01 ![X0]: (~product(g1,d1,d1,X0)|d1=X0|~sQ48_spl)),
% 27.53/9.01 inference(resolution,[status(thm)],[f779,f55])).
% 27.53/9.01 fof(f877,plain,(
% 27.53/9.01 ~product(g2,f,an_isomorphism(d2),an_isomorphism(d3))|~sQ41_spl|~sQ36_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f760,f93])).
% 27.53/9.01 fof(f887,plain,(
% 27.53/9.01 d3=d1|~sQ36_spl|~sQ30_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f517,f497])).
% 27.53/9.01 fof(f896,plain,(
% 27.53/9.01 ![X0]: (~product(g1,d1,d2,X0)|d3=X0)),
% 27.53/9.01 inference(resolution,[status(thm)],[f92,f55])).
% 27.53/9.01 fof(f898,plain,(
% 27.53/9.01 ~product(g2,f,an_isomorphism(d2),an_isomorphism(d1))|~sQ30_spl|~sQ41_spl|~sQ36_spl),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f887,f877])).
% 27.53/9.01 fof(f899,plain,(
% 27.53/9.01 ~product(g2,f,an_isomorphism(d2),f)|~sQ30_spl|~sQ41_spl|~sQ36_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f760,f898])).
% 27.53/9.01 fof(f909,plain,(
% 27.53/9.01 an_isomorphism(d2)=h|~sQ34_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f510,f88])).
% 27.53/9.01 fof(f970,plain,(
% 27.53/9.01 ~product(g2,f,f,f)|~sQ32_spl|~sQ30_spl|~sQ41_spl|~sQ36_spl),
% 27.53/9.01 inference(backward_demodulation,[status(thm)],[f971,f899])).
% 27.53/9.01 fof(f971,plain,(
% 27.53/9.01 an_isomorphism(d2)=f|~sQ32_spl),
% 27.53/9.01 inference(forward_demodulation,[status(thm)],[f504,f86])).
% 27.53/9.01 fof(f972,plain,(
% 27.53/9.01 $false|~sQ32_spl|~sQ30_spl|~sQ41_spl|~sQ36_spl),
% 27.53/9.01 inference(forward_subsumption_resolution,[status(thm)],[f970,f77])).
% 27.53/9.01 fof(f973,plain,(
% 27.53/9.01 ~sQ32_spl|~sQ30_spl|~sQ41_spl|~sQ36_spl),
% 27.53/9.01 inference(contradiction_clause,[status(thm)],[f972])).
% 27.53/9.01 fof(f985,plain,(
% 27.53/9.01 ![X0]: (~product(g1,d1,d2,X0)|d3=X0)),
% 27.53/9.02 inference(resolution,[status(thm)],[f92,f55])).
% 27.53/9.02 fof(f986,plain,(
% 27.53/9.02 ~d2=d1|~sQ35_spl|sQ32_spl),
% 27.53/9.02 inference(forward_demodulation,[status(thm)],[f514,f505])).
% 27.53/9.02 fof(f1069,plain,(
% 27.53/9.02 d1=multiply(g1,a,a)|~sQ35_spl|~sQ7_spl),
% 27.53/9.02 inference(forward_demodulation,[status(thm)],[f514,f253])).
% 27.53/9.02 fof(f1070,plain,(
% 27.53/9.02 d1=multiply(g1,d1,a)|~sQ35_spl|~sQ7_spl),
% 27.53/9.02 inference(forward_demodulation,[status(thm)],[f514,f1069])).
% 27.53/9.02 fof(f1071,plain,(
% 27.53/9.02 d1=multiply(g1,d1,d1)|~sQ35_spl|~sQ7_spl),
% 27.53/9.02 inference(forward_demodulation,[status(thm)],[f514,f1070])).
% 27.53/9.02 fof(f1073,plain,(
% 27.53/9.02 ~group_member(d1,g1)|~group_member(d1,g1)|product(g1,d1,d1,d1)|~sQ35_spl|~sQ7_spl),
% 27.53/9.02 inference(paramodulation,[status(thm)],[f1071,f52])).
% 27.53/9.02 fof(f1075,plain,(
% 27.53/9.02 ~sQ0_spl|sQ48_spl|~sQ35_spl|~sQ7_spl),
% 27.53/9.02 inference(split_clause,[status(thm)],[f1073,f207,f778,f513,f252])).
% 27.53/9.02 fof(f1085,plain,(
% 27.53/9.02 ~product(g2,f,an_isomorphism(d2),an_isomorphism(d3))|~sQ35_spl),
% 27.53/9.02 inference(forward_demodulation,[status(thm)],[f598,f93])).
% 27.53/9.02 fof(f1086,plain,(
% 27.53/9.02 d2=d1|~sQ35_spl|~sQ32_spl),
% 27.53/9.02 inference(forward_demodulation,[status(thm)],[f514,f504])).
% 27.53/9.03 fof(f1089,plain,(
% 27.53/9.03 ~product(g2,f,f,an_isomorphism(d3))|~sQ32_spl|~sQ35_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f971,f1085])).
% 27.53/9.03 fof(f1111,plain,(
% 27.53/9.03 ~product(g2,f,f,an_isomorphism(d1))|~sQ29_spl|~sQ32_spl|~sQ35_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f1113,f1089])).
% 27.53/9.03 fof(f1113,plain,(
% 27.53/9.03 d3=d1|~sQ35_spl|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1086,f834])).
% 27.53/9.03 fof(f1114,plain,(
% 27.53/9.03 ~product(g2,f,f,f)|~sQ29_spl|~sQ32_spl|~sQ35_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f598,f1111])).
% 27.53/9.03 fof(f1122,plain,(
% 27.53/9.03 ![X0,X1]: (~product(g2,X0,f,X1)|X0=X1|~sQ44_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f551,f129])).
% 27.53/9.03 fof(f1124,plain,(
% 27.53/9.03 ![X0,X1]: (~product(g2,f,X0,X1)|X0=X1|~sQ44_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f551,f117])).
% 27.53/9.03 fof(f1127,plain,(
% 27.53/9.03 ![X0]: (product(g2,X0,f,X0)|~sQ44_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f551,f48])).
% 27.53/9.03 fof(f1128,plain,(
% 27.53/9.03 ![X0]: (product(g2,f,X0,X0)|~sQ44_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f551,f47])).
% 27.53/9.03 fof(f1166,plain,(
% 27.53/9.03 c=multiply(g1,c,d1)|~sQ35_spl|~sQ18_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f514,f433])).
% 27.53/9.03 fof(f1168,plain,(
% 27.53/9.03 ~group_member(c,g1)|~group_member(d1,g1)|product(g1,c,d1,c)|~sQ35_spl|~sQ18_spl),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f1166,f52])).
% 27.53/9.03 fof(f1170,definition,(
% 27.53/9.03 sQ49_spl <=> (product(g1,c,d1,c))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f1171,plain,(
% 27.53/9.03 product(g1,c,d1,c)|~sQ49_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f1170])).
% 27.53/9.03 fof(f1173,plain,(
% 27.53/9.03 ~sQ16_spl|~sQ0_spl|sQ49_spl|~sQ35_spl|~sQ18_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f1168,f304,f207,f1170,f513,f432])).
% 27.53/9.03 fof(f1191,plain,(
% 27.53/9.03 an_isomorphism(d1)=g|~sQ36_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f517,f87])).
% 27.53/9.03 fof(f1313,plain,(
% 27.53/9.03 d1=multiply(g1,a,c)|~sQ37_spl|~sQ15_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f302])).
% 27.53/9.03 fof(f1319,definition,(
% 27.53/9.03 sQ50_spl <=> (product(g1,d2,d1,d1))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f1320,plain,(
% 27.53/9.03 product(g1,d2,d1,d1)|~sQ50_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f1319])).
% 27.53/9.03 fof(f1323,plain,(
% 27.53/9.03 d1=multiply(g1,a,d1)|~sQ37_spl|~sQ15_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f1313])).
% 27.53/9.03 fof(f1330,plain,(
% 27.53/9.03 ![X0]: (~group_member(X0,g1)|X0=a|X0=d1|X0=d1|~sQ36_spl|~sQ37_spl)),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f560])).
% 27.53/9.03 fof(f1331,plain,(
% 27.53/9.03 ![X0]: (~group_member(X0,g1)|X0=a|X0=d1|~sQ36_spl|~sQ37_spl)),
% 27.53/9.03 inference(duplicate_literals_removal,[status(thm)],[f1330])).
% 27.53/9.03 fof(f1332,plain,(
% 27.53/9.03 d2=a|d2=d1|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(resolution,[status(thm)],[f1331,f90])).
% 27.53/9.03 fof(f1337,definition,(
% 27.53/9.03 sQ51_spl <=> (d2=d1)),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f1338,plain,(
% 27.53/9.03 d2=d1|~sQ51_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f1337])).
% 27.53/9.03 fof(f1340,plain,(
% 27.53/9.03 sQ32_spl|sQ51_spl|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f1332,f503,f1337,f516,f519])).
% 27.53/9.03 fof(f1341,definition,(
% 27.53/9.03 sQ52_spl <=> (identity_for(g1)=d1)),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f1342,plain,(
% 27.53/9.03 identity_for(g1)=d1|~sQ52_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f1341])).
% 27.53/9.03 fof(f1343,plain,(
% 27.53/9.03 ~identity_for(g1)=d1|sQ52_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f1341])).
% 27.53/9.03 fof(f1345,definition,(
% 27.53/9.03 sQ53_spl <=> (d1=d1)),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f1485,plain,(
% 27.53/9.03 ~d1=d3|~sQ29_spl|sQ35_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f494,f515])).
% 27.53/9.03 fof(f1489,plain,(
% 27.53/9.03 d1=c|~sQ51_spl|~sQ34_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f1338,f510])).
% 27.53/9.03 fof(f1494,plain,(
% 27.53/9.03 sQ37_spl|~sQ51_spl|~sQ34_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f1489,f519,f1337,f509])).
% 27.53/9.03 fof(f1537,plain,(
% 27.53/9.03 ~d1=d1|~sQ51_spl|~sQ35_spl|sQ32_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1338,f986])).
% 27.53/9.03 fof(f1538,plain,(
% 27.53/9.03 $false|~sQ51_spl|~sQ35_spl|sQ32_spl),
% 27.53/9.03 inference(trivial_equality_resolution,[status(thm)],[f1537])).
% 27.53/9.03 fof(f1539,plain,(
% 27.53/9.03 ~sQ51_spl|~sQ35_spl|sQ32_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f1538])).
% 27.53/9.03 fof(f1540,plain,(
% 27.53/9.03 sQ41_spl|~sQ35_spl|~sQ36_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f632,f539,f513,f516])).
% 27.53/9.03 fof(f1542,plain,(
% 27.53/9.03 $false|~sQ44_spl|~sQ29_spl|~sQ32_spl|~sQ35_spl),
% 27.53/9.03 inference(forward_subsumption_resolution,[status(thm)],[f1114,f1128])).
% 27.53/9.03 fof(f1543,plain,(
% 27.53/9.03 ~sQ44_spl|~sQ29_spl|~sQ32_spl|~sQ35_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f1542])).
% 27.53/9.03 fof(f1602,plain,(
% 27.53/9.03 ~product(g2,g,an_isomorphism(d2),an_isomorphism(d3))|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f93])).
% 27.53/9.03 fof(f1628,plain,(
% 27.53/9.03 ![X0,X1]: (~product(g1,X0,a,X1)|X0=X1|~sQ26_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f484,f129])).
% 27.53/9.03 fof(f1630,plain,(
% 27.53/9.03 ![X0,X1]: (~product(g1,a,X0,X1)|X0=X1|~sQ26_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f484,f117])).
% 27.53/9.03 fof(f1664,plain,(
% 27.53/9.03 an_isomorphism(d3)=f|~sQ29_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f494,f86])).
% 27.53/9.03 fof(f1714,plain,(
% 27.53/9.03 ![X0,X1]: (~product(g1,X0,d1,X1)|X0=X1|~sQ52_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f1342,f129])).
% 27.53/9.03 fof(f1751,plain,(
% 27.53/9.03 an_isomorphism(d1)=h|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f88])).
% 27.53/9.03 fof(f1752,plain,(
% 27.53/9.03 g=h|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f1751])).
% 27.53/9.03 fof(f1761,plain,(
% 27.53/9.03 ![X0,X1]: (~product(g2,X0,g,X1)|X0=X1|~sQ45_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f554,f129])).
% 27.53/9.03 fof(f1767,plain,(
% 27.53/9.03 ![X0]: (product(g2,g,X0,X0)|~sQ45_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f554,f47])).
% 27.53/9.03 fof(f1777,definition,(
% 27.53/9.03 sQ56_spl <=> (group_member(g,g2))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f1779,plain,(
% 27.53/9.03 ~group_member(g,g2)|sQ56_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f1777])).
% 27.53/9.03 fof(f1821,plain,(
% 27.53/9.03 d1=a|~sQ52_spl|~sQ26_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1342,f484])).
% 27.53/9.03 fof(f1888,plain,(
% 27.53/9.03 ~d2=d1|~sQ37_spl|sQ34_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f511])).
% 27.53/9.03 fof(f1956,plain,(
% 27.53/9.03 ~d1=d1|~sQ51_spl|~sQ37_spl|sQ34_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1338,f1888])).
% 27.53/9.03 fof(f1957,plain,(
% 27.53/9.03 $false|~sQ51_spl|~sQ37_spl|sQ34_spl),
% 27.53/9.03 inference(trivial_equality_resolution,[status(thm)],[f1956])).
% 27.53/9.03 fof(f1958,plain,(
% 27.53/9.03 ~sQ51_spl|~sQ37_spl|sQ34_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f1957])).
% 27.53/9.03 fof(f2011,plain,(
% 27.53/9.03 sQ35_spl|~sQ52_spl|~sQ26_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f1821,f513,f1341,f483])).
% 27.53/9.03 fof(f2013,plain,(
% 27.53/9.03 identity_for(g1)=d1|~sQ36_spl|~sQ27_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f487])).
% 27.53/9.03 fof(f2016,plain,(
% 27.53/9.03 d3=d2|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f504,f494])).
% 27.53/9.03 fof(f2040,plain,(
% 27.53/9.03 ~product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d2))|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f2016,f93])).
% 27.53/9.03 fof(f2041,plain,(
% 27.53/9.03 ~product(g2,an_isomorphism(d1),an_isomorphism(d2),f)|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f971,f2040])).
% 27.53/9.03 fof(f2043,plain,(
% 27.53/9.03 ~product(g2,an_isomorphism(d1),f,f)|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f971,f2041])).
% 27.53/9.03 fof(f2233,plain,(
% 27.53/9.03 b=multiply(g1,b,d2)|~sQ32_spl|~sQ13_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f504,f291])).
% 27.53/9.03 fof(f2235,plain,(
% 27.53/9.03 ~group_member(b,g1)|~group_member(d2,g1)|product(g1,b,d2,b)|~sQ32_spl|~sQ13_spl),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f2233,f52])).
% 27.53/9.03 fof(f2237,definition,(
% 27.53/9.03 sQ57_spl <=> (product(g1,b,d2,b))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f2238,plain,(
% 27.53/9.03 product(g1,b,d2,b)|~sQ57_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f2237])).
% 27.53/9.03 fof(f2240,plain,(
% 27.53/9.03 ~sQ11_spl|~sQ1_spl|sQ57_spl|~sQ32_spl|~sQ13_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f2235,f275,f210,f2237,f503,f290])).
% 27.53/9.03 fof(f2267,plain,(
% 27.53/9.03 ~product(g2,h,an_isomorphism(d2),an_isomorphism(d3))|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1751,f93])).
% 27.53/9.03 fof(f2269,plain,(
% 27.53/9.03 ~product(g2,h,an_isomorphism(d1),an_isomorphism(d3))|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1751,f613])).
% 27.53/9.03 fof(f2270,plain,(
% 27.53/9.03 ~product(g2,h,h,an_isomorphism(d3))|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1751,f2269])).
% 27.53/9.03 fof(f2273,plain,(
% 27.53/9.03 ~product(g2,g,an_isomorphism(d2),an_isomorphism(d1))|~sQ30_spl|~sQ36_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f2274,f1602])).
% 27.53/9.03 fof(f2274,plain,(
% 27.53/9.03 d3=d1|~sQ36_spl|~sQ30_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f497])).
% 27.53/9.03 fof(f2355,plain,(
% 27.53/9.03 ![X0]: (~group_member(X0,g2)|X0=f|X0=g|X0=g|~sQ36_spl|~sQ37_spl)),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f1752,f67])).
% 27.53/9.03 fof(f2358,plain,(
% 27.53/9.03 ![X0]: (~group_member(X0,g2)|X0=f|X0=g|~sQ36_spl|~sQ37_spl)),
% 27.53/9.03 inference(duplicate_literals_removal,[status(thm)],[f2355])).
% 27.53/9.03 fof(f2360,plain,(
% 27.53/9.03 product(g2,g,g,g)|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1752,f82])).
% 27.53/9.03 fof(f2380,plain,(
% 27.53/9.03 ~product(g2,g,an_isomorphism(d1),an_isomorphism(d1))|~sQ36_spl|~sQ31_spl|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f625])).
% 27.53/9.03 fof(f2381,plain,(
% 27.53/9.03 ~product(g2,g,g,an_isomorphism(d1))|~sQ36_spl|~sQ31_spl|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f2380])).
% 27.53/9.03 fof(f2382,plain,(
% 27.53/9.03 ~product(g2,g,g,g)|~sQ36_spl|~sQ31_spl|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f2381])).
% 27.53/9.03 fof(f2383,plain,(
% 27.53/9.03 $false|~sQ36_spl|~sQ31_spl|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(forward_subsumption_resolution,[status(thm)],[f2382,f2360])).
% 27.53/9.03 fof(f2384,plain,(
% 27.53/9.03 ~sQ36_spl|~sQ31_spl|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f2383])).
% 27.53/9.03 fof(f2513,plain,(
% 27.53/9.03 ![X0]: (~group_member(X0,g1)|X0=d3|X0=b|X0=c|~sQ29_spl)),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f494,f66])).
% 27.53/9.03 fof(f2523,definition,(
% 27.53/9.03 sQ59_spl <=> (d3=d1)),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f2524,plain,(
% 27.53/9.03 d3=d1|~sQ59_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f2523])).
% 27.53/9.03 fof(f2527,definition,(
% 27.53/9.03 sQ60_spl <=> (identity_for(g1)=d3)),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f2528,plain,(
% 27.53/9.03 identity_for(g1)=d3|~sQ60_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f2527])).
% 27.53/9.03 fof(f2532,plain,(
% 27.53/9.03 ![X0]: (~group_member(X0,g1)|X0=a|X0=b|X0=d1|~sQ37_spl)),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f66])).
% 27.53/9.03 fof(f2547,plain,(
% 27.53/9.03 d1=b|~sQ59_spl|~sQ30_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f2524,f497])).
% 27.53/9.03 fof(f2551,plain,(
% 27.53/9.03 sQ36_spl|~sQ59_spl|~sQ30_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f2547,f516,f2523,f496])).
% 27.53/9.03 fof(f2690,plain,(
% 27.53/9.03 ~f=g|~sQ44_spl|sQ45_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f551,f555])).
% 27.53/9.03 fof(f2725,plain,(
% 27.53/9.03 ~d3=d1|~sQ60_spl|sQ52_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f2528,f1343])).
% 27.53/9.03 fof(f2777,plain,(
% 27.53/9.03 d1=multiply(g1,c,a)|~sQ37_spl|~sQ18_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f433])).
% 27.53/9.03 fof(f2778,plain,(
% 27.53/9.03 d1=multiply(g1,d1,a)|~sQ37_spl|~sQ18_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f2777])).
% 27.53/9.03 fof(f2791,definition,(
% 27.53/9.03 sQ63_spl <=> (product(g1,d1,d1,d3))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f2792,plain,(
% 27.53/9.03 product(g1,d1,d1,d3)|~sQ63_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f2791])).
% 27.53/9.03 fof(f2839,plain,(
% 27.53/9.03 an_isomorphism(d3)=g|~sQ30_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f497,f87])).
% 27.53/9.03 fof(f2853,plain,(
% 27.53/9.03 ~product(g2,h,h,g)|~sQ30_spl|~sQ37_spl|~sQ34_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f2839,f2270])).
% 27.53/9.03 fof(f2988,plain,(
% 27.53/9.03 ![X0]: (X0=multiply(g1,a,X0)|~group_member(a,g1)|~group_member(X0,g1)|~sQ26_spl)),
% 27.53/9.03 inference(resolution,[status(thm)],[f1630,f52])).
% 27.53/9.03 fof(f2990,definition,(
% 27.53/9.03 ![X0]: (sQ67_spl <=> (X0=multiply(g1,a,X0)|~group_member(X0,g1)))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f2993,plain,(
% 27.53/9.03 sQ67_spl|~sQ8_spl|~sQ26_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f2988,f2990,f255,f483])).
% 27.53/9.03 fof(f3017,plain,(
% 27.53/9.03 ![X0]: (X0=multiply(g2,X0,f)|~group_member(X0,g2)|~group_member(f,g2)|~sQ44_spl)),
% 27.53/9.03 inference(resolution,[status(thm)],[f1122,f52])).
% 27.53/9.03 fof(f3019,definition,(
% 27.53/9.03 ![X0]: (sQ69_spl <=> (X0=multiply(g2,X0,f)|~group_member(X0,g2)))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f3022,plain,(
% 27.53/9.03 sQ69_spl|~sQ47_spl|~sQ44_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f3017,f3019,f730,f550])).
% 27.53/9.03 fof(f3023,plain,(
% 27.53/9.03 $false|sQ47_spl),
% 27.53/9.03 inference(forward_subsumption_resolution,[status(thm)],[f732,f63])).
% 27.53/9.03 fof(f3024,plain,(
% 27.53/9.03 sQ47_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f3023])).
% 27.53/9.03 fof(f3036,plain,(
% 27.53/9.03 ![X0]: (X0=multiply(g1,X0,a)|~group_member(X0,g1)|~group_member(a,g1)|~sQ26_spl)),
% 27.53/9.03 inference(resolution,[status(thm)],[f1628,f52])).
% 27.53/9.03 fof(f3038,definition,(
% 27.53/9.03 ![X0]: (sQ70_spl <=> (X0=multiply(g1,X0,a)|~group_member(X0,g1)))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f3041,plain,(
% 27.53/9.03 sQ70_spl|~sQ8_spl|~sQ26_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f3036,f3038,f255,f483])).
% 27.53/9.03 fof(f3043,plain,(
% 27.53/9.03 ~group_member(a,g1)|~group_member(d1,g1)|product(g1,a,d1,d1)|~sQ37_spl|~sQ15_spl),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f1323,f52])).
% 27.53/9.03 fof(f3045,definition,(
% 27.53/9.03 sQ71_spl <=> (product(g1,a,d1,d1))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f3048,plain,(
% 27.53/9.03 ~sQ8_spl|~sQ0_spl|sQ71_spl|~sQ37_spl|~sQ15_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f3043,f255,f207,f3045,f519,f301])).
% 27.53/9.03 fof(f3053,plain,(
% 27.53/9.03 d1=d3|d1=b|d1=c|~sQ29_spl),
% 27.53/9.03 inference(resolution,[status(thm)],[f2513,f89])).
% 27.53/9.03 fof(f3056,plain,(
% 27.53/9.03 sQ59_spl|sQ36_spl|sQ37_spl|~sQ29_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f3053,f2523,f516,f519,f493])).
% 27.53/9.03 fof(f3170,plain,(
% 27.53/9.03 ~product(g2,g,f,f)|~sQ36_spl|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f2043])).
% 27.53/9.03 fof(f3171,plain,(
% 27.53/9.03 $false|~sQ45_spl|~sQ36_spl|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(forward_subsumption_resolution,[status(thm)],[f3170,f1767])).
% 27.53/9.03 fof(f3172,plain,(
% 27.53/9.03 ~sQ45_spl|~sQ36_spl|~sQ32_spl|~sQ29_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f3171])).
% 27.53/9.03 fof(f3178,plain,(
% 27.53/9.03 ~product(g2,g,an_isomorphism(d2),an_isomorphism(d3))|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f93])).
% 27.53/9.03 fof(f3195,definition,(
% 27.53/9.03 sQ72_spl <=> (d3=d2)),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f3196,plain,(
% 27.53/9.03 d3=d2|~sQ72_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f3195])).
% 27.53/9.03 fof(f3202,plain,(
% 27.53/9.03 f=identity_for(g2)|~sQ44_spl),
% 27.53/9.03 inference(resolution,[status(thm)],[f1127,f117])).
% 27.53/9.03 fof(f3257,plain,(
% 27.53/9.03 ![X0,X1]: (~product(g1,X0,d1,X1)|X0=X1|~sQ36_spl|~sQ27_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f2013,f129])).
% 27.53/9.03 fof(f3303,definition,(
% 27.53/9.03 sQ73_spl <=> (product(g1,d2,d2,d2))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f3304,plain,(
% 27.53/9.03 product(g1,d2,d2,d2)|~sQ73_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f3303])).
% 27.53/9.03 fof(f3345,plain,(
% 27.53/9.03 product(g1,a,d1,b)|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f69])).
% 27.53/9.03 fof(f3346,plain,(
% 27.53/9.03 product(g1,a,d1,d1)|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f3345])).
% 27.53/9.03 fof(f3347,plain,(
% 27.53/9.03 ~d3=d1|~sQ36_spl|sQ30_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f498])).
% 27.53/9.03 fof(f3382,plain,(
% 27.53/9.03 ~product(g2,g,h,an_isomorphism(d3))|~sQ34_spl|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f909,f3178])).
% 27.53/9.03 fof(f3383,plain,(
% 27.53/9.03 ~product(g2,g,h,f)|~sQ29_spl|~sQ34_spl|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1664,f3382])).
% 27.53/9.03 fof(f3384,plain,(
% 27.53/9.03 $false|~sQ29_spl|~sQ34_spl|~sQ36_spl),
% 27.53/9.03 inference(forward_subsumption_resolution,[status(thm)],[f3383,f83])).
% 27.53/9.03 fof(f3385,plain,(
% 27.53/9.03 ~sQ29_spl|~sQ34_spl|~sQ36_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f3384])).
% 27.53/9.03 fof(f3386,plain,(
% 27.53/9.03 d3=d1|~sQ36_spl|~sQ30_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f497])).
% 27.53/9.03 fof(f3701,plain,(
% 27.53/9.03 ~sQ59_spl|~sQ29_spl|sQ35_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f1485,f2523,f493,f513])).
% 27.53/9.03 fof(f3703,plain,(
% 27.53/9.03 d1=multiply(g1,b,d2)|~sQ36_spl|~sQ32_spl|~sQ13_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f2233])).
% 27.53/9.03 fof(f3704,plain,(
% 27.53/9.03 d1=multiply(g1,d1,d2)|~sQ36_spl|~sQ32_spl|~sQ13_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f517,f3703])).
% 27.53/9.03 fof(f3705,plain,(
% 27.53/9.03 ~sQ59_spl|~sQ36_spl|sQ30_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f3347,f2523,f516,f496])).
% 27.53/9.03 fof(f3708,plain,(
% 27.53/9.03 sQ59_spl|~sQ37_spl|~sQ31_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f628,f2523,f519,f499])).
% 27.53/9.03 fof(f3790,plain,(
% 27.53/9.03 ~product(g2,h,f,an_isomorphism(d3))|~sQ32_spl|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f971,f2267])).
% 27.53/9.03 fof(f3851,plain,(
% 27.53/9.03 an_isomorphism(d1)=h|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f88])).
% 27.53/9.03 fof(f3873,definition,(
% 27.53/9.03 sQ75_spl <=> (product(g1,d1,d2,d2))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f3874,plain,(
% 27.53/9.03 product(g1,d1,d2,d2)|~sQ75_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f3873])).
% 27.53/9.03 fof(f3877,plain,(
% 27.53/9.03 d1=multiply(g1,c,a)|~sQ37_spl|~sQ18_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f433])).
% 27.53/9.03 fof(f3878,plain,(
% 27.53/9.03 d1=multiply(g1,d1,a)|~sQ37_spl|~sQ18_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f3877])).
% 27.53/9.03 fof(f3880,plain,(
% 27.53/9.03 d1=multiply(g1,d1,d2)|~sQ32_spl|~sQ37_spl|~sQ18_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f504,f3878])).
% 27.53/9.03 fof(f3885,definition,(
% 27.53/9.03 sQ76_spl <=> (product(g1,d1,d2,d1))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f3886,plain,(
% 27.53/9.03 product(g1,d1,d2,d1)|~sQ76_spl),
% 27.53/9.03 inference(component_clause,[status(thm)],[f3885])).
% 27.53/9.03 fof(f3889,plain,(
% 27.53/9.03 d3=d1|~sQ32_spl|~sQ37_spl|~sQ18_spl|~sQ2_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f3880,f214])).
% 27.53/9.03 fof(f3893,plain,(
% 27.53/9.03 ~product(g2,g,f,an_isomorphism(d1))|~sQ32_spl|~sQ30_spl|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f971,f2273])).
% 27.53/9.03 fof(f3894,plain,(
% 27.53/9.03 ~product(g2,g,f,g)|~sQ32_spl|~sQ30_spl|~sQ36_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f1191,f3893])).
% 27.53/9.03 fof(f4062,plain,(
% 27.53/9.03 product(g1,d1,d1,c)|~sQ37_spl|~sQ49_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f1171])).
% 27.53/9.03 fof(f4063,plain,(
% 27.53/9.03 product(g1,d1,d1,d1)|~sQ37_spl|~sQ49_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f520,f4062])).
% 27.53/9.03 fof(f4078,plain,(
% 27.53/9.03 d2=d1|~sQ52_spl|~sQ50_spl),
% 27.53/9.03 inference(resolution,[status(thm)],[f1714,f1320])).
% 27.53/9.03 fof(f4084,plain,(
% 27.53/9.03 ![X0]: (X0=multiply(g1,X0,d1)|~group_member(X0,g1)|~group_member(d1,g1)|~sQ52_spl)),
% 27.53/9.03 inference(resolution,[status(thm)],[f1714,f52])).
% 27.53/9.03 fof(f4085,plain,(
% 27.53/9.03 sQ51_spl|~sQ52_spl|~sQ50_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f4078,f1337,f1341,f1319])).
% 27.53/9.03 fof(f4088,definition,(
% 27.53/9.03 ![X0]: (sQ77_spl <=> (X0=multiply(g1,X0,d1)|~group_member(X0,g1)))),
% 27.53/9.03 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 27.53/9.03 fof(f4091,plain,(
% 27.53/9.03 sQ77_spl|~sQ0_spl|~sQ52_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f4084,f4088,f207,f1341])).
% 27.53/9.03 fof(f4290,plain,(
% 27.53/9.03 g=f|g=g|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(resolution,[status(thm)],[f2358,f64])).
% 27.53/9.03 fof(f4292,plain,(
% 27.53/9.03 f=f|f=g|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(resolution,[status(thm)],[f2358,f63])).
% 27.53/9.03 fof(f4295,plain,(
% 27.53/9.03 sQ41_spl|sQ42_spl|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f4290,f539,f542,f516,f519])).
% 27.53/9.03 fof(f4296,plain,(
% 27.53/9.03 sQ43_spl|sQ41_spl|~sQ36_spl|~sQ37_spl),
% 27.53/9.03 inference(split_clause,[status(thm)],[f4292,f546,f539,f516,f519])).
% 27.53/9.03 fof(f4302,plain,(
% 27.53/9.03 $false|~sQ44_spl|~sQ32_spl|~sQ30_spl|~sQ36_spl),
% 27.53/9.03 inference(backward_subsumption_resolution,[status(thm)],[f3894,f1127])).
% 27.53/9.03 fof(f4316,plain,(
% 27.53/9.03 ~sQ44_spl|~sQ32_spl|~sQ30_spl|~sQ36_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f4302])).
% 27.53/9.03 fof(f4346,plain,(
% 27.53/9.03 ~g=f|~sQ45_spl|sQ44_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f554,f552])).
% 27.53/9.03 fof(f4392,plain,(
% 27.53/9.03 ~product(g2,h,f,an_isomorphism(d1))|~sQ18_spl|~sQ2_spl|~sQ32_spl|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f3889,f3790])).
% 27.53/9.03 fof(f4429,plain,(
% 27.53/9.03 d3=d2|~sQ33_spl|~sQ30_spl),
% 27.53/9.03 inference(backward_demodulation,[status(thm)],[f507,f497])).
% 27.53/9.03 fof(f4547,plain,(
% 27.53/9.03 ~product(g2,h,an_isomorphism(d2),an_isomorphism(d3))|~sQ37_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f3851,f93])).
% 27.53/9.03 fof(f4579,plain,(
% 27.53/9.03 an_isomorphism(d2)=g|~sQ33_spl),
% 27.53/9.03 inference(forward_demodulation,[status(thm)],[f507,f87])).
% 27.53/9.03 fof(f4630,plain,(
% 27.53/9.03 f=g|~sQ45_spl),
% 27.53/9.03 inference(resolution,[status(thm)],[f1761,f78])).
% 27.53/9.03 fof(f4636,plain,(
% 27.53/9.03 $false|sQ44_spl|~sQ45_spl),
% 27.53/9.03 inference(forward_subsumption_resolution,[status(thm)],[f4630,f4346])).
% 27.53/9.03 fof(f4637,plain,(
% 27.53/9.03 sQ44_spl|~sQ45_spl),
% 27.53/9.03 inference(contradiction_clause,[status(thm)],[f4636])).
% 27.53/9.03 fof(f4651,plain,(
% 27.53/9.03 ![X0]: (product(g2,f,X0,X0)|~sQ44_spl)),
% 27.53/9.03 inference(paramodulation,[status(thm)],[f3202,f47])).
% 27.53/9.03 fof(f4797,plain,(
% 27.53/9.03 product(g1,d2,d2,b)|~sQ33_spl|~sQ57_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f507,f2238])).
% 15.70/9.04 fof(f4798,plain,(
% 15.70/9.04 product(g1,d2,d2,d2)|~sQ33_spl|~sQ57_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f507,f4797])).
% 15.70/9.04 fof(f4804,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(a,g1)|product(g1,d1,a,d1)|~sQ37_spl|~sQ18_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f2778,f52])).
% 15.70/9.04 fof(f4806,definition,(
% 15.70/9.04 sQ79_spl <=> (product(g1,d1,a,d1))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f4809,plain,(
% 15.70/9.04 ~sQ0_spl|~sQ8_spl|sQ79_spl|~sQ37_spl|~sQ18_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f4804,f207,f255,f4806,f519,f432])).
% 15.70/9.04 fof(f4834,plain,(
% 15.70/9.04 d2=multiply(g1,d1,d2)|~sQ33_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f4429,f214])).
% 15.70/9.04 fof(f4836,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(d2,g1)|product(g1,d1,d2,d2)|~sQ33_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f4834,f52])).
% 15.70/9.04 fof(f4838,plain,(
% 15.70/9.04 ~sQ0_spl|~sQ1_spl|sQ75_spl|~sQ33_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f4836,f207,f210,f3873,f506,f496,f213])).
% 15.70/9.04 fof(f4843,plain,(
% 15.70/9.04 ![X0]: (X0=multiply(g2,f,X0)|~group_member(f,g2)|~group_member(X0,g2)|~sQ44_spl)),
% 15.70/9.04 inference(resolution,[status(thm)],[f1124,f52])).
% 15.70/9.04 fof(f4845,definition,(
% 15.70/9.04 ![X0]: (sQ80_spl <=> (X0=multiply(g2,f,X0)|~group_member(X0,g2)))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f4848,plain,(
% 15.70/9.04 sQ80_spl|~sQ47_spl|~sQ44_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f4843,f4845,f730,f550])).
% 15.70/9.04 fof(f4907,plain,(
% 15.70/9.04 sQ73_spl|~sQ33_spl|~sQ57_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f4798,f3303,f506,f2237])).
% 15.70/9.04 fof(f4932,definition,(
% 15.70/9.04 sQ83_spl <=> (a=multiply(g1,d2,d1))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f4933,plain,(
% 15.70/9.04 a=multiply(g1,d2,d1)|~sQ83_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f4932])).
% 15.70/9.04 fof(f4938,plain,(
% 15.70/9.04 ~group_member(d2,g1)|~group_member(d1,g1)|product(g1,d2,d1,a)|~sQ83_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f4933,f52])).
% 15.70/9.04 fof(f4940,definition,(
% 15.70/9.04 sQ84_spl <=> (product(g1,d2,d1,a))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f4941,plain,(
% 15.70/9.04 product(g1,d2,d1,a)|~sQ84_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f4940])).
% 15.70/9.04 fof(f4943,plain,(
% 15.70/9.04 ~sQ1_spl|~sQ0_spl|sQ84_spl|~sQ83_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f4938,f210,f207,f4940,f4932])).
% 15.70/9.04 fof(f4944,plain,(
% 15.70/9.04 ![X0]: (~product(g1,d1,b,X0)|a=X0|~sQ37_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f520,f347])).
% 15.70/9.04 fof(f4945,plain,(
% 15.70/9.04 ![X0]: (~product(g1,d1,d2,X0)|a=X0|~sQ33_spl|~sQ37_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f507,f4944])).
% 15.70/9.04 fof(f4947,plain,(
% 15.70/9.04 a=d1|~sQ33_spl|~sQ37_spl|~sQ76_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f4945,f3886])).
% 15.70/9.04 fof(f4948,plain,(
% 15.70/9.04 a=d2|~sQ33_spl|~sQ37_spl|~sQ75_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f4945,f3874])).
% 15.70/9.04 fof(f4950,plain,(
% 15.70/9.04 sQ35_spl|~sQ33_spl|~sQ37_spl|~sQ76_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f4947,f513,f506,f519,f3885])).
% 15.70/9.04 fof(f4951,plain,(
% 15.70/9.04 sQ32_spl|~sQ33_spl|~sQ37_spl|~sQ75_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f4948,f503,f506,f519,f3873])).
% 15.70/9.04 fof(f5003,plain,(
% 15.70/9.04 ~product(g2,h,f,h)|~sQ18_spl|~sQ2_spl|~sQ32_spl|~sQ37_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f3851,f4392])).
% 15.70/9.04 fof(f5036,plain,(
% 15.70/9.04 d2=a|d2=b|d2=d1|~sQ37_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f2532,f90])).
% 15.70/9.04 fof(f5040,plain,(
% 15.70/9.04 d1=a|d1=b|d1=d1|~sQ37_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f2532,f89])).
% 15.70/9.04 fof(f5041,plain,(
% 15.70/9.04 sQ32_spl|sQ33_spl|sQ51_spl|~sQ37_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5036,f503,f506,f1337,f519])).
% 15.70/9.04 fof(f5043,plain,(
% 15.70/9.04 sQ35_spl|sQ36_spl|sQ53_spl|~sQ37_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5040,f513,f516,f1345,f519])).
% 15.70/9.04 fof(f5123,plain,(
% 15.70/9.04 $false|~sQ18_spl|~sQ2_spl|~sQ32_spl|~sQ37_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f5003,f81])).
% 15.70/9.04 fof(f5124,plain,(
% 15.70/9.04 ~sQ18_spl|~sQ2_spl|~sQ32_spl|~sQ37_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f5123])).
% 15.70/9.04 fof(f5126,plain,(
% 15.70/9.04 $false|~sQ30_spl|~sQ37_spl|~sQ34_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f2853,f85])).
% 15.70/9.04 fof(f5127,plain,(
% 15.70/9.04 ~sQ30_spl|~sQ37_spl|~sQ34_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f5126])).
% 15.70/9.04 fof(f5214,plain,(
% 15.70/9.04 ~h=f|~sQ46_spl|sQ44_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f557,f552])).
% 15.70/9.04 fof(f5219,plain,(
% 15.70/9.04 ![X0,X1]: (~product(g2,X0,h,X1)|X0=X1|~sQ46_spl)),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f557,f129])).
% 15.70/9.04 fof(f5235,definition,(
% 15.70/9.04 sQ86_spl <=> (group_member(h,g2))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f5382,plain,(
% 15.70/9.04 f=h|~sQ46_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f5219,f80])).
% 15.70/9.04 fof(f5390,plain,(
% 15.70/9.04 $false|sQ44_spl|~sQ46_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f5382,f5214])).
% 15.70/9.04 fof(f5391,plain,(
% 15.70/9.04 sQ44_spl|~sQ46_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f5390])).
% 15.70/9.04 fof(f5496,plain,(
% 15.70/9.04 ![X0]: (~product(g1,d1,c,X0)|b=X0|~sQ37_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f520,f354])).
% 15.70/9.04 fof(f5497,plain,(
% 15.70/9.04 ![X0]: (~product(g1,d1,d1,X0)|b=X0|~sQ37_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f520,f5496])).
% 15.70/9.04 fof(f5499,plain,(
% 15.70/9.04 b=d3|~sQ37_spl|~sQ63_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f5497,f2792])).
% 15.70/9.04 fof(f5500,plain,(
% 15.70/9.04 b=d1|~sQ37_spl|~sQ49_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f5497,f4063])).
% 15.70/9.04 fof(f5501,plain,(
% 15.70/9.04 b=multiply(g1,d1,d1)|~group_member(d1,g1)|~group_member(d1,g1)|~sQ37_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f5497,f52])).
% 15.70/9.04 fof(f5502,plain,(
% 15.70/9.04 sQ30_spl|~sQ37_spl|~sQ63_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5499,f496,f519,f2791])).
% 15.70/9.04 fof(f5503,plain,(
% 15.70/9.04 sQ36_spl|~sQ37_spl|~sQ49_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5500,f516,f519,f1170])).
% 15.70/9.04 fof(f5504,definition,(
% 15.70/9.04 sQ89_spl <=> (b=multiply(g1,d1,d1))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f5505,plain,(
% 15.70/9.04 b=multiply(g1,d1,d1)|~sQ89_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f5504])).
% 15.70/9.04 fof(f5507,plain,(
% 15.70/9.04 sQ89_spl|~sQ0_spl|~sQ37_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5501,f5504,f207,f519])).
% 15.70/9.04 fof(f5528,plain,(
% 15.70/9.04 ~product(g2,h,g,an_isomorphism(d3))|~sQ33_spl|~sQ37_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f4579,f4547])).
% 15.70/9.04 fof(f5588,plain,(
% 15.70/9.04 product(g1,d1,d2,d1)|~sQ59_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f2524,f92])).
% 15.70/9.04 fof(f5592,plain,(
% 15.70/9.04 sQ76_spl|~sQ59_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5588,f3885,f2523])).
% 15.70/9.04 fof(f5676,plain,(
% 15.70/9.04 ~product(g2,h,g,f)|~sQ29_spl|~sQ33_spl|~sQ37_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f1664,f5528])).
% 15.70/9.04 fof(f5677,plain,(
% 15.70/9.04 $false|~sQ29_spl|~sQ33_spl|~sQ37_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f5676,f84])).
% 15.70/9.04 fof(f5678,plain,(
% 15.70/9.04 ~sQ29_spl|~sQ33_spl|~sQ37_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f5677])).
% 15.70/9.04 fof(f5682,plain,(
% 15.70/9.04 sQ59_spl|~sQ36_spl|~sQ30_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f3386,f2523,f516,f496])).
% 15.70/9.04 fof(f5686,plain,(
% 15.70/9.04 d3=d1|~sQ36_spl|~sQ30_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f497])).
% 15.70/9.04 fof(f5826,plain,(
% 15.70/9.04 product(g1,d1,c,a)|~sQ36_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f74])).
% 15.70/9.04 fof(f5848,plain,(
% 15.70/9.04 d1=multiply(g1,d1,d1)|~sQ36_spl|~sQ89_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f5505])).
% 15.70/9.04 fof(f5850,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(d1,g1)|product(g1,d1,d1,d1)|~sQ36_spl|~sQ89_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f5848,f52])).
% 15.70/9.04 fof(f5852,plain,(
% 15.70/9.04 ~sQ0_spl|sQ48_spl|~sQ36_spl|~sQ89_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5850,f207,f778,f516,f5504])).
% 15.70/9.04 fof(f5857,plain,(
% 15.70/9.04 d1=multiply(g1,a,b)|~sQ36_spl|~sQ10_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f273])).
% 15.70/9.04 fof(f5858,plain,(
% 15.70/9.04 d1=multiply(g1,a,d1)|~sQ36_spl|~sQ10_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f5857])).
% 15.70/9.04 fof(f5860,plain,(
% 15.70/9.04 ~group_member(a,g1)|~group_member(d1,g1)|product(g1,a,d1,d1)|~sQ36_spl|~sQ10_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f5858,f52])).
% 15.70/9.04 fof(f5862,plain,(
% 15.70/9.04 ~sQ8_spl|~sQ0_spl|sQ71_spl|~sQ36_spl|~sQ10_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5860,f255,f207,f3045,f516,f272])).
% 15.70/9.04 fof(f5866,plain,(
% 15.70/9.04 d1=multiply(g1,b,a)|~sQ36_spl|~sQ13_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f291])).
% 15.70/9.04 fof(f5867,plain,(
% 15.70/9.04 d1=multiply(g1,d1,a)|~sQ36_spl|~sQ13_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f5866])).
% 15.70/9.04 fof(f5869,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(a,g1)|product(g1,d1,a,d1)|~sQ36_spl|~sQ13_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f5867,f52])).
% 15.70/9.04 fof(f5871,plain,(
% 15.70/9.04 ~sQ0_spl|~sQ8_spl|sQ79_spl|~sQ36_spl|~sQ13_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5869,f207,f255,f4806,f516,f290])).
% 15.70/9.04 fof(f5872,plain,(
% 15.70/9.04 d1=multiply(g1,d1,d2)|~sQ36_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f5686,f214])).
% 15.70/9.04 fof(f5874,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(d2,g1)|product(g1,d1,d2,d1)|~sQ36_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f5872,f52])).
% 15.70/9.04 fof(f5876,plain,(
% 15.70/9.04 ~sQ0_spl|~sQ1_spl|sQ76_spl|~sQ36_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5874,f207,f210,f3885,f516,f496,f213])).
% 15.70/9.04 fof(f5934,plain,(
% 15.70/9.04 d2=d1|~sQ36_spl|~sQ33_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f517,f507])).
% 15.70/9.04 fof(f5968,plain,(
% 15.70/9.04 ![X0]: (~group_member(X0,g1)|X0=a|X0=d1|X0=d3|~sQ31_spl|~sQ36_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f500,f787])).
% 15.70/9.04 fof(f5971,plain,(
% 15.70/9.04 identity_for(g1)=a|identity_for(g1)=d1|identity_for(g1)=d3|~sQ31_spl|~sQ36_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f5968,f46])).
% 15.70/9.04 fof(f5975,plain,(
% 15.70/9.04 sQ26_spl|sQ52_spl|sQ60_spl|~sQ31_spl|~sQ36_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5971,f483,f1341,f2527,f499,f516])).
% 15.70/9.04 fof(f5985,plain,(
% 15.70/9.04 ~product(g2,g,g,an_isomorphism(d3))|~sQ33_spl|~sQ36_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f4579,f1602])).
% 15.70/9.04 fof(f5995,plain,(
% 15.70/9.04 a=d1|~sQ36_spl|~sQ27_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f3346,f3257])).
% 15.70/9.04 fof(f6007,plain,(
% 15.70/9.04 sQ35_spl|~sQ36_spl|~sQ27_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f5995,f513,f516,f486])).
% 15.70/9.04 fof(f6162,plain,(
% 15.70/9.04 product(g1,d1,d2,a)|~sQ34_spl|~sQ36_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f510,f790])).
% 15.70/9.04 fof(f6182,plain,(
% 15.70/9.04 d2=multiply(g1,a,c)|~sQ34_spl|~sQ15_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f510,f302])).
% 15.70/9.04 fof(f6183,plain,(
% 15.70/9.04 d2=multiply(g1,a,d2)|~sQ34_spl|~sQ15_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f510,f6182])).
% 15.70/9.04 fof(f6207,plain,(
% 15.70/9.04 d1=multiply(g1,d1,d2)|~sQ36_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f5686,f214])).
% 15.70/9.04 fof(f6245,plain,(
% 15.70/9.04 h=multiply(g2,g,g)|~group_member(g,g2)|~group_member(g,g2)),
% 15.70/9.04 inference(resolution,[status(thm)],[f408,f52])).
% 15.70/9.04 fof(f6246,definition,(
% 15.70/9.04 sQ90_spl <=> (h=multiply(g2,g,g))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6247,plain,(
% 15.70/9.04 h=multiply(g2,g,g)|~sQ90_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f6246])).
% 15.70/9.04 fof(f6249,plain,(
% 15.70/9.04 sQ90_spl|~sQ56_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6245,f6246,f1777])).
% 15.70/9.04 fof(f6250,plain,(
% 15.70/9.04 $false|sQ56_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f1779,f64])).
% 15.70/9.04 fof(f6251,plain,(
% 15.70/9.04 sQ56_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f6250])).
% 15.70/9.04 fof(f6252,plain,(
% 15.70/9.04 ~group_member(g,g2)|~group_member(g,g2)|group_member(h,g2)|~sQ90_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6247,f53])).
% 15.70/9.04 fof(f6253,plain,(
% 15.70/9.04 ~group_member(g,g2)|~group_member(g,g2)|product(g2,g,g,h)|~sQ90_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6247,f52])).
% 15.70/9.04 fof(f6254,plain,(
% 15.70/9.04 ~sQ56_spl|sQ86_spl|~sQ90_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6252,f1777,f5235,f6246])).
% 15.70/9.04 fof(f6255,definition,(
% 15.70/9.04 sQ91_spl <=> (product(g2,g,g,h))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6258,plain,(
% 15.70/9.04 ~sQ56_spl|sQ91_spl|~sQ90_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6253,f1777,f6255,f6246])).
% 15.70/9.04 fof(f6260,plain,(
% 15.70/9.04 f=multiply(g2,g,h)|~group_member(g,g2)|~group_member(h,g2)),
% 15.70/9.04 inference(resolution,[status(thm)],[f415,f52])).
% 15.70/9.04 fof(f6261,definition,(
% 15.70/9.04 sQ92_spl <=> (f=multiply(g2,g,h))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6262,plain,(
% 15.70/9.04 f=multiply(g2,g,h)|~sQ92_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f6261])).
% 15.70/9.04 fof(f6264,plain,(
% 15.70/9.04 sQ92_spl|~sQ56_spl|~sQ86_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6260,f6261,f1777,f5235])).
% 15.70/9.04 fof(f6266,plain,(
% 15.70/9.04 ~group_member(g,g2)|~group_member(h,g2)|product(g2,g,h,f)|~sQ92_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6262,f52])).
% 15.70/9.04 fof(f6268,definition,(
% 15.70/9.04 sQ93_spl <=> (product(g2,g,h,f))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6271,plain,(
% 15.70/9.04 ~sQ56_spl|~sQ86_spl|sQ93_spl|~sQ92_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6266,f1777,f5235,f6268,f6261])).
% 15.70/9.04 fof(f6273,plain,(
% 15.70/9.04 f=multiply(g2,h,g)|~group_member(h,g2)|~group_member(g,g2)),
% 15.70/9.04 inference(resolution,[status(thm)],[f422,f52])).
% 15.70/9.04 fof(f6274,definition,(
% 15.70/9.04 sQ94_spl <=> (f=multiply(g2,h,g))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6275,plain,(
% 15.70/9.04 f=multiply(g2,h,g)|~sQ94_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f6274])).
% 15.70/9.04 fof(f6277,plain,(
% 15.70/9.04 sQ94_spl|~sQ86_spl|~sQ56_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6273,f6274,f5235,f1777])).
% 15.70/9.04 fof(f6294,plain,(
% 15.70/9.04 ~group_member(h,g2)|~group_member(g,g2)|product(g2,h,g,f)|~sQ94_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6275,f52])).
% 15.70/9.04 fof(f6296,definition,(
% 15.70/9.04 sQ95_spl <=> (product(g2,h,g,f))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6299,plain,(
% 15.70/9.04 ~sQ86_spl|~sQ56_spl|sQ95_spl|~sQ94_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6294,f5235,f1777,f6296,f6274])).
% 15.70/9.04 fof(f6301,plain,(
% 15.70/9.04 g=multiply(g2,h,h)|~group_member(h,g2)|~group_member(h,g2)),
% 15.70/9.04 inference(resolution,[status(thm)],[f429,f52])).
% 15.70/9.04 fof(f6302,definition,(
% 15.70/9.04 sQ96_spl <=> (g=multiply(g2,h,h))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6303,plain,(
% 15.70/9.04 g=multiply(g2,h,h)|~sQ96_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f6302])).
% 15.70/9.04 fof(f6305,plain,(
% 15.70/9.04 sQ96_spl|~sQ86_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6301,f6302,f5235])).
% 15.70/9.04 fof(f6307,plain,(
% 15.70/9.04 ~group_member(h,g2)|~group_member(h,g2)|product(g2,h,h,g)|~sQ96_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6303,f52])).
% 15.70/9.04 fof(f6309,definition,(
% 15.70/9.04 sQ97_spl <=> (product(g2,h,h,g))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6312,plain,(
% 15.70/9.04 ~sQ86_spl|sQ97_spl|~sQ96_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6307,f5235,f6309,f6302])).
% 15.70/9.04 fof(f6313,plain,(
% 15.70/9.04 ![X0]: (~product(g1,d1,d2,X0)|d1=X0|~sQ36_spl|~sQ30_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f5686,f94])).
% 15.70/9.04 fof(f6314,plain,(
% 15.70/9.04 d1=a|~sQ30_spl|~sQ34_spl|~sQ36_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f6313,f6162])).
% 15.70/9.04 fof(f6317,plain,(
% 15.70/9.04 sQ35_spl|~sQ30_spl|~sQ34_spl|~sQ36_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6314,f513,f496,f509,f516])).
% 15.70/9.04 fof(f6359,plain,(
% 15.70/9.04 d2=a|d2=d1|d2=c|~sQ36_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f787,f90])).
% 15.70/9.04 fof(f6363,plain,(
% 15.70/9.04 d1=a|d1=d1|d1=c|~sQ36_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f787,f89])).
% 15.70/9.04 fof(f6365,plain,(
% 15.70/9.04 sQ32_spl|sQ51_spl|sQ34_spl|~sQ36_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6359,f503,f1337,f509,f516])).
% 15.70/9.04 fof(f6367,plain,(
% 15.70/9.04 sQ35_spl|sQ53_spl|sQ37_spl|~sQ36_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6363,f513,f1345,f519,f516])).
% 15.70/9.04 fof(f6369,plain,(
% 15.70/9.04 product(g1,d2,d2,d1)|~sQ36_spl|~sQ33_spl|~sQ73_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f5934,f3304])).
% 15.70/9.04 fof(f6373,plain,(
% 15.70/9.04 d1=multiply(g1,d1,d1)|~sQ33_spl|~sQ36_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f5934,f6207])).
% 15.70/9.04 fof(f6378,plain,(
% 15.70/9.04 product(g1,d1,d2,d1)|~sQ36_spl|~sQ33_spl|~sQ73_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f5934,f6369])).
% 15.70/9.04 fof(f6379,plain,(
% 15.70/9.04 product(g1,d1,d1,d1)|~sQ36_spl|~sQ33_spl|~sQ73_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f5934,f6378])).
% 15.70/9.04 fof(f6449,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(d1,g1)|product(g1,d1,d1,d1)|~sQ33_spl|~sQ36_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6373,f52])).
% 15.70/9.04 fof(f6451,plain,(
% 15.70/9.04 ~sQ0_spl|sQ48_spl|~sQ33_spl|~sQ36_spl|~sQ30_spl|~sQ2_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6449,f207,f778,f506,f516,f496,f213])).
% 15.70/9.04 fof(f6457,plain,(
% 15.70/9.04 d1=c|~sQ48_spl|~sQ36_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f860,f792])).
% 15.70/9.04 fof(f6459,plain,(
% 15.70/9.04 d1=multiply(g1,d1,d1)|~group_member(d1,g1)|~group_member(d1,g1)|~sQ48_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f860,f52])).
% 15.70/9.04 fof(f6461,plain,(
% 15.70/9.04 sQ37_spl|~sQ48_spl|~sQ36_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6457,f519,f778,f516])).
% 15.70/9.04 fof(f6462,definition,(
% 15.70/9.04 sQ99_spl <=> (d1=multiply(g1,d1,d1))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f6463,plain,(
% 15.70/9.04 d1=multiply(g1,d1,d1)|~sQ99_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f6462])).
% 15.70/9.04 fof(f6465,plain,(
% 15.70/9.04 sQ99_spl|~sQ0_spl|~sQ48_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6459,f6462,f207,f778])).
% 15.70/9.04 fof(f6488,plain,(
% 15.70/9.04 product(g1,d1,d2,a)|~sQ34_spl|~sQ36_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f510,f5826])).
% 15.70/9.04 fof(f6492,plain,(
% 15.70/9.04 an_isomorphism(d2)=h|~sQ34_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f510,f88])).
% 15.70/9.04 fof(f6514,plain,(
% 15.70/9.04 d3=d2|~sQ34_spl|~sQ31_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f510,f500])).
% 15.70/9.04 fof(f6708,plain,(
% 15.70/9.04 identity_for(g1)=d2|~sQ34_spl|~sQ28_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f510,f490])).
% 15.70/9.04 fof(f6757,plain,(
% 15.70/9.04 ~d2=a|~sQ34_spl|~sQ31_spl|sQ29_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f6514,f495])).
% 15.70/9.04 fof(f6758,plain,(
% 15.70/9.04 ~d2=d2|~sQ32_spl|~sQ34_spl|~sQ31_spl|sQ29_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f504,f6757])).
% 15.70/9.04 fof(f6759,plain,(
% 15.70/9.04 $false|~sQ32_spl|~sQ34_spl|~sQ31_spl|sQ29_spl),
% 15.70/9.04 inference(trivial_equality_resolution,[status(thm)],[f6758])).
% 15.70/9.04 fof(f6760,plain,(
% 15.70/9.04 ~sQ32_spl|~sQ34_spl|~sQ31_spl|sQ29_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f6759])).
% 15.70/9.04 fof(f6907,plain,(
% 15.70/9.04 h=multiply(g2,h,identity_for(g2))),
% 15.70/9.04 inference(resolution,[status(thm)],[f65,f244])).
% 15.70/9.04 fof(f6908,plain,(
% 15.70/9.04 h=multiply(g2,identity_for(g2),h)),
% 15.70/9.04 inference(resolution,[status(thm)],[f65,f236])).
% 15.70/9.04 fof(f6909,plain,(
% 15.70/9.04 h=multiply(g2,h,f)|~sQ44_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f3202,f6907])).
% 15.70/9.04 fof(f6910,plain,(
% 15.70/9.04 h=multiply(g2,f,h)|~sQ44_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f3202,f6908])).
% 15.70/9.04 fof(f6917,plain,(
% 15.70/9.04 d1=d2|~sQ52_spl|~sQ34_spl|~sQ28_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f1342,f6708])).
% 15.70/9.04 fof(f6935,plain,(
% 15.70/9.04 sQ51_spl|~sQ52_spl|~sQ34_spl|~sQ28_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6917,f1337,f1341,f509,f489])).
% 15.70/9.04 fof(f7016,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(d1,g1)|product(g1,d1,d1,d1)|~sQ99_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6463,f52])).
% 15.70/9.04 fof(f7018,plain,(
% 15.70/9.04 ~sQ0_spl|sQ48_spl|~sQ99_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7016,f207,f778,f6462])).
% 15.70/9.04 fof(f7181,plain,(
% 15.70/9.04 ~group_member(h,g2)|~group_member(f,g2)|product(g2,h,f,h)|~sQ44_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6909,f52])).
% 15.70/9.04 fof(f7183,definition,(
% 15.70/9.04 sQ100_spl <=> (product(g2,h,f,h))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f7186,plain,(
% 15.70/9.04 ~sQ86_spl|~sQ47_spl|sQ100_spl|~sQ44_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7181,f5235,f730,f7183,f550])).
% 15.70/9.04 fof(f7188,plain,(
% 15.70/9.04 ~group_member(f,g2)|~group_member(h,g2)|product(g2,f,h,h)|~sQ44_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f6910,f52])).
% 15.70/9.04 fof(f7190,definition,(
% 15.70/9.04 sQ101_spl <=> (product(g2,f,h,h))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f7193,plain,(
% 15.70/9.04 ~sQ47_spl|~sQ86_spl|sQ101_spl|~sQ44_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7188,f730,f5235,f7190,f550])).
% 15.70/9.04 fof(f7235,plain,(
% 15.70/9.04 ![X0]: (~product(g1,d1,d2,X0)|d2=X0|~sQ34_spl|~sQ31_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f6514,f896])).
% 15.70/9.04 fof(f7238,plain,(
% 15.70/9.04 d2=a|~sQ31_spl|~sQ34_spl|~sQ36_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f7235,f6488])).
% 15.70/9.04 fof(f7241,plain,(
% 15.70/9.04 sQ32_spl|~sQ31_spl|~sQ34_spl|~sQ36_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7238,f503,f499,f509,f516])).
% 15.70/9.04 fof(f7382,plain,(
% 15.70/9.04 an_isomorphism(d3)=h|~sQ31_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f500,f88])).
% 15.70/9.04 fof(f7490,plain,(
% 15.70/9.04 d3=d1|~sQ36_spl|~sQ32_spl|~sQ13_spl|~sQ2_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f3704,f214])).
% 15.70/9.04 fof(f7493,plain,(
% 15.70/9.04 sQ59_spl|~sQ36_spl|~sQ32_spl|~sQ13_spl|~sQ2_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7490,f2523,f516,f503,f290,f213])).
% 15.70/9.04 fof(f7504,plain,(
% 15.70/9.04 sQ48_spl|~sQ36_spl|~sQ33_spl|~sQ73_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f6379,f778,f516,f506,f3303])).
% 15.70/9.04 fof(f7505,plain,(
% 15.70/9.04 ~product(g2,g,g,h)|~sQ31_spl|~sQ33_spl|~sQ36_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f7382,f5985])).
% 15.70/9.04 fof(f7506,plain,(
% 15.70/9.04 $false|~sQ31_spl|~sQ33_spl|~sQ36_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f7505,f82])).
% 15.70/9.04 fof(f7507,plain,(
% 15.70/9.04 ~sQ31_spl|~sQ33_spl|~sQ36_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f7506])).
% 15.70/9.04 fof(f7613,plain,(
% 15.70/9.04 product(g1,d1,d1,d1)|~sQ51_spl|~sQ76_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f1338,f3886])).
% 15.70/9.04 fof(f7620,plain,(
% 15.70/9.04 sQ48_spl|~sQ51_spl|~sQ76_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7613,f778,f1337,f3885])).
% 15.70/9.04 fof(f7734,plain,(
% 15.70/9.04 d3=multiply(g1,d1,d1)|~sQ51_spl|~sQ2_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f1338,f214])).
% 15.70/9.04 fof(f7736,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(d1,g1)|product(g1,d1,d1,d3)|~sQ51_spl|~sQ2_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f7734,f52])).
% 15.70/9.04 fof(f7738,plain,(
% 15.70/9.04 ~sQ0_spl|sQ63_spl|~sQ51_spl|~sQ2_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7736,f207,f2791,f1337,f213])).
% 15.70/9.04 fof(f7907,plain,(
% 15.70/9.04 ![X0]: (~product(g1,d1,d1,X0)|d3=X0|~sQ51_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f1338,f985])).
% 15.70/9.04 fof(f7908,plain,(
% 15.70/9.04 d3=c|~sQ51_spl|~sQ36_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f7907,f792])).
% 15.70/9.04 fof(f7910,plain,(
% 15.70/9.04 d3=multiply(g1,d1,d1)|~group_member(d1,g1)|~group_member(d1,g1)|~sQ51_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f7907,f52])).
% 15.70/9.04 fof(f7911,plain,(
% 15.70/9.04 sQ31_spl|~sQ51_spl|~sQ36_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7908,f499,f1337,f516])).
% 15.70/9.04 fof(f7912,definition,(
% 15.70/9.04 sQ112_spl <=> (d3=multiply(g1,d1,d1))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f7913,plain,(
% 15.70/9.04 d3=multiply(g1,d1,d1)|~sQ112_spl),
% 15.70/9.04 inference(component_clause,[status(thm)],[f7912])).
% 15.70/9.04 fof(f7915,plain,(
% 15.70/9.04 sQ112_spl|~sQ0_spl|~sQ51_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f7910,f7912,f207,f1337])).
% 15.70/9.04 fof(f7916,plain,(
% 15.70/9.04 sQ51_spl|~sQ35_spl|~sQ32_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f1086,f1337,f513,f503])).
% 15.70/9.04 fof(f7959,plain,(
% 15.70/9.04 an_isomorphism(d3)=h|~sQ31_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f500,f88])).
% 15.70/9.04 fof(f7962,plain,(
% 15.70/9.04 ~product(g2,an_isomorphism(d1),an_isomorphism(d2),g)|~sQ30_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f2839,f93])).
% 15.70/9.04 fof(f8110,plain,(
% 15.70/9.04 ~product(g2,f,an_isomorphism(d2),g)|~sQ35_spl|~sQ30_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f598,f7962])).
% 15.70/9.04 fof(f8114,plain,(
% 15.70/9.04 ~d1=d3|~sQ31_spl|sQ37_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f500,f521])).
% 15.70/9.04 fof(f8117,plain,(
% 15.70/9.04 ~d3=d1|~sQ35_spl|sQ29_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f495])).
% 15.70/9.04 fof(f8128,plain,(
% 15.70/9.04 ~d3=a|~sQ31_spl|sQ20_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f500,f464])).
% 15.70/9.04 fof(f8129,plain,(
% 15.70/9.04 ~d3=d1|~sQ35_spl|~sQ31_spl|sQ20_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f8128])).
% 15.70/9.04 fof(f8403,plain,(
% 15.70/9.04 ~sQ59_spl|~sQ35_spl|~sQ31_spl|sQ20_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f8129,f2523,f513,f499,f462])).
% 15.70/9.04 fof(f8407,plain,(
% 15.70/9.04 ~sQ59_spl|~sQ35_spl|sQ29_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f8117,f2523,f513,f493])).
% 15.70/9.04 fof(f8408,plain,(
% 15.70/9.04 ~sQ59_spl|~sQ31_spl|sQ37_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f8114,f2523,f499,f519])).
% 15.70/9.04 fof(f8480,plain,(
% 15.70/9.04 b=multiply(g1,d1,b)|~sQ35_spl|~sQ10_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f273])).
% 15.70/9.04 fof(f8482,plain,(
% 15.70/9.04 ~group_member(d1,g1)|~group_member(b,g1)|product(g1,d1,b,b)|~sQ35_spl|~sQ10_spl),
% 15.70/9.04 inference(paramodulation,[status(thm)],[f8480,f52])).
% 15.70/9.04 fof(f8484,definition,(
% 15.70/9.04 sQ115_spl <=> (product(g1,d1,b,b))),
% 15.70/9.04 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 15.70/9.04 fof(f8487,plain,(
% 15.70/9.04 ~sQ0_spl|~sQ11_spl|sQ115_spl|~sQ35_spl|~sQ10_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f8482,f207,f275,f8484,f513,f272])).
% 15.70/9.04 fof(f8618,plain,(
% 15.70/9.04 d1=multiply(g1,a,a)|~sQ35_spl|~sQ7_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f253])).
% 15.70/9.04 fof(f8619,plain,(
% 15.70/9.04 d1=multiply(g1,d1,a)|~sQ35_spl|~sQ7_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f8618])).
% 15.70/9.04 fof(f8620,plain,(
% 15.70/9.04 d3=d1|~sQ35_spl|~sQ7_spl|~sQ112_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f8621,f7913])).
% 15.70/9.04 fof(f8621,plain,(
% 15.70/9.04 d1=multiply(g1,d1,d1)|~sQ35_spl|~sQ7_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f8619])).
% 15.70/9.04 fof(f8624,plain,(
% 15.70/9.04 sQ59_spl|~sQ35_spl|~sQ7_spl|~sQ112_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f8620,f2523,f513,f252,f7912])).
% 15.70/9.04 fof(f8637,plain,(
% 15.70/9.04 ~d2=d1|~sQ35_spl|sQ32_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f505])).
% 15.70/9.04 fof(f8803,plain,(
% 15.70/9.04 ![X0]: (~group_member(X0,g1)|X0=d3|X0=d2|X0=c|~sQ33_spl|~sQ29_spl)),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f507,f2513])).
% 15.70/9.04 fof(f8808,plain,(
% 15.70/9.04 d1=d3|d1=d2|d1=c|~sQ33_spl|~sQ29_spl),
% 15.70/9.04 inference(resolution,[status(thm)],[f8803,f89])).
% 15.70/9.04 fof(f8811,plain,(
% 15.70/9.04 sQ59_spl|sQ51_spl|sQ37_spl|~sQ33_spl|~sQ29_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f8808,f2523,f1337,f519,f506,f493])).
% 15.70/9.04 fof(f8815,plain,(
% 15.70/9.04 ~product(g2,f,g,g)|~sQ33_spl|~sQ35_spl|~sQ30_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f4579,f8110])).
% 15.70/9.04 fof(f8816,plain,(
% 15.70/9.04 $false|~sQ44_spl|~sQ33_spl|~sQ35_spl|~sQ30_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f8815,f4651])).
% 15.70/9.04 fof(f8817,plain,(
% 15.70/9.04 ~sQ44_spl|~sQ33_spl|~sQ35_spl|~sQ30_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f8816])).
% 15.70/9.04 fof(f9030,plain,(
% 15.70/9.04 d2=multiply(g1,d1,d2)|~sQ35_spl|~sQ34_spl|~sQ15_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f6183])).
% 15.70/9.04 fof(f9426,plain,(
% 15.70/9.04 ~d3=d2|~sQ33_spl|sQ30_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f507,f498])).
% 15.70/9.04 fof(f9470,plain,(
% 15.70/9.04 d3=c|~sQ60_spl|~sQ28_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f2528,f490])).
% 15.70/9.04 fof(f9474,plain,(
% 15.70/9.04 product(g1,d2,d1,d1)|~sQ35_spl|~sQ84_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f4941])).
% 15.70/9.04 fof(f9549,plain,(
% 15.70/9.04 d2=multiply(g1,d1,b)|~sQ33_spl|~sQ35_spl|~sQ10_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f507,f8480])).
% 15.70/9.04 fof(f9550,plain,(
% 15.70/9.04 d3=d2|~sQ33_spl|~sQ35_spl|~sQ10_spl|~sQ2_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f9551,f214])).
% 15.70/9.04 fof(f9551,plain,(
% 15.70/9.04 d2=multiply(g1,d1,d2)|~sQ33_spl|~sQ35_spl|~sQ10_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f507,f9549])).
% 15.70/9.04 fof(f9554,plain,(
% 15.70/9.04 $false|sQ30_spl|~sQ33_spl|~sQ35_spl|~sQ10_spl|~sQ2_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f9550,f9426])).
% 15.70/9.04 fof(f9555,plain,(
% 15.70/9.04 sQ30_spl|~sQ33_spl|~sQ35_spl|~sQ10_spl|~sQ2_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f9554])).
% 15.70/9.04 fof(f9637,plain,(
% 15.70/9.04 d2=a|~sQ34_spl|~sQ20_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f510,f463])).
% 15.70/9.04 fof(f9638,plain,(
% 15.70/9.04 d2=d1|~sQ35_spl|~sQ34_spl|~sQ20_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f514,f9637])).
% 15.70/9.04 fof(f9639,plain,(
% 15.70/9.04 $false|sQ32_spl|~sQ35_spl|~sQ34_spl|~sQ20_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f9638,f8637])).
% 15.70/9.04 fof(f9640,plain,(
% 15.70/9.04 sQ32_spl|~sQ35_spl|~sQ34_spl|~sQ20_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f9639])).
% 15.70/9.04 fof(f9648,plain,(
% 15.70/9.04 sQ31_spl|~sQ60_spl|~sQ28_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f9470,f499,f2527,f489])).
% 15.70/9.04 fof(f9650,plain,(
% 15.70/9.04 ~sQ59_spl|~sQ60_spl|sQ52_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f2725,f2523,f2527,f1341])).
% 15.70/9.04 fof(f9872,plain,(
% 15.70/9.04 sQ50_spl|~sQ35_spl|~sQ84_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f9474,f1319,f513,f4940])).
% 15.70/9.04 fof(f9966,plain,(
% 15.70/9.04 ~product(g2,f,h,an_isomorphism(d3))|~sQ34_spl|~sQ35_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f6492,f1085])).
% 15.70/9.04 fof(f10004,plain,(
% 15.70/9.04 ~d3=d2|~sQ34_spl|sQ31_spl),
% 15.70/9.04 inference(forward_demodulation,[status(thm)],[f510,f501])).
% 15.70/9.04 fof(f10005,plain,(
% 15.70/9.04 $false|~sQ34_spl|sQ31_spl|~sQ72_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f3196,f10004])).
% 15.70/9.04 fof(f10006,plain,(
% 15.70/9.04 ~sQ34_spl|sQ31_spl|~sQ72_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f10005])).
% 15.70/9.04 fof(f10027,plain,(
% 15.70/9.04 ~sQ41_spl|~sQ44_spl|sQ45_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f2690,f539,f550,f553])).
% 15.70/9.04 fof(f10032,plain,(
% 15.70/9.04 ~product(g2,f,h,h)|~sQ31_spl|~sQ34_spl|~sQ35_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f7959,f9966])).
% 15.70/9.04 fof(f10033,plain,(
% 15.70/9.04 $false|~sQ44_spl|~sQ31_spl|~sQ34_spl|~sQ35_spl),
% 15.70/9.04 inference(forward_subsumption_resolution,[status(thm)],[f10032,f4651])).
% 15.70/9.04 fof(f10034,plain,(
% 15.70/9.04 ~sQ44_spl|~sQ31_spl|~sQ34_spl|~sQ35_spl),
% 15.70/9.04 inference(contradiction_clause,[status(thm)],[f10033])).
% 15.70/9.04 fof(f10243,plain,(
% 15.70/9.04 d3=d2|~sQ35_spl|~sQ34_spl|~sQ15_spl|~sQ2_spl),
% 15.70/9.04 inference(backward_demodulation,[status(thm)],[f9030,f214])).
% 15.70/9.04 fof(f10246,plain,(
% 15.70/9.04 sQ72_spl|~sQ35_spl|~sQ34_spl|~sQ15_spl|~sQ2_spl),
% 15.70/9.04 inference(split_clause,[status(thm)],[f10243,f3195,f513,f509,f301,f213])).
% 15.70/9.04 fof(f10249,plain,(
% 15.70/9.04 $false),
% 15.70/9.04 inference(sat_refutation,[status(thm)],[f216,f223,f227,f229,f231,f249,f258,f265,f267,f278,f283,f285,f293,f298,f307,f312,f314,f435,f440,f452,f492,f502,f512,f522,f545,f549,f559,f821,f829,f830,f831,f973,f1075,f1173,f1340,f1494,f1539,f1540,f1543,f1958,f2011,f2240,f2384,f2551,f2993,f3022,f3024,f3041,f3048,f3056,f3172,f3385,f3701,f3705,f3708,f4085,f4091,f4295,f4296,f4316,f4637,f4809,f4838,f4848,f4907,f4943,f4950,f4951,f5041,f5043,f5124,f5127,f5391,f5502,f5503,f5507,f5592,f5678,f5682,f5852,f5862,f5871,f5876,f5975,f6007,f6249,f6251,f6254,f6258,f6264,f6271,f6277,f6299,f6305,f6312,f6317,f6365,f6367,f6451,f6461,f6465,f6760,f6935,f7018,f7186,f7193,f7241,f7493,f7504,f7507,f7620,f7738,f7911,f7915,f7916,f8403,f8407,f8408,f8487,f8624,f8811,f8817,f9555,f9640,f9648,f9650,f9872,f10006,f10027,f10034,f10246])).
% 15.70/9.04 % SZS output end CNFRefutation for theBenchmark.p
% 15.70/9.07 % Elapsed time: 3.662096 seconds
% 15.70/9.07 % CPU time: 28.442242 seconds
% 15.70/9.07 % Total memory used: 234.664 MB
% 15.70/9.07 % Net memory used: 216.204 MB
%------------------------------------------------------------------------------