%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP214-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : 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:34 PM UTC 2025
% Result : Unsatisfiable 14.14s 4.91s
% Output : CNFRefutation 14.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 16
% Syntax : Number of formulae : 183 ( 137 unt; 0 typ; 0 def)
% Number of atoms : 252 ( 241 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 152 ( 83 ~; 69 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 114 ( 114 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > sk_c7 > sk_c6 > sk_c5 > sk_c4 > sk_c3 > sk_c2 > sk_c1 > identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sk_c4,type,
sk_c4: $i ).
tff(sk_c7,type,
sk_c7: $i ).
tff(sk_c5,type,
sk_c5: $i ).
tff(sk_c2,type,
sk_c2: $i ).
tff(sk_c3,type,
sk_c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(sk_c6,type,
sk_c6: $i ).
tff(sk_c1,type,
sk_c1: $i ).
tff(identity,type,
identity: $i ).
tff(f_57,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_80,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_119,axiom,
! [X5,X3,X1,X2,X4] :
( ( multiply(X3,sk_c7) != sk_c6 )
| ( inverse(X3) != sk_c7 )
| ( multiply(sk_c7,X4) != sk_c6 )
| ( multiply(X2,sk_c7) != X1 )
| ( inverse(X2) != sk_c7 )
| ( multiply(X5,X1) != sk_c6 )
| ( inverse(X5) != X1 ) ),
file(unknown,unknown) ).
tff(f_92,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( inverse(sk_c3) = sk_c7 ) ),
file(unknown,unknown) ).
tff(f_89,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_98,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_95,axiom,
( ( multiply(sk_c7,sk_c2) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_71,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_74,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_65,axiom,
( ( multiply(sk_c1,sk_c7) = sk_c6 )
| ( multiply(sk_c3,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c3,sk_c7) = sk_c5 ) ),
file(unknown,unknown) ).
tff(f_83,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( multiply(sk_c4,sk_c5) = sk_c6 ) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( ( inverse(sk_c1) = sk_c7 )
| ( inverse(sk_c4) = sk_c5 ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_18,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_49,plain,
inverse(sk_c1) = sk_c7,
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_53,plain,
multiply(sk_c7,sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_49,c_4]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_80,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_104,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_80]) ).
tff(c_184,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_104]) ).
tff(c_217,plain,
multiply(inverse(sk_c7),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_53,c_184]) ).
tff(c_113,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_104]) ).
tff(c_318,plain,
multiply(inverse(inverse(sk_c7)),sk_c1) = identity,
inference(superposition,[status(thm),theory(equality)],[c_217,c_113]) ).
tff(c_444,plain,
multiply(inverse(inverse(inverse(sk_c7))),identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_318,c_113]) ).
tff(c_223,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_184]) ).
tff(c_587,plain,
inverse(sk_c7) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_444,c_223]) ).
tff(c_349,plain,
! [X_24] : ( multiply(inverse(inverse(X_24)),identity) = X_24 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_184]) ).
tff(c_355,plain,
! [X_24] : ( multiply(inverse(inverse(inverse(X_24))),X_24) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_349,c_113]) ).
tff(c_252,plain,
! [X_21] : ( multiply(inverse(identity),X_21) = X_21 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_184]) ).
tff(c_369,plain,
! [X_25] : ( multiply(inverse(inverse(identity)),X_25) = X_25 ),
inference(superposition,[status(thm),theory(equality)],[c_252,c_113]) ).
tff(c_393,plain,
inverse(identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_369,c_4]) ).
tff(c_10,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_62,plain,
multiply(sk_c1,sk_c7) = sk_c6,
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_101,plain,
! [Z_15] : ( multiply(sk_c7,multiply(sk_c1,Z_15)) = multiply(identity,Z_15) ),
inference(superposition,[status(thm),theory(equality)],[c_53,c_80]) ).
tff(c_160,plain,
! [Z_18] : ( multiply(sk_c7,multiply(sk_c1,Z_18)) = Z_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_101]) ).
tff(c_172,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_62,c_160]) ).
tff(c_202,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_172,c_184]) ).
tff(c_230,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_202]) ).
tff(c_32,plain,
! [X5_6,X2_9,X4_10,X3_7] :
( ( multiply(X5_6,inverse(X5_6)) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) )
| ( multiply(sk_c7,X4_10) != sk_c6 )
| ( inverse(X3_7) != sk_c7 )
| ( multiply(X3_7,sk_c7) != sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_139,plain,
! [X3_17] :
( ( inverse(X3_17) != sk_c7 )
| ( multiply(X3_17,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_146,plain,
inverse(sk_c1) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_62,c_139]) ).
tff(c_158,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49,c_146]) ).
tff(c_159,plain,
! [X4_10,X5_6,X2_9] :
( ( multiply(sk_c7,X4_10) != sk_c6 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) ) ),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_183,plain,
! [X5_6,X2_9] :
( ( multiply(X5_6,inverse(X5_6)) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) ) ),
inference(splitLeft,[status(thm)],[c_159]) ).
tff(c_334,plain,
! [X5_6,X2_9] :
( ( multiply(X5_6,inverse(X5_6)) != identity )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_230,c_183]) ).
tff(c_425,plain,
! [X2_9] :
( ( multiply(identity,identity) != identity )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(identity) ) ),
inference(superposition,[status(thm),theory(equality)],[c_393,c_334]) ).
tff(c_633,plain,
! [X2_29] :
( ( inverse(X2_29) != sk_c7 )
| ( multiply(X2_29,sk_c7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_393,c_2,c_425]) ).
tff(c_637,plain,
inverse(inverse(inverse(inverse(sk_c7)))) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_355,c_633]) ).
tff(c_656,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49,c_587,c_49,c_587,c_637]) ).
tff(c_657,plain,
! [X4_10] : ( multiply(sk_c7,X4_10) != sk_c6 ),
inference(splitRight,[status(thm)],[c_159]) ).
tff(c_26,plain,
( ( inverse(sk_c3) = sk_c7 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_68,plain,
multiply(sk_c7,sk_c2) = sk_c6,
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_659,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_657,c_68]) ).
tff(c_660,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_665,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_660,c_4]) ).
tff(c_661,plain,
multiply(sk_c7,sk_c2) != sk_c6,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_24,plain,
( ( multiply(sk_c3,sk_c7) = sk_c5 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_687,plain,
multiply(sk_c3,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_661,c_24]) ).
tff(c_699,plain,
! [X_30,Y_31,Z_32] : ( multiply(multiply(X_30,Y_31),Z_32) = multiply(X_30,multiply(Y_31,Z_32)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_723,plain,
! [Z_32] : ( multiply(sk_c7,multiply(sk_c3,Z_32)) = multiply(identity,Z_32) ),
inference(superposition,[status(thm),theory(equality)],[c_665,c_699]) ).
tff(c_842,plain,
! [Z_37] : ( multiply(sk_c7,multiply(sk_c3,Z_37)) = Z_37 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_723]) ).
tff(c_854,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_687,c_842]) ).
tff(c_732,plain,
! [X_2,Z_32] : ( multiply(inverse(X_2),multiply(X_2,Z_32)) = multiply(identity,Z_32) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_699]) ).
tff(c_972,plain,
! [X_42,Z_43] : ( multiply(inverse(X_42),multiply(X_42,Z_43)) = Z_43 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_732]) ).
tff(c_1011,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_854,c_972]) ).
tff(c_1064,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1011]) ).
tff(c_1093,plain,
multiply(sk_c3,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1064,c_687]) ).
tff(c_30,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_675,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_661,c_30]) ).
tff(c_28,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c7,sk_c2) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_693,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_661,c_28]) ).
tff(c_815,plain,
! [X3_36] :
( ( inverse(X3_36) != sk_c7 )
| ( multiply(X3_36,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_825,plain,
inverse(sk_c1) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_62,c_815]) ).
tff(c_839,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49,c_825]) ).
tff(c_840,plain,
! [X4_10,X5_6,X2_9] :
( ( multiply(sk_c7,X4_10) != sk_c6 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) ) ),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_954,plain,
! [X5_40,X2_41] :
( ( multiply(X5_40,inverse(X5_40)) != sk_c6 )
| ( inverse(X2_41) != sk_c7 )
| ( multiply(X2_41,sk_c7) != inverse(X5_40) ) ),
inference(splitLeft,[status(thm)],[c_840]) ).
tff(c_959,plain,
! [X2_41] :
( ( multiply(sk_c4,sk_c5) != sk_c6 )
| ( inverse(X2_41) != sk_c7 )
| ( multiply(X2_41,sk_c7) != inverse(sk_c4) ) ),
inference(superposition,[status(thm),theory(equality)],[c_675,c_954]) ).
tff(c_968,plain,
! [X2_41] :
( ( inverse(X2_41) != sk_c7 )
| ( multiply(X2_41,sk_c7) != sk_c5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_675,c_693,c_959]) ).
tff(c_1167,plain,
! [X2_41] :
( ( inverse(X2_41) != sk_c7 )
| ( multiply(X2_41,sk_c7) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1064,c_968]) ).
tff(c_1213,plain,
inverse(sk_c3) != sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_1093,c_1167]) ).
tff(c_1228,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_660,c_1213]) ).
tff(c_1230,plain,
! [X4_46] : ( multiply(sk_c7,X4_46) != sk_c6 ),
inference(splitRight,[status(thm)],[c_840]) ).
tff(c_1236,plain,
sk_c6 != identity,
inference(superposition,[status(thm),theory(equality)],[c_665,c_1230]) ).
tff(c_729,plain,
! [Z_32] : ( multiply(sk_c7,multiply(sk_c1,Z_32)) = multiply(identity,Z_32) ),
inference(superposition,[status(thm),theory(equality)],[c_53,c_699]) ).
tff(c_745,plain,
! [Z_33] : ( multiply(sk_c7,multiply(sk_c1,Z_33)) = Z_33 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_729]) ).
tff(c_757,plain,
multiply(sk_c7,sk_c6) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_62,c_745]) ).
tff(c_1239,plain,
! [X_47,Z_48] : ( multiply(inverse(X_47),multiply(X_47,Z_48)) = Z_48 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_732]) ).
tff(c_1257,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_757,c_1239]) ).
tff(c_1300,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1257]) ).
tff(c_1302,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1236,c_1300]) ).
tff(c_1304,plain,
multiply(sk_c1,sk_c7) != sk_c6,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_12,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_1337,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_1304,c_12]) ).
tff(c_14,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_1318,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_1304,c_14]) ).
tff(c_1322,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1318,c_4]) ).
tff(c_1344,plain,
! [X_49,Y_50,Z_51] : ( multiply(multiply(X_49,Y_50),Z_51) = multiply(X_49,multiply(Y_50,Z_51)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_1365,plain,
! [Z_51] : ( multiply(sk_c5,multiply(sk_c4,Z_51)) = multiply(identity,Z_51) ),
inference(superposition,[status(thm),theory(equality)],[c_1322,c_1344]) ).
tff(c_1387,plain,
! [Z_52] : ( multiply(sk_c5,multiply(sk_c4,Z_52)) = Z_52 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1365]) ).
tff(c_1399,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_1337,c_1387]) ).
tff(c_1374,plain,
! [X_2,Z_51] : ( multiply(inverse(X_2),multiply(X_2,Z_51)) = multiply(identity,Z_51) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1344]) ).
tff(c_1643,plain,
! [X_60,Z_61] : ( multiply(inverse(X_60),multiply(X_60,Z_61)) = Z_61 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1374]) ).
tff(c_1670,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_1399,c_1643]) ).
tff(c_1711,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1670]) ).
tff(c_1728,plain,
multiply(sk_c1,sk_c7) != identity,
inference(demodulation,[status(thm),theory(equality)],[c_1711,c_1304]) ).
tff(c_8,plain,
( ( multiply(sk_c3,sk_c7) = sk_c5 )
| ( multiply(sk_c1,sk_c7) = sk_c6 ) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_1332,plain,
multiply(sk_c3,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_1304,c_8]) ).
tff(c_1303,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_1308,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1303,c_4]) ).
tff(c_1368,plain,
! [Z_51] : ( multiply(sk_c7,multiply(sk_c3,Z_51)) = multiply(identity,Z_51) ),
inference(superposition,[status(thm),theory(equality)],[c_1308,c_1344]) ).
tff(c_1423,plain,
! [Z_54] : ( multiply(sk_c7,multiply(sk_c3,Z_54)) = Z_54 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1368]) ).
tff(c_1435,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_1332,c_1423]) ).
tff(c_1661,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_1435,c_1643]) ).
tff(c_1710,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1661]) ).
tff(c_1362,plain,
! [Z_51] : ( multiply(sk_c3,multiply(sk_c7,Z_51)) = multiply(sk_c5,Z_51) ),
inference(superposition,[status(thm),theory(equality)],[c_1332,c_1344]) ).
tff(c_1893,plain,
! [Z_65] : ( multiply(sk_c3,multiply(sk_c7,Z_65)) = Z_65 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1710,c_1362]) ).
tff(c_1923,plain,
multiply(sk_c3,identity) = sk_c1,
inference(superposition,[status(thm),theory(equality)],[c_53,c_1893]) ).
tff(c_1920,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm),theory(equality)],[c_1308,c_1893]) ).
tff(c_1948,plain,
sk_c3 = sk_c1,
inference(demodulation,[status(thm),theory(equality)],[c_1923,c_1920]) ).
tff(c_1721,plain,
multiply(sk_c3,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1710,c_1332]) ).
tff(c_1993,plain,
multiply(sk_c1,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1948,c_1721]) ).
tff(c_1998,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1728,c_1993]) ).
tff(c_1999,plain,
inverse(sk_c3) = sk_c7,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_2000,plain,
inverse(sk_c1) != sk_c7,
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_16,plain,
( ( multiply(sk_c3,sk_c7) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_2026,plain,
multiply(sk_c3,sk_c7) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_2000,c_16]) ).
tff(c_2004,plain,
multiply(sk_c7,sk_c3) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1999,c_4]) ).
tff(c_2042,plain,
! [X_67,Y_68,Z_69] : ( multiply(multiply(X_67,Y_68),Z_69) = multiply(X_67,multiply(Y_68,Z_69)) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_2066,plain,
! [Z_69] : ( multiply(sk_c7,multiply(sk_c3,Z_69)) = multiply(identity,Z_69) ),
inference(superposition,[status(thm),theory(equality)],[c_2004,c_2042]) ).
tff(c_2322,plain,
! [Z_78] : ( multiply(sk_c7,multiply(sk_c3,Z_78)) = Z_78 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2066]) ).
tff(c_2334,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_2026,c_2322]) ).
tff(c_2069,plain,
! [X_2,Z_69] : ( multiply(inverse(X_2),multiply(X_2,Z_69)) = multiply(identity,Z_69) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2042]) ).
tff(c_2345,plain,
! [X_79,Z_80] : ( multiply(inverse(X_79),multiply(X_79,Z_80)) = Z_80 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2069]) ).
tff(c_2363,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_2334,c_2345]) ).
tff(c_2403,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2363]) ).
tff(c_2449,plain,
multiply(sk_c3,sk_c7) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2403,c_2026]) ).
tff(c_2079,plain,
! [X_2,Z_69] : ( multiply(inverse(X_2),multiply(X_2,Z_69)) = Z_69 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2069]) ).
tff(c_2659,plain,
! [X_84,Z_85] : ( multiply(inverse(inverse(X_84)),Z_85) = multiply(X_84,Z_85) ),
inference(superposition,[status(thm),theory(equality)],[c_2345,c_2079]) ).
tff(c_2683,plain,
! [X_84] : ( multiply(X_84,inverse(X_84)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_2659,c_4]) ).
tff(c_20,plain,
( ( multiply(sk_c4,sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_2031,plain,
multiply(sk_c4,sk_c5) = sk_c6,
inference(negUnitSimplification,[status(thm)],[c_2000,c_20]) ).
tff(c_22,plain,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c1) = sk_c7 ) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_2012,plain,
inverse(sk_c4) = sk_c5,
inference(negUnitSimplification,[status(thm)],[c_2000,c_22]) ).
tff(c_2016,plain,
multiply(sk_c5,sk_c4) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2012,c_4]) ).
tff(c_2063,plain,
! [Z_69] : ( multiply(sk_c5,multiply(sk_c4,Z_69)) = multiply(identity,Z_69) ),
inference(superposition,[status(thm),theory(equality)],[c_2016,c_2042]) ).
tff(c_2081,plain,
! [Z_70] : ( multiply(sk_c5,multiply(sk_c4,Z_70)) = Z_70 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2063]) ).
tff(c_2093,plain,
multiply(sk_c5,sk_c6) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_2031,c_2081]) ).
tff(c_2369,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_2093,c_2345]) ).
tff(c_2404,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2369]) ).
tff(c_2128,plain,
! [X3_72] :
( ( inverse(X3_72) != sk_c7 )
| ( multiply(X3_72,sk_c7) != sk_c6 ) ),
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_2139,plain,
( ( inverse(inverse(sk_c7)) != sk_c7 )
| ( sk_c6 != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2128]) ).
tff(c_2147,plain,
sk_c6 != identity,
inference(splitLeft,[status(thm)],[c_2139]) ).
tff(c_2148,plain,
! [X_73,Z_74] : ( multiply(inverse(X_73),multiply(X_73,Z_74)) = Z_74 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2069]) ).
tff(c_2172,plain,
multiply(inverse(sk_c5),sk_c5) = sk_c6,
inference(superposition,[status(thm),theory(equality)],[c_2093,c_2148]) ).
tff(c_2207,plain,
sk_c6 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2172]) ).
tff(c_2209,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2147,c_2207]) ).
tff(c_2211,plain,
sk_c6 = identity,
inference(splitRight,[status(thm)],[c_2139]) ).
tff(c_2135,plain,
( ( inverse(sk_c3) != sk_c7 )
| ( sk_c6 != sk_c5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2026,c_2128]) ).
tff(c_2145,plain,
sk_c6 != sk_c5,
inference(demodulation,[status(thm),theory(equality)],[c_1999,c_2135]) ).
tff(c_2239,plain,
sk_c5 != identity,
inference(demodulation,[status(thm),theory(equality)],[c_2211,c_2145]) ).
tff(c_2105,plain,
! [Z_71] : ( multiply(sk_c7,multiply(sk_c3,Z_71)) = Z_71 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2066]) ).
tff(c_2117,plain,
multiply(sk_c7,sk_c5) = sk_c7,
inference(superposition,[status(thm),theory(equality)],[c_2026,c_2105]) ).
tff(c_2258,plain,
! [X_76,Z_77] : ( multiply(inverse(X_76),multiply(X_76,Z_77)) = Z_77 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_2069]) ).
tff(c_2282,plain,
multiply(inverse(sk_c7),sk_c7) = sk_c5,
inference(superposition,[status(thm),theory(equality)],[c_2117,c_2258]) ).
tff(c_2318,plain,
sk_c5 = identity,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2282]) ).
tff(c_2320,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2239,c_2318]) ).
tff(c_2321,plain,
! [X4_10,X5_6,X2_9] :
( ( multiply(sk_c7,X4_10) != sk_c6 )
| ( multiply(X5_6,inverse(X5_6)) != sk_c6 )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) ) ),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_2484,plain,
! [X4_10,X5_6,X2_9] :
( ( multiply(sk_c7,X4_10) != identity )
| ( multiply(X5_6,inverse(X5_6)) != identity )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2404,c_2404,c_2321]) ).
tff(c_2485,plain,
! [X5_6,X2_9] :
( ( multiply(X5_6,inverse(X5_6)) != identity )
| ( inverse(X2_9) != sk_c7 )
| ( multiply(X2_9,sk_c7) != inverse(X5_6) ) ),
inference(splitLeft,[status(thm)],[c_2484]) ).
tff(c_30264,plain,
! [X2_236,X5_237] :
( ( inverse(X2_236) != sk_c7 )
| ( multiply(X2_236,sk_c7) != inverse(X5_237) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_2683,c_2485]) ).
tff(c_30338,plain,
! [X5_237] :
( ( inverse(sk_c3) != sk_c7 )
| ( inverse(X5_237) != identity ) ),
inference(superposition,[status(thm),theory(equality)],[c_2449,c_30264]) ).
tff(c_30365,plain,
! [X5_237] : ( inverse(X5_237) != identity ),
inference(demodulation,[status(thm),theory(equality)],[c_1999,c_30338]) ).
tff(c_2450,plain,
multiply(identity,sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2403,c_2016]) ).
tff(c_2523,plain,
sk_c4 = identity,
inference(superposition,[status(thm),theory(equality)],[c_2450,c_2]) ).
tff(c_2451,plain,
inverse(sk_c4) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2403,c_2012]) ).
tff(c_2534,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_2523,c_2451]) ).
tff(c_30370,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_30365,c_2534]) ).
tff(c_30371,plain,
! [X4_10] : ( multiply(sk_c7,X4_10) != identity ),
inference(splitRight,[status(thm)],[c_2484]) ).
tff(c_30478,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_30371,c_2004]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP214-1 : TPTP v9.0.0. Released v2.5.0.
% 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.35 % Computer : n007.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Mon Apr 7 21:37:08 EDT 2025
% 0.14/0.35 % CPUTime :
% 14.14/4.91 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.38/4.93
% 14.38/4.93 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------