The lion eats the tiger. The lion is cold. The lion is kind. The lion is not round. The lion is young. The lion sees the tiger. The lion visits the tiger. The tiger eats the lion. The tiger is cold. The tiger is kind. The tiger is nice. The tiger is round. The tiger is young. The tiger sees the lion. The tiger visits the lion. If someone eats the lion then they see the lion. If someone is round then they see the lion. If someone sees the tiger and they visit the tiger then they eat the lion. If someone eats the lion then the lion sees the tiger. If the tiger is round and the lion does not visit the tiger then the lion does not see the tiger. If the tiger eats the lion and the lion does not visit the tiger then the tiger is not round. If someone is young and they do not eat the lion then they are not kind. If someone sees the tiger and they eat the lion then they are kind.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not round.
("lion" "is" "round" "-")
The lion is young.
("lion" "is" "young" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone eats the lion then they see the lion.
((("someone" "eats" "lion" "+")) -> ("someone" "sees" "lion" "+"))
If someone is round then they see the lion.
((("someone" "is" "round" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the tiger and they visit the tiger then they eat the lion.
((("someone" "sees" "tiger" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "eats" "lion" "+"))
If someone eats the lion then the lion sees the tiger.
((("someone" "eats" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If the tiger is round and the lion does not visit the tiger then the lion does not see the tiger.
((("tiger" "is" "round" "+") ("lion" "visits" "tiger" "~")) -> ("lion" "sees" "tiger" "-"))
If the tiger eats the lion and the lion does not visit the tiger then the tiger is not round.
((("tiger" "eats" "lion" "+") ("lion" "visits" "tiger" "~")) -> ("tiger" "is" "round" "-"))
If someone is young and they do not eat the lion then they are not kind.
((("someone" "is" "young" "+") ("someone" "eats" "lion" "~")) -> ("someone" "is" "kind" "-"))
If someone sees the tiger and they eat the lion then they are kind.
((("someone" "sees" "tiger" "+") ("someone" "eats" "lion" "+")) -> ("someone" "is" "kind" "+"))
The tiger eats the lion.
True
1
proof
[(triple8)]
("tiger" "eats" "lion" "+")
triple8
The lion is not kind.
False
1
inv-proof
[(triple3 OR ((triple6 ((triple6 triple7) -> rule3)) -> rule8) OR ((((triple8) -> rule4) ((triple6 triple7) -> rule3)) -> rule8) OR ((triple6 ((((triple8) -> rule4) triple7) -> rule3)) -> rule8) OR ((((triple8) -> rule4) ((((triple8) -> rule4) triple7) -> rule3)) -> rule8))]
("lion" "is" "kind" "-")
triple3
((triple6 ((triple6 triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple6 triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
((triple6 ((((triple8) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
((((triple8) -> (rule4 % int3)) ((((triple8) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion eats the lion.
True
3
proof
[(((triple6 triple7) -> rule3) OR ((((triple8) -> rule4) triple7) -> rule3))]
("lion" "eats" "lion" "+")
((triple6 triple7) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
((((triple8) -> (rule4 % int2)) triple7) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion does not eat the lion.
False
3
inv-proof
[(((triple6 triple7) -> rule3) OR ((((triple8) -> rule4) triple7) -> rule3))]
("lion" "eats" "lion" "-")
((triple6 triple7) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
((((triple8) -> (rule4 % int2)) triple7) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion sees the lion.
True
4
proof
[(((((triple6 triple7) -> rule3)) -> rule1) OR ((((((triple8) -> rule4) triple7) -> rule3)) -> rule1))]
("lion" "sees" "lion" "+")
((((triple6 triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
((((((triple8) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion does not see the lion.
False
4
inv-proof
[(((((triple6 triple7) -> rule3)) -> rule1) OR ((((((triple8) -> rule4) triple7) -> rule3)) -> rule1))]
("lion" "sees" "lion" "-")
((((triple6 triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
((((((triple8) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
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 visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The lion eats the tiger.[(triple1)] The lion is cold.[(triple2)] The lion is kind.[(triple3 OR ((triple6 ((triple6 triple7) -> rule3)) -> rule8) OR ((((triple8) -> rule4) ((triple6 triple7) -> rule3)) -> rule8) OR ((triple6 ((((triple8) -> rule4) triple7) -> rule3)) -> rule8) OR ((((triple8) -> rule4) ((((triple8) -> rule4) triple7) -> rule3)) -> rule8))] The lion is not round.[(triple4)] The lion is young.[(triple5)] The lion sees the tiger.[(triple6 OR ((triple8) -> rule4))] The lion visits the tiger.[(triple7)] The tiger eats the lion.[(triple8)] The tiger is cold.[(triple9)] The tiger is kind.[(triple10)] The tiger is nice.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger sees the lion.[(triple14 OR ((triple12) -> rule2) OR ((triple8) -> rule1))] The tiger visits the lion.[(triple15)] @1: The lion eats the lion.[(((triple6 triple7) -> rule3) OR ((((triple8) -> rule4) triple7) -> rule3))] @2: The lion sees the lion.[(((((triple6 triple7) -> rule3)) -> rule1) OR ((((((triple8) -> rule4) triple7) -> rule3)) -> rule1))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple6 ((triple6 triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple6 triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
((triple6 ((((triple8) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
((((triple8) -> (rule4 % int3)) ((((triple8) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion is not round.
("lion" "is" "round" "-")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple6
((triple8) -> (rule4 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple7
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple14
((triple12) -> (rule2 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
((triple8) -> (rule1 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple6 triple7) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
((((triple8) -> (rule4 % int2)) triple7) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((((triple6 triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
((((((triple8) -> (rule4 % int3)) triple7) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3