The cow visits the rabbit. The rabbit does not eat the cow. The rabbit is rough. If something visits the rabbit and the rabbit does not like the cow then it does not visit the cow. If something is nice then it visits the cow. If something is blue and it likes the rabbit then the rabbit eats the cow. If something is green then it does not like the rabbit. If something visits the rabbit then it is nice. If something visits the cow then it does not eat the rabbit.
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If something visits the rabbit and the rabbit does not like the cow then it does not visit the cow.
((("something" "visits" "rabbit" "+") ("rabbit" "likes" "cow" "~")) -> ("something" "visits" "cow" "-"))
If something is nice then it visits the cow.
((("something" "is" "nice" "+")) -> ("something" "visits" "cow" "+"))
If something is blue and it likes the rabbit then the rabbit eats the cow.
((("something" "is" "blue" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "eats" "cow" "+"))
If something is green then it does not like the rabbit.
((("something" "is" "green" "+")) -> ("something" "likes" "rabbit" "-"))
If something visits the rabbit then it is nice.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "nice" "+"))
If something visits the cow then it does not eat the rabbit.
((("something" "visits" "cow" "+")) -> ("something" "eats" "rabbit" "-"))
The cow visits the rabbit.
True
1
proof
[(triple1)]
("cow" "visits" "rabbit" "+")
triple1
The cow does not visit the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "visits" "rabbit" "-")
triple1
The cow is nice.
True
2
proof
[(((triple1) -> rule5))]
("cow" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("cow" "is" "nice" "-")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit visits the cow.
Unknown
rconc
[@2: The rabbit visits the cow.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The cow likes the rabbit.
Unknown
random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "+")
@0: The cow visits the rabbit.[(triple1)] The rabbit does not eat the cow.[(triple2)] The rabbit is rough.[(triple3)] @1: The cow is nice.[(((triple1) -> rule5))] @2: The cow visits the cow.[(((((triple1) -> rule5)) -> rule2))] @3: The cow does not eat the rabbit.[(((((((triple1) -> rule5)) -> rule2)) -> rule6))]
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple1
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
triple2
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow does not eat the rabbit.
("cow" "eats" "rabbit" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow does not eat the rabbit.
("cow" "eats" "rabbit" "-")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3