The cat chases the rabbit. The cat needs the rabbit. The rabbit chases the cat. The rabbit eats the cat. The rabbit is kind. The rabbit is young. The rabbit needs the cat. If something chases the rabbit and it is young then the rabbit chases the cat. If something is rough then it chases the cat. If something needs the cat and it eats the rabbit then it is rough. If something is rough and it chases the rabbit then the rabbit eats the cat. If something chases the cat and the cat chases the rabbit then the rabbit chases the cat. If something needs the cat then it is nice.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something chases the rabbit and it is young then the rabbit chases the cat.
((("something" "chases" "rabbit" "+") ("something" "is" "young" "+")) -> ("rabbit" "chases" "cat" "+"))
If something is rough then it chases the cat.
((("something" "is" "rough" "+")) -> ("something" "chases" "cat" "+"))
If something needs the cat and it eats the rabbit then it is rough.
((("something" "needs" "cat" "+") ("something" "eats" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If something is rough and it chases the rabbit then the rabbit eats the cat.
((("something" "is" "rough" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "eats" "cat" "+"))
If something chases the cat and the cat chases the rabbit then the rabbit chases the cat.
((("something" "chases" "cat" "+") ("cat" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cat" "+"))
If something needs the cat then it is nice.
((("something" "needs" "cat" "+")) -> ("something" "is" "nice" "+"))
The rabbit is kind.
True
1
proof
[(triple5)]
("rabbit" "is" "kind" "+")
triple5
The cat does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "chases" "rabbit" "-")
triple1
The rabbit is nice.
True
2
proof
[(((triple7) -> rule6))]
("rabbit" "is" "nice" "+")
((triple7) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not nice.
False
2
inv-proof
[(((triple7) -> rule6))]
("rabbit" "is" "nice" "-")
((triple7) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "rough" "-")
The cat chases the cat.
Unknown
rconc
[@2: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("cat" "chases" "cat" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat chases the rabbit.[(triple1)] The cat needs the rabbit.[(triple2)] The rabbit chases the cat.[(triple3)] The rabbit eats the cat.[(triple4)] The rabbit is kind.[(triple5)] The rabbit is young.[(triple6)] The rabbit needs the cat.[(triple7)] @1: The rabbit is nice.[(((triple7) -> rule6))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple3
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple7) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1