Input files and proofs for interval_meeting entailing Allens algebra

ontologies/allen_interval_algebra/mappings/theorems/intervalmeeting2allen/1.1 before-before.in

@@ -0,0 +1,61 @@
+% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).
+
+set(ignore_option_dependencies). % GUI handles dependencies
+
+if(Prover9). % Options for Prover9
+  assign(max_seconds, 60).
+end_if.
+
+if(Mace4).   % Options for Mace4
+  assign(max_seconds, 60).
+end_if.
+
+formulas(assumptions).
+
+%original interval meeting axioms
+(all i all j all k all m
+	((meets(i,k)
+	& meets(j,k)
+	& meets(i,m))
+	->
+	meets(j,m))).
+
+(all i all j all k all l
+	((meets(i,j)
+	& meets(k,l))
+	->
+	(meets(i,l)
+	| (exists n
+		((meets(i,n) & meets(n,l))
+		| (meets(k,n) & meets(n,j))))))).
+
+(all i all j
+	(meets(i,j)
+	->
+	-meets(j,i))).
+
+(all i all j all k all m
+	((meets(i,j)
+	& meets(j,k)
+	& meets(k,m))
+	->
+	(exists n
+		(meets(i,n)
+		& meets(n,m))))).
+
+%definition
+(all x all y
+	(b(x,y)
+	<->
+	(exists z
+		(meets(x,z)
+		& meets(z,y))))).
+
+end_of_list.
+
+formulas(goals).
+
+all x all y all z ((b(x,y) & b(y,z)) -> b(x,z)).
+
+end_of_list.
+

ontologies/allen_interval_algebra/mappings/theorems/intervalmeeting2allen/1.1 before-before.proof

@@ -0,0 +1,53 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 45076 was started by zhuojun on Zhuojun-Li.local,
+Wed May 10 00:25:04 2017
+The command was "/Users/zhuojun/Desktop/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.46 (+ 0.02) seconds.
+% Length of proof is 33.
+% Level of proof is 9.
+% Maximum clause weight is 22.
+% Given clauses 319.
+
+4 (all i all j all k all m (meets(i,j) & meets(j,k) & meets(k,m) -> (exists n (meets(i,n) & meets(n,m))))) # label(non_clause).  [assumption].
+5 (all x all y (b(x,y) <-> (exists z (meets(x,z) & meets(z,y))))) # label(non_clause).  [assumption].
+6 (all x all y all z (b(x,y) & b(y,z) -> b(x,z))) # label(non_clause) # label(goal).  [goal].
+7 b(x,y) | -meets(x,z) | -meets(z,y).  [clausify(5)].
+8 -b(x,y) | meets(x,f3(x,y)).  [clausify(5)].
+9 -b(x,y) | meets(f3(x,y),y).  [clausify(5)].
+10 b(c1,c2).  [deny(6)].
+11 b(c2,c3).  [deny(6)].
+12 -b(c1,c3).  [deny(6)].
+19 -meets(x,y) | -meets(y,z) | -meets(z,u) | meets(x,f2(x,y,z,u)).  [clausify(4)].
+20 -meets(x,y) | -meets(y,z) | -meets(z,u) | meets(f2(x,y,z,u),u).  [clausify(4)].
+21 -meets(x,y) | -meets(y,z) | meets(x,f3(x,z)).  [resolve(7,a,8,a)].
+22 -meets(x,y) | -meets(y,z) | meets(f3(x,z),z).  [resolve(7,a,9,a)].
+23 meets(c1,f3(c1,c2)).  [resolve(10,a,8,a)].
+24 meets(f3(c1,c2),c2).  [resolve(10,a,9,a)].
+25 meets(c2,f3(c2,c3)).  [resolve(11,a,8,a)].
+26 meets(f3(c2,c3),c3).  [resolve(11,a,9,a)].
+27 -meets(c1,x) | -meets(x,c3).  [resolve(12,a,7,a)].
+35 -meets(f3(c1,c2),x) | -meets(x,y) | meets(f2(c1,f3(c1,c2),x,y),y).  [resolve(23,a,20,a)].
+38 -meets(f3(c1,c2),x) | -meets(x,y) | meets(c1,f2(c1,f3(c1,c2),x,y)).  [resolve(23,a,19,a)].
+57 -meets(c2,x) | -meets(x,y) | meets(f2(f3(c1,c2),c2,x,y),y).  [resolve(24,a,20,a)].
+60 -meets(c2,x) | -meets(x,y) | meets(f3(c1,c2),f2(f3(c1,c2),c2,x,y)).  [resolve(24,a,19,a)].
+434 meets(f2(f3(c1,c2),c2,f3(c2,c3),c3),c3).  [resolve(57,b,26,a),unit_del(a,25)].
+451 -meets(x,f2(f3(c1,c2),c2,f3(c2,c3),c3)) | meets(f3(x,c3),c3).  [resolve(434,a,22,b)].
+453 -meets(x,f2(f3(c1,c2),c2,f3(c2,c3),c3)) | meets(x,f3(x,c3)).  [resolve(434,a,21,b)].
+725 meets(f3(c1,c2),f2(f3(c1,c2),c2,f3(c2,c3),c3)).  [resolve(60,b,26,a),unit_del(a,25)].
+1358 meets(f3(f3(c1,c2),c3),c3).  [resolve(451,a,725,a)].
+1391 -meets(f3(c1,c2),f3(f3(c1,c2),c3)) | meets(c1,f2(c1,f3(c1,c2),f3(f3(c1,c2),c3),c3)).  [resolve(1358,a,38,b)].
+1393 -meets(f3(c1,c2),f3(f3(c1,c2),c3)) | meets(f2(c1,f3(c1,c2),f3(f3(c1,c2),c3),c3),c3).  [resolve(1358,a,35,b)].
+1486 meets(f3(c1,c2),f3(f3(c1,c2),c3)).  [resolve(453,a,725,a)].
+1487 meets(f2(c1,f3(c1,c2),f3(f3(c1,c2),c3),c3),c3).  [back_unit_del(1393),unit_del(a,1486)].
+1488 meets(c1,f2(c1,f3(c1,c2),f3(f3(c1,c2),c3),c3)).  [back_unit_del(1391),unit_del(a,1486)].
+1668 $F.  [resolve(1487,a,27,b),unit_del(a,1488)].
+
+============================== end of proof ==========================

ontologies/allen_interval_algebra/mappings/theorems/intervalmeeting2allen/1.10 before-started-by.in

@@ -0,0 +1,74 @@
+% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).
+
+set(ignore_option_dependencies). % GUI handles dependencies
+
+if(Prover9). % Options for Prover9
+  assign(max_seconds, 60).
+end_if.
+
+if(Mace4).   % Options for Mace4
+  assign(max_seconds, 60).
+end_if.
+
+formulas(assumptions).
+
+%original interval meeting axioms
+
+(all i all j all k all m
+	((meets(i,k)
+	& meets(j,k)
+	& meets(i,m))
+	->
+	meets(j,m))).
+
+(all i all j all k all l
+	((meets(i,j)
+	& meets(k,l))
+	->
+	(meets(i,l)
+	| (exists n
+		((meets(i,n) & meets(n,l))
+		| (meets(k,n) & meets(n,j))))))).
+
+(all i all j
+	(meets(i,j)
+	->
+	-meets(j,i))).
+
+(all i all j all k all m
+	((meets(i,j)
+	& meets(j,k)
+	& meets(k,m))
+	->
+	(exists n
+		(meets(i,n)
+		& meets(n,m))))).
+
+all x all y (s(x,y) <-> si(y,x)).
+
+%definition
+(all x all y
+	(b(x,y)
+	<->
+	(exists z
+		(meets(x,z)
+		& meets(z,y))))).
+
+(all i all j
+	(s(i,j)
+	<->
+	(exists k exists m exists n
+		(meets(k,i)
+		& meets(i,m)
+		& meets(m,n)
+		& meets(k,j)
+		& meets(j,n))))).
+
+end_of_list.
+
+formulas(goals).
+
+all x all y all z ((b(x,y) & si(y,z)) -> b(x,z)).
+
+end_of_list.
+

ontologies/allen_interval_algebra/mappings/theorems/intervalmeeting2allen/1.10 before-started-by.proof

@@ -0,0 +1,44 @@
+============================== prooftrans ============================
+Prover9 (32) version Dec-2007, Dec 2007.
+Process 45295 was started by zhuojun on Zhuojun-Li.local,
+Wed May 10 01:04:21 2017
+The command was "/Users/zhuojun/Desktop/Prover9-Mace4-v05B.app/Contents/Resources/bin-mac-intel/prover9".
+============================== end of head ===========================
+
+============================== end of input ==========================
+
+============================== PROOF =================================
+
+% -------- Comments from original proof --------
+% Proof 1 at 0.11 (+ 0.01) seconds.
+% Length of proof is 24.
+% Level of proof is 4.
+% Maximum clause weight is 12.
+% Given clauses 46.
+
+1 (all i all j all k all m (meets(i,k) & meets(j,k) & meets(i,m) -> meets(j,m))) # label(non_clause).  [assumption].
+5 (all x all y (s(x,y) <-> si(y,x))) # label(non_clause).  [assumption].
+6 (all x all y (b(x,y) <-> (exists z (meets(x,z) & meets(z,y))))) # label(non_clause).  [assumption].
+7 (all i all j (s(i,j) <-> (exists k exists m exists n (meets(k,i) & meets(i,m) & meets(m,n) & meets(k,j) & meets(j,n))))) # label(non_clause).  [assumption].
+8 (all x all y all z (b(x,y) & si(y,z) -> b(x,z))) # label(non_clause) # label(goal).  [goal].
+9 s(x,y) | -si(y,x).  [clausify(5)].
+11 -s(x,y) | meets(f4(x,y),x).  [clausify(7)].
+14 -s(x,y) | meets(f4(x,y),y).  [clausify(7)].
+17 b(x,y) | -meets(x,z) | -meets(z,y).  [clausify(6)].
+18 -b(x,y) | meets(x,f3(x,y)).  [clausify(6)].
+19 -b(x,y) | meets(f3(x,y),y).  [clausify(6)].
+20 b(c1,c2).  [deny(8)].
+21 -b(c1,c3).  [deny(8)].
+22 meets(f4(x,y),x) | -si(y,x).  [resolve(11,a,9,a)].
+23 si(c2,c3).  [deny(8)].
+26 meets(f4(x,y),y) | -si(y,x).  [resolve(14,a,9,a)].
+29 -meets(x,y) | -meets(z,y) | -meets(x,u) | meets(z,u).  [clausify(1)].
+44 meets(c1,f3(c1,c2)).  [resolve(20,a,18,a)].
+45 meets(f3(c1,c2),c2).  [resolve(20,a,19,a)].
+46 -meets(c1,x) | -meets(x,c3).  [resolve(21,a,17,a)].
+47 meets(f4(c3,c2),c3).  [resolve(22,b,23,a)].
+50 meets(f4(c3,c2),c2).  [resolve(26,b,23,a)].
+210 -meets(f3(c1,c2),c3).  [resolve(46,a,44,a)].
+657 $F.  [ur(29,b,45,a,c,47,a,d,210,a),unit_del(a,50)].
+
+============================== end of proof ==========================

ontologies/allen_interval_algebra/mappings/theorems/intervalmeeting2allen/1.11 before-ends not after.in

@@ -0,0 +1,162 @@
+% Saved by Prover9-Mace4 Version 0.5B, March 2008 (Dec 2007 LADR).
+
+set(ignore_option_dependencies). % GUI handles dependencies
+
+if(Prover9). % Options for Prover9
+  assign(max_seconds, 60).
+end_if.
+
+if(Mace4).   % Options for Mace4
+  assign(max_seconds, 60).
+end_if.
+
+formulas(assumptions).
+
+%original interval meeting axioms
+
+(all i all j all k all m
+	((meets(i,k)
+	& meets(j,k)
+	& meets(i,m))
+	->
+	meets(j,m))).
+
+(all i all j all k all l
+	((meets(i,j)
+	& meets(k,l))
+	->
+	(meets(i,l)
+	| (exists n
+		((meets(i,n) & meets(n,l))
+		| (meets(k,n) & meets(n,j))))))).
+
+(all i all j
+	(meets(i,j)
+	->
+	-meets(j,i))).
+
+(all i all j all k all m
+	((meets(i,j)
+	& meets(j,k)
+	& meets(k,m))
+	->
+	(exists n
+		(meets(i,n)
+		& meets(n,m))))).
+
+all x all y (m(x,y) <-> meets(x,y)).
+
+%definition
+(all x all y
+	(b(x,y)
+	<->
+	(exists z
+		(meets(x,z)
+		& meets(z,y))))).
+
+(all i all j
+	(e(i,j)
+	<->
+	(exists k exists m exists n
+		(meets(k,m)
+		& meets(m,i)
+		& meets(i,n)
+		& meets(k,j)
+		& meets(j,n))))).
+
+all x all y (b(x,y) <-> a(y,x)).
+all x all y (d(x,y) <-> di(y,x)).
+all x all y (o(x,y) <-> oi(y,x)).
+all x all y (m(x,y) <-> mi(y,x)).
+all x all y (s(x,y) <-> si(y,x)).
+all x all y (e(x,y) <-> ei(y,x)).
+
+%proved lemma
+(all x all y all z (b(x,y) & b(y,z) -> b(x,z))).
+(all x all y all z (b(x,y) & di(y,z) -> b(x,z))).
+(all x all y all z (b(x,y) & o(y,z) -> b(x,z))).
+(all x all y all z (b(x,y) & m(y,z) -> b(x,z))).
+(all x all y all z (b(x,y) & s(y,z) -> b(x,z))).
+(all x all y all z (b(x,y) & si(y,z) -> b(x,z))).
+(all x all y all z (b(x,y) & ei(y,z) -> b(x,z))).
+
+(all x all y all z (a(x,y) & a(y,z) -> a(x,z))).
+(all x all y all z (a(x,y) & di(y,z) -> a(x,z))).
+(all x all y all z (a(x,y) & oi(y,z) -> a(x,z))).
+(all x all y all z (a(x,y) & si(y,z) -> a(x,z))).
+(all x all y all z (a(x,y) & e(y,z) -> a(x,z))).
+(all x all y all z (a(x,y) & ei(y,z) -> a(x,z))).
+
+(all x all y all z (d(x,y) & b(y,z) -> b(x,z))).
+(all x all y all z (d(x,y) & a(y,z) -> a(x,z))).
+(all x all y all z (d(x,y) & d(y,z) -> d(x,z))).
+(all x all y all z (d(x,y) & m(y,z) -> b(x,z))).
+(all x all y all z (d(x,y) & mi(y,z) -> a(x,z))).
+(all x all y all z (d(x,y) & s(y,z) -> d(x,z))).
+
+(all x all y all z (di(x,y) & di(y,z) -> di(x,z))).
+(all x all y all z (di(x,y) & si(y,z) -> di(x,z))).
+(all x all y all z (di(x,y) & ei(y,z) -> di(x,z))).
+
+(all x all y all z (o(x,y) & b(y,z) -> b(x,z))).
+(all x all y all z (o(x,y) & m(y,z) -> b(x,z))).
+
+(all x all y all z (oi(x,y) & a(y,z) -> a(x,z))).
+(all x all y all z (oi(x,y) & mi(y,z) -> a(x,z))).
+(all x all y all z (oi(x,y) & e(y,z) -> oi(x,z))).
+
+(all x all y all z (m(x,y) & b(y,z) -> b(x,z))).
+(all x all y all z (m(x,y) & di(y,z) -> b(x,z))).
+(all x all y all z (m(x,y) & o(y,z) -> b(x,z))).
+(all x all y all z (m(x,y) & m(y,z) -> b(x,z))).
+(all x all y all z (m(x,y) & s(y,z) -> m(x,z))).
+(all x all y all z (m(x,y) & si(y,z) -> m(x,z))).
+(all x all y all z (m(x,y) & ei(y,z) -> b(x,z))).
+
+(all x all y all z (mi(x,y) & b(y,z) -> a(x,z))).
+(all x all y all z (mi(x,y) & di(y,z) -> a(x,z))).
+(all x all y all z (mi(x,y) & oi(y,z) -> a(x,z))).
+(all x all y all z (mi(x,y) & mi(y,z) -> a(x,z))).
+(all x all y all z (mi(x,y) & si(y,z) -> a(x,z))).
+(all x all y all z (mi(x,y) & e(y,z) -> mi(x,z))).
+(all x all y all z (mi(x,y) & ei(y,z) -> mi(x,z))).
+
+(all x all y all z (s(x,y) & b(y,z) -> b(x,z))).
+(all x all y all z (s(x,y) & a(y,z) -> a(x,z))).
+(all x all y all z (s(x,y) & d(y,z) -> d(x,z))).
+(all x all y all z (s(x,y) & m(y,z) -> b(x,z))).
+(all x all y all z (s(x,y) & mi(y,z) -> mi(x,z))).
+(all x all y all z (s(x,y) & s(y,z) -> s(x,z))).
+(all x all y all z (s(x,y) & e(y,z) -> d(x,z))).
+
+(all x all y all z (si(x,y) & a(y,z) -> a(x,z))).
+(all x all y all z (si(x,y) & di(y,z) -> di(x,z))).
+(all x all y all z (si(x,y) & mi(y,z) -> mi(x,z))).
+(all x all y all z (si(x,y) & si(y,z) -> si(x,z))).
+(all x all y all z (si(x,y) & e(y,z) -> oi(x,z))).
+(all x all y all z (si(x,y) & ei(y,z) -> di(x,z))).
+
+(all x all y all z (e(x,y) & b(y,z) -> b(x,z))).
+(all x all y all z (e(x,y) & a(y,z) -> a(x,z))).
+(all x all y all z (e(x,y) & d(y,z) -> d(x,z))).
+(all x all y all z (e(x,y) & m(y,z) -> m(x,z))).
+(all x all y all z (e(x,y) & mi(y,z) -> a(x,z))).
+(all x all y all z (e(x,y) & s(y,z) -> d(x,z))).
+(all x all y all z (e(x,y) & e(y,z) -> e(x,z))).
+
+(all x all y all z (ei(x,y) & b(y,z) -> b(x,z))).
+(all x all y all z (ei(x,y) & di(y,z) -> di(x,z))).
+(all x all y all z (ei(x,y) & o(y,z) -> o(x,z))).
+(all x all y all z (ei(x,y) & m(y,z) -> m(x,z))).
+(all x all y all z (ei(x,y) & s(y,z) -> o(x,z))).
+(all x all y all z (ei(x,y) & si(y,z) -> di(x,z))).
+(all x all y all z (ei(x,y) & ei(y,z) -> ei(x,z))).
+
+end_of_list.
+
+formulas(goals).
+
+all x all y all z ((b(x,y) & e(y,z)) -> (-a(x,z))).
+
+end_of_list.
+