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