Fiona is blue. Fiona is furry. Fiona is green. Fiona is nice. Fiona is quiet. Fiona is rough. Fiona is young. All furry, quiet things are young. If Fiona is green then Fiona is nice. Quiet things are nice. Rough things are furry. If Fiona is quiet and Fiona is nice then Fiona is green. If Fiona is blue then Fiona is quiet.
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All furry, quiet things are young.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If Fiona is green then Fiona is nice.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "nice" "+"))
Quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If Fiona is quiet and Fiona is nice then Fiona is green.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "green" "+"))
If Fiona is blue then Fiona is quiet.
((("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "quiet" "+"))
Fiona is furry.
True
1
proof
[(triple2 OR ((triple6) -> rule4))]
("Fiona" "is" "furry" "+")
triple2
((triple6) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is not green.
False
1
inv-proof
[(triple3 OR ((triple5 triple4) -> rule5) OR ((triple5 ((triple5) -> rule3)) -> rule5) OR ((((triple1) -> rule6) triple4) -> rule5) OR ((((triple1) -> rule6) ((triple5) -> rule3)) -> rule5) OR ((triple5 ((((triple1) -> rule6)) -> rule3)) -> rule5) OR ((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule3)) -> rule5))]
("Fiona" "is" "green" "-")
triple3
((triple5 triple4) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple1) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((triple5 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
@0: Fiona is blue.[(triple1)] Fiona is furry.[(triple2 OR ((triple6) -> rule4))] Fiona is green.[(triple3 OR ((triple5 triple4) -> rule5) OR ((triple5 ((triple5) -> rule3)) -> rule5) OR ((((triple1) -> rule6) triple4) -> rule5) OR ((((triple1) -> rule6) ((triple5) -> rule3)) -> rule5) OR ((triple5 ((((triple1) -> rule6)) -> rule3)) -> rule5) OR ((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule3)) -> rule5))] Fiona is nice.[(triple4 OR ((triple3) -> rule2) OR ((triple5) -> rule3) OR ((((triple1) -> rule6)) -> rule3))] Fiona is quiet.[(triple5 OR ((triple1) -> rule6))] Fiona is rough.[(triple6)] Fiona is young.[(triple7 OR ((triple2 triple5) -> rule1) OR ((triple2 ((triple1) -> rule6)) -> rule1) OR ((((triple6) -> rule4) triple5) -> rule1) OR ((((triple6) -> rule4) ((triple1) -> rule6)) -> rule1))]
Fiona is blue.
("Fiona" "is" "blue" "+")
triple1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple2
((triple6) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple3
((triple5 triple4) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple1) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((triple5 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
((triple3) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((triple5) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
((triple1) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
((triple2 triple5) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple2 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple6) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3