The mouse eats the tiger. The mouse is not big. The mouse is not green. The mouse is rough. The mouse is round. The mouse is young. The mouse likes the tiger. The mouse sees the tiger. The tiger does not eat the mouse. The tiger is big. The tiger is green. The tiger is rough. The tiger is young. The tiger does not like the mouse. The tiger sees the mouse. If something sees the mouse then it does not see the tiger.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something sees the mouse then it does not see the tiger.
((("something" "sees" "mouse" "+")) -> ("something" "sees" "tiger" "-"))
The mouse sees the tiger.
True
1
proof
[(triple8)]
("mouse" "sees" "tiger" "+")
triple8
The mouse is green.
False
1
inv-proof
[(triple3)]
("mouse" "is" "green" "+")
triple3
The tiger does not see the tiger.
True
2
proof
[(((triple15) -> rule1))]
("tiger" "sees" "tiger" "-")
((triple15) -> (rule1 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The tiger sees the tiger.
False
2
inv-proof
[(((triple15) -> rule1))]
("tiger" "sees" "tiger" "+")
((triple15) -> (rule1 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse eats the tiger.[(triple1)] The mouse is not big.[(triple2)] The mouse is not green.[(triple3)] The mouse is rough.[(triple4)] The mouse is round.[(triple5)] The mouse is young.[(triple6)] The mouse likes the tiger.[(triple7)] The mouse sees the tiger.[(triple8)] The tiger does not eat the mouse.[(triple9)] The tiger does not like the mouse.[(triple14)] The tiger is big.[(triple10)] The tiger is green.[(triple11)] The tiger is rough.[(triple12)] The tiger is young.[(triple13)] The tiger sees the mouse.[(triple15)] @1: The tiger does not see the tiger.[(((triple15) -> rule1))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
The mouse is not big.
("mouse" "is" "big" "-")
triple2
The mouse is not green.
("mouse" "is" "green" "-")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple7
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple8
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
triple9
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
triple14
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
((triple15) -> (rule1 % int1))
The tiger does not see the tiger.
("tiger" "sees" "tiger" "-")
int1