%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP436-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n008.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 : Fri Sep 25 01:34:05 PM UTC 2026
% Result : Unsatisfiable 8.41s 1.76s
% Output : CNFRefutation 8.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 2
% Syntax : Number of formulae : 184 ( 184 unt; 0 def)
% Number of atoms : 657 ( 183 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 16 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 3 prp; 0-4 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 574 ( 0 sgn 574 !; 0 ?; 570 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X0))))) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_1) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X0))))) = X3,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(cnf_transformation,[],[f2]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X4)))),multiply(X5,multiply(multiply(inverse(X5),inverse(X3)),X0))))) = X4,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),inverse(X4))),multiply(X4,multiply(X2,X0))))) = X3,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),multiply(inverse(X3),inverse(multiply(X4,X5))))))),inverse(multiply(X5,multiply(X3,X2)))) = X4,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(X4,X0))))) = multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X2,X4))),inverse(X1))),
inference(superposition,[status(thm)],[c_62,c_51]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),inverse(X3))),multiply(X3,multiply(X1,X4)))) = multiply(X5,inverse(multiply(multiply(X6,multiply(multiply(inverse(X6),inverse(X2)),inverse(X7))),multiply(X7,multiply(X4,X5))))),
inference(superposition,[status(thm)],[c_62,c_62]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X5,X2))),inverse(X6))),X0))))) = multiply(X6,multiply(X5,inverse(X1))),
inference(superposition,[status(thm)],[c_62,c_62]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(X2)),inverse(X3))),multiply(X3,multiply(X4,X0))))) = inverse(multiply(X5,multiply(X6,multiply(multiply(inverse(X6),inverse(multiply(X2,X5))),X4)))),
inference(superposition,[status(thm)],[c_60,c_51]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(inverse(multiply(multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X4))),inverse(X5))),multiply(X5,multiply(X3,X6)))),X0))),multiply(inverse(X6),inverse(multiply(X7,X8))))))),inverse(multiply(X8,X4))) = X7,
inference(superposition,[status(thm)],[c_62,c_63]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X4,multiply(multiply(inverse(X4),inverse(X5)),X6)))),multiply(X7,multiply(multiply(inverse(X7),inverse(inverse(multiply(X8,multiply(X9,multiply(multiply(inverse(X9),inverse(multiply(X3,X8))),multiply(inverse(X2),inverse(multiply(X5,X1))))))))),X0))))) = X6,
inference(superposition,[status(thm)],[c_63,c_60]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),multiply(inverse(X3),inverse(multiply(X4,X5))))))) = multiply(X6,inverse(multiply(inverse(multiply(X5,multiply(X3,X2))),multiply(X7,multiply(multiply(inverse(X7),inverse(X4)),X6))))),
inference(superposition,[status(thm)],[c_63,c_51]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : multiply(inverse(multiply(X0,multiply(X1,X2))),inverse(multiply(multiply(X3,multiply(multiply(inverse(X3),inverse(multiply(inverse(multiply(X4,multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X2,X4))),multiply(inverse(X1),inverse(multiply(X6,X0))))))),X7))),inverse(X8))),multiply(X8,X6)))) = X7,
inference(superposition,[status(thm)],[c_63,c_62]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(X2)),inverse(X3))),multiply(X3,multiply(inverse(multiply(X4,multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X6,X4))),multiply(inverse(X7),inverse(multiply(X2,X8))))))),X0))))) = inverse(multiply(X8,multiply(X7,X6))),
inference(superposition,[status(thm)],[c_63,c_62]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),inverse(X3))) = iPr_def_10(X1,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_76]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(X4,X0))))) = iPr_def_10(X2,X4,X1),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_76]) ).
tcf(c_165,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,iPr_def_10(X1,X0,X2),X3) = multiply(X2,multiply(X1,inverse(X3))),
inference(demodulation,[status(thm)],[c_80,c_163,c_164]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),X3)))) = iPr_def_10(multiply(inverse(X4),inverse(X2)),X3,X4),
inference(demodulation,[status(thm)],[c_121,c_164]) ).
tcf(c_178,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(X2,multiply(X0,X3)))) = iPr_def_10(multiply(inverse(X4),inverse(X1)),X3,X4),
inference(demodulation,[status(thm)],[c_79,c_163,c_164]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X4,multiply(multiply(inverse(X4),inverse(X5)),X0))))) = iPr_def_11(X1,X2,X3,X5),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_151]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),multiply(inverse(X3),inverse(multiply(X4,X5))))))) = iPr_def_11(X5,X3,X2,X4),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_151]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(multiply(inverse(X0),inverse(X1)),iPr_def_11(X2,X3,X4,X1),X0) = inverse(multiply(X2,multiply(X3,X4))),
inference(demodulation,[status(thm)],[c_160,c_164,c_182]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(inverse(multiply(X0,multiply(X1,X2))),inverse(multiply(iPr_def_10(iPr_def_11(X0,X1,X2,X3),X4,X5),multiply(X5,X3)))) = X4,
inference(demodulation,[status(thm)],[c_155,c_163,c_182]) ).
tcf(c_189,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(iPr_def_11(X0,X1,inverse(multiply(iPr_def_10(X2,X3,X4),multiply(X4,multiply(X2,X1)))),X5),inverse(multiply(X0,X3))) = X5,
inference(demodulation,[status(thm)],[c_148,c_163,c_182]) ).
tcf(c_202,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : iPr_def_11(inverse(multiply(X0,multiply(X1,X2))),X3,multiply(multiply(inverse(X3),inverse(X4)),X5),iPr_def_11(X0,X1,X2,X4)) = X5,
inference(demodulation,[status(thm)],[c_150,c_181,c_182]) ).
tcf(c_206,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(iPr_def_10(X1,X2,X3),multiply(X3,multiply(X1,X0))))) = X2,
inference(demodulation,[status(thm)],[c_62,c_163]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(X0,X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),X3),X2) = X3,
inference(demodulation,[status(thm)],[c_60,c_181]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_11(X0,X1,X2,X3),inverse(multiply(X0,multiply(X1,X2)))) = X3,
inference(demodulation,[status(thm)],[c_63,c_182]) ).
tcf(c_386,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_11(multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),inverse(X3))),X3,multiply(X1,X4),X2) = X4,
inference(superposition,[status(thm)],[c_51,c_207]) ).
tcf(c_402,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),inverse(multiply(X1,iPr_def_10(X2,X1,X0)))) = X2,
inference(superposition,[status(thm)],[c_163,c_51]) ).
tcf(c_430,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,multiply(inverse(X1),inverse(multiply(X2,multiply(X3,multiply(X0,inverse(X1)))))),X3) = X2,
inference(superposition,[status(thm)],[c_164,c_51]) ).
tcf(c_455,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(iPr_def_10(X0,multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),inverse(X4)))),X5),multiply(X5,multiply(X0,X6)))) = iPr_def_10(X3,X6,X4),
inference(superposition,[status(thm)],[c_51,c_178]) ).
tcf(c_476,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : iPr_def_10(X0,inverse(multiply(iPr_def_10(X1,X2,X3),multiply(X3,multiply(X1,X0)))),X4) = multiply(X5,multiply(multiply(inverse(X5),inverse(X2)),inverse(X4))),
inference(superposition,[status(thm)],[c_178,c_165]) ).
tcf(c_479,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(X2,multiply(X0,X3)))) = inverse(multiply(iPr_def_10(X4,X1,X5),multiply(X5,multiply(X4,X3)))),
inference(superposition,[status(thm)],[c_178,c_178]) ).
tcf(c_591,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(X2,multiply(X0,multiply(inverse(X3),inverse(X4)))))) = iPr_def_11(inverse(multiply(X5,multiply(X6,X7))),X3,X1,iPr_def_11(X5,X6,X7,X4)),
inference(superposition,[status(thm)],[c_206,c_202]) ).
tcf(c_594,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : iPr_def_11(inverse(multiply(X0,multiply(X1,X2))),multiply(X3,multiply(X4,X5)),multiply(X6,X7),iPr_def_11(X0,X1,X2,multiply(iPr_def_10(iPr_def_11(X3,X4,X5,X8),X6,X9),multiply(X9,X8)))) = X7,
inference(superposition,[status(thm)],[c_188,c_202]) ).
tcf(c_606,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(multiply(inverse(X0),inverse(X1)),inverse(X2),X0) = inverse(multiply(X3,iPr_def_10(X1,X3,X2))),
inference(superposition,[status(thm)],[c_163,c_168]) ).
tcf(c_674,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_10(X0,X1,X2),X2,multiply(X0,X3),X1) = X3,
inference(demodulation,[status(thm)],[c_386,c_163]) ).
tcf(c_675,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(X2,multiply(X0,X3)))) = iPr_def_12(X1,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_479]) ).
tcf(c_678,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),inverse(X2))) = iPr_def_10(X3,iPr_def_12(X1,X3),X2),
inference(demodulation,[status(thm)],[c_476,c_675]) ).
tcf(c_689,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_12(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),inverse(X3)))),X4) = iPr_def_10(X2,X4,X3),
inference(demodulation,[status(thm)],[c_455,c_675]) ).
tcf(c_690,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(multiply(X0,iPr_def_10(X1,X0,X2)),X3) = iPr_def_10(X1,X3,X2),
inference(demodulation,[status(thm)],[c_689,c_163]) ).
tcf(c_692,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : iPr_def_11(inverse(multiply(X0,multiply(X1,X2))),X3,X4,iPr_def_11(X0,X1,X2,X5)) = iPr_def_12(X4,multiply(inverse(X3),inverse(X5))),
inference(demodulation,[status(thm)],[c_591,c_675]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : iPr_def_12(multiply(X0,X1),multiply(inverse(multiply(X2,multiply(X3,X4))),inverse(multiply(iPr_def_10(iPr_def_11(X2,X3,X4,X5),X0,X6),multiply(X6,X5))))) = X1,
inference(demodulation,[status(thm)],[c_594,c_692]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i] : iPr_def_12(multiply(X0,X1),X0) = X1,
inference(demodulation,[status(thm)],[c_713,c_188]) ).
tcf(c_751,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_11(X0,X1,iPr_def_12(X2,X1),X3),inverse(multiply(X0,X2))) = X3,
inference(demodulation,[status(thm)],[c_189,c_675]) ).
tcf(c_752,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_12(X1,X0)) = X1,
inference(demodulation,[status(thm)],[c_206,c_675]) ).
tcf(c_753,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(multiply(inverse(X0),inverse(X1)),X2,X0) = iPr_def_12(X1,X2),
inference(demodulation,[status(thm)],[c_178,c_675]) ).
tcf(c_754,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,iPr_def_11(X1,X2,X3,X0)) = inverse(multiply(X1,multiply(X2,X3))),
inference(demodulation,[status(thm)],[c_187,c_753]) ).
tcf(c_1602,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,multiply(inverse(X1),inverse(multiply(X2,X3)))) = iPr_def_11(X3,X1,X0,X2),
inference(superposition,[status(thm)],[c_752,c_207]) ).
tcf(c_1633,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_12(X0,X1),X2,multiply(multiply(inverse(X2),inverse(X0)),X3),X1) = X3,
inference(superposition,[status(thm)],[c_753,c_674]) ).
tcf(c_1637,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,iPr_def_10(X1,X0,X2)) = multiply(X3,iPr_def_10(X1,X3,X2)),
inference(superposition,[status(thm)],[c_690,c_752]) ).
tcf(c_1705,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(iPr_def_11(iPr_def_10(X0,X1,X2),X2,multiply(X0,X3),X4),iPr_def_12(X1,X3)) = X4,
inference(superposition,[status(thm)],[c_675,c_208]) ).
tcf(c_1754,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,multiply(inverse(X1),inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),inverse(X0)),inverse(X1))))))) = X2,
inference(superposition,[status(thm)],[c_430,c_753]) ).
tcf(c_1796,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),iPr_def_10(multiply(inverse(X1),inverse(X2)),inverse(X0),X1)) = X2,
inference(superposition,[status(thm)],[c_606,c_402]) ).
tcf(c_1829,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,iPr_def_10(X2,X1,X3)))),inverse(X4))) = iPr_def_10(X5,iPr_def_10(X2,X5,X3),X4),
inference(superposition,[status(thm)],[c_690,c_678]) ).
tcf(c_1844,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,iPr_def_12(multiply(X1,X2),X0),X3) = iPr_def_10(X1,X2,X3),
inference(superposition,[status(thm)],[c_678,c_163]) ).
tcf(c_1855,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(multiply(inverse(X0),inverse(X1)),multiply(inverse(X2),inverse(multiply(X3,iPr_def_10(X4,iPr_def_12(X1,X4),X2)))),X0) = X3,
inference(superposition,[status(thm)],[c_678,c_430]) ).
tcf(c_1857,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(iPr_def_12(X0,X1),multiply(X2,multiply(multiply(inverse(X2),inverse(X0)),inverse(X3))),X4) = multiply(X3,multiply(X1,inverse(X4))),
inference(superposition,[status(thm)],[c_678,c_165]) ).
tcf(c_1865,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),inverse(X2))) = multiply(X3,multiply(multiply(inverse(X3),inverse(X1)),inverse(X2))),
inference(superposition,[status(thm)],[c_678,c_678]) ).
tcf(c_1866,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,iPr_def_10(X1,X0,X2)) = iPr_def_13(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_1637]) ).
tcf(c_1868,plain,
! [X0: $i,X1: $i] : iPr_def_13(multiply(inverse(X0),inverse(X1)),X0) = X1,
inference(demodulation,[status(thm)],[c_1796,c_1866]) ).
tcf(c_1879,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),inverse(X2))),X2,X1,X3) = X3,
inference(demodulation,[status(thm)],[c_1754,c_1602]) ).
tcf(c_1884,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),inverse(X2))) = iPr_def_14(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_1865]) ).
tcf(c_1887,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,multiply(inverse(X1),inverse(multiply(X2,iPr_def_10(X3,iPr_def_12(X0,X3),X1))))) = X2,
inference(demodulation,[status(thm)],[c_1855,c_753]) ).
tcf(c_1894,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(iPr_def_12(X0,X1),iPr_def_14(X0,X2),X3) = multiply(X2,multiply(X1,inverse(X3))),
inference(demodulation,[status(thm)],[c_1857,c_1884]) ).
tcf(c_1905,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,iPr_def_10(X1,X0,X2),X3) = iPr_def_14(iPr_def_13(X1,X2),X3),
inference(demodulation,[status(thm)],[c_1829,c_1866,c_1884]) ).
tcf(c_2003,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_12(X1,X0),X2) = iPr_def_14(X1,X2),
inference(demodulation,[status(thm)],[c_678,c_1884]) ).
tcf(c_2004,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,inverse(X2))) = iPr_def_14(iPr_def_13(X1,X0),X2),
inference(demodulation,[status(thm)],[c_165,c_1905]) ).
tcf(c_2157,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_12(X0,X1),iPr_def_14(X0,X2)) = iPr_def_13(X1,X2),
inference(superposition,[status(thm)],[c_2003,c_1866]) ).
tcf(c_2158,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,iPr_def_12(X1,multiply(inverse(X2),inverse(X0)))) = iPr_def_14(X1,X2),
inference(superposition,[status(thm)],[c_2003,c_753]) ).
tcf(c_2192,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(iPr_def_14(iPr_def_13(X0,X1),X2),X1) = multiply(X0,inverse(X2)),
inference(superposition,[status(thm)],[c_2004,c_714]) ).
tcf(c_2209,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(multiply(X0,X1),X2) = iPr_def_10(X0,X1,X2),
inference(superposition,[status(thm)],[c_1844,c_2003]) ).
tcf(c_2388,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(X2)),inverse(X3))),multiply(X3,X2)))) = X0,
inference(superposition,[status(thm)],[c_1879,c_208]) ).
tcf(c_2391,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(iPr_def_12(X2,X3))),inverse(X3))),X2))) = X0,
inference(superposition,[status(thm)],[c_1879,c_751]) ).
tcf(c_2392,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),inverse(X2))),multiply(X2,X1))) = iPr_def_12(X3,X3),
inference(superposition,[status(thm)],[c_1879,c_754]) ).
tcf(c_2413,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,multiply(multiply(inverse(X1),inverse(multiply(X2,iPr_def_10(X3,iPr_def_12(X4,X3),X1)))),inverse(X5))) = iPr_def_10(X2,iPr_def_14(X4,X0),X5),
inference(superposition,[status(thm)],[c_1887,c_1894]) ).
tcf(c_2418,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(X0),inverse(multiply(X1,iPr_def_10(X2,iPr_def_12(X3,X2),X0)))),X1) = X3,
inference(superposition,[status(thm)],[c_1887,c_752]) ).
tcf(c_2419,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_10(X0,iPr_def_12(X1,X0),X2),X2,X1,X3) = X3,
inference(superposition,[status(thm)],[c_1887,c_1602]) ).
tcf(c_2425,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_14(X0,X1),X1,X0,X2) = X2,
inference(demodulation,[status(thm)],[c_2419,c_2003]) ).
tcf(c_2435,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(X0),inverse(multiply(X1,iPr_def_14(X2,X0)))),X1) = X2,
inference(demodulation,[status(thm)],[c_2418,c_2003]) ).
tcf(c_2465,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_14(X0,X1),multiply(X1,X0))) = iPr_def_12(X2,X2),
inference(demodulation,[status(thm)],[c_2392,c_1868,c_2004]) ).
tcf(c_2466,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(multiply(iPr_def_14(iPr_def_12(X1,X2),X2),X1))) = X0,
inference(demodulation,[status(thm)],[c_2391,c_1868,c_2004]) ).
tcf(c_2467,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(multiply(iPr_def_14(X1,X2),multiply(X2,X1)))) = X0,
inference(demodulation,[status(thm)],[c_2388,c_1868,c_2004]) ).
tcf(c_2526,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_14(iPr_def_13(multiply(inverse(X0),inverse(multiply(X1,iPr_def_14(X2,X0)))),X3),X4) = iPr_def_10(X1,iPr_def_14(X2,X3),X4),
inference(demodulation,[status(thm)],[c_2413,c_2003,c_2004]) ).
tcf(c_3915,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_10(X0,X1,X2),X2,multiply(X0,X1),X3) = X3,
inference(superposition,[status(thm)],[c_2209,c_2425]) ).
tcf(c_3979,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(iPr_def_11(iPr_def_10(X0,X1,X2),X2,multiply(X0,X1),X3),inverse(multiply(iPr_def_14(X4,X5),multiply(X5,X4)))) = X3,
inference(superposition,[status(thm)],[c_2465,c_1705]) ).
tcf(c_3991,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(iPr_def_14(X0,X1),multiply(X1,X0))) = inverse(multiply(iPr_def_14(X2,X3),multiply(X3,X2))),
inference(superposition,[status(thm)],[c_2465,c_2465]) ).
tcf(c_4016,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_14(iPr_def_12(X0,X1),X1),X0) = iPr_def_13(inverse(X2),X2),
inference(superposition,[status(thm)],[c_2466,c_1868]) ).
tcf(c_4028,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_11(iPr_def_12(X0,X1),X2,multiply(inverse(X2),inverse(X0)),X1) = inverse(multiply(iPr_def_14(iPr_def_12(X3,X4),X4),X3)),
inference(superposition,[status(thm)],[c_2466,c_1633]) ).
tcf(c_4030,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(iPr_def_12(iPr_def_10(X0,iPr_def_12(X1,X0),X2),X3),X3) = iPr_def_12(X1,inverse(X2)),
inference(superposition,[status(thm)],[c_2466,c_1887]) ).
tcf(c_4055,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_11(inverse(multiply(iPr_def_14(X0,X1),multiply(X1,X0))),X2,X3,X4) = iPr_def_12(X3,multiply(inverse(X2),inverse(X4))),
inference(superposition,[status(thm)],[c_2467,c_1602]) ).
tcf(c_4061,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_14(X0,X1),multiply(X1,X0)) = iPr_def_13(inverse(X2),X2),
inference(superposition,[status(thm)],[c_2467,c_1868]) ).
tcf(c_4074,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_11(iPr_def_12(X0,X1),X2,multiply(inverse(X2),inverse(X0)),X1) = inverse(multiply(iPr_def_14(X3,X4),multiply(X4,X3))),
inference(superposition,[status(thm)],[c_2467,c_1633]) ).
tcf(c_4083,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(X0,inverse(multiply(iPr_def_14(X1,X2),multiply(X2,X1)))) = iPr_def_14(multiply(inverse(X3),inverse(X0)),X3),
inference(superposition,[status(thm)],[c_2465,c_2158]) ).
tcf(c_4141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(iPr_def_13(multiply(inverse(X0),inverse(multiply(inverse(X1),iPr_def_14(X2,X0)))),X3),X1) = multiply(X3,X2),
inference(superposition,[status(thm)],[c_2435,c_2004]) ).
tcf(c_4158,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_12(iPr_def_14(X0,X1),X2),X2) = iPr_def_12(X0,inverse(X1)),
inference(demodulation,[status(thm)],[c_4030,c_2003]) ).
tcf(c_4164,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_14(X0,X1),multiply(X1,X0))) = iPr_def_15,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_3991]) ).
tcf(c_4168,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(X0),iPr_def_14(X1,X2),X0) = multiply(X2,X1),
inference(demodulation,[status(thm)],[c_4141,c_2526]) ).
tcf(c_4171,plain,
! [X0: $i,X1: $i] : iPr_def_14(multiply(inverse(X0),inverse(X1)),X0) = iPr_def_12(X1,iPr_def_15),
inference(demodulation,[status(thm)],[c_4083,c_4164]) ).
tcf(c_4172,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),inverse(X1),X0) = iPr_def_12(X1,iPr_def_15),
inference(demodulation,[status(thm)],[c_4171,c_2209]) ).
tcf(c_4192,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_12(X0,X1),X2,multiply(inverse(X2),inverse(X0)),X1) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4074,c_4164]) ).
tcf(c_4194,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,multiply(inverse(X1),inverse(X2))) = iPr_def_11(iPr_def_15,X1,X0,X2),
inference(demodulation,[status(thm)],[c_4055,c_4164]) ).
tcf(c_4196,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_14(iPr_def_12(X0,X1),X1),X0)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4028,c_4192]) ).
tcf(c_4205,plain,
! [X0: $i] : multiply(X0,iPr_def_15) = X0,
inference(demodulation,[status(thm)],[c_3979,c_3915,c_4164]) ).
tcf(c_4226,plain,
! [X0: $i] : iPr_def_12(X0,X0) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2465,c_4164]) ).
tcf(c_4227,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,iPr_def_11(iPr_def_15,X1,X2,X0)) = iPr_def_14(X2,X1),
inference(demodulation,[status(thm)],[c_2158,c_4194]) ).
tcf(c_4231,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_15,multiply(X0,X1))) = iPr_def_14(X1,X0),
inference(demodulation,[status(thm)],[c_4227,c_754]) ).
tcf(c_4953,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_15,iPr_def_14(X0,X1)) = iPr_def_13(X0,X1),
inference(superposition,[status(thm)],[c_4226,c_2157]) ).
tcf(c_4956,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_15,X1) = iPr_def_14(X0,X1),
inference(superposition,[status(thm)],[c_4226,c_2003]) ).
tcf(c_4972,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_14(X0,multiply(inverse(X1),inverse(multiply(X0,iPr_def_14(X2,X1))))),X2)) = iPr_def_15,
inference(superposition,[status(thm)],[c_2435,c_4164]) ).
tcf(c_5001,plain,
! [X0: $i] : inverse(iPr_def_14(iPr_def_12(iPr_def_15,X0),X0)) = iPr_def_15,
inference(superposition,[status(thm)],[c_4205,c_4196]) ).
tcf(c_5008,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(iPr_def_13(X0,X1),multiply(iPr_def_14(iPr_def_12(X2,X3),X3),X2)) = multiply(X1,multiply(X0,iPr_def_15)),
inference(superposition,[status(thm)],[c_4196,c_2004]) ).
tcf(c_5015,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(multiply(iPr_def_14(iPr_def_12(X0,X1),X1),X0),iPr_def_15) = iPr_def_10(inverse(X2),iPr_def_15,X2),
inference(superposition,[status(thm)],[c_4196,c_4172]) ).
tcf(c_5017,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(multiply(iPr_def_14(iPr_def_12(X0,X1),X1),X0),X2) = iPr_def_10(multiply(inverse(X3),iPr_def_15),X2,X3),
inference(superposition,[status(thm)],[c_4196,c_753]) ).
tcf(c_5032,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_12(X0,X1),X1) = inverse(multiply(iPr_def_15,X0)),
inference(superposition,[status(thm)],[c_752,c_4231]) ).
tcf(c_5035,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,multiply(inverse(X1),inverse(multiply(X0,iPr_def_14(X2,X1))))) = inverse(multiply(iPr_def_15,X2)),
inference(superposition,[status(thm)],[c_2435,c_4231]) ).
tcf(c_5036,plain,
! [X0: $i] : inverse(multiply(iPr_def_15,X0)) = iPr_def_14(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_4205,c_4231]) ).
tcf(c_5158,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_13(iPr_def_15,multiply(iPr_def_14(iPr_def_12(X0,X1),X1),X0)) = multiply(iPr_def_14(X2,X3),multiply(X3,X2)),
inference(superposition,[status(thm)],[c_4196,c_4061]) ).
tcf(c_5178,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(iPr_def_14(multiply(iPr_def_14(X0,X1),multiply(X1,X0)),X2),X3) = multiply(inverse(X3),inverse(X2)),
inference(superposition,[status(thm)],[c_4061,c_2192]) ).
tcf(c_5182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_14(iPr_def_12(X0,X1),X1),X0) = multiply(iPr_def_14(X2,X3),multiply(X3,X2)),
inference(superposition,[status(thm)],[c_4061,c_4016]) ).
tcf(c_5185,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_15,iPr_def_14(X0,X1)) = iPr_def_12(X0,inverse(X1)),
inference(superposition,[status(thm)],[c_4226,c_4158]) ).
tcf(c_5200,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_12(X0,X1),X1) = iPr_def_14(iPr_def_15,X0),
inference(demodulation,[status(thm)],[c_5032,c_5036]) ).
tcf(c_5219,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_14(X0,X1),multiply(X1,X0)) = multiply(iPr_def_14(iPr_def_15,X2),X2),
inference(demodulation,[status(thm)],[c_5182,c_5200]) ).
tcf(c_5220,plain,
! [X0: $i] : multiply(iPr_def_14(iPr_def_15,X0),X0) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_5219]) ).
tcf(c_5221,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14(X0,X1),multiply(X1,X0)) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_5219]) ).
tcf(c_5236,plain,
! [X0: $i] : iPr_def_14(inverse(X0),X0) = iPr_def_12(iPr_def_16,iPr_def_15),
inference(demodulation,[status(thm)],[c_5015,c_4956,c_5200,c_5220]) ).
tcf(c_5242,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,multiply(inverse(X1),inverse(multiply(X0,iPr_def_14(X2,X1))))) = iPr_def_14(iPr_def_15,X2),
inference(demodulation,[status(thm)],[c_5035,c_5036]) ).
tcf(c_5245,plain,
inverse(iPr_def_16) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4972,c_5220,c_5242]) ).
tcf(c_5249,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(X1)) = iPr_def_12(iPr_def_14(iPr_def_16,X1),X0),
inference(demodulation,[status(thm)],[c_5178,c_5221]) ).
tcf(c_5254,plain,
iPr_def_13(iPr_def_15,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_5158,c_5200,c_5220,c_5221]) ).
tcf(c_5270,plain,
! [X0: $i,X1: $i] : iPr_def_10(multiply(inverse(X0),iPr_def_15),X1,X0) = iPr_def_12(iPr_def_16,X1),
inference(demodulation,[status(thm)],[c_5017,c_5200,c_5220]) ).
tcf(c_5271,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),X1,X0) = iPr_def_12(iPr_def_16,X1),
inference(demodulation,[status(thm)],[c_5270,c_4205]) ).
tcf(c_5273,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,iPr_def_15)) = iPr_def_14(iPr_def_13(X1,X0),iPr_def_16),
inference(demodulation,[status(thm)],[c_5008,c_5200,c_5220]) ).
tcf(c_5274,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_13(X0,X1),iPr_def_16) = multiply(X1,X0),
inference(demodulation,[status(thm)],[c_5273,c_4205]) ).
tcf(c_5336,plain,
! [X0: $i,X1: $i] : iPr_def_13(iPr_def_12(iPr_def_14(iPr_def_16,X0),X1),X1) = X0,
inference(demodulation,[status(thm)],[c_1868,c_5249]) ).
tcf(c_5340,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_16,iPr_def_14(X0,X1)) = multiply(X1,X0),
inference(demodulation,[status(thm)],[c_4168,c_5271]) ).
tcf(c_5482,plain,
iPr_def_14(iPr_def_15,iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_5220,c_4205]) ).
tcf(c_5492,plain,
iPr_def_14(iPr_def_15,iPr_def_15) = inverse(iPr_def_15),
inference(superposition,[status(thm)],[c_4205,c_5036]) ).
tcf(c_5505,plain,
iPr_def_12(iPr_def_16,iPr_def_15) = iPr_def_14(iPr_def_15,iPr_def_16),
inference(superposition,[status(thm)],[c_5245,c_5236]) ).
tcf(c_5547,plain,
inverse(iPr_def_14(iPr_def_15,iPr_def_15)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_5001,c_5200]) ).
tcf(c_6459,plain,
inverse(iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_5492,c_5482]) ).
tcf(c_6471,plain,
iPr_def_14(iPr_def_15,iPr_def_14(iPr_def_15,iPr_def_15)) = iPr_def_12(iPr_def_16,iPr_def_15),
inference(superposition,[status(thm)],[c_5547,c_5236]) ).
tcf(c_6478,plain,
multiply(iPr_def_12(iPr_def_16,iPr_def_15),iPr_def_16) = iPr_def_16,
inference(superposition,[status(thm)],[c_5505,c_5220]) ).
tcf(c_6491,plain,
iPr_def_12(iPr_def_15,inverse(iPr_def_15)) = iPr_def_12(iPr_def_16,iPr_def_15),
inference(demodulation,[status(thm)],[c_6471,c_5185]) ).
tcf(c_6576,plain,
iPr_def_12(iPr_def_16,iPr_def_12(iPr_def_16,iPr_def_15)) = iPr_def_16,
inference(superposition,[status(thm)],[c_6478,c_714]) ).
tcf(c_6627,plain,
iPr_def_12(iPr_def_15,iPr_def_16) = iPr_def_12(iPr_def_16,iPr_def_15),
inference(superposition,[status(thm)],[c_6459,c_6491]) ).
tcf(c_6711,plain,
multiply(iPr_def_16,iPr_def_15) = iPr_def_14(iPr_def_16,iPr_def_16),
inference(superposition,[status(thm)],[c_5254,c_5274]) ).
tcf(c_6746,plain,
! [X0: $i] : iPr_def_13(iPr_def_15,iPr_def_14(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_4226,c_5336]) ).
tcf(c_6748,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_12(iPr_def_14(iPr_def_16,X1),X0)) = iPr_def_14(X1,iPr_def_16),
inference(superposition,[status(thm)],[c_5336,c_5274]) ).
tcf(c_6788,plain,
iPr_def_14(iPr_def_16,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_6711,c_4205]) ).
tcf(c_6835,plain,
! [X0: $i] : iPr_def_14(X0,iPr_def_16) = iPr_def_14(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_6748,c_752]) ).
tcf(c_7002,plain,
multiply(iPr_def_16,iPr_def_16) = iPr_def_12(iPr_def_16,iPr_def_16),
inference(superposition,[status(thm)],[c_6788,c_5340]) ).
tcf(c_7025,plain,
iPr_def_12(iPr_def_16,iPr_def_12(iPr_def_15,iPr_def_16)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_6576,c_6627]) ).
tcf(c_7031,plain,
multiply(iPr_def_16,iPr_def_16) = iPr_def_15,
inference(demodulation,[status(thm)],[c_7002,c_4226]) ).
tcf(c_7079,plain,
iPr_def_12(iPr_def_15,iPr_def_16) = iPr_def_16,
inference(superposition,[status(thm)],[c_7031,c_714]) ).
tcf(c_7286,plain,
! [X0: $i] : iPr_def_12(iPr_def_16,iPr_def_14(X0,iPr_def_16)) = multiply(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_6835,c_5340]) ).
tcf(c_7288,plain,
! [X0: $i] : multiply(iPr_def_15,iPr_def_14(X0,iPr_def_16)) = iPr_def_13(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_6835,c_4953]) ).
tcf(c_7292,plain,
! [X0: $i] : iPr_def_13(iPr_def_15,iPr_def_14(X0,iPr_def_16)) = X0,
inference(superposition,[status(thm)],[c_6835,c_6746]) ).
tcf(c_7349,plain,
! [X0: $i] : iPr_def_13(X0,iPr_def_16) = iPr_def_13(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_7288,c_4953]) ).
tcf(c_7351,plain,
! [X0: $i] : multiply(X0,iPr_def_16) = multiply(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_7286,c_5340]) ).
tcf(c_7585,plain,
iPr_def_12(iPr_def_16,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_7025,c_7079]) ).
tcf(c_7587,plain,
iPr_def_12(iPr_def_16,iPr_def_15) = iPr_def_16,
inference(demodulation,[status(thm)],[c_6627,c_7079]) ).
tcf(c_7589,plain,
iPr_def_15 = iPr_def_16,
inference(demodulation,[status(thm)],[c_7585,c_4226]) ).
tcf(c_7613,plain,
iPr_def_14(iPr_def_15,iPr_def_15) = iPr_def_15,
inference(demodulation,[status(thm)],[c_5482,c_7589]) ).
tcf(c_8516,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11(iPr_def_10(X0,iPr_def_16,X1),X1,multiply(X0,iPr_def_15),X2),iPr_def_16) = X2,
inference(superposition,[status(thm)],[c_7587,c_1705]) ).
tcf(c_8525,plain,
! [X0: $i] : multiply(iPr_def_12(iPr_def_15,X0),iPr_def_15) = iPr_def_13(X0,iPr_def_15),
inference(superposition,[status(thm)],[c_7613,c_2157]) ).
tcf(c_8541,plain,
! [X0: $i] : iPr_def_12(iPr_def_15,X0) = iPr_def_13(X0,iPr_def_15),
inference(demodulation,[status(thm)],[c_8525,c_4205]) ).
tcf(c_8556,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_16,iPr_def_11(iPr_def_10(X0,iPr_def_16,X1),X1,X0,X2)) = X2,
inference(demodulation,[status(thm)],[c_8516,c_4205,c_7351]) ).
tcf(c_8557,plain,
! [X0: $i] : multiply(iPr_def_15,X0) = X0,
inference(light_normalisation,[status(thm)],[c_8556,c_2425,c_4956,c_7589]) ).
tcf(c_8579,plain,
! [X0: $i] : iPr_def_14(iPr_def_15,X0) = inverse(X0),
inference(demodulation,[status(thm)],[c_5036,c_8557]) ).
tcf(c_8580,plain,
! [X0: $i,X1: $i] : iPr_def_13(X0,X1) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_4953,c_8557]) ).
tcf(c_8603,plain,
! [X0: $i] : iPr_def_13(iPr_def_15,X0) = inverse(X0),
inference(demodulation,[status(thm)],[c_8579,c_8580]) ).
tcf(c_8739,plain,
! [X0: $i] : iPr_def_13(iPr_def_15,iPr_def_14(X0,iPr_def_15)) = X0,
inference(superposition,[status(thm)],[c_7589,c_7292]) ).
tcf(c_8747,plain,
! [X0: $i] : iPr_def_13(X0,iPr_def_15) = iPr_def_13(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_7589,c_7349]) ).
tcf(c_8767,plain,
! [X0: $i] : iPr_def_12(iPr_def_15,X0) = inverse(X0),
inference(demodulation,[status(thm)],[c_8747,c_8541,c_8603]) ).
tcf(c_8771,plain,
! [X0: $i] : inverse(iPr_def_12(iPr_def_15,X0)) = X0,
inference(demodulation,[status(thm)],[c_8739,c_8541,c_8580,c_8603]) ).
tcf(c_8849,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = iPr_def_15,
inference(superposition,[status(thm)],[c_8767,c_752]) ).
tcf(c_8856,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(superposition,[status(thm)],[c_8767,c_8771]) ).
tcf(c_9036,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_15,
inference(superposition,[status(thm)],[c_8856,c_8849]) ).
tcf(c_9404,plain,
multiply(inverse(b1),b1) != iPr_def_15,
inference(demodulation,[status(thm)],[c_52,c_9036]) ).
tcf(c_9405,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_9404,c_9036]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP436-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 14:46:39 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.40 Running UEQ theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 8.41/1.76 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 8.41/1.76 % SZS status Started for theBenchmark.p
% 8.41/1.76 % SZS status Unsatisfiable for theBenchmark.p
% 8.41/1.76
% 8.41/1.76 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.41/1.76
% 8.41/1.76 % ------ iProver source info
% 8.41/1.76
% 8.41/1.76 % git: date: 2026-07-19 20:42:38 +0200
% 8.41/1.76 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.41/1.76 % git: non_committed_changes: false
% 8.41/1.76
% 8.41/1.76 % ------ Parsing...% successful
% 8.41/1.76
% 8.41/1.76
% 8.41/1.76 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 8.41/1.76 % ------ Proving...
% 8.41/1.76 % ------ Problem Properties
% 8.41/1.76
% 8.41/1.76 %
% 8.41/1.76 % clauses 2
% 8.41/1.76 % conjectures 1
% 8.41/1.76 % EPR 0
% 8.41/1.76 % Horn 2
% 8.41/1.76 % unary 2
% 8.41/1.76 % binary 0
% 8.41/1.76 % lits 2
% 8.41/1.76 % lits eq 2
% 8.41/1.76 % fd_pure 0
% 8.41/1.76 % fd_pseudo 0
% 8.41/1.76 % fd_cond 0
% 8.41/1.76 % fd_pseudo_cond 0
% 8.41/1.76 % AC symbols 0
% 8.41/1.76
% 8.41/1.76 % ------ Input Options Time Limit: Unbounded
% 8.41/1.76
% 8.41/1.76
% 8.41/1.76 % ------
% 8.41/1.76 % Current options:
% 8.41/1.76 % ------
% 8.41/1.76
% 8.41/1.76
% 8.41/1.76 %
% 8.41/1.76
% 8.41/1.76 % ------ Proving...
% 8.41/1.76 %
% 8.41/1.76
% 8.41/1.76 % SZS status Unsatisfiable for theBenchmark.p
% 8.41/1.76
% 8.41/1.76 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.41/1.76
% 8.41/1.76
%------------------------------------------------------------------------------