%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP088-1 : TPTP v9.0.0. Bugfixed v2.7.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 : n019.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:24:58 PM UTC 2025
% Result : Unsatisfiable 34.18s 22.58s
% Output : CNFRefutation 34.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 4
% Syntax : Number of formulae : 95 ( 91 unt; 0 typ; 0 def)
% Number of atoms : 104 ( 100 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 32 ( 23 ~; 9 |; 0 &)
% ( 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 : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 181 ( 181 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > divide > #nlpp > inverse > c3 > b4 > b3 > b2 > b1 > a4 > a3 > a2 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(a3,type,
a3: $i ).
tff(c3,type,
c3: $i ).
tff(divide,type,
divide: ( $i * $i ) > $i ).
tff(b2,type,
b2: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b1,type,
b1: $i ).
tff(b4,type,
b4: $i ).
tff(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(a4,type,
a4: $i ).
tff(f_33,axiom,
! [X,Z] : ( inverse(X) = divide(divide(Z,Z),X) ),
file(unknown,unknown) ).
tff(f_30,axiom,
! [X,Y,Z] : ( multiply(X,Y) = divide(X,divide(divide(Z,Z),Y)) ),
file(unknown,unknown) ).
tff(f_27,axiom,
! [X,Y,Z] : ( divide(X,divide(Y,divide(Z,divide(X,Y)))) = Z ),
file(unknown,unknown) ).
tff(f_44,axiom,
( ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(a4,b4) != multiply(b4,a4) ) ),
file(unknown,unknown) ).
tff(c_6,plain,
! [Z_8,X_7] : ( divide(divide(Z_8,Z_8),X_7) = inverse(X_7) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_4,plain,
! [X_4,Z_6,Y_5] : ( divide(X_4,divide(divide(Z_6,Z_6),Y_5)) = multiply(X_4,Y_5) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_9,plain,
! [X_4,Y_5] : ( divide(X_4,inverse(Y_5)) = multiply(X_4,Y_5) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4]) ).
tff(c_107,plain,
! [X_17,Y_18,Z_19] : ( divide(X_17,divide(Y_18,divide(Z_19,divide(X_17,Y_18)))) = Z_19 ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_124,plain,
! [Y_18,Z_19,Z_8] : ( inverse(divide(Y_18,divide(Z_19,divide(divide(Z_8,Z_8),Y_18)))) = Z_19 ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_6]) ).
tff(c_169,plain,
! [Y_18,Z_19] : ( inverse(divide(Y_18,multiply(Z_19,Y_18))) = Z_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_124]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3] : ( divide(X_1,divide(Y_2,divide(Z_3,divide(X_1,Y_2)))) = Z_3 ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_6771,plain,
! [Y_144,Z_145,X_146] : ( divide(Y_144,divide(divide(Z_145,divide(X_146,Y_144)),Z_145)) = X_146 ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_2]) ).
tff(c_7039,plain,
! [Y_150,X_151] : ( divide(Y_150,inverse(divide(X_151,Y_150))) = X_151 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_6771]) ).
tff(c_7112,plain,
! [Z_19,Y_18] : ( divide(multiply(Z_19,Y_18),Z_19) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_7039]) ).
tff(c_27,plain,
! [X_11,Y_12] : ( divide(X_11,inverse(Y_12)) = multiply(X_11,Y_12) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_4]) ).
tff(c_45,plain,
! [Z_8,Y_12] : ( multiply(divide(Z_8,Z_8),Y_12) = inverse(inverse(Y_12)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_27]) ).
tff(c_178,plain,
! [Y_20,Z_21] : ( inverse(divide(Y_20,multiply(Z_21,Y_20))) = Z_21 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_124]) ).
tff(c_190,plain,
! [Y_12,Z_8] : ( inverse(divide(Y_12,inverse(inverse(Y_12)))) = divide(Z_8,Z_8) ),
inference(superposition,[status(thm),theory(equality)],[c_45,c_178]) ).
tff(c_4211,plain,
! [Y_92,Z_93] : ( inverse(multiply(Y_92,inverse(Y_92))) = divide(Z_93,Z_93) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_190]) ).
tff(c_201,plain,
! [Y_12,Z_8] : ( inverse(multiply(Y_12,inverse(Y_12))) = divide(Z_8,Z_8) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_190]) ).
tff(c_4218,plain,
! [Z_93,Z_8] : ( divide(Z_93,Z_93) = divide(Z_8,Z_8) ),
inference(superposition,[status(thm),theory(equality)],[c_4211,c_201]) ).
tff(c_6839,plain,
! [Y_144,Z_93,X_146] : ( divide(Y_144,divide(divide(Z_93,Z_93),divide(X_146,Y_144))) = X_146 ),
inference(superposition,[status(thm),theory(equality)],[c_4218,c_6771]) ).
tff(c_6922,plain,
! [Y_147,X_148] : ( multiply(Y_147,divide(X_148,Y_147)) = X_148 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_6839]) ).
tff(c_198,plain,
! [Z_21,Z_8] : ( inverse(inverse(multiply(Z_21,divide(Z_8,Z_8)))) = Z_21 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_178]) ).
tff(c_6929,plain,
! [Y_147] : ( inverse(inverse(Y_147)) = Y_147 ),
inference(superposition,[status(thm),theory(equality)],[c_6922,c_198]) ).
tff(c_4287,plain,
! [Z_95,Z_94] : ( divide(Z_95,Z_95) = divide(Z_94,Z_94) ),
inference(superposition,[status(thm),theory(equality)],[c_4211,c_201]) ).
tff(c_4397,plain,
! [Z_8,Z_94] : ( inverse(divide(Z_8,Z_8)) = divide(Z_94,Z_94) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_4287]) ).
tff(c_7090,plain,
! [Z_94,Z_8] : ( divide(Z_94,inverse(inverse(divide(Z_8,Z_8)))) = Z_94 ),
inference(superposition,[status(thm),theory(equality)],[c_4397,c_7039]) ).
tff(c_7408,plain,
! [Z_158,Z_159] : ( divide(Z_158,divide(Z_159,Z_159)) = Z_158 ),
inference(demodulation,[status(thm),theory(equality)],[c_6929,c_7090]) ).
tff(c_7602,plain,
! [Z_160,Z_161] : ( divide(Z_160,divide(Z_160,Z_161)) = Z_161 ),
inference(superposition,[status(thm),theory(equality)],[c_7408,c_2]) ).
tff(c_7755,plain,
! [Z_162,Y_163] : ( divide(multiply(Z_162,Y_163),Y_163) = Z_162 ),
inference(superposition,[status(thm),theory(equality)],[c_7112,c_7602]) ).
tff(c_6914,plain,
! [Y_144,X_146] : ( multiply(Y_144,divide(X_146,Y_144)) = X_146 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_6839]) ).
tff(c_7775,plain,
! [Z_162,Y_163] : ( multiply(Z_162,Y_163) = multiply(Y_163,Z_162) ),
inference(superposition,[status(thm),theory(equality)],[c_7755,c_6914]) ).
tff(c_14616,plain,
! [X_242,Y_243,X_244] : ( divide(divide(X_242,Y_243),divide(X_244,Y_243)) = divide(X_242,X_244) ),
inference(superposition,[status(thm),theory(equality)],[c_6771,c_2]) ).
tff(c_14924,plain,
! [X_7,X_244,Z_8] : ( divide(inverse(X_7),divide(X_244,X_7)) = divide(divide(Z_8,Z_8),X_244) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_14616]) ).
tff(c_14975,plain,
! [X_245,X_246] : ( divide(inverse(X_245),divide(X_246,X_245)) = inverse(X_246) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_14924]) ).
tff(c_15122,plain,
! [Z_19,Y_18] : ( divide(inverse(Z_19),Y_18) = inverse(multiply(Z_19,Y_18)) ),
inference(superposition,[status(thm),theory(equality)],[c_7112,c_14975]) ).
tff(c_7125,plain,
! [Y_5,X_4] : ( divide(inverse(Y_5),inverse(multiply(X_4,Y_5))) = X_4 ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_7039]) ).
tff(c_14742,plain,
! [X_244,Y_243,X_242] : ( divide(X_244,divide(Y_243,divide(X_242,X_244))) = divide(X_242,Y_243) ),
inference(superposition,[status(thm),theory(equality)],[c_14616,c_2]) ).
tff(c_10022,plain,
! [X_193,Y_194,Z_195,Z_196] : ( divide(X_193,divide(divide(Y_194,divide(Z_195,divide(X_193,Y_194))),divide(Z_196,Z_195))) = Z_196 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_107]) ).
tff(c_113,plain,
! [Y_18,Z_19,X_17] : ( divide(Y_18,divide(divide(Z_19,divide(X_17,Y_18)),Z_19)) = X_17 ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_2]) ).
tff(c_10066,plain,
! [Z_196,Z_195,X_193,Y_194] : ( divide(divide(Z_196,Z_195),divide(Z_196,X_193)) = divide(Y_194,divide(Z_195,divide(X_193,Y_194))) ),
inference(superposition,[status(thm),theory(equality)],[c_10022,c_113]) ).
tff(c_21669,plain,
! [Z_297,Z_298,X_299] : ( divide(divide(Z_297,Z_298),divide(Z_297,X_299)) = divide(X_299,Z_298) ),
inference(demodulation,[status(thm),theory(equality)],[c_14742,c_10066]) ).
tff(c_21920,plain,
! [X_4,Y_5,X_299] : ( divide(X_4,divide(inverse(Y_5),X_299)) = divide(X_299,inverse(multiply(X_4,Y_5))) ),
inference(superposition,[status(thm),theory(equality)],[c_7125,c_21669]) ).
tff(c_22101,plain,
! [X_4,Y_5,X_299] : ( multiply(X_4,multiply(Y_5,X_299)) = multiply(X_299,multiply(X_4,Y_5)) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_15122,c_9,c_21920]) ).
tff(c_6194,plain,
! [Y_132,Z_133,X_134] : ( divide(Y_132,divide(divide(Z_133,divide(X_134,Y_132)),Z_133)) = X_134 ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_2]) ).
tff(c_6269,plain,
! [Y_132,Z_93,X_134] : ( divide(Y_132,divide(divide(Z_93,Z_93),divide(X_134,Y_132))) = X_134 ),
inference(superposition,[status(thm),theory(equality)],[c_4218,c_6194]) ).
tff(c_6352,plain,
! [Y_135,X_136] : ( multiply(Y_135,divide(X_136,Y_135)) = X_136 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_6269]) ).
tff(c_6359,plain,
! [Y_135] : ( inverse(inverse(Y_135)) = Y_135 ),
inference(superposition,[status(thm),theory(equality)],[c_6352,c_198]) ).
tff(c_4345,plain,
! [Y_5,Z_94] : ( multiply(inverse(Y_5),Y_5) = divide(Z_94,Z_94) ),
inference(superposition,[status(thm),theory(equality)],[c_4287,c_9]) ).
tff(c_4610,plain,
! [Y_100,Z_101,X_102] : ( divide(Y_100,divide(divide(Z_101,divide(X_102,Y_100)),Z_101)) = X_102 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_107]) ).
tff(c_4807,plain,
! [Y_105,X_106] : ( divide(Y_105,inverse(divide(X_106,Y_105))) = X_106 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_4610]) ).
tff(c_4874,plain,
! [Z_19,Y_18] : ( divide(multiply(Z_19,Y_18),Z_19) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_4807]) ).
tff(c_4401,plain,
! [Z_8,Z_95] : ( inverse(divide(Z_8,Z_8)) = divide(Z_95,Z_95) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_4287]) ).
tff(c_5063,plain,
! [Z_112,Z_113] : ( divide(Z_112,divide(Z_113,Z_113)) = Z_112 ),
inference(superposition,[status(thm),theory(equality)],[c_4401,c_4807]) ).
tff(c_5237,plain,
! [Z_114,Z_115] : ( divide(Z_114,divide(Z_114,Z_115)) = Z_115 ),
inference(superposition,[status(thm),theory(equality)],[c_5063,c_2]) ).
tff(c_4671,plain,
! [Y_100,Z_93,X_102] : ( divide(Y_100,divide(divide(Z_93,Z_93),divide(X_102,Y_100))) = X_102 ),
inference(superposition,[status(thm),theory(equality)],[c_4218,c_4610]) ).
tff(c_4744,plain,
! [Y_100,X_102] : ( multiply(Y_100,divide(X_102,Y_100)) = X_102 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_4671]) ).
tff(c_5456,plain,
! [Z_118,Z_119] : ( multiply(divide(Z_118,Z_119),Z_119) = Z_118 ),
inference(superposition,[status(thm),theory(equality)],[c_5237,c_4744]) ).
tff(c_5493,plain,
! [Z_19,Y_18] : ( multiply(Z_19,Y_18) = multiply(Y_18,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_4874,c_5456]) ).
tff(c_303,plain,
! [Y_26,Z_27] : ( inverse(multiply(Y_26,inverse(Y_26))) = divide(Z_27,Z_27) ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_190]) ).
tff(c_310,plain,
! [Z_8,Z_27] : ( divide(Z_8,Z_8) = divide(Z_27,Z_27) ),
inference(superposition,[status(thm),theory(equality)],[c_303,c_201]) ).
tff(c_721,plain,
! [Y_34,Z_35,X_36] : ( divide(Y_34,divide(divide(Z_35,divide(X_36,Y_34)),Z_35)) = X_36 ),
inference(superposition,[status(thm),theory(equality)],[c_107,c_2]) ).
tff(c_782,plain,
! [Y_34,Z_8,X_36] : ( divide(Y_34,divide(divide(Z_8,Z_8),divide(X_36,Y_34))) = X_36 ),
inference(superposition,[status(thm),theory(equality)],[c_310,c_721]) ).
tff(c_863,plain,
! [Y_37,X_38] : ( multiply(Y_37,divide(X_38,Y_37)) = X_38 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_782]) ).
tff(c_917,plain,
! [X_7,Z_8] : ( multiply(X_7,inverse(X_7)) = divide(Z_8,Z_8) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_863]) ).
tff(c_969,plain,
! [Y_40,X_41] : ( divide(Y_40,inverse(divide(X_41,Y_40))) = X_41 ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_721]) ).
tff(c_1036,plain,
! [Z_19,Y_18] : ( divide(multiply(Z_19,Y_18),Z_19) = Y_18 ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_969]) ).
tff(c_870,plain,
! [Y_37] : ( inverse(inverse(Y_37)) = Y_37 ),
inference(superposition,[status(thm),theory(equality)],[c_863,c_198]) ).
tff(c_384,plain,
! [Z_29,Z_28] : ( divide(Z_29,Z_29) = divide(Z_28,Z_28) ),
inference(superposition,[status(thm),theory(equality)],[c_303,c_201]) ).
tff(c_452,plain,
! [Z_8,Z_29] : ( inverse(divide(Z_8,Z_8)) = divide(Z_29,Z_29) ),
inference(superposition,[status(thm),theory(equality)],[c_384,c_6]) ).
tff(c_1014,plain,
! [Z_29,Z_8] : ( divide(Z_29,inverse(inverse(divide(Z_8,Z_8)))) = Z_29 ),
inference(superposition,[status(thm),theory(equality)],[c_452,c_969]) ).
tff(c_1202,plain,
! [Z_46,Z_47] : ( divide(Z_46,divide(Z_47,Z_47)) = Z_46 ),
inference(demodulation,[status(thm),theory(equality)],[c_870,c_1014]) ).
tff(c_1444,plain,
! [Z_50,Z_51] : ( divide(Z_50,divide(Z_50,Z_51)) = Z_51 ),
inference(superposition,[status(thm),theory(equality)],[c_1202,c_2]) ).
tff(c_855,plain,
! [Y_34,X_36] : ( multiply(Y_34,divide(X_36,Y_34)) = X_36 ),
inference(demodulation,[status(thm),theory(equality)],[c_9,c_6,c_782]) ).
tff(c_1586,plain,
! [Z_52,Z_53] : ( multiply(divide(Z_52,Z_53),Z_53) = Z_52 ),
inference(superposition,[status(thm),theory(equality)],[c_1444,c_855]) ).
tff(c_1623,plain,
! [Z_19,Y_18] : ( multiply(Z_19,Y_18) = multiply(Y_18,Z_19) ),
inference(superposition,[status(thm),theory(equality)],[c_1036,c_1586]) ).
tff(c_622,plain,
! [Y_32,Z_33] : ( multiply(inverse(Y_32),Y_32) = divide(Z_33,Z_33) ),
inference(superposition,[status(thm),theory(equality)],[c_9,c_384]) ).
tff(c_8,plain,
( ( multiply(b4,a4) != multiply(a4,b4) )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ) ),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_204,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_650,plain,
! [Z_33] : ( multiply(inverse(a1),a1) != divide(Z_33,Z_33) ),
inference(superposition,[status(thm),theory(equality)],[c_622,c_204]) ).
tff(c_3746,plain,
! [Z_85] : ( multiply(a1,inverse(a1)) != divide(Z_85,Z_85) ),
inference(demodulation,[status(thm),theory(equality)],[c_1623,c_650]) ).
tff(c_3754,plain,
! [Z_85,Z_8] : ( divide(Z_85,Z_85) != divide(Z_8,Z_8) ),
inference(superposition,[status(thm),theory(equality)],[c_917,c_3746]) ).
tff(c_4135,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3754,c_310]) ).
tff(c_4136,plain,
( ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(b4,a4) != multiply(a4,b4) ) ),
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_4408,plain,
multiply(b4,a4) != multiply(a4,b4),
inference(splitLeft,[status(thm)],[c_4136]) ).
tff(c_5644,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5493,c_4408]) ).
tff(c_5645,plain,
( ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 ) ),
inference(splitRight,[status(thm)],[c_4136]) ).
tff(c_5871,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(splitLeft,[status(thm)],[c_5645]) ).
tff(c_5873,plain,
! [Z_94] : ( multiply(divide(Z_94,Z_94),a2) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_4345,c_5871]) ).
tff(c_5874,plain,
inverse(inverse(a2)) != a2,
inference(demodulation,[status(thm),theory(equality)],[c_45,c_5873]) ).
tff(c_6418,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6359,c_5874]) ).
tff(c_6419,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitRight,[status(thm)],[c_5645]) ).
tff(c_8118,plain,
multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)),
inference(demodulation,[status(thm),theory(equality)],[c_7775,c_6419]) ).
tff(c_143503,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7775,c_22101,c_7775,c_22101,c_8118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP088-1 : TPTP v9.0.0. Bugfixed v2.7.0.
% 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.14/0.34 % Computer : n019.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 21:16:17 EDT 2025
% 0.14/0.34 % CPUTime :
% 34.18/22.58 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.30/22.59
% 34.30/22.59 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------