The bear is big. The mouse eats the bear. The mouse visits the bear. If the mouse is round and the mouse sees the bear then the bear visits the mouse. If someone visits the bear then the bear visits the mouse. If someone sees the bear then they are not big. If someone visits the mouse then they see the mouse. If someone sees the mouse then the mouse is not rough. If someone is red then they eat the mouse. If someone visits the mouse and they eat the bear then the bear is round. If the bear visits the mouse and the mouse does not eat the bear then the bear is rough.
The bear is big.
("bear" "is" "big" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If the mouse is round and the mouse sees the bear then the bear visits the mouse.
((("mouse" "is" "round" "+") ("mouse" "sees" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If someone visits the bear then the bear visits the mouse.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If someone sees the bear then they are not big.
((("someone" "sees" "bear" "+")) -> ("someone" "is" "big" "-"))
If someone visits the mouse then they see the mouse.
((("someone" "visits" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse then the mouse is not rough.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "rough" "-"))
If someone is red then they eat the mouse.
((("someone" "is" "red" "+")) -> ("someone" "eats" "mouse" "+"))
If someone visits the mouse and they eat the bear then the bear is round.
((("someone" "visits" "mouse" "+") ("someone" "eats" "bear" "+")) -> ("bear" "is" "round" "+"))
If the bear visits the mouse and the mouse does not eat the bear then the bear is rough.
((("bear" "visits" "mouse" "+") ("mouse" "eats" "bear" "~")) -> ("bear" "is" "rough" "+"))
The mouse visits the bear.
True
1
proof
[(triple3)]
("mouse" "visits" "bear" "+")
triple3
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The bear visits the mouse.
True
2
proof
[(((triple3) -> rule2))]
("bear" "visits" "mouse" "+")
((triple3) -> (rule2 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The bear does not visit the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("bear" "visits" "mouse" "-")
((triple3) -> (rule2 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The bear sees the mouse.
True
3
proof
[(((((triple3) -> rule2)) -> rule4))]
("bear" "sees" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The bear does not see the mouse.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule4))]
("bear" "sees" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse is not rough.
True
4
proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule5))]
("mouse" "is" "rough" "-")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3
The mouse is rough.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule5))]
("mouse" "is" "rough" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "rough" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The bear eats the mouse.
Unknown
rconc
[@1: The bear eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "mouse" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The bear is big.[(triple1)] The mouse eats the bear.[(triple2)] The mouse visits the bear.[(triple3)] @1: The bear visits the mouse.[(((triple3) -> rule2))] @2: The bear sees the mouse.[(((((triple3) -> rule2)) -> rule4))] @3: The mouse is not rough.[(((((((triple3) -> rule2)) -> rule4)) -> rule5))]
The bear is big.
("bear" "is" "big" "+")
triple1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple3
The bear visits the mouse.
("bear" "visits" "mouse" "+")
((triple3) -> (rule2 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse is not rough.
("mouse" "is" "rough" "-")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3