The dog chases the mouse. The dog visits the mouse. The dog visits the tiger. The mouse chases the dog. The mouse visits the dog. The tiger chases the dog. The tiger chases the mouse. The tiger is green. The tiger is rough. The tiger is round. The tiger needs the mouse. The tiger visits the dog. If the mouse visits the tiger and the tiger is green then the mouse chases the dog. If something chases the dog and the dog needs the tiger then the tiger needs the mouse. If something needs the dog and it needs the mouse then it chases the mouse. If something visits the dog then it chases the dog. If something visits the mouse then the mouse needs the tiger. If something visits the mouse then the mouse needs the tiger.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If the mouse visits the tiger and the tiger is green then the mouse chases the dog.
((("mouse" "visits" "tiger" "+") ("tiger" "is" "green" "+")) -> ("mouse" "chases" "dog" "+"))
If something chases the dog and the dog needs the tiger then the tiger needs the mouse.
((("something" "chases" "dog" "+") ("dog" "needs" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
If something needs the dog and it needs the mouse then it chases the mouse.
((("something" "needs" "dog" "+") ("something" "needs" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something visits the dog then it chases the dog.
((("something" "visits" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something visits the mouse then the mouse needs the tiger.
((("something" "visits" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If something visits the mouse then the mouse needs the tiger.
((("something" "visits" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
The tiger chases the mouse.
True
1
proof
[(triple7)]
("tiger" "chases" "mouse" "+")
triple7
The dog does not visit the tiger.
False
1
inv-proof
[(triple3)]
("dog" "visits" "tiger" "-")
triple3
The mouse needs the tiger.
True
2
proof
[(((triple2) -> rule5) OR ((triple2) -> rule6))]
("mouse" "needs" "tiger" "+")
((triple2) -> (rule5 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
((triple2) -> (rule6 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse does not need the tiger.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple2) -> rule6))]
("mouse" "needs" "tiger" "-")
((triple2) -> (rule5 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
((triple2) -> (rule6 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "chases" "dog" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The dog chases the mouse.[(triple1)] The dog visits the mouse.[(triple2)] The dog visits the tiger.[(triple3)] The mouse chases the dog.[(triple4 OR ((triple5) -> rule4))] The mouse visits the dog.[(triple5)] The tiger chases the dog.[(triple6 OR ((triple12) -> rule4))] The tiger chases the mouse.[(triple7)] The tiger is green.[(triple8)] The tiger is rough.[(triple9)] The tiger is round.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger visits the dog.[(triple12)] @1: The mouse needs the tiger.[(((triple2) -> rule5) OR ((triple2) -> rule6))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple4
((triple5) -> (rule4 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple5
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple6
((triple12) -> (rule4 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple2) -> (rule5 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
((triple2) -> (rule6 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1