Bob is big. Bob is cold. Bob is furry. Bob is not red. Bob is smart. Bob is white. Bob is young. Harry is big. Harry is cold. Harry is furry. Harry is red. Harry is smart. Harry is not white. Harry is young. If Bob is not big then Bob is not cold. If Bob is not red then Bob is cold. White things are cold. If something is young then it is cold. Cold things are young. If Harry is big and Harry is red then Harry is furry. If something is big and not red then it is white. If Bob is smart and Bob is furry then Bob is young.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not white.
("Harry" "is" "white" "-")
Harry is young.
("Harry" "is" "young" "+")
If Bob is not big then Bob is not cold.
((("Bob" "is" "big" "~")) -> ("Bob" "is" "cold" "-"))
If Bob is not red then Bob is cold.
((("Bob" "is" "red" "~")) -> ("Bob" "is" "cold" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Harry is big and Harry is red then Harry is furry.
((("Harry" "is" "big" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "furry" "+"))
If something is big and not red then it is white.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "white" "+"))
If Bob is smart and Bob is furry then Bob is young.
((("Bob" "is" "smart" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "young" "+"))
Harry is cold.
True
1
proof
[(triple9 OR ((triple14) -> rule4))]
("Harry" "is" "cold" "+")
triple9
((triple14) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not smart.
False
1
inv-proof
[(triple12)]
("Harry" "is" "smart" "-")
triple12
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((triple4) -> rule2) OR ((triple6) -> rule3) OR ((triple7) -> rule4) OR ((((triple1 triple4) -> rule7)) -> rule3) OR ((((triple5 triple3) -> rule8)) -> rule4))] Bob is furry.[(triple3)] Bob is not red.[(triple4)] Bob is smart.[(triple5)] Bob is white.[(triple6 OR ((triple1 triple4) -> rule7))] Bob is young.[(triple7 OR ((triple2) -> rule5) OR ((triple5 triple3) -> rule8) OR ((((triple4) -> rule2)) -> rule5) OR ((((triple6) -> rule3)) -> rule5) OR ((((((triple1 triple4) -> rule7)) -> rule3)) -> rule5))] Harry is big.[(triple8)] Harry is cold.[(triple9 OR ((triple14) -> rule4))] Harry is furry.[(triple10 OR ((triple8 triple11) -> rule6))] Harry is not white.[(triple13)] Harry is red.[(triple11)] Harry is smart.[(triple12)] Harry is young.[(triple14 OR ((triple9) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple7) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1 triple4) -> (rule7 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple5 triple3) -> (rule8 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is not red.
("Bob" "is" "red" "-")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple1 triple4) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple5 triple3) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple1 triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple14) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple10
((triple8 triple11) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple9) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1