%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP286-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 : n007.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:48 PM UTC 2025
% Result : Unsatisfiable 14.22s 4.64s
% Output : CNFRefutation 14.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 31
% Syntax : Number of formulae : 343 ( 270 unt; 0 typ; 0 def)
% Number of atoms : 516 ( 497 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 339 ( 166 ~; 173 |; 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 : 173 ( 173 !; 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_c8) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_116,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_125,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_152,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(sk_c8,sk_c7) != sk_c6 )
| ( multiply(X3,sk_c8) != sk_c7 )
| ( inverse(X3) != sk_c8 )
| ( multiply(X4,sk_c7) != sk_c6 )
| ( inverse(X4) != sk_c7 )
| ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( multiply(X1,sk_c7) != sk_c8 )
| ( inverse(X1) != sk_c7 )
| ( multiply(sk_c8,X2) != sk_c7 )
| ( multiply(X5,sk_c8) != X2 )
| ( inverse(X5) != sk_c8 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ( multiply(sk_c2,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c1,sk_c8) = sk_c7 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( multiply(sk_c8,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_110,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c8,sk_c5) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_101,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_104,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_107,axiom,
( ( inverse(sk_c1) = sk_c8 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_137,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c7,sk_c8) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_140,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c8 ) ),
file(unknown,unknown) ).
tff(f_143,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_149,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c4,sk_c8) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_146,axiom,
( ( inverse(sk_c2) = sk_c7 )
| ( multiply(sk_c8,sk_c5) = 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_25110,plain,
! [X_310,Y_311,Z_312] : ( multiply(multiply(X_310,Y_311),Z_312) = multiply(X_310,multiply(Y_311,Z_312)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_25146,plain,
! [X_2,Z_312] : ( multiply(inverse(X_2),multiply(X_2,Z_312)) = multiply(identity,Z_312) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25110]) ).
tff(c_25475,plain,
! [X_318,Z_319] : ( multiply(inverse(X_318),multiply(X_318,Z_319)) = Z_319 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25146]) ).
tff(c_25157,plain,
! [X_2,Z_312] : ( multiply(inverse(X_2),multiply(X_2,Z_312)) = Z_312 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25146]) ).
tff(c_25754,plain,
! [X_321,Z_322] : ( multiply(inverse(inverse(X_321)),Z_322) = multiply(X_321,Z_322) ),
inference(superposition,[status(thm),theory(equality)],[c_25475,c_25157]) ).
tff(c_25526,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_25475]) ).
tff(c_25761,plain,
! [X_321] : ( multiply(X_321,identity) = X_321 ),
inference(superposition,[status(thm),theory(equality)],[c_25754,c_25526]) ).
tff(c_14477,plain,
! [X_175,Y_176,Z_177] : ( multiply(multiply(X_175,Y_176),Z_177) = multiply(X_175,multiply(Y_176,Z_177)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14513,plain,
! [X_2,Z_177] : ( multiply(inverse(X_2),multiply(X_2,Z_177)) = multiply(identity,Z_177) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14477]) ).
tff(c_14524,plain,
! [X_2,Z_177] : ( multiply(inverse(X_2),multiply(X_2,Z_177)) = Z_177 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14513]) ).
tff(c_16346,plain,
! [X_214,Z_215] : ( multiply(inverse(X_214),multiply(X_214,Z_215)) = Z_215 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14513]) ).
tff(c_16736,plain,
! [X_218,Z_219] : ( multiply(inverse(inverse(X_218)),Z_219) = multiply(X_218,Z_219) ),
inference(superposition,[status(thm),theory(equality)],[c_14524,c_16346]) ).
tff(c_16394,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_16346]) ).
tff(c_16743,plain,
! [X_218] : ( multiply(X_218,identity) = X_218 ),
inference(superposition,[status(thm),theory(equality)],[c_16736,c_16394]) ).
tff(c_30,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_13638,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_42,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_98,plain,
inverse(sk_c1) = sk_c8,
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_102,plain,
multiply(sk_c8,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_98,c_4]) ).
tff(c_13693,plain,
! [X_158,Y_159,Z_160] : ( multiply(multiply(X_158,Y_159),Z_160) = multiply(X_158,multiply(Y_159,Z_160)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13732,plain,
! [Z_160] : ( multiply(sk_c8,multiply(sk_c1,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_13693]) ).
tff(c_13752,plain,
! [Z_161] : ( multiply(sk_c8,multiply(sk_c1,Z_161)) = Z_161 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13732]) ).
tff(c_13764,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_13638,c_13752]) ).
tff(c_12,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_115,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_121,plain,
multiply(sk_c1,sk_c8) = sk_c7,
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_12443,plain,
! [X_138,Y_139,Z_140] : ( multiply(multiply(X_138,Y_139),Z_140) = multiply(X_138,multiply(Y_139,Z_140)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12482,plain,
! [Z_140] : ( multiply(sk_c8,multiply(sk_c1,Z_140)) = multiply(identity,Z_140) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_12443]) ).
tff(c_12502,plain,
! [Z_141] : ( multiply(sk_c8,multiply(sk_c1,Z_141)) = Z_141 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12482]) ).
tff(c_12514,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_121,c_12502]) ).
tff(c_12518,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_115,c_12514]) ).
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_294,plain,
! [X_19,Z_20] : ( multiply(inverse(X_19),multiply(X_19,Z_20)) = Z_20 ),
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_604,plain,
! [X_24,Z_25] : ( multiply(inverse(inverse(X_24)),Z_25) = multiply(X_24,Z_25) ),
inference(superposition,[status(thm),theory(equality)],[c_294,c_189]) ).
tff(c_345,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_294]) ).
tff(c_615,plain,
! [X_24] : ( multiply(X_24,identity) = X_24 ),
inference(superposition,[status(thm),theory(equality)],[c_604,c_345]) ).
tff(c_173,plain,
! [Z_15] : ( multiply(sk_c8,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_c8,multiply(sk_c1,Z_16)) = Z_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_173]) ).
tff(c_203,plain,
multiply(sk_c8,sk_c7) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_121,c_191]) ).
tff(c_207,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_115,c_203]) ).
tff(c_210,plain,
multiply(sk_c6,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_207,c_115]) ).
tff(c_321,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_210,c_294]) ).
tff(c_353,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_321]) ).
tff(c_48,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_126,plain,
multiply(sk_c2,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_48]) ).
tff(c_66,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_85,plain,
inverse(sk_c2) = sk_c7,
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_89,plain,
multiply(sk_c7,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_85,c_4]) ).
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_253,plain,
! [Z_17] : ( multiply(sk_c7,multiply(sk_c2,Z_17)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_176]) ).
tff(c_265,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_126,c_253]) ).
tff(c_315,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_265,c_294]) ).
tff(c_352,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_315]) ).
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_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( multiply(sk_c7,sk_c8) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_239,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_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( multiply(sk_c7,sk_c6) != sk_c6 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c7 )
| ( multiply(sk_c6,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_207,c_207,c_207,c_207,c_207,c_207,c_207,c_207,c_68]) ).
tff(c_240,plain,
multiply(sk_c6,sk_c7) != sk_c6,
inference(splitLeft,[status(thm)],[c_239]) ).
tff(c_241,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_240,c_210]) ).
tff(c_242,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( multiply(sk_c7,sk_c6) != sk_c6 )
| ( inverse(X3_7) != sk_c6 )
| ( multiply(X3_7,sk_c6) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c6 )
| ( inverse(X5_6) != sk_c6 )
| ( multiply(sk_c6,multiply(X5_6,sk_c6)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_239]) ).
tff(c_7734,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_615,c_353,c_352,c_2,c_352,c_352,c_615,c_353,c_352,c_353,c_615,c_353,c_352,c_353,c_615,c_353,c_352,c_352,c_2,c_353,c_352,c_352,c_242]) ).
tff(c_7736,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_7734]) ).
tff(c_371,plain,
multiply(identity,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_353,c_89]) ).
tff(c_454,plain,
multiply(inverse(identity),identity) = sk_c2,
inference(superposition,[status(thm),theory(equality)],[c_371,c_189]) ).
tff(c_466,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_454]) ).
tff(c_372,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_353,c_85]) ).
tff(c_472,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_466,c_372]) ).
tff(c_7738,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7736,c_472]) ).
tff(c_7739,plain,
! [X1_8,X4_10,X3_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_7734]) ).
tff(c_11759,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_7739]) ).
tff(c_11761,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11759,c_472]) ).
tff(c_11762,plain,
! [X4_10,X1_8] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_7739]) ).
tff(c_11764,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_11762]) ).
tff(c_11766,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11764,c_472]) ).
tff(c_12382,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_11762]) ).
tff(c_12384,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12382,c_472]) ).
tff(c_12386,plain,
multiply(sk_c2,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_48]) ).
tff(c_44,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_12433,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12386,c_44]) ).
tff(c_12616,plain,
multiply(sk_c7,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12518,c_12433]) ).
tff(c_46,plain,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_12428,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_12386,c_46]) ).
tff(c_12617,plain,
multiply(sk_c3,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12518,c_12428]) ).
tff(c_12385,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_48]) ).
tff(c_12390,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12385,c_4]) ).
tff(c_12473,plain,
! [Z_140] : ( multiply(sk_c7,multiply(sk_c3,Z_140)) = multiply(identity,Z_140) ),
inference(superposition,[status(thm),theory(equality)],[c_12390,c_12443]) ).
tff(c_12718,plain,
! [Z_144] : ( multiply(sk_c7,multiply(sk_c3,Z_144)) = Z_144 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12473]) ).
tff(c_12730,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_12617,c_12718]) ).
tff(c_12734,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12616,c_12730]) ).
tff(c_12739,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12734,c_12616]) ).
tff(c_12488,plain,
! [X_2,Z_140] : ( multiply(inverse(X_2),multiply(X_2,Z_140)) = multiply(identity,Z_140) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_12443]) ).
tff(c_12500,plain,
! [X_2,Z_140] : ( multiply(inverse(X_2),multiply(X_2,Z_140)) = Z_140 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12488]) ).
tff(c_12879,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_12739,c_12500]) ).
tff(c_12885,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_12879]) ).
tff(c_12746,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12734,c_85]) ).
tff(c_12761,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_12746,c_4]) ).
tff(c_12952,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12885,c_12761]) ).
tff(c_12743,plain,
multiply(sk_c2,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_12734,c_12386]) ).
tff(c_12989,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12952,c_12885,c_12885,c_12743]) ).
tff(c_12991,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_20,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_13021,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_12991,c_20]) ).
tff(c_22,plain,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_13026,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_12991,c_22]) ).
tff(c_24,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_13003,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12991,c_24]) ).
tff(c_13007,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13003,c_4]) ).
tff(c_13053,plain,
! [X_148,Y_149,Z_150] : ( multiply(multiply(X_148,Y_149),Z_150) = multiply(X_148,multiply(Y_149,Z_150)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_13083,plain,
! [Z_150] : ( multiply(sk_c7,multiply(sk_c3,Z_150)) = multiply(identity,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_13007,c_13053]) ).
tff(c_13148,plain,
! [Z_153] : ( multiply(sk_c7,multiply(sk_c3,Z_153)) = Z_153 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13083]) ).
tff(c_13160,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13026,c_13148]) ).
tff(c_13164,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13021,c_13160]) ).
tff(c_13176,plain,
multiply(sk_c6,sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13164,c_89]) ).
tff(c_12990,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_13045,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_12991,c_28]) ).
tff(c_13098,plain,
! [X_2,Z_150] : ( multiply(inverse(X_2),multiply(X_2,Z_150)) = multiply(identity,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13053]) ).
tff(c_13231,plain,
! [X_154,Z_155] : ( multiply(inverse(X_154),multiply(X_154,Z_155)) = Z_155 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13098]) ).
tff(c_13258,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_13045,c_13231]) ).
tff(c_13280,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_12990,c_13258]) ).
tff(c_13110,plain,
! [X_2,Z_150] : ( multiply(inverse(X_2),multiply(X_2,Z_150)) = Z_150 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13098]) ).
tff(c_13295,plain,
multiply(inverse(sk_c8),sk_c8) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_13280,c_13110]) ).
tff(c_13301,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13295]) ).
tff(c_13303,plain,
multiply(sk_c8,identity) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_13301,c_13280]) ).
tff(c_13089,plain,
! [Z_150] : ( multiply(sk_c8,multiply(sk_c7,Z_150)) = multiply(sk_c6,Z_150) ),
inference(superposition,[status(thm),theory(equality)],[c_115,c_13053]) ).
tff(c_13377,plain,
! [Z_156] : ( multiply(sk_c8,multiply(sk_c6,Z_156)) = multiply(sk_c6,Z_156) ),
inference(demodulation,[status(thm),theory(equality)],[c_13164,c_13089]) ).
tff(c_13392,plain,
multiply(sk_c8,identity) = multiply(sk_c6,sk_c2),
inference(superposition,[status(thm),theory(equality)],[c_13176,c_13377]) ).
tff(c_13399,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13176,c_13303,c_13392]) ).
tff(c_13410,plain,
inverse(sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_13399,c_98]) ).
tff(c_13436,plain,
multiply(identity,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13410,c_4]) ).
tff(c_13518,plain,
multiply(inverse(identity),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_13436,c_13110]) ).
tff(c_13530,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_13518]) ).
tff(c_26,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c1,sk_c8) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_13034,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_12991,c_26]) ).
tff(c_13169,plain,
multiply(sk_c8,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13164,c_13034]) ).
tff(c_13486,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13399,c_13301,c_13169]) ).
tff(c_13174,plain,
multiply(sk_c1,sk_c8) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13164,c_12991]) ).
tff(c_13441,plain,
multiply(sk_c1,identity) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13399,c_13174]) ).
tff(c_13489,plain,
multiply(sk_c1,identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_13486,c_13441]) ).
tff(c_13623,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13530,c_13489]) ).
tff(c_13625,plain,
multiply(sk_c8,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_13768,plain,
sk_c8 != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13764,c_13625]) ).
tff(c_8,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_13674,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_13625,c_8]) ).
tff(c_10,plain,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_13681,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_13625,c_10]) ).
tff(c_13624,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_13629,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_13624,c_4]) ).
tff(c_13729,plain,
! [Z_160] : ( multiply(sk_c7,multiply(sk_c3,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_13629,c_13693]) ).
tff(c_13801,plain,
! [Z_163] : ( multiply(sk_c7,multiply(sk_c3,Z_163)) = Z_163 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13729]) ).
tff(c_13813,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13681,c_13801]) ).
tff(c_13817,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13674,c_13813]) ).
tff(c_14,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_13662,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_13625,c_14]) ).
tff(c_13858,plain,
multiply(sk_c8,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13817,c_13662]) ).
tff(c_18,plain,
( ( inverse(sk_c4) = sk_c8 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_13647,plain,
inverse(sk_c4) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_13625,c_18]) ).
tff(c_16,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( multiply(sk_c8,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_13688,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_13625,c_16]) ).
tff(c_13738,plain,
! [X_2,Z_160] : ( multiply(inverse(X_2),multiply(X_2,Z_160)) = multiply(identity,Z_160) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_13693]) ).
tff(c_13896,plain,
! [X_165,Z_166] : ( multiply(inverse(X_165),multiply(X_165,Z_166)) = Z_166 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_13738]) ).
tff(c_13932,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_13688,c_13896]) ).
tff(c_13955,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13858,c_13647,c_13932]) ).
tff(c_13957,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_13768,c_13955]) ).
tff(c_13959,plain,
multiply(sk_c1,sk_c8) != sk_c7,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_13991,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_13959,c_20]) ).
tff(c_13996,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_13959,c_22]) ).
tff(c_14016,plain,
! [X_167,Y_168,Z_169] : ( multiply(multiply(X_167,Y_168),Z_169) = multiply(X_167,multiply(Y_168,Z_169)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14049,plain,
! [Z_169] : ( multiply(sk_c7,multiply(sk_c3,Z_169)) = multiply(identity,Z_169) ),
inference(superposition,[status(thm),theory(equality)],[c_13629,c_14016]) ).
tff(c_14108,plain,
! [Z_172] : ( multiply(sk_c7,multiply(sk_c3,Z_172)) = Z_172 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14049]) ).
tff(c_14120,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_13996,c_14108]) ).
tff(c_14124,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_13991,c_14120]) ).
tff(c_14130,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14124,c_13991]) ).
tff(c_14058,plain,
! [X_2,Z_169] : ( multiply(inverse(X_2),multiply(X_2,Z_169)) = multiply(identity,Z_169) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14016]) ).
tff(c_14189,plain,
! [X_173,Z_174] : ( multiply(inverse(X_173),multiply(X_173,Z_174)) = Z_174 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14058]) ).
tff(c_14213,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_14130,c_14189]) ).
tff(c_14253,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_14213]) ).
tff(c_14003,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_13959,c_26]) ).
tff(c_14128,plain,
multiply(sk_c8,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14124,c_14003]) ).
tff(c_13958,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_13985,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_13959,c_28]) ).
tff(c_14231,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_13985,c_14189]) ).
tff(c_14254,plain,
sk_c8 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14128,c_13958,c_14231]) ).
tff(c_14269,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14253,c_14254]) ).
tff(c_14263,plain,
multiply(sk_c6,sk_c1) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_14254,c_102]) ).
tff(c_14400,plain,
sk_c1 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14269,c_14263]) ).
tff(c_14132,plain,
multiply(sk_c1,sk_c8) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14124,c_13959]) ).
tff(c_14409,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14400,c_14269,c_14253,c_14132]) ).
tff(c_14411,plain,
inverse(sk_c1) != sk_c8,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_38,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_14440,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14411,c_38]) ).
tff(c_40,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_14455,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_14411,c_40]) ).
tff(c_14410,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_14415,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14410,c_4]) ).
tff(c_14507,plain,
! [Z_177] : ( multiply(sk_c8,multiply(sk_c4,Z_177)) = multiply(identity,Z_177) ),
inference(superposition,[status(thm),theory(equality)],[c_14415,c_14477]) ).
tff(c_14820,plain,
! [Z_185] : ( multiply(sk_c8,multiply(sk_c4,Z_185)) = Z_185 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14507]) ).
tff(c_14832,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_14455,c_14820]) ).
tff(c_14836,plain,
sk_c8 = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14440,c_14832]) ).
tff(c_32,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_14435,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_14411,c_32]) ).
tff(c_34,plain,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_14446,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_14411,c_34]) ).
tff(c_36,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c8 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_14419,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_14411,c_36]) ).
tff(c_14423,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14419,c_4]) ).
tff(c_14504,plain,
! [Z_177] : ( multiply(sk_c7,multiply(sk_c3,Z_177)) = multiply(identity,Z_177) ),
inference(superposition,[status(thm),theory(equality)],[c_14423,c_14477]) ).
tff(c_14542,plain,
! [Z_179] : ( multiply(sk_c7,multiply(sk_c3,Z_179)) = Z_179 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14504]) ).
tff(c_14554,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14446,c_14542]) ).
tff(c_14558,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14435,c_14554]) ).
tff(c_14564,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14558,c_14435]) ).
tff(c_14662,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_14564,c_14524]) ).
tff(c_14668,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_14662]) ).
tff(c_14527,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_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( multiply(sk_c8,sk_c7) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14435,c_68]) ).
tff(c_14528,plain,
multiply(sk_c8,sk_c7) != sk_c6,
inference(splitLeft,[status(thm)],[c_14527]) ).
tff(c_14561,plain,
multiply(sk_c8,sk_c6) != sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14558,c_14528]) ).
tff(c_14784,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14668,c_14561]) ).
tff(c_14786,plain,
multiply(sk_c8,sk_c7) = sk_c6,
inference(splitRight,[status(thm)],[c_14527]) ).
tff(c_14839,plain,
multiply(sk_c7,sk_c7) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14836,c_14786]) ).
tff(c_14841,plain,
multiply(sk_c3,sk_c7) = sk_c7,
inference(demodulation,[status(thm),theory(equality)],[c_14836,c_14446]) ).
tff(c_16424,plain,
multiply(inverse(sk_c3),sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14841,c_14524]) ).
tff(c_16430,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14839,c_14419,c_16424]) ).
tff(c_16435,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16430,c_16430,c_14839]) ).
tff(c_16556,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_16435,c_14524]) ).
tff(c_16563,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_16556]) ).
tff(c_16576,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16563,c_16430]) ).
tff(c_14937,plain,
! [X_187,Z_188] : ( multiply(inverse(X_187),multiply(X_187,Z_188)) = Z_188 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14513]) ).
tff(c_15322,plain,
! [X_192,Z_193] : ( multiply(inverse(inverse(X_192)),Z_193) = multiply(X_192,Z_193) ),
inference(superposition,[status(thm),theory(equality)],[c_14937,c_14524]) ).
tff(c_14958,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_14937]) ).
tff(c_15329,plain,
! [X_192] : ( multiply(X_192,identity) = X_192 ),
inference(superposition,[status(thm),theory(equality)],[c_15322,c_14958]) ).
tff(c_14898,plain,
! [Z_186] : ( multiply(sk_c7,multiply(sk_c3,Z_186)) = Z_186 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14504]) ).
tff(c_14910,plain,
multiply(sk_c7,sk_c7) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_14841,c_14898]) ).
tff(c_14914,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14839,c_14910]) ).
tff(c_14920,plain,
multiply(sk_c6,sk_c6) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14914,c_14914,c_14839]) ).
tff(c_15102,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_14920,c_14524]) ).
tff(c_15109,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_15102]) ).
tff(c_15124,plain,
sk_c7 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15109,c_14914]) ).
tff(c_14785,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_14527]) ).
tff(c_14865,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X5_6) != sk_c7 )
| ( multiply(sk_c7,multiply(X5_6,sk_c7)) != sk_c7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_14836,c_14836,c_14836,c_14836,c_14836,c_14836,c_14785]) ).
tff(c_14866,plain,
! [X5_6] :
( ( inverse(X5_6) != sk_c7 )
| ( multiply(sk_c7,multiply(X5_6,sk_c7)) != sk_c7 ) ),
inference(splitLeft,[status(thm)],[c_14865]) ).
tff(c_16327,plain,
inverse(identity) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_15329,c_15124,c_15124,c_2,c_15124,c_15124,c_14866]) ).
tff(c_14928,plain,
inverse(sk_c2) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_14914,c_85]) ).
tff(c_14971,plain,
multiply(sk_c6,sk_c2) = identity,
inference(superposition,[status(thm),theory(equality)],[c_14928,c_4]) ).
tff(c_15183,plain,
sk_c2 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_15109,c_14971]) ).
tff(c_15122,plain,
inverse(sk_c2) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15109,c_14928]) ).
tff(c_15184,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_15183,c_15122]) ).
tff(c_16329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16327,c_15184]) ).
tff(c_16330,plain,
! [X1_8,X4_10,X3_7] :
( ( inverse(X1_8) != sk_c7 )
| ( multiply(X1_8,sk_c7) != sk_c7 )
| ( inverse(X4_10) != sk_c7 )
| ( multiply(X4_10,sk_c7) != sk_c6 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c7 ) ),
inference(splitRight,[status(thm)],[c_14865]) ).
tff(c_24619,plain,
! [X1_8,X4_10,X3_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_16743,c_16576,c_16576,c_16576,c_16743,c_16576,c_16563,c_16576,c_16743,c_16576,c_16576,c_16576,c_16330]) ).
tff(c_24621,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_24619]) ).
tff(c_16441,plain,
inverse(sk_c3) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_16430,c_14419]) ).
tff(c_16468,plain,
multiply(sk_c6,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_16441,c_4]) ).
tff(c_16612,plain,
sk_c3 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16563,c_16468]) ).
tff(c_16572,plain,
inverse(sk_c3) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16563,c_16441]) ).
tff(c_16613,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_16612,c_16572]) ).
tff(c_24623,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24621,c_16613]) ).
tff(c_24624,plain,
! [X4_10,X1_8] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_24619]) ).
tff(c_24626,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_24624]) ).
tff(c_24628,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24626,c_16613]) ).
tff(c_25027,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_24624]) ).
tff(c_25029,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_25027,c_16613]) ).
tff(c_25031,plain,
inverse(sk_c2) != sk_c7,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_56,plain,
( ( multiply(sk_c7,sk_c8) = sk_c6 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_25057,plain,
multiply(sk_c7,sk_c8) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_25031,c_56]) ).
tff(c_58,plain,
( ( multiply(sk_c3,sk_c7) = sk_c8 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_25078,plain,
multiply(sk_c3,sk_c7) = sk_c8,
inference(negUnitSimplification,[status(thm)],[c_25031,c_58]) ).
tff(c_60,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_25043,plain,
inverse(sk_c3) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_25031,c_60]) ).
tff(c_25047,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25043,c_4]) ).
tff(c_25140,plain,
! [Z_312] : ( multiply(sk_c7,multiply(sk_c3,Z_312)) = multiply(identity,Z_312) ),
inference(superposition,[status(thm),theory(equality)],[c_25047,c_25110]) ).
tff(c_25159,plain,
! [Z_313] : ( multiply(sk_c7,multiply(sk_c3,Z_313)) = Z_313 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25140]) ).
tff(c_25171,plain,
multiply(sk_c7,sk_c8) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_25078,c_25159]) ).
tff(c_25175,plain,
sk_c7 = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_25057,c_25171]) ).
tff(c_25179,plain,
multiply(sk_c6,sk_c8) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_25175,c_25057]) ).
tff(c_25496,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_25179,c_25475]) ).
tff(c_25533,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25496]) ).
tff(c_25030,plain,
inverse(sk_c4) = sk_c8,
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_64,plain,
( ( multiply(sk_c4,sk_c8) = sk_c5 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_25093,plain,
multiply(sk_c4,sk_c8) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_25031,c_64]) ).
tff(c_25511,plain,
multiply(inverse(sk_c4),sk_c5) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_25093,c_25475]) ).
tff(c_25536,plain,
multiply(sk_c8,sk_c5) = sk_c8,
inference(demodulation,[status(thm),theory(equality)],[c_25030,c_25511]) ).
tff(c_25571,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25533,c_2,c_25533,c_25536]) ).
tff(c_62,plain,
( ( multiply(sk_c8,sk_c5) = sk_c7 )
| ( inverse(sk_c2) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_25087,plain,
multiply(sk_c8,sk_c5) = sk_c7,
inference(negUnitSimplification,[status(thm)],[c_25031,c_62]) ).
tff(c_25177,plain,
multiply(sk_c8,sk_c5) = sk_c6,
inference(demodulation,[status(thm),theory(equality)],[c_25175,c_25087]) ).
tff(c_25577,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25571,c_2,c_25533,c_25177]) ).
tff(c_25218,plain,
! [X_314,Z_315] : ( multiply(inverse(X_314),multiply(X_314,Z_315)) = Z_315 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25146]) ).
tff(c_25236,plain,
multiply(inverse(sk_c6),sk_c6) = sk_c8,
inference(superposition,[status(thm),theory(equality)],[c_25179,c_25218]) ).
tff(c_25273,plain,
sk_c8 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25236]) ).
tff(c_25187,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_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( multiply(sk_c6,sk_c8) != sk_c6 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c6 )
| ( multiply(sk_c8,sk_c6) != sk_c6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25175,c_25175,c_25175,c_25175,c_25175,c_25175,c_25175,c_25175,c_68]) ).
tff(c_25188,plain,
multiply(sk_c8,sk_c6) != sk_c6,
inference(splitLeft,[status(thm)],[c_25187]) ).
tff(c_25421,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_25273,c_25188]) ).
tff(c_25422,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( multiply(sk_c6,sk_c8) != sk_c6 )
| ( inverse(X3_7) != sk_c8 )
| ( multiply(X3_7,sk_c8) != sk_c6 )
| ( inverse(X4_10) != sk_c6 )
| ( multiply(X4_10,sk_c6) != sk_c6 )
| ( inverse(X1_8) != sk_c6 )
| ( multiply(X1_8,sk_c6) != sk_c8 )
| ( inverse(X5_6) != sk_c8 )
| ( multiply(sk_c8,multiply(X5_6,sk_c8)) != sk_c6 ) ),
inference(splitRight,[status(thm)],[c_25187]) ).
tff(c_32437,plain,
! [X3_7,X4_10,X1_8,X5_6] :
( ( inverse(X3_7) != identity )
| ( identity != X3_7 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X5_6) != identity )
| ( identity != X5_6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_25761,c_25577,c_25533,c_2,c_25533,c_25533,c_25761,c_25577,c_25533,c_25577,c_25761,c_25577,c_25577,c_25577,c_25761,c_25577,c_25533,c_25533,c_25577,c_2,c_25577,c_25533,c_25422]) ).
tff(c_32439,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_32437]) ).
tff(c_25035,plain,
multiply(sk_c8,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_25030,c_4]) ).
tff(c_25543,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25533,c_25035]) ).
tff(c_25604,plain,
multiply(inverse(identity),identity) = sk_c4,
inference(superposition,[status(thm),theory(equality)],[c_25543,c_25157]) ).
tff(c_25616,plain,
sk_c4 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_25604]) ).
tff(c_25544,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25533,c_25030]) ).
tff(c_25620,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_25616,c_25544]) ).
tff(c_32441,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_32439,c_25620]) ).
tff(c_32442,plain,
! [X1_8,X4_10,X3_7] :
( ( inverse(X1_8) != identity )
| ( identity != X1_8 )
| ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X3_7) != identity )
| ( identity != X3_7 ) ),
inference(splitRight,[status(thm)],[c_32437]) ).
tff(c_35109,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_32442]) ).
tff(c_35111,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35109,c_25620]) ).
tff(c_35112,plain,
! [X4_10,X1_8] :
( ( inverse(X4_10) != identity )
| ( identity != X4_10 )
| ( inverse(X1_8) != identity )
| ( identity != X1_8 ) ),
inference(splitRight,[status(thm)],[c_32442]) ).
tff(c_35114,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_35112]) ).
tff(c_35116,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35114,c_25620]) ).
tff(c_35466,plain,
inverse(identity) != identity,
inference(splitRight,[status(thm)],[c_35112]) ).
tff(c_35468,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_35466,c_25620]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GRP286-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.35 % Computer : n007.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Mon Apr 7 21:40:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 14.22/4.64 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.35/4.66
% 14.35/4.66 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------