The dog is green. The lion is rough. The lion is round. The lion sees the tiger. The lion visits the tiger. The rabbit is green. The rabbit is rough. The tiger eats the dog. The tiger eats the rabbit. The tiger is blue. The tiger is rough. The tiger sees the lion. If someone visits the lion then the lion eats the tiger. If someone visits the dog and the dog sees the rabbit then the dog is blue. If someone visits the tiger then the tiger visits the dog. If someone is green then they see the rabbit. If someone is blue then they eat the tiger. If someone is round and they visit the lion then the lion eats the tiger. If someone visits the tiger then the tiger is rough. If the lion visits the dog then the lion visits the rabbit.
The dog is green.
("dog" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone visits the lion then the lion eats the tiger.
((("someone" "visits" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
If someone visits the dog and the dog sees the rabbit then the dog is blue.
((("someone" "visits" "dog" "+") ("dog" "sees" "rabbit" "+")) -> ("dog" "is" "blue" "+"))
If someone visits the tiger then the tiger visits the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If someone is green then they see the rabbit.
((("someone" "is" "green" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is blue then they eat the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is round and they visit the lion then the lion eats the tiger.
((("someone" "is" "round" "+") ("someone" "visits" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
If someone visits the tiger then the tiger is rough.
((("someone" "visits" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If the lion visits the dog then the lion visits the rabbit.
((("lion" "visits" "dog" "+")) -> ("lion" "visits" "rabbit" "+"))
The lion is round.
True
1
proof
[(triple3)]
("lion" "is" "round" "+")
triple3
The tiger is not blue.
False
1
inv-proof
[(triple10)]
("tiger" "is" "blue" "-")
triple10
The tiger visits the dog.
True
2
proof
[(((triple5) -> rule3))]
("tiger" "visits" "dog" "+")
((triple5) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The rabbit does not see the rabbit.
False
2
inv-proof
[(((triple6) -> rule4))]
("rabbit" "sees" "rabbit" "-")
((triple6) -> (rule4 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The dog is blue.
True
5
proof
[(((((triple5) -> rule3) ((triple1) -> rule4)) -> rule2))]
("dog" "is" "blue" "+")
((((triple5) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The dog is not blue.
False
5
inv-proof
[(((((triple5) -> rule3) ((triple1) -> rule4)) -> rule2))]
("dog" "is" "blue" "-")
((((triple5) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The dog eats the tiger.
True
6
proof
[(((((((triple5) -> rule3) ((triple1) -> rule4)) -> rule2)) -> rule5))]
("dog" "eats" "tiger" "+")
((((((triple5) -> (rule3 % int4)) ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The dog does not eat the tiger.
False
6
inv-proof
[(((((((triple5) -> rule3) ((triple1) -> rule4)) -> rule2)) -> rule5))]
("dog" "eats" "tiger" "-")
((((((triple5) -> (rule3 % int4)) ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4
The lion does not eat the tiger.
Unknown
inv-rconc
[@1: The lion eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "tiger" "-")
The tiger sees the rabbit.
Unknown
rconc
[@1: The tiger sees the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "rabbit" "+")
The lion does not visit the rabbit.
Unknown
inv-rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "visits" "rabbit" "-")
The lion sees the rabbit.
Unknown
rconc
[@1: The lion sees the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "rabbit" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
The rabbit does not see the lion.
Unknown
inv-random
[@0: The rabbit sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "lion" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The dog is green.[(triple1)] The lion is rough.[(triple2)] The lion is round.[(triple3)] The lion sees the tiger.[(triple4)] The lion visits the tiger.[(triple5)] The rabbit is green.[(triple6)] The rabbit is rough.[(triple7)] The tiger eats the dog.[(triple8)] The tiger eats the rabbit.[(triple9)] The tiger is blue.[(triple10)] The tiger is rough.[(triple11 OR ((triple5) -> rule7))] The tiger sees the lion.[(triple12)] @1: The dog sees the rabbit.[(((triple1) -> rule4))] The rabbit sees the rabbit.[(((triple6) -> rule4))] The tiger eats the tiger.[(((triple10) -> rule5))] The tiger visits the dog.[(((triple5) -> rule3))] @2: The dog is blue.[(((((triple5) -> rule3) ((triple1) -> rule4)) -> rule2))] @3: The dog eats the tiger.[(((((((triple5) -> rule3) ((triple1) -> rule4)) -> rule2)) -> rule5))]
The dog is green.
("dog" "is" "green" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple5
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple7
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple8
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
((triple5) -> (rule7 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple12
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple1) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple6) -> (rule4 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple10) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple5) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple5) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((((((triple5) -> (rule3 % int4)) ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int4