%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LAT020-1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n029.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:26 EDT 2022 % Result : Unsatisfiable 75.94s 76.44s % Output : CNFRefutation 75.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : LAT020-1 : TPTP v8.1.0. Released v2.2.0. % 0.00/0.09 % Command : fiesta-wrapper %s % 0.08/0.29 % Computer : n029.cluster.edu % 0.08/0.29 % Model : x86_64 x86_64 % 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.29 % Memory : 8042.1875MB % 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.29 % CPULimit : 300 % 0.08/0.29 % WCLimit : 600 % 0.08/0.29 % DateTime : Thu Jun 30 13:27:38 EDT 2022 % 0.08/0.29 % CPUTime : % 75.94/76.44 Theorem Proved. % 75.94/76.44 % SZS status Unsatisfiable % 75.94/76.44 % SZS output start CNFRefutation % 75.94/76.44 [1=axiom,[], % 75.94/76.44 meet(join(meet(join(X10,X11),X12),X11),join(X12,X10)) = join(meet(join(meet(X10,X11),X12),X11),meet(X12,X10))]. % 75.94/76.44 [2=axiom,[], % 75.94/76.44 meet(join(X10,meet(X11,X12)),join(X10,X11)) = join(X10,meet(X11,X12))]. % 75.94/76.44 [3=axiom,[], % 75.94/76.44 join(meet(X10,join(X11,X12)),meet(X10,X11)) = meet(X10,join(X11,X12))]. % 75.94/76.44 [4=axiom,[], % 75.94/76.44 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 75.94/76.44 [5=axiom,[], % 75.94/76.44 meet(meet(X10,X11),X12) = meet(X10,meet(X11,X12))]. % 75.94/76.44 [6=axiom,[], % 75.94/76.44 join(X10,X11) = join(X11,X10)]. % 75.94/76.44 [7=demod(1),[6,6], % 75.94/76.44 meet(join(X10,meet(join(X11,X10),X12)),join(X12,X11)) = join(meet(X12,X11),meet(join(meet(X11,X10),X12),X10))]. % 75.94/76.44 [8=demod(3),[6], % 75.94/76.44 join(meet(X10,X11),meet(X10,join(X11,X12))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [9=axiom,[], % 75.94/76.44 meet(X10,X11) = meet(X11,X10)]. % 75.94/76.44 [10=demod(2),[9], % 75.94/76.44 meet(join(X10,X11),join(X10,meet(X11,X12))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [11=demod(7),[9,9], % 75.94/76.44 meet(join(X10,X11),join(X12,meet(join(X11,X12),X10))) = join(meet(X10,X11),meet(X12,join(meet(X11,X12),X10)))]. % 75.94/76.44 [12=axiom,[], % 75.94/76.44 join(X10,X10) = X10]. % 75.94/76.44 [13=axiom,[], % 75.94/76.44 meet(X10,X10) = X10]. % 75.94/76.44 [14=axiom,[], % 75.94/76.44 thtop(X10,X10) = thmfalse]. % 75.94/76.44 [15=axiom,[6,9,9,6], % 75.94/76.44 thtop(meet(a,join(c,b)),join(meet(c,a),meet(b,a))) = thmtrue]. % 75.94/76.44 [17=param(4,12),[], % 75.94/76.44 join(X10,join(X10,X11)) = join(X10,X11)]. % 75.94/76.44 [18=param(6,4),[], % 75.94/76.44 join(X10,join(X11,X12)) = join(X11,join(X12,X10))]. % 75.94/76.44 [19=param(4,6),[4], % 75.94/76.44 join(X10,join(X11,X12)) = join(X11,join(X10,X12))]. % 75.94/76.44 [21=param(17,6),[4], % 75.94/76.44 join(X10,join(X11,X10)) = join(X10,X11)]. % 75.94/76.44 [22=param(5,9),[], % 75.94/76.44 meet(X10,meet(X11,X12)) = meet(X12,meet(X10,X11))]. % 75.94/76.44 [23=param(5,9),[5], % 75.94/76.44 meet(X10,meet(X11,X12)) = meet(X11,meet(X10,X12))]. % 75.94/76.44 [25=param(5,13),[], % 75.94/76.44 meet(X10,meet(X10,X11)) = meet(X10,X11)]. % 75.94/76.44 [27=param(25,9),[5], % 75.94/76.44 meet(X10,meet(X11,X10)) = meet(X10,X11)]. % 75.94/76.44 [29=param(27,5),[], % 75.94/76.44 meet(X10,meet(X11,meet(X12,X10))) = meet(X10,meet(X11,X12))]. % 75.94/76.44 [30=param(5,27),[5,5], % 75.94/76.44 meet(X10,meet(X11,meet(X10,X12))) = meet(X10,meet(X11,X12))]. % 75.94/76.44 [31=param(8,6),[], % 75.94/76.44 join(meet(X10,X11),meet(X10,join(X12,X11))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [32=param(8,9),[], % 75.94/76.44 join(meet(X10,X11),meet(X11,join(X10,X12))) = meet(X11,join(X10,X12))]. % 75.94/76.44 [34=param(8,13),[], % 75.94/76.44 join(X10,meet(X10,join(X10,X11))) = meet(X10,join(X10,X11))]. % 75.94/76.44 [35=param(8,13),[9,6,4,13], % 75.94/76.44 join(X10,join(X11,meet(X10,join(X10,X11)))) = join(X10,X11)]. % 75.94/76.44 [37=param(21,4),[], % 75.94/76.44 join(X10,join(X11,join(X12,X10))) = join(X10,join(X11,X12))]. % 75.94/76.44 [38=param(4,21),[4,4], % 75.94/76.44 join(X10,join(X11,join(X10,X12))) = join(X10,join(X11,X12))]. % 75.94/76.44 [39=param(38,6),[4,17], % 75.94/76.44 join(X10,join(X11,X12)) = join(X10,join(X12,X11))]. % 75.94/76.44 [40=param(10,6),[], % 75.94/76.44 meet(join(X10,X11),join(X11,meet(X10,X12))) = join(X11,meet(X10,X12))]. % 75.94/76.44 [41=param(10,6),[], % 75.94/76.44 meet(join(X10,X11),join(meet(X11,X12),X10)) = join(X10,meet(X11,X12))]. % 75.94/76.44 [42=param(10,9),[], % 75.94/76.44 meet(join(X10,X11),join(X10,meet(X12,X11))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [43=param(10,12),[], % 75.94/76.44 meet(X10,join(X10,meet(X10,X11))) = join(X10,meet(X10,X11))]. % 75.94/76.44 [44=param(10,12),[6,9,5,12], % 75.94/76.44 meet(X10,meet(X11,join(X10,meet(X10,X11)))) = meet(X10,X11)]. % 75.94/76.44 [48=param(18,4),[], % 75.94/76.44 join(X10,join(X11,join(X12,X13))) = join(X12,join(X13,join(X10,X11)))]. % 75.94/76.44 [55=param(19,18),[], % 75.94/76.44 join(X10,join(X11,join(X12,X13))) = join(X12,join(X10,join(X13,X11)))]. % 75.94/76.44 [76=param(8,39),[8], % 75.94/76.44 meet(X10,join(X11,join(X12,X13))) = meet(X10,join(X11,join(X13,X12)))]. % 75.94/76.44 [83=param(44,9),[5,9,43], % 75.94/76.44 meet(X11,join(X10,meet(X10,X11))) = meet(X10,X11)]. % 75.94/76.44 [85=param(8,83),[83], % 75.94/76.44 join(meet(X10,X11),meet(X11,X10)) = meet(X11,X10)]. % 75.94/76.44 [86=param(83,9),[], % 75.94/76.44 meet(X10,join(X11,meet(X10,X11))) = meet(X11,X10)]. % 75.94/76.44 [92=param(31,9),[], % 75.94/76.44 join(meet(X10,X11),meet(join(X12,X11),X10)) = meet(X10,join(X11,X12))]. % 75.94/76.44 [93=param(31,6),[], % 75.94/76.44 join(meet(X10,X12),meet(X10,join(X11,X12))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [94=demod(31),[93], % 75.94/76.44 meet(X10,join(X11,X12)) = meet(X10,join(X12,X11))]. % 75.94/76.44 [96=param(18,85),[], % 75.94/76.44 join(X10,meet(X11,X12)) = join(meet(X11,X12),join(X10,meet(X12,X11)))]. % 75.94/76.44 [97=param(19,85),[], % 75.94/76.44 join(meet(X12,X11),join(X10,meet(X11,X12))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [98=param(37,85),[21,97], % 75.94/76.44 join(meet(X10,X11),X12) = join(X12,meet(X11,X10))]. % 75.94/76.44 [110=param(10,98),[], % 75.94/76.44 meet(join(X10,X11),join(meet(X12,X11),X10)) = join(X10,meet(X11,X12))]. % 75.94/76.44 [123=param(94,9),[], % 75.94/76.44 meet(X10,join(X11,X12)) = meet(join(X12,X11),X10)]. % 75.94/76.44 [128=param(27,94),[], % 75.94/76.44 meet(join(X10,X11),meet(X12,join(X11,X10))) = meet(join(X10,X11),X12)]. % 75.94/76.44 [142=param(123,9),[], % 75.94/76.44 meet(join(X10,X11),X12) = meet(join(X11,X10),X12)]. % 75.94/76.44 [159=param(35,6),[4,6,34], % 75.94/76.44 join(X11,meet(X10,join(X10,X11))) = join(X10,X11)]. % 75.94/76.44 [161=param(159,6),[], % 75.94/76.44 join(X10,meet(X11,join(X10,X11))) = join(X11,X10)]. % 75.94/76.44 [163=param(19,159),[], % 75.94/76.44 join(X12,join(X10,meet(X11,join(X11,X12)))) = join(X10,join(X11,X12))]. % 75.94/76.44 [164=param(32,159),[159], % 75.94/76.44 join(meet(X10,X11),meet(X11,join(X12,X10))) = meet(X11,join(X12,X10))]. % 75.94/76.44 [174=param(159,161),[161], % 75.94/76.44 join(meet(X10,join(X11,X10)),meet(X11,join(X10,X11))) = join(X10,X11)]. % 75.94/76.44 [175=param(40,6),[], % 75.94/76.44 meet(join(X10,X11),join(meet(X10,X12),X11)) = join(X11,meet(X10,X12))]. % 75.94/76.44 [176=param(40,9),[], % 75.94/76.44 meet(join(X10,X11),join(X11,meet(X12,X10))) = join(X11,meet(X10,X12))]. % 75.94/76.44 [177=param(40,98),[], % 75.94/76.44 meet(join(X10,X11),join(meet(X12,X10),X11)) = join(X11,meet(X10,X12))]. % 75.94/76.44 [192=param(25,86),[27], % 75.94/76.44 meet(X10,join(X11,meet(X10,X11))) = meet(X10,X11)]. % 75.94/76.44 [193=param(23,192),[], % 75.94/76.44 meet(X11,meet(X10,join(X12,meet(X11,X12)))) = meet(X10,meet(X11,X12))]. % 75.94/76.44 [196=param(193,10),[192,22,9], % 75.94/76.44 meet(X11,meet(X10,join(X11,X10))) = meet(X10,X11)]. % 75.94/76.44 [202=param(5,196),[5,5], % 75.94/76.44 meet(X11,meet(X10,meet(join(X11,X10),X12))) = meet(X10,meet(X11,X12))]. % 75.94/76.44 [208=param(202,22),[5], % 75.94/76.44 meet(join(X11,X10),meet(X12,meet(X11,X10))) = meet(X10,meet(X11,X12))]. % 75.94/76.44 [211=param(29,202),[5,29,5,208], % 75.94/76.44 meet(join(X10,X11),meet(X12,meet(X11,X10))) = meet(X11,meet(X10,X12))]. % 75.94/76.44 [213=param(211,22),[], % 75.94/76.44 meet(join(X10,X11),meet(X10,meet(X12,X11))) = meet(X11,meet(X10,X12))]. % 75.94/76.44 [214=param(211,23),[], % 75.94/76.44 meet(join(X10,X11),meet(X11,meet(X12,X10))) = meet(X11,meet(X10,X12))]. % 75.94/76.44 [224=param(176,11),[12,13,164], % 75.94/76.44 join(X10,meet(X11,X10)) = meet(X10,join(X10,X11))]. % 75.94/76.44 [227=param(224,9),[], % 75.94/76.44 meet(X10,join(X10,X11)) = join(X10,meet(X10,X11))]. % 75.94/76.44 [230=demod(159),[227], % 75.94/76.44 join(X10,join(X11,meet(X11,X10))) = join(X11,X10)]. % 75.94/76.44 [232=demod(163),[227], % 75.94/76.44 join(X10,join(X11,join(X12,meet(X12,X10)))) = join(X11,join(X12,X10))]. % 75.94/76.44 [233=param(5,227),[], % 75.94/76.44 meet(join(X10,meet(X10,X11)),X12) = meet(X10,meet(join(X10,X11),X12))]. % 75.94/76.44 [234=param(227,6),[], % 75.94/76.44 meet(X10,join(X11,X10)) = join(X10,meet(X10,X11))]. % 75.94/76.44 [235=demod(174),[234,234,4,-96], % 75.94/76.44 join(X10,join(X11,meet(X10,X11))) = join(X10,X11)]. % 75.94/76.44 [236=param(227,18),[], % 75.94/76.44 meet(X10,join(X11,join(X12,X10))) = join(X10,meet(X10,join(X11,X12)))]. % 75.94/76.44 [238=param(227,19),[], % 75.94/76.44 meet(X10,join(X11,join(X10,X12))) = join(X10,meet(X10,join(X11,X12)))]. % 75.94/76.44 [245=param(4,235),[4,4], % 75.94/76.44 join(X10,join(X11,join(meet(X10,X11),X12))) = join(X10,join(X11,X12))]. % 75.94/76.44 [248=param(37,235),[4,48,245,38,4], % 75.94/76.44 join(X10,join(meet(X11,X10),join(X12,X11))) = join(X10,join(X11,X12))]. % 75.94/76.44 [254=param(233,9),[], % 75.94/76.44 meet(join(X10,meet(X11,X10)),X12) = meet(X10,meet(join(X10,X11),X12))]. % 75.94/76.44 [255=param(254,9),[], % 75.94/76.44 meet(X10,meet(join(X10,X11),X12)) = meet(X12,join(X10,meet(X11,X10)))]. % 75.94/76.44 [262=param(248,55),[], % 75.94/76.44 join(meet(X11,X10),join(X11,join(X10,X12))) = join(X10,join(X11,X12))]. % 75.94/76.44 [266=param(164,41),[227,4,38,41], % 75.94/76.44 join(X10,join(meet(X10,X11),meet(X11,X12))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [276=param(266,98),[], % 75.94/76.44 join(X10,join(meet(X11,X12),meet(X11,X10))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [280=param(38,276),[21], % 75.94/76.44 join(meet(X10,X11),join(X12,meet(X10,X12))) = join(meet(X10,X11),X12)]. % 75.94/76.44 [288=param(280,83),[83], % 75.94/76.44 join(meet(X10,X11),join(X12,meet(X11,X12))) = join(meet(X10,X11),X12)]. % 75.94/76.44 [294=param(288,18),[], % 75.94/76.44 join(meet(X11,X12),join(meet(X10,X11),X12)) = join(meet(X10,X11),X12)]. % 75.94/76.44 [296=param(21,288),[4,294,21,4], % 75.94/76.44 join(X10,join(meet(X12,X10),meet(X11,X12))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [299=param(296,19),[], % 75.94/76.44 join(meet(X12,X10),join(X10,meet(X11,X12))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [300=param(296,98),[], % 75.94/76.44 join(X10,join(meet(X11,X12),meet(X10,X12))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [303=param(42,92),[6,233,30,93], % 75.94/76.44 meet(X10,meet(join(X10,X11),join(X11,X12))) = meet(X10,join(X12,X11))]. % 75.94/76.44 [306=param(92,123),[], % 75.94/76.44 join(meet(X10,X11),meet(join(X12,X11),X10)) = meet(join(X12,X11),X10)]. % 75.94/76.44 [307=param(306,6),[-98], % 75.94/76.44 join(meet(X11,X12),meet(join(X10,X11),X12)) = meet(join(X10,X11),X12)]. % 75.94/76.44 [315=param(29,303),[128,227], % 75.94/76.44 meet(join(X10,X11),join(X12,meet(X12,X10))) = meet(join(X10,X11),X12)]. % 75.94/76.44 [318=param(303,123),[], % 75.94/76.44 meet(X10,meet(join(X11,X12),join(X11,X10))) = meet(X10,join(X12,X11))]. % 75.94/76.44 [322=param(318,142),[], % 75.94/76.44 meet(X10,meet(join(X11,X12),join(X12,X10))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [324=param(30,322),[27,234], % 75.94/76.44 meet(join(X10,X11),join(X12,meet(X12,X11))) = meet(join(X10,X11),X12)]. % 75.94/76.44 [325=param(324,9),[], % 75.94/76.44 meet(join(X10,X11),join(X12,meet(X11,X12))) = meet(join(X10,X11),X12)]. % 75.94/76.44 [341=param(255,324),[233,325], % 75.94/76.44 meet(X10,meet(join(X10,X11),X12)) = meet(X12,meet(join(X12,X11),X10))]. % 75.94/76.44 [347=param(213,341),[214,227], % 75.94/76.44 meet(X10,meet(X11,join(X10,X12))) = meet(X10,join(X11,meet(X11,X12)))]. % 75.94/76.44 [350=param(341,255),[], % 75.94/76.44 meet(X10,meet(join(X10,X11),X12)) = meet(X10,join(X12,meet(X11,X12)))]. % 75.94/76.44 [355=param(350,23),[], % 75.94/76.44 meet(join(X10,X12),meet(X10,X11)) = meet(X10,join(X11,meet(X12,X11)))]. % 75.94/76.44 [359=param(355,6),[], % 75.94/76.44 meet(join(X10,X11),meet(X11,X12)) = meet(X11,join(X12,meet(X10,X12)))]. % 75.94/76.44 [360=param(347,6),[], % 75.94/76.44 meet(X10,meet(X11,join(X12,X10))) = meet(X10,join(X11,meet(X11,X12)))]. % 75.94/76.44 [422=param(8,41),[359,6,4,8,41], % 75.94/76.44 join(X10,meet(X11,join(X12,meet(X10,X12)))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [425=param(360,10),[5,9,227,4,230,17,5,360], % 75.94/76.44 meet(X10,meet(X11,join(X12,meet(X10,X11)))) = meet(X10,join(X11,meet(X11,X12)))]. % 75.94/76.44 [437=param(347,40),[227,355,4,422,238], % 75.94/76.44 join(X10,meet(X10,join(X11,meet(X11,X12)))) = join(X10,meet(X10,meet(X11,X12)))]. % 75.94/76.44 [459=param(300,307),[4,4], % 75.94/76.44 join(X10,join(X11,meet(join(X10,X11),X12))) = join(X10,join(X11,meet(X11,X12)))]. % 75.94/76.44 [462=param(236,299),[5,425,6,5,192], % 75.94/76.44 meet(X10,join(X11,meet(X11,X12))) = join(meet(X10,X11),meet(X10,meet(X11,X12)))]. % 75.94/76.44 [463=demod(437),[462], % 75.94/76.44 join(X10,join(meet(X10,X11),meet(X10,meet(X11,X12)))) = join(X10,meet(X10,meet(X11,X12)))]. % 75.94/76.44 [466=demod(360),[462], % 75.94/76.44 meet(X10,meet(X11,join(X12,X10))) = join(meet(X10,X11),meet(X10,meet(X11,X12)))]. % 75.94/76.44 [468=demod(347),[462], % 75.94/76.44 meet(X10,meet(X11,join(X10,X12))) = join(meet(X10,X11),meet(X10,meet(X11,X12)))]. % 75.94/76.44 [470=demod(315),[462,22,350,6], % 75.94/76.44 join(meet(X10,join(X11,meet(X12,X11))),meet(join(X10,X12),X11)) = meet(join(X10,X12),X11)]. % 75.94/76.44 [481=param(76,234),[4,459], % 75.94/76.44 meet(join(X10,X11),join(X12,join(X11,X10))) = join(X10,join(X11,meet(X11,X12)))]. % 75.94/76.44 [485=param(236,262),[6,462,22,350,6,470,4,459], % 75.94/76.44 meet(join(X10,X11),join(X10,join(X12,X11))) = join(X10,join(X11,meet(X11,X12)))]. % 75.94/76.44 [502=param(175,21),[481,4], % 75.94/76.44 join(X10,join(X11,meet(X11,meet(X10,X12)))) = join(X11,join(X10,meet(X10,X12)))]. % 75.94/76.44 [515=param(502,466),[463,502], % 75.94/76.44 join(X10,join(X11,meet(X11,join(X12,X10)))) = join(X10,join(X11,meet(X11,X12)))]. % 75.94/76.44 [532=param(350,485),[227,462,463,236,4,4,17,515,232,236], % 75.94/76.44 join(X10,meet(X10,meet(X11,X12))) = join(X10,meet(X10,join(X12,X11)))]. % 75.94/76.44 [543=param(42,532),[462,9,227,532,22,9,227,532,462,27,12,4,85,5], % 75.94/76.44 join(X10,meet(join(X11,X12),X10)) = join(X10,meet(X12,meet(X11,X10)))]. % 75.94/76.44 [549=param(192,543),[], % 75.94/76.44 meet(join(X10,X11),join(X12,meet(X11,meet(X10,X12)))) = meet(join(X10,X11),X12)]. % 75.94/76.44 [555=param(543,359),[8,30], % 75.94/76.44 meet(X10,join(X11,meet(X12,X11))) = join(meet(X10,X11),meet(X10,meet(X12,X11)))]. % 75.94/76.44 [565=demod(350),[555], % 75.94/76.44 meet(X10,meet(join(X10,X11),X12)) = join(meet(X10,X12),meet(X10,meet(X11,X12)))]. % 75.94/76.44 [569=demod(359),[555], % 75.94/76.44 meet(join(X10,X11),meet(X11,X12)) = join(meet(X11,X12),meet(X11,meet(X10,X12)))]. % 75.94/76.44 [603=param(468,549),[27,569,25,12,29], % 75.94/76.44 join(meet(X10,join(X11,X12)),meet(X10,meet(X12,X11))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [713=param(4,8),[], % 75.94/76.44 join(meet(X10,X11),join(meet(X10,join(X11,X12)),X13)) = join(meet(X10,join(X11,X12)),X13)]. % 75.94/76.44 [714=param(8,25),[], % 75.94/76.44 join(meet(X10,X11),meet(X10,join(meet(X10,X11),X12))) = meet(X10,join(meet(X10,X11),X12))]. % 75.94/76.44 [716=param(5,10),[], % 75.94/76.44 meet(join(X10,X11),meet(join(X10,meet(X11,X12)),X13)) = meet(join(X10,meet(X11,X12)),X13)]. % 75.94/76.44 [782=param(42,17),[], % 75.94/76.44 meet(join(X10,X11),join(X10,meet(X12,join(X10,X11)))) = join(X10,meet(join(X10,X11),X12))]. % 75.94/76.44 [1131=param(307,41),[6,4,714,41], % 75.94/76.44 join(X10,meet(X11,join(meet(X11,X12),X10))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [1143=param(1131,98),[], % 75.94/76.44 join(X10,meet(X11,join(X10,meet(X12,X11)))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [1582=param(177,8),[9,5,782,-98,8], % 75.94/76.44 meet(X10,join(X11,meet(join(X11,X12),X10))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [1591=param(1582,6),[], % 75.94/76.44 meet(X10,join(X11,meet(join(X12,X11),X10))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [1592=param(1582,9),[], % 75.94/76.44 meet(X10,join(X11,meet(X10,join(X11,X12)))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [1638=param(30,1591),[30], % 75.94/76.44 meet(X10,meet(X11,join(X12,meet(join(X13,X12),X10)))) = meet(X10,meet(X11,join(X12,X13)))]. % 75.94/76.44 [1702=param(22,110),[], % 75.94/76.44 meet(X10,join(X11,meet(X12,X13))) = meet(join(meet(X13,X12),X11),meet(X10,join(X11,X12)))]. % 75.94/76.44 [3223=param(713,19),[], % 75.94/76.44 join(meet(X10,join(X11,X12)),join(meet(X10,X11),X13)) = join(meet(X10,join(X11,X12)),X13)]. % 75.94/76.44 [3249=param(714,1143),[], % 75.94/76.44 meet(X10,join(meet(X10,X11),meet(X12,X10))) = join(meet(X10,X11),meet(X10,X12))]. % 75.94/76.44 [3256=param(716,123),[], % 75.94/76.44 meet(join(X10,X11),meet(X12,join(meet(X11,X13),X10))) = meet(join(X10,meet(X11,X13)),X12)]. % 75.94/76.44 [3658=param(3223,230),[230], % 75.94/76.44 join(meet(X10,join(X11,X12)),join(meet(X10,X12),X13)) = join(meet(X10,join(X11,X12)),X13)]. % 75.94/76.44 [3679=param(1638,11),[565,234,462,3658,603], % 75.94/76.44 meet(X10,join(meet(X10,X11),meet(X12,join(meet(X11,X12),X10)))) = meet(X10,join(X12,X11))]. % 75.94/76.44 [3803=param(3679,6),[], % 75.94/76.44 meet(X10,join(meet(X11,join(meet(X12,X11),X10)),meet(X10,X12))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [3805=param(3679,9),[-3256,3803,-1702], % 75.94/76.44 meet(X10,join(X11,meet(X12,X10))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [3812=demod(3249),[3805], % 75.94/76.44 meet(X10,join(meet(X10,X11),X12)) = join(meet(X10,X11),meet(X10,X12))]. % 75.94/76.44 [3839=demod(1143),[3805], % 75.94/76.44 join(X10,meet(X11,join(X10,X12))) = join(X10,meet(X11,X12))]. % 75.94/76.44 [3843=demod(1592),[3839], % 75.94/76.44 meet(X10,join(X11,meet(X10,X12))) = meet(X10,join(X11,X12))]. % 75.94/76.44 [3849=param(3843,6),[3812], % 75.94/76.44 meet(X10,join(X12,X11)) = join(meet(X10,X11),meet(X10,X12))]. % 75.94/76.44 [4633=param(15,3849),[9,9,6,14], % 75.94/76.44 thmtrue = thmfalse]. % 75.94/76.44 % SZS output end CNFRefutation % 75.94/76.44 Space: 102084 KB %------------------------------------------------------------------------------