The dog is kind. If something is blue then it is round. Blue, kind things are green. Green, kind things are nice. Kind things are nice. If something is nice and not kind then it is blue. Nice things are blue.
The dog is kind.
("dog" "is" "kind" "+")
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Blue, kind things are green.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Green, kind things are nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not kind then it is blue.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "blue" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "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 nice.
True
2
proof
[(((triple1) -> rule4))]
("dog" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("dog" "is" "nice" "-")
((triple1) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is blue.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("dog" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is not blue.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("dog" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is round.
True
4
proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule1))]
("dog" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog is not green.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule6) triple1) -> rule2))]
("dog" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "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) -> rule4))] @2: The dog is blue.[(((((triple1) -> rule4)) -> rule6))] @3: The dog is green.[(((((((triple1) -> rule4)) -> rule6) triple1) -> rule2))] The dog is round.[(((((((triple1) -> rule4)) -> rule6)) -> rule1))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is green.
("dog" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog is round.
("dog" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3