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