%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP120-1 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n010.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:31 EDT 2022 % Result : Unsatisfiable 0.58s 0.96s % Output : CNFRefutation 0.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.07 % Problem : GRP120-1 : TPTP v8.1.0. Released v1.2.0. % 0.04/0.07 % Command : fiesta-wrapper %s % 0.06/0.26 % Computer : n010.cluster.edu % 0.06/0.26 % Model : x86_64 x86_64 % 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.26 % Memory : 8042.1875MB % 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.26 % WCLimit : 600 % 0.06/0.26 % DateTime : Mon Jun 13 03:59:39 EDT 2022 % 0.06/0.26 % CPUTime : % 0.58/0.96 Theorem Proved. % 0.58/0.96 % SZS status Unsatisfiable % 0.58/0.96 % SZS output start CNFRefutation % 0.58/0.96 [1=axiom,[], % 0.58/0.96 multiply(identity,identity) = identity]. % 0.58/0.96 [2=axiom,[], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),multiply(X11,X12))),multiply(X12,multiply(X12,X12)))) = X11]. % 0.58/0.96 [3=axiom,[], % 0.58/0.96 thtop(X10,X10) = thmfalse]. % 0.58/0.96 [4=axiom,[], % 0.58/0.96 thtop(multiply(identity,a),a) = thmtrue]. % 0.58/0.96 [6=param(2,1),[1], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),multiply(X11,identity))),identity)) = X11]. % 0.58/0.96 [7=param(6,1),[], % 0.58/0.96 multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X10,identity))),identity)) = X10]. % 0.58/0.96 [8=param(7,6),[1], % 0.58/0.96 multiply(identity,multiply(multiply(identity,X10),identity)) = multiply(identity,multiply(identity,multiply(X10,identity)))]. % 0.58/0.96 [9=demod(7),[8,8], % 0.58/0.96 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X10,identity),identity)))) = X10]. % 0.58/0.96 [10=param(8,8),[8,8,9], % 0.58/0.96 multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X10),identity),identity))) = X10]. % 0.58/0.96 [11=param(8,10),[8,9], % 0.58/0.96 multiply(multiply(identity,X10),identity) = multiply(identity,multiply(X10,identity))]. % 0.58/0.96 [12=param(2,1),[], % 0.58/0.96 multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11)))) = X10]. % 0.58/0.96 [13=param(2,11),[1,1], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),multiply(identity,multiply(X11,identity)))),identity)) = multiply(identity,X11)]. % 0.58/0.96 [14=param(11,2),[1], % 0.58/0.96 multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11))),identity)) = multiply(X10,identity)]. % 0.58/0.96 [18=param(13,6),[1], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(multiply(X10,X10),X11)),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))]. % 0.58/0.96 [20=param(12,9),[], % 0.58/0.96 multiply(identity,multiply(X10,multiply(multiply(multiply(X10,identity),identity),multiply(multiply(multiply(X10,identity),identity),multiply(multiply(X10,identity),identity))))) = identity]. % 0.58/0.96 [23=param(11,14),[], % 0.58/0.96 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.58/0.96 [24=param(11,20),[1], % 0.58/0.96 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.58/0.96 [25=param(12,24),[1,1,1,1,1], % 0.58/0.96 multiply(X10,multiply(multiply(multiply(X10,identity),identity),multiply(multiply(multiply(X10,identity),identity),multiply(multiply(X10,identity),identity)))) = identity]. % 0.58/0.96 [26=param(12,23),[1,1,11], % 0.58/0.96 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.58/0.96 [27=param(2,18),[1,1], % 0.58/0.96 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.58/0.96 [30=param(27,9),[], % 0.58/0.96 multiply(X10,multiply(multiply(X10,X11),identity)) = multiply(multiply(X10,X10),multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(X11,identity)))]. % 0.58/0.96 [31=param(2,27),[], % 0.58/0.96 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.58/0.96 [35=param(2,30),[1,1], % 0.58/0.96 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(multiply(X10,X11),identity)),identity)) = X11]. % 0.58/0.96 [36=param(35,2),[], % 0.58/0.96 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.58/0.96 [38=param(35,18),[11,11,11,9], % 0.58/0.96 multiply(multiply(X10,multiply(multiply(X10,X10),X11)),identity) = multiply(multiply(X10,X10),multiply(multiply(X10,X11),identity))]. % 0.58/0.96 [39=demod(18),[38], % 0.58/0.96 multiply(X10,multiply(multiply(X10,X10),multiply(multiply(X10,X11),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))]. % 0.58/0.96 [40=param(35,25),[1], % 0.58/0.96 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.58/0.96 [41=param(35,27),[1,1,1,1], % 0.58/0.96 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(X10,multiply(multiply(X10,identity),identity)),identity)) = multiply(X10,X10)]. % 0.58/0.96 [42=param(35,35),[], % 0.58/0.96 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.58/0.96 [47=param(39,11),[11,1,1,1,1], % 0.58/0.96 multiply(multiply(identity,X10),multiply(multiply(multiply(identity,X10),multiply(identity,X10)),multiply(identity,multiply(multiply(X10,identity),identity)))) = identity]. % 0.58/0.96 [48=param(39,38),[], % 0.58/0.96 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.58/0.96 [49=param(36,30),[38,39,9], % 0.58/0.96 multiply(multiply(X11,multiply(multiply(X11,X11),multiply(multiply(X11,X10),X12))),multiply(X12,multiply(X12,X12))) = X10]. % 0.58/0.96 [51=param(47,11),[11], % 0.58/0.96 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.58/0.96 [66=param(51,11),[11,9], % 0.58/0.96 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.58/0.96 [85=param(12,2),[1], % 0.58/0.96 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.58/0.96 [90=param(12,49),[85], % 0.58/0.96 multiply(identity,multiply(identity,multiply(multiply(identity,X10),X11))) = multiply(X12,multiply(multiply(X12,X12),multiply(multiply(X12,X10),X11)))]. % 0.58/0.96 [91=param(90,1),[], % 0.58/0.96 multiply(X11,multiply(multiply(X11,X11),multiply(multiply(X11,identity),X10))) = multiply(identity,multiply(identity,multiply(identity,X10)))]. % 0.58/0.96 [92=param(90,2),[1], % 0.58/0.96 multiply(X11,multiply(multiply(X11,X11),multiply(multiply(X11,multiply(identity,multiply(X10,X12))),multiply(X12,multiply(X12,X12))))) = multiply(identity,X10)]. % 0.58/0.96 [103=param(38,91),[11,11,11], % 0.58/0.96 multiply(multiply(X11,X11),multiply(multiply(X11,multiply(multiply(X11,identity),X10)),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(X10,identity))))]. % 0.58/0.96 [104=param(2,103),[1,1], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))),identity)) = multiply(X10,multiply(multiply(X10,identity),X11))]. % 0.58/0.96 [105=demod(27),[104], % 0.58/0.96 multiply(multiply(X10,X10),multiply(multiply(multiply(X10,X10),multiply(X10,X10)),X11)) = multiply(X10,multiply(multiply(X10,identity),X11))]. % 0.58/0.96 [106=demod(30),[105], % 0.58/0.96 multiply(X10,multiply(multiply(X10,X11),identity)) = multiply(X10,multiply(multiply(X10,identity),multiply(X11,identity)))]. % 0.58/0.96 [109=demod(104),[], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(identity,multiply(identity,multiply(identity,multiply(X11,identity))))),identity)) = multiply(X10,multiply(multiply(X10,identity),X11))]. % 0.58/0.96 [114=demod(31),[109], % 0.58/0.96 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(multiply(X10,identity),multiply(X11,X12))),multiply(X12,multiply(X12,X12)))) = X11]. % 0.58/0.96 [115=param(35,103),[11,11,11,9], % 0.58/0.96 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.58/0.96 [116=param(39,103),[], % 0.58/0.96 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.58/0.96 [119=param(35,106),[-42,105], % 0.58/0.96 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.58/0.96 [120=param(106,38),[39], % 0.58/0.96 multiply(X11,multiply(multiply(X11,identity),multiply(multiply(multiply(X11,X11),X10),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(X10,identity))))]. % 0.58/0.96 [121=demod(119),[120,9], % 0.58/0.96 multiply(multiply(X10,identity),multiply(X11,identity)) = multiply(multiply(X10,X11),identity)]. % 0.58/0.96 [132=demod(41),[-121], % 0.58/0.96 multiply(multiply(multiply(X10,X10),multiply(X10,X10)),multiply(multiply(X10,identity),multiply(multiply(multiply(X10,identity),identity),identity))) = multiply(X10,X10)]. % 0.58/0.96 [133=demod(38),[-121], % 0.58/0.96 multiply(multiply(X10,identity),multiply(multiply(multiply(X10,X10),X11),identity)) = multiply(multiply(X10,X10),multiply(multiply(X10,X11),identity))]. % 0.58/0.96 [134=demod(115),[-121], % 0.58/0.96 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.58/0.96 [143=demod(26),[-121,11,11,-121], % 0.58/0.96 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.58/0.96 [208=param(48,121),[116,-90], % 0.58/0.96 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.58/0.96 [216=param(121,133),[-121], % 0.58/0.96 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.58/0.96 [217=param(105,2),[105], % 0.58/0.96 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.58/0.96 [218=param(2,105),[], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(X10,multiply(multiply(X10,identity),X11))),multiply(X11,multiply(X11,X11)))) = multiply(multiply(X10,X10),multiply(X10,X10))]. % 0.58/0.96 [219=param(105,90),[], % 0.58/0.96 multiply(X10,multiply(multiply(X10,identity),multiply(multiply(multiply(X10,X10),X11),X12))) = multiply(identity,multiply(identity,multiply(multiply(identity,X11),X12)))]. % 0.58/0.96 [221=demod(217),[219], % 0.58/0.96 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.58/0.96 [226=param(219,121),[1], % 0.58/0.96 multiply(X10,multiply(multiply(X10,identity),multiply(multiply(multiply(X10,identity),multiply(X10,identity)),X11))) = multiply(identity,multiply(identity,multiply(identity,X11)))]. % 0.58/0.96 [269=param(226,90),[], % 0.58/0.96 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.58/0.96 [277=param(269,40),[1,269,1,9], % 0.58/0.96 multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X10,X10),multiply(multiply(X10,identity),identity))))) = multiply(X10,multiply(X10,X10))]. % 0.58/0.96 [278=param(269,121),[], % 0.58/0.96 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.58/0.96 [286=param(11,277),[-121,11,11,-121,278,208,1,1,1,1], % 0.58/0.96 multiply(multiply(X10,identity),multiply(multiply(X10,X10),identity)) = multiply(X10,multiply(multiply(X10,X10),identity))]. % 0.58/0.96 [292=demod(143),[286], % 0.58/0.96 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.58/0.96 [299=param(2,286),[-36,-121,91,9], % 0.58/0.96 multiply(X10,identity) = X10]. % 0.58/0.96 [300=demod(221),[299], % 0.58/0.96 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.58/0.96 [303=demod(292),[299,299,299,299,299], % 0.58/0.96 multiply(multiply(identity,multiply(identity,multiply(X10,X11))),multiply(X11,multiply(X11,X11))) = multiply(identity,multiply(identity,X10))]. % 0.58/0.96 [304=demod(12),[303], % 0.58/0.96 multiply(identity,multiply(identity,multiply(identity,X10))) = X10]. % 0.58/0.96 [306=demod(66),[304,304,304], % 0.58/0.96 multiply(X10,multiply(multiply(X10,X10),X10)) = identity]. % 0.58/0.96 [309=demod(277),[299,299,304], % 0.58/0.96 multiply(multiply(X10,X10),X10) = multiply(X10,multiply(X10,X10))]. % 0.58/0.96 [310=demod(306),[309], % 0.58/0.96 multiply(X10,multiply(X10,multiply(X10,X10))) = identity]. % 0.58/0.96 [312=demod(269),[299,304], % 0.58/0.96 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(identity,multiply(identity,multiply(multiply(identity,X11),X12))))]. % 0.58/0.96 [320=demod(218),[299], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(X10,multiply(X10,X11))),multiply(X11,multiply(X11,X11)))) = multiply(multiply(X10,X10),multiply(X10,X10))]. % 0.58/0.96 [321=demod(216),[299,299,299,299,299,299,299], % 0.58/0.96 multiply(multiply(X10,X10),multiply(X10,X11)) = multiply(X10,multiply(multiply(X10,X10),X11))]. % 0.58/0.96 [322=demod(320),[321,309,310], % 0.58/0.96 multiply(X10,multiply(multiply(X10,multiply(X10,multiply(X10,X11))),multiply(X11,multiply(X11,X11)))) = identity]. % 0.58/0.96 [327=demod(134),[321,309,310,299,299,299,299], % 0.58/0.96 multiply(identity,multiply(multiply(X10,X10),X11)) = multiply(X10,multiply(X10,X11))]. % 0.58/0.96 [328=demod(300),[327], % 0.58/0.96 multiply(identity,multiply(identity,multiply(multiply(X10,multiply(X10,multiply(X11,X12))),multiply(X12,multiply(X12,X12))))) = multiply(multiply(X10,X10),X11)]. % 0.58/0.96 [329=demod(132),[321,309,310,299,299,299,299], % 0.58/0.96 multiply(identity,multiply(X10,X10)) = multiply(X10,X10)]. % 0.58/0.96 [330=demod(114),[299], % 0.58/0.96 multiply(multiply(X10,X10),multiply(multiply(X10,multiply(X10,multiply(X11,X12))),multiply(X12,multiply(X12,X12)))) = X11]. % 0.58/0.96 [331=demod(105),[321,309,310,299], % 0.58/0.96 multiply(multiply(X10,X10),multiply(identity,X11)) = multiply(X10,multiply(X10,X11))]. % 0.58/0.96 [349=param(85,329),[327,327], % 0.58/0.96 multiply(X10,multiply(X10,multiply(multiply(X11,multiply(X11,X11)),multiply(multiply(X11,multiply(X11,X11)),multiply(X11,multiply(X11,X11)))))) = multiply(identity,multiply(X10,multiply(X10,X11)))]. % 0.58/0.96 [352=param(90,92),[299,303,321,331], % 0.58/0.96 multiply(identity,multiply(identity,X10)) = multiply(X11,multiply(X11,multiply(X11,multiply(X11,multiply(identity,X10)))))]. % 0.58/0.96 [358=param(331,304),[], % 0.58/0.96 multiply(multiply(X10,X10),X11) = multiply(X10,multiply(X10,multiply(identity,multiply(identity,X11))))]. % 0.58/0.96 [359=demod(330),[358], % 0.58/0.96 multiply(X10,multiply(X10,multiply(identity,multiply(identity,multiply(multiply(X10,multiply(X10,multiply(X11,X12))),multiply(X12,multiply(X12,X12))))))) = X11]. % 0.58/0.96 [375=demod(309),[358], % 0.58/0.96 multiply(X10,multiply(X10,multiply(identity,multiply(identity,X10)))) = multiply(X10,multiply(X10,X10))]. % 0.58/0.96 [378=demod(328),[358], % 0.58/0.96 multiply(identity,multiply(identity,multiply(multiply(X10,multiply(X10,multiply(X11,X12))),multiply(X12,multiply(X12,X12))))) = multiply(X10,multiply(X10,multiply(identity,multiply(identity,X11))))]. % 0.58/0.96 [379=demod(359),[378], % 0.58/0.96 multiply(X10,multiply(X10,multiply(X10,multiply(X10,multiply(identity,multiply(identity,X11)))))) = X11]. % 0.58/0.96 [380=demod(327),[358], % 0.58/0.96 multiply(identity,multiply(X10,multiply(X10,multiply(identity,multiply(identity,X11))))) = multiply(X10,multiply(X10,X11))]. % 0.58/0.96 [386=param(303,329),[329,358], % 0.58/0.96 multiply(X10,multiply(X10,multiply(identity,multiply(identity,multiply(X10,multiply(X10,X10)))))) = multiply(identity,multiply(identity,X10))]. % 0.58/0.96 [389=param(358,358),[329,329,310,358,304,358], % 0.58/0.96 multiply(X11,multiply(X11,multiply(identity,multiply(identity,multiply(X11,multiply(X11,multiply(identity,X10))))))) = multiply(identity,X10)]. % 0.58/0.96 [432=param(312,304),[], % 0.58/0.96 multiply(multiply(X10,multiply(identity,multiply(identity,X11))),X12) = multiply(X10,multiply(identity,multiply(identity,multiply(X11,X12))))]. % 0.58/0.96 [435=param(312,329),[358,380], % 0.58/0.96 multiply(multiply(X10,multiply(X11,X11)),X12) = multiply(X10,multiply(identity,multiply(X11,multiply(X11,X12))))]. % 0.58/0.96 [437=demod(349),[435,310,299,435], % 0.58/0.96 multiply(X10,multiply(X10,multiply(X11,multiply(identity,multiply(X11,multiply(X11,multiply(X11,multiply(identity,X11)))))))) = multiply(identity,multiply(X10,multiply(X10,X11)))]. % 0.58/0.96 [478=param(322,375),[310,299,432,375,432,386,304], % 0.58/0.96 multiply(X10,multiply(X10,multiply(X10,multiply(identity,X10)))) = identity]. % 0.58/0.96 [479=demod(437),[478,299,299], % 0.58/0.96 multiply(identity,multiply(X10,multiply(X10,X11))) = multiply(X10,multiply(X10,X11))]. % 0.58/0.96 [492=demod(389),[479,479], % 0.58/0.96 multiply(X10,multiply(X10,multiply(X10,multiply(X10,multiply(identity,X11))))) = multiply(identity,X11)]. % 0.58/0.96 [494=demod(352),[492], % 0.58/0.96 multiply(identity,multiply(identity,X10)) = multiply(identity,X10)]. % 0.58/0.96 [549=demod(379),[494,492], % 0.58/0.96 multiply(identity,X10) = X10]. % 0.58/0.96 [570=param(4,549),[3], % 0.58/0.96 thmtrue = thmfalse]. % 0.58/0.96 % SZS output end CNFRefutation % 0.58/0.96 Space: 1387 KB %------------------------------------------------------------------------------