The cat needs the squirrel. The squirrel is blue. Big, rough people are not blue. If someone needs the squirrel and they are green then the squirrel does not visit the cat. If someone likes the squirrel then they do not like the cat. If someone is green and round then they need the cat. If someone needs the cat then the cat needs the squirrel. If someone needs the cat then they visit the squirrel. If someone needs the squirrel and the squirrel is blue then they visit the squirrel. If the cat visits the squirrel then the cat likes the squirrel.
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
Big, rough people are not blue.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "-"))
If someone needs the squirrel and they are green then the squirrel does not visit the cat.
((("someone" "needs" "squirrel" "+") ("someone" "is" "green" "+")) -> ("squirrel" "visits" "cat" "-"))
If someone likes the squirrel then they do not like the cat.
((("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "cat" "-"))
If someone is green and round then they need the cat.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the cat then the cat needs the squirrel.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "squirrel" "+"))
If someone needs the cat then they visit the squirrel.
((("someone" "needs" "cat" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone needs the squirrel and the squirrel is blue then they visit the squirrel.
((("someone" "needs" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("someone" "visits" "squirrel" "+"))
If the cat visits the squirrel then the cat likes the squirrel.
((("cat" "visits" "squirrel" "+")) -> ("cat" "likes" "squirrel" "+"))
The squirrel is blue.
True
1
proof
[(triple2)]
("squirrel" "is" "blue" "+")
triple2
The squirrel is not blue.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "blue" "-")
triple2
The cat visits the squirrel.
True
3
proof
[(((triple1 triple2) -> rule7))]
("cat" "visits" "squirrel" "+")
((triple1 triple2) -> (rule7 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The cat does not visit the squirrel.
False
3
inv-proof
[(((triple1 triple2) -> rule7))]
("cat" "visits" "squirrel" "-")
((triple1 triple2) -> (rule7 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The cat likes the squirrel.
True
4
proof
[(((((triple1 triple2) -> rule7)) -> rule8))]
("cat" "likes" "squirrel" "+")
((((triple1 triple2) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The cat does not like the squirrel.
False
4
inv-proof
[(((((triple1 triple2) -> rule7)) -> rule8))]
("cat" "likes" "squirrel" "-")
((((triple1 triple2) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The cat does not like the cat.
True
5
proof
[(((((((triple1 triple2) -> rule7)) -> rule8)) -> rule3))]
("cat" "likes" "cat" "-")
((((((triple1 triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat does not like the cat.
("cat" "likes" "cat" "-")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3
The cat likes the cat.
False
5
inv-proof
[(((((((triple1 triple2) -> rule7)) -> rule8)) -> rule3))]
("cat" "likes" "cat" "+")
((((((triple1 triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat does not like the cat.
("cat" "likes" "cat" "-")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "cat" "-")
The squirrel needs the cat.
Unknown
rconc
[@1: The squirrel needs the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "cat" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@2: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The cat needs the squirrel.[(triple1)] The squirrel is blue.[(triple2)] @1: The cat visits the squirrel.[(((triple1 triple2) -> rule7))] @2: The cat likes the squirrel.[(((((triple1 triple2) -> rule7)) -> rule8))] @3: The cat does not like the cat.[(((((((triple1 triple2) -> rule7)) -> rule8)) -> rule3))]
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
((triple1 triple2) -> (rule7 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((((triple1 triple2) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The cat does not like the cat.
("cat" "likes" "cat" "-")
((((((triple1 triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The cat does not like the cat.
("cat" "likes" "cat" "-")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3