The cow is cold. The cow is not kind. The cow does not see the lion. The dog chases the lion. The dog is rough. The lion eats the dog. The lion is kind. The tiger does not eat the cow. The tiger eats the dog. The tiger eats the lion. If the cow eats the lion and the tiger does not chase the cow then the lion sees the tiger. If the dog is red then the dog is cold. If something chases the lion then it is cold. If something eats the cow then the cow is not cold. If something chases the tiger and the tiger is rough then the tiger eats the lion. If something is cold then it does not eat the dog.
The cow is cold.
("cow" "is" "cold" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow does not see the lion.
("cow" "sees" "lion" "-")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is rough.
("dog" "is" "rough" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is kind.
("lion" "is" "kind" "+")
The tiger does not eat the cow.
("tiger" "eats" "cow" "-")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If the cow eats the lion and the tiger does not chase the cow then the lion sees the tiger.
((("cow" "eats" "lion" "+") ("tiger" "chases" "cow" "~")) -> ("lion" "sees" "tiger" "+"))
If the dog is red then the dog is cold.
((("dog" "is" "red" "+")) -> ("dog" "is" "cold" "+"))
If something chases the lion then it is cold.
((("something" "chases" "lion" "+")) -> ("something" "is" "cold" "+"))
If something eats the cow then the cow is not cold.
((("something" "eats" "cow" "+")) -> ("cow" "is" "cold" "-"))
If something chases the tiger and the tiger is rough then the tiger eats the lion.
((("something" "chases" "tiger" "+") ("tiger" "is" "rough" "+")) -> ("tiger" "eats" "lion" "+"))
If something is cold then it does not eat the dog.
((("something" "is" "cold" "+")) -> ("something" "eats" "dog" "-"))
The lion eats the dog.
True
1
proof
[(triple6)]
("lion" "eats" "dog" "+")
triple6
The cow is kind.
False
1
inv-proof
[(triple2)]
("cow" "is" "kind" "+")
triple2
The cow does not eat the dog.
True
2
proof
[(((triple1) -> rule6))]
("cow" "eats" "dog" "-")
((triple1) -> (rule6 % int1))
The cow does not eat the dog.
("cow" "eats" "dog" "-")
int1
The dog is not cold.
False
2
inv-proof
[(((triple4) -> rule3))]
("dog" "is" "cold" "-")
((triple4) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not eat the dog.
True
3
proof
[(((((triple4) -> rule3)) -> rule6))]
("dog" "eats" "dog" "-")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog eats the dog.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule6))]
("dog" "eats" "dog" "+")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "cold" "-")
The lion sees the tiger.
Unknown
rconc
[@1: The lion sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "tiger" "+")
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "cold" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The cow does not see the lion.[(triple3)] The cow is cold.[(triple1)] The cow is not kind.[(triple2)] The dog chases the lion.[(triple4)] The dog is rough.[(triple5)] The lion eats the dog.[(triple6)] The lion is kind.[(triple7)] The tiger does not eat the cow.[(triple8)] The tiger eats the dog.[(triple9)] The tiger eats the lion.[(triple10)] @1: The cow does not eat the dog.[(((triple1) -> rule6))] The dog is cold.[(((triple4) -> rule3))] @2: The dog does not eat the dog.[(((((triple4) -> rule3)) -> rule6))]
The cow does not see the lion.
("cow" "sees" "lion" "-")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is not kind.
("cow" "is" "kind" "-")
triple2
The dog chases the lion.
("dog" "chases" "lion" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The lion eats the dog.
("lion" "eats" "dog" "+")
triple6
The lion is kind.
("lion" "is" "kind" "+")
triple7
The tiger does not eat the cow.
("tiger" "eats" "cow" "-")
triple8
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple9
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple10
The cow does not eat the dog.
("cow" "eats" "dog" "-")
((triple1) -> (rule6 % int1))
The cow does not eat the dog.
("cow" "eats" "dog" "-")
int1
The dog is cold.
("dog" "is" "cold" "+")
((triple4) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog does not eat the dog.
("dog" "eats" "dog" "-")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2