The cow does not chase the mouse. The mouse is not red. The tiger is rough. If the mouse is nice and the mouse likes the tiger then the mouse does not like the cow. If the mouse is not red then the mouse sees the tiger. If something sees the tiger then the tiger is nice. If the mouse likes the tiger and the mouse is not round then the tiger does not like the mouse. If something chases the mouse then it sees the tiger. If something chases the mouse and it likes the mouse then it chases the tiger. If something is nice then it does not like the cow. If something likes the mouse and it chases the cow then it does not see the mouse.
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
The mouse is not red.
("mouse" "is" "red" "-")
The tiger is rough.
("tiger" "is" "rough" "+")
If the mouse is nice and the mouse likes the tiger then the mouse does not like the cow.
((("mouse" "is" "nice" "+") ("mouse" "likes" "tiger" "+")) -> ("mouse" "likes" "cow" "-"))
If the mouse is not red then the mouse sees the tiger.
((("mouse" "is" "red" "~")) -> ("mouse" "sees" "tiger" "+"))
If something sees the tiger then the tiger is nice.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If the mouse likes the tiger and the mouse is not round then the tiger does not like the mouse.
((("mouse" "likes" "tiger" "+") ("mouse" "is" "round" "~")) -> ("tiger" "likes" "mouse" "-"))
If something chases the mouse then it sees the tiger.
((("something" "chases" "mouse" "+")) -> ("something" "sees" "tiger" "+"))
If something chases the mouse and it likes the mouse then it chases the tiger.
((("something" "chases" "mouse" "+") ("something" "likes" "mouse" "+")) -> ("something" "chases" "tiger" "+"))
If something is nice then it does not like the cow.
((("something" "is" "nice" "+")) -> ("something" "likes" "cow" "-"))
If something likes the mouse and it chases the cow then it does not see the mouse.
((("something" "likes" "mouse" "+") ("something" "chases" "cow" "+")) -> ("something" "sees" "mouse" "-"))
The mouse is not red.
True
1
proof
[(triple2)]
("mouse" "is" "red" "-")
triple2
The tiger is not rough.
False
1
inv-proof
[(triple3)]
("tiger" "is" "rough" "-")
triple3
The mouse sees the tiger.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse does not see the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "sees" "tiger" "-")
((triple2) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger is nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("tiger" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger is not nice.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("tiger" "is" "nice" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger does not like the cow.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule7))]
("tiger" "likes" "cow" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The tiger likes the cow.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule7))]
("tiger" "likes" "cow" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The cow does not chase the tiger.
Unknown
inv-rconc
[@1: The cow chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "chases" "tiger" "-")
The mouse chases the tiger.
Unknown
rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "chases" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The cow sees the tiger.
Unknown
rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "tiger" "+")
The mouse does not like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cow does not chase the mouse.[(triple1)] The mouse is not red.[(triple2)] The tiger is rough.[(triple3)] @1: The mouse sees the tiger.[(((triple2) -> rule2))] @2: The tiger is nice.[(((((triple2) -> rule2)) -> rule3))] @3: The tiger does not like the cow.[(((((((triple2) -> rule2)) -> rule3)) -> rule7))]
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
triple1
The mouse is not red.
("mouse" "is" "red" "-")
triple2
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3