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