The bear does not chase the cat. The bear chases the cow. The bear eats the cat. The bear eats the cow. The bear is not cold. The cat chases the bear. The cat eats the bear. The cat eats the cow. The cat is green. The cat is nice. The cat is rough. The cow chases the bear. The cow does not chase the cat. The cow is cold. The cow is rough. If something sees the cat and it is not rough then the cat sees the bear. If something sees the cow and the cow eats the cat then it does not chase the cow. If something is cold and it eats the bear then it sees the cat. If something chases the cow then it sees the cat. If something sees the bear and the bear sees the cat then it eats the cat. If something chases the bear then the bear sees the cat. If the cow chases the bear and the bear does not see the cow then the cow eats the cat. If something eats the cat then the cat sees the cow.
The bear does not chase the cat.
("bear" "chases" "cat" "-")
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is not cold.
("bear" "is" "cold" "-")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow does not chase the cat.
("cow" "chases" "cat" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow is rough.
("cow" "is" "rough" "+")
If something sees the cat and it is not rough then the cat sees the bear.
((("something" "sees" "cat" "+") ("something" "is" "rough" "~")) -> ("cat" "sees" "bear" "+"))
If something sees the cow and the cow eats the cat then it does not chase the cow.
((("something" "sees" "cow" "+") ("cow" "eats" "cat" "+")) -> ("something" "chases" "cow" "-"))
If something is cold and it eats the bear then it sees the cat.
((("something" "is" "cold" "+") ("something" "eats" "bear" "+")) -> ("something" "sees" "cat" "+"))
If something chases the cow then it sees the cat.
((("something" "chases" "cow" "+")) -> ("something" "sees" "cat" "+"))
If something sees the bear and the bear sees the cat then it eats the cat.
((("something" "sees" "bear" "+") ("bear" "sees" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something chases the bear then the bear sees the cat.
((("something" "chases" "bear" "+")) -> ("bear" "sees" "cat" "+"))
If the cow chases the bear and the bear does not see the cow then the cow eats the cat.
((("cow" "chases" "bear" "+") ("bear" "sees" "cow" "~")) -> ("cow" "eats" "cat" "+"))
If something eats the cat then the cat sees the cow.
((("something" "eats" "cat" "+")) -> ("cat" "sees" "cow" "+"))
The cow is rough.
True
1
proof
[(triple15)]
("cow" "is" "rough" "+")
triple15
The cat does not eat the bear.
False
1
inv-proof
[(triple7)]
("cat" "eats" "bear" "-")
triple7
The bear sees the cat.
True
2
proof
[(((triple12) -> rule6) OR ((triple2) -> rule4) OR ((triple6) -> rule6))]
("bear" "sees" "cat" "+")
((triple12) -> (rule6 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
((triple2) -> (rule4 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
((triple6) -> (rule6 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The bear does not see the cat.
False
2
inv-proof
[(((triple12) -> rule6) OR ((triple2) -> rule4) OR ((triple6) -> rule6))]
("bear" "sees" "cat" "-")
((triple12) -> (rule6 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
((triple2) -> (rule4 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
((triple6) -> (rule6 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "cat" "-")
The cow eats the cat.
Unknown
rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "cat" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear chases the cow.[(triple2)] The bear does not chase the cat.[(triple1)] The bear eats the cat.[(triple3)] The bear eats the cow.[(triple4)] The bear is not cold.[(triple5)] The cat chases the bear.[(triple6)] The cat eats the bear.[(triple7)] The cat eats the cow.[(triple8)] The cat is green.[(triple9)] The cat is nice.[(triple10)] The cat is rough.[(triple11)] The cow chases the bear.[(triple12)] The cow does not chase the cat.[(triple13)] The cow is cold.[(triple14)] The cow is rough.[(triple15)] @1: The bear sees the cat.[(((triple12) -> rule6) OR ((triple2) -> rule4) OR ((triple6) -> rule6))] The cat sees the cow.[(((triple3) -> rule8))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple2
The bear does not chase the cat.
("bear" "chases" "cat" "-")
triple1
The bear eats the cat.
("bear" "eats" "cat" "+")
triple3
The bear eats the cow.
("bear" "eats" "cow" "+")
triple4
The bear is not cold.
("bear" "is" "cold" "-")
triple5
The cat chases the bear.
("cat" "chases" "bear" "+")
triple6
The cat eats the bear.
("cat" "eats" "bear" "+")
triple7
The cat eats the cow.
("cat" "eats" "cow" "+")
triple8
The cat is green.
("cat" "is" "green" "+")
triple9
The cat is nice.
("cat" "is" "nice" "+")
triple10
The cat is rough.
("cat" "is" "rough" "+")
triple11
The cow chases the bear.
("cow" "chases" "bear" "+")
triple12
The cow does not chase the cat.
("cow" "chases" "cat" "-")
triple13
The cow is cold.
("cow" "is" "cold" "+")
triple14
The cow is rough.
("cow" "is" "rough" "+")
triple15
The bear sees the cat.
("bear" "sees" "cat" "+")
((triple12) -> (rule6 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
((triple2) -> (rule4 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
((triple6) -> (rule6 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple3) -> (rule8 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1