The dog visits the tiger. The rabbit eats the dog. The rabbit eats the tiger. The rabbit is not green. The rabbit is rough. The rabbit is round. The tiger eats the dog. The tiger eats the rabbit. The tiger is green. The tiger needs the dog. The tiger needs the rabbit. The tiger visits the dog. If someone is green and nice then they do not need the rabbit. If someone visits the tiger and they eat the rabbit then the rabbit visits the dog. If someone visits the rabbit and the rabbit is red then the rabbit does not visit the dog. If someone needs the tiger and the tiger visits the rabbit then they are rough. If the tiger is green then the tiger visits the rabbit. If someone needs the rabbit then they are green. If someone visits the dog then the dog needs the tiger. If someone is red and they do not visit the dog then they eat the tiger.
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone is green and nice then they do not need the rabbit.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "rabbit" "-"))
If someone visits the tiger and they eat the rabbit then the rabbit visits the dog.
((("someone" "visits" "tiger" "+") ("someone" "eats" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If someone visits the rabbit and the rabbit is red then the rabbit does not visit the dog.
((("someone" "visits" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("rabbit" "visits" "dog" "-"))
If someone needs the tiger and the tiger visits the rabbit then they are rough.
((("someone" "needs" "tiger" "+") ("tiger" "visits" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
If the tiger is green then the tiger visits the rabbit.
((("tiger" "is" "green" "+")) -> ("tiger" "visits" "rabbit" "+"))
If someone needs the rabbit then they are green.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If someone visits the dog then the dog needs the tiger.
((("someone" "visits" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If someone is red and they do not visit the dog then they eat the tiger.
((("someone" "is" "red" "+") ("someone" "visits" "dog" "~")) -> ("someone" "eats" "tiger" "+"))
The tiger needs the rabbit.
True
1
proof
[(triple11)]
("tiger" "needs" "rabbit" "+")
triple11
The rabbit is not round.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "round" "-")
triple6
The dog needs the tiger.
True
2
proof
[(((triple12) -> rule7))]
("dog" "needs" "tiger" "+")
((triple12) -> (rule7 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog does not need the tiger.
False
2
inv-proof
[(((triple12) -> rule7))]
("dog" "needs" "tiger" "-")
((triple12) -> (rule7 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog is rough.
True
5
proof
[(((((triple12) -> rule7) ((triple9) -> rule5)) -> rule4) OR ((((triple12) -> rule7) ((((triple11) -> rule6)) -> rule5)) -> rule4))]
("dog" "is" "rough" "+")
((((triple12) -> (rule7 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
((((triple12) -> (rule7 % int4)) ((((triple11) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int4
The dog is not rough.
False
5
inv-proof
[(((((triple12) -> rule7) ((triple9) -> rule5)) -> rule4) OR ((((triple12) -> rule7) ((((triple11) -> rule6)) -> rule5)) -> rule4))]
("dog" "is" "rough" "-")
((((triple12) -> (rule7 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
((((triple12) -> (rule7 % int4)) ((((triple11) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int4
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "rough" "-")
The dog eats the tiger.
Unknown
rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "eats" "tiger" "+")
The dog is not green.
Unknown
inv-rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "green" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
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 dog visits the rabbit.
Unknown
random
[@0: The dog visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "rabbit" "+")
@0: The dog visits the tiger.[(triple1)] The rabbit eats the dog.[(triple2)] The rabbit eats the tiger.[(triple3)] The rabbit is not green.[(triple4)] The rabbit is rough.[(triple5)] The rabbit is round.[(triple6)] The tiger eats the dog.[(triple7)] The tiger eats the rabbit.[(triple8)] The tiger is green.[(triple9 OR ((triple11) -> rule6))] The tiger needs the dog.[(triple10)] The tiger needs the rabbit.[(triple11)] The tiger visits the dog.[(triple12)] @1: The dog needs the tiger.[(((triple12) -> rule7))] The tiger visits the rabbit.[(((triple9) -> rule5) OR ((((triple11) -> rule6)) -> rule5))] @2: The dog is rough.[(((((triple12) -> rule7) ((triple9) -> rule5)) -> rule4) OR ((((triple12) -> rule7) ((((triple11) -> rule6)) -> rule5)) -> rule4))]
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple2
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple3
The rabbit is not green.
("rabbit" "is" "green" "-")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple7
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
((triple11) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((triple12) -> (rule7 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple9) -> (rule5 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
((((triple11) -> (rule6 % int2))) -> (rule5 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((triple12) -> (rule7 % int3)) ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int3
((((triple12) -> (rule7 % int4)) ((((triple11) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int4