The mouse chases the rabbit. The mouse chases the tiger. The mouse is cold. The mouse needs the rabbit. The rabbit chases the mouse. The rabbit is red. The rabbit likes the tiger. The tiger chases the mouse. The tiger is cold. The tiger is red. The tiger likes the rabbit. The tiger needs the mouse. If something needs the tiger and the tiger likes the rabbit then the tiger is blue. If something likes the rabbit and the rabbit chases the tiger then the tiger likes the rabbit. All young things are blue. If something is rough and it likes the rabbit then it needs the tiger. If something chases the rabbit then the rabbit chases the tiger. If something is young then it chases the tiger. If something likes the rabbit and the rabbit is rough then the rabbit likes the mouse. If the rabbit likes the mouse then the mouse is cold.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something needs the tiger and the tiger likes the rabbit then the tiger is blue.
((("something" "needs" "tiger" "+") ("tiger" "likes" "rabbit" "+")) -> ("tiger" "is" "blue" "+"))
If something likes the rabbit and the rabbit chases the tiger then the tiger likes the rabbit.
((("something" "likes" "rabbit" "+") ("rabbit" "chases" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is rough and it likes the rabbit then it needs the tiger.
((("something" "is" "rough" "+") ("something" "likes" "rabbit" "+")) -> ("something" "needs" "tiger" "+"))
If something chases the rabbit then the rabbit chases the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something is young then it chases the tiger.
((("something" "is" "young" "+")) -> ("something" "chases" "tiger" "+"))
If something likes the rabbit and the rabbit is rough then the rabbit likes the mouse.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "likes" "mouse" "+"))
If the rabbit likes the mouse then the mouse is cold.
((("rabbit" "likes" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
The mouse needs the rabbit.
True
1
proof
[(triple4)]
("mouse" "needs" "rabbit" "+")
triple4
The mouse does not need the rabbit.
False
1
inv-proof
[(triple4)]
("mouse" "needs" "rabbit" "-")
triple4
The rabbit chases the tiger.
True
2
proof
[(((triple1) -> rule5))]
("rabbit" "chases" "tiger" "+")
((triple1) -> (rule5 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit does not chase the tiger.
False
2
inv-proof
[(((triple1) -> rule5))]
("rabbit" "chases" "tiger" "-")
((triple1) -> (rule5 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The mouse does not need the tiger.
Unknown
inv-rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "tiger" "-")
The mouse is blue.
Unknown
rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "blue" "+")
The rabbit does not need the mouse.
Unknown
inv-random
[@0: The rabbit needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "mouse" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse chases the tiger.[(triple2)] The mouse is cold.[(triple3)] The mouse needs the rabbit.[(triple4)] The rabbit chases the mouse.[(triple5)] The rabbit is red.[(triple6)] The rabbit likes the tiger.[(triple7)] The tiger chases the mouse.[(triple8)] The tiger is cold.[(triple9)] The tiger is red.[(triple10)] The tiger likes the rabbit.[(triple11)] The tiger needs the mouse.[(triple12)] @1: The rabbit chases the tiger.[(((triple1) -> rule5))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple4
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple7
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple11
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple12
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
((triple1) -> (rule5 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1