The lion chases the tiger. The lion eats the tiger. The lion is green. The lion is not kind. The lion is nice. The lion is not rough. The lion visits the tiger. The tiger does not chase the lion. The tiger eats the lion. The tiger is blue. The tiger is green. The tiger is kind. The tiger is nice. The tiger is not rough. The tiger visits the lion. If something visits the tiger and it is blue then the tiger does not eat the lion. If something chases the tiger then the tiger visits the lion.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the tiger and it is blue then the tiger does not eat the lion.
((("something" "visits" "tiger" "+") ("something" "is" "blue" "+")) -> ("tiger" "eats" "lion" "-"))
If something chases the tiger then the tiger visits the lion.
((("something" "chases" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
The lion eats the tiger.
True
1
proof
[(triple2)]
("lion" "eats" "tiger" "+")
triple2
The tiger is not kind.
False
1
inv-proof
[(triple12)]
("tiger" "is" "kind" "-")
triple12
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The lion chases the tiger.[(triple1)] The lion eats the tiger.[(triple2)] The lion is green.[(triple3)] The lion is nice.[(triple5)] The lion is not kind.[(triple4)] The lion is not rough.[(triple6)] The lion visits the tiger.[(triple7)] The tiger does not chase the lion.[(triple8)] The tiger eats the lion.[(triple9)] The tiger is blue.[(triple10)] The tiger is green.[(triple11)] The tiger is kind.[(triple12)] The tiger is nice.[(triple13)] The tiger is not rough.[(triple14)] The tiger visits the lion.[(triple15 OR ((triple1) -> rule2))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple5
The lion is not kind.
("lion" "is" "kind" "-")
triple4
The lion is not rough.
("lion" "is" "rough" "-")
triple6
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple7
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
triple8
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger is not rough.
("tiger" "is" "rough" "-")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
((triple1) -> (rule2 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1