The cat eats the lion. The cat is young. The lion eats the cat. The lion eats the tiger. The lion is big. The lion likes the cat. The lion likes the tiger. The lion visits the cat. The lion visits the tiger. The tiger likes the lion. If something eats the cat and the cat likes the lion then the lion eats the cat. If something likes the lion and it eats the cat then the lion likes the cat. If something is blue and it visits the lion then it likes the tiger. If something is kind and it visits the tiger then it is nice. If the lion is blue and the lion likes the cat then the lion is young. If something is big and it visits the cat then the cat likes the tiger. If something eats the cat and it visits the lion then the cat visits the tiger. If something visits the cat and the cat eats the lion then it is kind.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is young.
("cat" "is" "young" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If something eats the cat and the cat likes the lion then the lion eats the cat.
((("something" "eats" "cat" "+") ("cat" "likes" "lion" "+")) -> ("lion" "eats" "cat" "+"))
If something likes the lion and it eats the cat then the lion likes the cat.
((("something" "likes" "lion" "+") ("something" "eats" "cat" "+")) -> ("lion" "likes" "cat" "+"))
If something is blue and it visits the lion then it likes the tiger.
((("something" "is" "blue" "+") ("something" "visits" "lion" "+")) -> ("something" "likes" "tiger" "+"))
If something is kind and it visits the tiger then it is nice.
((("something" "is" "kind" "+") ("something" "visits" "tiger" "+")) -> ("something" "is" "nice" "+"))
If the lion is blue and the lion likes the cat then the lion is young.
((("lion" "is" "blue" "+") ("lion" "likes" "cat" "+")) -> ("lion" "is" "young" "+"))
If something is big and it visits the cat then the cat likes the tiger.
((("something" "is" "big" "+") ("something" "visits" "cat" "+")) -> ("cat" "likes" "tiger" "+"))
If something eats the cat and it visits the lion then the cat visits the tiger.
((("something" "eats" "cat" "+") ("something" "visits" "lion" "+")) -> ("cat" "visits" "tiger" "+"))
If something visits the cat and the cat eats the lion then it is kind.
((("something" "visits" "cat" "+") ("cat" "eats" "lion" "+")) -> ("something" "is" "kind" "+"))
The lion visits the cat.
True
1
proof
[(triple8)]
("lion" "visits" "cat" "+")
triple8
The lion does not eat the tiger.
False
1
inv-proof
[(triple4)]
("lion" "eats" "tiger" "-")
triple4
The cat likes the tiger.
True
3
proof
[(((triple5 triple8) -> rule6))]
("cat" "likes" "tiger" "+")
((triple5 triple8) -> (rule6 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat does not like the tiger.
False
3
inv-proof
[(((triple5 triple8) -> rule6))]
("cat" "likes" "tiger" "-")
((triple5 triple8) -> (rule6 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The lion is nice.
True
5
proof
[(((((triple8 triple1) -> rule8) triple9) -> rule4))]
("lion" "is" "nice" "+")
((((triple8 triple1) -> (rule8 % int2)) triple9) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is not nice.
False
5
inv-proof
[(((((triple8 triple1) -> rule8) triple9) -> rule4))]
("lion" "is" "nice" "-")
((((triple8 triple1) -> (rule8 % int2)) triple9) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "visits" "tiger" "-")
The tiger is kind.
Unknown
rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "kind" "+")
The cat is not nice.
Unknown
inv-rconc
[@2: The cat is nice.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("cat" "is" "nice" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The cat eats the lion.[(triple1)] The cat is young.[(triple2)] The lion eats the cat.[(triple3)] The lion eats the tiger.[(triple4)] The lion is big.[(triple5)] The lion likes the cat.[(triple6)] The lion likes the tiger.[(triple7)] The lion visits the cat.[(triple8)] The lion visits the tiger.[(triple9)] The tiger likes the lion.[(triple10)] @1: The cat likes the tiger.[(((triple5 triple8) -> rule6))] The lion is kind.[(((triple8 triple1) -> rule8))] @2: The lion is nice.[(((((triple8 triple1) -> rule8) triple9) -> rule4))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The lion eats the cat.
("lion" "eats" "cat" "+")
triple3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple4
The lion is big.
("lion" "is" "big" "+")
triple5
The lion likes the cat.
("lion" "likes" "cat" "+")
triple6
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple7
The lion visits the cat.
("lion" "visits" "cat" "+")
triple8
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple9
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple10
The cat likes the tiger.
("cat" "likes" "tiger" "+")
((triple5 triple8) -> (rule6 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple8 triple1) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((((triple8 triple1) -> (rule8 % int2)) triple9) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2