The bear is kind. The cow chases the bear. If something chases the bear then it chases the cow. If something sees the bear then the bear does not chase the cow. If something is blue and it eats the bear then the bear chases the cow. If something eats the bear then the bear eats the cow. If the bear chases the cow then the cow does not see the bear. If something sees the cow then it is kind. If something sees the cow and the cow chases the bear then the bear is not blue. If something chases the cow then it is cold.
The bear is kind.
("bear" "is" "kind" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
If something chases the bear then it chases the cow.
((("something" "chases" "bear" "+")) -> ("something" "chases" "cow" "+"))
If something sees the bear then the bear does not chase the cow.
((("something" "sees" "bear" "+")) -> ("bear" "chases" "cow" "-"))
If something is blue and it eats the bear then the bear chases the cow.
((("something" "is" "blue" "+") ("something" "eats" "bear" "+")) -> ("bear" "chases" "cow" "+"))
If something eats the bear then the bear eats the cow.
((("something" "eats" "bear" "+")) -> ("bear" "eats" "cow" "+"))
If the bear chases the cow then the cow does not see the bear.
((("bear" "chases" "cow" "+")) -> ("cow" "sees" "bear" "-"))
If something sees the cow then it is kind.
((("something" "sees" "cow" "+")) -> ("something" "is" "kind" "+"))
If something sees the cow and the cow chases the bear then the bear is not blue.
((("something" "sees" "cow" "+") ("cow" "chases" "bear" "+")) -> ("bear" "is" "blue" "-"))
If something chases the cow then it is cold.
((("something" "chases" "cow" "+")) -> ("something" "is" "cold" "+"))
The cow chases the bear.
True
1
proof
[(triple2)]
("cow" "chases" "bear" "+")
triple2
The bear is not kind.
False
1
inv-proof
[(triple1)]
("bear" "is" "kind" "-")
triple1
The cow chases the cow.
True
2
proof
[(((triple2) -> rule1))]
("cow" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "chases" "cow" "-")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The bear does not eat the cow.
Unknown
inv-rconc
[@1: The bear eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "eats" "cow" "-")
The bear chases the cow.
Unknown
rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "cow" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is kind.[(triple1)] The cow chases the bear.[(triple2)] @1: The cow chases the cow.[(((triple2) -> rule1))] @2: The cow is cold.[(((((triple2) -> rule1)) -> rule8))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The cow chases the bear.
("cow" "chases" "bear" "+")
triple2
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2