The cow eats the mouse. The cow is big. The cow is green. The cow likes the mouse. The cow sees the mouse. The mouse likes the cow. The mouse sees the cow. If something sees the mouse and it eats the mouse then the mouse is kind.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something sees the mouse and it eats the mouse then the mouse is kind.
((("something" "sees" "mouse" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
The cow is big.
True
1
proof
[(triple2)]
("cow" "is" "big" "+")
triple2
The cow does not like the mouse.
False
1
inv-proof
[(triple4)]
("cow" "likes" "mouse" "-")
triple4
The mouse is kind.
True
3
proof
[(((triple5 triple1) -> rule1))]
("mouse" "is" "kind" "+")
((triple5 triple1) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
3
inv-proof
[(((triple5 triple1) -> rule1))]
("mouse" "is" "kind" "-")
((triple5 triple1) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cow eats the mouse.[(triple1)] The cow is big.[(triple2)] The cow is green.[(triple3)] The cow likes the mouse.[(triple4)] The cow sees the mouse.[(triple5)] The mouse likes the cow.[(triple6)] The mouse sees the cow.[(triple7)] @1: The mouse is kind.[(((triple5 triple1) -> rule1))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple5
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
((triple5 triple1) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1