%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP235-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 : n006.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:38 PM UTC 2025
% Result : Unsatisfiable 20.04s 9.80s
% Output : CNFRefutation 20.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 27
% Syntax : Number of formulae : 445 ( 369 unt; 0 typ; 0 def)
% Number of atoms : 585 ( 566 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 293 ( 153 ~; 140 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 214 ( 214 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X6,X3,X1,X2,X4] :
( ( inverse(sk_c8) != sk_c7 )
| ( inverse(X4) != sk_c8 )
| ( multiply(X4,sk_c7) != sk_c8 )
| ( multiply(X5,X6) != sk_c7 )
| ( inverse(X5) != X6 )
| ( multiply(X6,sk_c8) != sk_c7 )
| ( inverse(X1) != sk_c8 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( multiply(sk_c8,X2) != sk_c7 )
| ( multiply(X3,sk_c8) != X2 )
| ( inverse(X3) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( multiply(sk_c2,sk_c3) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( inverse(sk_c8) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_160,plain,
! [X_14,Y_15,Z_16] : ( multiply(multiply(X_14,Y_15),Z_16) = multiply(X_14,multiply(Y_15,Z_16)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_193,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_160]) ).
tff(c_2288,plain,
! [X_56,Z_57] : ( multiply(inverse(X_56),multiply(X_56,Z_57)) = Z_57 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_204,plain,
! [X_2,Z_16] : ( multiply(inverse(X_2),multiply(X_2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_2538,plain,
! [X_61,Z_62] : ( multiply(inverse(inverse(X_61)),Z_62) = multiply(X_61,Z_62) ),
inference(superposition,[status(thm),theory(equality)],[c_2288,c_204]) ).
tff(c_2559,plain,
! [X_61] : ( multiply(X_61,inverse(X_61)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_2538,c_4]) ).
tff(c_56,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_85,plain,
inverse(sk_c2) = sk_c3,
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_26,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_111,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_115,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_111,c_4]) ).
tff(c_8,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_98,plain,
inverse(sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_187,plain,
! [Z_16] : ( multiply(sk_c7,multiply(sk_c8,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_160]) ).
tff(c_229,plain,
! [Z_18] : ( multiply(sk_c7,multiply(sk_c8,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_187]) ).
tff(c_247,plain,
multiply(sk_c7,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_229]) ).
tff(c_36,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_137,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_184,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c1,Z_16)) = multiply(identity,Z_16) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_160]) ).
tff(c_206,plain,
! [Z_17] : ( multiply(sk_c8,multiply(sk_c1,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_184]) ).
tff(c_218,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_137,c_206]) ).
tff(c_420,plain,
! [Z_22] : ( multiply(sk_c1,multiply(sk_c7,Z_22)) = multiply(sk_c8,Z_22) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_160]) ).
tff(c_444,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c1,identity),
inference(superposition,[status(thm),theory(equality)],[c_102,c_420]) ).
tff(c_448,plain,
multiply(sk_c1,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_218,c_444]) ).
tff(c_201,plain,
! [Z_16] : ( multiply(sk_c8,multiply(sk_c1,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_184]) ).
tff(c_452,plain,
multiply(sk_c8,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_448,c_201]) ).
tff(c_202,plain,
! [Z_16] : ( multiply(sk_c7,multiply(sk_c8,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_187]) ).
tff(c_463,plain,
multiply(sk_c7,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_452,c_202]) ).
tff(c_469,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_247,c_463]) ).
tff(c_46,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_124,plain,
multiply(sk_c2,sk_c3) = sk_c7,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_481,plain,
multiply(sk_c2,sk_c3) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_469,c_124]) ).
tff(c_2306,plain,
multiply(inverse(sk_c2),sk_c1) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_481,c_2288]) ).
tff(c_2352,plain,
multiply(sk_c3,sk_c1) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_2306]) ).
tff(c_2413,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_2352,c_204]) ).
tff(c_2419,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2413]) ).
tff(c_2345,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2288]) ).
tff(c_2545,plain,
! [X_61] : ( multiply(X_61,identity) = X_61 ),
inference(superposition,[status(thm),theory(equality)],[c_2538,c_2345]) ).
tff(c_241,plain,
multiply(sk_c7,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_218,c_229]) ).
tff(c_475,plain,
multiply(sk_c1,sk_c1) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_469,c_469,c_241]) ).
tff(c_2427,plain,
multiply(identity,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_2419,c_2419,c_475]) ).
tff(c_2434,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2427]) ).
tff(c_563,plain,
! [X_23,Z_24] : ( multiply(inverse(X_23),multiply(X_23,Z_24)) = Z_24 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_193]) ).
tff(c_859,plain,
! [X_28,Z_29] : ( multiply(inverse(inverse(X_28)),Z_29) = multiply(X_28,Z_29) ),
inference(superposition,[status(thm),theory(equality)],[c_563,c_204]) ).
tff(c_623,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_563]) ).
tff(c_866,plain,
! [X_28] : ( multiply(X_28,identity) = X_28 ),
inference(superposition,[status(thm),theory(equality)],[c_859,c_623]) ).
tff(c_584,plain,
multiply(inverse(sk_c2),sk_c1) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_481,c_563]) ).
tff(c_631,plain,
multiply(sk_c3,sk_c1) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_85,c_584]) ).
tff(c_643,plain,
multiply(inverse(sk_c3),sk_c3) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_631,c_204]) ).
tff(c_649,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_643]) ).
tff(c_657,plain,
multiply(identity,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_649,c_649,c_475]) ).
tff(c_664,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_657]) ).
tff(c_285,plain,
! [Z_20] : ( multiply(sk_c1,multiply(sk_c7,Z_20)) = multiply(sk_c8,Z_20) ),
inference(superposition,[status(thm),theory(equality)],[c_137,c_160]) ).
tff(c_309,plain,
multiply(sk_c8,sk_c8) = multiply(sk_c1,identity),
inference(superposition,[status(thm),theory(equality)],[c_102,c_285]) ).
tff(c_313,plain,
multiply(sk_c1,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_218,c_309]) ).
tff(c_324,plain,
multiply(sk_c8,sk_c7) = identity,
inference(superposition,[status(thm),theory(equality)],[c_313,c_201]) ).
tff(c_335,plain,
multiply(sk_c7,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_324,c_202]) ).
tff(c_341,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_247,c_335]) ).
tff(c_348,plain,
multiply(sk_c1,sk_c1) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_341,c_341,c_241]) ).
tff(c_68,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c8 )
| ( inverse(X4_11) != sk_c8 )
| ( inverse(sk_c8) != sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_252,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c8 )
| ( inverse(X4_11) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_98,c_68]) ).
tff(c_253,plain,
! [X4_11] :
( ( multiply(X4_11,sk_c7) != sk_c8 )
| ( inverse(X4_11) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_252]) ).
tff(c_369,plain,
! [X4_11] :
( ( multiply(X4_11,sk_c1) != sk_c8 )
| ( inverse(X4_11) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_341,c_253]) ).
tff(c_391,plain,
inverse(sk_c1) != sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_348,c_369]) ).
tff(c_403,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_111,c_391]) ).
tff(c_404,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_252]) ).
tff(c_506,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),sk_c8) != sk_c1 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c1 )
| ( multiply(X1_9,sk_c1) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_469,c_469,c_469,c_469,c_404]) ).
tff(c_507,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c1 ) ),
inference(splitLeft,[status(thm)],[c_506]) ).
tff(c_2237,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_866,c_664,c_2,c_664,c_649,c_664,c_507]) ).
tff(c_483,plain,
inverse(sk_c8) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_469,c_98]) ).
tff(c_658,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_649,c_483]) ).
tff(c_716,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_664,c_658]) ).
tff(c_2239,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2237,c_716]) ).
tff(c_2240,plain,
! [X1_9,X5_6] :
( ( multiply(X1_9,sk_c1) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c8) != sk_c1 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c1 ) ),
inference(splitRight,[status(thm)],[c_506]) ).
tff(c_68415,plain,
! [X1_9,X5_6] :
( ( identity != X1_9 )
| ( inverse(X1_9) != identity )
| ( inverse(X5_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2559,c_2419,c_2545,c_2434,c_2419,c_2434,c_2545,c_2434,c_2419,c_2240]) ).
tff(c_68416,plain,
! [X5_6] : ( inverse(X5_6) != identity ),
inference(splitLeft,[status(thm)],[c_68415]) ).
tff(c_2428,plain,
inverse(sk_c8) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2419,c_483]) ).
tff(c_2450,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2434,c_2428]) ).
tff(c_68418,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68416,c_2450]) ).
tff(c_68420,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_68415]) ).
tff(c_68422,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68420,c_2450]) ).
tff(c_68424,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_68485,plain,
! [X_372,Y_373,Z_374] : ( multiply(multiply(X_372,Y_373),Z_374) = multiply(X_372,multiply(Y_373,Z_374)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_68524,plain,
! [Z_374] : ( multiply(sk_c7,multiply(sk_c8,Z_374)) = multiply(identity,Z_374) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_68485]) ).
tff(c_68717,plain,
! [Z_380] : ( multiply(sk_c7,multiply(sk_c8,Z_380)) = Z_380 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68524]) ).
tff(c_68738,plain,
multiply(sk_c7,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_68717]) ).
tff(c_28,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_68432,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_68438,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_68432,c_68424]) ).
tff(c_68439,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_68444,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68439,c_4]) ).
tff(c_68732,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_68444,c_68717]) ).
tff(c_68776,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_68738,c_68732]) ).
tff(c_30,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_68479,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_68424,c_30]) ).
tff(c_68777,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_68776,c_68479]) ).
tff(c_68781,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68424,c_68777]) ).
tff(c_68783,plain,
multiply(sk_c2,sk_c3) != sk_c7,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_42,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_69771,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_68783,c_42]) ).
tff(c_69787,plain,
! [X_399,Y_400,Z_401] : ( multiply(multiply(X_399,Y_400),Z_401) = multiply(X_399,multiply(Y_400,Z_401)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_69823,plain,
! [Z_401] : ( multiply(sk_c7,multiply(sk_c8,Z_401)) = multiply(identity,Z_401) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_69787]) ).
tff(c_69867,plain,
! [Z_403] : ( multiply(sk_c7,multiply(sk_c8,Z_403)) = Z_403 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69823]) ).
tff(c_69885,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_69771,c_69867]) ).
tff(c_69894,plain,
multiply(sk_c7,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_69867]) ).
tff(c_68782,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_68787,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68782,c_4]) ).
tff(c_69891,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_68787,c_69867]) ).
tff(c_70079,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_69894,c_69891]) ).
tff(c_68832,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_68783,c_42]) ).
tff(c_68849,plain,
! [X_382,Y_383,Z_384] : ( multiply(multiply(X_382,Y_383),Z_384) = multiply(X_382,multiply(Y_383,Z_384)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_68888,plain,
! [Z_384] : ( multiply(sk_c7,multiply(sk_c8,Z_384)) = multiply(identity,Z_384) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_68849]) ).
tff(c_69250,plain,
! [Z_392] : ( multiply(sk_c7,multiply(sk_c8,Z_392)) = Z_392 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68888]) ).
tff(c_69268,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_68832,c_69250]) ).
tff(c_69277,plain,
multiply(sk_c7,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_69250]) ).
tff(c_69274,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_68787,c_69250]) ).
tff(c_69467,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_69277,c_69274]) ).
tff(c_44,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c2,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_68844,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_68783,c_44]) ).
tff(c_69468,plain,
multiply(sk_c1,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_69467,c_68844]) ).
tff(c_68885,plain,
! [Z_384] : ( multiply(sk_c8,multiply(sk_c1,Z_384)) = multiply(identity,Z_384) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_68849]) ).
tff(c_68904,plain,
! [Z_384] : ( multiply(sk_c8,multiply(sk_c1,Z_384)) = Z_384 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68885]) ).
tff(c_69491,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69468,c_68904]) ).
tff(c_69497,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_68832,c_69491]) ).
tff(c_68820,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_68909,plain,
! [Z_385] : ( multiply(sk_c8,multiply(sk_c1,Z_385)) = Z_385 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_68885]) ).
tff(c_68921,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_68820,c_68909]) ).
tff(c_69502,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_69497,c_69497,c_68921]) ).
tff(c_69511,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_69268,c_69502]) ).
tff(c_69509,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69497,c_102]) ).
tff(c_69563,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69511,c_69511,c_69509]) ).
tff(c_69504,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_69497,c_68832]) ).
tff(c_69572,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69563,c_69511,c_69511,c_69504]) ).
tff(c_69510,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_69497,c_98]) ).
tff(c_69538,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_69511,c_69511,c_69510]) ).
tff(c_69576,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69572,c_69572,c_69538]) ).
tff(c_69579,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69572,c_69511]) ).
tff(c_64,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_68827,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_64]) ).
tff(c_69435,plain,
! [Z_395] : ( multiply(sk_c3,multiply(sk_c8,Z_395)) = multiply(sk_c7,Z_395) ),
inference(superposition,[status(thm),theory(equality)],[c_68827,c_68849]) ).
tff(c_69447,plain,
multiply(sk_c7,sk_c8) = multiply(sk_c3,sk_c7),
inference(superposition,[status(thm),theory(equality)],[c_68921,c_69435]) ).
tff(c_69466,plain,
multiply(sk_c3,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_102,c_69447]) ).
tff(c_69699,plain,
multiply(sk_c3,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69579,c_69466]) ).
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_69706,plain,
! [Z_5] : ( multiply(sk_c3,multiply(identity,Z_5)) = multiply(identity,Z_5) ),
inference(superposition,[status(thm),theory(equality)],[c_69699,c_6]) ).
tff(c_69715,plain,
! [Z_398] : ( multiply(sk_c3,Z_398) = Z_398 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2,c_69706]) ).
tff(c_89,plain,
multiply(sk_c3,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_69730,plain,
sk_c2 = identity,
inference(superposition,[status(thm),theory(equality)],[c_69715,c_89]) ).
tff(c_69746,plain,
inverse(identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_69730,c_85]) ).
tff(c_69750,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_69576,c_69746]) ).
tff(c_69519,plain,
multiply(sk_c2,sk_c3) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_69511,c_68783]) ).
tff(c_69693,plain,
multiply(sk_c2,sk_c3) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_69572,c_69519]) ).
tff(c_69743,plain,
multiply(identity,sk_c3) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_69730,c_69693]) ).
tff(c_69747,plain,
sk_c3 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69743]) ).
tff(c_69764,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_69750,c_69747]) ).
tff(c_69765,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(splitRight,[status(thm)],[c_64]) ).
tff(c_70080,plain,
multiply(sk_c1,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_70079,c_69765]) ).
tff(c_69820,plain,
! [Z_401] : ( multiply(sk_c8,multiply(sk_c1,Z_401)) = multiply(identity,Z_401) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_69787]) ).
tff(c_69839,plain,
! [Z_401] : ( multiply(sk_c8,multiply(sk_c1,Z_401)) = Z_401 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69820]) ).
tff(c_70103,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_70080,c_69839]) ).
tff(c_70109,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_69771,c_70103]) ).
tff(c_69844,plain,
! [Z_402] : ( multiply(sk_c8,multiply(sk_c1,Z_402)) = Z_402 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69820]) ).
tff(c_69856,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_68820,c_69844]) ).
tff(c_70217,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70109,c_70109,c_69856]) ).
tff(c_70226,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_69885,c_70217]) ).
tff(c_70231,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_70226,c_70109]) ).
tff(c_69879,plain,
multiply(sk_c7,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_69856,c_69867]) ).
tff(c_70273,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_70231,c_70226,c_70226,c_69879]) ).
tff(c_70224,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_70109,c_102]) ).
tff(c_70309,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_70273,c_70226,c_70226,c_70224]) ).
tff(c_70234,plain,
multiply(sk_c2,sk_c3) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_70226,c_68783]) ).
tff(c_70312,plain,
multiply(sk_c2,sk_c3) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_70309,c_70234]) ).
tff(c_69829,plain,
! [X_2,Z_401] : ( multiply(inverse(X_2),multiply(X_2,Z_401)) = multiply(identity,Z_401) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_69787]) ).
tff(c_70350,plain,
! [X_409,Z_410] : ( multiply(inverse(X_409),multiply(X_409,Z_410)) = Z_410 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69829]) ).
tff(c_69842,plain,
! [X_2,Z_401] : ( multiply(inverse(X_2),multiply(X_2,Z_401)) = Z_401 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_69829]) ).
tff(c_70512,plain,
! [X_414,Z_415] : ( multiply(inverse(inverse(X_414)),Z_415) = multiply(X_414,Z_415) ),
inference(superposition,[status(thm),theory(equality)],[c_70350,c_69842]) ).
tff(c_70377,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_70350]) ).
tff(c_70576,plain,
! [X_416] : ( multiply(X_416,identity) = X_416 ),
inference(superposition,[status(thm),theory(equality)],[c_70512,c_70377]) ).
tff(c_70371,plain,
multiply(inverse(sk_c3),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_89,c_70350]) ).
tff(c_70597,plain,
inverse(sk_c3) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_70576,c_70371]) ).
tff(c_70679,plain,
multiply(sk_c2,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_70597,c_4]) ).
tff(c_70686,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_70312,c_70679]) ).
tff(c_70688,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_70720,plain,
! [X_417,Y_418,Z_419] : ( multiply(multiply(X_417,Y_418),Z_419) = multiply(X_417,multiply(Y_418,Z_419)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_70753,plain,
! [Z_419] : ( multiply(sk_c7,multiply(sk_c8,Z_419)) = multiply(identity,Z_419) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_70720]) ).
tff(c_70803,plain,
! [Z_422] : ( multiply(sk_c7,multiply(sk_c8,Z_422)) = Z_422 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70753]) ).
tff(c_70827,plain,
multiply(sk_c7,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_115,c_70803]) ).
tff(c_38,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c3) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_68799,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_68783,c_38]) ).
tff(c_68803,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_68799,c_4]) ).
tff(c_70821,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_68803,c_70803]) ).
tff(c_70885,plain,
sk_c4 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_70827,c_70821]) ).
tff(c_70687,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_70886,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_70885,c_70687]) ).
tff(c_70890,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_70688,c_70886]) ).
tff(c_70892,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_22,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_70938,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_70892,c_22]) ).
tff(c_70952,plain,
! [X_424,Y_425,Z_426] : ( multiply(multiply(X_424,Y_425),Z_426) = multiply(X_424,multiply(Y_425,Z_426)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_70982,plain,
! [Z_426] : ( multiply(sk_c7,multiply(sk_c8,Z_426)) = multiply(identity,Z_426) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_70952]) ).
tff(c_71002,plain,
! [Z_427] : ( multiply(sk_c7,multiply(sk_c8,Z_427)) = Z_427 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70982]) ).
tff(c_71014,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_70938,c_71002]) ).
tff(c_18,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_70900,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_70892,c_18]) ).
tff(c_70904,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_70900,c_4]) ).
tff(c_71017,plain,
multiply(sk_c7,identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_70904,c_71002]) ).
tff(c_70891,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_70896,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_70891,c_4]) ).
tff(c_71020,plain,
multiply(sk_c7,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_70896,c_71002]) ).
tff(c_71300,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_71017,c_71020]) ).
tff(c_24,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_70929,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_70892,c_24]) ).
tff(c_71301,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_71300,c_70929]) ).
tff(c_70979,plain,
! [Z_426] : ( multiply(sk_c8,multiply(sk_c5,Z_426)) = multiply(identity,Z_426) ),
inference(superposition,[status(thm),theory(equality)],[c_70896,c_70952]) ).
tff(c_70997,plain,
! [Z_426] : ( multiply(sk_c8,multiply(sk_c5,Z_426)) = Z_426 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70979]) ).
tff(c_71449,plain,
! [Z_439] : ( multiply(sk_c8,multiply(sk_c4,Z_439)) = Z_439 ),
inference(demodulation,[status(thm),theory(equality)],[c_71300,c_70997]) ).
tff(c_71464,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_71301,c_71449]) ).
tff(c_71471,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70938,c_71464]) ).
tff(c_20,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_70917,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_70892,c_20]) ).
tff(c_71467,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_70917,c_71449]) ).
tff(c_77545,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_71014,c_71471,c_71471,c_71467]) ).
tff(c_77553,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_77545,c_77545,c_71014]) ).
tff(c_70988,plain,
! [X_2,Z_426] : ( multiply(inverse(X_2),multiply(X_2,Z_426)) = multiply(identity,Z_426) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_70952]) ).
tff(c_71000,plain,
! [X_2,Z_426] : ( multiply(inverse(X_2),multiply(X_2,Z_426)) = Z_426 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70988]) ).
tff(c_77623,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_77553,c_71000]) ).
tff(c_77629,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_77623]) ).
tff(c_77636,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_77629,c_77545]) ).
tff(c_77576,plain,
! [X_504,Z_505] : ( multiply(inverse(X_504),multiply(X_504,Z_505)) = Z_505 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70988]) ).
tff(c_77778,plain,
! [X_508,Z_509] : ( multiply(inverse(inverse(X_508)),Z_509) = multiply(X_508,Z_509) ),
inference(superposition,[status(thm),theory(equality)],[c_71000,c_77576]) ).
tff(c_77612,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_77576]) ).
tff(c_77788,plain,
! [X_508] : ( multiply(X_508,identity) = X_508 ),
inference(superposition,[status(thm),theory(equality)],[c_77778,c_77612]) ).
tff(c_71596,plain,
! [X_441,Z_442] : ( multiply(inverse(X_441),multiply(X_441,Z_442)) = Z_442 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_70988]) ).
tff(c_71758,plain,
! [X_444,Z_445] : ( multiply(inverse(inverse(X_444)),Z_445) = multiply(X_444,Z_445) ),
inference(superposition,[status(thm),theory(equality)],[c_71000,c_71596]) ).
tff(c_71805,plain,
! [X_444] : ( multiply(X_444,inverse(X_444)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_71758]) ).
tff(c_71533,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_71014,c_71471,c_71471,c_71467]) ).
tff(c_71497,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71471,c_102]) ).
tff(c_71574,plain,
multiply(sk_c6,sk_c6) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71533,c_71533,c_71497]) ).
tff(c_71541,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_71533,c_71533,c_71014]) ).
tff(c_71583,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71574,c_71541]) ).
tff(c_71590,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71583,c_71533]) ).
tff(c_71626,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_71596]) ).
tff(c_71768,plain,
! [X_444] : ( multiply(X_444,identity) = X_444 ),
inference(superposition,[status(thm),theory(equality)],[c_71758,c_71626]) ).
tff(c_71332,plain,
! [Z_435] : ( multiply(sk_c8,multiply(sk_c4,Z_435)) = Z_435 ),
inference(demodulation,[status(thm),theory(equality)],[c_71300,c_70997]) ).
tff(c_71347,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_71301,c_71332]) ).
tff(c_71354,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70938,c_71347]) ).
tff(c_71375,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_71354,c_70938]) ).
tff(c_71381,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_71354,c_98]) ).
tff(c_71042,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_71017,c_71020]) ).
tff(c_71043,plain,
multiply(sk_c4,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_71042,c_70929]) ).
tff(c_71098,plain,
! [Z_430] : ( multiply(sk_c8,multiply(sk_c4,Z_430)) = Z_430 ),
inference(demodulation,[status(thm),theory(equality)],[c_71042,c_70997]) ).
tff(c_71116,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_71043,c_71098]) ).
tff(c_71123,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_70938,c_71116]) ).
tff(c_71133,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71123,c_102]) ).
tff(c_71171,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71133,c_71014]) ).
tff(c_71128,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_71123,c_70938]) ).
tff(c_71197,plain,
sk_c7 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_71017,c_71171,c_71128]) ).
tff(c_71134,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_71123,c_98]) ).
tff(c_71032,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c8 )
| ( inverse(X4_11) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_98,c_68]) ).
tff(c_71033,plain,
! [X4_11] :
( ( multiply(X4_11,sk_c7) != sk_c8 )
| ( inverse(X4_11) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_71032]) ).
tff(c_71146,plain,
! [X4_11] :
( ( multiply(X4_11,sk_c7) != sk_c7 )
| ( inverse(X4_11) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_71123,c_71123,c_71033]) ).
tff(c_71175,plain,
( ( sk_c7 != identity )
| ( inverse(sk_c7) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_71133,c_71146]) ).
tff(c_71182,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_71134,c_71175]) ).
tff(c_71198,plain,
sk_c4 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_71197,c_71182]) ).
tff(c_71202,plain,
inverse(sk_c4) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_71197,c_71197,c_71134]) ).
tff(c_71260,plain,
multiply(sk_c4,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_71202,c_4]) ).
tff(c_71206,plain,
sk_c8 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_71197,c_71123]) ).
tff(c_71119,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_70917,c_71098]) ).
tff(c_71289,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71260,c_71206,c_71206,c_71197,c_71119]) ).
tff(c_71290,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_71198,c_71289]) ).
tff(c_71291,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_71032]) ).
tff(c_71310,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_71291]) ).
tff(c_71408,plain,
! [X3_437] :
( ( inverse(X3_437) != sk_c7 )
| ( multiply(sk_c7,multiply(X3_437,sk_c7)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_71354,c_71354,c_71354,c_71310]) ).
tff(c_71411,plain,
( ( inverse(sk_c7) != sk_c7 )
| ( multiply(sk_c7,sk_c6) != sk_c7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_71014,c_71408]) ).
tff(c_71426,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_71375,c_71381,c_71411]) ).
tff(c_71427,plain,
! [X1_9,X5_6] :
( ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_71291]) ).
tff(c_71524,plain,
! [X1_9,X5_6] :
( ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(inverse(X5_6),sk_c7) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_71471,c_71471,c_71471,c_71427]) ).
tff(c_71525,plain,
! [X5_6] :
( ( multiply(inverse(X5_6),sk_c7) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_71524]) ).
tff(c_77533,plain,
! [X5_6] : ( inverse(X5_6) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_71805,c_71590,c_71768,c_71590,c_71590,c_71525]) ).
tff(c_71498,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_71471,c_98]) ).
tff(c_71536,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_71533,c_71533,c_71498]) ).
tff(c_71587,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_71583,c_71583,c_71536]) ).
tff(c_77535,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_77533,c_71587]) ).
tff(c_77536,plain,
! [X1_9] :
( ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_71524]) ).
tff(c_78488,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_77636,c_77788,c_77636,c_77636,c_77536]) ).
tff(c_77548,plain,
inverse(sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_77545,c_77545,c_71498]) ).
tff(c_77634,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_77629,c_77629,c_77548]) ).
tff(c_78490,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_78488,c_77634]) ).
tff(c_78492,plain,
inverse(sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_12,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_78531,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_78492,c_12]) ).
tff(c_14,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_78550,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_78492,c_14]) ).
tff(c_16,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_78517,plain,
inverse(sk_c5) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_78492,c_16]) ).
tff(c_78521,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_78517,c_4]) ).
tff(c_78565,plain,
! [X_521,Y_522,Z_523] : ( multiply(multiply(X_521,Y_522),Z_523) = multiply(X_521,multiply(Y_522,Z_523)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_78589,plain,
! [Z_523] : ( multiply(sk_c8,multiply(sk_c5,Z_523)) = multiply(identity,Z_523) ),
inference(superposition,[status(thm),theory(equality)],[c_78521,c_78565]) ).
tff(c_78615,plain,
! [Z_524] : ( multiply(sk_c8,multiply(sk_c5,Z_524)) = Z_524 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_78589]) ).
tff(c_78627,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_78550,c_78615]) ).
tff(c_78631,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78531,c_78627]) ).
tff(c_78635,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78631,c_78531]) ).
tff(c_78601,plain,
! [X_2,Z_523] : ( multiply(inverse(X_2),multiply(X_2,Z_523)) = multiply(identity,Z_523) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_78565]) ).
tff(c_78613,plain,
! [X_2,Z_523] : ( multiply(inverse(X_2),multiply(X_2,Z_523)) = Z_523 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_78601]) ).
tff(c_78759,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_78635,c_78613]) ).
tff(c_78765,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_78759]) ).
tff(c_78637,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78631,c_78517]) ).
tff(c_78633,plain,
multiply(sk_c5,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_78631,c_78550]) ).
tff(c_78725,plain,
multiply(inverse(sk_c5),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_78633,c_78613]) ).
tff(c_78731,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78637,c_78725]) ).
tff(c_78814,plain,
multiply(sk_c7,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78765,c_78731]) ).
tff(c_78491,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_78642,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78631,c_78491]) ).
tff(c_78496,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_78491,c_4]) ).
tff(c_78640,plain,
multiply(sk_c7,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_78631,c_78496]) ).
tff(c_10,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_78536,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_78492,c_10]) ).
tff(c_78583,plain,
! [Z_523] : ( multiply(sk_c4,multiply(sk_c7,Z_523)) = multiply(sk_c8,Z_523) ),
inference(superposition,[status(thm),theory(equality)],[c_78536,c_78565]) ).
tff(c_78785,plain,
! [Z_527] : ( multiply(sk_c4,multiply(sk_c7,Z_527)) = multiply(sk_c7,Z_527) ),
inference(demodulation,[status(thm),theory(equality)],[c_78631,c_78583]) ).
tff(c_78806,plain,
multiply(sk_c7,sk_c4) = multiply(sk_c4,identity),
inference(superposition,[status(thm),theory(equality)],[c_78640,c_78785]) ).
tff(c_78813,plain,
multiply(sk_c4,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_78640,c_78806]) ).
tff(c_78834,plain,
multiply(inverse(sk_c4),identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_78813,c_78613]) ).
tff(c_78840,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_78814,c_78642,c_78834]) ).
tff(c_78657,plain,
multiply(sk_c7,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_78642,c_4]) ).
tff(c_78861,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_78840,c_78657]) ).
tff(c_78850,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_78840,c_78642]) ).
tff(c_78872,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_78861,c_78850]) ).
tff(c_78641,plain,
inverse(sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78631,c_78492]) ).
tff(c_78851,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_78840,c_78840,c_78641]) ).
tff(c_78896,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_78872,c_78851]) ).
tff(c_78898,plain,
inverse(sk_c2) != sk_c3,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_52,plain,
( ( multiply(sk_c8,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_87490,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_78898,c_52]) ).
tff(c_78984,plain,
! [X_528,Y_529,Z_530] : ( multiply(multiply(X_528,Y_529),Z_530) = multiply(X_528,multiply(Y_529,Z_530)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_79020,plain,
! [X_2,Z_530] : ( multiply(inverse(X_2),multiply(X_2,Z_530)) = multiply(identity,Z_530) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_78984]) ).
tff(c_80768,plain,
! [X_562,Z_563] : ( multiply(inverse(X_562),multiply(X_562,Z_563)) = Z_563 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_79020]) ).
tff(c_79032,plain,
! [X_2,Z_530] : ( multiply(inverse(X_2),multiply(X_2,Z_530)) = Z_530 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_79020]) ).
tff(c_81011,plain,
! [X_566,Z_567] : ( multiply(inverse(inverse(X_566)),Z_567) = multiply(X_566,Z_567) ),
inference(superposition,[status(thm),theory(equality)],[c_80768,c_79032]) ).
tff(c_81032,plain,
! [X_566] : ( multiply(X_566,inverse(X_566)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_81011,c_4]) ).
tff(c_78964,plain,
multiply(sk_c8,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_78898,c_52]) ).
tff(c_54,plain,
( ( multiply(sk_c5,sk_c8) = sk_c6 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_78954,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_78898,c_54]) ).
tff(c_78897,plain,
inverse(sk_c5) = sk_c8,
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_78902,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_78897,c_4]) ).
tff(c_79017,plain,
! [Z_530] : ( multiply(sk_c8,multiply(sk_c5,Z_530)) = multiply(identity,Z_530) ),
inference(superposition,[status(thm),theory(equality)],[c_78902,c_78984]) ).
tff(c_79057,plain,
! [Z_532] : ( multiply(sk_c8,multiply(sk_c5,Z_532)) = Z_532 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_79017]) ).
tff(c_79069,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_78954,c_79057]) ).
tff(c_79073,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_78964,c_79069]) ).
tff(c_78910,plain,
inverse(sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_78914,plain,
multiply(sk_c7,sk_c8) = identity,
inference(superposition,[status(thm),theory(equality)],[c_78910,c_4]) ).
tff(c_79186,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_79073,c_78914]) ).
tff(c_50,plain,
( ( multiply(sk_c4,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_78959,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_78898,c_50]) ).
tff(c_48,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_78934,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_78898,c_48]) ).
tff(c_78938,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_78934,c_4]) ).
tff(c_79008,plain,
! [Z_530] : ( multiply(sk_c8,multiply(sk_c4,Z_530)) = multiply(identity,Z_530) ),
inference(superposition,[status(thm),theory(equality)],[c_78938,c_78984]) ).
tff(c_79034,plain,
! [Z_531] : ( multiply(sk_c8,multiply(sk_c4,Z_531)) = Z_531 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_79008]) ).
tff(c_79046,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_78959,c_79034]) ).
tff(c_79178,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_79073,c_79073,c_79046]) ).
tff(c_80730,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_79186,c_79178]) ).
tff(c_80792,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_80768]) ).
tff(c_81018,plain,
! [X_566] : ( multiply(X_566,identity) = X_566 ),
inference(superposition,[status(thm),theory(equality)],[c_81011,c_80792]) ).
tff(c_79317,plain,
! [X_534,Z_535] : ( multiply(inverse(X_534),multiply(X_534,Z_535)) = Z_535 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_79020]) ).
tff(c_79560,plain,
! [X_538,Z_539] : ( multiply(inverse(inverse(X_538)),Z_539) = multiply(X_538,Z_539) ),
inference(superposition,[status(thm),theory(equality)],[c_79317,c_79032]) ).
tff(c_79341,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_79317]) ).
tff(c_79567,plain,
! [X_538] : ( multiply(X_538,identity) = X_538 ),
inference(superposition,[status(thm),theory(equality)],[c_79560,c_79341]) ).
tff(c_79279,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_79186,c_79178]) ).
tff(c_79084,plain,
inverse(sk_c4) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_79073,c_78934]) ).
tff(c_79081,plain,
multiply(sk_c4,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_79073,c_78959]) ).
tff(c_79075,plain,
! [X3_8,X1_9,X5_6,X4_11] :
( ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X4_11,sk_c7) != sk_c8 )
| ( inverse(X4_11) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_78910,c_68]) ).
tff(c_79076,plain,
! [X4_11] :
( ( multiply(X4_11,sk_c7) != sk_c8 )
| ( inverse(X4_11) != sk_c8 ) ),
inference(splitLeft,[status(thm)],[c_79075]) ).
tff(c_79153,plain,
! [X4_533] :
( ( multiply(X4_533,sk_c7) != sk_c7 )
| ( inverse(X4_533) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_79073,c_79073,c_79076]) ).
tff(c_79156,plain,
inverse(sk_c4) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_79081,c_79153]) ).
tff(c_79175,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_79084,c_79156]) ).
tff(c_79176,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),sk_c8) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c8 )
| ( inverse(X1_9) != sk_c8 )
| ( inverse(X3_8) != sk_c8 )
| ( multiply(sk_c8,multiply(X3_8,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_79075]) ).
tff(c_79252,plain,
! [X5_6,X1_9,X3_8] :
( ( multiply(inverse(X5_6),sk_c7) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 )
| ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( inverse(X3_8) != sk_c7 )
| ( multiply(sk_c7,multiply(X3_8,sk_c7)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_79073,c_79073,c_79073,c_79073,c_79073,c_79073,c_79176]) ).
tff(c_79253,plain,
! [X3_8] :
( ( inverse(X3_8) != sk_c7 )
| ( multiply(sk_c7,multiply(X3_8,sk_c7)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_79252]) ).
tff(c_80701,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_79567,c_79279,c_79279,c_2,c_79279,c_79279,c_79253]) ).
tff(c_79188,plain,
inverse(sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_79073,c_78910]) ).
tff(c_79295,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_79279,c_79279,c_79188]) ).
tff(c_80703,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_80701,c_79295]) ).
tff(c_80704,plain,
! [X1_9,X5_6] :
( ( multiply(X1_9,sk_c7) != sk_c7 )
| ( inverse(X1_9) != sk_c7 )
| ( multiply(inverse(X5_6),sk_c7) != sk_c7 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_79252]) ).
tff(c_87435,plain,
! [X1_9,X5_6] :
( ( identity != X1_9 )
| ( inverse(X1_9) != identity )
| ( inverse(X5_6) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_81032,c_80730,c_81018,c_80730,c_80730,c_80730,c_81018,c_80730,c_80730,c_80704]) ).
tff(c_87436,plain,
! [X5_6] : ( inverse(X5_6) != identity ),
inference(splitLeft,[status(thm)],[c_87435]) ).
tff(c_80746,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_80730,c_80730,c_79188]) ).
tff(c_87438,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_87436,c_80746]) ).
tff(c_87440,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_87435]) ).
tff(c_87442,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_87440,c_80746]) ).
tff(c_87444,plain,
inverse(sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_87475,plain,
multiply(sk_c5,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_87444,c_14]) ).
tff(c_87512,plain,
! [X_645,Y_646,Z_647] : ( multiply(multiply(X_645,Y_646),Z_647) = multiply(X_645,multiply(Y_646,Z_647)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_87542,plain,
! [Z_647] : ( multiply(sk_c8,multiply(sk_c5,Z_647)) = multiply(identity,Z_647) ),
inference(superposition,[status(thm),theory(equality)],[c_78902,c_87512]) ).
tff(c_87581,plain,
! [Z_649] : ( multiply(sk_c8,multiply(sk_c5,Z_649)) = Z_649 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_87542]) ).
tff(c_87593,plain,
multiply(sk_c8,sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_87475,c_87581]) ).
tff(c_87597,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_87490,c_87593]) ).
tff(c_87485,plain,
multiply(sk_c4,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_78898,c_50]) ).
tff(c_87443,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_87448,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87443,c_4]) ).
tff(c_87539,plain,
! [Z_647] : ( multiply(sk_c8,multiply(sk_c4,Z_647)) = multiply(identity,Z_647) ),
inference(superposition,[status(thm),theory(equality)],[c_87448,c_87512]) ).
tff(c_87558,plain,
! [Z_648] : ( multiply(sk_c8,multiply(sk_c4,Z_648)) = Z_648 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_87539]) ).
tff(c_87570,plain,
multiply(sk_c8,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_87485,c_87558]) ).
tff(c_87599,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_87597,c_87597,c_87570]) ).
tff(c_87545,plain,
! [X_2,Z_647] : ( multiply(inverse(X_2),multiply(X_2,Z_647)) = multiply(identity,Z_647) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_87512]) ).
tff(c_87665,plain,
! [X_650,Z_651] : ( multiply(inverse(X_650),multiply(X_650,Z_651)) = Z_651 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_87545]) ).
tff(c_87683,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_87599,c_87665]) ).
tff(c_87714,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_87683]) ).
tff(c_87607,plain,
inverse(sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_87597,c_87444]) ).
tff(c_87724,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_87714,c_87714,c_87607]) ).
tff(c_87610,plain,
inverse(sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_87597,c_78897]) ).
tff(c_87633,plain,
multiply(sk_c7,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87610,c_4]) ).
tff(c_87739,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_87714,c_87633]) ).
tff(c_87721,plain,
inverse(sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_87714,c_87610]) ).
tff(c_87754,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_87739,c_87721]) ).
tff(c_87755,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_87724,c_87754]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP235-1 : TPTP v9.0.0. Released v2.5.0.
% 0.04/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.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:38:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 20.04/9.80 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.04/9.85
% 20.04/9.85 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------