The bald eagle chases the mouse. The cow chases the bald eagle. The cow is rough. The lion chases the cow. The lion is rough. The mouse chases the lion. The mouse visits the lion. If someone is rough then they visit the cow. If someone likes the cow then they are rough. If someone chases the lion then they chase the bald eagle. If someone likes the lion and the lion visits the bald eagle then the bald eagle visits the cow. If someone likes the mouse then the mouse likes the cow. If someone chases the cow then the cow likes the lion. If someone visits the cow then the cow likes the mouse.
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
The cow is rough.
("cow" "is" "rough" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone is rough then they visit the cow.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "cow" "+"))
If someone likes the cow then they are rough.
((("someone" "likes" "cow" "+")) -> ("someone" "is" "rough" "+"))
If someone chases the lion then they chase the bald eagle.
((("someone" "chases" "lion" "+")) -> ("someone" "chases" "bald eagle" "+"))
If someone likes the lion and the lion visits the bald eagle then the bald eagle visits the cow.
((("someone" "likes" "lion" "+") ("lion" "visits" "bald eagle" "+")) -> ("bald eagle" "visits" "cow" "+"))
If someone likes the mouse then the mouse likes the cow.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If someone chases the cow then the cow likes the lion.
((("someone" "chases" "cow" "+")) -> ("cow" "likes" "lion" "+"))
If someone visits the cow then the cow likes the mouse.
((("someone" "visits" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
The cow is rough.
True
1
proof
[(triple3)]
("cow" "is" "rough" "+")
triple3
The cow does not chase the bald eagle.
False
1
inv-proof
[(triple2)]
("cow" "chases" "bald eagle" "-")
triple2
The lion visits the cow.
True
2
proof
[(((triple5) -> rule1))]
("lion" "visits" "cow" "+")
((triple5) -> (rule1 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The mouse does not chase the bald eagle.
False
2
inv-proof
[(((triple6) -> rule3))]
("mouse" "chases" "bald eagle" "-")
((triple6) -> (rule3 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The cow likes the mouse.
True
3
proof
[(((((triple3) -> rule1)) -> rule7) OR ((((triple5) -> rule1)) -> rule7))]
("cow" "likes" "mouse" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule7 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow does not like the mouse.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7) OR ((((triple5) -> rule1)) -> rule7))]
("cow" "likes" "mouse" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule7 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The mouse likes the cow.
True
4
proof
[(((((((triple3) -> rule1)) -> rule7)) -> rule5) OR ((((((triple5) -> rule1)) -> rule7)) -> rule5))]
("mouse" "likes" "cow" "+")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The mouse does not like the cow.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule7)) -> rule5) OR ((((((triple5) -> rule1)) -> rule7)) -> rule5))]
("mouse" "likes" "cow" "-")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The mouse is rough.
True
5
proof
[(((((((((triple3) -> rule1)) -> rule7)) -> rule5)) -> rule2) OR ((((((((triple5) -> rule1)) -> rule7)) -> rule5)) -> rule2))]
("mouse" "is" "rough" "+")
((((((((triple3) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
((((((((triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The mouse is not rough.
False
5
inv-proof
[(((((((((triple3) -> rule1)) -> rule7)) -> rule5)) -> rule2) OR ((((((((triple5) -> rule1)) -> rule7)) -> rule5)) -> rule2))]
("mouse" "is" "rough" "-")
((((((((triple3) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
((((((((triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The mouse visits the cow.
True
6
proof
[(((((((((((triple3) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule1) OR ((((((((((triple5) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule1))]
("mouse" "visits" "cow" "+")
((((((((((triple3) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The cow visits the cow.
("cow" "visits" "cow" "+")
int5
((((((((((triple5) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5
The mouse does not visit the cow.
False
6
inv-proof
[(((((((((((triple3) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule1) OR ((((((((((triple5) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule1))]
("mouse" "visits" "cow" "-")
((((((((((triple3) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The cow visits the cow.
("cow" "visits" "cow" "+")
int5
((((((((((triple5) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5
The bald eagle does not visit the cow.
Unknown
inv-rconc
[@2: The bald eagle visits the cow.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bald eagle" "visits" "cow" "-")
The bald eagle is rough.
Unknown
rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "rough" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The lion chases the bald eagle.
Unknown
rconc
[@1: The lion chases the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "bald eagle" "+")
The bald eagle does not chase the lion.
Unknown
inv-random
[@0: The bald eagle chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "lion" "-")
The bald eagle visits the mouse.
Unknown
random
[@0: The bald eagle visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "mouse" "+")
The cow does not visit the lion.
Unknown
inv-random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "-")
The bald eagle visits the lion.
Unknown
random
[@0: The bald eagle visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "lion" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The bald eagle chases the mouse.[(triple1)] The cow chases the bald eagle.[(triple2)] The cow is rough.[(triple3)] The lion chases the cow.[(triple4)] The lion is rough.[(triple5)] The mouse chases the lion.[(triple6)] The mouse visits the lion.[(triple7)] @1: The cow likes the lion.[(((triple4) -> rule6))] The cow visits the cow.[(((triple3) -> rule1))] The lion visits the cow.[(((triple5) -> rule1))] The mouse chases the bald eagle.[(((triple6) -> rule3))] @2: The cow likes the mouse.[(((((triple3) -> rule1)) -> rule7) OR ((((triple5) -> rule1)) -> rule7))] @3: The mouse likes the cow.[(((((((triple3) -> rule1)) -> rule7)) -> rule5) OR ((((((triple5) -> rule1)) -> rule7)) -> rule5))] @4: The mouse is rough.[(((((((((triple3) -> rule1)) -> rule7)) -> rule5)) -> rule2) OR ((((((((triple5) -> rule1)) -> rule7)) -> rule5)) -> rule2))] @5: The mouse visits the cow.[(((((((((((triple3) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule1) OR ((((((((((triple5) -> rule1)) -> rule7)) -> rule5)) -> rule2)) -> rule1))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple1
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The lion chases the cow.
("lion" "chases" "cow" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple6
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple7
The cow likes the lion.
("cow" "likes" "lion" "+")
((triple4) -> (rule6 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple3) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
((triple5) -> (rule1 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
((triple6) -> (rule3 % int1))
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule7 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((((((((triple3) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
((((((((triple5) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((((((((((triple3) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The cow visits the cow.
("cow" "visits" "cow" "+")
int5
((((((((((triple5) -> (rule1 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5