Fiona is big. Fiona is cold. Fiona is furry. Fiona is nice. Fiona is smart. Fiona is white. Fiona is young. Gary is big. Gary is cold. Gary is furry. Gary is nice. Gary is smart. Gary is white. Gary is young. All cold things are young. If something is young and white then it is furry. Smart, big things are young.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is young and white then it is furry.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Smart, big things are young.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Fiona is white.
True
1
proof
[(triple6)]
("Fiona" "is" "white" "+")
triple6
Gary is not big.
False
1
inv-proof
[(triple8)]
("Gary" "is" "big" "-")
triple8
@0: Fiona is big.[(triple1)] Fiona is cold.[(triple2)] Fiona is furry.[(triple3 OR ((triple7 triple6) -> rule2) OR ((((triple2) -> rule1) triple6) -> rule2) OR ((((triple5 triple1) -> rule3) triple6) -> rule2))] Fiona is nice.[(triple4)] Fiona is smart.[(triple5)] Fiona is white.[(triple6)] Fiona is young.[(triple7 OR ((triple2) -> rule1) OR ((triple5 triple1) -> rule3))] Gary is big.[(triple8)] Gary is cold.[(triple9)] Gary is furry.[(triple10 OR ((triple14 triple13) -> rule2) OR ((((triple9) -> rule1) triple13) -> rule2) OR ((((triple12 triple8) -> rule3) triple13) -> rule2))] Gary is nice.[(triple11)] Gary is smart.[(triple12)] Gary is white.[(triple13)] Gary is young.[(triple14 OR ((triple9) -> rule1) OR ((triple12 triple8) -> rule3))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
((triple7 triple6) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple2) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
((((triple5 triple1) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Fiona is smart.
("Fiona" "is" "smart" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
((triple2) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple5 triple1) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
((triple14 triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple9) -> (rule1 % int2)) triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple12 triple8) -> (rule3 % int2)) triple13) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Gary is white.
("Gary" "is" "white" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14
((triple9) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple12 triple8) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1