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