The cat is kind. The mouse visits the rabbit. The rabbit is big. The rabbit is kind. The tiger is nice. The tiger likes the rabbit. The tiger visits the mouse. If someone is kind then they like the cat. If someone needs the rabbit and they are kind then the rabbit is big. If someone visits the mouse then they are young. If someone likes the cat then they visit the tiger. If the rabbit visits the tiger then the tiger is kind. If someone needs the tiger then they need the mouse. If someone needs the tiger then they are young. If someone is young and they like the tiger then they are cold.
The cat is kind.
("cat" "is" "kind" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is kind then they like the cat.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "cat" "+"))
If someone needs the rabbit and they are kind then the rabbit is big.
((("someone" "needs" "rabbit" "+") ("someone" "is" "kind" "+")) -> ("rabbit" "is" "big" "+"))
If someone visits the mouse then they are young.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone likes the cat then they visit the tiger.
((("someone" "likes" "cat" "+")) -> ("someone" "visits" "tiger" "+"))
If the rabbit visits the tiger then the tiger is kind.
((("rabbit" "visits" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone needs the tiger then they need the mouse.
((("someone" "needs" "tiger" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the tiger then they are young.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone is young and they like the tiger then they are cold.
((("someone" "is" "young" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "is" "cold" "+"))
The rabbit is big.
True
1
proof
[(triple3)]
("rabbit" "is" "big" "+")
triple3
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "visits" "rabbit" "-")
triple2
The tiger is young.
True
2
proof
[(((triple7) -> rule3))]
("tiger" "is" "young" "+")
((triple7) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple7) -> rule3))]
("tiger" "is" "young" "-")
((triple7) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The rabbit visits the tiger.
True
3
proof
[(((((triple4) -> rule1)) -> rule4))]
("rabbit" "visits" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The rabbit does not visit the tiger.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule4))]
("rabbit" "visits" "tiger" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The tiger is kind.
True
4
proof
[(((((((triple4) -> rule1)) -> rule4)) -> rule5))]
("tiger" "is" "kind" "+")
((((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int3
The tiger is not kind.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule4)) -> rule5))]
("tiger" "is" "kind" "-")
((((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int3
The tiger likes the cat.
True
5
proof
[(((((((((triple4) -> rule1)) -> rule4)) -> rule5)) -> rule1))]
("tiger" "likes" "cat" "+")
((((((((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int4
The tiger does not like the cat.
False
5
inv-proof
[(((((((((triple4) -> rule1)) -> rule4)) -> rule5)) -> rule1))]
("tiger" "likes" "cat" "-")
((((((((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int4
The tiger visits the tiger.
True
6
proof
[(((((((((((triple4) -> rule1)) -> rule4)) -> rule5)) -> rule1)) -> rule4))]
("tiger" "visits" "tiger" "+")
((((((((((triple4) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int4
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int5
The tiger does not visit the tiger.
False
6
inv-proof
[(((((((((((triple4) -> rule1)) -> rule4)) -> rule5)) -> rule1)) -> rule4))]
("tiger" "visits" "tiger" "-")
((((((((((triple4) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int4
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int5
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "cold" "-")
The tiger needs the mouse.
Unknown
rconc
[@1: The tiger needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "needs" "mouse" "+")
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "-")
The cat is cold.
Unknown
rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "cold" "+")
The rabbit does not need the mouse.
Unknown
inv-rconc
[@1: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "needs" "mouse" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "young" "+")
The cat does not visit the rabbit.
Unknown
inv-random
[@0: The cat visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "rabbit" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
The rabbit does not visit the cat.
Unknown
inv-random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
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 rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The cat is kind.[(triple1)] The mouse visits the rabbit.[(triple2)] The rabbit is big.[(triple3)] The rabbit is kind.[(triple4)] The tiger is nice.[(triple5)] The tiger likes the rabbit.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The cat likes the cat.[(((triple1) -> rule1))] The rabbit likes the cat.[(((triple4) -> rule1))] The tiger is young.[(((triple7) -> rule3))] @2: The cat visits the tiger.[(((((triple1) -> rule1)) -> rule4))] The rabbit visits the tiger.[(((((triple4) -> rule1)) -> rule4))] @3: The tiger is kind.[(((((((triple4) -> rule1)) -> rule4)) -> rule5))] @4: The tiger likes the cat.[(((((((((triple4) -> rule1)) -> rule4)) -> rule5)) -> rule1))] @5: The tiger visits the tiger.[(((((((((((triple4) -> rule1)) -> rule4)) -> rule5)) -> rule1)) -> rule4))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The tiger is nice.
("tiger" "is" "nice" "+")
triple5
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple1) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((triple4) -> (rule1 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple7) -> (rule3 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
((((((triple4) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int3
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((((((((triple4) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((((((((triple4) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int4
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int5