Bob is blue. Bob is nice. Bob is quiet. Bob is round. Bob is smart. Fiona is blue. Fiona is nice. Fiona is quiet. Fiona is rough. Fiona is round. All quiet people are nice. If Fiona is rough and Fiona is nice then Fiona is round. If someone is quiet and rough then they are furry. Quiet people are blue. All rough, quiet people are smart. If someone is furry then they are round. If someone is rough and smart then they are furry. If someone is round and blue then they are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If Fiona is rough and Fiona is nice then Fiona is round.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "round" "+"))
If someone is quiet and rough then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
All rough, quiet people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is furry then they are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and smart then they are furry.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is round and blue then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Fiona is quiet.
True
1
proof
[(triple8)]
("Fiona" "is" "quiet" "+")
triple8
Bob is not smart.
False
1
inv-proof
[(triple5)]
("Bob" "is" "smart" "-")
triple5
Bob is furry.
True
3
proof
[(((triple4 triple1) -> rule8) OR ((triple4 ((triple3) -> rule4)) -> rule8))]
("Bob" "is" "furry" "+")
((triple4 triple1) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple4 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((triple4 triple1) -> rule8) OR ((triple4 ((triple3) -> rule4)) -> rule8))]
("Bob" "is" "furry" "-")
((triple4 triple1) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple4 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
@0: Bob is blue.[(triple1 OR ((triple3) -> rule4))] Bob is nice.[(triple2 OR ((triple3) -> rule1))] Bob is quiet.[(triple3)] Bob is round.[(triple4)] Bob is smart.[(triple5)] Fiona is blue.[(triple6 OR ((triple8) -> rule4))] Fiona is nice.[(triple7 OR ((triple8) -> rule1))] Fiona is quiet.[(triple8)] Fiona is rough.[(triple9)] Fiona is round.[(triple10 OR ((triple9 triple7) -> rule2) OR ((((triple8 triple9) -> rule3)) -> rule6) OR ((triple9 ((triple8) -> rule1)) -> rule2) OR ((((triple9 ((triple9 triple8) -> rule5)) -> rule7)) -> rule6))] @1: Bob is furry.[(((triple4 triple1) -> rule8) OR ((triple4 ((triple3) -> rule4)) -> rule8))] Fiona is furry.[(((triple10 triple6) -> rule8) OR ((triple8 triple9) -> rule3) OR ((triple10 ((triple8) -> rule4)) -> rule8) OR ((triple9 ((triple9 triple8) -> rule5)) -> rule7) OR ((((triple9 triple7) -> rule2) triple6) -> rule8) OR ((((triple9 triple7) -> rule2) ((triple8) -> rule4)) -> rule8) OR ((((triple9 ((triple8) -> rule1)) -> rule2) triple6) -> rule8) OR ((((triple9 ((triple8) -> rule1)) -> rule2) ((triple8) -> rule4)) -> rule8))] Fiona is smart.[(((triple9 triple8) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple3) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
((triple8) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
((triple8) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((triple9 triple7) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple8 triple9) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((triple9 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple9 ((triple9 triple8) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
((triple4 triple1) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple4 ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple10 triple6) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple8 triple9) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple10 ((triple8) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((triple9 ((triple9 triple8) -> (rule5 % int2))) -> (rule7 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple9 triple7) -> (rule2 % int2)) triple6) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((triple9 triple7) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((triple9 ((triple8) -> (rule1 % int3))) -> (rule2 % int2)) triple6) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
((((triple9 ((triple8) -> (rule1 % int4))) -> (rule2 % int3)) ((triple8) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9 triple8) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1