The bear is blue. The bear is nice. The bear sees the tiger. The dog needs the bear. The dog sees the tiger. The rabbit needs the dog. The tiger is rough. If someone is nice then they are rough. If someone is rough then they see the rabbit. All rough people are kind. If someone chases the rabbit and the rabbit is kind then they need the dog. If someone is green then they are nice. If someone is kind and they chase the bear then they chase the tiger. If someone chases the bear then they chase the rabbit. If the bear sees the rabbit then the rabbit is green. If the rabbit needs the dog then the rabbit sees the tiger.
The bear is blue.
("bear" "is" "blue" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they see the rabbit.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "rabbit" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the rabbit and the rabbit is kind then they need the dog.
((("someone" "chases" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("someone" "needs" "dog" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind and they chase the bear then they chase the tiger.
((("someone" "is" "kind" "+") ("someone" "chases" "bear" "+")) -> ("someone" "chases" "tiger" "+"))
If someone chases the bear then they chase the rabbit.
((("someone" "chases" "bear" "+")) -> ("someone" "chases" "rabbit" "+"))
If the bear sees the rabbit then the rabbit is green.
((("bear" "sees" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If the rabbit needs the dog then the rabbit sees the tiger.
((("rabbit" "needs" "dog" "+")) -> ("rabbit" "sees" "tiger" "+"))
The bear is blue.
True
1
proof
[(triple1)]
("bear" "is" "blue" "+")
triple1
The bear is not blue.
False
1
inv-proof
[(triple1)]
("bear" "is" "blue" "-")
triple1
The tiger sees the rabbit.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "sees" "rabbit" "+")
((triple7) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit does not see the tiger.
False
2
inv-proof
[(((triple6) -> rule9))]
("rabbit" "sees" "tiger" "-")
((triple6) -> (rule9 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The bear is kind.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("bear" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear does not see the rabbit.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("bear" "sees" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The rabbit is green.
True
4
proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule8))]
("rabbit" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The rabbit is not green.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule8))]
("rabbit" "is" "green" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The rabbit is nice.
True
5
proof
[(((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5))]
("rabbit" "is" "nice" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
int4
The rabbit is not nice.
False
5
inv-proof
[(((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5))]
("rabbit" "is" "nice" "-")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
int4
The rabbit is rough.
True
6
proof
[(((((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5)) -> rule1))]
("rabbit" "is" "rough" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int4
The bear is rough.
("bear" "is" "rough" "+")
int5
The rabbit is not rough.
False
6
inv-proof
[(((((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5)) -> rule1))]
("rabbit" "is" "rough" "-")
((((((((((triple2) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int4
The bear is rough.
("bear" "is" "rough" "+")
int5
The dog is not kind.
Unknown
inv-rconc
[@3: The dog is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule5 <- FAIL)]]
("dog" "is" "kind" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "nice" "-")
The bear needs the dog.
Unknown
rconc
[@2: The bear needs the dog.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("bear" "needs" "dog" "+")
The dog is not rough.
Unknown
inv-rconc
[@2: The dog is rough.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("dog" "is" "rough" "-")
The tiger chases the rabbit.
Unknown
rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "chases" "rabbit" "+")
The bear does not need the rabbit.
Unknown
inv-random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "-")
The tiger chases the bear.
Unknown
random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "+")
The rabbit does not see the dog.
Unknown
inv-random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "-")
The bear sees the dog.
Unknown
random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "+")
The tiger does not chase the dog.
Unknown
inv-random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "-")
The rabbit chases the dog.
Unknown
random
[@0: The rabbit chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "dog" "+")
@0: The bear is blue.[(triple1)] The bear is nice.[(triple2)] The bear sees the tiger.[(triple3)] The dog needs the bear.[(triple4)] The dog sees the tiger.[(triple5)] The rabbit needs the dog.[(triple6)] The tiger is rough.[(triple7)] @1: The bear is rough.[(((triple2) -> rule1))] The rabbit sees the tiger.[(((triple6) -> rule9))] The tiger is kind.[(((triple7) -> rule3))] The tiger sees the rabbit.[(((triple7) -> rule2))] @2: The bear is kind.[(((((triple2) -> rule1)) -> rule3))] The bear sees the rabbit.[(((((triple2) -> rule1)) -> rule2))] @3: The rabbit is green.[(((((((triple2) -> rule1)) -> rule2)) -> rule8))] @4: The rabbit is nice.[(((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5))] @5: The rabbit is rough.[(((((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5)) -> rule1))] @6: The rabbit is kind.[(((((((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5)) -> rule1)) -> rule3))] The rabbit sees the rabbit.[(((((((((((((triple2) -> rule1)) -> rule2)) -> rule8)) -> rule5)) -> rule1)) -> rule2))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple3
The dog needs the bear.
("dog" "needs" "bear" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The bear is rough.
("bear" "is" "rough" "+")
((triple2) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((triple6) -> (rule9 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple7) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple7) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((((((((triple2) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int4
The bear is rough.
("bear" "is" "rough" "+")
int5
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((((((((((triple2) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int5
The bear is rough.
("bear" "is" "rough" "+")
int6
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((((((triple2) -> (rule1 % int6))) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int5
The bear is rough.
("bear" "is" "rough" "+")
int6