The cow eats the lion. The cow is big. The cow is not cold. The cow likes the lion. The cow needs the lion. The lion is nice. The lion does not like the cow. The lion likes the rabbit. The lion needs the rabbit. The rabbit eats the lion. The rabbit is not big. The rabbit is cold. The rabbit is kind. The rabbit is not nice. The rabbit likes the cow. The rabbit likes the lion. If something is nice and not kind then it does not need the cow. If something needs the cow and the cow is not blue then the cow is not cold. If something is nice and it does not eat the lion then it eats the cow. If something needs the lion then it needs the rabbit. If something likes the lion and it likes the cow then it needs the lion. If something is nice and it does not need the lion then the lion likes the rabbit.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is not cold.
("cow" "is" "cold" "-")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion does not like the cow.
("lion" "likes" "cow" "-")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is not big.
("rabbit" "is" "big" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If something is nice and not kind then it does not need the cow.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "needs" "cow" "-"))
If something needs the cow and the cow is not blue then the cow is not cold.
((("something" "needs" "cow" "+") ("cow" "is" "blue" "~")) -> ("cow" "is" "cold" "-"))
If something is nice and it does not eat the lion then it eats the cow.
((("something" "is" "nice" "+") ("something" "eats" "lion" "~")) -> ("something" "eats" "cow" "+"))
If something needs the lion then it needs the rabbit.
((("something" "needs" "lion" "+")) -> ("something" "needs" "rabbit" "+"))
If something likes the lion and it likes the cow then it needs the lion.
((("something" "likes" "lion" "+") ("something" "likes" "cow" "+")) -> ("something" "needs" "lion" "+"))
If something is nice and it does not need the lion then the lion likes the rabbit.
((("something" "is" "nice" "+") ("something" "needs" "lion" "~")) -> ("lion" "likes" "rabbit" "+"))
The rabbit likes the lion.
True
1
proof
[(triple16)]
("rabbit" "likes" "lion" "+")
triple16
The lion does not need the rabbit.
False
1
inv-proof
[(triple9)]
("lion" "needs" "rabbit" "-")
triple9
The rabbit needs the lion.
True
3
proof
[(((triple16 triple15) -> rule5))]
("rabbit" "needs" "lion" "+")
((triple16 triple15) -> (rule5 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The cow does not need the rabbit.
False
2
inv-proof
[(((triple5) -> rule4))]
("cow" "needs" "rabbit" "-")
((triple5) -> (rule4 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit needs the rabbit.
True
4
proof
[(((((triple16 triple15) -> rule5)) -> rule4))]
("rabbit" "needs" "rabbit" "+")
((((triple16 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit does not need the rabbit.
False
4
inv-proof
[(((((triple16 triple15) -> rule5)) -> rule4))]
("rabbit" "needs" "rabbit" "-")
((((triple16 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "lion" "-")
The lion eats the cow.
Unknown
rconc
[@1: The lion eats the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "cow" "+")
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The lion does not eat the rabbit.
Unknown
inv-random
[@0: The lion eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "rabbit" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The cow eats the lion.[(triple1)] The cow is big.[(triple2)] The cow is not cold.[(triple3)] The cow likes the lion.[(triple4)] The cow needs the lion.[(triple5)] The lion does not like the cow.[(triple7)] The lion is nice.[(triple6)] The lion likes the rabbit.[(triple8)] The lion needs the rabbit.[(triple9)] The rabbit eats the lion.[(triple10)] The rabbit is cold.[(triple12)] The rabbit is kind.[(triple13)] The rabbit is not big.[(triple11)] The rabbit is not nice.[(triple14)] The rabbit likes the cow.[(triple15)] The rabbit likes the lion.[(triple16)] @1: The cow needs the rabbit.[(((triple5) -> rule4))] The rabbit needs the lion.[(((triple16 triple15) -> rule5))] @2: The rabbit needs the rabbit.[(((((triple16 triple15) -> rule5)) -> rule4))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is not cold.
("cow" "is" "cold" "-")
triple3
The cow likes the lion.
("cow" "likes" "lion" "+")
triple4
The cow needs the lion.
("cow" "needs" "lion" "+")
triple5
The lion does not like the cow.
("lion" "likes" "cow" "-")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple6
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple8
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple9
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple10
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
The rabbit is not big.
("rabbit" "is" "big" "-")
triple11
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple14
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple15
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple16
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((triple5) -> (rule4 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((triple16 triple15) -> (rule5 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple16 triple15) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2