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