The cat is kind. The cat sees the rabbit. The rabbit is blue. If someone sees the cat then they are cold. If someone sees the rabbit then the rabbit sees the cat.
The cat is kind.
("cat" "is" "kind" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
If someone sees the cat then they are cold.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the rabbit then the rabbit sees the cat.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
The rabbit is blue.
True
1
proof
[(triple3)]
("rabbit" "is" "blue" "+")
triple3
The rabbit is not blue.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "blue" "-")
triple3
The rabbit sees the cat.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "sees" "cat" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit does not see the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "sees" "cat" "-")
((triple2) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is cold.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("rabbit" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("rabbit" "is" "cold" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "cold" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The rabbit chases the cat.
Unknown
random
[@0: The rabbit chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cat" "+")
@0: The cat is kind.[(triple1)] The cat sees the rabbit.[(triple2)] The rabbit is blue.[(triple3)] @1: The rabbit sees the cat.[(((triple2) -> rule2))] @2: The rabbit is cold.[(((((triple2) -> rule2)) -> rule1))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2