The lion chases the tiger. The lion is nice. The lion is red. The lion likes the tiger. The lion needs the tiger. The tiger chases the lion. The tiger is blue. The tiger is not green. The tiger is not nice. The tiger is red. The tiger likes the lion. The tiger does not need the lion. All red things are blue.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
The tiger likes the lion.
True
1
proof
[(triple11)]
("tiger" "likes" "lion" "+")
triple11
The lion does not like the tiger.
False
1
inv-proof
[(triple4)]
("lion" "likes" "tiger" "-")
triple4
The lion is blue.
True
2
proof
[(((triple3) -> rule1))]
("lion" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "is" "blue" "-")
((triple3) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The lion chases the tiger.[(triple1)] The lion is nice.[(triple2)] The lion is red.[(triple3)] The lion likes the tiger.[(triple4)] The lion needs the tiger.[(triple5)] The tiger chases the lion.[(triple6)] The tiger does not need the lion.[(triple12)] The tiger is blue.[(triple7 OR ((triple10) -> rule1))] The tiger is not green.[(triple8)] The tiger is not nice.[(triple9)] The tiger is red.[(triple10)] The tiger likes the lion.[(triple11)] @1: The lion is blue.[(((triple3) -> rule1))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple5
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple6
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
triple12
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
((triple10) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not green.
("tiger" "is" "green" "-")
triple8
The tiger is not nice.
("tiger" "is" "nice" "-")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple11
The lion is blue.
("lion" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1