The lion chases the tiger. The lion eats the tiger. The lion is big. The lion is green. The lion is rough. The lion sees the tiger. The tiger chases the lion. The tiger eats the lion. The tiger is big. The tiger is green. The tiger is young. The tiger sees the lion. If something is rough and it eats the lion then it is green. If something sees the lion then it sees the tiger. If the tiger sees the lion then the lion eats 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 green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something is rough and it eats the lion then it is green.
((("something" "is" "rough" "+") ("something" "eats" "lion" "+")) -> ("something" "is" "green" "+"))
If something sees the lion then it sees the tiger.
((("something" "sees" "lion" "+")) -> ("something" "sees" "tiger" "+"))
If the tiger sees the lion then the lion eats the tiger.
((("tiger" "sees" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
The tiger is green.
True
1
proof
[(triple10)]
("tiger" "is" "green" "+")
triple10
The tiger is not big.
False
1
inv-proof
[(triple9)]
("tiger" "is" "big" "-")
triple9
The tiger sees the tiger.
True
2
proof
[(((triple12) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple12) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple12) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple12) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The lion chases the tiger.[(triple1)] The lion eats the tiger.[(triple2 OR ((triple12) -> rule3))] The lion is big.[(triple3)] The lion is green.[(triple4)] The lion is rough.[(triple5)] The lion sees the tiger.[(triple6)] The tiger chases the lion.[(triple7)] The tiger eats the lion.[(triple8)] The tiger is big.[(triple9)] The tiger is green.[(triple10)] The tiger is young.[(triple11)] The tiger sees the lion.[(triple12)] @1: The tiger sees the tiger.[(((triple12) -> rule2))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
((triple12) -> (rule3 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple6
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple7
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
triple11
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple12
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple12) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1