Anne is smart. Bob is kind. Charlie is smart. Dave is quiet. If someone is blue then they are quiet. All rough people are green. All nice, rough people are green. If someone is nice then they are rough. If someone is smart then they are kind. All smart people are blue. Rough, green people are kind. All rough, quiet people are nice.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
All nice, rough people are green.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Rough, green people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All rough, quiet people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Dave is quiet.
True
1
proof
[(triple4)]
("Dave" "is" "quiet" "+")
triple4
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is smart.[(triple1)] Bob is kind.[(triple2)] Charlie is smart.[(triple3)] Dave is quiet.[(triple4)] @1: Anne is blue.[(((triple1) -> rule6))] Anne is kind.[(((triple1) -> rule5))] Charlie is blue.[(((triple3) -> rule6))] Charlie is kind.[(((triple3) -> rule5))] @2: Anne is quiet.[(((((triple1) -> rule6)) -> rule1))] Charlie is quiet.[(((((triple3) -> rule6)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2