The rabbit visits the squirrel. The squirrel needs the rabbit. If someone likes the squirrel then the squirrel is rough. If someone needs the rabbit then they visit the squirrel. All rough people are nice. If someone needs the rabbit and they need the squirrel then the rabbit needs the squirrel. If someone needs the rabbit then the rabbit likes the squirrel. If someone visits the rabbit and they need the squirrel then the rabbit likes the squirrel. If someone visits the squirrel and they like the squirrel then the squirrel needs the rabbit. If someone visits the squirrel and they are blue then they need the squirrel.
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If someone likes the squirrel then the squirrel is rough.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If someone needs the rabbit then they visit the squirrel.
((("someone" "needs" "rabbit" "+")) -> ("someone" "visits" "squirrel" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the rabbit and they need the squirrel then the rabbit needs the squirrel.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "squirrel" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If someone needs the rabbit then the rabbit likes the squirrel.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If someone visits the rabbit and they need the squirrel then the rabbit likes the squirrel.
((("someone" "visits" "rabbit" "+") ("someone" "needs" "squirrel" "+")) -> ("rabbit" "likes" "squirrel" "+"))
If someone visits the squirrel and they like the squirrel then the squirrel needs the rabbit.
((("someone" "visits" "squirrel" "+") ("someone" "likes" "squirrel" "+")) -> ("squirrel" "needs" "rabbit" "+"))
If someone visits the squirrel and they are blue then they need the squirrel.
((("someone" "visits" "squirrel" "+") ("someone" "is" "blue" "+")) -> ("someone" "needs" "squirrel" "+"))
The squirrel needs the rabbit.
True
1
proof
[(triple2)]
("squirrel" "needs" "rabbit" "+")
triple2
The rabbit does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("rabbit" "visits" "squirrel" "-")
triple1
The rabbit likes the squirrel.
True
2
proof
[(((triple2) -> rule5))]
("rabbit" "likes" "squirrel" "+")
((triple2) -> (rule5 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "visits" "squirrel" "-")
((triple2) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is rough.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("squirrel" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The squirrel is not rough.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("squirrel" "is" "rough" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The squirrel is nice.
True
4
proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("squirrel" "is" "nice" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The squirrel is not nice.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("squirrel" "is" "nice" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit needs the squirrel.
Unknown
rconc
[@2: The rabbit needs the squirrel.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("rabbit" "needs" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The rabbit visits the squirrel.[(triple1)] The squirrel needs the rabbit.[(triple2)] @1: The rabbit likes the squirrel.[(((triple2) -> rule5))] The squirrel visits the squirrel.[(((triple2) -> rule2))] @2: The squirrel is rough.[(((((triple2) -> rule5)) -> rule1))] @3: The squirrel is nice.[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple1
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
((triple2) -> (rule5 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple2) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int3