The lion chases the tiger. The lion is blue. The lion is cold. The lion is kind. The lion is red. The lion is rough. The lion likes the tiger. The lion sees the tiger. The tiger chases the lion. The tiger is blue. The tiger is cold. The tiger is kind. The tiger is red. The tiger likes the lion. The tiger sees the lion. If someone sees the lion then they are red. If the tiger is cold then the tiger is red. If someone likes the tiger then they chase the tiger. If someone likes the lion then they like the tiger. If the lion likes the tiger and the lion is cold then the lion is blue. If someone chases the lion then they like the lion.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone sees the lion then they are red.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "red" "+"))
If the tiger is cold then the tiger is red.
((("tiger" "is" "cold" "+")) -> ("tiger" "is" "red" "+"))
If someone likes the tiger then they chase the tiger.
((("someone" "likes" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
If someone likes the lion then they like the tiger.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "tiger" "+"))
If the lion likes the tiger and the lion is cold then the lion is blue.
((("lion" "likes" "tiger" "+") ("lion" "is" "cold" "+")) -> ("lion" "is" "blue" "+"))
If someone chases the lion then they like the lion.
((("someone" "chases" "lion" "+")) -> ("someone" "likes" "lion" "+"))
The tiger is cold.
True
1
proof
[(triple11)]
("tiger" "is" "cold" "+")
triple11
The lion is not blue.
False
1
inv-proof
[(triple2 OR ((triple7 triple3) -> rule5))]
("lion" "is" "blue" "-")
triple2
((triple7 triple3) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The lion chases the tiger.[(triple1 OR ((triple7) -> rule3))] The lion is blue.[(triple2 OR ((triple7 triple3) -> rule5))] The lion is cold.[(triple3)] The lion is kind.[(triple4)] The lion is red.[(triple5)] The lion is rough.[(triple6)] The lion likes the tiger.[(triple7)] The lion sees the tiger.[(triple8)] The tiger chases the lion.[(triple9)] The tiger is blue.[(triple10)] The tiger is cold.[(triple11)] The tiger is kind.[(triple12)] The tiger is red.[(triple13 OR ((triple11) -> rule2) OR ((triple15) -> rule1))] The tiger likes the lion.[(triple14 OR ((triple9) -> rule6))] The tiger sees the lion.[(triple15)] @1: The tiger likes the tiger.[(((triple14) -> rule4) OR ((((triple9) -> rule6)) -> rule4))] @2: The tiger chases the tiger.[(((((triple14) -> rule4)) -> rule3) OR ((((((triple9) -> rule6)) -> rule4)) -> rule3))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
((triple7) -> (rule3 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple2
((triple7 triple3) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple7
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple8
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
((triple11) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple15) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
((triple9) -> (rule6 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple15
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple14) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple14) -> (rule4 % int2))) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int3