Bob is cold. Bob is furry. Bob is red. If something is blue and red then it is furry. If something is red then it is blue. If Bob is not red then Bob is blue. Smart, blue things are kind. If something is green and red then it is kind. If something is green and blue then it is not kind. If Bob is blue and Bob is furry then Bob is smart. Blue things are smart.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
If something is blue and red then it is furry.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If Bob is not red then Bob is blue.
((("Bob" "is" "red" "~")) -> ("Bob" "is" "blue" "+"))
Smart, blue things are kind.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is green and red then it is kind.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is green and blue then it is not kind.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
If Bob is blue and Bob is furry then Bob is smart.
((("Bob" "is" "blue" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "smart" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is not furry.
False
1
inv-proof
[(triple2 OR ((((triple3) -> rule2) triple3) -> rule1))]
("Bob" "is" "furry" "-")
triple2
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is blue.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
True
3
proof
[(((((triple3) -> rule2)) -> rule8) OR ((((triple3) -> rule2) triple2) -> rule7) OR ((((triple3) -> rule2) ((((triple3) -> rule2) triple3) -> rule1)) -> rule7))]
("Bob" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not smart.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule8) OR ((((triple3) -> rule2) triple2) -> rule7) OR ((((triple3) -> rule2) ((((triple3) -> rule2) triple3) -> rule1)) -> rule7))]
("Bob" "is" "smart" "-")
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2 OR ((((triple3) -> rule2) triple3) -> rule1))] Bob is red.[(triple3)] @1: Bob is blue.[(((triple3) -> rule2))] @2: Bob is smart.[(((((triple3) -> rule2)) -> rule8) OR ((((triple3) -> rule2) triple2) -> rule7) OR ((((triple3) -> rule2) ((((triple3) -> rule2) triple3) -> rule1)) -> rule7))] @3: Bob is kind.[(((((((triple3) -> rule2)) -> rule8) ((triple3) -> rule2)) -> rule4) OR ((((((triple3) -> rule2) triple2) -> rule7) ((triple3) -> rule2)) -> rule4) OR ((((((triple3) -> rule2) ((((triple3) -> rule2) triple3) -> rule1)) -> rule7) ((triple3) -> rule2)) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3) -> (rule2 % int2)) triple2) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple3) -> (rule2 % int3))) -> (rule8 % int2)) ((triple3) -> (rule2 % int3))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple3) -> (rule2 % int3)) triple2) -> (rule7 % int2)) ((triple3) -> (rule2 % int3))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4)) triple3) -> (rule1 % int3))) -> (rule7 % int2)) ((triple3) -> (rule2 % int4))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4