The bear is young. The mouse is nice. The mouse is young. If someone is nice then they need the bear. If someone needs the bear then they do not visit the bear. If someone needs the bear then they visit the mouse.
The bear is young.
("bear" "is" "young" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone is nice then they need the bear.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "bear" "+"))
If someone needs the bear then they do not visit the bear.
((("someone" "needs" "bear" "+")) -> ("someone" "visits" "bear" "-"))
If someone needs the bear then they visit the mouse.
((("someone" "needs" "bear" "+")) -> ("someone" "visits" "mouse" "+"))
The bear is young.
True
1
proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The mouse is not nice.
False
1
inv-proof
[(triple2)]
("mouse" "is" "nice" "-")
triple2
The mouse needs the bear.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "needs" "bear" "+")
((triple2) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not need the bear.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "needs" "bear" "-")
((triple2) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse visits the mouse.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("mouse" "visits" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse visits the bear.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("mouse" "visits" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear visits the mouse.
Unknown
rconc
[@2: The bear visits the mouse.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("bear" "visits" "mouse" "+")
The bear does not need the mouse.
Unknown
inv-random
[@0: The bear needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "mouse" "-")
The bear eats the mouse.
Unknown
random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear is young.[(triple1)] The mouse is nice.[(triple2)] The mouse is young.[(triple3)] @1: The mouse needs the bear.[(((triple2) -> rule1))] @2: The mouse does not visit the bear.[(((((triple2) -> rule1)) -> rule2))] The mouse visits the mouse.[(((((triple2) -> rule1)) -> rule3))]
The bear is young.
("bear" "is" "young" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple2) -> (rule1 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not visit the bear.
("mouse" "visits" "bear" "-")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2