The bear likes the lion. The cat eats the lion. The dog likes the lion. The lion visits the cat. If something likes the dog then it likes the lion. If the dog likes the cat and the cat visits the bear then the cat likes the bear. If something eats the lion then it is cold. If something is cold then it likes the lion. If something eats the dog and the dog eats the lion then the lion visits the bear. If something likes the lion and it is red then the lion eats the dog.
The bear likes the lion.
("bear" "likes" "lion" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If something likes the dog then it likes the lion.
((("something" "likes" "dog" "+")) -> ("something" "likes" "lion" "+"))
If the dog likes the cat and the cat visits the bear then the cat likes the bear.
((("dog" "likes" "cat" "+") ("cat" "visits" "bear" "+")) -> ("cat" "likes" "bear" "+"))
If something eats the lion then it is cold.
((("something" "eats" "lion" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it likes the lion.
((("something" "is" "cold" "+")) -> ("something" "likes" "lion" "+"))
If something eats the dog and the dog eats the lion then the lion visits the bear.
((("something" "eats" "dog" "+") ("dog" "eats" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If something likes the lion and it is red then the lion eats the dog.
((("something" "likes" "lion" "+") ("something" "is" "red" "+")) -> ("lion" "eats" "dog" "+"))
The bear likes the lion.
True
1
proof
[(triple1)]
("bear" "likes" "lion" "+")
triple1
The dog does not like the lion.
False
1
inv-proof
[(triple3)]
("dog" "likes" "lion" "-")
triple3
The cat is cold.
True
2
proof
[(((triple2) -> rule3))]
("cat" "is" "cold" "+")
((triple2) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "is" "cold" "-")
((triple2) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat likes the lion.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("cat" "likes" "lion" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat does not like the lion.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("cat" "likes" "lion" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The lion does not like the lion.
Unknown
inv-rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("lion" "likes" "lion" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "cold" "+")
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "cold" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
@0: The bear likes the lion.[(triple1)] The cat eats the lion.[(triple2)] The dog likes the lion.[(triple3)] The lion visits the cat.[(triple4)] @1: The cat is cold.[(((triple2) -> rule3))] @2: The cat likes the lion.[(((((triple2) -> rule3)) -> rule4))]
The bear likes the lion.
("bear" "likes" "lion" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
The dog likes the lion.
("dog" "likes" "lion" "+")
triple3
The lion visits the cat.
("lion" "visits" "cat" "+")
triple4
The cat is cold.
("cat" "is" "cold" "+")
((triple2) -> (rule3 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2