%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP527-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 : 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:26:26 PM UTC 2025
% Result : Unsatisfiable 11.97s 4.24s
% Output : CNFRefutation 11.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 4
% Syntax : Number of formulae : 40 ( 40 unt; 0 typ; 0 def)
% Number of atoms : 40 ( 39 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 5 ( 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 : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 79 ( 79 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > divide > #nlpp > inverse > c3 > b3 > a3
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a3,type,
a3: $i ).
tff(c3,type,
c3: $i ).
tff(divide,type,
divide: ( $i * $i ) > $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b3,type,
b3: $i ).
tff(f_27,axiom,
! [A,B] : ( inverse(A) = divide(divide(B,B),A) ),
file(unknown,unknown) ).
tff(f_23,axiom,
! [A,B,C] : ( divide(A,divide(divide(A,B),divide(C,B))) = C ),
file(unknown,unknown) ).
tff(f_25,axiom,
! [A,B,C] : ( multiply(A,B) = divide(A,divide(divide(C,C),B)) ),
file(unknown,unknown) ).
tff(f_29,axiom,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file(unknown,unknown) ).
tff(c_6,plain,
! [B_8,A_7] : ( divide(divide(B_8,B_8),A_7) = inverse(A_7) ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_10,plain,
! [B_9,A_10] : ( divide(divide(B_9,B_9),A_10) = inverse(A_10) ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_21,plain,
! [B_8,A_10] : ( divide(inverse(divide(B_8,B_8)),A_10) = inverse(A_10) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_10]) ).
tff(c_146,plain,
! [A_21,B_22,C_23] : ( divide(A_21,divide(divide(A_21,B_22),divide(C_23,B_22))) = C_23 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_238,plain,
! [B_24,C_25] : ( divide(B_24,inverse(divide(C_25,B_24))) = C_25 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_146]) ).
tff(c_4,plain,
! [A_4,C_6,B_5] : ( divide(A_4,divide(divide(C_6,C_6),B_5)) = multiply(A_4,B_5) ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_9,plain,
! [A_4,B_5] : ( divide(A_4,inverse(B_5)) = multiply(A_4,B_5) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4]) ).
tff(c_309,plain,
! [B_26,C_27] : ( multiply(B_26,divide(C_27,B_26)) = C_27 ),
inference(superposition,[status(thm),theory(equality)],[c_238,c_9]) ).
tff(c_545,plain,
! [A_36,B_37] : ( multiply(A_36,inverse(A_36)) = divide(B_37,B_37) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_309]) ).
tff(c_349,plain,
! [A_7,B_8] : ( multiply(A_7,inverse(A_7)) = divide(B_8,B_8) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_309]) ).
tff(c_639,plain,
! [B_39,B_38] : ( divide(B_39,B_39) = divide(B_38,B_38) ),
inference(superposition,[status(thm),theory(equality)],[c_545,c_349]) ).
tff(c_2,plain,
! [A_1,B_2,C_3] : ( divide(A_1,divide(divide(A_1,B_2),divide(C_3,B_2))) = C_3 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_800,plain,
! [A_40,B_41] : ( divide(A_40,divide(B_41,B_41)) = A_40 ),
inference(superposition,[status(thm),theory(equality)],[c_639,c_2]) ).
tff(c_171,plain,
! [B_8,B_22,C_23] : ( inverse(divide(divide(divide(B_8,B_8),B_22),divide(C_23,B_22))) = C_23 ),
inference(superposition,[status(thm),theory(equality)],[c_146,c_6]) ).
tff(c_228,plain,
! [B_22,C_23] : ( inverse(divide(inverse(B_22),divide(C_23,B_22))) = C_23 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_171]) ).
tff(c_829,plain,
! [B_41,A_40] : ( inverse(divide(inverse(divide(B_41,B_41)),A_40)) = A_40 ),
inference(superposition,[status(thm),theory(equality)],[c_800,c_228]) ).
tff(c_945,plain,
! [A_40] : ( inverse(inverse(A_40)) = A_40 ),
inference(demodulation,[status(thm),theory(equality)],[c_21,c_829]) ).
tff(c_408,plain,
! [B_32,C_33] : ( inverse(divide(inverse(B_32),divide(C_33,B_32))) = C_33 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_171]) ).
tff(c_220,plain,
! [B_8,C_23] : ( divide(B_8,inverse(divide(C_23,B_8))) = C_23 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_146]) ).
tff(c_470,plain,
! [C_34,B_35] : ( divide(divide(C_34,B_35),C_34) = inverse(B_35) ),
inference(superposition,[status(thm),theory(equality)],[c_408,c_220]) ).
tff(c_1258,plain,
! [C_49,B_50] : ( divide(divide(C_49,B_50),inverse(B_50)) = C_49 ),
inference(superposition,[status(thm),theory(equality)],[c_470,c_2]) ).
tff(c_1348,plain,
! [A_4,B_5] : ( divide(multiply(A_4,B_5),inverse(inverse(B_5))) = A_4 ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_1258]) ).
tff(c_1603,plain,
! [A_56,B_57] : ( divide(multiply(A_56,B_57),B_57) = A_56 ),
inference(demodulation,[status(thm),theory(equality)],[c_945,c_1348]) ).
tff(c_261,plain,
! [B_24,C_25] : ( multiply(B_24,divide(C_25,B_24)) = C_25 ),
inference(superposition,[status(thm),theory(equality)],[c_238,c_9]) ).
tff(c_1631,plain,
! [B_57,A_56] : ( multiply(B_57,A_56) = multiply(A_56,B_57) ),
inference(superposition,[status(thm),theory(equality)],[c_1603,c_261]) ).
tff(c_2599,plain,
! [A_72,C_73,B_74] : ( divide(divide(A_72,divide(C_73,B_74)),B_74) = divide(A_72,C_73) ),
inference(superposition,[status(thm),theory(equality)],[c_146,c_2]) ).
tff(c_423,plain,
! [C_33,B_32] : ( divide(divide(C_33,B_32),C_33) = inverse(B_32) ),
inference(superposition,[status(thm),theory(equality)],[c_408,c_220]) ).
tff(c_2810,plain,
! [C_75,B_76] : ( inverse(divide(C_75,B_76)) = divide(B_76,C_75) ),
inference(superposition,[status(thm),theory(equality)],[c_2599,c_423]) ).
tff(c_2895,plain,
! [B_5,A_4] : ( divide(inverse(B_5),A_4) = inverse(multiply(A_4,B_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_2810]) ).
tff(c_24220,plain,
! [B_240,A_241,C_242] : ( multiply(B_240,divide(A_241,C_242)) = divide(A_241,divide(C_242,B_240)) ),
inference(superposition,[status(thm),theory(equality)],[c_2599,c_261]) ).
tff(c_24575,plain,
! [A_4,B_5,B_240] : ( divide(A_4,divide(inverse(B_5),B_240)) = multiply(B_240,multiply(A_4,B_5)) ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_24220]) ).
tff(c_24659,plain,
! [B_240,A_4,B_5] : ( multiply(B_240,multiply(A_4,B_5)) = multiply(A_4,multiply(B_240,B_5)) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_2895,c_24575]) ).
tff(c_8,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_1698,plain,
multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_1631,c_8]) ).
tff(c_27022,plain,
multiply(a3,multiply(c3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_24659,c_1698]) ).
tff(c_27025,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1631,c_27022]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP527-1 : TPTP v9.0.0. Released v2.6.0.
% 0.10/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 : n002.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:55:17 EDT 2025
% 0.13/0.34 % CPUTime :
% 11.97/4.24 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.97/4.25
% 11.97/4.25 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------