The cat eats the rabbit. The cat eats the squirrel. The rabbit does not eat the cat. The rabbit is rough. The rabbit needs the squirrel. The squirrel eats the cat. The squirrel is rough. If someone needs the squirrel then the squirrel is big. If someone is red and they visit the rabbit then they are rough.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If someone needs the squirrel then the squirrel is big.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
If someone is red and they visit the rabbit then they are rough.
((("someone" "is" "red" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
The rabbit does not eat the cat.
True
1
proof
[(triple3)]
("rabbit" "eats" "cat" "-")
triple3
The squirrel is not rough.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "rough" "-")
triple7
The squirrel is big.
True
2
proof
[(((triple5) -> rule1))]
("squirrel" "is" "big" "+")
((triple5) -> (rule1 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is not big.
False
2
inv-proof
[(((triple5) -> rule1))]
("squirrel" "is" "big" "-")
((triple5) -> (rule1 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "rough" "-")
The rabbit eats the squirrel.
Unknown
random
[@0: The rabbit eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "squirrel" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The cat eats the rabbit.[(triple1)] The cat eats the squirrel.[(triple2)] The rabbit does not eat the cat.[(triple3)] The rabbit is rough.[(triple4)] The rabbit needs the squirrel.[(triple5)] The squirrel eats the cat.[(triple6)] The squirrel is rough.[(triple7)] @1: The squirrel is big.[(((triple5) -> rule1))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The rabbit does not eat the cat.
("rabbit" "eats" "cat" "-")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple4
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple5
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple6
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
((triple5) -> (rule1 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1