%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP167-5 : TPTP v9.0.0. Bugfixed v1.2.1.
% 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 : n027.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:25:25 PM UTC 2025
% Result : Unsatisfiable 9.69s 3.41s
% Output : CNFRefutation 9.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 10
% Syntax : Number of formulae : 39 ( 39 unt; 0 typ; 0 def)
% Number of atoms : 39 ( 38 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 4 ( 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; 2 con; 0-2 aty)
% Number of variables : 56 ( 56 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > least_upper_bound > greatest_lower_bound > #nlpp > positive_part > negative_part > inverse > identity > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(greatest_lower_bound,type,
greatest_lower_bound: ( $i * $i ) > $i ).
tff(least_upper_bound,type,
least_upper_bound: ( $i * $i ) > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(negative_part,type,
negative_part: $i > $i ).
tff(positive_part,type,
positive_part: $i > $i ).
tff(identity,type,
identity: $i ).
tff(f_97,axiom,
! [X,Y] : ( least_upper_bound(X,Y) = least_upper_bound(Y,X) ),
file(unknown,unknown) ).
tff(f_125,axiom,
! [X] : ( positive_part(X) = least_upper_bound(X,identity) ),
file(unknown,unknown) ).
tff(f_62,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_66,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_69,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_123,axiom,
! [A,B] : ( inverse(least_upper_bound(A,B)) = greatest_lower_bound(inverse(A),inverse(B)) ),
file(unknown,unknown) ).
tff(f_95,axiom,
! [X,Y] : ( greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X) ),
file(unknown,unknown) ).
tff(f_127,axiom,
! [X] : ( negative_part(X) = greatest_lower_bound(X,identity) ),
file(unknown,unknown) ).
tff(f_118,axiom,
! [Y,Z,X] : ( multiply(greatest_lower_bound(Y,Z),X) = greatest_lower_bound(multiply(Y,X),multiply(Z,X)) ),
file(unknown,unknown) ).
tff(f_133,axiom,
a != multiply(positive_part(a),negative_part(a)),
file(unknown,unknown) ).
tff(c_150,plain,
! [Y_53,X_54] : ( least_upper_bound(Y_53,X_54) = least_upper_bound(X_54,Y_53) ),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_34,plain,
! [X_36] : ( least_upper_bound(X_36,identity) = positive_part(X_36) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_166,plain,
! [X_54] : ( least_upper_bound(identity,X_54) = positive_part(X_54) ),
inference(superposition,[status(thm),theory(equality)],[c_150,c_34]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_1139,plain,
! [X_82,Y_83,Z_84] : ( multiply(multiply(X_82,Y_83),Z_84) = multiply(X_82,multiply(Y_83,Z_84)) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_1154,plain,
! [X_2,Z_84] : ( multiply(inverse(X_2),multiply(X_2,Z_84)) = multiply(identity,Z_84) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1139]) ).
tff(c_2507,plain,
! [X_115,Z_116] : ( multiply(inverse(X_115),multiply(X_115,Z_116)) = Z_116 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1154]) ).
tff(c_2559,plain,
! [X_117] : ( multiply(inverse(identity),X_117) = X_117 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_2507]) ).
tff(c_1162,plain,
! [X_2,Z_84] : ( multiply(inverse(X_2),multiply(X_2,Z_84)) = Z_84 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1154]) ).
tff(c_2667,plain,
! [X_119] : ( multiply(inverse(inverse(identity)),X_119) = X_119 ),
inference(superposition,[status(thm),theory(equality)],[c_2559,c_1162]) ).
tff(c_2712,plain,
inverse(identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_2667,c_4]) ).
tff(c_32,plain,
! [A_34,B_35] : ( greatest_lower_bound(inverse(A_34),inverse(B_35)) = inverse(least_upper_bound(A_34,B_35)) ),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_2752,plain,
! [B_35] : ( greatest_lower_bound(identity,inverse(B_35)) = inverse(least_upper_bound(identity,B_35)) ),
inference(superposition,[status(thm),theory(equality)],[c_2712,c_32]) ).
tff(c_7714,plain,
! [B_185] : ( greatest_lower_bound(identity,inverse(B_185)) = inverse(positive_part(B_185)) ),
inference(demodulation,[status(thm),theory(equality)],[c_166,c_2752]) ).
tff(c_319,plain,
! [Y_59,X_60] : ( greatest_lower_bound(Y_59,X_60) = greatest_lower_bound(X_60,Y_59) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_36,plain,
! [X_37] : ( greatest_lower_bound(X_37,identity) = negative_part(X_37) ),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_341,plain,
! [X_60] : ( greatest_lower_bound(identity,X_60) = negative_part(X_60) ),
inference(superposition,[status(thm),theory(equality)],[c_319,c_36]) ).
tff(c_7753,plain,
! [B_185] : ( negative_part(inverse(B_185)) = inverse(positive_part(B_185)) ),
inference(superposition,[status(thm),theory(equality)],[c_7714,c_341]) ).
tff(c_1438,plain,
! [Y_92,X_93,Z_94] : ( greatest_lower_bound(multiply(Y_92,X_93),multiply(Z_94,X_93)) = multiply(greatest_lower_bound(Y_92,Z_94),X_93) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_1487,plain,
! [Y_92,X_1] : ( multiply(greatest_lower_bound(Y_92,identity),X_1) = greatest_lower_bound(multiply(Y_92,X_1),X_1) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_1438]) ).
tff(c_9575,plain,
! [Y_204,X_205] : ( multiply(negative_part(Y_204),X_205) = greatest_lower_bound(multiply(Y_204,X_205),X_205) ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_1487]) ).
tff(c_9736,plain,
! [X_2] : ( multiply(negative_part(inverse(X_2)),X_2) = greatest_lower_bound(identity,X_2) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_9575]) ).
tff(c_9765,plain,
! [X_2] : ( multiply(inverse(positive_part(X_2)),X_2) = negative_part(X_2) ),
inference(demodulation,[status(thm),theory(equality)],[c_7753,c_341,c_9736]) ).
tff(c_15924,plain,
! [X_261,Z_262] : ( multiply(inverse(inverse(X_261)),Z_262) = multiply(X_261,Z_262) ),
inference(superposition,[status(thm),theory(equality)],[c_2507,c_1162]) ).
tff(c_16820,plain,
! [X_269,Z_270] : ( multiply(X_269,multiply(inverse(X_269),Z_270)) = Z_270 ),
inference(superposition,[status(thm),theory(equality)],[c_15924,c_1162]) ).
tff(c_16923,plain,
! [X_2] : ( multiply(positive_part(X_2),negative_part(X_2)) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_9765,c_16820]) ).
tff(c_42,plain,
multiply(positive_part(a),negative_part(a)) != a,
inference(cnfTransformation,[status(thm)],[f_133]) ).
tff(c_16958,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16923,c_42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP167-5 : TPTP v9.0.0. Bugfixed v1.2.1.
% 0.11/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.34 % Computer : n027.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:29:51 EDT 2025
% 0.13/0.34 % CPUTime :
% 9.69/3.41 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.69/3.42
% 9.69/3.42 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------