The bear chases the cow. The bear is round. The bear needs the cow. The bear does not see the cow. The cow chases the bear. The cow is cold. The cow is kind. The cow is round. The cow needs the bear. The cow does not see the bear. If the bear needs the cow and the cow is not red then the bear chases the cow. If something chases the bear and it is cold then the bear chases the cow. If something sees the cow and it needs the bear then it does not chase the cow. If something is cold then it sees the cow. If something needs the bear then the bear is not red. If something chases the cow and the cow is red then it needs the bear.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear does not see the cow.
("bear" "sees" "cow" "-")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow does not see the bear.
("cow" "sees" "bear" "-")
If the bear needs the cow and the cow is not red then the bear chases the cow.
((("bear" "needs" "cow" "+") ("cow" "is" "red" "~")) -> ("bear" "chases" "cow" "+"))
If something chases the bear and it is cold then the bear chases the cow.
((("something" "chases" "bear" "+") ("something" "is" "cold" "+")) -> ("bear" "chases" "cow" "+"))
If something sees the cow and it needs the bear then it does not chase the cow.
((("something" "sees" "cow" "+") ("something" "needs" "bear" "+")) -> ("something" "chases" "cow" "-"))
If something is cold then it sees the cow.
((("something" "is" "cold" "+")) -> ("something" "sees" "cow" "+"))
If something needs the bear then the bear is not red.
((("something" "needs" "bear" "+")) -> ("bear" "is" "red" "-"))
If something chases the cow and the cow is red then it needs the bear.
((("something" "chases" "cow" "+") ("cow" "is" "red" "+")) -> ("something" "needs" "bear" "+"))
The bear chases the cow.
True
1
proof
[(triple1 OR ((triple5 triple6) -> rule2))]
("bear" "chases" "cow" "+")
triple1
((triple5 triple6) -> (rule2 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear does not chase the cow.
False
1
inv-proof
[(triple1 OR ((triple5 triple6) -> rule2))]
("bear" "chases" "cow" "-")
triple1
((triple5 triple6) -> (rule2 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear is not red.
True
2
proof
[(((triple9) -> rule5))]
("bear" "is" "red" "-")
((triple9) -> (rule5 % int1))
The bear is not red.
("bear" "is" "red" "-")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple6) -> rule4))]
("cow" "sees" "cow" "-")
((triple6) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not chase the cow.
True
4
proof
[(((((triple6) -> rule4) triple9) -> rule3))]
("cow" "chases" "cow" "-")
((((triple6) -> (rule4 % int2)) triple9) -> (rule3 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow chases the cow.
False
4
inv-proof
[(((((triple6) -> rule4) triple9) -> rule3))]
("cow" "chases" "cow" "+")
((((triple6) -> (rule4 % int2)) triple9) -> (rule3 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The bear chases the cow.[(triple1 OR ((triple5 triple6) -> rule2))] The bear does not see the cow.[(triple4)] The bear is round.[(triple2)] The bear needs the cow.[(triple3)] The cow chases the bear.[(triple5)] The cow does not see the bear.[(triple10)] The cow is cold.[(triple6)] The cow is kind.[(triple7)] The cow is round.[(triple8)] The cow needs the bear.[(triple9)] @1: The bear is not red.[(((triple9) -> rule5))] The cow sees the cow.[(((triple6) -> rule4))] @2: The cow does not chase the cow.[(((((triple6) -> rule4) triple9) -> rule3))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
((triple5 triple6) -> (rule2 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear does not see the cow.
("bear" "sees" "cow" "-")
triple4
The bear is round.
("bear" "is" "round" "+")
triple2
The bear needs the cow.
("bear" "needs" "cow" "+")
triple3
The cow chases the bear.
("cow" "chases" "bear" "+")
triple5
The cow does not see the bear.
("cow" "sees" "bear" "-")
triple10
The cow is cold.
("cow" "is" "cold" "+")
triple6
The cow is kind.
("cow" "is" "kind" "+")
triple7
The cow is round.
("cow" "is" "round" "+")
triple8
The cow needs the bear.
("cow" "needs" "bear" "+")
triple9
The bear is not red.
("bear" "is" "red" "-")
((triple9) -> (rule5 % int1))
The bear is not red.
("bear" "is" "red" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple6) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not chase the cow.
("cow" "chases" "cow" "-")
((((triple6) -> (rule4 % int2)) triple9) -> (rule3 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2