The dog likes the mouse. The mouse likes the dog. If the mouse likes the dog then the dog chases the mouse. If the dog is cold and the dog does not visit the mouse then the dog does not chase the mouse. If something visits the dog and it visits the mouse then the dog chases the mouse. If something is cold then it chases the mouse. If something visits the mouse and it is not cold then it chases the mouse. If something chases the mouse then the mouse visits the dog. If something likes the mouse then the mouse chases the dog. If the dog chases the mouse then the dog likes the mouse.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
If the mouse likes the dog then the dog chases the mouse.
((("mouse" "likes" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If the dog is cold and the dog does not visit the mouse then the dog does not chase the mouse.
((("dog" "is" "cold" "+") ("dog" "visits" "mouse" "~")) -> ("dog" "chases" "mouse" "-"))
If something visits the dog and it visits the mouse then the dog chases the mouse.
((("something" "visits" "dog" "+") ("something" "visits" "mouse" "+")) -> ("dog" "chases" "mouse" "+"))
If something is cold then it chases the mouse.
((("something" "is" "cold" "+")) -> ("something" "chases" "mouse" "+"))
If something visits the mouse and it is not cold then it chases the mouse.
((("something" "visits" "mouse" "+") ("something" "is" "cold" "~")) -> ("something" "chases" "mouse" "+"))
If something chases the mouse then the mouse visits the dog.
((("something" "chases" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
If something likes the mouse then the mouse chases the dog.
((("something" "likes" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If the dog chases the mouse then the dog likes the mouse.
((("dog" "chases" "mouse" "+")) -> ("dog" "likes" "mouse" "+"))
The dog likes the mouse.
True
1
proof
[(triple1 OR ((((triple2) -> rule1)) -> rule8))]
("dog" "likes" "mouse" "+")
triple1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse does not like the dog.
False
1
inv-proof
[(triple2)]
("mouse" "likes" "dog" "-")
triple2
The mouse chases the dog.
True
2
proof
[(((triple1) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule7))]
("mouse" "chases" "dog" "+")
((triple1) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The mouse does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule7))]
("mouse" "chases" "dog" "-")
((triple1) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The mouse visits the dog.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("mouse" "visits" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse does not visit the dog.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("mouse" "visits" "dog" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The dog likes the mouse.[(triple1 OR ((((triple2) -> rule1)) -> rule8))] The mouse likes the dog.[(triple2)] @1: The dog chases the mouse.[(((triple2) -> rule1))] The mouse chases the dog.[(((triple1) -> rule7) OR ((((((triple2) -> rule1)) -> rule8)) -> rule7))] @2: The mouse visits the dog.[(((((triple2) -> rule1)) -> rule6))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple2) -> (rule1 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((triple1) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2