The cow sees the dog. The dog sees the lion. The lion does not chase the dog. If something sees the lion then it sees the cow. If something eats the lion and it eats the dog then it eats the cow. If something is red and it does not chase the cow then the cow sees the dog. Red things are not kind. Green things are kind. If something sees the cow then the cow is red.
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion does not chase the dog.
("lion" "chases" "dog" "-")
If something sees the lion then it sees the cow.
((("something" "sees" "lion" "+")) -> ("something" "sees" "cow" "+"))
If something eats the lion and it eats the dog then it eats the cow.
((("something" "eats" "lion" "+") ("something" "eats" "dog" "+")) -> ("something" "eats" "cow" "+"))
If something is red and it does not chase the cow then the cow sees the dog.
((("something" "is" "red" "+") ("something" "chases" "cow" "~")) -> ("cow" "sees" "dog" "+"))
Red things are not kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "-"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something sees the cow then the cow is red.
((("something" "sees" "cow" "+")) -> ("cow" "is" "red" "+"))
The lion does not chase the dog.
True
1
proof
[(triple3)]
("lion" "chases" "dog" "-")
triple3
The dog does not see the lion.
False
1
inv-proof
[(triple2)]
("dog" "sees" "lion" "-")
triple2
The dog sees the cow.
True
2
proof
[(((triple2) -> rule1))]
("dog" "sees" "cow" "+")
((triple2) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog does not see the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "sees" "cow" "-")
((triple2) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cow is red.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("cow" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow is not red.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("cow" "is" "red" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow is not kind.
True
4
proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
("cow" "is" "kind" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The cow is kind.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
("cow" "is" "kind" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The dog does not eat the cow.
Unknown
inv-rconc
[@1: The dog eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "cow" "-")
The dog is kind.
Unknown
rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "kind" "+")
The lion does not eat the cow.
Unknown
inv-rconc
[@1: The lion eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "cow" "-")
The lion is kind.
Unknown
rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "kind" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The cow eats the lion.
Unknown
random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "+")
@0: The cow sees the dog.[(triple1)] The dog sees the lion.[(triple2)] The lion does not chase the dog.[(triple3)] @1: The dog sees the cow.[(((triple2) -> rule1))] @2: The cow is red.[(((((triple2) -> rule1)) -> rule6))] @3: The cow is not kind.[(((((((triple2) -> rule1)) -> rule6)) -> rule4))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The dog sees the lion.
("dog" "sees" "lion" "+")
triple2
The lion does not chase the dog.
("lion" "chases" "dog" "-")
triple3
The dog sees the cow.
("dog" "sees" "cow" "+")
((triple2) -> (rule1 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The cow is not kind.
("cow" "is" "kind" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3