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