The cat eats the mouse. The cat is not round. The cow does not eat the cat. The cow is not kind. The cow is not young. The cow sees the cat. The cow sees the mouse. The mouse eats the cat. The mouse is round. The mouse is young. The mouse likes the cow. The mouse sees the cat. If someone sees the cat then the cat is young. If the cat is young then the cat likes the mouse. If someone sees the mouse and they are round then they eat the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is not round.
("cat" "is" "round" "-")
The cow does not eat the cat.
("cow" "eats" "cat" "-")
The cow is not kind.
("cow" "is" "kind" "-")
The cow is not young.
("cow" "is" "young" "-")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone sees the cat then the cat is young.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "young" "+"))
If the cat is young then the cat likes the mouse.
((("cat" "is" "young" "+")) -> ("cat" "likes" "mouse" "+"))
If someone sees the mouse and they are round then they eat the cat.
((("someone" "sees" "mouse" "+") ("someone" "is" "round" "+")) -> ("someone" "eats" "cat" "+"))
The mouse is young.
True
1
proof
[(triple10)]
("mouse" "is" "young" "+")
triple10
The cat does not eat the mouse.
False
1
inv-proof
[(triple1)]
("cat" "eats" "mouse" "-")
triple1
The cat is young.
True
2
proof
[(((triple12) -> rule1) OR ((triple6) -> rule1))]
("cat" "is" "young" "+")
((triple12) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple6) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not young.
False
2
inv-proof
[(((triple12) -> rule1) OR ((triple6) -> rule1))]
("cat" "is" "young" "-")
((triple12) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple6) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the mouse.
True
3
proof
[(((((triple12) -> rule1)) -> rule2) OR ((((triple6) -> rule1)) -> rule2))]
("cat" "likes" "mouse" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat does not like the mouse.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule2) OR ((((triple6) -> rule1)) -> rule2))]
("cat" "likes" "mouse" "-")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "cat" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The mouse eats the cow.
Unknown
random
[@0: The mouse eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cow" "+")
@0: The cat eats the mouse.[(triple1)] The cat is not round.[(triple2)] The cow does not eat the cat.[(triple3)] The cow is not kind.[(triple4)] The cow is not young.[(triple5)] The cow sees the cat.[(triple6)] The cow sees the mouse.[(triple7)] The mouse eats the cat.[(triple8)] The mouse is round.[(triple9)] The mouse is young.[(triple10)] The mouse likes the cow.[(triple11)] The mouse sees the cat.[(triple12)] @1: The cat is young.[(((triple12) -> rule1) OR ((triple6) -> rule1))] @2: The cat likes the mouse.[(((((triple12) -> rule1)) -> rule2) OR ((((triple6) -> rule1)) -> rule2))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is not round.
("cat" "is" "round" "-")
triple2
The cow does not eat the cat.
("cow" "eats" "cat" "-")
triple3
The cow is not kind.
("cow" "is" "kind" "-")
triple4
The cow is not young.
("cow" "is" "young" "-")
triple5
The cow sees the cat.
("cow" "sees" "cat" "+")
triple6
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple7
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple8
The mouse is round.
("mouse" "is" "round" "+")
triple9
The mouse is young.
("mouse" "is" "young" "+")
triple10
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple11
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple12
The cat is young.
("cat" "is" "young" "+")
((triple12) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple6) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2