The bear is kind. The bear sees the cow. The cat is kind. The cat sees the bear. The cow sees the squirrel. The cow visits the cat. The squirrel needs the cow. If the cow sees the bear then the bear sees the cat. If someone needs the cow then they need the bear. If the cow needs the bear and the bear sees the cat then the cow is round.
The bear is kind.
("bear" "is" "kind" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If the cow sees the bear then the bear sees the cat.
((("cow" "sees" "bear" "+")) -> ("bear" "sees" "cat" "+"))
If someone needs the cow then they need the bear.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "bear" "+"))
If the cow needs the bear and the bear sees the cat then the cow is round.
((("cow" "needs" "bear" "+") ("bear" "sees" "cat" "+")) -> ("cow" "is" "round" "+"))
The squirrel needs the cow.
True
1
proof
[(triple7)]
("squirrel" "needs" "cow" "+")
triple7
The cat is not kind.
False
1
inv-proof
[(triple3)]
("cat" "is" "kind" "-")
triple3
The squirrel needs the bear.
True
2
proof
[(((triple7) -> rule2))]
("squirrel" "needs" "bear" "+")
((triple7) -> (rule2 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel does not need the bear.
False
2
inv-proof
[(((triple7) -> rule2))]
("squirrel" "needs" "bear" "-")
((triple7) -> (rule2 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The cat does not need the bear.
Unknown
inv-rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "bear" "-")
The cow is round.
Unknown
rconc
[@2: The cow is round.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cow" "is" "round" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The bear sees the squirrel.
Unknown
random
[@0: The bear sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "squirrel" "+")
@0: The bear is kind.[(triple1)] The bear sees the cow.[(triple2)] The cat is kind.[(triple3)] The cat sees the bear.[(triple4)] The cow sees the squirrel.[(triple5)] The cow visits the cat.[(triple6)] The squirrel needs the cow.[(triple7)] @1: The squirrel needs the bear.[(((triple7) -> rule2))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear sees the cow.
("bear" "sees" "cow" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat sees the bear.
("cat" "sees" "bear" "+")
triple4
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple5
The cow visits the cat.
("cow" "visits" "cat" "+")
triple6
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple7
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
((triple7) -> (rule2 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1