Anne is nice. Erin is young. Fiona is white. Gary is blue. If Fiona is kind then Fiona is nice. If something is nice then it is blue. All blue things are white. White, blue things are kind. If something is quiet and not nice then it is not young. If something is white and not kind then it is quiet.
Anne is nice.
("Anne" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If Fiona is kind then Fiona is nice.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "nice" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
White, blue things are kind.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is quiet and not nice then it is not young.
((("something" "is" "quiet" "+") ("something" "is" "nice" "~")) -> ("something" "is" "young" "-"))
If something is white and not kind then it is quiet.
((("something" "is" "white" "+") ("something" "is" "kind" "~")) -> ("something" "is" "quiet" "+"))
Fiona is white.
True
1
proof
[(triple3)]
("Fiona" "is" "white" "+")
triple3
Fiona is not white.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "white" "-")
triple3
Gary is white.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "white" "+")
((triple4) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "white" "-")
((triple4) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "white" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
True
6
proof
[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule4))]
("Anne" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not kind.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule4))]
("Anne" "is" "kind" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "quiet" "-")
Erin is blue.
Unknown
rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "+")
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is nice.
Unknown
rconc
[@3: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "nice" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Erin is young.[(triple2)] Fiona is white.[(triple3)] Gary is blue.[(triple4)] @1: Anne is blue.[(((triple1) -> rule2))] Gary is white.[(((triple4) -> rule3))] @2: Anne is white.[(((((triple1) -> rule2)) -> rule3))] Gary is kind.[(((((triple4) -> rule3) triple4) -> rule4))] @3: Anne is kind.[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple4) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3