The bear chases the lion. The bear chases the tiger. The lion chases the rabbit. The lion chases the tiger. The rabbit does not chase the lion. The rabbit is cold. The tiger sees the rabbit. If something visits the lion and it is nice then it does not see the lion. If something is cold then it does not visit the rabbit. If the rabbit does not see the lion then the rabbit chases the tiger.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something visits the lion and it is nice then it does not see the lion.
((("something" "visits" "lion" "+") ("something" "is" "nice" "+")) -> ("something" "sees" "lion" "-"))
If something is cold then it does not visit the rabbit.
((("something" "is" "cold" "+")) -> ("something" "visits" "rabbit" "-"))
If the rabbit does not see the lion then the rabbit chases the tiger.
((("rabbit" "sees" "lion" "~")) -> ("rabbit" "chases" "tiger" "+"))
The lion chases the rabbit.
True
1
proof
[(triple3)]
("lion" "chases" "rabbit" "+")
triple3
The bear does not chase the tiger.
False
1
inv-proof
[(triple2)]
("bear" "chases" "tiger" "-")
triple2
The rabbit does not visit the rabbit.
True
2
proof
[(((triple6) -> rule2))]
("rabbit" "visits" "rabbit" "-")
((triple6) -> (rule2 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit visits the rabbit.
False
2
inv-proof
[(((triple6) -> rule2))]
("rabbit" "visits" "rabbit" "+")
((triple6) -> (rule2 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit does not chase the tiger.
Unknown
inv-rconc
[@1: The rabbit chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "tiger" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The tiger does not visit the bear.
Unknown
inv-random
[@0: The tiger visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "bear" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The bear chases the lion.[(triple1)] The bear chases the tiger.[(triple2)] The lion chases the rabbit.[(triple3)] The lion chases the tiger.[(triple4)] The rabbit does not chase the lion.[(triple5)] The rabbit is cold.[(triple6)] The tiger sees the rabbit.[(triple7)] @1: The rabbit does not visit the rabbit.[(((triple6) -> rule2))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple4
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple7
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
((triple6) -> (rule2 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1