%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP617-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:36:54 PM UTC 2026
% Result : Unsatisfiable 30.92s 4.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP617-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 20:22:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 30.92/4.34 % Refutation found
% 30.92/4.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 30.92/4.34 % SZS output start CNFRefutation for theBenchmark
% 30.92/4.34 fof(f1,axiom,(
% 30.92/4.34 (![X]: (product(identity,X,X) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f2,axiom,(
% 30.92/4.34 (![X]: (product(X,identity,X) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f3,axiom,(
% 30.92/4.34 (![X]: (product(inverse(X),X,identity) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f4,axiom,(
% 30.92/4.34 (![X]: (product(X,inverse(X),identity) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f5,axiom,(
% 30.92/4.34 (![X,Y]: (product(X,Y,multiply(X,Y)) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f6,axiom,(
% 30.92/4.34 (![X,Y,Z,W]: (( ~ product(X,Y,Z)| ~ product(X,Y,W)| Z = W ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f7,axiom,(
% 30.92/4.34 (![X,Y,U,Z,V,W]: (( ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W)| product(X,V,W) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f8,axiom,(
% 30.92/4.34 (![X,Y,U,Z,V,W]: (( ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(X,V,W)| product(U,Z,W) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f9,axiom,(
% 30.92/4.34 (![X]: (( ~ subgroup1_member(X)| subgroup1_member(inverse(X)) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f10,axiom,(
% 30.92/4.34 (![A,B,C]: (( ~ subgroup1_member(A)| ~ subgroup1_member(B)| ~ product(A,B,C)| subgroup1_member(C) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f11,axiom,(
% 30.92/4.34 (![X]: (( ~ subgroup2_member(X)| subgroup2_member(inverse(X)) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f12,axiom,(
% 30.92/4.34 (![A,B,C]: (( ~ subgroup2_member(A)| ~ subgroup2_member(B)| ~ product(A,B,C)| subgroup2_member(C) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f13,hypothesis,(
% 30.92/4.34 (![X,A]: (( ~ subgroup1_member(X)| subgroup1_member(multiply(A,multiply(X,inverse(A)))) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f14,hypothesis,(
% 30.92/4.34 (![X,A]: (( ~ subgroup2_member(X)| subgroup2_member(multiply(A,multiply(X,inverse(A)))) ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f15,hypothesis,(
% 30.92/4.34 (![X]: (( ~ subgroup1_member(X)| ~ subgroup2_member(X)| X = identity ) ))),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f16,hypothesis,(
% 30.92/4.34 subgroup1_member(v) ),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f17,hypothesis,(
% 30.92/4.34 subgroup2_member(u) ),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f18,negated_conjecture,(
% 30.92/4.34 multiply(v,u) != multiply(u,v) ),
% 30.92/4.34 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.92/4.34 fof(f19,plain,(
% 30.92/4.34 ![X0]: (product(identity,X0,X0))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f1])).
% 30.92/4.34 fof(f20,plain,(
% 30.92/4.34 ![X0]: (product(X0,identity,X0))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f2])).
% 30.92/4.34 fof(f21,plain,(
% 30.92/4.34 ![X0]: (product(inverse(X0),X0,identity))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f3])).
% 30.92/4.34 fof(f22,plain,(
% 30.92/4.34 ![X0]: (product(X0,inverse(X0),identity))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f4])).
% 30.92/4.34 fof(f23,plain,(
% 30.92/4.34 ![X0,X1]: (product(X0,X1,multiply(X0,X1)))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f5])).
% 30.92/4.34 fof(f24,plain,(
% 30.92/4.34 ![Z,W]: ((![X,Y]: (~product(X,Y,Z)|~product(X,Y,W)))|Z=W)),
% 30.92/4.34 inference(miniscoping,[status(thm)],[f6])).
% 30.92/4.34 fof(f25,plain,(
% 30.92/4.34 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|X2=X3)),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f24])).
% 30.92/4.34 fof(f26,plain,(
% 30.92/4.34 ![X,V,W]: ((![U,Z]: ((![Y]: (~product(X,Y,U)|~product(Y,Z,V)))|~product(U,Z,W)))|product(X,V,W))),
% 30.92/4.34 inference(miniscoping,[status(thm)],[f7])).
% 30.92/4.34 fof(f27,plain,(
% 30.92/4.34 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X1,X3,X4)|~product(X2,X3,X5)|product(X0,X4,X5))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f26])).
% 30.92/4.34 fof(f28,plain,(
% 30.92/4.34 ![U,Z,W]: ((![X,V]: ((![Y]: (~product(X,Y,U)|~product(Y,Z,V)))|~product(X,V,W)))|product(U,Z,W))),
% 30.92/4.34 inference(miniscoping,[status(thm)],[f8])).
% 30.92/4.34 fof(f29,plain,(
% 30.92/4.34 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X1,X3,X4)|~product(X0,X4,X5)|product(X2,X3,X5))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f28])).
% 30.92/4.34 fof(f30,plain,(
% 30.92/4.34 ![X0]: (~subgroup1_member(X0)|subgroup1_member(inverse(X0)))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f9])).
% 30.92/4.34 fof(f31,plain,(
% 30.92/4.34 ![C]: ((![A,B]: ((~subgroup1_member(A)|~subgroup1_member(B))|~product(A,B,C)))|subgroup1_member(C))),
% 30.92/4.34 inference(miniscoping,[status(thm)],[f10])).
% 30.92/4.34 fof(f32,plain,(
% 30.92/4.34 ![X0,X1,X2]: (~subgroup1_member(X0)|~subgroup1_member(X1)|~product(X0,X1,X2)|subgroup1_member(X2))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f31])).
% 30.92/4.34 fof(f33,plain,(
% 30.92/4.34 ![X0]: (~subgroup2_member(X0)|subgroup2_member(inverse(X0)))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f11])).
% 30.92/4.34 fof(f34,plain,(
% 30.92/4.34 ![C]: ((![A,B]: ((~subgroup2_member(A)|~subgroup2_member(B))|~product(A,B,C)))|subgroup2_member(C))),
% 30.92/4.34 inference(miniscoping,[status(thm)],[f12])).
% 30.92/4.34 fof(f35,plain,(
% 30.92/4.34 ![X0,X1,X2]: (~subgroup2_member(X0)|~subgroup2_member(X1)|~product(X0,X1,X2)|subgroup2_member(X2))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f34])).
% 30.92/4.34 fof(f36,plain,(
% 30.92/4.34 ![X]: (~subgroup1_member(X)|(![A]: subgroup1_member(multiply(A,multiply(X,inverse(A))))))),
% 30.92/4.34 inference(miniscoping,[status(thm)],[f13])).
% 30.92/4.34 fof(f37,plain,(
% 30.92/4.34 ![X0,X1]: (~subgroup1_member(X0)|subgroup1_member(multiply(X1,multiply(X0,inverse(X1)))))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f36])).
% 30.92/4.34 fof(f38,plain,(
% 30.92/4.34 ![X]: (~subgroup2_member(X)|(![A]: subgroup2_member(multiply(A,multiply(X,inverse(A))))))),
% 30.92/4.34 inference(miniscoping,[status(thm)],[f14])).
% 30.92/4.34 fof(f39,plain,(
% 30.92/4.34 ![X0,X1]: (~subgroup2_member(X0)|subgroup2_member(multiply(X1,multiply(X0,inverse(X1)))))),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f38])).
% 30.92/4.34 fof(f40,plain,(
% 30.92/4.34 ![X0]: (~subgroup1_member(X0)|~subgroup2_member(X0)|X0=identity)),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f15])).
% 30.92/4.34 fof(f41,plain,(
% 30.92/4.34 subgroup1_member(v)),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f16])).
% 30.92/4.34 fof(f42,plain,(
% 30.92/4.34 subgroup2_member(u)),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f17])).
% 30.92/4.34 fof(f43,plain,(
% 30.92/4.34 ~multiply(v,u)=multiply(u,v)),
% 30.92/4.34 inference(cnf_transformation,[status(thm)],[f18])).
% 30.92/4.34 fof(f45,plain,(
% 30.92/4.34 ![X0,X1]: (~product(identity,X0,X1)|X0=X1)),
% 30.92/4.34 inference(resolution,[status(thm)],[f25,f19])).
% 30.92/4.34 fof(f48,plain,(
% 30.92/4.34 ![X0,X1,X2]: (~product(X0,X1,X2)|multiply(X0,X1)=X2)),
% 30.92/4.34 inference(resolution,[status(thm)],[f25,f23])).
% 30.92/4.34 fof(f49,plain,(
% 30.92/4.34 subgroup1_member(inverse(v))),
% 30.92/4.34 inference(resolution,[status(thm)],[f30,f41])).
% 30.92/4.34 fof(f51,plain,(
% 30.92/4.34 subgroup2_member(inverse(u))),
% 30.92/4.34 inference(resolution,[status(thm)],[f33,f42])).
% 30.92/4.34 fof(f54,plain,(
% 30.92/4.34 inverse(identity)=identity),
% 30.92/4.34 inference(resolution,[status(thm)],[f45,f22])).
% 30.92/4.34 fof(f56,plain,(
% 30.92/4.34 ![X0]: (X0=multiply(identity,X0))),
% 30.92/4.34 inference(resolution,[status(thm)],[f45,f23])).
% 30.92/4.34 fof(f59,plain,(
% 30.92/4.34 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(identity,X1,X3)|product(inverse(X0),X2,X3))),
% 30.92/4.34 inference(resolution,[status(thm)],[f27,f21])).
% 30.92/4.34 fof(f63,plain,(
% 30.92/4.34 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~product(multiply(X3,X0),X1,X4)|product(X3,X2,X4))),
% 30.92/4.34 inference(resolution,[status(thm)],[f27,f23])).
% 30.92/4.34 fof(f68,plain,(
% 30.92/4.34 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~product(X3,X2,X4)|product(multiply(X3,X0),X1,X4))),
% 30.92/4.34 inference(resolution,[status(thm)],[f29,f23])).
% 30.92/4.34 fof(f73,plain,(
% 30.92/4.34 ![X0,X1]: (~subgroup1_member(X0)|~subgroup1_member(X1)|subgroup1_member(multiply(X0,X1)))),
% 30.92/4.34 inference(resolution,[status(thm)],[f32,f23])).
% 30.92/4.34 fof(f99,plain,(
% 30.92/4.34 ![X0,X1,X2,X3]: (~product(multiply(X0,X1),X2,X3)|product(X0,multiply(X1,X2),X3))),
% 30.92/4.34 inference(resolution,[status(thm)],[f63,f23])).
% 30.92/4.34 fof(f100,plain,(
% 30.92/4.34 ![X0,X1,X2]: (~product(X0,identity,X1)|product(multiply(X0,inverse(X2)),X2,X1))),
% 30.92/4.34 inference(resolution,[status(thm)],[f68,f21])).
% 30.92/4.34 fof(f102,plain,(
% 30.92/4.34 ![X0,X1,X2]: (~product(X0,identity,X1)|product(multiply(X0,X2),inverse(X2),X1))),
% 30.92/4.34 inference(resolution,[status(thm)],[f68,f22])).
% 30.92/4.34 fof(f104,plain,(
% 30.92/4.34 ![X0,X1,X2,X3]: (~product(X0,multiply(X1,X2),X3)|product(multiply(X0,X1),X2,X3))),
% 30.92/4.34 inference(resolution,[status(thm)],[f68,f23])).
% 30.92/4.34 fof(f118,plain,(
% 30.92/4.34 ![X0,X1]: (~subgroup2_member(X0)|~subgroup2_member(X1)|subgroup2_member(multiply(X0,X1)))),
% 30.92/4.34 inference(resolution,[status(thm)],[f35,f23])).
% 30.92/4.34 fof(f124,plain,(
% 30.92/4.34 ![X0]: (subgroup1_member(multiply(X0,multiply(v,inverse(X0)))))),
% 30.92/4.34 inference(resolution,[status(thm)],[f37,f41])).
% 30.92/4.34 fof(f128,plain,(
% 30.92/4.34 ![X0]: (subgroup2_member(multiply(X0,multiply(inverse(u),inverse(X0)))))),
% 30.92/4.34 inference(resolution,[status(thm)],[f39,f51])).
% 30.92/4.34 fof(f157,plain,(
% 30.92/4.34 ![X0]: (~subgroup2_member(X0)|subgroup2_member(multiply(u,X0)))),
% 30.92/4.34 inference(resolution,[status(thm)],[f118,f42])).
% 30.92/4.34 fof(f159,plain,(
% 30.92/4.34 ![X0,X1]: (~subgroup1_member(X0)|subgroup1_member(multiply(multiply(X1,multiply(v,inverse(X1))),X0)))),
% 30.92/4.34 inference(resolution,[status(thm)],[f124,f73])).
% 30.92/4.34 fof(f297,plain,(
% 30.92/4.34 ![X0,X1,X2]: (~product(identity,X0,X1)|product(inverse(X2),multiply(X2,X0),X1))),
% 30.92/4.34 inference(resolution,[status(thm)],[f59,f23])).
% 30.92/4.34 fof(f316,plain,(
% 30.92/4.34 ![X0,X1,X2]: (product(X0,multiply(X1,X2),multiply(multiply(X0,X1),X2)))),
% 30.92/4.34 inference(resolution,[status(thm)],[f99,f23])).
% 30.92/4.34 fof(f348,plain,(
% 30.92/4.34 ![X0,X1]: (product(multiply(X0,inverse(X1)),X1,X0))),
% 30.92/4.34 inference(resolution,[status(thm)],[f100,f20])).
% 30.92/4.34 fof(f356,plain,(
% 30.92/4.34 ![X0,X1]: (product(multiply(X0,X1),inverse(X1),X0))),
% 30.92/4.34 inference(resolution,[status(thm)],[f102,f20])).
% 30.92/4.34 fof(f374,plain,(
% 30.92/4.34 ![X0,X1]: (multiply(multiply(X0,inverse(X1)),X1)=X0)),
% 30.92/4.34 inference(resolution,[status(thm)],[f348,f48])).
% 30.92/4.34 fof(f400,plain,(
% 30.92/4.34 ![X0,X1]: (multiply(multiply(X0,X1),inverse(X1))=X0)),
% 30.92/4.34 inference(resolution,[status(thm)],[f356,f48])).
% 30.92/4.34 fof(f520,plain,(
% 30.92/4.34 ![X0,X1,X2]: (product(multiply(X0,X1),X2,multiply(X0,multiply(X1,X2))))),
% 30.92/4.34 inference(resolution,[status(thm)],[f104,f23])).
% 30.92/4.34 fof(f588,plain,(
% 30.92/4.34 ![X0]: (subgroup2_member(multiply(u,multiply(X0,multiply(inverse(u),inverse(X0))))))),
% 30.92/4.34 inference(resolution,[status(thm)],[f128,f157])).
% 30.92/4.34 fof(f626,plain,(
% 30.92/4.34 ![X0]: (subgroup1_member(multiply(multiply(X0,multiply(v,inverse(X0))),inverse(v))))),
% 30.92/4.34 inference(resolution,[status(thm)],[f159,f49])).
% 30.92/4.34 fof(f803,plain,(
% 30.92/4.34 ![X0,X1]: (product(inverse(X0),multiply(X0,X1),X1))),
% 30.92/4.34 inference(resolution,[status(thm)],[f297,f19])).
% 30.92/4.34 fof(f822,plain,(
% 30.92/4.34 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 30.92/4.34 inference(resolution,[status(thm)],[f803,f48])).
% 30.92/4.34 fof(f843,plain,(
% 30.92/4.34 ![X0,X1]: (multiply(inverse(multiply(X0,inverse(X1))),X0)=X1)),
% 30.92/4.34 inference(paramodulation,[status(thm)],[f374,f822])).
% 30.92/4.34 fof(f844,plain,(
% 30.92/4.34 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),X0)=inverse(X1))),
% 30.92/4.34 inference(paramodulation,[status(thm)],[f400,f822])).
% 30.92/4.34 fof(f1109,plain,(
% 30.92/4.34 ![X0,X1]: (multiply(X0,inverse(X1))=inverse(multiply(X1,inverse(X0))))),
% 30.92/4.34 inference(paramodulation,[status(thm)],[f843,f400])).
% 30.92/4.34 fof(f1136,plain,(
% 30.92/4.34 ![X0,X1]: (multiply(inverse(X0),inverse(X1))=inverse(multiply(X1,X0)))),
% 30.92/4.34 inference(paramodulation,[status(thm)],[f822,f844])).
% 30.92/4.34 fof(f1625,plain,(
% 30.92/4.34 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 30.92/4.34 inference(resolution,[status(thm)],[f316,f48])).
% 30.92/4.34 fof(f1927,plain,(
% 30.92/4.34 ![X0,X1,X2]: (product(multiply(X0,multiply(X1,inverse(X2))),X2,multiply(X0,X1)))),
% 30.92/4.34 inference(paramodulation,[status(thm)],[f374,f520])).
% 30.92/4.34 fof(f2342,plain,(
% 30.92/4.34 ![X0]: (~subgroup1_member(multiply(u,multiply(X0,multiply(inverse(u),inverse(X0)))))|multiply(u,multiply(X0,multiply(inverse(u),inverse(X0))))=identity)),
% 30.92/4.34 inference(resolution,[status(thm)],[f588,f40])).
% 30.92/4.34 fof(f5212,plain,(
% 30.92/4.34 ![X0]: (subgroup1_member(multiply(X0,multiply(multiply(v,inverse(X0)),inverse(v)))))),
% 30.92/4.34 inference(backward_demodulation,[status(thm)],[f1625,f626])).
% 30.92/4.34 fof(f5350,plain,(
% 30.92/4.34 ![X0]: (subgroup1_member(multiply(X0,multiply(v,multiply(inverse(X0),inverse(v))))))),
% 30.92/4.34 inference(forward_demodulation,[status(thm)],[f1625,f5212])).
% 30.92/4.34 fof(f5351,plain,(
% 30.92/4.34 ![X0]: (subgroup1_member(multiply(X0,multiply(v,inverse(multiply(v,X0))))))),
% 30.92/4.34 inference(forward_demodulation,[status(thm)],[f1136,f5350])).
% 30.92/4.34 fof(f21520,plain,(
% 30.92/4.34 ![X0]: (~subgroup1_member(multiply(u,multiply(X0,inverse(multiply(X0,u)))))|multiply(u,multiply(X0,multiply(inverse(u),inverse(X0))))=identity)),
% 30.92/4.34 inference(forward_demodulation,[status(thm)],[f1136,f2342])).
% 30.92/4.34 fof(f21521,plain,(
% 30.92/4.34 ![X0]: (~subgroup1_member(multiply(u,multiply(X0,inverse(multiply(X0,u)))))|multiply(u,multiply(X0,inverse(multiply(X0,u))))=identity)),
% 30.92/4.37 inference(forward_demodulation,[status(thm)],[f1136,f21520])).
% 30.92/4.37 fof(f21522,plain,(
% 30.92/4.37 multiply(u,multiply(v,inverse(multiply(v,u))))=identity),
% 30.92/4.37 inference(resolution,[status(thm)],[f21521,f5351])).
% 30.92/4.37 fof(f102956,plain,(
% 30.92/4.37 multiply(inverse(identity),u)=inverse(multiply(v,inverse(multiply(v,u))))),
% 30.92/4.37 inference(paramodulation,[status(thm)],[f21522,f844])).
% 30.92/4.37 fof(f103704,plain,(
% 30.92/4.37 multiply(identity,u)=inverse(multiply(v,inverse(multiply(v,u))))),
% 30.92/4.37 inference(forward_demodulation,[status(thm)],[f54,f102956])).
% 30.92/4.37 fof(f103705,plain,(
% 30.92/4.37 u=inverse(multiply(v,inverse(multiply(v,u))))),
% 30.92/4.37 inference(forward_demodulation,[status(thm)],[f56,f103704])).
% 30.92/4.37 fof(f103706,plain,(
% 30.92/4.37 u=multiply(multiply(v,u),inverse(v))),
% 30.92/4.37 inference(forward_demodulation,[status(thm)],[f1109,f103705])).
% 30.92/4.37 fof(f103707,plain,(
% 30.92/4.37 u=multiply(v,multiply(u,inverse(v)))),
% 30.92/4.37 inference(forward_demodulation,[status(thm)],[f1625,f103706])).
% 30.92/4.37 fof(f103824,plain,(
% 30.92/4.37 product(u,v,multiply(v,u))),
% 30.92/4.37 inference(paramodulation,[status(thm)],[f103707,f1927])).
% 30.92/4.37 fof(f104716,plain,(
% 30.92/4.37 multiply(u,v)=multiply(v,u)),
% 30.92/4.37 inference(resolution,[status(thm)],[f103824,f48])).
% 30.92/4.37 fof(f104721,plain,(
% 30.92/4.37 $false),
% 30.92/4.37 inference(forward_subsumption_resolution,[status(thm)],[f104716,f43])).
% 30.92/4.37 % SZS output end CNFRefutation for theBenchmark.p
% 30.92/4.39 % Elapsed time: 3.998115 seconds
% 30.92/4.39 % CPU time: 31.362958 seconds
% 30.92/4.39 % Total memory used: 245.029 MB
% 30.92/4.39 % Net memory used: 215.283 MB
%------------------------------------------------------------------------------