Bob is quiet. Bob is rough. Erin is quiet. Gary is smart. Harry is blue. Harry is nice. Harry is smart. If someone is furry then they are smart. All nice people are blue. Blue people are quiet. All furry, blue people are quiet. If Harry is quiet and Harry is white then Harry is furry. If Gary is blue and Gary is white then Gary is smart. If Gary is smart then Gary is nice. All blue, white people are nice.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is furry then they are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All furry, blue people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is quiet and Harry is white then Harry is furry.
((("Harry" "is" "quiet" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "furry" "+"))
If Gary is blue and Gary is white then Gary is smart.
((("Gary" "is" "blue" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is smart then Gary is nice.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "nice" "+"))
All blue, white people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule2))]
("Harry" "is" "blue" "-")
triple5
((triple6) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
True
2
proof
[(((triple5) -> rule3) OR ((((triple6) -> rule2)) -> rule3))]
("Harry" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not quiet.
False
2
inv-proof
[(((triple5) -> rule3) OR ((((triple6) -> rule2)) -> rule3))]
("Harry" "is" "quiet" "-")
((triple5) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Gary is blue.
True
3
proof
[(((((triple4) -> rule7)) -> rule2))]
("Gary" "is" "blue" "+")
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule2))]
("Gary" "is" "blue" "-")
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "furry" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Bob" "is" "blue" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is quiet.[(triple1)] Bob is rough.[(triple2)] Erin is quiet.[(triple3)] Gary is smart.[(triple4)] Harry is blue.[(triple5 OR ((triple6) -> rule2))] Harry is nice.[(triple6)] Harry is smart.[(triple7)] @1: Gary is nice.[(((triple4) -> rule7))] Harry is quiet.[(((triple5) -> rule3) OR ((((triple6) -> rule2)) -> rule3))] @2: Gary is blue.[(((((triple4) -> rule7)) -> rule2))] @3: Gary is quiet.[(((((((triple4) -> rule7)) -> rule2)) -> rule3))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
((triple6) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple5) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3