Harry is blue. Harry is nice. Harry is rough. Big things are quiet. If Harry is blue and Harry is quiet then Harry is green. If Harry is blue and Harry is big then Harry is green. All rough, big things are round. Round, rough things are big. Rough, blue things are round. If something is big and green then it is rough. All nice, green things are round.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Harry is blue and Harry is quiet then Harry is green.
((("Harry" "is" "blue" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
If Harry is blue and Harry is big then Harry is green.
((("Harry" "is" "blue" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "green" "+"))
All rough, big things are round.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Round, rough things are big.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Rough, blue things are round.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is big and green then it is rough.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All nice, green things are round.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Harry is nice.
True
1
proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Harry is not nice.
False
1
inv-proof
[(triple2)]
("Harry" "is" "nice" "-")
triple2
Harry is round.
True
3
proof
[(((triple3 triple1) -> rule6))]
("Harry" "is" "round" "+")
((triple3 triple1) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
3
inv-proof
[(((triple3 triple1) -> rule6))]
("Harry" "is" "round" "-")
((triple3 triple1) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
True
5
proof
[(((((triple3 triple1) -> rule6) triple3) -> rule5))]
("Harry" "is" "big" "+")
((((triple3 triple1) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not big.
False
5
inv-proof
[(((((triple3 triple1) -> rule6) triple3) -> rule5))]
("Harry" "is" "big" "-")
((((triple3 triple1) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
True
7
proof
[(((triple1 ((((triple3 triple1) -> rule6) triple3) -> rule5)) -> rule3) OR ((triple1 ((((((triple3 triple1) -> rule6) triple3) -> rule5)) -> rule1)) -> rule2))]
("Harry" "is" "green" "+")
((triple1 ((((triple3 triple1) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((triple1 ((((((triple3 triple1) -> (rule6 % int4)) triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is not quiet.
False
6
inv-proof
[(((((((triple3 triple1) -> rule6) triple3) -> rule5)) -> rule1))]
("Harry" "is" "quiet" "-")
((((((triple3 triple1) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
@0: Harry is blue.[(triple1)] Harry is nice.[(triple2)] Harry is rough.[(triple3)] @1: Harry is round.[(((triple3 triple1) -> rule6))] @2: Harry is big.[(((((triple3 triple1) -> rule6) triple3) -> rule5))] @3: Harry is green.[(((triple1 ((((triple3 triple1) -> rule6) triple3) -> rule5)) -> rule3) OR ((triple1 ((((((triple3 triple1) -> rule6) triple3) -> rule5)) -> rule1)) -> rule2))] Harry is quiet.[(((((((triple3 triple1) -> rule6) triple3) -> rule5)) -> rule1))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
((triple3 triple1) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple3 triple1) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple1 ((((triple3 triple1) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((triple1 ((((((triple3 triple1) -> (rule6 % int4)) triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple3 triple1) -> (rule6 % int3)) triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3