%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : BOO022-1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n032.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.69s 1.14s % Output : CNFRefutation 0.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : BOO022-1 : TPTP v8.1.0. Released v2.2.0. % 0.10/0.12 % Command : fiesta-wrapper %s % 0.11/0.32 % Computer : n032.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Wed Jun 1 22:52:00 EDT 2022 % 0.11/0.32 % CPUTime : % 0.69/1.14 Theorem Proved. % 0.69/1.14 % SZS status Unsatisfiable % 0.69/1.14 % SZS output start CNFRefutation % 0.69/1.14 [1=axiom,[], % 0.69/1.14 multiply(X10,inverse(X10)) = n0]. % 0.69/1.14 [2=axiom,[], % 0.69/1.14 add(X10,multiply(X11,X12)) = multiply(add(X11,X10),add(X12,X10))]. % 0.69/1.14 [3=axiom,[], % 0.69/1.14 add(multiply(X10,X11),X11) = X11]. % 0.69/1.14 [4=axiom,[], % 0.69/1.14 add(X10,inverse(X10)) = n1]. % 0.69/1.14 [5=axiom,[], % 0.69/1.14 add(multiply(X11,X10),multiply(X12,X10)) = multiply(X10,add(X11,X12))]. % 0.69/1.14 [6=axiom,[], % 0.69/1.14 multiply(add(X10,X11),X11) = X11]. % 0.69/1.14 [7=axiom,[], % 0.69/1.14 thtop(X10,X10) = thmfalse]. % 0.69/1.14 [8=axiom,[], % 0.69/1.14 thtop(multiply(multiply(a,b),c),multiply(a,multiply(b,c))) = thmtrue]. % 0.69/1.14 [9=param(6,4),[], % 0.69/1.14 multiply(n1,inverse(X10)) = inverse(X10)]. % 0.69/1.14 [10=param(2,1),[], % 0.69/1.14 add(X10,n0) = multiply(add(X11,X10),add(inverse(X11),X10))]. % 0.69/1.14 [13=param(2,4),[], % 0.69/1.14 multiply(n1,add(X10,inverse(X11))) = add(inverse(X11),multiply(X11,X10))]. % 0.69/1.14 [15=param(9,1),[], % 0.69/1.14 inverse(n1) = n0]. % 0.69/1.14 [16=param(2,9),[], % 0.69/1.14 add(X10,inverse(X11)) = multiply(add(n1,X10),add(inverse(X11),X10))]. % 0.69/1.14 [17=param(1,15),[], % 0.69/1.14 multiply(n1,n0) = n0]. % 0.69/1.14 [18=param(4,15),[], % 0.69/1.14 add(n1,n0) = n1]. % 0.69/1.14 [19=param(3,1),[], % 0.69/1.14 add(n0,inverse(X10)) = inverse(X10)]. % 0.69/1.14 [20=param(3,2),[], % 0.69/1.14 add(add(X10,multiply(X11,X12)),add(X12,X10)) = add(X12,X10)]. % 0.69/1.14 [23=param(3,6),[], % 0.69/1.14 add(X10,X10) = X10]. % 0.69/1.14 [24=param(6,3),[], % 0.69/1.14 multiply(X10,X10) = X10]. % 0.69/1.14 [25=param(2,24),[24], % 0.69/1.14 add(X10,X11) = add(X11,X10)]. % 0.69/1.14 [26=demod(3),[], % 0.69/1.14 add(multiply(X10,X11),X11) = X11]. % 0.69/1.14 [27=demod(18),[], % 0.69/1.14 add(n1,n0) = n1]. % 0.69/1.14 [29=param(2,27),[], % 0.69/1.14 multiply(add(X10,n0),n1) = add(n0,multiply(X10,n1))]. % 0.69/1.14 [30=param(5,1),[], % 0.69/1.14 add(n0,multiply(X10,inverse(X11))) = multiply(inverse(X11),add(X11,X10))]. % 0.69/1.14 [31=param(5,1),[], % 0.69/1.14 add(multiply(X10,inverse(X11)),n0) = multiply(inverse(X11),add(X10,X11))]. % 0.69/1.14 [34=param(6,5),[], % 0.69/1.14 multiply(multiply(X10,add(X11,X12)),multiply(X12,X10)) = multiply(X12,X10)]. % 0.69/1.14 [36=param(5,24),[], % 0.69/1.14 add(X10,multiply(X11,X10)) = multiply(X10,add(X10,X11))]. % 0.69/1.14 [39=param(5,24),[26], % 0.69/1.14 multiply(X10,add(X11,X10)) = X10]. % 0.69/1.14 [44=param(2,23),[6,36], % 0.69/1.14 multiply(X10,add(X10,X11)) = X10]. % 0.69/1.14 [45=demod(36),[44], % 0.69/1.14 add(X10,multiply(X11,X10)) = X10]. % 0.69/1.14 [48=param(23,5),[23], % 0.69/1.14 multiply(X10,X11) = multiply(X11,X10)]. % 0.69/1.14 [51=demod(29),[48], % 0.69/1.14 multiply(n1,add(X10,n0)) = add(n0,multiply(X10,n1))]. % 0.69/1.14 [52=demod(17),[48], % 0.69/1.14 multiply(n0,n1) = n0]. % 0.69/1.14 [54=param(2,52),[], % 0.69/1.14 add(X10,n0) = multiply(add(n0,X10),add(n1,X10))]. % 0.69/1.14 [55=demod(31),[], % 0.69/1.14 add(multiply(X10,inverse(X11)),n0) = multiply(inverse(X11),add(X10,X11))]. % 0.69/1.14 [56=param(5,52),[], % 0.69/1.14 add(n0,multiply(X10,n1)) = multiply(n1,add(n0,X10))]. % 0.69/1.14 [57=demod(51),[56], % 0.69/1.14 multiply(n1,add(X10,n0)) = multiply(n1,add(n0,X10))]. % 0.69/1.14 [60=param(10,4),[23,9], % 0.69/1.14 add(inverse(X10),n0) = inverse(X10)]. % 0.69/1.14 [62=param(10,4),[48,60], % 0.69/1.14 multiply(n1,add(X10,inverse(inverse(X10)))) = inverse(inverse(X10))]. % 0.69/1.14 [63=param(10,23),[39], % 0.69/1.14 add(X10,n0) = X10]. % 0.69/1.14 [64=demod(57),[63], % 0.69/1.14 multiply(n1,add(n0,X10)) = multiply(n1,X10)]. % 0.69/1.14 [66=demod(54),[63], % 0.69/1.14 multiply(add(n0,X10),add(n1,X10)) = X10]. % 0.69/1.14 [68=demod(10),[63], % 0.69/1.14 multiply(add(X11,X10),add(inverse(X11),X10)) = X10]. % 0.69/1.14 [69=demod(55),[63], % 0.69/1.14 multiply(inverse(X11),add(X10,X11)) = multiply(X10,inverse(X11))]. % 0.69/1.14 [70=param(2,63),[63], % 0.69/1.14 add(n0,multiply(X10,X11)) = multiply(X10,X11)]. % 0.69/1.14 [71=demod(30),[70], % 0.69/1.14 multiply(inverse(X11),add(X11,X10)) = multiply(X10,inverse(X11))]. % 0.69/1.14 [74=param(19,4),[], % 0.69/1.14 inverse(n0) = n1]. % 0.69/1.14 [75=param(13,4),[24,24], % 0.69/1.14 add(inverse(X10),X10) = n1]. % 0.69/1.14 [77=param(4,74),[], % 0.69/1.14 add(n0,n1) = n1]. % 0.69/1.14 [78=param(2,77),[39], % 0.69/1.14 add(n1,multiply(n0,X10)) = n1]. % 0.69/1.14 [81=param(16,23),[39], % 0.69/1.14 add(n1,inverse(X10)) = n1]. % 0.69/1.14 [83=param(2,81),[48], % 0.69/1.14 multiply(n1,add(X10,inverse(X11))) = add(inverse(X11),multiply(X10,n1))]. % 0.69/1.14 [84=param(75,2),[], % 0.69/1.14 multiply(add(X10,inverse(multiply(X10,X11))),add(X11,inverse(multiply(X10,X11)))) = n1]. % 0.69/1.14 [94=param(20,75),[], % 0.69/1.14 add(n1,add(X10,inverse(multiply(X11,X10)))) = add(X10,inverse(multiply(X11,X10)))]. % 0.69/1.14 [98=param(2,78),[], % 0.69/1.14 multiply(n1,add(X10,multiply(n0,X11))) = add(multiply(n0,X11),multiply(n1,X10))]. % 0.69/1.14 [99=param(2,78),[48], % 0.69/1.14 multiply(n1,add(X10,multiply(n0,X11))) = add(multiply(n0,X11),multiply(X10,n1))]. % 0.69/1.14 [108=param(44,4),[], % 0.69/1.14 multiply(X10,n1) = X10]. % 0.69/1.14 [109=demod(99),[108], % 0.69/1.14 multiply(n1,add(X10,multiply(n0,X11))) = add(multiply(n0,X11),X10)]. % 0.69/1.14 [111=demod(83),[108], % 0.69/1.14 multiply(n1,add(X10,inverse(X11))) = add(inverse(X11),X10)]. % 0.69/1.14 [114=param(5,44),[], % 0.69/1.14 add(X10,multiply(X11,add(X10,X12))) = multiply(add(X10,X12),add(X10,X11))]. % 0.69/1.14 [120=param(45,44),[], % 0.69/1.14 add(add(X10,X11),X10) = add(X10,X11)]. % 0.69/1.14 [121=param(25,2),[], % 0.69/1.14 add(multiply(X10,X11),X12) = multiply(add(X10,X12),add(X11,X12))]. % 0.69/1.14 [122=demod(109),[121], % 0.69/1.14 multiply(n1,add(X10,multiply(n0,X11))) = multiply(add(n0,X10),add(X11,X10))]. % 0.69/1.14 [124=demod(5),[121,45,48], % 0.69/1.14 multiply(X10,add(X11,multiply(X12,X10))) = multiply(X10,add(X11,X12))]. % 0.69/1.14 [128=demod(98),[121,70,39], % 0.69/1.14 multiply(n1,add(X10,multiply(n0,X11))) = multiply(n1,X10)]. % 0.69/1.14 [129=demod(122),[128], % 0.69/1.14 multiply(add(n0,X10),add(X11,X10)) = multiply(n1,X10)]. % 0.69/1.14 [130=demod(66),[129], % 0.69/1.14 multiply(n1,X10) = X10]. % 0.69/1.14 [133=demod(62),[130], % 0.69/1.14 add(X10,inverse(inverse(X10))) = inverse(inverse(X10))]. % 0.69/1.14 [136=demod(120),[], % 0.69/1.14 add(add(X10,X11),X10) = add(X10,X11)]. % 0.69/1.14 [138=demod(136),[], % 0.69/1.14 add(add(X10,X11),X10) = add(X10,X11)]. % 0.69/1.14 [143=demod(64),[130,130], % 0.69/1.14 add(n0,X10) = X10]. % 0.69/1.14 [146=demod(45),[], % 0.69/1.14 add(X10,multiply(X11,X10)) = X10]. % 0.69/1.14 [151=param(44,143),[], % 0.69/1.14 multiply(n0,X10) = n0]. % 0.69/1.14 [155=demod(138),[], % 0.69/1.14 add(add(X10,X11),X10) = add(X10,X11)]. % 0.69/1.14 [157=param(130,44),[], % 0.69/1.14 add(n1,X10) = n1]. % 0.69/1.14 [158=demod(94),[157], % 0.69/1.14 add(X10,inverse(multiply(X11,X10))) = n1]. % 0.69/1.14 [159=demod(84),[158,48,130], % 0.69/1.14 add(X10,inverse(multiply(X10,X11))) = n1]. % 0.69/1.14 [163=param(34,23),[], % 0.69/1.14 multiply(multiply(X10,X11),multiply(X11,X10)) = multiply(X11,X10)]. % 0.69/1.14 [170=param(34,146),[], % 0.69/1.14 multiply(multiply(X10,X11),multiply(multiply(X12,X11),X10)) = multiply(multiply(X12,X11),X10)]. % 0.69/1.14 [181=param(2,159),[48,130], % 0.69/1.14 add(X10,inverse(multiply(X11,X12))) = add(inverse(multiply(X11,X12)),multiply(X10,X11))]. % 0.69/1.14 [189=param(158,39),[16,157,130], % 0.69/1.14 add(inverse(X10),add(X11,X10)) = n1]. % 0.69/1.14 [190=param(158,44),[16,157,130], % 0.69/1.14 add(inverse(X10),add(X10,X11)) = n1]. % 0.69/1.14 [192=param(2,190),[48,130], % 0.69/1.14 add(X10,add(X11,X12)) = add(add(X11,X12),multiply(X10,inverse(X11)))]. % 0.69/1.14 [197=param(155,25),[], % 0.69/1.14 add(X10,add(X10,X11)) = add(X10,X11)]. % 0.69/1.14 [213=param(68,146),[124], % 0.69/1.14 multiply(X10,add(inverse(X10),X11)) = multiply(X11,X10)]. % 0.69/1.14 [226=param(44,133),[], % 0.69/1.14 multiply(X10,inverse(inverse(X10))) = X10]. % 0.69/1.14 [230=param(69,4),[48,130,226], % 0.69/1.14 inverse(inverse(X10)) = X10]. % 0.69/1.14 [234=param(69,189),[48,130], % 0.69/1.14 multiply(inverse(X11),inverse(add(X10,X11))) = inverse(add(X10,X11))]. % 0.69/1.14 [236=param(69,197),[48,1], % 0.69/1.14 multiply(X10,inverse(add(X10,X11))) = n0]. % 0.69/1.14 [307=param(114,213),[-111,4,130,48,130], % 0.69/1.14 add(inverse(X10),multiply(X11,X10)) = add(inverse(X10),X11)]. % 0.69/1.14 [316=param(307,68),[-111,130,192,48,236,63], % 0.69/1.14 add(X10,inverse(add(inverse(X11),X10))) = add(X11,X10)]. % 0.69/1.14 [321=param(71,316),[69,48,234], % 0.69/1.14 inverse(add(inverse(X10),X11)) = multiply(X10,inverse(X11))]. % 0.69/1.14 [337=param(321,159),[15,230], % 0.69/1.14 multiply(X10,multiply(inverse(X10),X11)) = n0]. % 0.69/1.14 [340=param(321,230),[], % 0.69/1.14 inverse(add(X10,X11)) = multiply(inverse(X10),inverse(X11))]. % 0.69/1.14 [353=param(230,340),[], % 0.69/1.14 add(X10,X11) = inverse(multiply(inverse(X10),inverse(X11)))]. % 0.69/1.14 [377=demod(25),[353,353], % 0.69/1.14 inverse(multiply(inverse(X10),inverse(X11))) = inverse(multiply(inverse(X11),inverse(X10)))]. % 0.69/1.14 [411=demod(181),[353,230,353,230], % 0.69/1.14 inverse(multiply(inverse(X10),multiply(X11,X12))) = inverse(multiply(multiply(X11,X12),inverse(multiply(X10,X11))))]. % 0.69/1.14 [421=demod(307),[353,230,353,230], % 0.69/1.14 inverse(multiply(X10,inverse(multiply(X11,X10)))) = inverse(multiply(X10,inverse(X11)))]. % 0.69/1.14 [454=param(170,48),[], % 0.69/1.14 multiply(multiply(multiply(X10,X11),X12),multiply(X12,X11)) = multiply(multiply(X10,X11),X12)]. % 0.69/1.14 [456=param(170,337),[48,151,48], % 0.69/1.14 multiply(X10,multiply(X11,multiply(inverse(X10),X12))) = n0]. % 0.69/1.14 [460=param(456,230),[], % 0.69/1.14 multiply(inverse(X10),multiply(X11,multiply(X10,X12))) = n0]. % 0.69/1.14 [462=param(460,48),[], % 0.69/1.14 multiply(inverse(X10),multiply(multiply(X10,X11),X12)) = n0]. % 0.69/1.14 [500=param(462,163),[], % 0.69/1.14 multiply(inverse(multiply(X10,X11)),multiply(multiply(X11,X10),X12)) = n0]. % 0.69/1.14 [531=param(230,421),[230], % 0.69/1.14 multiply(X10,inverse(multiply(X11,X10))) = multiply(X10,inverse(X11))]. % 0.69/1.14 [532=param(531,48),[], % 0.69/1.14 multiply(X10,inverse(multiply(X10,X11))) = multiply(X10,inverse(X11))]. % 0.69/1.14 [659=param(377,230),[230], % 0.69/1.14 inverse(multiply(X10,inverse(X11))) = inverse(multiply(inverse(X11),X10))]. % 0.69/1.14 [660=param(659,230),[230], % 0.69/1.14 inverse(multiply(X10,X11)) = inverse(multiply(X11,X10))]. % 0.69/1.14 [710=param(500,170),[], % 0.69/1.14 multiply(inverse(multiply(X10,X11)),multiply(multiply(X12,X10),X11)) = n0]. % 0.69/1.14 [715=param(710,660),[], % 0.69/1.14 multiply(inverse(multiply(X10,X11)),multiply(multiply(X12,X11),X10)) = n0]. % 0.69/1.14 [720=param(715,48),[], % 0.69/1.14 multiply(inverse(multiply(X10,X11)),multiply(multiply(X11,X12),X10)) = n0]. % 0.69/1.14 [741=param(720,48),[], % 0.69/1.14 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(X11,X12))) = n0]. % 0.69/1.14 [768=param(531,741),[74,48,130,230,48], % 0.69/1.14 multiply(multiply(X10,X11),multiply(X10,multiply(X11,X12))) = multiply(X10,multiply(X11,X12))]. % 0.69/1.14 [859=param(531,411),[532,230,230], % 0.69/1.14 multiply(multiply(X10,X11),multiply(X12,X10)) = multiply(multiply(X10,X11),X12)]. % 0.69/1.14 [870=param(859,48),[], % 0.69/1.14 multiply(multiply(X10,X11),multiply(X10,X12)) = multiply(multiply(X10,X11),X12)]. % 0.69/1.14 [871=demod(768),[870], % 0.69/1.14 multiply(multiply(X10,X11),multiply(X11,X12)) = multiply(X10,multiply(X11,X12))]. % 0.69/1.14 [872=demod(454),[871], % 0.69/1.14 multiply(multiply(X10,X11),multiply(X12,X11)) = multiply(multiply(X10,X11),X12)]. % 0.69/1.14 [881=param(872,48),[871], % 0.69/1.14 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 0.69/1.14 [969=param(8,881),[48,48,7], % 0.69/1.14 thmtrue = thmfalse]. % 0.69/1.14 % SZS output end CNFRefutation % 0.69/1.14 Space: 1424 KB %------------------------------------------------------------------------------