%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP346-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n004.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:26:00 PM UTC 2025
% Result : Unsatisfiable 24.65s 12.49s
% Output : CNFRefutation 24.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 30
% Syntax : Number of formulae : 544 ( 454 unt; 0 typ; 0 def)
% Number of atoms : 778 ( 750 equ)
% Maximal formula atoms : 12 ( 1 avg)
% Number of connectives : 503 ( 269 ~; 234 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 268 ( 268 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > 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(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_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
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_155,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_203,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X3) != sk_c7 )
| ( multiply(X3,sk_c6) != sk_c7 )
| ( inverse(X4) != sk_c6 )
| ( multiply(X4,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( inverse(X1) != sk_c6 )
| ( multiply(X2,sk_c7) != sk_c5 )
| ( inverse(X2) != sk_c7 ) ),
file(unknown,unknown) ).
tff(f_158,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_161,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( inverse(sk_c3) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c2,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c4,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c1,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_37896,plain,
! [X_300,Y_301,Z_302] : ( multiply(multiply(X_300,Y_301),Z_302) = multiply(X_300,multiply(Y_301,Z_302)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_37935,plain,
! [X_2,Z_302] : ( multiply(inverse(X_2),multiply(X_2,Z_302)) = multiply(identity,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_37896]) ).
tff(c_39029,plain,
! [X_324,Z_325] : ( multiply(inverse(X_324),multiply(X_324,Z_325)) = Z_325 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37935]) ).
tff(c_37947,plain,
! [X_2,Z_302] : ( multiply(inverse(X_2),multiply(X_2,Z_302)) = Z_302 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37935]) ).
tff(c_39240,plain,
! [X_327,Z_328] : ( multiply(inverse(inverse(X_327)),Z_328) = multiply(X_327,Z_328) ),
inference(superposition,[status(thm),theory(equality)],[c_39029,c_37947]) ).
tff(c_39083,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_39029]) ).
tff(c_39247,plain,
! [X_327] : ( multiply(X_327,identity) = X_327 ),
inference(superposition,[status(thm),theory(equality)],[c_39240,c_39083]) ).
tff(c_164,plain,
! [X_12,Y_13,Z_14] : ( multiply(multiply(X_12,Y_13),Z_14) = multiply(X_12,multiply(Y_13,Z_14)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_194,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_164]) ).
tff(c_204,plain,
! [X_2,Z_14] : ( multiply(inverse(X_2),multiply(X_2,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_194]) ).
tff(c_1390,plain,
! [X_37,Z_38] : ( multiply(inverse(X_37),multiply(X_37,Z_38)) = Z_38 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_194]) ).
tff(c_1513,plain,
! [X_40,Z_41] : ( multiply(inverse(inverse(X_40)),Z_41) = multiply(X_40,Z_41) ),
inference(superposition,[status(thm),theory(equality)],[c_204,c_1390]) ).
tff(c_1417,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1390]) ).
tff(c_1520,plain,
! [X_40] : ( multiply(X_40,identity) = X_40 ),
inference(superposition,[status(thm),theory(equality)],[c_1513,c_1417]) ).
tff(c_68,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_134,plain,
multiply(sk_c2,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_68]) ).
tff(c_62,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_95,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_99,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_95,c_4]) ).
tff(c_191,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_99,c_164]) ).
tff(c_848,plain,
! [Z_30] : ( multiply(sk_c6,multiply(sk_c2,Z_30)) = Z_30 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_191]) ).
tff(c_860,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_134,c_848]) ).
tff(c_44,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_129,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_26,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_108,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_112,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_108,c_4]) ).
tff(c_188,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_112,c_164]) ).
tff(c_803,plain,
! [Z_28] : ( multiply(sk_c7,multiply(sk_c1,Z_28)) = Z_28 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_188]) ).
tff(c_815,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_129,c_803]) ).
tff(c_20,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_123,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_185,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c7,Z_14)) = multiply(sk_c5,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_123,c_164]) ).
tff(c_841,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c5,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_815,c_185]) ).
tff(c_879,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_860,c_841]) ).
tff(c_888,plain,
! [X_31,Z_32] : ( multiply(inverse(X_31),multiply(X_31,Z_32)) = Z_32 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_194]) ).
tff(c_906,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_879,c_888]) ).
tff(c_961,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_906]) ).
tff(c_968,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_961,c_961,c_815]) ).
tff(c_976,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_968]) ).
tff(c_1019,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_976,c_976,c_860]) ).
tff(c_1025,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1019]) ).
tff(c_209,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_191]) ).
tff(c_221,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_134,c_209]) ).
tff(c_309,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_194]) ).
tff(c_345,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_221,c_309]) ).
tff(c_360,plain,
multiply(inverse(sk_c6),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_123,c_309]) ).
tff(c_480,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_345,c_360]) ).
tff(c_257,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_188]) ).
tff(c_272,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_129,c_257]) ).
tff(c_494,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_480,c_480,c_272]) ).
tff(c_504,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_221,c_494]) ).
tff(c_511,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_504,c_504,c_345]) ).
tff(c_519,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_511]) ).
tff(c_556,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_519,c_504]) ).
tff(c_78,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_207,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_123,c_78]) ).
tff(c_208,plain,
multiply(sk_c6,sk_c5) != sk_c7,
inference(splitLeft,[status(thm)],[c_207]) ).
tff(c_497,plain,
multiply(sk_c6,sk_c5) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_480,c_208]) ).
tff(c_793,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_556,c_2,c_556,c_519,c_497]) ).
tff(c_794,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(sk_c7) != sk_c5 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_207]) ).
tff(c_887,plain,
inverse(sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_794]) ).
tff(c_966,plain,
inverse(identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_961,c_887]) ).
tff(c_1054,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_1025,c_966]) ).
tff(c_974,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_961,c_112]) ).
tff(c_1076,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_974,c_204]) ).
tff(c_1088,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1076]) ).
tff(c_975,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_961,c_108]) ).
tff(c_1092,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1088,c_975]) ).
tff(c_1095,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1054,c_1092]) ).
tff(c_1097,plain,
inverse(sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_794]) ).
tff(c_1101,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1097,c_4]) ).
tff(c_1105,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1101,c_879]) ).
tff(c_1115,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1105,c_1097]) ).
tff(c_1131,plain,
multiply(identity,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1115,c_4]) ).
tff(c_1343,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_1131,c_2]) ).
tff(c_1355,plain,
multiply(identity,identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_1343,c_1343,c_815]) ).
tff(c_1361,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1355]) ).
tff(c_1187,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_1131,c_2]) ).
tff(c_819,plain,
! [Z_29] : ( multiply(sk_c6,multiply(sk_c7,Z_29)) = multiply(sk_c5,Z_29) ),
inference(superposition,[status(thm),theory(equality)],[c_123,c_164]) ).
tff(c_834,plain,
multiply(sk_c6,identity) = multiply(sk_c5,sk_c1),
inference(superposition,[status(thm),theory(equality)],[c_112,c_819]) ).
tff(c_1116,plain,
multiply(sk_c6,identity) = multiply(identity,sk_c1),
inference(demodulation,[status(thm),theory(equality)],[c_1105,c_834]) ).
tff(c_1122,plain,
multiply(sk_c6,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1116]) ).
tff(c_795,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_207]) ).
tff(c_1119,plain,
multiply(sk_c6,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_1105,c_795]) ).
tff(c_1172,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_1122,c_1119]) ).
tff(c_1208,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1187,c_1172]) ).
tff(c_1201,plain,
multiply(sk_c1,sk_c6) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_1172,c_129]) ).
tff(c_1279,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_2,c_1208,c_1201]) ).
tff(c_1096,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_794]) ).
tff(c_1162,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(sk_c7,identity) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != identity )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X4_7,identity) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1105,c_1105,c_1105,c_1096]) ).
tff(c_1163,plain,
multiply(sk_c7,identity) != sk_c6,
inference(splitLeft,[status(thm)],[c_1162]) ).
tff(c_1196,plain,
multiply(sk_c1,identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_1172,c_1163]) ).
tff(c_1334,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1279,c_2,c_1208,c_1196]) ).
tff(c_1335,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,identity) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != identity ) ),
inference(splitRight,[status(thm)],[c_1162]) ).
tff(c_28166,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( identity != X3_6 )
| ( inverse(X3_6) != identity )
| ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1520,c_1343,c_1343,c_1520,c_1361,c_1343,c_1361,c_1361,c_1520,c_1361,c_1343,c_1520,c_1361,c_1343,c_1335]) ).
tff(c_28168,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_28166]) ).
tff(c_1354,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1343,c_1115]) ).
tff(c_28170,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28168,c_1354]) ).
tff(c_28171,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( identity != X3_6 )
| ( inverse(X3_6) != identity ) ),
inference(splitRight,[status(thm)],[c_28166]) ).
tff(c_35537,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_28171]) ).
tff(c_35539,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35537,c_1354]) ).
tff(c_35540,plain,
! [X4_7,X1_8] :
( ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_28171]) ).
tff(c_35543,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_35540]) ).
tff(c_35545,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35543,c_1354]) ).
tff(c_35547,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_35540]) ).
tff(c_35549,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35547,c_1354]) ).
tff(c_35550,plain,
inverse(sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_35555,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_35550,c_4]) ).
tff(c_35551,plain,
multiply(sk_c2,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_68]) ).
tff(c_70,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_158]) ).
tff(c_35600,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_35551,c_70]) ).
tff(c_72,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_35565,plain,
inverse(sk_c3) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_35551,c_72]) ).
tff(c_35569,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_35565,c_4]) ).
tff(c_35626,plain,
! [X_248,Y_249,Z_250] : ( multiply(multiply(X_248,Y_249),Z_250) = multiply(X_248,multiply(Y_249,Z_250)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_35656,plain,
! [Z_250] : ( multiply(sk_c6,multiply(sk_c3,Z_250)) = multiply(identity,Z_250) ),
inference(superposition,[status(thm),theory(equality)],[c_35569,c_35626]) ).
tff(c_35873,plain,
! [Z_258] : ( multiply(sk_c6,multiply(sk_c3,Z_258)) = Z_258 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35656]) ).
tff(c_35885,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_35600,c_35873]) ).
tff(c_35889,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_123,c_35885]) ).
tff(c_35903,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_35889,c_123]) ).
tff(c_35906,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35555,c_35903]) ).
tff(c_35904,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35889,c_99]) ).
tff(c_35978,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35906,c_35904]) ).
tff(c_35901,plain,
multiply(sk_c2,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_35889,c_35551]) ).
tff(c_36074,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35978,c_35906,c_35906,c_35901]) ).
tff(c_36076,plain,
multiply(sk_c1,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_40,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_36113,plain,
inverse(sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_36076,c_40]) ).
tff(c_36117,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_36113,c_4]) ).
tff(c_42,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_36136,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_36076,c_42]) ).
tff(c_36075,plain,
inverse(sk_c3) = sk_c6,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_36080,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_36075,c_4]) ).
tff(c_36156,plain,
! [X_261,Y_262,Z_263] : ( multiply(multiply(X_261,Y_262),Z_263) = multiply(X_261,multiply(Y_262,Z_263)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_36192,plain,
! [Z_263] : ( multiply(sk_c6,multiply(sk_c3,Z_263)) = multiply(identity,Z_263) ),
inference(superposition,[status(thm),theory(equality)],[c_36080,c_36156]) ).
tff(c_36258,plain,
! [Z_266] : ( multiply(sk_c6,multiply(sk_c3,Z_266)) = Z_266 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36192]) ).
tff(c_36270,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_36136,c_36258]) ).
tff(c_36274,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_123,c_36270]) ).
tff(c_36312,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_36274,c_123]) ).
tff(c_36315,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36117,c_36312]) ).
tff(c_36322,plain,
multiply(identity,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36315,c_36117]) ).
tff(c_36375,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_36322,c_2]) ).
tff(c_36389,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36375,c_112]) ).
tff(c_36204,plain,
! [X_2,Z_263] : ( multiply(inverse(X_2),multiply(X_2,Z_263)) = multiply(identity,Z_263) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_36156]) ).
tff(c_36217,plain,
! [X_2,Z_263] : ( multiply(inverse(X_2),multiply(X_2,Z_263)) = Z_263 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36204]) ).
tff(c_36532,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_36389,c_36217]) ).
tff(c_36544,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_36532]) ).
tff(c_36310,plain,
multiply(sk_c1,sk_c5) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_36274,c_36076]) ).
tff(c_36492,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_36375,c_36315,c_36310]) ).
tff(c_36548,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_36544,c_36492]) ).
tff(c_36553,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36548]) ).
tff(c_36555,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_12,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_36568,plain,
inverse(sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_36555,c_12]) ).
tff(c_36572,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_36568,c_4]) ).
tff(c_66,plain,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_37053,plain,
multiply(sk_c2,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_37089,plain,
! [X_280,Y_281,Z_282] : ( multiply(multiply(X_280,Y_281),Z_282) = multiply(X_280,multiply(Y_281,Z_282)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_37131,plain,
! [Z_282] : ( multiply(sk_c6,multiply(sk_c2,Z_282)) = multiply(identity,Z_282) ),
inference(superposition,[status(thm),theory(equality)],[c_99,c_37089]) ).
tff(c_37164,plain,
! [Z_284] : ( multiply(sk_c6,multiply(sk_c2,Z_284)) = Z_284 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37131]) ).
tff(c_37176,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_37053,c_37164]) ).
tff(c_10,plain,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_37072,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_36555,c_10]) ).
tff(c_37122,plain,
! [Z_282] : ( multiply(sk_c5,multiply(sk_c7,Z_282)) = multiply(identity,Z_282) ),
inference(superposition,[status(thm),theory(equality)],[c_36572,c_37089]) ).
tff(c_37187,plain,
! [Z_285] : ( multiply(sk_c5,multiply(sk_c7,Z_285)) = Z_285 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37122]) ).
tff(c_37202,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_37072,c_37187]) ).
tff(c_37116,plain,
! [Z_282] : ( multiply(sk_c2,multiply(sk_c5,Z_282)) = multiply(sk_c6,Z_282) ),
inference(superposition,[status(thm),theory(equality)],[c_37053,c_37089]) ).
tff(c_37248,plain,
multiply(sk_c6,sk_c6) = multiply(sk_c2,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_37202,c_37116]) ).
tff(c_37254,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_37176,c_37053,c_37248]) ).
tff(c_37267,plain,
multiply(sk_c5,sk_c7) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_37254,c_36555]) ).
tff(c_37270,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_36572,c_37267]) ).
tff(c_36554,plain,
inverse(sk_c4) = sk_c7,
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_18,plain,
( ( multiply(sk_c4,sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_37063,plain,
multiply(sk_c4,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_36555,c_18]) ).
tff(c_37134,plain,
! [X_2,Z_282] : ( multiply(inverse(X_2),multiply(X_2,Z_282)) = multiply(identity,Z_282) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_37089]) ).
tff(c_37282,plain,
! [X_287,Z_288] : ( multiply(inverse(X_287),multiply(X_287,Z_288)) = Z_288 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37134]) ).
tff(c_37315,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_37063,c_37282]) ).
tff(c_37344,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_36554,c_37315]) ).
tff(c_37147,plain,
! [X_2,Z_282] : ( multiply(inverse(X_2),multiply(X_2,Z_282)) = Z_282 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37134]) ).
tff(c_37371,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_37344,c_37147]) ).
tff(c_37380,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36572,c_36568,c_37371]) ).
tff(c_37382,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37270,c_37380]) ).
tff(c_37383,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_36641,plain,
! [X_271,Y_272,Z_273] : ( multiply(multiply(X_271,Y_272),Z_273) = multiply(X_271,multiply(Y_272,Z_273)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_36674,plain,
! [Z_273] : ( multiply(sk_c5,multiply(sk_c7,Z_273)) = multiply(identity,Z_273) ),
inference(superposition,[status(thm),theory(equality)],[c_36572,c_36641]) ).
tff(c_36750,plain,
! [Z_276] : ( multiply(sk_c5,multiply(sk_c7,Z_276)) = Z_276 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36674]) ).
tff(c_36774,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_112,c_36750]) ).
tff(c_36559,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_36554,c_4]) ).
tff(c_36771,plain,
multiply(sk_c5,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_36559,c_36750]) ).
tff(c_36795,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_36774,c_36771]) ).
tff(c_36614,plain,
multiply(sk_c4,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_36555,c_18]) ).
tff(c_36836,plain,
multiply(sk_c1,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_36795,c_36614]) ).
tff(c_36620,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_36555,c_10]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_36626,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_36555,c_8]) ).
tff(c_36576,plain,
multiply(sk_c1,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_36804,plain,
! [Z_277] : ( multiply(sk_c1,multiply(sk_c6,Z_277)) = multiply(sk_c7,Z_277) ),
inference(superposition,[status(thm),theory(equality)],[c_36576,c_36641]) ).
tff(c_36825,plain,
multiply(sk_c7,sk_c5) = multiply(sk_c1,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_36626,c_36804]) ).
tff(c_36835,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36620,c_36825]) ).
tff(c_36855,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_36836,c_36835]) ).
tff(c_36879,plain,
multiply(sk_c5,sk_c7) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_36855,c_36555]) ).
tff(c_36882,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_36572,c_36879]) ).
tff(c_36683,plain,
! [Z_273] : ( multiply(sk_c7,multiply(sk_c1,Z_273)) = multiply(identity,Z_273) ),
inference(superposition,[status(thm),theory(equality)],[c_112,c_36641]) ).
tff(c_36700,plain,
! [Z_273] : ( multiply(sk_c7,multiply(sk_c1,Z_273)) = Z_273 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36683]) ).
tff(c_36859,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36836,c_36700]) ).
tff(c_36865,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36620,c_36859]) ).
tff(c_36944,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_36855,c_36865]) ).
tff(c_36848,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36835,c_36700]) ).
tff(c_37007,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_36944,c_36944,c_36855,c_36848]) ).
tff(c_36689,plain,
! [X_2,Z_273] : ( multiply(inverse(X_2),multiply(X_2,Z_273)) = multiply(identity,Z_273) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_36641]) ).
tff(c_36702,plain,
! [X_2,Z_273] : ( multiply(inverse(X_2),multiply(X_2,Z_273)) = Z_273 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36689]) ).
tff(c_37011,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_37007,c_36702]) ).
tff(c_37017,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_37011]) ).
tff(c_37019,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_36882,c_37017]) ).
tff(c_37021,plain,
multiply(sk_c1,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_37405,plain,
multiply(sk_c4,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_37021,c_46]) ).
tff(c_37420,plain,
! [X_289,Y_290,Z_291] : ( multiply(multiply(X_289,Y_290),Z_291) = multiply(X_289,multiply(Y_290,Z_291)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_37453,plain,
! [Z_291] : ( multiply(sk_c7,multiply(sk_c4,Z_291)) = multiply(identity,Z_291) ),
inference(superposition,[status(thm),theory(equality)],[c_36559,c_37420]) ).
tff(c_37545,plain,
! [Z_296] : ( multiply(sk_c7,multiply(sk_c4,Z_296)) = Z_296 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37453]) ).
tff(c_37557,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_37405,c_37545]) ).
tff(c_37561,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_37383,c_37557]) ).
tff(c_14,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_37394,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_36555,c_14]) ).
tff(c_37020,plain,
inverse(sk_c3) = sk_c6,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_37025,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37020,c_4]) ).
tff(c_37447,plain,
! [Z_291] : ( multiply(sk_c6,multiply(sk_c3,Z_291)) = multiply(identity,Z_291) ),
inference(superposition,[status(thm),theory(equality)],[c_37025,c_37420]) ).
tff(c_37505,plain,
! [Z_294] : ( multiply(sk_c6,multiply(sk_c3,Z_294)) = Z_294 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37447]) ).
tff(c_37517,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_37394,c_37505]) ).
tff(c_37564,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_37561,c_37517]) ).
tff(c_37462,plain,
! [X_2,Z_291] : ( multiply(inverse(X_2),multiply(X_2,Z_291)) = multiply(identity,Z_291) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_37420]) ).
tff(c_37475,plain,
! [X_2,Z_291] : ( multiply(inverse(X_2),multiply(X_2,Z_291)) = Z_291 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37462]) ).
tff(c_37691,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_37564,c_37475]) ).
tff(c_37697,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_37691]) ).
tff(c_37521,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_37517,c_36555]) ).
tff(c_37719,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_37697,c_37521]) ).
tff(c_37576,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_37561,c_108]) ).
tff(c_37598,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37576,c_4]) ).
tff(c_37804,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37697,c_37598]) ).
tff(c_37715,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37697,c_37576]) ).
tff(c_37805,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37804,c_37715]) ).
tff(c_37572,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_37561,c_36568]) ).
tff(c_37717,plain,
inverse(identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_37697,c_37572]) ).
tff(c_37810,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_37805,c_37717]) ).
tff(c_37812,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_37719,c_37810]) ).
tff(c_37814,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_24,plain,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_37853,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_37814,c_24]) ).
tff(c_37813,plain,
inverse(sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_37818,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37813,c_4]) ).
tff(c_37929,plain,
! [Z_302] : ( multiply(sk_c5,multiply(sk_c7,Z_302)) = multiply(identity,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_37818,c_37896]) ).
tff(c_38180,plain,
! [Z_307] : ( multiply(sk_c5,multiply(sk_c7,Z_307)) = Z_307 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37929]) ).
tff(c_38192,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_37853,c_38180]) ).
tff(c_39065,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_38192,c_39029]) ).
tff(c_39093,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_39065]) ).
tff(c_32,plain,
( ( multiply(sk_c4,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_37861,plain,
multiply(sk_c4,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_37814,c_32]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_37834,plain,
inverse(sk_c4) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_37814,c_34]) ).
tff(c_37838,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37834,c_4]) ).
tff(c_37923,plain,
! [Z_302] : ( multiply(sk_c7,multiply(sk_c4,Z_302)) = multiply(identity,Z_302) ),
inference(superposition,[status(thm),theory(equality)],[c_37838,c_37896]) ).
tff(c_38214,plain,
! [Z_308] : ( multiply(sk_c7,multiply(sk_c4,Z_308)) = Z_308 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37923]) ).
tff(c_38235,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_37861,c_38214]) ).
tff(c_38239,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_37853,c_38235]) ).
tff(c_37952,plain,
! [Z_303] : ( multiply(sk_c7,multiply(sk_c4,Z_303)) = Z_303 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37923]) ).
tff(c_37964,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_37861,c_37952]) ).
tff(c_37968,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_37853,c_37964]) ).
tff(c_37974,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_37968,c_37853]) ).
tff(c_38081,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_37974,c_37947]) ).
tff(c_38087,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_38081]) ).
tff(c_37979,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_37968,c_37813]) ).
tff(c_38040,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_37979,c_4]) ).
tff(c_38135,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38087,c_38040]) ).
tff(c_22,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_37867,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_37814,c_22]) ).
tff(c_37950,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_37867,c_37853,c_37813,c_78]) ).
tff(c_37951,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_37950]) ).
tff(c_37970,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_37968,c_37951]) ).
tff(c_38134,plain,
multiply(sk_c6,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_38087,c_37970]) ).
tff(c_38136,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_38135,c_38135,c_38134]) ).
tff(c_38151,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38136]) ).
tff(c_38153,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_37950]) ).
tff(c_38338,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_38239,c_38153]) ).
tff(c_39119,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_39093,c_39093,c_38338]) ).
tff(c_39127,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_39119]) ).
tff(c_38346,plain,
multiply(sk_c5,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38239,c_37818]) ).
tff(c_38418,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38346,c_38192]) ).
tff(c_38348,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_38239,c_37813]) ).
tff(c_38389,plain,
multiply(sk_c5,sk_c6) = identity,
inference(superposition,[status(thm),theory(equality)],[c_38348,c_4]) ).
tff(c_38444,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38418,c_38389]) ).
tff(c_38476,plain,
! [X_311,Z_312] : ( multiply(inverse(X_311),multiply(X_311,Z_312)) = Z_312 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37935]) ).
tff(c_38659,plain,
! [X_315,Z_316] : ( multiply(inverse(inverse(X_315)),Z_316) = multiply(X_315,Z_316) ),
inference(superposition,[status(thm),theory(equality)],[c_37947,c_38476]) ).
tff(c_38503,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_38476]) ).
tff(c_38666,plain,
! [X_315] : ( multiply(X_315,identity) = X_315 ),
inference(superposition,[status(thm),theory(equality)],[c_38659,c_38503]) ).
tff(c_38251,plain,
multiply(sk_c5,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38239,c_37818]) ).
tff(c_38280,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38251,c_38192]) ).
tff(c_38195,plain,
multiply(sk_c5,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_37838,c_38180]) ).
tff(c_38291,plain,
multiply(identity,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_38280,c_38195]) ).
tff(c_38292,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_38291]) ).
tff(c_38250,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38239,c_37834]) ).
tff(c_38298,plain,
inverse(identity) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38292,c_38250]) ).
tff(c_38253,plain,
inverse(sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_38239,c_37813]) ).
tff(c_38290,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38280,c_38253]) ).
tff(c_38152,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_37950]) ).
tff(c_38240,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_38152]) ).
tff(c_38311,plain,
! [X2_309] :
( ( inverse(X2_309) != sk_c6 )
| ( multiply(X2_309,sk_c6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_38280,c_38239,c_38239,c_38240]) ).
tff(c_38319,plain,
inverse(inverse(sk_c6)) != sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4,c_38311]) ).
tff(c_38325,plain,
inverse(identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_38290,c_38319]) ).
tff(c_38334,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_38298,c_38325]) ).
tff(c_38335,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_38152]) ).
tff(c_38416,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c6 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c6 )
| ( inverse(X3_6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_38239,c_38239,c_38239,c_38335]) ).
tff(c_38417,plain,
! [X3_6] :
( ( multiply(X3_6,sk_c6) != sk_c6 )
| ( inverse(X3_6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_38416]) ).
tff(c_39025,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_38444,c_38666,c_38444,c_38444,c_38417]) ).
tff(c_38429,plain,
inverse(sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38418,c_38348]) ).
tff(c_38459,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_38444,c_38429]) ).
tff(c_39027,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39025,c_38459]) ).
tff(c_39028,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_38416]) ).
tff(c_41543,plain,
! [X4_7,X1_8] :
( ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_39247,c_39093,c_39093,c_39093,c_39093,c_39247,c_39127,c_39093,c_39028]) ).
tff(c_41545,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_41543]) ).
tff(c_39121,plain,
inverse(identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_39093,c_38348]) ).
tff(c_39141,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_39127,c_39121]) ).
tff(c_41547,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41545,c_39141]) ).
tff(c_41549,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_41543]) ).
tff(c_41551,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41549,c_39141]) ).
tff(c_41552,plain,
inverse(sk_c4) = sk_c7,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_41557,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41552,c_4]) ).
tff(c_41553,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_54,plain,
( ( inverse(sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_41572,plain,
inverse(sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_41553,c_54]) ).
tff(c_41576,plain,
multiply(sk_c5,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41572,c_4]) ).
tff(c_43051,plain,
! [X_401,Y_402,Z_403] : ( multiply(multiply(X_401,Y_402),Z_403) = multiply(X_401,multiply(Y_402,Z_403)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_43078,plain,
! [Z_403] : ( multiply(sk_c5,multiply(sk_c7,Z_403)) = multiply(identity,Z_403) ),
inference(superposition,[status(thm),theory(equality)],[c_41576,c_43051]) ).
tff(c_43100,plain,
! [Z_404] : ( multiply(sk_c5,multiply(sk_c7,Z_404)) = Z_404 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43078]) ).
tff(c_43115,plain,
multiply(sk_c5,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_41557,c_43100]) ).
tff(c_41651,plain,
! [X_369,Y_370,Z_371] : ( multiply(multiply(X_369,Y_370),Z_371) = multiply(X_369,multiply(Y_370,Z_371)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_41690,plain,
! [X_2,Z_371] : ( multiply(inverse(X_2),multiply(X_2,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_41651]) ).
tff(c_41702,plain,
! [X_2,Z_371] : ( multiply(inverse(X_2),multiply(X_2,Z_371)) = Z_371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41690]) ).
tff(c_42571,plain,
! [X_390,Z_391] : ( multiply(inverse(X_390),multiply(X_390,Z_391)) = Z_391 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41690]) ).
tff(c_42748,plain,
! [X_394,Z_395] : ( multiply(inverse(inverse(X_394)),Z_395) = multiply(X_394,Z_395) ),
inference(superposition,[status(thm),theory(equality)],[c_41702,c_42571]) ).
tff(c_42592,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42571]) ).
tff(c_42755,plain,
! [X_394] : ( multiply(X_394,identity) = X_394 ),
inference(superposition,[status(thm),theory(equality)],[c_42748,c_42592]) ).
tff(c_56,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_41622,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_41553,c_56]) ).
tff(c_58,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_41561,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_41562,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41553,c_41561]) ).
tff(c_41563,plain,
inverse(sk_c3) = sk_c6,
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_41568,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41563,c_4]) ).
tff(c_41684,plain,
! [Z_371] : ( multiply(sk_c6,multiply(sk_c3,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_41568,c_41651]) ).
tff(c_41792,plain,
! [Z_374] : ( multiply(sk_c6,multiply(sk_c3,Z_374)) = Z_374 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41684]) ).
tff(c_41804,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_41622,c_41792]) ).
tff(c_50,plain,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_41634,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_41553,c_50]) ).
tff(c_52,plain,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_41597,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_41553,c_52]) ).
tff(c_41727,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_41634,c_41597,c_41572,c_78]) ).
tff(c_41728,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_41727]) ).
tff(c_41808,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41804,c_41728]) ).
tff(c_41816,plain,
! [X_375,Z_376] : ( multiply(inverse(X_375),multiply(X_375,Z_376)) = Z_376 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41690]) ).
tff(c_41834,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_41804,c_41816]) ).
tff(c_41889,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_41834]) ).
tff(c_41904,plain,
multiply(identity,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41889,c_41597]) ).
tff(c_41908,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41904]) ).
tff(c_41910,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_41808,c_41908]) ).
tff(c_41912,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_41727]) ).
tff(c_42306,plain,
! [Z_384] : ( multiply(sk_c6,multiply(sk_c3,Z_384)) = Z_384 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41684]) ).
tff(c_42327,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_41622,c_42306]) ).
tff(c_42331,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41912,c_42327]) ).
tff(c_42336,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_42331,c_41912]) ).
tff(c_42343,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41576,c_42336]) ).
tff(c_42353,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42343,c_41572]) ).
tff(c_42379,plain,
multiply(identity,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42353,c_4]) ).
tff(c_42389,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_42379,c_2]) ).
tff(c_41605,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_41610,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_41605,c_4]) ).
tff(c_41681,plain,
! [Z_371] : ( multiply(sk_c5,multiply(sk_c7,Z_371)) = multiply(identity,Z_371) ),
inference(superposition,[status(thm),theory(equality)],[c_41576,c_41651]) ).
tff(c_41704,plain,
! [Z_372] : ( multiply(sk_c5,multiply(sk_c7,Z_372)) = Z_372 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41681]) ).
tff(c_41716,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_41610,c_41704]) ).
tff(c_42350,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_42343,c_41716]) ).
tff(c_42354,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42350]) ).
tff(c_42367,plain,
inverse(identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_42354,c_41605]) ).
tff(c_42414,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42389,c_42367]) ).
tff(c_42423,plain,
! [X_385,Z_386] : ( multiply(inverse(X_385),multiply(X_385,Z_386)) = Z_386 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41690]) ).
tff(c_42478,plain,
! [X_387] : ( multiply(inverse(inverse(X_387)),identity) = X_387 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_42423]) ).
tff(c_42484,plain,
! [X_387] : ( multiply(inverse(inverse(inverse(X_387))),X_387) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_42478,c_41702]) ).
tff(c_42348,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42343,c_42331]) ).
tff(c_41699,plain,
! [Z_371] : ( multiply(sk_c5,multiply(sk_c7,Z_371)) = Z_371 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41681]) ).
tff(c_42170,plain,
! [Z_381] : ( multiply(sk_c6,multiply(sk_c3,Z_381)) = Z_381 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41684]) ).
tff(c_42191,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_41622,c_42170]) ).
tff(c_42195,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41912,c_42191]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_41916,plain,
! [Z_5] : ( multiply(sk_c6,multiply(sk_c7,Z_5)) = multiply(sk_c5,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_41912,c_6]) ).
tff(c_42214,plain,
! [Z_382] : ( multiply(sk_c5,Z_382) = Z_382 ),
inference(demodulation,[status(thm),theory(equality)],[c_41699,c_42195,c_41916]) ).
tff(c_42235,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_41576,c_42214]) ).
tff(c_42200,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_42195,c_41912]) ).
tff(c_42207,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41576,c_42200]) ).
tff(c_42244,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42207,c_41572]) ).
tff(c_42287,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42235,c_42244]) ).
tff(c_42240,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42207,c_42195]) ).
tff(c_41991,plain,
! [Z_378] : ( multiply(sk_c6,multiply(sk_c3,Z_378)) = Z_378 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_41684]) ).
tff(c_42012,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_41622,c_41991]) ).
tff(c_42016,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_41912,c_42012]) ).
tff(c_42021,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_42016,c_41912]) ).
tff(c_42028,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41576,c_42021]) ).
tff(c_42068,plain,
inverse(sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42028,c_41572]) ).
tff(c_42110,plain,
multiply(identity,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42068,c_4]) ).
tff(c_42131,plain,
sk_c7 = identity,
inference(superposition,[status(thm),theory(equality)],[c_42110,c_2]) ).
tff(c_42065,plain,
multiply(identity,identity) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_42028,c_41716]) ).
tff(c_42070,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_42065]) ).
tff(c_42081,plain,
inverse(identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_42070,c_41605]) ).
tff(c_42149,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42131,c_42081]) ).
tff(c_41911,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_41727]) ).
tff(c_41983,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_41911]) ).
tff(c_42091,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42028,c_41983]) ).
tff(c_42137,plain,
inverse(identity) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_42110,c_42091]) ).
tff(c_42160,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_42149,c_42131,c_42137]) ).
tff(c_42161,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_41911]) ).
tff(c_42162,plain,
! [X3_6] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_42161]) ).
tff(c_42270,plain,
! [X3_383] :
( ( multiply(X3_383,identity) != identity )
| ( inverse(X3_383) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42235,c_42235,c_42240,c_42162]) ).
tff(c_42284,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_2,c_42270]) ).
tff(c_42297,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_42287,c_42284]) ).
tff(c_42298,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_42161]) ).
tff(c_42363,plain,
! [X4_7,X1_8] :
( ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42348,c_42348,c_42348,c_42348,c_42343,c_42298]) ).
tff(c_42364,plain,
! [X1_8] :
( ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_42363]) ).
tff(c_42539,plain,
! [X1_389] :
( ( inverse(X1_389) != identity )
| ( multiply(X1_389,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_42389,c_42364]) ).
tff(c_42543,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_42484,c_42539]) ).
tff(c_42562,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_42414,c_42414,c_42414,c_42414,c_42543]) ).
tff(c_42563,plain,
! [X4_7] :
( ( multiply(X4_7,identity) != identity )
| ( inverse(X4_7) != identity ) ),
inference(splitRight,[status(thm)],[c_42363]) ).
tff(c_43009,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_42755,c_42563]) ).
tff(c_42341,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_42331,c_41563]) ).
tff(c_42603,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42343,c_42341]) ).
tff(c_42610,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_42603,c_4]) ).
tff(c_42618,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_42610,c_41702]) ).
tff(c_42630,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42618]) ).
tff(c_42634,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_42630,c_42603]) ).
tff(c_43011,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43009,c_42634]) ).
tff(c_43012,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_43112,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_41597,c_43100]) ).
tff(c_43072,plain,
! [Z_403] : ( multiply(sk_c6,multiply(sk_c5,Z_403)) = multiply(sk_c7,Z_403) ),
inference(superposition,[status(thm),theory(equality)],[c_43012,c_43051]) ).
tff(c_43401,plain,
multiply(sk_c7,sk_c6) = multiply(sk_c6,sk_c5),
inference(superposition,[status(thm),theory(equality)],[c_43112,c_43072]) ).
tff(c_43407,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43012,c_43401]) ).
tff(c_43095,plain,
! [Z_403] : ( multiply(sk_c5,multiply(sk_c7,Z_403)) = Z_403 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43078]) ).
tff(c_43423,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_43407,c_43095]) ).
tff(c_43429,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_41576,c_43423]) ).
tff(c_43432,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_43429,c_43112]) ).
tff(c_43441,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43115,c_43432]) ).
tff(c_43436,plain,
multiply(identity,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43429,c_43012]) ).
tff(c_43443,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43436]) ).
tff(c_43962,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43441,c_43443]) ).
tff(c_43452,plain,
inverse(sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43441,c_41572]) ).
tff(c_43970,plain,
inverse(sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43962,c_43452]) ).
tff(c_43974,plain,
multiply(sk_c4,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_43970,c_4]) ).
tff(c_43013,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_43021,plain,
multiply(sk_c4,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_43013,c_32]) ).
tff(c_43450,plain,
multiply(sk_c4,sk_c7) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43441,c_43021]) ).
tff(c_44035,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43974,c_43962,c_43450]) ).
tff(c_44039,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44035,c_43962]) ).
tff(c_43087,plain,
! [X_2,Z_403] : ( multiply(inverse(X_2),multiply(X_2,Z_403)) = multiply(identity,Z_403) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_43051]) ).
tff(c_43978,plain,
! [X_422,Z_423] : ( multiply(inverse(X_422),multiply(X_422,Z_423)) = Z_423 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43087]) ).
tff(c_43098,plain,
! [X_2,Z_403] : ( multiply(inverse(X_2),multiply(X_2,Z_403)) = Z_403 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43087]) ).
tff(c_44154,plain,
! [X_426,Z_427] : ( multiply(inverse(inverse(X_426)),Z_427) = multiply(X_426,Z_427) ),
inference(superposition,[status(thm),theory(equality)],[c_43978,c_43098]) ).
tff(c_44002,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_43978]) ).
tff(c_44161,plain,
! [X_426] : ( multiply(X_426,identity) = X_426 ),
inference(superposition,[status(thm),theory(equality)],[c_44154,c_44002]) ).
tff(c_43493,plain,
! [X_411,Z_412] : ( multiply(inverse(X_411),multiply(X_411,Z_412)) = Z_412 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43087]) ).
tff(c_43677,plain,
! [X_415,Z_416] : ( multiply(inverse(inverse(X_415)),Z_416) = multiply(X_415,Z_416) ),
inference(superposition,[status(thm),theory(equality)],[c_43098,c_43493]) ).
tff(c_43523,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_43493]) ).
tff(c_43688,plain,
! [X_415] : ( multiply(X_415,identity) = X_415 ),
inference(superposition,[status(thm),theory(equality)],[c_43677,c_43523]) ).
tff(c_43439,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43429,c_41563]) ).
tff(c_43459,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43441,c_43443]) ).
tff(c_28,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_43026,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_43013,c_28]) ).
tff(c_43435,plain,
multiply(sk_c3,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_43429,c_43026]) ).
tff(c_43531,plain,
multiply(sk_c3,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43459,c_43435]) ).
tff(c_43535,plain,
multiply(inverse(sk_c3),sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_43531,c_43098]) ).
tff(c_43541,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43439,c_43535]) ).
tff(c_43548,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43541,c_43459]) ).
tff(c_43173,plain,
! [X_406,Z_407] : ( multiply(inverse(X_406),multiply(X_406,Z_407)) = Z_407 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43087]) ).
tff(c_43191,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_43112,c_43173]) ).
tff(c_43213,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_43191]) ).
tff(c_43215,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_43213,c_43112]) ).
tff(c_43219,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43115,c_43215]) ).
tff(c_43084,plain,
! [Z_403] : ( multiply(sk_c7,multiply(sk_c4,Z_403)) = multiply(identity,Z_403) ),
inference(superposition,[status(thm),theory(equality)],[c_41557,c_43051]) ).
tff(c_43137,plain,
! [Z_405] : ( multiply(sk_c7,multiply(sk_c4,Z_405)) = Z_405 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_43084]) ).
tff(c_43152,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_43021,c_43137]) ).
tff(c_43156,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_41597,c_43152]) ).
tff(c_43214,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43213,c_43156]) ).
tff(c_43304,plain,
! [Z_403] : ( multiply(sk_c4,Z_403) = Z_403 ),
inference(demodulation,[status(thm),theory(equality)],[c_43219,c_2,c_43214,c_2,c_43213,c_43072]) ).
tff(c_43161,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_43156,c_43021]) ).
tff(c_43323,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43304,c_43219,c_43213,c_43161]) ).
tff(c_43327,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43323,c_43219]) ).
tff(c_43120,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_43012,c_41597,c_41572,c_78]) ).
tff(c_43121,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_43120]) ).
tff(c_43158,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_43156,c_43121]) ).
tff(c_43369,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_43327,c_43213,c_2,c_43213,c_43158]) ).
tff(c_43370,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(X3_6,sk_c6) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_43120]) ).
tff(c_43457,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(X3_6,identity) != sk_c7 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X4_7,sk_c4) != identity )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != sk_c7 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c4 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_43441,c_43429,c_43429,c_43429,c_43441,c_43429,c_43429,c_43370]) ).
tff(c_43458,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != sk_c4 ) ),
inference(splitLeft,[status(thm)],[c_43457]) ).
tff(c_43958,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_43688,c_43548,c_43541,c_43548,c_43458]) ).
tff(c_43467,plain,
inverse(sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_43459,c_43452]) ).
tff(c_43547,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_43541,c_43541,c_43467]) ).
tff(c_43960,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43958,c_43547]) ).
tff(c_43961,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != identity )
| ( multiply(X1_8,identity) != sk_c7 )
| ( multiply(X4_7,sk_c4) != identity )
| ( inverse(X4_7) != identity )
| ( multiply(X3_6,identity) != sk_c7 )
| ( inverse(X3_6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_43457]) ).
tff(c_113941,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( identity != X3_6 )
| ( inverse(X3_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_44039,c_44161,c_44039,c_44161,c_44035,c_44161,c_44039,c_43961]) ).
tff(c_113943,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_113941]) ).
tff(c_44038,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_44035,c_44035,c_43970]) ).
tff(c_113945,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_113943,c_44038]) ).
tff(c_113946,plain,
! [X4_7,X1_8] :
( ( identity != X4_7 )
| ( inverse(X4_7) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_113941]) ).
tff(c_113948,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_113946]) ).
tff(c_113950,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_113948,c_44038]) ).
tff(c_115733,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_113946]) ).
tff(c_115735,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_115733,c_44038]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP346-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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n004.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 21:42:53 EDT 2025
% 0.12/0.34 % CPUTime :
% 24.65/12.49 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.77/12.53
% 24.77/12.53 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------