The cat is big. The cat is nice. The cat visits the cow. The cat visits the mouse. The cow is kind. The cow likes the lion. The cow needs the mouse. The cow visits the cat. The cow visits the mouse. The lion is big. The lion is round. The lion likes the cat. The lion likes the cow. The mouse is nice. The mouse likes the cat. If someone likes the cat and they are nice then they visit the lion. If someone needs the cow and they are not kind then the cow does not like the lion. If someone is big then they like the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If someone likes the cat and they are nice then they visit the lion.
((("someone" "likes" "cat" "+") ("someone" "is" "nice" "+")) -> ("someone" "visits" "lion" "+"))
If someone needs the cow and they are not kind then the cow does not like the lion.
((("someone" "needs" "cow" "+") ("someone" "is" "kind" "~")) -> ("cow" "likes" "lion" "-"))
If someone is big then they like the cat.
((("someone" "is" "big" "+")) -> ("someone" "likes" "cat" "+"))
The lion likes the cow.
True
1
proof
[(triple13)]
("lion" "likes" "cow" "+")
triple13
The lion is not big.
False
1
inv-proof
[(triple10)]
("lion" "is" "big" "-")
triple10
The cat likes the cat.
True
2
proof
[(((triple1) -> rule3))]
("cat" "likes" "cat" "+")
((triple1) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The mouse does not visit the lion.
False
3
inv-proof
[(((triple15 triple14) -> rule1))]
("mouse" "visits" "lion" "-")
((triple15 triple14) -> (rule1 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The cat visits the lion.
True
4
proof
[(((((triple1) -> rule3) triple2) -> rule1))]
("cat" "visits" "lion" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat does not visit the lion.
False
4
inv-proof
[(((((triple1) -> rule3) triple2) -> rule1))]
("cat" "visits" "lion" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cat" "-")
The cow visits the lion.
Unknown
rconc
[@1: The cow visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "lion" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion needs the cat.
Unknown
random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cat is big.[(triple1)] The cat is nice.[(triple2)] The cat visits the cow.[(triple3)] The cat visits the mouse.[(triple4)] The cow is kind.[(triple5)] The cow likes the lion.[(triple6)] The cow needs the mouse.[(triple7)] The cow visits the cat.[(triple8)] The cow visits the mouse.[(triple9)] The lion is big.[(triple10)] The lion is round.[(triple11)] The lion likes the cat.[(triple12 OR ((triple10) -> rule3))] The lion likes the cow.[(triple13)] The mouse is nice.[(triple14)] The mouse likes the cat.[(triple15)] @1: The cat likes the cat.[(((triple1) -> rule3))] The mouse visits the lion.[(((triple15 triple14) -> rule1))] @2: The cat visits the lion.[(((((triple1) -> rule3) triple2) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple4
The cow is kind.
("cow" "is" "kind" "+")
triple5
The cow likes the lion.
("cow" "likes" "lion" "+")
triple6
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple7
The cow visits the cat.
("cow" "visits" "cat" "+")
triple8
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple9
The lion is big.
("lion" "is" "big" "+")
triple10
The lion is round.
("lion" "is" "round" "+")
triple11
The lion likes the cat.
("lion" "likes" "cat" "+")
triple12
((triple10) -> (rule3 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
triple13
The mouse is nice.
("mouse" "is" "nice" "+")
triple14
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple15
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple1) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
((triple15 triple14) -> (rule1 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2