Charlie is round. Dave is big. Gary is white. If Dave is big and Dave is not nice then Dave is white. Young things are not rough. All big, white things are rough. If Charlie is kind then Charlie is young. If something is white then it is not kind. If Gary is white and Gary is not big then Gary is not nice.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is white.
("Gary" "is" "white" "+")
If Dave is big and Dave is not nice then Dave is white.
((("Dave" "is" "big" "+") ("Dave" "is" "nice" "~")) -> ("Dave" "is" "white" "+"))
Young things are not rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
All big, white things are rough.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Charlie is kind then Charlie is young.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "young" "+"))
If something is white then it is not kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
If Gary is white and Gary is not big then Gary is not nice.
((("Gary" "is" "white" "+") ("Gary" "is" "big" "~")) -> ("Gary" "is" "nice" "-"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Gary is not kind.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "kind" "-")
((triple3) -> (rule5 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is kind.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "young" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is round.[(triple1)] Dave is big.[(triple2)] Gary is white.[(triple3)] @1: Gary is not kind.[(((triple3) -> rule5))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Gary is not kind.
("Gary" "is" "kind" "-")
((triple3) -> (rule5 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1