%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP371-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 : n002.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:33:25 PM UTC 2026
% Result : Unsatisfiable 31.94s 14.58s
% Output : CNFRefutation 31.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 33
% Syntax : Number of formulae : 466 ( 99 unt; 0 def)
% Number of atoms : 1139 (1049 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 1200 ( 527 ~; 673 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 8 ( 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 : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 355 ( 0 sgn 355 !; 0 ?; 315 :)
% 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_c3,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c10 = inverse(sk_c4)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c8 = inverse(sk_c5)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f14]) ).
fof(f18,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,negated_conjecture,
( inverse(sk_c6) = sk_c8
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f20,plain,
( sk_c8 = inverse(sk_c6)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f19]) ).
fof(f23,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f25]) ).
fof(f29,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f33]) ).
fof(f43,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c11 = inverse(sk_c3)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c10 = inverse(sk_c4)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c8 = inverse(sk_c5)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f53]) ).
fof(f57,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f58,plain,
( inverse(sk_c7) = sk_c6
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c6) = sk_c8
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f60,plain,
( sk_c8 = inverse(sk_c6)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f59]) ).
fof(f85,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f89]) ).
fof(f95,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f96,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f95]) ).
fof(f103,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| multiply(X5,sk_c10) != sk_c11
| inverse(X4) != X5
| multiply(X4,X5) != sk_c11
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c10
| multiply(sk_c9,sk_c10) != sk_c11
| multiply(X1,sk_c10) != sk_c11
| inverse(X0) != X1
| multiply(X0,X1) != sk_c11
| inverse(sk_c11) != sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c11 != multiply(X1,sk_c10)
| inverse(X0) != X1
| multiply(X0,X1) != sk_c11
| inverse(sk_c11) != sk_c10 ),
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
! [X2,X3,X0,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c11 != multiply(inverse(X0),sk_c10)
| sk_c11 != multiply(X0,inverse(X0))
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f104]) ).
fof(f106,plain,
! [X2,X3,X0,X6,X7,X4] :
( multiply(X6,inverse(X4)) != X7
| inverse(X4) != inverse(X7)
| inverse(X6) != X7
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c11 != multiply(inverse(X0),sk_c10)
| sk_c11 != multiply(X0,inverse(X0))
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f105]) ).
fof(f107,plain,
! [X2,X3,X0,X6,X4] :
( inverse(X6) != multiply(X6,inverse(X4))
| inverse(X4) != inverse(inverse(X6))
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c11 != multiply(inverse(X0),sk_c10)
| sk_c11 != multiply(X0,inverse(X0))
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f106]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c6) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c1,sk_c2) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c1,sk_c2) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_152,negated_conjecture,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c11) != sk_c10 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( multiply(sk_c9,sk_c10) != sk_c11 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X2),sk_c10) != sk_c11 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X2,inverse(X2)) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_617,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_156]) ).
tcf(c_618,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_156]) ).
tcf(c_619,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_156]) ).
tcf(c_620,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_156]) ).
tcf(c_621,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_156]) ).
tcf(c_622,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_623,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_624,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_626,plain,
( ( inverse(sk_c11) = inverse(sk_c11) )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_628,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_632,plain,
( ~ iPr_def_13
| ( inverse(inverse(sk_c11)) != inverse(sk_c11) )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c11 )
| ( multiply(sk_c11,inverse(sk_c11)) != inverse(sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_620]) ).
tcf(c_897,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_901,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c11) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_902,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(X0) )
| ( inverse(sk_c11) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_897]) ).
tcf(c_903,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_904,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c11) )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_907,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_914,plain,
! [X0: $i] :
( ( inverse(sk_c11) = X0 )
| ( X0 != inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_901]) ).
tcf(c_917,plain,
( ( sk_c10 = inverse(sk_c11) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_904]) ).
tcf(c_918,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_919,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_920,plain,
( ( inverse(sk_c11) = multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c11) != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_914]) ).
tcf(c_921,plain,
multiply(identity,inverse(sk_c11)) = inverse(sk_c11),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_923,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c11) )
| ( X1 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_924,plain,
( ( sk_c11 = inverse(sk_c11) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_933,plain,
! [X0: $i] : multiply(identity,inverse(X0)) = inverse(X0),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_935,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_959,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_919]) ).
tcf(c_960,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_959]) ).
tcf(c_966,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c11) )
| ( X1 != inverse(X0) )
| ( inverse(sk_c11) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_967,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c11) )
| ( X0 != multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_923]) ).
tcf(c_980,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c3) )
| ( X0 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_935]) ).
tcf(c_981,plain,
( ( sk_c11 = inverse(sk_c3) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_980]) ).
tcf(c_982,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( X0 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_935]) ).
tcf(c_991,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_1032,plain,
( ( sk_c10 = inverse(sk_c4) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_1033,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(sk_c11) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_902]) ).
tcf(c_1118,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,multiply(sk_c11,X0)) = multiply(sk_c10,X0) ) ),
inference(superposition,[status(thm)],[c_106,c_105]) ).
tcf(c_1145,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_1204,plain,
multiply(identity,multiply(identity,inverse(sk_c11))) = multiply(identity,inverse(sk_c11)),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1216,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_966]) ).
tcf(c_1229,plain,
( ( multiply(identity,sk_c10) = inverse(sk_c4) )
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_982]) ).
tcf(c_1230,plain,
multiply(identity,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1232,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_1261,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(identity,inverse(X0)) )
| ( X2 != X1 )
| ( multiply(identity,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_1263,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(identity,inverse(X2)) )
| ( X1 != inverse(X2) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_1279,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_919]) ).
tcf(c_1280,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_907]) ).
tcf(c_1281,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != inverse(sk_c11) )
| ( sk_c11 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_1293,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c11) )
| ( X0 != sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_935]) ).
tcf(c_1296,plain,
! [X0: $i] :
( ( inverse(sk_c11) = X0 )
| ( X0 != sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_901]) ).
tcf(c_1298,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1296]) ).
tcf(c_1308,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_1359,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_991]) ).
tcf(c_1360,plain,
! [X0: $i] :
( ( inverse(sk_c4) = X0 )
| ( X0 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_991]) ).
tcf(c_1371,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_991]) ).
tcf(c_1488,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c10,sk_c4) = identity ) ),
inference(superposition,[status(thm)],[c_129,c_104]) ).
tcf(c_1489,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c4) = identity ) ),
inference(superposition,[status(thm)],[c_109,c_104]) ).
tcf(c_1504,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1145,c_103]) ).
tcf(c_1516,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_1504]) ).
tcf(c_1519,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_1504,c_1504]) ).
tcf(c_1536,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_1541,plain,
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( sk_c11 != inverse(sk_c3) )
| ( multiply(sk_c9,sk_c10) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1308]) ).
tcf(c_1543,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c3) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_991]) ).
tcf(c_1851,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_623,c_104]) ).
tcf(c_1855,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_623,c_622]) ).
tcf(c_1856,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_623,c_624]) ).
tcf(c_1906,plain,
( ( inverse(sk_c11) = inverse(sk_c4) )
| ( sk_c11 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_903]) ).
tcf(c_1946,plain,
( ( multiply(identity,sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(sk_c4) )
| ( multiply(identity,sk_c10) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_966]) ).
tcf(c_1955,plain,
( ( multiply(identity,sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1293]) ).
tcf(c_1956,plain,
( ( inverse(sk_c11) = multiply(identity,sk_c10) )
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1296]) ).
tcf(c_1958,plain,
( ( sk_c10 = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_959]) ).
tcf(c_2125,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1232]) ).
tcf(c_2126,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != inverse(sk_c11) )
| ( sk_c11 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2125]) ).
tcf(c_2223,plain,
( ( multiply(identity,multiply(identity,inverse(sk_c11))) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) )
| ( multiply(identity,multiply(identity,inverse(sk_c11))) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_967]) ).
tcf(c_2283,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_2399,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_105,c_1504]) ).
tcf(c_2429,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,inverse(X0)) )
| ( X1 != inverse(X0) )
| ( multiply(identity,inverse(X0)) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1261]) ).
tcf(c_2463,plain,
( ( sk_c10 = multiply(identity,inverse(sk_c11)) )
| ( sk_c10 != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_2507,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1371]) ).
tcf(c_2593,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c4) )
| ( X0 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_2596,plain,
multiply(identity,inverse(sk_c4)) = inverse(sk_c4),
inference(instantiation,[status(thm)],[c_933]) ).
tcf(c_2686,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = inverse(X1) )
| ( inverse(X1) != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_1536]) ).
tcf(c_2693,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_1536]) ).
tcf(c_2746,plain,
( ( inverse(sk_c11) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_106,c_617]) ).
tcf(c_2747,plain,
( ~ iPr_def_10
| ( sk_c11 != sk_c10 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_103,c_617]) ).
tcf(c_2748,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_104,c_617]) ).
tcf(c_2806,plain,
( ( sk_c10 = inverse(sk_c4) )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1855,c_109]) ).
tcf(c_2819,plain,
( ( sk_c11 = multiply(sk_c1,sk_c2) )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_1855,c_117]) ).
tcf(c_2824,plain,
( ( sk_c11 = multiply(sk_c1,sk_c2) )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_1855,c_116]) ).
tcf(c_2853,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_1855,c_104]) ).
tcf(c_2903,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_1519,c_104]) ).
tcf(c_3211,plain,
( ( inverse(sk_c1) = sk_c2 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_128,c_618]) ).
tcf(c_3360,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( X0 != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1232]) ).
tcf(c_3394,plain,
( ( inverse(sk_c3) = inverse(sk_c11) )
| ( inverse(sk_c3) != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1359]) ).
tcf(c_3415,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_149,c_621]) ).
tcf(c_3446,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_127,c_2903]) ).
tcf(c_3448,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_129,c_2903]) ).
tcf(c_3449,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_109,c_2903]) ).
tcf(c_3450,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_131,c_2903]) ).
tcf(c_3451,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_111,c_2903]) ).
tcf(c_3457,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_2903,c_103]) ).
tcf(c_3618,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(X0),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_619,c_2903]) ).
tcf(c_3625,plain,
( ~ iPr_def_12
| ( sk_c11 != identity ) ),
inference(superposition,[status(thm)],[c_104,c_3618]) ).
tcf(c_3650,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_620,c_2903]) ).
tcf(c_3664,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(X0) != identity )
| ( inverse(inverse(X0)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_2903,c_3650]) ).
tcf(c_3677,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(sk_c11) != identity )
| ( inverse(inverse(sk_c11)) != inverse(sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3664]) ).
tcf(c_3757,plain,
( ( inverse(sk_c4) = inverse(sk_c4) )
| ( sk_c4 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_2593]) ).
tcf(c_3758,plain,
sk_c4 = sk_c4,
inference(instantiation,[status(thm)],[c_622]) ).
tcf(c_3861,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_3446,c_126]) ).
tcf(c_3871,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_3861,c_2903]) ).
tcf(c_4103,plain,
( ( inverse(sk_c11) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_617,c_106]) ).
tcf(c_4179,plain,
( ( sk_c10 = multiply(identity,multiply(identity,inverse(sk_c11))) )
| ( sk_c10 != inverse(sk_c11) )
| ( multiply(identity,multiply(identity,inverse(sk_c11))) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_4272,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_621,c_149]) ).
tcf(c_4334,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_4421,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_3448,c_128]) ).
tcf(c_4523,plain,
( ( sk_c10 = inverse(sk_c4) )
| ( sk_c10 = inverse(sk_c11) ) ),
inference(resolution,[status(thm)],[c_2806,c_1855]) ).
tcf(c_4537,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_3449,c_108]) ).
tcf(c_4578,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c10,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_4537,c_104]) ).
tcf(c_4638,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_3450,c_130]) ).
tcf(c_4785,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_3451,c_110]) ).
tcf(c_4795,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c10,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_4785,c_104]) ).
tcf(c_4944,plain,
( ( sk_c10 = multiply(identity,inverse(sk_c4)) )
| ( sk_c10 != inverse(sk_c4) )
| ( multiply(identity,inverse(sk_c4)) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2429]) ).
tcf(c_5687,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1145,c_103]) ).
tcf(c_6324,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,inverse(X0)) )
| ( multiply(sk_c9,sk_c10) != multiply(identity,inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_2693]) ).
tcf(c_6696,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = inverse(sk_c3) )
| ( inverse(sk_c3) != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_2686]) ).
tcf(c_7142,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,sk_c10) )
| ( X1 != X0 )
| ( multiply(identity,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_7191,plain,
! [X0: $i] :
( ( inverse(sk_c3) = multiply(identity,sk_c10) )
| ( inverse(sk_c3) != X0 )
| ( multiply(identity,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_1543]) ).
tcf(c_7240,plain,
( ( sk_c11 = multiply(sk_c1,sk_c2) )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_2824,c_617]) ).
tcf(c_7708,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,identity)),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_103,c_2399]) ).
tcf(c_8572,plain,
! [X0: $i] :
( ( multiply(X0,sk_c10) = multiply(identity,inverse(sk_c4)) )
| ( sk_c10 != inverse(sk_c4) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1263]) ).
tcf(c_9175,plain,
( ( inverse(sk_c11) = sk_c10 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_4103,c_107,c_2746]) ).
tcf(c_9192,plain,
( ( sk_c10 = inverse(sk_c11) )
| ~ iPr_def_10 ),
inference(resolution,[status(thm)],[c_9175,c_1855]) ).
tcf(c_9630,plain,
( ( sk_c11 = multiply(sk_c1,sk_c2) )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_7240,c_2819,c_7240]) ).
tcf(c_9764,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_1536]) ).
tcf(c_9896,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_4272,c_109,c_3415]) ).
tcf(c_9931,plain,
! [X0: $i] :
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_9896,c_623]) ).
tcf(c_10464,plain,
( ( inverse(sk_c4) = inverse(sk_c11) )
| ( inverse(sk_c4) != inverse(sk_c4) )
| ( inverse(sk_c11) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1216]) ).
tcf(c_10525,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2507]) ).
tcf(c_10850,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( X2 != X1 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_1856,c_624]) ).
tcf(c_11795,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(X0),identity)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_5687,c_7708]) ).
tcf(c_12278,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_4334]) ).
tcf(c_12279,plain,
( ( identity = sk_c11 )
| ( identity != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_12278]) ).
tcf(c_13200,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_104,c_618]) ).
tcf(c_13347,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1145,c_103]) ).
tcf(c_13416,plain,
! [X0: $i] : multiply(inverse(inverse(inverse(X0))),X0) = identity,
inference(superposition,[status(thm)],[c_1516,c_13347]) ).
tcf(c_14226,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X0)),identity) = X1,
inference(superposition,[status(thm)],[c_104,c_2399]) ).
tcf(c_14286,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,identity)),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_103,c_2399]) ).
tcf(c_14287,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_104,c_2399]) ).
tcf(c_14376,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(inverse(inverse(X1))))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_13416,c_2399]) ).
tcf(c_14392,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_14376,c_14287]) ).
tcf(c_14469,plain,
( ~ iPr_def_11
| ( sk_c9 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_13200,c_14392]) ).
tcf(c_14471,plain,
inverse(inverse(sk_c11)) = sk_c11,
inference(instantiation,[status(thm)],[c_14392]) ).
tcf(c_14653,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(X0),identity)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_14286]) ).
tcf(c_15548,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_14653,c_11795]) ).
tcf(c_15590,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = X1,
inference(demodulation,[status(thm)],[c_14226,c_15548]) ).
tcf(c_15711,plain,
! [X0: $i] : inverse(multiply(inverse(X0),X0)) = identity,
inference(superposition,[status(thm)],[c_15548,c_15590]) ).
tcf(c_15987,plain,
! [X0: $i] :
( ( multiply(identity,sk_c10) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(identity,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_16273,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_16665,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c4) )
| ( sk_c10 != inverse(X0) )
| ( inverse(sk_c4) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1280]) ).
tcf(c_16666,plain,
( ( sk_c10 = inverse(sk_c4) )
| ( sk_c10 != inverse(sk_c11) )
| ( inverse(sk_c4) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_16665]) ).
tcf(c_17869,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_2853,c_623]) ).
tcf(c_17870,plain,
( ( identity = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_17869]) ).
tcf(c_18149,plain,
( ( inverse(sk_c3) = multiply(identity,sk_c10) )
| ( inverse(sk_c3) != inverse(sk_c11) )
| ( multiply(identity,sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_7191]) ).
tcf(c_18271,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ~ iPr_def_10
| ( X0 != multiply(sk_c1,sk_c2) ) ),
inference(resolution,[status(thm)],[c_9630,c_623]) ).
tcf(c_18776,plain,
( ( multiply(sk_c9,sk_c10) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_9764]) ).
tcf(c_20745,plain,
( ( sk_c10 = inverse(sk_c11) )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_4523,c_1855]) ).
tcf(c_25331,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c10) )
| ( X0 != inverse(sk_c11) )
| ( multiply(identity,sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_7142]) ).
tcf(c_25332,plain,
( ( sk_c11 = multiply(identity,sk_c10) )
| ( sk_c11 != inverse(sk_c11) )
| ( multiply(identity,sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_25331]) ).
tcf(c_25754,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_16273]) ).
tcf(c_25755,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,X2) )
| ( sk_c10 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_25756,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_25754]) ).
tcf(c_25757,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(sk_c11,sk_c11) )
| ( sk_c10 != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_25755]) ).
tcf(c_27524,plain,
( ( multiply(identity,sk_c10) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_15987]) ).
tcf(c_27866,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_14392,c_104]) ).
tcf(c_28040,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_149,c_621]) ).
tcf(c_28041,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_147,c_621]) ).
tcf(c_28115,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_131,c_27866]) ).
tcf(c_28129,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_27866,c_105]) ).
tcf(c_28131,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_27866,c_105]) ).
tcf(c_28138,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(light_normalisation,[status(thm)],[c_1516,c_14392]) ).
tcf(c_28172,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,multiply(sk_c8,inverse(sk_c11))) = identity ) ),
inference(superposition,[status(thm)],[c_130,c_28131]) ).
tcf(c_28343,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_28129,c_103]) ).
tcf(c_28356,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_107,c_28343]) ).
tcf(c_28359,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,multiply(sk_c8,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_131,c_28343]) ).
tcf(c_28546,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_28115,c_130]) ).
tcf(c_28553,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_28546,c_27866]) ).
tcf(c_28635,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_28553,c_121]) ).
tcf(c_28636,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_28553,c_119]) ).
tcf(c_28637,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_28553,c_117]) ).
tcf(c_29735,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X0)),identity) = X1,
inference(superposition,[status(thm)],[c_104,c_2399]) ).
tcf(c_30119,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = X1,
inference(demodulation,[status(thm)],[c_29735,c_28138]) ).
tcf(c_30288,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_30119,c_2399]) ).
tcf(c_30985,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)) = multiply(X1,X2),
inference(superposition,[status(thm)],[c_30288,c_28343]) ).
tcf(c_31538,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),X2) = multiply(X1,multiply(inverse(X0),X2)),
inference(superposition,[status(thm)],[c_28343,c_30985]) ).
tcf(c_33848,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_28172,c_28359]) ).
tcf(c_35568,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != multiply(identity,multiply(identity,inverse(sk_c11))) )
| ( X0 != multiply(identity,multiply(identity,inverse(sk_c11))) ) ),
inference(instantiation,[status(thm)],[c_1232]) ).
tcf(c_37572,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(sk_c4) )
| ( inverse(sk_c4) != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_901]) ).
tcf(c_37573,plain,
( ( inverse(sk_c11) = inverse(sk_c4) )
| ( inverse(sk_c4) != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_37572]) ).
tcf(c_38050,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(inverse(X0),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1293]) ).
tcf(c_38051,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != inverse(sk_c11) )
| ( multiply(inverse(X0),sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_16273]) ).
tcf(c_38052,plain,
( ( multiply(inverse(sk_c11),sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_38050]) ).
tcf(c_38053,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c11 )
| ( sk_c11 != inverse(sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_38051]) ).
tcf(c_38236,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( sk_c10 != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_1232]) ).
tcf(c_38237,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( inverse(sk_c4) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_38236]) ).
tcf(c_38340,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(X0),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_16273]) ).
tcf(c_38342,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_38340]) ).
tcf(c_40128,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_1118,c_28356]) ).
tcf(c_40137,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c11) = sk_c11 ) ),
inference(instantiation,[status(thm)],[c_40128]) ).
tcf(c_40440,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_3360]) ).
tcf(c_40442,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_40440]) ).
tcf(c_40670,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_40671,plain,
( ( sk_c11 = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_40670]) ).
tcf(c_40951,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(X0),X0) )
| ~ iPr_def_10
| ( multiply(sk_c1,sk_c2) != identity ) ),
inference(resolution,[status(thm)],[c_18271,c_1851]) ).
tcf(c_40952,plain,
( ( sk_c11 = multiply(inverse(sk_c11),sk_c11) )
| ~ iPr_def_10
| ( multiply(sk_c1,sk_c2) != identity ) ),
inference(instantiation,[status(thm)],[c_40951]) ).
tcf(c_44123,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_25754]) ).
tcf(c_44124,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_44123]) ).
tcf(c_44309,plain,
! [X0: $i] :
( iPr_def_13
| ( X0 != sk_c10 )
| ( inverse(sk_c4) = X0 )
| iPr_def_10
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_9931,c_1360,c_3625,c_9931,c_28636]) ).
tcf(c_44310,plain,
! [X0: $i] :
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = X0 )
| ( X0 != sk_c10 ) ),
inference(renaming,[status(thm)],[c_44309]) ).
tcf(c_44311,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c11 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_44310]) ).
tcf(c_44776,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_10850,c_2853]) ).
tcf(c_44777,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_44776]) ).
tcf(c_45761,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,multiply(identity,inverse(sk_c11))) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,multiply(identity,inverse(sk_c11))) ) ),
inference(instantiation,[status(thm)],[c_35568]) ).
tcf(c_45762,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(identity,multiply(identity,inverse(sk_c11))) )
| ( sk_c10 != multiply(identity,inverse(sk_c11)) )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_25755]) ).
tcf(c_45763,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,multiply(identity,inverse(sk_c11))) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,multiply(identity,inverse(sk_c11))) ) ),
inference(instantiation,[status(thm)],[c_45761]) ).
tcf(c_45764,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(identity,multiply(identity,inverse(sk_c11))) )
| ( sk_c10 != multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_45762]) ).
tcf(c_45802,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_25755]) ).
tcf(c_45804,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_45802]) ).
tcf(c_48086,plain,
( ( multiply(sk_c9,sk_c10) = inverse(sk_c3) )
| ( inverse(sk_c3) != multiply(identity,sk_c10) )
| ( multiply(sk_c9,sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_6696]) ).
tcf(c_48224,plain,
( ( multiply(sk_c9,sk_c10) = multiply(identity,inverse(sk_c4)) )
| ( sk_c9 != identity )
| ( sk_c10 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_8572]) ).
tcf(c_48225,plain,
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,inverse(sk_c4)) )
| ( multiply(sk_c9,sk_c10) != multiply(identity,inverse(sk_c4)) ) ),
inference(instantiation,[status(thm)],[c_6324]) ).
tcf(c_49472,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_49474,plain,
multiply(identity,inverse(identity)) = inverse(identity),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_49483,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = X2 )
| ( X2 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_49484,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(X0,inverse(X0)) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_49472]) ).
tcf(c_49485,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,X1) )
| ( X0 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_49486,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_49484]) ).
tcf(c_49499,plain,
! [X0: $i] :
( ( sk_c11 = inverse(inverse(identity)) )
| ( sk_c11 != X0 )
| ( inverse(inverse(identity)) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_49505,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,inverse(X0)) )
| ( sk_c11 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_49528,plain,
! [X0: $i] :
( ( multiply(identity,inverse(identity)) = X0 )
| ( X0 != inverse(identity) )
| ( multiply(identity,inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_49483]) ).
tcf(c_49543,plain,
! [X0: $i] :
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(X0,sk_c10) )
| ( sk_c11 != X0 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_49485]) ).
tcf(c_49544,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(sk_c11,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_49543]) ).
tcf(c_49549,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_49553,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = inverse(inverse(multiply(inverse(X0),X0))) )
| ( sk_c11 != X1 )
| ( inverse(inverse(multiply(inverse(X0),X0))) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_49557,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,inverse(sk_c11)) = X1 )
| ( X1 != multiply(X0,sk_c10) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(X0,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_49483]) ).
tcf(c_49567,plain,
! [X0: $i] :
( ( inverse(identity) = inverse(X0) )
| ( identity != X0 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_49569,plain,
( ( inverse(identity) = inverse(sk_c11) )
| ( identity != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_49567]) ).
tcf(c_49576,plain,
( ( sk_c11 = inverse(inverse(identity)) )
| ( sk_c11 != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_49499]) ).
tcf(c_49577,plain,
inverse(inverse(identity)) = identity,
inference(instantiation,[status(thm)],[c_14392]) ).
tcf(c_49582,plain,
! [X0: $i] :
( ( multiply(identity,inverse(identity)) = inverse(X0) )
| ( inverse(X0) != inverse(identity) )
| ( multiply(identity,inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_49528]) ).
tcf(c_49583,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_49585,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_49583]) ).
tcf(c_49671,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_49549]) ).
tcf(c_49681,plain,
! [X0: $i] :
( ( sk_c11 = inverse(inverse(multiply(inverse(X0),X0))) )
| ( sk_c11 != multiply(inverse(X0),X0) )
| ( inverse(inverse(multiply(inverse(X0),X0))) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_49553]) ).
tcf(c_49682,plain,
! [X0: $i] : inverse(inverse(multiply(inverse(X0),X0))) = multiply(inverse(X0),X0),
inference(instantiation,[status(thm)],[c_14392]) ).
tcf(c_49768,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,inverse(X0)) )
| ( X2 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_49939,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(X1,X2) )
| ( multiply(X1,X2) != multiply(X0,sk_c10) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(X0,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_49557]) ).
tcf(c_49940,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(X1,sk_c10) )
| ( X2 != sk_c10 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_625]) ).
tcf(c_49941,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,sk_c11) != multiply(sk_c11,sk_c10) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_49939]) ).
tcf(c_49942,plain,
( ( multiply(sk_c11,sk_c11) = multiply(sk_c11,sk_c10) )
| ( sk_c11 != sk_c10 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_49940]) ).
tcf(c_50213,plain,
! [X0: $i] :
( ( sk_c11 = multiply(identity,inverse(identity)) )
| ( sk_c11 != inverse(X0) )
| ( multiply(identity,inverse(identity)) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_49505]) ).
tcf(c_50304,plain,
( ( inverse(inverse(identity)) = inverse(identity) )
| ( inverse(identity) != identity ) ),
inference(instantiation,[status(thm)],[c_49583]) ).
tcf(c_50512,plain,
! [X0: $i] :
( ( X0 = multiply(identity,inverse(identity)) )
| ( X0 != inverse(identity) )
| ( multiply(identity,inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_49768]) ).
tcf(c_50770,plain,
! [X0: $i] :
( ( inverse(inverse(multiply(inverse(X0),X0))) = inverse(identity) )
| ( inverse(multiply(inverse(X0),X0)) != identity ) ),
inference(instantiation,[status(thm)],[c_49583]) ).
tcf(c_51427,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(identity,sk_c10) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_49557]) ).
tcf(c_52071,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_52099,plain,
( ( multiply(identity,inverse(identity)) = inverse(inverse(identity)) )
| ( inverse(inverse(identity)) != inverse(identity) )
| ( multiply(identity,inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_49582]) ).
tcf(c_52707,plain,
! [X0: $i] :
( ( inverse(X0) = multiply(identity,inverse(identity)) )
| ( inverse(X0) != inverse(identity) )
| ( multiply(identity,inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_50512]) ).
tcf(c_52708,plain,
( ( inverse(sk_c11) = multiply(identity,inverse(identity)) )
| ( inverse(sk_c11) != inverse(identity) )
| ( multiply(identity,inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_52707]) ).
tcf(c_53933,plain,
! [X0: $i] :
( ( multiply(identity,inverse(identity)) = inverse(inverse(multiply(inverse(X0),X0))) )
| ( multiply(identity,inverse(identity)) != inverse(identity) )
| ( inverse(inverse(multiply(inverse(X0),X0))) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_49582]) ).
tcf(c_54260,plain,
( ( sk_c11 = multiply(identity,inverse(identity)) )
| ( sk_c11 != inverse(inverse(identity)) )
| ( multiply(identity,inverse(identity)) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_50213]) ).
tcf(c_54261,plain,
! [X0: $i] :
( ( sk_c11 = multiply(identity,inverse(identity)) )
| ( sk_c11 != inverse(inverse(multiply(inverse(X0),X0))) )
| ( multiply(identity,inverse(identity)) != inverse(inverse(multiply(inverse(X0),X0))) ) ),
inference(instantiation,[status(thm)],[c_50213]) ).
tcf(c_56372,plain,
! [X0: $i] :
( ( inverse(sk_c11) = X0 )
| ( X0 != multiply(identity,inverse(identity)) )
| ( inverse(sk_c11) != multiply(identity,inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_49549]) ).
tcf(c_56375,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != multiply(identity,inverse(identity)) )
| ( inverse(sk_c11) != multiply(identity,inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_56372]) ).
tcf(c_56497,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_56498,plain,
( ( inverse(inverse(sk_c11)) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_56497]) ).
tcf(c_57297,plain,
! [X0: $i,X1: $i] :
( ( inverse(identity) = X1 )
| ( X1 != inverse(X0) )
| ( inverse(identity) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_49671]) ).
tcf(c_57298,plain,
( ( inverse(identity) = sk_c11 )
| ( sk_c11 != inverse(sk_c11) )
| ( inverse(identity) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_57297]) ).
tcf(c_57407,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c11) = identity )
| ( identity != X0 )
| ( multiply(sk_c10,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_57408,plain,
( ( multiply(sk_c10,sk_c11) = identity )
| ( identity != sk_c11 )
| ( multiply(sk_c10,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_57407]) ).
tcf(c_60081,plain,
! [X0: $i] :
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != X0 )
| ( multiply(sk_c11,inverse(sk_c11)) != X0 ) ),
inference(instantiation,[status(thm)],[c_49483]) ).
tcf(c_60082,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != sk_c11 )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_60081]) ).
tcf(c_61256,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = identity )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_49549]) ).
tcf(c_61257,plain,
( ( inverse(sk_c11) = identity )
| ( identity != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_61256]) ).
tcf(c_76805,plain,
( iPr_def_11
| ( inverse(sk_c4) = sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_28040,c_109,c_628,c_918,c_924,c_1230,c_1955,c_2126,c_2283,c_2747,c_3457,c_3677,c_3757,c_3758,c_10464,c_10525,c_12279,c_16666,c_20745,c_25332,c_28636,c_37573,c_44124,c_44311,c_45804,c_49474,c_49569,c_49576,c_49577,c_49585,c_50304,c_52099,c_52708,c_54260,c_56375,c_56498,c_57298,c_61257]) ).
tcf(c_76814,plain,
( iPr_def_11
| ( inverse(sk_c3) = sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_28041,c_107,c_147,c_628,c_621,c_917,c_918,c_924,c_1230,c_1955,c_2126,c_2283,c_2747,c_3457,c_3625,c_3677,c_12279,c_25332,c_28637,c_44124,c_45804,c_49474,c_49569,c_49576,c_49577,c_49585,c_50304,c_52099,c_52708,c_54260,c_56375,c_56498,c_57298,c_61257]) ).
tcf(c_80310,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_52071]) ).
tcf(c_80311,plain,
( ( sk_c10 = identity )
| ( identity != sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_80310]) ).
tcf(c_81115,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2748,c_14392]) ).
tcf(c_81122,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_133,c_14392]) ).
tcf(c_81123,plain,
( ( inverse(sk_c6) = sk_c7 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_113,c_14392]) ).
tcf(c_81126,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_14392,c_104]) ).
tcf(c_81129,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_81115,c_628,c_924,c_1281,c_2748,c_3871,c_9192,c_14471,c_15711,c_17870,c_40951,c_40952,c_44777,c_49474,c_49681,c_49682,c_50770,c_52708,c_53933,c_54261,c_56375,c_80311]) ).
tcf(c_81131,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_621,c_81129]) ).
tcf(c_81232,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_129,c_81126]) ).
tcf(c_81233,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_109,c_81126]) ).
tcf(c_81242,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_81126,c_103]) ).
tcf(c_81284,plain,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ~ iPr_def_11
| ( sk_c11 != sk_c9 )
| ( inverse(sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_152,c_618]) ).
tcf(c_81291,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_104,c_618]) ).
tcf(c_81294,plain,
( ~ iPr_def_11
| ( sk_c9 != identity ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_81291,c_14392]) ).
tcf(c_81301,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(light_normalisation,[status(thm)],[c_1516,c_14392]) ).
tcf(c_81315,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X1),identity)) = inverse(multiply(X1,inverse(X0))),
inference(superposition,[status(thm)],[c_81301,c_31538]) ).
tcf(c_81316,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,inverse(X1))) = multiply(X1,inverse(X0)),
inference(demodulation,[status(thm)],[c_81315,c_81301]) ).
tcf(c_81347,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(X1)) = inverse(multiply(X1,X0)),
inference(superposition,[status(thm)],[c_14392,c_81316]) ).
tcf(c_81400,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),X0),
inference(superposition,[status(thm)],[c_14392,c_81347]) ).
tcf(c_81577,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_81122,c_134]) ).
tcf(c_81593,plain,
( ( sk_c8 = sk_c7 )
| ( multiply(sk_c1,sk_c2) = identity ) ),
inference(superposition,[status(thm)],[c_81577,c_81126]) ).
tcf(c_81608,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_81123,c_114]) ).
tcf(c_81648,plain,
( ( sk_c8 = sk_c7 )
| ( multiply(sk_c10,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_81608,c_104]) ).
tcf(c_81711,plain,
multiply(sk_c10,sk_c11) = identity,
inference(global_subsumption_just,[status(thm)],[c_81648,c_626,c_628,c_621,c_917,c_918,c_920,c_921,c_924,c_981,c_1032,c_1204,c_1230,c_1541,c_1955,c_2126,c_2223,c_2283,c_2463,c_2596,c_3394,c_3457,c_3625,c_3677,c_4179,c_4578,c_4795,c_4944,c_12279,c_14469,c_18149,c_18776,c_38342,c_40137,c_45763,c_45764,c_48086,c_48224,c_48225,c_49474,c_49576,c_49577,c_49585,c_50304,c_52099,c_52708,c_54260,c_56375,c_56498,c_57408,c_61257,c_76805,c_76814,c_81129]) ).
tcf(c_81776,plain,
( ( sk_c8 = sk_c7 )
| ( sk_c11 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_81593,c_121]) ).
tcf(c_81855,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1145,c_103]) ).
tcf(c_81877,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(superposition,[status(thm)],[c_14392,c_81855]) ).
tcf(c_81939,plain,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(inverse(sk_c10),identity) = sk_c4 ) ),
inference(superposition,[status(thm)],[c_1488,c_81855]) ).
tcf(c_81947,plain,
multiply(inverse(sk_c10),identity) = sk_c11,
inference(superposition,[status(thm)],[c_81711,c_81855]) ).
tcf(c_81962,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(superposition,[status(thm)],[c_81855,c_81400]) ).
tcf(c_81963,plain,
( ( sk_c11 = sk_c4 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(light_normalisation,[status(thm)],[c_81939,c_81947]) ).
tcf(c_81980,plain,
inverse(sk_c1) = sk_c2,
inference(global_subsumption_just,[status(thm)],[c_81232,c_129,c_127,c_628,c_621,c_918,c_924,c_981,c_1032,c_1033,c_1229,c_1230,c_1281,c_1541,c_1906,c_1946,c_1958,c_2596,c_2748,c_3211,c_3394,c_3457,c_3625,c_3677,c_3871,c_4421,c_4638,c_4944,c_9192,c_14471,c_15711,c_17870,c_18149,c_18776,c_33848,c_38052,c_38053,c_40442,c_40951,c_40952,c_44777,c_45804,c_48086,c_48224,c_48225,c_49474,c_49576,c_49577,c_49585,c_49681,c_49682,c_50304,c_50770,c_52099,c_52708,c_53933,c_54260,c_54261,c_56375,c_56498,c_80311,c_81963]) ).
tcf(c_82008,plain,
multiply(sk_c1,sk_c2) = identity,
inference(superposition,[status(thm)],[c_81980,c_81126]) ).
tcf(c_82059,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(inverse(sk_c11),sk_c9) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_149,c_81962]) ).
tcf(c_82060,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c9) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_147,c_81962]) ).
tcf(c_82066,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(inverse(identity),sk_c10) = inverse(sk_c4) ) ),
inference(superposition,[status(thm)],[c_1489,c_81962]) ).
tcf(c_82071,plain,
multiply(inverse(identity),sk_c10) = inverse(sk_c11),
inference(superposition,[status(thm)],[c_81711,c_81962]) ).
tcf(c_82083,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(X1),X2),
inference(superposition,[status(thm)],[c_81962,c_105]) ).
tcf(c_82084,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( inverse(inverse(multiply(sk_c10,X0))) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_81962,c_618]) ).
tcf(c_82091,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( inverse(sk_c11) = inverse(sk_c4) ) ),
inference(light_normalisation,[status(thm)],[c_82066,c_82071]) ).
tcf(c_82138,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(inverse(sk_c11),multiply(sk_c1,X0)) = multiply(inverse(sk_c2),X0) ) ),
inference(superposition,[status(thm)],[c_119,c_82083]) ).
tcf(c_82139,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c11),multiply(sk_c1,X0)) = multiply(inverse(sk_c2),X0) ) ),
inference(superposition,[status(thm)],[c_117,c_82083]) ).
tcf(c_82382,plain,
inverse(sk_c11) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_81233,c_1033,c_2806,c_82091]) ).
tcf(c_82398,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_81131,c_82382]) ).
tcf(c_82400,plain,
! [X0: $i] : inverse(multiply(sk_c10,X0)) = multiply(inverse(X0),sk_c11),
inference(superposition,[status(thm)],[c_82382,c_81400]) ).
tcf(c_82403,plain,
inverse(sk_c10) = sk_c11,
inference(superposition,[status(thm)],[c_82382,c_14392]) ).
tcf(c_83100,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( sk_c11 = identity ) ),
inference(global_subsumption_just,[status(thm)],[c_81776,c_28635]) ).
tcf(c_83101,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(renaming,[status(thm)],[c_83100]) ).
tcf(c_83110,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_83101,c_81126]) ).
tcf(c_83248,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_83110,c_120]) ).
tcf(c_83326,plain,
sk_c11 = identity,
inference(light_normalisation,[status(thm)],[c_83248,c_82008]) ).
tcf(c_83352,plain,
multiply(sk_c10,sk_c11) = sk_c11,
inference(demodulation,[status(thm)],[c_81711,c_83326]) ).
tcf(c_83354,plain,
( ~ iPr_def_11
| ( sk_c11 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_81294,c_83326]) ).
tcf(c_83355,plain,
! [X0: $i] : multiply(X0,sk_c11) = X0,
inference(demodulation,[status(thm)],[c_81301,c_83326]) ).
tcf(c_83356,plain,
inverse(sk_c11) = sk_c11,
inference(demodulation,[status(thm)],[c_81242,c_83326]) ).
tcf(c_83358,plain,
( ~ iPr_def_12
| ( sk_c11 != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_3625,c_83326]) ).
tcf(c_83359,plain,
! [X0: $i] : multiply(inverse(X0),X0) = sk_c11,
inference(demodulation,[status(thm)],[c_104,c_83326]) ).
tcf(c_83360,plain,
! [X0: $i] : multiply(sk_c11,X0) = X0,
inference(demodulation,[status(thm)],[c_103,c_83326]) ).
tcf(c_83385,plain,
sk_c11 = sk_c10,
inference(demodulation,[status(thm)],[c_83352,c_83355]) ).
tcf(c_83386,plain,
~ iPr_def_12,
inference(equality_resolution_simp,[status(thm)],[c_83358]) ).
tcf(c_83440,plain,
( iPr_def_13
| iPr_def_11
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_82398,c_83386]) ).
tcf(c_83441,plain,
( iPr_def_13
| iPr_def_11
| ( multiply(sk_c9,sk_c11) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_83440,c_83385]) ).
tcf(c_83442,plain,
( iPr_def_13
| iPr_def_11
| ( sk_c11 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_83441,c_83355]) ).
tcf(c_83443,plain,
multiply(sk_c11,sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_83360]) ).
tcf(c_83444,plain,
multiply(inverse(sk_c11),sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_83359]) ).
tcf(c_83581,plain,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_82059,c_82403,c_83356,c_83385]) ).
tcf(c_83588,plain,
( ( inverse(sk_c4) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_83581,c_81855]) ).
tcf(c_83595,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_82060,c_82403,c_83356]) ).
tcf(c_83602,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_83595,c_81855]) ).
tcf(c_85886,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( inverse(multiply(inverse(X0),sk_c11)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_82084,c_82400,c_83385]) ).
tcf(c_85887,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(sk_c10,X0) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_85886,c_81400,c_82382]) ).
tcf(c_85888,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( X0 != sk_c11 )
| ( inverse(X0) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_85887,c_83360,c_83385]) ).
tcf(c_85899,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X1),X0) != sk_c9 )
| ( multiply(inverse(X0),X1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_81400,c_85888]) ).
tcf(c_85902,plain,
( ~ iPr_def_11
| ( multiply(inverse(sk_c11),sk_c11) != sk_c9 )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_85899]) ).
tcf(c_86059,plain,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_82138,c_918,c_960,c_38237,c_76805,c_83385,c_83444,c_83588,c_85902]) ).
tcf(c_86061,plain,
inverse(sk_c4) = sk_c11,
inference(light_normalisation,[status(thm)],[c_86059,c_83385]) ).
tcf(c_86082,plain,
inverse(sk_c11) = sk_c4,
inference(superposition,[status(thm)],[c_86061,c_14392]) ).
tcf(c_86092,plain,
inverse(sk_c3) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_82139,c_76814,c_83444,c_83602,c_85902]) ).
tcf(c_86114,plain,
inverse(sk_c11) = sk_c3,
inference(superposition,[status(thm)],[c_86092,c_14392]) ).
tcf(c_86147,plain,
sk_c11 != sk_c9,
inference(global_subsumption_just,[status(thm)],[c_81284,c_628,c_632,c_918,c_960,c_1033,c_1230,c_1298,c_1956,c_2806,c_25756,c_25757,c_27524,c_40671,c_49486,c_49544,c_49941,c_49942,c_51427,c_56498,c_60082,c_82091,c_83385,c_83443,c_83442,c_83354]) ).
tcf(c_87336,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(inverse(multiply(X0,X1)),X2))) = X2,
inference(superposition,[status(thm)],[c_81877,c_105]) ).
tcf(c_87520,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(X1,multiply(X2,multiply(inverse(multiply(X0,multiply(X1,X2))),X3)))) = X3,
inference(superposition,[status(thm)],[c_105,c_87336]) ).
tcf(c_89297,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( multiply(X0,multiply(sk_c4,multiply(sk_c10,multiply(inverse(multiply(X0,sk_c9)),X1)))) = X1 ) ),
inference(superposition,[status(thm)],[c_148,c_87520]) ).
tcf(c_90608,plain,
sk_c11 = sk_c3,
inference(light_normalisation,[status(thm)],[c_82403,c_83385,c_86114]) ).
tcf(c_91329,plain,
sk_c11 = sk_c4,
inference(light_normalisation,[status(thm)],[c_86082,c_86114,c_90608]) ).
tcf(c_91755,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c11) = sk_c11 )
| ( multiply(X0,multiply(sk_c11,multiply(sk_c11,multiply(inverse(multiply(X0,sk_c9)),X1)))) = X1 ) ),
inference(light_normalisation,[status(thm)],[c_89297,c_83385,c_91329]) ).
tcf(c_91756,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = sk_c9 )
| ( multiply(X0,multiply(inverse(multiply(X0,sk_c9)),X1)) = X1 ) ),
inference(demodulation,[status(thm)],[c_91755,c_83355,c_83360]) ).
tcf(c_91757,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(multiply(X0,sk_c9)),X1)) = X1,
inference(forward_subsumption_resolution,[status(thm)],[c_91756,c_86147]) ).
tcf(c_91774,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),multiply(inverse(multiply(X0,multiply(X1,sk_c9))),X2)) = X2,
inference(superposition,[status(thm)],[c_105,c_91757]) ).
tcf(c_91885,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(inverse(multiply(X0,multiply(X1,sk_c9))),X2))) = X2,
inference(demodulation,[status(thm)],[c_91774,c_105]) ).
tcf(c_91952,plain,
! [X0: $i] : multiply(sk_c9,X0) = X0,
inference(superposition,[status(thm)],[c_91885,c_87520]) ).
tcf(c_92130,plain,
sk_c11 = sk_c9,
inference(superposition,[status(thm)],[c_91952,c_83355]) ).
tcf(c_92150,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_92130,c_86147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP371-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.10/5.54 % Computer : n002.cluster.edu
% 0.10/5.54 % Model : x86_64 x86_64
% 0.10/5.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.54 % Memory : 8046.5625MB
% 0.10/5.54 % OS : Linux 6.8.0-71-generic
% 0.10/5.54 % CPULimit : 300
% 0.10/5.54 % WCLimit : 300
% 0.10/5.54 % DateTime : Wed Sep 23 14:39:11 UTC 2026
% 0.10/5.55 % CPUTime :
% 0.10/5.55 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/5.58 Running first-order theorem proving
% 0.10/5.58 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.10/5.60
% 0.10/5.60 % ======== iProver multi-core TPTP/SMT =========
% 0.10/5.60
% 0.14/5.60 % Detected problem language: tptp
% 0.14/5.61 % Proving...
% 31.94/14.58 % SZS status Started for theBenchmark.p
% 31.94/14.58 % SZS status Unsatisfiable for theBenchmark.p
% 31.94/14.58
% 31.94/14.58 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 31.94/14.58
% 31.94/14.58 % ------ iProver source info
% 31.94/14.58
% 31.94/14.58 % git: date: 2026-07-19 20:42:38 +0200
% 31.94/14.58 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 31.94/14.58 % git: non_committed_changes: false
% 31.94/14.58
% 31.94/14.58 % ------ Parsing...% successful
% 31.94/14.58
% 31.94/14.58
% 31.94/14.58 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 31.94/14.58
% 31.94/14.58 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 31.94/14.58
% 31.94/14.58 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 31.94/14.58
% 31.94/14.58 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 31.94/14.58 % ------ Proving...
% 31.94/14.58 % ------ Problem Properties
% 31.94/14.58
% 31.94/14.58 %
% 31.94/14.58 % clauses 58
% 31.94/14.58 % conjectures 55
% 31.94/14.58 % EPR 0
% 31.94/14.58 % Horn 7
% 31.94/14.58 % unary 3
% 31.94/14.58 % binary 50
% 31.94/14.58 % lits 123
% 31.94/14.58 % lits eq 115
% 31.94/14.58 % fd_pure 0
% 31.94/14.58 % fd_pseudo 0
% 31.94/14.58 % fd_cond 0
% 31.94/14.58 % fd_pseudo_cond 0
% 31.94/14.58 % AC symbols 0
% 31.94/14.58
% 31.94/14.58 % ------ Input Options Time Limit: Unbounded
% 31.94/14.58
% 31.94/14.58
% 31.94/14.58 % ------
% 31.94/14.58 % Current options:
% 31.94/14.58 % ------
% 31.94/14.58
% 31.94/14.58
% 31.94/14.58 %
% 31.94/14.58
% 31.94/14.58 % ------ Proving...
% 31.94/14.58 %
% 31.94/14.58
% 31.94/14.58 % SZS status Unsatisfiable for theBenchmark.p
% 31.94/14.58
% 31.94/14.58 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 31.94/14.59
% 31.94/14.59
%------------------------------------------------------------------------------