%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : LAT043-1 : TPTP v8.1.0. Released v2.5.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:34 EDT 2022 % Result : Unsatisfiable 0.69s 1.14s % Output : CNFRefutation 0.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : LAT043-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.13 % Command : fiesta-wrapper %s % 0.13/0.33 % Computer : n029.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Jun 29 01:41:37 EDT 2022 % 0.13/0.33 % CPUTime : % 0.69/1.14 Theorem Proved. % 0.69/1.14 % SZS status Unsatisfiable % 0.69/1.14 % SZS output start CNFRefutation % 0.69/1.14 [1=axiom,[], % 0.69/1.14 complement(complement(X10)) = X10]. % 0.69/1.14 [2=axiom,[], % 0.69/1.14 meet(complement(X10),X10) = n0]. % 0.69/1.14 [3=axiom,[], % 0.69/1.14 join(complement(X10),X10) = n1]. % 0.69/1.14 [4=axiom,[], % 0.69/1.14 meet(X10,join(X11,X12)) = join(meet(X10,X11),meet(X10,X12))]. % 0.69/1.14 [5=axiom,[], % 0.69/1.14 join(join(X10,X11),X12) = join(X10,join(X11,X12))]. % 0.69/1.14 [6=axiom,[], % 0.69/1.14 meet(meet(X10,X11),X12) = meet(X10,meet(X11,X12))]. % 0.69/1.14 [7=axiom,[], % 0.69/1.14 join(X10,X11) = join(X11,X10)]. % 0.69/1.14 [8=demod(3),[7], % 0.69/1.14 join(X10,complement(X10)) = n1]. % 0.69/1.14 [9=axiom,[], % 0.69/1.14 meet(X10,X11) = meet(X11,X10)]. % 0.69/1.14 [10=demod(2),[9], % 0.69/1.14 meet(X10,complement(X10)) = n0]. % 0.69/1.14 [11=axiom,[], % 0.69/1.14 join(X10,meet(X10,X11)) = X10]. % 0.69/1.14 [14=axiom,[], % 0.69/1.14 meet(X10,X10) = X10]. % 0.69/1.14 [15=axiom,[], % 0.69/1.14 thtop(X10,X10) = thmfalse]. % 0.69/1.14 [16=axiom,[7,9], % 0.69/1.14 thtop(complement(join(d,c)),meet(complement(d),complement(c))) = thmtrue]. % 0.69/1.14 [17=param(4,8),[], % 0.69/1.14 join(meet(X10,X11),meet(X10,complement(X11))) = meet(X10,n1)]. % 0.69/1.14 [26=param(11,10),[], % 0.69/1.14 join(X10,n0) = X10]. % 0.69/1.14 [29=param(6,10),[], % 0.69/1.14 meet(X10,meet(X11,complement(meet(X10,X11)))) = n0]. % 0.69/1.14 [30=param(6,10),[], % 0.69/1.14 meet(X11,meet(complement(X11),X10)) = meet(n0,X10)]. % 0.69/1.14 [34=param(9,6),[], % 0.69/1.14 meet(X10,meet(X11,X12)) = meet(X11,meet(X12,X10))]. % 0.69/1.14 [35=param(6,9),[6], % 0.69/1.14 meet(X10,meet(X11,X12)) = meet(X11,meet(X10,X12))]. % 0.69/1.14 [36=param(11,9),[], % 0.69/1.14 join(X10,meet(X11,X10)) = X10]. % 0.69/1.14 [37=param(36,4),[5], % 0.69/1.14 join(X10,join(X11,join(meet(X12,X10),meet(X12,X11)))) = join(X10,X11)]. % 0.69/1.14 [39=param(5,36),[], % 0.69/1.14 join(X10,join(meet(X12,X10),X11)) = join(X10,X11)]. % 0.69/1.14 [44=param(7,26),[], % 0.69/1.14 join(n0,X10) = X10]. % 0.69/1.14 [47=param(44,11),[], % 0.69/1.14 meet(n0,X10) = n0]. % 0.69/1.14 [48=demod(30),[47], % 0.69/1.14 meet(X10,meet(complement(X10),X11)) = n0]. % 0.69/1.14 [51=param(17,9),[], % 0.69/1.14 join(meet(X10,X11),meet(X11,complement(X10))) = meet(X11,n1)]. % 0.69/1.14 [52=param(17,9),[], % 0.69/1.14 join(meet(X10,X11),meet(complement(X11),X10)) = meet(X10,n1)]. % 0.69/1.14 [53=param(17,10),[1,14,44], % 0.69/1.14 meet(X10,n1) = X10]. % 0.69/1.14 [54=demod(52),[53], % 0.69/1.14 join(meet(X10,X11),meet(complement(X11),X10)) = X10]. % 0.69/1.14 [56=demod(51),[53], % 0.69/1.14 join(meet(X10,X11),meet(X11,complement(X10))) = X11]. % 0.69/1.14 [105=param(48,9),[], % 0.69/1.14 meet(X10,meet(X11,complement(X10))) = n0]. % 0.69/1.14 [133=param(34,48),[], % 0.69/1.14 meet(complement(X10),meet(X11,X10)) = n0]. % 0.69/1.14 [139=param(34,105),[], % 0.69/1.14 meet(complement(X10),meet(X10,X11)) = n0]. % 0.69/1.14 [154=param(37,7),[39], % 0.69/1.14 join(X10,join(X11,meet(X12,X10))) = join(X10,X11)]. % 0.69/1.14 [233=param(54,9),[], % 0.69/1.14 join(meet(X10,X11),meet(complement(X10),X11)) = X11]. % 0.69/1.14 [245=param(54,133),[9,44], % 0.69/1.14 meet(complement(X10),complement(meet(X11,X10))) = complement(X10)]. % 0.69/1.14 [247=param(54,139),[9,44], % 0.69/1.14 meet(complement(X10),complement(meet(X10,X11))) = complement(X10)]. % 0.69/1.14 [286=param(154,56),[], % 0.69/1.14 join(complement(X10),meet(X10,X11)) = join(complement(X10),X11)]. % 0.69/1.14 [306=param(35,247),[], % 0.69/1.14 meet(complement(X11),meet(X10,complement(meet(X11,X12)))) = meet(X10,complement(X11))]. % 0.69/1.14 [324=param(233,29),[306,44], % 0.69/1.14 meet(X10,complement(meet(X11,X10))) = meet(X10,complement(X11))]. % 0.69/1.14 [332=param(233,245),[1,324,286], % 0.69/1.14 complement(meet(X11,X10)) = join(complement(X10),complement(X11))]. % 0.69/1.14 [360=param(1,332),[], % 0.69/1.14 meet(X11,X10) = complement(join(complement(X10),complement(X11)))]. % 0.69/1.14 [487=param(16,360),[1,1,7,15], % 0.69/1.14 thmtrue = thmfalse]. % 0.69/1.14 % SZS output end CNFRefutation % 0.69/1.14 Space: 366 KB %------------------------------------------------------------------------------