Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is nice. Anne is round. Anne is young. Harry is big. Harry is cold. Harry is furry. Harry is nice. Harry is young. If Harry is young then Harry is round. If something is furry then it is cold. If Anne is cold then Anne is round. All round things are young. If something is furry and cold then it is blue. All furry things are cold. Big things are young. If Anne is nice and Anne is blue then Anne is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is young then Harry is round.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "round" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If Anne is cold then Anne is round.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "round" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is furry and cold then it is blue.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Anne is nice and Anne is blue then Anne is round.
((("Anne" "is" "nice" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "round" "+"))
Anne is cold.
True
1
proof
[(triple3 OR ((triple4) -> rule2) OR ((triple4) -> rule6))]
("Anne" "is" "cold" "+")
triple3
((triple4) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple4 triple3) -> rule5) OR ((triple4 ((triple4) -> rule2)) -> rule5) OR ((triple4 ((triple4) -> rule6)) -> rule5))] Anne is cold.[(triple3 OR ((triple4) -> rule2) OR ((triple4) -> rule6))] Anne is furry.[(triple4)] Anne is nice.[(triple5)] Anne is round.[(triple6 OR ((triple3) -> rule3) OR ((triple5 triple2) -> rule8) OR ((((triple4) -> rule2)) -> rule3) OR ((((triple4) -> rule6)) -> rule3) OR ((triple5 ((triple4 triple3) -> rule5)) -> rule8) OR ((triple5 ((triple4 ((triple4) -> rule2)) -> rule5)) -> rule8) OR ((triple5 ((triple4 ((triple4) -> rule6)) -> rule5)) -> rule8))] Anne is young.[(triple7 OR ((triple1) -> rule7) OR ((triple6) -> rule4) OR ((((triple3) -> rule3)) -> rule4) OR ((((triple5 triple2) -> rule8)) -> rule4) OR ((((((triple4) -> rule2)) -> rule3)) -> rule4) OR ((((((triple4) -> rule6)) -> rule3)) -> rule4) OR ((((triple5 ((triple4 triple3) -> rule5)) -> rule8)) -> rule4) OR ((((triple5 ((triple4 ((triple4) -> rule2)) -> rule5)) -> rule8)) -> rule4) OR ((((triple5 ((triple4 ((triple4) -> rule6)) -> rule5)) -> rule8)) -> rule4))] Harry is big.[(triple8)] Harry is cold.[(triple9 OR ((triple10) -> rule2) OR ((triple10) -> rule6))] Harry is furry.[(triple10)] Harry is nice.[(triple11)] Harry is young.[(triple12 OR ((triple8) -> rule7))] @1: Harry is blue.[(((triple10 triple9) -> rule5) OR ((triple10 ((triple10) -> rule2)) -> rule5) OR ((triple10 ((triple10) -> rule6)) -> rule5))] Harry is round.[(((triple12) -> rule1) OR ((((triple8) -> rule7)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple4 triple3) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple4 ((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
((triple4) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((triple5 triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((triple4 triple3) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple5 ((triple4 ((triple4) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((triple5 ((triple4 ((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple1) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple6) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple5 triple2) -> (rule8 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple5 ((triple4 triple3) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((triple5 ((triple4 ((triple4) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
((((triple5 ((triple4 ((triple4) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple8) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple10 triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple10 ((triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple10 ((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple12) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple8) -> (rule7 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2