%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : REL011-2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n019.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 : 600s % DateTime : Mon Jul 18 19:23:10 EDT 2022 % Result : Unsatisfiable 162.73s 163.19s % Output : CNFRefutation 162.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : REL011-2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : fiesta-wrapper %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Fri Jul 8 14:17:38 EDT 2022 % 0.13/0.35 % CPUTime : % 162.73/163.19 Theorem Proved. % 162.73/163.19 % SZS status Unsatisfiable % 162.73/163.19 % SZS output start CNFRefutation % 162.73/163.19 [1=axiom,[], % 162.73/163.19 meet(sk1,composition(converse(sk2),sk3)) = zero]. % 162.73/163.19 [3=axiom,[], % 162.73/163.19 join(meet(composition(X10,X11),X12),meet(composition(X10,meet(X11,composition(converse(X10),X12))),X12)) = meet(composition(X10,meet(X11,composition(converse(X10),X12))),X12)]. % 162.73/163.19 [4=axiom,[], % 162.73/163.19 join(meet(composition(X10,X11),X12),composition(meet(X10,composition(X12,converse(X11))),meet(X11,composition(converse(X10),X12)))) = composition(meet(X10,composition(X12,converse(X11))),meet(X11,composition(converse(X10),X12)))]. % 162.73/163.19 [5=axiom,[], % 162.73/163.19 meet(X10,complement(X10)) = zero]. % 162.73/163.19 [6=axiom,[], % 162.73/163.19 join(X10,complement(X10)) = top]. % 162.73/163.19 [7=axiom,[], % 162.73/163.19 join(composition(converse(X10),complement(composition(X10,X11))),complement(X11)) = complement(X11)]. % 162.73/163.19 [8=axiom,[], % 162.73/163.19 converse(composition(X10,X11)) = composition(converse(X11),converse(X10))]. % 162.73/163.19 [9=axiom,[], % 162.73/163.19 join(converse(X10),converse(X11)) = converse(join(X10,X11))]. % 162.73/163.19 [10=axiom,[], % 162.73/163.19 converse(converse(X10)) = X10]. % 162.73/163.19 [11=axiom,[], % 162.73/163.19 join(composition(X10,X12),composition(X11,X12)) = composition(join(X10,X11),X12)]. % 162.73/163.19 [12=axiom,[], % 162.73/163.19 composition(X10,one) = X10]. % 162.73/163.19 [13=axiom,[], % 162.73/163.19 composition(composition(X10,X11),X12) = composition(X10,composition(X11,X12))]. % 162.73/163.19 [14=axiom,[], % 162.73/163.19 complement(join(complement(X10),complement(X11))) = meet(X10,X11)]. % 162.73/163.19 [15=axiom,[14], % 162.73/163.19 join(meet(X10,X11),complement(join(complement(X10),X11))) = X10]. % 162.73/163.19 [16=axiom,[], % 162.73/163.19 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 162.73/163.19 [17=axiom,[], % 162.73/163.19 join(X10,X11) = join(X11,X10)]. % 162.73/163.19 [18=demod(4),[17], % 162.73/163.19 join(composition(meet(X10,composition(X11,converse(X12))),meet(X12,composition(converse(X10),X11))),meet(composition(X10,X12),X11)) = composition(meet(X10,composition(X11,converse(X12))),meet(X12,composition(converse(X10),X11)))]. % 162.73/163.19 [19=demod(7),[17], % 162.73/163.19 join(complement(X10),composition(converse(X11),complement(composition(X11,X10)))) = complement(X10)]. % 162.73/163.19 [20=axiom,[], % 162.73/163.19 thtop(X10,X10) = thmfalse]. % 162.73/163.19 [21=axiom,[], % 162.73/163.19 thtop(meet(composition(sk2,sk1),sk3),zero) = thmtrue]. % 162.73/163.19 [23=param(9,10),[], % 162.73/163.19 join(converse(X10),X11) = converse(join(X10,converse(X11)))]. % 162.73/163.19 [24=param(23,6),[], % 162.73/163.19 converse(join(X10,converse(complement(converse(X10))))) = top]. % 162.73/163.19 [25=param(23,17),[], % 162.73/163.19 converse(join(X10,converse(X11))) = join(X11,converse(X10))]. % 162.73/163.19 [26=param(10,24),[], % 162.73/163.19 join(X10,converse(complement(converse(X10)))) = converse(top)]. % 162.73/163.19 [28=param(10,8),[], % 162.73/163.19 converse(composition(converse(X10),converse(X11))) = composition(X11,X10)]. % 162.73/163.19 [29=demod(1),[-28,10], % 162.73/163.19 meet(sk1,converse(composition(converse(sk3),sk2))) = zero]. % 162.73/163.19 [31=param(8,12),[], % 162.73/163.19 composition(converse(one),converse(X10)) = converse(X10)]. % 162.73/163.19 [34=param(8,10),[], % 162.73/163.19 composition(X10,converse(X11)) = converse(composition(X11,converse(X10)))]. % 162.73/163.19 [37=param(31,10),[10], % 162.73/163.19 composition(converse(one),X10) = X10]. % 162.73/163.19 [38=param(37,12),[], % 162.73/163.19 converse(one) = one]. % 162.73/163.19 [39=demod(37),[38], % 162.73/163.19 composition(one,X10) = X10]. % 162.73/163.19 [40=param(11,17),[11], % 162.73/163.19 composition(join(X10,X11),X12) = composition(join(X11,X10),X12)]. % 162.73/163.19 [43=param(11,39),[], % 162.73/163.19 join(X10,composition(X11,X10)) = composition(join(one,X11),X10)]. % 162.73/163.19 [44=param(11,39),[17], % 162.73/163.19 join(X10,composition(X11,X10)) = composition(join(X11,one),X10)]. % 162.73/163.19 [45=param(8,13),[], % 162.73/163.19 converse(composition(X10,composition(X11,X12))) = composition(converse(X12),converse(composition(X10,X11)))]. % 162.73/163.19 [46=param(13,8),[], % 162.73/163.19 composition(converse(composition(X10,X11)),X12) = composition(converse(X11),composition(converse(X10),X12))]. % 162.73/163.19 [52=param(14,6),[5], % 162.73/163.19 complement(top) = zero]. % 162.73/163.19 [53=param(6,14),[16], % 162.73/163.19 join(complement(X10),join(complement(X11),meet(X10,X11))) = top]. % 162.73/163.19 [56=param(14,17),[14], % 162.73/163.19 meet(X10,X11) = meet(X11,X10)]. % 162.73/163.19 [57=demod(3),[56,56], % 162.73/163.19 join(meet(composition(X10,X11),X12),meet(X12,composition(X10,meet(X11,composition(converse(X10),X12))))) = meet(X12,composition(X10,meet(X11,composition(converse(X10),X12))))]. % 162.73/163.19 [60=param(5,52),[56], % 162.73/163.19 meet(zero,top) = zero]. % 162.73/163.19 [62=param(14,52),[], % 162.73/163.19 complement(join(zero,complement(X10))) = meet(top,X10)]. % 162.73/163.19 [63=param(15,5),[14], % 162.73/163.19 join(zero,meet(X10,X10)) = X10]. % 162.73/163.19 [64=param(15,6),[52,17], % 162.73/163.19 join(zero,meet(X10,complement(complement(X10)))) = X10]. % 162.73/163.19 [65=param(15,14),[17], % 162.73/163.19 join(meet(X10,X11),meet(X10,complement(X11))) = X10]. % 162.73/163.19 [66=param(15,17),[], % 162.73/163.19 join(meet(X10,X11),complement(join(X11,complement(X10)))) = X10]. % 162.73/163.19 [67=param(15,26),[17], % 162.73/163.19 join(complement(converse(top)),meet(X10,converse(complement(converse(complement(X10)))))) = X10]. % 162.73/163.19 [69=param(15,60),[17], % 162.73/163.19 join(zero,complement(join(top,complement(zero)))) = zero]. % 162.73/163.19 [72=param(16,15),[], % 162.73/163.19 join(meet(X10,X12),join(complement(join(complement(X10),X12)),X11)) = join(X10,X11)]. % 162.73/163.19 [73=param(16,17),[], % 162.73/163.19 join(X10,join(X11,X12)) = join(X12,join(X10,X11))]. % 162.73/163.19 [74=param(16,17),[16], % 162.73/163.19 join(X10,join(X11,X12)) = join(X11,join(X10,X12))]. % 162.73/163.19 [79=param(15,56),[], % 162.73/163.19 join(meet(X10,X11),complement(join(complement(X11),X10))) = X11]. % 162.73/163.19 [100=param(19,38),[39,39], % 162.73/163.19 join(complement(X10),complement(X10)) = complement(X10)]. % 162.73/163.19 [119=param(14,100),[], % 162.73/163.19 meet(X10,X10) = complement(complement(X10))]. % 162.73/163.19 [121=demod(63),[119], % 162.73/163.19 join(zero,complement(complement(X10))) = X10]. % 162.73/163.19 [125=param(100,52),[52,52], % 162.73/163.19 join(zero,zero) = zero]. % 162.73/163.19 [126=param(16,125),[], % 162.73/163.19 join(zero,join(zero,X10)) = join(zero,X10)]. % 162.73/163.19 [131=param(121,14),[], % 162.73/163.19 join(complement(X10),complement(X11)) = join(zero,complement(meet(X10,X11)))]. % 162.73/163.19 [139=param(62,121),[], % 162.73/163.19 meet(top,complement(X10)) = complement(X10)]. % 162.73/163.19 [150=param(15,139),[52,62], % 162.73/163.19 join(complement(X10),meet(top,X10)) = top]. % 162.73/163.19 [153=param(150,56),[], % 162.73/163.19 join(complement(X10),meet(X10,top)) = top]. % 162.73/163.19 [157=param(16,153),[], % 162.73/163.19 join(complement(X11),join(meet(X11,top),X10)) = join(top,X10)]. % 162.73/163.19 [170=param(126,121),[121], % 162.73/163.19 join(zero,X10) = X10]. % 162.73/163.19 [171=demod(64),[170], % 162.73/163.19 meet(X10,complement(complement(X10))) = X10]. % 162.73/163.19 [176=demod(62),[170], % 162.73/163.19 meet(top,X10) = complement(complement(X10))]. % 162.73/163.19 [179=demod(69),[170], % 162.73/163.19 complement(join(top,complement(zero))) = zero]. % 162.73/163.19 [181=demod(121),[170], % 162.73/163.19 complement(complement(X10)) = X10]. % 162.73/163.19 [182=demod(176),[181], % 162.73/163.19 meet(top,X10) = X10]. % 162.73/163.19 [183=demod(171),[181], % 162.73/163.19 meet(X10,X10) = X10]. % 162.73/163.19 [186=demod(131),[170], % 162.73/163.19 join(complement(X10),complement(X11)) = complement(meet(X10,X11))]. % 162.73/163.19 [194=param(182,56),[], % 162.73/163.19 meet(X10,top) = X10]. % 162.73/163.19 [195=demod(157),[194], % 162.73/163.19 join(complement(X10),join(X10,X11)) = join(top,X11)]. % 162.73/163.19 [204=param(181,52),[], % 162.73/163.19 complement(zero) = top]. % 162.73/163.19 [205=demod(179),[204], % 162.73/163.19 complement(join(top,top)) = zero]. % 162.73/163.19 [209=param(15,204),[], % 162.73/163.19 join(meet(zero,X10),complement(join(top,X10))) = zero]. % 162.73/163.19 [211=param(25,170),[10], % 162.73/163.19 join(X10,converse(zero)) = X10]. % 162.73/163.19 [223=param(211,170),[], % 162.73/163.19 converse(zero) = zero]. % 162.73/163.19 [229=param(28,223),[], % 162.73/163.19 converse(composition(zero,converse(X10))) = composition(X10,zero)]. % 162.73/163.19 [242=param(40,43),[13,17], % 162.73/163.19 composition(join(one,X10),composition(X11,X12)) = composition(join(X11,composition(X10,X11)),X12)]. % 162.73/163.19 [254=param(6,205),[16,17,170], % 162.73/163.19 join(top,top) = top]. % 162.73/163.19 [255=param(16,254),[], % 162.73/163.19 join(top,join(top,X10)) = join(top,X10)]. % 162.73/163.19 [281=param(45,34),[10], % 162.73/163.19 converse(composition(X10,converse(composition(X11,converse(X12))))) = composition(X11,converse(composition(X10,X12)))]. % 162.73/163.19 [293=param(255,26),[26], % 162.73/163.19 join(top,converse(top)) = converse(top)]. % 162.73/163.19 [296=param(293,17),[23,293,10], % 162.73/163.19 converse(top) = top]. % 162.73/163.19 [306=demod(67),[296,52,170], % 162.73/163.19 meet(X10,converse(complement(converse(complement(X10))))) = X10]. % 162.73/163.19 [308=demod(26),[296], % 162.73/163.19 join(X10,converse(complement(converse(X10)))) = top]. % 162.73/163.19 [328=param(53,183),[17,6,17], % 162.73/163.19 join(top,complement(X10)) = top]. % 162.73/163.19 [333=param(328,181),[], % 162.73/163.19 join(top,X10) = top]. % 162.73/163.19 [335=demod(195),[333], % 162.73/163.19 join(complement(X10),join(X10,X11)) = top]. % 162.73/163.19 [338=demod(209),[333,52,17,170], % 162.73/163.19 meet(zero,X10) = zero]. % 162.73/163.19 [340=param(338,56),[], % 162.73/163.19 meet(X10,zero) = zero]. % 162.73/163.19 [341=param(333,17),[], % 162.73/163.19 join(X10,top) = top]. % 162.73/163.19 [343=param(44,333),[], % 162.73/163.19 join(X10,composition(top,X10)) = composition(top,X10)]. % 162.73/163.19 [349=param(343,333),[], % 162.73/163.19 composition(top,top) = top]. % 162.73/163.19 [351=param(65,29),[170], % 162.73/163.19 meet(sk1,complement(converse(composition(converse(sk3),sk2)))) = sk1]. % 162.73/163.19 [355=param(19,349),[52,296,52,-229,296,170,52], % 162.73/163.19 converse(composition(zero,top)) = zero]. % 162.73/163.19 [359=param(10,355),[223], % 162.73/163.19 composition(zero,top) = zero]. % 162.73/163.19 [365=param(46,359),[223,296,223], % 162.73/163.19 composition(top,composition(zero,X10)) = composition(zero,X10)]. % 162.73/163.19 [366=param(11,365),[43,242,170,13,333,365], % 162.73/163.19 composition(X10,composition(zero,X11)) = composition(zero,X11)]. % 162.73/163.19 [375=param(366,12),[12], % 162.73/163.19 composition(X10,zero) = zero]. % 162.73/163.19 [417=param(74,6),[341], % 162.73/163.19 join(X10,join(X11,complement(X10))) = top]. % 162.73/163.19 [438=param(417,72),[], % 162.73/163.19 join(X10,complement(meet(X10,X11))) = top]. % 162.73/163.19 [440=param(79,5),[181,170], % 162.73/163.19 complement(join(X10,X10)) = complement(X10)]. % 162.73/163.19 [447=param(74,79),[], % 162.73/163.19 join(meet(X12,X11),join(X10,complement(join(complement(X11),X12)))) = join(X10,X11)]. % 162.73/163.19 [461=param(181,440),[181], % 162.73/163.19 join(X10,X10) = X10]. % 162.73/163.19 [469=param(73,461),[], % 162.73/163.19 join(X11,join(X10,X11)) = join(X10,X11)]. % 162.73/163.19 [480=param(469,72),[17,15], % 162.73/163.19 join(X10,meet(X10,X11)) = X10]. % 162.73/163.19 [485=param(43,480),[39], % 162.73/163.19 join(X10,composition(meet(one,X11),X10)) = X10]. % 162.73/163.19 [486=param(480,56),[], % 162.73/163.19 join(X10,meet(X11,X10)) = X10]. % 162.73/163.19 [517=param(66,438),[56,52,17,170], % 162.73/163.19 meet(X10,meet(X10,X11)) = meet(X10,X11)]. % 162.73/163.19 [567=param(335,79),[17], % 162.73/163.19 join(X10,complement(meet(X11,X10))) = top]. % 162.73/163.19 [579=param(66,567),[56,52,17,170], % 162.73/163.19 meet(X10,meet(X11,X10)) = meet(X11,X10)]. % 162.73/163.19 [581=param(74,567),[341], % 162.73/163.19 join(X10,join(X11,complement(meet(X12,X10)))) = top]. % 162.73/163.19 [604=param(73,186),[], % 162.73/163.19 join(X10,complement(meet(X11,X12))) = join(complement(X12),join(X10,complement(X11)))]. % 162.73/163.19 [608=param(186,181),[], % 162.73/163.19 join(X10,complement(X11)) = complement(meet(complement(X10),X11))]. % 162.73/163.19 [633=demod(447),[608,608], % 162.73/163.19 complement(meet(complement(meet(X10,X11)),meet(complement(X12),join(complement(X11),X10)))) = join(X12,X11)]. % 162.73/163.19 [648=demod(581),[608,608], % 162.73/163.19 complement(meet(complement(X10),meet(complement(X11),meet(X12,X10)))) = top]. % 162.73/163.19 [649=demod(438),[608], % 162.73/163.19 complement(meet(complement(X10),meet(X10,X11))) = top]. % 162.73/163.19 [654=demod(604),[608,608,608,181], % 162.73/163.19 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X12,meet(complement(X10),X11)))]. % 162.73/163.19 [659=demod(649),[], % 162.73/163.19 complement(meet(complement(X10),meet(X10,X11))) = top]. % 162.73/163.19 [665=param(608,17),[], % 162.73/163.19 join(complement(X11),X10) = complement(meet(complement(X10),X11))]. % 162.73/163.19 [703=demod(633),[665], % 162.73/163.19 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = join(X12,X11)]. % 162.73/163.19 [721=param(608,23),[], % 162.73/163.19 converse(join(X10,converse(complement(X11)))) = complement(meet(complement(converse(X10)),X11))]. % 162.73/163.19 [724=param(608,181),[], % 162.73/163.19 join(X10,X11) = complement(meet(complement(X10),complement(X11)))]. % 162.73/163.19 [725=demod(18),[724], % 162.73/163.19 complement(meet(complement(composition(meet(X10,composition(X11,converse(X12))),meet(X12,composition(converse(X10),X11)))),complement(meet(composition(X10,X12),X11)))) = composition(meet(X10,composition(X11,converse(X12))),meet(X12,composition(converse(X10),X11)))]. % 162.73/163.19 [729=demod(486),[724], % 162.73/163.19 complement(meet(complement(X10),complement(meet(X11,X10)))) = X10]. % 162.73/163.19 [735=demod(57),[724], % 162.73/163.19 complement(meet(complement(meet(composition(X10,X11),X12)),complement(meet(X12,composition(X10,meet(X11,composition(converse(X10),X12))))))) = meet(X12,composition(X10,meet(X11,composition(converse(X10),X12))))]. % 162.73/163.19 [748=demod(703),[724], % 162.73/163.19 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = complement(meet(complement(X12),complement(X11)))]. % 162.73/163.19 [770=demod(485),[724], % 162.73/163.19 complement(meet(complement(X10),complement(composition(meet(one,X11),X10)))) = X10]. % 162.73/163.19 [806=demod(308),[724], % 162.73/163.19 complement(meet(complement(X10),complement(converse(complement(converse(X10)))))) = top]. % 162.73/163.19 [809=demod(721),[724], % 162.73/163.19 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),complement(converse(complement(X11))))))]. % 162.73/163.19 [951=param(5,659),[56,182], % 162.73/163.19 meet(complement(X10),meet(X10,X11)) = zero]. % 162.73/163.19 [953=param(951,181),[], % 162.73/163.19 meet(X10,meet(complement(X10),X11)) = zero]. % 162.73/163.19 [1003=param(181,729),[], % 162.73/163.19 meet(complement(X10),complement(meet(X11,X10))) = complement(X10)]. % 162.73/163.19 [1006=param(1003,56),[], % 162.73/163.19 meet(complement(X10),complement(meet(X10,X11))) = complement(X10)]. % 162.73/163.19 [1056=param(5,806),[56,182], % 162.73/163.19 meet(complement(X10),complement(converse(complement(converse(X10))))) = zero]. % 162.73/163.19 [1059=param(1056,10),[], % 162.73/163.19 meet(complement(converse(X10)),complement(converse(complement(X10)))) = zero]. % 162.73/163.19 [1068=param(5,648),[56,182], % 162.73/163.19 meet(complement(X10),meet(complement(X11),meet(X12,X10))) = zero]. % 162.73/163.19 [1072=param(1068,181),[], % 162.73/163.19 meet(complement(X10),meet(X11,meet(X12,X10))) = zero]. % 162.73/163.19 [1074=param(654,56),[], % 162.73/163.19 complement(meet(meet(X10,X11),complement(X12))) = complement(meet(X11,meet(complement(X12),X10)))]. % 162.73/163.19 [1127=param(1072,56),[], % 162.73/163.19 meet(complement(X10),meet(X11,meet(X10,X12))) = zero]. % 162.73/163.19 [1141=param(1072,1006),[181], % 162.73/163.19 meet(meet(X10,X11),meet(X12,complement(X10))) = zero]. % 162.73/163.19 [1144=param(1141,351),[56], % 162.73/163.19 meet(sk1,meet(converse(composition(converse(sk3),sk2)),X10)) = zero]. % 162.73/163.19 [1368=param(748,1006),[181,56,181], % 162.73/163.19 complement(meet(X10,complement(meet(X10,X11)))) = complement(meet(X10,complement(X11)))]. % 162.73/163.19 [1372=param(181,1368),[181], % 162.73/163.19 meet(X10,complement(meet(X10,X11))) = meet(X10,complement(X11))]. % 162.73/163.19 [1373=param(1372,56),[], % 162.73/163.19 meet(X10,complement(meet(X11,X10))) = meet(X10,complement(X11))]. % 162.73/163.19 [1376=param(1372,1056),[204,56,182,181], % 162.73/163.19 meet(complement(X10),converse(complement(converse(X10)))) = complement(X10)]. % 162.73/163.19 [1420=param(1003,1376),[181,56], % 162.73/163.19 meet(X10,complement(converse(complement(converse(X10))))) = complement(converse(complement(converse(X10))))]. % 162.73/163.19 [1424=param(1373,1059),[204,56,182,181,56], % 162.73/163.19 meet(converse(X10),complement(converse(complement(X10)))) = complement(converse(complement(X10)))]. % 162.73/163.19 [1425=param(1373,1072),[204,56,182,181,56], % 162.73/163.19 meet(X12,meet(X10,meet(X11,X12))) = meet(X10,meet(X11,X12))]. % 162.73/163.19 [1429=param(1373,1127),[204,56,182,181,56], % 162.73/163.19 meet(X11,meet(X10,meet(X11,X12))) = meet(X10,meet(X11,X12))]. % 162.73/163.19 [1441=param(1144,1424),[], % 162.73/163.19 meet(sk1,complement(converse(complement(composition(converse(sk3),sk2))))) = zero]. % 162.73/163.19 [1444=param(1372,1441),[204,194,181], % 162.73/163.19 meet(sk1,converse(complement(composition(converse(sk3),sk2)))) = sk1]. % 162.73/163.19 [1466=param(1429,56),[1425], % 162.73/163.19 meet(X10,meet(X11,X12)) = meet(X10,meet(X12,X11))]. % 162.73/163.19 [1607=param(1466,56),[], % 162.73/163.19 meet(X10,meet(X11,X12)) = meet(meet(X12,X11),X10)]. % 162.73/163.19 [1678=param(181,770),[], % 162.73/163.19 meet(complement(X10),complement(composition(meet(one,X11),X10))) = complement(X10)]. % 162.73/163.19 [1683=param(1003,1678),[181,181,56,181], % 162.73/163.19 meet(X10,composition(meet(one,X11),X10)) = composition(meet(one,X11),X10)]. % 162.73/163.19 [1703=param(1683,579),[579], % 162.73/163.19 meet(X10,composition(meet(X11,one),X10)) = composition(meet(X11,one),X10)]. % 162.73/163.19 [1723=param(953,1703),[], % 162.73/163.19 meet(X10,composition(meet(X11,one),complement(X10))) = zero]. % 162.73/163.19 [2046=param(809,306),[181,181,10,1420,181,10], % 162.73/163.19 complement(converse(complement(X10))) = converse(X10)]. % 162.73/163.19 [2069=demod(809),[2046], % 162.73/163.19 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 162.73/163.19 [2077=param(2046,181),[], % 162.73/163.19 complement(converse(X10)) = converse(complement(X10))]. % 162.73/163.19 [2078=demod(2069),[2077], % 162.73/163.19 complement(meet(converse(complement(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 162.73/163.19 [2440=param(2078,181),[181], % 162.73/163.19 complement(meet(converse(X10),X11)) = converse(complement(meet(X10,converse(X11))))]. % 162.73/163.19 [2447=param(181,2440),[2077,181], % 162.73/163.19 meet(converse(X10),X11) = converse(meet(X10,converse(X11)))]. % 162.73/163.19 [2537=param(2447,38),[], % 162.73/163.19 converse(meet(one,converse(X10))) = meet(one,X10)]. % 162.73/163.19 [2591=param(1723,2447),[38], % 162.73/163.19 meet(X10,composition(converse(meet(X11,one)),complement(X10))) = zero]. % 162.73/163.19 [2605=param(2537,10),[], % 162.73/163.19 meet(one,converse(X10)) = converse(meet(one,X10))]. % 162.73/163.19 [2635=param(1683,2605),[2605], % 162.73/163.19 meet(X10,composition(converse(meet(one,X11)),X10)) = composition(converse(meet(one,X11)),X10)]. % 162.73/163.19 [2778=param(2591,56),[], % 162.73/163.19 meet(X10,composition(converse(meet(one,X11)),complement(X10))) = zero]. % 162.73/163.19 [2834=param(2778,28),[10], % 162.73/163.19 meet(X10,converse(composition(converse(complement(X10)),meet(one,X11)))) = zero]. % 162.73/163.19 [3123=param(2834,2447),[2077,10,10], % 162.73/163.19 converse(meet(X10,composition(complement(X10),meet(one,X11)))) = zero]. % 162.73/163.19 [3127=param(10,3123),[223], % 162.73/163.19 meet(X10,composition(complement(X10),meet(one,X11))) = zero]. % 162.73/163.19 [3132=param(3127,181),[], % 162.73/163.19 meet(complement(X10),composition(X10,meet(one,X11))) = zero]. % 162.73/163.21 [3139=param(1372,3127),[204,194], % 162.73/163.21 meet(X10,complement(composition(complement(X10),meet(one,X11)))) = X10]. % 162.73/163.21 [3152=param(1372,3132),[204,56,182], % 162.73/163.21 meet(complement(X10),complement(composition(X10,meet(one,X11)))) = complement(X10)]. % 162.73/163.21 [3153=param(1373,3132),[204,56,182,181,56], % 162.73/163.21 meet(X10,composition(X10,meet(one,X11))) = composition(X10,meet(one,X11))]. % 162.73/163.21 [3302=param(1072,3139),[181], % 162.73/163.21 meet(composition(complement(X10),meet(one,X11)),meet(X12,X10)) = zero]. % 162.73/163.21 [3397=param(3302,1444),[2077,181,46,10,56], % 162.73/163.21 meet(sk1,composition(converse(sk2),composition(sk3,meet(one,X10)))) = zero]. % 162.73/163.21 [3858=param(1074,56),[], % 162.73/163.21 complement(meet(meet(X11,X10),complement(X12))) = complement(meet(X10,meet(X11,complement(X12))))]. % 162.73/163.21 [3859=param(3858,181),[181], % 162.73/163.21 complement(meet(meet(X10,X11),X12)) = complement(meet(X11,meet(X10,X12)))]. % 162.73/163.21 [3868=param(181,3859),[181], % 162.73/163.21 meet(meet(X11,X10),X12) = meet(X10,meet(X11,X12))]. % 162.73/163.21 [3974=demod(1607),[3868], % 162.73/163.21 meet(X10,meet(X11,X12)) = meet(X11,meet(X12,X10))]. % 162.73/163.21 [8331=param(735,3153),[12,183,3152,181,3153], % 162.73/163.21 composition(X10,meet(one,composition(converse(X10),X10))) = X10]. % 162.73/163.21 [12553=param(1683,8331),[56,3868,517,8331], % 162.73/163.21 meet(X10,meet(one,composition(converse(meet(one,X10)),meet(one,X10)))) = meet(one,X10)]. % 162.73/163.21 [27722=param(2635,3868),[], % 162.73/163.21 meet(X12,meet(X11,composition(converse(meet(one,X10)),meet(X11,X12)))) = composition(converse(meet(one,X10)),meet(X11,X12))]. % 162.73/163.21 [27723=demod(12553),[27722], % 162.73/163.21 composition(converse(meet(one,X10)),meet(one,X10)) = meet(one,X10)]. % 162.73/163.21 [27752=param(8,27723),[10,27723], % 162.73/163.21 converse(meet(one,X10)) = meet(one,X10)]. % 162.73/163.21 [38039=param(725,3397),[34,-281,27752,10,375,204,182,181,34,-281,27752,10,3397,375], % 162.73/163.21 meet(composition(sk2,sk1),composition(sk3,meet(one,X10))) = zero]. % 162.73/163.21 [38054=param(3974,38039),[340], % 162.73/163.21 meet(composition(sk3,meet(one,X10)),meet(X11,composition(sk2,sk1))) = zero]. % 162.73/163.21 [59415=param(38054,183),[12], % 162.73/163.21 meet(sk3,meet(X10,composition(sk2,sk1))) = zero]. % 162.73/163.21 [59438=param(59415,182),[], % 162.73/163.21 meet(sk3,composition(sk2,sk1)) = zero]. % 162.73/163.21 [60250=param(21,28),[-8,10,56,59438,20], % 162.73/163.21 thmtrue = thmfalse]. % 162.73/163.21 % SZS output end CNFRefutation % 162.73/163.21 Space: 563032 KB %------------------------------------------------------------------------------