Charlie is white. Gary is quiet. Harry is kind. Big things are kind. White things are smart. If something is white and smart then it is rough.
Charlie is white.
("Charlie" "is" "white" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is white and smart then it is rough.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Charlie is not white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Charlie is smart.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Charlie is white.[(triple1)] Gary is quiet.[(triple2)] Harry is kind.[(triple3)] @1: Charlie is smart.[(((triple1) -> rule2))] @2: Charlie is rough.[(((triple1 ((triple1) -> rule2)) -> rule3))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2