The cow visits the squirrel. The lion likes the tiger. The squirrel visits the tiger. The tiger visits the cow. If something visits the tiger then it needs the tiger. If something needs the cow then the cow is big.
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something visits the tiger then it needs the tiger.
((("something" "visits" "tiger" "+")) -> ("something" "needs" "tiger" "+"))
If something needs the cow then the cow is big.
((("something" "needs" "cow" "+")) -> ("cow" "is" "big" "+"))
The cow visits the squirrel.
True
1
proof
[(triple1)]
("cow" "visits" "squirrel" "+")
triple1
The squirrel does not visit the tiger.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "tiger" "-")
triple3
The squirrel needs the tiger.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "needs" "tiger" "+")
((triple3) -> (rule1 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel does not need the tiger.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "needs" "tiger" "-")
((triple3) -> (rule1 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The cow does not need the tiger.
Unknown
inv-rconc
[@1: The cow needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "needs" "tiger" "-")
The lion needs the tiger.
Unknown
rconc
[@1: The lion needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "tiger" "+")
The cow does not visit the lion.
Unknown
inv-random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "-")
The squirrel likes the cow.
Unknown
random
[@0: The squirrel likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cow" "+")
@0: The cow visits the squirrel.[(triple1)] The lion likes the tiger.[(triple2)] The squirrel visits the tiger.[(triple3)] The tiger visits the cow.[(triple4)] @1: The squirrel needs the tiger.[(((triple3) -> rule1))]
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple3
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple4
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
((triple3) -> (rule1 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1