%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP332-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 : n015.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:57 PM UTC 2025
% Result : Unsatisfiable 17.91s 7.15s
% Output : CNFRefutation 17.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 34
% Syntax : Number of formulae : 395 ( 317 unt; 0 typ; 0 def)
% Number of atoms : 576 ( 553 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 360 ( 179 ~; 181 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 190 ( 190 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c8 > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(sk_c8,type,
sk_c8: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_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_98,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_134,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( multiply(X3,sk_c7) != sk_c8 )
| ( inverse(X3) != sk_c7 )
| ( inverse(X4) != sk_c7 )
| ( multiply(X4,sk_c6) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c6 )
| ( multiply(X1,sk_c8) != sk_c7 )
| ( inverse(X1) != sk_c8 )
| ( multiply(sk_c8,X2) != sk_c7 )
| ( multiply(X5,sk_c8) != X2 )
| ( inverse(X5) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( multiply(sk_c2,sk_c6) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_128,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_131,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c8) = 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_50860,plain,
! [X_433,Y_434,Z_435] : ( multiply(multiply(X_433,Y_434),Z_435) = multiply(X_433,multiply(Y_434,Z_435)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_50896,plain,
! [X_2,Z_435] : ( multiply(inverse(X_2),multiply(X_2,Z_435)) = multiply(identity,Z_435) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_50860]) ).
tff(c_50907,plain,
! [X_2,Z_435] : ( multiply(inverse(X_2),multiply(X_2,Z_435)) = Z_435 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50896]) ).
tff(c_51093,plain,
! [X_439,Z_440] : ( multiply(inverse(X_439),multiply(X_439,Z_440)) = Z_440 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50896]) ).
tff(c_51394,plain,
! [X_443,Z_444] : ( multiply(inverse(inverse(X_443)),Z_444) = multiply(X_443,Z_444) ),
inference(superposition,[status(thm),theory(equality)],[c_50907,c_51093]) ).
tff(c_51123,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_51093]) ).
tff(c_51401,plain,
! [X_443] : ( multiply(X_443,identity) = X_443 ),
inference(superposition,[status(thm),theory(equality)],[c_51394,c_51123]) ).
tff(c_36343,plain,
! [X_298,Y_299,Z_300] : ( multiply(multiply(X_298,Y_299),Z_300) = multiply(X_298,multiply(Y_299,Z_300)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_36379,plain,
! [X_2,Z_300] : ( multiply(inverse(X_2),multiply(X_2,Z_300)) = multiply(identity,Z_300) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_36343]) ).
tff(c_36390,plain,
! [X_2,Z_300] : ( multiply(inverse(X_2),multiply(X_2,Z_300)) = Z_300 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36379]) ).
tff(c_36573,plain,
! [X_304,Z_305] : ( multiply(inverse(X_304),multiply(X_304,Z_305)) = Z_305 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36379]) ).
tff(c_36877,plain,
! [X_308,Z_309] : ( multiply(inverse(inverse(X_308)),Z_309) = multiply(X_308,Z_309) ),
inference(superposition,[status(thm),theory(equality)],[c_36390,c_36573]) ).
tff(c_36624,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_36573]) ).
tff(c_36884,plain,
! [X_308] : ( multiply(X_308,identity) = X_308 ),
inference(superposition,[status(thm),theory(equality)],[c_36877,c_36624]) ).
tff(c_30,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_33808,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_42,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_98,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_102,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_33858,plain,
! [X_246,Y_247,Z_248] : ( multiply(multiply(X_246,Y_247),Z_248) = multiply(X_246,multiply(Y_247,Z_248)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_33897,plain,
! [Z_248] : ( multiply(sk_c7,multiply(sk_c1,Z_248)) = multiply(identity,Z_248) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_33858]) ).
tff(c_33917,plain,
! [Z_249] : ( multiply(sk_c7,multiply(sk_c1,Z_249)) = Z_249 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33897]) ).
tff(c_33929,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33808,c_33917]) ).
tff(c_60,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_115,plain,
multiply(sk_c2,sk_c6) = sk_c7,
inference(splitLeft,[status(thm)],[c_60]) ).
tff(c_54,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_85,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_89,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
tff(c_32954,plain,
! [X_230,Y_231,Z_232] : ( multiply(multiply(X_230,Y_231),Z_232) = multiply(X_230,multiply(Y_231,Z_232)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_32996,plain,
! [Z_232] : ( multiply(sk_c7,multiply(sk_c2,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_32954]) ).
tff(c_33193,plain,
! [Z_238] : ( multiply(sk_c7,multiply(sk_c2,Z_238)) = Z_238 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32996]) ).
tff(c_33205,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_115,c_33193]) ).
tff(c_149,plain,
! [X_13,Y_14,Z_15] : ( multiply(multiply(X_13,Y_14),Z_15) = multiply(X_13,multiply(Y_14,Z_15)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_179,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_149]) ).
tff(c_424,plain,
! [X_21,Z_22] : ( multiply(inverse(X_21),multiply(X_21,Z_22)) = Z_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_189,plain,
! [X_2,Z_15] : ( multiply(inverse(X_2),multiply(X_2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_749,plain,
! [X_27,Z_28] : ( multiply(inverse(inverse(X_27)),Z_28) = multiply(X_27,Z_28) ),
inference(superposition,[status(thm),theory(equality)],[c_424,c_189]) ).
tff(c_472,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_424]) ).
tff(c_756,plain,
! [X_27] : ( multiply(X_27,identity) = X_27 ),
inference(superposition,[status(thm),theory(equality)],[c_749,c_472]) ).
tff(c_12,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_120,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_126,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_173,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_149]) ).
tff(c_191,plain,
! [Z_16] : ( multiply(sk_c7,multiply(sk_c1,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_173]) ).
tff(c_203,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_126,c_191]) ).
tff(c_207,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_120,c_203]) ).
tff(c_211,plain,
multiply(sk_c2,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_207,c_115]) ).
tff(c_176,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c2,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_149]) ).
tff(c_188,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c2,Z_15)) = Z_15 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_176]) ).
tff(c_408,plain,
! [Z_20] : ( multiply(sk_c6,multiply(sk_c2,Z_20)) = Z_20 ),
inference(demodulation,[status(thm),theory(equality)],[c_207,c_188]) ).
tff(c_420,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_211,c_408]) ).
tff(c_554,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_420,c_189]) ).
tff(c_560,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_554]) ).
tff(c_210,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_207,c_120]) ).
tff(c_460,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_210,c_424]) ).
tff(c_481,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_460]) ).
tff(c_300,plain,
! [X_18,Z_19] : ( multiply(inverse(X_18),multiply(X_18,Z_19)) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_336,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_210,c_300]) ).
tff(c_358,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_336]) ).
tff(c_68,plain,
! [X5_6,X1_8,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_242,plain,
! [X5_6,X1_8,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c6 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c6 )
| ( multiply(sk_c8,sk_c6) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( inverse(X4_10) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_210,c_207,c_207,c_207,c_207,c_207,c_207,c_207,c_207,c_68]) ).
tff(c_243,plain,
multiply(sk_c8,sk_c6) != sk_c6,
inference(splitLeft,[status(thm)],[c_242]) ).
tff(c_361,plain,
multiply(identity,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_358,c_243]) ).
tff(c_365,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_361]) ).
tff(c_366,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c8 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( inverse(X4_10) != sk_c6 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c6 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_242]) ).
tff(c_9313,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_756,c_560,c_481,c_2,c_481,c_481,c_756,c_560,c_481,c_481,c_560,c_756,c_560,c_560,c_756,c_560,c_481,c_560,c_366]) ).
tff(c_9315,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9313]) ).
tff(c_213,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_207,c_98]) ).
tff(c_570,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_560,c_213]) ).
tff(c_598,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_570,c_4]) ).
tff(c_626,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_598,c_189]) ).
tff(c_638,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_626]) ).
tff(c_643,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_638,c_570]) ).
tff(c_9317,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_9315,c_643]) ).
tff(c_9318,plain,
! [X1_8,X4_10,X3_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_9313]) ).
tff(c_31728,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_9318]) ).
tff(c_31730,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31728,c_643]) ).
tff(c_31731,plain,
! [X4_10,X1_8] :
( ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_9318]) ).
tff(c_31733,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_31731]) ).
tff(c_31735,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_31733,c_643]) ).
tff(c_32893,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_31731]) ).
tff(c_32895,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32893,c_643]) ).
tff(c_32897,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_26,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_32941,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_32897,c_26]) ).
tff(c_28,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_32946,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_32897,c_28]) ).
tff(c_32896,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_32901,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_32896,c_4]) ).
tff(c_32984,plain,
! [Z_232] : ( multiply(sk_c8,multiply(sk_c4,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_32901,c_32954]) ).
tff(c_33216,plain,
! [Z_239] : ( multiply(sk_c8,multiply(sk_c4,Z_239)) = Z_239 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32984]) ).
tff(c_33228,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_32946,c_33216]) ).
tff(c_33232,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_32941,c_33228]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_32927,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_32897,c_22]) ).
tff(c_33332,plain,
multiply(sk_c3,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33232,c_32927]) ).
tff(c_24,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_32909,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_32897,c_24]) ).
tff(c_32913,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_32909,c_4]) ).
tff(c_32981,plain,
! [Z_232] : ( multiply(sk_c8,multiply(sk_c3,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_32913,c_32954]) ).
tff(c_33007,plain,
! [Z_232] : ( multiply(sk_c8,multiply(sk_c3,Z_232)) = Z_232 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32981]) ).
tff(c_33401,plain,
! [Z_241] : ( multiply(sk_c7,multiply(sk_c3,Z_241)) = Z_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_33232,c_33007]) ).
tff(c_33413,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_33332,c_33401]) ).
tff(c_33417,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33205,c_33413]) ).
tff(c_33477,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33417,c_33417,c_33205]) ).
tff(c_32999,plain,
! [X_2,Z_232] : ( multiply(inverse(X_2),multiply(X_2,Z_232)) = multiply(identity,Z_232) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_32954]) ).
tff(c_33011,plain,
! [X_2,Z_232] : ( multiply(inverse(X_2),multiply(X_2,Z_232)) = Z_232 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_32999]) ).
tff(c_33627,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_33477,c_33011]) ).
tff(c_33633,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_33627]) ).
tff(c_33482,plain,
inverse(sk_c1) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33417,c_98]) ).
tff(c_33510,plain,
multiply(sk_c6,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33482,c_4]) ).
tff(c_33775,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33633,c_33510]) ).
tff(c_33336,plain,
multiply(sk_c1,sk_c7) != sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33232,c_32897]) ).
tff(c_33470,plain,
multiply(sk_c1,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33417,c_33417,c_33336]) ).
tff(c_33674,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_33633,c_33633,c_33470]) ).
tff(c_33793,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33775,c_33674]) ).
tff(c_33795,plain,
multiply(sk_c7,sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_8,plain,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_33838,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_33795,c_8]) ).
tff(c_33942,plain,
! [X5_6,X1_8,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 )
| ( inverse(X1_8) != sk_c8 )
| ( multiply(X1_8,sk_c8) != sk_c7 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c8 )
| ( sk_c7 != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_33929,c_33838,c_68]) ).
tff(c_33943,plain,
sk_c7 != sk_c6,
inference(splitLeft,[status(thm)],[c_33942]) ).
tff(c_33794,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_10,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_33851,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_33795,c_10]) ).
tff(c_33903,plain,
! [X_2,Z_248] : ( multiply(inverse(X_2),multiply(X_2,Z_248)) = multiply(identity,Z_248) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_33858]) ).
tff(c_33984,plain,
! [X_252,Z_253] : ( multiply(inverse(X_252),multiply(X_252,Z_253)) = Z_253 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_33903]) ).
tff(c_34020,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_33851,c_33984]) ).
tff(c_34070,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33838,c_33794,c_34020]) ).
tff(c_14,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_33844,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_33795,c_14]) ).
tff(c_18,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_33816,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_33795,c_18]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_33831,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_33795,c_16]) ).
tff(c_34029,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_33831,c_33984]) ).
tff(c_34071,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_33844,c_33816,c_34029]) ).
tff(c_34092,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34070,c_34071]) ).
tff(c_34093,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33943,c_34092]) ).
tff(c_34095,plain,
sk_c7 = sk_c6,
inference(splitRight,[status(thm)],[c_33942]) ).
tff(c_33933,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_33929,c_33795]) ).
tff(c_34126,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_34095,c_33933]) ).
tff(c_34128,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_20,plain,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_34148,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_34128,c_20]) ).
tff(c_34153,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34128,c_22]) ).
tff(c_33799,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_33794,c_4]) ).
tff(c_34180,plain,
! [X_255,Y_256,Z_257] : ( multiply(multiply(X_255,Y_256),Z_257) = multiply(X_255,multiply(Y_256,Z_257)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_34210,plain,
! [Z_257] : ( multiply(sk_c8,multiply(sk_c3,Z_257)) = multiply(identity,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_33799,c_34180]) ).
tff(c_34274,plain,
! [Z_260] : ( multiply(sk_c8,multiply(sk_c3,Z_260)) = Z_260 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34210]) ).
tff(c_34286,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_34153,c_34274]) ).
tff(c_34290,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34148,c_34286]) ).
tff(c_34166,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34128,c_26]) ).
tff(c_34292,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_34290,c_34166]) ).
tff(c_34127,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_34298,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34290,c_34127]) ).
tff(c_34158,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_33795,c_16]) ).
tff(c_34293,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_34290,c_34158]) ).
tff(c_34222,plain,
! [X_2,Z_257] : ( multiply(inverse(X_2),multiply(X_2,Z_257)) = multiply(identity,Z_257) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34180]) ).
tff(c_34234,plain,
! [X_2,Z_257] : ( multiply(inverse(X_2),multiply(X_2,Z_257)) = Z_257 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34222]) ).
tff(c_34445,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_34293,c_34234]) ).
tff(c_34451,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34292,c_34298,c_34445]) ).
tff(c_34295,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34290,c_34148]) ).
tff(c_34502,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34451,c_34295]) ).
tff(c_34506,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_34502,c_34234]) ).
tff(c_34512,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_34506]) ).
tff(c_34300,plain,
multiply(sk_c7,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34290,c_33795]) ).
tff(c_34455,plain,
multiply(sk_c6,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34451,c_34300]) ).
tff(c_34635,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34512,c_34455]) ).
tff(c_34637,plain,
multiply(sk_c2,sk_c6) != sk_c7,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_56,plain,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_35682,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_34637,c_56]) ).
tff(c_58,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_35676,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34637,c_58]) ).
tff(c_34636,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_60]) ).
tff(c_34641,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34636,c_4]) ).
tff(c_35700,plain,
! [X_286,Y_287,Z_288] : ( multiply(multiply(X_286,Y_287),Z_288) = multiply(X_286,multiply(Y_287,Z_288)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_35733,plain,
! [Z_288] : ( multiply(sk_c8,multiply(sk_c3,Z_288)) = multiply(identity,Z_288) ),
inference(superposition,[status(thm),theory(equality)],[c_34641,c_35700]) ).
tff(c_35782,plain,
! [Z_291] : ( multiply(sk_c8,multiply(sk_c3,Z_291)) = Z_291 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35733]) ).
tff(c_35794,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_35676,c_35782]) ).
tff(c_35798,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35682,c_35794]) ).
tff(c_62,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_35689,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34637,c_62]) ).
tff(c_35800,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35798,c_35689]) ).
tff(c_34678,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_34645,plain,
multiply(sk_c1,sk_c7) = sk_c8,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_34705,plain,
! [X_266,Y_267,Z_268] : ( multiply(multiply(X_266,Y_267),Z_268) = multiply(X_266,multiply(Y_267,Z_268)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_34744,plain,
! [Z_268] : ( multiply(sk_c7,multiply(sk_c1,Z_268)) = multiply(identity,Z_268) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_34705]) ).
tff(c_34866,plain,
! [Z_271] : ( multiply(sk_c7,multiply(sk_c1,Z_271)) = Z_271 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34744]) ).
tff(c_34878,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34645,c_34866]) ).
tff(c_34882,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34678,c_34878]) ).
tff(c_34695,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_34637,c_62]) ).
tff(c_34885,plain,
multiply(sk_c8,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34882,c_34695]) ).
tff(c_64,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_34684,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_34637,c_64]) ).
tff(c_66,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c2,sk_c6) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_34656,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_34637,c_66]) ).
tff(c_34660,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_34656,c_4]) ).
tff(c_34735,plain,
! [Z_268] : ( multiply(sk_c8,multiply(sk_c4,Z_268)) = multiply(identity,Z_268) ),
inference(superposition,[status(thm),theory(equality)],[c_34660,c_34705]) ).
tff(c_34981,plain,
! [Z_273] : ( multiply(sk_c8,multiply(sk_c4,Z_273)) = Z_273 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34735]) ).
tff(c_34993,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_34684,c_34981]) ).
tff(c_34997,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34885,c_34993]) ).
tff(c_34673,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_34637,c_56]) ).
tff(c_34887,plain,
multiply(sk_c8,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34882,c_34673]) ).
tff(c_34999,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34997,c_34887]) ).
tff(c_34750,plain,
! [X_2,Z_268] : ( multiply(inverse(X_2),multiply(X_2,Z_268)) = multiply(identity,Z_268) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_34705]) ).
tff(c_34762,plain,
! [X_2,Z_268] : ( multiply(inverse(X_2),multiply(X_2,Z_268)) = Z_268 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34750]) ).
tff(c_35080,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_34999,c_34762]) ).
tff(c_35086,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_35080]) ).
tff(c_34892,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_34882,c_89]) ).
tff(c_35094,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35086,c_34892]) ).
tff(c_35213,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_35094,c_34762]) ).
tff(c_35225,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_35213]) ).
tff(c_34889,plain,
multiply(sk_c2,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_34882,c_34637]) ).
tff(c_35093,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_35086,c_35086,c_34889]) ).
tff(c_35269,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35225,c_35093]) ).
tff(c_35271,plain,
multiply(sk_c7,sk_c8) != sk_c6,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_35291,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_35271,c_14]) ).
tff(c_35279,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_34637,c_64]) ).
tff(c_35298,plain,
! [X_277,Y_278,Z_279] : ( multiply(multiply(X_277,Y_278),Z_279) = multiply(X_277,multiply(Y_278,Z_279)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_35325,plain,
! [Z_279] : ( multiply(sk_c8,multiply(sk_c4,Z_279)) = multiply(identity,Z_279) ),
inference(superposition,[status(thm),theory(equality)],[c_34660,c_35298]) ).
tff(c_35393,plain,
! [Z_282] : ( multiply(sk_c8,multiply(sk_c4,Z_282)) = Z_282 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35325]) ).
tff(c_35405,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_35279,c_35393]) ).
tff(c_35409,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35291,c_35405]) ).
tff(c_35334,plain,
! [Z_279] : ( multiply(sk_c7,multiply(sk_c1,Z_279)) = multiply(identity,Z_279) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_35298]) ).
tff(c_35354,plain,
! [Z_280] : ( multiply(sk_c7,multiply(sk_c1,Z_280)) = Z_280 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35334]) ).
tff(c_35366,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_34645,c_35354]) ).
tff(c_35411,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_35409,c_35366]) ).
tff(c_35340,plain,
! [X_2,Z_279] : ( multiply(inverse(X_2),multiply(X_2,Z_279)) = multiply(identity,Z_279) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_35298]) ).
tff(c_35352,plain,
! [X_2,Z_279] : ( multiply(inverse(X_2),multiply(X_2,Z_279)) = Z_279 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35340]) ).
tff(c_35496,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_35411,c_35352]) ).
tff(c_35502,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_35496]) ).
tff(c_35372,plain,
sk_c7 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35366,c_35271]) ).
tff(c_35521,plain,
sk_c6 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_35502,c_35372]) ).
tff(c_35415,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35409,c_34673]) ).
tff(c_35635,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_35502,c_2,c_35502,c_35415]) ).
tff(c_35636,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35521,c_35635]) ).
tff(c_35637,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_35808,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35798,c_35637]) ).
tff(c_35638,plain,
multiply(sk_c1,sk_c7) != sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_35664,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_35638,c_28]) ).
tff(c_35804,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_35798,c_35664]) ).
tff(c_35742,plain,
! [X_2,Z_288] : ( multiply(inverse(X_2),multiply(X_2,Z_288)) = multiply(identity,Z_288) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_35700]) ).
tff(c_36012,plain,
! [X_294,Z_295] : ( multiply(inverse(X_294),multiply(X_294,Z_295)) = Z_295 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35742]) ).
tff(c_36036,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_35804,c_36012]) ).
tff(c_36082,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35800,c_35808,c_36036]) ).
tff(c_35801,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_35798,c_35682]) ).
tff(c_36123,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36082,c_35801]) ).
tff(c_35754,plain,
! [X_2,Z_288] : ( multiply(inverse(X_2),multiply(X_2,Z_288)) = Z_288 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35742]) ).
tff(c_36127,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_36123,c_35754]) ).
tff(c_36133,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_36127]) ).
tff(c_36094,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36082,c_89]) ).
tff(c_36260,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36133,c_36094]) ).
tff(c_36091,plain,
multiply(sk_c2,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36082,c_34637]) ).
tff(c_36258,plain,
multiply(sk_c2,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_36133,c_36133,c_36091]) ).
tff(c_36261,plain,
multiply(identity,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_36260,c_36258]) ).
tff(c_36265,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36261]) ).
tff(c_36267,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_36,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_36268,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_36276,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_36267,c_36268]) ).
tff(c_36278,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_32,plain,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_36318,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_36278,c_32]) ).
tff(c_34,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_36313,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_36278,c_34]) ).
tff(c_36277,plain,
inverse(sk_c3) = sk_c8,
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_36289,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_36277,c_4]) ).
tff(c_36370,plain,
! [Z_300] : ( multiply(sk_c8,multiply(sk_c3,Z_300)) = multiply(identity,Z_300) ),
inference(superposition,[status(thm),theory(equality)],[c_36289,c_36343]) ).
tff(c_36392,plain,
! [Z_301] : ( multiply(sk_c8,multiply(sk_c3,Z_301)) = Z_301 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36370]) ).
tff(c_36404,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_36313,c_36392]) ).
tff(c_36408,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36318,c_36404]) ).
tff(c_36410,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36408,c_36318]) ).
tff(c_36606,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36410,c_36573]) ).
tff(c_36633,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_36606]) ).
tff(c_38,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_36307,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_36278,c_38]) ).
tff(c_36412,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_36408,c_36307]) ).
tff(c_36656,plain,
multiply(sk_c6,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36633,c_36412]) ).
tff(c_36266,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_36417,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36408,c_36266]) ).
tff(c_40,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_36302,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_36278,c_40]) ).
tff(c_36413,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_36408,c_36302]) ).
tff(c_36600,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_36413,c_36573]) ).
tff(c_36632,plain,
multiply(sk_c6,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36417,c_36600]) ).
tff(c_36724,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36656,c_36632]) ).
tff(c_36460,plain,
! [X_302,Z_303] : ( multiply(inverse(X_302),multiply(X_302,Z_303)) = Z_303 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36379]) ).
tff(c_36484,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_36410,c_36460]) ).
tff(c_36510,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_36484]) ).
tff(c_36429,plain,
! [X5_6,X1_8,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(sk_c6,multiply(X5_6,sk_c6)) != sk_c7 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_36408,c_36408,c_36408,c_36408,c_36408,c_36408,c_36408,c_36408,c_68]) ).
tff(c_36430,plain,
multiply(sk_c7,sk_c6) != sk_c6,
inference(splitLeft,[status(thm)],[c_36429]) ).
tff(c_36511,plain,
multiply(identity,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_36510,c_36430]) ).
tff(c_36518,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_36511]) ).
tff(c_36519,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( multiply(sk_c6,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(sk_c6,multiply(X5_6,sk_c6)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_36429]) ).
tff(c_45113,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_36884,c_36724,c_2,c_36724,c_36633,c_36724,c_36884,c_36724,c_36633,c_36724,c_36633,c_36884,c_36724,c_36633,c_36884,c_36724,c_36633,c_36633,c_36724,c_2,c_36724,c_36633,c_36519]) ).
tff(c_45115,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_45113]) ).
tff(c_36638,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36633,c_89]) ).
tff(c_36671,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_36638,c_36390]) ).
tff(c_36683,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_36671]) ).
tff(c_36639,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36633,c_85]) ).
tff(c_36687,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_36683,c_36639]) ).
tff(c_45117,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_45115,c_36687]) ).
tff(c_45118,plain,
! [X1_8,X4_10,X3_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_45113]) ).
tff(c_49953,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_45118]) ).
tff(c_49955,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_49953,c_36687]) ).
tff(c_49956,plain,
! [X4_10,X1_8] :
( ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_45118]) ).
tff(c_49958,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_49956]) ).
tff(c_49960,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_49958,c_36687]) ).
tff(c_50777,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_49956]) ).
tff(c_50779,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_50777,c_36687]) ).
tff(c_50781,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_44,plain,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_50828,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_50781,c_44]) ).
tff(c_46,plain,
( ( multiply(sk_c3,sk_c8) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_50843,plain,
multiply(sk_c3,sk_c8) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_50781,c_46]) ).
tff(c_48,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_50793,plain,
inverse(sk_c3) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_50781,c_48]) ).
tff(c_50797,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_50793,c_4]) ).
tff(c_50890,plain,
! [Z_435] : ( multiply(sk_c8,multiply(sk_c3,Z_435)) = multiply(identity,Z_435) ),
inference(superposition,[status(thm),theory(equality)],[c_50797,c_50860]) ).
tff(c_50909,plain,
! [Z_436] : ( multiply(sk_c8,multiply(sk_c3,Z_436)) = Z_436 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50890]) ).
tff(c_50921,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_50843,c_50909]) ).
tff(c_50925,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_50828,c_50921]) ).
tff(c_50929,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_50925,c_50828]) ).
tff(c_51143,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_50929,c_50907]) ).
tff(c_51149,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_51143]) ).
tff(c_50,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_50835,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_50781,c_50]) ).
tff(c_50928,plain,
multiply(sk_c6,sk_c5) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_50925,c_50835]) ).
tff(c_51181,plain,
multiply(sk_c6,sk_c5) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51149,c_50928]) ).
tff(c_50780,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_50934,plain,
inverse(sk_c4) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_50925,c_50780]) ).
tff(c_52,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_50821,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_50781,c_52]) ).
tff(c_50930,plain,
multiply(sk_c4,sk_c6) = sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_50925,c_50821]) ).
tff(c_51221,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_50930,c_50907]) ).
tff(c_51227,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51181,c_50934,c_51221]) ).
tff(c_50976,plain,
! [X_437,Z_438] : ( multiply(inverse(X_437),multiply(X_437,Z_438)) = Z_438 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_50896]) ).
tff(c_51000,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_50929,c_50976]) ).
tff(c_51027,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_51000]) ).
tff(c_50939,plain,
! [X5_6,X1_8,X4_10,X3_7] :
( ( inverse(X5_6) != sk_c6 )
| ( multiply(sk_c6,multiply(X5_6,sk_c6)) != sk_c7 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_50925,c_50925,c_50925,c_50925,c_50925,c_50925,c_50925,c_50925,c_68]) ).
tff(c_50940,plain,
multiply(sk_c7,sk_c6) != sk_c6,
inference(splitLeft,[status(thm)],[c_50939]) ).
tff(c_51083,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51027,c_50940]) ).
tff(c_51084,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( multiply(sk_c6,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c7 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(sk_c6,multiply(X5_6,sk_c6)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_50939]) ).
tff(c_58238,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_51401,c_51227,c_2,c_51227,c_51149,c_51227,c_51401,c_51227,c_51149,c_51227,c_51149,c_51401,c_51227,c_51149,c_51401,c_51227,c_51149,c_51149,c_51227,c_2,c_51227,c_51149,c_51084]) ).
tff(c_58240,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_58238]) ).
tff(c_50932,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_50925,c_50793]) ).
tff(c_51136,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_50932,c_4]) ).
tff(c_51241,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_51227,c_51136]) ).
tff(c_51234,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51227,c_50932]) ).
tff(c_51250,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_51241,c_51234]) ).
tff(c_58242,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_58240,c_51250]) ).
tff(c_58243,plain,
! [X1_8,X4_10,X3_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_58238]) ).
tff(c_61197,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_58243]) ).
tff(c_61199,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61197,c_51250]) ).
tff(c_61200,plain,
! [X4_10,X1_8] :
( ( identity != X4_10 )
| ( inverse(X4_10) != identity )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_58243]) ).
tff(c_61202,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_61200]) ).
tff(c_61204,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61202,c_51250]) ).
tff(c_61755,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_61200]) ).
tff(c_61757,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_61755,c_51250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP332-1 : TPTP v9.0.0. Released v2.5.0.
% 0.03/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.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:42:20 EDT 2025
% 0.13/0.34 % CPUTime :
% 17.91/7.15 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.96/7.19
% 17.96/7.19 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------