The bald eagle chases the dog. The dog visits the squirrel. The mouse visits the squirrel. The squirrel chases the mouse. If something is nice then it is green. If something visits the dog then the dog chases the bald eagle. If the mouse visits the squirrel then the mouse is nice. If something sees the squirrel then the squirrel chases the mouse. If something visits the squirrel and the squirrel visits the dog then the dog sees the mouse. If something is green and it visits the squirrel then the squirrel sees the bald eagle. If the bald eagle chases the mouse then the bald eagle visits the mouse. If the bald eagle is young then the bald eagle does not chase the mouse.
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something visits the dog then the dog chases the bald eagle.
((("something" "visits" "dog" "+")) -> ("dog" "chases" "bald eagle" "+"))
If the mouse visits the squirrel then the mouse is nice.
((("mouse" "visits" "squirrel" "+")) -> ("mouse" "is" "nice" "+"))
If something sees the squirrel then the squirrel chases the mouse.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If something visits the squirrel and the squirrel visits the dog then the dog sees the mouse.
((("something" "visits" "squirrel" "+") ("squirrel" "visits" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
If something is green and it visits the squirrel then the squirrel sees the bald eagle.
((("something" "is" "green" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "sees" "bald eagle" "+"))
If the bald eagle chases the mouse then the bald eagle visits the mouse.
((("bald eagle" "chases" "mouse" "+")) -> ("bald eagle" "visits" "mouse" "+"))
If the bald eagle is young then the bald eagle does not chase the mouse.
((("bald eagle" "is" "young" "+")) -> ("bald eagle" "chases" "mouse" "-"))
The mouse visits the squirrel.
True
1
proof
[(triple3)]
("mouse" "visits" "squirrel" "+")
triple3
The dog does not visit the squirrel.
False
1
inv-proof
[(triple2)]
("dog" "visits" "squirrel" "-")
triple2
The mouse is nice.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "is" "nice" "+")
((triple3) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple3) -> rule3))]
("mouse" "is" "nice" "-")
((triple3) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("mouse" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("mouse" "is" "green" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel sees the bald eagle.
True
5
proof
[(((((((triple3) -> rule3)) -> rule1) triple3) -> rule6))]
("squirrel" "sees" "bald eagle" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The squirrel does not see the bald eagle.
False
5
inv-proof
[(((((((triple3) -> rule3)) -> rule1) triple3) -> rule6))]
("squirrel" "sees" "bald eagle" "-")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The bald eagle does not visit the mouse.
Unknown
inv-rconc
[@1: The bald eagle visits the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "visits" "mouse" "-")
The bald eagle is green.
Unknown
rconc
[@1: The bald eagle is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "green" "+")
The dog does not chase the bald eagle.
Unknown
inv-rconc
[@1: The dog chases the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "bald eagle" "-")
The dog is green.
Unknown
rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "green" "+")
The dog does not see the squirrel.
Unknown
inv-random
[@0: The dog sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "squirrel" "-")
The bald eagle is red.
Unknown
random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "+")
The dog does not see the bald eagle.
Unknown
inv-random
[@0: The dog sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bald eagle" "-")
The dog chases the squirrel.
Unknown
random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "+")
@0: The bald eagle chases the dog.[(triple1)] The dog visits the squirrel.[(triple2)] The mouse visits the squirrel.[(triple3)] The squirrel chases the mouse.[(triple4)] @1: The mouse is nice.[(((triple3) -> rule3))] @2: The mouse is green.[(((((triple3) -> rule3)) -> rule1))] @3: The squirrel sees the bald eagle.[(((((((triple3) -> rule3)) -> rule1) triple3) -> rule6))]
The bald eagle chases the dog.
("bald eagle" "chases" "dog" "+")
triple1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
((triple3) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
((((((triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3