%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP070-1 : TPTP v9.0.0. Bugfixed v2.3.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:24:55 PM UTC 2025
% Result : Unsatisfiable 20.15s 8.99s
% Output : CNFRefutation 20.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 3
% Syntax : Number of formulae : 72 ( 69 unt; 0 typ; 0 def)
% Number of atoms : 77 ( 74 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 21 ( 16 ~; 5 |; 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 : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 184 ( 184 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > divide > #nlpp > inverse > c3 > b3 > b2 > b1 > a3 > a2 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a1,type,
a1: $i ).
tff(a3,type,
a3: $i ).
tff(c3,type,
c3: $i ).
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(b1,type,
b1: $i ).
tff(b3,type,
b3: $i ).
tff(a2,type,
a2: $i ).
tff(f_28,axiom,
! [X,Y] : ( multiply(X,Y) = divide(X,inverse(Y)) ),
file(unknown,unknown) ).
tff(f_25,axiom,
! [X,Y,Z,U] : ( divide(divide(X,X),divide(Y,divide(divide(Z,divide(U,Y)),inverse(U)))) = Z ),
file(unknown,unknown) ).
tff(f_36,axiom,
( ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_5,Y_6] : ( divide(X_5,inverse(Y_6)) = multiply(X_5,Y_6) ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3,U_4] : ( divide(divide(X_1,X_1),divide(Y_2,divide(divide(Z_3,divide(U_4,Y_2)),inverse(U_4)))) = Z_3 ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_7,plain,
! [X_1,Y_2,Z_3,U_4] : ( divide(divide(X_1,X_1),divide(Y_2,multiply(divide(Z_3,divide(U_4,Y_2)),U_4))) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2]) ).
tff(c_17,plain,
! [X_9,Y_10,Z_11,U_12] : ( divide(divide(X_9,X_9),divide(Y_10,multiply(divide(Z_11,divide(U_12,Y_10)),U_12))) = Z_11 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2]) ).
tff(c_46789,plain,
! [X_397,Z_398,X_400,U_399,Y_401] : ( divide(divide(X_397,X_397),divide(multiply(divide(Z_398,divide(U_399,Y_401)),U_399),multiply(Z_398,Y_401))) = divide(X_400,X_400) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_32,plain,
! [U_4,Z_3,X_1,X_9,Y_2] : ( divide(divide(X_9,X_9),divide(multiply(divide(Z_3,divide(U_4,Y_2)),U_4),multiply(Z_3,Y_2))) = divide(X_1,X_1) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_46919,plain,
! [X_403,X_402] : ( divide(X_403,X_403) = divide(X_402,X_402) ),
inference(superposition,[status(thm),theory(equality)],[c_46789,c_32]) ).
tff(c_47004,plain,
! [X_1,Y_2,X_403,U_4] : ( divide(divide(X_1,X_1),divide(Y_2,multiply(divide(X_403,X_403),U_4))) = divide(U_4,Y_2) ),
inference(superposition,[status(thm),theory(equality)],[c_46919,c_7]) ).
tff(c_47488,plain,
! [X_420,Y_421,X_422,U_423] : ( divide(divide(X_420,X_420),divide(Y_421,multiply(divide(X_422,X_422),U_423))) = divide(U_423,Y_421) ),
inference(superposition,[status(thm),theory(equality)],[c_46919,c_7]) ).
tff(c_53113,plain,
! [Y_503,X_504,U_505,X_506] : ( divide(Y_503,multiply(divide(divide(X_504,X_504),divide(U_505,Y_503)),U_505)) = divide(X_506,X_506) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_47488]) ).
tff(c_55469,plain,
! [Z_522,U_523,Y_524,X_525] : ( divide(multiply(divide(Z_522,divide(U_523,Y_524)),U_523),multiply(Z_522,Y_524)) = divide(X_525,X_525) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_53113]) ).
tff(c_42,plain,
! [X_9,Y_6,Z_11,X_5] : ( divide(divide(X_9,X_9),divide(inverse(Y_6),multiply(divide(Z_11,multiply(X_5,Y_6)),X_5))) = Z_11 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_17]) ).
tff(c_55742,plain,
! [Y_524,Z_522,U_523,X_525,X_9] : ( multiply(divide(Z_522,divide(U_523,Y_524)),U_523) = divide(divide(X_9,X_9),divide(inverse(Y_524),multiply(divide(X_525,X_525),Z_522))) ),
inference(superposition,[status(thm),theory(equality)],[c_55469,c_42]) ).
tff(c_56161,plain,
! [Z_522,U_523,Y_524] : ( multiply(divide(Z_522,divide(U_523,Y_524)),U_523) = multiply(Z_522,Y_524) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_47004,c_55742]) ).
tff(c_56502,plain,
! [X_531,Y_532,Z_533] : ( divide(divide(X_531,X_531),divide(Y_532,multiply(Z_533,Y_532))) = Z_533 ),
inference(demodulation,[status(thm),theory(equality)],[c_56161,c_7]) ).
tff(c_47009,plain,
! [X_1,X_403,Z_3,X_402] : ( divide(divide(X_1,X_1),divide(X_403,multiply(divide(Z_3,divide(X_402,X_402)),X_403))) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_46919,c_7]) ).
tff(c_56527,plain,
! [Z_3,X_402] : ( divide(Z_3,divide(X_402,X_402)) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_56502,c_47009]) ).
tff(c_56677,plain,
! [Z_534,X_535] : ( divide(Z_534,divide(X_535,X_535)) = Z_534 ),
inference(superposition,[status(thm),theory(equality)],[c_56502,c_47009]) ).
tff(c_57011,plain,
! [Z_536,Y_537] : ( divide(Z_536,multiply(inverse(Y_537),Y_537)) = Z_536 ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_56677]) ).
tff(c_56180,plain,
! [X_1,Y_2,Z_3] : ( divide(divide(X_1,X_1),divide(Y_2,multiply(Z_3,Y_2))) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_56161,c_7]) ).
tff(c_57394,plain,
! [X_540,Y_541] : ( divide(divide(X_540,X_540),Y_541) = inverse(Y_541) ),
inference(superposition,[status(thm),theory(equality)],[c_57011,c_56180]) ).
tff(c_58449,plain,
! [X_551,X_552] : ( inverse(divide(X_551,X_551)) = divide(X_552,X_552) ),
inference(superposition,[status(thm),theory(equality)],[c_57394,c_56527]) ).
tff(c_58666,plain,
! [X_5,X_551,X_552] : ( multiply(X_5,divide(X_551,X_551)) = divide(X_5,divide(X_552,X_552)) ),
inference(superposition,[status(thm),theory(equality)],[c_58449,c_4]) ).
tff(c_58789,plain,
! [X_5,X_551] : ( multiply(X_5,divide(X_551,X_551)) = X_5 ),
inference(demodulation,[status(thm),theory(equality)],[c_56527,c_58666]) ).
tff(c_56181,plain,
! [Z_526,U_527,Y_528] : ( multiply(divide(Z_526,divide(U_527,Y_528)),U_527) = multiply(Z_526,Y_528) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_47004,c_55742]) ).
tff(c_47048,plain,
! [Y_404,X_405] : ( multiply(inverse(Y_404),Y_404) = divide(X_405,X_405) ),
inference(superposition,[status(thm),theory(equality)],[c_46919,c_4]) ).
tff(c_724,plain,
! [U_46,X_47,X_44,Z_45,Y_48] : ( divide(divide(X_44,X_44),divide(multiply(divide(Z_45,divide(U_46,Y_48)),U_46),multiply(Z_45,Y_48))) = divide(X_47,X_47) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_851,plain,
! [X_50,X_49] : ( divide(X_50,X_50) = divide(X_49,X_49) ),
inference(superposition,[status(thm),theory(equality)],[c_724,c_32]) ).
tff(c_936,plain,
! [X_1,Y_2,X_50,U_4] : ( divide(divide(X_1,X_1),divide(Y_2,multiply(divide(X_50,X_50),U_4))) = divide(U_4,Y_2) ),
inference(superposition,[status(thm),theory(equality)],[c_851,c_7]) ).
tff(c_11512,plain,
! [Z_174,Y_171,X_173,U_170,X_169,X_172] : ( divide(divide(X_172,X_172),divide(multiply(Z_174,Y_171),multiply(divide(X_169,X_169),multiply(divide(Z_174,divide(U_170,Y_171)),U_170)))) = divide(X_173,X_173) ),
inference(superposition,[status(thm),theory(equality)],[c_724,c_7]) ).
tff(c_12500,plain,
! [Z_175,U_176,Y_177,X_178] : ( divide(multiply(divide(Z_175,divide(U_176,Y_177)),U_176),multiply(Z_175,Y_177)) = divide(X_178,X_178) ),
inference(superposition,[status(thm),theory(equality)],[c_11512,c_7]) ).
tff(c_12805,plain,
! [X_178,Z_175,Y_177,U_176,X_9] : ( multiply(divide(Z_175,divide(U_176,Y_177)),U_176) = divide(divide(X_9,X_9),divide(inverse(Y_177),multiply(divide(X_178,X_178),Z_175))) ),
inference(superposition,[status(thm),theory(equality)],[c_12500,c_42]) ).
tff(c_13279,plain,
! [Z_175,U_176,Y_177] : ( multiply(divide(Z_175,divide(U_176,Y_177)),U_176) = multiply(Z_175,Y_177) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_936,c_12805]) ).
tff(c_13601,plain,
! [X_182,Y_183,Z_184] : ( divide(divide(X_182,X_182),divide(Y_183,multiply(Z_184,Y_183))) = Z_184 ),
inference(demodulation,[status(thm),theory(equality)],[c_13279,c_7]) ).
tff(c_14309,plain,
! [Z_190,Y_191] : ( divide(Z_190,multiply(inverse(Y_191),Y_191)) = Z_190 ),
inference(superposition,[status(thm),theory(equality)],[c_13601,c_42]) ).
tff(c_13298,plain,
! [X_1,Y_2,Z_3] : ( divide(divide(X_1,X_1),divide(Y_2,multiply(Z_3,Y_2))) = Z_3 ),
inference(demodulation,[status(thm),theory(equality)],[c_13279,c_7]) ).
tff(c_14572,plain,
! [X_192,Y_193] : ( divide(divide(X_192,X_192),Y_193) = inverse(Y_193) ),
inference(superposition,[status(thm),theory(equality)],[c_14309,c_13298]) ).
tff(c_16843,plain,
! [Y_213,Z_214] : ( inverse(divide(Y_213,multiply(Z_214,Y_213))) = Z_214 ),
inference(superposition,[status(thm),theory(equality)],[c_14572,c_13298]) ).
tff(c_14834,plain,
! [X_192,Y_6] : ( multiply(divide(X_192,X_192),Y_6) = inverse(inverse(Y_6)) ),
inference(superposition,[status(thm),theory(equality)],[c_14572,c_4]) ).
tff(c_14327,plain,
! [X_1,Y_191] : ( divide(divide(X_1,X_1),Y_191) = inverse(Y_191) ),
inference(superposition,[status(thm),theory(equality)],[c_14309,c_13298]) ).
tff(c_941,plain,
! [X_1,X_50,Z_3,X_49] : ( divide(divide(X_1,X_1),divide(X_50,multiply(divide(Z_3,divide(X_49,X_49)),X_50))) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_851,c_7]) ).
tff(c_13626,plain,
! [Z_3,X_49] : ( divide(Z_3,divide(X_49,X_49)) = Z_3 ),
inference(superposition,[status(thm),theory(equality)],[c_13601,c_941]) ).
tff(c_743,plain,
! [X_47,X_1] : ( divide(X_47,X_47) = divide(X_1,X_1) ),
inference(superposition,[status(thm),theory(equality)],[c_724,c_32]) ).
tff(c_15144,plain,
! [X_196,X_197] : ( inverse(divide(X_196,X_196)) = divide(X_197,X_197) ),
inference(superposition,[status(thm),theory(equality)],[c_743,c_14572]) ).
tff(c_15316,plain,
! [X_5,X_196,X_197] : ( multiply(X_5,divide(X_196,X_196)) = divide(X_5,divide(X_197,X_197)) ),
inference(superposition,[status(thm),theory(equality)],[c_15144,c_4]) ).
tff(c_15742,plain,
! [X_202,X_203] : ( multiply(X_202,divide(X_203,X_203)) = X_202 ),
inference(demodulation,[status(thm),theory(equality)],[c_13626,c_15316]) ).
tff(c_15773,plain,
! [X_1,X_203,X_202] : ( divide(divide(X_1,X_1),divide(divide(X_203,X_203),X_202)) = X_202 ),
inference(superposition,[status(thm),theory(equality)],[c_15742,c_13298]) ).
tff(c_15975,plain,
! [X_202] : ( inverse(inverse(X_202)) = X_202 ),
inference(demodulation,[status(thm),theory(equality)],[c_14834,c_4,c_14327,c_15773]) ).
tff(c_18651,plain,
! [Y_232,Z_233] : ( divide(Y_232,multiply(Z_233,Y_232)) = inverse(Z_233) ),
inference(superposition,[status(thm),theory(equality)],[c_16843,c_15975]) ).
tff(c_18678,plain,
! [Z_175,Z_233,Y_232] : ( multiply(divide(Z_175,inverse(Z_233)),Y_232) = multiply(Z_175,multiply(Z_233,Y_232)) ),
inference(superposition,[status(thm),theory(equality)],[c_18651,c_13279]) ).
tff(c_18775,plain,
! [Z_175,Z_233,Y_232] : ( multiply(multiply(Z_175,Z_233),Y_232) = multiply(Z_175,multiply(Z_233,Y_232)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_18678]) ).
tff(c_129,plain,
! [X_25,Z_26,X_28,Y_29,U_27] : ( divide(divide(X_25,X_25),divide(multiply(divide(Z_26,divide(U_27,Y_29)),U_27),multiply(Z_26,Y_29))) = divide(X_28,X_28) ),
inference(superposition,[status(thm),theory(equality)],[c_7,c_17]) ).
tff(c_245,plain,
! [Y_31,Z_32,Y_34,X_30,U_33] : ( multiply(inverse(Y_31),Y_31) = divide(divide(X_30,X_30),divide(multiply(divide(Z_32,divide(U_33,Y_34)),U_33),multiply(Z_32,Y_34))) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_4]) ).
tff(c_266,plain,
! [Y_31,X_1] : ( multiply(inverse(Y_31),Y_31) = divide(X_1,X_1) ),
inference(superposition,[status(thm),theory(equality)],[c_245,c_32]) ).
tff(c_486,plain,
! [Y_37,X_38] : ( multiply(inverse(Y_37),Y_37) = divide(X_38,X_38) ),
inference(superposition,[status(thm),theory(equality)],[c_245,c_32]) ).
tff(c_6,plain,
( ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) )
| ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(inverse(b1),b1) != multiply(inverse(a1),a1) ) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_127,plain,
multiply(inverse(b1),b1) != multiply(inverse(a1),a1),
inference(splitLeft,[status(thm)],[c_6]) ).
tff(c_658,plain,
! [X_41] : ( multiply(inverse(a1),a1) != divide(X_41,X_41) ),
inference(superposition,[status(thm),theory(equality)],[c_486,c_127]) ).
tff(c_666,plain,
! [X_41,X_1] : ( divide(X_41,X_41) != divide(X_1,X_1) ),
inference(superposition,[status(thm),theory(equality)],[c_266,c_658]) ).
tff(c_148,plain,
! [X_28,X_1] : ( divide(X_28,X_28) = divide(X_1,X_1) ),
inference(superposition,[status(thm),theory(equality)],[c_129,c_32]) ).
tff(c_678,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_666,c_148]) ).
tff(c_679,plain,
( ( multiply(multiply(inverse(b2),b2),a2) != a2 )
| ( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_698,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(splitLeft,[status(thm)],[c_679]) ).
tff(c_46751,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18775,c_698]) ).
tff(c_46752,plain,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(splitRight,[status(thm)],[c_679]) ).
tff(c_47080,plain,
! [X_405] : ( multiply(divide(X_405,X_405),a2) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_47048,c_46752]) ).
tff(c_56242,plain,
! [Y_528] : ( multiply(divide(a2,Y_528),Y_528) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_56181,c_47080]) ).
tff(c_56692,plain,
! [X_535] : ( multiply(a2,divide(X_535,X_535)) != a2 ),
inference(superposition,[status(thm),theory(equality)],[c_56677,c_56242]) ).
tff(c_58798,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_58789,c_56692]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP070-1 : TPTP v9.0.0. Bugfixed v2.3.0.
% 0.10/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:15:20 EDT 2025
% 0.13/0.34 % CPUTime :
% 20.15/8.99 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.28/9.00
% 20.28/9.00 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------