The dog chases the mouse. The dog eats the mouse. The dog is cold. The dog is kind. The dog is red. The dog sees the mouse. The mouse chases the dog. The mouse eats the dog. The mouse is green. The mouse sees the dog. If something is cold and it sees the dog then the dog is kind. If something chases the mouse and it eats the mouse then the mouse chases the dog. If something chases the dog and it eats the dog then it sees the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something is cold and it sees the dog then the dog is kind.
((("something" "is" "cold" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "kind" "+"))
If something chases the mouse and it eats the mouse then the mouse chases the dog.
((("something" "chases" "mouse" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If something chases the dog and it eats the dog then it sees the dog.
((("something" "chases" "dog" "+") ("something" "eats" "dog" "+")) -> ("something" "sees" "dog" "+"))
The mouse sees the dog.
True
1
proof
[(triple10 OR ((triple7 triple8) -> rule3) OR ((((triple1 triple2) -> rule2) triple8) -> rule3))]
("mouse" "sees" "dog" "+")
triple10
((triple7 triple8) -> (rule3 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
((((triple1 triple2) -> (rule2 % int2)) triple8) -> (rule3 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse is not green.
False
1
inv-proof
[(triple9)]
("mouse" "is" "green" "-")
triple9
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "dog" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The dog chases the mouse.[(triple1)] The dog eats the mouse.[(triple2)] The dog is cold.[(triple3)] The dog is kind.[(triple4)] The dog is red.[(triple5)] The dog sees the mouse.[(triple6)] The mouse chases the dog.[(triple7 OR ((triple1 triple2) -> rule2))] The mouse eats the dog.[(triple8)] The mouse is green.[(triple9)] The mouse sees the dog.[(triple10 OR ((triple7 triple8) -> rule3) OR ((((triple1 triple2) -> rule2) triple8) -> rule3))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
triple5
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple6
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple7
((triple1 triple2) -> (rule2 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple8
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple10
((triple7 triple8) -> (rule3 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
((((triple1 triple2) -> (rule2 % int2)) triple8) -> (rule3 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2