%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP467-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 : n025.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:18 PM UTC 2025
% Result : Unsatisfiable 9.16s 3.21s
% Output : CNFRefutation 9.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 3
% Syntax : Number of formulae : 37 ( 37 unt; 0 typ; 0 def)
% Number of atoms : 37 ( 36 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 7 ( 2 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 : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 105 ( 105 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > divide > #nlpp > inverse > b2 > a2
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(divide,type,
divide: ( $i * $i ) > $i ).
tff(b2,type,
b2: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(a2,type,
a2: $i ).
tff(f_25,axiom,
! [A,B] : ( multiply(A,B) = divide(A,inverse(B)) ),
file(unknown,unknown) ).
tff(f_23,axiom,
! [A,B,C,D] : ( divide(divide(A,A),divide(B,divide(divide(C,divide(D,B)),inverse(D)))) = C ),
file(unknown,unknown) ).
tff(f_27,axiom,
multiply(multiply(inverse(b2),b2),a2) != a2,
file(unknown,unknown) ).
tff(c_4,plain,
! [A_5,B_6] : ( divide(A_5,inverse(B_6)) = multiply(A_5,B_6) ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_2,plain,
! [A_1,B_2,C_3,D_4] : ( divide(divide(A_1,A_1),divide(B_2,divide(divide(C_3,divide(D_4,B_2)),inverse(D_4)))) = C_3 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_17,plain,
! [A_9,B_10,C_11,D_12] : ( divide(divide(A_9,A_9),divide(B_10,multiply(divide(C_11,divide(D_12,B_10)),D_12))) = C_11 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2]) ).
tff(c_7,plain,
! [A_1,B_2,C_3,D_4] : ( divide(divide(A_1,A_1),divide(B_2,multiply(divide(C_3,divide(D_4,B_2)),D_4))) = C_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2]) ).
tff(c_106,plain,
! [A_24,A_25,C_22,D_23,B_21] : ( divide(divide(A_24,A_24),divide(multiply(divide(C_22,divide(D_23,B_21)),D_23),multiply(C_22,B_21))) = divide(A_25,A_25) ),
inference(superposition,[status(thm),theory(equality)],[c_17,c_7]) ).
tff(c_23,plain,
! [C_11,A_1,B_10,D_12,A_9] : ( divide(divide(A_1,A_1),divide(multiply(divide(C_11,divide(D_12,B_10)),D_12),multiply(C_11,B_10))) = divide(A_9,A_9) ),
inference(superposition,[status(thm),theory(equality)],[c_17,c_7]) ).
tff(c_212,plain,
! [A_27,A_26] : ( divide(A_27,A_27) = divide(A_26,A_26) ),
inference(superposition,[status(thm),theory(equality)],[c_106,c_23]) ).
tff(c_597,plain,
! [A_42,B_43,A_44,D_45] : ( divide(divide(A_42,A_42),divide(B_43,multiply(divide(A_44,A_44),D_45))) = divide(D_45,B_43) ),
inference(superposition,[status(thm),theory(equality)],[c_212,c_7]) ).
tff(c_765,plain,
! [B_6,B_43,A_44,D_45] : ( divide(multiply(inverse(B_6),B_6),divide(B_43,multiply(divide(A_44,A_44),D_45))) = divide(D_45,B_43) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_597]) ).
tff(c_7365,plain,
! [A_141,A_144,B_142,D_143,C_139,A_140] : ( divide(divide(A_144,A_144),divide(multiply(C_139,B_142),multiply(divide(A_140,A_140),multiply(divide(C_139,divide(D_143,B_142)),D_143)))) = divide(A_141,A_141) ),
inference(superposition,[status(thm),theory(equality)],[c_106,c_7]) ).
tff(c_8183,plain,
! [C_145,D_146,B_147,A_148] : ( divide(multiply(divide(C_145,divide(D_146,B_147)),D_146),multiply(C_145,B_147)) = divide(A_148,A_148) ),
inference(superposition,[status(thm),theory(equality)],[c_7365,c_7]) ).
tff(c_81,plain,
! [A_17,B_18,C_19,A_20] : ( divide(divide(A_17,A_17),divide(inverse(B_18),multiply(divide(C_19,multiply(A_20,B_18)),A_20))) = C_19 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17]) ).
tff(c_103,plain,
! [B_6,B_18,C_19,A_20] : ( divide(multiply(inverse(B_6),B_6),divide(inverse(B_18),multiply(divide(C_19,multiply(A_20,B_18)),A_20))) = C_19 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_81]) ).
tff(c_8417,plain,
! [B_6,B_147,C_145,A_148,D_146] : ( multiply(divide(C_145,divide(D_146,B_147)),D_146) = divide(multiply(inverse(B_6),B_6),divide(inverse(B_147),multiply(divide(A_148,A_148),C_145))) ),
inference(superposition,[status(thm),theory(equality)],[c_8183,c_103]) ).
tff(c_8835,plain,
! [C_145,D_146,B_147] : ( multiply(divide(C_145,divide(D_146,B_147)),D_146) = multiply(C_145,B_147) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_765,c_8417]) ).
tff(c_9136,plain,
! [A_154,B_155,C_156] : ( divide(divide(A_154,A_154),divide(B_155,multiply(C_156,B_155))) = C_156 ),
inference(demodulation,[status(thm),theory(equality)],[c_8835,c_7]) ).
tff(c_273,plain,
! [A_1,A_26,C_3,A_27] : ( divide(divide(A_1,A_1),divide(A_26,multiply(divide(C_3,divide(A_27,A_27)),A_26))) = C_3 ),
inference(superposition,[status(thm),theory(equality)],[c_212,c_7]) ).
tff(c_9153,plain,
! [C_3,A_27] : ( divide(C_3,divide(A_27,A_27)) = C_3 ),
inference(superposition,[status(thm),theory(equality)],[c_9136,c_273]) ).
tff(c_125,plain,
! [A_9,A_25] : ( divide(A_9,A_9) = divide(A_25,A_25) ),
inference(superposition,[status(thm),theory(equality)],[c_106,c_23]) ).
tff(c_42,plain,
! [A_9,B_6,C_11,A_5] : ( divide(divide(A_9,A_9),divide(inverse(B_6),multiply(divide(C_11,multiply(A_5,B_6)),A_5))) = C_11 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17]) ).
tff(c_9659,plain,
! [C_160,B_161] : ( divide(C_160,multiply(inverse(B_161),B_161)) = C_160 ),
inference(superposition,[status(thm),theory(equality)],[c_9136,c_42]) ).
tff(c_8850,plain,
! [A_1,B_2,C_3] : ( divide(divide(A_1,A_1),divide(B_2,multiply(C_3,B_2))) = C_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_8835,c_7]) ).
tff(c_9961,plain,
! [A_163,B_164] : ( divide(divide(A_163,A_163),B_164) = inverse(B_164) ),
inference(superposition,[status(thm),theory(equality)],[c_9659,c_8850]) ).
tff(c_10398,plain,
! [A_165,A_166] : ( inverse(divide(A_165,A_165)) = divide(A_166,A_166) ),
inference(superposition,[status(thm),theory(equality)],[c_125,c_9961]) ).
tff(c_10636,plain,
! [A_5,A_165,A_166] : ( multiply(A_5,divide(A_165,A_165)) = divide(A_5,divide(A_166,A_166)) ),
inference(superposition,[status(thm),theory(equality)],[c_10398,c_4]) ).
tff(c_10760,plain,
! [A_5,A_165] : ( multiply(A_5,divide(A_165,A_165)) = A_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_9153,c_10636]) ).
tff(c_9289,plain,
! [C_157,A_158] : ( divide(C_157,divide(A_158,A_158)) = C_157 ),
inference(superposition,[status(thm),theory(equality)],[c_9136,c_273]) ).
tff(c_8852,plain,
! [C_149,D_150,B_151] : ( multiply(divide(C_149,divide(D_150,B_151)),D_150) = multiply(C_149,B_151) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_765,c_8417]) ).
tff(c_319,plain,
! [B_28,A_29] : ( multiply(inverse(B_28),B_28) = divide(A_29,A_29) ),
inference(superposition,[status(thm),theory(equality)],[c_212,c_4]) ).
tff(c_6,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_374,plain,
! [A_29] : ( multiply(divide(A_29,A_29),a2) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_319,c_6]) ).
tff(c_8912,plain,
! [B_151] : ( multiply(divide(a2,B_151),B_151) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_8852,c_374]) ).
tff(c_9304,plain,
! [A_158] : ( multiply(a2,divide(A_158,A_158)) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_9289,c_8912]) ).
tff(c_10768,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10760,c_9304]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP467-1 : TPTP v9.0.0. Released v2.6.0.
% 0.07/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.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:51:35 EDT 2025
% 0.13/0.34 % CPUTime :
% 9.16/3.21 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.16/3.21
% 9.16/3.21 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------