Fiona is furry. Fiona is kind. Fiona is quiet. Fiona is red. Fiona is rough. Fiona is round. Fiona is smart. If something is rough and quiet then it is kind. Quiet, round things are red. All rough things are smart. All quiet things are furry. All rough, round things are smart. All round, red things are furry. All round, quiet things are smart. Smart things are furry.
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is rough and quiet then it is kind.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Quiet, round things are red.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All rough, round things are smart.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All round, red things are furry.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All round, quiet things are smart.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Fiona is rough.
True
1
proof
[(triple5)]
("Fiona" "is" "rough" "+")
triple5
Fiona is not red.
False
1
inv-proof
[(triple4 OR ((triple3 triple6) -> rule2))]
("Fiona" "is" "red" "-")
triple4
((triple3 triple6) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
@0: Fiona is furry.[(triple1 OR ((triple3) -> rule4) OR ((triple7) -> rule8) OR ((triple6 triple4) -> rule6) OR ((((triple5) -> rule3)) -> rule8) OR ((((triple5 triple6) -> rule5)) -> rule8) OR ((((triple6 triple3) -> rule7)) -> rule8) OR ((triple6 ((triple3 triple6) -> rule2)) -> rule6))] Fiona is kind.[(triple2 OR ((triple5 triple3) -> rule1))] Fiona is quiet.[(triple3)] Fiona is red.[(triple4 OR ((triple3 triple6) -> rule2))] Fiona is rough.[(triple5)] Fiona is round.[(triple6)] Fiona is smart.[(triple7 OR ((triple5) -> rule3) OR ((triple5 triple6) -> rule5) OR ((triple6 triple3) -> rule7))]
Fiona is furry.
("Fiona" "is" "furry" "+")
triple1
((triple3) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple7) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple6 triple4) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple5 triple6) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple6 triple3) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple6 ((triple3 triple6) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
((triple5 triple3) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
((triple3 triple6) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
((triple5) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple5 triple6) -> (rule5 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple6 triple3) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1