%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : REL043+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n020.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:17 PM UTC 2025
% Result : Theorem 58.38s 44.07s
% Output : CNFRefutation 58.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 15
% Syntax : Number of formulae : 156 ( 155 unt; 0 typ; 0 def)
% Number of atoms : 157 ( 156 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 4 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 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 : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 208 ( 208 !; 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_53,axiom,
! [X0,X1] : ( join(X0,X1) = join(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux1_join_commutativity) ).
tff(f_120,negated_conjecture,
~ ! [X0,X1,X2] :
( ( join(composition(X0,converse(X1)),X2) = X2 )
=> ( join(composition(complement(X2),X1),complement(X0)) = complement(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
tff(f_80,axiom,
! [X0] : ( zero = meet(X0,complement(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_zero) ).
tff(f_78,axiom,
! [X0] : ( top = join(X0,complement(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_top) ).
tff(f_59,axiom,
! [X0,X1] : ( meet(X0,X1) = complement(join(complement(X0),complement(X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux4_definiton_of_meet) ).
tff(f_57,axiom,
! [X0,X1] : ( X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux3_a_kind_of_de_Morgan) ).
tff(f_55,axiom,
! [X0,X1,X2] : ( join(X0,join(X1,X2)) = join(join(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux2_join_associativity) ).
tff(f_69,axiom,
! [X0] : ( converse(converse(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
tff(f_71,axiom,
! [X0,X1] : ( converse(join(X0,X1)) = join(converse(X0),converse(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
tff(f_64,axiom,
! [X0] : ( composition(X0,one) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_identity) ).
tff(f_73,axiom,
! [X0,X1] : ( converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_multiplicativity) ).
tff(f_75,axiom,
! [X0,X1] : ( join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
tff(f_66,axiom,
! [X0,X1,X2] : ( composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
tff(f_62,axiom,
! [X0,X1,X2] : ( composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
tff(f_113,axiom,
! [X0,X1,X2] : ( join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+1.ax',modular_law_2) ).
tff(c_2,plain,
! [X1_2,X0_1] : ( join(X1_2,X0_1) = join(X0_1,X1_2) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_34,plain,
join(composition(complement('#skF_3'),'#skF_2'),complement('#skF_1')) != complement('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_38,plain,
join(complement('#skF_1'),composition(complement('#skF_3'),'#skF_2')) != complement('#skF_1'),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_34]) ).
tff(c_26,plain,
! [X0_25] : ( meet(X0_25,complement(X0_25)) = zero ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_24,plain,
! [X0_24] : ( join(X0_24,complement(X0_24)) = top ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_135,plain,
! [X0_41,X1_42] : ( complement(join(complement(X0_41),complement(X1_42))) = meet(X0_41,X1_42) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_169,plain,
! [X0_41] : ( meet(X0_41,complement(X0_41)) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_135]) ).
tff(c_172,plain,
complement(top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_169]) ).
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_59]) ).
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_57]) ).
tff(c_1042,plain,
! [X0_68,X1_69] : ( join(meet(X0_68,X1_69),complement(join(complement(X0_68),X1_69))) = X0_68 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_1099,plain,
! [X0_68] : ( join(meet(X0_68,complement(complement(X0_68))),complement(top)) = X0_68 ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_1042]) ).
tff(c_1111,plain,
! [X0_68] : ( join(zero,meet(X0_68,complement(complement(X0_68)))) = X0_68 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_172,c_1099]) ).
tff(c_182,plain,
join(top,zero) = top,
inference(superposition,[status(thm),theory(equality)],[c_172,c_24]) ).
tff(c_388,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_55]) ).
tff(c_457,plain,
! [X2_53] : ( join(top,join(zero,X2_53)) = join(top,X2_53) ),
inference(superposition,[status(thm),theory(equality)],[c_182,c_388]) ).
tff(c_478,plain,
join(top,complement(zero)) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_457]) ).
tff(c_179,plain,
! [X0_8] : ( complement(join(complement(X0_8),zero)) = meet(X0_8,top) ),
inference(superposition,[status(thm),theory(equality)],[c_172,c_8]) ).
tff(c_255,plain,
! [X0_44] : ( complement(join(zero,complement(X0_44))) = meet(X0_44,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_179]) ).
tff(c_304,plain,
meet(zero,top) = complement(top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_255]) ).
tff(c_308,plain,
meet(zero,top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_304]) ).
tff(c_1066,plain,
join(zero,complement(join(complement(zero),top))) = zero,
inference(superposition,[status(thm),theory(equality)],[c_308,c_1042]) ).
tff(c_1109,plain,
join(zero,complement(join(top,top))) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_478,c_2,c_1066]) ).
tff(c_176,plain,
! [X1_9] : ( complement(join(zero,complement(X1_9))) = meet(top,X1_9) ),
inference(superposition,[status(thm),theory(equality)],[c_172,c_8]) ).
tff(c_1339,plain,
meet(top,join(top,top)) = complement(zero),
inference(superposition,[status(thm),theory(equality)],[c_1109,c_176]) ).
tff(c_267,plain,
! [X0_44] : ( meet(top,X0_44) = meet(X0_44,top) ),
inference(superposition,[status(thm),theory(equality)],[c_255,c_176]) ).
tff(c_16,plain,
! [X0_17] : ( converse(converse(X0_17)) = X0_17 ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_425,plain,
! [X2_52] : ( join(top,join(zero,X2_52)) = join(top,X2_52) ),
inference(superposition,[status(thm),theory(equality)],[c_182,c_388]) ).
tff(c_1330,plain,
join(top,complement(join(top,top))) = join(top,zero),
inference(superposition,[status(thm),theory(equality)],[c_1109,c_425]) ).
tff(c_1343,plain,
join(top,complement(join(top,top))) = top,
inference(demodulation,[status(thm),theory(equality)],[c_182,c_1330]) ).
tff(c_361,plain,
! [X0_48,X1_49] : ( join(converse(X0_48),converse(X1_49)) = converse(join(X0_48,X1_49)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_736,plain,
! [X1_62,X0_63] : ( join(converse(X1_62),converse(X0_63)) = converse(join(X0_63,X1_62)) ),
inference(superposition,[status(thm),theory(equality)],[c_361,c_2]) ).
tff(c_18,plain,
! [X0_18,X1_19] : ( join(converse(X0_18),converse(X1_19)) = converse(join(X0_18,X1_19)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_776,plain,
! [X1_64,X0_65] : ( converse(join(X1_64,X0_65)) = converse(join(X0_65,X1_64)) ),
inference(superposition,[status(thm),theory(equality)],[c_736,c_18]) ).
tff(c_827,plain,
! [X1_64,X0_65] : ( converse(converse(join(X1_64,X0_65))) = join(X0_65,X1_64) ),
inference(superposition,[status(thm),theory(equality)],[c_776,c_16]) ).
tff(c_1561,plain,
join(complement(join(top,top)),top) = converse(converse(top)),
inference(superposition,[status(thm),theory(equality)],[c_1343,c_827]) ).
tff(c_1567,plain,
join(complement(join(top,top)),top) = top,
inference(demodulation,[status(thm),theory(equality)],[c_16,c_1561]) ).
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_1573,plain,
join(meet(join(top,top),top),complement(top)) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_1567,c_37]) ).
tff(c_1600,plain,
join(top,top) = top,
inference(demodulation,[status(thm),theory(equality)],[c_24,c_1339,c_267,c_2,c_172,c_1573]) ).
tff(c_1327,plain,
join(complement(join(top,top)),zero) = converse(converse(zero)),
inference(superposition,[status(thm),theory(equality)],[c_1109,c_827]) ).
tff(c_1342,plain,
join(complement(join(top,top)),zero) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_16,c_1327]) ).
tff(c_1613,plain,
join(complement(top),zero) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_1600,c_1342]) ).
tff(c_1618,plain,
join(zero,zero) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_1613]) ).
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_55]) ).
tff(c_2508,plain,
! [X2_96] : ( join(zero,join(zero,X2_96)) = join(zero,X2_96) ),
inference(superposition,[status(thm),theory(equality)],[c_1618,c_4]) ).
tff(c_2549,plain,
! [X0_68] : ( join(zero,meet(X0_68,complement(complement(X0_68)))) = join(zero,X0_68) ),
inference(superposition,[status(thm),theory(equality)],[c_1111,c_2508]) ).
tff(c_2583,plain,
! [X0_68] : ( join(zero,X0_68) = X0_68 ),
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_2549]) ).
tff(c_3512,plain,
! [X1_107,X0_108] : ( complement(join(complement(X1_107),complement(X0_108))) = meet(X0_108,X1_107) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_135]) ).
tff(c_3554,plain,
! [X1_107,X0_108] : ( meet(X1_107,X0_108) = meet(X0_108,X1_107) ),
inference(superposition,[status(thm),theory(equality)],[c_3512,c_8]) ).
tff(c_3585,plain,
! [X1_107] : ( complement(join(complement(X1_107),zero)) = meet(top,X1_107) ),
inference(superposition,[status(thm),theory(equality)],[c_172,c_3512]) ).
tff(c_3611,plain,
! [X1_107] : ( complement(complement(X1_107)) = meet(top,X1_107) ),
inference(demodulation,[status(thm),theory(equality)],[c_2583,c_2,c_3585]) ).
tff(c_12,plain,
! [X0_13] : ( composition(X0_13,one) = X0_13 ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_313,plain,
! [X1_45,X0_46] : ( composition(converse(X1_45),converse(X0_46)) = converse(composition(X0_46,X1_45)) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_3114,plain,
! [X0_102,X1_103] : ( converse(composition(converse(X0_102),X1_103)) = composition(converse(X1_103),X0_102) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_313]) ).
tff(c_3182,plain,
! [X0_102] : ( composition(converse(one),X0_102) = converse(converse(X0_102)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_3114]) ).
tff(c_3202,plain,
! [X0_104] : ( composition(converse(one),X0_104) = X0_104 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_3182]) ).
tff(c_3263,plain,
converse(one) = one,
inference(superposition,[status(thm),theory(equality)],[c_3202,c_12]) ).
tff(c_3199,plain,
! [X0_102] : ( composition(converse(one),X0_102) = X0_102 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_3182]) ).
tff(c_3295,plain,
! [X0_102] : ( composition(one,X0_102) = X0_102 ),
inference(demodulation,[status(thm),theory(equality)],[c_3263,c_3199]) ).
tff(c_3450,plain,
! [X0_106] : ( composition(one,X0_106) = X0_106 ),
inference(demodulation,[status(thm),theory(equality)],[c_3263,c_3199]) ).
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_75]) ).
tff(c_3483,plain,
! [X0_106] : ( join(composition(converse(one),complement(X0_106)),complement(X0_106)) = complement(X0_106) ),
inference(superposition,[status(thm),theory(equality)],[c_3450,c_22]) ).
tff(c_4326,plain,
! [X0_119] : ( join(complement(X0_119),complement(X0_119)) = complement(X0_119) ),
inference(demodulation,[status(thm),theory(equality)],[c_3295,c_2,c_3263,c_3483]) ).
tff(c_4341,plain,
! [X0_119] : ( join(meet(X0_119,complement(X0_119)),complement(complement(X0_119))) = X0_119 ),
inference(superposition,[status(thm),theory(equality)],[c_4326,c_37]) ).
tff(c_4394,plain,
! [X0_119] : ( meet(top,X0_119) = X0_119 ),
inference(demodulation,[status(thm),theory(equality)],[c_3611,c_2583,c_26,c_4341]) ).
tff(c_4411,plain,
! [X1_107] : ( complement(complement(X1_107)) = X1_107 ),
inference(demodulation,[status(thm),theory(equality)],[c_4394,c_3611]) ).
tff(c_4487,plain,
! [X1_121] : ( complement(complement(X1_121)) = X1_121 ),
inference(demodulation,[status(thm),theory(equality)],[c_4394,c_3611]) ).
tff(c_3504,plain,
! [X0_106] : ( join(complement(X0_106),complement(X0_106)) = complement(X0_106) ),
inference(demodulation,[status(thm),theory(equality)],[c_3295,c_2,c_3263,c_3483]) ).
tff(c_4499,plain,
! [X1_121] : ( join(complement(complement(X1_121)),X1_121) = complement(complement(X1_121)) ),
inference(superposition,[status(thm),theory(equality)],[c_4487,c_3504]) ).
tff(c_4732,plain,
! [X1_125] : ( join(X1_125,X1_125) = X1_125 ),
inference(demodulation,[status(thm),theory(equality)],[c_4411,c_4411,c_4499]) ).
tff(c_452,plain,
! [X0_50,X1_51] : ( join(X0_50,join(X1_51,complement(join(X0_50,X1_51)))) = top ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_388]) ).
tff(c_4754,plain,
! [X1_125] : ( join(X1_125,join(X1_125,complement(X1_125))) = top ),
inference(superposition,[status(thm),theory(equality)],[c_4732,c_452]) ).
tff(c_4845,plain,
! [X1_125] : ( join(X1_125,top) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_4754]) ).
tff(c_925,plain,
! [X1_66,X0_67] : ( converse(converse(join(X1_66,X0_67))) = join(X0_67,X1_66) ),
inference(superposition,[status(thm),theory(equality)],[c_776,c_16]) ).
tff(c_1015,plain,
! [X0_24] : ( join(complement(X0_24),X0_24) = converse(converse(top)) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_925]) ).
tff(c_1113,plain,
! [X0_70] : ( join(complement(X0_70),X0_70) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_1015]) ).
tff(c_1158,plain,
join(zero,top) = top,
inference(superposition,[status(thm),theory(equality)],[c_172,c_1113]) ).
tff(c_2268,plain,
! [X2_91] : ( join(zero,join(top,X2_91)) = join(top,X2_91) ),
inference(superposition,[status(thm),theory(equality)],[c_1158,c_4]) ).
tff(c_2311,plain,
! [X1_2] : ( join(zero,join(X1_2,top)) = join(top,X1_2) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_2268]) ).
tff(c_4975,plain,
! [X1_2] : ( join(top,X1_2) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_4845,c_4845,c_2311]) ).
tff(c_448,plain,
! [X0_24,X2_52] : ( join(X0_24,join(complement(X0_24),X2_52)) = join(top,X2_52) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_388]) ).
tff(c_6118,plain,
! [X0_137,X2_138] : ( join(X0_137,join(complement(X0_137),X2_138)) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_4975,c_448]) ).
tff(c_6168,plain,
! [X0_6,X2_138] : ( join(meet(X0_6,join(complement(complement(X0_6)),X2_138)),complement(top)) = X0_6 ),
inference(superposition,[status(thm),theory(equality)],[c_6118,c_37]) ).
tff(c_6321,plain,
! [X0_139,X2_140] : ( meet(X0_139,join(X0_139,X2_140)) = X0_139 ),
inference(demodulation,[status(thm),theory(equality)],[c_4411,c_2583,c_2,c_172,c_6168]) ).
tff(c_6455,plain,
! [X0_141] : ( meet(zero,X0_141) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_2583,c_6321]) ).
tff(c_6468,plain,
! [X0_141] : ( meet(X0_141,zero) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_6455,c_3554]) ).
tff(c_2595,plain,
! [X0_97] : ( join(zero,X0_97) = X0_97 ),
inference(demodulation,[status(thm),theory(equality)],[c_1111,c_2549]) ).
tff(c_2667,plain,
! [X0_1] : ( join(X0_1,zero) = X0_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_2595]) ).
tff(c_5307,plain,
! [X0_130,X1_131] : ( converse(join(converse(X0_130),X1_131)) = join(X0_130,converse(X1_131)) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_361]) ).
tff(c_5389,plain,
! [X0_130] : ( join(X0_130,converse(zero)) = converse(converse(X0_130)) ),
inference(superposition,[status(thm),theory(equality)],[c_2667,c_5307]) ).
tff(c_5446,plain,
! [X0_132] : ( join(X0_132,converse(zero)) = X0_132 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_5389]) ).
tff(c_5472,plain,
converse(zero) = zero,
inference(superposition,[status(thm),theory(equality)],[c_5446,c_2583]) ).
tff(c_5749,plain,
! [X0_134] : ( join(X0_134,converse(top)) = converse(top) ),
inference(superposition,[status(thm),theory(equality)],[c_4845,c_5307]) ).
tff(c_5758,plain,
converse(top) = top,
inference(superposition,[status(thm),theory(equality)],[c_5749,c_4975]) ).
tff(c_1345,plain,
! [X0_74,X1_75] : ( join(composition(converse(X0_74),complement(composition(X0_74,X1_75))),complement(X1_75)) = complement(X1_75) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_1402,plain,
! [X0_74,X0_8,X1_9] : ( join(composition(converse(X0_74),complement(composition(X0_74,join(complement(X0_8),complement(X1_9))))),meet(X0_8,X1_9)) = complement(join(complement(X0_8),complement(X1_9))) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_1345]) ).
tff(c_41715,plain,
! [X0_349,X0_350,X1_351] : ( join(composition(converse(X0_349),complement(composition(X0_349,join(complement(X0_350),complement(X1_351))))),meet(X0_350,X1_351)) = meet(X0_350,X1_351) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_1402]) ).
tff(c_42082,plain,
! [X0_349,X0_350] : ( join(composition(converse(X0_349),complement(composition(X0_349,top))),meet(X0_350,complement(X0_350))) = meet(X0_350,complement(X0_350)) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_41715]) ).
tff(c_43350,plain,
! [X0_357] : ( composition(converse(X0_357),complement(composition(X0_357,top))) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_2583,c_2,c_26,c_26,c_42082]) ).
tff(c_43450,plain,
composition(top,complement(composition(top,top))) = zero,
inference(superposition,[status(thm),theory(equality)],[c_5758,c_43350]) ).
tff(c_1654,plain,
! [X0_77,X2_78,X1_79] : ( join(composition(X0_77,X2_78),composition(X1_79,X2_78)) = composition(join(X0_77,X1_79),X2_78) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_1672,plain,
! [X1_79,X2_78,X0_77] : ( join(composition(X1_79,X2_78),composition(X0_77,X2_78)) = composition(join(X0_77,X1_79),X2_78) ),
inference(superposition,[status(thm),theory(equality)],[c_1654,c_2]) ).
tff(c_43563,plain,
! [X0_77] : ( join(zero,composition(X0_77,complement(composition(top,top)))) = composition(join(X0_77,top),complement(composition(top,top))) ),
inference(superposition,[status(thm),theory(equality)],[c_43450,c_1672]) ).
tff(c_43595,plain,
! [X0_77] : ( composition(X0_77,complement(composition(top,top))) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_43450,c_4845,c_2583,c_43563]) ).
tff(c_43688,plain,
! [X0_358] : ( composition(X0_358,complement(composition(top,top))) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_43450,c_4845,c_2583,c_43563]) ).
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_62]) ).
tff(c_1687,plain,
! [X0_10,X1_11,X2_12,X1_79] : ( join(composition(X0_10,composition(X1_11,X2_12)),composition(X1_79,X2_12)) = composition(join(composition(X0_10,X1_11),X1_79),X2_12) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_1654]) ).
tff(c_43696,plain,
! [X0_10,X1_79,X0_358] : ( join(composition(X0_10,zero),composition(X1_79,complement(composition(top,top)))) = composition(join(composition(X0_10,X0_358),X1_79),complement(composition(top,top))) ),
inference(superposition,[status(thm),theory(equality)],[c_43688,c_1687]) ).
tff(c_43851,plain,
! [X0_359] : ( composition(X0_359,zero) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_43595,c_2583,c_2,c_43595,c_43696]) ).
tff(c_325,plain,
! [X0_17,X1_45] : ( converse(composition(converse(X0_17),X1_45)) = composition(converse(X1_45),X0_17) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_313]) ).
tff(c_43914,plain,
! [X0_17] : ( composition(converse(zero),X0_17) = converse(zero) ),
inference(superposition,[status(thm),theory(equality)],[c_43851,c_325]) ).
tff(c_43967,plain,
! [X0_17] : ( composition(zero,X0_17) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_5472,c_5472,c_43914]) ).
tff(c_36,plain,
join(composition('#skF_1',converse('#skF_2')),'#skF_3') = '#skF_3',
inference(cnfTransformation,[status(thm)],[f_120]) ).
tff(c_6426,plain,
meet(composition('#skF_1',converse('#skF_2')),'#skF_3') = composition('#skF_1',converse('#skF_2')),
inference(superposition,[status(thm),theory(equality)],[c_36,c_6321]) ).
tff(c_7286,plain,
! [X0_151,X1_152,X2_153] : ( join(join(X0_151,X1_152),X2_153) = join(X1_152,join(X0_151,X2_153)) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_388]) ).
tff(c_7546,plain,
! [X0_24,X2_153] : ( join(complement(X0_24),join(X0_24,X2_153)) = join(top,X2_153) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_7286]) ).
tff(c_7594,plain,
! [X0_154,X2_155] : ( join(complement(X0_154),join(X0_154,X2_155)) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_4975,c_7546]) ).
tff(c_7727,plain,
! [X0_6,X1_7] : ( join(complement(meet(X0_6,X1_7)),X0_6) = top ),
inference(superposition,[status(thm),theory(equality)],[c_37,c_7594]) ).
tff(c_8723,plain,
! [X0_163,X1_164] : ( meet(join(complement(X0_163),complement(X1_164)),meet(X0_163,X1_164)) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_135,c_26]) ).
tff(c_8752,plain,
! [X1_164,X1_7] : ( meet(top,meet(meet(complement(X1_164),X1_7),X1_164)) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_7727,c_8723]) ).
tff(c_10582,plain,
! [X1_178,X1_179] : ( meet(X1_178,meet(complement(X1_178),X1_179)) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_4394,c_3554,c_8752]) ).
tff(c_13311,plain,
! [X1_196,X1_197] : ( meet(complement(X1_196),meet(X1_196,X1_197)) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_4411,c_10582]) ).
tff(c_14963,plain,
! [X1_207,X0_208] : ( meet(complement(X1_207),meet(X0_208,X1_207)) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_3554,c_13311]) ).
tff(c_15048,plain,
meet(complement('#skF_3'),composition('#skF_1',converse('#skF_2'))) = zero,
inference(superposition,[status(thm),theory(equality)],[c_6426,c_14963]) ).
tff(c_1874,plain,
! [X0_82,X1_83,X2_84] : ( join(meet(composition(X0_82,X1_83),X2_84),meet(composition(meet(X0_82,composition(X2_84,converse(X1_83))),X1_83),X2_84)) = meet(composition(meet(X0_82,composition(X2_84,converse(X1_83))),X1_83),X2_84) ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_1941,plain,
! [X0_82,X0_17,X2_84] : ( join(meet(composition(X0_82,converse(X0_17)),X2_84),meet(composition(meet(X0_82,composition(X2_84,X0_17)),converse(X0_17)),X2_84)) = meet(composition(meet(X0_82,composition(X2_84,converse(converse(X0_17)))),converse(X0_17)),X2_84) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_1874]) ).
tff(c_1956,plain,
! [X0_82,X0_17,X2_84] : ( join(meet(composition(X0_82,converse(X0_17)),X2_84),meet(composition(meet(X0_82,composition(X2_84,X0_17)),converse(X0_17)),X2_84)) = meet(composition(meet(X0_82,composition(X2_84,X0_17)),converse(X0_17)),X2_84) ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_1941]) ).
tff(c_47096,plain,
! [X0_375,X0_376,X2_377] : ( join(meet(composition(X0_375,converse(X0_376)),X2_377),meet(X2_377,composition(meet(X0_375,composition(X2_377,X0_376)),converse(X0_376)))) = meet(X2_377,composition(meet(X0_375,composition(X2_377,X0_376)),converse(X0_376))) ),
inference(demodulation,[status(thm),theory(equality)],[c_3554,c_3554,c_1956]) ).
tff(c_47281,plain,
join(meet(composition(complement('#skF_3'),converse(converse('#skF_2'))),'#skF_1'),meet('#skF_1',composition(zero,converse(converse('#skF_2'))))) = meet('#skF_1',composition(meet(complement('#skF_3'),composition('#skF_1',converse('#skF_2'))),converse(converse('#skF_2')))),
inference(superposition,[status(thm),theory(equality)],[c_15048,c_47096]) ).
tff(c_47496,plain,
meet('#skF_1',composition(complement('#skF_3'),'#skF_2')) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_6468,c_43967,c_2583,c_6468,c_43967,c_15048,c_3554,c_2,c_16,c_16,c_16,c_47281]) ).
tff(c_6600,plain,
! [X0_143,X1_144] : ( join(meet(X0_143,complement(X1_144)),meet(X0_143,X1_144)) = X0_143 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_1042]) ).
tff(c_166967,plain,
! [X1_701,X1_702] : ( join(meet(complement(X1_701),X1_702),meet(X1_702,X1_701)) = X1_702 ),
inference(superposition,[status(thm),theory(equality)],[c_3554,c_6600]) ).
tff(c_167541,plain,
join(meet(complement(composition(complement('#skF_3'),'#skF_2')),'#skF_1'),zero) = '#skF_1',
inference(superposition,[status(thm),theory(equality)],[c_47496,c_166967]) ).
tff(c_167918,plain,
meet('#skF_1',complement(composition(complement('#skF_3'),'#skF_2'))) = '#skF_1',
inference(demodulation,[status(thm),theory(equality)],[c_2583,c_2,c_3554,c_167541]) ).
tff(c_27287,plain,
! [X0_278,X0_279,X1_280] : ( meet(X0_278,join(complement(X0_279),complement(X1_280))) = complement(join(complement(X0_278),meet(X0_279,X1_280))) ),
inference(superposition,[status(thm),theory(equality)],[c_135,c_8]) ).
tff(c_27510,plain,
! [X0_278,X1_280] : ( complement(join(complement(X0_278),meet(top,X1_280))) = meet(X0_278,join(zero,complement(X1_280))) ),
inference(superposition,[status(thm),theory(equality)],[c_172,c_27287]) ).
tff(c_197871,plain,
! [X0_749,X1_750] : ( complement(join(complement(X0_749),X1_750)) = meet(X0_749,complement(X1_750)) ),
inference(demodulation,[status(thm),theory(equality)],[c_4394,c_2583,c_27510]) ).
tff(c_226331,plain,
! [X0_805,X1_806] : ( complement(meet(X0_805,complement(X1_806))) = join(complement(X0_805),X1_806) ),
inference(superposition,[status(thm),theory(equality)],[c_197871,c_4411]) ).
tff(c_226665,plain,
join(complement('#skF_1'),composition(complement('#skF_3'),'#skF_2')) = complement('#skF_1'),
inference(superposition,[status(thm),theory(equality)],[c_167918,c_226331]) ).
tff(c_226886,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_38,c_226665]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : REL043+2 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n020.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 : Tue Apr 8 18:10:34 EDT 2025
% 0.13/0.34 % CPUTime :
% 58.38/44.07 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 58.47/44.09
% 58.47/44.09 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------