Fiona is blue. Fiona is white. Harry is blue. Harry is furry. Harry is green. Harry is smart. Harry is white. If something is blue then it is smart. If something is white and not blue then it is not smart. If Fiona is smart and Fiona is cold then Fiona is not green. If something is blue and furry then it is cold. All blue things are cold. If something is blue and smart then it is big. All white, smart things are big. If something is white and not smart then it is not big.
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is blue then it is smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is white and not blue then it is not smart.
((("something" "is" "white" "+") ("something" "is" "blue" "~")) -> ("something" "is" "smart" "-"))
If Fiona is smart and Fiona is cold then Fiona is not green.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "green" "-"))
If something is blue and furry then it is cold.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is blue and smart then it is big.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All white, smart things are big.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
If something is white and not smart then it is not big.
((("something" "is" "white" "+") ("something" "is" "smart" "~")) -> ("something" "is" "big" "-"))
Harry is furry.
True
1
proof
[(triple4)]
("Harry" "is" "furry" "+")
triple4
Fiona is not white.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "white" "-")
triple2
Harry is big.
True
3
proof
[(((triple3 triple6) -> rule6) OR ((triple7 triple6) -> rule7) OR ((triple3 ((triple3) -> rule1)) -> rule6) OR ((triple7 ((triple3) -> rule1)) -> rule7))]
("Harry" "is" "big" "+")
((triple3 triple6) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple7 triple6) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple7 ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Fiona is not cold.
False
2
inv-proof
[(((triple1) -> rule5))]
("Fiona" "is" "cold" "-")
((triple1) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is big.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((triple2 ((triple1) -> rule1)) -> rule7))]
("Fiona" "is" "big" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple2 ((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
False
5
inv-proof
[(((((triple1) -> rule1) ((triple1) -> rule5)) -> rule3))]
("Fiona" "is" "green" "+")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
@0: Fiona is blue.[(triple1)] Fiona is white.[(triple2)] Harry is blue.[(triple3)] Harry is furry.[(triple4)] Harry is green.[(triple5)] Harry is smart.[(triple6 OR ((triple3) -> rule1))] Harry is white.[(triple7)] @1: Fiona is cold.[(((triple1) -> rule5))] Fiona is smart.[(((triple1) -> rule1))] Harry is big.[(((triple3 triple6) -> rule6) OR ((triple7 triple6) -> rule7) OR ((triple3 ((triple3) -> rule1)) -> rule6) OR ((triple7 ((triple3) -> rule1)) -> rule7))] Harry is cold.[(((triple3) -> rule5) OR ((triple3 triple4) -> rule4))] @2: Fiona is big.[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((triple2 ((triple1) -> rule1)) -> rule7))] Fiona is not green.[(((((triple1) -> rule1) ((triple1) -> rule5)) -> rule3))]
Fiona is blue.
("Fiona" "is" "blue" "+")
triple1
Fiona is white.
("Fiona" "is" "white" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple1) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple3 triple6) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple7 triple6) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((triple7 ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple3 triple4) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple2 ((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not green.
("Fiona" "is" "green" "-")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not green.
("Fiona" "is" "green" "-")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3