The mouse chases the tiger. The mouse is cold. The mouse is red. The mouse is rough. The mouse likes the tiger. The mouse needs the tiger. The tiger chases the mouse. The tiger is big. The tiger is red. The tiger is rough. The tiger likes the mouse. The tiger needs the mouse. If something is red then it chases the tiger. If the mouse likes the tiger and the mouse needs the tiger then the mouse is rough.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something is red then it chases the tiger.
((("something" "is" "red" "+")) -> ("something" "chases" "tiger" "+"))
If the mouse likes the tiger and the mouse needs the tiger then the mouse is rough.
((("mouse" "likes" "tiger" "+") ("mouse" "needs" "tiger" "+")) -> ("mouse" "is" "rough" "+"))
The mouse is rough.
True
1
proof
[(triple4 OR ((triple5 triple6) -> rule2))]
("mouse" "is" "rough" "+")
triple4
((triple5 triple6) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse does not like the tiger.
False
1
inv-proof
[(triple5)]
("mouse" "likes" "tiger" "-")
triple5
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The mouse chases the tiger.[(triple1 OR ((triple3) -> rule1))] The mouse is cold.[(triple2)] The mouse is red.[(triple3)] The mouse is rough.[(triple4 OR ((triple5 triple6) -> rule2))] The mouse likes the tiger.[(triple5)] The mouse needs the tiger.[(triple6)] The tiger chases the mouse.[(triple7)] The tiger is big.[(triple8)] The tiger is red.[(triple9)] The tiger is rough.[(triple10)] The tiger likes the mouse.[(triple11)] The tiger needs the mouse.[(triple12)] @1: The tiger chases the tiger.[(((triple9) -> rule1))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
((triple3) -> (rule1 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
((triple5 triple6) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple11
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple12
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple9) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1