Bob is big. Bob is blue. Bob is cold. Bob is furry. Bob is rough. Bob is round. Bob is young. If someone is big then they are round. If Bob is young then Bob is blue. If Bob is cold then Bob is rough. All big people are round. All blue people are furry. If Bob is round and Bob is big then Bob is cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Bob is young then Bob is blue.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "blue" "+"))
If Bob is cold then Bob is rough.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "rough" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Bob is round and Bob is big then Bob is cold.
((("Bob" "is" "round" "+") ("Bob" "is" "big" "+")) -> ("Bob" "is" "cold" "+"))
Bob is furry.
True
1
proof
[(triple4 OR ((triple2) -> rule5) OR ((((triple7) -> rule2)) -> rule5))]
("Bob" "is" "furry" "+")
triple4
((triple2) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not round.
False
1
inv-proof
[(triple6 OR ((triple1) -> rule1) OR ((triple1) -> rule4))]
("Bob" "is" "round" "-")
triple6
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple7) -> rule2))] Bob is cold.[(triple3 OR ((triple6 triple1) -> rule6) OR ((((triple1) -> rule1) triple1) -> rule6) OR ((((triple1) -> rule4) triple1) -> rule6))] Bob is furry.[(triple4 OR ((triple2) -> rule5) OR ((((triple7) -> rule2)) -> rule5))] Bob is rough.[(triple5 OR ((triple3) -> rule3) OR ((((triple6 triple1) -> rule6)) -> rule3) OR ((((((triple1) -> rule1) triple1) -> rule6)) -> rule3) OR ((((((triple1) -> rule4) triple1) -> rule6)) -> rule3))] Bob is round.[(triple6 OR ((triple1) -> rule1) OR ((triple1) -> rule4))] Bob is young.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple7) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple6 triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1) -> (rule1 % int2)) triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple4
((triple2) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple3) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6 triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple1) -> (rule1 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7