The lion is big. The lion is cold. The lion is nice. The lion is red. The lion is round. The lion needs the tiger. The lion sees the tiger. The lion visits the tiger. The tiger is cold. The tiger is nice. The tiger is red. The tiger is round. The tiger needs the lion. The tiger sees the lion. The tiger visits the lion. If the lion sees the tiger then the lion is big. If the tiger needs the lion then the tiger is big. If someone needs the lion and they need the tiger then the tiger visits the lion. If the lion sees the tiger then the tiger sees the lion. If someone is cold then they see the lion. If the tiger sees the lion and the lion visits the tiger then the tiger needs the lion. If someone is big then they see the tiger. If someone is big and they see the lion then the lion is nice.
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If the lion sees the tiger then the lion is big.
((("lion" "sees" "tiger" "+")) -> ("lion" "is" "big" "+"))
If the tiger needs the lion then the tiger is big.
((("tiger" "needs" "lion" "+")) -> ("tiger" "is" "big" "+"))
If someone needs the lion and they need the tiger then the tiger visits the lion.
((("someone" "needs" "lion" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
If the lion sees the tiger then the tiger sees the lion.
((("lion" "sees" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If someone is cold then they see the lion.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "lion" "+"))
If the tiger sees the lion and the lion visits the tiger then the tiger needs the lion.
((("tiger" "sees" "lion" "+") ("lion" "visits" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If someone is big then they see the tiger.
((("someone" "is" "big" "+")) -> ("someone" "sees" "tiger" "+"))
If someone is big and they see the lion then the lion is nice.
((("someone" "is" "big" "+") ("someone" "sees" "lion" "+")) -> ("lion" "is" "nice" "+"))
The tiger is round.
True
1
proof
[(triple12)]
("tiger" "is" "round" "+")
triple12
The tiger is not nice.
False
1
inv-proof
[(triple10)]
("tiger" "is" "nice" "-")
triple10
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The lion is big.[(triple1 OR ((triple7) -> rule1))] The lion is cold.[(triple2)] The lion is nice.[(triple3 OR ((triple1 ((triple2) -> rule5)) -> rule8) OR ((((triple13) -> rule2) triple14) -> rule8) OR ((((triple13) -> rule2) ((triple7) -> rule4)) -> rule8) OR ((((triple13) -> rule2) ((triple9) -> rule5)) -> rule8) OR ((((triple7) -> rule1) ((triple2) -> rule5)) -> rule8) OR ((((((triple14 triple8) -> rule6)) -> rule2) triple14) -> rule8) OR ((((triple13) -> rule2) ((((triple1) -> rule7)) -> rule4)) -> rule8) OR ((((((triple14 triple8) -> rule6)) -> rule2) ((triple7) -> rule4)) -> rule8) OR ((((((triple14 triple8) -> rule6)) -> rule2) ((triple9) -> rule5)) -> rule8) OR ((((((triple14 triple8) -> rule6)) -> rule2) ((((triple1) -> rule7)) -> rule4)) -> rule8) OR ((((((((triple7) -> rule4) triple8) -> rule6)) -> rule2) triple14) -> rule8) OR ((((((((triple9) -> rule5) triple8) -> rule6)) -> rule2) triple14) -> rule8) OR ((((((((triple7) -> rule4) triple8) -> rule6)) -> rule2) ((triple7) -> rule4)) -> rule8) OR ((((((((triple7) -> rule4) triple8) -> rule6)) -> rule2) ((triple9) -> rule5)) -> rule8) OR ((((((((triple9) -> rule5) triple8) -> rule6)) -> rule2) ((triple7) -> rule4)) -> rule8) OR ((((((((triple9) -> rule5) triple8) -> rule6)) -> rule2) ((triple9) -> rule5)) -> rule8) OR ((((((((triple7) -> rule4) triple8) -> rule6)) -> rule2) ((((triple1) -> rule7)) -> rule4)) -> rule8) OR ((((((((triple9) -> rule5) triple8) -> rule6)) -> rule2) ((((triple1) -> rule7)) -> rule4)) -> rule8) OR ((((((((((triple1) -> rule7)) -> rule4) triple8) -> rule6)) -> rule2) triple14) -> rule8) OR ((((((((((triple1) -> rule7)) -> rule4) triple8) -> rule6)) -> rule2) ((triple7) -> rule4)) -> rule8) OR ((((((((((triple1) -> rule7)) -> rule4) triple8) -> rule6)) -> rule2) ((triple9) -> rule5)) -> rule8) OR ((((((((((triple1) -> rule7)) -> rule4) triple8) -> rule6)) -> rule2) ((((triple1) -> rule7)) -> rule4)) -> rule8))] The lion is red.[(triple4)] The lion is round.[(triple5)] The lion needs the tiger.[(triple6)] The lion sees the tiger.[(triple7 OR ((triple1) -> rule7))] The lion visits the tiger.[(triple8)] The tiger is cold.[(triple9)] The tiger is nice.[(triple10)] The tiger is red.[(triple11)] The tiger is round.[(triple12)] The tiger needs the lion.[(triple13 OR ((triple14 triple8) -> rule6) OR ((((triple7) -> rule4) triple8) -> rule6) OR ((((triple9) -> rule5) triple8) -> rule6) OR ((((((triple1) -> rule7)) -> rule4) triple8) -> rule6))] The tiger sees the lion.[(triple14 OR ((triple7) -> rule4) OR ((triple9) -> rule5) OR ((((triple1) -> rule7)) -> rule4))] The tiger visits the lion.[(triple15)] @1: The lion sees the lion.[(((triple2) -> rule5))] The tiger is big.[(((triple13) -> rule2) OR ((((triple14 triple8) -> rule6)) -> rule2) OR ((((((triple7) -> rule4) triple8) -> rule6)) -> rule2) OR ((((((triple9) -> rule5) triple8) -> rule6)) -> rule2) OR ((((((((triple1) -> rule7)) -> rule4) triple8) -> rule6)) -> rule2))] @2: The tiger sees the tiger.[(((((triple13) -> rule2)) -> rule7) OR ((((((triple14 triple8) -> rule6)) -> rule2)) -> rule7) OR ((((((((triple7) -> rule4) triple8) -> rule6)) -> rule2)) -> rule7) OR ((((((((triple9) -> rule5) triple8) -> rule6)) -> rule2)) -> rule7) OR ((((((((((triple1) -> rule7)) -> rule4) triple8) -> rule6)) -> rule2)) -> rule7))]
The lion is big.
("lion" "is" "big" "+")
triple1
((triple7) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
((triple1 ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
((((triple13) -> (rule2 % int2)) triple14) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple13) -> (rule2 % int3)) ((triple7) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((triple13) -> (rule2 % int3)) ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((triple7) -> (rule1 % int3)) ((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((((((triple14 triple8) -> (rule6 % int3))) -> (rule2 % int2)) triple14) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
((((triple13) -> (rule2 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((((triple14 triple8) -> (rule6 % int4))) -> (rule2 % int3)) ((triple7) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int4
((((((triple14 triple8) -> (rule6 % int4))) -> (rule2 % int3)) ((triple9) -> (rule5 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int4
((((((triple14 triple8) -> (rule6 % int5))) -> (rule2 % int4)) ((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int5
((((((((triple7) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) triple14) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) triple14) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((triple7) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) ((triple7) -> (rule4 % int4))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((triple7) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) ((triple9) -> (rule5 % int4))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) ((triple7) -> (rule4 % int4))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) ((triple9) -> (rule5 % int4))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((triple7) -> (rule4 % int5)) triple8) -> (rule6 % int4))) -> (rule2 % int3)) ((((triple1) -> (rule7 % int2))) -> (rule4 % int5))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int4
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int5
((((((((triple9) -> (rule5 % int5)) triple8) -> (rule6 % int4))) -> (rule2 % int3)) ((((triple1) -> (rule7 % int2))) -> (rule4 % int5))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int4
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int5
((((((((((triple1) -> (rule7 % int5))) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) triple14) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int5
((((((((((triple1) -> (rule7 % int5))) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) ((triple7) -> (rule4 % int4))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int5
((((((((((triple1) -> (rule7 % int5))) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) ((triple9) -> (rule5 % int4))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int5
((((((((((triple1) -> (rule7 % int5))) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int5
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple6
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple7
((triple1) -> (rule7 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple13
((triple14 triple8) -> (rule6 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
((((triple7) -> (rule4 % int2)) triple8) -> (rule6 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
((((triple9) -> (rule5 % int2)) triple8) -> (rule6 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2)) triple8) -> (rule6 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple14
((triple7) -> (rule4 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
((triple9) -> (rule5 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple2) -> (rule5 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple13) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple14 triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
((((((triple7) -> (rule4 % int3)) triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int3
((((((triple9) -> (rule5 % int3)) triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule4 % int3)) triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int4
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple13) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((((triple14 triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
((((((((triple7) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((triple9) -> (rule5 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
((((((((((triple1) -> (rule7 % int5))) -> (rule4 % int4)) triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int5