%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP660+1 : TPTP v9.0.0. Released v4.0.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 : n028.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:54 PM UTC 2025
% Result : Theorem 69.00s 37.14s
% Output : CNFRefutation 69.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 6
% Syntax : Number of formulae : 65 ( 63 unt; 0 typ; 0 def)
% Number of atoms : 67 ( 66 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 6 ( 4 ~; 1 |; 1 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 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 : 5 ( 5 usr; 0 con; 1-2 aty)
% Number of variables : 133 ( 132 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rd > mult > ld > #nlpp > #skF_2 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(ld,type,
ld: ( $i * $i ) > $i ).
tff(rd,type,
rd: ( $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(mult,type,
mult: ( $i * $i ) > $i ).
tff(f_30,axiom,
! [B,A] : ( ld(A,mult(A,B)) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
tff(f_34,axiom,
! [B,A] : ( rd(mult(A,B),B) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
tff(f_32,axiom,
! [B,A] : ( mult(rd(A,B),B) = A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
tff(f_36,axiom,
! [C,B,A] : ( mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
tff(f_28,axiom,
! [B,A] : ( mult(A,ld(A,B)) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
tff(f_42,negated_conjecture,
~ ? [X0] :
! [X1] :
( ( mult(X1,X0) = X1 )
& ( mult(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
tff(c_4,plain,
! [A_4,B_3] : ( ld(A_4,mult(A_4,B_3)) = B_3 ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_8,plain,
! [A_8,B_7] : ( rd(mult(A_8,B_7),B_7) = A_8 ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_6,plain,
! [A_6,B_5] : ( mult(rd(A_6,B_5),B_5) = A_6 ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_114,plain,
! [A_27,B_28,C_29] : ( mult(mult(mult(A_27,B_28),C_29),A_27) = mult(A_27,mult(B_28,mult(C_29,A_27))) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_200,plain,
! [A_33,B_34,C_35] : ( rd(mult(A_33,mult(B_34,mult(C_35,A_33))),A_33) = mult(mult(A_33,B_34),C_35) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_8]) ).
tff(c_833,plain,
! [B_57,B_58,A_59] : ( rd(mult(B_57,mult(B_58,A_59)),B_57) = mult(mult(B_57,B_58),rd(A_59,B_57)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_200]) ).
tff(c_910,plain,
! [B_57,A_6,B_5] : ( mult(mult(B_57,rd(A_6,B_5)),rd(B_5,B_57)) = rd(mult(B_57,A_6),B_57) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_833]) ).
tff(c_2,plain,
! [A_2,B_1] : ( mult(A_2,ld(A_2,B_1)) = B_1 ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_308,plain,
! [A_39,B_40,B_41] : ( mult(A_39,mult(B_40,mult(ld(mult(A_39,B_40),B_41),A_39))) = mult(B_41,A_39) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_114]) ).
tff(c_1066,plain,
! [B_63,A_64,B_65] : ( mult(B_63,mult(ld(mult(A_64,B_63),B_65),A_64)) = ld(A_64,mult(B_65,A_64)) ),
inference(superposition,[status(thm),theory(equality)],[c_308,c_4]) ).
tff(c_2228,plain,
! [A_90,B_91,B_92] : ( rd(ld(A_90,mult(B_91,A_90)),mult(ld(mult(A_90,B_92),B_91),A_90)) = B_92 ),
inference(superposition,[status(thm),theory(equality)],[c_1066,c_8]) ).
tff(c_2365,plain,
! [B_93,B_94] : ( rd(B_93,mult(ld(mult(B_93,B_94),B_93),B_93)) = B_94 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2228]) ).
tff(c_39,plain,
! [A_18,B_19] : ( ld(A_18,mult(A_18,B_19)) = B_19 ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_48,plain,
! [A_6,B_5] : ( ld(rd(A_6,B_5),A_6) = B_5 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_39]) ).
tff(c_2445,plain,
! [B_95,B_96] : ( mult(ld(mult(B_95,B_96),B_95),B_95) = ld(B_96,B_95) ),
inference(superposition,[status(thm),theory(equality)],[c_2365,c_48]) ).
tff(c_2562,plain,
! [B_96,B_95] : ( rd(ld(B_96,B_95),B_95) = ld(mult(B_95,B_96),B_95) ),
inference(superposition,[status(thm),theory(equality)],[c_2445,c_8]) ).
tff(c_234,plain,
! [A_36,B_37,C_38] : ( mult(A_36,mult(ld(A_36,B_37),mult(C_38,A_36))) = mult(mult(B_37,C_38),A_36) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_114]) ).
tff(c_462,plain,
! [A_45,B_46,C_47] : ( mult(ld(A_45,B_46),mult(C_47,A_45)) = ld(A_45,mult(mult(B_46,C_47),A_45)) ),
inference(superposition,[status(thm),theory(equality)],[c_234,c_4]) ).
tff(c_2080,plain,
! [A_87,B_88,C_89] : ( rd(ld(A_87,mult(mult(B_88,C_89),A_87)),mult(C_89,A_87)) = ld(A_87,B_88) ),
inference(superposition,[status(thm),theory(equality)],[c_462,c_8]) ).
tff(c_11717,plain,
! [A_204,A_205,B_206] : ( rd(ld(A_204,mult(A_205,A_204)),mult(B_206,A_204)) = ld(A_204,rd(A_205,B_206)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_2080]) ).
tff(c_17090,plain,
! [B_244,A_245,B_246] : ( rd(ld(B_244,A_245),mult(B_246,B_244)) = ld(B_244,rd(rd(A_245,B_244),B_246)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_11717]) ).
tff(c_17344,plain,
! [B_246,B_96] : ( ld(mult(mult(B_246,B_96),B_96),mult(B_246,B_96)) = ld(B_96,rd(rd(mult(B_246,B_96),B_96),B_246)) ),
inference(superposition,[status(thm),theory(equality)],[c_2562,c_17090]) ).
tff(c_27504,plain,
! [B_313,B_314] : ( ld(mult(mult(B_313,B_314),B_314),mult(B_313,B_314)) = ld(B_314,rd(B_313,B_313)) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_17344]) ).
tff(c_27742,plain,
! [B_57] : ( ld(rd(mult(B_57,B_57),B_57),mult(B_57,rd(B_57,B_57))) = ld(rd(B_57,B_57),rd(B_57,B_57)) ),
inference(superposition,[status(thm),theory(equality)],[c_910,c_27504]) ).
tff(c_27911,plain,
! [B_57] : ( ld(rd(B_57,B_57),rd(B_57,B_57)) = rd(B_57,B_57) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8,c_27742]) ).
tff(c_2783,plain,
! [B_101,B_102] : ( rd(ld(B_101,B_102),B_102) = ld(mult(B_102,B_101),B_102) ),
inference(superposition,[status(thm),theory(equality)],[c_2445,c_8]) ).
tff(c_4103,plain,
! [A_121,B_122] : ( ld(mult(A_121,rd(A_121,B_122)),A_121) = rd(B_122,A_121) ),
inference(superposition,[status(thm),theory(equality)],[c_48,c_2783]) ).
tff(c_4160,plain,
! [A_121,B_122] : ( mult(mult(A_121,rd(A_121,B_122)),rd(B_122,A_121)) = A_121 ),
inference(superposition,[status(thm),theory(equality)],[c_4103,c_2]) ).
tff(c_543,plain,
! [A_48,B_49,C_50] : ( mult(rd(A_48,B_49),mult(B_49,mult(C_50,rd(A_48,B_49)))) = mult(mult(A_48,C_50),rd(A_48,B_49)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_114]) ).
tff(c_15083,plain,
! [A_231,B_232,C_233] : ( ld(rd(A_231,B_232),mult(mult(A_231,C_233),rd(A_231,B_232))) = mult(B_232,mult(C_233,rd(A_231,B_232))) ),
inference(superposition,[status(thm),theory(equality)],[c_543,c_4]) ).
tff(c_15320,plain,
! [B_122] : ( mult(B_122,mult(rd(B_122,B_122),rd(B_122,B_122))) = ld(rd(B_122,B_122),B_122) ),
inference(superposition,[status(thm),theory(equality)],[c_4160,c_15083]) ).
tff(c_15482,plain,
! [B_234] : ( mult(B_234,mult(rd(B_234,B_234),rd(B_234,B_234))) = B_234 ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_15320]) ).
tff(c_15715,plain,
! [B_234] : ( mult(rd(B_234,B_234),rd(B_234,B_234)) = ld(B_234,B_234) ),
inference(superposition,[status(thm),theory(equality)],[c_15482,c_4]) ).
tff(c_27948,plain,
! [B_315] : ( ld(rd(B_315,B_315),rd(B_315,B_315)) = rd(B_315,B_315) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_8,c_27742]) ).
tff(c_2598,plain,
! [B_1,A_2] : ( mult(ld(B_1,A_2),A_2) = ld(ld(A_2,B_1),A_2) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_2445]) ).
tff(c_28053,plain,
! [B_315] : ( ld(ld(rd(B_315,B_315),rd(B_315,B_315)),rd(B_315,B_315)) = mult(rd(B_315,B_315),rd(B_315,B_315)) ),
inference(superposition,[status(thm),theory(equality)],[c_27948,c_2598]) ).
tff(c_28140,plain,
! [B_315] : ( rd(B_315,B_315) = ld(B_315,B_315) ),
inference(demodulation,[status(thm),theory(equality)],[c_27911,c_27911,c_15715,c_28053]) ).
tff(c_28836,plain,
! [B_234] : ( mult(ld(B_234,B_234),ld(B_234,B_234)) = ld(B_234,B_234) ),
inference(demodulation,[status(thm),theory(equality)],[c_28140,c_28140,c_15715]) ).
tff(c_51,plain,
! [A_20,B_21] : ( mult(A_20,ld(A_20,B_21)) = B_21 ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_60,plain,
! [B_21,A_20] : ( rd(B_21,ld(A_20,B_21)) = A_20 ),
inference(superposition,[status(thm),theory(equality)],[c_51,c_8]) ).
tff(c_28080,plain,
! [B_315] : ( rd(rd(B_315,B_315),rd(B_315,B_315)) = rd(B_315,B_315) ),
inference(superposition,[status(thm),theory(equality)],[c_27948,c_60]) ).
tff(c_30027,plain,
! [B_315] : ( ld(ld(B_315,B_315),ld(B_315,B_315)) = ld(B_315,B_315) ),
inference(demodulation,[status(thm),theory(equality)],[c_28140,c_28140,c_28140,c_28140,c_28080]) ).
tff(c_225,plain,
! [B_5,B_34,A_6] : ( rd(mult(B_5,mult(B_34,A_6)),B_5) = mult(mult(B_5,B_34),rd(A_6,B_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_200]) ).
tff(c_30420,plain,
! [B_326] : ( mult(ld(B_326,B_326),ld(B_326,B_326)) = ld(B_326,B_326) ),
inference(demodulation,[status(thm),theory(equality)],[c_28140,c_28140,c_15715]) ).
tff(c_129,plain,
! [A_27,B_28,C_29] : ( rd(mult(A_27,mult(B_28,mult(C_29,A_27))),A_27) = mult(mult(A_27,B_28),C_29) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_8]) ).
tff(c_246,plain,
! [C_38,A_36,B_37] : ( rd(mult(mult(C_38,A_36),mult(mult(B_37,C_38),A_36)),mult(C_38,A_36)) = mult(mult(mult(C_38,A_36),A_36),ld(A_36,B_37)) ),
inference(superposition,[status(thm),theory(equality)],[c_234,c_129]) ).
tff(c_30459,plain,
! [B_326,B_37] : ( rd(mult(ld(B_326,B_326),mult(mult(B_37,ld(B_326,B_326)),ld(B_326,B_326))),mult(ld(B_326,B_326),ld(B_326,B_326))) = mult(mult(mult(ld(B_326,B_326),ld(B_326,B_326)),ld(B_326,B_326)),ld(ld(B_326,B_326),B_37)) ),
inference(superposition,[status(thm),theory(equality)],[c_30420,c_246]) ).
tff(c_121207,plain,
! [B_588,B_589] : ( mult(mult(ld(B_588,B_588),mult(B_589,ld(B_588,B_588))),ld(B_588,B_588)) = B_589 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28836,c_28836,c_30027,c_28140,c_225,c_28836,c_30459]) ).
tff(c_124284,plain,
! [B_596,A_597] : ( mult(mult(ld(B_596,B_596),A_597),ld(B_596,B_596)) = rd(A_597,ld(B_596,B_596)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_121207]) ).
tff(c_10,plain,
! [A_11,B_10,C_9] : ( mult(mult(mult(A_11,B_10),C_9),A_11) = mult(A_11,mult(B_10,mult(C_9,A_11))) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_124860,plain,
! [B_596,A_597] : ( mult(ld(B_596,B_596),mult(A_597,mult(ld(B_596,B_596),ld(B_596,B_596)))) = mult(rd(A_597,ld(B_596,B_596)),ld(B_596,B_596)) ),
inference(superposition,[status(thm),theory(equality)],[c_124284,c_10]) ).
tff(c_125119,plain,
! [B_596,A_597] : ( mult(ld(B_596,B_596),mult(A_597,ld(B_596,B_596))) = A_597 ),
inference(demodulation,[status(thm),theory(equality)],[c_28836,c_6,c_124860]) ).
tff(c_30692,plain,
! [B_326,B_37] : ( mult(mult(ld(B_326,B_326),mult(B_37,ld(B_326,B_326))),ld(B_326,B_326)) = B_37 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28836,c_28836,c_30027,c_28140,c_225,c_28836,c_30459]) ).
tff(c_125149,plain,
! [B_37,B_326] : ( mult(B_37,ld(B_326,B_326)) = B_37 ),
inference(demodulation,[status(thm),theory(equality)],[c_125119,c_30692]) ).
tff(c_126071,plain,
! [B_596,A_597] : ( mult(ld(B_596,B_596),A_597) = A_597 ),
inference(demodulation,[status(thm),theory(equality)],[c_125149,c_125119]) ).
tff(c_126082,plain,
! [B_600,B_601] : ( mult(B_600,ld(B_601,B_601)) = B_600 ),
inference(demodulation,[status(thm),theory(equality)],[c_125119,c_30692]) ).
tff(c_12,plain,
! [X0_12] :
( ( mult('#skF_2'(X0_12),X0_12) != '#skF_2'(X0_12) )
| ( mult(X0_12,'#skF_1'(X0_12)) != '#skF_1'(X0_12) ) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_127162,plain,
! [B_601] : ( mult(ld(B_601,B_601),'#skF_1'(ld(B_601,B_601))) != '#skF_1'(ld(B_601,B_601)) ),
inference(superposition,[status(thm),theory(equality)],[c_126082,c_12]) ).
tff(c_131687,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_126071,c_127162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP660+1 : TPTP v9.0.0. Released v4.0.0.
% 0.06/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.13/0.33 % Computer : n028.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Apr 7 22:21:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 69.00/37.14 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 69.00/37.19
% 69.00/37.19 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------