The dog sees the squirrel. The dog visits the rabbit. The dog visits the tiger. The rabbit is big. The rabbit is kind. The rabbit sees the dog. The rabbit sees the squirrel. The rabbit sees the tiger. The squirrel is kind. The squirrel sees the dog. The squirrel visits the tiger. The tiger is kind. The tiger likes the squirrel. The tiger visits the rabbit. The tiger visits the squirrel. If someone visits the rabbit then the rabbit sees the tiger. If someone sees the rabbit then they like the tiger. If someone sees the dog and they visit the squirrel then the squirrel is big. If the rabbit likes the squirrel and the rabbit visits the dog then the squirrel visits the dog. If someone sees the squirrel then they like the squirrel. If someone sees the tiger then the tiger sees the dog. If someone likes the tiger then the tiger visits the squirrel. If someone is blue then they like the tiger.
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone visits the rabbit then the rabbit sees the tiger.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If someone sees the rabbit then they like the tiger.
((("someone" "sees" "rabbit" "+")) -> ("someone" "likes" "tiger" "+"))
If someone sees the dog and they visit the squirrel then the squirrel is big.
((("someone" "sees" "dog" "+") ("someone" "visits" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
If the rabbit likes the squirrel and the rabbit visits the dog then the squirrel visits the dog.
((("rabbit" "likes" "squirrel" "+") ("rabbit" "visits" "dog" "+")) -> ("squirrel" "visits" "dog" "+"))
If someone sees the squirrel then they like the squirrel.
((("someone" "sees" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone sees the tiger then the tiger sees the dog.
((("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If someone likes the tiger then the tiger visits the squirrel.
((("someone" "likes" "tiger" "+")) -> ("tiger" "visits" "squirrel" "+"))
If someone is blue then they like the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
The squirrel visits the tiger.
True
1
proof
[(triple11)]
("squirrel" "visits" "tiger" "+")
triple11
The dog does not see the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "sees" "squirrel" "-")
triple1
The tiger sees the dog.
True
2
proof
[(((triple8) -> rule6) OR ((((triple14) -> rule1)) -> rule6) OR ((((triple2) -> rule1)) -> rule6))]
("tiger" "sees" "dog" "+")
((triple8) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger does not see the dog.
False
2
inv-proof
[(((triple8) -> rule6) OR ((((triple14) -> rule1)) -> rule6) OR ((((triple2) -> rule1)) -> rule6))]
("tiger" "sees" "dog" "-")
((triple8) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The squirrel is big.
True
4
proof
[(((((triple8) -> rule6) triple15) -> rule3) OR ((((((triple14) -> rule1)) -> rule6) triple15) -> rule3) OR ((((((triple2) -> rule1)) -> rule6) triple15) -> rule3))]
("squirrel" "is" "big" "+")
((((triple8) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((((((triple14) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
The squirrel is not big.
False
4
inv-proof
[(((((triple8) -> rule6) triple15) -> rule3) OR ((((((triple14) -> rule1)) -> rule6) triple15) -> rule3) OR ((((((triple2) -> rule1)) -> rule6) triple15) -> rule3))]
("squirrel" "is" "big" "-")
((((triple8) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((((((triple14) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
The squirrel does not visit the dog.
Unknown
inv-rconc
[@1: The squirrel visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "dog" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The dog sees the squirrel.[(triple1)] The dog visits the rabbit.[(triple2)] The dog visits the tiger.[(triple3)] The rabbit is big.[(triple4)] The rabbit is kind.[(triple5)] The rabbit sees the dog.[(triple6)] The rabbit sees the squirrel.[(triple7)] The rabbit sees the tiger.[(triple8 OR ((triple14) -> rule1) OR ((triple2) -> rule1))] The squirrel is kind.[(triple9)] The squirrel sees the dog.[(triple10)] The squirrel visits the tiger.[(triple11)] The tiger is kind.[(triple12)] The tiger likes the squirrel.[(triple13)] The tiger visits the rabbit.[(triple14)] The tiger visits the squirrel.[(triple15)] @1: The dog likes the squirrel.[(((triple1) -> rule5))] The rabbit likes the squirrel.[(((triple7) -> rule5))] The tiger sees the dog.[(((triple8) -> rule6) OR ((((triple14) -> rule1)) -> rule6) OR ((((triple2) -> rule1)) -> rule6))] @2: The squirrel is big.[(((((triple8) -> rule6) triple15) -> rule3) OR ((((((triple14) -> rule1)) -> rule6) triple15) -> rule3) OR ((((((triple2) -> rule1)) -> rule6) triple15) -> rule3))]
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple6
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple7
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple8
((triple14) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
((triple2) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple10
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple13
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple14
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple15
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((triple1) -> (rule5 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
((triple7) -> (rule5 % int1))
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple8) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple8) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((((((triple14) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3