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