Bob is cold. Bob is furry. Bob is nice. Bob is red. Bob is white. Bob is young. Harry is cold. Harry is furry. Harry is nice. Harry is red. All cold people are nice. If Harry is white then Harry is red. If someone is young and cold then they are white. If someone is white then they are rough. Red people are white. All rough, red people are young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
All cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If Harry is white then Harry is red.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "red" "+"))
If someone is young and cold then they are white.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All rough, red people are young.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Bob is white.
True
1
proof
[(triple5 OR ((triple4) -> rule5) OR ((triple6 triple1) -> rule3))]
("Bob" "is" "white" "+")
triple5
((triple4) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple6 triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Bob is rough.
True
2
proof
[(((triple5) -> rule4) OR ((((triple4) -> rule5)) -> rule4) OR ((((triple6 triple1) -> rule3)) -> rule4))]
("Bob" "is" "rough" "+")
((triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple6 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not rough.
False
2
inv-proof
[(((triple5) -> rule4) OR ((((triple4) -> rule5)) -> rule4) OR ((((triple6 triple1) -> rule3)) -> rule4))]
("Bob" "is" "rough" "-")
((triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple6 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Harry is rough.
True
3
proof
[(((((triple10) -> rule5)) -> rule4))]
("Harry" "is" "rough" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule4))]
("Harry" "is" "rough" "-")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
True
5
proof
[(((((((triple10) -> rule5)) -> rule4) triple10) -> rule6))]
("Harry" "is" "young" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not young.
False
5
inv-proof
[(((((((triple10) -> rule5)) -> rule4) triple10) -> rule6))]
("Harry" "is" "young" "-")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3 OR ((triple1) -> rule1))] Bob is red.[(triple4)] Bob is white.[(triple5 OR ((triple4) -> rule5) OR ((triple6 triple1) -> rule3))] Bob is young.[(triple6 OR ((((triple5) -> rule4) triple4) -> rule6) OR ((((((triple4) -> rule5)) -> rule4) triple4) -> rule6))] Harry is cold.[(triple7)] Harry is furry.[(triple8)] Harry is nice.[(triple9 OR ((triple7) -> rule1))] Harry is red.[(triple10)] @1: Bob is rough.[(((triple5) -> rule4) OR ((((triple4) -> rule5)) -> rule4) OR ((((triple6 triple1) -> rule3)) -> rule4))] Harry is white.[(((triple10) -> rule5))] @2: Harry is rough.[(((((triple10) -> rule5)) -> rule4))] @3: Harry is young.[(((((((triple10) -> rule5)) -> rule4) triple10) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
((triple4) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple6 triple1) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple6
((((triple5) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple4) -> (rule5 % int3))) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((triple7) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
Bob is rough.
("Bob" "is" "rough" "+")
((triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple6 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple10) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((((triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3