%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : BOO026-1 : TPTP v9.0.0. Released v2.2.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 : n003.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 05:45:07 PM UTC 2025
% Result : Unsatisfiable 19.10s 8.12s
% Output : CNFRefutation 19.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 10
% Syntax : Number of formulae : 168 ( 168 unt; 0 typ; 0 def)
% Number of atoms : 168 ( 167 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 6 ( 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 189 ( 189 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ multiply > add > #nlpp > inverse > n1 > n0 > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(inverse,type,
inverse: $i > $i ).
tff(multiply,type,
multiply: ( $i * $i ) > $i ).
tff(b,type,
b: $i ).
tff(n1,type,
n1: $i ).
tff(add,type,
add: ( $i * $i ) > $i ).
tff(n0,type,
n0: $i ).
tff(f_33,axiom,
! [X] : ( add(X,inverse(X)) = n1 ),
file(unknown,unknown) ).
tff(f_37,axiom,
! [X] : ( multiply(X,inverse(X)) = n0 ),
file(unknown,unknown) ).
tff(f_35,axiom,
! [X,Y,Z] : ( add(X,multiply(Y,Z)) = multiply(add(Y,X),add(Z,X)) ),
file(unknown,unknown) ).
tff(f_46,axiom,
! [X,Y] : ( multiply(add(X,inverse(X)),multiply(add(X,Y),add(inverse(X),Y))) = Y ),
file(unknown,unknown) ).
tff(f_31,axiom,
! [X,Y,Z] : ( multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) ),
file(unknown,unknown) ).
tff(f_40,axiom,
! [X,Y] : ( add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y ),
file(unknown,unknown) ).
tff(f_50,axiom,
! [X,Y] : ( multiply(add(X,inverse(Y)),multiply(add(X,X),add(inverse(Y),X))) = X ),
file(unknown,unknown) ).
tff(f_42,axiom,
! [X,Y] : ( add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X ),
file(unknown,unknown) ).
tff(f_48,axiom,
! [X,Y] : ( multiply(add(X,inverse(Y)),multiply(add(X,Y),add(inverse(Y),Y))) = X ),
file(unknown,unknown) ).
tff(f_53,axiom,
multiply(add(a,b),b) != b,
file(unknown,unknown) ).
tff(c_4,plain,
! [X_4] : ( add(X_4,inverse(X_4)) = n1 ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_8,plain,
! [X_8] : ( multiply(X_8,inverse(X_8)) = n0 ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_6,plain,
! [Y_6,X_5,Z_7] : ( multiply(add(Y_6,X_5),add(Z_7,X_5)) = add(X_5,multiply(Y_6,Z_7)) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_16,plain,
! [X_15,Y_16] : ( multiply(add(X_15,inverse(X_15)),multiply(add(X_15,Y_16),add(inverse(X_15),Y_16))) = Y_16 ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_26,plain,
! [X_15,Y_16] : ( multiply(add(X_15,inverse(X_15)),add(Y_16,multiply(X_15,inverse(X_15)))) = Y_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_16]) ).
tff(c_27,plain,
! [X_15,Y_16] : ( multiply(add(X_15,inverse(X_15)),add(Y_16,n0)) = Y_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_26]) ).
tff(c_28,plain,
! [Y_16] : ( multiply(n1,add(Y_16,n0)) = Y_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_27]) ).
tff(c_2,plain,
! [Y_2,X_1,Z_3] : ( add(multiply(Y_2,X_1),multiply(Z_3,X_1)) = multiply(X_1,add(Y_2,Z_3)) ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_10,plain,
! [X_9,Y_10] : ( add(multiply(X_9,inverse(X_9)),add(multiply(X_9,Y_10),multiply(inverse(X_9),Y_10))) = Y_10 ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_23,plain,
! [X_9,Y_10] : ( add(n0,add(multiply(X_9,Y_10),multiply(inverse(X_9),Y_10))) = Y_10 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_10]) ).
tff(c_29,plain,
! [Y_10,X_9] : ( add(n0,multiply(Y_10,add(X_9,inverse(X_9)))) = Y_10 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_23]) ).
tff(c_32,plain,
! [Y_10] : ( add(n0,multiply(Y_10,n1)) = Y_10 ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_29]) ).
tff(c_65,plain,
! [Y_25,X_26,Z_27] : ( multiply(add(Y_25,X_26),add(Z_27,X_26)) = add(X_26,multiply(Y_25,Z_27)) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_817,plain,
! [Y_57,Y_58] : ( multiply(add(Y_57,multiply(Y_58,n1)),Y_58) = add(multiply(Y_58,n1),multiply(Y_57,n0)) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_65]) ).
tff(c_905,plain,
! [Y_59] : ( multiply(Y_59,Y_59) = add(multiply(Y_59,n1),multiply(n0,n0)) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_817]) ).
tff(c_964,plain,
! [Y_6,X_5] : ( add(multiply(add(Y_6,X_5),n1),multiply(n0,n0)) = add(X_5,multiply(Y_6,Y_6)) ),
inference(superposition,[status(thm),theory(equality)],[c_905,c_6]) ).
tff(c_109,plain,
! [Y_30,X_31,Z_32] : ( add(multiply(Y_30,X_31),multiply(Z_32,X_31)) = multiply(X_31,add(Y_30,Z_32)) ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_3078,plain,
! [X_90,Y_91,Z_92,Z_93] : ( add(add(X_90,multiply(Y_91,Z_92)),multiply(Z_93,add(Z_92,X_90))) = multiply(add(Z_92,X_90),add(add(Y_91,X_90),Z_93)) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_109]) ).
tff(c_16572,plain,
! [Y_182,Z_183] : ( multiply(add(n1,n0),add(add(Y_182,n0),Z_183)) = add(Y_182,multiply(Z_183,add(n1,n0))) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_3078]) ).
tff(c_16702,plain,
! [Y_182] : ( add(n0,multiply(n1,add(Y_182,n0))) = add(Y_182,multiply(n0,add(n1,n0))) ),
inference(superposition,[status(thm),theory(equality)],[c_16572,c_6]) ).
tff(c_16832,plain,
! [Y_184] : ( add(Y_184,multiply(n0,add(n1,n0))) = add(n0,Y_184) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_16702]) ).
tff(c_16971,plain,
! [Y_2] : ( multiply(add(n1,n0),add(Y_2,n0)) = add(n0,multiply(Y_2,add(n1,n0))) ),
inference(superposition,[status(thm),theory(equality)],[c_16832,c_2]) ).
tff(c_19648,plain,
! [Y_195] : ( add(n0,multiply(Y_195,add(n1,n0))) = add(n0,multiply(n1,Y_195)) ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_16971]) ).
tff(c_16817,plain,
! [Y_182] : ( add(Y_182,multiply(n0,add(n1,n0))) = add(n0,Y_182) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_16702]) ).
tff(c_19662,plain,
add(n0,multiply(n1,n0)) = add(n0,n0),
inference(superposition,[status(thm),theory(equality)],[c_19648,c_16817]) ).
tff(c_19826,plain,
add(multiply(add(n0,n0),n1),multiply(n0,n0)) = add(multiply(n1,n0),multiply(n0,n0)),
inference(superposition,[status(thm),theory(equality)],[c_19662,c_964]) ).
tff(c_19854,plain,
multiply(n0,add(n1,n0)) = add(n0,multiply(n0,n0)),
inference(demodulation,[status(thm),theory(equality)],[c_964,c_2,c_19826]) ).
tff(c_20174,plain,
! [Y_196] : ( add(Y_196,add(n0,multiply(n0,n0))) = add(n0,Y_196) ),
inference(demodulation,[status(thm),theory(equality)],[c_19854,c_16817]) ).
tff(c_239,plain,
! [Y_39,X_40] : ( multiply(add(Y_39,inverse(X_40)),n1) = add(inverse(X_40),multiply(Y_39,X_40)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65]) ).
tff(c_293,plain,
! [X_41] : ( add(inverse(X_41),multiply(X_41,X_41)) = multiply(n1,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_239]) ).
tff(c_1121,plain,
! [Z_62,X_63] : ( add(inverse(add(Z_62,X_63)),add(X_63,multiply(Z_62,Z_62))) = multiply(n1,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_293]) ).
tff(c_1226,plain,
add(inverse(add(n1,n0)),n1) = multiply(n1,n1),
inference(superposition,[status(thm),theory(equality)],[c_32,c_1121]) ).
tff(c_1706,plain,
! [Y_72,Z_73] : ( multiply(add(Y_72,n0),add(n1,Z_73)) = add(Y_72,multiply(Z_73,add(Y_72,n0))) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_109]) ).
tff(c_1786,plain,
! [Y_72] : ( add(Y_72,multiply(n0,add(Y_72,n0))) = add(n0,multiply(Y_72,n1)) ),
inference(superposition,[status(thm),theory(equality)],[c_1706,c_6]) ).
tff(c_1857,plain,
! [Y_74] : ( add(Y_74,multiply(n0,add(Y_74,n0))) = Y_74 ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_1786]) ).
tff(c_130,plain,
! [Y_16,Z_32] : ( multiply(add(Y_16,n0),add(n1,Z_32)) = add(Y_16,multiply(Z_32,add(Y_16,n0))) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_109]) ).
tff(c_1867,plain,
! [Y_74] : ( multiply(add(Y_74,n0),add(n1,n0)) = Y_74 ),
inference(superposition,[status(thm),theory(equality)],[c_1857,c_130]) ).
tff(c_2077,plain,
! [Y_78,Z_79,X_80,Y_81] : ( add(multiply(Y_78,add(Z_79,X_80)),add(X_80,multiply(Y_81,Z_79))) = multiply(add(Z_79,X_80),add(Y_78,add(Y_81,X_80))) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_109]) ).
tff(c_2119,plain,
! [Y_74,Y_81] : ( multiply(add(n1,n0),add(add(Y_74,n0),add(Y_81,n0))) = add(Y_74,add(n0,multiply(Y_81,n1))) ),
inference(superposition,[status(thm),theory(equality)],[c_1867,c_2077]) ).
tff(c_2375,plain,
! [Y_74,Y_81] : ( multiply(add(n1,n0),add(add(Y_74,n0),add(Y_81,n0))) = add(Y_74,Y_81) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_2119]) ).
tff(c_1385,plain,
! [Y_67,Y_68] : ( multiply(add(Y_67,n0),add(Y_68,n1)) = add(multiply(Y_68,add(Y_67,n0)),Y_67) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_109]) ).
tff(c_1492,plain,
! [Y_16] : ( multiply(add(Y_16,n0),add(n1,n1)) = add(Y_16,Y_16) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_1385]) ).
tff(c_1499,plain,
! [Y_69] : ( multiply(add(Y_69,n0),add(n1,n1)) = add(Y_69,Y_69) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_1385]) ).
tff(c_136,plain,
! [X_8,Z_32] : ( multiply(inverse(X_8),add(X_8,Z_32)) = add(n0,multiply(Z_32,inverse(X_8))) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_109]) ).
tff(c_1539,plain,
! [Y_69] : ( multiply(inverse(Y_69),multiply(add(Y_69,n0),add(n1,n1))) = add(n0,multiply(Y_69,inverse(Y_69))) ),
inference(superposition,[status(thm),theory(equality)],[c_1499,c_136]) ).
tff(c_1624,plain,
! [Y_70] : ( multiply(inverse(Y_70),multiply(add(Y_70,n0),add(n1,n1))) = add(n0,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_1539]) ).
tff(c_1657,plain,
! [Y_71] : ( multiply(inverse(Y_71),add(Y_71,Y_71)) = add(n0,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_1492,c_1624]) ).
tff(c_2437,plain,
! [Z_83,X_84] : ( multiply(inverse(multiply(Z_83,X_84)),multiply(X_84,add(Z_83,Z_83))) = add(n0,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_1657]) ).
tff(c_10003,plain,
! [X_151,Y_152] : ( multiply(inverse(multiply(X_151,add(Y_152,X_151))),add(X_151,multiply(Y_152,X_151))) = add(n0,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_2437]) ).
tff(c_10167,plain,
! [Y_74] : ( multiply(inverse(add(Y_74,n1)),add(add(n1,n0),multiply(add(Y_74,n0),add(n1,n0)))) = add(n0,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_2375,c_10003]) ).
tff(c_10505,plain,
! [Y_153] : ( multiply(inverse(add(Y_153,n1)),add(add(n1,n0),Y_153)) = add(n0,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_6,c_10167]) ).
tff(c_10609,plain,
multiply(inverse(multiply(n1,n1)),add(add(n1,n0),inverse(add(n1,n0)))) = add(n0,n0),
inference(superposition,[status(thm),theory(equality)],[c_1226,c_10505]) ).
tff(c_10624,plain,
multiply(inverse(multiply(n1,n1)),n1) = add(n0,n0),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_10609]) ).
tff(c_362,plain,
! [X_44,Z_45] : ( multiply(inverse(X_44),add(X_44,Z_45)) = add(n0,multiply(Z_45,inverse(X_44))) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_109]) ).
tff(c_410,plain,
! [X_4] : ( add(n0,multiply(inverse(X_4),inverse(X_4))) = multiply(inverse(X_4),n1) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_362]) ).
tff(c_415,plain,
! [Z_46,X_47] : ( multiply(n1,add(Z_46,inverse(X_47))) = add(inverse(X_47),multiply(X_47,Z_46)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65]) ).
tff(c_499,plain,
! [X_8] : ( multiply(n1,add(inverse(X_8),inverse(X_8))) = add(inverse(X_8),n0) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_415]) ).
tff(c_1565,plain,
! [Y_2,X_1] : ( multiply(add(multiply(Y_2,X_1),n0),add(n1,n1)) = multiply(X_1,add(Y_2,Y_2)) ),
inference(superposition,[status(thm),theory(equality)],[c_1499,c_2]) ).
tff(c_10650,plain,
multiply(n1,add(inverse(multiply(n1,n1)),inverse(multiply(n1,n1)))) = multiply(add(add(n0,n0),n0),add(n1,n1)),
inference(superposition,[status(thm),theory(equality)],[c_10624,c_1565]) ).
tff(c_10718,plain,
add(inverse(multiply(n1,n1)),n0) = add(add(n0,n0),add(n0,n0)),
inference(demodulation,[status(thm),theory(equality)],[c_1492,c_499,c_10650]) ).
tff(c_11662,plain,
add(multiply(add(add(n0,n0),add(n0,n0)),n1),multiply(n0,n0)) = add(n0,multiply(inverse(multiply(n1,n1)),inverse(multiply(n1,n1)))),
inference(superposition,[status(thm),theory(equality)],[c_10718,c_964]) ).
tff(c_11724,plain,
add(add(n0,n0),add(n0,multiply(n0,n0))) = add(n0,n0),
inference(demodulation,[status(thm),theory(equality)],[c_10624,c_6,c_964,c_410,c_11662]) ).
tff(c_20204,plain,
add(n0,add(n0,n0)) = add(n0,n0),
inference(superposition,[status(thm),theory(equality)],[c_20174,c_11724]) ).
tff(c_10710,plain,
add(n0,add(n0,n0)) = inverse(multiply(n1,n1)),
inference(superposition,[status(thm),theory(equality)],[c_10624,c_32]) ).
tff(c_20351,plain,
inverse(multiply(n1,n1)) = add(n0,n0),
inference(demodulation,[status(thm),theory(equality)],[c_20204,c_10710]) ).
tff(c_319,plain,
! [X_42,Y_43] : ( multiply(inverse(X_42),add(Y_43,X_42)) = add(multiply(Y_43,inverse(X_42)),n0) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_109]) ).
tff(c_3620,plain,
! [Y_95] : ( multiply(inverse(multiply(Y_95,n1)),Y_95) = add(multiply(n0,inverse(multiply(Y_95,n1))),n0) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_319]) ).
tff(c_3741,plain,
! [Y_95] : ( multiply(n1,multiply(inverse(multiply(Y_95,n1)),Y_95)) = multiply(n0,inverse(multiply(Y_95,n1))) ),
inference(superposition,[status(thm),theory(equality)],[c_3620,c_28]) ).
tff(c_10659,plain,
multiply(n0,inverse(multiply(n1,n1))) = multiply(n1,add(n0,n0)),
inference(superposition,[status(thm),theory(equality)],[c_10624,c_3741]) ).
tff(c_10721,plain,
multiply(n0,inverse(multiply(n1,n1))) = n0,
inference(demodulation,[status(thm),theory(equality)],[c_28,c_10659]) ).
tff(c_20,plain,
! [X_19,Y_20] : ( multiply(add(X_19,inverse(Y_20)),multiply(add(X_19,X_19),add(inverse(Y_20),X_19))) = X_19 ),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_24,plain,
! [X_19,Y_20] : ( multiply(add(X_19,inverse(Y_20)),add(X_19,multiply(X_19,inverse(Y_20)))) = X_19 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_20]) ).
tff(c_10794,plain,
multiply(add(n0,inverse(multiply(n1,n1))),add(n0,n0)) = n0,
inference(superposition,[status(thm),theory(equality)],[c_10721,c_24]) ).
tff(c_20990,plain,
multiply(add(n0,add(n0,n0)),add(n0,n0)) = n0,
inference(demodulation,[status(thm),theory(equality)],[c_20351,c_10794]) ).
tff(c_20997,plain,
add(n0,multiply(n0,n0)) = n0,
inference(demodulation,[status(thm),theory(equality)],[c_6,c_20204,c_20990]) ).
tff(c_1849,plain,
! [Y_72] : ( add(Y_72,multiply(n0,add(Y_72,n0))) = Y_72 ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_1786]) ).
tff(c_20092,plain,
add(n1,add(n0,multiply(n0,n0))) = n1,
inference(superposition,[status(thm),theory(equality)],[c_19854,c_1849]) ).
tff(c_21347,plain,
add(n1,n0) = n1,
inference(demodulation,[status(thm),theory(equality)],[c_20997,c_20092]) ).
tff(c_21459,plain,
! [Y_74] : ( multiply(add(Y_74,n0),n1) = Y_74 ),
inference(demodulation,[status(thm),theory(equality)],[c_21347,c_1867]) ).
tff(c_16938,plain,
add(n0,n1) = n1,
inference(superposition,[status(thm),theory(equality)],[c_16832,c_1849]) ).
tff(c_899,plain,
! [Y_10] : ( multiply(Y_10,Y_10) = add(multiply(Y_10,n1),multiply(n0,n0)) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_817]) ).
tff(c_3478,plain,
! [Y_94] : ( multiply(add(n1,inverse(add(Y_94,n0))),n1) = add(inverse(add(Y_94,n0)),Y_94) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_239]) ).
tff(c_5041,plain,
! [Y_106] : ( add(n0,add(inverse(add(Y_106,n0)),Y_106)) = add(n1,inverse(add(Y_106,n0))) ),
inference(superposition,[status(thm),theory(equality)],[c_3478,c_32]) ).
tff(c_5087,plain,
add(n1,inverse(add(n1,n0))) = add(n0,multiply(n1,n1)),
inference(superposition,[status(thm),theory(equality)],[c_1226,c_5041]) ).
tff(c_5097,plain,
add(n1,inverse(add(n1,n0))) = n1,
inference(demodulation,[status(thm),theory(equality)],[c_32,c_5087]) ).
tff(c_12,plain,
! [X_11,Y_12] : ( add(multiply(X_11,inverse(Y_12)),add(multiply(X_11,Y_12),multiply(inverse(Y_12),Y_12))) = X_11 ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_31,plain,
! [X_11,Y_12] : ( add(multiply(X_11,inverse(Y_12)),multiply(Y_12,add(X_11,inverse(Y_12)))) = X_11 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_12]) ).
tff(c_5138,plain,
add(multiply(n1,inverse(add(n1,n0))),multiply(add(n1,n0),n1)) = n1,
inference(superposition,[status(thm),theory(equality)],[c_5097,c_31]) ).
tff(c_77,plain,
! [Y_25,Y_10] : ( multiply(add(Y_25,multiply(Y_10,n1)),Y_10) = add(multiply(Y_10,n1),multiply(Y_25,n0)) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_65]) ).
tff(c_5873,plain,
add(multiply(add(n1,n0),n1),multiply(multiply(n1,inverse(add(n1,n0))),n0)) = multiply(n1,add(n1,n0)),
inference(superposition,[status(thm),theory(equality)],[c_5138,c_77]) ).
tff(c_5891,plain,
add(multiply(add(n1,n0),n1),multiply(multiply(n1,inverse(add(n1,n0))),n0)) = n1,
inference(demodulation,[status(thm),theory(equality)],[c_28,c_5873]) ).
tff(c_21439,plain,
add(multiply(n1,n1),multiply(multiply(n1,inverse(n1)),n0)) = n1,
inference(demodulation,[status(thm),theory(equality)],[c_21347,c_21347,c_5891]) ).
tff(c_21465,plain,
multiply(n1,n1) = n1,
inference(demodulation,[status(thm),theory(equality)],[c_899,c_8,c_21439]) ).
tff(c_21610,plain,
add(n0,n0) = inverse(n1),
inference(demodulation,[status(thm),theory(equality)],[c_21465,c_20351]) ).
tff(c_22055,plain,
! [Y_200] : ( multiply(add(Y_200,n0),n1) = Y_200 ),
inference(demodulation,[status(thm),theory(equality)],[c_21347,c_1867]) ).
tff(c_22133,plain,
multiply(inverse(n1),n1) = n0,
inference(superposition,[status(thm),theory(equality)],[c_21610,c_22055]) ).
tff(c_917,plain,
! [X_4] : ( add(n0,add(multiply(inverse(X_4),n1),multiply(n0,n0))) = multiply(inverse(X_4),n1) ),
inference(superposition,[status(thm),theory(equality)],[c_905,c_410]) ).
tff(c_22200,plain,
add(n0,add(n0,multiply(n0,n0))) = multiply(inverse(n1),n1),
inference(superposition,[status(thm),theory(equality)],[c_22133,c_917]) ).
tff(c_22250,plain,
inverse(n1) = n0,
inference(demodulation,[status(thm),theory(equality)],[c_22133,c_21610,c_20997,c_22200]) ).
tff(c_22260,plain,
add(n0,n0) = n0,
inference(demodulation,[status(thm),theory(equality)],[c_22250,c_21610]) ).
tff(c_22734,plain,
multiply(n1,n0) = n0,
inference(superposition,[status(thm),theory(equality)],[c_22260,c_28]) ).
tff(c_17255,plain,
! [Y_186] : ( multiply(add(Y_186,n1),n1) = add(n1,multiply(Y_186,n0)) ),
inference(superposition,[status(thm),theory(equality)],[c_16938,c_6]) ).
tff(c_17339,plain,
! [Y_186] : ( add(n0,add(n1,multiply(Y_186,n0))) = add(Y_186,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_17255,c_32]) ).
tff(c_22864,plain,
add(n0,add(n1,n0)) = add(n1,n1),
inference(superposition,[status(thm),theory(equality)],[c_22734,c_17339]) ).
tff(c_22891,plain,
add(n1,n1) = n1,
inference(demodulation,[status(thm),theory(equality)],[c_16938,c_21347,c_22864]) ).
tff(c_23045,plain,
! [Y_16] : ( multiply(add(Y_16,n0),n1) = add(Y_16,Y_16) ),
inference(demodulation,[status(thm),theory(equality)],[c_22891,c_1492]) ).
tff(c_23049,plain,
! [Y_16] : ( add(Y_16,Y_16) = Y_16 ),
inference(demodulation,[status(thm),theory(equality)],[c_21459,c_23045]) ).
tff(c_23104,plain,
! [Y_203] : ( add(Y_203,Y_203) = Y_203 ),
inference(demodulation,[status(thm),theory(equality)],[c_21459,c_23045]) ).
tff(c_23303,plain,
! [Y_203] : ( add(n0,multiply(Y_203,inverse(Y_203))) = multiply(inverse(Y_203),Y_203) ),
inference(superposition,[status(thm),theory(equality)],[c_23104,c_136]) ).
tff(c_23385,plain,
! [Y_203] : ( multiply(inverse(Y_203),Y_203) = n0 ),
inference(demodulation,[status(thm),theory(equality)],[c_23049,c_8,c_23303]) ).
tff(c_20037,plain,
! [Y_182] : ( add(Y_182,add(n0,multiply(n0,n0))) = add(n0,Y_182) ),
inference(demodulation,[status(thm),theory(equality)],[c_19854,c_16817]) ).
tff(c_21346,plain,
! [Y_182] : ( add(n0,Y_182) = add(Y_182,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_20997,c_20037]) ).
tff(c_22704,plain,
add(multiply(n0,n1),multiply(n0,n0)) = add(n0,multiply(n0,n0)),
inference(superposition,[status(thm),theory(equality)],[c_22260,c_964]) ).
tff(c_22745,plain,
multiply(n0,n0) = n0,
inference(demodulation,[status(thm),theory(equality)],[c_20997,c_899,c_22704]) ).
tff(c_22259,plain,
multiply(n0,n1) = n0,
inference(demodulation,[status(thm),theory(equality)],[c_22250,c_22133]) ).
tff(c_24358,plain,
! [Y_209] : ( add(n0,Y_209) = add(Y_209,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_20997,c_20037]) ).
tff(c_4021,plain,
! [Y_98,Z_99,X_100,Y_101] : ( multiply(add(Y_98,multiply(Z_99,X_100)),multiply(X_100,add(Y_101,Z_99))) = add(multiply(Z_99,X_100),multiply(Y_98,multiply(Y_101,X_100))) ),
inference(superposition,[status(thm),theory(equality)],[c_109,c_6]) ).
tff(c_4399,plain,
! [Y_10,Y_101] : ( multiply(Y_10,multiply(n1,add(Y_101,Y_10))) = add(multiply(Y_10,n1),multiply(n0,multiply(Y_101,n1))) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_4021]) ).
tff(c_24398,plain,
! [Y_209] : ( multiply(Y_209,multiply(n1,add(Y_209,n0))) = add(multiply(Y_209,n1),multiply(n0,multiply(n0,n1))) ),
inference(superposition,[status(thm),theory(equality)],[c_24358,c_4399]) ).
tff(c_24518,plain,
! [Y_209] : ( multiply(Y_209,Y_209) = Y_209 ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_21346,c_22745,c_22259,c_28,c_24398]) ).
tff(c_24529,plain,
! [Y_210] : ( multiply(Y_210,Y_210) = Y_210 ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_21346,c_22745,c_22259,c_28,c_24398]) ).
tff(c_83,plain,
! [Y_25,X_4] : ( multiply(add(Y_25,inverse(X_4)),n1) = add(inverse(X_4),multiply(Y_25,X_4)) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_65]) ).
tff(c_24715,plain,
! [Y_210] : ( multiply(add(Y_210,inverse(Y_210)),n1) = add(inverse(Y_210),Y_210) ),
inference(superposition,[status(thm),theory(equality)],[c_24529,c_83]) ).
tff(c_25171,plain,
! [Y_212] : ( add(inverse(Y_212),Y_212) = n1 ),
inference(demodulation,[status(thm),theory(equality)],[c_24518,c_4,c_24715]) ).
tff(c_18,plain,
! [X_17,Y_18] : ( multiply(add(X_17,inverse(Y_18)),multiply(add(X_17,Y_18),add(inverse(Y_18),Y_18))) = X_17 ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_25,plain,
! [X_17,Y_18] : ( multiply(add(X_17,inverse(Y_18)),add(Y_18,multiply(X_17,inverse(Y_18)))) = X_17 ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_18]) ).
tff(c_25370,plain,
! [Y_18] : ( multiply(n1,add(Y_18,multiply(inverse(inverse(Y_18)),inverse(Y_18)))) = inverse(inverse(Y_18)) ),
inference(superposition,[status(thm),theory(equality)],[c_25171,c_25]) ).
tff(c_25438,plain,
! [Y_18] : ( inverse(inverse(Y_18)) = Y_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_23385,c_25370]) ).
tff(c_24737,plain,
! [Y_12] : ( add(inverse(Y_12),multiply(Y_12,add(inverse(Y_12),inverse(Y_12)))) = inverse(Y_12) ),
inference(superposition,[status(thm),theory(equality)],[c_24529,c_31]) ).
tff(c_29594,plain,
! [Y_237] : ( add(n0,inverse(Y_237)) = inverse(Y_237) ),
inference(demodulation,[status(thm),theory(equality)],[c_21346,c_8,c_23049,c_24737]) ).
tff(c_29673,plain,
! [Y_18] : ( inverse(inverse(Y_18)) = add(n0,Y_18) ),
inference(superposition,[status(thm),theory(equality)],[c_25438,c_29594]) ).
tff(c_29698,plain,
! [Y_18] : ( add(n0,Y_18) = Y_18 ),
inference(demodulation,[status(thm),theory(equality)],[c_25438,c_29673]) ).
tff(c_24380,plain,
! [Y_209] : ( multiply(add(n0,Y_209),n1) = Y_209 ),
inference(superposition,[status(thm),theory(equality)],[c_24358,c_21459]) ).
tff(c_29705,plain,
! [Y_209] : ( multiply(Y_209,n1) = Y_209 ),
inference(demodulation,[status(thm),theory(equality)],[c_29698,c_24380]) ).
tff(c_24756,plain,
! [X_5,Z_7] : ( add(X_5,multiply(Z_7,Z_7)) = add(Z_7,X_5) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_24529]) ).
tff(c_24803,plain,
! [Z_7,X_5] : ( add(Z_7,X_5) = add(X_5,Z_7) ),
inference(demodulation,[status(thm),theory(equality)],[c_24518,c_24756]) ).
tff(c_29960,plain,
! [Y_95] : ( multiply(n1,multiply(inverse(Y_95),Y_95)) = multiply(n0,inverse(Y_95)) ),
inference(demodulation,[status(thm),theory(equality)],[c_29705,c_29705,c_3741]) ).
tff(c_30716,plain,
! [Y_247] : ( multiply(n0,inverse(Y_247)) = n0 ),
inference(demodulation,[status(thm),theory(equality)],[c_22734,c_23385,c_29960]) ).
tff(c_30770,plain,
! [Y_18] : ( multiply(n0,Y_18) = n0 ),
inference(superposition,[status(thm),theory(equality)],[c_25438,c_30716]) ).
tff(c_22480,plain,
! [X_11] : ( add(multiply(X_11,inverse(n1)),multiply(n1,add(X_11,n0))) = X_11 ),
inference(superposition,[status(thm),theory(equality)],[c_22250,c_31]) ).
tff(c_22559,plain,
! [X_11] : ( add(multiply(X_11,n0),X_11) = X_11 ),
inference(demodulation,[status(thm),theory(equality)],[c_22250,c_28,c_22480]) ).
tff(c_28201,plain,
! [X_230] : ( add(multiply(X_230,n0),X_230) = X_230 ),
inference(demodulation,[status(thm),theory(equality)],[c_22250,c_28,c_22480]) ).
tff(c_28430,plain,
! [Z_3] : ( multiply(n0,add(multiply(Z_3,n0),Z_3)) = multiply(Z_3,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_28201]) ).
tff(c_28470,plain,
! [Z_3] : ( multiply(n0,Z_3) = multiply(Z_3,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_22559,c_28430]) ).
tff(c_31061,plain,
! [Z_3] : ( multiply(Z_3,n0) = n0 ),
inference(demodulation,[status(thm),theory(equality)],[c_30770,c_28470]) ).
tff(c_31251,plain,
! [Y_186] : ( add(n0,add(n1,n0)) = add(Y_186,n1) ),
inference(demodulation,[status(thm),theory(equality)],[c_31061,c_17339]) ).
tff(c_31253,plain,
! [Y_186] : ( add(Y_186,n1) = n1 ),
inference(demodulation,[status(thm),theory(equality)],[c_29698,c_29698,c_24803,c_31251]) ).
tff(c_31440,plain,
! [Y_254,Y_255] : ( multiply(add(Y_254,Y_255),Y_255) = add(Y_255,multiply(Y_254,Y_255)) ),
inference(superposition,[status(thm),theory(equality)],[c_23104,c_6]) ).
tff(c_31457,plain,
! [Y_254] : ( add(n1,multiply(Y_254,n1)) = add(Y_254,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_31440,c_29705]) ).
tff(c_31593,plain,
! [Y_254] : ( add(n1,Y_254) = n1 ),
inference(demodulation,[status(thm),theory(equality)],[c_31253,c_29705,c_31457]) ).
tff(c_24495,plain,
! [Y_209] : ( multiply(n1,add(n0,Y_209)) = Y_209 ),
inference(superposition,[status(thm),theory(equality)],[c_24358,c_28]) ).
tff(c_30059,plain,
! [Y_240] : ( multiply(n1,Y_240) = Y_240 ),
inference(demodulation,[status(thm),theory(equality)],[c_29698,c_24495]) ).
tff(c_30172,plain,
! [Y_240,Z_3] : ( multiply(Y_240,add(n1,Z_3)) = add(Y_240,multiply(Z_3,Y_240)) ),
inference(superposition,[status(thm),theory(equality)],[c_30059,c_2]) ).
tff(c_32546,plain,
! [Y_240,Z_3] : ( add(Y_240,multiply(Z_3,Y_240)) = Y_240 ),
inference(demodulation,[status(thm),theory(equality)],[c_29705,c_31593,c_30172]) ).
tff(c_23336,plain,
! [Y_6,Y_203] : ( multiply(add(Y_6,Y_203),Y_203) = add(Y_203,multiply(Y_6,Y_203)) ),
inference(superposition,[status(thm),theory(equality)],[c_23104,c_6]) ).
tff(c_22,plain,
multiply(add(a,b),b) != b,
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_31439,plain,
add(b,multiply(a,b)) != b,
inference(demodulation,[status(thm),theory(equality)],[c_23336,c_22]) ).
tff(c_32551,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_32546,c_31439]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : BOO026-1 : TPTP v9.0.0. Released v2.2.0.
% 0.00/0.09 % 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.08/0.28 % Computer : n003.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Mon Apr 7 15:24:48 EDT 2025
% 0.08/0.28 % CPUTime :
% 19.10/8.12 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.33/8.13
% 19.33/8.13 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------