The lion is big. The lion is blue. The lion is nice. The lion likes the tiger. The lion needs the tiger. The lion visits the tiger. The tiger is blue. The tiger likes the lion. The tiger needs the lion. The tiger visits the lion. If someone likes the lion then they like the tiger. If someone is big then they visit the tiger. If someone is kind then they like the lion. If someone visits the tiger and the tiger is blue then they are kind. If someone is round then they like the tiger. If someone needs the tiger and they like the lion then the tiger is kind.
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone likes the lion then they like the tiger.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is big then they visit the tiger.
((("someone" "is" "big" "+")) -> ("someone" "visits" "tiger" "+"))
If someone is kind then they like the lion.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "lion" "+"))
If someone visits the tiger and the tiger is blue then they are kind.
((("someone" "visits" "tiger" "+") ("tiger" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is round then they like the tiger.
((("someone" "is" "round" "+")) -> ("someone" "likes" "tiger" "+"))
If someone needs the tiger and they like the lion then the tiger is kind.
((("someone" "needs" "tiger" "+") ("someone" "likes" "lion" "+")) -> ("tiger" "is" "kind" "+"))
The lion needs the tiger.
True
1
proof
[(triple5)]
("lion" "needs" "tiger" "+")
triple5
The lion does not need the tiger.
False
1
inv-proof
[(triple5)]
("lion" "needs" "tiger" "-")
triple5
The tiger likes the tiger.
True
2
proof
[(((triple8) -> rule1) OR ((((((triple5 ((((triple6 triple7) -> rule4)) -> rule3)) -> rule6)) -> rule3)) -> rule1) OR ((((((triple5 ((((((triple1) -> rule2) triple7) -> rule4)) -> rule3)) -> rule6)) -> rule3)) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple8) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((((triple5 ((((triple6 triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
((((((triple5 ((((((triple1) -> (rule2 % int6)) triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int6
The lion is not kind.
False
3
inv-proof
[(((triple6 triple7) -> rule4) OR ((((triple1) -> rule2) triple7) -> rule4))]
("lion" "is" "kind" "-")
((triple6 triple7) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2)) triple7) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion likes the lion.
True
4
proof
[(((((triple6 triple7) -> rule4)) -> rule3) OR ((((((triple1) -> rule2) triple7) -> rule4)) -> rule3))]
("lion" "likes" "lion" "+")
((((triple6 triple7) -> (rule4 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((((triple1) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int3
The lion does not like the lion.
False
4
inv-proof
[(((((triple6 triple7) -> rule4)) -> rule3) OR ((((((triple1) -> rule2) triple7) -> rule4)) -> rule3))]
("lion" "likes" "lion" "-")
((((triple6 triple7) -> (rule4 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((((triple1) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The lion is big.[(triple1)] The lion is blue.[(triple2)] The lion is nice.[(triple3)] The lion likes the tiger.[(triple4 OR ((((((triple6 triple7) -> rule4)) -> rule3)) -> rule1) OR ((((((((triple1) -> rule2) triple7) -> rule4)) -> rule3)) -> rule1))] The lion needs the tiger.[(triple5)] The lion visits the tiger.[(triple6 OR ((triple1) -> rule2))] The tiger is blue.[(triple7)] The tiger likes the lion.[(triple8 OR ((((triple5 ((((triple6 triple7) -> rule4)) -> rule3)) -> rule6)) -> rule3) OR ((((triple5 ((((((triple1) -> rule2) triple7) -> rule4)) -> rule3)) -> rule6)) -> rule3))] The tiger needs the lion.[(triple9)] The tiger visits the lion.[(triple10)] @1: The lion is kind.[(((triple6 triple7) -> rule4) OR ((((triple1) -> rule2) triple7) -> rule4))] The tiger likes the tiger.[(((triple8) -> rule1) OR ((((((triple5 ((((triple6 triple7) -> rule4)) -> rule3)) -> rule6)) -> rule3)) -> rule1) OR ((((((triple5 ((((((triple1) -> rule2) triple7) -> rule4)) -> rule3)) -> rule6)) -> rule3)) -> rule1))] @2: The lion likes the lion.[(((((triple6 triple7) -> rule4)) -> rule3) OR ((((((triple1) -> rule2) triple7) -> rule4)) -> rule3))] @3: The tiger is kind.[(((triple5 ((((triple6 triple7) -> rule4)) -> rule3)) -> rule6) OR ((triple5 ((((((triple1) -> rule2) triple7) -> rule4)) -> rule3)) -> rule6))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
((((((triple6 triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((((triple1) -> (rule2 % int4)) triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int4
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple5
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple6
((triple1) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple8
((((triple5 ((((triple6 triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
((((triple5 ((((((triple1) -> (rule2 % int5)) triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int5
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple9
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple10
The lion is kind.
("lion" "is" "kind" "+")
((triple6 triple7) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2)) triple7) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple8) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
((((((triple5 ((((triple6 triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
((((((triple5 ((((((triple1) -> (rule2 % int6)) triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int6
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple6 triple7) -> (rule4 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((((triple1) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
((triple5 ((((triple6 triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((triple5 ((((((triple1) -> (rule2 % int4)) triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int4