Anne is big. Anne is cold. Anne is kind. Anne is rough. Anne is round. Anne is smart. Anne is young. Harry is cold. Harry is smart. Harry is young. Young things are rough. If Harry is rough then Harry is kind. If something is kind then it is rough. If Harry is big then Harry is kind. If Anne is cold and Anne is round then Anne is smart. All smart, kind things are big. Smart things are round. If Harry is young and Harry is cold then Harry is smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Harry is rough then Harry is kind.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "kind" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Harry is big then Harry is kind.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "kind" "+"))
If Anne is cold and Anne is round then Anne is smart.
((("Anne" "is" "cold" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "smart" "+"))
All smart, kind things are big.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If Harry is young and Harry is cold then Harry is smart.
((("Harry" "is" "young" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "smart" "+"))
Anne is kind.
True
1
proof
[(triple3)]
("Anne" "is" "kind" "+")
triple3
Anne is not young.
False
1
inv-proof
[(triple7)]
("Anne" "is" "young" "-")
triple7
Harry is rough.
True
2
proof
[(((triple10) -> rule1))]
("Harry" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple10) -> rule1))]
("Harry" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
True
3
proof
[(((((triple10) -> rule1)) -> rule2))]
("Harry" "is" "kind" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule2))]
("Harry" "is" "kind" "-")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
True
5
proof
[(((triple9 ((((triple10) -> rule1)) -> rule2)) -> rule6) OR ((((triple10 triple8) -> rule8) ((((triple10) -> rule1)) -> rule2)) -> rule6))]
("Harry" "is" "big" "+")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple10 triple8) -> (rule8 % int4)) ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is not big.
False
5
inv-proof
[(((triple9 ((((triple10) -> rule1)) -> rule2)) -> rule6) OR ((((triple10 triple8) -> rule8) ((((triple10) -> rule1)) -> rule2)) -> rule6))]
("Harry" "is" "big" "-")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple10 triple8) -> (rule8 % int4)) ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
@0: Anne is big.[(triple1 OR ((triple6 triple3) -> rule6) OR ((((triple2 triple5) -> rule5) triple3) -> rule6))] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is rough.[(triple4 OR ((triple3) -> rule3) OR ((triple7) -> rule1))] Anne is round.[(triple5 OR ((triple6) -> rule7))] Anne is smart.[(triple6 OR ((triple2 triple5) -> rule5))] Anne is young.[(triple7)] Harry is cold.[(triple8)] Harry is smart.[(triple9 OR ((triple10 triple8) -> rule8))] Harry is young.[(triple10)] @1: Harry is rough.[(((triple10) -> rule1))] Harry is round.[(((triple9) -> rule7) OR ((((triple10 triple8) -> rule8)) -> rule7))] @2: Harry is kind.[(((((triple10) -> rule1)) -> rule2))] @3: Harry is big.[(((triple9 ((((triple10) -> rule1)) -> rule2)) -> rule6) OR ((((triple10 triple8) -> rule8) ((((triple10) -> rule1)) -> rule2)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple6 triple3) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple2 triple5) -> (rule5 % int2)) triple3) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple3) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple7) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple6) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple2 triple5) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
((triple10 triple8) -> (rule8 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple9) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10 triple8) -> (rule8 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple9 ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple10 triple8) -> (rule8 % int4)) ((((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4