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