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