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