Charlie is blue. Charlie is furry. Charlie is quiet. Charlie is rough. Harry is blue. Harry is furry. Harry is green. Harry is kind. Harry is quiet. Harry is young. Green things are young. If something is quiet and rough then it is blue. All rough, kind things are green. Blue, quiet things are rough. All kind, young things are quiet. All green, rough things are quiet. If something is rough and young then it is green. If something is quiet then it is young.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something is quiet and rough then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All rough, kind things are green.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Blue, quiet things are rough.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All kind, young things are quiet.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All green, rough things are quiet.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is rough and young then it is green.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Harry is kind.
True
1
proof
[(triple8)]
("Harry" "is" "kind" "+")
triple8
Harry is not kind.
False
1
inv-proof
[(triple8)]
("Harry" "is" "kind" "-")
triple8
Charlie is young.
True
2
proof
[(((triple3) -> rule8))]
("Charlie" "is" "young" "+")
((triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple3) -> rule8))]
("Charlie" "is" "young" "-")
((triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is green.
True
4
proof
[(((triple4 ((triple3) -> rule8)) -> rule7) OR ((((triple1 triple3) -> rule4) ((triple3) -> rule8)) -> rule7))]
("Charlie" "is" "green" "+")
((triple4 ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple1 triple3) -> (rule4 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not green.
False
4
inv-proof
[(((triple4 ((triple3) -> rule8)) -> rule7) OR ((((triple1 triple3) -> rule4) ((triple3) -> rule8)) -> rule7))]
("Charlie" "is" "green" "-")
((triple4 ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple1 triple3) -> (rule4 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
@0: Charlie is blue.[(triple1 OR ((triple3 triple4) -> rule2))] Charlie is furry.[(triple2)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple4 OR ((triple1 triple3) -> rule4))] Harry is blue.[(triple5)] Harry is furry.[(triple6)] Harry is green.[(triple7 OR ((((triple5 triple9) -> rule4) triple10) -> rule7) OR ((((triple5 triple9) -> rule4) triple8) -> rule3) OR ((((triple5 triple9) -> rule4) ((triple9) -> rule8)) -> rule7) OR ((((triple5 ((triple8 triple10) -> rule5)) -> rule4) triple10) -> rule7) OR ((((triple5 ((triple8 triple10) -> rule5)) -> rule4) triple8) -> rule3) OR ((((triple5 ((triple8 triple10) -> rule5)) -> rule4) ((triple9) -> rule8)) -> rule7))] Harry is kind.[(triple8)] Harry is quiet.[(triple9 OR ((triple8 triple10) -> rule5) OR ((triple8 ((triple7) -> rule1)) -> rule5))] Harry is young.[(triple10 OR ((triple7) -> rule1) OR ((triple9) -> rule8) OR ((((((triple5 triple9) -> rule4) triple8) -> rule3)) -> rule1))] @1: Charlie is young.[(((triple3) -> rule8))] Harry is rough.[(((triple5 triple9) -> rule4) OR ((triple5 ((triple8 triple10) -> rule5)) -> rule4) OR ((triple5 ((triple8 ((triple7) -> rule1)) -> rule5)) -> rule4))] @2: Charlie is green.[(((triple4 ((triple3) -> rule8)) -> rule7) OR ((((triple1 triple3) -> rule4) ((triple3) -> rule8)) -> rule7))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple3 triple4) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((triple1 triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
((((triple5 triple9) -> (rule4 % int2)) triple10) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple5 triple9) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple5 triple9) -> (rule4 % int3)) ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((triple5 ((triple8 triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple10) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple5 ((triple8 triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple5 ((triple8 triple10) -> (rule5 % int4))) -> (rule4 % int3)) ((triple9) -> (rule8 % int2))) -> (rule7 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple8 triple10) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8 ((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple10
((triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple9) -> (rule8 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((((triple5 triple9) -> (rule4 % int3)) triple8) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple5 triple9) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple5 ((triple8 triple10) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple5 ((triple8 ((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((triple4 ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple1 triple3) -> (rule4 % int3)) ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3