The cat is young. The dog does not visit the mouse. The lion is big. The mouse is round. If someone chases the dog then they do not chase the mouse. If the dog does not visit the lion then the dog visits the cat. If the dog does not visit the mouse then the mouse does not chase the lion. If someone chases the lion then they are not rough. If the cat chases the mouse and the mouse chases the lion then the mouse chases the dog. If someone likes the lion and the lion chases the dog then the dog is not round. If someone is round and they do not chase the lion then the lion does not chase the mouse. If the lion does not chase the mouse then the lion visits the mouse.
The cat is young.
("cat" "is" "young" "+")
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
The lion is big.
("lion" "is" "big" "+")
The mouse is round.
("mouse" "is" "round" "+")
If someone chases the dog then they do not chase the mouse.
((("someone" "chases" "dog" "+")) -> ("someone" "chases" "mouse" "-"))
If the dog does not visit the lion then the dog visits the cat.
((("dog" "visits" "lion" "~")) -> ("dog" "visits" "cat" "+"))
If the dog does not visit the mouse then the mouse does not chase the lion.
((("dog" "visits" "mouse" "~")) -> ("mouse" "chases" "lion" "-"))
If someone chases the lion then they are not rough.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "rough" "-"))
If the cat chases the mouse and the mouse chases the lion then the mouse chases the dog.
((("cat" "chases" "mouse" "+") ("mouse" "chases" "lion" "+")) -> ("mouse" "chases" "dog" "+"))
If someone likes the lion and the lion chases the dog then the dog is not round.
((("someone" "likes" "lion" "+") ("lion" "chases" "dog" "+")) -> ("dog" "is" "round" "-"))
If someone is round and they do not chase the lion then the lion does not chase the mouse.
((("someone" "is" "round" "+") ("someone" "chases" "lion" "~")) -> ("lion" "chases" "mouse" "-"))
If the lion does not chase the mouse then the lion visits the mouse.
((("lion" "chases" "mouse" "~")) -> ("lion" "visits" "mouse" "+"))
The dog does not visit the mouse.
True
1
proof
[(triple2)]
("dog" "visits" "mouse" "-")
triple2
The dog visits the mouse.
False
1
inv-proof
[(triple2)]
("dog" "visits" "mouse" "+")
triple2
The mouse does not chase the lion.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "chases" "lion" "-")
((triple2) -> (rule3 % int1))
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int1
The mouse chases the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "chases" "lion" "+")
((triple2) -> (rule3 % int1))
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int1
The lion does not chase the mouse.
True
4
proof
[(((triple4 ((triple2) -> rule3)) -> rule7))]
("lion" "chases" "mouse" "-")
((triple4 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int2
The lion chases the mouse.
False
4
inv-proof
[(((triple4 ((triple2) -> rule3)) -> rule7))]
("lion" "chases" "mouse" "+")
((triple4 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int2
The lion visits the mouse.
True
5
proof
[(((((triple4 ((triple2) -> rule3)) -> rule7)) -> rule8))]
("lion" "visits" "mouse" "+")
((((triple4 ((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int2
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int3
The lion does not visit the mouse.
False
5
inv-proof
[(((((triple4 ((triple2) -> rule3)) -> rule7)) -> rule8))]
("lion" "visits" "mouse" "-")
((((triple4 ((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int2
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int3
The dog does not visit the cat.
Unknown
inv-rconc
[@1: The dog visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "cat" "-")
The mouse chases the dog.
Unknown
rconc
[@1: The mouse chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "dog" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion visits the dog.
Unknown
random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "+")
The cat does not chase the dog.
Unknown
inv-random
[@0: The cat chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "dog" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The cat is young.[(triple1)] The dog does not visit the mouse.[(triple2)] The lion is big.[(triple3)] The mouse is round.[(triple4)] @1: The mouse does not chase the lion.[(((triple2) -> rule3))] @2: The lion does not chase the mouse.[(((triple4 ((triple2) -> rule3)) -> rule7))] @3: The lion visits the mouse.[(((((triple4 ((triple2) -> rule3)) -> rule7)) -> rule8))]
The cat is young.
("cat" "is" "young" "+")
triple1
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
((triple2) -> (rule3 % int1))
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int1
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
((triple4 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int1
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((((triple4 ((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
int2
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int3