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