The cow is big. The lion sees the tiger. The rabbit does not like the tiger. The tiger likes the lion. If the lion does not need the rabbit then the lion does not need the cow. If someone likes the lion and the lion does not need the tiger then they see the rabbit. If someone needs the cow and they see the rabbit then they are rough. If someone is green then they do not like the lion. If someone is kind then they do not see the lion. If someone likes the lion then the lion is kind.
The cow is big.
("cow" "is" "big" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If the lion does not need the rabbit then the lion does not need the cow.
((("lion" "needs" "rabbit" "~")) -> ("lion" "needs" "cow" "-"))
If someone likes the lion and the lion does not need the tiger then they see the rabbit.
((("someone" "likes" "lion" "+") ("lion" "needs" "tiger" "~")) -> ("someone" "sees" "rabbit" "+"))
If someone needs the cow and they see the rabbit then they are rough.
((("someone" "needs" "cow" "+") ("someone" "sees" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
If someone is green then they do not like the lion.
((("someone" "is" "green" "+")) -> ("someone" "likes" "lion" "-"))
If someone is kind then they do not see the lion.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "lion" "-"))
If someone likes the lion then the lion is kind.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "kind" "+"))
The cow is big.
True
1
proof
[(triple1)]
("cow" "is" "big" "+")
triple1
The rabbit likes the tiger.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "tiger" "+")
triple3
The lion is kind.
True
2
proof
[(((triple4) -> rule6))]
("lion" "is" "kind" "+")
((triple4) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not kind.
False
2
inv-proof
[(((triple4) -> rule6))]
("lion" "is" "kind" "-")
((triple4) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion does not see the lion.
True
3
proof
[(((((triple4) -> rule6)) -> rule5))]
("lion" "sees" "lion" "-")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion sees the lion.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule5))]
("lion" "sees" "lion" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "rough" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "rough" "+")
The cow does not see the rabbit.
Unknown
inv-rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "rabbit" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not need the lion.
Unknown
inv-random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
@0: The cow is big.[(triple1)] The lion sees the tiger.[(triple2)] The rabbit does not like the tiger.[(triple3)] The tiger likes the lion.[(triple4)] @1: The lion is kind.[(((triple4) -> rule6))] @2: The lion does not see the lion.[(((((triple4) -> rule6)) -> rule5))]
The cow is big.
("cow" "is" "big" "+")
triple1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple2
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
triple3
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
((triple4) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion does not see the lion.
("lion" "sees" "lion" "-")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2