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