The dog needs the rabbit. The lion eats the rabbit. The lion eats the tiger. The lion is round. The rabbit is big. The tiger is big. The tiger is rough. If someone is round then they are green. If someone needs the rabbit then the rabbit is round. If the rabbit needs the dog and the dog is not green then the rabbit is big.
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is round.
("lion" "is" "round" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone needs the rabbit then the rabbit is round.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If the rabbit needs the dog and the dog is not green then the rabbit is big.
((("rabbit" "needs" "dog" "+") ("dog" "is" "green" "~")) -> ("rabbit" "is" "big" "+"))
The dog needs the rabbit.
True
1
proof
[(triple1)]
("dog" "needs" "rabbit" "+")
triple1
The tiger is not rough.
False
1
inv-proof
[(triple7)]
("tiger" "is" "rough" "-")
triple7
The rabbit is round.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "is" "round" "+")
((triple1) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "is" "round" "-")
((triple1) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is green.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is not green.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "is" "green" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "green" "-")
The dog is green.
Unknown
rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "green" "+")
The dog does not need the tiger.
Unknown
inv-random
[@0: The dog needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The lion does not chase the tiger.
Unknown
inv-random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The dog needs the rabbit.[(triple1)] The lion eats the rabbit.[(triple2)] The lion eats the tiger.[(triple3)] The lion is round.[(triple4)] The rabbit is big.[(triple5)] The tiger is big.[(triple6)] The tiger is rough.[(triple7)] @1: The lion is green.[(((triple4) -> rule1))] The rabbit is round.[(((triple1) -> rule2))] @2: The rabbit is green.[(((((triple1) -> rule2)) -> rule1))]
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
((triple4) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2