Anne is big. Anne is cold. Anne is kind. Anne is nice. Anne is red. Anne is rough. Anne is round. If something is cold then it is rough. If something is rough and red then it is round. Cold, round things are red. All cold, nice things are big. If Anne is rough and Anne is kind then Anne is big. Round things are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something is rough and red then it is round.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Cold, round things are red.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All cold, nice things are big.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If Anne is rough and Anne is kind then Anne is big.
((("Anne" "is" "rough" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "big" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Anne is kind.
True
1
proof
[(triple3)]
("Anne" "is" "kind" "+")
triple3
Anne is not round.
False
1
inv-proof
[(triple7 OR ((triple6 triple5) -> rule2) OR ((((triple2) -> rule1) triple5) -> rule2))]
("Anne" "is" "round" "-")
triple7
((triple6 triple5) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
@0: Anne is big.[(triple1 OR ((triple2 triple4) -> rule4) OR ((triple6 triple3) -> rule5) OR ((triple2 ((triple7) -> rule6)) -> rule4) OR ((((triple2) -> rule1) triple3) -> rule5) OR ((triple2 ((((triple6 triple5) -> rule2)) -> rule6)) -> rule4) OR ((triple2 ((((((triple2) -> rule1) triple5) -> rule2)) -> rule6)) -> rule4))] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4 OR ((triple7) -> rule6) OR ((((triple6 triple5) -> rule2)) -> rule6) OR ((((((triple2) -> rule1) triple5) -> rule2)) -> rule6))] Anne is red.[(triple5 OR ((triple2 triple7) -> rule3))] Anne is rough.[(triple6 OR ((triple2) -> rule1))] Anne is round.[(triple7 OR ((triple6 triple5) -> rule2) OR ((((triple2) -> rule1) triple5) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2 triple4) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple6 triple3) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple2 ((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple2) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
((triple2 ((((triple6 triple5) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((triple2 ((((((triple2) -> (rule1 % int4)) triple5) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple7) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple6 triple5) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple2) -> (rule1 % int3)) triple5) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple2 triple7) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple6
((triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple7
((triple6 triple5) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2