%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP167-5 : TPTP v8.1.0. Bugfixed v1.2.1. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n008.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 0.88s 1.24s % Output : CNFRefutation 0.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GRP167-5 : TPTP v8.1.0. Bugfixed v1.2.1. % 0.12/0.13 % Command : fiesta-wrapper %s % 0.12/0.34 % Computer : n008.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jun 14 13:59:07 EDT 2022 % 0.12/0.34 % CPUTime : % 0.88/1.24 Theorem Proved. % 0.88/1.24 % SZS status Unsatisfiable % 0.88/1.24 % SZS output start CNFRefutation % 0.88/1.24 [1=axiom,[], % 0.88/1.24 greatest_lower_bound(X10,least_upper_bound(X11,X12)) = least_upper_bound(greatest_lower_bound(X10,X11),greatest_lower_bound(X10,X12))]. % 0.88/1.24 [2=axiom,[1], % 0.88/1.24 least_upper_bound(greatest_lower_bound(least_upper_bound(X10,X11),X10),greatest_lower_bound(least_upper_bound(X10,X11),X12)) = least_upper_bound(X10,greatest_lower_bound(X11,X12))]. % 0.88/1.24 [3=axiom,[], % 0.88/1.24 greatest_lower_bound(X10,identity) = negative_part(X10)]. % 0.88/1.24 [4=axiom,[], % 0.88/1.24 least_upper_bound(X10,identity) = positive_part(X10)]. % 0.88/1.24 [5=axiom,[], % 0.88/1.24 greatest_lower_bound(inverse(X10),inverse(X11)) = inverse(least_upper_bound(X10,X11))]. % 0.88/1.24 [6=axiom,[], % 0.88/1.24 multiply(greatest_lower_bound(X10,X11),X12) = greatest_lower_bound(multiply(X10,X12),multiply(X11,X12))]. % 0.88/1.24 [7=axiom,[], % 0.88/1.24 multiply(least_upper_bound(X10,X11),X12) = least_upper_bound(multiply(X10,X12),multiply(X11,X12))]. % 0.88/1.24 [8=axiom,[], % 0.88/1.24 multiply(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(multiply(X10,X11),multiply(X10,X12))]. % 0.88/1.24 [11=axiom,[], % 0.88/1.24 least_upper_bound(X10,greatest_lower_bound(X10,X11)) = X10]. % 0.88/1.24 [12=axiom,[], % 0.88/1.24 greatest_lower_bound(X10,X10) = X10]. % 0.88/1.24 [14=axiom,[], % 0.88/1.24 least_upper_bound(least_upper_bound(X10,X11),X12) = least_upper_bound(X10,least_upper_bound(X11,X12))]. % 0.88/1.24 [16=axiom,[], % 0.88/1.24 least_upper_bound(X10,X11) = least_upper_bound(X11,X10)]. % 0.88/1.24 [17=axiom,[], % 0.88/1.24 greatest_lower_bound(X10,X11) = greatest_lower_bound(X11,X10)]. % 0.88/1.24 [18=demod(2),[17,1,12,11], % 0.88/1.24 least_upper_bound(X10,greatest_lower_bound(least_upper_bound(X10,X11),X12)) = least_upper_bound(X10,greatest_lower_bound(X11,X12))]. % 0.88/1.24 [19=axiom,[], % 0.88/1.24 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 0.88/1.24 [20=axiom,[], % 0.88/1.24 multiply(inverse(X10),X10) = identity]. % 0.88/1.24 [21=axiom,[], % 0.88/1.24 multiply(identity,X10) = X10]. % 0.88/1.24 [22=axiom,[], % 0.88/1.24 thtop(X10,X10) = thmfalse]. % 0.88/1.24 [23=axiom,[], % 0.88/1.24 thtop(a,multiply(positive_part(a),negative_part(a))) = thmtrue]. % 0.88/1.24 [24=param(1,4),[3,16], % 0.88/1.24 greatest_lower_bound(X10,positive_part(X11)) = least_upper_bound(negative_part(X10),greatest_lower_bound(X10,X11))]. % 0.88/1.24 [29=param(11,3),[], % 0.88/1.24 least_upper_bound(X10,negative_part(X10)) = X10]. % 0.88/1.24 [32=param(6,3),[21,17], % 0.88/1.24 multiply(negative_part(X10),X11) = greatest_lower_bound(X11,multiply(X10,X11))]. % 0.88/1.24 [34=param(17,3),[], % 0.88/1.24 greatest_lower_bound(identity,X10) = negative_part(X10)]. % 0.88/1.24 [39=param(7,4),[21,16], % 0.88/1.24 multiply(positive_part(X10),X11) = least_upper_bound(X11,multiply(X10,X11))]. % 0.88/1.24 [44=param(8,3),[], % 0.88/1.24 multiply(X10,negative_part(X11)) = greatest_lower_bound(multiply(X10,X11),multiply(X10,identity))]. % 0.88/1.24 [46=param(16,4),[], % 0.88/1.24 least_upper_bound(identity,X10) = positive_part(X10)]. % 0.88/1.24 [56=param(14,11),[], % 0.88/1.24 least_upper_bound(X10,least_upper_bound(greatest_lower_bound(X10,X12),X11)) = least_upper_bound(X10,X11)]. % 0.88/1.24 [81=param(18,4),[34], % 0.88/1.24 least_upper_bound(X10,greatest_lower_bound(positive_part(X10),X11)) = least_upper_bound(X10,negative_part(X11))]. % 0.88/1.24 [94=param(19,20),[21], % 0.88/1.24 multiply(inverse(X11),multiply(X11,X10)) = X10]. % 0.88/1.24 [108=param(94,20),[], % 0.88/1.24 multiply(inverse(inverse(X10)),identity) = X10]. % 0.88/1.24 [110=param(94,32),[8], % 0.88/1.24 greatest_lower_bound(multiply(inverse(negative_part(X10)),X11),multiply(inverse(negative_part(X10)),multiply(X10,X11))) = X11]. % 0.88/1.24 [112=param(94,94),[], % 0.88/1.24 multiply(inverse(inverse(X10)),X11) = multiply(X10,X11)]. % 0.88/1.24 [113=demod(108),[112], % 0.88/1.24 multiply(X10,identity) = X10]. % 0.88/1.24 [115=demod(44),[113,17], % 0.88/1.24 multiply(X10,negative_part(X11)) = greatest_lower_bound(X10,multiply(X10,X11))]. % 0.88/1.24 [116=param(113,20),[], % 0.88/1.24 inverse(identity) = identity]. % 0.88/1.24 [118=param(5,116),[34,46], % 0.88/1.24 inverse(positive_part(X10)) = negative_part(inverse(X10))]. % 0.88/1.24 [165=param(23,115),[39,1,17,24,12,16,29,81], % 0.88/1.24 thtop(a,least_upper_bound(a,negative_part(multiply(a,a)))) = thmtrue]. % 0.88/1.24 [171=param(112,113),[113], % 0.88/1.24 inverse(inverse(X10)) = X10]. % 0.88/1.24 [174=param(5,171),[], % 0.88/1.24 greatest_lower_bound(X10,inverse(X11)) = inverse(least_upper_bound(inverse(X10),X11))]. % 0.88/1.24 [179=param(171,118),[], % 0.88/1.24 inverse(negative_part(inverse(X10))) = positive_part(X10)]. % 0.88/1.24 [188=param(179,171),[], % 0.88/1.24 inverse(negative_part(X10)) = positive_part(inverse(X10))]. % 0.88/1.24 [189=demod(110),[188,39,188,39,94,16,1,17,1,12,11,17,1,17,56], % 0.88/1.24 least_upper_bound(X10,greatest_lower_bound(multiply(X11,X10),multiply(inverse(X11),X10))) = X10]. % 0.88/1.24 [213=param(174,171),[], % 0.88/1.24 greatest_lower_bound(X10,X11) = inverse(least_upper_bound(inverse(X10),inverse(X11)))]. % 0.88/1.24 [236=demod(189),[213], % 0.88/1.24 least_upper_bound(X10,inverse(least_upper_bound(inverse(multiply(X11,X10)),inverse(multiply(inverse(X11),X10))))) = X10]. % 0.88/1.24 [666=param(236,20),[116,171,46,118,171], % 0.88/1.24 least_upper_bound(X10,negative_part(multiply(X10,X10))) = X10]. % 0.88/1.24 [674=param(165,666),[22], % 0.88/1.24 thmtrue = thmfalse]. % 0.88/1.24 % SZS output end CNFRefutation % 0.88/1.24 Space: 1179 KB %------------------------------------------------------------------------------