The cat sees the mouse. The cow is big. The cow is cold. The cow sees the mouse. The mouse eats the cat. The tiger eats the mouse. The tiger is young. If something needs the tiger and the tiger eats the mouse then the mouse sees the tiger. If something needs the cat and it is not young then it is big. If something is big then it does not see the cow. If something eats the cat and it is big then it is not rough. If something eats the cow and the cow sees the tiger then the tiger is not rough. If the tiger needs the mouse then the tiger sees the mouse.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is young.
("tiger" "is" "young" "+")
If something needs the tiger and the tiger eats the mouse then the mouse sees the tiger.
((("something" "needs" "tiger" "+") ("tiger" "eats" "mouse" "+")) -> ("mouse" "sees" "tiger" "+"))
If something needs the cat and it is not young then it is big.
((("something" "needs" "cat" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
If something is big then it does not see the cow.
((("something" "is" "big" "+")) -> ("something" "sees" "cow" "-"))
If something eats the cat and it is big then it is not rough.
((("something" "eats" "cat" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If something eats the cow and the cow sees the tiger then the tiger is not rough.
((("something" "eats" "cow" "+") ("cow" "sees" "tiger" "+")) -> ("tiger" "is" "rough" "-"))
If the tiger needs the mouse then the tiger sees the mouse.
((("tiger" "needs" "mouse" "+")) -> ("tiger" "sees" "mouse" "+"))
The cow sees the mouse.
True
1
proof
[(triple4)]
("cow" "sees" "mouse" "+")
triple4
The cow is not big.
False
1
inv-proof
[(triple2)]
("cow" "is" "big" "-")
triple2
The cow does not see the cow.
True
2
proof
[(((triple2) -> rule3))]
("cow" "sees" "cow" "-")
((triple2) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cow sees the cow.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "sees" "cow" "+")
((triple2) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "big" "-")
The tiger sees the mouse.
Unknown
rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "mouse" "+")
The mouse does not need the cow.
Unknown
inv-random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The cat sees the mouse.[(triple1)] The cow is big.[(triple2)] The cow is cold.[(triple3)] The cow sees the mouse.[(triple4)] The mouse eats the cat.[(triple5)] The tiger eats the mouse.[(triple6)] The tiger is young.[(triple7)] @1: The cow does not see the cow.[(((triple2) -> rule3))]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple4
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple5
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple6
The tiger is young.
("tiger" "is" "young" "+")
triple7
The cow does not see the cow.
("cow" "sees" "cow" "-")
((triple2) -> (rule3 % int1))
The cow does not see the cow.
("cow" "sees" "cow" "-")
int1