%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : REL041-2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n004.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:54 EDT 2022 % Result : Unsatisfiable 18.77s 19.21s % Output : CNFRefutation 18.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : REL041-2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n004.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 08:57:07 EDT 2022 % 0.12/0.33 % CPUTime : % 18.77/19.21 Theorem Proved. % 18.77/19.21 % SZS status Unsatisfiable % 18.77/19.21 % SZS output start CNFRefutation % 18.77/19.21 [1=axiom,[], % 18.77/19.21 join(composition(converse(sk1),sk1),one) = one]. % 18.77/19.21 [3=axiom,[], % 18.77/19.21 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)]. % 18.77/19.21 [5=axiom,[], % 18.77/19.21 meet(X10,complement(X10)) = zero]. % 18.77/19.21 [6=axiom,[], % 18.77/19.21 join(X10,complement(X10)) = top]. % 18.77/19.21 [7=axiom,[], % 18.77/19.21 join(composition(converse(X10),complement(composition(X10,X11))),complement(X11)) = complement(X11)]. % 18.77/19.21 [8=axiom,[], % 18.77/19.21 converse(composition(X10,X11)) = composition(converse(X11),converse(X10))]. % 18.77/19.21 [9=axiom,[], % 18.77/19.21 join(converse(X10),converse(X11)) = converse(join(X10,X11))]. % 18.77/19.21 [10=axiom,[], % 18.77/19.21 converse(converse(X10)) = X10]. % 18.77/19.21 [11=axiom,[], % 18.77/19.21 join(composition(X10,X12),composition(X11,X12)) = composition(join(X10,X11),X12)]. % 18.77/19.21 [12=axiom,[], % 18.77/19.21 composition(X10,one) = X10]. % 18.77/19.21 [13=axiom,[], % 18.77/19.21 composition(composition(X10,X11),X12) = composition(X10,composition(X11,X12))]. % 18.77/19.21 [14=axiom,[], % 18.77/19.21 complement(join(complement(X10),complement(X11))) = meet(X10,X11)]. % 18.77/19.21 [15=axiom,[14], % 18.77/19.21 join(meet(X10,X11),complement(join(complement(X10),X11))) = X10]. % 18.77/19.21 [16=axiom,[], % 18.77/19.21 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 18.77/19.21 [17=axiom,[], % 18.77/19.21 join(X10,X11) = join(X11,X10)]. % 18.77/19.21 [18=demod(1),[17], % 18.77/19.21 join(one,composition(converse(sk1),sk1)) = one]. % 18.77/19.21 [19=demod(7),[17], % 18.77/19.21 join(complement(X10),composition(converse(X11),complement(composition(X11,X10)))) = complement(X10)]. % 18.77/19.21 [21=axiom,[], % 18.77/19.21 thtop(X10,X10) = thmfalse]. % 18.77/19.21 [22=axiom,[], % 18.77/19.21 thtop(meet(composition(sk1,sk2),composition(sk1,complement(sk2))),zero) = thmtrue]. % 18.77/19.21 [24=param(9,10),[], % 18.77/19.21 join(converse(X10),X11) = converse(join(X10,converse(X11)))]. % 18.77/19.21 [26=param(10,8),[], % 18.77/19.21 converse(composition(converse(X10),converse(X11))) = composition(X11,X10)]. % 18.77/19.21 [28=param(8,12),[], % 18.77/19.21 composition(converse(one),converse(X10)) = converse(X10)]. % 18.77/19.21 [30=param(8,10),[], % 18.77/19.21 composition(converse(X10),X11) = converse(composition(converse(X11),X10))]. % 18.77/19.21 [32=param(28,10),[10], % 18.77/19.21 composition(converse(one),X10) = X10]. % 18.77/19.21 [33=param(32,12),[], % 18.77/19.21 converse(one) = one]. % 18.77/19.21 [34=demod(32),[33], % 18.77/19.21 composition(one,X10) = X10]. % 18.77/19.21 [36=param(11,34),[], % 18.77/19.21 join(X10,composition(X11,X10)) = composition(join(one,X11),X10)]. % 18.77/19.21 [37=param(11,34),[17], % 18.77/19.21 join(X10,composition(X11,X10)) = composition(join(X11,one),X10)]. % 18.77/19.21 [39=param(13,8),[], % 18.77/19.21 composition(converse(composition(X10,X11)),X12) = composition(converse(X11),composition(converse(X10),X12))]. % 18.77/19.21 [40=param(24,6),[], % 18.77/19.21 converse(join(X10,converse(complement(converse(X10))))) = top]. % 18.77/19.21 [42=param(24,17),[], % 18.77/19.21 converse(join(X10,converse(X11))) = join(X11,converse(X10))]. % 18.77/19.21 [49=param(14,6),[5], % 18.77/19.21 complement(top) = zero]. % 18.77/19.21 [53=param(14,17),[14], % 18.77/19.21 meet(X10,X11) = meet(X11,X10)]. % 18.77/19.21 [54=demod(3),[53,53], % 18.77/19.21 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))))]. % 18.77/19.21 [57=param(5,49),[53], % 18.77/19.21 meet(zero,top) = zero]. % 18.77/19.21 [59=param(14,49),[], % 18.77/19.21 complement(join(zero,complement(X10))) = meet(top,X10)]. % 18.77/19.21 [60=param(15,5),[14], % 18.77/19.21 join(zero,meet(X10,X10)) = X10]. % 18.77/19.21 [65=param(15,57),[17], % 18.77/19.21 join(zero,complement(join(top,complement(zero)))) = zero]. % 18.77/19.21 [82=param(19,33),[34,34], % 18.77/19.21 join(complement(X10),complement(X10)) = complement(X10)]. % 18.77/19.21 [83=param(19,49),[49], % 18.77/19.21 join(zero,composition(converse(X10),complement(composition(X10,top)))) = zero]. % 18.77/19.21 [88=param(14,82),[], % 18.77/19.21 meet(X10,X10) = complement(complement(X10))]. % 18.77/19.21 [90=demod(60),[88], % 18.77/19.21 join(zero,complement(complement(X10))) = X10]. % 18.77/19.21 [91=param(16,82),[], % 18.77/19.21 join(complement(X10),join(complement(X10),X11)) = join(complement(X10),X11)]. % 18.77/19.21 [92=param(82,49),[49,49], % 18.77/19.21 join(zero,zero) = zero]. % 18.77/19.21 [93=param(16,92),[], % 18.77/19.21 join(zero,join(zero,X10)) = join(zero,X10)]. % 18.77/19.21 [98=param(90,14),[], % 18.77/19.21 join(complement(X10),complement(X11)) = join(zero,complement(meet(X10,X11)))]. % 18.77/19.21 [117=param(93,17),[], % 18.77/19.21 join(zero,join(X10,zero)) = join(zero,X10)]. % 18.77/19.21 [118=param(93,90),[90], % 18.77/19.21 join(zero,X10) = X10]. % 18.77/19.21 [119=demod(83),[118], % 18.77/19.21 composition(converse(X10),complement(composition(X10,top))) = zero]. % 18.77/19.21 [120=demod(59),[118], % 18.77/19.21 meet(top,X10) = complement(complement(X10))]. % 18.77/19.21 [124=demod(65),[118], % 18.77/19.21 complement(join(top,complement(zero))) = zero]. % 18.77/19.21 [125=demod(90),[118], % 18.77/19.21 complement(complement(X10)) = X10]. % 18.77/19.21 [126=demod(120),[125], % 18.77/19.21 meet(top,X10) = X10]. % 18.77/19.21 [130=demod(98),[118], % 18.77/19.21 join(complement(X10),complement(X11)) = complement(meet(X10,X11))]. % 18.77/19.21 [132=demod(117),[118,118], % 18.77/19.21 join(X10,zero) = X10]. % 18.77/19.21 [134=param(132,24),[], % 18.77/19.21 converse(join(X10,converse(zero))) = converse(X10)]. % 18.77/19.21 [150=param(125,49),[], % 18.77/19.21 complement(zero) = top]. % 18.77/19.21 [151=demod(124),[150], % 18.77/19.21 complement(join(top,top)) = zero]. % 18.77/19.21 [166=param(36,18),[34,13], % 18.77/19.21 join(X10,composition(converse(sk1),composition(sk1,X10))) = X10]. % 18.77/19.21 [169=param(36,132),[34], % 18.77/19.21 join(X10,composition(zero,X10)) = X10]. % 18.77/19.21 [178=param(37,118),[-26], % 18.77/19.21 converse(composition(converse(zero),converse(join(X10,one)))) = composition(X10,zero)]. % 18.77/19.21 [185=param(6,151),[17,118], % 18.77/19.21 join(top,top) = top]. % 18.77/19.21 [186=param(16,185),[], % 18.77/19.21 join(top,join(top,X10)) = join(top,X10)]. % 18.77/19.21 [195=param(169,118),[], % 18.77/19.21 composition(zero,zero) = zero]. % 18.77/19.21 [196=param(13,195),[], % 18.77/19.21 composition(zero,composition(zero,X10)) = composition(zero,X10)]. % 18.77/19.21 [209=param(10,40),[], % 18.77/19.21 join(X10,converse(complement(converse(X10)))) = converse(top)]. % 18.77/19.21 [212=param(10,134),[10], % 18.77/19.21 join(X10,converse(zero)) = X10]. % 18.77/19.21 [215=param(212,118),[], % 18.77/19.21 converse(zero) = zero]. % 18.77/19.21 [218=demod(178),[215], % 18.77/19.21 converse(composition(zero,converse(join(X10,one)))) = composition(X10,zero)]. % 18.77/19.21 [224=param(8,215),[], % 18.77/19.21 composition(zero,converse(X10)) = converse(composition(X10,zero))]. % 18.77/19.21 [229=param(26,215),[], % 18.77/19.21 converse(composition(zero,converse(X10))) = composition(X10,zero)]. % 18.77/19.21 [272=param(36,209),[33], % 18.77/19.21 join(X10,composition(converse(complement(one)),X10)) = composition(converse(top),X10)]. % 18.77/19.21 [276=param(186,209),[209], % 18.77/19.21 join(top,converse(top)) = converse(top)]. % 18.77/19.21 [278=param(42,276),[10,276], % 18.77/19.21 converse(top) = top]. % 18.77/19.21 [281=demod(272),[278], % 18.77/19.21 join(X10,composition(converse(complement(one)),X10)) = composition(top,X10)]. % 18.77/19.21 [290=param(8,278),[], % 18.77/19.21 composition(top,converse(X10)) = converse(composition(X10,top))]. % 18.77/19.21 [297=param(26,278),[], % 18.77/19.21 converse(composition(top,converse(X10))) = composition(X10,top)]. % 18.77/19.21 [325=param(16,130),[], % 18.77/19.21 join(complement(meet(X10,X11)),X12) = join(complement(X10),join(complement(X11),X12))]. % 18.77/19.21 [329=param(130,125),[], % 18.77/19.21 join(X10,complement(X11)) = complement(meet(complement(X10),X11))]. % 18.77/19.21 [394=param(329,17),[], % 18.77/19.21 join(complement(X11),X10) = complement(meet(complement(X10),X11))]. % 18.77/19.21 [403=demod(91),[394,329,125,394], % 18.77/19.21 complement(meet(X10,meet(complement(X11),X10))) = complement(meet(complement(X11),X10))]. % 18.77/19.21 [408=demod(325),[394,394,329,125], % 18.77/19.21 complement(meet(complement(X10),meet(X11,X12))) = complement(meet(X11,meet(complement(X10),X12)))]. % 18.77/19.21 [414=param(36,329),[], % 18.77/19.21 join(X11,composition(complement(X10),X11)) = composition(complement(meet(complement(one),X10)),X11)]. % 18.77/19.21 [416=param(329,125),[], % 18.77/19.21 join(X10,X11) = complement(meet(complement(X10),complement(X11)))]. % 18.77/19.21 [422=demod(166),[416], % 18.77/19.21 complement(meet(complement(X10),complement(composition(converse(sk1),composition(sk1,X10))))) = X10]. % 18.77/19.21 [423=demod(281),[416], % 18.77/19.21 complement(meet(complement(X10),complement(composition(converse(complement(one)),X10)))) = composition(top,X10)]. % 18.77/19.21 [432=demod(414),[416], % 18.77/19.21 complement(meet(complement(X10),complement(composition(complement(X11),X10)))) = composition(complement(meet(complement(one),X11)),X10)]. % 18.77/19.21 [436=demod(54),[416], % 18.77/19.21 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))))]. % 18.77/19.21 [460=demod(218),[416], % 18.77/19.21 converse(composition(zero,converse(complement(meet(complement(X10),complement(one)))))) = composition(X10,zero)]. % 18.77/19.21 [581=param(119,10),[-297,10], % 18.77/19.21 composition(X10,complement(converse(composition(top,X10)))) = zero]. % 18.77/19.21 [585=param(119,215),[], % 18.77/19.21 composition(zero,complement(composition(zero,top))) = zero]. % 18.77/19.21 [586=param(119,278),[], % 18.77/19.21 composition(top,complement(composition(top,top))) = zero]. % 18.77/19.22 [587=param(13,586),[], % 18.77/19.22 composition(top,composition(complement(composition(top,top)),X10)) = composition(zero,X10)]. % 18.77/19.22 [599=param(581,586),[215,150,-297], % 18.77/19.22 converse(composition(top,converse(complement(composition(top,top))))) = zero]. % 18.77/19.22 [624=param(224,290),[-229,10], % 18.77/19.22 composition(zero,composition(top,converse(X10))) = composition(zero,converse(composition(X10,top)))]. % 18.77/19.22 [632=param(10,599),[215], % 18.77/19.22 composition(top,converse(complement(composition(top,top)))) = zero]. % 18.77/19.22 [636=param(39,632),[215,10,278], % 18.77/19.22 composition(complement(composition(top,top)),composition(top,X10)) = composition(zero,X10)]. % 18.77/19.22 [712=param(587,297),[632,215,-229,278], % 18.77/19.22 converse(composition(zero,top)) = composition(zero,top)]. % 18.77/19.22 [714=param(587,636),[], % 18.77/19.22 composition(top,composition(zero,X10)) = composition(zero,composition(top,X10))]. % 18.77/19.22 [726=param(714,581),[-229,278,712,-229,278,712,712], % 18.77/19.22 composition(zero,composition(top,complement(composition(zero,top)))) = composition(zero,top)]. % 18.77/19.22 [728=param(636,714),[196], % 18.77/19.22 composition(complement(composition(top,top)),composition(zero,composition(top,X10))) = composition(zero,X10)]. % 18.77/19.22 [763=param(403,5),[125,125,53,5,150], % 18.77/19.22 complement(meet(X10,zero)) = top]. % 18.77/19.22 [768=param(5,763),[53,126], % 18.77/19.22 meet(X10,zero) = zero]. % 18.77/19.22 [769=param(768,53),[], % 18.77/19.22 meet(zero,X10) = zero]. % 18.77/19.22 [797=param(408,5),[768,150,125], % 18.77/19.22 complement(meet(complement(X10),meet(X11,X10))) = top]. % 18.77/19.22 [800=param(5,797),[53,126], % 18.77/19.22 meet(complement(X10),meet(X11,X10)) = zero]. % 18.77/19.22 [803=param(800,125),[], % 18.77/19.22 meet(X10,meet(X11,complement(X10))) = zero]. % 18.77/19.22 [860=param(125,422),[], % 18.77/19.22 meet(complement(X10),complement(composition(converse(sk1),composition(sk1,X10)))) = complement(X10)]. % 18.77/19.22 [871=param(423,49),[30,278,769,150], % 18.77/19.22 composition(top,top) = top]. % 18.77/19.22 [872=demod(728),[871,49,196], % 18.77/19.22 composition(zero,composition(top,X10)) = composition(zero,X10)]. % 18.77/19.22 [878=demod(624),[872], % 18.77/19.22 composition(zero,converse(composition(X10,top))) = composition(zero,converse(X10))]. % 18.77/19.22 [879=demod(726),[872,585], % 18.77/19.22 composition(zero,top) = zero]. % 18.77/19.22 [911=param(224,432),[150,-229,126,125,10], % 18.77/19.22 composition(zero,converse(complement(meet(complement(one),X10)))) = composition(zero,converse(complement(X10)))]. % 18.77/19.22 [917=param(878,432),[49,-297,769,150,278,879,911], % 18.77/19.22 composition(zero,converse(complement(X10))) = zero]. % 18.77/19.22 [918=demod(460),[917,215], % 18.77/19.22 composition(X10,zero) = zero]. % 18.77/19.22 [3052=param(803,860),[53], % 18.77/19.22 meet(complement(X10),composition(converse(sk1),composition(sk1,X10))) = zero]. % 18.77/19.22 [3168=param(3052,125),[], % 18.77/19.22 meet(X10,composition(converse(sk1),composition(sk1,complement(X10)))) = zero]. % 18.77/19.22 [20861=param(436,3168),[918,53,769,150,53,126,125,3168,918,53,769], % 18.77/19.22 meet(composition(sk1,X10),composition(sk1,complement(X10))) = zero]. % 18.77/19.22 [20862=param(22,20861),[21], % 18.77/19.22 thmtrue = thmfalse]. % 18.77/19.22 % SZS output end CNFRefutation % 18.77/19.22 Space: 100231 KB %------------------------------------------------------------------------------