The dog chases the rabbit. The dog chases the tiger. The dog is not round. The dog visits the rabbit. The rabbit is round. The rabbit visits the dog. The rabbit visits the tiger. The tiger is round. The tiger needs the rabbit. The tiger visits the rabbit. If someone chases the rabbit then they visit the dog. If someone visits the dog and the dog visits the rabbit then the rabbit chases the dog. If someone needs the tiger then the tiger chases the dog. If the tiger is round then the tiger does not chase the rabbit. If someone is round and green then they visit the rabbit. If someone chases the dog then they are green.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is not round.
("dog" "is" "round" "-")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone chases the rabbit then they visit the dog.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the dog and the dog visits the rabbit then the rabbit chases the dog.
((("someone" "visits" "dog" "+") ("dog" "visits" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If someone needs the tiger then the tiger chases the dog.
((("someone" "needs" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If the tiger is round then the tiger does not chase the rabbit.
((("tiger" "is" "round" "+")) -> ("tiger" "chases" "rabbit" "-"))
If someone is round and green then they visit the rabbit.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone chases the dog then they are green.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "green" "+"))
The dog chases the tiger.
True
1
proof
[(triple2)]
("dog" "chases" "tiger" "+")
triple2
The tiger does not need the rabbit.
False
1
inv-proof
[(triple9)]
("tiger" "needs" "rabbit" "-")
triple9
The tiger does not chase the rabbit.
True
2
proof
[(((triple8) -> rule4))]
("tiger" "chases" "rabbit" "-")
((triple8) -> (rule4 % int1))
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
int1
The rabbit does not chase the dog.
False
3
inv-proof
[(((triple6 triple4) -> rule2) OR ((((triple1) -> rule1) triple4) -> rule2))]
("rabbit" "chases" "dog" "-")
((triple6 triple4) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
((((triple1) -> (rule1 % int2)) triple4) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The rabbit is green.
True
4
proof
[(((((triple6 triple4) -> rule2)) -> rule6) OR ((((((triple1) -> rule1) triple4) -> rule2)) -> rule6))]
("rabbit" "is" "green" "+")
((((triple6 triple4) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
((((((triple1) -> (rule1 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The rabbit is not green.
False
4
inv-proof
[(((((triple6 triple4) -> rule2)) -> rule6) OR ((((((triple1) -> rule1) triple4) -> rule2)) -> rule6))]
("rabbit" "is" "green" "-")
((((triple6 triple4) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
((((((triple1) -> (rule1 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The rabbit visits the rabbit.
True
6
proof
[(((triple5 ((((triple6 triple4) -> rule2)) -> rule6)) -> rule5) OR ((triple5 ((((((triple1) -> rule1) triple4) -> rule2)) -> rule6)) -> rule5))]
("rabbit" "visits" "rabbit" "+")
((triple5 ((((triple6 triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
((triple5 ((((((triple1) -> (rule1 % int4)) triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4
The rabbit does not visit the rabbit.
False
6
inv-proof
[(((triple5 ((((triple6 triple4) -> rule2)) -> rule6)) -> rule5) OR ((triple5 ((((((triple1) -> rule1) triple4) -> rule2)) -> rule6)) -> rule5))]
("rabbit" "visits" "rabbit" "-")
((triple5 ((((triple6 triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
((triple5 ((((((triple1) -> (rule1 % int4)) triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4
The dog is not green.
Unknown
inv-rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "green" "-")
The tiger visits the dog.
Unknown
rconc
[@1: The tiger visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "dog" "+")
The tiger does not chase the dog.
Unknown
inv-rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "dog" "-")
The tiger is green.
Unknown
rconc
[@2: The tiger is green.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("tiger" "is" "green" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The dog chases the rabbit.[(triple1)] The dog chases the tiger.[(triple2)] The dog is not round.[(triple3)] The dog visits the rabbit.[(triple4)] The rabbit is round.[(triple5)] The rabbit visits the dog.[(triple6)] The rabbit visits the tiger.[(triple7)] The tiger is round.[(triple8)] The tiger needs the rabbit.[(triple9)] The tiger visits the rabbit.[(triple10)] @1: The dog visits the dog.[(((triple1) -> rule1))] The rabbit chases the dog.[(((triple6 triple4) -> rule2) OR ((((triple1) -> rule1) triple4) -> rule2))] The tiger does not chase the rabbit.[(((triple8) -> rule4))] @2: The rabbit is green.[(((((triple6 triple4) -> rule2)) -> rule6) OR ((((((triple1) -> rule1) triple4) -> rule2)) -> rule6))] @3: The rabbit visits the rabbit.[(((triple5 ((((triple6 triple4) -> rule2)) -> rule6)) -> rule5) OR ((triple5 ((((((triple1) -> rule1) triple4) -> rule2)) -> rule6)) -> rule5))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The dog is not round.
("dog" "is" "round" "-")
triple3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple6
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple7
The tiger is round.
("tiger" "is" "round" "+")
triple8
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple9
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple1) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((triple6 triple4) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
((((triple1) -> (rule1 % int2)) triple4) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
((triple8) -> (rule4 % int1))
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((((triple6 triple4) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
((((((triple1) -> (rule1 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple5 ((((triple6 triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
((triple5 ((((((triple1) -> (rule1 % int4)) triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4