%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP123-8.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 : n021.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 4.28s 2.04s
% Output : CNFRefutation 4.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 15
% Syntax : Number of formulae : 49 ( 25 unt; 0 typ; 0 def)
% Number of atoms : 99 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 95 ( 45 ~; 50 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 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 : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 55 ( 55 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ product2 > product1 > product > next > greater > equalish > cycle > group_element > #nlpp > e_3 > e_2 > e_1 > e_0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(group_element,type,
group_element: $i > $o ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff(cycle,type,
cycle: ( $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(e_0,type,
e_0: $i ).
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_121,axiom,
~ equalish(e_1,e_2),
file(unknown,unknown) ).
tff(f_123,axiom,
~ equalish(e_1,e_3),
file(unknown,unknown) ).
tff(f_117,axiom,
group_element(e_1),
file(unknown,unknown) ).
tff(f_119,axiom,
group_element(e_3),
file(unknown,unknown) ).
tff(f_143,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_169,axiom,
! [X] : product1(X,X,X),
file(unknown,unknown) ).
tff(f_167,axiom,
! [W,Y,X,Z] :
( ~ product1(W,Y,X)
| ~ product1(Z,Y,X)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_129,axiom,
~ equalish(e_3,e_1),
file(unknown,unknown) ).
tff(f_127,axiom,
~ equalish(e_2,e_3),
file(unknown,unknown) ).
tff(f_131,axiom,
~ equalish(e_3,e_2),
file(unknown,unknown) ).
tff(f_118,axiom,
group_element(e_2),
file(unknown,unknown) ).
tff(f_159,axiom,
! [X,W,Y,Z] :
( ~ product1(X,W,Y)
| ~ product1(X,Z,Y)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_215,axiom,
! [X,Y,Z1,Z2] :
( ~ product1(X,Y,Z1)
| ~ product1(Z1,Y,Z2)
| product2(Z2,X,Y) ),
file(unknown,unknown) ).
tff(f_207,axiom,
! [X] : product2(X,X,X),
file(unknown,unknown) ).
tff(f_189,axiom,
! [X,Y,W,Z] :
( ~ product2(X,Y,W)
| ~ product2(X,Y,Z)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(c_40,plain,
~ equalish(e_1,e_2),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_42,plain,
~ equalish(e_1,e_3),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_34,plain,
group_element(e_1),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_38,plain,
group_element(e_3),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_149,plain,
! [X_105,Y_106] :
( product1(X_105,Y_106,e_3)
| product1(X_105,Y_106,e_2)
| product1(X_105,Y_106,e_1)
| ~ group_element(Y_106)
| ~ group_element(X_105) ),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_60,plain,
! [X_35] : product1(X_35,X_35,X_35),
inference(cnfTransformation,[status(thm)],[f_169]) ).
tff(c_125,plain,
! [W_89,Z_90,Y_91,X_92] :
( equalish(W_89,Z_90)
| ~ product1(Z_90,Y_91,X_92)
| ~ product1(W_89,Y_91,X_92) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_128,plain,
! [W_89,X_35] :
( equalish(W_89,X_35)
| ~ product1(W_89,X_35,X_35) ),
inference(resolution,[status(thm)],[c_60,c_125]) ).
tff(c_155,plain,
! [X_105] :
( equalish(X_105,e_3)
| product1(X_105,e_3,e_2)
| product1(X_105,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(X_105) ),
inference(resolution,[status(thm)],[c_149,c_128]) ).
tff(c_173,plain,
! [X_105] :
( equalish(X_105,e_3)
| product1(X_105,e_3,e_2)
| product1(X_105,e_3,e_1)
| ~ group_element(X_105) ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_155]) ).
tff(c_48,plain,
~ equalish(e_3,e_1),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_46,plain,
~ equalish(e_2,e_3),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_50,plain,
~ equalish(e_3,e_2),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_36,plain,
group_element(e_2),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_519,plain,
! [X_146] :
( equalish(X_146,e_3)
| product1(X_146,e_3,e_2)
| product1(X_146,e_3,e_1)
| ~ group_element(X_146) ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_155]) ).
tff(c_99,plain,
! [W_75,Z_76,X_77,Y_78] :
( equalish(W_75,Z_76)
| ~ product1(X_77,Z_76,Y_78)
| ~ product1(X_77,W_75,Y_78) ),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_102,plain,
! [W_75,X_35] :
( equalish(W_75,X_35)
| ~ product1(X_35,W_75,X_35) ),
inference(resolution,[status(thm)],[c_60,c_99]) ).
tff(c_527,plain,
( equalish(e_3,e_2)
| equalish(e_2,e_3)
| product1(e_2,e_3,e_1)
| ~ group_element(e_2) ),
inference(resolution,[status(thm)],[c_519,c_102]) ).
tff(c_540,plain,
( equalish(e_3,e_2)
| equalish(e_2,e_3)
| product1(e_2,e_3,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_527]) ).
tff(c_541,plain,
product1(e_2,e_3,e_1),
inference(negUnitSimplification,[status(thm)],[c_46,c_50,c_540]) ).
tff(c_72,plain,
! [Z2_54,X_51,Y_52,Z1_53] :
( product2(Z2_54,X_51,Y_52)
| ~ product1(Z1_53,Y_52,Z2_54)
| ~ product1(X_51,Y_52,Z1_53) ),
inference(cnfTransformation,[status(thm)],[f_215]) ).
tff(c_641,plain,
! [X_153] :
( product2(e_1,X_153,e_3)
| ~ product1(X_153,e_3,e_2) ),
inference(resolution,[status(thm)],[c_541,c_72]) ).
tff(c_70,plain,
! [X_50] : product2(X_50,X_50,X_50),
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_115,plain,
! [W_83,Z_84,X_85,Y_86] :
( equalish(W_83,Z_84)
| ~ product2(X_85,Y_86,Z_84)
| ~ product2(X_85,Y_86,W_83) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_118,plain,
! [W_83,X_50] :
( equalish(W_83,X_50)
| ~ product2(X_50,X_50,W_83) ),
inference(resolution,[status(thm)],[c_70,c_115]) ).
tff(c_655,plain,
( equalish(e_3,e_1)
| ~ product1(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c_641,c_118]) ).
tff(c_672,plain,
~ product1(e_1,e_3,e_2),
inference(negUnitSimplification,[status(thm)],[c_48,c_655]) ).
tff(c_689,plain,
( equalish(e_1,e_3)
| product1(e_1,e_3,e_1)
| ~ group_element(e_1) ),
inference(resolution,[status(thm)],[c_173,c_672]) ).
tff(c_692,plain,
( equalish(e_1,e_3)
| product1(e_1,e_3,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_689]) ).
tff(c_693,plain,
product1(e_1,e_3,e_1),
inference(negUnitSimplification,[status(thm)],[c_42,c_692]) ).
tff(c_58,plain,
! [W_31,Z_34,Y_32,X_33] :
( equalish(W_31,Z_34)
| ~ product1(Z_34,Y_32,X_33)
| ~ product1(W_31,Y_32,X_33) ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_588,plain,
! [W_31] :
( equalish(W_31,e_2)
| ~ product1(W_31,e_3,e_1) ),
inference(resolution,[status(thm)],[c_541,c_58]) ).
tff(c_696,plain,
equalish(e_1,e_2),
inference(resolution,[status(thm)],[c_693,c_588]) ).
tff(c_711,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_40,c_696]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP123-8.003 : TPTP v9.0.0. Released v1.2.0.
% 0.12/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.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 21:19:58 EDT 2025
% 0.12/0.34 % CPUTime :
% 4.28/2.04 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.28/2.04
% 4.28/2.04 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------