Charlie is big. Dave is big. Gary is young. If Dave is round then Dave is young. All young people are white. White people are not nice. All big, white people are kind. If someone is round and not young then they are big. All round people are not big.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is round then Dave is young.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "young" "+"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
White people are not nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "-"))
All big, white people are kind.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If someone is round and not young then they are big.
((("someone" "is" "round" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "big" "+"))
All round people are not big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "-"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Gary is white.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "white" "+")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "white" "-")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not nice.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "nice" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "+")
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is big.[(triple1)] Dave is big.[(triple2)] Gary is young.[(triple3)] @1: Gary is white.[(((triple3) -> rule2))] @2: Gary is not nice.[(((((triple3) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2