The rabbit is rough. The squirrel is round. If someone needs the rabbit then they are round. If someone is rough then they need the rabbit. If someone likes the rabbit and the rabbit is young then they do not need the rabbit. If someone eats the squirrel and the squirrel is round then they like the squirrel. If someone eats the rabbit and the rabbit needs the squirrel then they are not blue. If someone is round then they eat the rabbit.
The rabbit is rough.
("rabbit" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone needs the rabbit then they are round.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they need the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone likes the rabbit and the rabbit is young then they do not need the rabbit.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("someone" "needs" "rabbit" "-"))
If someone eats the squirrel and the squirrel is round then they like the squirrel.
((("someone" "eats" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone eats the rabbit and the rabbit needs the squirrel then they are not blue.
((("someone" "eats" "rabbit" "+") ("rabbit" "needs" "squirrel" "+")) -> ("someone" "is" "blue" "-"))
If someone is round then they eat the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "eats" "rabbit" "+"))
The rabbit is rough.
True
1
proof
[(triple1)]
("rabbit" "is" "rough" "+")
triple1
The rabbit is not rough.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "rough" "-")
triple1
The rabbit needs the rabbit.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "needs" "rabbit" "+")
((triple1) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The squirrel does not eat the rabbit.
False
2
inv-proof
[(((triple2) -> rule6))]
("squirrel" "eats" "rabbit" "-")
((triple2) -> (rule6 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The rabbit is round.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is not round.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "is" "round" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit eats the rabbit.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule6))]
("rabbit" "eats" "rabbit" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit does not eat the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule6))]
("rabbit" "eats" "rabbit" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit does not like the squirrel.
Unknown
inv-rconc
[@1: The rabbit likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "likes" "squirrel" "-")
The squirrel needs the rabbit.
Unknown
rconc
[@1: The squirrel needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "rabbit" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The squirrel likes the rabbit.
Unknown
random
[@0: The squirrel likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "rabbit" "+")
The rabbit does not need the squirrel.
Unknown
inv-random
[@0: The rabbit needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "squirrel" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The rabbit is rough.[(triple1)] The squirrel is round.[(triple2)] @1: The rabbit needs the rabbit.[(((triple1) -> rule2))] The squirrel eats the rabbit.[(((triple2) -> rule6))] @2: The rabbit is round.[(((((triple1) -> rule2)) -> rule1))] @3: The rabbit eats the rabbit.[(((((((triple1) -> rule2)) -> rule1)) -> rule6))]
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple1
The squirrel is round.
("squirrel" "is" "round" "+")
triple2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple1) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((triple2) -> (rule6 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3