%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP346-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:18 PM UTC 2026
% Result : Unsatisfiable 15.37s 3.28s
% Output : CNFRefutation 15.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 45
% Syntax : Number of formulae : 421 ( 130 unt; 12 def)
% Number of atoms : 1481 ( 745 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 567 ( 177 ~; 390 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 16 usr; 17 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 70 ( 0 sgn 70 !; 0 ?; 56 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c6,sk_c5) = sk_c7
| multiply(sk_c6,sk_c7) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c7 = multiply(sk_c6,sk_c5)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( inverse(sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c5 = inverse(sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c6,sk_c7) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c7 = multiply(sk_c3,sk_c6)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( inverse(sk_c3) = sk_c6
| multiply(sk_c6,sk_c7) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c6 = inverse(sk_c3)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c5
| multiply(sk_c6,sk_c7) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c5 = multiply(sk_c4,sk_c7)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c6,sk_c7) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c7 = inverse(sk_c4)
| multiply(sk_c6,sk_c7) = sk_c5 ),
inference(reorient_equations,[],[f17]) ).
fof(f21,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( inverse(sk_c7) = sk_c5
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c5 = inverse(sk_c7)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c7 = multiply(sk_c3,sk_c6)
| sk_c7 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f33,negated_conjecture,
( multiply(sk_c6,sk_c5) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c7 = multiply(sk_c6,sk_c5)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( inverse(sk_c7) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c5 = inverse(sk_c7)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c7 = multiply(sk_c3,sk_c6)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( inverse(sk_c3) = sk_c6
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c6 = inverse(sk_c3)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c5
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c5 = multiply(sk_c4,sk_c7)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c1,sk_c6) = sk_c7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c7 = inverse(sk_c4)
| sk_c7 = multiply(sk_c1,sk_c6) ),
inference(reorient_equations,[],[f45]) ).
fof(f49,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f50,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( inverse(sk_c7) = sk_c5
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c5 = inverse(sk_c7)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c3,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c7 = multiply(sk_c3,sk_c6)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( inverse(sk_c3) = sk_c6
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c6 = inverse(sk_c3)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c5
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c5 = multiply(sk_c4,sk_c7)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( inverse(sk_c4) = sk_c7
| inverse(sk_c2) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c7 = inverse(sk_c4)
| sk_c6 = inverse(sk_c2) ),
inference(reorient_equations,[],[f59]) ).
fof(f63,negated_conjecture,
( multiply(sk_c7,sk_c5) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c6 = multiply(sk_c7,sk_c5)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c7) = sk_c5
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c5 = inverse(sk_c7)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c3,sk_c6) = sk_c7
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c7 = multiply(sk_c3,sk_c6)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c3) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f70,plain,
( sk_c6 = inverse(sk_c3)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c5
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c5 = multiply(sk_c4,sk_c7)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c7 = inverse(sk_c4)
| sk_c6 = multiply(sk_c2,sk_c5) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
! [X2,X3,X0,X1] :
( inverse(X3) != sk_c7
| multiply(X3,sk_c7) != sk_c5
| inverse(X2) != sk_c6
| multiply(X2,sk_c6) != sk_c7
| inverse(sk_c7) != sk_c5
| multiply(sk_c7,sk_c5) != sk_c6
| multiply(sk_c6,sk_c5) != sk_c7
| multiply(X1,sk_c5) != sk_c6
| inverse(X1) != sk_c6
| multiply(X0,sk_c6) != sk_c7
| inverse(X0) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
! [X2,X3,X0,X1] :
( sk_c7 != inverse(X3)
| sk_c5 != multiply(X3,sk_c7)
| sk_c6 != inverse(X2)
| sk_c7 != multiply(X2,sk_c6)
| sk_c5 != inverse(sk_c7)
| sk_c6 != multiply(sk_c7,sk_c5)
| sk_c7 != multiply(sk_c6,sk_c5)
| sk_c6 != multiply(X1,sk_c5)
| sk_c6 != inverse(X1)
| sk_c7 != multiply(X0,sk_c6)
| inverse(X0) != sk_c7
| multiply(sk_c6,sk_c7) != sk_c5 ),
inference(reorient_equations,[],[f75]) ).
tcf(c_88,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_89,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_91,negated_conjecture,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_92,negated_conjecture,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_93,negated_conjecture,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_94,negated_conjecture,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_95,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_96,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_97,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_99,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_101,negated_conjecture,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_105,negated_conjecture,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_106,negated_conjecture,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_108,negated_conjecture,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_110,negated_conjecture,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c6 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c7 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_122,negated_conjecture,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_124,negated_conjecture,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_126,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(sk_c7) != sk_c5 )
| ( inverse(X3) != sk_c7 )
| ( inverse(X2) != sk_c6 )
| ( inverse(X1) != sk_c6 )
| ( inverse(X0) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( multiply(X3,sk_c7) != sk_c5 )
| ( multiply(X2,sk_c6) != sk_c7 )
| ( multiply(X1,sk_c5) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_467,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_126]) ).
tcf(c_468,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c5) != sk_c6 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_126]) ).
tcf(c_469,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c5 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_126]) ).
tcf(c_470,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_126]) ).
tcf(c_471,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_126]) ).
tcf(c_472,definition,
iPr_def_14 = multiply(sk_c6,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_473,definition,
iPr_def_15 = multiply(sk_c6,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_474,definition,
iPr_def_16 = multiply(sk_c7,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_475,definition,
iPr_def_17 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_476,definition,
iPr_def_18 = multiply(sk_c2,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_477,definition,
iPr_def_19 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_478,definition,
iPr_def_20 = multiply(sk_c4,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_479,definition,
iPr_def_21 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_480,definition,
iPr_def_22 = multiply(sk_c3,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_481,definition,
iPr_def_23 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_482,definition,
iPr_def_24 = multiply(sk_c1,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_483,definition,
iPr_def_25 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_484,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_17 != sk_c5 )
| ( iPr_def_16 != sk_c6 )
| ( iPr_def_15 != sk_c7 )
| ( iPr_def_14 != sk_c5 ) ),
inference(demodulation,[status(thm)],[c_471,c_475,c_474,c_473,c_472]) ).
tcf(c_485,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_470]) ).
tcf(c_486,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c7 )
| ( multiply(X0,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm)],[c_469]) ).
tcf(c_487,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c5) != sk_c6 ) ),
inference(demodulation,[status(thm)],[c_468]) ).
tcf(c_488,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c6 )
| ( multiply(X0,sk_c6) != sk_c7 ) ),
inference(demodulation,[status(thm)],[c_467]) ).
tcf(c_489,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_125,c_477,c_476]) ).
tcf(c_490,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_124,c_478]) ).
tcf(c_491,negated_conjecture,
( ( iPr_def_21 = sk_c6 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_123,c_479]) ).
tcf(c_492,negated_conjecture,
( ( iPr_def_22 = sk_c7 )
| ( iPr_def_18 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_122,c_480]) ).
tcf(c_493,negated_conjecture,
( ( iPr_def_18 = sk_c6 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_494,negated_conjecture,
( ( iPr_def_18 = sk_c6 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_496,negated_conjecture,
( ( iPr_def_23 = sk_c6 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_118,c_481]) ).
tcf(c_497,negated_conjecture,
( ( iPr_def_23 = sk_c6 )
| ( iPr_def_20 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_498,negated_conjecture,
( ( iPr_def_23 = sk_c6 )
| ( iPr_def_21 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_499,negated_conjecture,
( ( iPr_def_23 = sk_c6 )
| ( iPr_def_22 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_115]) ).
tcf(c_500,negated_conjecture,
( ( iPr_def_23 = sk_c6 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_501,negated_conjecture,
( ( iPr_def_23 = sk_c6 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_503,negated_conjecture,
( ( iPr_def_24 = sk_c7 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_111,c_482]) ).
tcf(c_504,negated_conjecture,
( ( iPr_def_24 = sk_c7 )
| ( iPr_def_20 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_505,negated_conjecture,
( ( iPr_def_24 = sk_c7 )
| ( iPr_def_21 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_506,negated_conjecture,
( ( iPr_def_24 = sk_c7 )
| ( iPr_def_22 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_507,negated_conjecture,
( ( iPr_def_24 = sk_c7 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_508,negated_conjecture,
( ( iPr_def_24 = sk_c7 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_509,negated_conjecture,
( ( iPr_def_24 = sk_c7 )
| ( iPr_def_15 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_513,negated_conjecture,
( ( iPr_def_25 = sk_c7 )
| ( iPr_def_22 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_101]) ).
tcf(c_514,negated_conjecture,
( ( iPr_def_25 = sk_c7 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_515,negated_conjecture,
( ( iPr_def_25 = sk_c7 )
| ( iPr_def_16 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_517,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_97]) ).
tcf(c_518,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_96]) ).
tcf(c_519,negated_conjecture,
( ( iPr_def_21 = sk_c6 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_95]) ).
tcf(c_520,negated_conjecture,
( ( iPr_def_22 = sk_c7 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_94]) ).
tcf(c_521,negated_conjecture,
( ( iPr_def_17 = sk_c5 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_93]) ).
tcf(c_522,negated_conjecture,
( ( iPr_def_16 = sk_c6 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_523,negated_conjecture,
( ( iPr_def_15 = sk_c7 )
| ( iPr_def_14 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_91]) ).
tcf(c_835,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_23,sk_c7) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_496,c_472]) ).
tcf(c_877,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_493,c_474]) ).
tcf(c_878,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_490,c_474]) ).
tcf(c_908,plain,
( ( sk_c6 = iPr_def_21 )
| ( multiply(iPr_def_23,sk_c7) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_498,c_472]) ).
tcf(c_939,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_23,sk_c5) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_499,c_473]) ).
tcf(c_940,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_23,sk_c7) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_499,c_472]) ).
tcf(c_961,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c6 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_500,c_497]) ).
tcf(c_962,plain,
( ( sk_c6 = iPr_def_23 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_500,c_474]) ).
tcf(c_980,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(iPr_def_23,sk_c5) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_501,c_473]) ).
tcf(c_981,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(iPr_def_23,sk_c7) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_501,c_472]) ).
tcf(c_1032,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_24,sk_c5) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_503,c_474]) ).
tcf(c_1098,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c3,iPr_def_23) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_499,c_480]) ).
tcf(c_1100,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_23) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_496,c_480]) ).
tcf(c_1103,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c3,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_492,c_480]) ).
tcf(c_1104,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_491,c_480]) ).
tcf(c_1105,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_489,c_480]) ).
tcf(c_1194,plain,
multiply(iPr_def_17,sk_c7) = identity,
inference(superposition,[status(thm)],[c_475,c_89]) ).
tcf(c_1195,plain,
multiply(iPr_def_21,sk_c3) = identity,
inference(superposition,[status(thm)],[c_479,c_89]) ).
tcf(c_1196,plain,
multiply(iPr_def_19,sk_c4) = identity,
inference(superposition,[status(thm)],[c_477,c_89]) ).
tcf(c_1197,plain,
multiply(iPr_def_25,sk_c1) = identity,
inference(superposition,[status(thm)],[c_483,c_89]) ).
tcf(c_1198,plain,
multiply(iPr_def_23,sk_c2) = identity,
inference(superposition,[status(thm)],[c_481,c_89]) ).
tcf(c_1232,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_505,c_482]) ).
tcf(c_1233,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_505,c_480]) ).
tcf(c_1239,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(iPr_def_21,sk_c7) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_505,c_472]) ).
tcf(c_1312,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c4,iPr_def_24) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_506,c_478]) ).
tcf(c_1313,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_24,sk_c5) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_506,c_474]) ).
tcf(c_1334,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c7 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_507,c_504]) ).
tcf(c_1336,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_507,c_474]) ).
tcf(c_1366,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(sk_c1,iPr_def_16) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_508,c_482]) ).
tcf(c_1456,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_24,sk_c5) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_509,c_474]) ).
tcf(c_1671,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_17,iPr_def_25) = identity ) ),
inference(superposition,[status(thm)],[c_513,c_1194]) ).
tcf(c_1672,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_513,c_478]) ).
tcf(c_1675,plain,
( ( sk_c7 = iPr_def_22 )
| ( inverse(iPr_def_25) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_513,c_475]) ).
tcf(c_1709,plain,
( ( sk_c7 = iPr_def_25 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_514,c_474]) ).
tcf(c_1761,plain,
( ( sk_c7 = iPr_def_25 )
| ( multiply(sk_c1,iPr_def_16) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_515,c_482]) ).
tcf(c_1954,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_517,c_476]) ).
tcf(c_2037,plain,
( ( sk_c5 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_20) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_518,c_476]) ).
tcf(c_2100,plain,
( ( sk_c6 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_519,c_476]) ).
tcf(c_2183,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_520,c_476]) ).
tcf(c_2284,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c5 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_521,c_518]) ).
tcf(c_2290,plain,
( ( sk_c5 = iPr_def_14 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_521,c_474]) ).
tcf(c_2336,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_522,c_476]) ).
tcf(c_2538,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_24 )
| ( inverse(sk_c1) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_482,c_485]) ).
tcf(c_2558,plain,
( ~ iPr_def_13
| ( sk_c7 != iPr_def_25 )
| ( sk_c7 != iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_2538,c_483]) ).
tcf(c_2712,plain,
( ~ iPr_def_12
| ( sk_c5 != iPr_def_14 )
| ( inverse(sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_472,c_486]) ).
tcf(c_2713,plain,
( ~ iPr_def_12
| ( sk_c5 != iPr_def_20 )
| ( inverse(sk_c4) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_478,c_486]) ).
tcf(c_2716,plain,
( ~ iPr_def_12
| ( sk_c5 != identity )
| ( inverse(iPr_def_17) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_1194,c_486]) ).
tcf(c_2729,plain,
( ~ iPr_def_12
| ( sk_c5 != iPr_def_20 )
| ( sk_c7 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_2713,c_477]) ).
tcf(c_2814,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_18 )
| ( inverse(sk_c2) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_476,c_487]) ).
tcf(c_2815,plain,
( ~ iPr_def_11
| ( sk_c6 != sk_c5 )
| ( inverse(identity) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_88,c_487]) ).
tcf(c_2816,plain,
( ~ iPr_def_11
| ( sk_c6 != identity )
| ( inverse(inverse(sk_c5)) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_89,c_487]) ).
tcf(c_2835,plain,
( ~ iPr_def_11
| ( sk_c6 != iPr_def_23 )
| ( sk_c6 != iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_2814,c_481]) ).
tcf(c_2976,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_22 )
| ( inverse(sk_c3) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_480,c_488]) ).
tcf(c_2977,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_24 )
| ( inverse(sk_c1) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_482,c_488]) ).
tcf(c_2997,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_24 )
| ( sk_c6 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_2977,c_483]) ).
tcf(c_3001,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_22 )
| ( sk_c6 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_2976,c_479]) ).
tcf(c_3161,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c7 = iPr_def_19 )
| ( sk_c5 != iPr_def_17 )
| ( sk_c7 != iPr_def_15 )
| ( sk_c6 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_517,c_484]) ).
tcf(c_3165,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c7 = iPr_def_24 )
| ( iPr_def_14 != iPr_def_20 )
| ( sk_c5 != iPr_def_17 )
| ( sk_c7 != iPr_def_15 )
| ( sk_c6 != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_504,c_484]) ).
tcf(c_3344,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c7,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_472,c_90]) ).
tcf(c_3345,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c5,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_473,c_90]) ).
tcf(c_3347,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c6,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_480,c_90]) ).
tcf(c_3348,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c7,X0)) = multiply(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_478,c_90]) ).
tcf(c_3349,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c6,X0)) = multiply(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_482,c_90]) ).
tcf(c_3352,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_89,c_90]) ).
tcf(c_3354,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1194,c_90]) ).
tcf(c_3355,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1195,c_90]) ).
tcf(c_3356,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1196,c_90]) ).
tcf(c_3357,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1197,c_90]) ).
tcf(c_3358,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1198,c_90]) ).
tcf(c_3364,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3358,c_88]) ).
tcf(c_3365,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3357,c_88]) ).
tcf(c_3366,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3356,c_88]) ).
tcf(c_3367,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3355,c_88]) ).
tcf(c_3368,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3354,c_88]) ).
tcf(c_3768,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_23,sk_c7) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_961,c_472]) ).
tcf(c_4091,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_24,sk_c5) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1334,c_474]) ).
tcf(c_4696,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_2284,c_476]) ).
tcf(c_4891,plain,
multiply(iPr_def_23,iPr_def_18) = sk_c5,
inference(superposition,[status(thm)],[c_476,c_3364]) ).
tcf(c_4894,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(iPr_def_18,X0)) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_4891,c_90]) ).
tcf(c_4896,plain,
multiply(iPr_def_25,iPr_def_24) = sk_c6,
inference(superposition,[status(thm)],[c_482,c_3365]) ).
tcf(c_4899,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(iPr_def_24,X0)) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_4896,c_90]) ).
tcf(c_4927,plain,
multiply(iPr_def_19,iPr_def_20) = sk_c7,
inference(superposition,[status(thm)],[c_478,c_3366]) ).
tcf(c_4932,plain,
multiply(iPr_def_21,iPr_def_22) = sk_c6,
inference(superposition,[status(thm)],[c_480,c_3367]) ).
tcf(c_4935,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(iPr_def_22,X0)) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_4932,c_90]) ).
tcf(c_5216,plain,
multiply(iPr_def_17,iPr_def_16) = sk_c5,
inference(superposition,[status(thm)],[c_474,c_3368]) ).
tcf(c_6773,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_17,iPr_def_16) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_878,c_3368]) ).
tcf(c_6774,plain,
( ( sk_c5 = iPr_def_20 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_6773,c_5216]) ).
tcf(c_7661,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_23,iPr_def_14) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_520,c_939]) ).
tcf(c_7740,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_506,c_940]) ).
tcf(c_7966,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(iPr_def_23,iPr_def_14) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_522,c_980]) ).
tcf(c_8387,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_24,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_517,c_1032]) ).
tcf(c_8838,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1098,c_3367]) ).
tcf(c_8839,plain,
( ( sk_c7 = iPr_def_22 )
| ( sk_c6 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_8838,c_4932]) ).
tcf(c_8884,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1100,c_3367]) ).
tcf(c_8885,plain,
( ( sk_c7 = iPr_def_19 )
| ( sk_c6 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_8884,c_4932]) ).
tcf(c_9100,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_1103,c_3367]) ).
tcf(c_9101,plain,
( ( sk_c7 = iPr_def_22 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_9100,c_4932]) ).
tcf(c_9112,plain,
( ( sk_c6 = iPr_def_18 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1104,c_3367]) ).
tcf(c_9113,plain,
( ( sk_c6 = iPr_def_21 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_9112,c_4932]) ).
tcf(c_9124,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_1105,c_3367]) ).
tcf(c_9125,plain,
( ( sk_c7 = iPr_def_19 )
| ( sk_c6 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_9124,c_4932]) ).
tcf(c_9452,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(iPr_def_25,iPr_def_24) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1232,c_3365]) ).
tcf(c_9453,plain,
( ( sk_c7 = iPr_def_24 )
| ( sk_c6 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_9452,c_4896]) ).
tcf(c_9666,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_19,iPr_def_20) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1312,c_3366]) ).
tcf(c_9667,plain,
( ( sk_c7 = iPr_def_24 )
| ( sk_c7 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_9666,c_4927]) ).
tcf(c_9688,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_24,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_520,c_1313]) ).
tcf(c_10180,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(iPr_def_25,iPr_def_24) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1366,c_3365]) ).
tcf(c_10181,plain,
( ( sk_c7 = iPr_def_24 )
| ( sk_c6 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_10180,c_4896]) ).
tcf(c_10378,plain,
( ( sk_c7 = iPr_def_15 )
| ( multiply(iPr_def_24,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_523,c_1456]) ).
tcf(c_11179,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_19,iPr_def_20) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1672,c_3366]) ).
tcf(c_11180,plain,
( ( sk_c7 = iPr_def_25 )
| ( sk_c7 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_11179,c_4927]) ).
tcf(c_11671,plain,
( ( sk_c7 = iPr_def_25 )
| ( multiply(iPr_def_25,iPr_def_24) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1761,c_3365]) ).
tcf(c_11672,plain,
( ( sk_c7 = iPr_def_25 )
| ( sk_c6 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_11671,c_4896]) ).
tcf(c_11920,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(iPr_def_23,iPr_def_18) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1954,c_3364]) ).
tcf(c_11921,plain,
( ( sk_c5 = iPr_def_14 )
| ( sk_c7 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_11920,c_4891]) ).
tcf(c_12266,plain,
( ( sk_c5 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_18) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2037,c_3364]) ).
tcf(c_12267,plain,
( ( sk_c5 = iPr_def_20 )
| ( sk_c5 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_12266,c_4891]) ).
tcf(c_12619,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_23,iPr_def_18) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2183,c_3364]) ).
tcf(c_12620,plain,
( ( sk_c5 = iPr_def_14 )
| ( sk_c7 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_12619,c_4891]) ).
tcf(c_13400,plain,
multiply(sk_c6,iPr_def_16) = multiply(iPr_def_14,sk_c5),
inference(superposition,[status(thm)],[c_474,c_3344]) ).
tcf(c_14108,plain,
multiply(sk_c3,iPr_def_14) = multiply(iPr_def_22,sk_c7),
inference(superposition,[status(thm)],[c_472,c_3347]) ).
tcf(c_14109,plain,
multiply(sk_c3,iPr_def_15) = multiply(iPr_def_22,sk_c5),
inference(superposition,[status(thm)],[c_473,c_3347]) ).
tcf(c_14360,plain,
multiply(iPr_def_21,multiply(iPr_def_22,sk_c7)) = iPr_def_14,
inference(superposition,[status(thm)],[c_14108,c_3367]) ).
tcf(c_14471,plain,
multiply(iPr_def_21,multiply(iPr_def_22,sk_c5)) = iPr_def_15,
inference(superposition,[status(thm)],[c_14109,c_3367]) ).
tcf(c_14674,plain,
multiply(sk_c1,iPr_def_15) = multiply(iPr_def_24,sk_c5),
inference(superposition,[status(thm)],[c_473,c_3349]) ).
tcf(c_14969,plain,
multiply(iPr_def_25,multiply(iPr_def_24,sk_c5)) = iPr_def_15,
inference(superposition,[status(thm)],[c_14674,c_3365]) ).
tcf(c_16098,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_24,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_2284,c_4091]) ).
tcf(c_17225,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c6,iPr_def_14) = multiply(iPr_def_25,iPr_def_16) ) ),
inference(superposition,[status(thm)],[c_9688,c_4899]) ).
tcf(c_17382,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3352,c_88]) ).
tcf(c_17404,plain,
multiply(inverse(sk_c6),iPr_def_14) = sk_c7,
inference(superposition,[status(thm)],[c_472,c_17382]) ).
tcf(c_17411,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_88,c_17382]) ).
tcf(c_17412,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_89,c_17382]) ).
tcf(c_17515,plain,
multiply(inverse(iPr_def_17),identity) = sk_c7,
inference(superposition,[status(thm)],[c_1194,c_17382]) ).
tcf(c_17583,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_3368,c_17382]) ).
tcf(c_17584,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_3367,c_17382]) ).
tcf(c_17585,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3366,c_17382]) ).
tcf(c_17586,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3365,c_17382]) ).
tcf(c_17587,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3364,c_17382]) ).
tcf(c_17665,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_17382,c_17382]) ).
tcf(c_18688,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm)],[c_17515,c_17583]) ).
tcf(c_18713,plain,
multiply(sk_c4,sk_c7) = multiply(iPr_def_20,identity),
inference(superposition,[status(thm)],[c_18688,c_3348]) ).
tcf(c_18714,plain,
multiply(sk_c6,sk_c7) = multiply(iPr_def_14,identity),
inference(superposition,[status(thm)],[c_18688,c_3344]) ).
tcf(c_18717,plain,
multiply(iPr_def_14,identity) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_18714,c_472]) ).
tcf(c_18718,plain,
multiply(iPr_def_20,identity) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_18713,c_478]) ).
tcf(c_18813,plain,
multiply(inverse(iPr_def_20),iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_18718,c_17382]) ).
tcf(c_18899,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_17412,c_17665]) ).
tcf(c_18922,plain,
multiply(sk_c6,sk_c5) = multiply(iPr_def_15,identity),
inference(superposition,[status(thm)],[c_18899,c_3345]) ).
tcf(c_18924,plain,
multiply(sk_c6,identity) = multiply(iPr_def_21,iPr_def_22),
inference(superposition,[status(thm)],[c_18899,c_4935]) ).
tcf(c_18925,plain,
multiply(sk_c1,sk_c6) = multiply(iPr_def_24,identity),
inference(superposition,[status(thm)],[c_18899,c_3349]) ).
tcf(c_18928,plain,
multiply(sk_c6,identity) = multiply(iPr_def_25,iPr_def_24),
inference(superposition,[status(thm)],[c_18899,c_4899]) ).
tcf(c_18929,plain,
multiply(sk_c5,identity) = multiply(iPr_def_23,iPr_def_18),
inference(superposition,[status(thm)],[c_18899,c_4894]) ).
tcf(c_18934,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_18899,c_17411]) ).
tcf(c_18935,plain,
multiply(sk_c5,identity) = sk_c5,
inference(light_normalisation,[status(thm)],[c_18929,c_4891]) ).
tcf(c_18938,plain,
multiply(iPr_def_24,identity) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_18925,c_482]) ).
tcf(c_18941,plain,
multiply(iPr_def_15,identity) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_18922,c_473]) ).
tcf(c_18971,plain,
multiply(identity,identity) = identity,
inference(superposition,[status(thm)],[c_18934,c_89]) ).
tcf(c_18977,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_17)) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_17583,c_488]) ).
tcf(c_18978,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_17)) != sk_c7 )
| ( multiply(sk_c7,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_17583,c_485]) ).
tcf(c_18979,plain,
multiply(sk_c7,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_17583,c_89]) ).
tcf(c_18984,plain,
! [X0: $i] : multiply(sk_c7,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_17583,c_17382]) ).
tcf(c_18985,plain,
multiply(sk_c7,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_17583,c_18899]) ).
tcf(c_18999,plain,
( ( identity = iPr_def_16 )
| ( sk_c5 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_2290,c_18979]) ).
tcf(c_19000,plain,
( ( identity = iPr_def_16 )
| ( sk_c7 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1709,c_18979]) ).
tcf(c_19001,plain,
( ( identity = iPr_def_16 )
| ( sk_c7 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_1336,c_18979]) ).
tcf(c_19002,plain,
( ( identity = iPr_def_16 )
| ( sk_c6 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_962,c_18979]) ).
tcf(c_19003,plain,
( ( identity = iPr_def_16 )
| ( sk_c6 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_877,c_18979]) ).
tcf(c_19041,plain,
multiply(sk_c4,identity) = multiply(iPr_def_20,iPr_def_17),
inference(superposition,[status(thm)],[c_18979,c_3348]) ).
tcf(c_19042,plain,
multiply(sk_c6,identity) = multiply(iPr_def_14,iPr_def_17),
inference(superposition,[status(thm)],[c_18979,c_3344]) ).
tcf(c_19078,plain,
inverse(iPr_def_17) = sk_c7,
inference(demodulation,[status(thm)],[c_18985,c_18899]) ).
tcf(c_19102,plain,
! [X0: $i] :
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_24,multiply(iPr_def_17,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_506,c_18984]) ).
tcf(c_19121,plain,
multiply(sk_c7,sk_c5) = iPr_def_16,
inference(superposition,[status(thm)],[c_5216,c_18984]) ).
tcf(c_19565,plain,
( ( identity = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_18999,c_476]) ).
tcf(c_19569,plain,
( ( identity = iPr_def_16 )
| ( multiply(sk_c7,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_18999,c_474]) ).
tcf(c_20017,plain,
( ( iPr_def_24 = iPr_def_25 )
| ( identity = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_19001,c_19000]) ).
tcf(c_20289,plain,
( ( identity = iPr_def_16 )
| ( multiply(iPr_def_23,sk_c7) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_19002,c_472]) ).
tcf(c_20545,plain,
( ( identity = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_18) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_19003,c_482]) ).
tcf(c_20546,plain,
( ( identity = iPr_def_16 )
| ( multiply(sk_c3,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_19003,c_480]) ).
tcf(c_20667,plain,
multiply(iPr_def_20,iPr_def_17) = sk_c4,
inference(demodulation,[status(thm)],[c_19041,c_18899]) ).
tcf(c_20668,plain,
multiply(inverse(iPr_def_20),sk_c4) = iPr_def_17,
inference(superposition,[status(thm)],[c_20667,c_17382]) ).
tcf(c_20673,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),multiply(sk_c4,X0)) = multiply(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_20668,c_90]) ).
tcf(c_20721,plain,
( ( identity = iPr_def_16 )
| ( multiply(iPr_def_24,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_19001,c_19569]) ).
tcf(c_20762,plain,
multiply(iPr_def_14,iPr_def_17) = sk_c6,
inference(demodulation,[status(thm)],[c_19042,c_18899]) ).
tcf(c_20763,plain,
multiply(inverse(iPr_def_14),sk_c6) = iPr_def_17,
inference(superposition,[status(thm)],[c_20762,c_17382]) ).
tcf(c_20786,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(inverse(iPr_def_14),iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_508,c_20763]) ).
tcf(c_20787,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(inverse(iPr_def_14),iPr_def_21) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_505,c_20763]) ).
tcf(c_20789,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(inverse(iPr_def_14),iPr_def_23) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_501,c_20763]) ).
tcf(c_20790,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(inverse(iPr_def_14),iPr_def_23) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_499,c_20763]) ).
tcf(c_20794,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(inverse(iPr_def_14),iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_494,c_20763]) ).
tcf(c_20795,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(inverse(iPr_def_14),iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_492,c_20763]) ).
tcf(c_20798,plain,
( ~ iPr_def_10
| ( sk_c7 != iPr_def_17 )
| ( inverse(inverse(iPr_def_14)) != sk_c6 ) ),
inference(superposition,[status(thm)],[c_20763,c_488]) ).
tcf(c_20800,plain,
multiply(inverse(inverse(iPr_def_14)),iPr_def_17) = sk_c6,
inference(superposition,[status(thm)],[c_20763,c_17382]) ).
tcf(c_20801,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),multiply(sk_c6,X0)) = multiply(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_20763,c_90]) ).
tcf(c_20932,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(inverse(inverse(iPr_def_14)),iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_20786,c_17382]) ).
tcf(c_20987,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(inverse(inverse(iPr_def_14)),iPr_def_17) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_20787,c_17382]) ).
tcf(c_21015,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(inverse(inverse(iPr_def_14)),iPr_def_17) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_20789,c_17382]) ).
tcf(c_21029,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(inverse(inverse(iPr_def_14)),iPr_def_17) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_20790,c_17382]) ).
tcf(c_21301,plain,
multiply(sk_c3,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_17584,c_89]) ).
tcf(c_21306,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_17584,c_17382]) ).
tcf(c_21307,plain,
multiply(sk_c3,identity) = inverse(iPr_def_21),
inference(superposition,[status(thm)],[c_17584,c_18899]) ).
tcf(c_21323,plain,
( ( identity = iPr_def_22 )
| ( sk_c7 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_1233,c_21301]) ).
tcf(c_21370,plain,
multiply(iPr_def_21,identity) = iPr_def_21,
inference(superposition,[status(thm)],[c_21301,c_3367]) ).
tcf(c_21403,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(inverse(inverse(iPr_def_14)),iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_20794,c_17382]) ).
tcf(c_21414,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(inverse(inverse(iPr_def_14)),iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_20795,c_17382]) ).
tcf(c_22265,plain,
inverse(iPr_def_21) = sk_c3,
inference(demodulation,[status(thm)],[c_21307,c_18899]) ).
tcf(c_22270,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(sk_c3,iPr_def_14) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_1239,c_21306]) ).
tcf(c_22276,plain,
multiply(sk_c3,sk_c6) = iPr_def_22,
inference(superposition,[status(thm)],[c_4932,c_21306]) ).
tcf(c_22318,plain,
( ( sk_c7 = iPr_def_24 )
| ( multiply(iPr_def_22,sk_c7) = sk_c7 ) ),
inference(light_normalisation,[status(thm)],[c_22270,c_14108]) ).
tcf(c_23295,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_19)) != sk_c7 )
| ( multiply(sk_c4,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_17585,c_485]) ).
tcf(c_23296,plain,
multiply(sk_c4,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_17585,c_89]) ).
tcf(c_23299,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_19)) != sk_c7 )
| ( multiply(sk_c4,sk_c7) != sk_c5 ) ),
inference(superposition,[status(thm)],[c_17585,c_486]) ).
tcf(c_23301,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_17585,c_17382]) ).
tcf(c_23302,plain,
multiply(sk_c4,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_17585,c_18899]) ).
tcf(c_23359,plain,
inverse(iPr_def_19) = sk_c4,
inference(demodulation,[status(thm)],[c_23302,c_18899]) ).
tcf(c_23467,plain,
multiply(sk_c4,sk_c7) = iPr_def_20,
inference(superposition,[status(thm)],[c_4927,c_23301]) ).
tcf(c_23831,plain,
( ( identity = iPr_def_16 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_20546,c_3367]) ).
tcf(c_24140,plain,
multiply(sk_c1,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_17586,c_89]) ).
tcf(c_24143,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_25)) != sk_c7 )
| ( multiply(sk_c1,sk_c7) != sk_c5 ) ),
inference(superposition,[status(thm)],[c_17586,c_486]) ).
tcf(c_24146,plain,
multiply(sk_c1,identity) = inverse(iPr_def_25),
inference(superposition,[status(thm)],[c_17586,c_18899]) ).
tcf(c_24414,plain,
multiply(iPr_def_25,identity) = iPr_def_25,
inference(superposition,[status(thm)],[c_24140,c_3365]) ).
tcf(c_24652,plain,
inverse(iPr_def_25) = sk_c1,
inference(demodulation,[status(thm)],[c_24146,c_18899]) ).
tcf(c_24659,plain,
( ( sk_c1 = iPr_def_17 )
| ( sk_c7 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_1675,c_24652]) ).
tcf(c_26037,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_17,iPr_def_15) = multiply(iPr_def_24,sk_c5) ) ),
inference(superposition,[status(thm)],[c_24659,c_14674]) ).
tcf(c_26056,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_17,sk_c6) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_24659,c_482]) ).
tcf(c_28981,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_23)) != sk_c6 )
| ( multiply(sk_c2,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_17587,c_488]) ).
tcf(c_28983,plain,
multiply(sk_c2,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_17587,c_89]) ).
tcf(c_28988,plain,
! [X0: $i] : multiply(sk_c2,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_17587,c_17382]) ).
tcf(c_28989,plain,
multiply(sk_c2,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_17587,c_18899]) ).
tcf(c_29152,plain,
inverse(iPr_def_23) = sk_c2,
inference(demodulation,[status(thm)],[c_28989,c_18899]) ).
tcf(c_33103,plain,
( ( identity = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_14) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_20289,c_28988]) ).
tcf(c_33104,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_14) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_3768,c_28988]) ).
tcf(c_33106,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_14) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_981,c_28988]) ).
tcf(c_33108,plain,
( ( sk_c6 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_14) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_908,c_28988]) ).
tcf(c_33109,plain,
( ( sk_c7 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_14) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_835,c_28988]) ).
tcf(c_33114,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_15) = sk_c5 ) ),
inference(superposition,[status(thm)],[c_939,c_28988]) ).
tcf(c_33118,plain,
multiply(sk_c2,sk_c5) = iPr_def_18,
inference(superposition,[status(thm)],[c_4891,c_28988]) ).
tcf(c_33124,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_7740,c_28988]) ).
tcf(c_33127,plain,
( ( sk_c6 = iPr_def_16 )
| ( multiply(sk_c2,iPr_def_15) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_7966,c_28988]) ).
tcf(c_33128,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_15) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_7661,c_28988]) ).
tcf(c_33379,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(iPr_def_24,identity) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1671,c_19102]) ).
tcf(c_33611,plain,
( ( sk_c7 = iPr_def_22 )
| ~ iPr_def_13
| ( sk_c7 != iPr_def_24 )
| ( inverse(iPr_def_17) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_26056,c_485]) ).
tcf(c_33620,plain,
( ( sk_c7 = iPr_def_22 )
| ( multiply(sk_c7,iPr_def_24) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_26056,c_18984]) ).
tcf(c_33629,plain,
( ( sk_c7 = iPr_def_22 )
| ~ iPr_def_13
| ( sk_c7 != iPr_def_24 ) ),
inference(ground_joinability,[status(thm)],[c_33611,c_19078]) ).
tcf(c_43404,plain,
multiply(inverse(iPr_def_20),iPr_def_20) = multiply(iPr_def_17,sk_c7),
inference(superposition,[status(thm)],[c_23467,c_20673]) ).
tcf(c_43421,plain,
multiply(inverse(iPr_def_20),identity) = multiply(iPr_def_17,iPr_def_19),
inference(superposition,[status(thm)],[c_23296,c_20673]) ).
tcf(c_43683,plain,
multiply(inverse(iPr_def_14),multiply(iPr_def_14,sk_c5)) = multiply(iPr_def_17,iPr_def_16),
inference(superposition,[status(thm)],[c_13400,c_20801]) ).
tcf(c_43684,plain,
multiply(inverse(iPr_def_14),sk_c6) = multiply(iPr_def_17,identity),
inference(superposition,[status(thm)],[c_18899,c_20801]) ).
tcf(c_43730,plain,
multiply(inverse(iPr_def_14),multiply(iPr_def_14,sk_c5)) = sk_c5,
inference(light_normalisation,[status(thm)],[c_43683,c_5216]) ).
tcf(c_44113,plain,
( ( sk_c7 = iPr_def_22 )
| ~ iPr_def_13
| ( sk_c7 != iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_506,c_2558]) ).
tcf(c_44976,plain,
( ( sk_c7 = iPr_def_22 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_44113,c_9667,c_33629]) ).
tcf(c_47111,plain,
( ( sk_c7 = iPr_def_22 )
| ~ iPr_def_11
| ( sk_c6 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_492,c_2835]) ).
tcf(c_47113,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_11
| ( sk_c6 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_489,c_2835]) ).
tcf(c_47310,plain,
( ( sk_c7 = iPr_def_22 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_47111,c_8839,c_47111]) ).
tcf(c_47316,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_47113,c_8885,c_47113]) ).
tcf(c_48655,plain,
( ~ iPr_def_10
| ( sk_c6 != iPr_def_25 ) ),
inference(global_subsumption_just,[status(thm)],[c_2997,c_3001,c_2997,c_9453,c_9667]) ).
tcf(c_48701,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10
| ( iPr_def_21 != iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_491,c_48655]) ).
tcf(c_48702,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_10
| ( iPr_def_18 != iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_489,c_48655]) ).
tcf(c_49230,plain,
multiply(iPr_def_17,iPr_def_19) = inverse(iPr_def_20),
inference(demodulation,[status(thm)],[c_43421,c_18899]) ).
tcf(c_49245,plain,
multiply(sk_c7,inverse(iPr_def_20)) = iPr_def_19,
inference(superposition,[status(thm)],[c_49230,c_18984]) ).
tcf(c_49827,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_48701,c_3001,c_9101,c_9113]) ).
tcf(c_49866,plain,
multiply(iPr_def_20,inverse(iPr_def_20)) = multiply(sk_c4,iPr_def_19),
inference(superposition,[status(thm)],[c_49245,c_3348]) ).
tcf(c_49867,plain,
multiply(iPr_def_14,inverse(iPr_def_20)) = multiply(sk_c6,iPr_def_19),
inference(superposition,[status(thm)],[c_49245,c_3344]) ).
tcf(c_49870,plain,
multiply(iPr_def_20,inverse(iPr_def_20)) = identity,
inference(light_normalisation,[status(thm)],[c_49866,c_23296]) ).
tcf(c_51769,plain,
( ~ iPr_def_12
| ( inverse(sk_c6) != sk_c7 ) ),
inference(global_subsumption_just,[status(thm)],[c_2712,c_2729,c_2712,c_11921,c_12267]) ).
tcf(c_51816,plain,
( ( sk_c7 = iPr_def_19 )
| ~ iPr_def_12
| ( inverse(iPr_def_18) != sk_c7 ) ),
inference(superposition,[status(thm)],[c_489,c_51769]) ).
tcf(c_52124,plain,
multiply(inverse(iPr_def_14),multiply(iPr_def_14,inverse(iPr_def_20))) = multiply(iPr_def_17,iPr_def_19),
inference(superposition,[status(thm)],[c_49867,c_20801]) ).
tcf(c_52127,plain,
multiply(inverse(iPr_def_14),multiply(iPr_def_14,inverse(iPr_def_20))) = inverse(iPr_def_20),
inference(light_normalisation,[status(thm)],[c_52124,c_49230]) ).
tcf(c_53051,plain,
( ~ iPr_def_12
| ( sk_c5 != identity ) ),
inference(ground_joinability,[status(thm)],[c_2716,c_19078]) ).
tcf(c_53091,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_12
| ( identity != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_493,c_53051]) ).
tcf(c_53488,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_53091,c_2729,c_6774,c_9125]) ).
tcf(c_53720,plain,
( ~ iPr_def_11
| ( sk_c6 != identity )
| ( sk_c6 != sk_c5 ) ),
inference(light_normalisation,[status(thm)],[c_2815,c_18934]) ).
tcf(c_53762,plain,
( ( sk_c6 = iPr_def_23 )
| ~ iPr_def_11
| ( sk_c6 != iPr_def_20 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm)],[c_497,c_53720]) ).
tcf(c_53764,plain,
( ( sk_c6 = iPr_def_18 )
| ~ iPr_def_11
| ( sk_c6 != iPr_def_20 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm)],[c_490,c_53720]) ).
tcf(c_54361,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_53764,c_53762,c_53720,c_53488,c_52127,c_52124,c_51816,c_51769,c_49870,c_49866,c_49827,c_48702,c_47316,c_47310,c_44976,c_43730,c_43684,c_43683,c_43404,c_33620,c_33379,c_33128,c_33127,c_33124,c_33118,c_33114,c_33109,c_33108,c_33106,c_33104,c_33103,c_29152,c_28981,c_28983,c_26037,c_26056,c_24652,c_24414,c_24143,c_24140,c_23831,c_23467,c_23359,c_23299,c_23295,c_22318,c_22276,c_22265,c_21414,c_21403,c_21370,c_21323,c_21307,c_21029,c_21015,c_20987,c_20932,c_20800,c_20798,c_20763,c_20762,c_20721,c_20545,c_20017,c_19565,c_19121,c_19078,c_19042,c_19001,c_18978,c_18977,c_18985,c_18941,c_18938,c_18935,c_18929,c_18928,c_18924,c_18922,c_18934,c_18813,c_18717,c_18714,c_17404,c_17225,c_16098,c_14969,c_14674,c_14471,c_14360,c_14108,c_12620,c_11672,c_11180,c_10378,c_10181,c_9688,c_9667,c_8839,c_8387,c_4696,c_3165,c_3161,c_3001,c_2835,c_2816,c_2336,c_2183,c_2100,c_1954,c_18971,c_484,c_483,c_481,c_479,c_477,c_475]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP346-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 14:31:56 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 15.37/3.28 % SZS status Started for theBenchmark.p
% 15.37/3.28 % SZS status Unsatisfiable for theBenchmark.p
% 15.37/3.28
% 15.37/3.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.37/3.28
% 15.37/3.28 % ------ iProver source info
% 15.37/3.28
% 15.37/3.28 % git: date: 2026-07-19 20:42:38 +0200
% 15.37/3.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.37/3.28 % git: non_committed_changes: false
% 15.37/3.28
% 15.37/3.28 % ------ Parsing...% successful
% 15.37/3.28
% 15.37/3.28
% 15.37/3.28 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.37/3.28
% 15.37/3.28 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 15.37/3.28
% 15.37/3.28 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.37/3.28
% 15.37/3.28 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 15.37/3.28 % ------ Proving...
% 15.37/3.28 % ------ Problem Properties
% 15.37/3.28
% 15.37/3.28 %
% 15.37/3.28 % clauses 55
% 15.37/3.28 % conjectures 40
% 15.37/3.28 % EPR 36
% 15.37/3.28 % Horn 19
% 15.37/3.28 % unary 15
% 15.37/3.28 % binary 35
% 15.37/3.28 % lits 105
% 15.37/3.28 % lits eq 97
% 15.37/3.28 % fd_pure 0
% 15.37/3.28 % fd_pseudo 0
% 15.37/3.28 % fd_cond 0
% 15.37/3.28 % fd_pseudo_cond 0
% 15.37/3.28 % AC symbols 0
% 15.37/3.28
% 15.37/3.28 % ------ Schedule dynamic 5 is on
% 15.37/3.28
% 15.37/3.28 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 15.37/3.28
% 15.37/3.28
% 15.37/3.28 % ------
% 15.37/3.28 % Current options:
% 15.37/3.28 % ------
% 15.37/3.28
% 15.37/3.28
% 15.37/3.28 %
% 15.37/3.28
% 15.37/3.28 % ------ Proving...
% 15.37/3.28 %
% 15.37/3.28
% 15.37/3.28 % SZS status Unsatisfiable for theBenchmark.p
% 15.37/3.28
% 15.37/3.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 15.37/3.29
% 15.37/3.29
%------------------------------------------------------------------------------