%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP077-1 : TPTP v9.0.0. Bugfixed v2.3.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 : n024.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:24:56 PM UTC 2025
% Result : Unsatisfiable 15.93s 5.31s
% Output : CNFRefutation 16.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 5
% Syntax : Number of formulae : 109 ( 105 unt; 0 typ; 0 def)
% Number of atoms : 116 ( 113 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 15 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 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 : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 147 ( 147 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > double_divide > #nlpp > inverse > identity > c3 > b3 > 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(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(identity,type,
identity: $i ).
tff(f_29,axiom,
! [X,Y] : ( multiply(X,Y) = double_divide(double_divide(Y,X),identity) ),
file(unknown,unknown) ).
tff(f_32,axiom,
! [X] : ( inverse(X) = double_divide(X,identity) ),
file(unknown,unknown) ).
tff(f_35,axiom,
! [X] : ( identity = double_divide(X,inverse(X)) ),
file(unknown,unknown) ).
tff(f_43,axiom,
( ( multiply(inverse(a1),a1) != identity )
| ( multiply(identity,a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
file(unknown,unknown) ).
tff(f_26,axiom,
! [X,Y,Z] : ( double_divide(X,double_divide(double_divide(double_divide(identity,double_divide(double_divide(X,identity),double_divide(Y,Z))),Y),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_29]) ).
tff(c_6,plain,
! [X_6] : ( double_divide(X_6,identity) = inverse(X_6) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
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_35]) ).
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(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(identity,a2) != a2 )
| ( multiply(inverse(a1),a1) != identity ) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_188,plain,
( ( 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_189,plain,
inverse(identity) != identity,
inference(splitLeft,[status(thm)],[c_188]) ).
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_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_29]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3] : ( double_divide(X_1,double_divide(double_divide(double_divide(identity,double_divide(double_divide(X_1,identity),double_divide(Y_2,Z_3))),Y_2),identity)) = Z_3 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_90,plain,
! [X_15,Y_16,Z_17] : ( double_divide(X_15,multiply(Y_16,double_divide(identity,double_divide(inverse(X_15),double_divide(Y_16,Z_17))))) = Z_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_2]) ).
tff(c_120,plain,
! [X_15,X_7] : ( double_divide(X_15,multiply(X_7,double_divide(identity,double_divide(inverse(X_15),identity)))) = inverse(X_7) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_90]) ).
tff(c_124,plain,
! [X_15,X_7] : ( double_divide(X_15,multiply(X_7,double_divide(identity,inverse(inverse(X_15))))) = inverse(X_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_120]) ).
tff(c_368,plain,
! [X_15,X_7] : ( double_divide(X_15,multiply(X_7,double_divide(identity,multiply(identity,X_15)))) = inverse(X_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_83,c_124]) ).
tff(c_500,plain,
! [X_31,X_32] : ( double_divide(X_31,multiply(X_32,double_divide(identity,double_divide(inverse(X_31),inverse(X_32))))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_90]) ).
tff(c_546,plain,
! [X_31] : ( double_divide(X_31,multiply(inverse(X_31),double_divide(identity,identity))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_500]) ).
tff(c_552,plain,
! [X_33] : ( double_divide(X_33,multiply(inverse(X_33),inverse(identity))) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_546]) ).
tff(c_584,plain,
double_divide(inverse(identity),inverse(identity)) = identity,
inference(superposition,[status(thm),theory(equality)],[c_57,c_552]) ).
tff(c_11,plain,
! [X_1,Y_2,Z_3] : ( double_divide(X_1,multiply(Y_2,double_divide(identity,double_divide(inverse(X_1),double_divide(Y_2,Z_3))))) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4,c_2]) ).
tff(c_604,plain,
! [X_1] : ( double_divide(X_1,multiply(inverse(identity),double_divide(identity,double_divide(inverse(X_1),identity)))) = inverse(identity) ),
inference(superposition,[status(thm),theory(equality)],[c_584,c_11]) ).
tff(c_615,plain,
multiply(identity,identity) = inverse(identity),
inference(demodulation,[status(thm),theory(equality)],[c_83,c_368,c_83,c_6,c_604]) ).
tff(c_624,plain,
! [X_7] : ( double_divide(identity,multiply(X_7,double_divide(identity,inverse(identity)))) = inverse(X_7) ),
inference(superposition,[status(thm),theory(equality)],[c_615,c_368]) ).
tff(c_1049,plain,
! [X_43] : ( double_divide(identity,multiply(X_43,identity)) = inverse(X_43) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_624]) ).
tff(c_1094,plain,
double_divide(identity,inverse(identity)) = inverse(identity),
inference(superposition,[status(thm),theory(equality)],[c_615,c_1049]) ).
tff(c_1107,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_1094]) ).
tff(c_1109,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_189,c_1107]) ).
tff(c_1111,plain,
inverse(identity) = identity,
inference(splitRight,[status(thm)],[c_188]) ).
tff(c_1462,plain,
! [X_15,X_7] : ( double_divide(X_15,multiply(X_7,double_divide(identity,multiply(identity,X_15)))) = inverse(X_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_83,c_124]) ).
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_1672,plain,
! [X_59,X_60] : ( double_divide(X_59,multiply(X_60,double_divide(identity,double_divide(inverse(X_59),inverse(X_60))))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_90]) ).
tff(c_1730,plain,
! [X_59] : ( double_divide(X_59,multiply(inverse(X_59),double_divide(identity,identity))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_1672]) ).
tff(c_1741,plain,
! [X_61] : ( double_divide(X_61,multiply(inverse(X_61),identity)) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_6,c_1730]) ).
tff(c_1759,plain,
! [X_1,X_61] : ( double_divide(X_1,multiply(X_61,double_divide(identity,double_divide(inverse(X_1),identity)))) = multiply(inverse(X_61),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_1741,c_11]) ).
tff(c_1791,plain,
! [X_61] : ( multiply(inverse(X_61),identity) = inverse(X_61) ),
inference(demodulation,[status(thm),theory(equality)],[c_1462,c_46,c_1759]) ).
tff(c_153,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_165,plain,
! [X_19] : ( multiply(identity,inverse(X_19)) = double_divide(multiply(identity,X_19),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_153,c_4]) ).
tff(c_182,plain,
! [X_19] : ( multiply(identity,inverse(X_19)) = inverse(multiply(identity,X_19)) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_165]) ).
tff(c_1800,plain,
! [X_62] : ( multiply(inverse(X_62),identity) = inverse(X_62) ),
inference(demodulation,[status(thm),theory(equality)],[c_1462,c_46,c_1759]) ).
tff(c_1116,plain,
multiply(identity,identity) = double_divide(identity,identity),
inference(superposition,[status(thm),theory(equality)],[c_1111,c_46]) ).
tff(c_1128,plain,
multiply(identity,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_6,c_1116]) ).
tff(c_1463,plain,
! [X_54,X_55] : ( double_divide(X_54,multiply(X_55,double_divide(identity,multiply(identity,X_54)))) = inverse(X_55) ),
inference(demodulation,[status(thm),theory(equality)],[c_83,c_124]) ).
tff(c_1467,plain,
! [X_7] : ( double_divide(double_divide(identity,multiply(identity,identity)),multiply(X_7,inverse(identity))) = inverse(X_7) ),
inference(superposition,[status(thm),theory(equality)],[c_1463,c_1462]) ).
tff(c_1533,plain,
! [X_56] : ( double_divide(identity,multiply(X_56,identity)) = inverse(X_56) ),
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_6,c_1128,c_1111,c_1467]) ).
tff(c_1558,plain,
! [X_56] : ( multiply(multiply(X_56,identity),identity) = double_divide(inverse(X_56),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_1533,c_4]) ).
tff(c_1574,plain,
! [X_56] : ( multiply(multiply(X_56,identity),identity) = multiply(identity,X_56) ),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_1558]) ).
tff(c_1806,plain,
! [X_62] : ( multiply(inverse(X_62),identity) = multiply(identity,inverse(X_62)) ),
inference(superposition,[status(thm),theory(equality)],[c_1800,c_1574]) ).
tff(c_1840,plain,
! [X_62] : ( inverse(multiply(identity,X_62)) = inverse(X_62) ),
inference(demodulation,[status(thm),theory(equality)],[c_1791,c_182,c_1806]) ).
tff(c_1849,plain,
! [X_19] : ( multiply(identity,inverse(X_19)) = inverse(X_19) ),
inference(demodulation,[status(thm),theory(equality)],[c_1840,c_182]) ).
tff(c_1521,plain,
! [X_7] : ( double_divide(identity,multiply(X_7,identity)) = inverse(X_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_6,c_1128,c_1111,c_1467]) ).
tff(c_1809,plain,
! [X_62] : ( double_divide(identity,inverse(X_62)) = inverse(inverse(X_62)) ),
inference(superposition,[status(thm),theory(equality)],[c_1800,c_1521]) ).
tff(c_2016,plain,
! [X_66] : ( double_divide(identity,inverse(X_66)) = multiply(identity,X_66) ),
inference(demodulation,[status(thm),theory(equality)],[c_83,c_1809]) ).
tff(c_2056,plain,
! [X_6] : ( multiply(identity,inverse(X_6)) = double_divide(identity,multiply(identity,X_6)) ),
inference(superposition,[status(thm),theory(equality)],[c_83,c_2016]) ).
tff(c_23897,plain,
! [X_316] : ( double_divide(identity,multiply(identity,X_316)) = inverse(X_316) ),
inference(demodulation,[status(thm),theory(equality)],[c_1849,c_2056]) ).
tff(c_23924,plain,
! [Z_3] : ( inverse(double_divide(identity,double_divide(inverse(identity),double_divide(identity,Z_3)))) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_23897,c_11]) ).
tff(c_23960,plain,
! [Z_3] : ( multiply(double_divide(identity,double_divide(identity,Z_3)),identity) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1111,c_23924]) ).
tff(c_27198,plain,
! [Z_358] : ( multiply(double_divide(identity,double_divide(identity,Z_358)),identity) = Z_358 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1111,c_23924]) ).
tff(c_1838,plain,
! [X_11,Y_10] : ( multiply(multiply(X_11,Y_10),identity) = inverse(double_divide(Y_10,X_11)) ),
inference(superposition,[status(thm),theory(equality)],[c_37,c_1800]) ).
tff(c_1848,plain,
! [X_11,Y_10] : ( multiply(multiply(X_11,Y_10),identity) = multiply(X_11,Y_10) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1838]) ).
tff(c_27231,plain,
! [Z_358] : ( multiply(double_divide(identity,double_divide(identity,Z_358)),identity) = multiply(Z_358,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_27198,c_1848]) ).
tff(c_27292,plain,
! [Z_358] : ( multiply(Z_358,identity) = Z_358 ),
inference(demodulation,[status(thm),theory(equality)],[c_23960,c_27231]) ).
tff(c_24057,plain,
! [X_318,Y_319] : ( multiply(multiply(X_318,Y_319),identity) = multiply(X_318,Y_319) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1838]) ).
tff(c_24070,plain,
! [X_318] : ( multiply(identity,X_318) = multiply(X_318,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_24057,c_1574]) ).
tff(c_2076,plain,
! [X_6] : ( double_divide(identity,multiply(identity,X_6)) = inverse(X_6) ),
inference(demodulation,[status(thm),theory(equality)],[c_1849,c_2056]) ).
tff(c_2125,plain,
! [X_15,X_7] : ( double_divide(X_15,multiply(X_7,inverse(X_15))) = inverse(X_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_2076,c_1462]) ).
tff(c_2126,plain,
! [X_68] : ( double_divide(identity,multiply(identity,X_68)) = inverse(X_68) ),
inference(demodulation,[status(thm),theory(equality)],[c_1849,c_2056]) ).
tff(c_2183,plain,
! [Z_3] : ( inverse(double_divide(identity,double_divide(inverse(identity),double_divide(identity,Z_3)))) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_2126]) ).
tff(c_2198,plain,
! [Z_3] : ( multiply(double_divide(identity,double_divide(identity,Z_3)),identity) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1111,c_2183]) ).
tff(c_5862,plain,
! [Z_115] : ( multiply(double_divide(identity,double_divide(identity,Z_115)),identity) = Z_115 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1111,c_2183]) ).
tff(c_2321,plain,
! [X_71,Y_72] : ( multiply(multiply(X_71,Y_72),identity) = multiply(X_71,Y_72) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_1838]) ).
tff(c_2330,plain,
! [X_71,Y_72] : ( multiply(multiply(X_71,Y_72),identity) = multiply(identity,multiply(X_71,Y_72)) ),
inference(superposition,[status(thm),theory(equality)],[c_2321,c_1574]) ).
tff(c_2382,plain,
! [X_71,Y_72] : ( multiply(identity,multiply(X_71,Y_72)) = multiply(X_71,Y_72) ),
inference(demodulation,[status(thm),theory(equality)],[c_1848,c_2330]) ).
tff(c_5871,plain,
! [Z_115] : ( multiply(double_divide(identity,double_divide(identity,Z_115)),identity) = multiply(identity,Z_115) ),
inference(superposition,[status(thm),theory(equality)],[c_5862,c_2382]) ).
tff(c_5951,plain,
! [Z_115] : ( multiply(identity,Z_115) = Z_115 ),
inference(demodulation,[status(thm),theory(equality)],[c_2198,c_5871]) ).
tff(c_31,plain,
! [Y_10,X_11] : ( multiply(identity,double_divide(Y_10,X_11)) = double_divide(multiply(X_11,Y_10),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_4]) ).
tff(c_53,plain,
! [Y_10,X_11] : ( multiply(identity,double_divide(Y_10,X_11)) = inverse(multiply(X_11,Y_10)) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_31]) ).
tff(c_5981,plain,
! [X_11,Y_10] : ( inverse(multiply(X_11,Y_10)) = double_divide(Y_10,X_11) ),
inference(demodulation,[status(thm),theory(equality)],[c_5951,c_53]) ).
tff(c_5974,plain,
! [X_6] : ( double_divide(identity,X_6) = inverse(X_6) ),
inference(demodulation,[status(thm),theory(equality)],[c_5951,c_2076]) ).
tff(c_1122,plain,
! [Y_2,Z_3] : ( double_divide(identity,multiply(Y_2,double_divide(identity,double_divide(identity,double_divide(Y_2,Z_3))))) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_1111,c_11]) ).
tff(c_6753,plain,
! [Y_2,Z_3] : ( inverse(multiply(Y_2,inverse(multiply(Z_3,Y_2)))) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_5974,c_5974,c_37,c_5974,c_1122]) ).
tff(c_6986,plain,
! [Y_135,Z_136] : ( double_divide(double_divide(Y_135,Z_136),Y_135) = Z_136 ),
inference(demodulation,[status(thm),theory(equality)],[c_5981,c_5981,c_6753]) ).
tff(c_7039,plain,
! [X_7,X_15] : ( multiply(X_7,inverse(X_15)) = double_divide(inverse(X_7),X_15) ),
inference(superposition,[status(thm),theory(equality)],[c_2125,c_6986]) ).
tff(c_5895,plain,
! [Z_115] : ( multiply(double_divide(identity,double_divide(identity,Z_115)),identity) = multiply(Z_115,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_5862,c_1848]) ).
tff(c_5956,plain,
! [Z_115] : ( multiply(Z_115,identity) = Z_115 ),
inference(demodulation,[status(thm),theory(equality)],[c_2198,c_5895]) ).
tff(c_3970,plain,
! [Y_95,X_96,Z_97,X_98] : ( multiply(Y_95,double_divide(identity,double_divide(inverse(X_96),double_divide(Y_95,Z_97)))) = double_divide(X_98,multiply(X_96,double_divide(identity,double_divide(inverse(X_98),Z_97)))) ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_90]) ).
tff(c_4264,plain,
! [Y_95,X_96,X_98] : ( multiply(Y_95,double_divide(identity,double_divide(inverse(X_96),double_divide(Y_95,inverse(inverse(X_98)))))) = double_divide(X_98,multiply(X_96,double_divide(identity,identity))) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_3970]) ).
tff(c_4314,plain,
! [Y_95,X_96,X_98] : ( multiply(Y_95,double_divide(identity,double_divide(inverse(X_96),double_divide(Y_95,multiply(identity,X_98))))) = double_divide(X_98,multiply(X_96,identity)) ),
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_6,c_83,c_4264]) ).
tff(c_14697,plain,
! [Y_235,X_236,X_237] : ( multiply(Y_235,double_divide(multiply(X_236,Y_235),X_237)) = double_divide(X_236,X_237) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_7039,c_37,c_5974,c_5956,c_5951,c_4314]) ).
tff(c_14759,plain,
! [X_236,Y_235,X_237] : ( double_divide(double_divide(multiply(X_236,Y_235),X_237),Y_235) = inverse(double_divide(X_236,X_237)) ),
inference(superposition,[status(thm),theory(equality)],[c_14697,c_5981]) ).
tff(c_19117,plain,
! [X_273,Y_274,X_275] : ( double_divide(double_divide(multiply(X_273,Y_274),X_275),Y_274) = multiply(X_275,X_273) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_14759]) ).
tff(c_6911,plain,
! [Y_2,Z_3] : ( double_divide(double_divide(Y_2,Z_3),Y_2) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_5981,c_5981,c_6753]) ).
tff(c_7077,plain,
! [Z_137,Y_138] : ( double_divide(Z_137,double_divide(Y_138,Z_137)) = Y_138 ),
inference(superposition,[status(thm),theory(equality)],[c_6986,c_6911]) ).
tff(c_7105,plain,
! [Y_138,Z_137] : ( multiply(double_divide(Y_138,Z_137),Z_137) = double_divide(Y_138,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_7077,c_4]) ).
tff(c_7156,plain,
! [Y_138,Z_137] : ( multiply(double_divide(Y_138,Z_137),Z_137) = inverse(Y_138) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_7105]) ).
tff(c_19189,plain,
! [X_273,Y_274,X_275] : ( inverse(double_divide(multiply(X_273,Y_274),X_275)) = multiply(multiply(X_275,X_273),Y_274) ),
inference(superposition,[status(thm),theory(equality)],[c_19117,c_7156]) ).
tff(c_19372,plain,
! [X_275,X_273,Y_274] : ( multiply(multiply(X_275,X_273),Y_274) = multiply(X_275,multiply(X_273,Y_274)) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_19189]) ).
tff(c_1110,plain,
( ( multiply(identity,a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
inference(splitRight,[status(thm)],[c_188]) ).
tff(c_2124,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitLeft,[status(thm)],[c_1110]) ).
tff(c_23893,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_19372,c_2124]) ).
tff(c_23894,plain,
multiply(identity,a2) != a2,
inference(splitRight,[status(thm)],[c_1110]) ).
tff(c_24134,plain,
multiply(a2,identity) != a2,
inference(demodulation,[status(thm),theory(equality)],[c_24070,c_23894]) ).
tff(c_27456,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_27292,c_24134]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.13 % Problem : GRP077-1 : TPTP v9.0.0. Bugfixed v2.3.0.
% 0.10/0.14 % 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.34 % Computer : n024.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 21:15:21 EDT 2025
% 0.14/0.34 % CPUTime :
% 15.93/5.31 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.13/5.33
% 16.13/5.33 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------