%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP342-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:25:59 PM UTC 2025
% Result : Unsatisfiable 22.95s 9.15s
% Output : CNFRefutation 23.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 33
% Syntax : Number of formulae : 539 ( 447 unt; 0 typ; 0 def)
% Number of atoms : 753 ( 727 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 446 ( 232 ~; 214 |; 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 : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 249 ( 249 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( inverse(X3) != sk_c8 )
| ( multiply(X3,sk_c7) != sk_c8 )
| ( inverse(X4) != sk_c7 )
| ( multiply(X4,sk_c6) != sk_c7 )
| ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( multiply(X2,X1) != sk_c8 )
| ( inverse(X2) != X1 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( multiply(X5,sk_c8) != sk_c6 )
| ( inverse(X5) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c3,sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c3,sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c3,sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_66,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_20967,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_54,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_85,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_89,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_21027,plain,
! [X_220,Y_221,Z_222] : ( multiply(multiply(X_220,Y_221),Z_222) = multiply(X_220,multiply(Y_221,Z_222)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_21069,plain,
! [Z_222] : ( multiply(sk_c7,multiply(sk_c2,Z_222)) = multiply(identity,Z_222) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_21027]) ).
tff(c_21111,plain,
! [Z_224] : ( multiply(sk_c7,multiply(sk_c2,Z_224)) = Z_224 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21069]) ).
tff(c_21123,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20967,c_21111]) ).
tff(c_149,plain,
! [X_13,Y_14,Z_15] : ( multiply(multiply(X_13,Y_14),Z_15) = multiply(X_13,multiply(Y_14,Z_15)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_179,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_149]) ).
tff(c_189,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_237,plain,
! [X_18,Z_19] : ( multiply(inverse(X_18),multiply(X_18,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_1742,plain,
! [X_45,Z_46] : ( multiply(inverse(inverse(X_45)),Z_46) = multiply(X_45,Z_46) ),
inference(superposition,[status(thm),theory(equality)],[c_189,c_237]) ).
tff(c_1763,plain,
! [X_45] : ( multiply(X_45,inverse(X_45)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_1742,c_4]) ).
tff(c_116,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_176,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_149]) ).
tff(c_214,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c2,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_176]) ).
tff(c_226,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_116,c_214]) ).
tff(c_255,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_226,c_237]) ).
tff(c_12,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_111,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_276,plain,
multiply(inverse(sk_c7),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_111,c_237]) ).
tff(c_899,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_255,c_276]) ).
tff(c_36,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_122,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_24,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_98,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_102,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_173,plain,
! [Z_15] : ( multiply(sk_c8,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_149]) ).
tff(c_191,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c1,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_173]) ).
tff(c_203,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_122,c_191]) ).
tff(c_913,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_899,c_899,c_203]) ).
tff(c_920,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_226,c_913]) ).
tff(c_1609,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_920,c_920,c_255]) ).
tff(c_1616,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1609]) ).
tff(c_1644,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1616,c_920]) ).
tff(c_291,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_237]) ).
tff(c_1749,plain,
! [X_45] : ( multiply(X_45,identity) = X_45 ),
inference(superposition,[status(thm),theory(equality)],[c_1742,c_291]) ).
tff(c_397,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_255,c_276]) ).
tff(c_410,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_397,c_397,c_203]) ).
tff(c_416,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_226,c_410]) ).
tff(c_453,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_416,c_416,c_255]) ).
tff(c_460,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_453]) ).
tff(c_470,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_460,c_416]) ).
tff(c_68,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_303,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( multiply(sk_c8,sk_c6) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_111,c_68]) ).
tff(c_304,plain,
multiply(sk_c8,sk_c6) != sk_c7,
inference(splitLeft,[status(thm)],[c_303]) ).
tff(c_409,plain,
multiply(sk_c7,sk_c6) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_397,c_304]) ).
tff(c_565,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_470,c_2,c_470,c_460,c_409]) ).
tff(c_567,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(splitRight,[status(thm)],[c_303]) ).
tff(c_571,plain,
multiply(inverse(sk_c8),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_567,c_189]) ).
tff(c_910,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_899,c_571]) ).
tff(c_919,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_910]) ).
tff(c_941,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_919,c_920]) ).
tff(c_1051,plain,
! [X_30,Z_31] : ( multiply(inverse(inverse(X_30)),Z_31) = multiply(X_30,Z_31) ),
inference(superposition,[status(thm),theory(equality)],[c_237,c_189]) ).
tff(c_1058,plain,
! [X_30] : ( multiply(X_30,identity) = X_30 ),
inference(superposition,[status(thm),theory(equality)],[c_1051,c_291]) ).
tff(c_261,plain,
multiply(inverse(sk_c8),sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_203,c_237]) ).
tff(c_681,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_571,c_261]) ).
tff(c_566,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_303]) ).
tff(c_625,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_566]) ).
tff(c_741,plain,
! [X5_26] :
( ( inverse(X5_26) != sk_c6 )
| ( multiply(X5_26,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_681,c_681,c_625]) ).
tff(c_758,plain,
( ( inverse(sk_c2) != sk_c6 )
| ( sk_c7 != sk_c6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_116,c_741]) ).
tff(c_769,plain,
( ( sk_c7 != sk_c6 )
| ( sk_c7 != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_85,c_758]) ).
tff(c_784,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_769]) ).
tff(c_685,plain,
multiply(sk_c6,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_681,c_567]) ).
tff(c_170,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c8,Z_15)) = multiply(sk_c6,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_111,c_149]) ).
tff(c_799,plain,
! [Z_27] : ( multiply(sk_c7,multiply(sk_c6,Z_27)) = multiply(sk_c6,Z_27) ),
inference(demodulation,[status(thm),theory(equality)],[c_681,c_170]) ).
tff(c_817,plain,
multiply(sk_c7,sk_c7) = multiply(sk_c6,sk_c6),
inference(superposition,[status(thm),theory(equality)],[c_685,c_799]) ).
tff(c_822,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_685,c_226,c_817]) ).
tff(c_824,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_784,c_822]) ).
tff(c_826,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_769]) ).
tff(c_825,plain,
sk_c7 != sk_c6,
inference(splitRight,[status(thm)],[c_769]) ).
tff(c_842,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_826,c_825]) ).
tff(c_843,plain,
! [X2_9,X4_10,X3_7] :
( ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_566]) ).
tff(c_926,plain,
! [X2_9,X4_10,X3_7] :
( ( multiply(inverse(X2_9),sk_c7) != sk_c7 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c7 )
| ( inverse(X3_7) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_899,c_899,c_899,c_899,c_843]) ).
tff(c_927,plain,
! [X3_7] :
( ( multiply(X3_7,sk_c7) != sk_c7 )
| ( inverse(X3_7) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_926]) ).
tff(c_1604,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_941,c_1058,c_941,c_941,c_927]) ).
tff(c_294,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_237]) ).
tff(c_918,plain,
inverse(sk_c1) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_899,c_98]) ).
tff(c_975,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_941,c_918]) ).
tff(c_979,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_975,c_291]) ).
tff(c_988,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_294,c_979]) ).
tff(c_990,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_988,c_975]) ).
tff(c_1606,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1604,c_990]) ).
tff(c_1607,plain,
! [X4_10,X2_9] :
( ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c7 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_926]) ).
tff(c_18835,plain,
! [X4_10,X2_9] :
( ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1763,c_1644,c_1749,c_1644,c_1644,c_1644,c_1749,c_1644,c_1616,c_1607]) ).
tff(c_18836,plain,
! [X2_9] : ( inverse(X2_9) != identity ),
inference(splitLeft,[status(thm)],[c_18835]) ).
tff(c_1660,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1644,c_918]) ).
tff(c_1664,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_1660,c_291]) ).
tff(c_1673,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_294,c_1664]) ).
tff(c_1675,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1673,c_1660]) ).
tff(c_18838,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18836,c_1675]) ).
tff(c_18840,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_18835]) ).
tff(c_18842,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18840,c_1675]) ).
tff(c_18844,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_32,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_18889,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_18844,c_32]) ).
tff(c_40,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_18877,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_18844,c_40]) ).
tff(c_42,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_18859,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_18844,c_42]) ).
tff(c_18863,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_18859,c_4]) ).
tff(c_18905,plain,
! [X_186,Y_187,Z_188] : ( multiply(multiply(X_186,Y_187),Z_188) = multiply(X_186,multiply(Y_187,Z_188)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18932,plain,
! [Z_188] : ( multiply(sk_c8,multiply(sk_c5,Z_188)) = multiply(identity,Z_188) ),
inference(superposition,[status(thm),theory(equality)],[c_18863,c_18905]) ).
tff(c_19506,plain,
! [Z_201] : ( multiply(sk_c8,multiply(sk_c5,Z_201)) = Z_201 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18932]) ).
tff(c_19518,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_18877,c_19506]) ).
tff(c_19522,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_18889,c_19518]) ).
tff(c_38,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_18882,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_18844,c_38]) ).
tff(c_19527,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_19522,c_18882]) ).
tff(c_18843,plain,
inverse(sk_c3) = sk_c4,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_34,plain,
( ( multiply(sk_c3,sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_18899,plain,
multiply(sk_c3,sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_18844,c_34]) ).
tff(c_19525,plain,
multiply(sk_c3,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_19522,c_18899]) ).
tff(c_18950,plain,
! [X_2,Z_188] : ( multiply(inverse(X_2),multiply(X_2,Z_188)) = multiply(identity,Z_188) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18905]) ).
tff(c_19601,plain,
! [X_202,Z_203] : ( multiply(inverse(X_202),multiply(X_202,Z_203)) = Z_203 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18950]) ).
tff(c_19631,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_19525,c_19601]) ).
tff(c_19679,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_19527,c_18843,c_19631]) ).
tff(c_19526,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_19522,c_18889]) ).
tff(c_19628,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_19526,c_19601]) ).
tff(c_19678,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19628]) ).
tff(c_18947,plain,
! [Z_188] : ( multiply(sk_c7,multiply(sk_c2,Z_188)) = multiply(identity,Z_188) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_18905]) ).
tff(c_19480,plain,
! [Z_200] : ( multiply(sk_c7,multiply(sk_c2,Z_200)) = Z_200 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18947]) ).
tff(c_19495,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_116,c_19480]) ).
tff(c_19685,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19678,c_19495]) ).
tff(c_19857,plain,
multiply(sk_c4,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19679,c_19679,c_19685]) ).
tff(c_19696,plain,
multiply(sk_c3,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_19679,c_19525]) ).
tff(c_18962,plain,
! [X_2,Z_188] : ( multiply(inverse(X_2),multiply(X_2,Z_188)) = Z_188 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18950]) ).
tff(c_19876,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_19696,c_18962]) ).
tff(c_19882,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19857,c_18843,c_19876]) ).
tff(c_19533,plain,
multiply(sk_c7,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19522,c_102]) ).
tff(c_19697,plain,
multiply(sk_c4,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19679,c_19533]) ).
tff(c_19888,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_19882,c_19697]) ).
tff(c_19995,plain,
sk_c1 = identity,
inference(superposition,[status(thm),theory(equality)],[c_19888,c_2]) ).
tff(c_19531,plain,
multiply(sk_c1,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_19522,c_18844]) ).
tff(c_19695,plain,
multiply(sk_c1,sk_c4) != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_19679,c_19679,c_19531]) ).
tff(c_19982,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_19882,c_19882,c_19695]) ).
tff(c_20005,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_19995,c_19982]) ).
tff(c_20010,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20005]) ).
tff(c_20012,plain,
multiply(sk_c2,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_56,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_20062,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_20012,c_56]) ).
tff(c_64,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_20068,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_20012,c_64]) ).
tff(c_20011,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_20016,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20011,c_4]) ).
tff(c_20079,plain,
! [X_205,Y_206,Z_207] : ( multiply(multiply(X_205,Y_206),Z_207) = multiply(X_205,multiply(Y_206,Z_207)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20112,plain,
! [Z_207] : ( multiply(sk_c8,multiply(sk_c5,Z_207)) = multiply(identity,Z_207) ),
inference(superposition,[status(thm),theory(equality)],[c_20016,c_20079]) ).
tff(c_20540,plain,
! [Z_216] : ( multiply(sk_c8,multiply(sk_c5,Z_216)) = Z_216 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20112]) ).
tff(c_20552,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_20068,c_20540]) ).
tff(c_20556,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_20062,c_20552]) ).
tff(c_58,plain,
( ( multiply(sk_c3,sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_20073,plain,
multiply(sk_c3,sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20012,c_58]) ).
tff(c_60,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_20024,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_20012,c_60]) ).
tff(c_20028,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20024,c_4]) ).
tff(c_20109,plain,
! [Z_207] : ( multiply(sk_c4,multiply(sk_c3,Z_207)) = multiply(identity,Z_207) ),
inference(superposition,[status(thm),theory(equality)],[c_20028,c_20079]) ).
tff(c_20174,plain,
! [Z_210] : ( multiply(sk_c4,multiply(sk_c3,Z_210)) = Z_210 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20109]) ).
tff(c_20186,plain,
multiply(sk_c4,sk_c8) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_20073,c_20174]) ).
tff(c_20558,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_20556,c_20186]) ).
tff(c_62,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_20053,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20012,c_62]) ).
tff(c_20564,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_20556,c_20053]) ).
tff(c_20631,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_20558,c_20564]) ).
tff(c_20633,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_20631,c_20558]) ).
tff(c_20124,plain,
! [X_2,Z_207] : ( multiply(inverse(X_2),multiply(X_2,Z_207)) = multiply(identity,Z_207) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20079]) ).
tff(c_20136,plain,
! [X_2,Z_207] : ( multiply(inverse(X_2),multiply(X_2,Z_207)) = Z_207 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20124]) ).
tff(c_20805,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_20633,c_20136]) ).
tff(c_20812,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20805]) ).
tff(c_20643,plain,
inverse(sk_c2) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_20631,c_85]) ).
tff(c_20728,plain,
multiply(sk_c4,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20643,c_4]) ).
tff(c_20945,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20812,c_20728]) ).
tff(c_20563,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_20556,c_20062]) ).
tff(c_20632,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_20631,c_20631,c_20563]) ).
tff(c_20747,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20632,c_20136]) ).
tff(c_20753,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20747]) ).
tff(c_20641,plain,
multiply(sk_c2,sk_c6) != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_20631,c_20012]) ).
tff(c_20794,plain,
multiply(sk_c2,identity) != sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_20753,c_20641]) ).
tff(c_20953,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20945,c_20812,c_20794]) ).
tff(c_20955,plain,
multiply(sk_c7,sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_8,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_21010,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_20955,c_8]) ).
tff(c_16,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_21016,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_20955,c_16]) ).
tff(c_18,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_20980,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20955,c_18]) ).
tff(c_20984,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20980,c_4]) ).
tff(c_21054,plain,
! [Z_222] : ( multiply(sk_c8,multiply(sk_c5,Z_222)) = multiply(identity,Z_222) ),
inference(superposition,[status(thm),theory(equality)],[c_20984,c_21027]) ).
tff(c_21173,plain,
! [Z_227] : ( multiply(sk_c8,multiply(sk_c5,Z_227)) = Z_227 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21054]) ).
tff(c_21185,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21016,c_21173]) ).
tff(c_21189,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21010,c_21185]) ).
tff(c_21201,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21189,c_20955]) ).
tff(c_21207,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21123,c_21201]) ).
tff(c_21209,plain,
multiply(sk_c2,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_21242,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_21209,c_56]) ).
tff(c_21252,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_20955,c_16]) ).
tff(c_21208,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_21213,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21208,c_4]) ).
tff(c_21272,plain,
! [X_228,Y_229,Z_230] : ( multiply(multiply(X_228,Y_229),Z_230) = multiply(X_228,multiply(Y_229,Z_230)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_21302,plain,
! [Z_230] : ( multiply(sk_c8,multiply(sk_c5,Z_230)) = multiply(identity,Z_230) ),
inference(superposition,[status(thm),theory(equality)],[c_21213,c_21272]) ).
tff(c_21411,plain,
! [Z_235] : ( multiply(sk_c8,multiply(sk_c5,Z_235)) = Z_235 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21302]) ).
tff(c_21423,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21252,c_21411]) ).
tff(c_21427,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21242,c_21423]) ).
tff(c_10,plain,
( ( multiply(sk_c3,sk_c4) = sk_c8 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_21247,plain,
multiply(sk_c3,sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_20955,c_10]) ).
tff(c_20954,plain,
inverse(sk_c3) = sk_c4,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_20959,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20954,c_4]) ).
tff(c_21305,plain,
! [Z_230] : ( multiply(sk_c4,multiply(sk_c3,Z_230)) = multiply(identity,Z_230) ),
inference(superposition,[status(thm),theory(equality)],[c_20959,c_21272]) ).
tff(c_21366,plain,
! [Z_233] : ( multiply(sk_c4,multiply(sk_c3,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21305]) ).
tff(c_21378,plain,
multiply(sk_c4,sk_c8) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_21247,c_21366]) ).
tff(c_21430,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_21427,c_21378]) ).
tff(c_21314,plain,
! [X_2,Z_230] : ( multiply(inverse(X_2),multiply(X_2,Z_230)) = multiply(identity,Z_230) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21272]) ).
tff(c_21468,plain,
! [X_236,Z_237] : ( multiply(inverse(X_236),multiply(X_236,Z_237)) = Z_237 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21314]) ).
tff(c_21486,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_21430,c_21468]) ).
tff(c_21523,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21486]) ).
tff(c_21439,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21427,c_21208]) ).
tff(c_21528,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21523,c_21439]) ).
tff(c_21434,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21427,c_21252]) ).
tff(c_21590,plain,
multiply(sk_c5,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21523,c_21434]) ).
tff(c_21326,plain,
! [X_2,Z_230] : ( multiply(inverse(X_2),multiply(X_2,Z_230)) = Z_230 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21314]) ).
tff(c_21594,plain,
multiply(inverse(sk_c5),sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21590,c_21326]) ).
tff(c_21600,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21528,c_21594]) ).
tff(c_21440,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21427,c_20955]) ).
tff(c_21636,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21600,c_21523,c_2,c_21523,c_21440]) ).
tff(c_21638,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_20,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_21657,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_21638,c_20]) ).
tff(c_28,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_21688,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_21638,c_28]) ).
tff(c_30,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_21646,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_21647,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21638,c_21646]) ).
tff(c_21648,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_21653,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21648,c_4]) ).
tff(c_21707,plain,
! [X_239,Y_240,Z_241] : ( multiply(multiply(X_239,Y_240),Z_241) = multiply(X_239,multiply(Y_240,Z_241)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_21731,plain,
! [Z_241] : ( multiply(sk_c8,multiply(sk_c5,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_21653,c_21707]) ).
tff(c_21756,plain,
! [Z_242] : ( multiply(sk_c8,multiply(sk_c5,Z_242)) = Z_242 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21731]) ).
tff(c_21768,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_21688,c_21756]) ).
tff(c_21772,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21657,c_21768]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_21683,plain,
multiply(sk_c3,sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_21638,c_22]) ).
tff(c_22113,plain,
multiply(sk_c3,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_21683]) ).
tff(c_21637,plain,
inverse(sk_c3) = sk_c4,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_21642,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21637,c_4]) ).
tff(c_21734,plain,
! [Z_241] : ( multiply(sk_c4,multiply(sk_c3,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_21642,c_21707]) ).
tff(c_22175,plain,
! [Z_247] : ( multiply(sk_c4,multiply(sk_c3,Z_247)) = Z_247 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21734]) ).
tff(c_22187,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_22113,c_22175]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_21676,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_21638,c_26]) ).
tff(c_22114,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_21676]) ).
tff(c_22191,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_22187,c_22114]) ).
tff(c_22116,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_21657]) ).
tff(c_22201,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_22191,c_22191,c_22116]) ).
tff(c_21743,plain,
! [X_2,Z_241] : ( multiply(inverse(X_2),multiply(X_2,Z_241)) = multiply(identity,Z_241) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_21707]) ).
tff(c_23002,plain,
! [X_261,Z_262] : ( multiply(inverse(X_261),multiply(X_261,Z_262)) = Z_262 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21743]) ).
tff(c_23020,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22201,c_23002]) ).
tff(c_23054,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_23020]) ).
tff(c_21779,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_21676]) ).
tff(c_21778,plain,
multiply(sk_c3,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_21683]) ).
tff(c_21826,plain,
! [X_243,Z_244] : ( multiply(inverse(X_243),multiply(X_243,Z_244)) = Z_244 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21743]) ).
tff(c_21847,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_21778,c_21826]) ).
tff(c_21882,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_21779,c_21637,c_21847]) ).
tff(c_21885,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_21882,c_21882,c_21779]) ).
tff(c_21754,plain,
! [X_2,Z_241] : ( multiply(inverse(X_2),multiply(X_2,Z_241)) = Z_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21743]) ).
tff(c_21977,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_21885,c_21754]) ).
tff(c_21983,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21977]) ).
tff(c_21781,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_21657]) ).
tff(c_21957,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_21882,c_21882,c_21781]) ).
tff(c_21961,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_21957,c_21754]) ).
tff(c_21967,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_21961]) ).
tff(c_21774,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21657,c_68]) ).
tff(c_21775,plain,
multiply(sk_c7,sk_c8) != sk_c6,
inference(splitLeft,[status(thm)],[c_21774]) ).
tff(c_21803,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_21775]) ).
tff(c_21886,plain,
multiply(sk_c4,sk_c4) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21882,c_21882,c_21803]) ).
tff(c_22108,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21983,c_2,c_21983,c_21967,c_21886]) ).
tff(c_22110,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_21774]) ).
tff(c_22130,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_21772,c_22110]) ).
tff(c_22204,plain,
multiply(sk_c4,sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_22191,c_22191,c_22130]) ).
tff(c_23074,plain,
multiply(sk_c4,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23054,c_22204]) ).
tff(c_22202,plain,
multiply(sk_c3,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_22191,c_22113]) ).
tff(c_23090,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_22202,c_21754]) ).
tff(c_23099,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23074,c_21637,c_23090]) ).
tff(c_22207,plain,
sk_c8 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_22191,c_21772]) ).
tff(c_23110,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23099,c_22207]) ).
tff(c_23328,plain,
! [X_265,Z_266] : ( multiply(inverse(inverse(X_265)),Z_266) = multiply(X_265,Z_266) ),
inference(superposition,[status(thm),theory(equality)],[c_21754,c_23002]) ).
tff(c_23047,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23002]) ).
tff(c_23335,plain,
! [X_265] : ( multiply(X_265,identity) = X_265 ),
inference(superposition,[status(thm),theory(equality)],[c_23328,c_23047]) ).
tff(c_23366,plain,
! [X_265] : ( multiply(X_265,inverse(X_265)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23328]) ).
tff(c_22268,plain,
! [X_248,Z_249] : ( multiply(inverse(X_248),multiply(X_248,Z_249)) = Z_249 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_21743]) ).
tff(c_22566,plain,
! [X_251,Z_252] : ( multiply(inverse(inverse(X_251)),Z_252) = multiply(X_251,Z_252) ),
inference(superposition,[status(thm),theory(equality)],[c_21754,c_22268]) ).
tff(c_22316,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22268]) ).
tff(c_22573,plain,
! [X_251] : ( multiply(X_251,identity) = X_251 ),
inference(superposition,[status(thm),theory(equality)],[c_22566,c_22316]) ).
tff(c_22289,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22201,c_22268]) ).
tff(c_22324,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22289]) ).
tff(c_22344,plain,
multiply(sk_c4,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22324,c_22204]) ).
tff(c_22199,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_22191,c_22187]) ).
tff(c_22357,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22344,c_22199]) ).
tff(c_22366,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22357,c_22207]) ).
tff(c_22109,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_21774]) ).
tff(c_22214,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(X3_7,sk_c4) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c4 )
| ( inverse(X4_10) != sk_c4 )
| ( multiply(inverse(X2_9),sk_c4) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_22191,c_22191,c_22191,c_22191,c_22109]) ).
tff(c_22215,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_22214]) ).
tff(c_22956,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_22573,c_22366,c_22324,c_22366,c_22215]) ).
tff(c_22369,plain,
multiply(identity,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22357,c_21642]) ).
tff(c_22424,plain,
sk_c3 = identity,
inference(superposition,[status(thm),theory(equality)],[c_22369,c_2]) ).
tff(c_22370,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22357,c_21637]) ).
tff(c_22434,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22424,c_22370]) ).
tff(c_22958,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22956,c_22434]) ).
tff(c_22959,plain,
! [X2_9,X4_10,X3_7] :
( ( multiply(inverse(X2_9),sk_c4) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c4 )
| ( inverse(X4_10) != sk_c4 )
| ( multiply(X3_7,sk_c4) != sk_c8 )
| ( inverse(X3_7) != sk_c8 ) ),
inference(splitRight,[status(thm)],[c_22214]) ).
tff(c_46457,plain,
! [X2_9,X4_10,X3_7] :
( ( inverse(X2_9) != identity )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( identity != X3_7 )
| ( inverse(X3_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_23110,c_23335,c_23110,c_23099,c_23099,c_23335,c_23099,c_23054,c_23366,c_23110,c_23335,c_23110,c_23099,c_22959]) ).
tff(c_46459,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_46457]) ).
tff(c_22209,plain,
inverse(sk_c2) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_22191,c_85]) ).
tff(c_23109,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23099,c_22209]) ).
tff(c_23152,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23109,c_4]) ).
tff(c_23170,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_23152,c_21754]) ).
tff(c_23182,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_23170]) ).
tff(c_23186,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23182,c_23109]) ).
tff(c_46461,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46459,c_23186]) ).
tff(c_46462,plain,
! [X4_10,X2_9] :
( ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X2_9) != identity ) ),
inference(splitRight,[status(thm)],[c_46457]) ).
tff(c_46463,plain,
! [X2_9] : ( inverse(X2_9) != identity ),
inference(splitLeft,[status(thm)],[c_46462]) ).
tff(c_46465,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46463,c_23186]) ).
tff(c_47742,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_46462]) ).
tff(c_47744,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_47742,c_23186]) ).
tff(c_47746,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_44,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_47807,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_47746,c_44]) ).
tff(c_52,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_47779,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_47746,c_52]) ).
tff(c_47745,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_47750,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_47745,c_4]) ).
tff(c_47825,plain,
! [X_437,Y_438,Z_439] : ( multiply(multiply(X_437,Y_438),Z_439) = multiply(X_437,multiply(Y_438,Z_439)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_47858,plain,
! [Z_439] : ( multiply(sk_c8,multiply(sk_c5,Z_439)) = multiply(identity,Z_439) ),
inference(superposition,[status(thm),theory(equality)],[c_47750,c_47825]) ).
tff(c_48159,plain,
! [Z_445] : ( multiply(sk_c8,multiply(sk_c5,Z_445)) = Z_445 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47858]) ).
tff(c_48171,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_47779,c_48159]) ).
tff(c_48175,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_47807,c_48171]) ).
tff(c_46,plain,
( ( multiply(sk_c3,sk_c4) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_47773,plain,
multiply(sk_c3,sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_47746,c_46]) ).
tff(c_48,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_47758,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_47746,c_48]) ).
tff(c_47762,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_47758,c_4]) ).
tff(c_47855,plain,
! [Z_439] : ( multiply(sk_c4,multiply(sk_c3,Z_439)) = multiply(identity,Z_439) ),
inference(superposition,[status(thm),theory(equality)],[c_47762,c_47825]) ).
tff(c_47874,plain,
! [Z_440] : ( multiply(sk_c4,multiply(sk_c3,Z_440)) = Z_440 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47855]) ).
tff(c_47886,plain,
multiply(sk_c4,sk_c8) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_47773,c_47874]) ).
tff(c_48192,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_48175,c_47886]) ).
tff(c_50,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_47799,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_47746,c_50]) ).
tff(c_48194,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_48175,c_47799]) ).
tff(c_49002,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_48192,c_48194]) ).
tff(c_49010,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_49002,c_48192]) ).
tff(c_47861,plain,
! [X_2,Z_439] : ( multiply(inverse(X_2),multiply(X_2,Z_439)) = multiply(identity,Z_439) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_47825]) ).
tff(c_47872,plain,
! [X_2,Z_439] : ( multiply(inverse(X_2),multiply(X_2,Z_439)) = Z_439 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47861]) ).
tff(c_49124,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_49010,c_47872]) ).
tff(c_49130,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_49124]) ).
tff(c_49140,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49130,c_49002]) ).
tff(c_49034,plain,
! [X_462,Z_463] : ( multiply(inverse(X_462),multiply(X_462,Z_463)) = Z_463 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47861]) ).
tff(c_49301,plain,
! [X_466,Z_467] : ( multiply(inverse(inverse(X_466)),Z_467) = multiply(X_466,Z_467) ),
inference(superposition,[status(thm),theory(equality)],[c_47872,c_49034]) ).
tff(c_49067,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_49034]) ).
tff(c_49308,plain,
! [X_466] : ( multiply(X_466,identity) = X_466 ),
inference(superposition,[status(thm),theory(equality)],[c_49301,c_49067]) ).
tff(c_48193,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_48175,c_47807]) ).
tff(c_49012,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_49002,c_49002,c_48193]) ).
tff(c_49212,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49130,c_2,c_49130,c_49012]) ).
tff(c_49322,plain,
! [X_466] : ( multiply(X_466,inverse(X_466)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_49301,c_4]) ).
tff(c_48299,plain,
! [X_447,Z_448] : ( multiply(inverse(X_447),multiply(X_447,Z_448)) = Z_448 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47861]) ).
tff(c_48595,plain,
! [X_452,Z_453] : ( multiply(inverse(inverse(X_452)),Z_453) = multiply(X_452,Z_453) ),
inference(superposition,[status(thm),theory(equality)],[c_47872,c_48299]) ).
tff(c_48335,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_48299]) ).
tff(c_48602,plain,
! [X_452] : ( multiply(X_452,identity) = X_452 ),
inference(superposition,[status(thm),theory(equality)],[c_48595,c_48335]) ).
tff(c_48252,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_48192,c_48194]) ).
tff(c_48269,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_48252,c_48192]) ).
tff(c_48401,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_48269,c_47872]) ).
tff(c_48407,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_48401]) ).
tff(c_48417,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48407,c_48252]) ).
tff(c_47900,plain,
! [Z_441] : ( multiply(sk_c8,multiply(sk_c5,Z_441)) = Z_441 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47858]) ).
tff(c_47912,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_47779,c_47900]) ).
tff(c_47916,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_47807,c_47912]) ).
tff(c_47919,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_47916,c_47886]) ).
tff(c_48035,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_47919,c_47872]) ).
tff(c_48041,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_48035]) ).
tff(c_47920,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_47916,c_47807]) ).
tff(c_47993,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_47920,c_47872]) ).
tff(c_47999,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_47993]) ).
tff(c_47898,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_47807,c_68]) ).
tff(c_47899,plain,
multiply(sk_c7,sk_c8) != sk_c6,
inference(splitLeft,[status(thm)],[c_47898]) ).
tff(c_47918,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_47916,c_47899]) ).
tff(c_48149,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_48041,c_2,c_48041,c_47999,c_47918]) ).
tff(c_48151,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_47898]) ).
tff(c_48191,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_48175,c_48151]) ).
tff(c_48343,plain,
multiply(sk_c4,sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_48252,c_48252,c_48191]) ).
tff(c_48198,plain,
multiply(sk_c3,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_48175,c_47773]) ).
tff(c_48271,plain,
multiply(sk_c3,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_48252,c_48198]) ).
tff(c_48381,plain,
multiply(inverse(sk_c3),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_48271,c_47872]) ).
tff(c_48390,plain,
sk_c6 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_48343,c_47758,c_48381]) ).
tff(c_48410,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48407,c_48390]) ).
tff(c_48150,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_47898]) ).
tff(c_48236,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(X3_7,sk_c7) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c7 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c7 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_48175,c_48175,c_48175,c_48175,c_48175,c_48175,c_48150]) ).
tff(c_48237,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_48236]) ).
tff(c_48975,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_48602,c_48417,c_48410,c_48417,c_48237]) ).
tff(c_47787,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_48196,plain,
inverse(sk_c1) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_48175,c_47787]) ).
tff(c_48273,plain,
inverse(sk_c1) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_48252,c_48196]) ).
tff(c_48295,plain,
multiply(sk_c4,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_48273,c_4]) ).
tff(c_48467,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_48407,c_48295]) ).
tff(c_48413,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48407,c_48273]) ).
tff(c_48482,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_48467,c_48413]) ).
tff(c_48977,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48975,c_48482]) ).
tff(c_48978,plain,
! [X2_9,X4_10,X3_7] :
( ( multiply(inverse(X2_9),sk_c7) != sk_c7 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c7 )
| ( inverse(X3_7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_48236]) ).
tff(c_56728,plain,
! [X2_9,X4_10,X3_7] :
( ( inverse(X2_9) != identity )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( identity != X3_7 )
| ( inverse(X3_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_49140,c_49308,c_49140,c_49140,c_49140,c_49308,c_49212,c_49140,c_49322,c_49140,c_49308,c_49140,c_49140,c_48978]) ).
tff(c_56730,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_56728]) ).
tff(c_49015,plain,
inverse(sk_c1) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_49002,c_48196]) ).
tff(c_49081,plain,
multiply(sk_c4,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49015,c_4]) ).
tff(c_49194,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_49130,c_49081]) ).
tff(c_49136,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49130,c_49015]) ).
tff(c_49199,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_49194,c_49136]) ).
tff(c_56732,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56730,c_49199]) ).
tff(c_56733,plain,
! [X4_10,X2_9] :
( ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X2_9) != identity ) ),
inference(splitRight,[status(thm)],[c_56728]) ).
tff(c_56734,plain,
! [X2_9] : ( inverse(X2_9) != identity ),
inference(splitLeft,[status(thm)],[c_56733]) ).
tff(c_56736,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56734,c_49199]) ).
tff(c_56739,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_56733]) ).
tff(c_56741,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_56739,c_49199]) ).
tff(c_56743,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_56748,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_56743,c_20]) ).
tff(c_56772,plain,
! [X_552,Y_553,Z_554] : ( multiply(multiply(X_552,Y_553),Z_554) = multiply(X_552,multiply(Y_553,Z_554)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_56802,plain,
! [Z_554] : ( multiply(sk_c8,multiply(sk_c5,Z_554)) = multiply(identity,Z_554) ),
inference(superposition,[status(thm),theory(equality)],[c_47750,c_56772]) ).
tff(c_56840,plain,
! [Z_556] : ( multiply(sk_c8,multiply(sk_c5,Z_556)) = Z_556 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56802]) ).
tff(c_56852,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_47779,c_56840]) ).
tff(c_56856,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56748,c_56852]) ).
tff(c_56742,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_57187,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56742]) ).
tff(c_57190,plain,
multiply(sk_c3,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_47773]) ).
tff(c_56805,plain,
! [X_2,Z_554] : ( multiply(inverse(X_2),multiply(X_2,Z_554)) = multiply(identity,Z_554) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_56772]) ).
tff(c_57906,plain,
! [X_573,Z_574] : ( multiply(inverse(X_573),multiply(X_573,Z_574)) = Z_574 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56805]) ).
tff(c_57930,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_57190,c_57906]) ).
tff(c_57965,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_57187,c_47758,c_57930]) ).
tff(c_56799,plain,
! [Z_554] : ( multiply(sk_c4,multiply(sk_c3,Z_554)) = multiply(identity,Z_554) ),
inference(superposition,[status(thm),theory(equality)],[c_47762,c_56772]) ).
tff(c_56817,plain,
! [Z_555] : ( multiply(sk_c4,multiply(sk_c3,Z_555)) = Z_555 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56799]) ).
tff(c_56829,plain,
multiply(sk_c4,sk_c8) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_47773,c_56817]) ).
tff(c_57185,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56829]) ).
tff(c_58036,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_57965,c_57185]) ).
tff(c_56815,plain,
! [X_2,Z_554] : ( multiply(inverse(X_2),multiply(X_2,Z_554)) = Z_554 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56805]) ).
tff(c_58040,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_58036,c_56815]) ).
tff(c_58046,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_58040]) ).
tff(c_58053,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_58046,c_57965]) ).
tff(c_58208,plain,
! [X_578,Z_579] : ( multiply(inverse(inverse(X_578)),Z_579) = multiply(X_578,Z_579) ),
inference(superposition,[status(thm),theory(equality)],[c_57906,c_56815]) ).
tff(c_57957,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_57906]) ).
tff(c_58215,plain,
! [X_578] : ( multiply(X_578,identity) = X_578 ),
inference(superposition,[status(thm),theory(equality)],[c_58208,c_57957]) ).
tff(c_57186,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56748]) ).
tff(c_57927,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_57186,c_57906]) ).
tff(c_57964,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57927]) ).
tff(c_58229,plain,
! [X_578] : ( multiply(X_578,inverse(X_578)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_58208,c_4]) ).
tff(c_57268,plain,
! [X_561,Z_562] : ( multiply(inverse(X_561),multiply(X_561,Z_562)) = Z_562 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56805]) ).
tff(c_57584,plain,
! [X_566,Z_567] : ( multiply(inverse(inverse(X_566)),Z_567) = multiply(X_566,Z_567) ),
inference(superposition,[status(thm),theory(equality)],[c_57268,c_56815]) ).
tff(c_57307,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_57268]) ).
tff(c_57595,plain,
! [X_566] : ( multiply(X_566,identity) = X_566 ),
inference(superposition,[status(thm),theory(equality)],[c_57584,c_57307]) ).
tff(c_57228,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_57185,c_57187]) ).
tff(c_57230,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_57228,c_57185]) ).
tff(c_57331,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_57230,c_56815]) ).
tff(c_57337,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57331]) ).
tff(c_57387,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57337,c_57228]) ).
tff(c_56863,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56742]) ).
tff(c_56866,plain,
multiply(sk_c3,sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_47773]) ).
tff(c_56914,plain,
! [X_557,Z_558] : ( multiply(inverse(X_557),multiply(X_557,Z_558)) = Z_558 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_56805]) ).
tff(c_56938,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_56866,c_56914]) ).
tff(c_56967,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_56863,c_47758,c_56938]) ).
tff(c_56861,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56829]) ).
tff(c_57007,plain,
multiply(sk_c4,sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_56967,c_56861]) ).
tff(c_57011,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_57007,c_56815]) ).
tff(c_57017,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57011]) ).
tff(c_57025,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57017,c_56967]) ).
tff(c_56862,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56748]) ).
tff(c_57137,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57025,c_2,c_57025,c_56862]) ).
tff(c_56858,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_56748,c_68]) ).
tff(c_56859,plain,
multiply(sk_c7,sk_c8) != sk_c6,
inference(splitLeft,[status(thm)],[c_56858]) ).
tff(c_56888,plain,
multiply(sk_c7,sk_c7) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56859]) ).
tff(c_56972,plain,
multiply(sk_c4,sk_c4) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_56967,c_56967,c_56888]) ).
tff(c_57181,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_57137,c_57017,c_2,c_57017,c_56972]) ).
tff(c_57183,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_56858]) ).
tff(c_57204,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_57183]) ).
tff(c_57231,plain,
multiply(sk_c4,sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_57228,c_57228,c_57204]) ).
tff(c_57327,plain,
sk_c6 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_57230,c_57231]) ).
tff(c_57380,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57337,c_57327]) ).
tff(c_57182,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(X3_7,sk_c7) != sk_c8 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c8 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(X5_6,sk_c8) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_56858]) ).
tff(c_57212,plain,
! [X3_7,X4_10,X2_9,X5_6] :
( ( multiply(X3_7,sk_c7) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(inverse(X2_9),sk_c7) != sk_c7 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c7 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_56856,c_56856,c_56856,c_56856,c_56856,c_57182]) ).
tff(c_57213,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c7 )
| ( multiply(X5_6,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_57212]) ).
tff(c_57862,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_57595,c_57387,c_57380,c_57387,c_57213]) ).
tff(c_57390,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57337,c_47758]) ).
tff(c_57415,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_57390,c_4]) ).
tff(c_57422,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_57415,c_56815]) ).
tff(c_57434,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_57422]) ).
tff(c_57438,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_57434,c_57390]) ).
tff(c_57864,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_57862,c_57438]) ).
tff(c_57865,plain,
! [X2_9,X4_10,X3_7] :
( ( multiply(inverse(X2_9),sk_c7) != sk_c7 )
| ( multiply(X2_9,inverse(X2_9)) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c7 )
| ( inverse(X3_7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_57212]) ).
tff(c_65655,plain,
! [X2_9,X4_10,X3_7] :
( ( inverse(X2_9) != identity )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( identity != X3_7 )
| ( inverse(X3_7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_58053,c_58215,c_58053,c_58053,c_58053,c_58215,c_58053,c_57964,c_58229,c_58053,c_58215,c_58053,c_58053,c_57865]) ).
tff(c_65657,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_65655]) ).
tff(c_57192,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_56856,c_47745]) ).
tff(c_57978,plain,
inverse(sk_c5) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_57965,c_57192]) ).
tff(c_58032,plain,
multiply(sk_c4,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_57978,c_4]) ).
tff(c_58099,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_58046,c_58032]) ).
tff(c_58051,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_58046,c_57978]) ).
tff(c_58104,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_58099,c_58051]) ).
tff(c_65659,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65657,c_58104]) ).
tff(c_65660,plain,
! [X4_10,X2_9] :
( ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X2_9) != identity ) ),
inference(splitRight,[status(thm)],[c_65655]) ).
tff(c_65661,plain,
! [X2_9] : ( inverse(X2_9) != identity ),
inference(splitLeft,[status(thm)],[c_65660]) ).
tff(c_65663,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65661,c_58104]) ).
tff(c_65666,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_65660]) ).
tff(c_65668,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_65666,c_58104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP342-1 : TPTP v9.0.0. Released v2.5.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.35 % Computer : n021.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Mon Apr 7 21:43:13 EDT 2025
% 0.12/0.35 % CPUTime :
% 22.95/9.15 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.08/9.22
% 23.08/9.22 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------