Fiona is cold. Fiona is furry. Fiona is green. Fiona is red. Fiona is round. Fiona is smart. Fiona is white. All cold people are green. If someone is green then they are cold. Smart, cold people are white. All smart people are cold. If someone is round then they are cold. If someone is white and round then they are red.
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Smart, cold people are white.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is white and round then they are red.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Fiona is white.
True
1
proof
[(triple7 OR ((triple6 triple1) -> rule3) OR ((triple6 ((triple3) -> rule2)) -> rule3) OR ((triple6 ((triple5) -> rule5)) -> rule3) OR ((triple6 ((triple6) -> rule4)) -> rule3))]
("Fiona" "is" "white" "+")
triple7
((triple6 triple1) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple6 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple6 ((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple6 ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not green.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule1) OR ((((triple5) -> rule5)) -> rule1) OR ((((triple6) -> rule4)) -> rule1))]
("Fiona" "is" "green" "-")
triple3
((triple1) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
@0: Fiona is cold.[(triple1 OR ((triple3) -> rule2) OR ((triple5) -> rule5) OR ((triple6) -> rule4))] Fiona is furry.[(triple2)] Fiona is green.[(triple3 OR ((triple1) -> rule1) OR ((((triple5) -> rule5)) -> rule1) OR ((((triple6) -> rule4)) -> rule1))] Fiona is red.[(triple4 OR ((triple7 triple5) -> rule6) OR ((((triple6 triple1) -> rule3) triple5) -> rule6) OR ((((triple6 ((triple3) -> rule2)) -> rule3) triple5) -> rule6) OR ((((triple6 ((triple5) -> rule5)) -> rule3) triple5) -> rule6) OR ((((triple6 ((triple6) -> rule4)) -> rule3) triple5) -> rule6))] Fiona is round.[(triple5)] Fiona is smart.[(triple6)] Fiona is white.[(triple7 OR ((triple6 triple1) -> rule3) OR ((triple6 ((triple3) -> rule2)) -> rule3) OR ((triple6 ((triple5) -> rule5)) -> rule3) OR ((triple6 ((triple6) -> rule4)) -> rule3))]
Fiona is cold.
("Fiona" "is" "cold" "+")
triple1
((triple3) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple5) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((triple6) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
((triple1) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
triple4
((triple7 triple5) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple6 triple1) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((triple6 ((triple3) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((triple6 ((triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((triple6 ((triple6) -> (rule4 % int3))) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
triple5
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
((triple6 triple1) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((triple6 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple6 ((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple6 ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2