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