The cow needs the rabbit. The cow visits the lion. The lion is not kind. The lion is young. The rabbit does not need the tiger. The rabbit visits the tiger. The tiger needs the rabbit. If something needs the tiger and it likes the cow then the tiger needs the lion. If the tiger likes the cow then the cow does not need the rabbit. If something is big and it does not like the tiger then it does not need the tiger. If the rabbit likes the lion then the rabbit is blue. If something visits the tiger then it likes the lion. If something visits the tiger and the tiger is young then the tiger likes the cow.
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is young.
("lion" "is" "young" "+")
The rabbit does not need the tiger.
("rabbit" "needs" "tiger" "-")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something needs the tiger and it likes the cow then the tiger needs the lion.
((("something" "needs" "tiger" "+") ("something" "likes" "cow" "+")) -> ("tiger" "needs" "lion" "+"))
If the tiger likes the cow then the cow does not need the rabbit.
((("tiger" "likes" "cow" "+")) -> ("cow" "needs" "rabbit" "-"))
If something is big and it does not like the tiger then it does not need the tiger.
((("something" "is" "big" "+") ("something" "likes" "tiger" "~")) -> ("something" "needs" "tiger" "-"))
If the rabbit likes the lion then the rabbit is blue.
((("rabbit" "likes" "lion" "+")) -> ("rabbit" "is" "blue" "+"))
If something visits the tiger then it likes the lion.
((("something" "visits" "tiger" "+")) -> ("something" "likes" "lion" "+"))
If something visits the tiger and the tiger is young then the tiger likes the cow.
((("something" "visits" "tiger" "+") ("tiger" "is" "young" "+")) -> ("tiger" "likes" "cow" "+"))
The rabbit visits the tiger.
True
1
proof
[(triple6)]
("rabbit" "visits" "tiger" "+")
triple6
The cow does not visit the lion.
False
1
inv-proof
[(triple2)]
("cow" "visits" "lion" "-")
triple2
The rabbit likes the lion.
True
2
proof
[(((triple6) -> rule5))]
("rabbit" "likes" "lion" "+")
((triple6) -> (rule5 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit does not like the lion.
False
2
inv-proof
[(((triple6) -> rule5))]
("rabbit" "likes" "lion" "-")
((triple6) -> (rule5 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple6) -> rule5)) -> rule4))]
("rabbit" "is" "blue" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule4))]
("rabbit" "is" "blue" "-")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The cow does not like the lion.
Unknown
inv-rconc
[@1: The cow likes the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "lion" "-")
The tiger likes the lion.
Unknown
rconc
[@1: The tiger likes the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "lion" "+")
The tiger does not like the cow.
Unknown
inv-rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "cow" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The cow visits the rabbit.
Unknown
random
[@0: The cow visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "rabbit" "+")
@0: The cow needs the rabbit.[(triple1)] The cow visits the lion.[(triple2)] The lion is not kind.[(triple3)] The lion is young.[(triple4)] The rabbit does not need the tiger.[(triple5)] The rabbit visits the tiger.[(triple6)] The tiger needs the rabbit.[(triple7)] @1: The rabbit likes the lion.[(((triple6) -> rule5))] @2: The rabbit is blue.[(((((triple6) -> rule5)) -> rule4))]
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple1
The cow visits the lion.
("cow" "visits" "lion" "+")
triple2
The lion is not kind.
("lion" "is" "kind" "-")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The rabbit does not need the tiger.
("rabbit" "needs" "tiger" "-")
triple5
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple6
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple7
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((triple6) -> (rule5 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2