The mouse chases the tiger. The mouse is green. The mouse is kind. The mouse is rough. The mouse needs the tiger. The mouse sees the tiger. The tiger is kind. If the tiger needs the mouse then the mouse is round. If something needs the tiger then the tiger needs the mouse.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If the tiger needs the mouse then the mouse is round.
((("tiger" "needs" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something needs the tiger then the tiger needs the mouse.
((("something" "needs" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
The mouse is kind.
True
1
proof
[(triple3)]
("mouse" "is" "kind" "+")
triple3
The mouse is not kind.
False
1
inv-proof
[(triple3)]
("mouse" "is" "kind" "-")
triple3
The tiger needs the mouse.
True
2
proof
[(((triple5) -> rule2))]
("tiger" "needs" "mouse" "+")
((triple5) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The tiger does not need the mouse.
False
2
inv-proof
[(((triple5) -> rule2))]
("tiger" "needs" "mouse" "-")
((triple5) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse is round.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("mouse" "is" "round" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The mouse is not round.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("mouse" "is" "round" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger does not chase the mouse.
Unknown
inv-random
[@0: The tiger chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "mouse" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse is green.[(triple2)] The mouse is kind.[(triple3)] The mouse is rough.[(triple4)] The mouse needs the tiger.[(triple5)] The mouse sees the tiger.[(triple6)] The tiger is kind.[(triple7)] @1: The tiger needs the mouse.[(((triple5) -> rule2))] @2: The mouse is round.[(((((triple5) -> rule2)) -> rule1))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple5
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
((triple5) -> (rule2 % int1))
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
int2