%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LAT143-1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n024.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:56:02 EDT 2022 % Result : Unsatisfiable 34.11s 34.48s % Output : CNFRefutation 34.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : LAT143-1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 30 13:08:00 EDT 2022 % 0.13/0.34 % CPUTime : % 34.11/34.48 Theorem Proved. % 34.11/34.48 % SZS status Unsatisfiable % 34.11/34.48 % SZS output start CNFRefutation % 34.11/34.48 [1=axiom,[], % 34.11/34.48 join(meet(X10,X11),meet(X11,join(meet(X10,X11),meet(X12,join(X10,X11))))) = join(meet(X10,X11),meet(X11,X12))]. % 34.11/34.48 [2=axiom,[], % 34.11/34.48 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 34.11/34.48 [3=axiom,[], % 34.11/34.48 meet(meet(X10,X11),X12) = meet(X10,meet(X11,X12))]. % 34.11/34.48 [4=axiom,[], % 34.11/34.48 join(X10,X11) = join(X11,X10)]. % 34.11/34.48 [5=axiom,[], % 34.11/34.48 meet(X10,X11) = meet(X11,X10)]. % 34.11/34.48 [6=axiom,[], % 34.11/34.48 join(X10,meet(X10,X11)) = X10]. % 34.11/34.48 [7=axiom,[], % 34.11/34.48 meet(X10,join(X10,X11)) = X10]. % 34.11/34.48 [10=axiom,[], % 34.11/34.48 thtop(X10,X10) = thmfalse]. % 34.11/34.48 [11=axiom,[5,5,4,5,5,4,4,2], % 34.11/34.48 thtop(meet(a,join(meet(c,a),meet(b,a))),meet(a,join(meet(c,a),join(meet(c,join(b,a)),meet(b,a))))) = thmtrue]. % 34.11/34.48 [13=param(6,5),[], % 34.11/34.48 join(X10,meet(X11,X10)) = X10]. % 34.11/34.48 [20=param(2,13),[], % 34.11/34.48 join(X10,join(meet(X12,X10),X11)) = join(X10,X11)]. % 34.11/34.48 [21=param(13,7),[2], % 34.11/34.48 join(X10,join(X11,X10)) = join(X10,X11)]. % 34.11/34.48 [22=param(4,2),[], % 34.11/34.48 join(X10,join(X11,X12)) = join(X11,join(X12,X10))]. % 34.11/34.48 [24=param(7,4),[], % 34.11/34.48 meet(X10,join(X11,X10)) = X10]. % 34.11/34.48 [25=param(3,5),[], % 34.11/34.48 meet(X10,meet(X11,X12)) = meet(X12,meet(X10,X11))]. % 34.11/34.48 [28=param(3,7),[], % 34.11/34.48 meet(X10,meet(X11,join(meet(X10,X11),X12))) = meet(X10,X11)]. % 34.11/34.48 [32=param(13,3),[], % 34.11/34.48 join(X10,meet(X11,meet(X12,X10))) = X10]. % 34.11/34.48 [33=param(24,2),[], % 34.11/34.48 meet(X10,join(X11,join(X12,X10))) = X10]. % 34.11/34.48 [36=param(24,6),[3], % 34.11/34.48 meet(X10,meet(X11,X10)) = meet(X10,X11)]. % 34.11/34.48 [40=param(13,36),[], % 34.11/34.48 join(meet(X10,X11),meet(X11,X10)) = meet(X10,X11)]. % 34.11/34.48 [45=param(24,21),[], % 34.11/34.48 meet(join(X10,X11),join(X11,X10)) = join(X10,X11)]. % 34.11/34.48 [59=param(33,6),[3], % 34.11/34.48 meet(X10,meet(X11,join(X12,X10))) = meet(X10,X11)]. % 34.11/34.48 [71=param(32,7),[2], % 34.11/34.48 join(X10,join(X11,meet(X12,X10))) = join(X10,X11)]. % 34.11/34.48 [79=param(71,36),[], % 34.11/34.48 join(meet(X10,X11),join(X12,meet(X11,X10))) = join(meet(X10,X11),X12)]. % 34.11/34.48 [83=param(24,20),[5], % 34.11/34.48 meet(join(X10,X11),join(meet(X12,X10),X11)) = join(meet(X12,X10),X11)]. % 34.11/34.48 [112=param(13,59),[], % 34.11/34.48 join(meet(X10,join(X11,X12)),meet(X12,X10)) = meet(X10,join(X11,X12))]. % 34.11/34.48 [113=param(59,21),[], % 34.11/34.48 meet(join(X10,X11),meet(X12,join(X11,X10))) = meet(join(X10,X11),X12)]. % 34.11/34.48 [144=param(25,45),[113], % 34.11/34.48 meet(X10,join(X11,X12)) = meet(join(X12,X11),X10)]. % 34.11/34.48 [151=param(22,40),[79], % 34.11/34.48 join(X10,meet(X11,X12)) = join(meet(X12,X11),X10)]. % 34.11/34.48 [153=demod(112),[151], % 34.11/34.48 join(meet(X10,X11),meet(X10,join(X12,X11))) = meet(X10,join(X12,X11))]. % 34.11/34.48 [183=param(151,4),[], % 34.11/34.48 join(meet(X10,X11),X12) = join(meet(X11,X10),X12)]. % 34.11/34.48 [229=param(151,144),[], % 34.11/34.48 join(X10,meet(X11,join(X12,X13))) = join(meet(X11,join(X13,X12)),X10)]. % 34.11/34.48 [409=param(11,22),[153,229,4], % 34.11/34.48 thtop(meet(a,join(meet(c,a),meet(b,a))),meet(a,join(meet(c,join(b,a)),meet(b,a)))) = thmtrue]. % 34.11/34.48 [693=param(83,13),[], % 34.11/34.48 meet(X10,join(meet(X11,X10),meet(X12,X10))) = join(meet(X11,X10),meet(X12,X10))]. % 34.11/34.48 [1484=param(13,28),[151], % 34.11/34.48 join(meet(X10,X11),meet(X10,join(meet(X11,X10),X12))) = meet(X10,join(meet(X11,X10),X12))]. % 34.11/34.48 [1503=param(183,1),[1484], % 34.11/34.48 meet(X10,join(meet(X11,X10),meet(X12,join(X11,X10)))) = join(meet(X11,X10),meet(X10,X12))]. % 34.11/34.48 [4790=param(1503,4),[], % 34.11/34.48 meet(X10,join(meet(X11,join(X12,X10)),meet(X12,X10))) = join(meet(X12,X10),meet(X10,X11))]. % 34.11/34.48 [4822=param(409,4790),[693,5,4,10], % 34.11/34.48 thmtrue = thmfalse]. % 34.11/34.48 % SZS output end CNFRefutation % 34.11/34.48 Space: 84858 KB %------------------------------------------------------------------------------