Bob is smart. Erin is blue. Erin is smart. Harry is blue. Harry is nice. Harry is quiet. Harry is round. Furry things are smart. If something is smart and furry then it is rough. If Bob is smart then Bob is furry. Quiet things are blue. Quiet, rough things are smart. If something is quiet then it is blue. All blue things are rough. All nice things are furry.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is smart and furry then it is rough.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Bob is smart then Bob is furry.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "furry" "+"))
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Quiet, rough things are smart.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Harry is quiet.
True
1
proof
[(triple6)]
("Harry" "is" "quiet" "+")
triple6
Erin is not blue.
False
1
inv-proof
[(triple2)]
("Erin" "is" "blue" "-")
triple2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is smart.[(triple1)] Erin is blue.[(triple2)] Erin is smart.[(triple3)] Harry is blue.[(triple4 OR ((triple6) -> rule4) OR ((triple6) -> rule6))] Harry is nice.[(triple5)] Harry is quiet.[(triple6)] Harry is round.[(triple7)] @1: Bob is furry.[(((triple1) -> rule3))] Erin is rough.[(((triple2) -> rule7))] Harry is furry.[(((triple5) -> rule8))] Harry is rough.[(((triple4) -> rule7) OR ((((triple6) -> rule4)) -> rule7) OR ((((triple6) -> rule6)) -> rule7) OR ((((((triple5) -> rule8)) -> rule1) ((triple5) -> rule8)) -> rule2))] @2: Bob is rough.[(((triple1 ((triple1) -> rule3)) -> rule2))] Harry is smart.[(((((triple5) -> rule8)) -> rule1) OR ((triple6 ((triple4) -> rule7)) -> rule5) OR ((triple6 ((((triple6) -> rule4)) -> rule7)) -> rule5) OR ((triple6 ((((triple6) -> rule6)) -> rule7)) -> rule5))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
((triple6) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple6) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple2) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple5) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule7 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple5) -> (rule8 % int3))) -> (rule1 % int2)) ((triple5) -> (rule8 % int3))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple6 ((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple6 ((((triple6) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple6 ((((triple6) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3