The dog is kind. If something is kind then it is nice. Kind things are not round. If something is nice and not round then it is not green. If the dog is kind then the dog is nice. If the dog is green and the dog is round then the dog is not nice. If the dog is not green then the dog is blue.
The dog is kind.
("dog" "is" "kind" "+")
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Kind things are not round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "-"))
If something is nice and not round then it is not green.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "green" "-"))
If the dog is kind then the dog is nice.
((("dog" "is" "kind" "+")) -> ("dog" "is" "nice" "+"))
If the dog is green and the dog is round then the dog is not nice.
((("dog" "is" "green" "+") ("dog" "is" "round" "+")) -> ("dog" "is" "nice" "-"))
If the dog is not green then the dog is blue.
((("dog" "is" "green" "~")) -> ("dog" "is" "blue" "+"))
The dog is kind.
True
1
proof
[(triple1)]
("dog" "is" "kind" "+")
triple1
The dog is not kind.
False
1
inv-proof
[(triple1)]
("dog" "is" "kind" "-")
triple1
The dog is not round.
True
2
proof
[(((triple1) -> rule2))]
("dog" "is" "round" "-")
((triple1) -> (rule2 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The dog is not nice.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule4))]
("dog" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((triple1) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not green.
True
5
proof
[(((((triple1) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule3))]
("dog" "is" "green" "-")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
The dog is not round.
("dog" "is" "round" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
The dog is not round.
("dog" "is" "round" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog is green.
False
5
inv-proof
[(((((triple1) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule3))]
("dog" "is" "green" "+")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
The dog is not round.
("dog" "is" "round" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
The dog is not round.
("dog" "is" "round" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog is blue.
True
6
proof
[(((((((triple1) -> rule1) ((triple1) -> rule2)) -> rule3)) -> rule6) OR ((((((triple1) -> rule4) ((triple1) -> rule2)) -> rule3)) -> rule6))]
("dog" "is" "blue" "+")
((((((triple1) -> (rule1 % int4)) ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not green.
("dog" "is" "green" "-")
int2
The dog is not round.
("dog" "is" "round" "-")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4
((((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not green.
("dog" "is" "green" "-")
int2
The dog is not round.
("dog" "is" "round" "-")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4
The dog is not blue.
False
6
inv-proof
[(((((((triple1) -> rule1) ((triple1) -> rule2)) -> rule3)) -> rule6) OR ((((((triple1) -> rule4) ((triple1) -> rule2)) -> rule3)) -> rule6))]
("dog" "is" "blue" "-")
((((((triple1) -> (rule1 % int4)) ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not green.
("dog" "is" "green" "-")
int2
The dog is not round.
("dog" "is" "round" "-")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4
((((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not green.
("dog" "is" "green" "-")
int2
The dog is not round.
("dog" "is" "round" "-")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is kind.[(triple1)] @1: The dog is nice.[(((triple1) -> rule1) OR ((triple1) -> rule4))] The dog is not round.[(((triple1) -> rule2))] @2: The dog is not green.[(((((triple1) -> rule1) ((triple1) -> rule2)) -> rule3) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule3))] @3: The dog is blue.[(((((((triple1) -> rule1) ((triple1) -> rule2)) -> rule3)) -> rule6) OR ((((((triple1) -> rule4) ((triple1) -> rule2)) -> rule3)) -> rule6))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((triple1) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not round.
("dog" "is" "round" "-")
((triple1) -> (rule2 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The dog is not green.
("dog" "is" "green" "-")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
The dog is not round.
("dog" "is" "round" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is not green.
("dog" "is" "green" "-")
int1
The dog is not round.
("dog" "is" "round" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
((((((triple1) -> (rule1 % int4)) ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not green.
("dog" "is" "green" "-")
int2
The dog is not round.
("dog" "is" "round" "-")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4
((((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not green.
("dog" "is" "green" "-")
int2
The dog is not round.
("dog" "is" "round" "-")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4