The dog eats the lion. The dog is round. The lion eats the dog. The lion is big. The lion is kind. The lion likes the dog. The lion visits the dog. If someone visits the lion and they like the lion then the lion is round. If someone is kind and they visit the dog then they do not eat the lion. If someone visits the dog and they do not eat the lion then the lion is not young.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is round.
("dog" "is" "round" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone visits the lion and they like the lion then the lion is round.
((("someone" "visits" "lion" "+") ("someone" "likes" "lion" "+")) -> ("lion" "is" "round" "+"))
If someone is kind and they visit the dog then they do not eat the lion.
((("someone" "is" "kind" "+") ("someone" "visits" "dog" "+")) -> ("someone" "eats" "lion" "-"))
If someone visits the dog and they do not eat the lion then the lion is not young.
((("someone" "visits" "dog" "+") ("someone" "eats" "lion" "~")) -> ("lion" "is" "young" "-"))
The lion is kind.
True
1
proof
[(triple5)]
("lion" "is" "kind" "+")
triple5
The dog does not eat the lion.
False
1
inv-proof
[(triple1)]
("dog" "eats" "lion" "-")
triple1
The lion does not eat the lion.
True
3
proof
[(((triple5 triple7) -> rule2))]
("lion" "eats" "lion" "-")
((triple5 triple7) -> (rule2 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion eats the lion.
False
3
inv-proof
[(((triple5 triple7) -> rule2))]
("lion" "eats" "lion" "+")
((triple5 triple7) -> (rule2 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is not young.
True
5
proof
[(((triple7 ((triple5 triple7) -> rule2)) -> rule3))]
("lion" "is" "young" "-")
((triple7 ((triple5 triple7) -> (rule2 % int2))) -> (rule3 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int2
The lion is young.
False
5
inv-proof
[(((triple7 ((triple5 triple7) -> rule2)) -> rule3))]
("lion" "is" "young" "+")
((triple7 ((triple5 triple7) -> (rule2 % int2))) -> (rule3 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int2
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "round" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog eats the lion.[(triple1)] The dog is round.[(triple2)] The lion eats the dog.[(triple3)] The lion is big.[(triple4)] The lion is kind.[(triple5)] The lion likes the dog.[(triple6)] The lion visits the dog.[(triple7)] @1: The lion does not eat the lion.[(((triple5 triple7) -> rule2))] @2: The lion is not young.[(((triple7 ((triple5 triple7) -> rule2)) -> rule3))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The lion eats the dog.
("lion" "eats" "dog" "+")
triple3
The lion is big.
("lion" "is" "big" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion likes the dog.
("lion" "likes" "dog" "+")
triple6
The lion visits the dog.
("lion" "visits" "dog" "+")
triple7
The lion does not eat the lion.
("lion" "eats" "lion" "-")
((triple5 triple7) -> (rule2 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion is not young.
("lion" "is" "young" "-")
((triple7 ((triple5 triple7) -> (rule2 % int2))) -> (rule3 % int1))
The lion is not young.
("lion" "is" "young" "-")
int1
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int2