%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP439-1 : TPTP v9.0.0. Released v2.6.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 : n023.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:26:14 PM UTC 2025
% Result : Unsatisfiable 30.79s 13.62s
% Output : CNFRefutation 30.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 2
% Syntax : Number of formulae : 39 ( 39 unt; 0 typ; 0 def)
% Number of atoms : 39 ( 38 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 153 ( 153 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > #nlpp > inverse > b1 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b1,type,
b1: $i ).
tff(f_23,axiom,
! [A,B,C,D] : ( inverse(multiply(A,multiply(B,multiply(multiply(inverse(B),C),inverse(multiply(D,multiply(A,C))))))) = D ),
file(unknown,unknown) ).
tff(f_25,axiom,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file(unknown,unknown) ).
tff(c_5,plain,
! [A_5,B_6,C_7,D_8] : ( inverse(multiply(A_5,multiply(B_6,multiply(multiply(inverse(B_6),C_7),inverse(multiply(D_8,multiply(A_5,C_7))))))) = D_8 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_2,plain,
! [A_1,B_2,C_3,D_4] : ( inverse(multiply(A_1,multiply(B_2,multiply(multiply(inverse(B_2),C_3),inverse(multiply(D_4,multiply(A_1,C_3))))))) = D_4 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_141,plain,
! [A_24,C_23,B_21,D_20,A_26,D_22,C_25] : ( inverse(multiply(A_26,multiply(multiply(A_24,multiply(B_21,multiply(multiply(inverse(B_21),C_23),inverse(multiply(D_20,multiply(A_24,C_23)))))),multiply(multiply(D_20,C_25),inverse(multiply(D_22,multiply(A_26,C_25))))))) = D_22 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_11,plain,
! [B_6,C_7,D_8,B_2,A_5] : ( inverse(multiply(B_6,multiply(B_2,multiply(multiply(inverse(B_2),multiply(multiply(inverse(B_6),C_7),inverse(multiply(D_8,multiply(A_5,C_7))))),D_8)))) = A_5 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_1736,plain,
! [A_85,D_92,A_88,C_84,C_86,B_89,B_91,D_87,B_90] : ( multiply(A_88,multiply(B_90,multiply(multiply(inverse(B_90),C_86),inverse(multiply(D_87,multiply(A_88,C_86)))))) = inverse(multiply(B_89,multiply(B_91,multiply(multiply(inverse(B_91),multiply(multiply(inverse(B_89),multiply(multiply(D_87,C_84),inverse(multiply(D_92,multiply(A_85,C_84))))),D_92)),A_85)))) ),
inference(superposition,[status(thm),theory(equality)],[c_141,c_11]) ).
tff(c_26,plain,
! [D_9,C_11,B_10,A_12,B_13] : ( inverse(multiply(B_10,multiply(B_13,multiply(multiply(inverse(B_13),multiply(multiply(inverse(B_10),C_11),inverse(multiply(D_9,multiply(A_12,C_11))))),D_9)))) = A_12 ),
inference(superposition,[status(thm),theory(equality)],[c_5,c_2]) ).
tff(c_44,plain,
! [D_9,C_11,B_2,B_10,A_12,B_13] : ( inverse(multiply(B_13,multiply(B_2,multiply(multiply(inverse(B_2),multiply(multiply(inverse(B_13),multiply(multiply(inverse(B_10),C_11),inverse(multiply(D_9,multiply(A_12,C_11))))),D_9)),A_12)))) = B_10 ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_2]) ).
tff(c_2048,plain,
! [A_88,B_90,C_86,B_10] : ( multiply(A_88,multiply(B_90,multiply(multiply(inverse(B_90),C_86),inverse(multiply(inverse(B_10),multiply(A_88,C_86)))))) = B_10 ),
inference(superposition,[status(thm),theory(equality)],[c_1736,c_44]) ).
tff(c_2694,plain,
! [A_102,B_103,C_104,B_105] : ( multiply(A_102,multiply(B_103,multiply(multiply(inverse(B_103),C_104),inverse(multiply(inverse(B_105),multiply(A_102,C_104)))))) = B_105 ),
inference(superposition,[status(thm),theory(equality)],[c_1736,c_44]) ).
tff(c_4320,plain,
! [B_126,B_125,A_128,B_124,C_123,B_127] : ( multiply(A_128,multiply(B_127,multiply(multiply(inverse(B_127),multiply(B_124,multiply(multiply(inverse(B_124),C_123),inverse(multiply(inverse(B_126),multiply(A_128,C_123)))))),inverse(multiply(inverse(B_125),B_126))))) = B_125 ),
inference(superposition,[status(thm),theory(equality)],[c_2048,c_2694]) ).
tff(c_4660,plain,
! [B_127,B_10,B_125] : ( multiply(inverse(B_127),multiply(B_127,multiply(B_10,inverse(multiply(inverse(B_125),B_10))))) = B_125 ),
inference(superposition,[status(thm),theory(equality)],[c_2048,c_4320]) ).
tff(c_4942,plain,
! [B_129,B_130,B_131] : ( multiply(inverse(B_129),multiply(B_129,multiply(B_130,inverse(multiply(inverse(B_131),B_130))))) = B_131 ),
inference(superposition,[status(thm),theory(equality)],[c_2048,c_4320]) ).
tff(c_7706,plain,
! [B_155,D_156,B_153,A_157,B_154] : ( inverse(multiply(A_157,multiply(B_155,multiply(B_154,inverse(multiply(D_156,multiply(A_157,multiply(B_155,multiply(B_153,inverse(multiply(inverse(B_154),B_153))))))))))) = D_156 ),
inference(superposition,[status(thm),theory(equality)],[c_4942,c_2]) ).
tff(c_8026,plain,
! [B_127,B_125,D_156] : ( inverse(multiply(inverse(B_127),multiply(B_127,multiply(B_125,inverse(multiply(D_156,B_125)))))) = D_156 ),
inference(superposition,[status(thm),theory(equality)],[c_4660,c_7706]) ).
tff(c_8195,plain,
! [B_158,B_159,D_160] : ( inverse(multiply(inverse(B_158),multiply(B_158,multiply(B_159,inverse(multiply(D_160,B_159)))))) = D_160 ),
inference(superposition,[status(thm),theory(equality)],[c_4660,c_7706]) ).
tff(c_8313,plain,
! [B_158,B_90,B_159,D_160] : ( multiply(B_158,multiply(B_90,multiply(multiply(inverse(B_90),multiply(B_159,inverse(multiply(D_160,B_159)))),D_160))) = B_158 ),
inference(superposition,[status(thm),theory(equality)],[c_8195,c_2048]) ).
tff(c_10607,plain,
! [B_180,B_181,B_182,D_183] : ( multiply(B_180,multiply(B_181,multiply(multiply(inverse(B_181),multiply(B_182,inverse(multiply(D_183,B_182)))),D_183))) = B_180 ),
inference(superposition,[status(thm),theory(equality)],[c_8195,c_2048]) ).
tff(c_10800,plain,
! [D_183,A_88,B_10,B_182,B_90,B_181] : ( multiply(A_88,multiply(B_90,multiply(inverse(B_90),inverse(multiply(inverse(B_10),multiply(A_88,multiply(B_181,multiply(multiply(inverse(B_181),multiply(B_182,inverse(multiply(D_183,B_182)))),D_183)))))))) = B_10 ),
inference(superposition,[status(thm),theory(equality)],[c_10607,c_2048]) ).
tff(c_11343,plain,
! [A_184,B_185,B_186] : ( multiply(A_184,multiply(B_185,multiply(inverse(B_185),inverse(multiply(inverse(B_186),A_184))))) = B_186 ),
inference(demodulation,[status(thm),theory(equality)],[c_8313,c_10800]) ).
tff(c_14716,plain,
! [B_209,B_210,D_211,B_212] : ( multiply(multiply(B_209,multiply(B_210,inverse(multiply(D_211,B_210)))),multiply(B_212,multiply(inverse(B_212),D_211))) = B_209 ),
inference(superposition,[status(thm),theory(equality)],[c_8026,c_11343]) ).
tff(c_34091,plain,
! [B_334,B_333,B_332,D_336,B_335] : ( multiply(B_334,multiply(B_332,inverse(multiply(D_336,B_332)))) = inverse(multiply(B_335,multiply(B_333,multiply(multiply(inverse(B_333),multiply(inverse(B_335),D_336)),inverse(B_334))))) ),
inference(superposition,[status(thm),theory(equality)],[c_14716,c_2]) ).
tff(c_15213,plain,
! [C_215,A_216,B_214,B_217,D_213] : ( inverse(multiply(inverse(B_217),multiply(B_217,multiply(multiply(B_214,multiply(multiply(inverse(B_214),C_215),inverse(multiply(D_213,multiply(A_216,C_215))))),D_213)))) = A_216 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_8195]) ).
tff(c_15639,plain,
! [B_159,D_160,B_214,B_217,B_90,D_213,B_158] : ( inverse(multiply(inverse(B_217),multiply(B_217,multiply(multiply(B_214,multiply(multiply(inverse(B_214),multiply(B_90,multiply(multiply(inverse(B_90),multiply(B_159,inverse(multiply(D_160,B_159)))),D_160))),inverse(multiply(D_213,B_158)))),D_213)))) = B_158 ),
inference(superposition,[status(thm),theory(equality)],[c_8313,c_15213]) ).
tff(c_15919,plain,
! [B_217,B_214,D_213,B_158] : ( inverse(multiply(inverse(B_217),multiply(B_217,multiply(multiply(B_214,multiply(inverse(B_214),inverse(multiply(D_213,B_158)))),D_213)))) = B_158 ),
inference(demodulation,[status(thm),theory(equality)],[c_8313,c_15639]) ).
tff(c_36500,plain,
! [B_337,B_338,B_339] : ( multiply(B_337,multiply(B_338,inverse(multiply(inverse(multiply(inverse(B_337),B_339)),B_338)))) = B_339 ),
inference(superposition,[status(thm),theory(equality)],[c_34091,c_15919]) ).
tff(c_3086,plain,
! [B_103,B_2,C_3,D_4,B_105] : ( multiply(B_2,multiply(B_103,multiply(multiply(inverse(B_103),multiply(multiply(inverse(B_2),C_3),inverse(multiply(D_4,multiply(inverse(B_105),C_3))))),D_4))) = B_105 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_2694]) ).
tff(c_10784,plain,
! [D_183,B_103,B_2,D_4,B_105,B_182,B_181] : ( multiply(B_2,multiply(B_103,multiply(multiply(inverse(B_103),multiply(multiply(inverse(B_2),multiply(B_181,multiply(multiply(inverse(B_181),multiply(B_182,inverse(multiply(D_183,B_182)))),D_183))),inverse(multiply(D_4,inverse(B_105))))),D_4))) = B_105 ),
inference(superposition,[status(thm),theory(equality)],[c_10607,c_3086]) ).
tff(c_11288,plain,
! [B_2,B_103,D_4,B_105] : ( multiply(B_2,multiply(B_103,multiply(multiply(inverse(B_103),multiply(inverse(B_2),inverse(multiply(D_4,inverse(B_105))))),D_4))) = B_105 ),
inference(demodulation,[status(thm),theory(equality)],[c_8313,c_10784]) ).
tff(c_36666,plain,
! [B_2,B_103,B_339] : ( multiply(B_2,multiply(B_103,multiply(B_339,inverse(multiply(inverse(inverse(B_103)),B_339))))) = B_2 ),
inference(superposition,[status(thm),theory(equality)],[c_36500,c_11288]) ).
tff(c_39503,plain,
! [D_343,A_344,D_345,B_346] : ( multiply(multiply(D_343,multiply(A_344,multiply(inverse(A_344),D_345))),multiply(B_346,inverse(multiply(D_345,B_346)))) = D_343 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_34091]) ).
tff(c_58126,plain,
! [D_390,A_391,B_392] : ( multiply(inverse(multiply(D_390,multiply(A_391,multiply(inverse(A_391),inverse(B_392))))),D_390) = B_392 ),
inference(superposition,[status(thm),theory(equality)],[c_39503,c_4660]) ).
tff(c_59594,plain,
! [B_393,B_394] : ( multiply(inverse(inverse(B_393)),inverse(B_393)) = multiply(inverse(B_394),B_394) ),
inference(superposition,[status(thm),theory(equality)],[c_36666,c_58126]) ).
tff(c_59289,plain,
! [B_103,B_2] : ( multiply(inverse(inverse(B_103)),inverse(B_103)) = multiply(inverse(B_2),B_2) ),
inference(superposition,[status(thm),theory(equality)],[c_36666,c_58126]) ).
tff(c_61731,plain,
! [B_396,B_395] : ( multiply(inverse(B_396),B_396) = multiply(inverse(B_395),B_395) ),
inference(superposition,[status(thm),theory(equality)],[c_59594,c_59289]) ).
tff(c_4,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_63849,plain,
! [B_396] : ( multiply(inverse(a1),a1) != multiply(inverse(B_396),B_396) ),
inference(superposition,[status(thm),theory(equality)],[c_61731,c_4]) ).
tff(c_64209,plain,
$false,
inference(reflexivity,[status(thm),theory(equality)],[c_63849]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GRP439-1 : TPTP v9.0.0. Released v2.6.0.
% 0.11/0.12 % 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.32 % Computer : n023.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 21:50:24 EDT 2025
% 0.12/0.33 % CPUTime :
% 30.79/13.62 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.79/13.63
% 30.79/13.63 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------