The lion is big. The lion is kind. The lion is nice. The lion is round. The lion is young. The lion likes the tiger. The lion needs the tiger. The lion sees the tiger. The tiger is big. The tiger is not kind. The tiger is nice. The tiger is round. The tiger is young. The tiger does not like the lion. The tiger does not need the lion. The tiger sees the lion. If the tiger is round and the tiger likes the lion then the lion is not nice. If something likes the lion and it is nice then the lion likes the tiger. If something likes the lion then the lion likes the tiger. If something likes the lion then it is young. If something is round and it sees the tiger then the tiger sees the lion. If the tiger needs the lion then the tiger likes the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not like the lion.
("tiger" "likes" "lion" "-")
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If the tiger is round and the tiger likes the lion then the lion is not nice.
((("tiger" "is" "round" "+") ("tiger" "likes" "lion" "+")) -> ("lion" "is" "nice" "-"))
If something likes the lion and it is nice then the lion likes the tiger.
((("something" "likes" "lion" "+") ("something" "is" "nice" "+")) -> ("lion" "likes" "tiger" "+"))
If something likes the lion then the lion likes the tiger.
((("something" "likes" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If something likes the lion then it is young.
((("something" "likes" "lion" "+")) -> ("something" "is" "young" "+"))
If something is round and it sees the tiger then the tiger sees the lion.
((("something" "is" "round" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If the tiger needs the lion then the tiger likes the lion.
((("tiger" "needs" "lion" "+")) -> ("tiger" "likes" "lion" "+"))
The lion is round.
True
1
proof
[(triple4)]
("lion" "is" "round" "+")
triple4
The lion is not young.
False
1
inv-proof
[(triple5)]
("lion" "is" "young" "-")
triple5
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion is big.[(triple1)] The lion is kind.[(triple2)] The lion is nice.[(triple3)] The lion is round.[(triple4)] The lion is young.[(triple5)] The lion likes the tiger.[(triple6)] The lion needs the tiger.[(triple7)] The lion sees the tiger.[(triple8)] The tiger does not like the lion.[(triple14)] The tiger does not need the lion.[(triple15)] The tiger is big.[(triple9)] The tiger is nice.[(triple11)] The tiger is not kind.[(triple10)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger sees the lion.[(triple16 OR ((triple4 triple8) -> rule5))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple6
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple7
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple8
The tiger does not like the lion.
("tiger" "likes" "lion" "-")
triple14
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
triple15
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is not kind.
("tiger" "is" "kind" "-")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple16
((triple4 triple8) -> (rule5 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1