The dog is red. The dog needs the rabbit. The dog sees the tiger. The rabbit is kind. The rabbit likes the squirrel. The squirrel sees the tiger. The tiger is kind. The tiger is nice. The tiger is red. The tiger sees the rabbit. If something needs the squirrel and it needs the rabbit then it is red. If something sees the rabbit then the rabbit needs the squirrel. If something likes the rabbit then it sees the tiger. If something sees the rabbit then it is young. If the dog is green then the dog needs the rabbit. If something sees the squirrel then it likes the dog. If something is green and kind then it sees the squirrel. If something is red then it sees the rabbit.
The dog is red.
("dog" "is" "red" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something needs the squirrel and it needs the rabbit then it is red.
((("something" "needs" "squirrel" "+") ("something" "needs" "rabbit" "+")) -> ("something" "is" "red" "+"))
If something sees the rabbit then the rabbit needs the squirrel.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If something likes the rabbit then it sees the tiger.
((("something" "likes" "rabbit" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the rabbit then it is young.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "young" "+"))
If the dog is green then the dog needs the rabbit.
((("dog" "is" "green" "+")) -> ("dog" "needs" "rabbit" "+"))
If something sees the squirrel then it likes the dog.
((("something" "sees" "squirrel" "+")) -> ("something" "likes" "dog" "+"))
If something is green and kind then it sees the squirrel.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "sees" "squirrel" "+"))
If something is red then it sees the rabbit.
((("something" "is" "red" "+")) -> ("something" "sees" "rabbit" "+"))
The rabbit is kind.
True
1
proof
[(triple4)]
("rabbit" "is" "kind" "+")
triple4
The rabbit does not like the squirrel.
False
1
inv-proof
[(triple5)]
("rabbit" "likes" "squirrel" "-")
triple5
The rabbit needs the squirrel.
True
2
proof
[(((triple10) -> rule2) OR ((((triple1) -> rule8)) -> rule2) OR ((((triple9) -> rule8)) -> rule2))]
("rabbit" "needs" "squirrel" "+")
((triple10) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
((((triple9) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The tiger is not young.
False
2
inv-proof
[(((triple10) -> rule4) OR ((((triple9) -> rule8)) -> rule4))]
("tiger" "is" "young" "-")
((triple10) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The dog is young.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("dog" "is" "young" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog is not young.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("dog" "is" "young" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@2: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
The dog does not like the tiger.
Unknown
inv-random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "-")
The squirrel needs the dog.
Unknown
random
[@0: The squirrel needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "dog" "+")
@0: The dog is red.[(triple1)] The dog needs the rabbit.[(triple2)] The dog sees the tiger.[(triple3)] The rabbit is kind.[(triple4)] The rabbit likes the squirrel.[(triple5)] The squirrel sees the tiger.[(triple6)] The tiger is kind.[(triple7)] The tiger is nice.[(triple8)] The tiger is red.[(triple9)] The tiger sees the rabbit.[(triple10 OR ((triple9) -> rule8))] @1: The dog sees the rabbit.[(((triple1) -> rule8))] The rabbit needs the squirrel.[(((triple10) -> rule2) OR ((((triple1) -> rule8)) -> rule2) OR ((((triple9) -> rule8)) -> rule2))] The tiger is young.[(((triple10) -> rule4) OR ((((triple9) -> rule8)) -> rule4))] @2: The dog is young.[(((((triple1) -> rule8)) -> rule4))]
The dog is red.
("dog" "is" "red" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple5
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
((triple9) -> (rule8 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple1) -> (rule8 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
((triple10) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
((((triple9) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((triple10) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple9) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2