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