%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP242-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n017.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:32:26 PM UTC 2026
% Result : Unsatisfiable 37.75s 12.01s
% Output : CNFRefutation 37.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 38
% Syntax : Number of formulae : 318 ( 85 unt; 12 def)
% Number of atoms : 1129 ( 661 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 722 ( 300 ~; 422 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 158 ( 0 sgn 158 !; 0 ?; 123 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c10) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c9 = inverse(sk_c10)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f13,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c9 = multiply(sk_c8,sk_c11)
| multiply(sk_c1,sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f13]) ).
fof(f17,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( inverse(sk_c10) = sk_c9
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c9 = inverse(sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f19]) ).
fof(f25,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c9
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c9 = multiply(sk_c8,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f29,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f29]) ).
fof(f33,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c10 = inverse(sk_c7)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f35]) ).
fof(f39,negated_conjecture,
( inverse(sk_c8) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c11 = inverse(sk_c8)
| sk_c9 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f41]) ).
fof(f45,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c11 = multiply(sk_c7,sk_c10)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f48,plain,
( sk_c10 = inverse(sk_c7)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f47]) ).
fof(f51,negated_conjecture,
( inverse(sk_c8) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c11 = inverse(sk_c8)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| multiply(sk_c3,sk_c6) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| sk_c11 = multiply(sk_c3,sk_c6) ),
inference(reorient_equations,[],[f53]) ).
fof(f65,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| inverse(sk_c3) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| sk_c6 = inverse(sk_c3) ),
inference(reorient_equations,[],[f65]) ).
fof(f89,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| inverse(sk_c5) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f90,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| inverse(sk_c5) = sk_c4 ),
inference(reorient_equations,[],[f89]) ).
fof(f113,negated_conjecture,
( multiply(sk_c10,sk_c9) = sk_c11
| multiply(sk_c5,sk_c6) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_55) ).
fof(f114,plain,
( sk_c11 = multiply(sk_c10,sk_c9)
| sk_c4 = multiply(sk_c5,sk_c6) ),
inference(reorient_equations,[],[f113]) ).
fof(f125,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( inverse(X7) != sk_c11
| multiply(X7,sk_c11) != sk_c9
| inverse(X6) != sk_c10
| multiply(X6,sk_c10) != sk_c11
| inverse(sk_c10) != sk_c9
| multiply(sk_c10,sk_c9) != sk_c11
| multiply(X4,X3) != X5
| inverse(X5) != X3
| inverse(X4) != X5
| multiply(X3,sk_c10) != sk_c11
| inverse(X2) != X3
| multiply(X2,X3) != sk_c11
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != sk_c9
| inverse(X0) != sk_c11
| multiply(X0,sk_c11) != sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_61) ).
fof(f126,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( sk_c11 != inverse(X7)
| sk_c9 != multiply(X7,sk_c11)
| sk_c10 != inverse(X6)
| sk_c11 != multiply(X6,sk_c10)
| sk_c9 != inverse(sk_c10)
| sk_c11 != multiply(sk_c10,sk_c9)
| multiply(X4,X3) != X5
| inverse(X5) != X3
| inverse(X4) != X5
| sk_c11 != multiply(X3,sk_c10)
| inverse(X2) != X3
| sk_c11 != multiply(X2,X3)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(reorient_equations,[],[f125]) ).
fof(f127,plain,
! [X2,X0,X1,X6,X7,X4,X5] :
( sk_c11 != inverse(X7)
| sk_c9 != multiply(X7,sk_c11)
| sk_c10 != inverse(X6)
| sk_c11 != multiply(X6,sk_c10)
| sk_c9 != inverse(sk_c10)
| sk_c11 != multiply(sk_c10,sk_c9)
| multiply(X4,inverse(X2)) != X5
| inverse(X2) != inverse(X5)
| inverse(X4) != X5
| sk_c11 != multiply(inverse(X2),sk_c10)
| sk_c11 != multiply(X2,inverse(X2))
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f126]) ).
fof(f128,plain,
! [X2,X0,X1,X6,X7,X4] :
( sk_c11 != inverse(X7)
| sk_c9 != multiply(X7,sk_c11)
| sk_c10 != inverse(X6)
| sk_c11 != multiply(X6,sk_c10)
| sk_c9 != inverse(sk_c10)
| sk_c11 != multiply(sk_c10,sk_c9)
| inverse(X4) != multiply(X4,inverse(X2))
| inverse(X2) != inverse(inverse(X4))
| sk_c11 != multiply(inverse(X2),sk_c10)
| sk_c11 != multiply(X2,inverse(X2))
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(X0,sk_c11) ),
inference(equality_resolution,[],[f127]) ).
tcf(c_113,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_114,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c10,sk_c9) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c8,sk_c11) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c8) = sk_c11 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c3,sk_c6) = sk_c11 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_158,negated_conjecture,
( ( inverse(sk_c5) = sk_c4 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_170,negated_conjecture,
( ( multiply(sk_c5,sk_c6) = sk_c4 )
| ( multiply(sk_c10,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_176,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(X5) != sk_c10 )
| ( inverse(X4) != sk_c11 )
| ( inverse(X3) != sk_c10 )
| ( inverse(X2) != sk_c11 )
| ( multiply(sk_c10,sk_c9) != sk_c11 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(X5,sk_c10) != sk_c9 )
| ( multiply(X4,sk_c11) != sk_c9 )
| ( multiply(X3,sk_c10) != sk_c11 )
| ( multiply(X2,sk_c11) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_178,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_725,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_176]) ).
tcf(c_726,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_176]) ).
tcf(c_727,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_176]) ).
tcf(c_728,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_176]) ).
tcf(c_729,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_176]) ).
tcf(c_730,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(sk_c10,sk_c9) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_176]) ).
tcf(c_731,definition,
iPr_def_15 = multiply(sk_c10,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_732,definition,
iPr_def_16 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_734,definition,
iPr_def_18 = inverse(sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_735,definition,
iPr_def_19 = multiply(sk_c8,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_736,definition,
iPr_def_20 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_737,definition,
iPr_def_21 = multiply(sk_c7,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_741,definition,
iPr_def_25 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_742,definition,
iPr_def_26 = multiply(sk_c3,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_743,definition,
iPr_def_27 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_744,definition,
iPr_def_28 = multiply(sk_c2,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_745,definition,
iPr_def_29 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_746,definition,
iPr_def_30 = multiply(sk_c1,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_747,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 != sk_c9 )
| ( iPr_def_15 != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_730,c_732,c_731]) ).
tcf(c_748,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_729]) ).
tcf(c_749,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_728]) ).
tcf(c_750,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_727]) ).
tcf(c_751,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_726]) ).
tcf(c_752,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_725]) ).
tcf(c_758,negated_conjecture,
( ( iPr_def_17 = sk_c4 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_170]) ).
tcf(c_770,negated_conjecture,
( ( iPr_def_23 = sk_c4 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_158]) ).
tcf(c_782,negated_conjecture,
( ( iPr_def_25 = sk_c6 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_788,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_789,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_139,c_743]) ).
tcf(c_791,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_792,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_21 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_794,negated_conjecture,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_134]) ).
tcf(c_795,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_133,c_744]) ).
tcf(c_797,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_798,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_21 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_800,negated_conjecture,
( ( iPr_def_28 = sk_c9 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_802,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_805,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_806,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_808,negated_conjecture,
( ( iPr_def_30 = sk_c10 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_811,negated_conjecture,
( ( iPr_def_30 = sk_c10 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_812,negated_conjecture,
( ( iPr_def_30 = sk_c10 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_813,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_814,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_815,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_816,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_818,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_816]) ).
tcf(c_819,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_1389,plain,
multiply(iPr_def_16,sk_c10) = identity,
inference(superposition,[status(thm)],[c_732,c_114]) ).
tcf(c_1390,plain,
multiply(iPr_def_20,sk_c7) = identity,
inference(superposition,[status(thm)],[c_736,c_114]) ).
tcf(c_1391,plain,
multiply(iPr_def_18,sk_c8) = identity,
inference(superposition,[status(thm)],[c_734,c_114]) ).
tcf(c_1392,plain,
multiply(iPr_def_29,sk_c1) = identity,
inference(superposition,[status(thm)],[c_745,c_114]) ).
tcf(c_1393,plain,
multiply(iPr_def_27,sk_c2) = identity,
inference(superposition,[status(thm)],[c_743,c_114]) ).
tcf(c_1394,plain,
multiply(iPr_def_25,sk_c3) = identity,
inference(superposition,[status(thm)],[c_741,c_114]) ).
tcf(c_1429,plain,
( ( iPr_def_17 = iPr_def_23 )
| ( sk_c11 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_770,c_758]) ).
tcf(c_1578,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_1617,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1578]) ).
tcf(c_1651,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_1653,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_1662,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_16 )
| ( iPr_def_16 != inverse(sk_c10) )
| ( inverse(X0) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1617]) ).
tcf(c_1663,plain,
( ( inverse(sk_c10) = iPr_def_16 )
| ( iPr_def_16 != inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1662]) ).
tcf(c_1719,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c3,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_782,c_742]) ).
tcf(c_1794,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1578]) ).
tcf(c_1872,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_27,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_789,c_731]) ).
tcf(c_1923,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1653]) ).
tcf(c_1938,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_27,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_791,c_731]) ).
tcf(c_1988,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(iPr_def_27,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_792,c_731]) ).
tcf(c_2047,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_27,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_794,c_731]) ).
tcf(c_2231,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_29 )
| ( iPr_def_29 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_2582,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_2584,plain,
( ( sk_c11 = iPr_def_15 )
| ( iPr_def_15 != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1923]) ).
tcf(c_2628,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_805,c_802]) ).
tcf(c_2638,plain,
( ( sk_c11 = iPr_def_29 )
| ( multiply(sk_c10,iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_805,c_731]) ).
tcf(c_2683,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_806,c_746]) ).
tcf(c_3015,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1653]) ).
tcf(c_3018,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( sk_c11 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_3015]) ).
tcf(c_3089,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c10 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_811,c_808]) ).
tcf(c_3100,plain,
( ( sk_c10 = iPr_def_30 )
| ( multiply(sk_c10,iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_811,c_731]) ).
tcf(c_3154,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_812,c_744]) ).
tcf(c_3259,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_26 )
| ( sk_c9 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_788,c_747]) ).
tcf(c_3412,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_30 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_746,c_749]) ).
tcf(c_3414,plain,
( ~ iPr_def_13
| ( sk_c11 != sk_c10 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_113,c_749]) ).
tcf(c_3432,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_30 )
| ( sk_c11 != iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_3412,c_745]) ).
tcf(c_3546,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( inverse(iPr_def_16) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1389,c_750]) ).
tcf(c_3799,plain,
( ~ iPr_def_10
| ( sk_c11 != sk_c9 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_113,c_752]) ).
tcf(c_3800,plain,
( ~ iPr_def_10
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_114,c_752]) ).
tcf(c_3992,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_29 = X0 )
| ( iPr_def_29 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_4094,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_114,c_115]) ).
tcf(c_4096,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1389,c_115]) ).
tcf(c_4097,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1390,c_115]) ).
tcf(c_4098,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1391,c_115]) ).
tcf(c_4099,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1392,c_115]) ).
tcf(c_4100,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1393,c_115]) ).
tcf(c_4101,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1394,c_115]) ).
tcf(c_4112,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4101,c_113]) ).
tcf(c_4113,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4100,c_113]) ).
tcf(c_4114,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4099,c_113]) ).
tcf(c_4115,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c8,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4098,c_113]) ).
tcf(c_4116,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4097,c_113]) ).
tcf(c_4117,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4096,c_113]) ).
tcf(c_4182,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_4433,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_17 = iPr_def_23 )
| ( sk_c9 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1429,c_747]) ).
tcf(c_5208,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2582]) ).
tcf(c_5210,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_2582]) ).
tcf(c_5253,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_5361,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_5476,plain,
( ( iPr_def_15 = sk_c11 )
| ( iPr_def_15 != iPr_def_15 )
| ( sk_c11 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_5208]) ).
tcf(c_5477,plain,
iPr_def_15 = iPr_def_15,
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_6747,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_2628,c_746]) ).
tcf(c_7657,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_30,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_3089,c_731]) ).
tcf(c_8018,plain,
multiply(iPr_def_27,iPr_def_28) = sk_c10,
inference(superposition,[status(thm)],[c_744,c_4113]) ).
tcf(c_8055,plain,
multiply(iPr_def_29,iPr_def_30) = sk_c11,
inference(superposition,[status(thm)],[c_746,c_4114]) ).
tcf(c_8208,plain,
multiply(iPr_def_16,iPr_def_15) = sk_c9,
inference(superposition,[status(thm)],[c_731,c_4117]) ).
tcf(c_10362,plain,
! [X0: $i] :
( ( iPr_def_29 = X0 )
| ( iPr_def_29 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3992]) ).
tcf(c_11106,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_795,c_1872]) ).
tcf(c_11114,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_11106,c_8018]) ).
tcf(c_11256,plain,
( ( sk_c11 = iPr_def_18 )
| ( inverse(iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_11114,c_732]) ).
tcf(c_12064,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_797,c_1938]) ).
tcf(c_12074,plain,
( ( sk_c10 = iPr_def_20 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_12064,c_8018]) ).
tcf(c_12153,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_12074,c_737]) ).
tcf(c_12588,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_798,c_1988]) ).
tcf(c_12599,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_12588,c_8018]) ).
tcf(c_12870,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(iPr_def_16,iPr_def_15) = identity ) ),
inference(superposition,[status(thm)],[c_12599,c_1389]) ).
tcf(c_12891,plain,
( ( sk_c9 = identity )
| ( sk_c11 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_12870,c_8208]) ).
tcf(c_13568,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_800,c_2047]) ).
tcf(c_13581,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_13568,c_8018]) ).
tcf(c_13729,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_16,iPr_def_15) = identity ) ),
inference(superposition,[status(thm)],[c_13581,c_1389]) ).
tcf(c_13750,plain,
( ( sk_c9 = identity )
| ( sk_c11 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_13729,c_8208]) ).
tcf(c_15215,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_2683,c_4114]) ).
tcf(c_15216,plain,
( ( sk_c11 = iPr_def_29 )
| ( sk_c11 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_15215,c_8055]) ).
tcf(c_16643,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3154,c_4113]) ).
tcf(c_16644,plain,
( ( sk_c10 = iPr_def_30 )
| ( sk_c11 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_16643,c_8018]) ).
tcf(c_17231,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != iPr_def_29 )
| ( X0 != iPr_def_29 ) ),
inference(instantiation,[status(thm)],[c_1653]) ).
tcf(c_17234,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != iPr_def_29 )
| ( sk_c11 != iPr_def_29 ) ),
inference(instantiation,[status(thm)],[c_17231]) ).
tcf(c_17585,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1794]) ).
tcf(c_17586,plain,
( ( inverse(sk_c10) = sk_c9 )
| ( sk_c9 != iPr_def_16 )
| ( inverse(sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_17585]) ).
tcf(c_22446,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_4094,c_113]) ).
tcf(c_22495,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_113,c_22446]) ).
tcf(c_22496,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_22446]) ).
tcf(c_22693,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_4117,c_22446]) ).
tcf(c_22694,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_4116,c_22446]) ).
tcf(c_22695,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_4115,c_22446]) ).
tcf(c_22696,plain,
! [X0: $i] : multiply(inverse(iPr_def_29),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_4114,c_22446]) ).
tcf(c_22698,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_4112,c_22446]) ).
tcf(c_22759,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_22446,c_22446]) ).
tcf(c_23616,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_22496,c_22759]) ).
tcf(c_23643,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_23616,c_22495]) ).
tcf(c_24383,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_5361]) ).
tcf(c_24454,plain,
multiply(sk_c10,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_22693,c_114]) ).
tcf(c_24458,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_22693,c_22446]) ).
tcf(c_24459,plain,
multiply(sk_c10,identity) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_22693,c_23616]) ).
tcf(c_24479,plain,
( ( identity = iPr_def_15 )
| ( sk_c10 = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_3100,c_24454]) ).
tcf(c_24480,plain,
( ( identity = iPr_def_15 )
| ( sk_c11 = iPr_def_29 ) ),
inference(demodulation,[status(thm)],[c_2638,c_24454]) ).
tcf(c_25212,plain,
( ( identity = iPr_def_15 )
| ( multiply(iPr_def_30,sk_c9) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_24479,c_731]) ).
tcf(c_25425,plain,
( ( identity = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_24480,c_746]) ).
tcf(c_25682,plain,
inverse(iPr_def_16) = sk_c10,
inference(demodulation,[status(thm)],[c_24459,c_23616]) ).
tcf(c_28348,plain,
multiply(sk_c7,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_22694,c_114]) ).
tcf(c_28387,plain,
( ( identity = iPr_def_21 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_12153,c_28348]) ).
tcf(c_28586,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_16,iPr_def_15) = identity ) ),
inference(superposition,[status(thm)],[c_28387,c_1389]) ).
tcf(c_28606,plain,
( ( identity = iPr_def_21 )
| ( sk_c9 = identity ) ),
inference(light_normalisation,[status(thm)],[c_28586,c_8208]) ).
tcf(c_31446,plain,
multiply(sk_c8,iPr_def_18) = identity,
inference(superposition,[status(thm)],[c_22695,c_114]) ).
tcf(c_31551,plain,
( ( identity = sk_c11 )
| ( identity != iPr_def_21 )
| ( sk_c11 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_5210]) ).
tcf(c_33543,plain,
multiply(sk_c1,iPr_def_29) = identity,
inference(superposition,[status(thm)],[c_22696,c_114]) ).
tcf(c_33548,plain,
multiply(sk_c1,identity) = inverse(iPr_def_29),
inference(superposition,[status(thm)],[c_22696,c_23616]) ).
tcf(c_33592,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_6747,c_33543]) ).
tcf(c_33757,plain,
inverse(iPr_def_29) = sk_c1,
inference(demodulation,[status(thm)],[c_33548,c_23616]) ).
tcf(c_34029,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_30,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_33592,c_113]) ).
tcf(c_36837,plain,
( ( iPr_def_29 = iPr_def_26 )
| ( iPr_def_29 != sk_c11 )
| ( iPr_def_26 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_10362]) ).
tcf(c_36996,plain,
! [X0: $i] :
( ( X0 = iPr_def_29 )
| ( iPr_def_29 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2231]) ).
tcf(c_36997,plain,
( ( sk_c10 = iPr_def_29 )
| ( iPr_def_29 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_36996]) ).
tcf(c_37006,plain,
( ( identity = iPr_def_15 )
| ( iPr_def_15 != sk_c11 )
| ( identity != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_24383]) ).
tcf(c_39527,plain,
( ( identity = iPr_def_30 )
| ( identity = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_25425,c_33543]) ).
tcf(c_39586,plain,
! [X0: $i] :
( ( identity = iPr_def_15 )
| ( multiply(iPr_def_30,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_39527,c_113]) ).
tcf(c_39901,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_4182]) ).
tcf(c_39902,plain,
( ( sk_c10 = identity )
| ( identity != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_39901]) ).
tcf(c_39931,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_5253]) ).
tcf(c_39932,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_39931]) ).
tcf(c_44309,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != sk_c9 )
| ( inverse(X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1578]) ).
tcf(c_44312,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_44309]) ).
tcf(c_46271,plain,
multiply(sk_c3,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_22698,c_114]) ).
tcf(c_46312,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1719,c_46271]) ).
tcf(c_60378,plain,
! [X0: $i] :
( ( iPr_def_29 = X0 )
| ( iPr_def_29 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_3992]) ).
tcf(c_65720,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c9 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_34029,c_7657]) ).
tcf(c_67132,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_1653]) ).
tcf(c_67133,plain,
( ( sk_c11 = multiply(sk_c10,sk_c10) )
| ( sk_c11 != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_67132]) ).
tcf(c_69609,plain,
( ( identity = iPr_def_15 )
| ( sk_c9 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_39586,c_25212]) ).
tcf(c_74266,plain,
( ( identity = iPr_def_21 )
| ( identity = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_69609,c_28606]) ).
tcf(c_74292,plain,
( ( identity = iPr_def_15 )
| ( sk_c11 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_69609,c_13750]) ).
tcf(c_74294,plain,
( ( identity = iPr_def_15 )
| ( sk_c11 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_69609,c_12891]) ).
tcf(c_76334,plain,
identity = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_74266,c_5476,c_5477,c_31551,c_37006,c_74294,c_74292,c_74266]) ).
tcf(c_76378,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c11 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_46312,c_76334]) ).
tcf(c_76424,plain,
multiply(sk_c8,iPr_def_18) = iPr_def_15,
inference(demodulation,[status(thm)],[c_31446,c_76334]) ).
tcf(c_76456,plain,
inverse(iPr_def_15) = iPr_def_15,
inference(demodulation,[status(thm)],[c_23643,c_76334]) ).
tcf(c_76457,plain,
! [X0: $i] : multiply(X0,iPr_def_15) = X0,
inference(demodulation,[status(thm)],[c_23616,c_76334]) ).
tcf(c_76501,plain,
multiply(iPr_def_16,sk_c10) = iPr_def_15,
inference(demodulation,[status(thm)],[c_1389,c_76334]) ).
tcf(c_76503,plain,
! [X0: $i] : multiply(iPr_def_15,X0) = X0,
inference(demodulation,[status(thm)],[c_113,c_76334]) ).
tcf(c_76668,plain,
( ( iPr_def_15 = iPr_def_16 )
| ( sk_c11 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_11256,c_76456]) ).
tcf(c_76694,plain,
sk_c9 = iPr_def_16,
inference(demodulation,[status(thm)],[c_8208,c_76457]) ).
tcf(c_76733,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_65720,c_76694]) ).
tcf(c_76794,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 != iPr_def_16 )
| ( sk_c11 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_747,c_76694]) ).
tcf(c_76799,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( sk_c11 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_800,c_76694]) ).
tcf(c_76838,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 != iPr_def_15 ) ),
inference(equality_resolution_simp,[status(thm)],[c_76794]) ).
tcf(c_79828,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_15 )
| ( inverse(iPr_def_16) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_76501,c_751]) ).
tcf(c_79845,plain,
( ~ iPr_def_11
| ( sk_c11 != iPr_def_15 ) ),
inference(ground_joinability,[status(thm)],[c_79828,c_25682]) ).
tcf(c_80349,plain,
( ~ iPr_def_13
| ( sk_c11 != sk_c10 )
| ( inverse(iPr_def_15) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_76503,c_749]) ).
tcf(c_80352,plain,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != inverse(iPr_def_15) )
| ( inverse(inverse(iPr_def_15)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_76503,c_748]) ).
tcf(c_80359,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_15 )
| ( sk_c11 != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_80349,c_76456]) ).
tcf(c_80363,plain,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != iPr_def_15 )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_80352,c_76456]) ).
tcf(c_80368,plain,
( ~ iPr_def_14
| ( inverse(sk_c10) != iPr_def_15 )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_80363]) ).
tcf(c_81469,plain,
( ( iPr_def_16 = iPr_def_28 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_76799,c_79845]) ).
tcf(c_81509,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_11
| ( iPr_def_15 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_788,c_79845]) ).
tcf(c_82524,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_81469,c_76378,c_79845,c_81509]) ).
tcf(c_84484,plain,
( ~ iPr_def_13
| ( sk_c11 != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_3414,c_3432,c_15216,c_16644,c_80359]) ).
tcf(c_84519,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_13
| ( sk_c11 != iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_812,c_84484]) ).
tcf(c_84785,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_84519,c_3432,c_15216,c_16644]) ).
tcf(c_86553,plain,
( ~ iPr_def_12
| ( sk_c9 != identity ) ),
inference(ground_joinability,[status(thm)],[c_3546,c_25682]) ).
tcf(c_86554,plain,
( ~ iPr_def_12
| ( iPr_def_15 != iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_86553,c_76334,c_76694]) ).
tcf(c_86567,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_16 )
| ( sk_c11 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_3799,c_76334,c_76456,c_76694]) ).
tcf(c_87704,plain,
( ~ iPr_def_10
| ( iPr_def_15 != iPr_def_16 )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3800,c_76334,c_76694]) ).
tcf(c_87765,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_10
| ( iPr_def_15 != iPr_def_16 )
| ( inverse(inverse(iPr_def_29)) != iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_806,c_87704]) ).
tcf(c_87806,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_10
| ( iPr_def_15 != iPr_def_16 ) ),
inference(ground_joinability,[status(thm)],[c_87765,c_745,c_33757]) ).
tcf(c_87875,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_4433,c_3259,c_76694,c_76378,c_76838,c_82524]) ).
tcf(c_92749,plain,
( ( iPr_def_15 = iPr_def_16 )
| ( multiply(sk_c8,iPr_def_18) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_76668,c_735]) ).
tcf(c_92754,plain,
( ( iPr_def_15 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_92749,c_76424]) ).
tcf(c_94121,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1794]) ).
tcf(c_94122,plain,
( ( inverse(sk_c10) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_16 )
| ( inverse(sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_94121]) ).
tcf(c_108868,plain,
iPr_def_15 = iPr_def_16,
inference(superposition,[status(thm)],[c_92754,c_76733]) ).
tcf(c_108902,plain,
~ iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_86554,c_108868]) ).
tcf(c_108944,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_86567,c_108868]) ).
tcf(c_108973,plain,
sk_c9 = iPr_def_15,
inference(demodulation,[status(thm)],[c_76694,c_108868]) ).
tcf(c_109032,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_15,X0)) = X0,
inference(demodulation,[status(thm)],[c_24458,c_108868]) ).
tcf(c_109033,plain,
inverse(iPr_def_15) = sk_c10,
inference(demodulation,[status(thm)],[c_25682,c_108868]) ).
tcf(c_109067,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_87875,c_108902]) ).
tcf(c_109111,plain,
sk_c10 = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_109033,c_76456]) ).
tcf(c_109119,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_84484,c_109111]) ).
tcf(c_109446,plain,
! [X0: $i] : multiply(sk_c10,X0) = X0,
inference(light_normalisation,[status(thm)],[c_109032,c_76503]) ).
tcf(c_109605,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_109446]) ).
tcf(c_111004,plain,
( iPr_def_14
| iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_109067,c_84785,c_87806,c_87875,c_108902,c_108868,c_109119,c_108944]) ).
tcf(c_111006,plain,
iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_111004,c_84785,c_109119,c_111004]) ).
tcf(c_117463,plain,
( ( iPr_def_29 = iPr_def_15 )
| ( iPr_def_29 != iPr_def_26 )
| ( iPr_def_15 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_60378]) ).
tcf(c_140757,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_140758,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_140757]) ).
tcf(c_140765,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_140771,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_814]) ).
tcf(c_140778,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_140765]) ).
tcf(c_140779,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_140778]) ).
tcf(c_140806,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(X0,inverse(X0)) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_140771]) ).
tcf(c_140807,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,X1) )
| ( X0 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_815]) ).
tcf(c_140808,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = sk_c11 )
| ( sk_c11 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_140806]) ).
tcf(c_140809,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_140807]) ).
tcf(c_140810,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_140809,c_140808,c_140779,c_140758,c_117463,c_111006,c_109605,c_108868,c_108973,c_109111,c_94122,c_80368,c_76378,c_76694,c_76334,c_67133,c_44312,c_39932,c_39902,c_36997,c_36837,c_17586,c_17234,c_15216,c_3018,c_2584,c_1663,c_1651,c_806,c_788,c_732,c_819,c_818,c_178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP242-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/5.39 % Computer : n017.cluster.edu
% 0.12/5.39 % Model : x86_64 x86_64
% 0.12/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.39 % Memory : 8046.5625MB
% 0.12/5.39 % OS : Linux 6.8.0-71-generic
% 0.12/5.39 % CPULimit : 300
% 0.12/5.39 % WCLimit : 300
% 0.12/5.39 % DateTime : Wed Sep 23 14:09:50 UTC 2026
% 0.12/5.39 % CPUTime :
% 0.12/5.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.43 Running first-order theorem proving
% 0.16/5.43 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.44
% 0.16/5.44 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.44
% 0.16/5.44 % Detected problem language: tptp
% 0.16/5.46 % Proving...
% 37.75/12.01 % SZS status Started for theBenchmark.p
% 37.75/12.01 % SZS status Unsatisfiable for theBenchmark.p
% 37.75/12.01
% 37.75/12.01 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 37.75/12.01
% 37.75/12.01 % ------ iProver source info
% 37.75/12.01
% 37.75/12.01 % git: date: 2026-07-19 20:42:38 +0200
% 37.75/12.01 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 37.75/12.01 % git: non_committed_changes: false
% 37.75/12.01
% 37.75/12.01 % ------ Parsing...% successful
% 37.75/12.01
% 37.75/12.01
% 37.75/12.01 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 37.75/12.01
% 37.75/12.01 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 37.75/12.01
% 37.75/12.01 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 37.75/12.01
% 37.75/12.01 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 37.75/12.01 % ------ Proving...
% 37.75/12.01 % ------ Problem Properties
% 37.75/12.01
% 37.75/12.01 %
% 37.75/12.01 % clauses 85
% 37.75/12.01 % conjectures 66
% 37.75/12.01 % EPR 61
% 37.75/12.01 % Horn 24
% 37.75/12.01 % unary 19
% 37.75/12.01 % binary 60
% 37.75/12.01 % lits 163
% 37.75/12.01 % lits eq 153
% 37.75/12.01 % fd_pure 0
% 37.75/12.01 % fd_pseudo 0
% 37.75/12.01 % fd_cond 0
% 37.75/12.01 % fd_pseudo_cond 0
% 37.75/12.01 % AC symbols 0
% 37.75/12.01
% 37.75/12.01 % ------ Schedule dynamic 5 is on
% 37.75/12.01
% 37.75/12.01 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 37.75/12.01
% 37.75/12.01
% 37.75/12.01 % ------
% 37.75/12.01 % Current options:
% 37.75/12.01 % ------
% 37.75/12.01
% 37.75/12.01
% 37.75/12.01 %
% 37.75/12.01
% 37.75/12.01 % ------ Proving...
% 37.75/12.01 %
% 37.75/12.01
% 37.75/12.01 % SZS status Unsatisfiable for theBenchmark.p
% 37.75/12.01
% 37.75/12.01 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 37.75/12.02
% 37.75/12.02
%------------------------------------------------------------------------------