The cat chases the rabbit. The cat is round. The cat sees the lion. The cat sees the rabbit. The lion sees the cat. The lion sees the rabbit. The rabbit chases the lion. The rabbit is big. The rabbit is round. The rabbit does not need the lion. The rabbit sees the cat. The rabbit sees the lion. If the cat chases the lion then the cat chases the rabbit. If something sees the rabbit and the rabbit needs the lion then the rabbit sees the cat. If the rabbit is not round then the rabbit does not see the cat. If something is cold and blue then it needs the lion. If the lion sees the cat and the lion does not chase the rabbit then the rabbit is not kind. If something is big and it chases the lion then the lion is big.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is round.
("cat" "is" "round" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If the cat chases the lion then the cat chases the rabbit.
((("cat" "chases" "lion" "+")) -> ("cat" "chases" "rabbit" "+"))
If something sees the rabbit and the rabbit needs the lion then the rabbit sees the cat.
((("something" "sees" "rabbit" "+") ("rabbit" "needs" "lion" "+")) -> ("rabbit" "sees" "cat" "+"))
If the rabbit is not round then the rabbit does not see the cat.
((("rabbit" "is" "round" "~")) -> ("rabbit" "sees" "cat" "-"))
If something is cold and blue then it needs the lion.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "lion" "+"))
If the lion sees the cat and the lion does not chase the rabbit then the rabbit is not kind.
((("lion" "sees" "cat" "+") ("lion" "chases" "rabbit" "~")) -> ("rabbit" "is" "kind" "-"))
If something is big and it chases the lion then the lion is big.
((("something" "is" "big" "+") ("something" "chases" "lion" "+")) -> ("lion" "is" "big" "+"))
The cat sees the rabbit.
True
1
proof
[(triple4)]
("cat" "sees" "rabbit" "+")
triple4
The rabbit does not see the lion.
False
1
inv-proof
[(triple12)]
("rabbit" "sees" "lion" "-")
triple12
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "needs" "lion" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The cat chases the rabbit.[(triple1)] The cat is round.[(triple2)] The cat sees the lion.[(triple3)] The cat sees the rabbit.[(triple4)] The lion sees the cat.[(triple5)] The lion sees the rabbit.[(triple6)] The rabbit chases the lion.[(triple7)] The rabbit does not need the lion.[(triple10)] The rabbit is big.[(triple8)] The rabbit is round.[(triple9)] The rabbit sees the cat.[(triple11)] The rabbit sees the lion.[(triple12)] @1: The lion is big.[(((triple8 triple7) -> rule6))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple4
The lion sees the cat.
("lion" "sees" "cat" "+")
triple5
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple6
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple7
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
The lion is big.
("lion" "is" "big" "+")
((triple8 triple7) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1