The cow is cold. The mouse eats the cow. If the cow needs the mouse then the mouse is kind. If someone needs the mouse and the mouse is red then they are big. If someone is kind then they visit the cow. If someone eats the mouse then the mouse is not blue. If someone eats the cow then the cow needs the mouse. If someone is cold then they need the cow. If the mouse is cold and the mouse is not red then the mouse does not need the cow. If the cow visits the mouse and the mouse does not visit the cow then the mouse does not need the cow.
The cow is cold.
("cow" "is" "cold" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
If the cow needs the mouse then the mouse is kind.
((("cow" "needs" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If someone needs the mouse and the mouse is red then they are big.
((("someone" "needs" "mouse" "+") ("mouse" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is kind then they visit the cow.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "cow" "+"))
If someone eats the mouse then the mouse is not blue.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "blue" "-"))
If someone eats the cow then the cow needs the mouse.
((("someone" "eats" "cow" "+")) -> ("cow" "needs" "mouse" "+"))
If someone is cold then they need the cow.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "cow" "+"))
If the mouse is cold and the mouse is not red then the mouse does not need the cow.
((("mouse" "is" "cold" "+") ("mouse" "is" "red" "~")) -> ("mouse" "needs" "cow" "-"))
If the cow visits the mouse and the mouse does not visit the cow then the mouse does not need the cow.
((("cow" "visits" "mouse" "+") ("mouse" "visits" "cow" "~")) -> ("mouse" "needs" "cow" "-"))
The cow is cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The cow is not cold.
False
1
inv-proof
[(triple1)]
("cow" "is" "cold" "-")
triple1
The cow needs the cow.
True
2
proof
[(((triple1) -> rule6))]
("cow" "needs" "cow" "+")
((triple1) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple1) -> rule6))]
("cow" "needs" "cow" "-")
((triple1) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The mouse is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("mouse" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse is not kind.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("mouse" "is" "kind" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse visits the cow.
True
4
proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("mouse" "visits" "cow" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The mouse does not visit the cow.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("mouse" "visits" "cow" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "cow" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "big" "+")
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "big" "-")
The mouse needs the cow.
Unknown
rconc
[@1: The mouse needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "needs" "cow" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The cow does not visit the mouse.
Unknown
inv-random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cow is cold.[(triple1)] The mouse eats the cow.[(triple2)] @1: The cow needs the cow.[(((triple1) -> rule6))] The cow needs the mouse.[(((triple2) -> rule5))] @2: The mouse is kind.[(((((triple2) -> rule5)) -> rule1))] @3: The mouse visits the cow.[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple1) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple2) -> (rule5 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3