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