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