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