Charlie is white. All rough, young things are round. If something is furry then it is round. If Charlie is young and Charlie is quiet then Charlie is furry. White, smart things are furry. If something is white then it is quiet. If something is quiet then it is smart.
Charlie is white.
("Charlie" "is" "white" "+")
All rough, young things are round.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Charlie is young and Charlie is quiet then Charlie is furry.
((("Charlie" "is" "young" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "furry" "+"))
White, smart things are furry.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is white then it is quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
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 quiet.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple1) -> rule5)) -> rule6))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Charlie is white.[(triple1)] @1: Charlie is quiet.[(((triple1) -> rule5))] @2: Charlie is smart.[(((((triple1) -> rule5)) -> rule6))] @3: Charlie is furry.[(((triple1 ((((triple1) -> rule5)) -> rule6)) -> rule4))] @4: Charlie is round.[(((((triple1 ((((triple1) -> rule5)) -> rule6)) -> rule4)) -> rule2))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1 ((((triple1) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4