%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : REL010+2 : TPTP v9.0.0. Released v4.0.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 : n017.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 08:29:05 PM UTC 2025
% Result : Theorem 17.11s 6.45s
% Output : CNFRefutation 17.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 15
% Syntax : Number of formulae : 115 ( 114 unt; 0 typ; 0 def)
% Number of atoms : 116 ( 115 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 3 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 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 : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 141 ( 141 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ meet > join > composition > #nlpp > converse > complement > zero > top > one > #skF_2 > #skF_3 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(top,type,
top: $i ).
tff(converse,type,
converse: $i > $i ).
tff(join,type,
join: ( $i * $i ) > $i ).
tff(composition,type,
composition: ( $i * $i ) > $i ).
tff(complement,type,
complement: $i > $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(one,type,
one: $i ).
tff(meet,type,
meet: ( $i * $i ) > $i ).
tff(zero,type,
zero: $i ).
tff(f_121,negated_conjecture,
~ ! [X0,X1,X2] :
( ( meet(composition(X0,X1),X2) = zero )
=> ( meet(X1,composition(converse(X0),X2)) = zero ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
tff(f_81,axiom,
! [X0] : ( zero = meet(X0,complement(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_zero) ).
tff(f_79,axiom,
! [X0] : ( top = join(X0,complement(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',def_top) ).
tff(f_60,axiom,
! [X0,X1] : ( meet(X0,X1) = complement(join(complement(X0),complement(X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux4_definiton_of_meet) ).
tff(f_54,axiom,
! [X0,X1] : ( join(X0,X1) = join(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux1_join_commutativity) ).
tff(f_58,axiom,
! [X0,X1] : ( X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux3_a_kind_of_de_Morgan) ).
tff(f_56,axiom,
! [X0,X1,X2] : ( join(X0,join(X1,X2)) = join(join(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',maddux2_join_associativity) ).
tff(f_70,axiom,
! [X0] : ( converse(converse(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
tff(f_65,axiom,
! [X0] : ( composition(X0,one) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',composition_identity) ).
tff(f_74,axiom,
! [X0,X1] : ( converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_multiplicativity) ).
tff(f_76,axiom,
! [X0,X1] : ( join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
tff(f_72,axiom,
! [X0,X1] : ( converse(join(X0,X1)) = join(converse(X0),converse(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
tff(f_67,axiom,
! [X0,X1,X2] : ( composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
tff(f_63,axiom,
! [X0,X1,X2] : ( composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
tff(f_109,axiom,
! [X0,X1,X2] : ( join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/REL001+1.ax',dedekind_law) ).
tff(c_34,plain,
meet('#skF_2',composition(converse('#skF_1'),'#skF_3')) != zero,
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_26,plain,
! [X0_25] : ( meet(X0_25,complement(X0_25)) = zero ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_24,plain,
! [X0_24] : ( join(X0_24,complement(X0_24)) = top ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_115,plain,
! [X0_41,X1_42] : ( complement(join(complement(X0_41),complement(X1_42))) = meet(X0_41,X1_42) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_149,plain,
! [X0_41] : ( meet(X0_41,complement(X0_41)) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_115]) ).
tff(c_152,plain,
complement(top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_149]) ).
tff(c_2,plain,
! [X1_2,X0_1] : ( join(X1_2,X0_1) = join(X0_1,X1_2) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_646,plain,
! [X1_62,X0_63] : ( complement(join(complement(X1_62),complement(X0_63))) = meet(X0_63,X1_62) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_115]) ).
tff(c_8,plain,
! [X0_8,X1_9] : ( complement(join(complement(X0_8),complement(X1_9))) = meet(X0_8,X1_9) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_673,plain,
! [X1_62,X0_63] : ( meet(X1_62,X0_63) = meet(X0_63,X1_62) ),
inference(superposition,[status(thm),theory(equality)],[c_646,c_8]) ).
tff(c_6,plain,
! [X0_6,X1_7] : ( join(complement(join(complement(X0_6),complement(X1_7))),complement(join(complement(X0_6),X1_7))) = X0_6 ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_855,plain,
! [X0_67,X1_68] : ( join(meet(X0_67,X1_68),complement(join(complement(X0_67),X1_68))) = X0_67 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_921,plain,
! [X0_67] : ( join(meet(X0_67,complement(complement(X0_67))),complement(top)) = X0_67 ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_855]) ).
tff(c_932,plain,
! [X0_67] : ( join(zero,meet(X0_67,complement(complement(X0_67)))) = X0_67 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_152,c_921]) ).
tff(c_162,plain,
join(top,zero) = top,
inference(superposition,[status(thm),theory(equality)],[c_152,c_24]) ).
tff(c_360,plain,
! [X0_50,X1_51,X2_52] : ( join(join(X0_50,X1_51),X2_52) = join(X0_50,join(X1_51,X2_52)) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_414,plain,
! [X2_53] : ( join(top,join(zero,X2_53)) = join(top,X2_53) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_360]) ).
tff(c_435,plain,
join(top,complement(zero)) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_414]) ).
tff(c_159,plain,
! [X0_8] : ( complement(join(complement(X0_8),zero)) = meet(X0_8,top) ),
inference(superposition,[status(thm),theory(equality)],[c_152,c_8]) ).
tff(c_193,plain,
! [X0_45] : ( complement(join(zero,complement(X0_45))) = meet(X0_45,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_159]) ).
tff(c_227,plain,
meet(zero,top) = complement(top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_193]) ).
tff(c_230,plain,
meet(zero,top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_152,c_227]) ).
tff(c_891,plain,
join(zero,complement(join(complement(zero),top))) = zero,
inference(superposition,[status(thm),theory(equality)],[c_230,c_855]) ).
tff(c_929,plain,
join(zero,complement(join(top,top))) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_435,c_2,c_891]) ).
tff(c_388,plain,
! [X2_52] : ( join(top,join(zero,X2_52)) = join(top,X2_52) ),
inference(superposition,[status(thm),theory(equality)],[c_162,c_360]) ).
tff(c_990,plain,
join(top,complement(join(top,top))) = join(top,zero),
inference(superposition,[status(thm),theory(equality)],[c_929,c_388]) ).
tff(c_1002,plain,
join(top,complement(join(top,top))) = top,
inference(demodulation,[status(thm),theory(equality)],[c_162,c_990]) ).
tff(c_168,plain,
! [X0_8] : ( complement(join(zero,complement(X0_8))) = meet(X0_8,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_159]) ).
tff(c_999,plain,
meet(join(top,top),top) = complement(zero),
inference(superposition,[status(thm),theory(equality)],[c_929,c_168]) ).
tff(c_37,plain,
! [X0_6,X1_7] : ( join(meet(X0_6,X1_7),complement(join(complement(X0_6),X1_7))) = X0_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_1074,plain,
join(complement(zero),complement(join(complement(join(top,top)),top))) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_999,c_37]) ).
tff(c_1089,plain,
join(top,top) = top,
inference(demodulation,[status(thm),theory(equality)],[c_24,c_152,c_2,c_1002,c_2,c_1074]) ).
tff(c_1098,plain,
join(zero,complement(top)) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_1089,c_929]) ).
tff(c_1101,plain,
join(zero,zero) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_152,c_1098]) ).
tff(c_4,plain,
! [X0_3,X1_4,X2_5] : ( join(join(X0_3,X1_4),X2_5) = join(X0_3,join(X1_4,X2_5)) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_1384,plain,
! [X2_79] : ( join(zero,join(zero,X2_79)) = join(zero,X2_79) ),
inference(superposition,[status(thm),theory(equality)],[c_1101,c_4]) ).
tff(c_1414,plain,
! [X0_67] : ( join(zero,meet(X0_67,complement(complement(X0_67)))) = join(zero,X0_67) ),
inference(superposition,[status(thm),theory(equality)],[c_932,c_1384]) ).
tff(c_1448,plain,
! [X0_67] : ( join(zero,X0_67) = X0_67 ),
inference(demodulation,[status(thm),theory(equality)],[c_932,c_1414]) ).
tff(c_156,plain,
! [X1_9] : ( complement(join(zero,complement(X1_9))) = meet(top,X1_9) ),
inference(superposition,[status(thm),theory(equality)],[c_152,c_8]) ).
tff(c_1539,plain,
! [X1_9] : ( complement(complement(X1_9)) = meet(top,X1_9) ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_156]) ).
tff(c_1541,plain,
! [X0_83] : ( join(zero,X0_83) = X0_83 ),
inference(demodulation,[status(thm),theory(equality)],[c_932,c_1414]) ).
tff(c_1550,plain,
! [X0_67] : ( meet(X0_67,complement(complement(X0_67))) = X0_67 ),
inference(superposition,[status(thm),theory(equality)],[c_1541,c_932]) ).
tff(c_2331,plain,
! [X0_96] : ( meet(X0_96,meet(top,X0_96)) = X0_96 ),
inference(demodulation,[status(thm),theory(equality)],[c_1539,c_1550]) ).
tff(c_2368,plain,
! [X1_62] : ( meet(X1_62,meet(X1_62,top)) = X1_62 ),
inference(superposition,[status(thm),theory(equality)],[c_673,c_2331]) ).
tff(c_2163,plain,
! [X0_93] : ( complement(complement(X0_93)) = meet(X0_93,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_168]) ).
tff(c_731,plain,
! [X1_62] : ( meet(complement(X1_62),X1_62) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_646]) ).
tff(c_739,plain,
! [X1_62] : ( meet(complement(X1_62),X1_62) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_152,c_731]) ).
tff(c_2567,plain,
! [X0_99] : ( meet(meet(X0_99,top),complement(X0_99)) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_2163,c_739]) ).
tff(c_2572,plain,
! [X0_99] : ( join(zero,complement(join(complement(meet(X0_99,top)),complement(X0_99)))) = meet(X0_99,top) ),
inference(superposition,[status(thm),theory(equality)],[c_2567,c_37]) ).
tff(c_2628,plain,
! [X0_99] : ( meet(X0_99,top) = X0_99 ),
inference(demodulation,[status(thm),theory(equality)],[c_2368,c_1448,c_8,c_2,c_2572]) ).
tff(c_1540,plain,
! [X0_8] : ( complement(complement(X0_8)) = meet(X0_8,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_168]) ).
tff(c_2642,plain,
! [X0_8] : ( complement(complement(X0_8)) = X0_8 ),
inference(demodulation,[status(thm),theory(equality)],[c_2628,c_1540]) ).
tff(c_16,plain,
! [X0_17] : ( converse(converse(X0_17)) = X0_17 ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_12,plain,
! [X0_13] : ( composition(X0_13,one) = X0_13 ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_170,plain,
! [X1_43,X0_44] : ( composition(converse(X1_43),converse(X0_44)) = converse(composition(X0_44,X1_43)) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_2715,plain,
! [X0_101,X1_102] : ( converse(composition(converse(X0_101),X1_102)) = composition(converse(X1_102),X0_101) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_170]) ).
tff(c_2783,plain,
! [X0_101] : ( composition(converse(one),X0_101) = converse(converse(X0_101)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_2715]) ).
tff(c_2971,plain,
! [X0_105] : ( composition(converse(one),X0_105) = X0_105 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2783]) ).
tff(c_3032,plain,
converse(one) = one,
inference(superposition,[status(thm),theory(equality)],[c_2971,c_12]) ).
tff(c_2800,plain,
! [X0_101] : ( composition(converse(one),X0_101) = X0_101 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_2783]) ).
tff(c_3064,plain,
! [X0_101] : ( composition(one,X0_101) = X0_101 ),
inference(demodulation,[status(thm),theory(equality)],[c_3032,c_2800]) ).
tff(c_3119,plain,
! [X0_106] : ( composition(one,X0_106) = X0_106 ),
inference(demodulation,[status(thm),theory(equality)],[c_3032,c_2800]) ).
tff(c_22,plain,
! [X0_22,X1_23] : ( join(composition(converse(X0_22),complement(composition(X0_22,X1_23))),complement(X1_23)) = complement(X1_23) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_3152,plain,
! [X0_106] : ( join(composition(converse(one),complement(X0_106)),complement(X0_106)) = complement(X0_106) ),
inference(superposition,[status(thm),theory(equality)],[c_3119,c_22]) ).
tff(c_3379,plain,
! [X0_110] : ( join(complement(X0_110),complement(X0_110)) = complement(X0_110) ),
inference(demodulation,[status(thm),theory(equality)],[c_3064,c_2,c_3032,c_3152]) ).
tff(c_3400,plain,
! [X0_8] : ( join(X0_8,complement(complement(X0_8))) = complement(complement(X0_8)) ),
inference(superposition,[status(thm),theory(equality)],[c_2642,c_3379]) ).
tff(c_3439,plain,
! [X0_8] : ( join(X0_8,X0_8) = X0_8 ),
inference(demodulation,[status(thm),theory(equality)],[c_2642,c_2642,c_3400]) ).
tff(c_3727,plain,
! [X0_114,X1_115] : ( join(X0_114,join(X1_115,complement(join(X0_114,X1_115)))) = top ),
inference(superposition,[status(thm),theory(equality)],[c_360,c_24]) ).
tff(c_3765,plain,
! [X0_8] : ( join(X0_8,join(X0_8,complement(X0_8))) = top ),
inference(superposition,[status(thm),theory(equality)],[c_3439,c_3727]) ).
tff(c_3868,plain,
! [X0_116] : ( join(X0_116,top) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_3765]) ).
tff(c_254,plain,
! [X0_46,X1_47] : ( join(converse(X0_46),converse(X1_47)) = converse(join(X0_46,X1_47)) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_275,plain,
! [X0_17,X1_47] : ( converse(join(converse(X0_17),X1_47)) = join(X0_17,converse(X1_47)) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_254]) ).
tff(c_4032,plain,
! [X0_118] : ( join(X0_118,converse(top)) = converse(top) ),
inference(superposition,[status(thm),theory(equality)],[c_3868,c_275]) ).
tff(c_3902,plain,
! [X0_116] : ( join(top,X0_116) = top ),
inference(superposition,[status(thm),theory(equality)],[c_3868,c_2]) ).
tff(c_4037,plain,
converse(top) = top,
inference(superposition,[status(thm),theory(equality)],[c_4032,c_3902]) ).
tff(c_179,plain,
! [X0_44,X0_17] : ( converse(composition(X0_44,converse(X0_17))) = composition(X0_17,converse(X0_44)) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_170]) ).
tff(c_28511,plain,
! [X0_279] : ( composition(top,converse(X0_279)) = converse(composition(X0_279,top)) ),
inference(superposition,[status(thm),theory(equality)],[c_4037,c_179]) ).
tff(c_28580,plain,
converse(composition(top,top)) = composition(top,top),
inference(superposition,[status(thm),theory(equality)],[c_4037,c_28511]) ).
tff(c_20,plain,
! [X1_21,X0_20] : ( composition(converse(X1_21),converse(X0_20)) = converse(composition(X0_20,X1_21)) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_585,plain,
! [X0_60,X1_61] : ( join(composition(converse(X0_60),complement(composition(X0_60,X1_61))),complement(X1_61)) = complement(X1_61) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_618,plain,
! [X1_21,X0_20] : ( join(composition(converse(converse(X1_21)),complement(converse(composition(X0_20,X1_21)))),complement(converse(X0_20))) = complement(converse(X0_20)) ),
inference(superposition,[status(thm),theory(equality)],[c_20,c_585]) ).
tff(c_642,plain,
! [X0_20,X1_21] : ( join(complement(converse(X0_20)),composition(X1_21,complement(converse(composition(X0_20,X1_21))))) = complement(converse(X0_20)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16,c_618]) ).
tff(c_28639,plain,
join(complement(converse(top)),composition(top,complement(composition(top,top)))) = complement(converse(top)),
inference(superposition,[status(thm),theory(equality)],[c_28580,c_642]) ).
tff(c_28746,plain,
composition(top,complement(composition(top,top))) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_152,c_4037,c_1448,c_152,c_4037,c_28639]) ).
tff(c_14,plain,
! [X0_14,X2_16,X1_15] : ( join(composition(X0_14,X2_16),composition(X1_15,X2_16)) = composition(join(X0_14,X1_15),X2_16) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_28790,plain,
! [X1_15] : ( join(zero,composition(X1_15,complement(composition(top,top)))) = composition(join(top,X1_15),complement(composition(top,top))) ),
inference(superposition,[status(thm),theory(equality)],[c_28746,c_14]) ).
tff(c_28809,plain,
! [X1_15] : ( composition(X1_15,complement(composition(top,top))) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_28746,c_3902,c_1448,c_28790]) ).
tff(c_28815,plain,
! [X1_280] : ( composition(X1_280,complement(composition(top,top))) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_28746,c_3902,c_1448,c_28790]) ).
tff(c_10,plain,
! [X0_10,X1_11,X2_12] : ( composition(composition(X0_10,X1_11),X2_12) = composition(X0_10,composition(X1_11,X2_12)) ),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_28893,plain,
! [X0_10,X1_11] : ( composition(X0_10,composition(X1_11,complement(composition(top,top)))) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_28815,c_10]) ).
tff(c_28924,plain,
! [X0_10] : ( composition(X0_10,zero) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_28809,c_28893]) ).
tff(c_776,plain,
! [X1_65,X0_66] : ( meet(X1_65,X0_66) = meet(X0_66,X1_65) ),
inference(superposition,[status(thm),theory(equality)],[c_646,c_8]) ).
tff(c_36,plain,
meet(composition('#skF_1','#skF_2'),'#skF_3') = zero,
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_805,plain,
meet('#skF_3',composition('#skF_1','#skF_2')) = zero,
inference(superposition,[status(thm),theory(equality)],[c_776,c_36]) ).
tff(c_1777,plain,
! [X0_86,X1_87,X2_88] : ( join(meet(composition(X0_86,X1_87),X2_88),composition(meet(X0_86,composition(X2_88,converse(X1_87))),meet(X1_87,composition(converse(X0_86),X2_88)))) = composition(meet(X0_86,composition(X2_88,converse(X1_87))),meet(X1_87,composition(converse(X0_86),X2_88))) ),
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_1873,plain,
! [X0_17,X1_87,X2_88] : ( join(meet(composition(converse(X0_17),X1_87),X2_88),composition(meet(converse(X0_17),composition(X2_88,converse(X1_87))),meet(X1_87,composition(X0_17,X2_88)))) = composition(meet(converse(X0_17),composition(X2_88,converse(X1_87))),meet(X1_87,composition(converse(converse(X0_17)),X2_88))) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_1777]) ).
tff(c_40513,plain,
! [X0_348,X1_349,X2_350] : ( join(meet(composition(converse(X0_348),X1_349),X2_350),composition(meet(converse(X0_348),composition(X2_350,converse(X1_349))),meet(X1_349,composition(X0_348,X2_350)))) = composition(meet(converse(X0_348),composition(X2_350,converse(X1_349))),meet(X1_349,composition(X0_348,X2_350))) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_1873]) ).
tff(c_40878,plain,
join(meet(composition(converse('#skF_1'),'#skF_3'),'#skF_2'),composition(meet(converse('#skF_1'),composition('#skF_2',converse('#skF_3'))),zero)) = composition(meet(converse('#skF_1'),composition('#skF_2',converse('#skF_3'))),meet('#skF_3',composition('#skF_1','#skF_2'))),
inference(superposition,[status(thm),theory(equality)],[c_805,c_40513]) ).
tff(c_41028,plain,
meet('#skF_2',composition(converse('#skF_1'),'#skF_3')) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_28924,c_1448,c_2,c_28924,c_805,c_673,c_40878]) ).
tff(c_41030,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34,c_41028]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : REL010+2 : TPTP v9.0.0. Released v4.0.0.
% 0.03/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.12/0.34 % Computer : n017.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 : Tue Apr 8 17:44:25 EDT 2025
% 0.12/0.34 % CPUTime :
% 17.11/6.45 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.11/6.46
% 17.11/6.46 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------