The mouse is big. The mouse likes the tiger. The tiger chases the mouse. The tiger is not big. The tiger is blue. The tiger is rough. The tiger likes the mouse. If the tiger chases the mouse then the tiger needs the mouse. If someone needs the tiger then the tiger is big. If the mouse is round then the mouse is nice.
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If the tiger chases the mouse then the tiger needs the mouse.
((("tiger" "chases" "mouse" "+")) -> ("tiger" "needs" "mouse" "+"))
If someone needs the tiger then the tiger is big.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If the mouse is round then the mouse is nice.
((("mouse" "is" "round" "+")) -> ("mouse" "is" "nice" "+"))
The tiger is not big.
True
1
proof
[(triple4)]
("tiger" "is" "big" "-")
triple4
The tiger is not blue.
False
1
inv-proof
[(triple5)]
("tiger" "is" "blue" "-")
triple5
The tiger needs the mouse.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "needs" "mouse" "+")
((triple3) -> (rule1 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("tiger" "needs" "mouse" "-")
((triple3) -> (rule1 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "nice" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
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 chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The mouse is big.[(triple1)] The mouse likes the tiger.[(triple2)] The tiger chases the mouse.[(triple3)] The tiger is blue.[(triple5)] The tiger is not big.[(triple4)] The tiger is rough.[(triple6)] The tiger likes the mouse.[(triple7)] @1: The tiger needs the mouse.[(((triple3) -> rule1))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple2
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple5
The tiger is not big.
("tiger" "is" "big" "-")
triple4
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple7
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
((triple3) -> (rule1 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1