Anne is blue. Dave is blue. Dave is kind. Erin is not big. Erin is white. Gary is blue. Gary is quiet. If someone is quiet then they are red. If someone is quiet and not kind then they are not red. If someone is red then they are big.
Anne is blue.
("Anne" "is" "blue" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is white.
("Erin" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is quiet then they are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet and not kind then they are not red.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "red" "-"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Gary is not quiet.
False
1
inv-proof
[(triple7)]
("Gary" "is" "quiet" "-")
triple7
Gary is red.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "red" "+")
((triple7) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple7) -> rule1))]
("Gary" "is" "red" "-")
((triple7) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
True
3
proof
[(((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "big" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "big" "-")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Dave is blue.[(triple2)] Dave is kind.[(triple3)] Erin is not big.[(triple4)] Erin is white.[(triple5)] Gary is blue.[(triple6)] Gary is quiet.[(triple7)] @1: Gary is red.[(((triple7) -> rule1))] @2: Gary is big.[(((((triple7) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Erin is not big.
("Erin" "is" "big" "-")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
((triple7) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2