The bear likes the mouse. The bear visits the mouse. The mouse visits the bear. If someone likes the bear then they are round. If someone visits the bear then the bear visits the mouse. If someone visits the mouse and they eat the mouse then they are young. If someone is nice then they like the bear. If someone likes the mouse then the mouse likes the bear. If someone visits the bear then the bear is not nice.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If someone likes the bear then they are round.
((("someone" "likes" "bear" "+")) -> ("someone" "is" "round" "+"))
If someone visits the bear then the bear visits the mouse.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If someone visits the mouse and they eat the mouse then they are young.
((("someone" "visits" "mouse" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they like the bear.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "bear" "+"))
If someone likes the mouse then the mouse likes the bear.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If someone visits the bear then the bear is not nice.
((("someone" "visits" "bear" "+")) -> ("bear" "is" "nice" "-"))
The mouse visits the bear.
True
1
proof
[(triple3)]
("mouse" "visits" "bear" "+")
triple3
The mouse does not visit the bear.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "bear" "-")
triple3
The mouse likes the bear.
True
2
proof
[(((triple1) -> rule5))]
("mouse" "likes" "bear" "+")
((triple1) -> (rule5 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse does not like the bear.
False
2
inv-proof
[(((triple1) -> rule5))]
("mouse" "likes" "bear" "-")
((triple1) -> (rule5 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("mouse" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The mouse is not round.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("mouse" "is" "round" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "bear" "-")
The bear is young.
Unknown
rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "young" "+")
The bear is not round.
Unknown
inv-rconc
[@2: The bear is round.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("bear" "is" "round" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The bear likes the mouse.[(triple1)] The bear visits the mouse.[(triple2 OR ((triple3) -> rule2))] The mouse visits the bear.[(triple3)] @1: The bear is not nice.[(((triple3) -> rule6))] The mouse likes the bear.[(((triple1) -> rule5))] @2: The mouse is round.[(((((triple1) -> rule5)) -> rule1))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple2
((triple3) -> (rule2 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple3
The bear is not nice.
("bear" "is" "nice" "-")
((triple3) -> (rule6 % int1))
The bear is not nice.
("bear" "is" "nice" "-")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((triple1) -> (rule5 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2