The cow chases the mouse. The cow is blue. The cow is nice. The cow is round. The cow sees the rabbit. The mouse chases the cow. The mouse is blue. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit chases the mouse. The rabbit needs the cow. The rabbit sees the cow. If something chases the rabbit then the rabbit is rough. If something is rough and it needs the rabbit then it is round. If something is nice and it needs the rabbit then it sees the rabbit. If something needs the cow then the cow chases the rabbit. If the cow needs the rabbit and the rabbit is kind then the rabbit chases the cow. If the rabbit is rough then the rabbit sees the mouse. If something chases the mouse then it needs the cow. If something needs the mouse and it is round then it chases the cow.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something chases the rabbit then the rabbit is rough.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If something is rough and it needs the rabbit then it is round.
((("something" "is" "rough" "+") ("something" "needs" "rabbit" "+")) -> ("something" "is" "round" "+"))
If something is nice and it needs the rabbit then it sees the rabbit.
((("something" "is" "nice" "+") ("something" "needs" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If something needs the cow then the cow chases the rabbit.
((("something" "needs" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
If the cow needs the rabbit and the rabbit is kind then the rabbit chases the cow.
((("cow" "needs" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "chases" "cow" "+"))
If the rabbit is rough then the rabbit sees the mouse.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something chases the mouse then it needs the cow.
((("something" "chases" "mouse" "+")) -> ("something" "needs" "cow" "+"))
If something needs the mouse and it is round then it chases the cow.
((("something" "needs" "mouse" "+") ("something" "is" "round" "+")) -> ("something" "chases" "cow" "+"))
The cow is blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "+")
triple2
The cow is not nice.
False
1
inv-proof
[(triple3)]
("cow" "is" "nice" "-")
triple3
The cow needs the cow.
True
2
proof
[(((triple1) -> rule7))]
("cow" "needs" "cow" "+")
((triple1) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple1) -> rule7))]
("cow" "needs" "cow" "-")
((triple1) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The rabbit is rough.
True
3
proof
[(((((triple11) -> rule4)) -> rule1) OR ((((((triple1) -> rule7)) -> rule4)) -> rule1) OR ((((((triple10) -> rule7)) -> rule4)) -> rule1))]
("rabbit" "is" "rough" "+")
((((triple11) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit is not rough.
False
3
inv-proof
[(((((triple11) -> rule4)) -> rule1) OR ((((((triple1) -> rule7)) -> rule4)) -> rule1) OR ((((((triple10) -> rule7)) -> rule4)) -> rule1))]
("rabbit" "is" "rough" "-")
((((triple11) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit sees the mouse.
True
4
proof
[(((((((triple11) -> rule4)) -> rule1)) -> rule6) OR ((((((((triple1) -> rule7)) -> rule4)) -> rule1)) -> rule6) OR ((((((((triple10) -> rule7)) -> rule4)) -> rule1)) -> rule6))]
("rabbit" "sees" "mouse" "+")
((((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
((((((((triple10) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit does not see the mouse.
False
4
inv-proof
[(((((((triple11) -> rule4)) -> rule1)) -> rule6) OR ((((((((triple1) -> rule7)) -> rule4)) -> rule1)) -> rule6) OR ((((((((triple10) -> rule7)) -> rule4)) -> rule1)) -> rule6))]
("rabbit" "sees" "mouse" "-")
((((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
((((((((triple10) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "round" "-")
The rabbit chases the cow.
Unknown
rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "chases" "cow" "+")
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "round" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "chases" "cow" "+")
The cow does not need the mouse.
Unknown
inv-random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
@0: The cow chases the mouse.[(triple1)] The cow is blue.[(triple2)] The cow is nice.[(triple3)] The cow is round.[(triple4)] The cow sees the rabbit.[(triple5)] The mouse chases the cow.[(triple6)] The mouse is blue.[(triple7)] The mouse needs the rabbit.[(triple8)] The mouse sees the rabbit.[(triple9)] The rabbit chases the mouse.[(triple10)] The rabbit needs the cow.[(triple11 OR ((triple10) -> rule7))] The rabbit sees the cow.[(triple12)] @1: The cow chases the rabbit.[(((triple11) -> rule4) OR ((((triple1) -> rule7)) -> rule4) OR ((((triple10) -> rule7)) -> rule4))] The cow needs the cow.[(((triple1) -> rule7))] @2: The rabbit is rough.[(((((triple11) -> rule4)) -> rule1) OR ((((((triple1) -> rule7)) -> rule4)) -> rule1) OR ((((((triple10) -> rule7)) -> rule4)) -> rule1))] @3: The rabbit sees the mouse.[(((((((triple11) -> rule4)) -> rule1)) -> rule6) OR ((((((((triple1) -> rule7)) -> rule4)) -> rule1)) -> rule6) OR ((((((((triple10) -> rule7)) -> rule4)) -> rule1)) -> rule6))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple5
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple9
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple10
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple11
((triple10) -> (rule7 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple12
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((triple11) -> (rule4 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple1) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple11) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((((((triple11) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
((((((((triple10) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4