The rabbit is blue. The rabbit needs the tiger. The tiger eats the rabbit. If something needs the tiger and the tiger is nice then it is not round. If something eats the rabbit then it is round. If the tiger is round and the tiger does not eat the rabbit then the rabbit is green. If something visits the rabbit and the rabbit visits the tiger then it is nice. If something eats the rabbit then the rabbit does not eat the tiger. If something is round and it eats the rabbit then it visits the rabbit.
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If something needs the tiger and the tiger is nice then it is not round.
((("something" "needs" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("something" "is" "round" "-"))
If something eats the rabbit then it is round.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "round" "+"))
If the tiger is round and the tiger does not eat the rabbit then the rabbit is green.
((("tiger" "is" "round" "+") ("tiger" "eats" "rabbit" "~")) -> ("rabbit" "is" "green" "+"))
If something visits the rabbit and the rabbit visits the tiger then it is nice.
((("something" "visits" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("something" "is" "nice" "+"))
If something eats the rabbit then the rabbit does not eat the tiger.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "eats" "tiger" "-"))
If something is round and it eats the rabbit then it visits the rabbit.
((("something" "is" "round" "+") ("something" "eats" "rabbit" "+")) -> ("something" "visits" "rabbit" "+"))
The rabbit is blue.
True
1
proof
[(triple1)]
("rabbit" "is" "blue" "+")
triple1
The tiger does not eat the rabbit.
False
1
inv-proof
[(triple3)]
("tiger" "eats" "rabbit" "-")
triple3
The tiger is round.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "is" "round" "+")
((triple3) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not round.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "is" "round" "-")
((triple3) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the rabbit.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule6))]
("tiger" "visits" "rabbit" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger does not visit the rabbit.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule6))]
("tiger" "visits" "rabbit" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "green" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "nice" "+")
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "nice" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The rabbit is blue.[(triple1)] The rabbit needs the tiger.[(triple2)] The tiger eats the rabbit.[(triple3)] @1: The rabbit does not eat the tiger.[(((triple3) -> rule5))] The tiger is round.[(((triple3) -> rule2))] @2: The tiger visits the rabbit.[(((((triple3) -> rule2) triple3) -> rule6))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple3
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
((triple3) -> (rule5 % int1))
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple3) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2