%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP131-1.002 : 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/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 : n012.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:17 PM UTC 2025
% Result : Unsatisfiable 37.27s 25.33s
% Output : CNFRefutation 37.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 8
% Syntax : Number of formulae : 43 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 170 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 224 ( 97 ~; 127 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 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 : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 93 ( 93 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ product > equalish > group_element > #nlpp > e_2 > e_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(group_element,type,
group_element: $i > $o ).
tff(e_2,type,
e_2: $i ).
tff(product,type,
product: ( $i * $i * $i ) > $o ).
tff(equalish,type,
equalish: ( $i * $i ) > $o ).
tff(e_1,type,
e_1: $i ).
tff(f_34,axiom,
group_element(e_2),
file(unknown,unknown) ).
tff(f_33,axiom,
group_element(e_1),
file(unknown,unknown) ).
tff(f_36,axiom,
~ equalish(e_1,e_2),
file(unknown,unknown) ).
tff(f_48,axiom,
! [X,Y] :
( ~ group_element(X)
| ~ group_element(Y)
| product(X,Y,e_1)
| product(X,Y,e_2) ),
file(unknown,unknown) ).
tff(f_72,axiom,
! [W,Y,X,Z] :
( ~ product(W,Y,X)
| ~ product(Z,Y,X)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_86,axiom,
! [Y1,X1,Z2,Y2,X2,Z1] :
( ~ product(X1,Y1,Z1)
| ~ product(X2,Y2,Z1)
| ~ product(Z2,Y1,X1)
| ~ product(Z2,Y2,X2)
| equalish(X1,X2) ),
file(unknown,unknown) ).
tff(f_64,axiom,
! [X,W,Y,Z] :
( ~ product(X,W,Y)
| ~ product(X,Z,Y)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_38,axiom,
~ equalish(e_2,e_1),
file(unknown,unknown) ).
tff(c_4,plain,
group_element(e_2),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_2,plain,
group_element(e_1),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_6,plain,
~ equalish(e_1,e_2),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_10,plain,
! [X_1,Y_2] :
( product(X_1,Y_2,e_2)
| product(X_1,Y_2,e_1)
| ~ group_element(Y_2)
| ~ group_element(X_1) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_24,plain,
! [X_39,Y_40] :
( product(X_39,Y_40,e_2)
| product(X_39,Y_40,e_1)
| ~ group_element(Y_40)
| ~ group_element(X_39) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_16,plain,
! [W_11,Z_14,Y_12,X_13] :
( equalish(W_11,Z_14)
| ~ product(Z_14,Y_12,X_13)
| ~ product(W_11,Y_12,X_13) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_34,plain,
! [W_41,X_42,Y_43] :
( equalish(W_41,X_42)
| ~ product(W_41,Y_43,e_2)
| product(X_42,Y_43,e_1)
| ~ group_element(Y_43)
| ~ group_element(X_42) ),
inference(resolution,[status(thm)],[c_24,c_16]) ).
tff(c_37,plain,
! [X_1,X_42,Y_2] :
( equalish(X_1,X_42)
| product(X_42,Y_2,e_1)
| ~ group_element(X_42)
| product(X_1,Y_2,e_1)
| ~ group_element(Y_2)
| ~ group_element(X_1) ),
inference(resolution,[status(thm)],[c_10,c_34]) ).
tff(c_100,plain,
! [Z2_60,X1_59,Y2_64,X2_63,Z1_62,Y1_61] :
( equalish(X1_59,X2_63)
| ~ product(Z2_60,Y2_64,X2_63)
| ~ product(Z2_60,Y1_61,X1_59)
| ~ product(X2_63,Y2_64,Z1_62)
| ~ product(X1_59,Y1_61,Z1_62) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_207,plain,
! [X_79,X1_80,Y_81,Y1_78,Z1_77] :
( equalish(X1_80,e_2)
| ~ product(X_79,Y1_78,X1_80)
| ~ product(e_2,Y_81,Z1_77)
| ~ product(X1_80,Y1_78,Z1_77)
| product(X_79,Y_81,e_1)
| ~ group_element(Y_81)
| ~ group_element(X_79) ),
inference(resolution,[status(thm)],[c_10,c_100]) ).
tff(c_213,plain,
! [Y_81,X_42,X_1,Z1_77,Y_2] :
( equalish(e_1,e_2)
| ~ product(e_2,Y_81,Z1_77)
| ~ product(e_1,Y_2,Z1_77)
| product(X_42,Y_81,e_1)
| ~ group_element(Y_81)
| equalish(X_1,X_42)
| ~ group_element(X_42)
| product(X_1,Y_2,e_1)
| ~ group_element(Y_2)
| ~ group_element(X_1) ),
inference(resolution,[status(thm)],[c_37,c_207]) ).
tff(c_420,plain,
! [X_137,Y_136,Z1_135,Y_139,X_138] :
( ~ product(e_2,Y_136,Z1_135)
| ~ product(e_1,Y_139,Z1_135)
| product(X_137,Y_136,e_1)
| ~ group_element(Y_136)
| equalish(X_138,X_137)
| ~ group_element(X_137)
| product(X_138,Y_139,e_1)
| ~ group_element(Y_139)
| ~ group_element(X_138) ),
inference(negUnitSimplification,[status(thm)],[c_6,c_213]) ).
tff(c_435,plain,
! [Y_139,X_137,Y_2,X_138] :
( ~ product(e_1,Y_139,e_2)
| product(X_137,Y_2,e_1)
| equalish(X_138,X_137)
| ~ group_element(X_137)
| product(X_138,Y_139,e_1)
| ~ group_element(Y_139)
| ~ group_element(X_138)
| product(e_2,Y_2,e_1)
| ~ group_element(Y_2)
| ~ group_element(e_2) ),
inference(resolution,[status(thm)],[c_10,c_420]) ).
tff(c_9552,plain,
! [Y_448,X_449,Y_450,X_451] :
( ~ product(e_1,Y_448,e_2)
| product(X_449,Y_450,e_1)
| equalish(X_451,X_449)
| ~ group_element(X_449)
| product(X_451,Y_448,e_1)
| ~ group_element(Y_448)
| ~ group_element(X_451)
| product(e_2,Y_450,e_1)
| ~ group_element(Y_450) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_435]) ).
tff(c_9555,plain,
! [X_449,Y_450,X_451,Y_2] :
( product(X_449,Y_450,e_1)
| equalish(X_451,X_449)
| ~ group_element(X_449)
| product(X_451,Y_2,e_1)
| ~ group_element(X_451)
| product(e_2,Y_450,e_1)
| ~ group_element(Y_450)
| product(e_1,Y_2,e_1)
| ~ group_element(Y_2)
| ~ group_element(e_1) ),
inference(resolution,[status(thm)],[c_10,c_9552]) ).
tff(c_9558,plain,
! [X_449,Y_450,X_451,Y_2] :
( product(X_449,Y_450,e_1)
| equalish(X_451,X_449)
| ~ group_element(X_449)
| product(X_451,Y_2,e_1)
| ~ group_element(X_451)
| product(e_2,Y_450,e_1)
| ~ group_element(Y_450)
| product(e_1,Y_2,e_1)
| ~ group_element(Y_2) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_9555]) ).
tff(c_37552,plain,
! [X_449,Y_450,Y_2] :
( product(X_449,Y_450,e_1)
| equalish(e_1,X_449)
| ~ group_element(X_449)
| ~ group_element(e_1)
| product(e_2,Y_450,e_1)
| ~ group_element(Y_450)
| ~ group_element(Y_2)
| product(e_1,Y_2,e_1) ),
inference(factorization,[status(thm),theory(equality)],[c_9558]) ).
tff(c_37555,plain,
! [X_449,Y_450,Y_2] :
( product(X_449,Y_450,e_1)
| equalish(e_1,X_449)
| ~ group_element(X_449)
| product(e_2,Y_450,e_1)
| ~ group_element(Y_450)
| ~ group_element(Y_2)
| product(e_1,Y_2,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_37552]) ).
tff(c_41411,plain,
! [Y_2] :
( ~ group_element(Y_2)
| product(e_1,Y_2,e_1) ),
inference(splitLeft,[status(thm)],[c_37555]) ).
tff(c_41412,plain,
! [Y_777] :
( ~ group_element(Y_777)
| product(e_1,Y_777,e_1) ),
inference(splitLeft,[status(thm)],[c_37555]) ).
tff(c_14,plain,
! [W_8,Z_10,X_7,Y_9] :
( equalish(W_8,Z_10)
| ~ product(X_7,Z_10,Y_9)
| ~ product(X_7,W_8,Y_9) ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_42243,plain,
! [W_780,Y_781] :
( equalish(W_780,Y_781)
| ~ product(e_1,W_780,e_1)
| ~ group_element(Y_781) ),
inference(resolution,[status(thm)],[c_41412,c_14]) ).
tff(c_42799,plain,
! [Y_782,Y_783] :
( equalish(Y_782,Y_783)
| ~ group_element(Y_783)
| ~ group_element(Y_782) ),
inference(resolution,[status(thm)],[c_41411,c_42243]) ).
tff(c_8,plain,
~ equalish(e_2,e_1),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_42802,plain,
( ~ group_element(e_1)
| ~ group_element(e_2) ),
inference(resolution,[status(thm)],[c_42799,c_8]) ).
tff(c_42809,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2,c_42802]) ).
tff(c_42810,plain,
! [X_449,Y_450] :
( product(X_449,Y_450,e_1)
| equalish(e_1,X_449)
| ~ group_element(X_449)
| product(e_2,Y_450,e_1)
| ~ group_element(Y_450) ),
inference(splitRight,[status(thm)],[c_37555]) ).
tff(c_42822,plain,
! [Y_450] :
( equalish(e_1,e_2)
| ~ group_element(e_2)
| ~ group_element(Y_450)
| product(e_2,Y_450,e_1) ),
inference(factorization,[status(thm),theory(equality)],[c_42810]) ).
tff(c_42825,plain,
! [Y_450] :
( equalish(e_1,e_2)
| ~ group_element(Y_450)
| product(e_2,Y_450,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_42822]) ).
tff(c_42826,plain,
! [Y_450] :
( ~ group_element(Y_450)
| product(e_2,Y_450,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_6,c_42825]) ).
tff(c_43649,plain,
! [Y_786] :
( ~ group_element(Y_786)
| product(e_2,Y_786,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_6,c_42825]) ).
tff(c_44486,plain,
! [W_789,Y_790] :
( equalish(W_789,Y_790)
| ~ product(e_2,W_789,e_1)
| ~ group_element(Y_790) ),
inference(resolution,[status(thm)],[c_43649,c_14]) ).
tff(c_45042,plain,
! [Y_791,Y_792] :
( equalish(Y_791,Y_792)
| ~ group_element(Y_792)
| ~ group_element(Y_791) ),
inference(resolution,[status(thm)],[c_42826,c_44486]) ).
tff(c_45045,plain,
( ~ group_element(e_1)
| ~ group_element(e_2) ),
inference(resolution,[status(thm)],[c_45042,c_8]) ).
tff(c_45052,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2,c_45045]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP131-1.002 : TPTP v9.0.0. Released v1.2.0.
% 0.03/0.13 % 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.14/0.34 % Computer : n012.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:26:00 EDT 2025
% 0.14/0.34 % CPUTime :
% 37.27/25.33 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 37.27/25.34
% 37.27/25.34 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------