The bald eagle needs the lion. The dog is green. The lion is rough. If something needs the dog then it is nice. If something eats the lion then it eats the dog. If something is rough and nice then it eats the dog. If something needs the lion then the lion is nice. If something is cold and rough then it chases the bald eagle. If the lion eats the bald eagle then the lion does not chase the dog. If the lion eats the dog and the lion needs the dog then the lion does not chase the bald eagle. If something eats the dog then it does not need the bald eagle.
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The dog is green.
("dog" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
If something needs the dog then it is nice.
((("something" "needs" "dog" "+")) -> ("something" "is" "nice" "+"))
If something eats the lion then it eats the dog.
((("something" "eats" "lion" "+")) -> ("something" "eats" "dog" "+"))
If something is rough and nice then it eats the dog.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "eats" "dog" "+"))
If something needs the lion then the lion is nice.
((("something" "needs" "lion" "+")) -> ("lion" "is" "nice" "+"))
If something is cold and rough then it chases the bald eagle.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "chases" "bald eagle" "+"))
If the lion eats the bald eagle then the lion does not chase the dog.
((("lion" "eats" "bald eagle" "+")) -> ("lion" "chases" "dog" "-"))
If the lion eats the dog and the lion needs the dog then the lion does not chase the bald eagle.
((("lion" "eats" "dog" "+") ("lion" "needs" "dog" "+")) -> ("lion" "chases" "bald eagle" "-"))
If something eats the dog then it does not need the bald eagle.
((("something" "eats" "dog" "+")) -> ("something" "needs" "bald eagle" "-"))
The dog is green.
True
1
proof
[(triple2)]
("dog" "is" "green" "+")
triple2
The dog is not green.
False
1
inv-proof
[(triple2)]
("dog" "is" "green" "-")
triple2
The lion is nice.
True
2
proof
[(((triple1) -> rule4))]
("lion" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "is" "nice" "-")
((triple1) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion eats the dog.
True
4
proof
[(((triple3 ((triple1) -> rule4)) -> rule3))]
("lion" "eats" "dog" "+")
((triple3 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not eat the dog.
False
4
inv-proof
[(((triple3 ((triple1) -> rule4)) -> rule3))]
("lion" "eats" "dog" "-")
((triple3 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not need the bald eagle.
True
5
proof
[(((((triple3 ((triple1) -> rule4)) -> rule3)) -> rule8))]
("lion" "needs" "bald eagle" "-")
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion does not need the bald eagle.
("lion" "needs" "bald eagle" "-")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion needs the bald eagle.
False
5
inv-proof
[(((((triple3 ((triple1) -> rule4)) -> rule3)) -> rule8))]
("lion" "needs" "bald eagle" "+")
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion does not need the bald eagle.
("lion" "needs" "bald eagle" "-")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The bald eagle does not eat the dog.
Unknown
inv-rconc
[@1: The bald eagle eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "eats" "dog" "-")
The dog chases the bald eagle.
Unknown
rconc
[@1: The dog chases the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "chases" "bald eagle" "+")
The lion does not chase the bald eagle.
Unknown
inv-rconc
[@1: The lion chases the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "bald eagle" "-")
The bald eagle chases the bald eagle.
Unknown
rconc
[@1: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "chases" "bald eagle" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
@0: The bald eagle needs the lion.[(triple1)] The dog is green.[(triple2)] The lion is rough.[(triple3)] @1: The lion is nice.[(((triple1) -> rule4))] @2: The lion eats the dog.[(((triple3 ((triple1) -> rule4)) -> rule3))] @3: The lion does not need the bald eagle.[(((((triple3 ((triple1) -> rule4)) -> rule3)) -> rule8))]
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
((triple3 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not need the bald eagle.
("lion" "needs" "bald eagle" "-")
((((triple3 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion does not need the bald eagle.
("lion" "needs" "bald eagle" "-")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3