The dog is not green. The dog is round. The dog needs the mouse. The mouse eats the dog. The mouse is nice. The mouse is rough. The mouse sees the dog. If something needs the dog then the dog eats the mouse. If something is round and it sees the mouse then it needs the dog. If something needs the mouse and the mouse sees the dog then the dog sees the mouse.
The dog is not green.
("dog" "is" "green" "-")
The dog is round.
("dog" "is" "round" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something needs the dog then the dog eats the mouse.
((("something" "needs" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If something is round and it sees the mouse then it needs the dog.
((("something" "is" "round" "+") ("something" "sees" "mouse" "+")) -> ("something" "needs" "dog" "+"))
If something needs the mouse and the mouse sees the dog then the dog sees the mouse.
((("something" "needs" "mouse" "+") ("mouse" "sees" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
The mouse sees the dog.
True
1
proof
[(triple7)]
("mouse" "sees" "dog" "+")
triple7
The mouse does not see the dog.
False
1
inv-proof
[(triple7)]
("mouse" "sees" "dog" "-")
triple7
The dog sees the mouse.
True
3
proof
[(((triple3 triple7) -> rule3))]
("dog" "sees" "mouse" "+")
((triple3 triple7) -> (rule3 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog does not see the mouse.
False
3
inv-proof
[(((triple3 triple7) -> rule3))]
("dog" "sees" "mouse" "-")
((triple3 triple7) -> (rule3 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the dog.
True
5
proof
[(((triple2 ((triple3 triple7) -> rule3)) -> rule2))]
("dog" "needs" "dog" "+")
((triple2 ((triple3 triple7) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog does not need the dog.
False
5
inv-proof
[(((triple2 ((triple3 triple7) -> rule3)) -> rule2))]
("dog" "needs" "dog" "-")
((triple2 ((triple3 triple7) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog eats the mouse.
True
6
proof
[(((((triple2 ((triple3 triple7) -> rule3)) -> rule2)) -> rule1))]
("dog" "eats" "mouse" "+")
((((triple2 ((triple3 triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The dog does not eat the mouse.
False
6
inv-proof
[(((((triple2 ((triple3 triple7) -> rule3)) -> rule2)) -> rule1))]
("dog" "eats" "mouse" "-")
((((triple2 ((triple3 triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The mouse does not need the dog.
Unknown
inv-rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "dog" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The dog is not green.[(triple1)] The dog is round.[(triple2)] The dog needs the mouse.[(triple3)] The mouse eats the dog.[(triple4)] The mouse is nice.[(triple5)] The mouse is rough.[(triple6)] The mouse sees the dog.[(triple7)] @1: The dog sees the mouse.[(((triple3 triple7) -> rule3))] @2: The dog needs the dog.[(((triple2 ((triple3 triple7) -> rule3)) -> rule2))] @3: The dog eats the mouse.[(((((triple2 ((triple3 triple7) -> rule3)) -> rule2)) -> rule1))]
The dog is not green.
("dog" "is" "green" "-")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple7
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((triple3 triple7) -> (rule3 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple2 ((triple3 triple7) -> (rule3 % int2))) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((((triple2 ((triple3 triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3