The cat is young. The cow sees the squirrel. The mouse sees the cow. The squirrel likes the cow. If the mouse sees the cow then the mouse is young. If the cat is nice then the cat sees the cow. If something is young then it does not like the cow.
The cat is young.
("cat" "is" "young" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
If the mouse sees the cow then the mouse is young.
((("mouse" "sees" "cow" "+")) -> ("mouse" "is" "young" "+"))
If the cat is nice then the cat sees the cow.
((("cat" "is" "nice" "+")) -> ("cat" "sees" "cow" "+"))
If something is young then it does not like the cow.
((("something" "is" "young" "+")) -> ("something" "likes" "cow" "-"))
The mouse sees the cow.
True
1
proof
[(triple3)]
("mouse" "sees" "cow" "+")
triple3
The cow does not see the squirrel.
False
1
inv-proof
[(triple2)]
("cow" "sees" "squirrel" "-")
triple2
The mouse is young.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "is" "young" "+")
((triple3) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The cat likes the cow.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "likes" "cow" "+")
((triple1) -> (rule3 % int1))
The cat does not like the cow.
("cat" "likes" "cow" "-")
int1
The mouse does not like the cow.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("mouse" "likes" "cow" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse likes the cow.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("mouse" "likes" "cow" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cat does not see the cow.
Unknown
inv-rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cow" "-")
The mouse sees the squirrel.
Unknown
random
[@0: The mouse sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "squirrel" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The squirrel sees the cat.
Unknown
random
[@0: The squirrel sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cat" "+")
@0: The cat is young.[(triple1)] The cow sees the squirrel.[(triple2)] The mouse sees the cow.[(triple3)] The squirrel likes the cow.[(triple4)] @1: The cat does not like the cow.[(((triple1) -> rule3))] The mouse is young.[(((triple3) -> rule1))] @2: The mouse does not like the cow.[(((((triple3) -> rule1)) -> rule3))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple3
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple4
The cat does not like the cow.
("cat" "likes" "cow" "-")
((triple1) -> (rule3 % int1))
The cat does not like the cow.
("cat" "likes" "cow" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple3) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse does not like the cow.
("mouse" "likes" "cow" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2