%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP351-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 06:26:01 PM UTC 2025
% Result : Unsatisfiable 11.48s 3.89s
% Output : CNFRefutation 12.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 26
% Syntax : Number of formulae : 340 ( 271 unt; 0 typ; 0 def)
% Number of atoms : 513 ( 492 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 361 ( 188 ~; 173 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 177 ( 177 !; 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_116,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c3) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_167,axiom,
! [X3,X4,X1,X2] :
( ( multiply(sk_c6,sk_c5) != sk_c7 )
| ( 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 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( inverse(X1) != sk_c6 )
| ( inverse(X2) != sk_c5 )
| ( multiply(X2,sk_c6) != sk_c5 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c6,sk_c5) = sk_c7 )
| ( inverse(sk_c3) = 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_113,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c5 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c6) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c5 ) ),
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_16578,plain,
! [X_231,Y_232,Z_233] : ( multiply(multiply(X_231,Y_232),Z_233) = multiply(X_231,multiply(Y_232,Z_233)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_16611,plain,
! [X_2,Z_233] : ( multiply(inverse(X_2),multiply(X_2,Z_233)) = multiply(identity,Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16578]) ).
tff(c_17766,plain,
! [X_253,Z_254] : ( multiply(inverse(X_253),multiply(X_253,Z_254)) = Z_254 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16611]) ).
tff(c_16622,plain,
! [X_2,Z_233] : ( multiply(inverse(X_2),multiply(X_2,Z_233)) = Z_233 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16611]) ).
tff(c_18077,plain,
! [X_257,Z_258] : ( multiply(inverse(inverse(X_257)),Z_258) = multiply(X_257,Z_258) ),
inference(superposition,[status(thm),theory(equality)],[c_17766,c_16622]) ).
tff(c_17814,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17766]) ).
tff(c_18084,plain,
! [X_257] : ( multiply(X_257,identity) = X_257 ),
inference(superposition,[status(thm),theory(equality)],[c_18077,c_17814]) ).
tff(c_42,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_103,plain,
multiply(sk_c2,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_52,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_75,plain,
inverse(sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_52]) ).
tff(c_79,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_75,c_4]) ).
tff(c_4124,plain,
! [X_82,Y_83,Z_84] : ( multiply(multiply(X_82,Y_83),Z_84) = multiply(X_82,multiply(Y_83,Z_84)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4163,plain,
! [Z_84] : ( multiply(sk_c6,multiply(sk_c2,Z_84)) = multiply(identity,Z_84) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_4124]) ).
tff(c_4203,plain,
! [Z_86] : ( multiply(sk_c6,multiply(sk_c2,Z_86)) = Z_86 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4163]) ).
tff(c_4215,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_103,c_4203]) ).
tff(c_3774,plain,
! [X_75,Y_76,Z_77] : ( multiply(multiply(X_75,Y_76),Z_77) = multiply(X_75,multiply(Y_76,Z_77)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_3813,plain,
! [Z_77] : ( multiply(sk_c6,multiply(sk_c2,Z_77)) = multiply(identity,Z_77) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_3774]) ).
tff(c_3843,plain,
! [Z_79] : ( multiply(sk_c6,multiply(sk_c2,Z_79)) = Z_79 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3813]) ).
tff(c_3855,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_103,c_3843]) ).
tff(c_3816,plain,
! [X_2,Z_77] : ( multiply(inverse(X_2),multiply(X_2,Z_77)) = multiply(identity,Z_77) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_3774]) ).
tff(c_3920,plain,
! [X_80,Z_81] : ( multiply(inverse(X_80),multiply(X_80,Z_81)) = Z_81 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_3816]) ).
tff(c_3944,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_3855,c_3920]) ).
tff(c_3984,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_3944]) ).
tff(c_24,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_3725,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_135,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_165,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_135]) ).
tff(c_175,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_165]) ).
tff(c_866,plain,
! [X_26,Z_27] : ( multiply(inverse(X_26),multiply(X_26,Z_27)) = Z_27 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_165]) ).
tff(c_1162,plain,
! [X_32,Z_33] : ( multiply(inverse(inverse(X_32)),Z_33) = multiply(X_32,Z_33) ),
inference(superposition,[status(thm),theory(equality)],[c_175,c_866]) ).
tff(c_887,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_866]) ).
tff(c_1173,plain,
! [X_32] : ( multiply(X_32,identity) = X_32 ),
inference(superposition,[status(thm),theory(equality)],[c_1162,c_887]) ).
tff(c_162,plain,
! [Z_14] : ( multiply(sk_c6,multiply(sk_c2,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_135]) ).
tff(c_200,plain,
! [Z_16] : ( multiply(sk_c6,multiply(sk_c2,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_162]) ).
tff(c_212,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_103,c_200]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_108,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_482,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_212,c_108]) ).
tff(c_219,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_212,c_108]) ).
tff(c_22,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_115,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_32,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_87,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_91,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_87,c_4]) ).
tff(c_159,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_91,c_135]) ).
tff(c_177,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_159]) ).
tff(c_189,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_115,c_177]) ).
tff(c_228,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_219,c_219,c_189]) ).
tff(c_327,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_228,c_175]) ).
tff(c_333,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_327]) ).
tff(c_251,plain,
! [X_17,Z_18] : ( multiply(inverse(X_17),multiply(X_17,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_165]) ).
tff(c_275,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_212,c_251]) ).
tff(c_301,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_275]) ).
tff(c_58,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X2_9) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != 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_c6,sk_c5) != sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_217,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X2_9) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != 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_108,c_58]) ).
tff(c_218,plain,
multiply(sk_c6,sk_c7) != sk_c5,
inference(splitLeft,[status(thm)],[c_217]) ).
tff(c_227,plain,
multiply(sk_c6,sk_c6) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_219,c_218]) ).
tff(c_310,plain,
multiply(sk_c6,sk_c6) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_301,c_227]) ).
tff(c_323,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_228,c_310]) ).
tff(c_353,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_333,c_323]) ).
tff(c_355,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(splitRight,[status(thm)],[c_217]) ).
tff(c_490,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_482,c_355]) ).
tff(c_491,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_482,c_482,c_189]) ).
tff(c_851,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_490,c_491]) ).
tff(c_852,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_851,c_851,c_490]) ).
tff(c_945,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_852,c_175]) ).
tff(c_951,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_945]) ).
tff(c_959,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_951,c_851]) ).
tff(c_531,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_490,c_491]) ).
tff(c_532,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_531,c_531,c_490]) ).
tff(c_637,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_532,c_175]) ).
tff(c_643,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_637]) ).
tff(c_541,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_531,c_75]) ).
tff(c_570,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_541,c_4]) ).
tff(c_658,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_643,c_570]) ).
tff(c_648,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_643,c_541]) ).
tff(c_681,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_658,c_648]) ).
tff(c_589,plain,
! [X_20,Z_21] : ( multiply(inverse(X_20),multiply(X_20,Z_21)) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_165]) ).
tff(c_752,plain,
! [X_23] : ( multiply(inverse(inverse(X_23)),identity) = X_23 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_589]) ).
tff(c_758,plain,
! [X_23] : ( multiply(inverse(inverse(inverse(X_23))),X_23) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_752,c_175]) ).
tff(c_652,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_643,c_531]) ).
tff(c_364,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_212,c_108]) ).
tff(c_372,plain,
multiply(sk_c6,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_364,c_355]) ).
tff(c_373,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_364,c_364,c_189]) ).
tff(c_412,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_372,c_373]) ).
tff(c_422,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_412,c_75]) ).
tff(c_420,plain,
multiply(sk_c2,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_412,c_103]) ).
tff(c_354,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 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_217]) ).
tff(c_363,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_354]) ).
tff(c_431,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_412,c_363]) ).
tff(c_471,plain,
inverse(sk_c2) != sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_420,c_431]) ).
tff(c_480,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_422,c_471]) ).
tff(c_481,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( 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(splitRight,[status(thm)],[c_354]) ).
tff(c_514,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c6 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_482,c_482,c_482,c_481]) ).
tff(c_515,plain,
! [X3_6] :
( ( inverse(X3_6) != sk_c6 )
| ( multiply(X3_6,sk_c6) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_514]) ).
tff(c_811,plain,
! [X3_25] :
( ( inverse(X3_25) != identity )
| ( multiply(X3_25,identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_652,c_652,c_652,c_515]) ).
tff(c_815,plain,
inverse(inverse(inverse(inverse(identity)))) != identity,
inference(superposition,[status(thm),theory(equality)],[c_758,c_811]) ).
tff(c_834,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_681,c_681,c_681,c_681,c_815]) ).
tff(c_835,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_514]) ).
tff(c_3707,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1173,c_959,c_959,c_959,c_1173,c_959,c_951,c_959,c_835]) ).
tff(c_3709,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_3707]) ).
tff(c_861,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_851,c_75]) ).
tff(c_904,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_861,c_4]) ).
tff(c_1012,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_951,c_904]) ).
tff(c_957,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_951,c_861]) ).
tff(c_1013,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1012,c_957]) ).
tff(c_3711,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3709,c_1013]) ).
tff(c_3713,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_3707]) ).
tff(c_3715,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3713,c_1013]) ).
tff(c_3717,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_3731,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3725,c_3717]) ).
tff(c_3732,plain,
inverse(sk_c4) = sk_c5,
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_26,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_3762,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_3717,c_26]) ).
tff(c_3953,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_3762,c_3920]) ).
tff(c_3985,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3732,c_3953]) ).
tff(c_4008,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_3984,c_2,c_3984,c_3985]) ).
tff(c_3859,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3855,c_108]) ).
tff(c_3872,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3859,c_87]) ).
tff(c_3909,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_3872,c_4]) ).
tff(c_4020,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4008,c_3909]) ).
tff(c_3870,plain,
multiply(sk_c1,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_3859,c_3717]) ).
tff(c_4066,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4020,c_4008,c_4008,c_3870]) ).
tff(c_4068,plain,
multiply(sk_c6,sk_c5) != sk_c7,
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_4219,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_4215,c_4068]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_4104,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_4068,c_8]) ).
tff(c_10,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_4119,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_4068,c_10]) ).
tff(c_12,plain,
( ( inverse(sk_c3) = sk_c6 )
| ( multiply(sk_c6,sk_c5) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_4091,plain,
inverse(sk_c3) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_4068,c_12]) ).
tff(c_4095,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4091,c_4]) ).
tff(c_4148,plain,
! [Z_84] : ( multiply(sk_c6,multiply(sk_c3,Z_84)) = multiply(identity,Z_84) ),
inference(superposition,[status(thm),theory(equality)],[c_4095,c_4124]) ).
tff(c_4230,plain,
! [Z_87] : ( multiply(sk_c6,multiply(sk_c3,Z_87)) = Z_87 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4148]) ).
tff(c_4242,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4119,c_4230]) ).
tff(c_4246,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4104,c_4242]) ).
tff(c_4285,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4246,c_4246,c_4215]) ).
tff(c_4166,plain,
! [X_2,Z_84] : ( multiply(inverse(X_2),multiply(X_2,Z_84)) = multiply(identity,Z_84) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4124]) ).
tff(c_4322,plain,
! [X_89,Z_90] : ( multiply(inverse(X_89),multiply(X_89,Z_90)) = Z_90 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4166]) ).
tff(c_4340,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_4285,c_4322]) ).
tff(c_4374,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_4340]) ).
tff(c_4228,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X2_9) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X4_7) != sk_c6 )
| ( multiply(X4_7,sk_c6) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c6 )
| ( sk_c7 != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_4215,c_4104,c_58]) ).
tff(c_4229,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_4228]) ).
tff(c_4284,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4246,c_4229]) ).
tff(c_4379,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_4374,c_4284]) ).
tff(c_4292,plain,
inverse(sk_c3) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4246,c_4091]) ).
tff(c_4304,plain,
multiply(sk_c5,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4292,c_4]) ).
tff(c_4392,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4374,c_4304]) ).
tff(c_4288,plain,
multiply(sk_c3,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_4246,c_4119]) ).
tff(c_4485,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4392,c_4374,c_4288]) ).
tff(c_4486,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4379,c_4485]) ).
tff(c_4488,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_4228]) ).
tff(c_4489,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4219,c_4488]) ).
tff(c_4491,plain,
multiply(sk_c2,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_42]) ).
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_4535,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_4491,c_38]) ).
tff(c_40,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_4540,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_4491,c_40]) ).
tff(c_4490,plain,
inverse(sk_c3) = sk_c6,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_4496,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4490,c_4]) ).
tff(c_4552,plain,
! [X_92,Y_93,Z_94] : ( multiply(multiply(X_92,Y_93),Z_94) = multiply(X_92,multiply(Y_93,Z_94)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_4582,plain,
! [Z_94] : ( multiply(sk_c6,multiply(sk_c3,Z_94)) = multiply(identity,Z_94) ),
inference(superposition,[status(thm),theory(equality)],[c_4496,c_4552]) ).
tff(c_5008,plain,
! [Z_108] : ( multiply(sk_c6,multiply(sk_c3,Z_108)) = Z_108 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4582]) ).
tff(c_5020,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4540,c_5008]) ).
tff(c_5024,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_4535,c_5020]) ).
tff(c_46,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_4547,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_4491,c_46]) ).
tff(c_44,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_4510,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_4491,c_44]) ).
tff(c_4514,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_4510,c_4]) ).
tff(c_4579,plain,
! [Z_94] : ( multiply(sk_c5,multiply(sk_c4,Z_94)) = multiply(identity,Z_94) ),
inference(superposition,[status(thm),theory(equality)],[c_4514,c_4552]) ).
tff(c_4963,plain,
! [Z_106] : ( multiply(sk_c5,multiply(sk_c4,Z_106)) = Z_106 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4579]) ).
tff(c_4975,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_4547,c_4963]) ).
tff(c_5027,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5024,c_4975]) ).
tff(c_4594,plain,
! [X_2,Z_94] : ( multiply(inverse(X_2),multiply(X_2,Z_94)) = multiply(identity,Z_94) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4552]) ).
tff(c_5126,plain,
! [X_109,Z_110] : ( multiply(inverse(X_109),multiply(X_109,Z_110)) = Z_110 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4594]) ).
tff(c_5159,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5027,c_5126]) ).
tff(c_5206,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5159]) ).
tff(c_5039,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5024,c_75]) ).
tff(c_5054,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5039,c_4]) ).
tff(c_5241,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5206,c_5054]) ).
tff(c_5035,plain,
multiply(sk_c2,sk_c5) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5024,c_4491]) ).
tff(c_5222,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_5206,c_5206,c_5035]) ).
tff(c_5356,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5241,c_5222]) ).
tff(c_5358,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_28,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_5387,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_5358,c_28]) ).
tff(c_30,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_5400,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_5358,c_30]) ).
tff(c_5357,plain,
inverse(sk_c3) = sk_c6,
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_5362,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5357,c_4]) ).
tff(c_5419,plain,
! [X_112,Y_113,Z_114] : ( multiply(multiply(X_112,Y_113),Z_114) = multiply(X_112,multiply(Y_113,Z_114)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_5446,plain,
! [Z_114] : ( multiply(sk_c6,multiply(sk_c3,Z_114)) = multiply(identity,Z_114) ),
inference(superposition,[status(thm),theory(equality)],[c_5362,c_5419]) ).
tff(c_5488,plain,
! [Z_116] : ( multiply(sk_c6,multiply(sk_c3,Z_116)) = Z_116 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5446]) ).
tff(c_5500,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5400,c_5488]) ).
tff(c_5504,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5387,c_5500]) ).
tff(c_36,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_5405,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_5358,c_36]) ).
tff(c_34,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_5366,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_5367,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5358,c_5366]) ).
tff(c_5368,plain,
inverse(sk_c4) = sk_c5,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_5373,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_5368,c_4]) ).
tff(c_5443,plain,
! [Z_114] : ( multiply(sk_c5,multiply(sk_c4,Z_114)) = multiply(identity,Z_114) ),
inference(superposition,[status(thm),theory(equality)],[c_5373,c_5419]) ).
tff(c_5465,plain,
! [Z_115] : ( multiply(sk_c5,multiply(sk_c4,Z_115)) = Z_115 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5443]) ).
tff(c_5477,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_5405,c_5465]) ).
tff(c_5506,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5504,c_5477]) ).
tff(c_5452,plain,
! [X_2,Z_114] : ( multiply(inverse(X_2),multiply(X_2,Z_114)) = multiply(identity,Z_114) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_5419]) ).
tff(c_5463,plain,
! [X_2,Z_114] : ( multiply(inverse(X_2),multiply(X_2,Z_114)) = Z_114 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5452]) ).
tff(c_5763,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5506,c_5463]) ).
tff(c_5769,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5763]) ).
tff(c_5699,plain,
! [X_119,Z_120] : ( multiply(inverse(X_119),multiply(X_119,Z_120)) = Z_120 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5452]) ).
tff(c_5944,plain,
! [X_123,Z_124] : ( multiply(inverse(inverse(X_123)),Z_124) = multiply(X_123,Z_124) ),
inference(superposition,[status(thm),theory(equality)],[c_5463,c_5699]) ).
tff(c_5744,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_5699]) ).
tff(c_5951,plain,
! [X_123] : ( multiply(X_123,identity) = X_123 ),
inference(superposition,[status(thm),theory(equality)],[c_5944,c_5744]) ).
tff(c_5509,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5504,c_5387]) ).
tff(c_5723,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5509,c_5699]) ).
tff(c_5751,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5723]) ).
tff(c_5573,plain,
! [X_117,Z_118] : ( multiply(inverse(X_117),multiply(X_117,Z_118)) = Z_118 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5452]) ).
tff(c_5603,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_5509,c_5573]) ).
tff(c_5633,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5603]) ).
tff(c_5591,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_5506,c_5573]) ).
tff(c_5631,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_5591]) ).
tff(c_5525,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X2_9) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != 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_c5,sk_c5) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5504,c_5504,c_5504,c_5504,c_5504,c_5504,c_5504,c_5504,c_58]) ).
tff(c_5526,plain,
multiply(sk_c5,sk_c5) != sk_c7,
inference(splitLeft,[status(thm)],[c_5525]) ).
tff(c_5565,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5506,c_5526]) ).
tff(c_5635,plain,
sk_c7 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_5631,c_5565]) ).
tff(c_5667,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5633,c_5635]) ).
tff(c_5668,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 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_5525]) ).
tff(c_13380,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != identity )
| ( identity != X3_6 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X2_9 )
| ( inverse(X2_9) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5769,c_5951,c_5769,c_5769,c_5951,c_5769,c_5751,c_5769,c_5951,c_5769,c_5769,c_5769,c_5951,c_5769,c_5751,c_5751,c_5769,c_2,c_5769,c_5751,c_5668]) ).
tff(c_13382,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_13380]) ).
tff(c_5512,plain,
multiply(sk_c5,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5504,c_79]) ).
tff(c_5849,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_5769,c_5512]) ).
tff(c_5513,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_5504,c_75]) ).
tff(c_5785,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5769,c_5513]) ).
tff(c_5850,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_5849,c_5785]) ).
tff(c_13384,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13382,c_5850]) ).
tff(c_13385,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X3_6) != identity )
| ( identity != X3_6 ) ),
inference(splitRight,[status(thm)],[c_13380]) ).
tff(c_16494,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_13385]) ).
tff(c_16496,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16494,c_5850]) ).
tff(c_16497,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_13385]) ).
tff(c_16499,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_16497]) ).
tff(c_16501,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16499,c_5850]) ).
tff(c_16504,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_16497]) ).
tff(c_16506,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16504,c_5850]) ).
tff(c_16508,plain,
inverse(sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_48,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_16564,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_16508,c_48]) ).
tff(c_50,plain,
( ( multiply(sk_c3,sk_c6) = sk_c7 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_16556,plain,
multiply(sk_c3,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_16508,c_50]) ).
tff(c_16507,plain,
inverse(sk_c3) = sk_c6,
inference(splitRight,[status(thm)],[c_52]) ).
tff(c_16512,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16507,c_4]) ).
tff(c_16608,plain,
! [Z_233] : ( multiply(sk_c6,multiply(sk_c3,Z_233)) = multiply(identity,Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_16512,c_16578]) ).
tff(c_16647,plain,
! [Z_235] : ( multiply(sk_c6,multiply(sk_c3,Z_235)) = Z_235 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16608]) ).
tff(c_16659,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16556,c_16647]) ).
tff(c_16663,plain,
sk_c6 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16564,c_16659]) ).
tff(c_56,plain,
( ( multiply(sk_c4,sk_c6) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_16546,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_16508,c_56]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_16533,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_16508,c_54]) ).
tff(c_16537,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16533,c_4]) ).
tff(c_16602,plain,
! [Z_233] : ( multiply(sk_c5,multiply(sk_c4,Z_233)) = multiply(identity,Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_16537,c_16578]) ).
tff(c_16624,plain,
! [Z_234] : ( multiply(sk_c5,multiply(sk_c4,Z_234)) = Z_234 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16602]) ).
tff(c_16636,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16546,c_16624]) ).
tff(c_16986,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16663,c_16636]) ).
tff(c_17872,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16986,c_16622]) ).
tff(c_17878,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17872]) ).
tff(c_16987,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16663,c_16564]) ).
tff(c_17784,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16987,c_17766]) ).
tff(c_17821,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17784]) ).
tff(c_17081,plain,
! [X_239,Z_240] : ( multiply(inverse(X_239),multiply(X_239,Z_240)) = Z_240 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16611]) ).
tff(c_17111,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16986,c_17081]) ).
tff(c_17141,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17111]) ).
tff(c_17368,plain,
! [X_243,Z_244] : ( multiply(inverse(inverse(X_243)),Z_244) = multiply(X_243,Z_244) ),
inference(superposition,[status(thm),theory(equality)],[c_16622,c_17081]) ).
tff(c_17132,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17081]) ).
tff(c_17375,plain,
! [X_243] : ( multiply(X_243,identity) = X_243 ),
inference(superposition,[status(thm),theory(equality)],[c_17368,c_17132]) ).
tff(c_16668,plain,
multiply(sk_c5,sk_c5) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16663,c_16636]) ).
tff(c_16804,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_16668,c_16622]) ).
tff(c_16810,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16804]) ).
tff(c_16669,plain,
multiply(sk_c5,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_16663,c_16564]) ).
tff(c_16720,plain,
! [X_236,Z_237] : ( multiply(inverse(X_236),multiply(X_236,Z_237)) = Z_237 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16611]) ).
tff(c_16738,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_16669,c_16720]) ).
tff(c_16778,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16738]) ).
tff(c_16665,plain,
! [X2_9,X1_8,X4_7,X3_6] :
( ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X2_9) != sk_c5 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( 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_c6,sk_c5) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16564,c_58]) ).
tff(c_16666,plain,
multiply(sk_c6,sk_c5) != sk_c7,
inference(splitLeft,[status(thm)],[c_16665]) ).
tff(c_16694,plain,
multiply(sk_c5,sk_c5) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_16663,c_16666]) ).
tff(c_16784,plain,
multiply(sk_c5,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_16778,c_16694]) ).
tff(c_16956,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16810,c_2,c_16810,c_16784]) ).
tff(c_16957,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 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(X2_9,sk_c6) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_16665]) ).
tff(c_17020,plain,
! [X3_6,X4_7,X1_8,X2_9] :
( ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16663,c_16663,c_16663,c_16663,c_16663,c_16663,c_16957]) ).
tff(c_17021,plain,
! [X2_9] :
( ( multiply(X2_9,sk_c5) != sk_c5 )
| ( inverse(X2_9) != sk_c5 ) ),
inference(splitLeft,[status(thm)],[c_17020]) ).
tff(c_17755,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_17141,c_17375,c_17141,c_17141,c_17021]) ).
tff(c_17154,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17141,c_16537]) ).
tff(c_17238,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_17154,c_16622]) ).
tff(c_17250,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_17238]) ).
tff(c_17155,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17141,c_16533]) ).
tff(c_17255,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17250,c_17155]) ).
tff(c_17757,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_17755,c_17255]) ).
tff(c_17758,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != sk_c5 )
| ( multiply(X1_8,sk_c5) != sk_c7 )
| ( inverse(X4_7) != sk_c5 )
| ( multiply(X4_7,sk_c5) != sk_c5 )
| ( inverse(X3_6) != sk_c7 )
| ( multiply(X3_6,sk_c7) != sk_c5 ) ),
inference(splitRight,[status(thm)],[c_17020]) ).
tff(c_25953,plain,
! [X1_8,X4_7,X3_6] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X3_6) != identity )
| ( identity != X3_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18084,c_17878,c_17821,c_17821,c_18084,c_17878,c_17878,c_17878,c_18084,c_17878,c_17821,c_17878,c_17758]) ).
tff(c_25955,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25953]) ).
tff(c_17888,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17878,c_16537]) ).
tff(c_17946,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_17888,c_2]) ).
tff(c_17889,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17878,c_16533]) ).
tff(c_17956,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_17946,c_17889]) ).
tff(c_25957,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25955,c_17956]) ).
tff(c_25958,plain,
! [X4_7,X1_8] :
( ( inverse(X4_7) != identity )
| ( identity != X4_7 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_25953]) ).
tff(c_25960,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_25958]) ).
tff(c_25962,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25960,c_17956]) ).
tff(c_25965,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_25958]) ).
tff(c_25967,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25965,c_17956]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP351-1 : TPTP v9.0.0. Released v2.5.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 21:43:15 EDT 2025
% 0.12/0.34 % CPUTime :
% 11.48/3.89 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.83/3.94
% 11.83/3.94 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------