The cat likes the tiger. The lion likes the cat. The tiger is kind. If someone visits the tiger then the tiger likes the cat. If someone likes the cat then they do not visit the tiger. If someone is green and they visit the lion then they visit the tiger. If someone likes the cat then the cat is rough. If someone eats the lion then they eat the cat. If someone likes the lion and they eat the cat then they do not eat the lion. If someone is rough then they eat the lion. If the tiger does not like the cat then the tiger does not eat the cat.
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If someone visits the tiger then the tiger likes the cat.
((("someone" "visits" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If someone likes the cat then they do not visit the tiger.
((("someone" "likes" "cat" "+")) -> ("someone" "visits" "tiger" "-"))
If someone is green and they visit the lion then they visit the tiger.
((("someone" "is" "green" "+") ("someone" "visits" "lion" "+")) -> ("someone" "visits" "tiger" "+"))
If someone likes the cat then the cat is rough.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone eats the lion then they eat the cat.
((("someone" "eats" "lion" "+")) -> ("someone" "eats" "cat" "+"))
If someone likes the lion and they eat the cat then they do not eat the lion.
((("someone" "likes" "lion" "+") ("someone" "eats" "cat" "+")) -> ("someone" "eats" "lion" "-"))
If someone is rough then they eat the lion.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "lion" "+"))
If the tiger does not like the cat then the tiger does not eat the cat.
((("tiger" "likes" "cat" "~")) -> ("tiger" "eats" "cat" "-"))
The cat likes the tiger.
True
1
proof
[(triple1)]
("cat" "likes" "tiger" "+")
triple1
The tiger is not kind.
False
1
inv-proof
[(triple3)]
("tiger" "is" "kind" "-")
triple3
The cat is rough.
True
2
proof
[(((triple2) -> rule4))]
("cat" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "is" "rough" "-")
((triple2) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat eats the lion.
True
3
proof
[(((((triple2) -> rule4)) -> rule7))]
("cat" "eats" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat does not eat the lion.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("cat" "eats" "lion" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat eats the cat.
True
4
proof
[(((((((triple2) -> rule4)) -> rule7)) -> rule5))]
("cat" "eats" "cat" "+")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat does not eat the cat.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule7)) -> rule5))]
("cat" "eats" "cat" "-")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "eats" "lion" "+")
The tiger does not like the cat.
Unknown
inv-rconc
[@2: The tiger likes the cat.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("tiger" "likes" "cat" "-")
The tiger eats the cat.
Unknown
rconc
[@2: The tiger eats the cat.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("tiger" "eats" "cat" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger likes the lion.
Unknown
random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "+")
@0: The cat likes the tiger.[(triple1)] The lion likes the cat.[(triple2)] The tiger is kind.[(triple3)] @1: The cat is rough.[(((triple2) -> rule4))] The lion does not visit the tiger.[(((triple2) -> rule2))] @2: The cat eats the lion.[(((((triple2) -> rule4)) -> rule7))] @3: The cat eats the cat.[(((((((triple2) -> rule4)) -> rule7)) -> rule5))]
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple1
The lion likes the cat.
("lion" "likes" "cat" "+")
triple2
The tiger is kind.
("tiger" "is" "kind" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
((triple2) -> (rule2 % int1))
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3