%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LAT009-1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n021.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 : Sun Jul 17 04:55:23 EDT 2022 % Result : Unsatisfiable 3.24s 3.63s % Output : CNFRefutation 3.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : LAT009-1 : TPTP v8.1.0. Released v2.2.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 29 22:15:12 EDT 2022 % 0.12/0.34 % CPUTime : % 3.24/3.63 Theorem Proved. % 3.24/3.63 % SZS status Unsatisfiable % 3.24/3.63 % SZS output start CNFRefutation % 3.24/3.63 [1=axiom,[], % 3.24/3.63 meet(join(meet(join(X10,X11),X12),X11),join(X12,X10)) = join(meet(join(meet(X10,X11),X12),X11),meet(X12,X10))]. % 3.24/3.63 [2=axiom,[], % 3.24/3.63 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 3.24/3.63 [3=axiom,[], % 3.24/3.63 meet(meet(X10,X11),X12) = meet(X10,meet(X11,X12))]. % 3.24/3.63 [4=axiom,[], % 3.24/3.63 join(X10,X11) = join(X11,X10)]. % 3.24/3.63 [5=demod(1),[4,4], % 3.24/3.63 meet(join(X10,meet(join(X11,X10),X12)),join(X12,X11)) = join(meet(X12,X11),meet(join(meet(X11,X10),X12),X10))]. % 3.24/3.63 [6=axiom,[], % 3.24/3.63 meet(X10,X11) = meet(X11,X10)]. % 3.24/3.63 [7=demod(5),[6,6], % 3.24/3.63 meet(join(X10,X11),join(X12,meet(join(X11,X12),X10))) = join(meet(X10,X11),meet(X12,join(meet(X11,X12),X10)))]. % 3.24/3.63 [8=axiom,[], % 3.24/3.63 join(X10,meet(X10,X11)) = X10]. % 3.24/3.63 [9=axiom,[], % 3.24/3.63 meet(X10,join(X10,X11)) = X10]. % 3.24/3.63 [10=axiom,[], % 3.24/3.63 join(X10,X10) = X10]. % 3.24/3.63 [11=axiom,[], % 3.24/3.63 meet(X10,X10) = X10]. % 3.24/3.63 [12=axiom,[], % 3.24/3.63 thtop(X10,X10) = thmfalse]. % 3.24/3.63 [13=axiom,[6,4,4,6], % 3.24/3.63 thtop(join(a,meet(c,b)),meet(join(c,a),join(b,a))) = thmtrue]. % 3.24/3.63 [16=param(2,10),[], % 3.24/3.63 join(X10,join(X10,X11)) = join(X10,X11)]. % 3.24/3.63 [18=param(2,8),[], % 3.24/3.63 join(X10,join(meet(X10,X12),X11)) = join(X10,X11)]. % 3.24/3.63 [19=param(8,6),[], % 3.24/3.63 join(X10,meet(X11,X10)) = X10]. % 3.24/3.63 [20=param(3,6),[], % 3.24/3.63 meet(X10,meet(X11,X12)) = meet(X12,meet(X10,X11))]. % 3.24/3.63 [21=param(3,6),[3], % 3.24/3.63 meet(X10,meet(X11,X12)) = meet(X11,meet(X10,X12))]. % 3.24/3.63 [23=param(3,9),[], % 3.24/3.63 meet(X10,meet(X11,join(meet(X10,X11),X12))) = meet(X10,X11)]. % 3.24/3.63 [24=param(3,9),[], % 3.24/3.63 meet(X10,meet(join(X10,X12),X11)) = meet(X10,X11)]. % 3.24/3.63 [26=param(3,11),[], % 3.24/3.63 meet(X10,meet(X10,X11)) = meet(X10,X11)]. % 3.24/3.63 [27=param(19,2),[], % 3.24/3.63 join(X10,join(X11,meet(X12,join(X10,X11)))) = join(X10,X11)]. % 3.24/3.63 [28=param(2,19),[], % 3.24/3.63 join(X10,join(meet(X12,X10),X11)) = join(X10,X11)]. % 3.24/3.63 [29=param(19,3),[], % 3.24/3.63 join(X10,meet(X11,meet(X12,X10))) = X10]. % 3.24/3.63 [30=param(19,9),[2], % 3.24/3.63 join(X10,join(X11,X10)) = join(X10,X11)]. % 3.24/3.63 [31=param(4,2),[], % 3.24/3.63 join(X10,join(X11,X12)) = join(X11,join(X12,X10))]. % 3.24/3.63 [33=param(9,4),[], % 3.24/3.63 meet(X10,join(X11,X10)) = X10]. % 3.24/3.63 [34=param(8,7),[2,28], % 3.24/3.63 join(X10,join(X11,meet(X12,join(meet(X11,X12),X10)))) = join(X10,X11)]. % 3.24/3.63 [36=param(33,2),[], % 3.24/3.63 meet(X10,join(X11,join(X12,X10))) = X10]. % 3.24/3.63 [38=param(3,33),[], % 3.24/3.63 meet(X10,meet(join(X12,X10),X11)) = meet(X10,X11)]. % 3.24/3.63 [39=param(33,8),[3], % 3.24/3.63 meet(X10,meet(X11,X10)) = meet(X10,X11)]. % 3.24/3.63 [43=param(19,39),[], % 3.24/3.63 join(meet(X10,X11),meet(X11,X10)) = meet(X10,X11)]. % 3.24/3.63 [49=param(33,30),[], % 3.24/3.63 meet(join(X10,X11),join(X11,X10)) = join(X10,X11)]. % 3.24/3.63 [53=param(36,4),[2], % 3.24/3.63 meet(X10,join(X11,join(X10,X12))) = X10]. % 3.24/3.63 [54=param(36,8),[3], % 3.24/3.63 meet(X10,meet(X11,join(X12,X10))) = meet(X10,X11)]. % 3.24/3.63 [56=param(53,2),[], % 3.24/3.63 meet(X10,join(X11,join(X12,join(X10,X13)))) = X10]. % 3.24/3.63 [65=param(29,9),[2], % 3.24/3.63 join(X10,join(X11,meet(X12,X10))) = join(X10,X11)]. % 3.24/3.63 [72=param(18,4),[], % 3.24/3.63 join(X10,join(X11,meet(X10,X12))) = join(X10,X11)]. % 3.24/3.63 [75=param(53,18),[3], % 3.24/3.63 meet(X10,meet(X11,join(X10,X12))) = meet(X10,X11)]. % 3.24/3.63 [100=param(21,36),[], % 3.24/3.63 meet(X11,meet(X10,join(X12,join(X13,X11)))) = meet(X10,X11)]. % 3.24/3.63 [106=param(65,39),[], % 3.24/3.63 join(meet(X10,X11),join(X12,meet(X11,X10))) = join(meet(X10,X11),X12)]. % 3.24/3.63 [113=param(19,54),[], % 3.24/3.63 join(meet(X10,join(X11,X12)),meet(X12,X10)) = meet(X10,join(X11,X12))]. % 3.24/3.63 [115=param(54,30),[], % 3.24/3.63 meet(join(X10,X11),meet(X12,join(X11,X10))) = meet(join(X10,X11),X12)]. % 3.24/3.63 [117=param(23,6),[3,6], % 3.24/3.63 meet(X11,meet(X10,join(meet(X10,X11),X12))) = meet(X10,X11)]. % 3.24/3.63 [119=param(20,49),[115], % 3.24/3.63 meet(X10,join(X11,X12)) = meet(join(X12,X11),X10)]. % 3.24/3.63 [132=param(28,4),[2], % 3.24/3.63 join(meet(X12,X10),join(X11,X10)) = join(X10,X11)]. % 3.24/3.63 [140=param(132,4),[], % 3.24/3.63 join(meet(X10,X11),join(X11,X12)) = join(X11,X12)]. % 3.24/3.63 [159=param(31,43),[106], % 3.24/3.63 join(X10,meet(X11,X12)) = join(meet(X12,X11),X10)]. % 3.24/3.63 [161=demod(113),[159], % 3.24/3.63 join(meet(X10,X11),meet(X10,join(X12,X11))) = meet(X10,join(X12,X11))]. % 3.24/3.63 [176=param(21,56),[], % 3.24/3.63 meet(X11,meet(X10,join(X12,join(X13,join(X11,X14))))) = meet(X10,X11)]. % 3.24/3.63 [183=param(34,140),[4,19], % 3.24/3.63 join(X10,meet(X11,join(meet(X10,X11),meet(X12,X10)))) = X10]. % 3.24/3.63 [193=param(16,159),[30], % 3.24/3.63 join(X10,meet(X11,X12)) = join(X10,meet(X12,X11))]. % 3.24/3.63 [235=param(119,6),[], % 3.24/3.63 meet(join(X10,X11),X12) = meet(join(X11,X10),X12)]. % 3.24/3.63 [237=param(24,119),[75], % 3.24/3.63 meet(X10,join(X11,X12)) = meet(X10,join(X12,X11))]. % 3.24/3.63 [316=param(33,183),[3,6,117], % 3.24/3.63 meet(X11,join(meet(X10,X11),meet(X12,X10))) = meet(X10,X11)]. % 3.24/3.63 [325=param(316,159),[], % 3.24/3.63 meet(X10,join(meet(X11,X12),meet(X11,X10))) = meet(X11,X10)]. % 3.24/3.63 [328=param(325,20),[], % 3.24/3.63 meet(X10,join(meet(X11,meet(X12,X13)),meet(X13,X10))) = meet(X13,X10)]. % 3.24/3.63 [332=param(325,193),[], % 3.24/3.63 meet(X10,join(meet(X11,X12),meet(X10,X11))) = meet(X11,X10)]. % 3.24/3.63 [366=param(161,6),[], % 3.24/3.63 join(meet(X10,X11),meet(X11,join(X12,X10))) = meet(X11,join(X12,X10))]. % 3.24/3.63 [388=param(26,332),[39], % 3.24/3.63 meet(X10,join(meet(X11,X12),meet(X10,X11))) = meet(X10,X11)]. % 3.24/3.63 [394=param(388,159),[], % 3.24/3.63 meet(X10,join(meet(X10,X11),meet(X12,X11))) = meet(X10,X11)]. % 3.24/3.63 [403=param(394,33),[4], % 3.24/3.63 meet(X10,join(X11,meet(X10,join(X12,X11)))) = meet(X10,join(X12,X11))]. % 3.24/3.63 [801=param(366,9),[], % 3.24/3.63 join(X10,meet(join(X10,X11),join(X12,X10))) = meet(join(X10,X11),join(X12,X10))]. % 3.24/3.63 [802=param(366,33),[], % 3.24/3.63 join(X10,meet(join(X11,X10),join(X12,X10))) = meet(join(X11,X10),join(X12,X10))]. % 3.24/3.63 [944=param(27,801),[], % 3.24/3.63 join(X10,meet(join(X11,X12),join(X10,X11))) = join(X10,X11)]. % 3.24/3.63 [980=param(944,159),[4], % 3.24/3.63 join(X10,meet(join(X10,X11),join(X11,X12))) = join(X10,X11)]. % 3.24/3.63 [994=param(980,235),[], % 3.24/3.63 join(X10,meet(join(X11,X10),join(X11,X12))) = join(X10,X11)]. % 3.24/3.63 [1131=param(328,33),[], % 3.24/3.63 meet(X10,join(meet(X11,X12),meet(join(X13,X12),X10))) = meet(join(X13,X12),X10)]. % 3.24/3.63 [1181=param(994,1131),[], % 3.24/3.63 join(X10,meet(join(X11,X12),join(meet(X13,X12),X10))) = join(X10,meet(X13,X12))]. % 3.24/3.63 [1185=param(1181,235),[], % 3.24/3.63 join(X10,meet(join(X11,X12),join(meet(X13,X11),X10))) = join(X10,meet(X13,X11))]. % 3.24/3.63 [1187=param(1185,237),[], % 3.24/3.63 join(X10,meet(join(X11,X12),join(X10,meet(X13,X11)))) = join(X10,meet(X13,X11))]. % 3.24/3.63 [1188=param(1187,7),[72], % 3.24/3.63 join(X10,meet(X11,X12)) = join(X10,meet(join(X12,X10),X11))]. % 3.24/3.63 [1192=param(1188,6),[], % 3.24/3.63 join(X10,meet(join(X11,X10),X12)) = join(X10,meet(X11,X12))]. % 3.24/3.63 [1195=demod(802),[1192], % 3.24/3.63 meet(join(X11,X10),join(X12,X10)) = join(X10,meet(X11,join(X12,X10)))]. % 3.24/3.63 [1222=param(1192,100),[176], % 3.24/3.63 join(X10,meet(X11,join(X12,X10))) = join(X10,meet(X11,X12))]. % 3.24/3.63 [1225=demod(1195),[1222], % 3.24/3.63 meet(join(X10,X11),join(X12,X11)) = join(X11,meet(X10,X12))]. % 3.24/3.63 [1228=demod(403),[1222], % 3.24/3.63 meet(X10,join(X11,meet(X10,X12))) = meet(X10,join(X12,X11))]. % 3.24/3.63 [1247=param(1225,8),[], % 3.24/3.63 meet(X10,join(X11,meet(X10,X12))) = join(meet(X10,X12),meet(X10,X11))]. % 3.24/3.63 [1248=demod(1228),[1247], % 3.24/3.63 meet(X10,join(X11,X12)) = join(meet(X10,X11),meet(X10,X12))]. % 3.24/3.63 [1281=demod(115),[1248,1248,20,38,20,24], % 3.24/3.63 meet(join(X12,X10),X11) = join(meet(X10,X11),meet(X12,X11))]. % 3.24/3.63 [1317=param(13,1281),[1248,6,11,4,19,1248,65,12], % 3.24/3.63 thmtrue = thmfalse]. % 3.24/3.63 % SZS output end CNFRefutation % 3.24/3.63 Space: 9633 KB %------------------------------------------------------------------------------