Bob is big. Bob is furry. Bob is nice. Bob is red. Bob is not rough. Bob is not smart. Bob is white. If someone is big then they are furry. Rough people are furry. All smart people are big. Nice, red people are big. All rough people are big. Nice, big people are red. If Bob is not rough then Bob is red. If someone is smart and not big then they are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Nice, red people are big.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Nice, big people are red.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If Bob is not rough then Bob is red.
((("Bob" "is" "rough" "~")) -> ("Bob" "is" "red" "+"))
If someone is smart and not big then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "white" "+"))
Bob is nice.
True
1
proof
[(triple3)]
("Bob" "is" "nice" "+")
triple3
Bob is rough.
False
1
inv-proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
@0: Bob is big.[(triple1 OR ((triple3 triple4) -> rule4) OR ((triple3 ((triple5) -> rule7)) -> rule4))] Bob is furry.[(triple2 OR ((triple1) -> rule1) OR ((((triple3 triple4) -> rule4)) -> rule1) OR ((((triple3 ((triple5) -> rule7)) -> rule4)) -> rule1))] Bob is nice.[(triple3)] Bob is not rough.[(triple5)] Bob is not smart.[(triple6)] Bob is red.[(triple4 OR ((triple5) -> rule7) OR ((triple3 triple1) -> rule6))] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple4) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple3 ((triple5) -> (rule7 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple1) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple3 triple4) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple3 ((triple5) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not rough.
("Bob" "is" "rough" "-")
triple5
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple5) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple3 triple1) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7