Charlie is not big. Charlie is not cold. Charlie is kind. Charlie is nice. Charlie is white. Charlie is young. Harry is big. Harry is not nice. Harry is white. Harry is young. If Charlie is white and Charlie is not kind then Charlie is big. All smart, kind people are cold. If Charlie is kind then Charlie is not smart. If Harry is not smart and Harry is not white then Harry is kind. If someone is nice and not big then they are young. Big, nice people are young.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Charlie is white and Charlie is not kind then Charlie is big.
((("Charlie" "is" "white" "+") ("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "big" "+"))
All smart, kind people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is kind then Charlie is not smart.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "smart" "-"))
If Harry is not smart and Harry is not white then Harry is kind.
((("Harry" "is" "smart" "~") ("Harry" "is" "white" "~")) -> ("Harry" "is" "kind" "+"))
If someone is nice and not big then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "+"))
Big, nice people are young.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Charlie is white.
True
1
proof
[(triple5)]
("Charlie" "is" "white" "+")
triple5
Charlie is big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not smart.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "smart" "-")
((triple3) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is smart.
False
2
inv-proof
[(((triple3) -> rule3))]
("Charlie" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is not big.[(triple1)] Charlie is not cold.[(triple2)] Charlie is white.[(triple5)] Charlie is young.[(triple6 OR ((triple4 triple1) -> rule5))] Harry is big.[(triple7)] Harry is not nice.[(triple8)] Harry is white.[(triple9)] Harry is young.[(triple10)] @1: Charlie is not smart.[(((triple3) -> rule3))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple4 triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is not nice.
("Harry" "is" "nice" "-")
triple8
Harry is white.
("Harry" "is" "white" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is not smart.
("Charlie" "is" "smart" "-")
((triple3) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1