The lion is blue. The lion is cold. The lion is round. The lion sees the tiger. The tiger chases the lion. The tiger likes the lion. The tiger sees the lion. If someone sees the tiger and the tiger likes the lion then the lion sees the tiger. If someone sees the lion then they are young.
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone sees the tiger and the tiger likes the lion then the lion sees the tiger.
((("someone" "sees" "tiger" "+") ("tiger" "likes" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If someone sees the lion then they are young.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "young" "+"))
The lion sees the tiger.
True
1
proof
[(triple4)]
("lion" "sees" "tiger" "+")
triple4
The lion does not see the tiger.
False
1
inv-proof
[(triple4)]
("lion" "sees" "tiger" "-")
triple4
The tiger is young.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "is" "young" "+")
((triple7) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple7) -> rule2))]
("tiger" "is" "young" "-")
((triple7) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "young" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
@0: The lion is blue.[(triple1)] The lion is cold.[(triple2)] The lion is round.[(triple3)] The lion sees the tiger.[(triple4)] The tiger chases the lion.[(triple5)] The tiger likes the lion.[(triple6)] The tiger sees the lion.[(triple7)] @1: The tiger is young.[(((triple7) -> rule2))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple5
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple6
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple7
The tiger is young.
("tiger" "is" "young" "+")
((triple7) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1