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