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