The rabbit is big. The rabbit is cold. The rabbit likes the tiger. The rabbit needs the tiger. The rabbit sees the tiger. The tiger is big. The tiger likes the rabbit. If something sees the rabbit then it needs the rabbit. If something likes the rabbit and the rabbit likes the tiger then the tiger is nice.
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If something sees the rabbit then it needs the rabbit.
((("something" "sees" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If something likes the rabbit and the rabbit likes the tiger then the tiger is nice.
((("something" "likes" "rabbit" "+") ("rabbit" "likes" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
The rabbit is big.
True
1
proof
[(triple1)]
("rabbit" "is" "big" "+")
triple1
The rabbit is not cold.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "cold" "-")
triple2
The tiger is nice.
True
3
proof
[(((triple7 triple3) -> rule2))]
("tiger" "is" "nice" "+")
((triple7 triple3) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
3
inv-proof
[(((triple7 triple3) -> rule2))]
("tiger" "is" "nice" "-")
((triple7 triple3) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The tiger needs the rabbit.
Unknown
rconc
[@1: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "rabbit" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger sees the rabbit.
Unknown
random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "+")
@0: The rabbit is big.[(triple1)] The rabbit is cold.[(triple2)] The rabbit likes the tiger.[(triple3)] The rabbit needs the tiger.[(triple4)] The rabbit sees the tiger.[(triple5)] The tiger is big.[(triple6)] The tiger likes the rabbit.[(triple7)] @1: The tiger is nice.[(((triple7 triple3) -> rule2))]
The rabbit is big.
("rabbit" "is" "big" "+")
triple1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple3
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple4
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
((triple7 triple3) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1