The bald eagle is round. The cat needs the bald eagle. The dog is red. The mouse likes the cat. If something needs the bald eagle then the bald eagle is red. If something is red and round then it likes the mouse. If something visits the mouse then it is cold. If something needs the bald eagle and the bald eagle is blue then the bald eagle likes the mouse. If the cat needs the bald eagle and the bald eagle likes the mouse then the cat is red. If something likes the cat then the cat likes the mouse. If something is cold then it likes the bald eagle. If the bald eagle is red and the bald eagle is kind then the bald eagle needs the dog.
The bald eagle is round.
("bald eagle" "is" "round" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The dog is red.
("dog" "is" "red" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If something needs the bald eagle then the bald eagle is red.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "red" "+"))
If something is red and round then it likes the mouse.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the mouse then it is cold.
((("something" "visits" "mouse" "+")) -> ("something" "is" "cold" "+"))
If something needs the bald eagle and the bald eagle is blue then the bald eagle likes the mouse.
((("something" "needs" "bald eagle" "+") ("bald eagle" "is" "blue" "+")) -> ("bald eagle" "likes" "mouse" "+"))
If the cat needs the bald eagle and the bald eagle likes the mouse then the cat is red.
((("cat" "needs" "bald eagle" "+") ("bald eagle" "likes" "mouse" "+")) -> ("cat" "is" "red" "+"))
If something likes the cat then the cat likes the mouse.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If something is cold then it likes the bald eagle.
((("something" "is" "cold" "+")) -> ("something" "likes" "bald eagle" "+"))
If the bald eagle is red and the bald eagle is kind then the bald eagle needs the dog.
((("bald eagle" "is" "red" "+") ("bald eagle" "is" "kind" "+")) -> ("bald eagle" "needs" "dog" "+"))
The dog is red.
True
1
proof
[(triple3)]
("dog" "is" "red" "+")
triple3
The mouse does not like the cat.
False
1
inv-proof
[(triple4)]
("mouse" "likes" "cat" "-")
triple4
The bald eagle is red.
True
2
proof
[(((triple2) -> rule1))]
("bald eagle" "is" "red" "+")
((triple2) -> (rule1 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The cat does not like the mouse.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "likes" "mouse" "-")
((triple4) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The bald eagle likes the mouse.
True
4
proof
[(((((triple2) -> rule1) triple1) -> rule2))]
("bald eagle" "likes" "mouse" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle does not like the mouse.
False
4
inv-proof
[(((((triple2) -> rule1) triple1) -> rule2))]
("bald eagle" "likes" "mouse" "-")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The cat is red.
True
6
proof
[(((triple2 ((((triple2) -> rule1) triple1) -> rule2)) -> rule5))]
("cat" "is" "red" "+")
((triple2 ((((triple2) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The cat is not red.
False
6
inv-proof
[(((triple2 ((((triple2) -> rule1) triple1) -> rule2)) -> rule5))]
("cat" "is" "red" "-")
((triple2 ((((triple2) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The cat does not like the bald eagle.
Unknown
inv-rconc
[@2: The cat likes the bald eagle.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("cat" "likes" "bald eagle" "-")
The bald eagle is cold.
Unknown
rconc
[@1: The bald eagle is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "is" "cold" "+")
The bald eagle does not like the bald eagle.
Unknown
inv-rconc
[@2: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("bald eagle" "likes" "bald eagle" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The cat does not visit the bald eagle.
Unknown
inv-random
[@0: The cat visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bald eagle" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The bald eagle likes the cat.
Unknown
random
[@0: The bald eagle likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "cat" "+")
@0: The bald eagle is round.[(triple1)] The cat needs the bald eagle.[(triple2)] The dog is red.[(triple3)] The mouse likes the cat.[(triple4)] @1: The bald eagle is red.[(((triple2) -> rule1))] The cat likes the mouse.[(((triple4) -> rule6))] @2: The bald eagle likes the mouse.[(((((triple2) -> rule1) triple1) -> rule2))] @3: The cat is red.[(((triple2 ((((triple2) -> rule1) triple1) -> rule2)) -> rule5))]
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple4
The bald eagle is red.
("bald eagle" "is" "red" "+")
((triple2) -> (rule1 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((triple4) -> (rule6 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((triple2 ((((triple2) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3