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