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