The bald eagle likes the bear. The bald eagle likes the cat. The bald eagle visits the bear. The bald eagle visits the mouse. The bear likes the mouse. The bear needs the bald eagle. The bear needs the cat. The bear needs the mouse. The cat is nice. The mouse is big. The mouse needs the bear. The mouse visits the bald eagle. If someone needs the mouse then they like the cat. If the cat visits the bald eagle and the cat is round then the bald eagle is kind. If someone visits the mouse and the mouse is kind then the mouse is rough. If the bear likes the mouse and the mouse needs the bear then the mouse needs the cat. If someone likes the cat then the cat is round. If someone is nice then they like the bear. If someone is kind then they need the mouse. If someone is round then they visit the bald eagle.
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat is nice.
("cat" "is" "nice" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
If someone needs the mouse then they like the cat.
((("someone" "needs" "mouse" "+")) -> ("someone" "likes" "cat" "+"))
If the cat visits the bald eagle and the cat is round then the bald eagle is kind.
((("cat" "visits" "bald eagle" "+") ("cat" "is" "round" "+")) -> ("bald eagle" "is" "kind" "+"))
If someone visits the mouse and the mouse is kind then the mouse is rough.
((("someone" "visits" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "is" "rough" "+"))
If the bear likes the mouse and the mouse needs the bear then the mouse needs the cat.
((("bear" "likes" "mouse" "+") ("mouse" "needs" "bear" "+")) -> ("mouse" "needs" "cat" "+"))
If someone likes the cat then the cat is round.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "round" "+"))
If someone is nice then they like the bear.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "bear" "+"))
If someone is kind then they need the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is round then they visit the bald eagle.
((("someone" "is" "round" "+")) -> ("someone" "visits" "bald eagle" "+"))
The mouse visits the bald eagle.
True
1
proof
[(triple12)]
("mouse" "visits" "bald eagle" "+")
triple12
The bear does not need the bald eagle.
False
1
inv-proof
[(triple6)]
("bear" "needs" "bald eagle" "-")
triple6
The bear likes the cat.
True
2
proof
[(((triple8) -> rule1))]
("bear" "likes" "cat" "+")
((triple8) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat is not round.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple8) -> rule1)) -> rule5))]
("cat" "is" "round" "-")
((triple2) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat visits the bald eagle.
True
3
proof
[(((((triple2) -> rule5)) -> rule8) OR ((((((triple8) -> rule1)) -> rule5)) -> rule8))]
("cat" "visits" "bald eagle" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The cat does not visit the bald eagle.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule8) OR ((((((triple8) -> rule1)) -> rule5)) -> rule8))]
("cat" "visits" "bald eagle" "-")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The bald eagle is kind.
True
6
proof
[(((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2) OR ((((((triple2) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2) OR ((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2) OR ((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2))]
("bald eagle" "is" "kind" "+")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2) -> (rule5 % int4))) -> (rule8 % int3)) ((((triple8) -> (rule1 % int2))) -> (rule5 % int4))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bald eagle is not kind.
False
6
inv-proof
[(((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2) OR ((((((triple2) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2) OR ((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2) OR ((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2))]
("bald eagle" "is" "kind" "-")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2) -> (rule5 % int4))) -> (rule8 % int3)) ((((triple8) -> (rule1 % int2))) -> (rule5 % int4))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The cat does not need the mouse.
Unknown
inv-rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "needs" "mouse" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "bear" "+")
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "rough" "-")
The cat likes the cat.
Unknown
rconc
[@2: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("cat" "likes" "cat" "+")
The mouse does not visit the cat.
Unknown
inv-random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "-")
The bald eagle likes the bald eagle.
Unknown
random
[@0: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "bald eagle" "+")
The cat does not need the bald eagle.
Unknown
inv-random
[@0: The cat needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bald eagle" "-")
The mouse visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
@0: The bald eagle likes the bear.[(triple1)] The bald eagle likes the cat.[(triple2 OR ((((((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7)) -> rule1))] The bald eagle visits the bear.[(triple3)] The bald eagle visits the mouse.[(triple4)] The bear likes the mouse.[(triple5)] The bear needs the bald eagle.[(triple6)] The bear needs the cat.[(triple7)] The bear needs the mouse.[(triple8)] The cat is nice.[(triple9)] The mouse is big.[(triple10)] The mouse needs the bear.[(triple11)] The mouse visits the bald eagle.[(triple12)] @1: The bear likes the cat.[(((triple8) -> rule1))] The cat is round.[(((triple2) -> rule5) OR ((((triple8) -> rule1)) -> rule5))] The cat likes the bear.[(((triple9) -> rule6))] The mouse needs the cat.[(((triple5 triple11) -> rule4))] @2: The cat visits the bald eagle.[(((((triple2) -> rule5)) -> rule8) OR ((((((triple8) -> rule1)) -> rule5)) -> rule8))] @3: The bald eagle is kind.[(((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2) OR ((((((triple2) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2) OR ((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2) OR ((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2))] @4: The bald eagle needs the mouse.[(((((((((triple2) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2)) -> rule7) OR ((((((((triple2) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7) OR ((((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((triple2) -> rule5)) -> rule2)) -> rule7) OR ((((((((((triple8) -> rule1)) -> rule5)) -> rule8) ((((triple8) -> rule1)) -> rule5)) -> rule2)) -> rule7))]
The bald eagle likes the bear.
("bald eagle" "likes" "bear" "+")
triple1
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
triple2
((((((((((((triple8) -> (rule1 % int6))) -> (rule5 % int5))) -> (rule8 % int4)) ((((triple8) -> (rule1 % int6))) -> (rule5 % int5))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The bald eagle likes the cat.
("bald eagle" "likes" "cat" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5
The bear likes the cat.
("bear" "likes" "cat" "+")
int6
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
triple3
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
triple4
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple5
The bear needs the bald eagle.
("bear" "needs" "bald eagle" "+")
triple6
The bear needs the cat.
("bear" "needs" "cat" "+")
triple7
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple8
The cat is nice.
("cat" "is" "nice" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple11
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple12
The bear likes the cat.
("bear" "likes" "cat" "+")
((triple8) -> (rule1 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple2) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
((triple9) -> (rule6 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple5 triple11) -> (rule4 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
((((((triple2) -> (rule5 % int4))) -> (rule8 % int3)) ((((triple8) -> (rule1 % int2))) -> (rule5 % int4))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((triple2) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((((triple8) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule8 % int3)) ((triple2) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
((((((((triple2) -> (rule5 % int5))) -> (rule8 % int4)) ((((triple8) -> (rule1 % int3))) -> (rule5 % int5))) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5
((((((((((triple8) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) ((triple2) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The bear likes the cat.
("bear" "likes" "cat" "+")
int5
((((((((((triple8) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule8 % int3)) ((((triple8) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The bear likes the cat.
("bear" "likes" "cat" "+")
int5