%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP103-1 : TPTP v9.0.0. Bugfixed v2.7.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 : n013.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:00 PM UTC 2025
% Result : Unsatisfiable 32.26s 19.20s
% Output : CNFRefutation 32.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 5
% Syntax : Number of formulae : 136 ( 131 unt; 0 typ; 0 def)
% Number of atoms : 148 ( 145 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 34 ( 22 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 9 ( 2 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; 8 con; 0-2 aty)
% Number of variables : 235 ( 235 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > double_divide > #nlpp > inverse > identity > c3 > b4 > b3 > a4 > a3 > a2 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(a3,type,
a3: $i ).
tff(c3,type,
c3: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(double_divide,type,
double_divide: ( $i * $i ) > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b4,type,
b4: $i ).
tff(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(a4,type,
a4: $i ).
tff(identity,type,
identity: $i ).
tff(f_30,axiom,
! [X,Y] : ( multiply(X,Y) = double_divide(double_divide(Y,X),identity) ),
file(unknown,unknown) ).
tff(f_33,axiom,
! [X] : ( inverse(X) = double_divide(X,identity) ),
file(unknown,unknown) ).
tff(f_36,axiom,
! [X] : ( identity = double_divide(X,inverse(X)) ),
file(unknown,unknown) ).
tff(f_47,axiom,
( ( multiply(inverse(a1),a1) != identity )
| ( multiply(identity,a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(a4,b4) != multiply(b4,a4) ) ),
file(unknown,unknown) ).
tff(f_27,axiom,
! [X,Y,Z] : ( double_divide(double_divide(X,double_divide(double_divide(identity,Y),double_divide(Z,double_divide(Y,X)))),double_divide(identity,identity)) = Z ),
file(unknown,unknown) ).
tff(c_28,plain,
! [Y_10,X_11] : ( double_divide(double_divide(Y_10,X_11),identity) = multiply(X_11,Y_10) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_6,plain,
! [X_6] : ( double_divide(X_6,identity) = inverse(X_6) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_37,plain,
! [Y_10,X_11] : ( inverse(double_divide(Y_10,X_11)) = multiply(X_11,Y_10) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_6]) ).
tff(c_8,plain,
! [X_7] : ( double_divide(X_7,inverse(X_7)) = identity ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_4,plain,
! [Y_5,X_4] : ( double_divide(double_divide(Y_5,X_4),identity) = multiply(X_4,Y_5) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_52,plain,
! [X_7] : ( multiply(inverse(X_7),X_7) = double_divide(identity,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_28]) ).
tff(c_57,plain,
! [X_7] : ( multiply(inverse(X_7),X_7) = inverse(identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_52]) ).
tff(c_10,plain,
( ( multiply(b4,a4) != multiply(a4,b4) )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(identity,a2) != a2 )
| ( multiply(inverse(a1),a1) != identity ) ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_190,plain,
( ( multiply(b4,a4) != multiply(a4,b4) )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(identity,a2) != a2 )
| ( inverse(identity) != identity ) ),
inference(demodulation,[status(thm),theory(equality)],[c_57,c_10]) ).
tff(c_191,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_190]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3] : ( double_divide(double_divide(X_1,double_divide(double_divide(identity,Y_2),double_divide(Z_3,double_divide(Y_2,X_1)))),double_divide(identity,identity)) = Z_3 ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_90,plain,
! [X_15,Y_16,Z_17] : ( double_divide(double_divide(X_15,double_divide(double_divide(identity,Y_16),double_divide(Z_17,double_divide(Y_16,X_15)))),inverse(identity)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_2]) ).
tff(c_552,plain,
! [X_33,Z_34] : ( double_divide(double_divide(identity,double_divide(double_divide(identity,X_33),double_divide(Z_34,inverse(X_33)))),inverse(identity)) = Z_34 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_90]) ).
tff(c_611,plain,
! [X_7] : ( double_divide(double_divide(identity,double_divide(double_divide(identity,X_7),identity)),inverse(identity)) = X_7 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_552]) ).
tff(c_623,plain,
! [X_35] : ( double_divide(double_divide(identity,multiply(X_35,identity)),inverse(identity)) = X_35 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_6,c_611]) ).
tff(c_657,plain,
double_divide(double_divide(identity,inverse(identity)),inverse(identity)) = inverse(identity),
inference(superposition,[status(thm),theory(equality)],[c_57,c_623]) ).
tff(c_662,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_8,c_657]) ).
tff(c_664,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_191,c_662]) ).
tff(c_666,plain,
inverse(identity) = identity,
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_125,plain,
! [X_7,Z_17] : ( double_divide(double_divide(inverse(X_7),double_divide(double_divide(identity,X_7),double_divide(Z_17,identity))),inverse(identity)) = Z_17 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_90]) ).
tff(c_129,plain,
! [X_7,Z_17] : ( double_divide(double_divide(inverse(X_7),double_divide(double_divide(identity,X_7),inverse(Z_17))),inverse(identity)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_125]) ).
tff(c_998,plain,
! [X_46,Z_47] : ( multiply(double_divide(double_divide(identity,X_46),inverse(Z_47)),inverse(X_46)) = Z_47 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_666,c_129]) ).
tff(c_1043,plain,
! [X_46] : ( multiply(identity,inverse(X_46)) = double_divide(identity,X_46) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_998]) ).
tff(c_155,plain,
! [X_19] : ( double_divide(inverse(X_19),identity) = multiply(identity,X_19) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_28]) ).
tff(c_164,plain,
! [X_19] : ( multiply(identity,inverse(X_19)) = inverse(multiply(identity,X_19)) ),
inference(superposition,[status(thm),theory(equality)],[c_155,c_37]) ).
tff(c_1163,plain,
! [X_51] : ( inverse(multiply(identity,X_51)) = double_divide(identity,X_51) ),
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_164]) ).
tff(c_1205,plain,
! [X_46] : ( double_divide(identity,inverse(X_46)) = inverse(double_divide(identity,X_46)) ),
inference(superposition,[status(thm),theory(equality)],[c_1043,c_1163]) ).
tff(c_1217,plain,
! [X_46] : ( double_divide(identity,inverse(X_46)) = multiply(X_46,identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1205]) ).
tff(c_1019,plain,
! [Z_47] : ( multiply(double_divide(double_divide(identity,identity),inverse(Z_47)),identity) = Z_47 ),
inference(superposition,[status(thm),theory(equality)],[c_666,c_998]) ).
tff(c_1048,plain,
! [Z_47] : ( multiply(double_divide(identity,inverse(Z_47)),identity) = Z_47 ),
inference(demodulation,[status(thm),theory(equality)],[c_666,c_6,c_1019]) ).
tff(c_1266,plain,
! [Z_47] : ( multiply(multiply(Z_47,identity),identity) = Z_47 ),
inference(demodulation,[status(thm),theory(equality)],[c_1217,c_1048]) ).
tff(c_65,plain,
! [Y_13,X_14] : ( inverse(double_divide(Y_13,X_14)) = multiply(X_14,Y_13) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_6]) ).
tff(c_83,plain,
! [X_6] : ( inverse(inverse(X_6)) = multiply(identity,X_6) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_65]) ).
tff(c_40,plain,
! [Y_5,X_4] : ( multiply(identity,double_divide(Y_5,X_4)) = double_divide(multiply(X_4,Y_5),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_28]) ).
tff(c_55,plain,
! [Y_5,X_4] : ( multiply(identity,double_divide(Y_5,X_4)) = inverse(multiply(X_4,Y_5)) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_40]) ).
tff(c_46,plain,
! [X_6] : ( double_divide(inverse(X_6),identity) = multiply(identity,X_6) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_28]) ).
tff(c_1193,plain,
! [X_51] : ( multiply(identity,multiply(identity,X_51)) = double_divide(double_divide(identity,X_51),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_1163,c_46]) ).
tff(c_1583,plain,
! [X_60] : ( multiply(identity,multiply(identity,X_60)) = multiply(X_60,identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1193]) ).
tff(c_1627,plain,
! [X_46] : ( multiply(inverse(X_46),identity) = multiply(identity,double_divide(identity,X_46)) ),
inference(superposition,[status(thm),theory(equality)],[c_1043,c_1583]) ).
tff(c_1642,plain,
! [X_46] : ( multiply(inverse(X_46),identity) = inverse(multiply(X_46,identity)) ),
inference(demodulation,[status(thm),theory(equality)],[c_55,c_1627]) ).
tff(c_1016,plain,
! [X_46] : ( multiply(double_divide(double_divide(identity,X_46),identity),inverse(X_46)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_666,c_998]) ).
tff(c_1047,plain,
! [X_46] : ( multiply(multiply(X_46,identity),inverse(X_46)) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1016]) ).
tff(c_1051,plain,
! [X_48] : ( multiply(multiply(X_48,identity),inverse(X_48)) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1016]) ).
tff(c_74,plain,
! [Y_13,X_14] : ( double_divide(double_divide(Y_13,X_14),multiply(X_14,Y_13)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_65,c_8]) ).
tff(c_2497,plain,
! [X_76] : ( double_divide(double_divide(inverse(X_76),multiply(X_76,identity)),identity) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_1051,c_74]) ).
tff(c_2598,plain,
! [X_77] : ( inverse(double_divide(inverse(X_77),multiply(X_77,identity))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_2497,c_6]) ).
tff(c_997,plain,
! [X_7,Z_17] : ( multiply(double_divide(double_divide(identity,X_7),inverse(Z_17)),inverse(X_7)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_666,c_129]) ).
tff(c_2624,plain,
! [X_7,X_77] : ( multiply(double_divide(double_divide(identity,X_7),identity),inverse(X_7)) = double_divide(inverse(X_77),multiply(X_77,identity)) ),
inference(superposition,[status(thm),theory(equality)],[c_2598,c_997]) ).
tff(c_2727,plain,
! [X_78] : ( double_divide(inverse(X_78),multiply(X_78,identity)) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_1047,c_4,c_2624]) ).
tff(c_2818,plain,
! [Z_79] : ( double_divide(inverse(multiply(Z_79,identity)),Z_79) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_1266,c_2727]) ).
tff(c_11,plain,
! [X_1,Y_2,Z_3] : ( double_divide(double_divide(X_1,double_divide(double_divide(identity,Y_2),double_divide(Z_3,double_divide(Y_2,X_1)))),inverse(identity)) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_2]) ).
tff(c_1646,plain,
! [X_61,Y_62,Z_63] : ( double_divide(double_divide(X_61,double_divide(double_divide(identity,Y_62),double_divide(Z_63,double_divide(Y_62,X_61)))),identity) = Z_63 ),
inference(demodulation,[status(thm),theory(equality)],[c_666,c_11]) ).
tff(c_1820,plain,
! [Y_65,Z_66,Y_67] : ( multiply(double_divide(double_divide(identity,Y_65),double_divide(Z_66,double_divide(Y_65,Y_67))),Y_67) = Z_66 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1646]) ).
tff(c_1888,plain,
! [X_6,Z_66] : ( multiply(double_divide(double_divide(identity,X_6),double_divide(Z_66,inverse(X_6))),identity) = Z_66 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_1820]) ).
tff(c_2824,plain,
! [X_6] : ( multiply(double_divide(double_divide(identity,X_6),identity),identity) = inverse(multiply(inverse(X_6),identity)) ),
inference(superposition,[status(thm),theory(equality)],[c_2818,c_1888]) ).
tff(c_2932,plain,
! [X_80] : ( multiply(identity,multiply(X_80,identity)) = X_80 ),
inference(demodulation,[status(thm),theory(equality)],[c_83,c_1642,c_1266,c_4,c_2824]) ).
tff(c_1214,plain,
! [X_51] : ( multiply(identity,multiply(identity,X_51)) = multiply(X_51,identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_1193]) ).
tff(c_2944,plain,
! [X_80] : ( multiply(multiply(X_80,identity),identity) = multiply(identity,X_80) ),
inference(superposition,[status(thm),theory(equality)],[c_2932,c_1214]) ).
tff(c_3007,plain,
! [X_80] : ( multiply(identity,X_80) = X_80 ),
inference(demodulation,[status(thm),theory(equality)],[c_1266,c_2944]) ).
tff(c_3032,plain,
! [X_6] : ( double_divide(inverse(X_6),identity) = X_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_46]) ).
tff(c_3195,plain,
! [X_83] : ( inverse(inverse(X_83)) = X_83 ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_83]) ).
tff(c_3216,plain,
! [X_83] : ( double_divide(inverse(X_83),X_83) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_3195,c_8]) ).
tff(c_3027,plain,
! [X_46] : ( double_divide(identity,X_46) = inverse(X_46) ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_1043]) ).
tff(c_1723,plain,
! [X_61,Y_62,Z_63] : ( inverse(double_divide(X_61,double_divide(double_divide(identity,Y_62),double_divide(Z_63,double_divide(Y_62,X_61))))) = Z_63 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_1646]) ).
tff(c_4340,plain,
! [Y_109,Z_110,X_111] : ( multiply(double_divide(inverse(Y_109),double_divide(Z_110,double_divide(Y_109,X_111))),X_111) = Z_110 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3027,c_1723]) ).
tff(c_4394,plain,
! [Y_109,X_111] : ( multiply(double_divide(inverse(Y_109),identity),X_111) = inverse(double_divide(Y_109,X_111)) ),
inference(superposition,[status(thm),theory(equality)],[c_3216,c_4340]) ).
tff(c_4436,plain,
! [Y_109,X_111] : ( multiply(Y_109,X_111) = multiply(X_111,Y_109) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3032,c_4394]) ).
tff(c_3023,plain,
! [X_51] : ( multiply(X_51,identity) = X_51 ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_3007,c_1214]) ).
tff(c_3131,plain,
! [X_46] : ( double_divide(identity,inverse(X_46)) = X_46 ),
inference(demodulation,[status(thm),theory(equality)],[c_3023,c_1217]) ).
tff(c_1667,plain,
! [X_61,Y_62,Z_63] : ( multiply(identity,double_divide(X_61,double_divide(double_divide(identity,Y_62),double_divide(Z_63,double_divide(Y_62,X_61))))) = double_divide(Z_63,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_1646,c_4]) ).
tff(c_1735,plain,
! [X_61,Y_62,Z_63] : ( multiply(identity,double_divide(X_61,double_divide(double_divide(identity,Y_62),double_divide(Z_63,double_divide(Y_62,X_61))))) = inverse(Z_63) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_1667]) ).
tff(c_5382,plain,
! [X_132,Y_133,Z_134] : ( double_divide(X_132,double_divide(inverse(Y_133),double_divide(Z_134,double_divide(Y_133,X_132)))) = inverse(Z_134) ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_3027,c_1735]) ).
tff(c_5474,plain,
! [X_46,Z_134] : ( double_divide(inverse(X_46),double_divide(inverse(identity),double_divide(Z_134,X_46))) = inverse(Z_134) ),
inference(superposition,[status(thm),theory(equality)],[c_3131,c_5382]) ).
tff(c_10471,plain,
! [X_189,Z_190] : ( double_divide(inverse(X_189),multiply(X_189,Z_190)) = inverse(Z_190) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3027,c_666,c_5474]) ).
tff(c_1028,plain,
! [X_46,X_11,Y_10] : ( multiply(double_divide(double_divide(identity,X_46),multiply(X_11,Y_10)),inverse(X_46)) = double_divide(Y_10,X_11) ),
inference(superposition,[status(thm),theory(equality)],[c_37,c_998]) ).
tff(c_4706,plain,
! [X_46,X_11,Y_10] : ( multiply(double_divide(inverse(X_46),multiply(X_11,Y_10)),inverse(X_46)) = double_divide(Y_10,X_11) ),
inference(demodulation,[status(thm),theory(equality)],[c_3027,c_1028]) ).
tff(c_10525,plain,
! [Z_190,X_189] : ( multiply(inverse(Z_190),inverse(X_189)) = double_divide(Z_190,X_189) ),
inference(superposition,[status(thm),theory(equality)],[c_10471,c_4706]) ).
tff(c_4338,plain,
! [Y_62,Z_63,X_61] : ( multiply(double_divide(inverse(Y_62),double_divide(Z_63,double_divide(Y_62,X_61))),X_61) = Z_63 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3027,c_1723]) ).
tff(c_105,plain,
! [X_1,Y_2,Z_3,Z_17] : ( double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X_1,double_divide(double_divide(identity,Y_2),double_divide(Z_3,double_divide(Y_2,X_1))))),double_divide(Z_17,Z_3))),inverse(identity)) = Z_17 ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_90]) ).
tff(c_4088,plain,
! [Y_2,Z_3,X_1,Z_17] : ( double_divide(multiply(double_divide(inverse(Y_2),double_divide(Z_3,double_divide(Y_2,X_1))),X_1),double_divide(Z_17,Z_3)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3032,c_666,c_3027,c_666,c_3027,c_3027,c_105]) ).
tff(c_4339,plain,
! [Z_3,Z_17] : ( double_divide(Z_3,double_divide(Z_17,Z_3)) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_4338,c_4088]) ).
tff(c_4447,plain,
! [Z_112,Z_113] : ( double_divide(Z_112,double_divide(Z_113,Z_112)) = Z_113 ),
inference(demodulation,[status(thm),theory(equality)],[c_4338,c_4088]) ).
tff(c_4478,plain,
! [Z_17,Z_3] : ( double_divide(double_divide(Z_17,Z_3),Z_17) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_4339,c_4447]) ).
tff(c_10528,plain,
! [Z_190,X_189] : ( double_divide(inverse(Z_190),inverse(X_189)) = multiply(X_189,Z_190) ),
inference(superposition,[status(thm),theory(equality)],[c_10471,c_4478]) ).
tff(c_3028,plain,
! [X_4,Y_5] : ( inverse(multiply(X_4,Y_5)) = double_divide(Y_5,X_4) ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_55]) ).
tff(c_115,plain,
! [X_15,Z_17] : ( double_divide(double_divide(X_15,double_divide(inverse(identity),double_divide(Z_17,double_divide(identity,X_15)))),inverse(identity)) = Z_17 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_90]) ).
tff(c_1319,plain,
! [Z_17,X_15] : ( multiply(double_divide(identity,double_divide(Z_17,double_divide(identity,X_15))),X_15) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_666,c_666,c_115]) ).
tff(c_3309,plain,
! [Z_17,X_15] : ( multiply(inverse(double_divide(Z_17,inverse(X_15))),X_15) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_3027,c_3027,c_1319]) ).
tff(c_6300,plain,
! [X_143,Z_144] : ( multiply(multiply(inverse(X_143),Z_144),X_143) = Z_144 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3309]) ).
tff(c_18441,plain,
! [Y_248,X_249,Z_250] : ( multiply(multiply(double_divide(Y_248,X_249),Z_250),multiply(X_249,Y_248)) = Z_250 ),
inference(superposition,[status(thm),theory(equality)],[c_3028,c_6300]) ).
tff(c_18608,plain,
! [X_189,Z_190,Z_250] : ( multiply(multiply(multiply(X_189,Z_190),Z_250),multiply(inverse(X_189),inverse(Z_190))) = Z_250 ),
inference(superposition,[status(thm),theory(equality)],[c_10528,c_18441]) ).
tff(c_18844,plain,
! [X_189,Z_190,Z_250] : ( multiply(double_divide(X_189,Z_190),multiply(multiply(X_189,Z_190),Z_250)) = Z_250 ),
inference(demodulation,[status(thm),theory(equality)],[c_4436,c_10525,c_18608]) ).
tff(c_3033,plain,
! [X_6] : ( inverse(inverse(X_6)) = X_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_83]) ).
tff(c_5492,plain,
! [X_132,Y_133] : ( double_divide(X_132,double_divide(inverse(Y_133),identity)) = inverse(inverse(double_divide(Y_133,X_132))) ),
inference(superposition,[status(thm),theory(equality)],[c_3216,c_5382]) ).
tff(c_5542,plain,
! [Y_133,X_132] : ( double_divide(Y_133,X_132) = double_divide(X_132,Y_133) ),
inference(demodulation,[status(thm),theory(equality)],[c_3033,c_3032,c_5492]) ).
tff(c_10192,plain,
! [X_187,Z_188] : ( double_divide(X_187,multiply(inverse(X_187),Z_188)) = inverse(Z_188) ),
inference(superposition,[status(thm),theory(equality)],[c_6300,c_3028]) ).
tff(c_10256,plain,
! [X_187,Z_188] : ( multiply(inverse(X_187),Z_188) = double_divide(inverse(Z_188),X_187) ),
inference(superposition,[status(thm),theory(equality)],[c_10192,c_4478]) ).
tff(c_18752,plain,
! [Z_63,Y_62,X_61] : ( multiply(Z_63,multiply(double_divide(Z_63,double_divide(Y_62,X_61)),inverse(Y_62))) = X_61 ),
inference(superposition,[status(thm),theory(equality)],[c_4338,c_18441]) ).
tff(c_21704,plain,
! [Z_270,Y_271,X_272] : ( multiply(Z_270,double_divide(Y_271,multiply(double_divide(Y_271,X_272),Z_270))) = X_272 ),
inference(demodulation,[status(thm),theory(equality)],[c_5542,c_37,c_10256,c_4436,c_18752]) ).
tff(c_4472,plain,
! [Z_113,Z_112] : ( multiply(double_divide(Z_113,Z_112),Z_112) = inverse(Z_113) ),
inference(superposition,[status(thm),theory(equality)],[c_4447,c_37]) ).
tff(c_6544,plain,
! [X_147,Z_148] : ( multiply(multiply(X_147,Z_148),inverse(X_147)) = Z_148 ),
inference(superposition,[status(thm),theory(equality)],[c_3033,c_6300]) ).
tff(c_6589,plain,
! [Z_113,Z_112] : ( multiply(inverse(Z_113),inverse(double_divide(Z_113,Z_112))) = Z_112 ),
inference(superposition,[status(thm),theory(equality)],[c_4472,c_6544]) ).
tff(c_6651,plain,
! [Z_113,Z_112] : ( multiply(inverse(Z_113),multiply(Z_112,Z_113)) = Z_112 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_6589]) ).
tff(c_21805,plain,
! [Y_271,X_272,Z_270] : ( multiply(inverse(double_divide(Y_271,multiply(double_divide(Y_271,X_272),Z_270))),X_272) = Z_270 ),
inference(superposition,[status(thm),theory(equality)],[c_21704,c_6651]) ).
tff(c_50301,plain,
! [X_396,Y_397,Z_398] : ( multiply(X_396,multiply(Y_397,multiply(double_divide(Y_397,X_396),Z_398))) = Z_398 ),
inference(demodulation,[status(thm),theory(equality)],[c_4436,c_4436,c_37,c_21805]) ).
tff(c_50687,plain,
! [X_189,Z_190,Z_250] : ( multiply(multiply(X_189,Z_190),Z_250) = multiply(Z_190,multiply(X_189,Z_250)) ),
inference(superposition,[status(thm),theory(equality)],[c_18844,c_50301]) ).
tff(c_18799,plain,
! [X_4,Y_5,Z_250] : ( multiply(multiply(multiply(X_4,Y_5),Z_250),multiply(identity,double_divide(Y_5,X_4))) = Z_250 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_18441]) ).
tff(c_18893,plain,
! [Y_5,X_4,Z_250] : ( multiply(double_divide(Y_5,X_4),multiply(multiply(X_4,Y_5),Z_250)) = Z_250 ),
inference(demodulation,[status(thm),theory(equality)],[c_4436,c_3007,c_18799]) ).
tff(c_5285,plain,
! [X_130,Y_131] : ( inverse(multiply(X_130,Y_131)) = double_divide(Y_131,X_130) ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_55]) ).
tff(c_1713,plain,
! [Y_62,Z_63,Y_5] : ( multiply(double_divide(double_divide(identity,Y_62),double_divide(Z_63,double_divide(Y_62,Y_5))),Y_5) = Z_63 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1646]) ).
tff(c_2827,plain,
! [Z_79,Z_63] : ( multiply(double_divide(double_divide(identity,inverse(multiply(Z_79,identity))),double_divide(Z_63,identity)),Z_79) = Z_63 ),
inference(superposition,[status(thm),theory(equality)],[c_2818,c_1713]) ).
tff(c_2909,plain,
! [Z_79,Z_63] : ( multiply(double_divide(Z_79,inverse(Z_63)),Z_79) = Z_63 ),
inference(demodulation,[status(thm),theory(equality)],[c_1266,c_1217,c_6,c_2827]) ).
tff(c_19615,plain,
! [Z_256,Y_257,X_258] : ( multiply(double_divide(Z_256,double_divide(Y_257,X_258)),Z_256) = multiply(X_258,Y_257) ),
inference(superposition,[status(thm),theory(equality)],[c_5285,c_2909]) ).
tff(c_6366,plain,
! [X_6,Z_144] : ( multiply(multiply(X_6,Z_144),inverse(X_6)) = Z_144 ),
inference(superposition,[status(thm),theory(equality)],[c_3033,c_6300]) ).
tff(c_19699,plain,
! [X_258,Y_257,Z_256] : ( multiply(multiply(X_258,Y_257),inverse(double_divide(Z_256,double_divide(Y_257,X_258)))) = Z_256 ),
inference(superposition,[status(thm),theory(equality)],[c_19615,c_6366]) ).
tff(c_21188,plain,
! [X_267,Y_268,Z_269] : ( multiply(multiply(X_267,Y_268),multiply(double_divide(Y_268,X_267),Z_269)) = Z_269 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_19699]) ).
tff(c_30884,plain,
! [X_321,Y_322,Z_323] : ( multiply(multiply(X_321,Y_322),multiply(double_divide(X_321,Y_322),Z_323)) = Z_323 ),
inference(superposition,[status(thm),theory(equality)],[c_4436,c_21188]) ).
tff(c_31171,plain,
! [Y_5,X_4,Z_250] : ( multiply(multiply(Y_5,X_4),Z_250) = multiply(multiply(X_4,Y_5),Z_250) ),
inference(superposition,[status(thm),theory(equality)],[c_18893,c_30884]) ).
tff(c_132139,plain,
! [Y_5,X_4,Z_250] : ( multiply(Y_5,multiply(X_4,Z_250)) = multiply(X_4,multiply(Y_5,Z_250)) ),
inference(demodulation,[status(thm),theory(equality)],[c_50687,c_50687,c_31171]) ).
tff(c_1673,plain,
! [X_61,Y_62,Z_63] : ( inverse(double_divide(X_61,double_divide(double_divide(identity,Y_62),double_divide(Z_63,double_divide(Y_62,X_61))))) = Z_63 ),
inference(superposition,[status(thm),theory(equality)],[c_1646,c_6]) ).
tff(c_3600,plain,
! [Y_92,Z_93,X_94] : ( multiply(double_divide(inverse(Y_92),double_divide(Z_93,double_divide(Y_92,X_94))),X_94) = Z_93 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3027,c_1673]) ).
tff(c_3648,plain,
! [Y_92,X_94] : ( multiply(double_divide(inverse(Y_92),identity),X_94) = inverse(double_divide(Y_92,X_94)) ),
inference(superposition,[status(thm),theory(equality)],[c_3216,c_3600]) ).
tff(c_3688,plain,
! [Y_92,X_94] : ( multiply(Y_92,X_94) = multiply(X_94,Y_92) ),
inference(demodulation,[status(thm),theory(equality)],[c_3033,c_6,c_37,c_3648]) ).
tff(c_665,plain,
( ( multiply(identity,a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(b4,a4) != multiply(a4,b4) ) ),
inference(splitRight,[status(thm)],[c_190]) ).
tff(c_3594,plain,
( ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(b4,a4) != multiply(a4,b4) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3007,c_665]) ).
tff(c_3595,plain,
multiply(b4,a4) != multiply(a4,b4),
inference(splitLeft,[status(thm)],[c_3594]) ).
tff(c_4081,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3688,c_3595]) ).
tff(c_4082,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitRight,[status(thm)],[c_3594]) ).
tff(c_17496,plain,
multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_4436,c_4082]) ).
tff(c_132143,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_132139,c_17496]) ).
tff(c_132149,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4436,c_132143]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GRP103-1 : TPTP v9.0.0. Bugfixed v2.7.0.
% 0.03/0.14 % 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.36 % Computer : n013.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Mon Apr 7 21:17:02 EDT 2025
% 0.13/0.36 % CPUTime :
% 32.26/19.20 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 32.32/19.22
% 32.32/19.22 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------