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