The dog does not see the lion. The lion sees the tiger. The tiger sees the lion. If the tiger is kind and the tiger sees the lion then the lion is cold. If someone chases the lion then they eat the dog. If someone sees the lion then they are kind. If someone chases the dog then the dog does not eat the lion. If someone is kind then they chase the lion. If someone is kind and they see the tiger then the tiger chases the lion.
The dog does not see the lion.
("dog" "sees" "lion" "-")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If the tiger is kind and the tiger sees the lion then the lion is cold.
((("tiger" "is" "kind" "+") ("tiger" "sees" "lion" "+")) -> ("lion" "is" "cold" "+"))
If someone chases the lion then they eat the dog.
((("someone" "chases" "lion" "+")) -> ("someone" "eats" "dog" "+"))
If someone sees the lion then they are kind.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the dog then the dog does not eat the lion.
((("someone" "chases" "dog" "+")) -> ("dog" "eats" "lion" "-"))
If someone is kind then they chase the lion.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "lion" "+"))
If someone is kind and they see the tiger then the tiger chases the lion.
((("someone" "is" "kind" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
The dog does not see the lion.
True
1
proof
[(triple1)]
("dog" "sees" "lion" "-")
triple1
The dog sees the lion.
False
1
inv-proof
[(triple1)]
("dog" "sees" "lion" "+")
triple1
The tiger is kind.
True
2
proof
[(((triple3) -> rule3))]
("tiger" "is" "kind" "+")
((triple3) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple3) -> rule3))]
("tiger" "is" "kind" "-")
((triple3) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion is cold.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule1))]
("lion" "is" "cold" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The lion is not cold.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule1))]
("lion" "is" "cold" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the dog.
True
4
proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule2))]
("tiger" "eats" "dog" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger does not eat the dog.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule2))]
("tiger" "eats" "dog" "-")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The dog does not eat the dog.
Unknown
inv-rconc
[@3: The dog eats the dog.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule3 <- FAIL)]]
("dog" "eats" "dog" "-")
The lion eats the dog.
Unknown
rconc
[@3: The lion eats the dog.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule3 <- FAIL)]]
("lion" "eats" "dog" "+")
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "kind" "-")
The dog is kind.
Unknown
rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "kind" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The dog does not see the lion.[(triple1)] The lion sees the tiger.[(triple2)] The tiger sees the lion.[(triple3)] @1: The tiger is kind.[(((triple3) -> rule3))] @2: The lion is cold.[(((((triple3) -> rule3) triple3) -> rule1))] The tiger chases the lion.[(((((triple3) -> rule3)) -> rule5))] @3: The tiger eats the dog.[(((((((triple3) -> rule3)) -> rule5)) -> rule2))]
The dog does not see the lion.
("dog" "sees" "lion" "-")
triple1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple3
The tiger is kind.
("tiger" "is" "kind" "+")
((triple3) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3