The bear is blue. The bear is cold. The bear is round. The bear needs the cow. The bear sees the cow. The cow is big. The cow is cold. The cow needs the bear. The cow sees the bear. The cow visits the bear. If something needs the cow and it is blue then the cow is big. If something visits the cow then the cow is young. If something is blue then it visits the bear.
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
If something needs the cow and it is blue then the cow is big.
((("something" "needs" "cow" "+") ("something" "is" "blue" "+")) -> ("cow" "is" "big" "+"))
If something visits the cow then the cow is young.
((("something" "visits" "cow" "+")) -> ("cow" "is" "young" "+"))
If something is blue then it visits the bear.
((("something" "is" "blue" "+")) -> ("something" "visits" "bear" "+"))
The bear is cold.
True
1
proof
[(triple2)]
("bear" "is" "cold" "+")
triple2
The bear does not see the cow.
False
1
inv-proof
[(triple5)]
("bear" "sees" "cow" "-")
triple5
The bear visits the bear.
True
2
proof
[(((triple1) -> rule3))]
("bear" "visits" "bear" "+")
((triple1) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "visits" "bear" "-")
((triple1) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear is blue.[(triple1)] The bear is cold.[(triple2)] The bear is round.[(triple3)] The bear needs the cow.[(triple4)] The bear sees the cow.[(triple5)] The cow is big.[(triple6 OR ((triple4 triple1) -> rule1))] The cow is cold.[(triple7)] The cow needs the bear.[(triple8)] The cow sees the bear.[(triple9)] The cow visits the bear.[(triple10)] @1: The bear visits the bear.[(((triple1) -> rule3))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear needs the cow.
("bear" "needs" "cow" "+")
triple4
The bear sees the cow.
("bear" "sees" "cow" "+")
triple5
The cow is big.
("cow" "is" "big" "+")
triple6
((triple4 triple1) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
triple7
The cow needs the bear.
("cow" "needs" "bear" "+")
triple8
The cow sees the bear.
("cow" "sees" "bear" "+")
triple9
The cow visits the bear.
("cow" "visits" "bear" "+")
triple10
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1