Harry is nice. Harry is round. Harry is young. Young, round people are red. Round people are green. If Harry is green then Harry is kind. Nice, kind people are red. Nice people are round. All kind, red people are nice.
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Young, round people are red.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If Harry is green then Harry is kind.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "kind" "+"))
Nice, kind people are red.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All kind, red people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule5))]
("Harry" "is" "round" "-")
triple2
((triple1) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
True
2
proof
[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))]
("Harry" "is" "green" "+")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not red.
False
3
inv-proof
[(((triple3 triple2) -> rule1) OR ((triple3 ((triple1) -> rule5)) -> rule1) OR ((triple1 ((((triple2) -> rule2)) -> rule3)) -> rule4) OR ((triple1 ((((((triple1) -> rule5)) -> rule2)) -> rule3)) -> rule4))]
("Harry" "is" "red" "-")
((triple3 triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple3 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple1 ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
@0: Harry is nice.[(triple1 OR ((((((triple2) -> rule2)) -> rule3) ((triple3 triple2) -> rule1)) -> rule6))] Harry is round.[(triple2 OR ((triple1) -> rule5))] Harry is young.[(triple3)] @1: Harry is green.[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] Harry is red.[(((triple3 triple2) -> rule1) OR ((triple3 ((triple1) -> rule5)) -> rule1) OR ((triple1 ((((triple2) -> rule2)) -> rule3)) -> rule4) OR ((triple1 ((((((triple1) -> rule5)) -> rule2)) -> rule3)) -> rule4))] @2: Harry is kind.[(((((triple2) -> rule2)) -> rule3) OR ((((((triple1) -> rule5)) -> rule2)) -> rule3))]
Harry is nice.
("Harry" "is" "nice" "+")
triple1
((((((triple2) -> (rule2 % int4))) -> (rule3 % int3)) ((triple3 triple2) -> (rule1 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
triple2
((triple1) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple2) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple3 triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple3 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple1 ((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3