The cat is nice. The lion sees the tiger. The tiger visits the cat. If something visits the tiger then it visits the lion. If something visits the cat then the cat visits the tiger. If the tiger visits the lion then the tiger sees the lion.
The cat is nice.
("cat" "is" "nice" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something visits the tiger then it visits the lion.
((("something" "visits" "tiger" "+")) -> ("something" "visits" "lion" "+"))
If something visits the cat then the cat visits the tiger.
((("something" "visits" "cat" "+")) -> ("cat" "visits" "tiger" "+"))
If the tiger visits the lion then the tiger sees the lion.
((("tiger" "visits" "lion" "+")) -> ("tiger" "sees" "lion" "+"))
The tiger visits the cat.
True
1
proof
[(triple3)]
("tiger" "visits" "cat" "+")
triple3
The tiger does not visit the cat.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "cat" "-")
triple3
The cat visits the tiger.
True
2
proof
[(((triple3) -> rule2))]
("cat" "visits" "tiger" "+")
((triple3) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("cat" "visits" "tiger" "-")
((triple3) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat visits the lion.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("cat" "visits" "lion" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The cat does not visit the lion.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("cat" "visits" "lion" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "lion" "-")
The tiger sees the lion.
Unknown
rconc
[@2: The tiger sees the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("tiger" "sees" "lion" "+")
The tiger does not visit the lion.
Unknown
inv-rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "lion" "-")
The tiger chases the cat.
Unknown
random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The lion visits the tiger.
Unknown
random
[@0: The lion visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "tiger" "+")
@0: The cat is nice.[(triple1)] The lion sees the tiger.[(triple2)] The tiger visits the cat.[(triple3)] @1: The cat visits the tiger.[(((triple3) -> rule2))] @2: The cat visits the lion.[(((((triple3) -> rule2)) -> rule1))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple3) -> (rule2 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int2