The cow is blue. The cow likes the dog. The dog chases the cow. The dog chases the mouse. The dog is big. The dog is kind. The dog likes the cow. The mouse chases the cow. The mouse chases the dog. The mouse is blue. The mouse does not like the dog. The mouse sees the cow. If something likes the dog and the dog is not kind then the dog is young. If the dog is kind and the dog sees the mouse then the mouse chases the cow. All kind things are big. If something is green and it chases the cow then the cow does not chase the mouse. If something likes the mouse then the mouse is big. If something chases the mouse and the mouse chases the cow then the mouse is kind.
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something likes the dog and the dog is not kind then the dog is young.
((("something" "likes" "dog" "+") ("dog" "is" "kind" "~")) -> ("dog" "is" "young" "+"))
If the dog is kind and the dog sees the mouse then the mouse chases the cow.
((("dog" "is" "kind" "+") ("dog" "sees" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is green and it chases the cow then the cow does not chase the mouse.
((("something" "is" "green" "+") ("something" "chases" "cow" "+")) -> ("cow" "chases" "mouse" "-"))
If something likes the mouse then the mouse is big.
((("something" "likes" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something chases the mouse and the mouse chases the cow then the mouse is kind.
((("something" "chases" "mouse" "+") ("mouse" "chases" "cow" "+")) -> ("mouse" "is" "kind" "+"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The mouse is not blue.
False
1
inv-proof
[(triple10)]
("mouse" "is" "blue" "-")
triple10
The mouse is kind.
True
3
proof
[(((triple4 triple8) -> rule6))]
("mouse" "is" "kind" "+")
((triple4 triple8) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
3
inv-proof
[(((triple4 triple8) -> rule6))]
("mouse" "is" "kind" "-")
((triple4 triple8) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is big.
True
4
proof
[(((((triple4 triple8) -> rule6)) -> rule3))]
("mouse" "is" "big" "+")
((((triple4 triple8) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is not big.
False
4
inv-proof
[(((((triple4 triple8) -> rule6)) -> rule3))]
("mouse" "is" "big" "-")
((((triple4 triple8) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "young" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "big" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The cow chases the dog.
Unknown
random
[@0: The cow chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "dog" "+")
@0: The cow is blue.[(triple1)] The cow likes the dog.[(triple2)] The dog chases the cow.[(triple3)] The dog chases the mouse.[(triple4)] The dog is big.[(triple5 OR ((triple6) -> rule3))] The dog is kind.[(triple6)] The dog likes the cow.[(triple7)] The mouse chases the cow.[(triple8)] The mouse chases the dog.[(triple9)] The mouse does not like the dog.[(triple11)] The mouse is blue.[(triple10)] The mouse sees the cow.[(triple12)] @1: The mouse is kind.[(((triple4 triple8) -> rule6))] @2: The mouse is big.[(((((triple4 triple8) -> rule6)) -> rule3))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple2
The dog chases the cow.
("dog" "chases" "cow" "+")
triple3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
((triple6) -> (rule3 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
triple6
The dog likes the cow.
("dog" "likes" "cow" "+")
triple7
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple8
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple9
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
triple11
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple12
The mouse is kind.
("mouse" "is" "kind" "+")
((triple4 triple8) -> (rule6 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((((triple4 triple8) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2