The mouse sees the tiger. The tiger is blue. The tiger is young. If someone needs the mouse then the mouse needs the tiger. If the mouse sees the tiger and the tiger is young then the mouse needs the tiger. If someone visits the mouse then they are big. If someone visits the mouse then they see the tiger. If someone sees the mouse then they visit the mouse. If someone needs the tiger then the tiger visits the mouse.
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is young.
("tiger" "is" "young" "+")
If someone needs the mouse then the mouse needs the tiger.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If the mouse sees the tiger and the tiger is young then the mouse needs the tiger.
((("mouse" "sees" "tiger" "+") ("tiger" "is" "young" "+")) -> ("mouse" "needs" "tiger" "+"))
If someone visits the mouse then they are big.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "big" "+"))
If someone visits the mouse then they see the tiger.
((("someone" "visits" "mouse" "+")) -> ("someone" "sees" "tiger" "+"))
If someone sees the mouse then they visit the mouse.
((("someone" "sees" "mouse" "+")) -> ("someone" "visits" "mouse" "+"))
If someone needs the tiger then the tiger visits the mouse.
((("someone" "needs" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
The mouse sees the tiger.
True
1
proof
[(triple1)]
("mouse" "sees" "tiger" "+")
triple1
The mouse does not see the tiger.
False
1
inv-proof
[(triple1)]
("mouse" "sees" "tiger" "-")
triple1
The mouse needs the tiger.
True
3
proof
[(((triple1 triple3) -> rule2))]
("mouse" "needs" "tiger" "+")
((triple1 triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse does not need the tiger.
False
3
inv-proof
[(((triple1 triple3) -> rule2))]
("mouse" "needs" "tiger" "-")
((triple1 triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The tiger visits the mouse.
True
4
proof
[(((((triple1 triple3) -> rule2)) -> rule6))]
("tiger" "visits" "mouse" "+")
((((triple1 triple3) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The tiger does not visit the mouse.
False
4
inv-proof
[(((((triple1 triple3) -> rule2)) -> rule6))]
("tiger" "visits" "mouse" "-")
((((triple1 triple3) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The tiger sees the tiger.
True
5
proof
[(((((((triple1 triple3) -> rule2)) -> rule6)) -> rule4))]
("tiger" "sees" "tiger" "+")
((((((triple1 triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
The tiger does not see the tiger.
False
5
inv-proof
[(((((((triple1 triple3) -> rule2)) -> rule6)) -> rule4))]
("tiger" "sees" "tiger" "-")
((((((triple1 triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
The mouse is not big.
Unknown
inv-rconc
[@2: The mouse is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
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 needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The mouse sees the tiger.[(triple1)] The tiger is blue.[(triple2)] The tiger is young.[(triple3)] @1: The mouse needs the tiger.[(((triple1 triple3) -> rule2))] @2: The tiger visits the mouse.[(((((triple1 triple3) -> rule2)) -> rule6))] @3: The tiger is big.[(((((((triple1 triple3) -> rule2)) -> rule6)) -> rule3))] The tiger sees the tiger.[(((((((triple1 triple3) -> rule2)) -> rule6)) -> rule4))]
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple1 triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((((triple1 triple3) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((((triple1 triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((triple1 triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int3