The bear is round. The mouse sees the bear. The rabbit is kind. All round people are not young. If someone is big then they need the mouse. If someone sees the mouse then they see the rabbit. If someone needs the rabbit and the rabbit is blue then they are not big. All blue people are big. If the rabbit is not big then the rabbit is young. If the rabbit is big and the rabbit is kind then the rabbit is young. If the bear does not visit the mouse and the bear does not need the mouse then the bear visits the rabbit.
The bear is round.
("bear" "is" "round" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
All round people are not young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "-"))
If someone is big then they need the mouse.
((("someone" "is" "big" "+")) -> ("someone" "needs" "mouse" "+"))
If someone sees the mouse then they see the rabbit.
((("someone" "sees" "mouse" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone needs the rabbit and the rabbit is blue then they are not big.
((("someone" "needs" "rabbit" "+") ("rabbit" "is" "blue" "+")) -> ("someone" "is" "big" "-"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If the rabbit is not big then the rabbit is young.
((("rabbit" "is" "big" "~")) -> ("rabbit" "is" "young" "+"))
If the rabbit is big and the rabbit is kind then the rabbit is young.
((("rabbit" "is" "big" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "young" "+"))
If the bear does not visit the mouse and the bear does not need the mouse then the bear visits the rabbit.
((("bear" "visits" "mouse" "~") ("bear" "needs" "mouse" "~")) -> ("bear" "visits" "rabbit" "+"))
The bear is round.
True
1
proof
[(triple1)]
("bear" "is" "round" "+")
triple1
The bear is not round.
False
1
inv-proof
[(triple1)]
("bear" "is" "round" "-")
triple1
The bear is not young.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "young" "-")
((triple1) -> (rule1 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The bear is young.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "young" "+")
((triple1) -> (rule1 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "big" "-")
The mouse sees the rabbit.
Unknown
rconc
[@1: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "rabbit" "+")
The rabbit does not need the bear.
Unknown
inv-random
[@0: The rabbit needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bear" "-")
The bear sees the mouse.
Unknown
random
[@0: The bear sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "mouse" "+")
@0: The bear is round.[(triple1)] The mouse sees the bear.[(triple2)] The rabbit is kind.[(triple3)] @1: The bear is not young.[(((triple1) -> rule1))]
The bear is round.
("bear" "is" "round" "+")
triple1
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The bear is not young.
("bear" "is" "young" "-")
((triple1) -> (rule1 % int1))
The bear is not young.
("bear" "is" "young" "-")
int1