The bald eagle chases the cow. The bald eagle chases the mouse. The bald eagle is round. The bald eagle needs the cow. The cat is nice. The cat is round. The cat needs the bald eagle. The cat sees the mouse. The cow is cold. The cow does not need the bald eagle. The cow does not need the mouse. The mouse chases the cow. If something needs the mouse then the mouse is nice. If something needs the cat and the cat chases the bald eagle then the cat needs the cow. If something needs the cow then it is nice. If something needs the cow and it needs the cat then it does not see the cat. If something chases the cow and it chases the bald eagle then the cow sees the bald eagle. If something is young then it needs the mouse. All nice things are young.
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow does not need the bald eagle.
("cow" "needs" "bald eagle" "-")
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
If something needs the mouse then the mouse is nice.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If something needs the cat and the cat chases the bald eagle then the cat needs the cow.
((("something" "needs" "cat" "+") ("cat" "chases" "bald eagle" "+")) -> ("cat" "needs" "cow" "+"))
If something needs the cow then it is nice.
((("something" "needs" "cow" "+")) -> ("something" "is" "nice" "+"))
If something needs the cow and it needs the cat then it does not see the cat.
((("something" "needs" "cow" "+") ("something" "needs" "cat" "+")) -> ("something" "sees" "cat" "-"))
If something chases the cow and it chases the bald eagle then the cow sees the bald eagle.
((("something" "chases" "cow" "+") ("something" "chases" "bald eagle" "+")) -> ("cow" "sees" "bald eagle" "+"))
If something is young then it needs the mouse.
((("something" "is" "young" "+")) -> ("something" "needs" "mouse" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
The bald eagle needs the cow.
True
1
proof
[(triple4)]
("bald eagle" "needs" "cow" "+")
triple4
The cat is not nice.
False
1
inv-proof
[(triple5)]
("cat" "is" "nice" "-")
triple5
The bald eagle is nice.
True
2
proof
[(((triple4) -> rule3))]
("bald eagle" "is" "nice" "+")
((triple4) -> (rule3 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The cat is not young.
False
2
inv-proof
[(((triple5) -> rule7))]
("cat" "is" "young" "-")
((triple5) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat needs the mouse.
True
3
proof
[(((((triple5) -> rule7)) -> rule6))]
("cat" "needs" "mouse" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The bald eagle is not young.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule7))]
("bald eagle" "is" "young" "-")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The bald eagle needs the mouse.
True
4
proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule6))]
("bald eagle" "needs" "mouse" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int3
The bald eagle does not need the mouse.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule6))]
("bald eagle" "needs" "mouse" "-")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int3
The mouse is young.
True
5
proof
[(((((((((triple5) -> rule7)) -> rule6)) -> rule1)) -> rule7) OR ((((((((((triple4) -> rule3)) -> rule7)) -> rule6)) -> rule1)) -> rule7))]
("mouse" "is" "young" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((((((((((triple4) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int3
The bald eagle is young.
("bald eagle" "is" "young" "+")
int4
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int5
The mouse is not young.
False
5
inv-proof
[(((((((((triple5) -> rule7)) -> rule6)) -> rule1)) -> rule7) OR ((((((((((triple4) -> rule3)) -> rule7)) -> rule6)) -> rule1)) -> rule7))]
("mouse" "is" "young" "-")
((((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((((((((((triple4) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int3
The bald eagle is young.
("bald eagle" "is" "young" "+")
int4
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int5
The mouse needs the mouse.
True
6
proof
[(((((((((((triple5) -> rule7)) -> rule6)) -> rule1)) -> rule7)) -> rule6) OR ((((((((((((triple4) -> rule3)) -> rule7)) -> rule6)) -> rule1)) -> rule7)) -> rule6))]
("mouse" "needs" "mouse" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
The cat is young.
("cat" "is" "young" "+")
int5
((((((((((((triple4) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int4
The bald eagle is young.
("bald eagle" "is" "young" "+")
int5
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int6
The mouse does not need the mouse.
False
6
inv-proof
[(((((((((((triple5) -> rule7)) -> rule6)) -> rule1)) -> rule7)) -> rule6) OR ((((((((((((triple4) -> rule3)) -> rule7)) -> rule6)) -> rule1)) -> rule7)) -> rule6))]
("mouse" "needs" "mouse" "-")
((((((((((triple5) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
The cat is young.
("cat" "is" "young" "+")
int5
((((((((((((triple4) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int4
The bald eagle is young.
("bald eagle" "is" "young" "+")
int5
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int6
The cow is not young.
Unknown
inv-rconc
[@2: The cow is young.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("cow" "is" "young" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "nice" "+")
The cat does not need the cow.
Unknown
inv-rconc
[@1: The cat needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cow" "-")
The cow sees the bald eagle.
Unknown
rconc
[@1: The cow sees the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "bald eagle" "+")
The cow does not see the cat.
Unknown
inv-random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The bald eagle chases the bald eagle.
Unknown
random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "+")
The mouse does not chase the cat.
Unknown
inv-random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "-")
The cat chases the bald eagle.
Unknown
random
[@0: The cat chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bald eagle" "+")
The bald eagle does not see the mouse.
Unknown
inv-random
[@0: The bald eagle sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "mouse" "-")
The mouse needs the bald eagle.
Unknown
random
[@0: The mouse needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bald eagle" "+")
@0: The bald eagle chases the cow.[(triple1)] The bald eagle chases the mouse.[(triple2)] The bald eagle is round.[(triple3)] The bald eagle needs the cow.[(triple4)] The cat is nice.[(triple5)] The cat is round.[(triple6)] The cat needs the bald eagle.[(triple7)] The cat sees the mouse.[(triple8)] The cow does not need the bald eagle.[(triple10)] The cow does not need the mouse.[(triple11)] The cow is cold.[(triple9)] The mouse chases the cow.[(triple12)] @1: The bald eagle is nice.[(((triple4) -> rule3))] The cat is young.[(((triple5) -> rule7))] @2: The bald eagle is young.[(((((triple4) -> rule3)) -> rule7))] The cat needs the mouse.[(((((triple5) -> rule7)) -> rule6))] @3: The bald eagle needs the mouse.[(((((((triple4) -> rule3)) -> rule7)) -> rule6))] The mouse is nice.[(((((((triple5) -> rule7)) -> rule6)) -> rule1) OR ((((((((triple4) -> rule3)) -> rule7)) -> rule6)) -> rule1))] @4: The mouse is young.[(((((((((triple5) -> rule7)) -> rule6)) -> rule1)) -> rule7) OR ((((((((((triple4) -> rule3)) -> rule7)) -> rule6)) -> rule1)) -> rule7))] @5: The mouse needs the mouse.[(((((((((((triple5) -> rule7)) -> rule6)) -> rule1)) -> rule7)) -> rule6) OR ((((((((((((triple4) -> rule3)) -> rule7)) -> rule6)) -> rule1)) -> rule7)) -> rule6))]
The bald eagle chases the cow.
("bald eagle" "chases" "cow" "+")
triple1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple2
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple3
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple7
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple8
The cow does not need the bald eagle.
("cow" "needs" "bald eagle" "-")
triple10
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
triple11
The cow is cold.
("cow" "is" "cold" "+")
triple9
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple12
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
((triple4) -> (rule3 % int1))
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple5) -> (rule7 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
((((((triple5) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cat is young.
("cat" "is" "young" "+")
int3
((((((((triple4) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The bald eagle is young.
("bald eagle" "is" "young" "+")
int3
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int3
The cat is young.
("cat" "is" "young" "+")
int4
((((((((((triple4) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int3
The bald eagle is young.
("bald eagle" "is" "young" "+")
int4
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int5
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int4
The cat is young.
("cat" "is" "young" "+")
int5
((((((((((((triple4) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int4
The bald eagle is young.
("bald eagle" "is" "young" "+")
int5
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
int6