Bob is big. Bob is cold. Bob is furry. Bob is kind. Bob is red. Bob is rough. Bob is round. If Bob is cold then Bob is big. If something is red then it is kind. If something is big and round then it is cold. Round things are cold. If something is red and not round then it is rough. Big things are rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
If Bob is cold then Bob is big.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "big" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is big and round then it is cold.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is red and not round then it is rough.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "is" "rough" "+"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Bob is kind.
True
1
proof
[(triple4 OR ((triple5) -> rule2))]
("Bob" "is" "kind" "+")
triple4
((triple5) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not furry.
False
1
inv-proof
[(triple3)]
("Bob" "is" "furry" "-")
triple3
@0: Bob is big.[(triple1 OR ((triple2) -> rule1) OR ((((triple7) -> rule4)) -> rule1))] Bob is cold.[(triple2 OR ((triple7) -> rule4) OR ((triple1 triple7) -> rule3))] Bob is furry.[(triple3)] Bob is kind.[(triple4 OR ((triple5) -> rule2))] Bob is red.[(triple5)] Bob is rough.[(triple6 OR ((triple1) -> rule6) OR ((((triple2) -> rule1)) -> rule6) OR ((((((triple7) -> rule4)) -> rule1)) -> rule6))] Bob is round.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple7) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple1 triple7) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple5) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple1) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple7) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple7