The bald eagle is red. The bald eagle sees the lion. The cat likes the bald eagle. The cat visits the bald eagle. The cat does not visit the mouse. The lion sees the mouse. The mouse is green. If something visits the lion then it does not visit the bald eagle. If something sees the mouse then the mouse is cold. If something sees the cat and the cat sees the lion then it is not blue. If something is cold then it is blue. If something sees the cat then it is not nice. If something likes the mouse then the mouse visits the bald eagle. If something likes the bald eagle then it sees the mouse. If something is blue and it does not visit the bald eagle then the bald eagle visits the mouse.
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
If something visits the lion then it does not visit the bald eagle.
((("something" "visits" "lion" "+")) -> ("something" "visits" "bald eagle" "-"))
If something sees the mouse then the mouse is cold.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something sees the cat and the cat sees the lion then it is not blue.
((("something" "sees" "cat" "+") ("cat" "sees" "lion" "+")) -> ("something" "is" "blue" "-"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something sees the cat then it is not nice.
((("something" "sees" "cat" "+")) -> ("something" "is" "nice" "-"))
If something likes the mouse then the mouse visits the bald eagle.
((("something" "likes" "mouse" "+")) -> ("mouse" "visits" "bald eagle" "+"))
If something likes the bald eagle then it sees the mouse.
((("something" "likes" "bald eagle" "+")) -> ("something" "sees" "mouse" "+"))
If something is blue and it does not visit the bald eagle then the bald eagle visits the mouse.
((("something" "is" "blue" "+") ("something" "visits" "bald eagle" "~")) -> ("bald eagle" "visits" "mouse" "+"))
The cat visits the bald eagle.
True
1
proof
[(triple4)]
("cat" "visits" "bald eagle" "+")
triple4
The bald eagle is not red.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "red" "-")
triple1
The cat sees the mouse.
True
2
proof
[(((triple3) -> rule7))]
("cat" "sees" "mouse" "+")
((triple3) -> (rule7 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple6) -> rule2) OR ((((triple3) -> rule7)) -> rule2))]
("mouse" "is" "cold" "-")
((triple6) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse is blue.
True
3
proof
[(((((triple6) -> rule2)) -> rule4) OR ((((((triple3) -> rule7)) -> rule2)) -> rule4))]
("mouse" "is" "blue" "+")
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The mouse is not blue.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule4) OR ((((((triple3) -> rule7)) -> rule2)) -> rule4))]
("mouse" "is" "blue" "-")
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "blue" "-")
The lion is blue.
Unknown
rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "blue" "+")
The bald eagle does not visit the mouse.
Unknown
inv-rconc
[@1: The bald eagle visits the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "visits" "mouse" "-")
The bald eagle is green.
Unknown
random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "+")
The bald eagle does not visit the lion.
Unknown
inv-random
[@0: The bald eagle visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "lion" "-")
The mouse visits the lion.
Unknown
random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "+")
@0: The bald eagle is red.[(triple1)] The bald eagle sees the lion.[(triple2)] The cat does not visit the mouse.[(triple5)] The cat likes the bald eagle.[(triple3)] The cat visits the bald eagle.[(triple4)] The lion sees the mouse.[(triple6)] The mouse is green.[(triple7)] @1: The cat sees the mouse.[(((triple3) -> rule7))] The mouse is cold.[(((triple6) -> rule2) OR ((((triple3) -> rule7)) -> rule2))] @2: The mouse is blue.[(((((triple6) -> rule2)) -> rule4) OR ((((((triple3) -> rule7)) -> rule2)) -> rule4))]
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple2
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
triple5
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple3
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple4
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple3) -> (rule7 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple6) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3