%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP325-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:32:51 PM UTC 2026
% Result : Unsatisfiable 31.60s 8.45s
% Output : CNFRefutation 31.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 49
% Syntax : Number of formulae : 669 ( 107 unt; 0 def)
% Number of atoms : 1635 (1480 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 1573 ( 607 ~; 966 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 6 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 352 ( 0 sgn 352 !; 0 ?; 321 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
multiply(sk_c9,sk_c10) = sk_c8,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( inverse(sk_c9) = sk_c8
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c8 = inverse(sk_c9)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f12]) ).
fof(f18,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c10 = inverse(sk_c6)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( inverse(sk_c9) = sk_c8
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c8 = inverse(sk_c9)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c9 = inverse(sk_c5)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( inverse(sk_c7) = sk_c6
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f36]) ).
fof(f38,negated_conjecture,
( inverse(sk_c6) = sk_c10
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f39,plain,
( sk_c10 = inverse(sk_c6)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f38]) ).
fof(f40,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| inverse(sk_c1) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f41,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c9 = inverse(sk_c1) ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( inverse(sk_c9) = sk_c8
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c8 = inverse(sk_c9)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f49,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f48]) ).
fof(f50,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c9 = inverse(sk_c5)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f50]) ).
fof(f52,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f53,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f52]) ).
fof(f54,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( inverse(sk_c7) = sk_c6
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f54]) ).
fof(f56,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f57,plain,
( sk_c10 = inverse(sk_c6)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f56]) ).
fof(f58,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| multiply(sk_c10,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f59,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c3) ),
inference(reorient_equations,[],[f58]) ).
fof(f60,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c2,sk_c10) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f61,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c3 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f60]) ).
fof(f62,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f63,plain,
( sk_c10 = inverse(sk_c4)
| sk_c3 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f62]) ).
fof(f64,negated_conjecture,
( inverse(sk_c9) = sk_c8
| multiply(sk_c2,sk_c10) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( sk_c8 = inverse(sk_c9)
| sk_c3 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c2,sk_c10) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c3 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f66]) ).
fof(f72,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c2,sk_c10) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( inverse(sk_c7) = sk_c6
| sk_c3 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f72]) ).
fof(f74,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c10 = inverse(sk_c6)
| sk_c3 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f74]) ).
fof(f76,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| multiply(sk_c2,sk_c10) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f77,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c3 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f76]) ).
fof(f78,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f79,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f78]) ).
fof(f80,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_39) ).
fof(f81,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f80]) ).
fof(f82,negated_conjecture,
( inverse(sk_c9) = sk_c8
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f83,plain,
( sk_c8 = inverse(sk_c9)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f82]) ).
fof(f84,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
( sk_c9 = inverse(sk_c5)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f89,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f88]) ).
fof(f90,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f91,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f90]) ).
fof(f92,negated_conjecture,
( inverse(sk_c6) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f93,plain,
( sk_c10 = inverse(sk_c6)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f92]) ).
fof(f96,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,sk_c10) != X6
| inverse(X6) != sk_c10
| inverse(X5) != X6
| multiply(X4,sk_c8) != sk_c9
| inverse(X4) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c10
| multiply(X2,sk_c10) != X1
| multiply(sk_c10,X1) != sk_c9
| inverse(X0) != sk_c9
| multiply(X0,sk_c9) != sk_c10
| multiply(sk_c9,sk_c10) != sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f97,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,sk_c10) != X6
| sk_c10 != inverse(X6)
| inverse(X5) != X6
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c8 != inverse(sk_c9)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c10 != inverse(X2)
| multiply(X2,sk_c10) != X1
| sk_c9 != multiply(sk_c10,X1)
| inverse(X0) != sk_c9
| sk_c10 != multiply(X0,sk_c9)
| multiply(sk_c9,sk_c10) != sk_c8 ),
inference(reorient_equations,[],[f96]) ).
fof(f98,plain,
! [X2,X3,X0,X6,X4,X5] :
( multiply(X5,sk_c10) != X6
| sk_c10 != inverse(X6)
| inverse(X5) != X6
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c8 != inverse(sk_c9)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c10 != inverse(X2)
| sk_c9 != multiply(sk_c10,multiply(X2,sk_c10))
| inverse(X0) != sk_c9
| sk_c10 != multiply(X0,sk_c9)
| multiply(sk_c9,sk_c10) != sk_c8 ),
inference(equality_resolution,[],[f97]) ).
fof(f99,plain,
! [X2,X3,X0,X4,X5] :
( inverse(X5) != multiply(X5,sk_c10)
| sk_c10 != inverse(inverse(X5))
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c8 != inverse(sk_c9)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c10 != inverse(X2)
| sk_c9 != multiply(sk_c10,multiply(X2,sk_c10))
| inverse(X0) != sk_c9
| sk_c10 != multiply(X0,sk_c9)
| multiply(sk_c9,sk_c10) != sk_c8 ),
inference(equality_resolution,[],[f98]) ).
tcf(c_99,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_100,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_102,negated_conjecture,
multiply(sk_c9,sk_c10) = sk_c8,
inference(cnf_transformation,[],[f5]) ).
tcf(c_103,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_104,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_106,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_111,negated_conjecture,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_121,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_124,negated_conjecture,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_129,negated_conjecture,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( multiply(sk_c10,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c3 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_133,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c3 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c3 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c3 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_148,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c9) != sk_c8 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c10 )
| ( inverse(X1) != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c8 )
| ( inverse(inverse(X0)) != sk_c10 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c8) != sk_c9 )
| ( multiply(X1,sk_c9) != sk_c10 )
| ( multiply(X0,sk_c10) != inverse(X0) )
| ( multiply(sk_c10,multiply(X2,sk_c10)) != sk_c9 ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_150,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c9) != sk_c8 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c10 )
| ( inverse(X1) != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c10,multiply(X2,sk_c10)) != sk_c9 )
| ( multiply(X0,sk_c10) != inverse(X0) )
| ( multiply(X1,sk_c9) != sk_c10 )
| ( multiply(X3,sk_c8) != sk_c9 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( inverse(inverse(X0)) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_148,c_102,c_148]) ).
tcf(c_154,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c9) != sk_c8 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c9 )
| ( inverse(X2) != sk_c9 )
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( inverse(inverse(X1)) != sk_c10 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c8) != sk_c9 )
| ( multiply(X2,sk_c9) != sk_c10 )
| ( multiply(X1,sk_c10) != inverse(X1) )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(renaming,[status(thm)],[c_153]) ).
tcf(c_574,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_154]) ).
tcf(c_575,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_154]) ).
tcf(c_576,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(inverse(X0)) != sk_c10 )
| ( multiply(X0,sk_c10) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_154]) ).
tcf(c_577,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_154]) ).
tcf(c_578,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_154]) ).
tcf(c_579,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_154]) ).
tcf(c_580,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_581,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_582,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_583,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_586,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_589,plain,
( ~ iPr_def_12
| ( inverse(inverse(sk_c10)) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_576]) ).
tcf(c_842,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c9) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(X0,sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_844,plain,
multiply(identity,sk_c9) = sk_c9,
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_846,plain,
multiply(inverse(sk_c9),sk_c9) = identity,
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_855,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c9) = X2 )
| ( X2 != X1 )
| ( multiply(X0,sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_856,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c9) = sk_c10 )
| ( sk_c10 != multiply(X1,X2) )
| ( multiply(X0,sk_c9) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_842]) ).
tcf(c_857,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c9) = multiply(X1,X2) )
| ( sk_c9 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_868,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,sk_c9) )
| ( sk_c10 != X1 )
| ( multiply(X0,sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_869,plain,
( ( sk_c10 = multiply(sk_c10,sk_c9) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_868]) ).
tcf(c_882,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_855]) ).
tcf(c_885,plain,
! [X0: $i] :
( ( sk_c10 = sk_c9 )
| ( sk_c10 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_886,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c10 != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_885]) ).
tcf(c_887,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_889,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_891,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c9) = multiply(X1,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_857]) ).
tcf(c_892,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_893,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_897,plain,
! [X0: $i] :
( ( inverse(inverse(sk_c9)) = sk_c9 )
| ( sk_c9 != X0 )
| ( inverse(inverse(sk_c9)) != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_907,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_925,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c6,sk_c7) = identity ) ),
inference(superposition,[status(thm)],[c_118,c_100]) ).
tcf(c_934,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_940,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_944,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_968,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c9) = X2 )
| ( X2 != multiply(X1,sk_c9) )
| ( multiply(X0,sk_c9) != multiply(X1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_855]) ).
tcf(c_980,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c9) )
| ( X2 != X1 )
| ( multiply(X0,sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_982,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(X1,sk_c9) )
| ( X2 != sk_c9 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_984,plain,
( ( multiply(sk_c10,sk_c10) = multiply(sk_c10,sk_c9) )
| ( sk_c10 != sk_c10 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_1041,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c1,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_110,c_101]) ).
tcf(c_1042,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_109,c_101]) ).
tcf(c_1044,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c1,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_105,c_101]) ).
tcf(c_1045,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,multiply(sk_c9,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_104,c_101]) ).
tcf(c_1062,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c2,multiply(sk_c10,X0)) = multiply(sk_c3,X0) ) ),
inference(superposition,[status(thm)],[c_137,c_101]) ).
tcf(c_1063,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c2,multiply(sk_c10,X0)) = multiply(sk_c3,X0) ) ),
inference(superposition,[status(thm)],[c_136,c_101]) ).
tcf(c_1066,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,multiply(sk_c10,X0)) = multiply(sk_c3,X0) ) ),
inference(superposition,[status(thm)],[c_131,c_101]) ).
tcf(c_1068,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_100,c_101]) ).
tcf(c_1109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1180,plain,
( ( sk_c10 = multiply(sk_c4,sk_c10) )
| ( sk_c10 != sk_c9 )
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_889]) ).
tcf(c_1243,plain,
( ( sk_c9 = multiply(sk_c10,sk_c8) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_944]) ).
tcf(c_1244,plain,
( ( sk_c9 = inverse(sk_c5) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c5) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_944]) ).
tcf(c_1250,plain,
( ( sk_c9 = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_944]) ).
tcf(c_1286,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_1287,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1288,plain,
( ( identity = sk_c10 )
| ( identity != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_1330,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c9),sk_c9) )
| ( X0 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_1333,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c9) )
| ( X2 != multiply(X1,sk_c9) )
| ( multiply(X0,sk_c9) != multiply(X1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_1335,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c9) )
| ( X0 != multiply(sk_c10,sk_c8) )
| ( multiply(identity,sk_c9) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_1415,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1068,c_99]) ).
tcf(c_1423,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c10,multiply(sk_c6,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_119,c_1415]) ).
tcf(c_1426,plain,
multiply(inverse(sk_c9),sk_c8) = sk_c10,
inference(superposition,[status(thm)],[c_102,c_1415]) ).
tcf(c_1427,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_110,c_1415]) ).
tcf(c_1428,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_109,c_1415]) ).
tcf(c_1431,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_104,c_1415]) ).
tcf(c_1432,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_112,c_1415]) ).
tcf(c_1434,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(inverse(sk_c5),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_117,c_1415]) ).
tcf(c_1439,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_100,c_1415]) ).
tcf(c_1447,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_1415,c_1415]) ).
tcf(c_1498,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_1109]) ).
tcf(c_1504,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X0,X1),
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1508,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X1) = X4 )
| ( X4 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_1109]) ).
tcf(c_1727,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c5) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_575,c_117]) ).
tcf(c_1728,plain,
( ( inverse(sk_c2) = sk_c10 )
| ~ iPr_def_11
| ( inverse(sk_c5) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_575,c_144]) ).
tcf(c_1730,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c5) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_575,c_126]) ).
tcf(c_1775,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_13
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_577,c_112]) ).
tcf(c_1777,plain,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ~ iPr_def_13
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_577,c_103]) ).
tcf(c_1778,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_13
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_577,c_121]) ).
tcf(c_1825,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = X0 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_581,c_102]) ).
tcf(c_1832,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c9) = X0 )
| ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_581,c_106]) ).
tcf(c_1859,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = X0 )
| ( X0 != sk_c6 ) ),
inference(resolution,[status(thm)],[c_581,c_120]) ).
tcf(c_1862,plain,
! [X0: $i] :
( ( multiply(sk_c7,sk_c10) = X0 )
| ( multiply(sk_c10,sk_c3) = sk_c9 )
| ( X0 != sk_c6 ) ),
inference(resolution,[status(thm)],[c_581,c_129]) ).
tcf(c_1869,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_581,c_122]) ).
tcf(c_1872,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c3) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_581,c_127]) ).
tcf(c_1873,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_581,c_128]) ).
tcf(c_1874,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c3) = X0 )
| ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_581,c_124]) ).
tcf(c_1899,plain,
! [X0: $i] :
( ( inverse(sk_c2) = X0 )
| ( inverse(sk_c4) = sk_c10 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_581,c_140]) ).
tcf(c_1902,plain,
! [X0: $i] :
( ( inverse(sk_c2) = X0 )
| ( inverse(sk_c7) = sk_c6 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_581,c_145]) ).
tcf(c_1903,plain,
! [X0: $i] :
( ( inverse(sk_c2) = X0 )
| ( inverse(sk_c6) = sk_c10 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_581,c_146]) ).
tcf(c_1904,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_581,c_99]) ).
tcf(c_1905,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_581,c_100]) ).
tcf(c_1909,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_581,c_580]) ).
tcf(c_1910,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_581,c_583]) ).
tcf(c_1921,plain,
( ( sk_c9 = inverse(sk_c1) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_944]) ).
tcf(c_1925,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c10,sk_c3) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_944]) ).
tcf(c_1949,plain,
! [X0: $i] :
( ( multiply(X0,sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c1,sk_c9) )
| ( multiply(X0,sk_c9) != multiply(sk_c1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_856]) ).
tcf(c_1983,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(inverse(sk_c2),sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_131,c_1415]) ).
tcf(c_2028,plain,
( ( multiply(inverse(sk_c9),sk_c9) = multiply(sk_c1,sk_c9) )
| ( multiply(sk_c1,sk_c9) != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_882]) ).
tcf(c_2048,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c2),sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_132,c_1415]) ).
tcf(c_2054,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(inverse(sk_c2),sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_136,c_1415]) ).
tcf(c_2057,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(inverse(sk_c2),sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_137,c_1415]) ).
tcf(c_2060,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_1415]) ).
tcf(c_2066,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(inverse(sk_c5),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_144,c_1415]) ).
tcf(c_2096,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(inverse(sk_c1),sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_106,c_1415]) ).
tcf(c_2133,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c10,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_102,c_101]) ).
tcf(c_2181,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_101,c_1415]) ).
tcf(c_2245,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c10,sk_c8) )
| ( X1 != sk_c8 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_2247,plain,
( ( multiply(sk_c10,sk_c10) = multiply(sk_c10,sk_c8) )
| ( sk_c10 != sk_c8 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2245]) ).
tcf(c_2282,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(inverse(sk_c2),sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_133,c_1415]) ).
tcf(c_2290,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_2330,plain,
( ( multiply(sk_c10,sk_c8) = multiply(identity,sk_c9) )
| ( multiply(identity,sk_c9) != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,sk_c8) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1335]) ).
tcf(c_2331,plain,
multiply(sk_c10,sk_c8) = multiply(sk_c10,sk_c8),
inference(instantiation,[status(thm)],[c_1504]) ).
tcf(c_2370,plain,
( ( inverse(sk_c6) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_110,c_574]) ).
tcf(c_2371,plain,
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_109,c_574]) ).
tcf(c_2374,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_104,c_574]) ).
tcf(c_2376,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_100,c_574]) ).
tcf(c_2389,plain,
! [X0: $i] :
( ( multiply(X0,sk_c9) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(X0,sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_968]) ).
tcf(c_2390,plain,
( ( multiply(sk_c10,sk_c9) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(sk_c10,sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2389]) ).
tcf(c_2440,plain,
( ( identity = multiply(inverse(sk_c9),sk_c9) )
| ( identity != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_1330]) ).
tcf(c_2456,plain,
! [X0: $i] :
( ( identity = multiply(inverse(X0),X0) )
| ( identity != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_2457,plain,
( ( identity = multiply(inverse(sk_c10),sk_c10) )
| ( identity != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_2456]) ).
tcf(c_2475,plain,
! [X0: $i] :
( ( multiply(X0,sk_c9) = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_891]) ).
tcf(c_2477,plain,
( ( multiply(sk_c10,sk_c9) = multiply(identity,sk_c9) )
| ( sk_c10 != identity )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2475]) ).
tcf(c_2508,plain,
( ~ iPr_def_13
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_100,c_577]) ).
tcf(c_2529,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),X0) )
| ( X2 != X1 )
| ( multiply(inverse(X0),X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_2530,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2529]) ).
tcf(c_2691,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_1439,c_1447]) ).
tcf(c_2703,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_1447,c_100]) ).
tcf(c_2720,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X2) = X4 )
| ( X4 != multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_582,c_581]) ).
tcf(c_2740,plain,
! [X0: $i] :
( ( sk_c9 = multiply(X0,sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(X0,sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1333]) ).
tcf(c_2741,plain,
( ( sk_c9 = multiply(sk_c10,sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(sk_c10,sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2740]) ).
tcf(c_2747,plain,
sk_c8 = multiply(sk_c9,sk_c10),
inference(resolution,[status(thm)],[c_1909,c_102]) ).
tcf(c_2748,plain,
( ( sk_c10 = multiply(sk_c1,sk_c9) )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1909,c_104]) ).
tcf(c_2751,plain,
( ( sk_c10 = multiply(sk_c1,sk_c9) )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(resolution,[status(thm)],[c_1909,c_109]) ).
tcf(c_2752,plain,
( ( sk_c10 = multiply(sk_c1,sk_c9) )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1909,c_110]) ).
tcf(c_2754,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_1909,c_112]) ).
tcf(c_2756,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1909,c_103]) ).
tcf(c_2767,plain,
( ( sk_c10 = inverse(sk_c6) )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_1909,c_119]) ).
tcf(c_2773,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1909,c_122]) ).
tcf(c_2774,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_1909,c_123]) ).
tcf(c_2776,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(resolution,[status(thm)],[c_1909,c_127]) ).
tcf(c_2777,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1909,c_128]) ).
tcf(c_2778,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_1909,c_124]) ).
tcf(c_3010,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X0) = X2 )
| ( X2 != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1109]) ).
tcf(c_3209,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c10 )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_1426,c_575]) ).
tcf(c_3254,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_129,c_576]) ).
tcf(c_3257,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_120,c_576]) ).
tcf(c_3463,plain,
( ( inverse(sk_c6) = sk_c10 )
| ~ iPr_def_14
| ( inverse(sk_c2) != sk_c10 )
| ( multiply(sk_c10,sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_137,c_578]) ).
tcf(c_3464,plain,
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_14
| ( inverse(sk_c2) != sk_c10 )
| ( multiply(sk_c10,sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_136,c_578]) ).
tcf(c_3467,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_14
| ( inverse(sk_c2) != sk_c10 )
| ( multiply(sk_c10,sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_131,c_578]) ).
tcf(c_3468,plain,
( ~ iPr_def_14
| ( inverse(identity) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_99,c_578]) ).
tcf(c_3541,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(X0,X1) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1508]) ).
tcf(c_3666,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_142,c_579]) ).
tcf(c_3678,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = sk_c10 )
| ( sk_c10 != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_3687,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( X0 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_3699,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_140,c_2703]) ).
tcf(c_3705,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c6,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_146,c_2703]) ).
tcf(c_3709,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_2703,c_99]) ).
tcf(c_3731,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,X1) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1508]) ).
tcf(c_3732,plain,
( ( multiply(sk_c10,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_3731]) ).
tcf(c_3738,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c9,sk_c10) )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_1825,c_1909]) ).
tcf(c_3747,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != inverse(sk_c5) )
| ( X0 != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_3801,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X1) = X2 )
| ( X2 != X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1904,c_581]) ).
tcf(c_4033,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_3699,c_139]) ).
tcf(c_4255,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( X0 != multiply(sk_c9,sk_c10) ) ),
inference(resolution,[status(thm)],[c_2747,c_581]) ).
tcf(c_4257,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c1) )
| ( sk_c10 != X0 )
| ( inverse(sk_c1) != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_4258,plain,
( ( sk_c10 = inverse(sk_c1) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_4257]) ).
tcf(c_4435,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c10 != X0 )
| ( multiply(inverse(sk_c9),sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_868]) ).
tcf(c_4438,plain,
( ( sk_c10 = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c10 != sk_c10 )
| ( multiply(inverse(sk_c9),sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_4435]) ).
tcf(c_4440,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = sk_c10 )
| ( sk_c10 != multiply(X2,sk_c9) )
| ( multiply(X0,X1) != multiply(X2,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1508]) ).
tcf(c_4441,plain,
( ( multiply(sk_c10,sk_c10) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c9) )
| ( multiply(sk_c10,sk_c10) != multiply(sk_c10,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_4440]) ).
tcf(c_4656,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != multiply(X0,sk_c9) )
| ( sk_c10 != multiply(X0,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_887]) ).
tcf(c_4708,plain,
! [X0: $i,X1: $i] :
( ( X0 = multiply(inverse(X1),X1) )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_1905,c_1909]) ).
tcf(c_4709,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_4708]) ).
tcf(c_4818,plain,
( ( inverse(sk_c2) = sk_c10 )
| ~ iPr_def_13
| ( sk_c9 != identity )
| ( inverse(sk_c6) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_3705,c_577]) ).
tcf(c_4925,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c10,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_4033,c_100]) ).
tcf(c_5088,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_142,c_579]) ).
tcf(c_5089,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_115,c_579]) ).
tcf(c_5090,plain,
( iPr_def_14
| iPr_def_10
| ( inverse(sk_c2) = sk_c10 )
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_5088,c_146,c_143,c_141,c_1728,c_3666,c_4033,c_4818]) ).
tcf(c_5091,plain,
( iPr_def_14
| iPr_def_12
| iPr_def_10
| ( inverse(sk_c2) = sk_c10 ) ),
inference(renaming,[status(thm)],[c_5090]) ).
tcf(c_5096,plain,
( iPr_def_14
| iPr_def_10
| ( inverse(sk_c1) = sk_c9 )
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_5089,c_116,c_114,c_113,c_115,c_579,c_1727,c_1775]) ).
tcf(c_5097,plain,
( iPr_def_14
| iPr_def_12
| iPr_def_10
| ( inverse(sk_c1) = sk_c9 ) ),
inference(renaming,[status(thm)],[c_5096]) ).
tcf(c_5104,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(sk_c10,multiply(sk_c2,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_4925,c_101]) ).
tcf(c_5204,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c10 )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_1426,c_575]) ).
tcf(c_5217,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_1439,c_2691]) ).
tcf(c_5218,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( X0 != sk_c10 )
| ( multiply(X0,sk_c10) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_576,c_5217]) ).
tcf(c_5220,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5204,c_5217]) ).
tcf(c_5221,plain,
( ~ iPr_def_13
| ( sk_c9 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2508,c_5217]) ).
tcf(c_5222,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2376,c_5217]) ).
tcf(c_5223,plain,
( ~ iPr_def_12
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_5218]) ).
tcf(c_5238,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_5217,c_100]) ).
tcf(c_5242,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_113,c_5238]) ).
tcf(c_5258,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_5238,c_101]) ).
tcf(c_5490,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_5258,c_99]) ).
tcf(c_5496,plain,
! [X0: $i] : multiply(X0,identity) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_5238,c_5490]) ).
tcf(c_5530,plain,
( ~ iPr_def_14
| ( sk_c9 != sk_c10 )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_5490,c_578]) ).
tcf(c_5534,plain,
( ~ iPr_def_14
| ( sk_c9 != sk_c10 )
| ( multiply(sk_c10,identity) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_5530,c_5496]) ).
tcf(c_5535,plain,
( ~ iPr_def_14
| ( sk_c9 != sk_c10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5534,c_2691]) ).
tcf(c_6422,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c2) = X0 )
| ( inverse(sk_c4) = sk_c10 )
| ( X1 != sk_c10 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1899,c_581]) ).
tcf(c_6486,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c2) = X0 )
| ( inverse(sk_c7) = sk_c6 )
| ( X1 != sk_c10 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1902,c_581]) ).
tcf(c_6636,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != multiply(X1,sk_c9) )
| ( X0 != multiply(X1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_6700,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_5242,c_112]) ).
tcf(c_6709,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_2756,c_574]) ).
tcf(c_6715,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_6700,c_5238]) ).
tcf(c_6974,plain,
( ( sk_c10 = identity )
| ( sk_c9 = identity )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_6715,c_106]) ).
tcf(c_6979,plain,
( ( sk_c10 = identity )
| ( sk_c9 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_6715,c_104]) ).
tcf(c_7284,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_2778,c_579]) ).
tcf(c_7422,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(X1,sk_c9) )
| ( X0 != multiply(X1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_7424,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c9) )
| ( sk_c9 != multiply(sk_c10,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_7422]) ).
tcf(c_7501,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c2) = X0 )
| ( inverse(sk_c6) = sk_c10 )
| ( X1 != sk_c10 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1903,c_581]) ).
tcf(c_7855,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(sk_c10,sk_c8) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_3541]) ).
tcf(c_8532,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(sk_c10,multiply(sk_c2,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_5104,c_99]) ).
tcf(c_8545,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_131,c_8532]) ).
tcf(c_8664,plain,
( ( multiply(inverse(sk_c9),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c1,sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(sk_c1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1949]) ).
tcf(c_8665,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(inverse(sk_c9),sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_842]) ).
tcf(c_8947,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_8948,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_8947]) ).
tcf(c_9083,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c7,sk_c10) )
| ( inverse(sk_c1) = sk_c9 )
| ( X0 != sk_c6 ) ),
inference(resolution,[status(thm)],[c_1859,c_1909]) ).
tcf(c_9398,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_1730,c_125,c_1730]) ).
tcf(c_9408,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ~ iPr_def_11 ),
inference(resolution,[status(thm)],[c_9398,c_1909]) ).
tcf(c_9452,plain,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_1777,c_104,c_1777]) ).
tcf(c_9470,plain,
( ( sk_c10 = multiply(sk_c1,sk_c9) )
| ~ iPr_def_13 ),
inference(resolution,[status(thm)],[c_9452,c_1909]) ).
tcf(c_9598,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_1778,c_122,c_1778]) ).
tcf(c_9612,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ~ iPr_def_13 ),
inference(resolution,[status(thm)],[c_9598,c_1909]) ).
tcf(c_10108,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_6709,c_2754,c_6709]) ).
tcf(c_10168,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_140,c_2060]) ).
tcf(c_10425,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = multiply(identity,inverse(X1)) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1910,c_99]) ).
tcf(c_11229,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c9) )
| ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_1832,c_1909]) ).
tcf(c_11479,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = sk_c9 )
| ( sk_c9 != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_3010]) ).
tcf(c_11798,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_1862,c_576]) ).
tcf(c_12216,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_1439,c_2691]) ).
tcf(c_12232,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_12216,c_100]) ).
tcf(c_12236,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_113,c_12232]) ).
tcf(c_12564,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_12236,c_112]) ).
tcf(c_12573,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c9) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_12564,c_12216]) ).
tcf(c_12956,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c9,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_116,c_1434]) ).
tcf(c_13113,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_2048]) ).
tcf(c_13129,plain,
( ( sk_c9 = sk_c10 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_13113,c_123]) ).
tcf(c_13146,plain,
( ( sk_c8 = sk_c1 )
| ( sk_c9 = identity )
| ( sk_c9 = sk_c10 ) ),
inference(superposition,[status(thm)],[c_13129,c_12573]) ).
tcf(c_13317,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c9,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_143,c_2066]) ).
tcf(c_14026,plain,
( iPr_def_14
| iPr_def_10
| ( sk_c9 = multiply(sk_c10,sk_c3) )
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_7284,c_579,c_2778,c_2774,c_9408,c_9612]) ).
tcf(c_14027,plain,
( iPr_def_14
| iPr_def_12
| iPr_def_10
| ( sk_c9 = multiply(sk_c10,sk_c3) ) ),
inference(renaming,[status(thm)],[c_14026]) ).
tcf(c_14536,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != multiply(inverse(X0),X0) )
| ( sk_c10 != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_887]) ).
tcf(c_14537,plain,
( ( sk_c10 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_14536]) ).
tcf(c_14539,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(X1),X1) )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_14541,plain,
( ( identity = sk_c10 )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_14539]) ).
tcf(c_15330,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(inverse(X0)) = X2 )
| ( X2 != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_15331,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = sk_c10 )
| ( sk_c10 != inverse(X1) )
| ( inverse(inverse(X0)) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_3678]) ).
tcf(c_15332,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_583]) ).
tcf(c_15333,plain,
( ( inverse(inverse(sk_c10)) = sk_c10 )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(inverse(sk_c10)) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_15331]) ).
tcf(c_15334,plain,
( ( inverse(inverse(sk_c10)) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_15332]) ).
tcf(c_16518,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,sk_c8)) = sk_c10,
inference(superposition,[status(thm)],[c_102,c_2181]) ).
tcf(c_16592,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(inverse(multiply(X0,sk_c9)),multiply(X0,sk_c8)) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_13317,c_2181]) ).
tcf(c_16593,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(inverse(multiply(X0,sk_c9)),multiply(X0,sk_c8)) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_12956,c_2181]) ).
tcf(c_16703,plain,
( ( sk_c9 = sk_c10 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_16593,c_16518]) ).
tcf(c_16704,plain,
( ( sk_c9 = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_16592,c_16518]) ).
tcf(c_18793,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X3,X2) = inverse(X0) )
| ( X3 != identity )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_10425,c_2720]) ).
tcf(c_18794,plain,
( ( multiply(sk_c10,sk_c10) = inverse(sk_c10) )
| ( sk_c10 != identity )
| ( sk_c10 != sk_c10 )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_18793]) ).
tcf(c_19020,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_12
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_11798,c_127,c_3254]) ).
tcf(c_19034,plain,
( ( sk_c9 = multiply(sk_c10,sk_c3) )
| ~ iPr_def_12
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_19020,c_1909]) ).
tcf(c_19487,plain,
( ( sk_c10 = identity )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_4656]) ).
tcf(c_19919,plain,
( ( inverse(inverse(sk_c9)) = sk_c9 )
| ( sk_c9 != inverse(sk_c1) )
| ( inverse(inverse(sk_c9)) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_897]) ).
tcf(c_19926,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != inverse(sk_c1) )
| ( X0 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_19927,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c10 != inverse(sk_c1) )
| ( sk_c9 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_19926]) ).
tcf(c_19942,plain,
! [X0: $i] :
( ( multiply(identity,X0) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c3) )
| ( multiply(identity,X0) != multiply(sk_c10,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_11479]) ).
tcf(c_19944,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c3) )
| ( X0 != multiply(sk_c10,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_19945,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(sk_c10,sk_c3) )
| ( X0 != multiply(sk_c10,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_19946,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c3) )
| ( sk_c9 != multiply(sk_c10,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_19945]) ).
tcf(c_20022,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ~ iPr_def_10 ),
inference(resolution,[status(thm)],[c_10108,c_1909]) ).
tcf(c_20208,plain,
! [X0: $i] :
( iPr_def_14
| iPr_def_12
| iPr_def_10
| ( sk_c9 = X0 )
| ( X0 != multiply(sk_c10,sk_c3) ) ),
inference(resolution,[status(thm)],[c_14027,c_581]) ).
tcf(c_20209,plain,
( iPr_def_14
| iPr_def_12
| iPr_def_10
| ( sk_c9 = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_20208]) ).
tcf(c_21126,plain,
! [X0: $i] :
( ( multiply(identity,X0) = multiply(sk_c10,sk_c3) )
| ( multiply(sk_c10,sk_c3) != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_1498]) ).
tcf(c_22594,plain,
! [X0: $i] :
( iPr_def_14
| iPr_def_12
| iPr_def_10
| ( multiply(identity,X0) = sk_c9 )
| ( multiply(sk_c10,sk_c3) != X0 ) ),
inference(resolution,[status(thm)],[c_3801,c_14027]) ).
tcf(c_24716,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( X0 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_6636]) ).
tcf(c_24717,plain,
( ( identity = sk_c10 )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_24716]) ).
tcf(c_24896,plain,
( ( inverse(inverse(sk_c7)) = inverse(sk_c6) )
| ( inverse(sk_c7) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_15332]) ).
tcf(c_24902,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_25600,plain,
( ( identity = multiply(sk_c4,sk_c10) )
| ( identity != identity )
| ( multiply(sk_c4,sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_25965,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_100,c_2691]) ).
tcf(c_26005,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c1) = sk_c9 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_115,c_579]) ).
tcf(c_26006,plain,
( iPr_def_12
| ( inverse(sk_c1) = sk_c9 )
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_26005,c_5097,c_5535,c_16703]) ).
tcf(c_26007,plain,
( iPr_def_12
| iPr_def_10
| ( inverse(sk_c1) = sk_c9 ) ),
inference(renaming,[status(thm)],[c_26006]) ).
tcf(c_26236,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_1439,c_2691]) ).
tcf(c_26237,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( X0 != sk_c10 )
| ( multiply(X0,sk_c10) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_576,c_26236]) ).
tcf(c_26252,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_26236,c_100]) ).
tcf(c_26256,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_113,c_26252]) ).
tcf(c_26263,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_114,c_26252]) ).
tcf(c_26264,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c2,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_4033,c_26252]) ).
tcf(c_26269,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_26252,c_101]) ).
tcf(c_26270,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_26252,c_101]) ).
tcf(c_26368,plain,
( ( sk_c3 = identity )
| ( sk_c9 = identity )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_26264,c_133]) ).
tcf(c_26377,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_26269,c_99]) ).
tcf(c_26470,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_26256,c_112]) ).
tcf(c_26477,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_26470,c_26252]) ).
tcf(c_26515,plain,
( ( sk_c10 = identity )
| ( sk_c9 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_26477,c_104]) ).
tcf(c_26557,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c6) = sk_c10 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_26263,c_110]) ).
tcf(c_26558,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_26263,c_109]) ).
tcf(c_26635,plain,
( ( inverse(sk_c6) = sk_c10 )
| ~ iPr_def_13
| ( inverse(inverse(sk_c1)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1427,c_577]) ).
tcf(c_26647,plain,
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_13
| ( inverse(inverse(sk_c1)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1428,c_577]) ).
tcf(c_26683,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_13
| ( inverse(inverse(sk_c1)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1431,c_577]) ).
tcf(c_26688,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_113,c_1432]) ).
tcf(c_26694,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_26688,c_574]) ).
tcf(c_26712,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c1,multiply(sk_c9,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_106,c_26270]) ).
tcf(c_26821,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c9,sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_116,c_1434]) ).
tcf(c_26922,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_2048]) ).
tcf(c_27080,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_140,c_2060]) ).
tcf(c_27088,plain,
( ( inverse(sk_c2) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_27080,c_574]) ).
tcf(c_27423,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(multiply(sk_c10,sk_c6)) = identity ) ),
inference(superposition,[status(thm)],[c_1423,c_26270]) ).
tcf(c_27749,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,sk_c8)) = sk_c10,
inference(superposition,[status(thm)],[c_102,c_2181]) ).
tcf(c_27777,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(multiply(X0,sk_c10)),multiply(X0,sk_c10)) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_26922,c_2181]) ).
tcf(c_27825,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(inverse(multiply(X0,sk_c9)),multiply(X0,sk_c8)) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_26821,c_2181]) ).
tcf(c_27878,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = inverse(X1),
inference(superposition,[status(thm)],[c_26252,c_2181]) ).
tcf(c_27880,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = multiply(X2,inverse(multiply(X1,X2))),
inference(superposition,[status(thm)],[c_26270,c_2181]) ).
tcf(c_27885,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(X1),X2),
inference(superposition,[status(thm)],[c_26377,c_2181]) ).
tcf(c_27935,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_27880,c_27878]) ).
tcf(c_27937,plain,
( ( sk_c9 = sk_c10 )
| ( inverse(sk_c1) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_27825,c_27749]) ).
tcf(c_27970,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c3 ) ),
inference(demodulation,[status(thm)],[c_27777,c_27885]) ).
tcf(c_28104,plain,
( ( sk_c9 = sk_c10 )
| ( multiply(sk_c1,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_27937,c_26252]) ).
tcf(c_28127,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c8,inverse(sk_c9)) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_142,c_27935]) ).
tcf(c_28132,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c8,inverse(sk_c9)) = inverse(sk_c5) ) ),
inference(superposition,[status(thm)],[c_144,c_27935]) ).
tcf(c_28141,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c3,inverse(sk_c9)) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_128,c_27935]) ).
tcf(c_28142,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c3,inverse(sk_c9)) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_127,c_27935]) ).
tcf(c_28145,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c3,inverse(sk_c9)) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_122,c_27935]) ).
tcf(c_28149,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,inverse(sk_c3)) = inverse(sk_c2) ) ),
inference(superposition,[status(thm)],[c_137,c_27935]) ).
tcf(c_28150,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,inverse(sk_c3)) = inverse(sk_c2) ) ),
inference(superposition,[status(thm)],[c_136,c_27935]) ).
tcf(c_28153,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,inverse(sk_c3)) = inverse(sk_c2) ) ),
inference(superposition,[status(thm)],[c_131,c_27935]) ).
tcf(c_28155,plain,
! [X0: $i] : multiply(X0,inverse(identity)) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_100,c_27935]) ).
tcf(c_28164,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( multiply(sk_c7,inverse(identity)) = inverse(sk_c6) ) ),
inference(superposition,[status(thm)],[c_925,c_27935]) ).
tcf(c_28322,plain,
( ( inverse(sk_c1) = sk_c9 )
| ( inverse(inverse(sk_c7)) = inverse(sk_c6) ) ),
inference(demodulation,[status(thm)],[c_28164,c_28155]) ).
tcf(c_28507,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_27878,c_2691]) ).
tcf(c_28523,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(inverse(sk_c9),sk_c4) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_139,c_28507]) ).
tcf(c_29467,plain,
( ( sk_c10 = identity )
| ( identity != multiply(sk_c4,sk_c10) )
| ( sk_c10 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_887]) ).
tcf(c_30561,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_30572,plain,
( ( identity = sk_c9 )
| ( identity != identity )
| ( sk_c9 != identity ) ),
inference(instantiation,[status(thm)],[c_1286]) ).
tcf(c_30574,plain,
( ( multiply(inverse(sk_c9),sk_c9) = sk_c9 )
| ( sk_c9 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_882]) ).
tcf(c_30575,plain,
( ( sk_c9 = identity )
| ( identity != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_30561]) ).
tcf(c_30582,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(inverse(X0),X0) )
| ( sk_c9 != X1 )
| ( multiply(inverse(X0),X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_30585,plain,
( ( sk_c9 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c9 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_30582]) ).
tcf(c_30625,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_893]) ).
tcf(c_30627,plain,
( ( sk_c9 = inverse(sk_c10) )
| ( sk_c9 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_30625]) ).
tcf(c_30848,plain,
! [X0: $i] :
( ( sk_c10 = multiply(sk_c10,sk_c3) )
| ( sk_c10 != X0 )
| ( multiply(sk_c10,sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_889]) ).
tcf(c_30849,plain,
( ( sk_c10 = multiply(sk_c10,sk_c3) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c3) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_30848]) ).
tcf(c_31198,plain,
( ( multiply(inverse(sk_c9),sk_c9) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( multiply(inverse(sk_c9),sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_8665]) ).
tcf(c_31209,plain,
( ( sk_c10 = identity )
| ( identity != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_887]) ).
tcf(c_31219,plain,
! [X0: $i] :
( ( sk_c8 = sk_c9 )
| ( sk_c8 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_31223,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c8 != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_31219]) ).
tcf(c_32731,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_26515,c_586,c_846,c_886,c_1287,c_2028,c_2440,c_2748,c_4438,c_6979,c_8664,c_19487,c_28104,c_30574,c_31198]) ).
tcf(c_32741,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_32731,c_26252]) ).
tcf(c_32868,plain,
( ( identity = sk_c9 )
| ( identity != multiply(sk_c4,sk_c10) )
| ( sk_c9 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_3687]) ).
tcf(c_32871,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_940]) ).
tcf(c_32873,plain,
( ( identity = sk_c10 )
| ( identity != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_32871]) ).
tcf(c_32892,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2290]) ).
tcf(c_32894,plain,
( ( sk_c8 = sk_c10 )
| ( sk_c8 != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_32892]) ).
tcf(c_32949,plain,
( ( inverse(sk_c1) = sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_26694,c_586,c_886,c_1180,c_1287,c_5222,c_16703,c_20022,c_25600,c_29467,c_32741]) ).
tcf(c_32953,plain,
( ( inverse(sk_c2) = sk_c10 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_27088,c_586,c_886,c_1287,c_5222,c_10108,c_16704,c_25600,c_31209,c_32741,c_32868]) ).
tcf(c_34035,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = inverse(X3) )
| ( inverse(X3) != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_1109]) ).
tcf(c_34037,plain,
( ( multiply(sk_c10,sk_c10) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_34035]) ).
tcf(c_34499,plain,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c10) = inverse(sk_c5) ) ),
inference(superposition,[status(thm)],[c_28132,c_28127]) ).
tcf(c_35500,plain,
! [X0: $i] :
( ( inverse(inverse(sk_c7)) = X0 )
| ( X0 != inverse(sk_c6) )
| ( inverse(inverse(sk_c7)) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_15330]) ).
tcf(c_35502,plain,
( ( inverse(inverse(sk_c7)) = sk_c10 )
| ( sk_c10 != inverse(sk_c6) )
| ( inverse(inverse(sk_c7)) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_35500]) ).
tcf(c_35570,plain,
inverse(sk_c1) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_9083,c_118,c_2767,c_3257,c_26007,c_28322,c_32949,c_35502]) ).
tcf(c_35867,plain,
( ( sk_c8 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_4255,c_1869]) ).
tcf(c_35870,plain,
( ( sk_c8 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c9,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_4255,c_1872]) ).
tcf(c_35871,plain,
( ( sk_c8 = multiply(sk_c10,sk_c3) )
| ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_4255,c_1873]) ).
tcf(c_35872,plain,
( ( sk_c8 = multiply(sk_c10,sk_c3) )
| ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_4255,c_1874]) ).
tcf(c_35903,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_4255,c_3738]) ).
tcf(c_35904,plain,
( ( sk_c8 = sk_c10 )
| ( sk_c10 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_35903]) ).
tcf(c_36622,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_24902]) ).
tcf(c_36624,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != sk_c9 )
| ( inverse(X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_24902]) ).
tcf(c_36626,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != inverse(sk_c5) )
| ( inverse(X0) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_3747]) ).
tcf(c_36630,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_36624]) ).
tcf(c_36632,plain,
( ( inverse(sk_c10) = sk_c9 )
| ( sk_c9 != inverse(sk_c5) )
| ( inverse(sk_c10) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_36626]) ).
tcf(c_36699,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != multiply(inverse(X0),X0) )
| ( sk_c9 != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_30561]) ).
tcf(c_36700,plain,
( ( sk_c9 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c9 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_36699]) ).
tcf(c_37528,plain,
inverse(sk_c1) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_27423,c_118,c_2767,c_3257,c_26007,c_28322,c_32949,c_35502]) ).
tcf(c_37553,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c9,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_2096,c_37528]) ).
tcf(c_37565,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_1431,c_37528]) ).
tcf(c_37568,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c9,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_1428,c_37528]) ).
tcf(c_37569,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_1427,c_37528]) ).
tcf(c_37593,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c9,X0)) = X0,
inference(superposition,[status(thm)],[c_37528,c_26377]) ).
tcf(c_37594,plain,
multiply(sk_c1,sk_c9) = identity,
inference(superposition,[status(thm)],[c_37528,c_26252]) ).
tcf(c_37595,plain,
inverse(sk_c9) = sk_c1,
inference(superposition,[status(thm)],[c_37528,c_26236]) ).
tcf(c_37680,plain,
inverse(sk_c2) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_28523,c_143,c_586,c_869,c_886,c_892,c_984,c_1244,c_4441,c_5091,c_5223,c_5535,c_10168,c_16704,c_32953,c_34037,c_34499,c_36630,c_36632]) ).
tcf(c_37682,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,inverse(sk_c3)) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_28153,c_37680]) ).
tcf(c_37685,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,inverse(sk_c3)) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_28150,c_37680]) ).
tcf(c_37686,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,inverse(sk_c3)) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_28149,c_37680]) ).
tcf(c_37706,plain,
( ( multiply(sk_c10,sk_c3) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_2282,c_37680]) ).
tcf(c_37719,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_2057,c_37680]) ).
tcf(c_37720,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_2054,c_37680]) ).
tcf(c_37723,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_1983,c_37680]) ).
tcf(c_37759,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c10,X0)) = X0,
inference(superposition,[status(thm)],[c_37680,c_26377]) ).
tcf(c_37760,plain,
multiply(sk_c2,sk_c10) = identity,
inference(superposition,[status(thm)],[c_37680,c_26252]) ).
tcf(c_37761,plain,
inverse(sk_c10) = sk_c2,
inference(superposition,[status(thm)],[c_37680,c_26236]) ).
tcf(c_37957,plain,
( ( sk_c9 = sk_c10 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_37719,c_128]) ).
tcf(c_38320,plain,
( ( sk_c9 = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_37720,c_127]) ).
tcf(c_38346,plain,
( ( sk_c3 = identity )
| ( sk_c8 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_27970,c_37595,c_37760,c_37761]) ).
tcf(c_38354,plain,
! [X0: $i] :
( ( sk_c8 = sk_c1 )
| ( multiply(X0,sk_c3) = X0 ) ),
inference(superposition,[status(thm)],[c_38346,c_2691]) ).
tcf(c_38358,plain,
( ( sk_c8 = sk_c1 )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_38354]) ).
tcf(c_38359,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( sk_c9 = identity ) ),
inference(global_subsumption_just,[status(thm)],[c_26368,c_586,c_1288,c_1287,c_2778,c_6974,c_19946,c_30575,c_30849,c_37706]) ).
tcf(c_38360,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(renaming,[status(thm)],[c_38359]) ).
tcf(c_38385,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_26557,c_586,c_846,c_1287,c_2028,c_2440,c_2752,c_4438,c_8664,c_19487,c_37594]) ).
tcf(c_38395,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(global_subsumption_just,[status(thm)],[c_26558,c_586,c_846,c_1287,c_2028,c_2440,c_2751,c_4438,c_8664,c_19487,c_37594]) ).
tcf(c_38518,plain,
( ( inverse(sk_c6) = sk_c10 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_26635,c_586,c_846,c_1287,c_2028,c_2440,c_4438,c_5221,c_8664,c_9470,c_24717,c_30575,c_37594,c_37957]) ).
tcf(c_38522,plain,
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_26647,c_586,c_846,c_1287,c_2028,c_2440,c_4438,c_5221,c_8664,c_9470,c_24717,c_30575,c_37594,c_38320]) ).
tcf(c_38620,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_26683,c_586,c_846,c_1287,c_2028,c_2440,c_4438,c_5221,c_8545,c_8664,c_9470,c_9612,c_19946,c_24717,c_30575,c_30849,c_37594]) ).
tcf(c_38722,plain,
( ( sk_c9 = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_37723,c_122]) ).
tcf(c_39030,plain,
( ( sk_c9 = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_37706,c_124]) ).
tcf(c_40060,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = identity )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_934]) ).
tcf(c_40061,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != identity )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_24902]) ).
tcf(c_40065,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != identity )
| ( inverse(sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_40061]) ).
tcf(c_40346,plain,
( ( multiply(identity,sk_c9) = multiply(sk_c10,sk_c8) )
| ( identity != sk_c10 )
| ( sk_c9 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_857]) ).
tcf(c_41045,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1041,c_37593]) ).
tcf(c_41110,plain,
( ( sk_c10 = sk_c3 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_41045,c_37719]) ).
tcf(c_41148,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( inverse(sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_41045,c_26252]) ).
tcf(c_41166,plain,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_41045,c_37686]) ).
tcf(c_42237,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1042,c_37593]) ).
tcf(c_42301,plain,
( ( sk_c10 = sk_c3 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_42237,c_37720]) ).
tcf(c_42340,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_42237,c_26252]) ).
tcf(c_42359,plain,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_42237,c_37685]) ).
tcf(c_42848,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c8 != multiply(sk_c10,sk_c3) )
| ( sk_c9 != multiply(sk_c10,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_19944]) ).
tcf(c_42933,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c8 != multiply(sk_c10,sk_c3) )
| ( sk_c9 != multiply(sk_c10,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_19945]) ).
tcf(c_43296,plain,
! [X0: $i] :
( ( sk_c8 = sk_c1 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1044,c_37593,c_37595]) ).
tcf(c_43354,plain,
( ( sk_c8 = sk_c1 )
| ( sk_c9 = identity )
| ( sk_c9 = sk_c8 ) ),
inference(superposition,[status(thm)],[c_43296,c_38360]) ).
tcf(c_43400,plain,
( ( sk_c8 = sk_c1 )
| ( sk_c10 = identity ) ),
inference(superposition,[status(thm)],[c_43296,c_2691]) ).
tcf(c_43401,plain,
( ( sk_c8 = sk_c1 )
| ( inverse(sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_43296,c_26252]) ).
tcf(c_43402,plain,
! [X0: $i] :
( ( sk_c8 = sk_c1 )
| ( multiply(inverse(sk_c10),X0) = X0 ) ),
inference(superposition,[status(thm)],[c_43296,c_26377]) ).
tcf(c_43431,plain,
( ( sk_c8 = sk_c1 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_43402]) ).
tcf(c_43637,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1045,c_37593]) ).
tcf(c_43696,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( sk_c9 != sk_c8 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_43637,c_579]) ).
tcf(c_43700,plain,
( ( sk_c10 = sk_c3 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_43637,c_37723]) ).
tcf(c_43742,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_43637,c_26252]) ).
tcf(c_43764,plain,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_43637,c_37682]) ).
tcf(c_44144,plain,
! [X0: $i] :
( ( inverse(inverse(sk_c9)) = inverse(X0) )
| ( inverse(sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_15332]) ).
tcf(c_44178,plain,
( ( sk_c8 = sk_c1 )
| ( sk_c9 = identity ) ),
inference(global_subsumption_just,[status(thm)],[c_43354,c_150,c_1287,c_2457,c_13146,c_30585,c_36700,c_43431]) ).
tcf(c_44186,plain,
( ( sk_c8 = sk_c1 )
| ( inverse(sk_c9) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_44178,c_25965]) ).
tcf(c_44187,plain,
! [X0: $i] :
( ( sk_c8 = sk_c1 )
| ( multiply(X0,sk_c9) = X0 ) ),
inference(superposition,[status(thm)],[c_44178,c_2691]) ).
tcf(c_44189,plain,
! [X0: $i] :
( ( sk_c8 = sk_c1 )
| ( multiply(sk_c9,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_44178,c_99]) ).
tcf(c_44191,plain,
( ( sk_c8 = sk_c1 )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_44187]) ).
tcf(c_44851,plain,
( ( sk_c8 = sk_c1 )
| ( sk_c10 = sk_c8 ) ),
inference(superposition,[status(thm)],[c_44189,c_102]) ).
tcf(c_44863,plain,
( ( sk_c8 = sk_c1 )
| ~ iPr_def_11
| ( sk_c9 != sk_c8 )
| ( inverse(sk_c9) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_44189,c_575]) ).
tcf(c_45017,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( sk_c8 != X0 )
| ( inverse(sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_24902]) ).
tcf(c_45018,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( sk_c8 != sk_c10 )
| ( inverse(sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_45017]) ).
tcf(c_45952,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c3,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1062,c_37759]) ).
tcf(c_45999,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( inverse(sk_c9) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_45952,c_28141]) ).
tcf(c_46324,plain,
! [X0: $i] :
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c3,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1063,c_37759]) ).
tcf(c_46370,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c9) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_46324,c_28142]) ).
tcf(c_46511,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_11229,c_586,c_844,c_886,c_892,c_1250,c_1287,c_2330,c_2331,c_2778,c_7855,c_30572,c_32873,c_35872,c_37553,c_38360,c_39030,c_40346,c_42933]) ).
tcf(c_46517,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_579,c_46511]) ).
tcf(c_47628,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( sk_c8 != sk_c9 )
| ( inverse(sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_45017]) ).
tcf(c_47727,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c3,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_1066,c_37759]) ).
tcf(c_47770,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c9) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_47727,c_28145]) ).
tcf(c_47990,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c9 )
| ( sk_c9 != inverse(X0) )
| ( inverse(sk_c9) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_36622]) ).
tcf(c_47991,plain,
( ( inverse(sk_c9) = sk_c9 )
| ( sk_c9 != inverse(sk_c10) )
| ( inverse(sk_c9) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_47990]) ).
tcf(c_47992,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c9) = X1 )
| ( X1 != inverse(X0) )
| ( inverse(sk_c9) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_36622]) ).
tcf(c_47993,plain,
( ( inverse(sk_c9) = sk_c10 )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(sk_c9) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_47992]) ).
tcf(c_49673,plain,
( ( sk_c8 = sk_c1 )
| ~ iPr_def_12
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_43296,c_26237]) ).
tcf(c_49678,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_12
| ( sk_c10 != sk_c3 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_47727,c_26237]) ).
tcf(c_49680,plain,
( ( inverse(sk_c7) = sk_c6 )
| ~ iPr_def_12
| ( sk_c10 != sk_c3 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_46324,c_26237]) ).
tcf(c_49681,plain,
( ( inverse(sk_c6) = sk_c10 )
| ~ iPr_def_12
| ( sk_c10 != sk_c3 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_45952,c_26237]) ).
tcf(c_49695,plain,
( ( sk_c8 = sk_c1 )
| ~ iPr_def_12
| ( inverse(sk_c10) != sk_c10 ) ),
inference(equality_resolution_simp,[status(thm)],[c_49673]) ).
tcf(c_49935,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_26712,c_586,c_844,c_886,c_892,c_1250,c_1287,c_2330,c_2331,c_2778,c_7855,c_30572,c_32873,c_35872,c_37553,c_38360,c_39030,c_40346,c_42933]) ).
tcf(c_49959,plain,
( ( sk_c9 = sk_c8 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_49935,c_43637]) ).
tcf(c_49960,plain,
( ( sk_c8 = sk_c1 )
| ( sk_c9 = sk_c8 ) ),
inference(superposition,[status(thm)],[c_49935,c_43296]) ).
tcf(c_51309,plain,
( ( inverse(inverse(sk_c9)) = inverse(sk_c1) )
| ( inverse(sk_c9) != sk_c1 ) ),
inference(instantiation,[status(thm)],[c_44144]) ).
tcf(c_52092,plain,
( ( inverse(sk_c1) = identity )
| ( identity != sk_c9 )
| ( inverse(sk_c1) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_40060]) ).
tcf(c_52335,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != identity )
| ( inverse(sk_c1) != identity ) ),
inference(instantiation,[status(thm)],[c_40061]) ).
tcf(c_52337,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( sk_c10 != identity )
| ( inverse(sk_c1) != identity ) ),
inference(instantiation,[status(thm)],[c_52335]) ).
tcf(c_52342,plain,
! [X0: $i] :
( ( inverse(identity) = X0 )
| ( X0 != identity )
| ( inverse(identity) != identity ) ),
inference(instantiation,[status(thm)],[c_40061]) ).
tcf(c_52343,plain,
( ( inverse(identity) = sk_c10 )
| ( sk_c10 != identity )
| ( inverse(identity) != identity ) ),
inference(instantiation,[status(thm)],[c_52342]) ).
tcf(c_54682,plain,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_6422,c_143,c_118,c_122,c_586,c_869,c_886,c_892,c_984,c_1244,c_2374,c_2767,c_2773,c_3257,c_3467,c_4441,c_5091,c_5220,c_5223,c_5535,c_8948,c_10168,c_16704,c_26007,c_28322,c_32731,c_32894,c_32949,c_32953,c_34037,c_34499,c_35502,c_35867,c_36630,c_36632,c_37565,c_38620,c_38722,c_40065,c_42848,c_43700,c_43764,c_43742,c_43696,c_45018,c_47770,c_47993,c_49678,c_49959]) ).
tcf(c_54900,plain,
inverse(sk_c7) = sk_c6,
inference(global_subsumption_just,[status(thm)],[c_6486,c_143,c_127,c_586,c_869,c_886,c_892,c_984,c_1244,c_1921,c_2371,c_2776,c_3209,c_3464,c_4441,c_5091,c_5223,c_5535,c_10168,c_16704,c_19919,c_30627,c_32953,c_34037,c_34499,c_35570,c_35870,c_36630,c_36632,c_37568,c_37595,c_38320,c_38395,c_38522,c_40065,c_42301,c_42359,c_42340,c_42848,c_46370,c_46517,c_47628,c_47991,c_49680,c_51309]) ).
tcf(c_54915,plain,
inverse(sk_c6) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_7501,c_143,c_118,c_128,c_586,c_579,c_844,c_869,c_886,c_892,c_984,c_1244,c_1250,c_1287,c_2330,c_2331,c_2370,c_2767,c_2778,c_2777,c_3257,c_3463,c_4441,c_5091,c_5220,c_5223,c_5535,c_7855,c_10168,c_16704,c_26007,c_28322,c_30572,c_30627,c_32873,c_32949,c_32953,c_34037,c_34499,c_35502,c_35872,c_35871,c_36630,c_36632,c_37569,c_37553,c_37957,c_38360,c_38385,c_38518,c_39030,c_40065,c_40346,c_41110,c_41166,c_41148,c_42848,c_42933,c_45999,c_47628,c_47991,c_49681]) ).
tcf(c_54921,plain,
sk_c10 = inverse(sk_c6),
inference(resolution,[status(thm)],[c_54915,c_1909]) ).
tcf(c_56064,plain,
! [X0: $i] :
( iPr_def_14
| ( multiply(sk_c10,sk_c3) != X0 )
| ( multiply(identity,X0) = sk_c9 )
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_22594,c_99,c_143,c_118,c_127,c_586,c_869,c_886,c_892,c_984,c_1244,c_1921,c_2371,c_2767,c_2776,c_3209,c_3257,c_3464,c_4441,c_5091,c_5223,c_5535,c_10168,c_14027,c_16704,c_19034,c_19919,c_19942,c_21126,c_24896,c_26007,c_28322,c_30627,c_32949,c_32953,c_34037,c_34499,c_35502,c_35870,c_36630,c_36632,c_37568,c_37595,c_38320,c_38395,c_38522,c_40065,c_42301,c_42359,c_42340,c_42848,c_46370,c_46517,c_47628,c_47991,c_49680,c_51309,c_54921]) ).
tcf(c_56065,plain,
! [X0: $i] :
( iPr_def_14
| iPr_def_10
| ( multiply(identity,X0) = sk_c9 )
| ( multiply(sk_c10,sk_c3) != X0 ) ),
inference(renaming,[status(thm)],[c_56064]) ).
tcf(c_56091,plain,
( iPr_def_14
| iPr_def_10
| ~ iPr_def_13
| ( inverse(identity) != sk_c10 )
| ( multiply(sk_c10,sk_c3) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_56065,c_577]) ).
tcf(c_56117,plain,
( ~ iPr_def_13
| ( multiply(sk_c10,sk_c3) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_56091,c_586,c_846,c_1287,c_2028,c_2440,c_4438,c_5221,c_8664,c_9470,c_9612,c_19946,c_24717,c_30575,c_30849,c_37594]) ).
tcf(c_56890,negated_conjecture,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_113,c_54682]) ).
tcf(c_56896,negated_conjecture,
inverse(sk_c1) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_114,c_118,c_2767,c_3257,c_26007,c_28322,c_32949,c_35502]) ).
tcf(c_56903,plain,
( ( sk_c8 = sk_c1 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_105,c_37595]) ).
tcf(c_56905,plain,
multiply(sk_c9,sk_c1) = identity,
inference(superposition,[status(thm)],[c_56896,c_100]) ).
tcf(c_56912,negated_conjecture,
inverse(sk_c7) = sk_c6,
inference(global_subsumption_just,[status(thm)],[c_109,c_54900]) ).
tcf(c_56918,plain,
multiply(sk_c10,sk_c2) = identity,
inference(superposition,[status(thm)],[c_37680,c_100]) ).
tcf(c_56919,plain,
multiply(sk_c1,sk_c9) = identity,
inference(superposition,[status(thm)],[c_37595,c_100]) ).
tcf(c_56920,plain,
multiply(sk_c2,sk_c10) = identity,
inference(superposition,[status(thm)],[c_37761,c_100]) ).
tcf(c_56921,negated_conjecture,
inverse(sk_c6) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_110,c_54915]) ).
tcf(c_56935,plain,
( ( sk_c8 = sk_c1 )
| ( sk_c10 = identity ) ),
inference(demodulation,[status(thm)],[c_56903,c_56919]) ).
tcf(c_56936,plain,
sk_c8 = sk_c1,
inference(global_subsumption_just,[status(thm)],[c_56935,c_118,c_586,c_579,c_844,c_869,c_886,c_892,c_1243,c_1250,c_1287,c_1921,c_2247,c_2330,c_2331,c_2376,c_2477,c_2741,c_2767,c_2778,c_3257,c_3468,c_3709,c_3732,c_7424,c_7855,c_19919,c_26007,c_28322,c_30572,c_31223,c_32873,c_32949,c_35502,c_35872,c_35904,c_37553,c_37595,c_38358,c_38360,c_39030,c_40065,c_40346,c_42933,c_43400,c_43401,c_44186,c_44191,c_44851,c_44863,c_47628,c_49695,c_49960,c_51309,c_52343,c_56117]) ).
tcf(c_56938,plain,
multiply(sk_c8,sk_c9) = identity,
inference(demodulation,[status(thm)],[c_56919,c_56936]) ).
tcf(c_56940,plain,
inverse(sk_c9) = sk_c8,
inference(demodulation,[status(thm)],[c_37595,c_56936]) ).
tcf(c_56941,plain,
inverse(sk_c8) = sk_c9,
inference(demodulation,[status(thm)],[c_56896,c_56936]) ).
tcf(c_56942,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_579,c_56940]) ).
tcf(c_56948,negated_conjecture,
multiply(sk_c10,sk_c8) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_106,c_586,c_844,c_886,c_892,c_1250,c_1287,c_2330,c_2331,c_2778,c_7855,c_30572,c_32873,c_35872,c_37553,c_38360,c_39030,c_40346,c_42933]) ).
tcf(c_56950,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_56942,c_56948]) ).
tcf(c_56956,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_111,c_56936,c_56938]) ).
tcf(c_56966,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c8,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_56948,c_101]) ).
tcf(c_56984,plain,
multiply(sk_c9,sk_c8) = identity,
inference(light_normalisation,[status(thm)],[c_56905,c_56936]) ).
tcf(c_56985,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_56984,c_101]) ).
tcf(c_56987,plain,
( ( sk_c3 = identity )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_130,c_56920]) ).
tcf(c_57001,plain,
( ( sk_c3 = identity )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(light_normalisation,[status(thm)],[c_138,c_56920]) ).
tcf(c_57082,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_14
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c10,sk_c9) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_121,c_578]) ).
tcf(c_57095,plain,
( ( multiply(sk_c10,sk_c3) = sk_c9 )
| ~ iPr_def_14
| ( multiply(sk_c10,sk_c9) != sk_c9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_57082,c_56890]) ).
tcf(c_57116,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_1439,c_2691]) ).
tcf(c_57120,plain,
inverse(sk_c10) = sk_c4,
inference(superposition,[status(thm)],[c_56890,c_57116]) ).
tcf(c_57122,plain,
inverse(sk_c6) = sk_c7,
inference(superposition,[status(thm)],[c_56912,c_57116]) ).
tcf(c_57123,plain,
inverse(sk_c10) = sk_c6,
inference(superposition,[status(thm)],[c_56921,c_57116]) ).
tcf(c_57127,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_57116,c_100]) ).
tcf(c_57128,plain,
sk_c4 = sk_c6,
inference(light_normalisation,[status(thm)],[c_57120,c_57123]) ).
tcf(c_57130,plain,
( ( sk_c3 = identity )
| ( multiply(sk_c6,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_56987,c_57128]) ).
tcf(c_57142,plain,
sk_c10 = sk_c7,
inference(demodulation,[status(thm)],[c_57122,c_56921]) ).
tcf(c_57144,plain,
( ( sk_c3 = identity )
| ( multiply(sk_c10,sk_c10) = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_57001,c_57142]) ).
tcf(c_57146,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c10,sk_c10) = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_56956,c_57142]) ).
tcf(c_57148,plain,
sk_c6 = sk_c2,
inference(demodulation,[status(thm)],[c_57123,c_37761]) ).
tcf(c_57172,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_57127,c_101]) ).
tcf(c_57197,plain,
multiply(sk_c9,identity) = multiply(sk_c8,sk_c2),
inference(superposition,[status(thm)],[c_56918,c_2133]) ).
tcf(c_57213,plain,
multiply(sk_c9,inverse(sk_c8)) = multiply(sk_c10,identity),
inference(superposition,[status(thm)],[c_57127,c_56966]) ).
tcf(c_57229,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c8,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_56985,c_99]) ).
tcf(c_57232,plain,
multiply(sk_c9,identity) = inverse(sk_c8),
inference(superposition,[status(thm)],[c_57127,c_57229]) ).
tcf(c_57236,plain,
multiply(sk_c8,sk_c2) = sk_c9,
inference(light_normalisation,[status(thm)],[c_57197,c_56941,c_57232]) ).
tcf(c_57238,plain,
multiply(sk_c9,sk_c9) = sk_c2,
inference(superposition,[status(thm)],[c_57236,c_57229]) ).
tcf(c_57254,plain,
multiply(sk_c10,identity) = sk_c2,
inference(light_normalisation,[status(thm)],[c_57213,c_56941,c_57238]) ).
tcf(c_57255,plain,
sk_c10 = sk_c2,
inference(demodulation,[status(thm)],[c_57254,c_2691]) ).
tcf(c_57261,plain,
sk_c10 = sk_c6,
inference(demodulation,[status(thm)],[c_57148,c_57255]) ).
tcf(c_57262,plain,
multiply(sk_c10,sk_c10) = identity,
inference(demodulation,[status(thm)],[c_56918,c_57255]) ).
tcf(c_57264,plain,
inverse(sk_c10) = sk_c10,
inference(demodulation,[status(thm)],[c_37761,c_57255]) ).
tcf(c_57278,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_57172,c_99]) ).
tcf(c_57287,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_57116,c_57278]) ).
tcf(c_57362,plain,
( ( sk_c3 = identity )
| ( sk_c9 = identity ) ),
inference(light_normalisation,[status(thm)],[c_57130,c_57261,c_57262]) ).
tcf(c_57368,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( multiply(X0,sk_c3) = X0 ) ),
inference(superposition,[status(thm)],[c_57362,c_2691]) ).
tcf(c_57373,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c10,sk_c3) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_57368]) ).
tcf(c_57374,plain,
multiply(sk_c10,sk_c10) = sk_c6,
inference(global_subsumption_just,[status(thm)],[c_57144,c_150,c_586,c_589,c_844,c_892,c_1250,c_1287,c_1921,c_1925,c_2376,c_2390,c_2457,c_2477,c_3209,c_4258,c_4709,c_5221,c_5535,c_8948,c_14537,c_14541,c_15333,c_15334,c_18794,c_19919,c_19927,c_19946,c_20209,c_30575,c_30572,c_30849,c_35570,c_37595,c_51309,c_52092,c_52337,c_56950,c_57095,c_57146,c_57264,c_57373]) ).
tcf(c_57376,plain,
multiply(sk_c10,sk_c10) = sk_c10,
inference(light_normalisation,[status(thm)],[c_57374,c_57261,c_57262]) ).
tcf(c_57377,plain,
multiply(inverse(sk_c10),sk_c10) = sk_c10,
inference(superposition,[status(thm)],[c_57376,c_57287]) ).
tcf(c_57442,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_57377,c_57373,c_57264,c_57095,c_56950,c_52337,c_52092,c_51309,c_37595,c_35570,c_30849,c_30572,c_30575,c_20209,c_19946,c_19927,c_19919,c_18794,c_15334,c_15333,c_14541,c_14537,c_8948,c_5535,c_5221,c_4258,c_3209,c_2530,c_2477,c_2457,c_2390,c_2376,c_1925,c_1921,c_1287,c_1250,c_892,c_844,c_589,c_586,c_150]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP325-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 14:29:19 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.44
% 0.13/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.44
% 0.13/0.44 % Detected problem language: tptp
% 0.13/0.45 % Proving...
% 31.60/8.45 % SZS status Started for theBenchmark.p
% 31.60/8.45 % SZS status Unsatisfiable for theBenchmark.p
% 31.60/8.45
% 31.60/8.45 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 31.60/8.45
% 31.60/8.45 % ------ iProver source info
% 31.60/8.45
% 31.60/8.45 % git: date: 2026-07-19 20:42:38 +0200
% 31.60/8.45 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 31.60/8.45 % git: non_committed_changes: false
% 31.60/8.45
% 31.60/8.45 % ------ Parsing...% successful
% 31.60/8.45
% 31.60/8.45
% 31.60/8.45 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 31.60/8.45
% 31.60/8.45 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 31.60/8.45
% 31.60/8.45 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 31.60/8.45
% 31.60/8.45 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 31.60/8.45 % ------ Proving...
% 31.60/8.45 % ------ Problem Properties
% 31.60/8.45
% 31.60/8.45 %
% 31.60/8.45 % clauses 55
% 31.60/8.45 % conjectures 52
% 31.60/8.45 % EPR 0
% 31.60/8.45 % Horn 9
% 31.60/8.45 % unary 4
% 31.60/8.45 % binary 45
% 31.60/8.45 % lits 116
% 31.60/8.45 % lits eq 106
% 31.60/8.45 % fd_pure 0
% 31.60/8.45 % fd_pseudo 0
% 31.60/8.45 % fd_cond 0
% 31.60/8.45 % fd_pseudo_cond 0
% 31.60/8.45 % AC symbols 0
% 31.60/8.45
% 31.60/8.45 % ------ Input Options Time Limit: Unbounded
% 31.60/8.45
% 31.60/8.45
% 31.60/8.45 % ------
% 31.60/8.45 % Current options:
% 31.60/8.45 % ------
% 31.60/8.45
% 31.60/8.45
% 31.60/8.45 %
% 31.60/8.45
% 31.60/8.45 % ------ Proving...
% 31.60/8.45 %
% 31.60/8.45
% 31.60/8.45 % SZS status Unsatisfiable for theBenchmark.p
% 31.60/8.45
% 31.60/8.45 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 31.60/8.47
% 31.60/8.47
%------------------------------------------------------------------------------