The lion chases the tiger. The lion likes the tiger. The rabbit is blue. The rabbit is nice. The rabbit visits the tiger. The tiger chases the lion. The tiger chases the rabbit. The tiger is nice. The tiger is rough. The tiger visits the rabbit. If something chases the lion then it visits the tiger.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something chases the lion then it visits the tiger.
((("something" "chases" "lion" "+")) -> ("something" "visits" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple8)]
("tiger" "is" "nice" "+")
triple8
The lion does not chase the tiger.
False
1
inv-proof
[(triple1)]
("lion" "chases" "tiger" "-")
triple1
The tiger visits the tiger.
True
2
proof
[(((triple6) -> rule1))]
("tiger" "visits" "tiger" "+")
((triple6) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple6) -> rule1))]
("tiger" "visits" "tiger" "-")
((triple6) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The lion does not visit the tiger.
Unknown
inv-rconc
[@1: The lion visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "tiger" "-")
The lion visits the rabbit.
Unknown
random
[@0: The lion visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "rabbit" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The lion likes the rabbit.
Unknown
random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "+")
@0: The lion chases the tiger.[(triple1)] The lion likes the tiger.[(triple2)] The rabbit is blue.[(triple3)] The rabbit is nice.[(triple4)] The rabbit visits the tiger.[(triple5)] The tiger chases the lion.[(triple6)] The tiger chases the rabbit.[(triple7)] The tiger is nice.[(triple8)] The tiger is rough.[(triple9)] The tiger visits the rabbit.[(triple10)] @1: The tiger visits the tiger.[(((triple6) -> rule1))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple5
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple6
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple6) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1