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