Charlie is smart. Charlie is white. Gary is nice. If something is round then it is nice. All young, rough things are white. Young things are not rough. If Gary is rough and Gary is young then Gary is not round. If Charlie is not nice then Charlie is smart. If something is nice and rough then it is blue. All smart, white things are blue. Rough things are blue.
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All young, rough things are white.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Young things are not rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
If Gary is rough and Gary is young then Gary is not round.
((("Gary" "is" "rough" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "round" "-"))
If Charlie is not nice then Charlie is smart.
((("Charlie" "is" "nice" "~")) -> ("Charlie" "is" "smart" "+"))
If something is nice and rough then it is blue.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All smart, white things are blue.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Charlie is smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Charlie is blue.
True
3
proof
[(((triple1 triple2) -> rule7))]
("Charlie" "is" "blue" "+")
((triple1 triple2) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
3
inv-proof
[(((triple1 triple2) -> rule7))]
("Charlie" "is" "blue" "-")
((triple1 triple2) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is smart.[(triple1)] Charlie is white.[(triple2)] Gary is nice.[(triple3)] @1: Charlie is blue.[(((triple1 triple2) -> rule7))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1 triple2) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1