%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LAT022-1 : TPTP v8.1.0. Released v2.2.0. % 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 : Sun Jul 17 04:55:27 EDT 2022 % Result : Unsatisfiable 7.52s 7.91s % Output : CNFRefutation 7.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.10 % Problem : LAT022-1 : TPTP v8.1.0. Released v2.2.0. % 0.08/0.10 % Command : fiesta-wrapper %s % 0.10/0.29 % Computer : n032.cluster.edu % 0.10/0.29 % Model : x86_64 x86_64 % 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.29 % Memory : 8042.1875MB % 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.29 % CPULimit : 300 % 0.10/0.29 % WCLimit : 600 % 0.10/0.29 % DateTime : Wed Jun 29 00:02:42 EDT 2022 % 0.10/0.29 % CPUTime : % 7.52/7.91 Theorem Proved. % 7.52/7.91 % SZS status Unsatisfiable % 7.52/7.91 % SZS output start CNFRefutation % 7.52/7.91 [1=axiom,[], % 7.52/7.91 join(meet(X10,X11),meet(X12,join(X10,X11))) = meet(join(X10,X11),join(X12,meet(X10,X11)))]. % 7.52/7.91 [2=axiom,[], % 7.52/7.91 meet(join(X10,meet(X11,X12)),join(X10,X11)) = join(X10,meet(X11,X12))]. % 7.52/7.91 [3=axiom,[], % 7.52/7.91 join(meet(X10,join(X11,X12)),meet(X10,X11)) = meet(X10,join(X11,X12))]. % 7.52/7.91 [4=axiom,[], % 7.52/7.91 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 7.52/7.91 [5=axiom,[], % 7.52/7.91 meet(meet(X10,X11),X12) = meet(X10,meet(X11,X12))]. % 7.52/7.91 [6=axiom,[], % 7.52/7.91 join(X10,X11) = join(X11,X10)]. % 7.52/7.91 [7=demod(3),[6], % 7.52/7.91 join(meet(X10,X11),meet(X10,join(X11,X12))) = meet(X10,join(X11,X12))]. % 7.52/7.91 [8=axiom,[], % 7.52/7.91 meet(X10,X11) = meet(X11,X10)]. % 7.52/7.91 [9=demod(2),[8], % 7.52/7.91 meet(join(X10,X11),join(X10,meet(X11,X12))) = join(X10,meet(X11,X12))]. % 7.52/7.91 [10=axiom,[], % 7.52/7.91 join(X10,X10) = X10]. % 7.52/7.91 [11=axiom,[], % 7.52/7.91 meet(X10,X10) = X10]. % 7.52/7.91 [12=axiom,[], % 7.52/7.91 thtop(X10,X10) = thmfalse]. % 7.52/7.91 [13=axiom,[8,8,8,6], % 7.52/7.91 thtop(meet(a,join(b,meet(c,a))),join(meet(c,a),meet(b,a))) = thmtrue]. % 7.52/7.91 [14=param(1,10),[11,10,11], % 7.52/7.91 join(X10,meet(X11,X10)) = meet(X10,join(X11,X10))]. % 7.52/7.91 [15=param(5,8),[], % 7.52/7.91 meet(X10,meet(X11,X12)) = meet(X12,meet(X10,X11))]. % 7.52/7.91 [16=param(5,8),[5], % 7.52/7.91 meet(X10,meet(X11,X12)) = meet(X11,meet(X10,X12))]. % 7.52/7.91 [18=param(5,11),[], % 7.52/7.91 meet(X10,meet(X10,X11)) = meet(X10,X11)]. % 7.52/7.91 [19=param(4,6),[], % 7.52/7.91 join(X10,join(X11,X12)) = join(X12,join(X10,X11))]. % 7.52/7.91 [20=param(4,6),[4], % 7.52/7.91 join(X10,join(X11,X12)) = join(X11,join(X10,X12))]. % 7.52/7.91 [22=param(4,10),[], % 7.52/7.91 join(X10,join(X10,X11)) = join(X10,X11)]. % 7.52/7.91 [24=param(22,6),[4], % 7.52/7.91 join(X10,join(X11,X10)) = join(X10,X11)]. % 7.52/7.91 [26=param(24,4),[], % 7.52/7.91 join(X10,join(X11,join(X12,X10))) = join(X10,join(X11,X12))]. % 7.52/7.91 [27=param(4,24),[4,4], % 7.52/7.91 join(X10,join(X11,join(X10,X12))) = join(X10,join(X11,X12))]. % 7.52/7.91 [29=param(7,8),[], % 7.52/7.91 join(meet(X10,X11),meet(X11,join(X10,X12))) = meet(X11,join(X10,X12))]. % 7.52/7.91 [32=param(7,11),[8,6,4,11], % 7.52/7.91 join(X10,join(X11,meet(X10,join(X10,X11)))) = join(X10,X11)]. % 7.52/7.91 [34=param(18,8),[5], % 7.52/7.91 meet(X10,meet(X11,X10)) = meet(X10,X11)]. % 7.52/7.91 [36=param(34,5),[], % 7.52/7.91 meet(X10,meet(X11,meet(X12,X10))) = meet(X10,meet(X11,X12))]. % 7.52/7.91 [37=param(5,34),[5,5], % 7.52/7.91 meet(X10,meet(X11,meet(X10,X12))) = meet(X10,meet(X11,X12))]. % 7.52/7.91 [38=param(9,6),[], % 7.52/7.91 meet(join(X10,X11),join(X11,meet(X10,X12))) = join(X11,meet(X10,X12))]. % 7.52/7.91 [39=param(9,6),[], % 7.52/7.91 meet(join(X10,X11),join(meet(X11,X12),X10)) = join(X10,meet(X11,X12))]. % 7.52/7.91 [47=param(14,8),[], % 7.52/7.91 meet(X10,join(X11,X10)) = join(X10,meet(X10,X11))]. % 7.52/7.91 [49=demod(14),[47], % 7.52/7.91 join(X10,meet(X11,X10)) = join(X10,meet(X10,X11))]. % 7.52/7.91 [51=param(47,4),[], % 7.52/7.91 meet(X10,join(X11,join(X12,X10))) = join(X10,meet(X10,join(X11,X12)))]. % 7.52/7.91 [52=param(5,47),[], % 7.52/7.91 meet(join(X10,meet(X10,X11)),X12) = meet(X10,meet(join(X11,X10),X12))]. % 7.52/7.91 [53=param(47,6),[], % 7.52/7.91 meet(X10,join(X10,X11)) = join(X10,meet(X10,X11))]. % 7.52/7.91 [54=demod(32),[53,27], % 7.52/7.91 join(X10,join(X11,meet(X10,X11))) = join(X10,X11)]. % 7.52/7.91 [55=param(47,24),[8,47,4,22], % 7.52/7.91 meet(join(X10,X11),join(X11,X10)) = join(X10,join(X11,meet(X11,X10)))]. % 7.52/7.91 [64=param(15,53),[15], % 7.52/7.91 meet(X10,join(X11,meet(X11,X12))) = meet(X11,meet(join(X11,X12),X10))]. % 7.52/7.91 [67=param(54,6),[4,6], % 7.52/7.91 join(X11,join(X10,meet(X10,X11))) = join(X10,X11)]. % 7.52/7.91 [68=demod(55),[67], % 7.52/7.91 meet(join(X10,X11),join(X11,X10)) = join(X11,X10)]. % 7.52/7.91 [74=param(16,47),[], % 7.52/7.91 meet(X10,join(X11,meet(X11,X12))) = meet(X11,meet(X10,join(X12,X11)))]. % 7.52/7.91 [76=param(16,68),[], % 7.52/7.91 meet(join(X12,X11),meet(X10,join(X11,X12))) = meet(X10,join(X11,X12))]. % 7.52/7.91 [79=param(7,67),[67], % 7.52/7.91 join(meet(X10,X11),meet(X10,join(X12,X11))) = meet(X10,join(X12,X11))]. % 7.52/7.91 [90=param(36,68),[34,76], % 7.52/7.91 meet(join(X10,X11),X12) = meet(X12,join(X11,X10))]. % 7.52/7.91 [102=param(16,90),[], % 7.52/7.91 meet(X10,meet(X11,join(X12,X13))) = meet(join(X13,X12),meet(X10,X11))]. % 7.52/7.91 [114=param(29,9),[53,4,27,9], % 7.52/7.91 join(X10,join(meet(X10,X11),meet(X11,X12))) = join(X10,meet(X11,X12))]. % 7.52/7.91 [115=param(29,10),[10], % 7.52/7.91 join(meet(X10,X11),meet(X11,X10)) = meet(X11,X10)]. % 7.52/7.91 [121=param(19,115),[], % 7.52/7.91 join(X10,meet(X11,X12)) = join(meet(X11,X12),join(X10,meet(X12,X11)))]. % 7.52/7.91 [122=param(20,115),[], % 7.52/7.91 join(meet(X12,X11),join(X10,meet(X11,X12))) = join(X10,meet(X11,X12))]. % 7.52/7.91 [123=demod(121),[122], % 7.52/7.91 join(X10,meet(X11,X12)) = join(X10,meet(X12,X11))]. % 7.52/7.91 [124=param(26,115),[24,122], % 7.52/7.91 join(meet(X10,X11),X12) = join(X12,meet(X11,X10))]. % 7.52/7.91 [159=param(90,123),[], % 7.52/7.91 meet(X10,join(X11,meet(X12,X13))) = meet(join(meet(X13,X12),X11),X10)]. % 7.52/7.91 [161=param(38,7),[52,37,7], % 7.52/7.91 meet(X10,meet(join(X11,X10),join(X11,X12))) = meet(X10,join(X11,X12))]. % 7.52/7.91 [162=param(38,8),[], % 7.52/7.91 meet(join(X10,X11),join(X11,meet(X12,X10))) = join(X11,meet(X10,X12))]. % 7.52/7.91 [163=param(38,124),[], % 7.52/7.91 meet(join(X10,X11),join(meet(X12,X10),X11)) = join(X11,meet(X10,X12))]. % 7.52/7.91 [178=param(39,115),[6,90,6,5,53,34,115], % 7.52/7.91 meet(X10,join(X11,meet(X11,X10))) = meet(X11,X10)]. % 7.52/7.91 [179=param(5,178),[5,52], % 7.52/7.91 meet(X11,meet(X10,meet(join(X11,X10),X12))) = meet(X10,meet(X11,X12))]. % 7.52/7.91 [183=param(178,178),[52,9,178], % 7.52/7.91 meet(X10,join(X11,meet(X10,X11))) = meet(X10,X11)]. % 7.52/7.91 [228=param(179,15),[5], % 7.52/7.91 meet(join(X11,X10),meet(X12,meet(X11,X10))) = meet(X10,meet(X11,X12))]. % 7.52/7.91 [231=param(36,179),[5,36,5,228], % 7.52/7.91 meet(join(X10,X11),meet(X12,meet(X11,X10))) = meet(X11,meet(X10,X12))]. % 7.52/7.91 [233=param(231,15),[], % 7.52/7.91 meet(join(X10,X11),meet(X10,meet(X12,X11))) = meet(X11,meet(X10,X12))]. % 7.52/7.91 [234=param(231,16),[], % 7.52/7.91 meet(join(X10,X11),meet(X11,meet(X12,X10))) = meet(X11,meet(X10,X12))]. % 7.52/7.91 [247=param(74,8),[], % 7.52/7.91 meet(X10,join(X11,meet(X12,X11))) = meet(X11,meet(X10,join(X12,X11)))]. % 7.52/7.91 [254=param(36,161),[34,47], % 7.52/7.91 meet(join(X10,X11),join(X12,meet(X12,X10))) = meet(join(X10,X11),X12)]. % 7.52/7.91 [268=param(254,67),[67], % 7.52/7.91 meet(join(X10,X11),join(X12,meet(X12,X11))) = meet(join(X10,X11),X12)]. % 7.52/7.91 [273=param(64,268),[52,254], % 7.52/7.91 meet(X10,meet(join(X10,X11),X12)) = meet(X12,meet(join(X11,X12),X10))]. % 7.52/7.91 [284=param(26,114),[24], % 7.52/7.91 join(meet(X10,X11),join(X12,meet(X12,X10))) = join(meet(X10,X11),X12)]. % 7.52/7.91 [285=param(114,124),[], % 7.52/7.91 join(X10,join(meet(X11,X12),meet(X11,X10))) = join(X10,meet(X11,X12))]. % 7.52/7.91 [287=param(114,178),[178], % 7.52/7.91 join(X10,join(meet(X10,X11),meet(X12,X11))) = join(X10,meet(X12,X11))]. % 7.52/7.91 [292=param(26,287),[24], % 7.52/7.91 join(meet(X10,X11),join(X12,meet(X12,X11))) = join(meet(X10,X11),X12)]. % 7.52/7.91 [293=param(287,124),[], % 7.52/7.91 join(X10,join(meet(X11,X12),meet(X12,X10))) = join(X10,meet(X11,X12))]. % 7.52/7.91 [295=param(293,19),[], % 7.52/7.91 join(meet(X12,X10),join(X10,meet(X11,X12))) = join(X10,meet(X11,X12))]. % 7.52/7.91 [310=param(233,273),[234,53], % 7.52/7.91 meet(X10,meet(X11,join(X12,X10))) = meet(X10,join(X11,meet(X11,X12)))]. % 7.52/7.91 [311=demod(247),[310], % 7.52/7.91 meet(X10,join(X11,meet(X12,X11))) = meet(X11,join(X10,meet(X10,X12)))]. % 7.52/7.91 [313=param(234,273),[233,47], % 7.52/7.91 meet(X10,meet(X11,join(X10,X12))) = meet(X10,join(X11,meet(X11,X12)))]. % 7.52/7.91 [318=param(313,102),[], % 7.52/7.91 meet(X10,join(X11,meet(X11,X12))) = meet(join(X12,X10),meet(X10,X11))]. % 7.52/7.91 [319=param(318,8),[], % 7.52/7.91 meet(join(X12,X10),meet(X10,X11)) = meet(X10,join(X11,meet(X12,X11)))]. % 7.52/7.91 [321=param(319,8),[15], % 7.52/7.91 meet(X10,meet(join(X11,X10),X12)) = meet(X10,join(X12,meet(X11,X12)))]. % 7.52/7.91 [325=demod(52),[321], % 7.52/7.91 meet(join(X10,meet(X10,X11)),X12) = meet(X10,join(X12,meet(X11,X12)))]. % 7.52/7.91 [326=param(183,4),[], % 7.52/7.91 meet(X10,join(X11,join(X12,meet(X10,join(X11,X12))))) = meet(X10,join(X11,X12))]. % 7.52/7.91 [398=param(313,39),[5,90,47,4,67,22,5,310], % 7.52/7.91 meet(X10,meet(X11,join(X12,meet(X10,X11)))) = meet(X10,join(X11,meet(X11,X12)))]. % 7.52/7.91 [409=param(51,295),[5,398,6,5,183], % 7.52/7.91 meet(X10,join(X11,meet(X11,X12))) = join(meet(X10,X11),meet(X10,meet(X11,X12)))]. % 7.52/7.91 [411=demod(311),[409], % 7.52/7.91 meet(X10,join(X11,meet(X12,X11))) = join(meet(X11,X10),meet(X11,meet(X10,X12)))]. % 7.52/7.91 [424=param(285,7),[4,4], % 7.52/7.91 join(X10,join(X11,meet(X12,join(X10,X11)))) = join(X10,join(X11,meet(X12,X10)))]. % 7.52/7.91 [425=demod(326),[424], % 7.52/7.91 meet(X10,join(X11,join(X12,meet(X10,X11)))) = meet(X10,join(X11,X12))]. % 7.52/7.91 [432=param(425,124),[], % 7.52/7.91 meet(X10,join(X11,join(meet(X11,X10),X12))) = meet(X10,join(X11,X12))]. % 7.52/7.91 [437=param(432,292),[432], % 7.52/7.91 meet(X10,join(X11,join(X12,meet(X12,X10)))) = meet(X10,join(X11,X12))]. % 7.52/7.91 [455=param(163,49),[325,4,424,285], % 7.52/7.91 meet(X10,join(meet(X11,X10),meet(X12,X10))) = join(meet(X12,X10),meet(X10,X11))]. % 7.52/7.91 [650=param(411,124),[5,-124], % 7.52/7.91 meet(X10,join(X11,meet(X12,X11))) = join(meet(X10,X11),meet(X10,meet(X12,X11)))]. % 7.52/7.91 [688=param(1,8),[], % 7.52/7.91 meet(join(X10,X11),join(X12,meet(X10,X11))) = join(meet(X10,X11),meet(join(X10,X11),X12))]. % 7.52/7.91 [942=param(437,53),[22], % 7.52/7.91 meet(join(X10,X11),join(X12,join(X10,meet(X10,X11)))) = meet(join(X10,X11),join(X12,X10))]. % 7.52/7.91 [950=param(79,34),[], % 7.52/7.91 join(meet(X10,X11),meet(X10,join(X12,meet(X11,X10)))) = meet(X10,join(X12,meet(X11,X10)))]. % 7.52/7.91 [1286=param(284,53),[22,6,4,6], % 7.52/7.91 join(X10,join(meet(X10,X11),meet(join(X10,X11),X12))) = join(X10,meet(join(X10,X11),X12))]. % 7.52/7.91 [2051=param(688,22),[53,942,53,22,4,1286], % 7.52/7.91 meet(join(X10,X11),join(X12,X10)) = join(X10,meet(join(X10,X11),X12))]. % 7.52/7.91 [2074=param(34,2051),[162], % 7.52/7.91 meet(join(X11,X10),join(X10,X12)) = join(X10,meet(X11,join(X10,X12)))]. % 7.52/7.91 [2080=param(2051,67),[67], % 7.52/7.91 meet(join(X10,X11),join(X12,X11)) = join(X11,meet(join(X10,X11),X12))]. % 7.52/7.91 [2113=param(2080,6),[2074], % 7.52/7.91 join(X10,meet(join(X11,X10),X12)) = join(X10,meet(X11,join(X10,X12)))]. % 7.52/7.91 [2120=demod(2080),[2113], % 7.52/7.91 meet(join(X10,X11),join(X12,X11)) = join(X11,meet(X10,join(X11,X12)))]. % 7.52/7.91 [2128=param(2120,6),[2051], % 7.52/7.91 join(X10,meet(join(X10,X11),X12)) = join(X10,meet(X11,join(X10,X12)))]. % 7.52/7.91 [2194=param(455,2128),[6,650,285,455,90,6,950], % 7.52/7.91 join(meet(X10,X11),meet(X11,X12)) = meet(X11,join(X10,meet(X12,X11)))]. % 7.52/7.91 [2244=param(13,159),[8,6,90,6,-2194,8,6,12], % 7.52/7.91 thmtrue = thmfalse]. % 7.52/7.91 % SZS output end CNFRefutation % 7.52/7.91 Space: 22064 KB %------------------------------------------------------------------------------