The lion chases the tiger. The lion does not eat the tiger. The lion is big. The lion is cold. The lion is not green. The lion is kind. The lion is nice. 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 green. The tiger is kind. The tiger is nice. The tiger does not need the lion. If something needs the tiger then it needs the lion. If the tiger is green then the tiger does not need the lion. If something chases the tiger and it is not cold then it does not eat the tiger. If the lion eats the tiger and the tiger does not need the lion then the lion chases the tiger. If something eats the tiger then it chases the lion. If something chases the tiger and it does not chase the lion then the tiger eats the lion.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion does not eat the tiger.
("lion" "eats" "tiger" "-")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
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 green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
If something needs the tiger then it needs the lion.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "lion" "+"))
If the tiger is green then the tiger does not need the lion.
((("tiger" "is" "green" "+")) -> ("tiger" "needs" "lion" "-"))
If something chases the tiger and it is not cold then it does not eat the tiger.
((("something" "chases" "tiger" "+") ("something" "is" "cold" "~")) -> ("something" "eats" "tiger" "-"))
If the lion eats the tiger and the tiger does not need the lion then the lion chases the tiger.
((("lion" "eats" "tiger" "+") ("tiger" "needs" "lion" "~")) -> ("lion" "chases" "tiger" "+"))
If something eats the tiger then it chases the lion.
((("something" "eats" "tiger" "+")) -> ("something" "chases" "lion" "+"))
If something chases the tiger and it does not chase the lion then the tiger eats the lion.
((("something" "chases" "tiger" "+") ("something" "chases" "lion" "~")) -> ("tiger" "eats" "lion" "+"))
The tiger is nice.
True
1
proof
[(triple15)]
("tiger" "is" "nice" "+")
triple15
The tiger does not eat the lion.
False
1
inv-proof
[(triple10)]
("tiger" "eats" "lion" "-")
triple10
The lion needs the lion.
True
2
proof
[(((triple8) -> rule1))]
("lion" "needs" "lion" "+")
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple8) -> rule1))]
("lion" "needs" "lion" "-")
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not chase the lion.
Unknown
inv-rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "lion" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion chases the tiger.[(triple1)] The lion does not eat the tiger.[(triple2)] The lion is big.[(triple3)] The lion is cold.[(triple4)] The lion is kind.[(triple6)] The lion is nice.[(triple7)] The lion is not green.[(triple5)] The lion needs the tiger.[(triple8)] The tiger does not chase the lion.[(triple9)] The tiger does not need the lion.[(triple16 OR ((triple13) -> rule2))] The tiger eats the lion.[(triple10)] The tiger is big.[(triple11)] The tiger is cold.[(triple12)] The tiger is green.[(triple13)] The tiger is kind.[(triple14)] The tiger is nice.[(triple15)] @1: The lion needs the lion.[(((triple8) -> rule1))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion does not eat 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" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion is not green.
("lion" "is" "green" "-")
triple5
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple8
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
triple9
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
triple16
((triple13) -> (rule2 % int1))
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
int1
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 green.
("tiger" "is" "green" "+")
triple13
The tiger is kind.
("tiger" "is" "kind" "+")
triple14
The tiger is nice.
("tiger" "is" "nice" "+")
triple15
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1