The dog chases the rabbit. The dog needs the tiger. The rabbit chases the dog. The rabbit is kind. The rabbit is red. The rabbit is rough. The rabbit needs the tiger. The tiger chases the rabbit. The tiger is red. The tiger likes the dog. If someone likes the tiger then the tiger likes the rabbit. If someone chases the dog then the dog chases the tiger. If someone is big then they chase the rabbit. If someone needs the rabbit then the rabbit needs the dog. All kind people are big. If the tiger needs the rabbit and the rabbit needs the tiger then the tiger needs the dog. If someone is rough and they chase the rabbit then the rabbit likes the dog. If someone needs the tiger and they like the tiger then they like the rabbit.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If someone likes the tiger then the tiger likes the rabbit.
((("someone" "likes" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
If someone chases the dog then the dog chases the tiger.
((("someone" "chases" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If someone is big then they chase the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone needs the rabbit then the rabbit needs the dog.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If the tiger needs the rabbit and the rabbit needs the tiger then the tiger needs the dog.
((("tiger" "needs" "rabbit" "+") ("rabbit" "needs" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If someone is rough and they chase the rabbit then the rabbit likes the dog.
((("someone" "is" "rough" "+") ("someone" "chases" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
If someone needs the tiger and they like the tiger then they like the rabbit.
((("someone" "needs" "tiger" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "likes" "rabbit" "+"))
The rabbit is kind.
True
1
proof
[(triple4)]
("rabbit" "is" "kind" "+")
triple4
The tiger does not chase the rabbit.
False
1
inv-proof
[(triple8)]
("tiger" "chases" "rabbit" "-")
triple8
The dog chases the tiger.
True
2
proof
[(((triple3) -> rule2))]
("dog" "chases" "tiger" "+")
((triple3) -> (rule2 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog does not chase the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "chases" "tiger" "-")
((triple3) -> (rule2 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The rabbit chases the rabbit.
True
3
proof
[(((((triple4) -> rule5)) -> rule3))]
("rabbit" "chases" "rabbit" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule3))]
("rabbit" "chases" "rabbit" "-")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit likes the dog.
True
5
proof
[(((triple6 ((((triple4) -> rule5)) -> rule3)) -> rule7))]
("rabbit" "likes" "dog" "+")
((triple6 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit does not like the dog.
False
5
inv-proof
[(((triple6 ((((triple4) -> rule5)) -> rule3)) -> rule7))]
("rabbit" "likes" "dog" "-")
((triple6 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit needs the dog.
Unknown
rconc
[@1: The rabbit needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "needs" "dog" "+")
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "big" "-")
The tiger likes the rabbit.
Unknown
rconc
[@1: The tiger likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "rabbit" "+")
The dog does not need the rabbit.
Unknown
inv-random
[@0: The dog needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "rabbit" "-")
The tiger chases the dog.
Unknown
random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
@0: The dog chases the rabbit.[(triple1)] The dog needs the tiger.[(triple2)] The rabbit chases the dog.[(triple3)] The rabbit is kind.[(triple4)] The rabbit is red.[(triple5)] The rabbit is rough.[(triple6)] The rabbit needs the tiger.[(triple7)] The tiger chases the rabbit.[(triple8)] The tiger is red.[(triple9)] The tiger likes the dog.[(triple10)] @1: The dog chases the tiger.[(((triple3) -> rule2))] The rabbit is big.[(((triple4) -> rule5))] @2: The rabbit chases the rabbit.[(((((triple4) -> rule5)) -> rule3))] @3: The rabbit likes the dog.[(((triple6 ((((triple4) -> rule5)) -> rule3)) -> rule7))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple6
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple7
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple10
The dog chases the tiger.
("dog" "chases" "tiger" "+")
((triple3) -> (rule2 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple4) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple4) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
((triple6 ((((triple4) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3