The cat likes the lion. The cat visits the lion. The lion eats the cat. The lion eats the tiger. The lion is red. The lion is round. The lion likes the cat. The lion likes the tiger. The tiger eats the cat. The tiger eats the lion. The tiger is cold. The tiger is red. The tiger is round. The tiger visits the cat. The tiger visits the lion. If someone is cold then they visit the cat. If the lion is red and the lion likes the tiger then the lion visits the tiger. If someone eats the lion then the lion is round. If someone likes the tiger and they like the lion then the tiger is cold. If someone is green then they visit the lion. If someone likes the lion then they are red. If someone is young and they eat the cat then the cat likes the lion. If someone visits the lion then the lion is young.
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone is cold then they visit the cat.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cat" "+"))
If the lion is red and the lion likes the tiger then the lion visits the tiger.
((("lion" "is" "red" "+") ("lion" "likes" "tiger" "+")) -> ("lion" "visits" "tiger" "+"))
If someone eats the lion then the lion is round.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "round" "+"))
If someone likes the tiger and they like the lion then the tiger is cold.
((("someone" "likes" "tiger" "+") ("someone" "likes" "lion" "+")) -> ("tiger" "is" "cold" "+"))
If someone is green then they visit the lion.
((("someone" "is" "green" "+")) -> ("someone" "visits" "lion" "+"))
If someone likes the lion then they are red.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "red" "+"))
If someone is young and they eat the cat then the cat likes the lion.
((("someone" "is" "young" "+") ("someone" "eats" "cat" "+")) -> ("cat" "likes" "lion" "+"))
If someone visits the lion then the lion is young.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "young" "+"))
The tiger is cold.
True
1
proof
[(triple11)]
("tiger" "is" "cold" "+")
triple11
The lion does not like the tiger.
False
1
inv-proof
[(triple8)]
("lion" "likes" "tiger" "-")
triple8
The lion visits the tiger.
True
3
proof
[(((triple5 triple8) -> rule2))]
("lion" "visits" "tiger" "+")
((triple5 triple8) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion does not visit the tiger.
False
3
inv-proof
[(((triple5 triple8) -> rule2))]
("lion" "visits" "tiger" "-")
((triple5 triple8) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "lion" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "cat" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat likes the lion.[(triple1 OR ((((triple15) -> rule8) triple3) -> rule7) OR ((((triple2) -> rule8) triple3) -> rule7))] The cat visits the lion.[(triple2)] The lion eats the cat.[(triple3)] The lion eats the tiger.[(triple4)] The lion is red.[(triple5)] The lion is round.[(triple6 OR ((triple10) -> rule3))] The lion likes the cat.[(triple7)] The lion likes the tiger.[(triple8)] The tiger eats the cat.[(triple9)] The tiger eats the lion.[(triple10)] The tiger is cold.[(triple11)] The tiger is red.[(triple12)] The tiger is round.[(triple13)] The tiger visits the cat.[(triple14 OR ((triple11) -> rule1))] The tiger visits the lion.[(triple15)] @1: The cat is red.[(((triple1) -> rule6) OR ((((((triple15) -> rule8) triple3) -> rule7)) -> rule6) OR ((((((triple2) -> rule8) triple3) -> rule7)) -> rule6))] The lion is young.[(((triple15) -> rule8) OR ((triple2) -> rule8))] The lion visits the tiger.[(((triple5 triple8) -> rule2))]
The cat likes the lion.
("cat" "likes" "lion" "+")
triple1
((((triple15) -> (rule8 % int2)) triple3) -> (rule7 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple2) -> (rule8 % int2)) triple3) -> (rule7 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple2
The lion eats the cat.
("lion" "eats" "cat" "+")
triple3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The lion is round.
("lion" "is" "round" "+")
triple6
((triple10) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
triple7
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple8
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple9
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple14
((triple11) -> (rule1 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((((triple15) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((((((triple2) -> (rule8 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is young.
("lion" "is" "young" "+")
((triple15) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple2) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple5 triple8) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1