%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : BOO026-1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n018.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 : Thu Jul 14 23:38:50 EDT 2022 % Result : Unsatisfiable 0.85s 1.23s % Output : CNFRefutation 0.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : BOO026-1 : TPTP v8.1.0. Released v2.2.0. % 0.07/0.13 % Command : fiesta-wrapper %s % 0.13/0.35 % Computer : n018.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Wed Jun 1 20:13:14 EDT 2022 % 0.13/0.35 % CPUTime : % 0.85/1.23 Theorem Proved. % 0.85/1.23 % SZS status Unsatisfiable % 0.85/1.23 % SZS output start CNFRefutation % 0.85/1.23 [1=axiom,[], % 0.85/1.23 multiply(add(X10,inverse(X11)),multiply(add(X10,X10),add(inverse(X11),X10))) = X10]. % 0.85/1.23 [2=axiom,[], % 0.85/1.23 multiply(add(X10,inverse(X11)),multiply(add(X10,X11),add(inverse(X11),X11))) = X10]. % 0.85/1.23 [3=axiom,[], % 0.85/1.23 multiply(add(X10,inverse(X10)),multiply(add(X10,X11),add(inverse(X10),X11))) = X11]. % 0.85/1.23 [4=axiom,[], % 0.85/1.23 add(multiply(X10,inverse(X11)),add(multiply(X10,X10),multiply(inverse(X11),X10))) = X10]. % 0.85/1.23 [5=axiom,[], % 0.85/1.23 add(multiply(X10,inverse(X11)),add(multiply(X10,X11),multiply(inverse(X11),X11))) = X10]. % 0.85/1.23 [7=axiom,[], % 0.85/1.23 multiply(X10,inverse(X10)) = n0]. % 0.85/1.23 [9=axiom,[], % 0.85/1.23 add(X10,multiply(X11,X12)) = multiply(add(X11,X10),add(X12,X10))]. % 0.85/1.23 [10=demod(5),[9], % 0.85/1.23 add(multiply(X10,inverse(X11)),multiply(add(inverse(X11),multiply(X10,X11)),add(X11,multiply(X10,X11)))) = X10]. % 0.85/1.23 [12=axiom,[], % 0.85/1.23 add(X10,inverse(X10)) = n1]. % 0.85/1.23 [13=demod(3),[12], % 0.85/1.23 multiply(n1,multiply(add(X10,X11),add(inverse(X10),X11))) = X11]. % 0.85/1.23 [14=axiom,[], % 0.85/1.23 add(multiply(X11,X10),multiply(X12,X10)) = multiply(X10,add(X11,X12))]. % 0.85/1.23 [15=demod(4),[14], % 0.85/1.23 add(multiply(X10,inverse(X11)),multiply(X10,add(X10,inverse(X11)))) = X10]. % 0.85/1.23 [16=axiom,[], % 0.85/1.23 thtop(X10,X10) = thmfalse]. % 0.85/1.23 [17=axiom,[], % 0.85/1.23 thtop(multiply(add(a,b),b),b) = thmtrue]. % 0.85/1.23 [18=param(14,7),[], % 0.85/1.23 add(n0,multiply(X10,inverse(X11))) = multiply(inverse(X11),add(X11,X10))]. % 0.85/1.23 [19=param(14,7),[], % 0.85/1.23 add(multiply(X10,inverse(X11)),n0) = multiply(inverse(X11),add(X10,X11))]. % 0.85/1.23 [20=param(1,12),[-9,7], % 0.85/1.23 multiply(n1,add(X10,n0)) = X10]. % 0.85/1.23 [21=param(14,20),[], % 0.85/1.23 add(X10,multiply(X11,add(X10,n0))) = multiply(add(X10,n0),add(n1,X11))]. % 0.85/1.23 [23=param(19,7),[], % 0.85/1.23 add(n0,n0) = multiply(inverse(X10),add(X10,X10))]. % 0.85/1.23 [24=param(20,19),[], % 0.85/1.23 multiply(n1,multiply(inverse(X10),add(X11,X10))) = multiply(X11,inverse(X10))]. % 0.85/1.23 [26=param(23,23),[], % 0.85/1.23 multiply(inverse(n0),multiply(inverse(X10),add(X10,X10))) = add(n0,n0)]. % 0.85/1.23 [27=param(23,14),[], % 0.85/1.23 multiply(inverse(multiply(X10,X11)),multiply(X11,add(X10,X10))) = add(n0,n0)]. % 0.85/1.23 [29=param(24,23),[7], % 0.85/1.23 multiply(n1,multiply(inverse(n0),multiply(inverse(X10),add(X10,X10)))) = n0]. % 0.85/1.23 [30=param(9,7),[], % 0.85/1.23 add(X10,n0) = multiply(add(X11,X10),add(inverse(X11),X10))]. % 0.85/1.23 [31=param(9,20),[], % 0.85/1.23 add(X10,X11) = multiply(add(n1,X10),add(add(X11,n0),X10))]. % 0.85/1.23 [33=param(1,9),[], % 0.85/1.23 multiply(add(X10,inverse(X11)),add(X10,multiply(X10,inverse(X11)))) = X10]. % 0.85/1.23 [34=param(2,9),[], % 0.85/1.23 multiply(add(X10,inverse(X11)),add(X11,multiply(X10,inverse(X11)))) = X10]. % 0.85/1.23 [35=param(9,12),[], % 0.85/1.23 multiply(n1,add(X10,inverse(X11))) = add(inverse(X11),multiply(X11,X10))]. % 0.85/1.23 [36=param(9,12),[], % 0.85/1.23 multiply(add(X10,inverse(X11)),n1) = add(inverse(X11),multiply(X10,X11))]. % 0.85/1.23 [39=param(10,7),[9,12,12,9], % 0.85/1.23 add(n0,multiply(multiply(n1,n1),multiply(add(X10,X10),add(X10,X10)))) = X10]. % 0.85/1.23 [43=param(30,12),[], % 0.85/1.23 multiply(n1,add(inverse(X10),inverse(X10))) = add(inverse(X10),n0)]. % 0.85/1.23 [44=param(30,12),[], % 0.85/1.23 add(inverse(inverse(X10)),n0) = multiply(add(X10,inverse(inverse(X10))),n1)]. % 0.85/1.23 [46=param(15,7),[12], % 0.85/1.23 add(n0,multiply(X10,n1)) = X10]. % 0.85/1.23 [47=param(46,9),[], % 0.85/1.23 multiply(add(X10,n0),add(n1,n0)) = X10]. % 0.85/1.23 [48=param(9,46),[], % 0.85/1.23 multiply(X10,add(X11,multiply(X10,n1))) = add(multiply(X10,n1),multiply(n0,X11))]. % 0.85/1.23 [51=param(24,46),[], % 0.85/1.23 multiply(n1,multiply(inverse(multiply(X10,n1)),X10)) = multiply(n0,inverse(multiply(X10,n1)))]. % 0.85/1.23 [53=param(9,47),[], % 0.85/1.23 add(X10,X11) = multiply(add(add(X11,n0),X10),add(add(n1,n0),X10))]. % 0.85/1.23 [54=param(47,19),[], % 0.85/1.23 multiply(multiply(inverse(X10),add(X11,X10)),add(n1,n0)) = multiply(X11,inverse(X10))]. % 0.85/1.23 [55=param(47,30),[], % 0.85/1.23 multiply(multiply(add(X10,X11),add(inverse(X10),X11)),add(n1,n0)) = X11]. % 0.85/1.23 [59=param(21,20),[], % 0.85/1.23 add(X10,X10) = multiply(add(X10,n0),add(n1,n1))]. % 0.85/1.23 [60=demod(43),[59], % 0.85/1.23 multiply(n1,multiply(add(inverse(X10),n0),add(n1,n1))) = add(inverse(X10),n0)]. % 0.85/1.23 [70=param(27,20),[], % 0.85/1.23 add(n0,n0) = multiply(inverse(multiply(n0,n1)),n0)]. % 0.85/1.23 [74=demod(27),[70], % 0.85/1.23 multiply(inverse(multiply(X10,X11)),multiply(X11,add(X10,X10))) = multiply(inverse(multiply(n0,n1)),n0)]. % 0.85/1.23 [75=demod(26),[70], % 0.85/1.23 multiply(inverse(n0),multiply(inverse(X10),add(X10,X10))) = multiply(inverse(multiply(n0,n1)),n0)]. % 0.85/1.23 [77=demod(29),[75,51], % 0.85/1.23 multiply(n0,inverse(multiply(n0,n1))) = n0]. % 0.85/1.23 [82=param(9,77),[], % 0.85/1.23 add(X10,n0) = multiply(add(n0,X10),add(inverse(multiply(n0,n1)),X10))]. % 0.85/1.23 [86=param(34,18),[], % 0.85/1.23 multiply(add(X10,inverse(n0)),multiply(inverse(n0),add(n0,X10))) = X10]. % 0.85/1.23 [89=param(46,36),[], % 0.85/1.23 add(n0,add(inverse(X10),multiply(X11,X10))) = add(X11,inverse(X10))]. % 0.85/1.23 [91=param(48,14),[20], % 0.85/1.23 multiply(X10,add(n1,multiply(X10,n1))) = X10]. % 0.85/1.23 [93=param(91,9),[], % 0.85/1.23 multiply(X10,multiply(add(X10,n1),add(n1,n1))) = X10]. % 0.85/1.23 [96=param(91,21),[], % 0.85/1.23 add(X10,multiply(multiply(add(X10,n0),n1),add(X10,n0))) = add(X10,n0)]. % 0.85/1.23 [99=param(39,53),[], % 0.85/1.23 add(n0,multiply(multiply(n1,n1),add(add(n1,n0),n1))) = add(n1,n0)]. % 0.85/1.23 [101=param(20,82),[], % 0.85/1.23 multiply(n1,multiply(add(n0,X10),add(inverse(multiply(n0,n1)),X10))) = X10]. % 0.85/1.23 [109=param(14,9),[], % 0.85/1.23 multiply(X10,add(X11,X12)) = multiply(add(X12,multiply(X11,X10)),add(X10,multiply(X11,X10)))]. % 0.85/1.23 [110=demod(99),[109], % 0.85/1.23 add(n0,multiply(add(n1,multiply(add(n1,n0),multiply(n1,n1))),add(multiply(n1,n1),multiply(add(n1,n0),multiply(n1,n1))))) = add(n1,n0)]. % 0.85/1.23 [111=param(14,47),[], % 0.85/1.23 multiply(add(n1,n0),add(add(X10,n0),X11)) = add(X10,multiply(X11,add(n1,n0)))]. % 0.85/1.23 [112=param(14,47),[], % 0.85/1.23 add(multiply(X10,add(n1,n0)),X11) = multiply(add(n1,n0),add(X10,add(X11,n0)))]. % 0.85/1.23 [117=param(9,59),[], % 0.85/1.23 multiply(add(X10,X11),multiply(add(X11,n0),add(n1,n1))) = add(X11,multiply(X10,X11))]. % 0.85/1.23 [119=param(59,19),[9,-109], % 0.85/1.23 multiply(multiply(inverse(X10),add(X11,X10)),add(n1,n1)) = multiply(inverse(X10),add(X11,X11))]. % 0.85/1.23 [129=param(86,12),[59], % 0.85/1.23 multiply(multiply(add(inverse(n0),n0),add(n1,n1)),multiply(inverse(n0),n1)) = inverse(n0)]. % 0.85/1.23 [138=param(35,89),[], % 0.85/1.23 multiply(n1,add(n0,add(inverse(X10),multiply(X11,X10)))) = add(inverse(X10),multiply(X10,X11))]. % 0.85/1.23 [148=param(17,53),[31], % 0.85/1.23 thtop(multiply(multiply(add(add(b,n0),a),multiply(add(n1,add(n1,n0)),add(add(a,n0),add(n1,n0)))),b),b) = thmtrue]. % 0.85/1.23 [154=param(36,55),[-89,55], % 0.85/1.23 multiply(add(n0,add(inverse(add(n1,n0)),X10)),n1) = add(inverse(add(n1,n0)),X10)]. % 0.85/1.23 [156=param(101,46),[], % 0.85/1.23 multiply(n1,multiply(X10,add(inverse(multiply(n0,n1)),multiply(X10,n1)))) = multiply(X10,n1)]. % 0.85/1.23 [158=param(21,96),[47], % 0.85/1.23 add(X10,multiply(multiply(multiply(add(n1,n0),n1),add(n1,n0)),add(X10,n0))) = X10]. % 0.85/1.23 [160=param(154,12),[12], % 0.85/1.23 multiply(add(n0,n1),n1) = n1]. % 0.85/1.23 [163=param(14,160),[], % 0.85/1.23 multiply(n1,add(add(n0,n1),X10)) = add(n1,multiply(X10,n1))]. % 0.85/1.23 [167=param(74,53),[111,47], % 0.85/1.23 multiply(inverse(add(X10,n1)),add(add(n1,n0),X10)) = multiply(inverse(multiply(n0,n1)),n0)]. % 0.85/1.23 [170=param(163,20),[9], % 0.85/1.23 multiply(add(n0,n1),add(n1,n1)) = add(n0,n1)]. % 0.85/1.23 [171=param(163,35),[], % 0.85/1.23 add(inverse(X10),multiply(X10,add(n0,n1))) = add(n1,multiply(inverse(X10),n1))]. % 0.85/1.23 [174=param(93,170),[], % 0.85/1.23 multiply(n0,add(n0,n1)) = n0]. % 0.85/1.23 [176=param(14,174),[], % 0.85/1.23 add(n0,multiply(X10,add(n0,n1))) = multiply(add(n0,n1),add(n0,X10))]. % 0.85/1.23 [181=param(171,174),[], % 0.85/1.23 add(inverse(n0),n0) = add(n1,multiply(inverse(n0),n1))]. % 0.85/1.23 [182=demod(129),[181], % 0.85/1.23 multiply(multiply(add(n1,multiply(inverse(n0),n1)),add(n1,n1)),multiply(inverse(n0),n1)) = inverse(n0)]. % 0.85/1.23 [188=param(9,181),[], % 0.85/1.23 multiply(add(n1,multiply(inverse(n0),n1)),add(X10,n0)) = add(n0,multiply(inverse(n0),X10))]. % 0.85/1.23 [191=param(24,181),[91], % 0.85/1.23 multiply(inverse(n0),inverse(n0)) = multiply(n1,inverse(n0))]. % 0.85/1.23 [194=param(54,181),[91,191], % 0.85/1.23 multiply(inverse(n0),add(n1,n0)) = multiply(n1,inverse(n0))]. % 0.85/1.23 [197=param(18,191),[18,12], % 0.85/1.23 multiply(inverse(n0),add(n0,n1)) = multiply(inverse(n0),n1)]. % 0.85/1.23 [198=param(19,191),[19,194,181,91], % 0.85/1.23 multiply(n1,inverse(n0)) = inverse(n0)]. % 0.85/1.23 [200=demod(194),[198], % 0.85/1.23 multiply(inverse(n0),add(n1,n0)) = inverse(n0)]. % 0.85/1.23 [201=demod(191),[198], % 0.85/1.23 multiply(inverse(n0),inverse(n0)) = inverse(n0)]. % 0.85/1.23 [207=param(18,198),[12,197], % 0.85/1.23 multiply(inverse(n0),n1) = n1]. % 0.85/1.23 [213=demod(60),[], % 0.85/1.23 multiply(n1,multiply(add(inverse(X10),n0),add(n1,n1))) = add(inverse(X10),n0)]. % 0.85/1.23 [216=demod(188),[207], % 0.85/1.23 multiply(add(n1,n1),add(X10,n0)) = add(n0,multiply(inverse(n0),X10))]. % 0.85/1.23 [218=demod(182),[207,207], % 0.85/1.23 multiply(multiply(add(n1,n1),add(n1,n1)),n1) = inverse(n0)]. % 0.85/1.23 [219=demod(181),[207], % 0.85/1.23 add(inverse(n0),n0) = add(n1,n1)]. % 0.85/1.23 [220=param(19,198),[219,200], % 0.85/1.23 add(n1,n1) = inverse(n0)]. % 0.85/1.23 [221=demod(219),[220], % 0.85/1.23 add(inverse(n0),n0) = inverse(n0)]. % 0.85/1.23 [222=demod(218),[220,220,201,207], % 0.85/1.23 inverse(n0) = n1]. % 0.85/1.23 [223=demod(221),[222,222], % 0.85/1.23 add(n1,n0) = n1]. % 0.85/1.23 [225=demod(167),[223], % 0.85/1.23 multiply(inverse(add(X10,n1)),add(n1,X10)) = multiply(inverse(multiply(n0,n1)),n0)]. % 0.85/1.23 [227=demod(158),[223,223], % 0.85/1.23 add(X10,multiply(multiply(multiply(n1,n1),n1),add(X10,n0))) = X10]. % 0.85/1.23 [232=demod(112),[223,223], % 0.85/1.23 add(multiply(X10,n1),X11) = multiply(n1,add(X10,add(X11,n0)))]. % 0.85/1.23 [235=demod(110),[223,223,9,9,232,232,70,223], % 0.85/1.23 add(n0,multiply(add(n1,multiply(n1,multiply(n1,n1))),multiply(multiply(add(n1,n1),add(n1,n1)),multiply(n1,add(n1,multiply(n1,add(n1,multiply(inverse(multiply(n0,n1)),n0)))))))) = n1]. % 0.85/1.23 [245=demod(220),[222], % 0.85/1.23 add(n1,n1) = n1]. % 0.85/1.23 [246=demod(235),[245,245], % 0.85/1.23 add(n0,multiply(add(n1,multiply(n1,multiply(n1,n1))),multiply(multiply(n1,n1),multiply(n1,add(n1,multiply(n1,add(n1,multiply(inverse(multiply(n0,n1)),n0)))))))) = n1]. % 0.85/1.23 [249=demod(207),[222], % 0.85/1.23 multiply(n1,n1) = n1]. % 0.85/1.23 [250=demod(246),[249,249,245,249], % 0.85/1.23 add(n0,multiply(n1,multiply(n1,multiply(n1,add(n1,multiply(n1,add(n1,multiply(inverse(multiply(n0,n1)),n0)))))))) = n1]. % 0.85/1.23 [252=demod(227),[249,249,20], % 0.85/1.23 add(X10,X10) = X10]. % 0.85/1.23 [256=demod(70),[252], % 0.85/1.23 multiply(inverse(multiply(n0,n1)),n0) = n0]. % 0.85/1.23 [262=demod(250),[256,223,249,252,249,249,249], % 0.85/1.23 add(n0,n1) = n1]. % 0.85/1.23 [266=demod(176),[262,46,262], % 0.85/1.23 multiply(n1,add(n0,X10)) = X10]. % 0.85/1.23 [267=demod(138),[266], % 0.85/1.23 add(inverse(X10),multiply(X11,X10)) = add(inverse(X10),multiply(X10,X11))]. % 0.85/1.23 [272=demod(44),[], % 0.85/1.23 add(inverse(inverse(X10)),n0) = multiply(add(X10,inverse(inverse(X10))),n1)]. % 0.85/1.23 [275=demod(174),[262], % 0.85/1.23 multiply(n0,n1) = n0]. % 0.85/1.23 [278=demod(156),[275,222,91], % 0.85/1.23 multiply(n1,X10) = multiply(X10,n1)]. % 0.85/1.23 [280=demod(272),[-278], % 0.85/1.23 add(inverse(inverse(X10)),n0) = multiply(n1,add(X10,inverse(inverse(X10))))]. % 0.85/1.23 [292=demod(280),[], % 0.85/1.23 add(inverse(inverse(X10)),n0) = multiply(n1,add(X10,inverse(inverse(X10))))]. % 0.85/1.23 [295=demod(171),[262,9,12,-278], % 0.85/1.23 add(n1,multiply(n1,inverse(X10))) = multiply(n1,add(n1,inverse(X10)))]. % 0.85/1.23 [296=demod(163),[262], % 0.85/1.23 add(n1,multiply(X10,n1)) = multiply(n1,add(n1,X10))]. % 0.85/1.23 [297=demod(91),[296], % 0.85/1.23 multiply(X10,multiply(n1,add(n1,X10))) = X10]. % 0.85/1.23 [300=demod(225),[275,222,278,275], % 0.85/1.23 multiply(inverse(add(X10,n1)),add(n1,X10)) = n0]. % 0.85/1.23 [307=demod(292),[], % 0.85/1.23 add(inverse(inverse(X10)),n0) = multiply(n1,add(X10,inverse(inverse(X10))))]. % 0.85/1.23 [312=demod(39),[249,252,252], % 0.85/1.23 add(n0,multiply(n1,multiply(X10,X10))) = X10]. % 0.85/1.23 [317=demod(216),[252,20,222], % 0.85/1.23 add(n0,multiply(n1,X10)) = X10]. % 0.85/1.23 [318=demod(312),[317], % 0.85/1.23 multiply(X10,X10) = X10]. % 0.85/1.23 [323=demod(213),[252,-278,109,-278,317,-278,295,297], % 0.85/1.23 add(inverse(X10),n0) = multiply(n1,inverse(X10))]. % 0.85/1.23 [327=demod(307),[323], % 0.85/1.23 multiply(n1,add(X10,inverse(inverse(X10)))) = multiply(n1,inverse(inverse(X10)))]. % 0.85/1.23 [331=demod(119),[252,-278,24,252], % 0.85/1.23 multiply(X10,inverse(X11)) = multiply(inverse(X11),X10)]. % 0.85/1.23 [334=demod(117),[252,-278,20], % 0.85/1.23 multiply(add(X10,X11),X11) = add(X11,multiply(X10,X11))]. % 0.85/1.23 [348=param(2,318),[252], % 0.85/1.23 multiply(inverse(X10),add(inverse(X10),X10)) = inverse(X10)]. % 0.85/1.23 [350=demod(348),[], % 0.85/1.23 multiply(inverse(X10),add(inverse(X10),X10)) = inverse(X10)]. % 0.85/1.23 [358=param(14,318),[], % 0.85/1.23 add(X10,multiply(X11,X10)) = multiply(X10,add(X10,X11))]. % 0.85/1.23 [360=demod(109),[358], % 0.85/1.23 multiply(X10,add(X11,X12)) = multiply(add(X12,multiply(X11,X10)),multiply(X10,add(X10,X11)))]. % 0.85/1.23 [361=demod(334),[358], % 0.85/1.23 multiply(add(X10,X11),X11) = multiply(X11,add(X11,X10))]. % 0.85/1.23 [362=demod(350),[-361,12], % 0.85/1.23 multiply(n1,inverse(X10)) = inverse(X10)]. % 0.85/1.23 [363=demod(327),[362], % 0.85/1.23 multiply(n1,add(X10,inverse(inverse(X10)))) = inverse(inverse(X10))]. % 0.85/1.23 [374=param(14,318),[], % 0.85/1.23 add(multiply(X10,X11),X11) = multiply(X11,add(X10,X11))]. % 0.85/1.23 [376=param(35,318),[12,318], % 0.85/1.23 add(inverse(X10),X10) = n1]. % 0.85/1.23 [394=param(252,9),[358,-360,252], % 0.85/1.23 multiply(X10,X11) = multiply(X11,X10)]. % 0.85/1.23 [396=demod(361),[394], % 0.85/1.23 multiply(X10,add(X11,X10)) = multiply(X10,add(X10,X11))]. % 0.85/1.23 [413=param(13,252),[376], % 0.85/1.23 multiply(n1,multiply(X10,n1)) = X10]. % 0.85/1.23 [419=param(30,252),[376], % 0.85/1.23 add(X10,n0) = multiply(X10,n1)]. % 0.85/1.23 [463=demod(376),[], % 0.85/1.23 add(inverse(X10),X10) = n1]. % 0.85/1.23 [465=demod(374),[], % 0.85/1.23 add(multiply(X10,X11),X11) = multiply(X11,add(X10,X11))]. % 0.85/1.23 [469=param(34,463),[331,7,419,413], % 0.85/1.23 inverse(inverse(X10)) = X10]. % 0.85/1.23 [470=demod(363),[469,252,469], % 0.85/1.23 multiply(n1,X10) = X10]. % 0.85/1.23 [471=demod(413),[470], % 0.85/1.23 multiply(X10,n1) = X10]. % 0.85/1.23 [480=demod(419),[471], % 0.85/1.23 add(X10,n0) = X10]. % 0.85/1.23 [491=demod(465),[], % 0.85/1.23 add(multiply(X10,X11),X11) = multiply(X11,add(X10,X11))]. % 0.85/1.23 [495=demod(491),[], % 0.85/1.23 add(multiply(X10,X11),X11) = multiply(X11,add(X10,X11))]. % 0.85/1.23 [505=demod(495),[], % 0.85/1.23 add(multiply(X10,X11),X11) = multiply(X11,add(X10,X11))]. % 0.85/1.23 [515=param(148,480),[480,480,252,480,470,394], % 0.85/1.23 thtop(multiply(b,multiply(add(b,a),add(a,n1))),b) = thmtrue]. % 0.85/1.23 [522=demod(505),[], % 0.85/1.23 add(multiply(X10,X11),X11) = multiply(X11,add(X10,X11))]. % 0.85/1.23 [523=param(14,470),[522], % 0.85/1.23 multiply(X10,add(X11,X10)) = multiply(X10,add(X11,n1))]. % 0.85/1.23 [525=param(33,470),[318], % 0.85/1.23 add(n1,inverse(X10)) = n1]. % 0.85/1.23 [538=param(267,300),[469,480,469], % 0.85/1.23 add(add(X10,n1),multiply(add(n1,X10),inverse(add(X10,n1)))) = add(X10,n1)]. % 0.85/1.23 [539=param(525,469),[], % 0.85/1.23 add(n1,X10) = n1]. % 0.85/1.23 [540=demod(538),[539,470,12], % 0.85/1.23 add(X10,n1) = n1]. % 0.85/1.23 [541=demod(523),[540,471], % 0.85/1.23 multiply(X10,add(X11,X10)) = X10]. % 0.85/1.23 [545=demod(396),[541], % 0.85/1.23 multiply(X10,add(X10,X11)) = X10]. % 0.85/1.23 [553=param(515,540),[471,545,16], % 0.85/1.23 thmtrue = thmfalse]. % 0.85/1.23 % SZS output end CNFRefutation % 0.85/1.23 Space: 564 KB %------------------------------------------------------------------------------