Erin is cold. Erin is furry. Erin is green. Erin is kind. Erin is quiet. Erin is rough. Erin is round. Fiona is cold. Fiona is furry. Fiona is green. Fiona is kind. Fiona is quiet. Fiona is rough. Fiona is round. All kind things are quiet. If something is cold then it is round. Round things are furry. If Fiona is furry and Fiona is rough then Fiona is round. If something is cold then it is rough. All quiet, kind things are green. All cold things are quiet. If something is quiet and cold then it is green.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If Fiona is furry and Fiona is rough then Fiona is round.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "round" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All quiet, kind things are green.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and cold then it is green.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Erin is round.
True
1
proof
[(triple7 OR ((triple1) -> rule2))]
("Erin" "is" "round" "+")
triple7
((triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is not quiet.
False
1
inv-proof
[(triple12 OR ((triple11) -> rule1) OR ((triple8) -> rule7))]
("Fiona" "is" "quiet" "-")
triple12
((triple11) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple8) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
@0: Erin is cold.[(triple1)] Erin is furry.[(triple2 OR ((triple7) -> rule3) OR ((((triple1) -> rule2)) -> rule3))] Erin is green.[(triple3 OR ((triple5 triple1) -> rule8) OR ((triple5 triple4) -> rule6) OR ((((triple1) -> rule7) triple1) -> rule8) OR ((((triple1) -> rule7) triple4) -> rule6) OR ((((triple4) -> rule1) triple1) -> rule8) OR ((((triple4) -> rule1) triple4) -> rule6))] Erin is kind.[(triple4)] Erin is quiet.[(triple5 OR ((triple1) -> rule7) OR ((triple4) -> rule1))] Erin is rough.[(triple6 OR ((triple1) -> rule5))] Erin is round.[(triple7 OR ((triple1) -> rule2))] Fiona is cold.[(triple8)] Fiona is furry.[(triple9 OR ((triple14) -> rule3) OR ((((triple8) -> rule2)) -> rule3))] Fiona is green.[(triple10 OR ((triple12 triple11) -> rule6) OR ((triple12 triple8) -> rule8) OR ((((triple11) -> rule1) triple11) -> rule6) OR ((((triple11) -> rule1) triple8) -> rule8) OR ((((triple8) -> rule7) triple11) -> rule6) OR ((((triple8) -> rule7) triple8) -> rule8))] Fiona is kind.[(triple11)] Fiona is quiet.[(triple12 OR ((triple11) -> rule1) OR ((triple8) -> rule7))] Fiona is rough.[(triple13 OR ((triple8) -> rule5))] Fiona is round.[(triple14 OR ((triple8) -> rule2) OR ((triple9 triple13) -> rule4) OR ((triple9 ((triple8) -> rule5)) -> rule4))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple7) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple3
((triple5 triple1) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple5 triple4) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple1) -> (rule7 % int2)) triple1) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple1) -> (rule7 % int2)) triple4) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple4) -> (rule1 % int2)) triple1) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple1) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple4) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple1) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple7
((triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
((triple14) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple10
((triple12 triple11) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple12 triple8) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple11) -> (rule1 % int2)) triple11) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple11) -> (rule1 % int2)) triple8) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple8) -> (rule7 % int2)) triple11) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple8) -> (rule7 % int2)) triple8) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple12
((triple11) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple8) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple13
((triple8) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple14
((triple8) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple9 triple13) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple9 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2