%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP122-1 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n029.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 : Sat Jul 16 09:12:32 EDT 2022 % Result : Unsatisfiable 0.82s 1.19s % Output : CNFRefutation 0.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP122-1 : TPTP v8.1.0. Released v1.2.0. % 0.03/0.13 % Command : fiesta-wrapper %s % 0.14/0.34 % Computer : n029.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue Jun 14 00:31:25 EDT 2022 % 0.14/0.34 % CPUTime : % 0.82/1.19 Theorem Proved. % 0.82/1.19 % SZS status Unsatisfiable % 0.82/1.19 % SZS output start CNFRefutation % 0.82/1.19 [1=axiom,[], % 0.82/1.19 multiply(identity,identity) = identity]. % 0.82/1.19 [2=axiom,[], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),multiply(X11,X12))),multiply(X12,multiply(X12,X12)))) = X11]. % 0.82/1.19 [3=axiom,[], % 0.82/1.19 thtop(X10,X10) = thmfalse]. % 0.82/1.19 [4=axiom,[], % 0.82/1.19 thtop(multiply(multiply(a,b),c),multiply(a,multiply(b,c))) = thmtrue]. % 0.82/1.19 [6=param(2,1),[1], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),multiply(X11,identity))),identity)) = X11]. % 0.82/1.19 [7=param(6,1),[], % 0.82/1.19 multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X10,identity))),identity)) = X10]. % 0.82/1.19 [8=param(7,6),[1], % 0.82/1.19 multiply(identity,multiply(multiply(identity,X10),identity)) = multiply(identity,multiply(identity,multiply(X10,identity)))]. % 0.82/1.19 [9=demod(7),[8,8], % 0.82/1.19 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X10,identity),identity)))) = X10]. % 0.82/1.19 [10=param(8,8),[8,8,9], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X10),identity),identity))) = X10]. % 0.82/1.19 [11=param(8,10),[8,9], % 0.82/1.19 multiply(multiply(identity,X10),identity) = multiply(identity,multiply(X10,identity))]. % 0.82/1.19 [12=param(2,1),[], % 0.82/1.19 multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11)))) = X10]. % 0.82/1.19 [13=param(2,11),[1,1], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),multiply(identity,multiply(X11,identity)))),identity)) = multiply(identity,X11)]. % 0.82/1.19 [14=param(11,2),[1], % 0.82/1.19 multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11))),identity)) = multiply(X10,identity)]. % 0.82/1.19 [18=param(13,6),[1], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),X11)),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))]. % 0.82/1.19 [20=param(12,9),[], % 0.82/1.19 multiply(identity,multiply(X10,multiply(multiply(multiply(X10,identity),identity),multiply(multiply(multiply(X10,identity),identity),multiply(multiply(X10,identity),identity))))) = identity]. % 0.82/1.19 [23=param(11,14),[], % 0.82/1.19 multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11))),identity),identity)) = multiply(multiply(X10,identity),identity)]. % 0.82/1.19 [24=param(11,20),[1], % 0.82/1.19 multiply(identity,multiply(multiply(X10,multiply(multiply(multiply(X10,identity),identity),multiply(multiply(multiply(X10,identity),identity),multiply(multiply(X10,identity),identity)))),identity)) = identity]. % 0.82/1.19 [25=param(12,24),[1,1,1,1,1], % 0.82/1.19 multiply(X10,multiply(multiply(multiply(X10,identity),identity),multiply(multiply(multiply(X10,identity),identity),multiply(multiply(X10,identity),identity)))) = identity]. % 0.82/1.19 [26=param(12,23),[1,1,11], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(multiply(X10,identity),identity),identity))) = multiply(multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11))),identity)]. % 0.82/1.19 [27=param(2,18),[1,1], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))),identity)) = multiply(multiply(X10,X10),multiply(multiply(multiply(X10,X10),multiply(X10,X10)),X11))]. % 0.82/1.19 [30=param(27,9),[], % 0.82/1.19 multiply(X10,multiply(multiply(X10,X11),identity)) = multiply(multiply(X10,X10),multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(X11,identity)))]. % 0.82/1.19 [31=param(2,27),[], % 0.82/1.19 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(multiply(X10,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X11,X12),identity))))),identity)),multiply(X12,multiply(X12,X12)))) = X11]. % 0.82/1.19 [35=param(2,30),[1,1], % 0.82/1.19 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(multiply(X10,X11),identity)),identity)) = X11]. % 0.82/1.19 [36=param(35,2),[], % 0.82/1.19 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(X11,identity)),identity)) = multiply(multiply(X10,multiply(multiply(X10,X10),multiply(X11,X12))),multiply(X12,multiply(X12,X12)))]. % 0.82/1.19 [38=param(35,18),[11,11,11,9], % 0.82/1.19 multiply(multiply(X10,multiply(multiply(X10,X10),X11)),identity) = multiply(multiply(X10,X10),multiply(multiply(X10,X11),identity))]. % 0.82/1.19 [39=demod(18),[38], % 0.82/1.19 multiply(X10,multiply(multiply(X10,X10),multiply(multiply(X10,X11),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))]. % 0.82/1.19 [40=param(35,25),[1], % 0.82/1.19 multiply(multiply(multiply(X10,identity),identity),multiply(multiply(multiply(X10,identity),identity),multiply(multiply(X10,identity),identity))) = multiply(multiply(X10,X10),multiply(multiply(X10,identity),identity))]. % 0.82/1.19 [41=param(35,27),[1,1,1,1], % 0.82/1.19 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(X10,multiply(multiply(X10,identity),identity)),identity)) = multiply(X10,X10)]. % 0.82/1.19 [42=param(35,35),[], % 0.82/1.19 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(multiply(X10,X10),multiply(X11,identity)),identity)) = multiply(multiply(X10,multiply(multiply(X10,X11),identity)),identity)]. % 0.82/1.19 [47=param(39,11),[11,1,1,1,1], % 0.82/1.19 multiply(multiply(identity,X10),multiply(multiply(multiply(identity,X10),multiply(identity,X10)),multiply(identity,multiply(multiply(X10,identity),identity)))) = identity]. % 0.82/1.19 [48=param(39,38),[], % 0.82/1.19 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X10,X10),X11),identity)))) = multiply(X10,multiply(multiply(X10,X10),multiply(multiply(X10,X10),multiply(multiply(X10,X11),identity))))]. % 0.82/1.19 [49=param(36,30),[38,39,9], % 0.82/1.19 multiply(multiply(X11,multiply(multiply(X11,X11),multiply(multiply(X11,X10),X12))),multiply(X12,multiply(X12,X12))) = X10]. % 0.82/1.19 [51=param(47,11),[11], % 0.82/1.19 multiply(multiply(identity,multiply(identity,X10)),multiply(multiply(multiply(identity,multiply(identity,X10)),multiply(identity,multiply(identity,X10))),multiply(identity,multiply(identity,multiply(multiply(X10,identity),identity))))) = identity]. % 0.82/1.19 [57=param(2,40),[], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),multiply(X11,multiply(multiply(X12,identity),identity)))),multiply(multiply(X12,X12),multiply(multiply(X12,identity),identity)))) = X11]. % 0.82/1.19 [60=param(42,1),[], % 0.82/1.19 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(multiply(X10,X10),identity),identity)) = multiply(multiply(X10,multiply(multiply(X10,identity),identity)),identity)]. % 0.82/1.19 [66=param(51,11),[11,9], % 0.82/1.19 multiply(multiply(identity,multiply(identity,multiply(identity,X10))),multiply(multiply(multiply(identity,multiply(identity,multiply(identity,X10))),multiply(identity,multiply(identity,multiply(identity,X10)))),X10)) = identity]. % 0.82/1.19 [83=param(57,66),[], % 0.82/1.19 multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X10,multiply(multiply(X11,identity),identity))))),multiply(identity,multiply(multiply(X11,X11),multiply(multiply(X11,identity),identity)))) = X10]. % 0.82/1.19 [84=param(83,60),[], % 0.82/1.19 multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X10,multiply(multiply(multiply(X11,X11),identity),identity))))),multiply(identity,multiply(multiply(X11,multiply(multiply(X11,identity),identity)),identity))) = X10]. % 0.82/1.19 [85=param(12,2),[1], % 0.82/1.19 multiply(identity,multiply(multiply(identity,X10),multiply(multiply(X11,multiply(X11,X11)),multiply(multiply(X11,multiply(X11,X11)),multiply(X11,multiply(X11,X11)))))) = multiply(identity,multiply(identity,multiply(X10,X11)))]. % 0.82/1.19 [88=param(12,49),[85], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(identity,X10),X11))) = multiply(X12,multiply(multiply(X12,X12),multiply(multiply(X12,X10),X11)))]. % 0.82/1.19 [91=param(88,1),[], % 0.82/1.19 multiply(X11,multiply(multiply(X11,X11),multiply(multiply(X11,identity),X10))) = multiply(identity,multiply(identity,multiply(identity,X10)))]. % 0.82/1.19 [103=param(38,91),[11,11,11], % 0.82/1.19 multiply(multiply(X11,X11),multiply(multiply(X11,multiply(multiply(X11,identity),X10)),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(X10,identity))))]. % 0.82/1.19 [104=param(2,103),[1,1], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))),identity)) = multiply(X10,multiply(multiply(X10,identity),X11))]. % 0.82/1.19 [105=demod(27),[104], % 0.82/1.19 multiply(multiply(X10,X10),multiply(multiply(multiply(X10,X10),multiply(X10,X10)),X11)) = multiply(X10,multiply(multiply(X10,identity),X11))]. % 0.82/1.19 [106=demod(30),[105], % 0.82/1.19 multiply(X10,multiply(multiply(X10,X11),identity)) = multiply(X10,multiply(multiply(X10,identity),multiply(X11,identity)))]. % 0.82/1.19 [109=demod(104),[], % 0.82/1.19 multiply(X10,multiply(multiply(X10,multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))),identity)) = multiply(X10,multiply(multiply(X10,identity),X11))]. % 0.82/1.19 [114=demod(31),[109], % 0.82/1.19 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(multiply(X10,identity),multiply(X11,X12))),multiply(X12,multiply(X12,X12)))) = X11]. % 0.82/1.19 [115=param(35,103),[11,11,11,9], % 0.82/1.19 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(multiply(X10,X10),X11),identity)) = multiply(multiply(X10,multiply(multiply(X10,identity),X11)),identity)]. % 0.82/1.19 [116=param(39,103),[], % 0.82/1.19 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X10,identity),X11),identity)))) = multiply(X10,multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity)))))]. % 0.82/1.19 [119=param(35,106),[-42,105], % 0.82/1.19 multiply(X10,multiply(multiply(X10,identity),multiply(multiply(multiply(X10,X10),multiply(multiply(multiply(X10,identity),multiply(X11,identity)),identity)),identity))) = multiply(multiply(X10,X11),identity)]. % 0.82/1.19 [120=param(106,38),[39], % 0.82/1.19 multiply(X11,multiply(multiply(X11,identity),multiply(multiply(multiply(X11,X11),X10),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(X10,identity))))]. % 0.82/1.19 [121=demod(119),[120,9], % 0.82/1.19 multiply(multiply(X10,identity),multiply(X11,identity)) = multiply(multiply(X10,X11),identity)]. % 0.82/1.19 [132=demod(41),[-121], % 0.82/1.19 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(X10,identity),multiply(multiply(multiply(X10,identity),identity),identity))) = multiply(X10,X10)]. % 0.82/1.19 [133=demod(38),[-121], % 0.82/1.19 multiply(multiply(X10,identity),multiply(multiply(multiply(X10,X10),X11),identity)) = multiply(multiply(X10,X10),multiply(multiply(X10,X11),identity))]. % 0.82/1.19 [134=demod(115),[-121], % 0.82/1.19 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(multiply(X10,X10),X11),identity)) = multiply(multiply(X10,identity),multiply(multiply(multiply(X10,identity),X11),identity))]. % 0.82/1.19 [143=demod(26),[-121,11,11,-121], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(multiply(X10,identity),identity),identity))) = multiply(multiply(identity,multiply(identity,multiply(multiply(X10,X11),identity))),multiply(multiply(X11,identity),multiply(multiply(X11,X11),identity)))]. % 0.82/1.19 [156=demod(84),[-121], % 0.82/1.19 multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X10,multiply(multiply(multiply(X11,X11),identity),identity))))),multiply(identity,multiply(multiply(X11,identity),multiply(multiply(multiply(X11,identity),identity),identity)))) = X10]. % 0.82/1.19 [185=param(121,121),[], % 0.82/1.19 multiply(multiply(multiply(X10,identity),multiply(X11,identity)),multiply(X12,identity)) = multiply(multiply(multiply(X10,X11),X12),identity)]. % 0.82/1.19 [209=param(48,121),[116,-88], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X10,identity)),multiply(multiply(multiply(X10,identity),X11),identity)))) = multiply(multiply(X10,X10),multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity)))))]. % 0.82/1.19 [216=param(121,133),[-121], % 0.82/1.19 multiply(multiply(multiply(X10,identity),identity),multiply(multiply(multiply(multiply(X10,X10),X11),identity),identity)) = multiply(multiply(multiply(X10,X10),identity),multiply(multiply(multiply(X10,X11),identity),identity))]. % 0.82/1.19 [217=param(105,2),[105], % 0.82/1.19 multiply(X10,multiply(multiply(X10,identity),multiply(multiply(multiply(X10,X10),multiply(multiply(multiply(X10,X10),identity),multiply(X11,X12))),multiply(X12,multiply(X12,X12))))) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [219=param(105,88),[], % 0.82/1.19 multiply(X10,multiply(multiply(X10,identity),multiply(multiply(multiply(X10,X10),X11),X12))) = multiply(identity,multiply(identity,multiply(multiply(identity,X11),X12)))]. % 0.82/1.19 [221=demod(217),[219], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(X10,X10),identity),multiply(X11,X12))),multiply(X12,multiply(X12,X12))))) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [226=param(219,121),[1], % 0.82/1.19 multiply(X10,multiply(multiply(X10,identity),multiply(multiply(multiply(X10,identity),multiply(X10,identity)),X11))) = multiply(identity,multiply(identity,multiply(identity,X11)))]. % 0.82/1.19 [251=param(48,185),[9,-121,-88], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X10,identity)),multiply(multiply(multiply(X10,identity),identity),multiply(multiply(X11,identity),identity))))) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [260=param(185,39),[11,11,11,9,-185], % 0.82/1.19 multiply(multiply(multiply(X11,identity),multiply(X12,identity)),multiply(multiply(multiply(multiply(X11,X12),identity),multiply(multiply(X11,X12),identity)),multiply(multiply(multiply(multiply(X11,X12),X10),identity),identity))) = X10]. % 0.82/1.19 [269=param(226,88),[], % 0.82/1.19 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X10,identity),X11),X12)))) = multiply(X10,multiply(identity,multiply(identity,multiply(multiply(identity,X11),X12))))]. % 0.82/1.19 [273=param(269,40),[1,269,1,9], % 0.82/1.19 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X10,X10),multiply(multiply(X10,identity),identity))))) = multiply(X10,multiply(X10,X10))]. % 0.82/1.19 [274=param(269,121),[], % 0.82/1.19 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X10,X11),identity),X12)))) = multiply(X10,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X11,identity)),X12))))]. % 0.82/1.19 [286=param(11,273),[-121,11,11,-121,274,209,1,1,1,1], % 0.82/1.19 multiply(multiply(X10,identity),multiply(multiply(X10,X10),identity)) = multiply(X10,multiply(multiply(X10,X10),identity))]. % 0.82/1.19 [292=demod(143),[286], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(multiply(X10,identity),identity),identity))) = multiply(multiply(identity,multiply(identity,multiply(multiply(X10,X11),identity))),multiply(X11,multiply(multiply(X11,X11),identity)))]. % 0.82/1.19 [297=param(2,286),[-36,-121,91,9], % 0.82/1.19 multiply(X10,identity) = X10]. % 0.82/1.19 [298=demod(221),[297], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X10,X10),multiply(X11,X12))),multiply(X12,multiply(X12,X12))))) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [301=demod(292),[297,297,297,297,297], % 0.82/1.19 multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11))) = multiply(identity,multiply(identity,X10))]. % 0.82/1.19 [302=demod(12),[301], % 0.82/1.19 multiply(identity,multiply(identity,multiply(identity,X10))) = X10]. % 0.82/1.19 [304=demod(66),[302,302,302], % 0.82/1.19 multiply(X10,multiply(multiply(X10,X10),X10)) = identity]. % 0.82/1.19 [307=demod(273),[297,297,302], % 0.82/1.19 multiply(multiply(X10,X10),X10) = multiply(X10,multiply(X10,X10))]. % 0.82/1.19 [308=demod(304),[307], % 0.82/1.19 multiply(X10,multiply(X10,multiply(X10,X10))) = identity]. % 0.82/1.19 [310=demod(269),[297,302], % 0.82/1.19 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(identity,multiply(identity,multiply(multiply(identity,X11),X12))))]. % 0.82/1.19 [319=demod(216),[297,297,297,297,297,297,297], % 0.82/1.19 multiply(multiply(X10,X10),multiply(X10,X11)) = multiply(X10,multiply(multiply(X10,X10),X11))]. % 0.82/1.19 [325=demod(134),[319,307,308,297,297,297,297], % 0.82/1.19 multiply(identity,multiply(multiply(X10,X10),X11)) = multiply(X10,multiply(X10,X11))]. % 0.82/1.19 [326=demod(298),[325], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(X10,multiply(X10,multiply(X11,X12))),multiply(X12,multiply(X12,X12))))) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [327=demod(132),[319,307,308,297,297,297,297], % 0.82/1.19 multiply(identity,multiply(X10,X10)) = multiply(X10,X10)]. % 0.82/1.19 [328=demod(114),[297], % 0.82/1.19 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(X10,multiply(X11,X12))),multiply(X12,multiply(X12,X12)))) = X11]. % 0.82/1.19 [329=demod(105),[319,307,308,297], % 0.82/1.19 multiply(multiply(X10,X10),multiply(identity,X11)) = multiply(X10,multiply(X10,X11))]. % 0.82/1.19 [333=demod(251),[297,297,297,297,297], % 0.82/1.19 multiply(identity,multiply(identity,multiply(multiply(identity,X10),multiply(X10,X11)))) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [336=demod(156),[297,297,302,297,297,297,297,327], % 0.82/1.19 multiply(multiply(X10,multiply(X11,X11)),multiply(X11,X11)) = X10]. % 0.82/1.19 [342=demod(260),[297,297,297,297,297,297,319,-333], % 0.82/1.19 multiply(multiply(X10,X11),multiply(multiply(X10,X11),multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X10,X11)),multiply(multiply(X10,X11),X12)))))) = X12]. % 0.82/1.19 [352=param(302,85),[302], % 0.82/1.19 multiply(multiply(identity,X10),multiply(multiply(X11,multiply(X11,X11)),multiply(multiply(X11,multiply(X11,X11)),multiply(X11,multiply(X11,X11))))) = multiply(identity,multiply(X10,X11))]. % 0.82/1.19 [356=param(301,307),[327,327], % 0.82/1.19 multiply(multiply(identity,multiply(identity,multiply(X10,multiply(X10,X10)))),multiply(X10,multiply(X10,X10))) = multiply(X10,X10)]. % 0.82/1.19 [358=param(301,327),[327,319,319,307,308,297], % 0.82/1.19 multiply(identity,multiply(identity,X10)) = X10]. % 0.82/1.19 [363=demod(310),[358], % 0.82/1.19 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(multiply(identity,X11),X12))]. % 0.82/1.19 [366=demod(333),[-363,-363], % 0.82/1.19 multiply(multiply(identity,X10),multiply(X10,X11)) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [367=demod(342),[-363,-363], % 0.82/1.19 multiply(multiply(X10,X11),multiply(multiply(X10,X11),multiply(multiply(identity,multiply(X10,X11)),multiply(multiply(X10,X11),X12)))) = X12]. % 0.82/1.19 [368=demod(326),[358], % 0.82/1.19 multiply(multiply(X10,multiply(X10,multiply(X11,X12))),multiply(X12,multiply(X12,X12))) = multiply(multiply(X10,X10),X11)]. % 0.82/1.19 [369=demod(328),[368], % 0.82/1.19 multiply(multiply(X10,X10),multiply(multiply(X10,X10),X11)) = X11]. % 0.82/1.19 [370=demod(356),[358], % 0.82/1.19 multiply(multiply(X10,multiply(X10,X10)),multiply(X10,multiply(X10,X10))) = multiply(X10,X10)]. % 0.82/1.19 [371=demod(352),[370,336], % 0.82/1.19 multiply(multiply(identity,X10),X11) = multiply(identity,multiply(X10,X11))]. % 0.82/1.19 [372=demod(367),[371], % 0.82/1.19 multiply(multiply(X10,X11),multiply(multiply(X10,X11),multiply(identity,multiply(multiply(X10,X11),multiply(multiply(X10,X11),X12))))) = X12]. % 0.82/1.19 [373=demod(366),[371], % 0.82/1.19 multiply(multiply(X10,X10),X11) = multiply(identity,multiply(X10,multiply(X10,X11)))]. % 0.82/1.19 [380=demod(329),[373], % 0.82/1.19 multiply(identity,multiply(X10,multiply(X10,multiply(identity,X11)))) = multiply(X10,multiply(X10,X11))]. % 0.82/1.19 [384=demod(369),[373,373,380], % 0.82/1.19 multiply(X10,multiply(X10,multiply(X10,multiply(X10,X11)))) = X11]. % 0.82/1.19 [387=demod(319),[373,373], % 0.82/1.19 multiply(identity,multiply(X10,multiply(X10,multiply(X10,X11)))) = multiply(X10,multiply(identity,multiply(X10,multiply(X10,X11))))]. % 0.82/1.19 [388=demod(372),[-387,-387,384], % 0.82/1.19 multiply(identity,X10) = X10]. % 0.82/1.19 [399=demod(363),[388], % 0.82/1.19 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 0.82/1.19 [400=param(4,399),[3], % 0.82/1.19 thmtrue = thmfalse]. % 0.82/1.19 % SZS output end CNFRefutation % 0.82/1.19 Space: 1145 KB %------------------------------------------------------------------------------