The bear eats the mouse. The mouse is big. The rabbit is big. If something is kind then it does not visit the mouse. Big things are kind. If something visits the mouse then the mouse visits the rabbit. If the rabbit does not chase the bear then the bear does not visit the mouse. If something is young then it chases the mouse. If something is kind and it does not visit the bear then the bear eats the rabbit.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
If something is kind then it does not visit the mouse.
((("something" "is" "kind" "+")) -> ("something" "visits" "mouse" "-"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something visits the mouse then the mouse visits the rabbit.
((("something" "visits" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If the rabbit does not chase the bear then the bear does not visit the mouse.
((("rabbit" "chases" "bear" "~")) -> ("bear" "visits" "mouse" "-"))
If something is young then it chases the mouse.
((("something" "is" "young" "+")) -> ("something" "chases" "mouse" "+"))
If something is kind and it does not visit the bear then the bear eats the rabbit.
((("something" "is" "kind" "+") ("something" "visits" "bear" "~")) -> ("bear" "eats" "rabbit" "+"))
The bear eats the mouse.
True
1
proof
[(triple1)]
("bear" "eats" "mouse" "+")
triple1
The bear does not eat the mouse.
False
1
inv-proof
[(triple1)]
("bear" "eats" "mouse" "-")
triple1
The rabbit is kind.
True
2
proof
[(((triple3) -> rule2))]
("rabbit" "is" "kind" "+")
((triple3) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("rabbit" "is" "kind" "-")
((triple3) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit does not visit the mouse.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("rabbit" "visits" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit visits the mouse.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("rabbit" "visits" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "kind" "-")
The bear chases the mouse.
Unknown
rconc
[@1: The bear chases the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "chases" "mouse" "+")
The mouse does not visit the rabbit.
Unknown
inv-rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "rabbit" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The mouse does not chase the rabbit.
Unknown
inv-random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "-")
The rabbit eats the mouse.
Unknown
random
[@0: The rabbit eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "mouse" "+")
@0: The bear eats the mouse.[(triple1)] The mouse is big.[(triple2)] The rabbit is big.[(triple3)] @1: The mouse is kind.[(((triple2) -> rule2))] The rabbit is kind.[(((triple3) -> rule2))] @2: The mouse does not visit the mouse.[(((((triple2) -> rule2)) -> rule1))] The rabbit does not visit the mouse.[(((((triple3) -> rule2)) -> rule1))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple3) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2