%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP777-10 : TPTP v9.0.0. Released v8.1.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 : n002.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:27:10 PM UTC 2025
% Result : Unsatisfiable 45.85s 30.18s
% Output : CNFRefutation 46.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 10
% Syntax : Number of formulae : 183 ( 183 unt; 0 typ; 0 def)
% Number of atoms : 183 ( 182 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 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 : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 265 ( 265 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ bigC > quotient > product > difference > #nlpp > x0 > c > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(b,type,
b: $i ).
tff(product,type,
product: ( $i * $i ) > $i ).
tff(bigC,type,
bigC: ( $i * $i * $i ) > $i ).
tff(quotient,type,
quotient: ( $i * $i ) > $i ).
tff(difference,type,
difference: ( $i * $i ) > $i ).
tff(x0,type,
x0: $i ).
tff(c,type,
c: $i ).
tff(f_39,axiom,
! [A,B,C] : ( bigC(A,B,C) = product(product(A,B),product(C,A)) ),
file(unknown,unknown) ).
tff(f_32,axiom,
! [A,B,C,D] : ( product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)) ),
file(unknown,unknown) ).
tff(f_34,axiom,
! [A] : ( product(A,A) = A ),
file(unknown,unknown) ).
tff(f_40,axiom,
product(product(a,c),product(c,b)) = product(a,b),
file(unknown,unknown) ).
tff(f_24,axiom,
! [A,B] : ( difference(A,product(A,B)) = B ),
file(unknown,unknown) ).
tff(f_28,axiom,
! [A,B] : ( quotient(product(A,B),B) = A ),
file(unknown,unknown) ).
tff(f_30,axiom,
! [A,B] : ( product(quotient(A,B),B) = A ),
file(unknown,unknown) ).
tff(f_26,axiom,
! [A,B] : ( product(A,difference(A,B)) = B ),
file(unknown,unknown) ).
tff(f_37,axiom,
! [A,B] : ( product(product(product(A,B),B),product(B,product(B,A))) = B ),
file(unknown,unknown) ).
tff(f_42,axiom,
bigC(a,b,x0) != bigC(c,c,x0),
file(unknown,unknown) ).
tff(c_16,plain,
! [A_16,B_17,C_18] : ( product(product(A_16,B_17),product(C_18,A_16)) = bigC(A_16,B_17,C_18) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_365,plain,
! [A_40,C_41,B_42,D_43] : ( product(product(A_40,C_41),product(B_42,D_43)) = product(product(A_40,B_42),product(C_41,D_43)) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_874,plain,
! [A_52,C_53,B_54] : ( product(product(A_52,C_53),product(B_54,A_52)) = bigC(A_52,B_54,C_53) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_365]) ).
tff(c_937,plain,
! [A_52,C_53,B_54] : ( bigC(A_52,C_53,B_54) = bigC(A_52,B_54,C_53) ),
inference(superposition,[status(thm),theory(equality)],[c_874,c_16]) ).
tff(c_12,plain,
! [A_13] : ( product(A_13,A_13) = A_13 ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_204,plain,
! [A_34,B_35,C_36] : ( product(product(A_34,B_35),product(C_36,A_34)) = bigC(A_34,B_35,C_36) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_253,plain,
! [A_13,C_36] : ( product(A_13,product(C_36,A_13)) = bigC(A_13,A_13,C_36) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_204]) ).
tff(c_18,plain,
product(product(a,c),product(c,b)) = product(a,b),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_2,plain,
! [A_1,B_2] : ( difference(A_1,product(A_1,B_2)) = B_2 ),
inference(cnfTransformation,[status(thm)],[f_24]) ).
tff(c_173,plain,
difference(product(a,c),product(a,b)) = product(c,b),
inference(superposition,[status(thm),theory(equality)],[c_18,c_2]) ).
tff(c_4266,plain,
! [A_126,B_127,D_128] : ( product(product(A_126,B_127),product(A_126,D_128)) = product(A_126,product(B_127,D_128)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_365]) ).
tff(c_6,plain,
! [A_5,B_6] : ( quotient(product(A_5,B_6),B_6) = A_5 ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_4389,plain,
! [A_126,B_127,D_128] : ( quotient(product(A_126,product(B_127,D_128)),product(A_126,D_128)) = product(A_126,B_127) ),
inference(superposition,[status(thm),theory(equality)],[c_4266,c_6]) ).
tff(c_8,plain,
! [A_7,B_8] : ( product(quotient(A_7,B_8),B_8) = A_7 ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_9300,plain,
! [A_184,B_185,C_186,D_187] : ( product(product(quotient(A_184,B_185),C_186),product(B_185,D_187)) = product(A_184,product(C_186,D_187)) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_365]) ).
tff(c_10101,plain,
! [A_192,A_193,C_194] : ( product(product(quotient(A_192,A_193),C_194),A_193) = product(A_192,product(C_194,A_193)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_9300]) ).
tff(c_32887,plain,
! [A_338,C_339,A_340] : ( quotient(product(A_338,product(C_339,A_340)),A_340) = product(quotient(A_338,A_340),C_339) ),
inference(superposition,[status(thm),theory(equality)],[c_10101,c_6]) ).
tff(c_33294,plain,
product(quotient(product(a,c),b),c) = quotient(product(a,b),b),
inference(superposition,[status(thm),theory(equality)],[c_18,c_32887]) ).
tff(c_33334,plain,
product(quotient(product(a,c),b),c) = a,
inference(demodulation,[status(thm),theory(equality)],[c_6,c_33294]) ).
tff(c_33565,plain,
quotient(product(a,c),b) = quotient(a,c),
inference(superposition,[status(thm),theory(equality)],[c_33334,c_6]) ).
tff(c_34492,plain,
product(quotient(a,c),b) = product(a,c),
inference(superposition,[status(thm),theory(equality)],[c_33565,c_8]) ).
tff(c_9669,plain,
! [A_184,A_13,C_186] : ( product(product(quotient(A_184,A_13),C_186),A_13) = product(A_184,product(C_186,A_13)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_9300]) ).
tff(c_34707,plain,
product(product(a,c),c) = product(a,product(b,c)),
inference(superposition,[status(thm),theory(equality)],[c_34492,c_9669]) ).
tff(c_3855,plain,
! [A_120,A_121,B_122] : ( product(product(A_120,A_121),product(B_122,A_121)) = product(product(A_120,B_122),A_121) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_365]) ).
tff(c_3965,plain,
! [A_120,A_121,B_122] : ( difference(product(A_120,A_121),product(product(A_120,B_122),A_121)) = product(B_122,A_121) ),
inference(superposition,[status(thm),theory(equality)],[c_3855,c_2]) ).
tff(c_34932,plain,
difference(product(a,c),product(a,product(b,c))) = product(c,c),
inference(superposition,[status(thm),theory(equality)],[c_34707,c_3965]) ).
tff(c_35107,plain,
difference(product(a,c),product(a,product(b,c))) = c,
inference(demodulation,[status(thm),theory(equality)],[c_12,c_34932]) ).
tff(c_4,plain,
! [A_3,B_4] : ( product(A_3,difference(A_3,B_4)) = B_4 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_1169,plain,
! [A_62,C_63] : ( product(product(A_62,C_63),A_62) = bigC(A_62,A_62,C_63) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_874]) ).
tff(c_1282,plain,
! [A_3,B_4] : ( bigC(A_3,A_3,difference(A_3,B_4)) = product(B_4,A_3) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1169]) ).
tff(c_1848,plain,
! [A_80,B_81,C_82] : ( difference(product(A_80,B_81),bigC(A_80,B_81,C_82)) = product(C_82,A_80) ),
inference(superposition,[status(thm),theory(equality)],[c_204,c_2]) ).
tff(c_1873,plain,
! [A_3,B_4] : ( difference(product(A_3,A_3),product(B_4,A_3)) = product(difference(A_3,B_4),A_3) ),
inference(superposition,[status(thm),theory(equality)],[c_1282,c_1848]) ).
tff(c_2269,plain,
! [A_90,B_91] : ( product(difference(A_90,B_91),A_90) = difference(A_90,product(B_91,A_90)) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_1873]) ).
tff(c_2780,plain,
! [A_101,B_102] : ( difference(difference(A_101,B_102),difference(A_101,product(B_102,A_101))) = A_101 ),
inference(superposition,[status(thm),theory(equality)],[c_2269,c_2]) ).
tff(c_2879,plain,
! [B_8,A_7] : ( difference(difference(B_8,quotient(A_7,B_8)),difference(B_8,A_7)) = B_8 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_2780]) ).
tff(c_35201,plain,
difference(difference(product(a,c),quotient(product(a,product(b,c)),product(a,c))),c) = product(a,c),
inference(superposition,[status(thm),theory(equality)],[c_35107,c_2879]) ).
tff(c_35237,plain,
difference(product(c,b),c) = product(a,c),
inference(demodulation,[status(thm),theory(equality)],[c_173,c_4389,c_35201]) ).
tff(c_51,plain,
! [A_23,B_24] : ( product(A_23,difference(A_23,B_24)) = B_24 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_57,plain,
! [B_24,A_23] : ( quotient(B_24,difference(A_23,B_24)) = A_23 ),
inference(superposition,[status(thm),theory(equality)],[c_51,c_6]) ).
tff(c_265,plain,
! [A_37,B_38] : ( product(product(product(A_37,B_38),B_38),product(B_38,product(B_38,A_37))) = B_38 ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_5762,plain,
! [A_144,B_145] : ( difference(product(product(A_144,B_145),B_145),B_145) = product(B_145,product(B_145,A_144)) ),
inference(superposition,[status(thm),theory(equality)],[c_265,c_2]) ).
tff(c_5880,plain,
! [B_8,A_7] : ( product(B_8,product(B_8,quotient(A_7,B_8))) = difference(product(A_7,B_8),B_8) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_5762]) ).
tff(c_1297,plain,
! [A_64,B_65] : ( product(A_64,product(B_65,A_64)) = bigC(A_64,B_65,A_64) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_874]) ).
tff(c_1413,plain,
! [B_8,A_7] : ( bigC(B_8,quotient(A_7,B_8),B_8) = product(B_8,A_7) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_1297]) ).
tff(c_2066,plain,
! [A_85,B_86,C_87] : ( quotient(bigC(A_85,B_86,C_87),product(C_87,A_85)) = product(A_85,B_86) ),
inference(superposition,[status(thm),theory(equality)],[c_204,c_6]) ).
tff(c_2102,plain,
! [B_8,A_7] : ( quotient(product(B_8,A_7),product(B_8,B_8)) = product(B_8,quotient(A_7,B_8)) ),
inference(superposition,[status(thm),theory(equality)],[c_1413,c_2066]) ).
tff(c_2168,plain,
! [B_8,A_7] : ( quotient(product(B_8,A_7),B_8) = product(B_8,quotient(A_7,B_8)) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_2102]) ).
tff(c_6125,plain,
! [B_148,A_149] : ( product(B_148,product(B_148,quotient(A_149,B_148))) = difference(product(A_149,B_148),B_148) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_5762]) ).
tff(c_696,plain,
! [A_46,C_47] : ( product(A_46,product(C_47,A_46)) = bigC(A_46,A_46,C_47) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_204]) ).
tff(c_782,plain,
! [B_8,A_7] : ( bigC(B_8,B_8,quotient(A_7,B_8)) = product(B_8,A_7) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_696]) ).
tff(c_1946,plain,
! [A_83,C_84] : ( difference(product(A_83,C_84),bigC(A_83,A_83,C_84)) = A_83 ),
inference(superposition,[status(thm),theory(equality)],[c_1169,c_2]) ).
tff(c_1999,plain,
! [B_8,A_7] : ( difference(product(B_8,quotient(A_7,B_8)),product(B_8,A_7)) = B_8 ),
inference(superposition,[status(thm),theory(equality)],[c_782,c_1946]) ).
tff(c_6173,plain,
! [B_148,A_149] : ( difference(product(B_148,quotient(product(B_148,quotient(A_149,B_148)),B_148)),difference(product(A_149,B_148),B_148)) = B_148 ),
inference(superposition,[status(thm),theory(equality)],[c_6125,c_1999]) ).
tff(c_6430,plain,
! [A_152,B_153] : ( difference(difference(A_152,B_153),difference(product(A_152,B_153),B_153)) = B_153 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_5880,c_2168,c_6173]) ).
tff(c_7240,plain,
! [A_161,B_162] : ( difference(difference(quotient(A_161,B_162),B_162),difference(A_161,B_162)) = B_162 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_6430]) ).
tff(c_7288,plain,
! [A_161,B_162] : ( product(difference(quotient(A_161,B_162),B_162),B_162) = difference(A_161,B_162) ),
inference(superposition,[status(thm),theory(equality)],[c_7240,c_4]) ).
tff(c_13696,plain,
! [A_223,B_224,D_225] : ( product(A_223,product(difference(A_223,B_224),D_225)) = product(B_224,product(A_223,D_225)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4266]) ).
tff(c_13966,plain,
! [A_161,B_162] : ( product(quotient(A_161,B_162),difference(A_161,B_162)) = product(B_162,product(quotient(A_161,B_162),B_162)) ),
inference(superposition,[status(thm),theory(equality)],[c_7288,c_13696]) ).
tff(c_14103,plain,
! [A_226,B_227] : ( product(quotient(A_226,B_227),difference(A_226,B_227)) = product(B_227,A_226) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_13966]) ).
tff(c_4526,plain,
! [A_3,B_127,B_4] : ( product(A_3,product(B_127,difference(A_3,B_4))) = product(product(A_3,B_127),B_4) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4266]) ).
tff(c_14127,plain,
! [A_226,B_227] : ( product(product(A_226,quotient(A_226,B_227)),B_227) = product(A_226,product(B_227,A_226)) ),
inference(superposition,[status(thm),theory(equality)],[c_14103,c_4526]) ).
tff(c_17251,plain,
! [A_246,B_247] : ( product(product(A_246,quotient(A_246,B_247)),B_247) = bigC(A_246,A_246,B_247) ),
inference(demodulation,[status(thm),theory(equality)],[c_253,c_14127]) ).
tff(c_17521,plain,
! [A_246,B_247] : ( quotient(bigC(A_246,A_246,B_247),B_247) = product(A_246,quotient(A_246,B_247)) ),
inference(superposition,[status(thm),theory(equality)],[c_17251,c_6]) ).
tff(c_1031,plain,
! [A_13,C_53] : ( product(product(A_13,C_53),A_13) = bigC(A_13,A_13,C_53) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_874]) ).
tff(c_14681,plain,
! [B_230,A_231] : ( quotient(product(B_230,A_231),difference(A_231,B_230)) = quotient(A_231,B_230) ),
inference(superposition,[status(thm),theory(equality)],[c_14103,c_6]) ).
tff(c_14882,plain,
! [A_13,C_53] : ( quotient(bigC(A_13,A_13,C_53),difference(A_13,product(A_13,C_53))) = quotient(A_13,product(A_13,C_53)) ),
inference(superposition,[status(thm),theory(equality)],[c_1031,c_14681]) ).
tff(c_14950,plain,
! [A_13,C_53] : ( quotient(bigC(A_13,A_13,C_53),C_53) = quotient(A_13,product(A_13,C_53)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_14882]) ).
tff(c_22237,plain,
! [A_282,C_283] : ( quotient(A_282,product(A_282,C_283)) = product(A_282,quotient(A_282,C_283)) ),
inference(demodulation,[status(thm),theory(equality)],[c_17521,c_14950]) ).
tff(c_83,plain,
! [A_27,B_28] : ( product(quotient(A_27,B_28),B_28) = A_27 ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_89,plain,
! [A_27,B_28] : ( difference(quotient(A_27,B_28),A_27) = B_28 ),
inference(superposition,[status(thm),theory(equality)],[c_83,c_2]) ).
tff(c_22891,plain,
! [A_286,C_287] : ( difference(product(A_286,quotient(A_286,C_287)),A_286) = product(A_286,C_287) ),
inference(superposition,[status(thm),theory(equality)],[c_22237,c_89]) ).
tff(c_23053,plain,
! [B_24,A_23] : ( product(B_24,difference(A_23,B_24)) = difference(product(B_24,A_23),B_24) ),
inference(superposition,[status(thm),theory(equality)],[c_57,c_22891]) ).
tff(c_35631,plain,
product(product(c,b),product(a,c)) = c,
inference(superposition,[status(thm),theory(equality)],[c_35237,c_4]) ).
tff(c_450,plain,
! [A_40,C_41,B_42,D_43] : ( quotient(product(product(A_40,C_41),product(B_42,D_43)),product(C_41,D_43)) = product(A_40,B_42) ),
inference(superposition,[status(thm),theory(equality)],[c_365,c_6]) ).
tff(c_36040,plain,
quotient(c,product(b,c)) = product(c,a),
inference(superposition,[status(thm),theory(equality)],[c_35631,c_450]) ).
tff(c_6170,plain,
! [B_148,A_149] : ( product(B_148,quotient(product(B_148,quotient(A_149,B_148)),B_148)) = quotient(difference(product(A_149,B_148),B_148),B_148) ),
inference(superposition,[status(thm),theory(equality)],[c_6125,c_2168]) ).
tff(c_6313,plain,
! [A_150,B_151] : ( quotient(difference(product(A_150,B_151),B_151),B_151) = difference(A_150,B_151) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_5880,c_2168,c_6170]) ).
tff(c_7124,plain,
! [A_159,B_160] : ( quotient(difference(A_159,B_160),B_160) = difference(quotient(A_159,B_160),B_160) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_6313]) ).
tff(c_7959,plain,
! [A_171,B_172] : ( difference(quotient(quotient(A_171,B_172),A_171),A_171) = quotient(B_172,A_171) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_7124]) ).
tff(c_8010,plain,
! [A_171,B_172] : ( quotient(quotient(A_171,B_172),A_171) = quotient(A_171,quotient(B_172,A_171)) ),
inference(superposition,[status(thm),theory(equality)],[c_7959,c_57]) ).
tff(c_37713,plain,
quotient(c,quotient(product(b,c),c)) = quotient(product(c,a),c),
inference(superposition,[status(thm),theory(equality)],[c_36040,c_8010]) ).
tff(c_37786,plain,
product(c,quotient(a,c)) = quotient(c,b),
inference(demodulation,[status(thm),theory(equality)],[c_2168,c_6,c_37713]) ).
tff(c_2391,plain,
! [B_92,A_93] : ( quotient(product(B_92,A_93),B_92) = product(B_92,quotient(A_93,B_92)) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_2102]) ).
tff(c_2647,plain,
! [A_99,B_100] : ( product(A_99,quotient(difference(A_99,B_100),A_99)) = quotient(B_100,A_99) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2391]) ).
tff(c_2725,plain,
! [A_99,B_100] : ( quotient(difference(A_99,B_100),A_99) = difference(A_99,quotient(B_100,A_99)) ),
inference(superposition,[status(thm),theory(equality)],[c_2647,c_2]) ).
tff(c_24823,plain,
! [B_296,A_297] : ( product(B_296,difference(A_297,B_296)) = difference(product(B_296,A_297),B_296) ),
inference(superposition,[status(thm),theory(equality)],[c_57,c_22891]) ).
tff(c_25078,plain,
! [B_296,A_297] : ( difference(B_296,difference(product(B_296,A_297),B_296)) = difference(A_297,B_296) ),
inference(superposition,[status(thm),theory(equality)],[c_24823,c_2]) ).
tff(c_35553,plain,
difference(c,product(a,c)) = difference(b,c),
inference(superposition,[status(thm),theory(equality)],[c_35237,c_25078]) ).
tff(c_2341,plain,
! [A_90,B_91] : ( quotient(difference(A_90,product(B_91,A_90)),A_90) = difference(A_90,B_91) ),
inference(superposition,[status(thm),theory(equality)],[c_2269,c_6]) ).
tff(c_44694,plain,
quotient(difference(b,c),c) = difference(c,a),
inference(superposition,[status(thm),theory(equality)],[c_35553,c_2341]) ).
tff(c_5062,plain,
! [A_138,B_139] : ( product(product(A_138,B_139),product(B_139,product(B_139,quotient(A_138,B_139)))) = B_139 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_265]) ).
tff(c_5912,plain,
! [A_146,B_147] : ( product(A_146,product(B_147,product(B_147,quotient(quotient(A_146,B_147),B_147)))) = B_147 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_5062]) ).
tff(c_6043,plain,
! [B_147,A_146] : ( product(B_147,product(B_147,quotient(quotient(A_146,B_147),B_147))) = difference(A_146,B_147) ),
inference(superposition,[status(thm),theory(equality)],[c_5912,c_2]) ).
tff(c_45929,plain,
product(c,product(c,quotient(difference(c,a),c))) = difference(difference(b,c),c),
inference(superposition,[status(thm),theory(equality)],[c_44694,c_6043]) ).
tff(c_46049,plain,
difference(difference(b,c),c) = quotient(c,b),
inference(demodulation,[status(thm),theory(equality)],[c_37786,c_4,c_2725,c_45929]) ).
tff(c_54421,plain,
product(difference(b,c),quotient(c,b)) = c,
inference(superposition,[status(thm),theory(equality)],[c_46049,c_4]) ).
tff(c_54418,plain,
quotient(c,quotient(c,b)) = difference(b,c),
inference(superposition,[status(thm),theory(equality)],[c_46049,c_57]) ).
tff(c_9169,plain,
! [A_182,B_183] : ( quotient(quotient(A_182,B_183),A_182) = quotient(A_182,quotient(B_183,A_182)) ),
inference(superposition,[status(thm),theory(equality)],[c_7959,c_57]) ).
tff(c_9226,plain,
! [A_182,B_183] : ( difference(quotient(A_182,quotient(B_183,A_182)),quotient(A_182,B_183)) = A_182 ),
inference(superposition,[status(thm),theory(equality)],[c_9169,c_89]) ).
tff(c_37704,plain,
difference(quotient(c,quotient(product(b,c),c)),product(c,a)) = c,
inference(superposition,[status(thm),theory(equality)],[c_36040,c_9226]) ).
tff(c_37784,plain,
difference(quotient(c,b),product(c,a)) = c,
inference(demodulation,[status(thm),theory(equality)],[c_6,c_37704]) ).
tff(c_7404,plain,
! [B_163,A_164] : ( difference(B_163,difference(product(quotient(A_164,B_163),A_164),A_164)) = A_164 ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_6430]) ).
tff(c_7452,plain,
! [A_164,B_163] : ( difference(product(quotient(A_164,B_163),A_164),A_164) = product(B_163,A_164) ),
inference(superposition,[status(thm),theory(equality)],[c_7404,c_4]) ).
tff(c_6355,plain,
! [A_150,B_151] : ( product(difference(A_150,B_151),B_151) = difference(product(A_150,B_151),B_151) ),
inference(superposition,[status(thm),theory(equality)],[c_6313,c_8]) ).
tff(c_13975,plain,
! [A_150,B_151] : ( product(A_150,difference(product(A_150,B_151),B_151)) = product(B_151,product(A_150,B_151)) ),
inference(superposition,[status(thm),theory(equality)],[c_6355,c_13696]) ).
tff(c_14960,plain,
! [A_232,B_233] : ( product(A_232,difference(product(A_232,B_233),B_233)) = bigC(B_233,B_233,A_232) ),
inference(demodulation,[status(thm),theory(equality)],[c_253,c_13975]) ).
tff(c_15158,plain,
! [A_232,B_233] : ( difference(product(A_232,B_233),B_233) = difference(A_232,bigC(B_233,B_233,A_232)) ),
inference(superposition,[status(thm),theory(equality)],[c_14960,c_2]) ).
tff(c_7521,plain,
! [A_165,B_166] : ( difference(product(quotient(A_165,B_166),A_165),A_165) = product(B_166,A_165) ),
inference(superposition,[status(thm),theory(equality)],[c_7404,c_4]) ).
tff(c_7572,plain,
! [A_165,B_166] : ( quotient(A_165,product(B_166,A_165)) = product(quotient(A_165,B_166),A_165) ),
inference(superposition,[status(thm),theory(equality)],[c_7521,c_57]) ).
tff(c_35198,plain,
difference(product(a,c),quotient(product(a,product(b,c)),product(a,c))) = quotient(c,product(a,c)),
inference(superposition,[status(thm),theory(equality)],[c_35107,c_2725]) ).
tff(c_35236,plain,
product(quotient(c,a),c) = product(c,b),
inference(demodulation,[status(thm),theory(equality)],[c_173,c_4389,c_7572,c_35198]) ).
tff(c_15293,plain,
! [A_234,B_235] : ( difference(product(A_234,B_235),B_235) = difference(A_234,bigC(B_235,B_235,A_234)) ),
inference(superposition,[status(thm),theory(equality)],[c_14960,c_2]) ).
tff(c_15434,plain,
! [A_234,B_235] : ( product(product(A_234,B_235),difference(A_234,bigC(B_235,B_235,A_234))) = B_235 ),
inference(superposition,[status(thm),theory(equality)],[c_15293,c_4]) ).
tff(c_35292,plain,
product(product(c,b),difference(quotient(c,a),bigC(c,c,quotient(c,a)))) = c,
inference(superposition,[status(thm),theory(equality)],[c_35236,c_15434]) ).
tff(c_35491,plain,
bigC(c,a,b) = c,
inference(demodulation,[status(thm),theory(equality)],[c_937,c_16,c_7452,c_15158,c_35292]) ).
tff(c_10,plain,
! [A_9,C_11,B_10,D_12] : ( product(product(A_9,C_11),product(B_10,D_12)) = product(product(A_9,B_10),product(C_11,D_12)) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_323,plain,
product(product(product(product(c,b),product(a,c)),product(a,c)),product(product(a,c),product(a,b))) = product(a,c),
inference(superposition,[status(thm),theory(equality)],[c_18,c_265]) ).
tff(c_351,plain,
product(product(bigC(c,b,a),product(a,c)),product(product(a,c),product(a,b))) = product(a,c),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_323]) ).
tff(c_44167,plain,
product(product(c,a),product(a,b)) = product(a,c),
inference(demodulation,[status(thm),theory(equality)],[c_35491,c_937,c_18,c_10,c_12,c_10,c_351]) ).
tff(c_60751,plain,
! [A_381,B_382,D_383] : ( difference(A_381,product(B_382,product(A_381,D_383))) = product(difference(A_381,B_382),D_383) ),
inference(superposition,[status(thm),theory(equality)],[c_13696,c_2]) ).
tff(c_60938,plain,
product(difference(a,product(c,a)),b) = difference(a,product(a,c)),
inference(superposition,[status(thm),theory(equality)],[c_44167,c_60751]) ).
tff(c_61317,plain,
product(difference(a,product(c,a)),b) = c,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_60938]) ).
tff(c_61625,plain,
difference(a,product(c,a)) = quotient(c,b),
inference(superposition,[status(thm),theory(equality)],[c_61317,c_6]) ).
tff(c_61874,plain,
product(a,quotient(c,b)) = product(c,a),
inference(superposition,[status(thm),theory(equality)],[c_61625,c_4]) ).
tff(c_62380,plain,
quotient(difference(quotient(c,b),product(c,a)),quotient(c,b)) = difference(quotient(c,b),a),
inference(superposition,[status(thm),theory(equality)],[c_61874,c_2341]) ).
tff(c_62485,plain,
difference(quotient(c,b),a) = difference(b,c),
inference(demodulation,[status(thm),theory(equality)],[c_54418,c_37784,c_62380]) ).
tff(c_64098,plain,
quotient(a,difference(b,c)) = quotient(c,b),
inference(superposition,[status(thm),theory(equality)],[c_62485,c_57]) ).
tff(c_2175,plain,
! [B_88,A_89] : ( difference(product(B_88,quotient(A_89,B_88)),product(B_88,A_89)) = B_88 ),
inference(superposition,[status(thm),theory(equality)],[c_782,c_1946]) ).
tff(c_2190,plain,
! [B_88,A_89] : ( product(product(B_88,quotient(A_89,B_88)),B_88) = product(B_88,A_89) ),
inference(superposition,[status(thm),theory(equality)],[c_2175,c_4]) ).
tff(c_64226,plain,
product(product(difference(b,c),quotient(c,b)),difference(b,c)) = product(difference(b,c),a),
inference(superposition,[status(thm),theory(equality)],[c_64098,c_2190]) ).
tff(c_64256,plain,
product(difference(b,c),a) = product(a,c),
inference(demodulation,[status(thm),theory(equality)],[c_35237,c_23053,c_54421,c_64226]) ).
tff(c_64903,plain,
quotient(product(a,c),a) = difference(b,c),
inference(superposition,[status(thm),theory(equality)],[c_64256,c_6]) ).
tff(c_67038,plain,
product(a,quotient(c,a)) = difference(b,c),
inference(superposition,[status(thm),theory(equality)],[c_64903,c_2168]) ).
tff(c_579,plain,
! [A_40,A_13,B_42] : ( product(product(A_40,A_13),product(B_42,A_13)) = product(product(A_40,B_42),A_13) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_365]) ).
tff(c_35022,plain,
quotient(product(a,product(b,c)),product(a,c)) = product(product(a,c),quotient(c,product(a,c))),
inference(superposition,[status(thm),theory(equality)],[c_34707,c_2168]) ).
tff(c_35119,plain,
product(product(a,quotient(c,a)),c) = product(a,b),
inference(demodulation,[status(thm),theory(equality)],[c_4389,c_579,c_7572,c_35022]) ).
tff(c_68033,plain,
product(difference(b,c),c) = product(a,b),
inference(demodulation,[status(thm),theory(equality)],[c_67038,c_35119]) ).
tff(c_554,plain,
! [A_3,B_42,B_4,D_43] : ( product(product(A_3,B_42),product(difference(A_3,B_4),D_43)) = product(B_4,product(B_42,D_43)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_365]) ).
tff(c_68557,plain,
! [B_42] : ( product(product(b,B_42),product(a,b)) = product(c,product(B_42,c)) ),
inference(superposition,[status(thm),theory(equality)],[c_68033,c_554]) ).
tff(c_71815,plain,
! [B_398] : ( bigC(c,c,B_398) = bigC(b,B_398,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_253,c_16,c_68557]) ).
tff(c_71992,plain,
! [B_54] : ( bigC(c,B_54,c) = bigC(b,B_54,a) ),
inference(superposition,[status(thm),theory(equality)],[c_937,c_71815]) ).
tff(c_256,plain,
! [A_13,B_35] : ( product(product(A_13,B_35),A_13) = bigC(A_13,B_35,A_13) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_204]) ).
tff(c_22056,plain,
! [A_13,C_53] : ( quotient(A_13,product(A_13,C_53)) = product(A_13,quotient(A_13,C_53)) ),
inference(demodulation,[status(thm),theory(equality)],[c_17521,c_14950]) ).
tff(c_37774,plain,
product(quotient(c,b),c) = product(c,a),
inference(superposition,[status(thm),theory(equality)],[c_7572,c_36040]) ).
tff(c_55731,plain,
quotient(product(a,b),c) = product(a,quotient(c,a)),
inference(superposition,[status(thm),theory(equality)],[c_35119,c_6]) ).
tff(c_68031,plain,
quotient(product(a,b),c) = difference(b,c),
inference(demodulation,[status(thm),theory(equality)],[c_67038,c_55731]) ).
tff(c_69162,plain,
product(difference(difference(b,c),c),c) = difference(product(a,b),c),
inference(superposition,[status(thm),theory(equality)],[c_68031,c_7288]) ).
tff(c_69221,plain,
difference(product(a,b),c) = product(c,a),
inference(demodulation,[status(thm),theory(equality)],[c_37774,c_46049,c_69162]) ).
tff(c_72992,plain,
quotient(c,product(c,a)) = product(a,b),
inference(superposition,[status(thm),theory(equality)],[c_69221,c_57]) ).
tff(c_81642,plain,
product(c,quotient(c,a)) = product(a,b),
inference(superposition,[status(thm),theory(equality)],[c_22056,c_72992]) ).
tff(c_545,plain,
! [A_40,A_7,B_8,C_41] : ( product(product(A_40,quotient(A_7,B_8)),product(C_41,B_8)) = product(product(A_40,C_41),A_7) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_365]) ).
tff(c_82821,plain,
! [C_41] : ( product(product(a,b),product(C_41,a)) = product(product(c,C_41),c) ),
inference(superposition,[status(thm),theory(equality)],[c_81642,c_545]) ).
tff(c_83030,plain,
! [C_41] : ( bigC(b,C_41,a) = bigC(a,b,C_41) ),
inference(demodulation,[status(thm),theory(equality)],[c_71992,c_256,c_16,c_82821]) ).
tff(c_85679,plain,
! [B_54] : ( bigC(c,B_54,c) = bigC(a,b,B_54) ),
inference(demodulation,[status(thm),theory(equality)],[c_83030,c_71992]) ).
tff(c_599,plain,
! [A_44,B_45] : ( product(product(A_44,B_45),A_44) = bigC(A_44,B_45,A_44) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_204]) ).
tff(c_647,plain,
! [A_44,B_45] : ( quotient(bigC(A_44,B_45,A_44),A_44) = product(A_44,B_45) ),
inference(superposition,[status(thm),theory(equality)],[c_599,c_6]) ).
tff(c_4523,plain,
! [A_3,B_4,D_128] : ( product(A_3,product(difference(A_3,B_4),D_128)) = product(B_4,product(A_3,D_128)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_4266]) ).
tff(c_68581,plain,
product(c,product(b,c)) = product(b,product(a,b)),
inference(superposition,[status(thm),theory(equality)],[c_68033,c_4523]) ).
tff(c_68790,plain,
bigC(c,b,c) = bigC(b,a,b),
inference(demodulation,[status(thm),theory(equality)],[c_937,c_937,c_253,c_253,c_68581]) ).
tff(c_14397,plain,
! [A_1,B_2] : ( product(quotient(A_1,product(A_1,B_2)),B_2) = product(product(A_1,B_2),A_1) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_14103]) ).
tff(c_15815,plain,
! [A_238,B_239] : ( product(quotient(A_238,product(A_238,B_239)),B_239) = bigC(A_238,B_239,A_238) ),
inference(demodulation,[status(thm),theory(equality)],[c_256,c_14397]) ).
tff(c_16033,plain,
! [A_238,B_239] : ( quotient(bigC(A_238,B_239,A_238),B_239) = quotient(A_238,product(A_238,B_239)) ),
inference(superposition,[status(thm),theory(equality)],[c_15815,c_6]) ).
tff(c_22235,plain,
! [A_238,B_239] : ( quotient(bigC(A_238,B_239,A_238),B_239) = product(A_238,quotient(A_238,B_239)) ),
inference(demodulation,[status(thm),theory(equality)],[c_22056,c_16033]) ).
tff(c_72384,plain,
quotient(bigC(b,a,b),b) = product(c,quotient(c,b)),
inference(superposition,[status(thm),theory(equality)],[c_68790,c_22235]) ).
tff(c_72431,plain,
product(c,quotient(c,b)) = product(b,a),
inference(demodulation,[status(thm),theory(equality)],[c_647,c_72384]) ).
tff(c_73201,plain,
! [C_41] : ( product(product(b,a),product(C_41,b)) = product(product(c,C_41),c) ),
inference(superposition,[status(thm),theory(equality)],[c_72431,c_545]) ).
tff(c_73407,plain,
! [C_41] : ( bigC(c,C_41,c) = bigC(b,a,C_41) ),
inference(demodulation,[status(thm),theory(equality)],[c_256,c_16,c_73201]) ).
tff(c_86469,plain,
! [C_41] : ( bigC(b,a,C_41) = bigC(a,b,C_41) ),
inference(demodulation,[status(thm),theory(equality)],[c_85679,c_73407]) ).
tff(c_68784,plain,
! [B_42] : ( bigC(c,c,B_42) = bigC(b,B_42,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_253,c_16,c_68557]) ).
tff(c_20,plain,
bigC(c,c,x0) != bigC(a,b,x0),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_71813,plain,
bigC(b,x0,a) != bigC(a,b,x0),
inference(demodulation,[status(thm),theory(equality)],[c_68784,c_20]) ).
tff(c_71814,plain,
bigC(b,a,x0) != bigC(a,b,x0),
inference(demodulation,[status(thm),theory(equality)],[c_937,c_71813]) ).
tff(c_86693,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_86469,c_71814]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GRP777-10 : TPTP v9.0.0. Released v8.1.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n002.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 22:38:16 EDT 2025
% 0.14/0.34 % CPUTime :
% 45.85/30.18 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 45.85/30.20
% 45.85/30.20 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------