The mouse is big. The mouse is kind. The mouse is nice. The mouse is rough. The mouse is round. The mouse needs the tiger. The mouse sees the tiger. The mouse visits the tiger. The tiger is big. The tiger is kind. The tiger needs the mouse. The tiger visits the mouse. If something needs the mouse and it sees the mouse then it visits the mouse. If something needs the mouse then it visits the tiger.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something needs the mouse and it sees the mouse then it visits the mouse.
((("something" "needs" "mouse" "+") ("something" "sees" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something needs the mouse then it visits the tiger.
((("something" "needs" "mouse" "+")) -> ("something" "visits" "tiger" "+"))
The mouse is round.
True
1
proof
[(triple5)]
("mouse" "is" "round" "+")
triple5
The tiger is not big.
False
1
inv-proof
[(triple9)]
("tiger" "is" "big" "-")
triple9
The tiger visits the tiger.
True
2
proof
[(((triple11) -> rule2))]
("tiger" "visits" "tiger" "+")
((triple11) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple11) -> rule2))]
("tiger" "visits" "tiger" "-")
((triple11) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
@0: The mouse is big.[(triple1)] The mouse is kind.[(triple2)] The mouse is nice.[(triple3)] The mouse is rough.[(triple4)] The mouse is round.[(triple5)] The mouse needs the tiger.[(triple6)] The mouse sees the tiger.[(triple7)] The mouse visits the tiger.[(triple8)] The tiger is big.[(triple9)] The tiger is kind.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger visits the mouse.[(triple12)] @1: The tiger visits the tiger.[(((triple11) -> rule2))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple12
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple11) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1