%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP220-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 : n003.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:31:50 PM UTC 2026
% Result : Unsatisfiable 54.26s 9.27s
% Output : CNFRefutation 54.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 39
% Syntax : Number of formulae : 435 ( 106 unt; 0 def)
% Number of atoms : 1013 ( 933 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 973 ( 395 ~; 578 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 292 ( 0 sgn 292 !; 0 ?; 236 :)
% 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,
( inverse(sk_c12) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,negated_conjecture,
( inverse(sk_c6) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c12 = inverse(sk_c6)
| inverse(sk_c1) = sk_c12 ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| inverse(sk_c1) = sk_c12 ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c12 = multiply(sk_c7,sk_c10)
| inverse(sk_c1) = sk_c12 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c10 = inverse(sk_c7)
| inverse(sk_c1) = sk_c12 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( multiply(sk_c10,sk_c11) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c12 = multiply(sk_c10,sk_c11)
| inverse(sk_c1) = sk_c12 ),
inference(reorient_equations,[],[f14]) ).
fof(f21,negated_conjecture,
( inverse(sk_c12) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f22,plain,
( inverse(sk_c12) = sk_c11
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( inverse(sk_c6) = sk_c12
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c12 = inverse(sk_c6)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f25]) ).
fof(f37,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f38,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c12) = sk_c11
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f40,plain,
( inverse(sk_c12) = sk_c11
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( inverse(sk_c6) = sk_c12
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f42,plain,
( sk_c12 = inverse(sk_c6)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c12
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c12 = multiply(sk_c7,sk_c10)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( sk_c10 = inverse(sk_c7)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f47]) ).
fof(f57,negated_conjecture,
( inverse(sk_c12) = sk_c11
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f58,plain,
( inverse(sk_c12) = sk_c11
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c6) = sk_c12
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f60,plain,
( sk_c12 = inverse(sk_c6)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f62,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c12
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c12 = multiply(sk_c7,sk_c10)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c10 = inverse(sk_c7)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f65]) ).
fof(f73,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f73]) ).
fof(f93,negated_conjecture,
( inverse(sk_c12) = sk_c11
| multiply(sk_c12,sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f94,plain,
( inverse(sk_c12) = sk_c11
| sk_c11 = multiply(sk_c12,sk_c5) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( inverse(sk_c6) = sk_c12
| multiply(sk_c12,sk_c5) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f96,plain,
( sk_c12 = inverse(sk_c6)
| sk_c11 = multiply(sk_c12,sk_c5) ),
inference(reorient_equations,[],[f95]) ).
fof(f111,negated_conjecture,
( inverse(sk_c12) = sk_c11
| multiply(sk_c4,sk_c12) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_55) ).
fof(f112,plain,
( inverse(sk_c12) = sk_c11
| sk_c5 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f111]) ).
fof(f113,negated_conjecture,
( inverse(sk_c6) = sk_c12
| multiply(sk_c4,sk_c12) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f114,plain,
( sk_c12 = inverse(sk_c6)
| sk_c5 = multiply(sk_c4,sk_c12) ),
inference(reorient_equations,[],[f113]) ).
fof(f129,negated_conjecture,
( inverse(sk_c12) = sk_c11
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_64) ).
fof(f130,plain,
( inverse(sk_c12) = sk_c11
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f129]) ).
fof(f131,negated_conjecture,
( inverse(sk_c6) = sk_c12
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_65) ).
fof(f132,plain,
( sk_c12 = inverse(sk_c6)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f131]) ).
fof(f133,negated_conjecture,
( multiply(sk_c6,sk_c11) = sk_c12
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_66) ).
fof(f134,plain,
( sk_c12 = multiply(sk_c6,sk_c11)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f133]) ).
fof(f135,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c12
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_67) ).
fof(f136,plain,
( sk_c12 = multiply(sk_c7,sk_c10)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f135]) ).
fof(f137,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_68) ).
fof(f138,plain,
( sk_c10 = inverse(sk_c7)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f137]) ).
fof(f145,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| inverse(sk_c4) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_72) ).
fof(f146,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c12 = inverse(sk_c4) ),
inference(reorient_equations,[],[f145]) ).
fof(f147,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( multiply(X8,X7) != X9
| inverse(X9) != X7
| inverse(X8) != X9
| multiply(X7,sk_c11) != sk_c12
| inverse(X6) != X7
| multiply(X6,X7) != sk_c12
| multiply(X5,sk_c11) != sk_c12
| inverse(X5) != sk_c12
| inverse(sk_c12) != sk_c11
| inverse(X4) != sk_c12
| multiply(X4,sk_c12) != X3
| multiply(sk_c12,X3) != sk_c11
| multiply(X2,sk_c12) != sk_c11
| inverse(X1) != X2
| multiply(X1,X2) != sk_c11
| multiply(X0,sk_c11) != sk_c12
| inverse(X0) != sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_73) ).
fof(f148,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( multiply(X8,X7) != X9
| inverse(X9) != X7
| inverse(X8) != X9
| sk_c12 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c12 != multiply(X6,X7)
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| inverse(sk_c12) != sk_c11
| sk_c12 != inverse(X4)
| multiply(X4,sk_c12) != X3
| sk_c11 != multiply(sk_c12,X3)
| sk_c11 != multiply(X2,sk_c12)
| inverse(X1) != X2
| multiply(X1,X2) != sk_c11
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12 ),
inference(reorient_equations,[],[f147]) ).
fof(f149,plain,
! [X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( multiply(X8,X7) != X9
| inverse(X9) != X7
| inverse(X8) != X9
| sk_c12 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c12 != multiply(X6,X7)
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| inverse(sk_c12) != sk_c11
| sk_c12 != inverse(X4)
| multiply(X4,sk_c12) != X3
| sk_c11 != multiply(sk_c12,X3)
| sk_c11 != multiply(inverse(X1),sk_c12)
| sk_c11 != multiply(X1,inverse(X1))
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12 ),
inference(equality_resolution,[],[f148]) ).
fof(f150,plain,
! [X0,X1,X8,X6,X9,X7,X4,X5] :
( multiply(X8,X7) != X9
| inverse(X9) != X7
| inverse(X8) != X9
| sk_c12 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c12 != multiply(X6,X7)
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| inverse(sk_c12) != sk_c11
| sk_c12 != inverse(X4)
| sk_c11 != multiply(sk_c12,multiply(X4,sk_c12))
| sk_c11 != multiply(inverse(X1),sk_c12)
| sk_c11 != multiply(X1,inverse(X1))
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12 ),
inference(equality_resolution,[],[f149]) ).
fof(f151,plain,
! [X0,X1,X8,X6,X9,X4,X5] :
( multiply(X8,inverse(X6)) != X9
| inverse(X6) != inverse(X9)
| inverse(X8) != X9
| sk_c12 != multiply(inverse(X6),sk_c11)
| sk_c12 != multiply(X6,inverse(X6))
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| inverse(sk_c12) != sk_c11
| sk_c12 != inverse(X4)
| sk_c11 != multiply(sk_c12,multiply(X4,sk_c12))
| sk_c11 != multiply(inverse(X1),sk_c12)
| sk_c11 != multiply(X1,inverse(X1))
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12 ),
inference(equality_resolution,[],[f150]) ).
fof(f152,plain,
! [X0,X1,X8,X6,X4,X5] :
( inverse(X8) != multiply(X8,inverse(X6))
| inverse(X6) != inverse(inverse(X8))
| sk_c12 != multiply(inverse(X6),sk_c11)
| sk_c12 != multiply(X6,inverse(X6))
| sk_c12 != multiply(X5,sk_c11)
| sk_c12 != inverse(X5)
| inverse(sk_c12) != sk_c11
| sk_c12 != inverse(X4)
| sk_c11 != multiply(sk_c12,multiply(X4,sk_c12))
| sk_c11 != multiply(inverse(X1),sk_c12)
| sk_c11 != multiply(X1,inverse(X1))
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12 ),
inference(equality_resolution,[],[f151]) ).
tcf(c_125,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_126,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c10,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_139,negated_conjecture,
( ( multiply(sk_c6,sk_c11) = sk_c12 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_145,negated_conjecture,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c2,sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_149,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(sk_c7,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c2,sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_155,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_156,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c6) = sk_c12 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_158,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c7,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_163,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_173,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c12,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_174,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c12,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_182,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c5 ) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_183,negated_conjecture,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = sk_c5 ) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_191,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_192,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( inverse(sk_c6) = sk_c12 ) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_193,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_194,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_195,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( inverse(sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_199,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_200,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(sk_c12) != sk_c11 )
| ( inverse(X4) != sk_c12 )
| ( inverse(X3) != sk_c12 )
| ( inverse(X2) != sk_c12 )
| ( multiply(X3,sk_c11) != sk_c12 )
| ( multiply(X2,sk_c11) != sk_c12 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X5),sk_c12) != sk_c11 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X5,inverse(X5)) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) )
| ( multiply(sk_c12,multiply(X4,sk_c12)) != sk_c11 ) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_202,plain,
multiply(inverse(sk_c12),sk_c12) = identity,
inference(instantiation,[status(thm)],[c_126]) ).
tcf(c_841,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c11) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_200]) ).
tcf(c_842,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c12) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_200]) ).
tcf(c_843,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_200]) ).
tcf(c_844,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c12 )
| ( multiply(sk_c12,multiply(X0,sk_c12)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_200]) ).
tcf(c_845,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c12) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_200]) ).
tcf(c_846,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_847,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_848,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_849,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_850,plain,
( ( inverse(sk_c12) = inverse(sk_c12) )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_848]) ).
tcf(c_852,plain,
sk_c12 = sk_c12,
inference(instantiation,[status(thm)],[c_846]) ).
tcf(c_1208,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c12 )
| ( sk_c12 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1209,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c12) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1211,plain,
( ( inverse(sk_c12) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1208]) ).
tcf(c_1217,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_846]) ).
tcf(c_1220,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1221,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c12 )
| ( sk_c12 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1208]) ).
tcf(c_1222,plain,
! [X0: $i] :
( ( sk_c12 = sk_c11 )
| ( sk_c11 != X0 )
| ( sk_c12 != X0 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1230,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1232,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = inverse(X0) )
| ( sk_c12 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1235,plain,
! [X0: $i] :
( ( inverse(sk_c12) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1220]) ).
tcf(c_1243,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1220]) ).
tcf(c_1249,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_1307,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1230]) ).
tcf(c_1308,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_846]) ).
tcf(c_1309,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != sk_c11 )
| ( sk_c12 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1307]) ).
tcf(c_1312,plain,
( ( sk_c12 = inverse(sk_c6) )
| ( sk_c12 != sk_c12 )
| ( inverse(sk_c6) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1232]) ).
tcf(c_1316,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = inverse(X0) )
| ( sk_c12 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1232]) ).
tcf(c_1319,plain,
( ~ iPr_def_10
| ( inverse(sk_c1) != sk_c12 )
| ( multiply(sk_c1,sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_841]) ).
tcf(c_1336,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c12,sk_c4) = identity ) ),
inference(superposition,[status(thm)],[c_191,c_126]) ).
tcf(c_1445,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(sk_c6,multiply(sk_c11,X0)) = multiply(sk_c12,X0) ) ),
inference(superposition,[status(thm)],[c_139,c_127]) ).
tcf(c_1484,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_126,c_127]) ).
tcf(c_1554,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c12 )
| ( sk_c12 != inverse(sk_c6) )
| ( inverse(X0) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1221]) ).
tcf(c_1555,plain,
( ( inverse(sk_c12) = sk_c12 )
| ( sk_c12 != inverse(sk_c6) )
| ( inverse(sk_c12) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1554]) ).
tcf(c_1697,plain,
( ( sk_c11 = inverse(sk_c12) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1307]) ).
tcf(c_1818,plain,
! [X0: $i] :
( ( sk_c12 = inverse(X0) )
| ( sk_c12 != inverse(sk_c6) )
| ( inverse(X0) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1316]) ).
tcf(c_1819,plain,
( ( sk_c12 = inverse(sk_c12) )
| ( sk_c12 != inverse(sk_c6) )
| ( inverse(sk_c12) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1818]) ).
tcf(c_2073,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != inverse(sk_c12) )
| ( sk_c12 != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1222]) ).
tcf(c_2079,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c11 )
| ( sk_c11 != inverse(sk_c12) )
| ( inverse(X0) != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1243]) ).
tcf(c_2080,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( sk_c11 != inverse(sk_c12) )
| ( inverse(sk_c12) != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2079]) ).
tcf(c_2230,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c1) = sk_c12 ) ),
inference(resolution,[status(thm)],[c_845,c_128]) ).
tcf(c_2598,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_847,c_126]) ).
tcf(c_2599,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c12 )
| ( sk_c12 != identity ) ),
inference(instantiation,[status(thm)],[c_2598]) ).
tcf(c_2602,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_847,c_846]) ).
tcf(c_3499,plain,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ~ iPr_def_10
| ( inverse(sk_c6) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_139,c_841]) ).
tcf(c_3502,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_10
| ( inverse(sk_c6) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_130,c_841]) ).
tcf(c_3511,plain,
( ( inverse(sk_c6) = sk_c12 )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_138,c_841]) ).
tcf(c_3933,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c12,multiply(sk_c4,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_1336,c_127]) ).
tcf(c_3937,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c12,multiply(sk_c4,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_3933,c_125]) ).
tcf(c_3947,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c12,sk_c5) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_182,c_3937]) ).
tcf(c_4080,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1484,c_125]) ).
tcf(c_4101,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_193,c_4080]) ).
tcf(c_4102,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_157,c_4080]) ).
tcf(c_4103,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_130,c_4080]) ).
tcf(c_4181,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_4080,c_4080]) ).
tcf(c_4242,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_849,c_847]) ).
tcf(c_4273,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_10
| ( inverse(sk_c6) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_841,c_130]) ).
tcf(c_4424,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c1) = sk_c12 ) ),
inference(global_subsumption_just,[status(thm)],[c_2230,c_129,c_128,c_845,c_1319,c_3511,c_3502,c_3499]) ).
tcf(c_4473,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_4273,c_129,c_1319,c_3511,c_3502,c_3499]) ).
tcf(c_4475,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_4473,c_1319,c_3511,c_3499,c_4473]) ).
tcf(c_4543,plain,
( ( sk_c3 = inverse(sk_c2) )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2602,c_155]) ).
tcf(c_4576,plain,
! [X0: $i] : X0 = multiply(identity,X0),
inference(resolution,[status(thm)],[c_2602,c_125]) ).
tcf(c_4578,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_2602,c_126]) ).
tcf(c_4590,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c3 )
| ( sk_c3 != inverse(sk_c2) )
| ( inverse(X0) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1243]) ).
tcf(c_4955,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_4181,c_126]) ).
tcf(c_5294,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_192,c_4101]) ).
tcf(c_5303,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_156,c_4102]) ).
tcf(c_5322,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_129,c_4103]) ).
tcf(c_5451,plain,
( ( sk_c12 = sk_c11 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_3947,c_173]) ).
tcf(c_5511,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c12 = sk_c11 ) ),
inference(superposition,[status(thm)],[c_5451,c_845]) ).
tcf(c_5536,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( sk_c12 = sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_5511,c_129,c_1319,c_3511,c_3502,c_3499,c_5511]) ).
tcf(c_5544,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(sk_c12),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_5294,c_4080]) ).
tcf(c_5553,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(inverse(sk_c12),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_5303,c_4080]) ).
tcf(c_5578,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c12),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_5322,c_4080]) ).
tcf(c_5628,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_195,c_4955]) ).
tcf(c_5629,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c7,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_159,c_4955]) ).
tcf(c_5630,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_132,c_4955]) ).
tcf(c_5641,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_4955,c_127]) ).
tcf(c_5938,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_5628,c_194]) ).
tcf(c_5967,plain,
! [X0: $i,X1: $i] :
( ( X0 = multiply(inverse(X1),X1) )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_2598,c_2602]) ).
tcf(c_5968,plain,
( ( sk_c12 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c12 != identity ) ),
inference(instantiation,[status(thm)],[c_5967]) ).
tcf(c_5987,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_5629,c_158]) ).
tcf(c_6113,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_5630,c_131]) ).
tcf(c_6162,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_1209]) ).
tcf(c_6168,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c12) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_6169,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c12) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c12) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_1209]) ).
tcf(c_6171,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c11 )
| ( sk_c11 != multiply(sk_c12,sk_c12) )
| ( multiply(inverse(sk_c12),sk_c12) != multiply(sk_c12,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_6169]) ).
tcf(c_6226,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c3 = inverse(sk_c2) ) ),
inference(resolution,[status(thm)],[c_4543,c_845]) ).
tcf(c_6297,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( sk_c4 != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_1230]) ).
tcf(c_7079,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = multiply(inverse(X1),identity),
inference(superposition,[status(thm)],[c_5641,c_4080]) ).
tcf(c_9122,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = multiply(inverse(identity),identity),
inference(superposition,[status(thm)],[c_125,c_7079]) ).
tcf(c_9138,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c12) != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_845,c_129,c_845,c_1319,c_3511,c_3502,c_3499]) ).
tcf(c_9485,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_9122,c_126]) ).
tcf(c_9493,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c7,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_195,c_9485]) ).
tcf(c_9500,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = identity ) ),
inference(superposition,[status(thm)],[c_155,c_9485]) ).
tcf(c_9503,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_9485,c_127]) ).
tcf(c_9504,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_9485,c_125]) ).
tcf(c_9522,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_9503,c_125]) ).
tcf(c_9525,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_126,c_9522]) ).
tcf(c_9526,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_9485,c_9522]) ).
tcf(c_9554,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_9526,c_9525]) ).
tcf(c_9605,plain,
( ~ iPr_def_13
| ( sk_c12 != sk_c11 )
| ( inverse(inverse(sk_c12)) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_9522,c_844]) ).
tcf(c_9618,plain,
( ~ iPr_def_13
| ( inverse(identity) != sk_c12 )
| ( multiply(sk_c12,sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_125,c_844]) ).
tcf(c_9621,plain,
( ~ iPr_def_13
| ( sk_c12 != sk_c11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9605,c_9554]) ).
tcf(c_9623,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( multiply(inverse(X0),sk_c12) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_842,c_9485]) ).
tcf(c_9630,plain,
( ~ iPr_def_11
| ( sk_c11 != identity ) ),
inference(superposition,[status(thm)],[c_126,c_9623]) ).
tcf(c_9647,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_843,c_9554]) ).
tcf(c_9648,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( sk_c12 != identity )
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_9647,c_9485]) ).
tcf(c_9659,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( sk_c12 != identity )
| ( inverse(X0) != identity )
| ( inverse(X0) != inverse(identity) )
| ( multiply(inverse(X0),sk_c11) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_125,c_9648]) ).
tcf(c_9680,plain,
( ~ iPr_def_12
| ( sk_c12 != identity )
| ( inverse(sk_c12) != identity )
| ( inverse(sk_c12) != inverse(identity) )
| ( multiply(inverse(sk_c12),sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_9659]) ).
tcf(c_9750,plain,
( ~ iPr_def_13
| ( sk_c12 != identity )
| ( multiply(sk_c12,sk_c12) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_9618,c_9504]) ).
tcf(c_9786,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1484,c_125]) ).
tcf(c_9809,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_157,c_9786]) ).
tcf(c_9810,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_130,c_9786]) ).
tcf(c_9859,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(inverse(sk_c4),sk_c5) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_182,c_9786]) ).
tcf(c_9956,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_9493,c_194]) ).
tcf(c_9968,plain,
( ( sk_c12 = identity )
| ( multiply(sk_c12,sk_c4) = identity ) ),
inference(superposition,[status(thm)],[c_9956,c_126]) ).
tcf(c_10037,plain,
( ( sk_c12 = identity )
| ( multiply(inverse(sk_c12),identity) = sk_c4 ) ),
inference(superposition,[status(thm)],[c_9968,c_9786]) ).
tcf(c_10095,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c12) = sk_c4 ) ),
inference(demodulation,[status(thm)],[c_10037,c_9525]) ).
tcf(c_10159,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_9500,c_146]) ).
tcf(c_10165,plain,
( ( sk_c11 = identity )
| ( sk_c11 = sk_c4 )
| ( sk_c12 = identity ) ),
inference(superposition,[status(thm)],[c_10095,c_10159]) ).
tcf(c_10312,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_156,c_9809]) ).
tcf(c_10509,plain,
( ( inverse(sk_c2) = sk_c3 )
| ~ iPr_def_13
| ( sk_c12 != identity ) ),
inference(superposition,[status(thm)],[c_10312,c_9750]) ).
tcf(c_10515,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_129,c_9810]) ).
tcf(c_10527,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_13
| ( sk_c12 != identity ) ),
inference(superposition,[status(thm)],[c_10515,c_9750]) ).
tcf(c_10569,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_10570,plain,
( ( sk_c12 = identity )
| ( identity != sk_c12 )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_10569]) ).
tcf(c_10573,plain,
( ( sk_c11 = identity )
| ( identity != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1307]) ).
tcf(c_10696,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = identity )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1220]) ).
tcf(c_10698,plain,
( ( inverse(sk_c12) = identity )
| ( identity != sk_c12 )
| ( inverse(sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_10696]) ).
tcf(c_13310,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c12) )
| ( sk_c11 != sk_c11 )
| ( multiply(inverse(X0),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1307]) ).
tcf(c_13312,plain,
! [X0: $i] :
( ( inverse(sk_c12) = multiply(inverse(X0),sk_c12) )
| ( inverse(sk_c12) != sk_c11 )
| ( multiply(inverse(X0),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1235]) ).
tcf(c_13313,plain,
( ( inverse(sk_c12) = multiply(inverse(sk_c12),sk_c12) )
| ( inverse(sk_c12) != sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_13312]) ).
tcf(c_13314,plain,
( ( sk_c11 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c11 != sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_13310]) ).
tcf(c_13425,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(X0),sk_c12) = multiply(X2,X3) )
| ( multiply(X2,X3) != X1 )
| ( multiply(inverse(X0),sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_6168]) ).
tcf(c_13426,plain,
( ( multiply(inverse(sk_c12),sk_c12) = multiply(sk_c12,sk_c12) )
| ( multiply(sk_c12,sk_c12) != sk_c12 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_13425]) ).
tcf(c_13441,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c12,sk_c5) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_191,c_9859]) ).
tcf(c_13458,plain,
( ( sk_c12 = sk_c11 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_13441,c_173]) ).
tcf(c_13472,plain,
( ( sk_c11 = sk_c4 )
| ( sk_c12 = identity )
| ( sk_c12 = sk_c11 ) ),
inference(superposition,[status(thm)],[c_13458,c_10095]) ).
tcf(c_14997,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( sk_c3 != inverse(sk_c2) )
| ( inverse(sk_c2) != inverse(sk_c2) ) ),
inference(instantiation,[status(thm)],[c_4590]) ).
tcf(c_14998,plain,
inverse(sk_c2) = inverse(sk_c2),
inference(instantiation,[status(thm)],[c_1217]) ).
tcf(c_18326,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c12) != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_845,c_129,c_845,c_1319,c_3511,c_3502,c_3499]) ).
tcf(c_18562,plain,
( ( inverse(sk_c6) = sk_c12 )
| ~ iPr_def_13
| ( inverse(sk_c4) != sk_c12 )
| ( multiply(sk_c12,sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_183,c_844]) ).
tcf(c_18564,plain,
( ~ iPr_def_13
| ( inverse(identity) != sk_c12 )
| ( multiply(sk_c12,sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_125,c_844]) ).
tcf(c_18699,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1484,c_125]) ).
tcf(c_18747,plain,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(inverse(sk_c1),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_138,c_18699]) ).
tcf(c_18754,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(inverse(sk_c2),sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_146,c_18699]) ).
tcf(c_18770,plain,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(inverse(sk_c4),sk_c5) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_183,c_18699]) ).
tcf(c_18772,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_125,c_18699]) ).
tcf(c_18773,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_126,c_18699]) ).
tcf(c_18774,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_127,c_18699]) ).
tcf(c_18796,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_18699,c_18699]) ).
tcf(c_18829,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_18773,c_18796]) ).
tcf(c_18849,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_18796,c_126]) ).
tcf(c_18872,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_18829,c_18772]) ).
tcf(c_18873,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_18829,c_18796]) ).
tcf(c_18874,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_18873,c_18829]) ).
tcf(c_18881,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_843,c_18874]) ).
tcf(c_18882,plain,
( ~ iPr_def_12
| ( inverse(sk_c12) != sk_c12 )
| ( multiply(sk_c12,inverse(sk_c12)) != sk_c12 )
| ( multiply(sk_c12,inverse(sk_c12)) != inverse(sk_c12) )
| ( multiply(inverse(sk_c12),sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_18881]) ).
tcf(c_18897,plain,
( ( inverse(sk_c12) = sk_c4 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_191,c_18874]) ).
tcf(c_18899,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),X0) != sk_c11 )
| ( multiply(inverse(inverse(X0)),sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_18874,c_842]) ).
tcf(c_18901,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(X0,sk_c12) != sk_c11 )
| ( multiply(inverse(X0),X0) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_18899,c_18874]) ).
tcf(c_18902,plain,
( ~ iPr_def_11
| ( multiply(sk_c12,sk_c12) != sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_18901]) ).
tcf(c_18980,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_191,c_18849]) ).
tcf(c_18985,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_18849,c_127]) ).
tcf(c_19008,plain,
( ~ iPr_def_13
| ( sk_c12 != identity )
| ( multiply(sk_c12,sk_c12) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_18564,c_18872]) ).
tcf(c_19053,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c12) = sk_c11 )
| ( sk_c11 != sk_c4 ) ),
inference(superposition,[status(thm)],[c_18897,c_18326]) ).
tcf(c_19453,plain,
( ( sk_c5 = identity )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_18980,c_182]) ).
tcf(c_19468,plain,
( ( sk_c5 = identity )
| ( multiply(sk_c11,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_19453,c_126]) ).
tcf(c_19981,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_155,c_18754]) ).
tcf(c_19988,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(inverse(sk_c3),sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_19981,c_18699]) ).
tcf(c_20940,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X0)),identity) = X1,
inference(superposition,[status(thm)],[c_126,c_18774]) ).
tcf(c_21036,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = inverse(X1),
inference(superposition,[status(thm)],[c_18849,c_18774]) ).
tcf(c_21170,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_18985,c_18774]) ).
tcf(c_21208,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_21170,c_21036]) ).
tcf(c_22779,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = X2 )
| ( X2 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_22781,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,X1) )
| ( X0 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_849]) ).
tcf(c_23472,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = X1 )
| ( X2 != identity )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_4576,c_4242]) ).
tcf(c_23473,plain,
( ( multiply(sk_c12,sk_c12) = sk_c12 )
| ( sk_c12 != identity )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_23472]) ).
tcf(c_23673,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_4578,c_847]) ).
tcf(c_23674,plain,
( ( identity = sk_c12 )
| ( sk_c12 != multiply(inverse(sk_c12),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_23673]) ).
tcf(c_24012,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c12),sk_c12) = X0 )
| ( X0 != sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_6168]) ).
tcf(c_24013,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_24012]) ).
tcf(c_24078,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c11,inverse(sk_c12)) = inverse(sk_c1) ) ),
inference(superposition,[status(thm)],[c_137,c_21208]) ).
tcf(c_24113,plain,
! [X0: $i] : multiply(X0,inverse(identity)) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_126,c_21208]) ).
tcf(c_24455,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c12) )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_24456,plain,
( ( sk_c12 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c12 != sk_c12 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_24455]) ).
tcf(c_24577,plain,
! [X0: $i] :
( ( identity = sk_c11 )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_1249]) ).
tcf(c_24578,plain,
( ( identity = sk_c11 )
| ( identity != sk_c12 )
| ( sk_c11 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_24577]) ).
tcf(c_24718,plain,
! [X0: $i] :
( ( sk_c11 = inverse(sk_c12) )
| ( sk_c11 != X0 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_1230]) ).
tcf(c_24719,plain,
( ( sk_c11 = inverse(sk_c12) )
| ( sk_c11 != sk_c12 )
| ( inverse(sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_24718]) ).
tcf(c_28006,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( sk_c11 != sk_c4 ) ),
inference(global_subsumption_just,[status(thm)],[c_19053,c_129,c_845,c_1319,c_3511,c_3502,c_3499,c_19053]) ).
tcf(c_30542,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = X1,
inference(demodulation,[status(thm)],[c_20940,c_18829]) ).
tcf(c_30567,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(multiply(inverse(sk_c12),sk_c10)) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_133,c_30542]) ).
tcf(c_30573,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( inverse(multiply(inverse(sk_c8),sk_c9)) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_199,c_30542]) ).
tcf(c_30574,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(multiply(inverse(sk_c8),sk_c9)) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_163,c_30542]) ).
tcf(c_33321,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c12 )
| ( sk_c12 != multiply(inverse(X1),sk_c12) )
| ( inverse(X0) != multiply(inverse(X1),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1208]) ).
tcf(c_33325,plain,
( ( inverse(sk_c12) = sk_c12 )
| ( sk_c12 != multiply(inverse(sk_c12),sk_c12) )
| ( inverse(sk_c12) != multiply(inverse(sk_c12),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_33321]) ).
tcf(c_33513,plain,
! [X0: $i,X1: $i] :
( ( sk_c4 = multiply(inverse(X0),sk_c12) )
| ( sk_c4 != X1 )
| ( multiply(inverse(X0),sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_24455]) ).
tcf(c_33515,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( sk_c4 != multiply(inverse(X0),sk_c12) )
| ( sk_c11 != multiply(inverse(X0),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_6297]) ).
tcf(c_33516,plain,
( ( sk_c4 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c4 != sk_c12 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_33513]) ).
tcf(c_33517,plain,
( ( sk_c11 = sk_c4 )
| ( sk_c4 != multiply(inverse(sk_c12),sk_c12) )
| ( sk_c11 != multiply(inverse(sk_c12),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_33515]) ).
tcf(c_33758,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_848]) ).
tcf(c_33759,plain,
( ( inverse(sk_c12) = inverse(identity) )
| ( sk_c12 != identity ) ),
inference(instantiation,[status(thm)],[c_33758]) ).
tcf(c_34510,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c12,X0) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c12,X0) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1307]) ).
tcf(c_34513,plain,
( ( sk_c11 = multiply(sk_c12,sk_c12) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c12,sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_34510]) ).
tcf(c_34548,plain,
inverse(sk_c1) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_30567,c_128,c_852,c_1308,c_2599,c_4424,c_5322,c_5578,c_5968,c_6113,c_6171,c_9680,c_10527,c_10698,c_13313,c_13426,c_18902,c_23473,c_23674,c_33325,c_33759,c_34513]) ).
tcf(c_34552,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c11,inverse(sk_c12)) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_24078,c_34548]) ).
tcf(c_34566,plain,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_18747,c_34548]) ).
tcf(c_34658,plain,
inverse(sk_c4) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_30573,c_191,c_852,c_1308,c_2599,c_5294,c_5544,c_5938,c_5968,c_6171,c_9138,c_9680,c_10698,c_13313,c_13426,c_18902,c_19008,c_23473,c_23674,c_33325,c_33759,c_34513]) ).
tcf(c_34678,plain,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c12,sk_c5) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_18770,c_34658]) ).
tcf(c_34713,plain,
( ( inverse(sk_c6) = sk_c12 )
| ~ iPr_def_13
| ( multiply(sk_c12,sk_c5) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_18562,c_34658]) ).
tcf(c_34720,plain,
inverse(sk_c12) = sk_c4,
inference(superposition,[status(thm)],[c_34658,c_18874]) ).
tcf(c_34724,plain,
inverse(sk_c2) = sk_c3,
inference(global_subsumption_just,[status(thm)],[c_30574,c_155,c_852,c_1308,c_2599,c_4475,c_5303,c_5553,c_5968,c_5987,c_6171,c_6226,c_9680,c_10509,c_10698,c_13313,c_13426,c_14997,c_14998,c_18902,c_23473,c_23674,c_33325,c_33759,c_34513]) ).
tcf(c_34775,plain,
multiply(sk_c2,sk_c3) = identity,
inference(superposition,[status(thm)],[c_34724,c_18849]) ).
tcf(c_34776,plain,
inverse(sk_c3) = sk_c2,
inference(superposition,[status(thm)],[c_34724,c_18874]) ).
tcf(c_35024,plain,
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(inverse(sk_c12),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_34566,c_18699]) ).
tcf(c_35204,plain,
( ( sk_c12 = sk_c11 )
| ( inverse(sk_c6) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_34678,c_174]) ).
tcf(c_35602,plain,
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c11,sk_c4) = sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_34552,c_34720]) ).
tcf(c_35670,plain,
( ( sk_c11 = identity )
| ( sk_c11 = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_19988,c_34720,c_34775,c_34776]) ).
tcf(c_35678,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c11,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_35670,c_125]) ).
tcf(c_35747,plain,
( ( sk_c5 = identity )
| ( sk_c11 = sk_c4 )
| ( sk_c12 = identity ) ),
inference(superposition,[status(thm)],[c_35678,c_19468]) ).
tcf(c_35751,plain,
( ( sk_c11 = sk_c4 )
| ( sk_c12 = sk_c4 ) ),
inference(superposition,[status(thm)],[c_35678,c_35602]) ).
tcf(c_36044,plain,
( ( sk_c12 = identity )
| ( sk_c11 = sk_c4 ) ),
inference(global_subsumption_just,[status(thm)],[c_35747,c_202,c_852,c_6162,c_10165,c_10570,c_13472,c_23674,c_24013,c_24456]) ).
tcf(c_36045,plain,
( ( sk_c11 = sk_c4 )
| ( sk_c12 = identity ) ),
inference(renaming,[status(thm)],[c_36044]) ).
tcf(c_36050,plain,
( ( sk_c11 = sk_c4 )
| ( inverse(sk_c12) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_36045,c_18872]) ).
tcf(c_36053,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c12,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_36045,c_125]) ).
tcf(c_36105,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( multiply(inverse(sk_c12),X0) = X0 ) ),
inference(superposition,[status(thm)],[c_36053,c_18699]) ).
tcf(c_36135,plain,
( ( sk_c11 = sk_c4 )
| ( multiply(inverse(sk_c12),sk_c12) = sk_c12 ) ),
inference(instantiation,[status(thm)],[c_36105]) ).
tcf(c_40141,plain,
! [X0: $i] :
( ( multiply(sk_c12,inverse(sk_c12)) = multiply(X0,sk_c11) )
| ( sk_c12 != X0 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_22781]) ).
tcf(c_40148,plain,
( ( multiply(sk_c12,inverse(sk_c12)) = multiply(sk_c12,sk_c11) )
| ( sk_c12 != sk_c12 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_40141]) ).
tcf(c_40493,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != identity )
| ( sk_c12 != identity ) ),
inference(instantiation,[status(thm)],[c_1222]) ).
tcf(c_40511,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(inverse(X1),sk_c12) )
| ( X0 != multiply(inverse(X1),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1230]) ).
tcf(c_40512,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != multiply(inverse(sk_c12),sk_c12) )
| ( sk_c12 != multiply(inverse(sk_c12),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_40511]) ).
tcf(c_40515,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_845,c_129,c_850,c_852,c_845,c_1309,c_1308,c_1319,c_2080,c_3511,c_3502,c_3499,c_5536,c_24719,c_28006,c_36050]) ).
tcf(c_40541,plain,
multiply(sk_c4,sk_c12) = identity,
inference(superposition,[status(thm)],[c_34720,c_126]) ).
tcf(c_40544,plain,
inverse(inverse(identity)) = inverse(identity),
inference(superposition,[status(thm)],[c_24113,c_125]) ).
tcf(c_40545,plain,
inverse(inverse(inverse(inverse(identity)))) = identity,
inference(superposition,[status(thm)],[c_24113,c_126]) ).
tcf(c_40546,plain,
inverse(identity) = identity,
inference(light_normalisation,[status(thm)],[c_40545,c_40544]) ).
tcf(c_40549,plain,
multiply(sk_c12,sk_c4) = identity,
inference(superposition,[status(thm)],[c_34658,c_126]) ).
tcf(c_40565,plain,
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c12,sk_c5) = sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_173,c_34720]) ).
tcf(c_40578,plain,
( ( sk_c5 = identity )
| ( sk_c11 = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_182,c_40541,c_34720]) ).
tcf(c_40584,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c5,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_40578,c_125]) ).
tcf(c_40587,plain,
multiply(sk_c12,sk_c1) = identity,
inference(superposition,[status(thm)],[c_34548,c_126]) ).
tcf(c_40588,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(X0,identity),
inference(demodulation,[status(thm)],[c_24113,c_40546]) ).
tcf(c_40647,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c12,multiply(sk_c5,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_40565,c_127]) ).
tcf(c_40648,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c12,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_40541,c_127]) ).
tcf(c_40748,plain,
! [X0: $i] : multiply(sk_c12,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_40549,c_127]) ).
tcf(c_40750,plain,
! [X0: $i] : multiply(sk_c12,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_40748,c_125]) ).
tcf(c_40769,plain,
( ( sk_c11 = sk_c4 )
| ~ iPr_def_13
| ( inverse(sk_c5) != sk_c12 )
| ( multiply(sk_c11,sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_40647,c_844]) ).
tcf(c_40770,plain,
( ~ iPr_def_13
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c4) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_40750,c_844]) ).
tcf(c_40781,plain,
( ~ iPr_def_13
| ( sk_c12 != sk_c11 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_40770,c_34658]) ).
tcf(c_40832,plain,
! [X0: $i] : multiply(sk_c12,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_40587,c_127]) ).
tcf(c_40835,plain,
multiply(sk_c1,identity) = inverse(sk_c12),
inference(superposition,[status(thm)],[c_34548,c_40588]) ).
tcf(c_40847,plain,
! [X0: $i] : multiply(multiply(X0,identity),inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_40588,c_126]) ).
tcf(c_40854,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_40847,c_125,c_127]) ).
tcf(c_40866,plain,
multiply(sk_c2,sk_c3) = identity,
inference(superposition,[status(thm)],[c_34724,c_40854]) ).
tcf(c_40870,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_40854,c_127]) ).
tcf(c_40883,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c7,sk_c10) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_149,c_40866]) ).
tcf(c_40884,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c6,sk_c11) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_148,c_40866]) ).
tcf(c_40887,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c7) = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_150,c_40866]) ).
tcf(c_40888,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c6) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_147,c_40866]) ).
tcf(c_40918,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c7,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_40887,c_40854]) ).
tcf(c_40945,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c5,multiply(X0,X1)) = multiply(X0,X1) ) ),
inference(superposition,[status(thm)],[c_40584,c_127]) ).
tcf(c_40975,plain,
! [X0: $i] : multiply(sk_c12,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_40832,c_125]) ).
tcf(c_41024,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c12,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_40648,c_125]) ).
tcf(c_41036,plain,
multiply(sk_c4,identity) = sk_c1,
inference(superposition,[status(thm)],[c_40587,c_41024]) ).
tcf(c_41198,plain,
( ( sk_c11 = identity )
| ( sk_c12 = identity ) ),
inference(superposition,[status(thm)],[c_40918,c_40883]) ).
tcf(c_41312,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1484,c_125]) ).
tcf(c_41315,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( multiply(sk_c12,multiply(sk_c6,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_40888,c_41312]) ).
tcf(c_41317,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( multiply(sk_c10,multiply(sk_c7,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_40887,c_41312]) ).
tcf(c_41333,plain,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_139,c_41312]) ).
tcf(c_41371,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_127,c_41312]) ).
tcf(c_41385,plain,
multiply(inverse(sk_c12),identity) = sk_c4,
inference(superposition,[status(thm)],[c_40549,c_41312]) ).
tcf(c_41505,plain,
sk_c1 = sk_c4,
inference(light_normalisation,[status(thm)],[c_41385,c_34720,c_41036]) ).
tcf(c_41524,plain,
inverse(sk_c12) = sk_c1,
inference(demodulation,[status(thm)],[c_34720,c_41505]) ).
tcf(c_41552,plain,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(inverse(inverse(sk_c6)),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_41333,c_41312]) ).
tcf(c_41588,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_40870,c_125]) ).
tcf(c_41595,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_126,c_41588]) ).
tcf(c_41622,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(inverse(multiply(X0,X1)),X2))) = X2,
inference(superposition,[status(thm)],[c_41588,c_127]) ).
tcf(c_42549,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = inverse(X1),
inference(superposition,[status(thm)],[c_40854,c_41371]) ).
tcf(c_42825,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_42549,c_41595]) ).
tcf(c_42893,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(X1)) = inverse(multiply(X1,X0)),
inference(superposition,[status(thm)],[c_41312,c_42825]) ).
tcf(c_43482,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,inverse(multiply(X2,multiply(X0,X1))))) = inverse(X2),
inference(superposition,[status(thm)],[c_42893,c_41622]) ).
tcf(c_43508,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c12 )
| ( multiply(sk_c1,multiply(sk_c11,multiply(inverse(sk_c12),X0))) = X0 ) ),
inference(superposition,[status(thm)],[c_138,c_41622]) ).
tcf(c_43902,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_40884,c_41315]) ).
tcf(c_44129,plain,
sk_c11 = identity,
inference(global_subsumption_just,[status(thm)],[c_41317,c_852,c_1308,c_2599,c_5968,c_6171,c_10573,c_13314,c_13426,c_23473,c_23674,c_24578,c_34513,c_40512,c_41198,c_43902]) ).
tcf(c_44155,plain,
! [X0: $i] : multiply(X0,sk_c11) = X0,
inference(demodulation,[status(thm)],[c_41595,c_44129]) ).
tcf(c_44181,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = sk_c11,
inference(demodulation,[status(thm)],[c_40854,c_44129]) ).
tcf(c_44184,plain,
( ~ iPr_def_11
| ( sk_c11 != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_9630,c_44129]) ).
tcf(c_44195,plain,
! [X0: $i] : multiply(sk_c11,X0) = X0,
inference(demodulation,[status(thm)],[c_125,c_44129]) ).
tcf(c_44196,plain,
~ iPr_def_11,
inference(equality_resolution_simp,[status(thm)],[c_44184]) ).
tcf(c_44223,plain,
( iPr_def_13
| iPr_def_12 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40515,c_44196]) ).
tcf(c_44225,plain,
multiply(sk_c12,sk_c11) = sk_c12,
inference(instantiation,[status(thm)],[c_44155]) ).
tcf(c_44227,plain,
multiply(sk_c12,inverse(sk_c12)) = sk_c11,
inference(instantiation,[status(thm)],[c_44181]) ).
tcf(c_45128,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(sk_c12,X0) = multiply(sk_c6,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1445,c_44195]) ).
tcf(c_45362,plain,
! [X0: $i,X1: $i] :
( ( sk_c1 = sk_c11 )
| ( multiply(sk_c5,multiply(X0,X1)) = multiply(X0,X1) ) ),
inference(light_normalisation,[status(thm)],[c_40945,c_41505]) ).
tcf(c_45379,plain,
( ( sk_c1 = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_145,c_45362]) ).
tcf(c_51903,plain,
sk_c4 = sk_c4,
inference(instantiation,[status(thm)],[c_846]) ).
tcf(c_51922,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c12,inverse(sk_c12)) = X1 )
| ( X1 != multiply(X0,sk_c11) )
| ( multiply(sk_c12,inverse(sk_c12)) != multiply(X0,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_22779]) ).
tcf(c_51924,plain,
( ( multiply(sk_c12,inverse(sk_c12)) = sk_c12 )
| ( sk_c12 != multiply(sk_c12,sk_c11) )
| ( multiply(sk_c12,inverse(sk_c12)) != multiply(sk_c12,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_51922]) ).
tcf(c_52438,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_52499,plain,
! [X0: $i] :
( ( inverse(sk_c12) = X0 )
| ( X0 != sk_c4 )
| ( inverse(sk_c12) != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_52438]) ).
tcf(c_52640,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_52750,plain,
! [X0: $i] :
( ( sk_c4 = sk_c12 )
| ( sk_c4 != X0 )
| ( sk_c12 != X0 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_53707,plain,
( ( sk_c4 = sk_c12 )
| ( sk_c4 != sk_c4 )
| ( sk_c12 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_52750]) ).
tcf(c_54584,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c11) )
| ( X2 != X1 )
| ( multiply(X0,sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_847]) ).
tcf(c_54585,plain,
( ( sk_c12 = multiply(sk_c12,sk_c11) )
| ( sk_c12 != sk_c12 )
| ( multiply(sk_c12,sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_54584]) ).
tcf(c_55505,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c12) )
| ( X0 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_52640]) ).
tcf(c_56532,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( sk_c11 != sk_c4 )
| ( inverse(sk_c12) != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_52499]) ).
tcf(c_60157,plain,
( ( multiply(sk_c12,inverse(sk_c12)) = inverse(sk_c12) )
| ( inverse(sk_c12) != sk_c11 )
| ( multiply(sk_c12,inverse(sk_c12)) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_55505]) ).
tcf(c_74415,plain,
inverse(sk_c6) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_43508,c_202,c_129,c_174,c_852,c_845,c_1211,c_1308,c_1319,c_2599,c_3511,c_3502,c_3499,c_5968,c_6162,c_6171,c_9630,c_10573,c_13314,c_13426,c_18882,c_23473,c_23674,c_24578,c_33516,c_33517,c_34513,c_34713,c_34720,c_35024,c_35204,c_35751,c_36135,c_40148,c_40512,c_41198,c_43902,c_44225,c_44227,c_51903,c_51924,c_53707,c_54585,c_56532,c_60157]) ).
tcf(c_74421,plain,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(inverse(sk_c12),sk_c11) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_41552,c_74415]) ).
tcf(c_74674,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(X0,multiply(X1,inverse(multiply(sk_c12,multiply(X0,X1))))) = inverse(sk_c6) ) ),
inference(superposition,[status(thm)],[c_45128,c_43482]) ).
tcf(c_74857,plain,
( ( inverse(sk_c12) = inverse(sk_c6) )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_74674,c_43482]) ).
tcf(c_75346,plain,
multiply(sk_c1,sk_c11) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_45379,c_202,c_129,c_852,c_845,c_1308,c_1312,c_1319,c_1555,c_1697,c_1819,c_2073,c_2599,c_3511,c_3502,c_3499,c_5968,c_6162,c_6171,c_9621,c_9630,c_10573,c_13314,c_13426,c_18882,c_23473,c_23674,c_24578,c_33516,c_33517,c_34513,c_34720,c_35751,c_36135,c_40148,c_40512,c_41198,c_43902,c_44225,c_44227,c_51903,c_51924,c_53707,c_54585,c_56532,c_60157,c_74415,c_74421,c_74857]) ).
tcf(c_75362,plain,
multiply(sk_c12,sk_c12) = sk_c11,
inference(superposition,[status(thm)],[c_75346,c_40975]) ).
tcf(c_75630,plain,
sk_c11 = sk_c4,
inference(global_subsumption_just,[status(thm)],[c_40769,c_202,c_852,c_1308,c_2599,c_5968,c_6162,c_6171,c_10573,c_13314,c_13426,c_23473,c_23674,c_24578,c_33516,c_33517,c_34513,c_35751,c_36135,c_40512,c_41198,c_43902,c_51903,c_53707]) ).
tcf(c_75632,plain,
sk_c1 = sk_c11,
inference(demodulation,[status(thm)],[c_41505,c_75630]) ).
tcf(c_76143,plain,
multiply(sk_c11,sk_c11) = sk_c12,
inference(demodulation,[status(thm)],[c_75346,c_75632]) ).
tcf(c_76144,plain,
inverse(sk_c12) = sk_c11,
inference(demodulation,[status(thm)],[c_41524,c_75632]) ).
tcf(c_76172,plain,
multiply(inverse(sk_c12),sk_c11) = sk_c12,
inference(superposition,[status(thm)],[c_75362,c_41312]) ).
tcf(c_76220,plain,
sk_c12 = sk_c11,
inference(light_normalisation,[status(thm)],[c_40835,c_44129,c_75632,c_76143,c_76144]) ).
tcf(c_76230,plain,
sk_c12 = identity,
inference(demodulation,[status(thm)],[c_44129,c_76220]) ).
tcf(c_76231,plain,
( ~ iPr_def_13
| ( sk_c12 != sk_c12 ) ),
inference(demodulation,[status(thm)],[c_40781,c_76220]) ).
tcf(c_76233,plain,
~ iPr_def_13,
inference(equality_resolution_simp,[status(thm)],[c_76231]) ).
tcf(c_76237,plain,
iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_44223,c_76233]) ).
tcf(c_76273,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_76230,c_76237,c_76172,c_75630,c_60157,c_56532,c_54585,c_51924,c_44227,c_44225,c_44129,c_40493,c_40148,c_34720,c_18882,c_1211,c_852]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP220-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 14:12:19 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 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.11/0.42
% 0.11/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.42
% 0.11/0.42 % Detected problem language: tptp
% 0.11/0.43 % Proving...
% 54.26/9.27 % SZS status Started for theBenchmark.p
% 54.26/9.27 % SZS status Unsatisfiable for theBenchmark.p
% 54.26/9.27
% 54.26/9.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 54.26/9.27
% 54.26/9.27 % ------ iProver source info
% 54.26/9.27
% 54.26/9.27 % git: date: 2026-07-19 20:42:38 +0200
% 54.26/9.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 54.26/9.27 % git: non_committed_changes: false
% 54.26/9.27
% 54.26/9.27 % ------ Parsing...% successful
% 54.26/9.27
% 54.26/9.27
% 54.26/9.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 54.26/9.27
% 54.26/9.27 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 54.26/9.27
% 54.26/9.27 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 54.26/9.27
% 54.26/9.27 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 54.26/9.27 % ------ Proving...
% 54.26/9.27 % ------ Problem Properties
% 54.26/9.27
% 54.26/9.27 %
% 54.26/9.27 % clauses 80
% 54.26/9.27 % conjectures 77
% 54.26/9.27 % EPR 0
% 54.26/9.27 % Horn 7
% 54.26/9.27 % unary 3
% 54.26/9.27 % binary 72
% 54.26/9.27 % lits 166
% 54.26/9.27 % lits eq 158
% 54.26/9.27 % fd_pure 0
% 54.26/9.27 % fd_pseudo 0
% 54.26/9.27 % fd_cond 0
% 54.26/9.27 % fd_pseudo_cond 0
% 54.26/9.27 % AC symbols 0
% 54.26/9.27
% 54.26/9.27 % ------ Input Options Time Limit: Unbounded
% 54.26/9.27
% 54.26/9.27
% 54.26/9.27 % ------
% 54.26/9.27 % Current options:
% 54.26/9.27 % ------
% 54.26/9.27
% 54.26/9.27
% 54.26/9.27 %
% 54.26/9.27
% 54.26/9.27 % ------ Proving...
% 54.26/9.27 %
% 54.26/9.27
% 54.26/9.27 % SZS status Unsatisfiable for theBenchmark.p
% 54.26/9.27
% 54.26/9.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 54.26/9.28
% 54.26/9.28
%------------------------------------------------------------------------------