%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : REL012-2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n014.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:12 EDT 2022 % Result : Unsatisfiable 1.49s 1.91s % Output : CNFRefutation 1.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : REL012-2 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n014.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:22:06 EDT 2022 % 0.12/0.33 % CPUTime : % 1.49/1.91 Theorem Proved. % 1.49/1.91 % SZS status Unsatisfiable % 1.49/1.91 % SZS output start CNFRefutation % 1.49/1.91 [4=axiom,[], % 1.49/1.91 meet(X10,complement(X10)) = zero]. % 1.49/1.91 [5=axiom,[], % 1.49/1.91 join(X10,complement(X10)) = top]. % 1.49/1.91 [6=axiom,[], % 1.49/1.91 join(composition(converse(X10),complement(composition(X10,X11))),complement(X11)) = complement(X11)]. % 1.49/1.91 [7=axiom,[], % 1.49/1.91 converse(composition(X10,X11)) = composition(converse(X11),converse(X10))]. % 1.49/1.91 [8=axiom,[], % 1.49/1.91 join(converse(X10),converse(X11)) = converse(join(X10,X11))]. % 1.49/1.91 [9=axiom,[], % 1.49/1.91 converse(converse(X10)) = X10]. % 1.49/1.91 [10=axiom,[], % 1.49/1.91 join(composition(X10,X12),composition(X11,X12)) = composition(join(X10,X11),X12)]. % 1.49/1.91 [11=axiom,[], % 1.49/1.91 composition(X10,one) = X10]. % 1.49/1.91 [13=axiom,[], % 1.49/1.91 complement(join(complement(X10),complement(X11))) = meet(X10,X11)]. % 1.49/1.91 [14=axiom,[13], % 1.49/1.91 join(meet(X10,X11),complement(join(complement(X10),X11))) = X10]. % 1.49/1.91 [15=axiom,[], % 1.49/1.91 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 1.49/1.91 [16=axiom,[], % 1.49/1.91 join(X10,X11) = join(X11,X10)]. % 1.49/1.91 [18=demod(6),[16], % 1.49/1.91 join(complement(X10),composition(converse(X11),complement(composition(X11,X10)))) = complement(X10)]. % 1.49/1.91 [19=axiom,[], % 1.49/1.91 thtop(X10,X10) = thmfalse]. % 1.49/1.91 [20=axiom,[16], % 1.49/1.91 thtop(join(complement(sk1),composition(complement(composition(sk1,sk2)),converse(sk2))),complement(sk1)) = thmtrue]. % 1.49/1.91 [22=param(8,9),[], % 1.49/1.91 join(converse(X10),X11) = converse(join(X10,converse(X11)))]. % 1.49/1.91 [23=param(22,5),[], % 1.49/1.91 converse(join(X10,converse(complement(converse(X10))))) = top]. % 1.49/1.91 [28=param(7,11),[], % 1.49/1.91 composition(converse(one),converse(X10)) = converse(X10)]. % 1.49/1.91 [30=param(7,9),[], % 1.49/1.91 composition(X10,converse(X11)) = converse(composition(X11,converse(X10)))]. % 1.49/1.91 [33=param(28,9),[9], % 1.49/1.91 composition(converse(one),X10) = X10]. % 1.49/1.91 [34=param(33,11),[], % 1.49/1.91 converse(one) = one]. % 1.49/1.91 [35=demod(33),[34], % 1.49/1.91 composition(one,X10) = X10]. % 1.49/1.91 [38=param(10,35),[], % 1.49/1.91 join(X10,composition(X11,X10)) = composition(join(one,X11),X10)]. % 1.49/1.91 [50=param(13,5),[4], % 1.49/1.91 complement(top) = zero]. % 1.49/1.91 [54=param(13,16),[13], % 1.49/1.91 meet(X10,X11) = meet(X11,X10)]. % 1.49/1.91 [58=param(4,50),[54], % 1.49/1.91 meet(zero,top) = zero]. % 1.49/1.91 [60=param(13,50),[], % 1.49/1.91 complement(join(zero,complement(X10))) = meet(top,X10)]. % 1.49/1.91 [61=param(14,4),[13], % 1.49/1.91 join(zero,meet(X10,X10)) = X10]. % 1.49/1.91 [62=param(14,5),[50,16], % 1.49/1.91 join(zero,meet(X10,complement(complement(X10)))) = X10]. % 1.49/1.91 [66=param(14,58),[16], % 1.49/1.91 join(zero,complement(join(top,complement(zero)))) = zero]. % 1.49/1.91 [85=param(18,7),[9], % 1.49/1.91 join(complement(converse(X10)),composition(X11,complement(converse(composition(X10,X11))))) = complement(converse(X10))]. % 1.49/1.91 [89=param(18,34),[35,35], % 1.49/1.91 join(complement(X10),complement(X10)) = complement(X10)]. % 1.49/1.91 [90=param(18,50),[50], % 1.49/1.91 join(zero,composition(converse(X10),complement(composition(X10,top)))) = zero]. % 1.49/1.91 [96=param(9,23),[], % 1.49/1.91 join(X10,converse(complement(converse(X10)))) = converse(top)]. % 1.49/1.91 [98=param(13,89),[], % 1.49/1.91 meet(X10,X10) = complement(complement(X10))]. % 1.49/1.91 [100=demod(61),[98], % 1.49/1.91 join(zero,complement(complement(X10))) = X10]. % 1.49/1.91 [103=param(15,89),[], % 1.49/1.91 join(complement(X10),join(complement(X10),X11)) = join(complement(X10),X11)]. % 1.49/1.91 [104=param(89,50),[50,50], % 1.49/1.91 join(zero,zero) = zero]. % 1.49/1.91 [105=param(15,104),[], % 1.49/1.91 join(zero,join(zero,X10)) = join(zero,X10)]. % 1.49/1.91 [118=param(100,13),[], % 1.49/1.91 join(complement(X10),complement(X11)) = join(zero,complement(meet(X10,X11)))]. % 1.49/1.91 [149=param(105,16),[15], % 1.49/1.91 join(zero,join(X10,zero)) = join(zero,X10)]. % 1.49/1.91 [151=param(105,100),[100], % 1.49/1.91 join(zero,X10) = X10]. % 1.49/1.91 [152=demod(62),[151], % 1.49/1.91 meet(X10,complement(complement(X10))) = X10]. % 1.49/1.91 [157=demod(60),[151], % 1.49/1.91 meet(top,X10) = complement(complement(X10))]. % 1.49/1.91 [160=demod(66),[151], % 1.49/1.91 complement(join(top,complement(zero))) = zero]. % 1.49/1.91 [161=demod(100),[151], % 1.49/1.91 complement(complement(X10)) = X10]. % 1.49/1.91 [162=demod(157),[161], % 1.49/1.91 meet(top,X10) = X10]. % 1.49/1.91 [163=demod(152),[161], % 1.49/1.91 meet(X10,X10) = X10]. % 1.49/1.91 [166=demod(118),[151], % 1.49/1.91 join(complement(X10),complement(X11)) = complement(meet(X10,X11))]. % 1.49/1.91 [168=demod(90),[151], % 1.49/1.91 composition(converse(X10),complement(composition(X10,top))) = zero]. % 1.49/1.91 [170=demod(149),[151,151], % 1.49/1.91 join(X10,zero) = X10]. % 1.49/1.91 [171=param(14,170),[161,16], % 1.49/1.91 join(X10,meet(X10,zero)) = X10]. % 1.49/1.91 [190=param(161,50),[], % 1.49/1.91 complement(zero) = top]. % 1.49/1.91 [191=demod(160),[190], % 1.49/1.91 complement(join(top,top)) = zero]. % 1.49/1.91 [237=param(5,191),[15,16,151], % 1.49/1.91 join(top,top) = top]. % 1.49/1.91 [238=param(15,237),[], % 1.49/1.91 join(top,join(top,X10)) = join(top,X10)]. % 1.49/1.91 [272=param(171,54),[], % 1.49/1.91 join(X10,meet(zero,X10)) = X10]. % 1.49/1.91 [294=param(166,161),[], % 1.49/1.91 join(X10,complement(X11)) = complement(meet(complement(X10),X11))]. % 1.49/1.91 [295=demod(14),[294], % 1.49/1.91 complement(meet(complement(meet(X10,X11)),join(complement(X10),X11))) = X10]. % 1.49/1.91 [313=param(294,16),[], % 1.49/1.91 join(complement(X11),X10) = complement(meet(complement(X10),X11))]. % 1.49/1.91 [314=demod(295),[313], % 1.49/1.91 complement(meet(complement(meet(X10,X11)),complement(meet(complement(X11),X10)))) = X10]. % 1.49/1.91 [315=demod(85),[313,54], % 1.49/1.91 complement(meet(converse(X10),complement(composition(X11,complement(converse(composition(X10,X11))))))) = complement(converse(X10))]. % 1.49/1.91 [324=demod(103),[313,294,161,313], % 1.49/1.91 complement(meet(X10,meet(complement(X11),X10))) = complement(meet(complement(X11),X10))]. % 1.49/1.91 [328=param(294,22),[], % 1.49/1.91 converse(join(X10,converse(complement(X11)))) = complement(meet(complement(converse(X10)),X11))]. % 1.49/1.91 [331=param(294,161),[], % 1.49/1.91 join(X10,X11) = complement(meet(complement(X10),complement(X11)))]. % 1.49/1.91 [341=demod(272),[331], % 1.49/1.91 complement(meet(complement(X10),complement(meet(zero,X10)))) = X10]. % 1.49/1.91 [347=demod(38),[331,331], % 1.49/1.91 complement(meet(complement(X10),complement(composition(X11,X10)))) = composition(complement(meet(complement(one),complement(X11))),X10)]. % 1.49/1.91 [371=demod(96),[331], % 1.49/1.91 complement(meet(complement(X10),complement(converse(complement(converse(X10)))))) = converse(top)]. % 1.49/1.91 [372=demod(328),[331], % 1.49/1.91 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),complement(converse(complement(X11))))))]. % 1.49/1.91 [452=demod(238),[331,50,331,50,161,331,50], % 1.49/1.91 complement(meet(zero,meet(zero,complement(X10)))) = complement(meet(zero,complement(X10)))]. % 1.49/1.91 [456=param(20,331),[161,30], % 1.49/1.91 thtop(complement(meet(sk1,complement(converse(composition(sk2,converse(complement(composition(sk1,sk2)))))))),complement(sk1)) = thmtrue]. % 1.49/1.91 [458=param(168,9),[], % 1.49/1.91 composition(X10,complement(composition(converse(X10),top))) = zero]. % 1.49/1.91 [509=param(161,341),[], % 1.49/1.91 meet(complement(X10),complement(meet(zero,X10))) = complement(X10)]. % 1.49/1.91 [527=param(452,161),[161], % 1.49/1.91 complement(meet(zero,meet(zero,X10))) = complement(meet(zero,X10))]. % 1.49/1.91 [530=param(161,527),[161], % 1.49/1.91 meet(zero,meet(zero,X10)) = meet(zero,X10)]. % 1.49/1.91 [531=param(530,54),[], % 1.49/1.91 meet(zero,meet(X10,zero)) = meet(zero,X10)]. % 1.49/1.91 [532=param(509,531),[], % 1.49/1.91 meet(complement(meet(X10,zero)),complement(meet(zero,X10))) = complement(meet(X10,zero))]. % 1.49/1.91 [533=param(324,4),[161,161,54,4,190], % 1.49/1.91 complement(meet(X10,zero)) = top]. % 1.49/1.91 [534=demod(532),[533,162,533], % 1.49/1.91 complement(meet(zero,X10)) = top]. % 1.49/1.91 [542=param(4,534),[54,162], % 1.49/1.91 meet(zero,X10) = zero]. % 1.49/1.91 [551=param(161,314),[], % 1.49/1.91 meet(complement(meet(X10,X11)),complement(meet(complement(X11),X10))) = complement(X10)]. % 1.49/1.91 [560=param(161,315),[161], % 1.49/1.91 meet(converse(X10),complement(composition(X11,complement(converse(composition(X10,X11)))))) = converse(X10)]. % 1.49/1.91 [693=param(347,50),[54,542,190], % 1.49/1.91 complement(meet(complement(X10),complement(composition(top,X10)))) = composition(top,X10)]. % 1.49/1.91 [757=param(161,693),[], % 1.49/1.91 meet(complement(X10),complement(composition(top,X10))) = complement(composition(top,X10))]. % 1.49/1.91 [770=param(757,458),[161,190,54,162,458,190], % 1.49/1.91 composition(converse(top),top) = top]. % 1.49/1.91 [773=param(7,770),[9,770], % 1.49/1.91 converse(top) = top]. % 1.49/1.91 [783=demod(371),[773], % 1.49/1.91 complement(meet(complement(X10),complement(converse(complement(converse(X10)))))) = top]. % 1.49/1.91 [896=param(4,783),[54,162], % 1.49/1.91 meet(complement(X10),complement(converse(complement(converse(X10))))) = zero]. % 1.49/1.91 [898=param(896,9),[], % 1.49/1.91 meet(complement(converse(X10)),complement(converse(complement(X10)))) = zero]. % 1.49/1.91 [1385=param(551,896),[190,161,54,162,161], % 1.49/1.91 complement(meet(complement(X10),converse(complement(converse(X10))))) = X10]. % 1.49/1.91 [1386=param(551,896),[54,190,54,162,161], % 1.49/1.91 complement(meet(X10,complement(converse(complement(converse(X10)))))) = converse(complement(converse(X10)))]. % 1.49/1.91 [1388=param(551,898),[54,190,54,162,161], % 1.49/1.91 complement(meet(converse(X10),complement(converse(complement(X10))))) = converse(complement(X10))]. % 1.49/1.91 [1482=param(161,1385),[], % 1.49/1.91 meet(complement(X10),converse(complement(converse(X10)))) = complement(X10)]. % 1.49/1.91 [1485=param(372,1482),[161,9,1386,9], % 1.49/1.91 complement(converse(complement(X10))) = converse(X10)]. % 1.49/1.91 [1486=demod(372),[1485], % 1.49/1.91 complement(meet(complement(converse(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 1.49/1.91 [1541=demod(1388),[1485,163], % 1.49/1.91 complement(converse(X10)) = converse(complement(X10))]. % 1.49/1.91 [1546=demod(1486),[1541], % 1.49/1.91 complement(meet(converse(complement(X10)),X11)) = converse(complement(meet(complement(X10),converse(X11))))]. % 1.49/1.91 [1579=demod(560),[1541], % 1.49/1.91 meet(converse(X10),complement(composition(X11,converse(complement(composition(X10,X11)))))) = converse(X10)]. % 1.49/1.91 [1728=param(456,1541),[], % 1.49/1.91 thtop(complement(meet(sk1,converse(complement(composition(sk2,converse(complement(composition(sk1,sk2)))))))),complement(sk1)) = thmtrue]. % 1.49/1.91 [2633=param(1546,161),[161], % 1.49/1.91 complement(meet(converse(X10),X11)) = converse(complement(meet(X10,converse(X11))))]. % 1.49/1.91 [2652=param(161,2633),[1541,161], % 1.49/1.91 meet(converse(X10),X11) = converse(meet(X10,converse(X11)))]. % 1.49/1.91 [2672=demod(1579),[2652], % 1.49/1.91 converse(meet(X10,converse(complement(composition(X11,converse(complement(composition(X10,X11)))))))) = converse(X10)]. % 1.49/1.91 [2735=param(2652,54),[], % 1.49/1.91 converse(meet(X10,converse(X11))) = meet(X11,converse(X10))]. % 1.49/1.91 [2818=param(1728,2735),[54,2652,2672,9,19], % 1.49/1.91 thmtrue = thmfalse]. % 1.49/1.91 % SZS output end CNFRefutation % 1.49/1.91 Space: 7015 KB %------------------------------------------------------------------------------