The cow is blue. The cow likes the dog. The cow likes the rabbit. The cow needs the rabbit. The cow visits the rabbit. The dog is blue. The dog is red. The dog needs the rabbit. The dog visits the cow. The rabbit is green. The rabbit is rough. The rabbit likes the cow. The rabbit needs the dog. The rabbit visits the cow. The rabbit visits the dog. If someone needs the rabbit then the rabbit needs the dog. If someone likes the rabbit and they are cold then they need the rabbit. If someone likes the rabbit then the rabbit is cold. If someone is cold and they visit the rabbit then the rabbit is cold. If someone is blue then they visit the rabbit. If someone is green then they are blue.
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone needs the rabbit then the rabbit needs the dog.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If someone likes the rabbit and they are cold then they need the rabbit.
((("someone" "likes" "rabbit" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone likes the rabbit then the rabbit is cold.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is cold and they visit the rabbit then the rabbit is cold.
((("someone" "is" "cold" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is blue then they visit the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
The rabbit likes the cow.
True
1
proof
[(triple12)]
("rabbit" "likes" "cow" "+")
triple12
The rabbit is not rough.
False
1
inv-proof
[(triple11)]
("rabbit" "is" "rough" "-")
triple11
The dog visits the rabbit.
True
2
proof
[(((triple6) -> rule5))]
("dog" "visits" "rabbit" "+")
((triple6) -> (rule5 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple10) -> rule6))]
("rabbit" "is" "blue" "-")
((triple10) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the rabbit.
True
3
proof
[(((((triple10) -> rule6)) -> rule5))]
("rabbit" "visits" "rabbit" "+")
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit does not visit the rabbit.
False
3
inv-proof
[(((((triple10) -> rule6)) -> rule5))]
("rabbit" "visits" "rabbit" "-")
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The dog needs the cow.
Unknown
random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "+")
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 visits the dog.
Unknown
random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog likes the rabbit.
Unknown
random
[@0: The dog likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "rabbit" "+")
@0: The cow is blue.[(triple1)] The cow likes the dog.[(triple2)] The cow likes the rabbit.[(triple3)] The cow needs the rabbit.[(triple4)] The cow visits the rabbit.[(triple5 OR ((triple1) -> rule5))] The dog is blue.[(triple6)] The dog is red.[(triple7)] The dog needs the rabbit.[(triple8)] The dog visits the cow.[(triple9)] The rabbit is green.[(triple10)] The rabbit is rough.[(triple11)] The rabbit likes the cow.[(triple12)] The rabbit needs the dog.[(triple13 OR ((triple4) -> rule1) OR ((triple8) -> rule1))] The rabbit visits the cow.[(triple14)] The rabbit visits the dog.[(triple15)] @1: The dog visits the rabbit.[(((triple6) -> rule5))] The rabbit is blue.[(((triple10) -> rule6))] The rabbit is cold.[(((triple3) -> rule3))] @2: The rabbit visits the rabbit.[(((((triple10) -> rule6)) -> rule5))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple2
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple4
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple5
((triple1) -> (rule5 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog is red.
("dog" "is" "red" "+")
triple7
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple8
The dog visits the cow.
("dog" "visits" "cow" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple12
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple13
((triple4) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
((triple8) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple14
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple15
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((triple6) -> (rule5 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple10) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple3) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2