The bald eagle does not visit the cat. The cat does not chase the bald eagle. The lion chases the cat. Kind things are cold. If the lion does not chase the cat then the lion likes the cat. If something chases the cat then the cat likes the bald eagle. If something visits the cat then the cat does not visit the lion. If something likes the cat and the cat is cold then it chases the lion. If something likes the cat then it chases the lion. All cold things are big. If something likes the bald eagle then it visits the cat.
The bald eagle does not visit the cat.
("bald eagle" "visits" "cat" "-")
The cat does not chase the bald eagle.
("cat" "chases" "bald eagle" "-")
The lion chases the cat.
("lion" "chases" "cat" "+")
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If the lion does not chase the cat then the lion likes the cat.
((("lion" "chases" "cat" "~")) -> ("lion" "likes" "cat" "+"))
If something chases the cat then the cat likes the bald eagle.
((("something" "chases" "cat" "+")) -> ("cat" "likes" "bald eagle" "+"))
If something visits the cat then the cat does not visit the lion.
((("something" "visits" "cat" "+")) -> ("cat" "visits" "lion" "-"))
If something likes the cat and the cat is cold then it chases the lion.
((("something" "likes" "cat" "+") ("cat" "is" "cold" "+")) -> ("something" "chases" "lion" "+"))
If something likes the cat then it chases the lion.
((("something" "likes" "cat" "+")) -> ("something" "chases" "lion" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something likes the bald eagle then it visits the cat.
((("something" "likes" "bald eagle" "+")) -> ("something" "visits" "cat" "+"))
The cat does not chase the bald eagle.
True
1
proof
[(triple2)]
("cat" "chases" "bald eagle" "-")
triple2
The bald eagle visits the cat.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "cat" "+")
triple1
The cat likes the bald eagle.
True
2
proof
[(((triple3) -> rule3))]
("cat" "likes" "bald eagle" "+")
((triple3) -> (rule3 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The cat does not like the bald eagle.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "likes" "bald eagle" "-")
((triple3) -> (rule3 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The cat visits the cat.
True
3
proof
[(((((triple3) -> rule3)) -> rule8))]
("cat" "visits" "cat" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule8))]
("cat" "visits" "cat" "-")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The cat does not visit the lion.
True
4
proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule4))]
("cat" "visits" "lion" "-")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int3
The cat visits the lion.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule4))]
("cat" "visits" "lion" "+")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int3
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "cold" "-")
The lion likes the cat.
Unknown
rconc
[@1: The lion likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "cat" "+")
The lion does not visit the cat.
Unknown
inv-rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "visits" "cat" "-")
The cat is big.
Unknown
rconc
[@2: The cat is big.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("cat" "is" "big" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The lion does not visit the bald eagle.
Unknown
inv-random
[@0: The lion visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bald eagle" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The bald eagle does not visit the cat.[(triple1)] The cat does not chase the bald eagle.[(triple2)] The lion chases the cat.[(triple3)] @1: The cat likes the bald eagle.[(((triple3) -> rule3))] @2: The cat visits the cat.[(((((triple3) -> rule3)) -> rule8))] @3: The cat does not visit the lion.[(((((((triple3) -> rule3)) -> rule8)) -> rule4))]
The bald eagle does not visit the cat.
("bald eagle" "visits" "cat" "-")
triple1
The cat does not chase the bald eagle.
("cat" "chases" "bald eagle" "-")
triple2
The lion chases the cat.
("lion" "chases" "cat" "+")
triple3
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
((triple3) -> (rule3 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The cat does not visit the lion.
("cat" "visits" "lion" "-")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int3