The cat does not see the tiger. The tiger sees the cat. Green things are kind. If something sees the cat then it does not like the cat. If the tiger does not like the cat then the tiger needs the cat. If something needs the cat then it likes the tiger. If something likes the tiger and it is not green then the tiger is kind. If something likes the tiger and the tiger likes the cat then the cat is not kind.
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something sees the cat then it does not like the cat.
((("something" "sees" "cat" "+")) -> ("something" "likes" "cat" "-"))
If the tiger does not like the cat then the tiger needs the cat.
((("tiger" "likes" "cat" "~")) -> ("tiger" "needs" "cat" "+"))
If something needs the cat then it likes the tiger.
((("something" "needs" "cat" "+")) -> ("something" "likes" "tiger" "+"))
If something likes the tiger and it is not green then the tiger is kind.
((("something" "likes" "tiger" "+") ("something" "is" "green" "~")) -> ("tiger" "is" "kind" "+"))
If something likes the tiger and the tiger likes the cat then the cat is not kind.
((("something" "likes" "tiger" "+") ("tiger" "likes" "cat" "+")) -> ("cat" "is" "kind" "-"))
The tiger sees the cat.
True
1
proof
[(triple2)]
("tiger" "sees" "cat" "+")
triple2
The cat sees the tiger.
False
1
inv-proof
[(triple1)]
("cat" "sees" "tiger" "+")
triple1
The tiger does not like the cat.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "likes" "cat" "-")
((triple2) -> (rule2 % int1))
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int1
The tiger likes the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int1
The tiger needs the cat.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("tiger" "needs" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int2
The tiger does not need the cat.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("tiger" "needs" "cat" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int2
The tiger likes the tiger.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule4))]
("tiger" "likes" "tiger" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int3
The tiger does not like the tiger.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule4))]
("tiger" "likes" "tiger" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int3
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "kind" "-")
The cat likes the tiger.
Unknown
rconc
[@1: The cat likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "tiger" "+")
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "kind" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cat needs the tiger.
Unknown
random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "+")
@0: The cat does not see the tiger.[(triple1)] The tiger sees the cat.[(triple2)] @1: The tiger does not like the cat.[(((triple2) -> rule2))] @2: The tiger needs the cat.[(((((triple2) -> rule2)) -> rule3))] @3: The tiger likes the tiger.[(((((((triple2) -> rule2)) -> rule3)) -> rule4))]
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
triple1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
((triple2) -> (rule2 % int1))
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
int3