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