Bob is big. Bob is blue. Bob is not furry. Bob is nice. Bob is quiet. Bob is round. Bob is white. Fiona is big. Fiona is blue. Fiona is nice. Fiona is quiet. Fiona is round. All quiet people are blue. If someone is quiet then they are blue. If Bob is round and Bob is not big then Bob is blue. Blue, big people are quiet. If someone is quiet and not big then they are furry. If Fiona is blue then Fiona is white. If someone is round and not furry then they are nice. If someone is quiet then they are nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If Bob is round and Bob is not big then Bob is blue.
((("Bob" "is" "round" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "blue" "+"))
Blue, big people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and not big then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "+"))
If Fiona is blue then Fiona is white.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "white" "+"))
If someone is round and not furry then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Bob is nice.
True
1
proof
[(triple4 OR ((triple5) -> rule8) OR ((triple6 triple3) -> rule7) OR ((((triple2 triple1) -> rule4)) -> rule8))]
("Bob" "is" "nice" "+")
triple4
((triple5) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple6 triple3) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple2 triple1) -> (rule4 % int2))) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not round.
False
1
inv-proof
[(triple6)]
("Bob" "is" "round" "-")
triple6
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple5) -> rule1) OR ((triple5) -> rule2))] Bob is nice.[(triple4 OR ((triple5) -> rule8) OR ((triple6 triple3) -> rule7) OR ((((triple2 triple1) -> rule4)) -> rule8))] Bob is not furry.[(triple3)] Bob is quiet.[(triple5 OR ((triple2 triple1) -> rule4))] Bob is round.[(triple6)] Bob is white.[(triple7)] Fiona is big.[(triple8)] Fiona is blue.[(triple9 OR ((triple11) -> rule1) OR ((triple11) -> rule2))] Fiona is nice.[(triple10 OR ((triple11) -> rule8) OR ((((triple9 triple8) -> rule4)) -> rule8))] Fiona is quiet.[(triple11 OR ((triple9 triple8) -> rule4))] Fiona is round.[(triple12)] @1: Fiona is white.[(((triple9) -> rule6) OR ((((triple11) -> rule1)) -> rule6) OR ((((triple11) -> rule2)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple5) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple5) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
((triple5) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple6 triple3) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple2 triple1) -> (rule4 % int2))) -> (rule8 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple2 triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
((triple11) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple11) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple11) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple9 triple8) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
((triple9 triple8) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple12
Fiona is white.
("Fiona" "is" "white" "+")
((triple9) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple11) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2