%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP039-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:32 PM UTC 2026
% Result : Unsatisfiable 2.15s 0.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP039-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n003.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Sun Sep 20 19:56:46 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.43 % Drodi V4.1.1
% 2.15/0.78 % Refutation found
% 2.15/0.78 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.15/0.78 % SZS output start CNFRefutation for theBenchmark
% 2.15/0.78 fof(f1,axiom,(
% 2.15/0.78 (![X]: (product(identity,X,X) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f2,axiom,(
% 2.15/0.78 (![X]: (product(X,identity,X) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f3,axiom,(
% 2.15/0.78 (![X]: (product(inverse(X),X,identity) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f4,axiom,(
% 2.15/0.78 (![X]: (product(X,inverse(X),identity) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f5,axiom,(
% 2.15/0.78 (![X,Y]: (product(X,Y,multiply(X,Y)) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f6,axiom,(
% 2.15/0.78 (![X,Y,Z,W]: (( ~ product(X,Y,Z)| ~ product(X,Y,W)| Z = W ) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f7,axiom,(
% 2.15/0.78 (![X,Y,U,Z,V,W]: (( ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W)| product(X,V,W) ) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f8,axiom,(
% 2.15/0.78 (![X,Y,U,Z,V,W]: (( ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(X,V,W)| product(U,Z,W) ) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f9,axiom,(
% 2.15/0.78 (![X]: (( ~ subgroup_member(X)| subgroup_member(inverse(X)) ) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f10,axiom,(
% 2.15/0.78 (![A,B,C]: (( ~ subgroup_member(A)| ~ subgroup_member(B)| ~ product(A,B,C)| subgroup_member(C) ) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f11,axiom,(
% 2.15/0.78 (![A,B]: (( subgroup_member(element_in_O2(A,B))| subgroup_member(B)| subgroup_member(A) ) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f12,axiom,(
% 2.15/0.78 (![A,B]: (( product(A,element_in_O2(A,B),B)| subgroup_member(B)| subgroup_member(A) ) ))),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f13,negated_conjecture,(
% 2.15/0.78 subgroup_member(b) ),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f14,negated_conjecture,(
% 2.15/0.78 product(b,inverse(a),c) ),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f15,negated_conjecture,(
% 2.15/0.78 product(a,c,d) ),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f16,negated_conjecture,(
% 2.15/0.78 ~ subgroup_member(d) ),
% 2.15/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.15/0.78 fof(f17,plain,(
% 2.15/0.78 ![X0]: (product(identity,X0,X0))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f1])).
% 2.15/0.78 fof(f18,plain,(
% 2.15/0.78 ![X0]: (product(X0,identity,X0))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f2])).
% 2.15/0.78 fof(f19,plain,(
% 2.15/0.78 ![X0]: (product(inverse(X0),X0,identity))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f3])).
% 2.15/0.78 fof(f20,plain,(
% 2.15/0.78 ![X0]: (product(X0,inverse(X0),identity))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f4])).
% 2.15/0.78 fof(f21,plain,(
% 2.15/0.78 ![X0,X1]: (product(X0,X1,multiply(X0,X1)))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f5])).
% 2.15/0.78 fof(f22,plain,(
% 2.15/0.78 ![Z,W]: ((![X,Y]: (~product(X,Y,Z)|~product(X,Y,W)))|Z=W)),
% 2.15/0.78 inference(miniscoping,[status(thm)],[f6])).
% 2.15/0.78 fof(f23,plain,(
% 2.15/0.78 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|X2=X3)),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f22])).
% 2.15/0.78 fof(f24,plain,(
% 2.15/0.78 ![X,V,W]: ((![U,Z]: ((![Y]: (~product(X,Y,U)|~product(Y,Z,V)))|~product(U,Z,W)))|product(X,V,W))),
% 2.15/0.78 inference(miniscoping,[status(thm)],[f7])).
% 2.15/0.78 fof(f25,plain,(
% 2.15/0.78 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X1,X3,X4)|~product(X2,X3,X5)|product(X0,X4,X5))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f24])).
% 2.15/0.78 fof(f26,plain,(
% 2.15/0.78 ![U,Z,W]: ((![X,V]: ((![Y]: (~product(X,Y,U)|~product(Y,Z,V)))|~product(X,V,W)))|product(U,Z,W))),
% 2.15/0.78 inference(miniscoping,[status(thm)],[f8])).
% 2.15/0.78 fof(f27,plain,(
% 2.15/0.78 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X1,X3,X4)|~product(X0,X4,X5)|product(X2,X3,X5))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f26])).
% 2.15/0.78 fof(f28,plain,(
% 2.15/0.78 ![X0]: (~subgroup_member(X0)|subgroup_member(inverse(X0)))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f9])).
% 2.15/0.78 fof(f29,plain,(
% 2.15/0.78 ![C]: ((![A,B]: ((~subgroup_member(A)|~subgroup_member(B))|~product(A,B,C)))|subgroup_member(C))),
% 2.15/0.78 inference(miniscoping,[status(thm)],[f10])).
% 2.15/0.78 fof(f30,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~subgroup_member(X0)|~subgroup_member(X1)|~product(X0,X1,X2)|subgroup_member(X2))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f29])).
% 2.15/0.78 fof(f31,plain,(
% 2.15/0.78 ![A]: ((![B]: (subgroup_member(element_in_O2(A,B))|subgroup_member(B)))|subgroup_member(A))),
% 2.15/0.78 inference(miniscoping,[status(thm)],[f11])).
% 2.15/0.78 fof(f32,plain,(
% 2.15/0.78 ![X0,X1]: (subgroup_member(element_in_O2(X0,X1))|subgroup_member(X1)|subgroup_member(X0))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f31])).
% 2.15/0.78 fof(f33,plain,(
% 2.15/0.78 ![A]: ((![B]: (product(A,element_in_O2(A,B),B)|subgroup_member(B)))|subgroup_member(A))),
% 2.15/0.78 inference(miniscoping,[status(thm)],[f12])).
% 2.15/0.78 fof(f34,plain,(
% 2.15/0.78 ![X0,X1]: (product(X0,element_in_O2(X0,X1),X1)|subgroup_member(X1)|subgroup_member(X0))),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f33])).
% 2.15/0.78 fof(f35,plain,(
% 2.15/0.78 subgroup_member(b)),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f13])).
% 2.15/0.78 fof(f36,plain,(
% 2.15/0.78 product(b,inverse(a),c)),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f14])).
% 2.15/0.78 fof(f37,plain,(
% 2.15/0.78 product(a,c,d)),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f15])).
% 2.15/0.78 fof(f38,plain,(
% 2.15/0.78 ~subgroup_member(d)),
% 2.15/0.78 inference(cnf_transformation,[status(thm)],[f16])).
% 2.15/0.78 fof(f39,plain,(
% 2.15/0.78 ![X0,X1]: (~product(inverse(X0),X0,X1)|identity=X1)),
% 2.15/0.78 inference(resolution,[status(thm)],[f23,f19])).
% 2.15/0.78 fof(f40,plain,(
% 2.15/0.78 ![X0]: (~product(a,c,X0)|d=X0)),
% 2.15/0.78 inference(resolution,[status(thm)],[f23,f37])).
% 2.15/0.78 fof(f43,plain,(
% 2.15/0.78 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(identity,X1,X3)|product(inverse(X0),X2,X3))),
% 2.15/0.78 inference(resolution,[status(thm)],[f25,f19])).
% 2.15/0.78 fof(f44,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(c,X0,X1)|~product(d,X0,X2)|product(a,X1,X2))),
% 2.15/0.78 inference(resolution,[status(thm)],[f25,f37])).
% 2.15/0.78 fof(f45,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(inverse(a),X0,X1)|~product(c,X0,X2)|product(b,X1,X2))),
% 2.15/0.78 inference(resolution,[status(thm)],[f25,f36])).
% 2.15/0.78 fof(f46,plain,(
% 2.15/0.78 ![X0,X1,X2,X3]: (~product(inverse(X0),X1,X2)|~product(identity,X1,X3)|product(X0,X2,X3))),
% 2.15/0.78 inference(resolution,[status(thm)],[f25,f20])).
% 2.15/0.78 fof(f48,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(c,X0,X1)|~product(a,X1,X2)|product(d,X0,X2))),
% 2.15/0.78 inference(resolution,[status(thm)],[f27,f37])).
% 2.15/0.78 fof(f49,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(inverse(a),X0,X1)|~product(b,X1,X2)|product(c,X0,X2))),
% 2.15/0.78 inference(resolution,[status(thm)],[f27,f36])).
% 2.15/0.78 fof(f50,plain,(
% 2.15/0.78 ![X0,X1,X2,X3]: (~product(inverse(X0),X1,X2)|~product(X0,X2,X3)|product(identity,X1,X3))),
% 2.15/0.78 inference(resolution,[status(thm)],[f27,f20])).
% 2.15/0.78 fof(f52,plain,(
% 2.15/0.78 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|product(identity,X2,X3))),
% 2.15/0.78 inference(resolution,[status(thm)],[f17,f25])).
% 2.15/0.78 fof(f56,plain,(
% 2.15/0.78 ![X0,X1]: (~product(X0,identity,X1)|X0=X1)),
% 2.15/0.78 inference(resolution,[status(thm)],[f18,f23])).
% 2.15/0.78 fof(f57,plain,(
% 2.15/0.78 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~product(X3,X2,X4)|product(multiply(X3,X0),X1,X4))),
% 2.15/0.78 inference(resolution,[status(thm)],[f21,f27])).
% 2.15/0.78 fof(f58,plain,(
% 2.15/0.78 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~product(multiply(X3,X0),X1,X4)|product(X3,X2,X4))),
% 2.15/0.78 inference(resolution,[status(thm)],[f21,f25])).
% 2.15/0.78 fof(f59,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(X0,X1,X2)|multiply(X0,X1)=X2)),
% 2.15/0.78 inference(resolution,[status(thm)],[f21,f23])).
% 2.15/0.78 fof(f61,plain,(
% 2.15/0.78 ![X0]: (~subgroup_member(identity)|~subgroup_member(X0)|subgroup_member(X0))),
% 2.15/0.78 inference(resolution,[status(thm)],[f30,f17])).
% 2.15/0.78 fof(f63,plain,(
% 2.15/0.78 ~subgroup_member(a)|~subgroup_member(c)|subgroup_member(d)),
% 2.15/0.78 inference(resolution,[status(thm)],[f30,f37])).
% 2.15/0.78 fof(f64,plain,(
% 2.15/0.78 ~subgroup_member(b)|~subgroup_member(inverse(a))|subgroup_member(c)),
% 2.15/0.78 inference(resolution,[status(thm)],[f30,f36])).
% 2.15/0.78 fof(f67,plain,(
% 2.15/0.78 ![X0,X1]: (~subgroup_member(X0)|~subgroup_member(X1)|subgroup_member(multiply(X0,X1)))),
% 2.15/0.78 inference(resolution,[status(thm)],[f30,f21])).
% 2.15/0.78 fof(f68,definition,(
% 2.15/0.78 sQ0_spl <=> (subgroup_member(identity))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f71,definition,(
% 2.15/0.78 ![X0]: (sQ1_spl <=> (~subgroup_member(X0)|subgroup_member(X0)))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f74,plain,(
% 2.15/0.78 ~sQ0_spl|sQ1_spl),
% 2.15/0.78 inference(split_clause,[status(thm)],[f61,f68,f71])).
% 2.15/0.78 fof(f75,definition,(
% 2.15/0.78 ![X0]: (sQ2_spl <=> (~subgroup_member(inverse(X0))|~subgroup_member(X0)))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f76,plain,(
% 2.15/0.78 ![X0]: (~subgroup_member(inverse(X0))|~subgroup_member(X0)|~sQ2_spl)),
% 2.15/0.78 inference(component_clause,[status(thm)],[f75])).
% 2.15/0.78 fof(f79,definition,(
% 2.15/0.78 sQ3_spl <=> (subgroup_member(a))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f80,plain,(
% 2.15/0.78 subgroup_member(a)|~sQ3_spl),
% 2.15/0.78 inference(component_clause,[status(thm)],[f79])).
% 2.15/0.78 fof(f81,plain,(
% 2.15/0.78 ~subgroup_member(a)|sQ3_spl),
% 2.15/0.78 inference(component_clause,[status(thm)],[f79])).
% 2.15/0.78 fof(f82,definition,(
% 2.15/0.78 sQ4_spl <=> (subgroup_member(c))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f83,plain,(
% 2.15/0.78 subgroup_member(c)|~sQ4_spl),
% 2.15/0.78 inference(component_clause,[status(thm)],[f82])).
% 2.15/0.78 fof(f85,definition,(
% 2.15/0.78 sQ5_spl <=> (subgroup_member(d))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f86,plain,(
% 2.15/0.78 subgroup_member(d)|~sQ5_spl),
% 2.15/0.78 inference(component_clause,[status(thm)],[f85])).
% 2.15/0.78 fof(f88,plain,(
% 2.15/0.78 ~sQ3_spl|~sQ4_spl|sQ5_spl),
% 2.15/0.78 inference(split_clause,[status(thm)],[f63,f79,f82,f85])).
% 2.15/0.78 fof(f89,definition,(
% 2.15/0.78 sQ6_spl <=> (subgroup_member(b))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f91,plain,(
% 2.15/0.78 ~subgroup_member(b)|sQ6_spl),
% 2.15/0.78 inference(component_clause,[status(thm)],[f89])).
% 2.15/0.78 fof(f92,definition,(
% 2.15/0.78 sQ7_spl <=> (subgroup_member(inverse(a)))),
% 2.15/0.78 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 2.15/0.78 fof(f93,plain,(
% 2.15/0.78 subgroup_member(inverse(a))|~sQ7_spl),
% 2.15/0.78 inference(component_clause,[status(thm)],[f92])).
% 2.15/0.78 fof(f95,plain,(
% 2.15/0.78 ~sQ6_spl|~sQ7_spl|sQ4_spl),
% 2.15/0.78 inference(split_clause,[status(thm)],[f64,f89,f92,f82])).
% 2.15/0.78 fof(f98,plain,(
% 2.15/0.78 ![X0]: (~subgroup_member(X0)|~sQ2_spl)),
% 2.15/0.78 inference(forward_subsumption_resolution,[status(thm)],[f76,f28])).
% 2.15/0.78 fof(f99,plain,(
% 2.15/0.78 $false|sQ6_spl),
% 2.15/0.78 inference(forward_subsumption_resolution,[status(thm)],[f91,f35])).
% 2.15/0.78 fof(f100,plain,(
% 2.15/0.78 sQ6_spl),
% 2.15/0.78 inference(contradiction_clause,[status(thm)],[f99])).
% 2.15/0.78 fof(f101,plain,(
% 2.15/0.78 $false|~sQ5_spl),
% 2.15/0.78 inference(forward_subsumption_resolution,[status(thm)],[f86,f38])).
% 2.15/0.78 fof(f102,plain,(
% 2.15/0.78 ~sQ5_spl),
% 2.15/0.78 inference(contradiction_clause,[status(thm)],[f101])).
% 2.15/0.78 fof(f103,plain,(
% 2.15/0.78 ![X0,X1]: (subgroup_member(X0)|subgroup_member(X1)|subgroup_member(inverse(element_in_O2(X1,X0))))),
% 2.15/0.78 inference(resolution,[status(thm)],[f32,f28])).
% 2.15/0.78 fof(f105,plain,(
% 2.15/0.78 ![X0,X1,X2,X3,X4]: (subgroup_member(X0)|subgroup_member(X1)|~product(element_in_O2(X1,X0),X2,X3)|~product(X1,X3,X4)|product(X0,X2,X4))),
% 2.15/0.78 inference(resolution,[status(thm)],[f34,f27])).
% 2.15/0.78 fof(f106,plain,(
% 2.15/0.78 ![X0,X1,X2,X3,X4]: (subgroup_member(X0)|subgroup_member(X1)|~product(element_in_O2(X1,X0),X2,X3)|~product(X0,X2,X4)|product(X1,X3,X4))),
% 2.15/0.78 inference(resolution,[status(thm)],[f34,f25])).
% 2.15/0.78 fof(f107,plain,(
% 2.15/0.78 ![X0,X1,X2]: (subgroup_member(X0)|subgroup_member(X1)|~product(X1,element_in_O2(X1,X0),X2)|X0=X2)),
% 2.15/0.78 inference(resolution,[status(thm)],[f34,f23])).
% 2.15/0.78 fof(f118,plain,(
% 2.15/0.78 ![X0,X1]: (~product(d,X0,X1)|product(a,multiply(c,X0),X1))),
% 2.15/0.78 inference(resolution,[status(thm)],[f44,f21])).
% 2.15/0.78 fof(f125,plain,(
% 2.15/0.78 $false|~sQ2_spl),
% 2.15/0.78 inference(backward_subsumption_resolution,[status(thm)],[f35,f98])).
% 2.15/0.78 fof(f128,plain,(
% 2.15/0.78 ~sQ2_spl),
% 2.15/0.78 inference(contradiction_clause,[status(thm)],[f125])).
% 2.15/0.78 fof(f156,plain,(
% 2.15/0.78 ![X0,X1]: (~product(identity,X0,X1)|product(inverse(inverse(X0)),identity,X1))),
% 2.15/0.78 inference(resolution,[status(thm)],[f43,f19])).
% 2.15/0.78 fof(f157,plain,(
% 2.15/0.78 ![X0]: (~product(identity,c,X0)|product(inverse(a),d,X0))),
% 2.15/0.78 inference(resolution,[status(thm)],[f43,f37])).
% 2.15/0.78 fof(f159,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(identity,element_in_O2(X0,X1),X2)|product(inverse(X0),X1,X2)|subgroup_member(X1)|subgroup_member(X0))),
% 2.15/0.78 inference(resolution,[status(thm)],[f43,f34])).
% 2.15/0.78 fof(f162,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(identity,X0,X1)|product(inverse(X2),multiply(X2,X0),X1))),
% 2.15/0.78 inference(resolution,[status(thm)],[f43,f21])).
% 2.15/0.78 fof(f167,plain,(
% 2.15/0.78 ![X0,X1]: (~product(c,X0,X1)|product(b,multiply(inverse(a),X0),X1))),
% 2.15/0.78 inference(resolution,[status(thm)],[f45,f21])).
% 2.15/0.78 fof(f173,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(identity,element_in_O2(inverse(X0),X1),X2)|product(X0,X1,X2)|subgroup_member(X1)|subgroup_member(inverse(X0)))),
% 2.15/0.78 inference(resolution,[status(thm)],[f46,f34])).
% 2.15/0.78 fof(f177,plain,(
% 2.15/0.78 subgroup_member(inverse(c))|~sQ4_spl),
% 2.15/0.78 inference(resolution,[status(thm)],[f83,f28])).
% 2.15/0.78 fof(f180,plain,(
% 2.15/0.78 ![X0]: (~product(a,identity,X0)|product(d,inverse(c),X0))),
% 2.15/0.78 inference(resolution,[status(thm)],[f48,f20])).
% 2.15/0.78 fof(f181,plain,(
% 2.15/0.78 ![X0,X1]: (~product(a,multiply(c,X0),X1)|product(d,X0,X1))),
% 2.15/0.78 inference(resolution,[status(thm)],[f48,f21])).
% 2.15/0.78 fof(f186,plain,(
% 2.15/0.78 ![X0]: (~product(b,identity,X0)|product(c,a,X0))),
% 2.15/0.78 inference(resolution,[status(thm)],[f49,f19])).
% 2.15/0.78 fof(f209,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(X0,X1,X2)|product(identity,element_in_O2(inverse(X0),X1),X2)|subgroup_member(X1)|subgroup_member(inverse(X0)))),
% 2.15/0.78 inference(resolution,[status(thm)],[f50,f34])).
% 2.15/0.78 fof(f226,plain,(
% 2.15/0.78 ![X0,X1,X2]: (~product(X0,element_in_O2(X0,X1),X2)|product(identity,X1,X2)|subgroup_member(X1)|subgroup_member(X0))),
% 2.15/0.78 inference(resolution,[status(thm)],[f52,f34])).
% 2.15/0.78 fof(f265,plain,(
% 2.15/0.78 ![X0,X1]: (~product(X0,d,X1)|product(multiply(X0,a),c,X1))),
% 2.15/0.78 inference(resolution,[status(thm)],[f57,f37])).
% 2.15/0.78 fof(f267,plain,(
% 2.15/0.78 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|product(multiply(X0,X3),element_in_O2(X3,X1),X2)|subgroup_member(X1)|subgroup_member(X3))),
% 2.15/0.78 inference(resolution,[status(thm)],[f57,f34])).
% 2.15/0.78 fof(f275,plain,(
% 2.15/0.78 ![X0,X1,X2,X3]: (~product(multiply(X0,X1),element_in_O2(X1,X2),X3)|product(X0,X2,X3)|subgroup_member(X2)|subgroup_member(X1))),
% 2.15/0.78 inference(resolution,[status(thm)],[f58,f34])).
% 2.15/0.78 fof(f300,plain,(
% 2.15/0.78 ![X0]: (~subgroup_member(X0)|subgroup_member(multiply(b,X0)))),
% 2.15/0.78 inference(resolution,[status(thm)],[f67,f35])).
% 2.15/0.78 fof(f304,plain,(
% 2.15/0.78 ![X0,X1,X2]: (subgroup_member(X0)|subgroup_member(X1)|~product(X1,element_in_O2(X1,X0),X2)|product(X0,identity,X2))),
% 2.15/0.79 inference(resolution,[status(thm)],[f105,f18])).
% 2.15/0.79 fof(f305,plain,(
% 2.15/0.79 ![X0,X1,X2]: (subgroup_member(X0)|subgroup_member(X1)|~product(X1,identity,X2)|product(X0,inverse(element_in_O2(X1,X0)),X2))),
% 2.15/0.79 inference(resolution,[status(thm)],[f105,f20])).
% 2.15/0.79 fof(f306,plain,(
% 2.15/0.79 ![X0,X1,X2,X3]: (subgroup_member(X0)|subgroup_member(X1)|~product(X1,multiply(element_in_O2(X1,X0),X2),X3)|product(X0,X2,X3))),
% 2.15/0.79 inference(resolution,[status(thm)],[f105,f21])).
% 2.15/0.79 fof(f318,plain,(
% 2.15/0.79 ![X0,X1,X2]: (subgroup_member(X0)|subgroup_member(X1)|~product(X0,identity,X2)|product(X1,element_in_O2(X1,X0),X2))),
% 2.15/0.79 inference(resolution,[status(thm)],[f106,f18])).
% 2.15/0.79 fof(f319,plain,(
% 2.15/0.79 ![X0,X1,X2]: (subgroup_member(X0)|subgroup_member(X1)|~product(X0,inverse(element_in_O2(X1,X0)),X2)|product(X1,identity,X2))),
% 2.15/0.79 inference(resolution,[status(thm)],[f106,f20])).
% 2.15/0.79 fof(f320,plain,(
% 2.15/0.79 ![X0,X1,X2,X3]: (subgroup_member(X0)|subgroup_member(X1)|~product(X0,X2,X3)|product(X1,multiply(element_in_O2(X1,X0),X2),X3))),
% 2.15/0.79 inference(resolution,[status(thm)],[f106,f21])).
% 2.15/0.79 fof(f335,plain,(
% 2.15/0.79 ![X0]: (product(a,multiply(c,element_in_O2(d,X0)),X0)|subgroup_member(X0)|subgroup_member(d))),
% 2.15/0.79 inference(resolution,[status(thm)],[f118,f34])).
% 2.15/0.79 fof(f339,definition,(
% 2.15/0.79 ![X0]: (sQ17_spl <=> (product(a,multiply(c,element_in_O2(d,X0)),X0)|subgroup_member(X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f340,plain,(
% 2.15/0.79 ![X0]: (product(a,multiply(c,element_in_O2(d,X0)),X0)|subgroup_member(X0)|~sQ17_spl)),
% 2.15/0.79 inference(component_clause,[status(thm)],[f339])).
% 2.15/0.79 fof(f342,plain,(
% 2.15/0.79 sQ17_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f335,f339,f85])).
% 2.15/0.79 fof(f344,plain,(
% 2.15/0.79 ![X0]: (product(inverse(inverse(X0)),identity,X0))),
% 2.15/0.79 inference(resolution,[status(thm)],[f156,f17])).
% 2.15/0.79 fof(f359,plain,(
% 2.15/0.79 product(inverse(a),d,c)),
% 2.15/0.79 inference(resolution,[status(thm)],[f157,f17])).
% 2.15/0.79 fof(f376,plain,(
% 2.15/0.79 ![X0,X1]: (product(inverse(X0),X1,element_in_O2(X0,X1))|subgroup_member(X1)|subgroup_member(X0))),
% 2.15/0.79 inference(resolution,[status(thm)],[f159,f17])).
% 2.15/0.79 fof(f394,plain,(
% 2.15/0.79 ![X0,X1]: (product(inverse(X0),multiply(X0,X1),X1))),
% 2.15/0.79 inference(resolution,[status(thm)],[f162,f17])).
% 2.15/0.79 fof(f421,plain,(
% 2.15/0.79 ![X0,X1]: (subgroup_member(multiply(b,element_in_O2(X0,X1)))|subgroup_member(X1)|subgroup_member(X0))),
% 2.15/0.79 inference(resolution,[status(thm)],[f300,f32])).
% 2.15/0.79 fof(f424,plain,(
% 2.15/0.79 ![X0,X1]: (subgroup_member(multiply(b,inverse(element_in_O2(X0,X1))))|subgroup_member(X1)|subgroup_member(X0))),
% 2.15/0.79 inference(resolution,[status(thm)],[f300,f103])).
% 2.15/0.79 fof(f434,plain,(
% 2.15/0.79 ![X0]: (product(b,multiply(inverse(a),X0),multiply(c,X0)))),
% 2.15/0.79 inference(resolution,[status(thm)],[f167,f21])).
% 2.15/0.79 fof(f452,plain,(
% 2.15/0.79 ![X0,X1]: (product(X0,X1,element_in_O2(inverse(X0),X1))|subgroup_member(X1)|subgroup_member(inverse(X0)))),
% 2.15/0.79 inference(resolution,[status(thm)],[f173,f17])).
% 2.15/0.79 fof(f459,definition,(
% 2.15/0.79 sQ24_spl <=> (subgroup_member(inverse(identity)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f499,plain,(
% 2.15/0.79 product(d,inverse(c),a)),
% 2.15/0.79 inference(resolution,[status(thm)],[f180,f18])).
% 2.15/0.79 fof(f502,plain,(
% 2.15/0.79 ![X0]: (product(d,X0,multiply(a,multiply(c,X0))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f181,f21])).
% 2.15/0.79 fof(f509,plain,(
% 2.15/0.79 product(c,a,b)),
% 2.15/0.79 inference(resolution,[status(thm)],[f186,f18])).
% 2.15/0.79 fof(f519,plain,(
% 2.15/0.79 multiply(c,a)=b),
% 2.15/0.79 inference(resolution,[status(thm)],[f509,f59])).
% 2.15/0.79 fof(f567,plain,(
% 2.15/0.79 ![X0]: (inverse(inverse(X0))=X0)),
% 2.15/0.79 inference(resolution,[status(thm)],[f344,f56])).
% 2.15/0.79 fof(f575,plain,(
% 2.15/0.79 ![X0]: (~subgroup_member(inverse(inverse(X0)))|~subgroup_member(identity)|subgroup_member(X0))),
% 2.15/0.79 inference(resolution,[status(thm)],[f344,f30])).
% 2.15/0.79 fof(f581,definition,(
% 2.15/0.79 ![X0]: (sQ31_spl <=> (~subgroup_member(inverse(inverse(X0)))|subgroup_member(X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f584,plain,(
% 2.15/0.79 sQ31_spl|~sQ0_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f575,f581,f68])).
% 2.15/0.79 fof(f648,plain,(
% 2.15/0.79 multiply(inverse(a),d)=c),
% 2.15/0.79 inference(resolution,[status(thm)],[f359,f59])).
% 2.15/0.79 fof(f697,definition,(
% 2.15/0.79 sQ36_spl <=> (subgroup_member(inverse(c)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f699,plain,(
% 2.15/0.79 ~subgroup_member(inverse(c))|sQ36_spl),
% 2.15/0.79 inference(component_clause,[status(thm)],[f697])).
% 2.15/0.79 fof(f733,plain,(
% 2.15/0.79 subgroup_member(inverse(inverse(a)))|~sQ7_spl),
% 2.15/0.79 inference(resolution,[status(thm)],[f93,f28])).
% 2.15/0.79 fof(f735,plain,(
% 2.15/0.79 subgroup_member(a)|~sQ7_spl),
% 2.15/0.79 inference(forward_demodulation,[status(thm)],[f567,f733])).
% 2.15/0.79 fof(f736,plain,(
% 2.15/0.79 $false|sQ3_spl|~sQ7_spl),
% 2.15/0.79 inference(forward_subsumption_resolution,[status(thm)],[f735,f81])).
% 2.15/0.79 fof(f737,plain,(
% 2.15/0.79 sQ3_spl|~sQ7_spl),
% 2.15/0.79 inference(contradiction_clause,[status(thm)],[f736])).
% 2.15/0.79 fof(f809,plain,(
% 2.15/0.79 product(inverse(c),b,a)),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f519,f394])).
% 2.15/0.79 fof(f994,plain,(
% 2.15/0.79 ![X0]: (product(multiply(inverse(a),X0),element_in_O2(X0,d),c)|subgroup_member(d)|subgroup_member(X0))),
% 2.15/0.79 inference(resolution,[status(thm)],[f267,f359])).
% 2.15/0.79 fof(f1008,definition,(
% 2.15/0.79 ![X0]: (sQ49_spl <=> (product(multiply(inverse(a),X0),element_in_O2(X0,d),c)|subgroup_member(X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f1011,plain,(
% 2.15/0.79 sQ49_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f994,f1008,f85])).
% 2.15/0.79 fof(f1286,plain,(
% 2.15/0.79 ![X0,X1]: (~product(c,element_in_O2(d,X0),X1)|product(inverse(a),X0,X1)|subgroup_member(X0)|subgroup_member(d))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f648,f275])).
% 2.15/0.79 fof(f1292,definition,(
% 2.15/0.79 ![X0,X1]: (sQ55_spl <=> (~product(c,element_in_O2(d,X0),X1)|product(inverse(a),X0,X1)|subgroup_member(X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f1295,plain,(
% 2.15/0.79 sQ55_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f1286,f1292,f85])).
% 2.15/0.79 fof(f1378,plain,(
% 2.15/0.79 ~subgroup_member(inverse(c))|~subgroup_member(b)|subgroup_member(a)),
% 2.15/0.79 inference(resolution,[status(thm)],[f809,f30])).
% 2.15/0.79 fof(f1393,plain,(
% 2.15/0.79 ~sQ36_spl|~sQ6_spl|sQ3_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f1378,f697,f89,f79])).
% 2.15/0.79 fof(f1396,plain,(
% 2.15/0.79 $false|~sQ4_spl|sQ36_spl),
% 2.15/0.79 inference(forward_subsumption_resolution,[status(thm)],[f699,f177])).
% 2.15/0.79 fof(f1397,plain,(
% 2.15/0.79 ~sQ4_spl|sQ36_spl),
% 2.15/0.79 inference(contradiction_clause,[status(thm)],[f1396])).
% 2.15/0.79 fof(f1406,plain,(
% 2.15/0.79 subgroup_member(inverse(a))|~sQ3_spl),
% 2.15/0.79 inference(resolution,[status(thm)],[f80,f28])).
% 2.15/0.79 fof(f1407,plain,(
% 2.15/0.79 sQ7_spl|~sQ3_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f1406,f92,f79])).
% 2.15/0.79 fof(f1450,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(X0)|product(X0,multiply(element_in_O2(X0,d),inverse(c)),a))),
% 2.15/0.79 inference(resolution,[status(thm)],[f320,f499])).
% 2.15/0.79 fof(f1464,definition,(
% 2.15/0.79 ![X0]: (sQ63_spl <=> (subgroup_member(X0)|product(X0,multiply(element_in_O2(X0,d),inverse(c)),a)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f1467,plain,(
% 2.15/0.79 sQ5_spl|sQ63_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f1450,f85,f1464])).
% 2.15/0.79 fof(f1511,definition,(
% 2.15/0.79 sQ71_spl <=> (subgroup_member(inverse(d)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f1512,plain,(
% 2.15/0.79 subgroup_member(inverse(d))|~sQ71_spl),
% 2.15/0.79 inference(component_clause,[status(thm)],[f1511])).
% 2.15/0.79 fof(f2031,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(X0)|subgroup_member(X0)|identity=element_in_O2(X0,X0))),
% 2.15/0.79 inference(resolution,[status(thm)],[f376,f39])).
% 2.15/0.79 fof(f2033,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(X0)|product(multiply(inverse(X0),a),c,element_in_O2(X0,d)))),
% 2.15/0.79 inference(resolution,[status(thm)],[f376,f265])).
% 2.15/0.79 fof(f2082,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(X0)|identity=element_in_O2(X0,X0))),
% 2.15/0.79 inference(duplicate_literals_removal,[status(thm)],[f2031])).
% 2.15/0.79 fof(f2087,definition,(
% 2.15/0.79 ![X0]: (sQ101_spl <=> (subgroup_member(X0)|product(multiply(inverse(X0),a),c,element_in_O2(X0,d))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2090,plain,(
% 2.15/0.79 sQ5_spl|sQ101_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2033,f85,f2087])).
% 2.15/0.79 fof(f2139,plain,(
% 2.15/0.79 identity=element_in_O2(d,d)),
% 2.15/0.79 inference(resolution,[status(thm)],[f2082,f38])).
% 2.15/0.79 fof(f2278,definition,(
% 2.15/0.79 sQ131_spl <=> (subgroup_member(multiply(b,identity)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2294,definition,(
% 2.15/0.79 sQ132_spl <=> (subgroup_member(multiply(b,inverse(identity))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2349,plain,(
% 2.15/0.79 ![X0]: (~subgroup_member(b)|~subgroup_member(multiply(inverse(a),X0))|subgroup_member(multiply(c,X0)))),
% 2.15/0.79 inference(resolution,[status(thm)],[f434,f30])).
% 2.15/0.79 fof(f2379,definition,(
% 2.15/0.79 ![X0]: (sQ140_spl <=> (~subgroup_member(multiply(inverse(a),X0))|subgroup_member(multiply(c,X0))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2382,plain,(
% 2.15/0.79 ~sQ6_spl|sQ140_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2349,f89,f2379])).
% 2.15/0.79 fof(f2402,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(X0)|subgroup_member(inverse(d))|product(a,multiply(c,X0),element_in_O2(inverse(d),X0)))),
% 2.15/0.79 inference(resolution,[status(thm)],[f452,f118])).
% 2.15/0.79 fof(f2436,plain,(
% 2.15/0.79 subgroup_member(c)|subgroup_member(inverse(a))|d=element_in_O2(inverse(a),c)),
% 2.15/0.79 inference(resolution,[status(thm)],[f452,f40])).
% 2.15/0.79 fof(f2449,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(inverse(X0))|product(multiply(X0,a),c,element_in_O2(inverse(X0),d)))),
% 2.15/0.79 inference(resolution,[status(thm)],[f452,f265])).
% 2.15/0.79 fof(f2507,definition,(
% 2.15/0.79 ![X0]: (sQ147_spl <=> (subgroup_member(X0)|product(a,multiply(c,X0),element_in_O2(inverse(d),X0))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2510,plain,(
% 2.15/0.79 sQ147_spl|sQ71_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2402,f2507,f1511])).
% 2.15/0.79 fof(f2640,definition,(
% 2.15/0.79 sQ180_spl <=> (d=element_in_O2(inverse(a),c))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2641,plain,(
% 2.15/0.79 d=element_in_O2(inverse(a),c)|~sQ180_spl),
% 2.15/0.79 inference(component_clause,[status(thm)],[f2640])).
% 2.15/0.79 fof(f2643,plain,(
% 2.15/0.79 sQ4_spl|sQ7_spl|sQ180_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2436,f82,f92,f2640])).
% 2.15/0.79 fof(f2683,definition,(
% 2.15/0.79 ![X0]: (sQ187_spl <=> (subgroup_member(inverse(X0))|product(multiply(X0,a),c,element_in_O2(inverse(X0),d))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2686,plain,(
% 2.15/0.79 sQ5_spl|sQ187_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2449,f85,f2683])).
% 2.15/0.79 fof(f2733,plain,(
% 2.15/0.79 subgroup_member(inverse(inverse(d)))|~sQ71_spl),
% 2.15/0.79 inference(resolution,[status(thm)],[f1512,f28])).
% 2.15/0.79 fof(f2734,plain,(
% 2.15/0.79 subgroup_member(d)|~sQ71_spl),
% 2.15/0.79 inference(forward_demodulation,[status(thm)],[f567,f2733])).
% 2.15/0.79 fof(f2735,plain,(
% 2.15/0.79 $false|~sQ71_spl),
% 2.15/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2734,f38])).
% 2.15/0.79 fof(f2736,plain,(
% 2.15/0.79 ~sQ71_spl),
% 2.15/0.79 inference(contradiction_clause,[status(thm)],[f2735])).
% 2.15/0.79 fof(f2743,plain,(
% 2.15/0.79 ![X0]: (product(identity,X0,multiply(a,multiply(c,element_in_O2(d,X0))))|subgroup_member(X0)|subgroup_member(d))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f226])).
% 2.15/0.79 fof(f2744,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(X0)|subgroup_member(d)|product(X0,identity,multiply(a,multiply(c,element_in_O2(d,X0)))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f304])).
% 2.15/0.79 fof(f2745,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(X0)|subgroup_member(d)|X0=multiply(a,multiply(c,element_in_O2(d,X0))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f107])).
% 2.15/0.79 fof(f2746,plain,(
% 2.15/0.79 ![X0,X1]: (subgroup_member(X0)|subgroup_member(d)|product(X0,X1,multiply(a,multiply(c,multiply(element_in_O2(d,X0),X1)))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f306])).
% 2.15/0.79 fof(f2749,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(X0)|product(X0,element_in_O2(X0,d),multiply(a,multiply(c,identity))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f318])).
% 2.15/0.79 fof(f2750,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(X0)|subgroup_member(d)|product(X0,inverse(element_in_O2(d,X0)),multiply(a,multiply(c,identity))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f305])).
% 2.15/0.79 fof(f2755,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(X0)|product(X0,identity,multiply(a,multiply(c,inverse(element_in_O2(X0,d))))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f319])).
% 2.15/0.79 fof(f2758,plain,(
% 2.15/0.79 ![X0]: (product(identity,element_in_O2(inverse(d),X0),multiply(a,multiply(c,X0)))|subgroup_member(X0)|subgroup_member(inverse(d)))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f209])).
% 2.15/0.79 fof(f2759,plain,(
% 2.15/0.79 ![X0,X1]: (subgroup_member(d)|subgroup_member(X0)|product(X0,multiply(element_in_O2(X0,d),X1),multiply(a,multiply(c,X1))))),
% 2.15/0.79 inference(resolution,[status(thm)],[f502,f320])).
% 2.15/0.79 fof(f2782,definition,(
% 2.15/0.79 ![X0]: (sQ194_spl <=> (product(identity,X0,multiply(a,multiply(c,element_in_O2(d,X0))))|subgroup_member(X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2785,plain,(
% 2.15/0.79 sQ194_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2743,f2782,f85])).
% 2.15/0.79 fof(f2786,definition,(
% 2.15/0.79 ![X0]: (sQ195_spl <=> (subgroup_member(X0)|product(X0,identity,multiply(a,multiply(c,element_in_O2(d,X0))))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2789,plain,(
% 2.15/0.79 sQ195_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2744,f2786,f85])).
% 2.15/0.79 fof(f2790,definition,(
% 2.15/0.79 ![X0]: (sQ196_spl <=> (subgroup_member(X0)|X0=multiply(a,multiply(c,element_in_O2(d,X0)))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2793,plain,(
% 2.15/0.79 sQ196_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2745,f2790,f85])).
% 2.15/0.79 fof(f2794,definition,(
% 2.15/0.79 ![X0,X1]: (sQ197_spl <=> (subgroup_member(X0)|product(X0,X1,multiply(a,multiply(c,multiply(element_in_O2(d,X0),X1))))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2797,plain,(
% 2.15/0.79 sQ197_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2746,f2794,f85])).
% 2.15/0.79 fof(f2798,definition,(
% 2.15/0.79 ![X0]: (sQ198_spl <=> (subgroup_member(X0)|product(X0,element_in_O2(X0,d),multiply(a,multiply(c,identity)))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2801,plain,(
% 2.15/0.79 sQ5_spl|sQ198_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2749,f85,f2798])).
% 2.15/0.79 fof(f2802,definition,(
% 2.15/0.79 ![X0]: (sQ199_spl <=> (subgroup_member(X0)|product(X0,inverse(element_in_O2(d,X0)),multiply(a,multiply(c,identity)))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2805,plain,(
% 2.15/0.79 sQ199_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2750,f2802,f85])).
% 2.15/0.79 fof(f2813,definition,(
% 2.15/0.79 ![X0]: (sQ200_spl <=> (subgroup_member(X0)|product(X0,identity,multiply(a,multiply(c,inverse(element_in_O2(X0,d)))))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2816,plain,(
% 2.15/0.79 sQ5_spl|sQ200_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2755,f85,f2813])).
% 2.15/0.79 fof(f2817,definition,(
% 2.15/0.79 ![X0]: (sQ201_spl <=> (product(identity,element_in_O2(inverse(d),X0),multiply(a,multiply(c,X0)))|subgroup_member(X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2820,plain,(
% 2.15/0.79 sQ201_spl|sQ71_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2758,f2817,f1511])).
% 2.15/0.79 fof(f2821,definition,(
% 2.15/0.79 ![X0,X1]: (sQ202_spl <=> (subgroup_member(X0)|product(X0,multiply(element_in_O2(X0,d),X1),multiply(a,multiply(c,X1)))))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2824,plain,(
% 2.15/0.79 sQ5_spl|sQ202_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2759,f85,f2821])).
% 2.15/0.79 fof(f2842,plain,(
% 2.15/0.79 product(a,multiply(c,identity),d)|subgroup_member(d)|~sQ17_spl),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f340])).
% 2.15/0.79 fof(f2843,plain,(
% 2.15/0.79 subgroup_member(multiply(b,inverse(identity)))|subgroup_member(d)|subgroup_member(d)),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f424])).
% 2.15/0.79 fof(f2844,plain,(
% 2.15/0.79 subgroup_member(multiply(b,identity))|subgroup_member(d)|subgroup_member(d)),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f421])).
% 2.15/0.79 fof(f2845,plain,(
% 2.15/0.79 product(inverse(d),d,identity)|subgroup_member(d)|subgroup_member(d)),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f376])).
% 2.15/0.79 fof(f2846,plain,(
% 2.15/0.79 ![X0]: (~product(identity,identity,X0)|product(inverse(d),d,X0)|subgroup_member(d)|subgroup_member(d))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f159])).
% 2.15/0.79 fof(f2847,plain,(
% 2.15/0.79 ![X0]: (~product(d,identity,X0)|product(identity,d,X0)|subgroup_member(d)|subgroup_member(d))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f226])).
% 2.15/0.79 fof(f2848,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(d)|~product(d,inverse(identity),X0)|product(d,identity,X0))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f319])).
% 2.15/0.79 fof(f2849,plain,(
% 2.15/0.79 ![X0,X1]: (subgroup_member(d)|subgroup_member(d)|~product(d,multiply(identity,X0),X1)|product(d,X0,X1))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f306])).
% 2.15/0.79 fof(f2850,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(d)|~product(d,identity,X0)|product(d,identity,X0))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f304])).
% 2.15/0.79 fof(f2851,plain,(
% 2.15/0.79 ![X0,X1]: (~product(multiply(X0,d),identity,X1)|product(X0,d,X1)|subgroup_member(d)|subgroup_member(d))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f275])).
% 2.15/0.79 fof(f2852,plain,(
% 2.15/0.79 subgroup_member(d)|subgroup_member(d)|subgroup_member(inverse(identity))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f103])).
% 2.15/0.79 fof(f2853,plain,(
% 2.15/0.79 ![X0,X1,X2]: (subgroup_member(d)|subgroup_member(d)|~product(identity,X0,X1)|~product(d,X1,X2)|product(d,X0,X2))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f105])).
% 2.15/0.79 fof(f2854,plain,(
% 2.15/0.79 ![X0,X1,X2]: (subgroup_member(d)|subgroup_member(d)|~product(identity,X0,X1)|~product(d,X0,X2)|product(d,X1,X2))),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f106])).
% 2.15/0.79 fof(f2855,plain,(
% 2.15/0.79 ![X0]: (subgroup_member(d)|subgroup_member(d)|~product(d,identity,X0)|d=X0)),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f107])).
% 2.15/0.79 fof(f2856,plain,(
% 2.15/0.79 product(d,identity,d)|subgroup_member(d)|subgroup_member(d)),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f34])).
% 2.15/0.79 fof(f2857,plain,(
% 2.15/0.79 subgroup_member(identity)|subgroup_member(d)|subgroup_member(d)),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2139,f32])).
% 2.15/0.79 fof(f2858,definition,(
% 2.15/0.79 sQ204_spl <=> (product(a,multiply(c,identity),d))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2861,plain,(
% 2.15/0.79 sQ204_spl|sQ5_spl|~sQ17_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2842,f2858,f85,f339])).
% 2.15/0.79 fof(f2862,plain,(
% 2.15/0.79 sQ132_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2843,f2294,f85])).
% 2.15/0.79 fof(f2863,plain,(
% 2.15/0.79 sQ131_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2844,f2278,f85])).
% 2.15/0.79 fof(f2864,definition,(
% 2.15/0.79 sQ205_spl <=> (product(inverse(d),d,identity))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2867,plain,(
% 2.15/0.79 sQ205_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2845,f2864,f85])).
% 2.15/0.79 fof(f2868,definition,(
% 2.15/0.79 ![X0]: (sQ206_spl <=> (~product(identity,identity,X0)|product(inverse(d),d,X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ206_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2871,plain,(
% 2.15/0.79 sQ206_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2846,f2868,f85])).
% 2.15/0.79 fof(f2872,definition,(
% 2.15/0.79 ![X0]: (sQ207_spl <=> (~product(d,identity,X0)|product(identity,d,X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2875,plain,(
% 2.15/0.79 sQ207_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2847,f2872,f85])).
% 2.15/0.79 fof(f2876,definition,(
% 2.15/0.79 ![X0]: (sQ208_spl <=> (~product(d,inverse(identity),X0)|product(d,identity,X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2879,plain,(
% 2.15/0.79 sQ5_spl|sQ208_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2848,f85,f2876])).
% 2.15/0.79 fof(f2880,definition,(
% 2.15/0.79 ![X0,X1]: (sQ209_spl <=> (~product(d,multiply(identity,X0),X1)|product(d,X0,X1)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2883,plain,(
% 2.15/0.79 sQ5_spl|sQ209_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2849,f85,f2880])).
% 2.15/0.79 fof(f2884,definition,(
% 2.15/0.79 ![X0]: (sQ210_spl <=> (~product(d,identity,X0)|product(d,identity,X0)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2887,plain,(
% 2.15/0.79 sQ5_spl|sQ210_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2850,f85,f2884])).
% 2.15/0.79 fof(f2888,definition,(
% 2.15/0.79 ![X0,X1]: (sQ211_spl <=> (~product(multiply(X0,d),identity,X1)|product(X0,d,X1)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2891,plain,(
% 2.15/0.79 sQ211_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2851,f2888,f85])).
% 2.15/0.79 fof(f2892,plain,(
% 2.15/0.79 sQ5_spl|sQ24_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2852,f85,f459])).
% 2.15/0.79 fof(f2893,definition,(
% 2.15/0.79 ![X0,X1,X2]: (sQ212_spl <=> (~product(identity,X0,X1)|~product(d,X1,X2)|product(d,X0,X2)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2896,plain,(
% 2.15/0.79 sQ5_spl|sQ212_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2853,f85,f2893])).
% 2.15/0.79 fof(f2897,definition,(
% 2.15/0.79 ![X0,X1,X2]: (sQ213_spl <=> (~product(identity,X0,X1)|~product(d,X0,X2)|product(d,X1,X2)))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2900,plain,(
% 2.15/0.79 sQ5_spl|sQ213_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2854,f85,f2897])).
% 2.15/0.79 fof(f2901,definition,(
% 2.15/0.79 ![X0]: (sQ214_spl <=> (~product(d,identity,X0)|d=X0))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2904,plain,(
% 2.15/0.79 sQ5_spl|sQ214_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2855,f85,f2901])).
% 2.15/0.79 fof(f2905,definition,(
% 2.15/0.79 sQ215_spl <=> (product(d,identity,d))),
% 2.15/0.79 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 2.15/0.79 fof(f2908,plain,(
% 2.15/0.79 sQ215_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2856,f2905,f85])).
% 2.15/0.79 fof(f2909,plain,(
% 2.15/0.79 sQ0_spl|sQ5_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f2857,f68,f85])).
% 2.15/0.79 fof(f3039,plain,(
% 2.15/0.79 subgroup_member(d)|subgroup_member(c)|subgroup_member(inverse(a))|~sQ180_spl),
% 2.15/0.79 inference(paramodulation,[status(thm)],[f2641,f32])).
% 2.15/0.79 fof(f3105,plain,(
% 2.15/0.79 sQ5_spl|sQ4_spl|sQ7_spl|~sQ180_spl),
% 2.15/0.79 inference(split_clause,[status(thm)],[f3039,f85,f82,f92,f2640])).
% 2.15/0.79 fof(f3106,plain,(
% 2.15/0.79 $false),
% 2.15/0.79 inference(sat_refutation,[status(thm)],[f74,f88,f95,f100,f102,f128,f342,f584,f737,f1011,f1295,f1393,f1397,f1407,f1467,f2090,f2382,f2510,f2643,f2686,f2736,f2785,f2789,f2793,f2797,f2801,f2805,f2816,f2820,f2824,f2861,f2862,f2863,f2867,f2871,f2875,f2879,f2883,f2887,f2891,f2892,f2896,f2900,f2904,f2908,f2909,f3105])).
% 2.15/0.79 % SZS output end CNFRefutation for theBenchmark.p
% 0.75/0.80 % Elapsed time: 0.373292 seconds
% 0.75/0.80 % CPU time: 2.762903 seconds
% 0.75/0.80 % Total memory used: 101.642 MB
% 0.75/0.80 % Net memory used: 95.996 MB
%------------------------------------------------------------------------------