Anne is cold. Anne is furry. Anne is kind. Anne is nice. Anne is rough. Anne is round. Fiona is blue. Fiona is cold. Fiona is furry. Fiona is nice. Fiona is rough. Fiona is round. If Anne is nice and Anne is furry then Anne is kind. Rough, cold things are round. If something is kind and blue then it is cold. Blue things are cold. If something is rough and blue then it is nice. Nice things are 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 rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If Anne is nice and Anne is furry then Anne is kind.
((("Anne" "is" "nice" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "kind" "+"))
Rough, cold things are round.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is kind and blue then it is cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is rough and blue then it is nice.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Anne is furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple12 OR ((triple11 triple8) -> rule2) OR ((triple11 ((triple7) -> rule4)) -> rule2) OR ((triple11 ((((triple10) -> rule6)) -> rule4)) -> rule2))]
("Fiona" "is" "round" "-")
triple12
((triple11 triple8) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple11 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple11 ((((triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Anne is blue.
True
2
proof
[(((triple4) -> rule6))]
("Anne" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple4) -> rule6))]
("Anne" "is" "blue" "-")
((triple4) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
@0: Anne is cold.[(triple1 OR ((((triple4) -> rule6)) -> rule4) OR ((triple3 ((triple4) -> rule6)) -> rule3) OR ((((triple4 triple2) -> rule1) ((triple4) -> rule6)) -> rule3))] Anne is furry.[(triple2)] Anne is kind.[(triple3 OR ((triple4 triple2) -> rule1))] Anne is nice.[(triple4)] Anne is rough.[(triple5)] Anne is round.[(triple6 OR ((triple5 triple1) -> rule2) OR ((triple5 ((((triple4) -> rule6)) -> rule4)) -> rule2) OR ((triple5 ((triple3 ((triple4) -> rule6)) -> rule3)) -> rule2) OR ((triple5 ((((triple4 triple2) -> rule1) ((triple4) -> rule6)) -> rule3)) -> rule2))] Fiona is blue.[(triple7 OR ((triple10) -> rule6))] Fiona is cold.[(triple8 OR ((triple7) -> rule4) OR ((((triple10) -> rule6)) -> rule4))] Fiona is furry.[(triple9)] Fiona is nice.[(triple10 OR ((triple11 triple7) -> rule5))] Fiona is rough.[(triple11)] Fiona is round.[(triple12 OR ((triple11 triple8) -> rule2) OR ((triple11 ((triple7) -> rule4)) -> rule2) OR ((triple11 ((((triple10) -> rule6)) -> rule4)) -> rule2))] @1: Anne is blue.[(((triple4) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple3 ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple4 triple2) -> (rule1 % int3)) ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple4 triple2) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple5 triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple5 ((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((triple5 ((triple3 ((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((triple5 ((((triple4 triple2) -> (rule1 % int4)) ((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
((triple10) -> (rule6 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple7) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple11 triple7) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Fiona is round.
("Fiona" "is" "round" "+")
triple12
((triple11 triple8) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple11 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
((triple11 ((((triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1