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