Harry is blue. All round people are young. If Harry is round then Harry is rough. If Harry is white and Harry is rough then Harry is kind. Blue people are white. If Harry is blue and Harry is kind then Harry is young. Kind, white people are round. If someone is young and kind then they are blue. All white people are kind.
Harry is blue.
("Harry" "is" "blue" "+")
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If Harry is round then Harry is rough.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "rough" "+"))
If Harry is white and Harry is rough then Harry is kind.
((("Harry" "is" "white" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "kind" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Harry is blue and Harry is kind then Harry is young.
((("Harry" "is" "blue" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "young" "+"))
Kind, white people are round.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is young and kind then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Harry is blue.
True
1
proof
[(triple1)]
("Harry" "is" "blue" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple1)]
("Harry" "is" "blue" "-")
triple1
Harry is white.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "white" "+")
((triple1) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "white" "-")
((triple1) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule8))]
("Harry" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule8))]
("Harry" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
True
5
proof
[(((triple1 ((((triple1) -> rule4)) -> rule8)) -> rule5) OR ((((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule6)) -> rule1))]
("Harry" "is" "young" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is not round.
False
6
inv-proof
[(((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule6))]
("Harry" "is" "round" "-")
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
@0: Harry is blue.[(triple1)] @1: Harry is white.[(((triple1) -> rule4))] @2: Harry is kind.[(((((triple1) -> rule4)) -> rule8))] @3: Harry is round.[(((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule6))] Harry is young.[(((triple1 ((((triple1) -> rule4)) -> rule8)) -> rule5) OR ((((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule6)) -> rule1))] @4: Harry is rough.[(((((((((triple1) -> rule4)) -> rule8) ((triple1) -> rule4)) -> rule6)) -> rule2))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is white.
("Harry" "is" "white" "+")
((triple1) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2)) ((triple1) -> (rule4 % int3))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((((triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule8 % int3)) ((triple1) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4