The cow eats the lion. The cow is round. The cow likes the dog. The cow likes the lion. The cow sees the lion. The dog is nice. The dog sees the lion. The lion eats the cow. The lion is big. The lion likes the cow. If something sees the lion and the lion likes the cow then the cow eats the dog. If something sees the dog and it eats the dog then the dog eats the lion. If something eats the dog and the dog sees the lion then the dog likes the cow.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
If something sees the lion and the lion likes the cow then the cow eats the dog.
((("something" "sees" "lion" "+") ("lion" "likes" "cow" "+")) -> ("cow" "eats" "dog" "+"))
If something sees the dog and it eats the dog then the dog eats the lion.
((("something" "sees" "dog" "+") ("something" "eats" "dog" "+")) -> ("dog" "eats" "lion" "+"))
If something eats the dog and the dog sees the lion then the dog likes the cow.
((("something" "eats" "dog" "+") ("dog" "sees" "lion" "+")) -> ("dog" "likes" "cow" "+"))
The cow is round.
True
1
proof
[(triple2)]
("cow" "is" "round" "+")
triple2
The cow does not like the lion.
False
1
inv-proof
[(triple4)]
("cow" "likes" "lion" "-")
triple4
The cow eats the dog.
True
3
proof
[(((triple5 triple10) -> rule1) OR ((triple7 triple10) -> rule1))]
("cow" "eats" "dog" "+")
((triple5 triple10) -> (rule1 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
((triple7 triple10) -> (rule1 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow does not eat the dog.
False
3
inv-proof
[(((triple5 triple10) -> rule1) OR ((triple7 triple10) -> rule1))]
("cow" "eats" "dog" "-")
((triple5 triple10) -> (rule1 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
((triple7 triple10) -> (rule1 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The dog likes the cow.
True
5
proof
[(((((triple5 triple10) -> rule1) triple7) -> rule3) OR ((((triple7 triple10) -> rule1) triple7) -> rule3))]
("dog" "likes" "cow" "+")
((((triple5 triple10) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
((((triple7 triple10) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog does not like the cow.
False
5
inv-proof
[(((((triple5 triple10) -> rule1) triple7) -> rule3) OR ((((triple7 triple10) -> rule1) triple7) -> rule3))]
("dog" "likes" "cow" "-")
((((triple5 triple10) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
((((triple7 triple10) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog does not eat the lion.
Unknown
inv-rconc
[@1: The dog eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "lion" "-")
The lion eats the dog.
Unknown
random
[@0: The lion eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "dog" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The dog likes the lion.
Unknown
random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow eats the lion.[(triple1)] The cow is round.[(triple2)] The cow likes the dog.[(triple3)] The cow likes the lion.[(triple4)] The cow sees the lion.[(triple5)] The dog is nice.[(triple6)] The dog sees the lion.[(triple7)] The lion eats the cow.[(triple8)] The lion is big.[(triple9)] The lion likes the cow.[(triple10)] @1: The cow eats the dog.[(((triple5 triple10) -> rule1) OR ((triple7 triple10) -> rule1))] @2: The dog likes the cow.[(((((triple5 triple10) -> rule1) triple7) -> rule3) OR ((((triple7 triple10) -> rule1) triple7) -> rule3))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The cow likes the lion.
("cow" "likes" "lion" "+")
triple4
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The dog is nice.
("dog" "is" "nice" "+")
triple6
The dog sees the lion.
("dog" "sees" "lion" "+")
triple7
The lion eats the cow.
("lion" "eats" "cow" "+")
triple8
The lion is big.
("lion" "is" "big" "+")
triple9
The lion likes the cow.
("lion" "likes" "cow" "+")
triple10
The cow eats the dog.
("cow" "eats" "dog" "+")
((triple5 triple10) -> (rule1 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
((triple7 triple10) -> (rule1 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
((((triple5 triple10) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
((((triple7 triple10) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2