The bear likes the cow. The cow is nice. If someone sees the bear then they see the cow. If the bear chases the cow then the bear likes the cow. If someone is blue and they like the cow then the cow likes the bear. If someone chases the cow then they see the bear. If the bear chases the cow and the bear likes the cow then the cow is nice. If someone is cold and they like the cow then they like the bear. If someone is blue then they like the cow. If someone likes the cow then they chase the cow.
The bear likes the cow.
("bear" "likes" "cow" "+")
The cow is nice.
("cow" "is" "nice" "+")
If someone sees the bear then they see the cow.
((("someone" "sees" "bear" "+")) -> ("someone" "sees" "cow" "+"))
If the bear chases the cow then the bear likes the cow.
((("bear" "chases" "cow" "+")) -> ("bear" "likes" "cow" "+"))
If someone is blue and they like the cow then the cow likes the bear.
((("someone" "is" "blue" "+") ("someone" "likes" "cow" "+")) -> ("cow" "likes" "bear" "+"))
If someone chases the cow then they see the bear.
((("someone" "chases" "cow" "+")) -> ("someone" "sees" "bear" "+"))
If the bear chases the cow and the bear likes the cow then the cow is nice.
((("bear" "chases" "cow" "+") ("bear" "likes" "cow" "+")) -> ("cow" "is" "nice" "+"))
If someone is cold and they like the cow then they like the bear.
((("someone" "is" "cold" "+") ("someone" "likes" "cow" "+")) -> ("someone" "likes" "bear" "+"))
If someone is blue then they like the cow.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow then they chase the cow.
((("someone" "likes" "cow" "+")) -> ("someone" "chases" "cow" "+"))
The cow is nice.
True
1
proof
[(triple2 OR ((((triple1) -> rule8) triple1) -> rule5))]
("cow" "is" "nice" "+")
triple2
((((triple1) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The cow is not nice.
False
1
inv-proof
[(triple2 OR ((((triple1) -> rule8) triple1) -> rule5))]
("cow" "is" "nice" "-")
triple2
((((triple1) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear chases the cow.
True
2
proof
[(((triple1) -> rule8))]
("bear" "chases" "cow" "+")
((triple1) -> (rule8 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear does not chase the cow.
False
2
inv-proof
[(((triple1) -> rule8))]
("bear" "chases" "cow" "-")
((triple1) -> (rule8 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear sees the bear.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("bear" "sees" "bear" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear does not see the bear.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("bear" "sees" "bear" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear sees the cow.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule1))]
("bear" "sees" "cow" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
The bear does not see the cow.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule1))]
("bear" "sees" "cow" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3
The cow does not see the bear.
Unknown
inv-rconc
[@3: The cow sees the bear.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule7 <- FAIL)]]
("cow" "sees" "bear" "-")
The cow likes the cow.
Unknown
rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "likes" "cow" "+")
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "bear" "-")
The cow likes the bear.
Unknown
rconc
[@1: The cow likes the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "bear" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
The cow does not chase the bear.
Unknown
inv-random
[@0: The cow chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "bear" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The bear likes the cow.[(triple1)] The cow is nice.[(triple2 OR ((((triple1) -> rule8) triple1) -> rule5))] @1: The bear chases the cow.[(((triple1) -> rule8))] @2: The bear sees the bear.[(((((triple1) -> rule8)) -> rule4))] @3: The bear sees the cow.[(((((((triple1) -> rule8)) -> rule4)) -> rule1))]
The bear likes the cow.
("bear" "likes" "cow" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
((((triple1) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
((triple1) -> (rule8 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear sees the cow.
("bear" "sees" "cow" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear chases the cow.
("bear" "chases" "cow" "+")
int3