The bear sees the squirrel. The cow sees the bear. The squirrel eats the tiger. The tiger visits the bear. If something sees the bear then it sees the tiger. If something eats the bear and the bear is nice then it sees the cow.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something sees the bear then it sees the tiger.
((("something" "sees" "bear" "+")) -> ("something" "sees" "tiger" "+"))
If something eats the bear and the bear is nice then it sees the cow.
((("something" "eats" "bear" "+") ("bear" "is" "nice" "+")) -> ("something" "sees" "cow" "+"))
The tiger visits the bear.
True
1
proof
[(triple4)]
("tiger" "visits" "bear" "+")
triple4
The cow does not see the bear.
False
1
inv-proof
[(triple2)]
("cow" "sees" "bear" "-")
triple2
The cow sees the tiger.
True
2
proof
[(((triple2) -> rule1))]
("cow" "sees" "tiger" "+")
((triple2) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not see the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "sees" "tiger" "-")
((triple2) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "tiger" "-")
The squirrel sees the cow.
Unknown
rconc
[@1: The squirrel sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "cow" "+")
The squirrel does not eat the bear.
Unknown
inv-random
[@0: The squirrel eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "bear" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The bear sees the squirrel.[(triple1)] The cow sees the bear.[(triple2)] The squirrel eats the tiger.[(triple3)] The tiger visits the bear.[(triple4)] @1: The cow sees the tiger.[(((triple2) -> rule1))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple3
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple4
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple2) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1