The lion chases the tiger. The lion is blue. The lion is kind. The lion is nice. The lion is rough. The lion likes the tiger. The lion needs the tiger. The tiger chases the lion. The tiger is blue. The tiger is kind. The tiger is nice. The tiger is red. The tiger is rough. The tiger likes the lion. The tiger needs the lion. If something needs the tiger and it needs the lion then it likes the tiger. If something needs the lion then the lion chases the tiger. If something is kind and it chases the tiger then it is blue. If something is red then it chases the lion. If something needs the tiger and it chases the lion then the tiger is nice. Blue things are red. If something needs the tiger and the tiger likes the lion then it is rough. If something likes the lion and it is nice then it is kind.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something needs the tiger and it needs the lion then it likes the tiger.
((("something" "needs" "tiger" "+") ("something" "needs" "lion" "+")) -> ("something" "likes" "tiger" "+"))
If something needs the lion then the lion chases the tiger.
((("something" "needs" "lion" "+")) -> ("lion" "chases" "tiger" "+"))
If something is kind and it chases the tiger then it is blue.
((("something" "is" "kind" "+") ("something" "chases" "tiger" "+")) -> ("something" "is" "blue" "+"))
If something is red then it chases the lion.
((("something" "is" "red" "+")) -> ("something" "chases" "lion" "+"))
If something needs the tiger and it chases the lion then the tiger is nice.
((("something" "needs" "tiger" "+") ("something" "chases" "lion" "+")) -> ("tiger" "is" "nice" "+"))
Blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something needs the tiger and the tiger likes the lion then it is rough.
((("something" "needs" "tiger" "+") ("tiger" "likes" "lion" "+")) -> ("something" "is" "rough" "+"))
If something likes the lion and it is nice then it is kind.
((("something" "likes" "lion" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
The tiger is blue.
True
1
proof
[(triple9)]
("tiger" "is" "blue" "+")
triple9
The lion is not rough.
False
1
inv-proof
[(triple5 OR ((triple7 triple14) -> rule7))]
("lion" "is" "rough" "-")
triple5
((triple7 triple14) -> (rule7 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is red.
True
2
proof
[(((triple2) -> rule6) OR ((((triple3 triple1) -> rule3)) -> rule6) OR ((((triple3 ((triple15) -> rule2)) -> rule3)) -> rule6))]
("lion" "is" "red" "+")
((triple2) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple3 triple1) -> (rule3 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple3 ((triple15) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The lion is not red.
False
2
inv-proof
[(((triple2) -> rule6) OR ((((triple3 triple1) -> rule3)) -> rule6) OR ((((triple3 ((triple15) -> rule2)) -> rule3)) -> rule6))]
("lion" "is" "red" "-")
((triple2) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple3 triple1) -> (rule3 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple3 ((triple15) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
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 lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The lion chases the tiger.[(triple1 OR ((triple15) -> rule2))] The lion is blue.[(triple2 OR ((triple3 triple1) -> rule3) OR ((triple3 ((triple15) -> rule2)) -> rule3))] The lion is kind.[(triple3)] The lion is nice.[(triple4)] The lion is rough.[(triple5 OR ((triple7 triple14) -> rule7))] The lion likes the tiger.[(triple6)] The lion needs the tiger.[(triple7)] The tiger chases the lion.[(triple8 OR ((triple12) -> rule4) OR ((((triple9) -> rule6)) -> rule4))] The tiger is blue.[(triple9)] The tiger is kind.[(triple10 OR ((triple14 triple11) -> rule8) OR ((triple14 ((triple7 ((((triple2) -> rule6)) -> rule4)) -> rule5)) -> rule8) OR ((triple14 ((triple7 ((((((triple3 triple1) -> rule3)) -> rule6)) -> rule4)) -> rule5)) -> rule8) OR ((triple14 ((triple7 ((((((triple3 ((triple15) -> rule2)) -> rule3)) -> rule6)) -> rule4)) -> rule5)) -> rule8))] The tiger is nice.[(triple11 OR ((triple7 ((((triple2) -> rule6)) -> rule4)) -> rule5) OR ((triple7 ((((((triple3 triple1) -> rule3)) -> rule6)) -> rule4)) -> rule5) OR ((triple7 ((((((triple3 ((triple15) -> rule2)) -> rule3)) -> rule6)) -> rule4)) -> rule5))] The tiger is red.[(triple12 OR ((triple9) -> rule6))] The tiger is rough.[(triple13)] The tiger likes the lion.[(triple14)] The tiger needs the lion.[(triple15)] @1: The lion is red.[(((triple2) -> rule6) OR ((((triple3 triple1) -> rule3)) -> rule6) OR ((((triple3 ((triple15) -> rule2)) -> rule3)) -> rule6))] @2: The lion chases the lion.[(((((triple2) -> rule6)) -> rule4) OR ((((((triple3 triple1) -> rule3)) -> rule6)) -> rule4) OR ((((((triple3 ((triple15) -> rule2)) -> rule3)) -> rule6)) -> rule4))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
((triple15) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple2
((triple3 triple1) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((triple3 ((triple15) -> (rule2 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
((triple7 triple14) -> (rule7 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple6
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple7
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple8
((triple12) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
((triple14 triple11) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((triple14 ((triple7 ((((triple2) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
((triple14 ((triple7 ((((((triple3 triple1) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is blue.
("lion" "is" "blue" "+")
int5
((triple14 ((triple7 ((((((triple3 ((triple15) -> (rule2 % int6))) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is blue.
("lion" "is" "blue" "+")
int5
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int6
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
((triple7 ((((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((triple7 ((((((triple3 triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
((triple7 ((((((triple3 ((triple15) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int5
The tiger is red.
("tiger" "is" "red" "+")
triple12
((triple9) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple15
The lion is red.
("lion" "is" "red" "+")
((triple2) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple3 triple1) -> (rule3 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple3 ((triple15) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((((triple3 triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((((((triple3 ((triple15) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int4