%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP297-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 : n003.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:50 PM UTC 2025
% Result : Unsatisfiable 27.02s 14.27s
% Output : CNFRefutation 27.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 24
% Syntax : Number of formulae : 384 ( 329 unt; 0 typ; 0 def)
% Number of atoms : 494 ( 481 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 226 ( 116 ~; 110 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 181 ( 181 !; 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_86,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_164,axiom,
! [X2,X1,X3,X4] :
( ( multiply(sk_c7,sk_c6) != sk_c5 )
| ( multiply(X2,sk_c7) != sk_c6 )
| ( inverse(X2) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( inverse(X1) != sk_c7 )
| ( multiply(X1,sk_c6) != sk_c7 )
| ( multiply(X3,X4) != sk_c6 )
| ( inverse(X3) != X4 )
| ( multiply(X4,sk_c7) != sk_c6 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c7,sk_c6) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c7,sk_c5) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c4 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c4) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_22628,plain,
! [X_236,Y_237,Z_238] : ( multiply(multiply(X_236,Y_237),Z_238) = multiply(X_236,multiply(Y_237,Z_238)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_22661,plain,
! [X_2,Z_238] : ( multiply(inverse(X_2),multiply(X_2,Z_238)) = multiply(identity,Z_238) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22628]) ).
tff(c_23279,plain,
! [X_247,Z_248] : ( multiply(inverse(X_247),multiply(X_247,Z_248)) = Z_248 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22661]) ).
tff(c_22671,plain,
! [X_2,Z_238] : ( multiply(inverse(X_2),multiply(X_2,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22661]) ).
tff(c_25694,plain,
! [X_284,Z_285] : ( multiply(inverse(inverse(X_284)),Z_285) = multiply(X_284,Z_285) ),
inference(superposition,[status(thm),theory(equality)],[c_23279,c_22671]) ).
tff(c_23339,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_23279]) ).
tff(c_25738,plain,
! [X_286] : ( multiply(X_286,identity) = X_286 ),
inference(superposition,[status(thm),theory(equality)],[c_25694,c_23339]) ).
tff(c_23342,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_23279]) ).
tff(c_25756,plain,
inverse(identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25738,c_23342]) ).
tff(c_25715,plain,
! [X_284] : ( multiply(X_284,inverse(X_284)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_25694,c_4]) ).
tff(c_22014,plain,
! [X_224,Y_225,Z_226] : ( multiply(multiply(X_224,Y_225),Z_226) = multiply(X_224,multiply(Y_225,Z_226)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_22053,plain,
! [X_2,Z_226] : ( multiply(inverse(X_2),multiply(X_2,Z_226)) = multiply(identity,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_22014]) ).
tff(c_22127,plain,
! [X_230,Z_231] : ( multiply(inverse(X_230),multiply(X_230,Z_231)) = Z_231 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22053]) ).
tff(c_22199,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_22127]) ).
tff(c_22,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_92,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_34,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_73,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_77,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_73,c_4]) ).
tff(c_18907,plain,
! [X_160,Y_161,Z_162] : ( multiply(multiply(X_160,Y_161),Z_162) = multiply(X_160,multiply(Y_161,Z_162)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18946,plain,
! [Z_162] : ( multiply(sk_c7,multiply(sk_c1,Z_162)) = multiply(identity,Z_162) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_18907]) ).
tff(c_18962,plain,
! [Z_163] : ( multiply(sk_c7,multiply(sk_c1,Z_163)) = Z_163 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18946]) ).
tff(c_18974,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_92,c_18962]) ).
tff(c_10,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_99,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_120,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_144,plain,
! [Z_14] : ( multiply(sk_c7,multiply(sk_c1,Z_14)) = multiply(identity,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_77,c_120]) ).
tff(c_158,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_144]) ).
tff(c_170,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_92,c_158]) ).
tff(c_174,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_99,c_170]) ).
tff(c_180,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_174,c_73]) ).
tff(c_188,plain,
multiply(sk_c5,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_180,c_4]) ).
tff(c_147,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_120]) ).
tff(c_245,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_147]) ).
tff(c_272,plain,
multiply(inverse(sk_c5),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_188,c_245]) ).
tff(c_56,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c5 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_192,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c5) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c5 )
| ( inverse(X1_7) != sk_c5 )
| ( multiply(sk_c6,sk_c5) != sk_c5 )
| ( multiply(sk_c5,sk_c5) != sk_c6 )
| ( inverse(X2_6) != sk_c5 )
| ( multiply(X2_6,sk_c5) != sk_c6 )
| ( multiply(sk_c5,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_174,c_174,c_174,c_174,c_174,c_174,c_174,c_174,c_56]) ).
tff(c_193,plain,
multiply(sk_c5,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_192]) ).
tff(c_176,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_174,c_99]) ).
tff(c_194,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_193,c_176]) ).
tff(c_196,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(splitRight,[status(thm)],[c_192]) ).
tff(c_269,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_196,c_245]) ).
tff(c_291,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_269]) ).
tff(c_46,plain,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_87,plain,
multiply(sk_c7,sk_c5) = sk_c6,
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_178,plain,
multiply(sk_c5,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_174,c_87]) ).
tff(c_266,plain,
multiply(inverse(sk_c5),sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_178,c_245]) ).
tff(c_376,plain,
multiply(inverse(sk_c5),identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_291,c_266]) ).
tff(c_388,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_272,c_376]) ).
tff(c_406,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_388,c_180]) ).
tff(c_177,plain,
multiply(sk_c1,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_174,c_92]) ).
tff(c_296,plain,
multiply(sk_c1,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_291,c_177]) ).
tff(c_402,plain,
multiply(sk_c1,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_388,c_296]) ).
tff(c_329,plain,
! [X_19] : ( multiply(inverse(identity),X_19) = X_19 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_245]) ).
tff(c_156,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_147]) ).
tff(c_511,plain,
! [X_22] : ( multiply(inverse(inverse(identity)),X_22) = X_22 ),
inference(superposition,[status(thm),theory(equality)],[c_329,c_156]) ).
tff(c_532,plain,
inverse(identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_511,c_4]) ).
tff(c_621,plain,
! [X_24,Z_25] : ( multiply(inverse(inverse(X_24)),Z_25) = multiply(X_24,Z_25) ),
inference(superposition,[status(thm),theory(equality)],[c_156,c_245]) ).
tff(c_646,plain,
! [X_24] : ( multiply(X_24,inverse(X_24)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_621,c_4]) ).
tff(c_407,plain,
sk_c7 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_388,c_174]) ).
tff(c_138,plain,
! [Z_14] : ( multiply(sk_c1,multiply(sk_c7,Z_14)) = multiply(sk_c6,Z_14) ),
inference(superposition,[status(thm),theory(equality)],[c_92,c_120]) ).
tff(c_416,plain,
! [Z_14] : ( multiply(sk_c1,multiply(sk_c1,Z_14)) = Z_14 ),
inference(demodulation,[status(thm),theory(equality)],[c_407,c_2,c_291,c_138]) ).
tff(c_284,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_245]) ).
tff(c_632,plain,
! [X_24] : ( multiply(X_24,identity) = X_24 ),
inference(superposition,[status(thm),theory(equality)],[c_621,c_284]) ).
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_937,plain,
! [X_31,Y_32,Z_33] : ( multiply(inverse(multiply(X_31,Y_32)),multiply(X_31,multiply(Y_32,Z_33))) = Z_33 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_245]) ).
tff(c_985,plain,
! [X_31,X_24] : ( multiply(inverse(multiply(X_31,X_24)),multiply(X_31,identity)) = inverse(X_24) ),
inference(superposition,[status(thm),theory(equality)],[c_646,c_937]) ).
tff(c_1782,plain,
! [X_45,X_46] : ( multiply(inverse(multiply(X_45,X_46)),X_45) = inverse(X_46) ),
inference(demodulation,[status(thm),theory(equality)],[c_632,c_985]) ).
tff(c_1896,plain,
! [Z_14] : ( multiply(inverse(Z_14),sk_c1) = inverse(multiply(sk_c1,Z_14)) ),
inference(superposition,[status(thm),theory(equality)],[c_416,c_1782]) ).
tff(c_195,plain,
! [X2_6,X1_7,X3_8] :
( ( multiply(sk_c5,sk_c5) != sk_c6 )
| ( multiply(sk_c6,sk_c5) != sk_c5 )
| ( inverse(X2_6) != sk_c5 )
| ( multiply(X2_6,sk_c5) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c5 )
| ( inverse(X1_7) != sk_c5 )
| ( multiply(inverse(X3_8),sk_c5) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_192]) ).
tff(c_6551,plain,
! [X2_6,X1_7,X3_8] :
( ( inverse(X2_6) != sk_c1 )
| ( multiply(X2_6,sk_c1) != identity )
| ( sk_c1 != X1_7 )
| ( inverse(X1_7) != sk_c1 )
| ( inverse(multiply(sk_c1,X3_8)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_646,c_291,c_1896,c_388,c_291,c_388,c_632,c_388,c_291,c_388,c_291,c_388,c_2,c_291,c_402,c_388,c_388,c_291,c_195]) ).
tff(c_6553,plain,
! [X3_95] : ( inverse(multiply(sk_c1,X3_95)) != identity ),
inference(splitLeft,[status(thm)],[c_6551]) ).
tff(c_6577,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_646,c_6553]) ).
tff(c_6592,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_532,c_6577]) ).
tff(c_6593,plain,
! [X2_6,X1_7] :
( ( inverse(X2_6) != sk_c1 )
| ( multiply(X2_6,sk_c1) != identity )
| ( sk_c1 != X1_7 )
| ( inverse(X1_7) != sk_c1 ) ),
inference(splitRight,[status(thm)],[c_6551]) ).
tff(c_18773,plain,
inverse(sk_c1) != sk_c1,
inference(splitLeft,[status(thm)],[c_6593]) ).
tff(c_18775,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18773,c_406]) ).
tff(c_18777,plain,
! [X2_159] :
( ( inverse(X2_159) != sk_c1 )
| ( multiply(X2_159,sk_c1) != identity ) ),
inference(splitRight,[status(thm)],[c_6593]) ).
tff(c_18825,plain,
inverse(sk_c1) != sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_402,c_18777]) ).
tff(c_18850,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_406,c_18825]) ).
tff(c_18852,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_18978,plain,
sk_c7 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_18974,c_18852]) ).
tff(c_18949,plain,
! [X_2,Z_162] : ( multiply(inverse(X_2),multiply(X_2,Z_162)) = multiply(identity,Z_162) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18907]) ).
tff(c_19034,plain,
! [X_166,Z_167] : ( multiply(inverse(X_166),multiply(X_166,Z_167)) = Z_167 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18949]) ).
tff(c_19112,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_19034]) ).
tff(c_19064,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_18974,c_19034]) ).
tff(c_19117,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_19064]) ).
tff(c_8,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_18898,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_18852,c_8]) ).
tff(c_19171,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19117,c_18898]) ).
tff(c_18960,plain,
! [X_2,Z_162] : ( multiply(inverse(X_2),multiply(X_2,Z_162)) = Z_162 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_18949]) ).
tff(c_19385,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_19171,c_18960]) ).
tff(c_19397,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_19112,c_19385]) ).
tff(c_19399,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18978,c_19397]) ).
tff(c_19401,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_26,plain,
( ( multiply(sk_c3,sk_c4) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_20838,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_19401,c_26]) ).
tff(c_19463,plain,
! [X_172,Y_173,Z_174] : ( multiply(multiply(X_172,Y_173),Z_174) = multiply(X_172,multiply(Y_173,Z_174)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_19505,plain,
! [X_2,Z_174] : ( multiply(inverse(X_2),multiply(X_2,Z_174)) = multiply(identity,Z_174) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_19463]) ).
tff(c_20242,plain,
! [X_190,Z_191] : ( multiply(inverse(X_190),multiply(X_190,Z_191)) = Z_191 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19505]) ).
tff(c_20323,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_20242]) ).
tff(c_19443,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_19401,c_26]) ).
tff(c_28,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_19423,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_19401,c_28]) ).
tff(c_19427,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_19423,c_4]) ).
tff(c_19490,plain,
! [Z_174] : ( multiply(sk_c4,multiply(sk_c3,Z_174)) = multiply(identity,Z_174) ),
inference(superposition,[status(thm),theory(equality)],[c_19427,c_19463]) ).
tff(c_19531,plain,
! [Z_176] : ( multiply(sk_c4,multiply(sk_c3,Z_176)) = Z_176 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19490]) ).
tff(c_19543,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_19443,c_19531]) ).
tff(c_20272,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_19543,c_20242]) ).
tff(c_20327,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20272]) ).
tff(c_20,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_19435,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_19401,c_20]) ).
tff(c_20340,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20327,c_19435]) ).
tff(c_19516,plain,
! [X_2,Z_174] : ( multiply(inverse(X_2),multiply(X_2,Z_174)) = Z_174 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_19505]) ).
tff(c_20459,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_20340,c_19516]) ).
tff(c_20471,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20323,c_20459]) ).
tff(c_20483,plain,
multiply(sk_c5,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_20471,c_77]) ).
tff(c_19499,plain,
! [Z_174] : ( multiply(sk_c7,multiply(sk_c5,Z_174)) = multiply(sk_c6,Z_174) ),
inference(superposition,[status(thm),theory(equality)],[c_87,c_19463]) ).
tff(c_20502,plain,
! [Z_174] : ( multiply(sk_c5,multiply(sk_c5,Z_174)) = Z_174 ),
inference(demodulation,[status(thm),theory(equality)],[c_20471,c_2,c_20327,c_19499]) ).
tff(c_20614,plain,
multiply(sk_c5,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_20483,c_20502]) ).
tff(c_16,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_19413,plain,
multiply(sk_c7,sk_c6) = sk_c5,
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_20341,plain,
multiply(sk_c7,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20327,c_19413]) ).
tff(c_20579,plain,
multiply(sk_c5,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20471,c_20341]) ).
tff(c_20644,plain,
sk_c5 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_20614,c_20579]) ).
tff(c_20484,plain,
inverse(sk_c1) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_20471,c_73]) ).
tff(c_20668,plain,
inverse(sk_c1) = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_20644,c_20484]) ).
tff(c_20703,plain,
multiply(sk_c1,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20668,c_4]) ).
tff(c_20342,plain,
multiply(sk_c1,sk_c7) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20327,c_19401]) ).
tff(c_20474,plain,
multiply(sk_c1,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20471,c_20342]) ).
tff(c_20663,plain,
multiply(sk_c1,sk_c1) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_20644,c_20474]) ).
tff(c_20798,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20703,c_20663]) ).
tff(c_20799,plain,
inverse(sk_c3) = sk_c4,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_20804,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_20799,c_4]) ).
tff(c_20852,plain,
! [X_197,Y_198,Z_199] : ( multiply(multiply(X_197,Y_198),Z_199) = multiply(X_197,multiply(Y_198,Z_199)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_20879,plain,
! [Z_199] : ( multiply(sk_c4,multiply(sk_c3,Z_199)) = multiply(identity,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_20804,c_20852]) ).
tff(c_20942,plain,
! [Z_202] : ( multiply(sk_c4,multiply(sk_c3,Z_202)) = Z_202 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20879]) ).
tff(c_20954,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_20838,c_20942]) ).
tff(c_20891,plain,
! [X_2,Z_199] : ( multiply(inverse(X_2),multiply(X_2,Z_199)) = multiply(identity,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_20852]) ).
tff(c_20965,plain,
! [X_203,Z_204] : ( multiply(inverse(X_203),multiply(X_203,Z_204)) = Z_204 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20891]) ).
tff(c_20983,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20954,c_20965]) ).
tff(c_21041,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_20983]) ).
tff(c_21047,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_21041,c_20954]) ).
tff(c_21037,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_20965]) ).
tff(c_20800,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_20833,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_20800,c_8]) ).
tff(c_21050,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_21041,c_20833]) ).
tff(c_20902,plain,
! [X_2,Z_199] : ( multiply(inverse(X_2),multiply(X_2,Z_199)) = Z_199 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20891]) ).
tff(c_21181,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_21050,c_20902]) ).
tff(c_21193,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_21037,c_21181]) ).
tff(c_12,plain,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c6) = sk_c5 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_20826,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_20800,c_12]) ).
tff(c_19400,plain,
inverse(sk_c2) = sk_c7,
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_19405,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_19400,c_4]) ).
tff(c_20882,plain,
! [Z_199] : ( multiply(sk_c7,multiply(sk_c2,Z_199)) = multiply(identity,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_19405,c_20852]) ).
tff(c_20919,plain,
! [Z_201] : ( multiply(sk_c7,multiply(sk_c2,Z_201)) = Z_201 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_20882]) ).
tff(c_20931,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_20826,c_20919]) ).
tff(c_21048,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21041,c_20931]) ).
tff(c_21235,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_21193,c_21193,c_21048]) ).
tff(c_30,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_20821,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_19401,c_30]) ).
tff(c_20876,plain,
! [Z_199] : ( multiply(sk_c4,multiply(sk_c7,Z_199)) = multiply(sk_c6,Z_199) ),
inference(superposition,[status(thm),theory(equality)],[c_20821,c_20852]) ).
tff(c_21250,plain,
! [Z_207] : ( multiply(sk_c4,multiply(sk_c5,Z_207)) = Z_207 ),
inference(demodulation,[status(thm),theory(equality)],[c_21193,c_2,c_21041,c_20876]) ).
tff(c_21265,plain,
multiply(sk_c4,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_21235,c_21250]) ).
tff(c_21269,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_21047,c_21265]) ).
tff(c_21053,plain,
multiply(sk_c7,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_21041,c_20800]) ).
tff(c_21199,plain,
multiply(sk_c5,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_21193,c_21053]) ).
tff(c_21357,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_21269,c_21047,c_21269,c_21199]) ).
tff(c_21359,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_50,plain,
( ( multiply(sk_c3,sk_c4) = sk_c6 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_22003,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_21359,c_50]) ).
tff(c_52,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_21955,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_21359,c_52]) ).
tff(c_21959,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21955,c_4]) ).
tff(c_22044,plain,
! [Z_226] : ( multiply(sk_c4,multiply(sk_c3,Z_226)) = multiply(identity,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_21959,c_22014]) ).
tff(c_22066,plain,
! [Z_227] : ( multiply(sk_c4,multiply(sk_c3,Z_227)) = Z_227 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22044]) ).
tff(c_22078,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_22003,c_22066]) ).
tff(c_22154,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22078,c_22127]) ).
tff(c_22203,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22154]) ).
tff(c_44,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_21985,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_21359,c_44]) ).
tff(c_22249,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22203,c_21985]) ).
tff(c_22064,plain,
! [X_2,Z_226] : ( multiply(inverse(X_2),multiply(X_2,Z_226)) = Z_226 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22053]) ).
tff(c_22415,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_22249,c_22064]) ).
tff(c_22427,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22199,c_22415]) ).
tff(c_48,plain,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c7,sk_c5) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_21997,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_21359,c_48]) ).
tff(c_22032,plain,
! [Z_226] : ( multiply(sk_c2,multiply(sk_c6,Z_226)) = multiply(sk_c7,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_21997,c_22014]) ).
tff(c_22480,plain,
! [Z_226] : ( multiply(sk_c5,Z_226) = multiply(sk_c2,Z_226) ),
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_2,c_22203,c_22032]) ).
tff(c_22038,plain,
! [Z_226] : ( multiply(sk_c6,multiply(sk_c7,Z_226)) = multiply(sk_c5,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_21985,c_22014]) ).
tff(c_22364,plain,
! [Z_226] : ( multiply(sk_c7,Z_226) = multiply(sk_c5,Z_226) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22203,c_22038]) ).
tff(c_22252,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_22203,c_21359]) ).
tff(c_22365,plain,
multiply(sk_c5,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_22364,c_22252]) ).
tff(c_22481,plain,
multiply(sk_c2,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_22480,c_22365]) ).
tff(c_21358,plain,
inverse(sk_c2) = sk_c7,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_21950,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_21358,c_4]) ).
tff(c_22047,plain,
! [Z_226] : ( multiply(sk_c7,multiply(sk_c2,Z_226)) = multiply(identity,Z_226) ),
inference(superposition,[status(thm),theory(equality)],[c_21950,c_22014]) ).
tff(c_22104,plain,
! [Z_229] : ( multiply(sk_c7,multiply(sk_c2,Z_229)) = Z_229 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22047]) ).
tff(c_22116,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_21997,c_22104]) ).
tff(c_22244,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22203,c_22116]) ).
tff(c_22432,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22427,c_22427,c_22244]) ).
tff(c_22551,plain,
multiply(sk_c2,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22432,c_22480]) ).
tff(c_22564,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22481,c_22551]) ).
tff(c_22566,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_40,plain,
( ( inverse(sk_c3) = sk_c4 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_22578,plain,
inverse(sk_c3) = sk_c4,
inference(negUnitSimplification,[status(thm)],[c_22566,c_40]) ).
tff(c_22582,plain,
multiply(sk_c4,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22578,c_4]) ).
tff(c_38,plain,
( ( multiply(sk_c3,sk_c4) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_22599,plain,
multiply(sk_c3,sk_c4) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_22566,c_38]) ).
tff(c_22655,plain,
! [Z_238] : ( multiply(sk_c4,multiply(sk_c3,Z_238)) = multiply(identity,Z_238) ),
inference(superposition,[status(thm),theory(equality)],[c_22582,c_22628]) ).
tff(c_22673,plain,
! [Z_239] : ( multiply(sk_c4,multiply(sk_c3,Z_239)) = Z_239 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22655]) ).
tff(c_22685,plain,
multiply(sk_c4,sk_c6) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_22599,c_22673]) ).
tff(c_23306,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22685,c_23279]) ).
tff(c_23346,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_23306]) ).
tff(c_22649,plain,
! [Z_238] : ( multiply(sk_c3,multiply(sk_c4,Z_238)) = multiply(sk_c6,Z_238) ),
inference(superposition,[status(thm),theory(equality)],[c_22599,c_22628]) ).
tff(c_25322,plain,
! [Z_280] : ( multiply(sk_c3,multiply(sk_c4,Z_280)) = Z_280 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23346,c_22649]) ).
tff(c_25346,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_22582,c_25322]) ).
tff(c_32,plain,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_22593,plain,
multiply(sk_c6,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_22566,c_32]) ).
tff(c_23690,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22593]) ).
tff(c_23761,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_23690,c_22671]) ).
tff(c_23773,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23342,c_23761]) ).
tff(c_42,plain,
( ( multiply(sk_c4,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_22605,plain,
multiply(sk_c4,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_22566,c_42]) ).
tff(c_23688,plain,
multiply(sk_c4,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22605]) ).
tff(c_25369,plain,
multiply(sk_c4,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_23688]) ).
tff(c_25321,plain,
! [Z_238] : ( multiply(sk_c3,multiply(sk_c4,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23346,c_22649]) ).
tff(c_25373,plain,
multiply(sk_c3,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_25369,c_25321]) ).
tff(c_25441,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_25346,c_25373]) ).
tff(c_36,plain,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_22610,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_22566,c_36]) ).
tff(c_23687,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22610]) ).
tff(c_23776,plain,
multiply(sk_c2,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_23687]) ).
tff(c_25442,plain,
multiply(sk_c2,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_25441,c_23776]) ).
tff(c_23686,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22685]) ).
tff(c_22565,plain,
inverse(sk_c2) = sk_c7,
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_23781,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_22565]) ).
tff(c_25447,plain,
inverse(sk_c2) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_25441,c_23781]) ).
tff(c_25482,plain,
multiply(inverse(sk_c3),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_25447,c_23339]) ).
tff(c_25491,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_23686,c_22578,c_25482]) ).
tff(c_25498,plain,
inverse(sk_c3) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_25491,c_22578]) ).
tff(c_25292,plain,
multiply(sk_c5,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23781,c_4]) ).
tff(c_25443,plain,
multiply(sk_c3,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25441,c_25292]) ).
tff(c_25559,plain,
multiply(inverse(sk_c3),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_25443,c_22671]) ).
tff(c_25568,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_25442,c_25498,c_25559]) ).
tff(c_25449,plain,
sk_c7 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_25441,c_23773]) ).
tff(c_25577,plain,
sk_c7 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_25568,c_25449]) ).
tff(c_22646,plain,
! [Z_238] : ( multiply(sk_c4,multiply(sk_c7,Z_238)) = multiply(sk_c6,Z_238) ),
inference(superposition,[status(thm),theory(equality)],[c_22605,c_22628]) ).
tff(c_25641,plain,
! [Z_238] : ( multiply(sk_c2,multiply(sk_c2,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_25577,c_25491,c_2,c_23346,c_22646]) ).
tff(c_25701,plain,
! [X_284] : ( multiply(X_284,identity) = X_284 ),
inference(superposition,[status(thm),theory(equality)],[c_25694,c_23339]) ).
tff(c_25933,plain,
! [X_289,Y_290,Z_291] : ( multiply(inverse(multiply(X_289,Y_290)),multiply(X_289,multiply(Y_290,Z_291))) = Z_291 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_23279]) ).
tff(c_25969,plain,
! [X_289,X_284] : ( multiply(inverse(multiply(X_289,X_284)),multiply(X_289,identity)) = inverse(X_284) ),
inference(superposition,[status(thm),theory(equality)],[c_25715,c_25933]) ).
tff(c_27052,plain,
! [X_307,X_308] : ( multiply(inverse(multiply(X_307,X_308)),X_307) = inverse(X_308) ),
inference(demodulation,[status(thm),theory(equality)],[c_25701,c_25969]) ).
tff(c_27163,plain,
! [Z_238] : ( multiply(inverse(Z_238),sk_c2) = inverse(multiply(sk_c2,Z_238)) ),
inference(superposition,[status(thm),theory(equality)],[c_25641,c_27052]) ).
tff(c_25578,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_25568,c_25441]) ).
tff(c_23965,plain,
! [Z_256] : ( multiply(sk_c3,multiply(sk_c4,Z_256)) = Z_256 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23346,c_22649]) ).
tff(c_23992,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_22582,c_23965]) ).
tff(c_22570,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_22565,c_4]) ).
tff(c_22658,plain,
! [Z_238] : ( multiply(sk_c7,multiply(sk_c2,Z_238)) = multiply(identity,Z_238) ),
inference(superposition,[status(thm),theory(equality)],[c_22570,c_22628]) ).
tff(c_22696,plain,
! [Z_240] : ( multiply(sk_c7,multiply(sk_c2,Z_240)) = Z_240 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22658]) ).
tff(c_22708,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22610,c_22696]) ).
tff(c_23684,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22708]) ).
tff(c_23852,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_23773,c_23684]) ).
tff(c_22643,plain,
! [Z_238] : ( multiply(sk_c2,multiply(sk_c6,Z_238)) = multiply(sk_c7,Z_238) ),
inference(superposition,[status(thm),theory(equality)],[c_22610,c_22628]) ).
tff(c_23878,plain,
! [Z_254] : ( multiply(sk_c5,Z_254) = multiply(sk_c2,Z_254) ),
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_2,c_23346,c_22643]) ).
tff(c_23902,plain,
multiply(sk_c2,sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23852,c_23878]) ).
tff(c_23877,plain,
! [Z_238] : ( multiply(sk_c5,Z_238) = multiply(sk_c2,Z_238) ),
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_2,c_23346,c_22643]) ).
tff(c_24019,plain,
! [Z_257] : ( multiply(sk_c4,multiply(sk_c2,Z_257)) = Z_257 ),
inference(demodulation,[status(thm),theory(equality)],[c_23877,c_23773,c_2,c_23346,c_22646]) ).
tff(c_24037,plain,
multiply(sk_c4,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_23902,c_24019]) ).
tff(c_24044,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_23686,c_24037]) ).
tff(c_23864,plain,
multiply(sk_c4,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_23688]) ).
tff(c_23983,plain,
multiply(sk_c3,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_23864,c_23965]) ).
tff(c_24079,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_24044,c_23992,c_23983]) ).
tff(c_24090,plain,
inverse(sk_c3) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_24079,c_22578]) ).
tff(c_24053,plain,
inverse(sk_c2) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_24044,c_23781]) ).
tff(c_24074,plain,
multiply(sk_c4,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_24053,c_4]) ).
tff(c_24136,plain,
multiply(sk_c3,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24079,c_24074]) ).
tff(c_24140,plain,
multiply(inverse(sk_c3),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_24136,c_22671]) ).
tff(c_24146,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_23992,c_24090,c_24140]) ).
tff(c_24081,plain,
inverse(sk_c2) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_24079,c_24053]) ).
tff(c_24171,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_24146,c_24081]) ).
tff(c_23689,plain,
multiply(sk_c3,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22599]) ).
tff(c_24087,plain,
multiply(sk_c3,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24079,c_23689]) ).
tff(c_24189,plain,
multiply(sk_c2,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_24146,c_24146,c_24087]) ).
tff(c_24083,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_24079,c_24044]) ).
tff(c_24151,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_24146,c_24083]) ).
tff(c_23354,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22685]) ).
tff(c_23358,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22593]) ).
tff(c_23429,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_23358,c_22671]) ).
tff(c_23441,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23342,c_23429]) ).
tff(c_23352,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22708]) ).
tff(c_23444,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23441,c_23441,c_23352]) ).
tff(c_23581,plain,
! [Z_238] : ( multiply(sk_c4,multiply(sk_c5,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_23441,c_2,c_23346,c_22646]) ).
tff(c_23613,plain,
multiply(sk_c4,identity) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_23444,c_23581]) ).
tff(c_23622,plain,
sk_c5 = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_23354,c_23613]) ).
tff(c_22722,plain,
! [X_241,Z_242] : ( multiply(inverse(X_241),multiply(X_241,Z_242)) = Z_242 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22661]) ).
tff(c_22746,plain,
multiply(inverse(sk_c4),sk_c4) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_22685,c_22722]) ).
tff(c_22786,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_22746]) ).
tff(c_22829,plain,
multiply(sk_c4,identity) = sk_c4,
inference(demodulation,[status(thm),theory(equality)],[c_22786,c_22685]) ).
tff(c_22889,plain,
! [Z_244] : ( multiply(sk_c3,multiply(sk_c4,Z_244)) = Z_244 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_22786,c_22649]) ).
tff(c_22916,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_22582,c_22889]) ).
tff(c_22782,plain,
! [X_1] : ( multiply(inverse(identity),X_1) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_22722]) ).
tff(c_22833,plain,
multiply(identity,sk_c7) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22786,c_22593]) ).
tff(c_22942,plain,
multiply(inverse(identity),sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_22833,c_22671]) ).
tff(c_22954,plain,
sk_c7 = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22782,c_22942]) ).
tff(c_22831,plain,
multiply(sk_c4,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22786,c_22605]) ).
tff(c_22907,plain,
multiply(sk_c3,identity) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_22831,c_22889]) ).
tff(c_23031,plain,
multiply(sk_c3,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22954,c_22907]) ).
tff(c_23079,plain,
sk_c5 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_22916,c_23031]) ).
tff(c_22963,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22954,c_22565]) ).
tff(c_23102,plain,
inverse(sk_c2) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_23079,c_22963]) ).
tff(c_23120,plain,
multiply(sk_c3,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23102,c_4]) ).
tff(c_23142,plain,
multiply(inverse(sk_c3),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_23120,c_22671]) ).
tff(c_23151,plain,
sk_c4 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_22829,c_22578,c_23142]) ).
tff(c_22827,plain,
multiply(sk_c7,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22786,c_22708]) ).
tff(c_22959,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_22954,c_22954,c_22827]) ).
tff(c_23098,plain,
multiply(sk_c3,sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23079,c_23079,c_22959]) ).
tff(c_23127,plain,
multiply(inverse(sk_c3),identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_23098,c_22671]) ).
tff(c_23136,plain,
sk_c4 = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_22829,c_22578,c_23127]) ).
tff(c_23167,plain,
sk_c3 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_23151,c_23136]) ).
tff(c_22830,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_22786,c_22610]) ).
tff(c_22958,plain,
multiply(sk_c2,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22954,c_22830]) ).
tff(c_23096,plain,
multiply(sk_c2,identity) = sk_c3,
inference(demodulation,[status(thm),theory(equality)],[c_23079,c_22958]) ).
tff(c_23244,plain,
multiply(sk_c2,identity) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_23167,c_23096]) ).
tff(c_23177,plain,
sk_c5 = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_23167,c_23079]) ).
tff(c_22996,plain,
! [Z_238] : ( multiply(sk_c5,Z_238) = multiply(sk_c2,Z_238) ),
inference(demodulation,[status(thm),theory(equality)],[c_22954,c_2,c_22786,c_22643]) ).
tff(c_22713,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_22593,c_56]) ).
tff(c_22714,plain,
multiply(sk_c7,sk_c6) != sk_c5,
inference(splitLeft,[status(thm)],[c_22713]) ).
tff(c_22828,plain,
multiply(sk_c7,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22786,c_22714]) ).
tff(c_22981,plain,
multiply(sk_c5,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22954,c_22828]) ).
tff(c_22997,plain,
multiply(sk_c2,identity) != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_22996,c_22981]) ).
tff(c_23262,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_23244,c_23177,c_22997]) ).
tff(c_23263,plain,
! [X2_6,X1_7,X3_8] :
( ( multiply(sk_c7,sk_c5) != sk_c6 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_22713]) ).
tff(c_23351,plain,
multiply(sk_c7,sk_c5) != sk_c6,
inference(splitLeft,[status(thm)],[c_23263]) ).
tff(c_23363,plain,
multiply(sk_c7,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_23351]) ).
tff(c_23445,plain,
multiply(sk_c5,sk_c5) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_23441,c_23363]) ).
tff(c_23678,plain,
multiply(sk_c4,sk_c4) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_23622,c_23622,c_23445]) ).
tff(c_23449,plain,
inverse(sk_c2) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23441,c_22565]) ).
tff(c_23355,plain,
multiply(sk_c2,identity) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_23346,c_22610]) ).
tff(c_23520,plain,
multiply(sk_c2,identity) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_23441,c_23355]) ).
tff(c_23524,plain,
multiply(inverse(sk_c2),sk_c5) = identity,
inference(superposition,[status(thm),theory(equality)],[c_23520,c_22671]) ).
tff(c_23530,plain,
multiply(sk_c5,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23449,c_23524]) ).
tff(c_23680,plain,
multiply(sk_c4,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_23622,c_23622,c_23530]) ).
tff(c_23681,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23678,c_23680]) ).
tff(c_23682,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c7) != sk_c6 )
| ( multiply(X3_8,inverse(X3_8)) != sk_c6 )
| ( multiply(X1_7,sk_c6) != sk_c7 )
| ( inverse(X1_7) != sk_c7 )
| ( inverse(X2_6) != sk_c7 )
| ( multiply(X2_6,sk_c7) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_23263]) ).
tff(c_23789,plain,
! [X3_8,X1_7,X2_6] :
( ( multiply(inverse(X3_8),sk_c5) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity )
| ( multiply(X1_7,identity) != sk_c5 )
| ( inverse(X1_7) != sk_c5 )
| ( inverse(X2_6) != sk_c5 )
| ( multiply(X2_6,sk_c5) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_23773,c_23346,c_23773,c_23773,c_23773,c_23346,c_23346,c_23773,c_23346,c_23682]) ).
tff(c_23790,plain,
! [X2_6] :
( ( inverse(X2_6) != sk_c5 )
| ( multiply(X2_6,sk_c5) != identity ) ),
inference(splitLeft,[status(thm)],[c_23789]) ).
tff(c_25252,plain,
! [X2_279] :
( ( inverse(X2_279) != sk_c2 )
| ( multiply(X2_279,sk_c2) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24151,c_24151,c_23790]) ).
tff(c_25266,plain,
inverse(sk_c2) != sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_24189,c_25252]) ).
tff(c_25284,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24171,c_25266]) ).
tff(c_25285,plain,
! [X1_7,X3_8] :
( ( multiply(X1_7,identity) != sk_c5 )
| ( inverse(X1_7) != sk_c5 )
| ( multiply(inverse(X3_8),sk_c5) != identity )
| ( multiply(X3_8,inverse(X3_8)) != identity ) ),
inference(splitRight,[status(thm)],[c_23789]) ).
tff(c_129322,plain,
! [X1_7,X3_8] :
( ( sk_c2 != X1_7 )
| ( inverse(X1_7) != sk_c2 )
| ( inverse(multiply(sk_c2,X3_8)) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25715,c_27163,c_25578,c_25578,c_25701,c_25578,c_25285]) ).
tff(c_129324,plain,
! [X3_664] : ( inverse(multiply(sk_c2,X3_664)) != identity ),
inference(splitLeft,[status(thm)],[c_129322]) ).
tff(c_129373,plain,
inverse(identity) != identity,
inference(superposition,[status(thm),theory(equality)],[c_25715,c_129324]) ).
tff(c_129396,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_25756,c_129373]) ).
tff(c_129398,plain,
inverse(sk_c2) != sk_c2,
inference(splitRight,[status(thm)],[c_129322]) ).
tff(c_25574,plain,
inverse(sk_c2) = sk_c2,
inference(demodulation,[status(thm),theory(equality)],[c_25568,c_25498]) ).
tff(c_129400,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_129398,c_25574]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP297-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/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.13/0.33 % Computer : n003.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Apr 7 21:41:03 EDT 2025
% 0.13/0.33 % CPUTime :
% 27.02/14.27 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.11/14.32
% 27.11/14.32 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------