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