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