The rabbit chases the squirrel. The squirrel is cold. The squirrel is red. If someone chases the squirrel then they need the rabbit. If someone eats the rabbit and the rabbit is young then they are rough. If someone is kind and they chase the squirrel then they chase the rabbit. If someone chases the squirrel and they need the rabbit then the rabbit eats the squirrel. If the rabbit eats the squirrel then the rabbit is rough. If someone is red and they chase the squirrel then the squirrel chases the rabbit.
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If someone chases the squirrel then they need the rabbit.
((("someone" "chases" "squirrel" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone eats the rabbit and the rabbit is young then they are rough.
((("someone" "eats" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind and they chase the squirrel then they chase the rabbit.
((("someone" "is" "kind" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the squirrel and they need the rabbit then the rabbit eats the squirrel.
((("someone" "chases" "squirrel" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If the rabbit eats the squirrel then the rabbit is rough.
((("rabbit" "eats" "squirrel" "+")) -> ("rabbit" "is" "rough" "+"))
If someone is red and they chase the squirrel then the squirrel chases the rabbit.
((("someone" "is" "red" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "chases" "rabbit" "+"))
The squirrel is red.
True
1
proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The squirrel is not red.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "red" "-")
triple3
The rabbit needs the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "needs" "rabbit" "-")
((triple1) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the squirrel.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("rabbit" "eats" "squirrel" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit does not eat the squirrel.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("rabbit" "eats" "squirrel" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is rough.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule5))]
("rabbit" "is" "rough" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is not rough.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule5))]
("rabbit" "is" "rough" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The squirrel does not chase the rabbit.
Unknown
inv-rconc
[@1: The squirrel chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "rabbit" "-")
The squirrel needs the rabbit.
Unknown
rconc
[@1: The squirrel needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "rabbit" "+")
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The squirrel is rough.
Unknown
rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "rough" "+")
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 chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The squirrel eats the rabbit.
Unknown
random
[@0: The squirrel eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "rabbit" "+")
@0: The rabbit chases the squirrel.[(triple1)] The squirrel is cold.[(triple2)] The squirrel is red.[(triple3)] @1: The rabbit needs the rabbit.[(((triple1) -> rule1))] @2: The rabbit eats the squirrel.[(((triple1 ((triple1) -> rule1)) -> rule4))] @3: The rabbit is rough.[(((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule5))]
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3