The cow is kind. The cow is nice. The cow sees the lion. The cow sees the rabbit. The dog likes the lion. The dog needs the lion. The dog sees the cow. The lion is not kind. The lion needs the cow. The rabbit is young. The rabbit needs the cow. The rabbit needs the dog. If someone likes the rabbit then they see the cow. If someone is young then they like the rabbit. If someone likes the cow then they do not need the dog.
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion needs the cow.
("lion" "needs" "cow" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If someone likes the rabbit then they see the cow.
((("someone" "likes" "rabbit" "+")) -> ("someone" "sees" "cow" "+"))
If someone is young then they like the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the cow then they do not need the dog.
((("someone" "likes" "cow" "+")) -> ("someone" "needs" "dog" "-"))
The lion needs the cow.
True
1
proof
[(triple9)]
("lion" "needs" "cow" "+")
triple9
The cow is not kind.
False
1
inv-proof
[(triple1)]
("cow" "is" "kind" "-")
triple1
The rabbit likes the rabbit.
True
2
proof
[(((triple10) -> rule2))]
("rabbit" "likes" "rabbit" "+")
((triple10) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple10) -> rule2))]
("rabbit" "likes" "rabbit" "-")
((triple10) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the cow.
True
3
proof
[(((((triple10) -> rule2)) -> rule1))]
("rabbit" "sees" "cow" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit does not see the cow.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule1))]
("rabbit" "sees" "cow" "-")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The lion does not see the cow.
Unknown
inv-rconc
[@2: The lion sees the cow.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "sees" "cow" "-")
The cow sees the cow.
Unknown
rconc
[@2: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("cow" "sees" "cow" "+")
The dog does not like the rabbit.
Unknown
inv-rconc
[@1: The dog likes the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "rabbit" "-")
The dog sees the rabbit.
Unknown
random
[@0: The dog sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "rabbit" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cow is kind.[(triple1)] The cow is nice.[(triple2)] The cow sees the lion.[(triple3)] The cow sees the rabbit.[(triple4)] The dog likes the lion.[(triple5)] The dog needs the lion.[(triple6)] The dog sees the cow.[(triple7)] The lion is not kind.[(triple8)] The lion needs the cow.[(triple9)] The rabbit is young.[(triple10)] The rabbit needs the cow.[(triple11)] The rabbit needs the dog.[(triple12)] @1: The rabbit likes the rabbit.[(((triple10) -> rule2))] @2: The rabbit sees the cow.[(((((triple10) -> rule2)) -> rule1))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow sees the lion.
("cow" "sees" "lion" "+")
triple3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple4
The dog likes the lion.
("dog" "likes" "lion" "+")
triple5
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The dog sees the cow.
("dog" "sees" "cow" "+")
triple7
The lion is not kind.
("lion" "is" "kind" "-")
triple8
The lion needs the cow.
("lion" "needs" "cow" "+")
triple9
The rabbit is young.
("rabbit" "is" "young" "+")
triple10
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple11
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple12
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple10) -> (rule2 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2