% ------------------------------------------------------------------------- % Otter input file to check a derivation of Huntington's axiom from Robbins % algebra. % % The derivation is demodulation free. % ------------------------------------------------------------------------- op(500, xfy, +). set(para_from). set(para_into). set(input_sos_first). assign(bsub_hint_add_wt, -1024). set(keep_hint_subsumers). set(order_eq). assign(max_weight, 5). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). list(usable). x = x. x + y = y + x # label("commutativity"). end_of_list. list(sos). (x + y) + z = x + (y + z) # label("associativity"). n(n(n(x) + y) + n(x + y)) = y # label("Robbins"). end_of_list. list(passive). n(n(A) + B) + n(n(A) + n(B)) != A # label("denial of Huntington"). end_of_list. % ------------------------------------------------------------------------- % Hints for proof checking. % ------------------------------------------------------------------------- list(hints). x+y=y+x # label("Hint 1(2)"). (x+y)+z=x+y+z # label("Hint 2(3)"). n(n(n(x)+y)+n(x+y))=y # label("Hint 3(4)"). n(n(A)+B)+n(n(A)+n(B))!=A # label("Hint 4(5)"). (x+y)+z=y+x+z # label("Hint 5(153)"). (x+y+z)+u=x+y+z+u # label("Hint 6(155)"). x+y+z=z+x+y # label("Hint 7(156)"). n(n(x+n(y))+n(y+x))=x # label("Hint 8(157)"). n(n(n(x+y)+z)+n(x+y+z))=z # label("Hint 9(158)"). n(n(n(x)+y)+n(y+x))=y # label("Hint 10(159)"). n(n(x+y)+n(n(x)+y))=y # label("Hint 11(160)"). x+y+z=y+x+z # label("Hint 12(161)"). x+y+z=z+y+x # label("Hint 13(162)"). x+y+z+u=u+x+y+z # label("Hint 14(163)"). n(n(x+n(y)+z)+n(y+x+z))=x+z # label("Hint 15(164)"). n(n((x+y)+n(z))+n(x+z+y))=x+y # label("Hint 16(165)"). n(n(x+n(y+z))+n(z+y+x))=x # label("Hint 17(166)"). n(n(x+n(y+z))+n(y+z+x))=x # label("Hint 18(167)"). n(n(x+n(y))+n(x+y))=x # label("Hint 19(168)"). n(n(x+y)+n(y+n(x)))=y # label("Hint 20(169)"). n(n(x+y)+n(y+n(n(z)+x)+n(z+x)))=y # label("Hint 21(170)"). n(n(x+y)+n(n(y)+x))=x # label("Hint 22(171)"). n(n(x+y+z)+n(n(x+y)+z))=z # label("Hint 23(172)"). n(n(x+n(y+z))+n(z+x+y))=x # label("Hint 24(173)"). n(n(x+y)+n(x+n(y)))=x # label("Hint 25(174)"). n(n(x+y+z)+n((y+x)+n(z)))=y+x # label("Hint 26(175)"). n(n(x+n(y+z)+n(z+n(y)))+n(z+x))=x # label("Hint 27(176)"). n(n(n(n(x)+y)+y+x)+y)=n(n(x)+y) # label("Hint 28(177)"). n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y) # label("Hint 29(178)"). n(n(x+n(y+z)+n(y+n(z)))+n(x+y))=x # label("Hint 30(179)"). n(n(x+y)+n(x+n(y+z)+n(y+n(z))))=x # label("Hint 31(180)"). n(n(n(x+y+z)+u)+n(x+y+z+u))=u # label("Hint 32(181)"). n(x+n(x+y+n(n(y)+x)))=n(n(y)+x) # label("Hint 33(182)"). n(x+n(y+x+n(n(y)+x)))=n(n(y)+x) # label("Hint 34(183)"). n(n(n(x+y+z)+y+n(x)+z)+y+z)=n(x+y+z) # label("Hint 35(184)"). n(n(x+y+n(z))+n(x+z+y))=x+y # label("Hint 36(185)"). n(n(x+y+z)+n(y+x+n(z)))=y+x # label("Hint 37(186)"). n(n(n(n(x+y+z)+u)+x+y+z+u)+u)=n(n(x+y+z)+u) # label("Hint 38(187)"). n(n(n(n(x)+y)+ (x+y)+y)+n(n(x)+y))=y # label("Hint 39(188)"). n(n(x+n(y)+z)+n(z+y+x))=z+x # label("Hint 40(189)"). n(n(x+y)+n(y+n(n(z)+x)+n((n(n(z)+x)+x+z)+x)))=y # label("Hint 41(190)"). n(n(x+n(y+n(z)))+n(x+n(n(y+n(z))+z+y)+y))=x # label("Hint 42(191)"). n(n(n(x+y+z+u+v)+w)+n(x+y+z+u+v+w))=w # label("Hint 43(192)"). n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y # label("Hint 44(193)"). n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z))=z # label("Hint 45(194)"). n(n(n(x+y+z)+x+n(y)+z)+x+z)=n(y+x+z) # label("Hint 46(195)"). n(n(n(x+y+z)+x+n(y)+z)+z+x)=n(y+x+z) # label("Hint 47(196)"). n(n(x+n(y+n(z)))+n(x+n(z+y+n(y+n(z)))+y))=x # label("Hint 48(197)"). n(n(x+n(y+n(z)))+n(x+y+n(z+y+n(y+n(z)))))=x # label("Hint 49(198)"). n(n(x+y)+n(y+n(n(z)+x)+n(n(n(z)+x)+x+z+x)))=y # label("Hint 50(199)"). n(n(n(n(n(x)+y)+x+y+y)+ (n(n(x)+y)+z)+n(y+z))+z)=n(y+z) # label("Hint 51(200)"). n(n(x+y)+n(x+n(n(z)+y)+n(n(n(z)+y)+y+z+y)))=x # label("Hint 52(201)"). n(n(x+y)+n(x+n(n(z)+y)+n(n(n(z)+y)+y+y+z)))=x # label("Hint 53(202)"). n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z+n(y+z))+z)=n(y+z) # label("Hint 54(203)"). n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z)=n(y+z) # label("Hint 55(204)"). n(n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))=u # label("Hint 56(205)"). n(n((x+x+x)+n(n(x+x+x)+x)+x+x)+n(n(x+x+x)+n(n(x+x+x)+x)))=n(n(x+x+x)+x) # label("Hint 57(206)"). n(n(x+x+x+n(n(x+x+x)+x)+x+x)+n(n(x+x+x)+n(n(x+x+x)+x)))=n(n(x+x+x)+x) # label("Hint 58(207)"). n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n(x+x+x+n(n(x+x+x)+x)+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x) # label("Hint 59(208)"). n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n((n(n(x+x+x)+x)+x+x)+x+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x) # label("Hint 60(209)"). n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+x+x+x+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x) # label("Hint 61(210)"). n(x+x+x+n(n(x+x+x)+x)+x+x)=n(x+x+x) # label("Hint 62(211)"). n((n(n(x+x+x)+x)+x+x)+x+x+x)=n(x+x+x) # label("Hint 63(212)"). n(n(n(x+x+x)+n(n(x+x+x)+x)+x+x)+n(x+x+x))=n(n(x+x+x)+x)+x+x # label("Hint 64(213)"). n(n(n(x+x+x)+x)+x+x+x+x+x)=n(x+x+x) # label("Hint 65(214)"). n(n(n(n(n(x+x+x)+x)+x+x+x+x)+x)+n(x+x+x))=x # label("Hint 66(215)"). n(n(n(x+x+x)+x)+n(x+x+x))=x # label("Hint 67(216)"). n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+y))=y # label("Hint 68(217)"). n(n(n(x+x+x)+n(n(x+x+x)+x)+y)+n(x+y))=y # label("Hint 69(218)"). n(n(x+x+x)+x)+x+x=x+x # label("Hint 70(219)"). (x+x)+n(n(x+x+x)+x)=x+x # label("Hint 71(220)"). n(n((x+x)+n(n(n(x+x+x)+x)+y))+n(y+x+x))=x+x # label("Hint 72(221)"). n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(y+x+x))=n(n(x+x+x)+x) # label("Hint 73(222)"). n(n(x+x)+n(n(n(x+x+x)+x)+n(x+x)))=n(n(x+x+x)+x) # label("Hint 74(223)"). (x+x)+n(n(x+x+x)+x)+y= (x+x)+y # label("Hint 75(224)"). n(n(x+x+x)+x)+ (x+x)+y= (x+x)+y # label("Hint 76(225)"). n(n(n(n(x+x+x)+x)+n(y+x+x)+n((x+x)+n(y)))+n(x+x))=n(n(x+x+x)+x) # label("Hint 77(226)"). n(n((n(n(x+x+x)+x)+y)+n((x+x)+z))+n(z+ (x+x)+y))=n(n(x+x+x)+x)+y # label("Hint 78(227)"). n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y)))=n(n(x+x+x)+x) # label("Hint 79(228)"). n(n(n(x+x+x)+x)+n((x+x)+n(n(n(x+x+x)+x)+n(x+x))))=n(n(n(x+x+x)+x)+n(x+x)) # label("Hint 80(229)"). n(n((n(n(n(x+x+x)+x)+n((x+x)+y))+n(y+x+x))+z)+n(z+n(n(x+x+x)+x)))=z # label("Hint 81(230)"). n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n(((x+x)+y)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 82(231)"). n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(n(n(x+x+x)+x)+n((x+x)+y))+ ((x+x)+y)+n(n(x+x+x)+x)))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 83(232)"). n(n(n(n(x+x+x)+x)+y+n((x+x)+z))+n(z+ (x+x)+y))=n(n(x+x+x)+x)+y # label("Hint 84(233)"). n(n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(y+x+x)+z)+n(z+n(n(x+x+x)+x)))=z # label("Hint 85(234)"). n(n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))+n(n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))+x+x))=x+x # label("Hint 86(235)"). n(n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))+n((x+x)+n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))))=x+x # label("Hint 87(236)"). n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+ ((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 88(237)"). n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+ (x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 89(238)"). n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 90(239)"). n(n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n((x+x)+y)+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 91(240)"). n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(x+x+x)+x)+ (x+x)+y))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 92(241)"). n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(n(n(x+x+x)+x)+n((x+x)+y))+ (x+x)+y))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 93(242)"). n(n(n(n(x+x+x)+x)+n((x+x)+y))+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y))))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 94(243)"). n(n(n(n(x+x+x)+x)+n((x+x)+y))+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y))))=n(n(x+x+x)+x) # label("Hint 95(244)"). n(n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n((x+x)+y)+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 96(246)"). n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))=n((x+x)+y) # label("Hint 97(247)"). n((x+x)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n(x+x)))=n((x+x)+n(n(x+x+x)+x)) # label("Hint 98(248)"). n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))=n((x+x)+n(n(x+x+x)+x)) # label("Hint 99(249)"). n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))=n(x+x) # label("Hint 100(250)"). n(n(x+x)+n((x+x)+n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))))=x+x # label("Hint 101(251)"). n(n(x+x)+n((x+x)+n(x+x)))=x+x # label("Hint 102(252)"). n((x+x)+n(n(x+x)+ (x+x)+n((x+x)+ (x+x)+n((x+x)+n(x+x)))))=n(x+x) # label("Hint 103(253)"). n(n((x+x)+n(x+x))+n((x+x)+n((x+x)+n(x+x))+x+x))=n(n(x+x)+n((x+x)+n(x+x))) # label("Hint 104(254)"). n((x+x)+n((x+x)+n(x+x)+n((x+x)+ (x+x)+n((x+x)+n(x+x)))))=n(x+x) # label("Hint 105(255)"). n(n((x+x)+n(x+x))+n((x+x)+ (x+x)+n((x+x)+n(x+x))))=n(n(x+x)+n((x+x)+n(x+x))) # label("Hint 106(256)"). n(n((x+x)+n(x+x))+n((x+x)+ (x+x)+n((x+x)+n(x+x))))=x+x # label("Hint 107(257)"). n((x+x)+n((x+x)+n(x+x)+n((x+x)+ (x+x)+n((x+x)+n(x+x)))))=n((x+x)+ (x+x)+n((x+x)+n(x+x))) # label("Hint 108(258)"). n((x+x)+ (x+x)+n((x+x)+n(x+x)))=n(x+x) # label("Hint 109(259)"). n(n(n(n(x+x+x)+x)+n((x+x)+n(x+x))+n((x+x)+x+x))+n(x+x))=n(n(x+x+x)+x)+n((x+x)+n(x+x)) # label("Hint 110(260)"). n(n(n(n(x+x+x)+x)+n((x+x)+x+x)+n((x+x)+n(x+x)))+n(x+x))=n(n(x+x+x)+x)+n((x+x)+n(x+x)) # label("Hint 111(261)"). n(n(x+x+x)+x)+n((x+x)+n(x+x))=n(n(x+x+x)+x) # label("Hint 112(262)"). n(n(n(n(n(x+x+x)+x))+n(n(x+x)+x+x)+y)+n(y+n(n(x+x+x)+x)))=y # label("Hint 113(264)"). n(n(n((x+x)+n(x+x))+n(n(n(x+x+x)+x))+y)+n(y+n(n(x+x+x)+x)))=y+n((x+x)+n(x+x)) # label("Hint 114(265)"). n(n(n(n(n(x+x+x)+x))+n((x+x)+n(x+x))+y)+n(y+n(n(x+x+x)+x)))=y # label("Hint 115(266)"). n(n(n(n(n(x+x+x)+x))+n((x+x)+n(x+x))+y)+n(y+n(n(x+x+x)+x)))=y+n((x+x)+n(x+x)) # label("Hint 116(267)"). x+n((y+y)+n(y+y))=x # label("Hint 117(268)"). n((x+x)+n(x+x))+y=y # label("Hint 118(269)"). n(n(n((x+x)+n(x+x))+n(y))+n(y))=n((x+x)+n(x+x)) # label("Hint 119(271)"). n(n(x)+n(x+n(n((y+y)+n(y+y)))))=x # label("Hint 120(272)"). n(n(x+y+n(n((z+z)+n(z+z))))+n(x+y))=x+y # label("Hint 121(273)"). n(n(x+y)+n(n(y+n(n((z+z)+n(z+z))))+x+n(y)))=x # label("Hint 122(275)"). n(x+n(n(n((y+y)+n(y+y)))+x+n(x)))=n(x) # label("Hint 123(276)"). n(n(x)+n(n(n((y+y)+n(y+y)))+ (x+n(x))+x))=x # label("Hint 124(277)"). n(n(n(x)+n(n(n((y+y)+n(y+y)))+x+n(x)))+n(x))=n(n(n((y+y)+n(y+y)))+x+n(x)) # label("Hint 125(278)"). n(n(n((x+x)+n(x+x)))+n(n(n((y+y)+n(y+y)))+n((x+x)+n(x+x))+n(n((x+x)+n(x+x)))))=n((x+x)+n(x+x)) # label("Hint 126(279)"). n(n(x+n(n((y+y)+n(y+y))+n(z))+n(z))+n(x+n((y+y)+n(y+y))))=x # label("Hint 127(280)"). n(n(n((x+x)+n(x+x))+n(n((y+y)+n(y+y))+n(z))+n(z))+n(n((y+y)+n(y+y))))=n((x+x)+n(x+x)) # label("Hint 128(281)"). n(n(n((x+x)+n(x+x)))+n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))=n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y)))) # label("Hint 129(282)"). n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x)))))=n(n((x+x)+n(x+x))) # label("Hint 130(283)"). n(n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))+n(n((y+y)+n(y+y))))+n(n((x+x)+n(x+x))))=n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x)))) # label("Hint 131(284)"). n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))=n((x+x)+n(x+x)) # label("Hint 132(285)"). n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))+n((x+x)+n(x+x))=n((x+x)+n(x+x)) # label("Hint 133(286)"). n(n(x+n((y+y)+n(y+y)))+n(n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))+x+n(n((y+y)+n(y+y)))))=n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))+x # label("Hint 134(287)"). n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))+y=y # label("Hint 135(288)"). n(n(n(x+y)+n(x+n(y)))+n(n(n((z+z)+n(z+z))+n(n((z+z)+n(z+z))))+x))=n(n((z+z)+n(z+z))+n(n((z+z)+n(z+z)))) # label("Hint 136(292)"). n(x+n(n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))+x))=n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y)))) # label("Hint 137(294)"). n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))=n(y+n(y)) # label("Hint 138(295)"). n(x+n(x))=n(y+n(y)) # label("Hint 139(296)"). n(n(n(n(x))+x)+n(y+n(y)))=x # label("Hint 140(347)"). n(n(x))=x # label("Hint 141(349)"). n(n(x)+y)+n(x+y)=n(y) # label("Hint 142(350)"). n(n(x)+n(y))+n(x+n(y))=y # label("Hint 143(351)"). n(x+n(y))+n(n(x)+n(y))=y # label("Hint 144(352)"). n(x+n(y))+n(n(y)+n(x))=y # label("Hint 145(353)"). n(n(x)+y)+n(n(x)+n(y))=x # label("Hint 146(354)"). %$F # label("Hint 147(355)"). end_of_list.