%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP181-3 : 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/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 : n008.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:28 PM UTC 2025
% Result : Unsatisfiable 284.78s 237.13s
% Output : CNFRefutation 284.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 12
% Syntax : Number of formulae : 62 ( 62 unt; 0 typ; 0 def)
% Number of atoms : 62 ( 61 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 : 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 : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 89 ( 89 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > least_upper_bound > greatest_lower_bound > #nlpp > inverse > identity > c > b > 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(b,type,
b: $i ).
tff(identity,type,
identity: $i ).
tff(c,type,
c: $i ).
tff(f_125,axiom,
a != b,
file(unknown,unknown) ).
tff(f_59,axiom,
! [X] : ( multiply(identity,X) = X ),
file(unknown,unknown) ).
tff(f_63,axiom,
! [X] : ( multiply(inverse(X),X) = identity ),
file(unknown,unknown) ).
tff(f_66,axiom,
! [X,Y,Z] : ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ),
file(unknown,unknown) ).
tff(f_121,axiom,
! [X,Y] : ( inverse(greatest_lower_bound(X,Y)) = least_upper_bound(inverse(X),inverse(Y)) ),
file(unknown,unknown) ).
tff(f_94,axiom,
! [X,Y] : ( least_upper_bound(X,Y) = least_upper_bound(Y,X) ),
file(unknown,unknown) ).
tff(f_113,axiom,
! [Y,Z,X] : ( multiply(least_upper_bound(Y,Z),X) = least_upper_bound(multiply(Y,X),multiply(Z,X)) ),
file(unknown,unknown) ).
tff(f_109,axiom,
! [X,Y,Z] : ( multiply(X,least_upper_bound(Y,Z)) = least_upper_bound(multiply(X,Y),multiply(X,Z)) ),
file(unknown,unknown) ).
tff(f_119,axiom,
least_upper_bound(a,c) = least_upper_bound(b,c),
file(unknown,unknown) ).
tff(f_92,axiom,
! [X,Y] : ( greatest_lower_bound(X,Y) = greatest_lower_bound(Y,X) ),
file(unknown,unknown) ).
tff(f_111,axiom,
! [X,Y,Z] : ( multiply(X,greatest_lower_bound(Y,Z)) = greatest_lower_bound(multiply(X,Y),multiply(X,Z)) ),
file(unknown,unknown) ).
tff(f_118,axiom,
greatest_lower_bound(a,c) = greatest_lower_bound(b,c),
file(unknown,unknown) ).
tff(c_40,plain,
b != a,
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_2,plain,
! [X_1] : ( multiply(identity,X_1) = X_1 ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_4,plain,
! [X_2] : ( multiply(inverse(X_2),X_2) = identity ),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_1603,plain,
! [X_83,Y_84,Z_85] : ( multiply(multiply(X_83,Y_84),Z_85) = multiply(X_83,multiply(Y_84,Z_85)) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_1618,plain,
! [X_2,Z_85] : ( multiply(inverse(X_2),multiply(X_2,Z_85)) = multiply(identity,Z_85) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1603]) ).
tff(c_1626,plain,
! [X_2,Z_85] : ( multiply(inverse(X_2),multiply(X_2,Z_85)) = Z_85 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1618]) ).
tff(c_1628,plain,
! [X_86,Z_87] : ( multiply(inverse(X_86),multiply(X_86,Z_87)) = Z_87 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_1618]) ).
tff(c_2178,plain,
! [X_101,Z_102] : ( multiply(inverse(inverse(X_101)),Z_102) = multiply(X_101,Z_102) ),
inference(superposition,[status(thm),theory(equality)],[c_1626,c_1628]) ).
tff(c_2208,plain,
! [X_101,Z_85] : ( multiply(X_101,multiply(inverse(X_101),Z_85)) = Z_85 ),
inference(superposition,[status(thm),theory(equality)],[c_2178,c_1626]) ).
tff(c_6,plain,
! [X_3,Y_4,Z_5] : ( multiply(multiply(X_3,Y_4),Z_5) = multiply(X_3,multiply(Y_4,Z_5)) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_1649,plain,
! [X_2] : ( multiply(inverse(inverse(X_2)),identity) = X_2 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1628]) ).
tff(c_2201,plain,
! [X_101] : ( multiply(X_101,identity) = X_101 ),
inference(superposition,[status(thm),theory(equality)],[c_2178,c_1649]) ).
tff(c_2611,plain,
! [X_111] : ( multiply(X_111,inverse(X_111)) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_2178,c_4]) ).
tff(c_46854,plain,
! [X_359,Y_360] : ( multiply(X_359,multiply(Y_360,inverse(multiply(X_359,Y_360)))) = identity ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_2611]) ).
tff(c_46969,plain,
! [Y_360,X_359] : ( multiply(Y_360,inverse(multiply(X_359,Y_360))) = multiply(inverse(X_359),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_46854,c_1626]) ).
tff(c_47833,plain,
! [Y_367,X_368] : ( multiply(Y_367,inverse(multiply(X_368,Y_367))) = inverse(X_368) ),
inference(demodulation,[status(thm),theory(equality)],[c_2201,c_46969]) ).
tff(c_47932,plain,
! [X_368,X_101] : ( inverse(multiply(X_368,inverse(X_101))) = multiply(X_101,inverse(X_368)) ),
inference(superposition,[status(thm),theory(equality)],[c_47833,c_2208]) ).
tff(c_1656,plain,
! [X_88] : ( multiply(inverse(identity),X_88) = X_88 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_1628]) ).
tff(c_1810,plain,
! [X_93] : ( multiply(inverse(inverse(identity)),X_93) = X_93 ),
inference(superposition,[status(thm),theory(equality)],[c_1656,c_1626]) ).
tff(c_1837,plain,
inverse(identity) = identity,
inference(superposition,[status(thm),theory(equality)],[c_1810,c_4]) ).
tff(c_36,plain,
! [X_34,Y_35] : ( least_upper_bound(inverse(X_34),inverse(Y_35)) = inverse(greatest_lower_bound(X_34,Y_35)) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_1875,plain,
! [Y_35] : ( least_upper_bound(identity,inverse(Y_35)) = inverse(greatest_lower_bound(identity,Y_35)) ),
inference(superposition,[status(thm),theory(equality)],[c_1837,c_36]) ).
tff(c_10,plain,
! [Y_9,X_8] : ( least_upper_bound(Y_9,X_8) = least_upper_bound(X_8,Y_9) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_1931,plain,
! [Y_95,X_96,Z_97] : ( least_upper_bound(multiply(Y_95,X_96),multiply(Z_97,X_96)) = multiply(least_upper_bound(Y_95,Z_97),X_96) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_7689,plain,
! [Y_162,X_163] : ( multiply(least_upper_bound(Y_162,identity),X_163) = least_upper_bound(multiply(Y_162,X_163),X_163) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_1931]) ).
tff(c_7887,plain,
! [X_2] : ( multiply(least_upper_bound(inverse(X_2),identity),X_2) = least_upper_bound(identity,X_2) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_7689]) ).
tff(c_7925,plain,
! [X_2] : ( multiply(least_upper_bound(identity,inverse(X_2)),X_2) = least_upper_bound(identity,X_2) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_7887]) ).
tff(c_27312,plain,
! [X_277] : ( multiply(inverse(greatest_lower_bound(identity,X_277)),X_277) = least_upper_bound(identity,X_277) ),
inference(demodulation,[status(thm),theory(equality)],[c_1875,c_7925]) ).
tff(c_27334,plain,
! [X_277] : ( multiply(greatest_lower_bound(identity,X_277),least_upper_bound(identity,X_277)) = X_277 ),
inference(superposition,[status(thm),theory(equality)],[c_27312,c_2208]) ).
tff(c_2333,plain,
! [X_104,Y_105,Z_106] : ( least_upper_bound(multiply(X_104,Y_105),multiply(X_104,Z_106)) = multiply(X_104,least_upper_bound(Y_105,Z_106)) ),
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_2429,plain,
! [X_2,Y_105] : ( multiply(inverse(X_2),least_upper_bound(Y_105,X_2)) = least_upper_bound(multiply(inverse(X_2),Y_105),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_2333]) ).
tff(c_2457,plain,
! [X_2,Y_105] : ( multiply(inverse(X_2),least_upper_bound(Y_105,X_2)) = least_upper_bound(identity,multiply(inverse(X_2),Y_105)) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_2429]) ).
tff(c_34,plain,
least_upper_bound(b,c) = least_upper_bound(a,c),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_50752,plain,
! [X_380,Y_381] : ( multiply(inverse(X_380),least_upper_bound(Y_381,X_380)) = least_upper_bound(identity,multiply(inverse(X_380),Y_381)) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_2429]) ).
tff(c_51132,plain,
multiply(inverse(c),least_upper_bound(a,c)) = least_upper_bound(identity,multiply(inverse(c),b)),
inference(superposition,[status(thm),theory(equality)],[c_34,c_50752]) ).
tff(c_51211,plain,
least_upper_bound(identity,multiply(inverse(c),b)) = least_upper_bound(identity,multiply(inverse(c),a)),
inference(demodulation,[status(thm),theory(equality)],[c_2457,c_51132]) ).
tff(c_8,plain,
! [Y_7,X_6] : ( greatest_lower_bound(Y_7,X_6) = greatest_lower_bound(X_6,Y_7) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_1708,plain,
! [X_90,Y_91,Z_92] : ( greatest_lower_bound(multiply(X_90,Y_91),multiply(X_90,Z_92)) = multiply(X_90,greatest_lower_bound(Y_91,Z_92)) ),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_1784,plain,
! [X_2,Y_91] : ( multiply(inverse(X_2),greatest_lower_bound(Y_91,X_2)) = greatest_lower_bound(multiply(inverse(X_2),Y_91),identity) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_1708]) ).
tff(c_1806,plain,
! [X_2,Y_91] : ( multiply(inverse(X_2),greatest_lower_bound(Y_91,X_2)) = greatest_lower_bound(identity,multiply(inverse(X_2),Y_91)) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_1784]) ).
tff(c_32,plain,
greatest_lower_bound(b,c) = greatest_lower_bound(a,c),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_43866,plain,
! [X_349,Y_350] : ( multiply(inverse(X_349),greatest_lower_bound(Y_350,X_349)) = greatest_lower_bound(identity,multiply(inverse(X_349),Y_350)) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_1784]) ).
tff(c_44189,plain,
multiply(inverse(c),greatest_lower_bound(a,c)) = greatest_lower_bound(identity,multiply(inverse(c),b)),
inference(superposition,[status(thm),theory(equality)],[c_32,c_43866]) ).
tff(c_44252,plain,
greatest_lower_bound(identity,multiply(inverse(c),b)) = greatest_lower_bound(identity,multiply(inverse(c),a)),
inference(demodulation,[status(thm),theory(equality)],[c_1806,c_44189]) ).
tff(c_817113,plain,
multiply(greatest_lower_bound(identity,multiply(inverse(c),a)),least_upper_bound(identity,multiply(inverse(c),b))) = multiply(inverse(c),b),
inference(superposition,[status(thm),theory(equality)],[c_44252,c_27334]) ).
tff(c_817370,plain,
multiply(inverse(c),b) = multiply(inverse(c),a),
inference(demodulation,[status(thm),theory(equality)],[c_27334,c_51211,c_817113]) ).
tff(c_1646,plain,
! [X_3,Y_4,Z_5] : ( multiply(inverse(multiply(X_3,Y_4)),multiply(X_3,multiply(Y_4,Z_5))) = Z_5 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_1628]) ).
tff(c_817461,plain,
! [X_3] : ( multiply(inverse(multiply(X_3,inverse(c))),multiply(X_3,multiply(inverse(c),a))) = b ),
inference(superposition,[status(thm),theory(equality)],[c_817370,c_1646]) ).
tff(c_817633,plain,
b = a,
inference(demodulation,[status(thm),theory(equality)],[c_2208,c_1626,c_6,c_47932,c_817461]) ).
tff(c_817635,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40,c_817633]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP181-3 : TPTP v9.0.0. Bugfixed v1.2.1.
% 0.11/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 : n008.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:32:02 EDT 2025
% 0.13/0.35 % CPUTime :
% 284.78/237.13 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 284.78/237.14
% 284.78/237.14 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------