The cat is red. The dog is not red. The mouse is blue. If something sees the dog then the dog eats the cat. If something eats the mouse and it does not see the cat then the mouse is red. If something is young then it does not see the dog. If something sees the cat then the cat is young. If something eats the mouse then the mouse is young. If something is blue then it eats the mouse.
The cat is red.
("cat" "is" "red" "+")
The dog is not red.
("dog" "is" "red" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
If something sees the dog then the dog eats the cat.
((("something" "sees" "dog" "+")) -> ("dog" "eats" "cat" "+"))
If something eats the mouse and it does not see the cat then the mouse is red.
((("something" "eats" "mouse" "+") ("something" "sees" "cat" "~")) -> ("mouse" "is" "red" "+"))
If something is young then it does not see the dog.
((("something" "is" "young" "+")) -> ("something" "sees" "dog" "-"))
If something sees the cat then the cat is young.
((("something" "sees" "cat" "+")) -> ("cat" "is" "young" "+"))
If something eats the mouse then the mouse is young.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something is blue then it eats the mouse.
((("something" "is" "blue" "+")) -> ("something" "eats" "mouse" "+"))
The mouse is blue.
True
1
proof
[(triple3)]
("mouse" "is" "blue" "+")
triple3
The mouse is not blue.
False
1
inv-proof
[(triple3)]
("mouse" "is" "blue" "-")
triple3
The mouse eats the mouse.
True
2
proof
[(((triple3) -> rule6))]
("mouse" "eats" "mouse" "+")
((triple3) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse does not eat the mouse.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "eats" "mouse" "-")
((triple3) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is young.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("mouse" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse is not young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("mouse" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse does not see the dog.
True
4
proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule3))]
("mouse" "sees" "dog" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The mouse sees the dog.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule3))]
("mouse" "sees" "dog" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3
The dog does not eat the cat.
Unknown
inv-rconc
[@1: The dog eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "cat" "-")
The dog eats the mouse.
Unknown
rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "mouse" "+")
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "young" "-")
The mouse is red.
Unknown
rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "red" "+")
The cat does not like the mouse.
Unknown
inv-random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The mouse does not eat the cat.
Unknown
inv-random
[@0: The mouse eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "cat" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The cat is red.[(triple1)] The dog is not red.[(triple2)] The mouse is blue.[(triple3)] @1: The mouse eats the mouse.[(((triple3) -> rule6))] @2: The mouse is young.[(((((triple3) -> rule6)) -> rule5))] @3: The mouse does not see the dog.[(((((((triple3) -> rule6)) -> rule5)) -> rule3))]
The cat is red.
("cat" "is" "red" "+")
triple1
The dog is not red.
("dog" "is" "red" "-")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple3) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int3