The lion chases the rabbit. The lion likes the rabbit. The rabbit is red. The rabbit is round. The rabbit visits the tiger. The tiger is not young. The tiger does not like the rabbit. If something visits the rabbit then it is kind. If something is round and kind then it does not like the lion. If something is red then it chases the tiger. If something visits the lion then the lion chases the tiger. If something is young and it likes the rabbit then the rabbit does not chase the lion. If something is red then it visits the rabbit.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger does not like the rabbit.
("tiger" "likes" "rabbit" "-")
If something visits the rabbit then it is kind.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "kind" "+"))
If something is round and kind then it does not like the lion.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "likes" "lion" "-"))
If something is red then it chases the tiger.
((("something" "is" "red" "+")) -> ("something" "chases" "tiger" "+"))
If something visits the lion then the lion chases the tiger.
((("something" "visits" "lion" "+")) -> ("lion" "chases" "tiger" "+"))
If something is young and it likes the rabbit then the rabbit does not chase the lion.
((("something" "is" "young" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "chases" "lion" "-"))
If something is red then it visits the rabbit.
((("something" "is" "red" "+")) -> ("something" "visits" "rabbit" "+"))
The rabbit is round.
True
1
proof
[(triple4)]
("rabbit" "is" "round" "+")
triple4
The lion does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("lion" "chases" "rabbit" "-")
triple1
The rabbit visits the rabbit.
True
2
proof
[(((triple3) -> rule6))]
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not chase the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("rabbit" "chases" "tiger" "-")
((triple3) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit is kind.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("rabbit" "is" "kind" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is not kind.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("rabbit" "is" "kind" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit does not like the lion.
True
5
proof
[(((triple4 ((((triple3) -> rule6)) -> rule1)) -> rule2))]
("rabbit" "likes" "lion" "-")
((triple4 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit likes the lion.
False
5
inv-proof
[(((triple4 ((((triple3) -> rule6)) -> rule1)) -> rule2))]
("rabbit" "likes" "lion" "+")
((triple4 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The tiger does not visit the rabbit.
Unknown
inv-rconc
[@1: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "visits" "rabbit" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger is not kind.
Unknown
inv-rconc
[@2: The tiger is kind.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("tiger" "is" "kind" "-")
The lion is kind.
Unknown
rconc
[@2: The lion is kind.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("lion" "is" "kind" "+")
The lion does not visit the tiger.
Unknown
inv-random
[@0: The lion visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "tiger" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The rabbit does not chase the lion.
Unknown
inv-random
[@0: The rabbit chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "lion" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The lion chases the rabbit.[(triple1)] The lion likes the rabbit.[(triple2)] The rabbit is red.[(triple3)] The rabbit is round.[(triple4)] The rabbit visits the tiger.[(triple5)] The tiger does not like the rabbit.[(triple7)] The tiger is not young.[(triple6)] @1: The rabbit chases the tiger.[(((triple3) -> rule3))] The rabbit visits the rabbit.[(((triple3) -> rule6))] @2: The rabbit is kind.[(((((triple3) -> rule6)) -> rule1))] @3: The rabbit does not like the lion.[(((triple4 ((((triple3) -> rule6)) -> rule1)) -> rule2))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple5
The tiger does not like the rabbit.
("tiger" "likes" "rabbit" "-")
triple7
The tiger is not young.
("tiger" "is" "young" "-")
triple6
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
((triple3) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
((triple4 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3