The dog likes the rabbit. The rabbit is green. The rabbit likes the dog. The squirrel needs the dog. The squirrel needs the rabbit. The squirrel visits the dog. The squirrel visits the rabbit. If the rabbit visits the squirrel and the rabbit likes the dog then the dog visits the squirrel. If something is green then it visits the rabbit. If something is green and it visits the rabbit then the rabbit visits the squirrel.
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If the rabbit visits the squirrel and the rabbit likes the dog then the dog visits the squirrel.
((("rabbit" "visits" "squirrel" "+") ("rabbit" "likes" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If something is green then it visits the rabbit.
((("something" "is" "green" "+")) -> ("something" "visits" "rabbit" "+"))
If something is green and it visits the rabbit then the rabbit visits the squirrel.
((("something" "is" "green" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "+"))
The squirrel visits the dog.
True
1
proof
[(triple6)]
("squirrel" "visits" "dog" "+")
triple6
The squirrel does not need the dog.
False
1
inv-proof
[(triple4)]
("squirrel" "needs" "dog" "-")
triple4
The rabbit visits the rabbit.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "visits" "rabbit" "+")
((triple2) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "visits" "rabbit" "-")
((triple2) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the squirrel.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("rabbit" "visits" "squirrel" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit does not visit the squirrel.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("rabbit" "visits" "squirrel" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The dog does not visit the rabbit.
Unknown
inv-rconc
[@1: The dog visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "rabbit" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog likes the rabbit.[(triple1)] The rabbit is green.[(triple2)] The rabbit likes the dog.[(triple3)] The squirrel needs the dog.[(triple4)] The squirrel needs the rabbit.[(triple5)] The squirrel visits the dog.[(triple6)] The squirrel visits the rabbit.[(triple7)] @1: The rabbit visits the rabbit.[(((triple2) -> rule2))] @2: The rabbit visits the squirrel.[(((triple2 ((triple2) -> rule2)) -> rule3))] @3: The dog visits the squirrel.[(((((triple2 ((triple2) -> rule2)) -> rule3) triple3) -> rule1))]
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple3
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple4
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple5
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple6
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple7
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple2) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2)) triple3) -> (rule1 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3