The dog eats the tiger. The dog is rough. The dog sees the lion. The lion eats the rabbit. The lion is blue. The lion is not nice. The lion is rough. The lion likes the rabbit. The lion sees the rabbit. The lion sees the tiger. The rabbit is round. The rabbit likes the dog. The tiger eats the lion. The tiger eats the rabbit. The tiger is nice. The tiger is young. If someone is rough and they do not see the lion then the lion is nice. If someone is young and they see the rabbit then the rabbit sees the dog. If someone sees the dog then they see the tiger. If the lion likes the dog then the lion is young. If someone likes the tiger and they eat the lion then the lion likes the dog. If someone eats the rabbit and they eat the lion then they like the tiger. If the dog is round then the dog does not see the tiger.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is young.
("tiger" "is" "young" "+")
If someone is rough and they do not see the lion then the lion is nice.
((("someone" "is" "rough" "+") ("someone" "sees" "lion" "~")) -> ("lion" "is" "nice" "+"))
If someone is young and they see the rabbit then the rabbit sees the dog.
((("someone" "is" "young" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If someone sees the dog then they see the tiger.
((("someone" "sees" "dog" "+")) -> ("someone" "sees" "tiger" "+"))
If the lion likes the dog then the lion is young.
((("lion" "likes" "dog" "+")) -> ("lion" "is" "young" "+"))
If someone likes the tiger and they eat the lion then the lion likes the dog.
((("someone" "likes" "tiger" "+") ("someone" "eats" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If someone eats the rabbit and they eat the lion then they like the tiger.
((("someone" "eats" "rabbit" "+") ("someone" "eats" "lion" "+")) -> ("someone" "likes" "tiger" "+"))
If the dog is round then the dog does not see the tiger.
((("dog" "is" "round" "+")) -> ("dog" "sees" "tiger" "-"))
The lion eats the rabbit.
True
1
proof
[(triple4)]
("lion" "eats" "rabbit" "+")
triple4
The lion is nice.
False
1
inv-proof
[(triple6)]
("lion" "is" "nice" "+")
triple6
The tiger likes the tiger.
True
3
proof
[(((triple14 triple13) -> rule6))]
("tiger" "likes" "tiger" "+")
((triple14 triple13) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
3
inv-proof
[(((triple14 triple13) -> rule6))]
("tiger" "likes" "tiger" "-")
((triple14 triple13) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The lion likes the dog.
True
5
proof
[(((((triple14 triple13) -> rule6) triple13) -> rule5))]
("lion" "likes" "dog" "+")
((((triple14 triple13) -> (rule6 % int2)) triple13) -> (rule5 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The lion does not like the dog.
False
5
inv-proof
[(((((triple14 triple13) -> rule6) triple13) -> rule5))]
("lion" "likes" "dog" "-")
((((triple14 triple13) -> (rule6 % int2)) triple13) -> (rule5 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The lion is young.
True
6
proof
[(((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4))]
("lion" "is" "young" "+")
((((((triple14 triple13) -> (rule6 % int3)) triple13) -> (rule5 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The lion is not young.
False
6
inv-proof
[(((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4))]
("lion" "is" "young" "-")
((((((triple14 triple13) -> (rule6 % int3)) triple13) -> (rule5 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The rabbit sees the dog.
True
8
proof
[(((((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4) triple9) -> rule2))]
("rabbit" "sees" "dog" "+")
((((((((triple14 triple13) -> (rule6 % int4)) triple13) -> (rule5 % int3))) -> (rule4 % int2)) triple9) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The rabbit does not see the dog.
False
8
inv-proof
[(((((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4) triple9) -> rule2))]
("rabbit" "sees" "dog" "-")
((((((((triple14 triple13) -> (rule6 % int4)) triple13) -> (rule5 % int3))) -> (rule4 % int2)) triple9) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The rabbit sees the tiger.
True
9
proof
[(((((((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4) triple9) -> rule2)) -> rule3))]
("rabbit" "sees" "tiger" "+")
((((((((((triple14 triple13) -> (rule6 % int5)) triple13) -> (rule5 % int4))) -> (rule4 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion likes the dog.
("lion" "likes" "dog" "+")
int4
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int5
The rabbit does not see the tiger.
False
9
inv-proof
[(((((((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4) triple9) -> rule2)) -> rule3))]
("rabbit" "sees" "tiger" "-")
((((((((((triple14 triple13) -> (rule6 % int5)) triple13) -> (rule5 % int4))) -> (rule4 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion likes the dog.
("lion" "likes" "dog" "+")
int4
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int5
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The dog sees the tiger.
Unknown
rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "tiger" "+")
The dog does not like the tiger.
Unknown
inv-rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "tiger" "-")
The lion likes the tiger.
Unknown
rconc
[@1: The lion likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "tiger" "+")
The rabbit does not like the tiger.
Unknown
inv-rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "likes" "tiger" "-")
The tiger sees the rabbit.
Unknown
random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The tiger sees the lion.
Unknown
random
[@0: The tiger sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "lion" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The rabbit eats the tiger.
Unknown
random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The dog is rough.[(triple2)] The dog sees the lion.[(triple3)] The lion eats the rabbit.[(triple4)] The lion is blue.[(triple5)] The lion is not nice.[(triple6)] The lion is rough.[(triple7)] The lion likes the rabbit.[(triple8)] The lion sees the rabbit.[(triple9)] The lion sees the tiger.[(triple10)] The rabbit is round.[(triple11)] The rabbit likes the dog.[(triple12)] The tiger eats the lion.[(triple13)] The tiger eats the rabbit.[(triple14)] The tiger is nice.[(triple15)] The tiger is young.[(triple16)] @1: The tiger likes the tiger.[(((triple14 triple13) -> rule6))] @2: The lion likes the dog.[(((((triple14 triple13) -> rule6) triple13) -> rule5))] @3: The lion is young.[(((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4))] @4: The rabbit sees the dog.[(((((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4) triple9) -> rule2))] @5: The rabbit sees the tiger.[(((((((((((triple14 triple13) -> rule6) triple13) -> rule5)) -> rule4) triple9) -> rule2)) -> rule3))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog sees the lion.
("dog" "sees" "lion" "+")
triple3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is not nice.
("lion" "is" "nice" "-")
triple6
The lion is rough.
("lion" "is" "rough" "+")
triple7
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple8
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple9
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple12
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple13
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple14
The tiger is nice.
("tiger" "is" "nice" "+")
triple15
The tiger is young.
("tiger" "is" "young" "+")
triple16
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple14 triple13) -> (rule6 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
((((triple14 triple13) -> (rule6 % int2)) triple13) -> (rule5 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((((triple14 triple13) -> (rule6 % int3)) triple13) -> (rule5 % int2))) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((((((triple14 triple13) -> (rule6 % int4)) triple13) -> (rule5 % int3))) -> (rule4 % int2)) triple9) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((((((((((triple14 triple13) -> (rule6 % int5)) triple13) -> (rule5 % int4))) -> (rule4 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion likes the dog.
("lion" "likes" "dog" "+")
int4
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int5