The bald eagle chases the mouse. The bald eagle eats the cat. The bald eagle is not nice. The bald eagle is round. The bald eagle is young. The cat is red. The mouse eats the cat. The rabbit eats the bald eagle. The rabbit eats the mouse. The rabbit is kind. The rabbit is round. The rabbit visits the cat. If something visits the rabbit and the rabbit visits the cat then the cat is round. If something visits the bald eagle and the bald eagle chases the mouse then it visits the rabbit. If something eats the cat then the cat is not kind. If something chases the bald eagle and it visits the bald eagle then the bald eagle does not eat the cat. If the mouse is not young then the mouse does not eat the bald eagle. If something is round then it visits the bald eagle. If the bald eagle is young then the bald eagle chases the rabbit. If something is red and not round then it eats the bald eagle. If something is young then it does not eat the bald eagle.
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle is young.
("bald eagle" "is" "young" "+")
The cat is red.
("cat" "is" "red" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The rabbit eats the bald eagle.
("rabbit" "eats" "bald eagle" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something visits the rabbit and the rabbit visits the cat then the cat is round.
((("something" "visits" "rabbit" "+") ("rabbit" "visits" "cat" "+")) -> ("cat" "is" "round" "+"))
If something visits the bald eagle and the bald eagle chases the mouse then it visits the rabbit.
((("something" "visits" "bald eagle" "+") ("bald eagle" "chases" "mouse" "+")) -> ("something" "visits" "rabbit" "+"))
If something eats the cat then the cat is not kind.
((("something" "eats" "cat" "+")) -> ("cat" "is" "kind" "-"))
If something chases the bald eagle and it visits the bald eagle then the bald eagle does not eat the cat.
((("something" "chases" "bald eagle" "+") ("something" "visits" "bald eagle" "+")) -> ("bald eagle" "eats" "cat" "-"))
If the mouse is not young then the mouse does not eat the bald eagle.
((("mouse" "is" "young" "~")) -> ("mouse" "eats" "bald eagle" "-"))
If something is round then it visits the bald eagle.
((("something" "is" "round" "+")) -> ("something" "visits" "bald eagle" "+"))
If the bald eagle is young then the bald eagle chases the rabbit.
((("bald eagle" "is" "young" "+")) -> ("bald eagle" "chases" "rabbit" "+"))
If something is red and not round then it eats the bald eagle.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "eats" "bald eagle" "+"))
If something is young then it does not eat the bald eagle.
((("something" "is" "young" "+")) -> ("something" "eats" "bald eagle" "-"))
The rabbit is round.
True
1
proof
[(triple11)]
("rabbit" "is" "round" "+")
triple11
The rabbit is not round.
False
1
inv-proof
[(triple11)]
("rabbit" "is" "round" "-")
triple11
The cat is not kind.
True
2
proof
[(((triple2) -> rule3) OR ((triple7) -> rule3))]
("cat" "is" "kind" "-")
((triple2) -> (rule3 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
((triple7) -> (rule3 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The bald eagle does not visit the bald eagle.
False
2
inv-proof
[(((triple4) -> rule6))]
("bald eagle" "visits" "bald eagle" "-")
((triple4) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The rabbit visits the rabbit.
True
4
proof
[(((((triple11) -> rule6) triple1) -> rule2))]
("rabbit" "visits" "rabbit" "+")
((((triple11) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int2
The rabbit does not visit the rabbit.
False
4
inv-proof
[(((((triple11) -> rule6) triple1) -> rule2))]
("rabbit" "visits" "rabbit" "-")
((((triple11) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int2
The cat is round.
True
6
proof
[(((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1) OR ((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1))]
("cat" "is" "round" "+")
((((((triple11) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple12) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int3
((((((triple4) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple12) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int2
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int3
The cat is not round.
False
6
inv-proof
[(((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1) OR ((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1))]
("cat" "is" "round" "-")
((((((triple11) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple12) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int3
((((((triple4) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple12) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int2
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int3
The cat visits the bald eagle.
True
7
proof
[(((((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) OR ((((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6))]
("cat" "visits" "bald eagle" "+")
((((((((triple11) -> (rule6 % int4)) triple1) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int4
((((((((triple4) -> (rule6 % int4)) triple1) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int3
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int4
The cat does not visit the bald eagle.
False
7
inv-proof
[(((((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) OR ((((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6))]
("cat" "visits" "bald eagle" "-")
((((((((triple11) -> (rule6 % int4)) triple1) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int4
((((((((triple4) -> (rule6 % int4)) triple1) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int3
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int4
The cat visits the rabbit.
True
9
proof
[(((((((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) triple1) -> rule2) OR ((((((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) triple1) -> rule2))]
("cat" "visits" "rabbit" "+")
((((((((((triple11) -> (rule6 % int5)) triple1) -> (rule2 % int4)) triple12) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int5
((((((((((triple4) -> (rule6 % int5)) triple1) -> (rule2 % int4)) triple12) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int4
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int5
The cat does not visit the rabbit.
False
9
inv-proof
[(((((((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) triple1) -> rule2) OR ((((((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) triple1) -> rule2))]
("cat" "visits" "rabbit" "-")
((((((((((triple11) -> (rule6 % int5)) triple1) -> (rule2 % int4)) triple12) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int5
((((((((((triple4) -> (rule6 % int5)) triple1) -> (rule2 % int4)) triple12) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int4
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int5
The mouse does not visit the rabbit.
Unknown
inv-rconc
[@2: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("mouse" "visits" "rabbit" "-")
The mouse visits the bald eagle.
Unknown
rconc
[@1: The mouse visits the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "visits" "bald eagle" "+")
The mouse does not eat the bald eagle.
Unknown
inv-rconc
[@1: The mouse eats the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "bald eagle" "-")
The cat eats the bald eagle.
Unknown
rconc
[@1: The cat eats the bald eagle.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "eats" "bald eagle" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The cat does not visit the mouse.
Unknown
inv-random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The bald eagle is kind.
Unknown
random
[@0: The bald eagle is kind.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "kind" "+")
The bald eagle does not visit the cat.
Unknown
inv-random
[@0: The bald eagle visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "cat" "-")
The rabbit eats the cat.
Unknown
random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "+")
@0: The bald eagle chases the mouse.[(triple1)] The bald eagle eats the cat.[(triple2)] The bald eagle is not nice.[(triple3)] The bald eagle is round.[(triple4)] The bald eagle is young.[(triple5)] The cat is red.[(triple6)] The mouse eats the cat.[(triple7)] The rabbit eats the bald eagle.[(triple8)] The rabbit eats the mouse.[(triple9)] The rabbit is kind.[(triple10)] The rabbit is round.[(triple11)] The rabbit visits the cat.[(triple12)] @1: The bald eagle chases the rabbit.[(((triple5) -> rule7))] The bald eagle does not eat the bald eagle.[(((triple5) -> rule9))] The bald eagle visits the bald eagle.[(((triple4) -> rule6))] The cat is not kind.[(((triple2) -> rule3) OR ((triple7) -> rule3))] The rabbit visits the bald eagle.[(((triple11) -> rule6))] @2: The bald eagle visits the rabbit.[(((((triple4) -> rule6) triple1) -> rule2))] The rabbit visits the rabbit.[(((((triple11) -> rule6) triple1) -> rule2))] @3: The cat is round.[(((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1) OR ((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1))] @4: The cat visits the bald eagle.[(((((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) OR ((((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6))] @5: The cat visits the rabbit.[(((((((((((triple11) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) triple1) -> rule2) OR ((((((((((triple4) -> rule6) triple1) -> rule2) triple12) -> rule1)) -> rule6) triple1) -> rule2))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple1
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
triple2
The bald eagle is not nice.
("bald eagle" "is" "nice" "-")
triple3
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple4
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple7
The rabbit eats the bald eagle.
("rabbit" "eats" "bald eagle" "+")
triple8
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple12
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
((triple5) -> (rule7 % int1))
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
int1
The bald eagle does not eat the bald eagle.
("bald eagle" "eats" "bald eagle" "-")
((triple5) -> (rule9 % int1))
The bald eagle does not eat the bald eagle.
("bald eagle" "eats" "bald eagle" "-")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
((triple4) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The cat is not kind.
("cat" "is" "kind" "-")
((triple2) -> (rule3 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
((triple7) -> (rule3 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
((triple11) -> (rule6 % int1))
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int1
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
((((triple4) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple11) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((((((triple11) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple12) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int3
((((((triple4) -> (rule6 % int3)) triple1) -> (rule2 % int2)) triple12) -> (rule1 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int2
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int3
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
((((((((triple11) -> (rule6 % int4)) triple1) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int4
((((((((triple4) -> (rule6 % int4)) triple1) -> (rule2 % int3)) triple12) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int3
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int4
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((((((((((triple11) -> (rule6 % int5)) triple1) -> (rule2 % int4)) triple12) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int4
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int5
((((((((((triple4) -> (rule6 % int5)) triple1) -> (rule2 % int4)) triple12) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bald eagle visits the rabbit.
("bald eagle" "visits" "rabbit" "+")
int4
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int5