The bear eats the cow. The bear is big. The bear is cold. The bear is kind. The bear is red. The bear likes the cow. The bear needs the cow. The cow eats the bear. The cow is big. The cow is nice. The cow likes the bear. The cow needs the bear. If the bear needs the cow then the cow eats the bear. If something needs the bear then it does not like the cow. If the cow likes the bear and the cow does not eat the bear then the cow is kind.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
If the bear needs the cow then the cow eats the bear.
((("bear" "needs" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If something needs the bear then it does not like the cow.
((("something" "needs" "bear" "+")) -> ("something" "likes" "cow" "-"))
If the cow likes the bear and the cow does not eat the bear then the cow is kind.
((("cow" "likes" "bear" "+") ("cow" "eats" "bear" "~")) -> ("cow" "is" "kind" "+"))
The bear is cold.
True
1
proof
[(triple3)]
("bear" "is" "cold" "+")
triple3
The cow does not eat the bear.
False
1
inv-proof
[(triple8 OR ((triple7) -> rule1))]
("cow" "eats" "bear" "-")
triple8
((triple7) -> (rule1 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow does not like the cow.
True
2
proof
[(((triple12) -> rule2))]
("cow" "likes" "cow" "-")
((triple12) -> (rule2 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow likes the cow.
False
2
inv-proof
[(((triple12) -> rule2))]
("cow" "likes" "cow" "+")
((triple12) -> (rule2 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "kind" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The bear eats the cow.[(triple1)] The bear is big.[(triple2)] The bear is cold.[(triple3)] The bear is kind.[(triple4)] The bear is red.[(triple5)] The bear likes the cow.[(triple6)] The bear needs the cow.[(triple7)] The cow eats the bear.[(triple8 OR ((triple7) -> rule1))] The cow is big.[(triple9)] The cow is nice.[(triple10)] The cow likes the bear.[(triple11)] The cow needs the bear.[(triple12)] @1: The cow does not like the cow.[(((triple12) -> rule2))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is kind.
("bear" "is" "kind" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
triple5
The bear likes the cow.
("bear" "likes" "cow" "+")
triple6
The bear needs the cow.
("bear" "needs" "cow" "+")
triple7
The cow eats the bear.
("cow" "eats" "bear" "+")
triple8
((triple7) -> (rule1 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow is big.
("cow" "is" "big" "+")
triple9
The cow is nice.
("cow" "is" "nice" "+")
triple10
The cow likes the bear.
("cow" "likes" "bear" "+")
triple11
The cow needs the bear.
("cow" "needs" "bear" "+")
triple12
The cow does not like the cow.
("cow" "likes" "cow" "-")
((triple12) -> (rule2 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1