The bear sees the cow. The cow needs the bear. The squirrel is nice. If something needs the bear then it needs the cow.
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If something needs the bear then it needs the cow.
((("something" "needs" "bear" "+")) -> ("something" "needs" "cow" "+"))
The cow needs the bear.
True
1
proof
[(triple2)]
("cow" "needs" "bear" "+")
triple2
The cow does not need the bear.
False
1
inv-proof
[(triple2)]
("cow" "needs" "bear" "-")
triple2
The cow needs the cow.
True
2
proof
[(((triple2) -> rule1))]
("cow" "needs" "cow" "+")
((triple2) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "needs" "cow" "-")
((triple2) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel does not need the cow.
Unknown
inv-rconc
[@1: The squirrel needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "cow" "-")
The bear needs the cow.
Unknown
rconc
[@1: The bear needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "cow" "+")
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 visits the cow.
Unknown
random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "+")
@0: The bear sees the cow.[(triple1)] The cow needs the bear.[(triple2)] The squirrel is nice.[(triple3)] @1: The cow needs the cow.[(((triple2) -> rule1))]
The bear sees the cow.
("bear" "sees" "cow" "+")
triple1
The cow needs the bear.
("cow" "needs" "bear" "+")
triple2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1