The bear eats the cow. The bear sees the cow. The cow eats the bear. The cow is not rough. The cow does not see the bear. The mouse sees the bear. The mouse sees the cow. If something visits the bear and it sees the bear then the bear eats the mouse. If something is rough and not cold then it visits the bear. If something sees the cow then it visits the bear. If something eats the bear and it is cold then it is rough. If something visits the cow then it sees the cow. If the cow visits the mouse and the cow is young then the cow does not see the mouse. If something eats the mouse then the mouse is big. If the mouse does not visit the cow then the cow does not eat the mouse.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is not rough.
("cow" "is" "rough" "-")
The cow does not see the bear.
("cow" "sees" "bear" "-")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something visits the bear and it sees the bear then the bear eats the mouse.
((("something" "visits" "bear" "+") ("something" "sees" "bear" "+")) -> ("bear" "eats" "mouse" "+"))
If something is rough and not cold then it visits the bear.
((("something" "is" "rough" "+") ("something" "is" "cold" "~")) -> ("something" "visits" "bear" "+"))
If something sees the cow then it visits the bear.
((("something" "sees" "cow" "+")) -> ("something" "visits" "bear" "+"))
If something eats the bear and it is cold then it is rough.
((("something" "eats" "bear" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something visits the cow then it sees the cow.
((("something" "visits" "cow" "+")) -> ("something" "sees" "cow" "+"))
If the cow visits the mouse and the cow is young then the cow does not see the mouse.
((("cow" "visits" "mouse" "+") ("cow" "is" "young" "+")) -> ("cow" "sees" "mouse" "-"))
If something eats the mouse then the mouse is big.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If the mouse does not visit the cow then the cow does not eat the mouse.
((("mouse" "visits" "cow" "~")) -> ("cow" "eats" "mouse" "-"))
The bear sees the cow.
True
1
proof
[(triple2)]
("bear" "sees" "cow" "+")
triple2
The mouse does not see the bear.
False
1
inv-proof
[(triple6)]
("mouse" "sees" "bear" "-")
triple6
The mouse visits the bear.
True
2
proof
[(((triple7) -> rule3))]
("mouse" "visits" "bear" "+")
((triple7) -> (rule3 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The mouse does not visit the bear.
False
2
inv-proof
[(((triple7) -> rule3))]
("mouse" "visits" "bear" "-")
((triple7) -> (rule3 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The bear eats the mouse.
True
4
proof
[(((((triple7) -> rule3) triple6) -> rule1))]
("bear" "eats" "mouse" "+")
((((triple7) -> (rule3 % int2)) triple6) -> (rule1 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The bear does not eat the mouse.
False
4
inv-proof
[(((((triple7) -> rule3) triple6) -> rule1))]
("bear" "eats" "mouse" "-")
((((triple7) -> (rule3 % int2)) triple6) -> (rule1 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse is big.
True
5
proof
[(((((((triple7) -> rule3) triple6) -> rule1)) -> rule7))]
("mouse" "is" "big" "+")
((((((triple7) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
The mouse is not big.
False
5
inv-proof
[(((((((triple7) -> rule3) triple6) -> rule1)) -> rule7))]
("mouse" "is" "big" "-")
((((((triple7) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "rough" "-")
The mouse is rough.
Unknown
rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "rough" "+")
The cow does not visit the bear.
Unknown
inv-rconc
[@2: The cow visits the bear.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("cow" "visits" "bear" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "cow" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
@0: The bear eats the cow.[(triple1)] The bear sees the cow.[(triple2)] The cow does not see the bear.[(triple5)] The cow eats the bear.[(triple3)] The cow is not rough.[(triple4)] The mouse sees the bear.[(triple6)] The mouse sees the cow.[(triple7)] @1: The bear visits the bear.[(((triple2) -> rule3))] The mouse visits the bear.[(((triple7) -> rule3))] @2: The bear eats the mouse.[(((((triple7) -> rule3) triple6) -> rule1))] @3: The mouse is big.[(((((((triple7) -> rule3) triple6) -> rule1)) -> rule7))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear sees the cow.
("bear" "sees" "cow" "+")
triple2
The cow does not see the bear.
("cow" "sees" "bear" "-")
triple5
The cow eats the bear.
("cow" "eats" "bear" "+")
triple3
The cow is not rough.
("cow" "is" "rough" "-")
triple4
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple2) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
((triple7) -> (rule3 % int1))
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
((((triple7) -> (rule3 % int2)) triple6) -> (rule1 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((((((triple7) -> (rule3 % int3)) triple6) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
int3