%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP429-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/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:04 PM UTC 2026
% Result : Unsatisfiable 8.64s 2.49s
% Output : CNFRefutation 8.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 2
% Syntax : Number of formulae : 231 ( 231 unt; 0 def)
% Number of atoms : 876 ( 230 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 17 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 2 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 490 ( 0 sgn 490 !; 0 ?; 486 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_3) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3)))) = multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5))))),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X4)))),X1))),X5),inverse(multiply(X3,X5))))))))) = X4,
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(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4)))) = X2,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = iPr_def_10(X0,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_61]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3)))) = iPr_def_10(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_61]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_51,c_64]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2)))) = iPr_def_10(X3,iPr_def_10(inverse(X3),X1)),
inference(superposition,[status(thm)],[c_64,c_66]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),iPr_def_10(inverse(inverse(X1)),X2))),X3),inverse(multiply(X0,X3)))) = iPr_def_10(X1,inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5))))),
inference(superposition,[status(thm)],[c_64,c_65]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,multiply(inverse(inverse(X1)),X2)) = multiply(X0,iPr_def_10(X1,X2)),
inference(superposition,[status(thm)],[c_65,c_64]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,iPr_def_10(multiply(inverse(X2),multiply(inverse(X0),X3)),X1)))))) = X3,
inference(superposition,[status(thm)],[c_65,c_62]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),iPr_def_10(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4)))) = inverse(multiply(multiply(inverse(multiply(inverse(X6),X2)),X7),inverse(multiply(X6,X7)))),
inference(superposition,[status(thm)],[c_64,c_63]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X0),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4))) = multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(X6),X2)),inverse(multiply(multiply(inverse(multiply(inverse(X7),multiply(inverse(X6),X8))),X9),inverse(multiply(X7,X9))))),inverse(X8)))),
inference(superposition,[status(thm)],[c_63,c_63]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X0),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4))) = multiply(X1,inverse(multiply(X6,inverse(multiply(X7,inverse(multiply(multiply(inverse(multiply(inverse(X8),multiply(inverse(inverse(multiply(inverse(X7),X2))),X6))),X9),inverse(multiply(X8,X9))))))))),
inference(superposition,[status(thm)],[c_63,c_62]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,inverse(multiply(iPr_def_10(inverse(multiply(inverse(X1),iPr_def_10(inverse(X0),X2))),multiply(inverse(X1),X3)),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5)))),
inference(demodulation,[status(thm)],[c_134,c_64]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2)))) = iPr_def_11(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_180]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),iPr_def_11(multiply(inverse(X0),X3))),inverse(X3))) = multiply(X1,inverse(multiply(X4,inverse(multiply(X5,iPr_def_11(multiply(inverse(inverse(multiply(inverse(X5),X2))),X4))))))),
inference(demodulation,[status(thm)],[c_156,c_181]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,iPr_def_11(multiply(inverse(inverse(multiply(inverse(X2),X3))),X1))))))) = iPr_def_12(X0,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_203]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),X2))),iPr_def_11(multiply(inverse(X0),X3))),inverse(X3))) = iPr_def_12(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_203]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),iPr_def_11(multiply(inverse(X1),X3))),inverse(X3)))) = iPr_def_12(X0,X2),
inference(demodulation,[status(thm)],[c_151,c_181,c_205]) ).
tcf(c_217,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_11(X1)) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_64,c_181]) ).
tcf(c_218,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(inverse(inverse(X0)),X1)) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_65,c_181]) ).
tcf(c_220,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),iPr_def_11(multiply(inverse(X1),X3))),inverse(X3)))) = X2,
inference(demodulation,[status(thm)],[c_63,c_181]) ).
tcf(c_221,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_220,c_207]) ).
tcf(c_429,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_10(inverse(inverse(X0)),X1)) = iPr_def_10(X0,iPr_def_11(X1)),
inference(superposition,[status(thm)],[c_217,c_218]) ).
tcf(c_432,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_10(inverse(inverse(X1)),X2)) = multiply(X0,iPr_def_10(X1,iPr_def_11(X2))),
inference(superposition,[status(thm)],[c_217,c_102]) ).
tcf(c_433,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),iPr_def_10(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_102,c_66]) ).
tcf(c_438,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),iPr_def_11(X2)),inverse(iPr_def_10(X0,X2)))) = iPr_def_11(X1),
inference(superposition,[status(thm)],[c_217,c_181]) ).
tcf(c_441,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2))),X3) = iPr_def_11(multiply(inverse(iPr_def_11(X1)),X3)),
inference(superposition,[status(thm)],[c_181,c_218]) ).
tcf(c_453,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_11(inverse(multiply(X0,inverse(multiply(X1,iPr_def_10(multiply(inverse(X1),multiply(inverse(inverse(X2)),X3)),X0)))))) = inverse(multiply(multiply(inverse(X3),X4),inverse(multiply(X2,X4)))),
inference(superposition,[status(thm)],[c_104,c_181]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,inverse(multiply(X1,iPr_def_10(multiply(inverse(X1),multiply(inverse(inverse(X2)),X3)),X0))))) = iPr_def_12(X2,X3),
inference(superposition,[status(thm)],[c_104,c_221]) ).
tcf(c_455,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,inverse(multiply(X1,iPr_def_10(multiply(inverse(X1),multiply(inverse(inverse(X2)),X3)),X0))))) = iPr_def_10(X2,X3),
inference(superposition,[status(thm)],[c_104,c_66]) ).
tcf(c_506,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(multiply(multiply(inverse(multiply(inverse(X0),X1)),X2),inverse(multiply(X0,X2))),multiply(iPr_def_10(X3,iPr_def_10(inverse(X3),X1)),X4)) = X4,
inference(superposition,[status(thm)],[c_88,c_66]) ).
tcf(c_512,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_10(inverse(X0),X1)) = iPr_def_11(X1),
inference(superposition,[status(thm)],[c_88,c_181]) ).
tcf(c_651,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,inverse(multiply(X1,inverse(multiply(X2,iPr_def_11(multiply(inverse(inverse(multiply(inverse(X2),X3))),X1))))))) = iPr_def_11(iPr_def_12(inverse(inverse(X0)),X3)),
inference(superposition,[status(thm)],[c_204,c_218]) ).
tcf(c_661,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : iPr_def_12(X0,inverse(multiply(X1,inverse(multiply(X2,iPr_def_10(multiply(inverse(X2),multiply(inverse(inverse(X3)),X4)),X1)))))) = multiply(X0,inverse(multiply(multiply(inverse(X4),iPr_def_11(multiply(inverse(X3),X5))),inverse(X5)))),
inference(superposition,[status(thm)],[c_104,c_207]) ).
tcf(c_696,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),iPr_def_11(multiply(inverse(X0),X2))),inverse(X2))) = iPr_def_10(X3,iPr_def_12(inverse(X3),X1)),
inference(superposition,[status(thm)],[c_207,c_66]) ).
tcf(c_710,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_10(inverse(multiply(inverse(X0),X1)),X2),inverse(iPr_def_10(X0,X2)))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_438,c_217]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1) = iPr_def_12(X0,X1),
inference(demodulation,[status(thm)],[c_454,c_455]) ).
tcf(c_725,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),iPr_def_11(multiply(inverse(X0),X2))),inverse(X2))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_696,c_512,c_714]) ).
tcf(c_726,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_10(inverse(multiply(inverse(X0),X1)),multiply(inverse(X0),X2)),inverse(X2))) = iPr_def_11(X1),
inference(demodulation,[status(thm)],[c_725,c_217]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(inverse(iPr_def_11(X0)),multiply(iPr_def_11(X0),X1))) = X1,
inference(demodulation,[status(thm)],[c_506,c_512,c_441]) ).
tcf(c_752,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,inverse(multiply(X1,inverse(multiply(X2,iPr_def_11(multiply(inverse(inverse(multiply(inverse(X2),X3))),X1))))))) = iPr_def_10(X0,iPr_def_11(X3)),
inference(demodulation,[status(thm)],[c_651,c_429,c_714]) ).
tcf(c_753,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,inverse(multiply(X1,inverse(multiply(X2,iPr_def_10(multiply(inverse(X2),X3),X1)))))) = iPr_def_10(X0,iPr_def_11(X3)),
inference(demodulation,[status(thm)],[c_752,c_102,c_217]) ).
tcf(c_781,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1)))) = iPr_def_11(iPr_def_10(X2,X0)),
inference(demodulation,[status(thm)],[c_453,c_455]) ).
tcf(c_847,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(inverse(X1),iPr_def_11(multiply(inverse(X2),X3))),inverse(X3)))) = iPr_def_10(X0,iPr_def_11(multiply(inverse(inverse(X2)),X1))),
inference(demodulation,[status(thm)],[c_661,c_714,c_753]) ).
tcf(c_848,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(iPr_def_10(inverse(X1),multiply(inverse(X2),X3)),inverse(X3)))) = iPr_def_10(X0,iPr_def_10(X2,X1)),
inference(demodulation,[status(thm)],[c_847,c_217,c_218]) ).
tcf(c_2023,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(X0,iPr_def_10(X1,X2))) = multiply(inverse(inverse(X1)),X2),
inference(superposition,[status(thm)],[c_102,c_433]) ).
tcf(c_2042,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,multiply(inverse(iPr_def_11(X1)),multiply(iPr_def_11(X1),X2))) = multiply(X0,X2),
inference(superposition,[status(thm)],[c_746,c_217]) ).
tcf(c_2070,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,inverse(multiply(X1,iPr_def_10(X2,X0))))) = iPr_def_11(iPr_def_10(X1,X2)),
inference(superposition,[status(thm)],[c_433,c_781]) ).
tcf(c_2093,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_10(inverse(X0),X1),inverse(iPr_def_10(X2,X1)))) = iPr_def_11(iPr_def_10(X2,X0)),
inference(superposition,[status(thm)],[c_433,c_710]) ).
tcf(c_2115,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_10(inverse(X0),multiply(inverse(X1),X2)),inverse(X2))) = iPr_def_11(iPr_def_10(X1,X0)),
inference(superposition,[status(thm)],[c_433,c_726]) ).
tcf(c_2190,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = iPr_def_10(X0,iPr_def_10(inverse(X2),X2)),
inference(superposition,[status(thm)],[c_66,c_848]) ).
tcf(c_2550,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(inverse(X0)),iPr_def_10(inverse(X0),X1)) = multiply(inverse(X2),multiply(X2,iPr_def_11(X1))),
inference(superposition,[status(thm)],[c_512,c_2023]) ).
tcf(c_2568,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_11(X0)),multiply(iPr_def_11(X0),X1)) = multiply(inverse(X2),multiply(X2,X1)),
inference(superposition,[status(thm)],[c_2042,c_433]) ).
tcf(c_2570,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(inverse(iPr_def_11(X0)),multiply(iPr_def_11(X0),X1))) = iPr_def_10(X2,multiply(inverse(X2),X1)),
inference(superposition,[status(thm)],[c_2042,c_512]) ).
tcf(c_2599,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,multiply(inverse(multiply(inverse(iPr_def_11(X1)),multiply(iPr_def_11(X1),X2))),X2)) = multiply(X0,inverse(multiply(X3,inverse(X3)))),
inference(superposition,[status(thm)],[c_2042,c_2190]) ).
tcf(c_2603,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,iPr_def_10(inverse(inverse(X1)),iPr_def_10(inverse(X2),X2))) = multiply(X0,iPr_def_10(X1,inverse(multiply(X3,inverse(X3))))),
inference(superposition,[status(thm)],[c_2190,c_102]) ).
tcf(c_2607,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,multiply(inverse(iPr_def_11(X1)),iPr_def_10(iPr_def_11(X1),iPr_def_10(inverse(X2),X2)))) = multiply(X0,inverse(multiply(X3,inverse(X3)))),
inference(superposition,[status(thm)],[c_2190,c_2042]) ).
tcf(c_2614,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(X0,inverse(multiply(X1,inverse(X1))))) = iPr_def_10(inverse(X2),X2),
inference(superposition,[status(thm)],[c_2190,c_433]) ).
tcf(c_2617,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = iPr_def_11(X0),
inference(superposition,[status(thm)],[c_2190,c_512]) ).
tcf(c_2618,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(inverse(inverse(X0)),inverse(multiply(X1,inverse(X1))))) = iPr_def_10(X0,iPr_def_11(iPr_def_10(inverse(X2),X2))),
inference(superposition,[status(thm)],[c_2190,c_429]) ).
tcf(c_2686,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,inverse(X0))) = iPr_def_11(iPr_def_10(inverse(X1),X1)),
inference(superposition,[status(thm)],[c_66,c_2115]) ).
tcf(c_2818,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),iPr_def_11(X0)) = iPr_def_10(inverse(X1),X1),
inference(demodulation,[status(thm)],[c_2614,c_2617]) ).
tcf(c_2819,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),X0) = iPr_def_10(inverse(X1),X1),
inference(demodulation,[status(thm)],[c_2818,c_217]) ).
tcf(c_2821,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = iPr_def_13(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_2568]) ).
tcf(c_2825,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,multiply(inverse(X0),X1)) = iPr_def_11(iPr_def_13(X1)),
inference(demodulation,[status(thm)],[c_2570,c_2821]) ).
tcf(c_2826,plain,
! [X0: $i] : iPr_def_11(iPr_def_13(X0)) = X0,
inference(demodulation,[status(thm)],[c_2825,c_66]) ).
tcf(c_2827,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),iPr_def_10(inverse(X0),X1)) = iPr_def_13(iPr_def_11(X1)),
inference(demodulation,[status(thm)],[c_2550,c_2821]) ).
tcf(c_2828,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(X0)) = X0,
inference(demodulation,[status(thm)],[c_2827,c_433]) ).
tcf(c_2830,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11(iPr_def_10(inverse(X1),X1))) = iPr_def_11(iPr_def_11(inverse(inverse(X0)))),
inference(demodulation,[status(thm)],[c_2618,c_2617]) ).
tcf(c_2834,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,iPr_def_10(X1,inverse(multiply(X2,inverse(X2))))) = multiply(X0,iPr_def_10(X1,iPr_def_11(iPr_def_10(inverse(X3),X3)))),
inference(demodulation,[status(thm)],[c_2603,c_432]) ).
tcf(c_2836,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,iPr_def_10(X1,iPr_def_11(iPr_def_10(inverse(X2),X2)))) = iPr_def_14(X0,X1),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2834]) ).
tcf(c_2837,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_11(iPr_def_11(inverse(inverse(X1))))) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_2836,c_2830]) ).
tcf(c_2838,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11(inverse(inverse(X1)))) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_2837,c_217]) ).
tcf(c_2849,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,multiply(inverse(iPr_def_11(X1)),iPr_def_10(iPr_def_11(X1),iPr_def_10(inverse(X2),X2)))) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_2607,c_2617]) ).
tcf(c_2850,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_10(inverse(X1),X1)) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_2849,c_433]) ).
tcf(c_2851,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,multiply(inverse(iPr_def_13(X1)),X1)) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_2599,c_2617,c_2821]) ).
tcf(c_2935,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = iPr_def_13(iPr_def_10(X0,X1)),
inference(demodulation,[status(thm)],[c_2023,c_2821]) ).
tcf(c_3718,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_10(inverse(X0),X0),inverse(X1))) = iPr_def_11(iPr_def_10(X2,multiply(inverse(X2),X1))),
inference(superposition,[status(thm)],[c_2819,c_2115]) ).
tcf(c_3731,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_13(X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_2821,c_66]) ).
tcf(c_3748,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,iPr_def_10(X1,iPr_def_11(iPr_def_10(inverse(X2),X2)))) = iPr_def_10(X0,iPr_def_11(inverse(inverse(X1)))),
inference(superposition,[status(thm)],[c_2850,c_432]) ).
tcf(c_3757,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(iPr_def_10(inverse(X0),X0))) = iPr_def_10(inverse(X1),X1),
inference(superposition,[status(thm)],[c_2850,c_2819]) ).
tcf(c_3815,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_13(X0)),X0) = multiply(inverse(X1),iPr_def_11(X1)),
inference(superposition,[status(thm)],[c_2851,c_433]) ).
tcf(c_3824,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11(inverse(multiply(inverse(iPr_def_13(X1)),X1)))) = iPr_def_11(X0),
inference(superposition,[status(thm)],[c_2851,c_2850]) ).
tcf(c_3825,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(multiply(inverse(iPr_def_13(X0)),X0))) = iPr_def_10(inverse(X1),X1),
inference(superposition,[status(thm)],[c_2851,c_2819]) ).
tcf(c_3845,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,inverse(iPr_def_13(iPr_def_10(X1,iPr_def_10(X2,X0)))))) = iPr_def_11(iPr_def_10(inverse(inverse(X1)),X2)),
inference(superposition,[status(thm)],[c_2935,c_2070]) ).
tcf(c_3848,plain,
! [X0: $i,X1: $i] : iPr_def_13(iPr_def_10(X0,inverse(multiply(X1,inverse(X1))))) = iPr_def_11(inverse(inverse(X0))),
inference(superposition,[status(thm)],[c_2935,c_2617]) ).
tcf(c_3854,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_11(multiply(X0,inverse(X0)))) = iPr_def_11(iPr_def_10(inverse(X1),X1)),
inference(superposition,[status(thm)],[c_2617,c_2686]) ).
tcf(c_3886,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(iPr_def_10(inverse(X0),X0)),multiply(X1,inverse(X1))) = iPr_def_10(inverse(X2),X2),
inference(superposition,[status(thm)],[c_2686,c_2819]) ).
tcf(c_3904,plain,
! [X0: $i,X1: $i] : iPr_def_13(inverse(multiply(X0,inverse(X0)))) = iPr_def_10(inverse(X1),X1),
inference(superposition,[status(thm)],[c_2686,c_2828]) ).
tcf(c_3905,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,inverse(X0))) = inverse(multiply(X1,inverse(X1))),
inference(superposition,[status(thm)],[c_2686,c_2686]) ).
tcf(c_3978,plain,
! [X0: $i] : inverse(multiply(X0,inverse(X0))) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_3905]) ).
tcf(c_3980,plain,
! [X0: $i] : iPr_def_10(inverse(X0),X0) = iPr_def_13(iPr_def_16),
inference(demodulation,[status(thm)],[c_3904,c_3978]) ).
tcf(c_3981,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_13(X0)),X0) = iPr_def_10(inverse(X1),X1),
inference(demodulation,[status(thm)],[c_3815,c_217]) ).
tcf(c_3982,plain,
iPr_def_11(inverse(iPr_def_13(iPr_def_16))) = iPr_def_13(iPr_def_16),
inference(demodulation,[status(thm)],[c_3757,c_3980]) ).
tcf(c_3989,plain,
! [X0: $i] : inverse(iPr_def_11(multiply(X0,inverse(X0)))) = iPr_def_11(iPr_def_13(iPr_def_16)),
inference(demodulation,[status(thm)],[c_3854,c_3980]) ).
tcf(c_3990,plain,
! [X0: $i] : inverse(iPr_def_11(multiply(X0,inverse(X0)))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3989,c_2826]) ).
tcf(c_3991,plain,
! [X0: $i] : iPr_def_11(inverse(multiply(inverse(iPr_def_13(X0)),X0))) = iPr_def_13(iPr_def_16),
inference(demodulation,[status(thm)],[c_3825,c_3980]) ).
tcf(c_3992,plain,
! [X0: $i] : multiply(X0,iPr_def_16) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_3824,c_3731,c_3991]) ).
tcf(c_4005,plain,
! [X0: $i] : iPr_def_11(inverse(inverse(X0))) = iPr_def_13(iPr_def_10(X0,iPr_def_16)),
inference(demodulation,[status(thm)],[c_3848,c_3978]) ).
tcf(c_4027,plain,
! [X0: $i] : iPr_def_10(iPr_def_11(iPr_def_13(iPr_def_16)),multiply(X0,inverse(X0))) = iPr_def_13(iPr_def_16),
inference(demodulation,[status(thm)],[c_3886,c_3980]) ).
tcf(c_4028,plain,
! [X0: $i] : iPr_def_10(iPr_def_16,multiply(X0,inverse(X0))) = iPr_def_13(iPr_def_16),
inference(demodulation,[status(thm)],[c_4027,c_2826]) ).
tcf(c_4044,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_10(X1,iPr_def_11(iPr_def_13(iPr_def_16)))) = iPr_def_10(X0,iPr_def_11(inverse(inverse(X1)))),
inference(demodulation,[status(thm)],[c_3748,c_3980]) ).
tcf(c_4045,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_10(X1,iPr_def_16)) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_4044,c_2826,c_2838]) ).
tcf(c_4047,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_10(X0,multiply(inverse(X0),X1))) = inverse(multiply(iPr_def_13(iPr_def_16),inverse(X1))),
inference(demodulation,[status(thm)],[c_3718,c_3980]) ).
tcf(c_4048,plain,
! [X0: $i] : inverse(multiply(iPr_def_13(iPr_def_16),inverse(X0))) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_4047,c_66]) ).
tcf(c_4068,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,inverse(iPr_def_13(iPr_def_10(X1,iPr_def_10(X2,X0)))))) = iPr_def_10(X1,iPr_def_11(X2)),
inference(demodulation,[status(thm)],[c_3845,c_429]) ).
tcf(c_6958,plain,
inverse(iPr_def_13(iPr_def_16)) = iPr_def_13(iPr_def_13(iPr_def_16)),
inference(superposition,[status(thm)],[c_3982,c_2828]) ).
tcf(c_7014,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_11(multiply(X0,inverse(X0))),multiply(iPr_def_16,X1)) = X1,
inference(superposition,[status(thm)],[c_3990,c_66]) ).
tcf(c_7038,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(inverse(inverse(X0)))) = iPr_def_10(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_4005,c_2826]) ).
tcf(c_7051,plain,
! [X0: $i] : iPr_def_10(iPr_def_16,multiply(iPr_def_11(multiply(X0,inverse(X0))),iPr_def_16)) = iPr_def_13(iPr_def_16),
inference(superposition,[status(thm)],[c_3990,c_4028]) ).
tcf(c_7053,plain,
inverse(inverse(iPr_def_16)) = iPr_def_13(iPr_def_16),
inference(superposition,[status(thm)],[c_4028,c_66]) ).
tcf(c_7059,plain,
! [X0: $i] : multiply(X0,iPr_def_13(iPr_def_16)) = iPr_def_14(X0,inverse(iPr_def_16)),
inference(superposition,[status(thm)],[c_3980,c_4045]) ).
tcf(c_7077,plain,
! [X0: $i] : iPr_def_11(multiply(X0,inverse(X0))) = inverse(multiply(iPr_def_13(iPr_def_16),iPr_def_16)),
inference(superposition,[status(thm)],[c_3978,c_4048]) ).
tcf(c_7078,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(multiply(X0,inverse(X0)))) = inverse(multiply(iPr_def_13(iPr_def_16),iPr_def_16)),
inference(superposition,[status(thm)],[c_3990,c_4048]) ).
tcf(c_7180,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(inverse(iPr_def_13(X1)),X1)) = X0,
inference(superposition,[status(thm)],[c_3981,c_433]) ).
tcf(c_7190,plain,
! [X0: $i] : multiply(inverse(iPr_def_13(X0)),X0) = iPr_def_13(iPr_def_16),
inference(superposition,[status(thm)],[c_3981,c_3980]) ).
tcf(c_7214,plain,
! [X0: $i] : iPr_def_14(inverse(inverse(X0)),inverse(iPr_def_16)) = X0,
inference(demodulation,[status(thm)],[c_7180,c_7190,c_7059]) ).
tcf(c_7218,plain,
! [X0: $i] : iPr_def_11(multiply(X0,inverse(X0))) = inverse(iPr_def_16),
inference(demodulation,[status(thm)],[c_7077,c_2826,c_3992]) ).
tcf(c_7221,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_16),multiply(iPr_def_16,X0)) = X0,
inference(demodulation,[status(thm)],[c_7014,c_7218]) ).
tcf(c_7238,plain,
inverse(multiply(iPr_def_13(iPr_def_16),iPr_def_16)) = iPr_def_11(inverse(iPr_def_16)),
inference(demodulation,[status(thm)],[c_7078,c_7218]) ).
tcf(c_7239,plain,
iPr_def_11(inverse(iPr_def_16)) = inverse(iPr_def_16),
inference(demodulation,[status(thm)],[c_7238,c_2826,c_3992]) ).
tcf(c_7240,plain,
iPr_def_10(iPr_def_16,multiply(inverse(iPr_def_16),iPr_def_16)) = iPr_def_13(iPr_def_16),
inference(demodulation,[status(thm)],[c_7051,c_7218]) ).
tcf(c_7241,plain,
iPr_def_13(iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_7240,c_66]) ).
tcf(c_7360,plain,
inverse(inverse(iPr_def_16)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3990,c_7218]) ).
tcf(c_7361,plain,
! [X0: $i] : inverse(multiply(iPr_def_16,inverse(X0))) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_4048,c_7241]) ).
tcf(c_7363,plain,
! [X0: $i] : iPr_def_10(inverse(X0),X0) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3980,c_7241]) ).
tcf(c_7460,plain,
! [X0: $i] : iPr_def_13(iPr_def_10(iPr_def_16,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_7360,c_2935]) ).
tcf(c_7462,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_11(iPr_def_16)) = iPr_def_14(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_7360,c_2838]) ).
tcf(c_7484,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_11(iPr_def_13(iPr_def_16))) = iPr_def_14(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_7053,c_2838]) ).
tcf(c_7495,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_16)) = iPr_def_10(X0,inverse(iPr_def_16)),
inference(superposition,[status(thm)],[c_7239,c_217]) ).
tcf(c_7510,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),iPr_def_16) = X0,
inference(superposition,[status(thm)],[c_7363,c_433]) ).
tcf(c_7513,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_16) = iPr_def_11(X0),
inference(superposition,[status(thm)],[c_7363,c_512]) ).
tcf(c_7517,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_10(inverse(X0),X1),inverse(iPr_def_16))) = iPr_def_11(iPr_def_10(inverse(X1),X0)),
inference(superposition,[status(thm)],[c_7363,c_2093]) ).
tcf(c_7522,plain,
! [X0: $i] : iPr_def_14(X0,inverse(iPr_def_16)) = multiply(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_7363,c_4045]) ).
tcf(c_7524,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_11(inverse(iPr_def_13(iPr_def_13(iPr_def_16))))) = iPr_def_14(X0,iPr_def_13(iPr_def_16)),
inference(superposition,[status(thm)],[c_6958,c_2838]) ).
tcf(c_7532,plain,
! [X0: $i] : multiply(iPr_def_13(iPr_def_13(iPr_def_16)),multiply(iPr_def_13(iPr_def_16),X0)) = iPr_def_13(X0),
inference(superposition,[status(thm)],[c_6958,c_2821]) ).
tcf(c_7539,plain,
! [X0: $i] : multiply(iPr_def_13(iPr_def_13(iPr_def_16)),iPr_def_10(iPr_def_13(iPr_def_16),X0)) = X0,
inference(superposition,[status(thm)],[c_6958,c_433]) ).
tcf(c_7540,plain,
! [X0: $i] : iPr_def_10(iPr_def_13(iPr_def_16),multiply(iPr_def_13(iPr_def_13(iPr_def_16)),X0)) = X0,
inference(superposition,[status(thm)],[c_6958,c_66]) ).
tcf(c_7583,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1))) = iPr_def_14(inverse(iPr_def_11(iPr_def_10(X2,X0))),inverse(iPr_def_16)),
inference(superposition,[status(thm)],[c_781,c_7214]) ).
tcf(c_7605,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = iPr_def_13(inverse(iPr_def_16)),
inference(superposition,[status(thm)],[c_7218,c_2828]) ).
tcf(c_7612,plain,
! [X0: $i] : iPr_def_11(multiply(iPr_def_16,X0)) = iPr_def_10(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_7221,c_512]) ).
tcf(c_7643,plain,
! [X0: $i] : inverse(multiply(iPr_def_16,iPr_def_11(X0))) = iPr_def_11(multiply(iPr_def_16,inverse(X0))),
inference(superposition,[status(thm)],[c_7361,c_7361]) ).
tcf(c_7645,plain,
! [X0: $i] : iPr_def_14(inverse(iPr_def_11(X0)),inverse(iPr_def_16)) = multiply(iPr_def_16,inverse(X0)),
inference(superposition,[status(thm)],[c_7361,c_7214]) ).
tcf(c_7646,plain,
! [X0: $i] : iPr_def_10(iPr_def_11(X0),multiply(iPr_def_16,inverse(X0))) = iPr_def_16,
inference(superposition,[status(thm)],[c_7361,c_7363]) ).
tcf(c_7699,plain,
iPr_def_11(iPr_def_11(inverse(iPr_def_13(iPr_def_16)))) = iPr_def_10(inverse(iPr_def_16),iPr_def_16),
inference(superposition,[status(thm)],[c_7053,c_7038]) ).
tcf(c_7711,plain,
! [X0: $i] : iPr_def_11(inverse(inverse(X0))) = X0,
inference(demodulation,[status(thm)],[c_7510,c_2935,c_4005]) ).
tcf(c_7728,plain,
! [X0: $i] : iPr_def_14(X0,inverse(iPr_def_16)) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_7522,c_3992]) ).
tcf(c_7759,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_16) = iPr_def_14(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_7484,c_2826]) ).
tcf(c_7764,plain,
iPr_def_11(iPr_def_11(inverse(iPr_def_13(iPr_def_16)))) = iPr_def_11(inverse(iPr_def_16)),
inference(demodulation,[status(thm)],[c_7699,c_7513]) ).
tcf(c_7765,plain,
iPr_def_11(iPr_def_11(iPr_def_16)) = inverse(iPr_def_16),
inference(light_normalisation,[status(thm)],[c_7764,c_6958,c_7239,c_7241]) ).
tcf(c_7801,plain,
! [X0: $i] : iPr_def_10(iPr_def_16,multiply(iPr_def_16,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_7540,c_7241]) ).
tcf(c_7802,plain,
! [X0: $i] : multiply(iPr_def_16,iPr_def_10(iPr_def_16,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_7539,c_7241]) ).
tcf(c_7817,plain,
! [X0: $i] : multiply(iPr_def_16,inverse(X0)) = iPr_def_11(inverse(iPr_def_11(X0))),
inference(demodulation,[status(thm)],[c_7645,c_7728]) ).
tcf(c_7820,plain,
! [X0: $i] : inverse(multiply(iPr_def_16,iPr_def_11(X0))) = iPr_def_10(iPr_def_16,inverse(X0)),
inference(demodulation,[status(thm)],[c_7643,c_7612]) ).
tcf(c_7821,plain,
! [X0: $i] : inverse(iPr_def_10(iPr_def_16,X0)) = iPr_def_10(iPr_def_16,inverse(X0)),
inference(demodulation,[status(thm)],[c_7820,c_217]) ).
tcf(c_7835,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_16,X0)) = iPr_def_13(X0),
inference(light_normalisation,[status(thm)],[c_7532,c_7241]) ).
tcf(c_7852,plain,
! [X0: $i] : iPr_def_10(X0,inverse(iPr_def_16)) = iPr_def_14(X0,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_7524,c_7239,c_7241]) ).
tcf(c_7872,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_11(iPr_def_10(inverse(X0),X1))) = iPr_def_11(iPr_def_10(inverse(X1),X0)),
inference(demodulation,[status(thm)],[c_7517,c_7495,c_7513,c_7759,c_7852]) ).
tcf(c_7938,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(X0),X1),inverse(multiply(X2,X1))) = iPr_def_11(inverse(iPr_def_11(iPr_def_10(X2,X0)))),
inference(demodulation,[status(thm)],[c_7583,c_7728]) ).
tcf(c_7979,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_11(X1)) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_4045,c_7513]) ).
tcf(c_7983,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_7979,c_217]) ).
tcf(c_8981,plain,
! [X0: $i] : inverse(inverse(X0)) = iPr_def_13(X0),
inference(superposition,[status(thm)],[c_7711,c_2828]) ).
tcf(c_8998,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_16)) = iPr_def_10(X0,iPr_def_11(iPr_def_16)),
inference(superposition,[status(thm)],[c_7765,c_217]) ).
tcf(c_9084,plain,
! [X0: $i] : multiply(iPr_def_16,iPr_def_11(X0)) = iPr_def_10(inverse(iPr_def_16),X0),
inference(superposition,[status(thm)],[c_512,c_7802]) ).
tcf(c_9152,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_16),X0) = iPr_def_10(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_9084,c_217]) ).
tcf(c_9162,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_16)) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_8998,c_7462,c_7513,c_7983]) ).
tcf(c_9224,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_13(X0),X1) = iPr_def_13(iPr_def_10(X0,X1)),
inference(demodulation,[status(thm)],[c_2935,c_8981]) ).
tcf(c_9249,plain,
! [X0: $i] : inverse(iPr_def_13(X0)) = iPr_def_13(inverse(X0)),
inference(superposition,[status(thm)],[c_8981,c_8981]) ).
tcf(c_9264,plain,
! [X0: $i] : multiply(iPr_def_16,iPr_def_10(inverse(iPr_def_16),X0)) = iPr_def_13(iPr_def_11(X0)),
inference(superposition,[status(thm)],[c_512,c_7460]) ).
tcf(c_9282,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_13(inverse(iPr_def_16))) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_7605,c_66]) ).
tcf(c_9313,plain,
! [X0: $i] : multiply(iPr_def_16,iPr_def_13(X0)) = iPr_def_13(multiply(iPr_def_16,X0)),
inference(superposition,[status(thm)],[c_7835,c_7835]) ).
tcf(c_9377,plain,
! [X0: $i] : iPr_def_11(X0) = iPr_def_13(X0),
inference(demodulation,[status(thm)],[c_9282,c_3731,c_8981,c_9162]) ).
tcf(c_9399,plain,
! [X0: $i] : multiply(iPr_def_16,iPr_def_10(inverse(iPr_def_16),X0)) = iPr_def_11(iPr_def_11(X0)),
inference(demodulation,[status(thm)],[c_9264,c_9377]) ).
tcf(c_9400,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(X0)) = X0,
inference(demodulation,[status(thm)],[c_9399,c_7802,c_9152]) ).
tcf(c_9408,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11(X1)) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_3731,c_9377]) ).
tcf(c_9411,plain,
! [X0: $i] : inverse(inverse(X0)) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_8981,c_9377]) ).
tcf(c_9480,plain,
! [X0: $i] : inverse(iPr_def_11(X0)) = iPr_def_13(inverse(X0)),
inference(superposition,[status(thm)],[c_9377,c_9249]) ).
tcf(c_9628,plain,
! [X0: $i] : iPr_def_10(X0,multiply(iPr_def_16,inverse(iPr_def_11(X0)))) = iPr_def_16,
inference(superposition,[status(thm)],[c_9400,c_7646]) ).
tcf(c_9696,plain,
! [X0: $i] : inverse(iPr_def_11(X0)) = iPr_def_11(inverse(X0)),
inference(demodulation,[status(thm)],[c_9480,c_9377]) ).
tcf(c_9739,plain,
! [X0: $i] : iPr_def_10(X0,multiply(iPr_def_16,iPr_def_11(inverse(X0)))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_9628,c_9696]) ).
tcf(c_9740,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_10(iPr_def_16,inverse(X0))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_9739,c_217]) ).
tcf(c_9849,plain,
! [X0: $i] : multiply(iPr_def_16,inverse(X0)) = iPr_def_11(iPr_def_11(inverse(X0))),
inference(demodulation,[status(thm)],[c_7817,c_9696]) ).
tcf(c_9857,plain,
! [X0: $i] : multiply(iPr_def_16,inverse(X0)) = inverse(X0),
inference(demodulation,[status(thm)],[c_9849,c_9400]) ).
tcf(c_9883,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_11(inverse(X0)))) = multiply(iPr_def_16,iPr_def_11(X0)),
inference(superposition,[status(thm)],[c_9411,c_7817]) ).
tcf(c_9892,plain,
! [X0: $i] : iPr_def_10(iPr_def_16,iPr_def_11(inverse(iPr_def_11(X0)))) = inverse(X0),
inference(superposition,[status(thm)],[c_7817,c_7801]) ).
tcf(c_9917,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(X2),X4),inverse(multiply(inverse(inverse(X0)),X4)))),
inference(superposition,[status(thm)],[c_433,c_92]) ).
tcf(c_9933,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),iPr_def_10(iPr_def_11(X1),X2))),X3),inverse(multiply(X0,X3)))) = iPr_def_10(X1,inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5))))),
inference(superposition,[status(thm)],[c_9411,c_92]) ).
tcf(c_10035,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11(inverse(X0)),iPr_def_10(iPr_def_11(X0),X1)) = X1,
inference(superposition,[status(thm)],[c_9696,c_433]) ).
tcf(c_10036,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_11(X0),multiply(iPr_def_11(inverse(X0)),X1)) = X1,
inference(superposition,[status(thm)],[c_9696,c_66]) ).
tcf(c_10044,plain,
! [X0: $i] : multiply(iPr_def_16,iPr_def_11(X0)) = iPr_def_11(X0),
inference(superposition,[status(thm)],[c_9411,c_9857]) ).
tcf(c_10045,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_16,iPr_def_10(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3)))))) = iPr_def_10(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))),
inference(superposition,[status(thm)],[c_92,c_9857]) ).
tcf(c_10047,plain,
! [X0: $i] : multiply(iPr_def_16,iPr_def_13(inverse(X0))) = iPr_def_13(inverse(X0)),
inference(superposition,[status(thm)],[c_9249,c_9857]) ).
tcf(c_10057,plain,
! [X0: $i] : iPr_def_10(iPr_def_16,inverse(X0)) = inverse(X0),
inference(superposition,[status(thm)],[c_9857,c_7801]) ).
tcf(c_10072,plain,
! [X0: $i] : multiply(inverse(X0),iPr_def_16) = iPr_def_10(iPr_def_16,inverse(X0)),
inference(superposition,[status(thm)],[c_9740,c_433]) ).
tcf(c_10098,plain,
! [X0: $i] : inverse(iPr_def_10(iPr_def_16,inverse(X0))) = iPr_def_11(iPr_def_10(iPr_def_16,X0)),
inference(superposition,[status(thm)],[c_7821,c_9411]) ).
tcf(c_10129,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11(X0),X1) = iPr_def_13(iPr_def_10(X0,X1)),
inference(superposition,[status(thm)],[c_9377,c_9224]) ).
tcf(c_10139,plain,
! [X0: $i] : iPr_def_10(iPr_def_16,X0) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_10044,c_217]) ).
tcf(c_10156,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11(X0),X1) = iPr_def_11(iPr_def_10(X0,X1)),
inference(demodulation,[status(thm)],[c_10129,c_9377]) ).
tcf(c_10165,plain,
! [X0: $i] : multiply(inverse(X0),iPr_def_16) = inverse(X0),
inference(demodulation,[status(thm)],[c_10072,c_10057]) ).
tcf(c_10166,plain,
! [X0: $i] : iPr_def_11(inverse(X0)) = inverse(X0),
inference(demodulation,[status(thm)],[c_10165,c_3992]) ).
tcf(c_10172,plain,
! [X0: $i] : iPr_def_10(iPr_def_16,inverse(X0)) = iPr_def_11(inverse(X0)),
inference(demodulation,[status(thm)],[c_10047,c_7612,c_9313,c_9377]) ).
tcf(c_10182,plain,
! [X0: $i] : inverse(iPr_def_11(X0)) = inverse(X0),
inference(demodulation,[status(thm)],[c_9892,c_10139,c_10166]) ).
tcf(c_10205,plain,
! [X0: $i] : inverse(inverse(X0)) = iPr_def_11(iPr_def_11(X0)),
inference(demodulation,[status(thm)],[c_10098,c_10172,c_10139,c_10166]) ).
tcf(c_10206,plain,
! [X0: $i] : iPr_def_11(X0) = X0,
inference(demodulation,[status(thm)],[c_10205,c_9400,c_9411]) ).
tcf(c_10219,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_10(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_10036,c_10156,c_10206]) ).
tcf(c_10220,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),iPr_def_10(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_10035,c_10156,c_10206]) ).
tcf(c_10226,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_9883,c_10166,c_10182,c_10206]) ).
tcf(c_10227,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = iPr_def_11(X0),
inference(demodulation,[status(thm)],[c_10226,c_9411]) ).
tcf(c_10244,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_10(inverse(X0),inverse(X1))) = multiply(X1,X0),
inference(demodulation,[status(thm)],[c_9917,c_66,c_7872,c_7938,c_9400,c_9408,c_9411,c_9696]) ).
tcf(c_10281,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(inverse(multiply(inverse(X0),iPr_def_10(X1,X2))),X3),inverse(multiply(X0,X3)))) = iPr_def_10(X1,inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5))))),
inference(demodulation,[status(thm)],[c_9933,c_10206]) ).
tcf(c_10282,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_10(X0,X1)) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_10281,c_66,c_7938,c_9400,c_9408,c_9411,c_9696]) ).
tcf(c_10297,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = iPr_def_10(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))),
inference(demodulation,[status(thm)],[c_10045,c_10227,c_10282]) ).
tcf(c_10298,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_10297,c_66,c_217,c_7938,c_9400,c_9408,c_9411,c_9696]) ).
tcf(c_10493,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_9411,c_10206]) ).
tcf(c_10495,plain,
! [X0: $i] : iPr_def_13(X0) = X0,
inference(demodulation,[status(thm)],[c_9377,c_10206]) ).
tcf(c_10514,plain,
multiply(iPr_def_10(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm)],[c_52,c_10298]) ).
tcf(c_10515,plain,
iPr_def_10(iPr_def_10(a3,b3),c3) != iPr_def_10(a3,iPr_def_10(b3,c3)),
inference(demodulation,[status(thm)],[c_10514,c_10298]) ).
tcf(c_10863,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_10(inverse(X0),X1)) = multiply(inverse(X1),X0),
inference(superposition,[status(thm)],[c_10493,c_10244]) ).
tcf(c_10886,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),inverse(X1)) = inverse(multiply(X1,X0)),
inference(superposition,[status(thm)],[c_10244,c_10493]) ).
tcf(c_10943,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),inverse(X1)) = inverse(iPr_def_10(X1,X0)),
inference(demodulation,[status(thm)],[c_10886,c_10298]) ).
tcf(c_10944,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_10(inverse(X0),X1)) = iPr_def_10(inverse(X1),X0),
inference(demodulation,[status(thm)],[c_10863,c_10298]) ).
tcf(c_11143,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(iPr_def_10(X0,X1)),X0) = inverse(X1),
inference(superposition,[status(thm)],[c_10220,c_10944]) ).
tcf(c_11582,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(X0,X1),inverse(X1)) = X0,
inference(superposition,[status(thm)],[c_11143,c_10219]) ).
tcf(c_12883,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(X0),inverse(iPr_def_13(iPr_def_10(X1,X2))))) = iPr_def_10(X1,iPr_def_11(iPr_def_10(X2,X0))),
inference(superposition,[status(thm)],[c_11582,c_4068]) ).
tcf(c_12959,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1),X2) = iPr_def_10(X0,iPr_def_10(X1,X2)),
inference(demodulation,[status(thm)],[c_12883,c_10206,c_10298,c_10493,c_10495,c_10943]) ).
tcf(c_13201,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_10515,c_12959]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP429-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.61 % Computer : n004.cluster.edu
% 0.13/0.61 % Model : x86_64 x86_64
% 0.13/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.61 % Memory : 8046.5625MB
% 0.13/0.61 % OS : Linux 6.8.0-71-generic
% 0.13/0.61 % CPULimit : 300
% 0.13/0.61 % WCLimit : 300
% 0.13/0.61 % DateTime : Wed Sep 23 14:44:40 UTC 2026
% 0.13/0.61 % CPUTime :
% 0.13/0.62 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/0.65 Running UEQ theorem proving
% 0.17/0.65 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.67
% 0.17/0.67 % ======== iProver multi-core TPTP/SMT =========
% 0.17/0.67
% 0.17/0.67 % Detected problem language: tptp
% 0.17/0.68 % Proving...
% 8.64/2.49 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 8.64/2.49 % SZS status Started for theBenchmark.p
% 8.64/2.49 % SZS status Unsatisfiable for theBenchmark.p
% 8.64/2.49
% 8.64/2.49 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.64/2.49
% 8.64/2.49 % ------ iProver source info
% 8.64/2.49
% 8.64/2.49 % git: date: 2026-07-19 20:42:38 +0200
% 8.64/2.49 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.64/2.49 % git: non_committed_changes: false
% 8.64/2.49
% 8.64/2.49 % ------ Parsing...% successful
% 8.64/2.49
% 8.64/2.49
% 8.64/2.49 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 8.64/2.49 % ------ Proving...
% 8.64/2.49 % ------ Problem Properties
% 8.64/2.49
% 8.64/2.49 %
% 8.64/2.49 % clauses 2
% 8.64/2.49 % conjectures 1
% 8.64/2.49 % EPR 0
% 8.64/2.49 % Horn 2
% 8.64/2.49 % unary 2
% 8.64/2.49 % binary 0
% 8.64/2.49 % lits 2
% 8.64/2.49 % lits eq 2
% 8.64/2.49 % fd_pure 0
% 8.64/2.49 % fd_pseudo 0
% 8.64/2.49 % fd_cond 0
% 8.64/2.49 % fd_pseudo_cond 0
% 8.64/2.49 % AC symbols 0
% 8.64/2.49
% 8.64/2.49 % ------ Input Options Time Limit: Unbounded
% 8.64/2.49
% 8.64/2.49
% 8.64/2.49 % ------
% 8.64/2.49 % Current options:
% 8.64/2.49 % ------
% 8.64/2.49
% 8.64/2.49
% 8.64/2.49 %
% 8.64/2.49
% 8.64/2.49 % ------ Proving...
% 8.64/2.49 %
% 8.64/2.49
% 8.64/2.49 % SZS status Unsatisfiable for theBenchmark.p
% 8.64/2.49
% 8.64/2.49 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.64/2.49
% 8.64/2.49
%------------------------------------------------------------------------------