The cat does not need the mouse. The cow needs the mouse. The mouse needs the cow. If someone needs the cow then the cow eats the mouse. If someone eats the mouse then they see the cat. If someone eats the cat then they do not see the mouse.
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
If someone needs the cow then the cow eats the mouse.
((("someone" "needs" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
If someone eats the mouse then they see the cat.
((("someone" "eats" "mouse" "+")) -> ("someone" "sees" "cat" "+"))
If someone eats the cat then they do not see the mouse.
((("someone" "eats" "cat" "+")) -> ("someone" "sees" "mouse" "-"))
The cat does not need the mouse.
True
1
proof
[(triple1)]
("cat" "needs" "mouse" "-")
triple1
The cow does not need the mouse.
False
1
inv-proof
[(triple2)]
("cow" "needs" "mouse" "-")
triple2
The cow eats the mouse.
True
2
proof
[(((triple3) -> rule1))]
("cow" "eats" "mouse" "+")
((triple3) -> (rule1 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow does not eat the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("cow" "eats" "mouse" "-")
((triple3) -> (rule1 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow sees the cat.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("cow" "sees" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow does not see the cat.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("cow" "sees" "cat" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cat" "-")
The mouse sees the cat.
Unknown
rconc
[@1: The mouse sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "cat" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cat eats the cow.
Unknown
random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "+")
@0: The cat does not need the mouse.[(triple1)] The cow needs the mouse.[(triple2)] The mouse needs the cow.[(triple3)] @1: The cow eats the mouse.[(((triple3) -> rule1))] @2: The cow sees the cat.[(((((triple3) -> rule1)) -> rule2))]
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple3
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((triple3) -> (rule1 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2