%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GRP617-1 : TPTP v9.2.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:26:31 PM UTC 2026
% Result : Unsatisfiable 194.89s 108.08s
% Output : CNFRefutation 198.56s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_503)
% Comments :
%------------------------------------------------------------------------------
cnf(associativity1,axiom,
( product(X1,X5,X6)
| ~ product(X1,X2,X3)
| ~ product(X2,X4,X5)
| ~ product(X3,X4,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',associativity1) ).
cnf(associativity2,axiom,
( product(X3,X4,X6)
| ~ product(X1,X2,X3)
| ~ product(X2,X4,X5)
| ~ product(X1,X5,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',associativity2) ).
cnf(total_function2,axiom,
( X3 = X4
| ~ product(X1,X2,X3)
| ~ product(X1,X2,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',total_function2) ).
cnf(normality2,hypothesis,
( subgroup2_member(multiply(X2,multiply(X1,inverse(X2))))
| ~ subgroup2_member(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',normality2) ).
cnf(normality1,hypothesis,
( subgroup1_member(multiply(X2,multiply(X1,inverse(X2))))
| ~ subgroup1_member(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',normality1) ).
cnf(closure_of_product2,axiom,
( subgroup2_member(X3)
| ~ subgroup2_member(X1)
| ~ subgroup2_member(X2)
| ~ product(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_product2) ).
cnf(closure_of_product1,axiom,
( subgroup1_member(X3)
| ~ subgroup1_member(X1)
| ~ subgroup1_member(X2)
| ~ product(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_product1) ).
cnf(total_function1,axiom,
product(X1,X2,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',total_function1) ).
cnf(left_inverse,axiom,
product(inverse(X1),X1,identity),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',left_inverse) ).
cnf(right_inverse,axiom,
product(X1,inverse(X1),identity),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',right_inverse) ).
cnf(left_identity,axiom,
product(identity,X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',left_identity) ).
cnf(right_identity,axiom,
product(X1,identity,X1),
file('/export/starexec/sandbox/benchmark/Axioms/GRP003-0.ax',right_identity) ).
cnf(prove_vu_equals_uv,negated_conjecture,
multiply(v,u) != multiply(u,v),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_vu_equals_uv) ).
cnf(closure_of_inverse2,axiom,
( subgroup2_member(inverse(X1))
| ~ subgroup2_member(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_inverse2) ).
cnf(closure_of_inverse1,axiom,
( subgroup1_member(inverse(X1))
| ~ subgroup1_member(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_inverse1) ).
cnf(trivial_intersection,hypothesis,
( X1 = identity
| ~ subgroup1_member(X1)
| ~ subgroup2_member(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',trivial_intersection) ).
cnf(u_in_G2,hypothesis,
subgroup2_member(u),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u_in_G2) ).
cnf(v_in_G1,hypothesis,
subgroup1_member(v),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v_in_G1) ).
cnf(i_0_18,axiom,
( product(X1,X5,X6)
| ~ product(X1,X2,X3)
| ~ product(X2,X4,X5)
| ~ product(X3,X4,X6) ),
associativity1,
[final] ).
cnf(i_0_19,axiom,
( product(X3,X4,X6)
| ~ product(X1,X2,X3)
| ~ product(X2,X4,X5)
| ~ product(X1,X5,X6) ),
associativity2,
[final] ).
cnf(i_0_20,axiom,
( X3 = X4
| ~ product(X1,X2,X3)
| ~ product(X1,X2,X4) ),
total_function2,
[final] ).
cnf(i_0_21,hypothesis,
( subgroup2_member(multiply(X2,multiply(X1,inverse(X2))))
| ~ subgroup2_member(X1) ),
normality2,
[final] ).
cnf(i_0_22,hypothesis,
( subgroup1_member(multiply(X2,multiply(X1,inverse(X2))))
| ~ subgroup1_member(X1) ),
normality1,
[final] ).
cnf(i_0_23,axiom,
( subgroup2_member(X3)
| ~ subgroup2_member(X1)
| ~ subgroup2_member(X2)
| ~ product(X1,X2,X3) ),
closure_of_product2,
[final] ).
cnf(i_0_24,axiom,
( subgroup1_member(X3)
| ~ subgroup1_member(X1)
| ~ subgroup1_member(X2)
| ~ product(X1,X2,X3) ),
closure_of_product1,
[final] ).
cnf(i_0_25,axiom,
product(X1,X2,multiply(X1,X2)),
total_function1,
[final] ).
cnf(i_0_26,axiom,
product(inverse(X1),X1,identity),
left_inverse,
[final] ).
cnf(i_0_27,axiom,
product(X1,inverse(X1),identity),
right_inverse,
[final] ).
cnf(i_0_28,axiom,
product(identity,X1,X1),
left_identity,
[final] ).
cnf(i_0_29,axiom,
product(X1,identity,X1),
right_identity,
[final] ).
cnf(i_0_30,negated_conjecture,
multiply(v,u) != multiply(u,v),
prove_vu_equals_uv,
[final] ).
cnf(i_0_31,axiom,
( subgroup2_member(inverse(X1))
| ~ subgroup2_member(X1) ),
closure_of_inverse2,
[final] ).
cnf(i_0_32,axiom,
( subgroup1_member(inverse(X1))
| ~ subgroup1_member(X1) ),
closure_of_inverse1,
[final] ).
cnf(i_0_33,hypothesis,
( X1 = identity
| ~ subgroup1_member(X1)
| ~ subgroup2_member(X1) ),
trivial_intersection,
[final] ).
cnf(i_0_34,hypothesis,
subgroup2_member(u),
u_in_G2,
[final] ).
cnf(i_0_35,hypothesis,
subgroup1_member(v),
v_in_G1,
[final] ).
cnf(i_0_36,axiom,
X1 = X1 ).
cnf(i_0_37,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_38,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_39,axiom,
( X1 != X2
| multiply(X1,X3) = multiply(X2,X3) ) ).
cnf(i_0_40,axiom,
( X1 != X2
| multiply(X3,X1) = multiply(X3,X2) ) ).
cnf(i_0_41,axiom,
( X1 != X2
| ~ product(X1,X3,X4)
| product(X2,X3,X4) ) ).
cnf(i_0_42,axiom,
( X1 != X2
| ~ product(X3,X1,X4)
| product(X3,X2,X4) ) ).
cnf(i_0_43,axiom,
( X1 != X2
| ~ product(X3,X4,X1)
| product(X3,X4,X2) ) ).
cnf(i_0_44,axiom,
( X1 != X2
| ~ subgroup2_member(X1)
| subgroup2_member(X2) ) ).
cnf(i_0_45,axiom,
( X1 != X2
| ~ subgroup1_member(X1)
| subgroup1_member(X2) ) ).
cnf(i_0_521,plain,
inverse(inverse(identity)) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(scs_inference,[],[i_0_29,i_0_503,i_0_41]) ).
cnf(i_0_522,plain,
~ product(multiply(inverse(multiply(v,u)),multiply(u,v)),X1,inverse(inverse(X1))),
inference(rename_variables,[],[i_0_503]) ).
cnf(i_0_561,plain,
~ product(u,identity,multiply(inverse(v),multiply(u,v))),
inference(equality_inference,[],[554]) ).
cnf(i_0_572,plain,
~ product(identity,u,multiply(inverse(v),multiply(u,v))),
inference(equality_inference,[],[565]) ).
cnf(i_0_641,plain,
multiply(X1,inverse(X1)) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_701,plain,
multiply(inverse(X1),X1) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_891,plain,
multiply(inverse(X1),X1) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1085,plain,
multiply(X1,inverse(X1)) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1615,plain,
inverse(multiply(u,v)) != multiply(inverse(multiply(v,u)),identity),
inference(scs_inference,[],[i_0_1538,i_0_463,i_0_31,i_0_21,i_0_37]) ).
cnf(i_0_2179,plain,
multiply(X1,inverse(X1)) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_145,plain,
~ product(multiply(v,u),identity,multiply(u,v)),
inference(equality_inference,[],[138]) ).
cnf(i_0_148,plain,
multiply(u,v) != inverse(inverse(multiply(v,u))),
inference(scs_inference,[],[i_0_74,i_0_130,i_0_28,i_0_27,i_0_20,i_0_42]) ).
cnf(i_0_150,plain,
identity != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(scs_inference,[],[i_0_97,i_0_74,i_0_130,i_0_26,i_0_28,i_0_27,i_0_20,i_0_42,i_0_43]) ).
cnf(i_0_152,plain,
~ product(inverse(multiply(u,v)),multiply(v,u),identity),
inference(scs_inference,[],[i_0_71,i_0_97,i_0_74,i_0_130,i_0_26,i_0_28,i_0_149,i_0_27,i_0_20,i_0_42,i_0_43,i_0_18]) ).
cnf(i_0_156,plain,
~ product(multiply(v,u),inverse(identity),multiply(u,v)),
inference(scs_inference,[],[i_0_71,i_0_97,i_0_74,i_0_130,i_0_26,i_0_28,i_0_149,i_0_29,i_0_27,i_0_20,i_0_42,i_0_43,i_0_18,i_0_19]) ).
cnf(i_0_161,plain,
inverse(multiply(v,u)) != inverse(multiply(u,v)),
inference(scs_inference,[],[i_0_71,i_0_97,i_0_74,i_0_101,i_0_130,i_0_26,i_0_158,i_0_28,i_0_149,i_0_29,i_0_27,i_0_20,i_0_42,i_0_43,i_0_18,i_0_19,i_0_44,i_0_41]) ).
cnf(i_0_405,plain,
multiply(identity,multiply(u,v)) != inverse(inverse(multiply(v,u))),
inference(scs_inference,[],[i_0_25,i_0_134,i_0_43]) ).
cnf(i_0_519,plain,
~ product(multiply(inverse(multiply(v,u)),multiply(u,v)),inverse(X1),inverse(inverse(inverse(X1)))),
inference(equality_inference,[],[511]) ).
cnf(i_0_520,plain,
~ product(multiply(inverse(multiply(v,u)),multiply(u,v)),inverse(X1),inverse(inverse(inverse(X1)))),
inference(equality_inference,[],[512]) ).
cnf(i_0_526,plain,
multiply(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v))) != X1,
inference(scs_inference,[],[i_0_25,i_0_507,i_0_43]) ).
cnf(i_0_528,plain,
identity != inverse(multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(scs_inference,[],[i_0_146,i_0_29,i_0_25,i_0_507,i_0_43,i_0_42]) ).
cnf(i_0_531,plain,
inverse(multiply(inverse(multiply(v,u)),multiply(u,v))) != inverse(inverse(identity)),
inference(scs_inference,[],[i_0_146,i_0_26,i_0_29,i_0_25,i_0_507,i_0_43,i_0_42,i_0_41]) ).
cnf(i_0_532,plain,
~ product(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v)),X1),
inference(rename_variables,[],[i_0_507]) ).
cnf(i_0_534,plain,
~ product(identity,identity,inverse(multiply(inverse(multiply(v,u)),multiply(u,v)))),
inference(scs_inference,[],[i_0_97,i_0_146,i_0_26,i_0_29,i_0_28,i_0_25,i_0_507,i_0_43,i_0_42,i_0_41,i_0_19]) ).
cnf(i_0_546,plain,
inverse(inverse(inverse(identity))) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(scs_inference,[],[i_0_27,i_0_507,i_0_42]) ).
cnf(i_0_547,plain,
~ product(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v)),X1),
inference(rename_variables,[],[i_0_507]) ).
cnf(i_0_166,plain,
multiply(multiply(v,u),inverse(identity)) != multiply(u,v),
inference(scs_inference,[],[i_0_156,i_0_25,i_0_43]) ).
cnf(i_0_168,plain,
~ product(multiply(u,v),inverse(u),v),
inference(scs_inference,[],[i_0_71,i_0_156,i_0_25,i_0_167,i_0_26,i_0_43,i_0_18]) ).
cnf(i_0_183,plain,
multiply(inverse(multiply(u,v)),multiply(v,u)) != identity,
inference(scs_inference,[],[i_0_55,i_0_27,i_0_152,i_0_25,i_0_42,i_0_43]) ).
cnf(i_0_209,plain,
inverse(inverse(multiply(u,v))) != multiply(v,u),
inference(scs_inference,[],[i_0_27,i_0_152,i_0_42]) ).
cnf(i_0_316,plain,
~ product(identity,multiply(u,v),inverse(inverse(multiply(v,u)))),
inference(equality_inference,[],[315]) ).
cnf(i_0_318,plain,
~ product(identity,inverse(inverse(multiply(v,u))),multiply(u,v)),
inference(equality_inference,[],[317]) ).
cnf(i_0_525,plain,
~ product(multiply(inverse(multiply(v,u)),multiply(u,v)),X1,inverse(inverse(X1))),
inference(equality_inference,[],[524]) ).
cnf(i_0_663,plain,
multiply(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v))) != X1,
inference(rename_variables,[],[i_0_526]) ).
cnf(i_0_1695,plain,
X1 != multiply(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(scs_inference,[],[i_0_526,i_0_78,i_0_31,i_0_21,i_0_37]) ).
cnf(i_0_180,plain,
~ product(u,v,multiply(v,u)),
inference(equality_inference,[],[172]) ).
cnf(i_0_195,plain,
multiply(multiply(u,v),inverse(u)) != v,
inference(scs_inference,[],[i_0_168,i_0_25,i_0_43]) ).
cnf(i_0_197,plain,
~ product(multiply(u,v),inverse(identity),multiply(v,u)),
inference(scs_inference,[],[i_0_71,i_0_29,i_0_26,i_0_168,i_0_25,i_0_43,i_0_18]) ).
cnf(i_0_254,plain,
~ product(multiply(v,u),inverse(identity),multiply(u,v)),
inference(equality_inference,[],[251]) ).
cnf(i_0_255,plain,
subgroup1_member(multiply(v,v)),
inference(equality_inference,[],[252]) ).
cnf(i_0_256,plain,
~ product(u,v,multiply(v,u)),
inference(equality_inference,[],[253]) ).
cnf(i_0_297,plain,
~ product(multiply(v,u),inverse(identity),multiply(u,v)),
inference(equality_inference,[],[288]) ).
cnf(i_0_298,plain,
~ product(multiply(v,u),inverse(identity),multiply(u,v)),
inference(equality_inference,[],[289]) ).
cnf(i_0_573,plain,
multiply(u,v) != multiply(multiply(v,u),inverse(identity)),
inference(scs_inference,[],[i_0_166,i_0_37]) ).
cnf(i_0_574,plain,
subgroup2_member(inverse(u)),
inference(scs_inference,[],[i_0_166,i_0_34,i_0_37,i_0_31]) ).
cnf(i_0_576,plain,
subgroup1_member(inverse(v)),
inference(scs_inference,[],[i_0_166,i_0_34,i_0_35,i_0_37,i_0_31,i_0_32]) ).
cnf(i_0_578,plain,
subgroup2_member(identity),
inference(scs_inference,[],[i_0_166,i_0_34,i_0_35,i_0_37,i_0_31,i_0_32,i_0_414]) ).
cnf(i_0_579,plain,
subgroup1_member(identity),
inference(scs_inference,[],[i_0_166,i_0_34,i_0_35,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418]) ).
cnf(i_0_580,plain,
subgroup2_member(multiply(X1,multiply(u,inverse(X1)))),
inference(scs_inference,[],[i_0_166,i_0_34,i_0_35,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418,i_0_21]) ).
cnf(i_0_582,plain,
subgroup1_member(multiply(X1,multiply(v,inverse(X1)))),
inference(scs_inference,[],[i_0_166,i_0_34,i_0_35,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418,i_0_21,i_0_22]) ).
cnf(i_0_584,plain,
~ product(identity,multiply(multiply(v,u),inverse(identity)),multiply(u,v)),
inference(scs_inference,[],[i_0_166,i_0_34,i_0_35,i_0_28,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418,i_0_21,i_0_22,i_0_20]) ).
cnf(i_0_587,plain,
~ product(inverse(identity),identity,inverse(multiply(inverse(multiply(v,u)),multiply(u,v)))),
inference(scs_inference,[],[i_0_166,i_0_534,i_0_34,i_0_35,i_0_26,i_0_28,i_0_585,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418,i_0_21,i_0_22,i_0_20,i_0_19]) ).
cnf(i_0_591,plain,
~ product(inverse(identity),multiply(inverse(v),multiply(u,v)),u),
inference(scs_inference,[],[i_0_166,i_0_534,i_0_562,i_0_34,i_0_35,i_0_26,i_0_27,i_0_28,i_0_585,i_0_589,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418,i_0_21,i_0_22,i_0_20,i_0_19,i_0_18]) ).
cnf(i_0_597,plain,
multiply(identity,identity) != inverse(multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(scs_inference,[],[i_0_166,i_0_534,i_0_562,i_0_34,i_0_35,i_0_26,i_0_27,i_0_28,i_0_585,i_0_589,i_0_25,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418,i_0_21,i_0_22,i_0_20,i_0_19,i_0_18,i_0_33,i_0_43]) ).
cnf(i_0_599,plain,
subgroup2_member(multiply(inverse(u),inverse(u))),
inference(scs_inference,[],[i_0_166,i_0_534,i_0_562,i_0_34,i_0_35,i_0_26,i_0_27,i_0_28,i_0_585,i_0_589,i_0_25,i_0_598,i_0_37,i_0_31,i_0_32,i_0_414,i_0_418,i_0_21,i_0_22,i_0_20,i_0_19,i_0_18,i_0_33,i_0_43,i_0_23]) ).
cnf(i_0_1728,plain,
X1 != multiply(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(rename_variables,[],[i_0_1695]) ).
cnf(i_0_1990,plain,
X1 != multiply(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(rename_variables,[],[i_0_1695]) ).
cnf(i_0_205,plain,
~ product(v,u,multiply(u,v)),
inference(equality_inference,[],[201]) ).
cnf(i_0_206,plain,
subgroup2_member(multiply(multiply(u,u),multiply(u,u))),
inference(equality_inference,[],[202]) ).
cnf(i_0_207,plain,
subgroup1_member(multiply(multiply(v,v),multiply(v,v))),
inference(equality_inference,[],[203]) ).
cnf(i_0_208,plain,
~ product(X1,inverse(X1),multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(equality_inference,[],[204]) ).
cnf(i_0_211,plain,
multiply(multiply(u,v),inverse(identity)) != multiply(v,u),
inference(scs_inference,[],[i_0_27,i_0_152,i_0_197,i_0_25,i_0_42,i_0_43]) ).
cnf(i_0_250,plain,
~ product(multiply(u,v),inverse(u),v),
inference(equality_inference,[],[238]) ).
cnf(i_0_286,plain,
~ product(multiply(u,v),inverse(u),v),
inference(equality_inference,[],[277]) ).
cnf(i_0_287,plain,
~ product(multiply(u,v),inverse(u),v),
inference(equality_inference,[],[278]) ).
cnf(i_0_609,plain,
subgroup2_member(inverse(identity)),
inference(scs_inference,[],[i_0_578,i_0_31]) ).
cnf(i_0_611,plain,
subgroup1_member(inverse(identity)),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_31,i_0_32]) ).
cnf(i_0_613,plain,
subgroup2_member(multiply(X1,multiply(identity,inverse(X1)))),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_31,i_0_32,i_0_21]) ).
cnf(i_0_615,plain,
subgroup1_member(multiply(X1,multiply(identity,inverse(X1)))),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_31,i_0_32,i_0_21,i_0_22]) ).
cnf(i_0_649,plain,
subgroup2_member(inverse(inverse(u))),
inference(scs_inference,[],[i_0_574,i_0_31]) ).
cnf(i_0_672,plain,
subgroup1_member(multiply(X1,multiply(v,inverse(X1)))),
inference(rename_variables,[],[i_0_582]) ).
cnf(i_0_1351,plain,
subgroup2_member(inverse(multiply(inverse(u),inverse(u)))),
inference(scs_inference,[],[i_0_599,i_0_31]) ).
cnf(i_0_1353,plain,
subgroup2_member(multiply(X1,multiply(multiply(inverse(u),inverse(u)),inverse(X1)))),
inference(scs_inference,[],[i_0_599,i_0_31,i_0_21]) ).
cnf(i_0_1744,plain,
inverse(multiply(inverse(multiply(v,u)),multiply(u,v))) != multiply(identity,identity),
inference(scs_inference,[],[i_0_597,i_0_37]) ).
cnf(i_0_224,plain,
subgroup2_member(multiply(u,u)),
inference(equality_inference,[],[213]) ).
cnf(i_0_259,plain,
~ product(multiply(u,v),inverse(identity),multiply(v,u)),
inference(equality_inference,[],[257]) ).
cnf(i_0_260,plain,
~ product(identity,multiply(v,u),multiply(u,v)),
inference(equality_inference,[],[258]) ).
cnf(i_0_308,plain,
~ product(multiply(u,v),inverse(identity),multiply(v,u)),
inference(equality_inference,[],[299]) ).
cnf(i_0_309,plain,
~ product(multiply(u,v),inverse(identity),multiply(v,u)),
inference(equality_inference,[],[300]) ).
cnf(i_0_617,plain,
multiply(v,u) != multiply(multiply(u,v),inverse(identity)),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_211,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37]) ).
cnf(i_0_618,plain,
inverse(identity) = identity,
inference(scs_inference,[],[i_0_578,i_0_579,i_0_211,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33]) ).
cnf(i_0_620,plain,
product(inverse(inverse(identity)),identity,identity),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_211,i_0_26,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42]) ).
cnf(i_0_622,plain,
subgroup2_member(multiply(multiply(inverse(u),inverse(u)),multiply(inverse(u),inverse(u)))),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_211,i_0_599,i_0_26,i_0_25,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23]) ).
cnf(i_0_625,plain,
subgroup1_member(multiply(inverse(v),inverse(v))),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_599,i_0_26,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24]) ).
cnf(i_0_628,plain,
~ product(multiply(multiply(v,u),inverse(identity)),identity,multiply(u,v)),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_26,i_0_621,i_0_27,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19]) ).
cnf(i_0_632,plain,
~ product(identity,inverse(identity),inverse(multiply(inverse(multiply(v,u)),multiply(u,v)))),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_587,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18]) ).
cnf(i_0_636,plain,
~ product(inverse(identity),inverse(identity),multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_587,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18,i_0_204]) ).
cnf(i_0_638,plain,
multiply(X1,inverse(identity)) = multiply(X1,identity),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_587,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18,i_0_204,i_0_524,i_0_40]) ).
cnf(i_0_639,plain,
multiply(inverse(identity),X1) = multiply(identity,X1),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_587,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18,i_0_204,i_0_524,i_0_40,i_0_39]) ).
cnf(i_0_640,plain,
multiply(identity,inverse(inverse(identity))) != multiply(inverse(multiply(v,u)),multiply(u,v)),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_587,i_0_400,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18,i_0_204,i_0_524,i_0_40,i_0_39,i_0_38]) ).
cnf(i_0_642,plain,
~ product(inverse(inverse(identity)),identity,multiply(inverse(multiply(v,u)),multiply(u,v))),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_150,i_0_587,i_0_400,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18,i_0_204,i_0_524,i_0_40,i_0_39,i_0_38,i_0_20]) ).
cnf(i_0_645,plain,
product(identity,multiply(X1,inverse(identity)),multiply(X1,identity)),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_150,i_0_587,i_0_400,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_28,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18,i_0_204,i_0_524,i_0_40,i_0_39,i_0_38,i_0_20,i_0_44,i_0_43]) ).
cnf(i_0_647,plain,
product(identity,inverse(inverse(identity)),identity),
inference(scs_inference,[],[i_0_578,i_0_579,i_0_576,i_0_211,i_0_584,i_0_599,i_0_150,i_0_587,i_0_400,i_0_26,i_0_621,i_0_630,i_0_27,i_0_629,i_0_634,i_0_28,i_0_25,i_0_623,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37,i_0_33,i_0_42,i_0_23,i_0_24,i_0_19,i_0_18,i_0_204,i_0_524,i_0_40,i_0_39,i_0_38,i_0_20,i_0_44,i_0_43,i_0_41]) ).
cnf(i_0_651,plain,
subgroup1_member(inverse(inverse(identity))),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_31,i_0_32]) ).
cnf(i_0_653,plain,
subgroup2_member(multiply(X1,multiply(inverse(u),inverse(X1)))),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_31,i_0_32,i_0_21]) ).
cnf(i_0_655,plain,
subgroup1_member(multiply(X1,multiply(inverse(identity),inverse(X1)))),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_31,i_0_32,i_0_21,i_0_22]) ).
cnf(i_0_668,plain,
subgroup2_member(multiply(X1,multiply(identity,inverse(X1)))),
inference(rename_variables,[],[i_0_613]) ).
cnf(i_0_686,plain,
subgroup2_member(inverse(inverse(identity))),
inference(scs_inference,[],[i_0_609,i_0_31]) ).
cnf(i_0_719,plain,
subgroup2_member(inverse(inverse(inverse(u)))),
inference(scs_inference,[],[i_0_649,i_0_31]) ).
cnf(i_0_1385,plain,
subgroup2_member(inverse(inverse(multiply(inverse(u),inverse(u))))),
inference(scs_inference,[],[i_0_1351,i_0_31]) ).
cnf(i_0_1387,plain,
subgroup2_member(multiply(X1,multiply(inverse(multiply(inverse(u),inverse(u))),inverse(X1)))),
inference(scs_inference,[],[i_0_1351,i_0_31,i_0_21]) ).
cnf(i_0_1445,plain,
subgroup2_member(inverse(multiply(X1,multiply(identity,inverse(X1))))),
inference(scs_inference,[],[i_0_613,i_0_31]) ).
cnf(i_0_1447,plain,
subgroup2_member(multiply(X1,multiply(multiply(X2,multiply(identity,inverse(X2))),inverse(X1)))),
inference(scs_inference,[],[i_0_613,i_0_31,i_0_21]) ).
cnf(i_0_659,plain,
multiply(v,u) != multiply(identity,multiply(u,v)),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_398,i_0_638,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37]) ).
cnf(i_0_660,plain,
multiply(X1,multiply(X2,inverse(identity))) = multiply(X1,multiply(X2,identity)),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_398,i_0_638,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40]) ).
cnf(i_0_661,plain,
multiply(multiply(X1,inverse(identity)),X2) = multiply(multiply(X1,identity),X2),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_398,i_0_638,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39]) ).
cnf(i_0_664,plain,
~ product(identity,multiply(identity,multiply(u,v)),multiply(v,u)),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_618,i_0_398,i_0_638,i_0_526,i_0_28,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39,i_0_38,i_0_20]) ).
cnf(i_0_667,plain,
multiply(X1,multiply(identity,inverse(X1))) = identity,
inference(scs_inference,[],[i_0_574,i_0_611,i_0_618,i_0_398,i_0_638,i_0_613,i_0_615,i_0_526,i_0_28,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39,i_0_38,i_0_20,i_0_33]) ).
cnf(i_0_670,plain,
subgroup1_member(multiply(identity,multiply(v,inverse(inverse(identity))))),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_618,i_0_398,i_0_638,i_0_639,i_0_582,i_0_613,i_0_615,i_0_526,i_0_28,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39,i_0_38,i_0_20,i_0_33,i_0_45]) ).
cnf(i_0_671,plain,
multiply(inverse(identity),X1) = multiply(identity,X1),
inference(rename_variables,[],[i_0_639]) ).
cnf(i_0_674,plain,
product(identity,multiply(X1,inverse(identity)),multiply(X1,identity)),
inference(rename_variables,[],[i_0_645]) ).
cnf(i_0_675,plain,
multiply(inverse(identity),X1) = multiply(identity,X1),
inference(rename_variables,[],[i_0_639]) ).
cnf(i_0_681,plain,
product(identity,multiply(X1,inverse(identity)),multiply(X1,identity)),
inference(rename_variables,[],[i_0_645]) ).
cnf(i_0_688,plain,
subgroup1_member(inverse(multiply(inverse(v),inverse(v)))),
inference(scs_inference,[],[i_0_609,i_0_625,i_0_31,i_0_32]) ).
cnf(i_0_690,plain,
subgroup2_member(multiply(X1,multiply(inverse(identity),inverse(X1)))),
inference(scs_inference,[],[i_0_609,i_0_625,i_0_31,i_0_32,i_0_21]) ).
cnf(i_0_692,plain,
subgroup1_member(multiply(X1,multiply(multiply(inverse(v),inverse(v)),inverse(X1)))),
inference(scs_inference,[],[i_0_609,i_0_625,i_0_31,i_0_32,i_0_21,i_0_22]) ).
cnf(i_0_721,plain,
subgroup1_member(inverse(multiply(X1,multiply(inverse(identity),inverse(X1))))),
inference(scs_inference,[],[i_0_649,i_0_655,i_0_31,i_0_32]) ).
cnf(i_0_723,plain,
subgroup2_member(multiply(X1,multiply(inverse(inverse(u)),inverse(X1)))),
inference(scs_inference,[],[i_0_649,i_0_655,i_0_31,i_0_32,i_0_21]) ).
cnf(i_0_734,plain,
product(identity,multiply(X1,inverse(identity)),multiply(X1,identity)),
inference(rename_variables,[],[i_0_645]) ).
cnf(i_0_744,plain,
multiply(inverse(identity),X1) = multiply(identity,X1),
inference(rename_variables,[],[i_0_639]) ).
cnf(i_0_751,plain,
product(identity,multiply(X1,inverse(identity)),multiply(X1,identity)),
inference(rename_variables,[],[i_0_645]) ).
cnf(i_0_753,plain,
subgroup2_member(inverse(inverse(inverse(identity)))),
inference(scs_inference,[],[i_0_686,i_0_31]) ).
cnf(i_0_786,plain,
subgroup2_member(multiply(X1,multiply(inverse(u),inverse(X1)))),
inference(rename_variables,[],[i_0_653]) ).
cnf(i_0_798,plain,
~ product(inverse(identity),u,multiply(inverse(v),multiply(u,v))),
inference(scs_inference,[],[i_0_618,i_0_565]) ).
cnf(i_0_799,plain,
subgroup2_member(inverse(multiply(X1,multiply(u,inverse(X1))))),
inference(scs_inference,[],[i_0_580,i_0_618,i_0_565,i_0_31]) ).
cnf(i_0_801,plain,
subgroup1_member(inverse(multiply(X1,multiply(v,inverse(X1))))),
inference(scs_inference,[],[i_0_580,i_0_582,i_0_618,i_0_565,i_0_31,i_0_32]) ).
cnf(i_0_803,plain,
subgroup2_member(multiply(X1,multiply(multiply(X2,multiply(u,inverse(X2))),inverse(X1)))),
inference(scs_inference,[],[i_0_580,i_0_582,i_0_618,i_0_565,i_0_31,i_0_32,i_0_21]) ).
cnf(i_0_805,plain,
subgroup1_member(multiply(X1,multiply(multiply(X2,multiply(v,inverse(X2))),inverse(X1)))),
inference(scs_inference,[],[i_0_580,i_0_582,i_0_618,i_0_565,i_0_31,i_0_32,i_0_21,i_0_22]) ).
cnf(i_0_896,plain,
multiply(X1,inverse(identity)) = multiply(X1,identity),
inference(rename_variables,[],[i_0_638]) ).
cnf(i_0_988,plain,
multiply(inverse(identity),X1) = multiply(identity,X1),
inference(rename_variables,[],[i_0_639]) ).
cnf(i_0_992,plain,
subgroup2_member(inverse(inverse(inverse(inverse(u))))),
inference(scs_inference,[],[i_0_719,i_0_31]) ).
cnf(i_0_994,plain,
subgroup1_member(inverse(multiply(X1,multiply(identity,inverse(X1))))),
inference(scs_inference,[],[i_0_719,i_0_615,i_0_31,i_0_32]) ).
cnf(i_0_996,plain,
subgroup2_member(multiply(X1,multiply(inverse(inverse(inverse(u))),inverse(X1)))),
inference(scs_inference,[],[i_0_719,i_0_615,i_0_31,i_0_32,i_0_21]) ).
cnf(i_0_998,plain,
subgroup1_member(multiply(X1,multiply(multiply(X2,multiply(identity,inverse(X2))),inverse(X1)))),
inference(scs_inference,[],[i_0_719,i_0_615,i_0_31,i_0_32,i_0_21,i_0_22]) ).
cnf(i_0_1000,plain,
inverse(v) != multiply(u,inverse(multiply(u,v))),
inference(scs_inference,[],[i_0_485,i_0_719,i_0_615,i_0_31,i_0_32,i_0_21,i_0_22,i_0_37]) ).
cnf(i_0_1044,plain,
multiply(inverse(identity),X1) = multiply(identity,X1),
inference(rename_variables,[],[i_0_639]) ).
cnf(i_0_1092,plain,
product(identity,multiply(X1,inverse(identity)),multiply(X1,identity)),
inference(rename_variables,[],[i_0_645]) ).
cnf(i_0_1191,plain,
multiply(inverse(identity),X1) = multiply(identity,X1),
inference(rename_variables,[],[i_0_639]) ).
cnf(i_0_1413,plain,
subgroup2_member(inverse(multiply(X1,multiply(inverse(u),inverse(X1))))),
inference(scs_inference,[],[i_0_653,i_0_31]) ).
cnf(i_0_1415,plain,
subgroup2_member(multiply(X1,multiply(multiply(X2,multiply(inverse(u),inverse(X2))),inverse(X1)))),
inference(scs_inference,[],[i_0_653,i_0_31,i_0_21]) ).
cnf(i_0_1488,plain,
subgroup2_member(inverse(multiply(X1,multiply(identity,inverse(X1))))),
inference(rename_variables,[],[i_0_1445]) ).
cnf(i_0_1521,plain,
multiply(X1,inverse(identity)) = multiply(X1,identity),
inference(rename_variables,[],[i_0_638]) ).
cnf(i_0_1540,plain,
multiply(inverse(multiply(v,u)),multiply(u,v)) != multiply(identity,inverse(inverse(identity))),
inference(scs_inference,[],[i_0_640,i_0_59,i_0_31,i_0_21,i_0_37]) ).
cnf(i_0_673,plain,
product(identity,multiply(inverse(identity),inverse(identity)),multiply(identity,identity)),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_618,i_0_398,i_0_638,i_0_639,i_0_671,i_0_645,i_0_582,i_0_613,i_0_615,i_0_526,i_0_28,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39,i_0_38,i_0_20,i_0_33,i_0_45,i_0_43]) ).
cnf(i_0_676,plain,
product(identity,identity,inverse(identity)),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_618,i_0_398,i_0_638,i_0_639,i_0_671,i_0_645,i_0_582,i_0_613,i_0_615,i_0_526,i_0_28,i_0_665,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39,i_0_38,i_0_20,i_0_33,i_0_45,i_0_43,i_0_42]) ).
cnf(i_0_678,plain,
product(multiply(X1,identity),inverse(multiply(X1,inverse(identity))),identity),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_618,i_0_398,i_0_638,i_0_639,i_0_671,i_0_645,i_0_582,i_0_613,i_0_615,i_0_526,i_0_27,i_0_28,i_0_665,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39,i_0_38,i_0_20,i_0_33,i_0_45,i_0_43,i_0_42,i_0_41]) ).
cnf(i_0_680,plain,
~ product(inverse(inverse(identity)),multiply(multiply(v,u),identity),multiply(u,v)),
inference(scs_inference,[],[i_0_574,i_0_611,i_0_618,i_0_398,i_0_638,i_0_639,i_0_671,i_0_645,i_0_674,i_0_620,i_0_582,i_0_613,i_0_615,i_0_526,i_0_584,i_0_27,i_0_28,i_0_665,i_0_31,i_0_32,i_0_21,i_0_22,i_0_204,i_0_524,i_0_37,i_0_40,i_0_39,i_0_38,i_0_20,i_0_33,i_0_45,i_0_43,i_0_42,i_0_41,i_0_19]) ).
cnf(c_0_822,axiom,
( product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ product(X4,X6,X2)
| ~ product(X5,X6,X3) ),
i_0_18 ).
cnf(c_0_823,axiom,
product(identity,X1,X1),
i_0_28 ).
cnf(c_0_824,plain,
( product(X1,X2,X3)
| ~ product(X1,X4,identity)
| ~ product(X4,X3,X2) ),
inference(spm,[status(thm)],[c_0_822,c_0_823]) ).
cnf(c_0_825,axiom,
product(X1,inverse(X1),identity),
i_0_27 ).
cnf(c_0_826,axiom,
( X1 = X2
| ~ product(X3,X4,X1)
| ~ product(X3,X4,X2) ),
i_0_20 ).
cnf(c_0_827,axiom,
product(X1,identity,X1),
i_0_29 ).
cnf(c_0_828,axiom,
product(X1,X2,multiply(X1,X2)),
i_0_25 ).
cnf(c_0_829,plain,
( product(X1,X2,X3)
| ~ product(inverse(X1),X3,X2) ),
inference(spm,[status(thm)],[c_0_824,c_0_825]) ).
cnf(c_0_830,plain,
( X1 = X2
| ~ product(X2,identity,X1) ),
inference(spm,[status(thm)],[c_0_826,c_0_827]) ).
cnf(c_0_831,plain,
( X1 = multiply(X2,X3)
| ~ product(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_826,c_0_828]) ).
cnf(c_0_832,plain,
product(X1,identity,inverse(inverse(X1))),
inference(spm,[status(thm)],[c_0_829,c_0_825]) ).
cnf(c_0_833,plain,
multiply(X1,identity) = X1,
inference(spm,[status(thm)],[c_0_830,c_0_828]) ).
cnf(c_0_834,plain,
~ product(inverse(inverse(X1)),multiply(inverse(multiply(v,u)),multiply(u,v)),X1),
i_0_532 ).
cnf(c_0_835,plain,
inverse(inverse(X1)) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_831,c_0_832]),c_0_833]) ).
cnf(c_0_836,plain,
( product(X1,X2,multiply(X3,X4))
| ~ product(X5,X4,X2)
| ~ product(X1,X5,X3) ),
inference(spm,[status(thm)],[c_0_822,c_0_828]) ).
cnf(c_0_837,plain,
~ product(X1,multiply(inverse(multiply(v,u)),multiply(u,v)),X1),
inference(rw,[status(thm)],[c_0_834,c_0_835]) ).
cnf(c_0_838,plain,
( product(X1,multiply(X2,X3),multiply(X4,X3))
| ~ product(X1,X2,X4) ),
inference(spm,[status(thm)],[c_0_836,c_0_828]) ).
cnf(c_0_839,plain,
~ product(multiply(X1,multiply(u,v)),inverse(multiply(v,u)),X1),
inference(spm,[status(thm)],[c_0_837,c_0_838]) ).
cnf(c_0_840,plain,
( product(X1,X2,multiply(X3,X2))
| ~ product(X1,identity,X3) ),
inference(spm,[status(thm)],[c_0_836,c_0_823]) ).
cnf(c_0_841,axiom,
( product(X1,X2,X3)
| ~ product(X4,X5,X1)
| ~ product(X5,X2,X6)
| ~ product(X4,X6,X3) ),
i_0_19 ).
cnf(c_0_842,plain,
~ product(multiply(multiply(X1,inverse(multiply(v,u))),multiply(u,v)),identity,X1),
inference(spm,[status(thm)],[c_0_839,c_0_840]) ).
cnf(c_0_843,plain,
( product(X1,identity,multiply(X2,inverse(X3)))
| ~ product(X1,X3,X2) ),
inference(spm,[status(thm)],[c_0_836,c_0_825]) ).
cnf(c_0_844,plain,
( product(X1,identity,X2)
| ~ product(X3,X4,X2)
| ~ product(X3,X4,X1) ),
inference(spm,[status(thm)],[c_0_841,c_0_827]) ).
cnf(c_0_845,plain,
~ product(multiply(multiply(multiply(X1,inverse(X2)),inverse(multiply(v,u))),multiply(u,v)),X2,X1),
inference(spm,[status(thm)],[c_0_842,c_0_843]) ).
cnf(c_0_846,plain,
( product(X1,identity,multiply(X2,X3))
| ~ product(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_844,c_0_828]) ).
cnf(c_0_847,plain,
inverse(identity) = identity,
i_0_618 ).
cnf(c_0_848,plain,
product(X1,multiply(inverse(X1),X2),X2),
inference(spm,[status(thm)],[c_0_829,c_0_828]) ).
cnf(c_0_849,plain,
~ product(X1,X2,multiply(multiply(multiply(X1,X2),inverse(multiply(v,u))),multiply(u,v))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_845,c_0_846]),c_0_847]),c_0_833]) ).
cnf(c_0_850,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(spm,[status(thm)],[c_0_831,c_0_848]) ).
cnf(c_0_851,axiom,
product(inverse(X1),X1,identity),
i_0_26 ).
cnf(c_0_852,plain,
~ product(X1,X2,multiply(multiply(X1,multiply(X2,multiply(u,v))),inverse(multiply(v,u)))),
inference(spm,[status(thm)],[c_0_849,c_0_838]) ).
cnf(c_0_853,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(spm,[status(thm)],[c_0_850,c_0_835]) ).
cnf(c_0_854,plain,
( product(X1,X2,X3)
| ~ product(X4,inverse(X2),X1)
| ~ product(X4,identity,X3) ),
inference(spm,[status(thm)],[c_0_841,c_0_851]) ).
cnf(c_0_855,plain,
( X1 = X2
| ~ product(X3,multiply(inverse(X3),X2),X1) ),
inference(spm,[status(thm)],[c_0_826,c_0_848]) ).
cnf(c_0_856,plain,
( product(inverse(X1),X2,X3)
| ~ product(X1,X3,X2) ),
inference(spm,[status(thm)],[c_0_824,c_0_851]) ).
cnf(c_0_857,plain,
( X1 = identity
| ~ product(inverse(X2),X2,X1) ),
inference(spm,[status(thm)],[c_0_826,c_0_851]) ).
cnf(c_0_858,plain,
~ product(X1,inverse(u),multiply(multiply(X1,v),inverse(multiply(v,u)))),
inference(spm,[status(thm)],[c_0_852,c_0_853]) ).
cnf(c_0_859,plain,
( product(multiply(X1,inverse(X2)),X2,X3)
| ~ product(X1,identity,X3) ),
inference(spm,[status(thm)],[c_0_854,c_0_828]) ).
cnf(c_0_860,plain,
( X1 = X2
| ~ product(X3,X1,multiply(X3,X2)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_855,c_0_856]),c_0_835]) ).
cnf(c_0_861,plain,
multiply(inverse(X1),X1) = identity,
inference(spm,[status(thm)],[c_0_857,c_0_828]) ).
cnf(c_0_862,plain,
( product(X1,X2,identity)
| ~ product(X3,inverse(X4),X2)
| ~ product(X1,X3,X4) ),
inference(spm,[status(thm)],[c_0_822,c_0_825]) ).
cnf(c_0_863,plain,
~ product(X1,identity,multiply(multiply(multiply(X1,u),v),inverse(multiply(v,u)))),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_858,c_0_859]),c_0_835]) ).
cnf(c_0_864,plain,
( X1 = X2
| ~ product(inverse(X2),X1,identity) ),
inference(spm,[status(thm)],[c_0_860,c_0_861]) ).
cnf(c_0_865,plain,
( product(X1,multiply(X2,inverse(X3)),identity)
| ~ product(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_862,c_0_828]) ).
cnf(c_0_866,plain,
~ product(X1,multiply(v,u),multiply(multiply(X1,u),v)),
inference(spm,[status(thm)],[c_0_863,c_0_843]) ).
cnf(c_0_867,plain,
( multiply(X1,inverse(X2)) = X3
| ~ product(inverse(X3),X1,X2) ),
inference(spm,[status(thm)],[c_0_864,c_0_865]) ).
cnf(c_0_868,plain,
~ product(X1,multiply(multiply(inverse(X1),u),v),multiply(v,u)),
inference(spm,[status(thm)],[c_0_866,c_0_856]) ).
cnf(c_0_869,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_867,c_0_848]),c_0_835]) ).
cnf(c_0_870,plain,
~ product(inverse(X1),multiply(multiply(X1,u),v),multiply(v,u)),
inference(spm,[status(thm)],[c_0_868,c_0_835]) ).
cnf(c_0_871,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(spm,[status(thm)],[c_0_853,c_0_869]) ).
cnf(c_0_872,axiom,
( subgroup2_member(X1)
| ~ subgroup2_member(X2)
| ~ subgroup2_member(X3)
| ~ product(X2,X3,X1) ),
i_0_23 ).
cnf(c_0_873,plain,
~ product(multiply(u,X1),multiply(inverse(X1),v),multiply(v,u)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_870,c_0_871]),c_0_835]) ).
cnf(c_0_874,axiom,
( subgroup1_member(X1)
| ~ subgroup1_member(X2)
| ~ subgroup1_member(X3)
| ~ product(X2,X3,X1) ),
i_0_24 ).
cnf(c_0_875,plain,
( subgroup2_member(X1)
| ~ subgroup2_member(multiply(inverse(X2),X1))
| ~ subgroup2_member(X2) ),
inference(spm,[status(thm)],[c_0_872,c_0_848]) ).
cnf(c_0_876,plain,
subgroup2_member(multiply(X1,multiply(inverse(u),inverse(X1)))),
i_0_653 ).
cnf(c_0_877,plain,
~ product(multiply(u,multiply(v,X1)),inverse(X1),multiply(v,u)),
inference(spm,[status(thm)],[c_0_873,c_0_871]) ).
cnf(c_0_878,plain,
( subgroup1_member(X1)
| ~ subgroup1_member(inverse(X2))
| ~ subgroup1_member(X3)
| ~ product(X2,X1,X3) ),
inference(spm,[status(thm)],[c_0_874,c_0_856]) ).
cnf(c_0_879,plain,
subgroup1_member(inverse(v)),
i_0_576 ).
cnf(c_0_880,plain,
( subgroup2_member(multiply(inverse(u),X1))
| ~ subgroup2_member(X1) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_875,c_0_876]),c_0_835]) ).
cnf(c_0_881,plain,
~ product(multiply(u,multiply(v,inverse(X1))),X1,multiply(v,u)),
inference(spm,[status(thm)],[c_0_877,c_0_835]) ).
cnf(c_0_882,plain,
( subgroup1_member(X1)
| ~ subgroup1_member(X2)
| ~ product(v,X1,X2) ),
inference(spm,[status(thm)],[c_0_878,c_0_879]) ).
cnf(c_0_883,plain,
( subgroup2_member(X1)
| ~ subgroup2_member(multiply(u,X1)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_880,c_0_850]),c_0_835]) ).
cnf(c_0_884,plain,
subgroup2_member(multiply(X1,multiply(multiply(X2,multiply(u,inverse(X2))),inverse(X1)))),
i_0_803 ).
cnf(c_0_885,plain,
( multiply(X1,X2) = multiply(X3,multiply(X4,X2))
| ~ product(X3,X4,X1) ),
inference(spm,[status(thm)],[c_0_831,c_0_838]) ).
cnf(c_0_886,plain,
~ product(multiply(u,multiply(v,inverse(multiply(X1,u)))),X1,v),
inference(spm,[status(thm)],[c_0_881,c_0_838]) ).
cnf(c_0_887,plain,
( product(X1,inverse(X2),X3)
| ~ product(X4,identity,X3)
| ~ product(X4,X2,X1) ),
inference(spm,[status(thm)],[c_0_841,c_0_825]) ).
cnf(c_0_888,plain,
( X1 = X2
| ~ product(identity,X2,X1) ),
inference(spm,[status(thm)],[c_0_826,c_0_823]) ).
cnf(c_0_889,hypothesis,
( X1 = identity
| ~ subgroup1_member(X1)
| ~ subgroup2_member(X1) ),
i_0_33 ).
cnf(c_0_890,plain,
( subgroup1_member(multiply(inverse(v),X1))
| ~ subgroup1_member(X1) ),
inference(spm,[status(thm)],[c_0_882,c_0_848]) ).
cnf(c_0_891,plain,
subgroup2_member(multiply(multiply(X1,multiply(u,inverse(X1))),inverse(u))),
inference(spm,[status(thm)],[c_0_883,c_0_884]) ).
cnf(c_0_892,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(spm,[status(thm)],[c_0_885,c_0_828]) ).
cnf(c_0_893,plain,
~ product(multiply(u,multiply(v,X1)),inverse(multiply(u,X1)),v),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_886,c_0_871]),c_0_835]) ).
cnf(c_0_894,plain,
( product(X1,inverse(X2),X3)
| ~ product(X3,X2,X1) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_887,c_0_828]),c_0_833]) ).
cnf(c_0_895,plain,
multiply(X1,multiply(identity,inverse(X1))) = identity,
i_0_667 ).
cnf(c_0_896,plain,
multiply(identity,X1) = X1,
inference(spm,[status(thm)],[c_0_888,c_0_828]) ).
cnf(c_0_897,hypothesis,
( multiply(inverse(v),X1) = identity
| ~ subgroup1_member(X1)
| ~ subgroup2_member(multiply(inverse(v),X1)) ),
inference(spm,[status(thm)],[c_0_889,c_0_890]) ).
cnf(c_0_898,plain,
subgroup2_member(multiply(X1,multiply(u,multiply(inverse(X1),inverse(u))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_891,c_0_892]),c_0_892]) ).
cnf(c_0_899,plain,
subgroup1_member(multiply(X1,multiply(v,inverse(X1)))),
i_0_582 ).
cnf(c_0_900,plain,
~ product(v,multiply(u,X1),multiply(u,multiply(v,X1))),
inference(spm,[status(thm)],[c_0_893,c_0_894]) ).
cnf(c_0_901,plain,
multiply(X1,inverse(X1)) = identity,
inference(rw,[status(thm)],[c_0_895,c_0_896]) ).
cnf(c_0_902,plain,
product(inverse(X1),multiply(X1,X2),X2),
inference(spm,[status(thm)],[c_0_848,c_0_835]) ).
cnf(c_0_903,hypothesis,
multiply(inverse(v),multiply(u,multiply(v,inverse(u)))) = identity,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_897,c_0_898]),c_0_835]),c_0_835]),c_0_899])]) ).
cnf(c_0_904,plain,
~ product(v,identity,multiply(u,multiply(v,inverse(u)))),
inference(spm,[status(thm)],[c_0_900,c_0_901]) ).
cnf(c_0_905,hypothesis,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_902,c_0_903]),c_0_835]),c_0_904]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP617-1 : TPTP v9.2.1. Released v3.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.34 % Computer : n020.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 18:46:20 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 194.89/108.08 % Version : CSE_E---1.7
% 194.89/108.08 % Problem : theBenchmark.p
% 194.89/108.08 % SZS status Unsatisfiable for theBenchmark.p
% 194.89/108.08 % SZS output start CNFRefutation
% See solution above
% 198.56/111.78 % Total time : 106.946s
%------------------------------------------------------------------------------