Charlie is quiet. If someone is kind then they are green. If Charlie is quiet then Charlie is kind. Quiet, white people are round. All kind people are quiet. If someone is red and round then they are white. All quiet, blue people are green. If someone is green then they are round. If Charlie is blue and Charlie is red then Charlie is quiet.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If Charlie is quiet then Charlie is kind.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "kind" "+"))
Quiet, white people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red and round then they are white.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
All quiet, blue people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If Charlie is blue and Charlie is red then Charlie is quiet.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "quiet" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Charlie" "is" "green" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule7))]
("Charlie" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not round.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule7))]
("Charlie" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is quiet.[(triple1)] @1: Charlie is kind.[(((triple1) -> rule2))] @2: Charlie is green.[(((((triple1) -> rule2)) -> rule1))] @3: Charlie is round.[(((((((triple1) -> rule2)) -> rule1)) -> rule7))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3