%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP123-7.003 : TPTP v9.0.0. Released v1.2.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 : n011.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:04 PM UTC 2025
% Result : Unsatisfiable 6.46s 2.72s
% Output : CNFRefutation 6.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of formulae : 54 ( 24 unt; 0 typ; 0 def)
% Number of atoms : 118 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 119 ( 55 ~; 64 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 76 ( 76 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ product2 > product1 > product > next > greater > equalish > group_element > #nlpp > e_3 > e_2 > e_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(group_element,type,
group_element: $i > $o ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff(e_2,type,
e_2: $i ).
tff(product,type,
product: ( $i * $i * $i ) > $o ).
tff(next,type,
next: ( $i * $i ) > $o ).
tff(product1,type,
product1: ( $i * $i * $i ) > $o ).
tff(e_3,type,
e_3: $i ).
tff(equalish,type,
equalish: ( $i * $i ) > $o ).
tff(e_1,type,
e_1: $i ).
tff(product2,type,
product2: ( $i * $i * $i ) > $o ).
tff(f_54,axiom,
~ equalish(e_2,e_1),
file(unknown,unknown) ).
tff(f_52,axiom,
~ equalish(e_1,e_3),
file(unknown,unknown) ).
tff(f_46,axiom,
group_element(e_1),
file(unknown,unknown) ).
tff(f_47,axiom,
group_element(e_2),
file(unknown,unknown) ).
tff(f_72,axiom,
! [X,Y] :
( ~ group_element(X)
| ~ group_element(Y)
| product1(X,Y,e_1)
| product1(X,Y,e_2)
| product1(X,Y,e_3) ),
file(unknown,unknown) ).
tff(f_60,axiom,
~ equalish(e_3,e_2),
file(unknown,unknown) ).
tff(f_48,axiom,
group_element(e_3),
file(unknown,unknown) ).
tff(f_98,axiom,
! [X] : product1(X,X,X),
file(unknown,unknown) ).
tff(f_88,axiom,
! [X,W,Y,Z] :
( ~ product1(X,W,Y)
| ~ product1(X,Z,Y)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_96,axiom,
! [W,Y,X,Z] :
( ~ product1(W,Y,X)
| ~ product1(Z,Y,X)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_144,axiom,
! [X,Y,Z1,Z2] :
( ~ product1(X,Y,Z1)
| ~ product1(Z1,Y,Z2)
| product2(Z2,X,Y) ),
file(unknown,unknown) ).
tff(f_136,axiom,
! [X] : product2(X,X,X),
file(unknown,unknown) ).
tff(f_118,axiom,
! [X,Y,W,Z] :
( ~ product2(X,Y,W)
| ~ product2(X,Y,Z)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_126,axiom,
! [X,W,Y,Z] :
( ~ product2(X,W,Y)
| ~ product2(X,Z,Y)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(c_24,plain,
~ equalish(e_2,e_1),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_22,plain,
~ equalish(e_1,e_3),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_14,plain,
group_element(e_1),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_16,plain,
group_element(e_2),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_32,plain,
! [X_4,Y_5] :
( product1(X_4,Y_5,e_3)
| product1(X_4,Y_5,e_2)
| product1(X_4,Y_5,e_1)
| ~ group_element(Y_5)
| ~ group_element(X_4) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_30,plain,
~ equalish(e_3,e_2),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_18,plain,
group_element(e_3),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_40,plain,
! [X_18] : product1(X_18,X_18,X_18),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_221,plain,
! [X_99,Y_100] :
( product1(X_99,Y_100,e_3)
| product1(X_99,Y_100,e_2)
| product1(X_99,Y_100,e_1)
| ~ group_element(Y_100)
| ~ group_element(X_99) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_36,plain,
! [W_11,Z_13,X_10,Y_12] :
( equalish(W_11,Z_13)
| ~ product1(X_10,Z_13,Y_12)
| ~ product1(X_10,W_11,Y_12) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_333,plain,
! [W_105,Y_106,X_107] :
( equalish(W_105,Y_106)
| ~ product1(X_107,W_105,e_3)
| product1(X_107,Y_106,e_2)
| product1(X_107,Y_106,e_1)
| ~ group_element(Y_106)
| ~ group_element(X_107) ),
inference(resolution,[status(thm)],[c_221,c_36]) ).
tff(c_338,plain,
! [Y_106] :
( equalish(e_3,Y_106)
| product1(e_3,Y_106,e_2)
| product1(e_3,Y_106,e_1)
| ~ group_element(Y_106)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_40,c_333]) ).
tff(c_1160,plain,
! [Y_144] :
( equalish(e_3,Y_144)
| product1(e_3,Y_144,e_2)
| product1(e_3,Y_144,e_1)
| ~ group_element(Y_144) ),
inference(demodulation,[status(thm),theory(equality)],[c_18,c_338]) ).
tff(c_88,plain,
! [W_59,Z_60,Y_61,X_62] :
( equalish(W_59,Z_60)
| ~ product1(Z_60,Y_61,X_62)
| ~ product1(W_59,Y_61,X_62) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_91,plain,
! [W_59,X_18] :
( equalish(W_59,X_18)
| ~ product1(W_59,X_18,X_18) ),
inference(resolution,[status(thm)],[c_40,c_88]) ).
tff(c_1188,plain,
( equalish(e_3,e_2)
| product1(e_3,e_2,e_1)
| ~ group_element(e_2) ),
inference(resolution,[status(thm)],[c_1160,c_91]) ).
tff(c_1219,plain,
( equalish(e_3,e_2)
| product1(e_3,e_2,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_1188]) ).
tff(c_1220,plain,
product1(e_3,e_2,e_1),
inference(negUnitSimplification,[status(thm)],[c_30,c_1219]) ).
tff(c_52,plain,
! [Z2_37,X_34,Y_35,Z1_36] :
( product2(Z2_37,X_34,Y_35)
| ~ product1(Z1_36,Y_35,Z2_37)
| ~ product1(X_34,Y_35,Z1_36) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_1314,plain,
! [X_151] :
( product2(e_1,X_151,e_2)
| ~ product1(X_151,e_2,e_3) ),
inference(resolution,[status(thm)],[c_1220,c_52]) ).
tff(c_50,plain,
! [X_33] : product2(X_33,X_33,X_33),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_98,plain,
! [W_65,Z_66,X_67,Y_68] :
( equalish(W_65,Z_66)
| ~ product2(X_67,Y_68,Z_66)
| ~ product2(X_67,Y_68,W_65) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_101,plain,
! [W_65,X_33] :
( equalish(W_65,X_33)
| ~ product2(X_33,X_33,W_65) ),
inference(resolution,[status(thm)],[c_50,c_98]) ).
tff(c_1333,plain,
( equalish(e_2,e_1)
| ~ product1(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c_1314,c_101]) ).
tff(c_1357,plain,
~ product1(e_1,e_2,e_3),
inference(negUnitSimplification,[status(thm)],[c_24,c_1333]) ).
tff(c_1368,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(e_1) ),
inference(resolution,[status(thm)],[c_32,c_1357]) ).
tff(c_1371,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_16,c_1368]) ).
tff(c_1398,plain,
product1(e_1,e_2,e_1),
inference(splitLeft,[status(thm)],[c_1371]) ).
tff(c_38,plain,
! [W_14,Z_17,Y_15,X_16] :
( equalish(W_14,Z_17)
| ~ product1(Z_17,Y_15,X_16)
| ~ product1(W_14,Y_15,X_16) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_1260,plain,
! [W_14] :
( equalish(W_14,e_3)
| ~ product1(W_14,e_2,e_1) ),
inference(resolution,[status(thm)],[c_1220,c_38]) ).
tff(c_1416,plain,
equalish(e_1,e_3),
inference(resolution,[status(thm)],[c_1398,c_1260]) ).
tff(c_1433,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22,c_1416]) ).
tff(c_1434,plain,
product1(e_1,e_2,e_2),
inference(splitRight,[status(thm)],[c_1371]) ).
tff(c_128,plain,
! [Z2_83,X_84,Y_85,Z1_86] :
( product2(Z2_83,X_84,Y_85)
| ~ product1(Z1_86,Y_85,Z2_83)
| ~ product1(X_84,Y_85,Z1_86) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_132,plain,
! [X_87,X_88] :
( product2(X_87,X_88,X_87)
| ~ product1(X_88,X_87,X_87) ),
inference(resolution,[status(thm)],[c_40,c_128]) ).
tff(c_46,plain,
! [W_26,Z_28,X_25,Y_27] :
( equalish(W_26,Z_28)
| ~ product2(X_25,Z_28,Y_27)
| ~ product2(X_25,W_26,Y_27) ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_202,plain,
! [W_94,X_95,X_96] :
( equalish(W_94,X_95)
| ~ product2(X_96,W_94,X_96)
| ~ product1(X_95,X_96,X_96) ),
inference(resolution,[status(thm)],[c_132,c_46]) ).
tff(c_214,plain,
! [X_33,X_95] :
( equalish(X_33,X_95)
| ~ product1(X_95,X_33,X_33) ),
inference(resolution,[status(thm)],[c_50,c_202]) ).
tff(c_1440,plain,
equalish(e_2,e_1),
inference(resolution,[status(thm)],[c_1434,c_214]) ).
tff(c_1459,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_1440]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.08 % Problem : GRP123-7.003 : TPTP v9.0.0. Released v1.2.0.
% 0.02/0.08 % 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.08/0.27 % Computer : n011.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Mon Apr 7 21:19:33 EDT 2025
% 0.08/0.27 % CPUTime :
% 6.46/2.72 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.46/2.73
% 6.46/2.73 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------