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