The mouse eats the tiger. The tiger is rough. The tiger needs the mouse. If something visits the tiger then it is rough. If something visits the tiger then the tiger visits the mouse. If something needs the mouse then the mouse visits the tiger. If the mouse needs the tiger then the mouse visits the tiger. If something eats the mouse and the mouse eats the tiger then the tiger needs the mouse. If something visits the mouse and the mouse visits the tiger then the mouse is red.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something visits the tiger then it is rough.
((("something" "visits" "tiger" "+")) -> ("something" "is" "rough" "+"))
If something visits the tiger then the tiger visits the mouse.
((("something" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If something needs the mouse then the mouse visits the tiger.
((("something" "needs" "mouse" "+")) -> ("mouse" "visits" "tiger" "+"))
If the mouse needs the tiger then the mouse visits the tiger.
((("mouse" "needs" "tiger" "+")) -> ("mouse" "visits" "tiger" "+"))
If something eats the mouse and the mouse eats the tiger then the tiger needs the mouse.
((("something" "eats" "mouse" "+") ("mouse" "eats" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
If something visits the mouse and the mouse visits the tiger then the mouse is red.
((("something" "visits" "mouse" "+") ("mouse" "visits" "tiger" "+")) -> ("mouse" "is" "red" "+"))
The tiger needs the mouse.
True
1
proof
[(triple3)]
("tiger" "needs" "mouse" "+")
triple3
The tiger does not need the mouse.
False
1
inv-proof
[(triple3)]
("tiger" "needs" "mouse" "-")
triple3
The mouse visits the tiger.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "visits" "tiger" "-")
((triple3) -> (rule3 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("mouse" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("mouse" "is" "rough" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is red.
True
6
proof
[(((((((triple3) -> rule3)) -> rule2) ((triple3) -> rule3)) -> rule6))]
("mouse" "is" "red" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int3))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The mouse is not red.
False
6
inv-proof
[(((((((triple3) -> rule3)) -> rule2) ((triple3) -> rule3)) -> rule6))]
("mouse" "is" "red" "-")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int3))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse needs the tiger.
Unknown
random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "+")
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 mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The mouse eats the tiger.[(triple1)] The tiger is rough.[(triple2)] The tiger needs the mouse.[(triple3)] @1: The mouse visits the tiger.[(((triple3) -> rule3))] @2: The mouse is rough.[(((((triple3) -> rule3)) -> rule1))] The tiger visits the mouse.[(((((triple3) -> rule3)) -> rule2))] @3: The mouse is red.[(((((((triple3) -> rule3)) -> rule2) ((triple3) -> rule3)) -> rule6))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
The tiger is rough.
("tiger" "is" "rough" "+")
triple2
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((triple3) -> (rule3 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int3))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int3