The cow chases the mouse. The mouse chases the cow. The mouse is young. If the mouse chases the cow and the mouse sees the cow then the mouse does not need the cow. Blue people are cold. If someone chases the mouse and the mouse is young then they need the mouse. If someone chases the cow and the cow is not young then the cow needs the mouse. If someone needs the cow then they chase the cow. If someone needs the mouse then the mouse is blue.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is young.
("mouse" "is" "young" "+")
If the mouse chases the cow and the mouse sees the cow then the mouse does not need the cow.
((("mouse" "chases" "cow" "+") ("mouse" "sees" "cow" "+")) -> ("mouse" "needs" "cow" "-"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone chases the mouse and the mouse is young then they need the mouse.
((("someone" "chases" "mouse" "+") ("mouse" "is" "young" "+")) -> ("someone" "needs" "mouse" "+"))
If someone chases the cow and the cow is not young then the cow needs the mouse.
((("someone" "chases" "cow" "+") ("cow" "is" "young" "~")) -> ("cow" "needs" "mouse" "+"))
If someone needs the cow then they chase the cow.
((("someone" "needs" "cow" "+")) -> ("someone" "chases" "cow" "+"))
If someone needs the mouse then the mouse is blue.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
The mouse chases the cow.
True
1
proof
[(triple2)]
("mouse" "chases" "cow" "+")
triple2
The mouse is not young.
False
1
inv-proof
[(triple3)]
("mouse" "is" "young" "-")
triple3
The cow needs the mouse.
True
3
proof
[(((triple1 triple3) -> rule3))]
("cow" "needs" "mouse" "+")
((triple1 triple3) -> (rule3 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow does not need the mouse.
False
3
inv-proof
[(((triple1 triple3) -> rule3))]
("cow" "needs" "mouse" "-")
((triple1 triple3) -> (rule3 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse is blue.
True
4
proof
[(((((triple1 triple3) -> rule3)) -> rule6))]
("mouse" "is" "blue" "+")
((((triple1 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse is not blue.
False
4
inv-proof
[(((((triple1 triple3) -> rule3)) -> rule6))]
("mouse" "is" "blue" "-")
((((triple1 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse is cold.
True
5
proof
[(((((((triple1 triple3) -> rule3)) -> rule6)) -> rule2))]
("mouse" "is" "cold" "+")
((((((triple1 triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The mouse is not cold.
False
5
inv-proof
[(((((((triple1 triple3) -> rule3)) -> rule6)) -> rule2))]
("mouse" "is" "cold" "-")
((((((triple1 triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "cold" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not see the mouse.
Unknown
inv-random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "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 mouse chases the cow.[(triple2)] The mouse is young.[(triple3)] @1: The cow needs the mouse.[(((triple1 triple3) -> rule3))] @2: The mouse is blue.[(((((triple1 triple3) -> rule3)) -> rule6))] @3: The mouse is cold.[(((((((triple1 triple3) -> rule3)) -> rule6)) -> rule2))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple1 triple3) -> (rule3 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple1 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
((((((triple1 triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3