Charlie is white. Blue things are not green. Round things are not green. All young things are blue. White things are young. If something is green and not kind then it is not young. All green, kind things are not white. If Charlie is blue and Charlie is young then Charlie is white. If something is blue and white then it is quiet.
Charlie is white.
("Charlie" "is" "white" "+")
Blue things are not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
Round things are not green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "-"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is green and not kind then it is not young.
((("something" "is" "green" "+") ("something" "is" "kind" "~")) -> ("something" "is" "young" "-"))
All green, kind things are not white.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "-"))
If Charlie is blue and Charlie is young then Charlie is white.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "white" "+"))
If something is blue and white then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Charlie is not white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Charlie is young.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "young" "+")
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "young" "-")
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Charlie" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not green.
True
4
proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule1))]
("Charlie" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not quiet.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule3) triple1) -> rule8))]
("Charlie" "is" "quiet" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is white.[(triple1)] @1: Charlie is young.[(((triple1) -> rule4))] @2: Charlie is blue.[(((((triple1) -> rule4)) -> rule3))] @3: Charlie is not green.[(((((((triple1) -> rule4)) -> rule3)) -> rule1))] Charlie is quiet.[(((((((triple1) -> rule4)) -> rule3) triple1) -> rule8))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not green.
("Charlie" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3