%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : REL027-1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n007.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:31 EDT 2022 % Result : Unsatisfiable 17.94s 18.33s % Output : CNFRefutation 17.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : REL027-1 : TPTP v8.1.0. Released v4.0.0. % 0.08/0.12 % Command : fiesta-wrapper %s % 0.12/0.34 % Computer : n007.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 09:36:45 EDT 2022 % 0.12/0.34 % CPUTime : % 17.94/18.33 Theorem Proved. % 17.94/18.33 % SZS status Unsatisfiable % 17.94/18.33 % SZS output start CNFRefutation % 17.94/18.33 [1=axiom,[], % 17.94/18.33 join(sk1,one) = one]. % 17.94/18.33 [2=axiom,[], % 17.94/18.33 meet(X10,complement(X10)) = zero]. % 17.94/18.33 [3=axiom,[], % 17.94/18.33 join(X10,complement(X10)) = top]. % 17.94/18.33 [4=axiom,[], % 17.94/18.33 join(composition(converse(X10),complement(composition(X10,X11))),complement(X11)) = complement(X11)]. % 17.94/18.33 [5=axiom,[], % 17.94/18.33 converse(composition(X10,X11)) = composition(converse(X11),converse(X10))]. % 17.94/18.33 [6=axiom,[], % 17.94/18.33 join(converse(X10),converse(X11)) = converse(join(X10,X11))]. % 17.94/18.33 [7=axiom,[], % 17.94/18.33 converse(converse(X10)) = X10]. % 17.94/18.33 [8=axiom,[], % 17.94/18.33 join(composition(X10,X12),composition(X11,X12)) = composition(join(X10,X11),X12)]. % 17.94/18.33 [9=axiom,[], % 17.94/18.33 composition(X10,one) = X10]. % 17.94/18.33 [11=axiom,[], % 17.94/18.33 complement(join(complement(X10),complement(X11))) = meet(X10,X11)]. % 17.94/18.33 [12=axiom,[11], % 17.94/18.33 join(meet(X10,X11),complement(join(complement(X10),X11))) = X10]. % 17.94/18.33 [13=axiom,[], % 17.94/18.33 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 17.94/18.33 [14=axiom,[], % 17.94/18.33 join(X10,X11) = join(X11,X10)]. % 17.94/18.33 [15=demod(4),[14], % 17.94/18.33 join(complement(X10),composition(converse(X11),complement(composition(X11,X10)))) = complement(X10)]. % 17.94/18.33 [16=axiom,[], % 17.94/18.33 thtop(X10,X10) = thmfalse]. % 17.94/18.33 [17=axiom,[], % 17.94/18.33 thtop(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) = thmtrue]. % 17.94/18.33 [19=param(7,5),[], % 17.94/18.33 converse(composition(converse(X10),converse(X11))) = composition(X11,X10)]. % 17.94/18.33 [20=param(5,9),[], % 17.94/18.33 composition(converse(one),converse(X10)) = converse(X10)]. % 17.94/18.33 [21=param(5,7),[], % 17.94/18.33 composition(X10,converse(X11)) = converse(composition(X11,converse(X10)))]. % 17.94/18.33 [22=param(5,7),[], % 17.94/18.33 composition(converse(X10),X11) = converse(composition(converse(X11),X10))]. % 17.94/18.33 [24=param(20,7),[7], % 17.94/18.33 composition(converse(one),X10) = X10]. % 17.94/18.33 [25=param(24,9),[], % 17.94/18.33 converse(one) = one]. % 17.94/18.33 [26=demod(24),[25], % 17.94/18.33 composition(one,X10) = X10]. % 17.94/18.33 [30=param(6,7),[], % 17.94/18.33 join(converse(X10),X11) = converse(join(X10,converse(X11)))]. % 17.94/18.33 [34=param(8,26),[14], % 17.94/18.33 join(X10,composition(X11,X10)) = composition(join(X11,one),X10)]. % 17.94/18.33 [35=param(30,3),[], % 17.94/18.33 converse(join(X10,converse(complement(converse(X10))))) = top]. % 17.94/18.33 [37=param(30,14),[], % 17.94/18.33 converse(join(X10,converse(X11))) = join(X11,converse(X10))]. % 17.94/18.33 [51=param(11,3),[2], % 17.94/18.33 complement(top) = zero]. % 17.94/18.33 [52=param(3,11),[13], % 17.94/18.33 join(complement(X10),join(complement(X11),meet(X10,X11))) = top]. % 17.94/18.33 [53=param(11,11),[], % 17.94/18.33 complement(join(meet(X10,X11),complement(X12))) = meet(join(complement(X10),complement(X11)),X12)]. % 17.94/18.33 [54=param(11,11),[], % 17.94/18.33 complement(join(complement(X10),meet(X11,X12))) = meet(X10,join(complement(X11),complement(X12)))]. % 17.94/18.33 [55=param(11,14),[11], % 17.94/18.33 meet(X10,X11) = meet(X11,X10)]. % 17.94/18.33 [57=param(2,51),[55], % 17.94/18.33 meet(zero,top) = zero]. % 17.94/18.33 [59=param(11,51),[], % 17.94/18.33 complement(join(zero,complement(X10))) = meet(top,X10)]. % 17.94/18.33 [60=param(12,2),[11], % 17.94/18.33 join(zero,meet(X10,X10)) = X10]. % 17.94/18.33 [63=param(12,14),[], % 17.94/18.33 join(meet(X10,X11),complement(join(X11,complement(X10)))) = X10]. % 17.94/18.33 [65=param(12,57),[14], % 17.94/18.33 join(zero,complement(join(top,complement(zero)))) = zero]. % 17.94/18.33 [66=param(13,1),[], % 17.94/18.33 join(sk1,join(one,X10)) = join(one,X10)]. % 17.94/18.33 [69=param(13,12),[], % 17.94/18.33 join(meet(X10,X12),join(complement(join(complement(X10),X12)),X11)) = join(X10,X11)]. % 17.94/18.33 [70=param(13,14),[], % 17.94/18.33 join(X10,join(X11,X12)) = join(X12,join(X10,X11))]. % 17.94/18.33 [71=param(13,14),[13], % 17.94/18.33 join(X10,join(X11,X12)) = join(X11,join(X10,X12))]. % 17.94/18.33 [74=param(12,55),[], % 17.94/18.33 join(meet(X10,X11),complement(join(complement(X11),X10))) = X11]. % 17.94/18.33 [75=param(17,55),[55], % 17.94/18.33 thtop(meet(one,complement(composition(sk1,top))),meet(one,complement(sk1))) = thmtrue]. % 17.94/18.33 [82=param(15,7),[], % 17.94/18.33 join(complement(X10),composition(X11,complement(composition(converse(X11),X10)))) = complement(X10)]. % 17.94/18.33 [83=param(15,9),[], % 17.94/18.33 join(complement(one),composition(converse(X10),complement(X10))) = complement(one)]. % 17.94/18.33 [85=param(15,25),[26,26], % 17.94/18.33 join(complement(X10),complement(X10)) = complement(X10)]. % 17.94/18.33 [88=param(11,85),[], % 17.94/18.33 meet(X10,X10) = complement(complement(X10))]. % 17.94/18.33 [90=demod(60),[88], % 17.94/18.33 join(zero,complement(complement(X10))) = X10]. % 17.94/18.33 [92=param(85,51),[51,51], % 17.94/18.33 join(zero,zero) = zero]. % 17.94/18.33 [93=param(13,92),[], % 17.94/18.33 join(zero,join(zero,X10)) = join(zero,X10)]. % 17.94/18.33 [98=param(90,11),[], % 17.94/18.33 join(complement(X10),complement(X11)) = join(zero,complement(meet(X10,X11)))]. % 17.94/18.33 [100=demod(53),[98], % 17.94/18.33 complement(join(meet(X10,X11),complement(X12))) = meet(join(zero,complement(meet(X10,X11))),X12)]. % 17.94/18.33 [102=demod(54),[98], % 17.94/18.33 complement(join(complement(X10),meet(X11,X12))) = meet(X10,join(zero,complement(meet(X11,X12))))]. % 17.94/18.33 [117=param(93,14),[13], % 17.94/18.33 join(zero,join(X10,zero)) = join(zero,X10)]. % 17.94/18.33 [118=param(93,90),[90], % 17.94/18.33 join(zero,X10) = X10]. % 17.94/18.33 [119=demod(59),[118], % 17.94/18.33 meet(top,X10) = complement(complement(X10))]. % 17.94/18.33 [123=demod(65),[118], % 17.94/18.33 complement(join(top,complement(zero))) = zero]. % 17.94/18.33 [124=demod(90),[118], % 17.94/18.33 complement(complement(X10)) = X10]. % 17.94/18.33 [125=demod(119),[124], % 17.94/18.33 meet(top,X10) = X10]. % 17.94/18.33 [126=demod(88),[124], % 17.94/18.33 meet(X10,X10) = X10]. % 17.94/18.33 [128=demod(100),[118], % 17.94/18.33 complement(join(meet(X10,X11),complement(X12))) = meet(complement(meet(X10,X11)),X12)]. % 17.94/18.33 [129=demod(98),[118], % 17.94/18.33 join(complement(X10),complement(X11)) = complement(meet(X10,X11))]. % 17.94/18.33 [130=demod(102),[118], % 17.94/18.33 complement(join(complement(X10),meet(X11,X12))) = meet(X10,complement(meet(X11,X12)))]. % 17.94/18.33 [132=demod(117),[118,118], % 17.94/18.33 join(X10,zero) = X10]. % 17.94/18.33 [137=param(132,30),[], % 17.94/18.33 converse(join(X10,converse(zero))) = converse(X10)]. % 17.94/18.33 [142=param(125,55),[], % 17.94/18.33 meet(X10,top) = X10]. % 17.94/18.33 [148=param(124,51),[], % 17.94/18.33 complement(zero) = top]. % 17.94/18.33 [149=demod(123),[148], % 17.94/18.33 complement(join(top,top)) = zero]. % 17.94/18.33 [150=param(12,148),[], % 17.94/18.33 join(meet(zero,X10),complement(join(top,X10))) = zero]. % 17.94/18.33 [161=param(3,149),[13,14,118], % 17.94/18.33 join(top,top) = top]. % 17.94/18.33 [180=param(13,161),[], % 17.94/18.33 join(top,join(top,X10)) = join(top,X10)]. % 17.94/18.33 [188=param(34,19),[], % 17.94/18.33 join(X10,converse(composition(converse(X10),converse(X11)))) = composition(join(X11,one),X10)]. % 17.94/18.33 [196=param(34,1),[26], % 17.94/18.33 join(X10,composition(sk1,X10)) = X10]. % 17.94/18.33 [201=param(34,30),[25], % 17.94/18.33 composition(converse(join(X10,one)),X11) = join(X11,composition(converse(X10),X11))]. % 17.94/18.33 [207=param(196,21),[30,7], % 17.94/18.33 converse(join(X10,composition(X10,converse(sk1)))) = converse(X10)]. % 17.94/18.33 [212=param(7,35),[], % 17.94/18.33 join(X10,converse(complement(converse(X10)))) = converse(top)]. % 17.94/18.33 [230=param(7,137),[7], % 17.94/18.33 join(X10,converse(zero)) = X10]. % 17.94/18.33 [250=param(230,118),[], % 17.94/18.33 converse(zero) = zero]. % 17.94/18.33 [295=param(12,212),[14], % 17.94/18.33 join(complement(converse(top)),meet(X10,converse(complement(converse(complement(X10)))))) = X10]. % 17.94/18.33 [305=param(180,212),[212], % 17.94/18.33 join(top,converse(top)) = converse(top)]. % 17.94/18.33 [307=param(37,305),[7,305], % 17.94/18.33 converse(top) = top]. % 17.94/18.33 [314=demod(295),[307,51,118], % 17.94/18.33 meet(X10,converse(complement(converse(complement(X10))))) = X10]. % 17.94/18.33 [318=demod(212),[307], % 17.94/18.33 join(X10,converse(complement(converse(X10)))) = top]. % 17.94/18.33 [328=param(19,307),[], % 17.94/18.33 converse(composition(top,converse(X10))) = composition(X10,top)]. % 17.94/18.33 [364=param(52,126),[14,3,14], % 17.94/18.33 join(top,complement(X10)) = top]. % 17.94/18.33 [369=param(364,124),[], % 17.94/18.33 join(top,X10) = top]. % 17.94/18.33 [374=demod(150),[369,51,14,118], % 17.94/18.33 meet(zero,X10) = zero]. % 17.94/18.33 [380=param(369,14),[], % 17.94/18.33 join(X10,top) = top]. % 17.94/18.33 [383=param(34,369),[], % 17.94/18.33 join(X10,composition(top,X10)) = composition(top,X10)]. % 17.94/18.33 [444=param(71,3),[380], % 17.94/18.33 join(X10,join(X11,complement(X10))) = top]. % 17.94/18.33 [453=param(71,66),[], % 17.94/18.33 join(one,join(sk1,X10)) = join(one,X10)]. % 17.94/18.33 [469=param(74,2),[124,118], % 17.94/18.33 complement(join(X10,X10)) = complement(X10)]. % 17.94/18.33 [475=param(71,74),[], % 17.94/18.33 join(meet(X12,X11),join(X10,complement(join(complement(X11),X12)))) = join(X10,X11)]. % 17.94/18.33 [499=param(124,469),[124], % 17.94/18.33 join(X10,X10) = X10]. % 17.94/18.33 [508=param(70,499),[], % 17.94/18.33 join(X11,join(X10,X11)) = join(X10,X11)]. % 17.94/18.33 [522=param(508,69),[14,12], % 17.94/18.33 join(X10,meet(X10,X11)) = X10]. % 17.94/18.33 [532=param(522,55),[], % 17.94/18.33 join(X10,meet(X11,X10)) = X10]. % 17.94/18.33 [541=param(83,124),[22], % 17.94/18.33 join(complement(one),converse(composition(converse(X10),complement(X10)))) = complement(one)]. % 17.94/18.33 [589=param(444,69),[], % 17.94/18.33 join(X10,complement(meet(X10,X11))) = top]. % 17.94/18.33 [590=param(444,70),[], % 17.94/18.33 join(complement(X10),join(X10,X11)) = top]. % 17.94/18.33 [592=param(590,8),[], % 17.94/18.33 join(complement(composition(X10,X11)),composition(join(X10,X12),X11)) = top]. % 17.94/18.33 [599=param(590,37),[], % 17.94/18.33 join(complement(X10),converse(join(X11,converse(X10)))) = top]. % 17.94/18.33 [605=param(590,74),[14], % 17.94/18.33 join(X10,complement(meet(X11,X10))) = top]. % 17.94/18.33 [607=param(590,383),[], % 17.94/18.33 join(complement(X10),composition(top,X10)) = top]. % 17.94/18.33 [609=param(12,607),[51,14,118], % 17.94/18.33 meet(X10,composition(top,X10)) = X10]. % 17.94/18.33 [632=param(63,605),[55,51,14,118], % 17.94/18.33 meet(X10,meet(X11,X10)) = meet(X11,X10)]. % 17.94/18.33 [634=param(71,605),[380], % 17.94/18.33 join(X10,join(X11,complement(meet(X12,X10)))) = top]. % 17.94/18.33 [650=param(63,589),[55,51,14,118], % 17.94/18.33 meet(X10,meet(X10,X11)) = meet(X10,X11)]. % 17.94/18.33 [653=param(453,589),[14,369], % 17.94/18.33 join(one,complement(meet(sk1,X10))) = top]. % 17.94/18.33 [657=param(63,653),[55,51,14,118], % 17.94/18.33 meet(one,meet(sk1,X10)) = meet(sk1,X10)]. % 17.94/18.33 [688=param(128,63),[], % 17.94/18.33 meet(complement(meet(X10,X11)),join(X11,complement(X10))) = complement(X10)]. % 17.94/18.33 [689=param(128,74),[], % 17.94/18.33 meet(complement(meet(X11,X10)),join(complement(X10),X11)) = complement(X10)]. % 17.94/18.33 [701=param(70,129),[], % 17.94/18.33 join(X10,complement(meet(X11,X12))) = join(complement(X12),join(X10,complement(X11)))]. % 17.94/18.33 [702=param(71,129),[], % 17.94/18.33 join(X10,complement(meet(X11,X12))) = join(complement(X11),join(X10,complement(X12)))]. % 17.94/18.33 [704=param(129,124),[], % 17.94/18.33 join(X10,complement(X11)) = complement(meet(complement(X10),X11))]. % 17.94/18.33 [705=demod(688),[704], % 17.94/18.33 meet(complement(meet(X10,X11)),complement(meet(complement(X11),X10))) = complement(X10)]. % 17.94/18.33 [730=demod(475),[704,704], % 17.94/18.33 complement(meet(complement(meet(X10,X11)),meet(complement(X12),join(complement(X11),X10)))) = join(X12,X11)]. % 17.94/18.33 [744=demod(634),[704,704], % 17.94/18.33 complement(meet(complement(X10),meet(complement(X11),meet(X12,X10)))) = top]. % 17.94/18.33 [750=demod(589),[704], % 17.94/18.33 complement(meet(complement(X10),meet(X10,X11))) = top]. % 17.94/18.33 [756=demod(701),[704,704,704,124], % 17.94/18.33 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X12,meet(complement(X10),X11)))]. % 17.94/18.33 [761=demod(702),[704,704,704,124], % 17.94/18.33 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X11,meet(complement(X10),X12)))]. % 17.94/18.33 [762=demod(750),[], % 17.94/18.33 complement(meet(complement(X10),meet(X10,X11))) = top]. % 17.94/18.33 [766=param(130,55),[130], % 17.94/18.33 meet(X10,complement(meet(X11,X12))) = meet(X10,complement(meet(X12,X11)))]. % 17.94/18.33 [770=param(704,14),[], % 17.94/18.33 join(complement(X11),X10) = complement(meet(complement(X10),X11))]. % 17.94/18.33 [774=demod(599),[770,55], % 17.94/18.33 complement(meet(X10,complement(converse(join(X11,converse(X10)))))) = top]. % 17.94/18.33 [777=demod(541),[770,55], % 17.94/18.33 complement(meet(one,complement(converse(composition(converse(X10),complement(X10)))))) = complement(one)]. % 17.94/18.33 [785=demod(689),[770], % 17.94/18.33 meet(complement(meet(X10,X11)),complement(meet(complement(X10),X11))) = complement(X11)]. % 17.94/18.33 [792=demod(82),[770,55], % 17.94/18.33 complement(meet(X10,complement(composition(X11,complement(composition(converse(X11),X10)))))) = complement(X10)]. % 17.94/18.33 [793=demod(15),[770,55], % 17.94/18.33 complement(meet(X10,complement(composition(converse(X11),complement(composition(X11,X10)))))) = complement(X10)]. % 17.94/18.33 [796=demod(592),[770,55], % 17.94/18.33 complement(meet(composition(X10,X11),complement(composition(join(X10,X12),X11)))) = top]. % 17.94/18.33 [827=demod(730),[770], % 17.94/18.33 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = join(X12,X11)]. % 17.94/18.33 [835=param(704,30),[], % 17.94/18.33 converse(join(X10,converse(complement(X11)))) = complement(meet(complement(converse(X10)),X11))]. % 17.94/18.33 [838=param(66,704),[704,704], % 17.94/18.33 complement(meet(complement(sk1),meet(complement(one),X10))) = complement(meet(complement(one),X10))]. % 17.94/18.33 [840=param(704,124),[], % 17.94/18.33 join(X10,X11) = complement(meet(complement(X10),complement(X11)))]. % 17.94/18.33 [841=demod(1),[840], % 17.94/18.33 complement(meet(complement(sk1),complement(one))) = one]. % 17.94/18.33 [860=demod(188),[840,840], % 17.94/18.33 complement(meet(complement(X10),complement(converse(composition(converse(X10),converse(X11)))))) = composition(complement(meet(complement(X11),complement(one))),X10)]. % 17.94/18.33 [864=demod(318),[840], % 17.94/18.33 complement(meet(complement(X10),complement(converse(complement(converse(X10)))))) = top]. % 17.94/18.33 [866=demod(835),[840], % 17.94/18.33 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),complement(converse(complement(X11))))))]. % 17.94/18.33 [873=demod(774),[840], % 17.94/18.33 complement(meet(X10,complement(converse(complement(meet(complement(X11),complement(converse(X10)))))))) = top]. % 17.94/18.33 [879=demod(37),[840,840], % 17.94/18.33 converse(complement(meet(complement(X10),complement(converse(X11))))) = complement(meet(complement(X11),complement(converse(X10))))]. % 17.94/18.33 [899=demod(827),[840], % 17.94/18.33 complement(meet(complement(meet(X10,X11)),meet(complement(X12),complement(meet(complement(X10),X11))))) = complement(meet(complement(X12),complement(X11)))]. % 17.94/18.33 [930=demod(201),[840,840], % 17.94/18.33 composition(converse(complement(meet(complement(X10),complement(one)))),X11) = complement(meet(complement(X11),complement(composition(converse(X10),X11))))]. % 17.94/18.33 [936=demod(207),[840], % 17.94/18.33 converse(complement(meet(complement(X10),complement(composition(X10,converse(sk1)))))) = converse(X10)]. % 17.94/18.33 [939=demod(196),[840], % 17.94/18.33 complement(meet(complement(X10),complement(composition(sk1,X10)))) = X10]. % 17.94/18.33 [972=demod(796),[840], % 17.94/18.33 complement(meet(composition(X10,X11),complement(composition(complement(meet(complement(X10),complement(X12))),X11)))) = top]. % 17.94/18.33 [1073=demod(532),[840], % 17.94/18.33 complement(meet(complement(X10),complement(meet(X11,X10)))) = X10]. % 17.94/18.33 [1102=param(124,841),[], % 17.94/18.33 meet(complement(sk1),complement(one)) = complement(one)]. % 17.94/18.33 [1114=param(2,762),[55,125], % 17.94/18.33 meet(complement(X10),meet(X10,X11)) = zero]. % 17.94/18.33 [1116=param(1114,124),[], % 17.94/18.33 meet(X10,meet(complement(X10),X11)) = zero]. % 17.94/18.33 [1118=param(1116,55),[], % 17.94/18.33 meet(X10,meet(X11,complement(X10))) = zero]. % 17.94/18.33 [1154=param(124,1073),[], % 17.94/18.33 meet(complement(X10),complement(meet(X11,X10))) = complement(X10)]. % 17.94/18.33 [1155=param(1154,55),[], % 17.94/18.33 meet(complement(X10),complement(meet(X10,X11))) = complement(X10)]. % 17.94/18.33 [1156=param(1154,609),[55], % 17.94/18.33 meet(complement(X10),complement(composition(top,X10))) = complement(composition(top,X10))]. % 17.94/18.33 [1169=param(124,939),[], % 17.94/18.33 meet(complement(X10),complement(composition(sk1,X10))) = complement(X10)]. % 17.94/18.33 [1177=param(1169,124),[124], % 17.94/18.33 meet(X10,complement(composition(sk1,complement(X10)))) = X10]. % 17.94/18.33 [1179=param(1154,1169),[124,124,55,124], % 17.94/18.33 meet(X10,composition(sk1,X10)) = composition(sk1,X10)]. % 17.94/18.33 [1209=param(2,744),[55,125], % 17.94/18.33 meet(complement(X10),meet(complement(X11),meet(X12,X10))) = zero]. % 17.94/18.33 [1213=param(1209,124),[], % 17.94/18.33 meet(complement(X10),meet(X11,meet(X12,X10))) = zero]. % 17.94/18.33 [1214=param(1213,55),[], % 17.94/18.33 meet(complement(X10),meet(meet(X11,X10),X12)) = zero]. % 17.94/18.33 [1215=param(1213,55),[], % 17.94/18.33 meet(complement(X10),meet(X11,meet(X10,X12))) = zero]. % 17.94/18.33 [1227=param(1213,1155),[124], % 17.94/18.33 meet(meet(X10,X11),meet(X12,complement(X10))) = zero]. % 17.94/18.33 [1229=param(1213,1169),[124], % 17.94/18.33 meet(composition(sk1,X10),meet(X11,complement(X10))) = zero]. % 17.94/18.33 [1230=param(1213,1177),[124], % 17.94/18.33 meet(composition(sk1,complement(X10)),meet(X11,X10)) = zero]. % 17.94/18.33 [1244=param(1230,1155),[124,55], % 17.94/18.33 meet(complement(X10),composition(sk1,meet(X10,X11))) = zero]. % 17.94/18.33 [1256=param(124,756),[124], % 17.94/18.33 meet(X10,meet(complement(X11),X12)) = meet(complement(X11),meet(X12,X10))]. % 17.94/18.33 [1297=param(761,124),[124], % 17.94/18.33 complement(meet(X10,meet(X11,X12))) = complement(meet(X11,meet(X10,X12)))]. % 17.94/18.33 [1300=param(124,761),[124], % 17.94/18.33 meet(X10,meet(complement(X11),X12)) = meet(complement(X11),meet(X10,X12))]. % 17.94/18.33 [1340=param(766,705),[], % 17.94/18.33 meet(complement(meet(X10,X11)),complement(meet(X10,complement(X11)))) = complement(X10)]. % 17.94/18.33 [1356=param(777,25),[26], % 17.94/18.33 complement(meet(one,complement(converse(complement(one))))) = complement(one)]. % 17.94/18.33 [1358=param(124,1356),[124], % 17.94/18.33 meet(one,complement(converse(complement(one)))) = one]. % 17.94/18.33 [1360=param(1154,1358),[124,55,124], % 17.94/18.33 meet(complement(one),converse(complement(one))) = converse(complement(one))]. % 17.94/18.33 [1369=param(785,766),[], % 17.94/18.33 meet(complement(meet(X11,X10)),complement(meet(X10,complement(X11)))) = complement(X10)]. % 17.94/18.33 [1387=param(124,792),[124], % 17.94/18.33 meet(X10,complement(composition(X11,complement(composition(converse(X11),X10))))) = X10]. % 17.94/18.33 [1393=param(124,793),[124], % 17.94/18.33 meet(X10,complement(composition(converse(X11),complement(composition(X11,X10))))) = X10]. % 17.94/18.33 [1499=param(124,838),[124], % 17.94/18.33 meet(complement(sk1),meet(complement(one),X10)) = meet(complement(one),X10)]. % 17.94/18.33 [1528=param(1227,1169),[55], % 17.94/18.33 meet(complement(X10),meet(composition(sk1,X10),X11)) = zero]. % 17.94/18.33 [1668=param(2,864),[55,125], % 17.94/18.33 meet(complement(X10),complement(converse(complement(converse(X10))))) = zero]. % 17.94/18.33 [1677=param(866,314),[124,124,7], % 17.94/18.33 converse(complement(meet(complement(X10),complement(converse(complement(converse(complement(X10)))))))) = converse(X10)]. % 17.94/18.33 [1694=param(1499,314),[1102,124,25,1360], % 17.94/18.33 converse(complement(one)) = complement(one)]. % 17.94/18.33 [1697=param(1155,1499),[124,124], % 17.94/18.33 meet(sk1,complement(meet(complement(one),X10))) = sk1]. % 17.94/18.33 [1698=param(1499,1179),[1179], % 17.94/18.33 meet(complement(sk1),composition(sk1,complement(one))) = composition(sk1,complement(one))]. % 17.94/18.33 [1715=param(860,1694),[124,2,148], % 17.94/18.33 complement(meet(complement(X10),complement(converse(composition(converse(X10),complement(one)))))) = composition(top,X10)]. % 17.94/18.33 [1718=param(1697,55),[], % 17.94/18.33 meet(sk1,complement(meet(X10,complement(one)))) = sk1]. % 17.94/18.33 [1726=param(1718,866),[124,25], % 17.94/18.33 meet(sk1,converse(complement(meet(complement(X10),complement(one))))) = sk1]. % 17.94/18.33 [1732=param(2,873),[55,125], % 17.94/18.33 meet(X10,complement(converse(complement(meet(complement(X11),complement(converse(X10))))))) = zero]. % 17.94/18.33 [1751=param(1726,124),[], % 17.94/18.33 meet(sk1,converse(complement(meet(X10,complement(one))))) = sk1]. % 17.94/18.33 [1752=param(1751,55),[], % 17.94/18.33 meet(sk1,converse(complement(meet(complement(one),X10)))) = sk1]. % 17.94/18.33 [1757=param(879,1694),[124,55,124], % 17.94/18.33 complement(meet(one,complement(converse(X10)))) = converse(complement(meet(one,complement(X10))))]. % 17.94/18.33 [1771=param(124,1757),[], % 17.94/18.33 meet(one,complement(converse(X10))) = complement(converse(complement(meet(one,complement(X10)))))]. % 17.94/18.33 [1916=param(899,1155),[124,55,124], % 17.94/18.33 complement(meet(X10,complement(meet(X10,X11)))) = complement(meet(X10,complement(X11)))]. % 17.94/18.33 [1920=param(124,1916),[124], % 17.94/18.33 meet(X10,complement(meet(X10,X11))) = meet(X10,complement(X11))]. % 17.94/18.33 [1921=param(1920,55),[], % 17.94/18.33 meet(X10,complement(meet(X11,X10))) = meet(X10,complement(X11))]. % 17.94/18.33 [1994=param(1920,1668),[148,55,125,124], % 17.94/18.33 meet(complement(X10),converse(complement(converse(X10)))) = complement(X10)]. % 17.94/18.33 [2000=param(1920,1771),[124,124], % 17.94/18.33 meet(one,converse(complement(meet(one,complement(X10))))) = meet(one,converse(X10))]. % 17.94/18.33 [2011=param(1154,1994),[124,55], % 17.94/18.33 meet(X10,complement(converse(complement(converse(X10))))) = complement(converse(complement(converse(X10))))]. % 17.94/18.33 [2012=demod(1677),[2011,124,7], % 17.94/18.33 complement(converse(complement(X10))) = converse(X10)]. % 17.94/18.33 [2031=demod(1732),[2012], % 17.94/18.33 meet(X10,converse(meet(complement(X11),complement(converse(X10))))) = zero]. % 17.94/18.33 [2070=demod(1771),[2012], % 17.94/18.33 meet(one,complement(converse(X10))) = converse(meet(one,complement(X10)))]. % 17.94/18.33 [2075=demod(866),[2012], % 17.94/18.33 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 17.94/18.33 [2079=param(2012,124),[], % 17.94/18.33 complement(converse(X10)) = converse(complement(X10))]. % 17.94/18.33 [2080=demod(2075),[2079], % 17.94/18.33 complement(meet(converse(complement(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 17.94/18.33 [2082=demod(2070),[2079], % 17.94/18.33 meet(one,converse(complement(X10))) = converse(meet(one,complement(X10)))]. % 17.94/18.33 [2083=demod(2000),[2082,1920,124], % 17.94/18.33 meet(one,converse(X10)) = converse(meet(one,X10))]. % 17.94/18.33 [2086=demod(2031),[2079], % 17.94/18.33 meet(X10,converse(meet(complement(X11),converse(complement(X10))))) = zero]. % 17.94/18.33 [2169=demod(1715),[2079], % 17.94/18.33 complement(meet(complement(X10),converse(complement(composition(converse(X10),complement(one)))))) = composition(top,X10)]. % 17.94/18.33 [2281=param(1155,2083),[2079], % 17.94/18.33 meet(complement(one),converse(complement(meet(one,X10)))) = complement(one)]. % 17.94/18.33 [2292=param(1244,2083),[], % 17.94/18.33 meet(complement(one),composition(sk1,converse(meet(one,X10)))) = zero]. % 17.94/18.33 [2320=param(1921,1215),[148,55,125,124,55], % 17.94/18.33 meet(X11,meet(X10,meet(X11,X12))) = meet(X10,meet(X11,X12))]. % 17.94/18.33 [2325=param(1921,1229),[148,55,125,55,-1256], % 17.94/18.33 meet(X10,complement(X11)) = meet(complement(X11),meet(complement(composition(sk1,X11)),X10))]. % 17.94/18.33 [2331=param(1921,1244),[148,55,125,124,55], % 17.94/18.33 meet(X10,composition(sk1,meet(X10,X11))) = composition(sk1,meet(X10,X11))]. % 17.94/18.33 [2340=param(1921,1528),[148,55,125,124,55], % 17.94/18.33 meet(X10,meet(composition(sk1,X10),X11)) = meet(composition(sk1,X10),X11)]. % 17.94/18.33 [2409=param(930,1102),[124,25,26], % 17.94/18.33 complement(meet(complement(X10),complement(composition(converse(sk1),X10)))) = X10]. % 17.94/18.33 [2473=param(2281,657),[], % 17.94/18.33 meet(complement(one),converse(complement(meet(sk1,X10)))) = complement(one)]. % 17.94/18.33 [2478=param(7,936),[7], % 17.94/18.33 complement(meet(complement(X10),complement(composition(X10,converse(sk1))))) = X10]. % 17.94/18.33 [2525=param(1214,2473),[2079,124], % 17.94/18.33 meet(converse(meet(sk1,X10)),meet(complement(one),X11)) = zero]. % 17.94/18.33 [2694=param(972,2),[148], % 17.94/18.33 complement(meet(composition(X10,X11),complement(composition(top,X11)))) = top]. % 17.94/18.33 [2696=param(2,2694),[55,125], % 17.94/18.33 meet(composition(X10,X11),complement(composition(top,X11))) = zero]. % 17.94/18.33 [2700=param(2696,55),[], % 17.94/18.33 meet(complement(composition(top,X10)),composition(X11,X10)) = zero]. % 17.94/18.33 [2707=param(1920,2696),[148,55,125,124], % 17.94/18.33 meet(composition(X10,X11),composition(top,X11)) = composition(X10,X11)]. % 17.94/18.33 [2714=param(2707,55),[], % 17.94/18.33 meet(composition(top,X11),composition(X10,X11)) = composition(X10,X11)]. % 17.94/18.33 [2913=param(124,2478),[], % 17.94/18.33 meet(complement(X10),complement(composition(X10,converse(sk1)))) = complement(X10)]. % 17.94/18.33 [2921=param(1154,2913),[124,124,55,124], % 17.94/18.33 meet(X10,composition(X10,converse(sk1))) = composition(X10,converse(sk1))]. % 17.94/18.33 [2932=param(2921,19),[7], % 17.94/18.33 meet(X10,converse(composition(sk1,converse(X10)))) = composition(X10,converse(sk1))]. % 17.94/18.33 [2962=param(2921,2700),[21,307,2079,-5], % 17.94/18.33 converse(composition(sk1,complement(composition(sk1,top)))) = zero]. % 17.94/18.33 [2968=param(7,2962),[250], % 17.94/18.33 composition(sk1,complement(composition(sk1,top))) = zero]. % 17.94/18.33 [3206=param(124,2409),[], % 17.94/18.33 meet(complement(X10),complement(composition(converse(sk1),X10))) = complement(X10)]. % 17.94/18.33 [3218=param(1154,3206),[124,124,55,124], % 17.94/18.33 meet(X10,composition(converse(sk1),X10)) = composition(converse(sk1),X10)]. % 17.94/18.33 [3238=param(3218,5),[], % 17.94/18.33 meet(converse(X10),converse(composition(X10,sk1))) = composition(converse(sk1),converse(X10))]. % 17.94/18.33 [3275=param(1752,3218),[], % 17.94/18.33 meet(sk1,converse(complement(composition(converse(sk1),complement(one))))) = sk1]. % 17.94/18.33 [4134=param(1921,1116),[148,55,125,2325,-1300,650], % 17.94/18.33 meet(complement(X10),meet(complement(composition(sk1,X10)),X11)) = meet(complement(X10),X11)]. % 17.94/18.33 [5149=param(1256,55),[], % 17.94/18.33 meet(meet(complement(X10),X11),X12) = meet(complement(X10),meet(X11,X12))]. % 17.94/18.33 [5165=param(1256,55),[], % 17.94/18.33 meet(X10,meet(X11,complement(X12))) = meet(complement(X12),meet(X11,X10))]. % 17.94/18.33 [5645=param(124,1297),[124], % 17.94/18.33 meet(X10,meet(X11,X12)) = meet(X11,meet(X10,X12))]. % 17.94/18.33 [5803=demod(2525),[], % 17.94/18.33 meet(converse(meet(sk1,X10)),meet(complement(one),X11)) = zero]. % 17.94/18.33 [6264=param(1369,3275),[2325,4134,2169,2079,124], % 17.94/18.33 meet(complement(sk1),composition(top,sk1)) = converse(composition(converse(sk1),complement(one)))]. % 17.94/18.33 [6304=param(1393,2968),[148,-328,7,2079], % 17.94/18.33 meet(complement(composition(sk1,top)),converse(complement(composition(top,sk1)))) = complement(composition(sk1,top))]. % 17.94/18.33 [6359=param(5149,124),[124], % 17.94/18.33 meet(meet(X10,X11),X12) = meet(X10,meet(X11,X12))]. % 17.94/18.33 [6701=param(6359,6264),[], % 17.94/18.33 meet(converse(composition(converse(sk1),complement(one))),X10) = meet(complement(sk1),meet(composition(top,sk1),X10))]. % 17.94/18.33 [9627=param(2086,124),[], % 17.94/18.33 meet(X10,converse(meet(X11,converse(complement(X10))))) = zero]. % 17.94/18.33 [9630=param(9627,124),[], % 17.94/18.33 meet(complement(X10),converse(meet(X11,converse(X10)))) = zero]. % 17.94/18.33 [9652=param(9627,2079),[7], % 17.94/18.33 meet(converse(X10),converse(meet(X11,complement(X10)))) = zero]. % 17.94/18.33 [9685=param(9652,1155),[55], % 17.94/18.33 meet(converse(complement(X10)),converse(meet(X10,X11))) = zero]. % 17.94/18.33 [9712=param(9685,1156),[124], % 17.94/18.33 meet(converse(X10),converse(complement(composition(top,X10)))) = zero]. % 17.94/18.33 [9724=param(1921,9685),[148,55,125,2079,124,55], % 17.94/18.33 meet(converse(X10),converse(meet(X10,X11))) = converse(meet(X10,X11))]. % 17.94/18.33 [9734=param(9685,3238),[2079,7], % 17.94/18.33 meet(complement(X10),converse(composition(converse(sk1),converse(X10)))) = zero]. % 17.94/18.33 [9795=param(9712,21),[7,307,2079,7], % 17.94/18.33 meet(X10,complement(composition(X10,top))) = zero]. % 17.94/18.33 [9833=param(1920,9712),[148,55,125,2079,124], % 17.94/18.33 meet(converse(X10),converse(composition(top,X10))) = converse(X10)]. % 17.94/18.33 [9856=param(1920,9795),[148,142,124], % 17.94/18.33 meet(X10,composition(X10,top)) = X10]. % 17.94/18.33 [9857=param(1921,9795),[148,55,125,55], % 17.94/18.33 meet(complement(X10),complement(composition(X10,top))) = complement(composition(X10,top))]. % 17.94/18.33 [9882=param(6359,9856),[], % 17.94/18.33 meet(X10,meet(composition(X10,top),X11)) = meet(X10,X11)]. % 17.94/18.33 [10011=param(9882,2320),[650], % 17.94/18.33 meet(composition(X10,top),meet(X10,X11)) = meet(X10,X11)]. % 17.94/18.33 [10356=param(1921,9630),[148,55,125,124,55], % 17.94/18.33 meet(X11,converse(meet(X10,converse(X11)))) = converse(meet(X10,converse(X11)))]. % 17.94/18.33 [10485=param(9724,3238),[7,3238], % 17.94/18.33 meet(X10,converse(composition(converse(sk1),converse(X10)))) = converse(composition(converse(sk1),converse(X10)))]. % 17.94/18.33 [10495=param(9724,10011),[10011], % 17.94/18.33 meet(converse(composition(X10,top)),converse(meet(X10,X11))) = converse(meet(X10,X11))]. % 17.94/18.33 [10880=param(9734,5),[7,7], % 17.94/18.33 meet(complement(X10),composition(X10,sk1)) = zero]. % 17.94/18.33 [10929=param(1921,10880),[148,55,125,124,55], % 17.94/18.33 meet(X10,composition(X10,sk1)) = composition(X10,sk1)]. % 17.94/18.33 [10952=param(10929,2700),[-19], % 17.94/18.33 converse(composition(converse(sk1),converse(complement(composition(top,sk1))))) = zero]. % 17.94/18.33 [10960=param(5803,10929),[-19,1694,55,6701], % 17.94/18.33 meet(complement(sk1),meet(composition(top,sk1),converse(meet(sk1,X10)))) = zero]. % 17.94/18.33 [10963=param(6359,10929),[], % 17.94/18.33 meet(X10,meet(composition(X10,sk1),X11)) = meet(composition(X10,sk1),X11)]. % 17.94/18.33 [11731=param(7,10952),[250], % 17.94/18.33 composition(converse(sk1),converse(complement(composition(top,sk1)))) = zero]. % 17.94/18.33 [11739=param(1387,11731),[148,2325,4134,6304], % 17.94/18.33 converse(complement(composition(top,sk1))) = complement(composition(sk1,top))]. % 17.94/18.33 [11757=param(7,11739),[], % 17.94/18.33 complement(composition(top,sk1)) = converse(complement(composition(sk1,top)))]. % 17.94/18.33 [11764=param(124,11757),[2079,124], % 17.94/18.33 composition(top,sk1) = converse(composition(sk1,top))]. % 17.94/18.33 [11795=demod(10960),[11764,10495], % 17.94/18.33 meet(complement(sk1),converse(meet(sk1,X10))) = zero]. % 17.94/18.33 [11817=demod(6264),[11764], % 17.94/18.33 meet(complement(sk1),converse(composition(sk1,top))) = converse(composition(converse(sk1),complement(one)))]. % 17.94/18.33 [11841=param(9833,11764),[7], % 17.94/18.33 meet(converse(sk1),composition(sk1,top)) = converse(sk1)]. % 17.94/18.33 [11853=param(1369,11841),[2079,2079,55,2080,11817,2079,7], % 17.94/18.33 meet(converse(complement(sk1)),complement(composition(converse(sk1),complement(one)))) = complement(composition(sk1,top))]. % 17.94/18.33 [11868=param(11795,126),[55], % 17.94/18.33 meet(converse(sk1),complement(sk1)) = zero]. % 17.94/18.33 [11900=param(1920,11868),[148,55,125,124,55], % 17.94/18.33 meet(sk1,converse(sk1)) = converse(sk1)]. % 17.94/18.33 [11912=param(9724,11900),[7,55,11900,11900,7], % 17.94/18.33 converse(sk1) = sk1]. % 17.94/18.33 [11913=demod(11853),[11912], % 17.94/18.33 meet(converse(complement(sk1)),complement(composition(sk1,complement(one)))) = complement(composition(sk1,top))]. % 17.94/18.33 [12092=demod(10485),[11912,11912], % 17.94/18.33 meet(X10,converse(composition(sk1,converse(X10)))) = converse(composition(sk1,converse(X10)))]. % 17.94/18.33 [12176=demod(2932),[12092,11912], % 17.94/18.33 converse(composition(sk1,converse(X10))) = composition(X10,sk1)]. % 17.94/18.33 [12185=param(2079,11912),[], % 17.94/18.33 converse(complement(sk1)) = complement(sk1)]. % 17.94/18.33 [12186=demod(11913),[12185], % 17.94/18.33 meet(complement(sk1),complement(composition(sk1,complement(one)))) = complement(composition(sk1,top))]. % 17.94/18.33 [13921=param(10963,2714),[125,-12176,307], % 17.94/18.33 meet(converse(composition(sk1,top)),composition(X10,sk1)) = composition(X10,sk1)]. % 17.94/18.33 [13959=param(9685,13921),[2079,7], % 17.94/18.33 meet(complement(composition(sk1,top)),converse(composition(X10,sk1))) = zero]. % 17.94/18.33 [13969=param(13959,22),[11912,7], % 17.94/18.33 meet(complement(composition(sk1,top)),composition(sk1,X10)) = zero]. % 17.94/18.33 [13988=param(1921,13969),[148,55,125,124], % 17.94/18.33 meet(composition(sk1,X10),composition(sk1,top)) = composition(sk1,X10)]. % 17.94/18.33 [13990=param(13988,55),[], % 17.94/18.33 meet(composition(sk1,top),composition(sk1,X10)) = composition(sk1,X10)]. % 17.94/18.33 [14451=param(1340,1698),[12186,124,55,124], % 17.94/18.33 meet(composition(sk1,top),complement(composition(sk1,complement(one)))) = sk1]. % 17.94/18.33 [14461=param(1920,14451),[2325,4134,124,13990], % 17.94/18.33 meet(complement(sk1),composition(sk1,top)) = composition(sk1,complement(one))]. % 17.94/18.33 [14472=param(6359,14461),[], % 17.94/18.33 meet(composition(sk1,complement(one)),X10) = meet(complement(sk1),meet(composition(sk1,top),X10))]. % 17.96/18.33 [14577=param(1387,11912),[], % 17.96/18.33 meet(X10,complement(composition(sk1,complement(composition(sk1,X10))))) = X10]. % 17.96/18.33 [14604=param(1118,14577),[55], % 17.96/18.33 meet(X10,composition(sk1,complement(composition(sk1,X10)))) = zero]. % 17.96/18.33 [14646=param(14604,13990),[], % 17.96/18.33 composition(sk1,complement(composition(sk1,composition(sk1,top)))) = zero]. % 17.96/18.33 [14667=param(1393,14646),[11912,148,55,1169], % 17.96/18.33 complement(composition(sk1,composition(sk1,top))) = complement(composition(sk1,top))]. % 17.96/18.33 [14668=param(124,14667),[124], % 17.96/18.33 composition(sk1,composition(sk1,top)) = composition(sk1,top)]. % 17.96/18.33 [22697=param(5645,2340),[], % 17.96/18.33 meet(composition(sk1,X10),meet(X10,X11)) = meet(composition(sk1,X10),X11)]. % 17.96/18.33 [23136=param(22697,2292),[55,374,14472,13990], % 17.96/18.33 meet(complement(sk1),composition(sk1,converse(meet(one,X10)))) = zero]. % 17.96/18.33 [23215=param(23136,10356),[25,7], % 17.96/18.33 meet(complement(sk1),composition(sk1,meet(X10,one))) = zero]. % 17.96/18.33 [23228=param(23215,2331),[55], % 17.96/18.33 composition(sk1,meet(one,complement(sk1))) = zero]. % 17.96/18.33 [23238=param(1393,23228),[11912,148,2325,14668,5165,-1300,9857,632], % 17.96/18.33 meet(one,complement(composition(sk1,top))) = meet(one,complement(sk1))]. % 17.96/18.33 [23239=param(75,23238),[16], % 17.96/18.33 thmtrue = thmfalse]. % 17.96/18.33 % SZS output end CNFRefutation % 17.96/18.33 Space: 100957 KB %------------------------------------------------------------------------------