The bear visits the mouse. The mouse likes the bear. If the bear visits the mouse then the mouse is big. If the bear visits the mouse and the mouse is not big then the bear does not see the mouse. If something sees the mouse then it visits the bear. If something is big then it visits the bear. If the bear does not see the mouse then the mouse visits the bear. If something is big and it likes the mouse then it likes the bear. If the mouse visits the bear and the bear is red then the bear likes the mouse. If the mouse visits the bear then the bear likes the mouse.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If the bear visits the mouse then the mouse is big.
((("bear" "visits" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If the bear visits the mouse and the mouse is not big then the bear does not see the mouse.
((("bear" "visits" "mouse" "+") ("mouse" "is" "big" "~")) -> ("bear" "sees" "mouse" "-"))
If something sees the mouse then it visits the bear.
((("something" "sees" "mouse" "+")) -> ("something" "visits" "bear" "+"))
If something is big then it visits the bear.
((("something" "is" "big" "+")) -> ("something" "visits" "bear" "+"))
If the bear does not see the mouse then the mouse visits the bear.
((("bear" "sees" "mouse" "~")) -> ("mouse" "visits" "bear" "+"))
If something is big and it likes the mouse then it likes the bear.
((("something" "is" "big" "+") ("something" "likes" "mouse" "+")) -> ("something" "likes" "bear" "+"))
If the mouse visits the bear and the bear is red then the bear likes the mouse.
((("mouse" "visits" "bear" "+") ("bear" "is" "red" "+")) -> ("bear" "likes" "mouse" "+"))
If the mouse visits the bear then the bear likes the mouse.
((("mouse" "visits" "bear" "+")) -> ("bear" "likes" "mouse" "+"))
The mouse likes the bear.
True
1
proof
[(triple2)]
("mouse" "likes" "bear" "+")
triple2
The bear does not visit the mouse.
False
1
inv-proof
[(triple1)]
("bear" "visits" "mouse" "-")
triple1
The mouse is big.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "is" "big" "+")
((triple1) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "is" "big" "-")
((triple1) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse visits the bear.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("mouse" "visits" "bear" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse does not visit the bear.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("mouse" "visits" "bear" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The bear likes the mouse.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule8))]
("bear" "likes" "mouse" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The bear does not like the mouse.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule8))]
("bear" "likes" "mouse" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "bear" "-")
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 cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
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 visits the mouse.[(triple1)] The mouse likes the bear.[(triple2)] @1: The mouse is big.[(((triple1) -> rule1))] @2: The mouse visits the bear.[(((((triple1) -> rule1)) -> rule4))] @3: The bear likes the mouse.[(((((((triple1) -> rule1)) -> rule4)) -> rule8))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
((triple1) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3