The cat chases the rabbit. The rabbit sees the cat. If something is round then it sees the cat. If something sees the cat then it sees the rabbit. If something sees the rabbit then it eats the cat. If the rabbit is cold and the rabbit does not eat the cat then the rabbit chases the cat. If something eats the rabbit then the rabbit chases the cat. If something eats the cat and it does not chase the cat then the cat chases the rabbit.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something is round then it sees the cat.
((("something" "is" "round" "+")) -> ("something" "sees" "cat" "+"))
If something sees the cat then it sees the rabbit.
((("something" "sees" "cat" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the rabbit then it eats the cat.
((("something" "sees" "rabbit" "+")) -> ("something" "eats" "cat" "+"))
If the rabbit is cold and the rabbit does not eat the cat then the rabbit chases the cat.
((("rabbit" "is" "cold" "+") ("rabbit" "eats" "cat" "~")) -> ("rabbit" "chases" "cat" "+"))
If something eats the rabbit then the rabbit chases the cat.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "chases" "cat" "+"))
If something eats the cat and it does not chase the cat then the cat chases the rabbit.
((("something" "eats" "cat" "+") ("something" "chases" "cat" "~")) -> ("cat" "chases" "rabbit" "+"))
The cat chases the rabbit.
True
1
proof
[(triple1)]
("cat" "chases" "rabbit" "+")
triple1
The cat does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "chases" "rabbit" "-")
triple1
The rabbit sees the rabbit.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "sees" "rabbit" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "sees" "rabbit" "-")
((triple2) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the cat.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("rabbit" "eats" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit does not eat the cat.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("rabbit" "eats" "cat" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat eats the cat.
Unknown
rconc
[@3: The cat eats the cat.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("cat" "eats" "cat" "+")
The rabbit does not chase the cat.
Unknown
inv-rconc
[@1: The rabbit chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "cat" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
@0: The cat chases the rabbit.[(triple1)] The rabbit sees the cat.[(triple2)] @1: The rabbit sees the rabbit.[(((triple2) -> rule2))] @2: The rabbit eats the cat.[(((((triple2) -> rule2)) -> rule3))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2