%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP167-4 : TPTP v8.1.0. Bugfixed v1.2.1. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n020.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:13:01 EDT 2022 % Result : Unsatisfiable 3.28s 3.66s % Output : CNFRefutation 3.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.12 % Problem : GRP167-4 : TPTP v8.1.0. Bugfixed v1.2.1. % 0.13/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 19:32:35 EDT 2022 % 0.13/0.34 % CPUTime : % 3.28/3.66 Theorem Proved. % 3.28/3.66 % SZS status Unsatisfiable % 3.28/3.66 % SZS output start CNFRefutation % 3.28/3.66 [1=axiom,[], % 3.28/3.66 inverse(multiply(X10,X11)) = multiply(inverse(X11),inverse(X10))]. % 3.28/3.66 [2=axiom,[], % 3.28/3.66 inverse(inverse(X10)) = X10]. % 3.28/3.66 [3=axiom,[], % 3.28/3.66 inverse(identity) = identity]. % 3.28/3.66 [4=axiom,[], % 3.28/3.66 multiply(greatest_lower_bound(X10,X11),X12) = greatest_lower_bound(multiply(X10,X12),multiply(X11,X12))]. % 3.28/3.66 [5=axiom,[], % 3.28/3.66 multiply(least_upper_bound(X10,X11),X12) = least_upper_bound(multiply(X10,X12),multiply(X11,X12))]. % 3.28/3.66 [6=axiom,[], % 3.28/3.66 multiply(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(multiply(X10,X11),multiply(X10,X12))]. % 3.28/3.66 [7=axiom,[], % 3.28/3.66 multiply(X10,least_upper_bound(X11,X12)) = least_upper_bound(multiply(X10,X11),multiply(X10,X12))]. % 3.28/3.66 [8=axiom,[], % 3.28/3.66 greatest_lower_bound(X10,least_upper_bound(X10,X11)) = X10]. % 3.28/3.66 [9=axiom,[], % 3.28/3.66 least_upper_bound(X10,greatest_lower_bound(X10,X11)) = X10]. % 3.28/3.66 [12=axiom,[], % 3.28/3.66 least_upper_bound(least_upper_bound(X10,X11),X12) = least_upper_bound(X10,least_upper_bound(X11,X12))]. % 3.28/3.66 [13=axiom,[], % 3.28/3.66 greatest_lower_bound(greatest_lower_bound(X10,X11),X12) = greatest_lower_bound(X10,greatest_lower_bound(X11,X12))]. % 3.28/3.66 [14=axiom,[], % 3.28/3.66 least_upper_bound(X10,X11) = least_upper_bound(X11,X10)]. % 3.28/3.66 [15=axiom,[], % 3.28/3.66 greatest_lower_bound(X10,X11) = greatest_lower_bound(X11,X10)]. % 3.28/3.66 [16=axiom,[], % 3.28/3.66 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 3.28/3.66 [17=axiom,[], % 3.28/3.66 multiply(inverse(X10),X10) = identity]. % 3.28/3.66 [18=axiom,[], % 3.28/3.66 multiply(identity,X10) = X10]. % 3.28/3.66 [19=axiom,[], % 3.28/3.66 thtop(X10,X10) = thmfalse]. % 3.28/3.66 [20=axiom,[5,6,6,18,18,14], % 3.28/3.66 thtop(a,least_upper_bound(greatest_lower_bound(a,identity),greatest_lower_bound(multiply(a,a),multiply(a,identity)))) = thmtrue]. % 3.28/3.66 [23=param(1,3),[18], % 3.28/3.66 inverse(multiply(X10,identity)) = inverse(X10)]. % 3.28/3.66 [25=param(1,2),[], % 3.28/3.66 multiply(X10,inverse(X11)) = inverse(multiply(X11,inverse(X10)))]. % 3.28/3.66 [26=param(1,2),[], % 3.28/3.66 multiply(inverse(X10),X11) = inverse(multiply(inverse(X11),X10))]. % 3.28/3.66 [28=param(17,1),[-25], % 3.28/3.66 multiply(X10,inverse(X10)) = identity]. % 3.28/3.66 [30=param(28,4),[], % 3.28/3.66 greatest_lower_bound(multiply(X10,inverse(greatest_lower_bound(X10,X11))),multiply(X11,inverse(greatest_lower_bound(X10,X11)))) = identity]. % 3.28/3.66 [33=param(2,23),[2], % 3.28/3.66 multiply(X10,identity) = X10]. % 3.28/3.66 [35=param(9,15),[], % 3.28/3.66 least_upper_bound(X10,greatest_lower_bound(X11,X10)) = X10]. % 3.28/3.66 [37=param(8,14),[], % 3.28/3.66 greatest_lower_bound(X10,least_upper_bound(X11,X10)) = X10]. % 3.28/3.66 [39=param(37,35),[15], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(X11,X10)) = greatest_lower_bound(X11,X10)]. % 3.28/3.66 [41=param(8,12),[], % 3.28/3.66 greatest_lower_bound(least_upper_bound(X10,X11),least_upper_bound(X10,least_upper_bound(X11,X12))) = least_upper_bound(X10,X11)]. % 3.28/3.66 [43=param(12,9),[], % 3.28/3.66 least_upper_bound(X10,least_upper_bound(greatest_lower_bound(X10,X12),X11)) = least_upper_bound(X10,X11)]. % 3.28/3.66 [48=param(37,12),[], % 3.28/3.66 greatest_lower_bound(X10,least_upper_bound(X11,least_upper_bound(X12,X10))) = X10]. % 3.28/3.66 [53=param(9,13),[], % 3.28/3.66 least_upper_bound(greatest_lower_bound(X10,X11),greatest_lower_bound(X10,greatest_lower_bound(X11,X12))) = greatest_lower_bound(X10,X11)]. % 3.28/3.66 [54=param(13,15),[], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(X12,greatest_lower_bound(X10,X11))]. % 3.28/3.66 [55=param(13,15),[13], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(X11,greatest_lower_bound(X10,X12))]. % 3.28/3.66 [56=param(35,13),[], % 3.28/3.66 least_upper_bound(X10,greatest_lower_bound(X11,greatest_lower_bound(X12,X10))) = X10]. % 3.28/3.66 [58=param(13,37),[], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(least_upper_bound(X12,X10),X11)) = greatest_lower_bound(X10,X11)]. % 3.28/3.66 [60=param(13,39),[13,13], % 3.28/3.66 greatest_lower_bound(X11,greatest_lower_bound(X10,greatest_lower_bound(X11,X12))) = greatest_lower_bound(X10,greatest_lower_bound(X11,X12))]. % 3.28/3.66 [61=param(1,16),[], % 3.28/3.66 inverse(multiply(X10,multiply(X11,X12))) = multiply(inverse(X12),inverse(multiply(X10,X11)))]. % 3.28/3.66 [63=param(16,17),[18], % 3.28/3.66 multiply(inverse(X11),multiply(X11,X10)) = X10]. % 3.28/3.66 [65=param(16,28),[18], % 3.28/3.66 multiply(X11,multiply(inverse(X11),X10)) = X10]. % 3.28/3.66 [66=param(65,1),[], % 3.28/3.66 multiply(X10,inverse(multiply(X11,X10))) = inverse(X11)]. % 3.28/3.66 [72=param(66,4),[], % 3.28/3.66 multiply(X10,inverse(greatest_lower_bound(multiply(X11,X10),multiply(X12,X10)))) = inverse(greatest_lower_bound(X11,X12))]. % 3.28/3.66 [73=param(66,5),[], % 3.28/3.66 multiply(X10,inverse(least_upper_bound(multiply(X11,X10),multiply(X12,X10)))) = inverse(least_upper_bound(X11,X12))]. % 3.28/3.66 [80=param(56,15),[13], % 3.28/3.66 least_upper_bound(X10,greatest_lower_bound(X11,greatest_lower_bound(X10,X12))) = X10]. % 3.28/3.66 [81=param(37,56),[15], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(X11,greatest_lower_bound(X12,X10))) = greatest_lower_bound(X11,greatest_lower_bound(X12,X10))]. % 3.28/3.66 [89=param(48,9),[13], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(X11,least_upper_bound(X12,X10))) = greatest_lower_bound(X10,X11)]. % 3.28/3.66 [93=param(48,14),[12], % 3.28/3.66 greatest_lower_bound(X10,least_upper_bound(X11,least_upper_bound(X10,X12))) = X10]. % 3.28/3.66 [180=param(53,39),[], % 3.28/3.66 least_upper_bound(greatest_lower_bound(X10,X11),greatest_lower_bound(X11,X10)) = greatest_lower_bound(X10,X11)]. % 3.28/3.66 [188=param(89,180),[13,60,81,13], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(X12,greatest_lower_bound(X11,X10))]. % 3.28/3.66 [341=param(72,17),[], % 3.28/3.66 multiply(X10,inverse(greatest_lower_bound(identity,multiply(X11,X10)))) = inverse(greatest_lower_bound(inverse(X10),X11))]. % 3.28/3.66 [342=param(72,18),[], % 3.28/3.66 multiply(X10,inverse(greatest_lower_bound(X10,multiply(X11,X10)))) = inverse(greatest_lower_bound(identity,X11))]. % 3.28/3.66 [352=param(73,18),[], % 3.28/3.66 multiply(X10,inverse(least_upper_bound(X10,multiply(X11,X10)))) = inverse(least_upper_bound(identity,X11))]. % 3.28/3.66 [353=param(352,17),[], % 3.28/3.66 multiply(X10,inverse(least_upper_bound(X10,identity))) = inverse(least_upper_bound(identity,inverse(X10)))]. % 3.28/3.66 [356=param(61,352),[2,5,66,16,66], % 3.28/3.66 inverse(multiply(X10,inverse(least_upper_bound(identity,X11)))) = least_upper_bound(inverse(X10),multiply(X11,inverse(X10)))]. % 3.28/3.66 [363=param(66,353),[2,7,26,3,7,18,33,-1,7,33,14], % 3.28/3.66 least_upper_bound(inverse(least_upper_bound(X10,identity)),inverse(least_upper_bound(X10,multiply(X10,X10)))) = inverse(X10)]. % 3.28/3.66 [364=param(342,17),[], % 3.28/3.66 multiply(X10,inverse(greatest_lower_bound(X10,identity))) = inverse(greatest_lower_bound(identity,inverse(X10)))]. % 3.28/3.66 [373=param(30,364),[18], % 3.28/3.66 greatest_lower_bound(inverse(greatest_lower_bound(identity,inverse(X10))),inverse(greatest_lower_bound(X10,identity))) = identity]. % 3.28/3.66 [382=param(35,373),[14], % 3.28/3.66 least_upper_bound(identity,inverse(greatest_lower_bound(X10,identity))) = inverse(greatest_lower_bound(X10,identity))]. % 3.28/3.66 [390=param(8,382),[], % 3.28/3.66 greatest_lower_bound(identity,inverse(greatest_lower_bound(X10,identity))) = identity]. % 3.28/3.66 [391=param(41,382),[], % 3.28/3.66 greatest_lower_bound(least_upper_bound(X10,identity),least_upper_bound(X10,inverse(greatest_lower_bound(X11,identity)))) = least_upper_bound(X10,identity)]. % 3.28/3.66 [399=param(6,390),[33,33], % 3.28/3.66 greatest_lower_bound(X10,multiply(X10,inverse(greatest_lower_bound(X11,identity)))) = X10]. % 3.28/3.66 [407=param(399,364),[], % 3.28/3.66 greatest_lower_bound(X10,inverse(greatest_lower_bound(identity,inverse(X10)))) = X10]. % 3.28/3.66 [410=param(407,2),[], % 3.28/3.66 greatest_lower_bound(inverse(X10),inverse(greatest_lower_bound(identity,X10))) = inverse(X10)]. % 3.28/3.66 [427=param(410,37),[3,15], % 3.28/3.66 greatest_lower_bound(identity,inverse(least_upper_bound(X10,identity))) = inverse(least_upper_bound(X10,identity))]. % 3.28/3.66 [435=param(9,427),[], % 3.28/3.66 least_upper_bound(identity,inverse(least_upper_bound(X10,identity))) = identity]. % 3.28/3.66 [443=param(7,435),[33,33], % 3.28/3.66 least_upper_bound(X10,multiply(X10,inverse(least_upper_bound(X11,identity)))) = X10]. % 3.28/3.66 [499=param(443,353),[], % 3.28/3.66 least_upper_bound(X10,inverse(least_upper_bound(identity,inverse(X10)))) = X10]. % 3.28/3.66 [502=param(499,2),[], % 3.28/3.66 least_upper_bound(inverse(X10),inverse(least_upper_bound(identity,X10))) = inverse(X10)]. % 3.28/3.66 [518=param(502,9),[3,14], % 3.28/3.66 least_upper_bound(identity,inverse(greatest_lower_bound(identity,X10))) = inverse(greatest_lower_bound(identity,X10))]. % 3.28/3.66 [534=param(8,518),[], % 3.28/3.66 greatest_lower_bound(identity,inverse(greatest_lower_bound(identity,X10))) = identity]. % 3.28/3.66 [543=param(4,534),[18,18], % 3.28/3.66 greatest_lower_bound(X10,multiply(inverse(greatest_lower_bound(identity,X11)),X10)) = X10]. % 3.28/3.66 [567=param(543,1),[6,33], % 3.28/3.66 greatest_lower_bound(inverse(X10),inverse(greatest_lower_bound(X10,multiply(X10,X11)))) = inverse(X10)]. % 3.28/3.66 [822=param(567,63),[2,2], % 3.28/3.66 greatest_lower_bound(X10,inverse(greatest_lower_bound(inverse(X10),X11))) = X10]. % 3.28/3.66 [823=param(567,65),[], % 3.28/3.66 greatest_lower_bound(inverse(X10),inverse(greatest_lower_bound(X10,X11))) = inverse(X10)]. % 3.28/3.66 [829=param(822,15),[], % 3.28/3.66 greatest_lower_bound(X10,inverse(greatest_lower_bound(X11,inverse(X10)))) = X10]. % 3.28/3.66 [830=param(35,822),[14], % 3.28/3.66 least_upper_bound(X10,inverse(greatest_lower_bound(inverse(X10),X11))) = inverse(greatest_lower_bound(inverse(X10),X11))]. % 3.28/3.66 [844=param(829,2),[], % 3.28/3.66 greatest_lower_bound(inverse(X10),inverse(greatest_lower_bound(X11,X10))) = inverse(X10)]. % 3.28/3.66 [848=param(13,829),[], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(inverse(greatest_lower_bound(X12,inverse(X10))),X11)) = greatest_lower_bound(X10,X11)]. % 3.28/3.66 [861=param(844,8),[15], % 3.28/3.66 greatest_lower_bound(inverse(X10),inverse(least_upper_bound(X10,X11))) = inverse(least_upper_bound(X10,X11))]. % 3.28/3.66 [865=param(844,37),[15], % 3.28/3.66 greatest_lower_bound(inverse(X10),inverse(least_upper_bound(X11,X10))) = inverse(least_upper_bound(X11,X10))]. % 3.28/3.66 [886=param(9,865),[], % 3.28/3.66 least_upper_bound(inverse(X10),inverse(least_upper_bound(X11,X10))) = inverse(X10)]. % 3.28/3.66 [1307=param(848,373),[], % 3.28/3.66 greatest_lower_bound(X10,inverse(greatest_lower_bound(X10,identity))) = greatest_lower_bound(X10,identity)]. % 3.28/3.66 [1317=param(13,1307),[13], % 3.28/3.66 greatest_lower_bound(X10,greatest_lower_bound(inverse(greatest_lower_bound(X10,identity)),X11)) = greatest_lower_bound(X10,greatest_lower_bound(identity,X11))]. % 3.28/3.66 [1319=param(55,1307),[], % 3.28/3.66 greatest_lower_bound(X11,greatest_lower_bound(X10,inverse(greatest_lower_bound(X11,identity)))) = greatest_lower_bound(X10,greatest_lower_bound(X11,identity))]. % 3.28/3.66 [1326=param(1319,823),[54,15], % 3.28/3.66 greatest_lower_bound(identity,greatest_lower_bound(X10,inverse(X10))) = greatest_lower_bound(X10,inverse(X10))]. % 3.28/3.66 [1334=param(80,1326),[], % 3.28/3.66 least_upper_bound(identity,greatest_lower_bound(X10,greatest_lower_bound(X11,inverse(X11)))) = identity]. % 3.28/3.66 [1411=param(1334,58),[], % 3.28/3.66 least_upper_bound(identity,greatest_lower_bound(X10,inverse(least_upper_bound(X11,X10)))) = identity]. % 3.28/3.66 [1416=param(1334,188),[], % 3.28/3.66 least_upper_bound(identity,greatest_lower_bound(inverse(X10),greatest_lower_bound(X10,X11))) = identity]. % 3.28/3.66 [1425=param(865,1416),[3,15,1416,3], % 3.28/3.66 greatest_lower_bound(identity,inverse(greatest_lower_bound(inverse(X10),greatest_lower_bound(X10,X11)))) = identity]. % 3.28/3.66 [1434=param(1411,861),[], % 3.28/3.66 least_upper_bound(identity,inverse(least_upper_bound(X10,inverse(X10)))) = identity]. % 3.28/3.66 [1448=param(886,1434),[2,3,14,2], % 3.28/3.66 least_upper_bound(identity,least_upper_bound(X10,inverse(X10))) = least_upper_bound(X10,inverse(X10))]. % 3.28/3.66 [1472=param(93,1448),[], % 3.28/3.66 greatest_lower_bound(identity,least_upper_bound(X10,least_upper_bound(X11,inverse(X11)))) = identity]. % 3.28/3.66 [1509=param(1472,43),[], % 3.28/3.66 greatest_lower_bound(identity,least_upper_bound(X10,inverse(greatest_lower_bound(X10,X11)))) = identity]. % 3.28/3.66 [1554=param(13,1509),[], % 3.28/3.66 greatest_lower_bound(identity,greatest_lower_bound(least_upper_bound(X11,inverse(greatest_lower_bound(X11,X12))),X10)) = greatest_lower_bound(identity,X10)]. % 3.28/3.66 [1732=param(188,1425),[], % 3.28/3.66 greatest_lower_bound(X10,identity) = greatest_lower_bound(inverse(greatest_lower_bound(inverse(X11),greatest_lower_bound(X11,X12))),greatest_lower_bound(identity,X10))]. % 3.28/3.66 [2194=param(1317,55),[], % 3.28/3.66 greatest_lower_bound(inverse(greatest_lower_bound(X10,identity)),greatest_lower_bound(X10,X11)) = greatest_lower_bound(X10,greatest_lower_bound(identity,X11))]. % 3.28/3.66 [2195=param(2194,15),[], % 3.28/3.66 greatest_lower_bound(inverse(greatest_lower_bound(identity,X10)),greatest_lower_bound(X10,X11)) = greatest_lower_bound(X10,greatest_lower_bound(identity,X11))]. % 3.28/3.66 [2206=param(2195,1509),[3,1554], % 3.28/3.66 greatest_lower_bound(least_upper_bound(X11,inverse(greatest_lower_bound(X11,X12))),greatest_lower_bound(identity,X10)) = greatest_lower_bound(identity,X10)]. % 3.28/3.66 [2598=param(363,356),[14,2,2], % 3.28/3.66 least_upper_bound(inverse(least_upper_bound(identity,inverse(X10))),multiply(X10,inverse(least_upper_bound(identity,inverse(X10))))) = X10]. % 3.28/3.66 [2774=param(391,830),[15], % 3.28/3.66 greatest_lower_bound(least_upper_bound(X10,identity),inverse(greatest_lower_bound(identity,inverse(X10)))) = least_upper_bound(X10,identity)]. % 3.28/3.66 [2777=param(829,2774),[15,54,15,427,861], % 3.28/3.66 greatest_lower_bound(identity,inverse(X10)) = inverse(least_upper_bound(X10,identity))]. % 3.28/3.66 [2803=param(2777,2),[14], % 3.28/3.66 greatest_lower_bound(identity,X10) = inverse(least_upper_bound(identity,inverse(X10)))]. % 3.28/3.66 [2810=demod(341),[2803,2,7,33,66], % 3.28/3.66 inverse(greatest_lower_bound(inverse(X10),X11)) = least_upper_bound(X10,inverse(X11))]. % 3.28/3.66 [2883=demod(2206),[2803,2803], % 3.28/3.66 greatest_lower_bound(least_upper_bound(X10,inverse(greatest_lower_bound(X10,X11))),inverse(least_upper_bound(identity,inverse(X12)))) = inverse(least_upper_bound(identity,inverse(X12)))]. % 3.28/3.66 [2895=demod(1732),[2810,2803,2883], % 3.28/3.66 greatest_lower_bound(X10,identity) = inverse(least_upper_bound(identity,inverse(X10)))]. % 3.28/3.66 [3247=param(6,2895),[33,15], % 3.28/3.66 multiply(X10,inverse(least_upper_bound(identity,inverse(X11)))) = greatest_lower_bound(X10,multiply(X10,X11))]. % 3.28/3.66 [3249=demod(2598),[3247], % 3.28/3.66 least_upper_bound(inverse(least_upper_bound(identity,inverse(X10))),greatest_lower_bound(X10,multiply(X10,X10))) = X10]. % 3.28/3.66 [3250=param(20,2895),[33,15,3249,19], % 3.28/3.66 thmtrue = thmfalse]. % 3.28/3.66 % SZS output end CNFRefutation % 3.28/3.66 Space: 16242 KB %------------------------------------------------------------------------------