The cat visits the squirrel. The squirrel likes the cat. The squirrel does not visit the cat. If the cat eats the squirrel then the cat visits the squirrel. If the cat is not green then the cat visits the squirrel. If something is round and it visits the squirrel then it is red. If something likes the cat then the cat does not eat the squirrel. If the cat is round and the squirrel does not eat the cat then the squirrel does not like the cat. If something visits the squirrel and it does not eat the squirrel then it likes the squirrel. If something is big and it visits the cat then the cat does not like the squirrel. If something likes the cat and it likes the squirrel then the squirrel visits the cat.
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel does not visit the cat.
("squirrel" "visits" "cat" "-")
If the cat eats the squirrel then the cat visits the squirrel.
((("cat" "eats" "squirrel" "+")) -> ("cat" "visits" "squirrel" "+"))
If the cat is not green then the cat visits the squirrel.
((("cat" "is" "green" "~")) -> ("cat" "visits" "squirrel" "+"))
If something is round and it visits the squirrel then it is red.
((("something" "is" "round" "+") ("something" "visits" "squirrel" "+")) -> ("something" "is" "red" "+"))
If something likes the cat then the cat does not eat the squirrel.
((("something" "likes" "cat" "+")) -> ("cat" "eats" "squirrel" "-"))
If the cat is round and the squirrel does not eat the cat then the squirrel does not like the cat.
((("cat" "is" "round" "+") ("squirrel" "eats" "cat" "~")) -> ("squirrel" "likes" "cat" "-"))
If something visits the squirrel and it does not eat the squirrel then it likes the squirrel.
((("something" "visits" "squirrel" "+") ("something" "eats" "squirrel" "~")) -> ("something" "likes" "squirrel" "+"))
If something is big and it visits the cat then the cat does not like the squirrel.
((("something" "is" "big" "+") ("something" "visits" "cat" "+")) -> ("cat" "likes" "squirrel" "-"))
If something likes the cat and it likes the squirrel then the squirrel visits the cat.
((("something" "likes" "cat" "+") ("something" "likes" "squirrel" "+")) -> ("squirrel" "visits" "cat" "+"))
The squirrel likes the cat.
True
1
proof
[(triple2)]
("squirrel" "likes" "cat" "+")
triple2
The cat does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "visits" "squirrel" "-")
triple1
The cat does not eat the squirrel.
True
2
proof
[(((triple2) -> rule4))]
("cat" "eats" "squirrel" "-")
((triple2) -> (rule4 % int1))
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
int1
The cat eats the squirrel.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "eats" "squirrel" "+")
((triple2) -> (rule4 % int1))
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
int1
The cat likes the squirrel.
True
4
proof
[(((triple1 ((triple2) -> rule4)) -> rule6))]
("cat" "likes" "squirrel" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
int2
The cat does not like the squirrel.
False
4
inv-proof
[(((triple1 ((triple2) -> rule4)) -> rule6))]
("cat" "likes" "squirrel" "-")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
int2
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel is red.
Unknown
rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "red" "+")
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "red" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat visits the squirrel.[(triple1)] The squirrel does not visit the cat.[(triple3)] The squirrel likes the cat.[(triple2)] @1: The cat does not eat the squirrel.[(((triple2) -> rule4))] @2: The cat likes the squirrel.[(((triple1 ((triple2) -> rule4)) -> rule6))]
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple1
The squirrel does not visit the cat.
("squirrel" "visits" "cat" "-")
triple3
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple2
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
((triple2) -> (rule4 % int1))
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat does not eat the squirrel.
("cat" "eats" "squirrel" "-")
int2