The bald eagle is big. The bald eagle is red. The cat needs the mouse. The dog needs the bald eagle. The dog needs the mouse. The dog visits the bald eagle. The mouse is red. All nice things are big. If something is red then it visits the mouse. If something eats the dog and it visits the mouse then the mouse visits the bald eagle. If something visits the bald eagle then the bald eagle needs the mouse. If something eats the mouse then it eats the bald eagle. If something is rough and it visits the dog then the dog is nice. If something is young and it eats the cat then the cat is nice. If something visits the mouse then it needs the dog. If something needs the dog then the dog is red.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The bald eagle is red.
("bald eagle" "is" "red" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
The mouse is red.
("mouse" "is" "red" "+")
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is red then it visits the mouse.
((("something" "is" "red" "+")) -> ("something" "visits" "mouse" "+"))
If something eats the dog and it visits the mouse then the mouse visits the bald eagle.
((("something" "eats" "dog" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "visits" "bald eagle" "+"))
If something visits the bald eagle then the bald eagle needs the mouse.
((("something" "visits" "bald eagle" "+")) -> ("bald eagle" "needs" "mouse" "+"))
If something eats the mouse then it eats the bald eagle.
((("something" "eats" "mouse" "+")) -> ("something" "eats" "bald eagle" "+"))
If something is rough and it visits the dog then the dog is nice.
((("something" "is" "rough" "+") ("something" "visits" "dog" "+")) -> ("dog" "is" "nice" "+"))
If something is young and it eats the cat then the cat is nice.
((("something" "is" "young" "+") ("something" "eats" "cat" "+")) -> ("cat" "is" "nice" "+"))
If something visits the mouse then it needs the dog.
((("something" "visits" "mouse" "+")) -> ("something" "needs" "dog" "+"))
If something needs the dog then the dog is red.
((("something" "needs" "dog" "+")) -> ("dog" "is" "red" "+"))
The cat needs the mouse.
True
1
proof
[(triple3)]
("cat" "needs" "mouse" "+")
triple3
The mouse is not red.
False
1
inv-proof
[(triple7)]
("mouse" "is" "red" "-")
triple7
The bald eagle visits the mouse.
True
2
proof
[(((triple2) -> rule2))]
("bald eagle" "visits" "mouse" "+")
((triple2) -> (rule2 % int1))
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int1
The bald eagle does not visit the mouse.
False
2
inv-proof
[(((triple2) -> rule2))]
("bald eagle" "visits" "mouse" "-")
((triple2) -> (rule2 % int1))
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int1
The bald eagle needs the dog.
True
3
proof
[(((((triple2) -> rule2)) -> rule8))]
("bald eagle" "needs" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int1
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int2
The bald eagle does not need the dog.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule8))]
("bald eagle" "needs" "dog" "-")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int1
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int2
The dog is red.
True
4
proof
[(((((((triple2) -> rule2)) -> rule8)) -> rule9) OR ((((((triple7) -> rule2)) -> rule8)) -> rule9))]
("dog" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int2
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int3
((((((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The dog is not red.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule8)) -> rule9) OR ((((((triple7) -> rule2)) -> rule8)) -> rule9))]
("dog" "is" "red" "-")
((((((triple2) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int2
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int3
((((((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The dog visits the mouse.
True
5
proof
[(((((((((triple2) -> rule2)) -> rule8)) -> rule9)) -> rule2) OR ((((((((triple7) -> rule2)) -> rule8)) -> rule9)) -> rule2))]
("dog" "visits" "mouse" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int3
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int4
((((((((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4
The dog does not visit the mouse.
False
5
inv-proof
[(((((((((triple2) -> rule2)) -> rule8)) -> rule9)) -> rule2) OR ((((((((triple7) -> rule2)) -> rule8)) -> rule9)) -> rule2))]
("dog" "visits" "mouse" "-")
((((((((triple2) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int3
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int4
((((((((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4
The dog needs the dog.
True
6
proof
[(((((((((((triple2) -> rule2)) -> rule8)) -> rule9)) -> rule2)) -> rule8) OR ((((((((((triple7) -> rule2)) -> rule8)) -> rule9)) -> rule2)) -> rule8))]
("dog" "needs" "dog" "+")
((((((((((triple2) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int4
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int5
((((((((((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int5
The dog does not need the dog.
False
6
inv-proof
[(((((((((((triple2) -> rule2)) -> rule8)) -> rule9)) -> rule2)) -> rule8) OR ((((((((((triple7) -> rule2)) -> rule8)) -> rule9)) -> rule2)) -> rule8))]
("dog" "needs" "dog" "-")
((((((((((triple2) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int4
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int5
((((((((((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int5
The cat does not eat the bald eagle.
Unknown
inv-rconc
[@1: The cat eats the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "bald eagle" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "nice" "+")
The bald eagle does not eat the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "eats" "bald eagle" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "+")
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "nice" "-")
The dog eats the bald eagle.
Unknown
rconc
[@1: The dog eats the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "bald eagle" "+")
The bald eagle does not visit the bald eagle.
Unknown
inv-random
[@0: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bald eagle" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The bald eagle is big.[(triple1)] The bald eagle is red.[(triple2)] The cat needs the mouse.[(triple3)] The dog needs the bald eagle.[(triple4)] The dog needs the mouse.[(triple5)] The dog visits the bald eagle.[(triple6)] The mouse is red.[(triple7)] @1: The bald eagle needs the mouse.[(((triple6) -> rule4))] The bald eagle visits the mouse.[(((triple2) -> rule2))] The mouse visits the mouse.[(((triple7) -> rule2))] @2: The bald eagle needs the dog.[(((((triple2) -> rule2)) -> rule8))] The mouse needs the dog.[(((((triple7) -> rule2)) -> rule8))] @3: The dog is red.[(((((((triple2) -> rule2)) -> rule8)) -> rule9) OR ((((((triple7) -> rule2)) -> rule8)) -> rule9))] @4: The dog visits the mouse.[(((((((((triple2) -> rule2)) -> rule8)) -> rule9)) -> rule2) OR ((((((((triple7) -> rule2)) -> rule8)) -> rule9)) -> rule2))] @5: The dog needs the dog.[(((((((((((triple2) -> rule2)) -> rule8)) -> rule9)) -> rule2)) -> rule8) OR ((((((((((triple7) -> rule2)) -> rule8)) -> rule9)) -> rule2)) -> rule8))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple3
The dog needs the bald eagle.
("dog" "needs" "bald eagle" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple5
The dog visits the bald eagle.
("dog" "visits" "bald eagle" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
((triple6) -> (rule4 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
((triple2) -> (rule2 % int1))
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple7) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int1
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((((triple7) -> (rule2 % int2))) -> (rule8 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int2
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int3
((((((triple7) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((((((((triple2) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int3
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int4
((((((((triple7) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int4
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((((((triple2) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The bald eagle needs the dog.
("bald eagle" "needs" "dog" "+")
int4
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
int5
((((((((((triple7) -> (rule2 % int5))) -> (rule8 % int4))) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int4
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int5