%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP167-1 : TPTP v8.1.0. Bugfixed v1.2.1. % 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 : Sat Jul 16 09:13:01 EDT 2022 % Result : Unsatisfiable 3.02s 3.43s % Output : CNFRefutation 3.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : GRP167-1 : TPTP v8.1.0. Bugfixed v1.2.1. % 0.00/0.09 % Command : fiesta-wrapper %s % 0.09/0.28 % Computer : n032.cluster.edu % 0.09/0.28 % Model : x86_64 x86_64 % 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.28 % Memory : 8042.1875MB % 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.28 % CPULimit : 300 % 0.09/0.28 % WCLimit : 600 % 0.09/0.28 % DateTime : Mon Jun 13 09:55:11 EDT 2022 % 0.09/0.28 % CPUTime : % 3.02/3.43 Theorem Proved. % 3.02/3.43 % SZS status Unsatisfiable % 3.02/3.43 % SZS output start CNFRefutation % 3.02/3.43 [1=axiom,[], % 3.02/3.43 greatest_lower_bound(X10,least_upper_bound(X11,X12)) = least_upper_bound(greatest_lower_bound(X10,X11),greatest_lower_bound(X10,X12))]. % 3.02/3.43 [2=axiom,[1], % 3.02/3.43 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))]. % 3.02/3.43 [3=axiom,[], % 3.02/3.43 greatest_lower_bound(X10,identity) = negative_part(X10)]. % 3.02/3.43 [4=axiom,[], % 3.02/3.43 least_upper_bound(X10,identity) = positive_part(X10)]. % 3.02/3.43 [5=axiom,[], % 3.02/3.43 multiply(greatest_lower_bound(X10,X11),X12) = greatest_lower_bound(multiply(X10,X12),multiply(X11,X12))]. % 3.02/3.43 [6=axiom,[], % 3.02/3.43 multiply(least_upper_bound(X10,X11),X12) = least_upper_bound(multiply(X10,X12),multiply(X11,X12))]. % 3.02/3.43 [7=axiom,[], % 3.02/3.43 multiply(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(multiply(X10,X11),multiply(X10,X12))]. % 3.02/3.43 [8=axiom,[], % 3.02/3.43 multiply(X10,least_upper_bound(X11,X12)) = least_upper_bound(multiply(X10,X11),multiply(X10,X12))]. % 3.02/3.43 [10=axiom,[], % 3.02/3.43 least_upper_bound(X10,greatest_lower_bound(X10,X11)) = X10]. % 3.02/3.43 [11=axiom,[], % 3.02/3.43 greatest_lower_bound(X10,X10) = X10]. % 3.02/3.43 [12=axiom,[], % 3.02/3.43 least_upper_bound(X10,X10) = X10]. % 3.02/3.43 [13=axiom,[], % 3.02/3.43 least_upper_bound(least_upper_bound(X10,X11),X12) = least_upper_bound(X10,least_upper_bound(X11,X12))]. % 3.02/3.43 [14=axiom,[], % 3.02/3.43 greatest_lower_bound(greatest_lower_bound(X10,X11),X12) = greatest_lower_bound(X10,greatest_lower_bound(X11,X12))]. % 3.02/3.43 [15=axiom,[], % 3.02/3.43 least_upper_bound(X10,X11) = least_upper_bound(X11,X10)]. % 3.02/3.43 [16=axiom,[], % 3.02/3.43 greatest_lower_bound(X10,X11) = greatest_lower_bound(X11,X10)]. % 3.02/3.43 [17=demod(2),[16,1,11,10], % 3.02/3.43 least_upper_bound(X10,greatest_lower_bound(least_upper_bound(X10,X11),X12)) = least_upper_bound(X10,greatest_lower_bound(X11,X12))]. % 3.02/3.43 [18=axiom,[], % 3.02/3.43 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 3.02/3.43 [19=axiom,[], % 3.02/3.43 multiply(inverse(X10),X10) = identity]. % 3.02/3.43 [20=axiom,[], % 3.02/3.43 multiply(identity,X10) = X10]. % 3.02/3.43 [21=axiom,[], % 3.02/3.43 thtop(X10,X10) = thmfalse]. % 3.02/3.43 [22=axiom,[], % 3.02/3.43 thtop(a,multiply(positive_part(a),negative_part(a))) = thmtrue]. % 3.02/3.43 [23=param(1,4),[3,15], % 3.02/3.43 greatest_lower_bound(X10,positive_part(X11)) = least_upper_bound(negative_part(X10),greatest_lower_bound(X10,X11))]. % 3.02/3.43 [25=param(3,11),[], % 3.02/3.43 negative_part(identity) = identity]. % 3.02/3.43 [26=param(5,3),[20,16], % 3.02/3.43 multiply(negative_part(X10),X11) = greatest_lower_bound(X11,multiply(X10,X11))]. % 3.02/3.43 [28=param(1,10),[], % 3.02/3.43 least_upper_bound(greatest_lower_bound(X10,X11),greatest_lower_bound(X10,greatest_lower_bound(X11,X12))) = greatest_lower_bound(X10,X11)]. % 3.02/3.43 [29=param(10,3),[], % 3.02/3.43 least_upper_bound(X10,negative_part(X10)) = X10]. % 3.02/3.43 [31=param(6,4),[20,15], % 3.02/3.43 multiply(positive_part(X10),X11) = least_upper_bound(X11,multiply(X10,X11))]. % 3.02/3.43 [33=param(16,1),[], % 3.02/3.43 greatest_lower_bound(least_upper_bound(X10,X11),X12) = least_upper_bound(greatest_lower_bound(X12,X10),greatest_lower_bound(X12,X11))]. % 3.02/3.43 [34=param(16,3),[], % 3.02/3.43 greatest_lower_bound(identity,X10) = negative_part(X10)]. % 3.02/3.43 [35=param(10,16),[], % 3.02/3.43 least_upper_bound(X10,greatest_lower_bound(X11,X10)) = X10]. % 3.02/3.43 [36=param(34,1),[34,34], % 3.02/3.43 least_upper_bound(negative_part(X10),negative_part(X11)) = negative_part(least_upper_bound(X10,X11))]. % 3.02/3.43 [37=param(10,34),[], % 3.02/3.43 least_upper_bound(identity,negative_part(X10)) = identity]. % 3.02/3.43 [38=param(7,3),[], % 3.02/3.43 multiply(X10,negative_part(X11)) = greatest_lower_bound(multiply(X10,X11),multiply(X10,identity))]. % 3.02/3.43 [39=param(7,19),[], % 3.02/3.43 greatest_lower_bound(multiply(inverse(greatest_lower_bound(X10,X11)),X10),multiply(inverse(greatest_lower_bound(X10,X11)),X11)) = identity]. % 3.02/3.43 [43=param(8,4),[], % 3.02/3.43 multiply(X10,positive_part(X11)) = least_upper_bound(multiply(X10,X11),multiply(X10,identity))]. % 3.02/3.43 [44=param(8,19),[], % 3.02/3.43 least_upper_bound(multiply(inverse(least_upper_bound(X10,X11)),X10),multiply(inverse(least_upper_bound(X10,X11)),X11)) = identity]. % 3.02/3.43 [45=param(15,4),[], % 3.02/3.43 least_upper_bound(identity,X10) = positive_part(X10)]. % 3.02/3.43 [46=demod(37),[45], % 3.02/3.43 positive_part(negative_part(X10)) = identity]. % 3.02/3.43 [47=param(13,4),[4], % 3.02/3.43 least_upper_bound(X10,positive_part(X11)) = positive_part(least_upper_bound(X10,X11))]. % 3.02/3.43 [48=param(13,4),[45,47], % 3.02/3.43 least_upper_bound(positive_part(X10),X11) = positive_part(least_upper_bound(X10,X11))]. % 3.02/3.43 [52=param(13,12),[], % 3.02/3.43 least_upper_bound(X10,least_upper_bound(X10,X11)) = least_upper_bound(X10,X11)]. % 3.02/3.43 [53=param(13,15),[], % 3.02/3.43 least_upper_bound(X10,least_upper_bound(X11,X12)) = least_upper_bound(X12,least_upper_bound(X10,X11))]. % 3.02/3.43 [54=param(13,15),[13], % 3.02/3.43 least_upper_bound(X10,least_upper_bound(X11,X12)) = least_upper_bound(X11,least_upper_bound(X10,X12))]. % 3.02/3.43 [56=param(13,29),[], % 3.02/3.43 least_upper_bound(X10,least_upper_bound(negative_part(X10),X11)) = least_upper_bound(X10,X11)]. % 3.02/3.43 [59=param(48,12),[47,12], % 3.02/3.43 positive_part(positive_part(X10)) = positive_part(X10)]. % 3.02/3.43 [64=param(14,3),[3], % 3.02/3.43 greatest_lower_bound(X10,negative_part(X11)) = negative_part(greatest_lower_bound(X10,X11))]. % 3.02/3.43 [65=param(14,3),[34,64], % 3.02/3.43 greatest_lower_bound(negative_part(X10),X11) = negative_part(greatest_lower_bound(X10,X11))]. % 3.02/3.43 [67=param(14,11),[], % 3.02/3.43 greatest_lower_bound(X10,greatest_lower_bound(X10,X11)) = greatest_lower_bound(X10,X11)]. % 3.02/3.43 [68=param(14,16),[], % 3.02/3.43 greatest_lower_bound(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(X12,greatest_lower_bound(X10,X11))]. % 3.02/3.43 [69=param(14,16),[14], % 3.02/3.43 greatest_lower_bound(X10,greatest_lower_bound(X11,X12)) = greatest_lower_bound(X11,greatest_lower_bound(X10,X12))]. % 3.02/3.43 [74=param(17,3),[3], % 3.02/3.43 least_upper_bound(X10,negative_part(least_upper_bound(X10,X11))) = least_upper_bound(X10,negative_part(X11))]. % 3.02/3.43 [75=param(17,4),[34], % 3.02/3.43 least_upper_bound(X10,greatest_lower_bound(positive_part(X10),X11)) = least_upper_bound(X10,negative_part(X11))]. % 3.02/3.43 [85=param(18,19),[20], % 3.02/3.43 multiply(inverse(X11),multiply(X11,X10)) = X10]. % 3.02/3.43 [89=param(14,23),[], % 3.02/3.43 greatest_lower_bound(least_upper_bound(negative_part(X10),greatest_lower_bound(X10,X11)),X12) = greatest_lower_bound(X10,greatest_lower_bound(positive_part(X11),X12))]. % 3.02/3.43 [91=param(23,34),[25,34,45,46], % 3.02/3.43 negative_part(positive_part(X10)) = identity]. % 3.02/3.43 [93=param(65,91),[34], % 3.02/3.43 negative_part(greatest_lower_bound(positive_part(X11),X10)) = negative_part(X10)]. % 3.02/3.43 [99=param(85,19),[], % 3.02/3.43 multiply(inverse(inverse(X10)),identity) = X10]. % 3.02/3.43 [102=param(85,85),[], % 3.02/3.43 multiply(inverse(inverse(X10)),X11) = multiply(X10,X11)]. % 3.02/3.43 [103=demod(99),[102], % 3.02/3.43 multiply(X10,identity) = X10]. % 3.02/3.43 [104=demod(43),[103,15], % 3.02/3.43 multiply(X10,positive_part(X11)) = least_upper_bound(X10,multiply(X10,X11))]. % 3.02/3.43 [105=demod(38),[103,16], % 3.02/3.43 multiply(X10,negative_part(X11)) = greatest_lower_bound(X10,multiply(X10,X11))]. % 3.02/3.43 [110=param(85,31),[8], % 3.02/3.43 least_upper_bound(multiply(inverse(positive_part(X10)),X11),multiply(inverse(positive_part(X10)),multiply(X10,X11))) = X11]. % 3.02/3.43 [111=param(105,19),[], % 3.02/3.43 greatest_lower_bound(inverse(negative_part(X10)),multiply(inverse(negative_part(X10)),X10)) = identity]. % 3.02/3.43 [112=param(22,105),[31,1,16,23,11,15,29,75], % 3.02/3.43 thtop(a,least_upper_bound(a,negative_part(multiply(a,a)))) = thmtrue]. % 3.02/3.43 [113=param(104,19),[], % 3.02/3.43 least_upper_bound(inverse(positive_part(X10)),multiply(inverse(positive_part(X10)),X10)) = identity]. % 3.02/3.43 [114=param(102,19),[], % 3.02/3.43 multiply(X10,inverse(X10)) = identity]. % 3.02/3.43 [116=param(102,103),[103], % 3.02/3.43 inverse(inverse(X10)) = X10]. % 3.02/3.43 [119=param(114,18),[], % 3.02/3.43 multiply(X10,multiply(X11,inverse(multiply(X10,X11)))) = identity]. % 3.02/3.43 [146=param(67,16),[], % 3.02/3.43 greatest_lower_bound(X10,greatest_lower_bound(X11,X10)) = greatest_lower_bound(X10,X11)]. % 3.02/3.43 [151=param(146,23),[1,64,93,68], % 3.02/3.43 least_upper_bound(negative_part(X10),greatest_lower_bound(X11,greatest_lower_bound(positive_part(X11),X10))) = greatest_lower_bound(positive_part(X11),X10)]. % 3.02/3.43 [152=param(146,33),[1,16,1,146,28,1,16,1,146,15,28], % 3.02/3.43 greatest_lower_bound(least_upper_bound(X10,X11),X12) = least_upper_bound(greatest_lower_bound(X10,X12),greatest_lower_bound(X11,X12))]. % 3.02/3.43 [157=demod(89),[152,65,14], % 3.02/3.43 greatest_lower_bound(X10,greatest_lower_bound(positive_part(X12),X11)) = least_upper_bound(negative_part(greatest_lower_bound(X10,X11)),greatest_lower_bound(X10,greatest_lower_bound(X12,X11)))]. % 3.02/3.43 [158=demod(151),[157,67,15,29], % 3.02/3.43 greatest_lower_bound(positive_part(X11),X10) = least_upper_bound(negative_part(X10),greatest_lower_bound(X11,X10))]. % 3.02/3.43 [170=param(67,39),[3,39], % 3.02/3.43 negative_part(multiply(inverse(greatest_lower_bound(X10,X11)),X10)) = identity]. % 3.02/3.43 [189=param(52,44),[4,44], % 3.02/3.43 positive_part(multiply(inverse(least_upper_bound(X10,X11)),X10)) = identity]. % 3.02/3.43 [198=param(31,189),[20,18], % 3.02/3.43 least_upper_bound(X10,multiply(inverse(least_upper_bound(X11,X12)),multiply(X11,X10))) = X10]. % 3.02/3.43 [204=param(26,170),[20,18], % 3.02/3.43 greatest_lower_bound(X10,multiply(inverse(greatest_lower_bound(X11,X12)),multiply(X11,X10))) = X10]. % 3.02/3.43 [228=param(56,15),[], % 3.02/3.43 least_upper_bound(X10,least_upper_bound(X11,negative_part(X10))) = least_upper_bound(X10,X11)]. % 3.02/3.43 [237=param(54,56),[], % 3.02/3.43 least_upper_bound(negative_part(X10),least_upper_bound(X10,X11)) = least_upper_bound(X10,X11)]. % 3.02/3.43 [247=param(228,36),[], % 3.02/3.43 least_upper_bound(X10,negative_part(least_upper_bound(X11,X10))) = least_upper_bound(X10,negative_part(X11))]. % 3.02/3.43 [313=param(85,119),[103], % 3.02/3.43 multiply(X11,inverse(multiply(X10,X11))) = inverse(X10)]. % 3.02/3.43 [315=param(313,6),[], % 3.02/3.43 multiply(X10,inverse(least_upper_bound(multiply(X11,X10),multiply(X12,X10)))) = inverse(least_upper_bound(X11,X12))]. % 3.02/3.43 [321=param(85,313),[], % 3.02/3.43 multiply(inverse(X10),inverse(X11)) = inverse(multiply(X11,X10))]. % 3.02/3.43 [329=param(321,116),[], % 3.02/3.43 multiply(inverse(X10),X11) = inverse(multiply(inverse(X11),X10))]. % 3.02/3.43 [343=demod(111),[329,105,19,3], % 3.02/3.43 greatest_lower_bound(inverse(negative_part(X10)),inverse(negative_part(inverse(X10)))) = identity]. % 3.02/3.43 [344=demod(113),[329,104,19,4], % 3.02/3.43 least_upper_bound(inverse(positive_part(X10)),inverse(positive_part(inverse(X10)))) = identity]. % 3.02/3.43 [394=param(110,31),[59,59,8,110,15], % 3.02/3.43 least_upper_bound(X10,multiply(inverse(positive_part(X11)),X10)) = X10]. % 3.02/3.43 [395=param(110,114),[321,104,103,15], % 3.02/3.43 least_upper_bound(inverse(positive_part(X10)),inverse(least_upper_bound(X10,multiply(X10,X10)))) = inverse(X10)]. % 3.02/3.43 [403=param(394,45),[103], % 3.02/3.43 positive_part(inverse(positive_part(X10))) = identity]. % 3.02/3.43 [404=param(394,48),[104], % 3.02/3.43 positive_part(least_upper_bound(X10,least_upper_bound(inverse(positive_part(X11)),multiply(inverse(positive_part(X11)),X10)))) = positive_part(X10)]. % 3.02/3.43 [406=param(54,394),[], % 3.02/3.43 least_upper_bound(X11,least_upper_bound(X10,multiply(inverse(positive_part(X12)),X11))) = least_upper_bound(X10,X11)]. % 3.02/3.43 [407=demod(404),[406], % 3.02/3.43 positive_part(least_upper_bound(inverse(positive_part(X10)),X11)) = positive_part(X11)]. % 3.02/3.43 [425=param(158,403),[34], % 3.02/3.43 least_upper_bound(negative_part(X10),greatest_lower_bound(inverse(positive_part(X11)),X10)) = negative_part(X10)]. % 3.02/3.43 [668=param(425,11),[15,29], % 3.02/3.43 negative_part(inverse(positive_part(X10))) = inverse(positive_part(X10))]. % 3.02/3.43 [679=param(105,668),[], % 3.02/3.43 greatest_lower_bound(X10,multiply(X10,inverse(positive_part(X11)))) = multiply(X10,inverse(positive_part(X11)))]. % 3.02/3.43 [755=param(198,19),[103], % 3.02/3.43 least_upper_bound(X10,inverse(least_upper_bound(inverse(X10),X11))) = X10]. % 3.02/3.43 [758=param(198,114),[103], % 3.02/3.43 least_upper_bound(inverse(X10),inverse(least_upper_bound(X10,X11))) = inverse(X10)]. % 3.02/3.43 [764=param(755,4),[], % 3.02/3.43 least_upper_bound(X10,inverse(positive_part(inverse(X10)))) = X10]. % 3.02/3.43 [786=param(54,764),[], % 3.02/3.43 least_upper_bound(X11,least_upper_bound(X10,inverse(positive_part(inverse(X11))))) = least_upper_bound(X10,X11)]. % 3.02/3.43 [806=param(758,237),[], % 3.02/3.43 least_upper_bound(inverse(negative_part(X10)),inverse(least_upper_bound(X10,X11))) = inverse(negative_part(X10))]. % 3.02/3.43 [819=param(204,19),[103], % 3.02/3.43 greatest_lower_bound(X10,inverse(greatest_lower_bound(inverse(X10),X11))) = X10]. % 3.02/3.43 [822=param(204,114),[103], % 3.02/3.43 greatest_lower_bound(inverse(X10),inverse(greatest_lower_bound(X10,X11))) = inverse(X10)]. % 3.02/3.43 [828=param(819,3),[], % 3.02/3.43 greatest_lower_bound(X10,inverse(negative_part(inverse(X10)))) = X10]. % 3.02/3.43 [834=param(819,64),[], % 3.02/3.43 greatest_lower_bound(X10,inverse(negative_part(greatest_lower_bound(inverse(X10),X11)))) = X10]. % 3.02/3.43 [848=param(69,828),[], % 3.02/3.43 greatest_lower_bound(X11,greatest_lower_bound(X10,inverse(negative_part(inverse(X11))))) = greatest_lower_bound(X10,X11)]. % 3.02/3.43 [855=param(822,3),[], % 3.02/3.43 greatest_lower_bound(inverse(X10),inverse(negative_part(X10))) = inverse(X10)]. % 3.02/3.43 [882=param(35,855),[15], % 3.02/3.43 least_upper_bound(inverse(X10),inverse(negative_part(X10))) = inverse(negative_part(X10))]. % 3.02/3.43 [888=param(54,882),[], % 3.02/3.43 least_upper_bound(inverse(X11),least_upper_bound(X10,inverse(negative_part(X11)))) = least_upper_bound(X10,inverse(negative_part(X11)))]. % 3.02/3.43 [1043=param(848,343),[3,16], % 3.02/3.43 greatest_lower_bound(X10,inverse(negative_part(X10))) = negative_part(X10)]. % 3.02/3.43 [1049=param(69,1043),[64], % 3.02/3.43 greatest_lower_bound(X11,greatest_lower_bound(X10,inverse(negative_part(X11)))) = negative_part(greatest_lower_bound(X10,X11))]. % 3.02/3.43 [1053=param(848,1043),[64,16], % 3.02/3.43 negative_part(greatest_lower_bound(X10,inverse(X10))) = greatest_lower_bound(X10,inverse(X10))]. % 3.02/3.43 [1056=param(46,1053),[], % 3.02/3.43 positive_part(greatest_lower_bound(X10,inverse(X10))) = identity]. % 3.02/3.43 [1079=param(158,1056),[34,14], % 3.02/3.43 least_upper_bound(negative_part(X10),greatest_lower_bound(X11,greatest_lower_bound(inverse(X11),X10))) = negative_part(X10)]. % 3.02/3.43 [1278=param(806,15),[], % 3.02/3.43 least_upper_bound(inverse(negative_part(X10)),inverse(least_upper_bound(X11,X10))) = inverse(negative_part(X10))]. % 3.02/3.43 [1286=param(786,344),[4,15], % 3.02/3.43 least_upper_bound(X10,inverse(positive_part(X10))) = positive_part(X10)]. % 3.02/3.43 [1300=param(786,1286),[47,15], % 3.02/3.43 positive_part(least_upper_bound(X10,inverse(X10))) = least_upper_bound(X10,inverse(X10))]. % 3.02/3.43 [1304=param(91,1300),[], % 3.02/3.43 negative_part(least_upper_bound(X10,inverse(X10))) = identity]. % 3.02/3.43 [1313=param(668,1300),[1300], % 3.02/3.43 negative_part(inverse(least_upper_bound(X10,inverse(X10)))) = inverse(least_upper_bound(X10,inverse(X10)))]. % 3.02/3.43 [1327=param(247,1304),[4,15], % 3.02/3.43 least_upper_bound(negative_part(X10),inverse(X10)) = positive_part(inverse(X10))]. % 3.02/3.43 [2219=param(315,19),[45], % 3.02/3.43 multiply(X10,inverse(positive_part(multiply(X11,X10)))) = inverse(least_upper_bound(inverse(X10),X11))]. % 3.02/3.43 [2269=param(679,2219),[2219], % 3.02/3.43 greatest_lower_bound(X10,inverse(least_upper_bound(inverse(X10),X11))) = inverse(least_upper_bound(inverse(X10),X11))]. % 3.02/3.43 [2405=param(834,2269),[116], % 3.02/3.43 greatest_lower_bound(X10,inverse(negative_part(inverse(least_upper_bound(X10,X11))))) = X10]. % 3.02/3.43 [2409=param(2405,15),[], % 3.02/3.43 greatest_lower_bound(X10,inverse(negative_part(inverse(least_upper_bound(X11,X10))))) = X10]. % 3.02/3.43 [2425=param(1049,2409),[16], % 3.02/3.43 negative_part(greatest_lower_bound(X10,inverse(least_upper_bound(X11,X10)))) = greatest_lower_bound(X10,inverse(least_upper_bound(X11,X10)))]. % 3.02/3.43 [2809=param(407,395),[], % 3.02/3.43 positive_part(inverse(least_upper_bound(X10,multiply(X10,X10)))) = positive_part(inverse(X10))]. % 3.02/3.43 [3652=param(1079,16),[], % 3.02/3.43 least_upper_bound(negative_part(X10),greatest_lower_bound(X11,greatest_lower_bound(X10,inverse(X11)))) = negative_part(X10)]. % 3.02/3.43 [3662=param(3652,2409),[16,64,2425], % 3.02/3.43 least_upper_bound(negative_part(X10),greatest_lower_bound(X10,inverse(least_upper_bound(X11,X10)))) = negative_part(X10)]. % 3.02/3.43 [3666=param(3662,2269),[15], % 3.02/3.43 least_upper_bound(negative_part(X10),inverse(least_upper_bound(X10,inverse(X10)))) = negative_part(X10)]. % 3.02/3.43 [3673=param(1278,3666),[1313,116,15,53,15,888,1313,116], % 3.02/3.43 least_upper_bound(X10,inverse(negative_part(X10))) = least_upper_bound(X10,inverse(X10))]. % 3.02/3.43 [3684=param(2409,3673),[1313,116,1,16,1043,16,855,1327], % 3.02/3.43 inverse(negative_part(X10)) = positive_part(inverse(X10))]. % 3.02/3.43 [3785=param(116,3684),[], % 3.02/3.43 inverse(positive_part(inverse(X10))) = negative_part(X10)]. % 3.02/3.43 [3836=param(3785,116),[], % 3.02/3.43 inverse(positive_part(X10)) = negative_part(inverse(X10))]. % 3.02/3.43 [3951=param(3836,2809),[3836,116,116], % 3.02/3.43 negative_part(least_upper_bound(X10,multiply(X10,X10))) = negative_part(X10)]. % 3.02/3.43 [3968=param(74,3951),[29], % 3.02/3.43 least_upper_bound(X10,negative_part(multiply(X10,X10))) = X10]. % 3.02/3.43 [3978=param(112,3968),[21], % 3.02/3.43 thmtrue = thmfalse]. % 3.02/3.43 % SZS output end CNFRefutation % 3.02/3.43 Space: 11002 KB %------------------------------------------------------------------------------