The dog chases the mouse. The dog is blue. The dog is kind. The dog visits the mouse. The mouse chases the dog. The mouse is blue. The mouse visits the dog. If something visits the dog then it sees the dog. If something sees the dog then it is kind.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something visits the dog then it sees the dog.
((("something" "visits" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something sees the dog then it is kind.
((("something" "sees" "dog" "+")) -> ("something" "is" "kind" "+"))
The dog is kind.
True
1
proof
[(triple3)]
("dog" "is" "kind" "+")
triple3
The mouse does not visit the dog.
False
1
inv-proof
[(triple7)]
("mouse" "visits" "dog" "-")
triple7
The mouse sees the dog.
True
2
proof
[(((triple7) -> rule1))]
("mouse" "sees" "dog" "+")
((triple7) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse does not see the dog.
False
2
inv-proof
[(((triple7) -> rule1))]
("mouse" "sees" "dog" "-")
((triple7) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse is kind.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("mouse" "is" "kind" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse is not kind.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("mouse" "is" "kind" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog chases the mouse.[(triple1)] The dog is blue.[(triple2)] The dog is kind.[(triple3)] The dog visits the mouse.[(triple4)] The mouse chases the dog.[(triple5)] The mouse is blue.[(triple6)] The mouse visits the dog.[(triple7)] @1: The mouse sees the dog.[(((triple7) -> rule1))] @2: The mouse is kind.[(((((triple7) -> rule1)) -> rule2))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple7) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2