%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : RNG039-2 : TPTP v9.0.0. Released v1.0.0.
% 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 : 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 08:31:21 PM UTC 2025
% Result : Unsatisfiable 21.36s 8.46s
% Output : CNFRefutation 21.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 21
% Syntax : Number of formulae : 84 ( 43 unt; 0 typ; 0 def)
% Number of atoms : 139 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 117 ( 62 ~; 55 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 120 ( 120 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ sum > product > equalish > multiply > add > #nlpp > d > c > b > additive_identity > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(sum,type,
sum: ( $i * $i * $i ) > $o ).
tff(a,type,
a: $i ).
tff(product,type,
product: ( $i * $i * $i ) > $o ).
tff(additive_identity,type,
additive_identity: $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b,type,
b: $i ).
tff(add,type,
add: ( $i * $i ) > $i ).
tff(d,type,
d: $i ).
tff(equalish,type,
equalish: ( $i * $i ) > $o ).
tff(c,type,
c: $i ).
tff(f_303,axiom,
product(d,b,multiply(b,c)),
file(unknown,unknown) ).
tff(f_81,axiom,
! [X,Y,W,Z] :
( ~ equalish(X,Y)
| ~ product(X,W,Z)
| product(Y,W,Z) ),
file(unknown,unknown) ).
tff(f_229,axiom,
! [X] : product(additive_identity,X,additive_identity),
file(unknown,unknown) ).
tff(f_248,axiom,
! [X,Y,U,V] :
( ~ product(X,Y,U)
| ~ product(X,Y,V)
| equalish(U,V) ),
file(unknown,unknown) ).
tff(f_116,axiom,
! [X,Y] : product(X,Y,multiply(X,Y)),
file(unknown,unknown) ).
tff(f_307,axiom,
product(multiply(d,b),a,d),
file(unknown,unknown) ).
tff(f_73,axiom,
! [X,Y,W] :
( ~ equalish(X,Y)
| equalish(multiply(W,X),multiply(W,Y)) ),
file(unknown,unknown) ).
tff(f_298,axiom,
! [A,B] : product(multiply(A,B),B,multiply(A,B)),
file(unknown,unknown) ).
tff(f_231,axiom,
! [X] : product(X,additive_identity,additive_identity),
file(unknown,unknown) ).
tff(f_110,axiom,
! [X,Y,Z] :
( ~ equalish(X,Y)
| ~ equalish(Y,Z)
| equalish(X,Z) ),
file(unknown,unknown) ).
tff(f_97,axiom,
! [X,Y,W,Z] :
( ~ equalish(X,Y)
| ~ product(W,Z,X)
| product(W,Z,Y) ),
file(unknown,unknown) ).
tff(f_288,axiom,
! [A,B] : product(a,multiply(b,A),multiply(B,A)),
file(unknown,unknown) ).
tff(f_290,axiom,
product(a,multiply(b,c),c),
file(unknown,unknown) ).
tff(f_270,axiom,
! [A] : sum(A,A,additive_identity),
file(unknown,unknown) ).
tff(f_55,axiom,
! [X,Y,W,Z] :
( ~ equalish(X,Y)
| ~ sum(W,X,Z)
| sum(W,Y,Z) ),
file(unknown,unknown) ).
tff(f_149,axiom,
! [X,Y,Z] :
( ~ sum(X,Y,Z)
| sum(Y,X,Z) ),
file(unknown,unknown) ).
tff(f_264,axiom,
! [A,B,C,D] :
( ~ sum(A,B,C)
| ~ sum(A,D,C)
| equalish(D,B) ),
file(unknown,unknown) ).
tff(f_322,axiom,
~ equalish(c,d),
file(unknown,unknown) ).
tff(f_296,axiom,
product(a,d,multiply(c,a)),
file(unknown,unknown) ).
tff(f_89,axiom,
! [X,Y,W,Z] :
( ~ equalish(X,Y)
| ~ product(W,X,Z)
| product(W,Y,Z) ),
file(unknown,unknown) ).
tff(f_302,axiom,
product(multiply(c,a),b,c),
file(unknown,unknown) ).
tff(c_116,plain,
product(d,b,multiply(b,c)),
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_1213,plain,
! [Y_265,W_266,Z_267,X_268] :
( product(Y_265,W_266,Z_267)
| ~ product(X_268,W_266,Z_267)
| ~ equalish(X_268,Y_265) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_6157,plain,
! [Y_463] :
( product(Y_463,b,multiply(b,c))
| ~ equalish(d,Y_463) ),
inference(resolution,[status(thm)],[c_116,c_1213]) ).
tff(c_52,plain,
! [X_102] : product(additive_identity,X_102,additive_identity),
inference(cnfTransformation,[status(thm)],[f_229]) ).
tff(c_781,plain,
! [U_243,V_244,X_245,Y_246] :
( equalish(U_243,V_244)
| ~ product(X_245,Y_246,V_244)
| ~ product(X_245,Y_246,U_243) ),
inference(cnfTransformation,[status(thm)],[f_248]) ).
tff(c_894,plain,
! [U_243,X_102] :
( equalish(U_243,additive_identity)
| ~ product(additive_identity,X_102,U_243) ),
inference(resolution,[status(thm)],[c_52,c_781]) ).
tff(c_6190,plain,
( equalish(multiply(b,c),additive_identity)
| ~ equalish(d,additive_identity) ),
inference(resolution,[status(thm)],[c_6157,c_894]) ).
tff(c_6527,plain,
~ equalish(d,additive_identity),
inference(splitLeft,[status(thm)],[c_6190]) ).
tff(c_30,plain,
! [X_43,Y_44] : product(X_43,Y_44,multiply(X_43,Y_44)),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_10246,plain,
! [U_543,X_544,Y_545] :
( equalish(U_543,multiply(X_544,Y_545))
| ~ product(X_544,Y_545,U_543) ),
inference(resolution,[status(thm)],[c_30,c_781]) ).
tff(c_1339,plain,
! [Y_265,X_102] :
( product(Y_265,X_102,additive_identity)
| ~ equalish(additive_identity,Y_265) ),
inference(resolution,[status(thm)],[c_52,c_1213]) ).
tff(c_122,plain,
product(multiply(d,b),a,d),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_8898,plain,
! [U_511] :
( equalish(U_511,d)
| ~ product(multiply(d,b),a,U_511) ),
inference(resolution,[status(thm)],[c_122,c_781]) ).
tff(c_8941,plain,
( equalish(additive_identity,d)
| ~ equalish(additive_identity,multiply(d,b)) ),
inference(resolution,[status(thm)],[c_1339,c_8898]) ).
tff(c_8965,plain,
~ equalish(additive_identity,multiply(d,b)),
inference(splitLeft,[status(thm)],[c_8941]) ).
tff(c_10323,plain,
~ product(d,b,additive_identity),
inference(resolution,[status(thm)],[c_10246,c_8965]) ).
tff(c_14,plain,
! [W_24,X_22,Y_23] :
( equalish(multiply(W_24,X_22),multiply(W_24,Y_23))
| ~ equalish(X_22,Y_23) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_108,plain,
! [A_135,B_136] : product(multiply(A_135,B_136),B_136,multiply(A_135,B_136)),
inference(cnfTransformation,[status(thm)],[f_298]) ).
tff(c_54,plain,
! [X_103] : product(X_103,additive_identity,additive_identity),
inference(cnfTransformation,[status(thm)],[f_231]) ).
tff(c_1142,plain,
! [U_262,X_263] :
( equalish(U_262,additive_identity)
| ~ product(X_263,additive_identity,U_262) ),
inference(resolution,[status(thm)],[c_54,c_781]) ).
tff(c_1207,plain,
! [A_264] : equalish(multiply(A_264,additive_identity),additive_identity),
inference(resolution,[status(thm)],[c_108,c_1142]) ).
tff(c_24,plain,
! [X_38,Z_40,Y_39] :
( equalish(X_38,Z_40)
| ~ equalish(Y_39,Z_40)
| ~ equalish(X_38,Y_39) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_6357,plain,
! [X_470,A_471] :
( equalish(X_470,additive_identity)
| ~ equalish(X_470,multiply(A_471,additive_identity)) ),
inference(resolution,[status(thm)],[c_1207,c_24]) ).
tff(c_10779,plain,
! [W_554,X_555] :
( equalish(multiply(W_554,X_555),additive_identity)
| ~ equalish(X_555,additive_identity) ),
inference(resolution,[status(thm)],[c_14,c_6357]) ).
tff(c_1012,plain,
! [W_258,Z_259,Y_260,X_261] :
( product(W_258,Z_259,Y_260)
| ~ product(W_258,Z_259,X_261)
| ~ equalish(X_261,Y_260) ),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_1132,plain,
! [Y_260] :
( product(d,b,Y_260)
| ~ equalish(multiply(b,c),Y_260) ),
inference(resolution,[status(thm)],[c_116,c_1012]) ).
tff(c_10787,plain,
( product(d,b,additive_identity)
| ~ equalish(c,additive_identity) ),
inference(resolution,[status(thm)],[c_10779,c_1132]) ).
tff(c_10799,plain,
~ equalish(c,additive_identity),
inference(negUnitSimplification,[status(thm)],[c_10323,c_10787]) ).
tff(c_92,plain,
! [A_132,B_133] : product(a,multiply(b,A_132),multiply(B_133,A_132)),
inference(cnfTransformation,[status(thm)],[f_288]) ).
tff(c_96,plain,
product(a,multiply(b,c),c),
inference(cnfTransformation,[status(thm)],[f_290]) ).
tff(c_27884,plain,
! [U_791] :
( equalish(U_791,c)
| ~ product(a,multiply(b,c),U_791) ),
inference(resolution,[status(thm)],[c_96,c_781]) ).
tff(c_28024,plain,
! [B_792] : equalish(multiply(B_792,c),c),
inference(resolution,[status(thm)],[c_92,c_27884]) ).
tff(c_1127,plain,
! [X_43,Y_44,Y_260] :
( product(X_43,Y_44,Y_260)
| ~ equalish(multiply(X_43,Y_44),Y_260) ),
inference(resolution,[status(thm)],[c_30,c_1012]) ).
tff(c_28055,plain,
! [B_793] : product(B_793,c,c),
inference(resolution,[status(thm)],[c_28024,c_1127]) ).
tff(c_28063,plain,
equalish(c,additive_identity),
inference(resolution,[status(thm)],[c_28055,c_894]) ).
tff(c_28089,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10799,c_28063]) ).
tff(c_28090,plain,
equalish(additive_identity,d),
inference(splitRight,[status(thm)],[c_8941]) ).
tff(c_68,plain,
! [A_124] : sum(A_124,A_124,additive_identity),
inference(cnfTransformation,[status(thm)],[f_270]) ).
tff(c_523,plain,
! [W_212,Y_213,Z_214,X_215] :
( sum(W_212,Y_213,Z_214)
| ~ sum(W_212,X_215,Z_214)
| ~ equalish(X_215,Y_213) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_565,plain,
! [A_220,Y_221] :
( sum(A_220,Y_221,additive_identity)
| ~ equalish(A_220,Y_221) ),
inference(resolution,[status(thm)],[c_68,c_523]) ).
tff(c_38,plain,
! [Y_60,X_59,Z_61] :
( sum(Y_60,X_59,Z_61)
| ~ sum(X_59,Y_60,Z_61) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_571,plain,
! [Y_221,A_220] :
( sum(Y_221,A_220,additive_identity)
| ~ equalish(A_220,Y_221) ),
inference(resolution,[status(thm)],[c_565,c_38]) ).
tff(c_933,plain,
! [D_250,B_251,A_252,C_253] :
( equalish(D_250,B_251)
| ~ sum(A_252,D_250,C_253)
| ~ sum(A_252,B_251,C_253) ),
inference(cnfTransformation,[status(thm)],[f_264]) ).
tff(c_1542,plain,
! [A_284,B_285] :
( equalish(A_284,B_285)
| ~ sum(A_284,B_285,additive_identity) ),
inference(resolution,[status(thm)],[c_68,c_933]) ).
tff(c_1600,plain,
! [Y_221,A_220] :
( equalish(Y_221,A_220)
| ~ equalish(A_220,Y_221) ),
inference(resolution,[status(thm)],[c_571,c_1542]) ).
tff(c_28093,plain,
equalish(d,additive_identity),
inference(resolution,[status(thm)],[c_28090,c_1600]) ).
tff(c_28099,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6527,c_28093]) ).
tff(c_28101,plain,
equalish(d,additive_identity),
inference(splitRight,[status(thm)],[c_6190]) ).
tff(c_28159,plain,
equalish(additive_identity,d),
inference(resolution,[status(thm)],[c_28101,c_1600]) ).
tff(c_28558,plain,
! [X_801] :
( equalish(X_801,d)
| ~ equalish(X_801,additive_identity) ),
inference(resolution,[status(thm)],[c_28159,c_24]) ).
tff(c_148,plain,
~ equalish(c,d),
inference(cnfTransformation,[status(thm)],[f_322]) ).
tff(c_28583,plain,
~ equalish(c,additive_identity),
inference(resolution,[status(thm)],[c_28558,c_148]) ).
tff(c_106,plain,
product(a,d,multiply(c,a)),
inference(cnfTransformation,[status(thm)],[f_296]) ).
tff(c_659,plain,
! [W_236,Y_237,Z_238,X_239] :
( product(W_236,Y_237,Z_238)
| ~ product(W_236,X_239,Z_238)
| ~ equalish(X_239,Y_237) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_40092,plain,
! [Y_936] :
( product(a,Y_936,multiply(c,a))
| ~ equalish(d,Y_936) ),
inference(resolution,[status(thm)],[c_106,c_659]) ).
tff(c_893,plain,
! [U_243,X_103] :
( equalish(U_243,additive_identity)
| ~ product(X_103,additive_identity,U_243) ),
inference(resolution,[status(thm)],[c_54,c_781]) ).
tff(c_40118,plain,
( equalish(multiply(c,a),additive_identity)
| ~ equalish(d,additive_identity) ),
inference(resolution,[status(thm)],[c_40092,c_893]) ).
tff(c_40135,plain,
equalish(multiply(c,a),additive_identity),
inference(demodulation,[status(thm),theory(equality)],[c_28101,c_40118]) ).
tff(c_114,plain,
product(multiply(c,a),b,c),
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_1331,plain,
! [Y_265] :
( product(Y_265,b,c)
| ~ equalish(multiply(c,a),Y_265) ),
inference(resolution,[status(thm)],[c_114,c_1213]) ).
tff(c_40152,plain,
product(additive_identity,b,c),
inference(resolution,[status(thm)],[c_40135,c_1331]) ).
tff(c_40182,plain,
equalish(c,additive_identity),
inference(resolution,[status(thm)],[c_40152,c_894]) ).
tff(c_40202,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28583,c_40182]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : RNG039-2 : TPTP v9.0.0. Released v1.0.0.
% 0.03/0.14 % 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.12/0.35 % Computer : n019.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Tue Apr 8 18:30:17 EDT 2025
% 0.12/0.35 % CPUTime :
% 21.36/8.46 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.39/8.47
% 21.39/8.47 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------