%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : REL027-3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 19:23:33 EDT 2022 % Result : Unsatisfiable 10.07s 10.47s % Output : CNFRefutation 10.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : REL027-3 : TPTP v8.1.0. Released v4.0.0. % 0.08/0.13 % Command : fiesta-wrapper %s % 0.12/0.34 % Computer : n025.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 : 600 % 0.12/0.34 % DateTime : Fri Jul 8 08:04:14 EDT 2022 % 0.12/0.34 % CPUTime : % 10.07/10.47 Theorem Proved. % 10.07/10.47 % SZS status Unsatisfiable % 10.07/10.47 % SZS output start CNFRefutation % 10.07/10.47 [1=axiom,[], % 10.07/10.47 join(sk1,one) = one]. % 10.07/10.47 [3=axiom,[], % 10.07/10.47 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)]. % 10.07/10.47 [5=axiom,[], % 10.07/10.47 meet(X10,complement(X10)) = zero]. % 10.07/10.47 [6=axiom,[], % 10.07/10.47 join(X10,complement(X10)) = top]. % 10.07/10.47 [7=axiom,[], % 10.07/10.47 join(composition(converse(X10),complement(composition(X10,X11))),complement(X11)) = complement(X11)]. % 10.07/10.47 [8=axiom,[], % 10.07/10.47 converse(composition(X10,X11)) = composition(converse(X11),converse(X10))]. % 10.07/10.47 [9=axiom,[], % 10.07/10.47 join(converse(X10),converse(X11)) = converse(join(X10,X11))]. % 10.07/10.47 [10=axiom,[], % 10.07/10.47 converse(converse(X10)) = X10]. % 10.07/10.47 [11=axiom,[], % 10.07/10.47 join(composition(X10,X12),composition(X11,X12)) = composition(join(X10,X11),X12)]. % 10.07/10.47 [12=axiom,[], % 10.07/10.47 composition(X10,one) = X10]. % 10.07/10.47 [13=axiom,[], % 10.07/10.47 composition(composition(X10,X11),X12) = composition(X10,composition(X11,X12))]. % 10.07/10.47 [14=axiom,[], % 10.07/10.47 complement(join(complement(X10),complement(X11))) = meet(X10,X11)]. % 10.07/10.47 [15=axiom,[14], % 10.07/10.47 join(meet(X10,X11),complement(join(complement(X10),X11))) = X10]. % 10.07/10.47 [16=axiom,[], % 10.07/10.47 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 10.07/10.47 [17=axiom,[], % 10.07/10.47 join(X10,X11) = join(X11,X10)]. % 10.07/10.47 [19=demod(7),[17], % 10.07/10.47 join(complement(X10),composition(converse(X11),complement(composition(X11,X10)))) = complement(X10)]. % 10.07/10.47 [20=axiom,[], % 10.07/10.47 thtop(X10,X10) = thmfalse]. % 10.07/10.47 [21=axiom,[], % 10.07/10.47 thtop(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) = thmtrue]. % 10.07/10.47 [23=param(9,10),[], % 10.07/10.47 join(converse(X10),X11) = converse(join(X10,converse(X11)))]. % 10.07/10.47 [25=param(10,8),[], % 10.07/10.47 converse(composition(converse(X10),converse(X11))) = composition(X11,X10)]. % 10.07/10.47 [27=param(8,12),[], % 10.07/10.47 composition(converse(one),converse(X10)) = converse(X10)]. % 10.07/10.47 [28=param(8,10),[], % 10.07/10.47 composition(X10,converse(X11)) = converse(composition(X11,converse(X10)))]. % 10.07/10.47 [29=param(8,10),[], % 10.07/10.47 composition(converse(X10),X11) = converse(composition(converse(X11),X10))]. % 10.07/10.47 [31=param(27,10),[10], % 10.07/10.47 composition(converse(one),X10) = X10]. % 10.07/10.47 [32=param(31,12),[], % 10.07/10.47 converse(one) = one]. % 10.07/10.47 [33=demod(31),[32], % 10.07/10.47 composition(one,X10) = X10]. % 10.07/10.47 [35=param(11,33),[], % 10.07/10.47 join(X10,composition(X11,X10)) = composition(join(one,X11),X10)]. % 10.07/10.47 [36=param(11,33),[17], % 10.07/10.47 join(X10,composition(X11,X10)) = composition(join(X11,one),X10)]. % 10.07/10.47 [39=param(23,6),[], % 10.07/10.47 converse(join(X10,converse(complement(converse(X10))))) = top]. % 10.07/10.47 [41=param(23,17),[], % 10.07/10.47 converse(join(X10,converse(X11))) = join(X11,converse(X10))]. % 10.07/10.47 [42=param(23,32),[], % 10.07/10.47 converse(join(one,converse(X10))) = join(one,X10)]. % 10.07/10.47 [46=param(42,10),[], % 10.07/10.47 join(one,converse(X10)) = converse(join(one,X10))]. % 10.07/10.47 [48=param(14,6),[5], % 10.07/10.47 complement(top) = zero]. % 10.07/10.47 [49=param(6,14),[16], % 10.07/10.47 join(complement(X10),join(complement(X11),meet(X10,X11))) = top]. % 10.07/10.47 [50=param(14,14),[], % 10.07/10.47 complement(join(meet(X10,X11),complement(X12))) = meet(join(complement(X10),complement(X11)),X12)]. % 10.07/10.47 [51=param(14,14),[], % 10.07/10.47 complement(join(complement(X10),meet(X11,X12))) = meet(X10,join(complement(X11),complement(X12)))]. % 10.07/10.47 [52=param(14,17),[14], % 10.07/10.47 meet(X10,X11) = meet(X11,X10)]. % 10.07/10.47 [53=demod(3),[52,52], % 10.07/10.47 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))))]. % 10.07/10.47 [58=param(14,48),[], % 10.07/10.47 complement(join(zero,complement(X10))) = meet(top,X10)]. % 10.07/10.47 [59=param(15,5),[14], % 10.07/10.47 join(zero,meet(X10,X10)) = X10]. % 10.07/10.47 [60=param(15,6),[48,17], % 10.07/10.47 join(zero,meet(X10,complement(complement(X10)))) = X10]. % 10.07/10.47 [62=param(15,17),[], % 10.07/10.47 join(meet(X10,X11),complement(join(X11,complement(X10)))) = X10]. % 10.07/10.47 [65=param(16,1),[], % 10.07/10.47 join(sk1,join(one,X10)) = join(one,X10)]. % 10.07/10.47 [68=param(16,15),[], % 10.07/10.47 join(meet(X10,X12),join(complement(join(complement(X10),X12)),X11)) = join(X10,X11)]. % 10.07/10.47 [69=param(16,17),[], % 10.07/10.47 join(X10,join(X11,X12)) = join(X12,join(X10,X11))]. % 10.07/10.47 [70=param(16,17),[16], % 10.07/10.47 join(X10,join(X11,X12)) = join(X11,join(X10,X12))]. % 10.07/10.47 [73=param(15,52),[], % 10.07/10.47 join(meet(X10,X11),complement(join(complement(X11),X10))) = X11]. % 10.07/10.47 [74=param(21,52),[52], % 10.07/10.47 thtop(meet(one,complement(composition(sk1,top))),meet(one,complement(sk1))) = thmtrue]. % 10.07/10.47 [86=param(19,8),[10], % 10.07/10.47 join(complement(converse(X10)),composition(X11,complement(converse(composition(X10,X11))))) = complement(converse(X10))]. % 10.07/10.47 [87=param(19,10),[], % 10.07/10.47 join(complement(X10),composition(X11,complement(composition(converse(X11),X10)))) = complement(X10)]. % 10.07/10.47 [90=param(19,32),[33,33], % 10.07/10.47 join(complement(X10),complement(X10)) = complement(X10)]. % 10.07/10.47 [91=param(19,48),[48], % 10.07/10.47 join(zero,composition(converse(X10),complement(composition(X10,top)))) = zero]. % 10.07/10.47 [93=param(14,90),[], % 10.07/10.47 meet(X10,X10) = complement(complement(X10))]. % 10.07/10.47 [95=demod(59),[93], % 10.07/10.47 join(zero,complement(complement(X10))) = X10]. % 10.07/10.47 [97=param(90,48),[48,48], % 10.07/10.47 join(zero,zero) = zero]. % 10.07/10.47 [98=param(16,97),[], % 10.07/10.47 join(zero,join(zero,X10)) = join(zero,X10)]. % 10.07/10.47 [103=param(95,14),[], % 10.07/10.47 join(complement(X10),complement(X11)) = join(zero,complement(meet(X10,X11)))]. % 10.07/10.47 [105=demod(50),[103], % 10.07/10.47 complement(join(meet(X10,X11),complement(X12))) = meet(join(zero,complement(meet(X10,X11))),X12)]. % 10.07/10.47 [107=demod(51),[103], % 10.07/10.47 complement(join(complement(X10),meet(X11,X12))) = meet(X10,join(zero,complement(meet(X11,X12))))]. % 10.07/10.47 [122=param(98,17),[16], % 10.07/10.47 join(zero,join(X10,zero)) = join(zero,X10)]. % 10.07/10.47 [123=param(98,95),[95], % 10.07/10.47 join(zero,X10) = X10]. % 10.07/10.47 [124=demod(60),[123], % 10.07/10.47 meet(X10,complement(complement(X10))) = X10]. % 10.07/10.47 [125=demod(58),[123], % 10.07/10.47 meet(top,X10) = complement(complement(X10))]. % 10.07/10.47 [130=demod(95),[123], % 10.07/10.47 complement(complement(X10)) = X10]. % 10.07/10.47 [131=demod(125),[130], % 10.07/10.47 meet(top,X10) = X10]. % 10.07/10.47 [132=demod(124),[130], % 10.07/10.47 meet(X10,X10) = X10]. % 10.07/10.47 [134=demod(105),[123], % 10.07/10.47 complement(join(meet(X10,X11),complement(X12))) = meet(complement(meet(X10,X11)),X12)]. % 10.07/10.47 [135=demod(103),[123], % 10.07/10.47 join(complement(X10),complement(X11)) = complement(meet(X10,X11))]. % 10.07/10.47 [136=demod(107),[123], % 10.07/10.47 complement(join(complement(X10),meet(X11,X12))) = meet(X10,complement(meet(X11,X12)))]. % 10.07/10.47 [137=demod(91),[123], % 10.07/10.47 composition(converse(X10),complement(composition(X10,top))) = zero]. % 10.07/10.47 [138=demod(122),[123,123], % 10.07/10.47 join(X10,zero) = X10]. % 10.07/10.47 [143=param(138,23),[], % 10.07/10.47 converse(join(X10,converse(zero))) = converse(X10)]. % 10.07/10.47 [175=param(130,48),[], % 10.07/10.47 complement(zero) = top]. % 10.07/10.47 [189=param(36,1),[33], % 10.07/10.47 join(X10,composition(sk1,X10)) = X10]. % 10.07/10.47 [193=param(36,23),[32], % 10.07/10.47 composition(converse(join(X10,one)),X11) = join(X11,composition(converse(X10),X11))]. % 10.07/10.47 [207=param(189,28),[23,10], % 10.07/10.47 converse(join(X10,composition(X10,converse(sk1)))) = converse(X10)]. % 10.07/10.47 [223=param(10,39),[], % 10.07/10.47 join(X10,converse(complement(converse(X10)))) = converse(top)]. % 10.07/10.47 [242=param(10,143),[10], % 10.07/10.47 join(X10,converse(zero)) = X10]. % 10.07/10.47 [263=param(242,123),[], % 10.07/10.47 converse(zero) = zero]. % 10.07/10.47 [286=param(49,132),[17,6,17], % 10.07/10.47 join(top,complement(X10)) = top]. % 10.07/10.47 [291=param(286,130),[], % 10.07/10.47 join(top,X10) = top]. % 10.07/10.47 [296=param(291,17),[], % 10.07/10.47 join(X10,top) = top]. % 10.07/10.47 [298=param(36,291),[], % 10.07/10.47 join(X10,composition(top,X10)) = composition(top,X10)]. % 10.07/10.47 [299=param(41,291),[], % 10.07/10.47 join(X10,converse(top)) = converse(top)]. % 10.07/10.47 [302=param(299,291),[], % 10.07/10.47 converse(top) = top]. % 10.07/10.47 [304=demod(223),[302], % 10.07/10.47 join(X10,converse(complement(converse(X10)))) = top]. % 10.07/10.47 [313=param(25,302),[], % 10.07/10.47 converse(composition(top,converse(X10))) = composition(X10,top)]. % 10.07/10.47 [318=param(15,304),[48,17,123], % 10.07/10.47 meet(X10,converse(complement(converse(complement(X10))))) = X10]. % 10.07/10.47 [324=param(35,304),[32], % 10.07/10.47 join(X10,composition(converse(complement(one)),X10)) = composition(top,X10)]. % 10.07/10.47 [336=param(298,291),[], % 10.07/10.47 composition(top,top) = top]. % 10.07/10.47 [337=param(13,336),[], % 10.07/10.47 composition(top,composition(top,X10)) = composition(top,X10)]. % 10.07/10.47 [389=param(70,6),[296], % 10.07/10.47 join(X10,join(X11,complement(X10))) = top]. % 10.07/10.47 [393=param(70,36),[], % 10.07/10.47 join(X10,composition(join(X11,one),X12)) = join(X12,join(X10,composition(X11,X12)))]. % 10.07/10.47 [398=param(70,65),[], % 10.07/10.47 join(one,join(sk1,X10)) = join(one,X10)]. % 10.07/10.47 [415=param(398,304),[17,291,46], % 10.07/10.47 converse(join(one,complement(converse(sk1)))) = top]. % 10.07/10.47 [420=param(73,5),[130,123], % 10.07/10.47 complement(join(X10,X10)) = complement(X10)]. % 10.07/10.47 [426=param(70,73),[], % 10.07/10.47 join(meet(X12,X11),join(X10,complement(join(complement(X11),X12)))) = join(X10,X11)]. % 10.07/10.47 [442=param(130,420),[130], % 10.07/10.47 join(X10,X10) = X10]. % 10.07/10.47 [451=param(69,442),[], % 10.07/10.47 join(X11,join(X10,X11)) = join(X10,X11)]. % 10.07/10.47 [478=param(451,68),[17,15], % 10.07/10.47 join(X10,meet(X10,X11)) = X10]. % 10.07/10.47 [484=param(478,52),[], % 10.07/10.47 join(X10,meet(X11,X10)) = X10]. % 10.07/10.47 [487=param(398,478),[17,1], % 10.07/10.47 join(one,meet(sk1,X10)) = one]. % 10.07/10.47 [541=param(10,415),[302], % 10.07/10.47 join(one,complement(converse(sk1))) = top]. % 10.07/10.47 [546=param(62,541),[52,48,17,123], % 10.07/10.47 meet(one,converse(sk1)) = converse(sk1)]. % 10.07/10.47 [558=param(389,68),[], % 10.07/10.47 join(X10,complement(meet(X10,X11))) = top]. % 10.07/10.47 [559=param(389,69),[], % 10.07/10.47 join(complement(X10),join(X10,X11)) = top]. % 10.07/10.47 [563=param(559,11),[], % 10.07/10.47 join(complement(composition(X10,X11)),composition(join(X10,X12),X11)) = top]. % 10.07/10.47 [575=param(559,73),[17], % 10.07/10.47 join(X10,complement(meet(X11,X10))) = top]. % 10.07/10.47 [601=param(70,575),[296], % 10.07/10.47 join(X10,join(X11,complement(meet(X12,X10)))) = top]. % 10.07/10.47 [619=param(62,558),[52,48,17,123], % 10.07/10.47 meet(X10,meet(X10,X11)) = meet(X10,X11)]. % 10.07/10.47 [655=param(19,337),[302,35,17,291], % 10.07/10.47 composition(top,complement(composition(top,X10))) = complement(composition(top,X10))]. % 10.07/10.47 [664=param(134,73),[], % 10.07/10.47 meet(complement(meet(X11,X10)),join(complement(X10),X11)) = complement(X10)]. % 10.07/10.47 [671=param(69,135),[], % 10.07/10.47 join(X10,complement(meet(X11,X12))) = join(complement(X12),join(X10,complement(X11)))]. % 10.07/10.47 [672=param(70,135),[], % 10.07/10.47 join(X10,complement(meet(X11,X12))) = join(complement(X11),join(X10,complement(X12)))]. % 10.07/10.47 [674=param(135,130),[], % 10.07/10.47 join(X10,complement(X11)) = complement(meet(complement(X10),X11))]. % 10.07/10.47 [700=demod(426),[674,674], % 10.07/10.47 complement(meet(complement(meet(X10,X11)),meet(complement(X12),join(complement(X11),X10)))) = join(X12,X11)]. % 10.07/10.47 [718=demod(601),[674,674], % 10.07/10.47 complement(meet(complement(X10),meet(complement(X11),meet(X12,X10)))) = top]. % 10.07/10.47 [723=demod(558),[674], % 10.07/10.47 complement(meet(complement(X10),meet(X10,X11))) = top]. % 10.07/10.47 [729=demod(671),[674,674,674,130], % 10.07/10.47 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X12,meet(complement(X10),X11)))]. % 10.07/10.47 [733=demod(672),[674,674,674,130], % 10.07/10.47 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X11,meet(complement(X10),X12)))]. % 10.07/10.47 [736=demod(723),[], % 10.07/10.47 complement(meet(complement(X10),meet(X10,X11))) = top]. % 10.07/10.47 [741=param(136,52),[136], % 10.07/10.47 meet(X10,complement(meet(X11,X12))) = meet(X10,complement(meet(X12,X11)))]. % 10.07/10.47 [752=param(86,137),[10,263,175,-313,10], % 10.07/10.47 join(complement(X10),converse(composition(top,converse(complement(composition(X10,top)))))) = complement(X10)]. % 10.07/10.47 [756=param(674,17),[], % 10.07/10.47 join(complement(X11),X10) = complement(meet(complement(X10),X11))]. % 10.07/10.47 [764=demod(664),[756], % 10.07/10.47 meet(complement(meet(X10,X11)),complement(meet(complement(X10),X11))) = complement(X11)]. % 10.07/10.47 [771=demod(87),[756,52], % 10.07/10.47 complement(meet(X10,complement(composition(X11,complement(composition(converse(X11),X10)))))) = complement(X10)]. % 10.07/10.47 [772=demod(19),[756,52], % 10.07/10.47 complement(meet(X10,complement(composition(converse(X11),complement(composition(X11,X10)))))) = complement(X10)]. % 10.07/10.47 [777=demod(563),[756,52], % 10.07/10.47 complement(meet(composition(X10,X11),complement(composition(join(X10,X12),X11)))) = top]. % 10.07/10.47 [802=demod(752),[756,52], % 10.07/10.47 complement(meet(X10,complement(converse(composition(top,converse(complement(composition(X10,top)))))))) = complement(X10)]. % 10.07/10.47 [804=demod(700),[756], % 10.07/10.47 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = join(X12,X11)]. % 10.07/10.47 [822=param(674,23),[], % 10.07/10.47 converse(join(X10,converse(complement(X11)))) = complement(meet(complement(converse(X10)),X11))]. % 10.07/10.47 [825=param(65,674),[674,674], % 10.07/10.47 complement(meet(complement(sk1),meet(complement(one),X10))) = complement(meet(complement(one),X10))]. % 10.07/10.47 [827=param(674,130),[], % 10.07/10.47 join(X10,X11) = complement(meet(complement(X10),complement(X11)))]. % 10.07/10.47 [828=demod(1),[827], % 10.07/10.47 complement(meet(complement(sk1),complement(one))) = one]. % 10.07/10.47 [844=demod(53),[827], % 10.07/10.47 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))))]. % 10.07/10.47 [852=demod(484),[827], % 10.07/10.47 complement(meet(complement(X10),complement(meet(X11,X10)))) = X10]. % 10.07/10.47 [855=demod(487),[827], % 10.07/10.47 complement(meet(complement(one),complement(meet(sk1,X10)))) = one]. % 10.07/10.47 [867=demod(804),[827], % 10.07/10.47 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = complement(meet(complement(X12),complement(X11)))]. % 10.07/10.47 [876=demod(35),[827,827], % 10.07/10.47 complement(meet(complement(X10),complement(composition(X11,X10)))) = composition(complement(meet(complement(one),complement(X11))),X10)]. % 10.07/10.47 [883=demod(193),[827,827], % 10.07/10.47 composition(converse(complement(meet(complement(X10),complement(one)))),X11) = complement(meet(complement(X11),complement(composition(converse(X10),X11))))]. % 10.07/10.47 [886=demod(324),[827], % 10.07/10.47 complement(meet(complement(X10),complement(composition(converse(complement(one)),X10)))) = composition(top,X10)]. % 10.07/10.47 [890=demod(207),[827], % 10.07/10.47 converse(complement(meet(complement(X10),complement(composition(X10,converse(sk1)))))) = converse(X10)]. % 10.07/10.47 [896=demod(189),[827], % 10.07/10.47 complement(meet(complement(X10),complement(composition(sk1,X10)))) = X10]. % 10.07/10.47 [916=demod(777),[827], % 10.07/10.47 complement(meet(composition(X10,X11),complement(composition(complement(meet(complement(X10),complement(X12))),X11)))) = top]. % 10.07/10.47 [950=demod(304),[827], % 10.07/10.47 complement(meet(complement(X10),complement(converse(complement(converse(X10)))))) = top]. % 10.07/10.47 [953=demod(822),[827], % 10.07/10.47 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),complement(converse(complement(X11))))))]. % 10.07/10.47 [1076=demod(393),[827,827,827,827,130], % 10.07/10.47 complement(meet(complement(X10),complement(composition(complement(meet(complement(X11),complement(one))),X12)))) = complement(meet(complement(X12),meet(complement(X10),complement(composition(X11,X12)))))]. % 10.07/10.47 [1101=param(130,828),[], % 10.07/10.47 meet(complement(sk1),complement(one)) = complement(one)]. % 10.07/10.47 [1119=param(5,736),[52,131], % 10.07/10.47 meet(complement(X10),meet(X10,X11)) = zero]. % 10.07/10.47 [1121=param(1119,130),[], % 10.07/10.47 meet(X10,meet(complement(X10),X11)) = zero]. % 10.07/10.47 [1138=param(655,28),[302], % 10.07/10.47 composition(top,complement(converse(composition(X10,top)))) = complement(composition(top,converse(X10)))]. % 10.07/10.47 [1159=param(130,896),[], % 10.07/10.47 meet(complement(X10),complement(composition(sk1,X10))) = complement(X10)]. % 10.07/10.47 [1179=param(130,855),[], % 10.07/10.47 meet(complement(one),complement(meet(sk1,X10))) = complement(one)]. % 10.07/10.47 [1181=param(130,852),[], % 10.07/10.47 meet(complement(X10),complement(meet(X11,X10))) = complement(X10)]. % 10.07/10.47 [1187=param(1181,52),[], % 10.07/10.47 meet(complement(X10),complement(meet(X10,X11))) = complement(X10)]. % 10.07/10.47 [1191=param(1181,1159),[130,130,52,130], % 10.07/10.47 meet(X10,composition(sk1,X10)) = composition(sk1,X10)]. % 10.07/10.47 [1199=param(1187,546),[], % 10.07/10.47 meet(complement(one),complement(converse(sk1))) = complement(one)]. % 10.07/10.47 [1209=param(5,718),[52,131], % 10.07/10.47 meet(complement(X10),meet(complement(X11),meet(X12,X10))) = zero]. % 10.07/10.47 [1213=param(1209,130),[], % 10.07/10.47 meet(complement(X10),meet(X11,meet(X12,X10))) = zero]. % 10.07/10.47 [1225=param(1213,1159),[130], % 10.07/10.47 meet(composition(sk1,X10),meet(X11,complement(X10))) = zero]. % 10.07/10.47 [1230=param(1213,1187),[130], % 10.07/10.47 meet(meet(X10,X11),meet(X12,complement(X10))) = zero]. % 10.07/10.47 [1238=param(1230,52),[], % 10.07/10.47 meet(meet(X10,X11),meet(complement(X10),X12)) = zero]. % 10.07/10.47 [1253=param(130,729),[130], % 10.07/10.47 meet(X10,meet(complement(X11),X12)) = meet(complement(X11),meet(X12,X10))]. % 10.07/10.47 [1294=param(130,733),[130], % 10.07/10.47 meet(X10,meet(complement(X11),X12)) = meet(complement(X11),meet(X10,X12))]. % 10.07/10.47 [1295=demod(1238),[], % 10.07/10.47 meet(meet(X10,X11),meet(complement(X10),X12)) = zero]. % 10.07/10.47 [1328=param(1295,52),[], % 10.07/10.47 meet(meet(X10,X11),meet(complement(X11),X12)) = zero]. % 10.07/10.47 [1409=param(764,741),[], % 10.07/10.47 meet(complement(meet(X11,X10)),complement(meet(X10,complement(X11)))) = complement(X10)]. % 10.07/10.47 [1432=param(130,771),[130], % 10.07/10.47 meet(X10,complement(composition(X11,complement(composition(converse(X11),X10))))) = X10]. % 10.07/10.47 [1441=param(130,772),[130], % 10.07/10.47 meet(X10,complement(composition(converse(X11),complement(composition(X11,X10))))) = X10]. % 10.07/10.47 [1499=param(130,802),[130], % 10.07/10.47 meet(X10,complement(converse(composition(top,converse(complement(composition(X10,top))))))) = X10]. % 10.07/10.47 [1540=param(130,825),[130], % 10.07/10.47 meet(complement(sk1),meet(complement(one),X10)) = meet(complement(one),X10)]. % 10.07/10.47 [1629=param(1187,1540),[130,130], % 10.07/10.47 meet(sk1,complement(meet(complement(one),X10))) = sk1]. % 10.07/10.47 [1738=param(867,1187),[130,52,130], % 10.07/10.47 complement(meet(X10,complement(meet(X10,X11)))) = complement(meet(X10,complement(X11)))]. % 10.07/10.47 [1742=param(130,1738),[130], % 10.07/10.47 meet(X10,complement(meet(X10,X11))) = meet(X10,complement(X11))]. % 10.07/10.47 [1743=param(1742,52),[], % 10.07/10.47 meet(X10,complement(meet(X11,X10))) = meet(X10,complement(X11))]. % 10.07/10.47 [1830=param(1743,1225),[175,52,131,52,-1253], % 10.07/10.47 meet(X10,complement(X11)) = meet(complement(X11),meet(complement(composition(sk1,X11)),X10))]. % 10.07/10.47 [1912=param(876,1199),[130,33], % 10.07/10.47 complement(meet(complement(X10),complement(composition(converse(sk1),X10)))) = X10]. % 10.07/10.47 [1917=param(130,1912),[], % 10.07/10.47 meet(complement(X10),complement(composition(converse(sk1),X10))) = complement(X10)]. % 10.07/10.47 [1923=param(1181,1917),[130,130,52,130], % 10.07/10.47 meet(X10,composition(converse(sk1),X10)) = composition(converse(sk1),X10)]. % 10.07/10.47 [1927=param(1328,1917),[130], % 10.07/10.47 meet(complement(X10),meet(composition(converse(sk1),X10),X11)) = zero]. % 10.07/10.47 [1928=param(1742,1917),[130,52,5,130], % 10.07/10.47 meet(complement(X10),composition(converse(sk1),X10)) = zero]. % 10.07/10.47 [1929=param(1928,8),[], % 10.07/10.47 meet(complement(converse(X10)),converse(composition(X10,sk1))) = zero]. % 10.07/10.47 [1946=param(1179,1923),[], % 10.07/10.47 meet(complement(one),complement(composition(converse(sk1),sk1))) = complement(one)]. % 10.07/10.47 [1997=param(1181,1946),[130,130,52,130], % 10.07/10.47 meet(one,composition(converse(sk1),sk1)) = composition(converse(sk1),sk1)]. % 10.07/10.47 [2002=param(1629,883),[29,32,33], % 10.07/10.47 meet(sk1,converse(complement(meet(complement(X10),complement(one))))) = sk1]. % 10.07/10.47 [2011=param(2002,130),[], % 10.07/10.47 meet(sk1,converse(complement(meet(X10,complement(one))))) = sk1]. % 10.07/10.47 [2012=param(2011,52),[], % 10.07/10.47 meet(sk1,converse(complement(meet(complement(one),X10)))) = sk1]. % 10.07/10.47 [2024=param(2012,1923),[], % 10.07/10.47 meet(sk1,converse(complement(composition(converse(sk1),complement(one))))) = sk1]. % 10.07/10.47 [2031=param(886,25),[10], % 10.07/10.47 complement(meet(complement(X10),complement(converse(composition(converse(X10),complement(one)))))) = composition(top,X10)]. % 10.07/10.47 [2072=param(10,890),[10], % 10.07/10.47 complement(meet(complement(X10),complement(composition(X10,converse(sk1))))) = X10]. % 10.07/10.47 [2075=param(130,2072),[], % 10.07/10.47 meet(complement(X10),complement(composition(X10,converse(sk1)))) = complement(X10)]. % 10.07/10.47 [2080=param(1181,2075),[130,130,52,130], % 10.07/10.47 meet(X10,composition(X10,converse(sk1))) = composition(X10,converse(sk1))]. % 10.07/10.47 [2330=param(916,5),[175], % 10.07/10.47 complement(meet(composition(X10,X11),complement(composition(top,X11)))) = top]. % 10.07/10.47 [2332=param(5,2330),[52,131], % 10.07/10.47 meet(composition(X10,X11),complement(composition(top,X11))) = zero]. % 10.07/10.47 [2336=param(2332,52),[], % 10.07/10.47 meet(complement(composition(top,X10)),composition(X11,X10)) = zero]. % 10.07/10.47 [2359=param(2336,2080),[28,302,28], % 10.07/10.47 converse(composition(sk1,converse(complement(converse(composition(sk1,top)))))) = zero]. % 10.07/10.47 [2362=param(10,2359),[263], % 10.07/10.47 composition(sk1,converse(complement(converse(composition(sk1,top))))) = zero]. % 10.07/10.47 [2526=param(1927,1191),[], % 10.07/10.47 meet(complement(X10),composition(sk1,composition(converse(sk1),X10))) = zero]. % 10.07/10.47 [2534=param(1742,2526),[175,52,131], % 10.07/10.47 meet(complement(X10),complement(composition(sk1,composition(converse(sk1),X10)))) = complement(X10)]. % 10.07/10.47 [2535=param(1743,2526),[175,52,131,130,52], % 10.07/10.47 meet(X10,composition(sk1,composition(converse(sk1),X10))) = composition(sk1,composition(converse(sk1),X10))]. % 10.07/10.47 [2579=param(5,950),[52,131], % 10.07/10.47 meet(complement(X10),complement(converse(complement(converse(X10))))) = zero]. % 10.07/10.47 [2588=param(1743,2579),[175,52,131,130,52], % 10.07/10.47 meet(X10,complement(converse(complement(converse(X10))))) = complement(converse(complement(converse(X10))))]. % 10.07/10.47 [2592=param(953,318),[130,130,10,2588,130,10], % 10.07/10.47 complement(converse(complement(X10))) = converse(X10)]. % 10.07/10.47 [2594=demod(953),[2592], % 10.07/10.47 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 10.07/10.47 [2649=param(2592,130),[], % 10.07/10.47 complement(converse(X10)) = converse(complement(X10))]. % 10.07/10.47 [2654=demod(2594),[2649], % 10.07/10.47 complement(meet(converse(complement(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 10.07/10.47 [2674=demod(1929),[2649], % 10.07/10.47 meet(converse(complement(X10)),converse(composition(X10,sk1))) = zero]. % 10.07/10.47 [2710=demod(1499),[2649], % 10.07/10.47 meet(X10,converse(complement(composition(top,converse(complement(composition(X10,top))))))) = X10]. % 10.07/10.47 [2731=demod(1138),[2649], % 10.07/10.47 composition(top,converse(complement(composition(X10,top)))) = complement(composition(top,converse(X10)))]. % 10.07/10.47 [2732=demod(2710),[2731,130], % 10.07/10.47 meet(X10,converse(composition(top,converse(X10)))) = X10]. % 10.07/10.47 [2749=demod(2031),[2649], % 10.07/10.47 complement(meet(complement(X10),converse(complement(composition(converse(X10),complement(one)))))) = composition(top,X10)]. % 10.07/10.47 [2800=demod(2362),[2649,10], % 10.07/10.47 composition(sk1,complement(composition(sk1,top))) = zero]. % 10.07/10.47 [2917=param(2732,8),[10,302], % 10.07/10.47 meet(X10,composition(X10,top)) = X10]. % 10.07/10.47 [2933=param(1181,2917),[52], % 10.07/10.47 meet(complement(X10),complement(composition(X10,top))) = complement(composition(X10,top))]. % 10.07/10.47 [3529=param(2654,130),[130], % 10.07/10.47 complement(meet(converse(X10),X11)) = converse(complement(meet(X10,converse(X11))))]. % 10.07/10.47 [3577=param(130,3529),[2649,130], % 10.07/10.47 meet(converse(X10),X11) = converse(meet(X10,converse(X11)))]. % 10.07/10.47 [3784=demod(2674),[3577,10], % 10.07/10.47 converse(meet(complement(X10),composition(X10,sk1))) = zero]. % 10.07/10.47 [3916=param(10,3784),[263], % 10.07/10.47 meet(complement(X10),composition(X10,sk1)) = zero]. % 10.07/10.47 [3934=param(1743,3916),[175,52,131,130,52], % 10.07/10.47 meet(X10,composition(X10,sk1)) = composition(X10,sk1)]. % 10.07/10.47 [3948=param(1295,3934),[], % 10.07/10.47 meet(composition(X10,sk1),meet(complement(X10),X11)) = zero]. % 10.07/10.47 [3966=param(3934,2336),[-25], % 10.07/10.47 converse(composition(converse(sk1),converse(complement(composition(top,sk1))))) = zero]. % 10.07/10.47 [4101=param(1743,1121),[175,52,131,1830,-1294,619], % 10.07/10.47 meet(complement(X10),meet(complement(composition(sk1,X10)),X11)) = meet(complement(X10),X11)]. % 10.07/10.47 [4403=param(1743,3948),[175,52,131,1830,-1294,-1294,4101], % 10.07/10.47 meet(complement(X10),meet(complement(composition(X10,sk1)),X11)) = meet(complement(X10),X11)]. % 10.07/10.47 [5175=param(10,3966),[263], % 10.07/10.47 composition(converse(sk1),converse(complement(composition(top,sk1)))) = zero]. % 10.07/10.47 [7525=param(1409,2024),[1830,4403,2749,2649,130], % 10.07/10.47 meet(complement(sk1),composition(top,sk1)) = converse(composition(converse(sk1),complement(one)))]. % 10.07/10.47 [7593=param(1432,5175),[175,1830,4101], % 10.07/10.47 meet(complement(composition(sk1,top)),converse(complement(composition(top,sk1)))) = converse(complement(composition(top,sk1)))]. % 10.07/10.47 [7620=param(1441,2800),[175,-313,10,2649,7593], % 10.07/10.47 converse(complement(composition(top,sk1))) = complement(composition(sk1,top))]. % 10.07/10.47 [7633=param(10,7620),[], % 10.07/10.47 complement(composition(top,sk1)) = converse(complement(composition(sk1,top)))]. % 10.07/10.47 [7639=param(130,7633),[2649,130], % 10.07/10.47 composition(top,sk1) = converse(composition(sk1,top))]. % 10.07/10.47 [7646=demod(7525),[7639], % 10.07/10.47 meet(complement(sk1),converse(composition(sk1,top))) = converse(composition(converse(sk1),complement(one)))]. % 10.07/10.47 [8236=param(844,1997),[12,132,2535,2534,130,1997,2535], % 10.07/10.47 composition(sk1,composition(converse(sk1),sk1)) = sk1]. % 10.07/10.47 [8243=param(1191,8236),[52,1923,8236], % 10.07/10.47 composition(converse(sk1),sk1) = sk1]. % 10.07/10.47 [8255=param(8,8243),[10,8243], % 10.07/10.47 converse(sk1) = sk1]. % 10.07/10.47 [8285=demod(7646),[8255], % 10.07/10.47 meet(complement(sk1),converse(composition(sk1,top))) = converse(composition(sk1,complement(one)))]. % 10.07/10.47 [8458=param(2649,8255),[], % 10.07/10.47 converse(complement(sk1)) = complement(sk1)]. % 10.07/10.47 [8492=param(3577,8458),[], % 10.07/10.47 converse(meet(complement(sk1),converse(X10))) = meet(complement(sk1),X10)]. % 10.07/10.47 [8661=param(8492,10),[], % 10.07/10.47 meet(complement(sk1),converse(X10)) = converse(meet(complement(sk1),X10))]. % 10.07/10.47 [8662=demod(8285),[8661], % 10.07/10.47 converse(meet(complement(sk1),composition(sk1,top))) = converse(composition(sk1,complement(one)))]. % 10.07/10.47 [9010=param(10,8662),[10], % 10.07/10.47 meet(complement(sk1),composition(sk1,top)) = composition(sk1,complement(one))]. % 10.07/10.47 [9017=param(1742,9010),[2933], % 10.07/10.47 meet(complement(sk1),complement(composition(sk1,complement(one)))) = complement(composition(sk1,top))]. % 10.07/10.47 [14351=param(1076,9017),[130,1101,130,33,130,52], % 10.07/10.47 complement(meet(one,complement(composition(sk1,top)))) = complement(meet(one,complement(sk1)))]. % 10.07/10.47 [14364=param(130,14351),[130], % 10.07/10.47 meet(one,complement(composition(sk1,top))) = meet(one,complement(sk1))]. % 10.07/10.47 [14365=param(74,14364),[20], % 10.07/10.47 thmtrue = thmfalse]. % 10.07/10.47 % SZS output end CNFRefutation % 10.07/10.47 Space: 55013 KB %------------------------------------------------------------------------------