%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP567-1 : TPTP v9.0.0. Released v2.6.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 : n004.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:26:32 PM UTC 2025
% Result : Unsatisfiable 33.07s 20.22s
% Output : CNFRefutation 33.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 5
% Syntax : Number of formulae : 121 ( 121 unt; 0 typ; 0 def)
% Number of atoms : 121 ( 120 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 237 ( 237 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > double_divide > #nlpp > inverse > identity > c3 > b3 > a3
%Foreground sorts:
%Background operators:
%Foreground operators:
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(identity,type,
identity: $i ).
tff(f_27,axiom,
! [A] : ( inverse(A) = double_divide(A,identity) ),
file(unknown,unknown) ).
tff(f_29,axiom,
! [A] : ( identity = double_divide(A,inverse(A)) ),
file(unknown,unknown) ).
tff(f_23,axiom,
! [A,B,C] : ( double_divide(double_divide(A,double_divide(double_divide(B,double_divide(A,C)),double_divide(identity,C))),double_divide(identity,identity)) = B ),
file(unknown,unknown) ).
tff(f_25,axiom,
! [A,B] : ( multiply(A,B) = double_divide(double_divide(B,A),identity) ),
file(unknown,unknown) ).
tff(f_31,axiom,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file(unknown,unknown) ).
tff(c_6,plain,
! [A_6] : ( double_divide(A_6,identity) = inverse(A_6) ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_8,plain,
! [A_7] : ( double_divide(A_7,inverse(A_7)) = identity ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_2,plain,
! [A_1,B_2,C_3] : ( double_divide(double_divide(A_1,double_divide(double_divide(B_2,double_divide(A_1,C_3)),double_divide(identity,C_3))),double_divide(identity,identity)) = B_2 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_236,plain,
! [A_21,B_22,C_23] : ( double_divide(double_divide(A_21,double_divide(double_divide(B_22,double_divide(A_21,C_23)),double_divide(identity,C_23))),inverse(identity)) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_2]) ).
tff(c_272,plain,
! [A_6,B_22] : ( double_divide(double_divide(A_6,double_divide(double_divide(B_22,inverse(A_6)),double_divide(identity,identity))),inverse(identity)) = B_22 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_236]) ).
tff(c_711,plain,
! [A_38,B_39] : ( double_divide(double_divide(A_38,double_divide(double_divide(B_39,inverse(A_38)),inverse(identity))),inverse(identity)) = B_39 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_272]) ).
tff(c_777,plain,
! [A_7] : ( double_divide(double_divide(A_7,double_divide(identity,inverse(identity))),inverse(identity)) = A_7 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_711]) ).
tff(c_782,plain,
! [A_7] : ( double_divide(inverse(A_7),inverse(identity)) = A_7 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_8,c_777]) ).
tff(c_28,plain,
! [B_10,A_11] : ( double_divide(double_divide(B_10,A_11),identity) = multiply(A_11,B_10) ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_65,plain,
! [B_13,A_14] : ( inverse(double_divide(B_13,A_14)) = multiply(A_14,B_13) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_6]) ).
tff(c_83,plain,
! [A_6] : ( inverse(inverse(A_6)) = multiply(identity,A_6) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_65]) ).
tff(c_783,plain,
! [A_40] : ( double_divide(inverse(A_40),inverse(identity)) = A_40 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_8,c_777]) ).
tff(c_855,plain,
! [A_42] : ( double_divide(multiply(identity,A_42),inverse(identity)) = inverse(A_42) ),
inference(superposition,[status(thm),theory(equality)],[c_83,c_783]) ).
tff(c_293,plain,
! [A_6,B_22] : ( double_divide(double_divide(A_6,double_divide(double_divide(B_22,inverse(A_6)),inverse(identity))),inverse(identity)) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_272]) ).
tff(c_861,plain,
! [A_42] : ( double_divide(double_divide(identity,double_divide(inverse(A_42),inverse(identity))),inverse(identity)) = multiply(identity,A_42) ),
inference(superposition,[status(thm),theory(equality)],[c_855,c_293]) ).
tff(c_1043,plain,
! [A_47] : ( double_divide(double_divide(identity,A_47),inverse(identity)) = multiply(identity,A_47) ),
inference(demodulation,[status(thm),theory(equality)],[c_782,c_861]) ).
tff(c_1131,plain,
double_divide(inverse(identity),inverse(identity)) = multiply(identity,identity),
inference(superposition,[status(thm),theory(equality)],[c_6,c_1043]) ).
tff(c_1146,plain,
multiply(identity,identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_782,c_1131]) ).
tff(c_52,plain,
! [A_7] : ( multiply(inverse(A_7),A_7) = double_divide(identity,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_28]) ).
tff(c_57,plain,
! [A_7] : ( multiply(inverse(A_7),A_7) = inverse(identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_52]) ).
tff(c_37,plain,
! [B_10,A_11] : ( inverse(double_divide(B_10,A_11)) = multiply(A_11,B_10) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_6]) ).
tff(c_824,plain,
! [A_41] : ( multiply(inverse(identity),inverse(A_41)) = inverse(A_41) ),
inference(superposition,[status(thm),theory(equality)],[c_783,c_37]) ).
tff(c_845,plain,
! [A_11,B_10] : ( multiply(inverse(identity),multiply(A_11,B_10)) = inverse(double_divide(B_10,A_11)) ),
inference(superposition,[status(thm),theory(equality)],[c_37,c_824]) ).
tff(c_852,plain,
! [A_11,B_10] : ( multiply(inverse(identity),multiply(A_11,B_10)) = multiply(A_11,B_10) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_845]) ).
tff(c_1151,plain,
multiply(inverse(identity),identity) = multiply(identity,identity),
inference(superposition,[status(thm),theory(equality)],[c_1146,c_852]) ).
tff(c_1184,plain,
inverse(identity) = identity,
inference(demodulation,[status(thm),theory(equality)],[c_1146,c_57,c_1151]) ).
tff(c_1199,plain,
! [A_7] : ( double_divide(inverse(A_7),identity) = A_7 ),
inference(demodulation,[status(thm),theory(equality)],[c_1184,c_782]) ).
tff(c_46,plain,
! [A_6] : ( double_divide(inverse(A_6),identity) = multiply(identity,A_6) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_28]) ).
tff(c_1398,plain,
! [A_6] : ( multiply(identity,A_6) = A_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_1199,c_46]) ).
tff(c_1547,plain,
! [A_59] : ( inverse(inverse(A_59)) = A_59 ),
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_83]) ).
tff(c_1562,plain,
! [A_59] : ( double_divide(inverse(A_59),A_59) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_1547,c_8]) ).
tff(c_1210,plain,
! [A_7] : ( multiply(inverse(A_7),A_7) = identity ),
inference(demodulation,[status(thm),theory(equality)],[c_1184,c_57]) ).
tff(c_1645,plain,
! [A_61] : ( multiply(A_61,inverse(A_61)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_1547,c_1210]) ).
tff(c_4,plain,
! [B_5,A_4] : ( double_divide(double_divide(B_5,A_4),identity) = multiply(A_4,B_5) ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_269,plain,
! [B_5,A_4,B_22] : ( double_divide(double_divide(double_divide(B_5,A_4),double_divide(double_divide(B_22,multiply(A_4,B_5)),double_divide(identity,identity))),inverse(identity)) = B_22 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_236]) ).
tff(c_292,plain,
! [B_5,A_4,B_22] : ( double_divide(double_divide(double_divide(B_5,A_4),double_divide(double_divide(B_22,multiply(A_4,B_5)),inverse(identity))),inverse(identity)) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_269]) ).
tff(c_1238,plain,
! [A_4,B_5,B_22] : ( multiply(multiply(multiply(A_4,B_5),B_22),double_divide(B_5,A_4)) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_6,c_1184,c_37,c_6,c_1184,c_292]) ).
tff(c_1654,plain,
! [B_22,A_61] : ( multiply(multiply(identity,B_22),double_divide(inverse(A_61),A_61)) = B_22 ),
inference(superposition,[status(thm),theory(equality)],[c_1645,c_1238]) ).
tff(c_1679,plain,
! [B_22] : ( multiply(B_22,identity) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_1562,c_1398,c_1654]) ).
tff(c_1448,plain,
! [A_6] : ( inverse(inverse(A_6)) = A_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_83]) ).
tff(c_251,plain,
! [A_21,B_22,C_23] : ( multiply(inverse(identity),double_divide(A_21,double_divide(double_divide(B_22,double_divide(A_21,C_23)),double_divide(identity,C_23)))) = double_divide(B_22,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_236,c_4]) ).
tff(c_286,plain,
! [A_21,B_22,C_23] : ( multiply(inverse(identity),double_divide(A_21,double_divide(double_divide(B_22,double_divide(A_21,C_23)),double_divide(identity,C_23)))) = inverse(B_22) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_251]) ).
tff(c_1466,plain,
! [A_21,B_22,C_23] : ( double_divide(A_21,double_divide(double_divide(B_22,double_divide(A_21,C_23)),double_divide(identity,C_23))) = inverse(B_22) ),
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_1184,c_286]) ).
tff(c_11,plain,
! [A_1,B_2,C_3] : ( double_divide(double_divide(A_1,double_divide(double_divide(B_2,double_divide(A_1,C_3)),double_divide(identity,C_3))),inverse(identity)) = B_2 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_2]) ).
tff(c_254,plain,
! [A_1,B_2,C_3,B_22] : ( double_divide(double_divide(double_divide(A_1,double_divide(double_divide(B_2,double_divide(A_1,C_3)),double_divide(identity,C_3))),double_divide(double_divide(B_22,B_2),double_divide(identity,inverse(identity)))),inverse(identity)) = B_22 ),
inference(superposition,[status(thm),theory(equality)],[c_11,c_236]) ).
tff(c_287,plain,
! [A_1,B_2,C_3,B_22] : ( double_divide(double_divide(double_divide(A_1,double_divide(double_divide(B_2,double_divide(A_1,C_3)),double_divide(identity,C_3))),multiply(B_2,B_22)),inverse(identity)) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_6,c_8,c_254]) ).
tff(c_1728,plain,
! [B_63,B_64] : ( multiply(multiply(B_63,B_64),inverse(B_63)) = B_64 ),
inference(demodulation,[status(thm),theory(equality)],[c_1466,c_37,c_6,c_1184,c_287]) ).
tff(c_2361,plain,
! [B_78,B_79] : ( multiply(B_78,double_divide(B_78,B_79)) = inverse(B_79) ),
inference(superposition,[status(thm),theory(equality)],[c_1728,c_1238]) ).
tff(c_80,plain,
! [B_5,A_4] : ( multiply(identity,double_divide(B_5,A_4)) = inverse(multiply(A_4,B_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65]) ).
tff(c_1445,plain,
! [A_4,B_5] : ( inverse(multiply(A_4,B_5)) = double_divide(B_5,A_4) ),
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_80]) ).
tff(c_2378,plain,
! [B_78,B_79] : ( double_divide(double_divide(B_78,B_79),B_78) = inverse(inverse(B_79)) ),
inference(superposition,[status(thm),theory(equality)],[c_2361,c_1445]) ).
tff(c_2445,plain,
! [B_78,B_79] : ( double_divide(double_divide(B_78,B_79),B_78) = B_79 ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_2378]) ).
tff(c_283,plain,
! [A_21,B_22] : ( double_divide(double_divide(A_21,double_divide(double_divide(B_22,double_divide(A_21,inverse(identity))),identity)),inverse(identity)) = B_22 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_236]) ).
tff(c_434,plain,
! [A_29,B_30] : ( double_divide(double_divide(A_29,multiply(double_divide(A_29,inverse(identity)),B_30)),inverse(identity)) = B_30 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_6,c_283]) ).
tff(c_455,plain,
! [A_29,B_30] : ( multiply(inverse(identity),double_divide(A_29,multiply(double_divide(A_29,inverse(identity)),B_30))) = inverse(B_30) ),
inference(superposition,[status(thm),theory(equality)],[c_434,c_37]) ).
tff(c_1873,plain,
! [A_66,B_67] : ( double_divide(A_66,multiply(inverse(A_66),B_67)) = inverse(B_67) ),
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_6,c_1184,c_1184,c_455]) ).
tff(c_1919,plain,
! [B_67] : ( double_divide(identity,multiply(identity,B_67)) = inverse(B_67) ),
inference(superposition,[status(thm),theory(equality)],[c_1184,c_1873]) ).
tff(c_1932,plain,
! [B_67] : ( double_divide(identity,B_67) = inverse(B_67) ),
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_1919]) ).
tff(c_248,plain,
! [A_21,B_22,C_23] : ( multiply(inverse(identity),double_divide(A_21,double_divide(double_divide(B_22,double_divide(A_21,C_23)),double_divide(identity,C_23)))) = inverse(B_22) ),
inference(superposition,[status(thm),theory(equality)],[c_236,c_37]) ).
tff(c_4550,plain,
! [A_114,B_115,C_116] : ( double_divide(A_114,double_divide(double_divide(B_115,double_divide(A_114,C_116)),inverse(C_116))) = inverse(B_115) ),
inference(demodulation,[status(thm),theory(equality)],[c_1932,c_1398,c_1184,c_248]) ).
tff(c_4666,plain,
! [A_114,C_116] : ( double_divide(A_114,double_divide(A_114,C_116)) = inverse(inverse(C_116)) ),
inference(superposition,[status(thm),theory(equality)],[c_2445,c_4550]) ).
tff(c_4763,plain,
! [A_117,C_118] : ( double_divide(A_117,double_divide(A_117,C_118)) = C_118 ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_4666]) ).
tff(c_5108,plain,
! [C_121,A_122] : ( double_divide(C_121,A_122) = double_divide(A_122,C_121) ),
inference(superposition,[status(thm),theory(equality)],[c_4763,c_2445]) ).
tff(c_5427,plain,
! [C_123,A_124] : ( double_divide(double_divide(C_123,A_124),identity) = multiply(C_123,A_124) ),
inference(superposition,[status(thm),theory(equality)],[c_5108,c_4]) ).
tff(c_2462,plain,
! [B_80,B_81] : ( double_divide(double_divide(B_80,B_81),B_80) = B_81 ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_2378]) ).
tff(c_2565,plain,
! [B_82,B_83] : ( double_divide(B_82,double_divide(B_83,B_82)) = B_83 ),
inference(superposition,[status(thm),theory(equality)],[c_2462,c_2445]) ).
tff(c_2593,plain,
! [B_83,B_82] : ( multiply(double_divide(B_83,B_82),B_82) = inverse(B_83) ),
inference(superposition,[status(thm),theory(equality)],[c_2565,c_37]) ).
tff(c_5461,plain,
! [C_123,A_124] : ( multiply(multiply(C_123,A_124),identity) = inverse(double_divide(C_123,A_124)) ),
inference(superposition,[status(thm),theory(equality)],[c_5427,c_2593]) ).
tff(c_5594,plain,
! [C_123,A_124] : ( multiply(C_123,A_124) = multiply(A_124,C_123) ),
inference(demodulation,[status(thm),theory(equality)],[c_1679,c_37,c_5461]) ).
tff(c_5279,plain,
! [C_121,A_122] : ( double_divide(double_divide(C_121,A_122),identity) = multiply(C_121,A_122) ),
inference(superposition,[status(thm),theory(equality)],[c_5108,c_4]) ).
tff(c_4805,plain,
! [C_118,A_117] : ( double_divide(C_118,A_117) = double_divide(A_117,C_118) ),
inference(superposition,[status(thm),theory(equality)],[c_4763,c_2445]) ).
tff(c_1740,plain,
! [B_64,B_63] : ( multiply(B_64,double_divide(B_64,B_63)) = inverse(B_63) ),
inference(superposition,[status(thm),theory(equality)],[c_1728,c_1238]) ).
tff(c_1727,plain,
! [B_2,B_22] : ( multiply(multiply(B_2,B_22),inverse(B_2)) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_1466,c_37,c_6,c_1184,c_287]) ).
tff(c_819,plain,
! [A_11,B_10] : ( double_divide(multiply(A_11,B_10),inverse(identity)) = double_divide(B_10,A_11) ),
inference(superposition,[status(thm),theory(equality)],[c_37,c_783]) ).
tff(c_3324,plain,
! [A_96,B_97] : ( double_divide(multiply(A_96,B_97),identity) = double_divide(B_97,A_96) ),
inference(demodulation,[status(thm),theory(equality)],[c_1184,c_819]) ).
tff(c_3390,plain,
! [B_2,B_22] : ( double_divide(inverse(B_2),multiply(B_2,B_22)) = double_divide(B_22,identity) ),
inference(superposition,[status(thm),theory(equality)],[c_1727,c_3324]) ).
tff(c_3600,plain,
! [B_100,B_101] : ( double_divide(inverse(B_100),multiply(B_100,B_101)) = inverse(B_101) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_3390]) ).
tff(c_3663,plain,
! [B_64,B_63] : ( double_divide(inverse(B_64),inverse(B_63)) = inverse(double_divide(B_64,B_63)) ),
inference(superposition,[status(thm),theory(equality)],[c_1740,c_3600]) ).
tff(c_3718,plain,
! [B_64,B_63] : ( double_divide(inverse(B_64),inverse(B_63)) = multiply(B_63,B_64) ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_3663]) ).
tff(c_1467,plain,
! [A_56,B_57,C_58] : ( double_divide(A_56,double_divide(double_divide(B_57,double_divide(A_56,C_58)),double_divide(identity,C_58))) = inverse(B_57) ),
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_1184,c_286]) ).
tff(c_1473,plain,
! [B_57,A_56,C_58] : ( double_divide(double_divide(B_57,double_divide(A_56,C_58)),double_divide(inverse(B_57),double_divide(identity,double_divide(identity,C_58)))) = inverse(A_56) ),
inference(superposition,[status(thm),theory(equality)],[c_1467,c_1466]) ).
tff(c_101199,plain,
! [B_491,A_492,C_493] : ( double_divide(double_divide(B_491,double_divide(A_492,C_493)),double_divide(inverse(B_491),C_493)) = inverse(A_492) ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_1932,c_1932,c_1473]) ).
tff(c_102152,plain,
! [B_491,B_63,B_64] : ( double_divide(double_divide(B_491,multiply(B_63,B_64)),double_divide(inverse(B_491),inverse(B_63))) = inverse(inverse(B_64)) ),
inference(superposition,[status(thm),theory(equality)],[c_3718,c_101199]) ).
tff(c_102456,plain,
! [B_494,B_495,B_496] : ( double_divide(multiply(B_494,B_495),double_divide(B_495,multiply(B_494,B_496))) = B_496 ),
inference(demodulation,[status(thm),theory(equality)],[c_4805,c_3718,c_1448,c_102152]) ).
tff(c_111212,plain,
! [B_517,B_516,B_515] : ( double_divide(B_517,multiply(B_516,B_515)) = double_divide(B_515,multiply(B_516,B_517)) ),
inference(superposition,[status(thm),theory(equality)],[c_102456,c_2445]) ).
tff(c_112569,plain,
! [B_517,B_516,B_515] : ( double_divide(double_divide(B_517,multiply(B_516,B_515)),identity) = multiply(multiply(B_516,B_517),B_515) ),
inference(superposition,[status(thm),theory(equality)],[c_111212,c_4]) ).
tff(c_113497,plain,
! [B_516,B_517,B_515] : ( multiply(multiply(B_516,B_517),B_515) = multiply(B_517,multiply(B_516,B_515)) ),
inference(demodulation,[status(thm),theory(equality)],[c_5279,c_112569]) ).
tff(c_4748,plain,
! [A_114,C_116] : ( double_divide(A_114,double_divide(A_114,C_116)) = C_116 ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_4666]) ).
tff(c_102802,plain,
! [B_494,B_495,B_496] : ( double_divide(multiply(B_494,B_495),B_496) = double_divide(B_495,multiply(B_494,B_496)) ),
inference(superposition,[status(thm),theory(equality)],[c_102456,c_4748]) ).
tff(c_296,plain,
! [A_21,B_22] : ( double_divide(double_divide(A_21,multiply(double_divide(A_21,inverse(identity)),B_22)),inverse(identity)) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_6,c_283]) ).
tff(c_1206,plain,
! [A_21,B_22] : ( double_divide(double_divide(A_21,multiply(double_divide(A_21,identity),B_22)),identity) = B_22 ),
inference(demodulation,[status(thm),theory(equality)],[c_1184,c_1184,c_296]) ).
tff(c_2063,plain,
! [A_71,B_72] : ( multiply(multiply(inverse(A_71),B_72),A_71) = B_72 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_6,c_6,c_1206]) ).
tff(c_2133,plain,
! [B_73,A_74] : ( multiply(B_73,double_divide(B_73,inverse(A_74))) = A_74 ),
inference(superposition,[status(thm),theory(equality)],[c_2063,c_1238]) ).
tff(c_2150,plain,
! [A_74,B_73] : ( multiply(A_74,inverse(B_73)) = double_divide(B_73,inverse(A_74)) ),
inference(superposition,[status(thm),theory(equality)],[c_2133,c_1727]) ).
tff(c_3429,plain,
! [B_2,B_22] : ( double_divide(inverse(B_2),multiply(B_2,B_22)) = inverse(B_22) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_3390]) ).
tff(c_4852,plain,
! [B_2,B_22] : ( double_divide(inverse(B_2),inverse(B_22)) = multiply(B_2,B_22) ),
inference(superposition,[status(thm),theory(equality)],[c_3429,c_4763]) ).
tff(c_14070,plain,
! [B_194,A_195,B_196] : ( multiply(multiply(double_divide(B_194,A_195),B_196),multiply(A_195,B_194)) = B_196 ),
inference(superposition,[status(thm),theory(equality)],[c_37,c_1728]) ).
tff(c_15436,plain,
! [B_204,B_205,A_206] : ( multiply(B_204,double_divide(B_204,double_divide(B_205,A_206))) = multiply(A_206,B_205) ),
inference(superposition,[status(thm),theory(equality)],[c_14070,c_1238]) ).
tff(c_16113,plain,
! [B_209,A_210,B_211] : ( multiply(double_divide(double_divide(B_209,A_210),B_211),B_211) = multiply(A_210,B_209) ),
inference(superposition,[status(thm),theory(equality)],[c_2445,c_15436]) ).
tff(c_16219,plain,
! [A_210,B_209,B_211] : ( multiply(multiply(A_210,B_209),inverse(double_divide(double_divide(B_209,A_210),B_211))) = B_211 ),
inference(superposition,[status(thm),theory(equality)],[c_16113,c_1727]) ).
tff(c_20520,plain,
! [A_239,B_240,B_241] : ( multiply(multiply(A_239,B_240),multiply(B_241,double_divide(B_240,A_239))) = B_241 ),
inference(demodulation,[status(thm),theory(equality)],[c_37,c_16219]) ).
tff(c_20763,plain,
! [B_22,B_2,B_241] : ( multiply(multiply(inverse(B_22),inverse(B_2)),multiply(B_241,multiply(B_2,B_22))) = B_241 ),
inference(superposition,[status(thm),theory(equality)],[c_4852,c_20520]) ).
tff(c_24132,plain,
! [B_259,B_260,B_261] : ( multiply(double_divide(B_259,B_260),multiply(B_261,multiply(B_259,B_260))) = B_261 ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_2150,c_20763]) ).
tff(c_24223,plain,
! [B_259,B_260,B_261] : ( double_divide(inverse(double_divide(B_259,B_260)),B_261) = inverse(multiply(B_261,multiply(B_259,B_260))) ),
inference(superposition,[status(thm),theory(equality)],[c_24132,c_3429]) ).
tff(c_24643,plain,
! [B_260,B_259,B_261] : ( double_divide(multiply(B_260,B_259),B_261) = double_divide(multiply(B_259,B_260),B_261) ),
inference(demodulation,[status(thm),theory(equality)],[c_1445,c_37,c_24223]) ).
tff(c_135396,plain,
! [B_577,B_576,B_578] : ( double_divide(B_577,multiply(B_576,B_578)) = double_divide(B_576,multiply(B_577,B_578)) ),
inference(demodulation,[status(thm),theory(equality)],[c_102802,c_102802,c_24643]) ).
tff(c_136624,plain,
! [B_576,B_577,B_578] : ( double_divide(double_divide(B_576,multiply(B_577,B_578)),identity) = multiply(multiply(B_576,B_578),B_577) ),
inference(superposition,[status(thm),theory(equality)],[c_135396,c_4]) ).
tff(c_137636,plain,
! [B_578,B_576,B_577] : ( multiply(B_578,multiply(B_576,B_577)) = multiply(B_576,multiply(B_577,B_578)) ),
inference(demodulation,[status(thm),theory(equality)],[c_113497,c_5279,c_136624]) ).
tff(c_116920,plain,
! [B_527,B_528,B_529] : ( double_divide(multiply(B_527,B_528),B_529) = double_divide(B_528,multiply(B_527,B_529)) ),
inference(superposition,[status(thm),theory(equality)],[c_102456,c_4748]) ).
tff(c_123133,plain,
! [B_545,B_546,B_547] : ( double_divide(double_divide(B_545,multiply(B_546,B_547)),identity) = multiply(B_547,multiply(B_546,B_545)) ),
inference(superposition,[status(thm),theory(equality)],[c_116920,c_4]) ).
tff(c_123446,plain,
! [B_547,B_546,B_545] : ( multiply(B_547,multiply(B_546,B_545)) = multiply(B_545,multiply(B_546,B_547)) ),
inference(superposition,[status(thm),theory(equality)],[c_123133,c_5279]) ).
tff(c_10,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_5629,plain,
multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_5594,c_10]) ).
tff(c_131454,plain,
multiply(b3,multiply(a3,c3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_123446,c_5629]) ).
tff(c_141117,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_137636,c_131454]) ).
tff(c_141120,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5594,c_141117]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP567-1 : TPTP v9.0.0. Released v2.6.0.
% 0.04/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.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:56:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 33.07/20.22 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.16/20.24
% 33.16/20.24 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------