Dave is green. Smart people are blue. Green, nice people are blue. If someone is smart and not young then they are blue. If Dave is green then Dave is big. If Dave is kind then Dave is nice. Big people are kind.
Dave is green.
("Dave" "is" "green" "+")
Smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Green, nice people are blue.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and not young then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "blue" "+"))
If Dave is green then Dave is big.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "big" "+"))
If Dave is kind then Dave is nice.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "nice" "+"))
Big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Dave is not green.
False
1
inv-proof
[(triple1)]
("Dave" "is" "green" "-")
triple1
Dave is big.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "big" "+")
((triple1) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "big" "-")
((triple1) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
True
4
proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule5))]
("Dave" "is" "nice" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not nice.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule6)) -> rule5))]
("Dave" "is" "nice" "-")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is green.[(triple1)] @1: Dave is big.[(((triple1) -> rule4))] @2: Dave is kind.[(((((triple1) -> rule4)) -> rule6))] @3: Dave is nice.[(((((((triple1) -> rule4)) -> rule6)) -> rule5))] @4: Dave is blue.[(((triple1 ((((((triple1) -> rule4)) -> rule6)) -> rule5)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4