The bear visits the cow. The cow is blue. If something is round and it eats the bear then the bear does not see the cow. If something is blue and it does not eat the bear then the bear does not eat the cow. If something eats the bear and the bear eats the cow then it sees the cow. If the cow sees the bear then the bear does not visit the cow. If something visits the bear and the bear does not visit the cow then it is green. If something visits the cow then the cow does not visit the bear. If the bear is nice and the bear does not visit the cow then the cow visits the bear. Green things are rough.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
If something is round and it eats the bear then the bear does not see the cow.
((("something" "is" "round" "+") ("something" "eats" "bear" "+")) -> ("bear" "sees" "cow" "-"))
If something is blue and it does not eat the bear then the bear does not eat the cow.
((("something" "is" "blue" "+") ("something" "eats" "bear" "~")) -> ("bear" "eats" "cow" "-"))
If something eats the bear and the bear eats the cow then it sees the cow.
((("something" "eats" "bear" "+") ("bear" "eats" "cow" "+")) -> ("something" "sees" "cow" "+"))
If the cow sees the bear then the bear does not visit the cow.
((("cow" "sees" "bear" "+")) -> ("bear" "visits" "cow" "-"))
If something visits the bear and the bear does not visit the cow then it is green.
((("something" "visits" "bear" "+") ("bear" "visits" "cow" "~")) -> ("something" "is" "green" "+"))
If something visits the cow then the cow does not visit the bear.
((("something" "visits" "cow" "+")) -> ("cow" "visits" "bear" "-"))
If the bear is nice and the bear does not visit the cow then the cow visits the bear.
((("bear" "is" "nice" "+") ("bear" "visits" "cow" "~")) -> ("cow" "visits" "bear" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
The cow is blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "+")
triple2
The cow is not blue.
False
1
inv-proof
[(triple2)]
("cow" "is" "blue" "-")
triple2
The cow does not visit the bear.
True
2
proof
[(((triple1) -> rule6))]
("cow" "visits" "bear" "-")
((triple1) -> (rule6 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1
The cow visits the bear.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "visits" "bear" "+")
((triple1) -> (rule6 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1
The cow is not rough.
Unknown
inv-rconc
[@2: The cow is rough.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("cow" "is" "rough" "-")
The bear sees the cow.
Unknown
rconc
[@1: The bear sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "cow" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear visits the cow.[(triple1)] The cow is blue.[(triple2)] @1: The cow does not visit the bear.[(((triple1) -> rule6))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow does not visit the bear.
("cow" "visits" "bear" "-")
((triple1) -> (rule6 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1