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