Anne is red. Fiona is green. Fiona is nice. Fiona is quiet. Gary is not blue. Gary is green. Gary is red. All red, quiet people are nice. If someone is furry then they are not nice. If someone is nice and red then they are not smart. If someone is red and not blue then they are quiet. All green, furry people are quiet. If someone is nice and smart then they are red.
Anne is red.
("Anne" "is" "red" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
All red, quiet people are nice.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry then they are not nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "-"))
If someone is nice and red then they are not smart.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "-"))
If someone is red and not blue then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "+"))
All green, furry people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is nice and smart then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Fiona is nice.
True
1
proof
[(triple3)]
("Fiona" "is" "nice" "+")
triple3
Gary is not red.
False
1
inv-proof
[(triple7)]
("Gary" "is" "red" "-")
triple7
Gary is quiet.
True
3
proof
[(((triple7 triple5) -> rule4))]
("Gary" "is" "quiet" "+")
((triple7 triple5) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
3
inv-proof
[(((triple7 triple5) -> rule4))]
("Gary" "is" "quiet" "-")
((triple7 triple5) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
True
5
proof
[(((triple7 ((triple7 triple5) -> rule4)) -> rule1))]
("Gary" "is" "nice" "+")
((triple7 ((triple7 triple5) -> (rule4 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not nice.
False
5
inv-proof
[(((triple7 ((triple7 triple5) -> rule4)) -> rule1))]
("Gary" "is" "nice" "-")
((triple7 ((triple7 triple5) -> (rule4 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not smart.
True
7
proof
[(((((triple7 ((triple7 triple5) -> rule4)) -> rule1) triple7) -> rule3))]
("Gary" "is" "smart" "-")
((((triple7 ((triple7 triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is smart.
False
7
inv-proof
[(((((triple7 ((triple7 triple5) -> rule4)) -> rule1) triple7) -> rule3))]
("Gary" "is" "smart" "+")
((((triple7 ((triple7 triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "-")
Anne is nice.
Unknown
rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is red.[(triple1)] Fiona is green.[(triple2)] Fiona is nice.[(triple3)] Fiona is quiet.[(triple4)] Gary is green.[(triple6)] Gary is not blue.[(triple5)] Gary is red.[(triple7)] @1: Gary is quiet.[(((triple7 triple5) -> rule4))] @2: Gary is nice.[(((triple7 ((triple7 triple5) -> rule4)) -> rule1))] @3: Gary is not smart.[(((((triple7 ((triple7 triple5) -> rule4)) -> rule1) triple7) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is not blue.
("Gary" "is" "blue" "-")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7 triple5) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple7 ((triple7 triple5) -> (rule4 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not smart.
("Gary" "is" "smart" "-")
((((triple7 ((triple7 triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3