Bob is furry. If something is smart then it is nice. If something is furry then it is smart. Cold, smart things are nice. Young, furry things are green. Cold, green things are young. All smart, furry things are green. Smart, green things are young. Young things are white.
Bob is furry.
("Bob" "is" "furry" "+")
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Cold, smart things are nice.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Young, furry things are green.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Cold, green things are young.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
All smart, furry things are green.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Smart, green things are young.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is smart.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
True
7
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule6)) -> rule7))]
("Bob" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not young.
False
7
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule6)) -> rule7))]
("Bob" "is" "young" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
@0: Bob is furry.[(triple1)] @1: Bob is smart.[(((triple1) -> rule2))] @2: Bob is green.[(((((triple1) -> rule2) triple1) -> rule6))] Bob is nice.[(((((triple1) -> rule2)) -> rule1))] @3: Bob is young.[(((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule6)) -> rule7))] @4: Bob is white.[(((((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule6)) -> rule7)) -> rule8))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule2 % int4)) triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4