The rabbit visits the squirrel. The squirrel is round. If the rabbit visits the squirrel then the squirrel likes the rabbit. If someone likes the rabbit then they chase the squirrel.
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If the rabbit visits the squirrel then the squirrel likes the rabbit.
((("rabbit" "visits" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If someone likes the rabbit then they chase the squirrel.
((("someone" "likes" "rabbit" "+")) -> ("someone" "chases" "squirrel" "+"))
The squirrel is round.
True
1
proof
[(triple2)]
("squirrel" "is" "round" "+")
triple2
The rabbit does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("rabbit" "visits" "squirrel" "-")
triple1
The squirrel likes the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "likes" "rabbit" "+")
((triple1) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel does not like the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "likes" "rabbit" "-")
((triple1) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel chases the squirrel.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("squirrel" "chases" "squirrel" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel does not chase the squirrel.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("squirrel" "chases" "squirrel" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The rabbit does not chase the squirrel.
Unknown
inv-rconc
[@1: The rabbit chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The rabbit visits the squirrel.[(triple1)] The squirrel is round.[(triple2)] @1: The squirrel likes the rabbit.[(((triple1) -> rule1))] @2: The squirrel chases the squirrel.[(((((triple1) -> rule1)) -> rule2))]
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple1
The squirrel is round.
("squirrel" "is" "round" "+")
triple2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((triple1) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2