The dog eats the lion. The dog likes the lion. The lion likes the dog. If something needs the dog and the dog does not like the lion then the lion needs the dog. If something eats the lion then the lion eats the dog. If the lion likes the dog then the lion is round. If something is round then it does not need the lion. If something is young then it does not like the dog. If the lion does not eat the dog then the lion is young. If something is young and it needs the dog then it is round. If something eats the dog and the dog is round then it is blue.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
If something needs the dog and the dog does not like the lion then the lion needs the dog.
((("something" "needs" "dog" "+") ("dog" "likes" "lion" "~")) -> ("lion" "needs" "dog" "+"))
If something eats the lion then the lion eats the dog.
((("something" "eats" "lion" "+")) -> ("lion" "eats" "dog" "+"))
If the lion likes the dog then the lion is round.
((("lion" "likes" "dog" "+")) -> ("lion" "is" "round" "+"))
If something is round then it does not need the lion.
((("something" "is" "round" "+")) -> ("something" "needs" "lion" "-"))
If something is young then it does not like the dog.
((("something" "is" "young" "+")) -> ("something" "likes" "dog" "-"))
If the lion does not eat the dog then the lion is young.
((("lion" "eats" "dog" "~")) -> ("lion" "is" "young" "+"))
If something is young and it needs the dog then it is round.
((("something" "is" "young" "+") ("something" "needs" "dog" "+")) -> ("something" "is" "round" "+"))
If something eats the dog and the dog is round then it is blue.
((("something" "eats" "dog" "+") ("dog" "is" "round" "+")) -> ("something" "is" "blue" "+"))
The dog eats the lion.
True
1
proof
[(triple1)]
("dog" "eats" "lion" "+")
triple1
The dog does not like the lion.
False
1
inv-proof
[(triple2)]
("dog" "likes" "lion" "-")
triple2
The lion is round.
True
2
proof
[(((triple3) -> rule3))]
("lion" "is" "round" "+")
((triple3) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple3) -> rule3))]
("lion" "is" "round" "-")
((triple3) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "blue" "-")
The lion is blue.
Unknown
rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("lion" "is" "blue" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The dog eats the lion.[(triple1)] The dog likes the lion.[(triple2)] The lion likes the dog.[(triple3)] @1: The lion eats the dog.[(((triple1) -> rule2))] The lion is round.[(((triple3) -> rule3))] @2: The lion does not need the lion.[(((((triple3) -> rule3)) -> rule4))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog likes the lion.
("dog" "likes" "lion" "+")
triple2
The lion likes the dog.
("lion" "likes" "dog" "+")
triple3
The lion eats the dog.
("lion" "eats" "dog" "+")
((triple1) -> (rule2 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((triple3) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion does not need the lion.
("lion" "needs" "lion" "-")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is round.
("lion" "is" "round" "+")
int2