The cat is not big. The cat sees the tiger. The dog is not big. The dog does not see the tiger. The mouse likes the dog. The mouse visits the tiger. The tiger is green. If someone is red then they are green. If someone visits the dog then they like the dog. If someone likes the dog then they see the mouse. If someone visits the cat and they do not like the cat then they see the tiger. If someone visits the tiger then the tiger visits the dog. If someone is big and they like the tiger then the tiger visits the mouse. If someone sees the dog and the dog sees the cat then they like the mouse. If the cat visits the mouse and the cat does not like the dog then the cat likes the mouse.
The cat is not big.
("cat" "is" "big" "-")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The dog is not big.
("dog" "is" "big" "-")
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone visits the dog then they like the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "likes" "dog" "+"))
If someone likes the dog then they see the mouse.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "mouse" "+"))
If someone visits the cat and they do not like the cat then they see the tiger.
((("someone" "visits" "cat" "+") ("someone" "likes" "cat" "~")) -> ("someone" "sees" "tiger" "+"))
If someone visits the tiger then the tiger visits the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If someone is big and they like the tiger then the tiger visits the mouse.
((("someone" "is" "big" "+") ("someone" "likes" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone sees the dog and the dog sees the cat then they like the mouse.
((("someone" "sees" "dog" "+") ("dog" "sees" "cat" "+")) -> ("someone" "likes" "mouse" "+"))
If the cat visits the mouse and the cat does not like the dog then the cat likes the mouse.
((("cat" "visits" "mouse" "+") ("cat" "likes" "dog" "~")) -> ("cat" "likes" "mouse" "+"))
The mouse visits the tiger.
True
1
proof
[(triple6)]
("mouse" "visits" "tiger" "+")
triple6
The cat is big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The tiger visits the dog.
True
2
proof
[(((triple6) -> rule5))]
("tiger" "visits" "dog" "+")
((triple6) -> (rule5 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple5) -> rule3))]
("mouse" "sees" "mouse" "-")
((triple5) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The tiger likes the dog.
True
3
proof
[(((((triple6) -> rule5)) -> rule2))]
("tiger" "likes" "dog" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger does not like the dog.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule2))]
("tiger" "likes" "dog" "-")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger sees the mouse.
True
4
proof
[(((((((triple6) -> rule5)) -> rule2)) -> rule3))]
("tiger" "sees" "mouse" "+")
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The tiger does not see the mouse.
False
4
inv-proof
[(((((((triple6) -> rule5)) -> rule2)) -> rule3))]
("tiger" "sees" "mouse" "-")
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3
The cat does not see the mouse.
Unknown
inv-rconc
[@2: The cat sees the mouse.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cat" "sees" "mouse" "-")
The cat is green.
Unknown
rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "green" "+")
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The cat likes the dog.
Unknown
rconc
[@1: The cat likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "dog" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat likes the tiger.
Unknown
random
[@0: The cat likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "tiger" "+")
The mouse does not visit the cat.
Unknown
inv-random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The cat is not big.[(triple1)] The cat sees the tiger.[(triple2)] The dog does not see the tiger.[(triple4)] The dog is not big.[(triple3)] The mouse likes the dog.[(triple5)] The mouse visits the tiger.[(triple6)] The tiger is green.[(triple7)] @1: The mouse sees the mouse.[(((triple5) -> rule3))] The tiger visits the dog.[(((triple6) -> rule5))] @2: The tiger likes the dog.[(((((triple6) -> rule5)) -> rule2))] @3: The tiger sees the mouse.[(((((((triple6) -> rule5)) -> rule2)) -> rule3))]
The cat is not big.
("cat" "is" "big" "-")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
triple4
The dog is not big.
("dog" "is" "big" "-")
triple3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple5
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple5) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple6) -> (rule5 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((((triple6) -> (rule5 % int2))) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((((((triple6) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int3