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