%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : BOO002-2 : TPTP v9.0.0. Released v1.1.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 : n005.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 05:44:59 PM UTC 2025
% Result : Unsatisfiable 129.98s 97.51s
% Output : CNFRefutation 130.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 6
% Syntax : Number of formulae : 26 ( 26 unt; 0 typ; 0 def)
% Number of atoms : 26 ( 25 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 4 ( 1 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 : 4 ( 4 usr; 2 con; 0-3 aty)
% Number of variables : 74 ( 74 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(b,type,
b: $i ).
tff(multiply,type,
multiply: ( $i * $i * $i ) > $i ).
tff(f_31,axiom,
! [X,Y] : ( multiply(X,X,Y) = X ),
file(unknown,unknown) ).
tff(f_38,axiom,
! [X,Y] : ( multiply(X,Y,X) = X ),
file(unknown,unknown) ).
tff(f_27,axiom,
! [W,Z,X,Y,V] : ( multiply(multiply(V,W,X),Y,multiply(V,W,Z)) = multiply(V,W,multiply(X,Y,Z)) ),
file(unknown,unknown) ).
tff(f_29,axiom,
! [Y,X] : ( multiply(Y,X,X) = X ),
file(unknown,unknown) ).
tff(f_33,axiom,
! [Y,X] : ( multiply(inverse(Y),Y,X) = X ),
file(unknown,unknown) ).
tff(f_40,axiom,
multiply(a,inverse(a),b) != b,
file(unknown,unknown) ).
tff(c_6,plain,
! [X_8,Y_9] : ( multiply(X_8,X_8,Y_9) = X_8 ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_10,plain,
! [X_12,Y_13] : ( multiply(X_12,Y_13,X_12) = X_12 ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_99,plain,
! [W_24,Y_26,V_25,X_23,Z_22] : ( multiply(multiply(V_25,W_24,X_23),Y_26,multiply(V_25,W_24,Z_22)) = multiply(V_25,W_24,multiply(X_23,Y_26,Z_22)) ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_161,plain,
! [X_12,Y_13,X_23,Y_26] : ( multiply(multiply(X_12,Y_13,X_23),Y_26,X_12) = multiply(X_12,Y_13,multiply(X_23,Y_26,X_12)) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_99]) ).
tff(c_674,plain,
! [X_45,Y_46,X_47,Y_48] : ( multiply(multiply(X_45,Y_46,X_47),Y_48,X_45) = multiply(X_45,Y_46,multiply(X_47,Y_48,X_45)) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_99]) ).
tff(c_4,plain,
! [Y_6,X_7] : ( multiply(Y_6,X_7,X_7) = X_7 ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_141,plain,
! [Y_6,X_7,X_23,Y_26] : ( multiply(multiply(Y_6,X_7,X_23),Y_26,X_7) = multiply(Y_6,X_7,multiply(X_23,Y_26,X_7)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_99]) ).
tff(c_376706,plain,
! [Y_943,X_942,Y_941,Y_939,X_940] : ( multiply(multiply(X_942,Y_939,multiply(X_940,Y_941,X_942)),Y_943,Y_941) = multiply(multiply(X_942,Y_939,X_940),Y_941,multiply(X_942,Y_943,Y_941)) ),
inference(superposition,[status(thm),theory(equality)],[c_674,c_141]) ).
tff(c_404488,plain,
! [Y_977,Y_978,X_979,Y_980] : ( multiply(multiply(Y_977,Y_978,X_979),X_979,multiply(Y_977,Y_980,X_979)) = multiply(multiply(Y_977,Y_978,X_979),Y_980,X_979) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_376706]) ).
tff(c_406937,plain,
! [X_8,Y_978,Y_9] : ( multiply(multiply(X_8,Y_978,Y_9),Y_9,X_8) = multiply(multiply(X_8,Y_978,Y_9),X_8,Y_9) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_404488]) ).
tff(c_407527,plain,
! [X_981,Y_982,Y_983] : ( multiply(multiply(X_981,Y_982,Y_983),X_981,Y_983) = multiply(X_981,Y_982,Y_983) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_161,c_406937]) ).
tff(c_8,plain,
! [Y_10,X_11] : ( multiply(inverse(Y_10),Y_10,X_11) = X_11 ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_455,plain,
! [Y_38,X_39,X_40,Y_41] : ( multiply(multiply(Y_38,X_39,X_40),Y_41,X_39) = multiply(Y_38,X_39,multiply(X_40,Y_41,X_39)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_99]) ).
tff(c_21223,plain,
! [X_210,Y_214,Y_212,X_213,Y_211] : ( multiply(multiply(Y_211,X_210,multiply(X_213,Y_214,X_210)),Y_212,Y_214) = multiply(multiply(Y_211,X_210,X_213),Y_214,multiply(X_210,Y_212,Y_214)) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_455]) ).
tff(c_23561,plain,
! [Y_225,Y_226,X_227,Y_228] : ( multiply(multiply(Y_225,Y_226,X_227),X_227,multiply(Y_226,Y_228,X_227)) = multiply(multiply(Y_225,Y_226,X_227),Y_228,X_227) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_21223]) ).
tff(c_24171,plain,
! [Y_225,Y_10,X_11] : ( multiply(multiply(Y_225,inverse(Y_10),X_11),Y_10,X_11) = multiply(multiply(Y_225,inverse(Y_10),X_11),X_11,X_11) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_23561]) ).
tff(c_24333,plain,
! [Y_225,Y_10,X_11] : ( multiply(multiply(Y_225,inverse(Y_10),X_11),Y_10,X_11) = X_11 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_24171]) ).
tff(c_408737,plain,
! [X_981,Y_983] : ( multiply(X_981,inverse(X_981),Y_983) = Y_983 ),
inference(superposition,[status(thm),theory(equality)],[c_407527,c_24333]) ).
tff(c_12,plain,
multiply(a,inverse(a),b) != b,
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_410358,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_408737,c_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : BOO002-2 : TPTP v9.0.0. Released v1.1.0.
% 0.02/0.09 % 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.09/0.29 % Computer : n005.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Mon Apr 7 15:20:57 EDT 2025
% 0.09/0.29 % CPUTime :
% 129.98/97.51 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 129.98/97.51
% 129.98/97.51 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------