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