The cat is young. The dog chases the cat. The dog is blue. The mouse chases the dog. The mouse is not big. The tiger is blue. The tiger does not visit the cat. If something sees the cat then it chases the cat. If something is green and not young then it visits the tiger. If something is blue and it chases the tiger then the tiger sees the mouse. If something chases the cat then it visits the dog. If something visits the dog then it chases the tiger. If something is green and it does not visit the dog then it is not big.
The cat is young.
("cat" "is" "young" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is blue.
("dog" "is" "blue" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
If something sees the cat then it chases the cat.
((("something" "sees" "cat" "+")) -> ("something" "chases" "cat" "+"))
If something is green and not young then it visits the tiger.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "visits" "tiger" "+"))
If something is blue and it chases the tiger then the tiger sees the mouse.
((("something" "is" "blue" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If something chases the cat then it visits the dog.
((("something" "chases" "cat" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then it chases the tiger.
((("something" "visits" "dog" "+")) -> ("something" "chases" "tiger" "+"))
If something is green and it does not visit the dog then it is not big.
((("something" "is" "green" "+") ("something" "visits" "dog" "~")) -> ("something" "is" "big" "-"))
The cat is young.
True
1
proof
[(triple1)]
("cat" "is" "young" "+")
triple1
The dog does not chase the cat.
False
1
inv-proof
[(triple2)]
("dog" "chases" "cat" "-")
triple2
The dog visits the dog.
True
2
proof
[(((triple2) -> rule4))]
("dog" "visits" "dog" "+")
((triple2) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "visits" "dog" "-")
((triple2) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the tiger.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("dog" "chases" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog does not chase the tiger.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("dog" "chases" "tiger" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The tiger sees the mouse.
True
5
proof
[(((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule3))]
("tiger" "sees" "mouse" "+")
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The tiger does not see the mouse.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule3))]
("tiger" "sees" "mouse" "-")
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "tiger" "-")
The tiger chases the cat.
Unknown
rconc
[@1: The tiger chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "cat" "+")
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "tiger" "-")
The mouse chases the tiger.
Unknown
rconc
[@3: The mouse chases the tiger.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- FAIL)]]
("mouse" "chases" "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 dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The tiger chases the mouse.
Unknown
random
[@0: The tiger chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "mouse" "+")
@0: The cat is young.[(triple1)] The dog chases the cat.[(triple2)] The dog is blue.[(triple3)] The mouse chases the dog.[(triple4)] The mouse is not big.[(triple5)] The tiger does not visit the cat.[(triple7)] The tiger is blue.[(triple6)] @1: The dog visits the dog.[(((triple2) -> rule4))] @2: The dog chases the tiger.[(((((triple2) -> rule4)) -> rule5))] @3: The tiger sees the mouse.[(((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule3))]
The cat is young.
("cat" "is" "young" "+")
triple1
The dog chases the cat.
("dog" "chases" "cat" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple4
The mouse is not big.
("mouse" "is" "big" "-")
triple5
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple2) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3