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