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