%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP028-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 : n026.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:48 PM UTC 2025
% Result : Unsatisfiable 5.77s 2.37s
% Output : CNFRefutation 5.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 7
% Syntax : Number of formulae : 53 ( 32 unt; 0 typ; 0 def)
% Number of atoms : 87 ( 24 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 70 ( 36 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 0 con; 1-2 aty)
% Number of variables : 164 ( 164 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ product > right_solution > multiply > left_solution > #nlpp > not_identity
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(product,type,
product: ( $i * $i * $i ) > $o ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(right_solution,type,
right_solution: ( $i * $i ) > $i ).
tff(left_solution,type,
left_solution: ( $i * $i ) > $i ).
tff(not_identity,type,
not_identity: $i > $i ).
tff(f_50,axiom,
! [X,Y] : product(X,Y,multiply(X,Y)),
file(unknown,unknown) ).
tff(f_87,axiom,
! [X,Y] : product(X,right_solution(X,Y),Y),
file(unknown,unknown) ).
tff(f_59,axiom,
! [X,Y,Z,W] :
( ~ product(X,Y,Z)
| ~ product(X,Y,W)
| ( Z = W ) ),
file(unknown,unknown) ).
tff(f_85,axiom,
! [X,Y] : product(left_solution(X,Y),X,Y),
file(unknown,unknown) ).
tff(f_81,axiom,
! [W,U,Z,X,Y,V] :
( ~ product(X,Y,U)
| ~ product(Y,Z,V)
| ~ product(X,V,W)
| product(U,Z,W) ),
file(unknown,unknown) ).
tff(f_70,axiom,
! [W,U,Z,X,Y,V] :
( ~ product(X,Y,U)
| ~ product(Y,Z,V)
| ~ product(U,Z,W)
| product(X,V,W) ),
file(unknown,unknown) ).
tff(f_91,axiom,
! [X] : ~ product(not_identity(X),X,not_identity(X)),
file(unknown,unknown) ).
tff(c_2,plain,
! [X_1,Y_2] : product(X_1,Y_2,multiply(X_1,Y_2)),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_12,plain,
! [X_21,Y_22] : product(X_21,right_solution(X_21,Y_22),Y_22),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_19,plain,
! [Z_31,W_32,X_33,Y_34] :
( ( Z_31 = W_32 )
| ~ product(X_33,Y_34,W_32)
| ~ product(X_33,Y_34,Z_31) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_63,plain,
! [Z_46,Y_47,X_48] :
( ( Z_46 = Y_47 )
| ~ product(X_48,right_solution(X_48,Y_47),Z_46) ),
inference(resolution,[status(thm)],[c_12,c_19]) ).
tff(c_73,plain,
! [X_1,Y_47] : ( multiply(X_1,right_solution(X_1,Y_47)) = Y_47 ),
inference(resolution,[status(thm)],[c_2,c_63]) ).
tff(c_10,plain,
! [X_19,Y_20] : product(left_solution(X_19,Y_20),X_19,Y_20),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_74,plain,
! [X_51,Y_53,Z_50,W_52,U_49,V_54] :
( product(U_49,Z_50,W_52)
| ~ product(X_51,V_54,W_52)
| ~ product(Y_53,Z_50,V_54)
| ~ product(X_51,Y_53,U_49) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_146,plain,
! [Y_76,Y_72,U_75,X_73,Z_74] :
( product(U_75,Z_74,multiply(X_73,Y_76))
| ~ product(Y_72,Z_74,Y_76)
| ~ product(X_73,Y_72,U_75) ),
inference(resolution,[status(thm)],[c_2,c_74]) ).
tff(c_593,plain,
! [U_113,X_114,X_115,Y_116] :
( product(U_113,X_114,multiply(X_115,Y_116))
| ~ product(X_115,left_solution(X_114,Y_116),U_113) ),
inference(resolution,[status(thm)],[c_10,c_146]) ).
tff(c_638,plain,
! [Y_122,X_123,Y_124] : product(Y_122,X_123,multiply(left_solution(left_solution(X_123,Y_124),Y_122),Y_124)),
inference(resolution,[status(thm)],[c_10,c_593]) ).
tff(c_28,plain,
! [X_1,Y_2,Z_31] :
( ( multiply(X_1,Y_2) = Z_31 )
| ~ product(X_1,Y_2,Z_31) ),
inference(resolution,[status(thm)],[c_2,c_19]) ).
tff(c_766,plain,
! [X_128,Y_129,Y_130] : ( multiply(left_solution(left_solution(X_128,Y_129),Y_130),Y_129) = multiply(Y_130,X_128) ),
inference(resolution,[status(thm)],[c_638,c_28]) ).
tff(c_795,plain,
! [X_131,Y_132,Y_133] : product(left_solution(left_solution(X_131,Y_132),Y_133),Y_132,multiply(Y_133,X_131)),
inference(superposition,[status(thm),theory(equality)],[c_766,c_2]) ).
tff(c_29,plain,
! [V_38,Z_35,W_36,U_37,Y_40,X_39] :
( product(X_39,V_38,W_36)
| ~ product(U_37,Z_35,W_36)
| ~ product(Y_40,Z_35,V_38)
| ~ product(X_39,Y_40,U_37) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_364,plain,
! [Y_100,X_98,X_99,Y_97,V_96] :
( product(X_99,V_96,Y_100)
| ~ product(Y_97,right_solution(X_98,Y_100),V_96)
| ~ product(X_99,Y_97,X_98) ),
inference(resolution,[status(thm)],[c_12,c_29]) ).
tff(c_387,plain,
! [X_99,Y_22,X_21] :
( product(X_99,Y_22,Y_22)
| ~ product(X_99,X_21,X_21) ),
inference(resolution,[status(thm)],[c_12,c_364]) ).
tff(c_2140,plain,
! [X_193,Y_194,Y_195] : product(left_solution(left_solution(X_193,multiply(Y_194,X_193)),Y_194),Y_195,Y_195),
inference(resolution,[status(thm)],[c_795,c_387]) ).
tff(c_26,plain,
! [Z_31,Y_20,X_19] :
( ( Z_31 = Y_20 )
| ~ product(left_solution(X_19,Y_20),X_19,Z_31) ),
inference(resolution,[status(thm)],[c_10,c_19]) ).
tff(c_2242,plain,
! [X_196,Y_197] : ( left_solution(X_196,multiply(Y_197,X_196)) = Y_197 ),
inference(resolution,[status(thm)],[c_2140,c_26]) ).
tff(c_2371,plain,
! [X_1,Y_47] : ( left_solution(right_solution(X_1,Y_47),Y_47) = X_1 ),
inference(superposition,[status(thm),theory(equality)],[c_73,c_2242]) ).
tff(c_39,plain,
! [Z_41,Y_42,X_43] :
( ( Z_41 = Y_42 )
| ~ product(left_solution(X_43,Y_42),X_43,Z_41) ),
inference(resolution,[status(thm)],[c_10,c_19]) ).
tff(c_49,plain,
! [Y_2,Y_42] : ( multiply(left_solution(Y_2,Y_42),Y_2) = Y_42 ),
inference(resolution,[status(thm)],[c_2,c_39]) ).
tff(c_113,plain,
! [Y_64,Y_60,Z_61,X_62,U_63] :
( product(U_63,Z_61,Y_64)
| ~ product(Y_60,Z_61,right_solution(X_62,Y_64))
| ~ product(X_62,Y_60,U_63) ),
inference(resolution,[status(thm)],[c_12,c_74]) ).
tff(c_172,plain,
! [U_80,X_81,X_82,Y_83] :
( product(U_80,right_solution(X_81,right_solution(X_82,Y_83)),Y_83)
| ~ product(X_82,X_81,U_80) ),
inference(resolution,[status(thm)],[c_12,c_113]) ).
tff(c_27,plain,
! [Z_31,Y_22,X_21] :
( ( Z_31 = Y_22 )
| ~ product(X_21,right_solution(X_21,Y_22),Z_31) ),
inference(resolution,[status(thm)],[c_12,c_19]) ).
tff(c_203,plain,
! [X_84,Y_85,X_86] :
( ( right_solution(X_84,Y_85) = Y_85 )
| ~ product(X_84,X_86,X_86) ),
inference(resolution,[status(thm)],[c_172,c_27]) ).
tff(c_211,plain,
! [Y_20,Y_85] : ( right_solution(left_solution(Y_20,Y_20),Y_85) = Y_85 ),
inference(resolution,[status(thm)],[c_10,c_203]) ).
tff(c_856,plain,
! [Y_134,Y_135,Y_136] : ( multiply(left_solution(left_solution(right_solution(Y_134,Y_135),Y_136),Y_134),Y_136) = Y_135 ),
inference(resolution,[status(thm)],[c_638,c_27]) ).
tff(c_1766,plain,
! [Y_180,Y_181,Y_182] : ( multiply(left_solution(left_solution(Y_180,Y_181),left_solution(Y_182,Y_182)),Y_181) = Y_180 ),
inference(superposition,[status(thm),theory(equality)],[c_211,c_856]) ).
tff(c_1810,plain,
! [Y_180,Y_181,Y_182] : product(left_solution(left_solution(Y_180,Y_181),left_solution(Y_182,Y_182)),Y_181,Y_180),
inference(superposition,[status(thm),theory(equality)],[c_1766,c_2]) ).
tff(c_2706,plain,
! [U_200,X_201,Y_202,X_203] :
( product(U_200,right_solution(X_201,Y_202),multiply(X_203,Y_202))
| ~ product(X_203,X_201,U_200) ),
inference(resolution,[status(thm)],[c_12,c_146]) ).
tff(c_2922,plain,
! [X_206,Y_207,X_208] :
( ( multiply(X_206,Y_207) = Y_207 )
| ~ product(X_206,X_208,X_208) ),
inference(resolution,[status(thm)],[c_2706,c_27]) ).
tff(c_3492,plain,
! [Y_227,Y_228,Y_229] : ( multiply(left_solution(left_solution(Y_227,Y_227),left_solution(Y_228,Y_228)),Y_229) = Y_229 ),
inference(resolution,[status(thm)],[c_1810,c_2922]) ).
tff(c_691,plain,
! [X_125,X_126,Y_127] : product(multiply(X_125,left_solution(X_126,Y_127)),X_126,multiply(X_125,Y_127)),
inference(resolution,[status(thm)],[c_2,c_593]) ).
tff(c_893,plain,
! [Y_137,Y_138,X_139] : product(multiply(left_solution(Y_137,Y_138),left_solution(X_139,Y_137)),X_139,Y_138),
inference(superposition,[status(thm),theory(equality)],[c_49,c_691]) ).
tff(c_933,plain,
! [Y_137,Y_138,X_139] : ( multiply(multiply(left_solution(Y_137,Y_138),left_solution(X_139,Y_137)),X_139) = Y_138 ),
inference(resolution,[status(thm)],[c_893,c_28]) ).
tff(c_3542,plain,
! [X_139,Y_227,Y_228] : ( multiply(left_solution(X_139,left_solution(Y_227,Y_227)),X_139) = left_solution(Y_228,Y_228) ),
inference(superposition,[status(thm),theory(equality)],[c_3492,c_933]) ).
tff(c_122,plain,
! [U_65,X_66,Y_67,X_68] :
( product(U_65,X_66,Y_67)
| ~ product(X_68,left_solution(X_66,right_solution(X_68,Y_67)),U_65) ),
inference(resolution,[status(thm)],[c_10,c_113]) ).
tff(c_128,plain,
! [X_69,X_70,Y_71] : product(multiply(X_69,left_solution(X_70,right_solution(X_69,Y_71))),X_70,Y_71),
inference(resolution,[status(thm)],[c_2,c_122]) ).
tff(c_142,plain,
! [X_69,X_70,Y_71] : ( multiply(multiply(X_69,left_solution(X_70,right_solution(X_69,Y_71))),X_70) = Y_71 ),
inference(resolution,[status(thm)],[c_128,c_28]) ).
tff(c_4690,plain,
! [X_243,X_244,Y_245] : ( multiply(X_243,left_solution(X_244,right_solution(X_243,Y_245))) = left_solution(X_244,Y_245) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_2242]) ).
tff(c_4768,plain,
! [X_243,X_139,Y_227,Y_245] : ( multiply(X_243,multiply(left_solution(X_139,left_solution(Y_227,Y_227)),X_139)) = left_solution(right_solution(X_243,Y_245),Y_245) ),
inference(superposition,[status(thm),theory(equality)],[c_3542,c_4690]) ).
tff(c_4933,plain,
! [X_250,Y_251] : ( multiply(X_250,left_solution(Y_251,Y_251)) = X_250 ),
inference(demodulation,[status(thm),theory(equality)],[c_2371,c_49,c_4768]) ).
tff(c_5130,plain,
! [X_252,Y_253] : product(X_252,left_solution(Y_253,Y_253),X_252),
inference(superposition,[status(thm),theory(equality)],[c_4933,c_2]) ).
tff(c_14,plain,
! [X_23] : ~ product(not_identity(X_23),X_23,not_identity(X_23)),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_5229,plain,
$false,
inference(resolution,[status(thm)],[c_5130,c_14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.10 % Problem : GRP028-2 : TPTP v9.0.0. Released v1.1.0.
% 0.06/0.11 % 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.12/0.31 % Computer : n026.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Mon Apr 7 21:12:38 EDT 2025
% 0.17/0.31 % CPUTime :
% 5.77/2.37 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.77/2.38
% 5.77/2.38 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------