Charlie is smart. Erin is quiet. Fiona is furry. Gary is round. Furry, quiet things are nice. If something is blue and kind then it is nice. Smart things are kind. All furry, blue things are smart. Blue things are quiet. Blue, kind things are smart. Quiet things are blue. If something is round then it is quiet.
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Furry, quiet things are nice.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is blue and kind then it is nice.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All furry, blue things are smart.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Blue, kind things are smart.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is round then it is quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
Fiona is furry.
True
1
proof
[(triple3)]
("Fiona" "is" "furry" "+")
triple3
Gary is not round.
False
1
inv-proof
[(triple4)]
("Gary" "is" "round" "-")
triple4
Charlie is kind.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "blue" "-")
((triple2) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is blue.
True
3
proof
[(((((triple4) -> rule8)) -> rule7))]
("Gary" "is" "blue" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule7))]
("Gary" "is" "blue" "-")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is not nice.
Unknown
inv-rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule4 <- FAIL)]]
("Gary" "is" "nice" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Fiona" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is smart.[(triple1)] Erin is quiet.[(triple2)] Fiona is furry.[(triple3)] Gary is round.[(triple4)] @1: Charlie is kind.[(((triple1) -> rule3))] Erin is blue.[(((triple2) -> rule7))] Gary is quiet.[(((triple4) -> rule8))] @2: Gary is blue.[(((((triple4) -> rule8)) -> rule7))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2