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