The cat likes the lion. The cat likes the tiger. The lion is cold. The lion likes the tiger. The tiger chases the cat. The tiger chases the lion. The tiger visits the lion. If someone likes the lion then the lion visits the cat. If someone likes the cat then they chase the tiger. If someone visits the cat then the cat chases the tiger. If someone is nice then they like the tiger. If someone likes the cat and the cat likes the lion then they chase the cat. If someone chases the tiger then they visit the lion.
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone likes the lion then the lion visits the cat.
((("someone" "likes" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone likes the cat then they chase the tiger.
((("someone" "likes" "cat" "+")) -> ("someone" "chases" "tiger" "+"))
If someone visits the cat then the cat chases the tiger.
((("someone" "visits" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If someone is nice then they like the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the cat and the cat likes the lion then they chase the cat.
((("someone" "likes" "cat" "+") ("cat" "likes" "lion" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the tiger then they visit the lion.
((("someone" "chases" "tiger" "+")) -> ("someone" "visits" "lion" "+"))
The tiger chases the lion.
True
1
proof
[(triple6)]
("tiger" "chases" "lion" "+")
triple6
The cat does not like the tiger.
False
1
inv-proof
[(triple2)]
("cat" "likes" "tiger" "-")
triple2
The lion visits the cat.
True
2
proof
[(((triple1) -> rule1))]
("lion" "visits" "cat" "+")
((triple1) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "visits" "cat" "-")
((triple1) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat chases the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("cat" "chases" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat does not chase the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("cat" "chases" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat visits the lion.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule6))]
("cat" "visits" "lion" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat does not visit the lion.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule6))]
("cat" "visits" "lion" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "cat" "+")
The lion does not chase the cat.
Unknown
inv-rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "cat" "-")
The lion chases the tiger.
Unknown
rconc
[@1: The lion chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "tiger" "+")
The tiger does not like the lion.
Unknown
inv-random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The cat chases the lion.
Unknown
random
[@0: The cat chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "lion" "+")
@0: The cat likes the lion.[(triple1)] The cat likes the tiger.[(triple2)] The lion is cold.[(triple3)] The lion likes the tiger.[(triple4)] The tiger chases the cat.[(triple5)] The tiger chases the lion.[(triple6)] The tiger visits the lion.[(triple7)] @1: The lion visits the cat.[(((triple1) -> rule1))] @2: The cat chases the tiger.[(((((triple1) -> rule1)) -> rule3))] @3: The cat visits the lion.[(((((((triple1) -> rule1)) -> rule3)) -> rule6))]
The cat likes the lion.
("cat" "likes" "lion" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple5
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple6
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple7
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple1) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3