The bear eats the cow. The bear is cold. The bear is rough. The bear is young. The bear needs the cow. The cow eats the bear. The cow is cold. The cow is young. The cow likes the bear. The cow needs the bear. If someone likes the bear then the bear eats the cow. Big, cold people are rough. If someone likes the bear then they need the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
If someone likes the bear then the bear eats the cow.
((("someone" "likes" "bear" "+")) -> ("bear" "eats" "cow" "+"))
Big, cold people are rough.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the bear then they need the cow.
((("someone" "likes" "bear" "+")) -> ("someone" "needs" "cow" "+"))
The cow is young.
True
1
proof
[(triple8)]
("cow" "is" "young" "+")
triple8
The bear does not need the cow.
False
1
inv-proof
[(triple5)]
("bear" "needs" "cow" "-")
triple5
The cow needs the cow.
True
2
proof
[(((triple9) -> rule3))]
("cow" "needs" "cow" "+")
((triple9) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple9) -> rule3))]
("cow" "needs" "cow" "-")
((triple9) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "rough" "-")
The bear likes the cow.
Unknown
random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The bear eats the cow.[(triple1 OR ((triple9) -> rule1))] The bear is cold.[(triple2)] The bear is rough.[(triple3)] The bear is young.[(triple4)] The bear needs the cow.[(triple5)] The cow eats the bear.[(triple6)] The cow is cold.[(triple7)] The cow is young.[(triple8)] The cow likes the bear.[(triple9)] The cow needs the bear.[(triple10)] @1: The cow needs the cow.[(((triple9) -> rule3))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
((triple9) -> (rule1 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear needs the cow.
("bear" "needs" "cow" "+")
triple5
The cow eats the bear.
("cow" "eats" "bear" "+")
triple6
The cow is cold.
("cow" "is" "cold" "+")
triple7
The cow is young.
("cow" "is" "young" "+")
triple8
The cow likes the bear.
("cow" "likes" "bear" "+")
triple9
The cow needs the bear.
("cow" "needs" "bear" "+")
triple10
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple9) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1