The lion chases the tiger. The lion eats the tiger. The lion is big. The lion is cold. The lion is kind. The lion is not rough. The lion is young. The lion needs the tiger. The tiger does not chase the lion. The tiger eats the lion. The tiger is big. The tiger is cold. The tiger is kind. The tiger is young. The tiger needs the lion. If something chases the lion then the lion needs the tiger. If something eats the lion and it needs the tiger then it is kind. If something chases the lion then it needs the tiger.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion is young.
("lion" "is" "young" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something chases the lion then the lion needs the tiger.
((("something" "chases" "lion" "+")) -> ("lion" "needs" "tiger" "+"))
If something eats the lion and it needs the tiger then it is kind.
((("something" "eats" "lion" "+") ("something" "needs" "tiger" "+")) -> ("something" "is" "kind" "+"))
If something chases the lion then it needs the tiger.
((("something" "chases" "lion" "+")) -> ("something" "needs" "tiger" "+"))
The lion is not rough.
True
1
proof
[(triple6)]
("lion" "is" "rough" "-")
triple6
The lion is not kind.
False
1
inv-proof
[(triple5)]
("lion" "is" "kind" "-")
triple5
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The lion chases the tiger.[(triple1)] The lion eats the tiger.[(triple2)] The lion is big.[(triple3)] The lion is cold.[(triple4)] The lion is kind.[(triple5)] The lion is not rough.[(triple6)] The lion is young.[(triple7)] The lion needs the tiger.[(triple8)] The tiger does not chase the lion.[(triple9)] The tiger eats the lion.[(triple10)] The tiger is big.[(triple11)] The tiger is cold.[(triple12)] The tiger is kind.[(triple13)] The tiger is young.[(triple14)] The tiger needs the lion.[(triple15)]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion is not rough.
("lion" "is" "rough" "-")
triple6
The lion is young.
("lion" "is" "young" "+")
triple7
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple8
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
triple9
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple15