diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-02-17 15:05:43 +0100 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-02-17 15:05:43 +0100 |
| commit | 512ebfcff8674d15b911d2da5afe683ceff232ab (patch) | |
| tree | b178ba79d45c4137d16827a19d9f9791090029ec | |
| parent | 659ce79fa1764c2a174c398949de5862930d8f44 (diff) | |
Clean
| -rw-r--r-- | vampire-taks-with-unexpacted-behavoir/50-plus-secounds-for-iff-stamtent.p | 6 | ||||
| -rw-r--r-- | vampire-taks-with-unexpacted-behavoir/topological-basis-behovoir.p | 26 |
2 files changed, 0 insertions, 32 deletions
diff --git a/vampire-taks-with-unexpacted-behavoir/50-plus-secounds-for-iff-stamtent.p b/vampire-taks-with-unexpacted-behavoir/50-plus-secounds-for-iff-stamtent.p deleted file mode 100644 index 19ed046..0000000 --- a/vampire-taks-with-unexpacted-behavoir/50-plus-secounds-for-iff-stamtent.p +++ /dev/null @@ -1,6 +0,0 @@ -fof(inters_in_genopens,conjecture,unions(fB)=fX). -fof(topological_basis,axiom,![XB,XX]:(topological_basis(XB,XX)<=>(unions(XB)=XX&![XU,XV,Xx]:((elem(XU,XB)&elem(XV,XB)&elem(Xx,XU)&elem(Xx,XV))=>?[XW]:(elem(XW,XB)&elem(Xx,XW)&subseteq(XW,XU)&subseteq(XW,XV)))))). -fof(inters_in_genopens1,axiom,elem(fx,fVprimeprime)&subseteq(fVprimeprime,fC)&elem(fVprimeprime,fB)). -fof(inters_in_genopens2,axiom,elem(fx,fVprime)&subseteq(fVprime,fA)&elem(fVprime,fB)). -fof(inters_in_genopens3,axiom,elem(fx,inter(fA,fC))). -fof(inters_in_genopens4,axiom,topological_basis(fB,fX)). diff --git a/vampire-taks-with-unexpacted-behavoir/topological-basis-behovoir.p b/vampire-taks-with-unexpacted-behavoir/topological-basis-behovoir.p deleted file mode 100644 index 76b03e4..0000000 --- a/vampire-taks-with-unexpacted-behavoir/topological-basis-behovoir.p +++ /dev/null @@ -1,26 +0,0 @@ -% It doesn't make sense for me that this task takes so long. It taks on my computer nearly 50-60 secounds. - -fof(inters_in_genopens,conjecture,?[XW]:(elem(XW,fB)&elem(fx,XW)&subseteq(XW,fvprime)&subseteq(XW,fVprimeprime))). -%fof(topological_basis,axiom,![XB,XX]:(topological_basis(XB,XX)<=>(unions(XB)=XX&![XU,XV,Xx]:((elem(XU,XB)&elem(XV,XB)&elem(Xx,XU)&elem(Xx,XV))=>?[XW]:(elem(XW,XB)&elem(Xx,XW)&subseteq(XW,XU)&subseteq(XW,XV)))))). -fof(inters_in_genopens1,axiom,elem(fx,fVprimeprime)&subseteq(fVprimeprime,fC)&elem(fVprimeprime,fB)). -fof(inters_in_genopens2,axiom,elem(fx,fVprime)&subseteq(fVprime,fA)&elem(fVprime,fB)). -fof(inters_in_genopens3,axiom,elem(fx,inter(fA,fC))). -fof(inters_in_genopens4,axiom,topological_basis(fB,fX)). - -fof(topological_basis1,axiom,![XU,XV,Xx]:((elem(XU,fB)&elem(XV,fB)&elem(Xx,XU)&elem(Xx,XV))=>?[XW]:(elem(XW,fB)&elem(Xx,XW)&subseteq(XW,XU)&subseteq(XW,XV)))). - -fof(inters_in_genopens10,axiom,subseteq(fVprime,fA)). -fof(inters_in_genopens11,axiom,subseteq(fVprimeprime,fC)). -fof(inters_in_genopens12,axiom,elem(fx,fVprime)). -fof(inters_in_genopens13,axiom,elem(fx,fVprimeprime)). - - -% the task (unions(fB)=fX) takes only 0.2 secounds -% but if it is stated as an axiom it doesn't effect any proof time. - - -% with this axiom it takes 27 secounds so it improve the overall time, -% but this axiom is just a "and" more and combines axiom 1 and 2 -% fof(inters_in_genopens5,axiom,elem(fVprimeprime,fB)&elem(fVprimeprime,fB)&elem(fx,fVprime)&elem(fx,fVprimeprime)). - -% fof(topological_basis1,axiom,![XU,XV,Xx]:((elem(XU,fB)&elem(XV,fB)&elem(Xx,XU)&elem(Xx,XV))=>?[XW]:(elem(XW,fB)&elem(Xx,XW)&subseteq(XW,XU)&subseteq(XW,XV)))).
\ No newline at end of file |