%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : REL025-1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n009.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:28 EDT 2022 % Result : Unsatisfiable 6.31s 6.75s % Output : CNFRefutation 6.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : REL025-1 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 8 07:22:52 EDT 2022 % 0.12/0.34 % CPUTime : % 6.31/6.75 Theorem Proved. % 6.31/6.75 % SZS status Unsatisfiable % 6.31/6.75 % SZS output start CNFRefutation % 6.31/6.75 [1=axiom,[], % 6.31/6.75 join(sk1,one) = one]. % 6.31/6.75 [2=axiom,[], % 6.31/6.75 meet(X10,complement(X10)) = zero]. % 6.31/6.75 [3=axiom,[], % 6.31/6.75 join(X10,complement(X10)) = top]. % 6.31/6.75 [4=axiom,[], % 6.31/6.75 join(composition(converse(X10),complement(composition(X10,X11))),complement(X11)) = complement(X11)]. % 6.31/6.75 [5=axiom,[], % 6.31/6.75 converse(composition(X10,X11)) = composition(converse(X11),converse(X10))]. % 6.31/6.75 [6=axiom,[], % 6.31/6.75 join(converse(X10),converse(X11)) = converse(join(X10,X11))]. % 6.31/6.75 [7=axiom,[], % 6.31/6.75 converse(converse(X10)) = X10]. % 6.31/6.75 [8=axiom,[], % 6.31/6.75 join(composition(X10,X12),composition(X11,X12)) = composition(join(X10,X11),X12)]. % 6.31/6.75 [9=axiom,[], % 6.31/6.75 composition(X10,one) = X10]. % 6.31/6.75 [11=axiom,[], % 6.31/6.75 complement(join(complement(X10),complement(X11))) = meet(X10,X11)]. % 6.31/6.75 [12=axiom,[11], % 6.31/6.75 join(meet(X10,X11),complement(join(complement(X10),X11))) = X10]. % 6.31/6.75 [13=axiom,[], % 6.31/6.75 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 6.31/6.75 [14=axiom,[], % 6.31/6.75 join(X10,X11) = join(X11,X10)]. % 6.31/6.75 [15=demod(4),[14], % 6.31/6.75 join(complement(X10),composition(converse(X11),complement(composition(X11,X10)))) = complement(X10)]. % 6.31/6.75 [16=axiom,[], % 6.31/6.75 thtop(X10,X10) = thmfalse]. % 6.31/6.75 [17=axiom,[], % 6.31/6.75 thtop(converse(sk1),sk1) = thmtrue]. % 6.31/6.75 [19=param(7,5),[], % 6.31/6.75 converse(composition(converse(X10),converse(X11))) = composition(X11,X10)]. % 6.31/6.75 [20=param(5,9),[], % 6.31/6.75 composition(converse(one),converse(X10)) = converse(X10)]. % 6.31/6.75 [21=param(5,7),[], % 6.31/6.75 composition(X10,converse(X11)) = converse(composition(X11,converse(X10)))]. % 6.31/6.75 [22=param(5,7),[], % 6.31/6.75 composition(converse(X10),X11) = converse(composition(converse(X11),X10))]. % 6.31/6.75 [24=param(20,7),[7], % 6.31/6.75 composition(converse(one),X10) = X10]. % 6.31/6.75 [25=param(24,9),[], % 6.31/6.75 converse(one) = one]. % 6.31/6.75 [26=demod(24),[25], % 6.31/6.75 composition(one,X10) = X10]. % 6.31/6.75 [30=param(6,7),[], % 6.31/6.75 join(converse(X10),X11) = converse(join(X10,converse(X11)))]. % 6.31/6.75 [34=param(8,26),[14], % 6.31/6.75 join(X10,composition(X11,X10)) = composition(join(X11,one),X10)]. % 6.31/6.75 [35=param(30,3),[], % 6.31/6.75 converse(join(X10,converse(complement(converse(X10))))) = top]. % 6.31/6.75 [37=param(30,14),[], % 6.31/6.75 converse(join(X10,converse(X11))) = join(X11,converse(X10))]. % 6.31/6.75 [51=param(11,3),[2], % 6.31/6.75 complement(top) = zero]. % 6.31/6.75 [52=param(3,11),[13], % 6.31/6.75 join(complement(X10),join(complement(X11),meet(X10,X11))) = top]. % 6.31/6.75 [53=param(11,11),[], % 6.31/6.75 complement(join(meet(X10,X11),complement(X12))) = meet(join(complement(X10),complement(X11)),X12)]. % 6.31/6.75 [54=param(11,11),[], % 6.31/6.75 complement(join(complement(X10),meet(X11,X12))) = meet(X10,join(complement(X11),complement(X12)))]. % 6.31/6.75 [55=param(11,14),[11], % 6.31/6.75 meet(X10,X11) = meet(X11,X10)]. % 6.31/6.75 [57=param(2,51),[55], % 6.31/6.75 meet(zero,top) = zero]. % 6.31/6.75 [59=param(11,51),[], % 6.31/6.75 complement(join(zero,complement(X10))) = meet(top,X10)]. % 6.31/6.75 [60=param(12,2),[11], % 6.31/6.75 join(zero,meet(X10,X10)) = X10]. % 6.31/6.75 [63=param(12,14),[], % 6.31/6.75 join(meet(X10,X11),complement(join(X11,complement(X10)))) = X10]. % 6.31/6.75 [65=param(12,57),[14], % 6.31/6.75 join(zero,complement(join(top,complement(zero)))) = zero]. % 6.31/6.75 [66=param(13,1),[], % 6.31/6.75 join(sk1,join(one,X10)) = join(one,X10)]. % 6.31/6.75 [69=param(13,12),[], % 6.31/6.75 join(meet(X10,X12),join(complement(join(complement(X10),X12)),X11)) = join(X10,X11)]. % 6.31/6.75 [70=param(13,14),[], % 6.31/6.75 join(X10,join(X11,X12)) = join(X12,join(X10,X11))]. % 6.31/6.75 [71=param(13,14),[13], % 6.31/6.75 join(X10,join(X11,X12)) = join(X11,join(X10,X12))]. % 6.31/6.75 [74=param(12,55),[], % 6.31/6.75 join(meet(X10,X11),complement(join(complement(X11),X10))) = X11]. % 6.31/6.75 [77=param(15,7),[], % 6.31/6.75 join(complement(X10),composition(X11,complement(composition(converse(X11),X10)))) = complement(X10)]. % 6.31/6.75 [78=param(15,9),[], % 6.31/6.75 join(complement(one),composition(converse(X10),complement(X10))) = complement(one)]. % 6.31/6.75 [80=param(15,25),[26,26], % 6.31/6.75 join(complement(X10),complement(X10)) = complement(X10)]. % 6.31/6.75 [83=param(11,80),[], % 6.31/6.75 meet(X10,X10) = complement(complement(X10))]. % 6.31/6.75 [85=demod(60),[83], % 6.31/6.75 join(zero,complement(complement(X10))) = X10]. % 6.31/6.75 [87=param(80,51),[51,51], % 6.31/6.75 join(zero,zero) = zero]. % 6.31/6.75 [88=param(13,87),[], % 6.31/6.75 join(zero,join(zero,X10)) = join(zero,X10)]. % 6.31/6.75 [93=param(85,11),[], % 6.31/6.75 join(complement(X10),complement(X11)) = join(zero,complement(meet(X10,X11)))]. % 6.31/6.75 [95=demod(53),[93], % 6.31/6.75 complement(join(meet(X10,X11),complement(X12))) = meet(join(zero,complement(meet(X10,X11))),X12)]. % 6.31/6.75 [97=demod(54),[93], % 6.31/6.75 complement(join(complement(X10),meet(X11,X12))) = meet(X10,join(zero,complement(meet(X11,X12))))]. % 6.31/6.75 [112=param(88,14),[13], % 6.31/6.75 join(zero,join(X10,zero)) = join(zero,X10)]. % 6.31/6.75 [113=param(88,85),[85], % 6.31/6.75 join(zero,X10) = X10]. % 6.31/6.75 [114=demod(59),[113], % 6.31/6.75 meet(top,X10) = complement(complement(X10))]. % 6.31/6.75 [118=demod(65),[113], % 6.31/6.75 complement(join(top,complement(zero))) = zero]. % 6.31/6.75 [119=demod(85),[113], % 6.31/6.75 complement(complement(X10)) = X10]. % 6.31/6.75 [120=demod(114),[119], % 6.31/6.75 meet(top,X10) = X10]. % 6.31/6.75 [121=demod(83),[119], % 6.31/6.75 meet(X10,X10) = X10]. % 6.31/6.75 [123=demod(95),[113], % 6.31/6.75 complement(join(meet(X10,X11),complement(X12))) = meet(complement(meet(X10,X11)),X12)]. % 6.31/6.75 [124=demod(93),[113], % 6.31/6.75 join(complement(X10),complement(X11)) = complement(meet(X10,X11))]. % 6.31/6.75 [125=demod(97),[113], % 6.31/6.75 complement(join(complement(X10),meet(X11,X12))) = meet(X10,complement(meet(X11,X12)))]. % 6.31/6.75 [127=demod(112),[113,113], % 6.31/6.75 join(X10,zero) = X10]. % 6.31/6.75 [132=param(127,30),[], % 6.31/6.75 converse(join(X10,converse(zero))) = converse(X10)]. % 6.31/6.75 [137=param(120,55),[], % 6.31/6.75 meet(X10,top) = X10]. % 6.31/6.75 [143=param(119,51),[], % 6.31/6.75 complement(zero) = top]. % 6.31/6.75 [144=demod(118),[143], % 6.31/6.75 complement(join(top,top)) = zero]. % 6.31/6.75 [156=param(3,144),[13,14,113], % 6.31/6.75 join(top,top) = top]. % 6.31/6.75 [175=param(13,156),[], % 6.31/6.75 join(top,join(top,X10)) = join(top,X10)]. % 6.31/6.75 [183=param(34,19),[], % 6.31/6.75 join(X10,converse(composition(converse(X10),converse(X11)))) = composition(join(X11,one),X10)]. % 6.31/6.75 [191=param(34,1),[26], % 6.31/6.75 join(X10,composition(sk1,X10)) = X10]. % 6.31/6.75 [196=param(34,30),[25], % 6.31/6.75 composition(converse(join(X10,one)),X11) = join(X11,composition(converse(X10),X11))]. % 6.31/6.75 [202=param(191,21),[30,7], % 6.31/6.75 converse(join(X10,composition(X10,converse(sk1)))) = converse(X10)]. % 6.31/6.75 [207=param(7,35),[], % 6.31/6.75 join(X10,converse(complement(converse(X10)))) = converse(top)]. % 6.31/6.75 [225=param(7,132),[7], % 6.31/6.75 join(X10,converse(zero)) = X10]. % 6.31/6.75 [244=param(225,113),[], % 6.31/6.75 converse(zero) = zero]. % 6.31/6.75 [295=param(12,207),[14], % 6.31/6.75 join(complement(converse(top)),meet(X10,converse(complement(converse(complement(X10)))))) = X10]. % 6.31/6.75 [306=param(175,207),[207], % 6.31/6.75 join(top,converse(top)) = converse(top)]. % 6.31/6.75 [308=param(37,306),[7,306], % 6.31/6.75 converse(top) = top]. % 6.31/6.75 [316=demod(295),[308,51,113], % 6.31/6.75 meet(X10,converse(complement(converse(complement(X10))))) = X10]. % 6.31/6.75 [320=demod(207),[308], % 6.31/6.75 join(X10,converse(complement(converse(X10)))) = top]. % 6.31/6.75 [329=param(19,308),[], % 6.31/6.75 converse(composition(top,converse(X10))) = composition(X10,top)]. % 6.31/6.75 [352=param(52,121),[14,3,14], % 6.31/6.75 join(top,complement(X10)) = top]. % 6.31/6.75 [357=param(352,119),[], % 6.31/6.75 join(top,X10) = top]. % 6.31/6.75 [368=param(357,14),[], % 6.31/6.75 join(X10,top) = top]. % 6.31/6.75 [371=param(34,357),[], % 6.31/6.75 join(X10,composition(top,X10)) = composition(top,X10)]. % 6.31/6.75 [432=param(71,3),[368], % 6.31/6.75 join(X10,join(X11,complement(X10))) = top]. % 6.31/6.75 [441=param(71,66),[], % 6.31/6.75 join(one,join(sk1,X10)) = join(one,X10)]. % 6.31/6.75 [457=param(74,2),[119,113], % 6.31/6.75 complement(join(X10,X10)) = complement(X10)]. % 6.31/6.75 [463=param(71,74),[], % 6.31/6.75 join(meet(X12,X11),join(X10,complement(join(complement(X11),X12)))) = join(X10,X11)]. % 6.31/6.75 [485=param(119,457),[119], % 6.31/6.75 join(X10,X10) = X10]. % 6.31/6.75 [494=param(70,485),[], % 6.31/6.75 join(X11,join(X10,X11)) = join(X10,X11)]. % 6.31/6.75 [511=param(494,69),[14,12], % 6.31/6.75 join(X10,meet(X10,X11)) = X10]. % 6.31/6.75 [515=param(78,119),[22], % 6.31/6.75 join(complement(one),converse(composition(converse(X10),complement(X10)))) = complement(one)]. % 6.31/6.75 [520=param(511,55),[], % 6.31/6.75 join(X10,meet(X11,X10)) = X10]. % 6.31/6.75 [574=param(432,69),[], % 6.31/6.75 join(X10,complement(meet(X10,X11))) = top]. % 6.31/6.75 [575=param(432,70),[], % 6.31/6.75 join(complement(X10),join(X10,X11)) = top]. % 6.31/6.75 [577=param(575,8),[], % 6.31/6.75 join(complement(composition(X10,X11)),composition(join(X10,X12),X11)) = top]. % 6.31/6.75 [584=param(575,37),[], % 6.31/6.75 join(complement(X10),converse(join(X11,converse(X10)))) = top]. % 6.31/6.75 [590=param(575,74),[14], % 6.31/6.75 join(X10,complement(meet(X11,X10))) = top]. % 6.31/6.75 [591=param(575,371),[], % 6.31/6.75 join(complement(X10),composition(top,X10)) = top]. % 6.31/6.75 [594=param(12,591),[51,14,113], % 6.31/6.75 meet(X10,composition(top,X10)) = X10]. % 6.31/6.75 [620=param(71,590),[368], % 6.31/6.75 join(X10,join(X11,complement(meet(X12,X10)))) = top]. % 6.31/6.75 [635=param(63,574),[55,51,14,113], % 6.31/6.75 meet(X10,meet(X10,X11)) = meet(X10,X11)]. % 6.31/6.75 [638=param(441,574),[14,357], % 6.31/6.75 join(one,complement(meet(sk1,X10))) = top]. % 6.31/6.75 [642=param(63,638),[55,51,14,113], % 6.31/6.75 meet(one,meet(sk1,X10)) = meet(sk1,X10)]. % 6.31/6.75 [666=param(123,74),[], % 6.31/6.75 meet(complement(meet(X11,X10)),join(complement(X10),X11)) = complement(X10)]. % 6.31/6.75 [680=param(70,124),[], % 6.31/6.75 join(X10,complement(meet(X11,X12))) = join(complement(X12),join(X10,complement(X11)))]. % 6.31/6.75 [681=param(71,124),[], % 6.31/6.75 join(X10,complement(meet(X11,X12))) = join(complement(X11),join(X10,complement(X12)))]. % 6.31/6.75 [683=param(124,119),[], % 6.31/6.75 join(X10,complement(X11)) = complement(meet(complement(X10),X11))]. % 6.31/6.75 [709=demod(463),[683,683], % 6.31/6.75 complement(meet(complement(meet(X10,X11)),meet(complement(X12),join(complement(X11),X10)))) = join(X12,X11)]. % 6.31/6.75 [723=demod(620),[683,683], % 6.31/6.75 complement(meet(complement(X10),meet(complement(X11),meet(X12,X10)))) = top]. % 6.31/6.75 [729=demod(574),[683], % 6.31/6.75 complement(meet(complement(X10),meet(X10,X11))) = top]. % 6.31/6.75 [735=demod(680),[683,683,683,119], % 6.31/6.75 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X12,meet(complement(X10),X11)))]. % 6.31/6.75 [740=demod(681),[683,683,683,119], % 6.31/6.75 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X11,meet(complement(X10),X12)))]. % 6.31/6.75 [741=demod(729),[], % 6.31/6.75 complement(meet(complement(X10),meet(X10,X11))) = top]. % 6.31/6.75 [745=param(125,55),[125], % 6.31/6.75 meet(X10,complement(meet(X11,X12))) = meet(X10,complement(meet(X12,X11)))]. % 6.31/6.75 [749=param(683,14),[], % 6.31/6.75 join(complement(X11),X10) = complement(meet(complement(X10),X11))]. % 6.31/6.75 [751=demod(584),[749,55], % 6.31/6.75 complement(meet(X10,complement(converse(join(X11,converse(X10)))))) = top]. % 6.31/6.75 [755=demod(515),[749,55], % 6.31/6.75 complement(meet(one,complement(converse(composition(converse(X10),complement(X10)))))) = complement(one)]. % 6.31/6.75 [763=demod(666),[749], % 6.31/6.75 meet(complement(meet(X10,X11)),complement(meet(complement(X10),X11))) = complement(X11)]. % 6.31/6.75 [770=demod(77),[749,55], % 6.31/6.75 complement(meet(X10,complement(composition(X11,complement(composition(converse(X11),X10)))))) = complement(X10)]. % 6.31/6.75 [771=demod(15),[749,55], % 6.31/6.75 complement(meet(X10,complement(composition(converse(X11),complement(composition(X11,X10)))))) = complement(X10)]. % 6.31/6.75 [774=demod(577),[749,55], % 6.31/6.75 complement(meet(composition(X10,X11),complement(composition(join(X10,X12),X11)))) = top]. % 6.31/6.75 [806=demod(709),[749], % 6.31/6.75 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = join(X12,X11)]. % 6.31/6.75 [814=param(683,30),[], % 6.31/6.75 converse(join(X10,converse(complement(X11)))) = complement(meet(complement(converse(X10)),X11))]. % 6.31/6.75 [817=param(66,683),[683,683], % 6.31/6.75 complement(meet(complement(sk1),meet(complement(one),X10))) = complement(meet(complement(one),X10))]. % 6.31/6.75 [818=param(683,119),[], % 6.31/6.75 join(X10,X11) = complement(meet(complement(X10),complement(X11)))]. % 6.31/6.75 [819=demod(1),[818], % 6.31/6.75 complement(meet(complement(sk1),complement(one))) = one]. % 6.31/6.75 [835=demod(183),[818,818], % 6.31/6.75 complement(meet(complement(X10),complement(converse(composition(converse(X10),converse(X11)))))) = composition(complement(meet(complement(X11),complement(one))),X10)]. % 6.31/6.75 [839=demod(320),[818], % 6.31/6.75 complement(meet(complement(X10),complement(converse(complement(converse(X10)))))) = top]. % 6.31/6.75 [841=demod(814),[818], % 6.31/6.75 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),complement(converse(complement(X11))))))]. % 6.31/6.75 [848=demod(751),[818], % 6.31/6.75 complement(meet(X10,complement(converse(complement(meet(complement(X11),complement(converse(X10)))))))) = top]. % 6.31/6.75 [854=demod(37),[818,818], % 6.31/6.75 converse(complement(meet(complement(X10),complement(converse(X11))))) = complement(meet(complement(X11),complement(converse(X10))))]. % 6.31/6.75 [872=demod(806),[818], % 6.31/6.75 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = complement(meet(complement(X12),complement(X11)))]. % 6.31/6.75 [903=demod(196),[818,818], % 6.31/6.75 composition(converse(complement(meet(complement(X10),complement(one)))),X11) = complement(meet(complement(X11),complement(composition(converse(X10),X11))))]. % 6.31/6.75 [909=demod(202),[818], % 6.31/6.75 converse(complement(meet(complement(X10),complement(composition(X10,converse(sk1)))))) = converse(X10)]. % 6.31/6.75 [912=demod(191),[818], % 6.31/6.75 complement(meet(complement(X10),complement(composition(sk1,X10)))) = X10]. % 6.31/6.75 [945=demod(774),[818], % 6.31/6.75 complement(meet(composition(X10,X11),complement(composition(complement(meet(complement(X10),complement(X12))),X11)))) = top]. % 6.31/6.75 [1043=demod(520),[818], % 6.31/6.75 complement(meet(complement(X10),complement(meet(X11,X10)))) = X10]. % 6.31/6.75 [1072=param(119,819),[], % 6.31/6.75 meet(complement(sk1),complement(one)) = complement(one)]. % 6.31/6.75 [1085=param(2,741),[55,120], % 6.31/6.75 meet(complement(X10),meet(X10,X11)) = zero]. % 6.31/6.75 [1088=param(1085,119),[], % 6.31/6.75 meet(X10,meet(complement(X10),X11)) = zero]. % 6.31/6.75 [1121=param(119,1043),[], % 6.31/6.75 meet(complement(X10),complement(meet(X11,X10))) = complement(X10)]. % 6.31/6.75 [1122=param(1121,55),[], % 6.31/6.75 meet(complement(X10),complement(meet(X10,X11))) = complement(X10)]. % 6.31/6.75 [1123=param(1121,594),[55], % 6.31/6.75 meet(complement(X10),complement(composition(top,X10))) = complement(composition(top,X10))]. % 6.31/6.75 [1135=param(119,912),[], % 6.31/6.75 meet(complement(X10),complement(composition(sk1,X10))) = complement(X10)]. % 6.31/6.75 [1175=param(2,723),[55,120], % 6.31/6.75 meet(complement(X10),meet(complement(X11),meet(X12,X10))) = zero]. % 6.31/6.75 [1179=param(1175,119),[], % 6.31/6.75 meet(complement(X10),meet(X11,meet(X12,X10))) = zero]. % 6.31/6.75 [1181=param(1179,55),[], % 6.31/6.75 meet(complement(X10),meet(meet(X11,X10),X12)) = zero]. % 6.31/6.75 [1182=param(1179,55),[], % 6.31/6.75 meet(complement(X10),meet(X11,meet(X10,X12))) = zero]. % 6.31/6.75 [1196=param(1179,1135),[119], % 6.31/6.75 meet(composition(sk1,X10),meet(X11,complement(X10))) = zero]. % 6.31/6.75 [1222=param(119,735),[119], % 6.31/6.75 meet(X10,meet(complement(X11),X12)) = meet(complement(X11),meet(X12,X10))]. % 6.31/6.75 [1264=param(119,740),[119], % 6.31/6.75 meet(X10,meet(complement(X11),X12)) = meet(complement(X11),meet(X10,X12))]. % 6.31/6.75 [1316=param(755,25),[26], % 6.31/6.75 complement(meet(one,complement(converse(complement(one))))) = complement(one)]. % 6.31/6.75 [1318=param(119,1316),[119], % 6.31/6.75 meet(one,complement(converse(complement(one)))) = one]. % 6.31/6.75 [1320=param(1121,1318),[119,55,119], % 6.31/6.75 meet(complement(one),converse(complement(one))) = converse(complement(one))]. % 6.31/6.75 [1329=param(763,745),[], % 6.31/6.75 meet(complement(meet(X11,X10)),complement(meet(X10,complement(X11)))) = complement(X10)]. % 6.31/6.75 [1347=param(119,770),[119], % 6.31/6.75 meet(X10,complement(composition(X11,complement(composition(converse(X11),X10))))) = X10]. % 6.31/6.75 [1353=param(119,771),[119], % 6.31/6.75 meet(X10,complement(composition(converse(X11),complement(composition(X11,X10))))) = X10]. % 6.31/6.75 [1469=param(119,817),[119], % 6.31/6.75 meet(complement(sk1),meet(complement(one),X10)) = meet(complement(one),X10)]. % 6.31/6.75 [1625=param(2,839),[55,120], % 6.31/6.75 meet(complement(X10),complement(converse(complement(converse(X10))))) = zero]. % 6.31/6.75 [1634=param(841,316),[119,119,7], % 6.31/6.75 converse(complement(meet(complement(X10),complement(converse(complement(converse(complement(X10)))))))) = converse(X10)]. % 6.31/6.75 [1664=param(1469,316),[1072,119,25,1320], % 6.31/6.75 converse(complement(one)) = complement(one)]. % 6.31/6.75 [1667=param(1122,1469),[119,119], % 6.31/6.75 meet(sk1,complement(meet(complement(one),X10))) = sk1]. % 6.31/6.75 [1672=param(2,848),[55,120], % 6.31/6.75 meet(X10,complement(converse(complement(meet(complement(X11),complement(converse(X10))))))) = zero]. % 6.31/6.75 [1686=param(835,1664),[119,2,143], % 6.31/6.75 complement(meet(complement(X10),complement(converse(composition(converse(X10),complement(one)))))) = composition(top,X10)]. % 6.31/6.75 [1688=param(1667,55),[], % 6.31/6.75 meet(sk1,complement(meet(X10,complement(one)))) = sk1]. % 6.31/6.75 [1695=param(1688,841),[119,25], % 6.31/6.75 meet(sk1,converse(complement(meet(complement(X10),complement(one))))) = sk1]. % 6.31/6.75 [1716=param(854,1664),[119,55,119], % 6.31/6.75 complement(meet(one,complement(converse(X10)))) = converse(complement(meet(one,complement(X10))))]. % 6.31/6.75 [1721=param(119,1716),[], % 6.31/6.75 meet(one,complement(converse(X10))) = complement(converse(complement(meet(one,complement(X10)))))]. % 6.31/6.75 [1736=param(1695,119),[], % 6.31/6.75 meet(sk1,converse(complement(meet(X10,complement(one))))) = sk1]. % 6.31/6.75 [1737=param(1736,55),[], % 6.31/6.75 meet(sk1,converse(complement(meet(complement(one),X10)))) = sk1]. % 6.31/6.75 [1866=param(872,1122),[119,55,119], % 6.31/6.75 complement(meet(X10,complement(meet(X10,X11)))) = complement(meet(X10,complement(X11)))]. % 6.31/6.75 [1870=param(119,1866),[119], % 6.31/6.75 meet(X10,complement(meet(X10,X11))) = meet(X10,complement(X11))]. % 6.31/6.75 [1871=param(1870,55),[], % 6.31/6.75 meet(X10,complement(meet(X11,X10))) = meet(X10,complement(X11))]. % 6.31/6.75 [1942=param(1870,1625),[143,55,120,119], % 6.31/6.75 meet(complement(X10),converse(complement(converse(X10)))) = complement(X10)]. % 6.31/6.75 [1945=param(1870,1721),[119,119], % 6.31/6.75 meet(one,converse(complement(meet(one,complement(X10))))) = meet(one,converse(X10))]. % 6.31/6.75 [1954=param(1121,1942),[119,55], % 6.31/6.75 meet(X10,complement(converse(complement(converse(X10))))) = complement(converse(complement(converse(X10))))]. % 6.31/6.75 [1955=demod(1634),[1954,119,7], % 6.31/6.75 complement(converse(complement(X10))) = converse(X10)]. % 6.31/6.75 [1973=demod(1672),[1955], % 6.31/6.75 meet(X10,converse(meet(complement(X11),complement(converse(X10))))) = zero]. % 6.31/6.75 [2004=demod(1721),[1955], % 6.31/6.75 meet(one,complement(converse(X10))) = converse(meet(one,complement(X10)))]. % 6.31/6.75 [2016=param(1955,119),[], % 6.31/6.75 complement(converse(X10)) = converse(complement(X10))]. % 6.31/6.75 [2019=demod(2004),[2016], % 6.31/6.75 meet(one,converse(complement(X10))) = converse(meet(one,complement(X10)))]. % 6.31/6.75 [2020=demod(1945),[2019,1870,119], % 6.31/6.75 meet(one,converse(X10)) = converse(meet(one,X10))]. % 6.31/6.75 [2023=demod(1973),[2016], % 6.31/6.75 meet(X10,converse(meet(complement(X11),converse(complement(X10))))) = zero]. % 6.31/6.75 [2103=demod(1686),[2016], % 6.31/6.75 complement(meet(complement(X10),converse(complement(composition(converse(X10),complement(one)))))) = composition(top,X10)]. % 6.31/6.75 [2209=param(1122,2020),[2016], % 6.31/6.75 meet(complement(one),converse(complement(meet(one,X10)))) = complement(one)]. % 6.31/6.75 [2247=param(1871,1182),[143,55,120,119,55], % 6.31/6.75 meet(X11,meet(X10,meet(X11,X12))) = meet(X10,meet(X11,X12))]. % 6.31/6.75 [2252=param(1871,1196),[143,55,120,55,-1222], % 6.31/6.75 meet(X10,complement(X11)) = meet(complement(X11),meet(complement(composition(sk1,X11)),X10))]. % 6.31/6.75 [2338=param(903,1072),[119,25,26], % 6.31/6.75 complement(meet(complement(X10),complement(composition(converse(sk1),X10)))) = X10]. % 6.31/6.75 [2402=param(2209,642),[], % 6.31/6.75 meet(complement(one),converse(complement(meet(sk1,X10)))) = complement(one)]. % 6.31/6.75 [2406=param(7,909),[7], % 6.31/6.75 complement(meet(complement(X10),complement(composition(X10,converse(sk1))))) = X10]. % 6.31/6.75 [2446=param(1181,2402),[2016,119], % 6.31/6.75 meet(converse(meet(sk1,X10)),meet(complement(one),X11)) = zero]. % 6.31/6.75 [2616=param(945,2),[143], % 6.31/6.75 complement(meet(composition(X10,X11),complement(composition(top,X11)))) = top]. % 6.31/6.75 [2618=param(2,2616),[55,120], % 6.31/6.75 meet(composition(X10,X11),complement(composition(top,X11))) = zero]. % 6.31/6.75 [2622=param(2618,55),[], % 6.31/6.75 meet(complement(composition(top,X10)),composition(X11,X10)) = zero]. % 6.31/6.75 [2834=param(119,2406),[], % 6.31/6.75 meet(complement(X10),complement(composition(X10,converse(sk1)))) = complement(X10)]. % 6.31/6.75 [2842=param(1121,2834),[119,119,55,119], % 6.31/6.75 meet(X10,composition(X10,converse(sk1))) = composition(X10,converse(sk1))]. % 6.31/6.75 [2882=param(2842,2622),[21,308,2016,-5], % 6.31/6.75 converse(composition(sk1,complement(composition(sk1,top)))) = zero]. % 6.31/6.75 [2888=param(7,2882),[244], % 6.31/6.75 composition(sk1,complement(composition(sk1,top))) = zero]. % 6.31/6.75 [3097=param(119,2338),[], % 6.31/6.75 meet(complement(X10),complement(composition(converse(sk1),X10))) = complement(X10)]. % 6.31/6.75 [3109=param(1121,3097),[119,119,55,119], % 6.31/6.75 meet(X10,composition(converse(sk1),X10)) = composition(converse(sk1),X10)]. % 6.31/6.75 [3129=param(3109,5),[], % 6.31/6.75 meet(converse(X10),converse(composition(X10,sk1))) = composition(converse(sk1),converse(X10))]. % 6.31/6.75 [3166=param(1737,3109),[], % 6.31/6.75 meet(sk1,converse(complement(composition(converse(sk1),complement(one))))) = sk1]. % 6.31/6.75 [4161=param(1871,1088),[143,55,120,2252,-1264,635], % 6.31/6.75 meet(complement(X10),meet(complement(composition(sk1,X10)),X11)) = meet(complement(X10),X11)]. % 6.31/6.75 [5130=param(1222,55),[], % 6.31/6.75 meet(meet(complement(X10),X11),X12) = meet(complement(X10),meet(X11,X12))]. % 6.31/6.75 [5771=demod(2446),[], % 6.31/6.75 meet(converse(meet(sk1,X10)),meet(complement(one),X11)) = zero]. % 6.31/6.75 [6199=param(1329,3166),[2252,4161,2103,2016,119], % 6.31/6.75 meet(complement(sk1),composition(top,sk1)) = converse(composition(converse(sk1),complement(one)))]. % 6.31/6.75 [6228=param(1353,2888),[143,-329,7,2016], % 6.31/6.75 meet(complement(composition(sk1,top)),converse(complement(composition(top,sk1)))) = complement(composition(sk1,top))]. % 6.31/6.75 [6354=param(5130,119),[119], % 6.31/6.75 meet(meet(X10,X11),X12) = meet(X10,meet(X11,X12))]. % 6.31/6.75 [6690=param(6354,6199),[], % 6.31/6.75 meet(converse(composition(converse(sk1),complement(one))),X10) = meet(complement(sk1),meet(composition(top,sk1),X10))]. % 6.31/6.75 [9643=param(2023,119),[], % 6.31/6.75 meet(X10,converse(meet(X11,converse(complement(X10))))) = zero]. % 6.31/6.75 [9667=param(9643,2016),[7], % 6.31/6.75 meet(converse(X10),converse(meet(X11,complement(X10)))) = zero]. % 6.31/6.75 [9704=param(9667,1122),[55], % 6.31/6.75 meet(converse(complement(X10)),converse(meet(X10,X11))) = zero]. % 6.31/6.75 [9730=param(9704,1123),[119], % 6.31/6.75 meet(converse(X10),converse(complement(composition(top,X10)))) = zero]. % 6.31/6.75 [9742=param(1871,9704),[143,55,120,2016,119,55], % 6.31/6.75 meet(converse(X10),converse(meet(X10,X11))) = converse(meet(X10,X11))]. % 6.31/6.75 [9752=param(9704,3129),[2016,7], % 6.31/6.75 meet(complement(X10),converse(composition(converse(sk1),converse(X10)))) = zero]. % 6.31/6.75 [9807=param(9730,21),[7,308,2016,7], % 6.31/6.75 meet(X10,complement(composition(X10,top))) = zero]. % 6.31/6.75 [9871=param(1870,9807),[143,137,119], % 6.31/6.75 meet(X10,composition(X10,top)) = X10]. % 6.31/6.75 [9896=param(6354,9871),[], % 6.31/6.75 meet(X10,meet(composition(X10,top),X11)) = meet(X10,X11)]. % 6.31/6.75 [10059=param(9896,2247),[635], % 6.31/6.75 meet(composition(X10,top),meet(X10,X11)) = meet(X10,X11)]. % 6.31/6.75 [10613=param(9742,10059),[10059], % 6.31/6.75 meet(converse(composition(X10,top)),converse(meet(X10,X11))) = converse(meet(X10,X11))]. % 6.31/6.75 [10985=param(9752,5),[7,7], % 6.31/6.75 meet(complement(X10),composition(X10,sk1)) = zero]. % 6.31/6.75 [11017=param(1871,10985),[143,55,120,119,55], % 6.31/6.75 meet(X10,composition(X10,sk1)) = composition(X10,sk1)]. % 6.31/6.75 [11042=param(11017,2622),[-19], % 6.31/6.75 converse(composition(converse(sk1),converse(complement(composition(top,sk1))))) = zero]. % 6.31/6.75 [11050=param(5771,11017),[-19,1664,55,6690], % 6.31/6.75 meet(complement(sk1),meet(composition(top,sk1),converse(meet(sk1,X10)))) = zero]. % 6.31/6.75 [11710=param(7,11042),[244], % 6.31/6.75 composition(converse(sk1),converse(complement(composition(top,sk1)))) = zero]. % 6.31/6.75 [11720=param(1347,11710),[143,2252,4161,6228], % 6.31/6.75 converse(complement(composition(top,sk1))) = complement(composition(sk1,top))]. % 6.31/6.75 [11725=param(7,11720),[], % 6.31/6.75 complement(composition(top,sk1)) = converse(complement(composition(sk1,top)))]. % 6.31/6.75 [11739=param(119,11725),[2016,119], % 6.31/6.75 composition(top,sk1) = converse(composition(sk1,top))]. % 6.31/6.75 [11770=demod(11050),[11739,10613], % 6.31/6.75 meet(complement(sk1),converse(meet(sk1,X10))) = zero]. % 6.31/6.75 [11892=param(11770,121),[55], % 6.31/6.75 meet(converse(sk1),complement(sk1)) = zero]. % 6.31/6.75 [11919=param(1870,11892),[143,55,120,119,55], % 6.31/6.75 meet(sk1,converse(sk1)) = converse(sk1)]. % 6.31/6.75 [11934=param(9742,11919),[7,55,11919,11919,7], % 6.31/6.75 converse(sk1) = sk1]. % 6.31/6.75 [12204=param(17,11934),[16], % 6.31/6.75 thmtrue = thmfalse]. % 6.31/6.75 % SZS output end CNFRefutation % 6.31/6.75 Space: 44135 KB %------------------------------------------------------------------------------