The rabbit does not eat the tiger. The rabbit is not round. The rabbit likes the tiger. The rabbit sees the tiger. The tiger is red. The tiger likes the rabbit. The tiger sees the rabbit. If something is young and it does not see the tiger then it is round. If the rabbit is round and the rabbit does not eat the tiger then the rabbit does not like the tiger. If something likes the tiger and it is young then the tiger likes the rabbit. If something is red then it likes the rabbit. If something eats the rabbit then the rabbit is green. If something sees the tiger then it is young.
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something is young and it does not see the tiger then it is round.
((("something" "is" "young" "+") ("something" "sees" "tiger" "~")) -> ("something" "is" "round" "+"))
If the rabbit is round and the rabbit does not eat the tiger then the rabbit does not like the tiger.
((("rabbit" "is" "round" "+") ("rabbit" "eats" "tiger" "~")) -> ("rabbit" "likes" "tiger" "-"))
If something likes the tiger and it is young then the tiger likes the rabbit.
((("something" "likes" "tiger" "+") ("something" "is" "young" "+")) -> ("tiger" "likes" "rabbit" "+"))
If something is red then it likes the rabbit.
((("something" "is" "red" "+")) -> ("something" "likes" "rabbit" "+"))
If something eats the rabbit then the rabbit is green.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If something sees the tiger then it is young.
((("something" "sees" "tiger" "+")) -> ("something" "is" "young" "+"))
The rabbit sees the tiger.
True
1
proof
[(triple4)]
("rabbit" "sees" "tiger" "+")
triple4
The tiger is not red.
False
1
inv-proof
[(triple5)]
("tiger" "is" "red" "-")
triple5
The tiger is not round.
Unknown
inv-rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "round" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The rabbit does not eat the tiger.[(triple1)] The rabbit is not round.[(triple2)] The rabbit likes the tiger.[(triple3)] The rabbit sees the tiger.[(triple4)] The tiger is red.[(triple5)] The tiger likes the rabbit.[(triple6 OR ((triple5) -> rule4) OR ((triple3 ((triple4) -> rule6)) -> rule3))] The tiger sees the rabbit.[(triple7)] @1: The rabbit is young.[(((triple4) -> rule6))]
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
triple1
The rabbit is not round.
("rabbit" "is" "round" "-")
triple2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple3
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple4
The tiger is red.
("tiger" "is" "red" "+")
triple5
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple6
((triple5) -> (rule4 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
((triple3 ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple7
The rabbit is young.
("rabbit" "is" "young" "+")
((triple4) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1