Anne is kind. Charlie is big. Charlie is round. Charlie is smart. Gary is blue. Gary is kind. Gary is round. Gary is smart. Harry is big. Harry is blue. If Harry is blue and Harry is kind then Harry is smart. All big, kind people are blue. If someone is white then they are smart. If someone is kind then they are smart. If Harry is smart and Harry is kind then Harry is white. Kind people are blue. Green people are round. If someone is round then they are green.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Harry is blue and Harry is kind then Harry is smart.
((("Harry" "is" "blue" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "smart" "+"))
All big, kind people are blue.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Harry is smart and Harry is kind then Harry is white.
((("Harry" "is" "smart" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Charlie is smart.
True
1
proof
[(triple4)]
("Charlie" "is" "smart" "+")
triple4
Charlie is not big.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "big" "-")
triple2
Anne is blue.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is smart.
Unknown
rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Harry" "is" "smart" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is kind.[(triple1)] Charlie is big.[(triple2)] Charlie is round.[(triple3)] Charlie is smart.[(triple4)] Gary is blue.[(triple5 OR ((triple6) -> rule6))] Gary is kind.[(triple6)] Gary is round.[(triple7)] Gary is smart.[(triple8 OR ((triple6) -> rule4))] Harry is big.[(triple9)] Harry is blue.[(triple10)] @1: Anne is blue.[(((triple1) -> rule6))] Anne is smart.[(((triple1) -> rule4))] Charlie is green.[(((triple3) -> rule8))] Gary is green.[(((triple7) -> rule8))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
((triple6) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
triple8
((triple6) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple3) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1