The lion is blue. The lion is green. The lion is young. The lion needs the tiger. The lion sees the tiger. The rabbit is green. The rabbit is young. The rabbit needs the lion. The rabbit needs the tiger. The rabbit sees the tiger. The rabbit visits the lion. The rabbit visits the tiger. The tiger is rough. The tiger sees the lion. The tiger visits the lion. If something visits the lion and it visits the tiger then the tiger is blue. If something needs the tiger then it is nice. If something sees the lion and it visits the tiger then the lion sees the tiger. If something is young then it sees the tiger. If something needs the tiger and it is blue then it visits the tiger. If the tiger visits the rabbit and the tiger is green then the tiger visits the lion. If something is blue and it sees the lion then the lion visits the tiger. If something visits the rabbit and it is green then it needs the lion.
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the lion and it visits the tiger then the tiger is blue.
((("something" "visits" "lion" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If something needs the tiger then it is nice.
((("something" "needs" "tiger" "+")) -> ("something" "is" "nice" "+"))
If something sees the lion and it visits the tiger then the lion sees the tiger.
((("something" "sees" "lion" "+") ("something" "visits" "tiger" "+")) -> ("lion" "sees" "tiger" "+"))
If something is young then it sees the tiger.
((("something" "is" "young" "+")) -> ("something" "sees" "tiger" "+"))
If something needs the tiger and it is blue then it visits the tiger.
((("something" "needs" "tiger" "+") ("something" "is" "blue" "+")) -> ("something" "visits" "tiger" "+"))
If the tiger visits the rabbit and the tiger is green then the tiger visits the lion.
((("tiger" "visits" "rabbit" "+") ("tiger" "is" "green" "+")) -> ("tiger" "visits" "lion" "+"))
If something is blue and it sees the lion then the lion visits the tiger.
((("something" "is" "blue" "+") ("something" "sees" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
If something visits the rabbit and it is green then it needs the lion.
((("something" "visits" "rabbit" "+") ("something" "is" "green" "+")) -> ("something" "needs" "lion" "+"))
The lion is young.
True
1
proof
[(triple3)]
("lion" "is" "young" "+")
triple3
The rabbit does not need the lion.
False
1
inv-proof
[(triple8)]
("rabbit" "needs" "lion" "-")
triple8
The rabbit is nice.
True
2
proof
[(((triple9) -> rule2))]
("rabbit" "is" "nice" "+")
((triple9) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The lion does not visit the tiger.
False
3
inv-proof
[(((triple4 triple1) -> rule5) OR ((((triple11 triple12) -> rule1) triple14) -> rule7))]
("lion" "visits" "tiger" "-")
((triple4 triple1) -> (rule5 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
((((triple11 triple12) -> (rule1 % int2)) triple14) -> (rule7 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "lion" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The lion is blue.[(triple1)] The lion is green.[(triple2)] The lion is young.[(triple3)] The lion needs the tiger.[(triple4)] The lion sees the tiger.[(triple5 OR ((triple3) -> rule4))] The rabbit is green.[(triple6)] The rabbit is young.[(triple7)] The rabbit needs the lion.[(triple8)] The rabbit needs the tiger.[(triple9)] The rabbit sees the tiger.[(triple10 OR ((triple7) -> rule4))] The rabbit visits the lion.[(triple11)] The rabbit visits the tiger.[(triple12)] The tiger is rough.[(triple13)] The tiger sees the lion.[(triple14)] The tiger visits the lion.[(triple15)] @1: The lion is nice.[(((triple4) -> rule2))] The lion visits the tiger.[(((triple4 triple1) -> rule5) OR ((((triple11 triple12) -> rule1) triple14) -> rule7))] The rabbit is nice.[(((triple9) -> rule2))] The tiger is blue.[(((triple11 triple12) -> rule1))]
The lion is blue.
("lion" "is" "blue" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple5
((triple3) -> (rule4 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple8
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple9
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple10
((triple7) -> (rule4 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple11
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The lion is nice.
("lion" "is" "nice" "+")
((triple4) -> (rule2 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple4 triple1) -> (rule5 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
((((triple11 triple12) -> (rule1 % int2)) triple14) -> (rule7 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple9) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple11 triple12) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1