The bear eats the cow. The cow chases the bear. If something chases the bear then it is blue. If the cow is blue then the cow needs the bear. If something chases the bear then it needs the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
If something chases the bear then it is blue.
((("something" "chases" "bear" "+")) -> ("something" "is" "blue" "+"))
If the cow is blue then the cow needs the bear.
((("cow" "is" "blue" "+")) -> ("cow" "needs" "bear" "+"))
If something chases the bear then it needs the cow.
((("something" "chases" "bear" "+")) -> ("something" "needs" "cow" "+"))
The bear eats the cow.
True
1
proof
[(triple1)]
("bear" "eats" "cow" "+")
triple1
The cow does not chase the bear.
False
1
inv-proof
[(triple2)]
("cow" "chases" "bear" "-")
triple2
The cow is blue.
True
2
proof
[(((triple2) -> rule1))]
("cow" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "is" "blue" "-")
((triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the bear.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("cow" "needs" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow does not need the bear.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("cow" "needs" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The bear does not need the cow.
Unknown
inv-rconc
[@1: The bear needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "cow" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "blue" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The cow eats the bear.
Unknown
random
[@0: The cow eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bear" "+")
@0: The bear eats the cow.[(triple1)] The cow chases the bear.[(triple2)] @1: The cow is blue.[(((triple2) -> rule1))] The cow needs the cow.[(((triple2) -> rule3))] @2: The cow needs the bear.[(((((triple2) -> rule1)) -> rule2))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The cow chases the bear.
("cow" "chases" "bear" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2