%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP442-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 : n004.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:07 PM UTC 2026
% Result : Unsatisfiable 9.18s 2.18s
% Output : CNFRefutation 9.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 2
% Syntax : Number of formulae : 124 ( 124 unt; 0 def)
% Number of atoms : 475 ( 123 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 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 : 5 ( 3 usr; 3 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 397 ( 0 sgn 397 !; 0 ?; 393 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = 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] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = 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,X6: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,multiply(multiply(X4,inverse(X4)),inverse(multiply(X5,multiply(X2,X3)))))),X5),inverse(multiply(X6,multiply(X0,X1))))))) = X6,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(X4,inverse(X4)),X2)))) = X3,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))),multiply(multiply(multiply(X4,inverse(X4)),X1),multiply(multiply(X5,inverse(X5)),X2)))) = X3,
inference(superposition,[status(thm)],[c_61,c_51]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(multiply(X4,multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X6,multiply(X7,X4)))),multiply(multiply(X8,inverse(X8)),X6))),X7),X2)))) = X3,
inference(superposition,[status(thm)],[c_61,c_61]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,multiply(X3,X5)))),
inference(superposition,[status(thm)],[c_61,c_61]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,multiply(X5,X2)))),multiply(multiply(X6,inverse(X6)),X4))),X5),inverse(multiply(X7,multiply(X0,X1))))))) = X7,
inference(superposition,[status(thm)],[c_51,c_60]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(multiply(X4,multiply(X5,multiply(multiply(X6,inverse(X6)),inverse(multiply(X7,multiply(X4,X5)))))),X7),X2)))) = X3,
inference(superposition,[status(thm)],[c_51,c_60]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))),multiply(multiply(multiply(X4,inverse(X4)),X1),multiply(multiply(multiply(X5,multiply(X6,multiply(multiply(X7,inverse(X7)),inverse(multiply(X8,multiply(X5,X6)))))),X8),X2)))) = X3,
inference(superposition,[status(thm)],[c_61,c_60]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(X0,multiply(multiply(multiply(multiply(X1,multiply(X2,multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,multiply(X1,X2)))))),X4),inverse(multiply(X5,multiply(X6,X0)))),multiply(multiply(X7,inverse(X7)),X5)))) = X6,
inference(superposition,[status(thm)],[c_60,c_51]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))) = iPr_def_10(X1,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_74]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = iPr_def_10(X1,X3,X5),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_74]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(X0,multiply(multiply(multiply(multiply(X1,multiply(X2,iPr_def_10(X3,X1,X2))),X3),inverse(multiply(X4,multiply(X5,X0)))),multiply(multiply(X6,inverse(X6)),X4)))) = X5,
inference(demodulation,[status(thm)],[c_100,c_107]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(multiply(X3,multiply(X4,iPr_def_10(X5,X3,X4))),X5),X1)))) = X2,
inference(demodulation,[status(thm)],[c_96,c_107]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(iPr_def_10(X3,X4,X2),multiply(multiply(X5,inverse(X5)),X3))),X4),inverse(multiply(X6,multiply(X0,X1))))))) = X6,
inference(demodulation,[status(thm)],[c_93,c_107]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(multiply(multiply(X3,inverse(X3)),X0),multiply(multiply(multiply(X4,multiply(X5,iPr_def_10(X6,X4,X5))),X6),X1)))) = X2,
inference(demodulation,[status(thm)],[c_98,c_107]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(multiply(X3,multiply(iPr_def_10(X4,X5,X3),multiply(multiply(X6,inverse(X6)),X4))),X5),X1)))) = X2,
inference(demodulation,[status(thm)],[c_73,c_107]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1)))) = X2,
inference(demodulation,[status(thm)],[c_51,c_107]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(X3,inverse(X3)),X1)))) = X2,
inference(demodulation,[status(thm)],[c_61,c_107]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),inverse(multiply(X5,multiply(X0,X1))))))) = X5,
inference(demodulation,[status(thm)],[c_60,c_107]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2),inverse(multiply(X3,multiply(X4,X5)))) = iPr_def_10(X3,X4,X5),
inference(superposition,[status(thm)],[c_124,c_107]) ).
tcf(c_221,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(X5,iPr_def_10(X6,X4,X5))),X6),X7)))) = iPr_def_10(X1,X3,X7),
inference(superposition,[status(thm)],[c_124,c_108]) ).
tcf(c_222,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(iPr_def_10(X5,X6,X4),multiply(multiply(X7,inverse(X7)),X5))),X6),X8)))) = iPr_def_10(X1,X3,X8),
inference(superposition,[status(thm)],[c_125,c_108]) ).
tcf(c_248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(multiply(X3,multiply(iPr_def_10(X4,X5,X3),multiply(multiply(multiply(X6,multiply(iPr_def_10(X7,X8,X6),multiply(multiply(multiply(X9,multiply(X10,iPr_def_10(X11,X9,X10))),X11),X7))),X8),X4))),X5),X1)))) = X2,
inference(superposition,[status(thm)],[c_110,c_115]) ).
tcf(c_274,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),iPr_def_10(X1,X2,X3)),multiply(multiply(multiply(X4,inverse(X4)),multiply(multiply(X5,inverse(X5)),X1)),multiply(multiply(X6,inverse(X6)),multiply(multiply(X7,inverse(X7)),X2))))) = multiply(multiply(X8,inverse(X8)),X3),
inference(superposition,[status(thm)],[c_108,c_71]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),iPr_def_10(X3,X4,X1)),multiply(multiply(X5,inverse(X5)),multiply(multiply(X6,inverse(X6)),X3))))) = multiply(multiply(multiply(X7,multiply(X8,iPr_def_10(X9,X7,X8))),X9),X4),
inference(superposition,[status(thm)],[c_113,c_71]) ).
tcf(c_277,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),iPr_def_10(X5,X1,X3))))) = multiply(multiply(multiply(X6,multiply(iPr_def_10(X7,X8,X6),multiply(multiply(X9,inverse(X9)),X7))),X8),X5),
inference(superposition,[status(thm)],[c_115,c_71]) ).
tcf(c_280,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = multiply(multiply(multiply(X6,multiply(X7,iPr_def_10(X8,X6,X7))),X8),inverse(multiply(X1,multiply(X3,X5)))),
inference(superposition,[status(thm)],[c_126,c_71]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_10(X2,X3,X4)))),multiply(multiply(multiply(X5,inverse(X5)),X1),multiply(multiply(X6,inverse(X6)),multiply(X7,inverse(X7)))))) = inverse(multiply(X2,multiply(X3,X4))),
inference(superposition,[status(thm)],[c_107,c_71]) ).
tcf(c_312,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,multiply(X1,X2))),X0,X1) = X2,
inference(superposition,[status(thm)],[c_71,c_108]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(X5,iPr_def_10(X6,X4,X5))),X6),X7)))) = multiply(multiply(X8,inverse(X8)),inverse(multiply(X1,multiply(X3,X7)))),
inference(superposition,[status(thm)],[c_71,c_126]) ).
tcf(c_315,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),iPr_def_10(X5,X6,X1)),multiply(multiply(X7,inverse(X7)),multiply(multiply(X8,inverse(X8)),X5))))) = multiply(multiply(X9,inverse(X9)),X6),
inference(superposition,[status(thm)],[c_108,c_109]) ).
tcf(c_321,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),X5),multiply(multiply(X6,inverse(X6)),X7)))) = iPr_def_10(X1,X5,X7),
inference(superposition,[status(thm)],[c_125,c_109]) ).
tcf(c_323,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(multiply(multiply(multiply(X3,multiply(X4,iPr_def_10(X5,X3,X4))),X5),inverse(multiply(X6,iPr_def_10(X0,X1,X2)))),multiply(multiply(X7,inverse(X7)),X6)))) = multiply(X8,inverse(X8)),
inference(superposition,[status(thm)],[c_107,c_109]) ).
tcf(c_361,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(iPr_def_10(X5,X6,X4),multiply(multiply(X7,inverse(X7)),X5))),X6),iPr_def_10(X8,X1,X3))))) = multiply(multiply(X9,inverse(X9)),X8),
inference(superposition,[status(thm)],[c_108,c_111]) ).
tcf(c_366,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(multiply(multiply(multiply(X3,multiply(iPr_def_10(X4,X5,X3),multiply(multiply(X6,inverse(X6)),X4))),X5),X0),multiply(multiply(multiply(X7,multiply(iPr_def_10(X8,X9,X7),multiply(multiply(X10,inverse(X10)),X8))),X9),X1)))) = X2,
inference(superposition,[status(thm)],[c_115,c_111]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_10(X1,X2,X3))),X0,multiply(X4,inverse(X4))) = inverse(multiply(X1,multiply(X2,X3))),
inference(demodulation,[status(thm)],[c_281,c_108]) ).
tcf(c_457,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = iPr_def_11,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_323]) ).
tcf(c_467,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11,inverse(multiply(X0,multiply(X1,X2)))) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_313,c_221,c_457]) ).
tcf(c_470,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(iPr_def_11,X0),multiply(multiply(iPr_def_11,X1),multiply(iPr_def_11,X2)))) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_280,c_184,c_457]) ).
tcf(c_478,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1,X2),multiply(iPr_def_11,X0),multiply(iPr_def_11,X1)) = multiply(iPr_def_11,X2),
inference(demodulation,[status(thm)],[c_274,c_457,c_470]) ).
tcf(c_479,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,X1,iPr_def_10(X2,X0,X1)) = multiply(iPr_def_11,X2),
inference(demodulation,[status(thm)],[c_361,c_222,c_457]) ).
tcf(c_480,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1)) = multiply(iPr_def_11,X2),
inference(demodulation,[status(thm)],[c_315,c_321,c_457]) ).
tcf(c_481,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1))),X2),X3) = multiply(iPr_def_11,X3),
inference(demodulation,[status(thm)],[c_277,c_457,c_470,c_479]) ).
tcf(c_482,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2),X3) = multiply(iPr_def_11,X3),
inference(demodulation,[status(thm)],[c_276,c_457,c_470,c_480]) ).
tcf(c_483,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X1)))) = X2,
inference(demodulation,[status(thm)],[c_366,c_457,c_481]) ).
tcf(c_484,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1)))) = X2,
inference(demodulation,[status(thm)],[c_248,c_481,c_482]) ).
tcf(c_927,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2) = iPr_def_11,
inference(superposition,[status(thm)],[c_124,c_457]) ).
tcf(c_928,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_11)),X0,X1) = inverse(X1),
inference(superposition,[status(thm)],[c_457,c_312]) ).
tcf(c_934,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))) = iPr_def_10(X0,X1,inverse(X1)),
inference(superposition,[status(thm)],[c_457,c_467]) ).
tcf(c_951,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1))),X2) = iPr_def_11,
inference(superposition,[status(thm)],[c_484,c_457]) ).
tcf(c_960,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(X0,inverse(iPr_def_11),X1),multiply(iPr_def_11,X0),iPr_def_11) = multiply(iPr_def_11,X1),
inference(superposition,[status(thm)],[c_457,c_478]) ).
tcf(c_973,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_10(X0,inverse(iPr_def_11),X1),multiply(multiply(iPr_def_11,X0),iPr_def_11))) = X1,
inference(superposition,[status(thm)],[c_457,c_483]) ).
tcf(c_995,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X1)))) = iPr_def_10(inverse(iPr_def_11),X0,X1),
inference(superposition,[status(thm)],[c_457,c_470]) ).
tcf(c_2649,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_10(X0,inverse(multiply(X1,iPr_def_11)),X1)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_928,c_479]) ).
tcf(c_2700,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,X1,inverse(X1)) = iPr_def_10(X0,X2,inverse(X2)),
inference(superposition,[status(thm)],[c_934,c_934]) ).
tcf(c_2707,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))) = multiply(iPr_def_11,X1),
inference(superposition,[status(thm)],[c_934,c_479]) ).
tcf(c_2708,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))))) = X1,
inference(superposition,[status(thm)],[c_934,c_124]) ).
tcf(c_2716,plain,
! [X0: $i] : multiply(iPr_def_11,inverse(multiply(inverse(multiply(X0,iPr_def_11)),iPr_def_11))) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_934,c_928]) ).
tcf(c_2871,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,X0)))) = iPr_def_10(inverse(iPr_def_11),inverse(iPr_def_11),X0),
inference(superposition,[status(thm)],[c_457,c_995]) ).
tcf(c_3613,plain,
! [X0: $i,X1: $i] : inverse(inverse(multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1))))) = multiply(iPr_def_11,inverse(multiply(inverse(iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_927,c_2716]) ).
tcf(c_3720,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11,multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1)))) = iPr_def_10(X2,inverse(X2),multiply(iPr_def_11,inverse(iPr_def_11))),
inference(superposition,[status(thm)],[c_927,c_2707]) ).
tcf(c_3763,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(iPr_def_11))))) = multiply(X1,multiply(X2,iPr_def_10(iPr_def_11,X1,X2))),
inference(superposition,[status(thm)],[c_927,c_2708]) ).
tcf(c_3765,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(iPr_def_10(X1,iPr_def_11,X0),multiply(iPr_def_11,X1))) = inverse(multiply(X2,multiply(inverse(X2),multiply(iPr_def_11,inverse(iPr_def_11))))),
inference(superposition,[status(thm)],[c_951,c_2708]) ).
tcf(c_3791,plain,
multiply(iPr_def_11,inverse(multiply(inverse(iPr_def_11),iPr_def_11))) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_3613,c_124]) ).
tcf(c_3792,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1))) = inverse(multiply(X2,multiply(inverse(X2),iPr_def_11))),
inference(demodulation,[status(thm)],[c_3763,c_457]) ).
tcf(c_3793,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(X0),iPr_def_11))) = iPr_def_12,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_3792]) ).
tcf(c_3794,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1))) = iPr_def_12,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3792]) ).
tcf(c_3797,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),multiply(iPr_def_11,inverse(iPr_def_11))) = multiply(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_3720,c_3794]) ).
tcf(c_3798,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),iPr_def_11) = multiply(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_3797,c_457]) ).
tcf(c_3810,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(iPr_def_10(X1,iPr_def_11,X0),multiply(iPr_def_11,X1))) = inverse(multiply(X2,multiply(inverse(X2),iPr_def_11))),
inference(demodulation,[status(thm)],[c_3765,c_457]) ).
tcf(c_3811,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_10(X1,iPr_def_11,X0),multiply(iPr_def_11,X1))) = iPr_def_12,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3810]) ).
tcf(c_4292,plain,
! [X0: $i] : multiply(multiply(X0,multiply(inverse(X0),iPr_def_11)),iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_3793,c_457]) ).
tcf(c_4323,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_12),multiply(iPr_def_11,X0)))) = inverse(X0),
inference(superposition,[status(thm)],[c_3798,c_484]) ).
tcf(c_4342,plain,
multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_11)) = inverse(multiply(iPr_def_11,iPr_def_12)),
inference(superposition,[status(thm)],[c_3798,c_2649]) ).
tcf(c_4359,plain,
! [X0: $i] : inverse(multiply(iPr_def_10(inverse(multiply(inverse(iPr_def_11),iPr_def_11)),inverse(iPr_def_11),X0),multiply(inverse(iPr_def_11),iPr_def_11))) = X0,
inference(superposition,[status(thm)],[c_3791,c_973]) ).
tcf(c_4361,plain,
! [X0: $i] : iPr_def_10(iPr_def_10(inverse(multiply(inverse(iPr_def_11),iPr_def_11)),inverse(iPr_def_11),X0),inverse(iPr_def_11),iPr_def_11) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_3791,c_960]) ).
tcf(c_4367,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),inverse(iPr_def_11)) = multiply(iPr_def_11,inverse(iPr_def_11)),
inference(superposition,[status(thm)],[c_3791,c_2707]) ).
tcf(c_4538,plain,
multiply(iPr_def_12,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_3811,c_951]) ).
tcf(c_4539,plain,
inverse(iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_3811,c_484]) ).
tcf(c_4541,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),inverse(iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_4367,c_457]) ).
tcf(c_4550,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_11),iPr_def_12,X0) = inverse(X0),
inference(demodulation,[status(thm)],[c_4323,c_995]) ).
tcf(c_4556,plain,
! [X0: $i] : iPr_def_10(inverse(X0),inverse(iPr_def_11),iPr_def_11) = multiply(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_4361,c_928]) ).
tcf(c_4558,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(inverse(iPr_def_11),iPr_def_11))) = X0,
inference(demodulation,[status(thm)],[c_4359,c_928]) ).
tcf(c_7021,plain,
iPr_def_10(iPr_def_12,iPr_def_11,iPr_def_11) = multiply(iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_4539,c_3798]) ).
tcf(c_7028,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1,inverse(X1)) = iPr_def_10(X0,iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_4539,c_2700]) ).
tcf(c_7122,plain,
multiply(iPr_def_11,multiply(inverse(iPr_def_11),iPr_def_11)) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_4541,c_2649]) ).
tcf(c_7150,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,inverse(X1))),X0,multiply(X2,inverse(X2))) = inverse(multiply(inverse(iPr_def_11),multiply(iPr_def_12,X1))),
inference(superposition,[status(thm)],[c_4550,c_454]) ).
tcf(c_7374,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,inverse(X1))),X0,iPr_def_11) = inverse(multiply(inverse(iPr_def_11),multiply(iPr_def_12,X1))),
inference(demodulation,[status(thm)],[c_7150,c_457]) ).
tcf(c_7512,plain,
inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_12)))) = iPr_def_12,
inference(superposition,[status(thm)],[c_7021,c_124]) ).
tcf(c_7552,plain,
! [X0: $i] : iPr_def_10(inverse(multiply(X0,inverse(iPr_def_11))),X0,iPr_def_11) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(superposition,[status(thm)],[c_7122,c_312]) ).
tcf(c_7577,plain,
multiply(inverse(iPr_def_11),iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_7122,c_4292]) ).
tcf(c_7578,plain,
inverse(inverse(iPr_def_11)) = iPr_def_12,
inference(superposition,[status(thm)],[c_7122,c_3793]) ).
tcf(c_7596,plain,
iPr_def_10(inverse(inverse(multiply(iPr_def_11,iPr_def_12))),iPr_def_11,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_4342,c_312]) ).
tcf(c_7645,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,multiply(iPr_def_11,X1))),X0,multiply(X2,inverse(X2))) = inverse(multiply(inverse(X1),multiply(inverse(iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_4556,c_454]) ).
tcf(c_7659,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(iPr_def_11),multiply(iPr_def_11,X0))) = X0,
inference(superposition,[status(thm)],[c_4556,c_312]) ).
tcf(c_7687,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(iPr_def_11),iPr_def_11))) = multiply(inverse(X0),multiply(inverse(iPr_def_11),iPr_def_11)),
inference(superposition,[status(thm)],[c_4558,c_4558]) ).
tcf(c_7757,plain,
iPr_def_10(inverse(iPr_def_11),inverse(iPr_def_11),iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_7512,c_2871]) ).
tcf(c_7767,plain,
inverse(multiply(inverse(iPr_def_11),multiply(iPr_def_12,iPr_def_11))) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(demodulation,[status(thm)],[c_7552,c_7374]) ).
tcf(c_7768,plain,
inverse(multiply(inverse(iPr_def_11),iPr_def_11)) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_7767,c_4538]) ).
tcf(c_7809,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,multiply(iPr_def_11,X1))),X0,multiply(X2,inverse(X2))) = multiply(inverse(inverse(X1)),multiply(inverse(iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_7645,c_7687]) ).
tcf(c_7810,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),multiply(inverse(iPr_def_11),iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_7809,c_312,c_457]) ).
tcf(c_8610,plain,
! [X0: $i] : iPr_def_10(X0,inverse(iPr_def_11),iPr_def_12) = iPr_def_10(X0,iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_7578,c_7028]) ).
tcf(c_8630,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_12)),X0,multiply(X1,inverse(X1))) = inverse(multiply(inverse(iPr_def_11),multiply(inverse(iPr_def_11),iPr_def_12))),
inference(superposition,[status(thm)],[c_7757,c_454]) ).
tcf(c_8725,plain,
! [X0: $i] : iPr_def_10(inverse(X0),iPr_def_11,inverse(iPr_def_11)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_7659,c_312]) ).
tcf(c_8799,plain,
! [X0: $i] : multiply(inverse(iPr_def_12),multiply(inverse(iPr_def_11),iPr_def_11)) = multiply(X0,multiply(inverse(X0),iPr_def_11)),
inference(superposition,[status(thm)],[c_3793,c_7810]) ).
tcf(c_8882,plain,
! [X0: $i] : iPr_def_10(inverse(X0),iPr_def_12,iPr_def_11) = multiply(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_8725,c_7028]) ).
tcf(c_8905,plain,
! [X0: $i] : multiply(X0,multiply(inverse(X0),iPr_def_11)) = inverse(iPr_def_11),
inference(light_normalisation,[status(thm)],[c_8799,c_4539,c_7122]) ).
tcf(c_8972,plain,
! [X0: $i] : inverse(multiply(inverse(iPr_def_11),multiply(inverse(iPr_def_11),iPr_def_12))) = iPr_def_10(inverse(multiply(X0,iPr_def_12)),X0,iPr_def_11),
inference(demodulation,[status(thm)],[c_8630,c_457]) ).
tcf(c_8973,plain,
! [X0: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_12)),X0,iPr_def_11) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_8972,c_7577,c_7768]) ).
tcf(c_9070,plain,
iPr_def_10(inverse(iPr_def_11),iPr_def_12,iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_7757,c_8610]) ).
tcf(c_9071,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_9070,c_8882]) ).
tcf(c_9075,plain,
inverse(multiply(iPr_def_11,iPr_def_12)) = multiply(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_4342,c_9071]) ).
tcf(c_9079,plain,
iPr_def_10(inverse(multiply(iPr_def_11,iPr_def_12)),iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7596,c_9075]) ).
tcf(c_9080,plain,
multiply(inverse(iPr_def_11),iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_9079,c_8973]) ).
tcf(c_9081,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),iPr_def_11) = X0,
inference(demodulation,[status(thm)],[c_7810,c_9080]) ).
tcf(c_9083,plain,
inverse(iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7768,c_9080]) ).
tcf(c_10654,plain,
! [X0: $i] : multiply(inverse(X0),X0) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_9081,c_8905]) ).
tcf(c_10742,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_10654,c_9083]) ).
tcf(c_11196,plain,
multiply(inverse(b1),b1) != iPr_def_11,
inference(demodulation,[status(thm)],[c_52,c_10742]) ).
tcf(c_11199,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_11196,c_10742]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP442-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.12/0.37 % Computer : n004.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Wed Sep 23 14:46:35 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.40 Running UEQ theorem proving
% 0.12/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.12/0.41
% 0.12/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.41
% 0.12/0.41 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 9.18/2.18 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 9.18/2.18 % SZS status Started for theBenchmark.p
% 9.18/2.18 % SZS status Unsatisfiable for theBenchmark.p
% 9.18/2.18
% 9.18/2.18 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 9.18/2.18
% 9.18/2.18 % ------ iProver source info
% 9.18/2.18
% 9.18/2.18 % git: date: 2026-07-19 20:42:38 +0200
% 9.18/2.18 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 9.18/2.18 % git: non_committed_changes: false
% 9.18/2.18
% 9.18/2.18 % ------ Parsing...% successful
% 9.18/2.18
% 9.18/2.18
% 9.18/2.18 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 9.18/2.18 % ------ Proving...
% 9.18/2.18 % ------ Problem Properties
% 9.18/2.18
% 9.18/2.18 %
% 9.18/2.18 % clauses 2
% 9.18/2.18 % conjectures 1
% 9.18/2.18 % EPR 0
% 9.18/2.18 % Horn 2
% 9.18/2.18 % unary 2
% 9.18/2.18 % binary 0
% 9.18/2.18 % lits 2
% 9.18/2.18 % lits eq 2
% 9.18/2.18 % fd_pure 0
% 9.18/2.18 % fd_pseudo 0
% 9.18/2.18 % fd_cond 0
% 9.18/2.18 % fd_pseudo_cond 0
% 9.18/2.18 % AC symbols 0
% 9.18/2.18
% 9.18/2.18 % ------ Input Options Time Limit: Unbounded
% 9.18/2.18
% 9.18/2.18
% 9.18/2.18 % ------
% 9.18/2.18 % Current options:
% 9.18/2.18 % ------
% 9.18/2.18
% 9.18/2.18
% 9.18/2.18 %
% 9.18/2.18
% 9.18/2.18 % ------ Proving...
% 9.18/2.18 %
% 9.18/2.18
% 9.18/2.18 % SZS status Unsatisfiable for theBenchmark.p
% 9.18/2.18
% 9.18/2.18 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 9.18/2.19
% 9.18/2.19
%------------------------------------------------------------------------------