The bear is round. The cow eats the mouse. The mouse likes the cow. If something chases the bear and the bear chases the cow then it is rough. If something chases the mouse then it is nice. All rough things are nice. If something is round then it chases the cow. If the mouse is green then the mouse does not eat the cow. If the bear is round and the bear chases the cow then the bear chases the mouse.
The bear is round.
("bear" "is" "round" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If something chases the bear and the bear chases the cow then it is rough.
((("something" "chases" "bear" "+") ("bear" "chases" "cow" "+")) -> ("something" "is" "rough" "+"))
If something chases the mouse then it is nice.
((("something" "chases" "mouse" "+")) -> ("something" "is" "nice" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is round then it chases the cow.
((("something" "is" "round" "+")) -> ("something" "chases" "cow" "+"))
If the mouse is green then the mouse does not eat the cow.
((("mouse" "is" "green" "+")) -> ("mouse" "eats" "cow" "-"))
If the bear is round and the bear chases the cow then the bear chases the mouse.
((("bear" "is" "round" "+") ("bear" "chases" "cow" "+")) -> ("bear" "chases" "mouse" "+"))
The cow eats the mouse.
True
1
proof
[(triple2)]
("cow" "eats" "mouse" "+")
triple2
The cow does not eat the mouse.
False
1
inv-proof
[(triple2)]
("cow" "eats" "mouse" "-")
triple2
The bear chases the cow.
True
2
proof
[(((triple1) -> rule4))]
("bear" "chases" "cow" "+")
((triple1) -> (rule4 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear does not chase the cow.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "chases" "cow" "-")
((triple1) -> (rule4 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear chases the mouse.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("bear" "chases" "mouse" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear does not chase the mouse.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule6))]
("bear" "chases" "mouse" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear is nice.
True
5
proof
[(((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule2))]
("bear" "is" "nice" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
The bear is not nice.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule2))]
("bear" "is" "nice" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "rough" "-")
The cow is nice.
Unknown
rconc
[@2: The cow is nice.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("cow" "is" "nice" "+")
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "rough" "-")
The mouse chases the cow.
Unknown
rconc
[@1: The mouse chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "cow" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The cow does not like the bear.
Unknown
inv-random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "-")
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 is round.[(triple1)] The cow eats the mouse.[(triple2)] The mouse likes the cow.[(triple3)] @1: The bear chases the cow.[(((triple1) -> rule4))] @2: The bear chases the mouse.[(((triple1 ((triple1) -> rule4)) -> rule6))] @3: The bear is nice.[(((((triple1 ((triple1) -> rule4)) -> rule6)) -> rule2))]
The bear is round.
("bear" "is" "round" "+")
triple1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple3
The bear chases the cow.
("bear" "chases" "cow" "+")
((triple1) -> (rule4 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3