%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP040-3 : 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 : n009.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:51 PM UTC 2025
% Result : Unsatisfiable 12.07s 4.19s
% Output : CNFRefutation 12.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 17
% Syntax : Number of formulae : 93 ( 44 unt; 0 typ; 0 def)
% Number of atoms : 185 ( 13 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 182 ( 90 ~; 92 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 144 ( 144 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ product > subgroup_member > multiply > element_in_O2 > #nlpp > inverse > identity > d > c > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(product,type,
product: ( $i * $i * $i ) > $o ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b,type,
b: $i ).
tff(element_in_O2,type,
element_in_O2: ( $i * $i ) > $i ).
tff(d,type,
d: $i ).
tff(identity,type,
identity: $i ).
tff(subgroup_member,type,
subgroup_member: $i > $o ).
tff(c,type,
c: $i ).
tff(f_143,axiom,
subgroup_member(b),
file(unknown,unknown) ).
tff(f_55,axiom,
! [X] : product(X,inverse(X),identity),
file(unknown,unknown) ).
tff(f_125,axiom,
! [A,B,C] :
( ~ subgroup_member(A)
| ~ subgroup_member(B)
| ~ product(A,inverse(B),C)
| subgroup_member(C) ),
file(unknown,unknown) ).
tff(f_134,axiom,
! [A,B] :
( subgroup_member(element_in_O2(A,B))
| subgroup_member(B)
| subgroup_member(A) ),
file(unknown,unknown) ).
tff(f_49,axiom,
! [X] : product(identity,X,X),
file(unknown,unknown) ).
tff(f_142,axiom,
~ subgroup_member(a),
file(unknown,unknown) ).
tff(f_145,axiom,
~ subgroup_member(d),
file(unknown,unknown) ).
tff(f_58,axiom,
! [X,Y] : product(X,Y,multiply(X,Y)),
file(unknown,unknown) ).
tff(f_67,axiom,
! [X,Y,Z,W] :
( ~ product(X,Y,Z)
| ~ product(X,Y,W)
| ( Z = W ) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X] : product(inverse(X),X,identity),
file(unknown,unknown) ).
tff(f_51,axiom,
! [X] : product(X,identity,X),
file(unknown,unknown) ).
tff(f_89,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_146,axiom,
product(b,inverse(a),c),
file(unknown,unknown) ).
tff(f_78,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_149,axiom,
! [A] : ( inverse(inverse(A)) = A ),
file(unknown,unknown) ).
tff(f_147,axiom,
product(a,c,d),
file(unknown,unknown) ).
tff(f_140,axiom,
! [A,B] :
( product(A,element_in_O2(A,B),B)
| subgroup_member(B)
| subgroup_member(A) ),
file(unknown,unknown) ).
tff(c_26,plain,
subgroup_member(b),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_8,plain,
! [X_4] : product(X_4,inverse(X_4),identity),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_92,plain,
! [C_46,A_47,B_48] :
( subgroup_member(C_46)
| ~ product(A_47,inverse(B_48),C_46)
| ~ subgroup_member(B_48)
| ~ subgroup_member(A_47) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_120,plain,
! [X_4] :
( subgroup_member(identity)
| ~ subgroup_member(X_4) ),
inference(resolution,[status(thm)],[c_8,c_92]) ).
tff(c_122,plain,
! [X_4] : ~ subgroup_member(X_4),
inference(splitLeft,[status(thm)],[c_120]) ).
tff(c_20,plain,
! [A_26,B_27] :
( subgroup_member(A_26)
| subgroup_member(B_27)
| subgroup_member(element_in_O2(A_26,B_27)) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_127,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_122,c_122,c_122,c_20]) ).
tff(c_128,plain,
subgroup_member(identity),
inference(splitRight,[status(thm)],[c_120]) ).
tff(c_2,plain,
! [X_1] : product(identity,X_1,X_1),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_121,plain,
! [B_48] :
( subgroup_member(inverse(B_48))
| ~ subgroup_member(B_48)
| ~ subgroup_member(identity) ),
inference(resolution,[status(thm)],[c_2,c_92]) ).
tff(c_431,plain,
! [B_48] :
( subgroup_member(inverse(B_48))
| ~ subgroup_member(B_48) ),
inference(demodulation,[status(thm),theory(equality)],[c_128,c_121]) ).
tff(c_24,plain,
~ subgroup_member(a),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_28,plain,
~ subgroup_member(d),
inference(cnfTransformation,[status(thm)],[f_145]) ).
tff(c_10,plain,
! [X_5,Y_6] : product(X_5,Y_6,multiply(X_5,Y_6)),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_67,plain,
! [Z_42,W_43,X_44,Y_45] :
( ( Z_42 = W_43 )
| ~ product(X_44,Y_45,W_43)
| ~ product(X_44,Y_45,Z_42) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_255,plain,
! [Z_65,X_66] :
( ( Z_65 = X_66 )
| ~ product(identity,X_66,Z_65) ),
inference(resolution,[status(thm)],[c_2,c_67]) ).
tff(c_277,plain,
! [Y_6] : ( multiply(identity,Y_6) = Y_6 ),
inference(resolution,[status(thm)],[c_10,c_255]) ).
tff(c_6,plain,
! [X_3] : product(inverse(X_3),X_3,identity),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_4,plain,
! [X_2] : product(X_2,identity,X_2),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_229,plain,
! [X_60,U_61,Z_64,W_63,V_62,Y_59] :
( product(U_61,Z_64,W_63)
| ~ product(X_60,V_62,W_63)
| ~ product(Y_59,Z_64,V_62)
| ~ product(X_60,Y_59,U_61) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_803,plain,
! [U_106,Z_107,X_108,Y_109] :
( product(U_106,Z_107,X_108)
| ~ product(Y_109,Z_107,identity)
| ~ product(X_108,Y_109,U_106) ),
inference(resolution,[status(thm)],[c_4,c_229]) ).
tff(c_844,plain,
! [U_112,X_113,X_114] :
( product(U_112,X_113,X_114)
| ~ product(X_114,inverse(X_113),U_112) ),
inference(resolution,[status(thm)],[c_6,c_803]) ).
tff(c_873,plain,
! [X_5,X_113] : product(multiply(X_5,inverse(X_113)),X_113,X_5),
inference(resolution,[status(thm)],[c_10,c_844]) ).
tff(c_30,plain,
product(b,inverse(a),c),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_876,plain,
product(c,a,b),
inference(resolution,[status(thm)],[c_30,c_844]) ).
tff(c_129,plain,
! [U_51,Z_53,Y_50,X_52,W_49,V_54] :
( product(X_52,V_54,W_49)
| ~ product(U_51,Z_53,W_49)
| ~ product(Y_50,Z_53,V_54)
| ~ product(X_52,Y_50,U_51) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_1661,plain,
! [X_143,V_144,X_145,Y_146] :
( product(X_143,V_144,X_145)
| ~ product(Y_146,X_145,V_144)
| ~ product(X_143,Y_146,identity) ),
inference(resolution,[status(thm)],[c_2,c_129]) ).
tff(c_1964,plain,
! [X_156] :
( product(X_156,b,a)
| ~ product(X_156,c,identity) ),
inference(resolution,[status(thm)],[c_876,c_1661]) ).
tff(c_1968,plain,
product(multiply(identity,inverse(c)),b,a),
inference(resolution,[status(thm)],[c_873,c_1964]) ).
tff(c_1974,plain,
product(inverse(c),b,a),
inference(demodulation,[status(thm),theory(equality)],[c_277,c_1968]) ).
tff(c_34,plain,
! [A_30] : ( inverse(inverse(A_30)) = A_30 ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_109,plain,
! [C_46,A_47,A_30] :
( subgroup_member(C_46)
| ~ product(A_47,A_30,C_46)
| ~ subgroup_member(inverse(A_30))
| ~ subgroup_member(A_47) ),
inference(superposition,[status(thm),theory(equality)],[c_34,c_92]) ).
tff(c_2009,plain,
( subgroup_member(a)
| ~ subgroup_member(inverse(b))
| ~ subgroup_member(inverse(c)) ),
inference(resolution,[status(thm)],[c_1974,c_109]) ).
tff(c_2023,plain,
( ~ subgroup_member(inverse(b))
| ~ subgroup_member(inverse(c)) ),
inference(negUnitSimplification,[status(thm)],[c_24,c_2009]) ).
tff(c_2052,plain,
~ subgroup_member(inverse(c)),
inference(splitLeft,[status(thm)],[c_2023]) ).
tff(c_2056,plain,
~ subgroup_member(c),
inference(resolution,[status(thm)],[c_431,c_2052]) ).
tff(c_32,plain,
product(a,c,d),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_1713,plain,
! [X_147] :
( product(X_147,d,c)
| ~ product(X_147,a,identity) ),
inference(resolution,[status(thm)],[c_32,c_1661]) ).
tff(c_85,plain,
! [X_5,Y_6,Z_42] :
( ( multiply(X_5,Y_6) = Z_42 )
| ~ product(X_5,Y_6,Z_42) ),
inference(resolution,[status(thm)],[c_10,c_67]) ).
tff(c_1776,plain,
! [X_150] :
( ( multiply(X_150,d) = c )
| ~ product(X_150,a,identity) ),
inference(resolution,[status(thm)],[c_1713,c_85]) ).
tff(c_1784,plain,
multiply(multiply(identity,inverse(a)),d) = c,
inference(resolution,[status(thm)],[c_873,c_1776]) ).
tff(c_1791,plain,
multiply(inverse(a),d) = c,
inference(demodulation,[status(thm),theory(equality)],[c_277,c_1784]) ).
tff(c_1808,plain,
product(inverse(a),d,c),
inference(superposition,[status(thm),theory(equality)],[c_1791,c_10]) ).
tff(c_22,plain,
! [A_28,B_29] :
( subgroup_member(A_28)
| subgroup_member(B_29)
| product(A_28,element_in_O2(A_28,B_29),B_29) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_2655,plain,
! [U_184,Z_185,Y_186,X_187] :
( product(U_184,Z_185,identity)
| ~ product(Y_186,Z_185,X_187)
| ~ product(inverse(X_187),Y_186,U_184) ),
inference(resolution,[status(thm)],[c_6,c_229]) ).
tff(c_19189,plain,
! [U_497,A_498,B_499] :
( product(U_497,element_in_O2(A_498,B_499),identity)
| ~ product(inverse(B_499),A_498,U_497)
| subgroup_member(A_498)
| subgroup_member(B_499) ),
inference(resolution,[status(thm)],[c_22,c_2655]) ).
tff(c_19319,plain,
( product(c,element_in_O2(d,a),identity)
| subgroup_member(d)
| subgroup_member(a) ),
inference(resolution,[status(thm)],[c_1808,c_19189]) ).
tff(c_19435,plain,
product(c,element_in_O2(d,a),identity),
inference(negUnitSimplification,[status(thm)],[c_24,c_28,c_19319]) ).
tff(c_2772,plain,
! [Y_193,U_190,Y_192,Z_191,X_194] :
( product(U_190,Z_191,multiply(X_194,Y_192))
| ~ product(Y_193,Z_191,Y_192)
| ~ product(X_194,Y_193,U_190) ),
inference(resolution,[status(thm)],[c_10,c_229]) ).
tff(c_7554,plain,
! [U_316,X_317,X_318] :
( product(U_316,identity,multiply(X_317,X_318))
| ~ product(X_317,X_318,U_316) ),
inference(resolution,[status(thm)],[c_4,c_2772]) ).
tff(c_173,plain,
! [Z_56,X_57] :
( ( Z_56 = X_57 )
| ~ product(X_57,identity,Z_56) ),
inference(resolution,[status(thm)],[c_4,c_67]) ).
tff(c_189,plain,
! [X_5] : ( multiply(X_5,identity) = X_5 ),
inference(resolution,[status(thm)],[c_10,c_173]) ).
tff(c_635,plain,
! [U_91,Z_92,X_93,Y_94] :
( product(U_91,Z_92,X_93)
| ~ product(Y_94,Z_92,X_93)
| ~ product(identity,Y_94,U_91) ),
inference(resolution,[status(thm)],[c_2,c_229]) ).
tff(c_5740,plain,
! [U_277,Y_278,X_279] :
( product(U_277,Y_278,multiply(X_279,Y_278))
| ~ product(identity,X_279,U_277) ),
inference(resolution,[status(thm)],[c_10,c_635]) ).
tff(c_5140,plain,
! [U_260,X_261,X_262] :
( product(U_260,X_261,multiply(X_262,X_261))
| ~ product(X_262,identity,U_260) ),
inference(resolution,[status(thm)],[c_2,c_2772]) ).
tff(c_190,plain,
inverse(identity) = identity,
inference(resolution,[status(thm)],[c_6,c_173]) ).
tff(c_18,plain,
! [C_25,A_23,B_24] :
( subgroup_member(C_25)
| ~ product(A_23,inverse(B_24),C_25)
| ~ subgroup_member(B_24)
| ~ subgroup_member(A_23) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_198,plain,
! [C_25,A_23] :
( subgroup_member(C_25)
| ~ product(A_23,identity,C_25)
| ~ subgroup_member(identity)
| ~ subgroup_member(A_23) ),
inference(superposition,[status(thm),theory(equality)],[c_190,c_18]) ).
tff(c_211,plain,
! [C_25,A_23] :
( subgroup_member(C_25)
| ~ product(A_23,identity,C_25)
| ~ subgroup_member(A_23) ),
inference(demodulation,[status(thm),theory(equality)],[c_128,c_198]) ).
tff(c_5268,plain,
! [X_262,U_260] :
( subgroup_member(multiply(X_262,identity))
| ~ subgroup_member(U_260)
| ~ product(X_262,identity,U_260) ),
inference(resolution,[status(thm)],[c_5140,c_211]) ).
tff(c_5416,plain,
! [X_262,U_260] :
( subgroup_member(X_262)
| ~ subgroup_member(U_260)
| ~ product(X_262,identity,U_260) ),
inference(demodulation,[status(thm),theory(equality)],[c_189,c_5268]) ).
tff(c_5751,plain,
! [U_277,X_279] :
( subgroup_member(U_277)
| ~ subgroup_member(multiply(X_279,identity))
| ~ product(identity,X_279,U_277) ),
inference(resolution,[status(thm)],[c_5740,c_5416]) ).
tff(c_5984,plain,
! [U_277,X_279] :
( subgroup_member(U_277)
| ~ subgroup_member(X_279)
| ~ product(identity,X_279,U_277) ),
inference(demodulation,[status(thm),theory(equality)],[c_189,c_5751]) ).
tff(c_7558,plain,
! [X_317,X_318] :
( subgroup_member(multiply(X_317,X_318))
| ~ subgroup_member(identity)
| ~ product(X_317,X_318,identity) ),
inference(resolution,[status(thm)],[c_7554,c_5984]) ).
tff(c_8497,plain,
! [X_333,X_334] :
( subgroup_member(multiply(X_333,X_334))
| ~ product(X_333,X_334,identity) ),
inference(demodulation,[status(thm),theory(equality)],[c_128,c_7558]) ).
tff(c_942,plain,
! [X_119,X_120] : product(multiply(X_119,inverse(X_120)),X_120,X_119),
inference(resolution,[status(thm)],[c_10,c_844]) ).
tff(c_978,plain,
! [X_119,B_24] :
( subgroup_member(X_119)
| ~ subgroup_member(B_24)
| ~ subgroup_member(multiply(X_119,inverse(inverse(B_24)))) ),
inference(resolution,[status(thm)],[c_942,c_18]) ).
tff(c_1018,plain,
! [X_119,B_24] :
( subgroup_member(X_119)
| ~ subgroup_member(B_24)
| ~ subgroup_member(multiply(X_119,B_24)) ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_978]) ).
tff(c_8574,plain,
! [X_333,X_334] :
( subgroup_member(X_333)
| ~ subgroup_member(X_334)
| ~ product(X_333,X_334,identity) ),
inference(resolution,[status(thm)],[c_8497,c_1018]) ).
tff(c_19455,plain,
( subgroup_member(c)
| ~ subgroup_member(element_in_O2(d,a)) ),
inference(resolution,[status(thm)],[c_19435,c_8574]) ).
tff(c_19488,plain,
~ subgroup_member(element_in_O2(d,a)),
inference(negUnitSimplification,[status(thm)],[c_2056,c_19455]) ).
tff(c_19509,plain,
( subgroup_member(d)
| subgroup_member(a) ),
inference(resolution,[status(thm)],[c_20,c_19488]) ).
tff(c_19513,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24,c_28,c_19509]) ).
tff(c_19514,plain,
~ subgroup_member(inverse(b)),
inference(splitRight,[status(thm)],[c_2023]) ).
tff(c_19519,plain,
~ subgroup_member(b),
inference(resolution,[status(thm)],[c_431,c_19514]) ).
tff(c_19523,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_19519]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP040-3 : TPTP v9.0.0. Released v1.0.0.
% 0.12/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.12/0.34 % Computer : n009.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % 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:12:56 EDT 2025
% 0.12/0.34 % CPUTime :
% 12.07/4.19 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.07/4.20
% 12.07/4.20 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------