The mouse is big. The mouse is nice. The mouse is not rough. The mouse is young. The mouse does not like the tiger. The mouse needs the tiger. The mouse does not see the tiger. The tiger is big. The tiger is not nice. The tiger is red. The tiger is rough. The tiger is young. The tiger likes the mouse. The tiger needs the mouse. The tiger sees the mouse. If someone needs the tiger then the tiger likes the mouse.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone needs the tiger then the tiger likes the mouse.
((("someone" "needs" "tiger" "+")) -> ("tiger" "likes" "mouse" "+"))
The tiger is big.
True
1
proof
[(triple8)]
("tiger" "is" "big" "+")
triple8
The tiger is not young.
False
1
inv-proof
[(triple12)]
("tiger" "is" "young" "-")
triple12
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
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 does not like the tiger.[(triple5)] The mouse does not see the tiger.[(triple7)] The mouse is big.[(triple1)] The mouse is nice.[(triple2)] The mouse is not rough.[(triple3)] The mouse is young.[(triple4)] The mouse needs the tiger.[(triple6)] The tiger is big.[(triple8)] The tiger is not nice.[(triple9)] The tiger is red.[(triple10)] The tiger is rough.[(triple11)] The tiger is young.[(triple12)] The tiger likes the mouse.[(triple13 OR ((triple6) -> rule1))] The tiger needs the mouse.[(triple14)] The tiger sees the mouse.[(triple15)]
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
triple5
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse is not rough.
("mouse" "is" "rough" "-")
triple3
The mouse is young.
("mouse" "is" "young" "+")
triple4
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger is not nice.
("tiger" "is" "nice" "-")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger is young.
("tiger" "is" "young" "+")
triple12
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple13
((triple6) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15