The bear is rough. The rabbit is not kind. The squirrel is big. The tiger chases the squirrel. If someone chases the squirrel then they do not visit the squirrel. If someone chases the rabbit then the rabbit is nice. If someone visits the bear then they visit the rabbit. If someone visits the tiger then the tiger does not visit the bear. If someone needs the bear and the bear is not nice then they are kind. If someone chases the tiger then the tiger needs the squirrel.
The bear is rough.
("bear" "is" "rough" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
If someone chases the squirrel then they do not visit the squirrel.
((("someone" "chases" "squirrel" "+")) -> ("someone" "visits" "squirrel" "-"))
If someone chases the rabbit then the rabbit is nice.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If someone visits the bear then they visit the rabbit.
((("someone" "visits" "bear" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the tiger then the tiger does not visit the bear.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "bear" "-"))
If someone needs the bear and the bear is not nice then they are kind.
((("someone" "needs" "bear" "+") ("bear" "is" "nice" "~")) -> ("someone" "is" "kind" "+"))
If someone chases the tiger then the tiger needs the squirrel.
((("someone" "chases" "tiger" "+")) -> ("tiger" "needs" "squirrel" "+"))
The rabbit is not kind.
True
1
proof
[(triple2)]
("rabbit" "is" "kind" "-")
triple2
The squirrel is not big.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "big" "-")
triple3
The tiger does not visit the squirrel.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "visits" "squirrel" "-")
((triple4) -> (rule1 % int1))
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
int1
The tiger visits the squirrel.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "visits" "squirrel" "+")
((triple4) -> (rule1 % int1))
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
int1
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The rabbit visits the bear.
Unknown
random
[@0: The rabbit visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bear" "+")
@0: The bear is rough.[(triple1)] The rabbit is not kind.[(triple2)] The squirrel is big.[(triple3)] The tiger chases the squirrel.[(triple4)] @1: The tiger does not visit the squirrel.[(((triple4) -> rule1))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple4
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
((triple4) -> (rule1 % int1))
The tiger does not visit the squirrel.
("tiger" "visits" "squirrel" "-")
int1