The cow chases the mouse. The cow is cold. The cow is nice. The cow is red. The cow sees the mouse. The mouse chases the cow. The mouse is cold. The mouse is nice. The mouse likes the cow. The mouse sees the cow. If someone is red and they chase the cow then they like the cow. If someone sees the cow then the cow chases the mouse. If someone chases the cow then they like the cow. If someone likes the cow then they chase the mouse. If someone is rough and they like the cow then the cow is rough. If someone sees the mouse then the mouse sees the cow. If someone likes the mouse then the mouse chases the cow. If someone sees the cow then they chase the cow.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If someone is red and they chase the cow then they like the cow.
((("someone" "is" "red" "+") ("someone" "chases" "cow" "+")) -> ("someone" "likes" "cow" "+"))
If someone sees the cow then the cow chases the mouse.
((("someone" "sees" "cow" "+")) -> ("cow" "chases" "mouse" "+"))
If someone chases the cow then they like the cow.
((("someone" "chases" "cow" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow then they chase the mouse.
((("someone" "likes" "cow" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is rough and they like the cow then the cow is rough.
((("someone" "is" "rough" "+") ("someone" "likes" "cow" "+")) -> ("cow" "is" "rough" "+"))
If someone sees the mouse then the mouse sees the cow.
((("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
If someone likes the mouse then the mouse chases the cow.
((("someone" "likes" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
If someone sees the cow then they chase the cow.
((("someone" "sees" "cow" "+")) -> ("someone" "chases" "cow" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The cow is not red.
False
1
inv-proof
[(triple4)]
("cow" "is" "red" "-")
triple4
The mouse chases the mouse.
True
2
proof
[(((triple9) -> rule4) OR ((((triple6) -> rule3)) -> rule4) OR ((((((triple10) -> rule8)) -> rule3)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule8)) -> rule3)) -> rule4))]
("mouse" "chases" "mouse" "+")
((triple9) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
((((((triple10) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
((((((((triple5) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int4
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple9) -> rule4) OR ((((triple6) -> rule3)) -> rule4) OR ((((((triple10) -> rule8)) -> rule3)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule8)) -> rule3)) -> rule4))]
("mouse" "chases" "mouse" "-")
((triple9) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
((((((triple10) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
((((((((triple5) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int4
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "rough" "-")
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 see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cow chases the mouse.[(triple1 OR ((triple10) -> rule2) OR ((((triple5) -> rule6)) -> rule2))] The cow is cold.[(triple2)] The cow is nice.[(triple3)] The cow is red.[(triple4)] The cow sees the mouse.[(triple5)] The mouse chases the cow.[(triple6 OR ((triple10) -> rule8) OR ((((triple5) -> rule6)) -> rule8))] The mouse is cold.[(triple7)] The mouse is nice.[(triple8)] The mouse likes the cow.[(triple9 OR ((triple6) -> rule3) OR ((((triple10) -> rule8)) -> rule3) OR ((((((triple5) -> rule6)) -> rule8)) -> rule3))] The mouse sees the cow.[(triple10 OR ((triple5) -> rule6))] @1: The mouse chases the mouse.[(((triple9) -> rule4) OR ((((triple6) -> rule3)) -> rule4) OR ((((((triple10) -> rule8)) -> rule3)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule8)) -> rule3)) -> rule4))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
((triple10) -> (rule2 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple5
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple6
((triple10) -> (rule8 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule8 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple9
((triple6) -> (rule3 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
((((triple10) -> (rule8 % int2))) -> (rule3 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
((((((triple5) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
((triple5) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple9) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
((((((triple10) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
((((((((triple5) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int3
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int4