The cat chases the dog. The cat likes the mouse. The cat sees the mouse. The cow chases the mouse. The cow sees the mouse. The dog chases the cat. The mouse chases the cow. If something is young and it does not like the mouse then the mouse does not like the dog. If the dog sees the mouse then the mouse is not round. If the dog is not rough then the dog does not chase the cow. If something likes the cow then it is young. If something chases the cat then the cat likes the cow. If something sees the cow and it likes the mouse then the mouse chases the cow. If something likes the mouse and it is young then the mouse sees the cat. If the cat likes the mouse then the cat is rough.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
If something is young and it does not like the mouse then the mouse does not like the dog.
((("something" "is" "young" "+") ("something" "likes" "mouse" "~")) -> ("mouse" "likes" "dog" "-"))
If the dog sees the mouse then the mouse is not round.
((("dog" "sees" "mouse" "+")) -> ("mouse" "is" "round" "-"))
If the dog is not rough then the dog does not chase the cow.
((("dog" "is" "rough" "~")) -> ("dog" "chases" "cow" "-"))
If something likes the cow then it is young.
((("something" "likes" "cow" "+")) -> ("something" "is" "young" "+"))
If something chases the cat then the cat likes the cow.
((("something" "chases" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If something sees the cow and it likes the mouse then the mouse chases the cow.
((("something" "sees" "cow" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "chases" "cow" "+"))
If something likes the mouse and it is young then the mouse sees the cat.
((("something" "likes" "mouse" "+") ("something" "is" "young" "+")) -> ("mouse" "sees" "cat" "+"))
If the cat likes the mouse then the cat is rough.
((("cat" "likes" "mouse" "+")) -> ("cat" "is" "rough" "+"))
The cow sees the mouse.
True
1
proof
[(triple5)]
("cow" "sees" "mouse" "+")
triple5
The cat does not chase the dog.
False
1
inv-proof
[(triple1)]
("cat" "chases" "dog" "-")
triple1
The cat is rough.
True
2
proof
[(((triple2) -> rule8))]
("cat" "is" "rough" "+")
((triple2) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat does not like the cow.
False
2
inv-proof
[(((triple6) -> rule5))]
("cat" "likes" "cow" "-")
((triple6) -> (rule5 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat is young.
True
3
proof
[(((((triple6) -> rule5)) -> rule4))]
("cat" "is" "young" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat is not young.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule4))]
("cat" "is" "young" "-")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The mouse sees the cat.
True
5
proof
[(((triple2 ((((triple6) -> rule5)) -> rule4)) -> rule7))]
("mouse" "sees" "cat" "+")
((triple2 ((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The mouse does not see the cat.
False
5
inv-proof
[(((triple2 ((((triple6) -> rule5)) -> rule4)) -> rule7))]
("mouse" "sees" "cat" "-")
((triple2 ((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "young" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "young" "+")
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "young" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
The mouse does not see the cow.
Unknown
inv-random
[@0: The mouse sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cow" "-")
The dog sees the cat.
Unknown
random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "+")
The dog does not chase the cow.
Unknown
inv-random
[@0: The dog chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cow" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The cat chases the dog.[(triple1)] The cat likes the mouse.[(triple2)] The cat sees the mouse.[(triple3)] The cow chases the mouse.[(triple4)] The cow sees the mouse.[(triple5)] The dog chases the cat.[(triple6)] The mouse chases the cow.[(triple7)] @1: The cat is rough.[(((triple2) -> rule8))] The cat likes the cow.[(((triple6) -> rule5))] @2: The cat is young.[(((((triple6) -> rule5)) -> rule4))] @3: The mouse sees the cat.[(((triple2 ((((triple6) -> rule5)) -> rule4)) -> rule7))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple3
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple5
The dog chases the cat.
("dog" "chases" "cat" "+")
triple6
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple7
The cat is rough.
("cat" "is" "rough" "+")
((triple2) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple6) -> (rule5 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple2 ((((triple6) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3