%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : BOO002-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n028.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:44 EDT 2022 % Result : Unsatisfiable 1.33s 1.72s % Output : CNFRefutation 1.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : BOO002-1 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.12 % Command : fiesta-wrapper %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Jun 1 19:41:22 EDT 2022 % 0.13/0.33 % CPUTime : % 1.33/1.72 Theorem Proved. % 1.33/1.72 % SZS status Unsatisfiable % 1.33/1.72 % SZS output start CNFRefutation % 1.33/1.72 [1=axiom,[], % 1.33/1.72 multiply(inverse(X10),X10,X11) = X11]. % 1.33/1.72 [2=axiom,[], % 1.33/1.72 multiply(X10,X10,X11) = X10]. % 1.33/1.72 [3=axiom,[], % 1.33/1.72 multiply(X10,X11,X11) = X11]. % 1.33/1.72 [4=axiom,[], % 1.33/1.72 multiply(multiply(X10,X11,X12),X13,multiply(X10,X11,X14)) = multiply(X10,X11,multiply(X12,X13,X14))]. % 1.33/1.72 [5=axiom,[], % 1.33/1.72 thtop(X10,X10) = thmfalse]. % 1.33/1.72 [6=axiom,[], % 1.33/1.72 thtop(multiply(a,inverse(a),b),b) = thmtrue]. % 1.33/1.72 [7=param(4,2),[], % 1.33/1.72 multiply(X10,X11,multiply(X12,multiply(X10,X11,X12),X13)) = multiply(X10,X11,X12)]. % 1.33/1.72 [8=param(4,2),[2,2], % 1.33/1.72 multiply(X10,X11,X10) = X10]. % 1.33/1.72 [10=param(4,3),[], % 1.33/1.72 multiply(X10,X11,multiply(X12,X10,X13)) = multiply(X12,X10,multiply(X10,X11,X13))]. % 1.33/1.72 [11=param(4,3),[], % 1.33/1.72 multiply(multiply(X10,X11,X12),X13,X11) = multiply(X10,X11,multiply(X12,X13,X11))]. % 1.33/1.72 [12=param(4,8),[], % 1.33/1.72 multiply(X10,X11,multiply(X10,X12,X13)) = multiply(X10,X12,multiply(X10,X11,X13))]. % 1.33/1.72 [13=param(4,8),[], % 1.33/1.72 multiply(multiply(X10,X11,X12),X13,X10) = multiply(X10,X11,multiply(X12,X13,X10))]. % 1.33/1.72 [14=param(13,3),[], % 1.33/1.72 multiply(X12,X10,multiply(X10,X11,X12)) = multiply(X10,X11,X12)]. % 1.33/1.72 [15=param(7,3),[], % 1.33/1.72 multiply(X10,X11,multiply(X10,X11,X12)) = multiply(X10,X11,X12)]. % 1.33/1.72 [17=param(11,8),[], % 1.33/1.72 multiply(X10,X12,multiply(X10,X11,X12)) = multiply(X10,X11,X12)]. % 1.33/1.72 [18=param(7,17),[], % 1.33/1.72 multiply(X10,X11,multiply(X12,X13,multiply(X10,X11,X12))) = multiply(X10,X11,X12)]. % 1.33/1.72 [19=param(10,3),[], % 1.33/1.72 multiply(X11,X12,multiply(X10,X11,X12)) = multiply(X10,X11,X12)]. % 1.33/1.72 [20=param(7,19),[], % 1.33/1.72 multiply(X10,X11,multiply(X12,X13,multiply(X10,X11,X13))) = multiply(X10,X11,X13)]. % 1.33/1.72 [21=param(20,7),[3], % 1.33/1.72 multiply(X12,multiply(X10,X11,X12),X11) = multiply(X10,X11,X12)]. % 1.33/1.72 [22=param(17,21),[21], % 1.33/1.72 multiply(X10,X11,multiply(X12,X11,X10)) = multiply(X12,X11,X10)]. % 1.33/1.72 [23=param(18,7),[3], % 1.33/1.72 multiply(X12,multiply(X10,X11,X12),X10) = multiply(X10,X11,X12)]. % 1.33/1.72 [29=param(4,15),[4], % 1.33/1.72 multiply(X10,X11,multiply(X12,X13,multiply(X10,X11,X14))) = multiply(X10,X11,multiply(X12,X13,X14))]. % 1.33/1.72 [45=param(13,14),[], % 1.33/1.72 multiply(X12,X10,multiply(multiply(X10,X11,X12),X13,X12)) = multiply(multiply(X10,X11,X12),X13,X12)]. % 1.33/1.72 [47=param(13,21),[], % 1.33/1.72 multiply(multiply(X10,X11,X12),X13,X12) = multiply(X12,multiply(X10,X11,X12),multiply(X11,X13,X12))]. % 1.33/1.72 [48=demod(45),[47,47], % 1.33/1.72 multiply(X10,X11,multiply(X10,multiply(X11,X12,X10),multiply(X12,X13,X10))) = multiply(X10,multiply(X11,X12,X10),multiply(X12,X13,X10))]. % 1.33/1.72 [52=param(11,22),[11,11], % 1.33/1.72 multiply(X12,X11,multiply(X10,X11,multiply(X12,X13,X11))) = multiply(X10,X11,multiply(X12,X13,X11))]. % 1.33/1.72 [56=param(12,19),[], % 1.33/1.72 multiply(X10,X13,multiply(X10,X11,multiply(X12,X10,X13))) = multiply(X10,X11,multiply(X12,X10,X13))]. % 1.33/1.72 [57=param(12,21),[], % 1.33/1.72 multiply(X10,X11,multiply(X12,X13,X10)) = multiply(X10,multiply(X12,X13,X10),multiply(X10,X11,X13))]. % 1.33/1.72 [59=param(12,23),[], % 1.33/1.72 multiply(X10,X11,multiply(X12,X13,X10)) = multiply(X10,multiply(X12,X13,X10),multiply(X10,X11,X12))]. % 1.33/1.72 [60=param(47,2),[22], % 1.33/1.72 multiply(X10,multiply(X11,X10,X12),X12) = multiply(X11,X10,X12)]. % 1.33/1.72 [61=param(60,7),[7], % 1.33/1.72 multiply(X10,multiply(X11,X10,X12),multiply(X12,multiply(X11,X10,X12),X13)) = multiply(X11,X10,X12)]. % 1.33/1.72 [69=param(60,13),[13], % 1.33/1.72 multiply(X10,multiply(X11,X12,multiply(X13,X10,X11)),X11) = multiply(X11,X12,multiply(X13,X10,X11))]. % 1.33/1.72 [76=param(29,7),[3], % 1.33/1.72 multiply(X12,multiply(X10,X11,X12),multiply(X10,X11,X13)) = multiply(X10,X11,X12)]. % 1.33/1.72 [81=param(76,17),[], % 1.33/1.72 multiply(X10,multiply(X11,X12,X10),multiply(X11,X13,X12)) = multiply(X11,X12,X10)]. % 1.33/1.72 [82=param(17,76),[76], % 1.33/1.72 multiply(X10,multiply(X11,X12,X13),multiply(X11,X12,X10)) = multiply(X11,X12,X10)]. % 1.33/1.72 [85=param(76,23),[23], % 1.33/1.72 multiply(X10,multiply(X10,X11,X12),multiply(X12,multiply(X10,X11,X12),X13)) = multiply(X10,X11,X12)]. % 1.33/1.72 [135=param(76,56),[], % 1.33/1.72 multiply(X10,multiply(X11,X12,X10),multiply(X11,X13,multiply(X14,X11,X12))) = multiply(X11,X12,X10)]. % 1.33/1.72 [142=param(76,52),[], % 1.33/1.72 multiply(X10,multiply(X11,X12,X10),multiply(X13,X12,multiply(X11,X14,X12))) = multiply(X11,X12,X10)]. % 1.33/1.72 [153=param(57,15),[21], % 1.33/1.72 multiply(X11,X12,multiply(X10,multiply(X11,X12,X13),X11)) = multiply(X10,multiply(X11,X12,X13),X11)]. % 1.33/1.72 [181=param(85,8),[], % 1.33/1.72 multiply(X10,multiply(X10,X11,X12),X12) = multiply(X10,X11,X12)]. % 1.33/1.72 [186=param(181,13),[13,13,153], % 1.33/1.72 multiply(X12,multiply(X10,X11,multiply(X12,X13,X10)),X10) = multiply(X10,X11,multiply(X12,X13,X10))]. % 1.33/1.72 [194=param(186,21),[21], % 1.33/1.72 multiply(X10,multiply(X11,X12,multiply(X13,X11,X10)),X11) = multiply(X11,X12,multiply(X13,X11,X10))]. % 1.33/1.72 [195=param(186,23),[23], % 1.33/1.72 multiply(X10,multiply(X11,X12,multiply(X11,X13,X10)),X11) = multiply(X11,X12,multiply(X11,X13,X10))]. % 1.33/1.72 [202=param(195,142),[12,81,22], % 1.33/1.72 multiply(multiply(X10,X11,X12),multiply(X10,X12,X13),X13) = multiply(X10,X12,X13)]. % 1.33/1.72 [206=param(202,21),[21], % 1.33/1.72 multiply(multiply(X10,X11,multiply(X12,X13,X10)),multiply(X12,X13,X10),X13) = multiply(X12,X13,X10)]. % 1.33/1.72 [222=param(194,135),[135], % 1.33/1.72 multiply(multiply(X10,X11,X12),multiply(X11,X12,X13),X13) = multiply(X11,X12,X13)]. % 1.33/1.72 [223=param(222,21),[21], % 1.33/1.72 multiply(multiply(X10,X11,multiply(X12,X13,X11)),multiply(X12,X13,X11),X13) = multiply(X12,X13,X11)]. % 1.33/1.72 [287=param(11,11),[], % 1.33/1.72 multiply(multiply(X10,X11,multiply(X12,X13,X11)),X14,X13) = multiply(multiply(X10,X11,X12),X13,multiply(X11,X14,X13))]. % 1.33/1.72 [288=demod(223),[287,21], % 1.33/1.72 multiply(multiply(X10,X11,X12),X13,multiply(X12,X13,X11)) = multiply(X12,X13,X11)]. % 1.33/1.72 [289=param(11,13),[], % 1.33/1.72 multiply(multiply(X10,X11,multiply(X12,X13,X10)),X14,X13) = multiply(multiply(X10,X11,X12),X13,multiply(X10,X14,X13))]. % 1.33/1.72 [290=demod(206),[289,21], % 1.33/1.72 multiply(multiply(X10,X11,X12),X13,multiply(X12,X13,X10)) = multiply(X12,X13,X10)]. % 1.33/1.72 [295=param(290,23),[], % 1.33/1.72 multiply(multiply(X10,X11,X12),X13,multiply(X10,X13,X12)) = multiply(X10,X13,X12)]. % 1.33/1.72 [296=param(295,1),[47,1], % 1.33/1.72 multiply(X10,multiply(inverse(X11),X12,X10),multiply(X12,X11,X10)) = X10]. % 1.33/1.72 [581=param(57,296),[], % 1.33/1.72 multiply(X10,multiply(X11,X12,X10),multiply(X10,multiply(inverse(X12),X11,X10),X12)) = X10]. % 1.33/1.72 [587=param(57,82),[21], % 1.33/1.72 multiply(X13,multiply(X11,X12,X14),multiply(X10,multiply(X11,X12,X13),X13)) = multiply(X10,multiply(X11,X12,X13),X13)]. % 1.33/1.72 [611=param(61,288),[], % 1.33/1.72 multiply(X13,multiply(X10,multiply(X11,X12,X13),X13),X12) = multiply(X10,multiply(X11,X12,X13),X13)]. % 1.33/1.72 [937=param(581,611),[47,2,21,587], % 1.33/1.72 multiply(inverse(X10),multiply(X11,X10,X12),X12) = X12]. % 1.33/1.72 [960=param(937,13),[], % 1.33/1.72 multiply(inverse(X10),multiply(X11,X12,multiply(X13,X10,X11)),X11) = X11]. % 1.33/1.72 [982=param(960,59),[], % 1.33/1.72 multiply(inverse(X10),multiply(X11,multiply(X12,X10,X11),multiply(X11,X13,X12)),X11) = X11]. % 1.33/1.72 [1036=param(982,23),[], % 1.33/1.72 multiply(inverse(X10),multiply(X11,multiply(X12,X10,X11),multiply(X12,X13,X11)),X11) = X11]. % 1.33/1.72 [1056=param(1036,69),[], % 1.33/1.72 multiply(X10,multiply(X11,X12,X10),multiply(X11,inverse(X12),X10)) = X10]. % 1.33/1.72 [1066=param(48,1056),[8,2,14], % 1.33/1.72 multiply(X11,inverse(X11),X10) = X10]. % 1.33/1.72 [1073=param(6,1066),[5], % 1.33/1.72 thmtrue = thmfalse]. % 1.33/1.72 % SZS output end CNFRefutation % 1.33/1.72 Space: 4581 KB %------------------------------------------------------------------------------