The rabbit chases the squirrel. The rabbit is red. The rabbit likes the squirrel. The rabbit needs the squirrel. The squirrel is big. The squirrel is red. The squirrel is not young. If something likes the rabbit then it needs the rabbit. If the squirrel is not young then the squirrel likes the rabbit.
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is not young.
("squirrel" "is" "young" "-")
If something likes the rabbit then it needs the rabbit.
((("something" "likes" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If the squirrel is not young then the squirrel likes the rabbit.
((("squirrel" "is" "young" "~")) -> ("squirrel" "likes" "rabbit" "+"))
The squirrel is red.
True
1
proof
[(triple6)]
("squirrel" "is" "red" "+")
triple6
The squirrel is not red.
False
1
inv-proof
[(triple6)]
("squirrel" "is" "red" "-")
triple6
The squirrel likes the rabbit.
True
2
proof
[(((triple7) -> rule2))]
("squirrel" "likes" "rabbit" "+")
((triple7) -> (rule2 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel does not like the rabbit.
False
2
inv-proof
[(((triple7) -> rule2))]
("squirrel" "likes" "rabbit" "-")
((triple7) -> (rule2 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel needs the rabbit.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("squirrel" "needs" "rabbit" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel does not need the rabbit.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("squirrel" "needs" "rabbit" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The squirrel does not chase the rabbit.
Unknown
inv-random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The rabbit chases the squirrel.[(triple1)] The rabbit is red.[(triple2)] The rabbit likes the squirrel.[(triple3)] The rabbit needs the squirrel.[(triple4)] The squirrel is big.[(triple5)] The squirrel is not young.[(triple7)] The squirrel is red.[(triple6)] @1: The squirrel likes the rabbit.[(((triple7) -> rule2))] @2: The squirrel needs the rabbit.[(((((triple7) -> rule2)) -> rule1))]
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
triple2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple3
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel is not young.
("squirrel" "is" "young" "-")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple6
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((triple7) -> (rule2 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2