The cat visits the dog. The dog visits the cat. The lion does not visit the dog. The mouse is green. If something visits the lion then the lion chases the mouse. If something visits the cat then the cat visits the mouse. If something visits the dog then it is round. If the lion visits the cat then the lion visits the mouse. If something is round then it does not chase the cat. If something is big then it chases the mouse. If something chases the lion and it sees the dog then the dog is big. If the dog chases the mouse and the dog does not chase the cat then the mouse chases the lion.
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The lion does not visit the dog.
("lion" "visits" "dog" "-")
The mouse is green.
("mouse" "is" "green" "+")
If something visits the lion then the lion chases the mouse.
((("something" "visits" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
If something visits the cat then the cat visits the mouse.
((("something" "visits" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If something visits the dog then it is round.
((("something" "visits" "dog" "+")) -> ("something" "is" "round" "+"))
If the lion visits the cat then the lion visits the mouse.
((("lion" "visits" "cat" "+")) -> ("lion" "visits" "mouse" "+"))
If something is round then it does not chase the cat.
((("something" "is" "round" "+")) -> ("something" "chases" "cat" "-"))
If something is big then it chases the mouse.
((("something" "is" "big" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the lion and it sees the dog then the dog is big.
((("something" "chases" "lion" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "big" "+"))
If the dog chases the mouse and the dog does not chase the cat then the mouse chases the lion.
((("dog" "chases" "mouse" "+") ("dog" "chases" "cat" "~")) -> ("mouse" "chases" "lion" "+"))
The dog visits the cat.
True
1
proof
[(triple2)]
("dog" "visits" "cat" "+")
triple2
The cat does not visit the dog.
False
1
inv-proof
[(triple1)]
("cat" "visits" "dog" "-")
triple1
The cat visits the mouse.
True
2
proof
[(((triple2) -> rule2))]
("cat" "visits" "mouse" "+")
((triple2) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat does not visit the mouse.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "visits" "mouse" "-")
((triple2) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat does not chase the cat.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("cat" "chases" "cat" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat chases the cat.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("cat" "chases" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not chase the mouse.
Unknown
inv-rconc
[@1: The cat chases the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "mouse" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "round" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "round" "-")
The mouse visits the dog.
Unknown
random
[@0: The mouse visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "dog" "+")
The lion does not chase the dog.
Unknown
inv-random
[@0: The lion chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "dog" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
@0: The cat visits the dog.[(triple1)] The dog visits the cat.[(triple2)] The lion does not visit the dog.[(triple3)] The mouse is green.[(triple4)] @1: The cat is round.[(((triple1) -> rule3))] The cat visits the mouse.[(((triple2) -> rule2))] @2: The cat does not chase the cat.[(((((triple1) -> rule3)) -> rule5))]
The cat visits the dog.
("cat" "visits" "dog" "+")
triple1
The dog visits the cat.
("dog" "visits" "cat" "+")
triple2
The lion does not visit the dog.
("lion" "visits" "dog" "-")
triple3
The mouse is green.
("mouse" "is" "green" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple2) -> (rule2 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The cat does not chase the cat.
("cat" "chases" "cat" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The cat is round.
("cat" "is" "round" "+")
int2