The cow chases the mouse. The cow needs the dog. The cow needs the mouse. The cow sees the dog. The dog is green. The dog needs the mouse. The mouse is green. If someone chases the mouse then the mouse is blue. If someone needs the cow then they are cold. If the dog chases the cow and the dog needs the mouse then the mouse is blue. If someone sees the cow then they are rough. If someone is green then they chase the cow. If the mouse chases the dog and the mouse is green then the dog sees the cow. If someone chases the dog and the dog is cold then they chase the cow. If the mouse is blue then the mouse sees the cow.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
If someone chases the mouse then the mouse is blue.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone needs the cow then they are cold.
((("someone" "needs" "cow" "+")) -> ("someone" "is" "cold" "+"))
If the dog chases the cow and the dog needs the mouse then the mouse is blue.
((("dog" "chases" "cow" "+") ("dog" "needs" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone sees the cow then they are rough.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "rough" "+"))
If someone is green then they chase the cow.
((("someone" "is" "green" "+")) -> ("someone" "chases" "cow" "+"))
If the mouse chases the dog and the mouse is green then the dog sees the cow.
((("mouse" "chases" "dog" "+") ("mouse" "is" "green" "+")) -> ("dog" "sees" "cow" "+"))
If someone chases the dog and the dog is cold then they chase the cow.
((("someone" "chases" "dog" "+") ("dog" "is" "cold" "+")) -> ("someone" "chases" "cow" "+"))
If the mouse is blue then the mouse sees the cow.
((("mouse" "is" "blue" "+")) -> ("mouse" "sees" "cow" "+"))
The cow chases the mouse.
True
1
proof
[(triple1)]
("cow" "chases" "mouse" "+")
triple1
The dog is not green.
False
1
inv-proof
[(triple5)]
("dog" "is" "green" "-")
triple5
The mouse is blue.
True
2
proof
[(((triple1) -> rule1) OR ((((triple5) -> rule5) triple6) -> rule3))]
("mouse" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple5) -> (rule5 % int2)) triple6) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The dog does not chase the cow.
False
2
inv-proof
[(((triple5) -> rule5))]
("dog" "chases" "cow" "-")
((triple5) -> (rule5 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The mouse sees the cow.
True
3
proof
[(((((triple1) -> rule1)) -> rule8) OR ((((((triple5) -> rule5) triple6) -> rule3)) -> rule8))]
("mouse" "sees" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((((triple5) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The dog chases the cow.
("dog" "chases" "cow" "+")
int3
The mouse does not see the cow.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8) OR ((((((triple5) -> rule5) triple6) -> rule3)) -> rule8))]
("mouse" "sees" "cow" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((((triple5) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The dog chases the cow.
("dog" "chases" "cow" "+")
int3
The dog is not rough.
Unknown
inv-rconc
[@2: The dog is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("dog" "is" "rough" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "rough" "+")
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "cold" "-")
The mouse sees the dog.
Unknown
random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse needs the cow.
Unknown
random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "+")
@0: The cow chases the mouse.[(triple1)] The cow needs the dog.[(triple2)] The cow needs the mouse.[(triple3)] The cow sees the dog.[(triple4)] The dog is green.[(triple5)] The dog needs the mouse.[(triple6)] The mouse is green.[(triple7)] @1: The dog chases the cow.[(((triple5) -> rule5))] The mouse chases the cow.[(((triple7) -> rule5))] The mouse is blue.[(((triple1) -> rule1) OR ((((triple5) -> rule5) triple6) -> rule3))] @2: The mouse sees the cow.[(((((triple1) -> rule1)) -> rule8) OR ((((((triple5) -> rule5) triple6) -> rule3)) -> rule8))] @3: The mouse is rough.[(((((((triple1) -> rule1)) -> rule8)) -> rule4) OR ((((((((triple5) -> rule5) triple6) -> rule3)) -> rule8)) -> rule4))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The dog chases the cow.
("dog" "chases" "cow" "+")
((triple5) -> (rule5 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
((triple7) -> (rule5 % int1))
The mouse chases the cow.
("mouse" "chases" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple5) -> (rule5 % int2)) triple6) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((((triple5) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule8 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The dog chases the cow.
("dog" "chases" "cow" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((((triple5) -> (rule5 % int4)) triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The dog chases the cow.
("dog" "chases" "cow" "+")
int4