The bald eagle does not chase the lion. The bald eagle is round. The bald eagle sees the cat. The bald eagle visits the cat. The bald eagle visits the lion. The cat chases the bald eagle. The cat chases the lion. The cat is cold. The cat sees the bald eagle. The cat visits the bald eagle. The lion is kind. The lion visits the cat. If the cat chases the lion then the cat visits the bald eagle. If something is cold then it sees the lion. If something chases the cat then the cat is young. If something is kind and it does not chase the lion then the lion is not cold. If something is cold then it sees the cat. If something is cold and it sees the lion then it is round. If something chases the lion then it chases the bald eagle. If the cat sees the bald eagle and the cat does not visit the bald eagle then the bald eagle does not visit the lion.
The bald eagle does not chase the lion.
("bald eagle" "chases" "lion" "-")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
The cat chases the bald eagle.
("cat" "chases" "bald eagle" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If the cat chases the lion then the cat visits the bald eagle.
((("cat" "chases" "lion" "+")) -> ("cat" "visits" "bald eagle" "+"))
If something is cold then it sees the lion.
((("something" "is" "cold" "+")) -> ("something" "sees" "lion" "+"))
If something chases the cat then the cat is young.
((("something" "chases" "cat" "+")) -> ("cat" "is" "young" "+"))
If something is kind and it does not chase the lion then the lion is not cold.
((("something" "is" "kind" "+") ("something" "chases" "lion" "~")) -> ("lion" "is" "cold" "-"))
If something is cold then it sees the cat.
((("something" "is" "cold" "+")) -> ("something" "sees" "cat" "+"))
If something is cold and it sees the lion then it is round.
((("something" "is" "cold" "+") ("something" "sees" "lion" "+")) -> ("something" "is" "round" "+"))
If something chases the lion then it chases the bald eagle.
((("something" "chases" "lion" "+")) -> ("something" "chases" "bald eagle" "+"))
If the cat sees the bald eagle and the cat does not visit the bald eagle then the bald eagle does not visit the lion.
((("cat" "sees" "bald eagle" "+") ("cat" "visits" "bald eagle" "~")) -> ("bald eagle" "visits" "lion" "-"))
The bald eagle visits the lion.
True
1
proof
[(triple5)]
("bald eagle" "visits" "lion" "+")
triple5
The bald eagle does not visit the lion.
False
1
inv-proof
[(triple5)]
("bald eagle" "visits" "lion" "-")
triple5
The cat sees the cat.
True
2
proof
[(((triple8) -> rule5))]
("cat" "sees" "cat" "+")
((triple8) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat does not see the lion.
False
2
inv-proof
[(((triple8) -> rule2))]
("cat" "sees" "lion" "-")
((triple8) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat is round.
True
4
proof
[(((triple8 ((triple8) -> rule2)) -> rule6))]
("cat" "is" "round" "+")
((triple8 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The cat is not round.
False
4
inv-proof
[(((triple8 ((triple8) -> rule2)) -> rule6))]
("cat" "is" "round" "-")
((triple8 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "lion" "+")
The bald eagle does not see the lion.
Unknown
inv-rconc
[@1: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "sees" "lion" "-")
The bald eagle is kind.
Unknown
random
[@0: The bald eagle is kind.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "kind" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The bald eagle does not chase the lion.[(triple1)] The bald eagle is round.[(triple2)] The bald eagle sees the cat.[(triple3)] The bald eagle visits the cat.[(triple4)] The bald eagle visits the lion.[(triple5)] The cat chases the bald eagle.[(triple6 OR ((triple7) -> rule7))] The cat chases the lion.[(triple7)] The cat is cold.[(triple8)] The cat sees the bald eagle.[(triple9)] The cat visits the bald eagle.[(triple10 OR ((triple7) -> rule1))] The lion is kind.[(triple11)] The lion visits the cat.[(triple12)] @1: The cat sees the cat.[(((triple8) -> rule5))] The cat sees the lion.[(((triple8) -> rule2))] @2: The cat is round.[(((triple8 ((triple8) -> rule2)) -> rule6))]
The bald eagle does not chase the lion.
("bald eagle" "chases" "lion" "-")
triple1
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple3
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
triple4
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
triple5
The cat chases the bald eagle.
("cat" "chases" "bald eagle" "+")
triple6
((triple7) -> (rule7 % int1))
The cat chases the bald eagle.
("cat" "chases" "bald eagle" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
triple7
The cat is cold.
("cat" "is" "cold" "+")
triple8
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple9
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple10
((triple7) -> (rule1 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple11
The lion visits the cat.
("lion" "visits" "cat" "+")
triple12
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple8) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
((triple8) -> (rule2 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple8 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2