%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP288-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 : n019.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:49 PM UTC 2025
% Result : Unsatisfiable 23.76s 11.03s
% Output : CNFRefutation 23.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 27
% Syntax : Number of formulae : 337 ( 272 unt; 0 typ; 0 def)
% Number of atoms : 501 ( 482 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 332 ( 168 ~; 164 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 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 : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 178 ( 178 !; 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_68,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c7,sk_c6) != sk_c5 )
| ( multiply(X3,sk_c7) != sk_c6 )
| ( inverse(X3) != sk_c7 )
| ( multiply(X4,sk_c6) != sk_c5 )
| ( inverse(X4) != sk_c6 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( multiply(X2,sk_c6) != sk_c7 )
| ( inverse(X2) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( 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_46768,plain,
! [X_404,Y_405,Z_406] : ( multiply(multiply(X_404,Y_405),Z_406) = multiply(X_404,multiply(Y_405,Z_406)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_46801,plain,
! [X_2,Z_406] : ( multiply(inverse(X_2),multiply(X_2,Z_406)) = multiply(identity,Z_406) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_46768]) ).
tff(c_46996,plain,
! [X_410,Z_411] : ( multiply(inverse(X_410),multiply(X_410,Z_411)) = Z_411 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46801]) ).
tff(c_46812,plain,
! [X_2,Z_406] : ( multiply(inverse(X_2),multiply(X_2,Z_406)) = Z_406 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46801]) ).
tff(c_47272,plain,
! [X_413,Z_414] : ( multiply(inverse(inverse(X_413)),Z_414) = multiply(X_413,Z_414) ),
inference(superposition,[status(thm),theory(equality)],[c_46996,c_46812]) ).
tff(c_47041,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_46996]) ).
tff(c_47279,plain,
! [X_413] : ( multiply(X_413,identity) = X_413 ),
inference(superposition,[status(thm),theory(equality)],[c_47272,c_47041]) ).
tff(c_12046,plain,
! [X_185,Y_186,Z_187] : ( multiply(multiply(X_185,Y_186),Z_187) = multiply(X_185,multiply(Y_186,Z_187)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12079,plain,
! [X_2,Z_187] : ( multiply(inverse(X_2),multiply(X_2,Z_187)) = multiply(identity,Z_187) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12046]) ).
tff(c_12310,plain,
! [X_192,Z_193] : ( multiply(inverse(X_192),multiply(X_192,Z_193)) = Z_193 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12079]) ).
tff(c_12090,plain,
! [X_2,Z_187] : ( multiply(inverse(X_2),multiply(X_2,Z_187)) = Z_187 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12079]) ).
tff(c_12533,plain,
! [X_196,Z_197] : ( multiply(inverse(inverse(X_196)),Z_197) = multiply(X_196,Z_197) ),
inference(superposition,[status(thm),theory(equality)],[c_12310,c_12090]) ).
tff(c_12361,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12310]) ).
tff(c_12540,plain,
! [X_196] : ( multiply(X_196,identity) = X_196 ),
inference(superposition,[status(thm),theory(equality)],[c_12533,c_12361]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_26,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_108,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_30,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_87,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_91,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87,c_4]) ).
tff(c_9175,plain,
! [X_127,Y_128,Z_129] : ( multiply(multiply(X_127,Y_128),Z_129) = multiply(X_127,multiply(Y_128,Z_129)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9211,plain,
! [Z_129] : ( multiply(sk_c7,multiply(sk_c1,Z_129)) = multiply(identity,Z_129) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_9175]) ).
tff(c_9365,plain,
! [Z_135] : ( multiply(sk_c7,multiply(sk_c1,Z_135)) = Z_135 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9211]) ).
tff(c_9377,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_108,c_9365]) ).
tff(c_9381,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_9377]) ).
tff(c_9390,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9381,c_102]) ).
tff(c_9217,plain,
! [X_2,Z_129] : ( multiply(inverse(X_2),multiply(X_2,Z_129)) = multiply(identity,Z_129) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9175]) ).
tff(c_9475,plain,
! [X_136,Z_137] : ( multiply(inverse(X_136),multiply(X_136,Z_137)) = Z_137 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9217]) ).
tff(c_9511,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9390,c_9475]) ).
tff(c_9552,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_9511]) ).
tff(c_134,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_164,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_134]) ).
tff(c_174,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_164]) ).
tff(c_985,plain,
! [X_33,Z_34] : ( multiply(inverse(X_33),multiply(X_33,Z_34)) = Z_34 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_1230,plain,
! [X_38,Z_39] : ( multiply(inverse(inverse(X_38)),Z_39) = multiply(X_38,Z_39) ),
inference(superposition,[status(thm),theory(equality)],[c_174,c_985]) ).
tff(c_1021,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_985]) ).
tff(c_1241,plain,
! [X_38] : ( multiply(X_38,identity) = X_38 ),
inference(superposition,[status(thm),theory(equality)],[c_1230,c_1021]) ).
tff(c_50,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_75,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_50]) ).
tff(c_40,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_116,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_1012,plain,
multiply(inverse(sk_c2),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_116,c_985]) ).
tff(c_1028,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_1012]) ).
tff(c_1032,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_1028,c_174]) ).
tff(c_1038,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1032]) ).
tff(c_158,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_134]) ).
tff(c_366,plain,
! [Z_20] : ( multiply(sk_c7,multiply(sk_c1,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_378,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_108,c_366]) ).
tff(c_382,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_378]) ).
tff(c_386,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_382,c_102]) ).
tff(c_1095,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1038,c_2,c_1038,c_386]) ).
tff(c_467,plain,
! [X_22,Z_23] : ( multiply(inverse(X_22),multiply(X_22,Z_23)) = Z_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_164]) ).
tff(c_705,plain,
! [X_26,Z_27] : ( multiply(inverse(inverse(X_26)),Z_27) = multiply(X_26,Z_27) ),
inference(superposition,[status(thm),theory(equality)],[c_467,c_174]) ).
tff(c_497,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_467]) ).
tff(c_712,plain,
! [X_26] : ( multiply(X_26,identity) = X_26 ),
inference(superposition,[status(thm),theory(equality)],[c_705,c_497]) ).
tff(c_79,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_75,c_4]) ).
tff(c_161,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_134]) ).
tff(c_179,plain,
! [Z_15] : ( multiply(sk_c6,multiply(sk_c2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_191,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_116,c_179]) ).
tff(c_271,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_164]) ).
tff(c_295,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_191,c_271]) ).
tff(c_320,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_295]) ).
tff(c_221,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_158]) ).
tff(c_239,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_108,c_221]) ).
tff(c_243,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_239]) ).
tff(c_58,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_177,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c7 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_102,c_58]) ).
tff(c_178,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_177]) ).
tff(c_246,plain,
multiply(sk_c6,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_243,c_178]) ).
tff(c_251,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_191,c_246]) ).
tff(c_325,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_320,c_251]) ).
tff(c_250,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_243,c_87]) ).
tff(c_259,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_250,c_4]) ).
tff(c_337,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_320,c_259]) ).
tff(c_247,plain,
multiply(sk_c1,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_243,c_108]) ).
tff(c_355,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_337,c_320,c_247]) ).
tff(c_356,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_325,c_355]) ).
tff(c_358,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_384,plain,
multiply(sk_c6,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_382,c_358]) ).
tff(c_432,plain,
! [Z_21] : ( multiply(sk_c6,multiply(sk_c2,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_161]) ).
tff(c_444,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_116,c_432]) ).
tff(c_448,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_444]) ).
tff(c_450,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_448,c_384]) ).
tff(c_529,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_450,c_174]) ).
tff(c_535,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_529]) ).
tff(c_542,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_535,c_448]) ).
tff(c_357,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_177]) ).
tff(c_393,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( multiply(X1_8,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_382,c_382,c_382,c_382,c_382,c_357]) ).
tff(c_394,plain,
! [X2_9] :
( ( inverse(X2_9) != sk_c6 )
| ( multiply(X2_9,sk_c6) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_393]) ).
tff(c_966,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_712,c_542,c_535,c_542,c_394]) ).
tff(c_455,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_448,c_75]) ).
tff(c_541,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_535,c_455]) ).
tff(c_575,plain,
multiply(identity,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_541,c_4]) ).
tff(c_603,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_575,c_174]) ).
tff(c_615,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_603]) ).
tff(c_619,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_615,c_541]) ).
tff(c_968,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_966,c_619]) ).
tff(c_969,plain,
! [X1_8,X4_7,X3_6] :
( ( multiply(X1_8,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c5 )
| ( multiply(X3_6,sk_c5) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_393]) ).
tff(c_8723,plain,
! [X1_8,X4_7,X3_6] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X3_6) != identity )
| ( identity != X3_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1241,c_1095,c_1038,c_1038,c_1241,c_1095,c_1038,c_1095,c_1038,c_1241,c_1095,c_1038,c_969]) ).
tff(c_8725,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8723]) ).
tff(c_388,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_382,c_87]) ).
tff(c_973,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_388,c_4]) ).
tff(c_1053,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1038,c_973]) ).
tff(c_1042,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1038,c_388]) ).
tff(c_1058,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1053,c_1042]) ).
tff(c_8727,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8725,c_1058]) ).
tff(c_8728,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_8723]) ).
tff(c_8730,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_8728]) ).
tff(c_8732,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8730,c_1058]) ).
tff(c_9123,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_8728]) ).
tff(c_9125,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9123,c_1058]) ).
tff(c_9127,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_38,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_9157,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_9127,c_38]) ).
tff(c_9386,plain,
multiply(sk_c6,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9381,c_9157]) ).
tff(c_46,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_9139,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_9127,c_46]) ).
tff(c_44,plain,
( ( multiply(sk_c4,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_9169,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9127,c_44]) ).
tff(c_9384,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9381,c_9169]) ).
tff(c_9505,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9384,c_9475]) ).
tff(c_9550,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9386,c_9139,c_9505]) ).
tff(c_9575,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9552,c_9550]) ).
tff(c_9229,plain,
! [X_2,Z_129] : ( multiply(inverse(X_2),multiply(X_2,Z_129)) = Z_129 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9217]) ).
tff(c_9340,plain,
! [Z_134] : ( multiply(sk_c7,multiply(sk_c6,Z_134)) = multiply(sk_c5,Z_134) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_9175]) ).
tff(c_9361,plain,
multiply(sk_c7,identity) = multiply(sk_c5,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_79,c_9340]) ).
tff(c_9466,plain,
multiply(sk_c5,sk_c2) = multiply(sk_c5,identity),
inference(demodulation,[status(thm),theory(equality)],[c_9381,c_9361]) ).
tff(c_9493,plain,
multiply(inverse(sk_c5),multiply(sk_c5,identity)) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_9466,c_9475]) ).
tff(c_9548,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_9229,c_9493]) ).
tff(c_9562,plain,
multiply(sk_c2,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9552,c_9127]) ).
tff(c_9812,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9575,c_2,c_9548,c_9562]) ).
tff(c_9814,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_18,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_9857,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_9814,c_18]) ).
tff(c_24,plain,
( ( multiply(sk_c4,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_9845,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9814,c_24]) ).
tff(c_9813,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_9818,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9813,c_4]) ).
tff(c_9870,plain,
! [X_140,Y_141,Z_142] : ( multiply(multiply(X_140,Y_141),Z_142) = multiply(X_140,multiply(Y_141,Z_142)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_9900,plain,
! [Z_142] : ( multiply(sk_c6,multiply(sk_c4,Z_142)) = multiply(identity,Z_142) ),
inference(superposition,[status(thm),theory(equality)],[c_9818,c_9870]) ).
tff(c_10336,plain,
! [Z_151] : ( multiply(sk_c6,multiply(sk_c4,Z_151)) = Z_151 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9900]) ).
tff(c_10348,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9845,c_10336]) ).
tff(c_10352,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_9857,c_10348]) ).
tff(c_10394,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10352,c_9857]) ).
tff(c_9912,plain,
! [X_2,Z_142] : ( multiply(inverse(X_2),multiply(X_2,Z_142)) = multiply(identity,Z_142) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9870]) ).
tff(c_10492,plain,
! [X_153,Z_154] : ( multiply(inverse(X_153),multiply(X_153,Z_154)) = Z_154 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9912]) ).
tff(c_10531,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10394,c_10492]) ).
tff(c_10574,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10531]) ).
tff(c_10588,plain,
multiply(identity,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_10574,c_91]) ).
tff(c_9924,plain,
! [X_2,Z_142] : ( multiply(inverse(X_2),multiply(X_2,Z_142)) = Z_142 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9912]) ).
tff(c_10666,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_10588,c_9924]) ).
tff(c_10678,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10666]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_9862,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9814,c_22]) ).
tff(c_20,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_9827,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_9814,c_20]) ).
tff(c_9831,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_9827,c_4]) ).
tff(c_9897,plain,
! [Z_142] : ( multiply(sk_c7,multiply(sk_c3,Z_142)) = multiply(identity,Z_142) ),
inference(superposition,[status(thm),theory(equality)],[c_9831,c_9870]) ).
tff(c_9962,plain,
! [Z_145] : ( multiply(sk_c7,multiply(sk_c3,Z_145)) = Z_145 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9897]) ).
tff(c_9974,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_9862,c_9962]) ).
tff(c_10390,plain,
multiply(sk_c7,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10352,c_9974]) ).
tff(c_10578,plain,
multiply(identity,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10574,c_10574,c_10390]) ).
tff(c_10590,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10578]) ).
tff(c_10398,plain,
multiply(sk_c1,sk_c7) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10352,c_9814]) ).
tff(c_10579,plain,
multiply(sk_c1,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10574,c_10398]) ).
tff(c_10692,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_10678,c_10590,c_10579]) ).
tff(c_10694,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_11563,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_10694,c_8]) ).
tff(c_10732,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_10694,c_8]) ).
tff(c_14,plain,
( ( multiply(sk_c4,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_11195,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_10694,c_14]) ).
tff(c_16,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_10712,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_10694,c_16]) ).
tff(c_10716,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_10712,c_4]) ).
tff(c_11203,plain,
! [X_166,Y_167,Z_168] : ( multiply(multiply(X_166,Y_167),Z_168) = multiply(X_166,multiply(Y_167,Z_168)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11227,plain,
! [Z_168] : ( multiply(sk_c6,multiply(sk_c4,Z_168)) = multiply(identity,Z_168) ),
inference(superposition,[status(thm),theory(equality)],[c_10716,c_11203]) ).
tff(c_11331,plain,
! [Z_172] : ( multiply(sk_c6,multiply(sk_c4,Z_172)) = Z_172 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11227]) ).
tff(c_11343,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11195,c_11331]) ).
tff(c_11347,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_10732,c_11343]) ).
tff(c_11356,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11347,c_10732]) ).
tff(c_11242,plain,
! [X_2,Z_168] : ( multiply(inverse(X_2),multiply(X_2,Z_168)) = multiply(identity,Z_168) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11203]) ).
tff(c_11254,plain,
! [X_2,Z_168] : ( multiply(inverse(X_2),multiply(X_2,Z_168)) = Z_168 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11242]) ).
tff(c_11455,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11356,c_11254]) ).
tff(c_11461,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11455]) ).
tff(c_10707,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_11236,plain,
! [Z_168] : ( multiply(sk_c7,multiply(sk_c1,Z_168)) = multiply(identity,Z_168) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_11203]) ).
tff(c_11256,plain,
! [Z_169] : ( multiply(sk_c7,multiply(sk_c1,Z_169)) = Z_169 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11236]) ).
tff(c_11268,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_10707,c_11256]) ).
tff(c_11274,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11268,c_10694]) ).
tff(c_11465,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_11461,c_11274]) ).
tff(c_11470,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_11461,c_87]) ).
tff(c_11359,plain,
multiply(sk_c1,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11347,c_10707]) ).
tff(c_11509,plain,
multiply(sk_c1,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11461,c_11359]) ).
tff(c_11513,plain,
multiply(inverse(sk_c1),sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11509,c_11254]) ).
tff(c_11519,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11470,c_11513]) ).
tff(c_11521,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11465,c_11519]) ).
tff(c_11523,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_11544,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11523,c_24]) ).
tff(c_11522,plain,
inverse(sk_c4) = sk_c6,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_11527,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11522,c_4]) ).
tff(c_11572,plain,
! [X_175,Y_176,Z_177] : ( multiply(multiply(X_175,Y_176),Z_177) = multiply(X_175,multiply(Y_176,Z_177)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_11599,plain,
! [Z_177] : ( multiply(sk_c6,multiply(sk_c4,Z_177)) = multiply(identity,Z_177) ),
inference(superposition,[status(thm),theory(equality)],[c_11527,c_11572]) ).
tff(c_11661,plain,
! [Z_180] : ( multiply(sk_c6,multiply(sk_c4,Z_180)) = Z_180 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11599]) ).
tff(c_11673,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_11544,c_11661]) ).
tff(c_11677,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11563,c_11673]) ).
tff(c_11681,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11677,c_11563]) ).
tff(c_11611,plain,
! [X_2,Z_177] : ( multiply(inverse(X_2),multiply(X_2,Z_177)) = multiply(identity,Z_177) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_11572]) ).
tff(c_11623,plain,
! [X_2,Z_177] : ( multiply(inverse(X_2),multiply(X_2,Z_177)) = Z_177 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11611]) ).
tff(c_11941,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_11681,c_11623]) ).
tff(c_11947,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_11941]) ).
tff(c_11688,plain,
multiply(sk_c7,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_11677,c_10694]) ).
tff(c_11986,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_11947,c_11688]) ).
tff(c_11988,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_12013,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_11988,c_28]) ).
tff(c_34,plain,
( ( multiply(sk_c4,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_12029,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11988,c_34]) ).
tff(c_36,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_11996,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_11988,c_36]) ).
tff(c_12000,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_11996,c_4]) ).
tff(c_12070,plain,
! [Z_187] : ( multiply(sk_c6,multiply(sk_c4,Z_187)) = multiply(identity,Z_187) ),
inference(superposition,[status(thm),theory(equality)],[c_12000,c_12046]) ).
tff(c_12092,plain,
! [Z_188] : ( multiply(sk_c6,multiply(sk_c4,Z_188)) = Z_188 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12070]) ).
tff(c_12104,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12029,c_12092]) ).
tff(c_12108,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12013,c_12104]) ).
tff(c_12112,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12108,c_12013]) ).
tff(c_12331,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12112,c_12310]) ).
tff(c_12368,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12331]) ).
tff(c_11987,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_12377,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12368,c_11987]) ).
tff(c_12389,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12377,c_4]) ).
tff(c_12396,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_12389,c_12090]) ).
tff(c_12408,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12396]) ).
tff(c_12412,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12408,c_12377]) ).
tff(c_32,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_12018,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_11988,c_32]) ).
tff(c_12064,plain,
! [Z_187] : ( multiply(sk_c3,multiply(sk_c6,Z_187)) = multiply(sk_c7,Z_187) ),
inference(superposition,[status(thm),theory(equality)],[c_12018,c_12046]) ).
tff(c_12434,plain,
! [Z_194] : ( multiply(sk_c5,Z_194) = Z_194 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12408,c_2,c_12368,c_12108,c_12064]) ).
tff(c_12114,plain,
inverse(sk_c4) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12108,c_11996]) ).
tff(c_12124,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12114,c_4]) ).
tff(c_12446,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_12434,c_12124]) ).
tff(c_12471,plain,
inverse(identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12446,c_12114]) ).
tff(c_12473,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_12412,c_12471]) ).
tff(c_12190,plain,
! [X_190,Z_191] : ( multiply(inverse(X_190),multiply(X_190,Z_191)) = Z_191 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12079]) ).
tff(c_12214,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12112,c_12190]) ).
tff(c_12248,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12214]) ).
tff(c_12135,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c7 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c5,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_12108,c_12108,c_12108,c_12108,c_12108,c_12108,c_12108,c_12108,c_58]) ).
tff(c_12136,plain,
multiply(sk_c7,sk_c5) != sk_c5,
inference(splitLeft,[status(thm)],[c_12135]) ).
tff(c_12254,plain,
multiply(identity,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_12248,c_12136]) ).
tff(c_12261,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12254]) ).
tff(c_12262,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(sk_c5,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_12135]) ).
tff(c_20895,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != identity )
| ( identity != X3_6 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_12540,c_12473,c_12368,c_12473,c_12368,c_12540,c_12473,c_12368,c_12540,c_12473,c_12473,c_12473,c_12540,c_12473,c_12368,c_12368,c_12473,c_2,c_12473,c_12368,c_12262]) ).
tff(c_20897,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_20895]) ).
tff(c_20899,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_20897,c_12412]) ).
tff(c_20900,plain,
! [X1_8,X4_7,X3_6] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X3_6) != identity )
| ( identity != X3_6 ) ),
inference(splitRight,[status(thm)],[c_20895]) ).
tff(c_46685,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_20900]) ).
tff(c_46687,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46685,c_12412]) ).
tff(c_46688,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_20900]) ).
tff(c_46690,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_46688]) ).
tff(c_46692,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46690,c_12412]) ).
tff(c_46694,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_46688]) ).
tff(c_46696,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46694,c_12412]) ).
tff(c_46698,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_48,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_46739,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_46698,c_48]) ).
tff(c_54,plain,
( ( multiply(sk_c4,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_46753,plain,
multiply(sk_c4,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_46698,c_54]) ).
tff(c_56,plain,
( ( inverse(sk_c4) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_46711,plain,
inverse(sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_46698,c_56]) ).
tff(c_46715,plain,
multiply(sk_c6,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_46711,c_4]) ).
tff(c_46795,plain,
! [Z_406] : ( multiply(sk_c6,multiply(sk_c4,Z_406)) = multiply(identity,Z_406) ),
inference(superposition,[status(thm),theory(equality)],[c_46715,c_46768]) ).
tff(c_46814,plain,
! [Z_407] : ( multiply(sk_c6,multiply(sk_c4,Z_407)) = Z_407 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46795]) ).
tff(c_46826,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_46753,c_46814]) ).
tff(c_46830,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_46739,c_46826]) ).
tff(c_46834,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_46830,c_46739]) ).
tff(c_47014,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_46834,c_46996]) ).
tff(c_47048,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_47014]) ).
tff(c_46697,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_50]) ).
tff(c_47055,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47048,c_46697]) ).
tff(c_52,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_46746,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_46698,c_52]) ).
tff(c_46833,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_46830,c_46746]) ).
tff(c_47081,plain,
multiply(sk_c3,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47048,c_46833]) ).
tff(c_47085,plain,
multiply(inverse(sk_c3),identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_47081,c_46812]) ).
tff(c_47091,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_47055,c_47085]) ).
tff(c_46880,plain,
! [X_408,Z_409] : ( multiply(inverse(X_408),multiply(X_408,Z_409)) = Z_409 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46801]) ).
tff(c_46901,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_46834,c_46880]) ).
tff(c_46936,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_46901]) ).
tff(c_46849,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c7 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(sk_c5,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_46830,c_46830,c_46830,c_46830,c_46830,c_46830,c_46830,c_46830,c_58]) ).
tff(c_46850,plain,
multiply(sk_c7,sk_c5) != sk_c5,
inference(splitLeft,[status(thm)],[c_46849]) ).
tff(c_46971,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_46936,c_46850]) ).
tff(c_46972,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( multiply(sk_c5,sk_c7) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X1_8) != sk_c7 )
| ( inverse(X2_9) != sk_c5 )
| ( multiply(X2_9,sk_c5) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_46849]) ).
tff(c_55201,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != identity )
| ( identity != X3_6 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X2_9) != identity )
| ( identity != X2_9 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_47279,c_47091,c_47048,c_47091,c_47048,c_47279,c_47091,c_47048,c_47279,c_47091,c_47091,c_47091,c_47279,c_47091,c_47048,c_47048,c_47091,c_2,c_47091,c_47048,c_46972]) ).
tff(c_55203,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_55201]) ).
tff(c_47066,plain,
multiply(identity,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_47055,c_4]) ).
tff(c_47136,plain,
multiply(inverse(identity),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_47066,c_46812]) ).
tff(c_47148,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_47136]) ).
tff(c_47152,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_47148,c_47055]) ).
tff(c_55205,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_55203,c_47152]) ).
tff(c_55206,plain,
! [X1_8,X4_7,X3_6] :
( ( identity != X1_8 )
| ( inverse(X1_8) != identity )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X3_6) != identity )
| ( identity != X3_6 ) ),
inference(splitRight,[status(thm)],[c_55201]) ).
tff(c_77064,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_55206]) ).
tff(c_77066,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_77064,c_47152]) ).
tff(c_77067,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( identity != X1_8 )
| ( inverse(X1_8) != identity ) ),
inference(splitRight,[status(thm)],[c_55206]) ).
tff(c_78230,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_77067]) ).
tff(c_78232,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_78230,c_47152]) ).
tff(c_78234,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_77067]) ).
tff(c_78236,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_78234,c_47152]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : GRP288-1 : TPTP v9.0.0. Released v2.5.0.
% 0.00/0.09 % 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.09/0.29 % Computer : n019.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Mon Apr 7 21:40:32 EDT 2025
% 0.09/0.29 % CPUTime :
% 23.76/11.03 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.76/11.06
% 23.76/11.06 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------